hets/CASL/AS_Basic_CASL.der.hs

	AS_Basic_CASL.der.hs revision 330b955a293fdc64e9145a159b2f2faec1f8011e
967e5f3c25249c779575864692935627004d3f9eChristian Maeder{- |
967e5f3c25249c779575864692935627004d3f9eChristian MaederModule      :  $Header$
81d182b21020b815887e9057959228546cf61b6bChristian MaederCopyright   :  (c) Klaus L�ttich, Christian Maeder, Uni Bremen 2002-2004
f11f713bebd8e1e623a0a4361065df256033de47Christian MaederLicence     :  similar to LGPL, see HetCATS/LICENCE.txt or LIZENZ.txt
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian Maeder
967e5f3c25249c779575864692935627004d3f9eChristian MaederMaintainer  :  hets@tzi.de
3f69b6948966979163bdfe8331c38833d5d90ecdChristian MaederStability   :  provisional
967e5f3c25249c779575864692935627004d3f9eChristian MaederPortability :  portable
89054b2b95a3f92e78324dc852f3d34704e2ca49Christian Maeder
f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maeder   This is the Abstract Syntax tree of CASL Basic_specs, Symb_items and
717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maeder   Symb_map_items.
717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maeder   Follows Sect. II:2.2 of the CASL Reference Manual.
967e5f3c25249c779575864692935627004d3f9eChristian Maeder-}
967e5f3c25249c779575864692935627004d3f9eChristian Maeder
967e5f3c25249c779575864692935627004d3f9eChristian Maedermodule CASL.AS_Basic_CASL where
967e5f3c25249c779575864692935627004d3f9eChristian Maeder
967e5f3c25249c779575864692935627004d3f9eChristian Maederimport Common.Id
fd896e2068ad7e50aed66ac18c3720ea7ff2619fChristian Maederimport Common.AS_Annotation
650bafe7709533bc5f82bb9daf8fa06f431cd963Christian Maederimport Data.List (nub)
9cb4aa4ea6685489a38f9b609f5dbe5d37f25bc7Christian Maeder
7221c71b38c871ce66eee4537cb681d468308dfbChristian Maeder-- DrIFT command
ac19f8695aa1b2d2d1cd1319da2530edd8f46a96Christian Maeder{-! global: UpPos !-}
8b9fda012e5ee53b7b2320c0638896a0ff6e99f3Christian Maeder
e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian Maederdata BASIC_SPEC b s f = Basic_spec [Annoted (BASIC_ITEMS b s f)]
4ef2a978e66e2246ff0b7f00c77deb7aabb28b8eChristian Maeder          deriving (Show,Eq)
fd896e2068ad7e50aed66ac18c3720ea7ff2619fChristian Maeder
967e5f3c25249c779575864692935627004d3f9eChristian Maederdata BASIC_ITEMS b s f = Sig_items (SIG_ITEMS b s f)
ad270004874ce1d0697fb30d7309f180553bb315Christian Maeder                   -- the Annotation following the keyword is dropped
4ef2a978e66e2246ff0b7f00c77deb7aabb28b8eChristian Maeder           -- but preceding the keyword is now an Annotation allowed
fd896e2068ad7e50aed66ac18c3720ea7ff2619fChristian Maeder         | Free_datatype [Annoted DATATYPE_DECL] [Pos]
717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maeder           -- pos: free, type, semi colons
588c0c022a0f4e129a89c3bc569daf6a835e182dChristian Maeder         | Sort_gen [Annoted (SIG_ITEMS b s f)] [Pos]
717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maeder           -- pos: generated, opt. braces
967e5f3c25249c779575864692935627004d3f9eChristian Maeder         | Var_items [VAR_DECL] [Pos]
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder           -- pos: var, semi colons
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder         | Local_var_axioms [VAR_DECL] [Annoted (FORMULA f)] [Pos]
7a879b08ae0ca30006f9be887a73212b07f10204Christian Maeder           -- pos: forall, semi colons, dots
07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maeder         | Axiom_items [Annoted (FORMULA f)] [Pos]
588c0c022a0f4e129a89c3bc569daf6a835e182dChristian Maeder           -- pos: dots
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder                 | Ext_BASIC_ITEMS b
7a879b08ae0ca30006f9be887a73212b07f10204Christian Maeder           deriving (Show,Eq)
e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian Maeder
588c0c022a0f4e129a89c3bc569daf6a835e182dChristian Maederdata SIG_ITEMS b s f = Sort_items [Annoted (SORT_ITEM f)] [Pos]
e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian Maeder             -- pos: sort, semi colons
588c0c022a0f4e129a89c3bc569daf6a835e182dChristian Maeder           | Op_items [Annoted (OP_ITEM f)] [Pos]
588c0c022a0f4e129a89c3bc569daf6a835e182dChristian Maeder         -- pos: op, semi colons
6e39bfd041946fce4982ac89834be73fd1bfb39aChristian Maeder           | Pred_items [Annoted (PRED_ITEM f)] [Pos]
e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian Maeder         -- pos: pred, semi colons
62ecb1e7f8fd9573eea8369657de12c7bf9f4f25Christian Maeder           | Datatype_items [Annoted DATATYPE_DECL] [Pos]
588c0c022a0f4e129a89c3bc569daf6a835e182dChristian Maeder         -- type, semi colons
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder               | Ext_SIG_ITEMS s
588c0c022a0f4e129a89c3bc569daf6a835e182dChristian Maeder         deriving (Show,Eq)
588c0c022a0f4e129a89c3bc569daf6a835e182dChristian Maeder
d5c415f6373274fed04d83b9322891f3b82e9c26Christian Maederdata SORT_ITEM f = Sort_decl [SORT] [Pos]
588c0c022a0f4e129a89c3bc569daf6a835e182dChristian Maeder             -- pos: commas
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder           | Subsort_decl [SORT] SORT [Pos]
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder         -- pos: commas, <
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder           | Subsort_defn SORT VAR SORT (Annoted (FORMULA f)) [Pos]
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder         -- pos: "=", "{", ":", ".", "}"
e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder         -- the left anno list stored in Annoted Formula is
588c0c022a0f4e129a89c3bc569daf6a835e182dChristian Maeder         -- parsed after the equal sign
717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maeder           | Iso_decl [SORT] [Pos]
717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maeder             -- pos: "="s
d48085f765fca838c1d972d2123601997174583dChristian Maeder         deriving (Show,Eq)
d48085f765fca838c1d972d2123601997174583dChristian Maeder
717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maederdata OP_ITEM f = Op_decl [OP_NAME] OP_TYPE [OP_ATTR f] [Pos]
d48085f765fca838c1d972d2123601997174583dChristian Maeder           -- pos: commas, colon, OP_ATTR sep. by commas
d48085f765fca838c1d972d2123601997174583dChristian Maeder         | Op_defn OP_NAME OP_HEAD (Annoted (TERM f)) [Pos]
588c0c022a0f4e129a89c3bc569daf6a835e182dChristian Maeder           -- pos: "="
d48085f765fca838c1d972d2123601997174583dChristian Maeder           deriving (Show,Eq)
717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maeder
717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maederdata OP_TYPE = Total_op_type [SORT] SORT [Pos]
e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder           -- pos: "*"s, "->" ; if null [SORT] then [Pos] = []
588c0c022a0f4e129a89c3bc569daf6a835e182dChristian Maeder         | Partial_op_type [SORT] SORT [Pos]
588c0c022a0f4e129a89c3bc569daf6a835e182dChristian Maeder           -- pos: "*"s, "->?"; if null [SORT] then pos: "?"
e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian Maeder           deriving (Show,Eq,Ord)
e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder
588c0c022a0f4e129a89c3bc569daf6a835e182dChristian Maederargs_OP_TYPE :: OP_TYPE -> [SORT]
588c0c022a0f4e129a89c3bc569daf6a835e182dChristian Maederargs_OP_TYPE (Total_op_type args _ _) = args
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maederargs_OP_TYPE (Partial_op_type args _ _) = args
588c0c022a0f4e129a89c3bc569daf6a835e182dChristian Maeder
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maederres_OP_TYPE :: OP_TYPE -> SORT
e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maederres_OP_TYPE (Total_op_type _ res _) = res
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maederres_OP_TYPE (Partial_op_type _ res _) = res
588c0c022a0f4e129a89c3bc569daf6a835e182dChristian Maeder
c66a930944d9e4d64a8f0f38c748fdad0831ff87Christian Maederdata OP_HEAD = Total_op_head [ARG_DECL] SORT [Pos]
f11f713bebd8e1e623a0a4361065df256033de47Christian Maeder           -- pos: "(", semicolons, ")", colon
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder         | Partial_op_head [ARG_DECL] SORT [Pos]
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder           deriving (Show,Eq)
a578ec30cded5e396a7ce9a3b469e8cd3a88246aChristian Maeder
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maederdata ARG_DECL = Arg_decl [VAR] SORT [Pos]
967e5f3c25249c779575864692935627004d3f9eChristian Maeder            -- pos: commas, colon
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder        deriving (Show,Eq)
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder
e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian Maederdata OP_ATTR f = Assoc_op_attr | Comm_op_attr | Idem_op_attr
588c0c022a0f4e129a89c3bc569daf6a835e182dChristian Maeder         | Unit_op_attr (TERM f)
588c0c022a0f4e129a89c3bc569daf6a835e182dChristian Maeder           deriving (Show,Eq)
588c0c022a0f4e129a89c3bc569daf6a835e182dChristian Maeder
588c0c022a0f4e129a89c3bc569daf6a835e182dChristian Maederdata PRED_ITEM f = Pred_decl [PRED_NAME] PRED_TYPE [Pos]
e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian Maeder                 -- pos: commas, colon
47355d1ba4e212c5fd34c089f71a319cde53c4c8Christian Maeder           | Pred_defn PRED_NAME PRED_HEAD (Annoted (FORMULA f)) [Pos]
47355d1ba4e212c5fd34c089f71a319cde53c4c8Christian Maeder         -- pos: "<=>"
47355d1ba4e212c5fd34c089f71a319cde53c4c8Christian Maeder         deriving (Show,Eq)
81d182b21020b815887e9057959228546cf61b6bChristian Maeder
81d182b21020b815887e9057959228546cf61b6bChristian Maederdata PRED_TYPE = Pred_type [SORT] [Pos]
81d182b21020b815887e9057959228546cf61b6bChristian Maeder             -- pos: if null [SORT] then "(",")" else "*"s
47355d1ba4e212c5fd34c089f71a319cde53c4c8Christian Maeder         deriving (Show,Eq,Ord)
47355d1ba4e212c5fd34c089f71a319cde53c4c8Christian Maeder
47355d1ba4e212c5fd34c089f71a319cde53c4c8Christian Maederdata PRED_HEAD = Pred_head [ARG_DECL] [Pos]
a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian Maeder             -- pos: "(",semi colons , ")"
588c0c022a0f4e129a89c3bc569daf6a835e182dChristian Maeder         deriving (Show,Eq)
99f1a09ee1847410faf46527f5465bd2070800c2Christian Maeder
588c0c022a0f4e129a89c3bc569daf6a835e182dChristian Maederdata DATATYPE_DECL = Datatype_decl SORT [Annoted ALTERNATIVE] [Pos]
81d182b21020b815887e9057959228546cf61b6bChristian Maeder             -- pos: "::=", "|"s
81d182b21020b815887e9057959228546cf61b6bChristian Maeder             deriving (Show,Eq)
47355d1ba4e212c5fd34c089f71a319cde53c4c8Christian Maeder
47355d1ba4e212c5fd34c089f71a319cde53c4c8Christian Maederdata ALTERNATIVE = Total_construct OP_NAME [COMPONENTS] [Pos]
650bafe7709533bc5f82bb9daf8fa06f431cd963Christian Maeder           -- pos: "(", semi colons, ")"
588c0c022a0f4e129a89c3bc569daf6a835e182dChristian Maeder         | Partial_construct OP_NAME [COMPONENTS] [Pos]
588c0c022a0f4e129a89c3bc569daf6a835e182dChristian Maeder           -- pos: "(", semi colons, ")", "?"
588c0c022a0f4e129a89c3bc569daf6a835e182dChristian Maeder         | Subsorts [SORT] [Pos]
588c0c022a0f4e129a89c3bc569daf6a835e182dChristian Maeder           -- pos: sort, commas
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder           deriving (Show,Eq)
a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian Maeder
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maederdata COMPONENTS = Total_select [OP_NAME] SORT [Pos]
bfa9e03532243ceb487f0384d0f6a447f1ce7670Till Mossakowski                  -- pos: commas, colon
7221c71b38c871ce66eee4537cb681d468308dfbChristian Maeder        | Partial_select [OP_NAME] SORT [Pos]
7221c71b38c871ce66eee4537cb681d468308dfbChristian Maeder          -- pos: commas, ":?"
7221c71b38c871ce66eee4537cb681d468308dfbChristian Maeder        | Sort SORT
588c0c022a0f4e129a89c3bc569daf6a835e182dChristian Maeder          deriving (Show,Eq)
842eedc62639561781b6c33533d1949693ef6cc5Christian Maeder
42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowskidata VAR_DECL = Var_decl [VAR] SORT [Pos]
842eedc62639561781b6c33533d1949693ef6cc5Christian Maeder            -- pos: commas, colon
842eedc62639561781b6c33533d1949693ef6cc5Christian Maeder        deriving (Show,Eq,Ord)
588c0c022a0f4e129a89c3bc569daf6a835e182dChristian Maeder
588c0c022a0f4e129a89c3bc569daf6a835e182dChristian Maeder{- Position definition for FORMULA:
588c0c022a0f4e129a89c3bc569daf6a835e182dChristian Maeder   Information on parens are also encoded in [Pos].  If there
842eedc62639561781b6c33533d1949693ef6cc5Christian Maeder   are more Pos than necessary there is a pair of Pos enclosing the
bfa9e03532243ceb487f0384d0f6a447f1ce7670Till Mossakowski   other Pos informations which encode the brackets of every kind
967e5f3c25249c779575864692935627004d3f9eChristian Maeder-}
967e5f3c25249c779575864692935627004d3f9eChristian Maeder
967e5f3c25249c779575864692935627004d3f9eChristian Maederdata FORMULA f = Quantification QUANTIFIER [VAR_DECL] (FORMULA f) [Pos]
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder           -- pos: QUANTIFIER, semi colons, dot
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder         | Conjunction [FORMULA f] [Pos]
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder           -- pos: "/\"s
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder         | Disjunction [FORMULA f] [Pos]
588c0c022a0f4e129a89c3bc569daf6a835e182dChristian Maeder           -- pos: "\/"s
588c0c022a0f4e129a89c3bc569daf6a835e182dChristian Maeder         | Implication (FORMULA f) (FORMULA f) Bool [Pos]
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder           -- pos: "=>" or "if" (True -> "=>")
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder         | Equivalence (FORMULA f) (FORMULA f) [Pos]
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder           -- pos: "<=>"
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder         | Negation (FORMULA f) [Pos]
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder           -- pos: not
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder         | True_atom [Pos]
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder           -- pos: true
967e5f3c25249c779575864692935627004d3f9eChristian Maeder         | False_atom [Pos]
967e5f3c25249c779575864692935627004d3f9eChristian Maeder               -- pos: false
588c0c022a0f4e129a89c3bc569daf6a835e182dChristian Maeder         | Predication PRED_SYMB [TERM f] [Pos]
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian Maeder               -- pos: opt. "(",commas,")"
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian Maeder         | Definedness (TERM f) [Pos]
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian Maeder           -- pos: def
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian Maeder         | Existl_equation (TERM f) (TERM f) [Pos]
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian Maeder               -- pos: =e=
4ef2a978e66e2246ff0b7f00c77deb7aabb28b8eChristian Maeder         | Strong_equation (TERM f) (TERM f) [Pos]
4ef2a978e66e2246ff0b7f00c77deb7aabb28b8eChristian Maeder           -- pos: =
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian Maeder         | Membership (TERM f) SORT [Pos]
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian Maeder               -- pos: in
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian Maeder         | Mixfix_formula (TERM f)  -- Mixfix_ Term/Token/(..)/[..]/{..}
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian Maeder         -- a formula left original for mixfix analysis
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian Maeder         | Unparsed_formula String [Pos]
588c0c022a0f4e129a89c3bc569daf6a835e182dChristian Maeder           -- pos: first Char in String
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian Maeder         | Sort_gen_ax [Constraint]
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian Maeder         | ExtFORMULA f
4ef2a978e66e2246ff0b7f00c77deb7aabb28b8eChristian Maeder             -- needed for CASL extensions
4ef2a978e66e2246ff0b7f00c77deb7aabb28b8eChristian Maeder           deriving (Show,Eq,Ord)
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian Maeder
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian Maeder{- In the CASL institution, sort generation constraints have an
ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maederadditional signature morphism component (Sect. III:2.1.3, p.134 of the
2ac1742771a267119f1d839054b5e45d0a468085Christian MaederCASL Reference Manual).  The extra signature morphism component is
2ac1742771a267119f1d839054b5e45d0a468085Christian Maederneeded because the naive translation of sort generation constraints
588c0c022a0f4e129a89c3bc569daf6a835e182dChristian Maederalong signature morphisms may violate the satisfaction condition,
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maedernamely when sorts are identified by the translation, with the effect
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maederthat new terms can be formed. We avoid this extra component here and
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maederinstead use natural numbers to decorate sorts, in this way retaining
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maedertheir identity w.r.t. the original signature. The newSort in a
588c0c022a0f4e129a89c3bc569daf6a835e182dChristian MaederConstraint is implicitly decorated with its index in the list of
588c0c022a0f4e129a89c3bc569daf6a835e182dChristian MaederConstraints. The opSymbs component collects all the operation symbols
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian Maederwith newSort (with that index!) as a result sort. The argument sorts
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian Maederof an operation symbol are decorated explicitly via a list [Int] of
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maederintegers. The origSort in a Constraint is the original sort
2ac1742771a267119f1d839054b5e45d0a468085Christian Maedercorresponding to the index.  Note that this representation of sort
2ac1742771a267119f1d839054b5e45d0a468085Christian Maedergeneration constraints is efficiently tailored towards both the use in
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maederthe proof calculus (Chap. IV:2, p. 282 of the CASL Reference Manual)
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maederand the coding into second order logic (p. 429 of Theoret. Comp. Sci. 286).
588c0c022a0f4e129a89c3bc569daf6a835e182dChristian Maeder-}
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder
588c0c022a0f4e129a89c3bc569daf6a835e182dChristian Maederdata Constraint = Constraint { newSort :: SORT,
588c0c022a0f4e129a89c3bc569daf6a835e182dChristian Maeder                               opSymbs :: [(OP_SYMB,[Int])],
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder                               origSort :: SORT }
588c0c022a0f4e129a89c3bc569daf6a835e182dChristian Maeder                  deriving (Show,Eq,Ord)
588c0c022a0f4e129a89c3bc569daf6a835e182dChristian Maeder
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian Maeder-- | from a Sort_gex_ax, recover:
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian Maeder-- | a traditional sort generation constraint plus a sort mapping
588c0c022a0f4e129a89c3bc569daf6a835e182dChristian Maederrecover_Sort_gen_ax :: [Constraint] ->
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian Maeder                        ([SORT],[OP_SYMB],[(SORT,SORT)])
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian Maederrecover_Sort_gen_ax constrs =
967e5f3c25249c779575864692935627004d3f9eChristian Maeder  if length (nub sorts) == length sorts
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder     -- no duplicate sorts, i.e. injective sort map? Then we can ignore indices
4ef2a978e66e2246ff0b7f00c77deb7aabb28b8eChristian Maeder     then (sorts,map fst (concat (map opSymbs constrs)),[])
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder     -- otherwise, we have to introduce new sorts for the indices
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder     -- and afterwards rename them into the sorts they denote
588c0c022a0f4e129a89c3bc569daf6a835e182dChristian Maeder     else (map indSort1 indices,map indOp indOps1,map sortMap indSorts)
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder  where
97ee7048e63953c5617342ce38c30cbcb35cc0beChristian Maeder  sorts = map newSort constrs
97ee7048e63953c5617342ce38c30cbcb35cc0beChristian Maeder  indices = [0..length sorts-1]
07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maeder  indSorts = zip indices sorts
588c0c022a0f4e129a89c3bc569daf6a835e182dChristian Maeder  indSort (i,s) = if i<0 then s else indSort1 i
07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maeder  indSort1 i = origSort $ head (drop i constrs)
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder  sortMap (i,s) = (indSort1 i,s)
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder  indOps = zip indices (map opSymbs constrs)
07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maeder  indOps1 = concat (map (\(i,ops) -> map ((,) i) ops) indOps)
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder  indOp (res,(Qual_op_name on (Total_op_type args1 res1 pos1) pos,args)) =
07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maeder     Qual_op_name on
588c0c022a0f4e129a89c3bc569daf6a835e182dChristian Maeder         (Total_op_type (map indSort (zip args args1))
588c0c022a0f4e129a89c3bc569daf6a835e182dChristian Maeder                        (indSort (res,res1)) pos1) pos
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder  indOp (res,(Qual_op_name on (Partial_op_type args1 res1 pos1) pos,args)) =
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder     Qual_op_name on
588c0c022a0f4e129a89c3bc569daf6a835e182dChristian Maeder         (Partial_op_type (map indSort (zip args args1))
588c0c022a0f4e129a89c3bc569daf6a835e182dChristian Maeder                          (indSort (res,res1)) pos1) pos
07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maeder  indOp _ = error
      "CASL/AS_Basic_CASL: Internal error: Unqualified OP_SYMB in Sort_gen_ax"

