From 4865160fa1f2e9ce03b37b9cb3ac99c35e9c4e4d Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 13 Apr 2017 20:29:46 +0200 Subject: Renaming interp_rawcontext_evars using a more "standard" name. --- interp/constrintern.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'interp') diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 4dcf287efc..1d5d8e8658 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -2071,7 +2071,7 @@ let intern_context global_level env impl_env binders = with InternalizationError (loc,e) -> user_err ?loc ~hdr:"internalize" (explain_internalization_error e) -let interp_rawcontext_evars env evdref k bl = +let interp_glob_context_evars env evdref k bl = let open EConstr in let (env, par, _, impls) = List.fold_left @@ -2100,6 +2100,6 @@ let interp_rawcontext_evars env evdref k bl = let interp_context_evars ?(global_level=false) ?(impl_env=empty_internalization_env) ?(shift=0) env evdref params = let int_env,bl = intern_context global_level env impl_env params in - let x = interp_rawcontext_evars env evdref shift bl in + let x = interp_glob_context_evars env evdref shift bl in int_env, x -- cgit v1.2.3 From 8ab00e5f272aa8f16d70a00323c57f2d4ef66f03 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 13 Apr 2017 21:41:41 +0200 Subject: Creating a module Nameops.Name extending module Names.Name. This module collects the functions of Nameops which are about Name.t and somehow standardize or improve their name, resulting in particular from discussions in working group. Note the use of a dedicated exception rather than a failwith for Nameops.Name.out. Drawback of the approach: one needs to open Nameops, or to use long prefix Nameops.Name. --- interp/constrextern.ml | 16 ++++++++-------- interp/constrintern.ml | 4 ++-- interp/implicit_quantifiers.ml | 2 +- interp/notation_ops.ml | 2 +- interp/topconstr.ml | 28 ++++++++++++++-------------- 5 files changed, 26 insertions(+), 26 deletions(-) (limited to 'interp') diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 4c29fc8097..f6da10c961 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -740,7 +740,7 @@ let rec extern inctx scopes vars r = | GCases (sty,rtntypopt,tml,eqns) -> let vars' = - List.fold_right (name_fold Id.Set.add) + List.fold_right (Name.fold_right Id.Set.add) (cases_predicate_names tml) vars in let rtntypopt' = Option.map (extern_typ scopes vars') rtntypopt in let tml = List.map (fun (tm,(na,x)) -> @@ -790,12 +790,12 @@ let rec extern inctx scopes vars r = let (bl,ty,def) = blv.(i), tyv.(i), bv.(i) 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 + let vars0 = List.fold_right (Name.fold_right Id.Set.add) ids vars in + let vars1 = List.fold_right (Name.fold_right Id.Set.add) ids vars' in let n = match fst nv.(i) with | None -> None - | Some x -> Some (Loc.tag @@ out_name (List.nth assums x)) + | Some x -> Some (Loc.tag @@ Name.get_id (List.nth assums x)) in let ro = extern_recursion_order scopes vars (snd nv.(i)) in ((Loc.tag fi), (n, ro), bl, extern_typ scopes vars0 ty, @@ -807,8 +807,8 @@ let rec extern inctx scopes vars r = Array.mapi (fun i fi -> 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 + let vars0 = List.fold_right (Name.fold_right Id.Set.add) ids vars in + let vars1 = List.fold_right (Name.fold_right Id.Set.add) ids vars' in ((Loc.tag fi),bl,extern_typ scopes vars0 tyv.(i), sub_extern false scopes vars1 bv.(i))) idv in @@ -852,14 +852,14 @@ and extern_local_binder scopes vars = function [] -> ([],[],[]) | { v = GLocalDef (na,bk,bd,ty)}::l -> let (assums,ids,l) = - extern_local_binder scopes (name_fold Id.Set.add na vars) l in + extern_local_binder scopes (Name.fold_right Id.Set.add na vars) l in (assums,na::ids, CLocalDef((Loc.tag na), extern false scopes vars bd, Option.map (extern false scopes vars) ty) :: l) | { v = 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 + (match extern_local_binder scopes (Name.fold_right Id.Set.add na vars) l with (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') diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 1d5d8e8658..b8d333f0d0 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -536,7 +536,7 @@ let traverse_binder (terms,_,_ as subst) avoid (renaming,env) = function try (* Binders bound in the notation are considered first-order objects *) let _,na = coerce_to_name (fst (Id.Map.find id terms)) in - (renaming,{env with ids = name_fold Id.Set.add na env.ids}), na + (renaming,{env with ids = Name.fold_right Id.Set.add na env.ids}), na with Not_found -> (* Binders not bound in the notation do not capture variables *) (* outside the notation (i.e. in the substitution) *) @@ -1660,7 +1660,7 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c = | CCases (sty, rtnpo, tms, eqns) -> let as_in_vars = List.fold_left (fun acc (_,na,inb) -> Option.fold_left (fun acc tt -> Id.Set.union (ids_of_cases_indtype tt) acc) - (Option.fold_left (fun acc (_,y) -> name_fold Id.Set.add y acc) acc na) + (Option.fold_left (fun acc (_,y) -> Name.fold_right Id.Set.add y acc) acc na) inb) Id.Set.empty tms in (* as, in & return vars *) let forbidden_vars = Option.cata free_vars_of_constr_expr as_in_vars rtnpo in diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index cfc6e6c2a6..ade524141a 100644 --- a/interp/implicit_quantifiers.ml +++ b/interp/implicit_quantifiers.ml @@ -264,7 +264,7 @@ let implicits_of_glob_constr ?(with_products=true) l = let () = match bk with | Implicit -> Feedback.msg_warning (strbrk "Ignoring implicit status of product binder " ++ - pr_name na ++ strbrk " and following binders") + Name.print na ++ strbrk " and following binders") | _ -> () in [] | GLambda (na, bk, t, b) -> abs na bk b diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index 6f91009111..ec8fa498ca 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -184,7 +184,7 @@ let glob_constr_of_notation_constr_with_binders ?loc g f e nc = e',Some (Loc.tag ?loc (ind,nal')) in let e',na' = g e' na in (e',(f e tm,(na',t'))::tml')) tml (e,[]) in - let fold (idl,e) na = let (e,na) = g e na in ((name_cons na idl,e),na) in + let fold (idl,e) na = let (e,na) = g e na in ((Name.cons na idl,e),na) in let eqnl' = List.map (fun (patl,rhs) -> let ((idl,e),patl) = List.fold_map (cases_pattern_fold_map ?loc fold) ([],e) patl in diff --git a/interp/topconstr.ml b/interp/topconstr.ml index a79f10df6b..94bbc60eaf 100644 --- a/interp/topconstr.ml +++ b/interp/topconstr.ml @@ -83,13 +83,13 @@ let ids_of_cases_tomatch tms = (fun (_, ona, indnal) l -> Option.fold_right (fun t ids -> cases_pattern_fold_names Id.Set.add ids t) indnal - (Option.fold_right (down_located (name_fold Id.Set.add)) ona l)) + (Option.fold_right (down_located (Name.fold_right Id.Set.add)) ona l)) tms Id.Set.empty let rec fold_constr_expr_binders g f n acc b = function | (nal,bk,t)::l -> let nal = snd (List.split nal) in - let n' = List.fold_right (name_fold g) nal n in + let n' = List.fold_right (Name.fold_right g) nal n in f n (fold_constr_expr_binders g f n' acc b l) t | [] -> f n acc b @@ -97,10 +97,10 @@ let rec fold_constr_expr_binders g f n acc b = function let rec fold_local_binders g f n acc b = function | CLocalAssum (nal,bk,t)::l -> let nal = snd (List.split nal) in - let n' = List.fold_right (name_fold g) nal n in + let n' = List.fold_right (Name.fold_right g) nal n in f n (fold_local_binders g f n' acc b l) t | CLocalDef ((_,na),c,t)::l -> - Option.fold_left (f n) (f n (fold_local_binders g f (name_fold g na n) acc b l) c) t + Option.fold_left (f n) (f n (fold_local_binders g f (Name.fold_right g na n) acc b l) c) t | CLocalPattern (_,(pat,t))::l -> let acc = fold_local_binders g f (cases_pattern_fold_names g n pat) acc b l in Option.fold_left (f n) acc t @@ -112,7 +112,7 @@ let fold_constr_expr_with_binders g f n acc = CAst.with_val (function | CApp ((_,t),l) -> List.fold_left (f n) (f n acc t) (List.map fst l) | CProdN (l,b) | CLambdaN (l,b) -> fold_constr_expr_binders g f n acc b l | CLetIn (na,a,t,b) -> - f (name_fold g (snd na) n) (Option.fold_left (f n) (f n acc a) t) b + f (Name.fold_right g (snd na) n) (Option.fold_left (f n) (f n acc a) t) b | CCast (a,(CastConv b|CastVM b|CastNative b)) -> f n (f n acc a) b | CCast (a,CastCoerce) -> f n acc a | CNotation (_,(l,ll,bll)) -> @@ -133,12 +133,12 @@ let fold_constr_expr_with_binders g f n acc = CAst.with_val (function let ids = ids_of_pattern_list patl in f (Id.Set.fold g ids n) acc rhs) bl acc | CLetTuple (nal,(ona,po),b,c) -> - let n' = List.fold_right (down_located (name_fold g)) nal n in - f (Option.fold_right (down_located (name_fold g)) ona n') (f n acc b) c + let n' = List.fold_right (down_located (Name.fold_right g)) nal n in + f (Option.fold_right (down_located (Name.fold_right g)) ona n') (f n acc b) c | CIf (c,(ona,po),b1,b2) -> let acc = f n (f n (f n acc b1) b2) c in Option.fold_left - (f (Option.fold_right (down_located (name_fold g)) ona n)) acc po + (f (Option.fold_right (down_located (Name.fold_right g)) ona n)) acc po | CFix (_,l) -> let n' = List.fold_right (fun ((_,id),_,_,_,_) -> g id) l n in List.fold_right (fun (_,(_,o),lb,t,c) acc -> @@ -198,7 +198,7 @@ let split_at_annot bl na = (* Used in correctness and interface *) -let map_binder g e nal = List.fold_right (down_located (name_fold g)) nal e +let map_binder g e nal = List.fold_right (down_located (Name.fold_right g)) nal e let map_binders f g e bl = (* TODO: avoid variable capture in [t] by some [na] in [List.tl nal] *) @@ -212,7 +212,7 @@ let map_local_binders f g e bl = CLocalAssum(nal,k,ty) -> (map_binder g e nal, CLocalAssum(nal,k,f e ty)::bl) | CLocalDef((loc,na),c,ty) -> - (name_fold g na e, CLocalDef((loc,na),f e c,Option.map (f e) ty)::bl) + (Name.fold_right g na e, CLocalDef((loc,na),f e c,Option.map (f e) ty)::bl) | CLocalPattern (loc,(pat,t)) -> let ids = ids_of_pattern pat in (Id.Set.fold g ids e, CLocalPattern (loc,(pat,Option.map (f e) t))::bl) in @@ -228,7 +228,7 @@ let map_constr_expr_with_binders g f e = CAst.map (function | CLambdaN (bl,b) -> let (e,bl) = map_binders f g e bl in CLambdaN (bl,f e b) | CLetIn (na,a,t,b) -> - CLetIn (na,f e a,Option.map (f e) t,f (name_fold g (snd na) e) b) + CLetIn (na,f e a,Option.map (f e) t,f (Name.fold_right g (snd na) e) b) | CCast (a,c) -> CCast (f e a, Miscops.map_cast_type (f e) c) | CNotation (n,(l,ll,bll)) -> (* This is an approximation because we don't know what binds what *) @@ -247,11 +247,11 @@ let map_constr_expr_with_binders g f e = CAst.map (function let po = Option.map (f (Id.Set.fold g ids e)) rtnpo in CCases (sty, po, List.map (fun (tm,x,y) -> f e tm,x,y) a,bl) | CLetTuple (nal,(ona,po),b,c) -> - let e' = List.fold_right (down_located (name_fold g)) nal e in - let e'' = Option.fold_right (down_located (name_fold g)) ona e in + let e' = List.fold_right (down_located (Name.fold_right g)) nal e in + let e'' = Option.fold_right (down_located (Name.fold_right g)) ona e in CLetTuple (nal,(ona,Option.map (f e'') po),f e b,f e' c) | CIf (c,(ona,po),b1,b2) -> - let e' = Option.fold_right (down_located (name_fold g)) ona e in + let e' = Option.fold_right (down_located (Name.fold_right g)) ona e in CIf (f e c,(ona,Option.map (f e') po),f e b1,f e b2) | CFix (id,dl) -> CFix (id,List.map (fun (id,n,bl,t,d) -> -- cgit v1.2.3