ab039f2 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Fix universe checking bug

ab039f2Edwin Brady15 years ago

src/Core/Constraints.hs+6−3

compare with master

unifiedsplit

@@ -32,7 +32,7 @@ mkRels ((c, f) : cs) acc

32acyclic :: Relations -> [UExp] -> TC ()

33acyclic r cvs = checkCycle (FC "root" 0) r [] 0 cvs

34 where

35− checkCycle :: FC -> Relations -> [UExp] -> Int -> [UExp] -> TC ()

35+ checkCycle :: FC -> Relations -> [(UExp, FC)] -> Int -> [UExp] -> TC ()

36 checkCycle fc r path inc [] = return ()

37 checkCycle fc r path inc (c : cs)

38 = do check fc path inc c

@@ -42,10 +42,13 @@ acyclic r cvs = checkCycle (FC "root" 0) r [] 0 cvs

43 check fc path inc (UVar x) | x < 0 = return ()

44 check fc path inc cv

45+ | inc > 0 && cv `elem` map fst path

45− | inc > 0 && cv `elem` path = Error $ At fc UniverseError

46+ = Error $ At fc UniverseError

47+ -- FIXME: Make informative

48+ -- e.g. (Msg ("Cycle: " ++ show cv ++ ", " ++ show path))

46 | otherwise = case M.lookup cv r of

49 | otherwise = case M.lookup cv r of

47 Nothing -> return ()

50 Nothing -> return ()

48− Just cs -> mapM_ (next (cv:path) inc) cs

51+ Just cs -> mapM_ (next ((cv, fc):path) inc) cs

50 next path inc (ULT l r, fc) = check fc path (inc + 1) r

53 next path inc (ULT l r, fc) = check fc path (inc + 1) r

51 next path inc (ULE l r, fc) = check fc path inc r

54 next path inc (ULE l r, fc) = check fc path inc r

src/Idris/ElabDecls.hs+12−11

@@ -26,8 +26,9 @@ import Data.Maybe

26import Debug.Trace

29−recheckC ctxt fc env t

29+recheckC fc env t

30 = do -- t' <- applyOpts (forget t) (doesn't work, or speed things up...)

31+ ctxt <- getContext

31 (tm, ty, cs) <- tclift $ case recheck ctxt env (forget t) t of

32 (tm, ty, cs) <- tclift $ case recheck ctxt env (forget t) t of

32 Error e -> tfail (At fc e)

33 Error e -> tfail (At fc e)

33 OK x -> return x

34 OK x -> return x

@@ -35,7 +36,7 @@ recheckC ctxt fc env t

35 return (tm, ty)

36 return (tm, ty)

37checkDef fc ns = do ctxt <- getContext

38checkDef fc ns = do ctxt <- getContext

