From dfbee457fb846fd1acfa8417626983f374d4a421 Mon Sep 17 00:00:00 2001 From: Karl Palmskog Date: Sat, 28 Dec 2024 15:26:58 +0100 Subject: [PATCH 1/3] add coq-notation hom for metavars that replaces Definition with Notation in generated Coq code --- src/grammar_pp.ml | 18 ++++++++++++++---- src/grammar_typecheck.ml | 2 +- tests/gmap1.ott | 14 ++++++++++++++ 3 files changed, 29 insertions(+), 5 deletions(-) create mode 100644 tests/gmap1.ott diff --git a/src/grammar_pp.ml b/src/grammar_pp.ml index 1b7f633..1721642 100644 --- a/src/grammar_pp.ml +++ b/src/grammar_pp.ml @@ -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 diff --git a/src/grammar_typecheck.ml b/src/grammar_typecheck.ml index 66a8a51..334f0be 100644 --- a/src/grammar_typecheck.ml +++ b/src/grammar_typecheck.ml @@ -406,7 +406,7 @@ 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"], "rule")); diff --git a/tests/gmap1.ott b/tests/gmap1.ott new file mode 100644 index 0000000..ff409dd --- /dev/null +++ b/tests/gmap1.ott @@ -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. +}} From 9fd9d8d2222a33fd57c696183c4fbde517d30cad Mon Sep 17 00:00:00 2001 From: Karl Palmskog Date: Sat, 28 Dec 2024 16:32:45 +0100 Subject: [PATCH 2/3] add coq-notation hom for rules that replaces Definition with Notation in generated Coq code --- src/grammar_pp.ml | 20 ++++++++++++-------- src/grammar_typecheck.ml | 2 +- tests/gmap2.ott | 17 +++++++++++++++++ 3 files changed, 30 insertions(+), 9 deletions(-) create mode 100644 tests/gmap2.ott diff --git a/src/grammar_pp.ml b/src/grammar_pp.ml index 1721642..022f697 100644 --- a/src/grammar_pp.ml +++ b/src/grammar_pp.ml @@ -2750,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 = " diff --git a/src/grammar_typecheck.ml b/src/grammar_typecheck.ml index 334f0be..48c1b59 100644 --- a/src/grammar_typecheck.ml +++ b/src/grammar_typecheck.ml @@ -408,7 +408,7 @@ let allowable_hom_data = "nonterminal, metavar or indexvar root")); ( 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"; diff --git a/tests/gmap2.ott b/tests/gmap2.ott new file mode 100644 index 0000000..e2190df --- /dev/null +++ b/tests/gmap2.ott @@ -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. +}} From 8a46822ce42fa5eef94c8c07fb7c7b1574101e97 Mon Sep 17 00:00:00 2001 From: Karl Palmskog Date: Sat, 28 Dec 2024 17:03:36 +0100 Subject: [PATCH 3/3] add documentation and revision history on coq-notation hom --- doc/top2.mng | 2 ++ revision_history.txt | 2 ++ 2 files changed, 4 insertions(+) diff --git a/doc/top2.mng b/doc/top2.mng index 3923ad3..b243dd3 100644 --- a/doc/top2.mng +++ b/doc/top2.mng @@ -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 \\ @@ -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 \\ diff --git a/revision_history.txt b/revision_history.txt index 157a6ba..7dd0801 100644 --- a/revision_history.txt +++ b/revision_history.txt @@ -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