Main.hs revision 84a353c2e95b6b0842ca0e2665665e52a87f792e
7439eb4a3269fa24aebfe522eb5be6f212e618e2Christian Maedermodule Main where
7c808aadfb7293563388dbe16d84cf3384bb5d3cDaniel Calegariimport ParsecExpr
7c808aadfb7293563388dbe16d84cf3384bb5d3cDaniel Calegariimport Grothendieck
7439eb4a3269fa24aebfe522eb5be6f212e618e2Christian Maederimport StaticAnalysis
7439eb4a3269fa24aebfe522eb5be6f212e618e2Christian Maederimport Dynamic
ab8506c5100f101785452b5047259ec4f17ef436Daniel Calegaridata L1 = L1 deriving Show
7439eb4a3269fa24aebfe522eb5be6f212e618e2Christian Maederdata L2 = L2 deriving Show
acc049a844d19fb294ce7f68742390dee87447dcDaniel Calegariinstance Typeable L1 where typeOf _ = mkAppTy (mkTyCon "L1") []
acc049a844d19fb294ce7f68742390dee87447dcDaniel Calegariinstance Typeable L2 where typeOf _ = mkAppTy (mkTyCon "L2") []
7c808aadfb7293563388dbe16d84cf3384bb5d3cDaniel Calegariinstance Language L1 where language_name _ = "L1"
7c808aadfb7293563388dbe16d84cf3384bb5d3cDaniel Calegariinstance Language L2 where language_name _ = "L2"
7c808aadfb7293563388dbe16d84cf3384bb5d3cDaniel Calegaridata B1 = B1 deriving (Show, Eq)
ab8506c5100f101785452b5047259ec4f17ef436Daniel Calegaridata B2 = B2 deriving (Show, Eq)
ab8506c5100f101785452b5047259ec4f17ef436Daniel Calegariinstance Typeable B1 where typeOf _ = mkAppTy (mkTyCon "B1") []
7c808aadfb7293563388dbe16d84cf3384bb5d3cDaniel Calegariinstance Typeable B2 where typeOf _ = mkAppTy (mkTyCon "B2") []
acc049a844d19fb294ce7f68742390dee87447dcDaniel Calegariinstance Category L1 B1 B1 where
acc049a844d19fb294ce7f68742390dee87447dcDaniel Calegari identity = undefined
acc049a844d19fb294ce7f68742390dee87447dcDaniel Calegari o = undefined
f2c638409c8d870e5ad6edf2b064f959b0b86aa3Daniel Calegari dom = undefined
7439eb4a3269fa24aebfe522eb5be6f212e618e2Christian Maeder cod = undefined
7c808aadfb7293563388dbe16d84cf3384bb5d3cDaniel Calegariinstance Category L2 B2 B2 where
7c808aadfb7293563388dbe16d84cf3384bb5d3cDaniel Calegari identity = undefined
7c808aadfb7293563388dbe16d84cf3384bb5d3cDaniel Calegari o = undefined
7c808aadfb7293563388dbe16d84cf3384bb5d3cDaniel Calegari dom = undefined
acc049a844d19fb294ce7f68742390dee87447dcDaniel Calegari cod = undefined
acc049a844d19fb294ce7f68742390dee87447dcDaniel Calegariinstance Syntax L1 B1 B1 B1 B1 where
acc049a844d19fb294ce7f68742390dee87447dcDaniel Calegari parse_basic_spec _ =
ab8506c5100f101785452b5047259ec4f17ef436Daniel Calegari do string "{}"
7c808aadfb7293563388dbe16d84cf3384bb5d3cDaniel Calegari parse_symbol_mapping _ =
ab8506c5100f101785452b5047259ec4f17ef436Daniel Calegari do string "m"
acc049a844d19fb294ce7f68742390dee87447dcDaniel Calegari parse_sentence = undefined
acc049a844d19fb294ce7f68742390dee87447dcDaniel Calegariinstance Syntax L2 B2 B2 B2 B2 where
f2c638409c8d870e5ad6edf2b064f959b0b86aa3Daniel Calegari parse_basic_spec _ =
f2c638409c8d870e5ad6edf2b064f959b0b86aa3Daniel Calegari do string "#"
7c808aadfb7293563388dbe16d84cf3384bb5d3cDaniel Calegari parse_symbol_mapping _ =
7c808aadfb7293563388dbe16d84cf3384bb5d3cDaniel Calegari do string "n"
acc049a844d19fb294ce7f68742390dee87447dcDaniel Calegari parse_sentence = undefined
7c808aadfb7293563388dbe16d84cf3384bb5d3cDaniel Calegariinstance StaticAnalysis L1 B1 B1 B1 B1 B1 where
f2c638409c8d870e5ad6edf2b064f959b0b86aa3Daniel Calegari basic_analysis _ sig b = Just (sig,[])
7c808aadfb7293563388dbe16d84cf3384bb5d3cDaniel Calegari stat_symbol_mapping = undefined
7c808aadfb7293563388dbe16d84cf3384bb5d3cDaniel Calegariinstance StaticAnalysis L2 B2 B2 B2 B2 B2 where
acc049a844d19fb294ce7f68742390dee87447dcDaniel Calegari basic_analysis _ sig b = Just (sig,[])
acc049a844d19fb294ce7f68742390dee87447dcDaniel Calegari stat_symbol_mapping = undefined
acc049a844d19fb294ce7f68742390dee87447dcDaniel Calegariinstance Logic L1 B1 B1 B1 B1 B1 where
acc049a844d19fb294ce7f68742390dee87447dcDaniel Calegari empty_signature _ = B1
7c808aadfb7293563388dbe16d84cf3384bb5d3cDaniel Calegari map_sentence = undefined
f2c638409c8d870e5ad6edf2b064f959b0b86aa3Daniel Calegari prover = undefined
f2c638409c8d870e5ad6edf2b064f959b0b86aa3Daniel Calegariinstance Logic L2 B2 B2 B2 B2 B2 where
f2c638409c8d870e5ad6edf2b064f959b0b86aa3Daniel Calegari empty_signature _ = B2
acc049a844d19fb294ce7f68742390dee87447dcDaniel Calegari map_sentence = undefined
acc049a844d19fb294ce7f68742390dee87447dcDaniel Calegari prover = undefined
f2c638409c8d870e5ad6edf2b064f959b0b86aa3Daniel Calegarith1 = (G_theory L1 (B1,[]))
f2c638409c8d870e5ad6edf2b064f959b0b86aa3Daniel Calegarisp1 = (Basic_spec (G_basic_spec L1 B1))
7c808aadfb7293563388dbe16d84cf3384bb5d3cDaniel Calegarisp2 = (Basic_spec (G_basic_spec L2 B2))
ab8506c5100f101785452b5047259ec4f17ef436Daniel Calegarit1 = Logic_translation L1 L2 (\B1 -> B2) (\B1 -> B2) (\_ -> \B1 -> Just B2) (\_ -> \B2 -> Just B1)
ab8506c5100f101785452b5047259ec4f17ef436Daniel CalegarilogicGraph = ([("L1",G_logic L1),("L2",G_logic L2)],
7c808aadfb7293563388dbe16d84cf3384bb5d3cDaniel Calegari [("T1",G_LTR t1)])
acc049a844d19fb294ce7f68742390dee87447dcDaniel Calegariinstance Eq AnyLogic where
acc049a844d19fb294ce7f68742390dee87447dcDaniel Calegari (G_logic i1) == (G_logic (i2::id2)) =
acc049a844d19fb294ce7f68742390dee87447dcDaniel Calegari case (coerce i1)::Maybe id2 of
acc049a844d19fb294ce7f68742390dee87447dcDaniel Calegari Just _ -> True
7c808aadfb7293563388dbe16d84cf3384bb5d3cDaniel Calegariinstance Show AnyLogic where
7c808aadfb7293563388dbe16d84cf3384bb5d3cDaniel Calegari show id = case lookup id (map (\(x,y) -> (y,x)) (fst logicGraph)) of
7c808aadfb7293563388dbe16d84cf3384bb5d3cDaniel Calegari Nothing -> "???"
7c808aadfb7293563388dbe16d84cf3384bb5d3cDaniel Calegari Just s -> "Logic: "++ s
acc049a844d19fb294ce7f68742390dee87447dcDaniel Calegarip s = do let output = hetParse logicGraph s
acc049a844d19fb294ce7f68742390dee87447dcDaniel Calegari putStrLn (show output)
acc049a844d19fb294ce7f68742390dee87447dcDaniel Calegarimain = do putStrLn "Enter spec\n"