# LANGUAGE TupleSections #
module CTT where

import Control.Applicative
import Data.List
import Data.Maybe
import Pretty

--------------------------------------------------------------------------------
-- | Terms

data Loc = Loc { locFile :: String
               , locPos :: (Int, Int) }
  deriving Eq

type Ident  = String
type Label  = String
type Binder = (Ident,Loc)

noLoc :: String -> Binder
noLoc x = (x, Loc "" (0,0))

-- Branch of the form: c x1 .. xn -> e
type Brc    = (Label,([Binder],Ter))

  Telescope ( x1 : A1 ) .. ( xn : An )
type Tele   = [(Binder,Ter)]

-- Labelled sum: c (x1 : A1) .. (xn : An)
type LblSum = [(Binder,Tele)]

-- Context gives type values to identifiers
type Ctxt   = [(Binder,Val)]

-- Mutual recursive definitions: (x1 : A1) .. (xn : An) and x1 = e1 .. xn = en
type Decls  = [(Binder,Ter,Ter)]
data ODecls = ODecls Decls
            | Opaque Binder
            | Transp Binder
  deriving (Eq,Show)

declIdents :: Decls -> [Ident]
declIdents decl = [ x | ((x,_),_,_) <- decl]

declBinders :: Decls -> [Binder]
declBinders decl = [ x | (x,_,_) <- decl]

declTers :: Decls -> [Ter]
declTers decl = [ d | (_,_,d) <- decl]

declTele :: Decls -> Tele
declTele decl = [ (x,t) | (x,t,_) <- decl]

declDefs :: Decls -> [(Binder,Ter)]
declDefs decl = [ (x,d) | (x,_,d) <- decl]

-- Terms
data Ter = App Ter Ter
         | Pi Ter Ter
         | Lam Binder Ter
         | Sigma Ter Ter
         | SPair Ter Ter
         | Fst Ter
         | Snd Ter
         | Where Ter ODecls
         | Var Ident
         | U
         -- constructor c Ms
         | Con Label [Ter]
         -- branches c1 xs1  -> M1,..., cn xsn -> Mn
         | Split Loc [Brc]
  labelled sum c1 A1s , ... , cn Ans ( assumes terms are constructors )
         | Sum Binder LblSum
         | PN PN
  deriving Eq

-- Primitive notions
data PN = Id | Refl
        -- Inh A is an h-prop stating that A is inhabited.
        -- Here we take h-prop A as (Pi x y : A) Id A x y.
        | Inh
        -- Inc a : Inh A for a:A (A not needed ??)
        | Inc
  Squash a b : I d ( Inh A ) a b
        | Squash
  InhRec B p phi a : B ,
  p :  ) ,  : A - > B , a : Inh A ( cf . HoTT - book p.113 )
        | InhRec

        -- (A B : U) -> Id U A B -> A -> B
        -- For TransU we only need the eqproof and the element in A is needed
        | TransU

        -- (A B : U) -> Id U A B -> B -> A
        -- For TransU we only need the eqproof and the element in A is needed
        | TransInvU

  ( A : U ) - > ( a : A ) - > I d A a ( transport A ( refl U A ) a )
        | TransURef

        -- (A : U) (a b:A) (p:Id A a b) -> Id (singl A a) (pair a (refl A a)) (pair b p)
        | CSingl

        -- (A B : U) (f : A -> B) (a b : A) ->
        -- (p : Id A a b) -> Id B (f a) (f b)
        -- TODO: remove?
        | MapOnPath

        -- (A B : U) (f g : A -> B) (a b : A) ->
        -- Id (A->B) f g -> Id A a b -> Id B (f a) (g b)
        | AppOnPath

  Ext B f g p : I d ( Pi A B ) f g ,
  ( p : ( Pi x : A ) I d ( Bx ) ( fx , gx ) ) ; A not needed ? ?
        -- | Ext

  Ext B f g p : I d ( Pi A B ) f g ,
        -- (p : (Pi x y:A) IdS A (Bx) x y p fx gy)
        | HExt

  EquivEq A B f s t where
        -- A, B are types, f : A -> B,
        -- s : (y : B) -> fiber f y, and
  t : ( y : B ) ( z : fiber f y ) - > I d ( fiber f y ) ( s y ) z
  where fiber f y is Sigma x : A. I d B ( f x ) 
        | EquivEq
        -- (A : U) -> (s : (y : A) -> pathTo A a) ->
        -- (t : (y : B) -> (v : pathTo A a) -> Id (path To A a) (s y) v) ->
  I d ( I d U A A ) ( refl U A ) ( equivEq A A ( i d A ) s t )
        | EquivEqRef

        -- (A B : U) -> (f : A -> B) (s : (y : B) -> fiber A B f y) ->
        -- (t : (y : B) -> (v : fiber A B f y) -> Id (fiber A B f y) (s y) v) ->
        -- (a : A) -> Id B (f a) (transport A B (equivEq A B f s t) a)
        | TransUEquivEq

  IdP   :     ( A B : U ) - > I d U A B - >   A - > B - > U
  IdP A B p a b    is the type of paths   connecting a to b over p
        | IdP

        -- mapOnPathD :  (A : U) (F : A -> U) (f : (x : A) -> F x) (a0 a1 : A) (p : Id A a0 a1) ->
        --               IdS A F a0 a1 p  (f a0) (f a1)
  IdS : ( A : U ) ( F : A - > U ) ( a0 a1 : A ) ( p :     ) - > F a0 - > F a1 - > U
        -- IdS A F a0 a1 p = IdP (F a0) (F a1) (mapOnPath A U F a0 a1 p)
        -- TODO: remove in favor of AppOnPathD?
        | MapOnPathD

        -- AppOnPathD :  (A : U) (F : A -> U) (f g : (x : A) -> F x) -> Id ((x : A) -> F x) f g ->
        --               (a0 a1 : A) (p : Id A a0 a1) -> IdS A F a0 a1 p  (f a0) (g a1)
        -- | AppOnPathD

  mapOnPathS : ( A :  : A - > U ) ( C : U ) ( f : ( x : A ) - > F x - > C ) ( a0 a1 : A ) ( p :     )
        -- (b0:F a0) (b1:F a1) (q : IdS A F a0 a1 p b0 b1) -> Id C (f a0 b0) (f a1 b1)
  TODO :  ?

        -- S1 : U
        | Circle

        -- base : S1
        | Base

        -- loop : Id S1 base base
        | Loop

   : ( F : S1 - > U ) ( b : F base ) ( l : IdS F base base loop ) ( x : S1 ) - > F x
        | CircleRec

        -- I : U
        | I

  I0 , I1 : Int
        | I0 | I1

        -- line : Id Int I0 I1
        | Line


        -- intrec : (F : I -> U) (s : F I0) (e : F I1)
        --  (l : IdS Int F I0 I1 line s e) (x : I) -> F x
        | IntRec

        -- undefined constant
        | Undef Loc
  deriving (Eq, Show)

-- For an expression t, returns (u,ts) where u is no application
-- and t = u t
unApps :: Ter -> (Ter,[Ter])
unApps = aux []
  where aux :: [Ter] -> Ter -> (Ter,[Ter])
        aux acc (App r s) = aux (s:acc) r
        aux acc t         = (t,acc)
-- Non tail reccursive version:
-- unApps (App r s) = let (t,ts) = unApps r in (t, ts ++ [s])
-- unApps t         = (t,[])

mkApps :: Ter -> [Ter] -> Ter
mkApps (Con l us) vs = Con l (us ++ vs)
mkApps t ts          = foldl App t ts

mkLams :: [String] -> Ter -> Ter
mkLams bs t = foldr Lam t [noLoc b | b <- bs]

mkWheres :: [ODecls] -> Ter -> Ter
mkWheres []     e = e
mkWheres (d:ds) e = Where (mkWheres ds e) d

