From d91a0c27402f0f19a30147bb9d87387ca2a91fd0 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 2 Feb 2017 10:18:48 +0100 Subject: "Standardizing" the name LocalPatten into LocalRawPattern. --- interp/constrexpr_ops.ml | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) (limited to 'interp/constrexpr_ops.ml') diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml index 59c24900d2..c861641010 100644 --- a/interp/constrexpr_ops.ml +++ b/interp/constrexpr_ops.ml @@ -40,7 +40,7 @@ let names_of_local_assums bl = List.flatten (List.map (function LocalRawAssum(l,_,_)->l|_->[]) bl) let names_of_local_binders bl = - List.flatten (List.map (function LocalRawAssum(l,_,_)->l|LocalRawDef(l,_)->[l]|LocalPattern _ -> assert false) bl) + List.flatten (List.map (function LocalRawAssum(l,_,_)->l|LocalRawDef(l,_)->[l]|LocalRawPattern _ -> assert false) bl) (**********************************************************************) (* Functions on constr_expr *) @@ -272,7 +272,7 @@ let local_binder_loc = function | LocalRawAssum ((loc,_)::_,_,t) | LocalRawDef ((loc,_),t) -> Loc.merge loc (constr_loc t) | LocalRawAssum ([],_,_) -> assert false - | LocalPattern (loc,_,_) -> loc + | LocalRawPattern (loc,_,_) -> loc let local_binders_loc bll = match bll with | [] -> Loc.ghost @@ -314,7 +314,7 @@ let expand_pattern_binders mkC bl c = | LocalRawAssum (nl, _, _) -> let env = List.fold_left add_name_in_env env nl in (env, b :: bl, c) - | LocalPattern (loc, p, ty) -> + | LocalRawPattern (loc, p, ty) -> let ni = Hook.get fresh_var env c in let id = (loc, Name ni) in let b = @@ -344,7 +344,7 @@ let mkCProdN loc bll c = 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 + | LocalRawPattern (loc,p,ty) :: bll -> assert false in let (bll, c) = expand_pattern_binders loop bll c in loop loc bll c @@ -358,7 +358,7 @@ let mkCLambdaN loc bll c = 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 + | LocalRawPattern (loc,p,ty) :: bll -> assert false in let (bll, c) = expand_pattern_binders loop bll c in loop loc bll c @@ -369,7 +369,7 @@ let rec abstract_constr_expr c = function | LocalRawAssum (idl,bk,t)::bl -> List.fold_right (fun x b -> mkLambdaC([x],bk,t,b)) idl (abstract_constr_expr c bl) - | LocalPattern _::_ -> assert false + | LocalRawPattern _::_ -> assert false let rec prod_constr_expr c = function | [] -> c @@ -377,7 +377,7 @@ let rec prod_constr_expr c = function | LocalRawAssum (idl,bk,t)::bl -> List.fold_right (fun x b -> mkProdC([x],bk,t,b)) idl (prod_constr_expr c bl) - | LocalPattern _::_ -> assert false + | LocalRawPattern _::_ -> assert false let coerce_reference_to_id = function | Ident (_,id) -> id -- cgit v1.2.3 From 648ce5e08f7245f2a775abd1304783c4167e9f2e Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 2 Feb 2017 18:24:58 +0100 Subject: Unifying standard "constr_level" names for constructors of local_binder_expr. RawLocal -> CLocal --- interp/constrexpr_ops.ml | 52 ++++++++++++++++++++++++------------------------ 1 file changed, 26 insertions(+), 26 deletions(-) (limited to 'interp/constrexpr_ops.ml') diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml index c861641010..ee6acde6b2 100644 --- a/interp/constrexpr_ops.ml +++ b/interp/constrexpr_ops.ml @@ -37,10 +37,10 @@ let binder_kind_eq b1 b2 = match b1, b2 with let default_binder_kind = Default Explicit let names_of_local_assums bl = - List.flatten (List.map (function LocalRawAssum(l,_,_)->l|_->[]) bl) + List.flatten (List.map (function CLocalAssum(l,_,_)->l|_->[]) bl) let names_of_local_binders bl = - List.flatten (List.map (function LocalRawAssum(l,_,_)->l|LocalRawDef(l,_)->[l]|LocalRawPattern _ -> assert false) bl) + List.flatten (List.map (function CLocalAssum(l,_,_)->l|CLocalDef(l,_)->[l]|CLocalPattern _ -> assert false) bl) (**********************************************************************) (* Functions on constr_expr *) @@ -212,9 +212,9 @@ and recursion_order_expr_eq r1 r2 = match r1, r2 with | _ -> false and local_binder_eq l1 l2 = match l1, l2 with -| LocalRawDef (n1, e1), LocalRawDef (n2, e2) -> +| CLocalDef (n1, e1), CLocalDef (n2, e2) -> eq_located Name.equal n1 n2 && constr_expr_eq e1 e2 -| LocalRawAssum (n1, _, e1), LocalRawAssum (n2, _, e2) -> +| CLocalAssum (n1, _, e1), CLocalAssum (n2, _, e2) -> (** Don't care about the [binder_kind] *) List.equal (eq_located Name.equal) n1 n2 && constr_expr_eq e1 e2 | _ -> false @@ -269,10 +269,10 @@ let raw_cases_pattern_expr_loc = function | RCPatOr (loc,_) -> loc let local_binder_loc = function - | LocalRawAssum ((loc,_)::_,_,t) - | LocalRawDef ((loc,_),t) -> Loc.merge loc (constr_loc t) - | LocalRawAssum ([],_,_) -> assert false - | LocalRawPattern (loc,_,_) -> loc + | CLocalAssum ((loc,_)::_,_,t) + | CLocalDef ((loc,_),t) -> Loc.merge loc (constr_loc t) + | CLocalAssum ([],_,_) -> assert false + | CLocalPattern (loc,_,_) -> loc let local_binders_loc bll = match bll with | [] -> Loc.ghost @@ -308,17 +308,17 @@ let expand_pattern_binders mkC bl c = | b :: bl -> let (env, bl, c) = loop bl c in match b with - | LocalRawDef (n, _) -> + | CLocalDef (n, _) -> let env = add_name_in_env env n in (env, b :: bl, c) - | LocalRawAssum (nl, _, _) -> + | CLocalAssum (nl, _, _) -> let env = List.fold_left add_name_in_env env nl in (env, b :: bl, c) - | LocalRawPattern (loc, p, ty) -> + | CLocalPattern (loc, p, ty) -> let ni = Hook.get fresh_var env c in let id = (loc, Name ni) in let b = - LocalRawAssum + CLocalAssum ([id], Default Explicit, match ty with | Some ty -> ty @@ -338,13 +338,13 @@ let expand_pattern_binders mkC bl c = let mkCProdN loc bll c = let rec loop loc bll c = match bll with - | LocalRawAssum ((loc1,_)::_ as idl,bk,t) :: bll -> + | CLocalAssum ((loc1,_)::_ as idl,bk,t) :: bll -> CProdN (loc,[idl,bk,t],loop (Loc.merge loc1 loc) bll c) - | LocalRawDef ((loc1,_) as id,b) :: bll -> + | CLocalDef ((loc1,_) as id,b) :: bll -> CLetIn (loc,id,b,loop (Loc.merge loc1 loc) bll c) | [] -> c - | LocalRawAssum ([],_,_) :: bll -> loop loc bll c - | LocalRawPattern (loc,p,ty) :: bll -> assert false + | CLocalAssum ([],_,_) :: bll -> loop loc bll c + | CLocalPattern (loc,p,ty) :: bll -> assert false in let (bll, c) = expand_pattern_binders loop bll c in loop loc bll c @@ -352,32 +352,32 @@ let mkCProdN loc bll c = let mkCLambdaN loc bll c = let rec loop loc bll c = match bll with - | LocalRawAssum ((loc1,_)::_ as idl,bk,t) :: bll -> + | CLocalAssum ((loc1,_)::_ as idl,bk,t) :: bll -> CLambdaN (loc,[idl,bk,t],loop (Loc.merge loc1 loc) bll c) - | LocalRawDef ((loc1,_) as id,b) :: bll -> + | CLocalDef ((loc1,_) as id,b) :: bll -> CLetIn (loc,id,b,loop (Loc.merge loc1 loc) bll c) | [] -> c - | LocalRawAssum ([],_,_) :: bll -> loop loc bll c - | LocalRawPattern (loc,p,ty) :: bll -> assert false + | CLocalAssum ([],_,_) :: bll -> loop loc bll c + | CLocalPattern (loc,p,ty) :: bll -> assert false in let (bll, c) = expand_pattern_binders loop bll c in loop loc bll c let rec abstract_constr_expr c = function | [] -> c - | LocalRawDef (x,b)::bl -> mkLetInC(x,b,abstract_constr_expr c bl) - | LocalRawAssum (idl,bk,t)::bl -> + | CLocalDef (x,b)::bl -> mkLetInC(x,b,abstract_constr_expr c bl) + | CLocalAssum (idl,bk,t)::bl -> List.fold_right (fun x b -> mkLambdaC([x],bk,t,b)) idl (abstract_constr_expr c bl) - | LocalRawPattern _::_ -> assert false + | CLocalPattern _::_ -> assert false let rec prod_constr_expr c = function | [] -> c - | LocalRawDef (x,b)::bl -> mkLetInC(x,b,prod_constr_expr c bl) - | LocalRawAssum (idl,bk,t)::bl -> + | CLocalDef (x,b)::bl -> mkLetInC(x,b,prod_constr_expr c bl) + | CLocalAssum (idl,bk,t)::bl -> List.fold_right (fun x b -> mkProdC([x],bk,t,b)) idl (prod_constr_expr c bl) - | LocalRawPattern _::_ -> assert false + | CLocalPattern _::_ -> assert false let coerce_reference_to_id = function | Ident (_,id) -> id -- cgit v1.2.3 From f9a4ca41bc1313300f5f9b9092fe24825f435706 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 1 Feb 2017 15:56:45 +0100 Subject: Replacing "cast surgery" in LetIn by a proper field (see PR #404). This is a patch fulfilling the relevant remark of Maxime that an explicit information at the ML type level would be better than "cast surgery" to carry the optional type of a let-in. There are a very few semantic changes. - a "(x:t:=c)" in a block of binders is now written in the more standard way "(x:=c:t)" - in notations, the type of a let-in is not displayed if not explicitly asked so. See discussion at PR #417 for more information. --- interp/constrexpr_ops.ml | 30 ++++++++++++++++-------------- 1 file changed, 16 insertions(+), 14 deletions(-) (limited to 'interp/constrexpr_ops.ml') diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml index ee6acde6b2..53c97f6b6b 100644 --- a/interp/constrexpr_ops.ml +++ b/interp/constrexpr_ops.ml @@ -40,7 +40,7 @@ let names_of_local_assums bl = List.flatten (List.map (function CLocalAssum(l,_,_)->l|_->[]) bl) let names_of_local_binders bl = - List.flatten (List.map (function CLocalAssum(l,_,_)->l|CLocalDef(l,_)->[l]|CLocalPattern _ -> assert false) bl) + List.flatten (List.map (function CLocalAssum(l,_,_)->l|CLocalDef(l,_,_)->[l]|CLocalPattern _ -> assert false) bl) (**********************************************************************) (* Functions on constr_expr *) @@ -113,9 +113,10 @@ let rec constr_expr_eq e1 e2 = | CLambdaN(_,bl1,a1), CLambdaN(_,bl2,a2) -> List.equal binder_expr_eq bl1 bl2 && constr_expr_eq a1 a2 - | CLetIn(_,(_,na1),a1,b1), CLetIn(_,(_,na2),a2,b2) -> + | CLetIn(_,(_,na1),a1,t1,b1), CLetIn(_,(_,na2),a2,t2,b2) -> Name.equal na1 na2 && constr_expr_eq a1 a2 && + Option.equal constr_expr_eq t1 t2 && constr_expr_eq b1 b2 | CAppExpl(_,(proj1,r1,_),al1), CAppExpl(_,(proj2,r2,_),al2) -> Option.equal Int.equal proj1 proj2 && @@ -212,8 +213,8 @@ and recursion_order_expr_eq r1 r2 = match r1, r2 with | _ -> false and local_binder_eq l1 l2 = match l1, l2 with -| CLocalDef (n1, e1), CLocalDef (n2, e2) -> - eq_located Name.equal n1 n2 && constr_expr_eq e1 e2 +| CLocalDef (n1, e1, t1), CLocalDef (n2, e2, t2) -> + eq_located Name.equal n1 n2 && constr_expr_eq e1 e2 && Option.equal constr_expr_eq t1 t2 | CLocalAssum (n1, _, e1), CLocalAssum (n2, _, e2) -> (** Don't care about the [binder_kind] *) List.equal (eq_located Name.equal) n1 n2 && constr_expr_eq e1 e2 @@ -234,7 +235,7 @@ let constr_loc = function | CCoFix (loc,_,_) -> loc | CProdN (loc,_,_) -> loc | CLambdaN (loc,_,_) -> loc - | CLetIn (loc,_,_,_) -> loc + | CLetIn (loc,_,_,_,_) -> loc | CAppExpl (loc,_,_) -> loc | CApp (loc,_,_) -> loc | CRecord (loc,_) -> loc @@ -270,7 +271,8 @@ let raw_cases_pattern_expr_loc = function let local_binder_loc = function | CLocalAssum ((loc,_)::_,_,t) - | CLocalDef ((loc,_),t) -> Loc.merge loc (constr_loc t) + | CLocalDef ((loc,_),t,None) -> Loc.merge loc (constr_loc t) + | CLocalDef ((loc,_),b,Some t) -> Loc.merge loc (Loc.merge (constr_loc b) (constr_loc t)) | CLocalAssum ([],_,_) -> assert false | CLocalPattern (loc,_,_) -> loc @@ -285,7 +287,7 @@ let mkIdentC id = CRef (Ident (Loc.ghost, id),None) let mkRefC r = CRef (r,None) let mkCastC (a,k) = CCast (Loc.ghost,a,k) let mkLambdaC (idl,bk,a,b) = CLambdaN (Loc.ghost,[idl,bk,a],b) -let mkLetInC (id,a,b) = CLetIn (Loc.ghost,id,a,b) +let mkLetInC (id,a,t,b) = CLetIn (Loc.ghost,id,a,t,b) let mkProdC (idl,bk,a,b) = CProdN (Loc.ghost,[idl,bk,a],b) let mkAppC (f,l) = @@ -308,7 +310,7 @@ let expand_pattern_binders mkC bl c = | b :: bl -> let (env, bl, c) = loop bl c in match b with - | CLocalDef (n, _) -> + | CLocalDef (n, _, _) -> let env = add_name_in_env env n in (env, b :: bl, c) | CLocalAssum (nl, _, _) -> @@ -340,8 +342,8 @@ let mkCProdN loc bll c = match bll with | CLocalAssum ((loc1,_)::_ as idl,bk,t) :: bll -> CProdN (loc,[idl,bk,t],loop (Loc.merge loc1 loc) bll c) - | CLocalDef ((loc1,_) as id,b) :: bll -> - CLetIn (loc,id,b,loop (Loc.merge loc1 loc) bll c) + | CLocalDef ((loc1,_) as id,b,t) :: bll -> + CLetIn (loc,id,b,t,loop (Loc.merge loc1 loc) bll c) | [] -> c | CLocalAssum ([],_,_) :: bll -> loop loc bll c | CLocalPattern (loc,p,ty) :: bll -> assert false @@ -354,8 +356,8 @@ let mkCLambdaN loc bll c = match bll with | CLocalAssum ((loc1,_)::_ as idl,bk,t) :: bll -> CLambdaN (loc,[idl,bk,t],loop (Loc.merge loc1 loc) bll c) - | CLocalDef ((loc1,_) as id,b) :: bll -> - CLetIn (loc,id,b,loop (Loc.merge loc1 loc) bll c) + | CLocalDef ((loc1,_) as id,b,t) :: bll -> + CLetIn (loc,id,b,t,loop (Loc.merge loc1 loc) bll c) | [] -> c | CLocalAssum ([],_,_) :: bll -> loop loc bll c | CLocalPattern (loc,p,ty) :: bll -> assert false @@ -365,7 +367,7 @@ let mkCLambdaN loc bll c = let rec abstract_constr_expr c = function | [] -> c - | CLocalDef (x,b)::bl -> mkLetInC(x,b,abstract_constr_expr c bl) + | CLocalDef (x,b,t)::bl -> mkLetInC(x,b,t,abstract_constr_expr c bl) | CLocalAssum (idl,bk,t)::bl -> List.fold_right (fun x b -> mkLambdaC([x],bk,t,b)) idl (abstract_constr_expr c bl) @@ -373,7 +375,7 @@ let rec abstract_constr_expr c = function let rec prod_constr_expr c = function | [] -> c - | CLocalDef (x,b)::bl -> mkLetInC(x,b,prod_constr_expr c bl) + | CLocalDef (x,b,t)::bl -> mkLetInC(x,b,t,prod_constr_expr c bl) | CLocalAssum (idl,bk,t)::bl -> List.fold_right (fun x b -> mkProdC([x],bk,t,b)) idl (prod_constr_expr c bl) -- cgit v1.2.3