@@ -290,13 +290,13 @@ findSimplifiableEqs = procEqs . Set.toList
290
290
Just y -> Just y
291
291
292
292
-- | Replaces a symbol by a term in a term.
293
- replace'
293
+ replace
294
294
:: (Eq ty , Eq sym , Eq en , Eq fk , Eq att , Eq gen , Eq sk )
295
295
=> Head ty sym en fk att gen sk
296
296
-> Term var ty sym en fk att gen sk
297
297
-> Term var ty sym en fk att gen sk
298
298
-> Term var ty sym en fk att gen sk
299
- replace' toReplace replacer x = case x of
299
+ replace toReplace replacer x = case x of
300
300
Sk s -> if HSk s == toReplace then replacer else Sk s
301
301
Gen s -> if HGen s == toReplace then replacer else Gen s
302
302
Sym f [] -> if HSym f == toReplace then replacer else Sym f []
@@ -305,15 +305,15 @@ replace' toReplace replacer x = case x of
305
305
Att f a -> Att f $ self a
306
306
Var v -> Var v
307
307
where
308
- self = replace' toReplace replacer
308
+ self = replace toReplace replacer
309
309
310
310
replaceRepeatedly
311
311
:: (Eq ty , Eq sym , Eq en , Eq fk , Eq att , Eq gen , Eq sk )
312
312
=> [(Head ty sym en fk att gen sk , Term var ty sym en fk att gen sk )]
313
313
-> Term var ty sym en fk att gen sk
314
314
-> Term var ty sym en fk att gen sk
315
315
replaceRepeatedly [] t = t
316
- replaceRepeatedly ((s,t): r) e = replaceRepeatedly r $ replace' s t e
316
+ replaceRepeatedly ((s,t): r) e = replaceRepeatedly r $ replace s t e
317
317
318
318
-- | Takes in a theory and a translation function and repeatedly (to fixpoint) attempts to simplify (extend) it.
319
319
simplifyTheory
@@ -334,7 +334,7 @@ simplifyTheoryStep
334
334
simplifyTheoryStep eqs = case findSimplifiableEqs eqs of
335
335
Nothing -> Nothing
336
336
Just (toRemove, replacer) -> let
337
- eqs2 = Set. map (\ (ctx, EQ (lhs, rhs)) -> (ctx, EQ (replace' toRemove replacer lhs, replace' toRemove replacer rhs))) eqs
337
+ eqs2 = Set. map (\ (ctx, EQ (lhs, rhs)) -> (ctx, EQ (replace toRemove replacer lhs, replace toRemove replacer rhs))) eqs
338
338
eqs3 = Set. filter (\ (_ , EQ (x, y )) -> not $ x == y) eqs2
339
339
in Just (eqs3, (toRemove, replacer))
340
340
0 commit comments