Norms.hs

{-# LANGUAGE DeriveFunctor, PatternSynonyms #-}

module Norms where

import Control.Monad

data Nm
  = C (Can Nm)  -- canonical construction
  | F Nm [Nm]   -- abstraction with incomplete environment
  | Ne :! Cop   -- neutral, via compositional operator (arrow, if you like)
  deriving (Show, Eq)

infixl 4 :!

eval :: [Nm] -> Nm -> Nm
eval g (C cn)    = C (fmap (eval g) cn)
eval g (F b [])  = F b g
eval g (e :! c)  = run g e -! cop g c

data Can t
  = Set | Pi t t | Nat | Inx t :% t
  | Ze | Su t | Em | Pa t t | Va t | Ap t t | La t
  -- the following must be banished by quote
  | Io t
  | Kf t    -- K t is the constant function returning t
  deriving (Show, Eq, Functor)

data Inx t
  = Fin | Tm | Env t
  deriving (Show, Eq, Functor)

pattern SET     = C Set
pattern PI s t  = C (Pi s t)
pattern NAT     = C Nat
pattern FIN n   = C (Fin :% n)
pattern TM n    = C (Tm :% n)
pattern ENV t n = C (Env t :% n)
pattern SUB n m = ENV (TM m) n
pattern ZE      = C Ze
pattern SU n    = C (Su n)
pattern EM      = C Em
pattern s :& t  = C (Pa s t)
pattern IO t    = C (Io t)
pattern VA i    = C (Va i)
pattern AP f s  = C (Ap f s)
pattern LA t    = C (La t)
pattern K t     = C (Kf t)

arr :: Nm -> Nm -> Nm
arr s t = PI s (K t)

data Cop       -- identity, thinning, substitution
  = Id
  | Ma Cop     -- could be thinning, weakening, or mapping
  | Sh Cop     -- postcomposition with SU; never at the top in a normal form
  | Sb Nm Nm   -- target scope, environment
  deriving (Show, Eq)

-- smart map absorbs identity
sMa :: Cop -> Cop
sMa Id = Id
sMa c  = Ma c

sSb :: Nm -> Nm -> Cop
sSb n (IO _) = Id
sSb n sg     = case mkThin n 0 sg of
  Just rh -> Ma rh
  Nothing -> Sb n sg

mkThin :: Nm -> Int -> Nm -> Maybe Cop
mkThin m x (yz :& VA y) = do
      y <- mkNum y
      guard (y >= x)
      c <- mkThin m (y+1) yz
      return (iterate Sh (sMa c) !! (y - x))
mkThin (SU m) x EM = Sh <$> mkThin m x EM
mkThin ZE x EM = return Id
mkThin _ 0 (e :$ IdSub :! Id) = return Id
mkThin _ 0 (e :$ IdSub :! Ma Id) = return Id
mkThin _ 0 (e :$ IdSub :! Ma (Ma c)) = return c
mkThin m x (e :$ IdSub :! Ma (Ma (Sh c))) = mkThin m (x - 1) (e :$ IdSub :! sMa (sMa c))
mkThin _ _ _ = Nothing
mkNum :: Nm -> Maybe Int
mkNum ZE = Just 0
mkNum (SU x) = (1+) <$> mkNum x
mkNum _ = Nothing
    
-- eval for Cop pushes structurally
cop :: [Nm] -> Cop -> Cop
cop g Id       = Id
cop g (Ma c)   = sMa (cop g c)
cop g (Sh c)   = Sh (cop g c)
cop g (Sb n s) = sSb (eval g n) (eval g s)
-- but could potentially try to turn substitutions into renamings;
-- not doing so is a potential completeness hole

-- thinning then substitution
(<?) :: Cop -> Nm -> Nm
Id   <? xz = xz
Ma c <? xz = (c <? (xz -$ Pop)) :& (xz -$ Top)
Sh c <? xz = c <? (xz -$ Pop)

-- compositional operators are ... compositional
(>->) :: Cop -> Cop -> Cop
Id      >-> d = d
c       >-> Id = c
Ma c    >-> Ma d = sMa (c >-> d)
c       >-> Sh d = Sh (c >-> d)
Sh c    >-> Ma d = Sh (c >-> d)
Sb n sg >-> d = Sb (cod n d) (sg -! sMa d) where -- we know d isn't Id
  cod n Id = n
  cod n (Ma d)   = rod n d
  cod n (Sb m _) = m
  rod n Id = n
  rod (SU n) (Ma d) = SU (rod n d)
  rod n (Sh d) = SU (rod n d)
Ma c >-> Sb n sg = sSb n (c <? sg)

-- weakening of substitutions is a mere macro
wkSub :: Nm -> Nm
wkSub (IO n) = IO (SU n)
wkSub sg = (sg -! Ma (Ma (Sh Id))) :& VA ZE
-- note (further down) that it preserves identity by definition
-- but must check it preserves composition

infixl 4 -!

-- here's where identity substitution precomposes
-- (-$!) :: Ne -> Cop -> Nm
-- e :$ IdSub -$! Ma (Sb _ sg) = sg
-- e -$! c = e :! c


-- now let's make compositional operators act
(-!) :: Nm -> Cop -> Nm

-- yer main man
(e :! c) -! d = e :! (c >-> d)

-- some basics
t -! Id = t
i -! Sh c = SU (i -! c)

-- mapping a compositional operator over an environment
EM        -! Ma c = EM
(xz :& x) -! Ma c = (xz -! Ma c) :& (x -! c)
IO n      -! Ma Id = IO n
IO n      -! Ma (Ma Id) = IO n
IO n      -! Ma (Sb _ sg) = sg
IO n      -! Ma (Ma c) = go n c where
  go ZE _ = EM
  go (SU n) c = go n (Sh c) :& VA (n -! c)
  go (e :! Id) c = e :$ IdSub :! Ma (Ma c)
  
-- weakening a thinning on a variable
ZE   -! Ma c = ZE
SU i -! Ma c = SU (i -! c)

-- hitting a term with a thinning
VA i    -! Ma c = VA (i -! c)
AP f s  -! Ma c = AP (f -! Ma c) (s -! Ma c)
LA t    -! Ma c = LA (t -! Ma (Ma c))

-- hitting a term with a substitution
VA i     -! Sb n sg     = i -$ Get (TM n) sg
AP f s   -! c@(Sb n sg) = AP (f -! c) (s -! c)
LA t     -! Sb n sg     = LA (t -! sSb (SU n) (wkSub sg))

newtype Hide x = Hide x
instance Show (Hide x) where
  show _ = ""
instance Eq (Hide x) where
  _ == _ = True

data Ne
  = V Int               -- de Bruijn index
  | P Int (Hide Nm)     -- de Bruijn level, cacheing its type
  | Ne :$ Op Nm         -- basic elimination
  | Nm ::: Nm           -- type annotation
  deriving (Show, Eq)

infixl 4 :$

run :: [Nm] -> Ne -> Nm
run g (V i)     = g !! i
run g p@(P x s) = p :! Id
run g (e :$ o)  = run g e -$ fmap (eval g) o
run g (t ::: _) = eval g t

data Op t
  = A t        -- application
  | Top        -- top projection
  | Pop        -- top deletion
  | Get t t    -- target type, environment
  | IdSub      -- identity substitution of a given size
  deriving (Show, Eq, Functor)

infixl 4 -$

-- here's how these things actually work
(-$) :: Nm -> Op Nm -> Nm

(e :! Id) -$ o = (e :$ o) :! Id -- nothing in the way of staying stuck

-- applying functions
F b g    -$ A s = eval (s : g) b
K t      -$ A _ = t

-- projecting from environments
(tz :& t) -$ Top = t
(tz :& t) -$ Pop = tz
IO (SU _) -$ Top = VA ZE
IO (SU n) -$ Pop = IO n -! Ma (Ma (Sh Id))

-- pulling mapping out through projection
(e :! Ma c) -$ Top = e :$ Top :! Id -! c
(e :! Ma c) -$ Pop = e :$ Pop :! Id -! Ma c

-- projection from environments
i        -$ Get _ (IO _) = i
i        -$ Get t (e :! Ma c) = (i -$ Get s (e :! Id)) -! c
  where ENV s _ = syn e
ZE       -$ Get t xz = xz -$ Top
SU i     -$ Get t xz = i -$ Get t (xz -$ Pop)
(e :! c) -$ Get t xz = (e :$ Get t (c <? xz)) :! Id

-- identity substitution
n -$ IdSub = IO n

-- quote (root, level) turns every P that's at least the root back into a V
quote :: (Int, Int) -> Nm -> Nm -> Nm

-- quoting types
quote rl SET SET = SET
quote rl@(r, l) SET (PI s t) =
  PI (quote rl SET s)
     (F (quote (r, 1+l) SET (t -$ A (P l (Hide s) :! Id))) [])
quote rl SET NAT = NAT
quote rl SET (C (f :% n)) = C $ fmap (quote rl SET) f :% quote rl NAT n

-- quoting functions
quote rl@(r, l) (PI s t) f = F (quote (r, 1+l) (t -$ A x) (f -$ A x)) [] where
  x = P l (Hide s) :! Id

-- quoting natural numbers
quote rl NAT ZE = ZE
quote rl NAT (SU n) = C $ Su (quote rl NAT n)

-- quoting object variables
quote rl (FIN (SU n)) ZE = ZE
quote rl (FIN (SU n)) (SU i) = SU (quote rl (FIN n) i)
quote rl (FIN _) (e :! c) = quone rl e :! c

-- quoting object terms
quote rl (TM n) (VA i) = VA (quote rl (FIN n) i)
quote rl t@(TM _) (AP f s) = AP (quote rl t f) (quote rl t s)
quote rl (TM n) (LA t) = LA (quote rl (TM (SU n)) t)

-- quoting environments, expanding them
quote rl (ENV t ZE)     _ = EM
quote rl (ENV t (SU n)) g = 
  quote rl (ENV t n) (g -$ Pop) :& quote rl t (g -$ Top)
quote el (ENV _ (e :! Id)) (IO _) = e :$ IdSub :! Id

-- quoting the identity substitution composed (can this happen?)
quote rl (ENV t n) (e :$ IdSub :! Ma (Sb _ sg)) =
  quote rl (ENV t n) sg

-- quoting an environment, simplifying its compositional operator
quote rl (ENV t n) (e :! Ma c) = case quoneSyn rl e of
  (e, ENV s _) -> e :! sMa (go s t c) where
    go _ _ Id = Id
    go (ENV s _) (ENV t _) (Ma c) = sMa (go s t c)
    go (FIN (SU m)) (FIN (SU n)) (Ma c) = sMa (go (FIN m) (FIN n) c)
    go (TM m) (TM n) c = quosub rl m n c
    go (FIN m) (FIN (SU n)) (Sh c) = Sh (go (FIN m) (FIN n) c)

-- quoting a term, simplifying its compositional operator
quote rl (TM n) (e :! c) = case quoneSyn rl e of
  (e, TM m) -> e :! quosub rl m n c

-- quoting an unmapped thing is dull
quote rl _ (e :! Id) = quone rl e :! Id

-- this shouldn't happen for well typed things
quote rl t s = error ("QUOTE: " ++ show t ++ " :> " ++ show s)

-- quoting the terms embedded in a compositional operator
quosub :: (Int, Int) -> Nm -> Nm -> Cop -> Cop
quosub rl _ _ Id = Id
quosub rl m n (Sb _ tz) = sSb (quote rl NAT n) (quote rl (SUB m n) tz)
quosub rl m n (Ma c) = sMa c
quosub rl m n c =
  error ("QUOSUB: " ++ show m ++ " " ++ show n ++ " " ++ show c)

-- yer actual definitional equality
eq :: (Int, Int) -> Nm -> Nm -> Nm -> Bool
eq (_, l) ty s t = quote (l, l) ty s == quote (l, l) ty t

-- type reconstruction
syn :: Ne -> Nm
syn (P _ (Hide s)) = s
syn (e :$ o) = case (syn e, o) of
  (PI _ t,         A v)  -> t -$ A v
  (ENV t (SU n),   Top)  -> t
  (ENV t (SU n),   Pop)  -> ENV t n
  (NAT,          IdSub)  -> SUB (e :! Id) (e :! Id)
  (FIN n,     Get t vz)  -> t

-- quotation of neutrals
quone :: (Int, Int) -> Ne -> Ne
quone (r, l) (P k s)
  | k >= r = V (l - k - 1)
  | otherwise = P k s
quone rl (e :$ o) = case (quone rl e, syn e, o) of
  (e, PI s t,         A v)  -> e :$ A (quote rl s v)
  (e, ENV t (SU n),   Top)  -> e :$ Top
  (e, ENV t (SU n),   Pop)  -> e :$ Pop
  (e, NAT,          IdSub)  -> e :$ IdSub
  (e, FIN n,     Get t vz)  -> e :$ Get (quote rl SET t) (quote rl (ENV t n) vz)
  bad -> error ("QUONE: " ++ show bad)

-- quotation with type synthesis
quoneSyn :: (Int, Int) -> Ne -> (Ne, Nm)
quoneSyn rl e = (quone rl e, syn e)

-- test stuff

i <:> t = P i (Hide t) :! Id

n = 0 <:> NAT
m = 1 <:> NAT
sg = 2 <:> SUB n m
t = 3 <:> TM n
wt = t -! Ma (Sh Id)
wsg = wkSub sg
w'tsg = (t -! Sb m sg) -! Ma (Sh Id)
wtwsg = wt -! Sb (SU m) wsg

-- quote (4, 4) (TM (SU m)) w'tsg == quote (4, 4) (TM (SU m)) wtwsg

myv = 4 <:> FIN (SU (SU n))