diff options
Diffstat (limited to 'pretyping/evarutil.ml')
| -rw-r--r-- | pretyping/evarutil.ml | 1923 |
1 files changed, 1269 insertions, 654 deletions
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index b95b50b3..fc29ba6c 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <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 *) (************************************************************************) -(* $Id: evarutil.ml 14641 2011-11-06 11:59:10Z herbelin $ *) - open Util open Pp open Names @@ -23,11 +21,11 @@ open Reductionops open Pretype_errors open Retyping -open Pretype_errors -open Retyping +(****************************************************) +(* Expanding/testing/exposing existential variables *) +(****************************************************) -(* Expanding existential variables *) -(* 1- flush_and_check_evars fails if an existential is undefined *) +(* flush_and_check_evars fails if an existential is undefined *) exception Uninstantiated_evar of existential_key @@ -63,11 +61,99 @@ let nf_evar_info evc info = evar_body = match info.evar_body with | Evar_empty -> Evar_empty | Evar_defined c -> Evar_defined (Reductionops.nf_evar evc c) } +let nf_evars evm = + Evd.fold + (fun ev evi evm' -> Evd.add evm' ev (nf_evar_info evm evi)) + evm Evd.empty -let nf_evars evm = Evd.fold (fun ev evi evm' -> Evd.add evm' ev (nf_evar_info evm evi)) - evm Evd.empty +let nf_evars_undefined evm = + Evd.fold_undefined + (fun ev evi evm' -> Evd.add evm' ev (nf_evar_info evm evi)) + evm (defined_evars evm) let nf_evar_map evd = Evd.evars_reset_evd (nf_evars evd) evd +let nf_evar_map_undefined evd = Evd.evars_reset_evd (nf_evars_undefined evd) evd + +(*-------------------*) +(* Auxiliary functions for the conversion algorithms modulo evars + *) + +let has_undefined_evars_or_sorts evd t = + let rec has_ev t = + match kind_of_term t with + | Evar (ev,args) -> + (match evar_body (Evd.find evd ev) with + | Evar_defined c -> + has_ev c; Array.iter has_ev args + | Evar_empty -> + raise NotInstantiatedEvar) + | Sort s when is_sort_variable evd s -> raise Not_found + | _ -> iter_constr has_ev t in + try let _ = has_ev t in false + with (Not_found | NotInstantiatedEvar) -> true + +let is_ground_term evd t = + not (has_undefined_evars_or_sorts evd t) + +let is_ground_env evd env = + let is_ground_decl = function + (_,Some b,_) -> is_ground_term evd b + | _ -> true in + List.for_all is_ground_decl (rel_context env) && + List.for_all is_ground_decl (named_context env) +(* Memoization is safe since evar_map and environ are applicative + structures *) +let is_ground_env = memo1_2 is_ground_env + +(* Return the head evar if any *) + +exception NoHeadEvar + +let head_evar = + let rec hrec c = match kind_of_term c with + | Evar (evk,_) -> evk + | Case (_,_,c,_) -> hrec c + | App (c,_) -> hrec c + | Cast (c,_,_) -> hrec c + | _ -> raise NoHeadEvar + in + hrec + +(* Expand head evar if any (currently consider only applications but I + guess it should consider Case too) *) + +let whd_head_evar_stack sigma c = + let rec whrec (c, l as s) = + match kind_of_term c with + | Evar (evk,args as ev) when Evd.is_defined sigma evk + -> whrec (existential_value sigma ev, l) + | Cast (c,_,_) -> whrec (c, l) + | App (f,args) -> whrec (f, Array.fold_right (fun a l -> a::l) args l) + | _ -> s + in + whrec (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 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 *) @@ -76,6 +162,10 @@ let nf_evar_map evd = Evd.evars_reset_evd (nf_evars evd) evd (* Generator of metavariables *) let new_meta = let meta_ctr = ref 0 in + Summary.declare_summary "meta counter" + { Summary.freeze_function = (fun () -> !meta_ctr); + Summary.unfreeze_function = (fun n -> meta_ctr := n); + Summary.init_function = (fun () -> meta_ctr := 0) }; fun () -> incr meta_ctr; !meta_ctr let mk_new_meta () = mkMeta(new_meta()) @@ -84,14 +174,14 @@ let collect_evars emap c = let rec collrec acc c = match kind_of_term c with | Evar (evk,_) -> - if Evd.mem emap evk & not (Evd.is_defined emap evk) then evk::acc + if Evd.is_undefined emap evk then evk::acc else (* No recursion on the evar instantiation *) acc | _ -> fold_constr collrec acc c in list_uniquize (collrec [] c) let push_dependent_evars sigma emap = - Evd.fold (fun ev {evar_concl = ccl} (sigma',emap') -> + Evd.fold_undefined (fun ev {evar_concl = ccl} (sigma',emap') -> List.fold_left (fun (sigma',emap') ev -> (Evd.add sigma' ev (Evd.find emap' ev),Evd.remove emap' ev)) @@ -116,9 +206,22 @@ let push_duplicated_evars sigma emap c = (* replaces a mapping of existentials into a mapping of metas. Problem if an evar appears in the type of another one (pops anomaly) *) let evars_to_metas sigma (emap, c) = - let emap = nf_evars emap in + let emap = nf_evar_map_undefined emap in let sigma',emap' = push_dependent_evars sigma emap in let sigma',emap' = push_duplicated_evars sigma' emap' c in + (* if an evar has been instantiated in [emap] (as part of typing [c]) + then it is instantiated in [sigma]. *) + let repair_evars sigma emap = + fold_undefined begin fun ev _ sigma' -> + try + let info = find emap ev in + match evar_body info with + | Evar_empty -> sigma' + | Evar_defined body -> define ev body sigma' + with Not_found -> sigma' + end sigma sigma + in + let sigma' = repair_evars sigma' emap in let change_exist evar = let ty = nf_betaiota emap (existential_type emap evar) in let n = new_meta() in @@ -129,15 +232,23 @@ let evars_to_metas sigma (emap, c) = | _ -> map_constr replace c in (sigma', replace c) -(* The list of non-instantiated existential declarations *) +(* The list of non-instantiated existential declarations (order is important) *) let non_instantiated sigma = - let listev = to_list sigma in - List.fold_left - (fun l (ev,evi) -> - if evi.evar_body = Evar_empty then - ((ev,nf_evar_info sigma evi)::l) else l) - [] listev + let listev = Evd.undefined_list sigma in + List.map (fun (ev,evi) -> (ev,nf_evar_info sigma evi)) listev + +(************************) +(* 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)) (**********************) (* Creating new evars *) @@ -146,138 +257,16 @@ let non_instantiated sigma = (* Generator of existential names *) let new_untyped_evar = let evar_ctr = ref 0 in + Summary.declare_summary "evar counter" + { Summary.freeze_function = (fun () -> !evar_ctr); + Summary.unfreeze_function = (fun n -> evar_ctr := n); + Summary.init_function = (fun () -> evar_ctr := 0) }; fun () -> incr evar_ctr; existential_of_int !evar_ctr (*------------------------------------* * functional operations on evar sets * *------------------------------------*) -let new_evar_instance sign evd typ ?(src=(dummy_loc,InternalHole)) ?filter instance = - let instance = - match filter with - | None -> instance - | Some filter -> snd (list_filter2 (fun b c -> b) (filter,instance)) in - assert - (let ctxt = named_context_of_val sign in - list_distinct (ids_of_named_context ctxt)); - let newevk = new_untyped_evar() in - let evd = evar_declare sign newevk typ ~src:src ?filter evd in - (evd,mkEvar (newevk,Array.of_list instance)) - -(* 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_aliases sign = - List.fold_right (fun (id,b,c) aliases -> - match b with - | Some t -> - (match kind_of_term t with - | Var id' -> - let id'' = try Idmap.find id' aliases with Not_found -> id' in - Idmap.add id id'' aliases - | _ -> aliases) - | None -> aliases) sign Idmap.empty - -let alias_of_var id aliases = try Idmap.find id aliases with Not_found -> id - -let make_alias_map env = - let var_aliases = compute_aliases (named_context env) in - let rels = rel_context env in - let rel_aliases = - snd (List.fold_right (fun (_,b,t) (n,aliases) -> - (n-1, - match b with - | Some t when isRel t or isVar t -> Intmap.add n (lift n t) aliases - | _ -> aliases)) rels (List.length rels,Intmap.empty)) in - (var_aliases,rel_aliases) - -let expand_var_once aliases x = match kind_of_term x with - | Rel n -> Intmap.find n (snd aliases) - | Var id -> mkVar (Idmap.find id (fst aliases)) - | _ -> raise Not_found - -let rec expand_var_at_least_once aliases x = - let t = expand_var_once aliases x in - try expand_var_at_least_once aliases t - with Not_found -> t - -let expand_var aliases x = - try expand_var_at_least_once aliases x with Not_found -> x - -let expand_var_opt aliases x = - try Some (expand_var_at_least_once aliases x) with Not_found -> None - -let extend_alias (_,b,_) (var_aliases,rel_aliases) = - let rel_aliases = - Intmap.fold (fun n c -> Intmap.add (n+1) (lift 1 c)) - rel_aliases Intmap.empty in - let rel_aliases = - match b with - | Some t when isRel t or isVar t -> Intmap.add 1 (lift 1 t) rel_aliases - | _ -> rel_aliases in - (var_aliases, rel_aliases) - -let rec expand_vars_in_term_using aliases t = match kind_of_term t with - | Rel _ | Var _ -> - expand_var 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 rec expansions_of_var aliases x = - try - let t = expand_var_once aliases x in - t :: expansions_of_var aliases t - with Not_found -> - [x] - -let expand_full_opt aliases y = - try Some (expand_var aliases y) with Not_found -> None - -(* 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_aliases sign in - snd (List.fold_right - (fun (id,b,c) (args,l) -> - match b,args with - | None, a::rest -> - let a = whd_evar sigma a in - (rest,Idmap.add id [a,expand_full_opt aliases a,id] l) - | Some c, a::rest -> - let a = whd_evar sigma a in - (match kind_of_term c with - | Var id' -> - let idc = alias_of_var id' evar_aliases in - let sub = try Idmap.find idc l with Not_found -> [] in - if List.exists (fun (c,_,_) -> eq_constr a c) sub then (rest,l) - else - (rest,Idmap.add idc ((a,expand_full_opt aliases a,id)::sub) l) - | _ -> - (rest,Idmap.add id [a,expand_full_opt aliases a,id] l)) - | _ -> anomaly "Instance does not match its signature") - sign (array_rev_to_list args,Idmap.empty)) - -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 "Instance does not match its signature") - (evar_filtered_context evi) (array_rev_to_list args,[])) - (* [push_rel_context_to_named_context] builds the defining context and the * initial instance of an evar. If the evar is to be used in context * @@ -322,137 +311,258 @@ let push_rel_context_to_named_context env typ = let d = (id,Option.map (substl subst) c,substl subst t) in (mkVar id :: subst, id::avoid, push_named d env)) (rel_context env) ~init:([], ids, env) in - (named_context_val env, substl subst typ, inst_rels@inst_vars) + (named_context_val env, substl subst typ, inst_rels@inst_vars, subst) + +(*------------------------------------* + * Entry points to define new evars * + *------------------------------------*) + +let default_source = (dummy_loc,InternalHole) + +let new_pure_evar evd sign ?(src=default_source) ?filter ?candidates typ = + let newevk = new_untyped_evar() in + let evd = evar_declare sign newevk typ ~src ?filter ?candidates evd in + (evd,newevk) + +let new_evar_instance sign evd typ ?src ?filter ?candidates instance = + assert (not !Flags.debug || + list_distinct (ids_of_named_context (named_context_of_val sign))); + let evd,newevk = new_pure_evar evd sign ?src ?filter ?candidates typ in + (evd,mkEvar (newevk,Array.of_list instance)) (* [new_evar] declares a new existential in an env env with type typ *) (* Converting the env into the sign of the evar to define *) -let new_evar evd env ?(src=(dummy_loc,InternalHole)) ?filter typ = - let sign,typ',instance = push_rel_context_to_named_context env typ in - new_evar_instance sign evd typ' ~src:src ?filter instance +let new_evar evd env ?src ?filter ?candidates typ = + let sign,typ',instance,subst = push_rel_context_to_named_context env typ in + let candidates = Option.map (List.map (substl subst)) candidates in + let instance = + match filter with + | None -> instance + | Some filter -> list_filter_with filter instance in + new_evar_instance sign evd typ' ?src ?filter ?candidates instance + +let new_type_evar ?src ?filter evd env = + let evd', s = new_sort_variable evd in + new_evar evd' env ?src ?filter (mkSort s) (* The same using side-effect *) -let e_new_evar evdref env ?(src=(dummy_loc,InternalHole)) ?filter ty = - let (evd',ev) = new_evar !evdref env ~src:src ?filter ty in +let e_new_evar evdref env ?(src=(dummy_loc,InternalHole)) ?filter ?candidates ty = + let (evd',ev) = new_evar !evdref env ~src:src ?filter ?candidates ty in evdref := evd'; ev (*------------------------------------* - * operations on the evar constraints * + * Restricting existing evars * *------------------------------------*) -(* Pb: defined Rels and Vars should not be considered as a pattern... *) -(* -let is_pattern inst = - let rec is_hopat l = function - [] -> true - | t :: tl -> - (isRel t or isVar t) && not (List.mem t l) && is_hopat (t::l) tl in - is_hopat [] (Array.to_list inst) -*) +let restrict_evar_key evd evk filter candidates = + if filter = None && candidates = None then + evd,evk + else + let evi = Evd.find_undefined evd evk in + let oldfilter = evar_filter evi in + if filter = Some oldfilter && candidates = None then + evd,evk + else + let filter = + match filter with + | None -> evar_filter evi + | Some filter -> filter in + let candidates = + match candidates with None -> evi.evar_candidates | _ -> 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 = snd (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 + +(* 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) = + let evi = Evd.find sigma ev in + let sign = named_context_of_val evi.evar_hyps in + List.fold_left2 + (fun (c,inst as x) a d -> + if isRel a then (mkNamedProd_or_LetIn d c,a::inst) else x) + (evi.evar_concl,[]) (Array.to_list args) sign + +(***************************************) +(* 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 *) -(* 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. - * What we do is to formally introduce ?e1' in context x1..xq, Γ, y1..yk, - * but forbidding it to use the variables of Γ (otherwise said, - * Γ is here only for ensuring the correct typing of ?e1'). - * - * In fact, we optimize a little and try to compute a maximum - * common subpart of x1..xq and Γ. This is done by detecting the - * longest subcontext x1..xp such that Γ = x1'..xp' z1..zm and - * u1..up = x1'..xp'. - * - * At the end, we return ?e1'[x1..xn z1..zm y1..yk] so that ?e1 can be - * instantiated by (...\y1 ... \yk ... ?e1[x1..xn z1..zm y1..yk]) and the - * new problem is Σ; Γ, y1..yk |- ?e1'[u1..un z1..zm y1..yk] = c, - * making the z1..zm unavailable. - * - * This is what [extend_evar Γ evd k (?e1[u1..uq]) c] does. - *) +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 Idmap.find id' aliases with Not_found -> [] in + Idmap.add id (aliases_of_id@[t]) aliases + | _ -> + Idmap.add id [t] aliases) + | None -> aliases) + sign Idmap.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 Idmap.find id' var_aliases with Not_found -> [] in + Intmap.add n (aliases_of_n@[t]) aliases + | Rel p -> + let aliases_of_n = + try Intmap.find (p+n) aliases with Not_found -> [] in + Intmap.add n (aliases_of_n@[mkRel (p+n)]) aliases + | _ -> + Intmap.add n [lift n t] aliases) + | None -> aliases)) + rels (List.length rels,Intmap.empty)) -let shrink_context env subst ty = - let rev_named_sign = List.rev (named_context env) in - let rel_sign = rel_context env in - (* We merge the contexts (optimization) *) - let rec shrink_rel i subst rel_subst rev_rel_sign = - match subst,rev_rel_sign with - | (id,c)::subst,_::rev_rel_sign when c = mkRel i -> - shrink_rel (i-1) subst (mkVar id::rel_subst) rev_rel_sign - | _ -> - substl_rel_context rel_subst (List.rev rev_rel_sign), - substl rel_subst ty - in - let rec shrink_named subst named_subst rev_named_sign = - match subst,rev_named_sign with - | (id,c)::subst,(id',b',t')::rev_named_sign when c = mkVar id' -> - shrink_named subst ((id',mkVar id)::named_subst) rev_named_sign - | _::_, [] -> - let nrel = List.length rel_sign in - let rel_sign, ty = shrink_rel nrel subst [] (List.rev rel_sign) in - [], map_rel_context (replace_vars named_subst) rel_sign, - replace_vars named_subst ty - | _ -> - map_named_context (replace_vars named_subst) (List.rev rev_named_sign), - rel_sign, ty - in - shrink_named subst [] rev_named_sign - -let extend_evar env evdref k (evk1,args1) c = - let ty = get_type_of env !evdref c in - let overwrite_first v1 v2 = - let v = Array.copy v1 in - let n = Array.length v - Array.length v2 in - for i = 0 to Array.length v2 - 1 do v.(n+i) <- v2.(i) done; - v in - let evi1 = Evd.find !evdref evk1 in - let named_sign',rel_sign',ty = - if k = 0 then [], [], ty - else shrink_context env (List.rev (make_pure_subst evi1 args1)) ty in - let extenv = - List.fold_right push_rel rel_sign' - (List.fold_right push_named named_sign' (evar_unfiltered_env evi1)) in - let nb_to_hide = rel_context_length rel_sign' - k in - let rel_filter = list_map_i (fun i _ -> i > nb_to_hide) 1 rel_sign' in - let named_filter1 = List.map (fun _ -> true) (evar_context evi1) in - let named_filter2 = List.map (fun _ -> false) named_sign' in - let filter = rel_filter@named_filter2@named_filter1 in - let evar1' = e_new_evar evdref extenv ~filter:filter ty in - let evk1',args1'_in_env = destEvar evar1' in - let args1'_in_extenv = Array.map (lift k) (overwrite_first args1'_in_env args1) in - (evar1',(evk1',args1'_in_extenv)) - -let subfilter p filter l = - let (filter,_,l) = - List.fold_left (fun (filter,l,newl) b -> - if b then - let a,l' = match l with a::args -> a,args | _ -> assert false in - if p a then (true::filter,l',a::newl) else (false::filter,l',newl) - else (false::filter,l,newl)) - ([],l,[]) filter in - (List.rev filter,List.rev l) - -let restrict_upon_filter evd evi evk p args = - let filter = evar_filter evi in - let newfilter,newargs = subfilter p filter args in - if newfilter <> filter then - let (evd,newev) = new_evar evd (evar_unfiltered_env evi) ~src:(evar_source evk evd) - ~filter:newfilter evi.evar_concl in - let evd = Evd.define evk newev evd in - evd,fst (destEvar newev),newargs - else - evd,evk,args +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 collect_vars c = - let rec collrec acc c = +let lift_aliases n (var_aliases,rel_aliases as aliases) = + if n = 0 then aliases else + (var_aliases, + Intmap.fold (fun p l -> Intmap.add (p+n) (List.map (lift n) l)) + rel_aliases Intmap.empty) + +let get_alias_chain_of aliases x = match kind_of_term x with + | Rel n -> (try Intmap.find n (snd aliases) with Not_found -> []) + | Var id -> (try Idmap.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,Intmap.empty) (mkVar id)) + +let extend_alias (_,b,_) (var_aliases,rel_aliases) = + let rel_aliases = + Intmap.fold (fun n l -> Intmap.add (n+1) (List.map (lift 1) l)) + rel_aliases Intmap.empty in + let rel_aliases = + match b with + | Some t -> + (match kind_of_term t with + | Var id' -> + let aliases_of_binder = + try Idmap.find id' var_aliases with Not_found -> [] in + Intmap.add 1 (aliases_of_binder@[t]) rel_aliases + | Rel p -> + let aliases_of_binder = + try Intmap.find (p+1) rel_aliases with Not_found -> [] in + Intmap.add 1 (aliases_of_binder@[mkRel (p+1)]) rel_aliases + | _ -> + Intmap.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 rec 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 Intset.empty and acc2 = ref Idset.empty in + let cache_rel = ref Intset.empty and cache_var = ref Idset.empty in + let is_in_cache depth = function + | Rel n -> Intset.mem (n-depth) !cache_rel + | Var s -> Idset.mem s !cache_var + | _ -> false in + let put_in_cache depth = function + | Rel n -> cache_rel := Intset.add (n-depth) !cache_rel + | Var s -> cache_var := Idset.add s !cache_var + | _ -> () in + let rec frec (aliases,depth) c = match kind_of_term c with - | Var id -> list_add_set id acc - | _ -> fold_constr collrec acc c + | 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 := Idset.add id !acc2 + | Rel n -> if n >= depth+1 then acc1 := Intset.add (n-depth) !acc1 + | _ -> frec (aliases,depth) c end + | Const _ | Ind _ | Construct _ -> + acc2 := List.fold_right Idset.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 - collrec [] c + frec (aliases,0) c; + (!acc1,!acc2) + +(************************************) +(* Removing a dependency in an evar *) +(************************************) type clear_dependency_error = | OccurHypInSimpleClause of identifier option @@ -460,6 +570,10 @@ type clear_dependency_error = exception ClearDependencyError of identifier * clear_dependency_error +open Store.Field + +let cleared = Store.field () + let rec check_and_clear_in_constr evdref err ids c = (* returns a new constr where all the evars have been 'cleaned' (ie the hypotheses ids have been removed from the contexts of @@ -477,7 +591,7 @@ let rec check_and_clear_in_constr evdref err ids c = List.iter check vars; c | Evar (evk,l as ev) -> - if Evd.is_defined_evar !evdref ev then + if Evd.is_defined !evdref evk then (* If evk is already defined we replace it by its definition *) let nc = whd_evar !evdref c in (check_and_clear_in_constr evdref err ids nc) @@ -487,7 +601,7 @@ let rec check_and_clear_in_constr evdref err ids c = arguments. Concurrently, we build a new evar corresponding to e where hypotheses of ids have been removed *) - let evi = Evd.find !evdref evk in + let evi = Evd.find_undefined !evdref evk in let ctxt = Evd.evar_filtered_context evi in let (nhyps,nargs,rids) = List.fold_right2 @@ -495,7 +609,7 @@ let rec check_and_clear_in_constr evdref err ids c = (* Check if some id to clear occurs in the instance a of rid in ev and remember the dependency *) match - List.filter (fun id -> List.mem id ids) (collect_vars a) + List.filter (fun id -> List.mem id ids) (Idset.elements (collect_vars a)) with | id :: _ -> (hy,ar,(rid,id)::ri) | _ -> @@ -521,6 +635,13 @@ let rec check_and_clear_in_constr evdref err ids c = let ev'= e_new_evar evdref env ~src:(evar_source evk !evdref) nconcl in evdref := Evd.define evk ev' !evdref; let (evk',_) = destEvar ev' in + (* spiwack: hacking session to mark the old [evk] as having been "cleared" *) + let evi = Evd.find !evdref evk in + let extra = evi.evar_extra in + let extra' = cleared.set true extra in + let evi' = { evi with evar_extra = extra' } in + evdref := Evd.add !evdref evk evi' ; + (* spiwack: /hacking session *) mkEvar(evk', Array.of_list nargs) end @@ -553,6 +674,270 @@ 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 rec 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 -> Idset.mem id fv_ids + | Rel n -> Intset.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 = + is_unification_pattern_evar env evd (evk,args) [] t <> None + +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,Idmap.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 Idmap.find idc all with Not_found -> [] in + if List.exists (fun (c,_,_) -> eq_constr a c) sub then + (rest,all,cstrs) + else + (rest, + Idmap.add idc ((a,normalize_alias_opt aliases a,id)::sub) all, + cstrs) + | _ -> + (rest,Idmap.add id [a,normalize_alias_opt aliases a,id] all,cstrs)) + | _ -> anomaly "Instance does not match its signature") + sign (array_rev_to_list args,Idmap.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 "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 @@ -586,28 +971,28 @@ let clear_hyps_in_evi evdref hyps concl ids = * [make_projectable_subst]) *) -exception NotUnique -exception NotUniqueInType of types - type evar_projection = | ProjectVar | ProjectEvar of existential * evar_info * identifier * evar_projection +exception NotUnique +exception NotUniqueInType of (identifier * 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 y = c' then id + if eq_constr y c' then id else if l <> [] then assoc_up_to_alias sigma aliases y yc l else (* Last chance, we reason up to alias conversion *) - match (if c == c' then cc else expand_full_opt aliases c') with - | Some cc when yc = cc -> id - | _ -> raise Not_found + 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 = expand_var aliases y in + 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 @@ -623,7 +1008,7 @@ let rec find_projectable_vars with_evars aliases sigma y subst = 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 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' @@ -680,7 +1065,7 @@ let rec do_projection_effects define_fun env ty evd = function 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 (destEvar ty') ty evd else evd + if isEvar ty' then define_fun env evd (destEvar ty') ty else evd else evd @@ -712,47 +1097,75 @@ type projectibility_status = | CannotInvert | Invertible of projectibility_kind -let invert_arg_from_subst aliases k sigma subst_in_env c_in_env_extended_with_k_binders = +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 sigma t in + let t = whd_evar evd t in match kind_of_term t with - | Rel i when i>k -> - project_with_effects aliases sigma effects (mkRel (i-k)) subst_in_env - | Var id -> - project_with_effects aliases sigma effects t subst_in_env - | _ -> - map_constr_with_binders succ aux k t in + | 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 k c_in_env_extended_with_k_binders in + 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 aliases k sigma evk subst_in_env c_in_env_extended_with_k_binders = - let res = invert_arg_from_subst aliases k sigma subst_in_env c_in_env_extended_with_k_binders in +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 occur_evar evk c -> CannotInvert - | _ -> res - + | Invertible (UniqueProjection (c,_)) when not (noccur_evar fullenv evd evk c) + -> + CannotInvert + | _ -> + res let effective_projections = map_succeed (function Invertible c -> c | _ -> failwith"") let instance_of_projection f env t evd projs = - let ty = lazy (Retyping.get_type_of env evd t) in + let ty = lazy (nf_evar evd (Retyping.get_type_of env evd t)) in match projs with | NoUniqueProjection -> raise NotUnique | UniqueProjection (c,effects) -> (List.fold_left (do_projection_effects f env ty) evd effects, c) -let filter_of_projection = function CannotInvert -> false | _ -> true +exception NotEnoughInformationToInvert -let filter_along f projs v = - let l = Array.to_list v in - let _,l = list_filter2 (fun b c -> f b) (projs,l) in - Array.of_list l +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 filter_of_projection = function Invertible _ -> true | _ -> false + +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. @@ -767,7 +1180,26 @@ let filter_along f projs v = * such that "hyps' |- ?e : T" *) -let restrict_hyps evd evk filter = +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 (Idset.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 (nf_evar evd (evar_concl evi)) in + let test (id,c,_) b = b || Idset.mem id vars || c <> None in + let newfilter = List.map2 test (evar_context evi) filter in + if 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 @@ -778,61 +1210,75 @@ let restrict_hyps evd evk filter = 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 evi = Evd.find evd evk in - let env = evar_unfiltered_env evi in - let oldfilter = evar_filter evi in - let filter,_ = List.fold_right (fun oldb (l,filter) -> - if oldb then List.hd filter::l,List.tl filter else (false::l,filter)) - oldfilter ([],List.rev filter) in - (env,evar_source evk evd,filter,evi.evar_concl) - -let do_restrict_hyps evd evk projs = - let filter = List.map filter_of_projection projs in - if List.for_all (fun x -> x) filter then - evd,evk - else - let env,src,filter,ccl = restrict_hyps evd evk filter in - let evd,nc = new_evar evd env ~src ~filter ccl in - let evd = Evd.define evk nc evd in - let evk',_ = destEvar nc in - evd,evk' - -(* [postpone_evar_term] postpones an equation of the form ?e[σ] = c *) - -let postpone_evar_term env evd (evk,argsv) rhs = + 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 evi = Evd.find evd evk in - let evd,evk,args = - restrict_upon_filter evd evi evk - (* Keep only variables that depends in rhs *) + 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) + (fun a -> not (isRel a || isVar a) + || dependent a rhs || List.exists (fun (id,_) -> isVarId id a) sols) (Array.to_list argsv) in - let args = Array.of_list args in - let pb = (Reduction.CONV,env,mkEvar(evk,args),rhs) in - Evd.add_conv_pb pb evd + let filter = match filter with + | None -> None + | Some filter -> closure_of_filter evd evk filter in + let candidates = extract_candidates sols in + if candidates <> None then + restrict_evar evd evk filter candidates + else + (* 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 -(* [postpone_evar_evar] postpones an equation of the form ?e1[σ1] = ?e2[σ2] *) +(* [postpone_evar_evar] postpones an equation of the form ?e1[?1] = ?e2[?2] *) -let postpone_evar_evar env evd projs1 (evk1,args1) projs2 (evk2,args2) = +let postpone_evar_evar f env evd filter1 ev1 filter2 ev2 = (* Leave an equation between (restrictions of) ev1 andv ev2 *) - let args1' = filter_along filter_of_projection projs1 args1 in - let evd,evk1' = do_restrict_hyps evd evk1 projs1 in - let args2' = filter_along filter_of_projection projs2 args2 in - let evd,evk2' = do_restrict_hyps evd evk2 projs2 in - let pb = (Reduction.CONV,env,mkEvar(evk1',args1'),mkEvar (evk2',args2')) in - add_conv_pb pb evd + 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 ?2 to the subset v_k1..v_kq of the vj that are - * inversible and we set ?1[x1..xn] := ?2[φk1(x1..xn)..φkp(x1..xn)] + * 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 @@ -850,63 +1296,214 @@ let are_canonical_instances args1 args2 env = let n2 = Array.length args2 in let rec aux n = function | (id,_,c)::sign - when n < n1 && args1.(n) = mkVar id && args1.(n) = args2.(n) -> + when n < n1 && isVarId id args1.(n) && isVarId id args2.(n) -> aux (n+1) sign | [] -> let rec aux2 n = n = n1 || - (args1.(n) = mkRel (n1-n) && args2.(n) = mkRel (n1-n) && aux2 (n+1)) + (isRelN (n1-n) args1.(n) && isRelN (n1-n) args2.(n) && aux2 (n+1)) in aux2 n | _ -> false in n1 = n2 & aux 0 (named_context env) -exception CannotProject of projectibility_status list +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 + List.filter (fun c2 -> + (filter_compatible_candidates conv_algo env evd evi2 args2 c1' c2 + <> None)) l2 <> []) l1 in + if 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 solve_evar_evar_l2r f env evd (evk1,args1) (evk2,args2 as ev2) = - let aliases = make_alias_map env in - let subst = make_projectable_subst aliases evd (Evd.find evd evk2) args2 in +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 nparams = + (fst (Global.lookup_inductive ind)).Declarations.mind_nparams + in + if nparams > Array.length args + then true (* We don't try to be more clever *) + else + let params,_ = array_chop nparams 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',_) -> ev' <> ev (*If ev' needed, one may also try to restrict it*) + | Var id -> Idset.mem id fv_ids + | Rel n -> n <= k || Intset.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 -> Idset.mem id fv_ids + | Rel n -> n <= k || Intset.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 subst = List.map (fun (id,_,_) -> mkVar id) sign in - Evd.define evk2 (mkEvar(evk1,Array.of_list subst)) evd + let id_inst = list_map_to_array (fun (id,_,_) -> mkVar id) sign in + Evd.define evk2 (mkEvar(evk1,id_inst)) evd else - let proj1 = array_map_to_list (invert_arg aliases 0 evd evk2 subst) args1 in - try - (* Instantiate ev2 with (a restriction of) ev1 if uniquely projectable *) - let proj1' = effective_projections proj1 in - let evd,args1' = - list_fold_map (instance_of_projection f env (mkEvar ev2)) evd proj1' in - let evd,evk1' = do_restrict_hyps evd evk1 proj1 in - Evd.define evk2 (mkEvar(evk1',Array.of_list args1')) evd - with NotUnique -> - raise (CannotProject proj1) - -let solve_evar_evar f env evd ev1 ev2 = - try solve_evar_evar_l2r f env evd ev1 ev2 - with CannotProject projs1 -> - try solve_evar_evar_l2r f env evd ev2 ev1 - with CannotProject projs2 -> - postpone_evar_evar env evd projs1 ev1 projs2 ev2 - -(* Solve pbs (?i x1..xn) = (?i y1..yn) which arises often in fixpoint - * definitions. We try to unify the xi with the yi pairwise. The pairs - * that don't unify are discarded (i.e. ?i is redefined so that it does not + 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_unfiltered_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 e when Errors.noncritical e -> 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 conv_algo env evd evk argsv1 argsv2 = - if argsv1 = argsv2 then evd else - let evi = Evd.find evd evk in +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 evd,evk,args = - restrict_upon_filter evd evi evk + 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 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 *) - let args1,args2 = List.split args in - let argsv1 = Array.of_list args1 and argsv2 = Array.of_list args2 in - let pb = (Reduction.CONV,env,mkEvar(evk,argsv1),mkEvar(evk,argsv2)) in - Evd.add_conv_pb pb evd + 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 @@ -925,22 +1522,22 @@ let solve_refl conv_algo env evd evk argsv1 argsv2 = * 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] + * 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 +exception NotEnoughInformationToProgress of (identifier * evar_projection) list exception OccurCheckIn of evar_map * constr -let rec invert_definition choose env evd (evk,argsv as ev) rhs = +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 = make_projectable_subst aliases evd evi argsv in + let subst,cstr_subst = make_projectable_subst aliases evd evi argsv in (* Projection *) let project_variable t = @@ -951,67 +1548,120 @@ let rec invert_definition choose env evd (evk,argsv as ev) rhs = | [] -> raise Not_found | [id,p] -> (mkVar id, p) | (id,p)::_::_ -> - if choose then (mkVar id, p) - else raise (NotUniqueInType(find_solution_type (evar_env evi) sols)) + 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 env ty !evdref p 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 ty -> - if not !progress then raise NotEnoughInformationToProgress; + | 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_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 args' = filter_along (fun x -> x) filter argsv in - let evarenv,src,filter,_ = restrict_hyps !evdref evk filter in - let evd,evar = new_evar !evdref evarenv ~src ~filter ty in - let evk',_ = destEvar evar in - let pb = (Reduction.CONV,env,mkEvar(evk',args'),t) in - evdref := Evd.add_conv_pb pb evd; + 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 = + if candidates <> None then restrict_evar evd evk' filter candidates + else + let evd,ev'' = restrict_applied_evar evd ev' filter None in + Evd.add_conv_pb (Reduction.CONV,env,mkEvar ev'',t) evd 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 -> project_variable (mkRel (i-k)) - | Var id -> project_variable t + | 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 evk = evk' then raise (OccurCheckIn (evd,rhs)); (* Evar/Evar problem (but left evar is virtual) *) - let projs' = - array_map_to_list - (invert_arg_from_subst aliases k !evdref subst) args' - in - (try - (* Try to project (a restriction of) the right evar *) - let eprojs' = effective_projections projs' in - let evd,args' = - list_fold_map (instance_of_projection evar_define env' t) - !evdref eprojs' in - let evd,evk' = do_restrict_hyps evd evk' projs' in + 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; - mkEvar (evk',Array.of_list args') - with NotUnique -> + body + with + | EvarSolvedOnTheFly (evd,t) -> evdref:=evd; imitate envk t + | CannotProject filter' -> assert !progress; (* Make the virtual left evar real *) - let (evar'',ev'') = extend_evar env' evdref k ev t in + 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 solve_evar_evar_l2r evar_define env' !evdref ev'' ev' - with CannotProject projs'' -> - (* ... or postpone the problem *) - postpone_evar_evar env' !evdref projs'' ev'' projs' ev' in + (* 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; - (* 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 + 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 e when Errors.noncritical e -> 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 @@ -1024,15 +1674,19 @@ let rec invert_definition choose env evd (evk,argsv as ev) rhs = * context "hyps" and not referring to itself. *) -and occur_existential evm c = - let rec occrec c = match kind_of_term c with - | Evar (e, _) -> if not (is_defined evm e) then raise Occur - | _ -> iter_constr occrec c - in try occrec c; false with Occur -> true - -and evar_define ?(choose=false) env (evk,argsv as ev) rhs evd = +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 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 choose env evd ev rhs in + 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 *) @@ -1055,10 +1709,11 @@ and evar_define ?(choose=false) env (evk,argsv as ev) rhs evd = str "----> " ++ int ev ++ str " := " ++ print_constr body); raise e in*) - Evd.define evk body evd' + let evd' = Evd.define evk body evd' in + check_evar_instance evd' evk body conv_algo with - | NotEnoughInformationToProgress -> - postpone_evar_term env evd ev rhs + | 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) -> @@ -1072,138 +1727,6 @@ and evar_define ?(choose=false) env (evk,argsv as ev) rhs evd = | _ -> error_occur_check env evd evk rhs -(*-------------------*) -(* Auxiliary functions for the conversion algorithms modulo evars - *) - -let has_undefined_evars_or_sorts evd t = - let rec has_ev t = - match kind_of_term t with - | Evar (ev,args) -> - (match evar_body (Evd.find evd ev) with - | Evar_defined c -> - has_ev c; Array.iter has_ev args - | Evar_empty -> - raise NotInstantiatedEvar) - | Sort s when is_sort_variable evd s -> raise Not_found - | _ -> iter_constr has_ev t in - try let _ = has_ev t in false - with (Not_found | NotInstantiatedEvar) -> true - -let is_ground_term evd t = - not (has_undefined_evars_or_sorts evd t) - -let is_ground_env evd env = - let is_ground_decl = function - (_,Some b,_) -> is_ground_term evd b - | _ -> true in - List.for_all is_ground_decl (rel_context env) && - List.for_all is_ground_decl (named_context env) -(* Memoization is safe since evar_map and environ are applicative - structures *) -let is_ground_env = memo1_2 is_ground_env - -(* Return the head evar if any *) - -exception NoHeadEvar - -let head_evar = - let rec hrec c = match kind_of_term c with - | Evar (evk,_) -> evk - | Case (_,_,c,_) -> hrec c - | App (c,_) -> hrec c - | Cast (c,_,_) -> hrec c - | _ -> raise NoHeadEvar - in - hrec - -(* Expand head evar if any (currently consider only applications but I - guess it should consider Case too) *) - -let whd_head_evar_stack sigma c = - let rec whrec (c, l as s) = - match kind_of_term c with - | Evar (evk,args as ev) when Evd.is_defined sigma evk - -> whrec (existential_value sigma ev, l) - | Cast (c,_,_) -> whrec (c, l) - | App (f,args) -> whrec (f, Array.fold_right (fun a l -> a::l) args l) - | _ -> s - in - whrec (c, []) - -let whd_head_evar sigma c = applist (whd_head_evar_stack sigma c) - -(* Check if an applied evar "?X[args] l" is a Miller's pattern; note - that we don't care whether args itself contains Rel's or even Rel's - distinct from the ones in l *) - -let rec expand_and_check_vars env = function - | [] -> [] - | a::l -> - if isRel a or isVar a then - let l = expand_and_check_vars env l in - match expand_var_opt env a with - | None -> a :: l - | Some a' when isRel a' or isVar a' -> list_add_set a' l - | _ -> raise Exit - else - raise Exit - -let is_unification_pattern_evar env (_,args) l t = - List.for_all (fun x -> isRel x || isVar x) l (* common failure case *) - && - let aliases = make_alias_map env in - let l' = Array.to_list args @ l in - let l'' = try Some (expand_and_check_vars aliases l') with Exit -> None in - match l'' with - | Some l -> - let deps = - 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 t = expand_vars_in_term_using aliases t in - let fv_rels = free_rels t in - let fv_ids = global_vars env t in - List.filter (fun c -> - match kind_of_term c with - | Var id -> List.mem id fv_ids - | Rel n -> Intset.mem n fv_rels - | _ -> assert false) l in - list_distinct deps - | None -> false - -let is_unification_pattern (env,nb) f l t = - match kind_of_term f with - | Meta _ -> - array_for_all (fun c -> isRel c && destRel c <= nb) l - && array_distinct l - | Evar ev -> - is_unification_pattern_evar env ev (Array.to_list l) t - | _ -> - false - -(* From a unification problem "?X l1 = term1 l2" such that l1 is made - of distinct rel's, build "\x1...xn.(term1 l2)" (patterns unification) *) -(* NB: does not work when (term1 l2) contains 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 l1 c = - let l1 = List.map (expand_var (make_alias_map env)) l1 in - 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 (na,_,t) = lookup_rel n env in mkLambda (na,lift n t,c') - | Var id -> let (id,_,t) = lookup_named id env in mkNamedLambda id t c' - | _ -> assert false) - l1 c in - (* Warning: we may miss some opportunity to eta-reduce more since c' - is not in normal form *) - whd_eta c' - (* 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 @@ -1234,23 +1757,12 @@ 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) -(* Util *) - -let check_instance_type conv_algo env evd ev1 t2 = - let t2 = nf_evar evd t2 in - if has_undefined_evars_or_sorts evd t2 then - (* May contain larger constraints than needed: don't want to - commit to an equal solution while only subtyping is requested *) - evd - else - let typ2 = Retyping.get_type_of env evd (refresh_universes t2) in - if isEvar typ2 then (* Don't want to commit too early too *) evd - else - let typ1 = existential_type evd ev1 in - let evd,b = conv_algo env evd Reduction.CUMUL typ2 typ1 in - if b then evd else - user_err_loc (fst (evar_source (fst ev1) evd),"", - str "Unable to find a well-typed instantiation") +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 @@ -1261,51 +1773,75 @@ let check_instance_type conv_algo env evd ev1 t2 = 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 kind_of_term t2 with - | Evar (evk2,args2 as ev2) -> - if evk1 = evk2 then - solve_refl conv_algo env evd evk1 args1 args2 - else - if pbty = None - then solve_evar_evar evar_define env evd ev1 ev2 - else if pbty = Some true then - add_conv_pb (Reduction.CUMUL,env,mkEvar ev1,t2) evd - else - add_conv_pb (Reduction.CUMUL,env,t2,mkEvar ev1) evd + 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 | _ -> - let evd = - if pbty = Some false then - check_instance_type conv_algo env evd ev1 t2 - else - evd in - let evd = evar_define ~choose env ev1 t2 evd in - let evi = Evd.find evd evk1 in - if occur_existential evd evi.evar_concl then - let evenv = evar_unfiltered_env evi in - let evc = nf_evar evd evi.evar_concl in - match evi.evar_body with - | Evar_defined body -> - let ty = nf_evar evd (Retyping.get_type_of evenv evd body) in - add_conv_pb (Reduction.CUMUL,evenv,ty,evc) evd - | Evar_empty -> (* Resulted in a constraint *) - evd - else evd - in - 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 + 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 *) + let evars_of_term c = let rec evrec acc c = match kind_of_term c with - | Evar (n, _) -> Intset.add n acc + | Evar (n, l) -> Intset.add n (Array.fold_left evrec acc l) | _ -> fold_constr evrec acc c in - evrec Intset.empty c + evrec Intset.empty c + +(* spiwack: a few functions to gather evars on which goals depend. *) +let queue_set q is_dependent set = + Intset.iter (fun a -> Queue.push (is_dependent,a) q) set +let queue_term q is_dependent c = + queue_set q is_dependent (evars_of_term c) + +let process_dependent_evar q acc evm is_dependent e = + let evi = Evd.find evm e in + (* Queues evars appearing in the types of the goal (conclusion, then + hypotheses), they are all dependent. *) + queue_term q true evi.evar_concl; + List.iter begin fun (_,b,t) -> + queue_term q true t; + match b with + | None -> () + | Some b -> queue_term q true b + end (Environ.named_context_of_val evi.evar_hyps); + match evi.evar_body with + | Evar_empty -> + if is_dependent then Intmap.add e None acc else acc + | Evar_defined b -> + let subevars = evars_of_term b in + (* evars appearing in the definition of an evar [e] are marked + as dependent when [e] is dependent itself: if [e] is a + non-dependent goal, then, unless they are reach from another + path, these evars are just other non-dependent goals. *) + queue_set q is_dependent subevars; + if is_dependent then Intmap.add e (Some subevars) acc else acc + +let gather_dependent_evars q evm = + let acc = ref Intmap.empty in + while not (Queue.is_empty q) do + let (is_dependent,e) = Queue.pop q in + (* checks if [e] has already been added to [!acc] *) + begin if not (Intmap.mem e !acc) then + acc := process_dependent_evar q !acc evm is_dependent e + end + done; + !acc + +let gather_dependent_evars evm l = + let q = Queue.create () in + List.iter (fun a -> Queue.add (false,a) q) l; + gather_dependent_evars q evm + +(* /spiwack *) let evars_of_named_context nc = List.fold_right (fun (_, b, t) s -> @@ -1322,36 +1858,64 @@ let evars_of_evar_info evi = | Evar_defined b -> evars_of_term b) (evars_of_named_context (named_context_of_val evi.evar_hyps))) +(** The following functions return the set of undefined evars + contained in the object, the defined evars being traversed. + This is roughly a combination of the previous functions and + [nf_evar]. *) + +let undefined_evars_of_term evd t = + let rec evrec acc c = + match kind_of_term c with + | Evar (n, l) -> + let acc = Array.fold_left evrec acc l in + (try match (Evd.find evd n).evar_body with + | Evar_empty -> Intset.add n acc + | Evar_defined c -> evrec acc c + with Not_found -> anomaly "undefined_evars_of_term: evar not found") + | _ -> fold_constr evrec acc c + in + evrec Intset.empty t + +let undefined_evars_of_named_context evd nc = + List.fold_right (fun (_, b, t) s -> + Option.fold_left (fun s t -> + Intset.union s (undefined_evars_of_term evd t)) + (Intset.union s (undefined_evars_of_term evd t)) b) + nc Intset.empty + +let undefined_evars_of_evar_info evd evi = + Intset.union (undefined_evars_of_term evd evi.evar_concl) + (Intset.union + (match evi.evar_body with + | Evar_empty -> Intset.empty + | Evar_defined b -> undefined_evars_of_term evd b) + (undefined_evars_of_named_context evd + (named_context_of_val evi.evar_hyps))) + (* [check_evars] fails if some unresolved evar remains *) -(* it assumes that the defined existentials have already been substituted *) -let check_evars env initial_sigma evd c = - let sigma = evd in - let c = nf_evar sigma c in +let check_evars env initial_sigma sigma c = let rec proc_rec c = match kind_of_term c with - | Evar (evk,args) -> - assert (Evd.mem sigma evk); + | Evar (evk,_ as ev) -> + (match existential_opt_value sigma ev with + | Some c -> proc_rec c + | None -> if not (Evd.mem initial_sigma evk) then let (loc,k) = evar_source evk sigma in - (match k with + match k with | ImplicitArg (gr, (i, id), false) -> () | _ -> - let evi = nf_evar_info sigma (Evd.find sigma evk) in + let evi = nf_evar_info sigma (Evd.find_undefined sigma evk) in error_unsolvable_implicit loc env sigma evi k None) | _ -> iter_constr proc_rec c in proc_rec c -(* This returns the evars of [sigma] that are not in [sigma0] and - [sigma] minus these evars *) - -let subtract_evars sigma0 sigma = - Evd.fold (fun evk ev (sigma,sigma' as acc) -> - if Evd.mem sigma0 evk || Evd.mem sigma' evk then acc else - (Evd.remove sigma evk,Evd.add sigma' evk ev)) - sigma (sigma,Evd.empty) +open Glob_term +(****************************************) (* Operations on value/type constraints *) +(****************************************) type type_constraint_type = (int * int) option * constr type type_constraint = type_constraint_type option @@ -1390,44 +1954,92 @@ let empty_valcon = None (* Builds a value constraint *) let mk_valcon c = Some c -(* Refining an evar to a product or a sort *) -(* Declaring any type to be in the sort Type shouldn't be harmful since - cumulativity now includes Prop and Set in Type... - It is, but that's not too bad *) -let define_evar_as_abstraction abs evd (ev,args) = - let evi = Evd.find evd ev in +let idx = id_of_string "x" + +(* Refining an evar to a product *) + +let define_pure_evar_as_product evd evk = + let evi = Evd.find_undefined evd evk in let evenv = evar_unfiltered_env evi in - let (evd1,dom) = new_evar evd evenv (new_Type()) ~filter:(evar_filter evi) in - let nvar = - next_ident_away (id_of_string "x") - (ids_of_named_context (evar_context evi)) in - let newenv = push_named (nvar, None, dom) evenv in - let (evd2,rng) = - new_evar evd1 newenv ~src:(evar_source ev evd1) (new_Type()) - ~filter:(true::evar_filter evi) in - let prod = abs (Name nvar, dom, subst_var nvar rng) in - let evd3 = Evd.define ev prod evd2 in - let evdom = fst (destEvar dom), args in - let evrng = - fst (destEvar rng), array_cons (mkRel 1) (Array.map (lift 1) args) in - let prod' = abs (Name nvar, mkEvar evdom, mkEvar evrng) in - (evd3,prod') - -let define_evar_as_product evd (ev,args) = - define_evar_as_abstraction (fun t -> mkProd t) evd (ev,args) - -let define_evar_as_lambda evd (ev,args) = - define_evar_as_abstraction (fun t -> mkLambda t) evd (ev,args) + let id = next_ident_away idx (ids_of_named_context (evar_context evi)) in + let evd1,dom = new_type_evar evd evenv ~filter:(evar_filter evi) in + let evd2,rng = + let newenv = push_named (id, None, dom) evenv in + let src = evar_source evk evd1 in + let filter = true::evar_filter evi in + new_type_evar evd1 newenv ~src ~filter in + let prod = mkProd (Name id, dom, subst_var id rng) in + let evd3 = Evd.define evk prod evd2 in + evd3,prod + +(* Refine an applied evar to a product and returns its instantiation *) + +let define_evar_as_product evd (evk,args) = + let evd,prod = define_pure_evar_as_product evd evk in + (* Quick way to compute the instantiation of evk with args *) + let na,dom,rng = destProd prod in + let evdom = mkEvar (fst (destEvar dom), args) in + let evrngargs = array_cons (mkRel 1) (Array.map (lift 1) args) in + let evrng = mkEvar (fst (destEvar rng), evrngargs) in + evd,mkProd (na, evdom, evrng) + +(* Refine an evar with an abstraction + + I.e., solve x1..xq |- ?e:T(x1..xq) with e:=λy:A.?e'[x1..xq,y] where: + - either T(x1..xq) = πy:A(x1..xq).B(x1..xq,y) + or T(x1..xq) = ?d[x1..xq] and we define ?d := πy:?A.?B + with x1..xq |- ?A:Type and x1..xq,y |- ?B:Type + - x1..xq,y:A |- ?e':B +*) + +let define_pure_evar_as_lambda env evd evk = + let evi = Evd.find_undefined evd evk in + let evenv = evar_unfiltered_env evi in + let typ = whd_betadeltaiota env evd (evar_concl evi) in + let evd1,(na,dom,rng) = match kind_of_term typ with + | Prod (na,dom,rng) -> (evd,(na,dom,rng)) + | Evar ev' -> let evd,typ = define_evar_as_product evd ev' in evd,destProd typ + | _ -> error_not_product_loc dummy_loc env evd typ in + let avoid = ids_of_named_context (evar_context evi) in + let id = + next_name_away_with_default_using_types "x" na avoid (whd_evar evd dom) in + let newenv = push_named (id, None, dom) evenv in + let filter = true::evar_filter evi in + let src = evar_source evk evd1 in + let evd2,body = new_evar evd1 newenv ~src (subst1 (mkVar id) rng) ~filter in + let lam = mkLambda (Name id, dom, subst_var id body) in + Evd.define evk lam evd2, lam + +let define_evar_as_lambda env evd (evk,args) = + let evd,lam = define_pure_evar_as_lambda env evd evk in + (* Quick way to compute the instantiation of evk with args *) + let na,dom,body = destLambda lam in + let evbodyargs = array_cons (mkRel 1) (Array.map (lift 1) args) in + let evbody = mkEvar (fst (destEvar body), evbodyargs) in + evd,mkLambda (na, dom, evbody) + +let rec evar_absorb_arguments env evd (evk,args as ev) = function + | [] -> evd,ev + | a::l -> + (* TODO: optimize and avoid introducing intermediate evars *) + let evd,lam = define_pure_evar_as_lambda env evd evk in + let _,_,body = destLambda lam in + let evk = fst (destEvar body) in + evar_absorb_arguments env evd (evk, array_cons a args) l + +(* Refining an evar to a sort *) let define_evar_as_sort evd (ev,args) = - let s = new_Type () in - Evd.define ev s evd, destSort s + let evd, s = new_sort_variable evd in + Evd.define ev (mkSort s) evd, s (* We don't try to guess in which sort the type should be defined, since any type has type Type. May cause some trouble, but not so far... *) -let judge_of_new_Type () = Typeops.judge_of_type (new_univ ()) +let judge_of_new_Type evd = + let evd', s = new_univ_variable evd in + evd', Typeops.judge_of_type s (* Propagation of constraints through application and abstraction: Given a type constraint on a functional term, returns the type @@ -1443,10 +2055,13 @@ let split_tycon loc env evd tycon = let t = whd_betadeltaiota env evd c in match kind_of_term t with | Prod (na,dom,rng) -> evd, (na, dom, rng) - | Evar ev when not (Evd.is_defined_evar evd ev) -> + | Evar ev (* ev is undefined because of whd_betadeltaiota *) -> let (evd',prod) = define_evar_as_product evd ev in let (_,dom,rng) = destProd prod in evd',(Anonymous, dom, rng) + | App (c,args) when isEvar c -> + let (evd',lam) = define_evar_as_lambda env evd (destEvar c) in + real_split evd' (mkApp (lam,args)) | _ -> error_not_product_loc loc env evd c in match tycon with |