{- |

Module : $Header$

Copyright : (c) Uni Bremen 2003 - 2005

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

Maintainer : maeder@tzi.de

Stability : provisional

Portability : non-portable (imports Logic.Logic)

The embedding comorphism from HasCASL to Isabelle-HOL.

-}

module Comorphisms.HasCASL2IsabelleHOL where

import Logic.Logic as Logic

import Logic.Comorphism

import Common.Id

import Common.Result

import qualified Common.Lib.Map as Map

import Data.List

import Data.Maybe

import Common.AS_Annotation (Named(..))

import Common.PrettyPrint

-- HasCASL

import HasCASL.Logic_HasCASL

import HasCASL.Sublogic

import HasCASL.Le as Le

import HasCASL.As as As

import HasCASL.AsUtils

import HasCASL.Builtin

-- Isabelle

import Isabelle.IsaSign as IsaSign

import Isabelle.IsaConsts

import Isabelle.Logic_Isabelle

import Isabelle.Translate

-- | The identity of the comorphism

data HasCASL2IsabelleHOL = HasCASL2IsabelleHOL deriving (Show)

instance Language HasCASL2IsabelleHOL -- default definition is okay

instance Comorphism HasCASL2IsabelleHOL

HasCASL HasCASL_Sublogics

BasicSpec Le.Sentence SymbItems SymbMapItems

Env Morphism

Symbol RawSymbol ()

Isabelle () () IsaSign.Sentence () ()

IsaSign.Sign

IsabelleMorphism () () () where

sourceLogic HasCASL2IsabelleHOL = HasCASL

sourceSublogic HasCASL2IsabelleHOL = HasCASL_SL

{ has_sub = False, -- subsorting

has_part = True, -- partiality

has_eq = True, -- equality

has_pred = True, -- predicates

has_ho = True, -- higher order

has_type_classes = False,

has_polymorphism = True,

has_type_constructors = True,

which_logic = HOL

}

targetLogic HasCASL2IsabelleHOL = Isabelle

targetSublogic HasCASL2IsabelleHOL = ()

map_theory HasCASL2IsabelleHOL = mkTheoryMapping transSignature

(map_sentence HasCASL2IsabelleHOL)

map_morphism HasCASL2IsabelleHOL mor = do

(sig1,_) <- map_sign HasCASL2IsabelleHOL (Logic.dom HasCASL mor)

(sig2,_) <- map_sign HasCASL2IsabelleHOL (cod HasCASL mor)

inclusion Isabelle sig1 sig2

map_sentence HasCASL2IsabelleHOL sign phi =

case transSentence sign phi of

Nothing -> warning (Sentence {senTerm = true})

"translation of sentence not implemented" nullRange

Just (ts) -> return $ Sentence {senTerm = ts}

map_symbol HasCASL2IsabelleHOL _ = error "HasCASL2IsabelleHOL.map_symbol"

-- ============================ Signature ================================== --

baseSign :: BaseSig

baseSign = MainHC_thy

transSignature :: Env

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

transSignature sign =

return (IsaSign.emptySign {

baseSig = baseSign,

-- translation of typeconstructors

tsig = emptyTypeSig

{ arities = Map.foldWithKey extractTypeName

Map.empty

(typeMap sign) },

-- translation of operation declarations

constTab = Map.foldWithKey insertOps

Map.empty

(assumps sign),

-- translation of datatype declarations

dataTypeTab = transDatatype (typeMap sign),

showLemmas = True },

[] )

where

extractTypeName tyId typeInfo m =

if isDatatypeDefn typeInfo then m

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

-- translate the kind here!

isDatatypeDefn t = case typeDefn t of

DatatypeDefn _ -> True

_ -> False

insertOps name ops m =

let infos = opInfos ops

in if isSingle infos then

let transOp = transOpInfo (head infos)

in case transOp of

Just op ->

Map.insert (VName {new=showIsaConstT name baseSign,orig=show name}) op m

Nothing -> m

else

let transOps = map transOpInfo infos

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

case transOp of

Just typ -> Map.insert (VName {new=showIsaConstIT name i baseSign,

orig=show name ++ show i})

typ m'

Nothing -> m')

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

---------- translation of a type in an operation declaration ----------

-- extract type from OpInfo

-- omit datatype constructors

transOpInfo :: OpInfo -> Maybe Typ

