05bf9cbe382548c2665dd01a6a402640c9ec3813Christian Maeder{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}
bb4be59e45b3d484f091b81075375a8535ad01dbTill Mossakowski{- |
e9458b1a7a19a63aa4c179f9ab20f4d50681c168Jens ElknerModule : ./Comorphisms/Haskell2IsabelleHOLCF.hs
de6a40dbdd4712e5a9398b8519a59b1eaeab2f5aChristian MaederDescription : translating a Haskell subset to Isabelle HOLCF
ea0722105c689a2ba710686084a41d2a3d4767ccChristian MaederCopyright : (c) Paolo Torrini and Till Mossakowski and Uni Bremen 2004-2005
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederLicense : All rights reserved.
bb4be59e45b3d484f091b81075375a8535ad01dbTill Mossakowski
2eeec5240b424984e3ee26296da1eeab6c6d739eChristian MaederMaintainer : paolot@informatik.uni-bremen.de
bb4be59e45b3d484f091b81075375a8535ad01dbTill MossakowskiStability : provisional
bb4be59e45b3d484f091b81075375a8535ad01dbTill MossakowskiPortability : non-portable (imports Logic.Logic)
bb4be59e45b3d484f091b81075375a8535ad01dbTill Mossakowski
5c358300e78157f4bfaf5415c70e1096a9205b61Christian MaederThe embedding comorphisms from Haskell to Isabelle
d961b6905476ab0f53a2811ce3a3c52272e32ae2Paolo Torrini-}
9360d5eabfc2c13f82306dca39f18181f3929f88Paolo Torrini
410307167d116ddab45e02698eac31043619ed05Christian Maedermodule Comorphisms.Haskell2IsabelleHOLCF where
bb4be59e45b3d484f091b81075375a8535ad01dbTill Mossakowski
3ef0affb5c3f20d77ed29a51202a71315babcb75Paolo Torriniimport Comorphisms.Hs2HOLCF as Hs2HOLCF
3ef0affb5c3f20d77ed29a51202a71315babcb75Paolo Torrini
729aff22a7983f5bb113dcc604157edd728c1484Christian Maederimport Logic.Logic as Logic
95df121be79af0f220254b38ee826448ee622c39Paolo Torriniimport Logic.Comorphism
bb4be59e45b3d484f091b81075375a8535ad01dbTill Mossakowski
9360d5eabfc2c13f82306dca39f18181f3929f88Paolo Torrini-- Haskell
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maederimport Haskell.Logic_Haskell
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maederimport Haskell.HatParser as HatParser
d961b6905476ab0f53a2811ce3a3c52272e32ae2Paolo Torriniimport Haskell.HatAna as HatAna
bb4be59e45b3d484f091b81075375a8535ad01dbTill Mossakowski
bb4be59e45b3d484f091b81075375a8535ad01dbTill Mossakowski-- Isabelle
5d2e4f0bf48170b00f3445835e3f7911f6f8a2d9Christian Maederimport Isabelle.IsaSign as IsaSign
95df121be79af0f220254b38ee826448ee622c39Paolo Torriniimport Isabelle.Logic_Isabelle
d961b6905476ab0f53a2811ce3a3c52272e32ae2Paolo Torrini
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder-- * Comorphisms
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder
fc38d341dd4954308b9a2effc35af54a8ea962f9Paolo Torrini-- The identity of the comorphism
49f91677cae08b7095eda6c260b3311277775e4eChristian Maederdata Haskell2IsabelleHOLCF = Haskell2IsabelleHOLCF deriving Show
fc38d341dd4954308b9a2effc35af54a8ea962f9Paolo Torrini
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maederinstance Language Haskell2IsabelleHOLCF
95df121be79af0f220254b38ee826448ee622c39Paolo Torrini
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maederinstance Comorphism Haskell2IsabelleHOLCF
95df121be79af0f220254b38ee826448ee622c39Paolo Torrini Haskell ()
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder HsDecls (TiDecl PNT) () ()
d961b6905476ab0f53a2811ce3a3c52272e32ae2Paolo Torrini HatAna.Sign HaskellMorphism
95df121be79af0f220254b38ee826448ee622c39Paolo Torrini () () ()
95df121be79af0f220254b38ee826448ee622c39Paolo Torrini Isabelle () () IsaSign.Sentence () ()
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder IsaSign.Sign
1a2210d21fe7546333bb03d2768bb9ec562ef3abChristian Maeder IsabelleMorphism () () () where
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder sourceLogic _ = Haskell
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder sourceSublogic _ = ()
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder targetLogic _ = Isabelle
75f166d5467c01dbaf4d6d9815bed40e6ae27b3dChristian Maeder mapSublogic _ _ = Just ()
5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder map_theory _ (sign, sens) =
39f1a07923020496228e0577ac63aa94a91d63cbChristian Maeder Hs2HOLCF.transTheory (IsCont True) False sign sens
1a2210d21fe7546333bb03d2768bb9ec562ef3abChristian Maeder has_model_expansion _ = True
306e32e1cf1b4a38a2e64e03d8b2ac80b2dcbd0cChristian Maeder
49f91677cae08b7095eda6c260b3311277775e4eChristian Maederdata Haskell2IsabelleHOL = Haskell2IsabelleHOL deriving Show
306e32e1cf1b4a38a2e64e03d8b2ac80b2dcbd0cChristian Maeder
49f91677cae08b7095eda6c260b3311277775e4eChristian Maederinstance Language Haskell2IsabelleHOL where
49f91677cae08b7095eda6c260b3311277775e4eChristian Maeder language_name Haskell2IsabelleHOL = "Haskell2Isabelle"
306e32e1cf1b4a38a2e64e03d8b2ac80b2dcbd0cChristian Maeder
306e32e1cf1b4a38a2e64e03d8b2ac80b2dcbd0cChristian Maederinstance Comorphism Haskell2IsabelleHOL
306e32e1cf1b4a38a2e64e03d8b2ac80b2dcbd0cChristian Maeder Haskell ()
306e32e1cf1b4a38a2e64e03d8b2ac80b2dcbd0cChristian Maeder HsDecls (TiDecl PNT) () ()
306e32e1cf1b4a38a2e64e03d8b2ac80b2dcbd0cChristian Maeder HatAna.Sign HaskellMorphism
306e32e1cf1b4a38a2e64e03d8b2ac80b2dcbd0cChristian Maeder () () ()
306e32e1cf1b4a38a2e64e03d8b2ac80b2dcbd0cChristian Maeder Isabelle () () IsaSign.Sentence () ()
306e32e1cf1b4a38a2e64e03d8b2ac80b2dcbd0cChristian Maeder IsaSign.Sign
1a2210d21fe7546333bb03d2768bb9ec562ef3abChristian Maeder IsabelleMorphism () () () where
306e32e1cf1b4a38a2e64e03d8b2ac80b2dcbd0cChristian Maeder sourceLogic _ = Haskell
306e32e1cf1b4a38a2e64e03d8b2ac80b2dcbd0cChristian Maeder sourceSublogic _ = ()
306e32e1cf1b4a38a2e64e03d8b2ac80b2dcbd0cChristian Maeder targetLogic _ = Isabelle
75f166d5467c01dbaf4d6d9815bed40e6ae27b3dChristian Maeder mapSublogic _ _ = Just ()
306e32e1cf1b4a38a2e64e03d8b2ac80b2dcbd0cChristian Maeder map_theory _ (sign, sens) =
306e32e1cf1b4a38a2e64e03d8b2ac80b2dcbd0cChristian Maeder Hs2HOLCF.transTheory NotCont False sign sens