{- |
Module      :  ./HasCASL/FoldTerm.hs
Description :  fold functions for terms and program equations
Copyright   :  (c) Christian Maeder and Uni Bremen 2005
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Christian.Maeder@dfki.de
Stability   :  provisional
Portability :  portable

folding terms
-}

module HasCASL.FoldTerm where

import HasCASL.As
import Common.Id
import qualified Data.Set as Set

data FoldRec a b = FoldRec
    { FoldRec a b -> Term -> VarDecl -> a
foldQualVar :: Term -> VarDecl -> a
    , FoldRec a b
-> Term
-> OpBrand
-> PolyId
-> TypeScheme
-> [Type]
-> InstKind
-> Range
-> a
foldQualOp :: Term -> OpBrand -> PolyId -> TypeScheme -> [Type]
        -> InstKind -> Range -> a
    , FoldRec a b -> Term -> a -> a -> Range -> a
foldApplTerm :: Term -> a -> a -> Range -> a
    , FoldRec a b -> Term -> [a] -> Range -> a
foldTupleTerm :: Term -> [a] -> Range -> a
    , FoldRec a b -> Term -> a -> TypeQual -> Type -> Range -> a
foldTypedTerm :: Term -> a -> TypeQual -> Type -> Range -> a
    , FoldRec a b -> Term -> VarDecl -> a -> Range -> a
foldAsPattern :: Term -> VarDecl -> a -> Range -> a
    , FoldRec a b
-> Term -> Quantifier -> [GenVarDecl] -> a -> Range -> a
foldQuantifiedTerm
        :: Term -> Quantifier -> [GenVarDecl] -> a -> Range -> a
    , FoldRec a b -> Term -> [a] -> Partiality -> a -> Range -> a
foldLambdaTerm :: Term -> [a] -> Partiality -> a -> Range -> a
    , FoldRec a b -> Term -> a -> [b] -> Range -> a
foldCaseTerm :: Term -> a -> [b] -> Range -> a
    , FoldRec a b -> Term -> LetBrand -> [b] -> a -> Range -> a
foldLetTerm :: Term -> LetBrand -> [b] -> a -> Range -> a
    , FoldRec a b -> Term -> Id -> [Type] -> [a] -> Range -> a
foldResolvedMixTerm :: Term -> Id -> [Type] -> [a] -> Range -> a
    , FoldRec a b -> Term -> Token -> a
foldTermToken :: Term -> Token -> a
    , FoldRec a b -> Term -> TypeQual -> Type -> Range -> a
foldMixTypeTerm :: Term -> TypeQual -> Type -> Range -> a
    , FoldRec a b -> Term -> [a] -> a
foldMixfixTerm :: Term -> [a] -> a
    , FoldRec a b -> Term -> BracketKind -> [a] -> Range -> a
foldBracketTerm :: Term -> BracketKind -> [a] -> Range -> a
    , FoldRec a b -> ProgEq -> a -> a -> Range -> b
foldProgEq :: ProgEq -> a -> a -> Range -> b
    }

type MapRec = FoldRec Term ProgEq

mapRec :: MapRec
mapRec :: MapRec
mapRec = FoldRec :: forall a b.
(Term -> VarDecl -> a)
-> (Term
    -> OpBrand
    -> PolyId
    -> TypeScheme
    -> [Type]
    -> InstKind
    -> Range
    -> a)