transOpInfo (OpInfo t _ opDef) =

case opDef of

ConstructData _ -> Nothing

_ -> Just (transOpType t)

-- operation type

transOpType :: TypeScheme -> Typ

transOpType (TypeScheme _ op _) = transType op

-- types

transType :: Type -> Typ

transType t = case getTypeAppl t of

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

if n == 0 then

if tid == unitTypeId && null tyArgs then boolType

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

transType $ head tyArgs

else if isArrow tid && num == 2 then

let [t1, t2] = tyArgs

tr = transType t2

in mkFunType (transType t1) $

if isPartialArrow tid && not (isPredType t)

then mkOptionType tr else tr

else if isProductId tid && num > 1 then

foldl1 IsaSign.prodType $ map transType tyArgs

else foldl binTypeAppl (Type (showIsaTypeT tid baseSign) [] [])

$ map transType tyArgs

else foldl binTypeAppl (TFree (showIsaTypeT tid baseSign) [])

$ map transType tyArgs

_ -> error $ "transType " ++ showPretty t "\n" ++ show t

---------- translation of a datatype declaration ----------

transDatatype :: TypeMap -> DataTypeTab

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

where extractDataypes ti des = case typeDefn ti of

DatatypeDefn de -> des++[de]

_ -> des

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

transDataEntry :: DataEntry -> DataTypeTabEntry

transDataEntry (DataEntry _ tyId Le.Free tyArgs _ alts) =

[((transDName tyId tyArgs), (map transAltDefn alts))]

where transDName ti ta = Type (showIsaTypeT ti baseSign) [] (map transTypeArg ta)

transDataEntry _ = error "HasCASL2IsabelleHOL.transDataEntry"

-- arguments of datatype's typeconstructor

transTypeArg :: TypeArg -> Typ

transTypeArg ta = TFree (showIsaTypeT (getTypeVar ta) baseSign) []

-- datatype alternatives/constructors

transAltDefn :: AltDefn -> DataTypeAlt

transAltDefn (Construct opId ts Total _) =

let ts' = map transType ts

in case opId of

Just opId' -> ((VName {new=showIsaConstT opId' baseSign,

orig=show opId'}), ts')

Nothing -> ((VName {new="",orig=""}), ts')

transAltDefn _ = error "HasCASL2IsabelleHOL.transAltDefn"

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

-- simple variables

transVar :: Var -> VName

transVar v = mkVName $ showIsaConstT v baseSign

transSentence :: Env -> Le.Sentence -> Maybe IsaSign.Term

transSentence sign s = case s of

Le.Formula t -> Just (transTerm sign t)

DatatypeSen _ -> Nothing

ProgEqSen _ _ _pe -> Nothing

-- disambiguate operation names

transOpId :: Env -> UninstOpId -> TypeScheme -> String

transOpId sign op ts =

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

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

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

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

Just str -> str

Nothing -> showIsaConstT op baseSign

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

transProgEq sign (ProgEq pat t _) =

(transPattern sign pat, transPattern sign t)

-- terms

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

transTerm sign trm = case trm of

QualVar (VarDecl var t _ _) ->

let t' = transType t

ot = mkFunType t' $ mkOptionType t'

in termAppl (conSomeT ot) $ IsaSign.Free (transVar var) t'

QualOp _ (InstOpId opId _ _) ts _ ->

if opId == trueId then conDouble "True"

else if opId == falseId then conDouble "False"

else termAppl conSome (conDouble (transOpId sign opId ts))

QuantifiedTerm quan varDecls phi _ ->

let quantify q gvd phi' = case gvd of

GenVarDecl (VarDecl var typ _ _) ->

termAppl (conDouble $ qname q)

$ Abs (con $ transVar var) (transType typ) phi' NotCont

GenTypeVarDecl _ -> phi'

qname Universal = allS

qname Existential = exS

qname Unique = ex1S

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

TypedTerm t _ _ _ -> transTerm sign t

LambdaTerm pats p body _ ->

let lambdaAbs f = if null pats then termAppl conSome

(Abs (IsaSign.Free (mkVName "dummyVar") noType)

noType (f sign body) NotCont)

else termAppl conSome (foldr (abstraction sign)

(f sign body)

pats)

in case p of

-- distinguishes between partial and total lambda abstraction

-- total lambda bodies are of type 'a' instead of type 'a option'

Partial -> lambdaAbs transTerm

Total -> lambdaAbs transTotalLambda

LetTerm As.Let peqs body _ ->

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

TupleTerm ts@(_ : _) _ ->

foldl1 (binConst pairC) (map (transTerm sign) ts)

ApplTerm t1 t2 _ -> transAppl sign Nothing t1 t2

CaseTerm t peqs _ ->

-- flatten case alternatives

let alts = arangeCaseAlts sign peqs

in case t of

-- introduces new case statement if case variable is

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

QualVar (VarDecl decl _ _ _) ->

Case (IsaSign.Free (transVar decl) noType) alts

_ -> Case (transTerm sign t)

[(conDouble "None", conDouble "None"),

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

Case (IsaSign.Free (mkVName "caseVar") noType) alts)]

