Changeset 886 for src/Cminor/semantics.ma
- Timestamp:
- Jun 6, 2011, 1:27:59 PM (10 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/Cminor/semantics.ma
r881 r886 131 131 axiom WrongNumberOfParameters : String. 132 132 133 let rec bind_params (vs:list val) (ids:list ident) : res env ≝ 133 (* TODO: perhaps should do a little type checking? *) 134 let rec bind_params (vs:list val) (ids:list (ident×typ)) : res env ≝ 134 135 match vs with 135 136 [ nil ⇒ match ids with [ nil ⇒ OK ? (empty_map ??) | _ ⇒ Error ? (msg WrongNumberOfParameters) ] … … 137 138 match ids with 138 139 [ nil ⇒ Error ? (msg WrongNumberOfParameters) 139 | cons id idt ⇒ 140 | cons idh idt ⇒ 141 let 〈id,ty〉 ≝ idh in 140 142 do en ← bind_params vt idt; 141 143 OK ? (add ?? en id v) … … 143 145 ]. 144 146 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? *) 148 definition init_locals : env → list (ident×typ) → env ≝ 149 foldr ?? (λidty,en. add ?? en (\fst idty) Vundef). 147 150 148 151 axiom FailedStore : String.
Note: See TracChangeset
for help on using the changeset viewer.