diff options
| author | Greg Brown <greg.brown01@ed.ac.uk> | 2024-02-01 19:25:13 +0000 |
|---|---|---|
| committer | Greg Brown <greg.brown01@ed.ac.uk> | 2024-02-02 13:33:09 +0000 |
| commit | 4b9b6b0211f6fb5691d67ca77ac09be888e569b7 (patch) | |
| tree | 33451a63c169a06d0fee67393d0bf081f7e0b1e3 /src/SOAS/Var.idr | |
| parent | fa4de437fa3861189b506538f6ca4a39771ecbbb (diff) | |
Define generic syntax construction.main
Whilst it works (see `Example`), a generated data type would probably
work better.
Diffstat (limited to 'src/SOAS/Var.idr')
| -rw-r--r-- | src/SOAS/Var.idr | 16 |
1 files changed, 14 insertions, 2 deletions
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 @@ -127,8 +127,12 @@ 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 |