module Gradual.PrettyPrinting where

import Language.Fixpoint.Types
import Language.Haskell.Liquid.GHC.Misc


class Pretty a where
  pretty :: a -> String 

instance Pretty Expr where
  pretty :: Expr -> String
pretty = Expr -> String
forall a. PPrint a => a -> String
showpp (Expr -> String) -> (Expr -> Expr) -> Expr -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> Expr
simplifyExpr 

instance Pretty KVar where
  pretty :: KVar -> String
pretty (KV Symbol
x) = Symbol -> String
forall a. Pretty a => a -> String
pretty Symbol
x  

instance Pretty Symbol where
  pretty :: Symbol -> String
pretty = Symbol -> String
forall a. Show a => a -> String
show (Symbol -> String) -> (Symbol -> Symbol) -> Symbol -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> Symbol
dropModuleNames(Symbol -> Symbol) -> (Symbol -> Symbol) -> Symbol -> Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> Symbol
tidySymbol

instance (Pretty a, Pretty b) => Pretty (a, b) where 
  pretty :: (a, b) -> String
pretty (a
x,b
y) = a -> String
forall a. Pretty a => a -> String
pretty a
x String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" |-> " String -> String -> String
forall a. [a] -> [a] -> [a]
++ b -> String
forall a. Pretty a => a -> String
pretty b
y 

instance (Pretty a) => Pretty [a] where 
  pretty :: [a] -> String
pretty [a]
xs = [String] -> String
unlines ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ (a -> String) -> [a] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map a -> String
forall a. Pretty a => a -> String
pretty [a]
xs 

simplifyExpr :: Expr -> Expr
simplifyExpr :: Expr -> Expr
simplifyExpr = Expr -> Expr
go 
  where
    go :: Expr -> Expr
go (ECst Expr
e Sort
_)   = Expr -> Expr
go Expr
e
    go (EApp Expr
e1 Expr
e2) 
      | EVar Symbol
x <- Expr -> Expr
go Expr
e1 
      , Symbol
x Symbol -> [Symbol] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Symbol
applyName, Symbol
toIntName, Symbol
setToIntName, Symbol
bitVecToIntName, Symbol
mapToIntName, Symbol
realToIntName] 
      = Expr -> Expr
go Expr
e2 
    go (EApp Expr
e1 Expr
e2)
      = Expr -> Expr -> Expr
EApp (Expr -> Expr
go Expr
e1) (Expr -> Expr
go Expr
e2)
    go (ENeg Expr
e)     = Expr -> Expr
ENeg (Expr -> Expr
go Expr
e)
    go (EBin Bop
b Expr
e1 Expr
e2) = Bop -> Expr -> Expr -> Expr
EBin Bop
b (Expr -> Expr
go Expr
e1) (Expr -> Expr
go Expr
e2)
    go (EIte Expr
e Expr
e1 Expr
e2) = Expr -> Expr -> Expr -> Expr
EIte (Expr -> Expr
go Expr
e) (Expr -> Expr
go Expr
e1) (Expr -> Expr
go Expr
e2)
    go (PAnd [Expr]
es)      = [Expr] -> Expr
PAnd (Expr -> Expr
go (Expr -> Expr) -> [Expr] -> [Expr]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Expr]
es)
    go (POr [Expr]
es)       = [Expr] -> Expr
POr (Expr -> Expr
go (Expr -> Expr) -> [Expr] -> [Expr]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Expr]
es)
    go (PNot Expr
e)       = Expr -> Expr
PNot (Expr -> Expr
go Expr
e)
    go (PImp Expr
e1 Expr
e2)   = Expr -> Expr -> Expr
PImp (Expr -> Expr
go Expr
e1) (Expr -> Expr
go Expr
e2)
    go (PIff Expr
e1 Expr
e2)   = Expr -> Expr -> Expr
PIff (Expr -> Expr
go Expr
e1) (Expr -> Expr
go Expr
e2)
    go (PAtom Brel
a Expr
e1 Expr
e2) = Brel -> Expr -> Expr -> Expr
PAtom Brel
a  (Expr -> Expr
go Expr
e1) (Expr -> Expr
go Expr
e2)
    go (PAll [(Symbol, Sort)]
a Expr
e) = [(Symbol, Sort)] -> Expr -> Expr
PAll [(Symbol, Sort)]
a (Expr -> Expr
go Expr
e)
    go (PExist [(Symbol, Sort)]
a Expr
e) = [(Symbol, Sort)] -> Expr -> Expr
PExist [(Symbol, Sort)]
a (Expr -> Expr
go Expr
e)
    go (ETApp Expr
e Sort
a) = Expr -> Sort -> Expr
ETApp (Expr -> Expr
go Expr
e) Sort
a
    go (ELam (Symbol, Sort)
a Expr
e) = (Symbol, Sort) -> Expr -> Expr
ELam (Symbol, Sort)
a (Expr -> Expr
go Expr
e)
    go (EVar Symbol
x)   = Symbol -> Expr
EVar (Symbol -> Symbol
dropModuleNames (Symbol -> Symbol) -> Symbol -> Symbol
forall a b. (a -> b) -> a -> b
$ Symbol -> Symbol
tidySymbol Symbol
x)
    go Expr
e            = Expr
e