AS_Basic_CASL.der.hs revision 4d4ec273e5cb1f17985c6edcf90a295a8b612cef
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng JiangModule : $Header$
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng JiangDescription : Abstract syntax of CASL basic specifications
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng JiangCopyright : (c) Klaus L�ttich, Christian Maeder, Uni Bremen 2002-2006
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng JiangLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng JiangMaintainer : Christian.Maeder@dfki.de
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng JiangStability : provisional
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng JiangPortability : portable
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng JiangAbstract Syntax of CASL Basic_specs, Symb_items and Symb_map_items.
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang Follows Sect. II:2.2 of the CASL Reference Manual.
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang-- DrIFT command
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang{-! global: UpPos !-}
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiangdata BASIC_SPEC b s f = Basic_spec [Annoted (BASIC_ITEMS b s f)]
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang deriving Show
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiangdata BASIC_ITEMS b s f = Sig_items (SIG_ITEMS s f)
806bce66335c88260a63e7524b1efc68d8dfacc1Heng Jiang -- the Annotation following the keyword is dropped
806bce66335c88260a63e7524b1efc68d8dfacc1Heng Jiang -- but preceding the keyword is now an Annotation allowed
806bce66335c88260a63e7524b1efc68d8dfacc1Heng Jiang | Free_datatype [Annoted DATATYPE_DECL] Range
806bce66335c88260a63e7524b1efc68d8dfacc1Heng Jiang -- pos: free, type, semi colons
806bce66335c88260a63e7524b1efc68d8dfacc1Heng Jiang | Sort_gen [Annoted (SIG_ITEMS s f)] Range
806bce66335c88260a63e7524b1efc68d8dfacc1Heng Jiang -- pos: generated, opt. braces
806bce66335c88260a63e7524b1efc68d8dfacc1Heng Jiang | Var_items [VAR_DECL] Range
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang -- pos: var, semi colons
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang | Local_var_axioms [VAR_DECL] [Annoted (FORMULA f)] Range
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang -- pos: forall, semi colons, dots
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang | Axiom_items [Annoted (FORMULA f)] Range
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang -- pos: dots
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang | Ext_BASIC_ITEMS b
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang deriving Show
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiangdata SortsKind = NonEmptySorts | PossiblyEmptySorts deriving Show
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiangdata SIG_ITEMS s f = Sort_items SortsKind [Annoted (SORT_ITEM f)] Range
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang -- pos: sort, semi colons
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang | Op_items [Annoted (OP_ITEM f)] Range
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang -- pos: op, semi colons
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang | Pred_items [Annoted (PRED_ITEM f)] Range
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang -- pos: pred, semi colons
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang | Datatype_items [Annoted DATATYPE_DECL] Range
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang -- type, semi colons
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang | Ext_SIG_ITEMS s
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang deriving Show
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiangdata SORT_ITEM f = Sort_decl [SORT] Range
806bce66335c88260a63e7524b1efc68d8dfacc1Heng Jiang -- pos: commas
806bce66335c88260a63e7524b1efc68d8dfacc1Heng Jiang | Subsort_decl [SORT] SORT Range
806bce66335c88260a63e7524b1efc68d8dfacc1Heng Jiang -- pos: commas, <
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang | Subsort_defn SORT VAR SORT (Annoted (FORMULA f)) Range
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang -- pos: "=", "{", ":", ".", "}"
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang -- the left anno list stored in Annoted Formula is
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang -- parsed after the equal sign
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang | Iso_decl [SORT] Range
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang -- pos: "="s
806bce66335c88260a63e7524b1efc68d8dfacc1Heng Jiang deriving Show
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiangdata OP_ITEM f = Op_decl [OP_NAME] OP_TYPE [OP_ATTR f] Range
806bce66335c88260a63e7524b1efc68d8dfacc1Heng Jiang -- pos: commas, colon, OP_ATTR sep. by commas
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang | Op_defn OP_NAME OP_HEAD (Annoted (TERM f)) Range
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang deriving Show
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiangdata FunKind = Total | Partial deriving (Show, Eq, Ord)
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiangdata OP_TYPE = Op_type FunKind [SORT] SORT Range
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang -- pos: "*"s, "->" ; if null [SORT] then Range = [] or pos: "?"
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang deriving (Show, Eq, Ord)
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiangargs_OP_TYPE :: OP_TYPE -> [SORT]
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiangargs_OP_TYPE (Op_type _ args _ _) = args
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiangres_OP_TYPE :: OP_TYPE -> SORT
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiangres_OP_TYPE (Op_type _ _ res _) = res
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiangdata OP_HEAD = Op_head FunKind [ARG_DECL] SORT Range
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang -- pos: "(", semicolons, ")", colon
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang deriving Show
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiangdata ARG_DECL = Arg_decl [VAR] SORT Range
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang -- pos: commas, colon
6c8dc7ab7cb52a12cba748fe0f6b8d8d17a95eb9Heng Jiang deriving Show
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiangdata OP_ATTR f = Assoc_op_attr | Comm_op_attr | Idem_op_attr
6c8dc7ab7cb52a12cba748fe0f6b8d8d17a95eb9Heng Jiang | Unit_op_attr (TERM f)
6c8dc7ab7cb52a12cba748fe0f6b8d8d17a95eb9Heng Jiang deriving (Show, Eq, Ord)
6c8dc7ab7cb52a12cba748fe0f6b8d8d17a95eb9Heng Jiangdata PRED_ITEM f = Pred_decl [PRED_NAME] PRED_TYPE Range
6c8dc7ab7cb52a12cba748fe0f6b8d8d17a95eb9Heng Jiang -- pos: commas, colon
0b31ea5ec0e20f17d55845a5d803c48466e01ca3Heng Jiang | Pred_defn PRED_NAME PRED_HEAD (Annoted (FORMULA f)) Range
0b31ea5ec0e20f17d55845a5d803c48466e01ca3Heng Jiang -- pos: "<=>"
0b31ea5ec0e20f17d55845a5d803c48466e01ca3Heng Jiang deriving Show
0b31ea5ec0e20f17d55845a5d803c48466e01ca3Heng Jiangdata PRED_TYPE = Pred_type [SORT] Range
0b31ea5ec0e20f17d55845a5d803c48466e01ca3Heng Jiang -- pos: if null [SORT] then "(",")" else "*"s
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang deriving (Show, Eq, Ord)
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiangdata PRED_HEAD = Pred_head [ARG_DECL] Range
31ac08a9e5233b83a63fd5aaac494c32305c4c77Heng Jiang -- pos: "(",semi colons , ")"
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang deriving Show
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiangdata DATATYPE_DECL = Datatype_decl SORT [Annoted ALTERNATIVE] Range
f0a4ace924cef940ca4cc646fa180df70ef405d8Klaus Luettich -- pos: "::=", "|"s
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang deriving Show
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiangdata ALTERNATIVE = Alt_construct FunKind OP_NAME [COMPONENTS] Range
0b31ea5ec0e20f17d55845a5d803c48466e01ca3Heng Jiang -- pos: "(", semi colons, ")" optional "?"
0b31ea5ec0e20f17d55845a5d803c48466e01ca3Heng Jiang | Subsorts [SORT] Range
0b31ea5ec0e20f17d55845a5d803c48466e01ca3Heng Jiang -- pos: sort, commas
0b31ea5ec0e20f17d55845a5d803c48466e01ca3Heng Jiang deriving Show
0b31ea5ec0e20f17d55845a5d803c48466e01ca3Heng Jiangdata COMPONENTS = Cons_select FunKind [OP_NAME] SORT Range
0b31ea5ec0e20f17d55845a5d803c48466e01ca3Heng Jiang -- pos: commas, colon or ":?"
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang deriving Show
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiangdata VAR_DECL = Var_decl [VAR] SORT Range
31ac08a9e5233b83a63fd5aaac494c32305c4c77Heng Jiang -- pos: commas, colon
31ac08a9e5233b83a63fd5aaac494c32305c4c77Heng Jiang deriving (Show, Eq, Ord)
806bce66335c88260a63e7524b1efc68d8dfacc1Heng Jiang{- Position definition for FORMULA:
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang Information on parens are also encoded in Range. If there
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang are more Pos than necessary there is a pair of Pos enclosing the
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang other Pos informations which encode the brackets of every kind
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiangdata FORMULA f = Quantification QUANTIFIER [VAR_DECL] (FORMULA f) Range
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang -- pos: QUANTIFIER, semi colons, dot
6c8dc7ab7cb52a12cba748fe0f6b8d8d17a95eb9Heng Jiang | Conjunction [FORMULA f] Range
6c8dc7ab7cb52a12cba748fe0f6b8d8d17a95eb9Heng Jiang -- pos: "/\"s
6c8dc7ab7cb52a12cba748fe0f6b8d8d17a95eb9Heng Jiang | Disjunction [FORMULA f] Range
6c8dc7ab7cb52a12cba748fe0f6b8d8d17a95eb9Heng Jiang -- pos: "\/"s
6c8dc7ab7cb52a12cba748fe0f6b8d8d17a95eb9Heng Jiang | Implication (FORMULA f) (FORMULA f) Bool Range
6c8dc7ab7cb52a12cba748fe0f6b8d8d17a95eb9Heng Jiang -- pos: "=>" or "if" (True -> "=>")
6c8dc7ab7cb52a12cba748fe0f6b8d8d17a95eb9Heng Jiang | Equivalence (FORMULA f) (FORMULA f) Range
6c8dc7ab7cb52a12cba748fe0f6b8d8d17a95eb9Heng Jiang -- pos: "<=>"
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang | Negation (FORMULA f) Range
6c8dc7ab7cb52a12cba748fe0f6b8d8d17a95eb9Heng Jiang | True_atom Range
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang -- pos: true
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang | False_atom Range
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang -- pos: false
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang | Predication PRED_SYMB [TERM f] Range
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang -- pos: opt. "(",commas,")"
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang | Definedness (TERM f) Range
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang | Existl_equation (TERM f) (TERM f) Range
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang | Strong_equation (TERM f) (TERM f) Range
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang | Membership (TERM f) SORT Range
806bce66335c88260a63e7524b1efc68d8dfacc1Heng Jiang | Mixfix_formula (TERM f) -- Mixfix_ Term/Token/(..)/[..]/{..}
806bce66335c88260a63e7524b1efc68d8dfacc1Heng Jiang -- a formula left original for mixfix analysis
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang | Unparsed_formula String Range
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang -- pos: first Char in String
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang | Sort_gen_ax [Constraint] Bool -- flag: belongs to a free type?
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang | ExtFORMULA f
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang -- needed for CASL extensions
f0a4ace924cef940ca4cc646fa180df70ef405d8Klaus Luettich deriving (Show, Eq, Ord)
f0a4ace924cef940ca4cc646fa180df70ef405d8Klaus Luettichis_True_atom, is_False_atom :: FORMULA f -> Bool
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiangis_True_atom (True_atom _) = True
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiangis_True_atom _ = False
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiangis_False_atom (False_atom _) = True
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiangis_False_atom _ = False
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang{- In the CASL institution, sort generation constraints have an
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiangadditional signature morphism component (Sect. III:2.1.3, p.134 of the
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng JiangCASL Reference Manual). The extra signature morphism component is
6c8dc7ab7cb52a12cba748fe0f6b8d8d17a95eb9Heng Jiangneeded because the naive translation of sort generation constraints
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiangalong signature morphisms may violate the satisfaction condition,
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiangnamely when sorts are identified by the translation, with the effect
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiangthat new terms can be formed. We avoid this extra component here and
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jianginstead use natural numbers to decorate sorts, in this way retaining
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiangtheir identity w.r.t. the original signature. The newSort in a
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng JiangConstraint is implicitly decorated with its index in the list of
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng JiangConstraints. The opSymbs component collects all the operation symbols
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiangwith newSort (with that index!) as a result sort. The argument sorts
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiangof an operation symbol are decorated explicitly via a list [Int] of
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiangintegers. The origSort in a Constraint is the original sort
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiangcorresponding to the index. A negative index indicates a sort outside
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiangthe constraint (i.e. a "parameter sort"). Note that this representation of
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiangsort generation constraints is efficiently tailored towards both the use in
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiangthe proof calculus (Chap. IV:2, p. 282 of the CASL Reference Manual)
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiangand the coding into second order logic (p. 429 of Theoret. Comp. Sci. 286).
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiangdata Constraint = Constraint { newSort :: SORT,
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang opSymbs :: [(OP_SYMB,[Int])],
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang origSort :: SORT }
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang deriving (Show, Eq, Ord)
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang-- | from a Sort_gex_ax, recover:
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang-- | a traditional sort generation constraint plus a sort mapping
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiangrecover_Sort_gen_ax :: [Constraint] ->
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang ([SORT],[OP_SYMB],[(SORT,SORT)])
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiangrecover_Sort_gen_ax constrs =
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang if length (nub sorts) == length sorts
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang -- no duplicate sorts, i.e. injective sort map? Then we can ignore indices
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang then (sorts,map fst (concat (map opSymbs constrs)),[])
175c9e5fde43fc804a8d25198133288669b9d54cKlaus Luettich -- otherwise, we have to introduce new sorts for the indices
175c9e5fde43fc804a8d25198133288669b9d54cKlaus Luettich -- and afterwards rename them into the sorts they denote
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang else (map indSort1 indices,map indOp indOps1,map sortMap indSorts)
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang sorts = map newSort constrs
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang indices = [0..length sorts-1]
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang indSorts = zip indices sorts
b91c4dbd00294ce29ab1ae84ad4e8c93ca5ad943Heng Jiang indSort (i,s) = if i<0 then s else indSort1 i
b91c4dbd00294ce29ab1ae84ad4e8c93ca5ad943Heng Jiang indSort1 i = origSort $ head (drop i constrs)
175c9e5fde43fc804a8d25198133288669b9d54cKlaus Luettich sortMap (i,s) = (indSort1 i,s)
b91c4dbd00294ce29ab1ae84ad4e8c93ca5ad943Heng Jiang indOps = zip indices (map opSymbs constrs)
b91c4dbd00294ce29ab1ae84ad4e8c93ca5ad943Heng Jiang indOps1 = concat (map (\(i,ops) -> map ((,) i) ops) indOps)
b91c4dbd00294ce29ab1ae84ad4e8c93ca5ad943Heng Jiang indOp (res,(Qual_op_name on (Op_type k args1 res1 pos1) pos,args)) =
b91c4dbd00294ce29ab1ae84ad4e8c93ca5ad943Heng Jiang Qual_op_name on
b91c4dbd00294ce29ab1ae84ad4e8c93ca5ad943Heng Jiang (Op_type k (map indSort (zip args args1))
b91c4dbd00294ce29ab1ae84ad4e8c93ca5ad943Heng Jiang (indSort (res,res1)) pos1) pos
b91c4dbd00294ce29ab1ae84ad4e8c93ca5ad943Heng Jiang indOp _ = error
b91c4dbd00294ce29ab1ae84ad4e8c93ca5ad943Heng Jiang "CASL/AS_Basic_CASL: Internal error: Unqualified OP_SYMB in Sort_gen_ax"
b91c4dbd00294ce29ab1ae84ad4e8c93ca5ad943Heng Jiang-- | from a free Sort_gex_ax, recover:
b91c4dbd00294ce29ab1ae84ad4e8c93ca5ad943Heng Jiang-- | the sorts, each paired with the constructors
b91c4dbd00294ce29ab1ae84ad4e8c93ca5ad943Heng Jiang-- | fails (i.e. delivers Nothing) if the sort map is not injective
b91c4dbd00294ce29ab1ae84ad4e8c93ca5ad943Heng Jiangrecover_free_Sort_gen_ax :: [Constraint] -> Maybe [(SORT,[OP_SYMB])]
b91c4dbd00294ce29ab1ae84ad4e8c93ca5ad943Heng Jiangrecover_free_Sort_gen_ax constrs =
b91c4dbd00294ce29ab1ae84ad4e8c93ca5ad943Heng Jiang if length (nub sorts) == length sorts
b91c4dbd00294ce29ab1ae84ad4e8c93ca5ad943Heng Jiang -- no duplicate sorts, i.e. injective sort map?
b91c4dbd00294ce29ab1ae84ad4e8c93ca5ad943Heng Jiang then Just $ map getOpProfile constrs
b91c4dbd00294ce29ab1ae84ad4e8c93ca5ad943Heng Jiang else Nothing
b91c4dbd00294ce29ab1ae84ad4e8c93ca5ad943Heng Jiang sorts = map newSort constrs
b91c4dbd00294ce29ab1ae84ad4e8c93ca5ad943Heng Jiang getOpProfile constr = (newSort constr,map fst $ opSymbs constr)
b91c4dbd00294ce29ab1ae84ad4e8c93ca5ad943Heng Jiangdata QUANTIFIER = Universal | Existential | Unique_existential
b91c4dbd00294ce29ab1ae84ad4e8c93ca5ad943Heng Jiang deriving (Show, Eq, Ord)
b91c4dbd00294ce29ab1ae84ad4e8c93ca5ad943Heng Jiangdata PRED_SYMB = Pred_name PRED_NAME
b91c4dbd00294ce29ab1ae84ad4e8c93ca5ad943Heng Jiang | Qual_pred_name PRED_NAME PRED_TYPE Range
c51b5677113ce7260c44afb3c5932eea6c875e27Heng Jiang -- pos: "(", pred, colon, ")"
b91c4dbd00294ce29ab1ae84ad4e8c93ca5ad943Heng Jiang deriving (Show, Eq, Ord)
67d5e49547d78aa56a8f9ba5e64a950b730eba66Till Mossakowskidata TERM f = Simple_id SIMPLE_ID -- "Var" might be a better constructor
67d5e49547d78aa56a8f9ba5e64a950b730eba66Till Mossakowski | Qual_var VAR SORT Range
67d5e49547d78aa56a8f9ba5e64a950b730eba66Till Mossakowski -- pos: "(", var, colon, ")"
67d5e49547d78aa56a8f9ba5e64a950b730eba66Till Mossakowski | Application OP_SYMB [TERM f] Range
67d5e49547d78aa56a8f9ba5e64a950b730eba66Till Mossakowski -- pos: parens around TERM f if any and seperating commas
67d5e49547d78aa56a8f9ba5e64a950b730eba66Till Mossakowski | Sorted_term (TERM f) SORT Range
67d5e49547d78aa56a8f9ba5e64a950b730eba66Till Mossakowski -- pos: colon
67d5e49547d78aa56a8f9ba5e64a950b730eba66Till Mossakowski | Cast (TERM f) SORT Range
67d5e49547d78aa56a8f9ba5e64a950b730eba66Till Mossakowski | Conditional (TERM f) (FORMULA f) (TERM f) Range
67d5e49547d78aa56a8f9ba5e64a950b730eba66Till Mossakowski -- pos: "when", "else"
67d5e49547d78aa56a8f9ba5e64a950b730eba66Till Mossakowski | Unparsed_term String Range -- SML-CATS
67d5e49547d78aa56a8f9ba5e64a950b730eba66Till Mossakowski -- A new intermediate state
67d5e49547d78aa56a8f9ba5e64a950b730eba66Till Mossakowski | Mixfix_qual_pred PRED_SYMB -- as part of a mixfix formula
67d5e49547d78aa56a8f9ba5e64a950b730eba66Till Mossakowski | Mixfix_term [TERM f] -- not starting with Mixfix_sorted_term/cast
67d5e49547d78aa56a8f9ba5e64a950b730eba66Till Mossakowski | Mixfix_token Token -- NO-BRACKET-TOKEN, LITERAL, PLACE
6c8dc7ab7cb52a12cba748fe0f6b8d8d17a95eb9Heng Jiang | Mixfix_sorted_term SORT Range
6c8dc7ab7cb52a12cba748fe0f6b8d8d17a95eb9Heng Jiang -- pos: colon
6c8dc7ab7cb52a12cba748fe0f6b8d8d17a95eb9Heng Jiang | Mixfix_cast SORT Range
6c8dc7ab7cb52a12cba748fe0f6b8d8d17a95eb9Heng Jiang -- pos: "as"
6c8dc7ab7cb52a12cba748fe0f6b8d8d17a95eb9Heng Jiang | Mixfix_parenthesized [TERM f] Range -- non-emtpy term list
6c8dc7ab7cb52a12cba748fe0f6b8d8d17a95eb9Heng Jiang -- pos: "(", commas, ")"
6c8dc7ab7cb52a12cba748fe0f6b8d8d17a95eb9Heng Jiang | Mixfix_bracketed [TERM f] Range
6c8dc7ab7cb52a12cba748fe0f6b8d8d17a95eb9Heng Jiang -- pos: "[", commas, "]"
6c8dc7ab7cb52a12cba748fe0f6b8d8d17a95eb9Heng Jiang | Mixfix_braced [TERM f] Range -- also for list-notation
6c8dc7ab7cb52a12cba748fe0f6b8d8d17a95eb9Heng Jiang -- pos: "{", "}"
6c8dc7ab7cb52a12cba748fe0f6b8d8d17a95eb9Heng Jiang deriving (Show, Eq, Ord)
6c8dc7ab7cb52a12cba748fe0f6b8d8d17a95eb9Heng Jiangdata OP_SYMB = Op_name OP_NAME
6c8dc7ab7cb52a12cba748fe0f6b8d8d17a95eb9Heng Jiang | Qual_op_name OP_NAME OP_TYPE Range
6c8dc7ab7cb52a12cba748fe0f6b8d8d17a95eb9Heng Jiang -- pos: "(", op, colon, ")"
6c8dc7ab7cb52a12cba748fe0f6b8d8d17a95eb9Heng Jiang deriving (Show, Eq, Ord)
6c8dc7ab7cb52a12cba748fe0f6b8d8d17a95eb9Heng Jiangtype OP_NAME = Id
6c8dc7ab7cb52a12cba748fe0f6b8d8d17a95eb9Heng Jiangtype PRED_NAME = Id
67d5e49547d78aa56a8f9ba5e64a950b730eba66Till Mossakowskitype SORT = Id
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiangtype VAR = SIMPLE_ID
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiangdata SYMB_ITEMS = Symb_items SYMB_KIND [SYMB] Range
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang -- pos: SYMB_KIND, commas
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang deriving (Show, Eq)
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiangdata SYMB_MAP_ITEMS = Symb_map_items SYMB_KIND [SYMB_OR_MAP] Range
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang -- pos: SYMB_KIND, commas
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang deriving (Show, Eq)
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiangdata SYMB_KIND = Implicit | Sorts_kind
b91c4dbd00294ce29ab1ae84ad4e8c93ca5ad943Heng Jiang | Ops_kind | Preds_kind
c51b5677113ce7260c44afb3c5932eea6c875e27Heng Jiang deriving (Show, Eq)
b3c65285705f6d184b5f8b00b1a328d96b6b19c5Heng Jiangdata SYMB = Symb_id Id
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang | Qual_id Id TYPE Range
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang -- pos: colon
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang deriving (Show, Eq)
b3c65285705f6d184b5f8b00b1a328d96b6b19c5Heng Jiangdata TYPE = O_type OP_TYPE
c51b5677113ce7260c44afb3c5932eea6c875e27Heng Jiang | P_type PRED_TYPE
c51b5677113ce7260c44afb3c5932eea6c875e27Heng Jiang | A_type SORT -- ambiguous pred or (constant total) op
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang deriving (Show, Eq)
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiangdata SYMB_OR_MAP = Symb SYMB
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang | Symb_map SYMB SYMB Range
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang -- pos: "|->"
95242ab07e9aa13b37c16cac36a75d190e1766e4Heng Jiang deriving (Show, Eq)