module Language.EFLINT.Print where

import Prelude hiding (seq)

import Language.EFLINT.Spec
import Language.EFLINT.Interpreter  (Program(..))

import Data.List (intercalate, intersperse)

ppProgram :: Program -> String
ppProgram :: Program -> String
ppProgram Program
p = case Program
p of
  Program Phrase
p -> Phrase -> String
ppPhrase Phrase
p 
  PSeq Program
p1 Program
p2 -> Program -> String
ppProgram Program
p1 forall a. [a] -> [a] -> [a]
++ String
"\n" forall a. [a] -> [a] -> [a]
++ Program -> String
ppProgram Program
p2
  Program
ProgramSkip -> String
""

ppPhrase :: Phrase -> String
ppPhrase :: Phrase -> String
ppPhrase Phrase
p = case Phrase
p of
  PQuery Term
t          -> String
"?" forall a. [a] -> [a] -> [a]
++ Term -> String
ppTerm Term
t
  PInstQuery Bool
b [Var]
vs Term
t 
    | forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Var]
vs       -> String
keyw forall a. [a] -> [a] -> [a]
++ Term -> String
ppTerm Term
t
    | Bool
otherwise     -> String
keyw forall a. [a] -> [a] -> [a]
++ [Var] -> String -> String
foreach [Var]
vs (Term -> String
ppTerm Term
t)
   where keyw :: String
keyw | Bool
b         = String
"?--"
              | Bool
otherwise = String
"?-"
  PDo Tagged
t             -> Tagged -> String
ppTagged Tagged
t
  PTrigger [Var]
vs Term
t     -> [Var] -> String -> String
foreach [Var]
vs forall a b. (a -> b) -> a -> b
$ Term -> String
ppTerm Term
t
  Create [Var]
vs Term
t       -> String
"+" forall a. [a] -> [a] -> [a]
++ [Var] -> String -> String
foreach [Var]
vs (Term -> String
ppTerm Term
t)
  Terminate [Var]
vs Term
t    -> String
"-" forall a. [a] -> [a] -> [a]
++ [Var] -> String -> String
foreach [Var]
vs (Term -> String
ppTerm Term
t)
  Obfuscate [Var]
vs Term
t    -> String
"~" forall a. [a] -> [a] -> [a]
++ [Var] -> String -> String
foreach [Var]
vs (Term -> String
ppTerm Term
t)
  Phrase
PSkip             -> String
""
  PDeclBlock [Decl]
ds     -> [String] -> String
unlines (forall a b. (a -> b) -> [a] -> [b]
map Decl -> String
ppDecl [Decl]
ds)

ppCPhrase :: CPhrase -> String
ppCPhrase :: CPhrase -> String
ppCPhrase CPhrase
p = case CPhrase
p of 
  CPhrase
CPSkip          -> String
""
  CPhrase
CPOnlyDecls     -> String
""
  CSeq CPhrase
CPSkip CPhrase
p2  -> CPhrase -> String
ppCPhrase CPhrase
p2
  CSeq CPhrase
p1 CPhrase
CPSkip  -> CPhrase -> String
ppCPhrase CPhrase
p1
  CSeq CPhrase
p1 CPhrase
p2      -> [String] -> String
seq [CPhrase -> String
ppCPhrase CPhrase
p1,CPhrase -> String
ppCPhrase CPhrase
p2]
  CDo Tagged
te          -> Tagged -> String
ppTagged Tagged
te
  CTrigger [Var]
vs Term
t   -> [Var] -> String -> String
foreach [Var]
vs forall a b. (a -> b) -> a -> b
$ Term -> String
ppTerm Term
t
  CCreate [Var]
vs Term
t    -> String
"+" forall a. [a] -> [a] -> [a]
++ [Var] -> String -> String
foreach [Var]
vs (Term -> String
ppTerm Term
t)
  CTerminate [Var]
vs Term
t -> String
"-" forall a. [a] -> [a] -> [a]
++ [Var] -> String -> String
foreach [Var]
vs (Term -> String
ppTerm Term
t)
  CObfuscate [Var]
vs Term
t -> String
"~" forall a. [a] -> [a] -> [a]
++ [Var] -> String -> String
foreach [Var]
vs (Term -> String
ppTerm Term
t)
  CQuery Term
t        -> String
"?" forall a. [a] -> [a] -> [a]
++ Term -> String
ppTerm Term
t
  CInstQuery Bool
