← Back to branch summary

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

« back to all changes in this revision

Viewing changes to pretyping/retyping.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/retyping.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: retyping.ml 11897 2009-02-09 19:28:02Z barras $ *)
 
10
 
 
11
open Util
 
12
open Term
 
13
open Inductive
 
14
open Inductiveops
 
15
open Names
 
16
open Reductionops
 
17
open Environ
 
18
open Typeops
 
19
open Declarations
 
20
open Termops
 
21
 
 
22
let rec subst_type env sigma typ = function
 
23
  | [] -> typ
 
24
  | h::rest ->
 
25
      match kind_of_term (whd_betadeltaiota env sigma typ) with
 
26
        | Prod (na,c1,c2) -> subst_type env sigma (subst1 h c2) rest
 
27
        | _ -> anomaly "Non-functional construction"
 
28
 
 
29
(* Si ft est le type d'un terme f, lequel est appliqu� � args, *)
 
30
(* [sort_of_atomic_ty] calcule ft[args] qui doit �tre une sorte *)
 
31
(* On suit une m�thode paresseuse, en esp�rant que ft est une arit� *)
 
32
(* et sinon on substitue *)
 
33
 
 
34
let sort_of_atomic_type env sigma ft args =
 
35
  let rec concl_of_arity env ar =
 
36
    match kind_of_term (whd_betadeltaiota env sigma ar) with
 
37
    | Prod (na, t, b) -> concl_of_arity (push_rel (na,None,t) env) b
 
38
    | Sort s -> s
 
39
    | _ -> decomp_sort env sigma (subst_type env sigma ft (Array.to_list args))
 
40
  in concl_of_arity env ft
 
41
 
 
42
let type_of_var env id =
 
43
  try let (_,_,ty) = lookup_named id env in ty
 
44
  with Not_found ->
 
45
    anomaly ("type_of: variable "^(string_of_id id)^" unbound")
 
46
 
 
47
let retype sigma metamap =
 
48
  let rec type_of env cstr=
 
49
    match kind_of_term cstr with
 
50
    | Meta n ->
 
51
          (try strip_outer_cast (List.assoc n metamap)
 
52
           with Not_found -> anomaly ("type_of: unknown meta " ^ string_of_int n))
 
53
    | Rel n ->
 
54
        let (_,_,ty) = lookup_rel n env in
 
55
        lift n ty
 
56
    | Var id -> type_of_var env id
 
57
    | Const cst -> Typeops.type_of_constant env cst
 
58
    | Evar ev -> Evd.existential_type sigma ev
 
59
    | Ind ind -> type_of_inductive env ind
 
60
    | Construct cstr -> type_of_constructor env cstr
 
61
    | Case (_,p,c,lf) ->
 
62
        let Inductiveops.IndType(_,realargs) =
 
63
          try Inductiveops.find_rectype env sigma (type_of env c)
 
64
          with Not_found -> anomaly "type_of: Bad recursive type" in
 
65
        let t = whd_beta sigma (applist (p, realargs)) in
 
66
        (match kind_of_term (whd_betadeltaiota env sigma (type_of env t)) with
 
67
          | Prod _ -> whd_beta sigma (applist (t, [c]))
 
68
          | _ -> t)
 
69
    | Lambda (name,c1,c2) ->
 
70
          mkProd (name, c1, type_of (push_rel (name,None,c1) env) c2)
 
71
    | LetIn (name,b,c1,c2) ->
 
72
         subst1 b (type_of (push_rel (name,Some b,c1) env) c2)
 
73
    | Fix ((_,i),(_,tys,_)) -> tys.(i)
 
74
    | CoFix (i,(_,tys,_)) -> tys.(i)
 
75
    | App(f,args) when isGlobalRef f ->
 
76
        let t = type_of_global_reference_knowing_parameters env f args in
 
77
        strip_outer_cast (subst_type env sigma t (Array.to_list args))
 
78
    | App(f,args) ->
 
79
        strip_outer_cast
 
80
          (subst_type env sigma (type_of env f) (Array.to_list args))
 
81
    | Cast (c,_, t) -> t
 
82
    | Sort _ | Prod _ -> mkSort (sort_of env cstr)
 
83
 
 
84
  and sort_of env t = 
 
85
    match kind_of_term t with
 
86
    | Cast (c,_, s) when isSort s -> destSort s
 
87
    | Sort (Prop c) -> type1_sort
 
88
    | Sort (Type u) -> Type (Univ.super u)
 
89
    | Prod (name,t,c2) ->
 
90
        (match (sort_of env t, sort_of (push_rel (name,None,t) env) c2) with
 
91
          | _, (Prop Null as s) -> s
 
92
          | Prop _, (Prop Pos as s) -> s
 
93
          | Type _, (Prop Pos as s) when
 
94
              Environ.engagement env = Some ImpredicativeSet -> s
 
95
          | (Type _, _) | (_, Type _) -> new_Type_sort ()
 
96
(*
 
97
          | Type u1, Prop Pos -> Type (Univ.sup u1 Univ.type0_univ)
 
98
          | Prop Pos, (Type u2) -> Type (Univ.sup Univ.type0_univ u2)
 
99
          | Prop Null, (Type _ as s) -> s
 
100
          | Type u1, Type u2 -> Type (Univ.sup u1 u2)*))
 
101
    | App(f,args) when isGlobalRef f ->
 
102
        let t = type_of_global_reference_knowing_parameters env f args in
 
103
        sort_of_atomic_type env sigma t args
 
104
    | App(f,args) -> sort_of_atomic_type env sigma (type_of env f) args
 
105
    | Lambda _ | Fix _ | Construct _ ->
 
106
        anomaly "sort_of: Not a type (1)"
 
107
    | _ -> decomp_sort env sigma (type_of env t)
 
108
 
 
109
  and sort_family_of env t =
 
110
    match kind_of_term t with
 
111
    | Cast (c,_, s) when isSort s -> family_of_sort (destSort s)
 
112
    | Sort (Prop c) -> InType
 
113
    | Sort (Type u) -> InType
 
114
    | Prod (name,t,c2) -> 
 
115
        let s2 = sort_family_of (push_rel (name,None,t) env) c2 in
 
116
        if Environ.engagement env <> Some ImpredicativeSet &&
 
117
           s2 = InSet & sort_family_of env t = InType then InType else s2
 
118
    | App(f,args) when isGlobalRef f ->
 
119
        let t = type_of_global_reference_knowing_parameters env f args in
 
120
        family_of_sort (sort_of_atomic_type env sigma t args)
 
121
    | App(f,args) -> 
 
122
        family_of_sort (sort_of_atomic_type env sigma (type_of env f) args)
 
123
    | Lambda _ | Fix _ | Construct _ ->
 
124
        anomaly "sort_of: Not a type (1)"
 
125
    | _ -> family_of_sort (decomp_sort env sigma (type_of env t))
 
126
 
 
127
  and type_of_global_reference_knowing_parameters env c args =
 
128
    let argtyps = Array.map (fun c -> nf_evar sigma (type_of env c)) args in
 
129
    match kind_of_term c with
 
130
    | Ind ind ->
 
131
      let (_,mip) = lookup_mind_specif env ind in
 
132
      Inductive.type_of_inductive_knowing_parameters env mip argtyps
 
133
    | Const cst ->
 
134
      let t = constant_type env cst in
 
135
      Typeops.type_of_constant_knowing_parameters env t argtyps
 
136
    | Var id -> type_of_var env id
 
137
    | Construct cstr -> type_of_constructor env cstr
 
138
    | _ -> assert false
 
139
 
 
140
  in type_of, sort_of, sort_family_of,
 
141
     type_of_global_reference_knowing_parameters
 
142
 
 
143
let get_sort_of env sigma t = let _,f,_,_ = retype sigma [] in f env t
 
144
let get_sort_family_of env sigma c = let _,_,f,_ = retype sigma [] in f env c
 
145
let type_of_global_reference_knowing_parameters env sigma c args =
 
146
  let _,_,_,f = retype sigma [] in f env c args
 
147
 
 
148
let type_of_global_reference_knowing_conclusion env sigma c conclty =
 
149
  let conclty = nf_evar sigma conclty in
 
150
  match kind_of_term c with
 
151
    | Ind ind ->
 
152
        let (_,mip) = Inductive.lookup_mind_specif env ind in
 
153
        type_of_inductive_knowing_conclusion env mip conclty
 
154
    | Const cst ->
 
155
        let t = constant_type env cst in
 
156
        (* TODO *)
 
157
        Typeops.type_of_constant_knowing_parameters env t [||]
 
158
    | Var id -> type_of_var env id
 
159
    | Construct cstr -> type_of_constructor env cstr
 
160
    | _ -> assert false
 
161
 
 
162
(* We are outside the kernel: we take fresh universes *)
 
163
(* to avoid tactics and co to refresh universes themselves *)
 
164
let get_type_of env sigma c =
 
165
  let f,_,_,_ = retype sigma [] in refresh_universes (f env c)
 
166
 
 
167
let get_type_of_with_meta env sigma metamap c =
 
168
  let f,_,_,_ = retype sigma metamap in refresh_universes (f env c)
 
169
 
 
170
(* Makes an assumption from a constr *)
 
171
let get_assumption_of env evc c = c
 
172
 
 
173
(* Makes an unsafe judgment from a constr *)
 
174
let get_judgment_of env evc c = { uj_val = c; uj_type = get_type_of env evc c }
 
175