Ignore:
Timestamp:
Mar 11, 2013, 1:02:02 PM (7 years ago)
Author:
piccolo
Message:

1) Fixed a litte bug in Joint.ma
2) ERTL to ERTLptr correctness proof in place

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTLToERTLptr.ma

    r2820 r2843  
    100100| * #called #args #dest whd in match translate_step; normalize nodelta whd
    101101  [ #l' %{I} %{I} %{I} %
    102   | #r #l' whd %{I} % [2: %{I I} ] % [2: % [2: % [2: %{I} ]]] % try @I %{I} %1 %
     102  | #r #l' whd %{I} %
     103    [2: whd %{I} whd in match step_forall_registers; normalize nodelta
     104        whd in match step_registers; whd in match get_used_registers_from_step;
     105        normalize nodelta normalize cases(\fst called) [#r1 | #b1]
     106        normalize nodelta cases(\snd called) [1,3: #r2 |*: #b2 ]
     107        normalize nodelta /2 by All_mp, I/ % // [1,3,4: %2 % %]
     108        % [%2 %2 % %] %
     109    | %  [2: % [2: % [2: %{I} ]]] % try @I %{I} %1 %
     110    ]
    103111  ]
    104112| #a #l_true whd #l %{I} %{I} % %{I} [ %2 ] %1 %
     
    111119qed.
    112120
     121
    113122definition ertl_to_ertlptr: ertl_program → ertlptr_program ≝
    114123  b_graph_transform_program ERTL ERTLptr translate_data.
Note: See TracChangeset for help on using the changeset viewer.