diff options
Diffstat (limited to 'pretyping/evarsolve.ml')
| -rw-r--r-- | pretyping/evarsolve.ml | 111 |
1 files changed, 85 insertions, 26 deletions
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index bfd19c6c..35bc1de5 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -42,21 +42,20 @@ let get_polymorphic_positions f = templ.template_param_levels) | _ -> assert false -(** - forall A (l : list A) -> typeof A = Type i <= Datatypes.j -> i not refreshed - hd ?A (l : list t) -> A = t +let refresh_level evd s = + match Evd.is_sort_variable evd s with + | None -> true + | Some l -> not (Evd.is_flexible_level evd l) -*) let refresh_universes ?(inferred=false) ?(onlyalg=false) pbty env evd t = let evdref = ref evd in let modified = ref false in - let rec refresh dir t = + let rec refresh status dir t = match kind_of_term t with | Sort (Type u as s) when (match Univ.universe_level u with - | None -> true - | Some l -> not onlyalg && Option.is_empty (Evd.is_sort_variable evd s)) -> - let status = if inferred then Evd.univ_flexible_alg else Evd.univ_flexible in + | None -> true + | Some l -> not onlyalg && refresh_level evd s) -> let s' = evd_comb0 (new_sort_variable status) evdref in let evd = if dir then set_leq_sort env !evdref s' s @@ -64,11 +63,11 @@ let refresh_universes ?(inferred=false) ?(onlyalg=false) pbty env evd t = in modified := true; evdref := evd; mkSort s' | Prod (na,u,v) -> - mkProd (na,u,refresh dir v) + mkProd (na,u,refresh status dir v) | _ -> t (** Refresh the types of evars under template polymorphic references *) and refresh_term_evars onevars top t = - match kind_of_term t with + match kind_of_term (whd_evar !evdref t) with | App (f, args) when is_template_polymorphic env f -> let pos = get_polymorphic_positions f in refresh_polymorphic_positions args pos @@ -77,7 +76,7 @@ let refresh_universes ?(inferred=false) ?(onlyalg=false) pbty env evd t = Array.iter (refresh_term_evars onevars false) args | Evar (ev, a) when onevars -> let evi = Evd.find !evdref ev in - let ty' = refresh true evi.evar_concl in + let ty' = refresh univ_flexible true evi.evar_concl in if !modified then evdref := Evd.add !evdref ev {evi with evar_concl = ty'} else () @@ -99,7 +98,7 @@ let refresh_universes ?(inferred=false) ?(onlyalg=false) pbty env evd t = if isArity t then (match pbty with | None -> t - | Some dir -> refresh dir t) + | Some dir -> refresh univ_rigid dir t) else (refresh_term_evars false true t; t) in if !modified then !evdref, t' else !evdref, t @@ -107,6 +106,7 @@ let refresh_universes ?(inferred=false) ?(onlyalg=false) pbty env evd t = let get_type_of_refresh ?(polyprop=true) ?(lax=false) env sigma c = let ty = Retyping.get_type_of ~polyprop ~lax env sigma c in refresh_universes (Some false) env sigma ty + (************************) (* Unification results *) @@ -127,6 +127,34 @@ let add_conv_oriented_pb ?(tail=true) (pbty,env,t1,t2) evd = | Some false -> add_conv_pb ~tail (Reduction.CUMUL,env,t2,t1) evd | None -> add_conv_pb ~tail (Reduction.CONV,env,t1,t2) evd +(* We retype applications to ensure the universe constraints are collected *) + +exception IllTypedInstance of env * types * types + +let recheck_applications conv_algo env evdref t = + let rec aux env t = + match kind_of_term t with + | App (f, args) -> + let () = aux env f in + let fty = Retyping.get_type_of env !evdref f in + let argsty = Array.map (fun x -> aux env x; Retyping.get_type_of env !evdref x) args in + let rec aux i ty = + if i < Array.length argsty then + match kind_of_term (whd_betadeltaiota env !evdref ty) with + | Prod (na, dom, codom) -> + (match conv_algo env !evdref Reduction.CUMUL argsty.(i) dom with + | Success evd -> evdref := evd; + aux (succ i) (subst1 args.(i) codom) + | UnifFailure (evd, reason) -> + Pretype_errors.error_cannot_unify env evd ~reason (argsty.(i), dom)) + | _ -> raise (IllTypedInstance (env, ty, argsty.(i))) + else () + in aux 0 fty + | _ -> + iter_constr_with_full_binders (fun d env -> push_rel d env) aux env t + in aux env t + + (*------------------------------------* * Restricting existing evars * *------------------------------------*) @@ -157,6 +185,7 @@ let restrict_evar_key evd evk filter candidates = end (* Restrict an applied evar and returns its restriction in the same context *) +(* (the filter is assumed to be at least stronger than the original one) *) 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 @@ -693,7 +722,8 @@ let rec find_projectable_vars with_evars aliases sigma y subst = (* Then test if [idc] is (indirectly) bound in [subst] to some evar *) (* projectable on [y] *) if with_evars then - let idcl' = List.filter (fun (c,_,id) -> isEvar c) idcl in + let f (c,_,id) = isEvar c && is_undefined sigma (fst (destEvar c)) in + let idcl' = List.filter f idcl in match idcl' with | [c,_,id] -> begin @@ -885,6 +915,9 @@ let filter_candidates evd evk filter candidates_update = else UpdateWith l' +(* Given a filter refinement for the evar [evk], restrict it so that + dependencies are preserved *) + let closure_of_filter evd evk = function | None -> None | Some filter -> @@ -892,8 +925,11 @@ let closure_of_filter evd evk = function let vars = collect_vars (Evarutil.nf_evar evd (evar_concl evi)) in let test b (id,c,_) = b || Idset.mem id vars || match c with None -> false | Some c -> not (isRel c || isVar c) in let newfilter = Filter.map_along test filter (evar_context evi) in + (* Now ensure that restriction is at least what is was originally *) + let newfilter = Option.cata (Filter.map_along (&&) newfilter) newfilter (Filter.repr (evar_filter evi)) in if Filter.equal newfilter (evar_filter evi) then None else Some newfilter +(* The filter is assumed to be at least stronger than the original one *) 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. @@ -1099,8 +1135,6 @@ let project_evar_on_evar force g env evd aliases k2 pbty (evk1,argsv1 as ev1) (e else raise (CannotProject (evd,ev1')) -exception IllTypedInstance of env * types * types - let check_evar_instance evd evk1 body conv_algo = let evi = Evd.find evd evk1 in let evenv = evar_env evi in @@ -1114,10 +1148,19 @@ let check_evar_instance evd evk1 body conv_algo = | Success evd -> evd | UnifFailure _ -> raise (IllTypedInstance (evenv,ty,evi.evar_concl)) +let update_evar_source ev1 ev2 evd = + let loc, evs2 = evar_source ev2 evd in + match evs2 with + | (Evar_kinds.QuestionMark _ | Evar_kinds.ImplicitArg (_, _, false)) -> + let evi = Evd.find evd ev1 in + Evd.add evd ev1 {evi with evar_source = loc, evs2} + | _ -> evd + let solve_evar_evar_l2r force f g env evd aliases pbty ev1 (evk2,_ as ev2) = try let evd,body = project_evar_on_evar force g env evd aliases 0 pbty ev1 ev2 in let evd' = Evd.define evk2 body evd in + let evd' = update_evar_source (fst (destEvar body)) evk2 evd' in check_evar_instance evd' evk2 body g with EvarSolvedOnTheFly (evd,c) -> f env evd pbty ev2 c @@ -1129,8 +1172,8 @@ let preferred_orientation evd evk1 evk2 = let _,src2 = (Evd.find_undefined evd evk2).evar_source in (* This is a heuristic useful for program to work *) match src1,src2 with - | Evar_kinds.QuestionMark _, _ -> true - | _,Evar_kinds.QuestionMark _ -> false + | (Evar_kinds.QuestionMark _ | Evar_kinds.ImplicitArg (_, _, false)) , _ -> true + | _, (Evar_kinds.QuestionMark _ | Evar_kinds.ImplicitArg (_, _, false)) -> false | _ -> true let solve_evar_evar_aux force f g env evd pbty (evk1,args1 as ev1) (evk2,args2 as ev2) = @@ -1231,12 +1274,24 @@ let solve_candidates conv_algo env evd (evk,argsv) 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 + if Evd.is_undefined evd evk then + let evd' = Evd.define evk c evd in + check_evar_instance evd' evk c conv_algo + else evd | l when List.length l < List.length l' -> let candidates = List.map fst l in restrict_evar evd evk None (UpdateWith candidates) | l -> evd +let occur_evar_upto_types sigma n c = + let rec occur_rec c = match kind_of_term c with + | Evar (sp,_) when Evar.equal sp n -> raise Occur + | Evar e -> Option.iter occur_rec (existential_opt_value sigma e); + occur_rec (existential_type sigma e) + | _ -> iter_constr occur_rec c + in + try occur_rec c; false with Occur -> true + (* We try to instantiate the evar assuming the body won't depend * on arguments that are not Rels or Vars, or appearing several times * (i.e. we tackle a generalization of Miller-Pfenning patterns unification) @@ -1396,10 +1451,10 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs = evdref := restrict_evar evd (fst ev'') None (UpdateWith 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 - + (* 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 fast rhs = let filter_ctxt = evar_filtered_context evi in @@ -1418,9 +1473,13 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs = in let body = if fast rhs then nf_evar evd rhs - else imitate (env,0) rhs - in (!evdref,body) - + else + let t' = imitate (env,0) rhs in + if !progress then + (recheck_applications conv_algo (evar_env evi) evdref t'; t') + else t' + in (!evdref,body) + (* [define] tries to solve the problem "?ev[args] = rhs" when "?ev" is * an (uninstantiated) evar such that "hyps |- ?ev : typ". Otherwise said, * [define] tries to find an instance lhs such that @@ -1445,7 +1504,7 @@ and evar_define conv_algo ?(choose=false) env evd pbty (evk,argsv as ev) rhs = if occur_meta body then raise MetaOccurInBodyInternal; (* invert_definition may have instantiate some evars of rhs with evk *) (* so we recheck acyclicity *) - if occur_evar evk body then raise (OccurCheckIn (evd',body)); + if occur_evar_upto_types evd' evk body then raise (OccurCheckIn (evd',body)); (* needed only if an inferred type *) let evd', body = refresh_universes pbty env evd' body in (* Cannot strictly type instantiations since the unification algorithm |