source: extracted/aSMCosts.mli @ 2746

Last change on this file since 2746 was 2717, checked in by sacerdot, 7 years ago

Extracted code for the whole compiler.
The space cost model is not there yet.

I have fixed by hand the few extraction problems
(i.e. composed coercions not extracted and type
definitions with wrong syntax).

I have also changed all axioms to be implemented
so that they do not fail at initialization time.

File size: 2.0 KB
Line 
1open Preamble
2
3open String
4
5open LabelledObjects
6
7open BitVectorTrie
8
9open Exp
10
11open Arithmetic
12
13open Integers
14
15open AST
16
17open CostLabel
18
19open Proper
20
21open PositiveMap
22
23open Deqsets
24
25open ErrorMessages
26
27open PreIdentifiers
28
29open Errors
30
31open Extralib
32
33open Setoids
34
35open Monad
36
37open Option
38
39open Lists
40
41open Positive
42
43open Identifiers
44
45open Extranat
46
47open Vector
48
49open Div_and_mod
50
51open Jmeq
52
53open Russell
54
55open Types
56
57open List
58
59open Util
60
61open FoldStuff
62
63open Bool
64
65open Hints_declaration
66
67open Core_notation
68
69open Pts
70
71open Logic
72
73open Relations
74
75open Nat
76
77open BitVector
78
79open ASM
80
81open Fetch
82
83open StructuredTraces
84
85open AbstractStatus
86
87open Status
88
89open StatusProofs
90
91open Sets
92
93open Listb
94
95open Interpret
96
97val aSM_abstract_status :
98  BitVector.byte BitVectorTrie.bitVectorTrie -> CostLabel.costlabel
99  BitVectorTrie.bitVectorTrie -> StructuredTraces.abstract_status
100
101val trace_any_label_length :
102  BitVector.byte BitVectorTrie.bitVectorTrie -> CostLabel.costlabel
103  BitVectorTrie.bitVectorTrie -> StructuredTraces.trace_ends_with_ret ->
104  Status.status -> Status.status -> StructuredTraces.trace_any_label ->
105  Nat.nat
106
107val all_program_counter_list : Nat.nat -> BitVector.bitVector List.list
108
109val compute_paid_trace_any_label :
110  BitVector.byte BitVectorTrie.bitVectorTrie -> CostLabel.costlabel
111  BitVectorTrie.bitVectorTrie -> StructuredTraces.trace_ends_with_ret ->
112  Status.status -> Status.status -> StructuredTraces.trace_any_label ->
113  Nat.nat
114
115val compute_paid_trace_label_label :
116  BitVector.byte BitVectorTrie.bitVectorTrie -> CostLabel.costlabel
117  BitVectorTrie.bitVectorTrie -> StructuredTraces.trace_ends_with_ret ->
118  Status.status -> Status.status -> StructuredTraces.trace_label_label ->
119  Nat.nat
120
121val block_cost' :
122  BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.word -> Nat.nat ->
123  CostLabel.costlabel BitVectorTrie.bitVectorTrie -> Bool.bool -> Nat.nat
124  Types.sig0
125
126val block_cost :
127  BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.word ->
128  CostLabel.costlabel BitVectorTrie.bitVectorTrie -> Nat.nat Types.sig0
129
Note: See TracBrowser for help on using the repository browser.