on master help sign in
Merge pull request #1666 from edwinb/universes

Faster universe checking

commitfde21b756a633f15584aa7320fc1d3e1c63d3430 authorEdwin Brady <edwin.brady@gmail.com> dateSun 19 Oct 2014, 15:45 (12 years ago) parent64bd27ed34472a
1 file changed+12−10
src/Idris/Core/Constraints.hs+12−10
src/Idris/Core/Constraints.hs+12−10
@@ -11,7 +11,7 @@ import Control.Monad.RWS
1111import Control.Monad.State
1212import Data.List
1313import Data.Maybe
14−import qualified Data.Map as M
14+import qualified Data.Map.Strict as M
1515
1616import Debug.Trace
1717
@@ -20,7 +20,8 @@ ucheck :: [(UConstraint, FC)] -> TC ()
2020ucheck cs = acyclic rels (map fst (M.toList rels))
2121 where lhs (ULT l _) = l
2222 lhs (ULE l _) = l
23− rels = mkRels cs M.empty
23+ cs' = nub cs
24+ rels = mkRels cs' M.empty
2425
2526type Relations = M.Map UExp [(UConstraint, FC)]
2627
@@ -44,13 +45,13 @@ acyclic r cvs = checkCycle (fileFC "root") r [] 0 cvs
4445 checkCycle :: FC -> Relations -> [(UExp, FC)] -> Int -> [UExp] -> TC ()
4546 checkCycle fc r path inc [] = return ()
4647 checkCycle fc r path inc (c : cs)
47− = do check fc path inc c
48+ = do check fc r path inc c
4849 -- Remove c from r since we know there's no cycles now
4950 let r' = M.insert c [] r
5051 checkCycle fc r' path inc cs
5152
52− check fc path inc (UVar x) | x < 0 = return ()
53− check fc path inc cv
53+ check fc r path inc (UVar x) | x < 0 = return ()
54+ check fc r path inc cv
5455 | inc > 0 && cv `elem` map fst path
5556 = Error $ At fc UniverseError
5657 -- FIXME: Make informative
@@ -59,10 +60,11 @@ acyclic r cvs = checkCycle (fileFC "root") r [] 0 cvs
5960 -- fine, because they must all be equal, so stop.
6061 | inc == 0 && cv `elem` map fst path
6162 = return ()
62− | otherwise = case M.lookup cv r of
63− Nothing -> return ()
64− Just cs -> mapM_ (next ((cv, fc):path) inc) cs
63+ | otherwise
64+ = case M.lookup cv r of
65+ Nothing -> return ()
66+ Just cs -> mapM_ (next r ((cv, fc):path) inc) cs
6567
66− next path inc (ULT l r, fc) = check fc path (inc + 1) r
67− next path inc (ULE l r, fc) = check fc path inc r
68+ next r path inc (ULT l x, fc) = check fc r path (inc + 1) x
69+ next r path inc (ULE l x, fc) = check fc r path inc x
6870