extracted/label.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 val labels_of_expr : Csyntax.expr -> CostLabel.costlabel List.list
  78
  79 val labels_of_labeled_statements :
  80   Csyntax.labeled_statements -> CostLabel.costlabel List.list
  81
  82 val labels_of_statement : Csyntax.statement -> CostLabel.costlabel List.list
  83
  84 val labels_of_clight_fundef :
  85   (AST.ident, Csyntax.clight_fundef) Types.prod -> CostLabel.costlabel
  86   List.list
  87
  88 val labels_of_clight :
  89   Csyntax.clight_program -> CostLabel.costlabel List.list
  90
  91 type in_clight_label = CostLabel.costlabel Types.sig0
  92
  93 type clight_cost_map = CostLabel.costlabel -> Nat.nat
  94
  95 val clight_label_free : Csyntax.clight_program -> Bool.bool
  96
  97 val add_cost_before :
  98   Csyntax.statement -> Identifiers.universe -> (Csyntax.statement,
  99   Identifiers.universe) Types.prod
 100
 101 val add_cost_after :
 102   Csyntax.statement -> Identifiers.universe -> (Csyntax.statement,
 103   Identifiers.universe) Types.prod
 104
 105 val add_cost_expr :
 106   Csyntax.expr -> Identifiers.universe -> (Csyntax.expr,
 107   Identifiers.universe) Types.prod
 108
 109 val const_int : AST.intsize -> Nat.nat -> Csyntax.expr
 110
 111 val label_expr_descr :
 112   Csyntax.expr_descr -> Identifiers.universe -> Csyntax.type0 ->
 113   (Csyntax.expr_descr, Identifiers.universe) Types.prod
 114
 115 val label_expr :
 116   Csyntax.expr -> Identifiers.universe -> (Csyntax.expr,
 117   Identifiers.universe) Types.prod
 118
 119 val label_exprs :
 120   Csyntax.expr List.list -> Identifiers.universe -> (Csyntax.expr List.list,
 121   Identifiers.universe) Types.prod
 122
 123 val label_opt_expr :
 124   Csyntax.expr Types.option -> Identifiers.universe -> (Csyntax.expr
 125   Types.option, Identifiers.universe) Types.prod
 126
 127 val label_lstatements :
 128   Csyntax.labeled_statements -> Identifiers.universe ->
 129   (Csyntax.labeled_statements, Identifiers.universe) Types.prod
 130
 131 val label_statement :
 132   Csyntax.statement -> Identifiers.universe -> (Csyntax.statement,
 133   Identifiers.universe) Types.prod
 134
 135 val label_function :
 136   Identifiers.universe -> Csyntax.function0 -> (Csyntax.function0,
 137   Identifiers.universe) Types.prod
 138
 139 val label_fundef :
 140   Identifiers.universe -> Csyntax.clight_fundef -> (Csyntax.clight_fundef,
 141   Identifiers.universe) Types.prod
 142
 143 val clight_label :
 144   Csyntax.clight_program -> (Csyntax.clight_program, CostLabel.costlabel)
 145   Types.prod
 146