Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
Browse files

Some cleanup.

  • Loading branch information...
commit a592cc353aa44c6684377f975e95fcfed5a270b2 1 parent 604f4c1
@ziman authored
Showing with 51 additions and 43 deletions.
  1. +17 −14 Correctness.agda
  2. +34 −29 Execution.agda
View
31 Correctness.agda
@@ -14,21 +14,24 @@ open import Code
open import Compiler
open import Execution
--- Smart stack pusher
-infixr 5 _:::_
-_:::_ : {u s} Maybe (el u) State s State (Val u ∷ s)
-_:::_ nothing ![ n , st ] = ![ n , st ]
-_:::_ (just x) ![ n , st ] = ![ n , st ]
-_:::_ nothing ×[ u , n , st ] = ×[ u , n , st ]
-_:::_ (just x) ×[ u , n , st ] = ×[ u , n , st ]
-_:::_ nothing ✓[ st ] = ![ zero , unwindStack st zero ]
-_:::_ (just x) ✓[ st ] = ✓[ x :: st ]
+module Utils where
+ -- Smart stack pusher
+ infixr 5 _:::_
+ _:::_ : {u s} Maybe (el u) State s State (Val u ∷ s)
+ _:::_ nothing ![ n , st ] = ![ n , st ]
+ _:::_ (just x) ![ n , st ] = ![ n , st ]
+ _:::_ nothing ×[ u , n , st ] = ×[ u , n , st ]
+ _:::_ (just x) ×[ u , n , st ] = ×[ u , n , st ]
+ _:::_ nothing ✓[ st ] = ![ zero , unwindStack st zero ]
+ _:::_ (just x) ✓[ st ] = ✓[ x :: st ]
--- Execution distributes over ◅◅
-distr : {s t u} (st : State s) (c : Code s t) (d : Code t u)
- execCode (c ◅◅ d) st ≡ execCode d (execCode c st)
-distr st ε d = refl
-distr st (i ◅ is) d rewrite distr (execInstr i st) is d = refl
+ -- Execution distributes over ◅◅
+ distr : {s t u} (st : State s) (c : Code s t) (d : Code t u)
+ execCode (c ◅◅ d) st ≡ execCode d (execCode c st)
+ distr st ε d = refl
+ distr st (i ◅ is) d rewrite distr (execInstr i st) is d = refl
+
+open Utils
-- Central case analysis for binary operators
lemma-op : {s t u v} (r : Exp t) (l : Exp u) (op : Op u t v) (st : State s)
View
63 Execution.agda
@@ -15,39 +15,43 @@ open import Expression
open import Denotation
open import Code
--- Unwind the shape up to just below the n-th handle-mark from the top.
-unwindShape : Shape Shape
-unwindShape (Han _ ∷ xs) zero = xs
-unwindShape (Han _ ∷ xs) (suc n) = unwindShape xs n
-unwindShape (Skp _ ∷ xs) n = unwindShape xs n
-unwindShape (Val _ ∷ xs) n = unwindShape xs n
-unwindShape [] _ = []
+module MachineState where
+ -- Unwind the shape up to just below the n-th handle-mark from the top.
+ unwindShape : Shape Shape
+ unwindShape (Han _ ∷ xs) zero = xs
+ unwindShape (Han _ ∷ xs) (suc n) = unwindShape xs n
+ unwindShape (Skp _ ∷ xs) n = unwindShape xs n
+ unwindShape (Val _ ∷ xs) n = unwindShape xs n
+ unwindShape [] _ = []
--- Unwind the stack up to just below the n-th handle-mark from the top.
-unwindStack : {s} Stack s (n : ℕ) Stack (unwindShape s n)
-unwindStack (han _ :: xs) zero = xs
-unwindStack (han _ :: xs) (suc n) = unwindStack xs n
-unwindStack (skp _ :: xs) n = unwindStack xs n
-unwindStack ( _ :: xs) n = unwindStack xs n
-unwindStack snil _ = snil
+ -- Shape of the stack after skipping the n-th skip-mark from the top.
+ skipShape : Shape Shape
+ skipShape (Han _ xs) n = skipShape xs n
+ skipShape (Skp u ∷ xs) zero = Val u ∷ xs
+ skipShape (Skp _ xs) (suc n) = skipShape xs n
+ skipShape (Val _ ∷ xs) n = skipShape xs n
+ skipShape [] _ = []
--- Shape of the stack after skipping the n-th handler from the top.
-skipShape : Shape Shape
-skipShape (Han _ xs) n = skipShape xs n
-skipShape (Skp u ∷ xs) zero = Val u ∷ xs
-skipShape (Skp _ xs) (suc n) = skipShape xs n
-skipShape (Val _ ∷ xs) n = skipShape xs n
-skipShape [] _ = []
+ -- Unwind the stack up to just below the n-th handle-mark from the top.
+ unwindStack : {s} Stack s (n : ℕ) Stack (unwindShape s n)
+ unwindStack (han _ :: xs) zero = xs
+ unwindStack (han _ :: xs) (suc n) = unwindStack xs n
+ unwindStack (skp _ :: xs) n = unwindStack xs n
+ unwindStack ( _ :: xs) n = unwindStack xs n
+ unwindStack snil _ = snil
--- Execution state of the virtual machine.
-data State (s : Shape) : Set where
- -- Normal operation
- ✓[_] : (st : Stack s) State s
- -- Exceptional state
- ![_,_] : (n : ℕ) (st : Stack (unwindShape s n)) State s
- -- Handler skipping (forward jump)
- ×[_,_,_] : (u : U) (n : ℕ) (st : Stack (skipShape s n)) State s
+ -- Execution state of the virtual machine.
+ data State (s : Shape) : Set where
+ -- Normal operation
+ ✓[_] : (st : Stack s) State s
+ -- Exceptional state
+ ![_,_] : (n : ℕ) (st : Stack (unwindShape s n)) State s
+ -- Handler skipping (forward jump)
+ ×[_,_,_] : (u : U) (n : ℕ) (st : Stack (skipShape s n)) State s
+open MachineState
+
+-- Instruction execution
execInstr : {s t} Instr s t State s State t
-- Normal operation
@@ -80,6 +84,7 @@ execInstr HANDLE ![ zero , st ] = ✓[ st ]
-- Exception handling: no exception, skip the handler, keeping the current stack
execInstr HANDLE ✓[ x :: han u :: skp .u :: st ] = ×[ u , zero , x :: st ]
+-- Execution of code is nothing more than a left fold
execCode : {s t} Code s t State s State t
execCode ε st = st
execCode (i ◅ is) st = execCode is (execInstr i st)
Please sign in to comment.
Something went wrong with that request. Please try again.