Changeset 731


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

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

Location:
src
Files:
3 added
9 edited
1 moved

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%
  • src/RTLabs/RTLabs-sem.ma

    r727 r731  
    55include "RTLabs/RTLabs-syntax.ma".
    66
    7 include "common/Values.ma".
    87include "common/Errors.ma".
    9 include "common/Events.ma".
    108include "common/Globalenvs.ma".
    11 include "common/IOMonad.ma".
     9include "common/IO.ma".
    1210include "common/SmallstepExec.ma".
    1311
     
    10199].
    102100
    103 (* XXX below is from Cexec, should have common abstraction. *)
    104 
    105 (* Checking types of values given to / received from an external function call. *)
    106 
    107 definition eventval_type : ∀ty:typ. Type[0] ≝
    108 λty. match ty with [ ASTint ⇒ int | ASTptr _ ⇒ False | ASTfloat ⇒ float ].
    109 
    110 definition mk_eventval: ∀ty:typ. eventval_type ty → eventval ≝
    111 λty:typ. match ty return λty'.eventval_type ty' → eventval with [ ASTint ⇒ λv.EVint v | ASTptr r ⇒ ? | ASTfloat ⇒ λv.EVfloat v ].
    112 *; qed.
    113 
    114 definition mk_val: ∀ty:typ. eventval_type ty → val ≝
    115 λty:typ. match ty return λty'.eventval_type ty' → val with [ ASTint ⇒ λv.Vint v | ASTptr r ⇒ ? | ASTfloat ⇒ λv.Vfloat v ].
    116 *; qed.
    117 
    118 lemma mk_val_correct: ∀ty:typ. ∀v:eventval_type ty.
    119   eventval_match (mk_eventval ty v) ty (mk_val ty v).
    120 #ty cases ty; normalize; //; * *; qed.
    121 
    122 definition convert_eventval : ∀ev:eventval. ∀ty:typ. res val ≝
    123 λev,ty.
    124 match ty with
    125 [ ASTint ⇒ match ev with [ EVint i ⇒ OK ? (Vint i) | _ ⇒ Error ? ]
    126 | ASTfloat ⇒ match ev with [ EVfloat f ⇒ OK ? (Vfloat f) | _ ⇒ Error ? ]
    127 | _ ⇒ Error ?
    128 ].
    129 
    130 definition check_eventval' : ∀v:val. ∀ty:typ. res eventval ≝
    131 λv,ty.
    132 match ty with
    133 [ ASTint ⇒ match v with [ Vint i ⇒ OK ? (EVint i) | _ ⇒ Error ? ]
    134 | ASTfloat ⇒ match v with [ Vfloat f ⇒ OK ? (EVfloat f) | _ ⇒ Error ? ]
    135 | _ ⇒ Error ?
    136 ].
    137 
    138 let rec check_eventval_list (vs: list val) (tys: list typ) : res (list eventval) ≝
    139 match vs with
    140 [ nil ⇒ match tys with [ nil ⇒ OK ? (nil ?) | _ ⇒ Error ? ]
    141 | cons v vt ⇒
    142   match tys with
    143   [ nil ⇒ Error ?
    144   | cons ty tyt ⇒
    145     do ev ← check_eventval' v ty;
    146     do evt ← check_eventval_list vt tyt;
    147     OK ? (ev::evt)
    148   ]
    149 ].
    150 
    151 (* IO monad *)
    152 
    153 (* Interactions are function calls that return a value and do not change
    154    the rest of the Clight program's state. *)
    155 record io_out : Type[0] ≝
    156 { io_function: ident
    157 ; io_args: list eventval
    158 ; io_in_typ: typ
    159 }.
    160 
    161 definition io_in ≝ λo. eventval_type (io_in_typ o).
    162 
    163 definition do_io : ident → list eventval → ∀t:typ. IO io_out io_in (eventval_type t) ≝
    164 λfn,args,t. Interact ??? (mk_io_out fn args t) (λres. Value ??? res).
    165 
    166 definition ret: ∀T. T → (IO io_out io_in T) ≝
    167 λT,x.(Value ?? T x).
    168 
    169 (* XXX above is from Cexec, should make common abstraction. *)
    170101
    171102(* XXX put somewhere sensible *)
     
    289220].
    290221
    291 definition RTLabs_exec : execstep
     222definition RTLabs_exec : execstep io_out io_in
    292223  mk_execstep … ? is_final mem_of_state eval_statement.
    293224
     
    300231  OK ? 〈ge,Callstate f (nil ?) (dp ??? [[ ]]) (nil ?) m〉.
    301232
    302 definition exec_inf : ∀p:RTLabs_program. execution state io_out io_in ≝
    303 λp.
    304   match make_initial_state p with
    305   [ OK gs ⇒ exec_inf_aux RTLabs_exec (\fst gs) (ret ? 〈E0,\snd gs〉)
    306   | _ ⇒ e_wrong ???
    307   ].
     233definition RTLabs_fullexec : fullexec io_out io_in ≝
     234  mk_fullexec … RTLabs_exec ? make_initial_state.
     235
  • src/common/Animation.ma

    r730 r731  
    11
    2 include "Clight/Cexec.ma".
     2include "common/IO.ma".
     3include "common/SmallstepExec.ma".
    34
    45(* Functions to allow programs to be executed up to some number of steps, given
     
    1415].
    1516
    16 let rec up_to_nth_step (n:nat) (input:list eventval) (e:execution state io_out io_in) (t:trace) : res (trace × state) ≝
     17inductive snapshot (state:Type[0]) : Type[0] ≝
     18| running : trace → state → snapshot state
     19| finished : trace → int → mem → snapshot state
     20| input_exhausted : trace → snapshot state.
     21
     22let rec up_to_nth_step (n:nat) (ex:execstep io_out io_in) (input:list eventval) (e:execution (state ?? ex) io_out io_in) (t:trace) : res (snapshot (state ?? ex)) ≝
    1723match n with
    18 [ O ⇒ match e with [ e_step tr s _ ⇒ OK ? 〈t⧺tr, s〉
    19                    | e_stop tr r m ⇒ OK ? 〈t⧺tr, Returnstate (Vint r) Kstop m〉
     24[ O ⇒ match e with [ e_step tr s _ ⇒ OK ? (running ? (t⧺tr) s)
     25                   | e_stop tr r m ⇒ OK ? (finished ? (t⧺tr) r m)
    2026                   | _ ⇒ Error ? ]
    21 | S m ⇒ match e with [ e_step tr s e' ⇒ up_to_nth_step m input e' (t⧺tr)
    22                      | e_stop tr r m ⇒ OK ? 〈t⧺tr, Returnstate (Vint r) Kstop m〉
     27| S m ⇒ match e with [ e_step tr s e' ⇒ up_to_nth_step m ex input e' (t⧺tr)
     28                     | e_stop tr r m ⇒ OK ? (finished ? (t⧺tr) r m)
    2329                     | e_interact o k ⇒
    2430                         match input with
    25                          [ nil ⇒ Error ?
     31                         [ nil ⇒ OK ? (input_exhausted ? t)
    2632                         | cons h tl ⇒ do i ← get_input o h;
    27                                        up_to_nth_step m tl (k i) t
     33                                       up_to_nth_step m ex tl (k i) t
    2834                         ]
    2935                     | e_wrong ⇒ Error ?
     
    3137].
    3238
    33 definition exec_up_to : clight_program → nat → list eventval → res (trace × state) ≝
    34 λp,n,i. up_to_nth_step n i (exec_inf p) E0.
     39definition exec_up_to : ∀fx:fullexec io_out io_in. program ?? fx → nat → list eventval → res (snapshot (state ?? fx)) ≝
     40λfx,p,n,i. up_to_nth_step n fx i (exec_inf ?? fx p) E0.
    3541
    3642(* Provide an easy way to get a term in proof mode for reduction.
     
    4652| witness : ∀a:A. result A a.
    4753
     54definition finishes_with : int → ∀S.res (snapshot S) → Prop ≝
     55λr,S,s. match s with [ OK s' ⇒ match s' with [ finished t r' _ ⇒ r = r' | _ ⇒ False ] | _ ⇒ False ].
     56
    4857(* Hide the representation of memory to make displaying the results easier. *)
    4958
  • src/common/SmallstepExec.ma

    r702 r731  
    66include "common/Mem.ma".
    77
    8 record execstep : Type[1] ≝
     8record execstep (outty:Type[0]) (inty:outty → Type[0]) : Type[1] ≝
    99{ genv  : Type[0]
    1010; state : Type[0]
    11 ; output : Type[0]
    12 ; input : output → Type[0]
    1311; is_final : state → option int
    1412; mem_of_state : state → mem
    15 ; step : genv → state → IO output input (trace×state)
     13; step : genv → state → IO outty inty (trace×state)
    1614}.
    1715
    18 let rec repeat (n:nat) (exec:execstep) (g:genv exec) (s:state exec)
    19  : IO (output exec) (input exec) (trace × (state exec)) ≝
     16let rec repeat (n:nat) (outty:Type[0]) (inty:outty → Type[0]) (exec:execstep outty inty)
     17               (g:genv ?? exec) (s:state ?? exec)
     18 : IO outty inty (trace × (state ?? exec)) ≝
    2019match n with
    2120[ O ⇒ Value ??? 〈E0, s〉
    22 | S n' ⇒ ! 〈t1,s1〉 ← step exec g s;
    23          repeat n' exec g s1
     21| S n' ⇒ ! 〈t1,s1〉 ← step ?? exec g s;
     22         repeat n' ?? exec g s1
    2423].
    2524
     
    3534   state. *)
    3635
    37 let corec exec_inf_aux (exec:execstep) (ge:genv exec)
    38                        (s:IO (output exec) (input exec) (trace×(state exec)))
     36let corec exec_inf_aux (output:Type[0]) (input:output → Type[0])
     37                       (exec:execstep output input) (ge:genv ?? exec)
     38                       (s:IO output input (trace×(state ?? exec)))
    3939                       : execution ??? ≝
    4040match s with
    4141[ Wrong ⇒ e_wrong ???
    4242| Value v ⇒ match v with [ pair t s' ⇒
    43     match is_final exec s' with
    44     [ Some r ⇒ e_stop ??? t r (mem_of_state exec s')
    45     | None ⇒ e_step ??? t s' (exec_inf_aux ? ge (step exec ge s')) ] ]
    46 | Interact out k' ⇒ e_interact ??? out (λv. exec_inf_aux ? ge (k' v))
     43    match is_final ?? exec s' with
     44    [ Some r ⇒ e_stop ??? t r (mem_of_state ?? exec s')
     45    | None ⇒ e_step ??? t s' (exec_inf_aux ??? ge (step ?? exec ge s')) ] ]
     46| Interact out k' ⇒ e_interact ??? out (λv. exec_inf_aux ??? ge (k' v))
    4747].
    4848
    49 lemma execution_cases: ∀ex.∀e:execution (state ex) (output ex) (input ex).
     49lemma execution_cases: ∀o,i,s.∀e:execution s o i.
    5050 e = match e with [ e_stop tr r m ⇒ e_stop ??? tr r m
    5151 | e_step tr s e ⇒ e_step ??? tr s e
    5252 | e_wrong ⇒ e_wrong ??? | e_interact o k ⇒ e_interact ??? o k ].
    53 #ex #e cases e; //; qed.
     53#o #i #s #e cases e; //; qed.
    5454
    55 axiom exec_inf_aux_unfold: ∀exec,ge,s. exec_inf_aux exec ge s =
     55axiom exec_inf_aux_unfold: ∀o,i,exec,ge,s. exec_inf_aux o i exec ge s =
    5656match s with
    5757[ Wrong ⇒ e_wrong ???
    5858| Value v ⇒ match v with [ pair t s' ⇒
    59     match is_final exec s' with
    60     [ Some r ⇒ e_stop ??? t r (mem_of_state exec s')
    61     | None ⇒ e_step ??? t s' (exec_inf_aux ? ge (step exec ge s')) ] ]
    62 | Interact out k' ⇒ e_interact ??? out (λv. exec_inf_aux ? ge (k' v))
     59    match is_final ?? exec s' with
     60    [ Some r ⇒ e_stop ??? t r (mem_of_state ?? exec s')
     61    | None ⇒ e_step ??? t s' (exec_inf_aux ??? ge (step ?? exec ge s')) ] ]
     62| Interact out k' ⇒ e_interact ??? out (λv. exec_inf_aux ??? ge (k' v))
    6363].
    6464(*
     
    7171*)
    7272
    73 record execstep' : Type[1] ≝
    74 { es0 :> execstep
    75 ; initial : state es0 → Prop
     73record fullexec (outty:Type[0]) (inty:outty → Type[0]) : Type[1] ≝
     74{ es1 :> execstep outty inty
     75; program : Type[0]
     76; make_initial_state : program → res (genv ?? es1 × (state ?? es1))
     77}.
     78
     79definition exec_inf : ∀o,i.∀fx:fullexec o i. ∀p:program ?? fx. execution (state ?? fx) o i ≝
     80λo,i,fx,p.
     81  match make_initial_state ?? fx p with
     82  [ OK gs ⇒ exec_inf_aux ?? fx (\fst gs) (Value … 〈E0,\snd gs〉)
     83  | _ ⇒ e_wrong ???
     84  ].
     85
     86
     87record execstep' (outty:Type[0]) (inty:outty → Type[0]) : Type[1] ≝
     88{ es0 :> execstep outty inty
     89; initial : state ?? es0 → Prop
    7690}.
    7791
     
    7993alias symbol "and" (instance 2) = "logical and".
    8094record related_semantics : Type[1] ≝
    81 { sem1 : execstep'
    82 ; sem2 : execstep'
    83 ; ge1 : genv sem1
    84 ; ge2 : genv sem2
    85 ; match_states : state sem1 → state sem2 → Prop
    86 ; match_initial_states : ∀st1. (initial sem1) st1 → ∃st2. (initial sem2) st2 ∧ match_states st1 st2
    87 ; match_final_states : ∀st1,st2,r. match_states st1 st2 → (is_final sem1) st1 = Some ? r → (is_final sem2) st2 = Some ? r
     95{ output : Type[0]
     96; input : output → Type[0]
     97; sem1 : execstep' output input
     98; sem2 : execstep' output input
     99; ge1 : genv ?? sem1
     100; ge2 : genv ?? sem2
     101; match_states : state ?? sem1 → state ?? sem2 → Prop
     102; match_initial_states : ∀st1. (initial ?? sem1) st1 → ∃st2. (initial ?? sem2) st2 ∧ match_states st1 st2
     103; match_final_states : ∀st1,st2,r. match_states st1 st2 → (is_final ?? sem1) st1 = Some ? r → (is_final ?? sem2) st2 = Some ? r
    88104}.
    89105
     
    93109{ sems :> related_semantics
    94110; sim : ∀st1,st2,t,st1'.
    95         P_io' ?? (trace × (state (sem1 sems))) (λr. r = 〈t,st1'〉) (step (sem1 sems) (ge1 sems) st1) →
     111        P_io' ?? (trace × (state ?? (sem1 sems))) (λr. r = 〈t,st1'〉) (step ?? (sem1 sems) (ge1 sems) st1) →
    96112        match_states sems st1 st2 →
    97         ∃st2':(state (sem2 sems)).(∃n:nat.P_io' ?? (trace × (state (sem2 sems))) (λr. r = 〈t,st2'〉) (repeat n (sem2 sems) (ge2 sems) st2)) ∧
     113        ∃st2':(state ?? (sem2 sems)).(∃n:nat.P_io' ?? (trace × (state ?? (sem2 sems))) (λr. r = 〈t,st2'〉) (repeat n ?? (sem2 sems) (ge2 sems) st2)) ∧
    98114          match_states sems st1' st2'
    99115}.
Note: See TracChangeset for help on using the changeset viewer.