{-# OPTIONS -fglasgow-exts #-}

module LISS.PrettyPrinter where

import LISS.Syntax

import UU.Pretty

-- Pretty Printing utilities
paren, block :: PP_Doc -> PP_Doc
paren e = pp "(" >|< e >|< pp ")"
block e = pp " {" >-< e >-< pp " }"

pplist [] _ _ = empty
pplist [x] _ _ = pp x
pplist (h:t) sep comb = (pp h >|< sep) `comb` (pplist t sep comb)

pplistH a b = pplist a b (>|<)
pplistV a b = pplist a b (>-<)

ws = pp " "

-- Pretty Printing
instance PP Liss where
  pp (Liss pName body) = 
      pp "program " >|< pp pName >|< block (pp body)

instance PP Body where
  pp (Body decs stat) = 
      pp "declarations" 
    >-<
      ppDeclarations decs 
    >-< 
      pp "\nstatements" 
    >-<
      pp stat >|< pp ";"

-- For functions, print also the return statement
ppFB (Body decs stat) rs = 
      pp "declarations" 
    >-<
      ppDeclarations decs 
    >-< 
      pp "\nstatements" 
    >-<
      pp stat >|< pp ";" >-< pp rs >|< pp ";"

instance PP ReturnStat where
  pp (ReturnInt ie)   = pp "return " >|< pp ie
  pp (ReturnBool be)  = pp "return " >|< pp be
  pp (ReturnSeq se)   = pp "return " >|< pp se
  pp (ReturnSet se)   = pp "return " >|< pp se
  pp (ReturnArray ae) = pp "return " >|< pp ae

ppDeclarations :: Declarations -> PP_Doc
ppDeclarations l = pplistV (map pp l) ";" >|< pp ";"

instance PP Declaration where
--  pp (VarDec vars typ) =
--    pplist (map pp vars) ", " (>|<) >|< pp " -> " >|< pp typ
  pp (VarDec (Arg var typ)) =
    pp var >|< pp " -> " >|< pp typ
  pp (SubprogDec specs pn as rt fb rs) =
    pplistV (map pp specs) "; " >-< pp "subProgram " >|< pp pn 
      >|< paren (pplistH as ",") >|< pp " -> " >|< pp rt >|< block (ppFB fb rs)

instance PP Spec where
  pp (Pre p)  = pp "pre "  >|< pp p
  pp (Post p) = pp "post " >|< pp p

instance PP Term where
  pp (TIntConst i)    = pp i
  pp (TIntVar iv)     = pp iv
  pp (TNegative ie)   = pp "!" >|< pp ie
  pp (TSum ie1 ie2)   = paren $ pp ie1 >|< pp " + " >|< pp ie2
  pp (TSub ie1 ie2)   = paren $ pp ie1 >|< pp " - " >|< pp ie2
  pp (TMult ie1 ie2)  = paren $ pp ie1 >|< pp " * " >|< pp ie2
  pp (TDiv ie1 ie2)   = paren $ pp ie1 >|< pp " / " >|< pp ie2
  pp (TRem ie1 ie2)   = paren $ pp ie1 >|< pp " % " >|< pp ie2
  pp (THead se)           = paren $ pp "head " >|< pp se
  pp (TIntFun fn vs) = pp fn >|< paren (pplistH vs ",")
  pp (TArrayAccess a b) = a >|< "[" >|< b >|< "]"
  pp (TOld v)	      = pp "old" >|< paren (pp v)
--  pp (TOldPos v p)    = pp "old" >|< paren (v >|< "[" >|< p >|< "]")
  pp Result	      = pp "result"

instance PP Predicate where
  pp (PBoolConst b)        = pp b
  pp (PBoolVar bv)	   = pp bv
  pp (PNegation be)        = pp "!" >|< pp be
  pp (PEqual ie1 ie2)      = paren $ pp ie1 >|< pp " == "  >|< pp ie2
  pp (PDiff ie1 ie2)       = paren $ pp ie1 >|< pp " != "  >|< pp ie2
  pp (PLesser ie1 ie2)     = paren $ pp ie1 >|< pp " < "   >|< pp ie2
  pp (PLessEq ie1 ie2)     = paren $ pp ie1 >|< pp " <= "  >|< pp ie2
  pp (PGreater ie1 ie2)    = paren $ pp ie1 >|< pp " > "   >|< pp ie2
  pp (PGreatEq ie1 ie2)    = paren $ pp ie1 >|< pp " >= "  >|< pp ie2
  pp (PConj be1 be2)       = paren $ pp be1 >|< pp " && "  >|< pp be2
  pp (PDisj be1 be2)       = paren $ pp be1 >|< pp " || "  >|< pp be2
  pp (PImp be1 be2)        = paren $ pp be1 >|< pp " => "  >|< pp be2
  pp (PEquiv be1 be2)      = paren $ pp be1 >|< pp " <=> " >|< pp be2
  pp (PEmptySeq se)        = paren $ pp "emptySeq " >|< pp se
  pp (PElemSet ie se)      = paren $ pp "elemSet " >|< pp ie >|< ws >|< pp se
  pp (PBoolFunction fn v)  = pp fn >|< paren (pp v)
  pp (PIfThenElse t p1 p2) = pp "if" >|< paren (pp t) 
			       >|< pp " then " >|< paren (pp p1)  
				 >|< pp " else " >|< paren (pp p2)
  pp (Forall as p)	   = pp "forall" >|< paren (pplistH as ",") >|< pp ": " >|< pp p
  pp (Exists as p)	   = pp "exists" >|< paren (pplistH as ",") >|< pp ": " >|< pp p
  pp (ValidIndex t1 t2)	   = pp "valid_index" >|< paren (t1 >|< "," >|< t2)

instance PP Arg where
  pp (Arg an ty) = pp an >|< pp " -> " >|< pp ty

instance PP IntExp where
  pp (IntConst i)        = pp i
  pp (IntVarExp iv)      = pp iv
  pp (ArrayAccess av ie) = pp av >|< pp "[" >|< pp ie >|< pp "]"
  pp (Negative ie)       = pp "-" >|< pp ie
  pp (Sum ie1 ie2)       = paren $ pp ie1 >|< pp " + " >|< pp ie2
  pp (Sub ie1 ie2)       = paren $ pp ie1 >|< pp " - " >|< pp ie2
  pp (Mult ie1 ie2)      = paren $ pp ie1 >|< pp " * " >|< pp ie2
  pp (Div ie1 ie2)       = paren $ pp ie1 >|< pp " / " >|< pp ie2
  pp (Rem ie1 ie2)       = paren $ pp ie1 >|< pp " % " >|< pp ie2
  pp (Head se)           = paren $ pp "head " >|< pp se
  pp (IntFunction fn vs) = pp fn >|< paren (pplistH vs ",")

instance PP SeqExp where
  pp (SeqVarExp sv)      = pp sv
  pp (SeqConst ies)      = pp "[" >|< pplistH ies "," >|< pp "]"
  pp SeqNull             = pp "[]"
  pp (Tail se)           = paren $ pp "tail " >|< pp se
  pp (Cons ie se)        = paren $ pp "cons " >|< pp ie >|< ws >|< pp se
  pp (SeqFunction fn vs) = pp fn >|< paren (pplistH vs ",")

instance PP SetExp where
  pp (SetVarExp sv)      = pp sv
  pp (SetConst iv ie)    = pp "{ " >|< pp iv >|< pp " | " >|< pp ie >|< pp " }"
  pp SetNull             = pp "{ }"
  pp (Union se1 se2)     = paren $ pp "union " >|< pp se1 >|< ws >|< pp se2
  pp (Intersect se1 se2) = paren $ pp "intersect " >|< pp se1 >|< ws >|< pp se2
  pp (SetFunction fn vs) = pp fn >|< paren (pplistH vs ",")

instance PP ArrayExp where
  pp (ArrayVarExp av)      = pp av
  pp (ArrayFunction fn vs) = pp fn >|< paren (pplistH vs ",")

instance PP Bool where
  pp = pp . show

instance PP BoolExp where
  pp (BoolConst b)       = pp b
  pp (BoolVarExp bv)     = pp bv
  pp (Negation be)       = pp "!" >|< pp be
  pp (Equal ie1 ie2)     = paren $ pp ie1 >|< pp " == "  >|< pp ie2
  pp (Diff ie1 ie2)      = paren $ pp ie1 >|< pp " != "  >|< pp ie2
  pp (Lesser ie1 ie2)    = paren $ pp ie1 >|< pp " < "   >|< pp ie2
  pp (LessEq ie1 ie2)    = paren $ pp ie1 >|< pp " <= "  >|< pp ie2
  pp (Greater ie1 ie2)   = paren $ pp ie1 >|< pp " > "   >|< pp ie2
  pp (GreatEq ie1 ie2)   = paren $ pp ie1 >|< pp " >= "  >|< pp ie2
  pp (Conj be1 be2)      = paren $ pp be1 >|< pp " && "  >|< pp be2
  pp (Disj be1 be2)      = paren $ pp be1 >|< pp " || "  >|< pp be2
  pp (Imp be1 be2)       = paren $ pp be1 >|< pp " => "  >|< pp be2
  pp (Equiv be1 be2)     = paren $ pp be1 >|< pp " <=> " >|< pp be2
  pp (EmptySeq se)       = paren $ pp "emptySeq " >|< pp se
  pp (ElemSet ie se)     = paren $ pp "elemSet " >|< pp ie >|< ws >|< pp se
  pp (BoolFunction fn v) = pp fn >|< paren (pp v)

instance PP Type where
  pp Integer   = pp "Integer"
  pp Boolean   = pp "Boolean"
  pp Sequence  = pp "Sequence"
  pp Set       = pp "Set"
  pp (Array n) = pp "Array[" >|< pp n >|< pp "]"

instance PP Statement where
  pp (IntAssign intVar intExp) = pp intVar >|< pp " := " >|< pp intExp
  pp (SetAssign setVar setExp) = pp setVar >|< pp " := " >|< pp setExp
  pp (SeqAssign seqVar seqExp) = pp seqVar >|< pp " := " >|< pp seqExp
  pp (BoolAssign boolVar boolExp) = pp boolVar >|< pp " := " >|< pp boolExp
  pp (ArrayPosAssign av pos ie) = pp av >|< pp "[" >|< pp pos >|< pp "] := " >|< pp ie
  pp (SequenceS s1 s2) = pp s1 >|< pp ";" >-< pp s2
  pp (IfThenElse ce te ee) = pp_ite "if" " then " " else " "" (pp ce) (block (pp te >|< pp ";")) (block (pp ee >|< pp ";"))
  pp (While la be s) = la >-< pp "while" >|< pp be >|< pp " {"
    >-<
      pp s >|< pp ";"
    >-<
      pp "}"
  pp (For iv ie1 ie2 step be s) = 
    pp "for" >|< paren (pp iv >|< pp " in " >|< pp ie1 >|< pp " to " >|< pp ie2) 
      >|< pp " step " >|< pp step >|< ws 
      >|< pp "satisfying " >|< paren (pp be) >|< block (pp s >|< pp ";")
  pp (ForEach iv se be s) = 
    pp "foreach" >|< paren (pp iv >|< pp " inSeq " >|< pp se) 
      >|< pp " satisfying " >|< paren (pp be) >|< block (pp s >|< pp ";")
  pp (Read iv) = pp "read " >|< iv
  pp (Write ie) = pp "write " >|< ie
  pp (WriteString s) = pp "write \"" >|< s >|< "\""
  pp Skip = pp "skip"

instance PP (Assertion, Maybe WfArg) where -- LoopAnnot
  pp (a,Just wfa) = "invariant " >|< a >|< ";" >-< "variant " >|< wfa >|< ";"
  pp (a,Nothing) = "invariant " >|< a >|< ";"
