diff options
Diffstat (limited to 'pretyping/evarsolve.ml')
| -rw-r--r-- | pretyping/evarsolve.ml | 147 |
1 files changed, 64 insertions, 83 deletions
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index d0721439..2dd37219 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -69,7 +69,7 @@ let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) ?(refreshset=false) if onlyalg && alg then (evdref := Evd.make_flexible_variable !evdref ~algebraic:false l; t) else t)) - | Prop Pos when refreshset && not direction -> + | Set when refreshset && not direction -> (* Cannot make a universe "lower" than "Set", only refreshing when we want higher universes. *) refresh_sort status ~direction s @@ -89,9 +89,9 @@ let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) ?(refreshset=false) Array.iter (refresh_term_evars onevars false) args | Evar (ev, a) when onevars -> let evi = Evd.find !evdref ev in - let ty' = refresh ~onlyalg univ_flexible ~direction:true (EConstr.of_constr evi.evar_concl) in + let ty' = refresh ~onlyalg univ_flexible ~direction:true evi.evar_concl in if !modified then - evdref := Evd.add !evdref ev {evi with evar_concl = EConstr.Unsafe.to_constr ty'} + evdref := Evd.add !evdref ev {evi with evar_concl = ty'} else () | _ -> EConstr.iter !evdref (refresh_term_evars onevars false) t and refresh_polymorphic_positions args pos = @@ -137,8 +137,6 @@ let test_success conv_algo env evd c c' rhs = is_success (conv_algo env evd c c' rhs) let add_conv_oriented_pb ?(tail=true) (pbty,env,t1,t2) evd = - let t1 = EConstr.Unsafe.to_constr t1 in - let t2 = EConstr.Unsafe.to_constr t2 in match pbty with | Some true -> add_conv_pb ~tail (Reduction.CUMUL,env,t1,t2) evd | Some false -> add_conv_pb ~tail (Reduction.CUMUL,env,t2,t1) evd @@ -197,7 +195,7 @@ let restrict_evar_key evd evk filter candidates = | None -> evar_filter evi | Some filter -> filter in let candidates = match candidates with - | NoUpdate -> Option.map (fun l -> List.map EConstr.of_constr l) evi.evar_candidates + | NoUpdate -> evi.evar_candidates | UpdateWith c -> Some c in restrict_evar evd evk filter candidates end @@ -527,7 +525,7 @@ let is_unification_pattern_meta env evd nb m l t = match Option.List.map map l with | Some l -> begin match find_unification_pattern_args env evd l t with - | Some _ as x when not (dependent evd (mkMeta m) t) -> x + | Some _ as x when not (occur_metavariable evd m t) -> x | _ -> None end | None -> @@ -600,13 +598,13 @@ let solve_pattern_eqn env sigma l c = let make_projectable_subst aliases sigma evi args = let sign = evar_filtered_context evi in - let sign = List.map (fun d -> map_named_decl EConstr.of_constr d) sign in let evar_aliases = compute_var_aliases sign sigma in - let (_,full_subst,cstr_subst) = - List.fold_right - (fun decl (args,all,cstrs) -> + let (_,full_subst,cstr_subst,_) = + List.fold_right_i + (fun i decl (args,all,cstrs,revmap) -> match decl,args with | LocalAssum (id,c), a::rest -> + let revmap = Id.Map.add id i revmap in let cstrs = let a',args = decompose_app_vect sigma a in match EConstr.kind sigma a' with @@ -614,22 +612,26 @@ let make_projectable_subst aliases sigma evi args = let l = try Constrmap.find (fst cstr) cstrs with Not_found -> [] in Constrmap.add (fst cstr) ((args,id)::l) cstrs | _ -> cstrs in - (rest,Id.Map.add id [a,normalize_alias_opt sigma aliases a,id] all,cstrs) + let all = Int.Map.add i [a,normalize_alias_opt sigma aliases a,id] all in + (rest,all,cstrs,revmap) | LocalDef (id,c,_), a::rest -> + let revmap = Id.Map.add id i revmap in (match EConstr.kind sigma c with | Var id' -> let idc = normalize_alias_var sigma evar_aliases id' in - let sub = try Id.Map.find idc all with Not_found -> [] in + let ic, sub = + try let ic = Id.Map.find idc revmap in ic, Int.Map.find ic all + with Not_found -> i, [] (* e.g. [idc] is a filtered variable: treat [id] as an assumption *) in if List.exists (fun (c,_,_) -> EConstr.eq_constr sigma a c) sub then - (rest,all,cstrs) + (rest,all,cstrs,revmap) else - (rest, - Id.Map.add idc ((a,normalize_alias_opt sigma aliases a,id)::sub) all, - cstrs) + let all = Int.Map.add ic ((a,normalize_alias_opt sigma aliases a,id)::sub) all in + (rest,all,cstrs,revmap) | _ -> - (rest,Id.Map.add id [a,normalize_alias_opt sigma aliases a,id] all,cstrs)) - | _ -> anomaly (Pp.str "Instance does not match its signature.")) - sign (Array.rev_to_list args,Id.Map.empty,Constrmap.empty) in + let all = Int.Map.add i [a,normalize_alias_opt sigma aliases a,id] all in + (rest,all,cstrs,revmap)) + | _ -> anomaly (Pp.str "Instance does not match its signature.")) 0 + sign (Array.rev_to_list args,Int.Map.empty,Constrmap.empty,Id.Map.empty) in (full_subst,cstr_subst) (*------------------------------------* @@ -796,11 +798,11 @@ let rec assoc_up_to_alias sigma aliases y yc = function let rec find_projectable_vars with_evars aliases sigma y subst = let yc = normalize_alias sigma aliases y in - let is_projectable idc idcl subst' = + let is_projectable idc idcl (subst1,subst2 as subst') = (* First test if some [id] aliased to [idc] is bound to [y] in [subst] *) try let id = assoc_up_to_alias sigma aliases y yc idcl in - (id,ProjectVar)::subst' + (id,ProjectVar)::subst1,subst2 with Not_found -> (* Then test if [idc] is (indirectly) bound in [subst] to some evar *) (* projectable on [y] *) @@ -815,14 +817,18 @@ let rec find_projectable_vars with_evars aliases sigma y subst = 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' + | [id',p] -> (subst1,(id,ProjectEvar (t,evi,id',p))::subst2) | _ -> subst' end | [] -> subst' | _ -> anomaly (Pp.str "More than one non var in aliases class of evar instance.") else subst' in - Id.Map.fold is_projectable subst [] + let subst1,subst2 = Int.Map.fold is_projectable subst ([],[]) in + (* We return the substitution with ProjectVar first (from most + recent to oldest var), followed by ProjectEvar (from most recent + to oldest var too) *) + subst1 @ subst2 (* [filter_solution] checks if one and only one possible projection exists * among a set of solutions to a projection problem *) @@ -845,25 +851,6 @@ let rec find_solution_type evarenv = function | (id,ProjectEvar _)::l -> find_solution_type evarenv l | [] -> assert false -let is_preferred_projection_over sign (id,p) (id',p') = - (* We give priority to projection of variables over instantiation of - an evar considering that the latter is a stronger decision which - may even procude an incorrect (ill-typed) solution *) - match p, p' with - | ProjectEvar _, ProjectVar -> false - | ProjectVar, ProjectEvar _ -> true - | _, _ -> - List.index Id.equal id sign < List.index Id.equal id' sign - -let choose_projection evi sols = - let sign = List.map get_id (evar_filtered_context evi) in - match sols with - | y::l -> - List.fold_right (fun (id,p as x) (id',_ as y) -> - if is_preferred_projection_over sign x y then x else y) - l y - | _ -> assert false - (* In case the solution to a projection problem requires the instantiation of * subsidiary evars, [do_projection_effects] performs them; it * also try to instantiate the type of those subsidiary evars if their @@ -877,7 +864,7 @@ let choose_projection evi sols = let rec do_projection_effects define_fun env ty evd = function | ProjectVar -> evd | ProjectEvar ((evk,argsv),evi,id,p) -> - let evd = Evd.define evk (Constr.mkVar id) evd in + let evd = Evd.define evk (mkVar id) evd in (* TODO: simplify constraints involving evk *) let evd = do_projection_effects define_fun env ty evd p in let ty = whd_all env evd (Lazy.force ty) in @@ -887,7 +874,7 @@ let rec do_projection_effects define_fun env ty evd = function one (however, regarding coercions, because t is obtained by unif, we know that no coercion can be inserted) *) let subst = make_pure_subst evi argsv in - let ty' = replace_vars subst (EConstr.of_constr evi.evar_concl) in + let ty' = replace_vars subst evi.evar_concl in if isEvar evd ty' then define_fun env evd (Some false) (destEvar evd ty') ty else evd else evd @@ -1004,7 +991,7 @@ let filter_effective_candidates evd evi filter candidates = let filter_candidates evd evk filter candidates_update = let evi = Evd.find_undefined evd evk in let candidates = match candidates_update with - | NoUpdate -> Option.map (fun l -> List.map EConstr.of_constr l) evi.evar_candidates + | NoUpdate -> evi.evar_candidates | UpdateWith c -> Some c in match candidates with @@ -1023,13 +1010,12 @@ let closure_of_filter evd evk = function | None -> None | Some filter -> let evi = Evd.find_undefined evd evk in - let vars = collect_vars evd (EConstr.of_constr (evar_concl evi)) in + let vars = collect_vars evd (evar_concl evi) in let test b decl = b || Id.Set.mem (get_id decl) vars || match decl with | LocalAssum _ -> false | LocalDef (_,c,_) -> - let c = EConstr.of_constr c in not (isRel evd c || isVar evd c) in let newfilter = Filter.map_along test filter (evar_context evi) in @@ -1062,7 +1048,7 @@ let do_restrict_hyps evd (evk,args as ev) filter candidates = match candidates,filter with | UpdateWith [], _ -> user_err Pp.(str "Not solvable.") | UpdateWith [nc],_ -> - let evd = Evd.define evk (EConstr.Unsafe.to_constr nc) evd in + let evd = Evd.define evk nc evd in raise (EvarSolvedWhileRestricting (evd,mkEvar ev)) | NoUpdate, None -> evd,ev | _ -> restrict_applied_evar evd ev filter candidates @@ -1072,8 +1058,14 @@ let do_restrict_hyps evd (evk,args as ev) filter candidates = let postpone_non_unique_projection env evd pbty (evk,argsv as ev) sols rhs = let rhs = expand_vars_in_term env evd rhs in - let filter = - restrict_upon_filter evd evk + let filter a = match EConstr.kind evd a with + | Rel n -> not (noccurn evd n rhs) + | Var id -> + local_occur_var evd id rhs + || List.exists (fun (id', _) -> Id.equal id id') sols + | _ -> true + in + let filter = restrict_upon_filter evd evk filter argsv in (* 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 *) @@ -1081,9 +1073,6 @@ let postpone_non_unique_projection env evd pbty (evk,argsv as ev) sols rhs = (* 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 evd a || isVar evd a) - || dependent evd a rhs || List.exists (fun (id,_) -> isVarId evd id a) sols) - argsv in let filter = closure_of_filter evd evk filter in let candidates = extract_candidates sols in match candidates with @@ -1113,9 +1102,6 @@ let postpone_non_unique_projection env evd pbty (evk,argsv as ev) sols rhs = * Note: argument f is the function used to instantiate evars. *) -let instantiate_evar_array evi c args = - EConstr.of_constr (instantiate_evar_array evi (EConstr.Unsafe.to_constr c) (Array.map EConstr.Unsafe.to_constr args)) - let filter_compatible_candidates conv_algo env evd evi args rhs c = let c' = instantiate_evar_array evi c args in match conv_algo env evd Reduction.CONV rhs c' with @@ -1135,8 +1121,6 @@ let restrict_candidates conv_algo env evd filter1 (evk1,argsv1) (evk2,argsv2) = | _, None -> filter_candidates evd evk1 filter1 NoUpdate | None, Some _ -> raise DoesNotPreserveCandidateRestriction | Some l1, Some l2 -> - let l1 = List.map EConstr.of_constr l1 in - let l2 = List.map EConstr.of_constr l2 in let l1 = filter_effective_candidates evd evi1 filter1 l1 in let l1' = List.filter (fun c1 -> let c1' = instantiate_evar_array evi1 c1 argsv1 in @@ -1242,9 +1226,9 @@ let check_evar_instance evd evk1 body conv_algo = try Retyping.get_type_of ~lax:true evenv evd body with Retyping.RetypeError _ -> user_err Pp.(str "Ill-typed evar instance") in - match conv_algo evenv evd Reduction.CUMUL ty (EConstr.of_constr evi.evar_concl) with + match conv_algo evenv evd Reduction.CUMUL ty evi.evar_concl with | Success evd -> evd - | UnifFailure _ -> raise (IllTypedInstance (evenv,ty,EConstr.of_constr evi.evar_concl)) + | UnifFailure _ -> raise (IllTypedInstance (evenv,ty, evi.evar_concl)) let update_evar_source ev1 ev2 evd = let loc, evs2 = evar_source ev2 evd in @@ -1257,7 +1241,7 @@ let update_evar_source ev1 ev2 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 (EConstr.Unsafe.to_constr body) evd in + let evd' = Evd.define evk2 body evd in let evd' = update_evar_source (fst (destEvar evd body)) evk2 evd' in check_evar_instance evd' evk2 body g with EvarSolvedOnTheFly (evd,c) -> @@ -1292,17 +1276,19 @@ let solve_evar_evar_aux force f g env evd pbty (evk1,args1 as ev1) (evk2,args2 a let solve_evar_evar ?(force=false) f g env evd pbty (evk1,args1 as ev1) (evk2,args2 as ev2) = let pbty = if force then None else pbty in let evi = Evd.find evd evk1 in - let downcast evk t evd = downcast evk (EConstr.Unsafe.to_constr t) evd in + let downcast evk t evd = downcast evk t evd in let evd = try (* ?X : Π Δ. Type i = ?Y : Π Δ'. Type j. The body of ?X and ?Y just has to be of type Π Δ. Type k for some k <= i, j. *) let evienv = Evd.evar_env evi in - let ctx1, i = Reduction.dest_arity evienv evi.evar_concl in + let concl1 = EConstr.Unsafe.to_constr evi.evar_concl in + let ctx1, i = Reduction.dest_arity evienv concl1 in let ctx1 = List.map (fun c -> map_rel_decl EConstr.of_constr c) ctx1 in let evi2 = Evd.find evd evk2 in let evi2env = Evd.evar_env evi2 in - let ctx2, j = Reduction.dest_arity evi2env evi2.evar_concl in + let concl2 = EConstr.Unsafe.to_constr evi2.evar_concl in + let ctx2, j = Reduction.dest_arity evi2env concl2 in let ctx2 = List.map (fun c -> map_rel_decl EConstr.of_constr c) ctx2 in let ui, uj = univ_of_sort i, univ_of_sort j in if i == j || Evd.check_eq evd ui uj @@ -1375,14 +1361,14 @@ let solve_candidates conv_algo env evd (evk,argsv) rhs = | Some l -> let l' = List.map_filter - (fun c -> filter_compatible_candidates conv_algo env evd evi argsv rhs (EConstr.of_constr c)) l in + (fun c -> filter_compatible_candidates conv_algo env evd evi argsv rhs c) l in match l' with | [] -> raise IncompatibleCandidates | [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 - let evd' = Evd.define evk (EConstr.Unsafe.to_constr c) evd in + 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' -> @@ -1401,8 +1387,8 @@ let occur_evar_upto_types sigma n c = Array.iter occur_rec args else ( seen := Evar.Set.add sp !seen; - Option.iter occur_rec (existential_opt_value sigma e); - occur_rec (Evd.existential_type sigma e)) + Option.iter occur_rec (existential_opt_value0 sigma e); + occur_rec (Evd.existential_type0 sigma e)) | _ -> Constr.iter occur_rec c in try occur_rec c; false with Occur -> true @@ -1451,12 +1437,8 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs = let c, p = match sols with | [] -> raise Not_found | [id,p] -> (mkVar id, p) - | _ -> - if choose then - let (id,p) = choose_projection evi sols in - (mkVar id, p) - else - raise (NotUniqueInType sols) + | (id,p)::_ -> + if choose then (mkVar id, p) else raise (NotUniqueInType sols) in let ty = lazy (Retyping.get_type_of env !evdref (of_alias t)) in let evd = do_projection_effects (evar_define conv_algo ~choose) env ty !evdref p in @@ -1529,7 +1511,7 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs = (* Try to project (a restriction of) the left evar ... *) try let evd,body = project_evar_on_evar false conv_algo env' evd aliases 0 None ev'' ev' in - let evd = Evd.define evk' (EConstr.Unsafe.to_constr body) evd in + let evd = Evd.define evk' body evd in check_evar_instance evd evk' body conv_algo with | EvarSolvedOnTheFly _ -> assert false (* ev has no candidates *) @@ -1560,7 +1542,8 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs = let t = map_constr_with_full_binders !evdref (fun d (env,k) -> push_rel d env, k+1) imitate envk t in - t::l + (* Less dependent solutions come last *) + l@[t] with e when CErrors.noncritical e -> l in (match candidates with | [x] -> x @@ -1592,14 +1575,14 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs = Id.Set.subset (collect_vars evd rhs) !names in let body = - if fast rhs then EConstr.of_constr (EConstr.to_constr evd rhs) (** FIXME? *) + if fast rhs then nf_evar evd rhs (** FIXME? *) 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 @@ -1644,7 +1627,7 @@ and evar_define conv_algo ?(choose=false) env evd pbty (evk,argsv as ev) rhs = print_constr body); raise e in*) let evd' = check_evar_instance evd' evk body conv_algo in - Evd.define evk (EConstr.Unsafe.to_constr body) evd' + Evd.define evk body evd' with | NotEnoughInformationToProgress sols -> postpone_non_unique_projection env evd pbty ev sols rhs @@ -1691,8 +1674,6 @@ and evar_define conv_algo ?(choose=false) env evd pbty (evk,argsv as ev) rhs = *) let status_changed evd lev (pbty,_,t1,t2) = - let t1 = EConstr.of_constr t1 in - let t2 = EConstr.of_constr t2 in (try Evar.Set.mem (head_evar evd t1) lev with NoHeadEvar -> false) || (try Evar.Set.mem (head_evar evd t2) lev with NoHeadEvar -> false) @@ -1702,7 +1683,7 @@ let reconsider_unif_constraints conv_algo evd = (fun p (pbty,env,t1,t2 as x) -> match p with | Success evd -> - (match conv_algo env evd pbty (EConstr.of_constr t1) (EConstr.of_constr t2) with + (match conv_algo env evd pbty t1 t2 with | Success _ as x -> x | UnifFailure (i,e) -> UnifFailure (i,CannotSolveConstraint (x,e))) | UnifFailure _ as x -> x) |