4673N/A{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}

4673N/A{- |

4673N/AModule : ./Comorphisms/CFOL2IsabelleHOL.hs

4673N/ADescription : embedding from CASL (CFOL) to Isabelle-HOL

4673N/ACopyright : (c) Till Mossakowski and Uni Bremen 2003-2005

4673N/ALicense : GPLv2 or higher, see LICENSE.txt

4673N/A

4673N/AMaintainer : Christian.Maeder@dfki.de

4673N/AStability : provisional

4673N/APortability : non-portable (imports Logic.Logic)

4673N/A

4673N/AThe embedding comorphism from CASL to Isabelle-HOL.

4673N/A-}

4673N/A

4673N/Amodule Comorphisms.CFOL2IsabelleHOL

4673N/A ( CFOL2IsabelleHOL (..)

4673N/A , transTheory

4673N/A , transVar

4673N/A , typeToks

4673N/A , mapSen

4673N/A , IsaTheory

4673N/A , SignTranslator

4673N/A , FormulaTranslator

4673N/A , getAssumpsToks

4673N/A , formTrCASL

4673N/A , quantifyIsa

4673N/A , quantify

4673N/A , transFORMULA

4673N/A , transSort

4673N/A , transRecord

4673N/A , transOpSymb

4673N/A ) where

4673N/A

4673N/Aimport Logic.Logic

4673N/Aimport Logic.Comorphism

4673N/A

4673N/Aimport CASL.Logic_CASL

4673N/Aimport CASL.AS_Basic_CASL

4673N/Aimport CASL.Sublogic as SL

4673N/Aimport CASL.Sign

4673N/Aimport CASL.Morphism

4673N/Aimport CASL.Quantification

4673N/Aimport CASL.Fold

4673N/Aimport CASL.Induction

4673N/Aimport CASL.ToDoc

4673N/A

4673N/Aimport Isabelle.IsaSign as IsaSign hiding (qname)

4673N/Aimport Isabelle.IsaConsts

4673N/Aimport Isabelle.Logic_Isabelle

4673N/Aimport Isabelle.Translate

4673N/A

4673N/Aimport Common.AS_Annotation

4673N/Aimport Common.Id

4673N/Aimport Common.ProofTree

4673N/Aimport Common.Utils

4673N/Aimport qualified Common.Lib.MapSet as MapSet

4673N/A

4673N/Aimport qualified Data.Map as Map

4673N/Aimport qualified Data.Set as Set

4673N/Aimport Data.List

4673N/A

4673N/A-- | The identity of the comorphism

4673N/Adata CFOL2IsabelleHOL = CFOL2IsabelleHOL deriving Show

4673N/A

4673N/A-- Isabelle theories

4673N/Atype IsaTheory = (IsaSign.Sign, [Named IsaSign.Sentence])

4673N/A

4673N/A-- extended signature translation

4673N/Atype SignTranslator f e = CASL.Sign.Sign f e -> e -> IsaTheory -> IsaTheory

4673N/A

4673N/A-- extended signature translation for CASL

4673N/AsigTrCASL :: SignTranslator () ()

4673N/AsigTrCASL _ _ = id

4673N/A

4673N/A-- extended formula translation

4673N/Atype FormulaTranslator f e = CASL.Sign.Sign f e -> Set.Set String -> f -> Term

4673N/A

4673N/A-- extended formula translation for CASL

4673N/AformTrCASL :: FormulaTranslator () ()

4673N/AformTrCASL _ _ = error "CFOL2IsabelleHOL: No extended formulas allowed in CASL"

4673N/A

4673N/Ainstance Language CFOL2IsabelleHOL where

4673N/A language_name CFOL2IsabelleHOL = "CASL2Isabelle"

4673N/A

4673N/Ainstance Comorphism CFOL2IsabelleHOL

4673N/A CASL CASL_Sublogics

4673N/A CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS

4673N/A CASLSign

4673N/A CASLMor

4673N/A Symbol RawSymbol ProofTree

4673N/A Isabelle () () IsaSign.Sentence () ()

4673N/A IsaSign.Sign

4673N/A IsabelleMorphism () () () where

4673N/A sourceLogic CFOL2IsabelleHOL = CASL

4673N/A sourceSublogic CFOL2IsabelleHOL = SL.cFol

4673N/A targetLogic CFOL2IsabelleHOL = Isabelle

4673N/A mapSublogic cid sl = if sl `isSubElem` sourceSublogic cid

4673N/A then Just () else Nothing

4673N/A map_theory CFOL2IsabelleHOL = return . transTheory sigTrCASL formTrCASL

4673N/A map_sentence CFOL2IsabelleHOL sign =

4673N/A return . mapSen formTrCASL sign (typeToks sign)

4673N/A has_model_expansion CFOL2IsabelleHOL = True

4673N/A is_weakly_amalgamable CFOL2IsabelleHOL = True

4673N/A isInclusionComorphism CFOL2IsabelleHOL = True

4673N/A

4673N/A-- -------------------------- Signature -----------------------------

4673N/AbaseSign :: BaseSig

4673N/AbaseSign = Main_thy

4673N/A

