module CASL.ShowMixfix where
import CASL.AS_Basic_CASL
import CASL.Fold
import Common.Id
mkMixfixRecord :: (f -> f) -> Record f (FORMULA f) (TERM f)
mkMixfixRecord :: (f -> f) -> Record f (FORMULA f) (TERM f)
mkMixfixRecord mf :: f -> f
mf = ((f -> f) -> Record f (FORMULA f) (TERM f)
forall f g. (f -> g) -> Record f (FORMULA g) (TERM g)
mapRecord f -> f
mf)
{ foldApplication :: TERM f -> OP_SYMB -> [TERM f] -> Range -> TERM f
foldApplication = \ _ o :: OP_SYMB
o ts :: [TERM f]
ts ps :: Range
ps ->
if [TERM f] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TERM f]
ts then OP_SYMB -> [TERM f] -> Range -> TERM f
forall f. OP_SYMB -> [TERM f] -> Range -> TERM f
Application OP_SYMB
o [TERM f]
ts Range
ps else
[TERM f] -> TERM f
forall f. [TERM f] -> TERM f
Mixfix_term [OP_SYMB -> [TERM f] -> Range -> TERM f
forall f. OP_SYMB -> [TERM f] -> Range -> TERM f
Application OP_SYMB
o [] Range
nullRange, [TERM f] -> Range -> TERM f
forall f. [TERM f] -> Range -> TERM f
Mixfix_parenthesized [TERM f]
ts Range
ps]
, foldPredication :: FORMULA f -> PRED_SYMB -> [TERM f] -> Range -> FORMULA f
foldPredication = \ _ p :: PRED_SYMB
p ts :: [TERM f]
ts ps :: Range
ps ->
if [TERM f] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TERM f]
ts then PRED_SYMB -> [TERM f] -> Range -> FORMULA f
forall f. PRED_SYMB -> [TERM f] -> Range -> FORMULA f
Predication PRED_SYMB
p [TERM f]
ts Range
ps else TERM f -> FORMULA f
forall f. TERM f -> FORMULA f
Mixfix_formula (TERM f -> FORMULA f) -> TERM f -> FORMULA f
forall a b. (a -> b) -> a -> b
$
[TERM f] -> TERM f
forall f. [TERM f] -> TERM f
Mixfix_term [PRED_SYMB -> TERM f
forall f. PRED_SYMB -> TERM f
Mixfix_qual_pred PRED_SYMB
p, [TERM f] -> Range -> TERM f
forall f. [TERM f] -> Range -> TERM f
Mixfix_parenthesized [TERM f]
ts Range
ps]
}
mapTerm :: (f -> f) -> TERM f -> TERM f
mapTerm :: (f -> f) -> TERM f -> TERM f
mapTerm = Record f (FORMULA f) (TERM f) -> TERM f -> TERM f
forall f a b. Record f a b -> TERM f -> b
foldTerm (Record f (FORMULA f) (TERM f) -> TERM f -> TERM f)
-> ((f -> f) -> Record f (FORMULA f) (TERM f))
-> (f -> f)
-> TERM f
-> TERM f
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (f -> f) -> Record f (FORMULA f) (TERM f)
forall f. (f -> f) -> Record f (FORMULA f) (TERM f)
mkMixfixRecord
mapFormula :: (f -> f) -> FORMULA f -> FORMULA f
mapFormula :: (f -> f) -> FORMULA f -> FORMULA f
mapFormula = Record f (FORMULA f) (TERM f) -> FORMULA f -> FORMULA f
forall f a b. Record f a b -> FORMULA f -> a
foldFormula (Record f (FORMULA f) (TERM f) -> FORMULA f -> FORMULA f)
-> ((f -> f) -> Record f (FORMULA f) (TERM f))
-> (f -> f)
-> FORMULA f
-> FORMULA f
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (f -> f) -> Record f (FORMULA f) (TERM f)
forall f. (f -> f) -> Record f (FORMULA f) (TERM f)
mkMixfixRecord