b [Var]
vs Term
t 
    |forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Var]
vs      -> String
keyw forall a. [a] -> [a] -> [a]
++ Term -> String
ppTerm Term
t
    |Bool
otherwise    -> String
keyw forall a. [a] -> [a] -> [a]
++ [Var] -> String -> String
foreach [Var]
vs (Term -> String
ppTerm Term
t)
   where keyw :: String
keyw | Bool
b         = String
"?--"
              | Bool
otherwise = String
"?-"
  CPDir CDirective
dir       -> case CDirective
dir of
   DirInv String
ty      -> String
"Invariant " forall a. [a] -> [a] -> [a]
++ String
ty   

ppDecl :: Decl -> String
ppDecl :: Decl -> String
ppDecl Decl
td = case Decl
td of 
  PlaceholderDecl String
f String
t -> String -> String -> String
ppPlaceholder String
f String
t
  TypeExt String
ty [ModClause]
clauses -> String -> [ModClause] -> String
ppTypeExt String
ty [ModClause]
clauses
  TypeDecl String
ty TypeSpec
tspec -> String -> TypeSpec -> String
ppDeclSpec String
ty TypeSpec
tspec

ppTypeExt :: DomId -> [ModClause] -> String
ppTypeExt :: String -> [ModClause] -> String
ppTypeExt String
ty [ModClause]
clauses = String
"Type extension of " forall a. [a] -> [a] -> [a]
++ String
ty -- TODO, requires knowing kind of extended type

ppDeclSpec :: DomId -> TypeSpec -> String
ppDeclSpec :: String -> TypeSpec -> String
ppDeclSpec String
d TypeSpec
tspec = case TypeSpec -> Kind
kind TypeSpec
tspec of
  Fact FactSpec
fspec  -> String -> TypeSpec -> FactSpec -> String
ppFact String
d TypeSpec
tspec FactSpec
fspec
  Duty DutySpec
dspec  -> String -> TypeSpec -> DutySpec -> String
ppDuty String
d TypeSpec
tspec DutySpec
dspec
  Event EventSpec
espec -> String -> TypeSpec -> EventSpec -> String
ppEvent String
d TypeSpec
tspec EventSpec
espec
  Act ActSpec
aspec   -> String -> TypeSpec -> ActSpec -> String
ppAct String
d TypeSpec
tspec ActSpec
aspec

ppDirective :: Directive -> String
ppDirective :: Directive -> String
ppDirective (Include String
fp) = String
"#include" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show String
fp
ppDirective (Require String
fp) = String
"#require" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show String
fp

ppClauses :: [ModClause] -> String
ppClauses :: [ModClause] -> String
ppClauses = [String] -> String
unwords forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> [a] -> [a]
intersperse String
" " forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ModClause -> [String]
ppClause

ppClause :: ModClause -> [String]
ppClause :: ModClause -> [String]
ppClause ModClause
clause = case ModClause
clause of
  ConditionedByCl [Term]
pres | Bool -> Bool
not (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Term]
pres) -> [[Term] -> String
ppPreConditions [Term]
pres]
  DerivationCl [Derivation]
dvs | Bool -> Bool
not (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Derivation]
dvs) -> [[Derivation] -> String
ppDerivRules [Derivation]
dvs]
  SyncCl [Sync]
ss | Bool -> Bool
not (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Sync]
ss) -> [] -- TODO
  PostCondCl [Effect]
effs | Bool -> Bool
not (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Effect]
effs) -> [[Effect] -> String
ppPostConditions [Effect]
effs]
  ViolationCl [Term]
vcs | Bool -> Bool
not (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Term]
vcs) -> [[Term] -> String
ppViolationConds [Term]
vcs] 
  EnforcingActsCl [String]
ds | Bool -> Bool
not (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [String]
ds) -> [[String] -> String
ppEnforcingActs [String]
ds] 
  ModClause
_ -> []

