Changeset 797 for src/RTLabs/debug.ma


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/RTLabs/debug.ma

    r775 r797  
    77| Ret : ministate
    88| NoInput : ministate
    9 | Fail : ministate
     9| Fail : errmsg → ministate
    1010| MissingStmt : ministate
    1111| Done : int → ministate
     
    2424[ O ⇒ match e with [ e_step tr s _ ⇒ [mk_ministate s]
    2525                   | e_stop tr r m ⇒ [Done r]
    26                    | _ ⇒ [Fail]
     26                   | e_interact o k ⇒ [Fail (msg StoppedMidIO)]
     27                   | e_wrong m ⇒ [Fail m]
    2728                   ]
    2829| S m ⇒ match e with [ e_step tr s e' ⇒ (mk_ministate s)::(debug_up_to_aux m input e')
     
    3334                         | cons h tl ⇒ match get_input o h with
    3435                                       [ OK i ⇒ debug_up_to_aux m tl (k i)
    35                                        | _ ⇒ [Fail]
     36                                       | Error m ⇒ [Fail m]
    3637                                       ]
    3738                         ]
    38                      | e_wrong ⇒ [Fail]
     39                     | e_wrong m ⇒ [Fail m]
    3940                     ]
    4041].
Note: See TracChangeset for help on using the changeset viewer.