Changeset 731 for src/Clight


Ignore:
Timestamp:
Apr 1, 2011, 1:35:18 PM (10 years ago)
Author:
campbell
Message:

Common definition for animation semantics, and factor out IO definitions.

Location:
src/Clight
Files:
7 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/Cexec.ma

    r725 r731  
    22
    33include "utilities/extralib.ma".
    4 include "common/IOMonad.ma".
     4include "common/IO.ma".
    55include "common/SmallstepExec.ma".
    66include "Clight/Csem.ma".
     
    439439qed.
    440440
    441 (* Checking types of values given to / received from an external function call. *)
    442 
    443 definition eventval_type : ∀ty:typ. Type[0] ≝
    444 λty. match ty with [ ASTint ⇒ int | ASTptr _ ⇒ False | ASTfloat ⇒ float ].
    445 
    446 definition mk_eventval: ∀ty:typ. eventval_type ty → eventval ≝
    447 λty:typ. match ty return λty'.eventval_type ty' → eventval with [ ASTint ⇒ λv.EVint v | ASTptr r ⇒ ? | ASTfloat ⇒ λv.EVfloat v ].
    448 *; qed.
    449 
    450 definition mk_val: ∀ty:typ. eventval_type ty → val ≝
    451 λty:typ. match ty return λty'.eventval_type ty' → val with [ ASTint ⇒ λv.Vint v | ASTptr r ⇒ ? | ASTfloat ⇒ λv.Vfloat v ].
    452 *; qed.
    453 
    454 lemma mk_val_correct: ∀ty:typ. ∀v:eventval_type ty.
    455   eventval_match (mk_eventval ty v) ty (mk_val ty v).
    456 #ty cases ty; normalize; // * *; qed.
    457 
    458 definition convert_eventval : ∀ev:eventval. ∀ty:typ. res val ≝
    459 λev,ty.
    460 match ty with
    461 [ ASTint ⇒ match ev with [ EVint i ⇒ OK ? (Vint i) | _ ⇒ Error ? ]
    462 | ASTfloat ⇒ match ev with [ EVfloat f ⇒ OK ? (Vfloat f) | _ ⇒ Error ? ]
    463 | _ ⇒ Error ?
    464 ].
    465 
    466 definition check_eventval' : ∀v:val. ∀ty:typ. res eventval ≝
    467 λv,ty.
    468 match ty with
    469 [ ASTint ⇒ match v with [ Vint i ⇒ OK ? (EVint i) | _ ⇒ Error ? ]
    470 | ASTfloat ⇒ match v with [ Vfloat f ⇒ OK ? (EVfloat f) | _ ⇒ Error ? ]
    471 | _ ⇒ Error ?
    472 ].
    473 
    474 let rec check_eventval_list (vs: list val) (tys: list typ) : res (list eventval) ≝
    475 match vs with
    476 [ nil ⇒ match tys with [ nil ⇒ OK ? (nil ?) | _ ⇒ Error ? ]
    477 | cons v vt ⇒
    478   match tys with
    479   [ nil ⇒ Error ?
    480   | cons ty tyt ⇒
    481     do ev ← check_eventval' v ty;
    482     do evt ← check_eventval_list vt tyt;
    483     OK ? (ev::evt)
    484   ]
    485 ].
    486 
    487 (* IO monad *)
    488 
    489 (* Interactions are function calls that return a value and do not change
    490    the rest of the Clight program's state. *)
    491 record io_out : Type[0] ≝
    492 { io_function: ident
    493 ; io_args: list eventval
    494 ; io_in_typ: typ
    495 }.
    496 
    497 definition io_in ≝ λo. eventval_type (io_in_typ o).
    498 
    499 definition do_io : ident → list eventval → ∀t:typ. IO io_out io_in (eventval_type t) ≝
    500 λfn,args,t. Interact ??? (mk_io_out fn args t) (λres. Value ??? res).
    501 
    502 definition ret: ∀T. T → (IO io_out io_in T) ≝
    503 λT,x.(Value ?? T x).
    504441
    505442(* execution *)
     
    729666λs.match s with [ State f s k e m ⇒ m | Callstate f a k m ⇒ m | Returnstate r k m ⇒ m ].
    730667
    731 definition clight_exec : execstep
     668definition clight_exec : execstep io_out io_in
    732669  mk_execstep … is_final mem_of_state exec_step.
    733670
    734 definition exec_inf : ∀p:clight_program. execution state io_out io_in ≝
    735 λp.
    736   match make_initial_state p with
    737   [ OK gs ⇒ exec_inf_aux clight_exec (\fst gs) (ret ? 〈E0,\snd gs〉)
    738   | _ ⇒ e_wrong ???
    739   ].
     671definition clight_fullexec : fullexec io_out io_in ≝
     672  mk_fullexec ?? clight_exec ? make_initial_state.
  • src/Clight/test/duff.ma

    r726 r731  
    1 include "Clight/Animation.ma".
     1include "Clight/Cexec.ma".
     2include "common/Animation.ma".
    23
    34definition myprog := mk_program clight_fundef type
     
    403404.
    404405
    405 example exec:
    406   (do 〈t,s〉 ← exec_up_to myprog 1000 [EVint (repr 0)]; OK ? (is_final s)) = OK ? (Some ? (repr 6)).
     406example exec: finishes_with (repr 6) ? (exec_up_to clight_fullexec myprog 1000 [EVint (repr 0)]).
    407407normalize @refl
    408408qed.
  • src/Clight/test/factorial.ma

    r726 r731  
    1 include "Clight/Animation.ma".
     1include "Clight/Cexec.ma".
     2include "common/Animation.ma".
    23
    34definition myprog := mk_program clight_fundef type
     
    4344.
    4445
    45 example exec:
    46   (do 〈t,s〉 ← exec_up_to myprog 1000 [EVint (repr 5)]; OK ? (is_final s)) = OK ? (Some ? (repr 120)).
     46example exec: finishes_with (repr 120) ? (exec_up_to clight_fullexec myprog 1000 [EVint (repr 5)]).
    4747normalize  (* you can examine the result here *)
    4848@refl qed.
  • src/Clight/test/insertsort.ma

    r726 r731  
    1 include "Clight/Animation.ma".
     1include "Clight/Cexec.ma".
     2include "common/Animation.ma".
    23
    34definition myprog := mk_program clight_fundef type
     
    199200
    200201example exec:
    201   (do 〈t,s〉 ← exec_up_to myprog 1000 [EVint (repr 0);EVint (repr 0);EVint (repr 0);EVint (repr 0);EVint (repr 0);EVint (repr 0);EVint (repr 0)];
    202    OK ? t) = OK ?
     202  (do s ← exec_up_to clight_fullexec myprog 1000
     203     [EVint (repr 0);EVint (repr 0);EVint (repr 0);EVint (repr 0);EVint (repr 0);EVint (repr 0);EVint (repr 0)];
     204   match s with [ finished t _ _ ⇒ OK ? t | _ ⇒ Error ? ]) = OK ?
    203205[EVextcall (ident_of_nat 11) [EVint (repr 36)] (EVint (repr 0));
    204206 EVextcall (ident_of_nat 11) [EVint (repr 69)] (EVint (repr 0));
  • src/Clight/test/io.ma

    r726 r731  
    1 include "Clight/Animation.ma".
     1include "Clight/Cexec.ma".
     2include "common/Animation.ma".
    23
    34definition myprog := mk_program clight_fundef type
     
    2122
    2223example exec:
    23  (do 〈t,s〉 ← exec_up_to myprog 1000 [EVint (repr 7)]; do r ← opt_to_res … (is_final s); OK ? 〈t,r〉) =
     24 (do r ← exec_up_to clight_fullexec myprog 1000 [EVint (repr 7)];
     25  match r with [ finished t r _ ⇒ OK ? 〈t,r〉 | _ ⇒ Error ? ]) =
    2426 OK ? 〈[EVextcall (ident_of_nat 0) [EVint (repr 10)] (EVint (repr 7))], repr 7〉.
    2527normalize  (* you can examine the result here *)
  • src/Clight/test/io2.ma

    r726 r731  
    1 include "Clight/Animation.ma".
     1include "Clight/Cexec.ma".
     2include "common/Animation.ma".
    23
    34definition myprog := mk_program clight_fundef type
     
    3031
    3132example exec:
    32  (do 〈t,s〉 ← exec_up_to myprog 1000 [EVint (repr 7)]; do r ← opt_to_res … (is_final s); OK ? 〈t,r〉) =
     33 (do r ← exec_up_to clight_fullexec myprog 1000 [EVint (repr 7)];
     34   match r with [ finished t r _ ⇒ OK ? 〈t,r〉 | _ ⇒ Error ? ]) =
    3335 OK ? 〈[EVextcall (ident_of_nat 0) [EVint (repr 10)] (EVint (repr 7))], repr 9〉.
    3436normalize  (* you can examine the result here *)
  • src/Clight/test/search.ma

    r726 r731  
    1 include "Clight/Animation.ma".
     1include "Clight/Cexec.ma".
     2include "common/Animation.ma".
    23
    34definition myprog := mk_program clight_fundef type
     
    188189.
    189190
    190 example exec: result ? (exec_up_to myprog 1000 [EVint (repr 0)]).
     191example exec: result ? (exec_up_to clight_fullexec myprog 1000 [EVint (repr 0)]).
    191192normalize  (* you can examine the result here *)
    192193%
Note: See TracChangeset for help on using the changeset viewer.