diff options
Diffstat (limited to 'pretyping/evarutil.ml')
| -rw-r--r-- | pretyping/evarutil.ml | 140 |
1 files changed, 105 insertions, 35 deletions
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index 506cd03f..307c9886 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: evarutil.ml 8759 2006-04-28 12:24:14Z herbelin $ *) +(* $Id: evarutil.ml 9154 2006-09-20 17:18:18Z corbinea $ *) open Util open Pp @@ -21,13 +21,6 @@ open Evd open Reductionops open Pretype_errors - -let rec filter_unique = function - | [] -> [] - | x::l -> - if List.mem x l then filter_unique (List.filter (fun y -> x<>y) l) - else x::filter_unique l - (* Expanding existential variables (pretyping.ml) *) (* 1- whd_ise fails if an existential is undefined *) @@ -63,9 +56,9 @@ let jv_nf_evar = Pretype_errors.jv_nf_evar let tj_nf_evar = Pretype_errors.tj_nf_evar let nf_evar_info evc info = - { evar_concl = Reductionops.nf_evar evc info.evar_concl; - evar_hyps = map_named_val (Reductionops.nf_evar evc) info.evar_hyps; - evar_body = info.evar_body} + { info with + evar_concl = Reductionops.nf_evar evc info.evar_concl; + evar_hyps = map_named_val (Reductionops.nf_evar evc) info.evar_hyps} let nf_evars evm = Evd.fold (fun ev evi evm' -> Evd.add evm' ev (nf_evar_info evm evi)) evm Evd.empty @@ -310,29 +303,45 @@ let is_defined_equation env evd (ev,inst) rhs = * ?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. *) + * a prefix of ?2's env, included in ?1's env. + + Concretely, the assumptions are "env |- ev : T" and "Gamma |- + ev[hyps:=args]" for some Gamma whose de Bruijn context has length k. + We create "env' |- ev' : T" for some env' <= env and define ev:=ev' +*) -let do_restrict_hyps evd ev args = +let do_restrict_hyps env k evd ev args = let args = Array.to_list args in let evi = Evd.find (evars_of !evd) ev in - let env = evar_env evi in let hyps = evar_context evi in - let (sign,ncargs) = list_filter2 (fun _ a -> closed0 a) (hyps,args) in + let (hyps',ncargs) = list_filter2 (fun _ a -> closedn k a) (hyps,args) in (* No care is taken in case the evar type uses vars filtered out! - Is it important ? *) - let nc = - let env = - Sign.fold_named_context push_named sign ~init:(reset_context env) in - e_new_evar evd env ~src:(evar_source ev !evd) evi.evar_concl in + Assuming that the restriction comes from a well-typed Flex/Flex + unification problem (see real_clean), the type of the evar cannot + depend on variables that are not in the scope of the other evar, + since this other evar has the same type (up to unification). + Since moreover, the evar contexts uses names only, the + restriction raise no de Bruijn reallocation problem *) + let env' = + Sign.fold_named_context push_named hyps' ~init:(reset_context env) in + let nc = e_new_evar evd env' ~src:(evar_source ev !evd) evi.evar_concl in evd := Evd.evar_define ev nc !evd; let (evn,_) = destEvar nc in mkEvar(evn,Array.of_list ncargs) - -let need_restriction isevars args = not (array_for_all closed0 args) +let need_restriction k args = not (array_for_all (closedn k) args) (* We try to instantiate the evar assuming the body won't depend - * on arguments that are not Rels or Vars, or appearing several times. + * on arguments that are not Rels or Vars, or appearing several times + (i.e. we tackle only Miller-Pfenning patterns unification) + + 1) Let a unification problem "env |- ev[hyps:=args] = rhs" + 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 failing if some Rel/Var not in scope + + Note: we don't assume rhs in normal form, it may fail while it would + have succeeded after some reductions *) (* Note: error_not_clean should not be an error: it simply means that the * conversion test that lead to the faulty call to [real_clean] should return @@ -341,36 +350,52 @@ let need_restriction isevars args = not (array_for_all closed0 args) let real_clean env isevars ev evi args rhs = let evd = ref isevars in - let subst = List.map (fun (x,y) -> (y,mkVar x)) (filter_unique args) in + let subst = List.map (fun (x,y) -> (y,mkVar x)) (list_uniquize args) in let rec subs rigid k t = match kind_of_term t with | Rel i -> if i<=k then t - else (try List.assoc (mkRel (i-k)) subst with Not_found -> t) + else + (* Flex/Rel problem: unifiable as a pattern iff Rel in ev scope *) + (try List.assoc (mkRel (i-k)) subst + with Not_found -> if rigid then raise Exit else t) | Evar (ev,args) -> if Evd.is_defined_evar !evd (ev,args) then subs rigid k (existential_value (evars_of !evd) (ev,args)) else + (* Flex/Flex problem: restriction to a common scope *) let args' = Array.map (subs false k) args in - if need_restriction !evd args' then - do_restrict_hyps evd ev args' + if need_restriction k args' then + do_restrict_hyps (reset_context env) k evd ev args' else mkEvar (ev,args') | Var id -> + (* Flex/Var problem: unifiable as a pattern iff Var in scope of ev *) (try List.assoc t subst with Not_found -> if not rigid + (* I don't understand this line: vars from evar_context evi + are private (especially some of them are freshly + generated in push_rel_context_to_named_context). They + have a priori nothing to do with the vars in env. I + remove the test [HH 25/8/06] + or List.exists (fun (id',_,_) -> id=id') (evar_context evi) + *) then t - else - error_not_clean env (evars_of !evd) ev rhs - (evar_source ev !evd)) - | _ -> map_constr_with_binders succ (subs rigid) k t + else raise Exit) + + | _ -> + (* Flex/Rigid problem (or assimilated if not normal): we "imitate" *) + map_constr_with_binders succ (subs rigid) k t in - let body = subs true 0 (nf_evar (evars_of isevars) rhs) in - if not (closed0 body) - then error_not_clean env (evars_of !evd) ev body (evar_source ev !evd); + let rhs = nf_evar (evars_of isevars) rhs in + let rhs = whd_beta rhs (* heuristic *) in + let body = + try subs true 0 rhs + with Exit -> + error_not_clean env (evars_of !evd) ev rhs (evar_source ev !evd) in (!evd,body) (* [evar_define] solves the problem lhs = rhs when lhs is an uninstantiated @@ -464,6 +489,34 @@ let head_evar = in hrec +(* 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 is_unification_pattern_evar (_,args) l = + let l' = Array.to_list args @ l in + List.for_all (fun a -> isRel a or isVar a) l' & list_distinct l' + +let is_unification_pattern f l = + match kind_of_term f with + | Meta _ -> array_for_all isRel l & array_distinct l + | Evar ev -> is_unification_pattern_evar ev (Array.to_list l) + | _ -> 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) *) + +let solve_pattern_eqn env l1 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 (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 + 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 @@ -550,11 +603,28 @@ let solve_simple_eqn conv_algo env isevars (pbty,(n1,args1 as ev1),t2) = let (isevars,pbs) = get_conv_pbs isevars (status_changed lsp) in List.fold_left (fun (isevars,b as p) (pbty,t1,t2) -> - if b then conv_algo env isevars pbty t1 t2 else p) (isevars,true) + if b then conv_algo env isevars pbty t1 t2 else p) (isevars,true) pbs with e when precatchable_exception e -> (isevars,false) + +(* [check_evars] fails if some unresolved evar remains *) +(* it assumes that the defined existentials have already been substituted *) + +let check_evars env initial_sigma isevars c = + let sigma = evars_of isevars in + let c = nf_evar sigma c in + let rec proc_rec c = + match kind_of_term c with + | Evar (ev,args) -> + assert (Evd.mem sigma ev); + if not (Evd.mem initial_sigma ev) then + let (loc,k) = evar_source ev isevars in + error_unsolvable_implicit loc env sigma k + | _ -> iter_constr proc_rec c + in proc_rec c + (* Operations on value/type constraints *) type type_constraint_type = (int * int) option * constr |