BracketTypePattern k l _ -> bracket k $ ppWithCommas l
TypePatternArg t _ -> parens $ pretty t
-- | put proper brackets around a document
bracket :: BracketKind -> Doc -> Doc
-- | print a 'Kind' plus a preceding colon (or nothing)
printKind k = noPrint (k == universe) $ printVarKind InVar (VarKind k)
-- | print the kind of a variable with its variance and a preceding colon
printVarKind :: Variance -> VarKind -> Doc
printVarKind e vk = case vk of
Downset t -> less <+> pretty t
VarKind k -> colon <+> pretty e <> pretty k
data TypePrec = Outfix | Prefix | Lazyfix | ProdInfix | FunInfix | Absfix
parenPrec :: TypePrec -> (TypePrec, Doc) -> Doc
parenPrec p1 (p2, d) = if p2 < p1 then d else parens d
printTypeToken :: Token -> Doc
l = ("*", cross) : map ( \ (a, d) -> (show a, d) )
in case lookup (tokStr t) l of
printTypeId (Id ts cs _) = let (toks, pls) = splitMixToken ts in
fcat $ map printTypeToken toks
++ (if null cs then [] else [brackets $ sepByCommas $ map printTypeId cs])
++ map printTypeToken pls
toMixType :: Type -> (TypePrec, Doc)
toMixType typ = case typ of
TypeName name _ _ -> (Outfix, printTypeId name)
TypeToken tt -> (Outfix, printTypeToken tt)
(Absfix, sep [ lambda <+> pretty v, bullet <+> snd (toMixType t)])
ExpandedType t1 _ -> toMixType t1 -- here we print the unexpanded type
(Outfix, bracket k $ sepByCommas $ map (snd . toMixType) l)
(Lazyfix, fsep [parenPrec Lazyfix $ toMixType t, colon, pretty kind])
MixfixType ts -> (Prefix, fsep $ map (snd . toMixType) ts)
(topTy, tyArgs) = getTypeApplAux False typ
aArgs = (Prefix, sep [ parenPrec ProdInfix $ toMixType t1
, parenPrec Prefix $ toMixType t2 ])
TypeName name@(Id ts cs _) _k _i ->
case map toMixType tyArgs of
[e] | name == lazyTypeId ->
(Lazyfix, pretty e <+> parenPrec Lazyfix dArg)
[e1, e2, e3] | not (isPlace e1) && isPlace e2
&& not (isPlace e3) && null cs ->
(Outfix, fsep [pretty e1, snd dArg, pretty e3])
[dArg1, dArg2] -> case ts of
[_, e2, _] | isInfix name && null cs ->
if tokStr e2 == prodS then
[ parenPrec ProdInfix dArg1
, cross, parenPrec ProdInfix dArg2])
[ parenPrec FunInfix dArg1
, printTypeToken e2, snd dArg2])
dArgs -> if isProductIdWithArgs name $ length tyArgs then
(ProdInfix, fsep $ punctuate (space <> cross) $
map (parenPrec ProdInfix) dArgs) else aArgs
instance Pretty Type where
-- no curried notation for bound variables
instance Pretty TypeScheme where
pretty (TypeScheme vs t _) = let tdoc = pretty t in
if null vs then tdoc else
fsep [forallDoc, semiDs vs, bullet <+> tdoc]
instance Pretty Partiality where
instance Pretty Quantifier where
instance Pretty TypeQual where
instance Pretty Term where
pretty = printTerm . rmSomeTypes
isSimpleTerm :: Term -> Bool
isSimpleTerm trm = case trm of
ResolvedMixTerm _ _ _ _ -> True
BracketTerm _ _ _ -> True
-- | used only to produce CASL applications
isSimpleArgTerm :: Term -> Bool
isSimpleArgTerm trm = case trm of
QualVar vd -> not (isPatVarDecl vd)
ResolvedMixTerm n _ l _ -> placeCount n /= 0 || not (null l)
BracketTerm _ _ _ -> True
hasRightQuant :: Term -> Bool
hasRightQuant t = case t of
QuantifiedTerm {} -> True
LetTerm Let _ _ _ -> True
ResolvedMixTerm n _ ts _ | endPlace n && placeCount n == length ts
-> hasRightQuant (last ts)
ApplTerm (ResolvedMixTerm n _ [] _) t2 _ | endPlace n ->
TupleTerm ts _ | placeCount n == length ts -> hasRightQuant (last ts)
ApplTerm _ t2 _ -> hasRightQuant t2
zipArgs :: Id -> [Term] -> [Doc] -> [Doc]
zipArgs n ts ds = case (ts, ds) of
e = if hasRightQuant t then parens d else p
in if null r && null s && endPlace n then
[if hasRightQuant t then d else p]
isPatVarDecl :: VarDecl -> Bool
isPatVarDecl (VarDecl v ty _ _) = case ty of
TypeName t _ _ -> isSimpleId v && take 2 (show t) == "_v"
parenTermDoc :: Term -> Doc -> Doc
parenTermDoc trm = if isSimpleTerm trm then id else parens
printTermRec :: FoldRec Doc (Doc, Doc)
{ foldQualVar = \ _ vd@(VarDecl v _ _ _) ->
if isPatVarDecl vd then pretty v
else parens $ keyword varS <+> pretty vd
, foldQualOp = \ _ br n t tys _ -> (if null tys then id else
(<> brackets (ppWithCommas tys))) $
parens $ fsep [pretty br, pretty n, colon, pretty $
if isPred br then unPredTypeScheme t else t]
\ (ResolvedMixTerm _ _ os _) n@(Id toks cs ps) tys ts _ ->
let pn = placeCount n in if pn == length ts || null ts then
let ds = zipArgs n os ts in
if null tys then idApplDoc n ds
else let (ftoks, _) = splitMixToken toks
(fts, rts) = splitAt (placeCount fId) $ if null ts
then replicate pn $ pretty placeTok else ds
in fsep $ (idApplDoc fId fts <> brackets (ppWithCommas tys))
else idApplDoc applId [idDoc n, parens $ sepByCommas ts]
, foldApplTerm = \ (ApplTerm o1 o2 _) t1 t2 _ ->
-- comment out the following two guards for CASL applications
(ResolvedMixTerm n _ [] _, TupleTerm ts@(_ : _) _)
| placeCount n == length ts ->
idApplDoc n (zipArgs n ts $ map printTerm ts)
(ResolvedMixTerm n _ [] _, _) | placeCount n == 1
-> idApplDoc n $ zipArgs n [o2] [t2]
_ -> idApplDoc applId $ zipArgs applId [o1, o2] [t1, t2]
, foldTupleTerm = \ _ ts _ -> parens $ sepByCommas ts
, foldTypedTerm = \ (TypedTerm ot _ _ _) t q typ _ -> fsep [(case ot of
QuantifiedTerm {} -> parens
ApplTerm (ResolvedMixTerm n _ [] _) arg _ ->
let pn = placeCount n in case arg of
TupleTerm ts@(_ : _) _ | pn == length ts -> parens
_ -> id) t, pretty q, pretty typ]
, foldQuantifiedTerm = \ _ q vs t _ ->
fsep [pretty q, printGenVarDecls vs, bullet <+> t]
, foldLambdaTerm = \ _ ps q t _ ->
[p] -> if show p == "()" then empty else p
_ -> fcat $ map parens ps
Total -> bullet <> text exMark) <+> t]
, foldCaseTerm = \ _ t es _ ->
fsep [text caseS, t, text ofS,
cat $ punctuate (space <> bar <> space) $
map (printEq0 funArrow) es]
, foldLetTerm = \ _ br es t _ ->
let des = sep $ punctuate semi $ map (printEq0 equals) es
Let -> fsep [sep [text letS <+> des, text inS], t]
Where -> fsep [sep [t, text whereS], des]
Program -> text programS <+> des
, foldTermToken = \ _ t -> pretty t
, foldMixTypeTerm = \ _ q t _ -> pretty q <+> pretty t
, foldMixfixTerm = \ _ ts -> fsep ts
, foldBracketTerm = \ _ k l _ -> bracket k $ sepByCommas l
, foldAsPattern = \ _ (VarDecl v _ _ _) p _ ->
fsep [pretty v, text asP, p]
, foldProgEq = \ _ p t _ -> (p, t) }
printTerm = foldTerm printTermRec
{ foldQualOp = \ t _ i _ _ ps ->
if elem i $ map fst bList then
ResolvedMixTerm i [] [] ps else t
, foldTypedTerm = \ _ nt q ty ps ->
TypedTerm _ oq oty _ | oty == ty || oq == InType -> nt
QualVar (VarDecl _ oty _ _) | oty == ty -> nt
_ -> TypedTerm nt q ty ps }
rmSomeTypes :: Term -> Term
rmSomeTypes = foldTerm rmTypeRec
-- | put parenthesis around applications
ResolvedMixTerm _ _ [] _ -> t
_ -> TupleTerm [t] nullRange
{ foldApplTerm = \ _ t1 t2 ps ->
ApplTerm (addParAppl t1) (addParAppl t2) ps
, foldResolvedMixTerm = \ _ n tys ts ps ->
ResolvedMixTerm n tys (map addParAppl ts) ps
, foldTypedTerm = \ _ t q typ ps ->
TypedTerm (addParAppl t) q typ ps
, foldMixfixTerm = \ _ ts -> MixfixTerm $ map addParAppl ts
, foldAsPattern = \ _ v p ps -> AsPattern v (addParAppl p) ps
parenTerm :: Term -> Term
parenTerm = foldTerm parenTermRec
-- | print an equation with different symbols between 'Pattern' and 'Term'
printEq0 :: Doc -> (Doc, Doc) -> Doc
printEq0 s (p, t) = sep [p, hsep [s, t]]
printGenVarDecls :: [GenVarDecl] -> Doc
printGenVarDecls = fsep . punctuate semi . map
GenVarDecl (VarDecl _ t _ _) : _ -> sep
[ ppWithCommas (map ( \ (GenVarDecl (VarDecl v _ _ _)) -> v) l)
GenTypeVarDecl (TypeArg _ e c _ _ _ _) : _ -> sep
[ ppWithCommas (map ( \ (GenTypeVarDecl v) -> varOfTypeArg v) l)
_ -> error "printGenVarDecls") . groupBy sameType
sameType :: GenVarDecl -> GenVarDecl -> Bool
sameType g1 g2 = case (g1, g2) of
(GenVarDecl (VarDecl _ t1 Comma _), GenVarDecl (VarDecl _ t2 _ _))
(GenTypeVarDecl (TypeArg _ e1 c1 _ _ Comma _),
GenTypeVarDecl (TypeArg _ e2 c2 _ _ _ _)) | e1 == e2 && c1 == c2 -> True
printVarDeclType :: Type -> Doc
printVarDeclType t = case t of
instance Pretty VarDecl where
pretty (VarDecl v t _ _) = pretty v <+> printVarDeclType t
instance Pretty GenVarDecl where
GenTypeVarDecl tv -> pretty tv
instance Pretty TypeArg where
pretty (TypeArg v e c _ _ _ _) =
pretty v <+> printVarKind e c
-- | don't print an empty list and put parens around longer lists
printList0 :: (Pretty a) => [a] -> Doc
_ -> parens $ ppWithCommas l
instance Pretty BasicSpec where
pretty (BasicSpec l) = if null l then specBraces empty else
changeGlobalAnnos addBuiltins . vcat $ map pretty l
instance Pretty ProgEq where
pretty = printEq0 equals . foldEq printTermRec
instance Pretty BasicItem where
ProgItems l _ -> sep [keyword programS, semiAnnoted l]
Plain -> topSigKey (classS ++ if p then "es" else "") <+> b
Instance -> sep [keyword classS <+>
keyword (instanceS ++ if p then sS else ""), b]
GenVarItems l _ -> topSigKey (varS ++ pluralS l) <+> printGenVarDecls l
[ keyword freeS <+> keyword (typeS ++ pluralS l)
GenItems l _ -> let gkw = keyword generatedS in
(if all (isDatatype . item) l then \ i -> gkw <+> rmTopKey i
else \ i -> sep [gkw, specBraces i])
$ vcat $ map (printAnnoted pretty) l
AxiomItems vs fs _ -> sep
[ if null vs then empty else forallDoc <+> printGenVarDecls vs
_ -> let pp = addBullet . pretty in
vcat $ map (printAnnoted pp) (init fs)
++ [printSemiAnno pp True $ last fs]]
, specBraces $ vcat $ map (printAnnoted pretty) l]
plClass :: [Annoted ClassItem] -> Bool
plClass l = case map item l of
[ClassItem (ClassDecl (_ : _ : _) _ _) _ _] -> True
isDatatype :: SigItems -> Bool
isDatatype si = case si of
instance Pretty OpBrand where
pretty b = keyword $ show b
instance Pretty SigItems where
TypeItems i l _ -> let b = semiAnnos pretty l in case i of
Plain -> topSigKey ((if all (isSimpleTypeItem . item) l
then typeS else typeS) ++ plTypes l) <+> b
sep [keyword typeS <+> keyword (instanceS ++ plTypes l), b]
OpItems b l _ -> noNullPrint l $ topSigKey (show b ++ plOps l)
<+> let po = (prettyOpItem $ isPred b) in
OpDecl _ _ a@(_ : _) _ -> case last a of
then vcat (map (printSemiAnno po True) l)
plTypes :: [Annoted TypeItem] -> String
plTypes l = case map item l of
[TypeDecl (_ : _ : _) _ _] -> sS
[SubtypeDecl (_ : _ : _) _ _] -> sS
[IsoDecl (_ : _ : _) _] -> sS
plOps :: [Annoted OpItem] -> String
plOps l = case map item l of
[OpDecl (_ : _ : _) _ _ _] -> sS
isSimpleTypeItem :: TypeItem -> Bool
isSimpleTypeItem ti = case ti of
TypeDecl l k _ -> k == universe && all isSimpleTypePat l
SubtypeDecl l (TypeName i _ _) _ ->
not (isMixfix i) && all isSimpleTypePat l
SubtypeDefn p (Var _) t _ _ ->
isSimpleTypePat p && isSimpleType t
isSimpleTypePat :: TypePattern -> Bool
isSimpleTypePat tp = case tp of
TypePattern i [] _ -> not $ isMixfix i
isSimpleType :: Type -> Bool
isSimpleType t = case t of
TypeName i _ _ -> not $ isMixfix i
MixfixType[TypeToken _, BracketType Squares (_ : _) _] -> True
instance Pretty ClassItem where
pretty (ClassItem d l _) = pretty d $+$ noNullPrint l
(specBraces $ vcat $ map (printAnnoted pretty) l)
instance Pretty ClassDecl where
pretty (ClassDecl l k _) = let cs = ppWithCommas l in
if k == universe then cs else fsep [cs, less, pretty k]
instance Pretty Vars where
VarTuple vs _ -> parens $ ppWithCommas vs
instance Pretty TypeItem where
TypeDecl l k _ -> sep [ppWithCommas l, printKind k]
fsep [ppWithCommas l, less, pretty t]
IsoDecl l _ -> fsep $ punctuate (space <> equals) $ map pretty l
[pretty v, colon <+> pretty t, bullet <+> pretty f]]
AliasType p _ (TypeScheme l t _) _ ->
fsep $ pretty p : map (pretty . varOfTypeArg) l
++ [text assignS <+> pretty t]
prettyTypeScheme :: Bool -> TypeScheme -> Doc
prettyTypeScheme b = pretty . (if b then unPredTypeScheme else id)
prettyOpItem :: Bool -> OpItem -> Doc
prettyOpItem b oi = case oi of
OpDecl l t a _ -> fsep $ punctuate comma (map pretty l)
(if null a then id else (<> comma))(prettyTypeScheme b t)]
++ punctuate comma (map pretty a)
OpDefn n ps s t _ -> fcat $
((if null ps then (<> space) else id) $ pretty n)
: map ((<> space) . parens . semiDs) ps
++ (if b then [] else [colon <+> prettyTypeScheme b s <> space])
++ [(if b then equiv else equals) <> space, pretty t]
instance Pretty BinOpAttr where
pretty a = text $ case a of
instance Pretty OpAttr where
BinOpAttr a _ -> pretty a
UnitOpAttr t _ -> text unitS <+> pretty t
instance Pretty DatatypeDecl where
pretty (DatatypeDecl p k alts d _) =
fsep [ pretty p, printKind k, defn
<+> cat (punctuate (space <> bar <> space)
_ -> keyword derivingS <+> ppWithCommas d]
instance Pretty Alternative where
Constructor n cs p _ -> pretty n <+> fsep
(map ( \ l -> case (l, p) of
-- comment out the following line to output real CASL
([NoSelector (TypeToken t)], Total) | isSimpleId n -> pretty t
_ -> parens $ semiDs l) cs) <> pretty p
Subtype l _ -> text (if all isSimpleType l then typeS else typeS)
instance Pretty Component where
Selector n _ t _ _ -> sep [pretty n, colon <+> pretty t]
instance Pretty Symb where
sep $ pretty i : case mt of
Just (SymbType t) -> [colon <+> pretty t]
instance Pretty SymbItems where
pretty (SymbItems k syms _ _) =
printSK k syms <> ppWithCommas syms
instance Pretty SymbOrMap where
pretty (SymbOrMap s mt _) =
sep $ pretty s : case mt of
Just t -> [mapsto <+> pretty t]
instance Pretty SymbMapItems where
pretty (SymbMapItems k syms _ _) =
printSK k syms <> ppWithCommas syms
printSK :: SymbKind -> [a] -> Doc
_ -> keyword (drop 3 (show k) ++ case l of