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/Container.idr | 21 +++++++++------------
 1 file changed, 9 insertions(+), 12 deletions(-)

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

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} ->
-- 
cgit v1.2.3