{-# OPTIONS -fglasgow-exts -fallow-overlapping-instances #-}

module Why.PrettyPrinterFlattened where

import Why.SyntaxFlattened

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 (>-<)

pFun n t = n >|< paren (pplistH t ")(")

ws = pp " "

instance PP Bool where
  pp True  = pp "true"
  pp False = pp "false"

ppWhy :: [WhyF] -> PP_Doc
ppWhy why = pplistV why "\n"

-- Pretty Printing
--instance PP Term where
instance PP WhyF where
  pp (Const c)  = pp c
  pp (Sum a b)  = paren $ a >|< " + " >|< b
  pp (Sub a b)  = paren $ a >|< " - " >|< b
  pp (Mult a b) = paren $ a >|< " * " >|< b
  pp (Div a b)  = paren $ a >|< " / " >|< b
  pp (Rem a b)  = paren $ a >|< " % " >|< b
  pp (TNegation t) = paren $ "-" >|< t
  pp (TVar li) = pp li
  pp (TArrayAccess v t) = v >|< "[" >|< t >|< "]"
  pp (TOld v) = v >|< "@"
  pp (TFunction i t) = pFun i t
  pp (TResult) = pp "result"

--instance PP Constant where
  pp (IntConst c)  = pp c
  pp (RealConst c) = pp c
  pp (BoolConst c) = pp c
  pp Void	   = pp "void"

--instance PP Predicate where
  pp (PredTrue)	      = pp "true"
  pp (PredFalse)      = pp "false"
  pp (PVar i)	      = pp i
  pp (PFunction i t)  = pFun i t
  pp (Equal p1 p2)    = paren $ p1 >|< " = " >|< p2
  pp (Diff p1 p2)     = paren $ p1 >|< " <> " >|< p2
  pp (Lesser p1 p2)   = paren $ p1 >|< " < " >|< p2
  pp (LessEq p1 p2)   = paren $ p1 >|< " <= " >|< p2
  pp (Greater p1 p2)  = paren $ p1 >|< " > " >|< p2
  pp (GreatEq p1 p2)  = paren $ p1 >|< " >= " >|< p2
  pp (PNegation p)    = paren $ "not " >|< paren (pp p)
  pp (Conj p1 p2)     = paren $ p1 >|< " and " >|< p2
  pp (Disj p1 p2)     = paren $ p1 >|< " or " >|< p2
  pp (Imp p1 p2)      = paren $ p1 >|< " -> " >|< p2
  pp (Equiv p1 p2)    = paren $ p1 >|< " <-> " >|< p2
  pp (PIfThenElse t p1 p2) = "if " >|< paren (pp t) >|< " then " >|< paren (pp p1) >|< "else " >|< paren (pp p2)
  pp (Forall is ty ts p) = "forall " >|< pplistH is "," >|< " : " >|< ty >|< ws >|< ts >|< " . " >|< p
  pp (Exists is ty p) = "exists " >|< pplistH is "," >|< " : " >|< ty >|< " . " >|< p
  -- TODO: are the Triggers ok?

--instance PP (Identifiers, ValueType) where
  --pp = error "TODO: instance PP (Identifiers, ValueType)"

--instance PP Type where
  pp TInt = pp "int"
  pp TBool = pp "bool"
  pp TReal = pp "real"
  pp TUnit = pp "unit"
  pp (User i) = pp i

--instance PP LDeclaration where
  pp (DType e mtp i)	    = ppE e >|< "type " >|< pp mtp >|< ws >|< i
  pp (DLogic e is ty)	    = ppE e >|< "logic " >|< pplistH is "," >|< " : " >|< ty
  pp (DFunction i lbs ty t) = "function " >|< pFun i lbs >|< " : " >|< ty >-< "= " >|< t
  pp (DPredicate i lbs p)   = "predicate " >|< pFun i lbs >-< "= " >|< p
  pp (DAxiom i p)	    = "axiom " >|< i >|< " : " >-< p
  pp (DGoal i p)	    = "goal " >|< i >|< " : " >-< p

--instance PP LogicType where
  pp (Prop lats)       = pplistH lats "," >|< " -> prop"
  pp (LTArrow lats ty) = pplistH lats "," >|< " -> " >|< ty

--instance PP LogicArgType where
  pp (LATPrim ty)  = pp ty
  pp (LATArray ty) = pp ty >|< " array"

--instance PP SimpleValueType where
  pp (SVTPrim ty) = pp ty
  pp (SVTRef ty) = ty >|< " ref"
  pp (SVTArray ty) = ty >|< " array"

--instance PP ValueType where
  pp (Simple svt) = pp svt
  pp (VTArrow svt ct) = svt >|< " -> " >|< ct
  pp (VTLArrow i svt ct) = i >|< " : " >|< svt >|< " -> " >|< ct
 
--instance PP ComputationType where
  pp (CT mpre mi vt es mpos) = f mpre >|< g mi >|< vt >|< ws >|< es >|< h mpos
    where
      f = maybe empty (\a -> "{ " >|< a >|< " } ")
      h = maybe empty (\a -> "{ " >|< a >|< " } ")
      g = maybe empty (\a -> "returns " >|< a >|< " : ")

--instance PP Prog where
  pp (PConst c) = pp c
  pp (PIdent i) = pp i
  pp (RefAccess i) = "!" >|< i
  pp (Assign i p) = i >|< " := " >|< p
  pp (ArrayAccess i p) = i >|< "[" >|< p >|< "]"
  pp (ArrayAssign i p1 p2) = i >|< "[" >|< p1 >|< "] := " >|< p2
  pp (Infix p1 op p2) = paren $ p1 >|< op >|< p2
  pp (Symm p) = "-" >|< p
  pp (Not p) = paren $ "not " >|< p
  pp (LetIn i p1 p2) = "let " >|< i >|< " = " >|< p1 >|< " in " >-< p2
  pp (LetInRef i p1 p2) = "let " >|< i >|< " = ref " >|< p1 >|< " in " >-< p2
  pp (ProgIfThenElse p1 p2 mp3) = "if " >|< paren (pp p1) >|< " then " >|< p2 >|< maybe empty (\a -> " else " >|< a) mp3
  pp (While p1 la p2) = "while " >|< paren (pp p1) >|< " do " >|< la >|< ws >|< p2 >|< " done"
  pp (Seq p1 p2) = p1 >|< ";" >-< p2
  pp (Label l p) = l >|< ":" >-< p
  pp (Assert as p) = "assert {" >|< pplistH as "} {" >|< "};" >-< p
  pp (PPre pre p) = "{ " >|< pre >|< " }" >-< p
  pp (PPost1 p pos) = p >-< "{ " >|< pos >|< " }"
  pp (PPost2 p pos) = p >-< "{ { " >|< pos >|< " } }"
  pp (Fun bs p) = "fun " >|< ppBinders bs >|< " -> " >|< p
  pp (LetBind i bs p1 p2) = "let " >|< i >|< paren (pplistH bs ") (") >|< " = " >-< p1 >-< "in " >|< p2
  pp (LetRec rf mp) = "let rec " >|< rf >|< maybe empty (\a -> " in " >-< a) mp
  pp (App p1 p2) = p1 >|< ws >|< p2
  pp (Raise1 i mvt) = "raise " >|< i >|< maybe empty (\a -> " : " >|< a) mvt
  pp (Raise2 i p mvt) = "raise " >|< paren (i >|< ws >|< p) >|< maybe empty (\a -> " : " >|< a) mvt
  pp (TryWith p hs) = "try " >|< p >|< " with " >|< hs >|< " end"
  pp (Absurd mvt) = "absurd" >|< maybe empty (\a -> " : " >|< a) mvt
  pp (Block p) = "begin " >-< p >-< "end"

--instance PP InfixOp where
  pp OpPlus   = pp "+"
  pp OpMinus  = pp "-"
  pp OpMult   = pp "*"
  pp OpDiv    = pp "/"
  pp OpRem    = pp "%"
  pp OpEq     = pp "="
  pp OpNEq    = pp "<>"
  pp OpL      = pp "<"
  pp OpLE     = pp "<="
  pp OpG      = pp ">"
  pp OpGE     = pp ">="
  pp OpOr     = pp "||"
  pp OpAnd    = pp "&&"


--instance PP Handler where
  pp (Hand1 i p) = i >|< " -> " >|< p
  pp (Hand2 i1 i2 p) = i1 >|< ws >|< i2 >|< " -> " >|< p

--instance PP (Term, Maybe Identifier) where -- WfArg
--  pp (t,mi) = t >|< maybe empty (\a -> "for " >|< a) mi

--instance PP Declaration where
  pp (Let i mbs p) = "let " >|< i >|< ws >|< mbs >|< " = " >-< p
  pp (DLetRec rf) = "let rec " >|< rf
  pp (Parameter b is vt) = ppE b >|< "parameter " >|<  pplistH is "," >|< " : " >|< vt
  pp (Exception i mt) = "exception " >|< i >|< maybe empty (\a -> " of " >|< a) mt
  pp (L ld) = pp ld

ppE True  = pp "external "
ppE False = empty

ppBinders l = pplistH " " (map f l)
  where
    f (is,vt) = "(" >|< pplistH "," is >|< " : " >|< vt >|< ")"

instance PP a => PP (Maybe a) where
  pp Nothing  = empty
  pp (Just a) = pp a

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

instance PP (Identifier, WhyF) where -- LogicBinder
  pp (i, ty) = i >|< " : " >|< ty

instance PP (Maybe Identifiers, Maybe Identifiers, Maybe Identifiers) where -- Effects
  pp (m1, m2, m3) = 
    maybe empty (\a -> "reads " >|< pplistH "," a >|< "\n") m1 >|<
     maybe empty (\a -> "writes " >|< pplistH "," a >|< "\n") m2 >|<
       maybe empty (\a -> "raises " >|< pplistH "," a) m3

instance PP (WhyF, Maybe Identifier) where -- Assertion
  pp (p,mi) = p >|< maybe empty (\a -> " as " >|< a) mi

instance PP (Assertion, ExnConditions) where -- Post
  pp (a,exns) = a >|< ws >|< exns

instance PP (Identifier, Binders, WhyF, Maybe WfArg, WhyF) where -- RecFun
  pp (i,bs,vt,wfa,p) = i >|< ws >|< bs >|< " : " >|< vt >|< "{ variant " >|< wfa >|< " }" >|< " = " >|< p

instance PP (Identifier, Assertion) where -- ExnCondition
  pp (i,a) = " | " >|< i >|< " => " >|< a

instance PP (String, Maybe String) where -- LabIdentifier
  pp (i, l) = maybe (pp i) (\l' -> i >|< "@" >|< l') l
