{-# 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