update a couple of playground files

playground/samples/Combinatory.newt

@@ -1,6 +1,7 @@
 module Combinatory
 
 -- "A correct-by-construction conversion from lambda calculus to combinatory logic", Wouter Swierstra
+-- prj/menagerie/papers/combinatory
 
 data Unit : U where
   MkUnit : Unit
@@ -10,8 +11,6 @@ data List : U -> U where
   Nil : {A : U} -> List A
   _::_ : {A : U} -> A -> List A -> List A
 
--- prj/menagerie/papers/combinatory
-
 infixr 6 _~>_
 data Type : U where
   ι : Type
@@ -41,23 +40,17 @@ data Env : Ctx -> U where
   ENil : Env Nil
   _:::_ : {Γ : Ctx} {σ : Type} → Val σ → Env Γ → Env (σ :: Γ)
 
--- TODO there is a problem here with coverage checking
--- I suspect something is being split before it's ready
+lookup : {σ : Type} {Γ : Ctx} → Ref σ Γ → Env Γ → Val σ
+lookup Here (x ::: y) = x
+lookup () ENil
+lookup (There i) (x ::: env) = lookup i env
 
--- lookup : {σ : Type} {Γ : Ctx} → Ref σ Γ → Env Γ → Val σ
--- lookup Here (x ::: y) = x
--- lookup (There i) (x ::: env) = lookup i env
-
-lookup2 : {σ : Type} {Γ : Ctx} → Env Γ → Ref σ Γ → Val σ
-lookup2 (x ::: y) Here = x
-lookup2 (x ::: env) (There i) = lookup2 env i
-
--- TODO MixFix - this was ⟦_⟧
-eval : {Γ : Ctx} {σ : Type} → Term Γ σ → (Env Γ → Val σ)
+infixl 1 ⟦_⟧
+⟦_⟧ : {Γ : Ctx} {σ : Type} → Term Γ σ → (Env Γ → Val σ)
 -- there was a unification error in direct application
-eval (App t u) env = (eval t env) (eval u env)
-eval (Lam t) env = \ x => eval t (x ::: env)
-eval (Var i) env = lookup2 env i
+⟦ App t u ⟧ env = (⟦ t ⟧ env) (⟦ u ⟧ env)
+⟦ Lam t ⟧ env = \ x => ⟦ t ⟧ (x ::: env)
+⟦ Var i ⟧ env = lookup i env
 
 data Comb : (Γ : Ctx) → (u : Type) → (Env Γ → Val u) → U where
   S : {Γ : Ctx} {σ τ τ' : Type} → Comb Γ ((σ ~> τ ~> τ') ~> (σ ~> τ) ~> (σ ~> τ')) (\ env => \ f g x => (f x) (g x))
@@ -65,7 +58,7 @@ data Comb : (Γ : Ctx) → (u : Type) → (Env Γ → Val u) → U where
   I : {Γ : Ctx} {σ : Type} → Comb Γ (σ ~> σ) (\ env => \ x => x)
   B : {Γ : Ctx} {σ τ τ' : Type} → Comb Γ ((τ ~> τ') ~> (σ ~> τ) ~> (σ ~> τ')) (\ env => \ f g x => f (g x))
   C : {Γ : Ctx} {σ τ τ' : Type} → Comb Γ ((σ ~> τ ~> τ') ~> τ ~> (σ ~> τ')) (\ env => \ f g x => (f x) g)
-  CVar : {Γ : Ctx} {σ : Type} → (i : Ref σ Γ) → Comb Γ σ (\ env => lookup2 env i)
+  CVar : {Γ : Ctx} {σ : Type} → (i : Ref σ Γ) → Comb Γ σ (\ env => lookup i env)
   CApp : {Γ : Ctx} {σ τ : Type} {f : _} {x : _} → Comb Γ (σ ~> τ) f → Comb Γ σ x → Comb Γ τ (\ env => (f env) (x env))
 
 sapp : {Γ : Ctx} {σ τ ρ : Type} {f : _} {x : _} →
@@ -86,11 +79,12 @@ abs I = CApp K I
 abs B = CApp K B
 abs C = CApp K C
 abs (CApp t u) = sapp (abs t) (abs u)
--- lookup2 was getting stuck, needed to re-eval the types in the rewritten env.
+-- lookup was getting stuck, needed to re-eval the types in the rewritten env.
 abs (CVar Here) = I
 abs (CVar (There i)) = CApp K (CVar i)
 
-translate : {Γ : Ctx} {σ : Type} → (tm : Term Γ σ) → Comb Γ σ (eval tm)
+-- Was a bug in pratt parser when argument `⟦ tm ⟧` had a prefix operator
+translate : {Γ : Ctx} {σ : Type} → (tm : Term Γ σ) → Comb Γ σ ⟦ tm ⟧
 translate (App t u) = CApp (translate t) (translate u)
 translate (Lam t) = abs (translate t)
 translate (Var i) = CVar i

playground/samples/DSL.newt

@@ -1,24 +1,25 @@
 module DSL
 
+-- "A DSL for finite types and enumeration"
 -- https://www.youtube.com/watch?v=sFyy9sssK50
 
-data ℕ : U where
-  Z : ℕ
-  S : ℕ → ℕ
+data Nat : U where
+  Z : Nat
+  S : Nat → Nat
 
 infixl 7 _+_
 infixl 8 _*_
 
-_+_ : ℕ → ℕ → ℕ
+_+_ : Nat → Nat → Nat
 Z + m = m
 (S k) + m = S (k + m)
 
-_*_ : ℕ → ℕ → ℕ
+_*_ : Nat → Nat → Nat
 Z * m = Z
 (S k) * m = m + k * m
 
 infixr 4 _::_
-data Vec : U → ℕ → U where
+data Vec : U → Nat → U where
   Nil : {a} → Vec a Z
   _::_ : {a k} → a → Vec a k → Vec a (S k)
 
@@ -43,7 +44,7 @@ two = Add One One
 four : E
 four = Mul two two
 
-card : E → ℕ
+card : E → Nat
 card Zero = Z
 card One = S Z
 card (Add x y) = card x + card y
@@ -53,7 +54,7 @@ data Empty : U where
 
 data Unit : U where
   -- unit accepted but case building thinks its a var
-  unit : Unit
+  MkUnit : Unit
 
 data Either : U -> U -> U where
   Left : {A B} → A → Either A B
@@ -73,10 +74,10 @@ Bool : U
 Bool = typ two
 
 false : Bool
-false = Left unit
+false = Left MkUnit
 
 true : Bool
-true = Right unit
+true = Right MkUnit
 
 BothBoolBool : U
 BothBoolBool = typ four