{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}
{- |
Module      :  ./Comorphisms/CASL2HasCASL.hs
Description :  embedding CASL into HasCASL
Copyright   :  (c) Till Mossakowski, Christian Maeder and Uni Bremen 2003-2005
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Christian.Maeder@dfki.de
Stability   :  provisional
Portability :  non-portable (imports Logic.Logic)

The embedding comorphism from CASL to HasCASL.
-}

module Comorphisms.CASL2HasCASL where

import Logic.Logic
import Logic.Comorphism

import Common.AS_Annotation
import Common.Id
import Common.ProofTree
import Common.DocUtils

import qualified Data.Map as Map
import qualified Data.Set as Set

-- CASL
import CASL.Logic_CASL
import CASL.Sublogic as CasSub
import CASL.ToDoc
import CASL.Fold
import qualified CASL.AS_Basic_CASL as Cas
import qualified CASL.Sign as CasS
import qualified CASL.Morphism as CasM

import HasCASL.Logic_HasCASL
import HasCASL.As
import HasCASL.AsUtils
import HasCASL.Le
import HasCASL.Builtin
import HasCASL.Sublogic as HasSub
import HasCASL.FoldTerm as HasFold

-- | The identity of the comorphism
data CASL2HasCASL = CASL2HasCASL deriving (Int -> CASL2HasCASL -> ShowS
[CASL2HasCASL] -> ShowS
CASL2HasCASL -> String
(Int -> CASL2HasCASL -> ShowS)
-> (CASL2HasCASL -> String)
-> ([CASL2HasCASL] -> ShowS)
-> Show CASL2HasCASL
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [CASL2HasCASL] -> ShowS
$cshowList :: [CASL2HasCASL] -> ShowS
show :: CASL2HasCASL -> String
$cshow :: CASL2HasCASL -> String
showsPrec :: Int -> CASL2HasCASL -> ShowS
$cshowsPrec :: Int -> CASL2HasCASL -> ShowS
Show)

instance Language CASL2HasCASL -- default definition is okay

instance Comorphism CASL2HasCASL
               CASL CASL_Sublogics
               CASLBasicSpec Cas.CASLFORMULA Cas.SYMB_ITEMS
               Cas.SYMB_MAP_ITEMS
               CasS.CASLSign
               CasM.CASLMor
               CasS.Symbol CasM.RawSymbol ProofTree
               HasCASL Sublogic
               BasicSpec Sentence SymbItems SymbMapItems
               Env Morphism Symbol RawSymbol () where
    sourceLogic :: CASL2HasCASL -> CASL
sourceLogic CASL2HasCASL = CASL
CASL
    sourceSublogic :: CASL2HasCASL -> CASL_Sublogics
sourceSublogic CASL2HasCASL = CASL_Sublogics
forall a. Lattice a => CASL_SL a
CasSub.top
    targetLogic :: CASL2HasCASL -> HasCASL
targetLogic CASL2HasCASL = HasCASL
HasCASL
    mapSublogic :: CASL2HasCASL -> CASL_Sublogics -> Maybe Sublogic
mapSublogic CASL2HasCASL sl :: CASL_Sublogics
sl = Sublogic -> Maybe Sublogic
forall a. a -> Maybe a
Just (Sublogic -> Maybe Sublogic) -> Sublogic -> Maybe Sublogic
forall a b. (a -> b) -> a -> b
$ Sublogic -> Sublogic
sublogicUp (Sublogic -> Sublogic) -> Sublogic -> Sublogic
forall a b. (a -> b) -> a -> b
$
        (if CASL_Sublogics -> Bool
forall a. CASL_SL a -> Bool
has_cons CASL_Sublogics
sl then Sublogic -> Sublogic -> Sublogic
sublogic_max Sublogic
need_hol else Sublogic -> Sublogic
forall a. a -> a
id)
        Sublogic
caslLogic
        { has_sub :: Bool
HasSub.has_sub = CASL_Sublogics -> Bool
forall a. CASL_SL a -> Bool
CasSub.has_sub CASL_Sublogics
sl
        , has_part :: Bool
HasSub.has_part = CASL_Sublogics -> Bool
forall a. CASL_SL a -> Bool
CasSub.has_part CASL_Sublogics
sl
        , has_eq :: Bool
HasSub.has_eq = CASL_Sublogics -> Bool
forall a. CASL_SL a -> Bool
CasSub.has_eq CASL_Sublogics
sl
        , has_pred :: Bool
HasSub.has_pred = CASL_Sublogics -> Bool
forall a. CASL_SL a -> Bool
CasSub.has_pred CASL_Sublogics
sl
        , which_logic :: Formulas
HasSub.which_logic = case CASL_Sublogics -> CASL_Formulas
forall a. CASL_SL a -> CASL_Formulas
CasSub.which_logic CASL_Sublogics
sl of
             CasSub.Atomic -> Formulas
HasSub.Atomic
             CasSub.Horn -> Formulas
HasSub.Horn
             CasSub.GHorn -> Formulas
HasSub.GHorn
             CasSub.Prenex -> Formulas
HasSub.FOL -- at least for now
             CasSub.FOL -> Formulas
HasSub.FOL
             CasSub.SOL -> Formulas
HasSub.HOL
        }
    map_morphism :: CASL2HasCASL -> CASLMor -> Result Morphism
map_morphism CASL2HasCASL = Morphism -> Result Morphism
forall (m :: * -> *) a. Monad m => a -> m a
return (Morphism -> Result Morphism)
-> (CASLMor -> Morphism) -> CASLMor -> Result Morphism
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CASLMor -> Morphism
forall f e m. Morphism f e m -> Morphism
mapMor
    map_sentence :: CASL2HasCASL -> CASLSign -> CASLFORMULA -> Result Sentence
map_sentence CASL2HasCASL _ = Sentence -> Result Sentence
forall (m :: * -> *) a. Monad m => a -> m a
return (Sentence -> Result Sentence)
-> (CASLFORMULA -> Sentence) -> CASLFORMULA -> Result Sentence
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CASLFORMULA -> Sentence
forall f.
(TermExtension f, FormExtension f) =>
FORMULA f -> Sentence
toSentence
    map_symbol :: CASL2HasCASL -> CASLSign -> Symbol -> Set Symbol
