Changeset 1991


Ignore:
Timestamp:
May 24, 2012, 4:24:55 PM (5 years ago)
Author:
campbell
Message:

Put the front end transformations together and make an example use it.

Location:
src
Files:
2 added
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/test/search.c.ma

    r1876 r1991  
    184184.
    185185
    186 example exec: finishes_with (repr I32 3) ? (exec_up_to clight_fullexec myprog 1000 [ ]).
    187 normalize  (* you can examine the result here *)
    188 %
    189 qed.
    190 
    191 include "Clight/toCminor.ma".
    192 include "Cminor/semantics.ma".
    193 
    194 example e1: finishes_with (repr I32 3) ? (bind ? (snapshot state) (clight_to_cminor myprog) (λp. exec_up_to Cminor_fullexec p 1000 [ ])).
    195 (*
    196 example e1: finishes_with (repr I32 3) ? (do p ← clight_to_cminor myprog; exec_up_to Cminor_fullexec p 1000 [ ]).
    197 *)
    198 normalize
    199 %
    200 qed.
    201 
    202 include "Cminor/toRTLabs.ma".
    203 include "RTLabs/semantics.ma".
    204 
    205 example e2: finishes_with (repr 3) ? (
    206 do p1 ← clight_to_cminor myprog;
    207 bind ? (snapshot state) (cminor_to_rtlabs p1) (λp2.
    208  exec_up_to RTLabs_fullexec p2 1000 [ ])).
    209 (*
    210 example e2: finishes_with (repr 3) ? (
    211 do p1 ← clight_to_cminor myprog;
    212 do p2 ← cminor_to_rtlabs p1;
    213  exec_up_to RTLabs_fullexec p2 1000 [ ]).*)
    214 normalize
    215 %
    216 qed.
    217 (*
    218 example csc: True.
    219 letin yyy ≝ (
    220 let xxx ≝ (clight_to_cminor myprog) in
    221 do p ← xxx ; cminor_to_rtlabs p)
    222 normalize in yyy;
    223 include "RTLabs/RTLabsToRTL.ma".
    224 
    225 example csc: True.
    226 letin xxx ≝ (clight_to_cminor myprog)
    227 letin yyy ≝ (do p ← xxx ; cminor_to_rtlabs p)
    228 letin zzz ≝ (do p ← yyy ; rtlabs_to_rtl p)
    229 @⊥ normalize in xxx;
    230 *)
Note: See TracChangeset for help on using the changeset viewer.