Skip to content

Add coq-notation hom to replace Definition with Notation in generated Coq #120

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
palmskog merged 3 commits into from
Dec 30, 2024
Merged

Add coq-notation hom to replace Definition with Notation in generated Coq #120

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
dfbee45
add coq-notation hom for metavars that replaces Definition with Notat…
palmskog Dec 28, 2024
9fd9d8d
add coq-notation hom for rules that replaces Definition with Notation…
palmskog Dec 28, 2024
8a46822
add documentation and revision history on coq-notation hom
palmskog Dec 28, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 2 additions & 0 deletions doc/top2.mng
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3612,6 +3612,7 @@ file. The table below summarises their meanings. A \tick{} indicates that argum
\mykw{tex} & \tick & \myLaTeX{} typesetting for symbolic variables \\
\mykw{com} & & comment to appear in \myLaTeX{} syntax definition \\
\mykw{coq-equality} & & Coq proof script to decide equality over the representation type \\
\mykw{coq-notation} & & Coq sentence using \texttt{Notation} for the representation type \\
\mykw{coq-universe} & & Coq universe (e.g.~\texttt{Type}) for the representation type \\
\mykw{repr-locally-nameless} & & (Coq only) use a locally-nameless representation \\
\mykw{phantom} & & suppress the representation type definition in theorem prover output \\
Expand All @@ -3637,6 +3638,7 @@ file. The table below summarises their meanings. A \tick{} indicates that argum
\mykw{tex} & \tick & \myLaTeX{} typesetting for symbolic variables \\
\mykw{com} & \tick & comment to appear in \myLaTeX{} syntax definition \\
\mykw{coq-equality} & & Coq proof script to decide equality over the representation type \\
\mykw{coq-notation} & & Coq sentence using \texttt{Notation} for the representation type \\
\mykw{coq-universe} & & Coq universe (e.g.~\texttt{Type}) for the representation type \\
\mykw{phantom} & & suppress the representation type definition in theorem prover output \\
\mykw{aux} & (\tick)& construct an auxiliary grammar rule with a single production \\
Expand Down
2 changes: 2 additions & 0 deletions revision_history.txt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -575,3 +575,5 @@ Peter Sewell + Thibaut Pérami: Add "menhir-start-type" hom to specify the top l
2024-12 @palmskog: add explicit locality to generated Coq Hint commands

2024-12 @palmskog: move y2l to non-aux directory to avoid Windows problems, fix doc build

