749074bf849727439f584139415f6a985a8aa875Christian Maeder{- |

32a2f5f00ff72c095b39629101043db4407974f9Christian MaederModule : $EmptyHeader$

f8a1ab8012a1f36060d6ce9b63399fa4a8a2981cChristian MaederDescription : <optional short description entry>

f8a1ab8012a1f36060d6ce9b63399fa4a8a2981cChristian MaederCopyright : (c) <Authors or Affiliations>

f8a1ab8012a1f36060d6ce9b63399fa4a8a2981cChristian MaederLicense : GPLv2 or higher

f8a1ab8012a1f36060d6ce9b63399fa4a8a2981cChristian Maeder

f8a1ab8012a1f36060d6ce9b63399fa4a8a2981cChristian MaederMaintainer : <email>

f8a1ab8012a1f36060d6ce9b63399fa4a8a2981cChristian MaederStability : unstable | experimental | provisional | stable | frozen

f8a1ab8012a1f36060d6ce9b63399fa4a8a2981cChristian MaederPortability : portable | non-portable (<reason>)

ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maeder

ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maeder<optional description>

ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maeder-}

ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maedermodule Grothendieck (module Logic, module Grothendieck) where

ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maeder

ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maederimport Logic

ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maeder

ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maederdata AnyLogic =

ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maeder forall id s m sen b sy .

2986838ec286d67e7c199e7ea81e7364ca36ad25Christian Maeder Logic id s m sen b sy =>

ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maeder G_logic id

c7041924e85535e80c7c08699cb308071d7010beChristian Maeder

c7041924e85535e80c7c08699cb308071d7010beChristian Maederdata AnyTranslation =

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

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

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

b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian Maeder

b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian Maederinstance 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