aboutsummaryrefslogtreecommitdiff
path: root/parsing
diff options
context:
space:
mode:
Diffstat (limited to 'parsing')
-rw-r--r--parsing/g_constr.ml4107
-rw-r--r--parsing/g_proofs.ml43
-rw-r--r--parsing/g_vernac.ml423
-rw-r--r--parsing/pcoq.ml41
-rw-r--r--parsing/pcoq.mli1
-rw-r--r--parsing/ppvernac.ml7
6 files changed, 88 insertions, 54 deletions
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 9972d9e248..68389c54a4 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -99,10 +99,34 @@ let lpar_id_coloneq =
| _ -> raise Stream.Failure)
| _ -> raise Stream.Failure)
+let impl_ident =
+ Gram.Entry.of_parser "impl_ident"
+ (fun strm ->
+ match Stream.npeek 1 strm with
+ | [("IDENT",("wf"|"struct"|"measure"))] ->
+ raise Stream.Failure
+ | [("IDENT",s)] ->
+ Stream.junk strm;
+ Names.id_of_string s
+ | _ -> raise Stream.Failure)
+
+let ident_eq =
+ Gram.Entry.of_parser "ident_eq"
+ (fun strm ->
+ match Stream.npeek 1 strm with
+ | [("IDENT",s)] ->
+ (match Stream.npeek 2 strm with
+ | [_; ("", ":")] ->
+ Stream.junk strm; Stream.junk strm;
+ Names.id_of_string s
+ | _ -> raise Stream.Failure)
+ | _ -> raise Stream.Failure)
+
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 typeclass_constraint pattern;
+ binder binder_let binders_let delimited_binder_let delimited_binders_let
+ binders_let_fixannot typeclass_constraint pattern;
Constr.ident:
[ [ id = Prim.ident -> id
@@ -244,16 +268,16 @@ GEXTEND Gram
| "cofix" -> false ] ]
;
fix_decl:
- [ [ id=identref; bl=LIST0 binder_let; ann=fixannot; ty=type_cstr; ":=";
- c=operconstr LEVEL "200" -> (id,bl,ann,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)
- ] ]
- ;
+ [ [ 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,ty,ci,br) ] ]
@@ -332,53 +356,62 @@ GEXTEND Gram
ctx @ bl
| cl = LIST0 binder_let -> cl ] ]
;
+ binders_let_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)
+ | b = binder_let; bl = binders_let_fixannot ->
+ b :: fst bl, snd bl
+ | -> [], (None, CStructRec)
+ ] ]
+ ;
+
binder_let:
[ [ id=name ->
LocalRawAssum ([id],Default Explicit,CHole (loc, None))
- | "("; id=name; idl=LIST1 name; ":"; c=lconstr; ")" ->
+ | "("; id=name; idl=LIST1 name; ":"; c=lconstr; ")" ->
LocalRawAssum (id::idl,Default Explicit,c)
- | "("; id=name; ":"; c=lconstr; ")" ->
+ | "("; id=name; ":"; c=lconstr; ")" ->
LocalRawAssum ([id],Default Explicit,c)
- | "`"; id=name; "`" ->
+ | "{"; id=name; "}" ->
LocalRawAssum ([id],Default Implicit,CHole (loc, None))
- | "`"; id=name; idl=LIST1 name; ":"; c=lconstr; "`" ->
+ | "{"; id=name; idl=LIST1 name; ":"; c=lconstr; "}" ->
LocalRawAssum (id::idl,Default Implicit,c)
- | "`"; id=name; ":"; c=lconstr; "`" ->
+ | "{"; id=name; ":"; c=lconstr; "}" ->
LocalRawAssum ([id],Default Implicit,c)
- | "`"; id=name; idl=LIST1 name; "`" ->
+ | "{"; 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; ")" ->
+ | "("; id=name; ":"; t=lconstr; ":="; c=lconstr; ")" ->
LocalRawDef (id,CCast (join_loc (constr_loc t) loc,c, CastConv (DEFAULTcast,t)))
| "["; tc = typeclass_constraint_binder; "]" -> tc
] ]
-(* | b = delimited_binder_let -> b ] ] *)
;
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; "`" ->
- 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)))
+ | "{"; 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
] ]
;
binder:
[ [ id=name -> ([id],Default Explicit,CHole (loc, None))
| "("; idl=LIST1 name; ":"; c=lconstr; ")" -> (idl,Default Explicit,c)
- | "`"; idl=LIST1 name; ":"; c=lconstr; "`" -> (idl,Default Implicit,c)
+ | "{"; idl=LIST1 name; ":"; c=lconstr; "}" -> (idl,Default Implicit,c)
] ]
;
typeclass_constraint_binder:
@@ -388,22 +421,22 @@ GEXTEND Gram
] ]
;
typeclass_constraint:
- [ [ id=identref ; cl = LIST0 typeclass_param ->
- (loc, Anonymous), Explicit, CApp (loc, (None, mkIdentC (snd id)), cl)
- | "?" ; id=identref ; cl = LIST0 typeclass_param ->
- (loc, Anonymous), Implicit, CApp (loc, (None, mkIdentC (snd id)), cl)
- | iid=identref ; ":" ; id=typeclass_name ; cl = LIST0 typeclass_param ->
- (fst iid, Name (snd iid)), (fst id), CApp (loc, (None, mkIdentC (snd (snd id))), cl)
+ [ [ "!" ; qid=global ; cl = LIST0 typeclass_param ->
+ (loc, Anonymous), Explicit, CApp (loc, (None, mkRefC qid), cl)
+ | iid=ident_eq ; qid=typeclass_name ; cl = LIST0 typeclass_param ->
+ (loc, Name iid), (fst qid), CApp (loc, (None, mkRefC (snd qid)), cl)
+ | qid=global ; cl = LIST0 typeclass_param ->
+ (loc, Anonymous), Implicit, CApp (loc, (None, mkRefC qid), cl)
] ]
;
typeclass_name:
- [ [ id=identref -> (Explicit, id)
- | "?"; id = identref -> (Implicit, id)
+ [ [ id=global -> (Implicit, id)
+ | "!"; id=global -> (Explicit, id)
] ]
;
typeclass_param:
- [ [ id = identref -> CRef (Libnames.Ident id), None
+ [ [ id = global -> CRef id, None
| c = sort -> CSort (loc, c), None
| id = lpar_id_coloneq; c=lconstr; ")" ->
(c,Some (loc,ExplByName id))
diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4
index 796636c0e0..32a2427ed1 100644
--- a/parsing/g_proofs.ml4
+++ b/parsing/g_proofs.ml4
@@ -105,7 +105,8 @@ GEXTEND Gram
[ [ IDENT "Local" -> true | -> false ] ]
;
hint:
- [ [ IDENT "Resolve"; lc = LIST1 constr -> HintsResolve lc
+ [ [ IDENT "Resolve"; lc = LIST1 constr; n = OPT [ n = natural -> n ] ->
+ HintsResolve (List.map (fun x -> (n, x)) lc)
| IDENT "Immediate"; lc = LIST1 constr -> HintsImmediate lc
| IDENT "Unfold"; lqid = LIST1 global -> HintsUnfold lqid
| IDENT "Constructors"; lc = LIST1 global -> HintsConstructors lc
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 5c34f2e884..3b67407311 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -256,17 +256,19 @@ GEXTEND Gram
;
(* (co)-fixpoints *)
rec_definition:
- [ [ id = ident; bl = LIST1 binder_let;
- annot = rec_annotation; ty = type_cstr;
+ [ [ id = ident; b = binder_let;
+ bl = binders_let_fixannot;
+ ty = type_cstr;
":="; def = lconstr; ntn = decl_notation ->
+ let bl, annot = (b :: fst bl, snd bl) in
let names = List.map snd (names_of_local_assums bl) in
let ni =
match fst annot with
- Some id ->
- (try Some (list_index0 (Name id) names)
+ Some (_, id) ->
+ (try Some (list_index0 id names)
with Not_found -> Util.user_err_loc
(loc,"Fixpoint",
- Pp.str "No argument named " ++ Nameops.pr_id id))
+ Pp.str "No argument named " ++ Nameops.pr_name id))
| None ->
(* If there is only one argument, it is the recursive one,
otherwise, we search the recursive index later *)
@@ -279,13 +281,6 @@ GEXTEND Gram
def = lconstr; ntn = decl_notation ->
((id,bl,ty,def),ntn) ] ]
;
- rec_annotation:
- [ [ "{"; IDENT "struct"; id=IDENT; "}" -> (Some (id_of_string id), CStructRec)
- | "{"; IDENT "wf"; rel=constr; id=OPT IDENT; "}" -> (Option.map id_of_string id, CWfRec rel)
- | "{"; IDENT "measure"; rel=constr; id=OPT IDENT; "}" -> (Option.map id_of_string id, CMeasureRec rel)
- | -> (None, CStructRec)
- ] ]
- ;
type_cstr:
[ [ ":"; c=lconstr -> c
| -> CHole (loc, None) ] ]
@@ -495,9 +490,9 @@ GEXTEND Gram
VernacContext c
| IDENT "Instance"; sup = OPT [ l = delimited_binders_let ; "=>" -> l ];
- is = typeclass_constraint ; props = typeclass_field_defs ->
+ is = typeclass_constraint ; pri = OPT [ "|"; i = natural -> i ] ; props = typeclass_field_defs ->
let sup = match sup with None -> [] | Some l -> l in
- VernacInstance (sup, is, props)
+ VernacInstance (sup, is, props, pri)
| IDENT "Existing"; IDENT "Instance"; is = identref -> VernacDeclareInstance is
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index 68ddc19292..9976e07cc8 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -436,6 +436,7 @@ module Constr =
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"
end
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index d5cffd35bd..4fb9d03594 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -165,6 +165,7 @@ module Constr :
val binder_let : local_binder Gram.Entry.e
val delimited_binder_let : local_binder Gram.Entry.e
val binders_let : local_binder list Gram.Entry.e
+ val binders_let_fixannot : (local_binder list * (name 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
end
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index 0daccbba53..92d56e078d 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -191,7 +191,10 @@ let pr_hints local db h pr_c pr_pat =
let pph =
match h with
| HintsResolve l ->
- str "Resolve " ++ prlist_with_sep sep pr_c l
+ str "Resolve " ++ prlist_with_sep sep
+ (fun (pri, c) -> pr_c c ++
+ match pri with Some x -> spc () ++ str"(" ++ int x ++ str")" | None -> mt ())
+ l
| HintsImmediate l ->
str"Immediate" ++ spc() ++ prlist_with_sep sep pr_c l
| HintsUnfold l ->
@@ -703,7 +706,7 @@ let rec pr_vernac = function
prlist_with_sep (fun () -> str";" ++ spc())
(fun (lid,oc,c) -> pr_lident_constr ((if oc then str" :>" else str" :") ++ spc()) (lid,c)) props )
- | VernacInstance (sup, (instid, bk, cl), props) ->
+ | VernacInstance (sup, (instid, bk, cl), props, pri) ->
hov 1 (
str"Instance" ++ spc () ++
pr_and_type_binders_arg sup ++
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-28 15:08:11 +0000