agda/benchmark/Syntacticosmos/Subst.agda

module Subst (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
import Inst
open Inst Gnd U El

data _-[_]_ : Cxt -> Kind -> Cxt -> Set where
  ES : {D : Cxt}{C : Kind} -> EC -[ C ] D
  _[_-_:=_] : {G D : Cxt}{C : Kind} -> (G -[ C ] D) ->
              (x : Nom){Gx : [| G Hasn't x |]}(S : Kind) ->
              D [! C !]- S ->
              (G [ x - S ]){Gx} -[ C ] D

fetch : {G D : Cxt}{C S : Kind} -> (G -[ C ] D) ->
        Nom :- GooN G S -> D [! C !]- S
fetch ES [ x / () ]
fetch (g [ x - S := s ]) [ y / p ] with nomEq x y
fetch (g [ x - S := s ]) [ .x / refl ] | yes refl = s
fetch (g [ x - S := s ]) [ y / p ]     | no n = fetch g [ y / p ]

closed : {G : Cxt}{L : Loc}{T : Kind} ->
         G [ EL / Head ]- T  ->  G [ L / Head ]- T
closed (` x -! xg) = ` x -! xg
closed (# () -! _)

mutual

  wsubst : {C : Kind}{G D : Cxt} -> (G -[ C ] D) ->
          {L : Loc}{T : Kind}(t : L [ Term C ]- T) -> [| Good G t |] ->
          D [ L / Term C ]- T
  wsubst g [ s ] sg = G[ wsubsts g s sg ]
  wsubst g (fn A f) fg = Gfn A \ a -> wsubst g (f a) (fg a)
  wsubst g (\\ b)    bg = G\\ (wsubst g b bg)
  wsubst g (# v $ s) pg = (# v -! _) G$ wsubsts g s (snd pg)
  wsubst g (` x $ s) pg =
    go (shift closed (fetch g [ x / fst pg ])) (wsubsts g s (snd pg))

  wsubsts : {C : Kind}{G D : Cxt} -> (G -[ C ] D) ->
           {L : Loc}{Z : Gnd}{S : Kind}
           (s : L [ Args C Z ]- S) -> [| Good G s |] ->
           D [ L / Args C Z ]- S
  wsubsts g (a ^ s)   sg = a G^ wsubsts g s sg
  wsubsts g (r & s)   pg = wsubst g r (fst pg) G& wsubsts g s (snd pg)
  wsubsts g nil       _  = Gnil

subst : {C : Kind}{G D : Cxt} -> (G -[ C ] D) ->
        {L : Loc}{T : Kind} -> G [ L / Term C ]- T -> D [ L / Term C ]- T
subst g (t -! tg) = wsubst g t tg