@@ -314,23 +314,23 @@ replaceRepeatedly
314
314
replaceRepeatedly [] t = t
315
315
replaceRepeatedly ((s,t): r) e = replaceRepeatedly r $ replace' s t e
316
316
317
- -- | Takes in a theory and a translation function and repeatedly (to fixpoint) attempts to simplfiy (extend) it.
318
- simplifyFix
317
+ -- | Takes in a theory and a translation function and repeatedly (to fixpoint) attempts to simplify (extend) it.
318
+ simplifyTheory
319
319
:: (MultiTyMap '[Ord ] '[var , ty , sym , en , fk , att , gen , sk ])
320
320
=> Set (Ctx var (ty + en ), EQ var ty sym en fk att gen sk )
321
321
-> [(Head ty sym en fk att gen sk , Term var ty sym en fk att gen sk )]
322
322
-> (Set (Ctx var (ty + en ), EQ var ty sym en fk att gen sk ), [(Head ty sym en fk att gen sk , Term var ty sym en fk att gen sk )])
323
- simplifyFix eqs subst0 = case simplify eqs of
323
+ simplifyTheory eqs subst0 = case simplifyTheoryStep eqs of
324
324
Nothing -> (eqs, subst0)
325
- Just (eqs1, subst1) -> simplifyFix eqs1 $ subst0 ++ [subst1]
325
+ Just (eqs1, subst1) -> simplifyTheory eqs1 $ subst0 ++ [subst1]
326
326
327
327
-- | Does a one step simplifcation of a theory, looking for equations @gen/sk = term@, yielding also a
328
328
-- translation function from the old theory to the new, encoded as a list of (symbol, term) pairs.
329
- simplify
329
+ simplifyTheoryStep
330
330
:: (MultiTyMap '[Ord ] '[var , ty , sym , en , fk , att , gen , sk ])
331
331
=> Set (Ctx var (ty + en ), EQ var ty sym en fk att gen sk )
332
332
-> Maybe (Set (Ctx var (ty + en ), EQ var ty sym en fk att gen sk ), (Head ty sym en fk att gen sk , Term var ty sym en fk att gen sk ))
333
- simplify eqs = case findSimplifiable eqs of
333
+ simplifyTheoryStep eqs = case findSimplifiable eqs of
334
334
Nothing -> Nothing
335
335
Just (toRemove, replacer) -> let
336
336
eqs2 = Set. map (\ (ctx, EQ (lhs, rhs)) -> (ctx, EQ (replace' toRemove replacer lhs, replace' toRemove replacer rhs))) eqs
0 commit comments