-> (Term -> a -> a -> Range -> a)
-> (Term -> [a] -> Range -> a)
-> (Term -> a -> TypeQual -> Type -> Range -> a)
-> (Term -> VarDecl -> a -> Range -> a)
-> (Term -> Quantifier -> [GenVarDecl] -> a -> Range -> a)
-> (Term -> [a] -> Partiality -> a -> Range -> a)
-> (Term -> a -> [b] -> Range -> a)
-> (Term -> LetBrand -> [b] -> a -> Range -> a)
-> (Term -> Id -> [Type] -> [a] -> Range -> a)
-> (Term -> Token -> a)
-> (Term -> TypeQual -> Type -> Range -> a)
-> (Term -> [a] -> a)
-> (Term -> BracketKind -> [a] -> Range -> a)
-> (ProgEq -> a -> a -> Range -> b)
-> FoldRec a b
FoldRec
    { foldQualVar :: Term -> VarDecl -> Term
foldQualVar = (VarDecl -> Term) -> Term -> VarDecl -> Term
forall a b. a -> b -> a
const VarDecl -> Term
QualVar
    , foldQualOp :: Term
-> OpBrand
-> PolyId
-> TypeScheme
-> [Type]
-> InstKind
-> Range
-> Term
foldQualOp = (OpBrand
 -> PolyId -> TypeScheme -> [Type] -> InstKind -> Range -> Term)
-> Term
-> OpBrand
-> PolyId
-> TypeScheme
-> [Type]
-> InstKind
-> Range
-> Term
forall a b. a -> b -> a
const OpBrand
-> PolyId -> TypeScheme -> [Type] -> InstKind -> Range -> Term
QualOp
    , foldApplTerm :: Term -> Term -> Term -> Range -> Term
foldApplTerm = (Term -> Term -> Range -> Term)
-> Term -> Term -> Term -> Range -> Term
forall a b. a -> b -> a
const Term -> Term -> Range -> Term
ApplTerm
    , foldTupleTerm :: Term -> [Term] -> Range -> Term
foldTupleTerm = ([Term] -> Range -> Term) -> Term -> [Term] -> Range -> Term
forall a b. a -> b -> a
const [Term] -> Range -> Term
TupleTerm
    , foldTypedTerm :: Term -> Term -> TypeQual -> Type -> Range -> Term
foldTypedTerm = (Term -> TypeQual -> Type -> Range -> Term)
-> Term -> Term -> TypeQual -> Type -> Range -> Term
forall a b. a -> b -> a
const Term -> TypeQual -> Type -> Range -> Term
TypedTerm
    , foldAsPattern :: Term -> VarDecl -> Term -> Range -> Term
foldAsPattern = (VarDecl -> Term -> Range -> Term)
-> Term -> VarDecl -> Term -> Range -> Term
forall a b. a -> b -> a
const VarDecl -> Term -> Range -> Term
AsPattern
    , foldQuantifiedTerm :: Term -> Quantifier -> [GenVarDecl] -> Term -> Range -> Term
foldQuantifiedTerm = (Quantifier -> [GenVarDecl] -> Term -> Range -> Term)
-> Term -> Quantifier -> [GenVarDecl] -> Term -> Range -> Term
forall a b. a -> b -> a
const Quantifier -> [GenVarDecl] -> Term -> Range -> Term
QuantifiedTerm
    , foldLambdaTerm :: Term -> [Term] -> Partiality -> Term -> Range -> Term
foldLambdaTerm = ([Term] -> Partiality -> Term -> Range -> Term)
-> Term -> [Term] -> Partiality -> Term -> Range -> Term
forall a b. a -> b -> a
const [Term] -> Partiality -> Term -> Range -> Term
LambdaTerm
    , foldCaseTerm :: Term -> Term -> [ProgEq] -> Range -> Term
foldCaseTerm = (Term -> [ProgEq] -> Range -> Term)
-> Term -> Term -> [ProgEq] -> Range -> Term
forall a b. a -> b -> a
const Term -> [ProgEq] -> Range -> Term
CaseTerm
    , foldLetTerm :: Term -> LetBrand -> [ProgEq] -> Term -> Range -> Term
foldLetTerm = (LetBrand -> [ProgEq] -> Term -> Range -> Term)
-> Term -> LetBrand -> [ProgEq] -> Term -> Range -> Term
forall a b. a -> b -> a
const LetBrand -> [ProgEq] -> Term -> Range -> Term
LetTerm
    , foldResolvedMixTerm :: Term -> Id -> [Type] -> [Term] -> Range -> Term
foldResolvedMixTerm = (Id -> [Type] -> [Term] -> Range -> Term)
-> Term -> Id -> [Type] -> [Term] -> Range -> Term
forall a b. a -> b -> a
const Id -> [Type] -> [Term] -> Range -> Term
ResolvedMixTerm
    , foldTermToken :: Term -> Token -> Term
foldTermToken = (Token -> Term) -> Term -> Token -> Term
forall a b. a -> b -> a
const Token -> Term
TermToken
    , foldMixTypeTerm :: Term -> TypeQual -> Type -> Range -> Term
foldMixTypeTerm = (TypeQual -> Type -> Range -> Term)
-> Term -> TypeQual -> Type -> Range -> Term
forall a b. a -> b -> a
const TypeQual -> Type -> Range -> Term
MixTypeTerm
    , foldMixfixTerm :: Term -> [Term] -> Term
foldMixfixTerm = ([Term] -> Term) -> Term -> [Term] -> Term
forall a b. a -> b -> a
const [Term] -> Term
MixfixTerm
    , foldBracketTerm :: Term -> BracketKind -> [Term] -> Range -> Term
foldBracketTerm = (BracketKind -> [Term] -> Range -> Term)
-> Term -> BracketKind -> [Term] -> Range -> Term
forall a b. a -> b -> a
const BracketKind -> [Term] -> Range -> Term
BracketTerm
    , foldProgEq :: ProgEq -> Term -> Term -> Range -> ProgEq
foldProgEq = (Term -> Term -> Range -> ProgEq)
-> ProgEq -> Term -> Term -> Range -> ProgEq
forall a b. a -> b -> a
const Term -> Term -> Range -> ProgEq
ProgEq
    }

foldTerm :: FoldRec a b -> Term -> a
foldTerm :: FoldRec a b -> Term -> a
foldTerm r :: FoldRec a b
r t :: Term
t = case Term
t of
   QualVar vd :: VarDecl
vd -> FoldRec a b -> Term -> VarDecl -> a
forall a b. FoldRec a b -> Term -> VarDecl -> a
foldQualVar FoldRec a b
r Term
t VarDecl
vd
   QualOp b :: OpBrand
b i :: PolyId
i sc :: TypeScheme
sc tys :: [Type]
tys k :: InstKind
k qs :: Range
qs -> FoldRec a b
-> Term
-> OpBrand
-> PolyId
-> TypeScheme
-> [Type]
-> InstKind
-> Range
-> a
forall a b.
FoldRec a b
-> Term
-> OpBrand
-> PolyId
-> TypeScheme
-> [Type]
-> InstKind
-> Range
-> a
foldQualOp FoldRec a b
r Term
t OpBrand
b PolyId
i TypeScheme
sc [Type]
tys InstKind
k Range
qs
   ApplTerm t1 :: Term
