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/SmallstepExec.ma

    r751 r797  
    3737| e_stop : trace → int → mem → execution state output input
    3838| e_step : trace → state → execution state output input → execution state output input
    39 | e_wrong : execution state output input
     39| e_wrong : errmsg → execution state output input
    4040| e_interact : ∀o:output. (input o → execution state output input) → execution state output input.
    4141
     
    4949                       : execution ??? ≝
    5050match s with
    51 [ Wrong ⇒ e_wrong ???
     51[ Wrong m ⇒ e_wrong ??? m
    5252| Value v ⇒ match v with [ pair t s' ⇒
    5353    match is_final ?? exec s' with
     
    6060 e = match e with [ e_stop tr r m ⇒ e_stop ??? tr r m
    6161 | e_step tr s e ⇒ e_step ??? tr s e
    62  | e_wrong ⇒ e_wrong ??? | e_interact o k ⇒ e_interact ??? o k ].
     62 | e_wrong m ⇒ e_wrong ??? m | e_interact o k ⇒ e_interact ??? o k ].
    6363#o #i #s #e cases e; //; qed.
    6464
    6565axiom exec_inf_aux_unfold: ∀o,i,exec,ge,s. exec_inf_aux o i exec ge s =
    6666match s with
    67 [ Wrong ⇒ e_wrong ???
     67[ Wrong m ⇒ e_wrong ??? m
    6868| Value v ⇒ match v with [ pair t s' ⇒
    6969    match is_final ?? exec s' with
     
    9191  match make_initial_state ?? fx p with
    9292  [ OK gs ⇒ exec_inf_aux ?? fx (\fst gs) (Value … 〈E0,\snd gs〉)
    93   | _ ⇒ e_wrong ???
     93  | Error m ⇒ e_wrong ??? m
    9494  ].
    9595
Note: See TracChangeset for help on using the changeset viewer.