- Timestamp:
- Oct 7, 2011, 3:32:07 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/joint/semantics.ma
r1312 r1324 81 81 ; set_result: list val → state (mk_sem_params … more_sparams1) → res (state (mk_sem_params … more_sparams1)) 82 82 83 ; exec_extended: genv globals p → extend_statements (mk_sem_params … more_sparams1) → s tate (mk_sem_params … more_sparams1) → IO io_out io_in (trace × (state (mk_sem_params … more_sparams1)))83 ; exec_extended: genv globals p → extend_statements (mk_sem_params … more_sparams1) → succ p → state (mk_sem_params … more_sparams1) → IO io_out io_in (trace × (state (mk_sem_params … more_sparams1))) 84 84 }. 85 85 … … 220 220 | sequential seq l ⇒ 221 221 match seq with 222 [ extension c ⇒ exec_extended … p ge c st222 [ extension c ⇒ exec_extended … p ge c l st 223 223 | COST_LABEL cl ⇒ ret ? 〈Echarge cl, next … l st〉 224 224 | COMMENT c ⇒ ret ? 〈E0, next … l st〉
Note: See TracChangeset
for help on using the changeset viewer.