source: extracted/aSMCostsSplit.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: 1.4 KB
Line 
1open Preamble
2
3open StructuredTraces
4
5open AbstractStatus
6
7open Status
8
9open StatusProofs
10
11open Sets
12
13open Listb
14
15open Interpret
16
17open Fetch
18
19open String
20
21open LabelledObjects
22
23open BitVectorTrie
24
25open Exp
26
27open Arithmetic
28
29open Integers
30
31open AST
32
33open CostLabel
34
35open Proper
36
37open PositiveMap
38
39open Deqsets
40
41open ErrorMessages
42
43open PreIdentifiers
44
45open Errors
46
47open Extralib
48
49open Setoids
50
51open Monad
52
53open Option
54
55open Lists
56
57open Positive
58
59open Identifiers
60
61open Extranat
62
63open Vector
64
65open Div_and_mod
66
67open Jmeq
68
69open Russell
70
71open Types
72
73open List
74
75open Util
76
77open FoldStuff
78
79open Bool
80
81open Hints_declaration
82
83open Core_notation
84
85open Pts
86
87open Logic
88
89open Relations
90
91open Nat
92
93open BitVector
94
95open ASM
96
97open ASMCosts
98
99open UtilBranch
100
101val traverse_code_internal :
102  BitVector.byte BitVectorTrie.bitVectorTrie -> CostLabel.costlabel
103  BitVectorTrie.bitVectorTrie -> BitVector.word -> Nat.nat -> Nat.nat
104  Identifiers.identifier_map Types.sig0
105
106val traverse_code :
107  BitVector.byte BitVectorTrie.bitVectorTrie -> CostLabel.costlabel
108  BitVectorTrie.bitVectorTrie -> Nat.nat Identifiers.identifier_map
109  Types.sig0
110
111val compute_costs :
112  BitVector.byte List.list -> CostLabel.costlabel BitVectorTrie.bitVectorTrie
113  -> Nat.nat Identifiers.identifier_map Types.sig0
114
115val aSM_cost_map :
116  (BitVector.byte List.list, CostLabel.costlabel BitVectorTrie.bitVectorTrie)
117  Types.prod -> StructuredTraces.as_cost_map
118
Note: See TracBrowser for help on using the repository browser.