LogicGraph.hs revision 815e723d788c6d8f6578e08039bd7e2e01fc10b4
568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder-- needs ghc -fglasgow-exts
568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder Till Mossakowski
568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder Assembles all the logics and representations into a graph
568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder (represented as lists of nodes and edges, using existential
568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder The logic graph will be the basis for the Grothendieck logic.
568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder T. Mossakowski:
568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder Relating CASL with Other Specification Languages:
1d330b771706686190ad2f3711ec5769c555c708Christian Maeder the Institution Level
568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder Theoretical Computer Science, July 2003
568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder Add many many logics.
568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maedermodule LogicGraph where
568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maederimport Dynamic
1d330b771706686190ad2f3711ec5769c555c708Christian Maeder-- Existential types for logics and representations
568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maederdata AnyLogic = forall id sublogics
568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder basic_spec sentence symb_items symb_map_items
568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder local_env sign morphism symbol raw_symbol .
568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder Logic id sublogics
568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder basic_spec sentence symb_items symb_map_items
568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder local_env sign morphism symbol raw_symbol =>
568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maederdata AnyRepresentation = forall id1 sublogics1
568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder basic_spec1 sentence1 symb_items1 symb_map_items1
568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder local_env1 sign1 morphism1 symbol1 raw_symbol1
b475a916d62584a2af5f51749240db7a5f0c8b82Christian Maeder id2 sublogics2
b475a916d62584a2af5f51749240db7a5f0c8b82Christian Maeder basic_spec2 sentence2 symb_items2 symb_map_items2
568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder local_env2 sign2 morphism2 symbol2 raw_symbol2 .
16060a5c23e794535eb1e7aa62ec4c370f0bff6aChristian Maeder (Logic id1 sublogics1
b475a916d62584a2af5f51749240db7a5f0c8b82Christian Maeder basic_spec1 sentence1 symb_items1 symb_map_items1
568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder local_env1 sign1 morphism1 symbol1 raw_symbol1,
1d330b771706686190ad2f3711ec5769c555c708Christian Maeder Logic id2 sublogics2
1d330b771706686190ad2f3711ec5769c555c708Christian Maeder basic_spec2 sentence2 symb_items2 symb_map_items2
568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder local_env2 sign2 morphism2 symbol2 raw_symbol2) =>
1d330b771706686190ad2f3711ec5769c555c708Christian Maeder Repr(LogicRepr id1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder local_env1 sign1 morphism1 symbol1 raw_symbol1
568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder id2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder local_env2 sign2 morphism2 symbol2 raw_symbol2)
568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder-- Composition of representations
1d330b771706686190ad2f3711ec5769c555c708Christian Maedercoerce :: a -> Maybe b = fromDynamic . toDyn
1d330b771706686190ad2f3711ec5769c555c708Christian Maederthe = maybe undefined id
568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maederg `comp` (Just f) = \x -> f x >>= g
1d330b771706686190ad2f3711ec5769c555c708Christian Maederid_repr i s = LogicRepr{
1d330b771706686190ad2f3711ec5769c555c708Christian Maeder repr_name = "id_"++head (sublogic_names i s),
568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder source = i, target = i,
568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder source_sublogic = s,
568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder target_sublogic = s,
1d330b771706686190ad2f3711ec5769c555c708Christian Maeder-- map_basic_spec = Just,
1d330b771706686190ad2f3711ec5769c555c708Christian Maeder map_sentence = \_ -> Just,
1d330b771706686190ad2f3711ec5769c555c708Christian Maeder map_sign = Just,
568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder projection = Just (proj_sublogic_sign i s,
568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder proj_sublogic_morphism i s,
1d330b771706686190ad2f3711ec5769c555c708Christian Maeder proj_sublogic_epsilon i s,
568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder proj_sublogic_basic_spec i s,
568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder proj_sublogic_symbol i s),
1d330b771706686190ad2f3711ec5769c555c708Christian Maeder map_morphism = Just,
568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder map_symbol = \x -> [x]
1d330b771706686190ad2f3711ec5769c555c708Christian Maedercomp_repr :: AnyRepresentation -> AnyRepresentation -> Maybe AnyRepresentation
568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maedercomp_repr (Repr (r1 :: {-Logic id1 sublogics1
568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder basic_spec1 sentence1 symb_items1 symb_map_items1
1d330b771706686190ad2f3711ec5769c555c708Christian Maeder local_env1 sign1 morphism1 symbol1 raw_symbol1,
568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder Logic id2 sublogics2
1d330b771706686190ad2f3711ec5769c555c708Christian Maeder basic_spec2 sentence2 symb_items2 symb_map_items2
568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder local_env2 sign2 morphism2 symbol2 raw_symbol2) => -}
568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder LogicRepr id1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
1d330b771706686190ad2f3711ec5769c555c708Christian Maeder local_env1 sign1 morphism1 symbol1 raw_symbol1
568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder id2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder local_env2 sign2 morphism2 symbol2 raw_symbol2))
1d330b771706686190ad2f3711ec5769c555c708Christian Maeder (Repr (r2 :: {-Logic id3 sublogics3
568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder basic_spec3 sentence3 symb_items3 symb_map_items3
568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder local_env3 sign3 morphism3 symbol3 raw_symbol3,
1d330b771706686190ad2f3711ec5769c555c708Christian Maeder Logic id4 sublogics4
1d330b771706686190ad2f3711ec5769c555c708Christian Maeder basic_spec4 sentence4 symb_items4 symb_map_items4
1d330b771706686190ad2f3711ec5769c555c708Christian Maeder local_env4 sign4 morphism4 symbol4 raw_symbol4) => -}
b475a916d62584a2af5f51749240db7a5f0c8b82Christian Maeder LogicRepr id3 sublogics3 basic_spec3 sentence3 symb_items3 symb_map_items3
b475a916d62584a2af5f51749240db7a5f0c8b82Christian Maeder local_env3 sign3 morphism3 symbol3 raw_symbol3
b475a916d62584a2af5f51749240db7a5f0c8b82Christian Maeder id4 sublogics4 basic_spec4 sentence4 symb_items4 symb_map_items4
b475a916d62584a2af5f51749240db7a5f0c8b82Christian Maeder local_env4 sign4 morphism4 symbol4 raw_symbol4)) =
b475a916d62584a2af5f51749240db7a5f0c8b82Christian Maeder case coerce (source r2)::Maybe id2 of
b475a916d62584a2af5f51749240db7a5f0c8b82Christian Maeder Nothing -> Nothing
b475a916d62584a2af5f51749240db7a5f0c8b82Christian Maeder Just _ -> if target_sublogic r1 <= the (coerce (source_sublogic r2)::Maybe sublogics2) then
b475a916d62584a2af5f51749240db7a5f0c8b82Christian Maeder Just (Repr (LogicRepr{
b475a916d62584a2af5f51749240db7a5f0c8b82Christian Maeder repr_name = repr_name r1++";"++repr_name r2,
b475a916d62584a2af5f51749240db7a5f0c8b82Christian Maeder source = source r1, target = target r2,
b475a916d62584a2af5f51749240db7a5f0c8b82Christian Maeder source_sublogic = source_sublogic r1,
b475a916d62584a2af5f51749240db7a5f0c8b82Christian Maeder target_sublogic = target_sublogic r2,
b475a916d62584a2af5f51749240db7a5f0c8b82Christian Maeder -- map_basic_spec = map_basic_spec r2 `comp` (coerce (map_basic_spec r1)::Maybe(basic_spec1 -> Maybe basic_spec3)),
b475a916d62584a2af5f51749240db7a5f0c8b82Christian Maeder map_sentence =
b475a916d62584a2af5f51749240db7a5f0c8b82Christian Maeder map_sentence r2 (the (((coerce (map_sign r1 sigma))::Maybe sign3)))
b475a916d62584a2af5f51749240db7a5f0c8b82Christian Maeder `comp` (coerce (map_sentence r1 sigma)::Maybe(sentence1 -> Maybe sentence3))),
b475a916d62584a2af5f51749240db7a5f0c8b82Christian Maeder map_sign = map_sign r2 `comp` (coerce (map_sign r1)::Maybe(sign1 -> Maybe sign3)),
b475a916d62584a2af5f51749240db7a5f0c8b82Christian Maeder projection = undefined {- (proj_sublogic_sign i s,
b475a916d62584a2af5f51749240db7a5f0c8b82Christian Maeder proj_sublogic_morphism i s,
b475a916d62584a2af5f51749240db7a5f0c8b82Christian Maeder proj_sublogic_epsilon i s,
568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder proj_sublogic_basic_spec i s,
568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder proj_sublogic_symbol i s) -} ,
b475a916d62584a2af5f51749240db7a5f0c8b82Christian Maeder map_morphism = map_morphism r2 `comp` (coerce (map_morphism r1)::Maybe(morphism1 -> Maybe morphism3)),
568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maeder map_symbol = map_symbol r2 `comp` (coerce (map_symbol r1)::Maybe(symbol1 -> [symbol3]))
568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maederthe_logic_list :: [AnyLogic] = [] -- [Logic CASL, Logic HasCASL, ...]
568a1ce407fd05a2007c5db3c5c57098bf13997fChristian Maederthe_representation_list :: [AnyRepresentation] = []