t1 t2 :: Term
t2 ps :: Range
ps ->
       FoldRec a b -> Term -> a -> a -> Range -> a
forall a b. FoldRec a b -> Term -> a -> a -> Range -> a
foldApplTerm FoldRec a b
r Term
t (FoldRec a b -> Term -> a
forall a b. FoldRec a b -> Term -> a
foldTerm FoldRec a b
r Term
t1) (FoldRec a b -> Term -> a
forall a b. FoldRec a b -> Term -> a
foldTerm FoldRec a b
r Term
t2) Range
ps
   TupleTerm ts :: [Term]
ts ps :: Range
ps -> FoldRec a b -> Term -> [a] -> Range -> a
forall a b. FoldRec a b -> Term -> [a] -> Range -> a
foldTupleTerm FoldRec a b
r Term
t ((Term -> a) -> [Term] -> [a]
forall a b. (a -> b) -> [a] -> [b]
map (FoldRec a b -> Term -> a
forall a b. FoldRec a b -> Term -> a
foldTerm FoldRec a b
r) [Term]
ts) Range
ps
   TypedTerm te :: Term
te q :: TypeQual
q ty :: Type
ty ps :: Range
ps -> FoldRec a b -> Term -> a -> TypeQual -> Type -> Range -> a
forall a b.
FoldRec a b -> Term -> a -> TypeQual -> Type -> Range -> a
foldTypedTerm FoldRec a b
r Term
t (FoldRec a b -> Term -> a
forall a b. FoldRec a b -> Term -> a
foldTerm FoldRec a b
r Term
te) TypeQual
q Type
ty Range
ps
   QuantifiedTerm q :: Quantifier
q vs :: [GenVarDecl]
vs te :: Term
te ps :: Range
ps ->
       FoldRec a b
-> Term -> Quantifier -> [GenVarDecl] -> a -> Range -> a
forall a b.
FoldRec a b
-> Term -> Quantifier -> [GenVarDecl] -> a -> Range -> a
foldQuantifiedTerm FoldRec a b
r Term
t Quantifier
q [GenVarDecl]
vs (FoldRec a b -> Term -> a
forall a b. FoldRec a b -> Term -> a
foldTerm FoldRec a b
r Term
te) Range
ps
   LambdaTerm ps :: [Term]
ps p :: Partiality
p te :: Term
te qs :: Range
qs ->
       FoldRec a b -> Term -> [a] -> Partiality -> a -> Range -> a
forall a b.
FoldRec a b -> Term -> [a] -> Partiality -> a -> Range -> a
foldLambdaTerm FoldRec a b
r Term
t ((Term -> a) -> [Term] -> [a]
forall a b. (a -> b) -> [a] -> [b]
map (FoldRec a b -> Term -> a
forall a b. FoldRec a b -> Term -> a
foldTerm FoldRec a b
r) [Term]
ps) Partiality
p (FoldRec a b -> Term -> a
forall a b. FoldRec a b -> Term -> a
foldTerm FoldRec a b
r Term
te) Range
qs
   CaseTerm te :: Term
te es :: [ProgEq]
es ps :: Range
ps ->
       FoldRec a b -> Term -> a -> [b] -> Range -> a
forall a b. FoldRec a b -> Term -> a -> [b] -> Range -> a
foldCaseTerm FoldRec a b
r Term
t (FoldRec a b -> Term -> a
forall a b. FoldRec a b -> Term -> a
foldTerm FoldRec a b
r Term
te) ((ProgEq -> b) -> [ProgEq] -> [b]
forall a b. (a -> b) -> [a] -> [b]
map (FoldRec a b -> ProgEq -> b
forall a b. FoldRec a b -> ProgEq -> b
foldEq FoldRec a b
r) [ProgEq]
es) Range
ps
   LetTerm b :: LetBrand
b es :: [ProgEq]
es te :: Term
te ps :: Range
ps ->
       FoldRec a b -> Term -> LetBrand -> [b] -> a -> Range -> a
forall a b.
FoldRec a b -> Term -> LetBrand -> [b] -> a -> Range -> a
foldLetTerm FoldRec a b
r Term
t LetBrand
b ((ProgEq -> b) -> [ProgEq] -> [b]
forall a b. (a -> b) -> [a] -> [b]
map (FoldRec a b -> ProgEq -> b
forall a b. FoldRec a b -> ProgEq -> b
foldEq FoldRec a b
r) [ProgEq]
es) (FoldRec a b -> Term -> a
forall a b. FoldRec a b -> Term -> a
foldTerm FoldRec a b
r Term
te) Range
ps
   AsPattern vd :: VarDecl
vd pa :: Term
pa ps :: Range
ps -> FoldRec a b -> Term -> VarDecl -> a -> Range -> a
forall a b. FoldRec a b -> Term -> VarDecl -> a -> Range -> a
foldAsPattern FoldRec a b
r Term
t VarDecl
vd (FoldRec a b -> Term -> a
forall a b. FoldRec a b -> Term -> a
foldTerm FoldRec a b
r Term
pa) Range
ps
   TermToken tok :: Token