_ -> error $ "HasCASL2IsabelleHOL.transTerm " ++ showPretty trm "\n"

++ show trm

transAppl :: Env -> Maybe As.Type -> As.Term -> As.Term -> IsaSign.Term

transAppl s typ t' t'' = case t'' of

TupleTerm [] _ -> transTerm s t'

_ -> case t' of

QualVar (VarDecl _ ty _ _) -> if isPredType ty

then mkApp "pApp" s t' t''

else transApplOp s ty t' t''

QualOp _ (InstOpId opId _ _) (TypeScheme _ ty _) _ ->

if elem opId $ map fst bList then

-- logical formulas are translated seperatly (transLog)

if opId == whenElse then transWhenElse s t''

else transLog s opId t' t''

else if isPredType ty then mkApp "pApp" s 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'') typ

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 typ tt tt' = case getTypeAppl typ 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 -> binConst conj l r

| opId == orId -> binConst disj l r

| opId == implId -> binConst impl l r

| opId == infixIf -> binConst impl r l

| opId == eqvId -> binConst eqv l r

| opId == exEq -> binConst conj (binConst eq l r) $

binConst conj (termAppl defOp l) $

termAppl defOp r

| opId == eqId -> binConst eq 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) (getType pat) body NotCont where

-- Abs (transPattern sign pat) body NotCont where

getType t =

case t of

QualVar (VarDecl _ typ _ _) -> transType typ

TypedTerm _ _ typ _ -> transType typ

TupleTerm terms _ -> evalTupleType terms

_ ->

error "HasCASL2IsabelleHOL.abstraction"

evalTupleType t = foldr1 IsaSign.prodType (map getType t)

-- 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 typ _ _)) =

IsaSign.Free (transVar var) $ transType typ

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

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

transPattern _ (QualOp _ (InstOpId 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 typ _ _)) =

IsaSign.Free (transVar var) (transType typ)

transTotalLambda sign t@(QualOp _ (InstOpId 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 (VName {new="dummyVar",orig="dummyVar"}) noType)

noType (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 = Data.List.nub (map (groupCons peqs) consList)

in map (flattenPattern sign) groupedByCons

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

getCons :: Env -> TypeId -> [UninstOpId]

getCons sign tyId =

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

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

catMaybes (map stripConstruct 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 -> TypeId

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

getTypeName :: Pattern -> TypeId

getTypeName p =

case p of

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

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

TypedTerm _ _ typ _ -> name typ

ApplTerm t _ _ -> getTypeName t

TupleTerm ts _ -> getTypeName (head ts)

_ -> 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] -> UninstOpId -> [ProgEq]

groupCons peqs name = filter hasSameName peqs

where hasSameName (ProgEq pat _ _) =

hsn pat

hsn pat =

case pat of

QualOp _ (InstOpId 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 :: [Pattern],

newArgs :: [Pattern],

term :: As.Term } deriving (Show)

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

instance Eq CaseMatrix where

(==) cmx cmx' = (patBrand cmx == patBrand cmx')

&& (args cmx == args cmx')

&& (term cmx == term cmx')

&& (cons cmx == cons cmx')

&& (newArgs cmx == newArgs cmx')

{- 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 :: Pattern -> 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)

-- TypedTerm t' _ _ _ -> stripAppl t' 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) $

nub $ 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)

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) noType

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 _ (InstOpId i _ _) _ _) =

conDouble (showIsaConstT i baseSign)

transPat _ _ = error "HasCASL2IsabelleHOL.transPat"