add some missing files, clean up a little

TODO.md

@@ -1,6 +1,8 @@
 
 ## TODO
 
+- [ ] `newt/Problem.newt` coverage issues
+- [ ] Maybe make the editor json more compact
 - [ ] Remove erased args from primitive functions
 - [ ] consider moving primitive functions to a support file
   - Downside here is that we lose some dead code elimination, but it better supports bootstrapping when calling convention changes.

newt/Boehm.newt

@@ -0,0 +1,119 @@
+module Boehm
+
+-- https://okmij.org/ftp/tagless-final/course/Boehm-Berarducci.html
+
+import Prelude
+
+data Exp  = Lit Int
+          | Neg Exp
+          | ADD Exp Exp
+
+ti1 : Exp
+ti1 = ADD (Lit 8) (Neg (ADD (Lit 1) (Lit 2)))
+
+view : Exp → String
+view (Lit n) = show n
+view (Neg e) = "(-" ++ view e ++ ")"
+view (ADD e1 e2) = "("++ view e1 ++ " + " ++ view e2 ++ ")"
+
+record ExpOps a where
+  olit : Int → a
+  oneg : a → a
+  oadd : a → a → a
+
+foldExp : ∀ a. (Int → a) → (a → a) → (a → a → a) → Exp → a
+foldExp onlit onneg onadd (Lit n) = onlit n
+foldExp onlit onneg onadd (Neg e) = onneg (foldExp onlit onneg onadd e)
+foldExp onlit onneg onadd (ADD e1 e2) =
+  onadd (foldExp onlit onneg onadd e1)
+        (foldExp onlit onneg onadd e2)
+
+foldExp' : ∀ a. ExpOps a → Exp → a
+foldExp' ops = foldExp ops.olit ops.oneg ops.oadd
+
+viewOps : ExpOps String
+viewOps = MkExpOps show
+                   (\ e => "(-" ++ e ++ ")")
+                   (\ e1 e2 => "(" ++ e1 ++ " + " ++ e2 ++ ")")
+
+-- ok, I feel like I've done this before?
+-- or it was an example in another of his articles
+pushNeg : Exp → Exp
+pushNeg e@(Lit _) = e
+pushNeg e@(Neg (Lit _)) = e
+pushNeg (Neg (Neg e)) = e
+pushNeg (Neg (ADD e1 e2)) = (ADD (pushNeg $ Neg e1) (pushNeg $ Neg e2))
+pushNeg (ADD e1 e2) = ADD (pushNeg e1) (pushNeg e2)
+
+ti1Norm  : Exp
+ti1Norm = pushNeg ti1
+
+ti1NormView ti1NNormView : String
+ti1NormView = view ti1Norm
+
+ti1NNormView = view (pushNeg (Neg ti1))
+
+ExpBB1 : U
+ExpBB1 = ∀ a. ExpOps a → a
+
+-- curry record (he newtypes this.  do we need to?)
+
+ExpBB : U
+ExpBB = ∀ a. (Int → a) → (a → a) → (a → a → a) → a
+
+lit : Int → ExpBB
+lit x = \onlit onneg onadd => onlit x
+
+neg : ExpBB → ExpBB
+neg e = \ {a} onlit onneg onadd => onneg (e {a} onlit onneg onadd)
+
+add : ExpBB → ExpBB → ExpBB
+add e1 e2 = \ {a} onlit onneg onadd =>
+  onadd (e1 {a} onlit onneg onadd)
+        (e2 {a} onlit onneg onadd)
+
+bbOps : ExpOps ExpBB
+bbOps = MkExpOps lit neg add
+
+viewBB : ExpBB → String
+-- FIXME - without the {String} it is unifying Int → String with U
+-- Like an insert is not happening?
+viewBB e = e {String} onlit onneg onadd
+  where
+    onlit : Int → String
+    onlit n = show n
+    onneg : String → String
+    onneg e = "(-" ++ e ++ ")"
+    onadd : String → String → String
+    onadd e1 e2 = "(" ++ e1 ++ " , " ++ e2 ++ ")"
+
+
+-- extensionally:
+-- e (olit bbOps) (oneg bbOps) (oAdd bbOps) == e
+
+data ExpF a = FLit Int
+            | FNeg a
+            | FAdd a a
+
+roll : ExpF ExpBB → ExpBB
+roll (FLit n) = lit n
+roll (FNeg e) = neg e
+-- FIXME a {a} arg is being stripped off of the type before it's compared with ExpBB
+roll (FAdd e1 e2) = add e1 e2
+
+unroll : ExpBB → ExpF ExpBB
+unroll e = e onlit onneg onadd
+  where
+    onlit : Int → ExpF ExpBB
+    onlit n = FLit n
+    onneg : ExpF ExpBB → ExpF ExpBB
+    onneg e = FNeg (roll e)
+    onadd : ExpF ExpBB → ExpF ExpBB →  ExpF ExpBB
+    onadd e1 e2 = FAdd (roll e1) (roll e2)
+
+
+main : IO Unit
+main = do
+  putStrLn ti1NormView
+  putStrLn ti1NNormView
+

newt/Equality.newt

