{-# 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 : Id (Inh A) a b
| Squash
-- InhRec B p phi a : B,
-- p : hprop(B), phi : 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) -> Id 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 : Id (Pi A B) f g,
-- (p : (Pi x:A) Id (Bx) (fx,gx)); A not needed ??
-- | Ext
-- Ext B f g p : Id (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) -> Id (fiber f y) (s y) z
-- where fiber f y is Sigma x : A. Id B (f x) z.
| EquivEq
-- (A : U) -> (s : (y : A) -> pathTo A a) ->
-- (t : (y : B) -> (v : pathTo A a) -> Id (path To A a) (s y) v) ->
-- Id (Id U A A) (refl U A) (equivEq A A (id 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) -> Id 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:Id A a0 a1) -> 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:U)(F:A -> U) (C:U) (f: (x:A) -> F x -> C) (a0 a1 : A) (p:Id A a0 a1)
-- (b0:F a0) (b1:F a1) (q : IdS A F a0 a1 p b0 b1) -> Id C (f a0 b0) (f a1 b1)
| MapOnPathS -- TODO: AppOnPathS?
-- S1 : U
| Circle
-- base : S1
| Base
-- loop : Id S1 base base
| Loop
-- S1rec : (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]
-- 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 Val Val 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 Kan Com VU (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
| VLoop Name -- has type VCircle and connects base along the name
-- interval
| VI
| VI0
| VI1
| VLine Name -- connects start and end point along name
-- neutral values
| VApp Val Val -- the first Val must be neutral
| VAppName Val Name
| VSplit Val Val -- the second Val must be neutral
| VVar String Dim
| VInhRec Val Val Val Val -- the last Val must be neutral
| VCircleRec Val Val Val Val -- the last Val must be neutral
| VIntRec Val Val Val Val Val -- the last Val 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,g,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 (swap e x y)
VId a v0 v1 -> VId (sw a) (sw v0) (sw v1)
Path z v | z /= x && z /= y -> Path z (sw v)
| otherwise -> let z' = fresh ([x, y], v)
v' = swap v z z'
in Path 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 (swap z x y) (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 (swap z x y) (sw v0) (sw v1)
VCon c us -> VCon c (map sw us)
VEquivEq z a b f s t ->
VEquivEq (swap z x y) (sw a) (sw b) (sw f) (sw s) (sw t)
VPair z a v -> VPair (swap z x y) (sw a) (sw v)
VEquivSquare z w a s t ->
VEquivSquare (swap z x y) (swap w x y) (sw a) (sw s) (sw t)
VSquare z w v -> VSquare (swap z x y) (swap w x y) (sw v)
Kan Fill a b -> Kan Fill (sw a) (swap b x y)
VFillN a b -> VFillN (sw a) (swap b x y)
Kan Com a b@(Box _ z _ _)
| z /= x && z /= y -> Kan Com (sw a) (swap b x y)
| otherwise -> let z' = fresh ([x, y], u)
a' = swap a z z'
in sw (Kan Com a' (swap b z z'))
VComN a b@(Box _ z _ _)
| z /= x && z /= y -> VComN (sw a) (swap b x y)
| otherwise -> let z' = fresh ([x, y], u)
a' = swap a z z'
in sw (VComN a' (swap b z z'))
VComp b@(Box _ z _ _)
| z /= x && z /= y -> VComp (swap b x y)
| otherwise -> let z' = fresh ([x, y], u)
in sw (VComp (swap b z z'))
VFill z b@(Box dir n _ _)
| z /= x && z /= y -> VFill z (swap b x y)
| otherwise -> let
z' = fresh ([x, y], b)
in sw (VFill z' (swap b z z'))
VApp u v -> VApp (sw u) (sw v)
VAppName u n -> VAppName (sw u) (swap n x y)
VSplit u v -> VSplit (sw u) (sw v)
VVar s d -> VVar s (swap d x y)
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 (swap z x y)
VCircleRec f b l a -> VCircleRec (sw f) (sw b) (sw l) (sw a)
VI -> VI
VI0 -> VI0
VI1 -> VI1
VLine z -> VLine (swap z x y)
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 = do (_,t) <- lookupIdent x defs; return t
getBinder :: Ident -> [(Binder,a)] -> Maybe Binder
getBinder x defs = do (b,_) <- lookupIdent x defs; return b
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,g,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