git.iko.soy/Idris-dev
on master help sign in
Fix universe checking bug
commitab039f284a50b4eba9b390f8dc3466bddb91d403 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateWed 22 Feb 2012, 12:55 (15 years ago) parentdc67893
3 files changed+19−15
compare with master
unifiedsplit
src/Core/Constraints.hs+6−3 src/Idris/ElabDecls.hs+12−11 src/Idris/Prover.hs+1−1
src/Core/Constraints.hs+6−3
@@ -32,7 +32,7 @@ mkRels ((c, f) : cs) acc
3232acyclic :: Relations -> [UExp] -> TC ()
3333acyclic r cvs = checkCycle (FC "root" 0) r [] 0 cvs
3434 where
35− checkCycle :: FC -> Relations -> [UExp] -> Int -> [UExp] -> TC ()
35+ checkCycle :: FC -> Relations -> [(UExp, FC)] -> Int -> [UExp] -> TC ()
3636 checkCycle fc r path inc [] = return ()
3737 checkCycle fc r path inc (c : cs)
3838 = do check fc path inc c
@@ -42,10 +42,13 @@ acyclic r cvs = checkCycle (FC "root" 0) r [] 0 cvs
4242
4343 check fc path inc (UVar x) | x < 0 = return ()
4444 check fc path inc cv
45− | inc > 0 && cv `elem` path = Error $ At fc UniverseError
45+ | inc > 0 && cv `elem` map fst path
46+ = Error $ At fc UniverseError
47+ -- FIXME: Make informative
48+ -- e.g. (Msg ("Cycle: " ++ show cv ++ ", " ++ show path))
4649 | otherwise = case M.lookup cv r of
4750 Nothing -> return ()
48− Just cs -> mapM_ (next (cv:path) inc) cs
51+ Just cs -> mapM_ (next ((cv, fc):path) inc) cs
4952
5053 next path inc (ULT l r, fc) = check fc path (inc + 1) r
5154 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
2626import Debug.Trace
2727
2828
29−recheckC ctxt fc env t
29+recheckC fc env t
3030 = do -- t' <- applyOpts (forget t) (doesn't work, or speed things up...)
31+ ctxt <- getContext
3132 (tm, ty, cs) <- tclift $ case recheck ctxt env (forget t) t of
3233 Error e -> tfail (At fc e)
3334 OK x -> return x
@@ -35,7 +36,7 @@ recheckC ctxt fc env t
3536 return (tm, ty)
3637
3738checkDef fc ns = do ctxt <- getContext
38− mapM (\(n, t) -> do (t', _) <- recheckC ctxt fc [] t
39+ mapM (\(n, t) -> do (t', _) <- recheckC fc [] t
3940 return (n, t')) ns
4041
4142elabType :: 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
5455 addDeferred ds
5556 mapM_ (elabCaseBlock info) is
5657 ctxt <- getContext
57− (cty, _) <- recheckC ctxt fc [] tyT
58+ (cty, _) <- recheckC fc [] tyT
5859 addStatics n cty ty'
5960 logLvl 2 $ "---> " ++ show cty
6061 let nty = normalise ctxt [] cty
@@ -77,7 +78,7 @@ elabData info syn fc (PDatadecl n t_in dcons)
7778 def' <- checkDef fc defer
7879 addDeferred def'
7980 mapM_ (elabCaseBlock info) is
80− (cty, _) <- recheckC ctxt fc [] t'
81+ (cty, _) <- recheckC fc [] t'
8182 logLvl 2 $ "---> " ++ show cty
8283 updateContext (addTyDecl n cty) -- temporary, to check cons
8384 cons <- mapM (elabCon info syn n) dcons
@@ -205,7 +206,7 @@ elabCon info syn tn (n, t_in, fc)
205206 addDeferred def'
206207 mapM_ (elabCaseBlock info) is
207208 ctxt <- getContext
208− (cty, _) <- recheckC ctxt fc [] t'
209+ (cty, _) <- recheckC fc [] t'
209210 tyIs cty
210211 logLvl 2 $ "---> " ++ show n ++ " : " ++ show cty
211212 addIBC (IBCDef n)
@@ -326,7 +327,7 @@ elabVal info aspat tm_in
326327 logLvl 3 ("Value: " ++ show tm')
327328 let vtm = getInferTerm tm'
328329 logLvl 2 (show vtm)
329− recheckC ctxt (FC "(input)" 0) [] vtm
330+ recheckC (FC "(input)" 0) [] vtm
330331
331332-- checks if the clause is a possible left hand side. Returns the term if
332333-- possible, otherwise Nothing.
@@ -365,7 +366,7 @@ elabClause info tcgen (PClause fc fname lhs_in withs rhs_in whereblock)
365366 let lhs_tm = orderPats (getInferTerm lhs')
366367 let lhs_ty = getInferType lhs'
367368 logLvl 3 (show lhs_tm)
368− (clhs, clhsty) <- recheckC ctxt fc [] lhs_tm
369+ (clhs, clhsty) <- recheckC fc [] lhs_tm
369370 logLvl 5 ("Checked " ++ show clhs)
370371 -- Elaborate where block
371372 ist <- getIState
@@ -398,7 +399,7 @@ elabClause info tcgen (PClause fc fname lhs_in withs rhs_in whereblock)
398399 mapM_ (elabCaseBlock info) is
399400 ctxt <- getContext
400401 logLvl 5 $ "Rechecking"
401− (crhs, crhsty) <- recheckC ctxt fc [] rhs'
402+ (crhs, crhsty) <- recheckC fc [] rhs'
402403 i <- get
403404 checkInferred fc (delab' i crhs True) rhs
404405 return $ Just (clhs, crhs)
@@ -430,7 +431,7 @@ elabClause info tcgen (PWith fc fname lhs_in withs wval_in withblock)
430431 let lhs_ty = getInferType lhs'
431432 let ret_ty = getRetTy lhs_ty
432433 logLvl 3 (show lhs_tm)
433− (clhs, clhsty) <- recheckC ctxt fc [] lhs_tm
434+ (clhs, clhsty) <- recheckC fc [] lhs_tm
434435 logLvl 5 ("Checked " ++ show clhs)
435436 let bargs = getPBtys lhs_tm
436437 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)
448449 def' <- checkDef fc defer
449450 addDeferred def'
450451 mapM_ (elabCaseBlock info) is
451− (cwval, cwvalty) <- recheckC ctxt fc [] (getInferTerm wval')
452+ (cwval, cwvalty) <- recheckC fc [] (getInferTerm wval')
452453 logLvl 3 ("With type " ++ show cwvalty ++ "\nRet type " ++ show ret_ty)
453454 windex <- getName
454455 -- build a type declaration for the new function:
@@ -485,7 +486,7 @@ elabClause info tcgen (PWith fc fname lhs_in withs wval_in withblock)
485486 def' <- checkDef fc defer
486487 addDeferred def'
487488 mapM_ (elabCaseBlock info) is
488− (crhs, crhsty) <- recheckC ctxt fc [] rhs'
489+ (crhs, crhsty) <- recheckC fc [] rhs'
489490 return $ Just (clhs, crhs)
490491 where
491492 getImps (Bind n (Pi _) t) = pexp Placeholder : getImps t
src/Idris/Prover.hs+1−1
@@ -45,7 +45,7 @@ prove ctxt lit n ty
4545 put (i { last_proof = Just (n, prf) })
4646 let tree = simpleCase False True [(P Ref n ty, tm)]
4747 logLvl 3 (show tree)
48− (ptm, pty) <- recheckC ctxt (FC "proof" 0) [] tm
48+ (ptm, pty) <- recheckC (FC "proof" 0) [] tm
4949 ptm' <- applyOpts ptm
5050 updateContext (addCasedef n True False True [(P Ref n ty, ptm)]
5151 [(P Ref n ty, ptm')] ty)