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

git.iko.soy/Idris-dev

on master help sign in

Checking elaborated term and inferred term match

969e573Edwin Brady15 years ago

src/Idris/AbsSyntax.hs+44−18

compare with master

unifiedsplit

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

12import Control.Monad.State

13import Data.List

14import Data.Char

15+import Data.Either

15import Debug.Trace

16import Debug.Trace

17import qualified Epic.Epic as E

18import qualified Epic.Epic as E

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

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

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

1155

1156

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

1157-- 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.

1158

1159

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

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

1160−matchClause x y = match x y where

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

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

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

1162

1163

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

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

1164 fullApp x = x

1165 fullApp x = x

1165

1166

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

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

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

1167 | length args == length args'

1169 | length args == length args'

1168− = do mf <- match f f'

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

1169 ms <- zipWithM matchArg args args'

1171 ms <- zipWithM matchArg args args'

1170 return (mf ++ concat ms)

1172 return (mf ++ concat ms)

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

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

1172-- | otherwise = Nothing

1174-- | otherwise = Nothing

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

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

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

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

1175− mr <- match r r'

1177+ mr <- match' r r'

1176 return (ml ++ mr)

1178 return (ml ++ mr)

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

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

1178− mr <- match r r'

1180+ mr <- match' r r'

1179 return (ml ++ mr)

1181 return (ml ++ mr)

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

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

1181− mt <- match t t'

1183+ mt <- match' t t'

1182− mr <- match r r'

1184+ mr <- match' r r'

1183 return (ml ++ mt ++ mr)

1185 return (ml ++ mt ++ mr)

1184 match (PAlternative as) (PAlternative as')

1186 match (PAlternative as) (PAlternative as')

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

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

1186 return (concat ms)

1188 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 []

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

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

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

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

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

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

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

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

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

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

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

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

1193− ms <- match s s'

1205+ ms <- match' s s'

1194 return (mt ++ ms)

1206 return (mt ++ ms)

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

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

1196− ms <- match s s'

1208+ ms <- match' s s'

1197 return (mt ++ ms)

1209 return (mt ++ ms)

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)

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

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

1215+ match Placeholder _ = return []

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

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

1217 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

1201

1227

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

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

1203substMatches [] t = t

1229substMatches [] t = t

src/Idris/Delaborate.hs+5

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

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

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

44 | 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)

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

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

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

49 | 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)

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

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

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

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

src/Idris/ElabDecls.hs+23−10

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

197 logLvl 5 $ "Rechecking"

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

199 i <- get

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

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

201− showImp True rhs

202 return $ Just (clhs, crhs)

201 return $ Just (clhs, crhs)

203 where

202 where

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

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

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

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

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

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

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

294 return $ PClauses fc o wname cs'

293 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

296 mkAuxC wname lhs ns d = return $ d

295 mkAuxC wname lhs ns d = return $ d

297

296

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

297 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)

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

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

302 showImp True toplhs)

301 showImp True toplhs)

303 case matchClause toplhs tm of

302 case matchClause toplhs tm of

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

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

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

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

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

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

307− return $ PClause wname lhs ws rhs wheres

306+ return $ PClause wname lhs ws rhs wheres

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

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

309 = do i <- get

308 = do i <- get

310 let tm = addImpl i tm_in

309 let tm = addImpl i tm_in

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

312 showImp True toplhs)

311 showImp True toplhs)

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

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

314 case matchClause toplhs tm of

313 case matchClause toplhs tm of

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

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

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

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

317− return $ PWith wname lhs ws wval withs'

316+ return $ PWith wname lhs ws wval withs'

318

317

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

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

320 = return $ substMatches mvars $

319 = return $ substMatches mvars $

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

595

594

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

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

597

596

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)

598

611