extracted/rTLToERTL.mli

   1 open Preamble
   2
   3 open Order
   4
   5 open Proper
   6
   7 open PositiveMap
   8
   9 open Deqsets
  10
  11 open ErrorMessages
  12
  13 open PreIdentifiers
  14
  15 open Errors
  16
  17 open Extralib
  18
  19 open Lists
  20
  21 open Positive
  22
  23 open Identifiers
  24
  25 open Registers
  26
  27 open Exp
  28
  29 open Setoids
  30
  31 open Monad
  32
  33 open Option
  34
  35 open Extranat
  36
  37 open Vector
  38
  39 open Div_and_mod
  40
  41 open Russell
  42
  43 open Types
  44
  45 open List
  46
  47 open Util
  48
  49 open FoldStuff
  50
  51 open BitVector
  52
  53 open Arithmetic
  54
  55 open Jmeq
  56
  57 open Bool
  58
  59 open Hints_declaration
  60
  61 open Core_notation
  62
  63 open Pts
  64
  65 open Logic
  66
  67 open Relations
  68
  69 open Nat
  70
  71 open I8051
  72
  73 open RegisterSet
  74
  75 open Extra_bool
  76
  77 open Coqlib
  78
  79 open Values
  80
  81 open FrontEndVal
  82
  83 open GenMem
  84
  85 open FrontEndMem
  86
  87 open Globalenvs
  88
  89 open String
  90
  91 open Sets
  92
  93 open Listb
  94
  95 open LabelledObjects
  96
  97 open BitVectorTrie
  98
  99 open Graphs
 100
 101 open CostLabel
 102
 103 open Hide
 104
 105 open Integers
 106
 107 open AST
 108
 109 open Division
 110
 111 open Z
 112
 113 open BitVectorZ
 114
 115 open Pointers
 116
 117 open ByteValues
 118
 119 open BackEndOps
 120
 121 open Joint
 122
 123 open RTL
 124
 125 open ERTL
 126
 127 open Deqsets_extra
 128
 129 open State
 130
 131 open Bind_new
 132
 133 open BindLists
 134
 135 open Blocks
 136
 137 open TranslateUtils
 138
 139 val save_hdws :
 140   AST.ident List.list -> (Registers.register, I8051.register) Types.prod
 141   List.list -> Joint.joint_seq List.list
 142
 143 val restore_hdws :
 144   AST.ident List.list -> (Joint.psd_argument, I8051.register) Types.prod
 145   List.list -> Joint.joint_seq List.list
 146
 147 val get_params_hdw :
 148   AST.ident List.list -> Registers.register List.list -> Joint.joint_seq
 149   List.list
 150
 151 val get_param_stack :
 152   AST.ident List.list -> Registers.register -> Registers.register ->
 153   Registers.register -> Joint.joint_seq List.list
 154
 155 val get_params_stack :
 156   AST.ident List.list -> Registers.register -> Registers.register ->
 157   Registers.register -> Registers.register List.list -> Joint.joint_seq
 158   List.list
 159
 160 val get_params :
 161   AST.ident List.list -> Registers.register -> Registers.register ->
 162   Registers.register -> Registers.register List.list -> Joint.joint_seq
 163   List.list
 164
 165 val save_return :
 166   AST.ident List.list -> Joint.psd_argument List.list -> Joint.joint_seq
 167   List.list
 168
 169 val assign_result : AST.ident List.list -> Joint.joint_seq List.list
 170
 171 val epilogue :
 172   AST.ident List.list -> Registers.register List.list -> Registers.register
 173   -> Registers.register -> (Registers.register, I8051.register) Types.prod
 174   List.list -> Joint.joint_seq List.list Types.sig0
 175
 176 val prologue :
 177   AST.ident List.list -> Registers.register List.list -> Registers.register
 178   -> Registers.register -> Registers.register -> Registers.register ->
 179   Registers.register -> (Registers.register, I8051.register) Types.prod
 180   List.list -> (Registers.register, Joint.joint_seq List.list)
 181   Bind_new.bind_new
 182
 183 val set_params_hdw :
 184   AST.ident List.list -> Joint.psd_argument List.list -> Joint.joint_seq
 185   List.list
 186
 187 val set_param_stack :
 188   AST.ident List.list -> Registers.register -> Registers.register ->
 189   Joint.psd_argument -> Joint.joint_seq List.list
 190
 191 val set_params_stack :
 192   AST.ident List.list -> Joint.psd_argument List.list -> (Registers.register,
 193   Joint.joint_seq List.list) Bind_new.bind_new
 194
 195 val set_params :
 196   AST.ident List.list -> Joint.psd_argument List.list -> (Registers.register,
 197   Joint.joint_seq List.list) Bind_new.bind_new Types.sig0
 198
 199 val fetch_result :
 200   AST.ident List.list -> Registers.register List.list -> Joint.joint_seq
 201   List.list Types.sig0
 202
 203 val translate_step :
 204   AST.ident List.list -> Graphs.label -> Joint.joint_step ->
 205   Blocks.bind_step_block
 206
 207 val translate_fin_step :
 208   AST.ident List.list -> Registers.register List.list -> Registers.register
 209   -> Registers.register -> (Registers.register, I8051.register) Types.prod
 210   List.list -> Graphs.label -> Joint.joint_fin_step -> Blocks.bind_fin_block
 211
 212 val allocate_regs :
 213   ((Registers.register, I8051.register) Types.prod List.list ->
 214   (Registers.register, 'a1) Bind_new.bind_new) -> (Registers.register, 'a1)
 215   Bind_new.bind_new
 216
 217 val translate_data :
 218   AST.ident List.list -> Joint.joint_closed_internal_function ->
 219   TranslateUtils.bound_b_graph_translate_data
 220
 221 val rtl_to_ertl : RTL.rtl_program -> ERTL.ertl_program
 222