{- |
Module      :  ./CASL/Fold.hs
Description :  folding functions for CASL terms and formulas
Copyright   :  (c) Christian Maeder, Uni Bremen 2005
License     :  GPLv2 or higher, see LICENSE.txt

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

folding functions for CASL terms and formulas

-}

module CASL.Fold where

import Common.Id
import CASL.AS_Basic_CASL

data Record f a b = Record
    { Record f a b
-> FORMULA f -> QUANTIFIER -> [VAR_DECL] -> a -> Range -> a
foldQuantification :: FORMULA f -> QUANTIFIER -> [VAR_DECL] ->
                          a -> Range -> a
    , Record f a b -> FORMULA f -> Junctor -> [a] -> Range -> a
foldJunction :: FORMULA f -> Junctor -> [a] -> Range -> a
    , Record f a b -> FORMULA f -> a -> Relation -> a -> Range -> a
foldRelation :: FORMULA f -> a -> Relation -> a -> Range -> a
    , Record f a b -> FORMULA f -> a -> Range -> a
foldNegation :: FORMULA f -> a -> Range -> a
    , Record f a b -> FORMULA f -> Bool -> Range -> a
foldAtom :: FORMULA f -> Bool -> Range -> a
    , Record f a b -> FORMULA f -> PRED_SYMB -> [b] -> Range -> a
foldPredication :: FORMULA f -> PRED_SYMB -> [b] -> Range -> a
    , Record f a b -> FORMULA f -> b -> Range -> a
foldDefinedness :: FORMULA f -> b -> Range -> a
    , Record f a b -> FORMULA f -> b -> Equality -> b -> Range -> a
foldEquation :: FORMULA f -> b -> Equality -> b -> Range -> a
    , Record f a b -> FORMULA f -> b -> SORT -> Range -> a
foldMembership :: FORMULA f -> b -> SORT -> Range -> a
    , Record f a b -> FORMULA f -> b -> a
foldMixfix_formula :: FORMULA f -> b -> a
    , Record f a b -> FORMULA f -> [Constraint] -> Bool -> a
foldSort_gen_ax :: FORMULA f -> [Constraint] -> Bool -> a
    , Record f a b -> FORMULA f -> SORT -> OP_TYPE -> a -> a
foldQuantOp :: FORMULA f -> OP_NAME -> OP_TYPE -> a -> a
    , Record f a b -> FORMULA f -> SORT -> PRED_TYPE -> a -> a
foldQuantPred :: FORMULA f -> PRED_NAME -> PRED_TYPE -> a -> a
    , Record f a b -> FORMULA f -> f -> a
foldExtFORMULA :: FORMULA f -> f -> a
    , Record f a b -> TERM f -> VAR -> SORT -> Range -> b
foldQual_var :: TERM f -> VAR -> SORT -> Range -> b
    , Record f a b -> TERM f -> OP_SYMB -> [b] -> Range -> b
foldApplication :: TERM f -> OP_SYMB -> [b] -> Range -> b
    , Record f a b -> TERM f -> b -> SORT -> Range -> b
foldSorted_term :: TERM f -> b -> SORT -> Range -> b
    , Record f a b -> TERM f -> b -> SORT -> Range -> b
foldCast :: TERM f -> b -> SORT -> Range -> b
    , Record f a b -> TERM f -> b -> a -> b -> Range -> b
foldConditional :: TERM f -> b -> a -> b -> Range -> b
    , Record f a b -> TERM f -> PRED_SYMB -> b
foldMixfix_qual_pred :: TERM f -> PRED_SYMB -> b
    , Record f a b -> TERM f -> [b] -> b
foldMixfix_term :: TERM f -> [b] -> b
    , Record f a b -> TERM f -> VAR -> b
foldMixfix_token :: TERM f -> Token -> b
    , Record f a b -> TERM f -> SORT -> Range -> b
foldMixfix_sorted_term :: TERM f -> SORT -> Range -> b
    , Record f a b -> TERM f -> SORT -> Range -> b
foldMixfix_cast :: TERM f -> SORT -> Range -> b
    , Record f a b -> TERM f -> [b] -> Range -> b
foldMixfix_parenthesized :: TERM f -> [b] -> Range -> b
    , Record f a b -> TERM f -> [b] -> Range -> b
foldMixfix_bracketed :: TERM f -> [b] -> Range -> b
    , Record f a b -> TERM f -> [b] -> Range -> b
foldMixfix_braced :: TERM f -> [b] -> Range -> b
    , Record f a b -> TERM f -> f -> b
foldExtTERM :: TERM f -> f -> b
    }

