agda/benchmark/Syntacticosmos/Shift.agda

module Shift (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

popH : {D : Cxt}{M : Loc}{S T : Kind} ->
       D [ M / Head ]- T -> D [ M * S / Head ]- T
popH ( ` x -! xg )  = ` x -! xg
popH ( # v -! _ )   = # (pop v) -! _

weak : {G D : Cxt}{L M : Loc}{S : Kind} ->
       ({T : Kind} -> G [ L / Head ]- T -> D [ M / Head ]- T) ->
       {T : Kind} -> G [ L * S / Head ]- T -> D [ M * S / Head ]- T
weak rho (` x -! p )        = popH (rho (` x -! p))
weak rho (# top -! _ )      = # top -! _
weak rho (# (pop v) -! _ )  = popH (rho (# v -! _))

shift : {G D : Cxt}{L M : Loc} ->
  ({T : Kind} -> G [ L / Head ]- T -> D [ M / Head ]- T) ->
  {j : Jud}{T : Kind} -> G [ L / j ]- T  ->  D [ M / j ]- T
shift {G} {D} rho (t -! tg) = chug rho t tg where
  chug : {j : Jud}{L M : Loc} ->
    ({T : Kind} -> G [ L / Head ]- T -> D [ M / Head ]- T) ->
    {T : Kind}(t : L [ j ]- T) -> [| Good G t |] ->  D [ M / j ]- T
  chug {Head} rho h hg = rho ( h -! hg )
  chug rho [ s ] sg = G[ chug rho s sg ]
  chug rho (fn A f) fg = Gfn A (\ a -> chug rho (f a) (fg a))
  chug rho (\\ b) bg = G\\ (chug (weak rho) b bg)
  chug rho (a ^ s) sg = a G^ chug rho s sg
  chug rho (r & s) rsg = chug rho r (fst rsg) G& chug rho s (snd rsg)
  chug rho nil _ = Gnil
  chug rho (h $ s) hsg = chug rho h (fst hsg) G$ chug rho s (snd hsg)

bind : {G : Cxt}(x : Nom){Gx : [| G Hasn't x |]}{S : Kind}{j : Jud}{T : Kind} ->
       (G [ x - S ]) {Gx} [ EL / j ]- T -> G [ EL * S / j ]- T
bind {G} x {Gx}{S} = shift topx where
  topx : {T : Kind} -> (G [ x - S ]) {Gx} [ EL / Head ]- T ->
         G [ EL * S / Head ]- T
  topx (` y -! yg) with nomEq x y
  topx (` .x -! refl) | yes refl = # top -! _
  topx (` y -! yg)    | no _     = ` y -! yg
  topx (# () -! _)