-- Primitive notions
primHandle :: [(Ident,Int,PN)]
primHandle =
  [("Id"            , 3,  Id           ),
   ("refl"          , 2,  Refl         ),
  ( " funExt "         , 5 ,   Ext           ) ,
   ("funHExt"       , 5,  HExt          ),
   ("inh"           , 1,  Inh          ),
   ("inc"           , 2,  Inc          ),
   ("squash"        , 3,  Squash       ),
   ("inhrec"        , 5,  InhRec       ),
   ("equivEq"       , 5,  EquivEq      ),
   ("transport"     , 4,  TransU       ),
   ("transpInv"     , 4,  TransInvU    ),
   ("contrSingl"    , 4,  CSingl       ),
   ("transportRef"  , 2,  TransURef    ),
   ("equivEqRef"    , 3,  EquivEqRef   ),
   ("transpEquivEq" , 6,  TransUEquivEq),
   ("appOnPath"     , 8,  AppOnPath    ),
   ("mapOnPath"     , 6,  MapOnPath    ),
   ("IdP"           , 5,  IdP          ),
   ("mapOnPathD"    , 6,  MapOnPathD   ),
   ("mapOnPathS"    , 10, MapOnPathS   ),
   ("S1"            , 0,  Circle       ),
   ("base"          , 0,  Base         ),
   ("loop"          , 0,  Loop         ),
   ("S1rec"         , 4,  CircleRec    ),
   ("I"             , 0,  I            ),
   ("I0"            , 0,  I0           ),
   ("I1"            , 0,  I1           ),
   ("line"          , 0,  Line         ),
   ("intrec"        , 5,  IntRec       )]

reservedNames :: [String]
reservedNames = [ s | (s,_,_) <- primHandle ]