ppAct :: String -> TypeSpec -> ActSpec -> String
ppAct String
d TypeSpec
tspec ActSpec
aspec = String -> Domain -> Term -> [ModClause] -> String
ppAct' String
d (TypeSpec -> Domain
domain TypeSpec
tspec) (TypeSpec -> Term
domain_constraint TypeSpec
tspec) 
                        [[Derivation] -> ModClause
DerivationCl (TypeSpec -> [Derivation]
derivation TypeSpec
tspec) 
                        ,[Term] -> ModClause
ConditionedByCl (TypeSpec -> [Term]
conditions TypeSpec
tspec)
                        ,[Effect] -> ModClause
PostCondCl (ActSpec -> [Effect]
effects ActSpec
aspec)
                        ,[Sync] -> ModClause
SyncCl (ActSpec -> [Sync]
syncs ActSpec
aspec)
                        ]

-- TODO print syncs(?)
-- TODO recipient?
ppAct' :: String -> Domain -> Term -> [ModClause] -> String
ppAct' String
domainID Domain
domain Term
domain_constr [ModClause]
clauses = 
  String
"Act " forall a. [a] -> [a] -> [a]
++ String
domainID forall a. [a] -> [a] -> [a]
++ String
" Actor " forall a. [a] -> [a] -> [a]
++ Var -> String
ppVar Var
actor forall a. [a] -> [a] -> [a]
++ String
show_objects
    forall a. [a] -> [a] -> [a]
++ Term -> String
ppConstraint (Term
domain_constr)
    forall a. [a] -> [a] -> [a]
++ [ModClause] -> String
ppClauses [ModClause]
clauses
  where Products (Var
actor:[Var]
objects) = Domain
domain
        show_objects :: String
show_objects | forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Var]
objects = String
""
                     | Bool
otherwise    = String
" Related to " forall a. [a] -> [a] -> [a]
++ forall a. [a] -> [[a]] -> [a]
intercalate String
", " (forall a b. (a -> b) -> [a] -> [b]
map (\(Var String
x String
dec) -> String
xforall a. [a] -> [a] -> [a]
++String
dec) [Var]
objects)

ppPostConditions :: [Effect] -> String
ppPostConditions :: [Effect] -> String
ppPostConditions [Effect]
effects = String
created_facts forall a. [a] -> [a] -> [a]
++ String
terminated_facts forall a. [a] -> [a] -> [a]
++ String
obfuscated_facts
 where ([Effect]
createds, [Effect]
terminateds, [Effect]
obfs) = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Effect
-> ([Effect], [Effect], [Effect]) -> ([Effect], [Effect], [Effect])
op ([],[],[]) [Effect]
effects
         where op :: Effect
-> ([Effect], [Effect], [Effect]) -> ([Effect], [Effect], [Effect])
op e :: Effect
e@(CAll [Var]
_ Term
_) ([Effect]
cs,[Effect]
ts,[Effect]
os) = (Effect
eforall a. a -> [a] -> [a]
:[Effect]
cs,[Effect]
ts,[Effect]
os) 
               op e :: Effect
e@(TAll [Var]
_ Term
_) ([Effect]
cs,[Effect]
ts,[Effect]
os) = ([Effect]
cs,Effect
eforall a. a -> [a] -> [a]
:[Effect]
ts,[Effect]
os)
               op e :: Effect
e@(OAll [Var]
_ Term
_) ([Effect]
cs,[Effect]
ts,[Effect]
os) = ([Effect]
cs,[Effect]
ts,Effect
eforall a. a -> [a] -> [a]
:[Effect]
os)
       created_facts :: String
created_facts | forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Effect]
createds = String
""
                     | Bool
otherwise     = String
" Creates " forall a. [a] -> [a] -> [a]
++ forall a. [a] -> [[a]] -> [a]
intercalate String
", " (forall a b. (a -> b) -> [a] -> [b]
map Effect -> String
ppEffect [Effect]
createds)
       terminated_facts :: String
terminated_facts | forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Effect]
terminateds = String
""
                        | Bool
otherwise = String
" Terminates " forall a. [a] -> [a] -> [a]
++ forall a. [a] -> [[a]] -> [a]
intercalate String
", " (forall a b. (a -> b) -> [a] -> [b]
map Effect -> String
ppEffect [Effect]
terminateds)
       obfuscated_facts :: String
obfuscated_facts | forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Effect]
obfs = String
""
                        | Bool
otherwise = String
" Obfuscates " forall a. [a] -> [a] -> [a]
++ forall a. [a] -> [[a]] -> [a]
intercalate String
", " (forall a b. (a -> b) -> [a] -> [b]
map Effect -> String
ppEffect [Effect]
obfs)

