diff options
36 files changed, 538 insertions, 326 deletions
diff --git a/engine/eConstr.ml b/engine/eConstr.ml index 0a5f1ba68..095521e25 100644 --- a/engine/eConstr.ml +++ b/engine/eConstr.ml @@ -75,6 +75,8 @@ type constr = t type existential = t pexistential type fixpoint = (t, t) pfixpoint type cofixpoint = (t, t) pcofixpoint +type unsafe_judgment = (constr, types) Environ.punsafe_judgment +type unsafe_type_judgment = types Environ.punsafe_type_judgment let mkProp = of_kind (Sort Sorts.prop) let mkSet = of_kind (Sort Sorts.set) diff --git a/engine/eConstr.mli b/engine/eConstr.mli index 03e2d4ffc..10eb064a3 100644 --- a/engine/eConstr.mli +++ b/engine/eConstr.mli @@ -20,6 +20,8 @@ type constr = t type existential = t pexistential type fixpoint = (t, t) pfixpoint type cofixpoint = (t, t) pcofixpoint +type unsafe_judgment = (constr, types) Environ.punsafe_judgment +type unsafe_type_judgment = types Environ.punsafe_type_judgment (** {5 Destructors} *) diff --git a/engine/evarutil.ml b/engine/evarutil.ml index fc193b94a..bc55ac458 100644 --- a/engine/evarutil.ml +++ b/engine/evarutil.ml @@ -96,14 +96,15 @@ let rec whd_evar sigma c = | _ -> c let rec nf_evar sigma t = Constr.map (fun t -> nf_evar sigma t) (whd_evar sigma t) +let e_nf_evar sigma t = EConstr.of_constr (nf_evar sigma (EConstr.Unsafe.to_constr t)) let j_nf_evar sigma j = - { uj_val = nf_evar sigma j.uj_val; - uj_type = nf_evar sigma j.uj_type } + { uj_val = e_nf_evar sigma j.uj_val; + uj_type = e_nf_evar sigma j.uj_type } let jl_nf_evar sigma jl = List.map (j_nf_evar sigma) jl let jv_nf_evar sigma = Array.map (j_nf_evar sigma) let tj_nf_evar sigma {utj_val=v;utj_type=t} = - {utj_val=nf_evar sigma v;utj_type=t} + {utj_val=e_nf_evar sigma v;utj_type=t} let nf_evars_universes evm = Universes.nf_evars_and_universes_opt_subst (safe_evar_value evm) diff --git a/engine/evarutil.mli b/engine/evarutil.mli index dcb9bf247..8f3c3c352 100644 --- a/engine/evarutil.mli +++ b/engine/evarutil.mli @@ -141,13 +141,13 @@ val judge_of_new_Type : 'r Sigma.t -> (unsafe_judgment, 'r) Sigma.sigma val whd_evar : evar_map -> constr -> constr val nf_evar : evar_map -> constr -> constr -val j_nf_evar : evar_map -> unsafe_judgment -> unsafe_judgment +val j_nf_evar : evar_map -> EConstr.unsafe_judgment -> EConstr.unsafe_judgment val jl_nf_evar : - evar_map -> unsafe_judgment list -> unsafe_judgment list + evar_map -> EConstr.unsafe_judgment list -> EConstr.unsafe_judgment list val jv_nf_evar : - evar_map -> unsafe_judgment array -> unsafe_judgment array + evar_map -> EConstr.unsafe_judgment array -> EConstr.unsafe_judgment array val tj_nf_evar : - evar_map -> unsafe_type_judgment -> unsafe_type_judgment + evar_map -> EConstr.unsafe_type_judgment -> EConstr.unsafe_type_judgment val nf_named_context_evar : evar_map -> Context.Named.t -> Context.Named.t val nf_rel_context_evar : evar_map -> Context.Rel.t -> Context.Rel.t diff --git a/engine/termops.ml b/engine/termops.ml index c1198e05a..83f07d2c6 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -1141,6 +1141,7 @@ let impossible_default_case = ref None let set_impossible_default_clause c = impossible_default_case := Some c let coq_unit_judge = + let make_judge c t = make_judge (EConstr.of_constr c) (EConstr.of_constr t) in let na1 = Name (Id.of_string "A") in let na2 = Name (Id.of_string "H") in fun () -> diff --git a/engine/termops.mli b/engine/termops.mli index df3fdd124..27b3ea53c 100644 --- a/engine/termops.mli +++ b/engine/termops.mli @@ -274,10 +274,10 @@ val is_template_polymorphic : env -> Evd.evar_map -> EConstr.t -> bool (** Combinators on judgments *) -val on_judgment : (types -> types) -> unsafe_judgment -> unsafe_judgment -val on_judgment_value : (types -> types) -> unsafe_judgment -> unsafe_judgment -val on_judgment_type : (types -> types) -> unsafe_judgment -> unsafe_judgment +val on_judgment : ('a -> 'b) -> ('a, 'a) punsafe_judgment -> ('b, 'b) punsafe_judgment +val on_judgment_value : ('c -> 'c) -> ('c, 't) punsafe_judgment -> ('c, 't) punsafe_judgment +val on_judgment_type : ('t -> 't) -> ('c, 't) punsafe_judgment -> ('c, 't) punsafe_judgment (** {6 Functions to deal with impossible cases } *) val set_impossible_default_clause : (unit -> (constr * types) Univ.in_universe_context_set) -> unit -val coq_unit_judge : unit -> unsafe_judgment Univ.in_universe_context_set +val coq_unit_judge : unit -> EConstr.unsafe_judgment Univ.in_universe_context_set diff --git a/kernel/environ.ml b/kernel/environ.ml index 4a543f195..5688813ad 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -469,9 +469,11 @@ let lookup_modtype mp env = (*s Judgments. *) -type unsafe_judgment = { - uj_val : constr; - uj_type : types } +type ('constr, 'types) punsafe_judgment = { + uj_val : 'constr; + uj_type : 'types } + +type unsafe_judgment = (constr, types) punsafe_judgment let make_judge v tj = { uj_val = v; @@ -480,10 +482,12 @@ let make_judge v tj = let j_val j = j.uj_val let j_type j = j.uj_type -type unsafe_type_judgment = { - utj_val : constr; +type 'types punsafe_type_judgment = { + utj_val : 'types; utj_type : sorts } +type unsafe_type_judgment = types punsafe_type_judgment + (*s Compilation of global declaration *) let compile_constant_body = Cbytegen.compile_constant_body false diff --git a/kernel/environ.mli b/kernel/environ.mli index ea570cb4a..b7431dbe5 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -238,18 +238,21 @@ val keep_hyps : env -> Id.Set.t -> Context.Named.t actually only a datatype to store a term with its type and the type of its type. *) -type unsafe_judgment = { - uj_val : constr; - uj_type : types } +type ('constr, 'types) punsafe_judgment = { + uj_val : 'constr; + uj_type : 'types } -val make_judge : constr -> types -> unsafe_judgment -val j_val : unsafe_judgment -> constr -val j_type : unsafe_judgment -> types +type unsafe_judgment = (constr, types) punsafe_judgment -type unsafe_type_judgment = { - utj_val : constr; +val make_judge : 'constr -> 'types -> ('constr, 'types) punsafe_judgment +val j_val : ('constr, 'types) punsafe_judgment -> 'constr +val j_type : ('constr, 'types) punsafe_judgment -> 'types + +type 'types punsafe_type_judgment = { + utj_val : 'types; utj_type : sorts } +type unsafe_type_judgment = types punsafe_type_judgment (** {6 Compilation of global declaration } *) diff --git a/kernel/type_errors.ml b/kernel/type_errors.ml index 5071f0ad5..5e1763815 100644 --- a/kernel/type_errors.ml +++ b/kernel/type_errors.ml @@ -13,52 +13,56 @@ open Reduction (* Type errors. *) -type guard_error = +type 'constr pguard_error = (* Fixpoints *) | NotEnoughAbstractionInFixBody - | RecursionNotOnInductiveType of constr - | RecursionOnIllegalTerm of int * (env * constr) * int list * int list + | RecursionNotOnInductiveType of 'constr + | RecursionOnIllegalTerm of int * (env * 'constr) * int list * int list | NotEnoughArgumentsForFixCall of int (* CoFixpoints *) - | CodomainNotInductiveType of constr + | CodomainNotInductiveType of 'constr | NestedRecursiveOccurrences - | UnguardedRecursiveCall of constr - | RecCallInTypeOfAbstraction of constr - | RecCallInNonRecArgOfConstructor of constr - | RecCallInTypeOfDef of constr - | RecCallInCaseFun of constr - | RecCallInCaseArg of constr - | RecCallInCasePred of constr - | NotGuardedForm of constr - | ReturnPredicateNotCoInductive of constr + | UnguardedRecursiveCall of 'constr + | RecCallInTypeOfAbstraction of 'constr + | RecCallInNonRecArgOfConstructor of 'constr + | RecCallInTypeOfDef of 'constr + | RecCallInCaseFun of 'constr + | RecCallInCaseArg of 'constr + | RecCallInCasePred of 'constr + | NotGuardedForm of 'constr + | ReturnPredicateNotCoInductive of 'constr + +type guard_error = constr pguard_error type arity_error = | NonInformativeToInformative | StrongEliminationOnNonSmallType | WrongArity -type type_error = +type ('constr, 'types) ptype_error = | UnboundRel of int | UnboundVar of variable - | NotAType of unsafe_judgment - | BadAssumption of unsafe_judgment - | ReferenceVariables of identifier * constr - | ElimArity of pinductive * sorts_family list * constr * unsafe_judgment + | NotAType of ('constr, 'types) punsafe_judgment + | BadAssumption of ('constr, 'types) punsafe_judgment + | ReferenceVariables of identifier * 'constr + | ElimArity of pinductive * sorts_family list * 'constr * ('constr, 'types) punsafe_judgment * (sorts_family * sorts_family * arity_error) option - | CaseNotInductive of unsafe_judgment + | CaseNotInductive of ('constr, 'types) punsafe_judgment | WrongCaseInfo of pinductive * case_info - | NumberBranches of unsafe_judgment * int - | IllFormedBranch of constr * pconstructor * constr * constr - | Generalization of (Name.t * types) * unsafe_judgment - | ActualType of unsafe_judgment * types + | NumberBranches of ('constr, 'types) punsafe_judgment * int + | IllFormedBranch of 'constr * pconstructor * 'constr * 'constr + | Generalization of (Name.t * 'types) * ('constr, 'types) punsafe_judgment + | ActualType of ('constr, 'types) punsafe_judgment * 'types | CantApplyBadType of - (int * constr * constr) * unsafe_judgment * unsafe_judgment array - | CantApplyNonFunctional of unsafe_judgment * unsafe_judgment array - | IllFormedRecBody of guard_error * Name.t array * int * env * unsafe_judgment array + (int * 'constr * 'constr) * ('constr, 'types) punsafe_judgment * ('constr, 'types) punsafe_judgment array + | CantApplyNonFunctional of ('constr, 'types) punsafe_judgment * ('constr, 'types) punsafe_judgment array + | IllFormedRecBody of 'constr pguard_error * Name.t array * int * env * ('constr, 'types) punsafe_judgment array | IllTypedRecBody of - int * Name.t array * unsafe_judgment array * types array + int * Name.t array * ('constr, 'types) punsafe_judgment array * 'types array | UnsatisfiedConstraints of Univ.constraints +type type_error = (constr, types) ptype_error + exception TypeError of env * type_error let nfj env {uj_val=c;uj_type=ct} = diff --git a/kernel/type_errors.mli b/kernel/type_errors.mli index 0c3a952b8..bd6032716 100644 --- a/kernel/type_errors.mli +++ b/kernel/type_errors.mli @@ -14,52 +14,56 @@ open Environ (*i Rem: NotEnoughAbstractionInFixBody should only occur with "/i" Fix notation i*) -type guard_error = +type 'constr pguard_error = (** Fixpoints *) | NotEnoughAbstractionInFixBody - | RecursionNotOnInductiveType of constr - | RecursionOnIllegalTerm of int * (env * constr) * int list * int list + | RecursionNotOnInductiveType of 'constr + | RecursionOnIllegalTerm of int * (env * 'constr) * int list * int list | NotEnoughArgumentsForFixCall of int (** CoFixpoints *) - | CodomainNotInductiveType of constr + | CodomainNotInductiveType of 'constr | NestedRecursiveOccurrences - | UnguardedRecursiveCall of constr - | RecCallInTypeOfAbstraction of constr - | RecCallInNonRecArgOfConstructor of constr - | RecCallInTypeOfDef of constr - | RecCallInCaseFun of constr - | RecCallInCaseArg of constr - | RecCallInCasePred of constr - | NotGuardedForm of constr - | ReturnPredicateNotCoInductive of constr + | UnguardedRecursiveCall of 'constr + | RecCallInTypeOfAbstraction of 'constr + | RecCallInNonRecArgOfConstructor of 'constr + | RecCallInTypeOfDef of 'constr + | RecCallInCaseFun of 'constr + | RecCallInCaseArg of 'constr + | RecCallInCasePred of 'constr + | NotGuardedForm of 'constr + | ReturnPredicateNotCoInductive of 'constr + +type guard_error = constr pguard_error type arity_error = | NonInformativeToInformative | StrongEliminationOnNonSmallType | WrongArity -type type_error = +type ('constr, 'types) ptype_error = | UnboundRel of int | UnboundVar of variable - | NotAType of unsafe_judgment - | BadAssumption of unsafe_judgment - | ReferenceVariables of identifier * constr - | ElimArity of pinductive * sorts_family list * constr * unsafe_judgment + | NotAType of ('constr, 'types) punsafe_judgment + | BadAssumption of ('constr, 'types) punsafe_judgment + | ReferenceVariables of identifier * 'constr + | ElimArity of pinductive * sorts_family list * 'constr * ('constr, 'types) punsafe_judgment * (sorts_family * sorts_family * arity_error) option - | CaseNotInductive of unsafe_judgment + | CaseNotInductive of ('constr, 'types) punsafe_judgment | WrongCaseInfo of pinductive * case_info - | NumberBranches of unsafe_judgment * int - | IllFormedBranch of constr * pconstructor * constr * constr - | Generalization of (Name.t * types) * unsafe_judgment - | ActualType of unsafe_judgment * types + | NumberBranches of ('constr, 'types) punsafe_judgment * int + | IllFormedBranch of 'constr * pconstructor * 'constr * 'constr + | Generalization of (Name.t * 'types) * ('constr, 'types) punsafe_judgment + | ActualType of ('constr, 'types) punsafe_judgment * 'types | CantApplyBadType of - (int * constr * constr) * unsafe_judgment * unsafe_judgment array - | CantApplyNonFunctional of unsafe_judgment * unsafe_judgment array - | IllFormedRecBody of guard_error * Name.t array * int * env * unsafe_judgment array + (int * 'constr * 'constr) * ('constr, 'types) punsafe_judgment * ('constr, 'types) punsafe_judgment array + | CantApplyNonFunctional of ('constr, 'types) punsafe_judgment * ('constr, 'types) punsafe_judgment array + | IllFormedRecBody of 'constr pguard_error * Name.t array * int * env * ('constr, 'types) punsafe_judgment array | IllTypedRecBody of - int * Name.t array * unsafe_judgment array * types array + int * Name.t array * ('constr, 'types) punsafe_judgment array * 'types array | UnsatisfiedConstraints of Univ.constraints +type type_error = (constr, types) ptype_error + exception TypeError of env * type_error val error_unbound_rel : env -> int -> 'a diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml index d8c933912..142f061b5 100644 --- a/ltac/tacinterp.ml +++ b/ltac/tacinterp.ml @@ -2100,11 +2100,13 @@ let interp_redexp env sigma r = let _ = let eval ty env sigma lfun arg = + let ty = EConstr.Unsafe.to_constr ty in let ist = { lfun = lfun; extra = TacStore.empty; } in if Genarg.has_type arg (glbwit wit_tactic) then let tac = Genarg.out_gen (glbwit wit_tactic) arg in let tac = interp_tactic ist tac in - Pfedit.refine_by_tactic env sigma ty tac + let (c, sigma) = Pfedit.refine_by_tactic env sigma ty tac in + (EConstr.of_constr c, sigma) else failwith "not a tactic" in diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index 58454eedf..11da923e1 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -512,7 +512,7 @@ let f_equal = | _ -> Proofview.tclUNIT () end begin function (e, info) -> match e with - | Type_errors.TypeError _ -> Proofview.tclUNIT () + | Pretype_errors.PretypeError _ | Type_errors.TypeError _ -> Proofview.tclUNIT () | e -> Proofview.tclZERO ~info e end end } diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 92bd1e389..b43e2193a 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -89,9 +89,6 @@ let list_try_compile f l = let force_name = let nx = Name default_dependent_ident in function Anonymous -> nx | na -> na -let make_judge c ty = - make_judge (EConstr.Unsafe.to_constr c) (EConstr.Unsafe.to_constr ty) - (************************************************************************) (* Pattern-matching compilation (Cases) *) (************************************************************************) @@ -265,7 +262,7 @@ type 'a pattern_matching_problem = mat : 'a matrix; caseloc : Loc.t; casestyle : case_style; - typing_function: type_constraint -> env -> evar_map ref -> 'a option -> unsafe_judgment } + typing_function: type_constraint -> env -> evar_map ref -> 'a option -> EConstr.unsafe_judgment } (*--------------------------------------------------------------------------* * A few functions to infer the inductive type from the patterns instead of * @@ -366,12 +363,12 @@ let coerce_row typing_fun evdref env pats (tomatch,(_,indopt)) = let j = typing_fun tycon env evdref tomatch in let evd, j = Coercion.inh_coerce_to_base (loc_of_glob_constr tomatch) env !evdref j in evdref := evd; - let typ = EConstr.of_constr (nf_evar !evdref j.uj_type) in + let typ = EConstr.of_constr (nf_evar !evdref (EConstr.Unsafe.to_constr j.uj_type)) in let t = try try_find_ind env !evdref typ realnames with Not_found -> unify_tomatch_with_patterns evdref env loc typ pats realnames in - (EConstr.of_constr j.uj_val,t) + (j.uj_val,t) let coerce_to_indtype typing_fun evdref env matx tomatchl = let pats = List.map (fun r -> r.patterns) matx in @@ -415,7 +412,7 @@ let adjust_tomatch_to_pattern pb ((current,typ),deps,dep) = let _ = e_cumul pb.env pb.evdref indt typ in current else - EConstr.of_constr (evd_comb2 (Coercion.inh_conv_coerce_to true Loc.ghost pb.env) + (evd_comb2 (Coercion.inh_conv_coerce_to true Loc.ghost pb.env) pb.evdref (make_judge current typ) indt).uj_val in let sigma = !(pb.evdref) in (current,try_find_ind pb.env sigma indt names)) @@ -1002,7 +999,7 @@ let adjust_impossible_cases pb pred tomatch submat = | Evar (evk,_) when snd (evar_source evk !(pb.evdref)) == Evar_kinds.ImpossibleCase -> if not (Evd.is_defined !(pb.evdref) evk) then begin let evd, default = use_unit_judge !(pb.evdref) in - pb.evdref := Evd.define evk default.uj_type evd + pb.evdref := Evd.define evk (EConstr.Unsafe.to_constr default.uj_type) evd end; add_assert_false_case pb tomatch | _ -> @@ -1411,8 +1408,8 @@ and match_current pb (initial,tomatch) = make_case_or_project pb.env !(pb.evdref) indf ci pred current brvals in Typing.check_allowed_sort pb.env !(pb.evdref) mind current pred; - { uj_val = EConstr.Unsafe.to_constr (applist (case, inst)); - uj_type = EConstr.Unsafe.to_constr (prod_applist !(pb.evdref) typ inst) } + { uj_val = applist (case, inst); + uj_type = prod_applist !(pb.evdref) typ inst } (* Building the sub-problem when all patterns are variables. Case @@ -1429,8 +1426,8 @@ and shift_problem ((current,t),_,na) pb = history = pop_history pb.history; mat = List.map (push_current_pattern (current,ty)) pb.mat } in let j = compile pb in - { uj_val = EConstr.Unsafe.to_constr (subst1 current (EConstr.of_constr j.uj_val)); - uj_type = EConstr.Unsafe.to_constr (subst1 current (EConstr.of_constr j.uj_type)) } + { uj_val = subst1 current j.uj_val; + uj_type = subst1 current j.uj_type } (* Building the sub-problem when all patterns are variables, non-initial case. Variables which appear as subterms of constructor @@ -1453,7 +1450,7 @@ and compile_all_variables initial cur pb = (* Building the sub-problem when all patterns are variables *) and compile_branch initial current realargs names deps pb arsign eqns cstr = let sign, pb = build_branch initial current realargs deps names pb arsign eqns cstr in - sign, EConstr.of_constr (compile pb).uj_val + sign, (compile pb).uj_val (* Abstract over a declaration before continuing splitting *) and compile_generalization pb i d rest = @@ -1463,8 +1460,8 @@ and compile_generalization pb i d rest = tomatch = rest; mat = List.map (push_generalized_decl_eqn pb.env i d) pb.mat } in let j = compile pb in - { uj_val = Term.mkLambda_or_LetIn d j.uj_val; - uj_type = Term.mkProd_wo_LetIn d j.uj_type } + { uj_val = mkLambda_or_LetIn d j.uj_val; + uj_type = mkProd_wo_LetIn d j.uj_type } (* spiwack: the [initial] argument keeps track whether the alias has been introduced by a toplevel branch ([true]) or a deep one @@ -1482,11 +1479,11 @@ and compile_alias initial pb (na,orig,(expanded,expanded_typ)) rest = let j = compile pb in let sigma = !(pb.evdref) in { uj_val = - if isRel sigma c || isVar sigma c || count_occurrences sigma (mkRel 1) (EConstr.of_constr j.uj_val) <= 1 then - EConstr.Unsafe.to_constr (subst1 c (EConstr.of_constr j.uj_val)) + if isRel sigma c || isVar sigma c || count_occurrences sigma (mkRel 1) j.uj_val <= 1 then + subst1 c j.uj_val else - EConstr.Unsafe.to_constr (mkLetIn (na,c,t,EConstr.of_constr j.uj_val)); - uj_type = EConstr.Unsafe.to_constr (subst1 c (EConstr.of_constr j.uj_type)) } in + mkLetIn (na,c,t,j.uj_val); + uj_type = subst1 c j.uj_type } in (* spiwack: when an alias appears on a deep branch, its non-expanded form is automatically a variable of the same name. We avoid introducing such superfluous aliases so that refines are elegant. *) @@ -1726,7 +1723,7 @@ let build_tycon loc env tycon_env s subst tycon extenv evdref t = (t,tt) in let b = e_cumul env evdref tt (mkSort s) (* side effect *) in if not b then anomaly (Pp.str "Build_tycon: should be a type"); - { uj_val = EConstr.Unsafe.to_constr t; uj_type = EConstr.Unsafe.to_constr tt } + { uj_val = t; uj_type = tt } (* For a multiple pattern-matching problem Xi on t1..tn with return * type T, [build_inversion_problem Gamma Sigma (t1..tn) T] builds a return @@ -1851,7 +1848,7 @@ let build_inversion_problem loc env sigma tms t = caseloc = loc; casestyle = RegularStyle; typing_function = build_tycon loc env pb_env s subst} in - let pred = EConstr.of_constr (compile pb).uj_val in + let pred = (compile pb).uj_val in (!evdref,pred) (* Here, [pred] is assumed to be in the context built from all *) @@ -1905,7 +1902,7 @@ let extract_arity_signature ?(dolift=true) env0 tomatchl tmsign = let inh_conv_coerce_to_tycon loc env evdref j tycon = match tycon with | Some p -> - let (evd',j) = Coercion.inh_conv_coerce_to true loc env !evdref j (EConstr.of_constr p) in + let (evd',j) = Coercion.inh_conv_coerce_to true loc env !evdref j p in evdref := evd'; j | None -> j @@ -2029,7 +2026,7 @@ let prepare_predicate loc typing_fun env sigma tomatchs arsign tycon pred = let evdref = ref sigma in let predcclj = typing_fun (mk_tycon (EConstr.mkSort newt)) envar evdref rtntyp in let sigma = !evdref in - let predccl = EConstr.of_constr (j_nf_evar sigma predcclj).uj_val in + let predccl = EConstr.of_constr (nf_evar sigma (EConstr.Unsafe.to_constr predcclj.uj_val)) in [sigma, predccl] in List.map @@ -2095,7 +2092,7 @@ let constr_of_pat env evdref arsign pat avoid = let IndType (indf, _) = try find_rectype env ( !evdref) (lift (-(List.length realargs)) ty) with Not_found -> error_case_not_inductive env !evdref - {uj_val = EConstr.Unsafe.to_constr ty; uj_type = Typing.unsafe_type_of env !evdref ty} + {uj_val = ty; uj_type = EConstr.of_constr (Typing.unsafe_type_of env !evdref ty)} in let (ind,u), params = dest_ind_family indf in let params = List.map EConstr.of_constr params in @@ -2297,8 +2294,8 @@ let constrs_of_pats typing_fun env evdref eqns tomatchs sign neqs arity = in let rhs_env = push_rel_context rhs_rels' env in let j = typing_fun (mk_tycon tycon) rhs_env eqn.rhs.it in - let bbody = it_mkLambda_or_LetIn (EConstr.of_constr j.uj_val) rhs_rels' - and btype = it_mkProd_or_LetIn (EConstr.of_constr j.uj_type) rhs_rels' in + let bbody = it_mkLambda_or_LetIn j.uj_val rhs_rels' + and btype = it_mkProd_or_LetIn j.uj_type rhs_rels' in let _btype = evd_comb1 (Typing.type_of env) evdref bbody in let branch_name = Id.of_string ("program_branch_" ^ (string_of_int !i)) in let branch_decl = local_def (Name branch_name, lift !i bbody, lift !i btype) in @@ -2554,10 +2551,10 @@ let compile_program_cases loc style (typing_function, evdref) tycon env let j = compile pb in (* We check for unused patterns *) List.iter (check_unused_pattern env) matx; - let body = it_mkLambda_or_LetIn (applist (EConstr.of_constr j.uj_val, args)) lets in + let body = it_mkLambda_or_LetIn (applist (j.uj_val, args)) lets in let j = - { uj_val = EConstr.Unsafe.to_constr (it_mkLambda_or_LetIn body tomatchs_lets); - uj_type = EConstr.to_constr !evdref tycon; } + { uj_val = it_mkLambda_or_LetIn body tomatchs_lets; + uj_type = EConstr.of_constr (EConstr.to_constr !evdref tycon); } in j (**************************************************************************) @@ -2632,7 +2629,7 @@ let compile_cases loc style (typing_fun, evdref) tycon env (predopt, tomatchl, e let j = compile pb in (* We coerce to the tycon (if an elim predicate was provided) *) - let j = inh_conv_coerce_to_tycon loc env myevdref j (Option.map EConstr.Unsafe.to_constr tycon) in + let j = inh_conv_coerce_to_tycon loc env myevdref j tycon in evdref := !myevdref; j in diff --git a/pretyping/cases.mli b/pretyping/cases.mli index 9016ca5f3..9f26ae9ce 100644 --- a/pretyping/cases.mli +++ b/pretyping/cases.mli @@ -8,9 +8,9 @@ open Names open Term -open EConstr open Evd open Environ +open EConstr open Inductiveops open Glob_term open Evarutil @@ -111,11 +111,11 @@ type 'a pattern_matching_problem = typing_function: type_constraint -> env -> evar_map ref -> 'a option -> unsafe_judgment } -val compile : 'a pattern_matching_problem -> Environ.unsafe_judgment +val compile : 'a pattern_matching_problem -> unsafe_judgment val prepare_predicate : Loc.t -> (Evarutil.type_constraint -> - Environ.env -> Evd.evar_map ref -> 'a -> Environ.unsafe_judgment) -> + Environ.env -> Evd.evar_map ref -> 'a -> unsafe_judgment) -> Environ.env -> Evd.evar_map -> (types * tomatch_type) list -> diff --git a/pretyping/classops.ml b/pretyping/classops.ml index ad43bf322..9011186a3 100644 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -319,7 +319,7 @@ let coercion_value { coe_value = c; coe_type = t; coe_context = ctx; let subst, ctx = Universes.fresh_universe_context_set_instance ctx in let c' = Vars.subst_univs_level_constr subst c and t' = Vars.subst_univs_level_constr subst t in - (make_judge c' t', b, b'), ctx + (make_judge (EConstr.of_constr c') (EConstr.of_constr t'), b, b'), ctx (* pretty-print functions are now in Pretty *) (* rajouter une coercion dans le graphe *) diff --git a/pretyping/classops.mli b/pretyping/classops.mli index 9fb70534f..a1d030f12 100644 --- a/pretyping/classops.mli +++ b/pretyping/classops.mli @@ -8,9 +8,9 @@ open Names open Term +open Environ open EConstr open Evd -open Environ open Mod_subst (** {6 This is the type of class kinds } *) diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index b9f14aa43..2d4296fe4 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -53,16 +53,16 @@ let apply_coercion_args env evd check isproj argl funj = let rec apply_rec acc typ = function | [] -> if isproj then - let cst = fst (destConst !evdref (EConstr.of_constr (j_val funj))) in + let cst = fst (destConst !evdref (j_val funj)) in let p = Projection.make cst false in let pb = lookup_projection p env in let args = List.skipn pb.Declarations.proj_npars argl in let hd, tl = match args with hd :: tl -> hd, tl | [] -> assert false in - { uj_val = EConstr.Unsafe.to_constr (applist (mkProj (p, hd), tl)); - uj_type = EConstr.Unsafe.to_constr typ } + { uj_val = applist (mkProj (p, hd), tl); + uj_type = typ } else - { uj_val = EConstr.Unsafe.to_constr (applist (EConstr.of_constr (j_val funj),argl)); - uj_type = EConstr.Unsafe.to_constr typ } + { uj_val = applist (j_val funj,argl); + uj_type = typ } | h::restl -> (* On devrait pouvoir s'arranger pour qu'on n'ait pas a faire hnf_constr *) match EConstr.kind !evdref (EConstr.of_constr (whd_all env !evdref typ)) with | Prod (_,c1,c2) -> @@ -71,7 +71,7 @@ let apply_coercion_args env evd check isproj argl funj = apply_rec (h::acc) (Vars.subst1 h c2) restl | _ -> anomaly (Pp.str "apply_coercion_args") in - let res = apply_rec [] (EConstr.of_constr funj.uj_type) argl in + let res = apply_rec [] funj.uj_type argl in !evdref, res (* appliquer le chemin de coercions de patterns p *) @@ -367,7 +367,7 @@ let apply_coercion env sigma p hj typ_cl = (fun (ja,typ_cl,sigma) i -> let ((fv,isid,isproj),ctx) = coercion_value i in let sigma = Evd.merge_context_set Evd.univ_flexible sigma ctx in - let argl = (class_args_of env sigma typ_cl)@[EConstr.of_constr ja.uj_val] in + let argl = (class_args_of env sigma typ_cl)@[ja.uj_val] in let sigma, jres = apply_coercion_args env sigma true isproj argl fv in @@ -375,7 +375,7 @@ let apply_coercion env sigma p hj typ_cl = { uj_val = ja.uj_val; uj_type = jres.uj_type } else jres), - EConstr.of_constr jres.uj_type,sigma) + jres.uj_type,sigma) (hj,typ_cl,sigma) p in evd, j with NoCoercion as e -> raise e @@ -383,23 +383,23 @@ let apply_coercion env sigma p hj typ_cl = (* Try to coerce to a funclass; raise NoCoercion if not possible *) let inh_app_fun_core env evd j = - let t = whd_all env evd (EConstr.of_constr j.uj_type) in + let t = whd_all env evd j.uj_type in let t = EConstr.of_constr t in match EConstr.kind evd t with | Prod (_,_,_) -> (evd,j) | Evar ev -> let (evd',t) = Evardefine.define_evar_as_product evd ev in - (evd',{ uj_val = j.uj_val; uj_type = EConstr.Unsafe.to_constr t }) + (evd',{ uj_val = j.uj_val; uj_type = t }) | _ -> try let t,p = - lookup_path_to_fun_from env evd (EConstr.of_constr j.uj_type) in + lookup_path_to_fun_from env evd j.uj_type in apply_coercion env evd p j t with Not_found | NoCoercion -> if Flags.is_program_mode () then try let evdref = ref evd in let coercef, t = mu env evdref t in - let res = { uj_val = EConstr.Unsafe.to_constr (app_opt env evdref coercef (EConstr.of_constr j.uj_val)); uj_type = EConstr.Unsafe.to_constr t } in + let res = { uj_val = app_opt env evdref coercef j.uj_val; uj_type = t } in (!evdref, res) with NoSubtacCoercion | NoCoercion -> (evd,j) @@ -415,17 +415,23 @@ let inh_app_fun resolve_tc env evd j = try inh_app_fun_core env (saturate_evd env evd) j with NoCoercion -> (evd, j) +let type_judgment env sigma j = + match EConstr.kind sigma (EConstr.of_constr (whd_all env sigma j.uj_type)) with + | Sort s -> {utj_val = j.uj_val; utj_type = s } + | _ -> error_not_a_type env sigma j + let inh_tosort_force loc env evd j = try - let t,p = lookup_path_to_sort_from env evd (EConstr.of_constr j.uj_type) in + let t,p = lookup_path_to_sort_from env evd j.uj_type in let evd,j1 = apply_coercion env evd p j t in + let whd_evar evd c = EConstr.of_constr (whd_evar evd (EConstr.Unsafe.to_constr c)) in let j2 = on_judgment_type (whd_evar evd) j1 in - (evd,type_judgment env j2) + (evd,type_judgment env evd j2) with Not_found | NoCoercion -> error_not_a_type ~loc env evd j let inh_coerce_to_sort loc env evd j = - let typ = whd_all env evd (EConstr.of_constr j.uj_type) in + let typ = whd_all env evd j.uj_type in match EConstr.kind evd (EConstr.of_constr typ) with | Sort s -> (evd,{ utj_val = j.uj_val; utj_type = s }) | Evar ev -> @@ -437,10 +443,10 @@ let inh_coerce_to_sort loc env evd j = let inh_coerce_to_base loc env evd j = if Flags.is_program_mode () then let evdref = ref evd in - let ct, typ' = mu env evdref (EConstr.of_constr j.uj_type) in + let ct, typ' = mu env evdref j.uj_type in let res = - { uj_val = EConstr.Unsafe.to_constr (app_coercion env evdref ct (EConstr.of_constr j.uj_val)); - uj_type = EConstr.Unsafe.to_constr typ' } + { uj_val = (app_coercion env evdref ct j.uj_val); + uj_type = typ' } in !evdref, res else (evd, j) @@ -463,8 +469,8 @@ let inh_coerce_to_fail env evd rigidonly v t c1 = | Some v -> let evd,j = apply_coercion env evd p - {uj_val = EConstr.Unsafe.to_constr v; uj_type = EConstr.Unsafe.to_constr t} t2 in - evd, Some (EConstr.of_constr j.uj_val), (EConstr.of_constr j.uj_type) + {uj_val = v; uj_type = t} t2 in + evd, Some j.uj_val, j.uj_type | None -> evd, None, t with Not_found -> raise NoCoercion in @@ -510,27 +516,27 @@ let rec inh_conv_coerce_to_fail loc env evd rigidonly v t c1 = let inh_conv_coerce_to_gen resolve_tc rigidonly loc env evd cj t = let (evd', val') = try - inh_conv_coerce_to_fail loc env evd rigidonly (Some (EConstr.of_constr cj.uj_val)) (EConstr.of_constr cj.uj_type) t + inh_conv_coerce_to_fail loc env evd rigidonly (Some cj.uj_val) cj.uj_type t with NoCoercionNoUnifier (best_failed_evd,e) -> try if Flags.is_program_mode () then - coerce_itf loc env evd (Some (EConstr.of_constr cj.uj_val)) (EConstr.of_constr cj.uj_type) t + coerce_itf loc env evd (Some cj.uj_val) cj.uj_type t else raise NoSubtacCoercion with | NoSubtacCoercion when not resolve_tc || not !use_typeclasses_for_conversion -> - error_actual_type ~loc env best_failed_evd cj (EConstr.Unsafe.to_constr t) e + error_actual_type ~loc env best_failed_evd cj t e | NoSubtacCoercion -> let evd' = saturate_evd env evd in try if evd' == evd then - error_actual_type ~loc env best_failed_evd cj (EConstr.Unsafe.to_constr t) e + error_actual_type ~loc env best_failed_evd cj t e else - inh_conv_coerce_to_fail loc env evd' rigidonly (Some (EConstr.of_constr cj.uj_val)) (EConstr.of_constr cj.uj_type) t + inh_conv_coerce_to_fail loc env evd' rigidonly (Some cj.uj_val) cj.uj_type t with NoCoercionNoUnifier (_evd,_error) -> - error_actual_type ~loc env best_failed_evd cj (EConstr.Unsafe.to_constr t) e + error_actual_type ~loc env best_failed_evd cj t e in let val' = match val' with Some v -> v | None -> assert(false) in - (evd',{ uj_val = EConstr.Unsafe.to_constr val'; uj_type = EConstr.Unsafe.to_constr t }) + (evd',{ uj_val = val'; uj_type = t }) let inh_conv_coerce_to resolve_tc = inh_conv_coerce_to_gen resolve_tc false let inh_conv_coerce_rigid_to resolve_tc = inh_conv_coerce_to_gen resolve_tc true diff --git a/pretyping/coercion.mli b/pretyping/coercion.mli index 62d4fb004..bc63d092d 100644 --- a/pretyping/coercion.mli +++ b/pretyping/coercion.mli @@ -10,6 +10,7 @@ open Evd open Names open Term open Environ +open EConstr open Glob_term (** {6 Coercions. } *) @@ -36,7 +37,7 @@ val inh_coerce_to_base : Loc.t -> (** [inh_coerce_to_prod env isevars t] coerces [t] to a product type *) val inh_coerce_to_prod : Loc.t -> - env -> evar_map -> EConstr.types -> evar_map * EConstr.types + env -> evar_map -> types -> evar_map * types (** [inh_conv_coerce_to resolve_tc Loc.t env isevars j t] coerces [j] to an object of type [t]; i.e. it inserts a coercion into [j], if needed, in such @@ -44,16 +45,16 @@ val inh_coerce_to_prod : Loc.t -> applicable. resolve_tc=false disables resolving type classes (as the last resort before failing) *) val inh_conv_coerce_to : bool -> Loc.t -> - env -> evar_map -> unsafe_judgment -> EConstr.types -> evar_map * unsafe_judgment + env -> evar_map -> unsafe_judgment -> types -> evar_map * unsafe_judgment val inh_conv_coerce_rigid_to : bool -> Loc.t -> - env -> evar_map -> unsafe_judgment -> EConstr.types -> evar_map * unsafe_judgment + env -> evar_map -> unsafe_judgment -> types -> evar_map * unsafe_judgment (** [inh_conv_coerces_to loc env isevars t t'] checks if an object of type [t] is coercible to an object of type [t'] adding evar constraints if needed; it fails if no coercion exists *) val inh_conv_coerces_to : Loc.t -> - env -> evar_map -> EConstr.types -> EConstr.types -> evar_map + env -> evar_map -> types -> types -> evar_map (** [inh_pattern_coerce_to loc env isevars pat ind1 ind2] coerces the Cases pattern [pat] typed in [ind1] into a pattern typed in [ind2]; diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 3b420347b..639d6260e 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -1266,8 +1266,8 @@ let solve_unconstrained_impossible_cases env evd = let evd' = Evd.merge_context_set Evd.univ_flexible_alg ~loc evd' ctx in let ty = j_type j in let conv_algo = evar_conv_x full_transparent_state in - let evd' = check_evar_instance evd' evk (EConstr.of_constr ty) conv_algo in - Evd.define evk ty evd' + let evd' = check_evar_instance evd' evk ty conv_algo in + Evd.define evk (EConstr.Unsafe.to_constr ty) evd' | _ -> evd') evd evd let consider_remaining_unif_problems env diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml index 14b25ab36..673554005 100644 --- a/pretyping/pretype_errors.ml +++ b/pretyping/pretype_errors.ml @@ -31,11 +31,13 @@ type position_reporting = (position * int) * EConstr.t type subterm_unification_error = bool * position_reporting * position_reporting * (EConstr.constr * EConstr.constr * unification_error) option +type type_error = (EConstr.constr, EConstr.types) ptype_error + type pretype_error = (* Old Case *) - | CantFindCaseType of constr + | CantFindCaseType of EConstr.constr (* Type inference unification *) - | ActualTypeNotCoercible of unsafe_judgment * types * unification_error + | ActualTypeNotCoercible of EConstr.unsafe_judgment * EConstr.types * unification_error (* Tactic unification *) | UnifOccurCheck of existential_key * EConstr.constr | UnsolvableImplicit of existential_key * Evd.unsolvability_explanation option @@ -50,7 +52,7 @@ type pretype_error = | NonLinearUnification of Name.t * EConstr.constr (* Pretyping *) | VarNotFound of Id.t - | UnexpectedType of constr * constr + | UnexpectedType of EConstr.constr * EConstr.constr | NotProduct of EConstr.constr | TypingError of type_error | CannotUnifyOccurrences of subterm_unification_error @@ -75,14 +77,19 @@ let error_actual_type ?loc env sigma {uj_val=c;uj_type=actty} expty reason = raise_pretype_error ?loc (env, sigma, ActualTypeNotCoercible (j, expty, reason)) +let error_actual_type_core ?loc env sigma {uj_val=c;uj_type=actty} expty = + let j = {uj_val=c;uj_type=actty} in + raise_type_error ?loc + (env, sigma, ActualType (j, expty)) + let error_cant_apply_not_functional ?loc env sigma rator randl = raise_type_error ?loc - (env, sigma, CantApplyNonFunctional (rator, Array.of_list randl)) + (env, sigma, CantApplyNonFunctional (rator, randl)) let error_cant_apply_bad_type ?loc env sigma (n,c,t) rator randl = raise_type_error ?loc (env, sigma, - CantApplyBadType ((n,c,t), rator, Array.of_list randl)) + CantApplyBadType ((n,c,t), rator, randl)) let error_ill_formed_branch ?loc env sigma c i actty expty = raise_type_error @@ -98,9 +105,16 @@ let error_ill_typed_rec_body ?loc env sigma i na jl tys = raise_type_error ?loc (env, sigma, IllTypedRecBody (i, na, jl, tys)) +let error_elim_arity ?loc env sigma pi s c j a = + raise_type_error ?loc + (env, sigma, ElimArity (pi, s, c, j, a)) + let error_not_a_type ?loc env sigma j = raise_type_error ?loc (env, sigma, NotAType j) +let error_assumption ?loc env sigma j = + raise_type_error ?loc (env, sigma, BadAssumption j) + (*s Implicit arguments synthesis errors. It is hard to find a precise location. *) diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli index 2e707a0ff..0ebe4817c 100644 --- a/pretyping/pretype_errors.mli +++ b/pretyping/pretype_errors.mli @@ -32,11 +32,13 @@ type position_reporting = (position * int) * EConstr.t type subterm_unification_error = bool * position_reporting * position_reporting * (EConstr.constr * EConstr.constr * unification_error) option +type type_error = (EConstr.constr, EConstr.types) ptype_error + type pretype_error = (** Old Case *) - | CantFindCaseType of constr + | CantFindCaseType of EConstr.constr (** Type inference unification *) - | ActualTypeNotCoercible of unsafe_judgment * types * unification_error + | ActualTypeNotCoercible of EConstr.unsafe_judgment * EConstr.types * unification_error (** Tactic Unification *) | UnifOccurCheck of existential_key * EConstr.constr | UnsolvableImplicit of existential_key * Evd.unsolvability_explanation option @@ -51,7 +53,7 @@ type pretype_error = | NonLinearUnification of Name.t * EConstr.constr (** Pretyping *) | VarNotFound of Id.t - | UnexpectedType of constr * constr + | UnexpectedType of EConstr.constr * EConstr.constr | NotProduct of EConstr.constr | TypingError of type_error | CannotUnifyOccurrences of subterm_unification_error @@ -65,34 +67,45 @@ val precatchable_exception : exn -> bool (** Raising errors *) val error_actual_type : - ?loc:Loc.t -> env -> Evd.evar_map -> unsafe_judgment -> constr -> + ?loc:Loc.t -> env -> Evd.evar_map -> EConstr.unsafe_judgment -> EConstr.constr -> unification_error -> 'b +val error_actual_type_core : + ?loc:Loc.t -> env -> Evd.evar_map -> EConstr.unsafe_judgment -> EConstr.constr -> 'b + val error_cant_apply_not_functional : ?loc:Loc.t -> env -> Evd.evar_map -> - unsafe_judgment -> unsafe_judgment list -> 'b + EConstr.unsafe_judgment -> EConstr.unsafe_judgment array -> 'b val error_cant_apply_bad_type : - ?loc:Loc.t -> env -> Evd.evar_map -> int * constr * constr -> - unsafe_judgment -> unsafe_judgment list -> 'b + ?loc:Loc.t -> env -> Evd.evar_map -> int * EConstr.constr * EConstr.constr -> + EConstr.unsafe_judgment -> EConstr.unsafe_judgment array -> 'b val error_case_not_inductive : - ?loc:Loc.t -> env -> Evd.evar_map -> unsafe_judgment -> 'b + ?loc:Loc.t -> env -> Evd.evar_map -> EConstr.unsafe_judgment -> 'b val error_ill_formed_branch : ?loc:Loc.t -> env -> Evd.evar_map -> - constr -> pconstructor -> constr -> constr -> 'b + EConstr.constr -> pconstructor -> EConstr.constr -> EConstr.constr -> 'b val error_number_branches : ?loc:Loc.t -> env -> Evd.evar_map -> - unsafe_judgment -> int -> 'b + EConstr.unsafe_judgment -> int -> 'b val error_ill_typed_rec_body : ?loc:Loc.t -> env -> Evd.evar_map -> - int -> Name.t array -> unsafe_judgment array -> types array -> 'b + int -> Name.t array -> EConstr.unsafe_judgment array -> EConstr.types array -> 'b + +val error_elim_arity : + ?loc:Loc.t -> env -> Evd.evar_map -> + pinductive -> sorts_family list -> EConstr.constr -> + EConstr.unsafe_judgment -> (sorts_family * sorts_family * arity_error) option -> 'b val error_not_a_type : - ?loc:Loc.t -> env -> Evd.evar_map -> unsafe_judgment -> 'b + ?loc:Loc.t -> env -> Evd.evar_map -> EConstr.unsafe_judgment -> 'b + +val error_assumption : + ?loc:Loc.t -> env -> Evd.evar_map -> EConstr.unsafe_judgment -> 'b val error_cannot_coerce : env -> Evd.evar_map -> EConstr.constr * EConstr.constr -> 'b @@ -124,12 +137,12 @@ val error_non_linear_unification : env -> Evd.evar_map -> (** {6 Ml Case errors } *) val error_cant_find_case_type : - ?loc:Loc.t -> env -> Evd.evar_map -> constr -> 'b + ?loc:Loc.t -> env -> Evd.evar_map -> EConstr.constr -> 'b (** {6 Pretyping errors } *) val error_unexpected_type : - ?loc:Loc.t -> env -> Evd.evar_map -> constr -> constr -> 'b + ?loc:Loc.t -> env -> Evd.evar_map -> EConstr.constr -> EConstr.constr -> 'b val error_not_product : ?loc:Loc.t -> env -> Evd.evar_map -> EConstr.constr -> 'b diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index cac31a1c5..49a0bccee 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -34,6 +34,7 @@ open Reductionops open Environ open Type_errors open Typeops +open Typing open Globnames open Nameops open Evarutil @@ -124,7 +125,7 @@ let e_new_evar env evdref ?src ?naming typ = let sigma = Sigma.Unsafe.of_evar_map !evdref in let Sigma (e, sigma, _) = new_evar_instance sign sigma typ' ?src ?naming instance in evdref := Sigma.to_evar_map sigma; - e + EConstr.of_constr e let push_rec_types (lna,typarray,_) env = let ctxt = Array.map2_i (fun i na t -> local_assum (na, lift i t)) lna typarray in @@ -425,21 +426,19 @@ let invert_ltac_bound_name lvar env id0 id = str " which is not bound in current context.") let protected_get_type_of env sigma c = - try Retyping.get_type_of ~lax:true env.ExtraEnv.env sigma c + try EConstr.of_constr (Retyping.get_type_of ~lax:true env.ExtraEnv.env sigma c) with Retyping.RetypeError _ -> user_err (str "Cannot reinterpret " ++ quote (print_constr (EConstr.Unsafe.to_constr c)) ++ str " in the current environment.") -let j_val j = EConstr.of_constr (j_val j) - let pretype_id pretype k0 loc env evdref lvar id = let sigma = !evdref in (* Look for the binder of [id] *) try let (n,_,typ) = lookup_rel_id id (rel_context env) in let typ = EConstr.of_constr typ in - { uj_val = EConstr.Unsafe.to_constr (mkRel n); uj_type = EConstr.Unsafe.to_constr (lift n typ) } + { uj_val = mkRel n; uj_type = lift n typ } with Not_found -> let env = ltac_interp_name_env k0 lvar env in (* Check if [id] is an ltac variable *) @@ -447,7 +446,7 @@ let pretype_id pretype k0 loc env evdref lvar id = let (ids,c) = Id.Map.find id lvar.ltac_constrs in let subst = List.map (invert_ltac_bound_name lvar env id) ids in let c = substl subst (EConstr.of_constr c) in - { uj_val = EConstr.Unsafe.to_constr c; uj_type = protected_get_type_of env sigma c } + { uj_val = c; uj_type = protected_get_type_of env sigma c } with Not_found -> try let {closure;term} = Id.Map.find id lvar.ltac_uconstrs in let lvar = { @@ -472,7 +471,7 @@ let pretype_id pretype k0 loc env evdref lvar id = end; (* Check if [id] is a section or goal variable *) try - { uj_val = Constr.mkVar id; uj_type = NamedDecl.get_type (lookup_named id env) } + { uj_val = mkVar id; uj_type = EConstr.of_constr (NamedDecl.get_type (lookup_named id env)) } with Not_found -> (* [id] not found, standard error message *) error_var_not_found ~loc id @@ -511,9 +510,6 @@ let pretype_global loc rigid env evd gr us = let (sigma, c) = Evd.fresh_global ~loc ~rigid ?names:instance env.ExtraEnv.env evd gr in (sigma, EConstr.of_constr c) -let make_judge c t = - make_judge (EConstr.Unsafe.to_constr c) (EConstr.Unsafe.to_constr t) - let pretype_ref loc evdref env ref us = match ref with | VarRef id -> @@ -527,14 +523,14 @@ let pretype_ref loc evdref env ref us = | ref -> let evd, c = pretype_global loc univ_flexible env !evdref ref us in let () = evdref := evd in - let ty = Typing.unsafe_type_of env.ExtraEnv.env evd c in + let ty = unsafe_type_of env.ExtraEnv.env evd c in let ty = EConstr.of_constr ty in make_judge c ty let judge_of_Type loc evd s = let evd, s = interp_universe ~loc evd s in let judge = - { uj_val = Constr.mkSort (Type s); uj_type = Constr.mkSort (Type (Univ.super s)) } + { uj_val = mkSort (Type s); uj_type = mkSort (Type (Univ.super s)) } in evd, judge @@ -550,7 +546,7 @@ let new_type_evar env evdref loc = univ_flexible_alg ~src:(loc,Evar_kinds.InternalHole) in evdref := Sigma.to_evar_map sigma; - e + EConstr.of_constr e let (f_genarg_interp, genarg_interp_hook) = Hook.make () @@ -591,25 +587,25 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre let env = ltac_interp_name_env k0 lvar env in let ty = match tycon with - | Some ty -> EConstr.Unsafe.to_constr ty + | Some ty -> ty | None -> new_type_evar env evdref loc in let k = Evar_kinds.MatchingVar (someta,n) in - { uj_val = e_new_evar env evdref ~src:(loc,k) (EConstr.of_constr ty); uj_type = ty } + { uj_val = e_new_evar env evdref ~src:(loc,k) ty; uj_type = ty } | GHole (loc, k, naming, None) -> let env = ltac_interp_name_env k0 lvar env in let ty = match tycon with - | Some ty -> EConstr.Unsafe.to_constr ty + | Some ty -> ty | None -> new_type_evar env evdref loc in - { uj_val = e_new_evar env evdref ~src:(loc,k) ~naming (EConstr.of_constr ty); uj_type = ty } + { uj_val = e_new_evar env evdref ~src:(loc,k) ~naming ty; uj_type = ty } | GHole (loc, k, _naming, Some arg) -> let env = ltac_interp_name_env k0 lvar env in let ty = match tycon with - | Some ty -> EConstr.Unsafe.to_constr ty + | Some ty -> ty | None -> new_type_evar env evdref loc in let ist = lvar.ltac_genargs in @@ -622,14 +618,14 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre [] -> ctxt | (na,bk,None,ty)::bl -> let ty' = pretype_type empty_valcon env evdref lvar ty in - let dcl = LocalAssum (na, ty'.utj_val) in - let dcl' = LocalAssum (ltac_interp_name lvar na,ty'.utj_val) in + let dcl = local_assum (na, ty'.utj_val) in + let dcl' = local_assum (ltac_interp_name lvar na,ty'.utj_val) in type_bl (push_rel dcl env) (Context.Rel.add dcl' ctxt) bl | (na,bk,Some bd,ty)::bl -> let ty' = pretype_type empty_valcon env evdref lvar ty in - let bd' = pretype (mk_tycon (EConstr.of_constr ty'.utj_val)) env evdref lvar bd in - let dcl = LocalDef (na, bd'.uj_val, ty'.utj_val) in - let dcl' = LocalDef (ltac_interp_name lvar na, bd'.uj_val, ty'.utj_val) in + let bd' = pretype (mk_tycon ty'.utj_val) env evdref lvar bd in + let dcl = local_def (na, bd'.uj_val, ty'.utj_val) in + let dcl' = local_def (ltac_interp_name lvar na, bd'.uj_val, ty'.utj_val) in type_bl (push_rel dcl env) (Context.Rel.add dcl' ctxt) bl in let ctxtv = Array.map (type_bl env Context.Rel.empty) bl in let larj = @@ -637,8 +633,8 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre (fun e ar -> pretype_type empty_valcon (push_rel_context e env) evdref lvar ar) ctxtv lar in - let lara = Array.map (fun a -> EConstr.of_constr a.utj_val) larj in - let ftys = Array.map2 (fun e a -> EConstr.it_mkProd_or_LetIn a e) ctxtv lara in + let lara = Array.map (fun a -> a.utj_val) larj in + let ftys = Array.map2 (fun e a -> it_mkProd_or_LetIn a e) ctxtv lara in let nbfix = Array.length lar in let names = Array.map (fun id -> Name id) names in let _ = @@ -662,8 +658,8 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre (lift nbfix ftys.(i)) in let nenv = push_rel_context ctxt newenv in let j = pretype (mk_tycon ty) nenv evdref lvar def in - { uj_val = Termops.it_mkLambda_or_LetIn j.uj_val ctxt; - uj_type = Termops.it_mkProd_or_LetIn j.uj_type ctxt }) + { uj_val = it_mkLambda_or_LetIn j.uj_val ctxt; + uj_type = it_mkProd_or_LetIn j.uj_type ctxt }) ctxtv vdef in Typing.check_type_fixpoint loc env.ExtraEnv.env evdref names ftys vdefj; let nf c = nf_evar !evdref c in @@ -714,11 +710,11 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre (* Bidirectional typechecking hint: parameters of a constructor are completely determined by a typing constraint *) - if Flags.is_program_mode () && length > 0 && isConstruct !evdref (EConstr.of_constr fj.uj_val) then + if Flags.is_program_mode () && length > 0 && isConstruct !evdref fj.uj_val then match tycon with | None -> [] | Some ty -> - let ((ind, i), u) = destConstruct !evdref (EConstr.of_constr fj.uj_val) in + let ((ind, i), u) = destConstruct !evdref fj.uj_val in let npars = inductive_nparams ind in if Int.equal npars 0 then [] else @@ -731,7 +727,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre else [] in let app_f = - match EConstr.kind !evdref (EConstr.of_constr fj.uj_val) with + match EConstr.kind !evdref fj.uj_val with | Const (p, u) when Environ.is_projection p env.ExtraEnv.env -> let p = Projection.make p false in let pb = Environ.lookup_projection p env.ExtraEnv.env in @@ -746,7 +742,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre | c::rest -> let argloc = loc_of_glob_constr c in let resj = evd_comb1 (Coercion.inh_app_fun resolve_tc env.ExtraEnv.env) evdref resj in - let resty = whd_all env.ExtraEnv.env !evdref (EConstr.of_constr resj.uj_type) in + let resty = whd_all env.ExtraEnv.env !evdref resj.uj_type in let resty = EConstr.of_constr resty in match EConstr.kind !evdref resty with | Prod (na,c1,c2) -> @@ -761,18 +757,18 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre else [], j_val hj in let value, typ = app_f n (j_val resj) ujval, subst1 ujval c2 in - let j = { uj_val = EConstr.Unsafe.to_constr value; uj_type = EConstr.Unsafe.to_constr typ } in + let j = { uj_val = value; uj_type = typ } in apply_rec env (n+1) j candargs rest | _ -> let hj = pretype empty_tycon env evdref lvar c in error_cant_apply_not_functional ~loc:(Loc.merge floc argloc) env.ExtraEnv.env !evdref - resj [hj] + resj [|hj|] in let resj = apply_rec env 1 fj candargs args in let resj = - match EConstr.kind !evdref (EConstr.of_constr resj.uj_val) with + match EConstr.kind !evdref resj.uj_val with | App (f,args) -> if is_template_polymorphic env.ExtraEnv.env !evdref f then (* Special case for inductive type applications that must be @@ -804,7 +800,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre (* The name specified by ltac is used also to create bindings. So the substitution must also be applied on variables before they are looked up in the rel context. *) - let var = LocalAssum (name, j.utj_val) in + let var = local_assum (name, j.utj_val) in let j' = pretype rng (push_rel var env) evdref lvar c2 in let name = ltac_interp_name lvar name in let resj = judge_of_abstraction env.ExtraEnv.env (orelse_name name name') j j' in @@ -818,9 +814,9 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre let j' = match name with | Anonymous -> let j = pretype_type empty_valcon env evdref lvar c2 in - { j with utj_val = EConstr.Unsafe.to_constr (lift 1 (EConstr.of_constr j.utj_val)) } + { j with utj_val = lift 1 j.utj_val } | Name _ -> - let var = LocalAssum (name, j.utj_val) in + let var = local_assum (name, j.utj_val) in let env' = push_rel var env in pretype_type empty_valcon env' evdref lvar c2 in @@ -839,27 +835,27 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre match c1 with | GCast (loc, c, CastConv t) -> let tj = pretype_type empty_valcon env evdref lvar t in - pretype (mk_tycon (EConstr.of_constr tj.utj_val)) env evdref lvar c + pretype (mk_tycon tj.utj_val) env evdref lvar c | _ -> pretype empty_tycon env evdref lvar c1 in let t = evd_comb1 (Evarsolve.refresh_universes ~onlyalg:true ~status:Evd.univ_flexible (Some false) env.ExtraEnv.env) - evdref (EConstr.of_constr j.uj_type) in + evdref j.uj_type in + let t = EConstr.of_constr t in (* The name specified by ltac is used also to create bindings. So the substitution must also be applied on variables before they are looked up in the rel context. *) - let var = LocalDef (name, j.uj_val, t) in - let t = EConstr.of_constr t in + let var = local_def (name, j.uj_val, t) in let tycon = lift_tycon 1 tycon in let j' = pretype tycon (push_rel var env) evdref lvar c2 in let name = ltac_interp_name lvar name in - { uj_val = EConstr.Unsafe.to_constr (mkLetIn (name, EConstr.of_constr j.uj_val, t, EConstr.of_constr j'.uj_val)) ; - uj_type = EConstr.Unsafe.to_constr (subst1 (EConstr.of_constr j.uj_val) (EConstr.of_constr j'.uj_type)) } + { uj_val = mkLetIn (name, j.uj_val, t, j'.uj_val) ; + uj_type = subst1 j.uj_val j'.uj_type } | GLetTuple (loc,nal,(na,po),c,d) -> let cj = pretype empty_tycon env evdref lvar c in let (IndType (indf,realargs)) = - try find_rectype env.ExtraEnv.env !evdref (EConstr.of_constr cj.uj_type) + try find_rectype env.ExtraEnv.env !evdref cj.uj_type with Not_found -> let cloc = loc_of_glob_constr c in error_case_not_inductive ~loc:cloc env.ExtraEnv.env !evdref cj @@ -883,7 +879,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre | na :: names, (LocalAssum (_,t) :: l) -> let t = EConstr.of_constr t in let proj = Projection.make ps.(cs.cs_nargs - k) true in - local_def (na, lift (cs.cs_nargs - n) (mkProj (proj, EConstr.of_constr cj.uj_val)), t) + local_def (na, lift (cs.cs_nargs - n) (mkProj (proj, cj.uj_val)), t) :: aux (n+1) (k + 1) names l | na :: names, (decl :: l) -> set_name na decl :: aux (n+1) k names l @@ -897,7 +893,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre let fsign = List.map2 set_name nal fsign in let f = it_mkLambda_or_LetIn f fsign in let ci = make_case_info env.ExtraEnv.env (fst ind) LetStyle in - mkCase (ci, p, EConstr.of_constr cj.uj_val,[|f|]) + mkCase (ci, p, cj.uj_val,[|f|]) else it_mkLambda_or_LetIn f fsign in let env_f = push_rel_context fsign env in @@ -914,7 +910,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre | Some p -> let env_p = push_rel_context psign env in let pj = pretype_type empty_valcon env_p evdref lvar p in - let ccl = nf_evar !evdref (EConstr.of_constr pj.utj_val) in + let ccl = nf_evar !evdref pj.utj_val in let psign = make_arity_signature env.ExtraEnv.env true indf in (* with names *) let p = it_mkLambda_or_LetIn ccl psign in let inst = @@ -922,18 +918,19 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre @[EConstr.of_constr (build_dependent_constructor cs)] in let lp = lift cs.cs_nargs p in let fty = hnf_lam_applist env.ExtraEnv.env !evdref lp inst in - let fj = pretype (mk_tycon (EConstr.of_constr fty)) env_f evdref lvar d in + let fty = EConstr.of_constr fty in + let fj = pretype (mk_tycon fty) env_f evdref lvar d in let v = let ind,_ = dest_ind_family indf in - Typing.check_allowed_sort env.ExtraEnv.env !evdref ind (EConstr.of_constr cj.uj_val) p; - obj ind p cj.uj_val (EConstr.of_constr fj.uj_val) + Typing.check_allowed_sort env.ExtraEnv.env !evdref ind cj.uj_val p; + obj ind p cj.uj_val fj.uj_val in - { uj_val = EConstr.Unsafe.to_constr v; uj_type = EConstr.Unsafe.to_constr (substl (realargs@[EConstr.of_constr cj.uj_val]) ccl) } + { uj_val = v; uj_type = (substl (realargs@[cj.uj_val]) ccl) } | None -> let tycon = lift_tycon cs.cs_nargs tycon in let fj = pretype tycon env_f evdref lvar d in - let ccl = nf_evar !evdref (EConstr.of_constr fj.uj_type) in + let ccl = nf_evar !evdref fj.uj_type in let ccl = if noccur_between !evdref 1 cs.cs_nargs ccl then lift (- cs.cs_nargs) ccl @@ -944,14 +941,14 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre let p = it_mkLambda_or_LetIn (lift (nar+1) ccl) psign in let v = let ind,_ = dest_ind_family indf in - Typing.check_allowed_sort env.ExtraEnv.env !evdref ind (EConstr.of_constr cj.uj_val) p; - obj ind p cj.uj_val (EConstr.of_constr fj.uj_val) - in { uj_val = EConstr.Unsafe.to_constr v; uj_type = EConstr.Unsafe.to_constr ccl }) + Typing.check_allowed_sort env.ExtraEnv.env !evdref ind cj.uj_val p; + obj ind p cj.uj_val fj.uj_val + in { uj_val = v; uj_type = ccl }) | GIf (loc,c,(na,po),b1,b2) -> let cj = pretype empty_tycon env evdref lvar c in let (IndType (indf,realargs)) = - try find_rectype env.ExtraEnv.env !evdref (EConstr.of_constr cj.uj_type) + try find_rectype env.ExtraEnv.env !evdref cj.uj_type with Not_found -> let cloc = loc_of_glob_constr c in error_case_not_inductive ~loc:cloc env.ExtraEnv.env !evdref cj in @@ -973,16 +970,16 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre | Some p -> let env_p = push_rel_context psign env in let pj = pretype_type empty_valcon env_p evdref lvar p in - let ccl = nf_evar !evdref (EConstr.of_constr pj.utj_val) in + let ccl = nf_evar !evdref pj.utj_val in let pred = it_mkLambda_or_LetIn ccl psign in - let typ = lift (- nar) (EConstr.of_constr (beta_applist !evdref (pred,[EConstr.of_constr cj.uj_val]))) in + let typ = lift (- nar) (EConstr.of_constr (beta_applist !evdref (pred,[cj.uj_val]))) in pred, typ | None -> let p = match tycon with | Some ty -> ty | None -> let env = ltac_interp_name_env k0 lvar env in - EConstr.of_constr (new_type_evar env evdref loc) + new_type_evar env evdref loc in it_mkLambda_or_LetIn (lift (nar+1) p) psign, p in let pred = nf_evar !evdref pred in @@ -991,6 +988,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre let n = Context.Rel.length cs.cs_args in let pi = lift n pred in (* liftn n 2 pred ? *) let pi = beta_applist !evdref (pi, [EConstr.of_constr (build_dependent_constructor cs)]) in + let pi = EConstr.of_constr pi in let csgn = if not !allow_anonymous_refs then List.map (set_name Anonymous) cs.cs_args @@ -1000,18 +998,18 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre cs.cs_args in let env_c = push_rel_context csgn env in - let bj = pretype (mk_tycon (EConstr.of_constr pi)) env_c evdref lvar b in - it_mkLambda_or_LetIn (EConstr.of_constr bj.uj_val) cs.cs_args in + let bj = pretype (mk_tycon pi) env_c evdref lvar b in + it_mkLambda_or_LetIn bj.uj_val cs.cs_args in let b1 = f cstrs.(0) b1 in let b2 = f cstrs.(1) b2 in let v = let ind,_ = dest_ind_family indf in let ci = make_case_info env.ExtraEnv.env (fst ind) IfStyle in let pred = nf_evar !evdref pred in - Typing.check_allowed_sort env.ExtraEnv.env !evdref ind (EConstr.of_constr cj.uj_val) pred; - mkCase (ci, pred, EConstr.of_constr cj.uj_val, [|b1;b2|]) + Typing.check_allowed_sort env.ExtraEnv.env !evdref ind cj.uj_val pred; + mkCase (ci, pred, cj.uj_val, [|b1;b2|]) in - let cj = { uj_val = EConstr.Unsafe.to_constr v; uj_type = EConstr.Unsafe.to_constr p } in + let cj = { uj_val = v; uj_type = p } in inh_conv_coerce_to_tycon loc env evdref cj tycon | GCases (loc,sty,po,tml,eqns) -> @@ -1030,36 +1028,36 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre let tj = pretype_type empty_valcon env evdref lvar t in let tval = evd_comb1 (Evarsolve.refresh_universes ~onlyalg:true ~status:Evd.univ_flexible (Some false) env.ExtraEnv.env) - evdref (EConstr.of_constr tj.utj_val) in + evdref tj.utj_val in let tval = EConstr.of_constr tval in let tval = nf_evar !evdref tval in let cj, tval = match k with | VMcast -> let cj = pretype empty_tycon env evdref lvar c in - let cty = nf_evar !evdref (EConstr.of_constr cj.uj_type) and tval = nf_evar !evdref tval in + let cty = nf_evar !evdref cj.uj_type and tval = nf_evar !evdref tval in if not (occur_existential !evdref cty || occur_existential !evdref tval) then let (evd,b) = Reductionops.vm_infer_conv env.ExtraEnv.env !evdref cty tval in if b then (evdref := evd; cj, tval) else - error_actual_type ~loc env.ExtraEnv.env !evdref cj (EConstr.Unsafe.to_constr tval) + error_actual_type ~loc env.ExtraEnv.env !evdref cj tval (ConversionFailed (env.ExtraEnv.env,cty,tval)) else user_err ~loc (str "Cannot check cast with vm: " ++ str "unresolved arguments remain.") | NATIVEcast -> let cj = pretype empty_tycon env evdref lvar c in - let cty = nf_evar !evdref (EConstr.of_constr cj.uj_type) and tval = nf_evar !evdref tval in + let cty = nf_evar !evdref cj.uj_type and tval = nf_evar !evdref tval in begin let (evd,b) = Nativenorm.native_infer_conv env.ExtraEnv.env !evdref cty tval in if b then (evdref := evd; cj, tval) else - error_actual_type ~loc env.ExtraEnv.env !evdref cj (EConstr.Unsafe.to_constr tval) + error_actual_type ~loc env.ExtraEnv.env !evdref cj tval (ConversionFailed (env.ExtraEnv.env,cty,tval)) end | _ -> pretype (mk_tycon tval) env evdref lvar c, tval in - let v = mkCast (EConstr.of_constr cj.uj_val, k, tval) in - { uj_val = EConstr.Unsafe.to_constr v; uj_type = EConstr.Unsafe.to_constr tval } + let v = mkCast (cj.uj_val, k, tval) in + { uj_val = v; uj_type = tval } in inh_conv_coerce_to_tycon loc env evdref cj tycon and pretype_instance k0 resolve_tc env evdref lvar loc hyps evk update = @@ -1070,7 +1068,7 @@ and pretype_instance k0 resolve_tc env evdref lvar loc hyps evk update = try let c = List.assoc id update in let c = pretype k0 resolve_tc (mk_tycon t) env evdref lvar c in - EConstr.of_constr c.uj_val, List.remove_assoc id update + c.uj_val, List.remove_assoc id update with Not_found -> try let (n,_,t') = lookup_rel_id id (rel_context env) in @@ -1103,13 +1101,14 @@ and pretype_type k0 resolve_tc valcon (env : ExtraEnv.t) evdref lvar = function let s = let sigma = !evdref in let t = Retyping.get_type_of env.ExtraEnv.env sigma v in - match EConstr.kind sigma (EConstr.of_constr (whd_all env.ExtraEnv.env sigma (EConstr.of_constr t))) with + let t = EConstr.of_constr t in + match EConstr.kind sigma (EConstr.of_constr (whd_all env.ExtraEnv.env sigma t)) with | Sort s -> s | Evar ev when is_Type (existential_type sigma ev) -> evd_comb1 (define_evar_as_sort env.ExtraEnv.env) evdref ev | _ -> anomaly (Pp.str "Found a type constraint which is not a type") in - { utj_val = EConstr.Unsafe.to_constr v; + { utj_val = v; utj_type = s } | None -> let env = ltac_interp_name_env k0 lvar env in @@ -1123,10 +1122,10 @@ and pretype_type k0 resolve_tc valcon (env : ExtraEnv.t) evdref lvar = function match valcon with | None -> tj | Some v -> - if e_cumul env.ExtraEnv.env evdref v (EConstr.of_constr tj.utj_val) then tj + if e_cumul env.ExtraEnv.env evdref v tj.utj_val then tj else error_unexpected_type - ~loc:(loc_of_glob_constr c) env.ExtraEnv.env !evdref tj.utj_val (EConstr.Unsafe.to_constr v) + ~loc:(loc_of_glob_constr c) env.ExtraEnv.env !evdref tj.utj_val v let ise_pretype_gen flags env sigma lvar kind c = let env = make_env env in @@ -1140,7 +1139,7 @@ let ise_pretype_gen flags env sigma lvar kind c = | IsType -> (pretype_type k0 flags.use_typeclasses empty_valcon env evdref lvar c).utj_val in - process_inference_flags flags env.ExtraEnv.env sigma (!evdref,EConstr.of_constr c') + process_inference_flags flags env.ExtraEnv.env sigma (!evdref,c') let default_inference_flags fail = { use_typeclasses = true; @@ -1167,9 +1166,9 @@ let empty_lvar : ltac_var_map = { } let on_judgment sigma f j = - let c = mkCast(EConstr.of_constr j.uj_val,DEFAULTcast, EConstr.of_constr j.uj_type) in + let c = mkCast(j.uj_val,DEFAULTcast, j.uj_type) in let (c,_,t) = destCast sigma (f c) in - {uj_val = EConstr.Unsafe.to_constr c; uj_type = EConstr.Unsafe.to_constr t} + {uj_val = c; uj_type = t} let understand_judgment env sigma c = let env = make_env env in diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli index 603b9f9ea..2f3ce3afa 100644 --- a/pretyping/pretyping.mli +++ b/pretyping/pretyping.mli @@ -110,11 +110,11 @@ val understand : ?flags:inference_flags -> ?expected_type:typing_constraint -> (** Idem but returns the judgment of the understood term *) val understand_judgment : env -> evar_map -> - glob_constr -> unsafe_judgment Evd.in_evar_universe_context + glob_constr -> EConstr.unsafe_judgment Evd.in_evar_universe_context (** Idem but do not fail on unresolved evars (type cl*) val understand_judgment_tcc : env -> evar_map ref -> - glob_constr -> unsafe_judgment + glob_constr -> EConstr.unsafe_judgment val type_uconstr : ?flags:inference_flags -> @@ -145,11 +145,11 @@ val check_evars : env -> evar_map -> evar_map -> EConstr.constr -> unit (** Internal of Pretyping... *) val pretype : int -> bool -> type_constraint -> env -> evar_map ref -> - ltac_var_map -> glob_constr -> unsafe_judgment + ltac_var_map -> glob_constr -> EConstr.unsafe_judgment val pretype_type : int -> bool -> val_constraint -> env -> evar_map ref -> - ltac_var_map -> glob_constr -> unsafe_type_judgment + ltac_var_map -> glob_constr -> EConstr.unsafe_type_judgment val ise_pretype_gen : inference_flags -> env -> evar_map -> @@ -163,5 +163,5 @@ val interp_sort : ?loc:Loc.t -> evar_map -> glob_sort -> evar_map * sorts val interp_elimination_sort : glob_sort -> sorts_family val genarg_interp_hook : - (types -> env -> evar_map -> unbound_ltac_var_map -> - Genarg.glob_generic_argument -> constr * evar_map) Hook.t + (EConstr.types -> env -> evar_map -> unbound_ltac_var_map -> + Genarg.glob_generic_argument -> EConstr.constr * evar_map) Hook.t diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index 2efb02417..a7ccf98a6 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -244,7 +244,7 @@ let get_type_of ?(polyprop=true) ?(lax=false) env sigma c = if lax then EConstr.Unsafe.to_constr (f env c) else EConstr.Unsafe.to_constr (anomaly_on_error (f env) c) (* Makes an unsafe judgment from a constr *) -let get_judgment_of env evc c = { uj_val = EConstr.Unsafe.to_constr c; uj_type = get_type_of env evc c } +let get_judgment_of env evc c = { uj_val = c; uj_type = EConstr.of_constr (get_type_of env evc c) } (* Returns sorts of a context *) let sorts_of_context env evc ctxt = diff --git a/pretyping/retyping.mli b/pretyping/retyping.mli index 08f750287..c84403890 100644 --- a/pretyping/retyping.mli +++ b/pretyping/retyping.mli @@ -35,7 +35,7 @@ val get_sort_family_of : ?polyprop:bool -> env -> evar_map -> EConstr.types -> sorts_family (** Makes an unsafe judgment from a constr *) -val get_judgment_of : env -> evar_map -> EConstr.constr -> unsafe_judgment +val get_judgment_of : env -> evar_map -> EConstr.constr -> EConstr.unsafe_judgment val type_of_global_reference_knowing_parameters : env -> evar_map -> EConstr.constr -> EConstr.constr array -> types diff --git a/pretyping/typing.ml b/pretyping/typing.ml index c948f9b9a..17adea5f2 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -6,20 +6,31 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +module CVars = Vars + open Pp open CErrors open Util open Term +open EConstr open Vars open Environ open Reductionops -open Type_errors open Inductive open Inductiveops open Typeops open Arguments_renaming +open Pretype_errors open Context.Rel.Declaration +let local_assum (na, t) = + let inj = EConstr.Unsafe.to_constr in + LocalAssum (na, inj t) + +let local_def (na, b, t) = + let inj = EConstr.Unsafe.to_constr in + LocalDef (na, inj b, inj t) + let push_rec_types pfix env = let (i, c, t) = pfix in let inj c = EConstr.Unsafe.to_constr c in @@ -31,57 +42,57 @@ let meta_type evd mv = with Not_found -> anomaly (str "unknown meta ?" ++ str (Nameops.string_of_meta mv)) in meta_instance evd ty -let constant_type_knowing_parameters env cst jl = - let paramstyp = Array.map (fun j -> lazy j.uj_type) jl in +let constant_type_knowing_parameters env sigma cst jl = + let paramstyp = Array.map (fun j -> lazy (EConstr.to_constr sigma j.uj_type)) jl in EConstr.of_constr (type_of_constant_knowing_parameters_in env cst paramstyp) -let inductive_type_knowing_parameters env (ind,u) jl = +let inductive_type_knowing_parameters env sigma (ind,u) jl = let mspec = lookup_mind_specif env ind in - let paramstyp = Array.map (fun j -> lazy j.uj_type) jl in + let paramstyp = Array.map (fun j -> lazy (EConstr.to_constr sigma j.uj_type)) jl in EConstr.of_constr (Inductive.type_of_inductive_knowing_parameters env (mspec,u) paramstyp) let e_type_judgment env evdref j = - match EConstr.kind !evdref (EConstr.of_constr (whd_all env !evdref (EConstr.of_constr j.uj_type))) with + match EConstr.kind !evdref (EConstr.of_constr (whd_all env !evdref j.uj_type)) with | Sort s -> {utj_val = j.uj_val; utj_type = s } | Evar ev -> let (evd,s) = Evardefine.define_evar_as_sort env !evdref ev in evdref := evd; { utj_val = j.uj_val; utj_type = s } - | _ -> error_not_type env j + | _ -> error_not_a_type env !evdref j let e_assumption_of_judgment env evdref j = - try EConstr.of_constr (e_type_judgment env evdref j).utj_val - with TypeError _ -> - error_assumption env j + try (e_type_judgment env evdref j).utj_val + with Type_errors.TypeError _ | PretypeError _ -> + error_assumption env !evdref j let e_judge_of_apply env evdref funj argjv = let open EConstr in let rec apply_rec n typ = function | [] -> - { uj_val = Constr.mkApp (j_val funj, Array.map j_val argjv); - uj_type = EConstr.Unsafe.to_constr typ } + { uj_val = mkApp (j_val funj, Array.map j_val argjv); + uj_type = typ } | hj::restjl -> match EConstr.kind !evdref (EConstr.of_constr (whd_all env !evdref typ)) with | Prod (_,c1,c2) -> - if Evarconv.e_cumul env evdref (EConstr.of_constr hj.uj_type) c1 then - apply_rec (n+1) (Vars.subst1 (EConstr.of_constr hj.uj_val) c2) restjl + if Evarconv.e_cumul env evdref hj.uj_type c1 then + apply_rec (n+1) (subst1 hj.uj_val c2) restjl else - error_cant_apply_bad_type env (n, EConstr.Unsafe.to_constr c1, hj.uj_type) funj argjv + error_cant_apply_bad_type env !evdref (n, c1, hj.uj_type) funj argjv | Evar ev -> let (evd',t) = Evardefine.define_evar_as_product !evdref ev in evdref := evd'; let (_,_,c2) = destProd evd' t in - apply_rec (n+1) (Vars.subst1 (EConstr.of_constr hj.uj_val) c2) restjl + apply_rec (n+1) (subst1 hj.uj_val c2) restjl | _ -> - error_cant_apply_not_functional env funj argjv + error_cant_apply_not_functional env !evdref funj argjv in - apply_rec 1 (EConstr.of_constr funj.uj_type) (Array.to_list argjv) + apply_rec 1 funj.uj_type (Array.to_list argjv) let e_check_branch_types env evdref (ind,u) cj (lfj,explft) = if not (Int.equal (Array.length lfj) (Array.length explft)) then - error_number_branches env cj (Array.length explft); + error_number_branches env !evdref cj (Array.length explft); for i = 0 to Array.length explft - 1 do - if not (Evarconv.e_cumul env evdref (EConstr.of_constr lfj.(i).uj_type) (EConstr.of_constr explft.(i))) then - error_ill_formed_branch env cj.uj_val ((ind,i+1),u) lfj.(i).uj_type explft.(i) + if not (Evarconv.e_cumul env evdref lfj.(i).uj_type explft.(i)) then + error_ill_formed_branch env !evdref cj.uj_val ((ind,i+1),u) lfj.(i).uj_type explft.(i) done let max_sort l = @@ -92,13 +103,13 @@ let e_is_correct_arity env evdref c pj ind specif params = let open EConstr in let arsign = make_arity_signature env true (make_ind_family (ind,params)) in let allowed_sorts = elim_sorts specif in - let error () = error_elim_arity env ind allowed_sorts c pj None in + let error () = Pretype_errors.error_elim_arity env !evdref ind allowed_sorts c pj None in let rec srec env pt ar = let pt' = EConstr.of_constr (whd_all env !evdref pt) in match EConstr.kind !evdref pt', ar with | Prod (na1,a1,t), (LocalAssum (_,a1'))::ar' -> if not (Evarconv.e_cumul env evdref a1 (EConstr.of_constr a1')) then error (); - srec (push_rel (LocalAssum (na1,EConstr.Unsafe.to_constr a1)) env) t ar' + srec (push_rel (local_assum (na1,a1)) env) t ar' | Sort s, [] -> if not (Sorts.List.mem (Sorts.family s) allowed_sorts) then error () @@ -106,27 +117,43 @@ let e_is_correct_arity env evdref c pj ind specif params = let evd, s = Evd.fresh_sort_in_family env !evdref (max_sort allowed_sorts) in evdref := Evd.define ev (Constr.mkSort s) evd | _, (LocalDef _ as d)::ar' -> - srec (push_rel d env) (Vars.lift 1 pt') ar' + srec (push_rel d env) (lift 1 pt') ar' | _ -> error () in - srec env (EConstr.of_constr pj.uj_type) (List.rev arsign) + srec env pj.uj_type (List.rev arsign) + +let lambda_applist_assum sigma n c l = + let open EConstr in + let rec app n subst t l = + if Int.equal n 0 then + if l == [] then substl subst t + else anomaly (Pp.str "Not enough arguments") + else match EConstr.kind sigma t, l with + | Lambda(_,_,c), arg::l -> app (n-1) (arg::subst) c l + | LetIn(_,b,_,c), _ -> app (n-1) (substl subst b::subst) c l + | _ -> anomaly (Pp.str "Not enough lambda/let's") in + app n [] c l let e_type_case_branches env evdref (ind,largs) pj c = let specif = lookup_mind_specif env (fst ind) in let nparams = inductive_params specif in let (params,realargs) = List.chop nparams largs in let p = pj.uj_val in + let realargs = List.map EConstr.of_constr realargs in let () = e_is_correct_arity env evdref c pj ind specif params in - let lc = build_branches_type ind specif params p in + let lc = build_branches_type ind specif params (EConstr.to_constr !evdref p) in + let lc = Array.map EConstr.of_constr lc in let n = (snd specif).Declarations.mind_nrealdecls in - let ty = whd_betaiota !evdref (EConstr.of_constr (lambda_applist_assum (n+1) p (realargs@[c]))) in + let ty = whd_betaiota !evdref (lambda_applist_assum !evdref (n+1) p (realargs@[c])) in + let ty = EConstr.of_constr ty in (lc, ty) let e_judge_of_case env evdref ci pj cj lfj = + let open EConstr in let indspec = - try find_mrectype env !evdref (EConstr.of_constr cj.uj_type) - with Not_found -> error_case_not_inductive env cj in + try find_mrectype env !evdref cj.uj_type + with Not_found -> error_case_not_inductive env !evdref cj in let _ = check_case_info env (fst indspec) ci in let (bty,rslty) = e_type_case_branches env evdref indspec pj cj.uj_val in e_check_branch_types env evdref (fst indspec) cj (lfj,bty); @@ -138,27 +165,28 @@ let check_type_fixpoint loc env evdref lna lar vdefj = let lt = Array.length vdefj in if Int.equal (Array.length lar) lt then for i = 0 to lt-1 do - if not (Evarconv.e_cumul env evdref (EConstr.of_constr (vdefj.(i)).uj_type) - (Vars.lift lt lar.(i))) then - Pretype_errors.error_ill_typed_rec_body ~loc env !evdref - i lna vdefj (Array.map EConstr.Unsafe.to_constr lar) + if not (Evarconv.e_cumul env evdref (vdefj.(i)).uj_type + (lift lt lar.(i))) then + error_ill_typed_rec_body ~loc env !evdref + i lna vdefj lar done (* FIXME: might depend on the level of actual parameters!*) let check_allowed_sort env sigma ind c p = let pj = Retyping.get_judgment_of env sigma p in - let ksort = family_of_sort (sort_of_arity env sigma (EConstr.of_constr pj.uj_type)) in + let ksort = family_of_sort (sort_of_arity env sigma pj.uj_type) in let specif = Global.lookup_inductive (fst ind) in let sorts = elim_sorts specif in if not (List.exists ((==) ksort) sorts) then let s = inductive_sort_family (snd specif) in - error_elim_arity env ind sorts (EConstr.Unsafe.to_constr c) pj - (Some(ksort,s,error_elim_explain ksort s)) + error_elim_arity env sigma ind sorts c pj + (Some(ksort,s,Type_errors.error_elim_explain ksort s)) let e_judge_of_cast env evdref cj k tj = + let open EConstr in let expected_type = tj.utj_val in - if not (Evarconv.e_cumul env evdref (EConstr.of_constr cj.uj_type) (EConstr.of_constr expected_type)) then - error_actual_type env cj expected_type; + if not (Evarconv.e_cumul env evdref cj.uj_type expected_type) then + error_actual_type_core env !evdref cj expected_type; { uj_val = mkCast (cj.uj_val, k, expected_type); uj_type = expected_type } @@ -178,11 +206,56 @@ let check_cofix env sigma pcofix = let (idx, (ids, cs, ts)) = pcofix in check_cofix env (idx, (ids, Array.map inj cs, Array.map inj ts)) -let make_judge c ty = - make_judge (EConstr.Unsafe.to_constr c) (EConstr.Unsafe.to_constr ty) - (* The typing machine with universes and existential variables. *) +let judge_of_prop = + { uj_val = EConstr.mkProp; + uj_type = EConstr.mkSort type1_sort } + +let judge_of_set = + { uj_val = EConstr.mkSet; + uj_type = EConstr.mkSort type1_sort } + +let judge_of_prop_contents = function + | Null -> judge_of_prop + | Pos -> judge_of_set + +let judge_of_type u = + let uu = Univ.Universe.super u in + { uj_val = EConstr.mkType u; + uj_type = EConstr.mkType uu } + +let judge_of_relative env v = + Termops.on_judgment EConstr.of_constr (judge_of_relative env v) + +let judge_of_variable env id = + Termops.on_judgment EConstr.of_constr (judge_of_variable env id) + +let judge_of_projection env sigma p cj = + let pb = lookup_projection p env in + let (ind,u), args = + try find_mrectype env sigma cj.uj_type + with Not_found -> error_case_not_inductive env sigma cj + in + let args = List.map EConstr.of_constr args in + let ty = EConstr.of_constr (CVars.subst_instance_constr u pb.Declarations.proj_type) in + let ty = substl (cj.uj_val :: List.rev args) ty in + {uj_val = EConstr.mkProj (p,cj.uj_val); + uj_type = ty} + +let judge_of_abstraction env name var j = + { uj_val = mkLambda (name, var.utj_val, j.uj_val); + uj_type = mkProd (name, var.utj_val, j.uj_type) } + +let judge_of_product env name t1 t2 = + let s = sort_of_product env t1.utj_type t2.utj_type in + { uj_val = mkProd (name, t1.utj_val, t2.utj_val); + uj_type = mkSort s } + +let judge_of_letin env name defj typj j = + { uj_val = mkLetIn (name, defj.uj_val, typj.utj_val, j.uj_val) ; + uj_type = subst1 defj.uj_val j.uj_type } + (* cstr must be in n.f. w.r.t. evars and execute returns a judgement where both the term and type are in n.f. *) let rec execute env evdref cstr = @@ -190,13 +263,13 @@ let rec execute env evdref cstr = let cstr = EConstr.of_constr (whd_evar !evdref (EConstr.Unsafe.to_constr cstr)) in match EConstr.kind !evdref cstr with | Meta n -> - { uj_val = EConstr.Unsafe.to_constr cstr; uj_type = meta_type !evdref n } + { uj_val = cstr; uj_type = EConstr.of_constr (meta_type !evdref n) } | Evar ev -> let ty = EConstr.existential_type !evdref ev in let jty = execute env evdref ty in let jty = e_assumption_of_judgment env evdref jty in - { uj_val = EConstr.Unsafe.to_constr cstr; uj_type = EConstr.Unsafe.to_constr jty } + { uj_val = cstr; uj_type = jty } | Rel n -> judge_of_relative env n @@ -239,7 +312,7 @@ let rec execute env evdref cstr = | Proj (p, c) -> let cj = execute env evdref c in - judge_of_projection env p (Evarutil.j_nf_evar !evdref cj) + judge_of_projection env !evdref p cj | App (f,args) -> let jl = execute_array env evdref args in @@ -248,13 +321,11 @@ let rec execute env evdref cstr = | Ind ind when Environ.template_polymorphic_pind ind env -> (* Sort-polymorphism of inductive types *) make_judge f - (inductive_type_knowing_parameters env ind - (Evarutil.jv_nf_evar !evdref jl)) + (inductive_type_knowing_parameters env !evdref ind jl) | Const cst when Environ.template_polymorphic_pconstant cst env -> (* Sort-polymorphism of inductive types *) make_judge f - (constant_type_knowing_parameters env cst - (Evarutil.jv_nf_evar !evdref jl)) + (constant_type_knowing_parameters env !evdref cst jl) | _ -> execute env evdref f in @@ -263,14 +334,14 @@ let rec execute env evdref cstr = | Lambda (name,c1,c2) -> let j = execute env evdref c1 in let var = e_type_judgment env evdref j in - let env1 = push_rel (LocalAssum (name, var.utj_val)) env in + let env1 = push_rel (local_assum (name, var.utj_val)) env in let j' = execute env1 evdref c2 in judge_of_abstraction env1 name var j' | Prod (name,c1,c2) -> let j = execute env evdref c1 in let varj = e_type_judgment env evdref j in - let env1 = push_rel (LocalAssum (name, varj.utj_val)) env in + let env1 = push_rel (local_assum (name, varj.utj_val)) env in let j' = execute env1 evdref c2 in let varj' = e_type_judgment env1 evdref j' in judge_of_product env name varj varj' @@ -280,7 +351,7 @@ let rec execute env evdref cstr = let j2 = execute env evdref c2 in let j2 = e_type_judgment env evdref j2 in let _ = e_judge_of_cast env evdref j1 DEFAULTcast j2 in - let env1 = push_rel (LocalDef (name, j1.uj_val, j2.utj_val)) env in + let env1 = push_rel (local_def (name, j1.uj_val, j2.utj_val)) env in let j3 = execute env1 evdref c3 in judge_of_letin env name j1 j2 j3 @@ -295,7 +366,7 @@ and execute_recdef env evdref (names,lar,vdef) = let lara = Array.map (e_assumption_of_judgment env evdref) larj in let env1 = push_rec_types (names,lara,vdef) env in let vdefj = execute_array env1 evdref vdef in - let vdefv = Array.map (j_val %> EConstr.of_constr) vdefj in + let vdefv = Array.map j_val vdefj in let _ = check_type_fixpoint Loc.ghost env1 evdref names lara vdefj in (names,lara,vdefv) @@ -304,8 +375,8 @@ and execute_array env evdref = Array.map (execute env evdref) let e_check env evdref c t = let env = enrich_env env evdref in let j = execute env evdref c in - if not (Evarconv.e_cumul env evdref (EConstr.of_constr j.uj_type) t) then - error_actual_type env j (EConstr.to_constr !evdref t) + if not (Evarconv.e_cumul env evdref j.uj_type t) then + error_actual_type_core env !evdref j t (* Type of a constr *) @@ -313,7 +384,7 @@ let unsafe_type_of env evd c = let evdref = ref evd in let env = enrich_env env evdref in let j = execute env evdref c in - j.uj_type + EConstr.Unsafe.to_constr j.uj_type (* Sort of a type *) @@ -331,23 +402,23 @@ let type_of ?(refresh=false) env evd c = let j = execute env evdref c in (* side-effect on evdref *) if refresh then - Evarsolve.refresh_universes ~onlyalg:true (Some false) env !evdref (EConstr.of_constr j.uj_type) - else !evdref, j.uj_type + Evarsolve.refresh_universes ~onlyalg:true (Some false) env !evdref j.uj_type + else !evdref, EConstr.Unsafe.to_constr j.uj_type let e_type_of ?(refresh=false) env evdref c = let env = enrich_env env evdref in let j = execute env evdref c in (* side-effect on evdref *) if refresh then - let evd, c = Evarsolve.refresh_universes ~onlyalg:true (Some false) env !evdref (EConstr.of_constr j.uj_type) in + let evd, c = Evarsolve.refresh_universes ~onlyalg:true (Some false) env !evdref j.uj_type in let () = evdref := evd in c - else j.uj_type + else EConstr.Unsafe.to_constr j.uj_type let e_solve_evars env evdref c = let env = enrich_env env evdref in let c = (execute env evdref c).uj_val in (* side-effect on evdref *) - nf_evar !evdref c + nf_evar !evdref (EConstr.Unsafe.to_constr c) let _ = Evarconv.set_solve_evars (fun env evdref c -> EConstr.of_constr (e_solve_evars env evdref c)) diff --git a/pretyping/typing.mli b/pretyping/typing.mli index 3c1c4324d..1fb414906 100644 --- a/pretyping/typing.mli +++ b/pretyping/typing.mli @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Names open Term open Environ open Evd @@ -43,4 +44,11 @@ val check_allowed_sort : env -> evar_map -> pinductive -> EConstr.constr -> ECon (** Raise an error message if bodies have types not unifiable with the expected ones *) val check_type_fixpoint : Loc.t -> env -> evar_map ref -> - Names.Name.t array -> EConstr.types array -> unsafe_judgment array -> unit + Names.Name.t array -> EConstr.types array -> EConstr.unsafe_judgment array -> unit + +val judge_of_prop : EConstr.unsafe_judgment +val judge_of_set : EConstr.unsafe_judgment +val judge_of_abstraction : Environ.env -> Name.t -> + EConstr.unsafe_type_judgment -> EConstr.unsafe_judgment -> EConstr.unsafe_judgment +val judge_of_product : Environ.env -> Name.t -> + EConstr.unsafe_type_judgment -> EConstr.unsafe_type_judgment -> EConstr.unsafe_judgment diff --git a/pretyping/unification.ml b/pretyping/unification.ml index c5c19b49b..1b209fa77 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -120,6 +120,9 @@ let abstract_list_all env evd typ c l = | UserError _ -> error_cannot_find_well_typed_abstraction env evd p l None | Type_errors.TypeError (env',x) -> + (** FIXME: plug back the typing information *) + error_cannot_find_well_typed_abstraction env evd p l None + | Pretype_errors.PretypeError (env',evd,TypingError x) -> error_cannot_find_well_typed_abstraction env evd p l (Some (env',x)) in let typp = EConstr.of_constr typp in evd,(p,typp) @@ -1255,15 +1258,12 @@ let is_mimick_head sigma ts f = | (Rel _|Construct _|Ind _) -> true | _ -> false -let make_judge c t = - make_judge (EConstr.Unsafe.to_constr c) (EConstr.Unsafe.to_constr t) - let try_to_coerce env evd c cty tycon = let j = make_judge c cty in let (evd',j') = inh_conv_coerce_rigid_to true Loc.ghost env evd j tycon in let evd' = Evarconv.consider_remaining_unif_problems env evd' in let evd' = Evd.map_metas_fvalue (nf_evar evd') evd' in - (evd',EConstr.of_constr j'.uj_val) + (evd',j'.uj_val) let w_coerce_to_type env evd c cty mvty = let evd,tycon = pose_all_metas_as_evars env evd mvty in diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 2d621e97c..956be88c8 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -669,12 +669,14 @@ let evar_of_binder holes = function user_err (str "No such binder.") let define_with_type sigma env ev c = + let c = EConstr.of_constr c in let t = Retyping.get_type_of env sigma (EConstr.of_constr ev) in - let ty = Retyping.get_type_of env sigma (EConstr.of_constr c) in + let ty = Retyping.get_type_of env sigma c in + let ty = EConstr.of_constr ty in let j = Environ.make_judge c ty in let (sigma, j) = Coercion.inh_conv_coerce_to true (Loc.ghost) env sigma j (EConstr.of_constr t) in let (ev, _) = destEvar ev in - let sigma = Evd.define ev j.Environ.uj_val sigma in + let sigma = Evd.define ev (EConstr.Unsafe.to_constr j.Environ.uj_val) sigma in sigma let solve_evar_clause env sigma hyp_only clause = function diff --git a/proofs/refine.ml b/proofs/refine.ml index 0ed74c9b3..067764c00 100644 --- a/proofs/refine.ml +++ b/proofs/refine.ml @@ -133,7 +133,9 @@ let refine ?(unsafe = true) f = (** Useful definitions *) let with_type env evd c t = - let my_type = Retyping.get_type_of env evd (EConstr.of_constr c) in + let c = EConstr.of_constr c in + let my_type = Retyping.get_type_of env evd c in + let my_type = EConstr.of_constr my_type in let j = Environ.make_judge c my_type in let (evd,j') = Coercion.inh_conv_coerce_to true (Loc.ghost) env evd j (EConstr.of_constr t) @@ -147,6 +149,7 @@ let refine_casted ?unsafe f = Proofview.Goal.enter { enter = begin fun gl -> let f = { run = fun h -> let Sigma (c, h, p) = f.run h in let sigma, c = with_type env (Sigma.to_evar_map h) c concl in + let c = EConstr.Unsafe.to_constr c in Sigma (c, Sigma.Unsafe.of_evar_map sigma, p) } in refine ?unsafe f diff --git a/proofs/refine.mli b/proofs/refine.mli index 3d140f036..4158e446c 100644 --- a/proofs/refine.mli +++ b/proofs/refine.mli @@ -36,7 +36,7 @@ val refine_one : ?unsafe:bool -> ('a * Constr.t) Sigma.run -> 'a tactic (** {7 Helper functions} *) val with_type : Environ.env -> Evd.evar_map -> - Term.constr -> Term.types -> Evd.evar_map * Term.constr + Term.constr -> Term.types -> Evd.evar_map * EConstr.constr (** [with_type env sigma c t] ensures that [c] is of type [t] inserting a coercion if needed. *) diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml index 789028ac1..9580fdbfc 100644 --- a/tactics/contradiction.ml +++ b/tactics/contradiction.ml @@ -30,7 +30,7 @@ let absurd c = let sigma = Sigma.to_evar_map sigma in let j = Retyping.get_judgment_of env sigma (EConstr.of_constr c) in let sigma, j = Coercion.inh_coerce_to_sort Loc.ghost env sigma j in - let t = j.Environ.utj_val in + let t = EConstr.Unsafe.to_constr j.Environ.utj_val in let tac = Tacticals.New.tclTHENLIST [ elim_type (build_coq_False ()); diff --git a/toplevel/explainErr.ml b/toplevel/explainErr.ml index 17897460c..414087718 100644 --- a/toplevel/explainErr.ml +++ b/toplevel/explainErr.ml @@ -63,6 +63,7 @@ let process_vernac_interp_error with_header exn = match fst exn with mt() in wrap_vernac_error with_header exn (str "Universe inconsistency" ++ msg ++ str ".") | TypeError(ctx,te) -> + let te = Himsg.map_ptype_error EConstr.of_constr te in wrap_vernac_error with_header exn (Himsg.explain_type_error ctx Evd.empty te) | PretypeError(ctx,sigma,te) -> wrap_vernac_error with_header exn (Himsg.explain_pretype_error ctx sigma te) diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index 20cda947a..6e63a71fd 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -83,6 +83,8 @@ let rec contract3' env a b c = function (** Ad-hoc reductions *) +let to_unsafe_judgment j = on_judgment EConstr.Unsafe.to_constr j + let j_nf_betaiotaevar sigma j = { uj_val = Evarutil.nf_evar sigma j.uj_val; uj_type = Reductionops.nf_betaiota sigma (EConstr.of_constr j.uj_type) } @@ -170,6 +172,7 @@ let explain_unbound_var env v = let explain_not_type env sigma j = let j = Evarutil.j_nf_evar sigma j in + let j = to_unsafe_judgment j in let pe = pr_ne_context_of (str "In environment") env sigma in let pc,pt = pr_ljudge_env env sigma j in pe ++ str "The term" ++ brk(1,1) ++ pc ++ spc () ++ @@ -177,6 +180,7 @@ let explain_not_type env sigma j = str "which should be Set, Prop or Type." let explain_bad_assumption env sigma j = + let j = to_unsafe_judgment j in let pe = pr_ne_context_of (str "In environment") env sigma in let pc,pt = pr_ljudge_env env sigma j in pe ++ str "Cannot declare a variable or hypothesis over the term" ++ @@ -184,6 +188,7 @@ let explain_bad_assumption env sigma j = str "because this term is not a type." let explain_reference_variables id c = + let c = EConstr.Unsafe.to_constr c in (* c is intended to be a global reference *) let pc = pr_global (Globnames.global_of_constr c) in pc ++ strbrk " depends on the variable " ++ pr_id id ++ @@ -202,6 +207,8 @@ let pr_puniverses f env (c,u) = else mt()) let explain_elim_arity env sigma ind sorts c pj okinds = + let c = EConstr.Unsafe.to_constr c in + let pj = to_unsafe_judgment pj in let env = make_all_name_different env in let pi = pr_inductive env (fst ind) in let pc = pr_lconstr_env env sigma c in @@ -237,6 +244,7 @@ let explain_elim_arity env sigma ind sorts c pj okinds = let explain_case_not_inductive env sigma cj = let cj = Evarutil.j_nf_evar sigma cj in + let cj = to_unsafe_judgment cj in let env = make_all_name_different env in let pc = pr_lconstr_env env sigma cj.uj_val in let pct = pr_lconstr_env env sigma cj.uj_type in @@ -250,6 +258,7 @@ let explain_case_not_inductive env sigma cj = let explain_number_branches env sigma cj expn = let cj = Evarutil.j_nf_evar sigma cj in + let cj = to_unsafe_judgment cj in let env = make_all_name_different env in let pc = pr_lconstr_env env sigma cj.uj_val in let pct = pr_lconstr_env env sigma cj.uj_type in @@ -258,6 +267,9 @@ let explain_number_branches env sigma cj expn = str "expects " ++ int expn ++ str " branches." let explain_ill_formed_branch env sigma c ci actty expty = + let c = EConstr.Unsafe.to_constr c in + let actty = EConstr.Unsafe.to_constr actty in + let expty = EConstr.Unsafe.to_constr expty in let simp t = Reduction.nf_betaiota env (Evarutil.nf_evar sigma t) in let c = Evarutil.nf_evar sigma c in let env = make_all_name_different env in @@ -270,6 +282,8 @@ let explain_ill_formed_branch env sigma c ci actty expty = str "which should be" ++ brk(1,1) ++ pe ++ str "." let explain_generalization env sigma (name,var) j = + let var = EConstr.Unsafe.to_constr var in + let j = to_unsafe_judgment j in let pe = pr_ne_context_of (str "In environment") env sigma in let pv = pr_ltype_env env sigma var in let (pc,pt) = pr_ljudge_env (push_rel_assum (name,EConstr.of_constr var) env) sigma j in @@ -343,6 +357,8 @@ let explain_unification_error env sigma p1 p2 = function prlist_with_sep pr_semicolon (fun x -> x) l ++ str ")" let explain_actual_type env sigma j t reason = + let j = to_unsafe_judgment j in + let t = EConstr.Unsafe.to_constr t in let env = make_all_name_different env in let j = j_nf_betaiotaevar sigma j in let t = Reductionops.nf_betaiota sigma (EConstr.of_constr t) in @@ -359,10 +375,14 @@ let explain_actual_type env sigma j t reason = ppreason ++ str ".") let explain_cant_apply_bad_type env sigma (n,exptyp,actualtyp) rator randl = + let exptyp = EConstr.Unsafe.to_constr exptyp in + let actualtyp = EConstr.Unsafe.to_constr actualtyp in + let randl = Array.map to_unsafe_judgment randl in let randl = jv_nf_betaiotaevar sigma randl in let exptyp = Evarutil.nf_evar sigma exptyp in let actualtyp = Reductionops.nf_betaiota sigma (EConstr.of_constr actualtyp) in let rator = Evarutil.j_nf_evar sigma rator in + let rator = to_unsafe_judgment rator in let env = make_all_name_different env in let actualtyp, exptyp = pr_explicit env sigma actualtyp exptyp in let nargs = Array.length randl in @@ -388,7 +408,9 @@ let explain_cant_apply_bad_type env sigma (n,exptyp,actualtyp) rator randl = let explain_cant_apply_not_functional env sigma rator randl = let randl = Evarutil.jv_nf_evar sigma randl in + let randl = Array.map to_unsafe_judgment randl in let rator = Evarutil.j_nf_evar sigma rator in + let rator = to_unsafe_judgment rator in let env = make_all_name_different env in let nargs = Array.length randl in (* let pe = pr_ne_context_of (str "in environment") env sigma in*) @@ -424,6 +446,7 @@ let explain_not_product env sigma c = (* TODO: use the names *) (* (co)fixpoints *) let explain_ill_formed_rec_body env sigma err names i fixenv vdefj = + let pr_lconstr_env env sigma c = pr_lconstr_env env sigma (EConstr.Unsafe.to_constr c) in let prt_name i = match names.(i) with Name id -> str "Recursive definition of " ++ pr_id id @@ -511,6 +534,8 @@ let explain_ill_formed_rec_body env sigma err names i fixenv vdefj = let explain_ill_typed_rec_body env sigma i names vdefj vargs = let vdefj = Evarutil.jv_nf_evar sigma vdefj in + let vargs = Array.map EConstr.Unsafe.to_constr vargs in + let vdefj = Array.map to_unsafe_judgment vdefj in let vargs = Array.map (Evarutil.nf_evar sigma) vargs in let env = make_all_name_different env in let pvd = pr_lconstr_env env sigma vdefj.(i).uj_val in @@ -522,6 +547,7 @@ let explain_ill_typed_rec_body env sigma i names vdefj vargs = str "while it should be" ++ spc () ++ pv ++ str "." let explain_cant_find_case_type env sigma c = + let c = EConstr.Unsafe.to_constr c in let c = Evarutil.nf_evar sigma c in let env = make_all_name_different env in let pe = pr_lconstr_env env sigma c in @@ -822,14 +848,18 @@ let explain_pretype_error env sigma err = match err with | CantFindCaseType c -> explain_cant_find_case_type env sigma c | ActualTypeNotCoercible (j,t,e) -> + let j = to_unsafe_judgment j in + let t = EConstr.Unsafe.to_constr t in let {uj_val = c; uj_type = actty} = j in let (env, c, actty, expty), e = contract3' env c actty t e in let j = {uj_val = c; uj_type = actty} in - explain_actual_type env sigma j expty (Some e) + explain_actual_type env sigma (on_judgment EConstr.of_constr j) (EConstr.of_constr expty) (Some e) | UnifOccurCheck (ev,rhs) -> explain_occur_check env sigma ev rhs | UnsolvableImplicit (evk,exp) -> explain_unsolvable_implicit env sigma evk exp | VarNotFound id -> explain_var_not_found env id | UnexpectedType (actual,expect) -> + let actual = EConstr.Unsafe.to_constr actual in + let expect = EConstr.Unsafe.to_constr expect in let env, actual, expect = contract2 env actual expect in explain_unexpected_type env sigma actual expect | NotProduct c -> explain_not_product env sigma c @@ -1289,8 +1319,48 @@ let explain_pattern_matching_error env sigma = function | CannotInferPredicate typs -> explain_cannot_infer_predicate env sigma typs +let map_pguard_error f = function +| NotEnoughAbstractionInFixBody -> NotEnoughAbstractionInFixBody +| RecursionNotOnInductiveType c -> RecursionNotOnInductiveType (f c) +| RecursionOnIllegalTerm (n, (env, c), l1, l2) -> RecursionOnIllegalTerm (n, (env, f c), l1, l2) +| NotEnoughArgumentsForFixCall n -> NotEnoughArgumentsForFixCall n +| CodomainNotInductiveType c -> CodomainNotInductiveType (f c) +| NestedRecursiveOccurrences -> NestedRecursiveOccurrences +| UnguardedRecursiveCall c -> UnguardedRecursiveCall (f c) +| RecCallInTypeOfAbstraction c -> RecCallInTypeOfAbstraction (f c) +| RecCallInNonRecArgOfConstructor c -> RecCallInNonRecArgOfConstructor (f c) +| RecCallInTypeOfDef c -> RecCallInTypeOfDef (f c) +| RecCallInCaseFun c -> RecCallInCaseFun (f c) +| RecCallInCaseArg c -> RecCallInCaseArg (f c) +| RecCallInCasePred c -> RecCallInCasePred (f c) +| NotGuardedForm c -> NotGuardedForm (f c) +| ReturnPredicateNotCoInductive c -> ReturnPredicateNotCoInductive (f c) + +let map_ptype_error f = function +| UnboundRel n -> UnboundRel n +| UnboundVar id -> UnboundVar id +| NotAType j -> NotAType (on_judgment f j) +| BadAssumption j -> BadAssumption (on_judgment f j) +| ReferenceVariables (id, c) -> ReferenceVariables (id, f c) +| ElimArity (pi, dl, c, j, ar) -> ElimArity (pi, dl, f c, on_judgment f j, ar) +| CaseNotInductive j -> CaseNotInductive (on_judgment f j) +| WrongCaseInfo (pi, ci) -> WrongCaseInfo (pi, ci) +| NumberBranches (j, n) -> NumberBranches (on_judgment f j, n) +| IllFormedBranch (c, pc, t1, t2) -> IllFormedBranch (f c, pc, f t1, f t2) +| Generalization ((na, t), j) -> Generalization ((na, f t), on_judgment f j) +| ActualType (j, t) -> ActualType (on_judgment f j, f t) +| CantApplyBadType ((n, c1, c2), j, vj) -> + CantApplyBadType ((n, f c1, f c2), on_judgment f j, Array.map (on_judgment f) vj) +| CantApplyNonFunctional (j, jv) -> CantApplyNonFunctional (on_judgment f j, Array.map (on_judgment f) jv) +| IllFormedRecBody (ge, na, n, env, jv) -> + IllFormedRecBody (map_pguard_error f ge, na, n, env, Array.map (on_judgment f) jv) +| IllTypedRecBody (n, na, jv, t) -> + IllTypedRecBody (n, na, Array.map (on_judgment f) jv, Array.map f t) +| UnsatisfiedConstraints g -> UnsatisfiedConstraints g + let explain_reduction_tactic_error = function | Tacred.InvalidAbstraction (env,sigma,c,(env',e)) -> + let e = map_ptype_error EConstr.of_constr e in let c = EConstr.to_constr sigma c in str "The abstracted term" ++ spc () ++ quote (pr_goal_concl_style_env env sigma c) ++ diff --git a/toplevel/himsg.mli b/toplevel/himsg.mli index ced54fd27..6915ea921 100644 --- a/toplevel/himsg.mli +++ b/toplevel/himsg.mli @@ -40,3 +40,6 @@ val explain_module_error : Modops.module_typing_error -> std_ppcmds val explain_module_internalization_error : Modintern.module_internalization_error -> std_ppcmds + +val map_pguard_error : ('c -> 'd) -> 'c pguard_error -> 'd pguard_error +val map_ptype_error : ('c -> 'd) -> ('c, 'c) ptype_error -> ('d, 'd) ptype_error diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 01b15407b..3b8c62738 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -1579,7 +1579,8 @@ let vernac_check_may_eval redexp glopt rc = let c = nf c in let j = if Evarutil.has_undefined_evars sigma' (EConstr.of_constr c) then - Evarutil.j_nf_evar sigma' (Retyping.get_judgment_of env sigma' (EConstr.of_constr c)) + let j = Evarutil.j_nf_evar sigma' (Retyping.get_judgment_of env sigma' (EConstr.of_constr c)) in + Termops.on_judgment EConstr.Unsafe.to_constr j else (* OK to call kernel which does not support evars *) Arguments_renaming.rename_typing env c in |