Logic.hs revision 9b51fc5528c4d34260d97763fb59f427c3c7a63a
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor-- needs ghc -fglasgow-exts -fallow-overlapping-instances -package data
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor Till Mossakowski, Christian Maeder
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor Provides data structures for logics (with symbols). Logics are
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor a type class with an "identitiy" type (usually interpreted
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor by a singleton set) which serves to treat logics as
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor data. All the functions in the type class take the
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor identity as first argument in order to determine the logic.
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor For logic representations see LogicRepr.hs
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor References:
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor J. A. Goguen and R. M. Burstall
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor Institutions: Abstract Model Theory for Specification and
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor Programming
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor JACM 39, p. 95--146, 1992
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor (general notion of logic - model theory only)
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor J. Meseguer
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor General Logics
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor Logic Colloquium 87, p. 275--329, North Holland, 1989
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor (general notion of logic - also proof theory;
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor notion of logic representation, called map there)
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor T. Mossakowski:
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor Specification in an arbitrary institution with symbols
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor 14th WADT 1999, LNCS 1827, p. 252--270
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor (treatment of symbols and raw symbols, see also CASL semantics)
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor T. Mossakowski, B. Klin:
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor Institution Independent Static Analysis for CASL
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor 15h WADT 2001, LNCS 2267, p. 221-237, 2002.
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor (what is needed for static anaylsis)
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor S. Autexier and T. Mossakowski
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor Integrating HOLCASL into the Development Graph Manager MAYA
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor FroCoS 2002, to appear
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor (interface to provers)
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor Weak amalgamability
791057e5ead8cce851bbb30b06d552aef7e2c897gryzormodule Logic where
791057e5ead8cce851bbb30b06d552aef7e2c897gryzorimport GlobalAnnotations
791057e5ead8cce851bbb30b06d552aef7e2c897gryzorimport FiniteSet
791057e5ead8cce851bbb30b06d552aef7e2c897gryzorimport FiniteMap
791057e5ead8cce851bbb30b06d552aef7e2c897gryzorimport Graph
791057e5ead8cce851bbb30b06d552aef7e2c897gryzorimport Result
791057e5ead8cce851bbb30b06d552aef7e2c897gryzorimport Prover -- for one half of class Sentences
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor-- import IOExts(trace)
791057e5ead8cce851bbb30b06d552aef7e2c897gryzorimport PrettyPrint
791057e5ead8cce851bbb30b06d552aef7e2c897gryzorimport Dynamic
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor-- for coercion used in Grothendieck.hs and Analysis modules
791057e5ead8cce851bbb30b06d552aef7e2c897gryzorimport UnsafeCoerce
791057e5ead8cce851bbb30b06d552aef7e2c897gryzortype EndoMap a = FiniteMap a a
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor-- diagrams are just graphs
791057e5ead8cce851bbb30b06d552aef7e2c897gryzordata Diagram object morphism = Graph object morphism
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor-- languages, define like "data CASL = CASL deriving Show"
791057e5ead8cce851bbb30b06d552aef7e2c897gryzorclass Show lid => Language lid where
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor language_name :: lid -> String
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor language_name i = show i
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor-- (a bit unsafe) coercion using the language name
791057e5ead8cce851bbb30b06d552aef7e2c897gryzorcoerce :: (Typeable a, Typeable b, Language lid1, Language lid2, Show a) =>
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor lid1 -> lid2 -> a -> Maybe b
791057e5ead8cce851bbb30b06d552aef7e2c897gryzorcoerce i1 i2 a = if language_name i1 == language_name i2 then
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor --fromDynamic (toDyn (a)) else Nothing
d89089206f40f9a6d58528ff85050447d4a52d53lgentis (Just $ unsafeCoerce a) else Nothing
d89089206f40f9a6d58528ff85050447d4a52d53lgentisrcoerce1 :: (Typeable a, Typeable b, Language lid1, Language lid2, Show a) =>
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor lid1 -> lid2 -> Pos-> a -> b -> Result b
791057e5ead8cce851bbb30b06d552aef7e2c897gryzorrcoerce1 i1 i2 pos a b =
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor maybeToResult pos
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor (if language_name i1 == language_name i2 then
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor "Internal type error concerning types "++show (typeOf a)
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor ++" and "++show(typeOf b)
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor else "Logic "++ language_name i1 ++ " expected, but "
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor ++ language_name i2++" found")
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor (coerce i1 i2 a)
791057e5ead8cce851bbb30b06d552aef7e2c897gryzorrcoerce :: (Typeable a, Typeable b, Language lid1, Language lid2, Show a) =>
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor lid1 -> lid2 -> Pos-> a -> Result b
791057e5ead8cce851bbb30b06d552aef7e2c897gryzorrcoerce i1 i2 pos a = -- rcoerce1 i1 i2 pos a undefined
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor maybeToResult pos
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor (if language_name i1 == language_name i2 then
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor "Internal type error concerning type "++show (typeOf a)
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor else "Logic "++ language_name i1 ++ " expected, but "
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor ++ language_name i2++" found")
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor (coerce i1 i2 a)
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor-- Categories are given by a quotient,
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor-- i.e. we need equality
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor-- Should we allow arbitrary composition graphs and build paths?
791057e5ead8cce851bbb30b06d552aef7e2c897gryzorclass (Language lid, Eq sign, Show sign, Eq morphism, Show morphism) =>
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor Category lid sign morphism | lid -> sign, lid -> morphism where
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor ide :: lid -> sign -> morphism
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor comp :: lid -> morphism -> morphism -> Maybe morphism
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor -- diagrammatic order
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor dom, cod :: lid -> morphism -> sign
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor legal_obj :: lid -> sign -> Bool
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor legal_mor :: lid -> morphism -> Bool
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor-- abstract syntax, parsing and printing
791057e5ead8cce851bbb30b06d552aef7e2c897gryzortype ParseFun a = FilePath -> Int -> Int -> String -> (a,String,Int,Int)
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor -- args: filename, line, column, input text
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor -- result: value, remaining text, line, column
791057e5ead8cce851bbb30b06d552aef7e2c897gryzorclass (Language lid, PrettyPrint basic_spec, Eq basic_spec,
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor PrettyPrint symb_items, Eq symb_items,
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor PrettyPrint symb_map_items, Eq symb_map_items) =>
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor Syntax lid basic_spec symb_items symb_map_items
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor | lid -> basic_spec, lid -> symb_items,
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor lid -> symb_map_items
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor parse_basic_spec :: lid -> Maybe(ParseFun basic_spec)
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor parse_symb_items :: lid -> Maybe(ParseFun symb_items)
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor parse_symb_map_items :: lid -> Maybe(ParseFun symb_map_items)
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor-- sentences (plus prover stuff and "symbol" with "Ord" for efficient lookup)
791057e5ead8cce851bbb30b06d552aef7e2c897gryzorclass (Category lid sign morphism, Show sentence,
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor Ord symbol, Show symbol)
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor => Sentences lid sentence proof_tree sign morphism symbol
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor | lid -> sentence, lid -> sign, lid -> morphism,
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor lid -> symbol, lid -> proof_tree
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor -- sentence translation
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor map_sen :: lid -> morphism -> sentence -> Result sentence
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor -- parsing of sentences
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor parse_sentence :: lid -> sign -> String -> Result sentence
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor -- is a term parser needed as well?
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor provers :: lid -> [Prover sentence proof_tree symbol]
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor cons_checkers :: lid -> [Cons_checker
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor (TheoryMorphism sign sentence morphism)]
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor-- static analysis
791057e5ead8cce851bbb30b06d552aef7e2c897gryzorclass ( Syntax lid basic_spec symb_items symb_map_items
d89089206f40f9a6d58528ff85050447d4a52d53lgentis , Sentences lid sentence proof_tree sign morphism symbol
d89089206f40f9a6d58528ff85050447d4a52d53lgentis , Show raw_symbol, Eq raw_symbol)
d89089206f40f9a6d58528ff85050447d4a52d53lgentis => StaticAnalysis lid
d89089206f40f9a6d58528ff85050447d4a52d53lgentis basic_spec sentence proof_tree symb_items symb_map_items
d89089206f40f9a6d58528ff85050447d4a52d53lgentis sign morphism symbol raw_symbol
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor | lid -> basic_spec, lid -> sentence, lid -> symb_items,
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor lid -> symb_map_items, lid -> proof_tree,
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor lid -> sign, lid -> morphism, lid -> symbol, lid -> raw_symbol
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor -- static analysis of basic specifications and symbol maps
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor basic_analysis :: lid ->
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor Maybe((basic_spec, -- abstract syntax tree
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor sign, -- efficient table for env signature
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor GlobalAnnos) -> -- global annotations
d89089206f40f9a6d58528ff85050447d4a52d53lgentis Result (sign,sign,[(String,sentence)]))
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor -- the first output sign is the accumulated sign
d89089206f40f9a6d58528ff85050447d4a52d53lgentis -- the second output sign united with the input sing
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor -- should yield the first output sign
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor sign_to_basic_spec :: lid -> sign -> [(String,sentence)] -> basic_spec
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor stat_symb_map_items ::
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor lid -> [symb_map_items] -> Result (EndoMap raw_symbol)
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor stat_symb_items :: lid -> [symb_items] -> Result [raw_symbol]
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor -- architectural sharing analysis for one morphism
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor ensures_amalgamability :: lid ->
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor (Diagram sign morphism, Node, sign, LEdge morphism, morphism) ->
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor Result (Diagram sign morphism)
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor -- do we need it also for sinks consisting of two morphisms?
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor -- symbols and symbol maps
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor symbol_to_raw :: lid -> symbol -> raw_symbol
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor id_to_raw :: lid -> Id -> raw_symbol
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor sym_of :: lid -> sign -> Set symbol
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor symmap_of :: lid -> morphism -> EndoMap symbol
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor matches :: lid -> symbol -> raw_symbol -> Bool
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor sym_name :: lid -> symbol -> Id
d89089206f40f9a6d58528ff85050447d4a52d53lgentis -- operations on signatures and morphisms
d89089206f40f9a6d58528ff85050447d4a52d53lgentis add_sign :: lid -> sign -> sign -> sign
d89089206f40f9a6d58528ff85050447d4a52d53lgentis empty_signature :: lid -> sign
d89089206f40f9a6d58528ff85050447d4a52d53lgentis signature_union :: lid -> sign -> sign -> Result sign
d89089206f40f9a6d58528ff85050447d4a52d53lgentis morphism_union :: lid -> morphism -> morphism -> Result morphism
d89089206f40f9a6d58528ff85050447d4a52d53lgentis final_union :: lid -> sign -> sign -> Result sign
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor is_subsig :: lid -> sign -> sign -> Bool
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor generated_sign, cogenerated_sign ::
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor lid -> [symbol] -> sign -> Result morphism
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor induced_from_morphism ::
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor lid -> EndoMap raw_symbol -> sign -> Result morphism
d89089206f40f9a6d58528ff85050447d4a52d53lgentis induced_from_to_morphism ::
d89089206f40f9a6d58528ff85050447d4a52d53lgentis lid -> EndoMap raw_symbol -> sign -> sign -> Result morphism
d89089206f40f9a6d58528ff85050447d4a52d53lgentis extend_morphism ::
d89089206f40f9a6d58528ff85050447d4a52d53lgentis lid -> sign -> morphism -> sign -> sign -> Result morphism
d89089206f40f9a6d58528ff85050447d4a52d53lgentis-- sublogics
791057e5ead8cce851bbb30b06d552aef7e2c897gryzorclass (Ord l, Show l) => LatticeWithTop l where
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor meet, join :: l -> l -> l
791057e5ead8cce851bbb30b06d552aef7e2c897gryzorclass (StaticAnalysis lid
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor basic_spec sentence proof_tree symb_items symb_map_items
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor sign morphism symbol raw_symbol,
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor LatticeWithTop sublogics,
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor Typeable sublogics, Typeable basic_spec, Typeable sentence,
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor Typeable symb_items, Typeable symb_map_items, Typeable sign,
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor Typeable morphism, Typeable symbol, Typeable raw_symbol,
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor Typeable proof_tree) =>
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor Logic lid sublogics
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor basic_spec sentence symb_items symb_map_items
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor sign morphism symbol raw_symbol proof_tree
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor | lid -> sublogics, lid -> basic_spec, lid -> sentence, lid -> symb_items,
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor lid -> symb_map_items, lid -> proof_tree,
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor lid -> sign, lid -> morphism, lid ->symbol, lid -> raw_symbol
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor sublogic_names :: lid -> sublogics -> [String]
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor -- the first name is the principal name
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor all_sublogics :: lid -> [sublogics]
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor is_in_basic_spec :: lid -> sublogics -> basic_spec -> Bool
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor is_in_sentence :: lid -> sublogics -> sentence -> Bool
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor is_in_symb_items :: lid -> sublogics -> symb_items -> Bool
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor is_in_symb_map_items :: lid -> sublogics -> symb_map_items -> Bool
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor is_in_sign :: lid -> sublogics -> sign -> Bool
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor is_in_morphism :: lid -> sublogics -> morphism -> Bool
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor is_in_symbol :: lid -> sublogics -> symbol -> Bool
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor min_sublogic_basic_spec :: lid -> basic_spec -> sublogics
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor min_sublogic_sentence :: lid -> sentence -> sublogics
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor min_sublogic_symb_items :: lid -> symb_items -> sublogics
82e1cfb4bff36447df8e3a7b8a1c13b7d26b8114igalic min_sublogic_symb_map_items :: lid -> symb_map_items -> sublogics
82e1cfb4bff36447df8e3a7b8a1c13b7d26b8114igalic min_sublogic_sign :: lid -> sign -> sublogics
82e1cfb4bff36447df8e3a7b8a1c13b7d26b8114igalic min_sublogic_morphism :: lid -> morphism -> sublogics
d89089206f40f9a6d58528ff85050447d4a52d53lgentis min_sublogic_symbol :: lid -> symbol -> sublogics
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor proj_sublogic_basic_spec :: lid -> sublogics -> basic_spec -> basic_spec
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor proj_sublogic_symb_items :: lid -> sublogics -> symb_items -> Maybe symb_items
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor proj_sublogic_symb_map_items :: lid -> sublogics -> symb_map_items -> Maybe symb_map_items
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor proj_sublogic_sign :: lid -> sublogics -> sign -> sign
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor proj_sublogic_morphism :: lid -> sublogics -> morphism -> morphism
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor proj_sublogic_epsilon :: lid -> sublogics -> sign -> morphism
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor proj_sublogic_symbol :: lid -> sublogics -> symbol -> Maybe symbol
791057e5ead8cce851bbb30b06d552aef7e2c897gryzorinstance Typeable a => Typeable (Set a) where
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor typeOf l = mkAppTy (mkTyCon "Set") []
791057e5ead8cce851bbb30b06d552aef7e2c897gryzorinstance (Typeable a,Typeable b) => Typeable (FiniteMap a b) where
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor typeOf l = mkAppTy (mkTyCon "FiniteMap") []
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor{- class hierarchy:
67972b58b9a56ebc101bea2e9758569b973dd5cand __________/
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor Sentences Syntax
791057e5ead8cce851bbb30b06d552aef7e2c897gryzor StaticAnalysis (no sublogics)