git.iko.soy/Idris-dev
on fb3160e help sign in
Idris-dev/src/Core/Constraints.hs
52 lines 1.7 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
15ucheck :: [(UConstraint, FC)] -> TC ()
16ucheck cs = acyclic rels (map fst (M.toList rels))
17 where lhs (ULT l _) = l
18 lhs (ULE l _) = l
19 rels = mkRels cs M.empty
21type Relations = M.Map UExp [(UConstraint, FC)]
23mkRels :: [(UConstraint, FC)] -> Relations -> Relations
24mkRels [] acc = acc
25mkRels ((c, f) : cs) acc
26 = case M.lookup (lhs c) acc of
27 Nothing -> mkRels cs (M.insert (lhs c) [(c,f)] acc)
28 Just rs -> mkRels cs (M.insert (lhs c) ((c,f):rs) acc)
29 where lhs (ULT l _) = l
30 lhs (ULE l _) = l
32acyclic :: Relations -> [UExp] -> TC ()
33acyclic r cvs = checkCycle (FC "root" 0) r [] 0 cvs
34 where
35 checkCycle :: FC -> Relations -> [UExp] -> 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
39 -- Remove c from r since we know there's no cycles now
40 let r' = M.insert c [] r
41 checkCycle fc r' path inc cs
43 check fc path inc (UVar x) | x < 0 = return ()
44 check fc path inc cv
45 | inc > 0 && cv `elem` path = Error $ At fc UniverseError
46 | otherwise = case M.lookup cv r of
47 Nothing -> return ()
48 Just cs -> mapM_ (next (cv:path) inc) cs
50 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