source: extracted/linearise.ml @ 2717

Last change on this file since 2717 was 2717, checked in by sacerdot, 7 years ago

Extracted code for the whole compiler.
The space cost model is not there yet.

I have fixed by hand the few extraction problems
(i.e. composed coercions not extracted and type
definitions with wrong syntax).

I have also changed all axioms to be implemented
so that they do not fail at initialization time.

File size: 10.8 KB
Line 
1open Preamble
2
3open String
4
5open Sets
6
7open Listb
8
9open LabelledObjects
10
11open Graphs
12
13open I8051
14
15open Order
16
17open Registers
18
19open BitVectorTrie
20
21open CostLabel
22
23open Hide
24
25open Proper
26
27open PositiveMap
28
29open Deqsets
30
31open ErrorMessages
32
33open PreIdentifiers
34
35open Errors
36
37open Extralib
38
39open Setoids
40
41open Monad
42
43open Option
44
45open Lists
46
47open Identifiers
48
49open Integers
50
51open AST
52
53open Division
54
55open Exp
56
57open Arithmetic
58
59open Extranat
60
61open Vector
62
63open Div_and_mod
64
65open Jmeq
66
67open Russell
68
69open List
70
71open Util
72
73open FoldStuff
74
75open BitVector
76
77open Types
78
79open Bool
80
81open Relations
82
83open Nat
84
85open Hints_declaration
86
87open Core_notation
88
89open Pts
90
91open Logic
92
93open Positive
94
95open Z
96
97open BitVectorZ
98
99open Pointers
100
101open ByteValues
102
103open BackEndOps
104
105open Joint
106
107(** val graph_to_lin_statement :
108    Joint.unserialized_params -> AST.ident List.list -> 'a1
109    Identifiers.identifier_map -> Joint.joint_statement ->
110    Joint.joint_statement **)
111let graph_to_lin_statement p globals visited = function
112| Joint.Sequential (c, nxt) ->
113  (match c with
114   | Joint.COST_LABEL x -> Joint.Sequential (c, (Obj.magic Types.It))
115   | Joint.CALL (x, x0, x1) -> Joint.Sequential (c, (Obj.magic Types.It))
116   | Joint.COND (a, ltrue) ->
117     (match Identifiers.member0 PreIdentifiers.LabelTag visited
118              (Obj.magic nxt) with
119      | Bool.True -> Joint.FCOND (a, ltrue, (Obj.magic nxt))
120      | Bool.False -> Joint.Sequential (c, (Obj.magic Types.It)))
121   | Joint.Step_seq x -> Joint.Sequential (c, (Obj.magic Types.It)))
122| Joint.Final c -> Joint.Final c
123| Joint.FCOND (x, x0, x1) -> assert false (* absurd case *)
124
125(** val chop :
126    ('a1 -> Bool.bool) -> 'a1 List.list -> ('a1, 'a1 List.list) Types.prod
127    Types.option **)
128let rec chop test = function
129| List.Nil -> Types.None
130| List.Cons (x, l') ->
131  (match test x with
132   | Bool.True -> chop test l'
133   | Bool.False ->
134     Obj.magic
135       (Monad.m_return0 (Monad.max_def Option.option0) { Types.fst = x;
136         Types.snd = l' }))
137
138type graph_visit_ret_type =
139  ((Nat.nat Identifiers.identifier_map, Identifiers.identifier_set)
140  Types.prod, __) Types.prod Types.sig0
141
142(** val graph_visit :
143    Joint.unserialized_params -> AST.ident List.list -> __ ->
144    Identifiers.identifier_set -> Nat.nat Identifiers.identifier_map -> __ ->
145    Graphs.label List.list -> Nat.nat -> Nat.nat -> Graphs.label ->
146    graph_visit_ret_type **)
147let rec graph_visit p globals g0 required visited generated visiting gen_length n entry =
148  (match chop (fun x ->
149           Identifiers.member0 PreIdentifiers.LabelTag visited x) visiting with
150   | Types.None ->
151     (fun _ -> { Types.fst = { Types.fst = visited; Types.snd = required };
152       Types.snd = generated })
153   | Types.Some pr ->
154     (fun _ ->
155       let vis_hd = pr.Types.fst in
156       let vis_tl = pr.Types.snd in
157       (match n with
158        | Nat.O -> (fun _ -> assert false (* absurd case *))
159        | Nat.S n' ->
160          (fun _ ->
161            let visited' =
162              Identifiers.add PreIdentifiers.LabelTag visited vis_hd
163                gen_length
164            in
165            let statement =
166              Identifiers.lookup_safe PreIdentifiers.LabelTag (Obj.magic g0)
167                vis_hd
168            in
169            let translated_statement =
170              graph_to_lin_statement p globals visited' statement
171            in
172            let generated' = List.Cons ({ Types.fst = (Types.Some vis_hd);
173              Types.snd = translated_statement }, (Obj.magic generated))
174            in
175            let required' =
176              Identifiers.union_set PreIdentifiers.LabelTag
177                (Identifiers.set_from_list PreIdentifiers.LabelTag
178                  (Joint.stmt_explicit_labels (Joint.lp_to_p__o__stmt_pars p)
179                    globals translated_statement)) required
180            in
181            let visiting' =
182              List.append
183                (Joint.stmt_labels { Joint.uns_pars = (Joint.g_u_pars p);
184                  Joint.succ_label = (Obj.magic (fun x -> Types.Some x));
185                  Joint.has_fcond = Bool.False } globals statement) vis_tl
186            in
187            let add_req_gen =
188              match statement with
189              | Joint.Sequential (s, nxt) ->
190                (match s with
191                 | Joint.COST_LABEL x ->
192                   (match Identifiers.member0 PreIdentifiers.LabelTag
193                            visited' (Obj.magic nxt) with
194                    | Bool.True ->
195                      { Types.fst = { Types.fst = (Nat.S Nat.O); Types.snd =
196                        (Identifiers.add_set PreIdentifiers.LabelTag
197                          (Identifiers.empty_set PreIdentifiers.LabelTag)
198                          (Obj.magic nxt)) }; Types.snd = (List.Cons
199                        ({ Types.fst = Types.None; Types.snd =
200                        (let x0 = Joint.Final (Joint.GOTO (Obj.magic nxt)) in
201                        x0) }, List.Nil)) }
202                    | Bool.False ->
203                      { Types.fst = { Types.fst = Nat.O; Types.snd =
204                        (Identifiers.empty_set PreIdentifiers.LabelTag) };
205                        Types.snd = List.Nil })
206                 | Joint.CALL (x, x0, x1) ->
207                   (match Identifiers.member0 PreIdentifiers.LabelTag
208                            visited' (Obj.magic nxt) with
209                    | Bool.True ->
210                      { Types.fst = { Types.fst = (Nat.S Nat.O); Types.snd =
211                        (Identifiers.add_set PreIdentifiers.LabelTag
212                          (Identifiers.empty_set PreIdentifiers.LabelTag)
213                          (Obj.magic nxt)) }; Types.snd = (List.Cons
214                        ({ Types.fst = Types.None; Types.snd =
215                        (let x2 = Joint.Final (Joint.GOTO (Obj.magic nxt)) in
216                        x2) }, List.Nil)) }
217                    | Bool.False ->
218                      { Types.fst = { Types.fst = Nat.O; Types.snd =
219                        (Identifiers.empty_set PreIdentifiers.LabelTag) };
220                        Types.snd = List.Nil })
221                 | Joint.COND (x, x0) ->
222                   { Types.fst = { Types.fst = Nat.O; Types.snd =
223                     (Identifiers.empty_set PreIdentifiers.LabelTag) };
224                     Types.snd = List.Nil }
225                 | Joint.Step_seq x ->
226                   (match Identifiers.member0 PreIdentifiers.LabelTag
227                            visited' (Obj.magic nxt) with
228                    | Bool.True ->
229                      { Types.fst = { Types.fst = (Nat.S Nat.O); Types.snd =
230                        (Identifiers.add_set PreIdentifiers.LabelTag
231                          (Identifiers.empty_set PreIdentifiers.LabelTag)
232                          (Obj.magic nxt)) }; Types.snd = (List.Cons
233                        ({ Types.fst = Types.None; Types.snd =
234                        (let x0 = Joint.Final (Joint.GOTO (Obj.magic nxt)) in
235                        x0) }, List.Nil)) }
236                    | Bool.False ->
237                      { Types.fst = { Types.fst = Nat.O; Types.snd =
238                        (Identifiers.empty_set PreIdentifiers.LabelTag) };
239                        Types.snd = List.Nil }))
240              | Joint.Final x ->
241                { Types.fst = { Types.fst = Nat.O; Types.snd =
242                  (Identifiers.empty_set PreIdentifiers.LabelTag) };
243                  Types.snd = List.Nil }
244              | Joint.FCOND (x0, x1, x2) ->
245                { Types.fst = { Types.fst = Nat.O; Types.snd =
246                  (Identifiers.empty_set PreIdentifiers.LabelTag) };
247                  Types.snd = List.Nil }
248            in
249            graph_visit p globals g0
250              (Identifiers.union_set PreIdentifiers.LabelTag
251                add_req_gen.Types.fst.Types.snd required') visited'
252              (Obj.magic (List.append add_req_gen.Types.snd generated'))
253              visiting'
254              (Nat.plus add_req_gen.Types.fst.Types.fst (Nat.S gen_length))
255              n' entry)) __)) __
256
257(** val branch_compress :
258    Joint.graph_params -> AST.ident List.list -> __ -> Graphs.label
259    Types.sig0 -> __ **)
260let branch_compress p globals g0 entry =
261  g0
262
263(** val filter_labels :
264    PreIdentifiers.identifierTag -> (PreIdentifiers.identifier -> Bool.bool)
265    -> 'a1 LabelledObjects.labelled_obj List.list -> (__, 'a1) Types.prod
266    List.list **)
267let filter_labels tag test c =
268  List.map (fun s ->
269    let { Types.fst = l_opt; Types.snd = x } = s in
270    { Types.fst =
271    (Monad.m_bind0 (Monad.max_def Option.option0) l_opt (fun l ->
272      match test l with
273      | Bool.True -> Monad.m_return0 (Monad.max_def Option.option0) l
274      | Bool.False -> Obj.magic Types.None)); Types.snd = x }) (Obj.magic c)
275
276(** val linearise_code :
277    Joint.unserialized_params -> AST.ident List.list -> __ -> Graphs.label
278    Types.sig0 -> (__, Graphs.label -> Nat.nat Types.option) Types.prod
279    Types.sig0 **)
280let linearise_code p globals g0 entry_sig =
281  let g1 = branch_compress p globals g0 entry_sig in
282  let triple =
283    graph_visit p globals g1 (Identifiers.empty_set PreIdentifiers.LabelTag)
284      (Identifiers.empty_map PreIdentifiers.LabelTag) (Obj.magic List.Nil)
285      (List.Cons ((Types.pi1 entry_sig), List.Nil)) Nat.O
286      (Identifiers.id_map_size PreIdentifiers.LabelTag (Obj.magic g1))
287      (Types.pi1 entry_sig)
288  in
289  let sigma0 = triple.Types.fst.Types.fst in
290  let required = triple.Types.fst.Types.snd in
291  let crev = triple.Types.snd in
292  let lbld_code = Util.rev (Obj.magic crev) in
293  { Types.fst =
294  (Obj.magic
295    (filter_labels PreIdentifiers.LabelTag (fun l ->
296      Identifiers.member0 PreIdentifiers.LabelTag required l) lbld_code));
297  Types.snd = (Identifiers.lookup0 PreIdentifiers.LabelTag sigma0) }
298
299(** val linearise_int_fun :
300    Joint.unserialized_params -> AST.ident List.list ->
301    Joint.joint_closed_internal_function ->
302    (Joint.joint_closed_internal_function, Graphs.label -> Nat.nat
303    Types.option) Types.prod Types.sig0 **)
304let linearise_int_fun p globals f_sig =
305  let code_sigma =
306    linearise_code p globals (Types.pi1 f_sig).Joint.joint_if_code
307      (Obj.magic (Types.pi1 f_sig).Joint.joint_if_entry)
308  in
309  let code = (Types.pi1 code_sigma).Types.fst in
310  let sigma0 = (Types.pi1 code_sigma).Types.snd in
311  let entry = Nat.O in
312  { Types.fst = { Joint.joint_if_luniverse =
313  (Types.pi1 f_sig).Joint.joint_if_luniverse; Joint.joint_if_runiverse =
314  (Types.pi1 f_sig).Joint.joint_if_runiverse; Joint.joint_if_result =
315  (Types.pi1 f_sig).Joint.joint_if_result; Joint.joint_if_params =
316  (Types.pi1 f_sig).Joint.joint_if_params; Joint.joint_if_stacksize =
317  (Types.pi1 f_sig).Joint.joint_if_stacksize; Joint.joint_if_code = code;
318  Joint.joint_if_entry = (Obj.magic entry) }; Types.snd = sigma0 }
319
320(** val linearise :
321    Joint.unserialized_params -> (Joint.joint_function, Nat.nat) AST.program
322    -> (Joint.joint_function, Nat.nat) AST.program **)
323let linearise p pr =
324  AST.transform_program pr (fun globals ->
325    AST.transf_fundef (fun f_in ->
326      (Types.pi1 (linearise_int_fun p globals f_in)).Types.fst))
327
Note: See TracBrowser for help on using the repository browser.