From 8791efda0cf7392144117cf780bfb6d687d2da5e Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Tue, 4 Jul 2023 12:29:30 +0100
Subject: Add more built-in functions.

---
 src/Encoded/Arith.idr     | 55 +----------------------------------------------
 src/Encoded/Bool.idr      |  4 ++--
 src/Encoded/Container.idr | 21 ++++++++----------
 src/Encoded/Fin.idr       |  2 +-
 4 files changed, 13 insertions(+), 69 deletions(-)

(limited to 'src/Encoded')

diff --git a/src/Encoded/Arith.idr b/src/Encoded/Arith.idr
index fe9bc68..4dd3e10 100644
--- a/src/Encoded/Arith.idr
+++ b/src/Encoded/Arith.idr
@@ -21,48 +21,9 @@ rec = Abs $ Abs $ Abs $
   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 $ Abs $
-        let f = Var (There Here) in
-        let k = Var Here in
-        Rec k
-          (Lit 1)
-          (Const $
-            Rec (App f [<Zero])
-              Zero
-              (Const $ Suc $ App f [<Lit 1]))))
-    [<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])
+lte = Abs' (\m => isZero . App (Op Minus) [<m])
 
 export
 equal : Term (N ~> N ~> B) ctx
@@ -70,17 +31,3 @@ 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, Suc (App snd [<p])]
-        , App pair [<Suc (App fst [<p]), Zero]
-        , App mapSnd [<Abs' Suc, p]]))
diff --git a/src/Encoded/Bool.idr b/src/Encoded/Bool.idr
index 778f65d..731f45c 100644
--- a/src/Encoded/Bool.idr
+++ b/src/Encoded/Bool.idr
@@ -8,11 +8,11 @@ B = N
 
 export
 True : Term B ctx
-True = Lit 0
+True = 0
   
 export
 False : Term B ctx
-False = Lit 1
+False = 1
 
 export
 if' : Term (B ~> ty ~> ty ~> ty) ctx
diff --git a/src/Encoded/Container.idr b/src/Encoded/Container.idr
index 1334bc2..800623a 100644
--- a/src/Encoded/Container.idr
+++ b/src/Encoded/Container.idr
@@ -83,31 +83,28 @@ getFuel :
   {cont : Container} ->
   {c : Case} ->
   Term (semCase c (W cont) ~> N) ctx
-getFuel {c = (tag, k)} = App foldr [<Zero, plus] . App map [<Abs' Suc . fuel] . recurse
+getFuel {c = (tag, k)} = App foldr [<Zero, Op Plus] . App map [<Abs' Suc . fuel] . recurse
 
 -- Updates the base and stride for a single recursive position.
 -- These are multiplexed later.
 stepOffset : {k : Nat} -> Term (Fin k ~> (N ~> N * N) ~> (N ~> N * N)) ctx
-stepOffset = Abs $ Abs $ Abs $
-  let i = Var (There $ There Here) in
-  let f = Var (There Here) in
-  let x = Var Here in
+stepOffset = AbsAll [<_,_,_] (\[<i, f, x] =>
   App bimap
     -- Suc is for the initial tag
-    [<App (plus . forget . suc) [<i] . App mult [<Lit k]
-    , App mult [<Lit k]
+    [<Abs' (\n => Suc $ App forget [<shift i] + Op (Lit k) * n)
+    , Abs' (\n => Op (Lit k) * n)
     , App f [<x]
-    ]
+    ])
 
 -- Calculates all offsets for a new W value.
 getOffset :
   {cont : Container} ->
   {c : Case} ->
   Term (semCase c (W cont) ~> N ~> N * N) ctx
-getOffset {c = (tag, 0)} = Const $ Const $ App pair [<Lit 1, Zero]
+getOffset {c = (tag, 0)} = Const $ Const $ App pair [<1, 0]
 getOffset {c = (tag, k@(S _))} = Abs' (\x =>
-  App cons
-    [<App pair [<Lit 1, Zero]
+  App Container.cons
+    [<App pair [<1, 0]
     , Abs' (\n =>
       let dm = App (divmod' k) [<n] in
       let div = App fst [<dm] in
@@ -154,7 +151,7 @@ intro =
   gtabulate introCase
 
 calcIndex : Term (N * N ~> N ~> N) ctx
-calcIndex = Abs' (\bs => App (plus . fst) [<bs] . App (mult . snd) [<bs])
+calcIndex = AbsAll [<_, _] (\[<bs, n] => App fst [<bs] + App snd [<bs] * n)
 
 fillCase :
   {c : Case} ->
diff --git a/src/Encoded/Fin.idr b/src/Encoded/Fin.idr
index 0029760..3f369cf 100644
--- a/src/Encoded/Fin.idr
+++ b/src/Encoded/Fin.idr
@@ -40,4 +40,4 @@ forget = Id
 
 export
 divmod' : (k : Nat) -> {auto 0 ok : NonZero k} -> Term (N ~> N * Fin k) ctx
-divmod' k = Abs' (\n => App divmod [<n, Lit k])
+divmod' k = Abs' (\n => App pair [<n `div` Op (Lit k), n `mod` Op (Lit k)])
-- 
cgit v1.2.3