ppPreConditions :: [Term] -> String
ppPreConditions :: [Term] -> String
ppPreConditions [] = String
""
ppPreConditions [Term]
ts = String
" Conditioned by " forall a. [a] -> [a] -> [a]
++ forall a. [a] -> [[a]] -> [a]
intercalate String
", " (forall a b. (a -> b) -> [a] -> [b]
map Term -> String
ppTerm [Term]
ts)

ppEvent :: String -> TypeSpec -> EventSpec -> String
ppEvent String
d TypeSpec
tspec EventSpec
espec = String -> Domain -> Term -> [ModClause] -> String
ppEvent' String
d (TypeSpec -> Domain
domain TypeSpec
tspec) (TypeSpec -> Term
domain_constraint TypeSpec
tspec)
                          [[Derivation] -> ModClause
DerivationCl (TypeSpec -> [Derivation]
derivation TypeSpec
tspec)
                          ,[Term] -> ModClause
ConditionedByCl (TypeSpec -> [Term]
conditions TypeSpec
tspec) 
                          ,[Effect] -> ModClause
PostCondCl (EventSpec -> [Effect]
event_effects EventSpec
espec)]

ppEvent' :: String -> Domain -> Term -> [ModClause] -> String
ppEvent' String
domainID Domain
domain Term
domain_constr [ModClause]
clauses =
  String
"Event " forall a. [a] -> [a] -> [a]
++ String
domainID forall a. [a] -> [a] -> [a]
++ String
show_objects
    forall a. [a] -> [a] -> [a]
++ Term -> String
ppConstraint Term
domain_constr
    forall a. [a] -> [a] -> [a]
++ [ModClause] -> String
ppClauses [ModClause]
clauses
  where Products [Var]
objects = Domain
domain
        show_objects :: String
show_objects | forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Var]
objects = String
""
                     | Bool
otherwise    = String
" Related to " forall a. [a] -> [a] -> [a]
++ forall a. [a] -> [[a]] -> [a]
intercalate String
", " (forall a b. (a -> b) -> [a] -> [b]
map (\(Var String
x String
dec) -> String
xforall a. [a] -> [a] -> [a]
++String
dec) [Var]
objects)

ppEffect :: Effect -> String
ppEffect (CAll [Var]
vs Term
t) = [Var] -> String -> String
foreach [Var]
vs (Term -> String
ppTerm Term
t)
ppEffect (TAll [Var]
vs Term
t) = [Var] -> String -> String
foreach [Var]
vs (Term -> String
ppTerm Term
t)
ppEffect (OAll [Var]
vs Term
t) = [Var] -> String -> String
foreach [Var]
vs (Term -> String
ppTerm Term
t)

ppFact :: DomId -> TypeSpec -> FactSpec -> String
ppFact :: String -> TypeSpec -> FactSpec -> String
ppFact String
d TypeSpec
tspec FactSpec
fspec = 
  String
"Fact " forall a. [a] -> [a] -> [a]
++ String
d forall a. [a] -> [a] -> [a]
++ String
" Identified by " forall a. [a] -> [a] -> [a]
++ Domain -> Term -> String
ppDom (TypeSpec -> Domain
domain TypeSpec
tspec) (TypeSpec -> Term
domain_constraint TypeSpec
tspec) 
    forall a. [a] -> [a] -> [a]
++ [Term] -> String
ppPreConditions (TypeSpec -> [Term]
conditions TypeSpec
tspec)
    forall a. [a] -> [a] -> [a]
++ [Derivation] -> String
ppDerivRules (TypeSpec -> [Derivation]
derivation TypeSpec
tspec)

ppDerivRules :: [Derivation] -> String
ppDerivRules [Derivation]
deriv = case [Derivation]
deriv of 
                        [] -> String
"" 
                        [Derivation]
holds | forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Derivation -> Bool
isHolds [Derivation]
holds -> String
"\n  Holds when " forall a. [a] -> [a] -> [a]
++ forall a. [a] -> [[a]] -> [a]
intercalate String
", " (forall a b. (a -> b) -> [a] -> [b]
map Term -> String
ppTerm [Term]
ts)
                          where isHolds :: Derivation -> Bool
isHolds (HoldsWhen Term
_) = Bool
True
                                isHolds Derivation
_ = Bool
False
                                ts :: [Term]
ts = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Derivation -> [Term]
op [Derivation]
holds
                                  where op :: Derivation -> [Term]
op (HoldsWhen Term
t) = [Term
t]
                                        op Derivation
_             = []
                        [Derivation]
ts -> String
"\n  Derived from " forall a. [a] -> [a] -> [a]
++ forall a. [a] -> [[a]] -> [a]
intercalate String
", " (forall a b. (a -> b) -> [a] -> [b]
map Derivation -> String
ppDeriv [Derivation]
ts)

ppDuty :: String -> TypeSpec -> DutySpec -> String
ppDuty String
d TypeSpec
tspec DutySpec
dspec = String -> Domain -> Term -> [ModClause] -> String
ppDuty' String
d (TypeSpec -> Domain
domain TypeSpec
tspec) (TypeSpec -> Term
domain_constraint TypeSpec
tspec)
                              [[Derivation] -> ModClause
DerivationCl (TypeSpec -> [Derivation]
derivation TypeSpec
tspec)
                              ,[Term] -> ModClause
ConditionedByCl (TypeSpec -> [Term]
conditions TypeSpec
tspec)
                              ,[Term] -> ModClause
ViolationCl (DutySpec -> [Term]
violated_when DutySpec
dspec)]

ppDuty' :: String -> Domain -> Term -> [ModClause] -> String
ppDuty' String
domainID Domain
domain Term
domain_constr [ModClause]
clauses = 
  String
"Duty " forall a. [a] -> [a] -> [a]
++ String
domainID forall a. [a] -> [a] -> [a]
++ String
" Holder " forall a. [a] -> [a] -> [a]
++ Var -> String
ppVar Var
holder forall a. [a] -> [a] -> [a]
++ String
" Claimant " forall a. [a] -> [a] -> [a]
++ Var -> String
ppVar Var
claimant forall a. [a] -> [a] -> [a]
++ String
show_objects
          forall a. [a] -> [a] -> [a]
++ Term -> String
ppConstraint Term
domain_constr
          forall a. [a] -> [a] -> [a]
++ [ModClause] -> String
ppClauses [ModClause]
clauses
   where Products (Var
holder:Var
claimant:[Var]
objects) = Domain
domain
         show_objects :: String
show_objects | forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Var]
objects = String
""
                      | Bool
otherwise    = String
" Related to " forall a. [a] -> [a] -> [a]
++ forall a. [a] -> [[a]] -> [a]
intercalate String
", " (forall a b. (a -> b) -> [a] -> [b]
map (\(Var String
x String
dec) -> String
xforall a. [a] -> [a] -> [a]
++String
dec) [Var]
objects)

ppViolationConds :: [Term] -> String
ppViolationConds :: [Term] -> String
ppViolationConds [Term]
ts | forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Term]
ts = String
""
                    | Bool
otherwise = String
"\n  Violated when " forall a. [a] -> [a] -> [a]
++ forall a. [a] -> [[a]] -> [a]
intercalate String
", " (forall a b. (a -> b) -> [a] -> [b]
map Term -> String
ppTerm [Term]
ts)

ppEnforcingActs :: [DomId] -> String
ppEnforcingActs :: [String] -> String
ppEnforcingActs [String]
ds | forall (t :: * -> *) a. Foldable t => t a -> Bool
null [String]
ds = String
""
                   | Bool
otherwise = String
"\n  Enforced by " forall a. [a] -> [a] -> [a]
++ forall a. [a] -> [[a]] -> [a]
intercalate String
", " [String]
ds

ppDeriv :: Derivation -> String
ppDeriv :: Derivation -> String
ppDeriv (HoldsWhen Term
a) = String
"<HOLDS WHEN>"
ppDeriv (Dv [Var]
xs Term
t)     = [Var] -> String -> String
foreach [Var]
xs (Term -> String
ppTerm Term
t) 

ppDom :: Domain -> Term -> String
ppDom :: Domain -> Term -> String
ppDom Domain
dom Term
c = String
types forall a. [a] -> [a] -> [a]
++ Term -> String
ppConstraint Term
c
  where types :: String
types = case Domain
dom of
                  Strings [String]
ss  -> forall a. [a] -> [[a]] -> [a]
intercalate String
", " [String]
ss
                  Ints [Int]
is     -> forall a. [a] -> [[a]] -> [a]
intercalate String
", " (forall a b. (a -> b) -> [a] -> [b]
map forall a. Show a => a -> String
show [Int]
is)
                  Domain
