extracted/fetch.mli

   1 open Preamble
   2
   3 open Exp
   4
   5 open Setoids
   6
   7 open Monad
   8
   9 open Option
  10
  11 open Extranat
  12
  13 open Vector
  14
  15 open Div_and_mod
  16
  17 open Jmeq
  18
  19 open Russell
  20
  21 open Types
  22
  23 open List
  24
  25 open Util
  26
  27 open FoldStuff
  28
  29 open Bool
  30
  31 open Hints_declaration
  32
  33 open Core_notation
  34
  35 open Pts
  36
  37 open Logic
  38
  39 open Relations
  40
  41 open Nat
  42
  43 open BitVector
  44
  45 open Arithmetic
  46
  47 open BitVectorTrie
  48
  49 open String
  50
  51 open Integers
  52
  53 open AST
  54
  55 open LabelledObjects
  56
  57 open Proper
  58
  59 open PositiveMap
  60
  61 open Deqsets
  62
  63 open ErrorMessages
  64
  65 open PreIdentifiers
  66
  67 open Errors
  68
  69 open Extralib
  70
  71 open Lists
  72
  73 open Positive
  74
  75 open Identifiers
  76
  77 open CostLabel
  78
  79 open ASM
  80
  81 val inefficient_address_of_word_labels_code_mem :
  82   ASM.labelled_instruction List.list -> ASM.identifier -> BitVector.bitVector
  83
  84 type label_map = Nat.nat Identifiers.identifier_map
  85
  86 val create_label_cost_map0 :
  87   ASM.labelled_instruction List.list -> (label_map, CostLabel.costlabel
  88   BitVectorTrie.bitVectorTrie) Types.prod Types.sig0
  89
  90 val create_label_cost_map :
  91   ASM.labelled_instruction List.list -> (label_map, CostLabel.costlabel
  92   BitVectorTrie.bitVectorTrie) Types.prod
  93
  94 val address_of_word_labels :
  95   ASM.labelled_instruction List.list -> ASM.identifier -> BitVector.word
  96
  97 val bitvector_max_nat : Nat.nat -> Nat.nat
  98
  99 val code_memory_size : Nat.nat
 100
 101 val prod_inv_rect_Type0 :
 102   ('a1, 'a2) Types.prod -> ('a1 -> 'a2 -> __ -> 'a3) -> 'a3
 103
 104 val fetch0 :
 105   BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.word ->
 106   BitVector.byte -> ((ASM.instruction, BitVector.word) Types.prod, Nat.nat)
 107   Types.prod
 108
 109 val fetch :
 110   BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.word ->
 111   ((ASM.instruction, BitVector.word) Types.prod, Nat.nat) Types.prod
 112