From ecaf9deb4b1d2ce85617438e621690b2df3ea367 Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown01@ed.ac.uk>
Date: Tue, 12 Nov 2024 16:44:31 +0000
Subject: Add ability to desugar terms.

Remove `getChildren` construct---it's too niche for the core language.
---
 src/Inky/Data/SnocList/Elem.idr        |  6 ++++++
 src/Inky/Data/SnocList/Quantifiers.idr |  7 +++++++
 src/Inky/Data/SnocList/Thinning.idr    | 11 +++++++++++
 3 files changed, 24 insertions(+)

(limited to 'src/Inky/Data/SnocList')

diff --git a/src/Inky/Data/SnocList/Elem.idr b/src/Inky/Data/SnocList/Elem.idr
index 465e92c..c1e69f6 100644
--- a/src/Inky/Data/SnocList/Elem.idr
+++ b/src/Inky/Data/SnocList/Elem.idr
@@ -8,6 +8,7 @@ import Data.Singleton
 import Inky.Decidable
 import Inky.Decidable.Maybe
 import Inky.Data.Assoc
+import Inky.Data.List
 import Inky.Data.SnocList
 
 export
@@ -71,6 +72,11 @@ split Z pos = Left pos
 split (S len) Here = Right Here
 split (S len) (There pos) = mapSnd There $ split len pos
 
+public export
+wknL' : Elem x sx -> LengthOf xs -> Elem x (sx <>< xs)
+wknL' i Z = i
+wknL' i (S len) = wknL' (There i) len
+
 -- Lookup ----------------------------------------------------------------------
 
 export
diff --git a/src/Inky/Data/SnocList/Quantifiers.idr b/src/Inky/Data/SnocList/Quantifiers.idr
index 73c6551..ac6287b 100644
--- a/src/Inky/Data/SnocList/Quantifiers.idr
+++ b/src/Inky/Data/SnocList/Quantifiers.idr
@@ -4,6 +4,8 @@ import public Data.SnocList.Quantifiers
 
 import Data.List.Quantifiers
 import Inky.Data.Irrelevant
+import Inky.Data.SnocList
+import Inky.Data.SnocList.Elem
 import Inky.Decidable
 
 public export
@@ -40,6 +42,11 @@ relevant : (sx : SnocList a) -> (0 prfs : All p sx) -> All (Irrelevant . p) sx
 relevant [<] _ = [<]
 relevant (sx :< x) prfs = relevant sx (tail prfs) :< Forget (head prfs)
 
+public export
+tabulate : LengthOf sx -> (forall x. Elem x sx -> p x) -> All p sx
+tabulate Z f = [<]
+tabulate (S len) f = tabulate len (f . There) :< f Here
+
 public export
 data Pairwise : (a -> a -> Type) -> SnocList a -> Type where
   Lin : Pairwise r [<]
diff --git a/src/Inky/Data/SnocList/Thinning.idr b/src/Inky/Data/SnocList/Thinning.idr
index f766069..60666d2 100644
--- a/src/Inky/Data/SnocList/Thinning.idr
+++ b/src/Inky/Data/SnocList/Thinning.idr
@@ -2,6 +2,7 @@ module Inky.Data.SnocList.Thinning
 
 import Data.DPair
 import Data.Nat
+import Inky.Data.List
 import Inky.Data.SnocList
 import Inky.Data.SnocList.Var
 import Inky.Data.SnocList.Quantifiers
@@ -96,6 +97,16 @@ prf.index ((%%) n {pos}) = irrelevantEq $ toVarCong $ toNatInjective $ prf.index
 
 -- Useful for Parsers ----------------------------------------------------------
 
+public export
+(<><) : ctx1 `Thins` ctx2 -> LengthOf bound -> ctx1 <>< bound `Thins` ctx2 <>< bound
+f <>< Z = f
+f <>< S len = Keep f <>< len
+
+public export
+dropFish : ctx1 `Thins` ctx2 -> LengthOf bound -> ctx1 `Thins` ctx2 <>< bound
+dropFish f Z = f
+dropFish f (S len) = dropFish (Drop f) len
+
 public export
 dropPos : (pos : Elem x ctx) -> dropElem ctx pos `Thins` ctx
 dropPos Here = Drop Id
-- 
cgit v1.2.3