diff options
Diffstat (limited to 'pretyping')
-rw-r--r-- | pretyping/cases.ml | 1 | ||||
-rw-r--r-- | pretyping/coercion.ml | 6 | ||||
-rw-r--r-- | pretyping/evarconv.ml | 1 | ||||
-rw-r--r-- | pretyping/evardefine.ml | 209 | ||||
-rw-r--r-- | pretyping/evardefine.mli | 46 | ||||
-rw-r--r-- | pretyping/evarutil.ml | 899 | ||||
-rw-r--r-- | pretyping/evarutil.mli | 253 | ||||
-rw-r--r-- | pretyping/pretyping.ml | 18 | ||||
-rw-r--r-- | pretyping/pretyping.mli | 4 | ||||
-rw-r--r-- | pretyping/pretyping.mllib | 4 | ||||
-rw-r--r-- | pretyping/reductionops.ml | 30 | ||||
-rw-r--r-- | pretyping/typeclasses.ml | 2 | ||||
-rw-r--r-- | pretyping/typing.ml | 4 | ||||
-rw-r--r-- | pretyping/unification.ml | 1 |
14 files changed, 291 insertions, 1187 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 8a55a7aaa..c3968f896 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -25,6 +25,7 @@ open Glob_ops open Retyping open Pretype_errors open Evarutil +open Evardefine open Evarsolve open Evarconv open Evd diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index 57b273d0d..9d0f391e4 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -245,7 +245,7 @@ and coerce loc env evdref (x : Term.constr) (y : Term.constr) | Lambda (n, t, t') -> c, t' (*| Prod (n, t, t') -> t'*) | Evar (k, args) -> - let (evs, t) = Evarutil.define_evar_as_lambda env !evdref (k,args) in + let (evs, t) = Evardefine.define_evar_as_lambda env !evdref (k,args) in evdref := evs; let (n, dom, rng) = destLambda t in let dom = whd_evar !evdref dom in @@ -375,7 +375,7 @@ let inh_app_fun_core env evd j = match kind_of_term t with | Prod (_,_,_) -> (evd,j) | Evar ev -> - let (evd',t) = define_evar_as_product evd ev in + let (evd',t) = Evardefine.define_evar_as_product evd ev in (evd',{ uj_val = j.uj_val; uj_type = t }) | _ -> try let t,p = @@ -416,7 +416,7 @@ let inh_coerce_to_sort loc env evd j = match kind_of_term typ with | Sort s -> (evd,{ utj_val = j.uj_val; utj_type = s }) | Evar ev when not (is_defined evd (fst ev)) -> - let (evd',s) = define_evar_as_sort env evd ev in + let (evd',s) = Evardefine.define_evar_as_sort env evd ev in (evd',{ utj_val = j.uj_val; utj_type = s }) | _ -> inh_tosort_force loc env evd j diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 489a8a729..08973a05c 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -18,6 +18,7 @@ open Termops open Environ open Recordops open Evarutil +open Evardefine open Evarsolve open Globnames open Evd diff --git a/pretyping/evardefine.ml b/pretyping/evardefine.ml new file mode 100644 index 000000000..ef3a3f525 --- /dev/null +++ b/pretyping/evardefine.ml @@ -0,0 +1,209 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Errors +open Util +open Pp +open Names +open Term +open Vars +open Termops +open Namegen +open Pre_env +open Environ +open Evd +open Evarutil +open Pretype_errors +open Sigma.Notations + +let new_evar_unsafe env evd ?src ?filter ?candidates ?store ?naming ?principal typ = + let evd = Sigma.Unsafe.of_evar_map evd in + let Sigma (evk, evd, _) = new_evar env evd ?src ?filter ?candidates ?store ?naming ?principal typ in + (Sigma.to_evar_map evd, evk) + +let env_nf_evar sigma env = + let open Context.Rel.Declaration in + process_rel_context + (fun d e -> push_rel (map_constr (nf_evar sigma) d) e) env + +let env_nf_betaiotaevar sigma env = + let open Context.Rel.Declaration in + process_rel_context + (fun d e -> + push_rel (map_constr (Reductionops.nf_betaiota sigma) d) e) env + +(****************************************) +(* Operations on value/type constraints *) +(****************************************) + +type type_constraint = types option + +type val_constraint = constr option + +(* Old comment... + * Basically, we have the following kind of constraints (in increasing + * strength order): + * (false,(None,None)) -> no constraint at all + * (true,(None,None)) -> we must build a judgement which _TYPE is a kind + * (_,(None,Some ty)) -> we must build a judgement which _TYPE is ty + * (_,(Some v,_)) -> we must build a judgement which _VAL is v + * Maybe a concrete datatype would be easier to understand. + * We differentiate (true,(None,None)) from (_,(None,Some Type)) + * because otherwise Case(s) would be misled, as in + * (n:nat) Case n of bool [_]nat end would infer the predicate Type instead + * of Set. + *) + +(* The empty type constraint *) +let empty_tycon = None + +(* Builds a type constraint *) +let mk_tycon ty = Some ty + +(* Constrains the value of a type *) +let empty_valcon = None + +(* Builds a value constraint *) +let mk_valcon c = Some c + +let idx = Namegen.default_dependent_ident + +(* Refining an evar to a product *) + +let define_pure_evar_as_product evd evk = + let open Context.Named.Declaration in + let evi = Evd.find_undefined evd evk in + let evenv = evar_env evi in + let id = next_ident_away idx (ids_of_named_context (evar_context evi)) in + let concl = Reductionops.whd_betadeltaiota evenv evd evi.evar_concl in + let s = destSort concl in + let evd1,(dom,u1) = + let evd = Sigma.Unsafe.of_evar_map evd in + let Sigma (e, evd1, _) = new_type_evar evenv evd univ_flexible_alg ~filter:(evar_filter evi) in + (Sigma.to_evar_map evd1, e) + in + let evd2,rng = + let newenv = push_named (LocalAssum (id, dom)) evenv in + let src = evar_source evk evd1 in + let filter = Filter.extend 1 (evar_filter evi) in + if is_prop_sort s then + (* Impredicative product, conclusion must fall in [Prop]. *) + new_evar_unsafe newenv evd1 concl ~src ~filter + else + let status = univ_flexible_alg in + let evd3, (rng, srng) = + let evd1 = Sigma.Unsafe.of_evar_map evd1 in + let Sigma (e, evd3, _) = new_type_evar newenv evd1 status ~src ~filter in + (Sigma.to_evar_map evd3, e) + in + let prods = Univ.sup (univ_of_sort u1) (univ_of_sort srng) in + let evd3 = Evd.set_leq_sort evenv evd3 (Type prods) s in + evd3, rng + in + let prod = mkProd (Name id, dom, subst_var id rng) in + let evd3 = Evd.define evk prod evd2 in + evd3,prod + +(* Refine an applied evar to a product and returns its instantiation *) + +let define_evar_as_product evd (evk,args) = + let evd,prod = define_pure_evar_as_product evd evk in + (* Quick way to compute the instantiation of evk with args *) + let na,dom,rng = destProd prod in + let evdom = mkEvar (fst (destEvar dom), args) in + let evrngargs = Array.cons (mkRel 1) (Array.map (lift 1) args) in + let evrng = mkEvar (fst (destEvar rng), evrngargs) in + evd,mkProd (na, evdom, evrng) + +(* Refine an evar with an abstraction + + I.e., solve x1..xq |- ?e:T(x1..xq) with e:=λy:A.?e'[x1..xq,y] where: + - either T(x1..xq) = πy:A(x1..xq).B(x1..xq,y) + or T(x1..xq) = ?d[x1..xq] and we define ?d := πy:?A.?B + with x1..xq |- ?A:Type and x1..xq,y |- ?B:Type + - x1..xq,y:A |- ?e':B +*) + +let define_pure_evar_as_lambda env evd evk = + let open Context.Named.Declaration in + let evi = Evd.find_undefined evd evk in + let evenv = evar_env evi in + let typ = Reductionops.whd_betadeltaiota evenv evd (evar_concl evi) in + let evd1,(na,dom,rng) = match kind_of_term typ with + | Prod (na,dom,rng) -> (evd,(na,dom,rng)) + | Evar ev' -> let evd,typ = define_evar_as_product evd ev' in evd,destProd typ + | _ -> error_not_product_loc Loc.ghost env evd typ in + let avoid = ids_of_named_context (evar_context evi) in + let id = + next_name_away_with_default_using_types "x" na avoid (Reductionops.whd_evar evd dom) in + let newenv = push_named (LocalAssum (id, dom)) evenv in + let filter = Filter.extend 1 (evar_filter evi) in + let src = evar_source evk evd1 in + let evd2,body = new_evar_unsafe newenv evd1 ~src (subst1 (mkVar id) rng) ~filter in + let lam = mkLambda (Name id, dom, subst_var id body) in + Evd.define evk lam evd2, lam + +let define_evar_as_lambda env evd (evk,args) = + let evd,lam = define_pure_evar_as_lambda env evd evk in + (* Quick way to compute the instantiation of evk with args *) + let na,dom,body = destLambda lam in + let evbodyargs = Array.cons (mkRel 1) (Array.map (lift 1) args) in + let evbody = mkEvar (fst (destEvar body), evbodyargs) in + evd,mkLambda (na, dom, evbody) + +let rec evar_absorb_arguments env evd (evk,args as ev) = function + | [] -> evd,ev + | a::l -> + (* TODO: optimize and avoid introducing intermediate evars *) + let evd,lam = define_pure_evar_as_lambda env evd evk in + let _,_,body = destLambda lam in + let evk = fst (destEvar body) in + evar_absorb_arguments env evd (evk, Array.cons a args) l + +(* Refining an evar to a sort *) + +let define_evar_as_sort env evd (ev,args) = + let evd, u = new_univ_variable univ_rigid evd in + let evi = Evd.find_undefined evd ev in + let s = Type u in + let concl = Reductionops.whd_betadeltaiota (evar_env evi) evd evi.evar_concl in + let sort = destSort concl in + let evd' = Evd.define ev (mkSort s) evd in + Evd.set_leq_sort env evd' (Type (Univ.super u)) sort, s + +(* Propagation of constraints through application and abstraction: + Given a type constraint on a functional term, returns the type + constraint on its domain and codomain. If the input constraint is + an evar instantiate it with the product of 2 new evars. *) + +let split_tycon loc env evd tycon = + let rec real_split evd c = + let t = Reductionops.whd_betadeltaiota env evd c in + match kind_of_term t with + | Prod (na,dom,rng) -> evd, (na, dom, rng) + | Evar ev (* ev is undefined because of whd_betadeltaiota *) -> + let (evd',prod) = define_evar_as_product evd ev in + let (_,dom,rng) = destProd prod in + evd',(Anonymous, dom, rng) + | App (c,args) when isEvar c -> + let (evd',lam) = define_evar_as_lambda env evd (destEvar c) in + real_split evd' (mkApp (lam,args)) + | _ -> error_not_product_loc loc env evd c + in + match tycon with + | None -> evd,(Anonymous,None,None) + | Some c -> + let evd', (n, dom, rng) = real_split evd c in + evd', (n, mk_tycon dom, mk_tycon rng) + +let valcon_of_tycon x = x +let lift_tycon n = Option.map (lift n) + +let pr_tycon env = function + None -> str "None" + | Some t -> Termops.print_constr_env env t diff --git a/pretyping/evardefine.mli b/pretyping/evardefine.mli new file mode 100644 index 000000000..07b0e69d9 --- /dev/null +++ b/pretyping/evardefine.mli @@ -0,0 +1,46 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Names +open Term +open Evd +open Environ + +val env_nf_evar : evar_map -> env -> env +val env_nf_betaiotaevar : evar_map -> env -> env + +type type_constraint = types option +type val_constraint = constr option + +val empty_tycon : type_constraint +val mk_tycon : constr -> type_constraint +val empty_valcon : val_constraint +val mk_valcon : constr -> val_constraint + +(** Instantiate an evar by as many lambda's as needed so that its arguments + are moved to the evar substitution (i.e. turn [?x[vars1:=args1] args] into + [?y[vars1:=args1,vars:=args]] with + [vars1 |- ?x:=\vars.?y[vars1:=vars1,vars:=vars]] *) +val evar_absorb_arguments : env -> evar_map -> existential -> constr list -> + evar_map * existential + +val split_tycon : + Loc.t -> env -> evar_map -> type_constraint -> + evar_map * (Name.t * type_constraint * type_constraint) + +val valcon_of_tycon : type_constraint -> val_constraint +val lift_tycon : int -> type_constraint -> type_constraint + +val define_evar_as_product : evar_map -> existential -> evar_map * types +val define_evar_as_lambda : env -> evar_map -> existential -> evar_map * types +val define_evar_as_sort : env -> evar_map -> existential -> evar_map * sorts + +(** {6 debug pretty-printer:} *) + +val pr_tycon : env -> type_constraint -> Pp.std_ppcmds + diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml deleted file mode 100644 index ab70de057..000000000 --- a/pretyping/evarutil.ml +++ /dev/null @@ -1,899 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -open Errors -open Util -open Pp -open Names -open Term -open Vars -open Termops -open Namegen -open Pre_env -open Environ -open Evd -open Reductionops -open Pretype_errors -open Sigma.Notations - -(** Combinators *) - -let evd_comb0 f evdref = - let (evd',x) = f !evdref in - evdref := evd'; - x - -let evd_comb1 f evdref x = - let (evd',y) = f !evdref x in - evdref := evd'; - y - -let evd_comb2 f evdref x y = - let (evd',z) = f !evdref x y in - evdref := evd'; - z - -let e_new_global evdref x = - evd_comb1 (Evd.fresh_global (Global.env())) evdref x - -let new_global evd x = - Sigma.fresh_global (Global.env()) evd x - -(****************************************************) -(* Expanding/testing/exposing existential variables *) -(****************************************************) - -(* flush_and_check_evars fails if an existential is undefined *) - -exception Uninstantiated_evar of existential_key - -let rec flush_and_check_evars sigma c = - match kind_of_term c with - | Evar (evk,_ as ev) -> - (match existential_opt_value sigma ev with - | None -> raise (Uninstantiated_evar evk) - | Some c -> flush_and_check_evars sigma c) - | _ -> map_constr (flush_and_check_evars sigma) c - -(* let nf_evar_key = Profile.declare_profile "nf_evar" *) -(* let nf_evar = Profile.profile2 nf_evar_key Reductionops.nf_evar *) -let nf_evar = Reductionops.nf_evar -let j_nf_evar sigma j = - { uj_val = nf_evar sigma j.uj_val; - uj_type = nf_evar sigma j.uj_type } -let j_nf_betaiotaevar sigma j = - { uj_val = nf_evar sigma j.uj_val; - uj_type = Reductionops.nf_betaiota sigma j.uj_type } -let jl_nf_evar sigma jl = List.map (j_nf_evar sigma) jl -let jv_nf_betaiotaevar sigma jl = - Array.map (j_nf_betaiotaevar sigma) jl -let jv_nf_evar sigma = Array.map (j_nf_evar sigma) -let tj_nf_evar sigma {utj_val=v;utj_type=t} = - {utj_val=nf_evar sigma v;utj_type=t} - -let env_nf_evar sigma env = - let open Context.Rel.Declaration in - process_rel_context - (fun d e -> push_rel (map_constr (nf_evar sigma) d) e) env - -let env_nf_betaiotaevar sigma env = - let open Context.Rel.Declaration in - process_rel_context - (fun d e -> - push_rel (map_constr (Reductionops.nf_betaiota sigma) d) e) env - -let nf_evars_universes evm = - Universes.nf_evars_and_universes_opt_subst (Reductionops.safe_evar_value evm) - (Evd.universe_subst evm) - -let nf_evars_and_universes evm = - let evm = Evd.nf_constraints evm in - evm, nf_evars_universes evm - -let e_nf_evars_and_universes evdref = - evdref := Evd.nf_constraints !evdref; - nf_evars_universes !evdref, Evd.universe_subst !evdref - -let nf_evar_map_universes evm = - let evm = Evd.nf_constraints evm in - let subst = Evd.universe_subst evm in - if Univ.LMap.is_empty subst then evm, nf_evar evm - else - let f = nf_evars_universes evm in - Evd.raw_map (fun _ -> map_evar_info f) evm, f - -let nf_named_context_evar sigma ctx = - Context.Named.map (nf_evar sigma) ctx - -let nf_rel_context_evar sigma ctx = - Context.Rel.map (nf_evar sigma) ctx - -let nf_env_evar sigma env = - let nc' = nf_named_context_evar sigma (Environ.named_context env) in - let rel' = nf_rel_context_evar sigma (Environ.rel_context env) in - push_rel_context rel' (reset_with_named_context (val_of_named_context nc') env) - -let nf_evar_info evc info = map_evar_info (nf_evar evc) info - -let nf_evar_map evm = - Evd.raw_map (fun _ evi -> nf_evar_info evm evi) evm - -let nf_evar_map_undefined evm = - Evd.raw_map_undefined (fun _ evi -> nf_evar_info evm evi) evm - -(*-------------------*) -(* Auxiliary functions for the conversion algorithms modulo evars - *) - -(* A probably faster though more approximative variant of - [has_undefined (nf_evar c)]: instances are not substituted and - maybe an evar occurs in an instance and it would disappear by - instantiation *) - -let has_undefined_evars evd t = - let rec has_ev t = - match kind_of_term t with - | Evar (ev,args) -> - (match evar_body (Evd.find evd ev) with - | Evar_defined c -> - has_ev c; Array.iter has_ev args - | Evar_empty -> - raise NotInstantiatedEvar) - | _ -> iter_constr has_ev t in - try let _ = has_ev t in false - with (Not_found | NotInstantiatedEvar) -> true - -let is_ground_term evd t = - not (has_undefined_evars evd t) - -let is_ground_env evd env = - let open Context.Rel.Declaration in - let is_ground_rel_decl = function - | LocalDef (_,b,_) -> is_ground_term evd b - | _ -> true in - let open Context.Named.Declaration in - let is_ground_named_decl = function - | LocalDef (_,b,_) -> is_ground_term evd b - | _ -> true in - List.for_all is_ground_rel_decl (rel_context env) && - List.for_all is_ground_named_decl (named_context env) - -(* Memoization is safe since evar_map and environ are applicative - structures *) -let memo f = - let m = ref None in - fun x y -> match !m with - | Some (x', y', r) when x == x' && y == y' -> r - | _ -> let r = f x y in m := Some (x, y, r); r - -let is_ground_env = memo is_ground_env - -(* Return the head evar if any *) - -exception NoHeadEvar - -let head_evar = - let rec hrec c = match kind_of_term c with - | Evar (evk,_) -> evk - | Case (_,_,c,_) -> hrec c - | App (c,_) -> hrec c - | Cast (c,_,_) -> hrec c - | _ -> raise NoHeadEvar - in - hrec - -(* Expand head evar if any (currently consider only applications but I - guess it should consider Case too) *) - -let whd_head_evar_stack sigma c = - let rec whrec (c, l as s) = - match kind_of_term c with - | Evar (evk,args as ev) -> - let v = - try Some (existential_value sigma ev) - with NotInstantiatedEvar | Not_found -> None in - begin match v with - | None -> s - | Some c -> whrec (c, l) - end - | Cast (c,_,_) -> whrec (c, l) - | App (f,args) -> whrec (f, args :: l) - | _ -> s - in - whrec (c, []) - -let whd_head_evar sigma c = - let (f, args) = whd_head_evar_stack sigma c in - (** optim: don't reallocate if empty/singleton *) - match args with - | [] -> f - | [arg] -> mkApp (f, arg) - | _ -> mkApp (f, Array.concat args) - -(**********************) -(* Creating new metas *) -(**********************) - -let meta_counter_summary_name = "meta counter" - -(* Generator of metavariables *) -let new_meta = - let meta_ctr = Summary.ref 0 ~name:meta_counter_summary_name in - fun () -> incr meta_ctr; !meta_ctr - -let mk_new_meta () = mkMeta(new_meta()) - -(* The list of non-instantiated existential declarations (order is important) *) - -let non_instantiated sigma = - let listev = Evd.undefined_map sigma in - Evar.Map.smartmap (fun evi -> nf_evar_info sigma evi) listev - -(************************) -(* Manipulating filters *) -(************************) - -let make_pure_subst evi args = - let open Context.Named.Declaration in - snd (List.fold_right - (fun decl (args,l) -> - match args with - | a::rest -> (rest, (get_id decl, a)::l) - | _ -> anomaly (Pp.str "Instance does not match its signature")) - (evar_filtered_context evi) (Array.rev_to_list args,[])) - -(*------------------------------------* - * functional operations on evar sets * - *------------------------------------*) - -(* [push_rel_context_to_named_context] builds the defining context and the - * initial instance of an evar. If the evar is to be used in context - * - * Gamma = a1 ... an xp ... x1 - * \- named part -/ \- de Bruijn part -/ - * - * then the x1...xp are turned into variables so that the evar is declared in - * context - * - * a1 ... an xp ... x1 - * \----------- named part ------------/ - * - * but used applied to the initial instance "a1 ... an Rel(p) ... Rel(1)" - * so that ev[a1:=a1 ... an:=an xp:=Rel(p) ... x1:=Rel(1)] is correctly typed - * in context Gamma. - * - * Remark 1: The instance is reverted in practice (i.e. Rel(1) comes first) - * Remark 2: If some of the ai or xj are definitions, we keep them in the - * instance. This is necessary so that no unfolding of local definitions - * happens when inferring implicit arguments (consider e.g. the problem - * "x:nat; x':=x; f:forall y, y=y -> Prop |- f _ (refl_equal x')" which - * produces the equation "?y[x,x']=?y[x,x']" =? "x'=x'": we want - * the hole to be instantiated by x', not by x (which would have been - * the case in [invert_definition] if x' had disappeared from the instance). - * Note that at any time, if, in some context env, the instance of - * declaration x:A is t and the instance of definition x':=phi(x) is u, then - * we have the property that u and phi(t) are convertible in env. - *) - -let subst2 subst vsubst c = - substl subst (replace_vars vsubst c) - -let push_rel_context_to_named_context env typ = - (* compute the instances relative to the named context and rel_context *) - let open Context.Named.Declaration in - let ids = List.map get_id (named_context env) in - let inst_vars = List.map mkVar ids in - let inst_rels = List.rev (rel_list 0 (nb_rel env)) in - let replace_var_named_declaration id0 id decl = - let id' = get_id decl in - let id' = if Id.equal id0 id' then id else id' in - let vsubst = [id0 , mkVar id] in - decl |> set_id id' |> map_constr (replace_vars vsubst) - in - let replace_var_named_context id0 id env = - let nc = Environ.named_context env in - let nc' = List.map (replace_var_named_declaration id0 id) nc in - Environ.reset_with_named_context (val_of_named_context nc') env - in - let extract_if_neq id = function - | Anonymous -> None - | Name id' when id_ord id id' = 0 -> None - | Name id' -> Some id' - in - (* move the rel context to a named context and extend the named instance *) - (* with vars of the rel context *) - (* We do keep the instances corresponding to local definition (see above) *) - let (subst, vsubst, _, env) = - Context.Rel.fold_outside - (fun decl (subst, vsubst, avoid, env) -> - let open Context.Rel.Declaration in - let na = get_name decl in - let c = get_value decl in - let t = get_type decl in - let open Context.Named.Declaration in - let id = - (* ppedrot: we want to infer nicer names for the refine tactic, but - keeping at the same time backward compatibility in other code - using this function. For now, we only attempt to preserve the - old behaviour of Program, but ultimately, one should do something - about this whole name generation problem. *) - if Flags.is_program_mode () then next_name_away na avoid - else next_ident_away (id_of_name_using_hdchar env t na) avoid - in - match extract_if_neq id na with - | Some id0 when not (is_section_variable id0) -> - (* spiwack: if [id<>id0], rather than introducing a new - binding named [id], we will keep [id0] (the name given - by the user) and rename [id0] into [id] in the named - context. Unless [id] is a section variable. *) - let subst = List.map (replace_vars [id0,mkVar id]) subst in - let vsubst = (id0,mkVar id)::vsubst in - let d = match c with - | None -> LocalAssum (id0, subst2 subst vsubst t) - | Some c -> LocalDef (id0, subst2 subst vsubst c, subst2 subst vsubst t) - in - let env = replace_var_named_context id0 id env in - (mkVar id0 :: subst, vsubst, id::avoid, push_named d env) - | _ -> - (* spiwack: if [id0] is a section variable renaming it is - incorrect. We revert to a less robust behaviour where - the new binder has name [id]. Which amounts to the same - behaviour than when [id=id0]. *) - let d = match c with - | None -> LocalAssum (id, subst2 subst vsubst t) - | Some c -> LocalDef (id, subst2 subst vsubst c, subst2 subst vsubst t) - in - (mkVar id :: subst, vsubst, id::avoid, push_named d env) - ) - (rel_context env) ~init:([], [], ids, env) in - (named_context_val env, subst2 subst vsubst typ, inst_rels@inst_vars, subst, vsubst) - -(*------------------------------------* - * Entry points to define new evars * - *------------------------------------*) - -let default_source = (Loc.ghost,Evar_kinds.InternalHole) - -let restrict_evar evd evk filter candidates = - let evd = Sigma.to_evar_map evd in - let evd, evk' = Evd.restrict evk filter ?candidates evd in - Sigma.Unsafe.of_pair (evk', Evd.declare_future_goal evk' evd) - -let new_pure_evar_full evd evi = - let evd = Sigma.to_evar_map evd in - let (evd, evk) = Evd.new_evar evd evi in - let evd = Evd.declare_future_goal evk evd in - Sigma.Unsafe.of_pair (evk, evd) - -let new_pure_evar sign evd ?(src=default_source) ?(filter = Filter.identity) ?candidates ?(store = Store.empty) ?naming ?(principal=false) typ = - let evd = Sigma.to_evar_map evd in - let default_naming = Misctypes.IntroAnonymous in - let naming = Option.default default_naming naming in - let evi = { - evar_hyps = sign; - evar_concl = typ; - evar_body = Evar_empty; - evar_filter = filter; - evar_source = src; - evar_candidates = candidates; - evar_extra = store; } - in - let (evd, newevk) = Evd.new_evar evd ~naming evi in - let evd = - if principal then Evd.declare_principal_goal newevk evd - else Evd.declare_future_goal newevk evd - in - Sigma.Unsafe.of_pair (newevk, evd) - -let new_evar_instance sign evd typ ?src ?filter ?candidates ?store ?naming ?principal instance = - assert (not !Flags.debug || - List.distinct (ids_of_named_context (named_context_of_val sign))); - let Sigma (newevk, evd, p) = new_pure_evar sign evd ?src ?filter ?candidates ?store ?naming ?principal typ in - Sigma (mkEvar (newevk,Array.of_list instance), evd, p) - -(* [new_evar] declares a new existential in an env env with type typ *) -(* Converting the env into the sign of the evar to define *) -let new_evar env evd ?src ?filter ?candidates ?store ?naming ?principal typ = - let sign,typ',instance,subst,vsubst = push_rel_context_to_named_context env typ in - let candidates = Option.map (List.map (subst2 subst vsubst)) candidates in - let instance = - match filter with - | None -> instance - | Some filter -> Filter.filter_list filter instance in - new_evar_instance sign evd typ' ?src ?filter ?candidates ?store ?naming ?principal instance - -let new_evar_unsafe env evd ?src ?filter ?candidates ?store ?naming ?principal typ = - let evd = Sigma.Unsafe.of_evar_map evd in - let Sigma (evk, evd, _) = new_evar env evd ?src ?filter ?candidates ?store ?naming ?principal typ in - (Sigma.to_evar_map evd, evk) - -let new_type_evar env evd ?src ?filter ?naming ?principal rigid = - let Sigma (s, evd', p) = Sigma.new_sort_variable rigid evd in - let Sigma (e, evd', q) = new_evar env evd' ?src ?filter ?naming ?principal (mkSort s) in - Sigma ((e, s), evd', p +> q) - -let e_new_type_evar env evdref ?src ?filter ?naming ?principal rigid = - let sigma = Sigma.Unsafe.of_evar_map !evdref in - let Sigma (c, sigma, _) = new_type_evar env sigma ?src ?filter ?naming ?principal rigid in - let sigma = Sigma.to_evar_map sigma in - evdref := sigma; - c - -let new_Type ?(rigid=Evd.univ_flexible) env evd = - let Sigma (s, sigma, p) = Sigma.new_sort_variable rigid evd in - Sigma (mkSort s, sigma, p) - -let e_new_Type ?(rigid=Evd.univ_flexible) env evdref = - let evd', s = new_sort_variable rigid !evdref in - evdref := evd'; mkSort s - - (* The same using side-effect *) -let e_new_evar env evdref ?(src=default_source) ?filter ?candidates ?store ?naming ?principal ty = - let (evd',ev) = new_evar_unsafe env !evdref ~src:src ?filter ?candidates ?store ?naming ?principal ty in - evdref := evd'; - ev - -(* This assumes an evar with identity instance and generalizes it over only - the De Bruijn part of the context *) -let generalize_evar_over_rels sigma (ev,args) = - let evi = Evd.find sigma ev in - let sign = named_context_of_val evi.evar_hyps in - List.fold_left2 - (fun (c,inst as x) a d -> - if isRel a then (mkNamedProd_or_LetIn d c,a::inst) else x) - (evi.evar_concl,[]) (Array.to_list args) sign - -(************************************) -(* Removing a dependency in an evar *) -(************************************) - -type clear_dependency_error = -| OccurHypInSimpleClause of Id.t option -| EvarTypingBreak of existential - -exception ClearDependencyError of Id.t * clear_dependency_error - -let cleared = Store.field () - -exception Depends of Id.t - -let rec check_and_clear_in_constr env evdref err ids c = - (* returns a new constr where all the evars have been 'cleaned' - (ie the hypotheses ids have been removed from the contexts of - evars) *) - let check id' = - if Id.Set.mem id' ids then - raise (ClearDependencyError (id',err)) - in - match kind_of_term c with - | Var id' -> - check id'; c - - | ( Const _ | Ind _ | Construct _ ) -> - let vars = Environ.vars_of_global env c in - Id.Set.iter check vars; c - - | Evar (evk,l as ev) -> - if Evd.is_defined !evdref evk then - (* If evk is already defined we replace it by its definition *) - let nc = whd_evar !evdref c in - (check_and_clear_in_constr env evdref err ids nc) - else - (* We check for dependencies to elements of ids in the - evar_info corresponding to e and in the instance of - arguments. Concurrently, we build a new evar - corresponding to e where hypotheses of ids have been - removed *) - let evi = Evd.find_undefined !evdref evk in - let ctxt = Evd.evar_filtered_context evi in - let (rids,filter) = - List.fold_right2 - (fun h a (ri,filter) -> - try - (* 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 - (* 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 - then raise (Depends id) - in - let () = Id.Map.iter check ri in - (* No dependency at all, we can keep this ev's context hyp *) - (ri, true::filter) - with Depends id -> let open Context.Named.Declaration in - (Id.Map.add (get_id h) id ri, false::filter)) - ctxt (Array.to_list l) (Id.Map.empty,[]) in - (* Check if some rid to clear in the context of ev has dependencies - in the type of ev and adjust the source of the dependency *) - let _nconcl = - try - let nids = Id.Map.domain rids in - check_and_clear_in_constr env evdref (EvarTypingBreak ev) nids (evar_concl evi) - with ClearDependencyError (rid,err) -> - raise (ClearDependencyError (Id.Map.find rid rids,err)) in - - if Id.Map.is_empty rids then c - else - let origfilter = Evd.evar_filter evi in - let filter = Evd.Filter.apply_subfilter origfilter filter in - let evd = Sigma.Unsafe.of_evar_map !evdref in - let Sigma (_, evd, _) = restrict_evar evd evk filter None in - let evd = Sigma.to_evar_map evd in - evdref := evd; - (* spiwack: hacking session to mark the old [evk] as having been "cleared" *) - let evi = Evd.find !evdref evk in - let extra = evi.evar_extra in - let extra' = Store.set extra cleared true in - let evi' = { evi with evar_extra = extra' } in - evdref := Evd.add !evdref evk evi' ; - (* spiwack: /hacking session *) - whd_evar !evdref c - - | _ -> map_constr (check_and_clear_in_constr env evdref err ids) c - -let clear_hyps_in_evi_main env evdref hyps terms ids = - (* clear_hyps_in_evi erases hypotheses ids in hyps, checking if some - hypothesis does not depend on a element of ids, and erases ids in - the contexts of the evars occurring in evi *) - let terms = - List.map (check_and_clear_in_constr env evdref (OccurHypInSimpleClause None) ids) terms in - let nhyps = - let open Context.Named.Declaration in - let check_context decl = - let err = OccurHypInSimpleClause (Some (get_id decl)) in - map_constr (check_and_clear_in_constr env evdref err ids) decl - in - let check_value vk = match force_lazy_val vk with - | None -> vk - | Some (_, d) -> - if (Id.Set.for_all (fun e -> not (Id.Set.mem e d)) ids) then - (* v does depend on any of ids, it's ok *) - vk - else - (* v depends on one of the cleared hyps: - we forget the computed value *) - dummy_lazy_val () - in - remove_hyps ids check_context check_value hyps - in - (nhyps,terms) - -let clear_hyps_in_evi env evdref hyps concl ids = - match clear_hyps_in_evi_main env evdref hyps [concl] ids with - | (nhyps,[nconcl]) -> (nhyps,nconcl) - | _ -> assert false - -let clear_hyps2_in_evi env evdref hyps t concl ids = - match clear_hyps_in_evi_main env evdref hyps [t;concl] ids with - | (nhyps,[t;nconcl]) -> (nhyps,t,nconcl) - | _ -> assert false - -(* spiwack: a few functions to gather evars on which goals depend. *) -let queue_set q is_dependent set = - Evar.Set.iter (fun a -> Queue.push (is_dependent,a) q) set -let queue_term q is_dependent c = - queue_set q is_dependent (evars_of_term c) - -let process_dependent_evar q acc evm is_dependent e = - let evi = Evd.find evm e in - (* Queues evars appearing in the types of the goal (conclusion, then - hypotheses), they are all dependent. *) - queue_term q true evi.evar_concl; - List.iter begin fun decl -> - let open Context.Named.Declaration in - queue_term q true (get_type decl); - match decl with - | LocalAssum _ -> () - | LocalDef (_,b,_) -> queue_term q true b - end (Environ.named_context_of_val evi.evar_hyps); - match evi.evar_body with - | Evar_empty -> - if is_dependent then Evar.Map.add e None acc else acc - | Evar_defined b -> - let subevars = evars_of_term b in - (* evars appearing in the definition of an evar [e] are marked - as dependent when [e] is dependent itself: if [e] is a - non-dependent goal, then, unless they are reach from another - path, these evars are just other non-dependent goals. *) - queue_set q is_dependent subevars; - if is_dependent then Evar.Map.add e (Some subevars) acc else acc - -let gather_dependent_evars q evm = - let acc = ref Evar.Map.empty in - while not (Queue.is_empty q) do - let (is_dependent,e) = Queue.pop q in - (* checks if [e] has already been added to [!acc] *) - begin if not (Evar.Map.mem e !acc) then - acc := process_dependent_evar q !acc evm is_dependent e - end - done; - !acc - -let gather_dependent_evars evm l = - let q = Queue.create () in - List.iter (fun a -> Queue.add (false,a) q) l; - gather_dependent_evars q evm - -(* /spiwack *) - -(** The following functions return the set of undefined evars - contained in the object, the defined evars being traversed. - This is roughly a combination of the previous functions and - [nf_evar]. *) - -let undefined_evars_of_term evd t = - let rec evrec acc c = - match kind_of_term c with - | Evar (n, l) -> - let acc = Array.fold_left evrec acc l in - (try match (Evd.find evd n).evar_body with - | Evar_empty -> Evar.Set.add n acc - | Evar_defined c -> evrec acc c - with Not_found -> anomaly ~label:"undefined_evars_of_term" (Pp.str "evar not found")) - | _ -> fold_constr evrec acc c - in - evrec Evar.Set.empty t - -let undefined_evars_of_named_context evd nc = - let open Context.Named.Declaration in - Context.Named.fold_outside - (fold (fun c s -> Evar.Set.union s (undefined_evars_of_term evd c))) - nc - ~init:Evar.Set.empty - -let undefined_evars_of_evar_info evd evi = - Evar.Set.union (undefined_evars_of_term evd evi.evar_concl) - (Evar.Set.union - (match evi.evar_body with - | Evar_empty -> Evar.Set.empty - | Evar_defined b -> undefined_evars_of_term evd b) - (undefined_evars_of_named_context evd - (named_context_of_val evi.evar_hyps))) - -(* [check_evars] fails if some unresolved evar remains *) - -let check_evars env initial_sigma sigma c = - let rec proc_rec c = - match kind_of_term c with - | Evar (evk,_ as ev) -> - (match existential_opt_value sigma ev with - | Some c -> proc_rec c - | None -> - if not (Evd.mem initial_sigma evk) then - let (loc,k) = evar_source evk sigma in - match k with - | Evar_kinds.ImplicitArg (gr, (i, id), false) -> () - | _ -> error_unsolvable_implicit loc env sigma evk None) - | _ -> iter_constr proc_rec c - in proc_rec c - -(* spiwack: this is a more complete version of - {!Termops.occur_evar}. The latter does not look recursively into an - [evar_map]. If unification only need to check superficially, tactics - do not have this luxury, and need the more complete version. *) -let occur_evar_upto sigma n c = - let rec occur_rec c = match kind_of_term c with - | Evar (sp,_) when Evar.equal sp n -> raise Occur - | Evar e -> Option.iter occur_rec (existential_opt_value sigma e) - | _ -> iter_constr occur_rec c - in - try occur_rec c; false with Occur -> true - - -(****************************************) -(* Operations on value/type constraints *) -(****************************************) - -type type_constraint = types option - -type val_constraint = constr option - -(* Old comment... - * Basically, we have the following kind of constraints (in increasing - * strength order): - * (false,(None,None)) -> no constraint at all - * (true,(None,None)) -> we must build a judgement which _TYPE is a kind - * (_,(None,Some ty)) -> we must build a judgement which _TYPE is ty - * (_,(Some v,_)) -> we must build a judgement which _VAL is v - * Maybe a concrete datatype would be easier to understand. - * We differentiate (true,(None,None)) from (_,(None,Some Type)) - * because otherwise Case(s) would be misled, as in - * (n:nat) Case n of bool [_]nat end would infer the predicate Type instead - * of Set. - *) - -(* The empty type constraint *) -let empty_tycon = None - -(* Builds a type constraint *) -let mk_tycon ty = Some ty - -(* Constrains the value of a type *) -let empty_valcon = None - -(* Builds a value constraint *) -let mk_valcon c = Some c - -let idx = Namegen.default_dependent_ident - -(* Refining an evar to a product *) - -let define_pure_evar_as_product evd evk = - let open Context.Named.Declaration in - let evi = Evd.find_undefined evd evk in - let evenv = evar_env evi in - let id = next_ident_away idx (ids_of_named_context (evar_context evi)) in - let concl = whd_betadeltaiota evenv evd evi.evar_concl in - let s = destSort concl in - let evd1,(dom,u1) = - let evd = Sigma.Unsafe.of_evar_map evd in - let Sigma (e, evd1, _) = new_type_evar evenv evd univ_flexible_alg ~filter:(evar_filter evi) in - (Sigma.to_evar_map evd1, e) - in - let evd2,rng = - let newenv = push_named (LocalAssum (id, dom)) evenv in - let src = evar_source evk evd1 in - let filter = Filter.extend 1 (evar_filter evi) in - if is_prop_sort s then - (* Impredicative product, conclusion must fall in [Prop]. *) - new_evar_unsafe newenv evd1 concl ~src ~filter - else - let status = univ_flexible_alg in - let evd3, (rng, srng) = - let evd1 = Sigma.Unsafe.of_evar_map evd1 in - let Sigma (e, evd3, _) = new_type_evar newenv evd1 status ~src ~filter in - (Sigma.to_evar_map evd3, e) - in - let prods = Univ.sup (univ_of_sort u1) (univ_of_sort srng) in - let evd3 = Evd.set_leq_sort evenv evd3 (Type prods) s in - evd3, rng - in - let prod = mkProd (Name id, dom, subst_var id rng) in - let evd3 = Evd.define evk prod evd2 in - evd3,prod - -(* Refine an applied evar to a product and returns its instantiation *) - -let define_evar_as_product evd (evk,args) = - let evd,prod = define_pure_evar_as_product evd evk in - (* Quick way to compute the instantiation of evk with args *) - let na,dom,rng = destProd prod in - let evdom = mkEvar (fst (destEvar dom), args) in - let evrngargs = Array.cons (mkRel 1) (Array.map (lift 1) args) in - let evrng = mkEvar (fst (destEvar rng), evrngargs) in - evd,mkProd (na, evdom, evrng) - -(* Refine an evar with an abstraction - - I.e., solve x1..xq |- ?e:T(x1..xq) with e:=λy:A.?e'[x1..xq,y] where: - - either T(x1..xq) = πy:A(x1..xq).B(x1..xq,y) - or T(x1..xq) = ?d[x1..xq] and we define ?d := πy:?A.?B - with x1..xq |- ?A:Type and x1..xq,y |- ?B:Type - - x1..xq,y:A |- ?e':B -*) - -let define_pure_evar_as_lambda env evd evk = - let open Context.Named.Declaration in - let evi = Evd.find_undefined evd evk in - let evenv = evar_env evi in - let typ = whd_betadeltaiota evenv evd (evar_concl evi) in - let evd1,(na,dom,rng) = match kind_of_term typ with - | Prod (na,dom,rng) -> (evd,(na,dom,rng)) - | Evar ev' -> let evd,typ = define_evar_as_product evd ev' in evd,destProd typ - | _ -> error_not_product_loc Loc.ghost env evd typ in - let avoid = ids_of_named_context (evar_context evi) in - let id = - next_name_away_with_default_using_types "x" na avoid (whd_evar evd dom) in - let newenv = push_named (LocalAssum (id, dom)) evenv in - let filter = Filter.extend 1 (evar_filter evi) in - let src = evar_source evk evd1 in - let evd2,body = new_evar_unsafe newenv evd1 ~src (subst1 (mkVar id) rng) ~filter in - let lam = mkLambda (Name id, dom, subst_var id body) in - Evd.define evk lam evd2, lam - -let define_evar_as_lambda env evd (evk,args) = - let evd,lam = define_pure_evar_as_lambda env evd evk in - (* Quick way to compute the instantiation of evk with args *) - let na,dom,body = destLambda lam in - let evbodyargs = Array.cons (mkRel 1) (Array.map (lift 1) args) in - let evbody = mkEvar (fst (destEvar body), evbodyargs) in - evd,mkLambda (na, dom, evbody) - -let rec evar_absorb_arguments env evd (evk,args as ev) = function - | [] -> evd,ev - | a::l -> - (* TODO: optimize and avoid introducing intermediate evars *) - let evd,lam = define_pure_evar_as_lambda env evd evk in - let _,_,body = destLambda lam in - let evk = fst (destEvar body) in - evar_absorb_arguments env evd (evk, Array.cons a args) l - -(* Refining an evar to a sort *) - -let define_evar_as_sort env evd (ev,args) = - let evd, u = new_univ_variable univ_rigid evd in - let evi = Evd.find_undefined evd ev in - let s = Type u in - let concl = whd_betadeltaiota (evar_env evi) evd evi.evar_concl in - let sort = destSort concl in - let evd' = Evd.define ev (mkSort s) evd in - Evd.set_leq_sort env evd' (Type (Univ.super u)) sort, s - -(* We don't try to guess in which sort the type should be defined, since - any type has type Type. May cause some trouble, but not so far... *) - -let judge_of_new_Type evd = - let Sigma (s, evd', p) = Sigma.new_univ_variable univ_rigid evd in - Sigma ({ uj_val = mkSort (Type s); uj_type = mkSort (Type (Univ.super s)) }, evd', p) - -(* Propagation of constraints through application and abstraction: - Given a type constraint on a functional term, returns the type - constraint on its domain and codomain. If the input constraint is - an evar instantiate it with the product of 2 new evars. *) - -let split_tycon loc env evd tycon = - let rec real_split evd c = - let t = whd_betadeltaiota env evd c in - match kind_of_term t with - | Prod (na,dom,rng) -> evd, (na, dom, rng) - | Evar ev (* ev is undefined because of whd_betadeltaiota *) -> - let (evd',prod) = define_evar_as_product evd ev in - let (_,dom,rng) = destProd prod in - evd',(Anonymous, dom, rng) - | App (c,args) when isEvar c -> - let (evd',lam) = define_evar_as_lambda env evd (destEvar c) in - real_split evd' (mkApp (lam,args)) - | _ -> error_not_product_loc loc env evd c - in - match tycon with - | None -> evd,(Anonymous,None,None) - | Some c -> - let evd', (n, dom, rng) = real_split evd c in - evd', (n, mk_tycon dom, mk_tycon rng) - -let valcon_of_tycon x = x -let lift_tycon n = Option.map (lift n) - -let pr_tycon env = function - None -> str "None" - | Some t -> Termops.print_constr_env env t - -let subterm_source evk (loc,k) = - let evk = match k with - | Evar_kinds.SubEvar (evk) -> evk - | _ -> evk in - (loc,Evar_kinds.SubEvar evk) - - -(** Term exploration up to instantiation. *) -let kind_of_term_upto sigma t = - Constr.kind (Reductionops.whd_evar sigma t) - -(** [eq_constr_univs_test sigma1 sigma2 t u] tests equality of [t] and - [u] up to existential variable instantiation and equalisable - universes. The term [t] is interpreted in [sigma1] while [u] is - interpreted in [sigma2]. The universe constraints in [sigma2] are - assumed to be an extention of those in [sigma1]. *) -let eq_constr_univs_test sigma1 sigma2 t u = - (* spiwack: mild code duplication with {!Evd.eq_constr_univs}. *) - let open Evd in - let fold cstr sigma = - try Some (add_universe_constraints sigma cstr) - with Univ.UniverseInconsistency _ | UniversesDiffer -> None - in - let ans = - Universes.eq_constr_univs_infer_with - (fun t -> kind_of_term_upto sigma1 t) - (fun u -> kind_of_term_upto sigma2 u) - (universes sigma2) fold t u sigma2 - in - match ans with None -> false | Some _ -> true diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli deleted file mode 100644 index bc4c37a91..000000000 --- a/pretyping/evarutil.mli +++ /dev/null @@ -1,253 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -open Names -open Term -open Evd -open Environ - -(** {5 This modules provides useful functions for unification modulo evars } *) - -(** {6 Metas} *) - -(** [new_meta] is a generator of unique meta variables *) -val new_meta : unit -> metavariable -val mk_new_meta : unit -> constr - -(** {6 Creating a fresh evar given their type and context} *) -val new_evar : - env -> 'r Sigma.t -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t -> - ?candidates:constr list -> ?store:Store.t -> - ?naming:Misctypes.intro_pattern_naming_expr -> - ?principal:bool -> types -> (constr, 'r) Sigma.sigma - -val new_pure_evar : - named_context_val -> 'r Sigma.t -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t -> - ?candidates:constr list -> ?store:Store.t -> - ?naming:Misctypes.intro_pattern_naming_expr -> - ?principal:bool -> types -> (evar, 'r) Sigma.sigma - -val new_pure_evar_full : 'r Sigma.t -> evar_info -> (evar, 'r) Sigma.sigma - -(** the same with side-effects *) -val e_new_evar : - env -> evar_map ref -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t -> - ?candidates:constr list -> ?store:Store.t -> - ?naming:Misctypes.intro_pattern_naming_expr -> - ?principal:bool -> types -> constr - -(** Create a new Type existential variable, as we keep track of - them during type-checking and unification. *) -val new_type_evar : - env -> 'r Sigma.t -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t -> - ?naming:Misctypes.intro_pattern_naming_expr -> ?principal:bool -> rigid -> - (constr * sorts, 'r) Sigma.sigma - -val e_new_type_evar : env -> evar_map ref -> - ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t -> - ?naming:Misctypes.intro_pattern_naming_expr -> ?principal:bool -> rigid -> constr * sorts - -val new_Type : ?rigid:rigid -> env -> 'r Sigma.t -> (constr, 'r) Sigma.sigma -val e_new_Type : ?rigid:rigid -> env -> evar_map ref -> constr - -val restrict_evar : 'r Sigma.t -> existential_key -> Filter.t -> - constr list option -> (existential_key, 'r) Sigma.sigma - -(** Polymorphic constants *) - -val new_global : 'r Sigma.t -> Globnames.global_reference -> (constr, 'r) Sigma.sigma -val e_new_global : evar_map ref -> Globnames.global_reference -> constr - -(** Create a fresh evar in a context different from its definition context: - [new_evar_instance sign evd ty inst] creates a new evar of context - [sign] and type [ty], [inst] is a mapping of the evar context to - the context where the evar should occur. This means that the terms - of [inst] are typed in the occurrence context and their type (seen - as a telescope) is [sign] *) -val new_evar_instance : - named_context_val -> 'r Sigma.t -> types -> - ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t -> ?candidates:constr list -> - ?store:Store.t -> ?naming:Misctypes.intro_pattern_naming_expr -> - ?principal:bool -> - constr list -> (constr, 'r) Sigma.sigma - -val make_pure_subst : evar_info -> constr array -> (Id.t * constr) list - -(** {6 Evars/Metas switching...} *) - -val non_instantiated : evar_map -> evar_info Evar.Map.t - -(** {6 Unification utils} *) - -(** [head_evar c] returns the head evar of [c] if any *) -exception NoHeadEvar -val head_evar : constr -> existential_key (** may raise NoHeadEvar *) - -(* Expand head evar if any *) -val whd_head_evar : evar_map -> constr -> constr - -(* An over-approximation of [has_undefined (nf_evars evd c)] *) -val has_undefined_evars : evar_map -> constr -> bool - -val is_ground_term : evar_map -> constr -> bool -val is_ground_env : evar_map -> env -> bool -(** [check_evars env initial_sigma extended_sigma c] fails if some - new unresolved evar remains in [c] *) -val check_evars : env -> evar_map -> evar_map -> constr -> unit - -val define_evar_as_product : evar_map -> existential -> evar_map * types -val define_evar_as_lambda : env -> evar_map -> existential -> evar_map * types -val define_evar_as_sort : env -> evar_map -> existential -> evar_map * sorts - -(** Instantiate an evar by as many lambda's as needed so that its arguments - are moved to the evar substitution (i.e. turn [?x[vars1:=args1] args] into - [?y[vars1:=args1,vars:=args]] with - [vars1 |- ?x:=\vars.?y[vars1:=vars1,vars:=vars]] *) -val evar_absorb_arguments : env -> evar_map -> existential -> constr list -> - evar_map * existential - -(** [gather_dependent_evars evm seeds] classifies the evars in [evm] - as dependent_evars and goals (these may overlap). A goal is an - evar in [seeds] or an evar appearing in the (partial) definition - of a goal. A dependent evar is an evar appearing in the type - (hypotheses and conclusion) of a goal, or in the type or (partial) - definition of a dependent evar. The value return is a map - associating to each dependent evar [None] if it has no (partial) - definition or [Some s] if [s] is the list of evars appearing in - its (partial) definition. *) -val gather_dependent_evars : evar_map -> evar list -> (Evar.Set.t option) Evar.Map.t - -(** The following functions return the set of undefined evars - contained in the object, the defined evars being traversed. - This is roughly a combination of the previous functions and - [nf_evar]. *) - -val undefined_evars_of_term : evar_map -> constr -> Evar.Set.t -val undefined_evars_of_named_context : evar_map -> Context.Named.t -> Evar.Set.t -val undefined_evars_of_evar_info : evar_map -> evar_info -> Evar.Set.t - -(** [occur_evar_upto sigma k c] returns [true] if [k] appears in - [c]. It looks up recursively in [sigma] for the value of existential - variables. *) -val occur_evar_upto : evar_map -> Evar.t -> Constr.t -> bool - -(** {6 Value/Type constraints} *) - -val judge_of_new_Type : 'r Sigma.t -> (unsafe_judgment, 'r) Sigma.sigma - -type type_constraint = types option -type val_constraint = constr option - -val empty_tycon : type_constraint -val mk_tycon : constr -> type_constraint -val empty_valcon : val_constraint -val mk_valcon : constr -> val_constraint - -val split_tycon : - Loc.t -> env -> evar_map -> type_constraint -> - evar_map * (Name.t * type_constraint * type_constraint) - -val valcon_of_tycon : type_constraint -> val_constraint -val lift_tycon : int -> type_constraint -> type_constraint - -(***********************************************************) - -(** [flush_and_check_evars] raise [Uninstantiated_evar] if an evar remains - uninstantiated; [nf_evar] leaves uninstantiated evars as is *) - -val nf_evar : evar_map -> constr -> constr -val j_nf_evar : evar_map -> unsafe_judgment -> unsafe_judgment -val jl_nf_evar : - evar_map -> unsafe_judgment list -> unsafe_judgment list -val jv_nf_evar : - evar_map -> unsafe_judgment array -> unsafe_judgment array -val tj_nf_evar : - evar_map -> unsafe_type_judgment -> unsafe_type_judgment - -val nf_named_context_evar : evar_map -> Context.Named.t -> Context.Named.t -val nf_rel_context_evar : evar_map -> Context.Rel.t -> Context.Rel.t -val nf_env_evar : evar_map -> env -> env - -val nf_evar_info : evar_map -> evar_info -> evar_info -val nf_evar_map : evar_map -> evar_map -val nf_evar_map_undefined : evar_map -> evar_map - -val env_nf_evar : evar_map -> env -> env -val env_nf_betaiotaevar : evar_map -> env -> env - -val j_nf_betaiotaevar : evar_map -> unsafe_judgment -> unsafe_judgment -val jv_nf_betaiotaevar : - evar_map -> unsafe_judgment array -> unsafe_judgment array -(** Presenting terms without solved evars *) - -val nf_evars_universes : evar_map -> constr -> constr - -val nf_evars_and_universes : evar_map -> evar_map * (constr -> constr) -val e_nf_evars_and_universes : evar_map ref -> (constr -> constr) * Universes.universe_opt_subst - -(** Normalize the evar map w.r.t. universes, after simplification of constraints. - Return the substitution function for constrs as well. *) -val nf_evar_map_universes : evar_map -> evar_map * (constr -> constr) - -(** Replacing all evars, possibly raising [Uninstantiated_evar] *) -exception Uninstantiated_evar of existential_key -val flush_and_check_evars : evar_map -> constr -> constr - -(** {6 Term manipulation up to instantiation} *) - -(** Like {!Constr.kind} except that [kind_of_term sigma t] exposes [t] - as an evar [e] only if [e] is uninstantiated in [sigma]. Otherwise the - value of [e] in [sigma] is (recursively) used. *) -val kind_of_term_upto : evar_map -> constr -> (constr,types) kind_of_term - -(** [eq_constr_univs_test sigma1 sigma2 t u] tests equality of [t] and - [u] up to existential variable instantiation and equalisable - universes. The term [t] is interpreted in [sigma1] while [u] is - interpreted in [sigma2]. The universe constraints in [sigma2] are - assumed to be an extention of those in [sigma1]. *) -val eq_constr_univs_test : evar_map -> evar_map -> constr -> constr -> bool - -(** {6 debug pretty-printer:} *) - -val pr_tycon : env -> type_constraint -> Pp.std_ppcmds - - -(** {6 Removing hyps in evars'context} -raise OccurHypInSimpleClause if the removal breaks dependencies *) - -type clear_dependency_error = -| OccurHypInSimpleClause of Id.t option -| EvarTypingBreak of existential - -exception ClearDependencyError of Id.t * clear_dependency_error - -(* spiwack: marks an evar that has been "defined" by clear. - used by [Goal] and (indirectly) [Proofview] to handle the clear tactic gracefully*) -val cleared : bool Store.field - -val clear_hyps_in_evi : env -> evar_map ref -> named_context_val -> types -> - Id.Set.t -> named_context_val * types - -val clear_hyps2_in_evi : env -> evar_map ref -> named_context_val -> types -> types -> - Id.Set.t -> named_context_val * types * types - -val push_rel_context_to_named_context : Environ.env -> types -> - named_context_val * types * constr list * constr list * (identifier*constr) list - -val generalize_evar_over_rels : evar_map -> existential -> types * constr list - -(** Evar combinators *) - -val evd_comb0 : (evar_map -> evar_map * 'a) -> evar_map ref -> 'a -val evd_comb1 : (evar_map -> 'b -> evar_map * 'a) -> evar_map ref -> 'b -> 'a -val evd_comb2 : (evar_map -> 'b -> 'c -> evar_map * 'a) -> evar_map ref -> 'b -> 'c -> 'a - -val subterm_source : existential_key -> Evar_kinds.t Loc.located -> - Evar_kinds.t Loc.located - -val meta_counter_summary_name : string diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 8329de2ee..a765d3091 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -36,6 +36,7 @@ open Typeops open Globnames open Nameops open Evarutil +open Evardefine open Pretype_errors open Glob_term open Glob_ops @@ -234,6 +235,23 @@ let check_extra_evars_are_solved env current_sigma pending = | _ -> error_unsolvable_implicit loc env current_sigma evk None) pending +(* [check_evars] fails if some unresolved evar remains *) + +let check_evars env initial_sigma sigma c = + let rec proc_rec c = + match kind_of_term c with + | Evar (evk,_ as ev) -> + (match existential_opt_value sigma ev with + | Some c -> proc_rec c + | None -> + if not (Evd.mem initial_sigma evk) then + let (loc,k) = evar_source evk sigma in + match k with + | Evar_kinds.ImplicitArg (gr, (i, id), false) -> () + | _ -> Pretype_errors.error_unsolvable_implicit loc env sigma evk None) + | _ -> Constr.iter proc_rec c + in proc_rec c + let check_evars_are_solved env current_sigma frozen pending = check_typeclasses_instances_are_solved env current_sigma frozen; check_problems_are_solved env current_sigma; diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli index 40745ed09..4c4c535d8 100644 --- a/pretyping/pretyping.mli +++ b/pretyping/pretyping.mli @@ -130,6 +130,10 @@ val solve_remaining_evars : inference_flags -> val check_evars_are_solved : env -> (* current map: *) evar_map -> (* map to check: *) pending -> unit +(** [check_evars env initial_sigma extended_sigma c] fails if some + new unresolved evar remains in [c] *) +val check_evars : env -> evar_map -> evar_map -> constr -> unit + (**/**) (** Internal of Pretyping... *) val pretype : diff --git a/pretyping/pretyping.mllib b/pretyping/pretyping.mllib index b59589bda..c8b3307d7 100644 --- a/pretyping/pretyping.mllib +++ b/pretyping/pretyping.mllib @@ -1,4 +1,5 @@ Locusops +Pretype_errors Reductionops Inductiveops Vnorm @@ -6,9 +7,8 @@ Arguments_renaming Nativenorm Retyping Cbv -Pretype_errors Find_subterm -Evarutil +Evardefine Evarsolve Recordops Evarconv diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 935e18d8d..7f4249c5b 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -594,9 +594,7 @@ let pr_state (tm,sk) = (*** Reduction Functions Operators ***) (*************************************) -let safe_evar_value sigma ev = - try Some (Evd.existential_value sigma ev) - with NotInstantiatedEvar | Not_found -> None +let safe_evar_value = Evarutil.safe_evar_value let safe_meta_value sigma ev = try Some (Evd.meta_value sigma ev) @@ -1183,30 +1181,8 @@ let whd_zeta c = Stack.zip (local_whd_state_gen zeta Evd.empty (c,Stack.empty)) (****************************************************************************) (* Replacing defined evars for error messages *) -let rec whd_evar sigma c = - match kind_of_term c with - | Evar ev -> - let (evk, args) = ev in - let args = Array.map (fun c -> whd_evar sigma c) args in - (match safe_evar_value sigma (evk, args) with - Some c -> whd_evar sigma c - | None -> c) - | Sort (Type u) -> - let u' = Evd.normalize_universe sigma u in - if u' == u then c else mkSort (Sorts.sort_of_univ u') - | Const (c', u) when not (Univ.Instance.is_empty u) -> - let u' = Evd.normalize_universe_instance sigma u in - if u' == u then c else mkConstU (c', u') - | Ind (i, u) when not (Univ.Instance.is_empty u) -> - let u' = Evd.normalize_universe_instance sigma u in - if u' == u then c else mkIndU (i, u') - | Construct (co, u) when not (Univ.Instance.is_empty u) -> - let u' = Evd.normalize_universe_instance sigma u in - if u' == u then c else mkConstructU (co, u') - | _ -> c - -let nf_evar = - local_strong whd_evar +let whd_evar = Evarutil.whd_evar +let nf_evar = Evarutil.nf_evar (* lazy reduction functions. The infos must be created for each term *) (* Note by HH [oct 08] : why would it be the job of clos_norm_flags to add diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index 0faa35c87..3a5796fe1 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -490,7 +490,7 @@ let is_instance = function Nota: we will only check the resolvability status of undefined evars. *) -let resolvable = Store.field () +let resolvable = Proofview.Unsafe.typeclass_resolvable let set_resolvable s b = if b then Store.remove s resolvable diff --git a/pretyping/typing.ml b/pretyping/typing.ml index 5347d965b..52afa7f83 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -39,7 +39,7 @@ let e_type_judgment env evdref j = match kind_of_term (whd_betadeltaiota env !evdref j.uj_type) with | Sort s -> {utj_val = j.uj_val; utj_type = s } | Evar ev -> - let (evd,s) = Evarutil.define_evar_as_sort env !evdref ev in + let (evd,s) = Evardefine.define_evar_as_sort env !evdref ev in evdref := evd; { utj_val = j.uj_val; utj_type = s } | _ -> error_not_type env j @@ -61,7 +61,7 @@ let e_judge_of_apply env evdref funj argjv = else error_cant_apply_bad_type env (n,c1, hj.uj_type) funj argjv | Evar ev -> - let (evd',t) = Evarutil.define_evar_as_product !evdref ev in + let (evd',t) = Evardefine.define_evar_as_product !evdref ev in evdref := evd'; let (_,_,c2) = destProd t in apply_rec (n+1) (subst1 hj.uj_val c2) restjl diff --git a/pretyping/unification.ml b/pretyping/unification.ml index a7b415552..a4a386530 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -19,6 +19,7 @@ open Evd open Reduction open Reductionops open Evarutil +open Evardefine open Evarsolve open Pretype_errors open Retyping |