extracted/fetch.mli

   1 open Preamble
   2
   3 open Types
   4
   5 open Hints_declaration
   6
   7 open Core_notation
   8
   9 open Pts
  10
  11 open Logic
  12
  13 open Jmeq
  14
  15 open Russell
  16
  17 open Exp
  18
  19 open Setoids
  20
  21 open Monad
  22
  23 open Option
  24
  25 open Extranat
  26
  27 open Vector
  28
  29 open Div_and_mod
  30
  31 open List
  32
  33 open Util
  34
  35 open FoldStuff
  36
  37 open Bool
  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_label :
  82   ASM.labelled_instruction List.list -> ASM.identifier -> Nat.nat
  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, ASM.costlabel_map)
  88   Types.prod Types.sig0
  89
  90 val create_label_cost_map :
  91   ASM.labelled_instruction List.list -> (label_map, ASM.costlabel_map)
  92   Types.prod
  93
  94 val address_of_word_labels :
  95   ASM.labelled_instruction List.list -> ASM.identifier -> BitVector.word
  96
  97 val prod_inv_rect_Type0 :
  98   ('a1, 'a2) Types.prod -> ('a1 -> 'a2 -> __ -> 'a3) -> 'a3
  99
 100 val fetch0 :
 101   BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.word ->
 102   BitVector.byte -> ((ASM.instruction, BitVector.word) Types.prod, Nat.nat)
 103   Types.prod
 104
 105 val fetch :
 106   BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.word ->
 107   ((ASM.instruction, BitVector.word) Types.prod, Nat.nat) Types.prod
 108