95364f3 · elk · git.iko.soy

git.iko.soy/elk

Refactor lots of code in the type-checker. Also includes some efficiency improvements to make unification a bit faster.

95364f3evancz14 years ago

elm/Elm.cabal+2

compare with master

unifiedsplit

@@ -54,6 +54,7 @@ Library

54 Types.Types,

55 Types.Constrain,

56 Types.Hints,

57+ Types.Solver,

57 Types.Substitutions,

58 Types.Substitutions,

58 Types.Unify,

59 Types.Unify,

59 Paths_Elm

60 Paths_Elm

@@ -99,6 +100,7 @@ Executable elm

99 Types.Types,

100 Types.Types,

100 Types.Constrain,

101 Types.Constrain,

101 Types.Hints,

102 Types.Hints,

103+ Types.Solver,

102 Types.Substitutions,

104 Types.Substitutions,

103 Types.Unify,

105 Types.Unify,

104 Paths_Elm

106 Paths_Elm

elm/elm-runtime-0.5.5.js+8−21

@@ -2126,11 +2126,9 @@ function setPos(pos,e) {

2126 if (pos[2][0] !== "Near") e.style.bottom = 0;

2127 break;

2128 case "PositionAt":

2129− console.log(toPos(pos[1]),toPos(pos[2]));

2130 e.style.top = toPos(pos[2]);

2129 e.style.top = toPos(pos[2]);

2131 e.style.left = toPos(pos[1]);

2130 e.style.left = toPos(pos[1]);

2132 var shift = "translate(" + ~~(-e.style.width.slice(0,-2) / 2) + "px," + ~~(-e.style.height.slice(0,-2) / 2) + "px)";

2131 var shift = "translate(" + ~~(-e.style.width.slice(0,-2) / 2) + "px," + ~~(-e.style.height.slice(0,-2) / 2) + "px)";

2133− console.log(shift);

2134 e.style.transform = shift;

2132 e.style.transform = shift;

2135 e.style.msTransform = shift;

2133 e.style.msTransform = shift;

2136 e.style.MozTransform = shift;

2134 e.style.MozTransform = shift;

@@ -2828,7 +2826,7 @@ Elm.Random = function() {

2828 return { inRange:inRange, randomize:randomize };

2826 return { inRange:inRange, randomize:randomize };

2829}();Elm.Time = function() {

2827}();Elm.Time = function() {

2830 function timeNow() { return (new window.Date).getTime(); }

2828 function timeNow() { return (new window.Date).getTime(); }

2831− var now = function(t) {

2829+ var every = function(t) {

2832 var clock = Elm.Signal.constant(timeNow());

2830 var clock = Elm.Signal.constant(timeNow());

2833 function tellTime() { Dispatcher.notify(clock.id, timeNow()); }

2831 function tellTime() { Dispatcher.notify(clock.id, timeNow()); }

2834 setInterval(tellTime, t);

2832 setInterval(tellTime, t);

@@ -2841,16 +2839,6 @@ Elm.Random = function() {

2841 function f(t) { setTimeout(tick, msPerFrame); return t; }

2839 function f(t) { setTimeout(tick, msPerFrame); return t; }

2842 return Elm.Signal.lift(f)(ticker);

2840 return Elm.Signal.lift(f)(ticker);

2843 }

2841 }

2844− var every = function(t) {

2845− t *= 1000;

2846− var clock = Elm.Signal.constant(0);

2847− var time = 0;

2848− setInterval(function() {

2849− time += t;

2850− Dispatcher.notify(clock.id, time/1000);

2851− }, t);

2852− return clock;

2853− };

2854 var after = function(t) {

2842 var after = function(t) {

2855 t *= 1000;

2843 t *= 1000;

2856 var thread = Elm.Signal.constant(false);

2844 var thread = Elm.Signal.constant(false);

@@ -2867,8 +2855,7 @@ Elm.Random = function() {

2867 var t = window.Date.parse(s);

2855 var t = window.Date.parse(s);

2868 return isNaN(t) ? ["Nothing"] : ["Just",t];

2856 return isNaN(t) ? ["Nothing"] : ["Just",t];

2869 }

2857 }

2870− return {now:now,

2871− fps:fps,

2858+ return {fps:fps,

2872 every:every,

2859 every:every,

2873 after:after,

2860 after:after,

2874 before:before,

2861 before:before,

@@ -2876,9 +2863,9 @@ Elm.Random = function() {

2876 minutes : function(n) { return n * 60000; },

2863 minutes : function(n) { return n * 60000; },

2877 seconds : function(n) { return n * 1000; },

2864 seconds : function(n) { return n * 1000; },

2878 millis : function(n) { return n; },

2865 millis : function(n) { return n; },

2879− inHours : function(t) { return ~~(t / 3600000); },

2866+ inHours : function(t) { return t / 3600000; },

2880− inMinutes : function(t) { return ~~(t / 60000); },

2867+ inMinutes : function(t) { return t / 60000; },

2881− inSeconds : function(t) { return ~~(t / 1000); },

2868+ inSeconds : function(t) { return t / 1000; },

2882 inMillis : function(t) { return t; },

2869 inMillis : function(t) { return t; },

2883 toDate : function(t) { return new window.Date(t); },

2870 toDate : function(t) { return new window.Date(t); },

2884 read : read

2871 read : read

@@ -2907,7 +2894,7 @@ Elm.Random = function() {

2907Elm.Date = function() {

2894Elm.Date = function() {

2908

2895

2909 function dateNow() { return new window.Date; }

2896 function dateNow() { return new window.Date; }

2910− function now(t) {

2897+ function every(t) {

2911 var clock = Elm.Signal.constant(dateNow());

2898 var clock = Elm.Signal.constant(dateNow());

2912 function tellTime() { Dispatcher.notify(clock.id, dateNow()); }

2899 function tellTime() { Dispatcher.notify(clock.id, dateNow()); }

2913 setInterval(tellTime, t);

2900 setInterval(tellTime, t);

@@ -2924,7 +2911,7 @@ Elm.Date = function() {

2924 "Jul", "Aug", "Sep", "Oct", "Nov", "Dec"];

2911 "Jul", "Aug", "Sep", "Oct", "Nov", "Dec"];

2925

2912

2926 return {

2913 return {

2927− now : now,

2914+ every : every,

2928 read : readDate,

2915 read : readDate,

2929 year : function(d) { return d.getFullYear(); },

2916 year : function(d) { return d.getFullYear(); },

2930 month : function(d) { return [monthTable[d.getMonth()]]; },

2917 month : function(d) { return [monthTable[d.getMonth()]]; },

@@ -2932,7 +2919,7 @@ Elm.Date = function() {

2932 hour : function(d) { return d.getHours(); },

2919 hour : function(d) { return d.getHours(); },

2933 minute : function(d) { return d.getMinutes(); },

2920 minute : function(d) { return d.getMinutes(); },

2934 second : function(d) { return d.getSeconds(); },

2921 second : function(d) { return d.getSeconds(); },

2935− weekday : function(d) { return [dayTable[d.getDay()]]; },

2922+ dayOfWeek : function(d) { return [dayTable[d.getDay()]]; },

2936 toTime : function(d) { return d.getTime(); },

2923 toTime : function(d) { return d.getTime(); },

2937 Mon : ["Mon"], Tue : ["Tue"], Wed : ["Wed"],

2924 Mon : ["Mon"], Tue : ["Tue"], Wed : ["Wed"],

2938 Thu : ["Thu"], Fri : ["Fri"], Sat : ["Sat"], Sun : ["Sun"],

2925 Thu : ["Thu"], Fri : ["Fri"], Sat : ["Sat"], Sun : ["Sun"],

elm/src/Compiler.hs+1−3

@@ -18,8 +18,6 @@ import CompileToJS

18import GenerateHtml

19import Paths_Elm

21−import System.IO.Unsafe

22−

23data ELM =

21data ELM =

24 ELM { make :: Bool

22 ELM { make :: Bool

25 , files :: [FilePath]

23 , files :: [FilePath]

@@ -73,7 +71,7 @@ fileTo isMini get what jsFiles noscript outputDir rtLoc file = do

73 let path = fromMaybe "" outputDir </> file

71 let path = fromMaybe "" outputDir </> file

74 js = replaceExtension path ".js"

72 js = replaceExtension path ".js"

75 html = replaceExtension path ".html"

73 html = replaceExtension path ".html"

76− in case unsafePerformIO (print path) `seq` what of

74+ in case what of

77 JS -> writeFile js . formatJS $ jss ++ concatMap jsModule ms

75 JS -> writeFile js . formatJS $ jss ++ concatMap jsModule ms

78 HTML -> writeFile html . renderHtml $ modulesToHtml jsStyle "" rtLoc jss noscript ms

76 HTML -> writeFile html . renderHtml $ modulesToHtml jsStyle "" rtLoc jss noscript ms

79 Split -> do

77 Split -> do

elm/src/Types/Constrain.hs+11−11

@@ -200,20 +200,20 @@ stmtGen (Definition def) = do (as,cs,hint) <- defGen def

200

201stmtGen (Datatype name xs tcs) = do schemes <- mapM gen' tcs'

202 return (Map.empty, Set.empty, schemes)

203− where names = map (+ (length xs)) [1..5]

203+ where var n = length xs + n

204+ ( a, b, c) = ( var 1, var 2, var 3)

205+ (va,vb,vc) = (VarT a, VarT b, VarT c)

206+ rnm (ADT n []) | n == "Number" = va

207+ | n == "Appendable" = vb

208+ | n == "Comparable" = vc

209+ rnm t = t

204− tcs' = map (second . map $ rnm names) tcs

210+ tcs' = map (second (map rnm)) tcs

205− supers t = map (Context name) $ zipWith (:<:) (map VarT names)

211+ supers t = map (Context name) $

206− [ number, time, appendable t, comparable, transformable ]

212+ zipWith (:<:) [va,vb,vc] [number,appendable t,comparable]

207 gen' (n,ts) = do t <- beta

213 gen' (n,ts) = do t <- beta

208− let s = Forall (xs ++ names) (supers t) $

214+ let s = Forall (xs ++ [a,b,c]) (supers t) $

209 foldr (==>) (ADT name $ map VarT xs) ts

215 foldr (==>) (ADT name $ map VarT xs) ts

210 (,) n `liftM` generalize [] s

216 (,) n `liftM` generalize [] s

211− rnm [a,b,c,d,e] (ADT n []) | n == "Number" = VarT a

212− | n == "Time" = VarT b

213− | n == "Appendable" = VarT c

214− | n == "Comparable" = VarT d

215− | n == "Transformable" = VarT e

216− rnm _ t = t

217

218stmtGen (ExportEvent js elm tipe) = do

219 x <- guid

elm/src/Types/Hints.hs+40−7

@@ -179,11 +179,8 @@ http = prefix "HTTP"

179concreteSignals =

180 [ "Keyboard.Raw.keysDown" -: signalOf (listOf int)

181 , "Keyboard.Raw.charPressed" -: signalOf (maybeOf int)

182− , "Random.inRange" -: int ==> int ==> signalOf int

182+ , "Random.inRange" -: int ==> int ==> signalOf int

183− , "Random.randomize" -:: int ==> int ==> signalOf a ==> signalOf int

183+ , "Random.randomize" -:: int ==> int ==> signalOf a ==> signalOf int

184− , timeScheme "Time.every" (\t -> t ==> signalOf t)

185− , timeScheme "Time.before" (\t -> t ==> signalOf bool)

186− , timeScheme "Time.after" (\t -> t ==> signalOf bool)

187 , "Window.dimensions" -: signalOf point

184 , "Window.dimensions" -: signalOf point

188 , "Window.width" -: signalOf int

185 , "Window.width" -: signalOf int

189 , "Window.height" -: signalOf int

186 , "Window.height" -: signalOf int

@@ -202,6 +199,43 @@ concreteSignals =

202 , "Input.dropDown" -:: listOf (tupleOf [string,a]) ==> tupleOf [element, signalOf a]

199 , "Input.dropDown" -:: listOf (tupleOf [string,a]) ==> tupleOf [element, signalOf a]

203 ]

200 ]

204

201

202+times = prefix "Time"

203+ [ "deltas" -: signalOf time ==> signalOf time

204+ , "fps" -: number ==> signalOf time

205+ , "every" -: time ==> signalOf time

206+ , "fpsWhen" -: signalOf bool ==> number ==> signalOf time

207+-- , "everyWhen" -: signalOf bool ==> time ==> signalOf time

208+ , "before" -: time ==> signalOf bool

209+ , "after" -: time ==> signalOf bool

210+ , "hours" -: number ==> time

211+ , "minutes" -: number ==> time

212+ , "seconds" -: number ==> time

213+ , "millis" -: number ==> time

214+ , "inHours" -: time ==> float

215+ , "inMinutes" -: time ==> float

216+ , "inSeconds" -: time ==> float

217+ , "inMillis" -: time ==> float

218+ , "toDate" -: time ==> date

219+ , "read" -: string ==> maybeOf time

220+ ]

221+

222+dates =

223+ let days = map (-: day) ["Sun", "Mon", "Tue", "Wed", "Thu", "Fri", "Sat"]

224+ months = map (-: month) [ "Jan", "Feb", "Mar", "Apr", "May", "Jun"

225+ , "Jul", "Aug", "Sep", "Oct", "Nov", "Dec" ]

226+ in prefix "Date"

227+ ([ "every" -: time ==> signalOf date

228+ , "read" -: string ==> maybeOf date

229+ , "year" -: date ==> int

230+ , "month" -: date ==> month

231+ , "day" -: date ==> int

232+ , "hour" -: date ==> int

233+ , "minute" -: date ==> int

234+ , "second" -: date ==> int

235+ , "dayOfWeek" -: date ==> day

236+ , "toTime" -: date ==> time

237+ ] ++ days ++ months)

238+

205-------- Math and Binops --------

239-------- Math and Binops --------

206

240

207binop t = t ==> t ==> t

241binop t = t ==> t ==> t

@@ -213,7 +247,6 @@ scheme2 s1 s2 t name =

213 , Context ("`" ++ name ++ "'") $ VarT 1 :<: s2

247 , Context ("`" ++ name ++ "'") $ VarT 1 :<: s2

214 ] (t (VarT 0) (VarT 1)))

248 ] (t (VarT 0) (VarT 1)))

215numScheme t name = scheme1 number t name

249numScheme t name = scheme1 number t name

216−timeScheme name t = scheme1 time t name

217twoNums f name = scheme2 number number f name

250twoNums f name = scheme2 number number f name

218

251

219math =

252math =

@@ -377,5 +410,5 @@ hints = mapM (\(n,s) -> (,) n `liftM` rescheme s) hs

377 where hs = concat [ funcs, lists, signals, math, bools, textAttrs

410 where hs = concat [ funcs, lists, signals, math, bools, textAttrs

378 , graphicsElement, graphicsColor

411 , graphicsElement, graphicsColor

379 , concreteSignals, javascript, json, maybeFuncs

412 , concreteSignals, javascript, json, maybeFuncs

380− , http, dictionary, sets, automaton

413+ , http, dictionary, sets, automaton, times, dates

381 ]

414 ]

elm/src/Types/Solver.hsnew file+157

@@ -0,0 +1,157 @@

2+module Types.Solver (solver) where

4+import Control.Arrow (second)

5+import Control.Monad (liftM)

6+import Data.Either (lefts,rights)

7+import Data.List (foldl')

8+import Data.Maybe (isJust)

9+import qualified Data.Set as Set

10+import qualified Data.Map as Map

11+import Guid

12+import Types.Types

13+import Types.Constrain

14+import Types.Substitutions

15+

16+

17+eq ctx t1 t2 = Context ctx (t1 :=: t2)

18+

19+isSolved ss (Context _ (t1 :=: t2)) = t1 == t2

20+isSolved ss (Context _ (x :<<: _)) = isJust (lookup x ss)

21+isSolved ss c = False

22+

23+crush (Forall xs cs t) =

24+ do subs <- solver cs Map.empty

25+ return $ do ss' <- subs

26+ let ss = Map.toList ss'

27+ cs' = filter (not . isSolved ss) (subst ss cs)

28+ return $ Forall xs cs' (subst ss t)

29+

30+schemeSubHelp ctx x s t1 rltn t2 = do

31+ (t1',cs1) <- sub t1

32+ (t2',cs2) <- sub t2

33+ return (Context ctx (rltn t1' t2') : cs1 ++ cs2)

34+ where sub t | not (occurs x t) = return (t, [])

35+ | otherwise = do (st, cs) <- concretize s

36+ return (subst [(x,st)] t, cs)

37+

38+schemeSub x s c = do s' <- crush s

39+ case s' of

40+ Right s'' -> Right `liftM` schemeSub' x s'' c

41+ Left err -> return $ Left err

42+

43+schemeSub' x s (Context ctx (t1 :=: t2)) = schemeSubHelp ctx x s t1 (:=:) t2

44+schemeSub' x s (Context ctx (t1 :<: t2)) = schemeSubHelp ctx x s t1 (:<:) t2

45+schemeSub' x s c@(Context ctx (y :<<: Forall cxs ccs ctipe))

46+ | not (occurs x c) = return [c]

47+ | otherwise =

48+ do Forall xs cs tipe <- rescheme s

49+ let ss = [(x,tipe)]

50+ constraints = subst ss (cs ++ ccs)

51+ c' = y :<<: Forall (cxs ++ xs) constraints (subst ss ctipe)

52+ return [ Context ctx c' ]

53+

54+

55+solver :: [Context String Constraint]

56+ -> Map.Map X Type

57+ -> GuidCounter (Either String (Map.Map X Type))

58+solver [] subs = return $ Right subs

59+

60+-------- Destruct Type-constructors --------

61+

62+solver ((Context ctx (t1@(ADT n1 ts1) :=: t2@(ADT n2 ts2))) : cs) subs =

63+ if n1 /= n2 then uniError ctx t1 t2 else

64+ solver (zipWith (eq ctx) ts1 ts2 ++ cs) subs

65+solver ((Context ctx (LambdaT t1 t2 :=: LambdaT t1' t2')) : cs) subs =

66+ solver ([ eq ctx t1 t1', eq ctx t2 t2' ] ++ cs) subs

67+

68+-------- Type-equality --------

69+

70+solver (Context ctx (VarT x :=: VarT y) : cs) subs

71+ | x == y = solver cs subs

72+ | otherwise =

73+ case (Map.lookup x subs, Map.lookup y subs) of

74+ (Just (Super xts), Just (Super yts)) ->

75+ let ts = Set.intersection xts yts

76+ setXY t = Map.insert x t . Map.insert y t

77+ in case Set.toList ts of

78+ [] -> unionError ctx xts yts

79+ [t] -> let cs1 = subst [(x,t),(y,t)] cs in

80+ cs1 `seq` solver cs1 (setXY t subs)

81+ _ -> solver cs $ setXY (Super ts) subs

82+ (Just (Super xts), _) ->

83+ let cs2 = subst [(y,VarT x)] cs in

84+ solver cs2 $ Map.insert y (VarT x) subs

85+ (_, _) ->

86+ let cs3 = subst [(x,VarT y)] cs in

87+ solver cs3 $ Map.insert x (VarT y) subs

88+solver (Context ctx (VarT x :=: t) : cs) subs = do

89+ if x `occurs` t then occursError ctx (VarT x) t else

90+ (case Map.lookup x subs of

91+ Nothing -> let cs4 = subst [(x,t)] cs in

92+ solver cs4 . Map.map (subst [(x,t)]) $ Map.insert x t subs

93+ Just (Super ts) ->

94+ let ts' = Set.intersection ts (Set.singleton t) in

95+ case Set.toList ts' of

96+ [] -> solver (Context ctx (t :<: Super ts) : cs) subs

97+ [t'] -> let cs5 = subst [(x,t)] cs in

98+ solver cs5 $ Map.insert x t' subs

99+ _ -> solver cs $ Map.insert x (Super ts') subs

100+ Just t' -> solver (Context ctx (t' :=: t) : cs) subs

101+ )

102+solver ((Context ctx (t :=: VarT x)) : cs) subs =

103+ solver ((Context ctx (VarT x :=: t)) : cs) subs

104+solver ((Context ctx (t1 :=: t2)) : cs) subs

105+ | t1 == t2 = solver cs subs

106+ | otherwise = uniError ctx t1 t2

107+

108+

109+-------- subtypes --------

110+

111+solver (Context ctx (VarT x :<: Super ts) : cs) subs =

112+ case Map.lookup x subs of

113+ Nothing -> solver cs $ Map.insert x (Super ts) subs

114+ Just (Super ts') ->

115+ case Set.toList $ Set.intersection ts ts' of

116+ [] -> unionError ctx ts ts'

117+ [t] -> solver (subst [(x,t)] cs) $ Map.insert x t subs

118+ ts'' -> solver cs $ Map.insert x (Super $ Set.fromList ts'') subs

119+

120+solver (Context ctx (ADT "List" [t] :<: Super ts) : cs) subs

121+ | any f (Set.toList ts) = solver cs subs

122+ | otherwise = subtypeError ctx (ADT "List" [t]) (Super ts)

123+ where f (ADT "List" [VarT _]) = True

124+ f (ADT "List" [t']) = t == t'

125+ f _ = False

126+

127+solver (Context ctx (t :<: Super ts) : cs) subs

128+ | Set.member t ts = solver cs subs

129+ | otherwise = subtypeError ctx t (Super ts)

130+

131+solver (Context ctx (x :<<: s) : cs) subs

132+ | any (occurs x) cs =

133+ do css <- mapM (schemeSub x s) cs

134+ case lefts css of

135+ err : _ -> return $ Left err

136+ [] -> solver (concat (rights css)) subs

137+ | otherwise =

138+ do (t,cs7) <- concretize s

139+ let cs'' = (cs ++ Context ctx (VarT x :=: t) : map (extendCtx ctx) cs7)

140+ solver cs'' subs

141+

142+occursError ctx t1 t2 =

143+ return . Left $ "Type error: Occurs check: cannot construct the infinite type: " ++ show t1 ++

144+ " = " ++ show t2 ++

145+ " in context " ++ ctx

146+uniError ctx t1 t2 =

147+ return . Left $ "Type error: " ++ show t1 ++

148+ " is not equal to " ++ show t2 ++

149+ " in context " ++ ctx

150+unionError ctx ts ts' =

151+ return . Left $ concat [ "Type error: There are no types in both "

152+ , show (Super ts), " and ", show (Super ts')

153+ , " in context ", ctx ]

154+subtypeError ctx t s =

155+ return . Left $ concat [ "Type error: ", show t, " is not a ", show s

156+ , " in context ", ctx ]

157+

elm/src/Types/Substitutions.hs+69−96

@@ -1,10 +1,6 @@

2−module Types.Substitutions (cSub

2+module Types.Substitutions (subst

3− ,tSub

3+ ,occurs

4− ,cSubNoContext

5− ,hasVarC

6− ,freeVars

7− ,schemeSub

8 ,concretize

4 ,concretize

9 ,rescheme

5 ,rescheme

10 ,generalize) where

6 ,generalize) where

@@ -16,106 +12,83 @@ import qualified Data.Set as Set

16import Guid

12import Guid

17import Types.Types

13import Types.Types

19−force x = x `deepseq` x

20−a ++++ b = foldl' (\tl hd -> hd : tl) b a

21−map' f xs = map (\x -> let v = f x in v `seq` v) xs

22−

23−instance (NFData a) => NFData (Context c a) where

24− rnf (Context _ a) = a `deepseq` ()

25−

26−instance NFData Scheme where

27− rnf (Forall vs cs t) = vs `deepseq` cs `deepseq` t `deepseq` ()

28−

29−instance NFData Constraint where

30− rnf (t1 :=: t2) = t1 `deepseq` t2 `deepseq` ()

31− rnf (t1 :<: t2) = t1 `deepseq` t2 `deepseq` ()

32− rnf (t :<<: s) = t `deepseq` s `deepseq` ()

33−

34−instance NFData Type where

35− rnf (LambdaT t1 t2) = t1 `deepseq` t2 `deepseq` ()

36− rnf (ADT _ ts) = foldl' (\acc x -> x `deepseq` acc) () ts

37− rnf t = t `seq` ()

38−

39−tSub k v t@(VarT x) = if k == x then v else t

40−tSub k v (LambdaT t1 t2) = tSub k v t1 `seq` tSub k v t2 `seq` LambdaT (tSub k v t1) (tSub k v t2)

41−tSub k v (ADT name ts) = map' (tSub k v) ts `seq` ADT name (map' (tSub k v) ts)

42−tSub k v (Super ts) = Super ts

43−

44−schemeSubHelp k s c t1 t2 relation = do

45− (t1',cs1) <- f t1

46− (t2',cs2) <- f t2

47− return $ Context c (relation t1' t2') : cs1 ++++ cs2

48− where f t | hasVar k t = do (v, cs) <- concretize s; return (tSub k v t, cs)

49− | otherwise = return (t, [])

50−

51−schemeSub k s (Context ctx (t1 :=: t2)) = t1 `seq` t2 `seq` schemeSubHelp k s ctx t1 t2 (:=:)

52−schemeSub k s (Context ctx (t1 :<: t2)) = t1 `seq` t2 `seq` schemeSubHelp k s ctx t1 t2 (:<:)

53−schemeSub k s c@(Context ctx (x :<<: Forall cxs ccs ctipe)) =

54− if not $ hasVarC k c then return [c]

55− else do

56− Forall xs cs tipe <- rescheme s

57− let constraints = map' (cSub k tipe) $ cs ++ ccs

58− let c' = x :<<: Forall (cxs ++ xs) constraints (tSub k tipe ctipe)

59− return [ Context ctx c' ]

60−

61−hasVar v (VarT x) = v == x

62−hasVar v (LambdaT t1 t2) = force (hasVar v t1 || hasVar v t2)

63−hasVar v (ADT _ ts) = force $ any (hasVar v) ts

64−hasVar v (Super _ ) = False

65−

66−cSub k v (Context ctx c) = out `deepseq` out

67− where out = Context ctx (cSubNoContext' k v c)

68−

69−cSubNoContext k v c = c' `deepseq` c'

70− where c' = cSubNoContext' k v c

71−

72−cSubNoContext' k v (t1 :=: t2) = let { t1' = tSub k v $! t1 ; t2' = tSub k v $! t2 } in

73− t1' `seq` t2' `seq` t1' :=: t2'

74−cSubNoContext' k v (t :<: super) = let t' = tSub k v t in t' `seq` t' :<: super

75−cSubNoContext' k v (x :<<: poly@(Forall vs cs tipe)) = (x :<<: poly')

76− where poly' | k `elem` vs = poly

77− | otherwise = let tipe' = tSub k v tipe in

78− tipe' `deepseq` Forall vs (map' (cSub k v) cs) tipe'

80−concretize (Forall xs cs t) = do

16+class Subst a where

81− pairs <- zip xs `liftM` mapM (const guid) xs

17+ subst :: [(X,Type)] -> a -> a

82− let tipe = foldl' (\t' (k,v) -> tSub k (VarT v) $! t') t pairs

18+

83− let f c = foldl' (\c (k,v) -> cSub k (VarT v) $! c) c $! pairs

19+instance Subst Type where

84− let cs' = f `seq` map' f cs

20+ subst ss (VarT x) = case lookup x ss of

85− tipe `deepseq` cs' `deepseq` return (tipe, cs')

21+ Nothing -> VarT x

22+ Just (Super _) -> VarT x

23+ Just t -> t

24+ subst ss (LambdaT t1 t2) = LambdaT (subst ss t1) (subst ss t2)

25+ subst ss (ADT name ts) = ADT name (subst ss ts)

26+ subst ss (Super ts) = Super ts

27+

28+instance Subst Scheme where

29+ subst ss (Forall vs cs t) = Forall vs (subst ss cs) (subst ss t)

30+

31+instance Subst Constraint where

32+ subst ss (t1 :=: t2) = subst ss t1 :=: subst ss t2

33+ subst ss (t :<: super) = subst ss t :<: super

34+ subst ss (x :<<: poly) = x :<<: subst ss poly

35+

36+instance Subst a => Subst (Context c a) where

37+ subst ss (Context ctx c) = Context ctx (subst ss c)

38+

39+instance Subst a => Subst [a] where

40+ subst ss as = map (subst ss) as

87−rescheme :: Scheme -> GuidCounter Scheme

88−rescheme (Forall xs cs t) = do

89− pairs <- zip xs `liftM` mapM (const guid) xs

90− let tipe = foldl' (\t' (k,v) -> tSub k (VarT v) $! t') t pairs

91− let fs = map (\(k,v) -> cSub k (VarT v)) pairs

92− let cs' = map (\c -> foldl' (\c f -> f $! c) c fs) cs

93− tipe `deepseq` cs' `deepseq` (return $ Forall (map' snd pairs) cs' tipe)

95−freeVars t = let fs = freeVars' t in fs `deepseq` fs

43+class FreeVars a where

44+ freeVars :: a -> [X]

46+instance FreeVars Type where

97−freeVars' (VarT v) = [v]

47+ freeVars (VarT v) = [v]

98−freeVars' (LambdaT t1 t2) = freeVars' t1 ++++ freeVars' t2

48+ freeVars (LambdaT t1 t2) = freeVars t1 ++ freeVars t2

99−freeVars' (ADT _ ts) = concatMap freeVars' ts

49+ freeVars (ADT _ ts) = concatMap freeVars ts

100−freeVars' (Super _ ) = []

50+ freeVars (Super _ ) = []

101

102−cFreeVars c = let fs = cFreeVars' c in fs `deepseq` fs

52+instance FreeVars Constraint where

53+ freeVars (t1 :=: t2) = freeVars t1 ++ freeVars t2

54+ freeVars (t1 :<: t2) = freeVars t1 ++ freeVars t2

55+ freeVars (x :<<: Forall xs cs t) = filter (`notElem` xs) frees

56+ where frees = concatMap freeVars cs ++ freeVars t

103

104−cFreeVars' (t1 :=: t2) = freeVars' t1 ++++ freeVars' t2

58+instance FreeVars a => FreeVars (Context c a) where

105−cFreeVars' (t1 :<: t2) = freeVars' t1 ++++ freeVars' t2

59+ freeVars (Context _ c) = freeVars c

106−cFreeVars' (x :<<: Forall xs cs t) = filter (`notElem` xs) frees

107− where frees = concatMap (\(Context _ c) -> cFreeVars' c) cs ++++ freeVars' t

108

109

110−hasVarC x (Context _ (t1 :=: t2)) = hasVar x t1 || hasVar x t2

62+class Occurs a where

111−hasVarC x (Context _ (t1 :<: t2)) = hasVar x t1 || hasVar x t2

63+ occurs :: X -> a -> Bool

112−hasVarC x (Context _ (y :<<: Forall xs cs t)) = x == y || hasVar x t || inCs

113− where inCs = x `notElem` xs && any (hasVarC x) cs

114

115−decontext (Context _ c) = c

65+instance Occurs Type where

66+ occurs v (VarT x) = v == x

67+ occurs v (LambdaT t1 t2) = occurs v t1 || occurs v t2

68+ occurs v (ADT _ ts) = any (occurs v) ts

69+ occurs v (Super _ ) = False

70+

71+instance Occurs Constraint where

72+ occurs x (t1 :=: t2) = occurs x t1 || occurs x t2

73+ occurs x (t1 :<: t2) = occurs x t1 || occurs x t2

74+ occurs x (y :<<: Forall xs cs t) = x == y || occurs x t || inCs

75+ where inCs = x `notElem` xs && any (occurs x) cs

76+

77+instance Occurs a => Occurs (Context c a) where

78+ occurs x (Context _ c) = occurs x c

79+

80+concretize :: Scheme -> GuidCounter (Type, [Context String Constraint])

81+concretize (Forall xs cs t) = do

82+ ss <- zip xs `liftM` mapM (\_ -> liftM VarT guid) xs

83+ return (subst ss t, subst ss cs)

84+

85+rescheme :: Scheme -> GuidCounter Scheme

86+rescheme (Forall xs cs t) = do

87+ xs' <- mapM (const guid) xs

88+ let ss = zip xs (map VarT xs')

89+ return $ Forall xs' (subst ss cs) (subst ss t)

116

117generalize :: [X] -> Scheme -> GuidCounter Scheme

91generalize :: [X] -> Scheme -> GuidCounter Scheme

118generalize exceptions (Forall xs cs t) = rescheme (Forall (xs ++ frees) cs t)

92generalize exceptions (Forall xs cs t) = rescheme (Forall (xs ++ frees) cs t)

119− where allFrees = Set.fromList $ freeVars t ++ concatMap (cFreeVars . decontext) cs

93+ where allFrees = Set.fromList $ freeVars t ++ concatMap freeVars cs

120 frees = Set.toList $ Set.difference allFrees (Set.fromList exceptions)

94 frees = Set.toList $ Set.difference allFrees (Set.fromList exceptions)

121−

elm/src/Types/Types.hs+5−3

@@ -42,7 +42,10 @@ bool = tipe "Bool"

42string = listOf char -- tipe "String"

43text = tipe "Text"

45−time = Super (Set.fromList [ int, float ])

45+time = tipe "Time"

46+date = tipe "Date"

47+month = tipe "Month"

48+day = tipe "Day"

47element = tipe "Element"

50element = tipe "Element"

48direction = tipe "Direction"

51direction = tipe "Direction"

@@ -60,8 +63,7 @@ maybeOf t = ADT "Maybe" [t]

60pairOf t = tupleOf [t,t]

63pairOf t = tupleOf [t,t]

61point = pairOf int

64point = pairOf int

62appendable t = Super (Set.fromList [ string, text, listOf t ])

65appendable t = Super (Set.fromList [ string, text, listOf t ])

63−comparable = Super (Set.fromList [ int, float, char, string ])

66+comparable = Super (Set.fromList [ int, float, char, string, time, date ])

64−transformable = Super (Set.fromList [ shape, line ])

66jsBool = tipe "JSBool"

68jsBool = tipe "JSBool"

67jsNumber = tipe "JSNumber"

69jsNumber = tipe "JSNumber"

elm/src/Types/Unify.hs+2−113

@@ -1,20 +1,12 @@

2module Types.Unify (unify) where

4−import Control.Arrow (second)

5import Control.Monad (liftM)

4import Control.Monad (liftM)

6−import Data.List (foldl')

7−import qualified Data.Set as Set

8import qualified Data.Map as Map

5import qualified Data.Map as Map

9import Guid

7import Guid

10−import Types.Types

11import Types.Constrain

8import Types.Constrain

12−import Types.Substitutions

9+import Types.Solver

13−

14−import Control.DeepSeq (deepseq)

15−--import System.IO.Unsafe

16−

17−prints xs v = v --} unsafePerformIO (putStrLn "----------" >> mapM print xs) `seq` v

19unify hints modul = run $ do

11unify hints modul = run $ do

20 constraints <- constrain hints modul

12 constraints <- constrain hints modul

@@ -24,106 +16,3 @@ unify hints modul = run $ do

24 do subs <- solver cs Map.empty

16 do subs <- solver cs Map.empty

25 return ((,) escapees `liftM` subs)

17 return ((,) escapees `liftM` subs)

27−eq ctx t1 t2 = Context ctx (t1 :=: t2)

28−

29−

30−solver [] subs = prints (Map.toList subs) $ return $ Right subs

31−

32−-------- Destruct Type-constructors --------

33−

34−solver ((Context ctx (t1@(ADT n1 ts1) :=: t2@(ADT n2 ts2))) : cs) subs =

35− if n1 /= n2 then uniError ctx t1 t2 else

36− solver (zipWith (eq ctx) ts1 ts2 ++ cs) subs

37−solver ((Context ctx (LambdaT t1 t2 :=: LambdaT t1' t2')) : cs) subs =

38− solver ([ eq ctx t1 t1', eq ctx t2 t2' ] ++ cs) subs

39−

40−-------- Type-equality --------

41−

42−solver (Context ctx (VarT x :=: VarT y) : cs) subs

43− | x == y = solver cs subs

44− | otherwise =

45− case (Map.lookup x subs, Map.lookup y subs) of

46− (Just (Super xts), Just (Super yts)) ->

47− let ts = Set.intersection xts yts

48− setXY t = Map.insert x t . Map.insert y t

49− in case Set.toList ts of

50− [] -> unionError ctx xts yts

51− [t] -> let cs1 = map (\c -> cSub y t c `seq` cSub x t (cSub y t c)) cs in

52− cs1 `seq` solver cs1 (setXY t subs)

53− _ -> solver cs $ setXY (Super ts) subs

54− (Just (Super xts), _) ->

55− let cs2 = map (cSub y (VarT x)) cs in

56− cs2 `seq` solver cs2 $ Map.insert y (VarT x) subs

57− (_, _) ->

58− let cs3 = map (cSub x (VarT y)) cs in

59− cs3 `deepseq` solver cs3 $ Map.insert x (VarT y) subs

60−solver (Context ctx (VarT x :=: t) : cs) subs = do

61− if x `occursIn` t then occursError ctx (VarT x) t else

62− (case Map.lookup x subs of

63− Nothing -> let cs4 = map (cSub x t) cs in

64− cs4 `deepseq` (solver cs4 . Map.map (tSub x t) $ Map.insert x t subs)

65− Just (Super ts) ->

66− let ts' = Set.intersection ts (Set.singleton t) in

67− case Set.toList ts' of

68− [] -> solver (Context ctx (t :<: Super ts) : cs) subs

69− [t'] -> let cs5 = map (cSub x t) cs in

70− cs5 `seq` solver cs5 $ Map.insert x t' subs

71− _ -> solver cs $ Map.insert x (Super ts') subs

72− Just t' -> solver (Context ctx (t' :=: t) : cs) subs

73− )

74−solver ((Context ctx (t :=: VarT x)) : cs) subs =

75− solver ((Context ctx (VarT x :=: t)) : cs) subs

76−solver ((Context ctx (t1 :=: t2)) : cs) subs

77− | t1 == t2 = solver cs subs

78− | otherwise = uniError ctx t1 t2

79−

80−

81−-------- subtypes --------

82−

83−solver (Context ctx (VarT x :<: Super ts) : cs) subs =

84− case Map.lookup x subs of

85− Nothing -> solver cs $ Map.insert x (Super ts) subs

86− Just (Super ts') ->

87− case Set.toList $ Set.intersection ts ts' of

88− [] -> unionError ctx ts ts'

89− [t] -> solver (map (cSub x t) cs) $ Map.insert x t subs

90− ts'' -> solver cs $ Map.insert x (Super $ Set.fromList ts'') subs

91−

92−solver (Context ctx (ADT "List" [t] :<: Super ts) : cs) subs

93− | any f (Set.toList ts) = solver cs subs

94− | otherwise = subtypeError ctx (ADT "List" [t]) (Super ts)

95− where f (ADT "List" [VarT _]) = True

96− f (ADT "List" [t']) = t == t'

97− f _ = False

98−

99−solver (Context ctx (t :<: Super ts) : cs) subs

100− | Set.member t ts = solver cs subs

101− | otherwise = subtypeError ctx t (Super ts)

102−

103−solver (Context ctx (x :<<: s) : cs) subs

104− | any (hasVarC x) cs =

105− do cs6 <- concat `liftM` mapM (schemeSub x s) cs

106− solver cs6 subs

107− | otherwise =

108− do (t,cs7) <- concretize s

109− let cs'' = (cs ++ Context ctx (VarT x :=: t) : map (extendCtx ctx) cs7)

110− solver cs'' subs

111−

112−

113−occursError ctx t1 t2 =

114− return . Left $ "Type error: Occurs check: cannot construct the infinite type: " ++ show t1 ++

115− " = " ++ show t2 ++

116− " in context " ++ ctx

117−uniError ctx t1 t2 =

118− return . Left $ "Type error: " ++ show t1 ++

119− " is not equal to " ++ show t2 ++

120− " in context " ++ ctx

121−unionError ctx ts ts' =

122− return . Left $ concat [ "Type error: There are no types in both "

123− , show (Super ts), " and ", show (Super ts')

124− , " in context ", ctx ]

125−subtypeError ctx t s =

126− return . Left $ concat [ "Type error: ", show t, " is not a ", show s

127− , " in context ", ctx ]

128−

129−occursIn x t = x `elem` freeVars t