@@ -1,24 +0,0 @@
-module Equality
-
-data Eq : {A : U} -> A -> A -> U where
-  Refl : {A : U} {a : A} -> Eq a a
-
--- Some magic is not happening here.
-
-sym : {A : U} {x y : A} -> Eq x y -> Eq y x
-sym Refl = Refl
-
-trans : {A : U} {x y z : A} -> Eq x y -> Eq y z -> Eq x z
-trans Refl Refl = Refl
-
-coerce : {A B : U} -> Eq A B -> A -> B
-coerce Refl a = a
-
-J : {A : U} ->
-    {C : (x y : A) -> Eq x y -> U} ->
-    (c : (x : _) -> C x x Refl) ->
-    (x y : A) ->
-    (p : Eq x y) ->
-    C x y p
--- this was failing until I constrained scrutinee to the constructor + args
-J c x y Refl = c x

newt/Problem.newt

@@ -0,0 +1,55 @@
+module Problem
+
+data Unit : U where
+  MkUnit : Unit
+
+infixr 7 _::_
+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
+  _~>_ : Type -> Type -> Type
+
+A : U
+A = Unit
+
+Val : Type -> U
+Val ι = A
+Val (x ~> y) = Val x -> Val y
+
+Ctx : U
+Ctx = List Type
+
+data Ref : Type -> Ctx -> U where
+  Z : {σ : Type} {Γ : Ctx} -> Ref σ (σ :: Γ)
+  S : {σ τ : Type} {Γ : Ctx} -> Ref σ Γ -> Ref σ (τ :: Γ)
+
+data Term : Ctx -> Type -> U where
+  App : {Γ : Ctx} {σ τ : Type} -> Term Γ (σ ~> τ) -> Term Γ σ -> Term Γ τ
+  Lam : {Γ : Ctx} {σ τ : Type} -> Term (σ :: Γ) τ -> Term Γ (σ ~> τ)
+  Var : {Γ : Ctx} {σ : Type} -> Ref σ Γ → Term Γ σ
+
+infixr 7 _:::_
+data Env : Ctx -> U where
+  ENil : Env Nil
+  _:::_ : {Γ : Ctx} {σ : Type} → Val σ → Env Γ → Env (σ :: Γ)
+
+-- FIXME there is a problem here with coverage checking
+-- if we split Z first, we are fine.
+-- ENil is an impossible case, but we need to look at the constructors
+-- if we're running backwards, so
+--   lookup () ENil
+-- we don't have that notation yet.
+
+lookup : {σ : Type} {Γ : Ctx} → Ref σ Γ → Env Γ → Val σ
+lookup Z (x ::: y) = x
+-- and we have to way to say no cases here, either...
+-- lookup ref ENil = case ref of {}
+-- This does work
+-- lookup Z env = case env of (x ::: y) => x
+lookup (S i) (x ::: env) = lookup i env

newt/TypeClass.newt

