add smoke tests

tests/black/Zoo1.newt

@@ -0,0 +1,102 @@
+module Zoo1
+
+-- I'm starting to translate ezoo 01-eval-closures-debruijn as a test cases.
+
+ptype Int
+ptype String
+
+------- Prelude stuff
+
+data Nat : U where
+  Z : Nat
+  S : Nat -> Nat
+
+data Unit : U where
+  MkUnit : Unit
+
+data List : U -> U where
+  Nil : {a : U} -> List a
+  Cons : {a : U} -> a -> List a -> List a
+
+data Maybe : U -> U where
+  Just : {a : U} -> a -> Maybe a
+  Nothing : {a : U} -> Maybe a
+
+
+----------------------------------
+
+-- forward declaration
+Val : U
+
+data Tm : U where
+  Var : Nat -> Tm
+  Lam : Tm -> Tm -- lam (x.t)
+  App : Tm -> Tm -> Tm
+  Let : Tm -> Tm -> Tm -- let t (x.u)
+
+data Env : U where
+  ENil : Env
+  Define : Env -> Val -> Env
+
+data Closure : U where
+  MkClosure : Env -> Tm -> Closure
+
+data Val : U where
+  VVar : Nat -> Val
+  VApp : Val -> Val -> Val
+  VLam : Closure -> Val
+
+length : Env -> Nat
+length ENil = Z
+length (Define env _) = S (length env)
+
+lookup : Env -> Nat -> Maybe Val
+lookup (Define env v) Z = Just v
+-- If I write "Just (lookup env k)" on RHS, it's wrong, but the error message is unusable (mainly due to FC)
+-- The FC is fine if I write lookup {Val} env k
+lookup (Define env _) (S k) = lookup env k
+lookup (ENil) x = Nothing
+
+eval : Env -> Tm -> Val
+
+cApp : Closure -> Val -> Val
+-- If I put Closure instead of MkClosure, it reports missing case, fix that (should be bad constructor or something)
+cApp (MkClosure env t) u = eval (Define env u) t
+
+hole : Val
+
+-- TODO need to inline solved metas somewhere, as error messages are unreadable
+-- NEXT fix FC for missing case if we remove _
+
+eval env tm = case tm of
+  (Var x) =>
+    case lookup env x of
+    -- case doesn't use the new code.  We've got a wildcard here that
+    -- is forced to {Val}, but we don't have forcing/dotting
+    -- I guess we see what Jesper says about dotting
+    Just x => x
+    Nothing => VVar x
+  -- TODO no tupls yet
+  App t u => case eval env t of
+    VLam t => cApp t (eval env u)
+    t      => VApp t (eval env u)
+  Lam t => VLam (MkClosure env t)
+  Let t u => eval (Define env (eval env t)) u
+  -- NEXT this is unreachable, find out how to warn about it
+  -- _ => hole
+
+lvl2ix : Nat -> Nat -> Nat
+lvl2ix (S k) (S j) = lvl2ix k j
+lvl2ix Z (S j) = j
+lvl2ix _ Z = Z -- shouldn't happen
+
+quote : Nat -> Val -> Tm
+quote l v = case v of
+  VVar x => Var (lvl2ix l x)
+  VApp t u => App (quote l t) (quote l u)
+  VLam t => Lam (quote (S l) (cApp t (VVar l)))
+
+nf : Env -> Tm -> Tm
+nf env t = quote (length env) (eval env t)
+
+-- and then a parser / example

tests/black/test1.newt

@@ -0,0 +1,9 @@
+module Scratch
+
+nat : U
+nat = {C : U} -> C -> (nat -> C) -> C
+
+-- TESTCASE This was broken when I wasn't expanding Ref ty in check
+-- Also broken when I tried to put Def in VRef
+succ : nat -> nat
+succ = \n => \ z s => s n

tests/black/testcase.newt

