diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/evarconv.ml | 22 | ||||
| -rw-r--r-- | pretyping/evarsolve.ml | 18 | ||||
| -rw-r--r-- | pretyping/evarsolve.mli | 12 | ||||
| -rw-r--r-- | pretyping/recordops.ml | 22 | ||||
| -rw-r--r-- | pretyping/recordops.mli | 3 | ||||
| -rw-r--r-- | pretyping/retyping.ml | 12 |
6 files changed, 47 insertions, 42 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index cbf539c1e9..cdf2922516 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -244,24 +244,20 @@ let check_conv_record env sigma (t1,sk1) (t2,sk2) = Prod (_,a,b) -> (* assert (l2=[]); *) let _, a, b = destProd sigma t2 in if noccurn sigma 1 b then - lookup_canonical_conversion (proji, Prod_cs), + lookup_canonical_conversion env (proji, Prod_cs), (Stack.append_app [|a;pop b|] Stack.empty) else raise Not_found | Sort s -> let s = ESorts.kind sigma s in - lookup_canonical_conversion + lookup_canonical_conversion env (proji, Sort_cs (Sorts.family s)),[] | Proj (p, c) -> - let c2 = GlobRef.ConstRef (Projection.constant p) in - let c = Retyping.expand_projection env sigma p c [] in - let _, args = destApp sigma c in - let sk2 = Stack.append_app args sk2 in - lookup_canonical_conversion (proji, Const_cs c2), sk2 + lookup_canonical_conversion env (proji, Proj_cs (Projection.repr p)), Stack.append_app [|c|] sk2 | _ -> let (c2, _) = try destRef sigma t2 with DestKO -> raise Not_found in - lookup_canonical_conversion (proji, Const_cs c2),sk2 + lookup_canonical_conversion env (proji, Const_cs c2),sk2 with Not_found -> - let (c, cs) = lookup_canonical_conversion (proji,Default_cs) in + let (c, cs) = lookup_canonical_conversion env (proji,Default_cs) in (c,cs),[] in let t', { o_DEF = c; o_CTX = ctx; o_INJ=n; o_TABS = bs; @@ -273,6 +269,7 @@ let check_conv_record env sigma (t1,sk1) (t2,sk2) = | Some c -> (* A primitive projection applied to c *) let ty = Retyping.get_type_of ~lax:true env sigma c in let (i,u), ind_args = + (* Are we sure that ty is not an evar? *) try Inductiveops.find_mrectype env sigma ty with _ -> raise Not_found in Stack.append_app_list ind_args Stack.empty, c, sk1 @@ -1620,12 +1617,15 @@ let apply_conversion_problem_heuristic flags env evd with_ho pbty t1 t2 = in Success (solve_refl ~can_drop:true f flags env evd (position_problem true pbty) evk1 args1 args2) - | Evar ev1, Evar ev2 when app_empty -> + | Evar (evk1,_ as ev1), Evar ev2 when app_empty -> (* solve_evar_evar handles the cases ev1 and/or ev2 are frozen *) - Success (solve_evar_evar ~force:true + (try + Success (solve_evar_evar ~force:true (evar_define evar_unify flags ~choose:true) evar_unify flags env evd (position_problem true pbty) ev1 ev2) + with IllTypedInstance (env,t,u) -> + UnifFailure (evd,InstanceNotSameType (evk1,env,t,u))) | Evar ev1,_ when is_evar_allowed flags (fst ev1) && Array.length l1 <= Array.length l2 -> (* On "?n t1 .. tn = u u1 .. u(n+p)", try first-order unification *) (* and otherwise second-order matching *) diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index c58ebe1bbd..44414aa6a0 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -227,8 +227,7 @@ let recheck_applications unify flags env evdref t = (match unify flags TypeUnification 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)) + | UnifFailure (evd, reason) -> raise (IllTypedInstance (env, ty, argsty.(i)))) | _ -> raise (IllTypedInstance (env, ty, argsty.(i))) else () in aux 0 fty @@ -936,13 +935,6 @@ let project_with_effects aliases sigma t subst = in filter_solution (Int.Map.fold is_projectable subst []) -open Context.Named.Declaration -let rec find_solution_type evarenv = function - | (id,ProjectVar)::l -> get_type (lookup_named id evarenv) - | [id,ProjectEvar _] -> (* bugged *) get_type (lookup_named id evarenv) - | (id,ProjectEvar _)::l -> find_solution_type evarenv l - | [] -> 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 @@ -1553,10 +1545,10 @@ let rec invert_definition unify flags choose imitate_defs raise (NotEnoughInformationToProgress sols); (* No unique projection but still restrict to where it is possible *) (* materializing is necessary, but is restricting useful? *) - let ty = find_solution_type (evar_filtered_env env evi) sols in - let ty' = instantiate_evar_array evi ty argsv in + let t' = of_alias t in + let ty = Retyping.get_type_of env !evdref t' in let (evd,evar,(evk',argsv' as ev')) = - materialize_evar (evar_define unify flags ~choose) env !evdref 0 ev ty' in + materialize_evar (evar_define unify flags ~choose) env !evdref 0 ev ty in let ts = expansions_of_var evd aliases t in let test c = isEvar evd c || List.exists (is_alias evd c) ts in let filter = restrict_upon_filter evd evk test argsv' in @@ -1565,7 +1557,7 @@ let rec invert_definition unify flags choose imitate_defs let evd = match candidates with | NoUpdate -> let evd, ev'' = restrict_applied_evar evd ev' filter NoUpdate in - add_conv_oriented_pb ~tail:false (None,env,mkEvar ev'',of_alias t) evd + add_conv_oriented_pb ~tail:false (None,env,mkEvar ev'',t') evd | UpdateWith _ -> restrict_evar evd evk' filter candidates in diff --git a/pretyping/evarsolve.mli b/pretyping/evarsolve.mli index 8ff2d7fc63..094dae4828 100644 --- a/pretyping/evarsolve.mli +++ b/pretyping/evarsolve.mli @@ -99,7 +99,9 @@ type conversion_check = unify_flags -> unification_kind -> Preconditions: - [ev] does not occur in [c]. - [c] does not contain any Meta(_) - *) + + If [ev] and [c] have non inferably convertible types, an exception + [IllTypedInstance] is raised *) val instantiate_evar : unifier -> unify_flags -> env -> evar_map -> Evar.t -> constr -> evar_map @@ -107,7 +109,9 @@ val instantiate_evar : unifier -> unify_flags -> env -> evar_map -> (** [evar_define choose env ev c] try to instantiate [ev] with [c] (typed in [env]), possibly solving related unification problems, possibly leaving open some problems that cannot be solved in a unique way (except if choose is - true); fails if the instance is not valid for the given [ev] *) + true); fails if the instance is not valid for the given [ev]; + If [ev] and [c] have non inferably convertible types, an exception + [IllTypedInstance] is raised *) val evar_define : unifier -> unify_flags -> ?choose:bool -> ?imitate_defs:bool -> env -> evar_map -> bool option -> existential -> constr -> evar_map @@ -129,6 +133,8 @@ val solve_evar_evar : ?force:bool -> (env -> evar_map -> bool option -> existential -> constr -> evar_map) -> unifier -> unify_flags -> env -> evar_map -> bool option -> existential -> existential -> evar_map + (** The two evars are expected to be in inferably convertible types; + if not, an exception IllTypedInstance is raised *) val solve_simple_eqn : unifier -> unify_flags -> ?choose:bool -> ?imitate_defs:bool -> env -> evar_map -> bool option * existential * constr -> unification_result @@ -147,9 +153,9 @@ val noccur_evar : env -> evar_map -> Evar.t -> constr -> bool exception IllTypedInstance of env * types * types -(* May raise IllTypedInstance if types are not convertible *) val check_evar_instance : unifier -> unify_flags -> env -> evar_map -> Evar.t -> constr -> evar_map + (** May raise IllTypedInstance if types are not convertible *) val remove_instance_local_defs : evar_map -> Evar.t -> 'a list -> 'a list diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index e6e5ad8dd4..b6e44265ae 100644 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -144,19 +144,21 @@ type obj_typ = { type cs_pattern = Const_cs of GlobRef.t + | Proj_cs of Projection.Repr.t | Prod_cs | Sort_cs of Sorts.family | Default_cs -let eq_cs_pattern p1 p2 = match p1, p2 with -| Const_cs gr1, Const_cs gr2 -> GlobRef.equal gr1 gr2 +let eq_cs_pattern env p1 p2 = match p1, p2 with +| Const_cs gr1, Const_cs gr2 -> Environ.QGlobRef.equal env gr1 gr2 +| Proj_cs p1, Proj_cs p2 -> Environ.QProjection.Repr.equal env p1 p2 | Prod_cs, Prod_cs -> true | Sort_cs s1, Sort_cs s2 -> Sorts.family_equal s1 s2 | Default_cs, Default_cs -> true | _ -> false -let rec assoc_pat a = function - | ((pat, t), e) :: xs -> if eq_cs_pattern pat a then (t, e) else assoc_pat a xs +let rec assoc_pat env a = function + | ((pat, t), e) :: xs -> if eq_cs_pattern env pat a then (t, e) else assoc_pat env a xs | [] -> raise Not_found @@ -179,10 +181,7 @@ let rec cs_pattern_of_constr env t = patt, n, args @ Array.to_list vargs | Rel n -> Default_cs, Some n, [] | Prod (_,a,b) when Vars.noccurn 1 b -> Prod_cs, None, [a; Vars.lift (-1) b] - | Proj (p, c) -> - let ty = Retyping.get_type_of_constr env c in - let _, params = Inductive.find_rectype env ty in - Const_cs (GlobRef.ConstRef (Projection.constant p)), None, params @ [c] + | Proj (p, c) -> Proj_cs (Projection.repr p), None, [c] | Sort s -> Sort_cs (Sorts.family s), None, [] | _ -> Const_cs (fst @@ destRef t) , None, [] @@ -238,6 +237,7 @@ let compute_canonical_projections env ~warn (gref,ind) = let pr_cs_pattern = function Const_cs c -> Nametab.pr_global_env Id.Set.empty c + | Proj_cs p -> Nametab.pr_global_env Id.Set.empty (GlobRef.ConstRef (Projection.Repr.constant p)) | Prod_cs -> str "_ -> _" | Default_cs -> str "_" | Sort_cs s -> Sorts.pr_sort_family s @@ -253,7 +253,7 @@ let register_canonical_structure ~warn env sigma o = compute_canonical_projections env ~warn o |> List.iter (fun ((proj, (cs_pat, _ as pat)), s) -> let l = try GlobRef.Map.find proj !object_table with Not_found -> [] in - match assoc_pat cs_pat l with + match assoc_pat env cs_pat l with | exception Not_found -> object_table := GlobRef.Map.add proj ((pat, s) :: l) !object_table | _, cs -> @@ -320,8 +320,8 @@ let check_and_decompose_canonical_structure env sigma ref = error_not_structure ref (str "Got too few arguments to the record or structure constructor."); (ref,indsp) -let lookup_canonical_conversion (proj,pat) = - assoc_pat pat (GlobRef.Map.find proj !object_table) +let lookup_canonical_conversion env (proj,pat) = + assoc_pat env pat (GlobRef.Map.find proj !object_table) let decompose_projection sigma c args = match EConstr.kind sigma c with diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli index 3be60d5e62..5b8dc8184a 100644 --- a/pretyping/recordops.mli +++ b/pretyping/recordops.mli @@ -67,6 +67,7 @@ val find_primitive_projection : Constant.t -> Projection.Repr.t option (** A cs_pattern characterizes the form of a component of canonical structure *) type cs_pattern = Const_cs of GlobRef.t + | Proj_cs of Projection.Repr.t | Prod_cs | Sort_cs of Sorts.family | Default_cs @@ -88,7 +89,7 @@ val pr_cs_pattern : cs_pattern -> Pp.t type cs = GlobRef.t * inductive -val lookup_canonical_conversion : (GlobRef.t * cs_pattern) -> constr * obj_typ +val lookup_canonical_conversion : Environ.env -> (GlobRef.t * cs_pattern) -> constr * obj_typ val register_canonical_structure : warn:bool -> Environ.env -> Evd.evar_map -> cs -> unit val subst_canonical_structure : Mod_subst.substitution -> cs -> cs diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index 4bd22e76cb..34bcd0982c 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -67,6 +67,14 @@ let get_type_from_constraints env sigma t = | _ -> raise Not_found else raise Not_found +let sort_of_arity_with_constraints env sigma t = + try Reductionops.sort_of_arity env sigma t + with Reduction.NotArity -> + try + let t = get_type_from_constraints env sigma t in + Reductionops.sort_of_arity env sigma t + with Not_found | Reduction.NotArity -> retype_error NotAnArity + let rec subst_type env sigma typ = function | [] -> typ | h::rest -> @@ -187,9 +195,7 @@ let retype ?(polyprop=true) sigma = let mip = lookup_mind_specif env ind in let paramtyps = Array.map_to_list (fun arg () -> let t = type_of env arg in - let s = try Reductionops.sort_of_arity env sigma t - with Reduction.NotArity -> retype_error NotAnArity - in + let s = sort_of_arity_with_constraints env sigma t in Sorts.univ_of_sort (ESorts.kind sigma s)) args in |