1b05bdb88b90d3c947351f262d7ae7d68f0a4a6fTill Mossakowski{- |

1b05bdb88b90d3c947351f262d7ae7d68f0a4a6fTill MossakowskiModule : $Header$

1b05bdb88b90d3c947351f262d7ae7d68f0a4a6fTill MossakowskiCopyright : (c) Sonja Groening, C. Maeder, Uni Bremen 2003-2006

c06dd8856a03b72f6b3f69e874f8700f10cb8522Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

f7819aa9d183836144a98c70d4fa7d65e31cb513Till Mossakowski

c06dd8856a03b72f6b3f69e874f8700f10cb8522Christian MaederMaintainer : maeder@tzi.de

c06dd8856a03b72f6b3f69e874f8700f10cb8522Christian MaederStability : provisional

1b05bdb88b90d3c947351f262d7ae7d68f0a4a6fTill MossakowskiPortability : non-portable (imports Logic.Logic)

1b05bdb88b90d3c947351f262d7ae7d68f0a4a6fTill Mossakowski

e379124f467e5d0ef7d3c0ca238bff0521f70831Till MossakowskiThis embedding comorphism from HasCASL to Isabelle-HOL is an old

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maederversion that can be deleted as soon as case terms are implemented by

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian MaederPCoClTyConsHOL2IsabelleHOL.

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder-}

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maedermodule Comorphisms.HasCASL2IsabelleHOL where

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maederimport Logic.Logic as Logic

c06dd8856a03b72f6b3f69e874f8700f10cb8522Christian Maederimport Logic.Comorphism

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maederimport HasCASL.Logic_HasCASL

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maederimport HasCASL.Sublogic

c0ba7121c93e4f9292f2d95a0ac7460a7b9e5aeaTill Mossakowskiimport HasCASL.Le as Le

e3c9174a782e90f965a0b080c22861c3ef5af12dTill Mossakowskiimport HasCASL.As as As

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maederimport HasCASL.AsUtils

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maederimport HasCASL.Builtin

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maederimport Isabelle.IsaSign as IsaSign

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maederimport Isabelle.IsaConsts

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maederimport Isabelle.Logic_Isabelle

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maederimport Isabelle.Translate

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maederimport Common.DocUtils

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maederimport Common.Id

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maederimport Common.Result

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maederimport qualified Data.Map as Map

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maederimport Common.AS_Annotation

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maederimport Data.List (elemIndex, nub)

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maederimport Data.Maybe (catMaybes)

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder-- | The identity of the comorphism

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maederdata HasCASL2IsabelleHOL = HasCASL2IsabelleHOL deriving Show

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maederinstance Language HasCASL2IsabelleHOL -- default definition is okay

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maederinstance Comorphism HasCASL2IsabelleHOL

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder HasCASL Sublogic

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder BasicSpec Le.Sentence SymbItems SymbMapItems

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder Env Morphism

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder Symbol RawSymbol ()

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder Isabelle () () IsaSign.Sentence () ()

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder IsaSign.Sign

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder IsabelleMorphism () () () where

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder sourceLogic HasCASL2IsabelleHOL = HasCASL

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder sourceSublogic HasCASL2IsabelleHOL = sublogic_min noSubtypes noClasses

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder targetLogic HasCASL2IsabelleHOL = Isabelle

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder mapSublogic cid sl = if sl `isSubElem` sourceSublogic cid

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder then Just () else Nothing

e3c9174a782e90f965a0b080c22861c3ef5af12dTill Mossakowski map_theory HasCASL2IsabelleHOL = mkTheoryMapping transSignature

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder (map_sentence HasCASL2IsabelleHOL)

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder map_morphism = mapDefaultMorphism

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder map_sentence HasCASL2IsabelleHOL sign phi =

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder case transSentence sign phi of

1b05bdb88b90d3c947351f262d7ae7d68f0a4a6fTill Mossakowski Nothing -> warning (mkSen true)

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder "translation of sentence not implemented" nullRange

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder Just (ts) -> return $ mkSen ts

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder map_symbol = errMapSymbol

ba904a15082557e939db689fcfba0c68c9a4f740Christian Maeder

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski-- * Signature

ba904a15082557e939db689fcfba0c68c9a4f740Christian MaederbaseSign :: BaseSig

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian MaederbaseSign = MainHC_thy

ba904a15082557e939db689fcfba0c68c9a4f740Christian Maeder

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

ba904a15082557e939db689fcfba0c68c9a4f740Christian MaedertransSignature sign =

