From 4bf2172d00ce880a372e4385419465c8845e4749 Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown01@ed.ac.uk>
Date: Tue, 22 Nov 2022 18:56:04 +0000
Subject: Add more operations for dependent product.

---
 src/Soat/Data/Product.idr | 29 +++++++++++++++++++++++++----
 1 file changed, 25 insertions(+), 4 deletions(-)

diff --git a/src/Soat/Data/Product.idr b/src/Soat/Data/Product.idr
index 4f6ac34..4604300 100644
--- a/src/Soat/Data/Product.idr
+++ b/src/Soat/Data/Product.idr
@@ -1,10 +1,12 @@
 module Soat.Data.Product
 
 import Control.Relation
+import Data.List.Elem
 
 %default total
 
 infix 10 ^
+infix 5 ++
 
 -- Definitions
 
@@ -25,12 +27,14 @@ uncurry : map x is `ary` a -> x ^ is -> a
 uncurry f []        = f
 uncurry f (x :: xs) = uncurry (f x) xs
 
--- Operations
+-- Constructors
 
 public export
-map : (f : (i : a) -> x i -> y i) -> {is : List a} -> x ^ is -> y ^ is
-map f []        = []
-map f (x :: xs) = f _ x :: map f xs
+tabulate : {is : List a} -> ({i : a} -> Elem i is -> x i) -> x ^ is
+tabulate {is = []}        f = []
+tabulate {is = (i :: is)} f = f Here :: tabulate (f . There)
+
+-- Destructors
 
 public export
 head : x ^ (i :: is) -> x i
@@ -44,6 +48,23 @@ public export
 consHeadTail : (xs : x ^ (i :: is)) -> head xs :: tail xs = xs
 consHeadTail (x :: xs) = Refl
 
+public export
+index : x ^ is -> Elem i is -> x i
+index xs Here         = head xs
+index xs (There elem) = index (tail xs) elem
+
+-- Operations
+
+public export
+map : (f : (i : a) -> x i -> y i) -> {is : List a} -> x ^ is -> y ^ is
+map f []        = []
+map f (x :: xs) = f _ x :: map f xs
+
+public export
+(++) : x ^ is -> x ^ js -> x ^ (is ++ js)
+(++) []        ys = ys
+(++) (x :: xs) ys = x :: (xs ++ ys)
+
 -- Relations
 
 namespace Pointwise
-- 
cgit v1.2.3