Hets - the Heterogeneous Tool Set

Copyright(c) Christian Maeder, Uni Bremen 2005
LicenseGPLv2 or higher, see LICENSE.txt
MaintainerChristian.Maeder@dfki.de
Stabilityprovisional
Portabilityportable
Safe HaskellSafe-Inferred

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

Documentation

makeInjOrProj :: TermExtension f => (OP_TYPE -> Id) -> OpKind -> Range -> TERM f -> SORT -> TERM f

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

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