aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/typing.ml
blob: ece3586a19c986cb88220cc41b0773f4d47cc987 (plain)
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
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)

(* $Id$ *)

open Util
open Names
open Term
open Environ
open Reductionops
open Type_errors
open Pretype_errors
open Inductive
open Inductiveops
open Typeops
open Evd

let meta_type evd mv =
  let ty =
    try Evd.meta_ftype evd mv
    with Not_found -> anomaly ("unknown meta ?"^Nameops.string_of_meta mv) in
  meta_instance evd ty

let constant_type_knowing_parameters env cst jl =
  let paramstyp = Array.map (fun j -> j.uj_type) jl in
  type_of_constant_knowing_parameters env (constant_type env cst) paramstyp

let inductive_type_knowing_parameters env ind jl =
  let (mib,mip) = lookup_mind_specif env ind in
  let paramstyp = Array.map (fun j -> j.uj_type) jl in
  Inductive.type_of_inductive_knowing_parameters env mip paramstyp

(* The typing machine without information, without universes but with
   existential variables. *)

(* cstr must be in n.f. w.r.t. evars and execute returns a judgement
   where both the term and type are in n.f. *)
let rec execute env evd cstr =
  match kind_of_term cstr with
    | Meta n ->
        { uj_val = cstr; uj_type = nf_evar (evars_of evd) (meta_type evd n) }

    | Evar ev ->
        let sigma = Evd.evars_of evd in
	let ty = Evd.existential_type sigma ev in
	let jty = execute env evd (nf_evar (evars_of evd) ty) in
	let jty = assumption_of_judgment env jty in
	{ uj_val = cstr; uj_type = jty }
	
    | Rel n -> 
	j_nf_evar (evars_of evd) (judge_of_relative env n)

    | Var id -> 
        j_nf_evar (evars_of evd) (judge_of_variable env id)
	  
    | Const c ->
        make_judge cstr (nf_evar (evars_of evd) (type_of_constant env c))
	  
    | Ind ind ->
	make_judge cstr (nf_evar (evars_of evd) (type_of_inductive env ind))
	  
    | Construct cstruct -> 
	make_judge cstr
          (nf_evar (evars_of evd) (type_of_constructor env cstruct))

    | Case (ci,p,c,lf) ->
        let cj = execute env evd c in
        let pj = execute env evd p in
        let lfj = execute_array env evd lf in
        let (j,_) = judge_of_case env ci pj cj lfj in
        j
  
    | Fix ((vn,i as vni),recdef) ->
        let (_,tys,_ as recdef') = execute_recdef env evd recdef in
	let fix = (vni,recdef') in
        check_fix env fix;
	make_judge (mkFix fix) tys.(i)
	  
    | CoFix (i,recdef) ->
        let (_,tys,_ as recdef') = execute_recdef env evd recdef in
        let cofix = (i,recdef') in
        check_cofix env cofix;
	make_judge (mkCoFix cofix) tys.(i)
	  
    | Sort (Prop c) -> 
	judge_of_prop_contents c

    | Sort (Type u) ->
	judge_of_type u
	  
    | App (f,args) ->
        let jl = execute_array env evd args in
	let j =
	  match kind_of_term f with
	    | Ind ind ->
		(* Sort-polymorphism of inductive types *)
		make_judge f
		  (inductive_type_knowing_parameters env ind
		    (jv_nf_evar (evars_of evd) jl))
	    | Const cst -> 
		(* Sort-polymorphism of inductive types *)
		make_judge f
		  (constant_type_knowing_parameters env cst
		    (jv_nf_evar (evars_of evd) jl))
	    | _ -> 
		execute env evd f
	in
	fst (judge_of_apply env j jl)
	    
    | Lambda (name,c1,c2) -> 
        let j = execute env evd c1 in
	let var = type_judgment env j in
	let env1 = push_rel (name,None,var.utj_val) env in
        let j' = execute env1 evd c2 in 
        judge_of_abstraction env1 name var j'
	  
    | Prod (name,c1,c2) ->
        let j = execute env evd c1 in
        let varj = type_judgment env j in
	let env1 = push_rel (name,None,varj.utj_val) env in
        let j' = execute env1 evd c2 in
        let varj' = type_judgment env1 j' in
	judge_of_product env name varj varj'

     | LetIn (name,c1,c2,c3) ->
        let j1 = execute env evd c1 in
        let j2 = execute env evd c2 in
        let j2 = type_judgment env j2 in
        let _ =  judge_of_cast env j1 DEFAULTcast j2 in
        let env1 = push_rel (name,Some j1.uj_val,j2.utj_val) env in
        let j3 = execute env1 evd c3 in
        judge_of_letin env name j1 j2 j3
  
    | Cast (c,k,t) ->
        let cj = execute env evd c in
        let tj = execute env evd t in
	let tj = type_judgment env tj in
        let j, _ = judge_of_cast env cj k tj in
	j

and execute_recdef env evd (names,lar,vdef) =
  let larj = execute_array env evd lar in
  let lara = Array.map (assumption_of_judgment env) larj in
  let env1 = push_rec_types (names,lara,vdef) env in
  let vdefj = execute_array env1 evd vdef in
  let vdefv = Array.map j_val vdefj in
  let _ = type_fixpoint env1 names lara vdefj in
  (names,lara,vdefv)

and execute_array env evd = Array.map (execute env evd)

and execute_list env evd = List.map (execute env evd)

let mcheck env evd c t =
  let sigma = Evd.evars_of evd in
  let j = execute env evd (nf_evar sigma c) in
  if not (is_conv_leq env sigma j.uj_type t) then
    error_actual_type env j (nf_evar sigma t)

(* Type of a constr *)
 
let mtype_of env evd c =
  let j = execute env evd (nf_evar (evars_of evd) c) in
  (* We are outside the kernel: we take fresh universes *)
  (* to avoid tactics and co to refresh universes themselves *)
  Termops.refresh_universes j.uj_type

let msort_of env evd c =
  let j = execute env evd (nf_evar (evars_of evd) c) in
  let a = type_judgment env j in
  a.utj_type

let type_of env sigma c =
  mtype_of env (Evd.create_evar_defs sigma) c
let sort_of env sigma c =
  msort_of env (Evd.create_evar_defs sigma) c
let check env sigma c   =
  mcheck env (Evd.create_evar_defs sigma) c

(* The typed type of a judgment. *)

let mtype_of_type env evd constr =
  let j = execute env evd (nf_evar (evars_of evd) constr) in
  assumption_of_judgment env j