WIP : use smarter weakenings.better-thinning

1 files changed, 63 insertions, 0 deletions

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))