Grothendieck.hs revision 6f3198a56c02c18d02d19b4aaad1c395686aec07
9d0567bda351efa4286f38e85fb3e41ecd3683eaChristian Maeder-- needs ghc -fglasgow-exts
9d0567bda351efa4286f38e85fb3e41ecd3683eaChristian Maeder Till Mossakowski
9d0567bda351efa4286f38e85fb3e41ecd3683eaChristian Maeder The Grothendieck logic is defined to be the
9d0567bda351efa4286f38e85fb3e41ecd3683eaChristian Maeder heterogeneous logic over the logic graph.
9d0567bda351efa4286f38e85fb3e41ecd3683eaChristian Maeder This will be the logic over which the data
9d0567bda351efa4286f38e85fb3e41ecd3683eaChristian Maeder structures and algorithms for specification in-the-large
9f93b2a8b552789cd939d599504d39732672dc84Christian Maeder R. Diaconescu:
9f93b2a8b552789cd939d599504d39732672dc84Christian Maeder Grothendieck institutions
20bd79f8844604c145510c616fecdaf47eba2fdbChristian Maeder J. applied categorical structures, to appear
2119c0874c93fc1cdfea381bcfea69e8fdb8b6e2Christian Maeder T. Mossakowski:
9f93b2a8b552789cd939d599504d39732672dc84Christian Maeder Heterogeneous development graphs and heterogeneous borrowing
20bd79f8844604c145510c616fecdaf47eba2fdbChristian Maeder Fossacs 2002, LNCS 2303
3b48e17c1da54ee669e70b626d9fbc32ce495b2cChristian Maeder T. Mossakowski: Simplified heterogeneous specification
2119c0874c93fc1cdfea381bcfea69e8fdb8b6e2Christian Maedermodule Grothendieck where
2119c0874c93fc1cdfea381bcfea69e8fdb8b6e2Christian Maederimport LogicGraph
2119c0874c93fc1cdfea381bcfea69e8fdb8b6e2Christian Maederimport Dynamic
20bd79f8844604c145510c616fecdaf47eba2fdbChristian Maederdata Grothendieck = Grothendieck
20bd79f8844604c145510c616fecdaf47eba2fdbChristian Maederdata G_basic_spec = forall id sublogics
20bd79f8844604c145510c616fecdaf47eba2fdbChristian Maeder basic_spec sentence symb_items symb_map_items
20bd79f8844604c145510c616fecdaf47eba2fdbChristian Maeder local_env sign morphism symbol raw_symbol .
20bd79f8844604c145510c616fecdaf47eba2fdbChristian Maeder Logic id sublogics
20bd79f8844604c145510c616fecdaf47eba2fdbChristian Maeder basic_spec sentence symb_items symb_map_items
5afff1a0f62394414c33b06141175b3ab0b117a5Christian Maeder local_env sign morphism symbol raw_symbol =>
20bd79f8844604c145510c616fecdaf47eba2fdbChristian Maeder G_basic_spec id basic_spec
20bd79f8844604c145510c616fecdaf47eba2fdbChristian Maederdata G_sentence = forall id sublogics
a97055b3846103c11f2f39d16713fb278dd15d70Christian Maeder basic_spec sentence symb_items symb_map_items
20bd79f8844604c145510c616fecdaf47eba2fdbChristian Maeder local_env sign morphism symbol raw_symbol .
20bd79f8844604c145510c616fecdaf47eba2fdbChristian Maeder Logic id sublogics
3b48e17c1da54ee669e70b626d9fbc32ce495b2cChristian Maeder basic_spec sentence symb_items symb_map_items
9f93b2a8b552789cd939d599504d39732672dc84Christian Maeder local_env sign morphism symbol raw_symbol =>
9f93b2a8b552789cd939d599504d39732672dc84Christian Maeder G_sentence id sentence
9f93b2a8b552789cd939d599504d39732672dc84Christian Maederdata G_sign = forall id sublogics
9f93b2a8b552789cd939d599504d39732672dc84Christian Maeder basic_spec sentence symb_items symb_map_items
3b48e17c1da54ee669e70b626d9fbc32ce495b2cChristian Maeder local_env sign morphism symbol raw_symbol .
9f93b2a8b552789cd939d599504d39732672dc84Christian Maeder Logic id sublogics
9f93b2a8b552789cd939d599504d39732672dc84Christian Maeder basic_spec sentence symb_items symb_map_items
9f93b2a8b552789cd939d599504d39732672dc84Christian Maeder local_env sign morphism symbol raw_symbol =>
9f93b2a8b552789cd939d599504d39732672dc84Christian Maeder G_sign id sign
9f93b2a8b552789cd939d599504d39732672dc84Christian Maederdata G_morphism = forall id sublogics
9f93b2a8b552789cd939d599504d39732672dc84Christian Maeder basic_spec sentence symb_items symb_map_items
9f93b2a8b552789cd939d599504d39732672dc84Christian Maeder local_env sign morphism symbol raw_symbol .
9f93b2a8b552789cd939d599504d39732672dc84Christian Maeder Logic id sublogics
9f93b2a8b552789cd939d599504d39732672dc84Christian Maeder basic_spec sentence symb_items symb_map_items
9f93b2a8b552789cd939d599504d39732672dc84Christian Maeder local_env sign morphism symbol raw_symbol =>
9f93b2a8b552789cd939d599504d39732672dc84Christian Maeder G_morphism id morphism
9f93b2a8b552789cd939d599504d39732672dc84Christian Maederdata G_symbol = forall id sublogics
9f93b2a8b552789cd939d599504d39732672dc84Christian Maeder basic_spec sentence symb_items symb_map_items
9f93b2a8b552789cd939d599504d39732672dc84Christian Maeder local_env sign morphism symbol raw_symbol .
9f93b2a8b552789cd939d599504d39732672dc84Christian Maeder Logic id sublogics
9f93b2a8b552789cd939d599504d39732672dc84Christian Maeder basic_spec sentence symb_items symb_map_items
2119c0874c93fc1cdfea381bcfea69e8fdb8b6e2Christian Maeder local_env sign morphism symbol raw_symbol =>
2119c0874c93fc1cdfea381bcfea69e8fdb8b6e2Christian Maeder G_symbol id symbol
2119c0874c93fc1cdfea381bcfea69e8fdb8b6e2Christian Maederdata G_symb_items = forall id sublogics
2119c0874c93fc1cdfea381bcfea69e8fdb8b6e2Christian Maeder basic_spec sentence symb_items symb_map_items
2119c0874c93fc1cdfea381bcfea69e8fdb8b6e2Christian Maeder local_env sign morphism symbol raw_symbol .
2119c0874c93fc1cdfea381bcfea69e8fdb8b6e2Christian Maeder Logic id sublogics
2119c0874c93fc1cdfea381bcfea69e8fdb8b6e2Christian Maeder basic_spec sentence symb_items symb_map_items
2119c0874c93fc1cdfea381bcfea69e8fdb8b6e2Christian Maeder local_env sign morphism symbol raw_symbol =>
2119c0874c93fc1cdfea381bcfea69e8fdb8b6e2Christian Maeder G_symb_items id symb_items
2119c0874c93fc1cdfea381bcfea69e8fdb8b6e2Christian Maederdata G_symb_items_list = forall id sublogics
2119c0874c93fc1cdfea381bcfea69e8fdb8b6e2Christian Maeder basic_spec sentence symb_items symb_map_items
2119c0874c93fc1cdfea381bcfea69e8fdb8b6e2Christian Maeder local_env sign morphism symbol raw_symbol .
2119c0874c93fc1cdfea381bcfea69e8fdb8b6e2Christian Maeder Logic id sublogics
2119c0874c93fc1cdfea381bcfea69e8fdb8b6e2Christian Maeder basic_spec sentence symb_items symb_map_items
2119c0874c93fc1cdfea381bcfea69e8fdb8b6e2Christian Maeder local_env sign morphism symbol raw_symbol =>
2119c0874c93fc1cdfea381bcfea69e8fdb8b6e2Christian Maeder G_symb_items_list id [symb_items]
2119c0874c93fc1cdfea381bcfea69e8fdb8b6e2Christian Maederdata G_symb_map_items = forall id sublogics
2119c0874c93fc1cdfea381bcfea69e8fdb8b6e2Christian Maeder basic_spec sentence symb_items symb_map_items
2119c0874c93fc1cdfea381bcfea69e8fdb8b6e2Christian Maeder local_env sign morphism symbol raw_symbol .
2119c0874c93fc1cdfea381bcfea69e8fdb8b6e2Christian Maeder Logic id sublogics
2119c0874c93fc1cdfea381bcfea69e8fdb8b6e2Christian Maeder basic_spec sentence symb_items symb_map_items
2119c0874c93fc1cdfea381bcfea69e8fdb8b6e2Christian Maeder local_env sign morphism symbol raw_symbol =>
2119c0874c93fc1cdfea381bcfea69e8fdb8b6e2Christian Maeder G_symb_map_items id symb_map_items
2119c0874c93fc1cdfea381bcfea69e8fdb8b6e2Christian Maedercoerce :: a -> Maybe b = fromDynamic . toDyn
2119c0874c93fc1cdfea381bcfea69e8fdb8b6e2Christian Maederhomogenize_symb_items :: [G_symb_items] -> Maybe G_symb_items_list
2119c0874c93fc1cdfea381bcfea69e8fdb8b6e2Christian Maederhomogenize_symb_items [] = Nothing
2119c0874c93fc1cdfea381bcfea69e8fdb8b6e2Christian Maederhomogenize_symb_items (G_symb_items i (s::symb_map_items) : rest) =
2119c0874c93fc1cdfea381bcfea69e8fdb8b6e2Christian Maeder maybe Nothing
2119c0874c93fc1cdfea381bcfea69e8fdb8b6e2Christian Maeder (\l -> Just (G_symb_items_list i l))
2119c0874c93fc1cdfea381bcfea69e8fdb8b6e2Christian Maeder ( sequence (Just s :
2119c0874c93fc1cdfea381bcfea69e8fdb8b6e2Christian Maeder map (\(G_symb_items _ si) -> coerce si::Maybe symb_map_items) rest) )