extracted/lTL.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 (** val lTL : Joint.graph_params **)
 124 let lTL =
 125   Joint_LTL_LIN.lTL_LIN
 126
 127 type ltl_program = Joint.joint_program
 128
 129 (** val dpi1__o__byte_to_ltl_argument__o__inject :
 130     (BitVector.byte, 'a1) Types.dPair -> Joint.hdw_argument Types.sig0 **)
 131 let dpi1__o__byte_to_ltl_argument__o__inject x2 =
 132   Joint.hdw_argument_from_byte x2.Types.dpi1
 133
 134 (** val eject__o__byte_to_ltl_argument__o__inject :
 135     BitVector.byte Types.sig0 -> Joint.hdw_argument Types.sig0 **)
 136 let eject__o__byte_to_ltl_argument__o__inject x2 =
 137   Joint.hdw_argument_from_byte (Types.pi1 x2)
 138
 139 (** val byte_to_ltl_argument__o__inject :
 140     BitVector.byte -> Joint.hdw_argument Types.sig0 **)
 141 let byte_to_ltl_argument__o__inject x1 =
 142   Joint.hdw_argument_from_byte x1
 143
 144 (** val dpi1__o__byte_to_ltl_argument :
 145     (BitVector.byte, 'a1) Types.dPair -> Joint.hdw_argument **)
 146 let dpi1__o__byte_to_ltl_argument x1 =
 147   Joint.hdw_argument_from_byte x1.Types.dpi1
 148
 149 (** val eject__o__byte_to_ltl_argument :
 150     BitVector.byte Types.sig0 -> Joint.hdw_argument **)
 151 let eject__o__byte_to_ltl_argument x1 =
 152   Joint.hdw_argument_from_byte (Types.pi1 x1)
 153
 154 (** val dpi1__o__reg_to_ltl_argument__o__inject :
 155     (I8051.register, 'a1) Types.dPair -> Joint.hdw_argument Types.sig0 **)
 156 let dpi1__o__reg_to_ltl_argument__o__inject x2 =
 157   Joint.hdw_argument_from_reg x2.Types.dpi1
 158
 159 (** val eject__o__reg_to_ltl_argument__o__inject :
 160     I8051.register Types.sig0 -> Joint.hdw_argument Types.sig0 **)
 161 let eject__o__reg_to_ltl_argument__o__inject x2 =
 162   Joint.hdw_argument_from_reg (Types.pi1 x2)
 163
 164 (** val reg_to_ltl_argument__o__inject :
 165     I8051.register -> Joint.hdw_argument Types.sig0 **)
 166 let reg_to_ltl_argument__o__inject x1 =
 167   Joint.hdw_argument_from_reg x1
 168
 169 (** val dpi1__o__reg_to_ltl_argument :
 170     (I8051.register, 'a1) Types.dPair -> Joint.hdw_argument **)
 171 let dpi1__o__reg_to_ltl_argument x1 =
 172   Joint.hdw_argument_from_reg x1.Types.dpi1
 173
 174 (** val eject__o__reg_to_ltl_argument :
 175     I8051.register Types.sig0 -> Joint.hdw_argument **)
 176 let eject__o__reg_to_ltl_argument x1 =
 177   Joint.hdw_argument_from_reg (Types.pi1 x1)
 178
 179 (** val lTL_premain : ltl_program -> Joint.joint_closed_internal_function **)
 180 let lTL_premain p =
 181   let l1 = Positive.One in
 182   let l2 = Positive.P0 Positive.One in
 183   let l3 = Positive.P1 Positive.One in
 184   let res = { Joint.joint_if_luniverse = (Positive.P0 (Positive.P0
 185     Positive.One)); Joint.joint_if_runiverse = Positive.One;
 186     Joint.joint_if_result = (Obj.magic Types.It); Joint.joint_if_params =
 187     (Obj.magic Types.It); Joint.joint_if_stacksize = Nat.O;
 188     Joint.joint_if_local_stacksize = Nat.O; Joint.joint_if_code =
 189     (Obj.magic (Identifiers.empty_map PreIdentifiers.LabelTag));
 190     Joint.joint_if_entry = (Obj.magic l1) }
 191   in
 192   let res0 =
 193     Joint.add_graph lTL
 194       (Joint.prog_names (Joint.graph_params_to_params lTL) p) l1
 195       (Joint.Sequential ((Joint.COST_LABEL p.Joint.init_cost_label),
 196       (Obj.magic l2))) res
 197   in
 198   let res1 =
 199     Joint.add_graph lTL
 200       (Joint.prog_names (Joint.graph_params_to_params lTL) p) l2
 201       (Joint.Sequential ((Joint.CALL ((Types.Inl
 202       p.Joint.joint_prog.AST.prog_main), (Obj.magic Nat.O),
 203       (Obj.magic Types.It))), (Obj.magic l3))) res0
 204   in
 205   let res2 =
 206     Joint.add_graph lTL
 207       (Joint.prog_names (Joint.graph_params_to_params lTL) p) l3 (Joint.Final
 208       (Joint.GOTO l3)) res1
 209   in
 210   res2
 211