Agda-2.3.2.2: src/transl/agda/ISyntax.hs
{-# OPTIONS -cpp #-}
#include "config.h"
{-|
Pretty printer for ISyntax (as def. in ISynType)
-}
module ISyntax( module ISynType
, module ISynEnv
--, module ISynPP
, noPar, getExpPos, getExpPosLast -- , pprId
, module Id
, module MetaVars
, module PluginType
) where
import Id
import MetaVars
import ISynType
import ISynEnv
import Data.List(groupBy)
import PluginType
-- import ISynPP
-- This is silly, but hbc does not import instance decl otherwise.
import PPrint
import BinParse (Fixity(..))
import Utilities(t,pp)
import Literal()
import Position
import CITrans(varScope)
instance PPrint Exp where
pPrint = ppExp
ppExp :: PDetail -> Int -> Exp -> IText
ppExp d p = go where
go e0 = case e0 of
(EVar x _ )-> ppUId d x
(EConst c _ )-> ppUId d c
(EConstV c xs)-> debFCV xs (ppUId d c)
(ESort _ n )-> pPrint d p n
(EAbs _ _ )-> ppQuant d p e0
(EProd _ _ )-> ppQuant d p e0
(EArrow h e1 e2) -> pparen (p > 8) (separate [pPrint d 9 e1 ~. t(if h then " |->" else " ->"), pPrint d 8 e2])
(EApp h [e1,e2] ) | isBinExp h -> ppBinExp d p h (snd e1) (snd e2)
(EApp h es )-> ppar 9 $ go10 h `appArgs` es
(EBinOp e1 op e2)-> ppBinExp d p op e1 e2
(EIf b e1 e2) -> pparen (p>0) (separate [t"if " ~. pp d b ~. t" then", nest 4 (pp d e1), t"else", nest 4 (pp d e2)])
(EDef ds e)-> ppar 8 $ if null ds && not deb
then go10 e
else (t"let "~. foldr1 (^.) (map (pp d) ds))^. t"in " ~. go10 e
#ifdef NEWSYNTAX
(ECon c [e1, e2] )
| isBinOp c -> ppOp'' d p c (-666) (snd e1) (snd e2)
#endif
(ECon c es )-> ppCon c (t"" ) es
(EConF c e es )-> ppCon c (t"") es
(EData cbs)-> ppar 0 $ t"data " ~. ppCbs d cbs
(EIndData _ cbs)-> ppar 0 $ t"idata " `sepnest` ppIndCbs d cbs
(ECase e cbes )-> ppEcase d p e cbes
(EProj e i )-> ppar 12 $ go12 e ~. t"." ~. ppId d i
(ESig _ esigdefs )-> taggedblock "sig" esigdefs []
(EPackageType )-> t"Package "
(Epackage _ ds xs _ _ )-> taggedblock "package" ds xs
--(EpackageV _ ds xs _ _)-> taggedblock "package" ds xs
(EStruct _ ds xs _ _ )-> taggedblock "struct" ds xs
--(EStructV _ ds xs _ _)-> taggedblock "struct" ds xs
(EOpen e as b)-> (t"open " ~. go10 e ~. pp d as ~. t" in") ^. go10 b
(PreMeta )-> t"?"
(EMetaV m _ xs _ )-> debFCV xs (t("?"++show m))
(EMeta m _ _ cit pi maut) -> (if (isVisAut maut) then t"_" else t"?") ~. optnum where
optnum = if m==preMetaVar || readable then t""
else t("("++show m)~.pp PDDebug pi~.t")"
(EStop m e)-> if deb then pparen True (t(show m++"!")~.go e) else go e
(EClos env e)
| deb -> pparen True $ go e `sepnest` ppEnv d env
| readable -> go e
| otherwise -> case env `reducedFor` e of
(E (r,_))| null r -> go e
env' -> ppar 0 $ go e `sepnest` ppEnv d env'
(ELiteral _ l) -> t(ppReadable l)
(EExternal plugin) ->
t" external " ~. pp d plugin
( _ ) -> error "ppExp: unprintable"
ppQuant d p e = pparen (p > 8) $ separate (ppQuants d e)
where ppQuants :: PDetail -> Exp -> [IText]
ppQuants d (EAbs cb e) =
let cbs :: [(Bool,[UId],Exp)]
cbs = groupHidden cb
pcbs :: [IText]
pcbs = map (\cb -> t "\\" ~. pparg d 9 cb) cbs
in pcbs ++ ppQuants d e
ppQuants d (EProd cb e) =
let cbs = groupHidden cb
in map (pparg d 9) cbs ++ ppQuants d e
ppQuants d e = [pPrint d 8 e]
groupHidden :: ([(Bool,UId)],Exp)-> [(Bool,[UId],Exp)]
groupHidden (hxs,a) =
let hxss = groupBy (\(h,_) -> \(h',_) -> h == h') hxs
liftHidden :: [(Bool,UId)] -> (Bool,[UId],Exp)
liftHidden hxs' = let (hs,xs) = unzip hxs'
in (head hs,xs,a)
in map liftHidden hxss
pparg :: PDetail -> Int -> (Bool,[UId],Exp) -> IText
pparg d p (hidden,is,ty) = (pparen (p > 0)( (nsepList (map (ppUId d) is) (t",")) ~. t"::" ~. pPrint d 6 ty)) ~. t(if hidden then " |->" else " ->")
pplmds (EAbs bd e1) = t"\\"~.ppBind d 9 bd~.t" ->" : pplmds e1
pplmds e1 = [ppExp d 8 e1]
ppCon c pAt es | null es = ppar 12 $ ppc
| otherwise = ppar 9 $ ppc `appArgs` es
where ppc = ppId d c ~. pAt
taggedblock :: PPrint a => String -> [a] -> [UId] -> IText
taggedblock tag ds xs = debFCV xs $ ppar 8 $ if null ds then t(tag++" {}")
else separate $ [ t(tag++" {")
, nest 2 $ separate $ map ((~.(t";")) . pp d) ds , t"}"]
debFCV xs q = q -- if deb then q ^. t"FCVars="~. pp d xs else q
ppar n = pparen (p > n)
deb = d == PDDebug
readable = d == PDReadable
go10 = ppExp d 10
go12 = ppExp d 12
prArg (True,e) = text "|" ~. ppExp d 10 e
prArg (False,e) = ppExp d 10 e
appArgs q es = separate (q:map (nest 2 . prArg) es)
andargs q es = separate (q:map (nest 2 . go10) es)
sepnest q r = separate [q, nest 2 r]
reducedFor :: Environment -> Exp -> Environment
-- not correct, since indcase may insert free vars in a gamma.
env `reducedFor` e = case e of
(EStruct _ _ xs _ _ )-> remwith xs
--(EStructV _ _ xs _ _)-> remwith xs
(EConstV _ xs )-> remwith xs
(Epackage _ _ xs _ _ )-> remwith xs
--(EpackageV _ _ xs _ _)-> remwith xs
(EMeta _ _ _ (cit,_) _ _)-> remwith (varScope cit)
(EMetaV _ _ xs _ )-> remwith xs
( _ )-> removeEq env
where remwith xs = removeEq (retrieveE env xs)
{- still to go -}
instance PPrint Sort where
pPrint _ _ (Sort 0) = t"Set"
pPrint _ _ (Sort 1) = t"Type"
pPrint _ _ (Sort n) = t("#"++show n)
instance PPrint EProp where
pPrint _ _ p = t (tail (show p))
instance PPrint LetDef where
pPrint d p (DSimple def) = pPrint d p def
pPrint d p (DMutual ds) = (t"mutual " ~. foldr1 (^.) (map (pp d) ds))
instance PPrint Def where
pPrint d@PDDebug p (Def blocked _ ps c xs tel a (DExp e)) =
cseparate [sepList (map (pPrint d 0) ps) (t" "),
(if blocked then t"newtype " else t"")~.ppUId d c~.ppTel d 10 tel,
nest 4 $ t"::"~.pp d a~.t"=",
nest 2 $ pp d e,
t"fv="~.pPrint d 0 xs]
pPrint d p (Def blocked _ ps c _ [] a (DExp e)) =
separate [
separate [
separate ((map ((\s -> s ~. t" ") . pp d) ps)++ [(if blocked then t"newtype " else t"") ~. ppUId d c]) ,
nest 2 (t" :: " ~. pp d a)],
nest 2 (t"= " ~. pp d e)]
pPrint d p (Def blocked _ ps c _ tel a (DExp e)) =
separate [
separate [
separate [separate ((map ((\s -> s ~. t" ") . pp d) ps)
++[(if blocked then t"newtype " else t"") ~. ppUId d c]),
nest 2 (separate (map (ppBind d 12) tel))],
nest 2 (t" :: " ~. pp d a)],
nest 2 (t"= " ~. pp d e)]
pPrint d p (Def _ _ ps c _ tel a PN) =
separate[
separate [cseparate ((map ((\s -> s ~. t" ") . pp d) ps)++ [(t"postulate ")~.ppUId d c]), nest 2 (separate (map (ppBind d p) tel))],
nest 2 (t" :: " ~.pp d a)]
pPrint d p (Def _ _ ps c _ _ a Native) =
separate[
cseparate ((map ((\s -> s ~. t" ") . pp d) ps)++ [(t"native")~.ppUId d c]),
nest 2 (t" :: " ~.pp d a)]
pPrint d p (UnTypedDef blocked _ ps c _ (DExp e)) =
separate [
separate ((map ((\s -> s ~. t" ") . pp d) ps)++ [(if blocked then t"newtype " else t"") ~. ppUId d c]),
nest 2 (t"= " ~. pp d e)]
pPrint d p (UnTypedDef blocked _ ps c _ PN) =
cseparate ((map ((\s -> s ~. t" ") . pp d) ps)++ [(t"postulate ")~.ppUId d c])
pPrint d p (UnTypedDef _ _ ps c _ Native) =
cseparate ((map ((\s -> s ~. t" ") . pp d) ps)++ [(t"native ")~.ppUId d c])
pPrint d p (DOpen m as) = t"open " ~. pp d m ~. pp d as
instance PPrint Program where
pPrint d _ (Program ds) = foldr1 (^.) (map (pp d) ds)
ppBind :: PDetail -> Int -> Bind -> IText
ppBind d p (xs,a) = pparen (p > 0) ( nsepList (map (ppHUId d) xs) (t"," ) ~. t":: " ~. pPrint d 6 a)
where ppHUId d (hidden,x) = (if hidden then t"|" else t"") ~. ppUId d x
ppTel::PDetail -> Int -> Tel -> IText
ppTel d p ts = nseparate (map (ppBind d p) ts)
--ppSign:: PDetail -> Bind -> IText
--ppSign d (xs,a) = separate [nsepList (map (ppUId d) xs) (t"," ) ~. t" ::", nest 2 (pp d a )]
instance PPrint ESigDef where
pPrint d p (ESigAbs (xs,a)) = separate [nsepList (map (ppUId d.snd) xs) (t"," ) ~. t" ::", nest 2 (pp d a )]
pPrint d p (ESigDefn d') = pp d d'
ppCbs :: PDetail -> [ConBind] -> IText
ppCbs d cbs = sepList (map ppCon cbs) (t" |")
where ppCon (i, ts) = --separate (ppId d i : map (nest 2 . ppBind d 10) ts)
separate [ppId d i, nest 2 $ ppTel d 10 ts]
ppIndCbs :: PDetail -> [IndConBind] -> IText
ppIndCbs d indcbs = sepList (map ppIndCon indcbs) (t" |")
where ppIndCon ((i,ts),es) = separate
[ separate (ppId d i : map (nest 2 . pPrint d 10) ts)
, nest 2 . separate $ t":: _" : map (pPrint d 10) es]
instance PPrint OpenArg where
pPrint d _ (OpenConst ps c) = separate [separate (map (pp d) ps),ppUId d c]
pPrint d _ (OpenConstAs ps c1 c2) = sepList (map (pp d) ps) (t " ") ~. ppId d c1 ~. t" = " ~.ppUId d c2
pPrint d _(OpenConstT ps c a) = sepList (map (pp d) ps) (t " ") ~. ppUId d c ~. t" :: " ~. pPrint d 6 a
pPrint d _(OpenConstAsT ps i c a) = sepList (map (pp d) ps) (t " ") ~. ppUId d c ~. t" :: " ~. pPrint d 6 a ~. t" = "~. ppId d i
instance PPrint OpenArgs where
pPrint d p (OpenArgs us _) = t " use "~.sepList (map (pp d) us) (t",")
ppEq' d (x,e) = ppUId d x ~. t" = " ~. pPrint d 0 e
ppEq d (x,e) = case e of
EVar y _ | x == y -> (ppUId d x)
_ -> (ppUId d x ~. t"=" ~. pPrint d 0 e)
removeEq :: Environment -> Environment --- NOT CORRECT
removeEq (E (env,sigma)) = E ( removeEq' env,sigma)
where removeEq' env = filter uninteresting env
uninteresting (x,(EVar x' _)) = (toId x) /= (toId x')
uninteresting _ = True
instance PPrint PatArg where
pPrint d p (PArgT i a) = pparen (p > 0) $ ppUId d i ~.t"::"~. pp d a
pPrint d _ (PArg i) = ppUId d i
instance PPrint CaseBranch where
--pPrint PDDebug _ (CBCon i []) = ppId PDDebug i~.t"()"
--pPrint d p (CBCon i pas) = pparen (p>9) $ separate (ppId d i : map (pPrint d 10) pas)
pPrint d p (CBConM i pas _) =
pparen (p>9) $ separate (ppId d i : map (pPrint d 10) pas)
pPrint d p (CBLit _ l) = pPrint d p l
ppEcase :: PDetail -> Int -> Exp -> [(CaseBranch,Exp)] -> IText
ppEcase d p e [] = t"case " ~. pp d e ~. t" of { }"
ppEcase d p e arms
= pparen (p > 8) $ separate (t"case " ~. pp d e ~. t" of {" : [nest 2 (separate (map (\arm -> (ppBranch d arm) ~. t";") arms)), t"}"])
-- | otherwise = (t"case " ~. pp d e ~. t" of ") ^.
-- (nest 4 (foldr1 (^.) (map (ppBranch d) arms)))
where ppBranch d (br,e) = separate [pPrint d 10 br ~. t" -> ", nest 2 (pp d e)]
ppAbs :: PDetail -> Exp -> IText
ppAbs d e = separate (ppLmds d e)
where ppLmds d (EAbs b e) = (t "\\" ~. ppBind d 9 b ~. t(" ->") )
: (ppLmds d e)
ppLmds d e = [pPrint d 8 e]
ppProd p d e = pparen (p > 8) $ separate (ppProds p d e)
where ppProds p d (EProd b'@([(_,x)],b) a) =
if isDummyUId x
then (pPrint d 9 b ~. t(" ->")) : (ppProds 1 d a)
else (ppBind d 9 b' ~. t(" ->")) : (ppProds 8 d a)
ppProds p d (EProd b'@(x,b) a) =
(ppBind d 9 b' ~. t(" ->")) : (ppProds 8 d a)
ppProds _ d e = [pPrint d 8 e]
ppEnv :: PDetail -> Environment -> IText
ppEnv d env = pp d env
{-
instance PPrint Env where
pPrint PDDebug _ (Env []) = t"{}"
pPrint d@PDDebug _ (Env env) = t" where {" ~. csepList (map (ppEq d) env) (t",") ~. t"}"
pPrint d _ (Env []) = t""
pPrint d _ (Env env) = t" where " ~. foldr1 (^.) (map (ppEq d) env)
pPrint d p (EComp env1 env2) = pPrint d p env1
-}
instance PPrint Environment where
pPrint d p env =
if null xes then
if d == PDDebug then t"{}" else t""
else if d == PDDebug then t" where {" ~. csepList (map (ppEq d) xes) (t",") ~. t"}"
else t" where " ~. foldr1 (^.) (map (ppEq d) xes)
where xes = listEnv env
ppBinExp d pd e p1 p2 =
case e of
EVar x _ -> ppOp' d pd x p1 p2
EConst c _ -> ppOp' d pd c p1 p2
_ -> t"Internal error"
-- can't care less.
ppOp'' d@PDDebug pd i no p1 p2 =
let (p, lp, rp) =
case getFixity i of
FInfixl p -> (p, p, p+1)
FInfixr p -> (p, p+1, p)
FInfix p -> (p, p+1, p+1)
in pparen (d > PDReadable || pd>p)
(pPrint d lp p1 ~. t" " ~. ppInfix d i ~.t("#"++show no)~. t" " ~. pPrint d rp p2)
ppOp'' d pd i no p1 p2 =
let (p, lp, rp) =
case getFixity i of
FInfixl p -> (p, p, p+1)
FInfixr p -> (p, p+1, p)
FInfix p -> (p, p+1, p+1)
in pparen (d > PDReadable || pd>p)
(pPrint d lp p1 ~. t" " ~. ppInfix d i ~. t" " ~. pPrint d rp p2)
ppOp' d pd x = ppOp'' d pd (toId x) (getUIdNo x)
instance PPrint Drhs where
pPrint d _ (DExp e) = pp d e
pPrint d _ PN = t"PN"
pPrint _ _ Native = t"Native"
instance PPrint a => PPrint (Judgement a) where
pPrint d _ (IsType a) = t"type "~. pp d a
pPrint d _ (a :! v) = pp d a ~. t" :: " ~. pp d v
pPrintMJudg :: PDetail -> Judgement MetaVar -> IText
pPrintMJudg d (m :! v) = t("?"++show m++" :: ")~. pp d v
pPrintMJudg d (IsType m) = t("?"++show m++" Type")
-- Used for error messages
isBinExp :: Exp -> Bool
isBinExp (EVar x _) = isBinOp (toId x)
isBinExp (EConst c _) = isBinOp (toId c)
isBinExp (EConstV c _) = isBinOp (toId c)
isBinExp otherwise = False
precExp :: Exp -> Int
precExp (EVar _ _) = 12
precExp (EConst _ _) = 12
precExp (ESort _ _) = 12
precExp (EMeta _ _ _ _ _ _) = 12
precExp PreMeta = 12
precExp (EProj _ _) = 12
--precExp (EProjT _ _) = 12
precExp (EStruct _ _ _ _ _) = 12
precExp (Epackage _ _ _ _ _ ) = 12
precExp (ESig _ _) = 12
precExp (ECon _ [] ) = 12
precExp (EConF _ _ [] ) = 12
precExp (EStop _ e) = precExp e
precExp (EClos _ e) = precExp e
precExp (EProd ([(_,p)],_) _)
| isDummyUId p = 1
| otherwise = 9
precExp (EProd (p,_) _) = 9
precExp (EArrow _ e1 e2) = 1
precExp _ = 9
noPar :: Int
noPar = 0
getExpPos :: Exp -> Position
getExpPos (EVar x _) = getUIdPosition x
getExpPos (EConst c _) = getUIdPosition c
getExpPos (ESort pos _) = pos
getExpPos (EAbs b _) = getBindPos b
getExpPos (EProd b _) = getBindPos b
getExpPos (EArrow _ e1 _) = getExpPos e1
getExpPos (EApp h _) = getExpPos h
getExpPos (EDef [] e) = getExpPos e
getExpPos (EDef (l:_) _) = getLetDefPos l
getExpPos (ECon n _) = getIdPosition n
getExpPos (EConF n _ _) = getIdPosition n
getExpPos (EData []) = noPosition
getExpPos (EData ((n,_):_)) = getIdPosition n
getExpPos (EIndData _ (((n, _ ), _ ) :_ )) = getIdPosition n
getExpPos (ECase e _) = getExpPos e
getExpPos (EProj e _) = getExpPos e
--getExpPos (EProjT e _) = getExpPos e
getExpPos (ESig pos _) = pos
getExpPos (EStruct pos _ _ _ _ ) = pos
--getExpPos (EStructV pos _ _ _ _) = pos
getExpPos (Epackage pos _ _ _ _ ) = pos
--getExpPos (EpackageV pos _ _ _ _) = pos
getExpPos (EBinOp e _ _) = getExpPos e
getExpPos (EMeta _ pos _ _ _ _) = pos
getExpPos PreMeta = noPosition
getExpPos (EStop _ e) = getExpPos e
getExpPos (EClos _ e) = getExpPos e
getExpPos (EConstV c _) = getUIdPosition c
getExpPos (EOpen m _ _) = getExpPos m
--getExpPos (EUndef e) = getExpPos e
--getExpPos (EDefin e) = getExpPos e
getExpPos (ELiteral pos _) = pos
getExpPos _ = noPosition
getExpPosLast :: Exp -> Position
getExpPosLast (EAbs b e) = getExpPosLast e
getExpPosLast (EProd b e) = getExpPosLast e
getExpPosLast (EApp h []) = getExpPosLast h
getExpPosLast (EApp h es) = getExpPosLast (snd $ last es)
getExpPosLast (EDef _ e) = getExpPosLast e
getExpPosLast (ECon n []) = getIdPosition n
getExpPosLast (ECon n es) = getExpPosLast (snd$ last es)
getExpPosLast (EConF n e []) = getExpPosLast e
getExpPosLast (EConF n _ es) = getExpPosLast (snd$ last es)
getExpPosLast (EProj e x) = getIdPosition x
getExpPosLast (EBinOp _ _ e) = getExpPosLast e
getExpPosLast (EStop _ e) = getExpPosLast e
getExpPosLast (EClos _ e) = getExpPosLast e
getExpPosLast (EOpen _ _ e) = getExpPosLast e
getExpPosLast e = getExpPos e
getBindPos ((_,c):_,_) = getUIdPosition c
getBindPos (_,_) = error "getBindPos: "
getLetDefPos (DSimple d) = getDefPos d
getLetDefPos (DMutual (d:_)) = getDefPos d
getLetDefPos _ = error "getLetDefPos: "
getDefPos (Def _ _ _ c _ _ _ _) = getUIdPosition c
getDefPos (UnTypedDef _ _ _ c _ _) = getUIdPosition c
getDefPos (DOpen e _) = getExpPos e