diff options
Diffstat (limited to 'pretyping/retyping.ml')
| -rw-r--r-- | pretyping/retyping.ml | 165 |
1 files changed, 87 insertions, 78 deletions
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index 98b36fb9..3582b644 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -1,25 +1,32 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Pp open CErrors open Util open Term -open Vars +open Constr open Inductive open Inductiveops open Names open Reductionops open Environ open Termops +open EConstr +open Vars open Arguments_renaming open Context.Rel.Declaration +module RelDecl = Context.Rel.Declaration +module NamedDecl = Context.Named.Declaration + type retype_error = | NotASort | NotAnArity @@ -44,14 +51,14 @@ let retype_error re = raise (RetypeError re) let anomaly_on_error f x = try f x - with RetypeError e -> anomaly ~label:"retyping" (print_retype_error e) + with RetypeError e -> anomaly ~label:"retyping" (print_retype_error e ++ str ".") let get_type_from_constraints env sigma t = - if isEvar (fst (decompose_app t)) then + if isEvar sigma (fst (decompose_app_vect sigma t)) then match List.map_filter (fun (pbty,env,t1,t2) -> - if is_fconv Reduction.CONV env sigma t t1 then Some t2 - else if is_fconv Reduction.CONV env sigma t t2 then Some t1 + if is_fconv Reduction.CONV env sigma t (EConstr.of_constr t1) then Some t2 + else if is_fconv Reduction.CONV env sigma t (EConstr.of_constr t2) then Some t1 else None) (snd (Evd.extract_all_conv_pbs sigma)) with @@ -62,7 +69,7 @@ let get_type_from_constraints env sigma t = let rec subst_type env sigma typ = function | [] -> typ | h::rest -> - match kind_of_term (whd_all env sigma typ) with + match EConstr.kind sigma (whd_all env sigma typ) with | Prod (na,c1,c2) -> subst_type env sigma (subst1 h c2) rest | _ -> retype_error NonFunctionalConstruction @@ -71,49 +78,50 @@ let rec subst_type env sigma typ = function let sort_of_atomic_type env sigma ft args = let rec concl_of_arity env n ar args = - match kind_of_term (whd_all env sigma ar), args with + match EConstr.kind sigma (whd_all env sigma ar), args with | Prod (na, t, b), h::l -> concl_of_arity (push_rel (LocalDef (na, lift n h, t)) env) (n + 1) b l - | Sort s, [] -> s + | Sort s, [] -> ESorts.kind sigma s | _ -> retype_error NotASort in concl_of_arity env 0 ft (Array.to_list args) let type_of_var env id = - let open Context.Named.Declaration in - try get_type (lookup_named id env) + try NamedDecl.get_type (lookup_named id env) with Not_found -> retype_error (BadVariable id) let decomp_sort env sigma t = - match kind_of_term (whd_all env sigma t) with - | Sort s -> s + match EConstr.kind sigma (whd_all env sigma t) with + | Sort s -> ESorts.kind sigma s | _ -> retype_error NotASort +let destSort sigma s = ESorts.kind sigma (destSort sigma s) + let retype ?(polyprop=true) sigma = let rec type_of env cstr = - match kind_of_term cstr with + match EConstr.kind sigma cstr with | Meta n -> - (try strip_outer_cast (Evd.meta_ftype sigma n).Evd.rebus + (try strip_outer_cast sigma (EConstr.of_constr (Evd.meta_ftype sigma n).Evd.rebus) with Not_found -> retype_error (BadMeta n)) | Rel n -> - let ty = get_type (lookup_rel n env) in + let ty = RelDecl.get_type (lookup_rel n env) in lift n ty | Var id -> type_of_var env id - | Const cst -> rename_type_of_constant env cst - | Evar ev -> Evd.existential_type sigma ev - | Ind ind -> rename_type_of_inductive env ind - | Construct cstr -> rename_type_of_constructor env cstr + | Const (cst, u) -> EConstr.of_constr (rename_type_of_constant env (cst, EInstance.kind sigma u)) + | Evar ev -> existential_type sigma ev + | Ind (ind, u) -> EConstr.of_constr (rename_type_of_inductive env (ind, EInstance.kind sigma u)) + | Construct (cstr, u) -> EConstr.of_constr (rename_type_of_constructor env (cstr, EInstance.kind sigma u)) | Case (_,p,c,lf) -> let Inductiveops.IndType(indf,realargs) = let t = type_of env c in try Inductiveops.find_rectype env sigma t with Not_found -> try - let t = get_type_from_constraints env sigma t in + let t = EConstr.of_constr (get_type_from_constraints env sigma t) in Inductiveops.find_rectype env sigma t with Not_found -> retype_error BadRecursiveType in let n = inductive_nrealdecls_env env (fst (fst (dest_ind_family indf))) in let t = betazetaevar_applist sigma n p realargs in - (match kind_of_term (whd_all env sigma (type_of env t)) with + (match EConstr.kind sigma (whd_all env sigma (type_of env t)) with | Prod _ -> whd_beta sigma (applist (t, [c])) | _ -> t) | Lambda (name,c1,c2) -> @@ -122,25 +130,28 @@ let retype ?(polyprop=true) sigma = subst1 b (type_of (push_rel (LocalDef (name,b,c1)) env) c2) | Fix ((_,i),(_,tys,_)) -> tys.(i) | CoFix (i,(_,tys,_)) -> tys.(i) - | App(f,args) when is_template_polymorphic env f -> + | App(f,args) when is_template_polymorphic env sigma f -> let t = type_of_global_reference_knowing_parameters env f args in - strip_outer_cast (subst_type env sigma t (Array.to_list args)) + strip_outer_cast sigma (subst_type env sigma t (Array.to_list args)) | App(f,args) -> - strip_outer_cast + strip_outer_cast sigma (subst_type env sigma (type_of env f) (Array.to_list args)) | Proj (p,c) -> let ty = type_of env c in - (try + EConstr.of_constr (try Inductiveops.type_of_projection_knowing_arg env sigma p c ty with Invalid_argument _ -> retype_error BadRecursiveType) | Cast (c,_, t) -> t | Sort _ | Prod _ -> mkSort (sort_of env cstr) and sort_of env t = - match kind_of_term t with - | Cast (c,_, s) when isSort s -> destSort s - | Sort (Prop c) -> type1_sort - | Sort (Type u) -> Type (Univ.super u) + match EConstr.kind sigma t with + | Cast (c,_, s) when isSort sigma s -> destSort sigma s + | Sort s -> + begin match ESorts.kind sigma s with + | Prop _ -> Sorts.type1 + | Type u -> Type (Univ.super u) + end | Prod (name,t,c2) -> (match (sort_of env t, sort_of (push_rel (LocalAssum (name,t)) env) c2) with | _, (Prop Null as s) -> s @@ -150,69 +161,67 @@ let retype ?(polyprop=true) sigma = | Prop Pos, (Type u2) -> Type (Univ.sup Univ.type0_univ u2) | Prop Null, (Type _ as s) -> s | Type u1, Type u2 -> Type (Univ.sup u1 u2)) - | App(f,args) when is_template_polymorphic env f -> + | App(f,args) when is_template_polymorphic env sigma f -> let t = type_of_global_reference_knowing_parameters env f args in sort_of_atomic_type env sigma t args | App(f,args) -> sort_of_atomic_type env sigma (type_of env f) args | Lambda _ | Fix _ | Construct _ -> retype_error NotAType | _ -> decomp_sort env sigma (type_of env t) - and sort_family_of env t = - match kind_of_term t with - | Cast (c,_, s) when isSort s -> family_of_sort (destSort s) - | Sort (Prop c) -> InType - | Sort (Type u) -> InType + and type_of_global_reference_knowing_parameters env c args = + let argtyps = + Array.map (fun c -> lazy (EConstr.to_constr sigma (type_of env c))) args in + match EConstr.kind sigma c with + | Ind (ind, u) -> + let u = EInstance.kind sigma u in + let mip = lookup_mind_specif env ind in + EConstr.of_constr (try Inductive.type_of_inductive_knowing_parameters + ~polyprop env (mip, u) argtyps + with Reduction.NotArity -> retype_error NotAnArity) + | Construct (cstr, u) -> + let u = EInstance.kind sigma u in + EConstr.of_constr (type_of_constructor env (cstr, u)) + | _ -> assert false + + in type_of, sort_of, type_of_global_reference_knowing_parameters + +let get_sort_family_of ?(truncation_style=false) ?(polyprop=true) env sigma t = + let type_of,_,type_of_global_reference_knowing_parameters = retype ~polyprop sigma in + let rec sort_family_of env t = + match EConstr.kind sigma t with + | Cast (c,_, s) when isSort sigma s -> Sorts.family (destSort sigma s) + | Sort _ -> InType | Prod (name,t,c2) -> let s2 = sort_family_of (push_rel (LocalAssum (name,t)) env) c2 in if not (is_impredicative_set env) && s2 == InSet && sort_family_of env t == InType then InType else s2 - | App(f,args) when is_template_polymorphic env f -> + | App(f,args) when is_template_polymorphic env sigma f -> + if truncation_style then InType else let t = type_of_global_reference_knowing_parameters env f args in - family_of_sort (sort_of_atomic_type env sigma t args) + Sorts.family (sort_of_atomic_type env sigma t args) | App(f,args) -> - family_of_sort (sort_of_atomic_type env sigma (type_of env f) args) + Sorts.family (sort_of_atomic_type env sigma (type_of env f) args) | Lambda _ | Fix _ | Construct _ -> retype_error NotAType + | Ind _ when truncation_style && is_template_polymorphic env sigma t -> InType | _ -> - family_of_sort (decomp_sort env sigma (type_of env t)) - - and type_of_global_reference_knowing_parameters env c args = - let argtyps = - Array.map (fun c -> lazy (nf_evar sigma (type_of env c))) args in - match kind_of_term c with - | Ind ind -> - let mip = lookup_mind_specif env (fst ind) in - (try Inductive.type_of_inductive_knowing_parameters - ~polyprop env (mip,snd ind) argtyps - with Reduction.NotArity -> retype_error NotAnArity) - | Const cst -> - (try Typeops.type_of_constant_knowing_parameters_in env cst argtyps - with Reduction.NotArity -> retype_error NotAnArity) - | Var id -> type_of_var env id - | Construct cstr -> type_of_constructor env cstr - | _ -> assert false - - in type_of, sort_of, sort_family_of, - type_of_global_reference_knowing_parameters + Sorts.family (decomp_sort env sigma (type_of env t)) + in sort_family_of env t let get_sort_of ?(polyprop=true) env sigma t = - let _,f,_,_ = retype ~polyprop sigma in anomaly_on_error (f env) t -let get_sort_family_of ?(polyprop=true) env sigma c = - let _,_,f,_ = retype ~polyprop sigma in anomaly_on_error (f env) c + let _,f,_ = retype ~polyprop sigma in anomaly_on_error (f env) t let type_of_global_reference_knowing_parameters env sigma c args = - let _,_,_,f = retype sigma in anomaly_on_error (f env c) args + let _,_,f = retype sigma in anomaly_on_error (f env c) args let type_of_global_reference_knowing_conclusion env sigma c conclty = - let conclty = nf_evar sigma conclty in - match kind_of_term c with + match EConstr.kind sigma c with | Ind (ind,u) -> let spec = Inductive.lookup_mind_specif env ind in - type_of_inductive_knowing_conclusion env sigma (spec,u) conclty - | Const cst -> - let t = constant_type_in env cst in - (* TODO *) - sigma, Typeops.type_of_constant_type_knowing_parameters env t [||] + type_of_inductive_knowing_conclusion env sigma (spec, EInstance.kind sigma u) conclty + | Const (cst, u) -> + let t = constant_type_in env (cst, EInstance.kind sigma u) in + sigma, EConstr.of_constr t | Var id -> sigma, type_of_var env id - | Construct cstr -> sigma, type_of_constructor env cstr + | Construct (cstr, u) -> sigma, EConstr.of_constr (type_of_constructor env (cstr, EInstance.kind sigma u)) | _ -> assert false (* Profiling *) @@ -220,14 +229,14 @@ let type_of_global_reference_knowing_conclusion env sigma c conclty = (* let f,_,_,_ = retype ~polyprop sigma in *) (* if lax then f env c else anomaly_on_error (f env) c *) -(* let get_type_of_key = Profile.declare_profile "get_type_of" *) -(* let get_type_of = Profile.profile5 get_type_of_key get_type_of *) +(* let get_type_of_key = CProfile.declare_profile "get_type_of" *) +(* let get_type_of = CProfile.profile5 get_type_of_key get_type_of *) (* let get_type_of ?(polyprop=true) ?(lax=false) env sigma c = *) (* get_type_of polyprop lax env sigma c *) let get_type_of ?(polyprop=true) ?(lax=false) env sigma c = - let f,_,_,_ = retype ~polyprop sigma in + let f,_,_ = retype ~polyprop sigma in if lax then f env c else anomaly_on_error (f env) c (* Makes an unsafe judgment from a constr *) @@ -239,7 +248,7 @@ let sorts_of_context env evc ctxt = | [] -> env,[] | d :: ctxt -> let env,sorts = aux ctxt in - let s = get_sort_of env evc (get_type d) in + let s = get_sort_of env evc (RelDecl.get_type d) in (push_rel d env,s::sorts) in snd (aux ctxt) |