1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
|
(* $Id$ *)
open Util
open Term
open Inductive
open Names
open Generic
open Reduction
open Environ
open Typeops
(* A light version of mind_specif_of_mind *)
type mutind_id = inductive_path * constr array
type mutind =
{fullmind : constr;
mind : mutind_id;
nparams : int;
nconstr : int;
params : constr list;
realargs : constr list;
arity : constr}
(* raise Induc if not an inductive type *)
let try_mutind_of env sigma ty =
let (mind,largs) = find_mrectype env sigma ty in
let mispec = lookup_mind_specif mind env in
let nparams = mis_nparams mispec in
let (params,proper_args) = list_chop nparams largs in
{fullmind = ty;
mind = (let (sp,i,cv) = destMutInd mind in (sp,i),cv);
nparams = nparams;
nconstr = mis_nconstr mispec;
params = params;
realargs = proper_args;
arity = Instantiate.mis_arity mispec}
(******** A light version of type_of *********)
type metamap = (int * constr) list
let rec is_dep_case env sigma (pt,ar) =
match whd_betadeltaiota env sigma pt,whd_betadeltaiota env sigma ar with
DOP2(Prod,_,DLAM(_,t1)),DOP2(Prod,_,DLAM(_,t2)) ->
is_dep_case env sigma (t1,t2)
| DOP2(Prod,_,DLAM(_,_)),ki -> true
| k,ki -> false
let outsort env sigma t =
match whd_betadeltaiota env sigma t with
DOP0(Sort s) -> s
| _ -> anomaly "outsort: Not a sort"
let rec subst_type env sigma typ = function
[] -> typ
| h::rest ->
match whd_betadeltaiota env sigma typ with
DOP2(Prod,c1,DLAM(_,c2)) -> subst_type env sigma (subst1 h c2) rest
| _ -> anomaly "Non-functional construction"
(* Si ft est le type d'un terme f, lequel est appliqu� � args, *)
(* [sort_of_atomic_ty] calcule ft[args] qui doit �tre une sorte *)
(* On suit une m�thode paresseuse, en esp�rant que ft est une arit� *)
(* et sinon on substitue *)
let sort_of_atomic_type env sigma ft args =
let rec concl_of_arity ar =
match whd_betadeltaiota env sigma ar with
| DOP2 (Prod, _, DLAM (_, b)) -> concl_of_arity b
| DOP0 (Sort s) -> s
| _ -> outsort env sigma (subst_type env sigma ft args)
in concl_of_arity ft
let typeur sigma metamap =
let rec type_of env cstr=
match kind_of_term cstr with
IsMeta 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 n env)))
| IsVar id -> body_of_type (snd (lookup_var id env))
| IsAbst _ -> error "No more Abst" (*type_of env (abst_value cstr)*)
| IsConst _ -> (body_of_type (type_of_constant env sigma cstr))
| IsMutInd _ -> (body_of_type (type_of_inductive env sigma cstr))
| IsMutConstruct _ ->
let (typ,kind) = destCast (type_of_constructor env sigma cstr)
in typ
| IsMutCase (_,p,c,lf) ->
let {realargs=args;arity=arity;nparams=n} =
try try_mutind_of env sigma (type_of env c)
with Induc -> anomaly "type_of: Bad inductive" in
let (_,ar) = decomp_n_prod env sigma n arity in
let al =
if is_dep_case env sigma (type_of env p,ar)
then args@[c] else args in
whd_betadeltaiota env sigma (applist (p,al))
| IsLambda (name,c1,c2) ->
let var = make_typed c1 (sort_of env c1) in
mkProd name c1 (type_of (push_rel (name,var) env) c2)
| IsFix (vn,i,lar,lfi,vdef) -> lar.(i)
| IsCoFix (i,lar,lfi,vdef) -> lar.(i)
| IsAppL(f,args)-> strip_outer_cast (subst_type env sigma (type_of env f) args)
| IsCast (c,t) -> t
| IsSort _ | IsProd (_,_,_) | IsMutInd _ -> mkSort (sort_of env cstr)
| _ -> error "type_of: Unexpected constr"
and sort_of env t =
match kind_of_term t with
| IsCast (c,DOP0(Sort s)) -> s
| IsSort (Prop c) -> type_0
| IsSort (Type u) -> Type Univ.dummy_univ
| IsProd (name,t,c2) ->
let var = make_typed t (sort_of env t) in
(match (sort_of (push_rel (name,var) env) c2) with
| Prop _ as s -> s
| Type u2 -> Type Univ.dummy_univ)
| IsAppL(f,args) -> sort_of_atomic_type env sigma (type_of env f) args
| IsLambda _ | IsFix _ | IsMutConstruct _ ->
anomaly "sort_of: Not a type (1)"
| _ -> outsort env sigma (type_of env t)
in type_of, sort_of
let get_type_of env sigma = fst (typeur sigma []) env
let get_sort_of env sigma = snd (typeur sigma []) env
let get_type_of_with_meta env sigma metamap = fst (typeur sigma metamap) env
|