@@ -0,0 +1,76 @@
+module Scratch
+
+-- I'm testing cases here, but using examples carefully design to be
+-- simple case trees. Patterns are a var or a constructor applied to vars.
+
+-- There are indexes below, but we're got pulling constraints out of them yet.
+
+ptype Int
+
+data Nat : U where
+  Z : Nat
+  S : Nat -> Nat
+
+data Vect : Nat -> U -> U where
+  Nil : {a : U} -> Vect Z a
+  Cons : {a : U} {n : Nat} -> a -> Vect n a -> Vect (S n) a
+
+plus : Nat -> Nat -> Nat
+plus = \ n m => case n of
+  Z => m
+  S k => S (plus k m)
+
+-- Example from Jesper talk (translated to explicit case tree)
+max : Nat -> Nat -> Nat
+max = \ n m => case n of
+  Z => m
+  S k => case m of
+    Z => S k
+    S l => S (max k l)
+
+length : {a : U} {n : Nat} -> Vect n a -> Nat
+length = \ v => case v of
+  Nil => Z
+  Cons x xs => S (length xs)
+
+data Unit : U where
+  MkUnit : Unit
+
+-- This should fail (and does!)
+-- bar : Vect (S Z) Unit
+-- bar = (Cons MkUnit (Cons MkUnit Nil))
+
+data Bool : U where
+  True : Bool
+  False : Bool
+
+not : Bool -> Bool
+not = \ v => case v of
+  True => False
+  False => True
+
+
+not2 : Bool -> Bool
+not2 = \ v => case v of
+  True => False
+  x => True
+
+and : Bool -> Bool -> Bool
+and = \ x y => case x of
+  True => y
+  False => False
+
+-- FIXME - a case is evaluated here, and I don't know why.
+
+nand : Bool -> Bool -> Bool
+nand = \ x y => not (case x of
+    True => y
+    False => False)
+
+-- -- this should be an error.
+-- foo : Bool -> Bool
+
+data Void : U where
+
+foo : Int
+foo = 42

tests/black/testcase2.newt

@@ -0,0 +1,68 @@
+module Scratch
+
+data Nat : U where
+  Z : Nat
+  S : Nat -> Nat
+
+plus : Nat -> Nat -> Nat
+plus Z m = m
+-- if this is a capital K on LHS, it fails with a poor error message
+plus (S k) m = S (plus k m)
+
+-- -- Example from Jesper talk (translated to case tree)
+max : Nat -> Nat -> Nat
+max Z m = m
+max n Z = n
+max (S k) (S l) = S (max k l)
+
+data List : U -> U where
+  LN : {a : U} -> List a
+  LCons : {a : U} -> a -> List a -> List a
+
+data Vect : Nat -> U -> U where
+  Nil : {a : U} -> Vect Z a
+  Cons : {a : U} {n : Nat} -> a -> Vect n a -> Vect (S n) a
+
+-- NEXT Need to handle implicits
+-- I've hacked implicits, but need to figure out indices..
+length : {a : U} {n : Nat} -> Vect n a -> Nat
+length Nil = Z
+length (Cons x xs) = S (length xs)
+
+data Unit : U where
+  MkUnit : Unit
+
+-- This should fail (and does!)
+-- bar : Vect (S Z) Unit
+-- bar = (Cons MkUnit (Cons MkUnit Nil))
+
+data Bool : U where
+  True : Bool
+  False : Bool
+
+not : Bool -> Bool
+not True = False
+not False = True
+
+
+not2 : Bool -> Bool
+not2 True = False
+not2 x = True
+
+-- TEST CASE - remove second clause here and expect error
+and : Bool -> Bool -> Bool
+and True y = y
+and False _ = False
+
+nand : Bool -> Bool -> Bool
+nand x y = not (case x of
+    True => y
+    False => False)
+
+
+-- for stuff like this, we should add Agda () and check for no constructors
+data Void : U where
+
+SnocList : U -> U
+SnocList a = List a
+

