{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}
{- |
Module      :  ./Comorphisms/CoCFOL2IsabelleHOL.hs
Description :  Extension of CFOL2IsabelleHOL to CoCASL
Copyright   :  (c) Till Mossakowski and Uni Bremen 2003-2005
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  hausmann@informatik.uni-bremen.de
Stability   :  provisional
Portability :  non-portable (imports Logic.Logic)

The embedding comorphism from CoCASL to Isabelle-HOL.
-}

module Comorphisms.CoCFOL2IsabelleHOL (CoCFOL2IsabelleHOL (..)) where

import Logic.Logic as Logic
import Logic.Comorphism
-- CoCASL
import CoCASL.Logic_CoCASL
import CoCASL.CoCASLSign
import CoCASL.AS_CoCASL
import CoCASL.StatAna
import CoCASL.Sublogic

import CASL.Sublogic as SL
import CASL.AS_Basic_CASL
import CASL.Sign
import CASL.Morphism

import Comorphisms.CFOL2IsabelleHOL

-- Isabelle
import Isabelle.IsaSign as IsaSign
import Isabelle.IsaConsts
import Isabelle.Logic_Isabelle

import Common.Utils (number)

import Data.Char (ord, chr)
import Data.Maybe (fromMaybe)

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

instance Language CoCFOL2IsabelleHOL where
  language_name :: CoCFOL2IsabelleHOL -> String
language_name CoCFOL2IsabelleHOL = "CoCASL2Isabelle"

instance Comorphism CoCFOL2IsabelleHOL
               CoCASL CoCASL_Sublogics
               C_BASIC_SPEC CoCASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS
               CSign
               CoCASLMor
               Symbol RawSymbol ()
               Isabelle () () IsaSign.Sentence () ()
               IsaSign.Sign
               IsabelleMorphism () () () where
    sourceLogic :: CoCFOL2IsabelleHOL -> CoCASL
sourceLogic CoCFOL2IsabelleHOL = CoCASL
CoCASL
    sourceSublogic :: CoCFOL2IsabelleHOL -> CoCASL_Sublogics
sourceSublogic CoCFOL2IsabelleHOL = CoCASL_Sublogics
forall a. Lattice a => CASL_SL a
SL.cFol
    targetLogic :: CoCFOL2IsabelleHOL -> Isabelle
targetLogic CoCFOL2IsabelleHOL = Isabelle
Isabelle
    mapSublogic :: CoCFOL2IsabelleHOL -> CoCASL_Sublogics -> Maybe ()
mapSublogic cid :: CoCFOL2IsabelleHOL
cid sl :: CoCASL_Sublogics
sl = if CoCASL_Sublogics
sl CoCASL_Sublogics -> CoCASL_Sublogics -> Bool
forall l. SemiLatticeWithTop l => l -> l -> Bool
`isSubElem` CoCFOL2IsabelleHOL -> CoCASL_Sublogics
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 CoCFOL2IsabelleHOL
cid
                       then () -> Maybe ()
forall a. a -> Maybe a
Just () else Maybe ()
forall a. Maybe a
Nothing
    map_theory :: CoCFOL2IsabelleHOL
-> (CSign, [Named CoCASLFORMULA])
-> Result (Sign, [Named Sentence])
map_theory CoCFOL2IsabelleHOL =
      (Sign, [Named Sentence]) -> Result (Sign, [Named Sentence])
forall (m :: * -> *) a. Monad m => a -> m a
return ((Sign, [Named Sentence]) -> Result (Sign, [Named Sentence]))
-> ((CSign, [Named CoCASLFORMULA]) -> (Sign, [Named Sentence]))
-> (CSign, [Named CoCASLFORMULA])
-> Result (Sign, [Named Sentence])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SignTranslator C_FORMULA CoCASLSign
-> FormulaTranslator C_FORMULA CoCASLSign
-> (CSign, [Named CoCASLFORMULA])
-> (Sign, [Named Sentence])
forall f e.
FormExtension f =>
SignTranslator f e
-> FormulaTranslator f e
-> (Sign f e, [Named (FORMULA f)])
-> (Sign, [Named Sentence])
transTheory SignTranslator C_FORMULA CoCASLSign
sigTrCoCASL FormulaTranslator C_FORMULA CoCASLSign
formTrCoCASL
    map_sentence :: CoCFOL2IsabelleHOL -> CSign -> CoCASLFORMULA -> Result Sentence
