{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}

{- |

Module : $Header$

Description : direct comorphism from CommonLogic to Isabelle-HOL

Copyright : (c) Soeren Schulze, Uni Bremen 2012

License : GPLv2 or higher, see LICENSE.txt

Maintainer : s.schulze@uni-bremen.de

Stability : experimental

Portability : non-portable (imports Logic.Logic)

A direct comorphism from CommonLogic to Isabelle-HOL, passing arguments as

native Isabelle lists.

-}

module Comorphisms.CommonLogic2IsabelleHOL where

import qualified Data.Set as Set

import qualified Data.Map as Map

import Data.Maybe (fromMaybe)

import Logic.Logic

import Logic.Comorphism

import Common.ProofTree

import Common.Result

import Common.AS_Annotation as AS_Anno

import qualified Common.Id as Id

import Common.GlobalAnnotations (emptyGlobalAnnos)

import qualified CommonLogic.Logic_CommonLogic as ClLogic

import qualified CommonLogic.AS_CommonLogic as ClBasic

import qualified CommonLogic.Sign as ClSign

import qualified CommonLogic.Symbol as ClSymbol

import qualified CommonLogic.Morphism as ClMor

import qualified CommonLogic.Sublogic as ClSl

import CommonLogic.ModuleElimination

import Isabelle.IsaSign hiding (qname)

import Isabelle.IsaConsts

import Isabelle.Logic_Isabelle

import Isabelle.Translate

data CommonLogic2IsabelleHOL = CommonLogic2IsabelleHOL deriving Show

instance Language CommonLogic2IsabelleHOL where

language_name CommonLogic2IsabelleHOL = "CommonLogic2Isabelle"

instance Comorphism

CommonLogic2IsabelleHOL -- comorphism

ClLogic.CommonLogic -- lid domain

ClSl.CommonLogicSL -- sublogics codomain

ClBasic.BASIC_SPEC -- Basic spec domain

ClBasic.TEXT_META -- sentence domain

ClBasic.SYMB_ITEMS -- symbol items domain

ClBasic.SYMB_MAP_ITEMS -- symbol map items domain

ClSign.Sign -- signature domain

ClMor.Morphism -- morphism domain

ClSymbol.Symbol -- symbol domain

ClSymbol.Symbol -- rawsymbol domain

ProofTree -- proof tree codomain

Isabelle -- lid codomain

() -- sublogics codomain [none]

() -- Basic spec codomain [none]

Sentence -- sentence codomain

() -- symbol items codomain [none]

() -- symbol map items codomain [none]

Sign -- signature codomain

IsabelleMorphism -- morphism codomain

() -- symbol codomain [none]

() -- rawsymbol codomain [none]

() -- proof tree domain [none]

where

sourceLogic CommonLogic2IsabelleHOL = ClLogic.CommonLogic

sourceSublogic CommonLogic2IsabelleHOL = ClSl.top

targetLogic CommonLogic2IsabelleHOL = Isabelle

map_theory CommonLogic2IsabelleHOL = mapTheory

map_sentence CommonLogic2IsabelleHOL = mapSentence

has_model_expansion CommonLogic2IsabelleHOL = True

is_weakly_amalgamable CommonLogic2IsabelleHOL = True

isInclusionComorphism CommonLogic2IsabelleHOL = True

mapSentence :: ClSign.Sign -> ClBasic.TEXT_META -> Result Sentence

mapSentence sig = return . mkSen . transTextMeta sig

mapTheory :: (ClSign.Sign, [AS_Anno.Named ClBasic.TEXT_META])

-> Result (Sign, [AS_Anno.Named Sentence])

mapTheory (sig, namedTextMetas) =

return (mapSig sig, ax_that : map (transNamed sig) namedTextMetas)

individualS :: String

individualS = "individual"

individualT :: Typ

individualT = mkSType individualS

ax_that :: AS_Anno.Named Sentence

ax_that = makeNamed "Ax_that" $ forceSimp $ mkSen $

termAppl (conDouble "ALL") (Abs senTrm s NotCont)

where s = binEqv senTrm

(binVNameAppl

relSymb (termAppl (con thatSymb) senTrm) (nilPT NotCont))

senTrm = conDouble "sen"

forceSimp sen = sen { isSimp = True }

type RENAMES = Map.Map String VName

mkIndName :: String -> VName

mkIndName name = mkIsaConstT True emptyGlobalAnnos (-1)

(Id.stringToId name) Main_thy Set.empty

addRenames :: RENAMES -> [String] -> RENAMES

addRenames = foldr

