From 208a0f7bfa5249f9795e6e225f309cbe715c0fad Mon Sep 17 00:00:00 2001
From: Samuel Mimram <smimram@debian.org>
Date: Tue, 21 Nov 2006 21:38:49 +0000
Subject: Imported Upstream version 8.1~gamma

---
 pretyping/retyping.ml | 52 +++++++++++++++++++++++++++++----------------------
 1 file changed, 30 insertions(+), 22 deletions(-)

(limited to 'pretyping/retyping.ml')

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
-- 
cgit v1.2.3