diff options
Diffstat (limited to 'pretyping/retyping.ml')
| -rw-r--r-- | pretyping/retyping.ml | 99 |
1 files changed, 52 insertions, 47 deletions
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index 5ed6e6051..bb6948767 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -12,23 +12,25 @@ open Util open Term open Inductive open Names -open Reduction +open Reductionops open Environ open Typeops +open Declarations +open Instantiate type metamap = (int * constr) list let outsort env sigma t = match kind_of_term (whd_betadeltaiota env sigma t) with - | IsSort s -> s + | Sort s -> s | _ -> anomaly "Retyping: found a type of type which is not a sort" let rec subst_type env sigma typ = function | [] -> typ | h::rest -> match kind_of_term (whd_betadeltaiota env sigma typ) with - | IsProd (na,c1,c2) -> - subst_type (push_rel_assum (na,c1) env) sigma (subst1 h c2) rest + | Prod (na,c1,c2) -> + subst_type (push_rel (na,None,c1) env) sigma (subst1 h c2) rest | _ -> anomaly "Non-functional construction" (* Si ft est le type d'un terme f, lequel est appliqué à args, *) @@ -39,71 +41,74 @@ let rec subst_type env sigma typ = function let sort_of_atomic_type env sigma ft args = let rec concl_of_arity env ar = match kind_of_term (whd_betadeltaiota env sigma ar) with - | IsProd (na, t, b) -> concl_of_arity (push_rel_assum (na,t) env) b - | IsSort s -> s + | Prod (na, t, b) -> concl_of_arity (push_rel (na,None,t) env) b + | Sort s -> s | _ -> outsort env sigma (subst_type env sigma ft (Array.to_list args)) in concl_of_arity env ft let typeur sigma metamap = let rec type_of env cstr= match kind_of_term cstr with - | IsMeta n -> + | Meta n -> (try strip_outer_cast (List.assoc n metamap) with Not_found -> anomaly "type_of: this is not a well-typed term") - | IsRel n -> lift n (body_of_type (snd (lookup_rel_type n env))) - | IsVar id -> - (try body_of_type (snd (lookup_named id env)) - with Not_found -> - anomaly ("type_of: variable "^(string_of_id id)^" unbound")) - | IsConst c -> body_of_type (type_of_constant env sigma c) - | IsEvar ev -> type_of_existential env sigma ev - | IsMutInd ind -> body_of_type (type_of_inductive env sigma ind) - | IsMutConstruct cstr -> body_of_type (type_of_constructor env sigma cstr) - | IsMutCase (_,p,c,lf) -> - let IndType (indf,realargs) = - try find_rectype env sigma (type_of env c) + | Rel n -> + let (_,_,ty) = lookup_rel n env in + lift n (body_of_type ty) + | Var id -> + let (_,_,ty) = lookup_named id env in + (try body_of_type ty + with Not_found -> + anomaly ("type_of: variable "^(string_of_id id)^" unbound")) + | Const c -> + let cb = lookup_constant c env in + body_of_type cb.const_type + | Evar ev -> existential_type sigma ev + | Ind ind -> body_of_type (type_of_inductive env ind) + | Construct cstr -> body_of_type (type_of_constructor env cstr) + | Case (_,p,c,lf) -> + (* TODO: could avoid computing the type of branches *) + let i = + try find_rectype env (type_of env c) with Induc -> anomaly "type_of: Bad recursive type" in - let (aritysign,_) = get_arity indf in - let (psign,_) = splay_prod env sigma (type_of env p) in - let al = - if List.length psign > List.length aritysign - then realargs@[c] else realargs in - whd_betadeltaiota env sigma (applist (p,al)) - | IsLambda (name,c1,c2) -> - mkProd (name, c1, type_of (push_rel_assum (name,c1) env) c2) - | IsLetIn (name,b,c1,c2) -> - subst1 b (type_of (push_rel_def (name,b,c1) env) c2) - | IsFix ((_,i),(_,tys,_)) -> tys.(i) - | IsCoFix (i,(_,tys,_)) -> tys.(i) - | IsApp(f,args)-> + let pj = { uj_val = p; uj_type = type_of env p } in + let (_,ty,_) = type_case_branches env i pj c in + ty + | Lambda (name,c1,c2) -> + mkProd (name, c1, type_of (push_rel (name,None,c1) env) c2) + | LetIn (name,b,c1,c2) -> + subst1 b (type_of (push_rel (name,Some b,c1) env) c2) + | Fix ((_,i),(_,tys,_)) -> tys.(i) + | CoFix (i,(_,tys,_)) -> tys.(i) + | App(f,args)-> strip_outer_cast (subst_type env sigma (type_of env f) (Array.to_list args)) - | IsCast (c,t) -> t - | IsSort _ | IsProd (_,_,_) | IsMutInd _ -> mkSort (sort_of env cstr) + | Cast (c,t) -> t + | Sort _ | Prod (_,_,_) | Ind _ -> mkSort (sort_of env cstr) and sort_of env t = match kind_of_term t with - | IsCast (c,s) when isSort s -> destSort s - | IsSort (Prop c) -> type_0 - | IsSort (Type u) -> Type (fst (Univ.super u)) - | IsProd (name,t,c2) -> - (match (sort_of (push_rel_assum (name,t) env) c2) with + | Cast (c,s) when isSort s -> destSort s + | Sort (Prop c) -> type_0 + | Sort (Type u) -> Type (fst (Univ.super u)) + | Prod (name,t,c2) -> + (match (sort_of (push_rel (name,None,t) env) c2) with | Prop _ as s -> s | Type u2 as s -> s (*Type Univ.dummy_univ*)) - | IsApp(f,args) -> sort_of_atomic_type env sigma (type_of env f) args - | IsLambda _ | IsFix _ | IsMutConstruct _ -> + | App(f,args) -> sort_of_atomic_type env sigma (type_of env f) args + | Lambda _ | Fix _ | Construct _ -> anomaly "sort_of: Not a type (1)" | _ -> outsort env sigma (type_of env t) and sort_family_of env t = match kind_of_term (whd_betadeltaiota env sigma t) with - | IsCast (c,s) when isSort s -> family_of_sort (destSort s) - | IsSort (Prop c) -> InType - | IsSort (Type u) -> InType - | IsProd (name,t,c2) -> sort_family_of (push_rel_assum (name,t) env) c2 - | IsApp(f,args) -> + | Cast (c,s) when isSort s -> family_of_sort (destSort s) + | Sort (Prop c) -> InType + | Sort (Type u) -> InType + | Prod (name,t,c2) -> sort_family_of (push_rel (name,None,t) env) c2 + | App(f,args) -> family_of_sort (sort_of_atomic_type env sigma (type_of env f) args) - | IsLambda _ | IsFix _ | IsMutConstruct _ -> + | Lambda _ | Fix _ | Construct _ -> anomaly "sort_of: Not a type (1)" | _ -> family_of_sort (outsort env sigma (type_of env t)) |