diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-11-11 00:29:02 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-02-14 17:27:27 +0100 |
| commit | ca993b9e7765ac58f70740818758457c9367b0da (patch) | |
| tree | a813ef9a194638afbb09cefe1d1e2bce113a9d84 | |
| parent | c2855a3387be134d1220f301574b743572a94239 (diff) | |
Making judgment type generic over the type of inner constrs.
This allows to factorize code and prevents the unnecessary use of back and
forth conversions between the various types of terms.
Note that functions from typing may now raise errors as PretypeError rather
than TypeError, because they call the proper wrapper. I think that they were
wrongly calling the kernel because of an overlook of open modules.
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 |