From b6341a452599bb6f151902742ad027912090e2b8 Mon Sep 17 00:00:00 2001 From: eb Date: Wed, 2 Aug 2006 12:13:32 +0100 Subject: [PATCH] No need to look for holes inside let bound values ...since we don't put holes there. This results in quite a gain in efficiency. darcs-hash:20060802111332-974a0-003257f86c08488bc8018c790534ea4623d4cd05.gz --- Ivor/Tactics.lhs | 6 ++++-- ivor.cabal | 2 +- 2 files changed, 5 insertions(+), 3 deletions(-) diff --git a/Ivor/Tactics.lhs b/Ivor/Tactics.lhs index 2b35dc3..44e4ae0 100644 --- a/Ivor/Tactics.lhs +++ b/Ivor/Tactics.lhs @@ -126,6 +126,7 @@ FIXME: Why not use a state monad for the unified variables in rt? > rt env b@(Bind x (B (Let v) ty) _) > | x == n = do (Ind b',u) <- tactic gam env (Ind b) > return (b',u) +> -- | otherwise = return (b, []) -- fail "No such hole" > rt env b@(Bind x (B Lambda ty) _) > | x == n = do (Ind b',u) <- tactic gam env (Ind b) > return (b',u) @@ -148,8 +149,9 @@ FIXME: Why not use a state monad for the unified variables in rt? > return (Stage (Escape t'), u) > rt env x = return (x, []) > -> rtb env (Let x) = do (rtx, u) <- rt env x -> return (Let rtx, u) +> -- No holes in let bound values! +> --rtb env (Let x) = do (rtx, u) <- rt env x +> -- return (Let rtx, u) > rtb env (Guess x) = do (rtx, u) <- rt env x > return (Guess rtx, u) > rtb env b = return (b, []) diff --git a/ivor.cabal b/ivor.cabal index 379337b..4170147 100644 --- a/ivor.cabal +++ b/ivor.cabal @@ -6,7 +6,7 @@ License-file: LICENSE Maintainer: eb@dcs.st-and.ac.uk Homepage: http://www.dcs.st-and.ac.uk/~eb/Ivor/ Stability: experimental -Build-depends: base, haskell98, util, parsec, mtl, Cabal +Build-depends: base, haskell98, util, parsec, mtl Extensions: MultiParamTypeClasses, FunctionalDependencies, ExistentialQuantification, OverlappingInstances ghc-prof-options: -auto-all