source: extracted/aSMCosts.mli @ 2890

Last change on this file since 2890 was 2773, checked in by sacerdot, 7 years ago
  1. everything extracted again after all bugs in Matita's extraction have been fixed. No more need for manual patching
  2. new extraction after file reorganization (by James)
File size: 2.1 KB
RevLine 
[2601]1open Preamble
2
[2773]3open Fetch
[2649]4
[2773]5open Hide
[2601]6
[2773]7open Division
8
9open Z
10
11open BitVectorZ
12
13open Pointers
14
15open Coqlib
16
17open Values
18
19open Events
20
21open IOMonad
22
23open IO
24
25open Sets
26
27open Listb
28
29open StructuredTraces
30
31open AbstractStatus
32
[2717]33open BitVectorTrie
34
[2773]35open String
36
[2717]37open Exp
38
[2601]39open Arithmetic
40
[2773]41open Vector
42
43open FoldStuff
44
45open BitVector
46
47open Extranat
48
[2601]49open Integers
50
51open AST
52
[2773]53open LabelledObjects
[2601]54
55open Proper
56
57open PositiveMap
58
59open Deqsets
60
[2649]61open ErrorMessages
62
[2601]63open PreIdentifiers
64
65open Errors
66
67open Extralib
68
69open Setoids
70
71open Monad
72
73open Option
74
75open Div_and_mod
76
77open Jmeq
78
79open Russell
80
[2773]81open Util
[2601]82
83open List
84
[2773]85open Lists
[2601]86
87open Bool
88
[2773]89open Relations
90
91open Nat
92
93open Positive
94
[2601]95open Hints_declaration
96
97open Core_notation
98
99open Pts
100
101open Logic
102
[2773]103open Types
[2601]104
[2773]105open Identifiers
[2601]106
[2773]107open CostLabel
[2601]108
109open ASM
110
111open Status
112
113open StatusProofs
114
115open Interpret
116
117val aSM_abstract_status :
118  BitVector.byte BitVectorTrie.bitVectorTrie -> CostLabel.costlabel
119  BitVectorTrie.bitVectorTrie -> StructuredTraces.abstract_status
120
121val trace_any_label_length :
122  BitVector.byte BitVectorTrie.bitVectorTrie -> CostLabel.costlabel
123  BitVectorTrie.bitVectorTrie -> StructuredTraces.trace_ends_with_ret ->
124  Status.status -> Status.status -> StructuredTraces.trace_any_label ->
125  Nat.nat
126
127val all_program_counter_list : Nat.nat -> BitVector.bitVector List.list
128
129val compute_paid_trace_any_label :
130  BitVector.byte BitVectorTrie.bitVectorTrie -> CostLabel.costlabel
131  BitVectorTrie.bitVectorTrie -> StructuredTraces.trace_ends_with_ret ->
132  Status.status -> Status.status -> StructuredTraces.trace_any_label ->
133  Nat.nat
134
135val compute_paid_trace_label_label :
136  BitVector.byte BitVectorTrie.bitVectorTrie -> CostLabel.costlabel
137  BitVectorTrie.bitVectorTrie -> StructuredTraces.trace_ends_with_ret ->
138  Status.status -> Status.status -> StructuredTraces.trace_label_label ->
139  Nat.nat
140
141val block_cost' :
142  BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.word -> Nat.nat ->
143  CostLabel.costlabel BitVectorTrie.bitVectorTrie -> Bool.bool -> Nat.nat
144  Types.sig0
145
146val block_cost :
147  BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.word ->
148  CostLabel.costlabel BitVectorTrie.bitVectorTrie -> Nat.nat Types.sig0
149
Note: See TracBrowser for help on using the repository browser.