git.iko.soy/Idris-dev
on aa7262e help sign in
Idris-dev/src/Core/Constraints.hs
61 lines 2.0 kB history raw
1module Core.Constraints(ucheck) where
3import Core.TT
5import Control.Applicative
6import Control.Arrow
7import Control.Monad.Error
8import Control.Monad.RWS
9import Control.Monad.State
10import Data.List
11import Data.Maybe
12import qualified Data.Map as M
14import Debug.Trace
16ucheck :: [(UConstraint, FC)] -> TC ()
17ucheck cs = acyclic rels (map fst (M.toList rels))
18 where lhs (ULT l _) = l
19 lhs (ULE l _) = l
20 rels = mkRels cs M.empty
22type Relations = M.Map UExp [(UConstraint, FC)]
24mkRels :: [(UConstraint, FC)] -> Relations -> Relations
25mkRels [] acc = acc
26mkRels ((c, f) : cs) acc
27 | not (ignore c)
28 = case M.lookup (lhs c) acc of
29 Nothing -> mkRels cs (M.insert (lhs c) [(c,f)] acc)
30 Just rs -> mkRels cs (M.insert (lhs c) ((c,f):rs) acc)
31 | otherwise = mkRels cs acc
32 where lhs (ULT l _) = l
33 lhs (ULE l _) = l
34 ignore (ULE l r) = l == r
35 ignore _ = False
38acyclic :: Relations -> [UExp] -> TC ()
39acyclic r cvs = checkCycle (FC "root" 0) r [] 0 cvs
40 where
41 checkCycle :: FC -> Relations -> [(UExp, FC)] -> Int -> [UExp] -> TC ()
42 checkCycle fc r path inc [] = return ()
43 checkCycle fc r path inc (c : cs)
44 = do check fc path inc c
45 -- Remove c from r since we know there's no cycles now
46 let r' = M.insert c [] r
47 checkCycle fc r' path inc cs
49 check fc path inc (UVar x) | x < 0 = return ()
50 check fc path inc cv
51 | inc > 0 && cv `elem` map fst path
52 = Error $ At fc UniverseError
53 -- FIXME: Make informative
54 -- e.g. (Msg ("Cycle: " ++ show cv ++ ", " ++ show path))
55 | otherwise = case M.lookup cv r of
56 Nothing -> return ()
57 Just cs -> mapM_ (next ((cv, fc):path) inc) cs
59 next path inc (ULT l r, fc) = check fc path (inc + 1) r
60 next path inc (ULE l r, fc) = check fc path inc r