map_symbol CASL2HasCASL _ = Symbol -> Set Symbol
forall a. a -> Set a
Set.singleton (Symbol -> Set Symbol)
-> (Symbol -> Symbol) -> Symbol -> Set Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> Symbol
mapSym
    map_theory :: CASL2HasCASL
-> (CASLSign, [Named CASLFORMULA])
-> Result (Env, [Named Sentence])
map_theory CASL2HasCASL = (Env, [Named Sentence]) -> Result (Env, [Named Sentence])
forall (m :: * -> *) a. Monad m => a -> m a
return ((Env, [Named Sentence]) -> Result (Env, [Named Sentence]))
-> ((CASLSign, [Named CASLFORMULA]) -> (Env, [Named Sentence]))
-> (CASLSign, [Named CASLFORMULA])
-> Result (Env, [Named Sentence])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (CASLSign, [Named CASLFORMULA]) -> (Env, [Named Sentence])
forall f e.
(TermExtension f, FormExtension f) =>
(Sign f e, [Named (FORMULA f)]) -> (Env, [Named Sentence])
mapTheory
    has_model_expansion :: CASL2HasCASL -> Bool
has_model_expansion CASL2HasCASL = Bool
True
    is_weakly_amalgamable :: CASL2HasCASL -> Bool
is_weakly_amalgamable CASL2HasCASL = Bool
True
    isInclusionComorphism :: CASL2HasCASL -> Bool
isInclusionComorphism CASL2HasCASL = Bool
True

fromOPTYPE :: Cas.OP_TYPE -> Type
fromOPTYPE :: OP_TYPE -> Type
fromOPTYPE (Cas.Op_type ok :: OpKind
ok args :: [SORT]
args res :: SORT
res ps :: Range
ps) = let
  (total :: Bool
total, arr :: Arrow
arr) = case OpKind
ok of
    Cas.Total -> (Bool
True, Arrow
FunArr)
    Cas.Partial -> (Bool
False, Arrow
PFunArr)
  resTy :: Type
resTy = SORT -> Type
toType SORT
res
  in if [SORT] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [SORT]
args then if Bool
total then Type
resTy else Type -> Type
mkLazyType Type
resTy
  else Type -> Arrow -> Type -> Type
mkFunArrType ([Type] -> Range -> Type
mkProductTypeWithRange ((SORT -> Type) -> [SORT] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map SORT -> Type
toType [SORT]
args) Range
ps) Arrow
arr Type
resTy

fromOpType :: CasS.OpType -> Type
fromOpType :: OpType -> Type
fromOpType = OP_TYPE -> Type
fromOPTYPE (OP_TYPE -> Type) -> (OpType -> OP_TYPE) -> OpType -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. OpType -> OP_TYPE
CasS.toOP_TYPE

fromPREDTYPE :: Cas.PRED_TYPE -> Type
fromPREDTYPE :: PRED_TYPE -> Type
fromPREDTYPE (Cas.Pred_type args :: [SORT]
args ps :: Range
ps) =
   if [SORT] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [SORT]
