Main.hs revision 5957aa4a78c524b971d2275c42c3a925f30ff2a9
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 o = undefined
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski dom = undefined
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski cod = undefined
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowskiinstance Category L2 B2 B2 where
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski identity = undefined
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski o = undefined
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski dom = undefined
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski 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
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski basic_analysis _ sig b = Just (sig,[])
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski stat_symbol_mapping = undefined
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowskiinstance StaticAnalysis L2 B2 B2 B2 B2 B2 where
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski 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
da955132262baab309a50fdffe228c9efe68251dCui Jian map_sentence = undefined
da955132262baab309a50fdffe228c9efe68251dCui Jian prover = undefined
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowskiinstance Logic L2 B2 B2 B2 B2 B2 where
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski empty_signature _ = B2
da955132262baab309a50fdffe228c9efe68251dCui Jian map_sentence = undefined
da955132262baab309a50fdffe228c9efe68251dCui Jian 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))
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowskit1 = Logic_translation L1 L2 (\B1 -> B2) (\B1 -> B2) (\_ -> \B1 -> Just B2) (\_ -> \B2 -> Just B1)
047de69319a752b9c467166b1264f9e121459e2dTill MossakowskilogicGraph = ([("L1",G_logic L1),("L2",G_logic L2)],
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski [("T1",G_LTR t1)])
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowskiinstance Eq AnyLogic where
da955132262baab309a50fdffe228c9efe68251dCui Jian (G_logic i1) == (G_logic (i2::id2)) =
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski case (coerce i1)::Maybe id2 of
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski Just _ -> True
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowskiinstance Show AnyLogic where
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski show id = case lookup id (map (\(x,y) -> (y,x)) (fst logicGraph)) of
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski Nothing -> "???"
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowski Just s -> "Logic: "++ s
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowskip s = do let output = hetParse logicGraph s
da955132262baab309a50fdffe228c9efe68251dCui Jian putStrLn (show output)
047de69319a752b9c467166b1264f9e121459e2dTill Mossakowskimain = do putStrLn "Enter spec\n"