tok -> FoldRec a b -> Term -> Token -> a
forall a b. FoldRec a b -> Term -> Token -> a
foldTermToken FoldRec a b
r Term
t Token
tok
   MixfixTerm ts :: [Term]
ts -> FoldRec a b -> Term -> [a] -> a
forall a b. FoldRec a b -> Term -> [a] -> a
foldMixfixTerm FoldRec a b
r Term
t ([a] -> a) -> [a] -> a
forall a b. (a -> b) -> a -> b
$ (Term -> a) -> [Term] -> [a]
forall a b. (a -> b) -> [a] -> [b]
map (FoldRec a b -> Term -> a
forall a b. FoldRec a b -> Term -> a
foldTerm FoldRec a b
r) [Term]
ts
   BracketTerm b :: BracketKind
b ts :: [Term]
ts ps :: Range
ps -> FoldRec a b -> Term -> BracketKind -> [a] -> Range -> a
forall a b. FoldRec a b -> Term -> BracketKind -> [a] -> Range -> a
foldBracketTerm FoldRec a b
r Term
t BracketKind
b ((Term -> a) -> [Term] -> [a]
forall a b. (a -> b) -> [a] -> [b]
map (FoldRec a b -> Term -> a
forall a b. FoldRec a b -> Term -> a
foldTerm FoldRec a b
r) [Term]
ts) Range
ps
   MixTypeTerm q :: TypeQual
q ty :: Type
ty ps :: Range
ps -> FoldRec a b -> Term -> TypeQual -> Type -> Range -> a
forall a b. FoldRec a b -> Term -> TypeQual -> Type -> Range -> a
foldMixTypeTerm FoldRec a b
r Term
t TypeQual
q Type
ty Range
ps
   ResolvedMixTerm i :: Id
i tys :: [Type]
tys ts :: [Term]
ts ps :: Range
ps ->
       FoldRec a b -> Term -> Id -> [Type] -> [a] -> Range -> a
forall a b.
FoldRec a b -> Term -> Id -> [Type] -> [a] -> Range -> a
foldResolvedMixTerm FoldRec a b
r Term
t Id
i [Type]
tys ((Term -> a) -> [Term] -> [a]
forall a b. (a -> b) -> [a] -> [b]
map (FoldRec a b -> Term -> a
forall a b. FoldRec a b -> Term -> a
foldTerm FoldRec a b
r) [Term]
ts) Range
ps

foldEq :: FoldRec a b -> ProgEq -> b
foldEq :: FoldRec a b -> ProgEq -> b
foldEq r :: FoldRec a b
r e :: ProgEq
e@(ProgEq p :: Term
p t :: Term
t q :: Range
q) = FoldRec a b -> ProgEq -> a -> a -> Range -> b
forall a b. FoldRec a b -> ProgEq -> a -> a -> Range -> b
foldProgEq FoldRec a b
r ProgEq
e (FoldRec a b -> Term -> a
forall a b. FoldRec a b -> Term -> a
foldTerm FoldRec a b
r Term
p) (FoldRec a b -> Term -> a
forall a b. FoldRec a b -> Term -> a
foldTerm FoldRec a b
r Term
t) Range
q

getAllTypes :: Term -> [Type]
getAllTypes :: Term -> [Type]
getAllTypes = FoldRec [Type] [Type] -> Term -> [Type]
forall a b. FoldRec a b -> Term -> a
foldTerm FoldRec :: forall a b.
(Term -> VarDecl -> a)
-> (Term
    -> OpBrand
    -> PolyId
    -> TypeScheme
    -> [Type]
    -> InstKind
    -> Range
    -> a)
-> (Term -> a -> a -> Range -> a)
-> (Term -> [a] -> Range -> a)
-> (Term -> a -> TypeQual -> Type -> Range -> a)
-> (Term -> VarDecl -> a -> Range -> a)
-> (Term -> Quantifier -> [GenVarDecl] -> a -> Range -> a)
-> (Term -> [a] -> Partiality -> a -> Range -> a)
-> (Term -> a -> [b] -> Range -> a)
-> (Term -> LetBrand -> [b] -> a -> Range -> a)
-> (Term -> Id -> [Type] -> [a] -> Range -> a)
-> (Term -> Token -> a)
-> (Term -> TypeQual -> Type -> Range -> a)
-> (Term -> [a] -> a)
-> (Term -> BracketKind -> [a] -> Range -> a)
-> (ProgEq -> a -> a -> Range -> b)
-> FoldRec a b
FoldRec
    { foldQualVar :: Term -> VarDecl -> [Type]
foldQualVar = \ _ (VarDecl _ t :: Type
t _ _) -> [Type
t]
    , foldQualOp :: Term
-> OpBrand
-> PolyId
-> TypeScheme
-> [Type]
-> InstKind
-> Range
-> [Type]
foldQualOp = \ _ _ _ _ ts :: [Type]
ts _ _ -> [Type]
ts
    , foldApplTerm :: Term -> [Type] -> [Type] -> Range -> [Type]
foldApplTerm = \ _ t1 :: [Type]
t1 t2 :: [Type]
t2 _ -> [Type]
t1 [Type] -> [Type] -> [Type]
forall a. [a] -> [a] -> [a]
++ [Type]
t2
    , foldTupleTerm :: Term -> [[Type]] -> Range -> [Type]
foldTupleTerm = \ _ tts :: [[Type]]
tts _ -> [[Type]] -> [Type]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[Type]]
tts
    , foldTypedTerm :: Term -> [Type] -> TypeQual -> Type -> Range -> [Type]
