diff options
72 files changed, 825 insertions, 739 deletions
diff --git a/engine/evarutil.ml b/engine/evarutil.ml index 13444cb37..05f98a41f 100644 --- a/engine/evarutil.ml +++ b/engine/evarutil.ml @@ -540,12 +540,12 @@ let rec check_and_clear_in_constr env evdref err ids global c = (* Check if some id to clear occurs in the instance a of rid in ev and remember the dependency *) let check id = if Id.Set.mem id ids then raise (Depends id) in - let () = Id.Set.iter check (collect_vars a) in + let () = Id.Set.iter check (collect_vars !evdref (EConstr.of_constr a)) in (* Check if some rid to clear in the context of ev has dependencies in another hyp of the context of ev and transitively remember the dependency *) let check id _ = - if occur_var_in_decl (Global.env ()) id h + if occur_var_in_decl (Global.env ()) !evdref id h then raise (Depends id) in let () = Id.Map.iter check ri in 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,[]) diff --git a/engine/termops.mli b/engine/termops.mli index 78826f79a..5d53ce09e 100644 --- a/engine/termops.mli +++ b/engine/termops.mli @@ -69,8 +69,9 @@ val map_constr_with_binders_left_to_right : ('a -> constr -> constr) -> 'a -> constr -> constr val map_constr_with_full_binders : + Evd.evar_map -> (Context.Rel.Declaration.t -> 'a -> 'a) -> - ('a -> constr -> constr) -> 'a -> constr -> constr + ('a -> EConstr.t -> EConstr.t) -> 'a -> EConstr.t -> EConstr.t (** [fold_constr_with_binders g f n acc c] folds [f n] on the immediate subterms of [c] starting from [acc] and proceeding from left to @@ -80,11 +81,12 @@ val map_constr_with_full_binders : each binder traversal; it is not recursive *) val fold_constr_with_binders : - ('a -> 'a) -> ('a -> 'b -> constr -> 'b) -> 'a -> 'b -> constr -> 'b + Evd.evar_map -> ('a -> 'a) -> + ('a -> 'b -> EConstr.t -> 'b) -> 'a -> 'b -> EConstr.t -> 'b val fold_constr_with_full_binders : - (Context.Rel.Declaration.t -> 'a -> 'a) -> ('a -> 'b -> constr -> 'b) -> - 'a -> 'b -> constr -> 'b + Evd.evar_map -> (Context.Rel.Declaration.t -> 'a -> 'a) -> + ('a -> 'b -> EConstr.t -> 'b) -> 'a -> 'b -> EConstr.t -> 'b val iter_constr_with_full_binders : (Context.Rel.Declaration.t -> 'a -> 'a) -> ('a -> constr -> unit) -> 'a -> @@ -92,39 +94,39 @@ val iter_constr_with_full_binders : (**********************************************************************) -val strip_head_cast : constr -> constr -val drop_extra_implicit_args : constr -> constr +val strip_head_cast : Evd.evar_map -> EConstr.t -> EConstr.t +val drop_extra_implicit_args : Evd.evar_map -> EConstr.t -> constr (** occur checks *) exception Occur -val occur_meta : types -> bool -val occur_existential : types -> bool -val occur_meta_or_existential : types -> bool -val occur_evar : existential_key -> types -> bool -val occur_var : env -> Id.t -> types -> bool +val occur_meta : Evd.evar_map -> EConstr.t -> bool +val occur_existential : Evd.evar_map -> EConstr.t -> bool +val occur_meta_or_existential : Evd.evar_map -> EConstr.t -> bool +val occur_evar : Evd.evar_map -> existential_key -> EConstr.t -> bool +val occur_var : env -> Evd.evar_map -> Id.t -> EConstr.t -> bool val occur_var_in_decl : - env -> + env -> Evd.evar_map -> Id.t -> Context.Named.Declaration.t -> bool (** As {!occur_var} but assume the identifier not to be a section variable *) -val local_occur_var : Id.t -> types -> bool +val local_occur_var : Evd.evar_map -> Id.t -> EConstr.t -> bool -val free_rels : constr -> Int.Set.t +val free_rels : Evd.evar_map -> EConstr.t -> Int.Set.t (** [dependent m t] tests whether [m] is a subterm of [t] *) -val dependent : constr -> constr -> bool -val dependent_no_evar : constr -> constr -> bool -val dependent_univs : constr -> constr -> bool -val dependent_univs_no_evar : constr -> constr -> bool -val dependent_in_decl : constr -> Context.Named.Declaration.t -> bool -val count_occurrences : constr -> constr -> int -val collect_metas : constr -> int list -val collect_vars : constr -> Id.Set.t (** for visible vars only *) +val dependent : Evd.evar_map -> EConstr.t -> EConstr.t -> bool +val dependent_no_evar : Evd.evar_map -> EConstr.t -> EConstr.t -> bool +val dependent_univs : Evd.evar_map -> EConstr.t -> EConstr.t -> bool +val dependent_univs_no_evar : Evd.evar_map -> EConstr.t -> EConstr.t -> bool +val dependent_in_decl : Evd.evar_map -> EConstr.t -> Context.Named.Declaration.t -> bool +val count_occurrences : Evd.evar_map -> EConstr.t -> EConstr.t -> int +val collect_metas : Evd.evar_map -> EConstr.t -> int list +val collect_vars : Evd.evar_map -> EConstr.t -> Id.Set.t (** for visible vars only *) val vars_of_global_reference : env -> Globnames.global_reference -> Id.Set.t -val occur_term : constr -> constr -> bool (** Synonymous - of dependent - Substitution of metavariables *) +val occur_term : Evd.evar_map -> EConstr.t -> EConstr.t -> bool (** Synonymous of dependent *) + +(* Substitution of metavariables *) type meta_value_map = (metavariable * constr) list val subst_meta : meta_value_map -> constr -> constr @@ -132,7 +134,7 @@ val subst_meta : meta_value_map -> constr -> constr type meta_type_map = (metavariable * types) list (** [pop c] lifts by -1 the positive indexes in [c] *) -val pop : constr -> constr +val pop : EConstr.t -> constr (** {6 ... } *) (** Substitution of an arbitrary large term. Uses equality modulo @@ -140,20 +142,20 @@ val pop : constr -> constr (** [subst_term_gen eq d c] replaces [d] by [Rel 1] in [c] using [eq] as equality *) -val subst_term_gen : - (constr -> constr -> bool) -> constr -> constr -> constr +val subst_term_gen : Evd.evar_map -> + (Evd.evar_map -> EConstr.t -> EConstr.t -> bool) -> EConstr.t -> EConstr.t -> constr (** [replace_term_gen eq d e c] replaces [d] by [e] in [c] using [eq] as equality *) val replace_term_gen : - (constr -> constr -> bool) -> - constr -> constr -> constr -> constr + Evd.evar_map -> (Evd.evar_map -> EConstr.t -> EConstr.t -> bool) -> + EConstr.t -> EConstr.t -> EConstr.t -> constr (** [subst_term d c] replaces [d] by [Rel 1] in [c] *) -val subst_term : constr -> constr -> constr +val subst_term : Evd.evar_map -> EConstr.t -> EConstr.t -> constr (** [replace_term d e c] replaces [d] by [e] in [c] *) -val replace_term : constr -> constr -> constr -> constr +val replace_term : Evd.evar_map -> EConstr.t -> EConstr.t -> EConstr.t -> constr (** Alternative term equalities *) val base_sort_cmp : Reduction.conv_pb -> sorts -> sorts -> bool @@ -165,11 +167,11 @@ val eq_constr : constr -> constr -> bool (* FIXME rename: erases universes*) val eta_reduce_head : constr -> constr (** Flattens application lists *) -val collapse_appl : constr -> constr +val collapse_appl : Evd.evar_map -> EConstr.t -> constr (** Remove recursively the casts around a term i.e. [strip_outer_cast (Cast (Cast ... (Cast c, t) ... ))] is [c]. *) -val strip_outer_cast : constr -> constr +val strip_outer_cast : Evd.evar_map -> EConstr.t -> constr exception CannotFilter @@ -182,24 +184,24 @@ exception CannotFilter type subst = (Context.Rel.t * constr) Evar.Map.t val filtering : Context.Rel.t -> Reduction.conv_pb -> constr -> constr -> subst -val decompose_prod_letin : constr -> int * Context.Rel.t * constr -val align_prod_letin : constr -> constr -> Context.Rel.t * constr +val decompose_prod_letin : Evd.evar_map -> EConstr.t -> int * Context.Rel.t * constr +val align_prod_letin : Evd.evar_map -> EConstr.t -> EConstr.t -> Context.Rel.t * constr (** [nb_lam] {% $ %}[x_1:T_1]...[x_n:T_n]c{% $ %} where {% $ %}c{% $ %} is not an abstraction gives {% $ %}n{% $ %} (casts are ignored) *) -val nb_lam : constr -> int +val nb_lam : Evd.evar_map -> EConstr.t -> int (** Similar to [nb_lam], but gives the number of products instead *) -val nb_prod : constr -> int +val nb_prod : Evd.evar_map -> EConstr.t -> int (** Similar to [nb_prod], but zeta-contracts let-in on the way *) -val nb_prod_modulo_zeta : constr -> int +val nb_prod_modulo_zeta : Evd.evar_map -> EConstr.t -> int (** Get the last arg of a constr intended to be an application *) -val last_arg : constr -> constr +val last_arg : Evd.evar_map -> EConstr.t -> constr (** Force the decomposition of a term as an applicative one *) -val decompose_app_vect : constr -> constr * constr array +val decompose_app_vect : Evd.evar_map -> EConstr.t -> constr * constr array val adjust_app_list_size : constr -> constr list -> constr -> constr list -> (constr * constr list * constr * constr list) @@ -250,19 +252,19 @@ val compact_named_context : Context.Named.t -> Context.Compacted.t val clear_named_body : Id.t -> env -> env -val global_vars : env -> constr -> Id.t list -val global_vars_set_of_decl : env -> Context.Named.Declaration.t -> Id.Set.t +val global_vars : env -> Evd.evar_map -> EConstr.t -> Id.t list +val global_vars_set_of_decl : env -> Evd.evar_map -> Context.Named.Declaration.t -> Id.Set.t (** Gives an ordered list of hypotheses, closed by dependencies, containing a given set *) -val dependency_closure : env -> Context.Named.t -> Id.Set.t -> Id.t list +val dependency_closure : env -> Evd.evar_map -> Context.Named.t -> Id.Set.t -> Id.t list (** Test if an identifier is the basename of a global reference *) val is_section_variable : Id.t -> bool -val isGlobalRef : constr -> bool +val isGlobalRef : Evd.evar_map -> EConstr.t -> bool -val is_template_polymorphic : env -> constr -> bool +val is_template_polymorphic : env -> Evd.evar_map -> EConstr.t -> bool (** Combinators on judgments *) diff --git a/ltac/extratactics.ml4 b/ltac/extratactics.ml4 index 8ea60b39a..beaf778a6 100644 --- a/ltac/extratactics.ml4 +++ b/ltac/extratactics.ml4 @@ -747,14 +747,14 @@ let mkCaseEq a : unit Proofview.tactic = let case_eq_intros_rewrite x = Proofview.Goal.nf_enter { enter = begin fun gl -> - let n = nb_prod (Proofview.Goal.concl gl) in + let n = nb_prod (Tacmach.New.project gl) (EConstr.of_constr (Proofview.Goal.concl gl)) in (* Pp.msgnl (Printer.pr_lconstr x); *) Tacticals.New.tclTHENLIST [ mkCaseEq x; Proofview.Goal.nf_enter { enter = begin fun gl -> let concl = Proofview.Goal.concl gl in let hyps = Tacmach.New.pf_ids_of_hyps gl in - let n' = nb_prod concl in + let n' = nb_prod (Tacmach.New.project gl) (EConstr.of_constr concl) in let h = Tacmach.New.of_old (fun g -> fresh_id hyps (Id.of_string "heq") g) gl in Tacticals.New.tclTHENLIST [ Tacticals.New.tclDO (n'-n-1) intro; diff --git a/ltac/rewrite.ml b/ltac/rewrite.ml index 217f5f42e..cd76d4746 100644 --- a/ltac/rewrite.ml +++ b/ltac/rewrite.ml @@ -1527,23 +1527,24 @@ let cl_rewrite_clause_aux ?(abs=None) strat env avoid sigma concl is_hyp : resul in Some (Some (evars, res, newt)) (** Insert a declaration after the last declaration it depends on *) -let rec insert_dependent env decl accu hyps = match hyps with +let rec insert_dependent env sigma decl accu hyps = match hyps with | [] -> List.rev_append accu [decl] | ndecl :: rem -> - if occur_var_in_decl env (NamedDecl.get_id ndecl) decl then + if occur_var_in_decl env sigma (NamedDecl.get_id ndecl) decl then List.rev_append accu (decl :: hyps) else - insert_dependent env decl (ndecl :: accu) rem + insert_dependent env sigma decl (ndecl :: accu) rem let assert_replacing id newt tac = let prf = Proofview.Goal.nf_enter { enter = begin fun gl -> let concl = Proofview.Goal.concl gl in let env = Proofview.Goal.env gl in + let sigma = Tacmach.New.project gl in let ctx = Environ.named_context env in let after, before = List.split_when (NamedDecl.get_id %> Id.equal id) ctx in let nc = match before with | [] -> assert false - | d :: rem -> insert_dependent env (LocalAssum (NamedDecl.get_id d, newt)) [] after @ rem + | d :: rem -> insert_dependent env sigma (LocalAssum (NamedDecl.get_id d, newt)) [] after @ rem in let env' = Environ.reset_with_named_context (val_of_named_context nc) env in Refine.refine ~unsafe:false { run = begin fun sigma -> @@ -1616,7 +1617,7 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause = | Some id -> (** Only consider variables not depending on [id] *) let ctx = Environ.named_context env in - let filter decl = not (occur_var_in_decl env id decl) in + let filter decl = not (occur_var_in_decl env sigma id decl) in let nctx = List.filter filter ctx in Environ.reset_with_named_context (Environ.val_of_named_context nctx) env in diff --git a/ltac/tauto.ml b/ltac/tauto.ml index 756958c2f..6eab003b5 100644 --- a/ltac/tauto.ml +++ b/ltac/tauto.ml @@ -16,6 +16,7 @@ open Tacexpr open Tacinterp open Util open Tacticals.New +open Proofview.Notations let tauto_plugin = "tauto" let () = Mltop.add_known_module tauto_plugin @@ -111,14 +112,16 @@ let split = Tactics.split_with_bindings false [Misctypes.NoBindings] (** Test *) let is_empty _ ist = - if is_empty_type (assoc_var "X1" ist) then idtac else fail + Proofview.tclEVARMAP >>= fun sigma -> + if is_empty_type sigma (assoc_var "X1" ist) then idtac else fail (* Strictly speaking, this exceeds the propositional fragment as it matches also equality types (and solves them if a reflexivity) *) let is_unit_or_eq _ ist = + Proofview.tclEVARMAP >>= fun sigma -> let flags = assoc_flags ist in let test = if flags.strict_unit then is_unit_type else is_unit_or_eq_type in - if test (assoc_var "X1" ist) then idtac else fail + if test sigma (assoc_var "X1" ist) then idtac else fail let bugged_is_binary t = isApp t && @@ -132,21 +135,23 @@ let bugged_is_binary t = (** Dealing with conjunction *) let is_conj _ ist = + Proofview.tclEVARMAP >>= fun sigma -> let flags = assoc_flags ist in let ind = assoc_var "X1" ist in if (not flags.binary_mode_bugged_detection || bugged_is_binary ind) && - is_conjunction + is_conjunction sigma ~strict:flags.strict_in_hyp_and_ccl ~onlybinary:flags.binary_mode ind then idtac else fail let flatten_contravariant_conj _ ist = + Proofview.tclEVARMAP >>= fun sigma -> let flags = assoc_flags ist in let typ = assoc_var "X1" ist in let c = assoc_var "X2" ist in let hyp = assoc_var "id" ist in - match match_with_conjunction + match match_with_conjunction sigma ~strict:flags.strict_in_contravariant_hyp ~onlybinary:flags.binary_mode typ with @@ -160,21 +165,23 @@ let flatten_contravariant_conj _ ist = (** Dealing with disjunction *) let is_disj _ ist = + Proofview.tclEVARMAP >>= fun sigma -> let flags = assoc_flags ist in let t = assoc_var "X1" ist in if (not flags.binary_mode_bugged_detection || bugged_is_binary t) && - is_disjunction + is_disjunction sigma ~strict:flags.strict_in_hyp_and_ccl ~onlybinary:flags.binary_mode t then idtac else fail let flatten_contravariant_disj _ ist = + Proofview.tclEVARMAP >>= fun sigma -> let flags = assoc_flags ist in let typ = assoc_var "X1" ist in let c = assoc_var "X2" ist in let hyp = assoc_var "id" ist in - match match_with_disjunction + match match_with_disjunction sigma ~strict:flags.strict_in_contravariant_hyp ~onlybinary:flags.binary_mode typ with diff --git a/plugins/btauto/refl_btauto.ml b/plugins/btauto/refl_btauto.ml index 2c5b108e5..3ba5da149 100644 --- a/plugins/btauto/refl_btauto.ml +++ b/plugins/btauto/refl_btauto.ml @@ -14,8 +14,8 @@ let get_inductive dir s = let glob_ref () = Coqlib.find_reference contrib_name ("Coq" :: dir) s in Lazy.from_fun (fun () -> Globnames.destIndRef (glob_ref ())) -let decomp_term (c : Term.constr) = - Term.kind_of_term (Termops.strip_outer_cast c) +let decomp_term sigma (c : Term.constr) = + Term.kind_of_term (Termops.strip_outer_cast sigma (EConstr.of_constr c)) let lapp c v = Term.mkApp (Lazy.force c, v) @@ -105,7 +105,7 @@ module Bool = struct | Negb of t | Ifb of t * t * t - let quote (env : Env.t) (c : Term.constr) : t = + let quote (env : Env.t) sigma (c : Term.constr) : t = let trueb = Lazy.force trueb in let falseb = Lazy.force falseb in let andb = Lazy.force andb in @@ -113,7 +113,7 @@ module Bool = struct let xorb = Lazy.force xorb in let negb = Lazy.force negb in - let rec aux c = match decomp_term c with + let rec aux c = match decomp_term sigma c with | Term.App (head, args) -> if head === andb && Array.length args = 2 then Andb (aux args.(0), aux args.(1)) @@ -181,7 +181,7 @@ module Btauto = struct let var = lapp witness [|p|] in (* Compute an assignment that dissatisfies the goal *) let _, var = Tacmach.pf_reduction_of_red_expr gl (Genredexpr.CbvVm None) var in - let rec to_list l = match decomp_term l with + let rec to_list l = match decomp_term (Tacmach.project gl) l with | Term.App (c, _) when c === (Lazy.force CoqList._nil) -> [] | Term.App (c, [|_; h; t|]) @@ -220,7 +220,7 @@ module Btauto = struct Proofview.Goal.nf_enter { enter = begin fun gl -> let concl = Proofview.Goal.concl gl in let eq = Lazy.force eq in - let t = decomp_term concl in + let t = decomp_term (Tacmach.New.project gl) concl in match t with | Term.App (c, [|typ; p; _|]) when c === eq -> (* should be an equality [@eq poly ?p (Cst false)] *) @@ -234,15 +234,16 @@ module Btauto = struct let tac = Proofview.Goal.nf_enter { enter = begin fun gl -> let concl = Proofview.Goal.concl gl in + let sigma = Tacmach.New.project gl in let eq = Lazy.force eq in let bool = Lazy.force Bool.typ in - let t = decomp_term concl in + let t = decomp_term sigma concl in match t with | Term.App (c, [|typ; tl; tr|]) when typ === bool && c === eq -> let env = Env.empty () in - let fl = Bool.quote env tl in - let fr = Bool.quote env tr in + let fl = Bool.quote env sigma tl in + let fr = Bool.quote env sigma tr in let env = Env.to_list env in let fl = reify env fl in let fr = reify env fr in diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index b5ca2f50f..425bb2d6f 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -58,8 +58,8 @@ let rec decompose_term env sigma t= let tf=decompose_term env sigma f in let targs=Array.map (decompose_term env sigma) args in Array.fold_left (fun s t->Appli (s,t)) tf targs - | Prod (_,a,_b) when not (Termops.dependent (mkRel 1) _b) -> - let b = Termops.pop _b in + | Prod (_,a,_b) when EConstr.Vars.noccurn sigma 1 (EConstr.of_constr _b) -> + let b = Termops.pop (EConstr.of_constr _b) in let sort_b = sf_of env sigma b in let sort_a = sf_of env sigma a in Appli(Appli(Product (sort_a,sort_b) , @@ -86,7 +86,7 @@ let rec decompose_term env sigma t= let p' = Projection.map canon_const p in (Appli (Symb (mkConst (Projection.constant p')), decompose_term env sigma c)) | _ -> - let t = Termops.strip_outer_cast t in + let t = Termops.strip_outer_cast sigma (EConstr.of_constr t) in if closed0 t then Symb t else raise Not_found (* decompose equality in members and type *) @@ -112,8 +112,8 @@ let rec pattern_of_constr env sigma c = (Array.map_to_list (pattern_of_constr env sigma) args) in PApp (pf,List.rev pargs), List.fold_left Int.Set.union Int.Set.empty lrels - | Prod (_,a,_b) when not (Termops.dependent (mkRel 1) _b) -> - let b = Termops.pop _b in + | Prod (_,a,_b) when EConstr.Vars.noccurn sigma 1 (EConstr.of_constr _b) -> + let b = Termops.pop (EConstr.of_constr _b) in let pa,sa = pattern_of_constr env sigma a in let pb,sb = pattern_of_constr env sigma b in let sort_b = sf_of env sigma b in diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml index f68c01b18..65d273faf 100644 --- a/plugins/decl_mode/decl_interp.ml +++ b/plugins/decl_mode/decl_interp.ml @@ -374,7 +374,7 @@ let interp_cases info env sigma params (pat:cases_pattern_expr) hyps = match st'.st_it with Thesis nam -> {st_it=Thesis nam;st_label=st'.st_label} | This _ -> {st_it = This st.st_it;st_label=st.st_label} in - let thyps = fst (match_hyps blend nam2 (Termops.pop rest1) hyps) in + let thyps = fst (match_hyps blend nam2 (Termops.pop (EConstr.of_constr rest1)) hyps) in tparams,{pat_vars=tpatvars; pat_aliases=taliases; pat_constr=pat_pat; diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml index e19dc86c4..46fa5b408 100644 --- a/plugins/decl_mode/decl_proof_instr.ml +++ b/plugins/decl_mode/decl_proof_instr.ml @@ -445,7 +445,7 @@ let concl_refiner metas body gls = let bsort,_B,nbody = aux nenv (_x::avoid) ((n,mkVar _x)::subst) rest in let body = mkNamedLambda _x _A nbody in - if occur_term (mkVar _x) _B then + if local_occur_var evd _x (EConstr.of_constr _B) then begin let _P = mkNamedLambda _x _A _B in match bsort,sort with @@ -672,14 +672,14 @@ let rec metas_from n hyps = _ :: q -> n :: metas_from (succ n) q | [] -> [] -let rec build_product args body = +let rec build_product sigma args body = match args with (Hprop st| Hvar st )::rest -> - let pprod= lift 1 (build_product rest body) in + let pprod= lift 1 (build_product sigma rest body) in let lbody = match st.st_label with Anonymous -> pprod - | Name id -> subst_term (mkVar id) pprod in + | Name id -> subst_var id pprod in mkProd (st.st_label, st.st_it, lbody) | [] -> body @@ -694,7 +694,7 @@ let instr_suffices _then cut gls0 = let info = get_its_info gls0 in let c_id = pf_get_new_id (Id.of_string "_cofact") gls0 in let ctx,hd = cut.cut_stat in - let c_stat = build_product ctx (mk_stat_or_thesis info gls0 hd) in + let c_stat = build_product (project gls0) ctx (mk_stat_or_thesis info gls0 hd) in let metas = metas_from 1 ctx in let c_ctx,c_head = build_applist c_stat metas in let c_term = applist (mkVar c_id,List.map mkMeta metas) in @@ -780,7 +780,7 @@ let rec consider_match may_intro introduced available expected gls = gls let consider_tac c hyps gls = - match kind_of_term (strip_outer_cast c) with + match kind_of_term (strip_outer_cast (project gls) (EConstr.of_constr c)) with Var id -> consider_match false [] [id] hyps gls | _ -> @@ -805,18 +805,18 @@ let rec take_tac wits gls = (* tactics for define *) -let rec build_function args body = +let rec build_function sigma args body = match args with st::rest -> - let pfun= lift 1 (build_function rest body) in + let pfun= lift 1 (build_function sigma rest body) in let id = match st.st_label with Anonymous -> assert false | Name id -> id in - mkLambda (Name id, st.st_it, subst_term (mkVar id) pfun) + mkLambda (Name id, st.st_it, subst_term sigma (EConstr.mkVar id) (EConstr.of_constr pfun)) | [] -> body let define_tac id args body gls = - let t = build_function args body in + let t = build_function (project gls) args body in Proofview.V82.of_tactic (letin_tac None (Name id) t None Locusops.nowhere) gls (* tactics for reconsider *) @@ -880,7 +880,7 @@ let build_per_info etype casee gls = let concl=pf_concl gls in let env=pf_env gls in let ctyp=pf_unsafe_type_of gls casee in - let is_dep = dependent casee concl in + let is_dep = dependent (project gls) (EConstr.of_constr casee) (EConstr.of_constr concl) in let hd,args = decompose_app (special_whd gls ctyp) in let (ind,u) = try @@ -895,9 +895,9 @@ let build_per_info etype casee gls = let params,real_args = List.chop nparams args in let abstract_obj c body = let typ=pf_unsafe_type_of gls c in - lambda_create env (typ,subst_term c body) in + lambda_create env (typ,subst_term (project gls) (EConstr.of_constr c) (EConstr.of_constr body)) in let pred= List.fold_right abstract_obj - real_args (lambda_create env (ctyp,subst_term casee concl)) in + real_args (lambda_create env (ctyp,subst_term (project gls) (EConstr.of_constr casee) (EConstr.of_constr concl))) in is_dep, {per_casee=casee; per_ctype=ctyp; @@ -953,7 +953,7 @@ let suppose_tac hyps gls0 = let info = get_its_info gls0 in let thesis = pf_concl gls0 in let id = pf_get_new_id (Id.of_string "subcase_") gls0 in - let clause = build_product hyps thesis in + let clause = build_product (project gls0) hyps thesis in let ninfo1 = {pm_stack=Suppose_case::info.pm_stack} in let old_clauses,stack = register_nodep_subcase id info.pm_stack in let ninfo2 = {pm_stack=stack} in @@ -1263,9 +1263,9 @@ let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls = let params,real_args = List.chop nparams all_args in let abstract_obj c body = let typ=pf_unsafe_type_of gls c in - lambda_create env (typ,subst_term c body) in + lambda_create env (typ,subst_term (project gls) (EConstr.of_constr c) (EConstr.of_constr body)) in let elim_pred = List.fold_right abstract_obj - real_args (lambda_create env (ctyp,subst_term casee concl)) in + real_args (lambda_create env (ctyp,subst_term (project gls) (EConstr.of_constr casee) (EConstr.of_constr concl))) in let case_info = Inductiveops.make_case_info env ind RegularStyle in let gen_arities = Inductive.arities_of_constructors (ind,u) spec in let f_ids typ = diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index a980a43f5..85cacecdb 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -42,11 +42,11 @@ let none = Evd.empty let type_of env c = let polyprop = (lang() == Haskell) in - Retyping.get_type_of ~polyprop env none (strip_outer_cast c) + Retyping.get_type_of ~polyprop env none (strip_outer_cast none (EConstr.of_constr c)) let sort_of env c = let polyprop = (lang() == Haskell) in - Retyping.get_sort_family_of ~polyprop env none (strip_outer_cast c) + Retyping.get_sort_family_of ~polyprop env none (strip_outer_cast none (EConstr.of_constr c)) (*S Generation of flags and signatures. *) @@ -887,7 +887,7 @@ let extract_std_constant env kn body typ = break user's clever let-ins and partial applications). *) let rels, c = let n = List.length s - and m = nb_lam body in + and m = nb_lam Evd.empty (EConstr.of_constr body) (** FIXME *) in if n <= m then decompose_lam_n n body else let s,s' = List.chop m s in diff --git a/plugins/firstorder/formula.ml b/plugins/firstorder/formula.ml index b34a36492..79f185d18 100644 --- a/plugins/firstorder/formula.ml +++ b/plugins/firstorder/formula.ml @@ -79,13 +79,13 @@ type kind_of_formula= let kind_of_formula gl term = let normalize=special_nf gl in let cciterm=special_whd gl term in - match match_with_imp_term cciterm with - Some (a,b)-> Arrow(a,(pop b)) + match match_with_imp_term (project gl) cciterm with + Some (a,b)-> Arrow(a,(pop (EConstr.of_constr b))) |_-> - match match_with_forall_term cciterm with + match match_with_forall_term (project gl) cciterm with Some (_,a,b)-> Forall(a,b) |_-> - match match_with_nodep_ind cciterm with + match match_with_nodep_ind (project gl) cciterm with Some (i,l,n)-> let ind,u=destInd i in let (mib,mip) = Global.lookup_inductive ind in @@ -96,7 +96,7 @@ let kind_of_formula gl term = let has_realargs=(n>0) in let is_trivial= let is_constant c = - Int.equal (nb_prod c) mib.mind_nparams in + Int.equal (nb_prod (project gl) (EConstr.of_constr c)) mib.mind_nparams in Array.exists is_constant mip.mind_nf_lc in if Inductiveops.mis_is_recursive (ind,mib,mip) || (has_realargs && not is_trivial) @@ -108,7 +108,7 @@ let kind_of_formula gl term = else Or((ind,u),l,is_trivial) | _ -> - match match_with_sigma_type cciterm with + match match_with_sigma_type (project gl) cciterm with Some (i,l)-> Exists((destInd i),l) |_-> Atom (normalize cciterm) diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml index 7ffc78928..1d107e9af 100644 --- a/plugins/firstorder/rules.ml +++ b/plugins/firstorder/rules.ml @@ -38,8 +38,8 @@ let wrap n b continue seq gls= []->anomaly (Pp.str "Not the expected number of hyps") | nd::q-> let id = NamedDecl.get_id nd in - if occur_var env id (pf_concl gls) || - List.exists (occur_var_in_decl env id) ctx then + if occur_var env (project gls) id (EConstr.of_constr (pf_concl gls)) || + List.exists (occur_var_in_decl env (project gls) id) ctx then (aux (i-1) q (nd::ctx)) else add_formula Hyp (VarRef id) (NamedDecl.get_type nd) (aux (i-1) q (nd::ctx)) gls in diff --git a/plugins/firstorder/unify.ml b/plugins/firstorder/unify.ml index d9ab36ad6..01c019744 100644 --- a/plugins/firstorder/unify.ml +++ b/plugins/firstorder/unify.ml @@ -21,7 +21,10 @@ exception UFAIL of constr*constr to the equation set. Raises UFAIL with a pair of terms *) +let strip_outer_cast t = strip_outer_cast Evd.empty (EConstr.of_constr t) (** FIXME *) + let unif t1 t2= + let evd = Evd.empty in (** FIXME *) let bige=Queue.create () and sigma=ref [] in let bind i t= @@ -47,18 +50,18 @@ let unif t1 t2= else bind i nt2 | Meta i,_ -> let t=subst_meta !sigma nt2 in - if Int.Set.is_empty (free_rels t) && - not (occur_term (mkMeta i) t) then + if Int.Set.is_empty (free_rels evd (EConstr.of_constr t)) && + not (occur_term evd (EConstr.mkMeta i) (EConstr.of_constr t)) then bind i t else raise (UFAIL(nt1,nt2)) | _,Meta i -> let t=subst_meta !sigma nt1 in - if Int.Set.is_empty (free_rels t) && - not (occur_term (mkMeta i) t) then + if Int.Set.is_empty (free_rels evd (EConstr.of_constr t)) && + not (occur_term evd (EConstr.mkMeta i) (EConstr.of_constr t)) then bind i t else raise (UFAIL(nt1,nt2)) | Cast(_,_,_),_->Queue.add (strip_outer_cast nt1,nt2) bige | _,Cast(_,_,_)->Queue.add (nt1,strip_outer_cast nt2) bige | (Prod(_,a,b),Prod(_,c,d))|(Lambda(_,a,b),Lambda(_,c,d))-> - Queue.add (a,c) bige;Queue.add (pop b,pop d) bige + Queue.add (a,c) bige;Queue.add (pop (EConstr.of_constr b),pop (EConstr.of_constr d)) bige | Case (_,pa,ca,va),Case (_,pb,cb,vb)-> Queue.add (pa,pb) bige; Queue.add (ca,cb) bige; diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml index 8e193c753..a14ec8a2c 100644 --- a/plugins/fourier/fourierR.ml +++ b/plugins/fourier/fourierR.ml @@ -461,8 +461,9 @@ exception GoalDone let rec fourier () = Proofview.Goal.nf_enter { enter = begin fun gl -> let concl = Proofview.Goal.concl gl in + let sigma = Tacmach.New.project gl in Coqlib.check_required_library ["Coq";"fourier";"Fourier"]; - let goal = Termops.strip_outer_cast concl in + let goal = Termops.strip_outer_cast sigma (EConstr.of_constr concl) in let fhyp=Id.of_string "new_hyp_for_fourier" in (* si le but est une inéquation, on introduit son contraire, et le but à prouver devient False *) diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 527f4f0b1..f6567ab81 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -287,7 +287,7 @@ let change_eq env sigma hyp_id (context:Context.Rel.t) x t end_of_type = in let sub = compute_substitution Int.Map.empty (snd t1) (snd t2) in let sub = compute_substitution sub (fst t1) (fst t2) in - let end_of_type_with_pop = Termops.pop end_of_type in (*the equation will be removed *) + let end_of_type_with_pop = Termops.pop (EConstr.of_constr end_of_type) in (*the equation will be removed *) let new_end_of_type = (* Ugly hack to prevent Map.fold order change between ocaml-3.08.3 and ocaml-3.08.4 Can be safely replaced by the next comment for Ocaml >= 3.08.4 @@ -309,7 +309,7 @@ let change_eq env sigma hyp_id (context:Context.Rel.t) x t end_of_type = try let witness = Int.Map.find i sub in if is_local_def decl then anomaly (Pp.str "can not redefine a rel!"); - (Termops.pop end_of_type,ctxt_size,mkLetIn (RelDecl.get_name decl, witness, RelDecl.get_type decl, witness_fun)) + (Termops.pop (EConstr.of_constr end_of_type),ctxt_size,mkLetIn (RelDecl.get_name decl, witness, RelDecl.get_type decl, witness_fun)) with Not_found -> (mkProd_or_LetIn decl end_of_type, ctxt_size + 1, mkLambda_or_LetIn decl witness_fun) ) @@ -430,7 +430,7 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma = begin let pte,pte_args = (destApp t_x) in let (* fix_info *) prove_rec_hyp = (Id.Map.find (destVar pte) ptes_infos).proving_tac in - let popped_t' = Termops.pop t' in + let popped_t' = Termops.pop (EConstr.of_constr t') in let real_type_of_hyp = it_mkProd_or_LetIn popped_t' context in let prove_new_type_of_hyp = let context_length = List.length context in @@ -480,7 +480,7 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma = (* observe (str "In "++Ppconstr.pr_id hyp_id++ *) (* str " removing useless precond True" *) (* ); *) - let popped_t' = Termops.pop t' in + let popped_t' = Termops.pop (EConstr.of_constr t') in let real_type_of_hyp = it_mkProd_or_LetIn popped_t' context in @@ -508,7 +508,7 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma = ] else if is_trivial_eq t_x then (* t_x := t = t => we remove this precond *) - let popped_t' = Termops.pop t' in + let popped_t' = Termops.pop (EConstr.of_constr t') in let real_type_of_hyp = it_mkProd_or_LetIn popped_t' context in @@ -608,7 +608,7 @@ let treat_new_case ptes_infos nb_prod continue_tac term dyn_infos = let fun_body = mkLambda(Anonymous, pf_unsafe_type_of g' term, - Termops.replace_term term (mkRel 1) dyn_infos.info + Termops.replace_term (project g') (EConstr.of_constr term) (EConstr.mkRel 1) (EConstr.of_constr dyn_infos.info) ) in let new_body = pf_nf_betaiota g' (mkApp(fun_body,[| new_term_value |])) in @@ -699,7 +699,7 @@ let build_proof let t = dyn_info'.info in let dyn_infos = {dyn_info' with info = mkCase(ci,ct,t,cb)} in - let g_nb_prod = nb_prod (pf_concl g) in + let g_nb_prod = nb_prod (project g) (EConstr.of_constr (pf_concl g)) in let type_of_term = pf_unsafe_type_of g t in let term_eq = make_refl_eq (Lazy.force refl_equal) type_of_term t @@ -712,7 +712,7 @@ let build_proof (fun g -> observe_tac "toto" ( tclTHENSEQ [Proofview.V82.of_tactic (Simple.case t); (fun g' -> - let g'_nb_prod = nb_prod (pf_concl g') in + let g'_nb_prod = nb_prod (project g') (EConstr.of_constr (pf_concl g')) in let nb_instanciate_partial = g'_nb_prod - g_nb_prod in observe_tac "treat_new_case" (treat_new_case @@ -927,8 +927,8 @@ let generalize_non_dep hyp g = Environ.fold_named_context_reverse (fun (clear,keep) decl -> let hyp = get_id decl in if Id.List.mem hyp hyps - || List.exists (Termops.occur_var_in_decl env hyp) keep - || Termops.occur_var env hyp hyp_typ + || List.exists (Termops.occur_var_in_decl env (project g) hyp) keep + || Termops.occur_var env (project g) hyp (EConstr.of_constr hyp_typ) || Termops.is_section_variable hyp (* should be dangerous *) then (clear,decl::keep) else (hyp::clear,keep)) @@ -1042,7 +1042,7 @@ let do_replace (evd:Evd.evar_map ref) params rec_arg_num rev_args_id f fun_num a let _ = Typing.e_type_of ~refresh:true (Global.env ()) evd res in res in - let nb_intro_to_do = nb_prod (pf_concl g) in + let nb_intro_to_do = nb_prod (project g) (EConstr.of_constr (pf_concl g)) in tclTHEN (tclDO nb_intro_to_do (Proofview.V82.of_tactic intro)) ( diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index cc699e5d3..032d887de 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -110,7 +110,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = in let dummy_var = mkVar (Id.of_string "________") in let mk_replacement c i args = - let res = mkApp(rel_to_fun.(i), Array.map Termops.pop (array_get_start args)) in + let res = mkApp(rel_to_fun.(i), Array.map (fun c -> Termops.pop (EConstr.of_constr c)) (array_get_start args)) in observe (str "replacing " ++ pr_lconstr c ++ str " by " ++ pr_lconstr res); res in @@ -168,25 +168,25 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = let new_env = Environ.push_rel (LocalAssum (x,t)) env in let new_b,binders_to_remove_from_b = compute_new_princ_type remove new_env b in if List.exists (eq_constr (mkRel 1)) binders_to_remove_from_b - then (Termops.pop new_b), filter_map (eq_constr (mkRel 1)) Termops.pop binders_to_remove_from_b + then (Termops.pop (EConstr.of_constr new_b)), filter_map (eq_constr (mkRel 1)) (fun c -> Termops.pop (EConstr.of_constr c)) binders_to_remove_from_b else ( bind_fun(new_x,new_t,new_b), list_union_eq eq_constr binders_to_remove_from_t - (List.map Termops.pop binders_to_remove_from_b) + (List.map (fun c -> Termops.pop (EConstr.of_constr c)) binders_to_remove_from_b) ) with | Toberemoved -> (* observe (str "Decl of "++Ppconstr.pr_name x ++ str " is removed "); *) let new_b,binders_to_remove_from_b = compute_new_princ_type remove env (substnl [dummy_var] 1 b) in - new_b, List.map Termops.pop binders_to_remove_from_b + new_b, List.map (fun c -> Termops.pop (EConstr.of_constr c)) binders_to_remove_from_b | Toberemoved_with_rel (n,c) -> (* observe (str "Decl of "++Ppconstr.pr_name x ++ str " is removed "); *) let new_b,binders_to_remove_from_b = compute_new_princ_type remove env (substnl [c] n b) in - new_b, list_add_set_eq eq_constr (mkRel n) (List.map Termops.pop binders_to_remove_from_b) + new_b, list_add_set_eq eq_constr (mkRel n) (List.map (fun c -> Termops.pop (EConstr.of_constr c)) binders_to_remove_from_b) end and compute_new_princ_type_for_letin remove env x v t b = begin @@ -197,25 +197,25 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = let new_env = Environ.push_rel (LocalDef (x,v,t)) env in let new_b,binders_to_remove_from_b = compute_new_princ_type remove new_env b in if List.exists (eq_constr (mkRel 1)) binders_to_remove_from_b - then (Termops.pop new_b),filter_map (eq_constr (mkRel 1)) Termops.pop binders_to_remove_from_b + then (Termops.pop (EConstr.of_constr new_b)),filter_map (eq_constr (mkRel 1)) (fun c -> Termops.pop (EConstr.of_constr c)) binders_to_remove_from_b else ( mkLetIn(new_x,new_v,new_t,new_b), list_union_eq eq_constr (list_union_eq eq_constr binders_to_remove_from_t binders_to_remove_from_v) - (List.map Termops.pop binders_to_remove_from_b) + (List.map (fun c -> Termops.pop (EConstr.of_constr c)) binders_to_remove_from_b) ) with | Toberemoved -> (* observe (str "Decl of "++Ppconstr.pr_name x ++ str " is removed "); *) let new_b,binders_to_remove_from_b = compute_new_princ_type remove env (substnl [dummy_var] 1 b) in - new_b, List.map Termops.pop binders_to_remove_from_b + new_b, List.map (fun c -> Termops.pop (EConstr.of_constr c)) binders_to_remove_from_b | Toberemoved_with_rel (n,c) -> (* observe (str "Decl of "++Ppconstr.pr_name x ++ str " is removed "); *) let new_b,binders_to_remove_from_b = compute_new_princ_type remove env (substnl [c] n b) in - new_b, list_add_set_eq eq_constr (mkRel n) (List.map Termops.pop binders_to_remove_from_b) + new_b, list_add_set_eq eq_constr (mkRel n) (List.map (fun c -> Termops.pop (EConstr.of_constr c)) binders_to_remove_from_b) end and compute_new_princ_type_with_acc remove env e (c_acc,to_remove_acc) = let new_e,to_remove_from_e = compute_new_princ_type remove env e diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 99b04898b..a264c37c5 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -14,20 +14,21 @@ open Sigma.Notations module RelDecl = Context.Rel.Declaration -let is_rec_info scheme_info = +let is_rec_info sigma scheme_info = let test_branche min acc decl = acc || ( let new_branche = it_mkProd_or_LetIn mkProp (fst (decompose_prod_assum (RelDecl.get_type decl))) in - let free_rels_in_br = Termops.free_rels new_branche in + let free_rels_in_br = Termops.free_rels sigma (EConstr.of_constr new_branche) in let max = min + scheme_info.Tactics.npredicates in Int.Set.exists (fun i -> i >= min && i< max) free_rels_in_br ) in List.fold_left_i test_branche 1 false (List.rev scheme_info.Tactics.branches) -let choose_dest_or_ind scheme_info = - Tactics.induction_destruct (is_rec_info scheme_info) false +let choose_dest_or_ind scheme_info args = + Proofview.tclBIND Proofview.tclEVARMAP (fun sigma -> + Tactics.induction_destruct (is_rec_info sigma scheme_info) false args) let functional_induction with_clean c princl pat = let res = diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index c8b4e4833..cf42a809d 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -254,7 +254,7 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes let princ_type = nf_zeta princ_type in let princ_infos = Tactics.compute_elim_sig princ_type in (* The number of args of the function is then easily computable *) - let nb_fun_args = nb_prod (pf_concl g) - 2 in + let nb_fun_args = nb_prod (project g) (EConstr.of_constr (pf_concl g)) - 2 in let args_names = generate_fresh_id (Id.of_string "x") [] nb_fun_args in let ids = args_names@(pf_ids_of_hyps g) in (* Since we cannot ensure that the functional principle is defined in the @@ -467,7 +467,7 @@ let generalize_dependent_of x hyp g = tclMAP (function | LocalAssum (id,t) when not (Id.equal id hyp) && - (Termops.occur_var (pf_env g) x t) -> tclTHEN (Proofview.V82.of_tactic (Tactics.generalize [mkVar id])) (thin [id]) + (Termops.occur_var (pf_env g) (project g) x (EConstr.of_constr t)) -> tclTHEN (Proofview.V82.of_tactic (Tactics.generalize [mkVar id])) (thin [id]) | _ -> tclIDTAC ) (pf_hyps g) @@ -666,7 +666,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic = (* Then we get the number of argument of the function and compute a fresh name for each of them *) - let nb_fun_args = nb_prod (pf_concl g) - 2 in + let nb_fun_args = nb_prod (project g) (EConstr.of_constr (pf_concl g)) - 2 in let args_names = generate_fresh_id (Id.of_string "x") [] nb_fun_args in let ids = args_names@(pf_ids_of_hyps g) in (* and fresh names for res H and the principle (cf bug bug #1174) *) @@ -684,7 +684,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic = (fun decl -> List.map (fun id -> id) - (generate_fresh_id (Id.of_string "y") ids (nb_prod (RelDecl.get_type decl))) + (generate_fresh_id (Id.of_string "y") ids (nb_prod (project g) (EConstr.of_constr (RelDecl.get_type decl)))) ) branches in diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml index 19c2ed417..865042afb 100644 --- a/plugins/funind/merge.ml +++ b/plugins/funind/merge.ml @@ -32,7 +32,7 @@ module RelDecl = Context.Rel.Declaration (** {2 Useful operations on constr and glob_constr} *) -let rec popn i c = if i<=0 then c else pop (popn (i-1) c) +let rec popn i c = if i<=0 then c else pop (EConstr.of_constr (popn (i-1) c)) (** Substitutions in constr *) let compare_constr_nosub t1 t2 = @@ -985,7 +985,7 @@ let relprinctype_to_funprinctype relprinctype nfuns = (* first remove indarg and indarg_in_concl *) let relinfo_noindarg = { relinfo with indarg_in_concl = false; indarg = None; - concl = remove_last_arg (pop relinfo.concl); } in + concl = remove_last_arg (pop (EConstr.of_constr relinfo.concl)); } in (* the nfuns last induction arguments are functional ones: remove them *) let relinfo_argsok = { relinfo_noindarg with nargs = relinfo_noindarg.nargs - nfuns; diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 54066edfb..6b63d7771 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -407,7 +407,7 @@ let treat_case forbid_new_ids to_intros finalize_tac nb_lam e infos : tactic = let _,args = try destApp ty_teq with DestKO -> assert false in args.(1),args.(2) in - let new_b' = Termops.replace_term teq_lhs teq_rhs new_b in + let new_b' = Termops.replace_term (project g') (EConstr.of_constr teq_lhs) (EConstr.of_constr teq_rhs) (EConstr.of_constr new_b) in let new_infos = { infos with info = new_b'; @@ -681,7 +681,7 @@ let mkDestructEq : (fun decl -> let open Context.Named.Declaration in let id = get_id decl in - if Id.List.mem id not_on_hyp || not (Termops.occur_term expr (get_type decl)) + if Id.List.mem id not_on_hyp || not (Termops.occur_term (project g) (EConstr.of_constr expr) (EConstr.of_constr (get_type decl))) then None else Some id) hyps in let to_revert_constr = List.rev_map mkVar to_revert in let type_of_expr = pf_unsafe_type_of g expr in @@ -1251,7 +1251,7 @@ let clear_goals = | Prod(Name id as na,t',b) -> let b' = clear_goal b in if noccurn 1 b' && (is_rec_res id) - then Termops.pop b' + then Termops.pop (EConstr.of_constr b') else if b' == b then t else mkProd(na,t',b') | _ -> Term.map_constr clear_goal t @@ -1285,7 +1285,7 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp anomaly (Pp.str "open_new_goal with an unamed theorem") in let na = next_global_ident_away name [] in - if Termops.occur_existential gls_type then + if Termops.occur_existential sigma (EConstr.of_constr gls_type) then CErrors.error "\"abstract\" cannot handle existentials"; let hook _ _ = let opacity = @@ -1422,7 +1422,7 @@ let start_equation (f:global_reference) (term_f:global_reference) (cont_tactic:Id.t list -> tactic) g = let ids = pf_ids_of_hyps g in let terminate_constr = constr_of_global term_f in - let nargs = nb_prod (fst (type_of_const terminate_constr)) (*FIXME*) in + let nargs = nb_prod (project g) (EConstr.of_constr (fst (type_of_const terminate_constr))) (*FIXME*) in let x = n_x_id ids nargs in observe_tac (str "start_equation") (observe_tclTHENLIST (str "start_equation") [ h_intros x; @@ -1552,7 +1552,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num and functional_ref = destConst (constr_of_global functional_ref) and eq_ref = destConst (constr_of_global eq_ref) in generate_induction_principle f_ref tcc_lemma_constr - functional_ref eq_ref rec_arg_num rec_arg_type (nb_prod res) relation; + functional_ref eq_ref rec_arg_num rec_arg_type (nb_prod evm (EConstr.of_constr res)) relation; if Flags.is_verbose () then msgnl (h 1 (Ppconstr.pr_id function_name ++ spc () ++ str"is defined" )++ fnl () ++ diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index a063cbbfe..49fcf83b4 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -1221,7 +1221,7 @@ struct let g,env,tg = xparse_formula env tg b in mkformula_binary mkIff term f g,env,tg | _ -> parse_atom env tg term) - | Prod(typ,a,b) when not (Termops.dependent (mkRel 1) b)-> + | Prod(typ,a,b) when EConstr.Vars.noccurn Evd.empty 1 (EConstr.of_constr b) (** FIXME *) -> let f,env,tg = xparse_formula env tg a in let g,env,tg = xparse_formula env tg b in mkformula_binary mkI term f g,env,tg @@ -1687,7 +1687,8 @@ let rec mk_topo_order le l = | (Some v,l') -> v :: (mk_topo_order le l') -let topo_sort_constr l = mk_topo_order Termops.dependent l +let topo_sort_constr l = + mk_topo_order (fun c t -> Termops.dependent Evd.empty (** FIXME *) (EConstr.of_constr c) (EConstr.of_constr t)) l (** diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml index 6405c8ceb..c6376727a 100644 --- a/plugins/quote/quote.ml +++ b/plugins/quote/quote.ml @@ -183,7 +183,7 @@ type inversion_scheme = { let i_can't_do_that () = error "Quote: not a simple fixpoint" -let decomp_term c = kind_of_term (Termops.strip_outer_cast c) +let decomp_term gl c = kind_of_term (Termops.strip_outer_cast (Tacmach.New.project gl) (EConstr.of_constr c)) (*s [compute_lhs typ i nargsi] builds the term \texttt{(C ?nargsi ... ?2 ?1)}, where \texttt{C} is the [i]-th constructor of inductive @@ -223,14 +223,14 @@ let compute_rhs bodyi index_of_f = let compute_ivs f cs gl = let cst = try destConst f with DestKO -> i_can't_do_that () in let body = Environ.constant_value_in (Global.env()) cst in - match decomp_term body with + match decomp_term gl body with | Fix(([| len |], 0), ([| name |], [| typ |], [| body2 |])) -> let (args3, body3) = decompose_lam body2 in let nargs3 = List.length args3 in let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in let is_conv = Reductionops.is_conv env sigma in - begin match decomp_term body3 with + begin match decomp_term gl body3 with | Case(_,p,c,lci) -> (* <p> Case c of c1 ... cn end *) let n_lhs_rhs = ref [] and v_lhs = ref (None : constr option) @@ -267,7 +267,7 @@ let compute_ivs f cs gl = (* The Cases predicate is a lambda; we assume no dependency *) let p = match kind_of_term p with - | Lambda (_,_,p) -> Termops.pop p + | Lambda (_,_,p) -> Termops.pop (EConstr.of_constr p) | _ -> p in diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml index 367a13333..b129b0bb3 100644 --- a/plugins/rtauto/refl_tauto.ml +++ b/plugins/rtauto/refl_tauto.ml @@ -94,7 +94,7 @@ let rec make_form atom_env gls term = let cciterm=special_whd gls term in match kind_of_term cciterm with Prod(_,a,b) -> - if not (Termops.dependent (mkRel 1) b) && + if EConstr.Vars.noccurn Evd.empty (** FIXME *) 1 (EConstr.of_constr b) && Retyping.get_sort_family_of (pf_env gls) (Tacmach.project gls) a == InProp then @@ -134,7 +134,7 @@ let rec make_hyps atom_env gls lenv = function | LocalAssum (id,typ)::rest -> let hrec= make_hyps atom_env gls (typ::lenv) rest in - if List.exists (Termops.dependent (mkVar id)) lenv || + if List.exists (fun c -> Termops.local_occur_var Evd.empty (** FIXME *) id (EConstr.of_constr c)) lenv || (Retyping.get_sort_family_of (pf_env gls) (Tacmach.project gls) typ != InProp) then diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4 index 77e25b2a5..86cc928c8 100644 --- a/plugins/ssrmatching/ssrmatching.ml4 +++ b/plugins/ssrmatching/ssrmatching.ml4 @@ -702,7 +702,7 @@ let match_upats_HO ~on_instance upats env sigma0 ise c = let fixed_upat = function | {up_k = KpatFlex | KpatEvar _ | KpatProj _} -> false -| {up_t = t} -> not (occur_existential t) +| {up_t = t} -> not (occur_existential Evd.empty (EConstr.of_constr t)) (** FIXME *) let do_once r f = match !r with Some _ -> () | None -> r := Some (f ()) diff --git a/pretyping/cases.ml b/pretyping/cases.ml index d5b125135..6b480986c 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -535,19 +535,19 @@ let dependencies_in_pure_rhs nargs eqns = let deps_columns = matrix_transpose deps_rows in List.map (List.exists (fun x -> x)) deps_columns -let dependent_decl a = +let dependent_decl sigma a = function - | LocalAssum (na,t) -> dependent a t - | LocalDef (na,c,t) -> dependent a t || dependent a c + | LocalAssum (na,t) -> dependent sigma (EConstr.of_constr a) (EConstr.of_constr t) + | LocalDef (na,c,t) -> dependent sigma (EConstr.of_constr a) (EConstr.of_constr t) || dependent sigma (EConstr.of_constr a) (EConstr.of_constr c) -let rec dep_in_tomatch n = function - | (Pushed _ | Alias _ | NonDepAlias) :: l -> dep_in_tomatch n l - | Abstract (_,d) :: l -> dependent_decl (mkRel n) d || dep_in_tomatch (n+1) l +let rec dep_in_tomatch sigma n = function + | (Pushed _ | Alias _ | NonDepAlias) :: l -> dep_in_tomatch sigma n l + | Abstract (_,d) :: l -> dependent_decl sigma (mkRel n) d || dep_in_tomatch sigma (n+1) l | [] -> false -let dependencies_in_rhs nargs current tms eqns = +let dependencies_in_rhs sigma nargs current tms eqns = match kind_of_term current with - | Rel n when dep_in_tomatch n tms -> List.make nargs true + | Rel n when dep_in_tomatch sigma n tms -> List.make nargs true | _ -> dependencies_in_pure_rhs nargs eqns (* Computing the matrix of dependencies *) @@ -562,24 +562,24 @@ let dependencies_in_rhs nargs current tms eqns = [n-2;1], [1] points to [dn] and [n-2] to [d3] *) -let rec find_dependency_list tmblock = function +let rec find_dependency_list sigma tmblock = function | [] -> [] | (used,tdeps,d)::rest -> - let deps = find_dependency_list tmblock rest in - if used && List.exists (fun x -> dependent_decl x d) tmblock + let deps = find_dependency_list sigma tmblock rest in + if used && List.exists (fun x -> dependent_decl sigma x d) tmblock then List.add_set Int.equal (List.length rest + 1) (List.union Int.equal deps tdeps) else deps -let find_dependencies is_dep_or_cstr_in_rhs (tm,(_,tmtypleaves),d) nextlist = - let deps = find_dependency_list (tm::tmtypleaves) nextlist in +let find_dependencies sigma is_dep_or_cstr_in_rhs (tm,(_,tmtypleaves),d) nextlist = + let deps = find_dependency_list sigma (tm::tmtypleaves) nextlist in if is_dep_or_cstr_in_rhs || not (List.is_empty deps) then ((true ,deps,d)::nextlist) else ((false,[] ,d)::nextlist) -let find_dependencies_signature deps_in_rhs typs = - let l = List.fold_right2 find_dependencies deps_in_rhs typs [] in +let find_dependencies_signature sigma deps_in_rhs typs = + let l = List.fold_right2 (find_dependencies sigma) deps_in_rhs typs [] in List.map (fun (_,deps,_) -> deps) l (* Assume we had terms t1..tq to match in a context xp:Tp,...,x1:T1 |- @@ -1095,30 +1095,30 @@ let rec ungeneralize n ng body = let ungeneralize_branch n k (sign,body) cs = (sign,ungeneralize (n+cs.cs_nargs) k body) -let rec is_dependent_generalization ng body = +let rec is_dependent_generalization sigma ng body = match kind_of_term body with | Lambda (_,_,c) when Int.equal ng 0 -> - dependent (mkRel 1) c + not (EConstr.Vars.noccurn sigma 1 (EConstr.of_constr c)) | Lambda (na,t,c) -> (* We traverse an inner generalization *) - is_dependent_generalization (ng-1) c + is_dependent_generalization sigma (ng-1) c | LetIn (na,b,t,c) -> (* We traverse an alias *) - is_dependent_generalization ng c + is_dependent_generalization sigma ng c | Case (ci,p,c,brs) -> (* We traverse a split *) Array.exists2 (fun q c -> let _,b = decompose_lam_n_decls q c in - is_dependent_generalization ng b) + is_dependent_generalization sigma ng b) ci.ci_cstr_ndecls brs | App (g,args) -> (* We traverse an inner generalization *) assert (isCase g); - is_dependent_generalization (ng+Array.length args) g + is_dependent_generalization sigma (ng+Array.length args) g | _ -> assert false -let is_dependent_branch k (_,br) = - is_dependent_generalization k br +let is_dependent_branch sigma k (_,br) = + is_dependent_generalization sigma k br let postprocess_dependencies evd tocheck brs tomatch pred deps cs = let rec aux k brs tomatch pred tocheck deps = match deps, tomatch with @@ -1126,8 +1126,8 @@ let postprocess_dependencies evd tocheck brs tomatch pred deps cs = | n::deps, Abstract (i,d) :: tomatch -> let d = map_constr (nf_evar evd) d in let is_d = match d with LocalAssum _ -> false | LocalDef _ -> true in - if is_d || List.exists (fun c -> dependent_decl (lift k c) d) tocheck - && Array.exists (is_dependent_branch k) brs then + if is_d || List.exists (fun c -> dependent_decl evd (lift k c) d) tocheck + && Array.exists (is_dependent_branch evd k) brs then (* Dependency in the current term to match and its dependencies is real *) let brs,tomatch,pred,inst = aux (k+1) brs tomatch pred (mkRel n::tocheck) deps in let inst = match d with @@ -1249,8 +1249,8 @@ let build_branch initial current realargs deps (realnames,curname) pb arsign eqn (* We compute over which of x(i+1)..xn and x matching on xi will need a *) (* generalization *) let dep_sign = - find_dependencies_signature - (dependencies_in_rhs const_info.cs_nargs current pb.tomatch eqns) + find_dependencies_signature !(pb.evdref) + (dependencies_in_rhs !(pb.evdref) const_info.cs_nargs current pb.tomatch eqns) (List.rev typs') in (* The dependent term to subst in the types of the remaining UnPushed @@ -1452,7 +1452,7 @@ and compile_alias initial pb (na,orig,(expanded,expanded_typ)) rest = mat = List.map (push_alias_eqn alias) pb.mat } in let j = compile pb in { uj_val = - if isRel c || isVar c || count_occurrences (mkRel 1) j.uj_val <= 1 then + if isRel c || isVar c || count_occurrences !(pb.evdref) (EConstr.mkRel 1) (EConstr.of_constr j.uj_val) <= 1 then subst1 c j.uj_val else mkLetIn (na,c,t,j.uj_val); @@ -1561,7 +1561,7 @@ let matx_of_eqns env eqns = returning True never happens and any inhabited type can be put instead). *) -let adjust_to_extended_env_and_remove_deps env extenv subst t = +let adjust_to_extended_env_and_remove_deps env extenv sigma subst t = let n = Context.Rel.length (rel_context env) in let n' = Context.Rel.length (rel_context extenv) in (* We first remove the bindings that are dependently typed (they are @@ -1583,7 +1583,7 @@ let adjust_to_extended_env_and_remove_deps env extenv subst t = | LocalAssum _ -> p in let p = traverse_local_defs p in let u = lift (n' - n) u in - try Some (p, u, expand_vars_in_term extenv u) + try Some (p, u, expand_vars_in_term extenv sigma u) (* pedrot: does this really happen to raise [Failure _]? *) with Failure _ -> None in let subst0 = List.map_filter map subst in @@ -1617,7 +1617,7 @@ let abstract_tycon loc env evdref subst tycon extenv t = let src = match kind_of_term t with | Evar (evk,_) -> (loc,Evar_kinds.SubEvar evk) | _ -> (loc,Evar_kinds.CasesType true) in - let subst0,t0 = adjust_to_extended_env_and_remove_deps env extenv subst t in + let subst0,t0 = adjust_to_extended_env_and_remove_deps env extenv !evdref subst t in (* We traverse the type T of the original problem Xi looking for subterms that match the non-constructor part of the constraints (this part is in subst); these subterms are the "good" subterms and we replace them @@ -1644,7 +1644,8 @@ let abstract_tycon loc env evdref subst tycon extenv t = let good = List.filter (fun (_,u,_) -> is_conv_leq env !evdref t u) subst in match good with | [] -> - map_constr_with_full_binders push_binder aux x t + let self env c = EConstr.of_constr (aux env (EConstr.Unsafe.to_constr c)) in + EConstr.Unsafe.to_constr (map_constr_with_full_binders !evdref push_binder self x (EConstr.of_constr t)) | (_, _, u) :: _ -> (* u is in extenv *) let vl = List.map pi1 good in let ty = @@ -1652,16 +1653,16 @@ let abstract_tycon loc env evdref subst tycon extenv t = Evarutil.evd_comb1 (refresh_universes (Some false) env) evdref ty in let ty = lift (-k) (aux x ty) in - let depvl = free_rels ty in + let depvl = free_rels !evdref (EConstr.of_constr ty) in let inst = List.map_i (fun i _ -> if Int.List.mem i vl then u else mkRel i) 1 (rel_context extenv) in let rel_filter = - List.map (fun a -> not (isRel a) || dependent a u + List.map (fun a -> not (isRel a) || dependent !evdref (EConstr.of_constr a) (EConstr.of_constr u) || Int.Set.mem (destRel a) depvl) inst in let named_filter = - List.map (fun d -> dependent (mkVar (NamedDecl.get_id d)) u) + List.map (fun d -> local_occur_var !evdref (NamedDecl.get_id d) (EConstr.of_constr u)) (named_context extenv) in let filter = Filter.make (rel_filter @ named_filter) in let candidates = u :: List.map mkRel vl in @@ -1753,7 +1754,7 @@ let build_inversion_problem loc env sigma tms t = List.map (fun (c,d) -> (c,extract_inductive_data pb_env sigma d,d)) decls in let decls = List.rev decls in - let dep_sign = find_dependencies_signature (List.make n true) decls in + let dep_sign = find_dependencies_signature sigma (List.make n true) decls in let sub_tms = List.map2 (fun deps (tm, (tmtyp,_), decl) -> @@ -1878,7 +1879,7 @@ let prepare_predicate_from_arsign_tycon env sigma loc tomatchs arsign c = List.fold_right2 (fun (tm, tmtype) sign (subst, len) -> let signlen = List.length sign in match kind_of_term tm with - | Rel n when dependent tm c + | Rel n when dependent sigma (EConstr.of_constr tm) (EConstr.of_constr c) && Int.equal signlen 1 (* The term to match is not of a dependent type itself *) -> ((n, len) :: subst, len - signlen) | Rel n when signlen > 1 (* The term is of a dependent type, @@ -1890,13 +1891,13 @@ let prepare_predicate_from_arsign_tycon env sigma loc tomatchs arsign c = List.fold_left (fun (subst, len) arg -> match kind_of_term arg with - | Rel n when dependent arg c -> + | Rel n when dependent sigma (EConstr.of_constr arg) (EConstr.of_constr c) -> ((n, len) :: subst, pred len) | _ -> (subst, pred len)) (subst, len) realargs in let subst = - if dependent tm c && List.for_all isRel realargs + if dependent sigma (EConstr.of_constr tm) (EConstr.of_constr c) && List.for_all isRel realargs then (n, len) :: subst else subst in (subst, pred len)) | _ -> (subst, len - signlen)) @@ -2279,7 +2280,7 @@ let lift_ctx n ctx = in ctx' (* Turn matched terms into variables. *) -let abstract_tomatch env tomatchs tycon = +let abstract_tomatch env sigma tomatchs tycon = let prev, ctx, names, tycon = List.fold_left (fun (prev, ctx, names, tycon) (c, t) -> @@ -2288,7 +2289,7 @@ let abstract_tomatch env tomatchs tycon = Rel n -> (lift lenctx c, lift_tomatch_type lenctx t) :: prev, ctx, names, tycon | _ -> let tycon = Option.map - (fun t -> subst_term (lift 1 c) (lift 1 t)) tycon in + (fun t -> subst_term sigma (EConstr.of_constr (lift 1 c)) (EConstr.of_constr (lift 1 t))) tycon in let name = next_ident_away (Id.of_string "filtered_var") names in (mkRel 1, lift_tomatch_type (succ lenctx) t) :: lift_ctx 1 prev, LocalDef (Name name, lift lenctx c, lift lenctx $ type_of_tomatch t) :: ctx, @@ -2406,7 +2407,7 @@ let compile_program_cases loc style (typing_function, evdref) tycon env (* constructors found in patterns *) let tomatchs = coerce_to_indtype typing_function evdref env matx tomatchl in let tycon = valcon_of_tycon tycon in - let tomatchs, tomatchs_lets, tycon' = abstract_tomatch env tomatchs tycon in + let tomatchs, tomatchs_lets, tycon' = abstract_tomatch env !evdref tomatchs tycon in let env = push_rel_context tomatchs_lets env in let len = List.length eqns in let sign, allnames, signlen, eqs, neqs, args = @@ -2460,7 +2461,7 @@ let compile_program_cases loc style (typing_function, evdref) tycon env List.map (fun (c,d) -> (c,extract_inductive_data env !evdref d,d)) typs in let dep_sign = - find_dependencies_signature + find_dependencies_signature !evdref (List.make (List.length typs) true) typs in @@ -2535,7 +2536,7 @@ let compile_cases loc style (typing_fun, evdref) tycon env (predopt, tomatchl, e List.map (fun (c,d) -> (c,extract_inductive_data env sigma d,d)) typs in let dep_sign = - find_dependencies_signature + find_dependencies_signature !evdref (List.make (List.length typs) true) typs in diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index 2b860ae9c..a3970fc0f 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -487,7 +487,7 @@ let rec inh_conv_coerce_to_fail loc env evd rigidonly v t c1 = let v1 = Option.get v1 in let v2 = Option.map (fun v -> beta_applist (lift 1 v,[v1])) v in let t2 = match v2 with - | None -> subst_term v1 t2 + | None -> subst_term evd' (EConstr.of_constr v1) (EConstr.of_constr t2) | Some v2 -> Retyping.get_type_of env1 evd' v2 in let (evd'',v2') = inh_conv_coerce_to_fail loc env1 evd' rigidonly v2 t2 u2 in (evd'', Option.map (fun v2' -> mkLambda (name, u1, v2')) v2') diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml index 5ec44a68d..d7b73d333 100644 --- a/pretyping/constr_matching.ml +++ b/pretyping/constr_matching.ml @@ -79,7 +79,7 @@ let add_binders na1 na2 binding_vars (names, terms as subst) = (names, terms) | _ -> subst -let rec build_lambda vars ctx m = match vars with +let rec build_lambda sigma vars ctx m = match vars with | [] -> let len = List.length ctx in lift (-1 * len) m @@ -100,12 +100,12 @@ let rec build_lambda vars ctx m = match vars with let map i = if i > n then pred i else i in let vars = List.map map vars in (** Check that the abstraction is legal *) - let frels = free_rels t in + let frels = free_rels sigma (EConstr.of_constr t) in let brels = List.fold_right Int.Set.add vars Int.Set.empty in let () = if not (Int.Set.subset frels brels) then raise PatternMatchingFailure in (** Create the abstraction *) let m = mkLambda (na, t, m) in - build_lambda vars (pre @ suf) m + build_lambda sigma vars (pre @ suf) m let rec extract_bound_aux k accu frels ctx = match ctx with | [] -> accu @@ -133,12 +133,12 @@ let make_renaming ids = function end | _ -> dummy_constr -let merge_binding allow_bound_rels ctx n cT subst = +let merge_binding sigma allow_bound_rels ctx n cT subst = let c = match ctx with | [] -> (* Optimization *) ([], cT) | _ -> - let frels = free_rels cT in + let frels = free_rels sigma (EConstr.of_constr cT) in if allow_bound_rels then let vars = extract_bound_vars frels ctx in let ordered_vars = Id.Set.elements vars in @@ -169,7 +169,7 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels else false) in let rec sorec ctx env subst p t = - let cT = strip_outer_cast t in + let cT = strip_outer_cast sigma (EConstr.of_constr t) in match p,kind_of_term cT with | PSoApp (n,args),m -> let fold (ans, seen) = function @@ -179,13 +179,13 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels | _ -> error "Only bound indices allowed in second order pattern matching." in let relargs, relset = List.fold_left fold ([], Int.Set.empty) args in - let frels = free_rels cT in + let frels = free_rels sigma (EConstr.of_constr cT) in if Int.Set.subset frels relset then - constrain n ([], build_lambda relargs ctx cT) subst + constrain n ([], build_lambda sigma relargs ctx cT) subst else raise PatternMatchingFailure - | PMeta (Some n), m -> merge_binding allow_bound_rels ctx n cT subst + | PMeta (Some n), m -> merge_binding sigma allow_bound_rels ctx n cT subst | PMeta None, m -> subst @@ -216,7 +216,7 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels let subst = match meta with | None -> subst - | Some n -> merge_binding allow_bound_rels ctx n c subst in + | Some n -> merge_binding sigma allow_bound_rels ctx n c subst in Array.fold_left2 (sorec ctx env) subst args1 args22 else (* Might be a projection on the right *) match kind_of_term c2 with diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index cad5551c1..72cf31010 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -215,11 +215,11 @@ let lookup_name_as_displayed env t s = | Prod (name,_,c') -> (match compute_displayed_name_in RenamingForGoal avoid name c' with | (Name id,avoid') -> if Id.equal id s then Some n else lookup avoid' (n+1) c' - | (Anonymous,avoid') -> lookup avoid' (n+1) (pop c')) + | (Anonymous,avoid') -> lookup avoid' (n+1) (pop (EConstr.of_constr c'))) | LetIn (name,_,_,c') -> (match compute_displayed_name_in RenamingForGoal avoid name c' with | (Name id,avoid') -> if Id.equal id s then Some n else lookup avoid' (n+1) c' - | (Anonymous,avoid') -> lookup avoid' (n+1) (pop c')) + | (Anonymous,avoid') -> lookup avoid' (n+1) (pop (EConstr.of_constr c'))) | Cast (c,_,_) -> lookup avoid n c | _ -> None in lookup (ids_of_named_context (named_context env)) 1 t @@ -261,13 +261,13 @@ let update_name na ((_,(e,_)),c) = | _ -> na -let rec decomp_branch tags nal b (avoid,env as e) c = +let rec decomp_branch tags nal b (avoid,env as e) sigma c = let flag = if b then RenamingForGoal else RenamingForCasesPattern (fst env,c) in match tags with | [] -> (List.rev nal,(e,c)) | b::tags -> let na,c,f,body,t = - match kind_of_term (strip_outer_cast c), b with + match kind_of_term (strip_outer_cast sigma (EConstr.of_constr c)), b with | Lambda (na,t,c),false -> na,c,compute_displayed_let_name_in,None,Some t | LetIn (na,b,t,c),true -> na,c,compute_displayed_name_in,Some b,Some t @@ -279,17 +279,17 @@ let rec decomp_branch tags nal b (avoid,env as e) c = in let na',avoid' = f flag avoid na c in decomp_branch tags (na'::nal) b - (avoid', add_name_opt na' body t env) c + (avoid', add_name_opt na' body t env) sigma c -let rec build_tree na isgoal e ci cl = +let rec build_tree na isgoal e sigma ci cl = let mkpat n rhs pl = PatCstr(dl,(ci.ci_ind,n+1),pl,update_name na rhs) in let cnl = ci.ci_pp_info.cstr_tags in let cna = ci.ci_cstr_nargs in List.flatten (List.init (Array.length cl) - (fun i -> contract_branch isgoal e (cnl.(i),cna.(i),mkpat i,cl.(i)))) + (fun i -> contract_branch isgoal e sigma (cnl.(i),cna.(i),mkpat i,cl.(i)))) -and align_tree nal isgoal (e,c as rhs) = match nal with +and align_tree nal isgoal (e,c as rhs) sigma = match nal with | [] -> [[],rhs] | na::nal -> match kind_of_term c with @@ -298,20 +298,20 @@ and align_tree nal isgoal (e,c as rhs) = match nal with && not (Int.equal (Array.length cl) 0) && (* don't contract if p dependent *) computable p (List.length ci.ci_pp_info.ind_tags) (* FIXME: can do better *) -> - let clauses = build_tree na isgoal e ci cl in + let clauses = build_tree na isgoal e sigma ci cl in List.flatten (List.map (fun (pat,rhs) -> - let lines = align_tree nal isgoal rhs in + let lines = align_tree nal isgoal rhs sigma in List.map (fun (hd,rest) -> pat::hd,rest) lines) clauses) | _ -> let pat = PatVar(dl,update_name na rhs) in - let mat = align_tree nal isgoal rhs in + let mat = align_tree nal isgoal rhs sigma in List.map (fun (hd,rest) -> pat::hd,rest) mat -and contract_branch isgoal e (cdn,can,mkpat,b) = - let nal,rhs = decomp_branch cdn [] isgoal e b in - let mat = align_tree nal isgoal rhs in +and contract_branch isgoal e sigma (cdn,can,mkpat,b) = + let nal,rhs = decomp_branch cdn [] isgoal e sigma b in + let mat = align_tree nal isgoal rhs sigma in List.map (fun (hd,rhs) -> (mkpat rhs hd,rhs)) mat (**********************************************************************) @@ -439,7 +439,7 @@ let detype_instance sigma l = else Some (List.map (detype_level sigma) (Array.to_list (Univ.Instance.to_array l))) let rec detype flags avoid env sigma t = - match kind_of_term (collapse_appl t) with + match kind_of_term (collapse_appl sigma (EConstr.of_constr t)) with | Rel n -> (try match lookup_name_of_rel n (fst env) with | Name id -> GVar (dl, id) @@ -628,7 +628,7 @@ and share_names flags n l avoid env sigma c t = and detype_eqns flags avoid env sigma ci computable constructs consnargsl bl = try if !Flags.raw_print || not (reverse_matching ()) then raise Exit; - let mat = build_tree Anonymous (snd flags) (avoid,env) ci bl in + let mat = build_tree Anonymous (snd flags) (avoid,env) sigma ci bl in List.map (fun (pat,((avoid,env),c)) -> (dl,[],[pat],detype flags avoid env sigma c)) mat with e when CErrors.noncritical e -> diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index d06009dce..194d0b297 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -141,9 +141,10 @@ let check_conv_record env sigma (t1,sk1) (t2,sk2) = match kind_of_term t2 with Prod (_,a,b) -> (* assert (l2=[]); *) let _, a, b = destProd (Evarutil.nf_evar sigma t2) in - if dependent (mkRel 1) b then raise Not_found - else lookup_canonical_conversion (proji, Prod_cs), - (Stack.append_app [|a;pop b|] Stack.empty) + if EConstr.Vars.noccurn sigma 1 (EConstr.of_constr b) then + lookup_canonical_conversion (proji, Prod_cs), + (Stack.append_app [|a;pop (EConstr.of_constr b)|] Stack.empty) + else raise Not_found | Sort s -> lookup_canonical_conversion (proji, Sort_cs (family_of_sort s)),[] @@ -178,7 +179,7 @@ let check_conv_record env sigma (t1,sk1) (t2,sk2) = let c' = subst_univs_level_constr subst c in let t' = subst_univs_level_constr subst t' in let bs' = List.map (subst_univs_level_constr subst) bs in - let h, _ = decompose_app_vect t' in + let h, _ = decompose_app_vect sigma (EConstr.of_constr t') in ctx',(h, t2),c',bs',(Stack.append_app_list params Stack.empty,params1), (Stack.append_app_list us Stack.empty,us2),(extra_args1,extra_args2),c1, (n,Stack.zip(t2,sk2)) @@ -372,7 +373,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty | None -> fallback () | Some l1' -> (* Miller-Pfenning's patterns unification *) let t2 = nf_evar evd tM in - let t2 = solve_pattern_eqn env l1' t2 in + let t2 = solve_pattern_eqn env evd l1' t2 in solve_simple_eqn (evar_conv_x ts) env evd (position_problem on_left pbty,ev,t2) in @@ -893,7 +894,7 @@ and conv_record trs env evd (ctx,(h,h2),c,bs,(params,params1),(us,us2),(sk1,sk2) (fun i -> exact_ise_stack2 env i (evar_conv_x trs) sk1 sk2); test; (fun i -> evar_conv_x trs env i CONV h2 - (fst (decompose_app_vect (substl ks h))))] + (fst (decompose_app_vect i (EConstr.of_constr (substl ks h)))))] else UnifFailure(evd,(*dummy*)NotSameHead) and eta_constructor ts env evd sk1 ((ind, i), u) sk2 term2 = @@ -973,14 +974,14 @@ let apply_on_subterm env evdref f c t = in applyrec (env,(0,c)) t -let filter_possible_projections c ty ctxt args = +let filter_possible_projections evd c ty ctxt args = (* Since args in the types will be replaced by holes, we count the fv of args to have a well-typed filter; don't know how necessary it is however to have a well-typed filter here *) - let fv1 = free_rels (mkApp (c,args)) (* Hack: locally untyped *) in - let fv2 = collect_vars (mkApp (c,args)) in + let fv1 = free_rels evd (EConstr.of_constr (mkApp (c,args))) (* Hack: locally untyped *) in + let fv2 = collect_vars evd (EConstr.of_constr (mkApp (c,args))) in let len = Array.length args in - let tyvars = collect_vars ty in + let tyvars = collect_vars evd (EConstr.of_constr ty) in List.map_i (fun i decl -> let () = assert (i < len) in let a = Array.unsafe_get args i in @@ -1039,7 +1040,7 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs = let t = NamedDecl.get_type decl' in let evs = ref [] in let ty = Retyping.get_type_of env_rhs evd c in - let filter' = filter_possible_projections c ty ctxt args in + let filter' = filter_possible_projections evd c ty ctxt args in (id,t,c,ty,evs,Filter.make filter',occs) :: make_subst (ctxt',l,occsl) | _, _, [] -> [] | _ -> anomaly (Pp.str "Signature or instance are shorter than the occurrences list") in diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index bafb009f5..ea3ab17a7 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -73,7 +73,7 @@ let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) ?(refreshset=false) (** Refresh the types of evars under template polymorphic references *) and refresh_term_evars onevars top t = match kind_of_term (whd_evar !evdref t) with - | App (f, args) when is_template_polymorphic env f -> + | App (f, args) when is_template_polymorphic env !evdref (EConstr.of_constr f) -> let pos = get_polymorphic_positions f in refresh_polymorphic_positions args pos | App (f, args) when top && isEvar f -> @@ -356,14 +356,15 @@ let expansion_of_var aliases x = | [] -> x | a::_ -> a -let rec expand_vars_in_term_using aliases t = match kind_of_term t with +let rec expand_vars_in_term_using sigma aliases t = match kind_of_term t with | Rel _ | Var _ -> normalize_alias aliases t | _ -> - map_constr_with_full_binders - extend_alias expand_vars_in_term_using aliases t + let self aliases c = EConstr.of_constr (expand_vars_in_term_using sigma aliases (EConstr.Unsafe.to_constr c)) in + EConstr.Unsafe.to_constr (map_constr_with_full_binders sigma + extend_alias self aliases (EConstr.of_constr t)) -let expand_vars_in_term env = expand_vars_in_term_using (make_alias_map env) +let expand_vars_in_term env sigma = expand_vars_in_term_using sigma (make_alias_map env) let free_vars_and_rels_up_alias_expansion aliases c = let acc1 = ref Int.Set.empty and acc2 = ref Id.Set.empty in @@ -430,8 +431,8 @@ let constr_list_distinct l = | [] -> true in loop l -let get_actual_deps aliases l t = - if occur_meta_or_existential t then +let get_actual_deps evd aliases l t = + if occur_meta_or_existential evd (EConstr.of_constr t) then (* Probably no restrictions on allowed vars in presence of evars *) l else @@ -460,21 +461,21 @@ let remove_instance_local_defs evd evk args = (* Check if an applied evar "?X[args] l" is a Miller's pattern *) -let find_unification_pattern_args env l t = +let find_unification_pattern_args env evd l t = if List.for_all (fun x -> isRel x || isVar x) l (* common failure case *) then let aliases = make_alias_map env in match (try Some (expand_and_check_vars aliases l) with Exit -> None) with - | Some l as x when constr_list_distinct (get_actual_deps aliases l t) -> x + | Some l as x when constr_list_distinct (get_actual_deps evd aliases l t) -> x | _ -> None else None -let is_unification_pattern_meta env nb m l t = +let is_unification_pattern_meta env evd nb m l t = (* Variables from context and rels > nb are implicitly all there *) (* so we need to be a rel <= nb *) if List.for_all (fun x -> isRel x && destRel x <= nb) l then - match find_unification_pattern_args env l t with - | Some _ as x when not (dependent (mkMeta m) t) -> x + match find_unification_pattern_args env evd l t with + | Some _ as x when not (dependent evd (EConstr.mkMeta m) (EConstr.of_constr t)) -> x | _ -> None else None @@ -485,7 +486,7 @@ let is_unification_pattern_evar env evd (evk,args) l t = then let args = remove_instance_local_defs evd evk args in let n = List.length args in - match find_unification_pattern_args env (args @ l) t with + match find_unification_pattern_args env evd (args @ l) t with | Some l -> Some (List.skipn n l) | _ -> None else None @@ -498,7 +499,7 @@ let is_unification_pattern_pure_evar env evd (evk,args) t = let is_unification_pattern (env,nb) evd f l t = match kind_of_term f with - | Meta m -> is_unification_pattern_meta env nb m l t + | Meta m -> is_unification_pattern_meta env evd nb m l t | Evar ev -> is_unification_pattern_evar env evd ev l t | _ -> None @@ -509,9 +510,9 @@ let is_unification_pattern (env,nb) evd f l t = *implicitly* depend on Vars but lambda abstraction will not reflect this dependency: ?X x = ?1 (?1 is a meta) will return \_.?1 while it should return \y. ?1{x\y} (non constant function if ?1 depends on x) (BB) *) -let solve_pattern_eqn env l c = +let solve_pattern_eqn env sigma l c = let c' = List.fold_right (fun a c -> - let c' = subst_term (lift 1 a) (lift 1 c) in + let c' = subst_term sigma (EConstr.of_constr (lift 1 a)) (EConstr.of_constr (lift 1 c)) in match kind_of_term a with (* Rem: if [a] links to a let-in, do as if it were an assumption *) | Rel n -> @@ -550,7 +551,7 @@ let make_projectable_subst aliases sigma evi args = | LocalAssum (id,c), a::rest -> let a = whd_evar sigma a in let cstrs = - let a',args = decompose_app_vect a in + let a',args = decompose_app_vect sigma (EConstr.of_constr a) in match kind_of_term a' with | Construct cstr -> let l = try Constrmap.find (fst cstr) cstrs with Not_found -> [] in @@ -923,12 +924,12 @@ let invert_invertible_arg fullenv evd aliases k (evk,argsv) args' = let set_of_evctx l = List.fold_left (fun s decl -> Id.Set.add (get_id decl) s) Id.Set.empty l -let filter_effective_candidates evi filter candidates = +let filter_effective_candidates evd evi filter candidates = match filter with | None -> candidates | Some filter -> let ids = set_of_evctx (Filter.filter_list filter (evar_context evi)) in - List.filter (fun a -> Id.Set.subset (collect_vars a) ids) candidates + List.filter (fun a -> Id.Set.subset (collect_vars evd (EConstr.of_constr a)) ids) candidates let filter_candidates evd evk filter candidates_update = let evi = Evd.find_undefined evd evk in @@ -939,7 +940,7 @@ let filter_candidates evd evk filter candidates_update = match candidates with | None -> NoUpdate | Some l -> - let l' = filter_effective_candidates evi filter l in + let l' = filter_effective_candidates evd evi filter l in if List.length l = List.length l' && candidates_update = NoUpdate then NoUpdate else @@ -952,7 +953,7 @@ let closure_of_filter evd evk = function | None -> None | Some filter -> let evi = Evd.find_undefined evd evk in - let vars = collect_vars (Evarutil.nf_evar evd (evar_concl evi)) in + let vars = collect_vars evd (EConstr.of_constr (evar_concl evi)) in let test b decl = b || Idset.mem (get_id decl) vars || match decl with | LocalAssum _ -> @@ -999,7 +1000,7 @@ let do_restrict_hyps evd (evk,args as ev) filter candidates = (* ?e is assumed to have no candidates *) let postpone_non_unique_projection env evd pbty (evk,argsv as ev) sols rhs = - let rhs = expand_vars_in_term env rhs in + let rhs = expand_vars_in_term env evd rhs in let filter = restrict_upon_filter evd evk (* Keep only variables that occur in rhs *) @@ -1010,7 +1011,7 @@ let postpone_non_unique_projection env evd pbty (evk,argsv as ev) sols rhs = (* expands only rels and vars aliases, not rels or vars bound to an *) (* arbitrary complex term *) (fun a -> not (isRel a || isVar a) - || dependent a rhs || List.exists (fun (id,_) -> isVarId id a) sols) + || dependent evd (EConstr.of_constr a) (EConstr.of_constr rhs) || List.exists (fun (id,_) -> isVarId id a) sols) argsv in let filter = closure_of_filter evd evk filter in let candidates = extract_candidates sols in @@ -1060,7 +1061,7 @@ let restrict_candidates conv_algo env evd filter1 (evk1,argsv1) (evk2,argsv2) = | _, None -> filter_candidates evd evk1 filter1 NoUpdate | None, Some _ -> raise DoesNotPreserveCandidateRestriction | Some l1, Some l2 -> - let l1 = filter_effective_candidates evi1 filter1 l1 in + let l1 = filter_effective_candidates evd evi1 filter1 l1 in let l1' = List.filter (fun c1 -> let c1' = instantiate_evar_array evi1 c1 argsv1 in let filter c2 = @@ -1091,9 +1092,7 @@ exception CannotProject of evar_map * existential *) let rec is_constrainable_in top evd k (ev,(fv_rels,fv_ids) as g) t = - let f,args2 = decompose_app_vect t in - let f,args1 = decompose_app_vect (whd_evar evd f) in - let args = Array.append args1 args2 in + let f,args = decompose_app_vect evd (EConstr.of_constr t) in match kind_of_term f with | Construct ((ind,_),u) -> let n = Inductiveops.inductive_nparams ind in @@ -1450,7 +1449,7 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs = | _ -> progress := true; match - let c,args = decompose_app_vect t in + let c,args = decompose_app_vect !evdref (EConstr.of_constr t) in match kind_of_term c with | Construct (cstr,u) when noccur_between 1 k t -> (* This is common case when inferring the return clause of match *) @@ -1466,10 +1465,11 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs = let ty = get_type_of env' !evdref t in let candidates = try + let self env c = EConstr.of_constr (imitate env (EConstr.Unsafe.to_constr c)) in let t = - map_constr_with_full_binders (fun d (env,k) -> push_rel d env, k+1) - imitate envk t in - t::l + map_constr_with_full_binders !evdref (fun d (env,k) -> push_rel d env, k+1) + self envk (EConstr.of_constr t) in + EConstr.Unsafe.to_constr t::l with e when CErrors.noncritical e -> l in (match candidates with | [x] -> x @@ -1480,8 +1480,9 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs = evar'') | None -> (* Evar/Rigid problem (or assimilated if not normal): we "imitate" *) - map_constr_with_full_binders (fun d (env,k) -> push_rel d env, k+1) - imitate envk t + let self env c = EConstr.of_constr (imitate env (EConstr.Unsafe.to_constr c)) in + EConstr.Unsafe.to_constr (map_constr_with_full_binders !evdref (fun d (env,k) -> push_rel d env, k+1) + self envk (EConstr.of_constr t)) in let rhs = whd_beta evd rhs (* heuristic *) in let fast rhs = @@ -1498,7 +1499,7 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs = in is_id_subst filter_ctxt (Array.to_list argsv) && closed0 rhs && - Idset.subset (collect_vars rhs) !names + Idset.subset (collect_vars evd (EConstr.of_constr rhs)) !names in let body = if fast rhs then nf_evar evd rhs @@ -1530,7 +1531,7 @@ and evar_define conv_algo ?(choose=false) env evd pbty (evk,argsv as ev) rhs = with NoCandidates -> try let (evd',body) = invert_definition conv_algo choose env evd pbty ev rhs in - if occur_meta body then raise MetaOccurInBodyInternal; + if occur_meta evd' (EConstr.of_constr body) then raise MetaOccurInBodyInternal; (* invert_definition may have instantiate some evars of rhs with evk *) (* so we recheck acyclicity *) if occur_evar_upto_types evd' evk body then raise (OccurCheckIn (evd',body)); diff --git a/pretyping/evarsolve.mli b/pretyping/evarsolve.mli index f94c83b6d..cf059febf 100644 --- a/pretyping/evarsolve.mli +++ b/pretyping/evarsolve.mli @@ -18,7 +18,7 @@ val is_success : unification_result -> bool (** Replace the vars and rels that are aliases to other vars and rels by their representative that is most ancient in the context *) -val expand_vars_in_term : env -> constr -> constr +val expand_vars_in_term : env -> evar_map -> constr -> constr (** [evar_define choose env ev c] try to instantiate [ev] with [c] (typed in [env]), possibly solving related unification problems, possibly leaving open @@ -62,7 +62,7 @@ val is_unification_pattern_evar : env -> evar_map -> existential -> constr list val is_unification_pattern : env * int -> evar_map -> constr -> constr list -> constr -> constr list option -val solve_pattern_eqn : env -> constr list -> constr -> constr +val solve_pattern_eqn : env -> evar_map -> constr list -> constr -> constr val noccur_evar : env -> evar_map -> Evar.t -> constr -> bool diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 8f369a811..9b572f376 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -751,7 +751,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre match evar_kind_of_term !evdref resj.uj_val with | App (f,args) -> let f = whd_evar !evdref f in - if is_template_polymorphic env.ExtraEnv.env f then + if is_template_polymorphic env.ExtraEnv.env !evdref (EConstr.of_constr f) then (* Special case for inductive type applications that must be refreshed right away. *) let sigma = !evdref in @@ -1009,7 +1009,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre | VMcast -> let cj = pretype empty_tycon env evdref lvar c in let cty = nf_evar !evdref cj.uj_type and tval = nf_evar !evdref tval in - if not (occur_existential cty || occur_existential tval) then + if not (occur_existential !evdref (EConstr.of_constr cty) || occur_existential !evdref (EConstr.of_constr tval)) then let (evd,b) = Reductionops.vm_infer_conv env.ExtraEnv.env !evdref cty tval in if b then (evdref := evd; cj, tval) else diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index cda052b79..e897d5f5c 100644 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -171,7 +171,7 @@ let keep_true_projections projs kinds = let filter (p, (_, b)) = if b then Some p else None in List.map_filter filter (List.combine projs kinds) -let cs_pattern_of_constr t = +let cs_pattern_of_constr sigma t = match kind_of_term t with App (f,vargs) -> begin @@ -179,7 +179,7 @@ let cs_pattern_of_constr t = with e when CErrors.noncritical e -> raise Not_found end | Rel n -> Default_cs, Some n, [] - | Prod (_,a,b) when not (Termops.dependent (mkRel 1) b) -> Prod_cs, None, [a; Termops.pop b] + | Prod (_,a,b) when EConstr.Vars.noccurn sigma 1 (EConstr.of_constr b) -> Prod_cs, None, [a; Termops.pop (EConstr.of_constr b)] | Sort s -> Sort_cs (family_of_sort s), None, [] | _ -> begin @@ -217,7 +217,7 @@ let compute_canonical_projections warn (con,ind) = | Some proji_sp -> begin try - let patt, n , args = cs_pattern_of_constr t in + let patt, n , args = cs_pattern_of_constr Evd.empty t (** FIXME *) in ((ConstRef proji_sp, patt, t, n, args) :: l) with Not_found -> let con_pp = Nametab.pr_global_env Id.Set.empty (ConstRef con) diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli index a6a90c751..4a176760c 100644 --- a/pretyping/recordops.mli +++ b/pretyping/recordops.mli @@ -65,7 +65,7 @@ type obj_typ = { o_TCOMPS : constr list } (** ordered *) (** Return the form of the component of a canonical structure *) -val cs_pattern_of_constr : constr -> cs_pattern * int option * constr list +val cs_pattern_of_constr : Evd.evar_map -> constr -> cs_pattern * int option * constr list val pr_cs_pattern : cs_pattern -> Pp.std_ppcmds diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index a85e493ea..820974888 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -197,14 +197,14 @@ module Cst_stack = struct (** [best_replace d cst_l c] makes the best replacement for [d] by [cst_l] in [c] *) - let best_replace d cst_l c = + let best_replace sigma d cst_l c = let reconstruct_head = List.fold_left (fun t (i,args) -> mkApp (t,Array.sub args i (Array.length args - i))) in List.fold_right - (fun (cst,params,args) t -> Termops.replace_term - (reconstruct_head d args) - (applist (cst, List.rev params)) - t) cst_l c + (fun (cst,params,args) t -> Termops.replace_term sigma + (EConstr.of_constr (reconstruct_head d args)) + (EConstr.of_constr (applist (cst, List.rev params))) + (EConstr.of_constr t)) cst_l c let pr l = let open Pp in @@ -612,8 +612,9 @@ let safe_meta_value sigma ev = let strong whdfun env sigma t = let rec strongrec env t = - map_constr_with_full_binders push_rel strongrec env (whdfun env sigma t) in - strongrec env t + let t = EConstr.of_constr (whdfun env sigma (EConstr.Unsafe.to_constr t)) in + map_constr_with_full_binders sigma push_rel strongrec env t in + EConstr.Unsafe.to_constr (strongrec env (EConstr.of_constr t)) let local_strong whdfun sigma = let rec strongrec t = Constr.map strongrec (whdfun sigma t) in @@ -712,14 +713,14 @@ let contract_cofix ?env ?reference (bodynum,(names,types,bodies as typedbodies)) substl closure bodies.(bodynum) (** Similar to the "fix" case below *) -let reduce_and_refold_cofix recfun env refold cst_l cofix sk = +let reduce_and_refold_cofix recfun env sigma refold cst_l cofix sk = let raw_answer = let env = if refold then Some env else None in contract_cofix ?env ?reference:(Cst_stack.reference cst_l) cofix in apply_subst (fun x (t,sk') -> let t' = - if refold then Cst_stack.best_replace (mkCoFix cofix) cst_l t else t in + if refold then Cst_stack.best_replace sigma (mkCoFix cofix) cst_l t else t in recfun x (t',sk')) [] refold Cst_stack.empty raw_answer sk @@ -757,7 +758,7 @@ let contract_fix ?env ?reference ((recindices,bodynum),(names,types,bodies as ty replace the fixpoint by the best constant from [cst_l] Other rels are directly substituted by constants "magically found from the context" in contract_fix *) -let reduce_and_refold_fix recfun env refold cst_l fix sk = +let reduce_and_refold_fix recfun env sigma refold cst_l fix sk = let raw_answer = let env = if refold then None else Some env in contract_fix ?env ?reference:(Cst_stack.reference cst_l) fix in @@ -765,7 +766,7 @@ let reduce_and_refold_fix recfun env refold cst_l fix sk = (fun x (t,sk') -> let t' = if refold then - Cst_stack.best_replace (mkFix fix) cst_l t + Cst_stack.best_replace sigma (mkFix fix) cst_l t else t in recfun x (t',sk')) [] refold Cst_stack.empty raw_answer sk @@ -947,7 +948,7 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma = | Rel 1, [] -> let lc = Array.sub cl 0 (napp-1) in let u = if Int.equal napp 1 then f else appvect (f,lc) in - if noccurn 1 u then (pop u,Stack.empty),Cst_stack.empty else fold () + if noccurn 1 u then (pop (EConstr.of_constr u),Stack.empty),Cst_stack.empty else fold () | _ -> fold () else fold () | _ -> fold ()) @@ -974,7 +975,7 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma = |args, (Stack.Fix (f,s',cst_l)::s'') when use_fix -> let x' = Stack.zip(x,args) in let out_sk = s' @ (Stack.append_app [|x'|] s'') in - reduce_and_refold_fix whrec env refold cst_l f out_sk + reduce_and_refold_fix whrec env sigma refold cst_l f out_sk |args, (Stack.Cst (const,curr,remains,s',cst_l) :: s'') -> let x' = Stack.zip(x,args) in begin match remains with @@ -1010,7 +1011,7 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma = if CClosure.RedFlags.red_set flags CClosure.RedFlags.fCOFIX then match Stack.strip_app stack with |args, ((Stack.Case _ |Stack.Proj _)::s') -> - reduce_and_refold_cofix whrec env refold cst_l cofix stack + reduce_and_refold_cofix whrec env sigma refold cst_l cofix stack |_ -> fold () else fold () @@ -1043,7 +1044,7 @@ let local_whd_state_gen flags sigma = | Rel 1, [] -> let lc = Array.sub cl 0 (napp-1) in let u = if Int.equal napp 1 then f else appvect (f,lc) in - if noccurn 1 u then (pop u,Stack.empty) else s + if noccurn 1 u then (pop (EConstr.of_constr u),Stack.empty) else s | _ -> s else s | _ -> s) @@ -1568,10 +1569,10 @@ let meta_reducible_instance evd b = in let metas = Metaset.fold fold fm Metamap.empty in let rec irec u = - let u = whd_betaiota Evd.empty u in + let u = whd_betaiota Evd.empty u (** FIXME *) in match kind_of_term u with - | Case (ci,p,c,bl) when isMeta (strip_outer_cast c) -> - let m = destMeta (strip_outer_cast c) in + | Case (ci,p,c,bl) when EConstr.isMeta evd (EConstr.of_constr (strip_outer_cast evd (EConstr.of_constr c))) -> + let m = destMeta (strip_outer_cast evd (EConstr.of_constr c)) in (match try let g, s = Metamap.find m metas in @@ -1581,8 +1582,8 @@ let meta_reducible_instance evd b = with | Some g -> irec (mkCase (ci,p,g,bl)) | None -> mkCase (ci,irec p,c,Array.map irec bl)) - | App (f,l) when isMeta (strip_outer_cast f) -> - let m = destMeta (strip_outer_cast f) in + | App (f,l) when EConstr.isMeta evd (EConstr.of_constr (strip_outer_cast evd (EConstr.of_constr f))) -> + let m = destMeta (strip_outer_cast evd (EConstr.of_constr f)) in (match try let g, s = Metamap.find m metas in diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index 4cd7a2a86..8dcf5c084 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -44,7 +44,7 @@ module Cst_stack : sig val add_args : constr array -> t -> t val add_cst : constr -> t -> t val best_cst : t -> (constr * constr list) option - val best_replace : constr -> t -> constr -> constr + val best_replace : Evd.evar_map -> constr -> t -> constr -> constr val reference : t -> Constant.t option val pr : t -> Pp.std_ppcmds end diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index 5b67af3e7..ac3b5ef63 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -93,7 +93,7 @@ let retype ?(polyprop=true) sigma = let rec type_of env cstr = match kind_of_term cstr with | Meta n -> - (try strip_outer_cast (Evd.meta_ftype sigma n).Evd.rebus + (try strip_outer_cast sigma (EConstr.of_constr (Evd.meta_ftype sigma n).Evd.rebus) with Not_found -> retype_error (BadMeta n)) | Rel n -> let ty = RelDecl.get_type (lookup_rel n env) in @@ -124,12 +124,13 @@ let retype ?(polyprop=true) sigma = subst1 b (type_of (push_rel (LocalDef (name,b,c1)) env) c2) | Fix ((_,i),(_,tys,_)) -> tys.(i) | CoFix (i,(_,tys,_)) -> tys.(i) - | App(f,args) when is_template_polymorphic env f -> + | App(f,args) when is_template_polymorphic env sigma (EConstr.of_constr f) -> + let f = whd_evar sigma f in let t = type_of_global_reference_knowing_parameters env f args in - strip_outer_cast (subst_type env sigma t (Array.to_list args)) + strip_outer_cast sigma (EConstr.of_constr (subst_type env sigma t (Array.to_list args))) | App(f,args) -> - strip_outer_cast - (subst_type env sigma (type_of env f) (Array.to_list args)) + strip_outer_cast sigma + (EConstr.of_constr (subst_type env sigma (type_of env f) (Array.to_list args))) | Proj (p,c) -> let ty = type_of env c in (try @@ -152,7 +153,8 @@ let retype ?(polyprop=true) sigma = | Prop Pos, (Type u2) -> Type (Univ.sup Univ.type0_univ u2) | Prop Null, (Type _ as s) -> s | Type u1, Type u2 -> Type (Univ.sup u1 u2)) - | App(f,args) when is_template_polymorphic env f -> + | App(f,args) when is_template_polymorphic env sigma (EConstr.of_constr f) -> + let f = whd_evar sigma f in let t = type_of_global_reference_knowing_parameters env f args in sort_of_atomic_type env sigma t args | App(f,args) -> sort_of_atomic_type env sigma (type_of env f) args @@ -168,7 +170,8 @@ let retype ?(polyprop=true) sigma = let s2 = sort_family_of (push_rel (LocalAssum (name,t)) env) c2 in if not (is_impredicative_set env) && s2 == InSet && sort_family_of env t == InType then InType else s2 - | App(f,args) when is_template_polymorphic env f -> + | App(f,args) when is_template_polymorphic env sigma (EConstr.of_constr f) -> + let f = whd_evar sigma f in let t = type_of_global_reference_knowing_parameters env f args in family_of_sort (sort_of_atomic_type env sigma t args) | App(f,args) -> diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 7da738508..ff76abe37 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -177,7 +177,7 @@ let eval_table = Summary.ref (Cmap.empty : frozen) ~name:"evaluation" the xp..x1. *) -let check_fix_reversibility labs args ((lv,i),(_,tys,bds)) = +let check_fix_reversibility sigma labs args ((lv,i),(_,tys,bds)) = let n = List.length labs in let nargs = List.length args in if nargs > n then raise Elimconst; @@ -202,7 +202,7 @@ let check_fix_reversibility labs args ((lv,i),(_,tys,bds)) = raise Elimconst; List.iteri (fun i t_i -> if not (Int.List.mem_assoc (i+1) li) then - let fvs = List.map ((+) (i+1)) (Int.Set.elements (free_rels t_i)) in + let fvs = List.map ((+) (i+1)) (Int.Set.elements (free_rels sigma (EConstr.of_constr t_i))) in match List.intersect Int.equal fvs reversible_rels with | [] -> () | _ -> raise Elimconst) @@ -261,7 +261,7 @@ let compute_consteval_direct env sigma ref = let open Context.Rel.Declaration in srec (push_rel (LocalAssum (id,t)) env) (n+1) (t::labs) onlyproj g | Fix fix when not onlyproj -> - (try check_fix_reversibility labs l fix + (try check_fix_reversibility sigma labs l fix with Elimconst -> NotAnElimination) | Case (_,_,d,_) when isRel d && not onlyproj -> EliminationCases n | Case (_,_,d,_) -> srec env n labs true d @@ -1102,13 +1102,13 @@ let fold_one_com com env sigma c = (* Reason first on the beta-iota-zeta normal form of the constant as unfold produces it, so that the "unfold f; fold f" configuration works to refold fix expressions *) - let a = subst_term (clos_norm_flags unfold_side_red env sigma rcom) c in + let a = subst_term sigma (EConstr.of_constr (clos_norm_flags unfold_side_red env sigma rcom)) (EConstr.of_constr c) in if not (eq_constr a c) then subst1 com a else (* Then reason on the non beta-iota-zeta form for compatibility - even if it is probably a useless configuration *) - let a = subst_term rcom c in + let a = subst_term sigma (EConstr.of_constr rcom) (EConstr.of_constr c) in subst1 com a let fold_commands cl env sigma c = @@ -1133,8 +1133,8 @@ let compute = cbv_betadeltaiota let abstract_scheme env (locc,a) (c, sigma) = let ta = Retyping.get_type_of env sigma a in let na = named_hd env ta Anonymous in - if occur_meta ta then error "Cannot find a type for the generalisation."; - if occur_meta a then + if occur_meta sigma (EConstr.of_constr ta) then error "Cannot find a type for the generalisation."; + if occur_meta sigma (EConstr.of_constr a) then mkLambda (na,ta,c), sigma else let c', sigma' = subst_closed_term_occ env sigma (AtOccs locc) a c in diff --git a/pretyping/unification.ml b/pretyping/unification.ml index e2b3af7e9..3134dac6a 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -87,7 +87,7 @@ let abstract_scheme env evd c l lname_typ = are unclear... if occur_meta ta then error "cannot find a type for the generalisation" else *) - if occur_meta a then mkLambda_name env (na,ta,t), evd + if occur_meta evd (EConstr.of_constr a) then mkLambda_name env (na,ta,t), evd else let t', evd' = Find_subterm.subst_closed_term_occ env evd locc a t in mkLambda_name env (na,ta,t'), evd') @@ -182,7 +182,7 @@ let solve_pattern_eqn_array (env,nb) f l c (sigma,metasubst,evarsubst) = extra assumptions added by unification to the context *) let env' = pop_rel_context nb env in let sigma,c = pose_all_metas_as_evars env' sigma c in - let c = solve_pattern_eqn env l c in + let c = solve_pattern_eqn env sigma l c in let pb = (Conv,TypeNotProcessed) in if noccur_between 1 nb c then sigma,(k,lift (-nb) c,pb)::metasubst,evarsubst @@ -190,7 +190,7 @@ let solve_pattern_eqn_array (env,nb) f l c (sigma,metasubst,evarsubst) = | Evar ev -> let env' = pop_rel_context nb env in let sigma,c = pose_all_metas_as_evars env' sigma c in - sigma,metasubst,(env,ev,solve_pattern_eqn env l c)::evarsubst + sigma,metasubst,(env,ev,solve_pattern_eqn env sigma l c)::evarsubst | _ -> assert false let push d (env,n) = (push_rel_assum d env,n+1) @@ -679,7 +679,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb if k2 < k1 then sigma,(k1,cN,stN)::metasubst,evarsubst else sigma,(k2,cM,stM)::metasubst,evarsubst | Meta k, _ - when not (dependent cM cN) (* helps early trying alternatives *) -> + when not (dependent sigma (EConstr.of_constr cM) (EConstr.of_constr cN)) (* helps early trying alternatives *) -> let sigma = if opt.with_types && flags.check_applied_meta_types then (try @@ -699,7 +699,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb evarsubst) else error_cannot_unify_local curenv sigma (m,n,cN) | _, Meta k - when not (dependent cN cM) (* helps early trying alternatives *) -> + when not (dependent sigma (EConstr.of_constr cN) (EConstr.of_constr cM)) (* helps early trying alternatives *) -> let sigma = if opt.with_types && flags.check_applied_meta_types then (try @@ -728,15 +728,15 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb sigma,metasubst,((curenv,ev,cN)::evarsubst) | Evar (evk,_ as ev), _ when not (Evar.Set.mem evk flags.frozen_evars) - && not (occur_evar evk cN) -> - let cmvars = free_rels cM and cnvars = free_rels cN in + && not (occur_evar sigma evk (EConstr.of_constr cN)) -> + let cmvars = free_rels sigma (EConstr.of_constr cM) and cnvars = free_rels sigma (EConstr.of_constr cN) in if Int.Set.subset cnvars cmvars then sigma,metasubst,((curenv,ev,cN)::evarsubst) else error_cannot_unify_local curenv sigma (m,n,cN) | _, Evar (evk,_ as ev) when not (Evar.Set.mem evk flags.frozen_evars) - && not (occur_evar evk cM) -> - let cmvars = free_rels cM and cnvars = free_rels cN in + && not (occur_evar sigma evk (EConstr.of_constr cM)) -> + let cmvars = free_rels sigma (EConstr.of_constr cM) and cnvars = free_rels sigma (EConstr.of_constr cN) in if Int.Set.subset cmvars cnvars then sigma,metasubst,((curenv,ev,cM)::evarsubst) else error_cannot_unify_local curenv sigma (m,n,cN) @@ -1295,8 +1295,8 @@ let w_merge env with_types flags (evd,metas,evars) = (* This can make rhs' ill-typed if metas are *) let rhs' = subst_meta_instances metas rhs in match kind_of_term rhs with - | App (f,cl) when occur_meta rhs' -> - if occur_evar evk rhs' then + | App (f,cl) when occur_meta evd (EConstr.of_constr rhs') -> + if occur_evar evd evk (EConstr.of_constr rhs') then error_occur_check curenv evd evk rhs'; if is_mimick_head flags.modulo_delta f then let evd' = @@ -1474,16 +1474,16 @@ let iter_fail f a = (* make_abstraction: a variant of w_unify_to_subterm which works on contexts, with evars, and possibly with occurrences *) -let indirectly_dependent c d decls = +let indirectly_dependent sigma c d decls = not (isVar c) && (* This test is not needed if the original term is a variable, but it is needed otherwise, as e.g. when abstracting over "2" in "forall H:0=2, H=H:>(0=1+1) -> 0=2." where there is now obvious way to see that the second hypothesis depends indirectly over 2 *) - List.exists (fun d' -> dependent_in_decl (mkVar (NamedDecl.get_id d')) d) decls + List.exists (fun d' -> dependent_in_decl sigma (EConstr.mkVar (NamedDecl.get_id d')) d) decls -let indirect_dependency d decls = - decls |> List.filter (fun d' -> dependent_in_decl (mkVar (NamedDecl.get_id d')) d) |> List.hd |> NamedDecl.get_id +let indirect_dependency sigma d decls = + decls |> List.filter (fun d' -> dependent_in_decl sigma (EConstr.mkVar (NamedDecl.get_id d')) d) |> List.hd |> NamedDecl.get_id let finish_evar_resolution ?(flags=Pretyping.all_and_fail_flags) env current_sigma (pending,c) = let current_sigma = Sigma.to_evar_map current_sigma in @@ -1610,7 +1610,7 @@ let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl = let occ = if likefirst then LikeFirst else AtOccs occ in let newdecl = replace_term_occ_decl_modulo occ test mkvarid d in if Context.Named.Declaration.equal d newdecl - && not (indirectly_dependent c d depdecls) + && not (indirectly_dependent sigma c d depdecls) then if check_occs && not (in_every_hyp occs) then raise (PretypeError (env,sigma,NoOccurrenceFound (c,Some hyp))) @@ -1695,13 +1695,13 @@ let w_unify_to_subterm env evd ?(flags=default_unify_flags ()) (op,cl) = let bestexn = ref None in let kop = Keys.constr_key op in let rec matchrec cl = - let cl = strip_outer_cast cl in + let cl = strip_outer_cast evd (EConstr.of_constr cl) in (try if closed0 cl && not (isEvar cl) && keyed_unify env evd kop cl then (try if !keyed_unification then - let f1, l1 = decompose_app_vect op in - let f2, l2 = decompose_app_vect cl in + let f1, l1 = decompose_app_vect evd (EConstr.of_constr op) in + let f2, l2 = decompose_app_vect evd (EConstr.of_constr cl) in w_typed_unify_array env evd flags f1 l1 f2 l2,cl else w_typed_unify env evd CONV flags op cl,cl with ex when Pretype_errors.unsatisfiable_exception ex -> @@ -1788,7 +1788,7 @@ let w_unify_to_subterm_all env evd ?(flags=default_unify_flags ()) (op,cl) = in ffail 0 in let rec matchrec cl = - let cl = strip_outer_cast cl in + let cl = strip_outer_cast evd (EConstr.of_constr cl) in (bind (if closed0 cl then return (fun () -> w_typed_unify env evd CONV flags op cl,cl) @@ -1839,7 +1839,7 @@ let w_unify_to_subterm_list env evd flags hdmeta oplist t = else let allow_K = flags.allow_K_in_toplevel_higher_order_unification in let flags = - if occur_meta_or_existential op || !keyed_unification then + if occur_meta_or_existential evd (EConstr.of_constr op) || !keyed_unification then (* This is up to delta for subterms w/o metas ... *) flags else @@ -1848,7 +1848,7 @@ let w_unify_to_subterm_list env evd flags hdmeta oplist t = unify pre-existing non frozen evars of the goal or of the pattern *) set_no_delta_flags flags in - let t' = (strip_outer_cast op,t) in + let t' = (strip_outer_cast evd (EConstr.of_constr op),t) in let (evd',cl) = try if is_keyed_unification () then @@ -1864,7 +1864,7 @@ let w_unify_to_subterm_list env evd flags hdmeta oplist t = (* w_unify_to_subterm does not go through evars, so the next step, which was already in <= 8.4, is needed at least for compatibility of rewrite *) - dependent op t -> (evd,op) + dependent evd (EConstr.of_constr op) (EConstr.of_constr t) -> (evd,op) in if not allow_K && (* ensure we found a different instance *) diff --git a/printing/printer.ml b/printing/printer.ml index 3c8ad4255..b36df27ed 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -760,7 +760,8 @@ let pr_prim_rule = function str ";[" ++ cl ++ str"intro " ++ pr_id id ++ str"|idtac]") | Refine c -> - str(if Termops.occur_meta c then "refine " else "exact ") ++ + (** FIXME *) + str(if Termops.occur_meta Evd.empty (EConstr.of_constr c) then "refine " else "exact ") ++ Constrextern.with_meta_as_hole pr_constr c (* Backwards compatibility *) diff --git a/proofs/clenv.ml b/proofs/clenv.ml index fad656223..34bc83097 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -77,7 +77,7 @@ let clenv_push_prod cl = | Cast (t,_,_) -> clrec t | Prod (na,t,u) -> let mv = new_meta () in - let dep = dependent (mkRel 1) u in + let dep = not (EConstr.Vars.noccurn (cl_sigma cl) 1 (EConstr.of_constr u)) in let na' = if dep then na else Anonymous in let e' = meta_declare mv t ~name:na' cl.evd in let concl = if dep then subst1 (mkMeta mv) u else u in @@ -332,7 +332,7 @@ let clenv_pose_metas_as_evars clenv dep_mvs = let ty = clenv_meta_type clenv mv in (* Postpone the evar-ization if dependent on another meta *) (* This assumes no cycle in the dependencies - is it correct ? *) - if occur_meta ty then fold clenv (mvs@[mv]) + if occur_meta clenv.evd (EConstr.of_constr ty) then fold clenv (mvs@[mv]) else let src = evar_source_of_meta mv clenv.evd in let src = adjust_meta_source clenv.evd mv src in @@ -404,7 +404,7 @@ type arg_bindings = constr explicit_bindings * of cval, ctyp. *) let clenv_independent clenv = - let mvs = collect_metas (clenv_value clenv) in + let mvs = collect_metas clenv.evd (EConstr.of_constr (clenv_value clenv)) in let ctyp_mvs = (mk_freelisted (clenv_type clenv)).freemetas in let deps = Metaset.union (dependent_in_type_of_metas clenv mvs) ctyp_mvs in List.filter (fun mv -> not (Metaset.mem mv deps)) mvs @@ -522,7 +522,7 @@ let clenv_match_args bl clenv = exception NoSuchBinding let clenv_constrain_last_binding c clenv = - let all_mvs = collect_metas clenv.templval.rebus in + let all_mvs = collect_metas clenv.evd (EConstr.of_constr clenv.templval.rebus) in let k = try List.last all_mvs with Failure _ -> raise NoSuchBinding in clenv_assign_binding clenv k c @@ -612,7 +612,7 @@ let make_evar_clause env sigma ?len t = let sigma = Sigma.Unsafe.of_evar_map sigma in let Sigma (ev, sigma, _) = new_evar ~store env sigma t1 in let sigma = Sigma.to_evar_map sigma in - let dep = dependent (mkRel 1) t2 in + let dep = not (EConstr.Vars.noccurn sigma 1 (EConstr.of_constr t2)) in let hole = { hole_evar = ev; hole_type = t1; @@ -682,9 +682,9 @@ let solve_evar_clause env sigma hyp_only clause = function if h.hole_deps then (** Some subsequent term uses the hole *) let (ev, _) = destEvar h.hole_evar in - let is_dep hole = occur_evar ev hole.hole_type in + let is_dep hole = occur_evar sigma ev (EConstr.of_constr hole.hole_type) in let in_hyp = List.exists is_dep holes in - let in_ccl = occur_evar ev clause.cl_concl in + let in_ccl = occur_evar sigma ev (EConstr.of_constr clause.cl_concl) in let dep = if hyp_only then in_hyp && not in_ccl else in_hyp || in_ccl in let h = { h with hole_deps = dep } in h :: holes diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml index 98b5bc8b0..d8a20e08b 100644 --- a/proofs/clenvtac.ml +++ b/proofs/clenvtac.ml @@ -33,12 +33,12 @@ let clenv_cast_meta clenv = | _ -> map_constr crec u and crec_hd u = - match kind_of_term (strip_outer_cast u) with + match kind_of_term (strip_outer_cast clenv.evd (EConstr.of_constr u)) with | Meta mv -> (try let b = Typing.meta_type clenv.evd mv in - assert (not (occur_meta b)); - if occur_meta b then u + assert (not (occur_meta clenv.evd (EConstr.of_constr b))); + if occur_meta clenv.evd (EConstr.of_constr b) then u else mkCast (mkMeta mv, DEFAULTcast, b) with Not_found -> u) | App(f,args) -> mkApp (crec_hd f, Array.map crec args) diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml index ff0df9179..d4b308bbe 100644 --- a/proofs/evar_refiner.ml +++ b/proofs/evar_refiner.ml @@ -25,7 +25,7 @@ let depends_on_evar evk _ (pbty,_,t1,t2) = with NoHeadEvar -> false let define_and_solve_constraints evk c env evd = - if Termops.occur_evar evk c then + if Termops.occur_evar evd evk (EConstr.of_constr c) then Pretype_errors.error_occur_check env evd evk c; let evd = define evk c evd in let (evd,pbs) = extract_changed_conv_pbs evd (depends_on_evar evk) in diff --git a/proofs/logic.ml b/proofs/logic.ml index 44c629484..29f295682 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -138,12 +138,12 @@ let find_q x (m,q) = else find (Id.Set.union l accs) (i::acc) itl in find Id.Set.empty [] q -let occur_vars_in_decl env hyps d = +let occur_vars_in_decl env sigma hyps d = if Id.Set.is_empty hyps then false else - let ohyps = global_vars_set_of_decl env d in + let ohyps = global_vars_set_of_decl env sigma d in Id.Set.exists (fun h -> Id.Set.mem h ohyps) hyps -let reorder_context env sign ord = +let reorder_context env sigma sign ord = let ords = List.fold_right Id.Set.add ord Id.Set.empty in if not (Int.equal (List.length ord) (Id.Set.cardinal ords)) then error "Order list has duplicates"; @@ -152,13 +152,13 @@ let reorder_context env sign ord = | [] -> List.rev ctxt_tail @ ctxt_head | top::ord' when mem_q top moved_hyps -> let ((d,h),mh) = find_q top moved_hyps in - if occur_vars_in_decl env h d then + if occur_vars_in_decl env sigma h d then user_err ~hdr:"reorder_context" (str "Cannot move declaration " ++ pr_id top ++ spc() ++ str "before " ++ pr_sequence pr_id (Id.Set.elements (Id.Set.inter h - (global_vars_set_of_decl env d)))); + (global_vars_set_of_decl env sigma d)))); step ord' expected ctxt_head mh (d::ctxt_tail) | _ -> (match ctxt_head with @@ -173,16 +173,16 @@ let reorder_context env sign ord = ctxt (push_val x moved_hyps) (d::ctxt_tail)) in step ord ords sign mt_q [] -let reorder_val_context env sign ord = - val_of_named_context (reorder_context env (named_context_of_val sign) ord) +let reorder_val_context env sigma sign ord = + val_of_named_context (reorder_context env sigma (named_context_of_val sign) ord) -let check_decl_position env sign d = +let check_decl_position env sigma sign d = let x = NamedDecl.get_id d in - let needed = global_vars_set_of_decl env d in - let deps = dependency_closure env (named_context_of_val sign) needed in + let needed = global_vars_set_of_decl env sigma d in + let deps = dependency_closure env sigma (named_context_of_val sign) needed in if Id.List.mem x deps then user_err ~hdr:"Logic.check_decl_position" (str "Cannot create self-referring hypothesis " ++ pr_id x); @@ -233,12 +233,12 @@ let hyp_of_move_location = function | MoveBefore id -> id | _ -> assert false -let move_hyp toleft (left,declfrom,right) hto = +let move_hyp sigma toleft (left,declfrom,right) hto = let env = Global.env() in let test_dep d d2 = if toleft - then occur_var_in_decl env (NamedDecl.get_id d2) d - else occur_var_in_decl env (NamedDecl.get_id d) d2 + then occur_var_in_decl env sigma (NamedDecl.get_id d2) d + else occur_var_in_decl env sigma (NamedDecl.get_id d) d2 in let rec moverec first middle = function | [] -> @@ -278,10 +278,10 @@ let move_hyp toleft (left,declfrom,right) hto = List.fold_left (fun sign d -> push_named_context_val d sign) right left -let move_hyp_in_named_context hfrom hto sign = +let move_hyp_in_named_context sigma hfrom hto sign = let (left,right,declfrom,toleft) = split_sign hfrom hto (named_context_of_val sign) in - move_hyp toleft (left,declfrom,right) hto + move_hyp sigma toleft (left,declfrom,right) hto (**********************************************************************) @@ -320,10 +320,10 @@ let check_conv_leq_goal env sigma arg ty conclty = else sigma exception Stop of constr list -let meta_free_prefix a = +let meta_free_prefix sigma a = try let _ = Array.fold_left (fun acc a -> - if occur_meta a then raise (Stop acc) + if occur_meta sigma (EConstr.of_constr a) then raise (Stop acc) else a :: acc) [] a in a with Stop acc -> Array.rev_of_list acc @@ -338,7 +338,7 @@ let rec mk_refgoals sigma goal goalacc conclty trm = let mk_goal hyps concl = Goal.V82.mk_goal sigma hyps concl (Goal.V82.extra sigma goal) in - if (not !check) && not (occur_meta trm) then + if (not !check) && not (occur_meta sigma (EConstr.of_constr trm)) then let t'ty = Retyping.get_type_of env sigma trm in let sigma = check_conv_leq_goal env sigma trm t'ty conclty in (goalacc,t'ty,sigma,trm) @@ -346,7 +346,7 @@ let rec mk_refgoals sigma goal goalacc conclty trm = match kind_of_term trm with | Meta _ -> let conclty = nf_betaiota sigma conclty in - if !check && occur_meta conclty then + if !check && occur_meta sigma (EConstr.of_constr conclty) then raise (RefinerError (MetaInType conclty)); let (gl,ev,sigma) = mk_goal hyps conclty in gl::goalacc, conclty, sigma, ev @@ -367,10 +367,10 @@ let rec mk_refgoals sigma goal goalacc conclty trm = | App (f,l) -> let (acc',hdty,sigma,applicand) = - if is_template_polymorphic env f then + if is_template_polymorphic env sigma (EConstr.of_constr f) then let ty = (* Template sort-polymorphism of definition and inductive types *) - let firstmeta = Array.findi (fun i x -> occur_meta x) l in + let firstmeta = Array.findi (fun i x -> occur_meta sigma (EConstr.of_constr x)) l in let args, _ = Option.cata (fun i -> CArray.chop i l) (l, [||]) firstmeta in type_of_global_reference_knowing_parameters env sigma f args in @@ -406,7 +406,7 @@ let rec mk_refgoals sigma goal goalacc conclty trm = (acc'',conclty',sigma, ans) | _ -> - if occur_meta trm then + if occur_meta sigma (EConstr.of_constr trm) then anomaly (Pp.str "refiner called with a meta in non app/case subterm"); let t'ty = goal_type_of env sigma trm in let sigma = check_conv_leq_goal env sigma trm t'ty conclty in @@ -432,9 +432,9 @@ and mk_hdgoals sigma goal goalacc trm = | App (f,l) -> let (acc',hdty,sigma,applicand) = - if is_template_polymorphic env f + if is_template_polymorphic env sigma (EConstr.of_constr f) then - let l' = meta_free_prefix l in + let l' = meta_free_prefix sigma l in (goalacc,type_of_global_reference_knowing_parameters env sigma f l',sigma,f) else mk_hdgoals sigma goal goalacc f in @@ -464,7 +464,7 @@ and mk_hdgoals sigma goal goalacc trm = (acc',ty,sigma,c) | _ -> - if !check && occur_meta trm then + if !check && occur_meta sigma (EConstr.of_constr trm) then anomaly (Pp.str "refine called with a dependent meta"); goalacc, goal_type_of env sigma trm, sigma, trm @@ -511,9 +511,9 @@ let convert_hyp check sign sigma d = if check && not (Option.equal (is_conv env sigma) b c) then user_err ~hdr:"Logic.convert_hyp" (str "Incorrect change of the body of "++ pr_id id ++ str "."); - if check then reorder := check_decl_position env sign d; + if check then reorder := check_decl_position env sigma sign d; d) in - reorder_val_context env sign' !reorder + reorder_val_context env sigma sign' !reorder @@ -537,7 +537,7 @@ let prim_refiner r sigma goal = if replace then let nexthyp = get_hyp_after id (named_context_of_val sign) in let sign,t,cl,sigma = clear_hyps2 env sigma (Id.Set.singleton id) sign t cl in - move_hyp false ([], LocalAssum (id,t),named_context_of_val sign) + move_hyp sigma false ([], LocalAssum (id,t),named_context_of_val sign) nexthyp, t,cl,sigma else diff --git a/proofs/logic.mli b/proofs/logic.mli index 0dba9ef1e..8c8a01cad 100644 --- a/proofs/logic.mli +++ b/proofs/logic.mli @@ -57,5 +57,5 @@ val catchable_exception : exn -> bool val convert_hyp : bool -> Environ.named_context_val -> evar_map -> Context.Named.Declaration.t -> Environ.named_context_val -val move_hyp_in_named_context : Id.t -> Id.t Misctypes.move_location -> +val move_hyp_in_named_context : Evd.evar_map -> Id.t -> Id.t Misctypes.move_location -> Environ.named_context_val -> Environ.named_context_val diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml index 34443b93d..a442a5e63 100644 --- a/proofs/redexpr.ml +++ b/proofs/redexpr.ml @@ -25,7 +25,7 @@ open Misctypes (* call by value normalisation function using the virtual machine *) let cbv_vm env sigma c = let ctyp = Retyping.get_type_of env sigma c in - if Termops.occur_meta_or_existential c then + if Termops.occur_meta_or_existential sigma (EConstr.of_constr c) then error "vm_compute does not support existential variables."; Vnorm.cbv_vm env c ctyp diff --git a/tactics/auto.ml b/tactics/auto.ml index d4251555d..17fe7362d 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -302,7 +302,7 @@ let hintmap_of secvars hdc concl = match hdc with | None -> Hint_db.map_none ~secvars | Some hdc -> - if occur_existential concl then + if occur_existential Evd.empty (EConstr.of_constr concl) then (** FIXME *) Hint_db.map_existential ~secvars hdc concl else Hint_db.map_auto ~secvars hdc concl @@ -329,11 +329,12 @@ let rec trivial_fail_db dbg mod_delta db_list local_db = in Proofview.Goal.enter { enter = begin fun gl -> let concl = Tacmach.New.pf_nf_concl gl in + let sigma = Tacmach.New.project gl in let secvars = compute_secvars gl in Tacticals.New.tclFIRST ((dbg_assumption dbg)::intro_tac:: (List.map Tacticals.New.tclCOMPLETE - (trivial_resolve dbg mod_delta db_list local_db secvars concl))) + (trivial_resolve sigma dbg mod_delta db_list local_db secvars concl))) end } and my_find_search_nodelta db_list local_db secvars hdc concl = @@ -346,7 +347,7 @@ and my_find_search mod_delta = and my_find_search_delta db_list local_db secvars hdc concl = let f = hintmap_of secvars hdc concl in - if occur_existential concl then + if occur_existential Evd.empty (EConstr.of_constr concl) (** FIXME *) then List.map_append (fun db -> if Hint_db.use_dn db then @@ -402,10 +403,10 @@ and tac_of_hint dbg db_list local_db concl (flags, ({pat=p; code=t;poly=poly;db= in tclLOG dbg pr_hint (run_hint t tactic) -and trivial_resolve dbg mod_delta db_list local_db secvars cl = +and trivial_resolve sigma dbg mod_delta db_list local_db secvars cl = try let head = - try let hdconstr = decompose_app_bound cl in + try let hdconstr = decompose_app_bound sigma cl in Some hdconstr with Bound -> None in @@ -449,10 +450,10 @@ let h_trivial ?(debug=Off) lems l = gen_trivial ~debug lems l (* The classical Auto tactic *) (**************************************************************************) -let possible_resolve dbg mod_delta db_list local_db secvars cl = +let possible_resolve sigma dbg mod_delta db_list local_db secvars cl = try let head = - try let hdconstr = decompose_app_bound cl in + try let hdconstr = decompose_app_bound sigma cl in Some hdconstr with Bound -> None in @@ -488,12 +489,13 @@ let search d n mod_delta db_list local_db = (Tacticals.New.tclORELSE0 (intro_register d (search d n) local_db) ( Proofview.Goal.enter { enter = begin fun gl -> let concl = Tacmach.New.pf_nf_concl gl in + let sigma = Tacmach.New.project gl in let secvars = compute_secvars gl in let d' = incr_dbg d in Tacticals.New.tclFIRST (List.map (fun ntac -> Tacticals.New.tclTHEN ntac (search d' (n-1) local_db)) - (possible_resolve d mod_delta db_list local_db secvars concl)) + (possible_resolve sigma d mod_delta db_list local_db secvars concl)) end })) end [] in diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index a4243164e..fe7a09f77 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -279,9 +279,9 @@ let clenv_of_prods poly nprods (c, clenv) gl = let (c, _, _) = c in if poly || Int.equal nprods 0 then Some (None, clenv) else - let ty = Retyping.get_type_of (Proofview.Goal.env gl) - (Sigma.to_evar_map (Proofview.Goal.sigma gl)) c in - let diff = nb_prod ty - nprods in + let sigma = Tacmach.New.project gl in + let ty = Retyping.get_type_of (Proofview.Goal.env gl) sigma c in + let diff = nb_prod sigma (EConstr.of_constr ty) - nprods in if Pervasives.(>=) diff 0 then (* Was Some clenv... *) Some (Some diff, @@ -454,13 +454,13 @@ and e_my_find_search db_list local_db secvars hdc complete only_classes sigma co and e_trivial_resolve db_list local_db secvars only_classes sigma concl = try e_my_find_search db_list local_db secvars - (decompose_app_bound concl) true only_classes sigma concl + (decompose_app_bound sigma concl) true only_classes sigma concl with Bound | Not_found -> [] let e_possible_resolve db_list local_db secvars only_classes sigma concl = try e_my_find_search db_list local_db secvars - (decompose_app_bound concl) false only_classes sigma concl + (decompose_app_bound sigma concl) false only_classes sigma concl with Bound | Not_found -> [] let cut_of_hints h = @@ -666,7 +666,7 @@ module V85 = struct let needs_backtrack env evd oev concl = if Option.is_empty oev || is_Prop env evd concl then - occur_existential concl + occur_existential evd (EConstr.of_constr concl) else true let hints_tac hints sk fk {it = gl,info; sigma = s} = @@ -740,7 +740,7 @@ module V85 = struct let fk' = (fun e -> let do_backtrack = - if unique then occur_existential concl + if unique then occur_existential s' (EConstr.of_constr concl) else if info.unique then true else if List.is_empty gls' then needs_backtrack env s' info.is_evar concl @@ -975,7 +975,7 @@ module Search = struct NOT backtrack. *) let needs_backtrack env evd unique concl = if unique || is_Prop env evd concl then - occur_existential concl + occur_existential evd (EConstr.of_constr concl) else true let mark_unresolvables sigma goals = @@ -1486,16 +1486,17 @@ let _ = (** Take the head of the arity of a constr. Used in the partial application tactic. *) -let rec head_of_constr t = - let t = strip_outer_cast(collapse_appl t) in +let rec head_of_constr sigma t = + let t = strip_outer_cast sigma (EConstr.of_constr (collapse_appl sigma (EConstr.of_constr t))) in match kind_of_term t with - | Prod (_,_,c2) -> head_of_constr c2 - | LetIn (_,_,_,c2) -> head_of_constr c2 - | App (f,args) -> head_of_constr f + | Prod (_,_,c2) -> head_of_constr sigma c2 + | LetIn (_,_,_,c2) -> head_of_constr sigma c2 + | App (f,args) -> head_of_constr sigma f | _ -> t let head_of_constr h c = - let c = head_of_constr c in + Proofview.tclEVARMAP >>= fun sigma -> + let c = head_of_constr sigma c in letin_tac None (Name h) c None Locusops.allHyps let not_evar c = diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml index 6b29f574c..fcbad4bf0 100644 --- a/tactics/contradiction.ml +++ b/tactics/contradiction.ml @@ -66,12 +66,12 @@ let contradiction_context = let id = NamedDecl.get_id d in let typ = nf_evar sigma (NamedDecl.get_type d) in let typ = whd_all env sigma typ in - if is_empty_type typ then + if is_empty_type sigma typ then simplest_elim (mkVar id) else match kind_of_term typ with - | Prod (na,t,u) when is_empty_type u -> + | Prod (na,t,u) when is_empty_type sigma u -> let is_unit_or_eq = - if use_negated_unit_or_eq_type () then match_with_unit_or_eq_type t + if use_negated_unit_or_eq_type () then match_with_unit_or_eq_type sigma t else None in Tacticals.New.tclORELSE (match is_unit_or_eq with @@ -105,7 +105,7 @@ let is_negation_of env sigma typ t = match kind_of_term (whd_all env sigma t) with | Prod (na,t,u) -> let u = nf_evar sigma u in - is_empty_type u && is_conv_leq env sigma typ t + is_empty_type sigma u && is_conv_leq env sigma typ t | _ -> false let contradiction_term (c,lbind as cl) = @@ -115,7 +115,7 @@ let contradiction_term (c,lbind as cl) = let type_of = Tacmach.New.pf_unsafe_type_of gl in let typ = type_of c in let _, ccl = splay_prod env sigma typ in - if is_empty_type ccl then + if is_empty_type sigma ccl then Tacticals.New.tclTHEN (elim false None cl None) (Tacticals.New.tclTRY assumption) diff --git a/tactics/eauto.ml b/tactics/eauto.ml index 10c975b8d..6250fef2d 100644 --- a/tactics/eauto.ml +++ b/tactics/eauto.ml @@ -32,7 +32,8 @@ let e_give_exact ?(flags=eauto_unif_flags) c = Proofview.Goal.enter { enter = begin fun gl -> let t1 = Tacmach.New.pf_unsafe_type_of gl c in let t2 = Tacmach.New.pf_concl (Proofview.Goal.assume gl) in - if occur_existential t1 || occur_existential t2 then + let sigma = Tacmach.New.project gl in + if occur_existential sigma (EConstr.of_constr t1) || occur_existential sigma (EConstr.of_constr t2) then Tacticals.New.tclTHEN (Clenvtac.unify ~flags t1) (exact_no_check c) else exact_check c end } @@ -123,7 +124,7 @@ let hintmap_of secvars hdc concl = match hdc with | None -> fun db -> Hint_db.map_none ~secvars db | Some hdc -> - if occur_existential concl then + if occur_existential Evd.empty (EConstr.of_constr concl) then (** FIXME *) (fun db -> Hint_db.map_existential ~secvars hdc concl db) else (fun db -> Hint_db.map_auto ~secvars hdc concl db) (* FIXME: should be (Hint_db.map_eauto hdc concl db) *) @@ -147,7 +148,7 @@ let rec e_trivial_fail_db db_list local_db = let tacl = registered_e_assumption :: (Tacticals.New.tclTHEN Tactics.intro next) :: - (List.map fst (e_trivial_resolve db_list local_db secvars (Tacmach.New.pf_nf_concl gl))) + (List.map fst (e_trivial_resolve (Tacmach.New.project gl) db_list local_db secvars (Tacmach.New.pf_nf_concl gl))) in Tacticals.New.tclFIRST (List.map Tacticals.New.tclCOMPLETE tacl) end } @@ -181,13 +182,13 @@ and e_my_find_search db_list local_db secvars hdc concl = in List.map tac_of_hint hintl -and e_trivial_resolve db_list local_db secvars gl = - let hd = try Some (decompose_app_bound gl) with Bound -> None in +and e_trivial_resolve sigma db_list local_db secvars gl = + let hd = try Some (decompose_app_bound sigma gl) with Bound -> None in try priority (e_my_find_search db_list local_db secvars hd gl) with Not_found -> [] -let e_possible_resolve db_list local_db secvars gl = - let hd = try Some (decompose_app_bound gl) with Bound -> None in +let e_possible_resolve sigma db_list local_db secvars gl = + let hd = try Some (decompose_app_bound sigma gl) with Bound -> None in try List.map (fun (b, (tac, pp)) -> (tac, b, pp)) (e_my_find_search db_list local_db secvars hd gl) with Not_found -> [] @@ -289,7 +290,7 @@ module SearchProblem = struct let l = let concl = Reductionops.nf_evar (project g)(pf_concl g) in filter_tactics s.tacres - (e_possible_resolve s.dblist (List.hd s.localdb) secvars concl) + (e_possible_resolve (project g) s.dblist (List.hd s.localdb) secvars concl) in List.map (fun (lgls, cost, pp) -> diff --git a/tactics/elim.ml b/tactics/elim.ml index 3f0c01a29..12d8e98c4 100644 --- a/tactics/elim.ml +++ b/tactics/elim.ml @@ -79,11 +79,12 @@ let up_to_delta = ref false (* true *) let general_decompose recognizer c = Proofview.Goal.enter { enter = begin fun gl -> let type_of = pf_unsafe_type_of gl in + let sigma = project gl in let typc = type_of c in tclTHENS (cut typc) [ tclTHEN (intro_using tmphyp_name) (onLastHypId - (ifOnHyp recognizer (general_decompose_aux recognizer) + (ifOnHyp (recognizer sigma) (general_decompose_aux (recognizer sigma)) (fun id -> clear [id]))); exact_no_check c ] end } @@ -102,17 +103,17 @@ let head_in indl t gl = let decompose_these c l = Proofview.Goal.enter { enter = begin fun gl -> let indl = List.map (fun x -> x, Univ.Instance.empty) l in - general_decompose (fun (_,t) -> head_in indl t gl) c + general_decompose (fun sigma (_,t) -> head_in indl t gl) c end } let decompose_and c = general_decompose - (fun (_,t) -> is_record t) + (fun sigma (_,t) -> is_record sigma t) c let decompose_or c = general_decompose - (fun (_,t) -> is_disjunction t) + (fun sigma (_,t) -> is_disjunction sigma t) c let h_decompose l c = decompose_these c l @@ -133,7 +134,7 @@ let induction_trailer abs_i abs_j bargs = (fun id -> Proofview.Goal.nf_enter { enter = begin fun gl -> let idty = pf_unsafe_type_of gl (mkVar id) in - let fvty = global_vars (pf_env gl) idty in + let fvty = global_vars (pf_env gl) (project gl) (EConstr.of_constr idty) in let possible_bring_hyps = (List.tl (nLastDecls gl (abs_j - abs_i))) @ bargs.Tacticals.assums in diff --git a/tactics/equality.ml b/tactics/equality.ml index 7c819edad..74f6dd44a 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -405,7 +405,7 @@ let leibniz_rewrite_ebindings_clause cls lft2rgt tac c t l with_evars frzevars d let isatomic = isProd (whd_zeta evd hdcncl) in let dep_fun = if isatomic then dependent else dependent_no_evar in let type_of_cls = type_of_clause cls gl in - let dep = dep_proof_ok && dep_fun c type_of_cls in + let dep = dep_proof_ok && dep_fun evd (EConstr.of_constr c) (EConstr.of_constr type_of_cls) in let Sigma ((elim, effs), sigma, p) = find_elim hdcncl lft2rgt dep cls (Some t) gl in let tac = Proofview.tclEFFECTS effs <*> @@ -442,7 +442,7 @@ let general_rewrite_ebindings_clause cls lft2rgt occs frzevars dep_proof_ok ?tac let env = Proofview.Goal.env gl in let ctype = get_type_of env sigma c in let rels, t = decompose_prod_assum (whd_betaiotazeta sigma ctype) in - match match_with_equality_type t with + match match_with_equality_type sigma t with | Some (hdcncl,args) -> (* Fast path: direct leibniz-like rewrite *) let lft2rgt = adjust_rewriting_direction args lft2rgt in leibniz_rewrite_ebindings_clause cls lft2rgt tac c (it_mkProd_or_LetIn t rels) @@ -455,9 +455,10 @@ let general_rewrite_ebindings_clause cls lft2rgt occs frzevars dep_proof_ok ?tac end begin function | (e, info) -> + Proofview.tclEVARMAP >>= fun sigma -> let env' = push_rel_context rels env in let rels',t' = splay_prod_assum env' sigma t in (* Search for underlying eq *) - match match_with_equality_type t' with + match match_with_equality_type sigma t' with | Some (hdcncl,args) -> let lft2rgt = adjust_rewriting_direction args lft2rgt in leibniz_rewrite_ebindings_clause cls lft2rgt tac c @@ -932,9 +933,10 @@ let rec build_discriminator env sigma dirn c = function let gen_absurdity id = Proofview.Goal.enter { enter = begin fun gl -> + let sigma = project gl in let hyp_typ = pf_get_hyp_typ id (Proofview.Goal.assume gl) in let hyp_typ = pf_nf_evar gl hyp_typ in - if is_empty_type hyp_typ + if is_empty_type sigma hyp_typ then simplest_elim (mkVar id) else @@ -973,7 +975,7 @@ let apply_on_clause (f,t) clause = let sigma = clause.evd in let f_clause = mk_clenv_from_env clause.env sigma None (f,t) in let argmv = - (match kind_of_term (last_arg f_clause.templval.Evd.rebus) with + (match kind_of_term (last_arg f_clause.evd (EConstr.of_constr f_clause.templval.Evd.rebus)) with | Meta mv -> mv | _ -> user_err (str "Ill-formed clause applicator.")) in clenv_fchain ~with_univs:false argmv f_clause clause @@ -1025,7 +1027,7 @@ let onNegatedEquality with_evars tac = let ccl = Proofview.Goal.concl gl in let env = Proofview.Goal.env gl in match kind_of_term (hnf_constr env sigma ccl) with - | Prod (_,t,u) when is_empty_type u -> + | Prod (_,t,u) when is_empty_type sigma u -> tclTHEN introf (onLastHypId (fun id -> onEquality with_evars tac (mkVar id,NoBindings))) @@ -1079,7 +1081,7 @@ let find_sigma_data env s = build_sigma_type () *) let make_tuple env sigma (rterm,rty) lind = - assert (dependent (mkRel lind) rty); + assert (not (EConstr.Vars.noccurn sigma lind (EConstr.of_constr rty))); let sigdata = find_sigma_data env (get_sort_of env sigma rty) in let sigma, a = type_of ~refresh:true env sigma (mkRel lind) in let na = Context.Rel.Declaration.get_name (lookup_rel lind env) in @@ -1101,9 +1103,9 @@ let make_tuple env sigma (rterm,rty) lind = normalization *) let minimal_free_rels env sigma (c,cty) = - let cty_rels = free_rels cty in + let cty_rels = free_rels sigma (EConstr.of_constr cty) in let cty' = simpl env sigma cty in - let rels' = free_rels cty' in + let rels' = free_rels sigma (EConstr.of_constr cty') in if Int.Set.subset cty_rels rels' then (cty,cty_rels) else @@ -1302,6 +1304,7 @@ let set_eq_dec_scheme_kind k = eq_dec_scheme_kind_name := (fun _ -> k) let inject_if_homogenous_dependent_pair ty = Proofview.Goal.nf_enter { enter = begin fun gl -> try + let sigma = Tacmach.New.project gl in let eq,u,(t,t1,t2) = find_this_eq_data_decompose gl ty in (* fetch the informations of the pair *) let ceq = Universes.constr_of_global Coqlib.glob_eq in @@ -1310,8 +1313,8 @@ let inject_if_homogenous_dependent_pair ty = (* check whether the equality deals with dep pairs or not *) let eqTypeDest = fst (decompose_app t) in if not (Globnames.is_global (sigTconstr()) eqTypeDest) then raise Exit; - let hd1,ar1 = decompose_app_vect t1 and - hd2,ar2 = decompose_app_vect t2 in + let hd1,ar1 = decompose_app_vect sigma (EConstr.of_constr t1) and + hd2,ar2 = decompose_app_vect sigma (EConstr.of_constr t2) in if not (Globnames.is_global (existTconstr()) hd1) then raise Exit; if not (Globnames.is_global (existTconstr()) hd2) then raise Exit; let ind,_ = try pf_apply find_mrectype gl ar1.(0) with Not_found -> raise Exit in @@ -1543,7 +1546,7 @@ let subst_tuple_term env sigma dep_pair1 dep_pair2 b = (* We build the expected goal *) let abst_B = List.fold_right - (fun (e,t) body -> lambda_create env (t,subst_term e body)) e1_list b in + (fun (e,t) body -> lambda_create env (t,subst_term sigma (EConstr.of_constr e) (EConstr.of_constr body))) e1_list b in let pred_body = beta_applist(abst_B,proj_list) in let body = mkApp (lambda_create env (typ,pred_body),[|dep_pair1|]) in let expected_goal = beta_applist (abst_B,List.map fst e2_list) in @@ -1674,8 +1677,8 @@ let is_eq_x gl x d = in let c = pf_nf_evar gl (NamedDecl.get_type d) in let (_,lhs,rhs) = pi3 (find_eq_data_decompose gl c) in - if (is_var x lhs) && not (local_occur_var x rhs) then raise (FoundHyp (id,rhs,true)); - if (is_var x rhs) && not (local_occur_var x lhs) then raise (FoundHyp (id,lhs,false)) + if (is_var x lhs) && not (local_occur_var (project gl) x (EConstr.of_constr rhs)) then raise (FoundHyp (id,rhs,true)); + if (is_var x rhs) && not (local_occur_var (project gl) x (EConstr.of_constr lhs)) then raise (FoundHyp (id,lhs,false)) with Constr_matching.PatternMatchingFailure -> () @@ -1685,6 +1688,7 @@ let is_eq_x gl x d = let subst_one dep_proof_ok x (hyp,rhs,dir) = Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in + let sigma = Tacmach.New.project gl in let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in let concl = Proofview.Goal.concl (Proofview.Goal.assume gl) in (* The set of hypotheses using x *) @@ -1692,7 +1696,7 @@ let subst_one dep_proof_ok x (hyp,rhs,dir) = List.rev (pi3 (List.fold_right (fun dcl (dest,deps,allhyps) -> let id = NamedDecl.get_id dcl in if not (Id.equal id hyp) - && List.exists (fun y -> occur_var_in_decl env y dcl) deps + && List.exists (fun y -> occur_var_in_decl env sigma y dcl) deps then let id_dest = if !regular_subst_tactic then dest else MoveLast in (dest,id::deps,(id_dest,id)::allhyps) @@ -1701,7 +1705,7 @@ let subst_one dep_proof_ok x (hyp,rhs,dir) = hyps (MoveBefore x,[x],[]))) in (* In practice, no dep hyps before x, so MoveBefore x is good enough *) (* Decides if x appears in conclusion *) - let depconcl = occur_var env x concl in + let depconcl = occur_var env sigma x (EConstr.of_constr concl) in let need_rewrite = not (List.is_empty dephyps) || depconcl in tclTHENLIST ((if need_rewrite then @@ -1787,6 +1791,7 @@ let subst_all ?(flags=default_subst_tactic_flags ()) () = let process hyp = Proofview.Goal.enter { enter = begin fun gl -> let gl = Proofview.Goal.assume gl in + let sigma = project gl in let env = Proofview.Goal.env gl in let find_eq_data_decompose = find_eq_data_decompose gl in let c = pf_get_hyp hyp gl |> NamedDecl.get_type in @@ -1794,9 +1799,9 @@ let subst_all ?(flags=default_subst_tactic_flags ()) () = (* J.F.: added to prevent failure on goal containing x=x as an hyp *) if Term.eq_constr x y then Proofview.tclUNIT () else match kind_of_term x, kind_of_term y with - | Var x', _ when not (occur_term x y) && not (is_evaluable env (EvalVarRef x')) -> + | Var x', _ when not (occur_term sigma (EConstr.of_constr x) (EConstr.of_constr y)) && not (is_evaluable env (EvalVarRef x')) -> subst_one flags.rewrite_dependent_proof x' (hyp,y,true) - | _, Var y' when not (occur_term y x) && not (is_evaluable env (EvalVarRef y')) -> + | _, Var y' when not (occur_term sigma (EConstr.of_constr y) (EConstr.of_constr x)) && not (is_evaluable env (EvalVarRef y')) -> subst_one flags.rewrite_dependent_proof y' (hyp,x,false) | _ -> Proofview.tclUNIT () diff --git a/tactics/hints.ml b/tactics/hints.ml index 9fa49264f..55bf5f29e 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -45,8 +45,8 @@ type debug = Debug | Info | Off exception Bound -let head_constr_bound t = - let t = strip_outer_cast t in +let head_constr_bound sigma t = + let t = strip_outer_cast sigma (EConstr.of_constr t) in let _,ccl = decompose_prod_assum t in let hd,args = decompose_app ccl in match kind_of_term hd with @@ -54,13 +54,13 @@ let head_constr_bound t = | Proj (p, _) -> mkConst (Projection.constant p) | _ -> raise Bound -let head_constr c = - try head_constr_bound c with Bound -> error "Bound head variable." +let head_constr sigma c = + try head_constr_bound sigma c with Bound -> error "Bound head variable." -let decompose_app_bound t = - let t = strip_outer_cast t in +let decompose_app_bound sigma t = + let t = strip_outer_cast sigma (EConstr.of_constr t) in let _,ccl = decompose_prod_assum t in - let hd,args = decompose_app_vect ccl in + let hd,args = decompose_app_vect sigma (EConstr.of_constr ccl) in match kind_of_term hd with | Const (c,u) -> ConstRef c, args | Ind (i,u) -> IndRef i, args @@ -505,7 +505,7 @@ struct let match_mode m arg = match m with - | ModeInput -> not (occur_existential arg) + | ModeInput -> not (occur_existential Evd.empty (EConstr.of_constr arg)) (** FIXME *) | ModeNoHeadEvar -> Evarutil.(try ignore(head_evar arg); false with NoHeadEvar -> true) @@ -742,7 +742,7 @@ let secvars_of_global env gr = let make_exact_entry env sigma pri poly ?(name=PathAny) (c, cty, ctx) = let secvars = secvars_of_constr env c in - let cty = strip_outer_cast cty in + let cty = strip_outer_cast sigma (EConstr.of_constr cty) in match kind_of_term cty with | Prod _ -> failwith "make_exact_entry" | _ -> @@ -911,7 +911,7 @@ let make_trivial env sigma poly ?(name=PathAny) r = let c,ctx = fresh_global_or_constr env sigma poly r in let sigma = Evd.merge_context_set univ_flexible sigma ctx in let t = hnf_constr env sigma (unsafe_type_of env sigma c) in - let hd = head_of_constr_reference (head_constr t) in + let hd = head_of_constr_reference (head_constr sigma t) in let ce = mk_clenv_from_env env sigma None (c,t) in (Some hd, { pri=1; poly = poly; @@ -1013,7 +1013,7 @@ let subst_autohint (subst, obj) = let subst_key gr = let (lab'', elab') = subst_global subst gr in let gr' = - (try head_of_constr_reference (head_constr_bound elab') + (try head_of_constr_reference (head_constr_bound Evd.empty (** FIXME *) elab') with Bound -> lab'') in if gr' == gr then gr else gr' in @@ -1190,17 +1190,17 @@ let prepare_hint check (poly,local) env init (sigma,c) = thing make_resolves will do is to re-instantiate the products *) let sigma, subst = Evd.nf_univ_variables sigma in let c = Vars.subst_univs_constr subst (Evarutil.nf_evar sigma c) in - let c = drop_extra_implicit_args c in - let vars = ref (collect_vars c) in + let c = drop_extra_implicit_args sigma (EConstr.of_constr c) in + let vars = ref (collect_vars sigma (EConstr.of_constr c)) in let subst = ref [] in let rec find_next_evar c = match kind_of_term c with | Evar (evk,args as ev) -> (* We skip the test whether args is the identity or not *) let t = Evarutil.nf_evar sigma (existential_type sigma ev) in - let t = List.fold_right (fun (e,id) c -> replace_term e id c) !subst t in + let t = List.fold_right (fun (e,id) c -> replace_term sigma (EConstr.of_constr e) (EConstr.of_constr id) (EConstr.of_constr c)) !subst t in if not (closed0 c) then error "Hints with holes dependent on a bound variable not supported."; - if occur_existential t then + if occur_existential sigma (EConstr.of_constr t) then (* Not clever enough to construct dependency graph of evars *) error "Not clever enough to deal with evars dependent in other evars."; raise (Found (c,t)) @@ -1211,7 +1211,7 @@ let prepare_hint check (poly,local) env init (sigma,c) = let id = next_ident_away_from default_prepare_hint_ident (fun id -> Id.Set.mem id !vars) in vars := Id.Set.add id !vars; subst := (evar,mkVar id)::!subst; - mkNamedLambda id t (iter (replace_term evar (mkVar id) c)) in + mkNamedLambda id t (iter (replace_term sigma (EConstr.of_constr evar) (EConstr.mkVar id) (EConstr.of_constr c))) in let c' = iter c in if check then Pretyping.check_evars (Global.env()) Evd.empty sigma c'; let diff = Univ.ContextSet.diff (Evd.universe_context_set sigma) (Evd.universe_context_set init) in @@ -1394,13 +1394,13 @@ let pr_hint_ref ref = pr_hint_list_for_head ref (* Print all hints associated to head id in any database *) -let pr_hint_term cl = +let pr_hint_term sigma cl = try let dbs = current_db () in let valid_dbs = let fn = try - let hdc = decompose_app_bound cl in - if occur_existential cl then + let hdc = decompose_app_bound sigma cl in + if occur_existential sigma (EConstr.of_constr cl) then Hint_db.map_existential ~secvars:Id.Pred.full hdc cl else Hint_db.map_auto ~secvars:Id.Pred.full hdc cl with Bound -> Hint_db.map_none ~secvars:Id.Pred.full @@ -1423,7 +1423,7 @@ let pr_applicable_hint () = match glss.Evd.it with | [] -> CErrors.error "No focused goal." | g::_ -> - pr_hint_term (Goal.V82.concl glss.Evd.sigma g) + pr_hint_term glss.Evd.sigma (Goal.V82.concl glss.Evd.sigma g) let pp_hint_mode = function | ModeInput -> str"+" diff --git a/tactics/hints.mli b/tactics/hints.mli index edc65c407..c0eb2c3b8 100644 --- a/tactics/hints.mli +++ b/tactics/hints.mli @@ -24,7 +24,7 @@ open Vernacexpr exception Bound -val decompose_app_bound : constr -> global_reference * constr array +val decompose_app_bound : evar_map -> constr -> global_reference * constr array type debug = Debug | Info | Off diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml index 27af7200b..847ecf4b0 100644 --- a/tactics/hipattern.ml +++ b/tactics/hipattern.ml @@ -31,9 +31,9 @@ module RelDecl = Context.Rel.Declaration -- Eduardo (6/8/97). *) -type 'a matching_function = constr -> 'a option +type 'a matching_function = Evd.evar_map -> constr -> 'a option -type testing_function = constr -> bool +type testing_function = Evd.evar_map -> constr -> bool let mkmeta n = Nameops.make_ident "X" (Some n) let meta1 = mkmeta 1 @@ -43,7 +43,7 @@ let meta4 = mkmeta 4 let op2bool = function Some _ -> true | None -> false -let match_with_non_recursive_type t = +let match_with_non_recursive_type sigma t = match kind_of_term t with | App _ -> let (hdapp,args) = decompose_app t in @@ -56,21 +56,21 @@ let match_with_non_recursive_type t = | _ -> None) | _ -> None -let is_non_recursive_type t = op2bool (match_with_non_recursive_type t) +let is_non_recursive_type sigma t = op2bool (match_with_non_recursive_type sigma t) (* Test dependencies *) (* NB: we consider also the let-in case in the following function, since they may appear in types of inductive constructors (see #2629) *) -let rec has_nodep_prod_after n c = +let rec has_nodep_prod_after n sigma c = match kind_of_term c with | Prod (_,_,b) | LetIn (_,_,_,b) -> - ( n>0 || not (dependent (mkRel 1) b)) - && (has_nodep_prod_after (n-1) b) + ( n>0 || EConstr.Vars.noccurn sigma 1 (EConstr.of_constr b)) + && (has_nodep_prod_after (n-1) sigma b) | _ -> true -let has_nodep_prod = has_nodep_prod_after 0 +let has_nodep_prod sigma c = has_nodep_prod_after 0 sigma c (* A general conjunctive type is a non-recursive with-no-indices inductive type with only one constructor and no dependencies between argument; @@ -87,7 +87,7 @@ let is_lax_conjunction = function | Some false -> true | _ -> false -let match_with_one_constructor style onlybinary allow_rec t = +let match_with_one_constructor sigma style onlybinary allow_rec t = let (hdapp,args) = decompose_app t in let res = match kind_of_term hdapp with | Ind ind -> @@ -112,7 +112,7 @@ let match_with_one_constructor style onlybinary allow_rec t = else let ctyp = prod_applist mip.mind_nf_lc.(0) args in let cargs = List.map RelDecl.get_type (prod_assum ctyp) in - if not (is_lax_conjunction style) || has_nodep_prod ctyp then + if not (is_lax_conjunction style) || has_nodep_prod sigma ctyp then (* Record or non strict conjunction *) Some (hdapp,List.rev cargs) else @@ -125,28 +125,28 @@ let match_with_one_constructor style onlybinary allow_rec t = | Some (hdapp, [_; _]) -> res | _ -> None -let match_with_conjunction ?(strict=false) ?(onlybinary=false) t = - match_with_one_constructor (Some strict) onlybinary false t +let match_with_conjunction ?(strict=false) ?(onlybinary=false) sigma t = + match_with_one_constructor sigma (Some strict) onlybinary false t -let match_with_record t = - match_with_one_constructor None false false t +let match_with_record sigma t = + match_with_one_constructor sigma None false false t -let is_conjunction ?(strict=false) ?(onlybinary=false) t = - op2bool (match_with_conjunction ~strict ~onlybinary t) +let is_conjunction ?(strict=false) ?(onlybinary=false) sigma t = + op2bool (match_with_conjunction sigma ~strict ~onlybinary t) -let is_record t = - op2bool (match_with_record t) +let is_record sigma t = + op2bool (match_with_record sigma t) -let match_with_tuple t = - let t = match_with_one_constructor None false true t in +let match_with_tuple sigma t = + let t = match_with_one_constructor sigma None false true t in Option.map (fun (hd,l) -> let ind = destInd hd in let (mib,mip) = Global.lookup_pinductive ind in let isrec = mis_is_recursive (fst ind,mib,mip) in (hd,l,isrec)) t -let is_tuple t = - op2bool (match_with_tuple t) +let is_tuple sigma t = + op2bool (match_with_tuple sigma t) (* A general disjunction type is a non-recursive with-no-indices inductive type with of which all constructors have a single argument; @@ -159,7 +159,7 @@ let test_strict_disjunction n lc = | [LocalAssum (_,c)] -> isRel c && Int.equal (destRel c) (n - i) | _ -> false) 0 lc -let match_with_disjunction ?(strict=false) ?(onlybinary=false) t = +let match_with_disjunction ?(strict=false) ?(onlybinary=false) sigma t = let (hdapp,args) = decompose_app t in let res = match kind_of_term hdapp with | Ind (ind,u) -> @@ -187,13 +187,13 @@ let match_with_disjunction ?(strict=false) ?(onlybinary=false) t = | Some (hdapp,[_; _]) -> res | _ -> None -let is_disjunction ?(strict=false) ?(onlybinary=false) t = - op2bool (match_with_disjunction ~strict ~onlybinary t) +let is_disjunction ?(strict=false) ?(onlybinary=false) sigma t = + op2bool (match_with_disjunction ~strict ~onlybinary sigma t) (* An empty type is an inductive type, possible with indices, that has no constructors *) -let match_with_empty_type t = +let match_with_empty_type sigma t = let (hdapp,args) = decompose_app t in match (kind_of_term hdapp) with | Ind ind -> @@ -202,33 +202,33 @@ let match_with_empty_type t = if Int.equal nconstr 0 then Some hdapp else None | _ -> None -let is_empty_type t = op2bool (match_with_empty_type t) +let is_empty_type sigma t = op2bool (match_with_empty_type sigma t) (* This filters inductive types with one constructor with no arguments; Parameters and indices are allowed *) -let match_with_unit_or_eq_type t = +let match_with_unit_or_eq_type sigma t = let (hdapp,args) = decompose_app t in match (kind_of_term hdapp) with | Ind ind -> let (mib,mip) = Global.lookup_pinductive ind in let constr_types = mip.mind_nf_lc in let nconstr = Array.length mip.mind_consnames in - let zero_args c = Int.equal (nb_prod c) mib.mind_nparams in + let zero_args c = Int.equal (nb_prod sigma (EConstr.of_constr c)) mib.mind_nparams in if Int.equal nconstr 1 && zero_args constr_types.(0) then Some hdapp else None | _ -> None -let is_unit_or_eq_type t = op2bool (match_with_unit_or_eq_type t) +let is_unit_or_eq_type sigma t = op2bool (match_with_unit_or_eq_type sigma t) (* A unit type is an inductive type with no indices but possibly (useless) parameters, and that has no arguments in its unique constructor *) -let is_unit_type t = - match match_with_conjunction t with +let is_unit_type sigma t = + match match_with_conjunction sigma t with | Some (_,[]) -> true | _ -> false @@ -318,13 +318,13 @@ let is_inductive_equality ind = let nconstr = Array.length mip.mind_consnames in Int.equal nconstr 1 && Int.equal (constructor_nrealargs (ind,1)) 0 -let match_with_equality_type t = +let match_with_equality_type sigma t = let (hdapp,args) = decompose_app t in match (kind_of_term hdapp) with | Ind (ind,_) when is_inductive_equality ind -> Some (hdapp,args) | _ -> None -let is_equality_type t = op2bool (match_with_equality_type t) +let is_equality_type sigma t = op2bool (match_with_equality_type sigma t) (* Arrows/Implication/Negation *) @@ -338,37 +338,37 @@ let match_arrow_pattern t = assert (Id.equal m1 meta1 && Id.equal m2 meta2); (arg, mind) | _ -> anomaly (Pp.str "Incorrect pattern matching") -let match_with_imp_term c= +let match_with_imp_term sigma c = match kind_of_term c with - | Prod (_,a,b) when not (dependent (mkRel 1) b) ->Some (a,b) + | Prod (_,a,b) when EConstr.Vars.noccurn sigma 1 (EConstr.of_constr b) -> Some (a,b) | _ -> None -let is_imp_term c = op2bool (match_with_imp_term c) +let is_imp_term sigma c = op2bool (match_with_imp_term sigma c) -let match_with_nottype t = +let match_with_nottype sigma t = try let (arg,mind) = match_arrow_pattern t in - if is_empty_type mind then Some (mind,arg) else None + if is_empty_type sigma mind then Some (mind,arg) else None with PatternMatchingFailure -> None -let is_nottype t = op2bool (match_with_nottype t) +let is_nottype sigma t = op2bool (match_with_nottype sigma t) (* Forall *) -let match_with_forall_term c= +let match_with_forall_term sigma c= match kind_of_term c with | Prod (nam,a,b) -> Some (nam,a,b) | _ -> None -let is_forall_term c = op2bool (match_with_forall_term c) +let is_forall_term sigma c = op2bool (match_with_forall_term sigma c) -let match_with_nodep_ind t = +let match_with_nodep_ind sigma t = let (hdapp,args) = decompose_app t in match (kind_of_term hdapp) with | Ind ind -> let (mib,mip) = Global.lookup_pinductive ind in if Array.length (mib.mind_packets)>1 then None else - let nodep_constr = has_nodep_prod_after mib.mind_nparams in + let nodep_constr = has_nodep_prod_after mib.mind_nparams sigma in if Array.for_all nodep_constr mip.mind_nf_lc then let params= if Int.equal mip.mind_nrealargs 0 then args else @@ -378,9 +378,9 @@ let match_with_nodep_ind t = None | _ -> None -let is_nodep_ind t=op2bool (match_with_nodep_ind t) +let is_nodep_ind sigma t = op2bool (match_with_nodep_ind sigma t) -let match_with_sigma_type t= +let match_with_sigma_type sigma t = let (hdapp,args) = decompose_app t in match (kind_of_term hdapp) with | Ind ind -> @@ -388,14 +388,14 @@ let match_with_sigma_type t= if Int.equal (Array.length (mib.mind_packets)) 1 && (Int.equal mip.mind_nrealargs 0) && (Int.equal (Array.length mip.mind_consnames)1) && - has_nodep_prod_after (mib.mind_nparams+1) mip.mind_nf_lc.(0) then + has_nodep_prod_after (mib.mind_nparams+1) sigma mip.mind_nf_lc.(0) then (*allowing only 1 existential*) Some (hdapp,args) else None | _ -> None -let is_sigma_type t=op2bool (match_with_sigma_type t) +let is_sigma_type sigma t = op2bool (match_with_sigma_type sigma t) (***** Destructing patterns bound to some theory *) diff --git a/tactics/hipattern.mli b/tactics/hipattern.mli index 7cc41f1b9..8a453bf31 100644 --- a/tactics/hipattern.mli +++ b/tactics/hipattern.mli @@ -40,8 +40,8 @@ open Coqlib also work on ad-hoc disjunctions introduced by the user. (Eduardo, 6/8/97). *) -type 'a matching_function = constr -> 'a option -type testing_function = constr -> bool +type 'a matching_function = Evd.evar_map -> constr -> 'a option +type testing_function = Evd.evar_map -> constr -> bool val match_with_non_recursive_type : (constr * constr list) matching_function val is_non_recursive_type : testing_function diff --git a/tactics/inv.ml b/tactics/inv.ml index e7d8249e4..d1d6178da 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -32,8 +32,9 @@ module NamedDecl = Context.Named.Declaration let var_occurs_in_pf gl id = let env = Proofview.Goal.env gl in - occur_var env id (Proofview.Goal.concl gl) || - List.exists (occur_var_in_decl env id) (Proofview.Goal.hyps gl) + let sigma = project gl in + occur_var env sigma id (EConstr.of_constr (Proofview.Goal.concl gl)) || + List.exists (occur_var_in_decl env sigma id) (Proofview.Goal.hyps gl) (* [make_inv_predicate (ity,args) C] @@ -75,7 +76,7 @@ let make_inv_predicate env evd indf realargs id status concl = let hyps_arity,_ = get_arity env indf in (hyps_arity,concl) | Dep dflt_concl -> - if not (occur_var env id concl) then + if not (occur_var env !evd id (EConstr.of_constr concl)) then user_err ~hdr:"make_inv_predicate" (str "Current goal does not depend on " ++ pr_id id ++ str"."); (* We abstract the conclusion of goal with respect to @@ -183,7 +184,7 @@ let dependent_hyps env id idlist gl = | d::l -> (* Update the type of id1: it may have been subject to rewriting *) let d = pf_get_hyp (NamedDecl.get_id d) gl in - if occur_var_in_decl env id d + if occur_var_in_decl env (project gl) id d then d :: dep_rec l else dep_rec l in @@ -448,7 +449,7 @@ let raw_inversion inv_kind id status names = make_inv_predicate env evdref indf realargs id status concl in let sigma = !evdref in let (cut_concl,case_tac) = - if status != NoDep && (dependent c concl) then + if status != NoDep && (dependent sigma (EConstr.of_constr c) (EConstr.of_constr concl)) then Reduction.beta_appvect elim_predicate (Array.of_list (realargs@[c])), case_then_using else @@ -514,12 +515,14 @@ let invIn k names ids id = Proofview.Goal.nf_enter { enter = begin fun gl -> let hyps = List.map (fun id -> pf_get_hyp id gl) ids in let concl = Proofview.Goal.concl gl in - let nb_prod_init = nb_prod concl in + let sigma = project gl in + let nb_prod_init = nb_prod sigma (EConstr.of_constr concl) in let intros_replace_ids = Proofview.Goal.enter { enter = begin fun gl -> let concl = pf_nf_concl gl in + let sigma = project gl in let nb_of_new_hyp = - nb_prod concl - (List.length hyps + nb_prod_init) + nb_prod sigma (EConstr.of_constr concl) - (List.length hyps + nb_prod_init) in if nb_of_new_hyp < 1 then intros_replacing ids diff --git a/tactics/leminv.ml b/tactics/leminv.ml index 10fc5076c..46f1f7c8d 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -154,7 +154,7 @@ let compute_first_inversion_scheme env sigma ind sort dep_option = pty,goal else let i = mkAppliedInd ind in - let ivars = global_vars env i in + let ivars = global_vars env sigma (EConstr.of_constr i) in let revargs,ownsign = fold_named_context (fun env d (revargs,hyps) -> @@ -192,7 +192,7 @@ let inversion_scheme env sigma t sort dep_option inv_op = in assert (List.subset - (global_vars env invGoal) + (global_vars env sigma (EConstr.of_constr invGoal)) (ids_of_named_context (named_context invEnv))); (* user_err ~hdr:"lemma_inversion" @@ -277,7 +277,8 @@ let lemInvIn id c ids = let hyps = List.map (fun id -> pf_get_hyp id gl) ids in let intros_replace_ids = let concl = Proofview.Goal.concl gl in - let nb_of_new_hyp = nb_prod concl - List.length ids in + let sigma = project gl in + let nb_of_new_hyp = nb_prod sigma (EConstr.of_constr concl) - List.length ids in if nb_of_new_hyp < 1 then intros_replacing ids else diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index 93c04e373..676b23d09 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -630,7 +630,7 @@ module New = struct (* applying elimination_scheme just a little modified *) let elimclause = Tacmach.New.of_old (fun gls -> mk_clenv_from gls (elim,Tacmach.New.pf_unsafe_type_of gl elim)) gl in let indmv = - match kind_of_term (last_arg elimclause.templval.Evd.rebus) with + match kind_of_term (last_arg elimclause.evd (EConstr.of_constr elimclause.templval.Evd.rebus)) with | Meta mv -> mv | _ -> anomaly (str"elimination") in diff --git a/tactics/tactics.ml b/tactics/tactics.ml index e17bbfcb0..15dd1a97c 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -323,10 +323,11 @@ let apply_clear_request clear_flag dft c = let move_hyp id dest = Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in + let sigma = Tacmach.New.project gl in let ty = Proofview.Goal.raw_concl gl in let store = Proofview.Goal.extra gl in let sign = named_context_val env in - let sign' = move_hyp_in_named_context id dest sign in + let sign' = move_hyp_in_named_context sigma id dest sign in let env = reset_with_named_context sign' env in Refine.refine ~unsafe:true { run = begin fun sigma -> Evarutil.new_evar env sigma ~principal:true ~store ty @@ -497,7 +498,7 @@ fun env sigma p -> function let Sigma (rem, sigma, r) = mk_holes env sigma (p +> q) rem in Sigma (arg :: rem, sigma, r) -let rec check_mutind env sigma k cl = match kind_of_term (strip_outer_cast cl) with +let rec check_mutind env sigma k cl = match kind_of_term (strip_outer_cast sigma (EConstr.of_constr cl)) with | Prod (na, c1, b) -> if Int.equal k 1 then try @@ -936,13 +937,14 @@ let build_intro_tac id dest tac = match dest with let rec intro_then_gen name_flag move_flag force_flag dep_flag tac = let open Context.Rel.Declaration in Proofview.Goal.enter { enter = begin fun gl -> + let sigma = Tacmach.New.project gl in let concl = Proofview.Goal.concl (Proofview.Goal.assume gl) in let concl = nf_evar (Tacmach.New.project gl) concl in match kind_of_term concl with - | Prod (name,t,u) when not dep_flag || (dependent (mkRel 1) u) -> + | Prod (name,t,u) when not dep_flag || not (EConstr.Vars.noccurn sigma 1 (EConstr.of_constr u)) -> let name = find_name false (LocalAssum (name,t)) name_flag gl in build_intro_tac name move_flag tac - | LetIn (name,b,t,u) when not dep_flag || (dependent (mkRel 1) u) -> + | LetIn (name,b,t,u) when not dep_flag || not (EConstr.Vars.noccurn sigma 1 (EConstr.of_constr u)) -> let name = find_name false (LocalDef (name,b,t)) name_flag gl in build_intro_tac name move_flag tac | _ -> @@ -1285,7 +1287,7 @@ let clenv_refine_in ?(sidecond_first=false) with_evars ?(with_classes=true) in let new_hyp_typ = clenv_type clenv in if not with_evars then check_unresolved_evars_of_metas sigma0 clenv; - if not with_evars && occur_meta new_hyp_typ then + if not with_evars && occur_meta clenv.evd (EConstr.of_constr new_hyp_typ) then error_uninstantiated_metas new_hyp_typ clenv; let new_hyp_prf = clenv_value clenv in let exact_tac = Proofview.V82.tactic (Tacmach.refine_no_check new_hyp_prf) in @@ -1440,7 +1442,7 @@ let general_case_analysis_in_context with_evars clear_flag (c,lbindc) = let (mind,_) = reduce_to_quantified_ind env (Sigma.to_evar_map sigma) t in let sort = Tacticals.New.elimination_sort_of_goal gl in let Sigma (elim, sigma, p) = - if occur_term c concl then + if occur_term (Sigma.to_evar_map sigma) (EConstr.of_constr c) (EConstr.of_constr concl) then build_case_analysis_scheme env sigma mind true sort else build_case_analysis_scheme_default env sigma mind sort in @@ -1624,7 +1626,7 @@ let descend_in_conjunctions avoid tac (err, info) c = let t = Retyping.get_type_of env sigma c in let ((ind,u),t) = reduce_to_quantified_ind env sigma t in let sign,ccl = decompose_prod_assum t in - match match_with_tuple ccl with + match match_with_tuple sigma ccl with | Some (_,_,isrec) -> let n = (constructors_nrealargs ind).(0) in let sort = Tacticals.New.elimination_sort_of_goal gl in @@ -1689,12 +1691,13 @@ let tclORELSEOPT t k = let general_apply with_delta with_destruct with_evars clear_flag (loc,(c,lbind)) = Proofview.Goal.nf_enter { enter = begin fun gl -> let concl = Proofview.Goal.concl gl in + let sigma = Tacmach.New.project gl in let flags = if with_delta then default_unify_flags () else default_no_delta_unify_flags () in (* The actual type of the theorem. It will be matched against the goal. If this fails, then the head constant will be unfolded step by step. *) - let concl_nprod = nb_prod_modulo_zeta concl in + let concl_nprod = nb_prod_modulo_zeta sigma (EConstr.of_constr concl) in let rec try_main_apply with_destruct c = Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in @@ -1703,7 +1706,7 @@ let general_apply with_delta with_destruct with_evars clear_flag (loc,(c,lbind)) let thm_ty0 = nf_betaiota sigma (Retyping.get_type_of env sigma c) in let try_apply thm_ty nprod = try - let n = nb_prod_modulo_zeta thm_ty - nprod in + let n = nb_prod_modulo_zeta sigma (EConstr.of_constr thm_ty) - nprod in if n<0 then error "Applied theorem has not enough premisses."; let clause = make_clenv_binding_apply env sigma (Some n) (c,thm_ty) lbind in Clenvtac.res_pf clause ~with_evars ~flags @@ -1901,8 +1904,9 @@ let apply_in_delayed_once sidecond_first with_delta with_destruct with_evars nam let cut_and_apply c = Proofview.Goal.nf_enter { enter = begin fun gl -> + let sigma = Tacmach.New.project gl in match kind_of_term (Tacmach.New.pf_hnf_constr gl (Tacmach.New.pf_unsafe_type_of gl c)) with - | Prod (_,c1,c2) when not (dependent (mkRel 1) c2) -> + | Prod (_,c1,c2) when EConstr.Vars.noccurn sigma 1 (EConstr.of_constr c2) -> let concl = Proofview.Goal.concl gl in let env = Tacmach.New.pf_env gl in Refine.refine { run = begin fun sigma -> @@ -2049,7 +2053,7 @@ let clear_body ids = (** Do no recheck hypotheses that do not depend *) let sigma = if not seen then sigma - else if List.exists (fun id -> occur_var_in_decl env id decl) ids then + else if List.exists (fun id -> occur_var_in_decl env sigma id decl) ids then check_decl env sigma decl else sigma in @@ -2058,7 +2062,7 @@ let clear_body ids = in let (env, sigma, _) = List.fold_left check (base_env, sigma, false) (List.rev ctx) in let sigma = - if List.exists (fun id -> occur_var env id concl) ids then + if List.exists (fun id -> occur_var env sigma id (EConstr.of_constr concl)) ids then check_is_type env sigma concl else sigma in @@ -2096,12 +2100,13 @@ let keep hyps = Proofview.Goal.nf_enter { enter = begin fun gl -> Proofview.tclENV >>= fun env -> let ccl = Proofview.Goal.concl gl in + let sigma = Tacmach.New.project gl in let cl,_ = fold_named_context_reverse (fun (clear,keep) decl -> let hyp = NamedDecl.get_id decl in if Id.List.mem hyp hyps - || List.exists (occur_var_in_decl env hyp) keep - || occur_var env hyp ccl + || List.exists (occur_var_in_decl env sigma hyp) keep + || occur_var env sigma hyp (EConstr.of_constr ccl) then (clear,decl::keep) else (hyp::clear,keep)) ~init:([],[]) (Proofview.Goal.env gl) @@ -2310,15 +2315,16 @@ let rewrite_hyp_then assert_style with_evars thin l2r id tac = List.filter (fun (_,id) -> not (Id.equal id id')) thin in Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in + let sigma = Tacmach.New.project gl in let type_of = Tacmach.New.pf_unsafe_type_of gl in let whd_all = Tacmach.New.pf_apply whd_all gl in let t = whd_all (type_of (mkVar id)) in - let eqtac, thin = match match_with_equality_type t with + let eqtac, thin = match match_with_equality_type sigma t with | Some (hdcncl,[_;lhs;rhs]) -> - if l2r && isVar lhs && not (occur_var env (destVar lhs) rhs) then + if l2r && isVar lhs && not (occur_var env sigma (destVar lhs) (EConstr.of_constr rhs)) then let id' = destVar lhs in subst_on l2r id' rhs, early_clear id' thin - else if not l2r && isVar rhs && not (occur_var env (destVar rhs) lhs) then + else if not l2r && isVar rhs && not (occur_var env sigma (destVar rhs) (EConstr.of_constr lhs)) then let id' = destVar rhs in subst_on l2r id' lhs, early_clear id' thin else @@ -2763,8 +2769,8 @@ let generalized_name c t ids cl = function let generalize_goal_gen env sigma ids i ((occs,c,b),na) t cl = let open Context.Rel.Declaration in let decls,cl = decompose_prod_n_assum i cl in - let dummy_prod = it_mkProd_or_LetIn mkProp decls in - let newdecls,_ = decompose_prod_n_assum i (subst_term_gen eq_constr_nounivs c dummy_prod) in + let dummy_prod = EConstr.of_constr (it_mkProd_or_LetIn mkProp decls) in + let newdecls,_ = decompose_prod_n_assum i (subst_term_gen sigma EConstr.eq_constr_nounivs (EConstr.of_constr c) dummy_prod) in let cl',sigma' = subst_closed_term_occ env sigma (AtOccs occs) c (it_mkProd_or_LetIn cl newdecls) in let na = generalized_name c t ids cl' na in let decl = match b with @@ -2782,10 +2788,11 @@ let generalize_goal gl i ((occs,c,b),na as o) (cl,sigma) = let old_generalize_dep ?(with_let=false) c gl = let env = pf_env gl in let sign = pf_hyps gl in + let sigma = project gl in let init_ids = ids_of_named_context (Global.named_context()) in let seek (d:Context.Named.Declaration.t) (toquant:Context.Named.t) = - if List.exists (fun d' -> occur_var_in_decl env (NamedDecl.get_id d') d) toquant - || dependent_in_decl c d then + if List.exists (fun d' -> occur_var_in_decl env sigma (NamedDecl.get_id d') d) toquant + || dependent_in_decl sigma (EConstr.of_constr c) d then d::toquant else toquant in @@ -2901,14 +2908,14 @@ let specialize (c,lbind) ipat = let (thd,tstack) = whd_nored_stack clause.evd (clenv_value clause) in let rec chk = function | [] -> [] - | t::l -> if occur_meta t then [] else t :: chk l + | t::l -> if occur_meta clause.evd (EConstr.of_constr t) then [] else t :: chk l in let tstack = chk tstack in let term = applist(thd,List.map (nf_evar clause.evd) tstack) in - if occur_meta term then + if occur_meta clause.evd (EConstr.of_constr term) then user_err (str "Cannot infer an instance for " ++ - pr_name (meta_name clause.evd (List.hd (collect_metas term))) ++ + pr_name (meta_name clause.evd (List.hd (collect_metas clause.evd (EConstr.of_constr term)))) ++ str "."); clause.evd, term in let typ = Retyping.get_type_of env sigma term in @@ -3143,10 +3150,11 @@ let induct_discharge with_evars dests avoid' tac (avoid,ra) names = let expand_projections env sigma c = let sigma = Sigma.to_evar_map sigma in let rec aux env c = - match kind_of_term c with - | Proj (p, c) -> Retyping.expand_projection env sigma p (aux env c) [] - | _ -> map_constr_with_full_binders push_rel aux env c - in aux env c + match EConstr.kind sigma c with + | Proj (p, c) -> EConstr.of_constr (Retyping.expand_projection env sigma p (EConstr.Unsafe.to_constr (aux env c)) []) + | _ -> map_constr_with_full_binders sigma push_rel aux env c + in + EConstr.Unsafe.to_constr (aux env (EConstr.of_constr c)) (* Marche pas... faut prendre en compte l'occurrence précise... *) @@ -3173,16 +3181,17 @@ let atomize_param_of_ind_then (indref,nparams,_) hyp0 tac = else let c = List.nth argl (i-1) in match kind_of_term c with - | Var id when not (List.exists (occur_var env id) args') && - not (List.exists (occur_var env id) params') -> + | Var id when not (List.exists (fun c -> occur_var env (Sigma.to_evar_map sigma) id (EConstr.of_constr c)) args') && + not (List.exists (fun c -> occur_var env (Sigma.to_evar_map sigma) id (EConstr.of_constr c)) params') -> (* Based on the knowledge given by the user, all constraints on the variable are generalizable in the current environment so that it is clearable after destruction *) atomize_one (i-1) (c::args) (c::args') (id::avoid) | _ -> let c' = expand_projections env' sigma c in - if List.exists (dependent c) params' || - List.exists (dependent c) args' + let dependent t = dependent (Sigma.to_evar_map sigma) (EConstr.of_constr c) (EConstr.of_constr t) in + if List.exists dependent params' || + List.exists dependent args' then (* This is a case where the argument is constrained in a way which would require some kind of inversion; we @@ -3272,7 +3281,7 @@ let atomize_param_of_ind_then (indref,nparams,_) hyp0 tac = exception Shunt of Id.t move_location -let cook_sign hyp0_opt inhyps indvars env = +let cook_sign hyp0_opt inhyps indvars env sigma = (* First phase from L to R: get [toclear], [decldep] and [statuslist] for the hypotheses before (= more ancient than) hyp0 (see above) *) let toclear = ref [] in @@ -3299,11 +3308,11 @@ let cook_sign hyp0_opt inhyps indvars env = rhyp end else let dephyp0 = List.is_empty inhyps && - (Option.cata (fun id -> occur_var_in_decl env id decl) false hyp0_opt) + (Option.cata (fun id -> occur_var_in_decl env sigma id decl) false hyp0_opt) in let depother = List.is_empty inhyps && - (List.exists (fun id -> occur_var_in_decl env id decl) indvars || - List.exists (fun decl' -> occur_var_in_decl env (NamedDecl.get_id decl') decl) !decldeps) + (List.exists (fun id -> occur_var_in_decl env sigma id decl) indvars || + List.exists (fun decl' -> occur_var_in_decl env sigma (NamedDecl.get_id decl') decl) !decldeps) in if not (List.is_empty inhyps) && Id.List.mem hyp inhyps || dephyp0 || depother @@ -3549,7 +3558,7 @@ let make_abstract_generalize env id typ concl dep ctx body c eqs args refls = Sigma (mkApp (appeqs, abshypt), sigma, p) end } -let hyps_of_vars env sign nogen hyps = +let hyps_of_vars env sigma sign nogen hyps = if Id.Set.is_empty hyps then [] else let (_,lh) = @@ -3559,7 +3568,7 @@ let hyps_of_vars env sign nogen hyps = if Id.Set.mem x nogen then (hs,hl) else if Id.Set.mem x hs then (hs,x::hl) else - let xvars = global_vars_set_of_decl env d in + let xvars = global_vars_set_of_decl env sigma d in if not (Id.Set.is_empty (Id.Set.diff xvars hs)) then (Id.Set.add x hs, x :: hl) else (hs, hl)) @@ -3592,7 +3601,7 @@ let abstract_args gl generalize_vars dep id defined f args = let sigma = ref (Tacmach.project gl) in let env = Tacmach.pf_env gl in let concl = Tacmach.pf_concl gl in - let dep = dep || dependent (mkVar id) concl in + let dep = dep || local_occur_var !sigma id (EConstr.of_constr concl) in let avoid = ref [] in let get_id name = let id = fresh_id !avoid (match name with Name n -> n | Anonymous -> Id.of_string "gen_x") gl in @@ -3659,7 +3668,7 @@ let abstract_args gl generalize_vars dep id defined f args = let vars = if generalize_vars then let nogen = Id.Set.add id nogen in - hyps_of_vars (pf_env gl) (pf_hyps gl) nogen vars + hyps_of_vars (pf_env gl) (project gl) (pf_hyps gl) nogen vars else [] in let body, c' = @@ -3845,7 +3854,7 @@ let compute_elim_sig ?elimc elimt = let ccl = exchange_hd_app (mkVar (Id.of_string "__QI_DUMMY__")) conclusion in let concl_with_args = it_mkProd_or_LetIn ccl args_indargs in - let nparams = Int.Set.cardinal (free_rels concl_with_args) in + let nparams = Int.Set.cardinal (free_rels Evd.empty (** FIXME *) (EConstr.of_constr concl_with_args)) in let preds,params = List.chop (List.length params_preds - nparams) params_preds in (* A first approximation, further analysis will tweak it *) @@ -3905,7 +3914,7 @@ let compute_elim_sig ?elimc elimt = with e when CErrors.noncritical e -> error "Cannot find the inductive type of the inductive scheme." -let compute_scheme_signature scheme names_info ind_type_guess = +let compute_scheme_signature evd scheme names_info ind_type_guess = let open Context.Rel.Declaration in let f,l = decompose_app scheme.concl in (* Vérifier que les arguments de Qi sont bien les xi. *) @@ -3940,9 +3949,9 @@ let compute_scheme_signature scheme names_info ind_type_guess = let rec check_branch p c = match kind_of_term c with | Prod (_,t,c) -> - (is_pred p t, true, dependent (mkRel 1) c) :: check_branch (p+1) c + (is_pred p t, true, not (EConstr.Vars.noccurn evd 1 (EConstr.of_constr c))) :: check_branch (p+1) c | LetIn (_,_,_,c) -> - (OtherArg, false, dependent (mkRel 1) c) :: check_branch (p+1) c + (OtherArg, false, not (EConstr.Vars.noccurn evd 1 (EConstr.of_constr c))) :: check_branch (p+1) c | _ when is_pred p c == IndArg -> [] | _ -> raise Exit in @@ -3975,7 +3984,7 @@ let compute_scheme_signature scheme names_info ind_type_guess = different. *) let compute_elim_signature (evd,(elimc,elimt),ind_type_guess) names_info = let scheme = compute_elim_sig ~elimc:elimc elimt in - evd, (compute_scheme_signature scheme names_info ind_type_guess, scheme) + evd, (compute_scheme_signature evd scheme names_info ind_type_guess, scheme) let guess_elim isrec dep s hyp0 gl = let tmptyp0 = Tacmach.New.pf_get_hyp_typ hyp0 gl in @@ -4022,7 +4031,7 @@ let find_induction_type isrec elim hyp0 gl = let evd, (elimc,elimt),ind_guess = given_elim hyp0 e gl in let scheme = compute_elim_sig ~elimc elimt in if Option.is_empty scheme.indarg then error "Cannot find induction type"; - let indsign = compute_scheme_signature scheme hyp0 ind_guess in + let indsign = compute_scheme_signature evd scheme hyp0 ind_guess in let elim = ({elimindex = Some(-1); elimbody = elimc; elimrename = None},elimt) in scheme, ElimUsing (elim,indsign) in @@ -4049,7 +4058,7 @@ let get_eliminator elim dep s gl = | ElimOver (isrec,id) -> let evd, (elimc,elimt),_ as elims = guess_elim isrec dep s id gl in let _, (l, s) = compute_elim_signature elims id in - let branchlengthes = List.map (fun d -> assert (RelDecl.is_local_assum d); pi1 (decompose_prod_letin (RelDecl.get_type d))) + let branchlengthes = List.map (fun d -> assert (RelDecl.is_local_assum d); pi1 (decompose_prod_letin (Tacmach.New.project gl) (EConstr.of_constr (RelDecl.get_type d)))) (List.rev s.branches) in evd, isrec, ({elimindex = None; elimbody = elimc; elimrename = Some (isrec,Array.of_list branchlengthes)}, elimt), l @@ -4118,8 +4127,8 @@ let apply_induction_in_context with_evars hyp0 inhyps elim indvars names induct_ let env = Proofview.Goal.env gl in let sigma = Sigma.to_evar_map sigma in let concl = Tacmach.New.pf_nf_concl gl in - let statuslists,lhyp0,toclear,deps,avoid,dep_in_hyps = cook_sign hyp0 inhyps indvars env in - let dep_in_concl = Option.cata (fun id -> occur_var env id concl) false hyp0 in + let statuslists,lhyp0,toclear,deps,avoid,dep_in_hyps = cook_sign hyp0 inhyps indvars env sigma in + let dep_in_concl = Option.cata (fun id -> occur_var env sigma id (EConstr.of_constr concl)) false hyp0 in let dep = dep_in_hyps || dep_in_concl in let tmpcl = it_mkNamedProd_or_LetIn concl deps in let s = Retyping.get_sort_family_of env sigma tmpcl in @@ -4207,7 +4216,7 @@ let induction_without_atomization isrec with_evars elim names lid = (* assume that no occurrences are selected *) let clear_unselected_context id inhyps cls = Proofview.Goal.nf_enter { enter = begin fun gl -> - if occur_var (Tacmach.New.pf_env gl) id (Tacmach.New.pf_concl gl) && + if occur_var (Tacmach.New.pf_env gl) (Tacmach.New.project gl) id (EConstr.of_constr (Tacmach.New.pf_concl gl)) && cls.concl_occs == NoOccurrences then user_err (str "Conclusion must be mentioned: it depends on " ++ pr_id id @@ -4219,7 +4228,7 @@ let clear_unselected_context id inhyps cls = if Id.List.mem id' inhyps then (* if selected, do not erase *) None else (* erase if not selected and dependent on id or selected hyps *) - let test id = occur_var_in_decl (Tacmach.New.pf_env gl) id d in + let test id = occur_var_in_decl (Tacmach.New.pf_env gl) (Tacmach.New.project gl) id d in if List.exists test (id::inhyps) then Some id' else None in let ids = List.map_filter to_erase (Proofview.Goal.hyps gl) in clear ids @@ -4246,7 +4255,7 @@ let use_bindings env sigma elim must_be_closed (c,lbind) typ = let rec find_clause typ = try let indclause = make_clenv_binding env sigma (c,typ) lbind in - if must_be_closed && occur_meta (clenv_value indclause) then + if must_be_closed && occur_meta indclause.evd (EConstr.of_constr (clenv_value indclause)) then error "Need a fully applied argument."; (* We lose the possibility of coercions in with-bindings *) let (sigma, c) = pose_all_metas_as_evars env indclause.evd (clenv_value indclause) in @@ -4351,10 +4360,10 @@ let pose_induction_arg_then isrec with_evars (is_arg_pure_hyp,from_prefix) elim Sigma (tac, sigma', p +> q) end } -let has_generic_occurrences_but_goal cls id env ccl = +let has_generic_occurrences_but_goal cls id env sigma ccl = clause_with_generic_context_selection cls && (* TODO: whd_evar of goal *) - (cls.concl_occs != NoOccurrences || not (occur_var env id ccl)) + (cls.concl_occs != NoOccurrences || not (occur_var env sigma id (EConstr.of_constr ccl))) let induction_gen clear_flag isrec with_evars elim ((_pending,(c,lbind)),(eqname,names) as arg) cls = @@ -4371,7 +4380,7 @@ let induction_gen clear_flag isrec with_evars elim isVar c && not (mem_named_context_val (destVar c) (Global.named_context_val ())) && lbind == NoBindings && not with_evars && Option.is_empty eqname && clear_flag == None - && has_generic_occurrences_but_goal cls (destVar c) env ccl in + && has_generic_occurrences_but_goal cls (destVar c) env (Sigma.to_evar_map sigma) ccl in let enough_applied = check_enough_applied env sigma elim t in if is_arg_pure_hyp && enough_applied then (* First case: induction on a variable already in an inductive type and @@ -4423,11 +4432,12 @@ let induction_gen_l isrec with_evars elim names lc = | _ -> Proofview.Goal.enter { enter = begin fun gl -> let type_of = Tacmach.New.pf_unsafe_type_of gl in + let sigma = Tacmach.New.project gl in let x = id_of_name_using_hdchar (Global.env()) (type_of c) Anonymous in let id = new_fresh_id [] x gl in - let newl' = List.map (replace_term c (mkVar id)) l' in + let newl' = List.map (fun r -> replace_term sigma (EConstr.of_constr c) (EConstr.mkVar id) (EConstr.of_constr r)) l' in let _ = newlc:=id::!newlc in Tacticals.New.tclTHEN (letin_tac None (Name id) c None allHypsAndConcl) @@ -4601,8 +4611,9 @@ let reflexivity_red allowred = (* PL: usual reflexivity don't perform any reduction when searching for an equality, but we may need to do some when called back from inside setoid_reflexivity (see Optimize cases in setoid_replace.ml). *) + let sigma = Tacmach.New.project gl in let concl = maybe_betadeltaiota_concl allowred gl in - match match_with_equality_type concl with + match match_with_equality_type sigma concl with | None -> Proofview.tclZERO NoEquationFound | Some _ -> one_constructor 1 NoBindings end } diff --git a/tactics/term_dnet.ml b/tactics/term_dnet.ml index e4b45489d..6294f9fdc 100644 --- a/tactics/term_dnet.ml +++ b/tactics/term_dnet.ml @@ -351,7 +351,7 @@ struct (fun id acc -> let c_id = Opt.reduce (Ident.constr_of id) in let (ctx,wc) = - try Termops.align_prod_letin whole_c c_id + try Termops.align_prod_letin Evd.empty (EConstr.of_constr whole_c) (EConstr.of_constr c_id) (** FIXME *) with Invalid_argument _ -> [],c_id in let wc,whole_c = if Opt.direction then whole_c,wc else wc,whole_c in try diff --git a/toplevel/assumptions.ml b/toplevel/assumptions.ml index 8865cd646..deb2ed3e0 100644 --- a/toplevel/assumptions.ml +++ b/toplevel/assumptions.ml @@ -144,6 +144,27 @@ let label_of = function | ConstructRef ((kn,_),_) -> pi3 (repr_mind kn) | VarRef id -> Label.of_id id +let fold_constr_with_full_binders g f n acc c = + let open Context.Rel.Declaration in + match kind_of_term 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 + | 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 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 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 rec traverse current ctx accu t = match kind_of_term t with | Var id -> let body () = id |> Global.lookup_named |> NamedDecl.get_value in @@ -166,10 +187,10 @@ let rec traverse current ctx accu t = match kind_of_term t with traverse_object ~inhabits:(current,ctx,Vars.subst1 mkProp oty) accu body (ConstRef kn) | _ -> - Termops.fold_constr_with_full_binders + fold_constr_with_full_binders Context.Rel.add (traverse current) ctx accu t end -| _ -> Termops.fold_constr_with_full_binders +| _ -> fold_constr_with_full_binders Context.Rel.add (traverse current) ctx accu t and traverse_object ?inhabits (curr, data, ax2ty) body obj = diff --git a/toplevel/class.ml b/toplevel/class.ml index 0dc799014..46854e5c0 100644 --- a/toplevel/class.ml +++ b/toplevel/class.ml @@ -85,7 +85,7 @@ let uniform_cond nargs lt = let rec aux = function | (0,[]) -> true | (n,t::l) -> - let t = strip_outer_cast t in + let t = strip_outer_cast Evd.empty (EConstr.of_constr t) (** FIXME *) in isRel t && Int.equal (destRel t) n && aux ((n-1),l) | _ -> false in diff --git a/toplevel/command.ml b/toplevel/command.ml index ef918ef8d..62bbd4b97 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -685,7 +685,7 @@ let is_recursive mie = let rec is_recursive_constructor lift typ = match Term.kind_of_term typ with | Prod (_,arg,rest) -> - Termops.dependent (mkRel lift) arg || + not (EConstr.Vars.noccurn Evd.empty (** FIXME *) lift (EConstr.of_constr arg)) || is_recursive_constructor (lift+1) rest | LetIn (na,b,t,rest) -> is_recursive_constructor (lift+1) rest | _ -> false @@ -813,11 +813,11 @@ let warn_non_full_mutual = (fun (x,xge,y,yge,isfix,rest) -> non_full_mutual_message x xge y yge isfix rest) -let check_mutuality env isfix fixl = +let check_mutuality env evd isfix fixl = let names = List.map fst fixl in let preorder = List.map (fun (id,def) -> - (id, List.filter (fun id' -> not (Id.equal id id') && occur_var env id' def) names)) + (id, List.filter (fun id' -> not (Id.equal id id') && occur_var env evd id' (EConstr.of_constr def)) names)) fixl in let po = partial_order Id.equal preorder in match List.filter (function (_,Inr _) -> true | _ -> false) po with @@ -1144,7 +1144,7 @@ let check_recursive isfix env evd (fixnames,fixdefs,_) = check_evars_are_solved env evd (Evd.empty,evd); if List.for_all Option.has_some fixdefs then begin let fixdefs = List.map Option.get fixdefs in - check_mutuality env isfix (List.combine fixnames fixdefs) + check_mutuality env evd isfix (List.combine fixnames fixdefs) end let interp_fixpoint l ntns = diff --git a/toplevel/command.mli b/toplevel/command.mli index 616afb91f..fae783ef0 100644 --- a/toplevel/command.mli +++ b/toplevel/command.mli @@ -170,7 +170,7 @@ val do_cofixpoint : (** Utils *) -val check_mutuality : Environ.env -> bool -> (Id.t * types) list -> unit +val check_mutuality : Environ.env -> Evd.evar_map -> bool -> (Id.t * types) list -> unit val declare_fix : ?opaque:bool -> definition_kind -> Universes.universe_binders -> Univ.universe_context -> Id.t -> Safe_typing.private_constants Entries.proof_output -> types -> Impargs.manual_implicits -> global_reference diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index 891662b93..bfe86053e 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -1090,7 +1090,7 @@ let error_ill_formed_inductive env c v = let error_ill_formed_constructor env id c v nparams nargs = let pv = pr_lconstr_env env Evd.empty v in - let atomic = Int.equal (nb_prod c) 0 in + let atomic = Int.equal (nb_prod Evd.empty (EConstr.of_constr c)) (** FIXME *) 0 in str "The type of constructor" ++ brk(1,1) ++ pr_id id ++ brk(1,1) ++ str "is not valid;" ++ brk(1,1) ++ strbrk (if atomic then "it must be " else "its conclusion must be ") ++ diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml index 48521a8e5..3f818f960 100644 --- a/toplevel/indschemes.ml +++ b/toplevel/indschemes.ml @@ -313,7 +313,7 @@ let warn_cannot_build_congruence = strbrk "Cannot build congruence scheme because eq is not found") let declare_congr_scheme ind = - if Hipattern.is_equality_type (mkInd ind) then begin + if Hipattern.is_equality_type Evd.empty (mkInd ind) (** FIXME *) then begin if try Coqlib.check_required_library Coqlib.logic_module_name; true with e when CErrors.noncritical e -> false @@ -472,7 +472,7 @@ let build_combined_scheme env schemes = let (c, t) = List.hd defs in let ctx, ind, nargs = find_inductive t in (* Number of clauses, including the predicates quantification *) - let prods = nb_prod t - (nargs + 1) in + let prods = nb_prod Evd.empty (EConstr.of_constr t) - (nargs + 1) (** FIXME *) in let coqand = Coqlib.build_coq_and () and coqconj = Coqlib.build_coq_conj () in let relargs = rel_vect 0 prods in let concls = List.rev_map diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml index 9ada04317..1d5e4a2fa 100644 --- a/toplevel/obligations.ml +++ b/toplevel/obligations.ml @@ -145,7 +145,7 @@ let rec chop_product n t = if Int.equal n 0 then Some t else match kind_of_term t with - | Prod (_, _, b) -> if noccurn 1 b then chop_product (pred n) (Termops.pop b) else None + | Prod (_, _, b) -> if noccurn 1 b then chop_product (pred n) (Termops.pop (EConstr.of_constr b)) else None | _ -> None let evar_dependencies evm oev = @@ -396,7 +396,7 @@ let subst_deps expand obls deps t = (Vars.replace_vars (List.map (fun (n, (_, b)) -> n, b) osubst) t) let rec prod_app t n = - match kind_of_term (Termops.strip_outer_cast t) with + match kind_of_term (Termops.strip_outer_cast Evd.empty (EConstr.of_constr t)) (** FIXME *) with | Prod (_,_,b) -> subst1 n b | LetIn (_, b, t, b') -> prod_app (subst1 b b') n | _ -> @@ -521,7 +521,7 @@ let compute_possible_guardness_evidences (n,_) fixbody fixtype = but doing it properly involves delta-reduction, and it finally doesn't seem to worth the effort (except for huge mutual fixpoints ?) *) - let m = Termops.nb_prod fixtype in + let m = Termops.nb_prod Evd.empty (EConstr.of_constr fixtype) (** FIXME *) in let ctx = fst (decompose_prod_n_assum m fixtype) in List.map_i (fun i _ -> i) 0 ctx diff --git a/toplevel/record.ml b/toplevel/record.ml index c43b32762..7dee4aae0 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -374,7 +374,7 @@ let structure_signature ctx = let evm = Sigma.to_evar_map evm in let new_tl = Util.List.map_i (fun pos decl -> - RelDecl.map_type (fun t -> Termops.replace_term (mkRel pos) (mkEvar(ev,[||])) t) decl) 1 tl in + RelDecl.map_type (fun t -> Termops.replace_term evm (EConstr.mkRel pos) (EConstr.mkEvar(ev,[||])) (EConstr.of_constr t)) decl) 1 tl in deps_to_evar evm new_tl in deps_to_evar Evd.empty (List.rev ctx) diff --git a/toplevel/search.ml b/toplevel/search.ml index d319b2419..c0bcc403c 100644 --- a/toplevel/search.ml +++ b/toplevel/search.ml @@ -112,7 +112,7 @@ let generic_search glnumopt fn = (** This function tries to see whether the conclusion matches a pattern. *) (** FIXME: this is quite dummy, we may find a more efficient algorithm. *) let rec pattern_filter pat ref env typ = - let typ = Termops.strip_outer_cast typ in + let typ = Termops.strip_outer_cast Evd.empty (EConstr.of_constr typ) (** FIXME *) in if Constr_matching.is_matching env Evd.empty pat typ then true else match kind_of_term typ with | Prod (_, _, typ) @@ -120,7 +120,7 @@ let rec pattern_filter pat ref env typ = | _ -> false let rec head_filter pat ref env typ = - let typ = Termops.strip_outer_cast typ in + let typ = Termops.strip_outer_cast Evd.empty (EConstr.of_constr typ) (** FIXME *) in if Constr_matching.is_matching_head env Evd.empty pat typ then true else match kind_of_term typ with | Prod (_, _, typ) diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index ede88399e..bbbdbdb67 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -107,7 +107,7 @@ let show_intro all = let {Evd.it=gls ; sigma=sigma; } = Proof.V82.subgoals pf in if not (List.is_empty gls) then begin let gl = {Evd.it=List.hd gls ; sigma = sigma; } in - let l,_= decompose_prod_assum (Termops.strip_outer_cast (pf_concl gl)) in + let l,_= decompose_prod_assum (Termops.strip_outer_cast (project gl) (EConstr.of_constr (pf_concl gl))) in if all then let lid = Tactics.find_intro_names l gl in Feedback.msg_notice (hov 0 (prlist_with_sep spc pr_id lid)) |