Permalink
Browse files

Succ -> Okay (rename).

  • Loading branch information...
1 parent 510727c commit 38b7f789c41acbe685ecea7dd1d3a093bccb3189 @ziman committed Mar 18, 2012
Showing with 3 additions and 3 deletions.
  1. +3 −3 Execution.agda
View
@@ -28,11 +28,11 @@ unwindShape (Val _ ∷ xs) n = unwindShape xs n
unwindShape [] _ = []
data Resume (s : Shape) : Maybe U → Set where
- Succ : {u} Code s (Val u ∷ s) Stack s Resume s (just u)
+ Okay : {u} Code s (Val u ∷ s) Stack s Resume s (just u)
Fail : Resume s nothing
unwindStack : {s} Stack s (n : ℕ) Resume (unwindShape s n) (unwindHnd s n)
-unwindStack (h !! xs) zero = Succ h xs
+unwindStack (h !! xs) zero = Okay h xs
unwindStack (_ !! xs) (suc n) = unwindStack xs n
unwindStack (_ :: xs) n = unwindStack xs n
unwindStack snil _ = Fail
@@ -57,7 +57,7 @@ mutual
-- Non-trivial exception processing
execInstr (MARK _) ![ n , r ] = ![ suc n , r ]
execInstr UNMARK ![ suc n , r ] = ![ n , r ]
- execInstr UNMARK ![ zero , Succ h st ] = execCode h ✓[ st ]
+ execInstr UNMARK ![ zero , Okay h st ] = execCode h ✓[ st ]
-- Trivial exception processing: instruction skipping
execInstr THROW ![ n , r ] = ![ n , r ]

0 comments on commit 38b7f78

Please sign in to comment.