Changeset 886 for src/Cminor


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.

Location:
src/Cminor
Files:
2 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.
  • src/Cminor/syntax.ma

    r881 r886  
    3434
    3535record internal_function : Type[0] ≝
    36 { f_sig       : signature
    37 ; f_params    : list ident
    38 ; f_vars      : list ident
    39 ; f_ptrs      : list ident
     36{ f_return    : option typ
     37; f_params    : list (ident × typ)
     38; f_vars      : list (ident × typ)
    4039; f_stacksize : nat
    4140; f_body      : stmt
Note: See TracChangeset for help on using the changeset viewer.