@@ -1302,11 +1302,25 @@ substTerm :: Eq n => TT n {-^ Old term -} ->
1302 TT n {-^ template term -}
1302 TT n {-^ template term -}
1304substTerm old new = st where
1304substTerm old new = st where
1305− st t | t == old = new
1305+ st t | eqAlpha [] t old = new
1306 st (App s f a) = App s (st f) (st a)
1306 st (App s f a) = App s (st f) (st a)
1307 st (Bind x b sc) = Bind x (fmap st b) (st sc)
1307 st (Bind x b sc) = Bind x (fmap st b) (st sc)
1308 st t = t
1308 st t = t
1310+ eqAlpha as (P _ x _) (P _ y _)
1311+ = x == y || (x, y) `elem` as || (y, x) `elem` as
1312+ eqAlpha as (V x) (V y) = x == y
1313+ eqAlpha as (Bind x xb xs) (Bind y yb ys)
1314+ = eqAlphaB as xb yb && eqAlpha ((x, y) : as) xs ys
1315+ eqAlpha as (App _ fx ax) (App _ fy ay) = eqAlpha as fx fy && eqAlpha as ax ay
1316+ eqAlpha as x y = x == y
1318+ eqAlphaB as (Let xt xv) (Let yt yv)
1319+ = eqAlpha as xt yt && eqAlpha as xv yv
1320+ eqAlphaB as (Guess xt xv) (Guess yt yv)
1321+ = eqAlpha as xt yt && eqAlpha as xv yv
1322+ eqAlphaB as bx by = eqAlpha as (binderTy bx) (binderTy by)
1310-- | Return number of occurrences of V 0 or bound name i the term
1324-- | Return number of occurrences of V 0 or bound name i the term
1311occurrences :: Eq n => n -> TT n -> Int
1325occurrences :: Eq n => n -> TT n -> Int
1312occurrences n t = execState (no' 0 t) 0
1326occurrences n t = execState (no' 0 t) 0