extracted/frontend_misc.mli

   1 open Preamble
   2
   3 open CostLabel
   4
   5 open Coqlib
   6
   7 open Proper
   8
   9 open PositiveMap
  10
  11 open Deqsets
  12
  13 open ErrorMessages
  14
  15 open PreIdentifiers
  16
  17 open Errors
  18
  19 open Extralib
  20
  21 open Lists
  22
  23 open Positive
  24
  25 open Identifiers
  26
  27 open Exp
  28
  29 open Arithmetic
  30
  31 open Vector
  32
  33 open Div_and_mod
  34
  35 open Util
  36
  37 open FoldStuff
  38
  39 open BitVector
  40
  41 open Jmeq
  42
  43 open Russell
  44
  45 open List
  46
  47 open Setoids
  48
  49 open Monad
  50
  51 open Option
  52
  53 open Extranat
  54
  55 open Bool
  56
  57 open Relations
  58
  59 open Nat
  60
  61 open Integers
  62
  63 open Hints_declaration
  64
  65 open Core_notation
  66
  67 open Pts
  68
  69 open Logic
  70
  71 open Types
  72
  73 open AST
  74
  75 open Csyntax
  76
  77 open TypeComparison
  78
  79 open ClassifyOp
  80
  81 open Events
  82
  83 open Smallstep
  84
  85 open Extra_bool
  86
  87 open Values
  88
  89 open FrontEndVal
  90
  91 open Hide
  92
  93 open ByteValues
  94
  95 open Division
  96
  97 open Z
  98
  99 open BitVectorZ
 100
 101 open Pointers
 102
 103 open GenMem
 104
 105 open FrontEndMem
 106
 107 open Globalenvs
 108
 109 open Csem
 110
 111 open Star
 112
 113 open IOMonad
 114
 115 open IO
 116
 117 open Sets
 118
 119 open Listb
 120
 121 val typ_eq_dec : AST.typ -> AST.typ -> (__, __) Types.sum
 122
 123 val block_DeqSet : Deqsets.deqSet
 124
 125 val mem_assoc_env :
 126   AST.ident -> (AST.ident, Csyntax.type0) Types.prod List.list -> Bool.bool
 127
 128 type 'a lset = 'a List.list
 129
 130 val empty_lset : 'a1 List.list
 131
 132 val lset_union : 'a1 lset -> 'a1 lset -> 'a1 List.list
 133
 134 val lset_remove : Deqsets.deqSet -> __ lset -> __ -> __ List.list
 135
 136 val lset_difference : Deqsets.deqSet -> __ lset -> __ lset -> __ List.list
 137
 138 val wF_rect : ('a1 -> __ -> ('a1 -> __ -> 'a2) -> 'a2) -> 'a1 -> 'a2
 139
 140 val one_bv : Nat.nat -> BitVector.bitVector
 141
 142 val ith_carry :
 143   Nat.nat -> BitVector.bitVector -> BitVector.bitVector -> Bool.bool ->
 144   Bool.bool
 145
 146 val ith_bit :
 147   Nat.nat -> BitVector.bitVector -> BitVector.bitVector -> Bool.bool ->
 148   Bool.bool
 149
 150 val bitvector_fold :
 151   Nat.nat -> BitVector.bitVector -> (Nat.nat -> BitVector.bitVector ->
 152   Bool.bool) -> BitVector.bitVector
 153
 154 val bitvector_fold2 :
 155   Nat.nat -> BitVector.bitVector -> BitVector.bitVector -> (Nat.nat ->
 156   BitVector.bitVector -> BitVector.bitVector -> Bool.bool) ->
 157   BitVector.bitVector
 158
 159 val addition_n_direct :
 160   Nat.nat -> BitVector.bitVector -> BitVector.bitVector -> Bool.bool ->
 161   BitVector.bitVector
 162
 163 val increment_direct : Nat.nat -> BitVector.bitVector -> BitVector.bitVector
 164
 165 val twocomp_neg_direct :
 166   Nat.nat -> BitVector.bitVector -> BitVector.bitVector
 167
 168 val andb_fold : Nat.nat -> BitVector.bitVector -> Bool.bool
 169