xref/hets/Logic.hs

	Logic.hs revision 9b94043f6a8b10ddf748119a0e34002dd5e592c3
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski-- needs ghc -fglasgow-exts
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski{- HetCATS/Logic.hs
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski   $Id$
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski   Till Mossakowski
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski   Provides data structures for logics (with symbols)
601dc92e4c128d23a726593357c654fb776a63a7Till Mossakowski   and logic representations. Logics are
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski   a type class with an "identitiy" type (usually interpreted
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski   by a singleton set) which serves to treat logics as
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski   data. All the functions in the type class take the
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski   identity as first argument in order to determine the logic.
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski   Logic representations are just collections of
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski   functions between (some of) the types of logics.
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski   References:
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski   J. A. Goguen and R. M. Burstall
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski   Institutions: Abstract Model Theory for Specification and
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski     Programming
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski   JACM 39, p. 95--146, 1992
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski   (general notion of logic - model theory only)
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski   J. Meseguer
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski   General Logics
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski   Logic Colloquium 87, p. 275--329, North Holland, 1989
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski   (general notion of logic - also proof theory;
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski    notion of logic representation, called map there)
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski   T. Mossakowski:
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski   Specification in an arbitrary institution with symbols
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski   14th WADT 1999, LNCS 1827, p. 252--270
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski   (treatment of symbols and raw symbols, see also CASL semantics)
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski   T. Mossakowski, B. Klin:
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski   Institution Independent Static Analysis for CASL
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski   15h WADT 2001, LNCS 2267, p. 221-237, 2002.
da955132262baab309a50fdffe228c9efe68251dCui Jian   (what is needed for static anaylsis)
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski   S. Autexier and T. Mossakowski
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski   Integrating HOLCASL into the Development Graph Manager MAYA
da955132262baab309a50fdffe228c9efe68251dCui Jian   FroCoS 2002, to appear
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski   (interface to provers)
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski   Todo:
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski   ATerm, XML
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski   Weak amalgamability, also for reprs
da955132262baab309a50fdffe228c9efe68251dCui Jian   Metavars
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski   repr maps
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski   reprs out of sublogic relationships
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski-}
da955132262baab309a50fdffe228c9efe68251dCui Jian
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowskimodule Logic where
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowskiimport Id
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowskiimport AS_Annotation
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowskiimport Error
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowskiimport Dynamic
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski-- maps and sets, just a quick thing
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowskitype Set a = [a]
da955132262baab309a50fdffe228c9efe68251dCui Jiantype Map a = [(a,a)]
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski-- diagrams, nodes are just integers
da955132262baab309a50fdffe228c9efe68251dCui Jian
da955132262baab309a50fdffe228c9efe68251dCui Jiantype Node = Int
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowskitype Edge morphism = (Node,morphism,Node)
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowskidata Diagram object morphism = Diagram [(Node,object)] [Edge morphism]
da955132262baab309a50fdffe228c9efe68251dCui Jianempty_diagram :: Diagram o m
da955132262baab309a50fdffe228c9efe68251dCui Jianempty_diagram = Diagram [] []
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowskiadd_node :: Diagram o m -> o -> (Node,Diagram o m)
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowskiadd_node (Diagram nodes edges) obj =
da955132262baab309a50fdffe228c9efe68251dCui Jian         (node,Diagram ((node,obj):nodes) edges) where
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski            node = maximum (map fst nodes)
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowskiadd_edge :: Diagram o m -> Edge m -> Diagram o m
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowskiadd_edge (Diagram nodes edges) edge =
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski         Diagram nodes (edge:edges)
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowskiobject_at_node :: Node -> Diagram o m -> Maybe (Node,o)
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowskiobject_at_node node (Diagram nodes edges) =
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski         case lookup node nodes of
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski           Just obj -> Just (node,obj)
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski           Nothing -> Nothing
da955132262baab309a50fdffe228c9efe68251dCui Jiandiagram_nodes :: Diagram o m  -> [(Node,o)]
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowskidiagram_nodes (Diagram nodes edges) = nodes
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowskidiagram_edges :: Diagram o m -> [Edge m]
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowskidiagram_edges (Diagram nodes edges) = edges
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski-- Categories are given by a quotient,
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski-- i.e. we need equality
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski-- Should we allow arbitrary composition graphs and build paths?
da955132262baab309a50fdffe228c9efe68251dCui Jian
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowskiclass (Eq object, Eq morphism) =>
da955132262baab309a50fdffe228c9efe68251dCui Jian      Category id object morphism | id ->, id -> morphism where
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski         ide :: id -> object -> morphism
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski         o :: id -> morphism -> morphism -> Maybe morphism
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski         dom, cod :: id -> morphism -> object
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski         legal_obj :: id -> object -> Bool
         legal_mor :: id -> morphism -> Bool