args then Type -> Type
mkLazyType (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$ Range -> Type
unitTypeWithRange Range
ps
   else Range -> Type -> Type
predType Range
ps (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$ [Type] -> Range -> Type
mkProductTypeWithRange ((SORT -> Type) -> [SORT] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map SORT -> Type
toType [SORT]
args) Range
ps

fromPredType :: CasS.PredType -> Type
fromPredType :: PredType -> Type
fromPredType = PRED_TYPE -> Type
fromPREDTYPE (PRED_TYPE -> Type) -> (PredType -> PRED_TYPE) -> PredType -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PredType -> PRED_TYPE
CasS.toPRED_TYPE

mapTheory :: (CasS.TermExtension f, FormExtension f) =>
  (CasS.Sign f e, [Named (Cas.FORMULA f)]) -> (Env, [Named Sentence])
mapTheory :: (Sign f e, [Named (FORMULA f)]) -> (Env, [Named Sentence])
mapTheory (sig :: Sign f e
sig, sents :: [Named (FORMULA f)]
sents) =
  (Set (SORT, OpType) -> Sign f e -> Env
forall f e. Set (SORT, OpType) -> Sign f e -> Env
mapSig ([Named (FORMULA f)] -> Set (SORT, OpType)
forall f. [Named (FORMULA f)] -> Set (SORT, OpType)
CasS.getConstructors [Named (FORMULA f)]
sents) Sign f e
sig, (Named (FORMULA f) -> Named Sentence)
-> [Named (FORMULA f)] -> [Named Sentence]
forall a b. (a -> b) -> [a] -> [b]
map ((FORMULA f -> Sentence) -> Named (FORMULA f) -> Named Sentence
forall s t a. (s -> t) -> SenAttr s a -> SenAttr t a
mapNamed FORMULA f -> Sentence
forall f.
(TermExtension f, FormExtension f) =>
FORMULA f -> Sentence
toSentence) [Named (FORMULA f)]
sents)

mapSig :: Set.Set (Id, CasS.OpType) -> CasS.Sign f e -> Env
mapSig :: Set (SORT, OpType) -> Sign f e -> Env
mapSig = (SORT -> SORT)
-> (OpType -> Type)
-> (PredType -> Type)
-> Set (SORT, OpType)
-> Sign f e
-> Env
forall f e.
(SORT -> SORT)
-> (OpType -> Type)
-> (PredType -> Type)
-> Set (SORT, OpType)
-> Sign f e
-> Env
mapSigAux SORT -> SORT
trId OpType -> Type
fromOpType PredType -> Type
fromPredType

-- | sort names or not translated
mapSigAux :: (Id -> Id) -> (CasS.OpType -> Type) -> (CasS.PredType -> Type)
  -> Set.Set (Id, CasS.OpType) -> CasS.Sign f e -> Env
mapSigAux :: (SORT -> SORT)
-> (OpType -> Type)
-> (PredType -> Type)
-> Set (SORT, OpType)
-> Sign f e
-> Env
mapSigAux trI :: SORT -> SORT
trI trO :: OpType -> Type
trO trP :: PredType -> Type
trP constr :: Set (SORT, OpType)
constr sign :: Sign f e
sign =
    let f1 :: [(SORT, Type, OpDefn)]
f1 = ((SORT, OpType) -> (SORT, Type, OpDefn))
-> [(SORT, OpType)] -> [(SORT, Type, OpDefn)]
forall a b. (a -> b) -> [a] -> [b]
map ( \ (i :: SORT
i, ty :: OpType
ty) ->
                   (SORT -> SORT
trI SORT
i, OpType -> Type
trO OpType
ty,
                            if (SORT, OpType) -> Set (SORT, OpType) -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member (SORT
i, OpType -> OpType
CasS.mkPartial OpType
ty)
                               Set (SORT, OpType)
constr then SORT -> OpDefn
ConstructData (SORT -> OpDefn) -> SORT -> OpDefn
forall a b. (a -> b) -> a -> b
$ OpType -> SORT
CasS.opRes OpType
ty
                               else OpBrand -> OpDefn
NoOpDefn OpBrand
Op))
             ([(SORT, OpType)] -> [(SORT, Type, OpDefn)])
-> [(SORT, OpType)] -> [(SORT, Type, OpDefn)]
forall a b. (a -> b) -> a -> b
$ MapSet SORT OpType -> [(SORT, OpType)]
forall a b. MapSet a b -> [(a, b)]
CasS.mapSetToList (MapSet SORT OpType -> [(SORT, OpType)])
-> MapSet SORT OpType -> [(SORT, OpType)]
forall a b. (a -> b) -> a -> b
$ Sign f e -> MapSet SORT OpType
forall f e. Sign f e -> MapSet SORT OpType
CasS.opMap Sign f e
sign
        f2 :: [(SORT, Type, OpDefn)]
f2 = ((SORT, PredType) -> (SORT, Type, OpDefn))
-> [(SORT, PredType)] -> [(SORT, Type, OpDefn)]
forall a b. (a -> b) -> [a] -> [b]
map ( \ (i :: SORT
i, ty :: PredType
ty) -> let pTy :: Type
pTy = PredType -> Type
trP PredType
ty in
                   (SORT -> SORT
trI SORT
i, Type
pTy, OpBrand -> OpDefn
NoOpDefn
                   (OpBrand -> OpDefn) -> OpBrand -> OpDefn
forall a b. (a -> b) -> a -> b
$ if Type -> Bool
isPredType Type
pTy then OpBrand
Pred else OpBrand
Fun))
             ([(SORT, PredType)] -> [(SORT, Type, OpDefn)])
-> [(SORT, PredType)] -> [(SORT, Type, OpDefn)]
forall a b. (a -> b) -> a -> b
$ MapSet SORT PredType -> [(SORT, PredType)]
forall a b. MapSet a b -> [(a, b)]
CasS.mapSetToList (MapSet SORT PredType -> [(SORT, PredType)])
-> MapSet SORT PredType -> [(SORT, PredType)]
forall a b. (a -> b) -> a -> b
$ Sign f e -> MapSet SORT PredType
forall f e. Sign f e -> MapSet SORT PredType
CasS.predMap Sign f e
sign
        insF :: (k, Type, OpDefn) -> Map k (Set OpInfo) -> Map k (Set OpInfo)
insF (i :: k
i, ty :: Type
ty, defn :: OpDefn
defn) m :: Map k (Set OpInfo)
m =
            let os :: Set OpInfo
os = Set OpInfo -> k -> Map k (Set OpInfo) -> Set OpInfo
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault Set OpInfo
forall a. Set a
Set.empty k
i Map k (Set OpInfo)
m
            in k -> Set OpInfo -> Map k (Set OpInfo) -> Map k (Set OpInfo)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert k
i (OpInfo -> Set OpInfo -> Set OpInfo
forall a. Ord a => a -> Set a -> Set a
Set.insert
                             (TypeScheme -> Set OpAttr -> OpDefn -> OpInfo
OpInfo (Type -> TypeScheme
simpleTypeScheme Type
ty) Set OpAttr
forall a. Set a
Set.empty OpDefn
defn) Set OpInfo
os) Map k (Set OpInfo)
m
     in Env
initialEnv
     { classMap :: ClassMap
classMap = ClassMap
forall k a. Map k a
Map.empty,
       typeMap :: TypeMap
typeMap = [(SORT, TypeInfo)] -> TypeMap
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(SORT, TypeInfo)] -> TypeMap) -> [(SORT, TypeInfo)] -> TypeMap
forall a b. (a -> b) -> a -> b
$ (SORT -> (SORT, TypeInfo)) -> [SORT] -> [(SORT, TypeInfo)]
forall a b. (a -> b) -> [a] -> [b]
map
                 ( \ s :: SORT
s -> (SORT
s, TypeInfo
starTypeInfo
                           { superTypes :: Set SORT
superTypes = SORT -> Set SORT -> Set SORT
forall a. Ord a => a -> Set a -> Set a
Set.delete SORT
s (Set SORT -> Set SORT) -> Set SORT -> Set SORT
forall a b. (a -> b) -> a -> b
$
                                          SORT -> Sign f e -> Set SORT
forall f e. SORT -> Sign f e -> Set SORT
CasS.supersortsOf SORT
s Sign f e
sign
                           })) ([SORT] -> [(SORT, TypeInfo)]) -> [SORT] -> [(SORT, TypeInfo)]
forall a b. (a -> b) -> a -> b
$ Set SORT -> [SORT]
forall a. Set a -> [a]
Set.toList (Set SORT -> [SORT]) -> Set SORT -> [SORT]
forall a b. (a -> b) -> a -> b
$ Sign f e -> Set SORT
forall f e. Sign f e -> Set SORT
CasS.sortSet Sign f e
sign,
       assumps :: Assumps
assumps = ((SORT, Type, OpDefn) -> Assumps -> Assumps)
-> Assumps -> [(SORT, Type, OpDefn)] -> Assumps
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (SORT, Type, OpDefn) -> Assumps -> Assumps
forall k.
Ord k =>
(k, Type, OpDefn) -> Map k (Set OpInfo) -> Map k (Set OpInfo)
insF Assumps
forall k a. Map k a
Map.empty ([(SORT, Type, OpDefn)]
f1 [(SORT, Type, OpDefn)]
-> [(SORT, Type, OpDefn)] -> [(SORT, Type, OpDefn)]
forall a. [a] -> [a] -> [a]
++ [(SORT, Type, OpDefn)]
f2)}

