From be8797a3ef5cbad12a6c89f2407ebad25acda25e Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Wed, 20 Sep 2023 22:09:08 +0200
Subject: [PATCH] =?UTF-8?q?untyped=20=CE=BB=20calculus=20syntax?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 lib/Quox/Untyped/Syntax.idr | 129 ++++++++++++++++++++++++++++++++++++
 lib/quox-lib.ipkg           |   3 +-
 2 files changed, 131 insertions(+), 1 deletion(-)
 create mode 100644 lib/Quox/Untyped/Syntax.idr

diff --git a/lib/Quox/Untyped/Syntax.idr b/lib/Quox/Untyped/Syntax.idr
new file mode 100644
index 0000000..14519fc
--- /dev/null
+++ b/lib/Quox/Untyped/Syntax.idr
@@ -0,0 +1,129 @@
+module Quox.Untyped.Syntax
+
+import Quox.Var
+import Quox.Context
+import Quox.Name
+import Quox.Pretty
+
+import Data.Vect
+import Data.DPair
+import Data.SortedMap
+import Derive.Prelude
+%hide TT.Name
+
+%default total
+%language ElabReflection
+
+
+public export
+data Binder = Bind BaseName
+Eq Binder where _ == _ = True
+Ord Binder where compare _ _ = EQ
+%runElab derive "Binder" [Show]
+
+public export
+data Term : Nat -> Type where
+  F : (x : Name) -> Term n
+  B : (i : Var n) -> Term n
+
+  Lam : (x : Binder) -> (body : Term (S n)) -> Term n
+  App : (fun, arg : Term n) -> Term n
+
+  Pair : (fst, snd : Term n) -> Term n
+  Fst : (pair : Term n) -> Term n
+  Snd : (pair : Term n) -> Term n
+
+  Tag : (tag : String) -> Term n
+  CaseEnum : (tag : Term n) -> (cases : List (String, Term n)) -> Term n
+
+  Zero : Term n
+  Succ : (nat : Term n) -> Term n
+  CaseNat : (nat : Term n) ->
+            (zer : Term n) ->
+            (x, ih : Binder) -> (suc : Term (2 + n)) ->
+            Term n
+
+  ||| replacement for terms of type [0.A], for now
+  ErasedBox : Term n
+%name Term s, t, u
+%runElab deriveIndexed "Term" [Eq, Ord, Show]
+
+
+public export
+0 Definitions : Type
+Definitions = SortedMap Name $ Term 0
+
+
+parameters {opts : LayoutOpts}
+  export
+  prettyBind : Binder -> Eff Pretty (Doc opts)
+  prettyBind (Bind x) = hl TVar $ text $ baseStr x
+
+  export
+  prettyTerm : Context' Binder n -> Term n -> Eff Pretty (Doc opts)
+
+  export
+  prettyArg : Context' Binder n -> Term n -> Eff Pretty (Doc opts)
+  prettyArg xs arg = withPrec Arg $ prettyTerm xs arg
+
+  export
+  prettyApp' : Context' Binder n -> Doc opts -> Term n -> Eff Pretty (Doc opts)
+  prettyApp' xs fun arg =
+    parensIfM App =<< do
+      arg <- prettyArg xs arg
+      pure $ sep [fun, arg]
+
+  export
+  prettyApp : Context' Binder n -> Term n -> Term n -> Eff Pretty (Doc opts)
+  prettyApp xs fun arg = prettyApp' xs !(prettyArg xs fun) arg
+
+  public export
+  PrettyCaseArm : Nat -> Type
+  PrettyCaseArm n = Exists $ \s => (Vect s Binder, Term (s + n))
+
+  export %inline
+  caseArm : Vect s Binder -> Term (s + n) -> PrettyCaseArm n
+  caseArm xs t = Evidence _ (xs, t)
+
+  export
+  prettyCase : Context' Binder n ->
+               (a -> Eff Pretty (Doc opts)) ->
+               Term n -> List (a, PrettyCaseArm n) ->
+               Eff Pretty (Doc opts)
+  prettyCase xs f head arms =
+    parensIfM Outer =<< Prelude.do
+      header <- hsep <$> sequence [caseD, prettyTerm xs head, ofD]
+      cases  <- for arms $ \(lhs, (Evidence s (ys, rhs))) => do
+        lhs <- hsep <$> sequence [f lhs, darrowD]
+        rhs <- withPrec Outer $ prettyTerm (xs <>< ys) rhs
+        hangDSingle lhs rhs
+      body <- braces $ separateLoose !semiD cases
+      pure $ sep [header, body]
+
+  prettyTerm _  (F x) = prettyFree x
+  prettyTerm xs (B i) = prettyBind $ xs !!! i
+  prettyTerm xs (Lam x body) =
+    parensIfM Outer =<< do
+      header <- hsep <$> sequence [lamD, prettyBind x, darrowD]
+      body   <- withPrec Outer $ prettyTerm (xs :< x) body
+      hangDSingle header body
+  prettyTerm xs (App fun arg) = prettyApp xs fun arg
+  prettyTerm xs (Pair fst snd) =
+    parens =<< separateTight !commaD <$>
+      sequence {t = List} [prettyTerm xs fst, prettyTerm xs snd]
+  prettyTerm xs (Fst pair) = prettyApp' xs !fstD pair
+  prettyTerm xs (Snd pair) = prettyApp' xs !sndD pair
+  prettyTerm xs (Tag tag) = prettyTag tag
+  prettyTerm xs (CaseEnum tag cases) = assert_total
+    prettyCase xs prettyTag tag $ map (mapSnd $ caseArm []) cases
+  prettyTerm xs Zero = zeroD
+  prettyTerm xs (Succ nat) = prettyApp' xs !succD nat
+  prettyTerm xs (CaseNat nat zer x ih suc) = assert_total
+    prettyCase xs pure nat
+      [(!zeroD,  caseArm []      zer),
+       (!sucPat, caseArm [x, ih] suc)]
+    where
+      sucPat = separateTight {t = List} !commaD <$>
+               sequence [[|succD <++> prettyBind x|], prettyBind ih]
+  prettyTerm _ ErasedBox =
+    hl Syntax =<< ifUnicode "⌷" "[]"
diff --git a/lib/quox-lib.ipkg b/lib/quox-lib.ipkg
index 7e0af1b..26d4b6f 100644
--- a/lib/quox-lib.ipkg
+++ b/lib/quox-lib.ipkg
@@ -56,4 +56,5 @@ modules =
   Quox.Parser.LoadFile,
   Quox.Parser.FromParser,
   Quox.Parser.FromParser.Error,
-  Quox.Parser
+  Quox.Parser,
+  Quox.Untyped.Syntax