content: {-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}
  {- |
  Module      :  ./Comorphisms/HasCASL2IsabelleHOL.hs
  Description :  old translation that is only better for case terms
  Copyright   :  (c) Sonja Groening, C. Maeder, Uni Bremen 2003-2006
  License     :  GPLv2 or higher, see LICENSE.txt
  
  Maintainer  :  Christian.Maeder@dfki.de
  Stability   :  provisional
  Portability :  non-portable (imports Logic.Logic)
  
  This embedding comorphism from HasCASL to Isabelle-HOL is an old
  version that can be deleted as soon as case terms are implemented elsewhere
  -}
  
  module Comorphisms.HasCASL2IsabelleHOL where
  
  import Logic.Logic as Logic
  import Logic.Comorphism
  
  import HasCASL.Logic_HasCASL
  import HasCASL.Sublogic
  import HasCASL.Le as Le
  import HasCASL.As as As
  import HasCASL.AsUtils
  import HasCASL.Builtin
  
  import Isabelle.IsaSign as IsaSign hiding (qname)
  import Isabelle.IsaConsts
  import Isabelle.Logic_Isabelle
  import Isabelle.Translate
  
  import Common.DocUtils
  import Common.Id
  import Common.Result
  import Common.Utils
  import qualified Data.Map as Map
  import qualified Data.Set as Set
  import Common.AS_Annotation
  
  import Data.List (elemIndex)
  import Data.Maybe
  
  -- | The identity of the comorphism
  data HasCASL2IsabelleHOL = HasCASL2IsabelleHOL deriving Show
  
  instance Language HasCASL2IsabelleHOL where
    language_name HasCASL2IsabelleHOL = "HasCASL2IsabelleDeprecated"
  
  instance Comorphism HasCASL2IsabelleHOL
                 HasCASL Sublogic
                 BasicSpec Le.Sentence SymbItems SymbMapItems
                 Env Morphism
                 Symbol RawSymbol ()
                 Isabelle () () IsaSign.Sentence () ()
                 IsaSign.Sign
                 IsabelleMorphism () () () where
      sourceLogic HasCASL2IsabelleHOL = HasCASL
      sourceSublogic HasCASL2IsabelleHOL = sublogic_min noSubtypes noClasses
      targetLogic HasCASL2IsabelleHOL = Isabelle
      mapSublogic cid sl = if sl `isSubElem` sourceSublogic cid
                         then Just () else Nothing
      map_theory HasCASL2IsabelleHOL = mkTheoryMapping transSignature
                     (map_sentence HasCASL2IsabelleHOL)
      map_sentence HasCASL2IsabelleHOL sign phi =
         case transSentence sign phi of
           Nothing -> warning (mkSen true)
                             "translation of sentence not implemented" nullRange
           Just ts -> return $ mkSen ts
      isInclusionComorphism HasCASL2IsabelleHOL = True
  
  -- * 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.foldrWithKey extractTypeName
                                          Map.empty
                                          (typeMap sign) },
      -- translation of operation declarations
      constTab = Map.foldrWithKey insertOps
                                 Map.empty
                                 (assumps sign),
      -- translation of datatype declarations
      domainTab = 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 =
            if isSingleton ops then
              let transOp = transOpInfo (Set.findMin ops)
              in case transOp of
                   Just op ->
                       Map.insert (mkVName $ showIsaConstT name baseSign) op m
                   Nothing -> m
            else
              let transOps = map transOpInfo $ Set.toList ops
              in foldl (\ m' (transOp, i) ->
                             case transOp of
                               Just ty -> Map.insert
                                   (mkVName $ showIsaConstIT name i baseSign)
                                   ty m'
                               Nothing -> m')
                        m $ number transOps
  
  -- * 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) ->
        if n == 0 then case tyArgs of
            [] | tid == unitTypeId -> boolType
            [t1] | tid == lazyTypeId -> transType t1
            t1 : t2 : r
              | isArrow tid && null r -> let tr = transType t2 in
                  mkFunType (transType t1) $
                      if isPartialArrow tid && not (isPredType t)
                          then mkOptionType tr else tr
              | isProductId tid -> foldl1 prodType $ map transType tyArgs
            _ -> Type (showIsaTypeT tid baseSign) [] $ map transType tyArgs
         else TFree (showIsaTypeT tid baseSign) []
              -- type arguments are not allowed here!
     _ -> error $ "transType " ++ showDoc t "\n" ++ show t
  
  -- * translation of a datatype declaration
  
  transDatatype :: TypeMap -> DomainTab
  transDatatype tm = map transDataEntry (Map.foldr 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 -> [DomainEntry]
  transDataEntry (DataEntry _ tyId Le.Free tyArgs _ alts) =
      [(transDName tyId tyArgs, map transAltDefn $ Set.toList 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 -> (VName, [Typ])
  transAltDefn (Construct opId ts Total _) =
     let ts' = map transType ts
     in case opId of
          Just opId' -> (mkVName $ showIsaConstT opId' baseSign, ts')
          Nothing -> (mkVName "", ts')
  transAltDefn _ = error "HasCASL2IsabelleHOL.transAltDefn"
  
  -- * Formulas
  
  -- simple variables
  transVar :: Id -> 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 -> Id -> TypeScheme -> String
  transOpId sign op ts = fromMaybe (showIsaConstT op baseSign) $ do
    ops <- Map.lookup op (assumps sign)
    if isSingleton ops then Nothing else do
      i <- elemIndex ts $ map opType $ Set.toList ops
      Just $ showIsaConstIT op (i + 1) 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 _ _ _) ->
          termAppl conSome $ IsaSign.Free (transVar var)
      QualOp _ (PolyId opId _ _) ts _ _ _
        | opId == trueId -> true
        | opId == falseId -> false
        | otherwise -> termAppl conSome (conDouble (transOpId sign opId ts))
      QuantifiedTerm quan varDecls phi _ ->
          let quantify q gvd phi' = case gvd of
                  GenVarDecl (VarDecl var _ _ _) ->
                      termAppl (conDouble $ qname q)
                      $ Abs (IsaSign.Free $ transVar var) 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 = termAppl conSome $ if null pats then
                             Abs (IsaSign.Free $ mkVName "dummyVar")
                                      (f sign body) NotCont
                            else 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)) alts
          _ -> Case (transTerm sign t)
               [(conDouble "None", conDouble "None"),
                (App conSome (IsaSign.Free (mkVName "caseVar")) NotCont,
                 Case (IsaSign.Free (mkVName "caseVar")) alts)]
      _ -> error $ "HasCASL2IsabelleHOL.transTerm " ++ showDoc trm "\n"
                  ++ show trm
  
  transAppl :: Env -> Maybe As.Type -> As.Term -> As.Term -> IsaSign.Term
  transAppl s ty' t' t'' = case t'' of
      TupleTerm [] _ -> transTerm s t'
      _ -> case t' of
          QualVar (VarDecl _ ty _ _) -> transApplOp s ty t' t''
          QualOp _ (PolyId 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 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
    | all 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 = case peqs of
          [] -> error "No case alternatives."
          hd : _ -> getCons sign (getName hd)
        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)) =
            mapMaybe stripConstruct $ Set.toList altDefns
          extractIds _ = error "HasCASL2Isabelle.extractIds"
          stripConstruct (Construct i _ _ _) = i
          findInMap :: Ord k => k -> Map.Map k a -> a
          findInMap = Map.findWithDefault (error "HasCASL2isabelleHOL.findInMap")
  
  -- 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) -> case tyArgs of
                   t1 : t2 : r
                     | isArrow tyId && null r -> name t2
                     | isProductId tyId -> name t1
                   _ -> 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
    | all (null . 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
    | all (testPatBrand Appl) cmxs = redAppl cmxs sign
    | all (testPatBrand Tuple) cmxs = redAppl cmxs sign
    | otherwise = hd
    where testPatBrand pb cmx = pb == patBrand cmx
          hd : _ = cmxs
  
  {- 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
    | all (null . args) cmxs = hd
    | isSingle cmxs = hd
        { args = init hdArgs
        , newArgs = last hdArgs : newArgs hd }
    | all termIsVar lastArgs = substVar hd
    | otherwise = substTerm hd
     where hd : _ = cmxs
           hdArgs = args hd
           terms = map term cmxs
           lastArgs = map (last . args) cmxs
           varName = "caseVar" ++ show (length hdArgs)
           varId = mkId [mkSimpleId varName]
           newVar = QualVar (VarDecl varId (TypeName varId rStar 1)
                             As.Other nullRange)
           newPeqs = zipWith (curry newProgEq) lastArgs terms
           newPeqs' = recArgs sign newPeqs
           substVar cmx = case args cmx of
             [] -> cmx
             ac ->
                 cmx { args = if isSingle ac then [] else init ac,
                       newArgs = last ac : newArgs cmx }
           substTerm cmx = case args cmx of
             [] -> cmx
             ac ->
                 cmx { args = if isSingle ac then [] else init ac,
                       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 = case peqs of
            [] -> error "No case alternatives."
            hd : _ -> getCons sign (getName hd)
          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 as
                 Nothing -> error "HasCASL2IsabelleHOL.shrinkPat"
      Tuple -> TupleTerm as nullRange
      QuOp -> ha
      _ -> nha
    where mkApplT t1 t2 = ApplTerm t1 t2 nullRange
          ac = args cmx
          nac = newArgs cmx
          as = ac ++ nac
          ha : _ = ac
          nha : _ = nac
  
  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 _ -> all 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"
  