{-# LANGUAGE ExistentialQuantification #-}

module Grothendieck where

import Logic

import Data.Dynamic

data AnyLogic =

forall id s m sen b sy .

Logic id s m sen b sy =>

G_logic id

data AnyTranslation =

forall id1 s1 m1 sen1 b1 sy1 id2 s2 m2 sen2 b2 sy2 .

(Logic id1 s1 m1 sen1 b1 sy1, Logic id2 s2 m2 sen2 b2 sy2) =>

G_LTR (Logic_translation id1 s1 m1 sen1 b1 sy1 id2 s2 m2 sen2 b2 sy2)

instance Show AnyTranslation where

show _ = "<tr>"

type LogicGraph = ([(String, AnyLogic)], [(String, AnyTranslation)])

data G_basic_spec =

forall id s m sen b sy .

Logic id s m sen b sy =>

G_basic_spec id b

instance Show G_basic_spec where

show (G_basic_spec id b) = show b

data G_symbol_mapping_list =

forall id s m sen b sy .

Logic id s m sen b sy =>

G_symbol_mapping_list id sy

instance Show G_symbol_mapping_list where

show (G_symbol_mapping_list id sy) = show sy

data G_sentence =

forall id s m sen b sy .

Logic id s m sen b sy =>

G_sentence id sen

data G_theory =

forall id s m sen b sy .

Logic id s m sen b sy =>

G_theory id (Theory s sen)

data G_morphism =

forall id s m sen b sy .

Logic id s m sen b sy =>

G_morphism id m

instance Show G_theory where

show (G_theory _ (sig, ax)) = show sig

-- auxiliary functions for conversion between different logics

coerce :: (Typeable a, Typeable b) => a -> Maybe b

coerce = fromDynamic . toDyn

coerce1 :: (Typeable a, Typeable b) => a -> b

coerce1 = the . coerce

the :: Maybe a -> a

the (Just x) = x