{-# 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 Int -> HasCASL2IsabelleHOL -> ShowS
[HasCASL2IsabelleHOL] -> ShowS
HasCASL2IsabelleHOL -> String
(Int -> HasCASL2IsabelleHOL -> ShowS)
-> (HasCASL2IsabelleHOL -> String)
-> ([HasCASL2IsabelleHOL] -> ShowS)
-> Show HasCASL2IsabelleHOL
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [HasCASL2IsabelleHOL] -> ShowS
$cshowList :: [HasCASL2IsabelleHOL] -> ShowS
show :: HasCASL2IsabelleHOL -> String
$cshow :: HasCASL2IsabelleHOL -> String
showsPrec :: Int -> HasCASL2IsabelleHOL -> ShowS
$cshowsPrec :: Int -> HasCASL2IsabelleHOL -> ShowS
Show

instance Language HasCASL2IsabelleHOL where
  language_name :: HasCASL2IsabelleHOL -> String
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
sourceLogic HasCASL2IsabelleHOL = HasCASL
HasCASL
    sourceSublogic :: HasCASL2IsabelleHOL -> Sublogic
sourceSublogic HasCASL2IsabelleHOL = Sublogic -> Sublogic -> Sublogic
sublogic_min Sublogic
noSubtypes Sublogic
noClasses
    targetLogic :: HasCASL2IsabelleHOL -> Isabelle
targetLogic HasCASL2IsabelleHOL = Isabelle
Isabelle
    mapSublogic :: HasCASL2IsabelleHOL -> Sublogic -> Maybe ()
mapSublogic cid :: HasCASL2IsabelleHOL
cid sl :: Sublogic
sl = if Sublogic
sl Sublogic -> Sublogic -> Bool
forall l. SemiLatticeWithTop l => l -> l -> Bool
`isSubElem` HasCASL2IsabelleHOL -> Sublogic
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid -> sublogics1
sourceSublogic HasCASL2IsabelleHOL
cid
                       then () -> Maybe ()
forall a. a -> Maybe a
Just () else Maybe ()
forall a. Maybe a
Nothing
    map_theory :: HasCASL2IsabelleHOL
-> (Env, [Named Sentence]) -> Result (Sign, [Named Sentence])
map_theory HasCASL2IsabelleHOL = (Env -> Result (Sign, [Named Sentence]))
-> (Env -> Sentence -> Result Sentence)
-> (Env, [Named Sentence])
-> Result (Sign, [Named Sentence])
forall (m :: * -> *) sign1 sign2 sentence2 sentence1.
Monad m =>
(sign1 -> m (sign2, [Named sentence2]))
-> (sign1 -> sentence1 -> m sentence2)
-> (sign1, [Named sentence1])
-> m (sign2, [Named sentence2])
mkTheoryMapping Env -> Result (Sign, [Named Sentence])
transSignature
                   (HasCASL2IsabelleHOL -> Env -> Sentence -> Result Sentence
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid -> sign1 -> sentence1 -> Result sentence2
map_sentence HasCASL2IsabelleHOL
HasCASL2IsabelleHOL)
    map_sentence :: HasCASL2IsabelleHOL -> Env -> Sentence -> Result Sentence
map_sentence HasCASL2IsabelleHOL sign :: Env
sign phi :: Sentence
phi =
       case Env -> Sentence -> Maybe Term
transSentence Env
sign Sentence
phi of
         Nothing -> Sentence -> String -> Range -> Result Sentence
forall a. a -> String -> Range -> Result a
warning (Term -> Sentence
mkSen Term
true)
                           "translation of sentence not implemented" Range
nullRange
         Just ts :: Term
ts -> Sentence -> Result Sentence
forall (m :: * -> *) a. Monad m => a -> m a
return (Sentence -> Result Sentence) -> Sentence -> Result Sentence
forall a b. (a -> b) -> a -> b
$ Term -> Sentence
mkSen Term
ts
    isInclusionComorphism :: HasCASL2IsabelleHOL -> Bool
isInclusionComorphism HasCASL2IsabelleHOL = Bool
True

-- * Signature
baseSign :: BaseSig
baseSign :: BaseSig
baseSign = BaseSig
MainHC_thy

transSignature :: Env -> Result (IsaSign.Sign, [Named IsaSign.Sentence])
transSignature :: Env -> Result (Sign, [Named Sentence])
transSignature sign :: Env
sign =
  (Sign, [Named Sentence]) -> Result (Sign, [Named Sentence])
forall (m :: * -> *) a. Monad m => a -> m a
return (Sign
IsaSign.emptySign {
    baseSig :: BaseSig
baseSig = BaseSig
baseSign,
    -- translation of typeconstructors
    tsig :: TypeSig
tsig = TypeSig
emptyTypeSig
             { arities :: Arities
arities = (Id -> TypeInfo -> Arities -> Arities)
-> Arities -> Map Id TypeInfo -> Arities
forall k a b. (k -> a -> b -> b) -> b -> Map k a -> b
Map.foldrWithKey Id -> TypeInfo -> Arities -> Arities
forall a.
Id
-> TypeInfo
-> Map String [(IsaClass, [a])]
-> Map String [(IsaClass, [a])]
extractTypeName
                                        Arities
forall k a. Map k a
Map.empty
                                        (Env -> Map Id TypeInfo
typeMap Env
sign) },
    -- translation of operation declarations
    constTab :: ConstTab
constTab = (Id -> Set OpInfo -> ConstTab -> ConstTab)
-> ConstTab -> Map Id (Set OpInfo) -> ConstTab
forall k a b. (k -> a -> b -> b) -> b -> Map k a -> b
Map.foldrWithKey Id -> Set OpInfo -> ConstTab -> ConstTab
insertOps
                               ConstTab
forall k a. Map k a
Map.empty
                               (Env -> Map Id (Set OpInfo)
assumps Env
sign),
    -- translation of datatype declarations
    domainTab :: DomainTab
domainTab = Map Id TypeInfo -> DomainTab
transDatatype (Env -> Map Id TypeInfo
typeMap Env
sign),
    showLemmas :: Bool
showLemmas = Bool
True },
    [] )
   where
    extractTypeName :: Id
-> TypeInfo
-> Map String [(IsaClass, [a])]
-> Map String [(IsaClass, [a])]
extractTypeName tyId :: Id
tyId typeInfo :: TypeInfo
typeInfo m :: Map String [(IsaClass, [a])]
m =
        if TypeInfo -> Bool
isDatatypeDefn TypeInfo
typeInfo then Map String [(IsaClass, [a])]
m
           else String
-> [(IsaClass, [a])]
-> Map String [(IsaClass, [a])]
-> Map String [(IsaClass, [a])]
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (Id -> BaseSig -> String
showIsaTypeT Id
tyId BaseSig
baseSign) [(IsaClass
isaTerm, [])] Map String [(IsaClass, [a])]
m
                -- translate the kind here!
    isDatatypeDefn :: TypeInfo -> Bool
isDatatypeDefn t :: TypeInfo
t = case TypeInfo -> TypeDefn
typeDefn TypeInfo
t of
                         DatatypeDefn _ -> Bool
True
                         _ -> Bool
False
    insertOps :: Id -> Set OpInfo -> ConstTab -> ConstTab
insertOps name :: Id
name ops :: Set OpInfo
ops m :: ConstTab
m =
          if Set OpInfo -> Bool
forall a. Set a -> Bool
isSingleton Set OpInfo
ops then
            let transOp :: Maybe Typ
transOp = OpInfo -> Maybe Typ
transOpInfo (Set OpInfo -> OpInfo
forall a. Set a -> a
Set.findMin Set OpInfo
ops)
            in case Maybe Typ
transOp of
                 Just op :: Typ
op ->
                     VName -> Typ -> ConstTab -> ConstTab
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (String -> VName
mkVName (String -> VName) -> String -> VName
forall a b. (a -> b) -> a -> b
$ Id -> BaseSig -> String
showIsaConstT Id
name BaseSig
baseSign) Typ
op ConstTab
m
                 Nothing -> ConstTab
m
          else
            let transOps :: [Maybe Typ]
transOps = (OpInfo -> Maybe Typ) -> [OpInfo] -> [Maybe Typ]
forall a b. (a -> b) -> [a] -> [b]
map OpInfo -> Maybe Typ
transOpInfo ([OpInfo] -> [Maybe Typ]) -> [OpInfo] -> [Maybe Typ]
forall a b. (a -> b) -> a -> b
$ Set OpInfo -> [OpInfo]
forall a. Set a -> [a]
Set.toList Set OpInfo
ops
            in (ConstTab -> (Maybe Typ, Int) -> ConstTab)
-> ConstTab -> [(Maybe Typ, Int)] -> ConstTab
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\ m' :: ConstTab
m' (transOp :: Maybe Typ
transOp, i :: Int
i) ->
                           case Maybe Typ
transOp of
                             Just ty :: Typ
ty -> VName -> Typ -> ConstTab -> ConstTab
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert
                                 (String -> VName
mkVName (String -> VName) -> String -> VName
forall a b. (a -> b) -> a -> b
$ Id -> Int -> BaseSig -> String
showIsaConstIT Id
name Int
i BaseSig
baseSign)
                                 Typ
ty ConstTab
m'
                             Nothing -> ConstTab
m')
                      ConstTab
m ([(Maybe Typ, Int)] -> ConstTab) -> [(Maybe Typ, Int)] -> ConstTab
forall a b. (a -> b) -> a -> b
$ [Maybe Typ] -> [(Maybe Typ, Int)]
forall a. [a] -> [(a, Int)]
number [Maybe Typ]
transOps

