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
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(* $Id: term_typing.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
open Util
open Names
open Univ
open Term
open Reduction
open Sign
open Declarations
open Inductive
open Environ
open Entries
open Type_errors
open Indtypes
open Typeops
let constrain_type env j cst1 = function
| None ->
make_polymorphic_if_constant_for_ind env j, cst1
| Some t ->
let (tj,cst2) = infer_type env t in
let (_,cst3) = judge_of_cast env j DEFAULTcast tj in
assert (t = tj.utj_val);
NonPolymorphicType t, Constraint.union (Constraint.union cst1 cst2) cst3
let local_constrain_type env j cst1 = function
| None ->
j.uj_type, cst1
| Some t ->
let (tj,cst2) = infer_type env t in
let (_,cst3) = judge_of_cast env j DEFAULTcast tj in
assert (t = tj.utj_val);
t, Constraint.union (Constraint.union cst1 cst2) cst3
let translate_local_def env (b,topt) =
let (j,cst) = infer env b in
let (typ,cst) = local_constrain_type env j cst topt in
(j.uj_val,typ,cst)
let translate_local_assum env t =
let (j,cst) = infer env t in
let t = Typeops.assumption_of_judgment env j in
(t,cst)
(*
(* Same as push_named, but check that the variable is not already
there. Should *not* be done in Environ because tactics add temporary
hypothesis many many times, and the check performed here would
cost too much. *)
let safe_push_named (id,_,_ as d) env =
let _ =
try
let _ = lookup_named id env in
error ("Identifier "^string_of_id id^" already defined.")
with Not_found -> () in
push_named d env
let push_named_def = push_rel_or_named_def safe_push_named
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
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. *)
let infer_declaration env dcl =
match dcl with
| DefinitionEntry c ->
let (j,cst) = infer env c.const_entry_body in
let (typ,cst) = constrain_type env j cst c.const_entry_type in
Some (Declarations.from_val j.uj_val), typ, cst,
c.const_entry_opaque, c.const_entry_boxed, false
| ParameterEntry (t,nl) ->
let (j,cst) = infer env t in
None, NonPolymorphicType (Typeops.assumption_of_judgment env j), cst,
false, false, nl
let global_vars_set_constant_type env = function
| NonPolymorphicType t -> global_vars_set env t
| PolymorphicArity (ctx,_) ->
Sign.fold_rel_context
(fold_rel_declaration
(fun t c -> Idset.union (global_vars_set env t) c))
ctx ~init:Idset.empty
let build_constant_declaration env kn (body,typ,cst,op,boxed,inline) =
let ids =
match body with
| None -> global_vars_set_constant_type env typ
| Some b ->
Idset.union
(global_vars_set env (Declarations.force b))
(global_vars_set_constant_type env typ)
in
let tps = Cemitcodes.from_val (compile_constant_body env body op boxed) in
let hyps = keep_hyps env ids in
{ const_hyps = hyps;
const_body = body;
const_type = typ;
const_body_code = tps;
(* const_type_code = to_patch env typ;*)
const_constraints = cst;
const_opaque = op;
const_inline = inline}
(*s Global and local constant declaration. *)
let translate_constant env kn ce =
build_constant_declaration env kn (infer_declaration env ce)
let translate_recipe env kn r =
build_constant_declaration env kn (Cooking.cook_constant env r)
(* Insertion of inductive types. *)
let translate_mind env mie = check_inductive env mie
|
