991c229 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Better match checking

991c229Edwin Brady15 years ago

src/Idris/AbsSyntax.hs+5−2

@@ -1202,7 +1202,10 @@ toEither (RightOK ho) = Right ho

1202-- and what they match. Returns the pair that failed if not a match.

1203

1204matchClause :: PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]

1205+matchClause = matchClause' False

1206+

1207+matchClause' :: Bool -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]

1205−matchClause x y = checkRpts $ match (fullApp x) (fullApp y) where

1208+matchClause' names x y = checkRpts $ match (fullApp x) (fullApp y) where

1206 matchArg x y = match (fullApp (getTm x)) (fullApp (getTm y))

1209 matchArg x y = match (fullApp (getTm x)) (fullApp (getTm y))

1207

1210

1208 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))

1211 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

1219 match (PRef f n) (PApp _ x []) = match (PRef f n) x

1222 match (PRef f n) (PApp _ x []) = match (PRef f n) x

1220 match (PApp _ x []) (PRef f n) = match x (PRef f n)

1223 match (PApp _ x []) (PRef f n) = match x (PRef f n)

1221 match (PRef _ n) (PRef _ n') | n == n' = return []

1224 match (PRef _ n) (PRef _ n') | n == n' = return []

1222− match (PRef _ n) tm = return [(n, tm)]

1225+ match (PRef _ n) tm | not names = return [(n, tm)]

1223 match (PEq _ l r) (PEq _ l' r') = do ml <- match' l l'

1226 match (PEq _ l r) (PEq _ l' r') = do ml <- match' l l'

1224 mr <- match' r r'

1227 mr <- match' r r'

1225 return (ml ++ mr)

1228 return (ml ++ mr)

src/Idris/ElabDecls.hs+1−1

@@ -625,7 +625,7 @@ checkInferred :: FC -> PTerm -> PTerm -> Idris ()

625checkInferred fc inf user =

626 do logLvl 6 $ "Checked to\n" ++ showImp True inf ++ "\n" ++

627 showImp True user

628− tclift $ case matchClause user inf of

628+ tclift $ case matchClause' True user inf of

629 Right vs -> return ()

630 Left (x, y) -> tfail $ At fc

631 (Msg $ "The type-checked term and given term do not match: "