mapMor :: CasM.Morphism f e m -> Morphism
mapMor :: Morphism f e m -> Morphism
mapMor m :: Morphism f e m
m = let tm :: Sort_map
tm = Morphism f e m -> Sort_map
forall f e m. Morphism f e m -> Sort_map
CasM.sort_map Morphism f e m
m
               f1 :: [((SORT, TypeScheme), (SORT, TypeScheme))]
f1 = (((SORT, OpType), (SORT, OpKind))
 -> ((SORT, TypeScheme), (SORT, TypeScheme)))
-> [((SORT, OpType), (SORT, OpKind))]
-> [((SORT, TypeScheme), (SORT, TypeScheme))]
forall a b. (a -> b) -> [a] -> [b]
map ( \ ((i :: SORT
i, ot :: OpType
ot), (j :: SORT
j, t :: OpKind
t)) ->
                          ((SORT -> SORT
trId SORT
i, Type -> TypeScheme
simpleTypeScheme (Type -> TypeScheme) -> Type -> TypeScheme
forall a b. (a -> b) -> a -> b
$ OpType -> Type
fromOpType OpType
ot),
                           (SORT -> SORT
trId SORT
j, Type -> TypeScheme
simpleTypeScheme (Type -> TypeScheme) -> Type -> TypeScheme
forall a b. (a -> b) -> a -> b
$ Sort_map -> Type -> Type
mapType Sort_map
tm
                                 (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$ OpType -> Type
fromOpType OpType
ot { opKind :: OpKind
CasS.opKind = OpKind
t })))
                    ([((SORT, OpType), (SORT, OpKind))]
 -> [((SORT, TypeScheme), (SORT, TypeScheme))])
-> [((SORT, OpType), (SORT, OpKind))]
-> [((SORT, TypeScheme), (SORT, TypeScheme))]
forall a b. (a -> b) -> a -> b
$ Map (SORT, OpType) (SORT, OpKind)
-> [((SORT, OpType), (SORT, OpKind))]
forall k a. Map k a -> [(k, a)]
Map.toList (Map (SORT, OpType) (SORT, OpKind)
 -> [((SORT, OpType), (SORT, OpKind))])
-> Map (SORT, OpType) (SORT, OpKind)
-> [((SORT, OpType), (SORT, OpKind))]
forall a b. (a -> b) -> a -> b
$ Morphism f e m -> Map (SORT, OpType) (SORT, OpKind)
forall f e m. Morphism f e m -> Map (SORT, OpType) (SORT, OpKind)
CasM.op_map Morphism f e m
m
               f2 :: [((SORT, TypeScheme), (SORT, TypeScheme))]
f2 = (((SORT, PredType), SORT)
 -> ((SORT, TypeScheme), (SORT, TypeScheme)))
-> [((SORT, PredType), SORT)]
-> [((SORT, TypeScheme), (SORT, TypeScheme))]
forall a b. (a -> b) -> [a] -> [b]
map ( \ ((i :: SORT
i, pt :: PredType
pt), j :: SORT
j) ->
                          let ty :: Type
ty = PredType -> Type
fromPredType PredType
pt
                          in ( (SORT -> SORT
trId SORT
i, Type -> TypeScheme
simpleTypeScheme Type
ty)
                             , (SORT -> SORT
trId SORT
j, Type -> TypeScheme
simpleTypeScheme (Type -> TypeScheme) -> Type -> TypeScheme
forall a b. (a -> b) -> a -> b
$ Sort_map -> Type -> Type
mapType Sort_map
tm Type
ty)))
                    ([((SORT, PredType), SORT)]
 -> [((SORT, TypeScheme), (SORT, TypeScheme))])
-> [((SORT, PredType), SORT)]
-> [((SORT, TypeScheme), (SORT, TypeScheme))]
forall a b. (a -> b) -> a -> b
$ Map (SORT, PredType) SORT -> [((SORT, PredType), SORT)]
forall k a. Map k a -> [(k, a)]
Map.toList (Map (SORT, PredType) SORT -> [((SORT, PredType), SORT)])
-> Map (SORT, PredType) SORT -> [((SORT, PredType), SORT)]
forall a b. (a -> b) -> a -> b
$ Morphism f e m -> Map (SORT, PredType) SORT
forall f e m. Morphism f e m -> Map (SORT, PredType) SORT
CasM.pred_map Morphism f e m
m
            in (Env -> Env -> Morphism
mkMorphism (Set (SORT, OpType) -> Sign f e -> Env
forall f e. Set (SORT, OpType) -> Sign f e -> Env
mapSig Set (SORT, OpType)
forall a. Set a
Set.empty (Sign f e -> Env) -> Sign f e -> Env
forall a b. (a -> b) -> a -> b
$ Morphism f e m -> Sign f e
forall f e m. Morphism f e m -> Sign f e
CasM.msource Morphism f e m
m)
                               (Set (SORT, OpType) -> Sign f e -> Env
forall f e. Set (SORT, OpType) -> Sign f e -> Env
mapSig Set (SORT, OpType)
forall a. Set a
Set.empty (Sign f e -> Env) -> Sign f e -> Env
forall a b. (a -> b) -> a -> b
$ Morphism f e m -> Sign f e
forall f e m. Morphism f e m -> Sign f e
CasM.mtarget Morphism f e m
m))
           { typeIdMap :: Sort_map
typeIdMap = Sort_map
tm , funMap :: FunMap
funMap = [((SORT, TypeScheme), (SORT, TypeScheme))] -> FunMap
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([((SORT, TypeScheme), (SORT, TypeScheme))] -> FunMap)
-> [((SORT, TypeScheme), (SORT, TypeScheme))] -> FunMap
forall a b. (a -> b) -> a -> b
$ [((SORT, TypeScheme), (SORT, TypeScheme))]
f2 [((SORT, TypeScheme), (SORT, TypeScheme))]
-> [((SORT, TypeScheme), (SORT, TypeScheme))]
-> [((SORT, TypeScheme), (SORT, TypeScheme))]
forall a. [a] -> [a] -> [a]
++ [((SORT, TypeScheme), (SORT, TypeScheme))]
f1 }

mapSym :: CasS.Symbol -> Symbol
mapSym :: Symbol -> Symbol
mapSym = (SORT -> SORT)
-> (OpType -> Type) -> (PredType -> Type) -> Symbol -> Symbol
mapSymAux SORT -> SORT
trId OpType -> Type
fromOpType PredType -> Type
fromPredType

mapSymAux :: (Id -> Id) -> (CasS.OpType -> Type)
  -> (CasS.PredType -> Type) -> CasS.Symbol -> Symbol
mapSymAux :: (SORT -> SORT)
-> (OpType -> Type) -> (PredType -> Type) -> Symbol -> Symbol
mapSymAux trI :: SORT -> SORT
trI trO :: OpType -> Type
trO trP :: PredType -> Type
trP s :: Symbol
s = let
  n :: SORT
n = Symbol -> SORT
CasS.symName Symbol
s
  i :: SORT
i = SORT -> SORT
trI SORT
n
  in case Symbol -> SymbType
CasS.symbType Symbol
s of
    CasS.OpAsItemType ot :: OpType
ot -> SORT -> TypeScheme -> Symbol
idToOpSymbol SORT
i (TypeScheme -> Symbol) -> (Type -> TypeScheme) -> Type -> Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> TypeScheme
simpleTypeScheme (Type -> Symbol) -> Type -> Symbol
forall a b. (a -> b) -> a -> b
$ OpType -> Type
trO OpType
ot
    CasS.PredAsItemType pt :: PredType
pt -> SORT -> TypeScheme -> Symbol
idToOpSymbol SORT
i (TypeScheme -> Symbol) -> (Type -> TypeScheme) -> Type -> Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> TypeScheme
simpleTypeScheme (Type -> Symbol) -> Type -> Symbol
forall a b. (a -> b) -> a -> b
$ PredType -> Type
trP PredType
pt
    CasS.SortAsItemType -> SORT -> RawKind -> Symbol
idToTypeSymbol SORT
n RawKind
rStar
    CasS.SubsortAsItemType _ -> SORT -> RawKind -> Symbol
idToTypeSymbol SORT
n RawKind
rStar

toQuant :: Cas.QUANTIFIER -> Quantifier
toQuant :: QUANTIFIER -> Quantifier
toQuant Cas.Universal = Quantifier
Universal
toQuant Cas.Existential = Quantifier
Existential
toQuant Cas.Unique_existential = Quantifier
Unique

toVarDecl :: Cas.VAR_DECL -> [GenVarDecl]
toVarDecl :: VAR_DECL -> [GenVarDecl]
toVarDecl (Cas.Var_decl vs :: [VAR]
vs s :: SORT
s ps :: Range
ps) =
           (VAR -> GenVarDecl) -> [VAR] -> [GenVarDecl]
forall a b. (a -> b) -> [a] -> [b]
map ( \ i :: VAR
i -> VarDecl -> GenVarDecl
GenVarDecl (VarDecl -> GenVarDecl) -> VarDecl -> GenVarDecl
forall a b. (a -> b) -> a -> b
$
                 SORT -> Type -> SeparatorKind -> Range -> VarDecl
VarDecl (VAR -> SORT
simpleIdToId VAR
i) (SORT -> Type
toType SORT
s) SeparatorKind
Other Range
ps) [VAR]
vs

toSentence :: (CasS.TermExtension f, FormExtension f)
  => Cas.FORMULA f -> Sentence
toSentence :: FORMULA f -> Sentence
toSentence f :: FORMULA f
f = case FORMULA f
f of
   Cas.Sort_gen_ax cs :: [Constraint]
cs b :: Bool
b -> let
       (sorts :: [SORT]
sorts, ops :: [OP_SYMB]
ops, smap :: [(SORT, SORT)]
smap) = [Constraint] -> ([SORT], [OP_SYMB], [(SORT, SORT)])
Cas.recover_Sort_gen_ax [Constraint]
cs
       genKind :: GenKind
genKind = if Bool
b then GenKind
Free else GenKind
Generated
       mapPart :: Cas.OpKind -> Partiality
       mapPart :: OpKind -> Partiality
mapPart cp :: OpKind
cp = case OpKind
cp of
                Cas.Total -> Partiality
HasCASL.As.Total
                Cas.Partial -> Partiality
HasCASL.As.Partial
       in [DataEntry] -> Sentence
DatatypeSen ([DataEntry] -> Sentence) -> [DataEntry] -> Sentence
forall a b. (a -> b) -> a -> b
$ (SORT -> DataEntry) -> [SORT] -> [DataEntry]
forall a b. (a -> b) -> [a] -> [b]
map ( \ s :: SORT
s ->
          Sort_map
-> SORT
-> GenKind
-> [TypeArg]
-> RawKind
-> Set AltDefn
-> DataEntry
DataEntry ([(SORT, SORT)] -> Sort_map
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(SORT, SORT)]
smap) SORT
s GenKind
genKind [] RawKind
rStar
          (Set AltDefn -> DataEntry) -> Set AltDefn -> DataEntry
forall a b. (a -> b) -> a -> b
$ [AltDefn] -> Set AltDefn
forall a. Ord a => [a] -> Set a
Set.fromList ([AltDefn] -> Set AltDefn) -> [AltDefn] -> Set AltDefn
forall a b. (a -> b) -> a -> b
$ ((SORT, OpType) -> AltDefn) -> [(SORT, OpType)] -> [AltDefn]
forall a b. (a -> b) -> [a] -> [b]
map ( \ (i :: SORT
i, t :: OpType
t) ->
            let args :: [Type]
args = (SORT -> Type) -> [SORT] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map SORT -> Type
toType ([SORT] -> [Type]) -> [SORT] -> [Type]
forall a b. (a -> b) -> a -> b
$ OpType -> [SORT]
CasS.opArgs OpType
t in
            Maybe SORT -> [Type] -> Partiality -> [[Selector]] -> AltDefn
Construct (if SORT -> Bool
isInjName SORT
i then Maybe SORT
forall a. Maybe a
Nothing else SORT -> Maybe SORT
forall a. a -> Maybe a
Just SORT
i)
              (if [Type] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Type]
args then [] else [[Type] -> Type
mkProductType [Type]
args])
              (OpKind -> Partiality
mapPart (OpKind -> Partiality) -> OpKind -> Partiality
forall a b. (a -> b) -> a -> b
$ OpType -> OpKind
CasS.opKind OpType
t)
              ([[Selector]] -> AltDefn) -> [[Selector]] -> AltDefn
forall a b. (a -> b) -> a -> b
$ if [Type] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Type]
args then [] else
              [(Type -> Selector) -> [Type] -> [Selector]
forall a b. (a -> b) -> [a] -> [b]
map (\ a :: Type
a -> Maybe SORT -> Type -> Partiality -> Selector
Select Maybe SORT
forall a. Maybe a
Nothing Type
a Partiality
HasCASL.As.Total) [Type]
args])
          ([(SORT, OpType)] -> [AltDefn]) -> [(SORT, OpType)] -> [AltDefn]
