Ignore:
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:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/compiler.mli

    r2649 r2717  
    11open Preamble
    22
     3open BitVectorTrie
     4
    35open CostLabel
    46
     
    3133open Identifiers
    3234
     35open Exp
     36
    3337open Arithmetic
    3438
     
    148152
    149153open Initialisation
    150 
    151 open BitVectorTrie
    152154
    153155open Graphs
     
    165167  Types.prod, RTLabs_syntax.rTLabs_program) Types.prod Errors.res
    166168
     169open Deqsets
     170
     171open State
     172
     173open Bind_new
     174
     175open BindLists
     176
     177open Blocks
     178
     179open TranslateUtils
     180
     181open AssocList
     182
    167183open String
    168184
    169185open LabelledObjects
    170186
     187open I8051
     188
     189open BackEndOps
     190
     191open Joint
     192
     193open RTL
     194
     195open RTLabsToRTL
     196
     197open ERTL
     198
     199open RegisterSet
     200
     201open RTLToERTL
     202
     203open ERTLptr
     204
     205open ERTLToERTLptr
     206
     207open Fixpoints
     208
     209open Set_adt
     210
     211open Liveness
     212
     213open Interference
     214
     215open Joint_LTL_LIN
     216
     217open LTL
     218
     219open ERTLptrToLTL
     220
     221open LIN
     222
     223open Linearise
     224
     225open LTLToLIN
     226
    171227open ASM
    172228
     229open BitVectorTrieSet
     230
     231open LINToASM
     232
     233val compute_fixpoint : Fixpoints.fixpoint_computer
     234
     235val colour_graph : Interference.coloured_graph_computer
     236
    173237val back_end : RTLabs_syntax.rTLabs_program -> ASM.pseudo_assembly_program
    174238
    175239type object_code = BitVector.byte List.list
    176240
    177 type costlabel_map = CostLabel.costlabel BitVectorTrie.bitVectorTrie
     241type costlabel_map1 = CostLabel.costlabel BitVectorTrie.bitVectorTrie
     242
     243open Assembly
     244
     245open Status
     246
     247open Fetch
     248
     249open PolicyFront
     250
     251open PolicyStep
     252
     253open Policy
    178254
    179255val assembler :
    180   ASM.pseudo_assembly_program -> (object_code, costlabel_map) Types.prod
     256  ASM.pseudo_assembly_program -> (object_code, costlabel_map1) Types.prod
    181257  Errors.res
    182258
     
    185261open AbstractStatus
    186262
    187 open Status
    188 
    189263open StatusProofs
    190264
    191265open Interpret
    192 
    193 open Fetch
    194266
    195267open ASMCosts
     
    206278
    207279val compile :
    208   Csyntax.clight_program -> ((object_code, costlabel_map) Types.prod,
     280  Csyntax.clight_program -> ((object_code, costlabel_map1) Types.prod,
    209281  (Csyntax.clight_program, Label.clight_cost_map) Types.dPair) Types.prod
    210282  Errors.res
Note: See TracChangeset for help on using the changeset viewer.