mapRecord :: (f -> g) -> Record f (FORMULA g) (TERM g)
mapRecord :: (f -> g) -> Record f (FORMULA g) (TERM g)
mapRecord mf :: f -> g
mf = Record :: forall f a b.
(FORMULA f -> QUANTIFIER -> [VAR_DECL] -> a -> Range -> a)
-> (FORMULA f -> Junctor -> [a] -> Range -> a)
-> (FORMULA f -> a -> Relation -> a -> Range -> a)
-> (FORMULA f -> a -> Range -> a)
-> (FORMULA f -> Bool -> Range -> a)
-> (FORMULA f -> PRED_SYMB -> [b] -> Range -> a)
-> (FORMULA f -> b -> Range -> a)
-> (FORMULA f -> b -> Equality -> b -> Range -> a)
-> (FORMULA f -> b -> SORT -> Range -> a)
-> (FORMULA f -> b -> a)
-> (FORMULA f -> [Constraint] -> Bool -> a)
-> (FORMULA f -> SORT -> OP_TYPE -> a -> a)
-> (FORMULA f -> SORT -> PRED_TYPE -> a -> a)
-> (FORMULA f -> f -> a)
-> (TERM f -> VAR -> SORT -> Range -> b)
-> (TERM f -> OP_SYMB -> [b] -> Range -> b)
-> (TERM f -> b -> SORT -> Range -> b)
-> (TERM f -> b -> SORT -> Range -> b)
-> (TERM f -> b -> a -> b -> Range -> b)
-> (TERM f -> PRED_SYMB -> b)
-> (TERM f -> [b] -> b)
-> (TERM f -> VAR -> b)
-> (TERM f -> SORT -> Range -> b)
-> (TERM f -> SORT -> Range -> b)
-> (TERM f -> [b] -> Range -> b)
-> (TERM f -> [b] -> Range -> b)
-> (TERM f -> [b] -> Range -> b)
-> (TERM f -> f -> b)
-> Record f a b
Record
    { foldQuantification :: FORMULA f
-> QUANTIFIER -> [VAR_DECL] -> FORMULA g -> Range -> FORMULA g
foldQuantification = (QUANTIFIER -> [VAR_DECL] -> FORMULA g -> Range -> FORMULA g)
-> FORMULA f
-> QUANTIFIER
-> [VAR_DECL]
-> FORMULA g
-> Range
-> FORMULA g
forall a b. a -> b -> a
const QUANTIFIER -> [VAR_DECL] -> FORMULA g -> Range -> FORMULA g
forall f.
QUANTIFIER -> [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
Quantification
    , foldJunction :: FORMULA f -> Junctor -> [FORMULA g] -> Range -> FORMULA g
foldJunction = (Junctor -> [FORMULA g] -> Range -> FORMULA g)
-> FORMULA f -> Junctor -> [FORMULA g] -> Range -> FORMULA g
forall a b. a -> b -> a
const Junctor -> [FORMULA g] -> Range -> FORMULA g
forall f. Junctor -> [FORMULA f] -> Range -> FORMULA f
Junction
    , foldRelation :: FORMULA f
-> FORMULA g -> Relation -> FORMULA g -> Range -> FORMULA g
foldRelation = (FORMULA g -> Relation -> FORMULA g -> Range -> FORMULA g)
-> FORMULA f
-> FORMULA g
-> Relation
-> FORMULA g
-> Range
-> FORMULA g
forall a b. a -> b -> a
const FORMULA g -> Relation -> FORMULA g -> Range -> FORMULA g
forall f. FORMULA f -> Relation -> FORMULA f -> Range -> FORMULA f
Relation
    , foldNegation :: FORMULA f -> FORMULA g -> Range -> FORMULA g
foldNegation = (FORMULA g -> Range -> FORMULA g)
-> FORMULA f -> FORMULA g -> Range -> FORMULA g
forall a b. a -> b -> a
const FORMULA g -> Range -> FORMULA g
forall f. FORMULA f -> Range -> FORMULA f
Negation
    , foldAtom :: FORMULA f -> Bool -> Range -> FORMULA g
foldAtom = (Bool -> Range -> FORMULA g)
-> FORMULA f -> Bool -> Range -> FORMULA g
forall a b. a -> b -> a
const Bool -> Range -> FORMULA g
forall f. Bool -> Range -> FORMULA f
Atom
    , foldPredication :: FORMULA f -> PRED_SYMB -> [TERM g] -> Range -> FORMULA g
foldPredication = (PRED_SYMB -> [TERM g] -> Range -> FORMULA g)
-> FORMULA f -> PRED_SYMB -> [TERM g] -> Range -> FORMULA g
forall a b. a -> b -> a
const PRED_SYMB -> [TERM g] -> Range -> FORMULA g
forall f. PRED_SYMB -> [TERM f] -> Range -> FORMULA f
Predication
    , foldDefinedness :: FORMULA f -> TERM g -> Range -> FORMULA g
foldDefinedness = (TERM g -> Range -> FORMULA g)
-> FORMULA f -> TERM g -> Range -> FORMULA g
forall a b. a -> b -> a
const TERM g -> Range -> FORMULA g
forall f. TERM f -> Range -> FORMULA f
Definedness
    , foldEquation :: FORMULA f -> TERM g -> Equality -> TERM g -> Range -> FORMULA g
foldEquation = (TERM g -> Equality -> TERM g -> Range -> FORMULA g)
-> FORMULA f -> TERM g -> Equality -> TERM g -> Range -> FORMULA g
forall a b. a -> b -> a
const TERM g -> Equality -> TERM g -> Range -> FORMULA g
forall f. TERM f -> Equality -> TERM f -> Range -> FORMULA f
Equation
    , foldMembership :: FORMULA f -> TERM g -> SORT -> Range -> FORMULA g
foldMembership = (TERM g -> SORT -> Range -> FORMULA g)
-> FORMULA f -> TERM g -> SORT -> Range -> FORMULA g
forall a b. a -> b -> a
const TERM g -> SORT -> Range -> FORMULA g
forall f. TERM f -> SORT -> Range -> FORMULA f
Membership
    , foldMixfix_formula :: FORMULA f -> TERM g -> FORMULA g
foldMixfix_formula = (TERM g -> FORMULA g) -> FORMULA f -> TERM g -> FORMULA g
forall a b. a -> b -> a
const TERM g -> FORMULA g
forall f. TERM f -> FORMULA f
Mixfix_formula
    , foldSort_gen_ax :: FORMULA f -> [Constraint] -> Bool -> FORMULA g
foldSort_gen_ax = ([Constraint] -> Bool -> FORMULA g)
-> FORMULA f -> [Constraint] -> Bool -> FORMULA g
forall a b. a -> b -> a
const [Constraint] -> Bool -> FORMULA g
forall f. [Constraint] -> Bool -> FORMULA f
mkSort_gen_ax
    , foldQuantOp :: FORMULA f -> SORT -> OP_TYPE -> FORMULA g -> FORMULA g
foldQuantOp = (SORT -> OP_TYPE -> FORMULA g -> FORMULA g)
-> FORMULA f -> SORT -> OP_TYPE -> FORMULA g -> FORMULA g
forall a b. a -> b -> a
const SORT -> OP_TYPE -> FORMULA g -> FORMULA g
forall f. SORT -> OP_TYPE -> FORMULA f -> FORMULA f
QuantOp
    , foldQuantPred :: FORMULA f -> SORT -> PRED_TYPE -> FORMULA g -> FORMULA g
foldQuantPred = (SORT -> PRED_TYPE -> FORMULA g -> FORMULA g)
-> FORMULA f -> SORT -> PRED_TYPE -> FORMULA g -> FORMULA g
forall a b. a -> b -> a
const SORT -> PRED_TYPE -> FORMULA g -> FORMULA g
forall f. SORT -> PRED_TYPE -> FORMULA f -> FORMULA f
QuantPred
    , foldExtFORMULA :: FORMULA f -> f -> FORMULA g
foldExtFORMULA = \ _ -> g -> FORMULA g
forall f. f -> FORMULA f
ExtFORMULA (g -> FORMULA g) -> (f -> g) -> f -> FORMULA g
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f -> g
mf
    , foldQual_var :: TERM f -> VAR -> SORT -> Range -> TERM g
foldQual_var = (VAR -> SORT -> Range -> TERM g)
-> TERM f -> VAR -> SORT -> Range -> TERM g
forall a b. a -> b -> a
const VAR -> SORT -> Range -> TERM g
forall f. VAR -> SORT -> Range -> TERM f
Qual_var
    , foldApplication :: TERM f -> OP_SYMB -> [TERM g] -> Range -> TERM g
foldApplication = (OP_SYMB -> [TERM g] -> Range -> TERM g)
-> TERM f -> OP_SYMB -> [TERM g] -> Range -> TERM g
forall a b. a -> b -> a
const OP_SYMB -> [TERM g] -> Range -> TERM g
forall f. OP_SYMB -> [TERM f] -> Range -> TERM f
Application
    , foldSorted_term :: TERM f -> TERM g -> SORT -> Range -> TERM g
foldSorted_term = (TERM g -> SORT -> Range -> TERM g)
-> TERM f -> TERM g -> SORT -> Range -> TERM g
forall a b. a -> b -> a
const TERM g -> SORT -> Range -> TERM g
forall f. TERM f -> SORT -> Range -> TERM f
Sorted_term
    , foldCast :: TERM f -> TERM g -> SORT -> Range -> TERM g
foldCast = (TERM g -> SORT -> Range -> TERM g)
-> TERM f -> TERM g -> SORT -> Range -> TERM g
forall a b. a -> b -> a
const TERM g -> SORT -> Range -> TERM g
forall f. TERM f -> SORT -> Range -> TERM f
Cast
    , foldConditional :: TERM f -> TERM g -> FORMULA g -> TERM g -> Range -> TERM g
foldConditional = (TERM g -> FORMULA g -> TERM g -> Range -> TERM g)
-> TERM f -> TERM g -> FORMULA g -> TERM g -> Range -> TERM g
forall a b. a -> b -> a
const TERM g -> FORMULA g -> TERM g -> Range -> TERM g
forall f. TERM f -> FORMULA f -> TERM f -> Range -> TERM f
Conditional
    , foldMixfix_qual_pred :: TERM f -> PRED_SYMB -> TERM g
foldMixfix_qual_pred = (PRED_SYMB -> TERM g) -> TERM f -> PRED_SYMB -> TERM g
forall a b. a -> b -> a
const PRED_SYMB -> TERM g
forall f. PRED_SYMB -> TERM f
Mixfix_qual_pred
    , foldMixfix_term :: TERM f -> [TERM g] -> TERM g
foldMixfix_term = ([TERM g] -> TERM g) -> TERM f -> [TERM g] -> TERM g
forall a b. a -> b -> a
const [TERM g] -> TERM g
forall f. [TERM f] -> TERM f
Mixfix_term
    , foldMixfix_token :: TERM f -> VAR -> TERM g
foldMixfix_token = (VAR -> TERM g) -> TERM f -> VAR -> TERM g
forall a b. a -> b -> a
const VAR -> TERM g
forall f. VAR -> TERM f
Mixfix_token
    , foldMixfix_sorted_term :: TERM f -> SORT -> Range -> TERM g
foldMixfix_sorted_term = (SORT -> Range -> TERM g) -> TERM f -> SORT -> Range -> TERM g
forall a b. a -> b -> a
const SORT -> Range -> TERM g
forall f. SORT -> Range -> TERM f
Mixfix_sorted_term
    , foldMixfix_cast :: TERM f -> SORT -> Range -> TERM g
foldMixfix_cast = (SORT -> Range -> TERM g) -> TERM f -> SORT -> Range -> TERM g
forall a b. a -> b -> a
const SORT -> Range -> TERM g
forall f. SORT -> Range -> TERM f
Mixfix_cast
    , foldMixfix_parenthesized :: TERM f -> [TERM g] -> Range -> TERM g
foldMixfix_parenthesized = ([TERM g] -> Range -> TERM g)
-> TERM f -> [TERM g] -> Range -> TERM g
forall a b. a -> b -> a
const [TERM g] -> Range -> TERM g
forall f. [TERM f] -> Range -> TERM f
Mixfix_parenthesized
    , foldMixfix_bracketed :: TERM f -> [TERM g] -> Range -> TERM g
foldMixfix_bracketed = ([TERM g] -> Range -> TERM g)
-> TERM f -> [TERM g] -> Range -> TERM g
forall a b. a -> b -> a
const [TERM g] -> Range -> TERM g
forall f. [TERM f] -> Range -> TERM f
Mixfix_bracketed
    , foldMixfix_braced :: TERM f -> [TERM g] -> Range -> TERM g
foldMixfix_braced = ([TERM g] -> Range -> TERM g)
-> TERM f -> [TERM g] -> Range -> TERM g
forall a b. a -> b -> a
const [TERM g] -> Range -> TERM g
forall f. [TERM f] -> Range -> TERM f
Mixfix_braced
    , foldExtTERM :: TERM f -> f -> TERM g
foldExtTERM = \ _ -> g -> TERM g
forall f. f -> TERM f
ExtTERM (g -> TERM g) -> (f -> g) -> f -> TERM g
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f -> g
mf
    }

constRecord :: (f -> a) -> ([a] -> a) -> a -> Record f a a
constRecord :: (f -> a) -> ([a] -> a) -> a -> Record f a a
constRecord mf :: f -> a
mf join :: [a] -> a
join c :: a
c = Record :: forall f a b.
(FORMULA f -> QUANTIFIER -> [VAR_DECL] -> a -> Range -> a)
-> (FORMULA f -> Junctor -> [a] -> Range -> a)
-> (FORMULA f -> a -> Relation -> a -> Range -> a)
-> (FORMULA f -> a -> Range -> a)
-> (FORMULA f -> Bool -> Range -> a)
-> (FORMULA f -> PRED_SYMB -> [b] -> Range -> a)
-> (FORMULA f -> b -> Range -> a)
-> (FORMULA f -> b -> Equality -> b -> Range -> a)
-> (FORMULA f -> b -> SORT -> Range -> a)
-> (FORMULA f -> b -> a)
-> (FORMULA f -> [Constraint] -> Bool -> a)
-> (FORMULA f -> SORT -> OP_TYPE -> a -> a)
-> (FORMULA f -> SORT -> PRED_TYPE -> a -> a)
-> (FORMULA f -> f -> a)
-> (TERM f -> VAR -> SORT -> Range -> b)
-> (TERM f -> OP_SYMB -> [b] -> Range -> b)
-> (TERM f -> b -> SORT -> Range -> b)
-> (TERM f -> b -> SORT -> Range -> b)
-> (TERM f -> b -> a -> b -> Range -> b)
-> (TERM f -> PRED_SYMB -> b)
-> (TERM f -> [b] -> b)
-> (TERM f -> VAR -> b)
-> (TERM f -> SORT -> Range -> b)
-> (TERM f -> SORT -> Range -> b)
-> (TERM f -> [b] -> Range -> b)
-> (TERM f -> [b] -> Range -> b)
-> (TERM f -> [b] -> Range -> b)
-> (TERM f -> f -> b)
-> Record f a b
Record
    { foldQuantification :: FORMULA f -> QUANTIFIER -> [VAR_DECL] -> a -> Range -> a
foldQuantification = \ _ _ _ r :: a
r _ -> a
r
    , foldJunction :: FORMULA f -> Junctor -> [a] -> Range -> a
foldJunction = \ _ _ l :: [a]
l _ -> [a] -> a
join [a]
l
    , foldRelation :: FORMULA f -> a -> Relation -> a -> Range -> a
foldRelation = \ _ l :: a
l _ r :: a
r _ -> [a] -> a
join [a
l, a
r]
    , foldNegation :: FORMULA f -> a -> Range -> a
foldNegation = \ _ r :: a
r _ -> a
r
    , foldAtom :: FORMULA f -> Bool -> Range -> a
foldAtom = \ _ _ _ -> a
c
    , foldPredication :: FORMULA f -> PRED_SYMB -> [a] -> Range -> a
foldPredication = \ _ _ l :: [a]
l _ -> [a] -> a
join [a]
l
    , foldDefinedness :: FORMULA f -> a -> Range -> a
foldDefinedness = \ _ r :: a
r _ -> a
r
    , foldEquation :: FORMULA f -> a -> Equality -> a -> Range -> a
foldEquation = \ _ l :: a
l _ r :: a
r _ -> [a] -> a
join [a
l, a
r]
    , foldMembership :: FORMULA f -> a -> SORT -> Range -> a
foldMembership = \ _ r :: a
r _ _ -> a
r
    , foldMixfix_formula :: FORMULA f -> a -> a
foldMixfix_formula = \ _ r :: a
r -> a
r
    , foldSort_gen_ax :: FORMULA f -> [Constraint] -> Bool -> a
foldSort_gen_ax = \ _ _ _ -> a
c
    , foldQuantOp :: FORMULA f -> SORT -> OP_TYPE -> a -> a
foldQuantOp = \ _ _ _ a :: a
a -> a
a
    , foldQuantPred :: FORMULA f -> SORT -> PRED_TYPE -> a -> a
foldQuantPred = \ _ _ _ a :: a
a -> a
a
    , foldExtFORMULA :: FORMULA f -> f -> a
foldExtFORMULA = (f -> a) -> FORMULA f -> f -> a
forall a b. a -> b -> a
const f -> a
mf
    , foldQual_var :: TERM f -> VAR -> SORT -> Range -> a
foldQual_var = \ _ _ _ _ -> a
c
    , foldApplication :: TERM f -> OP_SYMB -> [a] -> Range -> a
foldApplication = \ _ _ l :: [a]
l _ -> [a] -> a
join [a]
l
    , foldSorted_term :: TERM f -> a -> SORT -> Range -> a
foldSorted_term = \ _ r :: a
r _ _ -> a
r
    , foldCast :: TERM f -> a -> SORT -> Range -> a
foldCast = \ _ r :: a
r _ _ -> a
r
    , foldConditional :: TERM f -> a -> a -> a -> Range -> a
foldConditional = \ _ l :: a
l f :: a
f r :: a
r _ -> [a] -> a
join [a
l, a
f, a
r]
    , foldMixfix_qual_pred :: TERM f -> PRED_SYMB -> a
foldMixfix_qual_pred = \ _ _ -> a
c
    , foldMixfix_term :: TERM f -> [a] -> a
foldMixfix_term = ([a] -> a) -> TERM f -> [a] -> a
forall a b. a -> b -> a
const [a] -> a
join
    , foldMixfix_token :: TERM f -> VAR -> a
foldMixfix_token = \ _ _ -> a
c
    , foldMixfix_sorted_term :: TERM f -> SORT -> Range -> a
foldMixfix_sorted_term = \ _ _ _ -> a
c
    , foldMixfix_cast :: TERM f -> SORT -> Range -> a
foldMixfix_cast = \ _ _ _ -> a
c
    , foldMixfix_parenthesized :: TERM f -> [a] -> Range -> a
foldMixfix_parenthesized = \ _ l :: [a]
l _ -> [a] -> a
join [a]
l
    , foldMixfix_bracketed :: TERM f -> [a] -> Range -> a
foldMixfix_bracketed = \ _ l :: [a]
l _ -> [a] -> a
join [a]
l
    , foldMixfix_braced :: TERM f -> [a] -> Range -> a
foldMixfix_braced = \ _ l :: [a]
l _ -> [a] -> a
join [a]
l
    , foldExtTERM :: TERM f -> f -> a
foldExtTERM = (f -> a) -> TERM f -> f -> a
forall a b. a -> b -> a
const f -> a
mf
    }

foldFormula :: Record f a b -> FORMULA f -> a
foldFormula :: Record f a b -> FORMULA f -> a
foldFormula r :: Record f a b
r f :: FORMULA f
f = case FORMULA f
f of
   Quantification q :: QUANTIFIER
q vs :: [VAR_DECL]
vs e :: FORMULA f
e ps :: Range
ps -> Record f a b
-> FORMULA f -> QUANTIFIER -> [VAR_DECL] -> a -> Range -> a
forall f a b.
Record f a b
-> FORMULA f -> QUANTIFIER -> [VAR_DECL] -> a -> Range -> a
foldQuantification Record f a b
r FORMULA f
f QUANTIFIER
q [VAR_DECL]
vs (Record f a b -> FORMULA f -> a
forall f a b. Record f a b -> FORMULA f -> a
foldFormula Record f a b
r FORMULA f
e) Range
ps
   Junction j :: Junctor
j fs :: [FORMULA f]
fs ps :: Range
ps -> Record f a b -> FORMULA f -> Junctor -> [a] -> Range -> a
forall f a b.
Record f a b -> FORMULA f -> Junctor -> [a] -> Range -> a
foldJunction Record f a b
r FORMULA f
f Junctor
j ((FORMULA f -> a) -> [FORMULA f] -> [a]
forall a b. (a -> b) -> [a] -> [b]
map (Record f a b -> FORMULA f -> a
forall f a b. Record f a b -> FORMULA f -> a
foldFormula Record f a b
r) [FORMULA f]
fs) Range
ps
   Relation f1 :: FORMULA f
f1 c :: Relation
c f2 :: FORMULA f
f2 ps :: Range
ps -> Record f a b -> FORMULA f -> a -> Relation -> a -> Range -> a
forall f a b.
Record f a b -> FORMULA f -> a -> Relation -> a -> Range -> a
foldRelation Record f a b
r FORMULA f
f (Record f a b -> FORMULA f -> a
forall f a b. Record f a b -> FORMULA f -> a
foldFormula Record f a b
r FORMULA f
f1) Relation
c
      (Record f a b -> FORMULA f -> a
forall f a b. Record f a b -> FORMULA f -> a
foldFormula Record f a b
r FORMULA f
f2) Range
ps
   Negation e :: FORMULA f
e ps :: Range
ps -> Record f a b -> FORMULA f -> a -> Range -> a
forall f a b. Record f a b -> FORMULA f -> a -> Range -> a
foldNegation Record f a b
r FORMULA f
f (Record f a b -> FORMULA f -> a
forall f a b. Record f a b -> FORMULA f -> a
foldFormula Record f a b
r FORMULA f
e) Range
ps
   Atom b :: Bool
b ps :: Range
ps -> Record f a b -> FORMULA f -> Bool -> Range -> a
forall f a b. Record f a b -> FORMULA f -> Bool -> Range -> a
foldAtom Record f a b
r FORMULA f
f Bool
b Range
ps
   Predication p :: PRED_SYMB
p ts :: [TERM f]
ts ps :: Range
ps -> Record f a b -> FORMULA f -> PRED_SYMB -> [b] -> Range -> a
forall f a b.
Record f a b -> FORMULA f -> PRED_SYMB -> [b] -> Range -> a
foldPredication Record f a b
r FORMULA f
f PRED_SYMB
p ((TERM f -> b) -> [TERM f] -> [b]
forall a b. (a -> b) -> [a] -> [b]
map (Record f a b -> TERM f -> b
forall f a b. Record f a b -> TERM f -> b
foldTerm Record f a b
r) [TERM f]
ts) Range
ps
   Definedness t :: TERM f
t ps :: Range
ps -> Record f a b -> FORMULA f -> b -> Range -> a
forall f a b. Record f a b -> FORMULA f -> b -> Range -> a
foldDefinedness Record f a b
r FORMULA f
f (Record f a b -> TERM f -> b
forall f a b. Record f a b -> TERM f -> b
foldTerm Record f a b
r TERM f
t) Range
ps
   Equation t1 :: TERM f
t1 e :: Equality
e t2 :: TERM f
t2 ps :: Range
ps -> Record f a b -> FORMULA f -> b -> Equality -> b -> Range -> a
forall f a b.
Record f a b -> FORMULA f -> b -> Equality -> b -> Range -> a
foldEquation Record f a b
r FORMULA f
f (Record f a b -> TERM f -> b
forall f a b. Record f a b -> TERM f -> b
foldTerm Record f a b
r TERM f
t1) Equality
e
      (Record f a b -> TERM f -> b
forall f a b. Record f a b -> TERM f -> b
foldTerm Record f a b
r TERM f
t2) Range
ps
   Membership t :: TERM f
t s :: SORT
s ps :: Range
ps -> Record f a b -> FORMULA f -> b -> SORT -> Range -> a
forall f a b. Record f a b -> FORMULA f -> b -> SORT -> Range -> a
foldMembership Record f a b
r FORMULA f
f (Record f a b -> TERM f -> b
forall f a b. Record f a b -> TERM f -> b
foldTerm Record f a b
r TERM f
t) SORT
s Range
ps
   Mixfix_formula t :: TERM f
t -> Record f a b -> FORMULA f -> b -> a
forall f a b. Record f a b -> FORMULA f -> b -> a
foldMixfix_formula Record f a b
r FORMULA f
f (Record f a b -> TERM f -> b
forall f a b. Record f a b -> TERM f -> b
foldTerm Record f a b
r TERM f
t)
   Unparsed_formula s :: String
s _ -> String -> a
forall a. HasCallStack => String -> a
error (String -> a) -> String -> a
forall a b. (a -> b) -> a -> b
$ "Fold.foldFormula.Unparsed" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s
   Sort_gen_ax cs :: [Constraint]
cs b :: Bool
b -> Record f a b -> FORMULA f -> [Constraint] -> Bool -> a
forall f a b.
Record f a b -> FORMULA f -> [Constraint] -> Bool -> a
foldSort_gen_ax Record f a b
r FORMULA f
f [Constraint]
cs Bool
b
   QuantOp o :: SORT
o t :: OP_TYPE
t q :: FORMULA f
q -> Record f a b -> FORMULA f -> SORT -> OP_TYPE -> a -> a
forall f a b.
Record f a b -> FORMULA f -> SORT -> OP_TYPE -> a -> a
foldQuantOp Record f a b
r FORMULA f
f SORT
o OP_TYPE
t (a -> a) -> a -> a
forall a b. (a -> b) -> a -> b
$ Record f a b -> FORMULA f -> a
forall f a b. Record f a b -> FORMULA f -> a
foldFormula Record f a b
r FORMULA f
q
   QuantPred p :: SORT
p t :: PRED_TYPE
t q :: FORMULA f
q -> Record f a b -> FORMULA f -> SORT -> PRED_TYPE -> a -> a
forall f a b.
Record f a b -> FORMULA f -> SORT -> PRED_TYPE -> a -> a
foldQuantPred Record f a b
r FORMULA f
f SORT
p PRED_TYPE
t (a -> a) -> a -> a
forall a b. (a -> b) -> a -> b
$ Record f a b -> FORMULA f -> a
forall f a b. Record f a b -> FORMULA f -> a
foldFormula Record f a b
r FORMULA f
q
   ExtFORMULA e :: f
e -> Record f a b -> FORMULA f -> f -> a
forall f a b. Record f a b -> FORMULA f -> f -> a
foldExtFORMULA Record f a b
r FORMULA f
f f
e

foldTerm :: Record f a b -> TERM f -> b
foldTerm :: Record f a b -> TERM f -> b
foldTerm r :: Record f a b
r = (FORMULA f -> a) -> Record f a b -> TERM f -> b
forall f a b. (FORMULA f -> a) -> Record f a b -> TERM f -> b
foldOnlyTerm (Record f a b -> FORMULA f -> a
forall f a b. Record f a b -> FORMULA f -> a
foldFormula Record f a b
r) Record f a b
r

foldOnlyTerm :: (FORMULA f -> a) -> Record f a b -> TERM f -> b
foldOnlyTerm :: (FORMULA f -> a) -> Record f a b -> TERM f -> b
foldOnlyTerm ff :: FORMULA f -> a
ff r :: Record f a b
r t :: TERM f
t = case TERM f
t of
   Qual_var v :: VAR
v s :: SORT
s ps :: Range
ps -> Record f a b -> TERM f -> VAR -> SORT -> Range -> b
forall f a b. Record f a b -> TERM f -> VAR -> SORT -> Range -> b
foldQual_var Record f a b
r TERM f
t VAR
v SORT
s Range
ps
   Application o :: OP_SYMB
o ts :: [TERM f]
ts ps :: Range
ps -> Record f a b -> TERM f -> OP_SYMB -> [b] -> Range -> b
forall f a b.
Record f a b -> TERM f -> OP_SYMB -> [b] -> Range -> b
foldApplication Record f a b
r TERM f
t OP_SYMB
o ((TERM f -> b) -> [TERM f] -> [b]
forall a b. (a -> b) -> [a] -> [b]
map ((FORMULA f -> a) -> Record f a b -> TERM f -> b
forall f a b. (FORMULA f -> a) -> Record f a b -> TERM f -> b
foldOnlyTerm FORMULA f -> a
ff Record f a b
r) [TERM f]
ts) Range
ps
   Sorted_term st :: TERM f
st s :: SORT
s ps :: Range
ps -> Record f a b -> TERM f -> b -> SORT -> Range -> b
forall f a b. Record f a b -> TERM f -> b -> SORT -> Range -> b
foldSorted_term Record f a b
r TERM f
t ((FORMULA f -> a) -> Record f a b -> TERM f -> b
forall f a b. (FORMULA f -> a) -> Record f a b -> TERM f -> b
foldOnlyTerm FORMULA f -> a
ff Record f a b
r TERM f
st) SORT
s Range
ps
   Cast ct :: TERM f
ct s :: SORT
s ps :: Range
ps -> Record f a b -> TERM f -> b -> SORT -> Range -> b
forall f a b. Record f a b -> TERM f -> b -> SORT -> Range -> b
foldCast Record f a b
r TERM f
t ((FORMULA f -> a) -> Record f a b -> TERM f -> b
forall f a b. (FORMULA f -> a) -> Record f a b -> TERM f -> b
foldOnlyTerm FORMULA f -> a
ff Record f a b
r TERM f
ct) SORT
s Range
ps
   Conditional t1 :: TERM f
t1 f :: FORMULA f
f t2 :: TERM f
t2 ps :: Range
ps -> Record f a b -> TERM f -> b -> a -> b -> Range -> b
forall f a b. Record f a b -> TERM f -> b -> a -> b -> Range -> b
foldConditional Record f a b
r TERM f
t ((FORMULA f -> a) -> Record f a b -> TERM f -> b
forall f a b. (FORMULA f -> a) -> Record f a b -> TERM f -> b
foldOnlyTerm FORMULA f -> a
ff Record f a b
r TERM f
t1)
      (FORMULA f -> a
ff FORMULA f
f) ((FORMULA f -> a) -> Record f a b -> TERM f -> b
forall f a b. (FORMULA f -> a) -> Record f a b -> TERM f -> b
foldOnlyTerm FORMULA f -> a
ff Record f a b
r TERM f
t2) Range
ps
   Unparsed_term s :: String
s _ -> String -> b
forall a. HasCallStack => String -> a
error (String -> b) -> String -> b
forall a b. (a -> b) -> a -> b
$ "Fold.Unparsed_term" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s
   Mixfix_qual_pred p :: PRED_SYMB
p -> Record f a b -> TERM f -> PRED_SYMB -> b
forall f a b. Record f a b -> TERM f -> PRED_SYMB -> b
foldMixfix_qual_pred Record f a b
r TERM f
t PRED_SYMB
p
   Mixfix_term ts :: [TERM f]
ts -> Record f a b -> TERM f -> [b] -> b
forall f a b. Record f a b -> TERM f -> [b] -> b
foldMixfix_term Record f a b
r TERM f
t ((TERM f -> b) -> [TERM f] -> [b]
forall a b. (a -> b) -> [a] -> [b]
map ((FORMULA f -> a) -> Record f a b -> TERM f -> b
forall f a b. (FORMULA f -> a) -> Record f a b -> TERM f -> b
foldOnlyTerm FORMULA f -> a
ff Record f a b
r) [TERM f]
ts)
   Mixfix_token s :: VAR
s -> Record f a b -> TERM f -> VAR -> b
forall f a b. Record f a b -> TERM f -> VAR -> b
foldMixfix_token Record f a b
r TERM f
t VAR
s
   Mixfix_sorted_term s :: SORT
s ps :: Range
ps -> Record f a b -> TERM f -> SORT -> Range -> b
forall f a b. Record f a b -> TERM f -> SORT -> Range -> b
foldMixfix_sorted_term Record f a b
r TERM f
t SORT
s Range
ps
   Mixfix_cast s :: SORT
s ps :: Range
ps -> Record f a b -> TERM f -> SORT -> Range -> b
forall f a b. Record f a b -> TERM f -> SORT -> Range -> b
foldMixfix_cast Record f a b
r TERM f
t SORT
s Range
ps
   Mixfix_parenthesized ts :: [TERM f]
ts ps :: Range
ps -> Record f a b -> TERM f -> [b] -> Range -> b
forall f a b. Record f a b -> TERM f -> [b] -> Range -> b
foldMixfix_parenthesized Record f a b
r TERM f
t
      ((TERM f -> b) -> [TERM f] -> [b]
forall a b. (a -> b) -> [a] -> [b]
map ((FORMULA f -> a) -> Record f a b -> TERM f -> b
forall f a b. (FORMULA f -> a) -> Record f a b -> TERM f -> b
foldOnlyTerm FORMULA f -> a
ff Record f a b
r) [TERM f]
ts) Range
ps
   Mixfix_bracketed ts :: [TERM f]
ts ps :: Range
ps -> Record f a b -> TERM f -> [b] -> Range -> b
forall f a b. Record f a b -> TERM f -> [b] -> Range -> b
foldMixfix_bracketed Record f a b
r TERM f
t
      ((TERM f -> b) -> [TERM f] -> [b]
forall a b. (a -> b) -> [a] -> [b]
map ((FORMULA f -> a) -> Record f a b -> TERM f -> b
forall f a b. (FORMULA f -> a) -> Record f a b -> TERM f -> b
foldOnlyTerm FORMULA f -> a
ff Record f a b
r) [TERM f]
ts) Range
ps
   Mixfix_braced ts :: [TERM f]
ts ps :: Range
ps -> Record f a b -> TERM f -> [b] -> Range -> b
forall f a b. Record f a b -> TERM f -> [b] -> Range -> b
foldMixfix_braced Record f a b
r TERM f
t
      ((TERM f -> b) -> [TERM f] -> [b]
forall a b. (a -> b) -> [a] -> [b]
map ((FORMULA f -> a) -> Record f a b -> TERM f -> b
forall f a b. (FORMULA f -> a) -> Record f a b -> TERM f -> b
foldOnlyTerm FORMULA f -> a
ff Record f a b
r) [TERM f]
ts) Range
ps
   ExtTERM e :: f
e -> Record f a b -> TERM f -> f -> b
forall f a b. Record f a b -> TERM f -> f -> b
foldExtTERM Record f a b
r TERM f
t f
e