From ce0176d8c25aa353c06b1f8f56ead63f28fb6efc Mon Sep 17 00:00:00 2001 From: ppedrot Date: Sun, 10 Feb 2013 00:37:57 +0000 Subject: Splitted Evarutil in two files git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16195 85f007b7-540e-0410-9357-904b9bb8a0f7 --- pretyping/evarsolve.ml | 1363 ++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 1363 insertions(+) create mode 100644 pretyping/evarsolve.ml (limited to 'pretyping/evarsolve.ml') 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 *) +(* (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) + -- cgit v1.2.3