38− mapM (\(n, t) -> do (t', _) <- recheckC ctxt fc [] t

39+ mapM (\(n, t) -> do (t', _) <- recheckC fc [] t

39 return (n, t')) ns

40 return (n, t')) ns

41elabType :: ElabInfo -> SyntaxInfo -> FC -> FnOpts -> Name -> PTerm -> Idris ()

42elabType :: ElabInfo -> SyntaxInfo -> FC -> FnOpts -> Name -> PTerm -> Idris ()

@@ -54,7 +55,7 @@ elabType info syn fc opts n ty' = {- let ty' = piBind (params info) ty_in

54 addDeferred ds

55 addDeferred ds

55 mapM_ (elabCaseBlock info) is

56 mapM_ (elabCaseBlock info) is

56 ctxt <- getContext

57 ctxt <- getContext

57− (cty, _) <- recheckC ctxt fc [] tyT

58+ (cty, _) <- recheckC fc [] tyT

58 addStatics n cty ty'

59 addStatics n cty ty'

59 logLvl 2 $ "---> " ++ show cty

60 logLvl 2 $ "---> " ++ show cty

60 let nty = normalise ctxt [] cty

61 let nty = normalise ctxt [] cty

@@ -77,7 +78,7 @@ elabData info syn fc (PDatadecl n t_in dcons)

77 def' <- checkDef fc defer

78 def' <- checkDef fc defer

78 addDeferred def'

79 addDeferred def'

79 mapM_ (elabCaseBlock info) is

80 mapM_ (elabCaseBlock info) is

80− (cty, _) <- recheckC ctxt fc [] t'

81+ (cty, _) <- recheckC fc [] t'

81 logLvl 2 $ "---> " ++ show cty

82 logLvl 2 $ "---> " ++ show cty

82 updateContext (addTyDecl n cty) -- temporary, to check cons

83 updateContext (addTyDecl n cty) -- temporary, to check cons

83 cons <- mapM (elabCon info syn n) dcons

84 cons <- mapM (elabCon info syn n) dcons

@@ -205,7 +206,7 @@ elabCon info syn tn (n, t_in, fc)

205 addDeferred def'

206 addDeferred def'

206 mapM_ (elabCaseBlock info) is

207 mapM_ (elabCaseBlock info) is

207 ctxt <- getContext

208 ctxt <- getContext

208− (cty, _) <- recheckC ctxt fc [] t'

209+ (cty, _) <- recheckC fc [] t'

209 tyIs cty

210 tyIs cty

210 logLvl 2 $ "---> " ++ show n ++ " : " ++ show cty

211 logLvl 2 $ "---> " ++ show n ++ " : " ++ show cty

211 addIBC (IBCDef n)

212 addIBC (IBCDef n)

@@ -326,7 +327,7 @@ elabVal info aspat tm_in

326 logLvl 3 ("Value: " ++ show tm')

327 logLvl 3 ("Value: " ++ show tm')

327 let vtm = getInferTerm tm'

328 let vtm = getInferTerm tm'

328 logLvl 2 (show vtm)

329 logLvl 2 (show vtm)

329− recheckC ctxt (FC "(input)" 0) [] vtm

330+ recheckC (FC "(input)" 0) [] vtm

330

331

331-- checks if the clause is a possible left hand side. Returns the term if

332-- checks if the clause is a possible left hand side. Returns the term if

332-- possible, otherwise Nothing.

333-- possible, otherwise Nothing.

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

365 let lhs_tm = orderPats (getInferTerm lhs')

366 let lhs_tm = orderPats (getInferTerm lhs')

366 let lhs_ty = getInferType lhs'

367 let lhs_ty = getInferType lhs'

367 logLvl 3 (show lhs_tm)

368 logLvl 3 (show lhs_tm)

368− (clhs, clhsty) <- recheckC ctxt fc [] lhs_tm

369+ (clhs, clhsty) <- recheckC fc [] lhs_tm

369 logLvl 5 ("Checked " ++ show clhs)

370 logLvl 5 ("Checked " ++ show clhs)

370 -- Elaborate where block

371 -- Elaborate where block

371 ist <- getIState

372 ist <- getIState

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

398 mapM_ (elabCaseBlock info) is

399 mapM_ (elabCaseBlock info) is

399 ctxt <- getContext

400 ctxt <- getContext

400 logLvl 5 $ "Rechecking"

401 logLvl 5 $ "Rechecking"

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

402+ (crhs, crhsty) <- recheckC fc [] rhs'

402 i <- get

403 i <- get

403 checkInferred fc (delab' i crhs True) rhs

404 checkInferred fc (delab' i crhs True) rhs

404 return $ Just (clhs, crhs)

405 return $ Just (clhs, crhs)

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

430 let lhs_ty = getInferType lhs'

431 let lhs_ty = getInferType lhs'

431 let ret_ty = getRetTy lhs_ty

432 let ret_ty = getRetTy lhs_ty

432 logLvl 3 (show lhs_tm)

433 logLvl 3 (show lhs_tm)

433− (clhs, clhsty) <- recheckC ctxt fc [] lhs_tm

434+ (clhs, clhsty) <- recheckC fc [] lhs_tm

434 logLvl 5 ("Checked " ++ show clhs)

435 logLvl 5 ("Checked " ++ show clhs)

435 let bargs = getPBtys lhs_tm

436 let bargs = getPBtys lhs_tm

436 let wval = addImplBound i (map fst bargs) wval_in

437 let wval = addImplBound i (map fst bargs) wval_in

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

448 def' <- checkDef fc defer

449 def' <- checkDef fc defer

449 addDeferred def'

450 addDeferred def'

450 mapM_ (elabCaseBlock info) is

451 mapM_ (elabCaseBlock info) is

451− (cwval, cwvalty) <- recheckC ctxt fc [] (getInferTerm wval')

452+ (cwval, cwvalty) <- recheckC fc [] (getInferTerm wval')

452 logLvl 3 ("With type " ++ show cwvalty ++ "\nRet type " ++ show ret_ty)

453 logLvl 3 ("With type " ++ show cwvalty ++ "\nRet type " ++ show ret_ty)

453 windex <- getName

454 windex <- getName

454 -- build a type declaration for the new function:

455 -- build a type declaration for the new function:

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

485 def' <- checkDef fc defer

486 def' <- checkDef fc defer

486 addDeferred def'

487 addDeferred def'

487 mapM_ (elabCaseBlock info) is

488 mapM_ (elabCaseBlock info) is

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

489+ (crhs, crhsty) <- recheckC fc [] rhs'

489 return $ Just (clhs, crhs)

490 return $ Just (clhs, crhs)

490 where

491 where

491 getImps (Bind n (Pi _) t) = pexp Placeholder : getImps t

492 getImps (Bind n (Pi _) t) = pexp Placeholder : getImps t

src/Idris/Prover.hs+1−1

@@ -45,7 +45,7 @@ prove ctxt lit n ty

45 put (i { last_proof = Just (n, prf) })

46 let tree = simpleCase False True [(P Ref n ty, tm)]

47 logLvl 3 (show tree)

48− (ptm, pty) <- recheckC ctxt (FC "proof" 0) [] tm

48+ (ptm, pty) <- recheckC (FC "proof" 0) [] tm

49 ptm' <- applyOpts ptm

50 updateContext (addCasedef n True False True [(P Ref n ty, ptm)]

51 [(P Ref n ty, ptm')] ty)