020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}

12b2ae689353ecbaad720a9af9f9be01c1a3fe2dChristian Maeder{- |

e071fb22ea9923a2a4ff41184d80ca46b55ee932Till MossakowskiModule : $Header$

020cdb5dad6b871aba61136a0e1567c00426de87Andy GimblettDescription : old translation that is only better for case terms

98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuCopyright : (c) Sonja Groening, C. Maeder, Uni Bremen 2003-2006

020cdb5dad6b871aba61136a0e1567c00426de87Andy GimblettLicense : GPLv2 or higher, see LICENSE.txt

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett

020cdb5dad6b871aba61136a0e1567c00426de87Andy GimblettMaintainer : Christian.Maeder@dfki.de

020cdb5dad6b871aba61136a0e1567c00426de87Andy GimblettStability : provisional

020cdb5dad6b871aba61136a0e1567c00426de87Andy GimblettPortability : non-portable (imports Logic.Logic)

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett

020cdb5dad6b871aba61136a0e1567c00426de87Andy GimblettThis embedding comorphism from HasCASL to Isabelle-HOL is an old

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblettversion that can be deleted as soon as case terms are implemented elsewhere

9ebbce450fb242e1a346f9f89367d8c46fcb2ec8Andy Gimblett-}

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett

576a4ca6de740c90afd448607c2323477139de24Liam O'Reillymodule Comorphisms.HasCASL2IsabelleHOL where

9f93b2a8b552789cd939d599504d39732672dc84Christian Maeder

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblettimport Logic.Logic as Logic

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblettimport Logic.Comorphism

05b3e12808da901dccd665715cb934462290d550Andy Gimblett

9ebbce450fb242e1a346f9f89367d8c46fcb2ec8Andy Gimblettimport HasCASL.Logic_HasCASL

aa0d5f8be9950e788884f7431cf4cb7bee74788cAndy Gimblettimport HasCASL.Sublogic

aa0d5f8be9950e788884f7431cf4cb7bee74788cAndy Gimblettimport HasCASL.Le as Le

9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reillyimport HasCASL.As as As

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblettimport HasCASL.AsUtils

12b2ae689353ecbaad720a9af9f9be01c1a3fe2dChristian Maederimport HasCASL.Builtin

12b2ae689353ecbaad720a9af9f9be01c1a3fe2dChristian Maeder

567db7182e691cce5816365d8c912d09ffe92f86Andy Gimblettimport Isabelle.IsaSign as IsaSign

12b2ae689353ecbaad720a9af9f9be01c1a3fe2dChristian Maederimport Isabelle.IsaConsts

12b2ae689353ecbaad720a9af9f9be01c1a3fe2dChristian Maederimport Isabelle.Logic_Isabelle

12b2ae689353ecbaad720a9af9f9be01c1a3fe2dChristian Maederimport Isabelle.Translate

12b2ae689353ecbaad720a9af9f9be01c1a3fe2dChristian Maeder

12b2ae689353ecbaad720a9af9f9be01c1a3fe2dChristian Maederimport Common.DocUtils

8db2221917c1bc569614f3481bcdb3b988facaedChristian Maederimport Common.Id

12b2ae689353ecbaad720a9af9f9be01c1a3fe2dChristian Maederimport Common.Result

8db2221917c1bc569614f3481bcdb3b988facaedChristian Maederimport Common.Utils

12b2ae689353ecbaad720a9af9f9be01c1a3fe2dChristian Maederimport qualified Data.Map as Map

1c7c4d95775a8ad5f7373e5cf0bad86f8301c56cAndy Gimblettimport qualified Data.Set as Set

9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reillyimport Common.AS_Annotation

9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly

9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reillyimport Data.List (elemIndex)

9f93b2a8b552789cd939d599504d39732672dc84Christian Maederimport Data.Maybe (catMaybes)

9f93b2a8b552789cd939d599504d39732672dc84Christian Maeder

9f93b2a8b552789cd939d599504d39732672dc84Christian Maeder-- | The identity of the comorphism

9f93b2a8b552789cd939d599504d39732672dc84Christian Maederdata HasCASL2IsabelleHOL = HasCASL2IsabelleHOL deriving Show

dd7da1b5fedc05b92ba023ebd803e6f4a662503bChristian Maeder

dd7da1b5fedc05b92ba023ebd803e6f4a662503bChristian Maederinstance Language HasCASL2IsabelleHOL where

dd7da1b5fedc05b92ba023ebd803e6f4a662503bChristian Maeder language_name HasCASL2IsabelleHOL = "HasCASL2IsabelleDeprecated"

9f93b2a8b552789cd939d599504d39732672dc84Christian Maeder

9f93b2a8b552789cd939d599504d39732672dc84Christian Maederinstance Comorphism HasCASL2IsabelleHOL

dd7da1b5fedc05b92ba023ebd803e6f4a662503bChristian Maeder HasCASL Sublogic

9f93b2a8b552789cd939d599504d39732672dc84Christian Maeder BasicSpec Le.Sentence SymbItems SymbMapItems

9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly Env Morphism

0b8146e4f675518993a34eb2255ad7ddd7bf82a4Christian Maeder Symbol RawSymbol ()

23a073e0a3433ca80a286d46202841b569ec36fdChristian Maeder Isabelle () () IsaSign.Sentence () ()

05cc55892e6c93bdd7b9c3f100ab1bb65fe6a21eLiam O'Reilly IsaSign.Sign

05cc55892e6c93bdd7b9c3f100ab1bb65fe6a21eLiam O'Reilly IsabelleMorphism () () () where

1c7c4d95775a8ad5f7373e5cf0bad86f8301c56cAndy Gimblett sourceLogic HasCASL2IsabelleHOL = HasCASL

53f89daf88665d3ea96d871110a5c0d9d8326bd2Andy Gimblett sourceSublogic HasCASL2IsabelleHOL = sublogic_min noSubtypes noClasses

1c7c4d95775a8ad5f7373e5cf0bad86f8301c56cAndy Gimblett targetLogic HasCASL2IsabelleHOL = Isabelle