tests/black/testcase3.newt

@@ -0,0 +1,25 @@
+module Scratch2
+
+data Nat : U where
+  Z : Nat
+  S : Nat -> Nat
+
+data Maybe : U -> U where
+  Just : {a : U} -> a -> Maybe a
+  Nothing : {a : U} -> Maybe a
+
+
+-- failed to unify _:1 with Val
+-- Legit on RHS, IMO. On LHS, we should be dotting?
+-- I either need to unify and collect constraints or figure out how
+-- other systems manage this.
+
+-- Note that an unused
+-- variable may stand for either a wildcard or a forced pattern. In the latter case our algorithm
+-- treats it as a let-bound variable in the right-hand side of the clause.
+
+-- we need let-bound in environment but we do have define.
+
+fromMaybe : Maybe Nat -> Nat
+fromMaybe (Just x) = x
+fromMaybe Nothing = Z

tests/black/testprim.newt

@@ -0,0 +1,43 @@
+module TestPrim
+
+
+-- we need to be able to declare a primitive type
+-- distinct from inductive type. there are no constructors per-se but it is inhabited
+
+ptype String
+ptype Int
+
+pfunc strlen : String -> Int := "(x) => x.length()"
+
+-- why is there an eta in here?
+foo : String -> Int
+foo = \ x => strlen x
+
+bar : String -> String -> Int
+bar = \ x y => strlen x
+
+pfunc append : String -> String -> String := "(a,b) => a + b"
+
+blah : String
+blah = append "hello" "world"
+
+pfunc plus : Int -> Int -> Int := "(a,b) => a + b"
+
+answer : Int
+answer = plus 40 2
+
+-- I'd like to define prim operators too
+
+-- codegen test cases
+-- works, but two looks like () => (eta1) => (eta0) => one(eta1, eta0)
+pfunc one : Int -> Int -> Int := "(x,y) => x + y"
+
+two : Int -> Int -> Int
+two = one
+
+three : Int -> Int -> Int
+three = \ x => two x
+
+four : Int -> Int -> Int
+four = \x y => three x y
+

tests/black/zoo2eg.newt

@@ -0,0 +1,38 @@
+module Zoo2
+
+id : (A : U) -> A -> A
+id = \ A x => x
+
+const : (A B : U) -> A -> B -> A
+const = \A B x y => x
+
+Nat : U
+Nat = (N : U) -> (N -> N) -> N -> N
+
+zero : Nat
+zero = \ _ s z => z
+
+succ : Nat -> Nat
+succ = \ n ty s z => s (n ty s z)
+
+-- need Nat to reduce (and syntax highlighting)
+five : Nat
+five = \ N s z => s (s (s (s (s z))))
+
+add : Nat -> Nat -> Nat
+add = \a b N s z => a N s (b N s z)
+
+mul : Nat -> Nat -> Nat
+mul = \a b N s z => a N (b N s) z
+
+ten : Nat
+ten = add five five
+
+hundred : Nat
+hundred = mul ten ten
+
+thousand : Nat
+thousand = mul ten hundred
+
+-- and then nf / eval of hundred
+-- #nf hundred

tests/black/zoo3eg.newt