arity :: PN -> Int
arity pn = fromMaybe 0 $ listToMaybe [n | (_,n,pn') <- primHandle, pn == pn']

mkPN :: String -> Maybe PN
mkPN s = listToMaybe [pn | (s',_,pn) <- primHandle, s == s']

--------------------------------------------------------------------------------
-- | Names, dimension, and nominal type class

type Name = Integer
type Dim  = [Name]

gensym :: Dim -> Name
gensym [] = 2
gensym xs = maximum xs + 1

gensyms :: Dim -> [Name]
gensyms d = let x = gensym d in x : gensyms (x : d)

class Nominal a where
  swap :: a -> Name -> Name -> a
  support :: a -> [Name]

fresh :: Nominal a => a -> Name
fresh = gensym . support

freshs :: Nominal a => a -> [Name]
freshs = gensyms . support

instance (Nominal a, Nominal b) => Nominal (a, b) where
  support (a, b)  = support a `union` support b
  swap (a, b) x y = (swap a x y, swap b x y)

instance Nominal a => Nominal [a]  where
  support vs  = unions (map support vs)
  swap vs x y = [swap v x y | v <- vs]

instance Nominal a => Nominal (Maybe a)  where
  support = maybe [] support
  swap v x y = fmap (\u -> swap u x y) v

-- Make Name an instance of Nominal
instance Nominal Integer where
  support 0 = []
  support 1 = []
  support n = [n]

  swap z x y | z == x    = y
             | z == y    = x
             | otherwise = z

--------------------------------------------------------------------------------
-- | Boxes

-- TODO: abstract the type of Intervals instead of exposing the encoding
type Dir = Integer

mirror :: Dir -> Dir
mirror 0 = 1
mirror 1 = 0
mirror n = error $ "mirror: 0 or 1 expected but " ++ show n ++ " given"

up, down :: Dir
up   = 1
down = 0

type Side = (Name,Dir)

allDirs :: [Name] -> [Side]
allDirs []     = []
allDirs (n:ns) = (n,down) : (n,up) : allDirs ns

data Box a = Box { dir   :: Dir
                 , pname :: Name
                 , pface :: a
                 , sides :: [(Side,a)] }
  deriving Eq

instance Show a => Show (Box a) where
  show (Box dir n f xs) = "Box" <+> show dir <+> show n <+> show f <+> show xs

mapBox :: (a -> b) -> Box a -> Box b
mapBox f (Box d n x xs) = Box d n (f x) [ (nnd,f v) | (nnd,v) <- xs ]

sequenceSnd :: Monad m => [(a,m b)] -> m [(a,b)]
sequenceSnd []          = return []
sequenceSnd ((a,b):abs) = do
  b' <- b
  acs <- sequenceSnd abs
  return $ (a,b') : acs

sequenceBox :: Monad m => Box (m a) -> m (Box a)
sequenceBox (Box d n x xs) = do
  x' <- x
  xs' <- sequenceSnd xs
  return $ Box d n x' xs'

mapBoxM :: Monad m => (a -> m b) -> Box a -> m (Box b)
mapBoxM f = sequenceBox . mapBox f

instance Functor Box where
  fmap = mapBox

lookBox :: Show a => Side -> Box a -> a
lookBox (y,dir) (Box d x v _)  | x == y && mirror d == dir = v
lookBox xd box@(Box _ _ _ nvs) = case lookup xd nvs of
  Just v  -> v
  Nothing -> error $ "lookBox: box not defined on " ++
                      show xd ++ "\nbox = " ++ show box

nonPrincipal :: Box a -> [Name]
nonPrincipal (Box _ _ _ nvs) = nub $ map (fst . fst) nvs

defBox :: Box a -> [(Name, Dir)]
defBox (Box d x _ nvs) = (x,mirror d) : [ zd | (zd,_) <- nvs ]

fromBox :: Box a -> [(Side,a)]
fromBox (Box d x v nvs) = ((x, mirror d),v) : nvs

modBox :: (Side -> a -> b) -> Box a -> Box b
modBox f (Box dir x v nvs) =
  Box dir x (f (x,mirror dir) v) [ (nd,f nd v) | (nd,v) <- nvs ]

modBoxM :: Monad m => (Side -> a -> m b) -> Box a -> m (Box b)
modBoxM f = sequenceBox . modBox f

-- Restricts the non-principal faces to np.
subBox :: [Name] -> Box a -> Box a
subBox np (Box dir x v nvs) =
  Box dir x v [ nv | nv@((n,_),_) <- nvs, n `elem` np]

shapeOfBox :: Box a -> Box ()
shapeOfBox = mapBox (const ())

  fst is down , snd is up
consBox :: (Name,(a,a)) -> Box a -> Box a
consBox (n,(v0,v1)) (Box dir x v nvs) =
  Box dir x v $ ((n,down),v0) : ((n,up),v1) : nvs

appendBox :: [(Name,(a,a))] -> Box a -> Box a
appendBox xs b = foldr consBox b xs

appendSides :: [(Side, a)] -> Box a -> Box a
appendSides sides (Box dir x v nvs) = Box dir x v (sides ++ nvs)

transposeBox :: Box [a] -> [Box a]
transposeBox b@(Box dir _ [] _)      = []
transposeBox (Box dir x (v:vs) nvss) =
  Box dir x v [ (nnd,head vs) | (nnd,vs) <- nvss ] :
  transposeBox (Box dir x vs [ (nnd,tail vs) | (nnd,vs) <- nvss ])

-- Nominal for boxes
instance Nominal a => Nominal (Box a) where
  support (Box dir n v nvs)  = support ((n, v), nvs)
  swap (Box dir z v nvs) x y = Box dir z' v' nvs' where
    ((z',v'), nvs') = swap ((z, v), nvs) x y

--------------------------------------------------------------------------------
-- | Values

data KanType = Fill | Com
  deriving (Show, Eq)

data Val = VU
         | Ter Ter OEnv
         | VPi Val Val
         | VId Val Val Val

         | VSigma Val Val
         | VSPair Val Val

         -- tag values which are paths
         | Path Name Val

  | VExt Name    Val
         | VHExt Name Val Val Val Val

         -- inhabited
         | VInh Val

         -- inclusion into inhabited
         | VInc Val

  squash type - connects the two values along the name
         | VSquash Name Val Val

         | VCon Ident [Val]

         | Kan KanType Val (Box Val)

         -- of type U connecting a and b along x
         -- VEquivEq x a b f s t
         | VEquivEq Name Val Val Val Val Val

         -- names x, y and values a, s, t
         | VEquivSquare Name Name Val Val Val

         -- of type VEquivEq
         | VPair Name Val Val

  of type VEquivSquare
         | VSquare Name Name Val

  a value of type    ( Box ( type of values ) )
         | VComp (Box Val)

  a value of type Kan Fill VU ( Box ( type of values minus name ) )
         -- the name is bound
         | VFill Name (Box Val)

         -- circle
         | VCircle
         | VBase
  has type VCircle and connects base along the name

         -- interval
         | VI
         | VI0
         | VI1
         | VLine Name           -- connects start and end point along name

         -- neutral values
  the first  must be neutral
         | VAppName Val Name
  the second  must be neutral
         | VVar String Dim
  the last  must be neutral
  the last  must be neutral
  the last  must be neutral
         | VFillN Val (Box Val)
         | VComN Val (Box Val)
         | VFst Val
         | VSnd Val
  deriving Eq

vepair :: Name -> Val -> Val -> Val
vepair x a b = VSPair a (Path x b)

mkVar :: Int -> Dim -> Val
mkVar k = VVar ('X' : show k)

isNeutral :: Val -> Bool
isNeutral (VApp u _)           = isNeutral u
isNeutral (VAppName u _)       = isNeutral u
isNeutral (VSplit _ v)         = isNeutral v
isNeutral (VVar _ _)           = True
isNeutral (VInhRec _ _ _ v)    = isNeutral v
isNeutral (VCircleRec _ _ _ v) = isNeutral v
isNeutral (VIntRec _ _ _ _ v)  = isNeutral v
isNeutral (VFillN _ _)         = True
isNeutral (VComN _ _)          = True
isNeutral (VFst v)             = isNeutral v
isNeutral (VSnd v)             = isNeutral v
isNeutral _                    = False

fstVal, sndVal, unSquare :: Val -> Val
fstVal (VPair _ a _)     = a
fstVal x                 = error $ "error fstVal: " ++ show x
sndVal (VPair _ _ v)     = v
sndVal x                 = error $ "error sndVal: " ++ show x
unSquare (VSquare _ _ v) = v
unSquare v               = error $ "unSquare bad input: " ++ show v

unCon :: Val -> [Val]
unCon (VCon _ vs) = vs
unCon v           = error $ "unCon: not a constructor: " ++ show v

unions :: Eq a => [[a]] -> [a]
unions = foldr union []

unionsMap :: Eq b => (a -> [b]) -> [a] -> [b]
unionsMap f = unions . map f

instance Nominal Val where
  support VU                            = []
  support (Ter _ e)                     = support e
  support (VId a v0 v1)                 = support [a,v0,v1]
  support (Path x v)                    = delete x $ support v
  support (VInh v)                      = support v
  support (VInc v)                      = support v
  support (VPi v1 v2)                   = support [v1,v2]
  support (VCon _ vs)                   = support vs
  support (VSquash x v0 v1)             = support (x, [v0,v1])
  support ( VExt x b f g p )            = support ( x , [ b , f ,  , p ] )
  support (VHExt x b f g p)             = support (x, [b,f,g,p])
  support (Kan Fill a box)              = support (a, box)
  support (VFillN a box)                = support (a, box)
  support (VComN   a box@(Box _ n _ _)) = delete n (support (a, box))
  support (Kan Com a box@(Box _ n _ _)) = delete n (support (a, box))
  support (VEquivEq x a b f s t)        = support (x, [a,b,f,s,t])
           -- names x, y and values a, s, t
  support (VEquivSquare x y a s t)      = support ((x,y), [a,s,t])
  support (VPair x a v)                 = support (x, [a,v])
  support (VComp box@(Box _ n _ _))     = delete n $ support box
  support (VFill x box)                 = delete x $ support box
  support (VApp u v)                    = support (u, v)
  support (VAppName u n)                = support (u, n)
  support (VSplit u v)                  = support (u, v)
  support (VVar x d)                    = support d
  support (VSigma u v)                  = support (u,v)
  support (VSPair u v)                  = support (u,v)
  support (VFst u)                      = support u
  support (VSnd u)                      = support u
  support (VInhRec b p h a)             = support [b,p,h,a]
  support VCircle                       = []
  support VBase                         = []
  support (VLoop n)                     = [n]
  support (VCircleRec f b l s)          = support [f,b,l,s]
  support VI                            = []
  support VI0                           = []
  support VI1                           = []
  support (VLine n)                     = [n]
  support (VIntRec f s e l u)           = support [f,s,e,l,u]
  support v                             = error ("support " ++ show v)

  swap u x y =
    let sw u = swap u x y in case u of
    VU                     -> VU
    Ter t e                -> Ter t (sw e)
    VId a v0 v1            -> VId (sw a) (sw v0) (sw v1)
    Path z v               -> Path (sw z) (sw v)
  VExt z b f g p       - > VExt ( swap z x y ) ( sw b ) ( sw f ) ( sw g ) ( sw p )
    VHExt z b f g p        -> VHExt (sw z) (sw b) (sw f) (sw g) (sw p)
    VPi a f                -> VPi (sw a) (sw f)
    VInh v                 -> VInh (sw v)
    VInc v                 -> VInc (sw v)
    VSquash z v0 v1        -> VSquash (sw z) (sw v0) (sw v1)
    VCon c us              -> VCon c (map sw us)
    VEquivEq z a b f s t   ->
      VEquivEq (sw z) (sw a) (sw b) (sw f) (sw s) (sw t)
    VPair z a v            -> VPair (sw z) (sw a) (sw v)
    VEquivSquare z w a s t ->
      VEquivSquare (sw z) (sw w) (sw a) (sw s) (sw t)
    VSquare z w v          -> VSquare (sw z) (sw w) (sw v)
    Kan Fill a b           -> Kan Fill (sw a) (sw b)
    VFillN a b             -> VFillN (sw a) (sw b)
    Kan Com a b            -> Kan Com (sw a) (sw b)
    VComN a b              -> VComN (sw a) (sw b)
    VComp b                -> VComp (sw b)
    VFill z b              -> VFill (sw z) (sw b)
    VApp u v               -> VApp (sw u) (sw v)
    VAppName u n           -> VAppName (sw u) (sw n)
    VSplit u v             -> VSplit (sw u) (sw v)
    VVar s d               -> VVar s (sw d)
    VSigma u v             -> VSigma (sw u) (sw v)
    VSPair u v             -> VSPair (sw u) (sw v)
    VFst u                 -> VFst (sw u)
    VSnd u                 -> VSnd (sw u)
    VInhRec b p h a        -> VInhRec (sw b) (sw p) (sw h) (sw a)
    VCircle                -> VCircle
    VBase                  -> VBase
    VLoop z                -> VLoop (sw z)
    VCircleRec f b l a     -> VCircleRec (sw f) (sw b) (sw l) (sw a)
    VI                     -> VI
    VI0                    -> VI0
    VI1                    -> VI1
    VLine z                -> VLine (sw z)
    VIntRec f s e l u      -> VIntRec (sw f) (sw s) (sw e) (sw l) (sw u)


--------------------------------------------------------------------------------
-- | Environments

data Env = Empty
         | Pair Env (Binder,Val)
         | PDef [(Binder,Ter)] Env
  deriving Eq

instance Show Env where
  show Empty            = ""
  show (PDef xas env)   = show env
  show (Pair env (x,u)) = parens $ showEnv1 env ++ show u
    where
      showEnv1 (Pair env (x,u)) = showEnv1 env ++ show u ++ ", "
      showEnv1 e                = show e

instance Nominal Env where
  swap e x y = mapEnv (\u -> swap u x y) e

  support Empty          = []
  support (Pair e (_,v)) = support (e, v)
  support (PDef _ e)     = support e

data OEnv = OEnv { env     :: Env,
                   opaques :: [Binder] }
  deriving Eq

oEmpty :: OEnv
oEmpty = OEnv Empty []

oPair :: OEnv -> (Binder,Val) -> OEnv
oPair (OEnv e o) u = OEnv (Pair e u) o

oPDef :: Bool -> ODecls -> OEnv -> OEnv
oPDef _    (ODecls decls)  (OEnv e o) = OEnv (PDef [(x,d) | (x,_,d) <- decls] e) o
oPDef True (Opaque d)      (OEnv e o) = OEnv e (d:o)
oPDef True (Transp d)      (OEnv e o) = OEnv e (d `delete` o)
oPDef _ _ e = e

instance Show OEnv where
  show (OEnv e s) = show e -- <+> parens ("with opaque:" <+> ccat s)

instance Nominal OEnv where
  swap (OEnv e s) x y = OEnv (swap e x y) s
  support (OEnv e s)  = support e

upds :: OEnv -> [(Binder,Val)] -> OEnv
upds = foldl oPair

lookupIdent :: Ident -> [(Binder,a)] -> Maybe (Binder, a)
lookupIdent x defs = lookup x [(y,((y,l),t)) | ((y,l),t) <- defs]

getIdent :: Ident -> [(Binder,a)] -> Maybe a
getIdent x defs = snd <$> lookupIdent x defs

getBinder :: Ident -> [(Binder,a)] -> Maybe Binder
getBinder x defs = fst <$> lookupIdent x defs

mapEnv :: (Val -> Val) -> Env -> Env
mapEnv _ Empty          = Empty
mapEnv f (Pair e (x,v)) = Pair (mapEnv f e) (x,f v)
mapEnv f (PDef ts e)    = PDef ts (mapEnv f e)

mapEnvM :: Applicative m => (Val -> m Val) -> Env -> m Env
mapEnvM _ Empty          = pure Empty
mapEnvM f (Pair e (x,v)) = Pair <$> mapEnvM f e <*> ( (x,) <$> f v)
mapEnvM f (PDef ts e)    = PDef ts <$> mapEnvM f e

mapOEnv :: (Val -> Val) -> OEnv -> OEnv
mapOEnv f (OEnv e o) = OEnv (mapEnv f e) o

mapOEnvM :: Applicative m => (Val -> m Val) -> OEnv -> m OEnv
mapOEnvM f (OEnv e o) = flip OEnv o <$> mapEnvM f e

valOfEnv :: Env -> [Val]
valOfEnv Empty            = []
valOfEnv (Pair env (_,v)) = v : valOfEnv env
valOfEnv (PDef _ env)     = valOfEnv env

valOfOEnv :: OEnv -> [Val]
valOfOEnv (OEnv e o) = valOfEnv e

--------------------------------------------------------------------------------
-- | Pretty printing

instance Show Loc where
  show (Loc name (i,j)) = name ++ "_L" ++ show i ++ "_C" ++ show j

instance Show Ter where
  show = showTer

showTer :: Ter -> String
showTer U             = "U"
showTer (App e0 e1)   = showTer e0 <+> showTer1 e1
showTer (Pi e0 e1)    = "Pi" <+> showTers [e0,e1]
showTer (Lam (x,_) e) = '\\' : x <+> "->" <+> showTer e
showTer (Fst e)       = showTer e ++ ".1"
showTer (Snd e)       = showTer e ++ ".2"
showTer (Sigma e0 e1) = "Sigma" <+> showTers [e0,e1]
showTer (SPair e0 e1) = "pair" <+> showTers [e0,e1]
showTer (Where e d)   = showTer e <+> "where" <+> showODecls d
showTer (Var x)       = x
showTer (Con c es)    = c <+> showTers es
showTer (Split l _)   = "split " ++ show l
showTer (Sum l _)     = "sum " ++ show l
showTer (PN pn)       = showPN pn

showTers :: [Ter] -> String
showTers = hcat . map showTer1

showTer1 :: Ter -> String
showTer1 U           = "U"
showTer1 (Con c [])  = c
showTer1 (Var x)     = x
showTer1 u@(Split{}) = showTer u
showTer1 u@(Sum{})   = showTer u
showTer1 u@(PN{})    = showTer u
showTer1 u           = parens $ showTer u

-- Warning: do not use showPN as a Show instance as it will loop
showPN :: PN -> String
showPN (Undef l) = show l
showPN pn              = case [s | (s,_,pn') <- primHandle, pn == pn'] of
  [s] -> s
  _   -> error $ "showPN: unknown primitive " ++ show pn

showDecls :: Decls -> String
showDecls defs = ccat (map (\((x,_),_,d) -> x <+> "=" <+> show d) defs)

showODecls :: ODecls -> String
showODecls (ODecls defs) = showDecls defs
showODecls (Opaque x)    = "opaque"      <+> show x
showODecls (Transp x)    = "transparent" <+> show x

instance Show Val where
  show = showVal

showVal :: Val -> String
showVal VU                       = "U"
showVal (Ter t env)              = show t <+> show env
showVal (VId a u v)              =
  "Id" <+> showVal1 a <+> showVal1 u <+> showVal1 v
showVal (Path n u)               = abrack (show n) <+> showVal u
  showVal ( VExt n b f g p )       = " funExt " < + > show n < + > showVals [ b , f ,  , p ]
showVal (VHExt n b f g p)        = "funHExt" <+> show n <+> showVals [b,f,g,p]
showVal (VCon c us)              = c <+> showVals us
showVal (VPi a f)                = "Pi" <+> showVals [a,f]
showVal (VInh u)                 = "inh" <+> showVal1 u
showVal (VInc u)                 = "inc" <+> showVal1 u
showVal (VInhRec b p h a)        = "inhrec" <+> showVals [b,p,h,a]
showVal (VSquash n u v)          = "squash" <+> show n <+> showVals [u,v]
showVal (Kan Fill v box)         = "Fill" <+> showVal1 v <+> parens (show box)
showVal (Kan Com v box)          = "Com" <+> showVal1 v <+> parens (show box)
showVal (VFillN v box)           = "FillN" <+> showVal1 v <+> parens (show box)
showVal (VComN v box)            = "ComN" <+> showVal1 v <+> parens (show box)
showVal (VPair n u v)            = "vpair" <+> show n <+> showVals [u,v]
showVal (VSquare x y u)          = "vsquare" <+> show x <+> show y <+> showVal1 u
showVal (VComp box)              = "vcomp" <+> parens (show box)
showVal (VFill n box)            = "vfill" <+> show n <+> parens (show box)
showVal (VApp u v)               = showVal u <+> showVal1 v
showVal (VAppName u n)           = showVal u <+> "@" <+> show n
showVal (VSplit u v)             = showVal u <+> showVal1 v
showVal (VVar x d)               = x <+> showDim d
showVal (VEquivEq n a b f _ _)   = "equivEq" <+> show n <+> showVals [a,b,f]
showVal (VEquivSquare x y a s t) =
  "equivSquare" <+> show x <+> show y <+> showVals [a,s,t]
showVal (VSPair u v)             = "pair" <+> showVals [u,v]
showVal (VSigma u v)             = "Sigma" <+> showVals [u,v]
showVal (VFst u)                 = showVal u ++ ".1"
showVal (VSnd u)                 = showVal u ++ ".2"
showVal VCircle                  = "S1"
showVal VBase                    = "base"
showVal (VLoop x)                = "loop" <+> show x
showVal (VCircleRec f b l s)     = "S1rec" <+> showVals [f,b,l,s]
showVal VI                       = "I"
showVal VI0                      = "I0"
showVal VI1                      = "I1"
showVal (VLine n)                = "line" <+> show n
showVal (VIntRec f s e l u)      = "intrec" <+> showVals [f,s,e,l,u]

showDim :: Show a => [a] -> String
showDim = parens . ccat . map show

showVals :: [Val] -> String
showVals = hcat . map showVal1

showVal1 :: Val -> String
showVal1 VU          = "U"
showVal1 (VCon c []) = c
showVal1 u@(VVar{})  = showVal u
showVal1 u           = parens $ showVal u

------------------------------------------------------------------------------
 | Terms
 Branch of the form: c x1 .. xn -> e
 Labelled sum: c (x1 : A1) .. (xn : An)
 Context gives type values to identifiers
 Mutual recursive definitions: (x1 : A1) .. (xn : An) and x1 = e1 .. xn = en
 Terms
 constructor c Ms
 branches c1 xs1  -> M1,..., cn xsn -> Mn
 Primitive notions
 Inh A is an h-prop stating that A is inhabited.
 Here we take h-prop A as (Pi x y : A) Id A x y.
 Inc a : Inh A for a:A (A not needed ??)
 (A B : U) -> Id U A B -> A -> B
 For TransU we only need the eqproof and the element in A is needed
 (A B : U) -> Id U A B -> B -> A
 For TransU we only need the eqproof and the element in A is needed
 (A : U) (a b:A) (p:Id A a b) -> Id (singl A a) (pair a (refl A a)) (pair b p)
 (A B : U) (f : A -> B) (a b : A) ->
 (p : Id A a b) -> Id B (f a) (f b)
 TODO: remove?
 (A B : U) (f g : A -> B) (a b : A) ->
 Id (A->B) f g -> Id A a b -> Id B (f a) (g b)
 | Ext
 (p : (Pi x y:A) IdS A (Bx) x y p fx gy)
 A, B are types, f : A -> B,
 s : (y : B) -> fiber f y, and
 (A : U) -> (s : (y : A) -> pathTo A a) ->
 (t : (y : B) -> (v : pathTo A a) -> Id (path To A a) (s y) v) ->
 (A B : U) -> (f : A -> B) (s : (y : B) -> fiber A B f y) ->
 (t : (y : B) -> (v : fiber A B f y) -> Id (fiber A B f y) (s y) v) ->
 (a : A) -> Id B (f a) (transport A B (equivEq A B f s t) a)
 mapOnPathD :  (A : U) (F : A -> U) (f : (x : A) -> F x) (a0 a1 : A) (p : Id A a0 a1) ->
               IdS A F a0 a1 p  (f a0) (f a1)
 IdS A F a0 a1 p = IdP (F a0) (F a1) (mapOnPath A U F a0 a1 p)
 TODO: remove in favor of AppOnPathD?
 AppOnPathD :  (A : U) (F : A -> U) (f g : (x : A) -> F x) -> Id ((x : A) -> F x) f g ->
               (a0 a1 : A) (p : Id A a0 a1) -> IdS A F a0 a1 p  (f a0) (g a1)
 | AppOnPathD
 (b0:F a0) (b1:F a1) (q : IdS A F a0 a1 p b0 b1) -> Id C (f a0 b0) (f a1 b1)
 S1 : U
 base : S1
 loop : Id S1 base base
 I : U
 line : Id Int I0 I1
 intrec : (F : I -> U) (s : F I0) (e : F I1)
  (l : IdS Int F I0 I1 line s e) (x : I) -> F x
 undefined constant
 For an expression t, returns (u,ts) where u is no application
 and t = u t
 Non tail reccursive version:
 unApps (App r s) = let (t,ts) = unApps r in (t, ts ++ [s])
 unApps t         = (t,[])
 Primitive notions
------------------------------------------------------------------------------
 | Names, dimension, and nominal type class
 Make Name an instance of Nominal
------------------------------------------------------------------------------
 | Boxes
 TODO: abstract the type of Intervals instead of exposing the encoding
 Restricts the non-principal faces to np.
 Nominal for boxes
------------------------------------------------------------------------------
 | Values
 tag values which are paths
 inhabited
 inclusion into inhabited
 of type U connecting a and b along x
 VEquivEq x a b f s t
 names x, y and values a, s, t
 of type VEquivEq
 the name is bound
 circle
 interval
 connects start and end point along name
 neutral values
 names x, y and values a, s, t
------------------------------------------------------------------------------
 | Environments
 <+> parens ("with opaque:" <+> ccat s)
------------------------------------------------------------------------------
 | Pretty printing
 Warning: do not use showPN as a Show instance as it will loop
# LANGUAGE TupleSections #
module CTT where

import Control.Applicative
import Data.List
import Data.Maybe
import Pretty


data Loc = Loc { locFile :: String
               , locPos :: (Int, Int) }
  deriving Eq

type Ident  = String
type Label  = String
type Binder = (Ident,Loc)

noLoc :: String -> Binder
noLoc x = (x, Loc "" (0,0))

type Brc    = (Label,([Binder],Ter))

  Telescope ( x1 : A1 ) .. ( xn : An )
type Tele   = [(Binder,Ter)]

type LblSum = [(Binder,Tele)]

type Ctxt   = [(Binder,Val)]

type Decls  = [(Binder,Ter,Ter)]
data ODecls = ODecls Decls
            | Opaque Binder
            | Transp Binder
  deriving (Eq,Show)

declIdents :: Decls -> [Ident]
declIdents decl = [ x | ((x,_),_,_) <- decl]

declBinders :: Decls -> [Binder]
declBinders decl = [ x | (x,_,_) <- decl]

declTers :: Decls -> [Ter]
declTers decl = [ d | (_,_,d) <- decl]

declTele :: Decls -> Tele
declTele decl = [ (x,t) | (x,t,_) <- decl]

declDefs :: Decls -> [(Binder,Ter)]
declDefs decl = [ (x,d) | (x,_,d) <- decl]

data Ter = App Ter Ter
         | Pi Ter Ter
         | Lam Binder Ter
         | Sigma Ter Ter
         | SPair Ter Ter
         | Fst Ter
         | Snd Ter
         | Where Ter ODecls
         | Var Ident
         | U
         | Con Label [Ter]
         | Split Loc [Brc]
  labelled sum c1 A1s , ... , cn Ans ( assumes terms are constructors )
         | Sum Binder LblSum
         | PN PN
  deriving Eq

data PN = Id | Refl
        | Inh
        | Inc
  Squash a b : I d ( Inh A ) a b
        | Squash
  InhRec B p phi a : B ,
  p :  ) ,  : A - > B , a : Inh A ( cf . HoTT - book p.113 )
        | InhRec

        | TransU

        | TransInvU

  ( A : U ) - > ( a : A ) - > I d A a ( transport A ( refl U A ) a )
        | TransURef

        | CSingl

        | MapOnPath

        | AppOnPath

  Ext B f g p : I d ( Pi A B ) f g ,
  ( p : ( Pi x : A ) I d ( Bx ) ( fx , gx ) ) ; A not needed ? ?

  Ext B f g p : I d ( Pi A B ) f g ,
        | HExt

  EquivEq A B f s t where
  t : ( y : B ) ( z : fiber f y ) - > I d ( fiber f y ) ( s y ) z
  where fiber f y is Sigma x : A. I d B ( f x ) 
        | EquivEq
  I d ( I d U A A ) ( refl U A ) ( equivEq A A ( i d A ) s t )
        | EquivEqRef

        | TransUEquivEq

  IdP   :     ( A B : U ) - > I d U A B - >   A - > B - > U
  IdP A B p a b    is the type of paths   connecting a to b over p
        | IdP

  IdS : ( A : U ) ( F : A - > U ) ( a0 a1 : A ) ( p :     ) - > F a0 - > F a1 - > U
        | MapOnPathD


  mapOnPathS : ( A :  : A - > U ) ( C : U ) ( f : ( x : A ) - > F x - > C ) ( a0 a1 : A ) ( p :     )
  TODO :  ?

        | Circle

        | Base

        | Loop

   : ( F : S1 - > U ) ( b : F base ) ( l : IdS F base base loop ) ( x : S1 ) - > F x
        | CircleRec

        | I

  I0 , I1 : Int
        | I0 | I1

        | Line


        | IntRec

        | Undef Loc
  deriving (Eq, Show)

unApps :: Ter -> (Ter,[Ter])
unApps = aux []
  where aux :: [Ter] -> Ter -> (Ter,[Ter])
        aux acc (App r s) = aux (s:acc) r
        aux acc t         = (t,acc)

mkApps :: Ter -> [Ter] -> Ter
mkApps (Con l us) vs = Con l (us ++ vs)
mkApps t ts          = foldl App t ts

mkLams :: [String] -> Ter -> Ter
mkLams bs t = foldr Lam t [noLoc b | b <- bs]

mkWheres :: [ODecls] -> Ter -> Ter
mkWheres []     e = e
mkWheres (d:ds) e = Where (mkWheres ds e) d

primHandle :: [(Ident,Int,PN)]
primHandle =
  [("Id"            , 3,  Id           ),
   ("refl"          , 2,  Refl         ),
  ( " funExt "         , 5 ,   Ext           ) ,
   ("funHExt"       , 5,  HExt          ),
   ("inh"           , 1,  Inh          ),
   ("inc"           , 2,  Inc          ),
   ("squash"        , 3,  Squash       ),
   ("inhrec"        , 5,  InhRec       ),
   ("equivEq"       , 5,  EquivEq      ),
   ("transport"     , 4,  TransU       ),
   ("transpInv"     , 4,  TransInvU    ),
   ("contrSingl"    , 4,  CSingl       ),
   ("transportRef"  , 2,  TransURef    ),
   ("equivEqRef"    , 3,  EquivEqRef   ),
   ("transpEquivEq" , 6,  TransUEquivEq),
   ("appOnPath"     , 8,  AppOnPath    ),
   ("mapOnPath"     , 6,  MapOnPath    ),
   ("IdP"           , 5,  IdP          ),
   ("mapOnPathD"    , 6,  MapOnPathD   ),
   ("mapOnPathS"    , 10, MapOnPathS   ),
   ("S1"            , 0,  Circle       ),
   ("base"          , 0,  Base         ),
   ("loop"          , 0,  Loop         ),
   ("S1rec"         , 4,  CircleRec    ),
   ("I"             , 0,  I            ),
   ("I0"            , 0,  I0           ),
   ("I1"            , 0,  I1           ),
   ("line"          , 0,  Line         ),
   ("intrec"        , 5,  IntRec       )]

reservedNames :: [String]
reservedNames = [ s | (s,_,_) <- primHandle ]

arity :: PN -> Int
arity pn = fromMaybe 0 $ listToMaybe [n | (_,n,pn') <- primHandle, pn == pn']

mkPN :: String -> Maybe PN
mkPN s = listToMaybe [pn | (s',_,pn) <- primHandle, s == s']


type Name = Integer
type Dim  = [Name]

gensym :: Dim -> Name
gensym [] = 2
gensym xs = maximum xs + 1

gensyms :: Dim -> [Name]
gensyms d = let x = gensym d in x : gensyms (x : d)

class Nominal a where
  swap :: a -> Name -> Name -> a
  support :: a -> [Name]

fresh :: Nominal a => a -> Name
fresh = gensym . support

freshs :: Nominal a => a -> [Name]
freshs = gensyms . support

instance (Nominal a, Nominal b) => Nominal (a, b) where
  support (a, b)  = support a `union` support b
  swap (a, b) x y = (swap a x y, swap b x y)

instance Nominal a => Nominal [a]  where
  support vs  = unions (map support vs)
  swap vs x y = [swap v x y | v <- vs]

instance Nominal a => Nominal (Maybe a)  where
  support = maybe [] support
  swap v x y = fmap (\u -> swap u x y) v

instance Nominal Integer where
  support 0 = []
  support 1 = []
  support n = [n]

  swap z x y | z == x    = y
             | z == y    = x
             | otherwise = z


type Dir = Integer

mirror :: Dir -> Dir
mirror 0 = 1
mirror 1 = 0
mirror n = error $ "mirror: 0 or 1 expected but " ++ show n ++ " given"

up, down :: Dir
up   = 1
down = 0

type Side = (Name,Dir)

allDirs :: [Name] -> [Side]
allDirs []     = []
allDirs (n:ns) = (n,down) : (n,up) : allDirs ns

data Box a = Box { dir   :: Dir
                 , pname :: Name
                 , pface :: a
                 , sides :: [(Side,a)] }
  deriving Eq

instance Show a => Show (Box a) where
  show (Box dir n f xs) = "Box" <+> show dir <+> show n <+> show f <+> show xs

mapBox :: (a -> b) -> Box a -> Box b
mapBox f (Box d n x xs) = Box d n (f x) [ (nnd,f v) | (nnd,v) <- xs ]

sequenceSnd :: Monad m => [(a,m b)] -> m [(a,b)]
sequenceSnd []          = return []
sequenceSnd ((a,b):abs) = do
  b' <- b
  acs <- sequenceSnd abs
  return $ (a,b') : acs

sequenceBox :: Monad m => Box (m a) -> m (Box a)
sequenceBox (Box d n x xs) = do
  x' <- x
  xs' <- sequenceSnd xs
  return $ Box d n x' xs'

mapBoxM :: Monad m => (a -> m b) -> Box a -> m (Box b)
mapBoxM f = sequenceBox . mapBox f

instance Functor Box where
  fmap = mapBox

lookBox :: Show a => Side -> Box a -> a
lookBox (y,dir) (Box d x v _)  | x == y && mirror d == dir = v
lookBox xd box@(Box _ _ _ nvs) = case lookup xd nvs of
  Just v  -> v
  Nothing -> error $ "lookBox: box not defined on " ++
                      show xd ++ "\nbox = " ++ show box

nonPrincipal :: Box a -> [Name]
nonPrincipal (Box _ _ _ nvs) = nub $ map (fst . fst) nvs

defBox :: Box a -> [(Name, Dir)]
defBox (Box d x _ nvs) = (x,mirror d) : [ zd | (zd,_) <- nvs ]

fromBox :: Box a -> [(Side,a)]
fromBox (Box d x v nvs) = ((x, mirror d),v) : nvs

modBox :: (Side -> a -> b) -> Box a -> Box b
modBox f (Box dir x v nvs) =
  Box dir x (f (x,mirror dir) v) [ (nd,f nd v) | (nd,v) <- nvs ]

modBoxM :: Monad m => (Side -> a -> m b) -> Box a -> m (Box b)
modBoxM f = sequenceBox . modBox f

subBox :: [Name] -> Box a -> Box a
subBox np (Box dir x v nvs) =
  Box dir x v [ nv | nv@((n,_),_) <- nvs, n `elem` np]

shapeOfBox :: Box a -> Box ()
shapeOfBox = mapBox (const ())

  fst is down , snd is up
consBox :: (Name,(a,a)) -> Box a -> Box a
consBox (n,(v0,v1)) (Box dir x v nvs) =
  Box dir x v $ ((n,down),v0) : ((n,up),v1) : nvs

appendBox :: [(Name,(a,a))] -> Box a -> Box a
appendBox xs b = foldr consBox b xs

appendSides :: [(Side, a)] -> Box a -> Box a
appendSides sides (Box dir x v nvs) = Box dir x v (sides ++ nvs)

transposeBox :: Box [a] -> [Box a]
transposeBox b@(Box dir _ [] _)      = []
transposeBox (Box dir x (v:vs) nvss) =
  Box dir x v [ (nnd,head vs) | (nnd,vs) <- nvss ] :
  transposeBox (Box dir x vs [ (nnd,tail vs) | (nnd,vs) <- nvss ])

instance Nominal a => Nominal (Box a) where
  support (Box dir n v nvs)  = support ((n, v), nvs)
  swap (Box dir z v nvs) x y = Box dir z' v' nvs' where
    ((z',v'), nvs') = swap ((z, v), nvs) x y


data KanType = Fill | Com
  deriving (Show, Eq)

data Val = VU
         | Ter Ter OEnv
         | VPi Val Val
         | VId Val Val Val

         | VSigma Val Val
         | VSPair Val Val

         | Path Name Val

  | VExt Name    Val
         | VHExt Name Val Val Val Val

         | VInh Val

         | VInc Val

  squash type - connects the two values along the name
         | VSquash Name Val Val

         | VCon Ident [Val]

         | Kan KanType Val (Box Val)

         | VEquivEq Name Val Val Val Val Val

         | VEquivSquare Name Name Val Val Val

         | VPair Name Val Val

  of type VEquivSquare
         | VSquare Name Name Val

  a value of type    ( Box ( type of values ) )
         | VComp (Box Val)

  a value of type Kan Fill VU ( Box ( type of values minus name ) )
         | VFill Name (Box Val)

         | VCircle
         | VBase
  has type VCircle and connects base along the name

         | VI
         | VI0
         | VI1

  the first  must be neutral
         | VAppName Val Name
  the second  must be neutral
         | VVar String Dim
  the last  must be neutral
  the last  must be neutral
  the last  must be neutral
         | VFillN Val (Box Val)
         | VComN Val (Box Val)
         | VFst Val
         | VSnd Val
  deriving Eq

vepair :: Name -> Val -> Val -> Val
vepair x a b = VSPair a (Path x b)

mkVar :: Int -> Dim -> Val
mkVar k = VVar ('X' : show k)

isNeutral :: Val -> Bool
isNeutral (VApp u _)           = isNeutral u
isNeutral (VAppName u _)       = isNeutral u
isNeutral (VSplit _ v)         = isNeutral v
isNeutral (VVar _ _)           = True
isNeutral (VInhRec _ _ _ v)    = isNeutral v
isNeutral (VCircleRec _ _ _ v) = isNeutral v
isNeutral (VIntRec _ _ _ _ v)  = isNeutral v
isNeutral (VFillN _ _)         = True
isNeutral (VComN _ _)          = True
isNeutral (VFst v)             = isNeutral v
isNeutral (VSnd v)             = isNeutral v
isNeutral _                    = False

fstVal, sndVal, unSquare :: Val -> Val
fstVal (VPair _ a _)     = a
fstVal x                 = error $ "error fstVal: " ++ show x
sndVal (VPair _ _ v)     = v
sndVal x                 = error $ "error sndVal: " ++ show x
unSquare (VSquare _ _ v) = v
unSquare v               = error $ "unSquare bad input: " ++ show v

unCon :: Val -> [Val]
unCon (VCon _ vs) = vs
unCon v           = error $ "unCon: not a constructor: " ++ show v

unions :: Eq a => [[a]] -> [a]
unions = foldr union []

unionsMap :: Eq b => (a -> [b]) -> [a] -> [b]
unionsMap f = unions . map f

instance Nominal Val where
  support VU                            = []
  support (Ter _ e)                     = support e
  support (VId a v0 v1)                 = support [a,v0,v1]
  support (Path x v)                    = delete x $ support v
  support (VInh v)                      = support v
  support (VInc v)                      = support v
  support (VPi v1 v2)                   = support [v1,v2]
  support (VCon _ vs)                   = support vs
  support (VSquash x v0 v1)             = support (x, [v0,v1])
  support ( VExt x b f g p )            = support ( x , [ b , f ,  , p ] )
  support (VHExt x b f g p)             = support (x, [b,f,g,p])
  support (Kan Fill a box)              = support (a, box)
  support (VFillN a box)                = support (a, box)
  support (VComN   a box@(Box _ n _ _)) = delete n (support (a, box))
  support (Kan Com a box@(Box _ n _ _)) = delete n (support (a, box))
  support (VEquivEq x a b f s t)        = support (x, [a,b,f,s,t])
  support (VEquivSquare x y a s t)      = support ((x,y), [a,s,t])
  support (VPair x a v)                 = support (x, [a,v])
  support (VComp box@(Box _ n _ _))     = delete n $ support box
  support (VFill x box)                 = delete x $ support box
  support (VApp u v)                    = support (u, v)
  support (VAppName u n)                = support (u, n)
  support (VSplit u v)                  = support (u, v)
  support (VVar x d)                    = support d
  support (VSigma u v)                  = support (u,v)
  support (VSPair u v)                  = support (u,v)
  support (VFst u)                      = support u
  support (VSnd u)                      = support u
  support (VInhRec b p h a)             = support [b,p,h,a]
  support VCircle                       = []
  support VBase                         = []
  support (VLoop n)                     = [n]
  support (VCircleRec f b l s)          = support [f,b,l,s]
  support VI                            = []
  support VI0                           = []
  support VI1                           = []
  support (VLine n)                     = [n]
  support (VIntRec f s e l u)           = support [f,s,e,l,u]
  support v                             = error ("support " ++ show v)

  swap u x y =
    let sw u = swap u x y in case u of
    VU                     -> VU
    Ter t e                -> Ter t (sw e)
    VId a v0 v1            -> VId (sw a) (sw v0) (sw v1)
    Path z v               -> Path (sw z) (sw v)
  VExt z b f g p       - > VExt ( swap z x y ) ( sw b ) ( sw f ) ( sw g ) ( sw p )
    VHExt z b f g p        -> VHExt (sw z) (sw b) (sw f) (sw g) (sw p)
    VPi a f                -> VPi (sw a) (sw f)
    VInh v                 -> VInh (sw v)
    VInc v                 -> VInc (sw v)
    VSquash z v0 v1        -> VSquash (sw z) (sw v0) (sw v1)
    VCon c us              -> VCon c (map sw us)
    VEquivEq z a b f s t   ->
      VEquivEq (sw z) (sw a) (sw b) (sw f) (sw s) (sw t)
    VPair z a v            -> VPair (sw z) (sw a) (sw v)
    VEquivSquare z w a s t ->
      VEquivSquare (sw z) (sw w) (sw a) (sw s) (sw t)
    VSquare z w v          -> VSquare (sw z) (sw w) (sw v)
    Kan Fill a b           -> Kan Fill (sw a) (sw b)
    VFillN a b             -> VFillN (sw a) (sw b)
    Kan Com a b            -> Kan Com (sw a) (sw b)
    VComN a b              -> VComN (sw a) (sw b)
    VComp b                -> VComp (sw b)
    VFill z b              -> VFill (sw z) (sw b)
    VApp u v               -> VApp (sw u) (sw v)
    VAppName u n           -> VAppName (sw u) (sw n)
    VSplit u v             -> VSplit (sw u) (sw v)
    VVar s d               -> VVar s (sw d)
    VSigma u v             -> VSigma (sw u) (sw v)
    VSPair u v             -> VSPair (sw u) (sw v)
    VFst u                 -> VFst (sw u)
    VSnd u                 -> VSnd (sw u)
    VInhRec b p h a        -> VInhRec (sw b) (sw p) (sw h) (sw a)
    VCircle                -> VCircle
    VBase                  -> VBase
    VLoop z                -> VLoop (sw z)
    VCircleRec f b l a     -> VCircleRec (sw f) (sw b) (sw l) (sw a)
    VI                     -> VI
    VI0                    -> VI0
    VI1                    -> VI1
    VLine z                -> VLine (sw z)
    VIntRec f s e l u      -> VIntRec (sw f) (sw s) (sw e) (sw l) (sw u)



data Env = Empty
         | Pair Env (Binder,Val)
         | PDef [(Binder,Ter)] Env
  deriving Eq

instance Show Env where
  show Empty            = ""
  show (PDef xas env)   = show env
  show (Pair env (x,u)) = parens $ showEnv1 env ++ show u
    where
      showEnv1 (Pair env (x,u)) = showEnv1 env ++ show u ++ ", "
      showEnv1 e                = show e

instance Nominal Env where
  swap e x y = mapEnv (\u -> swap u x y) e

  support Empty          = []
  support (Pair e (_,v)) = support (e, v)
  support (PDef _ e)     = support e

data OEnv = OEnv { env     :: Env,
                   opaques :: [Binder] }
  deriving Eq

oEmpty :: OEnv
oEmpty = OEnv Empty []

oPair :: OEnv -> (Binder,Val) -> OEnv
oPair (OEnv e o) u = OEnv (Pair e u) o

oPDef :: Bool -> ODecls -> OEnv -> OEnv
oPDef _    (ODecls decls)  (OEnv e o) = OEnv (PDef [(x,d) | (x,_,d) <- decls] e) o
oPDef True (Opaque d)      (OEnv e o) = OEnv e (d:o)
oPDef True (Transp d)      (OEnv e o) = OEnv e (d `delete` o)
oPDef _ _ e = e

instance Show OEnv where

instance Nominal OEnv where
  swap (OEnv e s) x y = OEnv (swap e x y) s
  support (OEnv e s)  = support e

upds :: OEnv -> [(Binder,Val)] -> OEnv
upds = foldl oPair

lookupIdent :: Ident -> [(Binder,a)] -> Maybe (Binder, a)
lookupIdent x defs = lookup x [(y,((y,l),t)) | ((y,l),t) <- defs]

getIdent :: Ident -> [(Binder,a)] -> Maybe a
getIdent x defs = snd <$> lookupIdent x defs

getBinder :: Ident -> [(Binder,a)] -> Maybe Binder
getBinder x defs = fst <$> lookupIdent x defs

mapEnv :: (Val -> Val) -> Env -> Env
mapEnv _ Empty          = Empty
mapEnv f (Pair e (x,v)) = Pair (mapEnv f e) (x,f v)
mapEnv f (PDef ts e)    = PDef ts (mapEnv f e)

mapEnvM :: Applicative m => (Val -> m Val) -> Env -> m Env
mapEnvM _ Empty          = pure Empty
mapEnvM f (Pair e (x,v)) = Pair <$> mapEnvM f e <*> ( (x,) <$> f v)
mapEnvM f (PDef ts e)    = PDef ts <$> mapEnvM f e

mapOEnv :: (Val -> Val) -> OEnv -> OEnv
mapOEnv f (OEnv e o) = OEnv (mapEnv f e) o

mapOEnvM :: Applicative m => (Val -> m Val) -> OEnv -> m OEnv
mapOEnvM f (OEnv e o) = flip OEnv o <$> mapEnvM f e

valOfEnv :: Env -> [Val]
valOfEnv Empty            = []
valOfEnv (Pair env (_,v)) = v : valOfEnv env
valOfEnv (PDef _ env)     = valOfEnv env

valOfOEnv :: OEnv -> [Val]
valOfOEnv (OEnv e o) = valOfEnv e


instance Show Loc where
  show (Loc name (i,j)) = name ++ "_L" ++ show i ++ "_C" ++ show j

instance Show Ter where
  show = showTer

showTer :: Ter -> String
showTer U             = "U"
showTer (App e0 e1)   = showTer e0 <+> showTer1 e1
showTer (Pi e0 e1)    = "Pi" <+> showTers [e0,e1]
showTer (Lam (x,_) e) = '\\' : x <+> "->" <+> showTer e
showTer (Fst e)       = showTer e ++ ".1"
showTer (Snd e)       = showTer e ++ ".2"
showTer (Sigma e0 e1) = "Sigma" <+> showTers [e0,e1]
showTer (SPair e0 e1) = "pair" <+> showTers [e0,e1]
showTer (Where e d)   = showTer e <+> "where" <+> showODecls d
showTer (Var x)       = x
showTer (Con c es)    = c <+> showTers es
showTer (Split l _)   = "split " ++ show l
showTer (Sum l _)     = "sum " ++ show l
showTer (PN pn)       = showPN pn

showTers :: [Ter] -> String
showTers = hcat . map showTer1

showTer1 :: Ter -> String
showTer1 U           = "U"
showTer1 (Con c [])  = c
showTer1 (Var x)     = x
showTer1 u@(Split{}) = showTer u
showTer1 u@(Sum{})   = showTer u
showTer1 u@(PN{})    = showTer u
showTer1 u           = parens $ showTer u

showPN :: PN -> String
showPN (Undef l) = show l
showPN pn              = case [s | (s,_,pn') <- primHandle, pn == pn'] of
  [s] -> s
  _   -> error $ "showPN: unknown primitive " ++ show pn

showDecls :: Decls -> String
showDecls defs = ccat (map (\((x,_),_,d) -> x <+> "=" <+> show d) defs)

showODecls :: ODecls -> String
showODecls (ODecls defs) = showDecls defs
showODecls (Opaque x)    = "opaque"      <+> show x
showODecls (Transp x)    = "transparent" <+> show x

instance Show Val where
  show = showVal

showVal :: Val -> String
showVal VU                       = "U"
showVal (Ter t env)              = show t <+> show env
showVal (VId a u v)              =
  "Id" <+> showVal1 a <+> showVal1 u <+> showVal1 v
showVal (Path n u)               = abrack (show n) <+> showVal u
  showVal ( VExt n b f g p )       = " funExt " < + > show n < + > showVals [ b , f ,  , p ]
showVal (VHExt n b f g p)        = "funHExt" <+> show n <+> showVals [b,f,g,p]
showVal (VCon c us)              = c <+> showVals us
showVal (VPi a f)                = "Pi" <+> showVals [a,f]
showVal (VInh u)                 = "inh" <+> showVal1 u
showVal (VInc u)                 = "inc" <+> showVal1 u
showVal (VInhRec b p h a)        = "inhrec" <+> showVals [b,p,h,a]
showVal (VSquash n u v)          = "squash" <+> show n <+> showVals [u,v]
showVal (Kan Fill v box)         = "Fill" <+> showVal1 v <+> parens (show box)
showVal (Kan Com v box)          = "Com" <+> showVal1 v <+> parens (show box)
showVal (VFillN v box)           = "FillN" <+> showVal1 v <+> parens (show box)
showVal (VComN v box)            = "ComN" <+> showVal1 v <+> parens (show box)
showVal (VPair n u v)            = "vpair" <+> show n <+> showVals [u,v]
showVal (VSquare x y u)          = "vsquare" <+> show x <+> show y <+> showVal1 u
showVal (VComp box)              = "vcomp" <+> parens (show box)
showVal (VFill n box)            = "vfill" <+> show n <+> parens (show box)
showVal (VApp u v)               = showVal u <+> showVal1 v
showVal (VAppName u n)           = showVal u <+> "@" <+> show n
showVal (VSplit u v)             = showVal u <+> showVal1 v
showVal (VVar x d)               = x <+> showDim d
showVal (VEquivEq n a b f _ _)   = "equivEq" <+> show n <+> showVals [a,b,f]
showVal (VEquivSquare x y a s t) =
  "equivSquare" <+> show x <+> show y <+> showVals [a,s,t]
showVal (VSPair u v)             = "pair" <+> showVals [u,v]
showVal (VSigma u v)             = "Sigma" <+> showVals [u,v]
showVal (VFst u)                 = showVal u ++ ".1"
showVal (VSnd u)                 = showVal u ++ ".2"
showVal VCircle                  = "S1"
showVal VBase                    = "base"
showVal (VLoop x)                = "loop" <+> show x
showVal (VCircleRec f b l s)     = "S1rec" <+> showVals [f,b,l,s]
showVal VI                       = "I"
showVal VI0                      = "I0"
showVal VI1                      = "I1"
showVal (VLine n)                = "line" <+> show n
showVal (VIntRec f s e l u)      = "intrec" <+> showVals [f,s,e,l,u]

showDim :: Show a => [a] -> String
showDim = parens . ccat . map show

showVals :: [Val] -> String
showVals = hcat . map showVal1

showVal1 :: Val -> String
showVal1 VU          = "U"
showVal1 (VCon c []) = c
showVal1 u@(VVar{})  = showVal u
showVal1 u           = parens $ showVal u