1c7c4d95775a8ad5f7373e5cf0bad86f8301c56cAndy Gimblett mapSublogic cid sl = if sl `isSubElem` sourceSublogic cid

53f89daf88665d3ea96d871110a5c0d9d8326bd2Andy Gimblett then Just () else Nothing

53f89daf88665d3ea96d871110a5c0d9d8326bd2Andy Gimblett map_theory HasCASL2IsabelleHOL = mkTheoryMapping transSignature

12b2ae689353ecbaad720a9af9f9be01c1a3fe2dChristian Maeder (map_sentence HasCASL2IsabelleHOL)

1c7c4d95775a8ad5f7373e5cf0bad86f8301c56cAndy Gimblett map_sentence HasCASL2IsabelleHOL sign phi =

c052e3ee4a53ee3a2da829aa142fd596ef6c9e3dAndy Gimblett case transSentence sign phi of

c052e3ee4a53ee3a2da829aa142fd596ef6c9e3dAndy Gimblett Nothing -> warning (mkSen true)

1c7c4d95775a8ad5f7373e5cf0bad86f8301c56cAndy Gimblett "translation of sentence not implemented" nullRange

b25c72845890740c2f8a21214752574990b943cfChristian Maeder Just (ts) -> return $ mkSen ts

b25c72845890740c2f8a21214752574990b943cfChristian Maeder isInclusionComorphism HasCASL2IsabelleHOL = True

b25c72845890740c2f8a21214752574990b943cfChristian Maeder

c052e3ee4a53ee3a2da829aa142fd596ef6c9e3dAndy Gimblett-- * Signature

a09bfcbcb0fba5663fca1968aa82daebf2e092c4Andy GimblettbaseSign :: BaseSig

a5f3a8cdc3ceb045c3c166ee840d3e59ec7efac6Christian MaederbaseSign = MainHC_thy

dfc58f5ec6492d1a9b9babd9cdcdbb15baa6e657Christian Maeder

a5f3a8cdc3ceb045c3c166ee840d3e59ec7efac6Christian MaedertransSignature :: Env -> Result (IsaSign.Sign,[Named IsaSign.Sentence])

a5f3a8cdc3ceb045c3c166ee840d3e59ec7efac6Christian MaedertransSignature sign =

dfc58f5ec6492d1a9b9babd9cdcdbb15baa6e657Christian Maeder return (IsaSign.emptySign {

b25c72845890740c2f8a21214752574990b943cfChristian Maeder baseSig = baseSign,

1c7c4d95775a8ad5f7373e5cf0bad86f8301c56cAndy Gimblett -- translation of typeconstructors

61051521e4d82769a47f23aecb5fb477de47d534Andy Gimblett tsig = emptyTypeSig

61051521e4d82769a47f23aecb5fb477de47d534Andy Gimblett { arities = Map.foldWithKey extractTypeName

61051521e4d82769a47f23aecb5fb477de47d534Andy Gimblett Map.empty

61051521e4d82769a47f23aecb5fb477de47d534Andy Gimblett (typeMap sign) },

61051521e4d82769a47f23aecb5fb477de47d534Andy Gimblett -- translation of operation declarations

b25c72845890740c2f8a21214752574990b943cfChristian Maeder constTab = Map.foldWithKey insertOps

1c7c4d95775a8ad5f7373e5cf0bad86f8301c56cAndy Gimblett Map.empty

b22c258cca179a5ffe777b64b32e10687c5f6b2cAndy Gimblett (assumps sign),

a5f3a8cdc3ceb045c3c166ee840d3e59ec7efac6Christian Maeder -- translation of datatype declarations

23a073e0a3433ca80a286d46202841b569ec36fdChristian Maeder domainTab = transDatatype (typeMap sign),

23a073e0a3433ca80a286d46202841b569ec36fdChristian Maeder showLemmas = True },

876bd2c70a93981cc80f8376284616bce4a0fefcChristian Maeder [] )

aa0d5f8be9950e788884f7431cf4cb7bee74788cAndy Gimblett where

aa0d5f8be9950e788884f7431cf4cb7bee74788cAndy Gimblett extractTypeName tyId typeInfo m =

aa0d5f8be9950e788884f7431cf4cb7bee74788cAndy Gimblett if isDatatypeDefn typeInfo then m

aa0d5f8be9950e788884f7431cf4cb7bee74788cAndy Gimblett else Map.insert (showIsaTypeT tyId baseSign) [(isaTerm, [])] m

afc52bfaabee38c4d55cee9f35b1a0028ba3854aAndy Gimblett -- translate the kind here!

afc52bfaabee38c4d55cee9f35b1a0028ba3854aAndy Gimblett isDatatypeDefn t = case typeDefn t of

197888c54795ec1e79e77289b7e20436a6db74c0Andy Gimblett DatatypeDefn _ -> True

197888c54795ec1e79e77289b7e20436a6db74c0Andy Gimblett _ -> False

197888c54795ec1e79e77289b7e20436a6db74c0Andy Gimblett insertOps name ops m =

b25c72845890740c2f8a21214752574990b943cfChristian Maeder if isSingleton ops then

b25c72845890740c2f8a21214752574990b943cfChristian Maeder let transOp = transOpInfo (Set.findMin ops)

a1f6118e7ce7f8892fc4299e316630ec74083f0aAndy Gimblett in case transOp of

b25c72845890740c2f8a21214752574990b943cfChristian Maeder Just op ->

afc52bfaabee38c4d55cee9f35b1a0028ba3854aAndy Gimblett Map.insert (mkVName $ showIsaConstT name baseSign) op m

fcd11c35e645b0744a308f7961a519826bbaa2f5Christian Maeder Nothing -> m

b25c72845890740c2f8a21214752574990b943cfChristian Maeder else

4f4e94264f48e255d4125f47649f585d9d062fabChristian Maeder let transOps = map transOpInfo $ Set.toList ops