foldTypedTerm = \ _ ts :: [Type]
ts _ t :: Type
t _ -> Type
t Type -> [Type] -> [Type]
forall a. a -> [a] -> [a]
: [Type]
ts
    , foldAsPattern :: Term -> VarDecl -> [Type] -> Range -> [Type]
foldAsPattern = \ _ (VarDecl _ t :: Type
t _ _) ts :: [Type]
ts _ -> Type
t Type -> [Type] -> [Type]
forall a. a -> [a] -> [a]
: [Type]
ts
    , foldQuantifiedTerm :: Term -> Quantifier -> [GenVarDecl] -> [Type] -> Range -> [Type]
foldQuantifiedTerm = \ _ _ gvs :: [GenVarDecl]
gvs ts :: [Type]
ts _ -> [Type]
ts [Type] -> [Type] -> [Type]
forall a. [a] -> [a] -> [a]
++ (GenVarDecl -> [Type]) -> [GenVarDecl] -> [Type]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap
         ( \ gv :: GenVarDecl
gv -> case GenVarDecl
gv of
                     GenVarDecl (VarDecl _ t :: Type
t _ _) -> [Type
t]
                     _ -> []) [GenVarDecl]
gvs
    , foldLambdaTerm :: Term -> [[Type]] -> Partiality -> [Type] -> Range -> [Type]
foldLambdaTerm = \ _ _ _ ts :: [Type]
ts _ -> [Type]
ts
    , foldCaseTerm :: Term -> [Type] -> [[Type]] -> Range -> [Type]
foldCaseTerm = \ _ ts :: [Type]
ts tts :: [[Type]]
tts _ -> [[Type]] -> [Type]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[Type]] -> [Type]) -> [[Type]] -> [Type]
forall a b. (a -> b) -> a -> b
$ [Type]
ts [Type] -> [[Type]] -> [[Type]]
forall a. a -> [a] -> [a]
: [[Type]]
tts
    , foldLetTerm :: Term -> LetBrand -> [[Type]] -> [Type] -> Range -> [Type]
foldLetTerm = \ _ _ tts :: [[Type]]
tts ts :: [Type]
ts _ -> [[Type]] -> [Type]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[Type]] -> [Type]) -> [[Type]] -> [Type]
forall a b. (a -> b) -> a -> b
$ [Type]
ts [Type] -> [[Type]] -> [[Type]]
forall a. a -> [a] -> [a]
: [[Type]]
tts
    , foldResolvedMixTerm :: Term -> Id -> [Type] -> [[Type]] -> Range -> [Type]
foldResolvedMixTerm = \ _ _ ts :: [Type]
ts tts :: [[Type]]
tts _ -> [Type]
ts [Type] -> [Type] -> [Type]
forall a. [a] -> [a] -> [a]
++ [[Type]] -> [Type]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[Type]]
tts
    , foldTermToken :: Term -> Token -> [Type]
foldTermToken = \ _ _ -> []
    , foldMixTypeTerm :: Term -> TypeQual -> Type -> Range -> [Type]
foldMixTypeTerm = \ _ _ _ _ -> []
    , foldMixfixTerm :: Term -> [[Type]] -> [Type]
foldMixfixTerm = ([[Type]] -> [Type]) -> Term -> [[Type]] -> [Type]
forall a b. a -> b -> a
const [[Type]] -> [Type]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
    , foldBracketTerm :: Term -> BracketKind -> [[Type]] -> Range -> [Type]
foldBracketTerm = \ _ _ tts :: [[Type]]
tts _ -> [[Type]] -> [Type]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[Type]]
tts
    , foldProgEq :: ProgEq -> [Type] -> [Type] -> Range -> [Type]
foldProgEq = \ _ ps :: [Type]
ps ts :: [Type]
ts _ -> [Type]
ps [Type] -> [Type] -> [Type]
forall a. [a] -> [a] -> [a]
++ [Type]
ts
    }

freeVars :: Term -> Set.Set VarDecl
freeVars :: Term -> Set VarDecl
freeVars = FoldRec (Set VarDecl) (Set VarDecl, Set VarDecl)
-> Term -> Set VarDecl
forall a b. FoldRec a b -> Term -> a
foldTerm FoldRec :: forall a b.
(Term -> VarDecl -> a)
-> (Term
    -> OpBrand
    -> PolyId
    -> TypeScheme
    -> [Type]
    -> InstKind
    -> Range
    -> a)