4673N/AtypeToks :: CASL.Sign.Sign f e -> Set.Set String

4673N/AtypeToks = Set.map (`showIsaTypeT` baseSign) . sortSet

4673N/A

4673N/AtransTheory :: FormExtension f => SignTranslator f e ->

4673N/A FormulaTranslator f e ->

4673N/A (CASL.Sign.Sign f e, [Named (FORMULA f)])

4673N/A -> IsaTheory

4673N/AtransTheory trSig trForm (sign, sens) =

4673N/A trSig sign (extendedInfo sign) (IsaSign.emptySign {

4673N/A baseSig = baseSign,

4673N/A tsig = emptyTypeSig {arities =

4673N/A Set.fold (\ s -> let s1 = showIsaTypeT s baseSign in

4673N/A Map.insert s1 [(isaTerm, [])])

4673N/A Map.empty (sortSet sign)},

4673N/A constTab = Map.foldWithKey insertPreds

4673N/A (Map.foldWithKey insertOps Map.empty

4673N/A . MapSet.toMap $ opMap sign) . MapSet.toMap $ predMap sign,

4673N/A domainTab = dtDefs},

4673N/A map (\ (s, n) -> makeNamed ("ga_induction_" ++ show n) $ myMapSen s)

4673N/A (number gens) ++

4673N/A map (mapNamed myMapSen) real_sens)

4673N/A -- for now, no new sentences

4673N/A where

gens =

map (inductionScheme . fst) genTypes

tyToks = typeToks sign

myMapSen = mkSen . transFORMULA sign tyToks trForm (getAssumpsToks sign)

(real_sens, sort_gen_axs) = foldr ( \ s (rs, cs) -> case sentence s of

Sort_gen_ax c b -> (rs, (c, b) : cs)

_ -> (s : rs, cs)) ([], []) sens

unique_sort_gen_axs = nubOrdOn (Set.fromList . map newSort . fst)

sort_gen_axs

(freeTypes, genTypes) = partition snd unique_sort_gen_axs

dtDefs = makeDtDefs sign tyToks $ map fst freeTypes

ga = globAnnos sign

insertOps op ts m = if isSingleton ts then

let t = Set.findMin ts in Map.insert

(mkIsaConstT False ga (length $ opArgs t) op baseSign tyToks)

(transOpType t) m

else foldl (\ m1 (t, i) -> Map.insert

(mkIsaConstIT False ga (length $ opArgs t) op i baseSign tyToks)

(transOpType t) m1) m $ number $ Set.toList ts

insertPreds pre ts m = if isSingleton ts then

let t = Set.findMin ts in Map.insert

(mkIsaConstT True ga (length $ predArgs t) pre baseSign tyToks)

(transPredType t) m

else foldl (\ m1 (t, i) -> Map.insert

(mkIsaConstIT True ga (length $ predArgs t) pre i baseSign tyToks)

(transPredType t) m1) m $ number $ Set.toList ts

makeDtDefs :: CASL.Sign.Sign f e -> Set.Set String -> [[Constraint]]

-> [[(Typ, [(VName, [Typ])])]]

makeDtDefs sign = map . makeDtDef sign

makeDtDef :: CASL.Sign.Sign f e -> Set.Set String -> [Constraint]

-> [(Typ, [(VName, [Typ])])]

makeDtDef sign tyToks constrs = map makeDt srts where

(srts, ops, _maps) = recover_Sort_gen_ax constrs

makeDt s = (transSort s, map makeOp (filter (hasTheSort s) ops))

makeOp opSym = (transOpSymb sign tyToks opSym, transArgs opSym)

hasTheSort s (Qual_op_name _ ot _) = s == res_OP_TYPE ot

hasTheSort _ _ = error "CFOL2IsabelleHOL.hasTheSort"

transArgs (Qual_op_name _ ot _) = map transSort $ args_OP_TYPE ot

transArgs _ = error "CFOL2IsabelleHOL.transArgs"

transSort :: SORT -> Typ

transSort s = Type (showIsaTypeT s baseSign) [] []

transOpType :: OpType -> Typ

transOpType ot = mkCurryFunType (map transSort $ opArgs ot)

$ transSort (opRes ot)

transPredType :: PredType -> Typ

transPredType pt = mkCurryFunType (map transSort $ predArgs pt) boolType

-- ---------------------------- Formulas ------------------------------

getAssumpsToks :: CASL.Sign.Sign f e -> Set.Set String

getAssumpsToks sign = Map.foldWithKey ( \ i ops s ->

Set.union s $ Set.unions

$ map ( \ (_, o) -> getConstIsaToks i o baseSign)

$ number $ Set.toList ops)

(Map.foldWithKey ( \ i prds s ->

Set.union s $ Set.unions

$ map ( \ (_, o) -> getConstIsaToks i o baseSign)

$ number $ Set.toList prds) Set.empty . MapSet.toMap

$ predMap sign)

. MapSet.toMap $ opMap sign

transVar :: Set.Set String -> VAR -> String

transVar toks v = let

s = showIsaConstT (simpleIdToId v) baseSign

renVar t = if Set.member t toks then renVar $ "X_" ++ t else t