forall a b. (a -> b) -> a -> b
$ ((SORT, OpType) -> Bool) -> [(SORT, OpType)] -> [(SORT, OpType)]
forall a. (a -> Bool) -> [a] -> [a]
filter ( \ (_, t :: OpType
t) -> OpType -> SORT
CasS.opRes OpType
t SORT -> SORT -> Bool
forall a. Eq a => a -> a -> Bool
== SORT
s)
                ([(SORT, OpType)] -> [(SORT, OpType)])
-> [(SORT, OpType)] -> [(SORT, OpType)]
forall a b. (a -> b) -> a -> b
$ (OP_SYMB -> (SORT, OpType)) -> [OP_SYMB] -> [(SORT, OpType)]
forall a b. (a -> b) -> [a] -> [b]
map ( \ o :: OP_SYMB
o -> case OP_SYMB
o of
                        Cas.Qual_op_name i :: SORT
i t :: OP_TYPE
t _ -> (SORT -> SORT
trId SORT
i, OP_TYPE -> OpType
CasS.toOpType OP_TYPE
t)
                        _ -> String -> (SORT, OpType)
forall a. HasCallStack => String -> a
error "CASL2HasCASL.toSentence") [OP_SYMB]
ops) [SORT]
sorts
   _ -> Term -> Sentence
