aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing/g_vernac.ml4
diff options
context:
space:
mode:
Diffstat (limited to 'parsing/g_vernac.ml4')
-rw-r--r--parsing/g_vernac.ml4157
1 files changed, 82 insertions, 75 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 1a582b293..f347ac20e 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -6,11 +6,10 @@
(* * GNU Lesser General Public License Version 2.1 *)
(***********************************************************************)
-(*i camlp4deps: "parsing/grammar.cma" i*)
-
(* $Id$ *)
-open Coqast
+open Names
+open Topconstr
open Vernacexpr
open Pcoq
open Pp
@@ -26,7 +25,7 @@ let join_binders (idl,c) = List.map (fun id -> (id,c)) idl
open Genarg
-let evar_constr loc = <:ast< (ISEVAR) >>
+let evar_constr loc = CHole loc
(* Rem: do not join the different GEXTEND into one, it breaks native *)
(* compilation on PowerPC and Sun architectures *)
@@ -40,10 +39,10 @@ GEXTEND Gram
| g = gallina_ext; "." -> g
| c = command; "." -> c
| c = syntax; "." -> c
- | n = Prim.natural; ":"; v = goal_vernac; "." -> v n
+ | n = natural; ":"; v = goal_vernac; "." -> v n
| "["; l = vernac_list_tail -> VernacList l
(* This is for "Grammar vernac" rules *)
- | id = Prim.metaident -> VernacVar (Ast.nvar_of_ast id) ] ]
+ | id = METAIDENT -> VernacVar (Names.id_of_string id) ] ]
;
goal_vernac:
[ [ tac = Tactic.tactic -> fun n -> VernacSolve (n,tac)
@@ -71,8 +70,8 @@ GEXTEND Gram
] ]
;
constr_body:
- [ [ ":="; c = constr; ":"; t = constr -> <:ast< (CAST $c $t) >>
- | ":"; t = constr; ":="; c = constr -> <:ast< (CAST $c $t) >>
+ [ [ ":="; c = constr; ":"; t = constr -> CCast(loc,c,t)
+ | ":"; t = constr; ":="; c = constr -> CCast(loc,c,t)
| ":="; c = constr -> c ] ]
;
vernac_list_tail:
@@ -123,31 +122,34 @@ GEXTEND Gram
| ":" -> false ] ]
;
params:
- [ [ idl = LIST1 ident SEP ","; coe = of_type_with_opt_coercion; c = constr
+ [ [ idl = LIST1 base_ident SEP ","; coe = of_type_with_opt_coercion; c = constr
-> List.map (fun c -> (coe,c)) (join_binders (idl,c))
] ]
;
ne_params_list:
[ [ ll = LIST1 params SEP ";" -> List.flatten ll ] ]
;
-ident_comma_list_tail:
- [ [ ","; idl = LIST1 ident SEP "," -> idl | -> [] ] ]
+ name_comma_list_tail:
+ [ [ ","; nal = LIST1 name SEP "," -> nal | -> [] ] ]
+ ;
+ ident_comma_list_tail:
+ [ [ ","; nal = LIST1 base_ident SEP "," -> nal | -> [] ] ]
;
type_option:
[ [ ":"; c = constr -> c
| -> evar_constr loc ] ]
;
opt_casted_constr:
- [ [ c = constr; ":"; t = constr -> <:ast< (CAST $c $t) >>
+ [ [ c = constr; ":"; t = constr -> CCast(loc,c,t)
| c = constr -> c ] ]
;
vardecls:
- [ [ id = ident; idl = ident_comma_list_tail; c = type_option ->
- LocalRawAssum (id::idl,c)
- | id = ident; "="; c = opt_casted_constr ->
- LocalRawDef (id,c)
- | id = ident; ":="; c = opt_casted_constr ->
- LocalRawDef (id,c)
+ [ [ na = name; nal = name_comma_list_tail; c = type_option
+ -> LocalRawAssum (na::nal,c)
+ | na = name; "="; c = opt_casted_constr ->
+ LocalRawDef (na,c)
+ | na = name; ":="; c = opt_casted_constr ->
+ LocalRawDef (na,c)
] ]
;
binders:
@@ -172,9 +174,9 @@ ident_comma_list_tail:
;
gallina:
(* Definition, Theorem, Variable, Axiom, ... *)
- [ [ thm = thm_token; id = ident; bl = binders_list; ":"; c = constr ->
+ [ [ thm = thm_token; id = base_ident; bl = binders_list; ":"; c = constr ->
VernacStartTheoremProof (thm, id, (bl, c), false, (fun _ _ -> ()))
- | (f,d) = def_token; id = ident; b = def_body ->
+ | (f,d) = def_token; id = base_ident; b = def_body ->
VernacDefinition (d, id, b, f)
| stre = assumption_token; bl = ne_params_list ->
VernacAssumption (stre, bl)
@@ -192,7 +194,7 @@ ident_comma_list_tail:
[ [ IDENT "Record" -> () | IDENT "Structure" -> () ] ]
;
constructor:
- [ [ id = ident; coe = of_type_with_opt_coercion; c = constr ->
+ [ [ id = base_ident; coe = of_type_with_opt_coercion; c = constr ->
(coe,(id,c)) ] ]
;
ne_constructor_list:
@@ -209,7 +211,7 @@ ident_comma_list_tail:
| ind = oneind_old_style -> [ind] ] ]
;
oneind_old_style:
- [ [ id = ident; ":"; c = constr; ":="; lc = constructor_list ->
+ [ [ id = base_ident; ":"; c = constr; ":="; lc = constructor_list ->
(id,c,lc) ] ]
;
block:
@@ -217,7 +219,7 @@ ident_comma_list_tail:
| ind = oneind -> [ind] ] ]
;
oneind:
- [ [ id = ident; indpar = indpar; ":"; c = constr; ":=";
+ [ [ id = base_ident; indpar = indpar; ":"; c = constr; ":=";
lc = constructor_list -> (id,indpar,c,lc) ] ]
;
indpar:
@@ -229,7 +231,7 @@ ident_comma_list_tail:
| -> false ] ]
;
onescheme:
- [ [ id = ident; ":="; dep = dep; ind = qualid; IDENT "Sort";
+ [ [ id = base_ident; ":="; dep = dep; ind = global; IDENT "Sort";
s = sort -> (id,dep,ind,s) ] ]
;
schemes:
@@ -240,34 +242,34 @@ ident_comma_list_tail:
| IDENT "Minimality"; IDENT "for" -> false ] ]
;
onerec:
- [ [ id = ident; idl = ne_simple_binders_list; ":"; c = constr;
+ [ [ id = base_ident; idl = ne_fix_binders; ":"; c = constr;
":="; def = constr -> (id,idl,c,def) ] ]
;
specifrec:
[ [ l = LIST1 onerec SEP "with" -> l ] ]
;
onecorec:
- [ [ id = ident; ":"; c = constr; ":="; def = constr ->
+ [ [ id = base_ident; ":"; c = constr; ":="; def = constr ->
(id,c,def) ] ]
;
specifcorec:
[ [ l = LIST1 onecorec SEP "with" -> l ] ]
;
record_field:
- [ [ id = ident; oc = of_type_with_opt_coercion; t = constr ->
+ [ [ id = base_ident; oc = of_type_with_opt_coercion; t = constr ->
(oc,AssumExpr (id,t))
- | id = ident; oc = of_type_with_opt_coercion; t = constr;
+ | id = base_ident; oc = of_type_with_opt_coercion; t = constr;
":="; b = constr ->
(oc,DefExpr (id,b,Some t))
- | id = ident; ":="; b = constr ->
+ | id = base_ident; ":="; b = constr ->
(false,DefExpr (id,b,None)) ] ]
;
fields:
[ [ fs = LIST0 record_field SEP ";" -> fs ] ]
;
simple_params:
- [ [ idl = LIST1 ident SEP ","; ":"; c = constr -> join_binders (idl, c)
- | idl = LIST1 ident SEP "," -> join_binders (idl, evar_constr dummy_loc)
+ [ [ idl = LIST1 base_ident SEP ","; ":"; c = constr -> join_binders (idl, c)
+ | idl = LIST1 base_ident SEP "," -> join_binders (idl, evar_constr dummy_loc)
] ]
;
simple_binders:
@@ -276,8 +278,19 @@ ident_comma_list_tail:
ne_simple_binders_list:
[ [ bll = LIST1 simple_binders -> List.flatten bll ] ]
;
+ fix_params:
+ [ [ idl = LIST1 name SEP ","; ":"; c = constr -> (idl, c)
+ | idl = LIST1 name SEP "," -> (idl, evar_constr dummy_loc)
+ ] ]
+ ;
+ fix_binders:
+ [ [ "["; bll = LIST1 fix_params SEP ";"; "]" -> bll ] ]
+ ;
+ ne_fix_binders:
+ [ [ bll = LIST1 fix_binders -> List.flatten bll ] ]
+ ;
rec_constructor:
- [ [ c = ident -> Some c
+ [ [ c = base_ident -> Some c
| -> None ] ]
;
gallina_ext:
@@ -285,7 +298,7 @@ ident_comma_list_tail:
indl = block_old_style ->
let indl' = List.map (fun (id,ar,c) -> (id,bl,ar,c)) indl in
VernacInductive (f,indl')
- | record_token; oc = opt_coercion; name = ident; ps = indpar; ":";
+ | record_token; oc = opt_coercion; name = base_ident; ps = indpar; ":";
s = sort; ":="; c = rec_constructor; "{"; fs = fields; "}" ->
VernacRecord ((oc,name),ps,s,c,fs)
] ]
@@ -296,25 +309,25 @@ ident_comma_list_tail:
| "Fixpoint"; recs = specifrec -> VernacFixpoint recs
| "CoFixpoint"; corecs = specifcorec -> VernacCoFixpoint corecs
| IDENT "Scheme"; l = schemes -> VernacScheme l
- | f = finite_token; s = sort; id = ident; indpar = indpar; ":=";
+ | f = finite_token; s = csort; id = base_ident; indpar = indpar; ":=";
lc = constructor_list ->
VernacInductive (f,[id,indpar,s,lc])
| f = finite_token; indl = block ->
VernacInductive (f,indl) ] ]
;
+ csort:
+ [ [ s = sort -> CSort (loc,s) ] ]
+ ;
gallina_ext:
[ [
(* Sections *)
- IDENT "Section"; id = ident -> VernacBeginSection id
- | IDENT "Chapter"; id = ident -> VernacBeginSection id ] ]
-(* | IDENT "Module"; id = ident ->
- warning "Module is currently unsupported"; VernacNop *)
+ IDENT "Section"; id = base_ident -> VernacBeginSection id
+ | IDENT "Chapter"; id = base_ident -> VernacBeginSection id ] ]
;
module_vardecls: (* This is interpreted by Pcoq.abstract_binder *)
- [ [ id = ident; idl = ident_comma_list_tail;
- ":"; mty = Module.module_type ->
- (id::idl,mty) ] ]
+ [ [ id = base_ident; idl = ident_comma_list_tail; ":"; mty = Module.module_type
+ -> (id::idl,mty) ] ]
;
module_binders:
[ [ "["; bl = LIST1 module_vardecls SEP ";"; "]" -> bl ] ]
@@ -334,64 +347,64 @@ ident_comma_list_tail:
gallina_ext:
[ [
(* Interactive module declaration *)
- IDENT "Module"; id = ident; bl = module_binders_list;
+ IDENT "Module"; id = base_ident; bl = module_binders_list;
mty_o = OPT of_module_type; mexpr_o = OPT is_module_expr ->
VernacDeclareModule (id, bl, mty_o, mexpr_o)
- | IDENT "Module"; "Type"; id = ident;
+ | IDENT "Module"; "Type"; id = base_ident;
bl = module_binders_list; mty_o = OPT is_module_type ->
VernacDeclareModuleType (id, bl, mty_o)
(* This end a Section a Module or a Module Type *)
- | IDENT "End"; id = ident -> VernacEndSegment id
+ | IDENT "End"; id = base_ident -> VernacEndSegment id
(* Transparent and Opaque *)
- | IDENT "Transparent"; l = LIST1 qualid -> VernacSetOpacity (false, l)
- | IDENT "Opaque"; l = LIST1 qualid -> VernacSetOpacity (true, l)
+ | IDENT "Transparent"; l = LIST1 global -> VernacSetOpacity (false, l)
+ | IDENT "Opaque"; l = LIST1 global -> VernacSetOpacity (true, l)
(* Canonical structure *)
- | IDENT "Canonical"; IDENT "Structure"; qid = qualid ->
+ | IDENT "Canonical"; IDENT "Structure"; qid = global ->
VernacCanonical qid
- | IDENT "Canonical"; IDENT "Structure"; qid = qualid; d = def_body ->
- let s = Ast.coerce_qualid_to_id qid in
+ | IDENT "Canonical"; IDENT "Structure"; qid = global; d = def_body ->
+ let s = Ast.coerce_global_to_id qid in
VernacDefinition (Global,s,d,Recordobj.add_object_hook)
(* Rem: LOBJECT, OBJCOERCION, LOBJCOERCION have been removed
(they were unused and undocumented) *)
(* Coercions *)
- | IDENT "Coercion"; qid = qualid; d = def_body ->
- let s = Ast.coerce_qualid_to_id qid in
+ | IDENT "Coercion"; qid = global; d = def_body ->
+ let s = Ast.coerce_global_to_id qid in
VernacDefinition (Global,s,d,Class.add_coercion_hook)
- | IDENT "Coercion"; IDENT "Local"; qid = qualid; d = def_body ->
- let s = Ast.coerce_qualid_to_id qid in
+ | IDENT "Coercion"; IDENT "Local"; qid = global; d = def_body ->
+ let s = Ast.coerce_global_to_id qid in
VernacDefinition (Local,s,d,Class.add_coercion_hook)
- | IDENT "Identity"; IDENT "Coercion"; IDENT "Local"; f = Prim.ident;
+ | IDENT "Identity"; IDENT "Coercion"; IDENT "Local"; f = base_ident;
":"; s = class_rawexpr; ">->"; t = class_rawexpr ->
VernacIdentityCoercion (Local, f, s, t)
- | IDENT "Identity"; IDENT "Coercion"; f = Prim.ident; ":";
+ | IDENT "Identity"; IDENT "Coercion"; f = base_ident; ":";
s = class_rawexpr; ">->"; t = class_rawexpr ->
VernacIdentityCoercion (Global, f, s, t)
- | IDENT "Coercion"; IDENT "Local"; qid = qualid; ":";
+ | IDENT "Coercion"; IDENT "Local"; qid = global; ":";
s = class_rawexpr; ">->"; t = class_rawexpr ->
VernacCoercion (Local, qid, s, t)
- | IDENT "Coercion"; qid = qualid; ":"; s = class_rawexpr; ">->";
+ | IDENT "Coercion"; qid = global; ":"; s = class_rawexpr; ">->";
t = class_rawexpr ->
VernacCoercion (Global, qid, s, t)
- | IDENT "Class"; IDENT "Local"; c = qualid ->
+ | IDENT "Class"; IDENT "Local"; c = global ->
Pp.warning "Class is obsolete"; VernacNop
- | IDENT "Class"; c = qualid ->
+ | IDENT "Class"; c = global ->
Pp.warning "Class is obsolete"; VernacNop
(* Implicit *)
- | IDENT "Syntactic"; "Definition"; id = ident; ":="; c = constr;
+ | IDENT "Syntactic"; "Definition"; id = base_ident; ":="; c = constr;
n = OPT [ "|"; n = natural -> n ] ->
VernacSyntacticDefinition (id,c,n)
- | IDENT "Implicits"; qid = qualid; "["; l = LIST0 natural; "]" ->
+ | IDENT "Implicits"; qid = global; "["; l = LIST0 natural; "]" ->
VernacDeclareImplicits (qid,Some l)
- | IDENT "Implicits"; qid = qualid -> VernacDeclareImplicits (qid,None)
+ | IDENT "Implicits"; qid = global -> VernacDeclareImplicits (qid,None)
(* For compatibility *)
| IDENT "Implicit"; IDENT "Arguments"; IDENT "On" ->
@@ -436,23 +449,17 @@ GEXTEND Gram
<:ast< (CompileFile ($STR $verbosely) ($STR $only_spec)
($STR $mname) ($STR $fname))>>
*)
- | IDENT "Read"; IDENT "Module"; qidl = LIST1 qualid ->
+ | IDENT "Read"; IDENT "Module"; qidl = LIST1 global ->
VernacRequire (None, None, qidl)
| IDENT "Require"; export = export_token; specif = specif_token;
- qidl = LIST1 qualid -> VernacRequire (Some export, specif, qidl)
+ qidl = LIST1 global -> VernacRequire (Some export, specif, qidl)
| IDENT "Require"; export = export_token; specif = specif_token;
- id = Prim.ident; filename = STRING ->
+ id = base_ident; filename = STRING ->
VernacRequireFrom (export, specif, id, filename)
-(*
- | IDENT "Write"; IDENT "Module"; id = identarg -> ExtraVernac
- <:ast< (WriteModule $id) >>
- | IDENT "Write"; IDENT "Module"; id = identarg; s = stringarg -> ExtraVernac
- <:ast< (WriteModule $id $s) >>
-*)
| IDENT "Declare"; IDENT "ML"; IDENT "Module"; l = LIST1 STRING ->
VernacDeclareMLModule l
- | IDENT "Import"; qidl = LIST1 qualid -> VernacImport (false,qidl)
- | IDENT "Export"; qidl = LIST1 qualid -> VernacImport (true,qidl)
+ | IDENT "Import"; qidl = LIST1 global -> VernacImport (false,qidl)
+ | IDENT "Export"; qidl = LIST1 global -> VernacImport (true,qidl)
]
]
;
@@ -471,10 +478,10 @@ GEXTEND Gram
| IDENT "Restore"; IDENT "State"; s = STRING -> VernacRestoreState s
(* Resetting *)
- | IDENT "Reset"; id = Prim.ident -> VernacResetName id
+ | IDENT "Reset"; id = identref -> VernacResetName id
| IDENT "Reset"; IDENT "Initial" -> VernacResetInitial
| IDENT "Back" -> VernacBack 1
- | IDENT "Back"; n = Prim.natural -> VernacBack n
+ | IDENT "Back"; n = natural -> VernacBack n
(* Tactic Debugger *)
| IDENT "Debug"; IDENT "On" -> VernacDebug true
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-12 01:00:32 +0000