Ignore:
Timestamp:
Jun 6, 2011, 1:27:59 PM (9 years ago)
Author:
campbell
Message:

Put types into parameter and variable lists in Cminor.
Temporarily breaks translation to RTLabs.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Cminor/semantics.ma

    r881 r886  
    131131axiom WrongNumberOfParameters : String.
    132132
    133 let rec bind_params (vs:list val) (ids:list ident) : res env ≝
     133(* TODO: perhaps should do a little type checking? *)
     134let rec bind_params (vs:list val) (ids:list (ident×typ)) : res env ≝
    134135match vs with
    135136[ nil ⇒ match ids with [ nil ⇒ OK ? (empty_map ??) | _ ⇒ Error ? (msg WrongNumberOfParameters) ]
     
    137138    match ids with
    138139    [ nil ⇒ Error ? (msg WrongNumberOfParameters)
    139     | cons id idt ⇒
     140    | cons idh idt ⇒
     141        let 〈id,ty〉 ≝ idh in
    140142        do en ← bind_params vt idt;
    141143        OK ? (add ?? en id v)
     
    143145].
    144146
    145 definition init_locals : env → list ident → env ≝
    146 foldr ?? (λid,en. add ?? en id Vundef).
     147(* TODO: perhaps should do a little type checking? *)
     148definition init_locals : env → list (ident×typ) → env ≝
     149foldr ?? (λidty,en. add ?? en (\fst idty) Vundef).
    147150
    148151axiom FailedStore : String.
Note: See TracChangeset for help on using the changeset viewer.