Module

Mycroft.SExpr

Package: purescript-mycroft
Repository: afcondon/purescript-mycroft

SMTLib2 surface syntax: atoms and lists, nothing else. Atoms are kept raw — a string literal is an atom that includes its quotes, a |quoted symbol| includes its pipes. print is the wire format; feed/finish is a streaming parser for chunked solver stdout.

#SExpr Source

data SExpr

Constructors

Atom String
List (Array SExpr)

Instances

#print Source

print :: SExpr -> String

#Mode Source

data Mode

#ParseState Source

type ParseState = { atom :: List Char, mode :: Mode, stack :: List (List SExpr) }

Streaming parser state. Feed chunks as they arrive from the solver; completed toplevel forms fall out of each feed.

#initialState Source

initialState :: ParseState

#feed Source

feed :: ParseState -> String -> Either String { exprs :: Array SExpr, state :: ParseState }

#finish Source

finish :: ParseState -> Either String (Array SExpr)

End of input: flush a trailing toplevel atom, reject anything left half-open.

#parseAll Source

parseAll :: String -> Either String (Array SExpr)

Modules: Mycroft.SExpr; Mycroft.SmtLib; Mycroft.Solver