5957aa4a78c524b971d2275c42c3a925f30ff2a9Christian Maeder{-# LANGUAGE ScopedTypeVariables, MultiParamTypeClasses, DeriveDataTypeable #-}
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowskimodule Main where
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowskiimport Grothendieck
5957aa4a78c524b971d2275c42c3a925f30ff2a9Christian Maederimport StaticAnalysis
5957aa4a78c524b971d2275c42c3a925f30ff2a9Christian Maederdata L1 = L1 deriving (Typeable, Show)
5957aa4a78c524b971d2275c42c3a925f30ff2a9Christian Maederdata L2 = L2 deriving (Typeable, Show)
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowskiinstance Language L1 where language_name _ = "L1"
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowskiinstance Language L2 where language_name _ = "L2"
5957aa4a78c524b971d2275c42c3a925f30ff2a9Christian Maederdata B1 = B1 deriving (Typeable, Show, Eq)
5957aa4a78c524b971d2275c42c3a925f30ff2a9Christian Maederdata B2 = B2 deriving (Typeable, Show, Eq)
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowskiinstance Category L1 B1 B1 where
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski identity = undefined
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski dom = undefined
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder cod = undefined
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowskiinstance Category L2 B2 B2 where
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski identity = undefined
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski dom = undefined
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder cod = undefined
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowskiinstance Syntax L1 B1 B1 B1 B1 where
da955132262baab309a50fdffe228c9efe68251dCui Jian parse_basic_spec _ =
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski do string "{}"
da955132262baab309a50fdffe228c9efe68251dCui Jian parse_symbol_mapping _ =
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski do string "m"
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski parse_sentence = undefined
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowskiinstance Syntax L2 B2 B2 B2 B2 where
da955132262baab309a50fdffe228c9efe68251dCui Jian parse_basic_spec _ =
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski do string "#"
da955132262baab309a50fdffe228c9efe68251dCui Jian parse_symbol_mapping _ =
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski do string "n"
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski parse_sentence = undefined
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowskiinstance StaticAnalysis L1 B1 B1 B1 B1 B1 where
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder basic_analysis _ sig b = Just (sig, [])
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski stat_symbol_mapping = undefined
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowskiinstance StaticAnalysis L2 B2 B2 B2 B2 B2 where
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder basic_analysis _ sig b = Just (sig, [])
da955132262baab309a50fdffe228c9efe68251dCui Jian stat_symbol_mapping = undefined
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowskiinstance Logic L1 B1 B1 B1 B1 B1 where
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski empty_signature _ = B1
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder map_sentence = undefined
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder prover = undefined
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederinstance Logic L2 B2 B2 B2 B2 B2 where
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski empty_signature _ = B2
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder map_sentence = undefined
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder prover = undefined
da955132262baab309a50fdffe228c9efe68251dCui Jianth1 = (G_theory L1 (B1,[]))
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowskisp1 = (Basic_spec (G_basic_spec L1 B1))
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowskisp2 = (Basic_spec (G_basic_spec L2 B2))
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroedert1 = Logic_translation L1 L2 (\ B1 -> B2) (\ B1 -> B2) (\ _ B1 -> Just B2) (\ _ B2 -> Just B1)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederlogicGraph = ([("L1", G_logic L1), ("L2", G_logic L2)],
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder [("T1", G_LTR t1)])
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowskiinstance Eq AnyLogic where
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder (G_logic i1) == (G_logic (i2 :: id2)) =
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder case coerce i1 :: Maybe id2 of
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski Just _ -> True
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowskiinstance Show AnyLogic where
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder show id = case lookup id (map (\ (x, y) -> (y, x)) (fst logicGraph)) of
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Nothing -> "???"
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Just s -> "Logic: " ++ s
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowskip s = do let output = hetParse logicGraph s
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowskimain = do putStrLn "Enter spec\n"