1N/A

1N/A-- needs ghc -fglasgow-exts -fallow-overlapping-instances -package data

1N/A

1N/A{- HetCATS/Logic.hs

1N/A $Id$

1N/A Till Mossakowski, Christian Maeder

1N/A

1N/A Provides data structures for logics (with symbols). Logics are

1N/A a type class with an "identitiy" type (usually interpreted

1N/A by a singleton set) which serves to treat logics as

1N/A data. All the functions in the type class take the

1N/A identity as first argument in order to determine the logic.

1N/A

1N/A For logic representations see LogicRepr.hs

1N/A

1N/A References:

1N/A

1N/A J. A. Goguen and R. M. Burstall

1N/A Institutions: Abstract Model Theory for Specification and

1N/A Programming

1N/A JACM 39, p. 95--146, 1992

1N/A (general notion of logic - model theory only)

1N/A

1N/A J. Meseguer

1N/A General Logics

1N/A Logic Colloquium 87, p. 275--329, North Holland, 1989

1N/A (general notion of logic - also proof theory;

1N/A notion of logic representation, called map there)

1N/A

1N/A T. Mossakowski:

1N/A Specification in an arbitrary institution with symbols

1N/A 14th WADT 1999, LNCS 1827, p. 252--270

1N/A (treatment of symbols and raw symbols, see also CASL semantics)

1N/A

1N/A T. Mossakowski, B. Klin:

1N/A Institution Independent Static Analysis for CASL

1N/A 15h WADT 2001, LNCS 2267, p. 221-237, 2002.

1N/A (what is needed for static anaylsis)

1N/A

1N/A S. Autexier and T. Mossakowski

1N/A Integrating HOLCASL into the Development Graph Manager MAYA

1N/A FroCoS 2002, to appear

1N/A (interface to provers)

1N/A

1N/A Todo:

1N/A ATerm, XML

1N/A Weak amalgamability

1N/A Metavars

1N/A

1N/A-}

1N/A

1N/Amodule Logic where

1N/A

1N/Aimport Id

1N/Aimport GlobalAnnotations

1N/Aimport FiniteSet

1N/Aimport FiniteMap

1N/Aimport Graph

1N/Aimport Result

1N/A--import Parsec

1N/Aimport Prover -- for one half of class Sentences

1N/A-- import IOExts(trace)

1N/Aimport PrettyPrint

1N/A

1N/A-- for coercion used in Grothendieck.hs and Analysis modules

1N/A

1N/Aimport UnsafeCoerce

1N/A

1N/A-- maps

1N/A

1N/Atype EndoMap a = FiniteMap a a

1N/A

1N/A-- diagrams are just graphs

1N/A

1N/Adata Diagram object morphism = Graph object morphism

1N/A

1N/A-- languages, define like "data CASL = CASL deriving Show"

1N/A

1N/Aclass Show lid => Language lid where

1N/A language_name :: lid -> String

1N/A language_name i = show i

1N/A

1N/A-- (a bit unsafe) coercion using the language name

1N/Acoerce :: (Language lid1, Language lid2, Show a) => lid1 -> lid2 -> a -> Maybe b

1N/Acoerce i1 i2 a = if language_name i1 == language_name i2 then

1N/A (Just $ unsafeCoerce a) else Nothing

1N/A

1N/Arcoerce :: (Language lid1, Language lid2, Show a) => lid1 -> lid2 -> Pos-> a -> Result b

1N/Arcoerce i1 i2 pos a =

1N/A maybeToResult pos

1N/A ("Logic "++ language_name i1 ++ " expected, but "

1N/A ++ language_name i2++" found")

1N/A (coerce i1 i2 a)

1N/A

1N/A-- Categories are given by a quotient,

1N/A-- i.e. we need equality

1N/A-- Should we allow arbitrary composition graphs and build paths?

1N/A

1N/Aclass (Language lid, Eq sign, Show sign, Eq morphism, Show morphism) =>

1N/A Category lid sign morphism | lid -> sign, lid -> morphism where

1N/A ide :: lid -> sign -> morphism

1N/A comp :: lid -> morphism -> morphism -> Maybe morphism

1N/A -- diagrammatic order

1N/A dom, cod :: lid -> morphism -> sign

1N/A legal_obj :: lid -> sign -> Bool

1N/A legal_mor :: lid -> morphism -> Bool

1N/A

1N/A-- abstract syntax, parsing and printing

1N/A

1N/Atype ParseFun a = FilePath -> Int -> Int -> String -> (a,String,Int,Int)

1N/A -- args: filename, line, column, input text

1N/A -- result: value, remaining text, line, column

1N/A

1N/Aclass (Language lid, PrettyPrint basic_spec, Eq basic_spec,

1N/A PrettyPrint symb_items, Eq symb_items,

1N/A PrettyPrint symb_map_items, Eq symb_map_items) =>

1N/A Syntax lid basic_spec symb_items symb_map_items

1N/A | lid -> basic_spec, lid -> symb_items,

1N/A lid -> symb_map_items

1N/A where

1N/A -- parsing

1N/A parse_basic_spec :: lid -> Maybe(ParseFun basic_spec)

1N/A parse_symb_items :: lid -> Maybe(ParseFun symb_items)

1N/A parse_symb_map_items :: lid -> Maybe(ParseFun symb_map_items)

1N/A

1N/A-- sentences (plus prover stuff and "symbol" with "Ord" for efficient lookup)

1N/A

1N/Aclass (Category lid sign morphism, Show sentence,

Ord symbol, Show symbol)

=> Sentences lid sentence proof_tree sign morphism symbol