map_sentence CoCFOL2IsabelleHOL sign :: CSign
sign =
      Sentence -> Result Sentence
forall (m :: * -> *) a. Monad m => a -> m a
return (Sentence -> Result Sentence)
-> (CoCASLFORMULA -> Sentence) -> CoCASLFORMULA -> Result Sentence
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FormulaTranslator C_FORMULA CoCASLSign
-> CSign -> Set String -> CoCASLFORMULA -> Sentence
forall f e.
FormulaTranslator f e
-> Sign f e -> Set String -> FORMULA f -> Sentence
mapSen FormulaTranslator C_FORMULA CoCASLSign
formTrCoCASL CSign
sign (CSign -> Set String
forall f e. Sign f e -> Set String
typeToks CSign
sign)
    has_model_expansion :: CoCFOL2IsabelleHOL -> Bool
has_model_expansion CoCFOL2IsabelleHOL = Bool
True
    is_weakly_amalgamable :: CoCFOL2IsabelleHOL -> Bool
is_weakly_amalgamable CoCFOL2IsabelleHOL = Bool
True

xvar :: Int -> String
xvar :: Int -> String
xvar i :: Int
i = if Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= 26 then [Int -> Char
chr (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Char -> Int
ord 'a')] else 'x' Char -> ShowS
forall a. a -> [a] -> [a]
: Int -> String
forall a. Show a => a -> String
show Int
i

rvar :: Int -> String
rvar :: Int -> String
rvar i :: Int
i = if Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= 9 then [Int -> Char
chr (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Char -> Int
ord 'R' )] else 'R' Char -> ShowS
forall a. a -> [a] -> [a]
: Int -> String
forall a. Show a => a -> String
show Int
i

-- | extended signature translation for CoCASL
sigTrCoCASL :: SignTranslator C_FORMULA CoCASLSign
sigTrCoCASL :: SignTranslator C_FORMULA CoCASLSign
sigTrCoCASL _ _ = (Sign, [Named Sentence]) -> (Sign, [Named Sentence])
forall a. a -> a
id

conjs :: [Term] -> Term
conjs :: [Term] -> Term
conjs l :: [Term]
l = if [Term] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Term]
l then Term
true else (Term -> Term -> Term) -> [Term] -> Term
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 Term -> Term -> Term
binConj [Term]
l

-- | extended formula translation for CoCASL
formTrCoCASL :: FormulaTranslator C_FORMULA CoCASLSign
formTrCoCASL :: FormulaTranslator C_FORMULA CoCASLSign
formTrCoCASL sign :: CSign
sign tyToks :: Set String
tyToks (CoSort_gen_ax sorts :: [SORT]
sorts ops :: [OP_SYMB]
ops _) =
  ((String, Typ) -> Term -> Term) -> Term -> [(String, Typ)] -> Term
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (String -> (String, Typ) -> Term -> Term
quantifyIsa "All") Term
phi ([(String, Typ)] -> Term) -> [(String, Typ)] -> Term
forall a b. (a -> b) -> a -> b
$ [(String, Typ)]
predDecls [(String, Typ)] -> [(String, Typ)] -> [(String, Typ)]
forall a. [a] -> [a] -> [a]
++ [("u", Typ
ts), ("v", Typ
ts)]
  where
  ts :: Typ
ts = SORT -> Typ
transSort (SORT -> Typ) -> SORT -> Typ
forall a b. (a -> b) -> a -> b
$ [SORT] -> SORT
forall a. [a] -> a
head [SORT]
sorts
  -- phi expresses: all bisimulations are the equality
  phi :: Term
phi = Term
prems Term -> Term -> Term
`binImpl` Term
concls
  -- indices and predicates for all involved sorts
  indexedSorts :: [(SORT, Int)]
indexedSorts = [SORT] -> [(SORT, Int)]
forall a. [a] -> [(a, Int)]
number [SORT]
sorts
  predDecls :: [(String, Typ)]
predDecls = ((SORT, Int) -> (String, Typ)) -> [(SORT, Int)] -> [(String, Typ)]
forall a b. (a -> b) -> [a] -> [b]
map (\ (s :: SORT
s, i :: Int
i) -> (Int -> String
rvar Int
i, SORT -> Typ
binPred SORT
s)) [(SORT, Int)]
indexedSorts
  binPred :: SORT -> Typ
