Changeset 886 for src/Cminor/semantics.ma

Timestamp:

Jun 6, 2011, 1:27:59 PM (10 years ago)

Author:

campbell

Message:

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

File:

• src/Cminor/semantics.ma (modified) (3 diffs)

src/Cminor/semantics.ma

@@ -131 +131 @@
 axiom WrongNumberOfParameters : String.
 
-let rec bind_params (vs:list val) (ids:list ident) : res env ≝
+(* TODO: perhaps should do a little type checking? *)
+let rec bind_params (vs:list val) (ids:list (ident×typ)) : res env ≝
 match vs with
 [ nil ⇒ match ids with [ nil ⇒ OK ? (empty_map ??) | _ ⇒ Error ? (msg WrongNumberOfParameters) ]
@@ -137 +138 @@
     match ids with
     [ nil ⇒ Error ? (msg WrongNumberOfParameters)
-    | cons id idt ⇒
+    | cons idh idt ⇒
+        let 〈id,ty〉 ≝ idh in
         do en ← bind_params vt idt;
         OK ? (add ?? en id v)
@@ -143 +145 @@
 ].
 
-definition init_locals : env → list ident → env ≝
-foldr ?? (λid,en. add ?? en id Vundef).
+(* TODO: perhaps should do a little type checking? *)
+definition init_locals : env → list (ident×typ) → env ≝
+foldr ?? (λidty,en. add ?? en (\fst idty) Vundef).
 
 axiom FailedStore : String.