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/constrextern.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'interp/constrextern.ml') diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 3077231be0..8e0f5678ce 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -843,7 +843,7 @@ and extern_local_binder scopes vars = function if !Flags.raw_print then Some (extern_typ scopes vars ty) else None in let p = extern_cases_pattern vars p in let (assums,ids,l) = extern_local_binder scopes vars l in - (assums,ids, LocalPattern(Loc.ghost,p,ty) :: l) + (assums,ids, LocalRawPattern(Loc.ghost,p,ty) :: l) and extern_eqn inctx scopes vars (loc,ids,pl,c) = (loc,[loc,List.map (extern_cases_pattern_in_scope scopes vars) pl], -- 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/constrextern.ml | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) (limited to 'interp/constrextern.ml') diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 8e0f5678ce..b6aacb5ea5 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -821,20 +821,20 @@ and extern_local_binder scopes vars = function let (assums,ids,l) = extern_local_binder scopes (name_fold Id.Set.add na vars) l in (assums,na::ids, - LocalRawDef((Loc.ghost,na), extern false scopes vars bd) :: l) + CLocalDef((Loc.ghost,na), extern false scopes vars bd) :: l) | (Inl na,bk,None,ty)::l -> let ty = extern_typ scopes vars ty in (match extern_local_binder scopes (name_fold Id.Set.add na vars) l with - (assums,ids,LocalRawAssum(nal,k,ty')::l) + (assums,ids,CLocalAssum(nal,k,ty')::l) when constr_expr_eq ty ty' && match na with Name id -> not (occur_var_constr_expr id ty') | _ -> true -> (na::assums,na::ids, - LocalRawAssum((Loc.ghost,na)::nal,k,ty')::l) + CLocalAssum((Loc.ghost,na)::nal,k,ty')::l) | (assums,ids,l) -> (na::assums,na::ids, - LocalRawAssum([(Loc.ghost,na)],Default bk,ty) :: l)) + CLocalAssum([(Loc.ghost,na)],Default bk,ty) :: l)) | (Inr p,bk,Some bd,ty)::l -> assert false @@ -843,7 +843,7 @@ and extern_local_binder scopes vars = function if !Flags.raw_print then Some (extern_typ scopes vars ty) else None in let p = extern_cases_pattern vars p in let (assums,ids,l) = extern_local_binder scopes vars l in - (assums,ids, LocalRawPattern(Loc.ghost,p,ty) :: l) + (assums,ids, CLocalPattern(Loc.ghost,p,ty) :: l) and extern_eqn inctx scopes vars (loc,ids,pl,c) = (loc,[loc,List.map (extern_cases_pattern_in_scope scopes vars) pl], -- cgit v1.2.3 From 71cd2838bf3eb23a8f29df973d8012ebe2ec77b0 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 2 Feb 2017 20:21:14 +0100 Subject: Using the same type of binders for interning and externing. Previously a union type was used for externing. In particular, moving extended_glob_local_binder to glob_constr.ml. --- interp/constrextern.ml | 21 +++++++++++++-------- 1 file changed, 13 insertions(+), 8 deletions(-) (limited to 'interp/constrextern.ml') diff --git a/interp/constrextern.ml b/interp/constrextern.ml index b6aacb5ea5..e723acd13e 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -597,6 +597,13 @@ let extern_optimal_prim_token scopes r r' = | Some n, (Some (CDelimiters _) | None) | _, Some n -> n | _ -> raise No_match +(**********************************************************************) +(* mapping decl *) + +let extended_glob_local_binder_of_decl loc = function + | (p,bk,Some x,t) -> GLocalDef (loc,p,bk,x,t) + | (p,bk,None,t) -> GLocalAssum (loc,p,bk,t) + (**********************************************************************) (* mapping glob_constr to constr_expr *) @@ -756,7 +763,7 @@ let rec extern inctx scopes vars r = let listdecl = Array.mapi (fun i fi -> let (bl,ty,def) = blv.(i), tyv.(i), bv.(i) in - let bl = List.map (fun (p,bk,x,t) -> (Inl p,bk,x,t)) bl in + let bl = List.map (extended_glob_local_binder_of_decl loc) bl in let (assums,ids,bl) = extern_local_binder scopes vars bl in let vars0 = List.fold_right (name_fold Id.Set.add) ids vars in let vars1 = List.fold_right (name_fold Id.Set.add) ids vars' in @@ -773,7 +780,7 @@ let rec extern inctx scopes vars r = | GCoFix n -> let listdecl = Array.mapi (fun i fi -> - let bl = List.map (fun (p,bk,x,t) -> (Inl p,bk,x,t)) blv.(i) in + let bl = List.map (extended_glob_local_binder_of_decl loc) blv.(i) in let (_,ids,bl) = extern_local_binder scopes vars bl in let vars0 = List.fold_right (name_fold Id.Set.add) ids vars in let vars1 = List.fold_right (name_fold Id.Set.add) ids vars' in @@ -817,13 +824,13 @@ and factorize_lambda inctx scopes vars na bk aty c = and extern_local_binder scopes vars = function [] -> ([],[],[]) - | (Inl na,bk,Some bd,ty)::l -> + | GLocalDef (_,na,bk,bd,ty)::l -> let (assums,ids,l) = extern_local_binder scopes (name_fold Id.Set.add na vars) l in (assums,na::ids, CLocalDef((Loc.ghost,na), extern false scopes vars bd) :: l) - | (Inl na,bk,None,ty)::l -> + | GLocalAssum (_,na,bk,ty)::l -> let ty = extern_typ scopes vars ty in (match extern_local_binder scopes (name_fold Id.Set.add na vars) l with (assums,ids,CLocalAssum(nal,k,ty')::l) @@ -836,9 +843,7 @@ and extern_local_binder scopes vars = function (na::assums,na::ids, CLocalAssum([(Loc.ghost,na)],Default bk,ty) :: l)) - | (Inr p,bk,Some bd,ty)::l -> assert false - - | (Inr p,bk,None,ty)::l -> + | GLocalPattern (_,(p,_),_,bk,ty)::l -> let ty = if !Flags.raw_print then Some (extern_typ scopes vars ty) else None in let p = extern_cases_pattern vars p in @@ -1052,5 +1057,5 @@ let extern_constr_pattern env sigma pat = let extern_rel_context where env sigma sign = let a = detype_rel_context where [] (names_of_rel_context env,env) sigma sign in let vars = vars_of_env env in - let a = List.map (fun (p,bk,x,t) -> (Inl p,bk,x,t)) a in + let a = List.map (extended_glob_local_binder_of_decl Loc.ghost) a in pi3 (extern_local_binder (None,[]) vars a) -- 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/constrextern.ml | 16 ++++++++++------ 1 file changed, 10 insertions(+), 6 deletions(-) (limited to 'interp/constrextern.ml') diff --git a/interp/constrextern.ml b/interp/constrextern.ml index e723acd13e..925e9517c7 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -601,8 +601,9 @@ let extern_optimal_prim_token scopes r r' = (* mapping decl *) let extended_glob_local_binder_of_decl loc = function - | (p,bk,Some x,t) -> GLocalDef (loc,p,bk,x,t) | (p,bk,None,t) -> GLocalAssum (loc,p,bk,t) + | (p,bk,Some x,GHole (_, _, Misctypes.IntroAnonymous, None)) -> GLocalDef (loc,p,bk,x,None) + | (p,bk,Some x,t) -> GLocalDef (loc,p,bk,x,Some t) (**********************************************************************) (* mapping glob_constr to constr_expr *) @@ -699,8 +700,9 @@ let rec extern inctx scopes vars r = explicitize loc inctx [] (None,sub_extern false scopes vars f) (List.map (fun c -> lazy (sub_extern true scopes vars c)) args)) - | GLetIn (loc,na,t,c) -> - CLetIn (loc,(loc,na),sub_extern false scopes vars t, + | GLetIn (loc,na,b,t,c) -> + CLetIn (loc,(loc,na),sub_extern false scopes vars b, + Option.map (extern_typ scopes vars) t, extern inctx scopes (add_vname vars na) c) | GProd (loc,na,bk,t,c) -> @@ -828,7 +830,8 @@ and extern_local_binder scopes vars = function let (assums,ids,l) = extern_local_binder scopes (name_fold Id.Set.add na vars) l in (assums,na::ids, - CLocalDef((Loc.ghost,na), extern false scopes vars bd) :: l) + CLocalDef((Loc.ghost,na), extern false scopes vars bd, + Option.map (extern false scopes vars) ty) :: l) | GLocalAssum (_,na,bk,ty)::l -> let ty = extern_typ scopes vars ty in @@ -1020,8 +1023,9 @@ let rec glob_of_pat env sigma = function List.map (glob_of_pat env sigma) args) | PProd (na,t,c) -> GProd (loc,na,Explicit,glob_of_pat env sigma t,glob_of_pat (na::env) sigma c) - | PLetIn (na,t,c) -> - GLetIn (loc,na,glob_of_pat env sigma t, glob_of_pat (na::env) sigma c) + | PLetIn (na,b,t,c) -> + GLetIn (loc,na,glob_of_pat env sigma b, Option.map (glob_of_pat env sigma) t, + glob_of_pat (na::env) sigma c) | PLambda (na,t,c) -> GLambda (loc,na,Explicit,glob_of_pat env sigma t, glob_of_pat (na::env) sigma c) | PIf (c,b1,b2) -> -- cgit v1.2.3