Formula (Term -> Sentence) -> Term -> Sentence
forall a b. (a -> b) -> a -> b
$ FORMULA f -> Term
forall f. (TermExtension f, FormExtension f) => FORMULA f -> Term
toTerm FORMULA f
f

toTerm :: (CasS.TermExtension f, FormExtension f) => Cas.FORMULA f -> Term
toTerm :: FORMULA f -> Term
toTerm f :: FORMULA f
f = Record f Term Term -> FORMULA f -> Term
forall f a b. Record f a b -> FORMULA f -> a
foldFormula (String -> Record f Term Term
forall f. TermExtension f => String -> Record f Term Term
transRecord (String -> Record f Term Term) -> String -> Record f Term Term
forall a b. (a -> b) -> a -> b
$ FORMULA f -> ShowS
forall a. Pretty a => a -> ShowS
showDoc FORMULA f
f "") FORMULA f
f

transRecord :: CasS.TermExtension f => String -> Record f Term Term
transRecord :: String -> Record f Term Term
transRecord str :: String
str = let err :: a
err = String -> a
forall a. HasCallStack => String -> a
error (String -> a) -> String -> a
forall a b. (a -> b) -> a -> b
$ "CASL2HasCASL.unexpected formula: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
str
  in ((f -> Term) -> ([Term] -> Term) -> Term -> Record f Term Term
forall f a. (f -> a) -> ([a] -> a) -> a -> Record f a a
constRecord f -> Term
forall a. a
err [Term] -> Term
forall a. a
err Term
forall a. a
err)
  { foldQuantification :: FORMULA f -> QUANTIFIER -> [VAR_DECL] -> Term -> Range -> Term
foldQuantification = \ _ q :: QUANTIFIER
q -> Quantifier -> [GenVarDecl] -> Term -> Range -> Term
QuantifiedTerm (QUANTIFIER -> Quantifier
toQuant QUANTIFIER
q)
        ([GenVarDecl] -> Term -> Range -> Term)
-> ([VAR_DECL] -> [GenVarDecl])
-> [VAR_DECL]
-> Term
-> Range
-> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (VAR_DECL -> [GenVarDecl]) -> [VAR_DECL] -> [GenVarDecl]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap VAR_DECL -> [GenVarDecl]
toVarDecl
  , foldJunction :: FORMULA f -> Junctor -> [Term] -> Range -> Term
foldJunction = \ _ j :: Junctor
j fs :: [Term]
fs ps :: Range
ps -> let
       (n :: SORT
n, op :: SORT
op) = case Junctor
j of
          Cas.Con -> (SORT
trueId, SORT
andId)
          Cas.Dis -> (SORT
falseId, SORT
orId)
       in case [Term]
fs of
        [] -> SORT -> Range -> Term
unitTerm SORT
n Range
ps
        _ -> SORT -> [Term] -> Range -> Term
toBinJunctor SORT
op [Term]
fs Range
ps
  , foldRelation :: FORMULA f -> Term -> Relation -> Term -> Range -> Term
foldRelation = \ _ f1 :: Term
f1 c :: Relation
c f2 :: Term
f2 ps :: Range
ps -> case Relation
c of
       Cas.Implication -> SORT -> Range -> Term -> Term -> Term
mkLogTerm SORT
implId Range
ps Term
f1 Term
f2
       Cas.RevImpl -> SORT -> Range -> Term -> Term -> Term
mkLogTerm SORT
infixIf Range
ps Term
f2 Term
f1
       Cas.Equivalence -> SORT -> Range -> Term -> Term -> Term
mkLogTerm SORT
eqvId Range
ps Term
f1 Term
f2
  , foldNegation :: FORMULA f -> Term -> Range -> Term
foldNegation = \ _ frm :: Term
frm ps :: Range
ps -> SORT -> TypeScheme -> [Type] -> Range -> Term -> Term
mkTerm SORT
notId TypeScheme
notType [] Range
ps Term
frm
  , foldAtom :: FORMULA f -> Bool -> Range -> Term
foldAtom = \ _ b :: Bool
b -> SORT -> Range -> Term
unitTerm (SORT -> Range -> Term) -> SORT -> Range -> Term
forall a b. (a -> b) -> a -> b
$ if Bool
b then SORT
trueId else SORT
falseId
  , foldEquation :: FORMULA f -> Term -> Equality -> Term -> Range -> Term
foldEquation = \ o :: FORMULA f
o t1 :: Term
t1 e :: Equality
e t2 :: Term
t2 ps :: Range
ps ->
        let Cas.Equation c1 :: TERM f
c1 _ _ _ = FORMULA f
o in
        SORT -> Type -> Range -> Term -> Term -> Term
mkEqTerm (if Equality
e Equality -> Equality -> Bool
forall a. Eq a => a -> a -> Bool
== Equality
Cas.Existl then SORT
exEq else SORT
eqId)
                     (TERM f -> Type
forall f. TermExtension f => TERM f -> Type
typeOfTerm TERM f
c1) Range
ps Term
t1 Term
t2
  , foldPredication :: FORMULA f -> PRED_SYMB -> [Term] -> Range -> Term
foldPredication = \ _ qpn :: PRED_SYMB
qpn args :: [Term]
args qs :: Range
qs ->
        let Cas.Qual_pred_name ui :: SORT
ui pty :: PRED_TYPE
pty@(Cas.Pred_type ts :: [SORT]
ts _) ps :: Range
ps = PRED_SYMB
qpn
            i :: SORT
i = SORT -> SORT
trId SORT
ui
            sc :: TypeScheme
sc = Type -> TypeScheme
simpleTypeScheme (Type -> TypeScheme) -> Type -> TypeScheme
forall a b. (a -> b) -> a -> b
$ PRED_TYPE -> Type
fromPREDTYPE PRED_TYPE
pty
            p :: Term
p = OpBrand
-> PolyId -> TypeScheme -> [Type] -> InstKind -> Range -> Term
QualOp OpBrand
Pred (SORT -> [TypeArg] -> Range -> PolyId
PolyId SORT
i [] Range
ps) TypeScheme
sc [] InstKind
Infer Range
ps
            in if [Term] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Term]
