Changeset 2717 for extracted/compiler.mli

Timestamp:

Feb 23, 2013, 1:16:55 AM (7 years ago)

Author:

sacerdot

Message:

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:

• extracted/compiler.mli (modified) (6 diffs)

extracted/compiler.mli

@@ -1 +1 @@
 open Preamble
 
+open BitVectorTrie
+
 open CostLabel
 
@@ -31 +33 @@
 open Identifiers
 
+open Exp
+
 open Arithmetic
 
@@ -148 +152 @@
 
 open Initialisation
-
-open BitVectorTrie
 
 open Graphs
@@ -165 +167 @@
   Types.prod, RTLabs_syntax.rTLabs_program) Types.prod Errors.res
 
+open Deqsets
+
+open State
+
+open Bind_new
+
+open BindLists
+
+open Blocks
+
+open TranslateUtils
+
+open AssocList
+
 open String
 
 open LabelledObjects
 
+open I8051
+
+open BackEndOps
+
+open Joint
+
+open RTL
+
+open RTLabsToRTL
+
+open ERTL
+
+open RegisterSet
+
+open RTLToERTL
+
+open ERTLptr
+
+open ERTLToERTLptr
+
+open Fixpoints
+
+open Set_adt
+
+open Liveness
+
+open Interference
+
+open Joint_LTL_LIN
+
+open LTL
+
+open ERTLptrToLTL
+
+open LIN
+
+open Linearise
+
+open LTLToLIN
+
 open ASM
 
+open BitVectorTrieSet
+
+open LINToASM
+
+val compute_fixpoint : Fixpoints.fixpoint_computer
+
+val colour_graph : Interference.coloured_graph_computer
+
 val back_end : RTLabs_syntax.rTLabs_program -> ASM.pseudo_assembly_program
 
 type object_code = BitVector.byte List.list
 
-type costlabel_map = CostLabel.costlabel BitVectorTrie.bitVectorTrie
+type costlabel_map1 = CostLabel.costlabel BitVectorTrie.bitVectorTrie
+
+open Assembly
+
+open Status
+
+open Fetch
+
+open PolicyFront
+
+open PolicyStep
+
+open Policy
 
 val assembler :
-  ASM.pseudo_assembly_program -> (object_code, costlabel_map) Types.prod
+  ASM.pseudo_assembly_program -> (object_code, costlabel_map1) Types.prod
   Errors.res
 
@@ -185 +261 @@
 open AbstractStatus
 
-open Status
-
 open StatusProofs
 
 open Interpret
-
-open Fetch
 
 open ASMCosts
@@ -206 +278 @@
 
 val compile :
-  Csyntax.clight_program -> ((object_code, costlabel_map) Types.prod,
+  Csyntax.clight_program -> ((object_code, costlabel_map1) Types.prod,
   (Csyntax.clight_program, Label.clight_cost_map) Types.dPair) Types.prod
   Errors.res