finish old cc, start new

pkg/proto/lib/Nock.hs

@@ -4,15 +4,32 @@ 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
+data Tree a  = A !a
+             | C !(Tree a) !(Tree a)
+  deriving (Eq, Ord, Read, Functor)
+
+data Fern a = FernA !a
+            | FernF [Fern a]
+
+toFern :: Tree a -> Fern a
+toFern = \case
+  A a -> FernA a
+  C h t -> case toFern t of
+    a@FernA{} -> FernF [toFern h, a]
+    FernF fs -> FernF (toFern h : fs)
+
+instance Show a => Show (Fern a) where
+  show = \case
+    FernA a -> show a
+    FernF xs -> "[" <> intercalate " " (map show xs) <> "]"
+
+instance Show a => Show (Tree a) where
+  show = show . toFern
 
 yes, no :: Noun
-yes = Atom 0
+yes = A 0
-no  = Atom 1
+no  = A 1
 
 -- | Tree address
 type Axis = Atom
@@ -31,75 +48,78 @@ data Nock = NC Nock Nock           -- ^ ^: autocons
           | N10 (Axis, Nock) Nock  -- ^ 10, edit
           | N11 Hint Nock          -- ^ 11, hint
           | N12 Nock Nock          -- ^ 12, scry
-  deriving (Eq, Ord, Read, Show)
+  deriving (Eq, Ord, Read)
 
 data Hint = Tag Atom
           | Assoc Atom Nock
   deriving (Eq, Ord, Read, Show)
 
+instance Show Nock where
+  show = show . nockToNoun
+
 nockToNoun :: Nock -> Noun
 nockToNoun = go
   where
     go = \case
-      NC f g -> Cell (go f) (go g)
+      NC f g -> C (go f) (go g)
-      N0 a -> Cell (Atom 0) (Atom a)
+      N0 a -> C (A 0) (A a)
-      N1 n -> Cell (Atom 1) n
+      N1 n -> C (A 1) n
-      N2 f g -> Cell (Atom 2) (Cell (go f) (go g))
+      N2 f g -> C (A 2) (C (go f) (go g))
-      N3 f -> Cell (Atom 3) (go f)
+      N3 f -> C (A 3) (go f)
-      N4 f -> Cell (Atom 4) (go f)
+      N4 f -> C (A 4) (go f)
-      N5 f g -> Cell (Atom 5) (Cell (go f) (go g))
+      N5 f g -> C (A 5) (C (go f) (go g))
-      N6 f g h -> Cell (Atom 5) (Cell (go f) (Cell (go g) (go h)))
+      N6 f g h -> C (A 5) (C (go f) (C (go g) (go h)))
-      N7 f g -> Cell (Atom 7) (Cell (go f) (go g))
+      N7 f g -> C (A 7) (C (go f) (go g))
-      N8 f g -> Cell (Atom 8) (Cell (go f) (go g))
+      N8 f g -> C (A 8) (C (go f) (go g))
-      N9 a f -> Cell (Atom 9) (Cell (Atom a) (go f))
+      N9 a f -> C (A 9) (C (A a) (go f))
-      N10 (a, f) g -> Cell (Atom 10) (Cell (Cell (Atom a) (go f)) (go g))
+      N10 (a, f) g -> C (A 10) (C (C (A a) (go f)) (go g))
-      N11 (Tag a) f -> Cell (Atom 11) (Cell (Atom a) (go f))
+      N11 (Tag a) f -> C (A 11) (C (A a) (go f))
-      N11 (Assoc a f) g -> Cell (Atom 11) (Cell (Cell (Atom a) (go f)) (go g))
+      N11 (Assoc a f) g -> C (A 11) (C (C (A a) (go f)) (go g))
-      N12 f g -> Cell (Atom 12) (Cell (go f) (go g))
+      N12 f g -> C (A 12) (C (go f) (go g))
 
 nounToNock :: Noun -> Nock
 nounToNock = go
   where
     go = \case
-      Atom{} -> error "nounToNock: atom"
+      A{} -> error "nounToNock: atom"
-      Cell n@Cell{} m -> NC (go n) (go m)
+      C n@C{} m -> NC (go n) (go m)
-      Cell (Atom op) n -> case op of
+      C (A op) n -> case op of
-        0  | (Atom a)                   <- n  -> N0 a
+        0  | (A a)              <- n  -> N0 a
         1                             -> N1 n
