- Timestamp:
- Sep 15, 2011, 2:27:50 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/joint/semantics.ma
r1213 r1214 156 156 let sp ≝ sub sp (val_of_memory_chunk chunk) in 157 157 let st ≝ set_sp … (address_of_val sp) st in 158 (*CSC: no monadic notation here *)159 bind ?? (opt_to_res ? (msg FailedStore) (loadv chunk (m … st) sp))160 (λv. bind ?? (Byte_of_val v) (λv. OK ? 〈st,v〉)).*)158 do v ← opt_to_res ? (msg FailedStore) (loadv chunk (m … st) sp); 159 do v ← Byte_of_val v; 160 OK ? 〈st,v〉).*) 161 161 162 162 definition save_ra : ∀p. state p → label → res (state p) ≝ 163 163 λp,st,l. 164 164 let 〈addrl,addrh〉 ≝ address_of_label … (m … st) l in 165 (* No monadic notation here *)166 bind ?? (push … st addrl) (λst.push … st addrh).165 do st ← push … st addrl; 166 push … st addrh. 167 167 168 168 definition fetch_ra : ∀p.state p → res (state p × address) ≝ 169 169 λp,st. 170 (* No monadic notation here *) 171 bind ?? (pop … st) (λres. let 〈st,addrh〉 ≝ res in 172 bind ?? (pop … st) (λres. let 〈st,addrl〉 ≝ res in 173 OK ? 〈st, 〈addrl,addrh〉〉)). 170 do 〈st,addrh〉 ← pop … st; 171 do 〈st,addrl〉 ← pop … st; 172 OK ? 〈st, 〈addrl,addrh〉〉. 174 173 175 174 axiom MissingSymbol : String. … … 289 288 qed. 290 289 291 definition is_final: ∀globals:list ident. ∀p: sem_params2 globals. address → nat → state p → option ((*CSC: why not res*) int) ≝ 292 λglobals: list ident. 293 λp. 294 λexit. 295 λregistersno. 296 λst. 297 (* CSC: monadic notation missing here *) 298 match fetch_statement … st with 299 [ Error _ ⇒ None ? 300 | OK s ⇒ 301 match s with 302 [ joint_st_return ⇒ 303 match fetch_ra … st with 304 [ Error _ ⇒ None ? 305 | OK st_l ⇒ 306 let 〈st,l〉 ≝ st_l in 307 if eq_address l exit then 308 (* CSC: monadic notation missing here *) 309 match fetch_result globals p st registersno with 310 [ Error _ ⇒ None ? 311 | OK val ⇒ 312 match val with 313 [ Vint sz i ⇒ intsize_eq_elim ? sz I32 ? i (λi. Some ? i) (None ?) 314 | _ ⇒ None ?]] 315 else 316 None ? ] 317 | _ ⇒ None ? ]]. 290 definition is_final: ∀globals:list ident. ∀p: sem_params2 globals. address → nat → state p → option int ≝ 291 λglobals,p,exit,registersno,st. res_to_opt … ( 292 do s ← fetch_statement … st; 293 match s with 294 [ joint_st_return ⇒ 295 do 〈st,l〉 ← fetch_ra … st; 296 if eq_address l exit then 297 do val ← fetch_result globals p st registersno; 298 match val with 299 [ Vint sz i ⇒ intsize_eq_elim ? sz I32 ? i (λi. OK ? i) (Error ? []) 300 | _ ⇒ Error ? []] 301 else 302 Error ? [] 303 | _ ⇒ Error ? []]). 318 304 319 305 definition joint_exec: ∀globals:list ident. sem_params2 globals → address → nat → execstep io_out io_in ≝
Note: See TracChangeset
for help on using the changeset viewer.