{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}
{- |
Module      :  ./Comorphisms/PCoClTyConsHOL2IsabelleHOL.hs
Description :  translating a HasCASL subset to Isabelle
Copyright   :  (c) C. Maeder, DFKI 2006
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Christian.Maeder@dfki.de
Stability   :  provisional
Portability :  non-portable (imports Logic.Logic)

The embedding comorphism from HasCASL without subtypes to
Isabelle-HOL.  Partial functions yield an option or bool result in
Isabelle. Case-terms and constructor classes are not supported yet.
-}

module Comorphisms.PCoClTyConsHOL2IsabelleHOL
    (PCoClTyConsHOL2IsabelleHOL (..)) where

import Comorphisms.PPolyTyConsHOL2IsaUtils
import Logic.Logic as Logic
import Logic.Comorphism

import HasCASL.Logic_HasCASL
import HasCASL.Sublogic
import HasCASL.As
import HasCASL.Le as Le

import Isabelle.IsaSign as Isa
import Isabelle.Logic_Isabelle

-- | The identity of the comorphism
data PCoClTyConsHOL2IsabelleHOL = PCoClTyConsHOL2IsabelleHOL deriving Int -> PCoClTyConsHOL2IsabelleHOL -> ShowS
[PCoClTyConsHOL2IsabelleHOL] -> ShowS
PCoClTyConsHOL2IsabelleHOL -> String
(Int -> PCoClTyConsHOL2IsabelleHOL -> ShowS)
-> (PCoClTyConsHOL2IsabelleHOL -> String)
-> ([PCoClTyConsHOL2IsabelleHOL] -> ShowS)
-> Show PCoClTyConsHOL2IsabelleHOL
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [PCoClTyConsHOL2IsabelleHOL] -> ShowS
$cshowList :: [PCoClTyConsHOL2IsabelleHOL] -> ShowS
show :: PCoClTyConsHOL2IsabelleHOL -> String
$cshow :: PCoClTyConsHOL2IsabelleHOL -> String
showsPrec :: Int -> PCoClTyConsHOL2IsabelleHOL -> ShowS
$cshowsPrec :: Int -> PCoClTyConsHOL2IsabelleHOL -> ShowS
Show

instance Language PCoClTyConsHOL2IsabelleHOL where
  language_name :: PCoClTyConsHOL2IsabelleHOL -> String
language_name PCoClTyConsHOL2IsabelleHOL = "HasCASL2IsabelleOption"

instance Comorphism PCoClTyConsHOL2IsabelleHOL
               HasCASL Sublogic
               BasicSpec Le.Sentence SymbItems SymbMapItems
               Env Morphism
               Symbol RawSymbol ()
               Isabelle () () Isa.Sentence () ()
               Isa.Sign
               IsabelleMorphism () () () where
    sourceLogic :: PCoClTyConsHOL2IsabelleHOL -> HasCASL
sourceLogic PCoClTyConsHOL2IsabelleHOL = HasCASL
HasCASL
    sourceSublogic :: PCoClTyConsHOL2IsabelleHOL -> Sublogic
sourceSublogic PCoClTyConsHOL2IsabelleHOL = Sublogic
noSubtypes
    targetLogic :: PCoClTyConsHOL2IsabelleHOL -> Isabelle
targetLogic PCoClTyConsHOL2IsabelleHOL = Isabelle
Isabelle
    mapSublogic :: PCoClTyConsHOL2IsabelleHOL -> Sublogic -> Maybe ()
mapSublogic cid :: PCoClTyConsHOL2IsabelleHOL
cid sl :: Sublogic
sl = if Sublogic
sl Sublogic -> Sublogic -> Bool
forall l. SemiLatticeWithTop l => l -> l -> Bool
`isSubElem` PCoClTyConsHOL2IsabelleHOL -> Sublogic
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid -> sublogics1
sourceSublogic PCoClTyConsHOL2IsabelleHOL
cid
                       then () -> Maybe ()
forall a. a -> Maybe a
Just () else Maybe ()
forall a. Maybe a
Nothing
    map_theory :: PCoClTyConsHOL2IsabelleHOL
-> (Env, [Named Sentence]) -> Result (Sign, [Named Sentence])
map_theory PCoClTyConsHOL2IsabelleHOL =
        SimpKind
-> Simplifier
-> (Env, [Named Sentence])
-> Result (Sign, [Named Sentence])
mapTheory (OldSimpKind -> SimpKind
Old OldSimpKind
Lift2Case) Simplifier
simpForOption
    map_sentence :: PCoClTyConsHOL2IsabelleHOL -> Env -> Sentence -> Result Sentence
map_sentence PCoClTyConsHOL2IsabelleHOL sign :: Env
sign =
        Env
-> Set String
-> SimpKind
-> Simplifier
-> Sentence
-> Result Sentence
transSentence Env
sign (Env -> Set String
typeToks Env
sign) (OldSimpKind -> SimpKind
Old OldSimpKind
Lift2Case) Simplifier
simpForOption
    isInclusionComorphism :: PCoClTyConsHOL2IsabelleHOL -> Bool
isInclusionComorphism PCoClTyConsHOL2IsabelleHOL = Bool
True
    has_model_expansion :: PCoClTyConsHOL2IsabelleHOL -> Bool
has_model_expansion PCoClTyConsHOL2IsabelleHOL = Bool
True