| Copyright | (c) Christian Maeder Uni Bremen 2005 |
|---|---|
| License | GPLv2 or higher, see LICENSE.txt |
| Maintainer | Christian.Maeder@dfki.de |
| Stability | provisional |
| Portability | portable |
| Safe Haskell | Safe |
CASL.Inject
Description
Replace Sorted_term(s) with explicit injection functions. Don't do this after simplification since crucial sort information may be missing
Synopsis
- makeInjOrProj :: TermExtension f => (OP_TYPE -> Id) -> OpKind -> Range -> TERM f -> SORT -> TERM f
- injectUnique :: TermExtension f => Range -> TERM f -> SORT -> TERM f
- uniqueInjName :: OP_TYPE -> Id
- injRecord :: TermExtension f => (f -> f) -> Record f (FORMULA f) (TERM f)
- injTerm :: TermExtension f => (f -> f) -> TERM f -> TERM f
- injFormula :: TermExtension f => (f -> f) -> FORMULA f -> FORMULA f
- insertInjOps :: Sign f e -> [OP_SYMB] -> Sign f e
Documentation
makeInjOrProj :: TermExtension f => (OP_TYPE -> Id) -> OpKind -> Range -> TERM f -> SORT -> TERM f Source #
injectUnique :: TermExtension f => Range -> TERM f -> SORT -> TERM f Source #
uniqueInjName :: OP_TYPE -> Id Source #
injFormula :: TermExtension f => (f -> f) -> FORMULA f -> FORMULA f Source #
insertInjOps :: Sign f e -> [OP_SYMB] -> Sign f e Source #
takes a list of OP_SYMB generated by
recover_Sort_gen_ax and inserts these operations into
the signature; unqualified OP_SYMBs yield an error