CurryInfo: contract-prover-4.0.0 / ESMT.ppCmd

 
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!"

 argument 1

 deterministic operation

 
Pretty printing of SMT-LIB commands.

 <FAILING>

 referentially transparent operation

 no fixity defined

 {({Assert}) |-> {:} || ({CheckSat}) |-> {:} || ({DeclareVar}) |-> {:} || ({DeclareDatatypes}) |-> {:} || ({DeclareFun}) |-> {:} || ({DefineFunsRec}) |-> {:} || ({DeclareSort}) |-> {:} || ({Comment}) |-> _ || ({DefineSigsRec}) |-> _ || ({EmptyLine}) |-> _}

 ppCmd

 no precedence defined

 _

 Command -> [Text.PrettyImpl.Doc]

 operation might suspend on free variables

 possibly non-terminating

 possibly non-reducible on same data term