{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}
{- |
Module      :  ./Comorphisms/MonadicHasCASLTranslation.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.MonadicHasCASLTranslation
    (MonadicHasCASL2IsabelleHOL (..)) 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 MonadicHasCASL2IsabelleHOL = MonadicHasCASL2IsabelleHOL deriving Int -> MonadicHasCASL2IsabelleHOL -> ShowS
[MonadicHasCASL2IsabelleHOL] -> ShowS
MonadicHasCASL2IsabelleHOL -> String
(Int -> MonadicHasCASL2IsabelleHOL -> ShowS)
-> (MonadicHasCASL2IsabelleHOL -> String)
-> ([MonadicHasCASL2IsabelleHOL] -> ShowS)
-> Show MonadicHasCASL2IsabelleHOL
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [MonadicHasCASL2IsabelleHOL] -> ShowS
$cshowList :: [MonadicHasCASL2IsabelleHOL] -> ShowS
show :: MonadicHasCASL2IsabelleHOL -> String
$cshow :: MonadicHasCASL2IsabelleHOL -> String
showsPrec :: Int -> MonadicHasCASL2IsabelleHOL -> ShowS
$cshowsPrec :: Int -> MonadicHasCASL2IsabelleHOL -> ShowS
Show

instance Language MonadicHasCASL2IsabelleHOL where
  language_name :: MonadicHasCASL2IsabelleHOL -> String
language_name MonadicHasCASL2IsabelleHOL = "MonadicTranslation"

instance Comorphism MonadicHasCASL2IsabelleHOL
               HasCASL Sublogic
               BasicSpec Le.Sentence SymbItems SymbMapItems
               Env Morphism
               Symbol RawSymbol ()
               Isabelle () () Isa.Sentence () ()
               Isa.Sign
               IsabelleMorphism () () () where
    sourceLogic :: MonadicHasCASL2IsabelleHOL -> HasCASL
sourceLogic MonadicHasCASL2IsabelleHOL = HasCASL
HasCASL
    sourceSublogic :: MonadicHasCASL2IsabelleHOL -> Sublogic
sourceSublogic MonadicHasCASL2IsabelleHOL = Sublogic
noSubtypes
    targetLogic :: MonadicHasCASL2IsabelleHOL -> Isabelle
targetLogic MonadicHasCASL2IsabelleHOL = Isabelle
Isabelle
    mapSublogic :: MonadicHasCASL2IsabelleHOL -> Sublogic -> Maybe ()
mapSublogic cid :: MonadicHasCASL2IsabelleHOL
cid sl :: Sublogic
sl = if Sublogic
sl Sublogic -> Sublogic -> Bool
forall l. SemiLatticeWithTop l => l -> l -> Bool
`isSubElem` MonadicHasCASL2IsabelleHOL -> 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 MonadicHasCASL2IsabelleHOL
cid
                       then () -> Maybe ()
forall a. a -> Maybe a
Just () else Maybe ()
forall a. Maybe a
Nothing
    map_theory :: MonadicHasCASL2IsabelleHOL
-> (Env, [Named Sentence]) -> Result (Sign, [Named Sentence])
map_theory MonadicHasCASL2IsabelleHOL =
        SimpKind
-> Simplifier
-> (Env, [Named Sentence])
-> Result (Sign, [Named Sentence])
mapTheory (OldSimpKind -> SimpKind
Old OldSimpKind
NoSimpLift) Simplifier
simpForOption
    map_sentence :: MonadicHasCASL2IsabelleHOL -> Env -> Sentence -> Result Sentence
map_sentence MonadicHasCASL2IsabelleHOL sign :: Env
sign =
        Env
-> Set String
-> SimpKind
-> Simplifier
-> Sentence
-> Result Sentence
transSentence Env
sign (Env -> Set String
typeToks Env
sign) (OldSimpKind -> SimpKind
Old OldSimpKind
NoSimpLift) Simplifier
simpForOption
    isInclusionComorphism :: MonadicHasCASL2IsabelleHOL -> Bool
isInclusionComorphism MonadicHasCASL2IsabelleHOL = Bool
True
    has_model_expansion :: MonadicHasCASL2IsabelleHOL -> Bool
has_model_expansion MonadicHasCASL2IsabelleHOL = Bool
True