A tool to translate FlatCurry operations into SMT assertions.
Author: Michael Hanus
Version: May 2021
funcs2SMT
:: [(String,String)] -> StateT VState IO [([String],FunSig,Term)]
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
:: Maybe Term -> 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. |
preludeType2SMT
:: String -> [Command]
Translates a prelude type into an SMT datatype declaration, if necessary. |
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. |
|
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 type 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 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. |