content: {-# LANGUAGE OverloadedStrings,PatternGuards #-}
  module HipSpec.Lang.PrettyAltErgo where
  
  import Text.PrettyPrint
  
  import HipSpec.Lang.PolyFOL
  import HipSpec.Lang.PrettyUtils
  
  import Control.Monad
  
  prime :: Doc -> Doc
  prime d = "\'" <> d
  
  alphabet :: [String]
  alphabet = do
      n <- [1..]
      replicateM n ['a'..'z']
  
  commasep,commasepP :: [Doc] -> Doc
  commasep = sep . punctuate ","
  
  commasepP xs | length xs >= 2 = parens (commasep xs)
               | otherwise      = commasep xs
  
  ppClause :: PP a b -> Clause a b -> Doc
  ppClause p cls = case cls of
      SortSig x n
          -> "type" <+> commasepP (map (prime . text) (take n alphabet)) <+> pp_symb p x
  
      TypeSig x _tvs args res -> hang "logic" 2 (ppTySig p (pp_symb p x) args res)
  
      Clause name _trg cl _tvs phi -> hang (ppClType cl <+> "_" <> nm <+> ":") 2 (ppForm p phi)
        where
          nm = maybe empty int name
  
      Comment s            -> hang "(*" 2 (vcat (map text (lines s)) <+> "*)")
  
  ppClType :: ClType -> Doc
  ppClType cl = case cl of
      Axiom -> "axiom"
      Goal  -> "goal"
  
  ppTySig :: PP a b -> Doc -> [Type a b] -> Type a b -> Doc
  ppTySig p x args res
      = hang (x <+> ":") 2 (pp_args (ppType p res))
    where
      pp_args = case args of
          [] -> id
          _  -> hang (commasep (map (ppType p) args) <+> "->") 2
  
  ppType :: PP a b -> Type a b -> Doc
  ppType p = go
    where
      go t0 = case t0 of
          TyCon tc ts -> commasepP (map go ts) <+> pp_symb p tc
          TyVar x     -> prime (pp_var p x)
          TType       -> error "PrettyAltErgo.ppType: TType"
          Integer     -> "int"
  
  ppForm :: PP a b -> Formula a b -> Doc
  ppForm p f0 = case f0 of
      _ | Just (op,fs) <- collectFOp f0 -> inside "(" (ppFOp op) ")" (map (ppForm p) fs)
      Q q x t f         -> hang (ppQ q <+> ppTySig p (pp_var p x) [] t <+> ".") 2 (ppForm p f)
      TOp op t1 t2      -> sep [ppTerm p t1 <+> ppTOp op,ppTerm p t2]
      Neg f             -> "not" <+> parens (ppForm p f)
  --    Pred q fs         -> pp_symb p q <> csv (map (ppForm p) fs)
      FOp{}             -> error "PrettyAltErgo.ppForm: FOp"
      DataDecl _ fm     -> ppForm p fm
  
  ppQ :: Q -> Doc
  ppQ q = case q of
      Forall -> "forall"
      Exists -> "exists"
  
  ppFOp :: FOp -> Doc
  ppFOp op = case op of
      And     -> " and "
      Or      -> " or "
      Implies -> " -> "
      Equiv   -> " <-> "
  
  ppTOp :: TOp -> Doc
  ppTOp op = case op of
      Equal   -> "="
      Unequal -> "<>"
  
  ppTerm :: PP a b -> Term a b -> Doc
  ppTerm p = go
    where
      go tm0 = case tm0 of
          Apply f _ts as -> pp_symb p f <> empty {- ("(*" <+> csv (map (ppType p) ts) <+> "*)") -} <> csv (map go as)
          Var v         -> pp_var p v
          Lit x         -> integer x
  
  