From 4b9b6b0211f6fb5691d67ca77ac09be888e569b7 Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown01@ed.ac.uk>
Date: Thu, 1 Feb 2024 19:25:13 +0000
Subject: Define generic syntax construction.

Whilst it works (see `Example`), a generated data type would probably
work better.
---
 src/SOAS/Var.idr | 16 ++++++++++++++--
 1 file changed, 14 insertions(+), 2 deletions(-)

(limited to 'src/SOAS/Var.idr')

diff --git a/src/SOAS/Var.idr b/src/SOAS/Var.idr
index 22e8028..8362126 100644
--- a/src/SOAS/Var.idr
+++ b/src/SOAS/Var.idr
@@ -7,7 +7,7 @@ import SOAS.Context
 import SOAS.Family
 
 prefix 4 %%
-infixr 3 ~> , ~:>
+infixr 3 ~> , ~:>, ^, ^^
 
 --------------------------------------------------------------------------------
 -- Variables
@@ -126,9 +126,13 @@ x.extend {ty} u theta = x.copair (S Z) theta (x.singleton u)
 --------------------------------------------------------------------------------
 -- Families
 
+public export 0
+(^^) : (tgt : type.Family) -> (src : type.SortedFamily) -> type.Family
+(tgt ^^ src) ctx = src.subst ctx -||> tgt
+
 public export 0
 (^) : (tgt, src : type.SortedFamily) -> type.SortedFamily
-(tgt ^ src) ty ctx = src.subst ctx -||> tgt ty
+(tgt ^ src) ty = tgt ty ^^ src
 
 public export 0
 Nil : type.SortedFamily -> type.SortedFamily
@@ -138,3 +142,11 @@ Nil f = f ^ Var
 (*) : (derivative, tangent : type.SortedFamily) -> type.SortedFamily
 (derivative * tangent) ty ctx =
   (ctx' : type.Ctx ** (derivative ty ctx' , tangent.subst ctx' ctx))
+
+--------------------------------------------------------------------------------
+-- Utilities
+
+export
+lookup : ctx.All p -> {k : Nat} -> (0 pos : ctx.varAt n k ty) -> p n ty
+lookup (sx :< px) Here = px
+lookup (sx :< px) (There v) = lookup sx v
-- 
cgit v1.2.3