Ignore:
Timestamp:
Feb 23, 2013, 1:16:55 AM (8 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/smallstepExec.mli

    r2649 r2717  
    4747open IOMonad
    4848
     49open Exp
     50
    4951open Arithmetic
    5052
     
    5860
    5961open Integers
     62
     63open BitVectorTrie
    6064
    6165open CostLabel
     
    225229
    226230type assert0 = __
     231
     232type assert_nz = __
    227233
    228234type after_aux = __
     
    339345  'a2) execution) Types.prod Types.option
    340346
     347val exec_steps :
     348  Nat.nat -> ('a1, 'a2) fullexec -> __ -> __ -> ((__, Events.trace)
     349  Types.prod List.list, __) Types.prod Errors.res
     350
     351val gather_trace : ('a1, Events.trace) Types.prod List.list -> Events.trace
     352
     353val switch_trace_aux :
     354  Events.trace -> ('a1, Events.trace) Types.prod List.list -> 'a1 ->
     355  (Events.trace, 'a1) Types.prod List.list
     356
     357val switch_trace :
     358  ('a1, Events.trace) Types.prod List.list -> 'a1 -> (Events.trace, 'a1)
     359  Types.prod List.list
     360
Note: See TracChangeset for help on using the changeset viewer.