-
Exported names:
-
Imported modules:
Module ESMT
This module provides some utility functions for the SMT-LIB language defined
in the package smtlib
that are needed for checking Curry programs.
For example, functions for substituting sorts in terms, simplifying terms
and removing polymorphism in SMT-LIB scripts are provided.
Author: Michael Hanus
Version: Juli 2021
Summary of exported operations:
showSort
:: Sort -> String 
Sorts |
isTypeParameter
:: Sort -> Bool
Does the sort represent a type parameter ( TVar i)?
|
sortedConst
:: String -> Sort -> Term
Terms A constant with a sort declaration. |
sAssert
:: Term -> Command
Assert a simplified formula. |
allQIdsOfTerm
:: Term -> [QIdent]
|
allQIdsOfSigs
:: [([String],FunSig,Term)] -> [QIdent]
|
allQIdsOfAsserts
:: [Command] -> [QIdent]
|
allQIdsOfAssert
:: Command -> [QIdent]
|
typeParamsOfSort
:: Sort -> [String]
All type parameters occurring in a sort. |
typeParamsOfTerm
:: Term -> [String]
All type parameters contained in a term. |
typeParamsOfQId
:: QIdent -> [String]
|
typeParamsOfSV
:: SortedVar -> [String]
|
typeParamsOfFunSig
:: FunSig -> [String]
|
emptyTPSubst
:: Map String Sort
The empty substitution |
matchSort
:: Sort -> Sort -> Maybe (Map String Sort)
Compute sort matching, i.e., if matchSort t1 t2 = s, then t2 = s(t1).
|
matchSorts
:: [Sort] -> [Sort] -> Maybe (Map String Sort)
|
substSort
:: Map String Sort -> Sort -> Sort
Applies a sort substitution to a sort. |
substTerm
:: Map String Sort -> Term -> Term
Applies a sort substitution to a term. |
substQId
:: Map String Sort -> QIdent -> QIdent
|
substSV
:: Map String Sort -> SortedVar -> SortedVar
|
substFunSig
:: Map String Sort -> FunSig -> FunSig
|
substDefSig
:: Map String Sort -> ([String],FunSig,Term) -> ([String],FunSig,Term)
|
rnmTerm
:: (String -> String) -> Term -> Term
|
rnmQId
:: (String -> String) -> QIdent -> QIdent
|
rnmFunSig
:: (String -> String) -> FunSig -> FunSig
|
rnmDefSig
:: (String -> String) -> ([String],FunSig,Term) -> ([String],FunSig,Term)
|
simpTerm
:: Term -> Term
|
reduceAsInTerm
:: Term -> Term
|
sortIdsOfSort
:: Sort -> [String]
|
sortsOfTerm
:: Term -> [Sort]
|
sortOfSortedVar
:: SortedVar -> Sort
|
unpoly
:: [Either [([String],FunSig,Term)] Command] -> [Command]
|
funSigTermsToCommands
:: [([String],FunSig,Term)] -> [Command]
|
addAllInstancesOfSigs
:: [QIdent] -> [([String],FunSig,Term)] -> ([QIdent],[([String],FunSig,Term)])
|
addInstancesOfSigs
:: [QIdent] -> [([String],FunSig,Term)] -> ([QIdent],[([String],FunSig,Term)])
|
addInstancesOfSig
:: [QIdent] -> [([String],FunSig,Term)] -> ([String],FunSig,Term) -> ([QIdent],[([String],FunSig,Term)])
|
rnmQIdWithTInst
:: [(String,([String],Sort))] -> QIdent -> QIdent
|
rnmQIdWithTInstTerm
:: [(String,([String],Sort))] -> Term -> Term
|
toTInstName
:: String -> [String] -> Map String Sort -> String -> String
|
addTInstName
:: [String] -> Map String Sort -> String -> String
|
nameOfSig
:: ([String],FunSig,Term) -> String
|
sigNameSort
:: ([String],FunSig,Term) -> (String,([String],Sort))
|
sigTypeAsSort
:: [Sort] -> Sort -> Sort
|
Exported datatypes:
FunSig
Function signatures The signature of a function declaration.
Constructors:
FunSigTerm
A definition of a polymorphic, possibly non-deterministic, operation.
The first component is a list of type paramters
which can be used in the type signature and the term.
The term in the third argument is the axiomatization of the function
definition. Thus, it contains all quantifiers and the equation
(= (f x1...xn) rhs-term)
so that it can also be used to specify,
by exploiting disjunctions, the meaning of non-deterministic operations.
Type synonym: FunSigTerm = ([Ident],FunSig,Term)
TPSubst
A type parameter substitution.
Type synonym: TPSubst = Map Ident Sort
Exported operations:
|
Does the sort represent a type parameter ( |
|
Terms A constant with a sort declaration.
|
|
|
|
|
|
|
|
|
|
All type parameters occurring in a sort. |
|
All type parameters contained in a term. |
|
|
|
|
|
|
|
The empty substitution
|
|
Compute sort matching, i.e., if |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|