diff options
Diffstat (limited to 'engine/termops.ml')
-rw-r--r-- | engine/termops.ml | 303 |
1 files changed, 159 insertions, 144 deletions
diff --git a/engine/termops.ml b/engine/termops.ml index 35917b368..356312e2f 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -236,35 +236,35 @@ let it_mkLambda_or_LetIn_from_no_LetIn c decls = (* *) (* strips head casts and flattens head applications *) -let rec strip_head_cast c = match kind_of_term c with +let rec strip_head_cast sigma c = match EConstr.kind sigma c with | App (f,cl) -> - let rec collapse_rec f cl2 = match kind_of_term f with + let rec collapse_rec f cl2 = match EConstr.kind sigma f with | App (g,cl1) -> collapse_rec g (Array.append cl1 cl2) | Cast (c,_,_) -> collapse_rec c cl2 - | _ -> if Int.equal (Array.length cl2) 0 then f else mkApp (f,cl2) + | _ -> if Int.equal (Array.length cl2) 0 then f else EConstr.mkApp (f,cl2) in collapse_rec f cl - | Cast (c,_,_) -> strip_head_cast c + | Cast (c,_,_) -> strip_head_cast sigma c | _ -> c -let rec drop_extra_implicit_args c = match kind_of_term c with +let rec drop_extra_implicit_args sigma c = match EConstr.kind sigma c with (* Removed trailing extra implicit arguments, what improves compatibility for constants with recently added maximal implicit arguments *) - | App (f,args) when isEvar (Array.last args) -> - drop_extra_implicit_args - (mkApp (f,fst (Array.chop (Array.length args - 1) args))) - | _ -> c + | App (f,args) when EConstr.isEvar sigma (Array.last args) -> + drop_extra_implicit_args sigma + (EConstr.mkApp (f,fst (Array.chop (Array.length args - 1) args))) + | _ -> EConstr.Unsafe.to_constr c (* Get the last arg of an application *) -let last_arg c = match kind_of_term c with - | App (f,cl) -> Array.last cl +let last_arg sigma c = match EConstr.kind sigma c with + | App (f,cl) -> EConstr.Unsafe.to_constr (Array.last cl) | _ -> anomaly (Pp.str "last_arg") (* Get the last arg of an application *) -let decompose_app_vect c = - match kind_of_term c with - | App (f,cl) -> (f, cl) - | _ -> (c,[||]) +let decompose_app_vect sigma c = + match EConstr.kind sigma c with + | App (f,cl) -> (EConstr.Unsafe.to_constr f, Array.map EConstr.Unsafe.to_constr cl) + | _ -> (EConstr.Unsafe.to_constr c,[||]) let adjust_app_list_size f1 l1 f2 l2 = let len1 = List.length l1 and len2 = List.length l2 in @@ -400,9 +400,11 @@ let map_constr_with_binders_left_to_right g f l c = else mkCoFix (ln,(lna,tl',bl')) (* strong *) -let map_constr_with_full_binders g f l cstr = +let map_constr_with_full_binders sigma g f l cstr = + let inj c = EConstr.Unsafe.to_constr c in + let open EConstr in let open RelDecl in - match kind_of_term cstr with + match EConstr.kind sigma cstr with | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ | Construct _) -> cstr | Cast (c,k, t) -> @@ -411,16 +413,16 @@ let map_constr_with_full_binders g f l cstr = if c==c' && t==t' then cstr else mkCast (c', k, t') | Prod (na,t,c) -> let t' = f l t in - let c' = f (g (LocalAssum (na,t)) l) c in + let c' = f (g (LocalAssum (na, inj t)) l) c in if t==t' && c==c' then cstr else mkProd (na, t', c') | Lambda (na,t,c) -> let t' = f l t in - let c' = f (g (LocalAssum (na,t)) l) c in + let c' = f (g (LocalAssum (na, inj t)) l) c in if t==t' && c==c' then cstr else mkLambda (na, t', c') | LetIn (na,b,t,c) -> let b' = f l b in let t' = f l t in - let c' = f (g (LocalDef (na,b,t)) l) c in + let c' = f (g (LocalDef (na, inj b, inj t)) l) c in if b==b' && t==t' && c==c' then cstr else mkLetIn (na, b', t', c') | App (c,al) -> let c' = f l c in @@ -441,7 +443,7 @@ let map_constr_with_full_binders g f l cstr = | Fix (ln,(lna,tl,bl)) -> let tl' = Array.map (f l) tl in let l' = - Array.fold_left2 (fun l na t -> g (LocalAssum (na,t)) l) l lna tl in + Array.fold_left2 (fun l na t -> g (LocalAssum (na, inj t)) l) l lna tl in let bl' = Array.map (f l') bl in if Array.for_all2 (==) tl tl' && Array.for_all2 (==) bl bl' then cstr @@ -449,7 +451,7 @@ let map_constr_with_full_binders g f l cstr = | CoFix(ln,(lna,tl,bl)) -> let tl' = Array.map (f l) tl in let l' = - Array.fold_left2 (fun l na t -> g (LocalAssum (na,t)) l) l lna tl in + Array.fold_left2 (fun l na t -> g (LocalAssum (na, inj t)) l) l lna tl in let bl' = Array.map (f l') bl in if Array.for_all2 (==) tl tl' && Array.for_all2 (==) bl bl' then cstr @@ -462,30 +464,31 @@ let map_constr_with_full_binders g f l cstr = index) which is processed by [g] (which typically add 1 to [n]) at each binder traversal; it is not recursive *) -let fold_constr_with_full_binders g f n acc c = +let fold_constr_with_full_binders sigma g f n acc c = let open RelDecl in - match kind_of_term c with + let inj c = EConstr.Unsafe.to_constr c in + match EConstr.kind sigma c with | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ | Construct _) -> acc | Cast (c,_, t) -> f n (f n acc c) t - | Prod (na,t,c) -> f (g (LocalAssum (na,t)) n) (f n acc t) c - | Lambda (na,t,c) -> f (g (LocalAssum (na,t)) n) (f n acc t) c - | LetIn (na,b,t,c) -> f (g (LocalDef (na,b,t)) n) (f n (f n acc b) t) c + | Prod (na,t,c) -> f (g (LocalAssum (na, inj t)) n) (f n acc t) c + | Lambda (na,t,c) -> f (g (LocalAssum (na, inj t)) n) (f n acc t) c + | LetIn (na,b,t,c) -> f (g (LocalDef (na, inj b, inj t)) n) (f n (f n acc b) t) c | App (c,l) -> Array.fold_left (f n) (f n acc c) l | Proj (p,c) -> f n acc c | Evar (_,l) -> Array.fold_left (f n) acc l | Case (_,p,c,bl) -> Array.fold_left (f n) (f n (f n acc p) c) bl | Fix (_,(lna,tl,bl)) -> - let n' = CArray.fold_left2 (fun c n t -> g (LocalAssum (n,t)) c) n lna tl in + let n' = CArray.fold_left2 (fun c n t -> g (LocalAssum (n, inj t)) c) n lna tl in let fd = Array.map2 (fun t b -> (t,b)) tl bl in Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd | CoFix (_,(lna,tl,bl)) -> - let n' = CArray.fold_left2 (fun c n t -> g (LocalAssum (n,t)) c) n lna tl in + let n' = CArray.fold_left2 (fun c n t -> g (LocalAssum (n, inj t)) c) n lna tl in let fd = Array.map2 (fun t b -> (t,b)) tl bl in Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd -let fold_constr_with_binders g f n acc c = - fold_constr_with_full_binders (fun _ x -> g x) f n acc c +let fold_constr_with_binders sigma g f n acc c = + fold_constr_with_full_binders sigma (fun _ x -> g x) f n acc c (* [iter_constr_with_full_binders g f acc c] iters [f acc] on the immediate subterms of [c]; it carries an extra data [acc] which is processed by [g] at @@ -520,29 +523,29 @@ let iter_constr_with_full_binders g f l c = exception Occur -let occur_meta c = - let rec occrec c = match kind_of_term c with +let occur_meta sigma c = + let rec occrec c = match EConstr.kind sigma c with | Meta _ -> raise Occur - | _ -> iter_constr occrec c + | _ -> EConstr.iter sigma occrec c in try occrec c; false with Occur -> true -let occur_existential c = - let rec occrec c = match kind_of_term c with +let occur_existential sigma c = + let rec occrec c = match EConstr.kind sigma c with | Evar _ -> raise Occur - | _ -> iter_constr occrec c + | _ -> EConstr.iter sigma occrec c in try occrec c; false with Occur -> true -let occur_meta_or_existential c = - let rec occrec c = match kind_of_term c with +let occur_meta_or_existential sigma c = + let rec occrec c = match EConstr.kind sigma c with | Evar _ -> raise Occur | Meta _ -> raise Occur - | _ -> iter_constr occrec c + | _ -> EConstr.iter sigma occrec c in try occrec c; false with Occur -> true -let occur_evar n c = - let rec occur_rec c = match kind_of_term c with +let occur_evar sigma n c = + let rec occur_rec c = match EConstr.kind sigma c with | Evar (sp,_) when Evar.equal sp n -> raise Occur - | _ -> iter_constr occur_rec c + | _ -> EConstr.iter sigma occur_rec c in try occur_rec c; false with Occur -> true @@ -550,55 +553,55 @@ let occur_in_global env id constr = let vars = vars_of_global env constr in if Id.Set.mem id vars then raise Occur -let occur_var env id c = +let occur_var env sigma id c = let rec occur_rec c = - match kind_of_term c with - | Var _ | Const _ | Ind _ | Construct _ -> occur_in_global env id c - | _ -> iter_constr occur_rec c + match EConstr.kind sigma c with + | Var _ | Const _ | Ind _ | Construct _ -> occur_in_global env id (EConstr.to_constr sigma c) + | _ -> EConstr.iter sigma occur_rec c in try occur_rec c; false with Occur -> true -let occur_var_in_decl env hyp decl = +let occur_var_in_decl env sigma hyp decl = let open NamedDecl in match decl with - | LocalAssum (_,typ) -> occur_var env hyp typ + | LocalAssum (_,typ) -> occur_var env sigma hyp (EConstr.of_constr typ) | LocalDef (_, body, typ) -> - occur_var env hyp typ || - occur_var env hyp body + occur_var env sigma hyp (EConstr.of_constr typ) || + occur_var env sigma hyp (EConstr.of_constr body) -let local_occur_var id c = - let rec occur c = match kind_of_term c with +let local_occur_var sigma id c = + let rec occur c = match EConstr.kind sigma c with | Var id' -> if Id.equal id id' then raise Occur - | _ -> Constr.iter occur c + | _ -> EConstr.iter sigma occur c in try occur c; false with Occur -> true (* returns the list of free debruijn indices in a term *) -let free_rels m = - let rec frec depth acc c = match kind_of_term c with +let free_rels sigma m = + let rec frec depth acc c = match EConstr.kind sigma c with | Rel n -> if n >= depth then Int.Set.add (n-depth+1) acc else acc - | _ -> fold_constr_with_binders succ frec depth acc c + | _ -> fold_constr_with_binders sigma succ frec depth acc c in frec 1 Int.Set.empty m (* collects all metavar occurrences, in left-to-right order, preserving * repetitions and all. *) -let collect_metas c = +let collect_metas sigma c = let rec collrec acc c = - match kind_of_term c with + match EConstr.kind sigma c with | Meta mv -> List.add_set Int.equal mv acc - | _ -> fold_constr collrec acc c + | _ -> EConstr.fold sigma collrec acc c in List.rev (collrec [] c) (* collects all vars; warning: this is only visible vars, not dependencies in all section variables; for the latter, use global_vars_set *) -let collect_vars c = - let rec aux vars c = match kind_of_term c with +let collect_vars sigma c = + let rec aux vars c = match EConstr.kind sigma c with | Var id -> Id.Set.add id vars - | _ -> fold_constr aux vars c in + | _ -> EConstr.fold sigma aux vars c in aux Id.Set.empty c let vars_of_global_reference env gr = @@ -608,54 +611,54 @@ let vars_of_global_reference env gr = (* Tests whether [m] is a subterm of [t]: [m] is appropriately lifted through abstractions of [t] *) -let dependent_main noevar univs m t = +let dependent_main noevar univs sigma m t = let eqc x y = - if univs then not (Option.is_empty (Universes.eq_constr_universes x y)) - else eq_constr_nounivs x y + if univs then not (Option.is_empty (EConstr.eq_constr_universes sigma x y)) + else EConstr.eq_constr_nounivs sigma x y in let rec deprec m t = if eqc m t then raise Occur else - match kind_of_term m, kind_of_term t with + match EConstr.kind sigma m, EConstr.kind sigma t with | App (fm,lm), App (ft,lt) when Array.length lm < Array.length lt -> - deprec m (mkApp (ft,Array.sub lt 0 (Array.length lm))); + deprec m (EConstr.mkApp (ft,Array.sub lt 0 (Array.length lm))); CArray.Fun1.iter deprec m (Array.sub lt (Array.length lm) ((Array.length lt) - (Array.length lm))) - | _, Cast (c,_,_) when noevar && isMeta c -> () + | _, Cast (c,_,_) when noevar && EConstr.isMeta sigma c -> () | _, Evar _ when noevar -> () - | _ -> iter_constr_with_binders (fun c -> lift 1 c) deprec m t + | _ -> EConstr.iter_with_binders sigma (fun c -> EConstr.Vars.lift 1 c) deprec m t in try deprec m t; false with Occur -> true -let dependent = dependent_main false false -let dependent_no_evar = dependent_main true false +let dependent sigma c t = dependent_main false false sigma c t +let dependent_no_evar sigma c t = dependent_main true false sigma c t -let dependent_univs = dependent_main false true -let dependent_univs_no_evar = dependent_main true true +let dependent_univs sigma c t = dependent_main false true sigma c t +let dependent_univs_no_evar sigma c t = dependent_main true true sigma c t -let dependent_in_decl a decl = +let dependent_in_decl sigma a decl = let open NamedDecl in match decl with - | LocalAssum (_,t) -> dependent a t - | LocalDef (_, body, t) -> dependent a body || dependent a t + | LocalAssum (_,t) -> dependent sigma a (EConstr.of_constr t) + | LocalDef (_, body, t) -> dependent sigma a (EConstr.of_constr body) || dependent sigma a (EConstr.of_constr t) -let count_occurrences m t = +let count_occurrences sigma m t = let n = ref 0 in let rec countrec m t = - if eq_constr m t then + if EConstr.eq_constr sigma m t then incr n else - match kind_of_term m, kind_of_term t with + match EConstr.kind sigma m, EConstr.kind sigma t with | App (fm,lm), App (ft,lt) when Array.length lm < Array.length lt -> - countrec m (mkApp (ft,Array.sub lt 0 (Array.length lm))); + countrec m (EConstr.mkApp (ft,Array.sub lt 0 (Array.length lm))); Array.iter (countrec m) (Array.sub lt (Array.length lm) ((Array.length lt) - (Array.length lm))) - | _, Cast (c,_,_) when isMeta c -> () + | _, Cast (c,_,_) when EConstr.isMeta sigma c -> () | _, Evar _ -> () - | _ -> iter_constr_with_binders (lift 1) countrec m t + | _ -> EConstr.iter_with_binders sigma (EConstr.Vars.lift 1) countrec m t in countrec m t; !n @@ -663,7 +666,7 @@ let count_occurrences m t = (* Synonymous *) let occur_term = dependent -let pop t = lift (-1) t +let pop t = EConstr.Unsafe.to_constr (EConstr.Vars.lift (-1) t) (***************************) (* bindings functions *) @@ -678,45 +681,45 @@ let rec subst_meta bl c = | Meta i -> (try Int.List.assoc i bl with Not_found -> c) | _ -> map_constr (subst_meta bl) c -let rec strip_outer_cast c = match kind_of_term c with - | Cast (c,_,_) -> strip_outer_cast c - | _ -> c +let rec strip_outer_cast sigma c = match EConstr.kind sigma c with + | Cast (c,_,_) -> strip_outer_cast sigma c + | _ -> EConstr.Unsafe.to_constr c (* flattens application lists throwing casts in-between *) -let collapse_appl c = match kind_of_term c with +let collapse_appl sigma c = match EConstr.kind sigma c with | App (f,cl) -> let rec collapse_rec f cl2 = - match kind_of_term (strip_outer_cast f) with + match EConstr.kind sigma (EConstr.of_constr (strip_outer_cast sigma f)) with | App (g,cl1) -> collapse_rec g (Array.append cl1 cl2) - | _ -> mkApp (f,cl2) + | _ -> EConstr.mkApp (f,cl2) in - collapse_rec f cl - | _ -> c + EConstr.Unsafe.to_constr (collapse_rec f cl) + | _ -> EConstr.Unsafe.to_constr c (* First utilities for avoiding telescope computation for subst_term *) -let prefix_application eq_fun (k,c) (t : constr) = - let c' = collapse_appl c and t' = collapse_appl t in - match kind_of_term c', kind_of_term t' with +let prefix_application sigma eq_fun (k,c) t = + let c' = EConstr.of_constr (collapse_appl sigma c) and t' = EConstr.of_constr (collapse_appl sigma t) in + match EConstr.kind sigma c', EConstr.kind sigma t' with | App (f1,cl1), App (f2,cl2) -> let l1 = Array.length cl1 and l2 = Array.length cl2 in if l1 <= l2 - && eq_fun c' (mkApp (f2, Array.sub cl2 0 l1)) then - Some (mkApp (mkRel k, Array.sub cl2 l1 (l2 - l1))) + && eq_fun sigma c' (EConstr.mkApp (f2, Array.sub cl2 0 l1)) then + Some (EConstr.mkApp (EConstr.mkRel k, Array.sub cl2 l1 (l2 - l1))) else None | _ -> None -let my_prefix_application eq_fun (k,c) (by_c : constr) (t : constr) = - let c' = collapse_appl c and t' = collapse_appl t in - match kind_of_term c', kind_of_term t' with +let my_prefix_application sigma eq_fun (k,c) by_c t = + let c' = EConstr.of_constr (collapse_appl sigma c) and t' = EConstr.of_constr (collapse_appl sigma t) in + match EConstr.kind sigma c', EConstr.kind sigma t' with | App (f1,cl1), App (f2,cl2) -> let l1 = Array.length cl1 and l2 = Array.length cl2 in if l1 <= l2 - && eq_fun c' (mkApp (f2, Array.sub cl2 0 l1)) then - Some (mkApp ((lift k by_c), Array.sub cl2 l1 (l2 - l1))) + && eq_fun sigma c' (EConstr.mkApp (f2, Array.sub cl2 0 l1)) then + Some (EConstr.mkApp ((EConstr.Vars.lift k by_c), Array.sub cl2 l1 (l2 - l1))) else None | _ -> None @@ -725,35 +728,35 @@ let my_prefix_application eq_fun (k,c) (by_c : constr) (t : constr) = substitutes [(Rel 1)] for all occurrences of term [c] in a term [t]; works if [c] has rels *) -let subst_term_gen eq_fun c t = +let subst_term_gen sigma eq_fun c t = let rec substrec (k,c as kc) t = - match prefix_application eq_fun kc t with + match prefix_application sigma eq_fun kc t with | Some x -> x | None -> - if eq_fun c t then mkRel k + if eq_fun sigma c t then EConstr.mkRel k else - map_constr_with_binders (fun (k,c) -> (k+1,lift 1 c)) substrec kc t + EConstr.map_with_binders sigma (fun (k,c) -> (k+1, EConstr.Vars.lift 1 c)) substrec kc t in - substrec (1,c) t + EConstr.Unsafe.to_constr (substrec (1,c) t) -let subst_term = subst_term_gen eq_constr +let subst_term sigma c t = subst_term_gen sigma EConstr.eq_constr c t (* Recognizing occurrences of a given subterm in a term : [replace_term c1 c2 t] substitutes [c2] for all occurrences of term [c1] in a term [t]; works if [c1] and [c2] have rels *) -let replace_term_gen eq_fun c by_c in_t = +let replace_term_gen sigma eq_fun c by_c in_t = let rec substrec (k,c as kc) t = - match my_prefix_application eq_fun kc by_c t with + match my_prefix_application sigma eq_fun kc by_c t with | Some x -> x | None -> - (if eq_fun c t then (lift k by_c) else - map_constr_with_binders (fun (k,c) -> (k+1,lift 1 c)) + (if eq_fun sigma c t then (EConstr.Vars.lift k by_c) else + EConstr.map_with_binders sigma (fun (k,c) -> (k+1,EConstr.Vars.lift 1 c)) substrec kc t) in - substrec (0,c) in_t + EConstr.Unsafe.to_constr (substrec (0,c) in_t) -let replace_term = replace_term_gen eq_constr +let replace_term sigma c byc t = replace_term_gen sigma EConstr.eq_constr c byc t let vars_of_env env = let s = @@ -804,13 +807,13 @@ let is_section_variable id = try let _ = Global.lookup_named id in true with Not_found -> false -let isGlobalRef c = - match kind_of_term c with +let isGlobalRef sigma c = + match EConstr.kind sigma c with | Const _ | Ind _ | Construct _ | Var _ -> true | _ -> false -let is_template_polymorphic env f = - match kind_of_term f with +let is_template_polymorphic env sigma f = + match EConstr.kind sigma f with | Ind ind -> Environ.template_polymorphic_pind ind env | Const c -> Environ.template_polymorphic_pconstant c env | _ -> false @@ -882,45 +885,46 @@ let filtering env cv_pb c1 c2 = in aux env cv_pb c1 c2; !evm -let decompose_prod_letin : constr -> int * Context.Rel.t * constr = - let rec prodec_rec i l c = match kind_of_term c with - | Prod (n,t,c) -> prodec_rec (succ i) (RelDecl.LocalAssum (n,t)::l) c - | LetIn (n,d,t,c) -> prodec_rec (succ i) (RelDecl.LocalDef (n,d,t)::l) c - | Cast (c,_,_) -> prodec_rec i l c - | _ -> i,l,c in - prodec_rec 0 [] +let decompose_prod_letin sigma c = + let inj c = EConstr.Unsafe.to_constr c in + let rec prodec_rec i l sigma c = match EConstr.kind sigma c with + | Prod (n,t,c) -> prodec_rec (succ i) (RelDecl.LocalAssum (n, inj t)::l) sigma c + | LetIn (n,d,t,c) -> prodec_rec (succ i) (RelDecl.LocalDef (n, inj d, inj t)::l) sigma c + | Cast (c,_,_) -> prodec_rec i l sigma c + | _ -> i,l, inj c in + prodec_rec 0 [] sigma c (* (nb_lam [na1:T1]...[nan:Tan]c) where c is not an abstraction * gives n (casts are ignored) *) -let nb_lam = - let rec nbrec n c = match kind_of_term c with +let nb_lam sigma c = + let rec nbrec n c = match EConstr.kind sigma c with | Lambda (_,_,c) -> nbrec (n+1) c | Cast (c,_,_) -> nbrec n c | _ -> n in - nbrec 0 + nbrec 0 c (* similar to nb_lam, but gives the number of products instead *) -let nb_prod = - let rec nbrec n c = match kind_of_term c with +let nb_prod sigma c = + let rec nbrec n c = match EConstr.kind sigma c with | Prod (_,_,c) -> nbrec (n+1) c | Cast (c,_,_) -> nbrec n c | _ -> n in - nbrec 0 + nbrec 0 c -let nb_prod_modulo_zeta x = +let nb_prod_modulo_zeta sigma x = let rec count n c = - match kind_of_term c with + match EConstr.kind sigma c with Prod(_,_,t) -> count (n+1) t - | LetIn(_,a,_,t) -> count n (subst1 a t) + | LetIn(_,a,_,t) -> count n (EConstr.Vars.subst1 a t) | Cast(c,_,_) -> count n c | _ -> n in count 0 x -let align_prod_letin c a : Context.Rel.t * constr = - let (lc,_,_) = decompose_prod_letin c in - let (la,l,a) = decompose_prod_letin a in +let align_prod_letin sigma c a : Context.Rel.t * constr = + let (lc,_,_) = decompose_prod_letin sigma c in + let (la,l,a) = decompose_prod_letin sigma a in if not (la >= lc) then invalid_arg "align_prod_letin"; let (l1,l2) = Util.List.chop lc l in l2,it_mkProd_or_LetIn a l1 @@ -1031,22 +1035,33 @@ let clear_named_body id env = | d -> push_named d in fold_named_context aux env ~init:(reset_context env) -let global_vars env ids = Id.Set.elements (global_vars_set env ids) +let global_vars_set env sigma constr = + let rec filtrec acc c = + let acc = match EConstr.kind sigma c with + | Var _ | Const _ | Ind _ | Construct _ -> + Id.Set.union (vars_of_global env (EConstr.Unsafe.to_constr c)) acc + | _ -> acc + in + EConstr.fold sigma filtrec acc c + in + filtrec Id.Set.empty constr + +let global_vars env sigma ids = Id.Set.elements (global_vars_set env sigma ids) -let global_vars_set_of_decl env = function - | NamedDecl.LocalAssum (_,t) -> global_vars_set env t +let global_vars_set_of_decl env sigma = function + | NamedDecl.LocalAssum (_,t) -> global_vars_set env sigma (EConstr.of_constr t) | NamedDecl.LocalDef (_,c,t) -> - Id.Set.union (global_vars_set env t) - (global_vars_set env c) + Id.Set.union (global_vars_set env sigma (EConstr.of_constr t)) + (global_vars_set env sigma (EConstr.of_constr c)) -let dependency_closure env sign hyps = +let dependency_closure env sigma sign hyps = if Id.Set.is_empty hyps then [] else let (_,lh) = Context.Named.fold_inside (fun (hs,hl) d -> let x = NamedDecl.get_id d in if Id.Set.mem x hs then - (Id.Set.union (global_vars_set_of_decl env d) (Id.Set.remove x hs), + (Id.Set.union (global_vars_set_of_decl env sigma d) (Id.Set.remove x hs), x::hl) else (hs,hl)) ~init:(hyps,[]) |