4f4e94264f48e255d4125f47649f585d9d062fabChristian Maeder in foldl (\ m' (transOp,i) ->

afc52bfaabee38c4d55cee9f35b1a0028ba3854aAndy Gimblett case transOp of

4f4e94264f48e255d4125f47649f585d9d062fabChristian Maeder Just ty -> Map.insert

4f4e94264f48e255d4125f47649f585d9d062fabChristian Maeder (mkVName $ showIsaConstIT name i baseSign)

b25c72845890740c2f8a21214752574990b943cfChristian Maeder ty m'

4f4e94264f48e255d4125f47649f585d9d062fabChristian Maeder Nothing -> m')

afc52bfaabee38c4d55cee9f35b1a0028ba3854aAndy Gimblett m $ number transOps

fcd11c35e645b0744a308f7961a519826bbaa2f5Christian Maeder

4f4e94264f48e255d4125f47649f585d9d062fabChristian Maeder-- * translation of a type in an operation declaration

4f4e94264f48e255d4125f47649f585d9d062fabChristian Maeder

4f4e94264f48e255d4125f47649f585d9d062fabChristian Maeder-- extract type from OpInfo

afc52bfaabee38c4d55cee9f35b1a0028ba3854aAndy Gimblett-- omit datatype constructors

b25c72845890740c2f8a21214752574990b943cfChristian MaedertransOpInfo :: OpInfo -> Maybe Typ

4f4e94264f48e255d4125f47649f585d9d062fabChristian MaedertransOpInfo (OpInfo t _ opDef) =

b25c72845890740c2f8a21214752574990b943cfChristian Maeder case opDef of

4f4e94264f48e255d4125f47649f585d9d062fabChristian Maeder ConstructData _ -> Nothing

afc52bfaabee38c4d55cee9f35b1a0028ba3854aAndy Gimblett _ -> Just (transOpType t)

b25c72845890740c2f8a21214752574990b943cfChristian Maeder

4f4e94264f48e255d4125f47649f585d9d062fabChristian Maeder-- operation type

b25c72845890740c2f8a21214752574990b943cfChristian MaedertransOpType :: TypeScheme -> Typ

4f4e94264f48e255d4125f47649f585d9d062fabChristian MaedertransOpType (TypeScheme _ op _) = transType op

b25c72845890740c2f8a21214752574990b943cfChristian Maeder

4f4e94264f48e255d4125f47649f585d9d062fabChristian Maeder-- types

b25c72845890740c2f8a21214752574990b943cfChristian MaedertransType :: Type -> Typ

b25c72845890740c2f8a21214752574990b943cfChristian MaedertransType t = case getTypeAppl t of

b25c72845890740c2f8a21214752574990b943cfChristian Maeder (TypeName tid _ n, tyArgs) -> let num = length tyArgs in

4f4e94264f48e255d4125f47649f585d9d062fabChristian Maeder if n == 0 then

b25c72845890740c2f8a21214752574990b943cfChristian Maeder if tid == unitTypeId && null tyArgs then boolType

b25c72845890740c2f8a21214752574990b943cfChristian Maeder else if tid == lazyTypeId && num == 1 then

b25c72845890740c2f8a21214752574990b943cfChristian Maeder transType $ head tyArgs

0a83f8dcd5598436966584b858313eb5efd95d5bLiam O'Reilly else if isArrow tid && num == 2 then

9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly let [t1, t2] = tyArgs

2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly tr = transType t2

2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly in mkFunType (transType t1) $

23a073e0a3433ca80a286d46202841b569ec36fdChristian Maeder if isPartialArrow tid && not (isPredType t)

23a073e0a3433ca80a286d46202841b569ec36fdChristian Maeder then mkOptionType tr else tr

7371f8fe3a9a286a74ea30a3cd18e7740f67d537Andy Gimblett else if isProductId tid && num > 1 then

fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly foldl1 prodType $ map transType tyArgs

fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly else Type (showIsaTypeT tid baseSign) [] $ map transType tyArgs

fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly else TFree (showIsaTypeT tid baseSign) []

fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly -- type arguments are not allowed here!

afc52bfaabee38c4d55cee9f35b1a0028ba3854aAndy Gimblett _ -> error $ "transType " ++ showDoc t "\n" ++ show t

4f4e94264f48e255d4125f47649f585d9d062fabChristian Maeder

4f4e94264f48e255d4125f47649f585d9d062fabChristian Maeder-- * translation of a datatype declaration

da955132262baab309a50fdffe228c9efe68251dCui Jian

4f4e94264f48e255d4125f47649f585d9d062fabChristian MaedertransDatatype :: TypeMap -> DomainTab

4f4e94264f48e255d4125f47649f585d9d062fabChristian MaedertransDatatype tm = map transDataEntry (Map.fold extractDataypes [] tm)

310d12b88f902a597cdb08a1c7d11ae7130855eeChristian Maeder where extractDataypes ti des = case typeDefn ti of

310d12b88f902a597cdb08a1c7d11ae7130855eeChristian Maeder DatatypeDefn de -> des++[de]

310d12b88f902a597cdb08a1c7d11ae7130855eeChristian Maeder _ -> des

310d12b88f902a597cdb08a1c7d11ae7130855eeChristian Maeder

4f4e94264f48e255d4125f47649f585d9d062fabChristian Maeder-- datatype with name (tyId) + args (tyArgs) and alternatives

4f4e94264f48e255d4125f47649f585d9d062fabChristian MaedertransDataEntry :: DataEntry -> [DomainEntry]

4f4e94264f48e255d4125f47649f585d9d062fabChristian MaedertransDataEntry (DataEntry _ tyId Le.Free tyArgs _ alts) =

9efe365d7ce90313e53ea5cfeca391d118fd8629Christian Maeder [(transDName tyId tyArgs, map transAltDefn $ Set.toList alts)]

9efe365d7ce90313e53ea5cfeca391d118fd8629Christian Maeder where transDName ti ta = Type (showIsaTypeT ti baseSign) []

9efe365d7ce90313e53ea5cfeca391d118fd8629Christian Maeder $ map transTypeArg ta

9efe365d7ce90313e53ea5cfeca391d118fd8629Christian MaedertransDataEntry _ = error "HasCASL2IsabelleHOL.transDataEntry"

9efe365d7ce90313e53ea5cfeca391d118fd8629Christian Maeder

9efe365d7ce90313e53ea5cfeca391d118fd8629Christian Maeder-- arguments of datatype's typeconstructor

9efe365d7ce90313e53ea5cfeca391d118fd8629Christian MaedertransTypeArg :: TypeArg -> Typ

9efe365d7ce90313e53ea5cfeca391d118fd8629Christian MaedertransTypeArg ta = TFree (showIsaTypeT (getTypeVar ta) baseSign) []

9efe365d7ce90313e53ea5cfeca391d118fd8629Christian Maeder

9efe365d7ce90313e53ea5cfeca391d118fd8629Christian Maeder-- datatype alternatives/constructors

9efe365d7ce90313e53ea5cfeca391d118fd8629Christian MaedertransAltDefn :: AltDefn -> (VName, [Typ])

9efe365d7ce90313e53ea5cfeca391d118fd8629Christian MaedertransAltDefn (Construct opId ts Total _) =

9efe365d7ce90313e53ea5cfeca391d118fd8629Christian Maeder let ts' = map transType ts

9efe365d7ce90313e53ea5cfeca391d118fd8629Christian Maeder in case opId of

9efe365d7ce90313e53ea5cfeca391d118fd8629Christian Maeder Just opId' -> (mkVName $ showIsaConstT opId' baseSign, ts')

9efe365d7ce90313e53ea5cfeca391d118fd8629Christian Maeder Nothing -> (mkVName "", ts')

4f4e94264f48e255d4125f47649f585d9d062fabChristian MaedertransAltDefn _ = error "HasCASL2IsabelleHOL.transAltDefn"

4f4e94264f48e255d4125f47649f585d9d062fabChristian Maeder

4f4e94264f48e255d4125f47649f585d9d062fabChristian Maeder-- * Formulas

4f4e94264f48e255d4125f47649f585d9d062fabChristian Maeder

4f4e94264f48e255d4125f47649f585d9d062fabChristian Maeder-- simple variables

4f4e94264f48e255d4125f47649f585d9d062fabChristian MaedertransVar :: Id -> VName

4f4e94264f48e255d4125f47649f585d9d062fabChristian MaedertransVar v = mkVName $ showIsaConstT v baseSign

4f4e94264f48e255d4125f47649f585d9d062fabChristian Maeder

4f4e94264f48e255d4125f47649f585d9d062fabChristian MaedertransSentence :: Env -> Le.Sentence -> Maybe IsaSign.Term

4f4e94264f48e255d4125f47649f585d9d062fabChristian MaedertransSentence sign s = case s of

4f4e94264f48e255d4125f47649f585d9d062fabChristian Maeder Le.Formula t -> Just (transTerm sign t)

4f4e94264f48e255d4125f47649f585d9d062fabChristian Maeder DatatypeSen _ -> Nothing

4f4e94264f48e255d4125f47649f585d9d062fabChristian Maeder ProgEqSen _ _ _pe -> Nothing

4f4e94264f48e255d4125f47649f585d9d062fabChristian Maeder

4f4e94264f48e255d4125f47649f585d9d062fabChristian Maeder-- disambiguate operation names

4f4e94264f48e255d4125f47649f585d9d062fabChristian MaedertransOpId :: Env -> Id -> TypeScheme -> String

4f4e94264f48e255d4125f47649f585d9d062fabChristian MaedertransOpId sign op ts =

4f4e94264f48e255d4125f47649f585d9d062fabChristian Maeder case (do ops <- Map.lookup op (assumps sign)

4f4e94264f48e255d4125f47649f585d9d062fabChristian Maeder if isSingleton ops then return $ showIsaConstT op baseSign

4f4e94264f48e255d4125f47649f585d9d062fabChristian Maeder else do i <- elemIndex ts $ map opType $ Set.toList ops

afc52bfaabee38c4d55cee9f35b1a0028ba3854aAndy Gimblett return $ showIsaConstIT op (i+1) baseSign) of

7371f8fe3a9a286a74ea30a3cd18e7740f67d537Andy Gimblett Just str -> str

7371f8fe3a9a286a74ea30a3cd18e7740f67d537Andy Gimblett Nothing -> showIsaConstT op baseSign

7371f8fe3a9a286a74ea30a3cd18e7740f67d537Andy Gimblett

576a4ca6de740c90afd448607c2323477139de24Liam O'ReillytransProgEq :: Env -> ProgEq -> (IsaSign.Term, IsaSign.Term)

7371f8fe3a9a286a74ea30a3cd18e7740f67d537Andy GimbletttransProgEq sign (ProgEq pat t _) =

fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly (transPattern sign pat, transPattern sign t)

fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly

2bb060537a37352251aa04d8dc09aa53aad5d4bfLiam O'Reilly-- terms

576a4ca6de740c90afd448607c2323477139de24Liam O'ReillytransTerm :: Env -> As.Term -> IsaSign.Term

b25c72845890740c2f8a21214752574990b943cfChristian MaedertransTerm sign trm = case trm of

576a4ca6de740c90afd448607c2323477139de24Liam O'Reilly QualVar (VarDecl var _ _ _) ->

b25c72845890740c2f8a21214752574990b943cfChristian Maeder termAppl conSome $ IsaSign.Free (transVar var)

b25c72845890740c2f8a21214752574990b943cfChristian Maeder

576a4ca6de740c90afd448607c2323477139de24Liam O'Reilly QualOp _ (PolyId opId _ _) ts _ _ _ ->

b25c72845890740c2f8a21214752574990b943cfChristian Maeder if opId == trueId then true

b25c72845890740c2f8a21214752574990b943cfChristian Maeder else if opId == falseId then false

576a4ca6de740c90afd448607c2323477139de24Liam O'Reilly else termAppl conSome (conDouble (transOpId sign opId ts))

b25c72845890740c2f8a21214752574990b943cfChristian Maeder

b25c72845890740c2f8a21214752574990b943cfChristian Maeder QuantifiedTerm quan varDecls phi _ ->

576a4ca6de740c90afd448607c2323477139de24Liam O'Reilly let quantify q gvd phi' = case gvd of

576a4ca6de740c90afd448607c2323477139de24Liam O'Reilly GenVarDecl (VarDecl var _ _ _) ->

b25c72845890740c2f8a21214752574990b943cfChristian Maeder termAppl (conDouble $ qname q)

b25c72845890740c2f8a21214752574990b943cfChristian Maeder $ Abs (IsaSign.Free $ transVar var) phi' NotCont

434c11a96bc623ebd5b60781efabef319bb15b0eChristian Maeder GenTypeVarDecl _ -> phi'

434c11a96bc623ebd5b60781efabef319bb15b0eChristian Maeder qname Universal = allS

b25c72845890740c2f8a21214752574990b943cfChristian Maeder qname Existential = exS

576a4ca6de740c90afd448607c2323477139de24Liam O'Reilly qname Unique = ex1S

576a4ca6de740c90afd448607c2323477139de24Liam O'Reilly in foldr (quantify quan) (transTerm sign phi) varDecls

b25c72845890740c2f8a21214752574990b943cfChristian Maeder TypedTerm t _ _ _ -> transTerm sign t

b25c72845890740c2f8a21214752574990b943cfChristian Maeder LambdaTerm pats p body _ ->

b25c72845890740c2f8a21214752574990b943cfChristian Maeder let lambdaAbs f = if null pats then termAppl conSome

b25c72845890740c2f8a21214752574990b943cfChristian Maeder (Abs (IsaSign.Free $ mkVName "dummyVar")

b25c72845890740c2f8a21214752574990b943cfChristian Maeder (f sign body) NotCont)

b25c72845890740c2f8a21214752574990b943cfChristian Maeder else termAppl conSome (foldr (abstraction sign)

b25c72845890740c2f8a21214752574990b943cfChristian Maeder (f sign body)

576a4ca6de740c90afd448607c2323477139de24Liam O'Reilly pats)

b25c72845890740c2f8a21214752574990b943cfChristian Maeder in case p of

b25c72845890740c2f8a21214752574990b943cfChristian Maeder -- distinguishes between partial and total lambda abstraction

576a4ca6de740c90afd448607c2323477139de24Liam O'Reilly -- total lambda bodies are of type 'a' instead of type 'a option'

b25c72845890740c2f8a21214752574990b943cfChristian Maeder Partial -> lambdaAbs transTerm

b25c72845890740c2f8a21214752574990b943cfChristian Maeder Total -> lambdaAbs transTotalLambda

576a4ca6de740c90afd448607c2323477139de24Liam O'Reilly LetTerm As.Let peqs body _ ->

b25c72845890740c2f8a21214752574990b943cfChristian Maeder IsaSign.Let (map (transProgEq sign) peqs) $ transTerm sign body

b25c72845890740c2f8a21214752574990b943cfChristian Maeder TupleTerm ts@(_ : _) _ ->

576a4ca6de740c90afd448607c2323477139de24Liam O'Reilly foldl1 (binConst pairC) (map (transTerm sign) ts)

576a4ca6de740c90afd448607c2323477139de24Liam O'Reilly ApplTerm t1 t2 _ -> transAppl sign Nothing t1 t2

b25c72845890740c2f8a21214752574990b943cfChristian Maeder CaseTerm t peqs _ ->

b25c72845890740c2f8a21214752574990b943cfChristian Maeder -- flatten case alternatives

b25c72845890740c2f8a21214752574990b943cfChristian Maeder let alts = arangeCaseAlts sign peqs

b25c72845890740c2f8a21214752574990b943cfChristian Maeder in case t of

b25c72845890740c2f8a21214752574990b943cfChristian Maeder -- introduces new case statement if case variable is

576a4ca6de740c90afd448607c2323477139de24Liam O'Reilly -- a term application that may evaluate to 'Some x' or 'None'

576a4ca6de740c90afd448607c2323477139de24Liam O'Reilly QualVar (VarDecl decl _ _ _) ->

b25c72845890740c2f8a21214752574990b943cfChristian Maeder Case (IsaSign.Free (transVar decl)) alts

b25c72845890740c2f8a21214752574990b943cfChristian Maeder _ -> Case (transTerm sign t)

b25c72845890740c2f8a21214752574990b943cfChristian Maeder [(conDouble "None", conDouble "None"),

576a4ca6de740c90afd448607c2323477139de24Liam O'Reilly (App conSome (IsaSign.Free (mkVName "caseVar")) NotCont,

576a4ca6de740c90afd448607c2323477139de24Liam O'Reilly Case (IsaSign.Free (mkVName "caseVar")) alts)]

b25c72845890740c2f8a21214752574990b943cfChristian Maeder _ -> error $ "HasCASL2IsabelleHOL.transTerm " ++ showDoc trm "\n"

b25c72845890740c2f8a21214752574990b943cfChristian Maeder ++ show trm

b25c72845890740c2f8a21214752574990b943cfChristian Maeder

576a4ca6de740c90afd448607c2323477139de24Liam O'ReillytransAppl :: Env -> Maybe As.Type -> As.Term -> As.Term -> IsaSign.Term

b25c72845890740c2f8a21214752574990b943cfChristian MaedertransAppl s ty' t' t'' = case t'' of

7371f8fe3a9a286a74ea30a3cd18e7740f67d537Andy Gimblett TupleTerm [] _ -> transTerm s t'

7371f8fe3a9a286a74ea30a3cd18e7740f67d537Andy Gimblett _ -> case t' of

7371f8fe3a9a286a74ea30a3cd18e7740f67d537Andy Gimblett QualVar (VarDecl _ ty _ _) -> transApplOp s ty t' t''

7371f8fe3a9a286a74ea30a3cd18e7740f67d537Andy Gimblett QualOp _ (PolyId opId _ _) (TypeScheme _ ty _) _ _ _ ->

7371f8fe3a9a286a74ea30a3cd18e7740f67d537Andy Gimblett if elem opId $ map fst bList then

dd7da1b5fedc05b92ba023ebd803e6f4a662503bChristian Maeder -- logical formulas are translated seperatly (transLog)

if opId == whenElse then transWhenElse s t''

else transLog s opId t' t''

else transApplOp s ty t' t''

-- distinguishes between partial and total term application

TypedTerm tt' _ typ' _ -> transAppl s (Just typ') tt' t''

_ -> maybe (mkApp "app" s t' t'')

( \ ty -> transApplOp s ty t' t'') ty'

mkApp :: String -> Env -> As.Term -> As.Term -> IsaSign.Term

mkApp s sg tt tt' = termAppl (termAppl (conDouble s) (transTerm sg tt))

(transTerm sg tt')

transApplOp :: Env -> As.Type -> As.Term -> As.Term -> IsaSign.Term

transApplOp s ty tt tt' = if isPredType ty then mkApp "pApp" s tt tt'

else case getTypeAppl ty of

(TypeName tid _ 0, [_, _]) | isArrow tid ->

if isPartialArrow tid then mkApp "app" s tt tt'

else mkApp "apt" s tt tt'

_ -> mkApp "app" s tt tt'

-- translation formulas with logical connectives

transLog :: Env -> Id -> As.Term -> As.Term -> IsaSign.Term

transLog sign opId opTerm t = case t of

TupleTerm [l' , r'] _

| opId == andId -> binConj l r

| opId == orId -> binDisj l r

| opId == implId -> binImpl l r

| opId == infixIf -> binImpl r l

| opId == eqvId -> binEq l r

| opId == exEq -> binConj (binEq l r) $

binConj (termAppl defOp l) $

termAppl defOp r

| opId == eqId -> binEq l r

where l = transTerm sign l'

r = transTerm sign r'

_ | opId == notId -> termAppl notOp (transTerm sign t)

| opId == defId -> termAppl defOp (transTerm sign t)

| otherwise -> termAppl (transTerm sign opTerm) (transTerm sign t)

-- | when else statement

transWhenElse :: Env -> As.Term -> IsaSign.Term

transWhenElse sign t =

case t of

TupleTerm terms _ ->

let ts = (map (transTerm sign) terms)

in case ts of

[i, c, e] -> If c i e NotCont

_ -> error "HasCASL2IsabelleHOL.transWhenElse.tuple"

_ -> error "HasCASL2IsabelleHOL.transWhenElse"

-- * translation of lambda abstractions

-- form Abs(pattern term)

abstraction :: Env -> As.Term -> IsaSign.Term -> IsaSign.Term

abstraction sign pat body =

Abs (transPattern sign pat) body NotCont

-- translation of lambda patterns

-- a pattern keeps his type 't', isn't translated to 't option'

transPattern :: Env -> As.Term -> IsaSign.Term

transPattern _ (QualVar (VarDecl var _ _ _)) =

IsaSign.Free (transVar var)

transPattern sign (TupleTerm terms@(_ : _) _) =

foldl1 (binConst isaPair) $ map (transPattern sign) terms

transPattern _ (QualOp _ (PolyId opId _ _) _ _ _ _) =

conDouble $ showIsaConstT opId baseSign

transPattern sign (TypedTerm t _ _ _) = transPattern sign t

transPattern sign (ApplTerm t1 t2 _) =

App (transPattern sign t1) (transPattern sign t2) NotCont

transPattern sign t = transTerm sign t

-- translation of total lambda abstraction bodies

transTotalLambda :: Env -> As.Term -> IsaSign.Term

transTotalLambda _ (QualVar (VarDecl var _ _ _)) =

IsaSign.Free (transVar var)

transTotalLambda sign t@(QualOp _ (PolyId opId _ _) _ _ _ _) =

if opId == trueId || opId == falseId then transTerm sign t

else conDouble $ showIsaConstT opId baseSign

transTotalLambda sign (ApplTerm term1 term2 _) =

termAppl (transTotalLambda sign term1) $ transTotalLambda sign term2

transTotalLambda sign (TypedTerm t _ _ _) = transTotalLambda sign t

transTotalLambda sign (LambdaTerm pats part body _) =

case part of

Partial -> lambdaAbs transTerm

Total -> lambdaAbs transTotalLambda

where

lambdaAbs f =

if (null pats) then Abs (IsaSign.Free (mkVName "dummyVar"))

(f sign body) NotCont

-- if (null pats) then Abs [("dummyVar", noType)]

else foldr (abstraction sign) (f sign body) pats

transTotalLambda sign (TupleTerm terms@(_ : _) _) =

foldl1 (binConst isaPair) $ map (transTotalLambda sign) terms

transTotalLambda sign (CaseTerm t pEqs _) =

Case (transTotalLambda sign t) $ map transCaseAltTotal pEqs

where transCaseAltTotal (ProgEq pat trm _) =

(transPat sign pat, transTotalLambda sign trm)

transTotalLambda sign t = transTerm sign t

-- * translation of case alternatives

{- Annotation concerning Patterns:

Following the HasCASL-Summary and the limits of the encoding

from HasCASL to Isabelle/HOL patterns may take the form:

QualVar, QualOp, ApplTerm, TupleTerm and TypedTerm

-}

-- Input: List of case alternative (one pattern per term)

-- Functionality: Tests wheter pattern is a variable -> case alternative is

-- translated

arangeCaseAlts :: Env -> [ProgEq]-> [(IsaSign.Term, IsaSign.Term)]

arangeCaseAlts sign peqs

| and (map patIsVar peqs) = map (transCaseAlt sign) peqs

| otherwise = sortCaseAlts sign peqs

{- Input: List of case alternatives, that patterns does consist of

datatype constructors (with arguments) or tupels

Functionality: Groups case alternatives by leading

pattern-constructor each pattern group is flattened

-}

sortCaseAlts :: Env -> [ProgEq]-> [(IsaSign.Term, IsaSign.Term)]

sortCaseAlts sign peqs =

let consList

| null peqs = error "No case alternatives."

| otherwise = getCons sign (getName (head peqs))

groupedByCons = nubOrd (map (groupCons peqs) consList)

in map (flattenPattern sign) groupedByCons

-- Returns a list of the constructors of the used datatype

getCons :: Env -> Id -> [Id]

getCons sign tyId =

extractIds (typeDefn (findInMap tyId (typeMap sign)))

where extractIds (DatatypeDefn (DataEntry _ _ _ _ _ altDefns)) =

catMaybes $ map stripConstruct $ Set.toList altDefns

extractIds _ = error "HasCASL2Isabelle.extractIds"

stripConstruct (Construct i _ _ _) = i

findInMap :: Ord k => k -> Map.Map k a -> a

findInMap k m = maybe (error "HasCASL2isabelleHOL.findInMap") id $

Map.lookup k m

-- Extracts the type of the used datatype in case patterns

getName :: ProgEq -> Id

getName (ProgEq pat _ _) = (getTypeName pat)

getTypeName :: As.Term -> Id

getTypeName p =

case p of

QualVar (VarDecl _ ty _ _) -> name ty

QualOp _ _ (TypeScheme _ ty _) _ _ _ -> name ty

TypedTerm _ _ ty _ -> name ty

ApplTerm t _ _ -> getTypeName t

TupleTerm (t : _) _ -> getTypeName t

_ -> error "HasCASL2IsabelleHOL.getTypeName"

where name tp = case getTypeAppl tp of

(TypeName tyId _ 0, tyArgs) -> let num = length tyArgs in

if isArrow tyId && num == 2 then

name $ head $ tail tyArgs

else if isProductId tyId && num > 1 then

name $ head tyArgs

else tyId

_ -> error "HasCASL2IsabelleHOL.name (of type)"

-- Input: Case alternatives and name of one constructor

-- Functionality: Filters case alternatives by constructor's name

groupCons :: [ProgEq] -> Id -> [ProgEq]

groupCons peqs name = filter hasSameName peqs

where hasSameName (ProgEq pat _ _) =

hsn pat

hsn pat =

case pat of

QualOp _ (PolyId n _ _) _ _ _ _ -> n == name

ApplTerm t1 _ _ -> hsn t1

TypedTerm t _ _ _ -> hsn t

TupleTerm _ _ -> True

_ -> False

-- Input: List of case alternatives with same leading constructor

-- Functionality: Tests whether the constructor has no arguments, if so

-- translates case alternatives

flattenPattern :: Env -> [ProgEq] -> (IsaSign.Term, IsaSign.Term)

flattenPattern sign peqs = case peqs of

[] -> error "Missing constructor alternative in case pattern."

[h] -> transCaseAlt sign h

-- at this stage there are patterns left which use 'ApplTerm' or 'TupleTerm'

-- or the 'TypedTerm' variant of one of them

_ -> let m = concentrate (matricize peqs) sign in

transCaseAlt sign (ProgEq (shrinkPat m) (term m) nullRange)

data CaseMatrix = CaseMatrix

{ patBrand :: PatBrand

, cons :: Maybe As.Term

, args :: [As.Term]

, newArgs :: [As.Term]

, term :: As.Term

} deriving (Show, Eq, Ord)

data PatBrand = Appl | Tuple | QuOp | QuVar deriving (Show, Eq, Ord)

{- First of all a matrix is allocated (matriArg) with the arguments of a

constructor resp. of a tuple. They're binded with the term, that would

be executed if the pattern matched. Then the resulting list of

matrices is grouped by the leading argument. (groupArgs) Afterwards -

if a list of grouped arguments has more than one element - the last

pattern argument (in the list 'patterns') is replaced by a new variable.

n patterns are reduced to one pattern.

This procedure is repeated until there's only one case alternative

for each constructor.

-}

-- Functionality: turns ProgEq into CaseMatrix

matricize :: [ProgEq] -> [CaseMatrix]

matricize = map matriPEq

matriPEq :: ProgEq -> CaseMatrix

matriPEq (ProgEq pat altTerm _) = matriArg pat altTerm

matriArg :: As.Term -> As.Term -> CaseMatrix

matriArg pat cTerm =

case pat of

ApplTerm t1 t2 _ -> let (c, p) = stripAppl t1 (Nothing, []) in CaseMatrix

{ patBrand = Appl,

cons = c,

args = p ++ [t2],

newArgs = [],

term = cTerm }

TupleTerm ts _ -> CaseMatrix

{ patBrand = Tuple,

cons = Nothing,

args = ts,

newArgs = [],

term = cTerm }

TypedTerm t _ _ _ -> matriArg t cTerm

qv@(QualVar _) -> CaseMatrix

{ patBrand = QuVar,

cons = Nothing,

args = [qv],

newArgs = [],

term = cTerm }

qo@(QualOp _ _ _ _ _ _) -> CaseMatrix

{ patBrand = QuOp,

cons = Nothing,

args = [qo],

newArgs = [],

term = cTerm }

_ -> error "HasCASL2IsabelleHOL.matriArg"

-- Assumption: The innermost term of a case-pattern consisting of a ApplTerm

-- is a QualOp, that is a datatype constructor

where stripAppl ct tp = case ct of

TypedTerm (ApplTerm q@(QualOp _ _ _ _ _ _) t' _) _ _ _ ->

(Just q, [t'] ++ snd tp)

TypedTerm (ApplTerm (TypedTerm

q@(QualOp _ _ _ _ _ _) _ _ _) t' _) _ _ _ ->

(Just q, [t'] ++ snd tp)

TypedTerm (ApplTerm t' t'' _) _ _ _ ->

stripAppl t' (fst tp, [t''] ++ snd tp)

ApplTerm q@(QualOp _ _ _ _ _ _) t' _ -> (Just q, [t'] ++ snd tp)

ApplTerm (TypedTerm

q@(QualOp _ _ _ _ _ _) _ _ _) t' _ -> (Just q, [t'])

ApplTerm t' t'' _ -> stripAppl t' (fst tp, [t''] ++ snd tp)

q@(QualOp _ _ _ _ _ _) -> (Just q, snd tp)

_ -> (Nothing, [ct] ++ snd tp)

-- Input: List with CaseMatrix of same leading constructor pattern

-- Functionality: First: Groups CMs so that these CMs are in one list

-- that only differ in their last argument

-- then: reduces list of every CMslist to one CM

concentrate :: [CaseMatrix] -> Env -> CaseMatrix

concentrate cmxs sign = case map (redArgs sign) $ nubOrd

$ map (groupByArgs cmxs) [0..(length cmxs-1)] of

[h] -> h

l -> concentrate l sign

groupByArgs :: [CaseMatrix] -> Int -> [CaseMatrix]

groupByArgs cmxs i

| and (map null (map args cmxs)) = cmxs

| otherwise = (filter equalPat cmxs)

where patE = init (args (cmxs !! i))

equalPat cmx = isSingle (args cmx) || init (args cmx) == patE

redArgs :: Env -> [CaseMatrix] -> CaseMatrix

redArgs sign cmxs

| and (map (testPatBrand Appl) cmxs) = redAppl cmxs sign

| and (map (testPatBrand Tuple) cmxs) = redAppl cmxs sign

| isSingle cmxs = head cmxs

| otherwise = head cmxs

where testPatBrand pb cmx = pb == patBrand cmx

{- Input: List of CMs thats leading constructor and arguments except

the last one are equal

Functionality: Reduces n CMs to one with same last argument in

pattern (perhaps a new variable

-}

redAppl :: [CaseMatrix] -> Env -> CaseMatrix

redAppl cmxs sign

| and (map null (map args cmxs)) = head cmxs

| isSingle cmxs =

(head cmxs) { args = init $ args $ head cmxs,

newArgs = last (args $ head cmxs) : newArgs (head cmxs) }

| and (map termIsVar lastArgs) = substVar (head cmxs)

| otherwise = substTerm (head cmxs)

where terms = map term cmxs

lastArgs = map last (map args cmxs)

varName = "caseVar" ++ show (length (args (head cmxs)))

varId = (mkId [(mkSimpleId varName)])

newVar = QualVar (VarDecl varId (TypeName varId rStar 1)

As.Other nullRange)

newPeqs = (map newProgEq (zip lastArgs terms))

newPeqs' = recArgs sign newPeqs

substVar cmx

| null (args cmx) = cmx

| isSingle (args cmx) =

cmx { args = [],

newArgs = last(args cmx) : (newArgs cmx) }

| otherwise =

cmx { args = init (args cmx),

newArgs = last(args cmx) : (newArgs cmx) }

substTerm cmx

| null (args cmx) = cmx

| isSingle (args cmx) =

cmx { args = [],

newArgs = newVar : (newArgs cmx),

term = CaseTerm newVar newPeqs' nullRange }

| otherwise =

cmx { args = init(args cmx),

newArgs = newVar : (newArgs cmx),

term = CaseTerm newVar newPeqs' nullRange }

newProgEq (p, t) = ProgEq p t nullRange

-- Input: ProgEqs that were build to replace an argument

-- with a case statement

-- Functionality:

recArgs :: Env -> [ProgEq] -> [ProgEq]

recArgs sign peqs

| isSingle groupedByCons

|| null groupedByCons = []

| otherwise = doPEQ groupedByCons []

where consList

| null peqs = error "No case alternatives."

| otherwise = getCons sign (getName (head peqs))

groupedByCons = map (groupCons peqs) consList

doPEQ [] res = res

doPEQ (g:gByCs) res

| isSingle g = doPEQ gByCs (res ++ g)

| otherwise = doPEQ gByCs (res ++ [(toPEQ (testPEQs sign g))])

toPEQ cmx = ProgEq (shrinkPat cmx) (term cmx) nullRange

testPEQs sig ps

| null peqs = error "HasCASL2IsabelleHOL.testPEQs"

| otherwise = concentrate (matricize ps) sig

-- accumulates arguments of caseMatrix to one pattern

shrinkPat :: CaseMatrix -> As.Term

shrinkPat cmx =

case patBrand cmx of

Appl -> case cons cmx of

Just c -> foldl mkApplT c ((args cmx) ++ (newArgs cmx))

Nothing -> error "HasCASL2IsabelleHOL.shrinkPat"

Tuple -> TupleTerm (args cmx ++ newArgs cmx) nullRange

QuOp -> head (args cmx)

_ -> head (newArgs cmx)

where mkApplT t1 t2 = ApplTerm t1 t2 nullRange

patIsVar :: ProgEq -> Bool

patIsVar (ProgEq pat _ _) = termIsVar pat

termIsVar :: As.Term -> Bool

termIsVar t = case t of

QualVar _ -> True

TypedTerm tr _ _ _ -> termIsVar tr

TupleTerm ts _ -> and (map termIsVar ts)

_ -> False

patHasNoArg :: ProgEq -> Bool

patHasNoArg (ProgEq pat _ _) = termHasNoArg pat

termHasNoArg :: As.Term -> Bool

termHasNoArg t = case t of

QualOp _ _ _ _ _ _ -> True

TypedTerm tr _ _ _ -> termHasNoArg tr

_ -> False

transCaseAlt :: Env -> ProgEq -> (IsaSign.Term, IsaSign.Term)

transCaseAlt sign (ProgEq pat trm _) =

(transPat sign pat, (transTerm sign trm))

transPat :: Env -> As.Term -> IsaSign.Term

transPat _ (QualVar (VarDecl var _ _ _)) =

IsaSign.Free (transVar var)

transPat sign (ApplTerm term1 term2 _) =

termAppl (transPat sign term1) (transPat sign term2)

transPat sign (TypedTerm trm _ _ _) = transPat sign trm

transPat sign (TupleTerm terms@(_ : _) _) =

foldl1 (binConst isaPair) (map (transPat sign) terms)

transPat _ (QualOp _ (PolyId i _ _) _ _ _ _) =

conDouble (showIsaConstT i baseSign)

transPat _ _ = error "HasCASL2IsabelleHOL.transPat"

-- | apply binary operation to arguments

binConst :: String -> IsaSign.Term -> IsaSign.Term -> IsaSign.Term

binConst s = binVNameAppl $ mkVName s

-- | upper case curried pair constructor

isaPair :: String

isaPair = "Pair"