source: extracted/linearise.ml @ 2773

Last change on this file since 2773 was 2773, checked in by sacerdot, 7 years ago
  1. everything extracted again after all bugs in Matita's extraction have been fixed. No more need for manual patching
  2. new extraction after file reorganization (by James)
File size: 10.8 KB
RevLine 
[2717]1open Preamble
2
3open String
4
5open Sets
6
7open Listb
8
9open LabelledObjects
10
[2773]11open BitVectorTrie
12
[2717]13open Graphs
14
15open I8051
16
17open Order
18
19open Registers
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 Lists
40
41open Identifiers
42
43open Integers
44
45open AST
46
47open Division
48
49open Exp
50
51open Arithmetic
52
[2773]53open Setoids
54
55open Monad
56
57open Option
58
[2717]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) ->
[2773]117     (match Identifiers.member PreIdentifiers.LabelTag visited
[2717]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
[2773]135       (Monad.m_return0 (Monad.max_def Option.option) { Types.fst = x;
[2717]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 **)
[2773]147let rec graph_visit p globals g required visited generated visiting gen_length n entry =
148  (match chop (fun x -> Identifiers.member PreIdentifiers.LabelTag visited x)
149           visiting with
[2717]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 =
[2773]166              Identifiers.lookup_safe PreIdentifiers.LabelTag (Obj.magic g)
[2717]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 ->
[2773]192                   (match Identifiers.member PreIdentifiers.LabelTag visited'
193                            (Obj.magic nxt) with
[2717]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) ->
[2773]207                   (match Identifiers.member PreIdentifiers.LabelTag visited'
208                            (Obj.magic nxt) with
[2717]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 ->
[2773]226                   (match Identifiers.member PreIdentifiers.LabelTag visited'
227                            (Obj.magic nxt) with
[2717]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
[2773]249            graph_visit p globals g
[2717]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 -> __ **)
[2773]260let branch_compress p globals g entry =
261  g
[2717]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 =
[2773]271    (Monad.m_bind0 (Monad.max_def Option.option) l_opt (fun l ->
[2717]272      match test l with
[2773]273      | Bool.True -> Monad.m_return0 (Monad.max_def Option.option) l
[2717]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 **)
[2773]280let linearise_code p globals g entry_sig =
281  let g0 = branch_compress p globals g entry_sig in
[2717]282  let triple =
[2773]283    graph_visit p globals g0 (Identifiers.empty_set PreIdentifiers.LabelTag)
[2717]284      (Identifiers.empty_map PreIdentifiers.LabelTag) (Obj.magic List.Nil)
285      (List.Cons ((Types.pi1 entry_sig), List.Nil)) Nat.O
[2773]286      (Identifiers.id_map_size PreIdentifiers.LabelTag (Obj.magic g0))
[2717]287      (Types.pi1 entry_sig)
288  in
[2773]289  let sigma = triple.Types.fst.Types.fst in
[2717]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 ->
[2773]296      Identifiers.member PreIdentifiers.LabelTag required l) lbld_code));
297  Types.snd = (Identifiers.lookup PreIdentifiers.LabelTag sigma) }
[2717]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
[2773]310  let sigma = (Types.pi1 code_sigma).Types.snd in
[2717]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;
[2773]318  Joint.joint_if_entry = (Obj.magic entry) }; Types.snd = sigma }
[2717]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.