extracted/frontEndVal.mli

   1 open Preamble
   2
   3 open Proper
   4
   5 open PositiveMap
   6
   7 open Deqsets
   8
   9 open Extralib
  10
  11 open Lists
  12
  13 open Identifiers
  14
  15 open Integers
  16
  17 open AST
  18
  19 open Division
  20
  21 open Exp
  22
  23 open Arithmetic
  24
  25 open Extranat
  26
  27 open Vector
  28
  29 open FoldStuff
  30
  31 open BitVector
  32
  33 open Z
  34
  35 open BitVectorZ
  36
  37 open Pointers
  38
  39 open ErrorMessages
  40
  41 open Option
  42
  43 open Setoids
  44
  45 open Monad
  46
  47 open Positive
  48
  49 open PreIdentifiers
  50
  51 open Errors
  52
  53 open Div_and_mod
  54
  55 open Jmeq
  56
  57 open Russell
  58
  59 open Util
  60
  61 open Bool
  62
  63 open Relations
  64
  65 open Nat
  66
  67 open List
  68
  69 open Hints_declaration
  70
  71 open Core_notation
  72
  73 open Pts
  74
  75 open Logic
  76
  77 open Types
  78
  79 open Coqlib
  80
  81 open Values
  82
  83 open Hide
  84
  85 open ByteValues
  86
  87 val make_parts : ByteValues.part List.list
  88
  89 val make_be_null : ByteValues.beval List.list
  90
  91 val bytes_of_bitvector :
  92   Nat.nat -> BitVector.bitVector -> BitVector.byte List.list
  93
  94 val fe_to_be_values : AST.typ -> Values.val0 -> ByteValues.beval List.list
  95
  96 val check_be_null : Nat.nat -> ByteValues.beval List.list -> Bool.bool
  97
  98 val build_integer :
  99   Nat.nat -> ByteValues.beval List.list -> BitVector.bitVector Types.option
 100
 101 val build_integer_val : AST.typ -> ByteValues.beval List.list -> Values.val0
 102
 103 val be_to_fe_value : AST.typ -> ByteValues.beval List.list -> Values.val0
 104