summaryrefslogtreecommitdiff
path: root/pretyping/evarsolve.ml
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <gareuselesinge@debian.org>2015-11-13 11:31:34 +0100
committerGravatar Enrico Tassi <gareuselesinge@debian.org>2015-11-13 11:31:34 +0100
commit2280477a96e19ba5060de2d48dcc8fd7c8079d22 (patch)
tree074182834cb406d1304aec4233718564a9c06ba1 /pretyping/evarsolve.ml
parent0aa2544d04dbd4b6ee665b551ed165e4fb02d2fa (diff)
Imported Upstream version 8.5~beta3+dfsg
Diffstat (limited to 'pretyping/evarsolve.ml')
-rw-r--r--pretyping/evarsolve.ml111
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