From 51487456df6d641f005efd5aef1baa26054b87db Mon Sep 17 00:00:00 2001 From: pilfer-pandex <47340789+pilfer-pandex@users.noreply.github.com> Date: Tue, 10 Sep 2019 18:57:00 -0400 Subject: [PATCH] some nock stuff --- pkg/proto/app/Main.hs | 4 +- pkg/proto/lib/Lib.hs | 6 - pkg/proto/lib/Nock.hs | 166 ++++++++++++++++++++++++++++ pkg/proto/lib/PrintUntypedLambda.hs | 23 ++++ pkg/proto/lib/UntypedLambda.hs | 50 +++++++++ pkg/proto/package.yaml | 8 +- stack.yaml | 11 ++ 7 files changed, 259 insertions(+), 9 deletions(-) delete mode 100644 pkg/proto/lib/Lib.hs create mode 100644 pkg/proto/lib/Nock.hs create mode 100644 pkg/proto/lib/PrintUntypedLambda.hs create mode 100644 pkg/proto/lib/UntypedLambda.hs create mode 100644 stack.yaml diff --git a/pkg/proto/app/Main.hs b/pkg/proto/app/Main.hs index de1c1ab35c..05a3d00760 100644 --- a/pkg/proto/app/Main.hs +++ b/pkg/proto/app/Main.hs @@ -1,6 +1,6 @@ module Main where -import Lib +import ClassyPrelude main :: IO () -main = someFunc +main = pure () diff --git a/pkg/proto/lib/Lib.hs b/pkg/proto/lib/Lib.hs deleted file mode 100644 index d36ff2714d..0000000000 --- a/pkg/proto/lib/Lib.hs +++ /dev/null @@ -1,6 +0,0 @@ -module Lib - ( someFunc - ) where - -someFunc :: IO () -someFunc = putStrLn "someFunc" diff --git a/pkg/proto/lib/Nock.hs b/pkg/proto/lib/Nock.hs new file mode 100644 index 0000000000..c2f3bb0f04 --- /dev/null +++ b/pkg/proto/lib/Nock.hs @@ -0,0 +1,166 @@ +module Nock where + +import ClassyPrelude + +type Atom = Integer + +data Tree a = Atom !a + | Cell !(Tree a) !(Tree a) + deriving (Eq, Ord, Read, Show, Functor) + +type Noun = Tree Atom + +yes, no :: Noun +yes = Atom 0 +no = Atom 1 + +-- | Tree address +type Axis = Atom + +data Nock = NC Nock Nock -- ^ ^: autocons + | N0 Axis -- ^ 0, axis: tree addressing + | N1 Noun -- ^ 1, const: constant + | N2 Nock Nock -- ^ 2, compose: compute subject, formula; apply + | N3 Nock -- ^ 3, is cell + | N4 Nock -- ^ 4, succ + | N5 Nock Nock -- ^ 5, eq + | N6 Nock Nock Nock -- ^ 6, if + | N7 Nock Nock -- ^ 7, then: => + | N8 Nock Nock -- ^ 8, push: =+ + | N9 Axis Nock -- ^ 9, invoke + | N10 (Axis, Nock) Nock -- ^ 10, edit + | N11 Hint Nock -- ^ 11, hint + | N12 Nock Nock -- ^ 12, scry + deriving (Eq, Ord, Read, Show) + +data Hint = Tag Atom + | Assoc Atom Nock + deriving (Eq, Ord, Read, Show) + +nockToNoun :: Nock -> Noun +nockToNoun = go + where + go = \case + NC f g -> Cell (go f) (go g) + N0 a -> Cell (Atom 0) (Atom a) + N1 n -> Cell (Atom 1) n + N2 f g -> Cell (Atom 2) (Cell (go f) (go g)) + N3 f -> Cell (Atom 3) (go f) + N4 f -> Cell (Atom 4) (go f) + N5 f g -> Cell (Atom 5) (Cell (go f) (go g)) + N6 f g h -> Cell (Atom 5) (Cell (go f) (Cell (go g) (go h))) + N7 f g -> Cell (Atom 7) (Cell (go f) (go g)) + N8 f g -> Cell (Atom 8) (Cell (go f) (go g)) + N9 a f -> Cell (Atom 9) (Cell (Atom a) (go f)) + N10 (a, f) g -> Cell (Atom 10) (Cell (Cell (Atom a) (go f)) (go g)) + N11 (Tag a) f -> Cell (Atom 11) (Cell (Atom a) (go f)) + N11 (Assoc a f) g -> Cell (Atom 11) (Cell (Cell (Atom a) (go f)) (go g)) + N12 f g -> Cell (Atom 12) (Cell (go f) (go g)) + +nounToNock :: Noun -> Nock +nounToNock = go + where + go = \case + Atom{} -> error "nounToNock: atom" + Cell n@Cell{} m -> NC (go n) (go m) + Cell (Atom op) n -> case op of + 0 | (Atom a) <- n -> N0 a + 1 -> N1 n + 2 | (Cell m o) <- n -> N2 (go m) (go o) + 3 -> N3 (go n) + 4 -> N4 (go n) + 5 | (Cell m o) <- n -> N5 (go m) (go o) + 6 | (Cell m (Cell o p)) <- n -> N6 (go m) (go o) (go p) + 7 | (Cell m o) <- n -> N7 (go m) (go o) + 8 | (Cell m o) <- n -> N8 (go m) (go o) + 9 | (Cell (Atom a) m) <- n -> N9 a (go m) + 10 | (Cell (Cell (Atom a) m) o) <- n -> N10 (a, (go m)) (go o) + 11 | (Cell (Cell (Atom a) m) o) <- n -> N11 (Assoc a (go m)) (go o) + | (Cell (Atom a) m) <- n -> N11 (Tag a) (go m) + 12 | (Cell m o) <- n -> N12 (go m) (go o) + _ -> error ("nockToNoun: invalid " <> show op <> " " <> show n) + +-- | Nock interpreter +nock :: Noun -> Nock -> Noun +nock n = \case + NC f g -> Cell (nock n f) (nock n g) + N0 a -> axis a n + N1 n' -> n' + N2 sf ff -> nock (nock n sf) (nounToNock (nock n ff)) + N3 f -> case nock n f of + Cell{} -> yes + Atom{} -> no + N4 f -> case nock n f of + Cell{} -> error "nock: cannot increment cell" + Atom a -> Atom (a + 1) + N5 f g -> if nock n f == nock n g then yes else no + N6 f g h -> case nock n f of + (Atom 0) -> nock n g + (Atom 1) -> nock n h + _ -> error "nock: invalid test value" + N7 f g -> nock (nock n f) g + N8 f g -> nock (Cell (nock n f) n) g + N9 a f -> let c = nock n f in nock c (nounToNock (axis a c)) + N10{} -> error "nock: I don't want to implement editing right now" + N11 _ f -> nock n f + N12{} -> error "nock: scrying is not allowed" + + +-- Axis logic + +data Dir = L | R + deriving (Eq, Ord, Enum, Read, Show) +type Path = [Dir] + +-- Write an axis as a binary number; e.g. 5 as 101. +-- The rule is: after droping the 1 in the msb, you read from left to right. +-- 0 becomes L and 1 becomes R. + +cap :: Axis -> Dir +cap = \case + 2 -> L + 3 -> R + a | a <= 1 -> error "cap: bad axis" + | otherwise -> cap (div a 2) + +mas :: Axis -> Axis +mas = \case + 2 -> 1 + 3 -> 1 + a | a <= 1 -> error "mas: bad axis" + | otherwise -> (mod a 2) + 2 * mas (div a 2) + +capMas :: Axis -> (Dir, Axis) +capMas = \case + 2 -> (L, 1) + 3 -> (R, 1) + a | a <= 1 -> error "capMas: bad axis" + | otherwise -> (d, (mod a 2) + 2 * r) + where + (d, r) = capMas (div a 2) + +peg :: Axis -> Axis -> Axis +peg a = \case + 1 -> a + 2 -> a * 2 + 3 -> a * 2 + 1 + b -> (mod b 2) + 2 * peg a (div b 2) + +axis :: Axis -> Tree a -> Tree a +axis 1 n = n +axis (capMas -> (d, r)) (Cell n m) = case d of + L -> axis r n + R -> axis r m +axis a n = error ("bad axis: " ++ show a) + +toPath :: Axis -> Path +toPath = \case + 1 -> [] + (capMas -> (d, r)) -> d : toPath r + +toAxis :: Path -> Axis +toAxis = foldl' step 1 + where + step r = \case + L -> 2 * r + R -> 2 * r + 1 diff --git a/pkg/proto/lib/PrintUntypedLambda.hs b/pkg/proto/lib/PrintUntypedLambda.hs new file mode 100644 index 0000000000..f94af44b42 --- /dev/null +++ b/pkg/proto/lib/PrintUntypedLambda.hs @@ -0,0 +1,23 @@ +module PrintUntypedLambda where + +-- it's pretty clowny but whatever + +import Prelude + +import Bound +import Data.Foldable + +import UntypedLambda + +prettyPrec :: [String] -> Bool -> Int -> Exp String -> ShowS +prettyPrec _ d n (Var a) = showString a +prettyPrec vs d n (App x y) = showParen d $ + prettyPrec vs False n x . showChar ' ' . prettyPrec vs True n y +prettyPrec (v:vs) d n (Lam b) = showParen d $ + showString v . showString ". " . prettyPrec vs False n (instantiate1 (Var v) b) + +prettyWith :: [String] -> Exp String -> String +prettyWith vs t = prettyPrec (filter (`notElem` toList t) vs) False 0 t "" + +pretty :: Exp String -> String +pretty = prettyWith $ [ [i] | i <- ['a'..'z']] ++ [i : show j | j <- [1 :: Int ..], i <- ['a'..'z'] ] diff --git a/pkg/proto/lib/UntypedLambda.hs b/pkg/proto/lib/UntypedLambda.hs new file mode 100644 index 0000000000..b06f9abf78 --- /dev/null +++ b/pkg/proto/lib/UntypedLambda.hs @@ -0,0 +1,50 @@ +module UntypedLambda where + +import ClassyPrelude + +import Bound +import Data.Deriving (deriveEq1, deriveOrd1, deriveRead1, deriveShow1) +import Control.Monad.State + +import Nock + +data Exp a + = Var a + | App (Exp a) (Exp a) + | Lam (Scope () Exp a) + deriving (Functor, Foldable, Traversable) + +deriveEq1 ''Exp +deriveOrd1 ''Exp +deriveRead1 ''Exp +deriveShow1 ''Exp +makeBound ''Exp + +deriving instance Eq a => Eq (Exp a) +deriving instance Ord a => Ord (Exp a) +deriving instance Read a => Read (Exp a) +deriving instance Show a => Show (Exp a) + +lam :: Eq a => a -> Exp a -> Exp a +lam v e = Lam (abstract1 v e) + +eval :: Exp a -> Exp a +eval = \case + e@Var{} -> e + e@Lam{} -> e + (App e f) -> case eval e of + (Lam s) -> instantiate1 (eval f) s + e' -> (App e' (eval f)) + +newtype Ref = Ref { unRef :: Int } + +nextRef :: Ref -> Ref +nextRef = Ref . (+ 1) . unRef + +old :: Exp a -> Nock +old = undefined + + +-- x. y. x +-- old: [8 [1 0] [1 8 [1 0] [1 0 30] 0 1] 0 1] +-- =+ 0 = diff --git a/pkg/proto/package.yaml b/pkg/proto/package.yaml index 8d5ab9fdb9..ab55ad876a 100644 --- a/pkg/proto/package.yaml +++ b/pkg/proto/package.yaml @@ -6,7 +6,12 @@ dependencies: - base - bound - containers + - classy-prelude + - deriving-compat + - mtl - text + - transformers + - transformers-compat - unordered-containers default-extensions: @@ -37,6 +42,7 @@ default-extensions: - RankNTypes - RecordWildCards - ScopedTypeVariables + - StandaloneDeriving - TemplateHaskell - TupleSections - TypeApplications @@ -66,7 +72,7 @@ executables: - -fwarn-incomplete-patterns tests: - proto: + proto-test: main: Spec.hs source-dirs: test dependencies: diff --git a/stack.yaml b/stack.yaml new file mode 100644 index 0000000000..f6c8e08811 --- /dev/null +++ b/stack.yaml @@ -0,0 +1,11 @@ +resolver: lts-13.10 + +packages: + - pkg/proto + +nix: + packages: + - pkgconfig + - SDL2 + - SDL2_image + - zlib