A tool to translate FlatCurry operations into SMT assertions.
Author: Michael Hanus
Version: September 2019
funcs2SMT
:: Options -> IORef VState -> [(String,String)] -> IO (Command,[AFuncDecl TypeExpr],[((String,String),Bool)])
Translates a list of operations specified by their qualified name (together with all operations on which these operation depend on) into an SMT string that axiomatizes their semantics. |
fun2SMT
:: AFuncDecl TypeExpr -> ([String],FunSig,Term)
|
exp2SMT
:: AExpr TypeExpr -> Term
|
patternTest
:: APattern TypeExpr -> Term -> Term
|
constructorTest
:: Bool -> (String,String) -> Term -> TypeExpr -> Term
Translates a constructor name and a term into an SMT formula implementing a test on the term for this constructor. |
selectors
:: (String,String) -> [String]
Computes the SMT selector names for a given constructor. |
polytype2sort
:: TypeExpr -> Sort
Translates a FlatCurry type expression into a corresponding SMT sort. |
polytype2psort
:: TypeExpr -> Sort
Translates a FlatCurry type expression into a parametric SMT sort. |
type2sort
:: [(String,String)] -> Bool -> Bool -> TypeExpr -> Sort
Translates a FlatCurry type expression into a corresponding SMT sort. |
tcons2SMT
:: (String,String) -> String
Translates a FlatCurry type constructor name into SMT. |
tdecl2SMT
:: TypeDecl -> Command
Translates a type declaration into an SMT datatype declaration. |
genSelName
:: (String,String) -> Int -> String
Generates the name of the i-th selector for a given constructor. |
preludeSort2SMT
:: String -> [Command]
Translates a prelude sort (with SMT name) into an SMT datatype declaration, if necessary. |
pairType
:: [Command]
|
maybeType
:: [Command]
|
eitherType
:: [Command]
|
orderingType
:: [Command]
|
unitType
:: [Command]
|
dictType
:: [Command]
|
cons2SMT
:: Bool -> Bool -> (String,String) -> TypeExpr -> QIdent
Translates a qualifed name with given result type into an SMT identifier. |
pat2SMT
:: APattern TypeExpr -> Term
Translates a pattern into an SMT expression. |
lit2SMT
:: Literal -> Term
Translates a literal into an SMT expression. |
transOpName
:: (String,String) -> String
Translates a qualified FlatCurry name into an SMT string. |
encodeSpecialChars
:: String -> String
Encode special characters in strings |
decodeSpecialChars
:: String -> String
Translates urlencoded string into equivalent ASCII string. |
untransOpName
:: String -> Maybe (String,String)
Translates a (translated) SMT string back into qualified FlatCurry name. |
Translates a list of operations specified by their qualified name
(together with all operations on which these operation depend on)
into an SMT string that axiomatizes their semantics.
Non-deterministic operations are axiomatized by the "planned choice"
translation (see module |
|
Translates a constructor name and a term into an SMT formula
implementing a test on the term for this constructor.
If the first argument is true, parametric sorts are used
(i.e., we translate a polymorphic function), otherwise
type variables are translated into the sort |
Computes the SMT selector names for a given constructor. |
Translates a FlatCurry type expression into a corresponding SMT sort.
Polymorphic type variables are translated into the sort |
Translates a FlatCurry type expression into a parametric SMT sort.
Thus, a polymorphic type variable |
Translates a FlatCurry type expression into a corresponding SMT sort.
If the first argument is null, then type variables are
translated into the sort |
Translates a FlatCurry type constructor name into SMT. |
Generates the name of the i-th selector for a given constructor. |
Translates a prelude sort (with SMT name) into an SMT datatype declaration, if necessary. |
|
|
Translates a qualifed name with given result type into an SMT identifier.
If the first argument is true and the result type is not a base type,
the type is attached via |
Translates a literal into an SMT expression. We represent character as ints. |
Translates a qualified FlatCurry name into an SMT string. |
Encode special characters in strings |
Translates urlencoded string into equivalent ASCII string. |
Translates a (translated) SMT string back into qualified FlatCurry name. Returns Nothing if it was not a qualified name. |