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/smallstepExec.ml

    r2649 r2717  
    4747open IOMonad
    4848
     49open Exp
     50
    4951open Arithmetic
    5052
     
    5860
    5961open Integers
     62
     63open BitVectorTrie
    6064
    6165open CostLabel
     
    9599    ('a1, 'a2, (Events.trace, __) Types.prod) IOMonad.iO) -> 'a3) -> ('a1,
    96100    'a2) trans_system -> 'a3 **)
    97 let rec trans_system_rect_Type4 h_mk_trans_system x_7818 =
    98   let { is_final = is_final0; step = step0 } = x_7818 in
     101let rec trans_system_rect_Type4 h_mk_trans_system x_5847 =
     102  let { is_final = is_final0; step = step0 } = x_5847 in
    99103  h_mk_trans_system __ __ is_final0 step0
    100104
     
    103107    ('a1, 'a2, (Events.trace, __) Types.prod) IOMonad.iO) -> 'a3) -> ('a1,
    104108    'a2) trans_system -> 'a3 **)
    105 let rec trans_system_rect_Type5 h_mk_trans_system x_7820 =
    106   let { is_final = is_final0; step = step0 } = x_7820 in
     109let rec trans_system_rect_Type5 h_mk_trans_system x_5849 =
     110  let { is_final = is_final0; step = step0 } = x_5849 in
    107111  h_mk_trans_system __ __ is_final0 step0
    108112
     
    111115    ('a1, 'a2, (Events.trace, __) Types.prod) IOMonad.iO) -> 'a3) -> ('a1,
    112116    'a2) trans_system -> 'a3 **)
    113 let rec trans_system_rect_Type3 h_mk_trans_system x_7822 =
    114   let { is_final = is_final0; step = step0 } = x_7822 in
     117let rec trans_system_rect_Type3 h_mk_trans_system x_5851 =
     118  let { is_final = is_final0; step = step0 } = x_5851 in
    115119  h_mk_trans_system __ __ is_final0 step0
    116120
     
    119123    ('a1, 'a2, (Events.trace, __) Types.prod) IOMonad.iO) -> 'a3) -> ('a1,
    120124    'a2) trans_system -> 'a3 **)
    121 let rec trans_system_rect_Type2 h_mk_trans_system x_7824 =
    122   let { is_final = is_final0; step = step0 } = x_7824 in
     125let rec trans_system_rect_Type2 h_mk_trans_system x_5853 =
     126  let { is_final = is_final0; step = step0 } = x_5853 in
    123127  h_mk_trans_system __ __ is_final0 step0
    124128
     
    127131    ('a1, 'a2, (Events.trace, __) Types.prod) IOMonad.iO) -> 'a3) -> ('a1,
    128132    'a2) trans_system -> 'a3 **)
    129 let rec trans_system_rect_Type1 h_mk_trans_system x_7826 =
    130   let { is_final = is_final0; step = step0 } = x_7826 in
     133let rec trans_system_rect_Type1 h_mk_trans_system x_5855 =
     134  let { is_final = is_final0; step = step0 } = x_5855 in
    131135  h_mk_trans_system __ __ is_final0 step0
    132136
     
    135139    ('a1, 'a2, (Events.trace, __) Types.prod) IOMonad.iO) -> 'a3) -> ('a1,
    136140    'a2) trans_system -> 'a3 **)
    137 let rec trans_system_rect_Type0 h_mk_trans_system x_7828 =
    138   let { is_final = is_final0; step = step0 } = x_7828 in
     141let rec trans_system_rect_Type0 h_mk_trans_system x_5857 =
     142  let { is_final = is_final0; step = step0 } = x_5857 in
    139143  h_mk_trans_system __ __ is_final0 step0
    140144
     
    223227    (__ -> __ -> (__, __) trans_system -> __ -> (__ -> Bool.bool) -> 'a1) ->
    224228    await_value_stuff -> 'a1 **)
    225 let rec await_value_stuff_rect_Type4 h_mk_await_value_stuff x_7990 =
    226   let { avs_exec = avs_exec0; avs_g = avs_g0; avs_inv = avs_inv0 } = x_7990
     229let rec await_value_stuff_rect_Type4 h_mk_await_value_stuff x_6019 =
     230  let { avs_exec = avs_exec0; avs_g = avs_g0; avs_inv = avs_inv0 } = x_6019
    227231  in
    228232  h_mk_await_value_stuff __ __ avs_exec0 avs_g0 avs_inv0
     
    231235    (__ -> __ -> (__, __) trans_system -> __ -> (__ -> Bool.bool) -> 'a1) ->
    232236    await_value_stuff -> 'a1 **)
    233 let rec await_value_stuff_rect_Type5 h_mk_await_value_stuff x_7992 =
    234   let { avs_exec = avs_exec0; avs_g = avs_g0; avs_inv = avs_inv0 } = x_7992
     237let rec await_value_stuff_rect_Type5 h_mk_await_value_stuff x_6021 =
     238  let { avs_exec = avs_exec0; avs_g = avs_g0; avs_inv = avs_inv0 } = x_6021
    235239  in
    236240  h_mk_await_value_stuff __ __ avs_exec0 avs_g0 avs_inv0
     
    239243    (__ -> __ -> (__, __) trans_system -> __ -> (__ -> Bool.bool) -> 'a1) ->
    240244    await_value_stuff -> 'a1 **)
    241 let rec await_value_stuff_rect_Type3 h_mk_await_value_stuff x_7994 =
    242   let { avs_exec = avs_exec0; avs_g = avs_g0; avs_inv = avs_inv0 } = x_7994
     245let rec await_value_stuff_rect_Type3 h_mk_await_value_stuff x_6023 =
     246  let { avs_exec = avs_exec0; avs_g = avs_g0; avs_inv = avs_inv0 } = x_6023
    243247  in
    244248  h_mk_await_value_stuff __ __ avs_exec0 avs_g0 avs_inv0
     
    247251    (__ -> __ -> (__, __) trans_system -> __ -> (__ -> Bool.bool) -> 'a1) ->
    248252    await_value_stuff -> 'a1 **)
    249 let rec await_value_stuff_rect_Type2 h_mk_await_value_stuff x_7996 =
    250   let { avs_exec = avs_exec0; avs_g = avs_g0; avs_inv = avs_inv0 } = x_7996
     253let rec await_value_stuff_rect_Type2 h_mk_await_value_stuff x_6025 =
     254  let { avs_exec = avs_exec0; avs_g = avs_g0; avs_inv = avs_inv0 } = x_6025
    251255  in
    252256  h_mk_await_value_stuff __ __ avs_exec0 avs_g0 avs_inv0
     
    255259    (__ -> __ -> (__, __) trans_system -> __ -> (__ -> Bool.bool) -> 'a1) ->
    256260    await_value_stuff -> 'a1 **)
    257 let rec await_value_stuff_rect_Type1 h_mk_await_value_stuff x_7998 =
    258   let { avs_exec = avs_exec0; avs_g = avs_g0; avs_inv = avs_inv0 } = x_7998
     261let rec await_value_stuff_rect_Type1 h_mk_await_value_stuff x_6027 =
     262  let { avs_exec = avs_exec0; avs_g = avs_g0; avs_inv = avs_inv0 } = x_6027
    259263  in
    260264  h_mk_await_value_stuff __ __ avs_exec0 avs_g0 avs_inv0
     
    263267    (__ -> __ -> (__, __) trans_system -> __ -> (__ -> Bool.bool) -> 'a1) ->
    264268    await_value_stuff -> 'a1 **)
    265 let rec await_value_stuff_rect_Type0 h_mk_await_value_stuff x_8000 =
    266   let { avs_exec = avs_exec0; avs_g = avs_g0; avs_inv = avs_inv0 } = x_8000
     269let rec await_value_stuff_rect_Type0 h_mk_await_value_stuff x_6029 =
     270  let { avs_exec = avs_exec0; avs_g = avs_g0; avs_inv = avs_inv0 } = x_6029
    267271  in
    268272  h_mk_await_value_stuff __ __ avs_exec0 avs_g0 avs_inv0
     
    317321
    318322type assert0 = __
     323
     324type assert_nz = __
    319325
    320326type after_aux = __
     
    450456    (__ -> ('a1, 'a2) trans_system -> (__ -> __) -> (__ -> __ Errors.res) ->
    451457    'a3) -> ('a1, 'a2) fullexec -> 'a3 **)
    452 let rec fullexec_rect_Type4 h_mk_fullexec x_8018 =
     458let rec fullexec_rect_Type4 h_mk_fullexec x_6047 =
    453459  let { es1 = es2; make_global = make_global0; make_initial_state =
    454     make_initial_state0 } = x_8018
     460    make_initial_state0 } = x_6047
    455461  in
    456462  h_mk_fullexec __ es2 make_global0 make_initial_state0
     
    459465    (__ -> ('a1, 'a2) trans_system -> (__ -> __) -> (__ -> __ Errors.res) ->
    460466    'a3) -> ('a1, 'a2) fullexec -> 'a3 **)
    461 let rec fullexec_rect_Type5 h_mk_fullexec x_8020 =
     467let rec fullexec_rect_Type5 h_mk_fullexec x_6049 =
    462468  let { es1 = es2; make_global = make_global0; make_initial_state =
    463     make_initial_state0 } = x_8020
     469    make_initial_state0 } = x_6049
    464470  in
    465471  h_mk_fullexec __ es2 make_global0 make_initial_state0
     
    468474    (__ -> ('a1, 'a2) trans_system -> (__ -> __) -> (__ -> __ Errors.res) ->
    469475    'a3) -> ('a1, 'a2) fullexec -> 'a3 **)
    470 let rec fullexec_rect_Type3 h_mk_fullexec x_8022 =
     476let rec fullexec_rect_Type3 h_mk_fullexec x_6051 =
    471477  let { es1 = es2; make_global = make_global0; make_initial_state =
    472     make_initial_state0 } = x_8022
     478    make_initial_state0 } = x_6051
    473479  in
    474480  h_mk_fullexec __ es2 make_global0 make_initial_state0
     
    477483    (__ -> ('a1, 'a2) trans_system -> (__ -> __) -> (__ -> __ Errors.res) ->
    478484    'a3) -> ('a1, 'a2) fullexec -> 'a3 **)
    479 let rec fullexec_rect_Type2 h_mk_fullexec x_8024 =
     485let rec fullexec_rect_Type2 h_mk_fullexec x_6053 =
    480486  let { es1 = es2; make_global = make_global0; make_initial_state =
    481     make_initial_state0 } = x_8024
     487    make_initial_state0 } = x_6053
    482488  in
    483489  h_mk_fullexec __ es2 make_global0 make_initial_state0
     
    486492    (__ -> ('a1, 'a2) trans_system -> (__ -> __) -> (__ -> __ Errors.res) ->
    487493    'a3) -> ('a1, 'a2) fullexec -> 'a3 **)
    488 let rec fullexec_rect_Type1 h_mk_fullexec x_8026 =
     494let rec fullexec_rect_Type1 h_mk_fullexec x_6055 =
    489495  let { es1 = es2; make_global = make_global0; make_initial_state =
    490     make_initial_state0 } = x_8026
     496    make_initial_state0 } = x_6055
    491497  in
    492498  h_mk_fullexec __ es2 make_global0 make_initial_state0
     
    495501    (__ -> ('a1, 'a2) trans_system -> (__ -> __) -> (__ -> __ Errors.res) ->
    496502    'a3) -> ('a1, 'a2) fullexec -> 'a3 **)
    497 let rec fullexec_rect_Type0 h_mk_fullexec x_8028 =
     503let rec fullexec_rect_Type0 h_mk_fullexec x_6057 =
    498504  let { es1 = es2; make_global = make_global0; make_initial_state =
    499     make_initial_state0 } = x_8028
     505    make_initial_state0 } = x_6057
    500506  in
    501507  h_mk_fullexec __ es2 make_global0 make_initial_state0
     
    578584   | E_interact (x0, x1) -> Types.None)
    579585
     586(** val exec_steps :
     587    Nat.nat -> ('a1, 'a2) fullexec -> __ -> __ -> ((__, Events.trace)
     588    Types.prod List.list, __) Types.prod Errors.res **)
     589let rec exec_steps n fx g0 s =
     590  match n with
     591  | Nat.O ->
     592    Obj.magic
     593      (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = List.Nil;
     594        Types.snd = s })
     595  | Nat.S m ->
     596    (match fx.es1.is_final g0 s with
     597     | Types.None ->
     598       (match fx.es1.step g0 s with
     599        | IOMonad.Interact (x, x0) ->
     600          Errors.Error (Errors.msg ErrorMessages.UnexpectedIO)
     601        | IOMonad.Value trs ->
     602          Obj.magic
     603            (Monad.m_bind2 (Monad.max_def Errors.res0)
     604              (Obj.magic (exec_steps m fx g0 trs.Types.snd)) (fun tl s' ->
     605              Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
     606                (List.Cons ({ Types.fst = s; Types.snd = trs.Types.fst },
     607                tl)); Types.snd = s' }))
     608        | IOMonad.Wrong m0 -> Errors.Error m0)
     609     | Types.Some r ->
     610       Errors.Error (Errors.msg ErrorMessages.TerminatedEarly))
     611
     612(** val gather_trace :
     613    ('a1, Events.trace) Types.prod List.list -> Events.trace **)
     614let rec gather_trace = function
     615| List.Nil -> Events.e0
     616| List.Cons (h, t) -> Events.eapp h.Types.snd (gather_trace t)
     617
     618(** val switch_trace_aux :
     619    Events.trace -> ('a1, Events.trace) Types.prod List.list -> 'a1 ->
     620    (Events.trace, 'a1) Types.prod List.list **)
     621let rec switch_trace_aux tr l s' =
     622  match l with
     623  | List.Nil -> List.Cons ({ Types.fst = tr; Types.snd = s' }, List.Nil)
     624  | List.Cons (h, t) ->
     625    List.Cons ({ Types.fst = tr; Types.snd = h.Types.fst },
     626      (switch_trace_aux h.Types.snd t s'))
     627
     628(** val switch_trace :
     629    ('a1, Events.trace) Types.prod List.list -> 'a1 -> (Events.trace, 'a1)
     630    Types.prod List.list **)
     631let switch_trace l s' =
     632  match l with
     633  | List.Nil -> List.Nil
     634  | List.Cons (h, t) -> switch_trace_aux h.Types.snd t s'
     635
Note: See TracChangeset for help on using the changeset viewer.