source: extracted/liveness.mli @ 2717

Last change on this file since 2717 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.1 KB
Line 
1open Preamble
2
3open Div_and_mod
4
5open Jmeq
6
7open Russell
8
9open Bool
10
11open Relations
12
13open Nat
14
15open Hints_declaration
16
17open Core_notation
18
19open Pts
20
21open Logic
22
23open Types
24
25open List
26
27open Util
28
29open String
30
31open Sets
32
33open Listb
34
35open LabelledObjects
36
37open Graphs
38
39open I8051
40
41open Order
42
43open Registers
44
45open BitVectorTrie
46
47open CostLabel
48
49open Hide
50
51open Proper
52
53open PositiveMap
54
55open Deqsets
56
57open ErrorMessages
58
59open PreIdentifiers
60
61open Errors
62
63open Extralib
64
65open Setoids
66
67open Monad
68
69open Option
70
71open Lists
72
73open Identifiers
74
75open Integers
76
77open AST
78
79open Division
80
81open Exp
82
83open Arithmetic
84
85open Extranat
86
87open Vector
88
89open FoldStuff
90
91open BitVector
92
93open Positive
94
95open Z
96
97open BitVectorZ
98
99open Pointers
100
101open ByteValues
102
103open BackEndOps
104
105open Joint
106
107open ERTL
108
109open ERTLptr
110
111open Set_adt
112
113open Fixpoints
114
115val register_lattice : Fixpoints.property_lattice
116
117val rl_bottom : __
118
119val rl_psingleton : Registers.register -> __
120
121val rl_hsingleton : I8051.register -> __
122
123val rl_join : __ -> __ -> __
124
125val rl_diff : __ -> __ -> __
126
127val defined : AST.ident List.list -> Joint.joint_statement -> __
128
129val ret_regs : I8051.register Set_adt.set0
130
131val rl_arg : Joint.psd_argument -> __
132
133val used :
134  AST.ident List.list -> Joint.joint_statement -> (Registers.register
135  Set_adt.set0, I8051.register Set_adt.set0) Types.prod
136
137val eliminable :
138  AST.ident List.list -> __ -> Joint.joint_statement -> __ Types.option
139
140val statement_semantics :
141  AST.ident List.list -> Joint.joint_statement -> __ -> __
142
143val livebefore :
144  AST.ident List.list -> Joint.joint_internal_function ->
145  PreIdentifiers.identifier -> Fixpoints.valuation -> __
146
147val liveafter :
148  AST.ident List.list -> Joint.joint_internal_function ->
149  PreIdentifiers.identifier -> Fixpoints.valuation -> __
150
151val analyse_liveness :
152  Fixpoints.fixpoint_computer -> AST.ident List.list ->
153  Joint.joint_internal_function -> Fixpoints.valuation
154
155type vertex = (Registers.register, I8051.register) Types.sum
156
157val plives : Registers.register -> __ -> Bool.bool
158
159val hlives : I8051.register -> __ -> Bool.bool
160
161val lives : vertex -> __ -> Bool.bool
162
Note: See TracBrowser for help on using the repository browser.