Skip to content
Browse files

Switch evaluator for evalCtxt

  • Loading branch information...
1 parent 5b4553c commit 0a21a34fb95a1a7c20e6f9a537aa2ee0f87ab8ac Edwin Brady committed Sep 15, 2010
Showing with 4 additions and 2 deletions.
  1. +2 −1 Ivor/PatternDefs.lhs
  2. +2 −1 Ivor/TT.lhs
View
3 Ivor/PatternDefs.lhs
@@ -351,7 +351,8 @@ fails, reporting which case isn't matched, if patterns don't cover.
> matches' (P x) (P y) | x == y = return [(y, P x)]
> matches' t (P n) = return [(n,t)]
> matches' (P nm@(MN ("INFER",_))) t = return []
-> matches' x y = if x == y then return [] else fail "With pattern does not match parent"
+> matches' (Bind _ _ _) (Bind _ _ _) = return []
+> matches' x y = if x == y then return [] else fail $ "With pattern does not match parent"
> expandClause :: Gamma Name -> RawScheme -> IvorM [RawScheme]
View
3 Ivor/TT.lhs
@@ -95,6 +95,7 @@
> import Ivor.Scopecheck
> import Ivor.Gadgets
> import Ivor.Nobby
+> import Ivor.Evaluator
> import Ivor.SC
> import Ivor.Bytecode
> import Ivor.Datatype
@@ -763,7 +764,7 @@ Give a parseable but ugly representation of a term.
> DefaultGoal -> head (holequeue st)
> case (Tactics.findhole (defs st) (Just h) prf holeenv) of
> (Just env) -> do (tm, ty) <- tt $ Ivor.Typecheck.check (defs st) env rawtm Nothing
-> let tnorm = normaliseEnv env (defs st) tm
+> let tnorm = eval_nf_env env (defs st) tm
> return $ Term (tnorm, ty)
> Nothing -> fail "No such goal"
> where holeenv :: Gamma Name -> Env Name -> Indexed Name -> Env Name

0 comments on commit 0a21a34

Please sign in to comment.
Something went wrong with that request. Please try again.