Ignore:
Timestamp:
Mar 8, 2013, 11:18:50 PM (7 years ago)
Author:
sacerdot
Message:

Semantics files committed.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/compiler.mli

    r2775 r2829  
    185185open CostInj
    186186
     187open State
     188
     189open Bind_new
     190
     191open BindLists
     192
     193open Blocks
     194
     195open TranslateUtils
     196
     197open String
     198
     199open LabelledObjects
     200
     201open I8051
     202
     203open BackEndOps
     204
     205open Joint
     206
     207open RTL
     208
     209open RTLabsToRTL
     210
     211open ERTL
     212
     213open RegisterSet
     214
     215open RTLToERTL
     216
     217open ERTLptr
     218
     219open ERTLToERTLptr
     220
     221open Fixpoints
     222
     223open Set_adt
     224
     225open Liveness
     226
     227open Interference
     228
     229open Joint_LTL_LIN
     230
     231open LTL
     232
     233open ERTLptrToLTL
     234
     235open LIN
     236
     237open Linearise
     238
     239open LTLToLIN
     240
     241open ASM
     242
     243open BitVectorTrieSet
     244
     245open LINToASM
     246
     247type pass =
     248| Clight_pass
     249| Clight_switch_removed_pass
     250| Clight_label_pass
     251| Clight_simplified_pass
     252| Cminor_pass
     253| Rtlabs_pass
     254| Rtl_separate_pass
     255| Rtl_uniq_pass
     256| Ertl_pass
     257| Ertlptr_pass
     258| Ltl_pass
     259| Lin_pass
     260
     261val pass_rect_Type4 :
     262  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
     263  -> 'a1 -> pass -> 'a1
     264
     265val pass_rect_Type5 :
     266  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
     267  -> 'a1 -> pass -> 'a1
     268
     269val pass_rect_Type3 :
     270  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
     271  -> 'a1 -> pass -> 'a1
     272
     273val pass_rect_Type2 :
     274  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
     275  -> 'a1 -> pass -> 'a1
     276
     277val pass_rect_Type1 :
     278  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
     279  -> 'a1 -> pass -> 'a1
     280
     281val pass_rect_Type0 :
     282  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
     283  -> 'a1 -> pass -> 'a1
     284
     285val pass_inv_rect_Type4 :
     286  pass -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
     287  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
     288  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
     289
     290val pass_inv_rect_Type3 :
     291  pass -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
     292  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
     293  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
     294
     295val pass_inv_rect_Type2 :
     296  pass -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
     297  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
     298  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
     299
     300val pass_inv_rect_Type1 :
     301  pass -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
     302  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
     303  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
     304
     305val pass_inv_rect_Type0 :
     306  pass -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
     307  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
     308  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
     309
     310val pass_discr : pass -> pass -> __
     311
     312val pass_jmdiscr : pass -> pass -> __
     313
     314type syntax_of_pass = __
     315
     316type observe_pass = pass -> syntax_of_pass -> Types.unit0
     317
    187318val front_end :
    188   Csyntax.clight_program -> ((CostLabel.costlabel, Csyntax.clight_program)
    189   Types.prod, RTLabs_syntax.rTLabs_program) Types.prod Errors.res
    190 
    191 open State
    192 
    193 open Bind_new
    194 
    195 open BindLists
    196 
    197 open Blocks
    198 
    199 open TranslateUtils
    200 
    201 open String
    202 
    203 open LabelledObjects
    204 
    205 open I8051
    206 
    207 open BackEndOps
    208 
    209 open Joint
    210 
    211 open RTL
    212 
    213 open RTLabsToRTL
    214 
    215 open ERTL
    216 
    217 open RegisterSet
    218 
    219 open RTLToERTL
    220 
    221 open ERTLptr
    222 
    223 open ERTLToERTLptr
    224 
    225 open Fixpoints
    226 
    227 open Set_adt
    228 
    229 open Liveness
    230 
    231 open Interference
    232 
    233 open Joint_LTL_LIN
    234 
    235 open LTL
    236 
    237 open ERTLptrToLTL
    238 
    239 open LIN
    240 
    241 open Linearise
    242 
    243 open LTLToLIN
    244 
    245 open ASM
    246 
    247 open BitVectorTrieSet
    248 
    249 open LINToASM
     319  observe_pass -> Csyntax.clight_program -> ((CostLabel.costlabel,
     320  Csyntax.clight_program) Types.prod, RTLabs_syntax.rTLabs_program)
     321  Types.prod Errors.res
    250322
    251323val compute_fixpoint : Fixpoints.fixpoint_computer
     
    254326
    255327val back_end :
    256   RTLabs_syntax.rTLabs_program -> ((ASM.pseudo_assembly_program,
    257   Joint.stack_cost_model) Types.prod, Nat.nat) Types.prod Errors.res
     328  observe_pass -> RTLabs_syntax.rTLabs_program ->
     329  ((ASM.pseudo_assembly_program, Joint.stack_cost_model) Types.prod, Nat.nat)
     330  Types.prod Errors.res
    258331
    259332open Assembly
     
    364437val compiler_output_jmdiscr : compiler_output -> compiler_output -> __
    365438
    366 val compile : Csyntax.clight_program -> compiler_output Errors.res
    367 
     439val compile :
     440  observe_pass -> Csyntax.clight_program -> compiler_output Errors.res
     441
Note: See TracChangeset for help on using the changeset viewer.