diff options
Diffstat (limited to 'pretyping/retyping.ml')
| -rw-r--r-- | pretyping/retyping.ml | 52 |
1 files changed, 30 insertions, 22 deletions
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index 428a7306..ecead438 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: retyping.ml 8871 2006-05-28 16:46:48Z herbelin $ *) +(* $Id: retyping.ml 9314 2006-10-29 20:11:08Z herbelin $ *) open Util open Term @@ -17,6 +17,7 @@ open Reductionops open Environ open Typeops open Declarations +open Termops let rec subst_type env sigma typ = function | [] -> typ @@ -38,6 +39,11 @@ let sort_of_atomic_type env sigma ft args = | _ -> decomp_sort env sigma (subst_type env sigma ft (Array.to_list args)) in concl_of_arity env ft +let type_of_var env id = + try let (_,_,ty) = lookup_named id env in ty + with Not_found -> + anomaly ("type_of: variable "^(string_of_id id)^" unbound") + let typeur sigma metamap = let rec type_of env cstr= match kind_of_term cstr with @@ -47,18 +53,11 @@ let typeur sigma metamap = | Rel n -> let (_,_,ty) = lookup_rel n env in lift n ty - | Var id -> - (try - let (_,_,ty) = lookup_named id env in - 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 + | Var id -> type_of_var env id + | Const cst -> Typeops.type_of_constant env cst | Evar ev -> Evd.existential_type sigma ev - | Ind ind -> body_of_type (type_of_inductive env ind) - | Construct cstr -> body_of_type (type_of_constructor env cstr) + | Ind ind -> type_of_inductive env ind + | Construct cstr -> type_of_constructor env cstr | Case (_,p,c,lf) -> let Inductiveops.IndType(_,realargs) = try Inductiveops.find_rectype env sigma (type_of env c) @@ -73,8 +72,8 @@ let typeur sigma metamap = 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) when isInd f -> - let t = type_of_inductive_knowing_parameters env (destInd f) args in + | App(f,args) when isGlobalRef 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)) | App(f,args) -> strip_outer_cast @@ -97,8 +96,8 @@ let typeur sigma metamap = | Prop Pos, (Type u2) -> Type (Univ.sup Univ.base_univ u2) | Prop Null, (Type _ as s) -> s | Type u1, Type u2 -> Type (Univ.sup u1 u2)) - | App(f,args) when isInd f -> - let t = type_of_inductive_knowing_parameters env (destInd f) args in + | App(f,args) when isGlobalRef 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 _ -> @@ -117,18 +116,27 @@ let typeur sigma metamap = anomaly "sort_of: Not a type (1)" | _ -> family_of_sort (decomp_sort env sigma (type_of env t)) - and type_of_inductive_knowing_parameters env ind args = - let (_,mip) = lookup_mind_specif env ind in + and type_of_global_reference_knowing_parameters env c args = let argtyps = Array.map (fun c -> nf_evar sigma (type_of env c)) args in - Inductive.type_of_inductive_knowing_parameters env mip argtyps + match kind_of_term c with + | Ind ind -> + let (_,mip) = lookup_mind_specif env ind in + Inductive.type_of_inductive_knowing_parameters env mip argtyps + | Const cst -> + let t = constant_type env cst in + Typeops.type_of_constant_knowing_parameters env t argtyps + | 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_inductive_knowing_parameters + in type_of, sort_of, sort_family_of, + type_of_global_reference_knowing_parameters let get_type_of env sigma c = let f,_,_,_ = typeur sigma [] in f env c let get_sort_of env sigma t = let _,f,_,_ = typeur sigma [] in f env t let get_sort_family_of env sigma c = let _,_,f,_ = typeur sigma [] in f env c -let type_of_inductive_knowing_parameters env sigma ind args = - let _,_,_,f = typeur sigma [] in f env ind args +let type_of_global_reference_knowing_parameters env sigma c args = + let _,_,_,f = typeur sigma [] in f env c args let get_type_of_with_meta env sigma metamap = let f,_,_,_ = typeur sigma metamap in f env |