extracted/eRTLToLTL.ml

   1 open Preamble
   2
   3 open Extra_bool
   4
   5 open Coqlib
   6
   7 open Values
   8
   9 open FrontEndVal
  10
  11 open GenMem
  12
  13 open FrontEndMem
  14
  15 open Globalenvs
  16
  17 open String
  18
  19 open Sets
  20
  21 open Listb
  22
  23 open LabelledObjects
  24
  25 open BitVectorTrie
  26
  27 open Graphs
  28
  29 open I8051
  30
  31 open Order
  32
  33 open Registers
  34
  35 open CostLabel
  36
  37 open Hide
  38
  39 open Proper
  40
  41 open PositiveMap
  42
  43 open Deqsets
  44
  45 open ErrorMessages
  46
  47 open PreIdentifiers
  48
  49 open Errors
  50
  51 open Extralib
  52
  53 open Lists
  54
  55 open Identifiers
  56
  57 open Integers
  58
  59 open AST
  60
  61 open Division
  62
  63 open Exp
  64
  65 open Arithmetic
  66
  67 open Setoids
  68
  69 open Monad
  70
  71 open Option
  72
  73 open Extranat
  74
  75 open Vector
  76
  77 open Div_and_mod
  78
  79 open Jmeq
  80
  81 open Russell
  82
  83 open List
  84
  85 open Util
  86
  87 open FoldStuff
  88
  89 open BitVector
  90
  91 open Types
  92
  93 open Bool
  94
  95 open Relations
  96
  97 open Nat
  98
  99 open Hints_declaration
 100
 101 open Core_notation
 102
 103 open Pts
 104
 105 open Logic
 106
 107 open Positive
 108
 109 open Z
 110
 111 open BitVectorZ
 112
 113 open Pointers
 114
 115 open ByteValues
 116
 117 open BackEndOps
 118
 119 open Joint
 120
 121 open Joint_LTL_LIN
 122
 123 open LTL
 124
 125 open Fixpoints
 126
 127 open Set_adt
 128
 129 open ERTL
 130
 131 open Liveness
 132
 133 open Interference
 134
 135 open Deqsets_extra
 136
 137 open State
 138
 139 open Bind_new
 140
 141 open BindLists
 142
 143 open Blocks
 144
 145 open TranslateUtils
 146
 147 (** val dpi1__o__Reg_to_dec__o__inject :
 148     (I8051.register, 'a1) Types.dPair -> Interference.decision Types.sig0 **)
 149 let dpi1__o__Reg_to_dec__o__inject x2 =
 150   Interference.Decision_colour x2.Types.dpi1
 151
 152 (** val eject__o__Reg_to_dec__o__inject :
 153     I8051.register Types.sig0 -> Interference.decision Types.sig0 **)
 154 let eject__o__Reg_to_dec__o__inject x2 =
 155   Interference.Decision_colour (Types.pi1 x2)
 156
 157 (** val reg_to_dec__o__inject :
 158     I8051.register -> Interference.decision Types.sig0 **)
 159 let reg_to_dec__o__inject x1 =
 160   Interference.Decision_colour x1
 161
 162 (** val dpi1__o__Reg_to_dec :
 163     (I8051.register, 'a1) Types.dPair -> Interference.decision **)
 164 let dpi1__o__Reg_to_dec x1 =
 165   Interference.Decision_colour x1.Types.dpi1
 166
 167 (** val eject__o__Reg_to_dec :
 168     I8051.register Types.sig0 -> Interference.decision **)
 169 let eject__o__Reg_to_dec x1 =
 170   Interference.Decision_colour (Types.pi1 x1)
 171
 172 type arg_decision =
 173 | Arg_decision_colour of I8051.register
 174 | Arg_decision_spill of Nat.nat
 175 | Arg_decision_imm of BitVector.byte
 176
 177 (** val arg_decision_rect_Type4 :
 178     (I8051.register -> 'a1) -> (Nat.nat -> 'a1) -> (BitVector.byte -> 'a1) ->
 179     arg_decision -> 'a1 **)
 180 let rec arg_decision_rect_Type4 h_arg_decision_colour h_arg_decision_spill h_arg_decision_imm = function
 181 | Arg_decision_colour x_19045 -> h_arg_decision_colour x_19045
 182 | Arg_decision_spill x_19046 -> h_arg_decision_spill x_19046
 183 | Arg_decision_imm x_19047 -> h_arg_decision_imm x_19047
 184
 185 (** val arg_decision_rect_Type5 :
 186     (I8051.register -> 'a1) -> (Nat.nat -> 'a1) -> (BitVector.byte -> 'a1) ->
 187     arg_decision -> 'a1 **)
 188 let rec arg_decision_rect_Type5 h_arg_decision_colour h_arg_decision_spill h_arg_decision_imm = function
 189 | Arg_decision_colour x_19052 -> h_arg_decision_colour x_19052
 190 | Arg_decision_spill x_19053 -> h_arg_decision_spill x_19053
 191 | Arg_decision_imm x_19054 -> h_arg_decision_imm x_19054
 192
 193 (** val arg_decision_rect_Type3 :
 194     (I8051.register -> 'a1) -> (Nat.nat -> 'a1) -> (BitVector.byte -> 'a1) ->
 195     arg_decision -> 'a1 **)
 196 let rec arg_decision_rect_Type3 h_arg_decision_colour h_arg_decision_spill h_arg_decision_imm = function
 197 | Arg_decision_colour x_19059 -> h_arg_decision_colour x_19059
 198 | Arg_decision_spill x_19060 -> h_arg_decision_spill x_19060
 199 | Arg_decision_imm x_19061 -> h_arg_decision_imm x_19061
 200
 201 (** val arg_decision_rect_Type2 :
 202     (I8051.register -> 'a1) -> (Nat.nat -> 'a1) -> (BitVector.byte -> 'a1) ->
 203     arg_decision -> 'a1 **)
 204 let rec arg_decision_rect_Type2 h_arg_decision_colour h_arg_decision_spill h_arg_decision_imm = function
 205 | Arg_decision_colour x_19066 -> h_arg_decision_colour x_19066
 206 | Arg_decision_spill x_19067 -> h_arg_decision_spill x_19067
 207 | Arg_decision_imm x_19068 -> h_arg_decision_imm x_19068
 208
 209 (** val arg_decision_rect_Type1 :
 210     (I8051.register -> 'a1) -> (Nat.nat -> 'a1) -> (BitVector.byte -> 'a1) ->
 211     arg_decision -> 'a1 **)
 212 let rec arg_decision_rect_Type1 h_arg_decision_colour h_arg_decision_spill h_arg_decision_imm = function
 213 | Arg_decision_colour x_19073 -> h_arg_decision_colour x_19073
 214 | Arg_decision_spill x_19074 -> h_arg_decision_spill x_19074
 215 | Arg_decision_imm x_19075 -> h_arg_decision_imm x_19075
 216
 217 (** val arg_decision_rect_Type0 :
 218     (I8051.register -> 'a1) -> (Nat.nat -> 'a1) -> (BitVector.byte -> 'a1) ->
 219     arg_decision -> 'a1 **)
 220 let rec arg_decision_rect_Type0 h_arg_decision_colour h_arg_decision_spill h_arg_decision_imm = function
 221 | Arg_decision_colour x_19080 -> h_arg_decision_colour x_19080
 222 | Arg_decision_spill x_19081 -> h_arg_decision_spill x_19081
 223 | Arg_decision_imm x_19082 -> h_arg_decision_imm x_19082
 224
 225 (** val arg_decision_inv_rect_Type4 :
 226     arg_decision -> (I8051.register -> __ -> 'a1) -> (Nat.nat -> __ -> 'a1)
 227     -> (BitVector.byte -> __ -> 'a1) -> 'a1 **)
 228 let arg_decision_inv_rect_Type4 hterm h1 h2 h3 =
 229   let hcut = arg_decision_rect_Type4 h1 h2 h3 hterm in hcut __
 230
 231 (** val arg_decision_inv_rect_Type3 :
 232     arg_decision -> (I8051.register -> __ -> 'a1) -> (Nat.nat -> __ -> 'a1)
 233     -> (BitVector.byte -> __ -> 'a1) -> 'a1 **)
 234 let arg_decision_inv_rect_Type3 hterm h1 h2 h3 =
 235   let hcut = arg_decision_rect_Type3 h1 h2 h3 hterm in hcut __
 236
 237 (** val arg_decision_inv_rect_Type2 :
 238     arg_decision -> (I8051.register -> __ -> 'a1) -> (Nat.nat -> __ -> 'a1)
 239     -> (BitVector.byte -> __ -> 'a1) -> 'a1 **)
 240 let arg_decision_inv_rect_Type2 hterm h1 h2 h3 =
 241   let hcut = arg_decision_rect_Type2 h1 h2 h3 hterm in hcut __
 242
 243 (** val arg_decision_inv_rect_Type1 :
 244     arg_decision -> (I8051.register -> __ -> 'a1) -> (Nat.nat -> __ -> 'a1)
 245     -> (BitVector.byte -> __ -> 'a1) -> 'a1 **)
 246 let arg_decision_inv_rect_Type1 hterm h1 h2 h3 =
 247   let hcut = arg_decision_rect_Type1 h1 h2 h3 hterm in hcut __
 248
 249 (** val arg_decision_inv_rect_Type0 :
 250     arg_decision -> (I8051.register -> __ -> 'a1) -> (Nat.nat -> __ -> 'a1)
 251     -> (BitVector.byte -> __ -> 'a1) -> 'a1 **)
 252 let arg_decision_inv_rect_Type0 hterm h1 h2 h3 =
 253   let hcut = arg_decision_rect_Type0 h1 h2 h3 hterm in hcut __
 254
 255 (** val arg_decision_discr : arg_decision -> arg_decision -> __ **)
 256 let arg_decision_discr x y =
 257   Logic.eq_rect_Type2 x
 258     (match x with
 259      | Arg_decision_colour a0 -> Obj.magic (fun _ dH -> dH __)
 260      | Arg_decision_spill a0 -> Obj.magic (fun _ dH -> dH __)
 261      | Arg_decision_imm a0 -> Obj.magic (fun _ dH -> dH __)) y
 262
 263 (** val arg_decision_jmdiscr : arg_decision -> arg_decision -> __ **)
 264 let arg_decision_jmdiscr x y =
 265   Logic.eq_rect_Type2 x
 266     (match x with
 267      | Arg_decision_colour a0 -> Obj.magic (fun _ dH -> dH __)
 268      | Arg_decision_spill a0 -> Obj.magic (fun _ dH -> dH __)
 269      | Arg_decision_imm a0 -> Obj.magic (fun _ dH -> dH __)) y
 270
 271 (** val dpi1__o__Reg_to_arg_dec__o__inject :
 272     (I8051.register, 'a1) Types.dPair -> arg_decision Types.sig0 **)
 273 let dpi1__o__Reg_to_arg_dec__o__inject x2 =
 274   Arg_decision_colour x2.Types.dpi1
 275
 276 (** val eject__o__Reg_to_arg_dec__o__inject :
 277     I8051.register Types.sig0 -> arg_decision Types.sig0 **)
 278 let eject__o__Reg_to_arg_dec__o__inject x2 =
 279   Arg_decision_colour (Types.pi1 x2)
 280
 281 (** val reg_to_arg_dec__o__inject :
 282     I8051.register -> arg_decision Types.sig0 **)
 283 let reg_to_arg_dec__o__inject x1 =
 284   Arg_decision_colour x1
 285
 286 (** val dpi1__o__Reg_to_arg_dec :
 287     (I8051.register, 'a1) Types.dPair -> arg_decision **)
 288 let dpi1__o__Reg_to_arg_dec x1 =
 289   Arg_decision_colour x1.Types.dpi1
 290
 291 (** val eject__o__Reg_to_arg_dec :
 292     I8051.register Types.sig0 -> arg_decision **)
 293 let eject__o__Reg_to_arg_dec x1 =
 294   Arg_decision_colour (Types.pi1 x1)
 295
 296 (** val preserve_carry_bit :
 297     AST.ident List.list -> Bool.bool -> Joint.joint_seq List.list ->
 298     Joint.joint_seq List.list **)
 299 let preserve_carry_bit globals do_it steps =
 300   match do_it with
 301   | Bool.True ->
 302     List.Cons ((Joint.Extension_seq (Obj.magic Joint_LTL_LIN.SAVE_CARRY)),
 303       (List.append steps (List.Cons ((Joint.Extension_seq
 304         (Obj.magic Joint_LTL_LIN.RESTORE_CARRY)), List.Nil))))
 305   | Bool.False -> steps
 306
 307 (** val a : Types.unit0 **)
 308 let a =
 309   Types.It
 310
 311 (** val dpi1__o__beval_of_byte__o__inject :
 312     (BitVector.byte, 'a1) Types.dPair -> ByteValues.beval Types.sig0 **)
 313 let dpi1__o__beval_of_byte__o__inject x2 =
 314   ByteValues.BVByte x2.Types.dpi1
 315
 316 (** val eject__o__beval_of_byte__o__inject :
 317     BitVector.byte Types.sig0 -> ByteValues.beval Types.sig0 **)
 318 let eject__o__beval_of_byte__o__inject x2 =
 319   ByteValues.BVByte (Types.pi1 x2)
 320
 321 (** val beval_of_byte__o__inject :
 322     BitVector.byte -> ByteValues.beval Types.sig0 **)
 323 let beval_of_byte__o__inject x1 =
 324   ByteValues.BVByte x1
 325
 326 (** val dpi1__o__beval_of_byte :
 327     (BitVector.byte, 'a1) Types.dPair -> ByteValues.beval **)
 328 let dpi1__o__beval_of_byte x1 =
 329   ByteValues.BVByte x1.Types.dpi1
 330
 331 (** val eject__o__beval_of_byte :
 332     BitVector.byte Types.sig0 -> ByteValues.beval **)
 333 let eject__o__beval_of_byte x1 =
 334   ByteValues.BVByte (Types.pi1 x1)
 335
 336 (** val set_dp_by_offset :
 337     AST.ident List.list -> Nat.nat -> Joint.joint_seq List.list **)
 338 let set_dp_by_offset globals off =
 339   List.Cons ((Joint.MOVE
 340     (Obj.magic (Joint_LTL_LIN.Int_to_acc (a, (Joint.byte_of_nat off))))),
 341     (List.Cons ((Joint.OP2 (BackEndOps.Add, (Obj.magic a), (Obj.magic a),
 342     (Obj.magic (Joint.hdw_argument_from_reg I8051.registerSPL)))), (List.Cons
 343     ((Joint.MOVE
 344     (Obj.magic (Joint_LTL_LIN.From_acc (I8051.RegisterDPL, a)))), (List.Cons
 345     ((Joint.MOVE
 346     (Obj.magic (Joint_LTL_LIN.Int_to_acc (a, Joint.zero_byte)))), (List.Cons
 347     ((Joint.OP2 (BackEndOps.Addc, (Obj.magic a), (Obj.magic a),
 348     (Obj.magic (Joint.hdw_argument_from_reg I8051.registerSPH)))), (List.Cons
 349     ((Joint.MOVE
 350     (Obj.magic (Joint_LTL_LIN.From_acc (I8051.RegisterDPH, a)))),
 351     List.Nil)))))))))))
 352
 353 (** val get_stack :
 354     AST.ident List.list -> Nat.nat -> I8051.register -> Nat.nat ->
 355     Joint.joint_seq List.list **)
 356 let get_stack globals localss r off =
 357   let off0 = Nat.plus localss off in
 358   List.append (set_dp_by_offset globals off0)
 359     (List.append (List.Cons ((Joint.LOAD ((Obj.magic a),
 360       (Obj.magic Types.It), (Obj.magic Types.It))), List.Nil))
 361       (match I8051.eq_Register r I8051.RegisterA with
 362        | Bool.True -> List.Nil
 363        | Bool.False ->
 364          List.Cons ((Joint.MOVE (Obj.magic (Joint_LTL_LIN.From_acc (r, a)))),
 365            List.Nil)))
 366
 367 (** val set_stack_not_a :
 368     AST.ident List.list -> Nat.nat -> Nat.nat -> I8051.register ->
 369     Joint.joint_seq List.list **)
 370 let set_stack_not_a globals localss off r =
 371   let off0 = Nat.plus localss off in
 372   List.append (set_dp_by_offset globals off0) (List.Cons ((Joint.MOVE
 373     (Obj.magic (Joint_LTL_LIN.To_acc (a, r)))), (List.Cons ((Joint.STORE
 374     ((Obj.magic Types.It), (Obj.magic Types.It), (Obj.magic a))),
 375     List.Nil))))
 376
 377 (** val set_stack_a :
 378     AST.ident List.list -> Nat.nat -> Nat.nat -> Joint.joint_seq List.list **)
 379 let set_stack_a globals localss off =
 380   List.append (List.Cons ((Joint.MOVE
 381     (Obj.magic (Joint_LTL_LIN.From_acc (I8051.registerST1, a)))), List.Nil))
 382     (set_stack_not_a globals localss off I8051.registerST1)
 383
 384 (** val set_stack :
 385     AST.ident List.list -> Nat.nat -> Nat.nat -> I8051.register ->
 386     Joint.joint_seq List.list **)
 387 let set_stack globals localss off r =
 388   match I8051.eq_Register r I8051.RegisterA with
 389   | Bool.True -> set_stack_a globals localss off
 390   | Bool.False -> set_stack_not_a globals localss off r
 391
 392 (** val set_stack_int :
 393     AST.ident List.list -> Nat.nat -> Nat.nat -> BitVector.byte ->
 394     Joint.joint_seq List.list **)
 395 let set_stack_int globals localss off int =
 396   let off0 = Nat.plus localss off in
 397   List.append (set_dp_by_offset globals off0) (List.Cons ((Joint.MOVE
 398     (Obj.magic (Joint_LTL_LIN.Int_to_acc (a, int)))), (List.Cons
 399     ((Joint.STORE ((Obj.magic Types.It), (Obj.magic Types.It),
 400     (Obj.magic a))), List.Nil))))
 401
 402 (** val move :
 403     AST.ident List.list -> Nat.nat -> Bool.bool -> Interference.decision ->
 404     arg_decision -> Joint.joint_seq List.list **)
 405 let move globals localss carry_lives_after dst src =
 406   match dst with
 407   | Interference.Decision_spill dsto ->
 408     (match src with
 409      | Arg_decision_colour srcr ->
 410        preserve_carry_bit globals carry_lives_after
 411          (set_stack globals localss dsto srcr)
 412      | Arg_decision_spill srco ->
 413        (match Nat.eqb srco dsto with
 414         | Bool.True -> List.Nil
 415         | Bool.False ->
 416           preserve_carry_bit globals carry_lives_after
 417             (List.append (get_stack globals localss I8051.RegisterA srco)
 418               (set_stack globals localss dsto I8051.RegisterA)))
 419      | Arg_decision_imm int ->
 420        preserve_carry_bit globals carry_lives_after
 421          (set_stack_int globals localss dsto int))
 422   | Interference.Decision_colour dstr ->
 423     (match src with
 424      | Arg_decision_colour srcr ->
 425        (match I8051.eq_Register dstr srcr with
 426         | Bool.True -> List.Nil
 427         | Bool.False ->
 428           (match I8051.eq_Register dstr I8051.RegisterA with
 429            | Bool.True ->
 430              List.Cons ((Joint.MOVE
 431                (Obj.magic (Joint_LTL_LIN.To_acc (a, srcr)))), List.Nil)
 432            | Bool.False ->
 433              (match I8051.eq_Register srcr I8051.RegisterA with
 434               | Bool.True ->
 435                 List.Cons ((Joint.MOVE
 436                   (Obj.magic (Joint_LTL_LIN.From_acc (dstr, a)))), List.Nil)
 437               | Bool.False ->
 438                 List.Cons ((Joint.MOVE
 439                   (Obj.magic (Joint_LTL_LIN.To_acc (a, srcr)))), (List.Cons
 440                   ((Joint.MOVE
 441                   (Obj.magic (Joint_LTL_LIN.From_acc (dstr, a)))),
 442                   List.Nil))))))
 443      | Arg_decision_spill srco ->
 444        preserve_carry_bit globals carry_lives_after
 445          (get_stack globals localss dstr srco)
 446      | Arg_decision_imm int ->
 447        List.append (List.Cons ((Joint.MOVE
 448          (Obj.magic (Joint_LTL_LIN.Int_to_acc (a, int)))), List.Nil))
 449          (match I8051.eq_Register dstr I8051.RegisterA with
 450           | Bool.True -> List.Nil
 451           | Bool.False ->
 452             List.Cons ((Joint.MOVE
 453               (Obj.magic (Joint_LTL_LIN.From_acc (dstr, a)))), List.Nil)))
 454
 455 (** val arg_is_spilled : arg_decision -> Bool.bool **)
 456 let arg_is_spilled = function
 457 | Arg_decision_colour x0 -> Bool.False
 458 | Arg_decision_spill x0 -> Bool.True
 459 | Arg_decision_imm x0 -> Bool.False
 460
 461 (** val is_spilled : Interference.decision -> Bool.bool **)
 462 let is_spilled = function
 463 | Interference.Decision_spill x0 -> Bool.True
 464 | Interference.Decision_colour x0 -> Bool.False
 465
 466 (** val newframe :
 467     AST.ident List.list -> Nat.nat -> Joint.joint_seq List.list **)
 468 let newframe globals stack_sz =
 469   List.Cons (Joint.CLEAR_CARRY, (List.Cons ((Joint.MOVE
 470     (Obj.magic (Joint_LTL_LIN.To_acc (a, I8051.registerSPL)))), (List.Cons
 471     ((Joint.OP2 (BackEndOps.Sub, (Obj.magic a), (Obj.magic a),
 472     (Obj.magic (Joint.hdw_argument_from_byte (Joint.byte_of_nat stack_sz))))),
 473     (List.Cons ((Joint.MOVE
 474     (Obj.magic (Joint_LTL_LIN.From_acc (I8051.registerSPL, a)))), (List.Cons
 475     ((Joint.MOVE (Obj.magic (Joint_LTL_LIN.To_acc (a, I8051.registerSPH)))),
 476     (List.Cons ((Joint.OP2 (BackEndOps.Sub, (Obj.magic a), (Obj.magic a),
 477     (Obj.magic (Joint.hdw_argument_from_byte Joint.zero_byte)))), (List.Cons
 478     ((Joint.MOVE
 479     (Obj.magic (Joint_LTL_LIN.From_acc (I8051.registerSPH, a)))),
 480     List.Nil)))))))))))))
 481
 482 (** val delframe :
 483     AST.ident List.list -> Nat.nat -> Joint.joint_seq List.list **)
 484 let delframe globals stack_sz =
 485   List.Cons ((Joint.MOVE
 486     (Obj.magic (Joint_LTL_LIN.To_acc (a, I8051.registerSPL)))), (List.Cons
 487     ((Joint.OP2 (BackEndOps.Add, (Obj.magic a), (Obj.magic a),
 488     (Obj.magic (Joint.hdw_argument_from_byte (Joint.byte_of_nat stack_sz))))),
 489     (List.Cons ((Joint.MOVE
 490     (Obj.magic (Joint_LTL_LIN.From_acc (I8051.registerSPL, a)))), (List.Cons
 491     ((Joint.MOVE (Obj.magic (Joint_LTL_LIN.To_acc (a, I8051.registerSPH)))),
 492     (List.Cons ((Joint.OP2 (BackEndOps.Addc, (Obj.magic a), (Obj.magic a),
 493     (Obj.magic (Joint.hdw_argument_from_byte Joint.zero_byte)))), (List.Cons
 494     ((Joint.MOVE
 495     (Obj.magic (Joint_LTL_LIN.From_acc (I8051.registerSPH, a)))),
 496     List.Nil)))))))))))
 497
 498 (** val commutative : BackEndOps.op2 -> Bool.bool **)
 499 let commutative = function
 500 | BackEndOps.Add -> Bool.True
 501 | BackEndOps.Addc -> Bool.True
 502 | BackEndOps.Sub -> Bool.False
 503 | BackEndOps.And -> Bool.True
 504 | BackEndOps.Or -> Bool.True
 505 | BackEndOps.Xor -> Bool.True
 506
 507 (** val uses_carry : BackEndOps.op2 -> Bool.bool **)
 508 let uses_carry = function
 509 | BackEndOps.Add -> Bool.False
 510 | BackEndOps.Addc -> Bool.True
 511 | BackEndOps.Sub -> Bool.True
 512 | BackEndOps.And -> Bool.False
 513 | BackEndOps.Or -> Bool.False
 514 | BackEndOps.Xor -> Bool.False
 515
 516 (** val sets_carry : BackEndOps.op2 -> Bool.bool **)
 517 let sets_carry = function
 518 | BackEndOps.Add -> Bool.True
 519 | BackEndOps.Addc -> Bool.True
 520 | BackEndOps.Sub -> Bool.True
 521 | BackEndOps.And -> Bool.False
 522 | BackEndOps.Or -> Bool.False
 523 | BackEndOps.Xor -> Bool.False
 524
 525 (** val translate_op2 :
 526     AST.ident List.list -> Nat.nat -> Bool.bool -> BackEndOps.op2 ->
 527     Interference.decision -> arg_decision -> arg_decision -> Joint.joint_seq
 528     List.list **)
 529 let translate_op2 globals localss carry_lives_after op dst arg1 arg2 =
 530   List.append
 531     (preserve_carry_bit globals
 532       (Bool.andb (uses_carry op)
 533         (Bool.orb (arg_is_spilled arg1) (arg_is_spilled arg2)))
 534       (List.append
 535         (move globals localss Bool.False (Interference.Decision_colour
 536           I8051.RegisterB) arg2)
 537         (move globals localss Bool.False (Interference.Decision_colour
 538           I8051.RegisterA) arg1)))
 539     (List.append (List.Cons ((Joint.OP2 (op, (Obj.magic a), (Obj.magic a),
 540       (Obj.magic (Joint.hdw_argument_from_reg I8051.RegisterB)))), List.Nil))
 541       (move globals localss (Bool.andb (sets_carry op) carry_lives_after) dst
 542         (Arg_decision_colour I8051.RegisterA)))
 543
 544 (** val translate_op2_smart :
 545     AST.ident List.list -> Nat.nat -> Bool.bool -> BackEndOps.op2 ->
 546     Interference.decision -> arg_decision -> arg_decision -> Joint.joint_seq
 547     List.list **)
 548 let translate_op2_smart globals localss carry_lives_after op dst arg1 arg2 =
 549   preserve_carry_bit globals
 550     (Bool.andb (Bool.andb (Bool.notb (sets_carry op)) carry_lives_after)
 551       (Bool.orb (Bool.orb (arg_is_spilled arg1) (arg_is_spilled arg2))
 552         (is_spilled dst)))
 553     (match arg2 with
 554      | Arg_decision_colour arg2r ->
 555        List.append
 556          (move globals localss (uses_carry op) (Interference.Decision_colour
 557            I8051.RegisterA) arg1)
 558          (List.append (List.Cons ((Joint.OP2 (op, (Obj.magic a),
 559            (Obj.magic a), (Obj.magic (Joint.hdw_argument_from_reg arg2r)))),
 560            List.Nil))
 561            (move globals localss
 562              (Bool.andb (sets_carry op) carry_lives_after) dst
 563              (Arg_decision_colour I8051.RegisterA)))
 564      | Arg_decision_spill x ->
 565        (match commutative op with
 566         | Bool.True ->
 567           (match arg1 with
 568            | Arg_decision_colour arg1r ->
 569              List.append
 570                (move globals localss (uses_carry op)
 571                  (Interference.Decision_colour I8051.RegisterA) arg2)
 572                (List.append (List.Cons ((Joint.OP2 (op, (Obj.magic a),
 573                  (Obj.magic a),
 574                  (Obj.magic (Joint.hdw_argument_from_reg arg1r)))),
 575                  List.Nil))
 576                  (move globals localss
 577                    (Bool.andb (sets_carry op) carry_lives_after) dst
 578                    (Arg_decision_colour I8051.RegisterA)))
 579            | Arg_decision_spill x0 ->
 580              translate_op2 globals localss carry_lives_after op dst arg1 arg2
 581            | Arg_decision_imm arg1i ->
 582              List.append
 583                (move globals localss (uses_carry op)
 584                  (Interference.Decision_colour I8051.RegisterA) arg2)
 585                (List.append (List.Cons ((Joint.OP2 (op, (Obj.magic a),
 586                  (Obj.magic a),
 587                  (Obj.magic (Joint.hdw_argument_from_byte arg1i)))),
 588                  List.Nil))
 589                  (move globals localss
 590                    (Bool.andb (sets_carry op) carry_lives_after) dst
 591                    (Arg_decision_colour I8051.RegisterA))))
 592         | Bool.False ->
 593           translate_op2 globals localss carry_lives_after op dst arg1 arg2)
 594      | Arg_decision_imm arg2i ->
 595        List.append
 596          (move globals localss (uses_carry op) (Interference.Decision_colour
 597            I8051.RegisterA) arg1)
 598          (List.append (List.Cons ((Joint.OP2 (op, (Obj.magic a),
 599            (Obj.magic a), (Obj.magic (Joint.hdw_argument_from_byte arg2i)))),
 600            List.Nil))
 601            (move globals localss
 602              (Bool.andb (sets_carry op) carry_lives_after) dst
 603              (Arg_decision_colour I8051.RegisterA))))
 604
 605 (** val dec_to_arg_dec : Interference.decision -> arg_decision **)
 606 let dec_to_arg_dec = function
 607 | Interference.Decision_spill n -> Arg_decision_spill n
 608 | Interference.Decision_colour r -> Arg_decision_colour r
 609
 610 (** val reg_to_dec__o__dec_arg_dec__o__inject :
 611     I8051.register -> arg_decision Types.sig0 **)
 612 let reg_to_dec__o__dec_arg_dec__o__inject x0 =
 613   dec_to_arg_dec (Interference.Decision_colour x0)
 614
 615 (** val dpi1__o__Reg_to_dec__o__dec_arg_dec__o__inject :
 616     (I8051.register, 'a1) Types.dPair -> arg_decision Types.sig0 **)
 617 let dpi1__o__Reg_to_dec__o__dec_arg_dec__o__inject x2 =
 618   dec_to_arg_dec (dpi1__o__Reg_to_dec x2)
 619
 620 (** val eject__o__Reg_to_dec__o__dec_arg_dec__o__inject :
 621     I8051.register Types.sig0 -> arg_decision Types.sig0 **)
 622 let eject__o__Reg_to_dec__o__dec_arg_dec__o__inject x2 =
 623   dec_to_arg_dec (eject__o__Reg_to_dec x2)
 624
 625 (** val dpi1__o__dec_arg_dec__o__inject :
 626     (Interference.decision, 'a1) Types.dPair -> arg_decision Types.sig0 **)
 627 let dpi1__o__dec_arg_dec__o__inject x2 =
 628   dec_to_arg_dec x2.Types.dpi1
 629
 630 (** val eject__o__dec_arg_dec__o__inject :
 631     Interference.decision Types.sig0 -> arg_decision Types.sig0 **)
 632 let eject__o__dec_arg_dec__o__inject x2 =
 633   dec_to_arg_dec (Types.pi1 x2)
 634
 635 (** val dec_arg_dec__o__inject :
 636     Interference.decision -> arg_decision Types.sig0 **)
 637 let dec_arg_dec__o__inject x1 =
 638   dec_to_arg_dec x1
 639
 640 (** val reg_to_dec__o__dec_arg_dec : I8051.register -> arg_decision **)
 641 let reg_to_dec__o__dec_arg_dec x0 =
 642   dec_to_arg_dec (Interference.Decision_colour x0)
 643
 644 (** val dpi1__o__Reg_to_dec__o__dec_arg_dec :
 645     (I8051.register, 'a1) Types.dPair -> arg_decision **)
 646 let dpi1__o__Reg_to_dec__o__dec_arg_dec x1 =
 647   dec_to_arg_dec (dpi1__o__Reg_to_dec x1)
 648
 649 (** val eject__o__Reg_to_dec__o__dec_arg_dec :
 650     I8051.register Types.sig0 -> arg_decision **)
 651 let eject__o__Reg_to_dec__o__dec_arg_dec x1 =
 652   dec_to_arg_dec (eject__o__Reg_to_dec x1)
 653
 654 (** val dpi1__o__dec_arg_dec :
 655     (Interference.decision, 'a1) Types.dPair -> arg_decision **)
 656 let dpi1__o__dec_arg_dec x1 =
 657   dec_to_arg_dec x1.Types.dpi1
 658
 659 (** val eject__o__dec_arg_dec :
 660     Interference.decision Types.sig0 -> arg_decision **)
 661 let eject__o__dec_arg_dec x1 =
 662   dec_to_arg_dec (Types.pi1 x1)
 663
 664 (** val translate_op1 :
 665     AST.ident List.list -> Nat.nat -> Bool.bool -> BackEndOps.op1 ->
 666     Interference.decision -> Interference.decision -> Joint.joint_seq
 667     List.list **)
 668 let translate_op1 globals localss carry_lives_after op dst arg =
 669   let preserve_carry =
 670     Bool.andb carry_lives_after (Bool.orb (is_spilled dst) (is_spilled arg))
 671   in
 672   preserve_carry_bit globals preserve_carry
 673     (List.append
 674       (move globals localss Bool.False (Interference.Decision_colour
 675         I8051.RegisterA) (dec_to_arg_dec arg)) (List.Cons ((Joint.OP1 (op,
 676       (Obj.magic Types.It), (Obj.magic Types.It))),
 677       (move globals localss Bool.False dst (Arg_decision_colour
 678         I8051.RegisterA)))))
 679
 680 (** val translate_opaccs :
 681     AST.ident List.list -> Nat.nat -> Bool.bool -> BackEndOps.opAccs ->
 682     Interference.decision -> Interference.decision -> arg_decision ->
 683     arg_decision -> Joint.joint_seq List.list **)
 684 let translate_opaccs globals localss carry_lives_after op dst1 dst2 arg1 arg2 =
 685   List.append
 686     (move globals localss Bool.False (Interference.Decision_colour
 687       I8051.RegisterB) arg2)
 688     (List.append
 689       (move globals localss Bool.False (Interference.Decision_colour
 690         I8051.RegisterA) arg1) (List.Cons ((Joint.OPACCS (op,
 691       (Obj.magic Types.It), (Obj.magic Types.It), (Obj.magic Types.It),
 692       (Obj.magic Types.It))),
 693       (List.append
 694         (move globals localss Bool.False dst1 (Arg_decision_colour
 695           I8051.RegisterA))
 696         (List.append
 697           (move globals localss Bool.False dst2 (Arg_decision_colour
 698             I8051.RegisterB))
 699           (match Bool.andb carry_lives_after
 700                    (Bool.orb (is_spilled dst1) (is_spilled dst2)) with
 701            | Bool.True -> List.Cons (Joint.CLEAR_CARRY, List.Nil)
 702            | Bool.False -> List.Nil))))))
 703
 704 (** val move_to_dp :
 705     AST.ident List.list -> Nat.nat -> arg_decision -> arg_decision ->
 706     Joint.joint_seq List.list **)
 707 let move_to_dp globals localss arg1 arg2 =
 708   match Bool.notb (arg_is_spilled arg1) with
 709   | Bool.True ->
 710     List.append
 711       (move globals localss Bool.False (Interference.Decision_colour
 712         I8051.RegisterDPH) arg2)
 713       (move globals localss Bool.False (Interference.Decision_colour
 714         I8051.RegisterDPL) arg1)
 715   | Bool.False ->
 716     (match Bool.notb (arg_is_spilled arg2) with
 717      | Bool.True ->
 718        List.append
 719          (move globals localss Bool.False (Interference.Decision_colour
 720            I8051.RegisterDPL) arg1)
 721          (move globals localss Bool.False (Interference.Decision_colour
 722            I8051.RegisterDPH) arg2)
 723      | Bool.False ->
 724        List.append
 725          (move globals localss Bool.False (Interference.Decision_colour
 726            I8051.RegisterB) arg1)
 727          (List.append
 728            (move globals localss Bool.False (Interference.Decision_colour
 729              I8051.RegisterDPH) arg2)
 730            (move globals localss Bool.False (Interference.Decision_colour
 731              I8051.RegisterDPL) (Arg_decision_colour I8051.RegisterB))))
 732
 733 (** val translate_store :
 734     AST.ident List.list -> Nat.nat -> Bool.bool -> arg_decision ->
 735     arg_decision -> arg_decision -> Joint.joint_seq List.list **)
 736 let translate_store globals localss carry_lives_after addr1 addr2 src =
 737   preserve_carry_bit globals
 738     (Bool.andb carry_lives_after
 739       (Bool.orb (Bool.orb (arg_is_spilled addr1) (arg_is_spilled addr1))
 740         (arg_is_spilled src)))
 741     (let move_to_dptr = move_to_dp globals localss addr1 addr2 in
 742     List.append
 743       (match arg_is_spilled src with
 744        | Bool.True ->
 745          List.append
 746            (move globals localss Bool.False (Interference.Decision_colour
 747              I8051.registerST0) src)
 748            (List.append move_to_dptr (List.Cons ((Joint.MOVE
 749              (Obj.magic (Joint_LTL_LIN.To_acc (a, I8051.registerST0)))),
 750              List.Nil)))
 751        | Bool.False ->
 752          List.append move_to_dptr
 753            (move globals localss Bool.False (Interference.Decision_colour
 754              I8051.RegisterA) src)) (List.Cons ((Joint.STORE
 755       ((Obj.magic Types.It), (Obj.magic Types.It), (Obj.magic a))),
 756       List.Nil)))
 757
 758 (** val translate_load :
 759     AST.ident List.list -> Nat.nat -> Bool.bool -> Interference.decision ->
 760     arg_decision -> arg_decision -> Joint.joint_seq List.list **)
 761 let translate_load globals localss carry_lives_after dst addr1 addr2 =
 762   preserve_carry_bit globals
 763     (Bool.andb carry_lives_after
 764       (Bool.orb (Bool.orb (is_spilled dst) (arg_is_spilled addr1))
 765         (arg_is_spilled addr1)))
 766     (List.append (move_to_dp globals localss addr1 addr2)
 767       (List.append (List.Cons ((Joint.LOAD ((Obj.magic a),
 768         (Obj.magic Types.It), (Obj.magic Types.It))), List.Nil))
 769         (move globals localss Bool.False dst (Arg_decision_colour
 770           I8051.RegisterA))))
 771
 772 (** val translate_address :
 773     __ List.list -> Nat.nat -> Bool.bool -> __ -> BitVector.word ->
 774     Interference.decision -> Interference.decision -> Joint.joint_seq
 775     List.list **)
 776 let translate_address globals localss carry_lives_after id off addr1 addr2 =
 777   preserve_carry_bit (Obj.magic globals)
 778     (Bool.andb carry_lives_after
 779       (Bool.orb (is_spilled addr1) (is_spilled addr2))) (List.Cons
 780     ((Joint.ADDRESS ((Obj.magic id), off, (Obj.magic Types.It),
 781     (Obj.magic Types.It))),
 782     (List.append
 783       (move (Obj.magic globals) localss Bool.False addr1 (Arg_decision_colour
 784         I8051.RegisterDPL))
 785       (move (Obj.magic globals) localss Bool.False addr2 (Arg_decision_colour
 786         I8051.RegisterDPH)))))
 787
 788 (** val translate_step :
 789     AST.ident List.list -> Joint.joint_internal_function -> Nat.nat ->
 790     Fixpoints.valuation -> Interference.coloured_graph -> Nat.nat ->
 791     Graphs.label -> Joint.joint_step -> Blocks.bind_step_block **)
 792 let translate_step globals fn localss after grph stack_sz lbl s =
 793   Bind_new.Bret
 794     (let lookup = fun r -> grph.Interference.colouring (Types.Inl r) in
 795     let lookup_arg = fun a0 ->
 796       match a0 with
 797       | Joint.Reg r -> dec_to_arg_dec (lookup r)
 798       | Joint.Imm b -> Arg_decision_imm b
 799     in
 800     let carry_lives_after = Liveness.hlives I8051.RegisterCarry (after lbl)
 801     in
 802     let move0 = move globals localss carry_lives_after in
 803     (match Liveness.eliminable_step globals (after lbl) s with
 804      | Bool.True ->
 805        let x =
 806          Blocks.ensure_step_block (Joint.graph_params_to_params LTL.lTL)
 807            globals List.Nil
 808        in
 809        x
 810      | Bool.False ->
 811        (match s with
 812         | Joint.COST_LABEL cost_lbl ->
 813           { Types.fst = { Types.fst = List.Nil; Types.snd = (fun x ->
 814             Joint.COST_LABEL cost_lbl) }; Types.snd = List.Nil }
 815         | Joint.CALL (f, n_args, x) ->
 816           (match f with
 817            | Types.Inl f0 ->
 818              { Types.fst = { Types.fst = List.Nil; Types.snd = (fun x0 ->
 819                Joint.CALL ((Types.Inl f0), n_args, (Obj.magic Types.It))) };
 820                Types.snd = List.Nil }
 821            | Types.Inr dp ->
 822              let { Types.fst = dpl; Types.snd = dph } = dp in
 823              { Types.fst = { Types.fst =
 824              (List.append
 825                (Blocks.add_dummy_variance
 826                  (move_to_dp globals localss (Obj.magic lookup_arg dpl)
 827                    (Obj.magic lookup_arg dph))) (List.Cons ((fun l ->
 828                let x0 = Joint.Extension_seq
 829                  (Obj.magic (Joint_LTL_LIN.LOW_ADDRESS (Obj.magic l)))
 830                in
 831                x0), (List.Cons ((fun x0 -> Joint.PUSH (Obj.magic Types.It)),
 832                (List.Cons ((fun l -> Joint.Extension_seq
 833                (Obj.magic (Joint_LTL_LIN.HIGH_ADDRESS (Obj.magic l)))),
 834                (List.Cons ((fun x0 -> Joint.PUSH (Obj.magic Types.It)),
 835                (List.Cons ((fun x0 -> Joint.MOVE
 836                (Obj.magic (Joint_LTL_LIN.Int_to_acc (a, Joint.zero_byte)))),
 837                List.Nil))))))))))); Types.snd = (fun x0 -> Joint.CALL
 838              ((Types.Inr { Types.fst = (Obj.magic Types.It); Types.snd =
 839              (Obj.magic Types.It) }), n_args, (Obj.magic Types.It))) };
 840              Types.snd = List.Nil })
 841         | Joint.COND (r, ltrue) ->
 842           { Types.fst = { Types.fst =
 843             (Blocks.add_dummy_variance
 844               (move0 (Interference.Decision_colour I8051.RegisterA)
 845                 (dec_to_arg_dec (Obj.magic lookup r)))); Types.snd =
 846             (fun x -> Joint.COND ((Obj.magic Types.It), ltrue)) };
 847             Types.snd = List.Nil }
 848         | Joint.Step_seq s' ->
 849           (match s' with
 850            | Joint.COMMENT c ->
 851              Blocks.ensure_step_block (Joint.graph_params_to_params LTL.lTL)
 852                globals (List.Cons ((Joint.COMMENT c), List.Nil))
 853            | Joint.MOVE pair_regs ->
 854              let lookup_move_dst = fun x ->
 855                match x with
 856                | ERTL.PSD r -> lookup r
 857                | ERTL.HDW r -> Interference.Decision_colour r
 858              in
 859              let dst = lookup_move_dst (Obj.magic pair_regs).Types.fst in
 860              let src =
 861                match (Obj.magic pair_regs).Types.snd with
 862                | Joint.Reg r -> dec_to_arg_dec (lookup_move_dst r)
 863                | Joint.Imm b -> Arg_decision_imm b
 864              in
 865              Blocks.ensure_step_block (Joint.graph_params_to_params LTL.lTL)
 866                globals (move0 dst src)
 867            | Joint.POP r ->
 868              Blocks.ensure_step_block (Joint.graph_params_to_params LTL.lTL)
 869                globals (List.Cons ((Joint.POP (Obj.magic a)),
 870                (move0 (Obj.magic lookup r) (Arg_decision_colour
 871                  I8051.RegisterA))))
 872            | Joint.PUSH a0 ->
 873              Blocks.ensure_step_block (Joint.graph_params_to_params LTL.lTL)
 874                globals
 875                (List.append
 876                  (move0 (Interference.Decision_colour I8051.RegisterA)
 877                    (Obj.magic lookup_arg a0)) (List.Cons ((Joint.PUSH
 878                  (Obj.magic a)), List.Nil)))
 879            | Joint.ADDRESS (lbl0, off, dpl, dph) ->
 880              Blocks.ensure_step_block (Joint.graph_params_to_params LTL.lTL)
 881                globals
 882                (translate_address (Obj.magic globals) localss
 883                  carry_lives_after (Obj.magic lbl0) off
 884                  (Obj.magic lookup dpl) (Obj.magic lookup dph))
 885            | Joint.OPACCS (op, dst1, dst2, arg1, arg2) ->
 886              Blocks.ensure_step_block (Joint.graph_params_to_params LTL.lTL)
 887                globals
 888                (translate_opaccs globals localss carry_lives_after op
 889                  (Obj.magic lookup dst1) (Obj.magic lookup dst2)
 890                  (Obj.magic lookup_arg arg1) (Obj.magic lookup_arg arg2))
 891            | Joint.OP1 (op, dst, arg) ->
 892              Blocks.ensure_step_block (Joint.graph_params_to_params LTL.lTL)
 893                globals
 894                (translate_op1 globals localss carry_lives_after op
 895                  (Obj.magic lookup dst) (Obj.magic lookup arg))
 896            | Joint.OP2 (op, dst, arg1, arg2) ->
 897              Blocks.ensure_step_block (Joint.graph_params_to_params LTL.lTL)
 898                globals
 899                (translate_op2_smart globals localss carry_lives_after op
 900                  (Obj.magic lookup dst) (Obj.magic lookup_arg arg1)
 901                  (Obj.magic lookup_arg arg2))
 902            | Joint.CLEAR_CARRY ->
 903              Blocks.ensure_step_block (Joint.graph_params_to_params LTL.lTL)
 904                globals (List.Cons (Joint.CLEAR_CARRY, List.Nil))
 905            | Joint.SET_CARRY ->
 906              Blocks.ensure_step_block (Joint.graph_params_to_params LTL.lTL)
 907                globals (List.Cons (Joint.SET_CARRY, List.Nil))
 908            | Joint.LOAD (dstr, addr1, addr2) ->
 909              Blocks.ensure_step_block (Joint.graph_params_to_params LTL.lTL)
 910                globals
 911                (translate_load globals localss carry_lives_after
 912                  (Obj.magic lookup dstr) (Obj.magic lookup_arg addr1)
 913                  (Obj.magic lookup_arg addr2))
 914            | Joint.STORE (addr1, addr2, srcr) ->
 915              Blocks.ensure_step_block (Joint.graph_params_to_params LTL.lTL)
 916                globals
 917                (translate_store globals localss carry_lives_after
 918                  (Obj.magic lookup_arg addr1) (Obj.magic lookup_arg addr2)
 919                  (Obj.magic lookup_arg srcr))
 920            | Joint.Extension_seq ext ->
 921              Blocks.ensure_step_block (Joint.graph_params_to_params LTL.lTL)
 922                globals
 923                (match Obj.magic ext with
 924                 | ERTL.Ertl_new_frame -> newframe globals stack_sz
 925                 | ERTL.Ertl_del_frame -> delframe globals stack_sz
 926                 | ERTL.Ertl_frame_size r ->
 927                   move0 (lookup r) (Arg_decision_imm
 928                     (Joint.byte_of_nat stack_sz)))))))
 929
 930 (** val translate_fin_step :
 931     AST.ident List.list -> Graphs.label -> Joint.joint_fin_step ->
 932     Blocks.bind_fin_block **)
 933 let translate_fin_step globals lbl s =
 934   Bind_new.Bret { Types.fst = List.Nil; Types.snd =
 935     (match s with
 936      | Joint.GOTO l -> Joint.GOTO l
 937      | Joint.RETURN -> Joint.RETURN
 938      | Joint.TAILCALL (x, x0) -> assert false (* absurd case *)) }
 939
 940 (** val translate_data :
 941     Fixpoints.fixpoint_computer -> Interference.coloured_graph_computer ->
 942     AST.ident List.list -> Joint.joint_closed_internal_function ->
 943     (Registers.register, TranslateUtils.b_graph_translate_data)
 944     Bind_new.bind_new **)
 945 let translate_data the_fixpoint build globals int_fun =
 946   let after =
 947     Liveness.analyse_liveness the_fixpoint globals (Types.pi1 int_fun)
 948   in
 949   let coloured_graph =
 950     build globals (Types.pi1 int_fun)
 951       (Fixpoints.fix_lfp Liveness.register_lattice
 952         (Liveness.liveafter globals (Types.pi1 int_fun)) after)
 953   in
 954   let stack_sz =
 955     Nat.plus coloured_graph.Interference.spilled_no
 956       (Types.pi1 int_fun).Joint.joint_if_stacksize
 957   in
 958   Bind_new.Bret { TranslateUtils.init_ret = (Obj.magic Types.It);
 959   TranslateUtils.init_params = (Obj.magic Types.It);
 960   TranslateUtils.init_stack_size = stack_sz; TranslateUtils.added_prologue =
 961   List.Nil; TranslateUtils.new_regs = List.Nil; TranslateUtils.f_step =
 962   (translate_step globals (Types.pi1 int_fun)
 963     (Types.pi1 int_fun).Joint.joint_if_local_stacksize
 964     (Fixpoints.fix_lfp Liveness.register_lattice
 965       (Liveness.liveafter globals (Types.pi1 int_fun)) after) coloured_graph
 966     stack_sz); TranslateUtils.f_fin = (translate_fin_step globals) }
 967
 968 (** val ertl_to_ltl :
 969     Fixpoints.fixpoint_computer -> Interference.coloured_graph_computer ->
 970     ERTL.ertl_program -> ((LTL.ltl_program, Joint.stack_cost_model)
 971     Types.prod, Nat.nat) Types.prod **)
 972 let ertl_to_ltl the_fixpoint build pr =
 973   let ltlprog =
 974     TranslateUtils.b_graph_transform_program ERTL.eRTL LTL.lTL
 975       (fun globals h -> translate_data the_fixpoint build globals h) pr
 976   in
 977   { Types.fst = { Types.fst = ltlprog; Types.snd =
 978   (Joint.stack_cost (Joint.graph_params_to_params LTL.lTL) ltlprog) };
 979   Types.snd =
 980   (Nat.minus
 981     (Exp.exp (Nat.S (Nat.S Nat.O)) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 982       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 983       Nat.O)))))))))))))))))
 984     (Joint.globals_stacksize (Joint.graph_params_to_params LTL.lTL) ltlprog)) }
 985