agda/benchmark/Syntacticosmos/Eta.agda

module Eta (Gnd : Set)(U : Set)(El : U -> Set) where

open import Basics
open import Pr
open import Nom
import Kind
open Kind Gnd U El
import Cxt
open Cxt Kind
import Loc
open Loc Kind
import Term
open Term Gnd U El
import Shift
open Shift Gnd U El

data Sawn (G : Cxt)(C : Kind)(L : Loc)(R : Kind) : Kind -> Set where
  snil : Sawn G C L R R
  scons : {S T : Kind} -> Sawn G C L R (S |> T) ->
                          G [ L / Term C ]- S ->
                          Sawn G C L R T
  sarg : {A : U}{K : El A -> Kind} ->
         Sawn G C L R (Pi A K) -> (a : El A) ->
         Sawn G C L R (K a)

stitch : {G : Cxt}{C : Kind}{Z : Gnd}{L : Loc}{R S : Kind} ->
         Sawn G C L R S -> G [ L / Args C Z ]- S -> G [ L / Args C Z ]- R
stitch snil s = s
stitch (scons r s) t = stitch r (s G& t)
stitch (sarg r a) t = stitch r (a G^ t)

sawsh : {G : Cxt}{C : Kind}{L M : Loc} ->
        ({T : Kind} -> G [ L / Head ]- T -> G [ M / Head ]- T) ->
        {R S : Kind} -> Sawn G C L R S -> Sawn G C M R S
sawsh rho snil = snil
sawsh rho (scons r s) = scons (sawsh rho r) (shift rho s)
sawsh rho (sarg r a) = sarg (sawsh rho r) a

long : {G : Cxt}{C : Kind}{L : Loc}(S : Kind){T : Kind} ->
       G [ L / Head ]- T ->
       Sawn G C L T S ->
       G [ L / Term C ]- S
long (Ty Z)   h s = h G$ (stitch s Gnil)
long (Pi A K) h s = Gfn A \ a -> long (K a) h (sarg s a)
long (S |> T) h s =
  G\\ (long T (popH h) (scons (sawsh popH s) (long S (# top -! _) snil)))

var : {G : Cxt}{C : Kind}(x : Nom){Gx : [| G Has x |]} ->
      G [ EL / Term C ]- (wit ((G ?- x) {Gx}))
var {G} x {Gx} with (G ?- x) {Gx}
... | [ T / g ] = long T (` x -! g) snil