Changeset 725


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

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

Location:
src/Clight
Files:
10 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/Cexec.ma

    r718 r725  
    636636| Callstate f0 vargs k m ⇒
    637637  match f0 with
    638   [ Internal f ⇒
     638  [ CL_Internal f ⇒
    639639    match exec_alloc_variables empty_env m ((fn_params f) @ (fn_vars f)) with [ pair e m1 ⇒
    640640      ! m2 ← exec_bind_parameters e m1 (fn_params f) vargs;
    641641      ret ? 〈E0, State f (fn_body f) k e m2〉
    642642    ]
    643   | External f argtys retty ⇒
     643  | CL_External f argtys retty ⇒
    644644      ! evargs ← check_eventval_list vargs (typlist_of_typelist argtys);
    645645      ! evres ← do_io f evargs (proj_sig_res (signature_of_type argtys retty));
  • src/Clight/Csem.ma

    r717 r725  
    452452  and function pointers to their definitions.  (See module [Globalenvs].) *)
    453453
    454 definition genv ≝ (genv_t Genv) fundef.
     454definition genv ≝ (genv_t Genv) clight_fundef.
    455455
    456456(* * The local environment maps local variables to block references.
     
    924924      ∀m: mem.  state
    925925  | Callstate:
    926       ∀fd: fundef.
     926      ∀fd: clight_fundef.
    927927      ∀args: list val.
    928928      ∀k: cont.
     
    11521152      alloc_variables empty_env m ((fn_params f) @ (fn_vars f)) e m1 →
    11531153      bind_parameters e m1 (fn_params f) vargs m2 →
    1154       step ge (Callstate (Internal f) vargs k m)
     1154      step ge (Callstate (CL_Internal f) vargs k m)
    11551155           E0 (State f (fn_body f) k e m2)
    11561156
    11571157  | step_external_function: ∀id,targs,tres,vargs,k,m,vres,t.
    11581158      event_match (external_function id targs tres) vargs t vres →
    1159       step ge (Callstate (External id targs tres) vargs k m)
     1159      step ge (Callstate (CL_External id targs tres) vargs k m)
    11601160            t (Returnstate vres k m)
    11611161
  • src/Clight/Csyntax.ma

    r720 r725  
    326326}.
    327327
    328 (* * Functions can either be defined ([Internal]) or declared as
    329   external functions ([External]). *)
    330 
    331 inductive fundef : Type[0] ≝
    332   | Internal: function → fundef
    333   | External: ident → typelist → type → fundef.
     328(* * Functions can either be defined ([CL_Internal]) or declared as
     329  external functions ([CL_External]).  Similar to the AST definition, but
     330  with high level type information for external functions. *)
     331
     332inductive clight_fundef : Type[0] ≝
     333  | CL_Internal: function → clight_fundef
     334  | CL_External: ident → typelist → type → clight_fundef.
    334335
    335336(* * ** Programs *)
     
    339340  data.  See module [AST] for more details. *)
    340341
    341 definition clight_program : Type[0] ≝ program fundef type.
     342definition clight_program : Type[0] ≝ program clight_fundef type.
    342343
    343344(* * * Operations over types *)
     
    354355  Tfunction (type_of_params (fn_params f)) (fn_return f).
    355356
    356 definition type_of_fundef : fundef → type ≝ λf.
     357definition type_of_fundef : clight_fundef → type ≝ λf.
    357358  match f with
    358   [ Internal fd ⇒ type_of_function fd
    359   | External id args res ⇒ Tfunction args res
     359  [ CL_Internal fd ⇒ type_of_function fd
     360  | CL_External id args res ⇒ Tfunction args res
    360361  ].
    361362
  • 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.