@@ -1,84 +0,0 @@
-module TypeClass
-
-data Monad : (U -> U) -> U where
-  MkMonad : { M : U -> U } ->
-            (bind : {A B : U} -> (M A) -> (A -> M B) -> M B) ->
-            (pure : {A : U} -> A -> M A) ->
-            Monad M
-
-infixl 1 _>>=_ _>>_
-_>>=_ : {a b : U} -> {m : U -> U} -> {{x : Monad m}} -> (m a) -> (a -> m b) -> m b
-_>>=_ {a} {b} {m} {{MkMonad bind' _}}  ma amb = bind' {a} {b} ma amb
-
-_>>_ : {a b : U} -> {m : U -> U} -> {{x : Monad m}} -> m a -> m b -> m b
-ma >> mb = mb
-
-pure : {a : U} {m : U -> U} {{_ : Monad m}} -> a -> m a
-pure {_} {_} {{MkMonad _ pure'}} a = pure' a
-
-data Either : U -> U -> U where
-  Left : {A B : U} -> A -> Either A B
-  Right : {A B : U} -> B -> Either A B
-
-bindEither : {A B C : U} -> (Either A B) -> (B -> Either A C) -> Either A C
-bindEither (Left a) amb = Left a
-bindEither (Right b) amb = amb b
-
-EitherMonad : {A : U} -> Monad (Either A)
-EitherMonad = MkMonad {Either A} bindEither Right
-
-data Maybe : U -> U where
-  Just    : {A : U} -> A -> Maybe A
-  Nothing : {A : U} -> Maybe A
-
-bindMaybe : {A B : U} -> Maybe A -> (A -> Maybe B) -> Maybe B
-bindMaybe Nothing amb = Nothing
-bindMaybe (Just a) amb = amb a
-
-MaybeMonad : Monad Maybe
-MaybeMonad = MkMonad bindMaybe Just
-
-infixr 7 _::_
-data List : U -> U where
-  Nil : {A : U} -> List A
-  _::_ : {A : U} -> A -> List A -> List A
-
-infixl 7 _++_
-_++_ : {A : U} -> List A -> List A -> List A
-Nil ++ ys = ys
-(x :: xs) ++ ys = x :: (xs ++ ys)
-
-bindList : {A B : U} -> List A -> (A -> List B) -> List B
-bindList Nil f = Nil
-bindList (x :: xs) f = f x ++ bindList xs f
-
-singleton : {A : U} -> A -> List A
-singleton a = a :: Nil
-
--- TODO need better error when the monad is not defined
-ListMonad : Monad List
-ListMonad = MkMonad bindList singleton
-
-infixr 1 _,_
-data Pair : U -> U -> U where
-  _,_ : {A B : U} -> A -> B -> Pair A B
-
-
-
-test : Maybe Int
-test = pure 10
-
-foo : Int -> Maybe Int
-foo x = Just 42 >> Just x >>= (\ x => pure {_} {Maybe} 10)
-
-bar : Int -> Maybe Int
-bar x = do
-  let y = x
-  z <- Just x
-  pure z
-
-baz : {A B : U} -> List A -> List B -> List (Pair A B)
-baz xs ys = do
-  x <- xs
-  y <- ys
-  pure (x , y)

tests/BadAlt.newt

@@ -0,0 +1,6 @@
+module BadAlt
+
+import Prelude
+
+foo : List Int → Int
+foo (xs :< x) = x

tests/Combinatory.newt

@@ -0,0 +1,96 @@
+module Combinatory
+
+-- "A correct-by-construction conversion from lambda calculus to combinatory logic", Wouter Swierstra
+
+data Unit : U where
+  MkUnit : Unit
+
+infixr 7 _::_
+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
+  _~>_ : Type -> Type -> Type
+
+A : U
+A = Unit
+
+Val : Type -> U
+Val ι = A
+Val (x ~> y) = Val x -> Val y
+
+Ctx : U
+Ctx = List Type
+
+data Ref : Type -> Ctx -> U where
+  Here : {σ : Type} {Γ : Ctx} -> Ref σ (σ :: Γ)
+  There : {σ τ : Type} {Γ : Ctx} -> Ref σ Γ -> Ref σ (τ :: Γ)
+
+data Term : Ctx -> Type -> U where
+  App : {Γ : Ctx} {σ τ : Type} -> Term Γ (σ ~> τ) -> Term Γ σ -> Term Γ τ
+  Lam : {Γ : Ctx} {σ τ : Type} -> Term (σ :: Γ) τ -> Term Γ (σ ~> τ)
+  Var : {Γ : Ctx} {σ : Type} -> Ref σ Γ → Term Γ σ
+
+infixr 7 _:::_
+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 (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 σ)
+-- 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
+
+data Comb : (Γ : Ctx) → (u : Type) → (Env Γ → Val u) → U where
+  S : {Γ : Ctx} {σ τ τ' : Type} → Comb Γ ((σ ~> τ ~> τ') ~> (σ ~> τ) ~> (σ ~> τ')) (\ env => \ f g x => (f x) (g x))
+  K : {Γ : Ctx} {σ τ : Type} → Comb Γ (σ ~> (τ ~> σ)) (\ env => \ x y => x)
+  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)
+  CApp : {Γ : Ctx} {σ τ : Type} {f : _} {x : _} → Comb Γ (σ ~> τ) f → Comb Γ σ x → Comb Γ τ (\ env => (f env) (x env))
+
+sapp : {Γ : Ctx} {σ τ ρ : Type} {f : _} {x : _} →
+  Comb Γ (σ ~> τ ~> ρ) f →
+  Comb Γ (σ ~> τ) x →
+  Comb Γ (σ ~> ρ) (\ env y => (f env y) (x env y))
+sapp (CApp K t) I = t
+sapp (CApp K t) (CApp K u) = CApp K (CApp t u)
+-- was out of pattern because of unexpanded lets.
+sapp (CApp K t) u = CApp (CApp B t) u
+sapp t (CApp K u) = CApp (CApp C t) u
+sapp t u = CApp (CApp S t) u
+
+abs : {Γ : Ctx} {σ τ : Type} {f : _} → Comb (σ :: Γ) τ f → Comb Γ (σ ~> τ) (\ env x => f (x ::: env))
+abs S = CApp K S
+abs K = CApp K K
+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.
+abs (CVar Here) = I
+abs (CVar (There i)) = CApp K (CVar i)
+
+translate : {Γ : Ctx} {σ : Type} → (tm : Term Γ σ) → Comb Γ σ (eval tm)
+translate (App t u) = CApp (translate t) (translate u)
+translate (Lam t) = abs (translate t)
+translate (Var i) = CVar i

tests/Duplicate.newt

@@ -0,0 +1,6 @@
+module Duplicate
+
+-- duplicate name should fail
+data Either : U -> U -> U where
+  Left : {a b : U} -> a -> Either a b
+  Left : {a b : U} -> b -> Either a b

tests/Duplicate.newt.fail

@@ -0,0 +1,9 @@
+*** Process tests/Duplicate.newt
+module Duplicate
+ERROR at tests/Duplicate.newt:4:1--4:5: Duplicate.Left is already defined at tests/Duplicate.newt:4:1--4:5
+  
+  -- duplicate name should fail
+  data Either : U -> U -> U where
+  ^^^^
+
+Compile failed