-> (Term -> a -> a -> Range -> a)
-> (Term -> [a] -> Range -> a)
-> (Term -> a -> TypeQual -> Type -> Range -> a)
-> (Term -> VarDecl -> a -> Range -> a)
-> (Term -> Quantifier -> [GenVarDecl] -> a -> Range -> a)
-> (Term -> [a] -> Partiality -> a -> Range -> a)
-> (Term -> a -> [b] -> Range -> a)
-> (Term -> LetBrand -> [b] -> a -> Range -> a)
-> (Term -> Id -> [Type] -> [a] -> Range -> a)
-> (Term -> Token -> a)
-> (Term -> TypeQual -> Type -> Range -> a)
-> (Term -> [a] -> a)
-> (Term -> BracketKind -> [a] -> Range -> a)
-> (ProgEq -> a -> a -> Range -> b)
-> FoldRec a b
FoldRec
    { foldQualVar :: Term -> VarDecl -> Set VarDecl
foldQualVar = (VarDecl -> Set VarDecl) -> Term -> VarDecl -> Set VarDecl
forall a b. a -> b -> a
const VarDecl -> Set VarDecl
forall a. a -> Set a
Set.singleton
    , foldQualOp :: Term
-> OpBrand
-> PolyId
-> TypeScheme
-> [Type]
-> InstKind
-> Range
-> Set VarDecl
foldQualOp = \ _ _ _ _ _ _ _ -> Set VarDecl
forall a. Set a
Set.empty
    , foldApplTerm :: Term -> Set VarDecl -> Set VarDecl -> Range -> Set VarDecl
foldApplTerm = \ _ t1 :: Set VarDecl
t1 t2 :: Set VarDecl
t2 _ -> Set VarDecl -> Set VarDecl -> Set VarDecl
forall a. Ord a => Set a -> Set a -> Set a
Set.union Set VarDecl
t1 Set VarDecl
t2
    , foldTupleTerm :: Term -> [Set VarDecl] -> Range -> Set VarDecl
foldTupleTerm = \ _ tts :: [Set VarDecl]
tts _ -> [Set VarDecl] -> Set VarDecl
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions [Set VarDecl]
tts
    , foldTypedTerm :: Term -> Set VarDecl -> TypeQual -> Type -> Range -> Set VarDecl
foldTypedTerm = \ _ ts :: Set VarDecl
ts _ _ _ -> Set VarDecl
ts
    , foldAsPattern :: Term -> VarDecl -> Set VarDecl -> Range -> Set VarDecl
foldAsPattern = \ _ t :: VarDecl
t ts :: Set VarDecl
ts _ -> VarDecl -> Set VarDecl -> Set VarDecl
forall a. Ord a => a -> Set a -> Set a
Set.insert VarDecl
t Set VarDecl
ts
    , foldQuantifiedTerm :: Term
-> Quantifier
-> [GenVarDecl]
-> Set VarDecl
-> Range
-> Set VarDecl
foldQuantifiedTerm = \ _ _ gvs :: [GenVarDecl]
gvs ts :: Set VarDecl
ts _ -> Set VarDecl -> Set VarDecl -> Set VarDecl
forall a. Ord a => Set a -> Set a -> Set a
Set.difference Set VarDecl
ts (Set VarDecl -> Set VarDecl) -> Set VarDecl -> Set VarDecl
forall a b. (a -> b) -> a -> b
$
         (GenVarDecl -> Set VarDecl -> Set VarDecl)
-> Set VarDecl -> [GenVarDecl] -> Set VarDecl
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ( \ gv :: GenVarDecl
gv -> case GenVarDecl
gv of
           GenVarDecl t :: VarDecl
t -> VarDecl -> Set VarDecl -> Set VarDecl
forall a. Ord a => a -> Set a -> Set a
Set.insert VarDecl
t
           _ -> Set VarDecl -> Set VarDecl
forall a. a -> a
id) Set VarDecl
forall a. Set a
Set.empty [GenVarDecl]
gvs
    , foldLambdaTerm :: Term
-> [Set VarDecl]
-> Partiality
-> Set VarDecl
-> Range
-> Set VarDecl
foldLambdaTerm = \ _ pats :: [Set VarDecl]
pats _ ts :: Set VarDecl
ts _ -> Set VarDecl -> Set VarDecl -> Set VarDecl
forall a. Ord a => Set a -> Set a -> Set a
Set.difference Set VarDecl
ts (Set VarDecl -> Set VarDecl) -> Set VarDecl -> Set VarDecl
forall a b. (a -> b) -> a -> b
$ [Set VarDecl] -> Set VarDecl
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions [Set VarDecl]
pats
    , foldCaseTerm :: Term
-> Set VarDecl
-> [(Set VarDecl, Set VarDecl)]
-> Range
-> Set VarDecl
foldCaseTerm = \ _ ts :: Set VarDecl
ts tts :: [(Set VarDecl, Set VarDecl)]
tts _ -> Set VarDecl -> Set VarDecl -> Set VarDecl
forall a. Ord a => Set a -> Set a -> Set a
Set.difference
          ([Set VarDecl] -> Set VarDecl
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ([Set VarDecl] -> Set VarDecl) -> [Set VarDecl] -> Set VarDecl
forall a b. (a -> b) -> a -> b
$ Set VarDecl
ts Set VarDecl -> [Set VarDecl] -> [Set VarDecl]
forall a. a -> [a] -> [a]
: ((Set VarDecl, Set VarDecl) -> Set VarDecl)
-> [(Set VarDecl, Set VarDecl)] -> [Set VarDecl]
forall a b. (a -> b) -> [a] -> [b]
map (Set VarDecl, Set VarDecl) -> Set VarDecl
forall a b. (a, b) -> b
snd [(Set VarDecl, Set VarDecl)]
tts) (Set VarDecl -> Set VarDecl) -> Set VarDecl -> Set VarDecl
forall a b. (a -> b) -> a -> b
$ [Set VarDecl] -> Set VarDecl
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ([Set VarDecl] -> Set VarDecl) -> [Set VarDecl] -> Set VarDecl
forall a b. (a -> b) -> a -> b
$ ((Set VarDecl, Set VarDecl) -> Set VarDecl)
-> [(Set VarDecl, Set VarDecl)] -> [Set VarDecl]
forall a b. (a -> b) -> [a] -> [b]
map (Set VarDecl, Set VarDecl) -> Set VarDecl
forall a b. (a, b) -> a
fst [(Set VarDecl, Set VarDecl)]
tts
    , foldLetTerm :: Term
-> LetBrand
-> [(Set VarDecl, Set VarDecl)]
-> Set VarDecl
-> Range
-> Set VarDecl
foldLetTerm = \ _ _ tts :: [(Set VarDecl, Set VarDecl)]
tts ts :: Set VarDecl
ts _ -> Set VarDecl -> Set VarDecl -> Set VarDecl
forall a. Ord a => Set a -> Set a -> Set a
Set.difference
          ([Set VarDecl] -> Set VarDecl
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ([Set VarDecl] -> Set VarDecl) -> [Set VarDecl] -> Set VarDecl
forall a b. (a -> b) -> a -> b
$ Set VarDecl
ts Set VarDecl -> [Set VarDecl] -> [Set VarDecl]
forall a. a -> [a] -> [a]
: ((Set VarDecl, Set VarDecl) -> Set VarDecl)
-> [(Set VarDecl, Set VarDecl)] -> [Set VarDecl]
forall a b. (a -> b) -> [a] -> [b]
map (Set VarDecl, Set VarDecl) -> Set VarDecl
forall a b. (a, b) -> b
snd [(Set VarDecl, Set VarDecl)]
tts) (Set VarDecl -> Set VarDecl) -> Set VarDecl -> Set VarDecl
forall a b. (a -> b) -> a -> b
$ [Set VarDecl] -> Set VarDecl
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ([Set VarDecl] -> Set VarDecl) -> [Set VarDecl] -> Set VarDecl
forall a b. (a -> b) -> a -> b
$ ((Set VarDecl, Set VarDecl) -> Set VarDecl)
-> [(Set VarDecl, Set VarDecl)] -> [Set VarDecl]
forall a b. (a -> b) -> [a] -> [b]
map (Set VarDecl, Set VarDecl) -> Set VarDecl
forall a b. (a, b) -> a
fst [(Set VarDecl, Set VarDecl)]
tts
    , foldResolvedMixTerm :: Term -> Id -> [Type] -> [Set VarDecl] -> Range -> Set VarDecl
foldResolvedMixTerm = \ _ _ _ tts :: [Set VarDecl]
tts _ -> [Set VarDecl] -> Set VarDecl
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions [Set VarDecl]
tts
    , foldTermToken :: Term -> Token -> Set VarDecl
foldTermToken = \ _ _ -> Set VarDecl
forall a. Set a
Set.empty
    , foldMixTypeTerm :: Term -> TypeQual -> Type -> Range -> Set VarDecl
foldMixTypeTerm = \ _ _ _ _ -> Set VarDecl
forall a. Set a
Set.empty
    , foldMixfixTerm :: Term -> [Set VarDecl] -> Set VarDecl
foldMixfixTerm = ([Set VarDecl] -> Set VarDecl)
-> Term -> [Set VarDecl] -> Set VarDecl
forall a b. a -> b -> a
const [Set VarDecl] -> Set VarDecl
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions
    , foldBracketTerm :: Term -> BracketKind -> [Set VarDecl] -> Range -> Set VarDecl
foldBracketTerm = \ _ _ tts :: [Set VarDecl]
tts _ -> [Set VarDecl] -> Set VarDecl
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions [Set VarDecl]
tts
    , foldProgEq :: ProgEq
-> Set VarDecl
-> Set VarDecl
-> Range
-> (Set VarDecl, Set VarDecl)
foldProgEq = \ _ ps :: Set VarDecl
ps ts :: Set VarDecl
ts _ -> (Set VarDecl
ps, Set VarDecl
ts)
    }

