Merge pull request #120 from ott-lang/coq-notation

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

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 \\

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

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 
@@ -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 = "

src/grammar_typecheck.ml

@@ -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";

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.
+}}

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.
+}}