(\ k m -> let k' = unclash k m

v = mkIndName k' in

Map.insert k v $ Map.insert k' v m)

where unclash k m = if Map.member k m

then unclash ("X_" ++ k) m

else k

makeRenames :: [String] -> RENAMES

makeRenames = addRenames Map.empty

basicRenames :: ClSign.Sign -> RENAMES

basicRenames sig = addRenames

(Map.fromList [("rel", relSymb), ("fun", funSymb),

("that", thatSymb)])

(map (Id.tokStr . Id.idToSimpleId)

( Set.toList (ClSign.sequenceMarkers sig)

++ Set.toList (ClSign.discourseNames sig)))

rename :: RENAMES -> String -> VName

rename rn s = fromMaybe (error $ "Symbol " ++ show s ++ "not found") $

Map.lookup s rn

mapSig :: ClSign.Sign -> Sign

mapSig sig = emptySign {

tsig = emptyTypeSig {

arities = Map.singleton individualS [(isaTerm, [])]

},

constTab = Map.insert relSymb

(mkCurryFunType [individualT, mkListType individualT] boolType) $

Map.insert funSymb

(mkCurryFunType [individualT, mkListType individualT] individualT) $

Map.insert thatSymb

(mkCurryFunType [boolType] individualT) $

Map.union (Map.fromList

(map ((\ name -> (rename rn name, individualT)) .

Id.tokStr . Id.idToSimpleId) $ Set.toList $

ClSign.discourseNames sig))

(Map.fromList

(map ((\ name -> (rename rn name, mkListType individualT)) .

Id.tokStr . Id.idToSimpleId) $ Set.toList $

ClSign.sequenceMarkers sig))

}

where rn = basicRenames sig

relSymb, funSymb, thatSymb :: VName

relSymb = mkIsaConstT True emptyGlobalAnnos 2

(Id.stringToId "rel")

Main_thy Set.empty

funSymb = mkIsaConstT False emptyGlobalAnnos 2

(Id.stringToId "fun")

Main_thy Set.empty

thatSymb = mkIsaConstT False emptyGlobalAnnos 1

(Id.stringToId "that")

Main_thy Set.empty

quantify :: RENAMES -> ClBasic.QUANT -> String -> Term -> Term

quantify rn q v s = termAppl (conDouble $ qname q)

(Abs (con $ rename rn v) s NotCont)

where qname ClBasic.Universal = allS

qname ClBasic.Existential = exS

transTextMeta :: ClSign.Sign -> ClBasic.TEXT_META -> Term

transTextMeta sig = transText renames . ClBasic.getText . eliminateModules

where renames = basicRenames sig

transNamed :: ClSign.Sign -> AS_Anno.Named ClBasic.TEXT_META

-> AS_Anno.Named Sentence

transNamed sig = AS_Anno.mapNamed $ mkSen . transTextMeta sig

transText :: RENAMES -> ClBasic.TEXT -> Term

transText rn txt = case txt of

ClBasic.Text phrs _ ->

let phrs' = filter nonImport phrs

in if null phrs' then true

else foldl1 binConj (map (transPhrase rn) phrs')

ClBasic.Named_text _ t _ -> transText rn t

where nonImport p = case p of

ClBasic.Importation _ -> False

_ -> True

transPhrase :: RENAMES -> ClBasic.PHRASE -> Term

transPhrase rn phr = case phr of

ClBasic.Module _ -> error "transPhase: \"module\" found"

ClBasic.Sentence s -> transSen rn s

ClBasic.Importation _ -> error "transPhase: \"import\" found"

ClBasic.Comment_text _ t _ -> transText rn t

transTerm :: RENAMES -> ClBasic.TERM -> Term

transTerm rn trm = case trm of

ClBasic.Name_term name -> con $ rename rn (Id.tokStr name)

ClBasic.Funct_term op args _ -> applyTermSeq funSymb rn op args

ClBasic.Comment_term t _ _ -> transTerm rn t

ClBasic.That_term sen _ -> termAppl (con thatSymb) (transSen rn sen)

transNameOrSeqmark :: ClBasic.NAME_OR_SEQMARK -> String

transNameOrSeqmark ts = Id.tokStr $ case ts of

ClBasic.Name name -> name

ClBasic.SeqMark seqm -> seqm

transTermSeq :: RENAMES -> ClBasic.TERM_SEQ -> Term

transTermSeq rn ts = case ts of

ClBasic.Term_seq trm -> (termAppl . termAppl (conC consV))

(transTerm rn trm) (nilPT NotCont)

ClBasic.Seq_marks seqm -> con $ rename rn (Id.tokStr seqm)

{- applicable for a non-empty argument list where only the last argument

(or none) is a seqmark -}

transArgsSimple :: RENAMES -> [ClBasic.TERM_SEQ] -> Maybe Term

transArgsSimple rn tss =

foldr

(\ ts trm ->

do trm' <- trm

case ts of

ClBasic.Term_seq clTrm ->

Just $ (termAppl . termAppl (conC consV)) (transTerm rn clTrm) trm'

_ -> Nothing)

(Just $ transTermSeq rn $ last tss)

(init tss)

transArgs :: RENAMES -> [ClBasic.TERM_SEQ] -> Term

transArgs rn tss = case (tss, transArgsSimple rn tss) of

([], _) -> nilPT NotCont

(_, Just trm) -> trm

(_, Nothing) -> foldr1 (termAppl . termAppl (con appendV))

(map (transTermSeq rn) tss)

applyTermSeq :: VName -> RENAMES -> ClBasic.TERM -> [ClBasic.TERM_SEQ] -> Term

applyTermSeq metaSymb rn clTrm clArgs = binVNameAppl metaSymb trm args

where trm = transTerm rn clTrm

args = transArgs rn clArgs

transSen :: RENAMES -> ClBasic.SENTENCE -> Term

transSen rn sen = case sen of

ClBasic.Bool_sent bs _ -> case bs of

ClBasic.Negation s -> termAppl notOp (transSen rn s)

ClBasic.Junction j ss ->

if null ss then true

else foldr1 (case j of ClBasic.Conjunction -> binConj

ClBasic.Disjunction -> binDisj)

(map (transSen rn) ss)

ClBasic.BinOp j s1 s2 ->

(case j of ClBasic.Implication -> binImpl

ClBasic.Biconditional -> binEqv)

(transSen rn s1) (transSen rn s2)

ClBasic.Quant_sent q bs s _ -> foldr (quantify rn' q) (transSen rn' s) varNames

where rn' = addRenames rn varNames

varNames = map transNameOrSeqmark bs

ClBasic.Atom_sent at _ -> case at of

ClBasic.Equation t1 t2 -> binEq (transTerm rn t1) (transTerm rn t2)

ClBasic.Atom p args -> applyTermSeq relSymb rn p args

ClBasic.Comment_sent _ s _ -> transSen rn s

ClBasic.Irregular_sent s _ -> transSen rn s