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
|
(***********************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
(* \VV/ *************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(***********************************************************************)
(* $Id$ *)
open Util
open Names
open Univ
open Term
open Reduction
open Sign
open Declarations
open Inductive
open Environ
open Type_errors
open Indtypes
type judgment = unsafe_judgment
let j_val = j_val
let j_type = j_type
(* Exported machines. *)
let safe_infer = Typeops.infer
let safe_infer_type = Typeops.infer_type
(*s Safe environments. *)
type safe_environment = env
let empty_environment = empty_env
(* Insertion of variables (named and de Bruijn'ed). They are now typed before
being added to the environment. *)
let push_rel_or_named_def push (id,b) env =
let (j,cst) = safe_infer env b in
let env' = add_constraints cst env in
let env'' = push (id,Some j.uj_val,j.uj_type) env' in
(cst,env'')
let push_named_def = push_rel_or_named_def push_named_decl
let push_rel_def = push_rel_or_named_def push_rel
let push_rel_or_named_assum push (id,t) env =
let (j,cst) = safe_infer env t in
let t = Typeops.assumption_of_judgment env j in
let env' = add_constraints cst env in
let env'' = push (id,None,t) env' in
(cst,env'')
let push_named_assum = push_rel_or_named_assum push_named_decl
let push_rel_assum d env = snd (push_rel_or_named_assum push_rel d env)
let push_rels_with_univ vars env =
List.fold_left (fun env nvar -> push_rel_assum nvar env) env vars
(* Insertion of constants and parameters in environment. *)
type global_declaration = Def of constr * bool | Assum of constr
(* Definition always declared transparent *)
let safe_infer_declaration env dcl =
match dcl with
| Def (c,op) ->
let (j,cst) = safe_infer env c in
Some j.uj_val, j.uj_type, cst, op
| Assum t ->
let (j,cst) = safe_infer env t in
None, Typeops.assumption_of_judgment env j, cst, false
let add_global_declaration sp env (body,typ,cst,op) =
let env' = add_constraints cst env in
let ids = match body with
| None -> global_vars_set env typ
| Some b ->
Idset.union (global_vars_set env b) (global_vars_set env typ) in
let hyps = keep_hyps env ids in
let cb = {
const_body = body;
const_type = typ;
const_hyps = hyps;
const_constraints = cst;
const_opaque = op } in
Environ.add_constant sp cb env'
let add_parameter sp t env =
add_global_declaration sp env (safe_infer_declaration env (Assum t))
(*s Global and local constant declaration. *)
type constant_entry = {
const_entry_body : constr;
const_entry_type : types option;
const_entry_opaque : bool }
let add_constant sp ce env =
let body =
match ce.const_entry_type with
| None -> ce.const_entry_body
| Some ty -> mkCast (ce.const_entry_body, ty) in
add_global_declaration sp env
(safe_infer_declaration env (Def (body, ce.const_entry_opaque)))
let add_discharged_constant sp r env =
let (body,typ,cst,op) = Cooking.cook_constant env r in
match body with
| None ->
add_parameter sp typ (* Bricolage avant poubelle *) env
| Some c ->
(* let c = hcons1_constr c in *)
let ids =
Idset.union (global_vars_set env c)
(global_vars_set env (body_of_type typ))
in
let hyps = keep_hyps env ids in
let env' = Environ.add_constraints cst env in
let cb =
{ const_body = Some c;
const_type = typ;
const_hyps = hyps;
const_constraints = cst;
const_opaque = op } in
Environ.add_constant sp cb env'
(* Insertion of inductive types. *)
let add_mind sp mie env =
let mib = check_inductive env mie in
let cst = mib.mind_constraints in
Environ.add_mind sp mib (add_constraints cst env)
let add_constraints = Environ.add_constraints
let rec pop_named_decls idl env =
match idl with
| [] -> env
| id::l -> pop_named_decls l (Environ.pop_named_decl id env)
let export = export
let import = import
let env_of_safe_env e = e
(* Exported typing functions *)
let typing env c =
let (j,cst) = safe_infer env c in
let _ = add_constraints cst env in
j
|