@@ -0,0 +1,58 @@
+module Zoo3
+
+id : (A : _) -> A -> A
+id = \ A x => x
+
+List : U -> U
+List = \ A => (L : _) -> (A -> L -> L) -> L -> L
+
+nil : (A : _) -> List A
+nil = \ A L cons nil => nil
+
+cons : (A : _) -> A -> List A -> List A
+cons = \A x xs L cons nil => cons x (xs _ cons nil)
+
+Bool : U
+Bool = (B : _) -> B -> B -> B
+
+true : Bool
+true = \ B t f => t
+
+false : Bool
+false = \ B t f => f
+
+not : Bool -> Bool
+not = \ b B t f => b B f t
+
+Eq : (A : _) -> A -> A -> U
+Eq = \A x y => (P : A -> U) -> P x -> P y
+
+refl : (A : _) (x : A) -> Eq A x x
+refl = \ A x p px => px
+
+list1 : List Bool
+list1 = cons _ true (cons _ false (nil _))
+
+Nat : U
+Nat = (N : U) -> (N -> N) -> N -> N
+
+five : Nat
+five = \ N s z => s (s (s (s (s z))))
+
+add : Nat -> Nat -> Nat
+add = \ a b N s z => a N s (b N s z)
+
+mul : Nat -> Nat -> Nat
+mul = \a b N s z => a N (b N s) z
+
+ten : Nat
+ten = add five five
+
+hundred : Nat
+hundred = mul ten ten
+
+thousand : Nat
+thousand = mul ten hundred
+
+eqTest : Eq _ hundred hundred
+eqTest = refl _ _

tests/black/zoo4eg.newt

@@ -0,0 +1,93 @@
+module Zoo4
+
+id : {A : U} -> A -> A
+id = \x => x   -- elaborated to \{A} x. x
+
+-- implicit arg types can be omitted
+const : {A B} -> A -> B -> A
+const = \x y => x
+
+-- function arguments can be grouped:
+group1 : {A B : U}(x y z : A) -> B -> B
+group1 = \x y z b => b
+
+group2 : {A B}(x y z : A) -> B -> B
+group2 = \x y z b=> b
+
+-- explicit id function used for annotation as in Idris
+the : (A : _) -> A -> A
+the = \_ x => x
+
+-- implicit args can be explicitly given
+-- NB kovacs left off the type (different syntax), so I put a hole in there
+argTest1 : _
+argTest1 = const {U} {U} U
+
+-- I've decided not to do = in the {} for now.
+-- let argTest2 = const {B = U} U;  -- only give B, the second implicit arg
+
+-- again no type, this hits a lambda in infer.
+-- I think we need to create two metas and make a pi of them.
+insert2 : _
+insert2 = (\{A} x => the A x) U -- (\{A} x => the A x) {U} U
+
+Bool : U
+Bool = (B : _) -> B -> B -> B
+
+true : Bool
+true = \B t f => t
+
+false : Bool
+false = \B t f => f
+
+List : U -> U
+List = \A => (L : _) -> (A -> L -> L) -> L -> L
+
+nil : {A} -> List A
+nil = \L cons nil => nil
+
+cons : {A} -> A -> List A -> List A
+cons = \ x xs L cons nil => cons x (xs L cons nil)
+
+map : {A B} -> (A -> B) -> List A -> List B
+map = \{A} {B} f xs L c n => xs L (\a => c (f a)) n
+
+list1 : List Bool
+list1 = cons true (cons false (cons true nil))
+
+-- dependent function composition
+comp : {A} {B : A -> U} {C : {a} -> B a -> U}
+       (f : {a} (b : B a) -> C b)
+       (g : (a : A) -> B a)
+       (a : A)
+       -> C (g a)
+comp = \f g a => f (g a)
+
+compExample : _
+compExample = comp (cons true) (cons false) nil
+
+Nat : U
+Nat = (N : U) -> (N -> N) -> N -> N
+
+-- TODO - first underscore there, why are there two metas?
+mul : Nat -> Nat -> Nat
+mul = \a b N s z => a _ (b _ s) z
+
+ten : Nat
+ten = \N s z => (s (s (s (s (s (s (s (s (s (s z))))))))))
+
+hundred : _
+hundred = mul ten ten
+
+-- Leibniz equality
+Eq : {A} -> A -> A -> U
+Eq = \{A} x y => (P : A -> U) -> P x -> P y
+
+refl : {A} {x : A} -> Eq x x
+refl = \_ px => px
+
+sym : {A x y} -> Eq {A} x y -> Eq y x
+sym = \p => p (\y => Eq y x) refl
+
+eqtest : Eq (mul ten ten) hundred
+eqtest = refl