git.iko.soy/Idris-dev
on master help sign in
Added Constraints.hs for universe constrain solving (but don't expect it
536112dEdwin Brady
src/Core/Constraints.hsnew file+112
compare with master
unifiedsplit
@@ -0,0 +1,112 @@
1+{-# LANGUAGE FlexibleContexts #-}
2+
3+module Core.Constraints(ucheck) where
4+
5+import Core.TT
6+
7+import Control.Applicative
8+import Control.Arrow
9+import Control.Monad.Error
10+import Control.Monad.RWS
11+import Control.Monad.State
12+import Data.List
13+import Data.Maybe
14+import qualified Data.Map as M
15+
16+
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))
24+
25+type Relations = M.Map UExp [(UConstraint, FC)]
26+
27+mkRels :: [(UConstraint, FC)] -> Relations -> Relations
28+mkRels [] acc = acc
29+mkRels ((c, f) : cs) acc
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+ where lhs (ULT l _) = l
34+ lhs (ULE l _) = l
35+
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
110+
111+solve :: Node -> Either String (M.Map String Int)
112+solve n = fst <$> execStateT (solveFrom 0 n) (M.empty, [])