data QUANTIFIER = Universal | Existential | Unique_existential
          deriving (Show,Eq,Ord)

data PRED_SYMB = Pred_name PRED_NAME
           | Qual_pred_name PRED_NAME PRED_TYPE [Pos]
         -- pos: "(", pred, colon, ")"
         deriving (Show,Eq,Ord)

data TERM f = Simple_id SIMPLE_ID    -- "Var" might be a better constructor
      | Qual_var VAR SORT [Pos]
        -- pos: "(", var, colon, ")"
      | Application OP_SYMB [TERM f] [Pos]
        -- pos: parens around TERM f if any and seperating commas
      | Sorted_term (TERM f) SORT [Pos]
        -- pos: colon
      | Cast (TERM f) SORT [Pos]
        -- pos: "as"
      | Conditional (TERM f) (FORMULA f) (TERM f) [Pos]
        -- pos: "when", "else"
      | Unparsed_term String [Pos]        -- SML-CATS

      -- A new intermediate state
          | Mixfix_qual_pred PRED_SYMB -- as part of a mixfix formula
          | Mixfix_term [TERM f]  -- not starting with Mixfix_sorted_term/cast
      | Mixfix_token Token   -- NO-BRACKET-TOKEN, LITERAL, PLACE
      | Mixfix_sorted_term SORT [Pos]
        -- pos: colon
      | Mixfix_cast SORT [Pos]
        -- pos: "as"
          | Mixfix_parenthesized [TERM f] [Pos]  -- non-emtpy term list
        -- pos: "(", commas, ")"
          | Mixfix_bracketed [TERM f] [Pos]
        -- pos: "[", commas, "]"
          | Mixfix_braced [TERM f] [Pos]         -- also for list-notation
        -- pos: "{", "}"
        deriving (Show,Eq,Ord)

