diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/evarutil.ml | 124 | ||||
| -rw-r--r-- | pretyping/termops.ml | 19 | ||||
| -rw-r--r-- | pretyping/termops.mli | 3 |
3 files changed, 73 insertions, 73 deletions
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index b9f09509c..0fa1111ff 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -391,77 +391,68 @@ let check_restricted_occur evd refine env filter constr = let res = aux 0 constr in Array.to_list filter, res +(* We have a unification problem Σ; Γ |- ?e[u1..uq] = ty : s where ?e is not + * defined in Σ but yet known to be definable in some context x1:T1..xq:Tq. + * [declare_dangling_evar ... Γ Σ c ty (x1:T1..xq:Tq) .. (u1..uq) (x1..xq)] + * declares x1:T1..xq:Tq |- ?e : s such that ?e[u1..uq] = ty holds. + *) + +let define_evar_from_virtual_equation define_fun env evd t_in_env sign filter inst_in_env + inst_in_sign = + 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 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 + * 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. + * [extend_evar Γ evd k (?e1[u1..uq]) c] extend Σ 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 * - * This is what [extend_evar Γ evd k (?e1[u1..uq]) c] does. + * 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 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 isRel c && destRel c = 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 isVar c && destVar c = 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 +let materialize_evar define_fun env evd k (evk1,args1) ty = + 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 ids1 = List.map pi1 (named_context_of_val sign1) 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) -> + match b with + | None -> + 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 inst_in_sign in + (push_named_context_val (id,None,t_in_sign) sign,true::filter, + (mkRel 1)::(List.map (lift 1) inst_in_env),(mkVar id)::inst_in_sign, + push_rel d env,evd,id::avoid) + | Some b -> + (sign,filter,inst_in_env,inst_in_sign, + push_rel d env,evd,avoid)) + rel_sign + (sign1,evar_filter evi1,Array.to_list args1, + List.map mkVar ids1,env1,evd,ids1) in - shrink_named subst [] rev_named_sign - -let extend_evar env evdref k (evk1,args1) ty = - 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_undefined !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 evd,ev2ty_in_sign = + define_evar_from_virtual_equation define_fun env evd ty + sign2 filter2 inst2_in_env inst2_in_sign 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 subfilter env ccl filter newfilter args = let vars = collect_vars ccl in @@ -1104,11 +1095,12 @@ let rec invert_definition conv_algo choose env evd (evk,argsv as ev) rhs = assert !progress; (* Make the virtual left evar real *) let ty = get_type_of env' !evdref t in - let (evar'',ev'') = extend_evar env' evdref k ev ty in - (try + let (evd,evar'',ev'') = + materialize_evar (evar_define conv_algo) env' !evdref k ev ty in + (try let evd = (* Try to project (a restriction of) the left evar ... *) - try solve_evar_evar_l2r (evar_define conv_algo) env' !evdref ev'' ev' + try solve_evar_evar_l2r (evar_define conv_algo) env' evd ev'' ev' with CannotProject projs'' -> (* ... or postpone the problem *) postpone_evar_evar env' evd projs'' ev'' projs' ev' diff --git a/pretyping/termops.ml b/pretyping/termops.ml index 452b395dd..b28f8046f 100644 --- a/pretyping/termops.ml +++ b/pretyping/termops.ml @@ -623,7 +623,8 @@ let my_prefix_application eq_fun (k,c) (by_c : constr) (t : constr) = | _ -> None (* Recognizing occurrences of a given subterm in a term: [subst_term c t] - substitutes [(Rel 1)] for all occurrences of term [c] in a term [t] *) + substitutes [(Rel 1)] for all occurrences of term [c] in a term [t]; + works if [c] has rels *) let subst_term_gen eq_fun c t = let rec substrec (k,c as kc) t = @@ -636,10 +637,11 @@ let subst_term_gen eq_fun c t = in substrec (1,c) t +let subst_term = subst_term_gen eq_constr + (* Recognizing occurrences of a given subterm in a term : [replace_term c1 c2 t] substitutes [c2] for all occurrences of - term [c1] in a term [t] *) -(*i Meme remarque : a priori [c] n'est pas forcement clos i*) + term [c1] in a term [t]; works if [c1] and [c2] have rels *) let replace_term_gen eq_fun c by_c in_t = let rec substrec (k,c as kc) t = @@ -652,8 +654,6 @@ let replace_term_gen eq_fun c by_c in_t = in substrec (0,c) in_t -let subst_term = subst_term_gen eq_constr - let replace_term = replace_term_gen eq_constr (* Substitute only at a list of locations or excluding a list of @@ -1068,7 +1068,7 @@ let on_judgment_value f j = { j with uj_val = f j.uj_val } let on_judgment_type f j = { j with uj_type = f j.uj_type } (* Cut a context ctx in 2 parts (ctx1,ctx2) with ctx1 containing k - variables *) + variables; skips let-in's *) let context_chop k ctx = let rec chop_aux acc = function | (0, l2) -> (List.rev acc, l2) @@ -1077,6 +1077,13 @@ let context_chop k ctx = | (_, []) -> anomaly "context_chop" in chop_aux [] (k,ctx) +(* Do not skip let-in's *) +let env_rel_context_chop k env = + let rels = rel_context env in + let ctx1,ctx2 = list_chop k rels in + push_rel_context ctx2 (reset_with_named_context (named_context_val env) env), + ctx1 + (*******************************************) (* Functions to deal with impossible cases *) (*******************************************) diff --git a/pretyping/termops.mli b/pretyping/termops.mli index 2028e5aca..d101d7d4f 100644 --- a/pretyping/termops.mli +++ b/pretyping/termops.mli @@ -240,7 +240,8 @@ val ids_of_named_context : named_context -> identifier list val ids_of_context : env -> identifier list val names_of_rel_context : env -> names_context -val context_chop : int -> rel_context -> (rel_context*rel_context) +val context_chop : int -> rel_context -> rel_context * rel_context +val env_rel_context_chop : int -> env -> env * rel_context (** Set of local names *) val vars_of_env: env -> Idset.t |