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
|
(**************************************************************************)
(* *)
(* The Why platform for program certification *)
(* *)
(* Copyright (C) 2002-2011 *)
(* *)
(* Jean-Christophe FILLIATRE, CNRS & Univ. Paris-sud 11 *)
(* Claude MARCHE, INRIA & Univ. Paris-sud 11 *)
(* Yannick MOY, Univ. Paris-sud 11 *)
(* Romain BARDOU, Univ. Paris-sud 11 *)
(* *)
(* Secondary contributors: *)
(* *)
(* Thierry HUBERT, Univ. Paris-sud 11 (former Caduceus front-end) *)
(* Nicolas ROUSSET, Univ. Paris-sud 11 (on Jessie & Krakatoa) *)
(* Ali AYAD, CNRS & CEA Saclay (floating-point support) *)
(* Sylvie BOLDO, INRIA (floating-point support) *)
(* Jean-Francois COUCHOT, INRIA (sort encodings, hyps pruning) *)
(* Mehdi DOGGUY, Univ. Paris-sud 11 (Why GUI) *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Lesser General Public *)
(* License version 2.1, with the special exception on linking *)
(* described in file LICENSE. *)
(* *)
(* This software is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *)
(* *)
(**************************************************************************)
open Ml_misc
open Jc_env
open Jc_fenv
exception Not_found_str of string
module IdentMap = Map.Make(
struct
type t = Ml_ocaml.Ident.t
let compare x y = String.compare (Ml_ocaml.Ident.unique_name x)
(Ml_ocaml.Ident.unique_name y)
end)
type t = {
vars: Jc_env.var_info StringMap.t;
funs: Jc_fenv.fun_info StringMap.t;
(*fields: Jc_env.field_info StringMap.t;
constructors: (Jc_env.struct_info * int * Jc_env.field_info list) StringMap.t;
structs: Jc_env.struct_info StringMap.t;*)
logic_funs: Jc_fenv.logic_info StringMap.t;
(*tags: Jc_env.field_info StringMap.t;*)
fun_specs: Ml_ocaml.Typedtree.function_spec IdentMap.t;
(*type_specs: Ml_ocaml.Typedtree.type_spec IdentMap.t;*)
}
let empty = {
vars = StringMap.empty;
funs = StringMap.empty;
(*fields = StringMap.empty;
constructors = StringMap.empty;
structs = StringMap.empty;*)
logic_funs = StringMap.empty;
(*tags = StringMap.empty;*)
fun_specs = IdentMap.empty;
(*type_specs = IdentMap.empty;*)
}
let add_var name ty env =
let vi = make_var name ty in
{ env with vars = StringMap.add name vi env.vars }, vi
let add_fun name params return_type env =
let jc_name = identifier_of_symbol name in
let fi = make_fun_info jc_name return_type params () in
{ env with funs = StringMap.add name fi env.funs }
(*let add_field name ty si env =
let fi = {
jc_field_info_tag = fresh_int ();
jc_field_info_name = name;
jc_field_info_final_name = name;
jc_field_info_type = ty;
jc_field_info_struct = si;
jc_field_info_root = si.jc_struct_info_root;
jc_field_info_rep = false;
} in
{ env with fields = StringMap.add name fi env.fields }, fi
let add_constructor name tyl si i env =
let _, fil = list_fold_map
(fun cnt ty -> cnt + 1,
let name = name^"_"^string_of_int cnt in
{
jc_field_info_tag = fresh_int ();
jc_field_info_name = name;
jc_field_info_final_name = name;
jc_field_info_type = ty;
jc_field_info_struct = si;
jc_field_info_root = si.jc_struct_info_root;
jc_field_info_rep = false;
})
0 tyl
in
{ env with constructors = StringMap.add name (si, i, fil) env.constructors },
fil
let add_struct si env =
{ env with structs = StringMap.add si.jc_struct_info_name si env.structs }
let add_tag si env =
let fi = {
jc_field_info_tag = fresh_int ();
jc_field_info_name = "jessica_tag";
jc_field_info_final_name = "jessica_tag";
jc_field_info_type = JCTnative Tinteger;
jc_field_info_struct = si;
jc_field_info_root = si.jc_struct_info_root;
jc_field_info_rep = false;
} in
{ env with tags = StringMap.add si.jc_struct_info_name fi env.tags }, fi*)
let add_logic_fun name params return_type env =
let li = {
jc_logic_info_tag = fresh_int ();
jc_logic_info_name = name;
jc_logic_info_final_name = name;
jc_logic_info_result_type = return_type;
jc_logic_info_parameters = params;
jc_logic_info_effects = Jc_pervasives.empty_effects; (* ! *)
jc_logic_info_calls = [];
jc_logic_info_result_region = default_region;
jc_logic_info_param_regions = [];
jc_logic_info_labels = [];
} in
{ env with logic_funs = StringMap.add name li env.logic_funs }, li
let add_fun_spec id spec env =
{ env with fun_specs = IdentMap.add id spec env.fun_specs }
(*let add_type_spec id spec env =
{ env with type_specs = IdentMap.add id spec env.type_specs }*)
let nf s f k m =
try
f k m
with Not_found ->
raise (Not_found_str s)
let find_var name env = nf name StringMap.find name env.vars
let find_fun name env = nf name StringMap.find name env.funs
(*let find_field name env = nf name StringMap.find name env.fields
let find_constructor name env = nf name StringMap.find name env.constructors
let find_struct name env = nf name StringMap.find name env.structs*)
let find_logic_fun name env = nf name StringMap.find name env.logic_funs
(*let find_tag si env =
let name = si.jc_struct_info_name in
nf name StringMap.find name env.tags*)
let find_fun_spec id env =
nf (Ml_ocaml.Ident.name id) IdentMap.find id env.fun_specs
(*let find_type_spec id env =
nf (Ml_ocaml.Ident.name id) IdentMap.find id env.type_specs*)
(*
Local Variables:
compile-command: "unset LANG; make -C .. -f build.makefile jessica.all"
End:
*)
|