opsInTerm :: Term -> Set.Set Term
opsInTerm :: Term -> Set Term
opsInTerm = FoldRec (Set Term) (Set Term) -> Term -> Set Term
forall a b. FoldRec a b -> Term -> a
foldTerm FoldRec :: forall a b.
(Term -> VarDecl -> a)
-> (Term
    -> OpBrand
    -> PolyId
    -> TypeScheme
    -> [Type]
    -> InstKind
    -> Range
    -> a)
-> (Term -> a -> a -> Range -> a)
-> (Term -> [a] -> Range -> a)
-> (Term -> a -> TypeQual -> Type -> Range -> a)
-> (Term -> VarDecl -> a -> Range -> a)
-> (Term -> Quantifier -> [GenVarDecl] -> a -> Range -> a)
-> (Term -> [a] -> Partiality -> a -> Range -> a)
-> (Term -> a -> [b] -> Range -> a)
-> (Term -> LetBrand -> [b] -> a -> Range -> a)
-> (Term -> Id -> [Type] -> [a] -> Range -> a)
-> (Term -> Token -> a)
-> (Term -> TypeQual -> Type -> Range -> a)
-> (Term -> [a] -> a)
-> (Term -> BracketKind -> [a] -> Range -> a)
-> (ProgEq -> a -> a -> Range -> b)
-> FoldRec a b
FoldRec
    { foldQualVar :: Term -> VarDecl -> Set Term
foldQualVar = \ _ _ -> Set Term
forall a. Set a
Set.empty
    , foldQualOp :: Term
-> OpBrand
-> PolyId
-> TypeScheme
-> [Type]
-> InstKind
-> Range
-> Set Term
foldQualOp = \ _ ob :: OpBrand
ob n :: PolyId
n ts :: TypeScheme
ts tl :: [Type]
tl ik :: InstKind
ik rg :: Range
rg ->
                   Term -> Set Term
forall a. a -> Set a
Set.singleton (Term -> Set Term) -> Term -> Set Term
forall a b. (a -> b) -> a -> b
$ OpBrand
-> PolyId -> TypeScheme -> [Type] -> InstKind -> Range -> Term
QualOp OpBrand
ob PolyId
n TypeScheme
ts [Type]
tl InstKind
ik Range
rg
    , foldApplTerm :: Term -> Set Term -> Set Term -> Range -> Set Term
foldApplTerm = \ _ t1 :: Set Term
t1 t2 :: Set Term
t2 _ -> Set Term -> Set Term -> Set Term
forall a. Ord a => Set a -> Set a -> Set a
Set.union Set Term
t1 Set Term
t2
    , foldTupleTerm :: Term -> [Set Term] -> Range -> Set Term
foldTupleTerm = \ _ tts :: [Set Term]
tts _ -> [Set Term] -> Set Term
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions [Set Term]
tts
    , foldTypedTerm :: Term -> Set Term -> TypeQual -> Type -> Range -> Set Term
foldTypedTerm = \ _ ts :: Set Term
ts _ _ _ -> Set Term
ts
    , foldAsPattern :: Term -> VarDecl -> Set Term -> Range -> Set Term
foldAsPattern = \ _ _ ts :: Set Term
ts _ -> Set Term
ts
    , foldQuantifiedTerm :: Term -> Quantifier -> [GenVarDecl] -> Set Term -> Range -> Set Term
foldQuantifiedTerm = \ _ _ _ ts :: Set Term
ts _ -> Set Term
ts
    , foldLambdaTerm :: Term -> [Set Term] -> Partiality -> Set Term -> Range -> Set Term
foldLambdaTerm = \ _ pats :: [Set Term]
pats _ ts :: Set Term
ts _ -> [Set Term] -> Set Term
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ([Set Term] -> Set Term) -> [Set Term] -> Set Term
forall a b. (a -> b) -> a -> b
$ Set Term
ts Set Term -> [Set Term] -> [Set Term]
forall a. a -> [a] -> [a]
: [Set Term]
pats
    , foldCaseTerm :: Term -> Set Term -> [Set Term] -> Range -> Set Term
foldCaseTerm = \ _ ts :: Set Term
ts tts :: [Set Term]
tts _ -> [Set Term] -> Set Term
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ([Set Term] -> Set Term) -> [Set Term] -> Set Term
forall a b. (a -> b) -> a -> b
$ Set Term
ts Set Term -> [Set Term] -> [Set Term]
forall a. a -> [a] -> [a]
: [Set Term]
tts
    , foldLetTerm :: Term -> LetBrand -> [Set Term] -> Set Term -> Range -> Set Term
foldLetTerm = \ _ _ tts :: [Set Term]
tts ts :: Set Term
ts _ -> [Set Term] -> Set Term
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ([Set Term] -> Set Term) -> [Set Term] -> Set Term
forall a b. (a -> b) -> a -> b
$ Set Term
ts Set Term -> [Set Term] -> [Set Term]
forall a. a -> [a] -> [a]
: [Set Term]
tts
    , foldResolvedMixTerm :: Term -> Id -> [Type] -> [Set Term] -> Range -> Set Term
foldResolvedMixTerm = \ _ _ _ tts :: [Set Term]
tts _ -> [Set Term] -> Set Term
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions [Set Term]
tts
    , foldTermToken :: Term -> Token -> Set Term
foldTermToken = \ _ _ -> Set Term
forall a. Set a
Set.empty
    , foldMixTypeTerm :: Term -> TypeQual -> Type -> Range -> Set Term
foldMixTypeTerm = \ _ _ _ _ -> Set Term
forall a. Set a
Set.empty
    , foldMixfixTerm :: Term -> [Set Term] -> Set Term
foldMixfixTerm = ([Set Term] -> Set Term) -> Term -> [Set Term] -> Set Term
forall a b. a -> b -> a
const [Set Term] -> Set Term
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions
    , foldBracketTerm :: Term -> BracketKind -> [Set Term] -> Range -> Set Term
foldBracketTerm = \ _ _ tts :: [Set Term]
tts _ -> [Set Term] -> Set Term
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions [Set Term]
tts
    , foldProgEq :: ProgEq -> Set Term -> Set Term -> Range -> Set Term
foldProgEq = \ _ ps :: Set Term
ps ts :: Set Term
ts _ -> Set Term -> Set Term -> Set Term
forall a. Ord a => Set a -> Set a -> Set a
Set.union Set Term
ps Set Term
ts
    }