git.iko.soy/Idris-dev
on d66da21 help sign in
Idris-dev/src/Core/Constraints.hs
67 lines 2.2 kB history raw
1-- | Check universe constraints.
2module Core.Constraints(ucheck) where
4import Core.TT
6import Control.Applicative
7import Control.Arrow
8import Control.Monad.Error
9import Control.Monad.RWS
10import Control.Monad.State
11import Data.List
12import Data.Maybe
13import qualified Data.Map as M
15import Debug.Trace
17-- | Check that a list of universe constraints can be satisfied.
18ucheck :: [(UConstraint, FC)] -> TC ()
19ucheck cs = acyclic rels (map fst (M.toList rels))
20 where lhs (ULT l _) = l
21 lhs (ULE l _) = l
22 rels = mkRels cs M.empty
24type Relations = M.Map UExp [(UConstraint, FC)]
26mkRels :: [(UConstraint, FC)] -> Relations -> Relations
27mkRels [] acc = acc
28mkRels ((c, f) : cs) acc
29 | not (ignore c)
30 = case M.lookup (lhs c) acc of
31 Nothing -> mkRels cs (M.insert (lhs c) [(c,f)] acc)
32 Just rs -> mkRels cs (M.insert (lhs c) ((c,f):rs) acc)
33 | otherwise = mkRels cs acc
34 where lhs (ULT l _) = l
35 lhs (ULE l _) = l
36 ignore (ULE l r) = l == r
37 ignore _ = False
40acyclic :: Relations -> [UExp] -> TC ()
41acyclic r cvs = checkCycle (fileFC "root") r [] 0 cvs
42 where
43 checkCycle :: FC -> Relations -> [(UExp, FC)] -> Int -> [UExp] -> TC ()
44 checkCycle fc r path inc [] = return ()
45 checkCycle fc r path inc (c : cs)
46 = do check fc path inc c
47 -- Remove c from r since we know there's no cycles now
48 let r' = M.insert c [] r
49 checkCycle fc r' path inc cs
51 check fc path inc (UVar x) | x < 0 = return ()
52 check fc path inc cv
53 | inc > 0 && cv `elem` map fst path
54 = Error $ At fc UniverseError
55 -- FIXME: Make informative
56 -- e.g. (Msg ("Cycle: " ++ show cv ++ ", " ++ show path))
57 -- if we reach a cycle but we're at the same universe level, it's
58 -- fine, because they must all be equal, so stop.
59 | inc == 0 && cv `elem` map fst path
60 = return ()
61 | otherwise = case M.lookup cv r of
62 Nothing -> return ()
63 Just cs -> mapM_ (next ((cv, fc):path) inc) cs
65 next path inc (ULT l r, fc) = check fc path (inc + 1) r
66 next path inc (ULE l r, fc) = check fc path inc r