| lid -> sentence, lid -> sign, lid -> morphism,

lid -> symbol, lid -> proof_tree

where

-- sentence translation

map_sen :: lid -> morphism -> sentence -> Result sentence

-- parsing of sentences

parse_sentence :: lid -> sign -> String -> Result sentence

-- is a term parser needed as well?

provers :: lid -> [Prover sentence proof_tree symbol]

cons_checkers :: lid -> [Cons_checker

(TheoryMorphism sign sentence morphism)]

-- static analysis

class ( Syntax lid basic_spec symb_items symb_map_items

, Sentences lid sentence proof_tree sign morphism symbol

, Show raw_symbol, Eq raw_symbol)

=> StaticAnalysis lid

basic_spec sentence proof_tree symb_items symb_map_items

sign morphism symbol raw_symbol

| lid -> basic_spec, lid -> sentence, lid -> symb_items,

lid -> symb_map_items, lid -> proof_tree,

lid -> sign, lid -> morphism, lid -> symbol, lid -> raw_symbol

where

-- static analysis of basic specifications and symbol maps

basic_analysis :: lid ->

Maybe((basic_spec, -- abstract syntax tree

sign, -- efficient table for env signature

GlobalAnnos) -> -- global annotations

Result (sign,sign,[(String,sentence)]))

-- the first output sign is the accumulated sign

-- the second output sign united with the input sing

-- should yield the first output sign

sign_to_basic_spec :: lid -> sign -> [(String,sentence)] -> basic_spec

stat_symb_map_items ::

lid -> [symb_map_items] -> Result (EndoMap raw_symbol)

stat_symb_items :: lid -> [symb_items] -> Result [raw_symbol]

-- architectural sharing analysis for one morphism

ensures_amalgamability :: lid ->

(Diagram sign morphism, Node, sign, LEdge morphism, morphism) ->

Result (Diagram sign morphism)

-- do we need it also for sinks consisting of two morphisms?

-- symbols and symbol maps

symbol_to_raw :: lid -> symbol -> raw_symbol

id_to_raw :: lid -> Id -> raw_symbol

sym_of :: lid -> sign -> Set symbol

symmap_of :: lid -> morphism -> EndoMap symbol

matches :: lid -> symbol -> raw_symbol -> Bool

sym_name :: lid -> symbol -> Id

-- operations on signatures and morphisms

add_sign :: lid -> sign -> sign -> sign

empty_signature :: lid -> sign

signature_union :: lid -> sign -> sign -> Result sign

morphism_union :: lid -> morphism -> morphism -> Result morphism

final_union :: lid -> sign -> sign -> Result sign

is_subsig :: lid -> sign -> sign -> Bool

generated_sign, cogenerated_sign ::

lid -> [symbol] -> sign -> Result morphism

induced_from_morphism ::

lid -> EndoMap raw_symbol -> sign -> Result morphism

induced_from_to_morphism ::

lid -> EndoMap raw_symbol -> sign -> sign -> Result morphism

extend_morphism ::

lid -> sign -> morphism -> sign -> sign -> Result morphism

-- sublogics

class (Ord l, Show l) => LatticeWithTop l where

meet, join :: l -> l -> l

top :: l

-- logics

class (StaticAnalysis lid

basic_spec sentence proof_tree symb_items symb_map_items

sign morphism symbol raw_symbol,

LatticeWithTop sublogics) =>

Logic lid sublogics

basic_spec sentence symb_items symb_map_items

sign morphism symbol raw_symbol proof_tree

| lid -> sublogics, lid -> basic_spec, lid -> sentence, lid -> symb_items,

lid -> symb_map_items, lid -> proof_tree,

lid -> sign, lid -> morphism, lid ->symbol, lid -> raw_symbol

where

sublogic_names :: lid -> sublogics -> [String]

-- the first name is the principal name

all_sublogics :: lid -> [sublogics]

is_in_basic_spec :: lid -> sublogics -> basic_spec -> Bool

is_in_sentence :: lid -> sublogics -> sentence -> Bool

is_in_symb_items :: lid -> sublogics -> symb_items -> Bool

is_in_symb_map_items :: lid -> sublogics -> symb_map_items -> Bool

is_in_sign :: lid -> sublogics -> sign -> Bool

is_in_morphism :: lid -> sublogics -> morphism -> Bool

is_in_symbol :: lid -> sublogics -> symbol -> Bool

min_sublogic_basic_spec :: lid -> basic_spec -> sublogics

min_sublogic_sentence :: lid -> sentence -> sublogics

min_sublogic_symb_items :: lid -> symb_items -> sublogics

min_sublogic_symb_map_items :: lid -> symb_map_items -> sublogics

min_sublogic_sign :: lid -> sign -> sublogics

min_sublogic_morphism :: lid -> morphism -> sublogics

min_sublogic_symbol :: lid -> symbol -> sublogics

proj_sublogic_basic_spec :: lid -> sublogics -> basic_spec -> basic_spec

proj_sublogic_symb_items :: lid -> sublogics -> symb_items -> Maybe symb_items

proj_sublogic_symb_map_items :: lid -> sublogics -> symb_map_items -> Maybe symb_map_items

proj_sublogic_sign :: lid -> sublogics -> sign -> sign

proj_sublogic_morphism :: lid -> sublogics -> morphism -> morphism

proj_sublogic_epsilon :: lid -> sublogics -> sign -> morphism

proj_sublogic_symbol :: lid -> sublogics -> symbol -> Maybe symbol

{- class hierarchy:

Language

__________/

Category

| /

Sentences Syntax

\ /

StaticAnalysis (no sublogics)

\

\

Logic

-}