source: src/common/Animation.ma @ 1213

Last change on this file since 1213 was 1213, checked in by sacerdot, 8 years ago

1) New values (joint/BEValues.ma) and memory model for the back-ends

(joint/BEMem.ma) where all values are Byte-valued.

2) Improved joint semantics for the back-end languages based on the new

memory model (work in progress).

3) SmallStepExec? made more general to accomodate states with an arbitrary

memory inside.

4) New files common/Pointers.ma and common/GenMem.ma shared between the

front-end and the back-end. GenMem?.ma, at the moment, is not used in Mem.ma
(cut&paste code).

File size: 4.6 KB
RevLine 
[409]1
[731]2include "common/IO.ma".
3include "common/SmallstepExec.ma".
[963]4include "arithmetics/nat.ma".
[409]5
6(* Functions to allow programs to be executed up to some number of steps, given
7   a predetermined set of input values.  Note that we throw away the state if
8   we stop at a continuation - it can be too large to work with. *)
9
[487]10definition get_input : ∀o:io_out. eventval → res (io_in o) ≝
[409]11λo,ev.
12match io_in_typ o return λt. res (eventval_type t) with
[961]13[ ASTint sz _ ⇒ match ev with [ EVint sz' i ⇒ intsize_eq_elim ? sz' sz ? i (λi.OK ? i) (Error ? (msg IllTypedEvent)) | _ ⇒ Error ? (msg IllTypedEvent) ]
[879]14| ASTfloat _ ⇒ match ev with [ EVfloat f ⇒ OK ? f | _ ⇒ Error ? (msg IllTypedEvent) ]
[797]15| ASTptr _ ⇒ Error ? (msg IllTypedEvent)
[409]16].
17
[731]18inductive snapshot (state:Type[0]) : Type[0] ≝
19| running : trace → state → snapshot state
[1213]20| finished : trace → int → state → snapshot state
[731]21| input_exhausted : trace → snapshot state.
22
[797]23axiom StoppedMidIO : String.
24
[731]25let 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)) ≝
[409]26match n with
[731]27[ O ⇒ match e with [ e_step tr s _ ⇒ OK ? (running ? (t⧺tr) s)
28                   | e_stop tr r m ⇒ OK ? (finished ? (t⧺tr) r m)
[797]29                   | e_interact o k ⇒ Error ? (msg StoppedMidIO)
30                   | e_wrong m ⇒ Error ? m ]
[731]31| S m ⇒ match e with [ e_step tr s e' ⇒ up_to_nth_step m ex input e' (t⧺tr)
32                     | e_stop tr r m ⇒ OK ? (finished ? (t⧺tr) r m)
[409]33                     | e_interact o k ⇒
34                         match input with
[731]35                         [ nil ⇒ OK ? (input_exhausted ? t)
[409]36                         | cons h tl ⇒ do i ← get_input o h;
[731]37                                       up_to_nth_step m ex tl (k i) t
[409]38                         ]
[797]39                     | e_wrong m ⇒ Error ? m
[409]40                     ]
41].
42
[731]43definition exec_up_to : ∀fx:fullexec io_out io_in. program ?? fx → nat → list eventval → res (snapshot (state ?? fx)) ≝
44λfx,p,n,i. up_to_nth_step n fx i (exec_inf ?? fx p) E0.
[409]45
[963]46(* A version of exec_up_to that reports the state prior to failure. *)
47
48inductive snapshot' (state:Type[0]) : Type[0] ≝
49| running' : trace → state → snapshot' state
[1213]50| finished' : nat → trace → int → state → snapshot' state
[963]51| input_exhausted' : trace → snapshot' state
52| failed' : errmsg → nat → state → snapshot' state
53| init_state_fail' : errmsg → snapshot' state.
54
55let rec up_to_nth_step' (n:nat) (total:nat) (ex:execstep io_out io_in) (input:list eventval) (e:execution (state ?? ex) io_out io_in) (prev:state ?? ex) (t:trace) : snapshot' (state ?? ex) ≝
56match n with
57[ O ⇒ match e with [ e_step tr s _ ⇒ running' ? (t⧺tr) s
58                   | e_stop tr r m ⇒ finished' ? total (t⧺tr) r m
59                   | e_interact o k ⇒ failed' ? (msg StoppedMidIO) total prev
60                   | e_wrong m ⇒ failed' ? m total prev ]
61| S m ⇒ match e with [ e_step tr s e' ⇒ up_to_nth_step' m total ex input e' s (t⧺tr)
62                     | e_stop tr r m ⇒ finished' ? (minus total n) (t⧺tr) r m
63                     | e_interact o k ⇒
64                         match input with
65                         [ nil ⇒ input_exhausted' ? t
66                         | cons h tl ⇒ match get_input o h with
67                                       [ OK i ⇒ up_to_nth_step' m total ex tl (k i) prev t
68                                       | Error m ⇒ failed' ? m (minus total n) prev
69                                       ]
70                         ]
71                     | e_wrong m ⇒ failed' ? m (minus total n) prev
72                     ]
73].
74
75definition exec_up_to' : ∀fx:fullexec io_out io_in. program ?? fx → nat → list eventval → snapshot' (state ?? fx) ≝
76λfx,p,n,i.
77match make_initial_state ?? fx p with
78[ OK gs ⇒ up_to_nth_step' n n fx i (exec_inf_aux ?? fx (\fst gs) (Value … 〈E0,\snd gs〉)) (\snd gs) E0
79| Error m ⇒ init_state_fail' ? m
80].
81
[409]82(* Provide an easy way to get a term in proof mode for reduction.
83   For example,
84   
[487]85   example exec: result ? (exec_up_to myprog 20 [EVint (repr 12)]).
86   normalize  (* you can examine the result here *)
87   % qed.
[409]88   
89 *)
90
[487]91inductive result (A:Type[0]) : A → Type[0] ≝
[409]92| witness : ∀a:A. result A a.
93
[731]94definition finishes_with : int → ∀S.res (snapshot S) → Prop ≝
95λr,S,s. match s with [ OK s' ⇒ match s' with [ finished t r' _ ⇒ r = r' | _ ⇒ False ] | _ ⇒ False ].
96
[1213]97include "common/Mem.ma".
98
[409]99(* Hide the representation of memory to make displaying the results easier. *)
100
101notation < "'MEM'" with precedence 1 for @{ 'mem }.
102interpretation "hide memory" 'mem = (mk_mem ???).
Note: See TracBrowser for help on using the repository browser.