@@ -16,6 +16,7 @@ import qualified AST.PrettyPrint as PP
1616import qualified AST.Type as T
1717import qualified AST.Variable as Var
1818
19+
1920data Term1 a
2021 = App1 a a
2122 | Fun1 a a
@@ -24,27 +25,40 @@ data Term1 a
2425 | Record1 (Map.Map String [a]) a
2526 deriving Show
2627
28+
2729data TermN a
2830 = VarN (Maybe Var.Canonical) a
2931 | TermN (Maybe Var.Canonical) (Term1 (TermN a))
3032 deriving Show
3133
34+
3235varN :: a -> TermN a
3336varN = VarN Nothing
3437
38+
3539termN :: (Term1 (TermN a)) -> TermN a
3640termN = TermN Nothing
3741
42+
3843record :: Map.Map String [TermN a] -> TermN a -> TermN a
3944record fs rec = termN (Record1 fs rec)
4045
46+
4147type Type = TermN Variable
48+
49+
4250type Variable = UF.Point Descriptor
4351
52+
4453type SchemeName = String
54+
55+
4556type TypeName = Var.Canonical
4657
58+
4759type Constraint a b = Located (BasicConstraint a b)
60+
61+
4862data BasicConstraint a b
4963 = CTrue
5064 | CSaveEnv
@@ -54,19 +68,25 @@ data BasicConstraint a b
5468 | CInstance SchemeName a
5569 deriving Show
5670
57−data Scheme a b = Scheme {
58− rigidQuantifiers :: [b],
59− flexibleQuantifiers :: [b],
60− constraint :: Constraint a b,
61− header :: Map.Map String a
62−} deriving Show
71+
72+data Scheme a b = Scheme
73+ { rigidQuantifiers :: [b]
74+ , flexibleQuantifiers :: [b]
75+ , constraint :: Constraint a b
76+ , header :: Map.Map String a
77+ }
78+ deriving Show
79+
6380
6481type TypeConstraint = Constraint Type Variable
82+
6583type TypeScheme = Scheme Type Variable
6684
85+
6786monoscheme :: Map.Map String a -> Scheme a b
6887monoscheme headers = Scheme [] [] (noneNoDocs CTrue) headers
6988
89+
7090infixl 8 /\
7191
7292(/\) :: Constraint a b -> Constraint a b -> Constraint a b
@@ -76,13 +96,17 @@ a@(A _ c1) /\ b@(A _ c2) =
7696 (_, CTrue) -> a
7797 _ -> mergeOldDocs a b (CAnd [a,b])
7898
99+
79100infixr 9 ==>
101+
80102(==>) :: Type -> Type -> Type
81103a ==> b = termN (Fun1 a b)
82104
105+
83106(<|) :: TermN a -> TermN a -> TermN a
84107f <| a = termN (App1 f a)
85108
109+
86110data Descriptor = Descriptor
87111 { structure :: Maybe (Term1 Variable)
88112 , rank :: Int
@@ -91,25 +115,40 @@ data Descriptor = Descriptor
91115 , copy :: Maybe Variable
92116 , mark :: Int
93117 , alias :: Maybe Var.Canonical
94− } deriving Show
118+ }
119+ deriving Show
120+
95121
96122noRank :: Int
97123noRank = -1
98124
125+
99126outermostRank :: Int
100127outermostRank = 0
101128
129+
102130noMark :: Int
103131noMark = 0
104132
133+
105134initialMark :: Int
106135initialMark = 1
107136
108−data Flex = Rigid | Flexible | Constant | Is SuperType
109− deriving (Show, Eq)
110137
111−data SuperType = Number | Comparable | Appendable
112− deriving (Show, Eq)
138+data Flex
139+ = Rigid
140+ | Flexible
141+ | Constant
142+ | Is SuperType
143+ deriving (Show, Eq)
144+
145+
146+data SuperType
147+ = Number
148+ | Comparable
149+ | Appendable
150+ deriving (Show, Eq)
151+
113152
114153namedVar :: Flex -> Var.Canonical -> IO Variable
115154namedVar flex name = UF.fresh $ Descriptor
@@ -122,6 +161,7 @@ namedVar flex name = UF.fresh $ Descriptor
122161 , alias = Nothing
123162 }
124163
164+
125165variable :: Flex -> IO Variable
126166variable flex = UF.fresh $ Descriptor
127167 { structure = Nothing
@@ -139,32 +179,40 @@ ex :: [Variable] -> TypeConstraint -> TypeConstraint
139179ex fqs constraint@(A ann _) =
140180 A ann $ CLet [Scheme [] fqs constraint Map.empty] (A ann CTrue)
141181
182+
142183-- fl qs constraint == forall qs. constraint
143184fl :: [Variable] -> TypeConstraint -> TypeConstraint
144185fl rqs constraint@(A ann _) =
145186 A ann $ CLet [Scheme rqs [] constraint Map.empty] (A ann CTrue)
146187
188+
147189exists :: Error e => (Type -> ErrorT e IO TypeConstraint) -> ErrorT e IO TypeConstraint
148−exists f = do
149− v <- liftIO $ variable Flexible
150− ex [v] <$> f (varN v)
190+exists f =
191+ do v <- liftIO $ variable Flexible
192+ ex [v] <$> f (varN v)
193+
151194
152195existsNumber :: Error e => (Type -> ErrorT e IO TypeConstraint) -> ErrorT e IO TypeConstraint
153−existsNumber f = do
154− v <- liftIO $ variable (Is Number)
155− ex [v] <$> f (varN v)
196+existsNumber f =
197+ do v <- liftIO $ variable (Is Number)
198+ ex [v] <$> f (varN v)
199+
156200
201+-- TYPES TO PRETTY STRINGS
157202
158203instance Show a => Show (UF.Point a) where
159− show point = unsafePerformIO $ fmap show (UF.descriptor point)
204+ show point =
205+ unsafePerformIO $ fmap show (UF.descriptor point)
160206
161207
162208instance PrettyType a => PrettyType (UF.Point a) where
163− pretty when point = unsafePerformIO $ fmap (pretty when) (UF.descriptor point)
209+ pretty when point =
210+ unsafePerformIO $ fmap (pretty when) (UF.descriptor point)
164211
165212
166213instance PrettyType t => PrettyType (Annotated a t) where
167− pretty when (A _ e) = pretty when e
214+ pretty when (A _ e) =
215+ pretty when e
168216
169217
170218instance PrettyType a => PrettyType (Term1 a) where
@@ -190,7 +238,8 @@ instance PrettyType a => PrettyType (Term1 a) where
190238
191239 EmptyRecord1 -> P.braces P.empty
192240
193− Record1 fields ext -> P.braces (extend <+> commaSep prettyFields)
241+ Record1 fields ext ->
242+ P.braces (extend <+> commaSep prettyFields)
194243 where
195244 prettyExt = prty ext
196245 extend | P.render prettyExt == "{}" = P.empty
@@ -210,6 +259,7 @@ instance PrettyType a => PrettyType (TermN a) where
210259 Just alias -> PP.pretty alias
211260 Nothing -> doc
212261
262+
213263instance PrettyType Descriptor where
214264 pretty when desc = do
215265 case (alias desc, structure desc, name desc) of
@@ -256,6 +306,7 @@ instance (PrettyType a, PrettyType b) => PrettyType (BasicConstraint a b) where
256306 CInstance name tipe ->
257307 P.text name <+> P.text "<" <+> prty tipe
258308
309+
259310instance (PrettyType a, PrettyType b) => PrettyType (Scheme a b) where
260311 pretty _ (Scheme rqs fqs (A _ constraint) headers) =
261312 P.sep [ forall, cs, headers' ]
@@ -281,6 +332,9 @@ instance (PrettyType a, PrettyType b) => PrettyType (Scheme a b) where
281332extraPretty :: (PrettyType t, Crawl t) => t -> IO Doc
282333extraPretty t = pretty Never <$> addNames t
283334
335+
336+-- ADDING NAMES TO TYPES
337+
284338addNames :: (Crawl t) => t -> IO t
285339addNames value = do
286340 (rawVars, _, _, _) <- execStateT (crawl getNames value) ([], 0, 0, 0)
@@ -309,8 +363,12 @@ addNames value = do
309363 where
310364 local v = Just (Var.local v)
311365
366+
367+-- CRAWLING OVER TYPES
368+
312369type CrawlState = ([String], Int, Int, Int)
313370
371+
314372-- Code for traversing all the type data-structures and giving
315373-- names to the variables embedded deep in there.
316374class Crawl t where
@@ -318,9 +376,11 @@ class Crawl t where
318376 -> t
319377 -> StateT CrawlState IO t
320378
379+
321380instance Crawl e => Crawl (Annotated a e) where
322381 crawl nextState (A ann e) = A ann <$> crawl nextState e
323382
383+
324384instance (Crawl t, Crawl v) => Crawl (BasicConstraint t v) where
325385 crawl nextState constraint =
326386 let rnm = crawl nextState in
@@ -332,19 +392,31 @@ instance (Crawl t, Crawl v) => Crawl (BasicConstraint t v) where
332392 CLet schemes c -> CLet <$> crawl nextState schemes <*> crawl nextState c
333393 CInstance name tipe -> CInstance name <$> rnm tipe
334394
395+
335396instance Crawl a => Crawl [a] where
336397 crawl nextState list = mapM (crawl nextState) list
337398
399+
338400instance (Crawl t, Crawl v) => Crawl (Scheme t v) where
339401 crawl nextState (Scheme rqs fqs c headers) =
340− let rnm = crawl nextState in
341− Scheme <$> rnm rqs <*> rnm fqs <*> crawl nextState c <*> return headers
402+ let rnm = crawl nextState
403+ in
404+ Scheme
405+ <$> rnm rqs
406+ <*> rnm fqs
407+ <*> crawl nextState c
408+ <*> return headers
409+
342410
343411instance Crawl t => Crawl (TermN t) where
344412 crawl nextState tipe =
345413 case tipe of
346− VarN a x -> VarN a <$> crawl nextState x
347− TermN a term -> TermN a <$> crawl nextState term
414+ VarN a x ->
415+ VarN a <$> crawl nextState x
416+
417+ TermN a term ->
418+ TermN a <$> crawl nextState term
419+
348420
349421instance Crawl t => Crawl (Term1 t) where
350422 crawl nextState term =
@@ -357,30 +429,32 @@ instance Crawl t => Crawl (Term1 t) where
357429 Record1 fields ext ->
358430 Record1 <$> traverse (mapM rnm) fields <*> rnm ext
359431
432+
360433instance Crawl a => Crawl (UF.Point a) where
361− crawl nextState point = do
362− desc <- liftIO $ UF.descriptor point
363− desc' <- crawl nextState desc
364− liftIO $ UF.setDescriptor point desc'
365− return point
434+ crawl nextState point =
435+ do desc <- liftIO $ UF.descriptor point
436+ desc' <- crawl nextState desc
437+ liftIO $ UF.setDescriptor point desc'
438+ return point
439+
366440
367441instance Crawl Descriptor where
368− crawl nextState desc = do
369− state <- get
370− let (name', state') = nextState desc state
371− structure' <- traverse (crawl nextState) (structure desc)
372− put state'
373− return $ desc { name = name', structure = structure' }
442+ crawl nextState desc =
443+ do state <- get
444+ let (name', state') = nextState desc state
445+ structure' <- traverse (crawl nextState) (structure desc)
446+ put state'
447+ return $ desc { name = name', structure = structure' }
374448
375449
376450toSrcType :: Variable -> IO T.CanonicalType
377451toSrcType var =
378452 go =<< addNames var
379453 where
380− go v = do
381− desc <- UF.descriptor v
382− srcType <- maybe (backupSrcType desc) termToSrcType (structure desc)
383− return $ maybe srcType (\name -> T.Aliased name srcType) (alias desc)
454+ go v =
455+ do desc <- UF.descriptor v
456+ srcType <- maybe (backupSrcType desc) termToSrcType (structure desc)
457+ return $ maybe srcType (\name -> T.Aliased name srcType) (alias desc)
384458
385459 backupSrcType desc =
386460 case name desc of
@@ -426,18 +500,24 @@ toSrcType var =
426500
427501data AppStructure = List Variable | Tuple [Variable] | Other
428502
503+
429504collectApps :: Variable -> IO AppStructure
430505collectApps var = go [] var
431506 where
432507 go vars var = do
433508 desc <- UF.descriptor var
434509 case (structure desc, vars) of
435− (Nothing, [v]) -> case name desc of
436− Just n | Var.isList n -> return (List v)
437− _ -> return Other
438− (Nothing, vs) -> case name desc of
439− Just n | Var.isTuple n -> return (Tuple vs)
440− _ -> return Other
441− (Just term, _) -> case term of
442− App1 a b -> go (vars ++ [b]) a
443− _ -> return Other
510+ (Nothing, [v]) ->
511+ case name desc of
512+ Just n | Var.isList n -> return (List v)
513+ _ -> return Other
514+
515+ (Nothing, vs) ->
516+ case name desc of
517+ Just n | Var.isTuple n -> return (Tuple vs)
518+ _ -> return Other
519+
520+ (Just term, _) ->
521+ case term of
522+ App1 a b -> go (vars ++ [b]) a
523+ _ -> return Other