binPred s :: SORT
s = let s' :: Typ
s' = SORT -> Typ
transSort SORT
s in [Typ] -> Typ -> Typ
mkCurryFunType [Typ
s', Typ
s'] Typ
boolType
  -- premises: all relations are bisimulations
  prems :: Term
prems = [Term] -> Term
conjs (((SORT, Int) -> Term) -> [(SORT, Int)] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map (SORT, Int) -> Term
prem [(SORT, Int)]
indexedSorts)
  {- generate premise for s, where s is the i-th sort
     for all x,y of that sort,
      if all sel_j(x) R_j sel_j(y), where sel_j ranges over the selectors for s
      then x R y
     here, R_i is the relation for the result type of sel_j, or the equality
  -}
  prem :: (SORT, Int) -> Term
prem (s :: SORT
s, i :: Int
i) =
    let -- get all selectors with first argument sort s
        sels :: [OP_SYMB]
sels = (OP_SYMB -> Bool) -> [OP_SYMB] -> [OP_SYMB]
forall a. (a -> Bool) -> [a] -> [a]
filter OP_SYMB -> Bool
isSelForS [OP_SYMB]
ops
        isSelForS :: OP_SYMB -> Bool
isSelForS (Qual_op_name _ t :: OP_TYPE
t _) = case OP_TYPE -> [SORT]
args_OP_TYPE OP_TYPE
t of
           s1 :: SORT
s1 : _ -> SORT
s1 SORT -> SORT -> Bool
forall a. Eq a => a -> a -> Bool
== SORT
s
           _ -> Bool
False
        isSelForS _ = Bool
False
        premSel :: OP_SYMB -> Term
premSel opsymb :: OP_SYMB
opsymb@(Qual_op_name _n :: SORT
_n t :: OP_TYPE
t _) =
         let -- get extra parameters of the selectors
             args :: [SORT]
args = [SORT] -> [SORT]
forall a. [a] -> [a]
tail ([SORT] -> [SORT]) -> [SORT] -> [SORT]
forall a b. (a -> b) -> a -> b
$ OP_TYPE -> [SORT]
args_OP_TYPE OP_TYPE
t
             indicesArgs :: [(SORT, Int)]
indicesArgs = [SORT] -> [(SORT, Int)]
forall a. [a] -> [(a, Int)]
number [SORT]
args
             res :: SORT
res = OP_TYPE -> SORT
res_OP_TYPE OP_TYPE
t
             -- variables for the extra parameters
             varDecls :: [(String, Typ)]
varDecls = ((SORT, Int) -> (String, Typ)) -> [(SORT, Int)] -> [(String, Typ)]
forall a b. (a -> b) -> [a] -> [b]
map (\ (a :: SORT
a, j :: Int
j) -> (Int -> String
xvar Int
j, SORT -> Typ
transSort SORT
a))
                        [(SORT, Int)]
indicesArgs
             -- the selector ...
             topC :: Term
topC = VName -> Term
con (CSign -> Set String -> OP_SYMB -> VName
forall f e. Sign f e -> Set String -> OP_SYMB -> VName
transOpSymb CSign
sign Set String
tyToks OP_SYMB
opsymb)
             -- applied to x and extra parameter vars
             appFold :: Term -> [Term] -> Term
appFold = (Term -> Term -> Term) -> Term -> [Term] -> Term
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Term -> Term -> Term
termAppl
             rhs :: Term
rhs = Term -> [Term] -> Term
appFold (Term -> Term -> Term
termAppl Term
topC (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ String -> Term
mkFree "x")
                       ([Term] -> Term) -> [Term] -> Term
forall a b. (a -> b) -> a -> b
$ ((SORT, Int) -> Term) -> [(SORT, Int)] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map (String -> Term
mkFree (String -> Term) -> ((SORT, Int) -> String) -> (SORT, Int) -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> String
xvar (Int -> String) -> ((SORT, Int) -> Int) -> (SORT, Int) -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SORT, Int) -> Int
forall a b. (a, b) -> b
snd) [(SORT, Int)]
indicesArgs
             -- applied to y and extra parameter vars
             lhs :: Term
lhs = Term -> [Term] -> Term
appFold (Term -> Term -> Term
termAppl Term
topC (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ String -> Term
mkFree "y")
                             ([Term] -> Term) -> [Term] -> Term
forall a b. (a -> b) -> a -> b
$ ((SORT, Int) -> Term) -> [(SORT, Int)] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map (String -> Term
mkFree (String -> Term) -> ((SORT, Int) -> String) -> (SORT, Int) -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> String
xvar (Int -> String) -> ((SORT, Int) -> Int) -> (SORT, Int) -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SORT, Int) -> Int
forall a b. (a, b) -> b
snd) [(SORT, Int)]
indicesArgs
             chi :: Term
chi = -- is the result of selector non-observable?
                   if SORT
res SORT -> [SORT] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [SORT]
sorts
                     -- then apply corresponding relation
                     then Term -> Term -> Term
termAppl (Term -> Term -> Term
termAppl (String -> Term
mkFree (String -> Term) -> String -> Term
forall a b. (a -> b) -> a -> b
$
                          Int -> String
rvar (Int -> String) -> Int -> String
forall a b. (a -> b) -> a -> b
$ Int -> Maybe Int -> Int
forall a. a -> Maybe a -> a
fromMaybe
                                   (String -> Int
forall a. HasCallStack => String -> a
error "CoCASL2Isabelle.premSel.chi")
                               (Maybe Int -> Int) -> Maybe Int -> Int
forall a b. (a -> b) -> a -> b
$ SORT -> [(SORT, Int)] -> Maybe Int
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup SORT
res [(SORT, Int)]
indexedSorts )
                               Term
rhs) Term
lhs
                     -- else use equality
                     else Term -> Term -> Term
binEq Term
rhs Term
lhs
          in ((String, Typ) -> Term -> Term) -> Term -> [(String, Typ)] -> Term
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (String -> (String, Typ) -> Term -> Term
quantifyIsa "All") Term
chi [(String, Typ)]
varDecls
        premSel _ = String -> Term
forall a. HasCallStack => String -> a
error "CoCASL2Isabelle.premSel"
        prem1 :: Term
prem1 = [Term] -> Term
conjs ((OP_SYMB -> Term) -> [OP_SYMB] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map OP_SYMB -> Term
premSel [OP_SYMB]
sels)
        concl1 :: Term
concl1 = Term -> Term -> Term
termAppl (Term -> Term -> Term
termAppl (String -> Term
mkFree (String -> Term) -> String -> Term
forall a b. (a -> b) -> a -> b
$ Int -> String
rvar Int
i) (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ String -> Term
mkFree "x")
                 (String -> Term
mkFree "y")
        psi :: Term
psi = Term
concl1 Term -> Term -> Term
`binImpl` Term
prem1
        typS :: Typ
typS = SORT -> Typ
transSort SORT
s
     in ((String, Typ) -> Term -> Term) -> Term -> [(String, Typ)] -> Term
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (String -> (String, Typ) -> Term -> Term
quantifyIsa "All") Term
psi [("x", Typ
typS), ("y", Typ
typS)]
  -- conclusion: all relations are the equality
  concls :: Term
concls = [Term] -> Term
conjs (((SORT, Int) -> Term) -> [(SORT, Int)] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map (SORT, Int) -> Term
forall a. (a, Int) -> Term
concl [(SORT, Int)]
indexedSorts)
  concl :: (a, Int) -> Term
concl (_, i :: Int
i) = Term -> Term -> Term
binImpl (Term -> Term -> Term
termAppl (Term -> Term -> Term
termAppl (String -> Term
mkFree (String -> Term) -> String -> Term
forall a b. (a -> b) -> a -> b
$ Int -> String
rvar Int
i) (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ String -> Term
mkFree "u")
                     (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ String -> Term
mkFree "v")
                             (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Term -> Term -> Term
binEq (String -> Term
mkFree "u") (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ String -> Term
mkFree "v"
formTrCoCASL _sign :: CSign
_sign _ (BoxOrDiamond _ _mod :: MODALITY
_mod _phi :: CoCASLFORMULA
_phi _) =
    String -> Term
forall a. HasCallStack => String -> a
error "CoCFOL2IsabelleHOL.formTrCoCASL.BoxOrDiamond"