aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing
diff options
context:
space:
mode:
Diffstat (limited to 'parsing')
-rw-r--r--parsing/egramcoq.ml8
-rw-r--r--parsing/g_constr.ml449
-rw-r--r--parsing/g_vernac.ml46
-rw-r--r--parsing/pcoq.mli10
4 files changed, 38 insertions, 35 deletions
diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml
index 07e4ddf84..496b20002 100644
--- a/parsing/egramcoq.ml
+++ b/parsing/egramcoq.ml
@@ -233,11 +233,11 @@ type (_, _) entry =
| TTName : ('self, Name.t Loc.located) entry
| TTReference : ('self, reference) entry
| TTBigint : ('self, Bigint.bigint) entry
-| TTBinder : ('self, local_binder list) entry
+| TTBinder : ('self, local_binder_expr list) entry
| TTConstr : prod_info * 'r target -> ('r, 'r) entry
| TTConstrList : prod_info * Tok.t list * 'r target -> ('r, 'r list) entry
-| TTBinderListT : ('self, local_binder list) entry
-| TTBinderListF : Tok.t list -> ('self, local_binder list list) entry
+| TTBinderListT : ('self, local_binder_expr list) entry
+| TTBinderListF : Tok.t list -> ('self, local_binder_expr list list) entry
type _ any_entry = TTAny : ('s, 'r) entry -> 's any_entry
@@ -324,7 +324,7 @@ let cases_pattern_expr_of_name (loc,na) = match na with
type 'r env = {
constrs : 'r list;
constrlists : 'r list list;
- binders : (local_binder list * bool) list;
+ binders : (local_binder_expr list * bool) list;
}
let push_constr subst v = { subst with constrs = v :: subst.constrs }
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 47455f984..c127e7880 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -38,7 +38,7 @@ let mk_cast = function
in CCast(loc, c, CastConv ty)
let binder_of_name expl (loc,na) =
- LocalRawAssum ([loc, na], Default expl,
+ CLocalAssum ([loc, na], Default expl,
CHole (loc, Some (Evar_kinds.BinderType na), IntroAnonymous, None))
let binders_of_names l =
@@ -240,17 +240,18 @@ GEXTEND Gram
mkCLambdaN (!@loc) bl c
| "let"; id=name; bl = binders; ty = type_cstr; ":=";
c1 = operconstr LEVEL "200"; "in"; c2 = operconstr LEVEL "200" ->
- let loc1 =
- Loc.merge (local_binders_loc bl) (constr_loc c1)
- in
- CLetIn(!@loc,id,mkCLambdaN loc1 bl (mk_cast(c1,ty)),c2)
+ let ty,c1 = match ty, c1 with
+ | (_,None), CCast(loc,c, CastConv t) -> (constr_loc t,Some t), c (* Tolerance, see G_vernac.def_body *)
+ | _, _ -> ty, c1 in
+ CLetIn(!@loc,id,mkCLambdaN (constr_loc c1) bl c1,
+ Option.map (mkCProdN (fst ty) bl) (snd ty), c2)
| "let"; fx = single_fix; "in"; c = operconstr LEVEL "200" ->
let fixp = mk_single_fix fx in
let (li,id) = match fixp with
CFix(_,id,_) -> id
| CCoFix(_,id,_) -> id
| _ -> assert false in
- CLetIn(!@loc,(li,Name id),fixp,c)
+ CLetIn(!@loc,(li,Name id),fixp,None,c)
| "let"; lb = ["("; l=LIST0 name SEP ","; ")" -> l | "()" -> []];
po = return_type;
":="; c1 = operconstr LEVEL "200"; "in";
@@ -412,11 +413,11 @@ GEXTEND Gram
impl_ident_tail:
[ [ "}" -> binder_of_name Implicit
| nal=LIST1 name; ":"; c=lconstr; "}" ->
- (fun na -> LocalRawAssum (na::nal,Default Implicit,c))
+ (fun na -> CLocalAssum (na::nal,Default Implicit,c))
| nal=LIST1 name; "}" ->
- (fun na -> LocalRawAssum (na::nal,Default Implicit,CHole (Loc.join_loc (fst na) !@loc, Some (Evar_kinds.BinderType (snd na)), IntroAnonymous, None)))
+ (fun na -> CLocalAssum (na::nal,Default Implicit,CHole (Loc.join_loc (fst na) !@loc, Some (Evar_kinds.BinderType (snd na)), IntroAnonymous, None)))
| ":"; c=lconstr; "}" ->
- (fun na -> LocalRawAssum ([na],Default Implicit,c))
+ (fun na -> CLocalAssum ([na],Default Implicit,c))
] ]
;
fixannot:
@@ -442,12 +443,12 @@ GEXTEND Gram
the latter is unique *)
[ [ (* open binder *)
id = name; idl = LIST0 name; ":"; c = lconstr ->
- [LocalRawAssum (id::idl,Default Explicit,c)]
+ [CLocalAssum (id::idl,Default Explicit,c)]
(* binders factorized with open binder *)
| id = name; idl = LIST0 name; bl = binders ->
binders_of_names (id::idl) @ bl
| id1 = name; ".."; id2 = name ->
- [LocalRawAssum ([id1;(!@loc,Name ldots_var);id2],
+ [CLocalAssum ([id1;(!@loc,Name ldots_var);id2],
Default Explicit,CHole (!@loc, None, IntroAnonymous, None))]
| bl = closed_binder; bl' = binders ->
bl@bl'
@@ -457,37 +458,39 @@ GEXTEND Gram
[ [ l = LIST0 binder -> List.flatten l ] ]
;
binder:
- [ [ id = name -> [LocalRawAssum ([id],Default Explicit,CHole (!@loc, None, IntroAnonymous, None))]
+ [ [ id = name -> [CLocalAssum ([id],Default Explicit,CHole (!@loc, None, IntroAnonymous, None))]
| bl = closed_binder -> bl ] ]
;
closed_binder:
[ [ "("; id=name; idl=LIST1 name; ":"; c=lconstr; ")" ->
- [LocalRawAssum (id::idl,Default Explicit,c)]
+ [CLocalAssum (id::idl,Default Explicit,c)]
| "("; id=name; ":"; c=lconstr; ")" ->
- [LocalRawAssum ([id],Default Explicit,c)]
+ [CLocalAssum ([id],Default Explicit,c)]
| "("; id=name; ":="; c=lconstr; ")" ->
- [LocalRawDef (id,c)]
+ (match c with
+ | CCast(_,c, CastConv t) -> [CLocalDef (id,c,Some t)]
+ | _ -> [CLocalDef (id,c,None)])
| "("; id=name; ":"; t=lconstr; ":="; c=lconstr; ")" ->
- [LocalRawDef (id,CCast (Loc.merge (constr_loc t) (!@loc),c, CastConv t))]
+ [CLocalDef (id,c,Some t)]
| "{"; id=name; "}" ->
- [LocalRawAssum ([id],Default Implicit,CHole (!@loc, None, IntroAnonymous, None))]
+ [CLocalAssum ([id],Default Implicit,CHole (!@loc, None, IntroAnonymous, None))]
| "{"; id=name; idl=LIST1 name; ":"; c=lconstr; "}" ->
- [LocalRawAssum (id::idl,Default Implicit,c)]
+ [CLocalAssum (id::idl,Default Implicit,c)]
| "{"; id=name; ":"; c=lconstr; "}" ->
- [LocalRawAssum ([id],Default Implicit,c)]
+ [CLocalAssum ([id],Default Implicit,c)]
| "{"; id=name; idl=LIST1 name; "}" ->
- List.map (fun id -> LocalRawAssum ([id],Default Implicit,CHole (!@loc, None, IntroAnonymous, None))) (id::idl)
+ List.map (fun id -> CLocalAssum ([id],Default Implicit,CHole (!@loc, None, IntroAnonymous, None))) (id::idl)
| "`("; tc = LIST1 typeclass_constraint SEP "," ; ")" ->
- List.map (fun (n, b, t) -> LocalRawAssum ([n], Generalized (Implicit, Explicit, b), t)) tc
+ List.map (fun (n, b, t) -> CLocalAssum ([n], Generalized (Implicit, Explicit, b), t)) tc
| "`{"; tc = LIST1 typeclass_constraint SEP "," ; "}" ->
- List.map (fun (n, b, t) -> LocalRawAssum ([n], Generalized (Implicit, Implicit, b), t)) tc
+ List.map (fun (n, b, t) -> CLocalAssum ([n], Generalized (Implicit, Implicit, b), t)) tc
| "'"; p = pattern LEVEL "0" ->
let (p, ty) =
match p with
| CPatCast (_, p, ty) -> (p, Some ty)
| _ -> (p, None)
in
- [LocalPattern (!@loc, p, ty)]
+ [CLocalPattern (!@loc, p, ty)]
] ]
;
typeclass_constraint:
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 23f1dccaf..ded7a557c 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -243,7 +243,7 @@ GEXTEND Gram
| _ -> DefineBody (bl, red, c, None))
| bl = binders; ":"; t = lconstr; ":="; red = reduce; c = lconstr ->
let ((bl, c), tyo) =
- if List.exists (function LocalPattern _ -> true | _ -> false) bl
+ if List.exists (function CLocalPattern _ -> true | _ -> false) bl
then
let c = CCast (!@loc, c, CastConv t) in
(expand_pattern_binders mkCLambdaN bl c, None)
@@ -334,8 +334,8 @@ GEXTEND Gram
binder_nodef:
[ [ b = binder_let ->
(match b with
- LocalRawAssum(l,ty) -> (l,ty)
- | LocalRawDef _ ->
+ CLocalAssum(l,ty) -> (l,ty)
+ | CLocalDef _ ->
Util.user_err_loc
(loc,"fix_param",Pp.str"defined binder not allowed here.")) ] ]
;
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index cf5174af9..6c148d393 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -162,11 +162,11 @@ module Constr :
val pattern : cases_pattern_expr Gram.entry
val constr_pattern : constr_expr Gram.entry
val lconstr_pattern : constr_expr Gram.entry
- val closed_binder : local_binder list Gram.entry
- val binder : local_binder list Gram.entry (* closed_binder or variable *)
- val binders : local_binder list Gram.entry (* list of binder *)
- val open_binders : local_binder list Gram.entry
- val binders_fixannot : (local_binder list * (Id.t located option * recursion_order_expr)) Gram.entry
+ val closed_binder : local_binder_expr list Gram.entry
+ val binder : local_binder_expr list Gram.entry (* closed_binder or variable *)
+ val binders : local_binder_expr list Gram.entry (* list of binder *)
+ val open_binders : local_binder_expr list Gram.entry
+ val binders_fixannot : (local_binder_expr list * (Id.t located option * recursion_order_expr)) Gram.entry
val typeclass_constraint : (Name.t located * bool * constr_expr) Gram.entry
val record_declaration : constr_expr Gram.entry
val appl_arg : (constr_expr * explicitation located option) Gram.entry
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-29 08:20:15 +0000