-- * translation of a type in an operation declaration

-- extract type from OpInfo omit datatype constructors
transOpInfo :: OpInfo -> Maybe Typ
transOpInfo :: OpInfo -> Maybe Typ
transOpInfo (OpInfo t :: TypeScheme
t _ opDef :: OpDefn
opDef) =
  case OpDefn
opDef of
    ConstructData _ -> Maybe Typ
forall a. Maybe a
Nothing
    _ -> Typ -> Maybe Typ
forall a. a -> Maybe a
Just (TypeScheme -> Typ
transOpType TypeScheme
t)

-- operation type
transOpType :: TypeScheme -> Typ
transOpType :: TypeScheme -> Typ
transOpType (TypeScheme _ op :: Type
op _) = Type -> Typ
transType Type
op

-- types
transType :: Type -> Typ
transType :: Type -> Typ
transType t :: Type
t = case Type -> (Type, [Type])
getTypeAppl Type
t of
   (TypeName tid :: Id
tid _ n :: Int
n, tyArgs :: [Type]
tyArgs) ->
      if Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== 0 then case [Type]
tyArgs of
          [] | Id
tid Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
== Id
unitTypeId -> Typ
boolType
          [t1 :: Type
t1] | Id
tid Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
== Id
lazyTypeId -> Type -> Typ
transType Type
t1
          t1 :: Type
t1 : t2 :: Type
t2 : r :: [Type]
r
            | Id -> Bool
isArrow Id
tid Bool -> Bool -> Bool
&& [Type] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Type]
r -> let tr :: Typ
tr = Type -> Typ
transType Type
t2 in
                Typ -> Typ -> Typ
mkFunType (Type -> Typ
transType Type
t1) (Typ -> Typ) -> Typ -> Typ
forall a b. (a -> b) -> a -> b
$
                    if Id -> Bool
isPartialArrow Id
tid Bool -> Bool -> Bool
&& Bool -> Bool
not (Type -> Bool
isPredType Type
t)
                        then Typ -> Typ
mkOptionType Typ
tr else Typ
tr
            | Id -> Bool
isProductId Id
tid -> (Typ -> Typ -> Typ) -> [Typ] -> Typ
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldl1 Typ -> Typ -> Typ
prodType ([Typ] -> Typ) -> [Typ] -> Typ
forall a b. (a -> b) -> a -> b
$ (Type -> Typ) -> [Type] -> [Typ]
forall a b. (a -> b) -> [a] -> [b]
map Type -> Typ
transType [Type]
tyArgs
          _ -> String -> Sort -> [Typ] -> Typ
Type (Id -> BaseSig -> String
showIsaTypeT Id
tid BaseSig
baseSign) [] ([Typ] -> Typ) -> [Typ] -> Typ
forall a b. (a -> b) -> a -> b
$ (Type -> Typ) -> [Type] -> [Typ]
forall a b. (a -> b) -> [a] -> [b]
map Type -> Typ
transType [Type]
tyArgs
       else String -> Sort -> Typ
TFree (Id -> BaseSig -> String
showIsaTypeT Id
tid BaseSig
baseSign) []
            -- type arguments are not allowed here!
   _ -> String -> Typ
forall a. HasCallStack => String -> a
error (String -> Typ) -> String -> Typ
forall a b. (a -> b) -> a -> b
$ "transType " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Type -> ShowS
forall a. Pretty a => a -> ShowS
showDoc Type
t "\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Type -> String
forall a. Show a => a -> String
show Type
t

-- * translation of a datatype declaration

transDatatype :: TypeMap -> DomainTab
transDatatype :: Map Id TypeInfo -> DomainTab
transDatatype tm :: Map Id TypeInfo
tm = (DataEntry -> [DomainEntry]) -> [DataEntry] -> DomainTab
forall a b. (a -> b) -> [a] -> [b]
map DataEntry -> [DomainEntry]
transDataEntry ((TypeInfo -> [DataEntry] -> [DataEntry])
-> [DataEntry] -> Map Id TypeInfo -> [DataEntry]
forall a b k. (a -> b -> b) -> b -> Map k a -> b
Map.foldr TypeInfo -> [DataEntry] -> [DataEntry]
extractDataypes [] Map Id TypeInfo
tm)
  where extractDataypes :: TypeInfo -> [DataEntry] -> [DataEntry]
extractDataypes ti :: TypeInfo
ti des :: [DataEntry]
des = case TypeInfo -> TypeDefn
typeDefn TypeInfo
ti of
                                   DatatypeDefn de :: DataEntry
de -> [DataEntry]
des [DataEntry] -> [DataEntry] -> [DataEntry]
forall a. [a] -> [a] -> [a]
++ [DataEntry
de]
                                   _ -> [DataEntry]
des

-- datatype with name (tyId) + args (tyArgs) and alternatives
transDataEntry :: DataEntry -> [DomainEntry]
transDataEntry :: DataEntry -> [DomainEntry]
transDataEntry (DataEntry _ tyId :: Id
tyId Le.Free tyArgs :: [TypeArg]
tyArgs _ alts :: Set AltDefn
alts) =
    [(Id -> [TypeArg] -> Typ
transDName Id
tyId [TypeArg]
tyArgs, (AltDefn -> (VName, [Typ])) -> [AltDefn] -> [(VName, [Typ])]
forall a b. (a -> b) -> [a] -> [b]
map AltDefn -> (VName, [Typ])
transAltDefn ([AltDefn] -> [(VName, [Typ])]) -> [AltDefn] -> [(VName, [Typ])]
forall a b. (a -> b) -> a -> b
$ Set AltDefn -> [AltDefn]
forall a. Set a -> [a]
Set.toList Set AltDefn
alts)]
  where transDName :: Id -> [TypeArg] -> Typ
transDName ti :: Id
ti ta :: [TypeArg]
ta = String -> Sort -> [Typ] -> Typ
Type (Id -> BaseSig -> String
showIsaTypeT Id
ti BaseSig
baseSign) []
                           ([Typ] -> Typ) -> [Typ] -> Typ
forall a b. (a -> b) -> a -> b
$ (TypeArg -> Typ) -> [TypeArg] -> [Typ]
forall a b. (a -> b) -> [a] -> [b]
map TypeArg -> Typ
transTypeArg [TypeArg]
ta
transDataEntry _ = String -> [DomainEntry]
forall a. HasCallStack => String -> a
error "HasCASL2IsabelleHOL.transDataEntry"

-- arguments of datatype's typeconstructor
transTypeArg :: TypeArg -> Typ
transTypeArg :: TypeArg -> Typ
transTypeArg ta :: TypeArg
ta = String -> Sort -> Typ
TFree (Id -> BaseSig -> String
showIsaTypeT (TypeArg -> Id
getTypeVar TypeArg
ta) BaseSig
baseSign) []

-- datatype alternatives/constructors
transAltDefn :: AltDefn -> (VName, [Typ])
transAltDefn :: AltDefn -> (VName, [Typ])
transAltDefn (Construct opId :: Maybe Id
opId ts :: [Type]
ts Total _) =
   let ts' :: [Typ]
ts' = (Type -> Typ) -> [Type] -> [Typ]
forall a b. (a -> b) -> [a] -> [b]
map Type -> Typ
transType [Type]
ts
   in case Maybe Id
opId of
        Just opId' :: Id
