source: extracted/eRTLToERTLptr.ml @ 2817

Last change on this file since 2817 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: 4.4 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
107open ERTL
108
109open ERTLptr
110
[2730]111open Deqsets_extra
[2717]112
113open State
114
115open Bind_new
116
117open BindLists
118
119open Blocks
120
121open TranslateUtils
122
123(** val seq_embed :
124    AST.ident List.list -> Joint.joint_seq -> Joint.joint_seq **)
125let seq_embed globals = function
126| Joint.COMMENT s0 -> Joint.COMMENT s0
127| Joint.MOVE a -> Joint.MOVE a
128| Joint.POP a -> Joint.POP a
129| Joint.PUSH a -> Joint.PUSH a
130| Joint.ADDRESS (i, reg1, reg2) -> Joint.ADDRESS (i, reg1, reg2)
[2773]131| Joint.OPACCS (op, reg1, reg2, reg3, reg4) ->
132  Joint.OPACCS (op, reg1, reg2, reg3, reg4)
133| Joint.OP1 (op, reg1, reg2) -> Joint.OP1 (op, reg1, reg2)
134| Joint.OP2 (op, reg1, reg2, arg) -> Joint.OP2 (op, reg1, reg2, arg)
[2717]135| Joint.CLEAR_CARRY -> Joint.CLEAR_CARRY
136| Joint.SET_CARRY -> Joint.SET_CARRY
137| Joint.LOAD (reg1, reg2, reg3) -> Joint.LOAD (reg1, reg2, reg3)
138| Joint.STORE (arg1, arg2, reg) -> Joint.STORE (arg1, arg2, reg)
139| Joint.Extension_seq s0 ->
140  Joint.Extension_seq (Obj.magic (ERTLptr.Ertlptr_ertl (Obj.magic s0)))
141
142(** val translate_step :
143    AST.ident List.list -> Graphs.label -> Joint.joint_step ->
144    Blocks.bind_step_block **)
145let translate_step globals l = function
146| Joint.COST_LABEL c ->
147  Bind_new.Bret { Types.fst = { Types.fst = List.Nil; Types.snd = (fun x ->
148    Joint.COST_LABEL c) }; Types.snd = List.Nil }
149| Joint.CALL (called, args, dest) ->
150  (match called with
151   | Types.Inl id ->
152     Bind_new.Bret { Types.fst = { Types.fst = List.Nil; Types.snd =
153       (fun x -> Joint.CALL ((Types.Inl id), args, dest)) }; Types.snd =
154       List.Nil }
155   | Types.Inr dest1 ->
156     Bind_new.Bnew (fun reg -> Bind_new.Bret { Types.fst = { Types.fst =
157       (List.Cons ((fun l0 ->
158       let x =
159         ERTLptr.ertlptr_seq_joint globals
160           (Obj.magic (ERTLptr.LOW_ADDRESS (reg, (Obj.magic l0))))
161       in
162       x), (List.Cons ((fun x -> Joint.PUSH (Obj.magic (Joint.Reg reg))),
163       (List.Cons ((fun l0 ->
164       ERTLptr.ertlptr_seq_joint globals
165         (Obj.magic (ERTLptr.HIGH_ADDRESS (reg, (Obj.magic l0))))),
166       (List.Cons ((fun x -> Joint.PUSH (Obj.magic (Joint.Reg reg))),
167       List.Nil)))))))); Types.snd = (fun x -> Joint.CALL ((Types.Inr dest1),
168       args, dest)) }; Types.snd = List.Nil }))
169| Joint.COND (reg, l0) ->
170  Bind_new.Bret { Types.fst = { Types.fst = List.Nil; Types.snd = (fun x ->
171    Joint.COND (reg, l0)) }; Types.snd = List.Nil }
172| Joint.Step_seq x ->
173  Bind_new.Bret
174    (Blocks.ensure_step_block (Joint.graph_params_to_params ERTLptr.eRTLptr)
175      globals (List.Cons ((seq_embed globals x), List.Nil)))
176
177(** val fin_step_embed : Joint.joint_fin_step -> Joint.joint_fin_step **)
178let fin_step_embed = function
179| Joint.GOTO l -> Joint.GOTO l
180| Joint.RETURN -> Joint.RETURN
181| Joint.TAILCALL (arg, arg') -> Joint.TAILCALL (arg, arg')
182
183(** val translate_fin_step :
184    AST.ident List.list -> Graphs.label -> Joint.joint_fin_step ->
185    Blocks.bind_fin_block **)
186let translate_fin_step globals l s =
187  Bind_new.Bret { Types.fst = List.Nil; Types.snd = (fin_step_embed s) }
188
189(** val translate_data :
190    AST.ident List.list -> Joint.joint_closed_internal_function ->
191    (Registers.register, TranslateUtils.b_graph_translate_data)
192    Bind_new.bind_new **)
193let translate_data globals def =
194  Bind_new.Bret { TranslateUtils.init_ret =
195    (Types.pi1 def).Joint.joint_if_result; TranslateUtils.init_params =
196    (Types.pi1 def).Joint.joint_if_params; TranslateUtils.init_stack_size =
197    (Types.pi1 def).Joint.joint_if_stacksize; TranslateUtils.added_prologue =
198    List.Nil; TranslateUtils.f_step = (translate_step globals);
199    TranslateUtils.f_fin = (translate_fin_step globals) }
200
201(** val ertl_to_ertlptr : ERTL.ertl_program -> ERTLptr.ertlptr_program **)
202let ertl_to_ertlptr =
203  TranslateUtils.b_graph_transform_program ERTL.eRTL ERTLptr.eRTLptr
204    translate_data
205
Note: See TracBrowser for help on using the repository browser.