{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TypeSynonymInstances #-}

module Sygus.Print (printSygus) where

import Sygus.Syntax

import Data.Semigroup
import Data.Text (Text, pack, intercalate)

class PrintSygus sy where
    printSygus :: sy -> Text

instance PrintSygus Lit where
    printSygus :: Lit -> Text
printSygus (LitNum Integer
i)
        | Integer
i forall a. Ord a => a -> a -> Bool
>= Integer
0 = [Char] -> Text
pack forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> [Char]
show Integer
i
        | Bool
otherwise = [Char] -> Text
pack forall a b. (a -> b) -> a -> b
$ [Char]
"(- " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show (forall a. Num a => a -> a
abs Integer
i) forall a. [a] -> [a] -> [a]
++ [Char]
")"
    printSygus (LitDec Integer
n Integer
d) = [Char] -> Text
pack (forall a. Show a => a -> [Char]
show Integer
n forall a. [a] -> [a] -> [a]
++ [Char]
"." forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Integer
d) 
    printSygus (LitBool Bool
b) = forall sy. PrintSygus sy => sy -> Text
printSygus Bool
b
    printSygus (Hexidecimal [Char]
s) = [Char] -> Text
pack [Char]
s
    printSygus (Binary [Char]
s) = [Char] -> Text
pack [Char]
s
    printSygus (LitStr [Char]
s) = Text
"\"" forall a. Semigroup a => a -> a -> a
<> [Char] -> Text
pack [Char]
s forall a. Semigroup a => a -> a -> a
<> Text
"\""

instance PrintSygus Symbol where
    printSygus :: [Char] -> Text
printSygus [Char]
s = [Char] -> Text
pack [Char]
s

instance PrintSygus [Cmd] where
    printSygus :: [Cmd] -> Text
printSygus = forall sy. PrintSygus sy => [sy] -> Text
printSygusList

instance PrintSygus Cmd where
    printSygus :: Cmd -> Text
printSygus Cmd
CheckSynth = Text
"(check-synth)"
    printSygus (Constraint Term
t) = Text
"(constraint " forall a. Semigroup a => a -> a -> a
<> forall sy. PrintSygus sy => sy -> Text
printSygus Term
t forall a. Semigroup a => a -> a -> a
<> Text
")"
    printSygus (DeclareVar [Char]
symb Sort
s) =
        Text
"(declare-var " forall a. Semigroup a => a -> a -> a
<> forall sy. PrintSygus sy => sy -> Text
printSygus [Char]
symb forall a. Semigroup a => a -> a -> a
<> Text
" " forall a. Semigroup a => a -> a -> a
<> forall sy. PrintSygus sy => sy -> Text
printSygus Sort
s forall a. Semigroup a => a -> a -> a
<> Text
")"
    printSygus (InvConstraint [Char]
s1 [Char]
s2 [Char]
s3 [Char]
s4) =
        Text
"(inv-constraint " forall a. Semigroup a => a -> a -> a
<> forall sy. PrintSygus sy => [sy] -> Text
printSygusList [[Char]
s1, [Char]
s2, [Char]
s3, [Char]
s4] forall a. Semigroup a => a -> a -> a
<> Text
")"
    printSygus (SetFeature Feature
f Bool
b) =
        Text
"(set-feature :" forall a. Semigroup a => a -> a -> a
<> forall sy. PrintSygus sy => sy -> Text
printSygus Feature
f forall a. Semigroup a => a -> a -> a
<> Text
" " forall a. Semigroup a => a -> a -> a
<> forall sy. PrintSygus sy => sy -> Text
printSygus Bool
b forall a. Semigroup a => a -> a -> a
<> Text
")"
    printSygus (SynthFun [Char]
symb [SortedVar]
sv Sort
s Maybe GrammarDef
gd) =
        Text
"(synth-fun " forall a. Semigroup a => a -> a -> a
<> forall sy. PrintSygus sy => sy -> Text
printSygus [Char]
symb forall a. Semigroup a => a -> a -> a
<> Text
" (" forall a. Semigroup a => a -> a -> a
<> forall sy. PrintSygus sy => [sy] -> Text
printSygusList [SortedVar]
sv forall a. Semigroup a => a -> a -> a
<> Text
") "
            forall a. Semigroup a => a -> a -> a
<> forall sy. PrintSygus sy => sy -> Text
printSygus Sort
s forall a. Semigroup a => a -> a -> a
<> Text
" " forall a. Semigroup a => a -> a -> a
<> forall sy. PrintSygus sy => sy -> Text
printSygus Maybe GrammarDef
gd forall a. Semigroup a => a -> a -> a
<> Text
")"
    printSygus (SynthInv [Char]
symb [SortedVar]
sv Maybe GrammarDef
gd) =
        Text
"(synth-inv " forall a. Semigroup a => a -> a -> a
<> forall sy. PrintSygus sy => sy -> Text
printSygus [Char]
symb forall a. Semigroup a => a -> a -> a
<> Text
" (" forall a. Semigroup a => a -> a -> a
<> forall sy. PrintSygus sy => [sy] -> Text
printSygusList [SortedVar]
sv forall a. Semigroup a => a -> a -> a
<> Text
") " forall a. Semigroup a => a -> a -> a
<> forall sy. PrintSygus sy => sy -> Text
printSygus Maybe GrammarDef
gd forall a. Semigroup a => a -> a -> a
<> Text
")"
    printSygus (SmtCmd SmtCmd
smt) = forall sy. PrintSygus sy => sy -> Text
printSygus SmtCmd
smt

instance PrintSygus Identifier where
    printSygus :: Identifier -> Text
printSygus (ISymb [Char]
symb) = forall sy. PrintSygus sy => sy -> Text
printSygus [Char]
symb
    printSygus (Indexed [Char]
symb [Index]
ind) =
        Text
"(_ " forall a. Semigroup a => a -> a -> a
<> forall sy. PrintSygus sy => sy -> Text
printSygus [Char]
symb forall a. Semigroup a => a -> a -> a
<> Text
" " forall a. Semigroup a => a -> a -> a
<> forall sy. PrintSygus sy => [sy] -> Text
printSygusList [Index]
ind forall a. Semigroup a => a -> a -> a
<> Text
")"

instance PrintSygus Index where
    printSygus :: Index -> Text
printSygus (IndNumeral Integer
i) = [Char] -> Text
pack forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> [Char]
show Integer
i
    printSygus (IndSymb [Char]
s) = forall sy. PrintSygus sy => sy -> Text
printSygus [Char]
s 

instance PrintSygus Sort where
    printSygus :: Sort -> Text
printSygus (IdentSort Identifier
i) = forall sy. PrintSygus sy => sy -> Text
printSygus Identifier
i
    printSygus (IdentSortSort Identifier
i [Sort]
xs) =
        Text
"(" forall a. Semigroup a => a -> a -> a
<> forall sy. PrintSygus sy => sy -> Text
printSygus Identifier
i forall a. Semigroup a => a -> a -> a
<> Text
" " forall a. Semigroup a => a -> a -> a
<> forall sy. PrintSygus sy => [sy] -> Text
printSygusList [Sort]
xs forall a. Semigroup a => a -> a -> a
<> Text
")"

instance PrintSygus Term where
    printSygus :: Term -> Text
printSygus (TermIdent Identifier
i) = forall sy. PrintSygus sy => sy -> Text
printSygus Identifier
i
    printSygus (TermLit Lit
l) = forall sy. PrintSygus sy => sy -> Text
printSygus Lit
l
    printSygus (TermCall Identifier
i [Term]
ts) =
        Text
"(" forall a. Semigroup a => a -> a -> a
<> forall sy. PrintSygus sy => sy -> Text
printSygus Identifier
i forall a. Semigroup a => a -> a -> a
<> Text
" " forall a. Semigroup a => a -> a -> a
<> forall sy. PrintSygus sy => [sy] -> Text
printSygusList [Term]
ts forall a. Semigroup a => a -> a -> a
<> Text
")"
    printSygus (TermExists [SortedVar]
sv Term
t) =
        Text
"(exists " forall a. Semigroup a => a -> a -> a
<> Text
"(" forall a. Semigroup a => a -> a -> a
<> forall sy. PrintSygus sy => [sy] -> Text
printSygusList [SortedVar]
sv forall a. Semigroup a => a -> a -> a
<> Text
")" forall a. Semigroup a => a -> a -> a
<> forall sy. PrintSygus sy => sy -> Text
printSygus Term
t forall a. Semigroup a => a -> a -> a
<> Text
")"
    printSygus (TermForAll [SortedVar]
sv Term
t) =
        Text
"(forall " forall a. Semigroup a => a -> a -> a
<> Text
"(" forall a. Semigroup a => a -> a -> a
<> forall sy. PrintSygus sy => [sy] -> Text
printSygusList [SortedVar]
sv forall a. Semigroup a => a -> a -> a
<> Text
")" forall a. Semigroup a => a -> a -> a
<> forall sy. PrintSygus sy => sy -> Text
printSygus Term
t forall a. Semigroup a => a -> a -> a
<> Text
")"
    printSygus (TermLet [VarBinding]
vb Term
t) =
        Text
"(let (" forall a. Semigroup a => a -> a -> a
<> forall sy. PrintSygus sy => [sy] -> Text
printSygusList [VarBinding]
vb forall a. Semigroup a => a -> a -> a
<> Text
") " forall a. Semigroup a => a -> a -> a
<> forall sy. PrintSygus sy => sy -> Text
printSygus Term
t forall a. Semigroup a => a -> a -> a
<> Text
")"

instance PrintSygus BfTerm where
    printSygus :: BfTerm -> Text
printSygus (BfIdentifier Identifier
i) = forall sy. PrintSygus sy => sy -> Text
printSygus Identifier
i
    printSygus (BfLiteral Lit
l) = forall sy. PrintSygus sy => sy -> Text
printSygus Lit
l
    printSygus (BfIdentifierBfs Identifier
i [BfTerm]
bfs) =
        Text
"(" forall a. Semigroup a => a -> a -> a
<> forall sy. PrintSygus sy => sy -> Text
printSygus Identifier
i forall a. Semigroup a => a -> a -> a
<> Text
" " forall a. Semigroup a => a -> a -> a
<> forall sy. PrintSygus sy => [sy] -> Text
printSygusList [BfTerm]
bfs forall a. Semigroup a => a -> a -> a
<> Text
")"

instance PrintSygus SortedVar where
    printSygus :: SortedVar -> Text
printSygus (SortedVar [Char]
symb Sort
s) =
        Text
"(" forall a. Semigroup a => a -> a -> a
<> forall sy. PrintSygus sy => sy -> Text
printSygus [Char]
symb forall a. Semigroup a => a -> a -> a
<> Text
" " forall a. Semigroup a => a -> a -> a
<> forall sy. PrintSygus sy => sy -> Text
printSygus Sort
s forall a. Semigroup a => a -> a -> a
<> Text
")"

instance PrintSygus VarBinding where
    printSygus :: VarBinding -> Text
printSygus (VarBinding [Char]
symb Term
t) =
        Text
"(" forall a. Semigroup a => a -> a -> a
<> forall sy. PrintSygus sy => sy -> Text
printSygus [Char]
symb forall a. Semigroup a => a -> a -> a
<> Text
" " forall a. Semigroup a => a -> a -> a
<> forall sy. PrintSygus sy => sy -> Text
printSygus Term
t forall a. Semigroup a => a -> a -> a
<> Text
")"

instance PrintSygus Feature where
    printSygus :: Feature -> Text
printSygus Feature
Grammars = Text
"grammars"
    printSygus Feature
FwdDecls = Text
"fwd-decls"
    printSygus Feature
Recursion = Text
"recursion"

instance PrintSygus SmtCmd where
    printSygus :: SmtCmd -> Text
printSygus (DeclareDatatype [Char]
symb DTDec
dt) =
        Text
"(declare-datatype " forall a. Semigroup a => a -> a -> a
<> forall sy. PrintSygus sy => sy -> Text
printSygus [Char]
symb forall a. Semigroup a => a -> a -> a
<> Text
" " forall a. Semigroup a => a -> a -> a
<> forall sy. PrintSygus sy => sy -> Text
printSygus DTDec
dt forall a. Semigroup a => a -> a -> a
<> Text
")"
    printSygus (DeclareDatatypes [SortDecl]
sd [DTDec]
dt) =
        Text
"(declare-datatypes (" forall a. Semigroup a => a -> a -> a
<> forall sy. PrintSygus sy => [sy] -> Text
printSygusList [SortDecl]
sd forall a. Semigroup a => a -> a -> a
<> Text
") (" forall a. Semigroup a => a -> a -> a
<> forall sy. PrintSygus sy => [sy] -> Text
printSygusList [DTDec]
dt forall a. Semigroup a => a -> a -> a
<> Text
"))" 
    printSygus (DeclareSort [Char]
symb Integer
i) =
        Text
"(declare-sort " forall a. Semigroup a => a -> a -> a
<> forall sy. PrintSygus sy => sy -> Text
printSygus [Char]
symb forall a. Semigroup a => a -> a -> a
<> Text
" " forall a. Semigroup a => a -> a -> a
<> forall sy. PrintSygus sy => sy -> Text
printSygus Integer
i forall a. Semigroup a => a -> a -> a
<> Text
")"
    printSygus (DefineFun [Char]
symb [SortedVar]
sv Sort
s Term
t) =
        Text
"(define-fun " forall a. Semigroup a => a -> a -> a
<> forall sy. PrintSygus sy => sy -> Text
printSygus [Char]
symb forall a. Semigroup a => a -> a -> a
<> Text
" (" forall a. Semigroup a => a -> a -> a
<> forall sy. PrintSygus sy => [sy] -> Text
printSygusList [SortedVar]
sv forall a. Semigroup a => a -> a -> a
<> Text
") "
            forall a. Semigroup a => a -> a -> a
<> forall sy. PrintSygus sy => sy -> Text
printSygus Sort
s forall a. Semigroup a => a -> a -> a
<> Text
" " forall a. Semigroup a => a -> a -> a
<> forall sy. PrintSygus sy => sy -> Text
printSygus Term
t forall a. Semigroup a => a -> a -> a
<> Text
")"
    printSygus (DefineSort [Char]
symb Sort
s) =
        Text
"(define-sort " forall a. Semigroup a => a -> a -> a
<> forall sy. PrintSygus sy => sy -> Text
printSygus [Char]
symb forall a. Semigroup a => a -> a -> a
<> Text
" " forall a. Semigroup a => a -> a -> a
<> forall sy. PrintSygus sy => sy -> Text
printSygus Sort
s forall a. Semigroup a => a -> a -> a
<> Text
")"
    printSygus (SetLogic [Char]
l) = Text
"(set-logic " forall a. Semigroup a => a -> a -> a
<> forall sy. PrintSygus sy => sy -> Text
printSygus [Char]
l forall a. Semigroup a => a -> a -> a
<> Text
")"
    printSygus (SetOption [Char]
symb Lit
l) =
        Text
"(set-option " forall a. Semigroup a => a -> a -> a
<> forall sy. PrintSygus sy => sy -> Text
printSygus [Char]
symb forall a. Semigroup a => a -> a -> a
<> Text
" " forall a. Semigroup a => a -> a -> a
<> forall sy. PrintSygus sy => sy -> Text
printSygus Lit
l forall a. Semigroup a => a -> a -> a
<> Text
")"

instance PrintSygus SortDecl where
    printSygus :: SortDecl -> Text
printSygus (SortDecl [Char]
symb Integer
i) =
        Text
"(" forall a. Semigroup a => a -> a -> a
<> forall sy. PrintSygus sy => sy -> Text
printSygus [Char]
symb forall a. Semigroup a => a -> a -> a
<> Text
" " forall a. Semigroup a => a -> a -> a
<> forall sy. PrintSygus sy => sy -> Text
printSygus Integer
i forall a. Semigroup a => a -> a -> a
<> Text
")"

instance PrintSygus DTDec where
    printSygus :: DTDec -> Text
printSygus (DTDec [DTConsDec]
dt) = Text
"(" forall a. Semigroup a => a -> a -> a
<> forall sy. PrintSygus sy => [sy] -> Text
printSygusList [DTConsDec]
dt forall a. Semigroup a => a -> a -> a
<> Text
")"

instance PrintSygus DTConsDec where
    printSygus :: DTConsDec -> Text
printSygus (DTConsDec [Char]
symb [SortedVar]
sv) = Text
"(" forall a. Semigroup a => a -> a -> a
<> forall sy. PrintSygus sy => sy -> Text
printSygus [Char]
symb forall a. Semigroup a => a -> a -> a
<> Text
" " forall a. Semigroup a => a -> a -> a
<> forall sy. PrintSygus sy => [sy] -> Text
printSygusList [SortedVar]
sv forall a. Semigroup a => a -> a -> a
<> Text
")"

instance PrintSygus GrammarDef where
    printSygus :: GrammarDef -> Text
printSygus (GrammarDef [SortedVar]
sv [GroupedRuleList]
grl) =
        Text
"(" forall a. Semigroup a => a -> a -> a
<> forall sy. PrintSygus sy => [sy] -> Text
printSygusList [SortedVar]
sv forall a. Semigroup a => a -> a -> a
<> Text
") (" forall a. Semigroup a => a -> a -> a
<> forall sy. PrintSygus sy => [sy] -> Text
printSygusList [GroupedRuleList]
grl forall a. Semigroup a => a -> a -> a
<> Text
")"

instance PrintSygus GroupedRuleList where
    printSygus :: GroupedRuleList -> Text
printSygus (GroupedRuleList [Char]
symb Sort
s [GTerm]
ts) =
        Text
"(" forall a. Semigroup a => a -> a -> a
<> forall sy. PrintSygus sy => sy -> Text
printSygus [Char]
symb forall a. Semigroup a => a -> a -> a
<> Text
" " forall a. Semigroup a => a -> a -> a
<> forall sy. PrintSygus sy => sy -> Text
printSygus Sort
s forall a. Semigroup a => a -> a -> a
<> Text
" (" forall a. Semigroup a => a -> a -> a
<> forall sy. PrintSygus sy => [sy] -> Text
printSygusList [GTerm]
ts forall a. Semigroup a => a -> a -> a
<> Text
"))"

instance PrintSygus GTerm where
    printSygus :: GTerm -> Text
printSygus (GConstant Sort
s) = Text
"(Constant " forall a. Semigroup a => a -> a -> a
<> forall sy. PrintSygus sy => sy -> Text
printSygus Sort
s forall a. Semigroup a => a -> a -> a
<> Text
")"
    printSygus (GVariable Sort
s) = Text
"(Variable " forall a. Semigroup a => a -> a -> a
<> forall sy. PrintSygus sy => sy -> Text
printSygus Sort
s forall a. Semigroup a => a -> a -> a
<> Text
")"
    printSygus (GBfTerm BfTerm
b) = forall sy. PrintSygus sy => sy -> Text
printSygus BfTerm
b

instance PrintSygus sy => PrintSygus (Maybe sy) where
    printSygus :: Maybe sy -> Text
printSygus (Just sy
s) = forall sy. PrintSygus sy => sy -> Text
printSygus sy
s
    printSygus Maybe sy
Nothing = Text
""

instance PrintSygus Integer where
    printSygus :: Integer -> Text
printSygus = [Char] -> Text
pack forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> [Char]
show

instance PrintSygus Bool where
    printSygus :: Bool -> Text
printSygus Bool
True = Text
"true"
    printSygus Bool
False = Text
"false"

printSygusList :: PrintSygus sy => [sy] -> Text
printSygusList :: forall sy. PrintSygus sy => [sy] -> Text
printSygusList = Text -> [Text] -> Text
intercalate Text
" " forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map forall sy. PrintSygus sy => sy -> Text
printSygus