969e573 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Checking elaborated term and inferred term match

commit969e573a39487d9300a2f625639140677e70a1d0 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateMon 9 Jan 2012, 11:11 (15 years ago) parent3af0ae0

3 files changed+72−28

compare with master

unifiedsplit

src/Idris/AbsSyntax.hs+44−18 src/Idris/Delaborate.hs+5 src/Idris/ElabDecls.hs+23−10

src/Idris/AbsSyntax.hs+44−18

@@ -12,6 +12,7 @@ import System.Console.Haskeline

1212import Control.Monad.State

1313import Data.List

1414import Data.Char

15+import Data.Either

1516import Debug.Trace

1617

1718import qualified Epic.Epic as E

@@ -1154,50 +1155,75 @@ dumpDecl _ = "..."

11541155-- dumpDecl (PImport i) = "import " ++ i

11551156

11561157-- syntactic match of a against b, returning pair of variables in a

1157−-- and what they match. Returns 'Nothing' if not a match.

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

11581159

1159−matchClause :: PTerm -> PTerm -> Maybe [(Name, PTerm)]

1160−matchClause x y = match x y where

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

1161+matchClause x y = checkRpts $ match (fullApp x) (fullApp y) where

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

11621163

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

11641165 fullApp x = x

11651166

1167+ match' x y = match (fullApp x) (fullApp y)

11661168 match (PApp _ f args) (PApp _ f' args')

11671169 | length args == length args'

1168− = do mf <- match f f'

1170+ = do mf <- match' f f'

11691171 ms <- zipWithM matchArg args args'

11701172 return (mf ++ concat ms)

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

11721174-- | otherwise = Nothing

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

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

1175− mr <- match r r'

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

1177+ mr <- match' r r'

11761178 return (ml ++ mr)

1177− match (PPair _ l r) (PPair _ l' r') = do ml <- match l l'

1178− mr <- match r r'

1179+ match (PPair _ l r) (PPair _ l' r') = do ml <- match' l l'

1180+ mr <- match' r r'

11791181 return (ml ++ mr)