ba904a15082557e939db689fcfba0c68c9a4f740Christian Maeder return (IsaSign.emptySign {

ba904a15082557e939db689fcfba0c68c9a4f740Christian Maeder baseSig = baseSign,

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder -- translation of typeconstructors

c616e681da8c052b62e14247fea522da099ac0e4Christian Maeder tsig = emptyTypeSig

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder { arities = Map.foldWithKey extractTypeName

ba904a15082557e939db689fcfba0c68c9a4f740Christian Maeder Map.empty

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder (typeMap sign) },

e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski -- translation of operation declarations

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder constTab = Map.foldWithKey insertOps

e18f5e61d29064a427ca7bef421e250a9a4c9701Till Mossakowski Map.empty

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder (assumps sign),

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder -- translation of datatype declarations

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder domainTab = transDatatype (typeMap sign),

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder showLemmas = True },

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder [] )

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder where

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder extractTypeName tyId typeInfo m =

c616e681da8c052b62e14247fea522da099ac0e4Christian Maeder if isDatatypeDefn typeInfo then m

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder else Map.insert (showIsaTypeT tyId baseSign) [(isaTerm, [])] m

1b05bdb88b90d3c947351f262d7ae7d68f0a4a6fTill Mossakowski -- translate the kind here!

1b05bdb88b90d3c947351f262d7ae7d68f0a4a6fTill Mossakowski isDatatypeDefn t = case typeDefn t of

1b05bdb88b90d3c947351f262d7ae7d68f0a4a6fTill Mossakowski DatatypeDefn _ -> True

1b05bdb88b90d3c947351f262d7ae7d68f0a4a6fTill Mossakowski _ -> False

1b05bdb88b90d3c947351f262d7ae7d68f0a4a6fTill Mossakowski insertOps name ops m =

e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski let infos = opInfos ops

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder in if isSingle infos then

1b05bdb88b90d3c947351f262d7ae7d68f0a4a6fTill Mossakowski let transOp = transOpInfo (head infos)

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder in case transOp of

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder Just op ->

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder Map.insert (mkVName $ showIsaConstT name baseSign) op m

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder Nothing -> m

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder else

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder let transOps = map transOpInfo infos

