diff --git a/newt/Combinatory.newt b/playground/samples/Combinatory.newt similarity index 96% rename from newt/Combinatory.newt rename to playground/samples/Combinatory.newt index b4cbc83..e263e8e 100644 --- a/newt/Combinatory.newt +++ b/playground/samples/Combinatory.newt @@ -81,7 +81,7 @@ 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 -- TODO unsolved meta, out of pattern fragment -sapp t (CApp K u) = CApp (CApp C t) u +sapp t (CApp K u) = ? -- CApp (CApp C t) u -- TODO unsolved meta, out of pattern fragment sapp t u = ? -- CApp (CApp S t) u @@ -92,7 +92,7 @@ abs I = CApp K I abs B = CApp K B abs C = CApp K C abs (CApp t u) = sapp (abs t) (abs u) --- -- TODO lookup2 was getting stuck, needed to bounce the types in a rewritten env. +-- lookup2 was getting stuck, needed to bounce the types in a rewritten env. abs (CVar Here) = I abs (CVar (There i)) = CApp K (CVar i) diff --git a/playground/samples/DSL.newt b/playground/samples/DSL.newt new file mode 100644 index 0000000..d4f9ba0 --- /dev/null +++ b/playground/samples/DSL.newt @@ -0,0 +1,120 @@ +module DSL + +-- https://www.youtube.com/watch?v=sFyy9sssK50 + +data ℕ : U where + Z : ℕ + S : ℕ → ℕ + +infixl 7 _+_ +infixl 8 _*_ + +_+_ : ℕ → ℕ → ℕ +Z + m = m +(S k) + m = S (k + m) + +_*_ : ℕ → ℕ → ℕ +Z * m = Z +(S k) * m = m + k * m + +infixr 4 _::_ +data Vec : U → ℕ → U where + Nil : {a} → Vec a Z + _::_ : {a k} → a → Vec a k → Vec a (S k) + +infixl 5 _++_ +_++_ : {a n m} → Vec a n → Vec a m → Vec a (n + m) +Nil ++ ys = ys +(x :: xs) ++ ys = x :: (xs ++ ys) + +map : {a b n} → (a → b) → Vec a n → Vec b n +map f Nil = Nil +map f (x :: xs) = f x :: map f xs + +data E : U where + Zero : E + One : E + Add : E → E → E + Mul : E → E → E + +two : E +two = Add One One + +four : E +four = Mul two two + +card : E → ℕ +card Zero = Z +card One = S Z +card (Add x y) = card x + card y +card (Mul x y) = card x * card y + +data Empty : U where + +data Unit : U where + -- unit accepted but case building thinks its a var + unit : Unit + +data Either : U -> U -> U where + Left : {A B} → A → Either A B + Right : {A B} → B → Either A B + +infixr 4 _,_ +data Both : U → U → U where + _,_ : {A B} → A → B → Both A B + +typ : E → U +typ Zero = Empty +typ One = Unit +typ (Add x y) = Either (typ x) (typ y) +typ (Mul x y) = Both (typ x) (typ y) + +Bool : U +Bool = typ two + +false : Bool +false = Left unit + +true : Bool +true = Right unit + +BothBoolBool : U +BothBoolBool = typ four + +ex1 : BothBoolBool +ex1 = (false, true) + +enumAdd : {a b m n} → Vec a m → Vec b n → Vec (Either a b) (m + n) +enumAdd xs ys = map Left xs ++ map Right ys + +-- for this I followed the shape of _*_, the lecture was slightly different +enumMul : {a b m n} → Vec a m → Vec b n → Vec (Both a b) (m * n) +enumMul Nil ys = Nil +enumMul (x :: xs) ys = map (_,_ x) ys ++ enumMul xs ys + +enumerate : (t : E) → Vec (typ t) (card t) +enumerate Zero = Nil +enumerate One = unit :: Nil +enumerate (Add x y) = enumAdd (enumerate x) (enumerate y) +enumerate (Mul x y) = enumMul (enumerate x) (enumerate y) + +test2 : Vec (typ two) (card two) +test2 = enumerate two + +test4 : Vec (typ four) (card four) +test4 = enumerate four + +-- TODO I need to add #eval, like Lean +-- #eval enumerate two + +-- for now, I'll define ≡ to check + +infixl 2 _≡_ +data _≡_ : {A} → A → A → U where + Refl : {A} {a : A} → a ≡ a + +test2' : test2 ≡ false :: true :: Nil +test2' = Refl + +test4' : test4 ≡ (false, false) :: (false, true) :: (true, false) :: (true, true) :: Nil +test4' = Refl diff --git a/playground/src/main.ts b/playground/src/main.ts index 7fb9099..93c8f8a 100644 --- a/playground/src/main.ts +++ b/playground/src/main.ts @@ -144,14 +144,15 @@ function Tabs() { const SAMPLES = [ "Tour.newt", + "DSL.newt", "Tree.newt", - // "Prelude.newt", "Reasoning.newt", "Lists.newt", "Day1.newt", "Day2.newt", "Lib.newt", "TypeClass.newt", + "Combinatory.newt", ]; function EditWrap({vertical, toggle}: {vertical: boolean, toggle: () => void}) { diff --git a/src/Lib/Parser.idr b/src/Lib/Parser.idr index 3db1b68..d65f02c 100644 --- a/src/Lib/Parser.idr +++ b/src/Lib/Parser.idr @@ -385,7 +385,7 @@ parseData : Parser Decl parseData = do fc <- getPos keyword "data" - name <- uident <|> token MixFix + name <- uident <|> ident <|> token MixFix keyword ":" ty <- typeExpr keyword "where"