AnyString   -> String
"String"
                  Domain
AnyInt      -> String
"Int"
                  -- Products rs -> intercalate " * " (map show rs)
                  Products [Var]
rs -> forall a. [a] -> [[a]] -> [a]
intercalate String
" * " (forall a b. (a -> b) -> [a] -> [b]
map Var -> String
ppVar [Var]
rs)
                  Domain
Time        -> String
"<TIME>"

ppConstraint :: Term -> String
ppConstraint Term
c = case Term
c of  BoolLit Bool
True -> String
""
                            (Exists [] (BoolLit Bool
True)) -> String
""
                            Term
_         -> String
" Where " forall a. [a] -> [a] -> [a]
++ Term -> String
ppTerm Term
c

ppTerm :: Term -> String
ppTerm :: Term -> String
ppTerm Term
t = case Term
t of
  Not Term
t -> String -> [String] -> String
app String
"Not" [Term -> String
ppTerm Term
t]
  And Term
t1 Term
t2 -> String -> String -> String -> String
app_infix String
"&&" (Term -> String
ppTerm Term
t1) (Term -> String
ppTerm Term
t2)
  Or Term
t1 Term
t2 -> String -> String -> String -> String
app_infix String
"||" (Term -> String
ppTerm Term
t1) (Term -> String
ppTerm Term
t2)
  BoolLit Bool
b -> forall a. Show a => a -> String
show Bool
b
  Leq Term
t1 Term
t2 -> String -> String -> String -> String
app_infix String
"<=" (Term -> String
ppTerm Term
t1) (Term -> String
ppTerm Term
t2)
  Geq Term
t1 Term
t2 -> String -> String -> String -> String
app_infix String
">=" (Term -> String
ppTerm Term
t1) (Term -> String
ppTerm Term
t2)
  Ge Term
t1 Term
t2 -> String -> String -> String -> String
app_infix String
">" (Term -> String
ppTerm Term
t1) (Term -> String
ppTerm Term
t2)
  Le Term
t1 Term
t2 -> String -> String -> String -> String
app_infix String
"<" (Term -> String
ppTerm Term
t1) (Term -> String
ppTerm Term
t2)
  Sub Term
t1 Term
t2 -> String -> String -> String -> String
app_infix String
"-" (Term -> String
ppTerm Term
t1) (Term -> String
ppTerm Term
t2)
  Add Term
t1 Term
t2 -> String -> String -> String -> String
app_infix String
"+" (Term -> String
ppTerm Term
t1) (Term -> String
ppTerm Term
t2)
  Mult Term
t1 Term
t2 -> String -> String -> String -> String
app_infix String
"*" (Term -> String
ppTerm Term
t1) (Term -> String
ppTerm Term
t2)
  Mod Term
t1 Term
t2 -> String -> String -> String -> String
app_infix String
"%" (Term -> String
ppTerm Term
t1) (Term -> String
ppTerm Term
t2)
  Div Term
t1 Term
t2 -> String -> String -> String -> String
app_infix String
"/" (Term -> String
ppTerm Term
t1) (Term -> String
ppTerm Term
t2)
  IntLit Int
i -> forall a. Show a => a -> String
show Int
i
  StringLit String
s -> forall a. Show a => a -> String
show String
s
  Eq Term
t1 Term
t2 -> String -> String -> String -> String
app_infix String
"==" (Term -> String
ppTerm Term
t1) (Term -> String
ppTerm Term
t2)
  Neq Term
t1 Term
t2 -> String -> String -> String -> String
app_infix String
"!=" (Term -> String
ppTerm Term
t1) (Term -> String
ppTerm Term
t2)
  Exists [Var]
vs Term
t -> [Var] -> String -> String
exists [Var]
vs (Term -> String
ppTerm Term
t)
  Forall [Var]
vs Term
t -> [Var] -> String -> String
forall [Var]
vs (Term -> String
ppTerm Term
t)
  Count [Var]
vs Term
t  -> String
"Count" forall a. [a] -> [a] -> [a]
++ [Var] -> String -> String
foreach [Var]
vs (Term -> String
ppTerm Term
t)
  Sum [Var]
vs Term
t    -> String
"Sum" forall a. [a] -> [a] -> [a]
++ [Var] -> String -> String
foreach [Var]
vs (Term -> String
ppTerm Term
t)
  Max [Var]