e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski in foldl (\ m' (transOp,i) ->

1b05bdb88b90d3c947351f262d7ae7d68f0a4a6fTill Mossakowski case transOp of

e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski Just typ -> Map.insert

1b05bdb88b90d3c947351f262d7ae7d68f0a4a6fTill Mossakowski (mkVName $ showIsaConstIT name i baseSign)

1b05bdb88b90d3c947351f262d7ae7d68f0a4a6fTill Mossakowski typ m'

1b05bdb88b90d3c947351f262d7ae7d68f0a4a6fTill Mossakowski Nothing -> m')

1b05bdb88b90d3c947351f262d7ae7d68f0a4a6fTill Mossakowski m (zip transOps [1::Int ..])

1b05bdb88b90d3c947351f262d7ae7d68f0a4a6fTill Mossakowski

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder-- * translation of a type in an operation declaration

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder-- extract type from OpInfo

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder-- omit datatype constructors

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian MaedertransOpInfo :: OpInfo -> Maybe Typ

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian MaedertransOpInfo (OpInfo t _ opDef) =

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder case opDef of

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder ConstructData _ -> Nothing

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder _ -> Just (transOpType t)

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder-- operation type

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian MaedertransOpType :: TypeScheme -> Typ

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian MaedertransOpType (TypeScheme _ op _) = transType op

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder

e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski-- types

e379124f467e5d0ef7d3c0ca238bff0521f70831Till MossakowskitransType :: Type -> Typ

e379124f467e5d0ef7d3c0ca238bff0521f70831Till MossakowskitransType t = case getTypeAppl t of

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

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder if n == 0 then

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder if tid == unitTypeId && null tyArgs then boolType

e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski else if tid == lazyTypeId && num == 1 then

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder transType $ head tyArgs

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder else if isArrow tid && num == 2 then

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder let [t1, t2] = tyArgs

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder tr = transType t2

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski in mkFunType (transType t1) $

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder if isPartialArrow tid && not (isPredType t)

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder then mkOptionType tr else tr

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder else if isProductId tid && num > 1 then

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder foldl1 prodType $ map transType tyArgs

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder else Type (showIsaTypeT tid baseSign) [] $ map transType tyArgs

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder else TFree (showIsaTypeT tid baseSign) []

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder -- type arguments are not allowed here!

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder _ -> error $ "transType " ++ showDoc t "\n" ++ show t

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder-- * translation of a datatype declaration

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian MaedertransDatatype :: TypeMap -> DomainTab

e379124f467e5d0ef7d3c0ca238bff0521f70831Till MossakowskitransDatatype tm = map transDataEntry (Map.fold extractDataypes [] tm)

e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski where extractDataypes ti des = case typeDefn ti of

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder DatatypeDefn de -> des++[de]

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder _ -> des

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder-- datatype with name (tyId) + args (tyArgs) and alternatives

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian MaedertransDataEntry :: DataEntry -> [DomainEntry]

e379124f467e5d0ef7d3c0ca238bff0521f70831Till MossakowskitransDataEntry (DataEntry _ tyId Le.Free tyArgs _ alts) =

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder [(transDName tyId tyArgs, map transAltDefn alts)]

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder where transDName ti ta = Type (showIsaTypeT ti baseSign) []

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder $ map transTypeArg ta

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian MaedertransDataEntry _ = error "HasCASL2IsabelleHOL.transDataEntry"

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder-- arguments of datatype's typeconstructor

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian MaedertransTypeArg :: TypeArg -> Typ

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian MaedertransTypeArg ta = TFree (showIsaTypeT (getTypeVar ta) baseSign) []

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski-- datatype alternatives/constructors

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian MaedertransAltDefn :: AltDefn -> (VName, [Typ])

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian MaedertransAltDefn (Construct opId ts Total _) =

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder let ts' = map transType ts

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder in case opId of

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder Just opId' -> (mkVName $ showIsaConstT opId' baseSign, ts')

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder Nothing -> (mkVName "", ts')

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian MaedertransAltDefn _ = error "HasCASL2IsabelleHOL.transAltDefn"

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder-- * Formulas

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder-- simple variables

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian MaedertransVar :: Var -> VName

e379124f467e5d0ef7d3c0ca238bff0521f70831Till MossakowskitransVar v = mkVName $ showIsaConstT v baseSign

e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian MaedertransSentence :: Env -> Le.Sentence -> Maybe IsaSign.Term

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian MaedertransSentence sign s = case s of

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder Le.Formula t -> Just (transTerm sign t)

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski DatatypeSen _ -> Nothing

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski ProgEqSen _ _ _pe -> Nothing

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder-- disambiguate operation names

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian MaedertransOpId :: Env -> UninstOpId -> TypeScheme -> String

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian MaedertransOpId sign op ts =

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder case (do ops <- Map.lookup op (assumps sign)

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder if isSingle (opInfos ops) then return $ showIsaConstT op baseSign

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder else do i <- elemIndex ts (map opType (opInfos ops))

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder return $ showIsaConstIT op (i+1) baseSign) of

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder Just str -> str

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder Nothing -> showIsaConstT op baseSign

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian MaedertransProgEq :: Env -> ProgEq -> (IsaSign.Term, IsaSign.Term)

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian MaedertransProgEq sign (ProgEq pat t _) =

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder (transPattern sign pat, transPattern sign t)

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder-- terms

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian MaedertransTerm :: Env -> As.Term -> IsaSign.Term

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian MaedertransTerm sign trm = case trm of

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder QualVar (VarDecl var _ _ _) ->

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder termAppl conSome $ IsaSign.Free (transVar var)

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder QualOp _ (InstOpId opId _ _) ts _ ->

e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski if opId == trueId then true

e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski else if opId == falseId then false

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder else termAppl conSome (conDouble (transOpId sign opId ts))

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder QuantifiedTerm quan varDecls phi _ ->

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder let quantify q gvd phi' = case gvd of

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder GenVarDecl (VarDecl var _ _ _) ->

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder termAppl (conDouble $ qname q)

e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski $ Abs (IsaSign.Free $ transVar var) phi' NotCont

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder GenTypeVarDecl _ -> phi'

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder qname Universal = allS

e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski qname Existential = exS

e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski qname Unique = ex1S

e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski in foldr (quantify quan) (transTerm sign phi) varDecls

e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski TypedTerm t _ _ _ -> transTerm sign t

e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski LambdaTerm pats p body _ ->

e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski let lambdaAbs f = if null pats then termAppl conSome

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder (Abs (IsaSign.Free $ mkVName "dummyVar")

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder (f sign body) NotCont)

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder else termAppl conSome (foldr (abstraction sign)

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder (f sign body)

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder pats)

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder in case p of

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder -- distinguishes between partial and total lambda abstraction

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder -- total lambda bodies are of type 'a' instead of type 'a option'

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder Partial -> lambdaAbs transTerm

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder Total -> lambdaAbs transTotalLambda

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder LetTerm As.Let peqs body _ ->

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

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder TupleTerm ts@(_ : _) _ ->

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder foldl1 (binConst pairC) (map (transTerm sign) ts)

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder ApplTerm t1 t2 _ -> transAppl sign Nothing t1 t2

e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski CaseTerm t peqs _ ->

e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski -- flatten case alternatives

e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski let alts = arangeCaseAlts sign peqs

e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski in case t of

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder -- introduces new case statement if case variable is

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder -- a term application that may evaluate to 'Some x' or 'None'

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder QualVar (VarDecl decl _ _ _) ->

e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski Case (IsaSign.Free (transVar decl)) alts

e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski _ -> Case (transTerm sign t)

e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski [(conDouble "None", conDouble "None"),

e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski (App conSome (IsaSign.Free (mkVName "caseVar")) NotCont,

21dae7237ac384abdb94a81e00b3f099873ec623Till Mossakowski Case (IsaSign.Free (mkVName "caseVar")) alts)]

e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski _ -> error $ "HasCASL2IsabelleHOL.transTerm " ++ showDoc trm "\n"

e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski ++ show trm

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian MaedertransAppl :: Env -> Maybe As.Type -> As.Term -> As.Term -> IsaSign.Term

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian MaedertransAppl s typ t' t'' = case t'' of

e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski TupleTerm [] _ -> transTerm s t'

e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski _ -> case t' of

e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski QualVar (VarDecl _ ty _ _) -> transApplOp s ty t' t''

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder QualOp _ (InstOpId opId _ _) (TypeScheme _ ty _) _ ->

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder if elem opId $ map fst bList then

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder -- logical formulas are translated seperatly (transLog)

e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski if opId == whenElse then transWhenElse s t''

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder else transLog s opId t' t''

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder else transApplOp s ty t' t''

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder -- distinguishes between partial and total term application

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

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

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder ( \ ty -> transApplOp s ty t' t'') typ

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian MaedermkApp :: String -> Env -> As.Term -> As.Term -> IsaSign.Term

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian MaedermkApp s sg tt tt' = termAppl (termAppl (conDouble s) (transTerm sg tt))

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder (transTerm sg tt')

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian MaedertransApplOp :: Env -> As.Type -> As.Term -> As.Term -> IsaSign.Term

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian MaedertransApplOp s typ tt tt' = if isPredType typ then mkApp "pApp" s tt tt'

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder else case getTypeAppl typ of

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

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

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder else mkApp "apt" s tt tt'

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder _ -> mkApp "app" s tt tt'

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder-- translation formulas with logical connectives

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian MaedertransLog :: Env -> Id -> As.Term -> As.Term -> IsaSign.Term

e379124f467e5d0ef7d3c0ca238bff0521f70831Till MossakowskitransLog sign opId opTerm t = case t of

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder TupleTerm [l' , r'] _

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder | opId == andId -> binConj l r

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder | opId == orId -> binDisj l r

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder | opId == implId -> binImpl l r

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder | opId == infixIf -> binImpl r l

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder | opId == eqvId -> binEq l r

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

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder binConj (termAppl defOp l) $

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder termAppl defOp r

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder | opId == eqId -> binEq l r

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder where l = transTerm sign l'

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder r = transTerm sign r'

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

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

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

e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder-- | when else statement

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian MaedertransWhenElse :: Env -> As.Term -> IsaSign.Term

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian MaedertransWhenElse sign t =

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder case t of

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder TupleTerm terms _ ->

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder let ts = (map (transTerm sign) terms)

e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski in case ts of

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

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder _ -> error "HasCASL2IsabelleHOL.transWhenElse.tuple"

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder _ -> error "HasCASL2IsabelleHOL.transWhenElse"

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder-- * translation of lambda abstractions

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder-- form Abs(pattern term)

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maederabstraction :: Env -> As.Term -> IsaSign.Term -> IsaSign.Term

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maederabstraction sign pat body =

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder Abs (transPattern sign pat) body NotCont where

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder-- Abs (transPattern sign pat) body NotCont where

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder getType t =

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder case t of

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder QualVar (VarDecl _ typ _ _) -> transType typ

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder TypedTerm _ _ typ _ -> transType typ

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder TupleTerm terms _ -> evalTupleType terms

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder _ ->

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder error "HasCASL2IsabelleHOL.abstraction"

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder evalTupleType t = foldr1 prodType (map getType t)

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder-- translation of lambda patterns

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

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian MaedertransPattern :: Env -> As.Term -> IsaSign.Term

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian MaedertransPattern _ (QualVar (VarDecl var _ _ _)) =

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder IsaSign.Free (transVar var)

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian MaedertransPattern sign (TupleTerm terms@(_ : _) _) =

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder foldl1 (binConst isaPair) $ map (transPattern sign) terms

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian MaedertransPattern _ (QualOp _ (InstOpId opId _ _) _ _) =

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder conDouble $ showIsaConstT opId baseSign

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian MaedertransPattern sign (TypedTerm t _ _ _) = transPattern sign t

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian MaedertransPattern sign (ApplTerm t1 t2 _) =

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder App (transPattern sign t1) (transPattern sign t2) NotCont

e379124f467e5d0ef7d3c0ca238bff0521f70831Till MossakowskitransPattern sign t = transTerm sign t

e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski

e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski-- translation of total lambda abstraction bodies

e379124f467e5d0ef7d3c0ca238bff0521f70831Till MossakowskitransTotalLambda :: Env -> As.Term -> IsaSign.Term

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian MaedertransTotalLambda _ (QualVar (VarDecl var _ _ _)) =

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder IsaSign.Free (transVar var)

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian MaedertransTotalLambda sign t@(QualOp _ (InstOpId opId _ _) _ _) =

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder if opId == trueId || opId == falseId then transTerm sign t

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder else conDouble $ showIsaConstT opId baseSign

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian MaedertransTotalLambda sign (ApplTerm term1 term2 _) =

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder termAppl (transTotalLambda sign term1) $ transTotalLambda sign term2

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

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian MaedertransTotalLambda sign (LambdaTerm pats part body _) =

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder case part of

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder Partial -> lambdaAbs transTerm

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder Total -> lambdaAbs transTotalLambda

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder where

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder lambdaAbs f =

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

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder (f sign body) NotCont

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

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder else foldr (abstraction sign) (f sign body) pats

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian MaedertransTotalLambda sign (TupleTerm terms@(_ : _) _) =

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder foldl1 (binConst isaPair) $ map (transTotalLambda sign) terms

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian MaedertransTotalLambda sign (CaseTerm t pEqs _) =

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder Case (transTotalLambda sign t) $ map transCaseAltTotal pEqs

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder where transCaseAltTotal (ProgEq pat trm _) =

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder (transPat sign pat, transTotalLambda sign trm)

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian MaedertransTotalLambda sign t = transTerm sign t

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder-- * translation of case alternatives

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder{- Annotation concerning Patterns:

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder Following the HasCASL-Summary and the limits of the encoding

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

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder QualVar, QualOp, ApplTerm, TupleTerm and TypedTerm

e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski-}

e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski

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

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

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder-- translated

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian MaederarangeCaseAlts :: Env -> [ProgEq]-> [(IsaSign.Term, IsaSign.Term)]

e379124f467e5d0ef7d3c0ca238bff0521f70831Till MossakowskiarangeCaseAlts sign peqs

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

e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski | otherwise = sortCaseAlts sign peqs

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder

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

c616e681da8c052b62e14247fea522da099ac0e4Christian Maeder datatype constructors (with arguments) or tupels

e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski Functionality: Groups case alternatives by leading

74e82e43f5787027c5d4e523397525a259d6d001Christian Maeder pattern-constructor each pattern group is flattened

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder-}

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

74e82e43f5787027c5d4e523397525a259d6d001Christian MaedersortCaseAlts sign peqs =

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder let consList

e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski | null peqs = error "No case alternatives."

74e82e43f5787027c5d4e523397525a259d6d001Christian Maeder | otherwise = getCons sign (getName (head peqs))

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder groupedByCons = nub (map (groupCons peqs) consList)

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder in map (flattenPattern sign) groupedByCons

e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski

74e82e43f5787027c5d4e523397525a259d6d001Christian Maeder-- Returns a list of the constructors of the used datatype

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian MaedergetCons :: Env -> TypeId -> [UninstOpId]

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian MaedergetCons sign tyId =

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder extractIds (typeDefn (findInMap tyId (typeMap sign)))

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder where extractIds (DatatypeDefn (DataEntry _ _ _ _ _ altDefns)) =

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder catMaybes (map stripConstruct altDefns)

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder extractIds _ = error "HasCASL2Isabelle.extractIds"

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder stripConstruct (Construct i _ _ _) = i

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder findInMap :: Ord k => k -> Map.Map k a -> a

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

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder Map.lookup k m

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder-- Extracts the type of the used datatype in case patterns

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian MaedergetName :: ProgEq -> TypeId

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian MaedergetName (ProgEq pat _ _) = (getTypeName pat)

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder

e379124f467e5d0ef7d3c0ca238bff0521f70831Till MossakowskigetTypeName :: Pattern -> TypeId

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian MaedergetTypeName p =

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder case p of

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder QualVar (VarDecl _ typ _ _) -> name typ

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder QualOp _ _ (TypeScheme _ typ _) _ -> name typ

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder TypedTerm _ _ typ _ -> name typ

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder ApplTerm t _ _ -> getTypeName t

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder TupleTerm ts _ -> getTypeName (head ts)

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder _ -> error "HasCASL2IsabelleHOL.getTypeName"

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder where name tp = case getTypeAppl tp of

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

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder if isArrow tyId && num == 2 then

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder name $ head $ tail tyArgs

e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski else if isProductId tyId && num > 1 then

e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski name $ head tyArgs

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder else tyId

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

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder-- Input: Case alternatives and name of one constructor

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder-- Functionality: Filters case alternatives by constructor's name

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian MaedergroupCons :: [ProgEq] -> UninstOpId -> [ProgEq]

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian MaedergroupCons peqs name = filter hasSameName peqs

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder where hasSameName (ProgEq pat _ _) =

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder hsn pat

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder hsn pat =

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder case pat of

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder QualOp _ (InstOpId n _ _) _ _ -> n == name

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder ApplTerm t1 _ _ -> hsn t1

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder TypedTerm t _ _ _ -> hsn t

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder TupleTerm _ _ -> True

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder _ -> False

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder-- Input: List of case alternatives with same leading constructor

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

e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski-- translates case alternatives

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

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian MaederflattenPattern sign peqs = case peqs of

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

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder [h] -> transCaseAlt sign h

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

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder -- or the 'TypedTerm' variant of one of them

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

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder transCaseAlt sign (ProgEq (shrinkPat m) (term m) nullRange)

e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski

e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowskidata CaseMatrix = CaseMatrix { patBrand :: PatBrand,

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder cons :: Maybe As.Term,

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder args :: [Pattern],

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder newArgs :: [Pattern],

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder term :: As.Term } deriving (Show)

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maederdata PatBrand = Appl | Tuple | QuOp | QuVar deriving (Eq, Show)

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maederinstance Eq CaseMatrix where

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder (==) cmx cmx' = (patBrand cmx == patBrand cmx')

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder && (args cmx == args cmx')

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder && (term cmx == term cmx')

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder && (cons cmx == cons cmx')

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder && (newArgs cmx == newArgs cmx')

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder

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

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

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder be executed if the pattern matched. Then the resulting list of

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

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

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

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder n patterns are reduced to one pattern.

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

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder for each constructor.

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder -}

e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski

e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski-- Functionality: turns ProgEq into CaseMatrix

e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowskimatricize :: [ProgEq] -> [CaseMatrix]

e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowskimatricize = map matriPEq

e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian MaedermatriPEq :: ProgEq -> CaseMatrix

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian MaedermatriPEq (ProgEq pat altTerm _) = matriArg pat altTerm

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian MaedermatriArg :: Pattern -> As.Term -> CaseMatrix

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian MaedermatriArg pat cTerm =

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder case pat of

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder ApplTerm t1 t2 _ -> let (c, p) = stripAppl t1 (Nothing, [])

e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski in

e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski CaseMatrix { patBrand = Appl,

e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski cons = c,

e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski args = p ++ [t2],

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder newArgs = [],

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder term = cTerm }

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder TupleTerm ts _ -> CaseMatrix { patBrand = Tuple,

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder cons = Nothing,

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder args = ts,

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder newArgs = [],

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder term = cTerm }

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder TypedTerm t _ _ _ -> matriArg t cTerm

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder qv@(QualVar _) -> CaseMatrix { patBrand = QuVar,

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder cons = Nothing,

e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski args = [qv],

74e82e43f5787027c5d4e523397525a259d6d001Christian Maeder newArgs = [],

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder term = cTerm }

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder qo@(QualOp _ _ _ _) -> CaseMatrix { patBrand = QuOp,

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder cons = Nothing,

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder args = [qo],

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder newArgs = [],

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder term = cTerm }

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder _ -> error "HasCASL2IsabelleHOL.matriArg"

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

e3c9174a782e90f965a0b080c22861c3ef5af12dTill Mossakowski-- is a QualOp, that is a datatype constructor

e3c9174a782e90f965a0b080c22861c3ef5af12dTill Mossakowski where stripAppl ct tp = case ct of

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

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

21dae7237ac384abdb94a81e00b3f099873ec623Till Mossakowski TypedTerm (ApplTerm (TypedTerm

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

21dae7237ac384abdb94a81e00b3f099873ec623Till Mossakowski TypedTerm (ApplTerm t' t'' _) _ _ _ ->

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

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

e3c9174a782e90f965a0b080c22861c3ef5af12dTill Mossakowski ApplTerm (TypedTerm

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

e3c9174a782e90f965a0b080c22861c3ef5af12dTill Mossakowski ApplTerm t' t'' _ ->

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

e3c9174a782e90f965a0b080c22861c3ef5af12dTill Mossakowski-- TypedTerm t' _ _ _ -> stripAppl t' tp

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

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

e3c9174a782e90f965a0b080c22861c3ef5af12dTill Mossakowski

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

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

e3c9174a782e90f965a0b080c22861c3ef5af12dTill Mossakowski-- that only differ in their last argument

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

e3c9174a782e90f965a0b080c22861c3ef5af12dTill Mossakowskiconcentrate :: [CaseMatrix] -> Env -> CaseMatrix

21dae7237ac384abdb94a81e00b3f099873ec623Till Mossakowskiconcentrate cmxs sign = case map (redArgs sign) $

21dae7237ac384abdb94a81e00b3f099873ec623Till Mossakowski nub $ map (groupByArgs cmxs) [0..(length cmxs-1)] of

21dae7237ac384abdb94a81e00b3f099873ec623Till Mossakowski [h] -> h

21dae7237ac384abdb94a81e00b3f099873ec623Till Mossakowski l -> concentrate l sign

21dae7237ac384abdb94a81e00b3f099873ec623Till Mossakowski

e3c9174a782e90f965a0b080c22861c3ef5af12dTill MossakowskigroupByArgs :: [CaseMatrix] -> Int -> [CaseMatrix]

e3c9174a782e90f965a0b080c22861c3ef5af12dTill MossakowskigroupByArgs cmxs i

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

e3c9174a782e90f965a0b080c22861c3ef5af12dTill Mossakowski | otherwise = (filter equalPat cmxs)

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

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder equalPat cmx = isSingle (args cmx) || init (args cmx) == patE

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder

4184cb191a9081cb2a9cf3ef5f060f56f0ca5922Till MossakowskiredArgs :: Env -> [CaseMatrix] -> CaseMatrix

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian MaederredArgs sign cmxs

4184cb191a9081cb2a9cf3ef5f060f56f0ca5922Till Mossakowski | and (map (testPatBrand Appl) cmxs) = redAppl cmxs sign

4184cb191a9081cb2a9cf3ef5f060f56f0ca5922Till Mossakowski | and (map (testPatBrand Tuple) cmxs) = redAppl cmxs sign

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder | isSingle cmxs = head cmxs

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder | otherwise = head cmxs

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder where testPatBrand pb cmx = pb == patBrand cmx

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder

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

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder the last one are equal

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

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder pattern (perhaps a new variable

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder-}

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian MaederredAppl :: [CaseMatrix] -> Env -> CaseMatrix

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian MaederredAppl cmxs sign

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder | and (map null (map args cmxs)) = head cmxs

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder | isSingle cmxs =

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder (head cmxs) { args = init $ args $ head cmxs,

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder newArgs = last (args $ head cmxs) : newArgs (head cmxs) }

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder | and (map termIsVar lastArgs) = substVar (head cmxs)

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder | otherwise = substTerm (head cmxs)

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder where terms = map term cmxs

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski lastArgs = map last (map args cmxs)

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

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder varId = (mkId [(mkSimpleId varName)])

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder newVar = QualVar (VarDecl varId (TypeName varId rStar 1)

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder Other nullRange)

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder newPeqs = (map newProgEq (zip lastArgs terms))

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder newPeqs' = recArgs sign newPeqs

4184cb191a9081cb2a9cf3ef5f060f56f0ca5922Till Mossakowski substVar cmx

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder | null (args cmx) = cmx

4184cb191a9081cb2a9cf3ef5f060f56f0ca5922Till Mossakowski | isSingle (args cmx) =

4184cb191a9081cb2a9cf3ef5f060f56f0ca5922Till Mossakowski cmx { args = [],

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder newArgs = last(args cmx) : (newArgs cmx) }

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder | otherwise =

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder cmx { args = init (args cmx),

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder newArgs = last(args cmx) : (newArgs cmx) }

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder substTerm cmx

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder | null (args cmx) = cmx

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder | isSingle (args cmx) =

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder cmx { args = [],

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder newArgs = newVar : (newArgs cmx),

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski term = CaseTerm newVar newPeqs' nullRange }

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski | otherwise =

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder cmx { args = init(args cmx),

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder newArgs = newVar : (newArgs cmx),

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder term = CaseTerm newVar newPeqs' nullRange }

4184cb191a9081cb2a9cf3ef5f060f56f0ca5922Till Mossakowski newProgEq (p, t) = ProgEq p t nullRange

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder-- Input: ProgEqs that were build to replace an argument

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder-- with a case statement

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder-- Functionality:

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian MaederrecArgs :: Env -> [ProgEq] -> [ProgEq]

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian MaederrecArgs sign peqs

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder | isSingle groupedByCons

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder || null groupedByCons = []

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder | otherwise = doPEQ groupedByCons []

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder where consList

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder | null peqs = error "No case alternatives."

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder | otherwise = getCons sign (getName (head peqs))

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder groupedByCons = map (groupCons peqs) consList

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder doPEQ [] res = res

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder doPEQ (g:gByCs) res

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

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

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder toPEQ cmx = ProgEq (shrinkPat cmx) (term cmx) nullRange

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder testPEQs sig ps

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder | null peqs = error "HasCASL2IsabelleHOL.testPEQs"

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder | otherwise = concentrate (matricize ps) sig

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder-- accumulates arguments of caseMatrix to one pattern

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian MaedershrinkPat :: CaseMatrix -> As.Term

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian MaedershrinkPat cmx =

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder case patBrand cmx of

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder Appl -> case cons cmx of

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

c616e681da8c052b62e14247fea522da099ac0e4Christian Maeder Nothing -> error "HasCASL2IsabelleHOL.shrinkPat"

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder Tuple -> TupleTerm ((args cmx) ++ (newArgs cmx)) nullRange

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder QuOp -> head (args cmx)

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder _ -> head (newArgs cmx)

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder where mkApplT t1 t2 = ApplTerm t1 t2 nullRange

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian MaederpatIsVar :: ProgEq -> Bool

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian MaederpatIsVar (ProgEq pat _ _) = termIsVar pat

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian MaedertermIsVar :: As.Term -> Bool

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian MaedertermIsVar t = case t of

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder QualVar _ -> True

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder TypedTerm tr _ _ _ -> termIsVar tr

e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski TupleTerm ts _ -> and (map termIsVar ts)

e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski _ -> False

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian MaederpatHasNoArg :: ProgEq -> Bool

e379124f467e5d0ef7d3c0ca238bff0521f70831Till MossakowskipatHasNoArg (ProgEq pat _ _) = termHasNoArg pat

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian MaedertermHasNoArg :: As.Term -> Bool

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian MaedertermHasNoArg t = case t of

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder QualOp _ _ _ _ -> True

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder TypedTerm tr _ _ _ -> termHasNoArg tr

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder _ -> False

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian MaedertransCaseAlt :: Env -> ProgEq -> (IsaSign.Term, IsaSign.Term)

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian MaedertransCaseAlt sign (ProgEq pat trm _) =

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder (transPat sign pat, (transTerm sign trm))

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian MaedertransPat :: Env -> As.Term -> IsaSign.Term

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian MaedertransPat _ (QualVar (VarDecl var _ _ _)) =

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder IsaSign.Free (transVar var)

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian MaedertransPat sign (ApplTerm term1 term2 _) =

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder termAppl (transPat sign term1) (transPat sign term2)

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian MaedertransPat sign (TypedTerm trm _ _ _) = transPat sign trm

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian MaedertransPat sign (TupleTerm terms@(_ : _) _) =

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder foldl1 (binConst isaPair) (map (transPat sign) terms)

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian MaedertransPat _ (QualOp _ (InstOpId i _ _) _ _) =

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder conDouble (showIsaConstT i baseSign)

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian MaedertransPat _ _ = error "HasCASL2IsabelleHOL.transPat"

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder-- | apply binary operation to arguments

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian MaederbinConst :: String -> IsaSign.Term -> IsaSign.Term -> IsaSign.Term

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian MaederbinConst s = binVNameAppl $ mkVName s

e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski

e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski-- | upper case curried pair constructor

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian MaederisaPair :: String

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian MaederisaPair = "Pair"

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder