1ac35b084d7e57853f66169d2ca5532977fc403aJens Elkner-- needs ghc -fglasgow-exts

1ac35b084d7e57853f66169d2ca5532977fc403aJens Elkner

1ac35b084d7e57853f66169d2ca5532977fc403aJens Elkner{- HetCATS/LogicGraph.hs

e048ebd09f239ef0cac9f73d361cac09bed4c5e2Christian Maeder $Id$

4f747850e4f251b38ae9e8af25f40a3018368ceaChristian Maeder Till Mossakowski

e048ebd09f239ef0cac9f73d361cac09bed4c5e2Christian Maeder

e08effb60f632f903bf781107fd6df9ed59d824bChristian Maeder Assembles all the logics and representations into a graph

4f747850e4f251b38ae9e8af25f40a3018368ceaChristian Maeder (represented as lists of nodes and edges, using existential

e08effb60f632f903bf781107fd6df9ed59d824bChristian Maeder types).

834a709f214cdafa3b46dabddd9e072d3f030c4dChristian Maeder The logic graph will be the basis for the Grothendieck logic.

1ac35b084d7e57853f66169d2ca5532977fc403aJens Elkner

834a709f214cdafa3b46dabddd9e072d3f030c4dChristian Maeder References:

ab47f17102a0d0e6aa2cb937dfea1d7ec36c74cdChristian Maeder

834a709f214cdafa3b46dabddd9e072d3f030c4dChristian Maeder T. Mossakowski:

834a709f214cdafa3b46dabddd9e072d3f030c4dChristian Maeder Relating CASL with Other Specification Languages:

4f747850e4f251b38ae9e8af25f40a3018368ceaChristian Maeder the Institution Level

834a709f214cdafa3b46dabddd9e072d3f030c4dChristian Maeder Theoretical Computer Science, July 2003

e048ebd09f239ef0cac9f73d361cac09bed4c5e2Christian Maeder

834a709f214cdafa3b46dabddd9e072d3f030c4dChristian Maeder Todo:

Add many many logics.

-}

module LogicGraph where

import Logic

-- Existential types for logics and representations

data AnyLogic = forall id

basic_spec sentence symb_items symb_map_items anno

local_env sign morphism symbol raw_symbol .

Logic id

basic_spec sentence symb_items symb_map_items anno

local_env sign morphism symbol raw_symbol =>

Ins id

data AnyRepresentation = forall id1

basic_spec1 sentence1 symb_items1 symb_map_items1 anno1

local_env1 sign1 morphism1 symbol1 raw_symbol1

id2

basic_spec2 sentence2 symb_items2 symb_map_items2 anno2

local_env2 sign2 morphism2 symbol2 raw_symbol2 .

(Logic id1

basic_spec1 sentence1 symb_items1 symb_map_items1 anno1

local_env1 sign1 morphism1 symbol1 raw_symbol1,

Logic id2

basic_spec2 sentence2 symb_items2 symb_map_items2 anno2

local_env2 sign2 morphism2 symbol2 raw_symbol2) =>

Repr(LogicRepr id1 basic_spec1 sentence1 symb_items1 symb_map_items1 anno1

local_env1 sign1 morphism1 symbol1 raw_symbol1

id2 basic_spec2 sentence2 symb_items2 symb_map_items2 anno2

local_env2 sign2 morphism2 symbol2 raw_symbol2)

{- Composition of representations

data Translation = forall id1 as1 id2 as2 . (Language id1 as1, Language id2 as2) => T id1 (as1->as2) id2

idtrans i = T i id i

comp_repr :: AnyRepresentation -> AnyRepresentation -> Maybe AnyRepresentation

comp_repr (

T i_src1 (t1::as_src1->as_tar1) i_tar1) (T i_src2 (t2::as_src2->as_tar2) i_tar2) =

case ((Dynamic.fromDynamic (Dynamic.toDyn t2))::Maybe (as_tar1->as_tar2)) of

Just t -> Just (T i_src1 (t . t1) i_tar2)

Nothing -> Nothing

-}

the_logic_list :: [AnyLogic] = []

the_representation_list :: [AnyRepresentation] = []