-        2  | (Cell m o)                 <- n  -> N2 (go m) (go o)
+        2  | (C 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)
+        5  | (C m o)            <- n  -> N5 (go m) (go o)
-        6  | (Cell m (Cell o p))        <- n  -> N6 (go m) (go o) (go p)
+        6  | (C m (C o p))      <- n  -> N6 (go m) (go o) (go p)
-        7  | (Cell m o)                 <- n  -> N7 (go m) (go o)
+        7  | (C m o)            <- n  -> N7 (go m) (go o)
-        8  | (Cell m o)                 <- n  -> N8 (go m) (go o)
+        8  | (C m o)            <- n  -> N8 (go m) (go o)
-        9  | (Cell (Atom a) m)          <- n  -> N9 a (go m)
+        9  | (C (A a) m)        <- n  -> N9 a (go m)
-        10 | (Cell (Cell (Atom a) m) o) <- n  -> N10 (a, (go m)) (go o)
+        10 | (C (C (A 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)
+        11 | (C (C (A a) m) o)  <- n  -> N11 (Assoc a (go m)) (go o)
-           | (Cell (Atom a) m)          <- n  -> N11 (Tag a) (go m)
+           | (C (A a) m)        <- n  -> N11 (Tag a) (go m)
-        12 | (Cell m o)                 <- n  -> N12 (go m) (go o)
+        12 | (C 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)
+  NC f g -> C (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
+    C{} -> yes
-    Atom{} -> no
+    A{} -> no
   N4 f -> case nock n f of
-    Cell{} -> error "nock: cannot increment cell"
+    C{} -> error "nock: cannot increment cell"
-    Atom a -> Atom (a + 1)
+    A a -> A (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
+    (A 0) -> nock n g
-    (Atom 1) -> nock n h
+    (A 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
+  N8 f g -> nock (C (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
@@ -148,7 +168,7 @@ peg a = \case
 
 axis :: Axis -> Tree a -> Tree a
 axis 1 n = n
-axis (capMas -> (d, r)) (Cell n m) = case d of
+axis (capMas -> (d, r)) (C n m) = case d of
   L -> axis r n
   R -> axis r m
 axis a n = error ("bad axis: " ++ show a)

pkg/proto/lib/UntypedLambda.hs

@@ -3,11 +3,16 @@ module UntypedLambda where
 import ClassyPrelude
 
 import Bound
-import Data.Deriving (deriveEq1, deriveOrd1, deriveRead1, deriveShow1)
 import Control.Monad.State
+import Data.Deriving (deriveEq1, deriveOrd1, deriveRead1, deriveShow1)
+import Data.List (elemIndex)
+import Data.Maybe (fromJust)
+import Data.Void
 
 import Nock
 
+type Nat = Int
+
 data Exp a
   = Var a
   | App (Exp a) (Exp a)
@@ -36,13 +41,106 @@ eval = \case
     (Lam s) -> instantiate1 (eval f) s
     e' -> (App e' (eval f))
 
-newtype Ref = Ref { unRef :: Int }
+-- 6, 30, 126, 510, ...
+oldDeBruijn :: Nat -> Axis
+oldDeBruijn = toAxis . go
+  where
+    go = \case
+      0 -> [R,L]
+      n -> [R,R] ++ go (n - 1)
 
-nextRef :: Ref -> Ref
+-- | Raw de Bruijn
-nextRef = Ref . (+ 1) . unRef
+data Exp'
+  = Var' Nat
+  | App' Exp' Exp'
+  | Lam' Exp'
+  deriving (Eq, Ord, Read, Show)
 
+toExp' :: Exp a -> Exp'
+toExp' = go \v -> error "toExp': free variable"
+  where
+    go :: (a -> Nat) -> Exp a -> Exp'
+    go env = \case
+      Var v   -> Var' (env v)
+      App e f -> App' (go env e) (go env f)
+      Lam s   -> Lam' (go env' (fromScope s))
+        where
+          env' = \case
+            B () -> 0
+            F v  -> 1 + env v
+
+-- | The old calling convention; i.e., what the (%-, |=) sublanguage of hoon
+-- compiles to
 old :: Exp a -> Nock
-old = undefined
+old = go \v -> error "old: free variable"
+  where
+    go :: (a -> Path) -> Exp a -> Nock
+    go env = \case
+      Var v   -> N0 (toAxis (env v))
+      App e f -> app (go env e) (go (\v -> R : env v) f)
+      Lam s   -> lam (nockToNoun (go env' (fromScope s)))
+        where
+          env' = \case
+            B () -> [R,L]
+            F v  -> [R,R] ++ env v
+    app ef ff =
+      N8
+        ef  -- =+ callee so we don't modify the orig's bunt
+        (N9 2
+          (N10 (6, ff)
+            (N0 2)))
+    lam ff =
+      N8  -- pushes onto the context
+        (N1 (A 0))  -- a bunt value (in hoon, actually depends on type)
+        (NC  -- then conses (N8 would also work, but hoon doesn't)
+          (N1 ff)  -- the battery (nock code)
+          (N0 1))  -- onto the pair of bunt and context
+
+data CopyVar
+  = Argument
+  | Lexical Nat
+
+data CopyExp
+  = CVar CopyVar
+  | CApp CopyExp CopyExp
+  | CLam [CopyVar] CopyExp
+
+toCopy :: forall a. Ord a => Exp a -> CopyExp
+toCopy = fst . go \v -> error "toCopy: free variable"
+  where
+    go :: (a -> CopyVar) -> Exp a -> (CopyExp, Set a)
+    go env = \case
+      Var v -> (CVar (env v), singleton v)
+      App e f -> (CApp ec fc, union eu fu)
+        where
+          (ec, eu) = go env e
+          (fc, fu) = go env f
+      Lam s -> (CLam (map env u) c, fromList u)
+        where
+          c :: CopyExp
+          (c, u') = go env' (fromScope s)
+          env' :: Var () a -> CopyVar
+          env' = \case
+            B () -> Argument
+            F v  -> Lexical (fromJust (elemIndex v u))
+          u = mapMaybe pred (toList u')
+          pred = \case
+            B () -> Nothing
+            F v  -> Just v
+
+copyToNock :: CopyExp -> Nock
+copyToNock = \case
+  CVar v -> toAxis case v of
+    Argument -> [R]
+    Lexical n -> L : repeat n R ++ L
+  CApp e f -> N2 (copyToNock f) (copyToNock e)
+
+-- | The proposed new calling convention
+new :: Exp a -> Nock
+new = go \v -> error "new: free variable"
+  where
+    go = undefined
+
 
 
 -- x. y. x