From 0ddaf1b2c9ca66cf0ae03d2f6ad792c7885dfc32 Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Wed, 21 Jun 2023 16:05:44 +0100
Subject: Add sums, vectors and arithmetic encodings.

Also define pretty printing of terms.
---
 src/Encoded/Arith.idr | 81 +++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 81 insertions(+)
 create mode 100644 src/Encoded/Arith.idr

(limited to 'src/Encoded/Arith.idr')

diff --git a/src/Encoded/Arith.idr b/src/Encoded/Arith.idr
new file mode 100644
index 0000000..d2f83bc
--- /dev/null
+++ b/src/Encoded/Arith.idr
@@ -0,0 +1,81 @@
+module Encoded.Arith
+
+import Encoded.Bool
+import Encoded.Pair
+import Term.Syntax
+
+export
+rec : {ty : Ty} -> Term (N ~> ty ~> (N * ty ~> ty) ~> ty) ctx
+rec = Abs $ Abs $ Abs $
+  let n = Var $ There $ There Here in
+  let z = Var $ There Here in
+  let s = Var Here in
+  let 
+    p : Term (N * ty) (ctx :< N :< ty :< (N * ty ~> ty))
+    p = Rec n
+      (App pair [<Zero, z])
+      (Abs' (\p =>
+        App pair
+          [<Suc (App fst [<p])
+          , App (shift s) [<p]]))
+  in
+  App snd [<p]
+
+export
+plus : Term (N ~> N ~> N) ctx
+plus = Abs' (\n => Rec n Id (Abs' (Abs' Suc .)))
+
+export
+pred : Term (N ~> N) ctx
+-- pred = Abs' (\n => App rec [<n, Zero, fst])
+pred = Abs'
+  (\n => App
+    (Rec n
+      (Const Zero)
+      (Abs' (\f =>
+        Rec (App f [<Zero])
+          (Abs' (\k => Rec k (Suc Zero) (Const Zero)))
+          (Const $ Abs' (\k => Rec k (Suc Zero) (Abs' Suc . shift f))))))
+    [<Lit 1])
+
+export
+minus : Term (N ~> N ~> N) ctx
+minus = Abs $ Abs $
+  let m = Var $ There Here in
+  let n = Var Here in
+  Rec n m pred
+
+export
+mult : Term (N ~> N ~> N) ctx
+mult = Abs' (\n =>
+  Rec n
+    (Const Zero)
+    (Abs $ Abs $
+      let f = Var $ There Here in
+      let m = Var Here in
+      App plus [<m, App f [<m]]))
+
+export
+lte : Term (N ~> N ~> B) ctx
+lte = Abs' (\m => isZero . App minus [<m])
+
+export
+equal : Term (N ~> N ~> B) ctx
+equal = Abs $ Abs $
+  let m = Var $ There Here in
+  let n = Var Here in
+  App and [<App lte [<m, n], App lte [<n, m]]
+
+export
+divmod : Term (N ~> N ~> N * N) ctx
+divmod = Abs $ Abs $
+  let n = Var (There Here) in
+  let d = Var Here in
+  Rec
+    n
+    (App pair [<Zero, Zero])
+    (Abs' (\p =>
+      App if'
+        [<App lte [<shift d, App snd [<p]]
+        , App pair [<Suc (App fst [<p]), Zero]
+        , App mapSnd [<Abs' Suc, p]]))
-- 
cgit v1.2.3