-- | Stability of logic implementations
data Stability = Stable | Testing | Unstable | Experimental
-- | shortcut for class constraints
class ShATermConvertible a => Convertible a
instance ShATermConvertible a => Convertible a
-- | shortcut for class constraints
class (Pretty a, Convertible a) => PrintTypeConv a
instance (Pretty a, Convertible a) => PrintTypeConv a
-- | shortcut for class constraints with equality
class (Eq a, PrintTypeConv a) => EqPrintTypeConv a
instance (Eq a, PrintTypeConv a) => EqPrintTypeConv a
{- | the name of a logic.
Define instances like "data CASL = CASL deriving Show"
class Show lid => Language lid where
language_name :: lid -> String
description :: lid -> String
-- default implementation
{- | Categories are given as usual: objects, morphisms, identities,
domain, codomain and composition. The type id is the name, or
the identity of the category. It is an argument to all functions
of the type class, serving disambiguation among instances
(via the functional dependency lid -> object morphism).
The types for objects and morphisms may be restricted to
subtypes, using legal_obj and legal_mor. For example, for the
category of sets and injective maps, legal_mor would check
injectivity. Since Eq is a subclass of Category, it is also
possible to impose a quotient on the types for objects and morphisms.
Require Ord instances only for efficiency,
i.e. in sets or maps.
class (Ord object, Ord morphism)
=> Category object morphism | morphism -> object where
ide :: object -> morphism
{- | composition, in diagrammatic order,
if intermediate objects are equal (not checked!) -}
composeMorphisms :: morphism -> morphism -> Result morphism
-- | domain and codomain of morphisms
dom, cod :: morphism -> object
-- | the inverse of a morphism
inverse :: morphism -> Result morphism
-- | test if the signature morphism an inclusion
isInclusion :: morphism -> Bool
isInclusion _ = False -- in general no inclusion
-- | is a value of type morphism denoting a legal morphism?
legal_mor :: morphism -> Result ()
-- | test if the signature morphism is the identity
isIdentity :: Category object morphism => morphism -> Bool
isIdentity m = isInclusion m && dom m == cod m
comp :: Category object morphism => morphism -> morphism -> Result morphism
comp m1 m2 = if cod m1 == dom m2 then composeMorphisms m1 m2 else
fail "target of first and source of second morphism are different"
instance Ord sign => Category sign (DefaultMorphism sign) where
dom = domOfDefaultMorphism
cod = codOfDefaultMorphism
ide = ideOfDefaultMorphism
composeMorphisms = compOfDefaultMorphism
{- | Abstract syntax, parsing and printing.
There are three types for abstract syntax:
basic_spec is for basic specifications (see CASL RefMan p. 5ff.),
symb_items is for symbol lists (see CASL RefMan p. 35ff.),
symb_map_items is for symbol maps (see CASL RefMan p. 35ff.).
class (Language lid, PrintTypeConv basic_spec, GetRange basic_spec,
EqPrintTypeConv symb_items,
EqPrintTypeConv symb_map_items)
=> Syntax lid basic_spec symb_items symb_map_items
| lid -> basic_spec symb_items symb_map_items
-- | parsers and printers
parsersAndPrinters :: lid ->
Map.Map IRI
(AParser st basic_spec, basic_spec -> Doc)
parsersAndPrinters li = case parse_basic_spec li of
Just p -> makeDefault (p, pretty)
-- | parser for basic specifications
parse_basic_spec :: lid -> Maybe (AParser st basic_spec)
-- | parser for symbol lists
parse_symb_items :: lid -> Maybe (AParser st symb_items)
-- | parser for symbol maps
parse_symb_map_items :: lid -> Maybe (AParser st symb_map_items)
toItem :: lid -> basic_spec -> Item
-- default implementations
parse_basic_spec _ = Nothing
parse_symb_items _ = Nothing
parse_symb_map_items _ = Nothing
toItem _ bs = mkFlatItem ("Basicspec", pretty bs) $ getRangeSpan bs
basicSpecParser :: Syntax lid basic_spec symb_items symb_map_items
=> Maybe IRI -> lid -> Maybe (AParser st basic_spec)
basicSpecParser sm = fmap fst . parserAndPrinter sm
basicSpecPrinter :: Syntax lid basic_spec symb_items symb_map_items
=> Maybe IRI -> lid -> Maybe (basic_spec -> Doc)
basicSpecPrinter sm = fmap snd . parserAndPrinter sm
parserAndPrinter :: Syntax lid basic_spec symb_items symb_map_items
=> Maybe IRI -> lid -> Maybe (AParser st basic_spec, basic_spec -> Doc)
parserAndPrinter sm = lookupDefault sm . parsersAndPrinters
-- | function to lookup parser or printer
lookupDefault :: Maybe IRI ->
Map.Map IRI b -> Maybe b
showSyntax :: Language lid => lid -> Maybe IRI -> String
showSyntax lid = (("logic " ++ language_name lid) ++)
. maybe "" ((" serialization " ++) . iriToStringUnsecure)
addSyntax =
Map.insert . simpleIdToIRI . mkSimpleId
{- | Sentences, provers and symbols.
Provers capture the entailment relation between sets of sentences
and sentences. They may return proof trees witnessing proofs.
Signatures are equipped with underlying sets of symbols
(such that the category of signatures becomes a concrete category),
see CASL RefMan p. 191ff.
class (Language lid, Category sign morphism, Ord sentence,
Ord symbol, -- for efficient lookup
PrintTypeConv sign, PrintTypeConv morphism,
GetRange sentence, GetRange symbol,
PrintTypeConv sentence, PrintTypeConv symbol)
=> Sentences lid sentence sign morphism symbol
| lid -> sentence sign morphism symbol
-- | sentence translation along a signature morphism
map_sen :: lid -> morphism -> sentence -> Result sentence
map_sen l _ _ = statFail l "map_sen"
-- | simplification of sentences (leave out qualifications)
simplify_sen :: lid -> sign -> sentence -> sentence
-- | negation of a sentence for disproving
negation :: lid -> sentence -> Maybe sentence
-- | modified signature printing when followed by sentences
print_sign :: lid -> sign -> Doc
-- | print a sentence with comments
print_named :: lid -> Named sentence -> Doc
print_named _ = printAnnoted (addBullet . pretty) . fromLabelledSen
-- --------------------- symbols ---------------------------
-- | dependency ordered list of symbol sets for a signature
sym_of :: lid -> sign -> [
Set.Set symbol]
{- | Dependency ordered list of a bigger symbol set for a
signature. This function contains more symbols than those being subject
to hiding and renaming (given by 'sym_of') to better represent a
signature as a set of symbols given within xml files. At least for CASL
additional symbols for (direct) subsorts will be created, but note, that
no symbol for a partial function will be created, if the signature
contains this function as total, although a signature with just that
partial function would be a subsignature. This function is supposed to
work over partial signatures created by 'signatureDiff'. -}
mostSymsOf :: lid -> sign -> [symbol]
-- | symbol map for a signature morphism
symmap_of :: lid -> morphism -> EndoMap symbol
-- | symbols have a name, see CASL RefMan p. 192
sym_name :: lid -> symbol -> Id
sym_name l _ = statError l "sym_name"
-- | a logic dependent kind of a symbol
symKind :: lid -> symbol -> String
-- | the symbols occuring in a sentence (any order)
symsOfSen :: lid -> sentence -> [symbol]
-- | makes a singleton list from the given value
singletonList :: a -> [a]
-- | set of symbols for a signature
symset_of :: forall lid sentence sign morphism symbol .
Sentences lid sentence sign morphism symbol =>
-- | dependency ordered list of symbols for a signature
symlist_of :: forall lid sentence sign morphism symbol .
Sentences lid sentence sign morphism symbol =>
symlist_of lid sig = concatMap
Set.toList $ sym_of lid sig
-- | a dummy static analysis function to allow type checking *
.inline.hs files
inlineAxioms :: StaticAnalysis lid
basic_spec sentence symb_items symb_map_items
sign morphism symbol raw_symbol => lid -> String -> [Named sentence]
inlineAxioms _ _ = error "inlineAxioms"
-- | fail function for static analysis
statFail :: (Language lid, Monad m) => lid -> String -> m a
statFail lid = fail . statErrMsg lid
statError :: Language lid => lid -> String -> a
statError lid = error . statErrMsg lid
-- | error message for static analysis
statErrMsg :: Language lid => lid -> String -> String
"Logic." ++ str ++ " not implemented for: " ++ language_name lid
This type class provides the data needed for an institution with symbols,
as explained in the structured specification semantics in the CASL
reference manual, chapter III.4.
The static analysis computes signatures from basic specifications,
and signature morphisms from symbol lists and symbol maps. The latter
needs an intermediate stage, so-called raw symbols, which are possibly
unqualified symbols. Normal symbols are always fully qualified.
In the CASL reference manual, our symbols are called "signature symbols",
and our raw symbols are called "symbols". (Terminology should be adapted.)
class ( Syntax lid basic_spec symb_items symb_map_items
, Sentences lid sentence sign morphism symbol
, GetRange raw_symbol, Ord raw_symbol, Pretty raw_symbol
basic_spec sentence symb_items symb_map_items
sign morphism symbol raw_symbol
| lid -> basic_spec sentence symb_items symb_map_items
sign morphism symbol raw_symbol
{- | static analysis of basic specifications and symbol maps.
The resulting bspec has analyzed axioms in it.
The resulting sign is an extension of the input sign
plus newly declared or redeclared symbols.
See CASL RefMan p. 138 ff. -}
-> Maybe ((basic_spec, sign, GlobalAnnos)
-> Result (basic_spec, ExtSign sign symbol, [Named sentence]))
basic_analysis _ = Nothing
-- | a basic analysis with additional arguments
extBasicAnalysis :: lid -> IRI -> LibId
-> basic_spec -> sign -> GlobalAnnos
-> Result (basic_spec, ExtSign sign symbol, [Named sentence])
extBasicAnalysis l _ _ b s g = case basic_analysis l of
Nothing -> statFail l "basic_analysis"
-- | static analysis of symbol maps, see CASL RefMan p. 222f.
stat_symb_map_items :: lid -> sign -> Maybe sign -> [symb_map_items]
-> Result (EndoMap raw_symbol)
stat_symb_map_items l _ _ _ = statFail l "stat_symb_map_items"
-- | static analysis of symbol lists, see CASL RefMan p. 221f.
stat_symb_items :: lid -> sign -> [symb_items] -> Result [raw_symbol]
stat_symb_items l _ _ = statFail l "stat_symb_items"
-- | convert a theory to basic specs for different serializations
convertTheory :: lid -> Maybe ((sign, [Named sentence]) -> basic_spec)
convertTheory _ = Nothing
{- ----------------------- amalgamation ---------------------------
Computation of colimits of signature diagram.
Indeed, it suffices to compute a cocone that is weakly amalgamable
Heterogeneous specification and the heterogeneous tool set
-- | architectural sharing analysis, see CASL RefMan p. 247ff.
ensures_amalgamability :: lid ->
([CASLAmalgOpt], -- the program options
Gr sign (Int, morphism), -- the diagram to be analyzed
[(Int, morphism)], -- the sink
Gr String String) -- the descriptions of nodes and edges
ensures_amalgamability l _ = warning Amalgamates
("amalgamability test not implemented for logic " ++ show l)
-- | quotient term algebra for normalization of freeness
quotient_term_algebra :: lid -- the logic
-> morphism -- sigma : Sigma -> SigmaM
-> [Named sentence] -- Th(M)
[Named sentence] -- Ax(K)
quotient_term_algebra l _ _ = statFail l "quotient_term_algebra"
signature_colimit :: lid -> Gr sign (Int, morphism)
-> Result (sign,
Map.Map Int morphism)
signature_colimit l _ = statFail l "signature_colimit"
{- | rename and qualify the symbols considering a united incoming
morphisms, code out overloading and
create sentences for the overloading relation -}
qualify :: lid -> SIMPLE_ID -> LibId -> morphism -> sign
-> Result (morphism, [Named sentence])
qualify l _ _ _ _ = statFail l "qualify"
-- ------------------ symbols and raw symbols ---------------------
{- | Construe a symbol, like f:->t, as a raw symbol.
This is a one-sided inverse to the function SymSySigSym
in the CASL RefMan p. 192. -}
symbol_to_raw :: lid -> symbol -> raw_symbol
symbol_to_raw l _ = statError l "symbol_to_raw"
{- | Construe an identifier, like f, as a raw symbol.
See CASL RefMan p. 192, function IDAsSym -}
id_to_raw :: lid -> Id -> raw_symbol
id_to_raw l _ = statError l "id_to_raw"
{- | Check wether a symbol matches a raw symbol, for
example, f:s->t matches f. See CASL RefMan p. 192 -}
matches :: lid -> symbol -> raw_symbol -> Bool
-- ------------- operations on signatures and morphisms -----------
-- | the empty (initial) signature, see CASL RefMan p. 193
empty_signature :: lid -> sign
-- | adds a symbol to a given signature
add_symb_to_sign :: lid -> sign -> symbol -> Result sign
add_symb_to_sign l _ _ = statFail l "add_symb_to_sign"
-- | union of signatures, see CASL RefMan p. 193
signature_union :: lid -> sign -> sign -> Result sign
signature_union l _ _ = statFail l "signature_union"
-- | difference of signatures resulting in unclosed pre-signatures
signatureDiff :: lid -> sign -> sign -> Result sign
signatureDiff l _ _ = statFail l "signatureDiff"
-- | intersection of signatures
intersection :: lid -> sign -> sign -> Result sign
intersection l _ _ = statFail l "intersection"
-- | final union of signatures, see CASL RefMan p. 194
final_union :: lid -> sign -> sign -> Result sign
final_union l _ _ = statFail l "final_union"
-- | union of signature morphims, see CASL RefMan p. 196
morphism_union :: lid -> morphism -> morphism -> Result morphism
morphism_union l _ _ = statFail l "morphism_union"
-- | subsignatures, see CASL RefMan p. 194
is_subsig :: lid -> sign -> sign -> Bool
{- | construct the inclusion morphisms between subsignatures,
see CASL RefMan p. 194 -}
subsig_inclusion :: lid -> sign -> sign -> Result morphism
subsig_inclusion l _ _ = statFail l "subsig_inclusion"
{- | the signature (co)generated by a set of symbols in another
signature is the smallest (largest) signature containing
(excluding) the set of symbols. Needed for revealing and
hiding, see CASL RefMan p. 197ff. -}
generated_sign, cogenerated_sign ::
lid ->
Set.Set symbol -> sign -> Result morphism
generated_sign l _ _ = statFail l "generated_sign"
cogenerated_sign l _ _ = statFail l "cogenerated_sign"
{- | Induce a signature morphism from a source signature and
a raw symbol map. Needed for translation (SP with SM).
See CASL RefMan p. 198 -}
lid -> EndoMap raw_symbol -> sign -> Result morphism
induced_from_morphism l _ _ = statFail l "induced_from_morphism"
{- | Induce a signature morphism between two signatures by a
raw symbol map. Needed for instantiation and views.
See CASL RefMan p. 198f. -}
induced_from_to_morphism ::
lid -> EndoMap raw_symbol -> ExtSign sign symbol
-> ExtSign sign symbol -> Result morphism
induced_from_to_morphism l rm (ExtSign sig _) (ExtSign tar _) = do
mor <- induced_from_morphism l rm sig
inclusion l (cod mor) tar >>= composeMorphisms mor
{- | Check whether a signature morphism is transportable.
See CASL RefMan p. 304f. -}
is_transportable :: lid -> morphism -> Bool
is_transportable _ _ = False
{- | Check whether the underlying symbol map of a signature morphism
is_injective :: lid -> morphism -> Bool
-- | generate an ontological taxonomy, if this makes sense
theory_to_taxonomy :: lid
-> sign -> [Named sentence]
theory_to_taxonomy l _ _ _ _ = statFail l "theory_to_taxonomy"
-- | print a whole theory
printTheory :: StaticAnalysis lid basic_spec sentence symb_items symb_map_items
sign morphism symbol raw_symbol
=> Maybe IRI -> lid -> (sign, [Named sentence]) -> Doc
printTheory sm lid th@(s, l) = case
(convertTheory lid, basicSpecPrinter sm lid) of
(Just c, Just p) -> p (c th)
_ -> print_sign lid s $++$ vsep (map (print_named lid) l)
inclusion :: StaticAnalysis lid basic_spec sentence symb_items symb_map_items
sign morphism symbol raw_symbol
=> lid -> sign -> sign -> Result morphism
inclusion l s1 s2 = if is_subsig l s1 s2 then subsig_inclusion l s1 s2
, text "symbol(s) missing in target:"
{- | semi lattices with top (needed for sublogics). Note that `Ord` is
only used for efficiency and is not related to the /partial/ order given
by the lattice. Only `Eq` is used to define `isSubElem` -}
class (Ord l, Show l) => SemiLatticeWithTop l where
instance SemiLatticeWithTop () where
-- | less or equal for semi lattices
isSubElem :: SemiLatticeWithTop l => l -> l -> Bool
isSubElem a b = join a b == b
-- | class providing the minimal sublogic of an item
class MinSublogic sublogic item where
minSublogic :: item -> sublogic
-- | a default instance for no sublogics
instance MinSublogic () a where
-- | class providing also the projection of an item to a sublogic
class MinSublogic sublogic item => ProjectSublogic sublogic item where
projectSublogic :: sublogic -> item -> item
-- | a default instance for no sublogics
instance ProjectSublogic () b where
-- | like ProjectSublogic, but providing a partial projection
class MinSublogic sublogic item => ProjectSublogicM sublogic item where
projectSublogicM :: sublogic -> item -> Maybe item
-- | a default instance for no sublogics
instance ProjectSublogicM () b where
projectSublogicM _ = Just
-- | a class for providing a sublogi name
class SublogicName l where
sublogicName :: l -> String
instance SublogicName () where
-- | a type for syntax information eventually stored in the signature
type SyntaxTable = (PrecMap, AssocMap)
{- Type class logic. The central type class of Hets, providing the
interface for logics. This type class is instantiated for many logics,
and it is used for the logic independent parts of Hets.
It hence provides an abstraction barrier between logic specific and
This type class extends the class StaticAnalysis by a sublogic mechanism.
Sublogics are important since they avoid the need to provide an own
instance of the class logic for each sublogic. Instead, the sublogic
can use the datastructures and operations of the main logic, and
functions are provided to test whether a given item lies within the
sublogic. Also, projection functions from a super-logic to a sublogic
class (StaticAnalysis lid
basic_spec sentence symb_items symb_map_items
sign morphism symbol raw_symbol,
SemiLatticeWithTop sublogics,
MinSublogic sublogics sentence,
ProjectSublogic sublogics basic_spec,
ProjectSublogicM sublogics symb_items,
ProjectSublogicM sublogics symb_map_items,
ProjectSublogic sublogics sign,
ProjectSublogic sublogics morphism,
ProjectSublogicM sublogics symbol,
Ord proof_tree, Show proof_tree,
basic_spec sentence symb_items symb_map_items
sign morphism symbol raw_symbol proof_tree
basic_spec sentence symb_items symb_map_items
sign morphism symbol raw_symbol proof_tree
-- | stability of the implementation
stability :: lid -> Stability
stability _ = Experimental
-- | for a process logic, return its data logic
data_logic :: lid -> Maybe AnyLogic
-- | the top sublogic, corresponding to the whole logic
top_sublogic :: lid -> sublogics
-- | list all the sublogics of the current logic
all_sublogics :: lid -> [sublogics]
all_sublogics li = [top_sublogic li]
{- a bottom sublogic can be extended along several dimensions
joining all last elements of a dimension should yield the top-sublogic
bottomSublogic :: lid -> Maybe sublogics
bottomSublogic _ = Nothing
sublogicDimensions :: lid -> [[sublogics]]
sublogicDimensions li = [all_sublogics li]
-- | parse sublogic (override more efficiently)
parseSublogic :: lid -> String -> Maybe sublogics
parseSublogic li s = lookup s $ map (\ l -> (sublogicName l, l))
{- | provide the embedding of a projected signature into the
proj_sublogic_epsilon :: lid -> sublogics -> sign -> morphism
proj_sublogic_epsilon _ _ = ide
-- --------------------- provers ---------------------------
-- | several provers can be provided. See module "
Logic.Prover"
provers :: lid -> [Prover sign sentence morphism sublogics proof_tree]
-- | consistency checkers
-> [ConsChecker sign sentence
sublogics morphism proof_tree]
-- | conservativity checkers
conservativityCheck :: lid
-> [ConservativityChecker sign sentence morphism]
conservativityCheck _ = []
-- | the empty proof tree
empty_proof_tree :: lid -> proof_tree
empty_proof_tree l = statError l "empty_proof_tree"
-- --------------------- OMDoc ---------------------------
syntaxTable :: lid -> sign -> Maybe SyntaxTable
syntaxTable _ _ = Nothing
{- default implementation, no logic should throw an error here
and the base of omcd should be a parseable URI -}
omdoc_metatheory _ = Nothing
export_symToOmdoc l _ _ = statFail l "export_symToOmdoc"
export_senToOmdoc l _ _ = statFail l "export_senToOmdoc"
{- | additional information which has to be exported can be
exported by this function -}
{- default implementation does no extra export
, sufficient in some cases -}
export_theoryToOmdoc _ _ _ _ = return []
-> String -> Result symbol
omdocToSym l _ _ _ = statFail l "omdocToSym"
-> String -> Result (Maybe (Named sentence))
omdocToSen l _ _ _ = statFail l "omdocToSen"
{- | Algebraic Data Types are imported with this function.
By default the input is returned without changes. -}
-> Result (sign, [Named sentence])
-- no logic should throw an error here
addOMadtToTheory l _ t adts = do
unless (null adts) $ warning ()
(concat [ "ADT handling not implemented for logic "
, show l, " but some adts have to be handled" ])
{- | additional information which has to be imported can be
imported by this function. By default the input is returned
-> Result (sign, [Named sentence])
-- no logic should throw an error here
addOmdocToTheory _ _ t _ = return t
{- The class of logics which can be used as logical frameworks, in which object
logics can be specified by the user. Currently the only logics implementing
this class are LF, Maude, and Isabelle, with the latter two only having
The function "base_sig" returns the base signature of the framework -
for details see Integrating Logical Frameworks in Hets by M. Codescu et al
The function "write_logic" constructs the contents of the Logic_L
file, where L is the name of the object logic passed as an argument.
Typically, this file will declare the lid of the object logic L and
instances of the classes Language, Syntax, Sentences, Logic, and
StaticAnalysis. The instance of Category is usually inherited from
the framework itself as the object logic reuses the signatures and
morphisms of the framework.
The function "write_syntax" constructs the contents of the file declaring
the Ltruth morphism (see the reference given above). If proofs and models
are later integrated into Hets, there should be analogous functions
"write_proofs" and "write_models" added, declaring the Lpf and
Lmod morphisms respectively. -}
class Logic lid sublogics basic_spec sentence
symb_items symb_map_items sign
morphism symbol raw_symbol proof_tree
=> LogicFram lid sublogics basic_spec sentence
symb_items symb_map_items sign
morphism symbol raw_symbol proof_tree
| lid -> sublogics basic_spec sentence symb_items symb_map_items
sign morphism symbol raw_symbol proof_tree
base_sig l = error $ "Function base_sig nyi for logic " ++ shows l "."
{- | generation of the object logic instances
second argument is object logic name -}
write_logic :: lid -> String -> String
$ "Function write_logic nyi for logic " ++ shows l "."
{- | generation of the Ltruth morphism declaration
second argument is the object logic name
third argument is the Ltruth morphism -}
write_syntax :: lid -> String -> morphism -> String
"Function write_syntax nyi for logic " ++ shows l "."
write_proof :: lid -> String -> morphism -> String
"Function write_proof nyi for logic " ++ shows l "."
write_model :: lid -> String -> morphism -> String
"Function write_model nyi for logic " ++ shows l "."
read_morphism :: lid -> FilePath -> morphism
read_morphism l _ = error $
"Function read_morphism nyi for logic " ++ shows l "."
write_comorphism :: lid -> String -> String -> String
-> morphism -> morphism -> morphism
write_comorphism l = error $
"Function write_comorphism nyi for logic " ++ shows l "."
{- --------------------------------------------------------------
-------------------------------------------------------------- -}
emptyTheory :: StaticAnalysis lid
basic_spec sentence symb_items symb_map_items
sign morphism symbol raw_symbol =>
lid -> Theory sign sentence proof_tree
emptyTheory lid = Theory (empty_signature lid)
Map.empty{- --------------------------------------------------------------
Existential type covering any logic
-------------------------------------------------------------- -}
-- | the disjoint union of all logics
data AnyLogic = forall lid sublogics
basic_spec sentence symb_items symb_map_items
sign morphism symbol raw_symbol proof_tree .
basic_spec sentence symb_items symb_map_items
sign morphism symbol raw_symbol proof_tree =>
instance GetRange AnyLogic
instance Show AnyLogic where
show (Logic lid) = language_name lid
instance Eq AnyLogic where
a == b = compare a b == EQ
instance Ord AnyLogic where
StaticAnalysis (no sublogics)