| Safe Haskell | None |
|---|---|
| Language | Haskell98 |
Idris.PartialEval
- partial_eval :: Context -> [(Name, Maybe Int)] -> [Either Term (Term, Term)] -> [Either Term (Term, Term)]
- getSpecApps :: IState -> [Name] -> Term -> [(Name, [(PEArgType, Term)])]
- specType :: [(PEArgType, Term)] -> Type -> (Type, [(PEArgType, Term)])
- mkPE_TyDecl :: IState -> [(PEArgType, Term)] -> Type -> PTerm
- mkPE_TermDecl :: IState -> Name -> Name -> [(PEArgType, Term)] -> [(PTerm, PTerm)]
- data PEArgType
Documentation
partial_eval :: Context -> [(Name, Maybe Int)] -> [Either Term (Term, Term)] -> [Either Term (Term, Term)] Source
Partially evaluates given terms under the given context.
getSpecApps :: IState -> [Name] -> Term -> [(Name, [(PEArgType, Term)])] Source
Get specialised applications for a given function
specType :: [(PEArgType, Term)] -> Type -> (Type, [(PEArgType, Term)]) Source
Specialises the type of a partially evaluated TT function returning a pair of the specialised type and the types of expected arguments.
mkPE_TyDecl :: IState -> [(PEArgType, Term)] -> Type -> PTerm Source
Creates an Idris type declaration given current state and a specialised TT function application type.
Can be used in combination with the output of specType.
mkPE_TermDecl :: IState -> Name -> Name -> [(PEArgType, Term)] -> [(PTerm, PTerm)] Source
Creates a new clause for a specialised function application