-- Demo code from 2nd AFP Agda lecture

module Demo2 where

-- Imports & helper defintions
------------------------------

open import Agda.Builtin.Nat
open import Agda.Builtin.Bool
open import Agda.Builtin.List
open import Agda.Builtin.String
open import Agda.Builtin.Equality

data _∈_ : String → List String → Set where
  here : ∀{s} {xs} → s ∈ (s ∷ xs)
  there : ∀{s x xs} → s ∈ xs → s ∈ (x ∷ xs)

ex4 : "helo" ∈ ("helo" ∷ [])
ex4 = here

-- ex5 : "world" ∈ ("helo" ∷ [])
-- ex5 = {!   !}

ex6 : "helo" ∈ ("world" ∷ "helo" ∷ [])
ex6 = there here

-- Type of well-typed & well-scoped Exp ressions
------------------------------------------------

data TyTag : Set where
  bool : TyTag
  nat : TyTag

data Exp (Γ : List String) : TyTag -> Set where
  add : Exp Γ nat -> Exp Γ nat -> Exp Γ nat
  lit-i : Nat -> Exp Γ nat
  lit-b : Bool -> Exp Γ bool
  if_then_else_
    : {ty : TyTag}
    -> Exp Γ bool
    -> Exp Γ ty
    -> Exp Γ ty
    -> Exp Γ ty
  var : (s : String) → s ∈ Γ -> Exp Γ nat

-- Example Exp s
----------------

ex1 : Exp [] nat
ex1 = add (lit-i 1) (add (lit-i 2) (lit-i 3))

ex3 : Exp ("x" ∷ []) nat
ex3 = add (lit-i 1) (add (lit-i 2) (var "x" here))

-- Evaluator
------------

[[_]] : TyTag -> Set
[[ bool ]] = Bool
[[ nat  ]] = Nat

eval : ∀{ty}{Γ} -> ((s : String) -> s ∈ Γ -> Nat) -> Exp Γ ty -> [[ ty ]]
eval env (add e1 e2) = eval env e1 + eval env e2
eval env (lit-i x) = x
eval env (lit-b x) = x
eval env (if c then t else e) with eval env c
eval env (if c then t else e) | false = eval env e
eval env (if c then t else e) | true  = eval env t
eval env (var s s∈Γ) = env s s∈Γ

-- Automated test
-----------------

env1 : (s : String) → s ∈ ("x" ∷ "y" ∷ "z" ∷ []) → Nat
env1 s here                 = 4
env1 s (there here)         = 2
env1 s (there (there here)) = 1

test2 : eval env1 (add (lit-i 1) (lit-i 2))
      ≡ eval env1 (add (lit-i 3) (lit-i 0))
test2 = refl