5957aa4a78c524b971d2275c42c3a925f30ff2a9Christian Maeder{-# LANGUAGE ExistentialQuantification #-}
5957aa4a78c524b971d2275c42c3a925f30ff2a9Christian Maedermodule Grothendieck where
da955132262baab309a50fdffe228c9efe68251dCui Jiandata AnyLogic =
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski forall id s m sen b sy .
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder 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>"
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroedertype LogicGraph = ([(String, AnyLogic)], [(String, AnyTranslation)])
da955132262baab309a50fdffe228c9efe68251dCui Jiandata G_basic_spec =
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski forall id s m sen b sy .
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Logic id s m sen b sy =>
da955132262baab309a50fdffe228c9efe68251dCui Jian G_basic_spec id b
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowskiinstance Show G_basic_spec where
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski show (G_basic_spec id b) = show b
da955132262baab309a50fdffe228c9efe68251dCui Jiandata G_symbol_mapping_list =
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski forall id s m sen b sy .
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder 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
da955132262baab309a50fdffe228c9efe68251dCui Jiandata G_sentence =
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski forall id s m sen b sy .
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Logic id s m sen b sy =>
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski G_sentence id sen
da955132262baab309a50fdffe228c9efe68251dCui Jiandata G_theory =
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski forall id s m sen b sy .
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Logic id s m sen b sy =>
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski G_theory id (Theory s sen)
da955132262baab309a50fdffe228c9efe68251dCui Jiandata G_morphism =
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski forall id s m sen b sy .
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Logic id s m sen b sy =>
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski G_morphism id m
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowskiinstance Show G_theory where
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder 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
da955132262baab309a50fdffe228c9efe68251dCui Jiancoerce1 = the . coerce
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowskithe :: Maybe a -> a
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowskithe (Just x) = x