-- abstract syntax, parsing and printing

class (Show basic_spec, Eq basic_spec, Show sentence, Show symb_items,
       Show symb_map_items, Eq symb_items, Eq symb_map_items) =>
      Syntax basic_spec sentence symb_items symb_map_items
      where
         -- parsing
         parse_basic_spec :: id -> String -> Result basic_spec
         parse_sentence :: id -> String -> Result sentence
         parse_symb_items :: id -> String -> Result [symb_items]
         parse_symb_map_items :: id -> String -> Result [symb_map_items]
         comment_line :: id -> String
         comment_group :: id -> (String,String)


-- lattices (for sublogics)

class Ord l => LatticeWithTop l where
  meet, join :: l -> l -> l
  top :: l


-- theories and theory morphisms

data Theory sign sen =
     Theory {sign_of :: sign,
             ax_of :: [(String,sen)]
            }

data TheoryMorphism sign sen mor =
     TheoryMorphism {t_source, t_target :: Theory sign sen,
                     t_morphism :: mor
                    }


-- proofs and provers

type Rule = String

data Proof_tree sen = Axiom sen
                    | Branch (sen,Rule,[Proof_tree sen])  -- add substitutions here?

type Tactic_script = String  -- the file name

data Proof_status sen = Open sen
                      | Disproved sen
                      | Proved(sen,
                               [sen], -- used axioms
                               Proof_tree sen,
                               Tactic_script)

data Prover sen symbol =
     Prover { prover_name :: String,
              prover_sublogic :: String,
              add_sym :: symbol -> IO(Bool),  -- returns True if succeeded
              remove_sym :: symbol -> IO(Bool), -- returns True if succeeded
              add_sen :: sen -> IO(Bool),  -- returns True if succeeded
              remove_sen :: sen -> IO(Bool), -- returns True if succeeded
              prove :: sen -> IO([Proof_status sen]) -- proof status for goal and lemmas
            }

data Cons_checker morphism =
     Cons_checker {cons_checker_name :: String,
                   cons_checker_sublogic :: String,
                   cons_check :: morphism -> IO(Bool, Tactic_script)
                  }


-- logics