2024-12 @palmskog: add coq-notation hom to allow using Coq Notation sentences instead of Definition
38 changes: 26 additions & 12 deletions src/grammar_pp.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1273,10 +1273,20 @@ and pp_metavardefn m xd mvd =
| true -> ""
| false -> ( match m with
| Coq co ->
let type_name = pp_metavarroot_ty m xd mvd.mvd_name in
let universe = try pp_hom_spec m xd (List.assoc "coq-universe" mvd.mvd_rep) with Not_found -> "Set" in
"Definition " ^ type_name ^ " : " ^ universe ^ " := "
^ (pp_metavarrep m xd mvd.mvd_rep type_name mvd.mvd_loc) ^ "." ^ pp_com ^ "\n"
let type_name = pp_metavarroot_ty m xd mvd.mvd_name in
let universe =
try pp_hom_spec m xd (List.assoc "coq-universe" mvd.mvd_rep)
with Not_found -> "Set"
in
let body = pp_metavarrep m xd mvd.mvd_rep type_name mvd.mvd_loc in
let sentence =
if List.mem_assoc "coq-notation" mvd.mvd_rep then
"Notation " ^ type_name ^ " := (" ^ body ^ " : " ^ universe ^ ")."
else
"Definition " ^ type_name ^ " : " ^ universe ^ " := " ^ body ^ "."
in
sentence
^ pp_com ^ "\n"
^ coq_maybe_decide_equality m xd mvd.mvd_rep (Mvr mvd.mvd_name) mvd.mvd_loc
| Caml oo ->
let type_name = pp_metavarroot_ty m xd mvd.mvd_name in
Expand Down Expand Up @@ -2740,14 +2750,18 @@ and pp_rule_list m xd rs =
^ pp_nontermroot_ty m xd ntr ^ " = ``:"
^ pp_hom_spec m xd hs
^ "``\n"
| Coq _ ->
let universe =
try pp_hom_spec m xd (List.assoc "coq-universe" (Auxl.rule_of_ntr xd ntr).rule_homs)
with Not_found -> "Set" in
"\nDefinition "
^ pp_nontermroot_ty m xd ntr ^ " : " ^ universe ^ " := "
^ pp_hom_spec m xd hs
^ ".\n"
| Coq _ ->
let homs = (Auxl.rule_of_ntr xd ntr).rule_homs in
let type_name = pp_nontermroot_ty m xd ntr in
let universe =
try pp_hom_spec m xd (List.assoc "coq-universe" homs)
with Not_found -> "Set"
in
let body = pp_hom_spec m xd hs in
if List.mem_assoc "coq-notation" homs then
"\nNotation " ^ type_name ^ " := (" ^ body ^ " : " ^ universe ^ ").\n"
else
"\nDefinition " ^ type_name ^ " : " ^ universe ^ " := " ^ body ^ ".\n"
| Twf _ ->
"\n%abbrev "
^ pp_nontermroot_ty m xd ntr ^ " : type = "
Expand Down
4 changes: 2 additions & 2 deletions src/grammar_typecheck.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -406,9 +406,9 @@ let allowable_hom_data =
[
( Hu_root , (["isa";"coq";"hol";"lem";(*"twf";*)"tex";"ocaml"],
"nonterminal, metavar or indexvar root"));
( Hu_metavar , (["isa";"coq";"hol";"lem";(*"twf";*)"tex";"ocaml";"com";"coq-equality";"coq-universe";"lex";"texvar";"isavar";"holvar";"lemvar";"ocamlvar";"repr-locally-nameless";(*"repr-nominal";*)"phantom";"ocamllex";"ocamllex-remove";"ocamllex-of-string";"pp";"pp-raw";"pp-suppress"],
( Hu_metavar , (["isa";"coq";"hol";"lem";(*"twf";*)"tex";"ocaml";"com";"coq-equality";"coq-notation";"coq-universe";"lex";"texvar";"isavar";"holvar";"lemvar";"ocamlvar";"repr-locally-nameless";(*"repr-nominal";*)"phantom";"ocamllex";"ocamllex-remove";"ocamllex-of-string";"pp";"pp-raw";"pp-suppress"],
"metavar declaration"));
( Hu_rule , (["isa";"coq";"hol";"lem";(*"twf";*)"tex";"ocaml";"com";"coq-equality";"coq-universe";(*"icht";*)"icho";"ichlo";"ich";"ichl";"ic";"ch";"ih";"phantom";"aux";"auxparam";"menhir-start";"menhir-start-type";"quotient-with";"pp";"pp-raw";"pp-suppress";"pp-params";"lex-comment"],
( Hu_rule , (["isa";"coq";"hol";"lem";(*"twf";*)"tex";"ocaml";"com";"coq-equality";"coq-notation";"coq-universe";(*"icht";*)"icho";"ichlo";"ich";"ichl";"ic";"ch";"ih";"phantom";"aux";"auxparam";"menhir-start";"menhir-start-type";"quotient-with";"pp";"pp-raw";"pp-suppress";"pp-params";"lex-comment"],
"rule"));
( Hu_rule_meta, (["com"], "special rule"));
( Hu_prod , (["isa";"coq";"hol";"lem";(*"twf";*)"tex";"texlong";"ocaml";"com";"order";"isasyn";"isaprec";(*"icht";*)"icho";"ichlo";"ich";"ichl";"ic";"ch";"ih";
Expand Down
14 changes: 14 additions & 0 deletions tests/gmap1.ott
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,14 @@
embed
{{ coq
From stdpp Require Import gmap.
}}
metavar context ::=
{{ coq gmap nat nat }}
{{ coq-universe Type }}
{{ coq-notation }}
embed
{{ coq
Fact insert_lookup_ne_context: forall (C:context) i j x y,
i <> j -> C !! i = Some x -> <[j:=y]> C !! i = Some x.
Proof. by intros; simplify_map_eq. Qed.
}}
17 changes: 17 additions & 0 deletions tests/gmap2.ott
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,17 @@
embed
{{ coq
From stdpp Require Import gmap.
}}
grammar
context :: context_ ::=
{{ coq gmap nat nat }}
{{ coq-universe Type }}
{{ coq-notation }}
| [] :: M :: empty
{{ coq GMap GEmpty }}
embed
{{ coq
Fact insert_lookup_ne_context: forall (C:context) i j x y,
i <> j -> C !! i = Some x -> <[j:=y]> C !! i = Some x.
Proof. by intros; simplify_map_eq. Qed.
}}
Loading