data OP_SYMB = Op_name OP_NAME
         | Qual_op_name OP_NAME OP_TYPE [Pos]
         -- pos: "(", op, colon, ")"
           deriving (Show,Eq,Ord)

type OP_NAME = Id

type PRED_NAME = Id

type SORT = Id

type VAR = SIMPLE_ID

-----
data SYMB_ITEMS = Symb_items SYMB_KIND [SYMB] [Pos]
          -- pos: SYMB_KIND, commas
          deriving (Show,Eq)

data SYMB_ITEMS_LIST = Symb_items_list [SYMB_ITEMS] [Pos]
          -- pos: commas
          deriving (Show,Eq)

data SYMB_MAP_ITEMS = Symb_map_items SYMB_KIND [SYMB_OR_MAP] [Pos]
              -- pos: SYMB_KIND, commas
              deriving (Show,Eq)

data SYMB_MAP_ITEMS_LIST = Symb_map_items_list [SYMB_MAP_ITEMS] [Pos]
          -- pos: commas
          deriving (Show,Eq)

data SYMB_KIND = Implicit | Sorts_kind
           | Ops_kind | Preds_kind
         deriving (Show,Eq)

data SYMB = Symb_id Id
      | Qual_id Id TYPE [Pos]
        -- pos: colon
        deriving (Show,Eq)

data TYPE = O_type OP_TYPE
      | P_type PRED_TYPE
      | A_type SORT -- ambiguous pred or (constant total) op
        deriving (Show,Eq)

data SYMB_OR_MAP = Symb SYMB
         | Symb_map SYMB SYMB [Pos]
           -- pos: "|->"
           deriving (Show,Eq)