Permalink
Browse files

Better match checking

  • Loading branch information...
1 parent a3c6231 commit 991c2298a184e5b4d246fe853dc3f28a792ec361 Edwin Brady committed Jan 16, 2012
Showing with 6 additions and 3 deletions.
  1. +5 −2 src/Idris/AbsSyntax.hs
  2. +1 −1 src/Idris/ElabDecls.hs
@@ -1202,7 +1202,10 @@ toEither (RightOK ho) = Right ho
-- and what they match. Returns the pair that failed if not a match.
matchClause :: PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
-matchClause x y = checkRpts $ match (fullApp x) (fullApp y) where
+matchClause = matchClause' False
+
+matchClause' :: Bool -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
+matchClause' names x y = checkRpts $ match (fullApp x) (fullApp y) where
matchArg x y = match (fullApp (getTm x)) (fullApp (getTm y))
fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))
@@ -1219,7 +1222,7 @@ matchClause x y = checkRpts $ match (fullApp x) (fullApp y) where
match (PRef f n) (PApp _ x []) = match (PRef f n) x
match (PApp _ x []) (PRef f n) = match x (PRef f n)
match (PRef _ n) (PRef _ n') | n == n' = return []
- match (PRef _ n) tm = return [(n, tm)]
+ match (PRef _ n) tm | not names = return [(n, tm)]
match (PEq _ l r) (PEq _ l' r') = do ml <- match' l l'
mr <- match' r r'
return (ml ++ mr)
@@ -625,7 +625,7 @@ checkInferred :: FC -> PTerm -> PTerm -> Idris ()
checkInferred fc inf user =
do logLvl 6 $ "Checked to\n" ++ showImp True inf ++ "\n" ++
showImp True user
- tclift $ case matchClause user inf of
+ tclift $ case matchClause' True user inf of
Right vs -> return ()
Left (x, y) -> tfail $ At fc
(Msg $ "The type-checked term and given term do not match: "

0 comments on commit 991c229

Please sign in to comment.