@@ -1,5 +1,3 @@
1−{-# LANGUAGE FlexibleContexts #-}
2−
31module Core.Constraints(ucheck) where
42
53import Core.TT
@@ -14,13 +12,11 @@ import Data.Maybe
1412import qualified Data.Map as M
1513
1614
17−ucheck :: Int -> [(UConstraint, FC)] -> TC ()
18−ucheck num cs = case solve (mkNode num cs) of
19− Left _ -> tfail UniverseError
20− Right _ -> return ()
21−
22−mkNode :: Int -> [(UConstraint, FC)] -> Node
23−mkNode num cs = relNode num (M.toList (mkRels cs M.empty))
15+ucheck :: [(UConstraint, FC)] -> TC ()
16+ucheck 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
2420
2521type Relations = M.Map UExp [(UConstraint, FC)]
2622
@@ -33,80 +29,23 @@ mkRels ((c, f) : cs) acc
3329 where lhs (ULT l _) = l
3430 lhs (ULE l _) = l
3531
36−relNode :: Int -> [(UExp, [(UConstraint, FC)])] -> Node
37−relNode num [] = CI 0 $ map Le (map (expNode . UVar) [0..num])
38−relNode num ((c, cons) : cs) = relNode num cs
39−
40−data Child = Lt Node | Le Node
41− deriving Show
42−
43−data Node = CI Int [Child]
44− | CV String [Child]
45− deriving Show
46−
47−expNode :: UExp -> Node
48−expNode (UVar i) = CV (show (UVar i)) []
49−expNode (UVal i) = CI i []
50−
51−test :: Node
52−test = CI 0 $ [Lt x, Lt y, Le z] ++ map Le ints
53− where
54− x = CV "x" []
55− y = CV "y" [Lt z]
56− z = CV "z" [Lt x]
57− ints = [ -- CI 3 [Lt y]
58− ]
59−
60−add :: Node -> Node -> Node
61−add i node = undefined
62−
63−test2 :: Node
64−test2 = CI 0 $ [ Le v84, Le q25 ] ++ map Le [g,e85,v29,f90,j45,g86,n45,v84,q25,y48,q45,h45,g90]
65− where
66− g = CV "g" [Le y48]
67− e85 = CV "e85" [Le n45, Le q45, Le h45]
68− v29 = CV "v29" [Lt g90]
69− f90 = CV "f90" [Lt g90]
70− j45 = CV "j45" [Lt f90]
71− g86 = CV "g86" [Lt f90]
72− n45 = CV "n45" []
73− v84 = CV "v84" []
74− q25 = CV "q25" []
75− y48 = CV "y48" []
76− q45 = CV "q45" []
77− h45 = CV "h45" []
78− g90 = CV "g90" []
79−
80−cyclic :: Node
81−cyclic = CI 0 $ map Le [a,b,c]
82− where
83− a = CV "a" [Lt b]
84− b = CV "b" [Lt c]
85− c = CV "c" [Lt a]
86−
87−-- onChild :: Int -> Child -> m ()
88−onChild i (Lt n) = solveFrom (i+1) n
89−onChild i (Le n) = solveFrom i n
90−
91−solveFrom ::
92− ( Applicative m
93− , MonadState (M.Map String Int, [String]) m
94− , MonadError String m
95− ) => Int -> Node -> m ()
96−solveFrom num (CI i chs ) = do
97− let numi = max num i
98− mapM_ (onChild numi) chs
99−solveFrom num (CV nm chs) = do
100− nms <- snd <$> get
101− if nm `elem` nms
102− then throwError $ "cycle: " ++ intercalate ", " nms
103− else do
104− modify $ second (nm:) -- add this node for cycle detection
105− i <- M.lookup nm . fst <$> get
106− let numi = max num (fromMaybe 0 i)
107− modify $ first (M.insert nm numi)
108− mapM_ (onChild numi) chs
109− modify $ second (drop 1) -- remove the node
32+acyclic :: Relations -> [UExp] -> TC ()
33+acyclic 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
42+
43+ check fc path inc cv
44+ | inc > 0 && cv `elem` path = Error $ At fc UniverseError
45+ | otherwise = case M.lookup cv r of
46+ Nothing -> return ()
47+ Just cs -> mapM_ (next (cv:path) inc) cs
48+
49+ next path inc (ULT l r, fc) = check fc path (inc + 1) r
50+ next path inc (ULE l r, fc) = check fc path inc r
11051
111−solve :: Node -> Either String (M.Map String Int)
112−solve n = fst <$> execStateT (solveFrom 0 n) (M.empty, [])