module Language.Haskell.FreeTheorems.Variations.PolySeq.PrettyPrint (prettyMarkedTyp, prettyUnMarkedTyp, prettyMarkedTerm, prettyUnMarkedTerm, prettyConstraint, prettyLabel, adjustTypAbstraction) where

import Text.PrettyPrint

import Language.Haskell.FreeTheorems.Variations.PolySeq.Syntax

prettyLabel :: Label -> Doc
prettyLabel l =
    case l of
      LVar (LabVar i) -> text ("v" ++ show i)
      LVal Nbr        -> text "n"
      LVal Epsilon    -> text "e"
      Non             -> text "?"


prettyMarkedTyp   = prettyTyp True
prettyUnMarkedTyp = prettyTyp False

prettyTyp :: Bool -> Typ -> Doc
prettyTyp mark tau =
    case tau of
      TVar (TypVar s)          -> text s
      TArrow l tau1 tau2       -> parens (fsep [prettyTyp mark tau1, if mark then text "->^" <> prettyLabel l else text "->",
						(prettyTyp mark tau2)])
      TAll   l (TypVar s) tau' -> parens (fsep [text "forall" <> if mark then text "^" <> (prettyLabel l) else empty,
						text s <> text ".", prettyTyp mark tau'])
      TList tau'               -> brackets (prettyTyp mark tau')
      TInt                     -> text "Int"
      TBool                    -> text "Bool"


prettyMarkedTerm   = prettyTerm True
prettyUnMarkedTerm = prettyTerm False

adjustTypAbstraction :: Bool -> Term -> Term
adjustTypAbstraction True t = t
adjustTypAbstraction _    t = 
    case t of
      TAbs _ t' -> adjustTypAbstraction False t'
      _         -> t

prettyTerm :: Bool -> Term -> Doc
prettyTerm mark t =
    case t of
      Var (TermVar s)        -> text s
      Abs (TermVar s) tau t' -> parens (fsep [text ("\\" ++ s ++ "::") <> prettyTyp mark tau <> text ".",
					      prettyTerm mark t'])
      App t1 t2              -> parens (fsep [prettyTerm mark t1,prettyTerm mark t2])
      TAbs (TypVar s) t'     -> parens (fsep [text ("/\\" ++ s ++ "."),prettyTerm mark t'])
      TApp t' tau            -> prettyTerm mark t' <> text "_" <> braces (prettyTyp mark tau)
      Nil tau                -> text "[]_" <> braces (prettyTyp mark tau)
      Cons t1 t2             -> parens (prettyTerm mark t1 <> text ":" <> prettyTerm mark t2)
      LCase t1 t2 (TermVar s1) (TermVar s2) t3 
	                     -> parens (fsep [text "case" <+> prettyTerm mark t1<+> text "of {[] ->",
					      prettyTerm mark t2 <> semi, text (s1 ++ ":" ++ s2 ++ " ->"),
					      prettyTerm mark t3 <> text "}"])
      Fix t'                 -> case t' of
			          Abs x tau (Var y) -> if x == y 
						       then text "undefined_" <> braces (prettyTyp mark tau)
						       else parens (text "fix" <+> prettyTerm mark t')
                                  _                 -> parens (text "fix" <+> prettyTerm mark t')
      LSeq (TermVar s) t1 t2 -> parens (fsep [text "let!", text s, equals, prettyTerm mark t1, text "in",
					      prettyTerm mark t2])
      Let  (TermVar s) t1 t2 -> parens (fsep [text "let", text s, equals, prettyTerm mark t1,
					      text "in",prettyTerm mark t2])
      Seq t1 t2              -> parens (text "seq" <+> prettyTerm mark t1 <+> prettyTerm mark t2)
      I i                    -> text (show i)
      Add t1 t2              -> parens (fsep [prettyTerm mark t1, text "+", prettyTerm mark t2])
      T                      -> text "True"
      F                      -> text "False"
      BCase t1 t2 t3         -> parens (fsep [text "if", prettyTerm mark t1, text "then", prettyTerm mark t2,
					      text "else", prettyTerm mark t3])


prettyConstraint :: Constraint -> Doc
prettyConstraint c =
    case c of
      Conj c1 c2 -> fsep [prettyConstraint c1, text " ^ ", prettyConstraint c2]
      Impl c1 c2 -> parens (fsep [prettyConstraint c1, text " -> ", prettyConstraint c2])
      Leq  l1 l2 -> parens (fsep [prettyLabel l1, text " <= ", prettyLabel l2])
      Eq   l1 l2 -> parens (fsep [prettyLabel l1, text " == ", prettyLabel l2])
      Tru        -> text "T"
      Fls        -> text "F"