args then Term
p else Term -> TypeQual -> Type -> Range -> Term
TypedTerm
              (Term -> Term -> Range -> Term
ApplTerm Term
p ([Term] -> Range -> Term
mkTupleTerm ((Term -> SORT -> Term) -> [Term] -> [SORT] -> [Term]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith
               (\ tr :: Term
tr ty :: SORT
ty -> Term -> TypeQual -> Type -> Range -> Term
TypedTerm Term
tr TypeQual
Inferred (SORT -> Type
toType SORT
ty) Range
ps)
                [Term]
args [SORT]
ts) Range
qs) Range
qs)
              TypeQual
Inferred Type
unitType Range
ps
  , foldDefinedness :: FORMULA f -> Term -> Range -> Term
foldDefinedness = \ o :: FORMULA f
o t :: Term
t ps :: Range
ps ->
        let Cas.Definedness c :: TERM f
c _ = FORMULA f
o in
        SORT -> TypeScheme -> [Type] -> Range -> Term -> Term
mkTerm SORT
defId TypeScheme
defType [TERM f -> Type
forall f. TermExtension f => TERM f -> Type
typeOfTerm TERM f
c] Range
ps Term
t
  , foldMembership :: FORMULA f -> Term -> SORT -> Range -> Term
foldMembership = \ _ t :: Term
t -> Term -> TypeQual -> Type -> Range -> Term
TypedTerm Term
t TypeQual
InType (Type -> Range -> Term) -> (SORT -> Type) -> SORT -> Range -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SORT -> Type
toType
  , foldQuantOp :: FORMULA f -> SORT -> OP_TYPE -> Term -> Term
foldQuantOp = \ _ uo :: SORT
uo ty :: OP_TYPE
ty frm :: Term
frm -> let o :: SORT
o = SORT -> SORT
trId SORT
uo in
         Quantifier -> [GenVarDecl] -> Term -> Range -> Term
QuantifiedTerm Quantifier
Universal
         [VarDecl -> GenVarDecl
GenVarDecl (VarDecl -> GenVarDecl) -> VarDecl -> GenVarDecl
forall a b. (a -> b) -> a -> b
$ SORT -> Type -> SeparatorKind -> Range -> VarDecl
VarDecl SORT
o (OP_TYPE -> Type
fromOPTYPE OP_TYPE
ty) SeparatorKind
Other Range
nullRange]
         (SORT -> Term -> Term
qualName2var SORT
o Term
frm) Range
nullRange
  , foldQuantPred :: FORMULA f -> SORT -> PRED_TYPE -> Term -> Term
foldQuantPred = \ _ up :: SORT
up ty :: PRED_TYPE
ty frm :: Term
frm -> let p :: SORT
p = SORT -> SORT
trId SORT
up in
         Quantifier -> [GenVarDecl] -> Term -> Range -> Term
QuantifiedTerm Quantifier
Universal
         [VarDecl -> GenVarDecl
GenVarDecl (VarDecl -> GenVarDecl) -> VarDecl -> GenVarDecl
forall a b. (a -> b) -> a -> b
$ SORT -> Type -> SeparatorKind -> Range -> VarDecl
VarDecl SORT
p (PRED_TYPE -> Type
fromPREDTYPE PRED_TYPE
ty) SeparatorKind
Other Range
nullRange]
         (SORT -> Term -> Term
qualName2var SORT
p Term
frm) Range
nullRange
  , foldQual_var :: TERM f -> VAR -> SORT -> Range -> Term
foldQual_var = \ _ v :: VAR
v ty :: SORT
ty ->
        VarDecl -> Term
QualVar (VarDecl -> Term) -> (Range -> VarDecl) -> Range -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SORT -> Type -> SeparatorKind -> Range -> VarDecl
VarDecl (VAR -> SORT
simpleIdToId VAR
v) (SORT -> Type
toType SORT
ty) SeparatorKind
Other
  , foldApplication :: TERM f -> OP_SYMB -> [Term] -> Range -> Term
foldApplication = \ _ qon :: OP_SYMB
qon args :: [Term]
args qs :: Range
qs ->
        let Cas.Qual_op_name ui :: SORT
ui ot :: OP_TYPE
ot ps :: Range
ps = OP_SYMB
qon
            i :: SORT
