Changeset 2960 for extracted/policy.ml


Ignore:
Timestamp:
Mar 26, 2013, 4:51:40 PM (7 years ago)
Author:
sacerdot
Message:

New extraction, it diverges in RTL execution now.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/policy.ml

    r2904 r2960  
    9494let rec jump_expansion_internal program n =
    9595  let labels = PolicyFront.create_label_map (Types.pi1 program) in
    96   let rec aux res =
    97 prerr_endline "JEI_start";
    98    let { Types.fst = no_ch; Types.snd = z } = res in
    99     match z with
    100      | Types.None ->
    101        { Types.fst = Bool.False; Types.snd = Types.None }
    102      | Types.Some op ->
    103          match no_ch with
    104          | Bool.True -> res
    105          | Bool.False ->
    106            aux
    107             (Types.pi1
    108              (PolicyStep.jump_expansion_step program (Types.pi1 labels)
    109                op))
    110   in
    111    aux
    112     { Types.fst = Bool.False; Types.snd =
    113        (Types.pi1
    114          (PolicyFront.jump_expansion_start program (Types.pi1 labels))) }
    115 (*
    11696  (match n with
    11797   | Nat.O ->
     
    134114              Types.pi1
    135115                (PolicyStep.jump_expansion_step program (Types.pi1 labels)
    136                   op))) __)) __)) __*)
     116                  op))) __)) __)) __
    137117
    138118(** val measure_int :
Note: See TracChangeset for help on using the changeset viewer.