Changeset 725 for src/Clight/test


Ignore:
Timestamp:
Mar 30, 2011, 4:16:08 PM (10 years ago)
Author:
campbell
Message:

Do some light manual disambiguation to make Clight examples go through more
easily.

Location:
src/Clight/test
Files:
7 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/test/duff.ma

    r717 r725  
    11include "Clight/Animation.ma".
    22
    3 definition myprog := mk_program fundef type
    4   [〈succ_pos_of_nat 0 (* copy *), Internal (
     3definition myprog := mk_program clight_fundef type
     4  [〈succ_pos_of_nat 0 (* copy *), CL_Internal (
    55     mk_function Tvoid [〈succ_pos_of_nat 19, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈succ_pos_of_nat 20, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈succ_pos_of_nat 21, (Tint I32 Signed  )〉 ] [〈succ_pos_of_nat 1, (Tint I32 Signed  )〉 ; 〈succ_pos_of_nat 2, (Tint I32 Signed  )〉 ; 〈succ_pos_of_nat 3, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈succ_pos_of_nat 4, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈succ_pos_of_nat 5, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈succ_pos_of_nat 6, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈succ_pos_of_nat 7, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈succ_pos_of_nat 8, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈succ_pos_of_nat 9, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈succ_pos_of_nat 10, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈succ_pos_of_nat 11, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈succ_pos_of_nat 12, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈succ_pos_of_nat 13, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈succ_pos_of_nat 14, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈succ_pos_of_nat 15, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈succ_pos_of_nat 16, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈succ_pos_of_nat 17, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈succ_pos_of_nat 18, (Tpointer Any (Tint I16 Signed  ))〉 ]
    66       (Ssequence
     
    325325     
    326326   )〉;
    327   〈succ_pos_of_nat 23 (* main *), Internal (
     327  〈succ_pos_of_nat 23 (* main *), CL_Internal (
    328328    mk_function (Tint I32 Signed  ) [] [〈succ_pos_of_nat 24, (Tarray Any (Tint I16 Signed  ) 3)〉 ; 〈succ_pos_of_nat 25, (Tarray Any (Tint I16 Signed  ) 3)〉 ]
    329329      (Ssequence
  • src/Clight/test/factorial.ma

    r717 r725  
    11include "Clight/Animation.ma".
    22
    3 definition myprog := mk_program fundef type
    4   [〈succ_pos_of_nat 0 (* get_input *), External (succ_pos_of_nat 0) Tnil (Tint I32 Signed  )〉;
    5   〈succ_pos_of_nat 1 (* main *), Internal (
     3definition myprog := mk_program clight_fundef type
     4  [〈succ_pos_of_nat 0 (* get_input *), CL_External (succ_pos_of_nat 0) Tnil (Tint I32 Signed  )〉;
     5  〈succ_pos_of_nat 1 (* main *), CL_Internal (
    66    mk_function (Tint I32 Signed  ) [] [〈succ_pos_of_nat 2, (Tint I32 Signed  )〉 ; 〈succ_pos_of_nat 3, (Tint I32 Signed  )〉 ; 〈succ_pos_of_nat 4, (Tint I32 Signed  )〉 ]
    77      (Ssequence
  • src/Clight/test/insertsort.ma

    r717 r725  
    11include "Clight/Animation.ma".
    2 (* FIXME: need this due to punning of fundef? *)
    3 include "Clight/Csyntax.ma".
    42
    5 definition myprog := mk_program fundef type
    6   [〈succ_pos_of_nat 0 (* insert *), Internal (
     3definition myprog := mk_program clight_fundef type
     4  [〈succ_pos_of_nat 0 (* insert *), CL_Internal (
    75     mk_function Tvoid [〈succ_pos_of_nat 2, (Tpointer PData (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil))))〉 ; 〈succ_pos_of_nat 6, (Tpointer Any (Tpointer PData (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil)))))〉 ] [〈succ_pos_of_nat 1, (Tint I32 Signed  )〉 ]
    86       (Ssequence
     
    7674     
    7775   )〉;
    78   〈succ_pos_of_nat 7 (* sort *), Internal (
     76  〈succ_pos_of_nat 7 (* sort *), CL_Internal (
    7977    mk_function Tvoid [〈succ_pos_of_nat 10, (Tpointer Any (Tpointer PData (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil)))))〉 ] [〈succ_pos_of_nat 8, (Tpointer PData (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil))))〉 ; 〈succ_pos_of_nat 5, (Tpointer PData (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil))))〉 ; 〈succ_pos_of_nat 9, (Tpointer PData (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil))))〉 ]
    8078      (Ssequence
     
    127125   
    128126  )〉;
    129   〈succ_pos_of_nat 11 (* out *), External (succ_pos_of_nat 11) (Tcons (Tint I8 Unsigned ) Tnil) Tvoid〉;
    130   〈succ_pos_of_nat 12 (* main *), Internal (
     127  〈succ_pos_of_nat 11 (* out *), CL_External (succ_pos_of_nat 11) (Tcons (Tint I8 Unsigned ) Tnil) Tvoid〉;
     128  〈succ_pos_of_nat 12 (* main *), CL_Internal (
    131129    mk_function (Tint I32 Signed  ) [] [〈succ_pos_of_nat 13, (Tpointer PData (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil))))〉 ]
    132130      (Ssequence
  • src/Clight/test/io.ma

    r717 r725  
    11include "Clight/Animation.ma".
    22
    3 definition myprog := mk_program fundef type
    4   [〈succ_pos_of_nat 0 (* dosomething *), External (succ_pos_of_nat 0) (Tcons (Tint I32 Signed  ) Tnil) (Tint I32 Signed  )〉;
    5   〈succ_pos_of_nat 1 (* main *), Internal (
     3definition myprog := mk_program clight_fundef type
     4  [〈succ_pos_of_nat 0 (* dosomething *), CL_External (succ_pos_of_nat 0) (Tcons (Tint I32 Signed  ) Tnil) (Tint I32 Signed  )〉;
     5  〈succ_pos_of_nat 1 (* main *), CL_Internal (
    66    mk_function (Tint I32 Signed  ) [] [〈succ_pos_of_nat 2, (Tint I32 Signed  )〉 ]
    77      (Ssequence
  • src/Clight/test/io2.ma

    r717 r725  
    11include "Clight/Animation.ma".
    22
    3 definition myprog := mk_program fundef type
    4   [〈succ_pos_of_nat 0 (* dosomething *), External (succ_pos_of_nat 0) (Tcons (Tint I32 Signed  ) Tnil) (Tint I32 Signed  )〉;
    5   〈succ_pos_of_nat 1 (* main *), Internal (
     3definition myprog := mk_program clight_fundef type
     4  [〈succ_pos_of_nat 0 (* dosomething *), CL_External (succ_pos_of_nat 0) (Tcons (Tint I32 Signed  ) Tnil) (Tint I32 Signed  )〉;
     5  〈succ_pos_of_nat 1 (* main *), CL_Internal (
    66    mk_function (Tint I32 Signed  ) [] [〈succ_pos_of_nat 2, (Tint I32 Signed  )〉 ; 〈succ_pos_of_nat 3, (Tint I32 Signed  )〉 ]
    77      (Ssequence
  • src/Clight/test/search.ma

    r717 r725  
    11include "Clight/Animation.ma".
    22
    3 definition myprog := mk_program fundef type
    4   [〈succ_pos_of_nat 0 (* search *), Internal (
     3definition myprog := mk_program clight_fundef type
     4  [〈succ_pos_of_nat 0 (* search *), CL_Internal (
    55     mk_function (Tint I8 Unsigned ) [〈succ_pos_of_nat 4, (Tpointer Any (Tint I8 Unsigned ))〉 ; 〈succ_pos_of_nat 5, (Tint I8 Unsigned )〉 ; 〈succ_pos_of_nat 6, (Tint I8 Unsigned )〉 ] [〈succ_pos_of_nat 1, (Tint I8 Unsigned )〉 ; 〈succ_pos_of_nat 2, (Tint I8 Unsigned )〉 ; 〈succ_pos_of_nat 3, (Tint I8 Unsigned )〉 ]
    66       (Ssequence
     
    114114     
    115115   )〉;
    116   〈succ_pos_of_nat 7 (* main *), Internal (
     116  〈succ_pos_of_nat 7 (* main *), CL_Internal (
    117117    mk_function (Tint I32 Signed  ) [] [〈succ_pos_of_nat 4, (Tarray Any (Tint I8 Unsigned ) 5)〉 ; 〈succ_pos_of_nat 8, (Tint I8 Unsigned )〉 ]
    118118      (Ssequence
  • src/Clight/test/transform1.ma

    r717 r725  
    1919ndefinition skippy_fd : fundef → fundef ≝ λf.
    2020match f with
    21 [ Internal fd ⇒ Internal (skippy_f fd)
    22 | External id args res ⇒ External id args res
     21[ CL_Internal fd ⇒ Internal (skippy_f fd)
     22| CL_External id args res ⇒ External id args res
    2323].
    2424
     
    3131mk_program ??
    3232  (map ?? (λfd. match snd ?? fd with
    33              [ Internal f ⇒
     33             [ CL_Internal f ⇒
    3434               〈fst ?? fd,
    35                 Internal
     35                CL_Internal
    3636                 (mk_function (fn_return f) (fn_params f) (fn_vars f) (skippy_s (fn_body f)))〉
    37              | External _ _ _ ⇒ fd ])
     37             | CL_External _ _ _ ⇒ fd ])
    3838    (prog_funct ?? p))
    3939  (prog_main ?? p)
Note: See TracChangeset for help on using the changeset viewer.