Ignore:
Timestamp:
May 13, 2011, 1:10:23 PM (9 years ago)
Author:
campbell
Message:

Add error messages wherever the error monad is used.
Sticks to CompCert? style strings+identifiers for the moment.
Use axioms for strings as we currently have no representation or literals
for them - still *very* useful for animation in the proof assistant.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/Animation.ma

    r731 r797  
    1010λo,ev.
    1111match io_in_typ o return λt. res (eventval_type t) with
    12 [ ASTint ⇒ match ev with [ EVint i ⇒ OK ? i | _ ⇒ Error ? ]
    13 | ASTfloat ⇒ match ev with [ EVfloat f ⇒ OK ? f | _ ⇒ Error ? ]
    14 | ASTptr _ ⇒ Error ?
     12[ ASTint ⇒ match ev with [ EVint i ⇒ OK ? i | _ ⇒ Error ? (msg IllTypedEvent) ]
     13| ASTfloat ⇒ match ev with [ EVfloat f ⇒ OK ? f | _ ⇒ Error ? (msg IllTypedEvent) ]
     14| ASTptr _ ⇒ Error ? (msg IllTypedEvent)
    1515].
    1616
     
    2020| input_exhausted : trace → snapshot state.
    2121
     22axiom StoppedMidIO : String.
     23
    2224let 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)) ≝
    2325match n with
    2426[ O ⇒ match e with [ e_step tr s _ ⇒ OK ? (running ? (t⧺tr) s)
    2527                   | e_stop tr r m ⇒ OK ? (finished ? (t⧺tr) r m)
    26                    | _ ⇒ Error ? ]
     28                   | e_interact o k ⇒ Error ? (msg StoppedMidIO)
     29                   | e_wrong m ⇒ Error ? m ]
    2730| S m ⇒ match e with [ e_step tr s e' ⇒ up_to_nth_step m ex input e' (t⧺tr)
    2831                     | e_stop tr r m ⇒ OK ? (finished ? (t⧺tr) r m)
     
    3336                                       up_to_nth_step m ex tl (k i) t
    3437                         ]
    35                      | e_wrong ⇒ Error ?
     38                     | e_wrong m ⇒ Error ? m
    3639                     ]
    3740].
Note: See TracChangeset for help on using the changeset viewer.