From ed7179a846a03546e4ac8a24f13b5734304a7a89 Mon Sep 17 00:00:00 2001
From: Joscha <joscha@plugh.de>
Date: Thu, 26 Nov 2020 16:07:56 +0100
Subject: [PATCH] Restructure and begin displaying lambdas

---
 app/Main.hs                 | 13 +++++++++++--
 props.cabal                 |  6 +++---
 src/Props.hs                |  4 ----
 src/Props/Lambda.hs         | 23 -----------------------
 src/Props/Lambda/Display.hs | 31 +++++++++++++++++++++++++++++++
 src/Props/Lambda/Term.hs    | 33 +++++++++++++++++++++++++++++++++
 6 files changed, 78 insertions(+), 32 deletions(-)
 delete mode 100644 src/Props.hs
 delete mode 100644 src/Props/Lambda.hs
 create mode 100644 src/Props/Lambda/Display.hs
 create mode 100644 src/Props/Lambda/Term.hs

diff --git a/app/Main.hs b/app/Main.hs
index d94efcc..3eacdac 100644
--- a/app/Main.hs
+++ b/app/Main.hs
@@ -1,6 +1,15 @@
 module Main where
 
-import           Props
+import Data.Void
+
+import Props.Lambda.Term
+
+yCombinator :: Term Void String String
+yCombinator = Lambda "f"
+  (App
+    (Lambda "x" (App (Var 1) (App (Var 0) (Var 0))))
+    (Lambda "x" (App (Var 1) (App (Var 0) (Var 0))))
+  )
 
 main :: IO ()
-main = putStrLn helloWorld
+main = print yCombinator
diff --git a/props.cabal b/props.cabal
index bc459b3..d0e1c22 100644
--- a/props.cabal
+++ b/props.cabal
@@ -4,7 +4,7 @@ cabal-version: 1.18
 --
 -- see: https://github.com/sol/hpack
 --
--- hash: 5e16e68a3016455a93f44cbee36b19144a1a414a8cb0bf4a062a1566b7119a38
+-- hash: 5a5ea1f94c0aefd4530bcfe91d7e5265b092b9e1b361d21bef695382fe4422a5
 
 name:           props
 version:        0.1.0.0
@@ -22,8 +22,8 @@ extra-doc-files:
 
 library
   exposed-modules:
-      Props
-      Props.Lambda
+      Props.Lambda.Display
+      Props.Lambda.Term
   other-modules:
       Paths_props
   hs-source-dirs:
diff --git a/src/Props.hs b/src/Props.hs
deleted file mode 100644
index 8caf1dc..0000000
--- a/src/Props.hs
+++ /dev/null
@@ -1,4 +0,0 @@
-module Props where
-
-helloWorld :: String
-helloWorld = "Hello World!"
diff --git a/src/Props/Lambda.hs b/src/Props/Lambda.hs
deleted file mode 100644
index 1b71ce6..0000000
--- a/src/Props/Lambda.hs
+++ /dev/null
@@ -1,23 +0,0 @@
-{-# LANGUAGE OverloadedStrings #-}
-
-module Props.Lambda
-  ( Term(..)
-  , displayTerm
-  ) where
-
-import qualified Data.Set  as Set
-import qualified Data.Text as T
-
-type Name = T.Text
-type PreferredName = Maybe Name
-
--- | Lambda calculus term using De Bruijn indexing
-data Term a
-  = Var PreferredName Int
-  | Lambda PreferredName (Term a)
-  | App (Term a) (Term a)
-  | Native a
-  deriving (Show)
-
-displayTerm :: (Set.Set Name -> a -> T.Text) -> Term a -> T.Text
-displayTerm = undefined
diff --git a/src/Props/Lambda/Display.hs b/src/Props/Lambda/Display.hs
new file mode 100644
index 0000000..2ed95a6
--- /dev/null
+++ b/src/Props/Lambda/Display.hs
@@ -0,0 +1,31 @@
+module Props.Lambda.Display
+  ( displayTerm
+  ) where
+
+import qualified Data.Text         as T
+
+import           Props.Lambda.Term
+
+type Name = T.Text
+
+varNames :: [Name]
+varNames = chars ++ (mappend <$> constNames <*> chars)
+  where
+    chars = map T.singleton ['a'..'z']
+
+constNames :: [Name]
+constNames = chars ++ (mappend <$> constNames <*> chars)
+  where
+    chars = map T.singleton ['A'..'Z']
+
+findConstNames :: Term e (Maybe Name) v -> Term e Name v
+findConstNames = undefined
+
+makeVarNamesUnique :: Term e c (Maybe Name) -> Term e c (Maybe Name)
+makeVarNamesUnique = undefined
+
+findVarNames :: Term e c (Maybe Name) -> Term e c Name
+findVarNames = undefined
+
+displayTerm :: (e -> T.Text) -> Term e (Maybe Name) (Maybe Name) -> T.Text
+displayTerm = undefined
diff --git a/src/Props/Lambda/Term.hs b/src/Props/Lambda/Term.hs
new file mode 100644
index 0000000..4609016
--- /dev/null
+++ b/src/Props/Lambda/Term.hs
@@ -0,0 +1,33 @@
+module Props.Lambda.Term
+  ( Term(..)
+  , vars
+  , consts
+  ) where
+
+import           Numeric.Natural
+
+-- | Lambda calculus term using De Bruijn indexing and expanded to deal with
+-- naming complexity and extensions.
+data Term e c v
+  = Var Natural
+  -- ^ Variable using a De Bruijn index
+  | Const c
+  -- ^ Constant living outside the variable namespace
+  | Lambda v (Term e c v)
+  -- ^ Lambda definition
+  | App (Term e c v) (Term e c v)
+  -- ^ Lambda application
+  | Ext e
+  -- ^ Term extension (set @e@ to 'Void' if you don't need this)
+  deriving (Show)
+
+vars :: Term e c v -> [v]
+vars (Lambda v t) = v : vars t
+vars (App l r)    = vars l <> vars r
+vars _            = []
+
+consts :: Term e c v -> [c]
+consts (Const c)    = [c]
+consts (Lambda _ t) = consts t
+consts (App l r)    = consts l <> consts r
+consts _            = []