fix

Author: jsiek

src/examples/Arith.agda

@@ -41,7 +41,7 @@ sig op-error = []
 open import ScopedTuple using (Tuple; _✖_; zip)
 open import Fold2 Op sig
 
-open import AbstractBindingTree Op sig renaming (ABT to AST)
+open import AbstractBindingTree Op sig renaming (ABT to AST) public
 pattern $ n  = op-num n ⦅ nil ⦆
 pattern # b  = op-bool b ⦅ nil ⦆
 infixl 7  _⊗_

src/examples/ArithTypeSafety.agda

@@ -1,16 +1,20 @@
 open import Data.Bool using (true; false; if_then_else_) renaming (Bool to 𝔹)
 open import Data.List using (List; []; _∷_; length)
 open import Data.Maybe using (Maybe; nothing; just)
+open import Data.Nat
+    using (ℕ; zero; suc; _+_; _*_; _⊔_; _∸_; _≤_; _<_; z≤n; s≤s)
 open import Data.Product
     using (_×_; proj₁; proj₂; Σ-syntax) renaming (_,_ to ⟨_,_⟩ )
 open import Data.Unit.Polymorphic using (⊤; tt)
 open import Data.Vec using (Vec) renaming ([] to []̌; _∷_ to _∷̌_)
-open import examples.Arith
+open import examples.Arith hiding (eval-op; eval; evaluate)
+open import Fold Op sig
 open import FoldPreserve Op sig
 open import Relation.Binary.PropositionalEquality using (_≡_; refl)
 open import Sig
-open import Structures using (lower; lift-lower-id)
-open import Var 
+open import Level using (Level; Lift; lift; lower)
+open import Var
+import Agda.Builtin.Unit
 
 module examples.ArithTypeSafety where
 
@@ -57,12 +61,44 @@ compress-⊢v : ∀{v A B Δ} → (B ∷ Δ) ⊢v v ⦂ A → Δ ⊢v v ⦂ A
 compress-⊢v {.nothing} ⊢v-none = ⊢v-none
 compress-⊢v {.(just _)} (⊢v-just x) = ⊢v-just x
 
+open import Structures
+open WithOpSig Op sig
+open import ScopedTuple using (Tuple; _✖_; zip)
+
+eval-op : (op : Op) → Tuple (sig op) (Bind (Maybe Val) (Maybe Val))
+        → Maybe Val
+eval-op (op-num n) tt = just (v-num n)
+eval-op op-error tt = nothing
+eval-op op-mult ⟨ x , ⟨ y , tt ⟩ ⟩ = do
+   v₁ ← x ; v₂ ← y 
+   num? v₁ (λ n → num? v₂ (λ m → just (v-num (n * m))))
+eval-op op-let ⟨ mv , ⟨ f , tt ⟩ ⟩ = f mv
+   {- skipping check on mv, simpler -}
+eval-op (op-bool b) tt = just (v-bool b)
+eval-op op-if ⟨ cnd , ⟨ thn , ⟨ els , tt ⟩ ⟩ ⟩ = do
+   vᶜ ← cnd
+   bool? vᶜ (λ b → if b then thn else els)
+
+instance
+  MVal-is-Foldable : Foldable (Maybe Val) (Maybe Val)
+  MVal-is-Foldable = record { ret = λ x → x ; fold-op = eval-op }
+
+eval : (Var → Maybe Val) → AST → Maybe Val
+eval = fold
+
+evaluate : AST → Maybe Val
+evaluate M = eval (λ x → nothing) M
+
 instance
   _ : FoldPreservable (Maybe Val) (Maybe Val) (Type)
   _ = record { 𝑉 = 𝑉 ; 𝑃 = 𝑃 ; 𝐴 = 𝐴 ; _⊢v_⦂_ = _⊢v_⦂_ ; _⊢c_⦂_ = _⊢c_⦂_
              ; ret-pres = λ x → x ; shift-⊢v = shift-⊢v
              ; 𝑉-⊢v = λ { refl ⊢v⦂ → ⊢v⦂ } ; prev-𝑉 = λ x → x }
 
+lift-lower-id : ∀{ℓ ℓ′ : Level}{A : Set ℓ}{x : Lift ℓ′ A}
+    → lift (lower x) ≡ x
+lift-lower-id = refl
+
 op-pres : ∀ {op}{Rs}{Δ}{A : Type}{As : Vec Type (length (sig op))}{Bs}
           → sig op ∣ Δ ∣ Bs ⊢ᵣ₊ Rs ⦂ As
           → 𝑃 op As Bs A → Δ ⊢c (eval-op op Rs) ⦂ A
@@ -78,8 +114,8 @@ op-pres {op-let} {A = Tᵣ}{As = T₁ ∷̌ T₂ ∷̌ []̆}
                 (cons-r (bind-r{b}{Δ = Δ}{f = f} Pbody) nil-r))
         ⟨ refl , refl ⟩ =
     compress-⊢v {B = T₁} (⊢ᵣ→⊢c G)
-    where G : Sig.Sig.■ ∣ T₁ ∷ Δ ∣ tt ⊢ᵣ Structures.lift (lower (f c)) ⦂ Tᵣ
-          G rewrite lift-lower-id (f c) = Pbody {c} (shift-⊢v Prhs) tt
+    where G : ■ ∣ T₁ ∷ Δ ∣ lift Agda.Builtin.Unit.tt ⊢ᵣ f c ⦂ Tᵣ
+          G = Pbody (shift-⊢v Prhs) tt
 op-pres {op-bool b} nil-r refl = ⊢v-just ⊢-bool
 op-pres {op-if} (cons-r (ast-r Pc) (cons-r (ast-r Pthn)
                                    (cons-r (ast-r Pels) nil-r)))