Ignore:
Timestamp:
Apr 20, 2011, 5:39:00 PM (9 years ago)
Author:
campbell
Message:

Remove superfluous register in RTLabs return statements.

Also fix up RTLabs prototype pretty printer's handling of global variables.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/semantics.ma

    r762 r765  
    3737   state
    3838| Returnstate :
    39    ∀ rtv : val.
     39   ∀ rtv : option val.
    4040   ∀ dst : option register.
    4141   ∀ stk : list frame.
     
    177177      ]
    178178
    179   | St_return src ⇒
    180       ! v ← reg_retrieve (locals f) src;
     179  | St_return ⇒
     180      ! v ← match f_result (func f) with
     181            [ None ⇒ ret ? (None ?)
     182            | Some r ⇒ ! v ← reg_retrieve (locals f) r; ret ? (Some ? v)
     183            ];
    181184      ret ? 〈E0, Returnstate v (retdst f) fs (free m (sp f))〉
    182185  ]
     
    190193        ! evargs ← check_eventval_list params (sig_args (ef_sig fn));
    191194        ! evres ← do_io (ef_id fn) evargs (match (sig_res (ef_sig fn)) with [ None ⇒ ASTint | Some t ⇒ t ]);  (* XXX hack, should allow none *)
    192         ret ? 〈Eextcall (ef_id fn) evargs (mk_eventval ? evres), Returnstate (mk_val ? evres) dst fs m〉
    193 
     195        ret ? 〈Eextcall (ef_id fn) evargs (mk_eventval ? evres), Returnstate (Some ? (mk_val ? evres) (*FIXME should allow None *)) dst fs m〉
    194196    ]
    195197| Returnstate v dst fs m ⇒
     
    197199    [ nil ⇒ Error ? (* Already in final state *)
    198200    | cons f fs' ⇒
    199         ! locals ← match dst with [ None ⇒ OK ? (locals f)
    200                                   | Some d ⇒ reg_store d v (locals f) ];
     201        ! locals ← match dst with
     202                   [ None ⇒ match v with [ None ⇒ OK ? (locals f)
     203                                         | _ ⇒ Error ? ]
     204                   | Some d ⇒ match v with [ None ⇒ Error ?
     205                                           | Some v' ⇒ reg_store d v' (locals f) ] ];
    201206        ret ? 〈E0, State (mk_frame (func f) locals (next f) (sp f) (retdst f)) fs' m〉
    202207    ]
     
    208213| Callstate _ _ _ _ _ ⇒ None ?
    209214| Returnstate v _ fs _ ⇒
    210     match fs with [ nil ⇒ match v with [ Vint i ⇒ Some ? i | _ ⇒ None ? ] | cons _ _ ⇒ None ? ]
     215    match fs with [ nil ⇒ match v with [ Some v' ⇒ match v' with [ Vint i ⇒ Some ? i | _ ⇒ None ? ] | None ⇒ None ? ] | cons _ _ ⇒ None ? ]
    211216].
    212217
Note: See TracChangeset for help on using the changeset viewer.