aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--dev/printers.mllib1
-rw-r--r--pretyping/cases.ml1
-rw-r--r--pretyping/evarconv.ml1
-rw-r--r--pretyping/evarsolve.ml1363
-rw-r--r--pretyping/evarsolve.mli48
-rw-r--r--pretyping/evarutil.ml1345
-rw-r--r--pretyping/evarutil.mli40
-rw-r--r--pretyping/pretyping.mllib1
-rw-r--r--pretyping/unification.ml1
9 files changed, 1428 insertions, 1373 deletions
diff --git a/dev/printers.mllib b/dev/printers.mllib
index 7caf268b9..fa6d9324c 100644
--- a/dev/printers.mllib
+++ b/dev/printers.mllib
@@ -95,6 +95,7 @@ Retyping
Cbv
Pretype_errors
Evarutil
+Evarsolve
Term_dnet
Recordops
Evarconv
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index ce8e296ba..60e3025b4 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -24,6 +24,7 @@ open Glob_ops
open Retyping
open Pretype_errors
open Evarutil
+open Evarsolve
open Evarconv
open Evd
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index ca5ed190f..cb0bed51e 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -17,6 +17,7 @@ open Termops
open Environ
open Recordops
open Evarutil
+open Evarsolve
open Globnames
open Evd
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
new file mode 100644
index 000000000..1b8518098
--- /dev/null
+++ b/pretyping/evarsolve.ml
@@ -0,0 +1,1363 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+open Pp
+open Util
+open Errors
+open Names
+open Term
+open Environ
+open Termops
+open Evd
+open Namegen
+open Retyping
+open Reductionops
+open Evarutil
+open Pretype_errors
+
+let normalize_evar evd ev =
+ match kind_of_term (whd_evar evd (mkEvar ev)) with
+ | Evar (evk,args) -> (evk,args)
+ | _ -> assert false
+
+(************************)
+(* Manipulating filters *)
+(************************)
+
+let extract_subfilter initial_filter refined_filter =
+ snd (List.filter2 (fun b1 b2 -> b1) initial_filter refined_filter)
+
+let apply_subfilter filter subfilter =
+ fst (List.fold_right (fun oldb (l,filter) ->
+ if oldb then List.hd filter::l,List.tl filter else (false::l,filter))
+ filter ([], List.rev subfilter))
+
+(*------------------------------------*
+ * Restricting existing evars *
+ *------------------------------------*)
+
+let rec eq_filter l1 l2 = match l1, l2 with
+| [], [] -> true
+| h1 :: l1, h2 :: l2 ->
+ (if h1 then h2 else not h2) && eq_filter l1 l2
+| _ -> false
+
+let restrict_evar_key evd evk filter candidates =
+ match filter, candidates with
+ | None, None -> evd, evk
+ | _ ->
+ let evi = Evd.find_undefined evd evk in
+ let oldfilter = evar_filter evi in
+ begin match filter, candidates with
+ | Some filter, None when eq_filter oldfilter filter ->
+ evd, evk
+ | _ ->
+ let filter = match filter with
+ | None -> evar_filter evi
+ | Some filter -> filter in
+ let candidates = match candidates with
+ | None -> evi.evar_candidates
+ | Some _ -> candidates in
+ let ccl = evi.evar_concl in
+ let sign = evar_hyps evi in
+ let src = evi.evar_source in
+ let evd,newevk = new_pure_evar evd sign ccl ~src ~filter ?candidates in
+ let _, ctxt = List.filter2 (fun b c -> b) filter (evar_context evi) in
+ let id_inst = Array.of_list (List.map (fun (id,_,_) -> mkVar id) ctxt) in
+ Evd.define evk (mkEvar(newevk,id_inst)) evd,newevk
+ end
+
+(* Restrict an applied evar and returns its restriction in the same context *)
+let restrict_applied_evar evd (evk,argsv) filter candidates =
+ let evd,newevk = restrict_evar_key evd evk filter candidates in
+ let newargsv = match filter with
+ | None -> (* optim *) argsv
+ | Some filter ->
+ let evi = Evd.find evd evk in
+ let subfilter = extract_subfilter (evar_filter evi) filter in
+ Array.filter_with subfilter argsv in
+ evd,(newevk,newargsv)
+
+(* Restrict an evar in the current evar_map *)
+let restrict_evar evd evk filter candidates =
+ fst (restrict_evar_key evd evk filter candidates)
+
+(* Restrict an evar in the current evar_map *)
+let restrict_instance evd evk filter argsv =
+ match filter with None -> argsv | Some filter ->
+ let evi = Evd.find evd evk in
+ Array.filter_with (extract_subfilter (evar_filter evi) filter) argsv
+
+let noccur_evar env evd evk c =
+ let rec occur_rec k c = match kind_of_term c with
+ | Evar (evk',args' as ev') ->
+ (match safe_evar_value evd ev' with
+ | Some c -> occur_rec k c
+ | None ->
+ if Int.equal evk evk' then raise Occur
+ else Array.iter (occur_rec k) args')
+ | Rel i when i > k ->
+ (match pi2 (Environ.lookup_rel (i-k) env) with
+ | None -> ()
+ | Some b -> occur_rec k (lift i b))
+ | _ -> iter_constr_with_binders succ occur_rec k c
+ in
+ try occur_rec 0 c; true with Occur -> false
+
+(***************************************)
+(* Managing chains of local definitons *)
+(***************************************)
+
+(* Expand rels and vars that are bound to other rels or vars so that
+ dependencies in variables are canonically associated to the most ancient
+ variable in its family of aliased variables *)
+
+let compute_var_aliases sign =
+ List.fold_right (fun (id,b,c) aliases ->
+ match b with
+ | Some t ->
+ (match kind_of_term t with
+ | Var id' ->
+ let aliases_of_id =
+ try Id.Map.find id' aliases with Not_found -> [] in
+ Id.Map.add id (aliases_of_id@[t]) aliases
+ | _ ->
+ Id.Map.add id [t] aliases)
+ | None -> aliases)
+ sign Id.Map.empty
+
+let compute_rel_aliases var_aliases rels =
+ snd (List.fold_right (fun (_,b,t) (n,aliases) ->
+ (n-1,
+ match b with
+ | Some t ->
+ (match kind_of_term t with
+ | Var id' ->
+ let aliases_of_n =
+ try Id.Map.find id' var_aliases with Not_found -> [] in
+ Int.Map.add n (aliases_of_n@[t]) aliases
+ | Rel p ->
+ let aliases_of_n =
+ try Int.Map.find (p+n) aliases with Not_found -> [] in
+ Int.Map.add n (aliases_of_n@[mkRel (p+n)]) aliases
+ | _ ->
+ Int.Map.add n [lift n t] aliases)
+ | None -> aliases))
+ rels (List.length rels,Int.Map.empty))
+
+let make_alias_map env =
+ (* We compute the chain of aliases for each var and rel *)
+ let var_aliases = compute_var_aliases (named_context env) in
+ let rel_aliases = compute_rel_aliases var_aliases (rel_context env) in
+ (var_aliases,rel_aliases)
+
+let lift_aliases n (var_aliases,rel_aliases as aliases) =
+ if Int.equal n 0 then aliases else
+ (var_aliases,
+ Int.Map.fold (fun p l -> Int.Map.add (p+n) (List.map (lift n) l))
+ rel_aliases Int.Map.empty)
+
+let get_alias_chain_of aliases x = match kind_of_term x with
+ | Rel n -> (try Int.Map.find n (snd aliases) with Not_found -> [])
+ | Var id -> (try Id.Map.find id (fst aliases) with Not_found -> [])
+ | _ -> []
+
+let normalize_alias_opt aliases x =
+ match get_alias_chain_of aliases x with
+ | [] -> None
+ | a::_ when isRel a or isVar a -> Some a
+ | [_] -> None
+ | _::a::_ -> Some a
+
+let normalize_alias aliases x =
+ match normalize_alias_opt aliases x with
+ | Some a -> a
+ | None -> x
+
+let normalize_alias_var var_aliases id =
+ destVar (normalize_alias (var_aliases,Int.Map.empty) (mkVar id))
+
+let extend_alias (_,b,_) (var_aliases,rel_aliases) =
+ let rel_aliases =
+ Int.Map.fold (fun n l -> Int.Map.add (n+1) (List.map (lift 1) l))
+ rel_aliases Int.Map.empty in
+ let rel_aliases =
+ match b with
+ | Some t ->
+ (match kind_of_term t with
+ | Var id' ->
+ let aliases_of_binder =
+ try Id.Map.find id' var_aliases with Not_found -> [] in
+ Int.Map.add 1 (aliases_of_binder@[t]) rel_aliases
+ | Rel p ->
+ let aliases_of_binder =
+ try Int.Map.find (p+1) rel_aliases with Not_found -> [] in
+ Int.Map.add 1 (aliases_of_binder@[mkRel (p+1)]) rel_aliases
+ | _ ->
+ Int.Map.add 1 [lift 1 t] rel_aliases)
+ | None -> rel_aliases in
+ (var_aliases, rel_aliases)
+
+let expand_alias_once aliases x =
+ match get_alias_chain_of aliases x with
+ | [] -> None
+ | l -> Some (List.last l)
+
+let expansions_of_var aliases x =
+ match get_alias_chain_of aliases x with
+ | [] -> [x]
+ | a::_ as l when isRel a || isVar a -> x :: List.rev l
+ | _::l -> x :: List.rev l
+
+let expansion_of_var aliases x =
+ match get_alias_chain_of aliases x with
+ | [] -> x
+ | a::_ -> a
+
+let rec expand_vars_in_term_using 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 expand_vars_in_term env = expand_vars_in_term_using (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
+ let cache_rel = ref Int.Set.empty and cache_var = ref Id.Set.empty in
+ let is_in_cache depth = function
+ | Rel n -> Int.Set.mem (n-depth) !cache_rel
+ | Var s -> Id.Set.mem s !cache_var
+ | _ -> false in
+ let put_in_cache depth = function
+ | Rel n -> cache_rel := Int.Set.add (n-depth) !cache_rel
+ | Var s -> cache_var := Id.Set.add s !cache_var
+ | _ -> () in
+ let rec frec (aliases,depth) c =
+ match kind_of_term c with
+ | Rel _ | Var _ as ck ->
+ if is_in_cache depth ck then () else begin
+ put_in_cache depth ck;
+ let c = expansion_of_var aliases c in
+ match kind_of_term c with
+ | Var id -> acc2 := Id.Set.add id !acc2
+ | Rel n -> if n >= depth+1 then acc1 := Int.Set.add (n-depth) !acc1
+ | _ -> frec (aliases,depth) c end
+ | Const _ | Ind _ | Construct _ ->
+ acc2 := List.fold_right Id.Set.add (vars_of_global (Global.env()) c) !acc2
+ | _ ->
+ iter_constr_with_full_binders
+ (fun d (aliases,depth) -> (extend_alias d aliases,depth+1))
+ frec (aliases,depth) c
+ in
+ frec (aliases,0) c;
+ (!acc1,!acc2)
+
+(********************************)
+(* Managing pattern-unification *)
+(********************************)
+
+let rec expand_and_check_vars aliases = function
+ | [] -> []
+ | a::l when isRel a or isVar a ->
+ let a = expansion_of_var aliases a in
+ if isRel a or isVar a then a :: expand_and_check_vars aliases l
+ else raise Exit
+ | _ ->
+ raise Exit
+
+module Constrhash = Hashtbl.Make
+ (struct type t = constr
+ let equal = eq_constr
+ let hash = hash_constr
+ end)
+
+let constr_list_distinct l =
+ let visited = Constrhash.create 23 in
+ let rec loop = function
+ | h::t ->
+ if Constrhash.mem visited h then false
+ else (Constrhash.add visited h h; loop t)
+ | [] -> true
+ in loop l
+
+let get_actual_deps aliases l t =
+ if occur_meta_or_existential t then
+ (* Probably no restrictions on allowed vars in presence of evars *)
+ l
+ else
+ (* Probably strong restrictions coming from t being evar-closed *)
+ let (fv_rels,fv_ids) = free_vars_and_rels_up_alias_expansion aliases t in
+ List.filter (fun c ->
+ match kind_of_term c with
+ | Var id -> Id.Set.mem id fv_ids
+ | Rel n -> Int.Set.mem n fv_rels
+ | _ -> assert false) l
+
+let remove_instance_local_defs evd evk args =
+ let evi = Evd.find evd evk in
+ let rec aux = function
+ | (_,Some _,_)::sign, a::args -> aux (sign,args)
+ | (_,None,_)::sign, a::args -> a::aux (sign,args)
+ | [], [] -> []
+ | _ -> assert false in
+ aux (evar_filtered_context evi, args)
+
+(* Check if an applied evar "?X[args] l" is a Miller's pattern *)
+
+let find_unification_pattern_args env 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
+ | _ -> None
+ else
+ None
+
+let is_unification_pattern_meta env 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
+ | _ -> None
+ else
+ None
+
+let is_unification_pattern_evar env evd (evk,args) l t =
+ if List.for_all (fun x -> isRel x || isVar x) l & noccur_evar env evd evk t
+ then
+ let args = remove_instance_local_defs evd evk (Array.to_list args) in
+ let n = List.length args in
+ match find_unification_pattern_args env (args @ l) t with
+ | Some l -> Some (List.skipn n l)
+ | _ -> None
+ else
+ None
+
+let is_unification_pattern_pure_evar env evd (evk,args) t =
+ let is_ev = is_unification_pattern_evar env evd (evk,args) [] t in
+ match is_ev with
+ | None -> false
+ | Some _ -> true
+
+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
+ | Evar ev -> is_unification_pattern_evar env evd ev l t
+ | _ -> None
+
+(* From a unification problem "?X l = c", build "\x1...xn.(term1 l2)"
+ (pattern unification). It is assumed that l is made of rel's that
+ are distinct and not bound to aliases. *)
+(* It is also assumed that c does not contain metas because metas
+ *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 c' = List.fold_right (fun a c ->
+ let c' = subst_term (lift 1 a) (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 ->
+ let d = map_rel_declaration (lift n) (lookup_rel n env) in
+ mkLambda_or_LetIn d c'
+ | Var id ->
+ let d = lookup_named id env in mkNamedLambda_or_LetIn d c'
+ | _ -> assert false)
+ l c in
+ (* Warning: we may miss some opportunity to eta-reduce more since c'
+ is not in normal form *)
+ whd_eta c'
+
+(*****************************************)
+(* Refining/solving unification problems *)
+(*****************************************)
+
+(* Knowing that [Gamma |- ev : T] and that [ev] is applied to [args],
+ * [make_projectable_subst ev args] builds the substitution [Gamma:=args].
+ * If a variable and an alias of it are bound to the same instance, we skip
+ * the alias (we just use eq_constr -- instead of conv --, since anyway,
+ * only instances that are variables -- or evars -- are later considered;
+ * morever, we can bet that similar instances came at some time from
+ * the very same substitution. The removal of aliased duplicates is
+ * useful to ensure the uniqueness of a projection.
+*)
+
+let make_projectable_subst aliases sigma evi args =
+ let sign = evar_filtered_context evi in
+ let evar_aliases = compute_var_aliases sign in
+ let (_,full_subst,cstr_subst) =
+ List.fold_right
+ (fun (id,b,c) (args,all,cstrs) ->
+ match b,args with
+ | None, a::rest ->
+ let a = whd_evar sigma a in
+ let cstrs =
+ let a',args = decompose_app_vect a in
+ match kind_of_term a' with
+ | Construct cstr ->
+ let l = try Constrmap.find cstr cstrs with Not_found -> [] in
+ Constrmap.add cstr ((args,id)::l) cstrs
+ | _ -> cstrs in
+ (rest,Id.Map.add id [a,normalize_alias_opt aliases a,id] all,cstrs)
+ | Some c, a::rest ->
+ let a = whd_evar sigma a in
+ (match kind_of_term c with
+ | Var id' ->
+ let idc = normalize_alias_var evar_aliases id' in
+ let sub = try Id.Map.find idc all with Not_found -> [] in
+ if List.exists (fun (c,_,_) -> eq_constr a c) sub then
+ (rest,all,cstrs)
+ else
+ (rest,
+ Id.Map.add idc ((a,normalize_alias_opt aliases a,id)::sub) all,
+ cstrs)
+ | _ ->
+ (rest,Id.Map.add id [a,normalize_alias_opt aliases a,id] all,cstrs))
+ | _ -> anomaly (Pp.str "Instance does not match its signature"))
+ sign (Array.rev_to_list args,Id.Map.empty,Constrmap.empty) in
+ (full_subst,cstr_subst)
+
+(*------------------------------------*
+ * operations on the evar constraints *
+ *------------------------------------*)
+
+(* We have a unification problem Σ; Γ |- ?e[u1..uq] = t : s where ?e is not yet
+ * declared in Σ but yet known to be declarable in some context x1:T1..xq:Tq.
+ * [define_evar_from_virtual_equation ... Γ Σ t (x1:T1..xq:Tq) .. (u1..uq) (x1..xq)]
+ * declares x1:T1..xq:Tq |- ?e : s such that ?e[u1..uq] = t holds.
+ *)
+
+let define_evar_from_virtual_equation define_fun env evd t_in_env sign filter inst_in_env =
+ let ty_t_in_env = Retyping.get_type_of env evd t_in_env in
+ let evd,evar_in_env = new_evar_instance sign evd ty_t_in_env ~filter inst_in_env in
+ let t_in_env = whd_evar evd t_in_env in
+ let evd = define_fun env evd (destEvar evar_in_env) t_in_env in
+ let ids = List.map pi1 (named_context_of_val sign) in
+ let inst_in_sign = List.map mkVar (List.filter_with filter ids) in
+ let evar_in_sign = mkEvar (fst (destEvar evar_in_env), Array.of_list inst_in_sign) in
+ (evd,whd_evar evd evar_in_sign)
+
+(* We have x1..xq |- ?e1 : τ and had to solve something like
+ * Σ; Γ |- ?e1[u1..uq] = (...\y1 ... \yk ... c), where c is typically some
+ * ?e2[v1..vn], hence flexible. We had to go through k binders and now
+ * virtually have x1..xq, y1'..yk' | ?e1' : τ' and the equation
+ * Γ, y1..yk |- ?e1'[u1..uq y1..yk] = c.
+ * [materialize_evar Γ evd k (?e1[u1..uq]) τ'] extends Σ with the declaration
+ * of ?e1' and returns both its instance ?e1'[x1..xq y1..yk] in an extension
+ * of the context of e1 so that e1 can be instantiated by
+ * (...\y1' ... \yk' ... ?e1'[x1..xq y1'..yk']),
+ * and the instance ?e1'[u1..uq y1..yk] so that the remaining equation
+ * ?e1'[u1..uq y1..yk] = c can be registered
+ *
+ * Note that, because invert_definition does not check types, we need to
+ * guess the types of y1'..yn' by inverting the types of y1..yn along the
+ * substitution u1..uq.
+ *)
+
+let materialize_evar define_fun env evd k (evk1,args1) ty_in_env =
+ let evi1 = Evd.find_undefined evd evk1 in
+ let env1,rel_sign = env_rel_context_chop k env in
+ let sign1 = evar_hyps evi1 in
+ let filter1 = evar_filter evi1 in
+ let ids1 = List.map pi1 (named_context_of_val sign1) in
+ let inst_in_sign = List.map mkVar (List.filter_with filter1 ids1) in
+ let (sign2,filter2,inst2_in_env,inst2_in_sign,_,evd,_) =
+ List.fold_right (fun (na,b,t_in_env as d) (sign,filter,inst_in_env,inst_in_sign,env,evd,avoid) ->
+ let id = next_name_away na avoid in
+ let evd,t_in_sign =
+ define_evar_from_virtual_equation define_fun env evd t_in_env
+ sign filter inst_in_env in
+ let evd,b_in_sign = match b with
+ | None -> evd,None
+ | Some b ->
+ let evd,b = define_evar_from_virtual_equation define_fun env evd b
+ sign filter inst_in_env in
+ evd,Some b in
+ (push_named_context_val (id,b_in_sign,t_in_sign) sign,true::filter,
+ (mkRel 1)::(List.map (lift 1) inst_in_env),
+ (mkRel 1)::(List.map (lift 1) inst_in_sign),
+ push_rel d env,evd,id::avoid))
+ rel_sign
+ (sign1,filter1,Array.to_list args1,inst_in_sign,env1,evd,ids1)
+ in
+ let evd,ev2ty_in_sign =
+ define_evar_from_virtual_equation define_fun env evd ty_in_env
+ sign2 filter2 inst2_in_env in
+ let evd,ev2_in_sign =
+ new_evar_instance sign2 evd ev2ty_in_sign ~filter:filter2 inst2_in_sign in
+ let ev2_in_env = (fst (destEvar ev2_in_sign), Array.of_list inst2_in_env) in
+ (evd, ev2_in_sign, ev2_in_env)
+
+let restrict_upon_filter evd evk p args =
+ let newfilter = List.map p args in
+ if List.for_all (fun id -> id) newfilter then
+ None
+ else
+ let oldfullfilter = evar_filter (Evd.find_undefined evd evk) in
+ Some (apply_subfilter oldfullfilter newfilter)
+
+(* Inverting constructors in instances (common when inferring type of match) *)
+
+let find_projectable_constructor env evd cstr k args cstr_subst =
+ try
+ let l = Constrmap.find cstr cstr_subst in
+ let args = Array.map (lift (-k)) args in
+ let l =
+ List.filter (fun (args',id) ->
+ (* is_conv is maybe too strong (and source of useless computation) *)
+ (* (at least expansion of aliases is needed) *)
+ Array.for_all2 (is_conv env evd) args args') l in
+ List.map snd l
+ with Not_found ->
+ []
+
+(* [find_projectable_vars env sigma y subst] finds all vars of [subst]
+ * that project on [y]. It is able to find solutions to the following
+ * two kinds of problems:
+ *
+ * - ?n[...;x:=y;...] = y
+ * - ?n[...;x:=?m[args];...] = y with ?m[args] = y recursively solvable
+ *
+ * (see test-suite/success/Fixpoint.v for an example of application of
+ * the second kind of problem).
+ *
+ * The seek for [y] is up to variable aliasing. In case of solutions that
+ * differ only up to aliasing, the binding that requires the less
+ * steps of alias reduction is kept. At the end, only one solution up
+ * to aliasing is kept.
+ *
+ * [find_projectable_vars] also unifies against evars that themselves mention
+ * [y] and recursively.
+ *
+ * In short, the following situations give the following solutions:
+ *
+ * problem evar ctxt soluce remark
+ * z1; z2:=z1 |- ?ev[z1;z2] = z1 y1:A; y2:=y1 y1 \ thanks to defs kept in
+ * z1; z2:=z1 |- ?ev[z1;z2] = z2 y1:A; y2:=y1 y2 / subst and preferring =
+ * z1; z2:=z1 |- ?ev[z1] = z2 y1:A y1 thanks to expand_var
+ * z1; z2:=z1 |- ?ev[z2] = z1 y1:A y1 thanks to expand_var
+ * z3 |- ?ev[z3;z3] = z3 y1:A; y2:=y1 y2 see make_projectable_subst
+ *
+ * Remark: [find_projectable_vars] assumes that identical instances of
+ * variables in the same set of aliased variables are already removed (see
+ * [make_projectable_subst])
+ *)
+
+type evar_projection =
+| ProjectVar
+| ProjectEvar of existential * evar_info * Id.t * evar_projection
+
+exception NotUnique
+exception NotUniqueInType of (Id.t * evar_projection) list
+
+let rec assoc_up_to_alias sigma aliases y yc = function
+ | [] -> raise Not_found
+ | (c,cc,id)::l ->
+ let c' = whd_evar sigma c in
+ if eq_constr y c' then id
+ else
+ match l with
+ | _ :: _ -> assoc_up_to_alias sigma aliases y yc l
+ | [] ->
+ (* Last chance, we reason up to alias conversion *)
+ match (if c == c' then cc else normalize_alias_opt aliases c') with
+ | Some cc when eq_constr yc cc -> id
+ | _ -> if eq_constr yc c then id else raise Not_found
+
+let rec find_projectable_vars with_evars aliases sigma y subst =
+ let yc = normalize_alias aliases y in
+ let is_projectable idc idcl subst' =
+ (* First test if some [id] aliased to [idc] is bound to [y] in [subst] *)
+ try
+ let id = assoc_up_to_alias sigma aliases y yc idcl in
+ (id,ProjectVar)::subst'
+ with Not_found ->
+ (* Then test if [idc] is (indirectly) bound in [subst] to some evar *)
+ (* projectable on [y] *)
+ if with_evars then
+ let idcl' = List.filter (fun (c,_,id) -> isEvar c) idcl in
+ match idcl' with
+ | [c,_,id] ->
+ begin
+ let (evk,argsv as t) = destEvar c in
+ let evi = Evd.find sigma evk in
+ let subst,_ = make_projectable_subst aliases sigma evi argsv in
+ let l = find_projectable_vars with_evars aliases sigma y subst in
+ match l with
+ | [id',p] -> (id,ProjectEvar (t,evi,id',p))::subst'
+ | _ -> subst'
+ end
+ | [] -> subst'
+ | _ -> anomaly (Pp.str "More than one non var in aliases class of evar instance")
+ else
+ subst' in
+ Id.Map.fold is_projectable subst []
+
+(* [filter_solution] checks if one and only one possible projection exists
+ * among a set of solutions to a projection problem *)
+
+let filter_solution = function
+ | [] -> raise Not_found
+ | (id,p)::_::_ -> raise NotUnique
+ | [id,p] -> (mkVar id, p)
+
+let project_with_effects aliases sigma effects t subst =
+ let c, p =
+ filter_solution (find_projectable_vars false aliases sigma t subst) in
+ effects := p :: !effects;
+ c
+
+let rec find_solution_type evarenv = function
+ | (id,ProjectVar)::l -> pi3 (lookup_named id evarenv)
+ | [id,ProjectEvar _] -> (* bugged *) pi3 (lookup_named id evarenv)
+ | (id,ProjectEvar _)::l -> find_solution_type evarenv l
+ | [] -> assert false
+
+(* In case the solution to a projection problem requires the instantiation of
+ * subsidiary evars, [do_projection_effects] performs them; it
+ * also try to instantiate the type of those subsidiary evars if their
+ * type is an evar too.
+ *
+ * Note: typing creates new evar problems, which induces a recursive dependency
+ * with [define]. To avoid a too large set of recursive functions, we
+ * pass [define] to [do_projection_effects] as a parameter.
+ *)
+
+let rec do_projection_effects define_fun env ty evd = function
+ | ProjectVar -> evd
+ | ProjectEvar ((evk,argsv),evi,id,p) ->
+ let evd = Evd.define evk (mkVar id) evd in
+ (* TODO: simplify constraints involving evk *)
+ let evd = do_projection_effects define_fun env ty evd p in
+ let ty = whd_betadeltaiota env evd (Lazy.force ty) in
+ if not (isSort ty) then
+ (* Don't try to instantiate if a sort because if evar_concl is an
+ evar it may commit to a univ level which is not the right
+ one (however, regarding coercions, because t is obtained by
+ unif, we know that no coercion can be inserted) *)
+ let subst = make_pure_subst evi argsv in
+ let ty' = replace_vars subst evi.evar_concl in
+ let ty' = whd_evar evd ty' in
+ if isEvar ty' then define_fun env evd (destEvar ty') ty else evd
+ else
+ evd
+
+(* Assuming Σ; Γ, y1..yk |- c, [invert_arg_from_subst Γ k Σ [x1:=u1..xn:=un] c]
+ * tries to return φ(x1..xn) such that equation φ(u1..un) = c is valid.
+ * The strategy is to imitate the structure of c and then to invert
+ * the variables of c (i.e. rels or vars of Γ) using the algorithm
+ * implemented by project_with_effects/find_projectable_vars.
+ * It returns either a unique solution or says whether 0 or more than
+ * 1 solutions is found.
+ *
+ * Precondition: Σ; Γ, y1..yk |- c /\ Σ; Γ |- u1..un
+ * Postcondition: if φ(x1..xn) is returned then
+ * Σ; Γ, y1..yk |- φ(u1..un) = c /\ x1..xn |- φ(x1..xn)
+ *
+ * The effects correspond to evars instantiated while trying to project.
+ *
+ * [invert_arg_from_subst] is used on instances of evars. Since the
+ * evars are flexible, these instances are potentially erasable. This
+ * is why we don't investigate whether evars in the instances of evars
+ * are unifiable, to the contrary of [invert_definition].
+ *)
+
+type projectibility_kind =
+ | NoUniqueProjection
+ | UniqueProjection of constr * evar_projection list
+
+type projectibility_status =
+ | CannotInvert
+ | Invertible of projectibility_kind
+
+let invert_arg_from_subst evd aliases k0 subst_in_env_extended_with_k_binders c_in_env_extended_with_k_binders =
+ let effects = ref [] in
+ let rec aux k t =
+ let t = whd_evar evd t in
+ match kind_of_term t with
+ | Rel i when i>k0+k -> aux' k (mkRel (i-k))
+ | Var id -> aux' k t
+ | _ -> map_constr_with_binders succ aux k t
+ and aux' k t =
+ try project_with_effects aliases evd effects t subst_in_env_extended_with_k_binders
+ with Not_found ->
+ match expand_alias_once aliases t with
+ | None -> raise Not_found
+ | Some c -> aux k c in
+ try
+ let c = aux 0 c_in_env_extended_with_k_binders in
+ Invertible (UniqueProjection (c,!effects))
+ with
+ | Not_found -> CannotInvert
+ | NotUnique -> Invertible NoUniqueProjection
+
+let invert_arg fullenv evd aliases k evk subst_in_env_extended_with_k_binders c_in_env_extended_with_k_binders =
+ let res = invert_arg_from_subst evd aliases k subst_in_env_extended_with_k_binders c_in_env_extended_with_k_binders in
+ match res with
+ | Invertible (UniqueProjection (c,_)) when not (noccur_evar fullenv evd evk c)
+ ->
+ CannotInvert
+ | _ ->
+ res
+
+exception NotEnoughInformationToInvert
+
+let extract_unique_projections projs =
+ List.map (function
+ | Invertible (UniqueProjection (c,_)) -> c
+ | _ ->
+ (* For instance, there are evars with non-invertible arguments and *)
+ (* we cannot arbitrarily restrict these evars before knowing if there *)
+ (* will really be used; it can also be due to some argument *)
+ (* (typically a rel) that is not inversible and that cannot be *)
+ (* inverted either because it is needed for typing the conclusion *)
+ (* of the evar to project *)
+ raise NotEnoughInformationToInvert) projs
+
+let extract_candidates sols =
+ try
+ Some
+ (List.map (function (id,ProjectVar) -> mkVar id | _ -> raise Exit) sols)
+ with Exit ->
+ None
+
+let invert_invertible_arg fullenv evd aliases k (evk,argsv) args' =
+ let evi = Evd.find_undefined evd evk in
+ let subst,_ = make_projectable_subst aliases evd evi argsv in
+ let projs =
+ Array.map_to_list (invert_arg fullenv evd aliases k evk subst) args' in
+ Array.of_list (extract_unique_projections projs)
+
+(* Redefines an evar with a smaller context (i.e. it may depend on less
+ * variables) such that c becomes closed.
+ * Example: in "fun (x:?1) (y:list ?2[x]) => x = y :> ?3[x,y] /\ x = nil bool"
+ * ?3 <-- ?1 no pb: env of ?3 is larger than ?1's
+ * ?1 <-- list ?2 pb: ?2 may depend on x, but not ?1.
+ * What we do is that ?2 is defined by a new evar ?4 whose context will be
+ * a prefix of ?2's env, included in ?1's env.
+ *
+ * If "hyps |- ?e : T" and "filter" selects a subset hyps' of hyps then
+ * [do_restrict_hyps evd ?e filter] sets ?e:=?e'[hyps'] and returns ?e'
+ * such that "hyps' |- ?e : T"
+ *)
+
+let filter_candidates evd evk filter candidates =
+ let evi = Evd.find_undefined evd evk in
+ let candidates = match candidates with
+ | None -> evi.evar_candidates
+ | Some _ -> candidates in
+ match candidates,filter with
+ | None,_ | _, None -> candidates
+ | Some l, Some filter ->
+ let ids = List.map pi1 (List.filter_with filter (evar_context evi)) in
+ Some (List.filter (fun a ->
+ List.subset (Id.Set.elements (collect_vars a)) ids) l)
+
+let eq_filter f1 f2 =
+ let eq_bool b1 b2 = if b1 then b2 else not b2 in
+ List.equal eq_bool f1 f2
+
+let closure_of_filter evd evk filter =
+ let evi = Evd.find_undefined evd evk in
+ let vars = collect_vars (evar_concl evi) in
+ let ids = List.map pi1 (evar_context evi) in
+ let test id b = b || Id.Set.mem id vars in
+ let newfilter = List.map2 test ids filter in
+ if eq_filter newfilter (evar_filter evi) then None else Some newfilter
+
+let restrict_hyps evd evk filter candidates =
+ (* What to do with dependencies?
+ Assume we have x:A, y:B(x), z:C(x,y) |- ?e:T(x,y,z) and restrict on y.
+ - If y is in a non-erasable position in C(x,y) (i.e. it is not below an
+ occurrence of x in the hnf of C), then z should be removed too.
+ - If y is in a non-erasable position in T(x,y,z) then the problem is
+ unsolvable.
+ Computing whether y is erasable or not may be costly and the
+ interest for this early detection in practice is not obvious. We let
+ it for future work. In any case, thanks to the use of filters, the whole
+ (unrestricted) context remains consistent. *)
+ let candidates = filter_candidates evd evk (Some filter) candidates in
+ let typablefilter = closure_of_filter evd evk filter in
+ (typablefilter,candidates)
+
+exception EvarSolvedWhileRestricting of evar_map * constr
+
+let do_restrict_hyps evd (evk,args as ev) filter candidates =
+ let filter,candidates = match filter with
+ | None -> None,candidates
+ | Some filter -> restrict_hyps evd evk filter candidates in
+ match candidates,filter with
+ | Some [], _ -> error "Not solvable."
+ | Some [nc],_ ->
+ let evd = Evd.define evk nc evd in
+ raise (EvarSolvedWhileRestricting (evd,whd_evar evd (mkEvar ev)))
+ | None, None -> evd,ev
+ | _ -> restrict_applied_evar evd ev filter candidates
+
+(* [postpone_non_unique_projection] postpones equation of the form ?e[?] = c *)
+(* ?e is assumed to have no candidates *)
+
+let postpone_non_unique_projection env evd (evk,argsv as ev) sols rhs =
+ let rhs = expand_vars_in_term env rhs in
+ let filter =
+ restrict_upon_filter evd evk
+ (* Keep only variables that occur in rhs *)
+ (* This is not safe: is the variable is a local def, its body *)
+ (* may contain references to variables that are removed, leading to *)
+ (* a ill-formed context. We would actually need a notion of filter *)
+ (* that says that the body is hidden. Note that expand_vars_in_term *)
+ (* 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)
+ (Array.to_list argsv) in
+ let filter = match filter with
+ | None -> None
+ | Some filter -> closure_of_filter evd evk filter in
+ let candidates = extract_candidates sols in
+ match candidates with
+ | None ->
+ (* We made an approximation by not expanding a local definition *)
+ let evd,ev = restrict_applied_evar evd ev filter None in
+ let pb = (Reduction.CONV,env,mkEvar ev,rhs) in
+ Evd.add_conv_pb pb evd
+ | Some _ ->
+ restrict_evar evd evk filter candidates
+
+(* [postpone_evar_evar] postpones an equation of the form ?e1[?1] = ?e2[?2] *)
+
+let postpone_evar_evar f env evd filter1 ev1 filter2 ev2 =
+ (* Leave an equation between (restrictions of) ev1 andv ev2 *)
+ try
+ let evd,ev1' = do_restrict_hyps evd ev1 filter1 None in
+ try
+ let evd,ev2' = do_restrict_hyps evd ev2 filter2 None in
+ add_conv_pb (Reduction.CONV,env,mkEvar ev1',mkEvar ev2') evd
+ with EvarSolvedWhileRestricting (evd,ev2) ->
+ (* ev2 solved on the fly *)
+ f env evd ev1' ev2
+ with EvarSolvedWhileRestricting (evd,ev1) ->
+ (* ev1 solved on the fly *)
+ f env evd ev2 ev1
+
+(* [solve_evar_evar f Γ Σ ?e1[u1..un] ?e2[v1..vp]] applies an heuristic
+ * to solve the equation Σ; Γ ⊢ ?e1[u1..un] = ?e2[v1..vp]:
+ * - if there are at most one φj for each vj s.t. vj = φj(u1..un),
+ * we first restrict ?e2 to the subset v_k1..v_kq of the vj that are
+ * inversible and we set ?e1[x1..xn] := ?e2[φk1(x1..xn)..φkp(x1..xn)]
+ * (this is a case of pattern-unification)
+ * - symmetrically if there are at most one ψj for each uj s.t.
+ * uj = ψj(v1..vp),
+ * - otherwise, each position i s.t. ui does not occur in v1..vp has to
+ * be restricted and similarly for the vi, and we leave the equation
+ * as an open equation (performed by [postpone_evar])
+ *
+ * Warning: the notion of unique φj is relative to some given class
+ * of unification problems
+ *
+ * Note: argument f is the function used to instantiate evars.
+ *)
+
+let are_canonical_instances args1 args2 env =
+ let n1 = Array.length args1 in
+ let n2 = Array.length args2 in
+ let rec aux n = function
+ | (id,_,c)::sign
+ when n < n1 && isVarId id args1.(n) && isVarId id args2.(n) ->
+ aux (n+1) sign
+ | [] ->
+ let rec aux2 n =
+ Int.equal n n1 ||
+ (isRelN (n1-n) args1.(n) && isRelN (n1-n) args2.(n) && aux2 (n+1))
+ in aux2 n
+ | _ -> false in
+ Int.equal n1 n2 && aux 0 (named_context env)
+
+let filter_compatible_candidates conv_algo env evd evi args rhs c =
+ let c' = instantiate_evar (evar_filtered_context evi) c args in
+ let evd, b = conv_algo env evd Reduction.CONV rhs c' in
+ if b then Some (c,evd) else None
+
+exception DoesNotPreserveCandidateRestriction
+
+let restrict_candidates conv_algo env evd filter1 (evk1,argsv1) (evk2,argsv2) =
+ let evi1 = Evd.find evd evk1 in
+ let evi2 = Evd.find evd evk2 in
+ let cand1 = filter_candidates evd evk1 filter1 None in
+ let cand2 = evi2.evar_candidates in
+ match cand1, cand2 with
+ | _, None -> cand1
+ | None, Some _ -> raise DoesNotPreserveCandidateRestriction
+ | Some l1, Some l2 ->
+ let args1 = Array.to_list argsv1 in
+ let args2 = Array.to_list argsv2 in
+ let l1' = List.filter (fun c1 ->
+ let c1' = instantiate_evar (evar_filtered_context evi1) c1 args1 in
+ let filter c2 =
+ let compatibility = filter_compatible_candidates conv_algo env evd evi2 args2 c1' c2 in
+ match compatibility with
+ | None -> false
+ | Some _ -> true
+ in
+ let filtered = List.filter filter l2 in
+ match filtered with [] -> false | _ -> true) l1 in
+ if Int.equal (List.length l1) (List.length l1') then None else Some l1'
+
+exception CannotProject of bool list option
+
+(* Assume that FV(?n[x1:=t1..xn:=tn]) belongs to some set U.
+ Can ?n be instantiated by a term u depending essentially on xi such that the
+ FV(u[x1:=t1..xn:=tn]) are in the set U?
+ - If ti is a variable, it has to be in U.
+ - If ti is a constructor, its parameters cannot be erased even if u
+ matches on it, so we have to discard ti if the parameters
+ contain variables not in U.
+ - If ti is rigid, we have to discard it if it contains variables in U.
+
+ Note: when restricting as part of an equation ?n[x1:=t1..xn:=tn] = ?m[...]
+ then, occurrences of ?m in the ti can be seen, like variables, as occurrences
+ of subterms to eventually discard so as to be allowed to keep ti.
+*)
+
+let rec is_constrainable_in k (ev,(fv_rels,fv_ids) as g) t =
+ let f,args = decompose_app_vect t in
+ match kind_of_term f with
+ | Construct (ind,_) ->
+ let params,_ = Array.chop (Inductiveops.inductive_nparams ind) args in
+ Array.for_all (is_constrainable_in k g) params
+ | Ind _ -> Array.for_all (is_constrainable_in k g) args
+ | Prod (_,t1,t2) -> is_constrainable_in k g t1 && is_constrainable_in k g t2
+ | Evar (ev',_) -> not (Int.equal ev' ev) (*If ev' needed, one may also try to restrict it*)
+ | Var id -> Id.Set.mem id fv_ids
+ | Rel n -> n <= k || Int.Set.mem n fv_rels
+ | Sort _ -> true
+ | _ -> (* We don't try to be more clever *) true
+
+let has_constrainable_free_vars evd aliases k ev (fv_rels,fv_ids as fvs) t =
+ let t = expansion_of_var aliases t in
+ match kind_of_term t with
+ | Var id -> Id.Set.mem id fv_ids
+ | Rel n -> n <= k || Int.Set.mem n fv_rels
+ | _ -> is_constrainable_in k (ev,fvs) t
+
+let ensure_evar_independent g env evd (evk1,argsv1 as ev1) (evk2,argsv2 as ev2)=
+ let filter1 =
+ restrict_upon_filter evd evk1 (noccur_evar env evd evk2)
+ (Array.to_list argsv1)
+ in
+ let candidates1 = restrict_candidates g env evd filter1 ev1 ev2 in
+ let evd,(evk1,_ as ev1) = do_restrict_hyps evd ev1 filter1 candidates1 in
+ let filter2 =
+ restrict_upon_filter evd evk2 (noccur_evar env evd evk1)
+ (Array.to_list argsv2)
+ in
+ let candidates2 = restrict_candidates g env evd filter2 ev2 ev1 in
+ let evd,ev2 = do_restrict_hyps evd ev2 filter2 candidates2 in
+ evd,ev1,ev2
+
+exception EvarSolvedOnTheFly of evar_map * constr
+
+let project_evar_on_evar g env evd aliases k2 (evk1,argsv1 as ev1) (evk2,argsv2 as ev2) =
+ (* Apply filtering on ev1 so that fvs(ev1) are in fvs(ev2). *)
+ let fvs2 = free_vars_and_rels_up_alias_expansion aliases (mkEvar ev2) in
+ let filter1 = restrict_upon_filter evd evk1
+ (has_constrainable_free_vars evd aliases k2 evk2 fvs2)
+ (Array.to_list argsv1) in
+ (* Only try pruning on variable substitutions, postpone otherwise. *)
+ (* Rules out non-linear instances. *)
+ if is_unification_pattern_pure_evar env evd ev2 (mkEvar ev1) then
+ try
+ let candidates1 = restrict_candidates g env evd filter1 ev1 ev2 in
+ let evd,(evk1',args1) = do_restrict_hyps evd ev1 filter1 candidates1 in
+ evd,mkEvar (evk1',invert_invertible_arg env evd aliases k2 ev2 args1)
+ with
+ | EvarSolvedWhileRestricting (evd,ev1) ->
+ raise (EvarSolvedOnTheFly (evd,ev1))
+ | DoesNotPreserveCandidateRestriction | NotEnoughInformationToInvert ->
+ raise (CannotProject filter1)
+ else
+ raise (CannotProject filter1)
+
+let solve_evar_evar_l2r f g env evd aliases ev1 (evk2,_ as ev2) =
+ try
+ let evd,body = project_evar_on_evar g env evd aliases 0 ev1 ev2 in
+ Evd.define evk2 body evd
+ with EvarSolvedOnTheFly (evd,c) ->
+ f env evd ev2 c
+
+let solve_evar_evar ?(force=false) f g env evd (evk1,args1 as ev1) (evk2,args2 as ev2) =
+ if are_canonical_instances args1 args2 env then
+ (* If instances are canonical, we solve the problem in linear time *)
+ let sign = evar_filtered_context (Evd.find evd evk2) in
+ let id_inst = Array.map (fun (id,_,_) -> mkVar id) (Array.of_list sign) in
+ Evd.define evk2 (mkEvar(evk1,id_inst)) evd
+ else
+ let evd,ev1,ev2 =
+ (* If an evar occurs in the instance of the other evar and the
+ use of an heuristic is forced, we restrict *)
+ if force then ensure_evar_independent g env evd ev1 ev2 else (evd,ev1,ev2) in
+ let aliases = make_alias_map env in
+ try solve_evar_evar_l2r f g env evd aliases ev1 ev2
+ with CannotProject filter1 ->
+ try solve_evar_evar_l2r f g env evd aliases ev2 ev1
+ with CannotProject filter2 ->
+ postpone_evar_evar f env evd filter1 ev1 filter2 ev2
+
+type conv_fun =
+ env -> evar_map -> conv_pb -> constr -> constr -> evar_map * bool
+
+let check_evar_instance evd evk1 body conv_algo =
+ let evi = Evd.find evd evk1 in
+ let evenv = evar_env evi in
+ (* FIXME: The body might be ill-typed when this is called from w_merge *)
+ let ty =
+ try Retyping.get_type_of evenv evd body
+ with _ -> error "Ill-typed evar instance"
+ in
+ let evd,b = conv_algo evenv evd Reduction.CUMUL ty evi.evar_concl in
+ if b then evd else
+ user_err_loc (fst (evar_source evk1 evd),"",
+ str "Unable to find a well-typed instantiation")
+
+(* Solve pbs ?e[t1..tn] = ?e[u1..un] which arise often in fixpoint
+ * definitions. We try to unify the ti with the ui pairwise. The pairs
+ * that don't unify are discarded (i.e. ?e is redefined so that it does not
+ * depend on these args). *)
+
+let solve_refl ?(can_drop=false) conv_algo env evd evk argsv1 argsv2 =
+ if Array.equal eq_constr argsv1 argsv2 then evd else
+ (* Filter and restrict if needed *)
+ let untypedfilter =
+ restrict_upon_filter evd evk
+ (fun (a1,a2) -> snd (conv_algo env evd Reduction.CONV a1 a2))
+ (List.combine (Array.to_list argsv1) (Array.to_list argsv2)) in
+ let candidates = filter_candidates evd evk untypedfilter None in
+ let filter = match untypedfilter with
+ | None -> None
+ | Some filter -> closure_of_filter evd evk filter in
+ let evd,ev1 = restrict_applied_evar evd (evk,argsv1) filter candidates in
+ if Int.equal (fst ev1) evk && can_drop then (* No refinement *) evd else
+ (* either progress, or not allowed to drop, e.g. to preserve possibly *)
+ (* informative equations such as ?e[x:=?y]=?e[x:=?y'] where we don't know *)
+ (* if e can depend on x until ?y is not resolved, or, conversely, we *)
+ (* don't know if ?y has to be unified with ?y, until e is resolved *)
+ let argsv2 = restrict_instance evd evk filter argsv2 in
+ let ev2 = (fst ev1,argsv2) in
+ (* Leave a unification problem *)
+ Evd.add_conv_pb (Reduction.CONV,env,mkEvar ev1,mkEvar ev2) evd
+
+(* If the evar can be instantiated by a finite set of candidates known
+ in advance, we check which of them apply *)
+
+exception NoCandidates
+
+let solve_candidates conv_algo env evd (evk,argsv as ev) rhs =
+ let evi = Evd.find evd evk in
+ let args = Array.to_list argsv in
+ match evi.evar_candidates with
+ | None -> raise NoCandidates
+ | Some l ->
+ let l' =
+ List.map_filter
+ (filter_compatible_candidates conv_algo env evd evi args rhs) l in
+ match l' with
+ | [] -> error_cannot_unify env evd (mkEvar ev, rhs)
+ | [c,evd] ->
+ (* solve_candidates might have been called recursively in the mean *)
+ (* time and the evar been solved by the filtering process *)
+ if Evd.is_undefined evd evk then Evd.define evk c evd else evd
+ | l when List.length l < List.length l' ->
+ let candidates = List.map fst l in
+ restrict_evar evd evk None (Some candidates)
+ | l -> evd
+
+(* We try to instantiate the evar assuming the body won't depend
+ * on arguments that are not Rels or Vars, or appearing several times
+ * (i.e. we tackle a generalization of Miller-Pfenning patterns unification)
+ *
+ * 1) Let "env |- ?ev[hyps:=args] = rhs" be the unification problem
+ * 2) We limit it to a patterns unification problem "env |- ev[subst] = rhs"
+ * where only Rel's and Var's are relevant in subst
+ * 3) We recur on rhs, "imitating" the term, and failing if some Rel/Var is
+ * not in the scope of ?ev. For instance, the problem
+ * "y:nat |- ?x[] = y" where "|- ?1:nat" is not satisfiable because
+ * ?1 would be instantiated by y which is not in the scope of ?1.
+ * 4) We try to "project" the term if the process of imitation fails
+ * and that only one projection is possible
+ *
+ * Note: we don't assume rhs in normal form, it may fail while it would
+ * have succeeded after some reductions.
+ *
+ * This is the work of [invert_definition Γ Σ ?ev[hyps:=args] c]
+ * Precondition: Σ; Γ, y1..yk |- c /\ Σ; Γ |- u1..un
+ * Postcondition: if φ(x1..xn) is returned then
+ * Σ; Γ, y1..yk |- φ(u1..un) = c /\ x1..xn |- φ(x1..xn)
+ *)
+
+exception NotInvertibleUsingOurAlgorithm of constr
+exception NotEnoughInformationToProgress of (Id.t * evar_projection) list
+exception OccurCheckIn of evar_map * constr
+
+let rec invert_definition conv_algo choose env evd (evk,argsv as ev) rhs =
+ let aliases = make_alias_map env in
+ let evdref = ref evd in
+ let progress = ref false in
+ let evi = Evd.find evd evk in
+ let subst,cstr_subst = make_projectable_subst aliases evd evi argsv in
+
+ (* Projection *)
+ let project_variable t =
+ (* Evar/Var problem: unifiable iff variable projectable from ev subst *)
+ try
+ let sols = find_projectable_vars true aliases !evdref t subst in
+ let c, p = match sols with
+ | [] -> raise Not_found
+ | [id,p] -> (mkVar id, p)
+ | (id,p)::_::_ ->
+ if choose then (mkVar id, p) else raise (NotUniqueInType sols)
+ in
+ let ty = lazy (Retyping.get_type_of env !evdref t) in
+ let evd = do_projection_effects (evar_define conv_algo) env ty !evdref p in
+ evdref := evd;
+ c
+ with
+ | Not_found -> raise (NotInvertibleUsingOurAlgorithm t)
+ | NotUniqueInType sols ->
+ if not !progress then
+ raise (NotEnoughInformationToProgress sols);
+ (* No unique projection but still restrict to where it is possible *)
+ (* materializing is necessary, but is restricting useful? *)
+ let ty = find_solution_type (evar_filtered_env evi) sols in
+ let sign = evar_filtered_context evi in
+ let ty' = instantiate_evar sign ty (Array.to_list argsv) in
+ let (evd,evar,(evk',argsv' as ev')) =
+ materialize_evar (evar_define conv_algo) env !evdref 0 ev ty' in
+ let ts = expansions_of_var aliases t in
+ let test c = isEvar c or List.mem c ts in
+ let filter = Array.map_to_list test argsv' in
+ let filter = apply_subfilter (evar_filter (Evd.find_undefined evd evk)) filter in
+
+ let filter = closure_of_filter evd evk' filter in
+ let candidates = extract_candidates sols in
+ let evd = match candidates with
+ | None ->
+ let evd, ev'' = restrict_applied_evar evd ev' filter None in
+ Evd.add_conv_pb (Reduction.CONV,env,mkEvar ev'',t) evd
+ | Some _ ->
+ restrict_evar evd evk' filter candidates
+ in
+ evdref := evd;
+ evar in
+
+ let rec imitate (env',k as envk) t =
+ let t = whd_evar !evdref t in
+ match kind_of_term t with
+ | Rel i when i>k ->
+ (match pi2 (Environ.lookup_rel (i-k) env') with
+ | None -> project_variable (mkRel (i-k))
+ | Some b ->
+ try project_variable (mkRel (i-k))
+ with NotInvertibleUsingOurAlgorithm _ -> imitate envk (lift i b))
+ | Var id ->
+ (match pi2 (Environ.lookup_named id env') with
+ | None -> project_variable t
+ | Some b ->
+ try project_variable t
+ with NotInvertibleUsingOurAlgorithm _ -> imitate envk b)
+ | Evar (evk',args' as ev') ->
+ if Int.equal evk evk' then raise (OccurCheckIn (evd,rhs));
+ (* Evar/Evar problem (but left evar is virtual) *)
+ let aliases = lift_aliases k aliases in
+ (try
+ let ev = (evk,Array.map (lift k) argsv) in
+ let evd,body = project_evar_on_evar conv_algo env' !evdref aliases k ev' ev in
+ evdref := evd;
+ body
+ with
+ | EvarSolvedOnTheFly (evd,t) -> evdref:=evd; imitate envk t
+ | CannotProject filter' ->
+ assert !progress;
+ (* Make the virtual left evar real *)
+ let ty = get_type_of env' !evdref t in
+ let (evd,evar'',ev'') =
+ materialize_evar (evar_define conv_algo) env' !evdref k ev ty in
+ (* materialize_evar may instantiate ev' by another evar; adjust it *)
+ let (evk',args' as ev') = normalize_evar evd ev' in
+ let evd =
+ (* Try to project (a restriction of) the left evar ... *)
+ try
+ let evd,body = project_evar_on_evar conv_algo env' evd aliases 0 ev'' ev' in
+ Evd.define evk' body evd
+ with
+ | EvarSolvedOnTheFly _ -> assert false (* ev has no candidates *)
+ | CannotProject filter'' ->
+ (* ... or postpone the problem *)
+ postpone_evar_evar (evar_define conv_algo) env' evd filter'' ev'' filter' ev' in
+ evdref := evd;
+ evar'')
+ | _ ->
+ progress := true;
+ match
+ let c,args = decompose_app_vect t in
+ match kind_of_term c with
+ | Construct cstr when noccur_between 1 k t ->
+ (* This is common case when inferring the return clause of match *)
+ (* (currently rudimentary: we do not treat the case of multiple *)
+ (* possible inversions; we do not treat overlap with a possible *)
+ (* alternative inversion of the subterms of the constructor, etc)*)
+ (match find_projectable_constructor env evd cstr k args cstr_subst with
+ | _::_ as l -> Some (List.map mkVar l)
+ | _ -> None)
+ | _ -> None
+ with
+ | Some l ->
+ let ty = get_type_of env' !evdref t in
+ let candidates =
+ try
+ let t =
+ map_constr_with_full_binders (fun d (env,k) -> push_rel d env, k+1)
+ imitate envk t in
+ t::l
+ with _ -> l in
+ (match candidates with
+ | [x] -> x
+ | _ ->
+ let (evd,evar'',ev'') =
+ materialize_evar (evar_define conv_algo) env' !evdref k ev ty in
+ evdref := restrict_evar evd (fst ev'') None (Some candidates);
+ 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 in
+
+ let rhs = whd_beta evd rhs (* heuristic *) in
+ let body = imitate (env,0) rhs in
+ (!evdref,body)
+
+(* [define] tries to solve the problem "?ev[args] = rhs" when "?ev" is
+ * an (uninstantiated) evar such that "hyps |- ?ev : typ". Otherwise said,
+ * [define] tries to find an instance lhs such that
+ * "lhs [hyps:=args]" unifies to rhs. The term "lhs" must be closed in
+ * context "hyps" and not referring to itself.
+ *)
+
+and evar_define conv_algo ?(choose=false) env evd (evk,argsv as ev) rhs =
+ match kind_of_term rhs with
+ | Evar (evk2,argsv2 as ev2) ->
+ if Int.equal evk evk2 then
+ solve_refl ~can_drop:choose conv_algo env evd evk argsv argsv2
+ else
+ solve_evar_evar ~force:choose
+ (evar_define conv_algo) conv_algo env evd ev ev2
+ | _ ->
+ try solve_candidates conv_algo env evd ev rhs
+ with NoCandidates ->
+ try
+ let (evd',body) = invert_definition conv_algo choose env evd ev rhs in
+ if occur_meta body then error "Meta cannot occur in evar body.";
+ (* invert_definition may have instantiate some evars of rhs with evk *)
+ (* so we recheck acyclicity *)
+ if occur_evar evk body then raise (OccurCheckIn (evd',body));
+ (* needed only if an inferred type *)
+ let body = refresh_universes body in
+(* Cannot strictly type instantiations since the unification algorithm
+ * does not unify applications from left to right.
+ * e.g problem f x == g y yields x==y and f==g (in that order)
+ * Another problem is that type variables are evars of type Type
+ let _ =
+ try
+ let env = evar_filtered_env evi in
+ let ty = evi.evar_concl in
+ Typing.check env evd' body ty
+ with e ->
+ msg_info
+ (str "Ill-typed evar instantiation: " ++ fnl() ++
+ pr_evar_map evd' ++ fnl() ++
+ str "----> " ++ int ev ++ str " := " ++
+ print_constr body);
+ raise e in*)
+ let evd' = Evd.define evk body evd' in
+ check_evar_instance evd' evk body conv_algo
+ with
+ | NotEnoughInformationToProgress sols ->
+ postpone_non_unique_projection env evd ev sols rhs
+ | NotInvertibleUsingOurAlgorithm t ->
+ error_not_clean env evd evk t (evar_source evk evd)
+ | OccurCheckIn (evd,rhs) ->
+ (* last chance: rhs actually reduces to ev *)
+ let c = whd_betadeltaiota env evd rhs in
+ match kind_of_term c with
+ | Evar (evk',argsv2) when Int.equal evk evk' ->
+ solve_refl
+ (fun env sigma pb c c' -> (evd,is_fconv pb env sigma c c'))
+ env evd evk argsv argsv2
+ | _ ->
+ error_occur_check env evd evk rhs
+
+(* This code (i.e. solve_pb, etc.) takes a unification
+ * problem, and tries to solve it. If it solves it, then it removes
+ * all the conversion problems, and re-runs conversion on each one, in
+ * the hopes that the new solution will aid in solving them.
+ *
+ * The kinds of problems it knows how to solve are those in which
+ * the usable arguments of an existential var are all themselves
+ * universal variables.
+ * The solution to this problem is to do renaming for the Var's,
+ * to make them match up with the Var's which are found in the
+ * hyps of the existential, to do a "pop" for each Rel which is
+ * not an argument of the existential, and a subst1 for each which
+ * is, again, with the corresponding variable. This is done by
+ * define
+ *
+ * Thus, we take the arguments of the existential which we are about
+ * to assign, and zip them with the identifiers in the hypotheses.
+ * Then, we process all the Var's in the arguments, and sort the
+ * Rel's into ascending order. Then, we just march up, doing
+ * subst1's and pop's.
+ *
+ * NOTE: We can do this more efficiently for the relative arguments,
+ * by building a long substituend by hand, but this is a pain in the
+ * ass.
+ *)
+
+let status_changed lev (pbty,_,t1,t2) =
+ (try ExistentialSet.mem (head_evar t1) lev with NoHeadEvar -> false) or
+ (try ExistentialSet.mem (head_evar t2) lev with NoHeadEvar -> false)
+
+let reconsider_conv_pbs conv_algo evd =
+ let (evd,pbs) = extract_changed_conv_pbs evd status_changed in
+ List.fold_left
+ (fun (evd,b as p) (pbty,env,t1,t2) ->
+ if b then conv_algo env evd pbty t1 t2 else p) (evd,true)
+ pbs
+
+(* Tries to solve problem t1 = t2.
+ * Precondition: t1 is an uninstantiated evar
+ * Returns an optional list of evars that were instantiated, or None
+ * if the problem couldn't be solved. *)
+
+(* Rq: uncomplete algorithm if pbty = CONV_X_LEQ ! *)
+let solve_simple_eqn conv_algo ?(choose=false) env evd (pbty,(evk1,args1 as ev1),t2) =
+ try
+ let t2 = whd_betaiota evd t2 in (* includes whd_evar *)
+ let evd =
+ match pbty with
+ | Some true when isEvar t2 ->
+ add_conv_pb (Reduction.CUMUL,env,mkEvar ev1,t2) evd
+ | Some false when isEvar t2 ->
+ add_conv_pb (Reduction.CUMUL,env,t2,mkEvar ev1) evd
+ | _ ->
+ evar_define conv_algo ~choose env evd ev1 t2 in
+ reconsider_conv_pbs conv_algo evd
+ with e when precatchable_exception e ->
+ (evd,false)
+
diff --git a/pretyping/evarsolve.mli b/pretyping/evarsolve.mli
new file mode 100644
index 000000000..6c7635449
--- /dev/null
+++ b/pretyping/evarsolve.mli
@@ -0,0 +1,48 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+open Term
+open Evd
+open Environ
+
+(** 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
+
+type conv_fun =
+ env -> evar_map -> conv_pb -> constr -> constr -> evar_map * bool
+
+(** [evar_define choose env ev c] try to instantiate [ev] with [c] (typed in [env]),
+ possibly solving related unification problems, possibly leaving open
+ some problems that cannot be solved in a unique way (except if choose is
+ true); fails if the instance is not valid for the given [ev] *)
+val evar_define : conv_fun -> ?choose:bool -> env -> evar_map ->
+ existential -> constr -> evar_map
+
+val solve_refl : ?can_drop:bool -> conv_fun -> env -> evar_map ->
+ existential_key -> constr array -> constr array -> evar_map
+
+val solve_evar_evar : ?force:bool ->
+ (env -> evar_map -> existential -> constr -> evar_map) -> conv_fun ->
+ env -> evar_map -> existential -> existential -> evar_map
+
+val solve_simple_eqn : conv_fun -> ?choose:bool -> env -> evar_map ->
+ bool option * existential * constr -> evar_map * bool
+
+val reconsider_conv_pbs : conv_fun -> evar_map -> evar_map * bool
+
+val is_unification_pattern_evar : env -> evar_map -> existential -> constr list ->
+ constr -> constr list option
+
+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 check_evar_instance : evar_map -> existential_key -> constr -> conv_fun ->
+ evar_map
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 0c339df4e..39d6a59db 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -158,27 +158,6 @@ let whd_head_evar_stack sigma c =
let whd_head_evar sigma c = applist (whd_head_evar_stack sigma c)
-let noccur_evar env evd evk c =
- let rec occur_rec k c = match kind_of_term c with
- | Evar (evk',args' as ev') ->
- (match safe_evar_value evd ev' with
- | Some c -> occur_rec k c
- | None ->
- if Int.equal evk evk' then raise Occur
- else Array.iter (occur_rec k) args')
- | Rel i when i > k ->
- (match pi2 (Environ.lookup_rel (i-k) env) with
- | None -> ()
- | Some b -> occur_rec k (lift i b))
- | _ -> iter_constr_with_binders succ occur_rec k c
- in
- try occur_rec 0 c; true with Occur -> false
-
-let normalize_evar evd ev =
- match kind_of_term (whd_evar evd (mkEvar ev)) with
- | Evar (evk,args) -> (evk,args)
- | _ -> assert false
-
(**********************)
(* Creating new metas *)
(**********************)
@@ -266,14 +245,17 @@ let non_instantiated sigma =
(* Manipulating filters *)
(************************)
-let apply_subfilter filter subfilter =
- fst (List.fold_right (fun oldb (l,filter) ->
- if oldb then List.hd filter::l,List.tl filter else (false::l,filter))
- filter ([], List.rev subfilter))
-
let extract_subfilter initial_filter refined_filter =
snd (List.filter2 (fun b1 b2 -> b1) initial_filter refined_filter)
+let make_pure_subst evi args =
+ snd (List.fold_right
+ (fun (id,b,c) (args,l) ->
+ match args with
+ | a::rest -> (rest, (id,a)::l)
+ | _ -> anomaly (Pp.str "Instance does not match its signature"))
+ (evar_filtered_context evi) (Array.rev_to_list args,[]))
+
(**********************)
(* Creating new evars *)
(**********************)
@@ -376,62 +358,6 @@ let e_new_evar evdref env ?(src=(Loc.ghost,Evar_kinds.InternalHole)) ?filter ?ca
evdref := evd';
ev
-(*------------------------------------*
- * Restricting existing evars *
- *------------------------------------*)
-
-let rec eq_filter l1 l2 = match l1, l2 with
-| [], [] -> true
-| h1 :: l1, h2 :: l2 ->
- (if h1 then h2 else not h2) && eq_filter l1 l2
-| _ -> false
-
-let restrict_evar_key evd evk filter candidates =
- match filter, candidates with
- | None, None -> evd, evk
- | _ ->
- let evi = Evd.find_undefined evd evk in
- let oldfilter = evar_filter evi in
- begin match filter, candidates with
- | Some filter, None when eq_filter oldfilter filter ->
- evd, evk
- | _ ->
- let filter = match filter with
- | None -> evar_filter evi
- | Some filter -> filter in
- let candidates = match candidates with
- | None -> evi.evar_candidates
- | Some _ -> candidates in
- let ccl = evi.evar_concl in
- let sign = evar_hyps evi in
- let src = evi.evar_source in
- let evd,newevk = new_pure_evar evd sign ccl ~src ~filter ?candidates in
- let _, ctxt = List.filter2 (fun b c -> b) filter (evar_context evi) in
- let id_inst = Array.of_list (List.map (fun (id,_,_) -> mkVar id) ctxt) in
- Evd.define evk (mkEvar(newevk,id_inst)) evd,newevk
- end
-
-(* Restrict an applied evar and returns its restriction in the same context *)
-let restrict_applied_evar evd (evk,argsv) filter candidates =
- let evd,newevk = restrict_evar_key evd evk filter candidates in
- let newargsv = match filter with
- | None -> (* optim *) argsv
- | Some filter ->
- let evi = Evd.find evd evk in
- let subfilter = extract_subfilter (evar_filter evi) filter in
- Array.filter_with subfilter argsv in
- evd,(newevk,newargsv)
-
-(* Restrict an evar in the current evar_map *)
-let restrict_evar evd evk filter candidates =
- fst (restrict_evar_key evd evk filter candidates)
-
-(* Restrict an evar in the current evar_map *)
-let restrict_instance evd evk filter argsv =
- match filter with None -> argsv | Some filter ->
- let evi = Evd.find evd evk in
- Array.filter_with (extract_subfilter (evar_filter evi) filter) argsv
-
(* 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) =
@@ -442,156 +368,6 @@ let generalize_evar_over_rels sigma (ev,args) =
if isRel a then (mkNamedProd_or_LetIn d c,a::inst) else x)
(evi.evar_concl,[]) (Array.to_list args) sign
-(***************************************)
-(* Managing chains of local definitons *)
-(***************************************)
-
-(* Expand rels and vars that are bound to other rels or vars so that
- dependencies in variables are canonically associated to the most ancient
- variable in its family of aliased variables *)
-
-let compute_var_aliases sign =
- List.fold_right (fun (id,b,c) aliases ->
- match b with
- | Some t ->
- (match kind_of_term t with
- | Var id' ->
- let aliases_of_id =
- try Id.Map.find id' aliases with Not_found -> [] in
- Id.Map.add id (aliases_of_id@[t]) aliases
- | _ ->
- Id.Map.add id [t] aliases)
- | None -> aliases)
- sign Id.Map.empty
-
-let compute_rel_aliases var_aliases rels =
- snd (List.fold_right (fun (_,b,t) (n,aliases) ->
- (n-1,
- match b with
- | Some t ->
- (match kind_of_term t with
- | Var id' ->
- let aliases_of_n =
- try Id.Map.find id' var_aliases with Not_found -> [] in
- Int.Map.add n (aliases_of_n@[t]) aliases
- | Rel p ->
- let aliases_of_n =
- try Int.Map.find (p+n) aliases with Not_found -> [] in
- Int.Map.add n (aliases_of_n@[mkRel (p+n)]) aliases
- | _ ->
- Int.Map.add n [lift n t] aliases)
- | None -> aliases))
- rels (List.length rels,Int.Map.empty))
-
-let make_alias_map env =
- (* We compute the chain of aliases for each var and rel *)
- let var_aliases = compute_var_aliases (named_context env) in
- let rel_aliases = compute_rel_aliases var_aliases (rel_context env) in
- (var_aliases,rel_aliases)
-
-let lift_aliases n (var_aliases,rel_aliases as aliases) =
- if Int.equal n 0 then aliases else
- (var_aliases,
- Int.Map.fold (fun p l -> Int.Map.add (p+n) (List.map (lift n) l))
- rel_aliases Int.Map.empty)
-
-let get_alias_chain_of aliases x = match kind_of_term x with
- | Rel n -> (try Int.Map.find n (snd aliases) with Not_found -> [])
- | Var id -> (try Id.Map.find id (fst aliases) with Not_found -> [])
- | _ -> []
-
-let normalize_alias_opt aliases x =
- match get_alias_chain_of aliases x with
- | [] -> None
- | a::_ when isRel a or isVar a -> Some a
- | [_] -> None
- | _::a::_ -> Some a
-
-let normalize_alias aliases x =
- match normalize_alias_opt aliases x with
- | Some a -> a
- | None -> x
-
-let normalize_alias_var var_aliases id =
- destVar (normalize_alias (var_aliases,Int.Map.empty) (mkVar id))
-
-let extend_alias (_,b,_) (var_aliases,rel_aliases) =
- let rel_aliases =
- Int.Map.fold (fun n l -> Int.Map.add (n+1) (List.map (lift 1) l))
- rel_aliases Int.Map.empty in
- let rel_aliases =
- match b with
- | Some t ->
- (match kind_of_term t with
- | Var id' ->
- let aliases_of_binder =
- try Id.Map.find id' var_aliases with Not_found -> [] in
- Int.Map.add 1 (aliases_of_binder@[t]) rel_aliases
- | Rel p ->
- let aliases_of_binder =
- try Int.Map.find (p+1) rel_aliases with Not_found -> [] in
- Int.Map.add 1 (aliases_of_binder@[mkRel (p+1)]) rel_aliases
- | _ ->
- Int.Map.add 1 [lift 1 t] rel_aliases)
- | None -> rel_aliases in
- (var_aliases, rel_aliases)
-
-let expand_alias_once aliases x =
- match get_alias_chain_of aliases x with
- | [] -> None
- | l -> Some (List.last l)
-
-let expansions_of_var aliases x =
- match get_alias_chain_of aliases x with
- | [] -> [x]
- | a::_ as l when isRel a || isVar a -> x :: List.rev l
- | _::l -> x :: List.rev l
-
-let expansion_of_var aliases x =
- match get_alias_chain_of aliases x with
- | [] -> x
- | a::_ -> a
-
-let rec expand_vars_in_term_using 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 expand_vars_in_term env = expand_vars_in_term_using (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
- let cache_rel = ref Int.Set.empty and cache_var = ref Id.Set.empty in
- let is_in_cache depth = function
- | Rel n -> Int.Set.mem (n-depth) !cache_rel
- | Var s -> Id.Set.mem s !cache_var
- | _ -> false in
- let put_in_cache depth = function
- | Rel n -> cache_rel := Int.Set.add (n-depth) !cache_rel
- | Var s -> cache_var := Id.Set.add s !cache_var
- | _ -> () in
- let rec frec (aliases,depth) c =
- match kind_of_term c with
- | Rel _ | Var _ as ck ->
- if is_in_cache depth ck then () else begin
- put_in_cache depth ck;
- let c = expansion_of_var aliases c in
- match kind_of_term c with
- | Var id -> acc2 := Id.Set.add id !acc2
- | Rel n -> if n >= depth+1 then acc1 := Int.Set.add (n-depth) !acc1
- | _ -> frec (aliases,depth) c end
- | Const _ | Ind _ | Construct _ ->
- acc2 := List.fold_right Id.Set.add (vars_of_global (Global.env()) c) !acc2
- | _ ->
- iter_constr_with_full_binders
- (fun d (aliases,depth) -> (extend_alias d aliases,depth+1))
- frec (aliases,depth) c
- in
- frec (aliases,0) c;
- (!acc1,!acc2)
-
(************************************)
(* Removing a dependency in an evar *)
(************************************)
@@ -708,1111 +484,6 @@ let clear_hyps_in_evi evdref hyps concl ids =
in
(nhyps,nconcl)
-(********************************)
-(* Managing pattern-unification *)
-(********************************)
-
-let rec expand_and_check_vars aliases = function
- | [] -> []
- | a::l when isRel a or isVar a ->
- let a = expansion_of_var aliases a in
- if isRel a or isVar a then a :: expand_and_check_vars aliases l
- else raise Exit
- | _ ->
- raise Exit
-
-module Constrhash = Hashtbl.Make
- (struct type t = constr
- let equal = eq_constr
- let hash = hash_constr
- end)
-
-let constr_list_distinct l =
- let visited = Constrhash.create 23 in
- let rec loop = function
- | h::t ->
- if Constrhash.mem visited h then false
- else (Constrhash.add visited h h; loop t)
- | [] -> true
- in loop l
-
-let get_actual_deps aliases l t =
- if occur_meta_or_existential t then
- (* Probably no restrictions on allowed vars in presence of evars *)
- l
- else
- (* Probably strong restrictions coming from t being evar-closed *)
- let (fv_rels,fv_ids) = free_vars_and_rels_up_alias_expansion aliases t in
- List.filter (fun c ->
- match kind_of_term c with
- | Var id -> Id.Set.mem id fv_ids
- | Rel n -> Int.Set.mem n fv_rels
- | _ -> assert false) l
-
-let remove_instance_local_defs evd evk args =
- let evi = Evd.find evd evk in
- let rec aux = function
- | (_,Some _,_)::sign, a::args -> aux (sign,args)
- | (_,None,_)::sign, a::args -> a::aux (sign,args)
- | [], [] -> []
- | _ -> assert false in
- aux (evar_filtered_context evi, args)
-
-(* Check if an applied evar "?X[args] l" is a Miller's pattern *)
-
-let find_unification_pattern_args env 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
- | _ -> None
- else
- None
-
-let is_unification_pattern_meta env 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
- | _ -> None
- else
- None
-
-let is_unification_pattern_evar env evd (evk,args) l t =
- if List.for_all (fun x -> isRel x || isVar x) l & noccur_evar env evd evk t
- then
- let args = remove_instance_local_defs evd evk (Array.to_list args) in
- let n = List.length args in
- match find_unification_pattern_args env (args @ l) t with
- | Some l -> Some (List.skipn n l)
- | _ -> None
- else
- None
-
-let is_unification_pattern_pure_evar env evd (evk,args) t =
- let is_ev = is_unification_pattern_evar env evd (evk,args) [] t in
- match is_ev with
- | None -> false
- | Some _ -> true
-
-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
- | Evar ev -> is_unification_pattern_evar env evd ev l t
- | _ -> None
-
-(* From a unification problem "?X l = c", build "\x1...xn.(term1 l2)"
- (pattern unification). It is assumed that l is made of rel's that
- are distinct and not bound to aliases. *)
-(* It is also assumed that c does not contain metas because metas
- *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 c' = List.fold_right (fun a c ->
- let c' = subst_term (lift 1 a) (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 ->
- let d = map_rel_declaration (lift n) (lookup_rel n env) in
- mkLambda_or_LetIn d c'
- | Var id ->
- let d = lookup_named id env in mkNamedLambda_or_LetIn d c'
- | _ -> assert false)
- l c in
- (* Warning: we may miss some opportunity to eta-reduce more since c'
- is not in normal form *)
- whd_eta c'
-
-(*****************************************)
-(* Refining/solving unification problems *)
-(*****************************************)
-
-(* Knowing that [Gamma |- ev : T] and that [ev] is applied to [args],
- * [make_projectable_subst ev args] builds the substitution [Gamma:=args].
- * If a variable and an alias of it are bound to the same instance, we skip
- * the alias (we just use eq_constr -- instead of conv --, since anyway,
- * only instances that are variables -- or evars -- are later considered;
- * morever, we can bet that similar instances came at some time from
- * the very same substitution. The removal of aliased duplicates is
- * useful to ensure the uniqueness of a projection.
-*)
-
-let make_projectable_subst aliases sigma evi args =
- let sign = evar_filtered_context evi in
- let evar_aliases = compute_var_aliases sign in
- let (_,full_subst,cstr_subst) =
- List.fold_right
- (fun (id,b,c) (args,all,cstrs) ->
- match b,args with
- | None, a::rest ->
- let a = whd_evar sigma a in
- let cstrs =
- let a',args = decompose_app_vect a in
- match kind_of_term a' with
- | Construct cstr ->
- let l = try Constrmap.find cstr cstrs with Not_found -> [] in
- Constrmap.add cstr ((args,id)::l) cstrs
- | _ -> cstrs in
- (rest,Id.Map.add id [a,normalize_alias_opt aliases a,id] all,cstrs)
- | Some c, a::rest ->
- let a = whd_evar sigma a in
- (match kind_of_term c with
- | Var id' ->
- let idc = normalize_alias_var evar_aliases id' in
- let sub = try Id.Map.find idc all with Not_found -> [] in
- if List.exists (fun (c,_,_) -> eq_constr a c) sub then
- (rest,all,cstrs)
- else
- (rest,
- Id.Map.add idc ((a,normalize_alias_opt aliases a,id)::sub) all,
- cstrs)
- | _ ->
- (rest,Id.Map.add id [a,normalize_alias_opt aliases a,id] all,cstrs))
- | _ -> anomaly (Pp.str "Instance does not match its signature"))
- sign (Array.rev_to_list args,Id.Map.empty,Constrmap.empty) in
- (full_subst,cstr_subst)
-
-let make_pure_subst evi args =
- snd (List.fold_right
- (fun (id,b,c) (args,l) ->
- match args with
- | a::rest -> (rest, (id,a)::l)
- | _ -> anomaly (Pp.str "Instance does not match its signature"))
- (evar_filtered_context evi) (Array.rev_to_list args,[]))
-
-(*------------------------------------*
- * operations on the evar constraints *
- *------------------------------------*)
-
-(* We have a unification problem Σ; Γ |- ?e[u1..uq] = t : s where ?e is not yet
- * declared in Σ but yet known to be declarable in some context x1:T1..xq:Tq.
- * [define_evar_from_virtual_equation ... Γ Σ t (x1:T1..xq:Tq) .. (u1..uq) (x1..xq)]
- * declares x1:T1..xq:Tq |- ?e : s such that ?e[u1..uq] = t holds.
- *)
-
-let define_evar_from_virtual_equation define_fun env evd t_in_env sign filter inst_in_env =
- let ty_t_in_env = Retyping.get_type_of env evd t_in_env in
- let evd,evar_in_env = new_evar_instance sign evd ty_t_in_env ~filter inst_in_env in
- let t_in_env = whd_evar evd t_in_env in
- let evd = define_fun env evd (destEvar evar_in_env) t_in_env in
- let ids = List.map pi1 (named_context_of_val sign) in
- let inst_in_sign = List.map mkVar (List.filter_with filter ids) in
- let evar_in_sign = mkEvar (fst (destEvar evar_in_env), Array.of_list inst_in_sign) in
- (evd,whd_evar evd evar_in_sign)
-
-(* We have x1..xq |- ?e1 : τ and had to solve something like
- * Σ; Γ |- ?e1[u1..uq] = (...\y1 ... \yk ... c), where c is typically some
- * ?e2[v1..vn], hence flexible. We had to go through k binders and now
- * virtually have x1..xq, y1'..yk' | ?e1' : τ' and the equation
- * Γ, y1..yk |- ?e1'[u1..uq y1..yk] = c.
- * [materialize_evar Γ evd k (?e1[u1..uq]) τ'] extends Σ with the declaration
- * of ?e1' and returns both its instance ?e1'[x1..xq y1..yk] in an extension
- * of the context of e1 so that e1 can be instantiated by
- * (...\y1' ... \yk' ... ?e1'[x1..xq y1'..yk']),
- * and the instance ?e1'[u1..uq y1..yk] so that the remaining equation
- * ?e1'[u1..uq y1..yk] = c can be registered
- *
- * Note that, because invert_definition does not check types, we need to
- * guess the types of y1'..yn' by inverting the types of y1..yn along the
- * substitution u1..uq.
- *)
-
-let materialize_evar define_fun env evd k (evk1,args1) ty_in_env =
- let evi1 = Evd.find_undefined evd evk1 in
- let env1,rel_sign = env_rel_context_chop k env in
- let sign1 = evar_hyps evi1 in
- let filter1 = evar_filter evi1 in
- let ids1 = List.map pi1 (named_context_of_val sign1) in
- let inst_in_sign = List.map mkVar (List.filter_with filter1 ids1) in
- let (sign2,filter2,inst2_in_env,inst2_in_sign,_,evd,_) =
- List.fold_right (fun (na,b,t_in_env as d) (sign,filter,inst_in_env,inst_in_sign,env,evd,avoid) ->
- let id = next_name_away na avoid in
- let evd,t_in_sign =
- define_evar_from_virtual_equation define_fun env evd t_in_env
- sign filter inst_in_env in
- let evd,b_in_sign = match b with
- | None -> evd,None
- | Some b ->
- let evd,b = define_evar_from_virtual_equation define_fun env evd b
- sign filter inst_in_env in
- evd,Some b in
- (push_named_context_val (id,b_in_sign,t_in_sign) sign,true::filter,
- (mkRel 1)::(List.map (lift 1) inst_in_env),
- (mkRel 1)::(List.map (lift 1) inst_in_sign),
- push_rel d env,evd,id::avoid))
- rel_sign
- (sign1,filter1,Array.to_list args1,inst_in_sign,env1,evd,ids1)
- in
- let evd,ev2ty_in_sign =
- define_evar_from_virtual_equation define_fun env evd ty_in_env
- sign2 filter2 inst2_in_env in
- let evd,ev2_in_sign =
- new_evar_instance sign2 evd ev2ty_in_sign ~filter:filter2 inst2_in_sign in
- let ev2_in_env = (fst (destEvar ev2_in_sign), Array.of_list inst2_in_env) in
- (evd, ev2_in_sign, ev2_in_env)
-
-let restrict_upon_filter evd evk p args =
- let newfilter = List.map p args in
- if List.for_all (fun id -> id) newfilter then
- None
- else
- let oldfullfilter = evar_filter (Evd.find_undefined evd evk) in
- Some (apply_subfilter oldfullfilter newfilter)
-
-(* Inverting constructors in instances (common when inferring type of match) *)
-
-let find_projectable_constructor env evd cstr k args cstr_subst =
- try
- let l = Constrmap.find cstr cstr_subst in
- let args = Array.map (lift (-k)) args in
- let l =
- List.filter (fun (args',id) ->
- (* is_conv is maybe too strong (and source of useless computation) *)
- (* (at least expansion of aliases is needed) *)
- Array.for_all2 (is_conv env evd) args args') l in
- List.map snd l
- with Not_found ->
- []
-
-(* [find_projectable_vars env sigma y subst] finds all vars of [subst]
- * that project on [y]. It is able to find solutions to the following
- * two kinds of problems:
- *
- * - ?n[...;x:=y;...] = y
- * - ?n[...;x:=?m[args];...] = y with ?m[args] = y recursively solvable
- *
- * (see test-suite/success/Fixpoint.v for an example of application of
- * the second kind of problem).
- *
- * The seek for [y] is up to variable aliasing. In case of solutions that
- * differ only up to aliasing, the binding that requires the less
- * steps of alias reduction is kept. At the end, only one solution up
- * to aliasing is kept.
- *
- * [find_projectable_vars] also unifies against evars that themselves mention
- * [y] and recursively.
- *
- * In short, the following situations give the following solutions:
- *
- * problem evar ctxt soluce remark
- * z1; z2:=z1 |- ?ev[z1;z2] = z1 y1:A; y2:=y1 y1 \ thanks to defs kept in
- * z1; z2:=z1 |- ?ev[z1;z2] = z2 y1:A; y2:=y1 y2 / subst and preferring =
- * z1; z2:=z1 |- ?ev[z1] = z2 y1:A y1 thanks to expand_var
- * z1; z2:=z1 |- ?ev[z2] = z1 y1:A y1 thanks to expand_var
- * z3 |- ?ev[z3;z3] = z3 y1:A; y2:=y1 y2 see make_projectable_subst
- *
- * Remark: [find_projectable_vars] assumes that identical instances of
- * variables in the same set of aliased variables are already removed (see
- * [make_projectable_subst])
- *)
-
-type evar_projection =
-| ProjectVar
-| ProjectEvar of existential * evar_info * Id.t * evar_projection
-
-exception NotUnique
-exception NotUniqueInType of (Id.t * evar_projection) list
-
-let rec assoc_up_to_alias sigma aliases y yc = function
- | [] -> raise Not_found
- | (c,cc,id)::l ->
- let c' = whd_evar sigma c in
- if eq_constr y c' then id
- else
- match l with
- | _ :: _ -> assoc_up_to_alias sigma aliases y yc l
- | [] ->
- (* Last chance, we reason up to alias conversion *)
- match (if c == c' then cc else normalize_alias_opt aliases c') with
- | Some cc when eq_constr yc cc -> id
- | _ -> if eq_constr yc c then id else raise Not_found
-
-let rec find_projectable_vars with_evars aliases sigma y subst =
- let yc = normalize_alias aliases y in
- let is_projectable idc idcl subst' =
- (* First test if some [id] aliased to [idc] is bound to [y] in [subst] *)
- try
- let id = assoc_up_to_alias sigma aliases y yc idcl in
- (id,ProjectVar)::subst'
- with Not_found ->
- (* Then test if [idc] is (indirectly) bound in [subst] to some evar *)
- (* projectable on [y] *)
- if with_evars then
- let idcl' = List.filter (fun (c,_,id) -> isEvar c) idcl in
- match idcl' with
- | [c,_,id] ->
- begin
- let (evk,argsv as t) = destEvar c in
- let evi = Evd.find sigma evk in
- let subst,_ = make_projectable_subst aliases sigma evi argsv in
- let l = find_projectable_vars with_evars aliases sigma y subst in
- match l with
- | [id',p] -> (id,ProjectEvar (t,evi,id',p))::subst'
- | _ -> subst'
- end
- | [] -> subst'
- | _ -> anomaly (Pp.str "More than one non var in aliases class of evar instance")
- else
- subst' in
- Id.Map.fold is_projectable subst []
-
-(* [filter_solution] checks if one and only one possible projection exists
- * among a set of solutions to a projection problem *)
-
-let filter_solution = function
- | [] -> raise Not_found
- | (id,p)::_::_ -> raise NotUnique
- | [id,p] -> (mkVar id, p)
-
-let project_with_effects aliases sigma effects t subst =
- let c, p =
- filter_solution (find_projectable_vars false aliases sigma t subst) in
- effects := p :: !effects;
- c
-
-let rec find_solution_type evarenv = function
- | (id,ProjectVar)::l -> pi3 (lookup_named id evarenv)
- | [id,ProjectEvar _] -> (* bugged *) pi3 (lookup_named id evarenv)
- | (id,ProjectEvar _)::l -> find_solution_type evarenv l
- | [] -> assert false
-
-(* In case the solution to a projection problem requires the instantiation of
- * subsidiary evars, [do_projection_effects] performs them; it
- * also try to instantiate the type of those subsidiary evars if their
- * type is an evar too.
- *
- * Note: typing creates new evar problems, which induces a recursive dependency
- * with [define]. To avoid a too large set of recursive functions, we
- * pass [define] to [do_projection_effects] as a parameter.
- *)
-
-let rec do_projection_effects define_fun env ty evd = function
- | ProjectVar -> evd
- | ProjectEvar ((evk,argsv),evi,id,p) ->
- let evd = Evd.define evk (mkVar id) evd in
- (* TODO: simplify constraints involving evk *)
- let evd = do_projection_effects define_fun env ty evd p in
- let ty = whd_betadeltaiota env evd (Lazy.force ty) in
- if not (isSort ty) then
- (* Don't try to instantiate if a sort because if evar_concl is an
- evar it may commit to a univ level which is not the right
- one (however, regarding coercions, because t is obtained by
- unif, we know that no coercion can be inserted) *)
- let subst = make_pure_subst evi argsv in
- let ty' = replace_vars subst evi.evar_concl in
- let ty' = whd_evar evd ty' in
- if isEvar ty' then define_fun env evd (destEvar ty') ty else evd
- else
- evd
-
-(* Assuming Σ; Γ, y1..yk |- c, [invert_arg_from_subst Γ k Σ [x1:=u1..xn:=un] c]
- * tries to return φ(x1..xn) such that equation φ(u1..un) = c is valid.
- * The strategy is to imitate the structure of c and then to invert
- * the variables of c (i.e. rels or vars of Γ) using the algorithm
- * implemented by project_with_effects/find_projectable_vars.
- * It returns either a unique solution or says whether 0 or more than
- * 1 solutions is found.
- *
- * Precondition: Σ; Γ, y1..yk |- c /\ Σ; Γ |- u1..un
- * Postcondition: if φ(x1..xn) is returned then
- * Σ; Γ, y1..yk |- φ(u1..un) = c /\ x1..xn |- φ(x1..xn)
- *
- * The effects correspond to evars instantiated while trying to project.
- *
- * [invert_arg_from_subst] is used on instances of evars. Since the
- * evars are flexible, these instances are potentially erasable. This
- * is why we don't investigate whether evars in the instances of evars
- * are unifiable, to the contrary of [invert_definition].
- *)
-
-type projectibility_kind =
- | NoUniqueProjection
- | UniqueProjection of constr * evar_projection list
-
-type projectibility_status =
- | CannotInvert
- | Invertible of projectibility_kind
-
-let invert_arg_from_subst evd aliases k0 subst_in_env_extended_with_k_binders c_in_env_extended_with_k_binders =
- let effects = ref [] in
- let rec aux k t =
- let t = whd_evar evd t in
- match kind_of_term t with
- | Rel i when i>k0+k -> aux' k (mkRel (i-k))
- | Var id -> aux' k t
- | _ -> map_constr_with_binders succ aux k t
- and aux' k t =
- try project_with_effects aliases evd effects t subst_in_env_extended_with_k_binders
- with Not_found ->
- match expand_alias_once aliases t with
- | None -> raise Not_found
- | Some c -> aux k c in
- try
- let c = aux 0 c_in_env_extended_with_k_binders in
- Invertible (UniqueProjection (c,!effects))
- with
- | Not_found -> CannotInvert
- | NotUnique -> Invertible NoUniqueProjection
-
-let invert_arg fullenv evd aliases k evk subst_in_env_extended_with_k_binders c_in_env_extended_with_k_binders =
- let res = invert_arg_from_subst evd aliases k subst_in_env_extended_with_k_binders c_in_env_extended_with_k_binders in
- match res with
- | Invertible (UniqueProjection (c,_)) when not (noccur_evar fullenv evd evk c)
- ->
- CannotInvert
- | _ ->
- res
-
-exception NotEnoughInformationToInvert
-
-let extract_unique_projections projs =
- List.map (function
- | Invertible (UniqueProjection (c,_)) -> c
- | _ ->
- (* For instance, there are evars with non-invertible arguments and *)
- (* we cannot arbitrarily restrict these evars before knowing if there *)
- (* will really be used; it can also be due to some argument *)
- (* (typically a rel) that is not inversible and that cannot be *)
- (* inverted either because it is needed for typing the conclusion *)
- (* of the evar to project *)
- raise NotEnoughInformationToInvert) projs
-
-let extract_candidates sols =
- try
- Some
- (List.map (function (id,ProjectVar) -> mkVar id | _ -> raise Exit) sols)
- with Exit ->
- None
-
-let invert_invertible_arg fullenv evd aliases k (evk,argsv) args' =
- let evi = Evd.find_undefined evd evk in
- let subst,_ = make_projectable_subst aliases evd evi argsv in
- let projs =
- Array.map_to_list (invert_arg fullenv evd aliases k evk subst) args' in
- Array.of_list (extract_unique_projections projs)
-
-(* Redefines an evar with a smaller context (i.e. it may depend on less
- * variables) such that c becomes closed.
- * Example: in "fun (x:?1) (y:list ?2[x]) => x = y :> ?3[x,y] /\ x = nil bool"
- * ?3 <-- ?1 no pb: env of ?3 is larger than ?1's
- * ?1 <-- list ?2 pb: ?2 may depend on x, but not ?1.
- * What we do is that ?2 is defined by a new evar ?4 whose context will be
- * a prefix of ?2's env, included in ?1's env.
- *
- * If "hyps |- ?e : T" and "filter" selects a subset hyps' of hyps then
- * [do_restrict_hyps evd ?e filter] sets ?e:=?e'[hyps'] and returns ?e'
- * such that "hyps' |- ?e : T"
- *)
-
-let filter_candidates evd evk filter candidates =
- let evi = Evd.find_undefined evd evk in
- let candidates = match candidates with
- | None -> evi.evar_candidates
- | Some _ -> candidates in
- match candidates,filter with
- | None,_ | _, None -> candidates
- | Some l, Some filter ->
- let ids = List.map pi1 (List.filter_with filter (evar_context evi)) in
- Some (List.filter (fun a ->
- List.subset (Id.Set.elements (collect_vars a)) ids) l)
-
-let closure_of_filter evd evk filter =
- let evi = Evd.find_undefined evd evk in
- let vars = collect_vars (evar_concl evi) in
- let ids = List.map pi1 (evar_context evi) in
- let test id b = b || Id.Set.mem id vars in
- let newfilter = List.map2 test ids filter in
- if eq_filter newfilter (evar_filter evi) then None else Some newfilter
-
-let restrict_hyps evd evk filter candidates =
- (* What to do with dependencies?
- Assume we have x:A, y:B(x), z:C(x,y) |- ?e:T(x,y,z) and restrict on y.
- - If y is in a non-erasable position in C(x,y) (i.e. it is not below an
- occurrence of x in the hnf of C), then z should be removed too.
- - If y is in a non-erasable position in T(x,y,z) then the problem is
- unsolvable.
- Computing whether y is erasable or not may be costly and the
- interest for this early detection in practice is not obvious. We let
- it for future work. In any case, thanks to the use of filters, the whole
- (unrestricted) context remains consistent. *)
- let candidates = filter_candidates evd evk (Some filter) candidates in
- let typablefilter = closure_of_filter evd evk filter in
- (typablefilter,candidates)
-
-exception EvarSolvedWhileRestricting of evar_map * constr
-
-let do_restrict_hyps evd (evk,args as ev) filter candidates =
- let filter,candidates = match filter with
- | None -> None,candidates
- | Some filter -> restrict_hyps evd evk filter candidates in
- match candidates,filter with
- | Some [], _ -> error "Not solvable."
- | Some [nc],_ ->
- let evd = Evd.define evk nc evd in
- raise (EvarSolvedWhileRestricting (evd,whd_evar evd (mkEvar ev)))
- | None, None -> evd,ev
- | _ -> restrict_applied_evar evd ev filter candidates
-
-(* [postpone_non_unique_projection] postpones equation of the form ?e[?] = c *)
-(* ?e is assumed to have no candidates *)
-
-let postpone_non_unique_projection env evd (evk,argsv as ev) sols rhs =
- let rhs = expand_vars_in_term env rhs in
- let filter =
- restrict_upon_filter evd evk
- (* Keep only variables that occur in rhs *)
- (* This is not safe: is the variable is a local def, its body *)
- (* may contain references to variables that are removed, leading to *)
- (* a ill-formed context. We would actually need a notion of filter *)
- (* that says that the body is hidden. Note that expand_vars_in_term *)
- (* 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)
- (Array.to_list argsv) in
- let filter = match filter with
- | None -> None
- | Some filter -> closure_of_filter evd evk filter in
- let candidates = extract_candidates sols in
- match candidates with
- | None ->
- (* We made an approximation by not expanding a local definition *)
- let evd,ev = restrict_applied_evar evd ev filter None in
- let pb = (Reduction.CONV,env,mkEvar ev,rhs) in
- Evd.add_conv_pb pb evd
- | Some _ ->
- restrict_evar evd evk filter candidates
-
-(* [postpone_evar_evar] postpones an equation of the form ?e1[?1] = ?e2[?2] *)
-
-let postpone_evar_evar f env evd filter1 ev1 filter2 ev2 =
- (* Leave an equation between (restrictions of) ev1 andv ev2 *)
- try
- let evd,ev1' = do_restrict_hyps evd ev1 filter1 None in
- try
- let evd,ev2' = do_restrict_hyps evd ev2 filter2 None in
- add_conv_pb (Reduction.CONV,env,mkEvar ev1',mkEvar ev2') evd
- with EvarSolvedWhileRestricting (evd,ev2) ->
- (* ev2 solved on the fly *)
- f env evd ev1' ev2
- with EvarSolvedWhileRestricting (evd,ev1) ->
- (* ev1 solved on the fly *)
- f env evd ev2 ev1
-
-(* [solve_evar_evar f Γ Σ ?e1[u1..un] ?e2[v1..vp]] applies an heuristic
- * to solve the equation Σ; Γ ⊢ ?e1[u1..un] = ?e2[v1..vp]:
- * - if there are at most one φj for each vj s.t. vj = φj(u1..un),
- * we first restrict ?e2 to the subset v_k1..v_kq of the vj that are
- * inversible and we set ?e1[x1..xn] := ?e2[φk1(x1..xn)..φkp(x1..xn)]
- * (this is a case of pattern-unification)
- * - symmetrically if there are at most one ψj for each uj s.t.
- * uj = ψj(v1..vp),
- * - otherwise, each position i s.t. ui does not occur in v1..vp has to
- * be restricted and similarly for the vi, and we leave the equation
- * as an open equation (performed by [postpone_evar])
- *
- * Warning: the notion of unique φj is relative to some given class
- * of unification problems
- *
- * Note: argument f is the function used to instantiate evars.
- *)
-
-let are_canonical_instances args1 args2 env =
- let n1 = Array.length args1 in
- let n2 = Array.length args2 in
- let rec aux n = function
- | (id,_,c)::sign
- when n < n1 && isVarId id args1.(n) && isVarId id args2.(n) ->
- aux (n+1) sign
- | [] ->
- let rec aux2 n =
- Int.equal n n1 ||
- (isRelN (n1-n) args1.(n) && isRelN (n1-n) args2.(n) && aux2 (n+1))
- in aux2 n
- | _ -> false in
- Int.equal n1 n2 && aux 0 (named_context env)
-
-let filter_compatible_candidates conv_algo env evd evi args rhs c =
- let c' = instantiate_evar (evar_filtered_context evi) c args in
- let evd, b = conv_algo env evd Reduction.CONV rhs c' in
- if b then Some (c,evd) else None
-
-exception DoesNotPreserveCandidateRestriction
-
-let restrict_candidates conv_algo env evd filter1 (evk1,argsv1) (evk2,argsv2) =
- let evi1 = Evd.find evd evk1 in
- let evi2 = Evd.find evd evk2 in
- let cand1 = filter_candidates evd evk1 filter1 None in
- let cand2 = evi2.evar_candidates in
- match cand1, cand2 with
- | _, None -> cand1
- | None, Some _ -> raise DoesNotPreserveCandidateRestriction
- | Some l1, Some l2 ->
- let args1 = Array.to_list argsv1 in
- let args2 = Array.to_list argsv2 in
- let l1' = List.filter (fun c1 ->
- let c1' = instantiate_evar (evar_filtered_context evi1) c1 args1 in
- let filter c2 =
- let compatibility = filter_compatible_candidates conv_algo env evd evi2 args2 c1' c2 in
- match compatibility with
- | None -> false
- | Some _ -> true
- in
- let filtered = List.filter filter l2 in
- match filtered with [] -> false | _ -> true) l1 in
- if Int.equal (List.length l1) (List.length l1') then None else Some l1'
-
-exception CannotProject of bool list option
-
-(* Assume that FV(?n[x1:=t1..xn:=tn]) belongs to some set U.
- Can ?n be instantiated by a term u depending essentially on xi such that the
- FV(u[x1:=t1..xn:=tn]) are in the set U?
- - If ti is a variable, it has to be in U.
- - If ti is a constructor, its parameters cannot be erased even if u
- matches on it, so we have to discard ti if the parameters
- contain variables not in U.
- - If ti is rigid, we have to discard it if it contains variables in U.
-
- Note: when restricting as part of an equation ?n[x1:=t1..xn:=tn] = ?m[...]
- then, occurrences of ?m in the ti can be seen, like variables, as occurrences
- of subterms to eventually discard so as to be allowed to keep ti.
-*)
-
-let rec is_constrainable_in k (ev,(fv_rels,fv_ids) as g) t =
- let f,args = decompose_app_vect t in
- match kind_of_term f with
- | Construct (ind,_) ->
- let params,_ = Array.chop (Inductiveops.inductive_nparams ind) args in
- Array.for_all (is_constrainable_in k g) params
- | Ind _ -> Array.for_all (is_constrainable_in k g) args
- | Prod (_,t1,t2) -> is_constrainable_in k g t1 && is_constrainable_in k g t2
- | Evar (ev',_) -> not (Int.equal ev' ev) (*If ev' needed, one may also try to restrict it*)
- | Var id -> Id.Set.mem id fv_ids
- | Rel n -> n <= k || Int.Set.mem n fv_rels
- | Sort _ -> true
- | _ -> (* We don't try to be more clever *) true
-
-let has_constrainable_free_vars evd aliases k ev (fv_rels,fv_ids as fvs) t =
- let t = expansion_of_var aliases t in
- match kind_of_term t with
- | Var id -> Id.Set.mem id fv_ids
- | Rel n -> n <= k || Int.Set.mem n fv_rels
- | _ -> is_constrainable_in k (ev,fvs) t
-
-let ensure_evar_independent g env evd (evk1,argsv1 as ev1) (evk2,argsv2 as ev2)=
- let filter1 =
- restrict_upon_filter evd evk1 (noccur_evar env evd evk2)
- (Array.to_list argsv1)
- in
- let candidates1 = restrict_candidates g env evd filter1 ev1 ev2 in
- let evd,(evk1,_ as ev1) = do_restrict_hyps evd ev1 filter1 candidates1 in
- let filter2 =
- restrict_upon_filter evd evk2 (noccur_evar env evd evk1)
- (Array.to_list argsv2)
- in
- let candidates2 = restrict_candidates g env evd filter2 ev2 ev1 in
- let evd,ev2 = do_restrict_hyps evd ev2 filter2 candidates2 in
- evd,ev1,ev2
-
-exception EvarSolvedOnTheFly of evar_map * constr
-
-let project_evar_on_evar g env evd aliases k2 (evk1,argsv1 as ev1) (evk2,argsv2 as ev2) =
- (* Apply filtering on ev1 so that fvs(ev1) are in fvs(ev2). *)
- let fvs2 = free_vars_and_rels_up_alias_expansion aliases (mkEvar ev2) in
- let filter1 = restrict_upon_filter evd evk1
- (has_constrainable_free_vars evd aliases k2 evk2 fvs2)
- (Array.to_list argsv1) in
- (* Only try pruning on variable substitutions, postpone otherwise. *)
- (* Rules out non-linear instances. *)
- if is_unification_pattern_pure_evar env evd ev2 (mkEvar ev1) then
- try
- let candidates1 = restrict_candidates g env evd filter1 ev1 ev2 in
- let evd,(evk1',args1) = do_restrict_hyps evd ev1 filter1 candidates1 in
- evd,mkEvar (evk1',invert_invertible_arg env evd aliases k2 ev2 args1)
- with
- | EvarSolvedWhileRestricting (evd,ev1) ->
- raise (EvarSolvedOnTheFly (evd,ev1))
- | DoesNotPreserveCandidateRestriction | NotEnoughInformationToInvert ->
- raise (CannotProject filter1)
- else
- raise (CannotProject filter1)
-
-let solve_evar_evar_l2r f g env evd aliases ev1 (evk2,_ as ev2) =
- try
- let evd,body = project_evar_on_evar g env evd aliases 0 ev1 ev2 in
- Evd.define evk2 body evd
- with EvarSolvedOnTheFly (evd,c) ->
- f env evd ev2 c
-
-let solve_evar_evar ?(force=false) f g env evd (evk1,args1 as ev1) (evk2,args2 as ev2) =
- if are_canonical_instances args1 args2 env then
- (* If instances are canonical, we solve the problem in linear time *)
- let sign = evar_filtered_context (Evd.find evd evk2) in
- let id_inst = Array.map (fun (id,_,_) -> mkVar id) (Array.of_list sign) in
- Evd.define evk2 (mkEvar(evk1,id_inst)) evd
- else
- let evd,ev1,ev2 =
- (* If an evar occurs in the instance of the other evar and the
- use of an heuristic is forced, we restrict *)
- if force then ensure_evar_independent g env evd ev1 ev2 else (evd,ev1,ev2) in
- let aliases = make_alias_map env in
- try solve_evar_evar_l2r f g env evd aliases ev1 ev2
- with CannotProject filter1 ->
- try solve_evar_evar_l2r f g env evd aliases ev2 ev1
- with CannotProject filter2 ->
- postpone_evar_evar f env evd filter1 ev1 filter2 ev2
-
-type conv_fun =
- env -> evar_map -> conv_pb -> constr -> constr -> evar_map * bool
-
-let check_evar_instance evd evk1 body conv_algo =
- let evi = Evd.find evd evk1 in
- let evenv = evar_env evi in
- (* FIXME: The body might be ill-typed when this is called from w_merge *)
- let ty =
- try Retyping.get_type_of evenv evd body
- with _ -> error "Ill-typed evar instance"
- in
- let evd,b = conv_algo evenv evd Reduction.CUMUL ty evi.evar_concl in
- if b then evd else
- user_err_loc (fst (evar_source evk1 evd),"",
- str "Unable to find a well-typed instantiation")
-
-(* Solve pbs ?e[t1..tn] = ?e[u1..un] which arise often in fixpoint
- * definitions. We try to unify the ti with the ui pairwise. The pairs
- * that don't unify are discarded (i.e. ?e is redefined so that it does not
- * depend on these args). *)
-
-let solve_refl ?(can_drop=false) conv_algo env evd evk argsv1 argsv2 =
- if Array.equal eq_constr argsv1 argsv2 then evd else
- (* Filter and restrict if needed *)
- let untypedfilter =
- restrict_upon_filter evd evk
- (fun (a1,a2) -> snd (conv_algo env evd Reduction.CONV a1 a2))
- (List.combine (Array.to_list argsv1) (Array.to_list argsv2)) in
- let candidates = filter_candidates evd evk untypedfilter None in
- let filter = match untypedfilter with
- | None -> None
- | Some filter -> closure_of_filter evd evk filter in
- let evd,ev1 = restrict_applied_evar evd (evk,argsv1) filter candidates in
- if Int.equal (fst ev1) evk && can_drop then (* No refinement *) evd else
- (* either progress, or not allowed to drop, e.g. to preserve possibly *)
- (* informative equations such as ?e[x:=?y]=?e[x:=?y'] where we don't know *)
- (* if e can depend on x until ?y is not resolved, or, conversely, we *)
- (* don't know if ?y has to be unified with ?y, until e is resolved *)
- let argsv2 = restrict_instance evd evk filter argsv2 in
- let ev2 = (fst ev1,argsv2) in
- (* Leave a unification problem *)
- Evd.add_conv_pb (Reduction.CONV,env,mkEvar ev1,mkEvar ev2) evd
-
-(* If the evar can be instantiated by a finite set of candidates known
- in advance, we check which of them apply *)
-
-exception NoCandidates
-
-let solve_candidates conv_algo env evd (evk,argsv as ev) rhs =
- let evi = Evd.find evd evk in
- let args = Array.to_list argsv in
- match evi.evar_candidates with
- | None -> raise NoCandidates
- | Some l ->
- let l' =
- List.map_filter
- (filter_compatible_candidates conv_algo env evd evi args rhs) l in
- match l' with
- | [] -> error_cannot_unify env evd (mkEvar ev, rhs)
- | [c,evd] ->
- (* solve_candidates might have been called recursively in the mean *)
- (* time and the evar been solved by the filtering process *)
- if Evd.is_undefined evd evk then Evd.define evk c evd else evd
- | l when List.length l < List.length l' ->
- let candidates = List.map fst l in
- restrict_evar evd evk None (Some candidates)
- | l -> evd
-
-(* We try to instantiate the evar assuming the body won't depend
- * on arguments that are not Rels or Vars, or appearing several times
- * (i.e. we tackle a generalization of Miller-Pfenning patterns unification)
- *
- * 1) Let "env |- ?ev[hyps:=args] = rhs" be the unification problem
- * 2) We limit it to a patterns unification problem "env |- ev[subst] = rhs"
- * where only Rel's and Var's are relevant in subst
- * 3) We recur on rhs, "imitating" the term, and failing if some Rel/Var is
- * not in the scope of ?ev. For instance, the problem
- * "y:nat |- ?x[] = y" where "|- ?1:nat" is not satisfiable because
- * ?1 would be instantiated by y which is not in the scope of ?1.
- * 4) We try to "project" the term if the process of imitation fails
- * and that only one projection is possible
- *
- * Note: we don't assume rhs in normal form, it may fail while it would
- * have succeeded after some reductions.
- *
- * This is the work of [invert_definition Γ Σ ?ev[hyps:=args] c]
- * Precondition: Σ; Γ, y1..yk |- c /\ Σ; Γ |- u1..un
- * Postcondition: if φ(x1..xn) is returned then
- * Σ; Γ, y1..yk |- φ(u1..un) = c /\ x1..xn |- φ(x1..xn)
- *)
-
-exception NotInvertibleUsingOurAlgorithm of constr
-exception NotEnoughInformationToProgress of (Id.t * evar_projection) list
-exception OccurCheckIn of evar_map * constr
-
-let rec invert_definition conv_algo choose env evd (evk,argsv as ev) rhs =
- let aliases = make_alias_map env in
- let evdref = ref evd in
- let progress = ref false in
- let evi = Evd.find evd evk in
- let subst,cstr_subst = make_projectable_subst aliases evd evi argsv in
-
- (* Projection *)
- let project_variable t =
- (* Evar/Var problem: unifiable iff variable projectable from ev subst *)
- try
- let sols = find_projectable_vars true aliases !evdref t subst in
- let c, p = match sols with
- | [] -> raise Not_found
- | [id,p] -> (mkVar id, p)
- | (id,p)::_::_ ->
- if choose then (mkVar id, p) else raise (NotUniqueInType sols)
- in
- let ty = lazy (Retyping.get_type_of env !evdref t) in
- let evd = do_projection_effects (evar_define conv_algo) env ty !evdref p in
- evdref := evd;
- c
- with
- | Not_found -> raise (NotInvertibleUsingOurAlgorithm t)
- | NotUniqueInType sols ->
- if not !progress then
- raise (NotEnoughInformationToProgress sols);
- (* No unique projection but still restrict to where it is possible *)
- (* materializing is necessary, but is restricting useful? *)
- let ty = find_solution_type (evar_filtered_env evi) sols in
- let sign = evar_filtered_context evi in
- let ty' = instantiate_evar sign ty (Array.to_list argsv) in
- let (evd,evar,(evk',argsv' as ev')) =
- materialize_evar (evar_define conv_algo) env !evdref 0 ev ty' in
- let ts = expansions_of_var aliases t in
- let test c = isEvar c or List.mem c ts in
- let filter = Array.map_to_list test argsv' in
- let filter = apply_subfilter (evar_filter (Evd.find_undefined evd evk)) filter in
-
- let filter = closure_of_filter evd evk' filter in
- let candidates = extract_candidates sols in
- let evd = match candidates with
- | None ->
- let evd, ev'' = restrict_applied_evar evd ev' filter None in
- Evd.add_conv_pb (Reduction.CONV,env,mkEvar ev'',t) evd
- | Some _ ->
- restrict_evar evd evk' filter candidates
- in
- evdref := evd;
- evar in
-
- let rec imitate (env',k as envk) t =
- let t = whd_evar !evdref t in
- match kind_of_term t with
- | Rel i when i>k ->
- (match pi2 (Environ.lookup_rel (i-k) env') with
- | None -> project_variable (mkRel (i-k))
- | Some b ->
- try project_variable (mkRel (i-k))
- with NotInvertibleUsingOurAlgorithm _ -> imitate envk (lift i b))
- | Var id ->
- (match pi2 (Environ.lookup_named id env') with
- | None -> project_variable t
- | Some b ->
- try project_variable t
- with NotInvertibleUsingOurAlgorithm _ -> imitate envk b)
- | Evar (evk',args' as ev') ->
- if Int.equal evk evk' then raise (OccurCheckIn (evd,rhs));
- (* Evar/Evar problem (but left evar is virtual) *)
- let aliases = lift_aliases k aliases in
- (try
- let ev = (evk,Array.map (lift k) argsv) in
- let evd,body = project_evar_on_evar conv_algo env' !evdref aliases k ev' ev in
- evdref := evd;
- body
- with
- | EvarSolvedOnTheFly (evd,t) -> evdref:=evd; imitate envk t
- | CannotProject filter' ->
- assert !progress;
- (* Make the virtual left evar real *)
- let ty = get_type_of env' !evdref t in
- let (evd,evar'',ev'') =
- materialize_evar (evar_define conv_algo) env' !evdref k ev ty in
- (* materialize_evar may instantiate ev' by another evar; adjust it *)
- let (evk',args' as ev') = normalize_evar evd ev' in
- let evd =
- (* Try to project (a restriction of) the left evar ... *)
- try
- let evd,body = project_evar_on_evar conv_algo env' evd aliases 0 ev'' ev' in
- Evd.define evk' body evd
- with
- | EvarSolvedOnTheFly _ -> assert false (* ev has no candidates *)
- | CannotProject filter'' ->
- (* ... or postpone the problem *)
- postpone_evar_evar (evar_define conv_algo) env' evd filter'' ev'' filter' ev' in
- evdref := evd;
- evar'')
- | _ ->
- progress := true;
- match
- let c,args = decompose_app_vect t in
- match kind_of_term c with
- | Construct cstr when noccur_between 1 k t ->
- (* This is common case when inferring the return clause of match *)
- (* (currently rudimentary: we do not treat the case of multiple *)
- (* possible inversions; we do not treat overlap with a possible *)
- (* alternative inversion of the subterms of the constructor, etc)*)
- (match find_projectable_constructor env evd cstr k args cstr_subst with
- | _::_ as l -> Some (List.map mkVar l)
- | _ -> None)
- | _ -> None
- with
- | Some l ->
- let ty = get_type_of env' !evdref t in
- let candidates =
- try
- let t =
- map_constr_with_full_binders (fun d (env,k) -> push_rel d env, k+1)
- imitate envk t in
- t::l
- with _ -> l in
- (match candidates with
- | [x] -> x
- | _ ->
- let (evd,evar'',ev'') =
- materialize_evar (evar_define conv_algo) env' !evdref k ev ty in
- evdref := restrict_evar evd (fst ev'') None (Some candidates);
- 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 in
-
- let rhs = whd_beta evd rhs (* heuristic *) in
- let body = imitate (env,0) rhs in
- (!evdref,body)
-
-(* [define] tries to solve the problem "?ev[args] = rhs" when "?ev" is
- * an (uninstantiated) evar such that "hyps |- ?ev : typ". Otherwise said,
- * [define] tries to find an instance lhs such that
- * "lhs [hyps:=args]" unifies to rhs. The term "lhs" must be closed in
- * context "hyps" and not referring to itself.
- *)
-
-and evar_define conv_algo ?(choose=false) env evd (evk,argsv as ev) rhs =
- match kind_of_term rhs with
- | Evar (evk2,argsv2 as ev2) ->
- if Int.equal evk evk2 then
- solve_refl ~can_drop:choose conv_algo env evd evk argsv argsv2
- else
- solve_evar_evar ~force:choose
- (evar_define conv_algo) conv_algo env evd ev ev2
- | _ ->
- try solve_candidates conv_algo env evd ev rhs
- with NoCandidates ->
- try
- let (evd',body) = invert_definition conv_algo choose env evd ev rhs in
- if occur_meta body then error "Meta cannot occur in evar body.";
- (* invert_definition may have instantiate some evars of rhs with evk *)
- (* so we recheck acyclicity *)
- if occur_evar evk body then raise (OccurCheckIn (evd',body));
- (* needed only if an inferred type *)
- let body = refresh_universes body in
-(* Cannot strictly type instantiations since the unification algorithm
- * does not unify applications from left to right.
- * e.g problem f x == g y yields x==y and f==g (in that order)
- * Another problem is that type variables are evars of type Type
- let _ =
- try
- let env = evar_filtered_env evi in
- let ty = evi.evar_concl in
- Typing.check env evd' body ty
- with e ->
- msg_info
- (str "Ill-typed evar instantiation: " ++ fnl() ++
- pr_evar_map evd' ++ fnl() ++
- str "----> " ++ int ev ++ str " := " ++
- print_constr body);
- raise e in*)
- let evd' = Evd.define evk body evd' in
- check_evar_instance evd' evk body conv_algo
- with
- | NotEnoughInformationToProgress sols ->
- postpone_non_unique_projection env evd ev sols rhs
- | NotInvertibleUsingOurAlgorithm t ->
- error_not_clean env evd evk t (evar_source evk evd)
- | OccurCheckIn (evd,rhs) ->
- (* last chance: rhs actually reduces to ev *)
- let c = whd_betadeltaiota env evd rhs in
- match kind_of_term c with
- | Evar (evk',argsv2) when Int.equal evk evk' ->
- solve_refl
- (fun env sigma pb c c' -> (evd,is_fconv pb env sigma c c'))
- env evd evk argsv argsv2
- | _ ->
- error_occur_check env evd evk rhs
-
-(* This code (i.e. solve_pb, etc.) takes a unification
- * problem, and tries to solve it. If it solves it, then it removes
- * all the conversion problems, and re-runs conversion on each one, in
- * the hopes that the new solution will aid in solving them.
- *
- * The kinds of problems it knows how to solve are those in which
- * the usable arguments of an existential var are all themselves
- * universal variables.
- * The solution to this problem is to do renaming for the Var's,
- * to make them match up with the Var's which are found in the
- * hyps of the existential, to do a "pop" for each Rel which is
- * not an argument of the existential, and a subst1 for each which
- * is, again, with the corresponding variable. This is done by
- * define
- *
- * Thus, we take the arguments of the existential which we are about
- * to assign, and zip them with the identifiers in the hypotheses.
- * Then, we process all the Var's in the arguments, and sort the
- * Rel's into ascending order. Then, we just march up, doing
- * subst1's and pop's.
- *
- * NOTE: We can do this more efficiently for the relative arguments,
- * by building a long substituend by hand, but this is a pain in the
- * ass.
- *)
-
-let status_changed lev (pbty,_,t1,t2) =
- (try ExistentialSet.mem (head_evar t1) lev with NoHeadEvar -> false) or
- (try ExistentialSet.mem (head_evar t2) lev with NoHeadEvar -> false)
-
-let reconsider_conv_pbs conv_algo evd =
- let (evd,pbs) = extract_changed_conv_pbs evd status_changed in
- List.fold_left
- (fun (evd,b as p) (pbty,env,t1,t2) ->
- if b then conv_algo env evd pbty t1 t2 else p) (evd,true)
- pbs
-
-(* Tries to solve problem t1 = t2.
- * Precondition: t1 is an uninstantiated evar
- * Returns an optional list of evars that were instantiated, or None
- * if the problem couldn't be solved. *)
-
-(* Rq: uncomplete algorithm if pbty = CONV_X_LEQ ! *)
-let solve_simple_eqn conv_algo ?(choose=false) env evd (pbty,(evk1,args1 as ev1),t2) =
- try
- let t2 = whd_betaiota evd t2 in (* includes whd_evar *)
- let evd =
- match pbty with
- | Some true when isEvar t2 ->
- add_conv_pb (Reduction.CUMUL,env,mkEvar ev1,t2) evd
- | Some false when isEvar t2 ->
- add_conv_pb (Reduction.CUMUL,env,t2,mkEvar ev1) evd
- | _ ->
- evar_define conv_algo ~choose env evd ev1 t2 in
- reconsider_conv_pbs conv_algo evd
- with e when precatchable_exception e ->
- (evd,false)
(** The following functions return the set of evars immediately
contained in the object, including defined evars *)
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index 5c32a9a5c..7f605ce3a 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -32,6 +32,10 @@ val new_evar :
evar_map -> env -> ?src:Loc.t * Evar_kinds.t -> ?filter:bool list ->
?candidates:constr list -> types -> evar_map * constr
+val new_pure_evar :
+ evar_map -> named_context_val -> ?src:Loc.t * Evar_kinds.t -> ?filter:bool list ->
+ ?candidates:constr list -> types -> evar_map * evar
+
(** the same with side-effects *)
val e_new_evar :
evar_map ref -> env -> ?src:Loc.t * Evar_kinds.t -> ?filter:bool list ->
@@ -53,18 +57,6 @@ val new_evar_instance :
val make_pure_subst : evar_info -> constr array -> (Id.t * constr) list
-(** {6 Instantiate evars} *)
-
-type conv_fun =
- env -> evar_map -> conv_pb -> constr -> constr -> evar_map * bool
-
-(** [evar_define choose env ev c] try to instantiate [ev] with [c] (typed in [env]),
- possibly solving related unification problems, possibly leaving open
- some problems that cannot be solved in a unique way (except if choose is
- true); fails if the instance is not valid for the given [ev] *)
-val evar_define : conv_fun -> ?choose:bool -> env -> evar_map ->
- existential -> constr -> evar_map
-
(** {6 Evars/Metas switching...} *)
(** [evars_to_metas] generates new metavariables for each non dependent
@@ -85,16 +77,6 @@ val whd_head_evar : evar_map -> constr -> constr
val is_ground_term : evar_map -> constr -> bool
val is_ground_env : evar_map -> env -> bool
-val solve_refl : ?can_drop:bool -> conv_fun -> env -> evar_map ->
- existential_key -> constr array -> constr array -> evar_map
-val solve_evar_evar : ?force:bool ->
- (env -> evar_map -> existential -> constr -> evar_map) -> conv_fun ->
- env -> evar_map -> existential -> existential -> evar_map
-
-val solve_simple_eqn : conv_fun -> ?choose:bool -> env -> evar_map ->
- bool option * existential * constr -> evar_map * bool
-val reconsider_conv_pbs : conv_fun -> evar_map -> evar_map * 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
@@ -103,17 +85,9 @@ 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 : evar_map -> existential -> evar_map * sorts
-val is_unification_pattern_evar : env -> evar_map -> existential -> constr list ->
- constr -> constr list option
-
-val is_unification_pattern : env * int -> evar_map -> constr -> constr list ->
- constr -> constr list option
-
val evar_absorb_arguments : env -> evar_map -> existential -> constr list ->
evar_map * existential
-val solve_pattern_eqn : env -> constr list -> constr -> constr
-
(** The following functions return the set of evars immediately
contained in the object, including defined evars *)
@@ -196,10 +170,6 @@ val jv_nf_betaiotaevar :
exception Uninstantiated_evar of existential_key
val flush_and_check_evars : evar_map -> constr -> constr
-(** 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
-
(** {6 debug pretty-printer:} *)
val pr_tycon : env -> type_constraint -> Pp.std_ppcmds
@@ -226,6 +196,4 @@ val push_rel_context_to_named_context : Environ.env -> types ->
val generalize_evar_over_rels : evar_map -> existential -> types * constr list
-val check_evar_instance : evar_map -> existential_key -> constr -> conv_fun ->
- evar_map
diff --git a/pretyping/pretyping.mllib b/pretyping/pretyping.mllib
index 506c59ef3..d4892f2f8 100644
--- a/pretyping/pretyping.mllib
+++ b/pretyping/pretyping.mllib
@@ -10,6 +10,7 @@ Retyping
Cbv
Pretype_errors
Evarutil
+Evarsolve
Term_dnet
Recordops
Evarconv
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index d5fee4595..d6f1fac88 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -17,6 +17,7 @@ open Evd
open Reduction
open Reductionops
open Evarutil
+open Evarsolve
open Pretype_errors
open Retyping
open Coercion
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-02 11:17:27 +0000