From cedc6109895a53ce6ed667e0391b232bf5463387 Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Thu, 15 Jun 2023 16:09:42 +0100
Subject: WIP : use smarter weakenings.

---
 src/Total/Encoded/Test.idr | 63 ++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 63 insertions(+)
 create mode 100644 src/Total/Encoded/Test.idr

(limited to 'src/Total/Encoded')

diff --git a/src/Total/Encoded/Test.idr b/src/Total/Encoded/Test.idr
new file mode 100644
index 0000000..cf5aa8e
--- /dev/null
+++ b/src/Total/Encoded/Test.idr
@@ -0,0 +1,63 @@
+module Total.Encoded.Test
+
+import Total.NormalForm
+import Total.Pretty
+import Total.Encoded.Util
+
+namespace List
+  ListC : Container
+  ListC = (Unit, 0) ::: [(N, 1)]
+
+  export
+  List : Ty
+  List = fix ListC
+
+  export
+  nil : FullTerm List [<]
+  nil = app (intro {c = ListC} Here) (app' pair [<arb, Pair.nil])
+
+  export
+  cons : FullTerm (N ~> List ~> List) [<]
+  cons = abs' (S $ S Z)
+    (\t, ts =>
+      app (lift $ intro {c = ListC} $ There Here)
+        (app' (lift pair)
+          [<t
+          , app' (lift Pair.cons) [<ts, lift Pair.nil]
+          ]))
+
+  export
+  fold : {ty : Ty} -> FullTerm ((N ~> ty ~> ty) ~> ty ~> List ~> ty) [<]
+  fold = abs' (S $ S Z)
+    (\f, z => elim
+      [ abs (drop z)
+      , abs' (S Z) (\p =>
+        app' (drop f)
+          [<app (lift $ fst {u = Vect 1 ty}) p
+          , app (lift (index {n = 1} FZ . snd {t = N})) p
+          ])
+      ])
+
+MkList : List Nat -> FullTerm List [<]
+MkList = foldr (\n, ts => app' cons [<lit n, ts]) nil
+
+sum : FullTerm (List ~> N) [<]
+sum = app' fold [<add, zero]
+
+ten : FullTerm N [<]
+ten = (app sum (MkList [1,2,3,4]))
+
+tenNf : Term [<] N
+tenNf = toTerm (normalize ten).term
+
+main : IO Builtin.Unit
+main = do
+  let
+    cases =
+      [(lit 1, id)
+      ,(lit 3, abs' (S Z) (\n => app' (lift add) [<n, n]))
+      ,(lit 2, abs' (S Z) (\n => app (lift pred) n))]
+  let t : FullTerm (N ~> N) [<] = cond cases
+  -- let t : FullTerm N [<] = app sum (MkList [1,2,3,4])
+  putDoc (group $ Doc.pretty "Input:" <+> line <+> pretty (toTerm t))
+  putDoc (group $ Doc.pretty "Normal Form:" <+> line <+> pretty (toTerm (normalize t).term))
-- 
cgit v1.2.3