opId' -> (String -> VName
mkVName (String -> VName) -> String -> VName
forall a b. (a -> b) -> a -> b
$ Id -> BaseSig -> String
showIsaConstT Id
opId' BaseSig
baseSign, [Typ]
ts')
        Nothing -> (String -> VName
mkVName "", [Typ]
ts')
transAltDefn _ = String -> (VName, [Typ])
forall a. HasCallStack => String -> a
error "HasCASL2IsabelleHOL.transAltDefn"

-- * Formulas

-- simple variables
transVar :: Id -> VName
transVar :: Id -> VName
transVar v :: Id
v = String -> VName
mkVName (String -> VName) -> String -> VName
forall a b. (a -> b) -> a -> b
$ Id -> BaseSig -> String
showIsaConstT Id
v BaseSig
baseSign

transSentence :: Env -> Le.Sentence -> Maybe IsaSign.Term
transSentence :: Env -> Sentence -> Maybe Term
transSentence sign :: Env
sign s :: Sentence
s = case Sentence
s of
    Le.Formula t :: Term
t -> Term -> Maybe Term
forall a. a -> Maybe a
Just (Env -> Term -> Term
transTerm Env
sign Term
t)
    DatatypeSen _ -> Maybe Term
forall a. Maybe a
Nothing
    ProgEqSen _ _ _pe :: ProgEq
_pe -> Maybe Term
forall a. Maybe a
Nothing

-- disambiguate operation names
transOpId :: Env -> Id -> TypeScheme -> String
transOpId :: Env -> Id -> TypeScheme -> String
transOpId sign :: Env
sign op :: Id
op ts :: TypeScheme
ts = String -> Maybe String -> String
forall a. a -> Maybe a -> a
fromMaybe (Id -> BaseSig -> String
showIsaConstT Id
op BaseSig
baseSign) (Maybe String -> String) -> Maybe String -> String
forall a b. (a -> b) -> a -> b
$ do
  Set OpInfo
ops <- Id -> Map Id (Set OpInfo) -> Maybe (Set OpInfo)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Id
op (Env -> Map Id (Set OpInfo)
assumps Env
sign)
  if Set OpInfo -> Bool
forall a. Set a -> Bool
isSingleton Set OpInfo
ops then Maybe String
forall a. Maybe a
Nothing else do
    Int
i <- TypeScheme -> [TypeScheme] -> Maybe Int
forall a. Eq a => a -> [a] -> Maybe Int
elemIndex TypeScheme
ts ([TypeScheme] -> Maybe Int) -> [TypeScheme] -> Maybe Int
forall a b. (a -> b) -> a -> b
$ (OpInfo -> TypeScheme) -> [OpInfo] -> [TypeScheme]
forall a b. (a -> b) -> [a] -> [b]
map OpInfo -> TypeScheme
opType ([OpInfo] -> [TypeScheme]) -> [OpInfo] -> [TypeScheme]
forall a b. (a -> b) -> a -> b
$ Set OpInfo -> [OpInfo]
forall a. Set a -> [a]
Set.toList Set OpInfo
ops
    String -> Maybe String
forall a. a -> Maybe a
Just (String -> Maybe String) -> String -> Maybe String
forall a b. (a -> b) -> a -> b
$ Id -> Int -> BaseSig -> String
showIsaConstIT Id
op (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1) BaseSig
baseSign

transProgEq :: Env -> ProgEq -> (IsaSign.Term, IsaSign.Term)
transProgEq :: Env -> ProgEq -> (Term, Term)
transProgEq sign :: Env
sign (ProgEq pat :: Term
pat t :: Term
t _) =
      (Env -> Term -> Term
transPattern Env
sign Term
pat, Env -> Term -> Term
transPattern Env
sign Term
t)

-- terms
transTerm :: Env -> As.Term -> IsaSign.Term
transTerm :: Env -> Term -> Term
transTerm sign :: Env
sign trm :: Term
trm = case Term
trm of
    QualVar (VarDecl var :: Id
var _ _ _) ->
        Term -> Term -> Term
termAppl Term
conSome (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ VName -> Term
IsaSign.Free (Id -> VName
transVar Id
var)
    QualOp _ (PolyId opId :: Id
opId _ _) ts :: TypeScheme
ts _ _ _
      | Id
opId Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
== Id
trueId -> Term
true
      | Id
opId Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
== Id
falseId -> Term
false
      | Bool
otherwise -> Term -> Term -> Term
termAppl Term
conSome (String -> Term
conDouble (Env -> Id -> TypeScheme -> String
transOpId Env
sign Id
opId TypeScheme
ts))
    QuantifiedTerm quan :: Quantifier
quan varDecls :: [GenVarDecl]
varDecls phi :: Term
phi _ ->
        let quantify :: Quantifier -> GenVarDecl -> Term -> Term
quantify q :: Quantifier
q gvd :: GenVarDecl
gvd phi' :: Term
phi' = case GenVarDecl
gvd of
                GenVarDecl (VarDecl var :: Id
var _ _ _) ->
                    Term -> Term -> Term
termAppl (String -> Term
conDouble (String -> Term) -> String -> Term
forall a b. (a -> b) -> a -> b
$ Quantifier -> String
qname Quantifier
q)
                    (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Term -> Term -> Continuity -> Term
Abs (VName -> Term
IsaSign.Free (VName -> Term) -> VName -> Term
forall a b. (a -> b) -> a -> b
$ Id -> VName
transVar Id
var) Term
phi' Continuity
NotCont
                GenTypeVarDecl _ -> Term
phi'
            qname :: Quantifier -> String
qname Universal = String
allS
            qname Existential = String
exS
            qname Unique = String
ex1S
        in (GenVarDecl -> Term -> Term) -> Term -> [GenVarDecl] -> Term
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Quantifier -> GenVarDecl -> Term -> Term
quantify Quantifier
quan) (Env -> Term -> Term
transTerm Env
sign Term
phi) [GenVarDecl]
varDecls
    TypedTerm t :: Term
t _ _ _ -> Env -> Term -> Term
transTerm Env
sign Term
t
    LambdaTerm pats :: [Term]
pats p :: Partiality
p body :: Term
body _ ->
        let lambdaAbs :: (Env -> Term -> Term) -> Term
lambdaAbs f :: Env -> Term -> Term
f = Term -> Term -> Term
termAppl Term
conSome (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ if [Term] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Term]
pats then
                           Term -> Term -> Continuity -> Term
Abs (VName -> Term
IsaSign.Free (VName -> Term) -> VName -> Term
forall a b. (a -> b) -> a -> b
$ String -> VName
mkVName "dummyVar")
                                    (Env -> Term -> Term
f Env
sign Term
body) Continuity
NotCont
                          else (Term -> Term -> Term) -> Term -> [Term] -> Term
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Env -> Term -> Term -> Term
abstraction Env
sign)
                                 (Env -> Term -> Term
f Env
sign Term
body) [Term]
pats
        in case Partiality
p of
         {- distinguishes between partial and total lambda abstraction
         total lambda bodies are of type 'a' instead of type 'a option' -}
        Partial -> (Env -> Term -> Term) -> Term
lambdaAbs Env -> Term -> Term
transTerm
        Total -> (Env -> Term -> Term) -> Term
lambdaAbs Env -> Term -> Term
transTotalLambda
    LetTerm As.Let peqs :: [ProgEq]
peqs body :: Term
body _ ->
        [(Term, Term)] -> Term -> Term
IsaSign.Let ((ProgEq -> (Term, Term)) -> [ProgEq] -> [(Term, Term)]
forall a b. (a -> b) -> [a] -> [b]
map (Env -> ProgEq -> (Term, Term)
transProgEq Env
sign) [ProgEq]
peqs) (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Env -> Term -> Term
transTerm Env
sign Term
body
    TupleTerm ts :: [Term]
ts@(_ : _) _ ->
        (Term -> Term -> Term) -> [Term] -> Term
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldl1 (String -> Term -> Term -> Term
binConst String
pairC) ((Term -> Term) -> [Term] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map (Env -> Term -> Term
transTerm Env
sign) [Term]
ts)
    ApplTerm t1 :: Term
t1 t2 :: Term
t2 _ -> Env -> Maybe Type -> Term -> Term -> Term
transAppl Env
sign Maybe Type
forall a. Maybe a
Nothing Term
t1 Term
t2
    CaseTerm t :: Term
t peqs :: [ProgEq]
peqs _ ->
        -- flatten case alternatives
        let alts :: [(Term, Term)]
alts = Env -> [ProgEq] -> [(Term, Term)]
arangeCaseAlts Env
sign [ProgEq]
peqs
        in case Term
t of
        {- introduces new case statement if case variable is
        a term application that may evaluate to 'Some x' or 'None' -}
        QualVar (VarDecl decl :: Id
decl _ _ _) ->
            Term -> [(Term, Term)] -> Term
Case (VName -> Term
IsaSign.Free (Id -> VName
transVar Id
decl)) [(Term, Term)]
alts
        _ -> Term -> [(Term, Term)] -> Term
Case (Env -> Term -> Term
transTerm Env
sign Term
t)
             [(String -> Term
conDouble "None", String -> Term
conDouble "None"),
              (Term -> Term -> Continuity -> Term
App Term
conSome (VName -> Term
IsaSign.Free (String -> VName
mkVName "caseVar")) Continuity
NotCont,
               Term -> [(Term, Term)] -> Term
Case (VName -> Term
IsaSign.Free (String -> VName
mkVName "caseVar")) [(Term, Term)]
alts)]
    _ -> String -> Term
forall a. HasCallStack => String -> a
error (String -> Term) -> String -> Term
forall a b. (a -> b) -> a -> b
$ "HasCASL2IsabelleHOL.transTerm " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term -> ShowS
forall a. Pretty a => a -> ShowS
showDoc Term
trm "\n"
                String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term -> String
forall a. Show a => a -> String
show Term
trm

transAppl :: Env -> Maybe As.Type -> As.Term -> As.Term -> IsaSign.Term
transAppl :: Env -> Maybe Type -> Term -> Term -> Term
transAppl s :: Env
s ty' :: Maybe Type
ty' t' :: Term
t' t'' :: Term
t'' = case Term
t'' of
    TupleTerm [] _ -> Env -> Term -> Term
transTerm Env
s Term
t'
    _ -> case Term
t' of
        QualVar (VarDecl _ ty :: Type
ty _ _) -> Env -> Type -> Term -> Term -> Term
transApplOp Env
s Type
ty Term
t' Term
t''
        QualOp _ (PolyId opId :: Id
opId _ _) (TypeScheme _ ty :: Type
ty _) _ _ _ ->
            if Id -> [Id] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem Id
opId ([Id] -> Bool) -> [Id] -> Bool
forall a b. (a -> b) -> a -> b
$ ((Id, TypeScheme) -> Id) -> [(Id, TypeScheme)] -> [Id]
forall a b. (a -> b) -> [a] -> [b]
map (Id, TypeScheme) -> Id
forall a b. (a, b) -> a
fst [(Id, TypeScheme)]
bList then
               -- logical formulas are translated seperatly (transLog)
               if Id
opId Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
== Id
whenElse then Env -> Term -> Term
transWhenElse Env
s Term
t''
               else Env -> Id -> Term -> Term -> Term
transLog Env
s Id
opId Term
t' Term
t''
            else Env -> Type -> Term -> Term -> Term
transApplOp Env
s Type
ty Term
t' Term
t''
        -- distinguishes between partial and total term application
        TypedTerm tt' :: Term
tt' _ typ' :: Type
typ' _ -> Env -> Maybe Type -> Term -> Term -> Term
transAppl Env
s (Type -> Maybe Type
forall a. a -> Maybe a
Just Type
typ') Term
tt' Term
t''
        _ -> Term -> (Type -> Term) -> Maybe Type -> Term
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (String -> Env -> Term -> Term -> Term
mkApp "app" Env
s Term
t' Term
t'')
                  ( \ ty :: Type
ty -> Env -> Type -> Term -> Term -> Term
transApplOp Env
s Type
ty Term
t' Term
t'') Maybe Type
ty'

mkApp :: String -> Env -> As.Term -> As.Term -> IsaSign.Term
mkApp :: String -> Env -> Term -> Term -> Term
mkApp s :: String
s sg :: Env
sg tt :: Term
tt tt' :: Term
tt' = Term -> Term -> Term
termAppl (Term -> Term -> Term
termAppl (String -> Term
conDouble String
s) (Env -> Term -> Term
transTerm Env
sg Term
tt))
                         (Env -> Term -> Term
transTerm Env
sg Term
tt')

transApplOp :: Env -> As.Type -> As.Term -> As.Term -> IsaSign.Term
transApplOp :: Env -> Type -> Term -> Term -> Term
transApplOp s :: Env
s ty :: Type
ty tt :: Term
tt tt' :: Term
tt' = if Type -> Bool
isPredType Type
ty then String -> Env -> Term -> Term -> Term
mkApp "pApp" Env
s Term
tt Term
tt'
    else case Type -> (Type, [Type])
getTypeAppl Type
ty of
            (TypeName tid :: Id
tid _ 0, [_, _]) | Id -> Bool
isArrow Id
tid ->
                if Id -> Bool
isPartialArrow Id
tid then String -> Env -> Term -> Term -> Term
mkApp "app" Env
s Term
tt Term
tt'
                   else String -> Env -> Term -> Term -> Term
mkApp "apt" Env
s Term
tt Term
tt'
            _ -> String -> Env -> Term -> Term -> Term
mkApp "app" Env
s Term
tt Term
tt'

-- translation formulas with logical connectives
transLog :: Env -> Id -> As.Term -> As.Term -> IsaSign.Term
transLog :: Env -> Id -> Term -> Term -> Term
transLog sign :: Env
sign opId :: Id
opId opTerm :: Term
opTerm t :: Term
t = case Term
t of
 TupleTerm [l' :: Term
l' , r' :: Term
r'] _
  | Id
opId Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
== Id
andId -> Term -> Term -> Term
binConj Term
l Term
r
  | Id
opId Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
== Id
orId -> Term -> Term -> Term
binDisj Term
l Term
r
  | Id
opId Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
== Id
implId -> Term -> Term -> Term
binImpl Term
l Term
r
  | Id
opId Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
== Id
infixIf -> Term -> Term -> Term
binImpl Term
r Term
l
  | Id
opId Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
== Id
eqvId -> Term -> Term -> Term
binEq Term
l Term
r
  | Id
opId Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
== Id
exEq -> Term -> Term -> Term
binConj (Term -> Term -> Term
binEq Term
l Term
r) (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$
                      Term -> Term -> Term
binConj (Term -> Term -> Term
termAppl Term
defOp Term
l) (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$
                      Term -> Term -> Term
termAppl Term
defOp Term
r
  | Id
opId Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
== Id
eqId -> Term -> Term -> Term
binEq Term
l Term
r
  where l :: Term
l = Env -> Term -> Term
transTerm Env
sign Term
l'
        r :: Term
r = Env -> Term -> Term
transTerm Env
sign Term
r'
 _ | Id
opId Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
== Id
notId -> Term -> Term -> Term
termAppl Term
notOp (Env -> Term -> Term
transTerm Env
sign Term
t)
   | Id
opId Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
== Id
defId -> Term -> Term -> Term
termAppl Term
defOp (Env -> Term -> Term
transTerm Env
sign Term
t)
   | Bool
otherwise -> Term -> Term -> Term
termAppl (Env -> Term -> Term
transTerm Env
sign Term
opTerm) (Env -> Term -> Term
transTerm Env
sign Term
t)

-- | when else statement
transWhenElse :: Env -> As.Term -> IsaSign.Term
transWhenElse :: Env -> Term -> Term
transWhenElse sign :: Env
sign t :: Term
t =
    case Term
t of
      TupleTerm terms :: [Term]
terms _ ->
        let ts :: [Term]
ts = (Term -> Term) -> [Term] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map (Env -> Term -> Term
transTerm Env
sign) [Term]
terms
        in case [Term]
ts of
           [i :: Term
i, c :: Term
c, e :: Term
e] -> Term -> Term -> Term -> Continuity -> Term
If Term
c Term
i Term
e Continuity
NotCont
           _ -> String -> Term
forall a. HasCallStack => String -> a
error "HasCASL2IsabelleHOL.transWhenElse.tuple"
      _ -> String -> Term
forall a. HasCallStack => String -> a
error "HasCASL2IsabelleHOL.transWhenElse"

-- * translation of lambda abstractions

-- form Abs(pattern term)
abstraction :: Env -> As.Term -> IsaSign.Term -> IsaSign.Term
abstraction :: Env -> Term -> Term -> Term
abstraction sign :: Env
sign pat :: Term
pat body :: Term
body =
    Term -> Term -> Continuity -> Term
Abs (Env -> Term -> Term
transPattern Env
sign Term
pat) Term
body Continuity
NotCont

{- translation of lambda patterns
a pattern keeps his type 't', isn't translated to 't option' -}
transPattern :: Env -> As.Term -> IsaSign.Term
transPattern :: Env -> Term -> Term
transPattern _ (QualVar (VarDecl var :: Id
var _ _ _)) =
  VName -> Term
IsaSign.Free (Id -> VName
transVar Id
var)
transPattern sign :: Env
sign (TupleTerm terms :: [Term]
terms@(_ : _) _) =
    (Term -> Term -> Term) -> [Term] -> Term
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldl1 (String -> Term -> Term -> Term
binConst String
isaPair) ([Term] -> Term) -> [Term] -> Term
forall a b. (a -> b) -> a -> b
$ (Term -> Term) -> [Term] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map (Env -> Term -> Term
transPattern Env
sign) [Term]
terms
transPattern _ (QualOp _ (PolyId opId :: Id
opId _ _) _ _ _ _) =
    String -> Term
conDouble (String -> Term) -> String -> Term
forall a b. (a -> b) -> a -> b
$ Id -> BaseSig -> String
showIsaConstT Id
opId BaseSig
baseSign
transPattern sign :: Env
sign (TypedTerm t :: Term
t _ _ _) = Env -> Term -> Term
transPattern Env
sign Term
t
transPattern sign :: Env
sign (ApplTerm t1 :: Term
t1 t2 :: Term
t2 _) =
    Term -> Term -> Continuity -> Term
App (Env -> Term -> Term
transPattern Env
sign Term
t1) (Env -> Term -> Term
transPattern Env
sign Term
t2) Continuity
NotCont
transPattern sign :: Env
sign t :: Term
t = Env -> Term -> Term
transTerm Env
sign Term
t

-- translation of total lambda abstraction bodies
transTotalLambda :: Env -> As.Term -> IsaSign.Term
transTotalLambda :: Env -> Term -> Term
transTotalLambda _ (QualVar (VarDecl var :: Id
var _ _ _)) =
  VName -> Term
IsaSign.Free (Id -> VName
transVar Id
var)
transTotalLambda sign :: Env
sign t :: Term
t@(QualOp _ (PolyId opId :: Id
opId _ _) _ _ _ _) =
  if Id
opId Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
== Id
trueId Bool -> Bool -> Bool
|| Id
opId Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
== Id
falseId then Env -> Term -> Term
transTerm Env
sign Term
t
    else String -> Term
conDouble (String -> Term) -> String -> Term
forall a b. (a -> b) -> a -> b
$ Id -> BaseSig -> String
showIsaConstT Id
opId BaseSig
baseSign
transTotalLambda sign :: Env
sign (ApplTerm term1 :: Term
term1 term2 :: Term
term2 _) =
  Term -> Term -> Term
termAppl (Env -> Term -> Term
transTotalLambda Env
sign Term
term1) (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Env -> Term -> Term
transTotalLambda Env
sign Term
term2
transTotalLambda sign :: Env
sign (TypedTerm t :: Term
t _ _ _) = Env -> Term -> Term
transTotalLambda Env
sign Term
t
transTotalLambda sign :: Env
sign (LambdaTerm pats :: [Term]
pats part :: Partiality
part body :: Term
body _) =
  case Partiality
part of
    Partial -> (Env -> Term -> Term) -> Term
lambdaAbs Env -> Term -> Term
transTerm
    Total -> (Env -> Term -> Term) -> Term
lambdaAbs Env -> Term -> Term
transTotalLambda
  where
    lambdaAbs :: (Env -> Term -> Term) -> Term
lambdaAbs f :: Env -> Term -> Term
f =
      if [Term] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Term]
pats then Term -> Term -> Continuity -> Term
Abs (VName -> Term
IsaSign.Free (String -> VName
mkVName "dummyVar"))
                               (Env -> Term -> Term
f Env
sign Term
body) Continuity
NotCont
-- if (null pats) then Abs [("dummyVar", noType)]
        else (Term -> Term -> Term) -> Term -> [Term] -> Term
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Env -> Term -> Term -> Term
abstraction Env
sign) (Env -> Term -> Term
f Env
sign Term
body) [Term]
pats
transTotalLambda sign :: Env
sign (TupleTerm terms :: [Term]
terms@(_ : _) _) =
  (Term -> Term -> Term) -> [Term] -> Term
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldl1 (String -> Term -> Term -> Term
binConst String
isaPair) ([Term] -> Term) -> [Term] -> Term
forall a b. (a -> b) -> a -> b
$ (Term -> Term) -> [Term] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map (Env -> Term -> Term
transTotalLambda Env
sign) [Term]
terms
transTotalLambda sign :: Env
sign (CaseTerm t :: Term
t pEqs :: [ProgEq]
pEqs _) =
  Term -> [(Term, Term)] -> Term
Case (Env -> Term -> Term
transTotalLambda Env
sign Term
t) ([(Term, Term)] -> Term) -> [(Term, Term)] -> Term
forall a b. (a -> b) -> a -> b
$ (ProgEq -> (Term, Term)) -> [ProgEq] -> [(Term, Term)]
forall a b. (a -> b) -> [a] -> [b]
map ProgEq -> (Term, Term)
transCaseAltTotal [ProgEq]
pEqs
  where transCaseAltTotal :: ProgEq -> (Term, Term)
transCaseAltTotal (ProgEq pat :: Term
pat trm :: Term
trm _) =
                (Env -> Term -> Term
transPat Env
sign Term
pat, Env -> Term -> Term
transTotalLambda Env
sign Term
trm)
transTotalLambda sign :: Env
sign t :: Term
t = Env -> Term -> Term
transTerm Env
sign Term
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 :: Env -> [ProgEq] -> [(Term, Term)]
arangeCaseAlts sign :: Env
sign peqs :: [ProgEq]
peqs
  | (ProgEq -> Bool) -> [ProgEq] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all ProgEq -> Bool
patIsVar [ProgEq]
peqs = (ProgEq -> (Term, Term)) -> [ProgEq] -> [(Term, Term)]
forall a b. (a -> b) -> [a] -> [b]
map (Env -> ProgEq -> (Term, Term)
transCaseAlt Env
sign) [ProgEq]
peqs
  | Bool
otherwise = Env -> [ProgEq] -> [(Term, Term)]
sortCaseAlts Env
sign [ProgEq]
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 :: Env -> [ProgEq] -> [(Term, Term)]
sortCaseAlts sign :: Env
sign peqs :: [ProgEq]
peqs =
  let consList :: [Id]
consList = case [ProgEq]
peqs of
        [] -> String -> [Id]
forall a. HasCallStack => String -> a
error "No case alternatives."
        hd :: ProgEq
hd : _ -> Env -> Id -> [Id]
getCons Env
sign (ProgEq -> Id
getName ProgEq
hd)
      groupedByCons :: [[ProgEq]]
groupedByCons = [[ProgEq]] -> [[ProgEq]]
forall a. Ord a => [a] -> [a]
nubOrd ((Id -> [ProgEq]) -> [Id] -> [[ProgEq]]
forall a b. (a -> b) -> [a] -> [b]
map ([ProgEq] -> Id -> [ProgEq]
groupCons [ProgEq]
peqs) [Id]
consList)
  in ([ProgEq] -> (Term, Term)) -> [[ProgEq]] -> [(Term, Term)]
forall a b. (a -> b) -> [a] -> [b]
map (Env -> [ProgEq] -> (Term, Term)
flattenPattern Env
sign) [[ProgEq]]
groupedByCons

-- Returns a list of the constructors of the used datatype
getCons :: Env -> Id -> [Id]
getCons :: Env -> Id -> [Id]
getCons sign :: Env
sign tyId :: Id
tyId =
  TypeDefn -> [Id]
extractIds (TypeInfo -> TypeDefn
typeDefn (Id -> Map Id TypeInfo -> TypeInfo
forall k a. Ord k => k -> Map k a -> a
findInMap Id
tyId (Env -> Map Id TypeInfo
typeMap Env
sign)))
  where extractIds :: TypeDefn -> [Id]
extractIds (DatatypeDefn (DataEntry _ _ _ _ _ altDefns :: Set AltDefn
altDefns)) =
          (AltDefn -> Maybe Id) -> [AltDefn] -> [Id]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe AltDefn -> Maybe Id
stripConstruct ([AltDefn] -> [Id]) -> [AltDefn] -> [Id]
forall a b. (a -> b) -> a -> b
$ Set AltDefn -> [AltDefn]
forall a. Set a -> [a]
Set.toList Set AltDefn
altDefns
        extractIds _ = String -> [Id]
forall a. HasCallStack => String -> a
error "HasCASL2Isabelle.extractIds"
        stripConstruct :: AltDefn -> Maybe Id
stripConstruct (Construct i :: Maybe Id
i _ _ _) = Maybe Id
i
        findInMap :: Ord k => k -> Map.Map k a -> a
        findInMap :: k -> Map k a -> a
findInMap = a -> k -> Map k a -> a
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault (String -> a
forall a. HasCallStack => String -> a
error "HasCASL2isabelleHOL.findInMap")

-- Extracts the type of the used datatype in case patterns
getName :: ProgEq -> Id
getName :: ProgEq -> Id
getName (ProgEq pat :: Term
pat _ _) = Term -> Id
getTypeName Term
pat

getTypeName :: As.Term -> Id
getTypeName :: Term -> Id
getTypeName p :: Term
p =
   case Term
p of
     QualVar (VarDecl _ ty :: Type
ty _ _) -> Type -> Id
name Type
ty
     QualOp _ _ (TypeScheme _ ty :: Type
ty _) _ _ _ -> Type -> Id
name Type
ty
     TypedTerm _ _ ty :: Type
ty _ -> Type -> Id
name Type
ty
     ApplTerm t :: Term
t _ _ -> Term -> Id
getTypeName Term
t
     TupleTerm (t :: Term
t : _) _ -> Term -> Id
getTypeName Term
t
     _ -> String -> Id
forall a. HasCallStack => String -> a
error "HasCASL2IsabelleHOL.getTypeName"
   where name :: Type -> Id
name tp :: Type
tp = case Type -> (Type, [Type])
getTypeAppl Type
tp of
             (TypeName tyId :: Id
tyId _ 0, tyArgs :: [Type]
tyArgs) -> case [Type]
tyArgs of
                 t1 :: Type
t1 : t2 :: Type
t2 : r :: [Type]
r
                   | Id -> Bool
isArrow Id
tyId Bool -> Bool -> Bool
&& [Type] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Type]
r -> Type -> Id
name Type
t2
                   | Id -> Bool
isProductId Id
tyId -> Type -> Id
name Type
t1
                 _ -> Id
tyId
             _ -> String -> Id
forall a. HasCallStack => String -> a
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 :: [ProgEq] -> Id -> [ProgEq]
groupCons peqs :: [ProgEq]
peqs name :: Id
name = (ProgEq -> Bool) -> [ProgEq] -> [ProgEq]
forall a. (a -> Bool) -> [a] -> [a]
filter ProgEq -> Bool
hasSameName [ProgEq]
peqs
  where hasSameName :: ProgEq -> Bool
hasSameName (ProgEq pat :: Term
pat _ _) =
           Term -> Bool
hsn Term
pat
        hsn :: Term -> Bool
hsn pat :: Term
pat =
          case Term
pat of
            QualOp _ (PolyId n :: Id
n _ _) _ _ _ _ -> Id
n Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
== Id
name
            ApplTerm t1 :: Term
t1 _ _ -> Term -> Bool
hsn Term
t1
            TypedTerm t :: Term
t _ _ _ -> Term -> Bool
hsn Term
t
            TupleTerm _ _ -> Bool
True
            _ -> Bool
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 :: Env -> [ProgEq] -> (Term, Term)
flattenPattern sign :: Env
sign peqs :: [ProgEq]
peqs = case [ProgEq]
peqs of
  [] -> String -> (Term, Term)
forall a. HasCallStack => String -> a
error "Missing constructor alternative in case pattern."
  [h :: ProgEq
h] -> Env -> ProgEq -> (Term, Term)
transCaseAlt Env
sign ProgEq
h
  {- at this stage there are patterns left which use 'ApplTerm' or 'TupleTerm'
  or the 'TypedTerm' variant of one of them -}
  _ -> let m :: CaseMatrix
m = [CaseMatrix] -> Env -> CaseMatrix
concentrate ([ProgEq] -> [CaseMatrix]
matricize [ProgEq]
peqs) Env
sign in
              Env -> ProgEq -> (Term, Term)
transCaseAlt Env
sign (Term -> Term -> Range -> ProgEq
ProgEq (CaseMatrix -> Term
shrinkPat CaseMatrix
m) (CaseMatrix -> Term
term CaseMatrix
m) Range
nullRange)

data CaseMatrix = CaseMatrix
    { CaseMatrix -> PatBrand
patBrand :: PatBrand
    , CaseMatrix -> Maybe Term
cons :: Maybe As.Term
    , CaseMatrix -> [Term]
args :: [As.Term]
    , CaseMatrix -> [Term]
newArgs :: [As.Term]
    , CaseMatrix -> Term
term :: As.Term
    } deriving (Int -> CaseMatrix -> ShowS
[CaseMatrix] -> ShowS
CaseMatrix -> String
(Int -> CaseMatrix -> ShowS)
-> (CaseMatrix -> String)
-> ([CaseMatrix] -> ShowS)
-> Show CaseMatrix
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [CaseMatrix] -> ShowS
$cshowList :: [CaseMatrix] -> ShowS
show :: CaseMatrix -> String
$cshow :: CaseMatrix -> String
showsPrec :: Int -> CaseMatrix -> ShowS
$cshowsPrec :: Int -> CaseMatrix -> ShowS
Show, CaseMatrix -> CaseMatrix -> Bool
(CaseMatrix -> CaseMatrix -> Bool)
-> (CaseMatrix -> CaseMatrix -> Bool) -> Eq CaseMatrix
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: CaseMatrix -> CaseMatrix -> Bool
$c/= :: CaseMatrix -> CaseMatrix -> Bool
== :: CaseMatrix -> CaseMatrix -> Bool
$c== :: CaseMatrix -> CaseMatrix -> Bool
Eq, Eq CaseMatrix
Eq CaseMatrix =>
(CaseMatrix -> CaseMatrix -> Ordering)
-> (CaseMatrix -> CaseMatrix -> Bool)
-> (CaseMatrix -> CaseMatrix -> Bool)
-> (CaseMatrix -> CaseMatrix -> Bool)
-> (CaseMatrix -> CaseMatrix -> Bool)
-> (CaseMatrix -> CaseMatrix -> CaseMatrix)
-> (CaseMatrix -> CaseMatrix -> CaseMatrix)
-> Ord CaseMatrix
CaseMatrix -> CaseMatrix -> Bool
CaseMatrix -> CaseMatrix -> Ordering
CaseMatrix -> CaseMatrix -> CaseMatrix
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: CaseMatrix -> CaseMatrix -> CaseMatrix
$cmin :: CaseMatrix -> CaseMatrix -> CaseMatrix
max :: CaseMatrix -> CaseMatrix -> CaseMatrix
$cmax :: CaseMatrix -> CaseMatrix -> CaseMatrix
>= :: CaseMatrix -> CaseMatrix -> Bool
$c>= :: CaseMatrix -> CaseMatrix -> Bool
> :: CaseMatrix -> CaseMatrix -> Bool
$c> :: CaseMatrix -> CaseMatrix -> Bool
<= :: CaseMatrix -> CaseMatrix -> Bool
$c<= :: CaseMatrix -> CaseMatrix -> Bool
< :: CaseMatrix -> CaseMatrix -> Bool
$c< :: CaseMatrix -> CaseMatrix -> Bool
compare :: CaseMatrix -> CaseMatrix -> Ordering
$ccompare :: CaseMatrix -> CaseMatrix -> Ordering
$cp1Ord :: Eq CaseMatrix
Ord)

data PatBrand = Appl | Tuple | QuOp | QuVar deriving (Int -> PatBrand -> ShowS
[PatBrand] -> ShowS
PatBrand -> String
(Int -> PatBrand -> ShowS)
-> (PatBrand -> String) -> ([PatBrand] -> ShowS) -> Show PatBrand
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [PatBrand] -> ShowS
$cshowList :: [PatBrand] -> ShowS
show :: PatBrand -> String
$cshow :: PatBrand -> String
showsPrec :: Int -> PatBrand -> ShowS
$cshowsPrec :: Int -> PatBrand -> ShowS
Show, PatBrand -> PatBrand -> Bool
(PatBrand -> PatBrand -> Bool)
-> (PatBrand -> PatBrand -> Bool) -> Eq PatBrand
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: PatBrand -> PatBrand -> Bool
$c/= :: PatBrand -> PatBrand -> Bool
== :: PatBrand -> PatBrand -> Bool
$c== :: PatBrand -> PatBrand -> Bool
Eq, Eq PatBrand
Eq PatBrand =>
(PatBrand -> PatBrand -> Ordering)
-> (PatBrand -> PatBrand -> Bool)
-> (PatBrand -> PatBrand -> Bool)
-> (PatBrand -> PatBrand -> Bool)
-> (PatBrand -> PatBrand -> Bool)
-> (PatBrand -> PatBrand -> PatBrand)
-> (PatBrand -> PatBrand -> PatBrand)
-> Ord PatBrand
PatBrand -> PatBrand -> Bool
PatBrand -> PatBrand -> Ordering
PatBrand -> PatBrand -> PatBrand
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: PatBrand -> PatBrand -> PatBrand
$cmin :: PatBrand -> PatBrand -> PatBrand
max :: PatBrand -> PatBrand -> PatBrand
$cmax :: PatBrand -> PatBrand -> PatBrand
>= :: PatBrand -> PatBrand -> Bool
$c>= :: PatBrand -> PatBrand -> Bool
> :: PatBrand -> PatBrand -> Bool
$c> :: PatBrand -> PatBrand -> Bool
<= :: PatBrand -> PatBrand -> Bool
$c<= :: PatBrand -> PatBrand -> Bool
< :: PatBrand -> PatBrand -> Bool
$c< :: PatBrand -> PatBrand -> Bool
compare :: PatBrand -> PatBrand -> Ordering
$ccompare :: PatBrand -> PatBrand -> Ordering
$cp1Ord :: Eq PatBrand
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 :: [ProgEq] -> [CaseMatrix]
matricize = (ProgEq -> CaseMatrix) -> [ProgEq] -> [CaseMatrix]
forall a b. (a -> b) -> [a] -> [b]
map ProgEq -> CaseMatrix
matriPEq

matriPEq :: ProgEq -> CaseMatrix
matriPEq :: ProgEq -> CaseMatrix
matriPEq (ProgEq pat :: Term
pat altTerm :: Term
altTerm _) = Term -> Term -> CaseMatrix
matriArg Term
pat Term
altTerm

matriArg :: As.Term -> As.Term -> CaseMatrix
matriArg :: Term -> Term -> CaseMatrix
matriArg pat :: Term
pat cTerm :: Term
cTerm =
  case Term
pat of
    ApplTerm t1 :: Term
t1 t2 :: Term
t2 _ -> let (c :: Maybe Term
c, p :: [Term]
p) = Term -> (Maybe Any, [Term]) -> (Maybe Term, [Term])
forall a. Term -> (a, [Term]) -> (Maybe Term, [Term])
stripAppl Term
t1 (Maybe Any
forall a. Maybe a
Nothing, []) in CaseMatrix :: PatBrand -> Maybe Term -> [Term] -> [Term] -> Term -> CaseMatrix
CaseMatrix
        { patBrand :: PatBrand
patBrand = PatBrand
Appl,
          cons :: Maybe Term
cons = Maybe Term
c,
          args :: [Term]
args = [Term]
p [Term] -> [Term] -> [Term]
forall a. [a] -> [a] -> [a]
++ [Term
t2],
          newArgs :: [Term]
newArgs = [],
          term :: Term
term = Term
cTerm }
    TupleTerm ts :: [Term]
ts _ -> CaseMatrix :: PatBrand -> Maybe Term -> [Term] -> [Term] -> Term -> CaseMatrix
CaseMatrix
        { patBrand :: PatBrand
patBrand = PatBrand
Tuple,
          cons :: Maybe Term
cons = Maybe Term
forall a. Maybe a
Nothing,
          args :: [Term]
args = [Term]
ts,
          newArgs :: [Term]
newArgs = [],
          term :: Term
term = Term
cTerm }
    TypedTerm t :: Term
t _ _ _ -> Term -> Term -> CaseMatrix
matriArg Term
t Term
cTerm
    qv :: Term
qv@(QualVar _) -> CaseMatrix :: PatBrand -> Maybe Term -> [Term] -> [Term] -> Term -> CaseMatrix
CaseMatrix
        { patBrand :: PatBrand
patBrand = PatBrand
QuVar,
          cons :: Maybe Term
cons = Maybe Term
forall a. Maybe a
Nothing,
          args :: [Term]
args = [Term
qv],
          newArgs :: [Term]
newArgs = [],
          term :: Term
term = Term
cTerm }
    qo :: Term
qo@(QualOp {}) -> CaseMatrix :: PatBrand -> Maybe Term -> [Term] -> [Term] -> Term -> CaseMatrix
CaseMatrix
        { patBrand :: PatBrand
patBrand = PatBrand
QuOp,
          cons :: Maybe Term
cons = Maybe Term
forall a. Maybe a
Nothing,
          args :: [Term]
args = [Term
qo],
          newArgs :: [Term]
newArgs = [],
          term :: Term
term = Term
cTerm }
    _ -> String -> CaseMatrix
forall a. HasCallStack => String -> a
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 :: Term -> (a, [Term]) -> (Maybe Term, [Term])
stripAppl ct :: Term
ct tp :: (a, [Term])
tp = case Term
ct of
            TypedTerm (ApplTerm q :: Term
q@(QualOp {}) t' :: Term
t' _) _ _ _ ->
                (Term -> Maybe Term
forall a. a -> Maybe a
Just Term
q, Term
t' Term -> [Term] -> [Term]
forall a. a -> [a] -> [a]
: (a, [Term]) -> [Term]
forall a b. (a, b) -> b
snd (a, [Term])
tp)
            TypedTerm (ApplTerm (TypedTerm
              q :: Term
q@(QualOp {}) _ _ _) t' :: Term
t' _) _ _ _ ->
                (Term -> Maybe Term
forall a. a -> Maybe a
Just Term
q, Term
t' Term -> [Term] -> [Term]
forall a. a -> [a] -> [a]
: (a, [Term]) -> [Term]
forall a b. (a, b) -> b
snd (a, [Term])
tp)
            TypedTerm (ApplTerm t' :: Term
t' t'' :: Term
t'' _) _ _ _ ->
              Term -> (a, [Term]) -> (Maybe Term, [Term])
stripAppl Term
t' ((a, [Term]) -> a
forall a b. (a, b) -> a
fst (a, [Term])
tp, Term
t'' Term -> [Term] -> [Term]
forall a. a -> [a] -> [a]
: (a, [Term]) -> [Term]
forall a b. (a, b) -> b
snd (a, [Term])
tp)
            ApplTerm q :: Term
q@(QualOp {}) t' :: Term
t' _ -> (Term -> Maybe Term
forall a. a -> Maybe a
Just Term
q, Term
t' Term -> [Term] -> [Term]
forall a. a -> [a] -> [a]
: (a, [Term]) -> [Term]
forall a b. (a, b) -> b
snd (a, [Term])
tp)
            ApplTerm (TypedTerm
              q :: Term
q@(QualOp {}) _ _ _) t' :: Term
t' _ -> (Term -> Maybe Term
forall a. a -> Maybe a
Just Term
q, [Term
t'])
            ApplTerm t' :: Term
t' t'' :: Term
t'' _ -> Term -> (a, [Term]) -> (Maybe Term, [Term])
stripAppl Term
t' ((a, [Term]) -> a
forall a b. (a, b) -> a
fst (a, [Term])
tp, Term
t'' Term -> [Term] -> [Term]
forall a. a -> [a] -> [a]
: (a, [Term]) -> [Term]
forall a b. (a, b) -> b
snd (a, [Term])
tp)
            q :: Term
q@(QualOp {}) -> (Term -> Maybe Term
forall a. a -> Maybe a
Just Term
q, (a, [Term]) -> [Term]
forall a b. (a, b) -> b
snd (a, [Term])
tp)
            _ -> (Maybe Term
forall a. Maybe a
Nothing, Term
ct Term -> [Term] -> [Term]
forall a. a -> [a] -> [a]
: (a, [Term]) -> [Term]
forall a b. (a, b) -> b
snd (a, [Term])
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 :: [CaseMatrix] -> Env -> CaseMatrix
concentrate cmxs :: [CaseMatrix]
cmxs sign :: Env
sign = case ([CaseMatrix] -> CaseMatrix) -> [[CaseMatrix]] -> [CaseMatrix]
forall a b. (a -> b) -> [a] -> [b]
map (Env -> [CaseMatrix] -> CaseMatrix
redArgs Env
sign) ([[CaseMatrix]] -> [CaseMatrix]) -> [[CaseMatrix]] -> [CaseMatrix]
forall a b. (a -> b) -> a -> b
$ [[CaseMatrix]] -> [[CaseMatrix]]
forall a. Ord a => [a] -> [a]
nubOrd
    ([[CaseMatrix]] -> [[CaseMatrix]])
-> [[CaseMatrix]] -> [[CaseMatrix]]
forall a b. (a -> b) -> a -> b
$ (Int -> [CaseMatrix]) -> [Int] -> [[CaseMatrix]]
forall a b. (a -> b) -> [a] -> [b]
map ([CaseMatrix] -> Int -> [CaseMatrix]
groupByArgs [CaseMatrix]
cmxs) [0 .. ([CaseMatrix] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [CaseMatrix]
cmxs Int -> Int -> Int
forall a. Num a => a -> a -> a
- 1)] of
  [h :: CaseMatrix
h] -> CaseMatrix
h
  l :: [CaseMatrix]
l -> [CaseMatrix] -> Env -> CaseMatrix
concentrate [CaseMatrix]
l Env
sign

groupByArgs :: [CaseMatrix] -> Int -> [CaseMatrix]
groupByArgs :: [CaseMatrix] -> Int -> [CaseMatrix]
groupByArgs cmxs :: [CaseMatrix]
cmxs i :: Int
i
  | (CaseMatrix -> Bool) -> [CaseMatrix] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all ([Term] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([Term] -> Bool) -> (CaseMatrix -> [Term]) -> CaseMatrix -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CaseMatrix -> [Term]
args) [CaseMatrix]
cmxs = [CaseMatrix]
cmxs
  | Bool
otherwise = (CaseMatrix -> Bool) -> [CaseMatrix] -> [CaseMatrix]
forall a. (a -> Bool) -> [a] -> [a]
filter CaseMatrix -> Bool
equalPat [CaseMatrix]
cmxs
  where patE :: [Term]
patE = [Term] -> [Term]
forall a. [a] -> [a]
init (CaseMatrix -> [Term]
args ([CaseMatrix]
cmxs [CaseMatrix] -> Int -> CaseMatrix
forall a. [a] -> Int -> a
!! Int
i))
        equalPat :: CaseMatrix -> Bool
equalPat cmx :: CaseMatrix
cmx = [Term] -> Bool
forall a. [a] -> Bool
isSingle (CaseMatrix -> [Term]
args CaseMatrix
cmx) Bool -> Bool -> Bool
|| [Term] -> [Term]
forall a. [a] -> [a]
init (CaseMatrix -> [Term]
args CaseMatrix
cmx) [Term] -> [Term] -> Bool
forall a. Eq a => a -> a -> Bool
== [Term]
patE

redArgs :: Env -> [CaseMatrix] -> CaseMatrix
redArgs :: Env -> [CaseMatrix] -> CaseMatrix
redArgs sign :: Env
sign cmxs :: [CaseMatrix]
cmxs
  | (CaseMatrix -> Bool) -> [CaseMatrix] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (PatBrand -> CaseMatrix -> Bool
testPatBrand PatBrand
Appl) [CaseMatrix]
cmxs = [CaseMatrix] -> Env -> CaseMatrix
redAppl [CaseMatrix]
cmxs Env
sign
  | (CaseMatrix -> Bool) -> [CaseMatrix] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (PatBrand -> CaseMatrix -> Bool
testPatBrand PatBrand
Tuple) [CaseMatrix]
cmxs = [CaseMatrix] -> Env -> CaseMatrix
redAppl [CaseMatrix]
cmxs Env
sign
  | Bool
otherwise = CaseMatrix
hd
  where testPatBrand :: PatBrand -> CaseMatrix -> Bool
testPatBrand pb :: PatBrand
pb cmx :: CaseMatrix
cmx = PatBrand
pb PatBrand -> PatBrand -> Bool
forall a. Eq a => a -> a -> Bool
== CaseMatrix -> PatBrand
patBrand CaseMatrix
cmx
        hd :: CaseMatrix
hd : _ = [CaseMatrix]
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 :: [CaseMatrix] -> Env -> CaseMatrix
redAppl cmxs :: [CaseMatrix]
cmxs sign :: Env
sign
  | (CaseMatrix -> Bool) -> [CaseMatrix] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all ([Term] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([Term] -> Bool) -> (CaseMatrix -> [Term]) -> CaseMatrix -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CaseMatrix -> [Term]
args) [CaseMatrix]
cmxs = CaseMatrix
hd
  | [CaseMatrix] -> Bool
forall a. [a] -> Bool
isSingle [CaseMatrix]
cmxs = CaseMatrix
hd
      { args :: [Term]
args = [Term] -> [Term]
forall a. [a] -> [a]
init [Term]
hdArgs
      , newArgs :: [Term]
newArgs = [Term] -> Term
forall a. [a] -> a
last [Term]
hdArgs Term -> [Term] -> [Term]
forall a. a -> [a] -> [a]
: CaseMatrix -> [Term]
newArgs CaseMatrix
hd }
  | (Term -> Bool) -> [Term] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Term -> Bool
termIsVar [Term]
lastArgs = CaseMatrix -> CaseMatrix
substVar CaseMatrix
hd
  | Bool
otherwise = CaseMatrix -> CaseMatrix
substTerm CaseMatrix
hd
   where hd :: CaseMatrix
hd : _ = [CaseMatrix]
cmxs
         hdArgs :: [Term]
hdArgs = CaseMatrix -> [Term]
args CaseMatrix
hd
         terms :: [Term]
terms = (CaseMatrix -> Term) -> [CaseMatrix] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map CaseMatrix -> Term
term [CaseMatrix]
cmxs
         lastArgs :: [Term]
lastArgs = (CaseMatrix -> Term) -> [CaseMatrix] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map ([Term] -> Term
forall a. [a] -> a
last ([Term] -> Term) -> (CaseMatrix -> [Term]) -> CaseMatrix -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CaseMatrix -> [Term]
args) [CaseMatrix]
cmxs
         varName :: String
varName = "caseVar" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show ([Term] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Term]
hdArgs)
         varId :: Id
varId = [Token] -> Id
mkId [String -> Token
mkSimpleId String
varName]
         newVar :: Term
newVar = VarDecl -> Term
QualVar (Id -> Type -> SeparatorKind -> Range -> VarDecl
VarDecl Id
varId (Id -> RawKind -> Int -> Type
TypeName Id
varId RawKind
rStar 1)
                           SeparatorKind
As.Other Range
nullRange)
         newPeqs :: [ProgEq]
newPeqs = (Term -> Term -> ProgEq) -> [Term] -> [Term] -> [ProgEq]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (((Term, Term) -> ProgEq) -> Term -> Term -> ProgEq
forall a b c. ((a, b) -> c) -> a -> b -> c
curry (Term, Term) -> ProgEq
newProgEq) [Term]
lastArgs [Term]
terms
         newPeqs' :: [ProgEq]
newPeqs' = Env -> [ProgEq] -> [ProgEq]
recArgs Env
sign [ProgEq]
newPeqs
         substVar :: CaseMatrix -> CaseMatrix
substVar cmx :: CaseMatrix
cmx = case CaseMatrix -> [Term]
args CaseMatrix
cmx of
           [] -> CaseMatrix
cmx
           ac :: [Term]
ac ->
               CaseMatrix
cmx { args :: [Term]
args = if [Term] -> Bool
forall a. [a] -> Bool
isSingle [Term]
ac then [] else [Term] -> [Term]
forall a. [a] -> [a]
init [Term]
ac,
                     newArgs :: [Term]
newArgs = [Term] -> Term
forall a. [a] -> a
last [Term]
ac Term -> [Term] -> [Term]
forall a. a -> [a] -> [a]
: CaseMatrix -> [Term]
newArgs CaseMatrix
cmx }
         substTerm :: CaseMatrix -> CaseMatrix
substTerm cmx :: CaseMatrix
cmx = case CaseMatrix -> [Term]
args CaseMatrix
cmx of
           [] -> CaseMatrix
cmx
           ac :: [Term]
ac ->
               CaseMatrix
cmx { args :: [Term]
args = if [Term] -> Bool
forall a. [a] -> Bool
isSingle [Term]
ac then [] else [Term] -> [Term]
forall a. [a] -> [a]
init [Term]
ac,
                     newArgs :: [Term]
newArgs = Term
newVar Term -> [Term] -> [Term]
forall a. a -> [a] -> [a]
: CaseMatrix -> [Term]
newArgs CaseMatrix
cmx,
                     term :: Term
term = Term -> [ProgEq] -> Range -> Term
CaseTerm Term
newVar [ProgEq]
newPeqs' Range
nullRange }
         newProgEq :: (Term, Term) -> ProgEq
newProgEq (p :: Term
p, t :: Term
t) = Term -> Term -> Range -> ProgEq
ProgEq Term
p Term
t Range
nullRange

{- Input: ProgEqs that were build to replace an argument
with a case statement
Functionality: -}
recArgs :: Env -> [ProgEq] -> [ProgEq]
recArgs :: Env -> [ProgEq] -> [ProgEq]
recArgs sign :: Env
sign peqs :: [ProgEq]
peqs
  | [[ProgEq]] -> Bool
forall a. [a] -> Bool
isSingle [[ProgEq]]
groupedByCons
      Bool -> Bool -> Bool
|| [[ProgEq]] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [[ProgEq]]
groupedByCons = []
  | Bool
otherwise = [[ProgEq]] -> [ProgEq] -> [ProgEq]
doPEQ [[ProgEq]]
groupedByCons []
  where consList :: [Id]
consList = case [ProgEq]
peqs of
          [] -> String -> [Id]
forall a. HasCallStack => String -> a
error "No case alternatives."
          hd :: ProgEq
hd : _ -> Env -> Id -> [Id]
getCons Env
sign (ProgEq -> Id
getName ProgEq
hd)
        groupedByCons :: [[ProgEq]]
groupedByCons = (Id -> [ProgEq]) -> [Id] -> [[ProgEq]]
forall a b. (a -> b) -> [a] -> [b]
map ([ProgEq] -> Id -> [ProgEq]
groupCons [ProgEq]
peqs) [Id]
consList
        doPEQ :: [[ProgEq]] -> [ProgEq] -> [ProgEq]
doPEQ [] res :: [ProgEq]
res = [ProgEq]
res
        doPEQ (g :: [ProgEq]
g : gByCs :: [[ProgEq]]
gByCs) res :: [ProgEq]
res
          | [ProgEq] -> Bool
forall a. [a] -> Bool
isSingle [ProgEq]
g = [[ProgEq]] -> [ProgEq] -> [ProgEq]
doPEQ [[ProgEq]]
gByCs ([ProgEq]
res [ProgEq] -> [ProgEq] -> [ProgEq]
forall a. [a] -> [a] -> [a]
++ [ProgEq]
g)
          | Bool
otherwise = [[ProgEq]] -> [ProgEq] -> [ProgEq]
doPEQ [[ProgEq]]
gByCs ([ProgEq]
res [ProgEq] -> [ProgEq] -> [ProgEq]
forall a. [a] -> [a] -> [a]
++ [CaseMatrix -> ProgEq
toPEQ (Env -> [ProgEq] -> CaseMatrix
testPEQs Env
sign [ProgEq]
g)])
        toPEQ :: CaseMatrix -> ProgEq
toPEQ cmx :: CaseMatrix
cmx = Term -> Term -> Range -> ProgEq
ProgEq (CaseMatrix -> Term
shrinkPat CaseMatrix
cmx) (CaseMatrix -> Term
term CaseMatrix
cmx) Range
nullRange
        testPEQs :: Env -> [ProgEq] -> CaseMatrix
testPEQs sig :: Env
sig ps :: [ProgEq]
ps
          | [ProgEq] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [ProgEq]
peqs = String -> CaseMatrix
forall a. HasCallStack => String -> a
error "HasCASL2IsabelleHOL.testPEQs"
          | Bool
otherwise = [CaseMatrix] -> Env -> CaseMatrix
concentrate ([ProgEq] -> [CaseMatrix]
matricize [ProgEq]
ps) Env
sig

-- accumulates arguments of caseMatrix to one pattern
shrinkPat :: CaseMatrix -> As.Term
shrinkPat :: CaseMatrix -> Term
shrinkPat cmx :: CaseMatrix
cmx =
  case CaseMatrix -> PatBrand
patBrand CaseMatrix
cmx of
    Appl -> case CaseMatrix -> Maybe Term
cons CaseMatrix
cmx of
               Just c :: Term
c -> (Term -> Term -> Term) -> Term -> [Term] -> Term
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Term -> Term -> Term
mkApplT Term
c [Term]
as
               Nothing -> String -> Term
forall a. HasCallStack => String -> a
error "HasCASL2IsabelleHOL.shrinkPat"
    Tuple -> [Term] -> Range -> Term
TupleTerm [Term]
as Range
nullRange
    QuOp -> Term
ha
    _ -> Term
nha
  where mkApplT :: Term -> Term -> Term
mkApplT t1 :: Term
t1 t2 :: Term
t2 = Term -> Term -> Range -> Term
ApplTerm Term
t1 Term
t2 Range
nullRange
        ac :: [Term]
ac = CaseMatrix -> [Term]
args CaseMatrix
cmx
        nac :: [Term]
nac = CaseMatrix -> [Term]
newArgs CaseMatrix
cmx
        as :: [Term]
as = [Term]
ac [Term] -> [Term] -> [Term]
forall a. [a] -> [a] -> [a]
++ [Term]
nac
        ha :: Term
ha : _ = [Term]
ac
        nha :: Term
nha : _ = [Term]
nac

patIsVar :: ProgEq -> Bool
patIsVar :: ProgEq -> Bool
patIsVar (ProgEq pat :: Term
pat _ _) = Term -> Bool
termIsVar Term
pat

termIsVar :: As.Term -> Bool
termIsVar :: Term -> Bool
termIsVar t :: Term
t = case Term
t of
    QualVar _ -> Bool
True
    TypedTerm tr :: Term
tr _ _ _ -> Term -> Bool
termIsVar Term
tr
    TupleTerm ts :: [Term]
ts _ -> (Term -> Bool) -> [Term] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Term -> Bool
termIsVar [Term]
ts
    _ -> Bool
False

patHasNoArg :: ProgEq -> Bool
patHasNoArg :: ProgEq -> Bool
patHasNoArg (ProgEq pat :: Term
pat _ _) = Term -> Bool
termHasNoArg Term
pat

termHasNoArg :: As.Term -> Bool
termHasNoArg :: Term -> Bool
termHasNoArg t :: Term
t = case Term
t of
    QualOp {} -> Bool
True
    TypedTerm tr :: Term
tr _ _ _ -> Term -> Bool
termHasNoArg Term
tr
    _ -> Bool
False

transCaseAlt :: Env -> ProgEq -> (IsaSign.Term, IsaSign.Term)
transCaseAlt :: Env -> ProgEq -> (Term, Term)
transCaseAlt sign :: Env
sign (ProgEq pat :: Term
pat trm :: Term
trm _) =
  (Env -> Term -> Term
transPat Env
sign Term
pat, Env -> Term -> Term
transTerm Env
sign Term
trm)

transPat :: Env -> As.Term -> IsaSign.Term
transPat :: Env -> Term -> Term
transPat _ (QualVar (VarDecl var :: Id
var _ _ _)) =
    VName -> Term
IsaSign.Free (Id -> VName
transVar Id
var)
transPat sign :: Env
sign (ApplTerm term1 :: Term
term1 term2 :: Term
term2 _) =
    Term -> Term -> Term
termAppl (Env -> Term -> Term
transPat Env
sign Term
term1) (Env -> Term -> Term
transPat Env
sign Term
term2)
transPat sign :: Env
sign (TypedTerm trm :: Term
trm _ _ _) = Env -> Term -> Term
transPat Env
sign Term
trm
transPat sign :: Env
sign (TupleTerm terms :: [Term]
terms@(_ : _) _) =
    (Term -> Term -> Term) -> [Term] -> Term
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldl1 (String -> Term -> Term -> Term
binConst String
isaPair) ((Term -> Term) -> [Term] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map (Env -> Term -> Term
transPat Env
sign) [Term]
terms)
transPat _ (QualOp _ (PolyId i :: Id
i _ _) _ _ _ _) =
    String -> Term
conDouble (Id -> BaseSig -> String
showIsaConstT Id
i BaseSig
baseSign)
transPat _ _ = String -> Term
forall a. HasCallStack => String -> a
error "HasCASL2IsabelleHOL.transPat"

-- | apply binary operation to arguments
binConst :: String -> IsaSign.Term -> IsaSign.Term -> IsaSign.Term
binConst :: String -> Term -> Term -> Term
binConst s :: String
s = VName -> Term -> Term -> Term
binVNameAppl (VName -> Term -> Term -> Term) -> VName -> Term -> Term -> Term
forall a b. (a -> b) -> a -> b
$ String -> VName
mkVName String
s

-- | upper case curried pair constructor
isaPair :: String
isaPair :: String
isaPair = "Pair"