Grothendieck.hs revision 047de69319a752b9c467166b1264f9e121459e2d
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowskimodule Grothendieck (module Logic, module Grothendieck) where
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowskidata AnyLogic =
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski forall id s m sen b sy .
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski Logic id s m sen b sy =>
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowskidata AnyTranslation =
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski forall id1 s1 m1 sen1 b1 sy1 id2 s2 m2 sen2 b2 sy2 .
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski (Logic id1 s1 m1 sen1 b1 sy1, Logic id2 s2 m2 sen2 b2 sy2) =>
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski G_LTR (Logic_translation id1 s1 m1 sen1 b1 sy1 id2 s2 m2 sen2 b2 sy2)
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowskiinstance Show AnyTranslation where
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski show _ = "<tr>"
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowskitype LogicGraph = ([(String,AnyLogic)],[(String,AnyTranslation)])
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowskidata G_basic_spec =
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski forall id s m sen b sy .
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski Logic id s m sen b sy =>
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski G_basic_spec id b
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowskiinstance Show G_basic_spec where
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski show (G_basic_spec id b) = show b
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowskidata G_symbol_mapping_list =
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski forall id s m sen b sy .
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski Logic id s m sen b sy =>
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski G_symbol_mapping_list id sy
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowskiinstance Show G_symbol_mapping_list where
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski show (G_symbol_mapping_list id sy) = show sy
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowskidata G_sentence =
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski forall id s m sen b sy .
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski Logic id s m sen b sy =>
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski G_sentence id sen
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowskidata G_theory =
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski forall id s m sen b sy .
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski Logic id s m sen b sy =>
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski G_theory id (Theory s sen)
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowskidata G_morphism =
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski forall id s m sen b sy .
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski Logic id s m sen b sy =>
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski G_morphism id m
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowskiinstance Show G_theory where
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski show (G_theory _ (sig,ax)) = show sig
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski-- auxiliary functions for conversion between different logics
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowskicoerce :: (Typeable a, Typeable b) => a -> Maybe b
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowskicoerce = fromDynamic . toDyn
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowskicoerce1 :: (Typeable a, Typeable b) => a -> b
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowskicoerce1 = the . coerce
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowskithe :: Maybe a -> a
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowskithe (Just x) = x