@@ -17,6 +17,19 @@ import qualified AST.Type as T
1717import qualified AST.Variable as Var
1818
1919
20+-- CONCRETE TYPES
21+
22+type Type = TermN Variable
23+
24+type Variable = UF.Point Descriptor
25+
26+type TypeConstraint = Constraint Type Variable
27+
28+type TypeScheme = Scheme Type Variable
29+
30+
31+-- TYPE PRIMITIVES
32+
2033data Term1 a
2134 = App1 a a
2235 | Fun1 a a
@@ -26,82 +39,26 @@ data Term1 a
2639
2740
2841data TermN a
29− = VarN (Maybe Var.Canonical) a
42+ = VarN (Maybe Var.Canonical) a
3043 | TermN (Maybe Var.Canonical) (Term1 (TermN a))
3144
3245
3346varN :: a -> TermN a
34−varN = VarN Nothing
47+varN =
48+ VarN Nothing
3549
3650
3751termN :: (Term1 (TermN a)) -> TermN a
38−termN = TermN Nothing
52+termN =
53+ TermN Nothing
3954
4055
4156record :: Map.Map String [TermN a] -> TermN a -> TermN a
42−record fs rec = termN (Record1 fs rec)
43−
44−
45−type Type = TermN Variable
46−
47−
48−type Variable = UF.Point Descriptor
49−
50−
51−type SchemeName = String
52−
53−
54−type TypeName = Var.Canonical
55−
56−
57−type Constraint a b = Located (BasicConstraint a b)
58−
59−
60−data BasicConstraint a b
61− = CTrue
62− | CSaveEnv
63− | CEqual a a
64− | CAnd [Constraint a b]
65− | CLet [Scheme a b] (Constraint a b)
66− | CInstance SchemeName a
67−
68−
69−data Scheme a b = Scheme
70− { rigidQuantifiers :: [b]
71− , flexibleQuantifiers :: [b]
72− , constraint :: Constraint a b
73− , header :: Map.Map String a
74− }
75−
76−
77−type TypeConstraint = Constraint Type Variable
78−
79−type TypeScheme = Scheme Type Variable
80−
81−
82−monoscheme :: Map.Map String a -> Scheme a b
83−monoscheme headers = Scheme [] [] (noneNoDocs CTrue) headers
84−
85−
86−infixl 8 /\
87−
88−(/\) :: Constraint a b -> Constraint a b -> Constraint a b
89−a@(A _ c1) /\ b@(A _ c2) =
90− case (c1, c2) of
91− (CTrue, _) -> b
92− (_, CTrue) -> a
93− _ -> mergeOldDocs a b (CAnd [a,b])
94−
95−
96−infixr 9 ==>
97−
98−(==>) :: Type -> Type -> Type
99−a ==> b = termN (Fun1 a b)
100−
57+record fs rec =
58+ termN (Record1 fs rec)
10159
102−(<|) :: TermN a -> TermN a -> TermN a
103−f <| a = termN (App1 f a)
10460
61+-- DESCRIPTORS
10562
10663data Descriptor = Descriptor
10764 { structure :: Maybe (Term1 Variable)
@@ -113,23 +70,18 @@ data Descriptor = Descriptor
11370 , alias :: Maybe Var.Canonical
11471 }
11572
116−
11773noRank :: Int
11874noRank = -1
11975
120−
12176outermostRank :: Int
12277outermostRank = 0
12378
124−
12579noMark :: Int
12680noMark = 0
12781
128−
12982initialMark :: Int
13083initialMark = 1
13184
132−
13385data Flex
13486 = Rigid
13587 | Flexible
@@ -137,7 +89,6 @@ data Flex
13789 | Is SuperType
13890 deriving (Eq)
13991
140−
14192data SuperType
14293 = Number
14394 | Comparable
@@ -145,6 +96,47 @@ data SuperType
14596 deriving (Eq)
14697
14798
99+-- CONSTRAINTS
100+
101+type Constraint a b =
102+ Located (BasicConstraint a b)
103+
104+data BasicConstraint a b
105+ = CTrue
106+ | CSaveEnv
107+ | CEqual a a
108+ | CAnd [Constraint a b]
109+ | CLet [Scheme a b] (Constraint a b)
110+ | CInstance SchemeName a
111+
112+type SchemeName = String
113+
114+type TypeName = Var.Canonical
115+
116+data Scheme a b = Scheme
117+ { rigidQuantifiers :: [b]
118+ , flexibleQuantifiers :: [b]
119+ , constraint :: Constraint a b
120+ , header :: Map.Map String a
121+ }
122+
123+
124+-- TYPE HELPERS
125+
126+infixr 9 ==>
127+
128+(==>) :: Type -> Type -> Type
129+(==>) a b =
130+ termN (Fun1 a b)
131+
132+
133+(<|) :: TermN a -> TermN a -> TermN a
134+(<|) f a =
135+ termN (App1 f a)
136+
137+
138+-- VARIABLE HELPERS
139+
148140namedVar :: Flex -> Var.Canonical -> IO Variable
149141namedVar flex name = UF.fresh $ Descriptor
150142 { structure = Nothing
@@ -169,6 +161,23 @@ variable flex = UF.fresh $ Descriptor
169161 }
170162
171163
164+-- CONSTRAINT HELPERS
165+
166+monoscheme :: Map.Map String a -> Scheme a b
167+monoscheme headers =
168+ Scheme [] [] (noneNoDocs CTrue) headers
169+
170+
171+infixl 8 /\
172+
173+(/\) :: Constraint a b -> Constraint a b -> Constraint a b
174+(/\) a@(A _ c1) b@(A _ c2) =
175+ case (c1, c2) of
176+ (CTrue, _) -> b
177+ (_, CTrue) -> a
178+ _ -> mergeOldDocs a b (CAnd [a,b])
179+
180+
172181-- ex qs constraint == exists qs. constraint
173182ex :: [Variable] -> TypeConstraint -> TypeConstraint
174183ex fqs constraint@(A ann _) =
@@ -213,36 +222,51 @@ instance PrettyType a => PrettyType (Term1 a) where
213222 parensIf needed (px <+> pretty App x)
214223 where
215224 px = prty f
216− needed = case when of
217− App -> True
218− _ -> False
225+ needed =
226+ case when of
227+ App -> True
228+ _ -> False
219229
220230 Fun1 arg body ->
221231 parensIf needed (pretty Fn arg <+> P.text "->" <+> prty body)
222232 where
223− needed = case when of
224− Never -> False
225− _ -> True
233+ needed =
234+ case when of
235+ Never -> False
236+ _ -> True
226237
227− Var1 x -> prty x
238+ Var1 x ->
239+ prty x
228240
229− EmptyRecord1 -> P.braces P.empty
241+ EmptyRecord1 ->
242+ P.braces P.empty
230243
231244 Record1 fields ext ->
232245 P.braces (extend <+> commaSep prettyFields)
233246 where
234247 prettyExt = prty ext
235− extend | P.render prettyExt == "{}" = P.empty
236− | otherwise = prettyExt <+> P.text "|"
237− mkPretty f t = P.text f <+> P.text ":" <+> prty t
238− prettyFields = concatMap (\(f,ts) -> map (mkPretty f) ts) (Map.toList fields)
248+
249+ extend
250+ | P.render prettyExt == "{}" =
251+ P.empty
252+ | otherwise =
253+ prettyExt <+> P.text "|"
254+
255+ mkPretty f t =
256+ P.text f <+> P.text ":" <+> prty t
257+
258+ prettyFields =
259+ concatMap (\(f,ts) -> map (mkPretty f) ts) (Map.toList fields)
239260
240261
241262instance PrettyType a => PrettyType (TermN a) where
242263 pretty when term =
243264 case term of
244− VarN alias x -> either alias (pretty when x)
245− TermN alias t1 -> either alias (pretty when t1)
265+ VarN alias x ->
266+ either alias (pretty when x)
267+
268+ TermN alias t1 ->
269+ either alias (pretty when t1)
246270 where
247271 either maybeAlias doc =
248272 case maybeAlias of
@@ -251,16 +275,20 @@ instance PrettyType a => PrettyType (TermN a) where
251275
252276
253277instance PrettyType Descriptor where
254− pretty when desc = do
278+ pretty when desc =
255279 case (alias desc, structure desc, name desc) of
256− (Just name, _, _) -> PP.pretty name
257− (_, Just term, _) -> pretty when term
280+ (Just name, _, _) ->
281+ PP.pretty name
282+
283+ (_, Just term, _) ->
284+ pretty when term
285+
258286 (_, _, Just name)
259287 | Var.isTuple name ->
260288 P.parens . P.text $ replicate (read (drop 6 (Var.toString name)) - 1) ','
261289 | otherwise ->
262290 P.text (Var.toString name)
263−
291+
264292 _ -> P.text "?"
265293
266294
@@ -320,20 +348,27 @@ instance (PrettyType a, PrettyType b) => PrettyType (Scheme a b) where
320348
321349
322350extraPretty :: (PrettyType t, Crawl t) => t -> IO Doc
323−extraPretty t = pretty Never <$> addNames t
351+extraPretty t =
352+ pretty Never <$> addNames t
324353
325354
326355-- ADDING NAMES TO TYPES
327356
328357addNames :: (Crawl t) => t -> IO t
329−addNames value = do
330− (rawVars, _, _, _) <- execStateT (crawl getNames value) ([], 0, 0, 0)
331− let vars = map head . List.group $ List.sort rawVars
332− suffix s = map (++s) (map (:[]) ['a'..'z'])
333− allVars = concatMap suffix $ ["","'","_"] ++ map show [ (0 :: Int) .. ]
334− okayVars = filter (`notElem` vars) allVars
335− runStateT (crawl rename value) (okayVars, 0, 0, 0)
336− return value
358+addNames value =
359+ do (rawVars, _, _, _) <- execStateT (crawl getNames value) ([], 0, 0, 0)
360+
361+ let vars = map head . List.group $ List.sort rawVars
362+
363+ let suffix s = map (++s) (map (:[]) ['a'..'z'])
364+
365+ let allVars = concatMap suffix $ ["","'","_"] ++ map show [ (0 :: Int) .. ]
366+
367+ let okayVars = filter (`notElem` vars) allVars
368+
369+ runStateT (crawl rename value) (okayVars, 0, 0, 0)
370+
371+ return value
337372 where
338373 getNames desc state@(vars, a, b, c) =
339374 let name' = name desc in
@@ -368,23 +403,25 @@ class Crawl t where
368403
369404
370405instance Crawl e => Crawl (Annotated a e) where
371− crawl nextState (A ann e) = A ann <$> crawl nextState e
406+ crawl nextState (A ann e) =
407+ A ann <$> crawl nextState e
372408
373409
374410instance (Crawl t, Crawl v) => Crawl (BasicConstraint t v) where
375− crawl nextState constraint =
411+ crawl nextState constraint =
376412 let rnm = crawl nextState in
377413 case constraint of
378414 CTrue -> return CTrue
379415 CSaveEnv -> return CSaveEnv
380416 CEqual a b -> CEqual <$> rnm a <*> rnm b
381417 CAnd cs -> CAnd <$> crawl nextState cs
382− CLet schemes c -> CLet <$> crawl nextState schemes <*> crawl nextState c
418+ CLet schemes c -> CLet <$> crawl nextState schemes <*> crawl nextState c
383419 CInstance name tipe -> CInstance name <$> rnm tipe
384420
385421
386422instance Crawl a => Crawl [a] where
387− crawl nextState list = mapM (crawl nextState) list
423+ crawl nextState list =
424+ mapM (crawl nextState) list
388425
389426
390427instance (Crawl t, Crawl v) => Crawl (Scheme t v) where
@@ -410,14 +447,24 @@ instance Crawl t => Crawl (TermN t) where
410447
411448instance Crawl t => Crawl (Term1 t) where
412449 crawl nextState term =
413− let rnm = crawl nextState in
414− case term of
415− App1 a b -> App1 <$> rnm a <*> rnm b
416− Fun1 a b -> Fun1 <$> rnm a <*> rnm b
417− Var1 a -> Var1 <$> rnm a
418− EmptyRecord1 -> return EmptyRecord1
450+ let rnm = crawl nextState in
451+ case term of
452+ App1 a b ->
453+ App1 <$> rnm a <*> rnm b
454+
455+ Fun1 a b ->
456+ Fun1 <$> rnm a <*> rnm b
457+
458+ Var1 a ->
459+ Var1 <$> rnm a
460+
461+ EmptyRecord1 ->
462+ return EmptyRecord1
463+
419464 Record1 fields ext ->
420− Record1 <$> traverse (mapM rnm) fields <*> rnm ext
465+ Record1
466+ <$> traverse (mapM rnm) fields
467+ <*> rnm ext
421468
422469
423470instance Crawl a => Crawl (UF.Point a) where
@@ -436,7 +483,7 @@ instance Crawl Descriptor where
436483 put state'
437484 return $ desc { name = name', structure = structure' }
438485
439−
486+
440487toSrcType :: Variable -> IO T.CanonicalType
441488toSrcType var =
442489 go =<< addNames var
@@ -446,40 +493,53 @@ toSrcType var =
446493 srcType <- maybe (backupSrcType desc) termToSrcType (structure desc)
447494 return $ maybe srcType (\name -> T.Aliased name srcType) (alias desc)
448495
449− backupSrcType desc =
496+ backupSrcType :: Descriptor -> IO T.CanonicalType
497+ backupSrcType desc =
450498 case name desc of
451499 Just v@(Var.Canonical _ x@(c:_))
452− | Char.isLower c -> return (T.Var x)
453− | otherwise -> return $ T.Type v
454−
455− _ -> error $ concat
456− [ "Problem converting the following type "
457− , "from a type-checker type to a source-syntax type:"
458− , P.render (pretty Never var) ]
459−
500+ | Char.isLower c ->
501+ return (T.Var x)
502+ | otherwise ->
503+ return $ T.Type v
504+
505+ _ ->
506+ error $
507+ concat
508+ [ "Problem converting the following type "
509+ , "from a type-checker type to a source-syntax type:"
510+ , P.render (pretty Never var)
511+ ]
512+
513+ termToSrcType :: Term1 Variable -> IO T.CanonicalType
460514 termToSrcType term =
461515 case term of
462− App1 a b -> do
463− a' <- go a
464− b' <- go b
465− case a' of
466− T.App f args -> return $ T.App f (args ++ [b'])
467− _ -> return $ T.App a' [b']
468−
469− Fun1 a b -> T.Lambda <$> go a <*> go b
470−
471− Var1 a -> go a
472−
473− EmptyRecord1 -> return $ T.Record [] Nothing
474−
475− Record1 tfields extension -> do
476− fields' <- traverse (mapM go) tfields
477− let fields = concat [ map ((,) name) ts | (name,ts) <- Map.toList fields' ]
478− ext' <- dealias <$> go extension
479− return $ case ext' of
480− T.Record fs ext -> T.Record (fs ++ fields) ext
481− T.Var _ -> T.Record fields (Just ext')
482− _ -> error "Used toSrcType on a type that is not well-formed"
516+ App1 a b ->
517+ do a' <- go a
518+ b' <- go b
519+ case a' of
520+ T.App f args ->
521+ return $ T.App f (args ++ [b'])
522+ _ ->
523+ return $ T.App a' [b']
524+
525+ Fun1 a b ->
526+ T.Lambda <$> go a <*> go b
527+
528+ Var1 a ->
529+ go a
530+
531+ EmptyRecord1 ->
532+ return $ T.Record [] Nothing
533+
534+ Record1 tfields extension ->
535+ do fields' <- traverse (mapM go) tfields
536+ let fields = concat [ map ((,) name) ts | (name,ts) <- Map.toList fields' ]
537+ ext' <- dealias <$> go extension
538+ return $
539+ case ext' of
540+ T.Record fs ext -> T.Record (fs ++ fields) ext
541+ T.Var _ -> T.Record fields (Just ext')
542+ _ -> error "Used toSrcType on a type that is not well-formed"
483543
484544 dealias :: T.CanonicalType -> T.CanonicalType
485545 dealias t =
@@ -488,11 +548,15 @@ toSrcType var =
488548 _ -> t
489549
490550
491−data AppStructure = List Variable | Tuple [Variable] | Other
551+data AppStructure
552+ = List Variable
553+ | Tuple [Variable]
554+ | Other
492555
493556
494557collectApps :: Variable -> IO AppStructure
495−collectApps var = go [] var
558+collectApps var =
559+ go [] var
496560 where
497561 go vars var = do
498562 desc <- UF.descriptor var