aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing
diff options
context:
space:
mode:
Diffstat (limited to 'parsing')
-rw-r--r--parsing/g_constr.ml497
-rw-r--r--parsing/g_ltac.ml44
-rw-r--r--parsing/g_vernac.ml433
-rw-r--r--parsing/pcoq.ml42
-rw-r--r--parsing/pcoq.mli4
-rw-r--r--parsing/ppvernac.ml7
6 files changed, 57 insertions, 90 deletions
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index ea8d532f9..25a7d0b69 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -23,7 +23,7 @@ open Util
let constr_kw =
[ "forall"; "fun"; "match"; "fix"; "cofix"; "with"; "in"; "for";
- "end"; "as"; "let"; "dest"; "if"; "then"; "else"; "return";
+ "end"; "as"; "let"; "if"; "then"; "else"; "return";
"Prop"; "Set"; "Type"; ".("; "_"; ".." ]
let _ = List.iter (fun s -> Lexer.add_token("",s)) constr_kw
@@ -129,7 +129,7 @@ let aliasvar = function CPatAlias (_, _, id) -> Some (Name id) | _ -> None
GEXTEND Gram
GLOBAL: binder_constr lconstr constr operconstr sort global
constr_pattern lconstr_pattern Constr.ident
- binder binder_let binders_let delimited_binder_let delimited_binders_let
+ binder binder_let binders_let
binders_let_fixannot typeclass_constraint pattern appl_arg;
Constr.ident:
[ [ id = Prim.ident -> id
@@ -210,7 +210,7 @@ GEXTEND Gram
mkCProdN loc bl c
| "fun"; bl = binder_list; "=>"; c = operconstr LEVEL "200" ->
mkCLambdaN loc bl c
- | "let"; id=name; bl = LIST0 binder_let; ty = type_cstr; ":=";
+ | "let"; id=name; bl = binders_let; ty = type_cstr; ":=";
c1 = operconstr LEVEL "200"; "in"; c2 = operconstr LEVEL "200" ->
let loc1 = loc_of_binder_let bl in
CLetIn(loc,id,mkCLambdaN loc1 bl (mk_cast(c1,ty)),c2)
@@ -273,13 +273,6 @@ GEXTEND Gram
[ [ id=identref; bl=binders_let_fixannot; ty=type_cstr; ":=";
c=operconstr LEVEL "200" -> (id,fst bl,snd bl,c,ty) ] ]
;
-(* fixannot: *)
-(* [ [ "{"; IDENT "struct"; id=name; "}" -> (Some id, CStructRec) *)
-(* | "{"; IDENT "wf"; rel=constr; id=OPT name; "}" -> (id, CWfRec rel) *)
-(* | "{"; IDENT "measure"; rel=constr; id=OPT name; "}" -> (id, CMeasureRec rel) *)
-(* | -> (None, CStructRec) *)
-(* ] ] *)
-(* ; *)
match_constr:
[ [ "match"; ci=LIST1 case_item SEP ","; ty=OPT case_type; "with";
br=branches; "end" -> CCases(loc,RegularStyle,ty,ci,br) ] ]
@@ -340,24 +333,13 @@ GEXTEND Gram
| s = string -> CPatPrim (loc, String s) ] ]
;
binder_list:
- [ [ idl=LIST1 name; bl=LIST0 binder_let ->
- LocalRawAssum (idl,Default Explicit,CHole (loc, Some (Evd.BinderType (snd (List.hd idl)))))::bl
- | idl=LIST1 name; ":"; c=lconstr ->
- [LocalRawAssum (idl,Default Explicit,c)]
- | cl = binders_let -> cl
+ [ [ idl=LIST1 name; bl=binders_let ->
+ LocalRawAssum (idl,Default Explicit,CHole (loc, Some (Evd.BinderType (snd (List.hd idl)))))::bl
+ | idl=LIST1 name; ":"; c=lconstr ->
+ [LocalRawAssum (idl,Default Explicit,c)]
+ | cl = binders_let -> cl
] ]
;
- delimited_binders_let:
- [ [ "["; ctx = LIST1 typeclass_constraint_binder SEP ","; "]"; bl=binders_let ->
- ctx @ bl
- | b = delimited_binder_let; cl = LIST0 binder_let -> b :: cl
- | -> [] ] ]
- ;
- binders_let:
- [ [ "["; ctx = LIST1 typeclass_constraint_binder SEP ","; "]"; bl=binders_let ->
- ctx @ bl
- | cl = LIST0 binder_let -> cl ] ]
- ;
binder_assum:
[ [ "}" -> fun id -> LocalRawAssum([id], Default Implicit, CHole(loc, None))
| idl=LIST1 name; ":"; c=lconstr; "}" ->
@@ -379,51 +361,34 @@ GEXTEND Gram
(assum (loc, Name id) :: fst bl), snd bl
| f = fixannot -> [], f
| b = binder_let; bl = binders_let_fixannot ->
- b :: fst bl, snd bl
+ b @ fst bl, snd bl
| -> [], (None, CStructRec)
] ]
;
-
+ binders_let:
+ [ [ b = binder_let; bl = binders_let -> b @ bl
+ | -> [] ] ]
+ ;
binder_let:
[ [ id=name ->
- LocalRawAssum ([id],Default Explicit,CHole (loc, None))
- | "("; id=name; idl=LIST1 name; ":"; c=lconstr; ")" ->
- LocalRawAssum (id::idl,Default Explicit,c)
- | "("; id=name; ":"; c=lconstr; ")" ->
- LocalRawAssum ([id],Default Explicit,c)
- | "{"; id=name; "}" ->
- LocalRawAssum ([id],Default Implicit,CHole (loc, None))
- | "{"; id=name; idl=LIST1 name; ":"; c=lconstr; "}" ->
- LocalRawAssum (id::idl,Default Implicit,c)
- | "{"; id=name; ":"; c=lconstr; "}" ->
- LocalRawAssum ([id],Default Implicit,c)
- | "{"; id=name; idl=LIST1 name; "}" ->
- LocalRawAssum (id::idl,Default Implicit,CHole (loc, None))
- | "("; id=name; ":="; c=lconstr; ")" ->
- LocalRawDef (id,c)
- | "("; id=name; ":"; t=lconstr; ":="; c=lconstr; ")" ->
- LocalRawDef (id,CCast (join_loc (constr_loc t) loc,c, CastConv (DEFAULTcast,t)))
- | "["; tc = typeclass_constraint_binder; "]" -> tc
- ] ]
- ;
- delimited_binder_let:
- [ [ "("; id=name; idl=LIST1 name; ":"; c=lconstr; ")" ->
- LocalRawAssum (id::idl,Default Explicit,c)
- | "("; id=name; ":"; c=lconstr; ")" ->
- LocalRawAssum ([id],Default Explicit,c)
- | "("; id=name; ":="; c=lconstr; ")" ->
- LocalRawDef (id,c)
- | "("; id=name; ":"; t=lconstr; ":="; c=lconstr; ")" ->
- LocalRawDef (id,CCast (join_loc (constr_loc t) loc,c, CastConv (DEFAULTcast,t)))
- | "{"; id=name; "}" ->
- LocalRawAssum ([id],Default Implicit,CHole (loc, None))
- | "{"; id=name; idl=LIST1 name; ":"; c=lconstr; "}" ->
- LocalRawAssum (id::idl,Default Implicit,c)
- | "{"; id=name; ":"; c=lconstr; "}" ->
- LocalRawAssum ([id],Default Implicit,c)
- | "{"; id=name; idl=LIST1 name; "}" ->
- LocalRawAssum (id::idl,Default Implicit,CHole (loc, None))
- | "["; tc = typeclass_constraint_binder; "]" -> tc
+ [LocalRawAssum ([id],Default Explicit,CHole (loc, None))]
+ | "("; id=name; idl=LIST1 name; ":"; c=lconstr; ")" ->
+ [LocalRawAssum (id::idl,Default Explicit,c)]
+ | "("; id=name; ":"; c=lconstr; ")" ->
+ [LocalRawAssum ([id],Default Explicit,c)]
+ | "("; id=name; ":="; c=lconstr; ")" ->
+ [LocalRawDef (id,c)]
+ | "("; id=name; ":"; t=lconstr; ":="; c=lconstr; ")" ->
+ [LocalRawDef (id,CCast (join_loc (constr_loc t) loc,c, CastConv (DEFAULTcast,t)))]
+ | "{"; id=name; "}" ->
+ [LocalRawAssum ([id],Default Implicit,CHole (loc, None))]
+ | "{"; id=name; idl=LIST1 name; ":"; c=lconstr; "}" ->
+ [LocalRawAssum (id::idl,Default Implicit,c)]
+ | "{"; id=name; ":"; c=lconstr; "}" ->
+ [LocalRawAssum ([id],Default Implicit,c)]
+ | "{"; id=name; idl=LIST1 name; "}" ->
+ List.map (fun id -> LocalRawAssum ([id],Default Implicit,CHole (loc, None))) (id::idl)
+ | "["; tc = LIST1 typeclass_constraint_binder SEP ","; "]" -> tc
] ]
;
binder:
diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4
index eefbe7da0..cd10e51f1 100644
--- a/parsing/g_ltac.ml4
+++ b/parsing/g_ltac.ml4
@@ -203,9 +203,9 @@ GEXTEND Gram
(* Definitions for tactics *)
tacdef_body:
- [ [ name = identref; it=LIST1 input_fun; redef = ltac_def_kind; body = tactic_expr ->
+ [ [ name = Constr.global; it=LIST1 input_fun; redef = ltac_def_kind; body = tactic_expr ->
(name, redef, TacFun (it, body))
- | name = identref; redef = ltac_def_kind; body = tactic_expr ->
+ | name = Constr.global; redef = ltac_def_kind; body = tactic_expr ->
(name, redef, body) ] ]
;
tactic:
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 3769d7b3e..4eafbd68c 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -157,7 +157,7 @@ GEXTEND Gram
;
gallina_ext:
[ [ b = record_token; oc = opt_coercion; name = identref;
- ps = LIST0 binder_let;
+ ps = binders_let;
s = [ ":"; s = lconstr -> s | -> CSort (loc,Rawterm.RType None) ];
":="; cstr = OPT identref; "{";
fs = LIST0 record_field SEP ";"; "}" ->
@@ -237,7 +237,7 @@ GEXTEND Gram
;
(* Inductives and records *)
inductive_definition:
- [ [ id = identref; indpar = LIST0 binder_let;
+ [ [ id = identref; indpar = binders_let;
c = [ ":"; c = lconstr -> c | -> CSort (loc,Rawterm.RType None) ];
":="; lc = constructor_list; ntn = decl_notation ->
((id,indpar,c,lc),ntn) ] ]
@@ -258,11 +258,11 @@ GEXTEND Gram
;
(* (co)-fixpoints *)
rec_definition:
- [ [ id = ident; b = binder_let;
+ [ [ id = ident;
bl = binders_let_fixannot;
ty = type_cstr;
":="; def = lconstr; ntn = decl_notation ->
- let bl, annot = (b :: fst bl, snd bl) in
+ let bl, annot = bl in
let names = names_of_local_assums bl in
let ni =
match fst annot with
@@ -282,7 +282,7 @@ GEXTEND Gram
((id,(ni,snd annot),bl,ty,def),ntn) ] ]
;
corec_definition:
- [ [ id = ident; bl = LIST0 binder_let; ty = type_cstr; ":=";
+ [ [ id = ident; bl = binders_let; ty = type_cstr; ":=";
def = lconstr; ntn = decl_notation ->
((id,bl,ty,def),ntn) ] ]
;
@@ -337,10 +337,10 @@ GEXTEND Gram
(oc,(idl,c)) ] ]
;
constructor:
- [ [ id = identref; l = LIST0 binder_let;
+ [ [ id = identref; l = binders_let;
coe = of_type_with_opt_coercion; c = lconstr ->
(coe,(id,mkCProdN loc l c))
- | id = identref; l = LIST0 binder_let ->
+ | id = identref; l = binders_let ->
(false,(id,mkCProdN loc l (CHole (loc, None)))) ] ]
;
of_type_with_opt_coercion:
@@ -485,7 +485,7 @@ GEXTEND Gram
VernacClass (qid, pars, s, [], props)
(* Type classes *)
- | IDENT "Class"; sup = OPT [ l = delimited_binders_let; "=>" -> l ];
+ | IDENT "Class"; sup = OPT [ l = binders_let; "=>" -> l ];
qid = identref; pars = binders_let;
s = [ ":"; c = sort -> Some (loc, c) | -> None ];
props = typeclass_field_types ->
@@ -493,15 +493,20 @@ GEXTEND Gram
| IDENT "Context"; c = typeclass_context ->
VernacContext c
-
+
| global = [ IDENT "Global" -> true | -> false ];
- IDENT "Instance"; sup = OPT [ l = delimited_binders_let ; "=>" -> l ];
- is = typeclass_constraint ; pri = OPT [ "|"; i = natural -> i ] ; props = typeclass_field_defs ->
+ IDENT "Instance"; name = OPT identref; sup = OPT [ l = binders_let -> l ];
+(* name' = OPT [ "=>"; id = identref -> id ]; *)
+ ":" ; expl = [ "!" -> Rawterm.Implicit | -> Rawterm.Explicit ] ; t = operconstr LEVEL "200";
+ pri = OPT [ "|"; i = natural -> i ] ; props = typeclass_field_defs ->
let sup = match sup with None -> [] | Some l -> l in
let is = (* We reverse the default binding mode on the right *)
- let n, bk, t = is in
- n, (match bk with Rawterm.Implicit -> Rawterm.Explicit
- | Rawterm.Explicit -> Rawterm.Implicit), t
+ let n =
+ match name with
+ | Some (loc, id) -> (loc, Name id)
+ | None -> (dummy_loc, Anonymous)
+ in
+ n, expl, t
in
VernacInstance (global, sup, is, props, pri)
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index 481b73fd0..01b309f3c 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -442,10 +442,8 @@ module Constr =
let lconstr_pattern = gec_constr "lconstr_pattern"
let binder = Gram.Entry.create "constr:binder"
let binder_let = Gram.Entry.create "constr:binder_let"
- let delimited_binder_let = Gram.Entry.create "constr:delimited_binder_let"
let binders_let = Gram.Entry.create "constr:binders_let"
let binders_let_fixannot = Gram.Entry.create "constr:binders_let_fixannot"
- let delimited_binders_let = Gram.Entry.create "constr:delimited_binders_let"
let typeclass_constraint = Gram.Entry.create "constr:typeclass_constraint"
let appl_arg = Gram.Entry.create "constr:appl_arg"
end
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 6f6cff275..2525c430a 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -163,11 +163,9 @@ module Constr :
val constr_pattern : constr_expr Gram.Entry.e
val lconstr_pattern : constr_expr Gram.Entry.e
val binder : (name located list * binder_kind * constr_expr) Gram.Entry.e
- val binder_let : local_binder Gram.Entry.e
- val delimited_binder_let : local_binder Gram.Entry.e
+ val binder_let : local_binder list Gram.Entry.e
val binders_let : local_binder list Gram.Entry.e
val binders_let_fixannot : (local_binder list * (identifier located option * recursion_order_expr)) Gram.Entry.e
- val delimited_binders_let : local_binder list Gram.Entry.e
val typeclass_constraint : (name located * binding_kind * constr_expr) Gram.Entry.e
val appl_arg : (constr_expr * explicitation located option) Gram.Entry.e
end
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index 535a4c380..bd87e09c6 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -50,7 +50,7 @@ let pr_lname = function
(loc,Name id) -> pr_lident (loc,id)
| lna -> pr_located pr_name lna
-let pr_ltac_id = Nameops.pr_id
+let pr_ltac_id = Libnames.pr_reference
let pr_module = Libnames.pr_reference
@@ -795,13 +795,14 @@ let rec pr_vernac = function
match body with
| Tacexpr.TacFun (idl,b) -> idl,b
| _ -> [], body in
- pr_located pr_ltac_id id ++
+ pr_ltac_id id ++
prlist (function None -> str " _"
| Some id -> spc () ++ pr_id id) idl
++ (if redef then str" ::=" else str" :=") ++ brk(1,1) ++
let idl = List.map Option.get (List.filter (fun x -> not (x=None)) idl)in
pr_raw_tactic_env
- (idl @ List.map snd (List.map (fun (x, _, _) -> x) l))
+ (idl @ List.map coerce_global_to_id
+ (List.map (fun (x, _, _) -> x) (List.filter (fun (_, redef, _) -> not redef) l)))
(Global.env())
body in
hov 1
generated by cgit v1.2.3 (git 2.39.1) at 2024-09-16 09:27:20 +0000