AS_Basic_CASL.der.hs revision dfd9b88881346e61fa33e54f7d03924404e35d46
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder{- |
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian MaederModule : $Header$
3a6c7a7ff823616f56cd3d205fc44664a683effdChristian MaederDescription : Abstract syntax of CASL basic specifications
73dfcef93ee2ba07fedf4f3c74bace31853d1b9fChristian MaederCopyright : (c) Klaus Luettich, Christian Maeder, Uni Bremen 2002-2006
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian MaederLicense : GPLv2 or higher, see LICENSE.txt
2eeec5240b424984e3ee26296da1eeab6c6d739eChristian Maeder
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian MaederMaintainer : Christian.Maeder@dfki.de
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian MaederStability : provisional
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian MaederPortability : portable
e6d40133bc9f858308654afb1262b8b483ec5922Till Mossakowski
e6d40133bc9f858308654afb1262b8b483ec5922Till MossakowskiAbstract Syntax of CASL Basic_specs, Symb_items and Symb_map_items.
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder Follows Sect. II:2.2 of the CASL Reference Manual.
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder-}
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maedermodule CASL.AS_Basic_CASL where
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder
85ebda7270c6883b503d3bde4757033c09c25644Christian Maederimport Common.Id
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maederimport Common.AS_Annotation
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maederimport qualified Data.Set as Set
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder
ad270004874ce1d0697fb30d7309f180553bb315Christian Maeder-- DrIFT command
ad270004874ce1d0697fb30d7309f180553bb315Christian Maeder{-! global: GetRange !-}
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maederdata BASIC_SPEC b s f = Basic_spec [Annoted (BASIC_ITEMS b s f)]
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder deriving Show
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maederdata BASIC_ITEMS b s f = Sig_items (SIG_ITEMS s f)
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder {- the Annotation following the keyword is dropped
8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maeder but preceding the keyword is now an Annotation allowed -}
8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maeder | Free_datatype SortsKind [Annoted DATATYPE_DECL] Range
8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maeder -- pos: free, type, semi colons
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder | Sort_gen [Annoted (SIG_ITEMS s f)] Range
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder -- pos: generated, opt. braces
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder | Var_items [VAR_DECL] Range
8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maeder -- pos: var, semi colons
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder | Local_var_axioms [VAR_DECL] [Annoted (FORMULA f)] Range
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder -- pos: forall, semi colons, dots
8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maeder | Axiom_items [Annoted (FORMULA f)] Range
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder -- pos: dots
8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maeder | Ext_BASIC_ITEMS b
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder deriving Show
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maederdata SortsKind = NonEmptySorts | PossiblyEmptySorts deriving Show
8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maeder
6abfd7000f15635fd29746bd841b4c36819e552bTill Mossakowskidata SIG_ITEMS s f = Sort_items SortsKind [Annoted (SORT_ITEM f)] Range
6abfd7000f15635fd29746bd841b4c36819e552bTill Mossakowski -- pos: sort, semi colons
6abfd7000f15635fd29746bd841b4c36819e552bTill Mossakowski | Op_items [Annoted (OP_ITEM f)] Range
6abfd7000f15635fd29746bd841b4c36819e552bTill Mossakowski -- pos: op, semi colons
6abfd7000f15635fd29746bd841b4c36819e552bTill Mossakowski | Pred_items [Annoted (PRED_ITEM f)] Range
6abfd7000f15635fd29746bd841b4c36819e552bTill Mossakowski -- pos: pred, semi colons
6abfd7000f15635fd29746bd841b4c36819e552bTill Mossakowski | Datatype_items SortsKind [Annoted DATATYPE_DECL] Range
6abfd7000f15635fd29746bd841b4c36819e552bTill Mossakowski -- type, semi colons
6abfd7000f15635fd29746bd841b4c36819e552bTill Mossakowski | Ext_SIG_ITEMS s
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder deriving Show
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maederdata SORT_ITEM f = Sort_decl [SORT] Range
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder -- pos: commas
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder | Subsort_decl [SORT] SORT Range
6abfd7000f15635fd29746bd841b4c36819e552bTill Mossakowski -- pos: commas, <
8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maeder | Subsort_defn SORT VAR SORT (Annoted (FORMULA f)) Range
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder {- pos: "=", "{", ":", ".", "}"
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder the left anno list stored in Annoted Formula is
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder parsed after the equal sign -}
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder | Iso_decl [SORT] Range
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder -- pos: "="s
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder deriving Show
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maederdata OP_ITEM f = Op_decl [OP_NAME] OP_TYPE [OP_ATTR f] Range
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder -- pos: commas, colon, OP_ATTR sep. by commas
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder | Op_defn OP_NAME OP_HEAD (Annoted (TERM f)) Range
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder -- pos: "="
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder deriving Show
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maederdata OpKind = Total | Partial deriving (Show, Eq, Ord)
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maederdata OP_TYPE = Op_type OpKind [SORT] SORT Range
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder -- pos: "*"s, "->" ; if null [SORT] then Range = [] or pos: "?"
8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maeder deriving (Show, Eq, Ord)
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maederargs_OP_TYPE :: OP_TYPE -> [SORT]
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maederargs_OP_TYPE (Op_type _ args _ _) = args
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder
8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maederres_OP_TYPE :: OP_TYPE -> SORT
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maederres_OP_TYPE (Op_type _ _ res _) = res
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maederdata OP_HEAD = Op_head OpKind [VAR_DECL] SORT Range
0fe1b901cec27c06b8aad7548f56a7cab4dee6a4Till Mossakowski -- pos: "(", semicolons, ")", colon
0fe1b901cec27c06b8aad7548f56a7cab4dee6a4Till Mossakowski deriving Show
0fe1b901cec27c06b8aad7548f56a7cab4dee6a4Till Mossakowski
0fe1b901cec27c06b8aad7548f56a7cab4dee6a4Till Mossakowskidata OP_ATTR f = Assoc_op_attr | Comm_op_attr | Idem_op_attr
0fe1b901cec27c06b8aad7548f56a7cab4dee6a4Till Mossakowski | Unit_op_attr (TERM f)
0fe1b901cec27c06b8aad7548f56a7cab4dee6a4Till Mossakowski deriving (Show, Eq, Ord)
0fe1b901cec27c06b8aad7548f56a7cab4dee6a4Till Mossakowski
0fe1b901cec27c06b8aad7548f56a7cab4dee6a4Till Mossakowskidata PRED_ITEM f = Pred_decl [PRED_NAME] PRED_TYPE Range
b20cc520e698253354303b7bf3bc17f84240b213Klaus Luettich -- pos: commas, colon
da955132262baab309a50fdffe228c9efe68251dCui Jian | Pred_defn PRED_NAME PRED_HEAD (Annoted (FORMULA f)) Range
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder -- pos: "<=>"
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder deriving Show
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maederdata PRED_TYPE = Pred_type [SORT] Range
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder -- pos: if null [SORT] then "(",")" else "*"s
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder deriving (Show, Eq, Ord)
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder
8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maederdata PRED_HEAD = Pred_head [VAR_DECL] Range
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder -- pos: "(",semi colons , ")"
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder deriving Show
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maederdata DATATYPE_DECL = Datatype_decl SORT [Annoted ALTERNATIVE] Range
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder -- pos: "::=", "|"s
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder deriving Show
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder
8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maederdata ALTERNATIVE = Alt_construct OpKind OP_NAME [COMPONENTS] Range
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder -- pos: "(", semi colons, ")" optional "?"
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder | Subsorts [SORT] Range
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder -- pos: sort, commas
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder deriving Show
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maederdata COMPONENTS = Cons_select OpKind [OP_NAME] SORT Range
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder -- pos: commas, colon or ":?"
8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maeder | Sort SORT
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder deriving Show
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maederdata VAR_DECL = Var_decl [VAR] SORT Range
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder -- pos: commas, colon
8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maeder deriving (Show, Eq, Ord)
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian MaedervarDeclRange :: VAR_DECL -> [Pos]
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian MaedervarDeclRange (Var_decl vs s _) = case vs of
07baaf27fc0029203075ed916999006dcc619ef0Christian Maeder [] -> []
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder v : _ -> joinRanges [tokenRange v, idRange s]
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder{- Position definition for FORMULA:
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder Information on parens are also encoded in Range. If there
8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maeder are more Pos than necessary there is a pair of Pos enclosing the
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder other Pos informations which encode the brackets of every kind
07baaf27fc0029203075ed916999006dcc619ef0Christian Maeder-}
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder
8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maederdata FORMULA f = Quantification QUANTIFIER [VAR_DECL] (FORMULA f) Range
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder -- pos: QUANTIFIER, semi colons, dot
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder | Conjunction [FORMULA f] Range
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder -- pos: "/\"s
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder | Disjunction [FORMULA f] Range
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder -- pos: "\/"s
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder | Implication (FORMULA f) (FORMULA f) Bool Range
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder -- pos: "=>" or "if" (True -> "=>")
8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maeder | Equivalence (FORMULA f) (FORMULA f) Range
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder -- pos: "<=>"
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder | Negation (FORMULA f) Range
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder -- pos: not
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder | True_atom Range
8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maeder -- pos: true
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder | False_atom Range
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder -- pos: false
999f839e42d594e4ae288208fec398626837c41cTill Mossakowski | Predication PRED_SYMB [TERM f] Range
999f839e42d594e4ae288208fec398626837c41cTill Mossakowski -- pos: opt. "(",commas,")"
999f839e42d594e4ae288208fec398626837c41cTill Mossakowski | Definedness (TERM f) Range
999f839e42d594e4ae288208fec398626837c41cTill Mossakowski -- pos: def
999f839e42d594e4ae288208fec398626837c41cTill Mossakowski | Existl_equation (TERM f) (TERM f) Range
999f839e42d594e4ae288208fec398626837c41cTill Mossakowski -- pos: =e=
999f839e42d594e4ae288208fec398626837c41cTill Mossakowski | Strong_equation (TERM f) (TERM f) Range
ad69cb3627839ed3d33f13d71c81378b65a24b35Till Mossakowski -- pos: =
ad69cb3627839ed3d33f13d71c81378b65a24b35Till Mossakowski | Membership (TERM f) SORT Range
ad69cb3627839ed3d33f13d71c81378b65a24b35Till Mossakowski -- pos: in
| Mixfix_formula (TERM f)
{- Mixfix_ Term/Token/(..)/[..]/{..}
a formula left original for mixfix analysis -}
| Unparsed_formula String Range
-- pos: first Char in String
| Sort_gen_ax [Constraint] Bool -- flag: belongs to a free type?
| QuantOp OP_NAME OP_TYPE (FORMULA f) -- second order quantifiers
| QuantPred PRED_NAME PRED_TYPE (FORMULA f)
| ExtFORMULA f
-- needed for CASL extensions
deriving (Show, Eq, Ord)
is_True_atom, is_False_atom :: FORMULA f -> Bool
is_True_atom (True_atom _) = True
is_True_atom _ = False
is_False_atom (False_atom _) = True
is_False_atom _ = False
{- In the CASL institution, sort generation constraints have an
additional signature morphism component (Sect. III:2.1.3, p.134 of the
CASL Reference Manual). The extra signature morphism component is
needed because the naive translation of sort generation constraints
along signature morphisms may violate the satisfaction condition,
namely when sorts are identified by the translation, with the effect
that new terms can be formed. We avoid this extra component here and
instead use natural numbers to decorate sorts, in this way retaining
their identity w.r.t. the original signature. The newSort in a
Constraint is implicitly decorated with its index in the list of
Constraints. The opSymbs component collects all the operation symbols
with newSort (with that index!) as a result sort. The argument sorts
of an operation symbol are decorated explicitly via a list [Int] of
integers. The origSort in a Constraint is the original sort
corresponding to the index. A negative index indicates a sort outside
the constraint (i.e. a "parameter sort"). Note that this representation of
sort generation constraints is efficiently tailored towards both the use in
the proof calculus (Chap. IV:2, p. 282 of the CASL Reference Manual)
and the coding into second order logic (p. 429 of Theoret. Comp. Sci. 286).
-}
data Constraint = Constraint { newSort :: SORT,
opSymbs :: [(OP_SYMB, [Int])],
origSort :: SORT }
deriving (Show, Eq, Ord)
-- | no duplicate sorts, i.e. injective sort map?
isInjectiveList :: Ord a => [a] -> Bool
isInjectiveList l = Set.size (Set.fromList l) == length l
{- | from a Sort_gex_ax, recover:
a traditional sort generation constraint plus a sort mapping -}
recover_Sort_gen_ax :: [Constraint] ->
([SORT], [OP_SYMB], [(SORT, SORT)])
recover_Sort_gen_ax constrs =
if isInjectiveList sorts
-- we can ignore indices
then (sorts, map fst (concatMap opSymbs constrs), [])
{- otherwise, we have to introduce new sorts for the indices
and afterwards rename them into the sorts they denote -}
else (map indSort1 indices, map indOp indOps1, map sortMap indSorts)
where
sorts = map newSort constrs
indices = [0 .. length sorts - 1]
indSorts = zip indices sorts
indSort (i, s) = if i < 0 then s else indSort1 i
indSort1 = origSort . (constrs !!)
sortMap (i, s) = (indSort1 i, s)
indOps = zip indices (map opSymbs constrs)
indOps1 = concatMap (\ (i, ops) -> map ((,) i) ops) indOps
indOp (res, (Qual_op_name on (Op_type k args1 res1 pos1) pos, args)) =
Qual_op_name on
(Op_type k (map indSort (zip args args1))
(indSort (res, res1)) pos1) pos
indOp _ = error
"CASL/AS_Basic_CASL: Internal error: Unqualified OP_SYMB in Sort_gen_ax"
{- | from a free Sort_gex_ax, recover:
the sorts, each paired with the constructors
fails (i.e. delivers Nothing) if the sort map is not injective -}
recover_free_Sort_gen_ax :: [Constraint] -> Maybe [(SORT, [OP_SYMB])]
recover_free_Sort_gen_ax constrs =
if isInjectiveList sorts
then Just $ map getOpProfile constrs
else Nothing
where
sorts = map newSort constrs
getOpProfile constr = (newSort constr, map fst $ opSymbs constr)
data QUANTIFIER = Universal | Existential | Unique_existential
deriving (Show, Eq, Ord)
data PRED_SYMB = Pred_name PRED_NAME
| Qual_pred_name PRED_NAME PRED_TYPE Range
-- pos: "(", pred, colon, ")"
deriving (Show, Eq, Ord)
predSymbName :: PRED_SYMB -> PRED_NAME
predSymbName p = case p of
Pred_name n -> n
Qual_pred_name n _ _ -> n
data TERM f = Qual_var VAR SORT Range -- pos: "(", var, colon, ")"
| Application OP_SYMB [TERM f] Range
-- pos: parens around TERM f if any and seperating commas
| Sorted_term (TERM f) SORT Range
-- pos: colon
| Cast (TERM f) SORT Range
-- pos: "as"
| Conditional (TERM f) (FORMULA f) (TERM f) Range
-- pos: "when", "else"
| Unparsed_term String Range -- 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 Range
-- pos: colon
| Mixfix_cast SORT Range
-- pos: "as"
| Mixfix_parenthesized [TERM f] Range
{- non-emtpy term list
pos: "(", commas, ")" -}
| Mixfix_bracketed [TERM f] Range
-- pos: "[", commas, "]"
| Mixfix_braced [TERM f] Range
{- also for list-notation
pos: "{", "}" -}
| ExtTERM f
deriving (Show, Eq, Ord)
-- | state after mixfix- but before overload resolution
varOrConst :: Token -> TERM f
varOrConst t = Application (Op_name $ simpleIdToId t) [] $ tokPos t
data OP_SYMB = Op_name OP_NAME
| Qual_op_name OP_NAME OP_TYPE Range
-- pos: "(", op, colon, ")"
deriving (Show, Eq, Ord)
opSymbName :: OP_SYMB -> OP_NAME
opSymbName o = case o of
Op_name n -> n
Qual_op_name n _ _ -> n
type CASLFORMULA = FORMULA ()
type CASLTERM = TERM ()
type OP_NAME = Id
type PRED_NAME = Id
type SORT = Id
type VAR = Token
data SYMB_ITEMS = Symb_items SYMB_KIND [SYMB] Range
-- pos: SYMB_KIND, commas
deriving (Show, Eq)
data SYMB_MAP_ITEMS = Symb_map_items SYMB_KIND [SYMB_OR_MAP] Range
-- pos: SYMB_KIND, commas
deriving (Show, Eq)
data SYMB_KIND = Implicit | Sorts_kind
| Ops_kind | Preds_kind | OtherKinds String
deriving (Show, Eq, Ord)
data SYMB = Symb_id Id
| Qual_id Id TYPE Range
-- 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 Range
-- pos: "|->"
deriving (Show, Eq)