class (Syntax basic_spec sentence symb_items symb_map_items,
       Show sign, Show morphism, Show symbol, Show raw_symbol,
       Ord symbol, --  needed for efficient symbol tables
       Eq raw_symbol,
       Category id sign morphism,
       LatticeWithTop sublogics,
       -- needed for heterogeneous coercions:
       Typeable id, Typeable sublogics, Typeable sign, Typeable morphism, Typeable symbol, Typeable raw_symbol,
       Typeable basic_spec, Typeable sentence, Typeable symb_items, Typeable symb_map_items) =>
      Logic id sublogics
        basic_spec sentence symb_items symb_map_items
        local_env sign morphism symbol raw_symbol
        | id -> sublogics, id -> basic_spec, id -> sentence, id -> symb_items,
          id -> symb_map_items, id -> local_env,
          id -> sign, id -> morphism, id ->symbol, id -> raw_symbol
       where
         logic_name :: id -> String
         has_parser :: id -> Bool
         has_printer :: id -> Bool
         has_analysis :: id -> Bool

         -- sentence translation
         map_sen :: id -> morphism -> sentence -> Result sentence

         -- static analysis of basic specifications and symbol maps
         basic_analysis :: id ->
                           (basic_spec,  -- abstract syntax tree
                            local_env,   -- efficient table for env signature
                            [Annotation]) ->   -- global annotations
                           Result (sign,[(String,sentence)])
                                   -- these include any new annotations
         stat_symb_map_items :: id -> [symb_map_items] -> Result (Map raw_symbol)
         stat_symb_items :: id -> [symb_items] -> Result [raw_symbol]

         -- architectural sharing analysis for one morphism
         ensures_amalgamability :: id ->
              (Diagram sign morphism, Node, sign, Edge morphism, morphism) ->
               Result (Diagram sign morphism)
         -- do we need it also for sinks consisting of two morphisms?

         -- symbols and symbol maps
         symbol_to_raw :: id -> symbol -> raw_symbol
         id_to_raw :: id -> Id -> raw_symbol
         sym_of :: id -> sign -> Set symbol
         symmap_of :: id -> morphism -> Map symbol
         matches :: id -> symbol -> raw_symbol -> Bool
         sym_name :: id -> symbol -> Id

         -- operations on local envs, signatures and morphisms
         empty_local_env :: local_env
         add_sign :: sign -> local_env -> local_env
         empty_signature :: id -> sign
         signature_union :: id -> sign -> sign -> Result sign
         final_union :: id -> sign -> sign -> Result sign
         is_subsig :: id -> sign -> sign -> Bool
         generated_sign, cogenerated_sign :: id -> [raw_symbol] -> sign -> Result morphism
         induced_from_morphism :: id -> Map raw_symbol -> sign -> Result morphism
         induced_from_to_morphism :: id -> Map raw_symbol -> sign -> sign -> Result morphism
         extend_morphism :: Id -> sign -> morphism -> sign -> sign -> Result morphism

         -- sublogics
         sublogic_names :: id -> sublogics -> [String]
             -- the first name is the principal name
         all_sublogics :: id -> [sublogics]

         is_in_basic_spec :: id -> sublogics -> basic_spec -> Bool
         is_in_sentence :: id -> sublogics -> sentence -> Bool
         is_in_symb_items :: id -> sublogics -> symb_items -> Bool
         is_in_symb_map_items :: id -> sublogics -> symb_map_items -> Bool
         is_in_sign :: id -> sublogics -> sign -> Bool
         is_in_morphism :: id -> sublogics -> morphism -> Bool
         is_in_symbol :: id -> sublogics -> symbol -> Bool

         min_sublogic_basic_spec :: id -> basic_spec -> sublogics
         min_sublogic_sentence :: id -> sentence -> sublogics
         min_sublogic_symb_items :: id -> symb_items -> sublogics
         min_sublogic_symb_map_items :: id -> symb_map_items -> sublogics
         min_sublogic_sign :: id -> sign -> sublogics
         min_sublogic_morphism :: id -> morphism -> sublogics
         min_sublogic_symbol :: id -> symbol -> sublogics

         proj_sublogic_basic_spec :: id -> sublogics -> basic_spec -> basic_spec
         proj_sublogic_symb_items :: id -> sublogics -> symb_items -> Maybe symb_items
         proj_sublogic_symb_map_items :: id -> sublogics -> symb_map_items -> Maybe symb_map_items
         proj_sublogic_sign :: id -> sublogics -> sign -> sign
         proj_sublogic_morphism :: id -> sublogics -> morphism -> morphism
         proj_sublogic_epsilon :: id -> sublogics -> sign -> morphism
         proj_sublogic_symbol :: id -> sublogics -> symbol -> Maybe symbol

         -- provers
         provers :: [Prover sentence symbol]
         cons_checkers :: [Cons_checker (TheoryMorphism sign sentence morphism)]

         -- derived operations, need not to be given

         -- printing, accessible via logic identity
         show_basic_spec :: id -> basic_spec -> String
         show_sentence :: id -> sentence -> String
         show_symb_items :: id -> symb_items -> String
         show_symb_items_list :: id -> [symb_items] -> String
         show_symb_map_items :: id -> symb_map_items -> String
         show_symb_map_items_list :: id -> [symb_map_items] -> String
         show_sign :: id -> sign -> String
         show_morphism :: id -> morphism -> String
         show_symbol :: id -> symbol -> String
         show_raw_symbol :: id -> raw_symbol -> String

         show_basic_spec _ = show
         show_sentence _ = show
         show_symb_items _ = show
         show_symb_items_list _ l = showList l ""
         show_symb_map_items _ = show
         show_symb_map_items_list _ l = showList l ""
         show_sign _ = show
         show_morphism _ = show
         show_symbol _ = show
         show_raw_symbol _ = show


-- Simple logic representations (possibly also morphisms via adjointness)

data (Logic id1 sublogics1
        basic_spec1 sentence1 symb_items1 symb_map_items1
        local_env1 sign1 morphism1 symbol1 raw_symbol1,
      Logic id2 sublogics2
        basic_spec2 sentence2 symb_items2 symb_map_items2
        local_env2 sign2 morphism2 symbol2 raw_symbol2) =>
  LogicRepr id1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
                local_env1 sign1 morphism1 symbol1 raw_symbol1
            id2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
                local_env2 sign2 morphism2 symbol2 raw_symbol2
     =
     LogicRepr {repr_name :: String,
                source :: id1, source_sublogic :: sublogics1,
                target :: id2, target_sublogic :: sublogics2,
                -- the translation functions are partial
                -- because the target may be a sublanguage
                -- map_basic_spec :: basic_spec1 -> Maybe basic_spec2,
                map_sign :: sign1 -> Maybe sign2,
                projection:: Maybe (sign2 -> sign1, morphism2 -> morphism1,
                                    sign2 -> morphism2,
                                    -- right adjoint and counit
                                    basic_spec2 -> basic_spec1,
                                    symbol2 -> Maybe symbol1),
                map_morphism :: morphism1 -> Maybe morphism2,
                map_sentence :: sign1 -> sentence1 -> Maybe sentence2,
                      -- also covers semi-representations
                      -- with no sentence translation
                map_symbol :: symbol1 -> Set symbol2
                  -- codings may be more complex
               }