i = SORT -> SORT
trId SORT
ui
            sc :: TypeScheme
sc = Type -> TypeScheme
simpleTypeScheme (Type -> TypeScheme) -> Type -> TypeScheme
forall a b. (a -> b) -> a -> b
$ OP_TYPE -> Type
fromOPTYPE OP_TYPE
ot
            o :: Term
o = OpBrand
-> PolyId -> TypeScheme -> [Type] -> InstKind -> Range -> Term
QualOp OpBrand
Op (SORT -> [TypeArg] -> Range -> PolyId
PolyId SORT
i [] Range
ps) TypeScheme
sc [] InstKind
Infer Range
ps
            at :: OpType
at = OP_TYPE -> OpType
CasS.toOpType OP_TYPE
ot
        in if [Term] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Term]
args then Term
o else Term -> TypeQual -> Type -> Range -> Term
TypedTerm
           (Term -> Term -> Range -> Term
ApplTerm Term
o ([Term] -> Range -> Term
mkTupleTerm ((Term -> SORT -> Term) -> [Term] -> [SORT] -> [Term]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith
               (\ tr :: Term
tr ty :: SORT
ty -> Term -> TypeQual -> Type -> Range -> Term
TypedTerm Term
tr TypeQual
Inferred (SORT -> Type
toType SORT
ty) Range
ps)
                [Term]
args ([SORT] -> [Term]) -> [SORT] -> [Term]
forall a b. (a -> b) -> a -> b
$ OpType -> [SORT]
CasS.opArgs OpType
at) Range
qs) Range
qs)
           TypeQual
Inferred (SORT -> Type
toType (SORT -> Type) -> SORT -> Type
forall a b. (a -> b) -> a -> b
$ OpType -> SORT
CasS.opRes OpType
at) Range
ps
  , foldSorted_term :: TERM f -> Term -> SORT -> Range -> Term
foldSorted_term = \ _ trm :: Term
trm -> Term -> TypeQual -> Type -> Range -> Term
TypedTerm Term
trm TypeQual
OfType (Type -> Range -> Term) -> (SORT -> Type) -> SORT -> Range -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SORT -> Type
toType
  , foldCast :: TERM f -> Term -> SORT -> Range -> Term
foldCast = \ _ trm :: Term
trm -> Term -> TypeQual -> Type -> Range -> Term
TypedTerm Term
trm TypeQual
AsType (Type -> Range -> Term) -> (SORT -> Type) -> SORT -> Range -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SORT -> Type
toType
  , foldConditional :: TERM f -> Term -> Term -> Term -> Range -> Term
foldConditional = \ o :: TERM f
o t1 :: Term
t1 f :: Term
f t2 :: Term
t2 ps :: Range
ps ->
        let Cas.Conditional c1 :: TERM f
c1 _ _ _ = TERM f
o in
        SORT -> TypeScheme -> [Type] -> Range -> Term -> Term
mkTerm SORT
whenElse TypeScheme
whenType [TERM f -> Type
forall f. TermExtension f => TERM f -> Type
typeOfTerm TERM f
c1] Range
ps
          (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ [Term] -> Range -> Term
TupleTerm [Term
t1, Term
f, Term
t2] Range
ps
  , foldSort_gen_ax :: FORMULA f -> [Constraint] -> Bool -> Term
foldSort_gen_ax = \ _ cs :: [Constraint]
cs _ ->
      String -> Term
forall a. HasCallStack => String -> a
error (String -> Term) -> String -> Term
forall a b. (a -> b) -> a -> b
$ "unexpected sort generation constraint: "
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ [String] -> String
unlines ((Annoted DATATYPE_DECL -> String)
-> [Annoted DATATYPE_DECL] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (Annoted DATATYPE_DECL -> ShowS
forall a. Pretty a => a -> ShowS
`showDoc` "") ([Annoted DATATYPE_DECL] -> [String])
-> [Annoted DATATYPE_DECL] -> [String]
forall a b. (a -> b) -> a -> b
$ [Constraint] -> [Annoted DATATYPE_DECL]
recoverType [Constraint]
cs)
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ "in: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
str
  }

typeOfTerm :: CasS.TermExtension f => Cas.TERM f -> Type
typeOfTerm :: TERM f -> Type
typeOfTerm = SORT -> Type
toType (SORT -> Type) -> (TERM f -> SORT) -> TERM f -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TERM f -> SORT
forall f. TermExtension f => f -> SORT
CasS.sortOfTerm

-- | replace qualified names by variables in second order formulas
qualName2var :: Id -> Term -> Term
qualName2var :: SORT -> Term -> Term
qualName2var i :: SORT
i = FoldRec Term ProgEq -> Term -> Term
forall a b. FoldRec a b -> Term -> a
HasFold.foldTerm FoldRec Term ProgEq
mapRec
  { foldQualOp :: Term
-> OpBrand
-> PolyId
-> TypeScheme
-> [Type]
-> InstKind
-> Range
-> Term
foldQualOp = \ t :: Term
t _ (PolyId j :: SORT
j _ _) (TypeScheme _ ty :: Type
ty _) _ _ ps :: Range
ps ->
      if SORT
i SORT -> SORT -> Bool
forall a. Eq a => a -> a -> Bool
== SORT
j then VarDecl -> Term
QualVar (VarDecl -> Term) -> VarDecl -> Term
forall a b. (a -> b) -> a -> b
$ SORT -> Type -> SeparatorKind -> Range -> VarDecl
VarDecl SORT
i Type
ty SeparatorKind
Other Range
ps else Term
t }

-- | the invisible identifier is reserved for application
trId :: Id -> Id
trId :: SORT -> SORT
trId i :: SORT
i@(Id ts :: [VAR]
ts cs :: [SORT]
cs ps :: Range
ps) = if [SORT] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [SORT]
cs Bool -> Bool -> Bool
&& (VAR -> Bool) -> [VAR] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all VAR -> Bool
isPlace [VAR]
ts then
  [VAR] -> [SORT] -> Range -> SORT
Id [String -> Int -> VAR
genNumVar "empty" (Int -> VAR) -> Int -> VAR
forall a b. (a -> b) -> a -> b
$ [VAR] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [VAR]
ts] [SORT]
cs Range
ps else SORT
i