{-# 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