vs Term
t    -> String
"Max" forall a. [a] -> [a] -> [a]
++ [Var] -> String -> String
foreach [Var]
vs (Term -> String
ppTerm Term
t)
  Min [Var]
vs Term
t    -> String
"Min" forall a. [a] -> [a] -> [a]
++ [Var] -> String -> String
foreach [Var]
vs (Term -> String
ppTerm Term
t)
  When Term
t1 Term
t2  -> String -> String -> String -> String
app_infix String
"When" (Term -> String
ppTerm Term
t1) (Term -> String
ppTerm Term
t2)
  Present Term
t   -> String -> [String] -> String
app String
"Holds" [Term -> String
ppTerm Term
t]
  Violated Term
t  -> String -> [String] -> String
app String
"Violated" [Term -> String
ppTerm Term
t] 
  Enabled Term
t   -> String -> [String] -> String
app String
"Enabled" [Term -> String
ppTerm Term
t] 
  Project Term
t Var
v -> String -> [String] -> String
app String
"" [Term -> String
ppTerm Term
t] forall a. [a] -> [a] -> [a]
++ String
"." forall a. [a] -> [a] -> [a]
++ Var -> String
ppVar Var
v
  Tag Term
t String
d     -> String -> [String] -> String
app String
d [Term -> String
ppTerm Term
t]
  Untag Term
t     -> String -> [String] -> String
app String
"Untag" [Term -> String
ppTerm Term
t]
  Ref Var
v       -> Var -> String
ppVar Var
v
  App String
d Arguments
args  -> case Arguments
args of
    Left [Term]
ts   -> String -> [String] -> String
app String
d forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map Term -> String
ppTerm [Term]
ts
    Right [Modifier]
ms  -> String -> [String] -> String
app String
d forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map Modifier -> String
ppMod [Modifier]
ms
  Term
CurrentTime -> String
"<TIME>"

ppVar :: Var -> String
ppVar :: Var -> String
ppVar (Var String
x String
dec) = String
x forall a. [a] -> [a] -> [a]
++ String
dec

ppMod :: Modifier -> String
ppMod :: Modifier -> String
ppMod (Rename Var
v Term
t) = Var -> String
ppVar Var
v forall a. [a] -> [a] -> [a]
++ String
"=" forall a. [a] -> [a] -> [a]
++ Term -> String
ppTerm Term
t 

ppPlaceholder :: DomId -> DomId -> String
ppPlaceholder :: String -> String -> String
ppPlaceholder String
var String
for = String
"Placeholder " forall a. [a] -> [a] -> [a]
++ String
var forall a. [a] -> [a] -> [a]
++ String
" For " forall a. [a] -> [a] -> [a]
++ String
for

seq :: [String] -> String
seq :: [String] -> String
seq = forall a. [a] -> [[a]] -> [a]
intercalate String
".\n" 

foreach :: [Var] -> String -> String
foreach = String -> [Var] -> String -> String
binder String
"Foreach"
exists :: [Var] -> String -> String
exists = String -> [Var] -> String -> String
binder String
"Exists"
forall :: [Var] -> String -> String
forall = String -> [Var] -> String -> String
binder String
"Forall"
count :: [Var] -> String -> String
count = String -> [Var] -> String -> String
binder String
"Count"

binder :: String -> [Var] -> String -> String
binder :: String -> [Var] -> String -> String
binder String
op [] String
str = String
str
binder String
op [Var]
vs String
str = String
"(" forall a. [a] -> [a] -> [a]
++ String
op forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ forall a. [a] -> [[a]] -> [a]
intercalate String
"," (forall a b. (a -> b) -> [a] -> [b]
map Var -> String
ppVar [Var]
vs) forall a. [a] -> [a] -> [a]
++ String
": " forall a. [a] -> [a] -> [a]
++ String
str forall a. [a] -> [a] -> [a]
++ String
")"

app :: String -> [String] -> String
app :: String -> [String] -> String
app String
cons [String]
args = String
cons forall a. [a] -> [a] -> [a]
++ String
"(" forall a. [a] -> [a] -> [a]
++ forall a. [a] -> [[a]] -> [a]
intercalate String
"," [String]
args forall a. [a] -> [a] -> [a]
++ String
")"

app_infix :: String -> String -> String -> String
app_infix :: String -> String -> String -> String
app_infix String
op String
x String
y = String
x forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ String
op forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ String
y