| definition: |
ppCmd :: Command -> [Doc]
ppCmd cmd = case cmd of
Assert t -> [text "assert", pretty (reduceAsInTerm t)] -- for nicer printing
CheckSat -> [text "check-sat"]
DeclareVar (SV v s) -> [text "declare-const", prettyVar v, pretty s]
DeclareDatatypes sds -> -- use old SMT syntax:
if length sds /= 1
then error "Datatype declaration with more than one type!"
else let (tc, _, DT tvs cs) = head sds
in [ text "declare-datatypes"
, parent (map text tvs)
, parent [parent (text tc : map pretty cs)]
]
--DeclareDatatypes sds -> let (ss, ars, ds) = unzip3 sds in
-- [ text "declare-datatypes"
-- , parent (map (\ (s,a) -> parent [text s, int a])
-- (zip ss ars))
-- , parent (map pretty ds)
-- ]
DeclareFun fn ss s -> [ text "declare-fun"
, text fn
, parent (map pretty ss)
, pretty s
]
DefineFunsRec fts -> let (fs, ts) = unzip fts in
[ text "define-funs-rec"
, parent (map pretty fs)
, parent (map pretty ts)
]
DeclareSort sym n -> [text "declare-sort", text sym, int n]
_ -> error $ "ppCmd: command '" ++ show cmd ++ "' not reachable!"
|
| demand: |
argument 1 |
| deterministic: |
deterministic operation |
| documentation: |
--- Pretty printing of SMT-LIB commands. |
| failfree: |
<FAILING> |
| indeterministic: |
referentially transparent operation |
| infix: |
no fixity defined |
| iotype: |
{({Assert}) |-> {:} || ({CheckSat}) |-> {:} || ({DeclareVar}) |-> {:} || ({DeclareDatatypes}) |-> {:} || ({DeclareFun}) |-> {:} || ({DefineFunsRec}) |-> {:} || ({DeclareSort}) |-> {:} || ({Comment}) |-> _ || ({DefineSigsRec}) |-> _ || ({EmptyLine}) |-> _}
|
| name: |
ppCmd |
| precedence: |
no precedence defined |
| result-values: |
_ |
| signature: |
Command -> [Text.PrettyImpl.Doc] |
| solution-complete: |
operation might suspend on free variables |
| terminating: |
possibly non-terminating |
| totally-defined: |
possibly non-reducible on same data term |