From 8f5d447769a41cd251701272a6ff71a7a20de658 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Mon, 5 Dec 2016 11:36:12 +0100 Subject: Improving the API of constrexpr_ops.mli. Deprecating abstract_constr_expr in favor of mkCLambdaN, prod_constr_expr in favor of mkCProdN. Note: They did not do exactly the same, the first ones were interpreting "(x y z:_)" as "(x:_) (y:_) (z:_)" while the second ones were preserving the original sharing of the type, what I think is the correct thing to do. So, there is also a "fix" of semantic here. --- interp/constrexpr_ops.mli | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) (limited to 'interp/constrexpr_ops.mli') diff --git a/interp/constrexpr_ops.mli b/interp/constrexpr_ops.mli index a92da035f..7d3011a6e 100644 --- a/interp/constrexpr_ops.mli +++ b/interp/constrexpr_ops.mli @@ -49,14 +49,14 @@ val mkLambdaC : Name.t located list * binder_kind * constr_expr * constr_expr -> val mkLetInC : Name.t located * constr_expr * constr_expr -> constr_expr val mkProdC : Name.t located list * binder_kind * constr_expr * constr_expr -> constr_expr -val abstract_constr_expr : constr_expr -> local_binder list -> constr_expr -val prod_constr_expr : constr_expr -> local_binder list -> constr_expr - val mkCLambdaN : Loc.t -> local_binder list -> constr_expr -> constr_expr -(** Same as [abstract_constr_expr], with location *) - val mkCProdN : Loc.t -> local_binder list -> constr_expr -> constr_expr -(** Same as [prod_constr_expr], with location *) + +(** @deprecated variant of mkCLambdaN *) +val abstract_constr_expr : constr_expr -> local_binder list -> constr_expr + +(** @deprecated variant of mkCProdN *) +val prod_constr_expr : constr_expr -> local_binder list -> constr_expr val fresh_var_hook : (Names.Id.t list -> Constrexpr.constr_expr -> Names.Id.t) Hook.t val expand_pattern_binders : -- cgit v1.2.3 From 45a411377244da33111cf5d7002df70de912bc64 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Mon, 5 Dec 2016 11:57:58 +0100 Subject: Factorizing/unifying code in dealing with binders. Note: This reveals a little bug yet to fix in g_vernac.ml4. In Definition f '((x,y):id nat * id nat) '((x',y'):id nat * id nat) := Eval unfold id in x+y = x'+y'. the "id" are wrongly unfolded and in Definition f '(x,y) '(x',y') := x+y = x'+y' : Prop. an unexpected cast remains in the body of f. --- interp/constrexpr_ops.ml | 68 +++++++++++++++++------------------------------ interp/constrexpr_ops.mli | 3 --- parsing/g_vernac.ml4 | 14 +++++++--- 3 files changed, 34 insertions(+), 51 deletions(-) (limited to 'interp/constrexpr_ops.mli') diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml index 7433336f8..223ec1547 100644 --- a/interp/constrexpr_ops.ml +++ b/interp/constrexpr_ops.ml @@ -301,67 +301,47 @@ let add_name_in_env env n = let (fresh_var, fresh_var_hook) = Hook.make ~default:(fun _ _ -> assert false) () -let expand_pattern_binders mkC bl c = - let rec loop bl c = +let expand_binders mkC loc bl c = + let rec loop loc bl c = match bl with - | [] -> ([], [], c) + | [] -> ([], c) | b :: bl -> - let (env, bl, c) = loop bl c in match b with - | LocalRawDef (n, _) -> + | LocalRawDef ((loc1,_) as n, b) -> + let env, c = loop (Loc.merge loc1 loc) bl c in let env = add_name_in_env env n in - (env, b :: bl, c) - | LocalRawAssum (nl, _, _) -> + (env, CLetIn (loc,n,b,c)) + | LocalRawAssum ((loc1,_)::_ as nl, bk, t) -> + let env, c = loop (Loc.merge loc1 loc) bl c in let env = List.fold_left add_name_in_env env nl in - (env, b :: bl, c) - | LocalPattern (loc, p, ty) -> + (env, mkC loc (nl,bk,t) c) + | LocalRawAssum ([],_,_) -> loop loc bl c + | LocalPattern (loc1, p, ty) -> + let env, c = loop (Loc.merge loc1 loc) bl c in let ni = Hook.get fresh_var env c in - let id = (loc, Name ni) in - let b = - LocalRawAssum - ([id], Default Explicit, - match ty with + let id = (loc1, Name ni) in + let ty = match ty with | Some ty -> ty - | None -> CHole (loc, None, IntroAnonymous, None)) + | None -> CHole (loc1, None, IntroAnonymous, None) in - let e = CRef (Libnames.Ident (loc, ni), None) in + let e = CRef (Libnames.Ident (loc1, ni), None) in let c = CCases (loc, LetPatternStyle, None, [(e,None,None)], - [(loc, [(loc,[p])], mkC loc bl c)]) + [(loc1, [(loc1,[p])], c)]) in - (ni :: env, [b], c) + (ni :: env, mkC loc ([id],Default Explicit,ty) c) in - let (_, bl, c) = loop bl c in - (bl, c) + let (_, c) = loop loc bl c in + c let mkCProdN loc bll c = - let rec loop loc bll c = - match bll with - | LocalRawAssum ((loc1,_)::_ as idl,bk,t) :: bll -> - CProdN (loc,[idl,bk,t],loop (Loc.merge loc1 loc) bll c) - | LocalRawDef ((loc1,_) as id,b) :: bll -> - CLetIn (loc,id,b,loop (Loc.merge loc1 loc) bll c) - | [] -> c - | LocalRawAssum ([],_,_) :: bll -> loop loc bll c - | LocalPattern (loc,p,ty) :: bll -> assert false - in - let (bll, c) = expand_pattern_binders loop bll c in - loop loc bll c + let mk loc b c = CProdN (loc,[b],c) in + expand_binders mk loc bll c let mkCLambdaN loc bll c = - let rec loop loc bll c = - match bll with - | LocalRawAssum ((loc1,_)::_ as idl,bk,t) :: bll -> - CLambdaN (loc,[idl,bk,t],loop (Loc.merge loc1 loc) bll c) - | LocalRawDef ((loc1,_) as id,b) :: bll -> - CLetIn (loc,id,b,loop (Loc.merge loc1 loc) bll c) - | [] -> c - | LocalRawAssum ([],_,_) :: bll -> loop loc bll c - | LocalPattern (loc,p,ty) :: bll -> assert false - in - let (bll, c) = expand_pattern_binders loop bll c in - loop loc bll c + let mk loc b c = CLambdaN (loc,[b],c) in + expand_binders mk loc bll c (* Deprecated *) let abstract_constr_expr c bl = mkCLambdaN (local_binders_loc bl) bl c diff --git a/interp/constrexpr_ops.mli b/interp/constrexpr_ops.mli index 7d3011a6e..9d154340f 100644 --- a/interp/constrexpr_ops.mli +++ b/interp/constrexpr_ops.mli @@ -59,9 +59,6 @@ val abstract_constr_expr : constr_expr -> local_binder list -> constr_expr val prod_constr_expr : constr_expr -> local_binder list -> constr_expr val fresh_var_hook : (Names.Id.t list -> Constrexpr.constr_expr -> Names.Id.t) Hook.t -val expand_pattern_binders : - (Loc.t -> local_binder list -> constr_expr -> constr_expr) -> - local_binder list -> constr_expr -> local_binder list * constr_expr (** {6 Destructors}*) diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 18807113c..ba441a662 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -243,16 +243,22 @@ GEXTEND Gram (* Simple definitions *) def_body: [ [ bl = binders; ":="; red = reduce; c = lconstr -> - let (bl, c) = expand_pattern_binders mkCLambdaN bl c in - (match c with - CCast(_,c, CastConv t) -> DefineBody (bl, red, c, Some t) + if List.exists (function LocalPattern _ -> true | _ -> false) bl + then + (* FIXME: "red" will be applied to types in bl and Cast with remain *) + let c = mkCLambdaN (!@loc) bl c in + DefineBody ([], red, c, None) + else + (match c with + | CCast(_,c, CastConv t) -> DefineBody (bl, red, c, Some t) | _ -> 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 then + (* FIXME: "red" will be applied to types in bl and Cast with remain *) let c = CCast (!@loc, c, CastConv t) in - (expand_pattern_binders mkCLambdaN bl c, None) + (([],mkCLambdaN (!@loc) bl c), None) else ((bl, c), Some t) in DefineBody (bl, red, c, tyo) -- cgit v1.2.3