content: {-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}
  {- |
  Module      :  ./Comorphisms/Haskell2IsabelleHOLCF.hs
  Description :  translating a Haskell subset to Isabelle HOLCF
  Copyright   :  (c) Paolo Torrini and Till Mossakowski and Uni Bremen 2004-2005
  License     :  All rights reserved.
  
  Maintainer  :  paolot@informatik.uni-bremen.de
  Stability   :  provisional
  Portability :  non-portable (imports Logic.Logic)
  
  The embedding comorphisms from Haskell to Isabelle
  -}
  
  module Comorphisms.Haskell2IsabelleHOLCF where
  
  import Comorphisms.Hs2HOLCF as Hs2HOLCF
  
  import Logic.Logic as Logic
  import Logic.Comorphism
  
  -- Haskell
  import Haskell.Logic_Haskell
  import Haskell.HatParser as HatParser
  import Haskell.HatAna as HatAna
  
  -- Isabelle
  import Isabelle.IsaSign as IsaSign
  import Isabelle.Logic_Isabelle
  
  -- * Comorphisms
  
  -- The identity of the comorphism
  data Haskell2IsabelleHOLCF = Haskell2IsabelleHOLCF deriving Show
  
  instance Language Haskell2IsabelleHOLCF
  
  instance Comorphism Haskell2IsabelleHOLCF
                 Haskell ()
                 HsDecls (TiDecl PNT) () ()
                 HatAna.Sign HaskellMorphism
                 () () ()
                 Isabelle () () IsaSign.Sentence () ()
                 IsaSign.Sign
                 IsabelleMorphism () () () where
      sourceLogic _ = Haskell
      sourceSublogic _ = ()
      targetLogic _ = Isabelle
      mapSublogic _ _ = Just ()
      map_theory _ (sign, sens) =
          Hs2HOLCF.transTheory (IsCont True) False sign sens
      has_model_expansion _ = True
  
  data Haskell2IsabelleHOL = Haskell2IsabelleHOL deriving Show
  
  instance Language Haskell2IsabelleHOL where
    language_name Haskell2IsabelleHOL = "Haskell2Isabelle"
  
  instance Comorphism Haskell2IsabelleHOL
                 Haskell ()
                 HsDecls (TiDecl PNT) () ()
                 HatAna.Sign HaskellMorphism
                 () () ()
                 Isabelle () () IsaSign.Sentence () ()
                 IsaSign.Sign
                 IsabelleMorphism () () () where
      sourceLogic _ = Haskell
      sourceSublogic _ = ()
      targetLogic _ = Isabelle
      mapSublogic _ _ = Just ()
      map_theory _ (sign, sens) =
          Hs2HOLCF.transTheory NotCont False sign sens
  