← Back to branch summary

~ubuntu-branches/ubuntu/wily/coq-doc/wily

« back to all changes in this revision

Viewing changes to pretyping/typing.ml

  • Committer: Bazaar Package Importer
  • Author(s): Stéphane Glondu, Stéphane Glondu, Samuel Mimram
  • Date: 2010-01-07 22:50:39 UTC
  • mfrom: (1.2.2 upstream)
  • Revision ID: james.westby@ubuntu.com-20100107225039-n3cq82589u0qt0s2
Tags: 8.2pl1-1
http://bugs.debian.org/563669
http://bugs.debian.org/543545
[ Stéphane Glondu ]
* New upstream release (Closes: #563669)
  - remove patches
* Packaging overhaul:
  - use git, advertise it in Vcs-* fields of debian/control
  - use debhelper 7 and dh with override
  - use source format 3.0 (quilt)
* debian/control:
  - set Maintainer to d-o-m, set Uploaders to Sam and myself
  - add Homepage field
  - bump Standards-Version to 3.8.3
* Register PDF documentation into doc-base
* Add debian/watch
* Update debian/copyright

[ Samuel Mimram ]
* Change coq-doc's description to mention that it provides documentation in
  pdf format, not postscript, closes: #543545.

Show diffs side-by-side

added added

removed removed

Lines of Context:
pretyping/typing.ml
 
1
(************************************************************************)
 
2
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
 
4
(*   \VV/  **************************************************************)
 
5
(*    //   *      This file is distributed under the terms of the       *)
 
6
(*         *       GNU Lesser General Public License Version 2.1        *)
 
7
(************************************************************************)
 
8
 
 
9
(* $Id: typing.ml 10785 2008-04-13 21:41:54Z herbelin $ *)
 
10
 
 
11
open Util
 
12
open Names
 
13
open Term
 
14
open Environ
 
15
open Reductionops
 
16
open Type_errors
 
17
open Pretype_errors
 
18
open Inductive
 
19
open Inductiveops
 
20
open Typeops
 
21
open Evd
 
22
 
 
23
let meta_type evd mv =
 
24
  let ty =
 
25
    try Evd.meta_ftype evd mv
 
26
    with Not_found -> anomaly ("unknown meta ?"^Nameops.string_of_meta mv) in
 
27
  meta_instance evd ty
 
28
 
 
29
let constant_type_knowing_parameters env cst jl =
 
30
  let paramstyp = Array.map (fun j -> j.uj_type) jl in
 
31
  type_of_constant_knowing_parameters env (constant_type env cst) paramstyp
 
32
 
 
33
let inductive_type_knowing_parameters env ind jl =
 
34
  let (mib,mip) = lookup_mind_specif env ind in
 
35
  let paramstyp = Array.map (fun j -> j.uj_type) jl in
 
36
  Inductive.type_of_inductive_knowing_parameters env mip paramstyp
 
37
 
 
38
(* The typing machine without information, without universes but with
 
39
   existential variables. *)
 
40
 
 
41
(* cstr must be in n.f. w.r.t. evars and execute returns a judgement
 
42
   where both the term and type are in n.f. *)
 
43
let rec execute env evd cstr =
 
44
  match kind_of_term cstr with
 
45
    | Meta n ->
 
46
        { uj_val = cstr; uj_type = nf_evar (evars_of evd) (meta_type evd n) }
 
47
 
 
48
    | Evar ev ->
 
49
        let sigma = Evd.evars_of evd in
 
50
        let ty = Evd.existential_type sigma ev in
 
51
        let jty = execute env evd (nf_evar (evars_of evd) ty) in
 
52
        let jty = assumption_of_judgment env jty in
 
53
        { uj_val = cstr; uj_type = jty }
 
54
        
 
55
    | Rel n -> 
 
56
        j_nf_evar (evars_of evd) (judge_of_relative env n)
 
57
 
 
58
    | Var id -> 
 
59
        j_nf_evar (evars_of evd) (judge_of_variable env id)
 
60
          
 
61
    | Const c ->
 
62
        make_judge cstr (nf_evar (evars_of evd) (type_of_constant env c))
 
63
          
 
64
    | Ind ind ->
 
65
        make_judge cstr (nf_evar (evars_of evd) (type_of_inductive env ind))
 
66
          
 
67
    | Construct cstruct -> 
 
68
        make_judge cstr
 
69
          (nf_evar (evars_of evd) (type_of_constructor env cstruct))
 
70
 
 
71
    | Case (ci,p,c,lf) ->
 
72
        let cj = execute env evd c in
 
73
        let pj = execute env evd p in
 
74
        let lfj = execute_array env evd lf in
 
75
        let (j,_) = judge_of_case env ci pj cj lfj in
 
76
        j
 
77
  
 
78
    | Fix ((vn,i as vni),recdef) ->
 
79
        let (_,tys,_ as recdef') = execute_recdef env evd recdef in
 
80
        let fix = (vni,recdef') in
 
81
        check_fix env fix;
 
82
        make_judge (mkFix fix) tys.(i)
 
83
          
 
84
    | CoFix (i,recdef) ->
 
85
        let (_,tys,_ as recdef') = execute_recdef env evd recdef in
 
86
        let cofix = (i,recdef') in
 
87
        check_cofix env cofix;
 
88
        make_judge (mkCoFix cofix) tys.(i)
 
89
          
 
90
    | Sort (Prop c) -> 
 
91
        judge_of_prop_contents c
 
92
 
 
93
    | Sort (Type u) ->
 
94
        judge_of_type u
 
95
          
 
96
    | App (f,args) ->
 
97
        let jl = execute_array env evd args in
 
98
        let j =
 
99
          match kind_of_term f with
 
100
            | Ind ind ->
 
101
                (* Sort-polymorphism of inductive types *)
 
102
                make_judge f
 
103
                  (inductive_type_knowing_parameters env ind
 
104
                    (jv_nf_evar (evars_of evd) jl))
 
105
            | Const cst -> 
 
106
                (* Sort-polymorphism of inductive types *)
 
107
                make_judge f
 
108
                  (constant_type_knowing_parameters env cst
 
109
                    (jv_nf_evar (evars_of evd) jl))
 
110
            | _ -> 
 
111
                execute env evd f
 
112
        in
 
113
        fst (judge_of_apply env j jl)
 
114
            
 
115
    | Lambda (name,c1,c2) -> 
 
116
        let j = execute env evd c1 in
 
117
        let var = type_judgment env j in
 
118
        let env1 = push_rel (name,None,var.utj_val) env in
 
119
        let j' = execute env1 evd c2 in 
 
120
        judge_of_abstraction env1 name var j'
 
121
          
 
122
    | Prod (name,c1,c2) ->
 
123
        let j = execute env evd c1 in
 
124
        let varj = type_judgment env j in
 
125
        let env1 = push_rel (name,None,varj.utj_val) env in
 
126
        let j' = execute env1 evd c2 in
 
127
        let varj' = type_judgment env1 j' in
 
128
        judge_of_product env name varj varj'
 
129
 
 
130
     | LetIn (name,c1,c2,c3) ->
 
131
        let j1 = execute env evd c1 in
 
132
        let j2 = execute env evd c2 in
 
133
        let j2 = type_judgment env j2 in
 
134
        let _ =  judge_of_cast env j1 DEFAULTcast j2 in
 
135
        let env1 = push_rel (name,Some j1.uj_val,j2.utj_val) env in
 
136
        let j3 = execute env1 evd c3 in
 
137
        judge_of_letin env name j1 j2 j3
 
138
  
 
139
    | Cast (c,k,t) ->
 
140
        let cj = execute env evd c in
 
141
        let tj = execute env evd t in
 
142
        let tj = type_judgment env tj in
 
143
        let j, _ = judge_of_cast env cj k tj in
 
144
        j
 
145
 
 
146
and execute_recdef env evd (names,lar,vdef) =
 
147
  let larj = execute_array env evd lar in
 
148
  let lara = Array.map (assumption_of_judgment env) larj in
 
149
  let env1 = push_rec_types (names,lara,vdef) env in
 
150
  let vdefj = execute_array env1 evd vdef in
 
151
  let vdefv = Array.map j_val vdefj in
 
152
  let _ = type_fixpoint env1 names lara vdefj in
 
153
  (names,lara,vdefv)
 
154
 
 
155
and execute_array env evd = Array.map (execute env evd)
 
156
 
 
157
and execute_list env evd = List.map (execute env evd)
 
158
 
 
159
let mcheck env evd c t =
 
160
  let sigma = Evd.evars_of evd in
 
161
  let j = execute env evd (nf_evar sigma c) in
 
162
  if not (is_conv_leq env sigma j.uj_type t) then
 
163
    error_actual_type env j (nf_evar sigma t)
 
164
 
 
165
(* Type of a constr *)
 
166
 
 
167
let mtype_of env evd c =
 
168
  let j = execute env evd (nf_evar (evars_of evd) c) in
 
169
  (* We are outside the kernel: we take fresh universes *)
 
170
  (* to avoid tactics and co to refresh universes themselves *)
 
171
  Termops.refresh_universes j.uj_type
 
172
 
 
173
let msort_of env evd c =
 
174
  let j = execute env evd (nf_evar (evars_of evd) c) in
 
175
  let a = type_judgment env j in
 
176
  a.utj_type
 
177
 
 
178
let type_of env sigma c =
 
179
  mtype_of env (Evd.create_evar_defs sigma) c
 
180
let sort_of env sigma c =
 
181
  msort_of env (Evd.create_evar_defs sigma) c
 
182
let check env sigma c   =
 
183
  mcheck env (Evd.create_evar_defs sigma) c
 
184
 
 
185
(* The typed type of a judgment. *)
 
186
 
 
187
let mtype_of_type env evd constr =
 
188
  let j = execute env evd (nf_evar (evars_of evd) constr) in
 
189
  assumption_of_judgment env j