1180− match (PDPair _ l t r) (PDPair _ l' t' r') = do ml <- match l l'

1181− mt <- match t t'

1182− mr <- match r r'

1182+ match (PDPair _ l t r) (PDPair _ l' t' r') = do ml <- match' l l'

1183+ mt <- match' t t'

1184+ mr <- match' r r'

11831185 return (ml ++ mt ++ mr)

11841186 match (PAlternative as) (PAlternative as')

1185− = do ms <- zipWithM match as as'

1187+ = do ms <- zipWithM match' as as'

11861188 return (concat ms)

1189+ match a@(PAlternative as) b

1190+ = do let ms = zipWith match' as (repeat b)

1191+ case (rights ms) of

1192+ (x: _) -> return x

1193+ _ -> Left (a, b)

1194+ match (PCase _ _ _) _ = return [] -- lifted out

1195+ match (PMetavar _) _ = return [] -- modified

1196+ match (PQuote _) _ = return []

1197+ match (PProof _) _ = return []

1198+ match (PTactics _) _ = return []

11871199 match (PRefl _) (PRefl _) = return []

11881200 match (PResolveTC _) (PResolveTC _) = return []

11891201 match (PTrue _) (PTrue _) = return []

11901202 match (PFalse _) (PFalse _) = return []

11911203 match (PReturn _) (PReturn _) = return []

1192− match (PPi _ _ t s) (PPi _ _ t' s') = do mt <- match t t'

1193− ms <- match s s'

1204+ match (PPi _ _ t s) (PPi _ _ t' s') = do mt <- match' t t'

1205+ ms <- match' s s'

11941206 return (mt ++ ms)

1195− match (PLam _ t s) (PLam _ t' s') = do mt <- match t t'

1196− ms <- match s s'

1207+ match (PLam _ t s) (PLam _ t' s') = do mt <- match' t t'

1208+ ms <- match' s s'

11971209 return (mt ++ ms)

1198− match (PHidden x) (PHidden y) = match x y

1210+ match (PLet _ t ty s) (PLet _ t' ty' s') = do mt <- match' t t'

1211+ mty <- match' ty ty'

1212+ ms <- match' s s'

1213+ return (mt ++ mty ++ ms)

1214+ match (PHidden x) (PHidden y) = match' x y

1215+ match Placeholder _ = return []

1216+ match (PResolveTC _) _ = return []

11991217 match a b | a == b = return []

1200− | otherwise = Nothing

1218+ | otherwise = Left (a, b)

1219+

1220+ checkRpts (Right ms) = check ms where

1221+ check ((n,t):xs)

1222+ | Just t' <- lookup n xs = if t/=t' then Left (t, t')

1223+ else check xs

1224+ check (_:xs) = check xs

1225+ check [] = Right ms

1226+ checkRpts x = x

12011227

12021228substMatches :: [(Name, PTerm)] -> PTerm -> PTerm

12031229substMatches [] t = t

src/Idris/Delaborate.hs+5

@@ -42,8 +42,13 @@ delab' ist tm fullname = de [] tm

4242 deFn env (App f a) args = deFn env f (a:args)

4343 deFn env (P _ n _) [l,r] | n == pairTy = PPair un (de env l) (de env r)

4444 | n == eqCon = PRefl un

45+ | n == UN "lazy" = de env r

46+ | n == UN "Exists" = PDPair un (de env l) Placeholder

47+ (de env r)

4548 deFn env (P _ n _) [_,_,l,r] | n == pairCon = PPair un (de env l) (de env r)

4649 | n == eqTy = PEq un (de env l) (de env r)

50+ | n == UN "Ex_intro" = PDPair un (de env l) Placeholder

51+ (de env r)

4752 deFn env (P _ n _) args = mkPApp (dens n) (map (de env) args)

4853 deFn env f args = PApp un (de env f) (map pexp (map (de env) args))

4954

src/Idris/ElabDecls.hs+23−10

@@ -197,8 +197,7 @@ elabClause info fc tcgen (PClause fname lhs_in withs rhs_in whereblock)

197197 logLvl 5 $ "Rechecking"

198198 (crhs, crhsty) <- recheckC ctxt fc [] rhs'

199199 i <- get

200− logLvl 6 $ "Checked to\n" ++ showImp True (delab' i crhs True) ++ "\n" ++

201− showImp True rhs

200+ checkInferred fc (delab' i crhs True) rhs

202201 return $ Just (clhs, crhs)

203202 where

204203 decorate x = UN (show fname ++ "#" ++ show x)

@@ -292,7 +291,7 @@ elabClause info fc tcgen (PWith fname lhs_in withs wval_in withblock)

292291 mkAuxC wname lhs ns (PClauses fc o n cs)

293292 | True = do cs' <- mapM (mkAux wname lhs ns) cs

294293 return $ PClauses fc o wname cs'

295− | otherwise = fail $ "with clause uses wrong function name " ++ show n

294+ | otherwise = fail $ show fc ++ "with clause uses wrong function name " ++ show n

296295 mkAuxC wname lhs ns d = return $ d

297296

298297 mkAux wname toplhs ns (PClause n tm_in (w:ws) rhs wheres)

@@ -301,10 +300,10 @@ elabClause info fc tcgen (PWith fname lhs_in withs wval_in withblock)

301300 logLvl 2 ("Matching " ++ showImp True tm ++ " against " ++

302301 showImp True toplhs)

303302 case matchClause toplhs tm of

304− Nothing -> fail "with clause does not match top level"

305− Just mvars -> do logLvl 3 ("Match vars : " ++ show mvars)

306− lhs <- updateLHS n wname mvars ns (fullApp tm) w

307− return $ PClause wname lhs ws rhs wheres

303+ Left _ -> fail $ show fc ++ "with clause does not match top level"

304+ Right mvars -> do logLvl 3 ("Match vars : " ++ show mvars)

305+ lhs <- updateLHS n wname mvars ns (fullApp tm) w

306+ return $ PClause wname lhs ws rhs wheres

308307 mkAux wname toplhs ns (PWith n tm_in (w:ws) wval withs)

309308 = do i <- get

310309 let tm = addImpl i tm_in

@@ -312,9 +311,9 @@ elabClause info fc tcgen (PWith fname lhs_in withs wval_in withblock)

312311 showImp True toplhs)

313312 withs' <- mapM (mkAuxC wname toplhs ns) withs

314313 case matchClause toplhs tm of

315− Nothing -> fail "with clause does not match top level"

316− Just mvars -> do lhs <- updateLHS n wname mvars ns (fullApp tm) w

317− return $ PWith wname lhs ws wval withs'

314+ Left _ -> fail $ show fc ++ "with clause does not match top level"

315+ Right mvars -> do lhs <- updateLHS n wname mvars ns (fullApp tm) w

316+ return $ PWith wname lhs ws wval withs'

318317

319318 updateLHS n wname mvars ns (PApp fc (PRef fc' n') args) w

320319 = return $ substMatches mvars $

@@ -595,4 +594,18 @@ elabCaseBlock info d@(PClauses f o n ps)

595594

596595-- elabDecl' info (PImport i) = loadModule i

597596

597+-- Check that the result of type checking matches what the programmer wrote

598+-- (i.e. - if we inferred any arguments that the user provided, make sure

599+-- they are the same!)

600+

601+checkInferred :: FC -> PTerm -> PTerm -> Idris ()

602+checkInferred fc inf user =

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

604+ showImp True user

605+ tclift $ case matchClause user inf of

606+ Right _ -> return ()

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

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

609+ ++ show x ++ " and " ++ show y)

610+-- ++ "\n" ++ showImp True inf ++ "\n" ++ showImp True user)

598611