in renVar s

quantifyIsa :: String -> (String, Typ) -> Term -> Term

quantifyIsa q (v, _) phi =

termAppl (conDouble q) (Abs (mkFree v) phi NotCont)

quantify :: Set.Set String -> QUANTIFIER -> (VAR, SORT) -> Term -> Term

quantify toks q (v, t) =

quantifyIsa (qname q) (transVar toks v, transSort t)

where

qname Universal = allS

qname Existential = exS

qname Unique_existential = ex1S

transOpSymb :: CASL.Sign.Sign f e -> Set.Set String -> OP_SYMB -> VName

transOpSymb sign tyToks qo = case qo of

Qual_op_name op ot _ -> let

ga = globAnnos sign

l = length $ args_OP_TYPE ot

in case Set.toList . MapSet.lookup op $ opMap sign of

[] -> error $ "CASL2Isabelle unknown op: " ++ show op

[_] -> mkIsaConstT False ga l op baseSign tyToks

ots -> case elemIndex (toOpType ot) ots of

Just i -> mkIsaConstIT False ga l op (i + 1) baseSign tyToks

Nothing -> error $ "CASL2Isabelle unknown type for op: " ++ show op

Op_name op -> error $ "CASL2Isabelle: unqualified op: " ++ show op

transPredSymb :: CASL.Sign.Sign f e -> Set.Set String -> PRED_SYMB -> VName

transPredSymb sign tyToks qp =

let ga = globAnnos sign

d = mkIsaConstT True ga (-1) (predSymbName qp) baseSign tyToks

-- for predicate names in induction schemes

in case qp of

Qual_pred_name p pt@(Pred_type args _) _ -> let

l = length args

in case Set.toList . MapSet.lookup p $ predMap sign of

[] -> d

[_] -> mkIsaConstT True ga l p baseSign tyToks

pts -> case elemIndex (toPredType pt) pts of

Just i -> mkIsaConstIT True ga l p (i + 1) baseSign tyToks

Nothing -> d

Pred_name _ -> d

mapSen :: FormulaTranslator f e -> CASL.Sign.Sign f e -> Set.Set String

-> FORMULA f -> Sentence

mapSen trForm sign tyToks =

mkSen . transFORMULA sign tyToks trForm (getAssumpsToks sign)

transRecord :: CASL.Sign.Sign f e -> Set.Set String -> FormulaTranslator f e

-> Set.Set String -> Record f Term Term

transRecord sign tyToks tr toks = Record

{ foldQuantification = \ _ qu vdecl phi _ ->

foldr (quantify toks qu) phi (flatVAR_DECLs vdecl)

, foldJunction = \ _ j phis _ -> let

(n, op) = case j of

Con -> (true, binConj)

Dis -> (false, binDisj)

in if null phis then n else foldr1 op phis

, foldRelation = \ _ phi1 c phi2 _ -> (if c == Equivalence

then binEqv else binImpl) phi1 phi2

, foldNegation = \ _ phi _ -> termAppl notOp phi

, foldAtom = \ _ b _ -> if b then true else false

, foldPredication = \ _ psymb args _ ->

foldl termAppl (con $ transPredSymb sign tyToks psymb) args

, foldDefinedness = \ _ _ _ -> true -- totality assumed

, foldEquation = \ _ t1 _ t2 _ -> binEq t1 t2 -- equal types assumed

, foldMembership = \ _ _ _ _ -> true -- no subsorting assumed

, foldMixfix_formula = error "transRecord: Mixfix_formula"

, foldSort_gen_ax = error "transRecord: Sort_gen_ax"

, foldQuantOp = error "transRecord: QuantOp"

, foldQuantPred = error "transRecord: QuantPred"

, foldExtFORMULA = \ _ -> tr sign tyToks

, foldQual_var = \ _ v _ _ -> mkFree $ transVar toks v

, foldApplication = \ _ opsymb args _ ->

foldl termAppl (con $ transOpSymb sign tyToks opsymb) args

, foldSorted_term = \ _ t _ _ -> t -- no subsorting assumed

, foldCast = \ _ t _ _ -> t -- no subsorting assumed

, foldConditional = \ _ t1 phi t2 _ -> -- equal types assumed

If phi t1 t2 NotCont

, foldMixfix_qual_pred = error "transRecord: Mixfix_qual_pred"

, foldMixfix_term = error "transRecord: Mixfix_term"

, foldMixfix_token = error "transRecord: Mixfix_token"

, foldMixfix_sorted_term = error "transRecord: Mixfix_sorted_term"

, foldMixfix_cast = error "transRecord: Mixfix_cast"

, foldMixfix_parenthesized = error "transRecord: Mixfix_parenthesized"

, foldMixfix_bracketed = error "transRecord: Mixfix_bracketed"

, foldMixfix_braced = error "transRecord: Mixfix_braced"

, foldExtTERM = error "transRecord: ExtTERM"

}

transFORMULA :: CASL.Sign.Sign f e -> Set.Set String -> FormulaTranslator f e

-> Set.Set String -> FORMULA f -> Term

transFORMULA sign tyToks tr = foldFormula . transRecord sign tyToks tr