summaryrefslogtreecommitdiff
path: root/Type.hs
diff options
context:
space:
mode:
Diffstat (limited to 'Type.hs')
-rw-r--r--Type.hs1707
1 files changed, 0 insertions, 1707 deletions
diff --git a/Type.hs b/Type.hs
deleted file mode 100644
index af0a1206..00000000
--- a/Type.hs
+++ /dev/null
@@ -1,1707 +0,0 @@
1{-# LANGUAGE OverloadedStrings #-}
2{-# LANGUAGE LambdaCase #-}
3{-# LANGUAGE PatternSynonyms #-}
4{-# LANGUAGE DeriveFunctor #-}
5{-# LANGUAGE DeriveFoldable #-}
6{-# LANGUAGE DeriveTraversable #-}
7{-# LANGUAGE GeneralizedNewtypeDeriving #-}
8{-# LANGUAGE NoMonomorphismRestriction #-}
9{-# LANGUAGE TypeSynonymInstances #-}
10{-# LANGUAGE FlexibleInstances #-}
11{-# LANGUAGE FlexibleContexts #-}
12{-# LANGUAGE MultiParamTypeClasses #-}
13{-# LANGUAGE StandaloneDeriving #-}
14{-# LANGUAGE ViewPatterns #-}
15{-# LANGUAGE TypeFamilies #-}
16{-# LANGUAGE ScopedTypeVariables #-}
17{-# LANGUAGE UndecidableInstances #-}
18module Type where
19
20import Data.Function
21import Data.Char
22import Data.Either
23import Data.String
24import Data.Maybe
25import Data.List
26import Data.Set (Set)
27import qualified Data.Set as Set
28import Data.Map (Map)
29import qualified Data.Map as Map
30import Data.Monoid
31import Data.Foldable hiding (foldr)
32import Data.Traversable
33import Control.Monad.Except
34import Control.Monad.State
35import Control.Monad.Identity
36import Control.Monad.Reader
37import Control.Monad.Writer
38import Control.Applicative
39import Control.Arrow hiding ((<+>))
40import Text.Parsec.Pos
41import Text.Parsec.Error
42import GHC.Exts (Constraint)
43import Debug.Trace
44
45import ParserUtil (ParseError)
46import Pretty
47
48trace' x = trace (ppShow x) x
49
50(<&>) = flip (<$>)
51
52-------------------------------------------------------------------------------- literals
53
54data Lit
55 = LInt Integer
56 | LNat Int -- invariant property: >= 0
57 | LChar Char
58 | LString String
59 | LFloat Double
60 deriving (Eq, Ord)
61
62-- literals in expressions
63pattern EInt a = ELit (LInt a)
64pattern ENat a = ELit (LNat a)
65pattern EChar a = ELit (LChar a)
66pattern EString a = ELit (LString a)
67pattern EFloat a = ELit (LFloat a)
68
69-------------------------------------------------------------------------------- patterns
70
71-- TODO: remove
72data Pat_ t c v b -- type; constructor info; variable info; sub-pattern
73 = PLit_ Lit
74 | PVar_ t v
75 | PCon_ t c [b]
76 | PTuple_ [b]
77 | PRecord_ [(Name, b)]
78 | PAt_ v b -- used before pattern compilation
79 | Wildcard_ t -- TODO: merge into PVar
80 -- aux
81 | PPrec_ b [(b{-TODO: Name-}, b)] -- used before precedence calculation
82 deriving (Functor,Foldable,Traversable)
83
84-- TODO: remove
85instance Eq Pat where (==) = error "Eq Pat"
86instance Ord Pat where compare = error "Ord Pat"
87
88mapPat :: (t -> t') -> (c -> c') -> (v -> v') -> Pat_ t c v b -> Pat_ t' c' v' b
89mapPat tf f g = \case
90 PLit_ l -> PLit_ l
91 PVar_ t v -> PVar_ (tf t) $ g v
92 PCon_ t c p -> PCon_ (tf t) (f c) p
93 PTuple_ p -> PTuple_ p
94 PRecord_ p -> PRecord_ p -- $ map (g *** id) p
95 PAt_ v p -> PAt_ (g v) p
96 Wildcard_ t -> Wildcard_ (tf t)
97 PPrec_ b bs -> PPrec_ b bs
98
99--------------------------------------------
100
101data PatR = PatR Range (Pat_ ExpR Name Name PatR)
102
103-- TODO: remove
104pattern PatR' a <- PatR _ a where
105 PatR' a = PatR mempty a
106
107pattern PVar' a b = PatR a (PVar_ TWildcard b)
108pattern PCon' a b c = PatR a (PCon_ TWildcard b c)
109
110--------------------------------------------
111
112type Pat = PatR
113
114pattern Pat a <- PatR _ a where
115 Pat a = PatR mempty a
116
117pattern PAt v l = Pat (PAt_ v l)
118pattern PLit l = Pat (PLit_ l)
119pattern PVar t l = Pat (PVar_ t l)
120pattern PCon t c l = Pat (PCon_ t c l)
121pattern PTuple l = Pat (PTuple_ l)
122pattern Wildcard t = Pat (Wildcard_ t)
123
124patternVars' :: ParPat Exp -> [Name]
125patternVars' = concatMap $ \case
126 PatVar n -> [n]
127 PatCon _ ps -> foldMap patternVars' ps
128 PatLit{} -> []
129 ViewPat _ p -> patternVars' p
130 PatPrec p ps -> patternVars' p ++ foldMap patternVars' (map snd ps)
131
132patternVars :: Pat -> [(Name, Exp)]
133patternVars (Pat p) = case p of
134 PVar_ t v -> [(v, t)]
135 PAt_ v p -> [(v, tyOfPat p)]
136 p -> foldMap patternVars p
137
138-------------------------------------------------------------------------------- expressions
139
140data Exp_ v p b -- TODO: remove p
141 = Star_
142 | ELit_ Lit
143
144 | EVar_ b v
145 | TCon_ b v -- TODO: use it or remove it
146 | TWildcard_ -- star kinded type variable
147 -- | TFun_ v [a] -- TODO
148
149 | Forall_ Visibility (Maybe v) b b
150 | ELam_ (Maybe b){-Just:hidden + type-} p b
151 | EApp_ b b b
152 | ETyApp_ b b b
153 | EPrec_ b [(b, b)] -- aux: used only before precedence calculation
154 | ELet_ p b b -- TODO: remove?
155
156 | TRecord_ (Map v b)
157 | ERecord_ [(Name, b)]
158 | EFieldProj_ b Name
159
160 | TTuple_ [b] -- TODO: remove?
161 | ETuple_ [b] -- TODO: remove?
162 | ENamedRecord_ Name [(Name, b)]
163
164 | WRefl_ b
165 | CEq_ b (TypeFun v b) -- unification between a type and a fully applied type function; CEq t f: t ~ f
166 -- TODO: merge with CUnify?
167 | CUnify_ b b -- unification between (non-type-function) types; CUnify t s: t ~ s
168 | Split_ b b b -- Split x y z: x, y, z are records; fields of x = disjoint union of the fields of y and z
169
170 | ETypeSig_ b b
171 | Case_ b b [(p {-Name, [Name{-v-}]-}, b)] -- simple case expression, not used yet
172 | WhereBlock_ [(Name{-v-}, b)] b -- not used yet
173 | PrimFun b Name [b] Int -- type, name, collected args, arity
174 | FunAlts_ Int{-number of parameters-} [([ParPat b], GuardTree b)]
175 -- TODO: remove
176 | EAlts_ [b] -- function alternatives
177 | ENext_ Doc b -- go to next alternative
178
179 deriving (Eq,Ord,Functor,Foldable,Traversable) -- TODO: elim Eq instance
180
181-- TODO! remove
182instance Eq Doc where _ == _ = True
183instance Ord Doc where _ `compare` _ = EQ
184
185type ParPat e = [Pat' e]
186
187data ConName
188 = TupleName Int
189 | ConName Name
190-- | ConLit Lit
191 deriving (Eq, Ord)
192
193data Pat' e
194 = PatVar Name -- v
195 | PatCon ConName [ParPat e]
196 | PatLit Lit
197 | ViewPat e (ParPat e)
198 | PatPrec (ParPat e) [(ParPat e{-TODO: Name-}, ParPat e)] -- used before precedence calculation
199 deriving (Eq,Ord,Functor,Foldable,Traversable) -- TODO: elim Eq instance
200
201data GuardTree e
202 = GuardCon e ConName [ParPat e] (GuardTree e)
203 | GuardWhere (Binds e) (GuardTree e)
204 | GuardAlts [GuardTree e]
205 | GuardExp e
206 | GuardPat e (ParPat e) (GuardTree e) -- used only before precedence calculation
207 deriving (Eq,Ord,Functor,Foldable,Traversable) -- TODO: elim Eq instance
208
209type Binds e = [(Pat, e)] -- TODO: replace with Env
210
211data Visibility = Visible | Hidden | Irrelevant deriving (Eq, Ord)
212
213type ExpR = Exp
214
215pattern ExpR r e <- (peelThunkR -> (r, e)) where
216 ExpR r e = ExpTh r mempty e
217
218expR = ExpR mempty
219pattern EVarR' a b = ExpR a (EVar_ TWildcard b)
220pattern EAppR' a b c = ExpR a (EApp_ TWildcard b c)
221--pattern ELamR' a b c = ExpR a (ELam_ False b c)
222
223pattern ExpR' a <- ExpR _ a where
224 ExpR' a = ExpR mempty a
225
226pattern TWildcard = ExpR' TWildcard_
227
228data Exp = ExpTh Range Subst Exp'
229type Exp' = Exp_ Name Pat Exp
230
231type Ty = Exp
232
233pattern Exp a <- (peelThunk -> a) where
234 Exp a = thunk a
235
236thunk = ExpTh mempty{-TODO: review this-} mempty
237
238-- TODO: eliminate or improve
239instance Eq Exp where Exp a == Exp b = a == b
240instance Ord Exp where Exp a `compare` Exp b = a `compare` b
241
242pattern TCon k a <- Exp (TCon_ k (TypeIdN a)) where
243 TCon k a = Exp (TCon_ k (TypeIdN' a "typecon"))
244
245pattern Con0 t a = TVar t (ExpN a)
246
247pattern Star = Exp Star_
248
249pattern TRecord b = Exp (TRecord_ b)
250pattern TTuple b = Exp (TTuple_ b)
251pattern TUnit = TTuple []
252pattern CEq a b = Exp (CEq_ a b)
253pattern CUnify a b = Exp (CUnify_ a b)
254pattern Split a b c = Exp (Split_ a b c)
255pattern Forall a b c = Exp (Forall_ Visible (Just a) b c)
256pattern TArr a b = Exp (Forall_ Visible Nothing a b)
257pattern ELit a = Exp (ELit_ a)
258pattern EVar a <- Exp (EVar_ _ a)
259pattern TVar k b = Exp (EVar_ k b)
260pattern EApp a b <- Exp (EApp_ _ a b)
261pattern TApp k a b = Exp (EApp_ k a b)
262pattern ETyApp k a b = Exp (ETyApp_ k a b)
263pattern ELam a b = Exp (ELam_ Nothing a b)
264pattern ELet a b c = Exp (ELet_ a b c)
265pattern ETuple a = Exp (ETuple_ a)
266pattern ERecord b = Exp (ERecord_ b)
267pattern EFieldProj k a = Exp (EFieldProj_ k a)
268pattern EAlts b = Exp (EAlts_ b)
269pattern ENext i k = Exp (ENext_ i k)
270pattern Case t b as = Exp (Case_ t b as)
271pattern WRefl k = Exp (WRefl_ k)
272pattern FunAlts i as = Exp (FunAlts_ i as)
273
274pattern A0 x <- EVar (ExpIdN x)
275pattern A1 f x <- EApp (A0 f) x
276pattern A2 f x y <- EApp (A1 f x) y
277pattern A3 f x y z <- EApp (A2 f x y) z
278pattern A4 f x y z v <- EApp (A3 f x y z) v
279pattern A5 f x y z v w <- EApp (A4 f x y z v) w
280pattern A6 f x y z v w q <- EApp (A5 f x y z v w) q
281pattern A7 f x y z v w q r <- EApp (A6 f x y z v w q) r
282pattern A8 f x y z v w q r s <- EApp (A7 f x y z v w q r) s
283pattern A9 f x y z v w q r s t <- EApp (A8 f x y z v w q r s) t
284pattern A10 f x y z v w q r s t a <- EApp (A9 f x y z v w q r s t) a
285pattern A11 f x y z v w q r s t a b <- EApp (A10 f x y z v w q r s t a) b
286
287infixr 7 ~>, ~~>
288a ~> b = TArr a b
289
290(~~>) :: [Exp] -> Exp -> Exp
291args ~~> res = foldr (~>) res args
292
293infix 4 ~~, ~~~
294(~~) = CEq
295(~~~) = CUnify
296
297buildApp :: (Exp -> Exp) -> Exp -> [Exp] -> Exp
298buildApp n restype args = f restype $ reverse args
299 where
300 f ty [] = n ty
301 f ty (a:as) = TApp ty (f (tyOf a ~> ty) as) a
302
303
304mapExp_ :: (PShow v, PShow p, PShow b, Ord v') => (v -> v') -> (p -> p') -> Exp_ v p b -> Exp_ v' p' b
305mapExp_ vf f = \case
306 ELit_ x -> ELit_ x
307 EVar_ k x -> EVar_ k $ vf x
308 EApp_ k x y -> EApp_ k x y
309 ELam_ h x y -> ELam_ h (f x) y
310 ELet_ x y z -> ELet_ (f x) y z
311 ETuple_ x -> ETuple_ x
312 ERecord_ x -> ERecord_ $ x --map (vf *** id) x
313 ENamedRecord_ n x -> ENamedRecord_ n x --(vf n) $ map (vf *** id) x
314 EFieldProj_ k x -> EFieldProj_ k x -- $ vf x
315 ETypeSig_ x y -> ETypeSig_ x y
316 EAlts_ x -> EAlts_ x
317 Case_ t x xs -> Case_ t x $ map (f *** id) xs
318 ENext_ i k -> ENext_ i k
319 ETyApp_ k b t -> ETyApp_ k b t
320 PrimFun k a b c -> PrimFun k a b c
321 Star_ -> Star_
322 TCon_ k v -> TCon_ k (vf v)
323 -- | TFun_ f [a]
324 Forall_ h mv b1 b2 -> Forall_ h (vf <$> mv) b1 b2
325 TTuple_ bs -> TTuple_ bs
326 TRecord_ m -> TRecord_ $ Map.fromList $ map (vf *** id) $ Map.toList m -- (Map v b)
327 CEq_ a (TypeFun n as) -> CEq_ a (TypeFun (vf n) as)
328 CUnify_ a1 a2 -> CUnify_ a1 a2
329 Split_ a1 a2 a3 -> Split_ a1 a2 a3
330 WRefl_ k -> WRefl_ k
331 TWildcard_ -> TWildcard_
332 EPrec_ e es -> EPrec_ e es
333 FunAlts_ i as -> FunAlts_ i as
334 x -> error $ "mapExp: " ++ ppShow x
335
336--traverseExp :: (Applicative m, Ord v') => (v -> v') -> (t -> m t') -> Exp_ v p t -> m (Exp_ v' p t')
337traverseExp nf f = fmap (mapExp_ nf id) . traverse f
338
339----------------
340
341data TypeFun n a = TypeFun n [a]
342 deriving (Eq,Ord,Functor,Foldable,Traversable)
343
344type TypeFunT = TypeFun IdN Exp
345
346-------------------------------------------------------------------------------- cached type inference
347
348inferLit :: Lit -> Exp
349inferLit a = thunk $ TCon_ (thunk Star_) $ flip TypeIdN' "typecon" $ case a of
350 LInt _ -> "Int"
351 LChar _ -> "Char"
352 LFloat _ -> "Float"
353 LString _ -> "String"
354 LNat _ -> "Nat"
355
356tyFunRes :: Exp -> Exp
357tyFunRes = \case
358 TArr a b -> b
359 x -> error $ "tyFunRes: not implemented " ++ ppShow x
360
361tyOf :: Exp -> Exp
362tyOf = \case
363 Exp t -> case t of
364 ELit_ l -> inferLit l
365 EVar_ k _ -> k
366 EApp_ k _ _ -> k
367 ETyApp_ k _ _ -> k
368 ETuple_ es -> TTuple $ map tyOf es
369 ELam_ (Just k) _ _ -> k
370 ELam_ Nothing (tyOfPat -> a) (tyOf -> b) -> Exp $ Forall_ Visible Nothing{-TODO-} a b
371 Case_ t _ _ -> t
372 ETypeSig_ b t -> t -- tyOf b
373 ELet_ _ _ e -> tyOf e
374 ERecord_ (unzip -> (fs, es)) -> TRecord $ Map.fromList $ zip fs $ map tyOf es
375 EFieldProj_ k _ -> k
376 EAlts_ bs -> tyOf $ head bs
377 ENext_ _ k -> k
378 PrimFun k _ _ _ -> k
379 -- was types
380 Star_ -> Star
381 TCon_ k _ -> k
382 Forall_ _ _ _ _ -> Star
383 TTuple_ _ -> Star
384 TRecord_ _ -> Star
385 CEq_ _ _ -> Star
386 CUnify_ _ _ -> Star
387 Split_ _ _ _ -> Star
388 WRefl_ k -> k
389 TWildcard_ -> TWildcard
390 e -> error $ "tyOf " ++ ppShow e
391
392tyOfPat :: Pat -> Exp
393tyOfPat = \case
394 PCon t _ _ -> t
395 PVar t _ -> t
396 Wildcard t -> t
397 PLit l -> inferLit l
398 PTuple xs -> thunk $ TTuple_ $ map tyOfPat xs
399-- PRecord xs -> [(Name, b)]
400 PAt _ p -> tyOfPat p
401 e -> error $ "tyOfPat " ++ ppShow e
402
403isStar = \case
404 Star -> True
405 _ -> False
406
407-------------------------------------------------------------------------------- tag handling
408
409class GetTag c where
410 type Tag c
411 getTag :: c -> Tag c
412
413instance GetTag ExpR where
414 type Tag ExpR = Range
415 getTag (ExpR a _) = a
416instance GetTag PatR where
417 type Tag PatR = Range
418 getTag (PatR a _) = a
419
420-------------------------------------------------------------------------------- names
421
422data NameSpace = TypeNS | ExpNS
423 deriving (Eq, Ord)
424
425-- TODO: more structure instead of Doc
426data NameInfo = NameInfo (Maybe Fixity) Doc
427
428data N = N
429 { nameSpace :: NameSpace
430 , qualifier :: [String]
431 , nName :: String
432 , nameInfo :: NameInfo
433 }
434
435instance Eq N where N a b c d == N a' b' c' d' = (a, b, c) == (a', b', c')
436instance Ord N where N a b c d `compare` N a' b' c' d' = (a, b, c) `compare` (a', b', c')
437
438type Fixity = (Maybe FixityDir, Int)
439data FixityDir = FDLeft | FDRight
440
441pattern ExpN n <- N ExpNS [] n _ where
442 ExpN n = N ExpNS [] n (NameInfo Nothing "exp")
443pattern ExpN' n i = N ExpNS [] n (NameInfo Nothing i)
444pattern TypeN n <- N TypeNS [] n _ where
445 TypeN n = N TypeNS [] n (NameInfo Nothing "type")
446pattern TypeN' n i = N TypeNS [] n (NameInfo Nothing i)
447
448addPrefix :: String -> Name -> Name
449addPrefix s (N a b c d) = N a b (s ++ c) d
450
451-- TODO: rename/eliminate
452type Name = N
453type TName = N
454type TCName = N -- type constructor name; if this turns out to be slow use Int or ADT instead of String
455type EName = N
456type FName = N
457type MName = N -- module name
458type ClassName = N
459
460toExpN (N _ a b i) = N ExpNS a b i
461toTypeN (N _ a b i) = N TypeNS a b i
462isTypeVar (N ns _ _ _) = ns == TypeNS
463isConstr (N _ _ (c:_) _) = isUpper c || c == ':'
464
465-------------------------------------------------------------------------------- error handling
466
467-- TODO: add more structure to support desugaring
468data Range
469 = Range SourcePos SourcePos
470 | NoRange
471
472instance Monoid Range where
473 mempty = NoRange
474 Range a1 a2 `mappend` Range b1 b2 = Range (min a1 a2) (max b1 b2)
475 NoRange `mappend` a = a
476 a `mappend` b = a
477
478type WithRange = (,) Range
479pattern WithRange a b = (a, b)
480
481--------------------------------------------------------------------------------
482
483type WithExplanation = (,) Doc
484
485pattern WithExplanation d x = (d, x)
486
487-- TODO: add more structure
488data ErrorMsg
489 = AddRange Range ErrorMsg
490 | InFile String ErrorMsg
491 | ErrorCtx Doc ErrorMsg
492 | ErrorMsg Doc
493 | EParseError ParseError
494 | UnificationError Exp Exp [WithExplanation [Exp]]
495
496instance Monoid ErrorMsg where
497 mempty = ErrorMsg "<<>>"
498 mappend a b = a
499
500instance Show ErrorMsg where
501 show = show . f Nothing Nothing Nothing where
502 f d file rng = \case
503 InFile s e -> f d (Just s) Nothing e
504 AddRange NoRange e -> {- showRange file (Just r) <$$> -} f d file rng e
505 AddRange r e -> {- showRange file (Just r) <$$> -} f d file (Just r) e
506 ErrorCtx d e -> {-"during" <+> d <$$> -} f (Just d) file rng e
507 EParseError pe -> text $ show pe
508 ErrorMsg e -> maybe "" ("during" <+>) d <$$> (showRange file rng) <$$> e
509 UnificationError a b tys -> maybe "" ("during" <+>) d <$$> (showRange file rng) <$$> "cannot unify" <+> pShow a </> "with" <+> pShow b
510 <$$> "----------- equations"
511 <$$> vcat (map (\(s, l) -> s <$$> vcat (map pShow l)) tys)
512
513dummyPos = newPos "" 0 0
514
515showErr :: ErrorMsg -> (SourcePos, SourcePos, String)
516showErr e = (i, j, show msg)
517 where
518 (r, msg) = f Nothing e
519 (i, j) = case r of
520 Just (Range i j) -> (i, j)
521 _ -> (dummyPos, dummyPos)
522 f rng = \case
523 InFile s e -> f Nothing e
524 AddRange r e -> f (Just r) e
525 ErrorCtx d e -> {-(("during" <+> d) <+>) <$> -} f rng e
526 EParseError pe -> (Just $ Range p (incSourceColumn p 1), {-vcat $ map (text . messageString) $ errorMessages-} text $ show pe)
527 where p = errorPos pe
528 ErrorMsg d -> (rng, d)
529 UnificationError a b tys -> (rng, "cannot unify" <+> pShow a </> "with" <+> pShow b)
530
531type ErrorT = ExceptT ErrorMsg
532
533throwParseError = throwError . EParseError
534
535mapError f m = catchError m $ throwError . f
536
537addCtx d = mapError (ErrorCtx d)
538
539addRange :: MonadError ErrorMsg m => Range -> m a -> m a
540addRange NoRange = id
541addRange r = mapError $ AddRange r
542
543--throwErrorTCM :: Doc -> TCM a
544throwErrorTCM = throwError . ErrorMsg
545
546showRange :: Maybe String -> Maybe Range -> Doc
547showRange Nothing Nothing = "no file position"
548showRange Nothing (Just _) = "no file"
549showRange (Just _) Nothing = "no position"
550showRange (Just src) (Just (Range s e)) = str
551 where
552 startLine = sourceLine s - 1
553 endline = sourceLine e - if sourceColumn e == 1 then 1 else 0
554 len = endline - startLine
555 str = vcat $ ("position:" <+> text (show s) <+> "-" <+> text (show e)):
556 map text (take len $ drop startLine $ lines src)
557 ++ [text $ replicate (sourceColumn s - 1) ' ' ++ replicate (sourceColumn e - sourceColumn s) '^' | len == 1]
558
559-------------------------------------------------------------------------------- parser output
560
561data ValueDef p e = ValueDef Bool{-recursive-} p e
562data TypeSig n t = TypeSig n t
563
564data ModuleR
565 = Module
566 { extensions :: [Extension]
567 , moduleImports :: [Name] -- TODO
568 , moduleExports :: Maybe [Export]
569 , definitions :: [DefinitionR]
570 }
571
572type DefinitionR = WithRange Definition
573data Definition
574 = DValueDef Bool{-True: use in instance search-} (ValueDef PatR ExpR)
575 | DAxiom (TypeSig Name ExpR)
576 | DDataDef Name [(Name, ExpR)] [WithRange ConDef] -- TODO: remove, use GADT
577 | GADT Name [(Name, ExpR)] [WithRange (Name, ConDef')]
578 | ClassDef [ExpR] Name [(Name, ExpR)] [TypeSig Name ExpR]
579 | InstanceDef [ExpR] Name [ExpR] [ValueDef PatR ExpR]
580 | TypeFamilyDef Name [(Name, ExpR)] ExpR
581 | PrecDef Name Fixity
582-- used only during parsing
583 | PreValueDef (Range, EName) [PatR] WhereRHS
584 | DTypeSig (TypeSig EName ExpR)
585 | ForeignDef Name ExpR
586
587-- used only during parsing
588data WhereRHS = WhereRHS GuardedRHS (Maybe WhereBlock)
589type WhereBlock = [DefinitionR]
590
591-- used only during parsing
592data GuardedRHS
593 = Guards Range [(ExpR, ExpR)]
594 | NoGuards ExpR
595
596data ConDef = ConDef Name [FieldTy]
597data ConDef' = ConDef' [(Maybe Name, ExpR)] [FieldTy] ExpR
598data FieldTy = FieldTy {fieldName :: Maybe (Name, Bool{-True: context projection-}), fieldType :: ExpR}
599
600type TypeFunR = TypeFun Name ExpR
601type ValueDefR = ValueDef PatR ExpR
602
603data Extension
604 = NoImplicitPrelude
605 deriving (Eq, Ord, Show)
606
607data Export
608 = ExportModule Name
609 | ExportId Name
610
611-------------------------------------------------------------------------------- names with unique ids
612
613type IdN = N
614pattern IdN a = a
615--newtype IdN = IdN N deriving (Eq, Ord)
616{- TODO
617data IdN = IdN !Int N
618
619instance Eq IdN where IdN i _ == IdN j _ = i == j
620instance Ord IdN where IdN i _ `compare` IdN j _ = i `compare` j
621-}
622
623pattern TypeIdN n <- IdN (TypeN n)
624pattern TypeIdN' n i = IdN (TypeN' n i)
625pattern ExpIdN n <- IdN (ExpN n)
626pattern ExpIdN' n i = IdN (ExpN' n i)
627
628type FreshVars = [String] -- fresh typevar names
629
630type VarMT = StateT FreshVars
631
632show5 :: Int -> String
633show5 i = replicate (5 - length s) '0' ++ s where s = show i
634
635freshTypeVars :: FreshVars
636freshTypeVars = map ('t':) $ map show5 [0..]
637
638resetVars :: MonadState FreshVars m => m ()
639resetVars = put freshTypeVars
640
641newName :: MonadState FreshVars m => Doc -> m IdN
642newName info = do
643 i <- gets head
644 modify tail
645 return $ TypeN' i info
646
647newEName = do
648 i <- gets head
649 modify tail
650 return $ ExpN $ "e" ++ i
651
652
653-------------------------------------------------------------------------------- environments
654
655type Env' a = Map Name a
656type Env a = Map IdN a
657
658data Item = ISubst Bool{-True: found & replaced def-} Exp | ISig Bool{-True: Rigid-} Exp
659
660tyOfItem = eitherItem (const tyOf) $ const id
661
662eitherItem f g (ISubst r x) = f r x
663eitherItem f g (ISig r x) = g r x
664
665pureSubst se = null [x | ISig rigid x <- Map.elems $ getTEnv se]
666onlySig (TEnv x) = TEnv $ Map.filter isSig x
667isSig = eitherItem (\_ -> const False) (\rigid -> const True)
668
669newtype Subst = Subst {getSubst :: Env Exp}
670
671instance Monoid Subst where
672 mempty = Subst mempty
673 -- semantics: subst (m1 <> m2) = subst m1 . subst m2
674 -- example: subst ({y -> z} <> {x -> y}) = subst {y -> z} . subst {x -> y} = subst {y -> z, x -> z}
675 -- example2: subst ({x -> z} <> {x -> y}) = subst {x -> z} . subst {x -> y} = subst {x -> y}
676 m1@(Subst y1) `mappend` Subst y2 = Subst $ (subst_ m1 <$> y2) <> y1
677
678subst_ = subst
679singSubst' a b = Subst $ Map.singleton a b
680
681nullSubst (Subst s) = Map.null s
682toTEnv (Subst s) = TEnv $ ISubst False <$> s
683toSubst (TEnv s) = Subst $ Map.map (\(ISubst _ e) -> e) $ Map.filter (eitherItem (\_ -> const True) (\_ -> const False)) s
684
685newtype TEnv = TEnv {getTEnv :: Env Item} -- either substitution or bound name
686
687instance Monoid TEnv where
688 mempty = TEnv mempty
689 -- semantics: apply (m1 <> m2) = apply m1 . apply m2
690 -- example: subst ({y -> z} <> {x -> y}) = subst {y -> z} . subst {x -> y} = subst {y -> z, x -> z}
691 -- example2: subst ({x -> z} <> {x -> y}) = subst {x -> z} . subst {x -> y} = subst {x -> y}
692 m1@(TEnv y1) `mappend` TEnv y2 = TEnv $ Map.unionWith mergeSubsts (subst (toSubst m1) <$> y2) y1
693
694mergeSubsts (ISubst _ s) (ISig _ _) = ISubst True s
695mergeSubsts (ISubst b s) (ISubst b' _) = ISubst (b || b') s
696mergeSubsts (ISig _ _) (ISubst _ s) = ISubst True s
697mergeSubsts a _ = a
698
699singSubst a b = TEnv $ Map.singleton a $ ISubst False b
700singSubstTy_ a b = TEnv $ Map.singleton a $ ISig False b
701
702-- build recursive environment -- TODO: generalize
703recEnv :: Pat -> Exp -> Exp
704recEnv (PVar _ v) th_ = th where th = subst (singSubst' v th) th_
705recEnv _ th = th
706
707mapExp' f nf pf e = mapExp_ nf pf $ f <$> e
708
709peelThunkR :: Exp -> (Range, Exp')
710peelThunkR e@(ExpTh r _ _) = (r, peelThunk e)
711
712peelThunk :: Exp -> Exp'
713peelThunk (ExpTh _ env@(Subst m) e)
714-- | Map.null m = e
715 | otherwise = case e of
716 Forall_ h (Just n) a b -> Forall_ h (Just n) (f a) $ subst_ (delEnv n (f a) env) b
717 ELam_ h x y -> ELam_ (f <$> h) (mapPat' x) $ subst_ (delEnvs (patternVars x) env) y
718 Case_ t e cs -> Case_ (f t) (f e) [(mapPat' x, subst_ (delEnvs (patternVars x) env) y) | (x, y) <- cs]
719 ELet_ x y z -> ELet_ (mapPat' x) (g y) (g z) where
720 g = subst_ (delEnvs (patternVars x) env)
721 EVar_ k v -> case Map.lookup v m of
722 Just e -> case peelThunk e of
723 PrimFun _ a b c -> PrimFun (f k) a b c -- hack!
724 x -> x
725 _ -> EVar_ (f k) v
726 FunAlts_ i ts -> FunAlts_ i $ flip map ts $ \(p, t) -> (p, subst (delEnvs' (foldMap patternVars' p) env) t)
727 _ -> mapExp' f id (error "peelT") e
728 where
729 f = subst_ env
730
731 mapPat' :: Pat -> Pat
732 mapPat' (Pat p) = Pat $ mapPat f id id $ mapPat' <$> p
733
734 delEnv n x = delEnvs [(n, x)]
735
736delEnvs xs (Subst env) = Subst $ foldr Map.delete env $ map fst xs
737delEnvs' xs (Subst env) = Subst $ foldr Map.delete env xs
738
739subst1 :: Subst -> Exp -> Exp
740subst1 s@(Subst m) = \case
741 TVar k v -> case Map.lookup v m of
742 Just e -> subst1 s e
743 _ -> TVar k v
744 e -> e
745
746--------------------------------------------------------------------------------
747-- fix :: forall (a :: *) . (a -> a) -> a
748-- fix = \{a :: *} (f :: a -> a) -> [ x |-> f x ] x :: a
749
750fixName = ExpN "fix"
751
752fixBody :: Exp
753fixBody = Exp $ ELam_ (Just ty) (PVar Star an) $ Exp $ ELam_ Nothing (PVar a fn) fx
754 where
755 ty = Exp $ Forall_ Hidden (Just an) Star $ (a ~> a) ~> a
756
757 fx = ExpTh mempty{-TODO: review this-} (singSubst' x $ TApp a f fx) $ EVar_ a x
758
759 an = TypeN "a"
760 a = TVar Star an
761 fn = ExpN "f"
762 f = TVar (a ~> a) fn
763 x = ExpN "x"
764
765--------------------------------------------------------------------------------
766
767data PolyEnv = PolyEnv
768 { instanceDefs :: InstanceDefs
769 , getPolyEnv :: Env' Item
770 , constructors :: Env' [(Name, Int)]
771 , precedences :: PrecMap
772 , typeFamilies :: InstEnv
773 , infos :: Infos
774 }
775
776type Info = (SourcePos, SourcePos, String)
777type Infos = [Info]
778
779type InstEnv = Env' Exp
780
781type PrecMap = Env' Fixity
782
783type InstanceDefs = Env' (Map Name ())
784
785emptyPolyEnv :: PolyEnv
786emptyPolyEnv = PolyEnv mempty mempty mempty mempty mempty mempty
787
788startPolyEnv = emptyPolyEnv {getPolyEnv = Map.singleton fixName $ ISubst True fixBody}
789
790joinPolyEnvs :: forall m. MonadError ErrorMsg m => Bool -> [PolyEnv] -> m PolyEnv
791joinPolyEnvs allownameshadow ps = PolyEnv
792 <$> mkJoin' instanceDefs
793 <*> mkJoin allownameshadow getPolyEnv
794 <*> mkJoin allownameshadow constructors
795 <*> mkJoin False precedences
796 <*> mkJoin False typeFamilies
797 <*> pure (concatMap infos ps)
798 where
799 mkJoin :: Bool -> (PolyEnv -> Env a) -> m (Env a)
800 mkJoin True f = return $ Map.unions $ map f ps
801 mkJoin False f = case filter (not . Map.null) . map f $ ps of
802 [m] -> return m
803 ms -> case filter (not . null . drop 1 . snd) $ Map.toList ms' of
804 [] -> return $ fmap head $ Map.filter (not . null) ms'
805 xs -> throwErrorTCM $ "Definition clash:" <+> pShow (map fst xs)
806 where
807 ms' = Map.unionsWith (++) $ map ((:[]) <$>) ms
808
809 mkJoin' f = case [(n, x) | (n, s) <- Map.toList ms', (x, is) <- Map.toList s, not $ null $ drop 1 is] of
810 _ -> return $ fmap head . Map.filter (not . null) <$> ms'
811-- xs -> throwErrorTCM $ "Definition clash':" <+> pShow xs
812 where
813 ms' = Map.unionsWith (Map.unionWith (++)) $ map ((((:[]) <$>) <$>) . f) ps
814
815addPolyEnv pe m = do
816 env <- ask
817 env <- joinPolyEnvs True [pe, env]
818 local (const env) m
819
820-- reversed order!
821getApp (Exp x) = case x of
822 EApp_ _ f x -> (id *** (x:)) <$> getApp f
823 TCon_ _ n -> Just (n, [])
824 _ -> Nothing
825
826withTyping ts = addPolyEnv $ emptyPolyEnv {getPolyEnv = ISig False <$> ts}
827
828-------------------------------------------------------------------------------- monads
829
830nullTEnv (TEnv m) = Map.null m
831
832type TypingT = WriterT' TEnv
833
834type EnvType = (TEnv, Exp)
835
836hidden = \case
837 Visible -> False
838 _ -> True
839
840toEnvType :: Exp -> ([(Visibility, (Name, Exp))], Exp)
841toEnvType = \case
842 Exp (Forall_ v@(hidden -> True) (Just n) t x) -> ((v, (n, t)):) *** id $ toEnvType x
843 x -> (mempty, x)
844
845envType d = TEnv $ Map.fromList $ map ((id *** ISig False) . snd) d
846
847addInstance n ((envType *** id) . toEnvType -> (_, getApp -> Just (c, _)))
848 = addPolyEnv $ emptyPolyEnv {instanceDefs = Map.singleton c $ Map.singleton n ()}
849
850monoInstType v k = Map.singleton v k
851
852toTCMS :: Exp -> TCMS ([Exp], Exp)
853toTCMS (toEnvType -> (typ@(envType -> TEnv se), ty)) = WriterT' $ do
854 let fv = map (fst . snd) typ
855 newVars <- forM fv $ \case
856 TypeN' n i -> newName $ "instvar" <+> text n <+> i
857 v -> error $ "instT: " ++ ppShow v
858 let s = Map.fromList $ zip fv newVars
859 return (TEnv $ repl s se, (map (repl s . uncurry (flip TVar)) $ hiddenVars typ, repl s ty))
860
861hiddenVars ty = [x | (Hidden, x) <- ty]
862
863instantiateTyping_ vis info se ty = do
864 ambiguityCheck ("ambcheck" <+> info) se ty --(subst su se) (subst su ty)
865 typingToTy_ vis ".." (se, ty)
866 where
867 su = toSubst se
868
869splitEnv (TEnv se) = TEnv *** TEnv $ cycle (f gr') (se', gr')
870 where
871 (se', gr') = flip Map.partition se $ \case
872 ISubst False _ -> False
873 _ -> True
874 f = foldMap (\(k, ISubst False x) -> Set.insert k $ freeVars x) . Map.toList
875 f' = foldMap (\(k, ISig False x) -> Set.insert k $ freeVars x) . Map.toList
876 cycle acc (se, gr) = (if Set.null s then id else cycle (acc <> s)) (se', gr <> gr')
877 where
878 (se', gr') = flip Map.partitionWithKey se $ \k -> \case
879 ISig False t -> not $ Set.insert k (freeVars t) `hasSame` acc
880 _ -> True
881 s = f' gr'
882
883hasSame a b = not $ Set.null $ a `Set.intersection` b
884
885instantiateTyping_' :: Bool -> Doc -> TEnv -> Exp -> TCM ([(IdN, Exp)], Exp)
886instantiateTyping_' typ info se ty = do
887 ty <- instantiateTyping_ (if typ then Hidden else Irrelevant) info se ty
888 return (hiddenVars $ fst $ toEnvType ty, ty)
889
890-- Ambiguous: (Int ~ F a) => Int
891-- Not ambiguous: (Show a, a ~ F b) => b
892--ambiguityCheck :: Doc -> TCMS Exp -> TCMS Exp
893ambiguityCheck msg se ty = do
894 pe <- asks getPolyEnv
895 let defined = dependentVars (Map.toList $ getTEnv se) $ Map.keysSet pe <> freeVars ty
896 case [(n, c) | (n, ISig rigid c) <- Map.toList $ getTEnv se, not $ any (`Set.member` defined) $ Set.insert n $ freeVars c] of
897 [] -> return ()
898 err -> do
899 tt <- typingToTy' (se, ty)
900 throwErrorTCM $
901 "during" <+> msg </> "ambiguous type:" <$$> pShow tt <$$> "problematic vars:" <+> pShow err
902
903-- compute dependent type vars in constraints
904-- Example: dependentVars [(a, b) ~ F b c, d ~ F e] [c] == [a,b,c]
905dependentVars :: [(IdN, Item)] -> Set TName -> Set TName
906dependentVars ie s = cycle mempty s
907 where
908 cycle acc s
909 | Set.null s = acc
910 | otherwise = cycle (acc <> s) (grow s Set.\\ acc)
911
912 grow = flip foldMap ie $ \case
913 (n, ISig rigid t) -> (Set.singleton n <-> freeVars t) <> case t of
914 CEq ty f -> freeVars ty <-> freeVars f
915 Split a b c -> freeVars a <-> (freeVars b <> freeVars c)
916-- CUnify{} -> mempty --error "dependentVars: impossible"
917 _ -> mempty
918-- (n, ISubst False x) -> (Set.singleton n <-> freeVars x)
919 _ -> mempty
920 where
921 a --> b = \s -> if Set.null $ a `Set.intersection` s then mempty else b
922 a <-> b = (a --> b) <> (b --> a)
923
924--typingToTy' :: EnvType -> Exp
925typingToTy' (s, t) = typingToTy "typingToTy" s t
926
927--typingToTy :: Doc -> TEnv -> Exp -> Exp
928typingToTy msg env ty = removeStar . renameVars <$> typingToTy_ Hidden msg (env, ty)
929 where
930 removeStar (Exp (Forall_ (hidden -> True) _ Star t)) = removeStar t
931 removeStar t = t
932
933 renameVars :: Exp -> Exp
934 renameVars = flip evalState (map (:[]) ['a'..]) . f mempty
935 where
936 f m (Exp e) = Exp <$> case e of
937 Forall_ h (Just n) k e -> do
938 n' <- gets (TypeN . head)
939 modify tail
940 Forall_ h (Just n') <$> f m k <*> f (Map.insert n n' m) e
941 e -> traverseExp nf (f m) e
942 where
943 nf n = fromMaybe n $ Map.lookup n m
944
945--typingToTy_ :: Visibility -> Doc -> EnvType -> Exp
946typingToTy_ vs msg (env, ty) = do
947 pe <- asks getPolyEnv
948 return $ f (Map.keysSet pe) l
949 where
950 l = sortBy (compare `on` constrKind . snd) [(n, t) | (n, ISig rigid t) <- Map.toList $ getTEnv env]
951 forall_ n k t
952-- | n `Set.notMember` freeVars t = TArrH k t
953 | otherwise = Exp $ Forall_ vs (Just n) k t
954
955 constrKind = \case
956 Star -> 0
957 _ -> 2
958
959 -- TODO: make more efficient?
960 f s [] = ty
961 f s ts = case [x | x@((n, t), ts') <- getOne ts, let fv = freeVars t, fv `Set.isSubsetOf` s] of
962 (((n, t), ts): _) -> forall_ n t $ f (Set.insert n s) ts
963 _ -> error $ show $ "orderEnv:" <+> msg <$$> pShow ts <$$> pShow l <$$> pShow ty
964
965getOne xs = [(b, a ++ c) | (a, b: c) <- zip (inits xs) (tails xs)]
966
967instance PShow Subst where
968 pShowPrec p (Subst t) = "Subst" <+> pShow t
969
970-- type checking monad transformer
971type TCMT m = ReaderT PolyEnv (ErrorT (WriterT Infos (VarMT m)))
972
973type TCM = TCMT Identity
974
975type TCMS = TypingT TCM
976
977catchExc :: TCM a -> TCM (Maybe a)
978catchExc = mapReaderT $ lift . fmap (either (const Nothing) Just) . runExceptT
979
980-------------------------------------------------------------------------------- free variables
981
982class FreeVars a where freeVars :: a -> Set IdN
983
984instance FreeVars Exp where
985 freeVars = \case
986 Exp x -> case x of
987 ELam_ h x y -> freeVars y Set.\\ Set.fromList (map fst $ patternVars x) -- TODO: h?
988 Case_ t e cs -> freeVars t <> freeVars e <> foldMap (\(x, y) -> freeVars y Set.\\ Set.fromList (map fst $ patternVars x)) cs
989 ELet_ x y z -> (freeVars y <> freeVars z) Set.\\ Set.fromList (map fst $ patternVars x) -- TODO: revise
990 EVar_ k a -> Set.singleton a <> freeVars k
991 Forall_ h (Just v) k t -> freeVars k <> Set.delete v (freeVars t)
992 x -> foldMap freeVars x
993
994instance FreeVars a => FreeVars [a] where freeVars = foldMap freeVars
995instance FreeVars a => FreeVars (TypeFun n a) where freeVars = foldMap freeVars
996instance FreeVars a => FreeVars (Env a) where freeVars = foldMap freeVars
997
998-------------------------------------------------------------------------------- replacement
999
1000type Repl = Map IdN IdN
1001
1002-- TODO: express with Substitute?
1003class Replace a where repl :: Repl -> a -> a
1004
1005-- TODO: make more efficient
1006instance Replace Exp where
1007 repl st = \case
1008 ty | Map.null st -> ty -- optimization
1009 Exp s -> Exp $ case s of
1010 ELam_ h _ _ -> error "repl lam"
1011 Case_ _ _ _ -> error "repl case"
1012 ELet_ _ _ _ -> error "repl let"
1013 Forall_ h (Just n) a b -> Forall_ h (Just n) (f a) (repl (Map.delete n st) b)
1014 t -> mapExp' f rn (error "repl") t
1015 where
1016 f = repl st
1017 rn a
1018 | Just t <- Map.lookup a st = t
1019 | otherwise = a
1020
1021instance Replace a => Replace (Env a) where
1022 repl st e = Map.fromList $ map (r *** repl st) $ Map.toList e
1023 where
1024 r x = fromMaybe x $ Map.lookup x st
1025
1026instance (Replace a, Replace b) => Replace (Either a b) where
1027 repl st = either (Left . repl st) (Right . repl st)
1028instance Replace Item where
1029 repl st = eitherItem (\r -> ISubst r . repl st) (\r -> ISig r . repl st)
1030
1031-------------------------------------------------------------------------------- substitution
1032
1033-- TODO: review usage (use only after unification)
1034class Substitute x a where subst :: x -> a -> a
1035
1036--instance Substitute a => Substitute (Constraint' n a) where subst = fmap . subst
1037instance Substitute x a => Substitute x [a] where subst = fmap . subst
1038instance (Substitute x a, Substitute x b) => Substitute x (a, b) where subst s (a, b) = (subst s a, subst s b)
1039instance (Substitute x a, Substitute x b) => Substitute x (Either a b) where subst s = subst s +++ subst s
1040instance Substitute x Exp => Substitute x Item where subst s = eitherItem (\r -> ISubst r . subst s) (\r -> ISig r . subst s)
1041{-
1042instance Substitute Pat where
1043 subst s = \case
1044 PVar t v -> PVar $ subst s v
1045 PCon t n l -> PCon (VarE n $ subst s ty) $ subst s l
1046 Pat p -> Pat $ subst s <$> p
1047-}
1048--instance Substitute TEnv Exp where subst = subst . toSubst --m1 (ExpTh m exp) = ExpTh (toSubst m1 <> m) exp
1049instance Substitute Subst Exp where subst m1 (ExpTh r m exp) = ExpTh r (m1 <> m) exp
1050--instance Substitute TEnv TEnv where subst s (TEnv m) = TEnv $ subst s <$> m
1051instance Substitute Subst TEnv where subst s (TEnv m) = TEnv $ subst s <$> m
1052{-
1053instance Substitute Subst (Pat' Exp) where
1054 subst s = \case
1055 = PatVar v ->Name -- v
1056 | PatCon ConName [ParPat e]
1057 | PatLit Lit
1058 | ViewPat e (ParPat e)
1059 | PatPrec (ParPat e) [(ParPat e{-TODO-}, ParPat e)] -- used before precedence calculation
1060 x -> fmap (subst s) x
1061-}
1062instance Substitute Subst (GuardTree Exp) where
1063 subst s = \case
1064 GuardPat e p t -> GuardPat e p $ subst (delEnvs' (patternVars' p) s) t
1065 GuardCon e n ps t -> GuardCon e n ps $ subst (delEnvs' (foldMap patternVars' ps) s) t
1066 GuardWhere bs t -> GuardWhere (map (id *** subst s') bs) $ subst s' t
1067 where s' = delEnvs (foldMap patternVars $ map fst bs) s
1068 x -> fmap (subst s) x
1069
1070-------------------------------------------------------------------------------- LambdaCube specific definitions
1071-- TODO: eliminate most of these
1072pattern StarStar = TArr Star Star
1073
1074pattern TCon0 a = TCon Star a
1075pattern TCon1 a b = TApp Star (TCon StarStar a) b
1076pattern TCon2 a b c = TApp Star (TApp StarStar (TCon (TArr Star StarStar) a) b) c
1077pattern TCon2' a b c = TApp Star (TApp StarStar (TCon VecKind a) b) c
1078pattern TCon3' a b c d = TApp Star (TApp StarStar (TApp VecKind (TCon (TArr Star VecKind) a) b) c) d
1079
1080pattern TVec a b = TCon2' "Vec" (ENat a) b
1081pattern TMat a b c = TApp Star (TApp StarStar (TApp VecKind (TCon MatKind "Mat") (ENat a)) (ENat b)) c
1082pattern TSingRecord x t <- TRecord (singletonView -> Just (x, t))
1083singletonView m = case Map.toList m of
1084 [a] -> Just a
1085 _ -> Nothing
1086
1087-- basic types
1088pattern TChar = TCon0 "Char"
1089pattern TString = TCon0 "String"
1090pattern TBool = TCon0 "Bool"
1091pattern TOrdering = TCon0 "Ordering"
1092pattern TWord = TCon0 "Word"
1093pattern TInt = TCon0 "Int"
1094pattern TNat = TCon0 "Nat"
1095pattern TFloat = TCon0 "Float"
1096pattern VecKind = TArr TNat StarStar
1097pattern MatKind = TArr TNat (TArr TNat StarStar)
1098pattern TList a = TCon1 "List" a
1099
1100pattern Ordering = TCon0 "Ordering"
1101
1102-- Semantic
1103pattern Depth a = TCon1 "Depth" a
1104pattern Stencil a = TCon1 "Stencil" a
1105pattern Color a = TCon1 "Color" a
1106
1107-- GADT
1108pattern TFragmentOperation b = TCon1 "FragmentOperation" b
1109pattern TImage b c = TCon2' "Image" b c
1110pattern TInterpolated b = TCon1 "Interpolated" b
1111pattern TFrameBuffer b c = TCon2' "FrameBuffer" b c
1112pattern TSampler = TCon0 "Sampler"
1113
1114pattern ClassN n <- TypeN n where
1115 ClassN n = TypeN' n "class"
1116pattern IsValidOutput = ClassN "ValidOutput"
1117pattern IsTypeLevelNatural = ClassN "TNat"
1118pattern IsValidFrameBuffer = ClassN "ValidFrameBuffer"
1119pattern IsAttributeTuple = ClassN "AttributeTuple"
1120
1121pattern TypeFunS a b <- TypeFun (TypeN a) b where
1122 TypeFunS a b = TypeFun (TypeN' a "typefun") b
1123pattern TFMat a b = TypeFunS "TFMat" [a, b] -- may be data family
1124pattern TFVec a b = TypeFunS "TFVec" [a, b] -- may be data family
1125pattern TFMatVecElem a = TypeFunS "MatVecElem" [a]
1126pattern TFMatVecScalarElem a = TypeFunS "MatVecScalarElem" [a]
1127pattern TFVecScalar a b = TypeFunS "VecScalar" [a, b]
1128pattern TFFTRepr' a = TypeFunS "FTRepr'" [a]
1129pattern TFColorRepr a = TypeFunS "ColorRepr" [a]
1130pattern TFFrameBuffer a = TypeFunS "TFFrameBuffer" [a]
1131pattern TFFragOps a = TypeFunS "FragOps" [a]
1132pattern TFJoinTupleType a b = TypeFunS "JoinTupleType" [a, b]
1133
1134--------------------------------------------------------------------------------
1135-- reducer implemented following
1136-- "A Tutorial Implementation of a Dependently Typed Lambda Calculus"
1137-- Andres Löh, Conor McBride and Wouter Swierstra following
1138
1139reduceNew :: Exp -> Exp
1140reduceNew e = quote (tyOf e) 0 $ eEval mempty e mempty
1141
1142vQuote = VNeutral . NGlobal
1143qname i = ExpN $ "quote" ++ show i
1144
1145quote :: Exp -> Int -> Value -> Exp
1146quote ty ii VStar = Star
1147quote ty ii (VLit i) = ELit i
1148quote ty ii (VCCon t (TupleName _) vs) = ETuple $ zipWith (\ty x -> quote ty ii x) (tupleTypes vs t) vs
1149quote ty ii val@(VCCon t (ConName n) vs) = mkApp t (Exp $ EVar_ t n) vs
1150 where
1151 mkApp t@(Exp (Forall_ _ _ a b)) e (x:xs) = mkApp b (Exp $ EApp_ b e $ quote a ii x) xs
1152 mkApp t e [] = e
1153 mkApp a b c = error $ "mkApp: " ++ ppShow t ++ "; " ++ show val
1154quote ty ii (VLam_ t) = Exp $ ELam_ Nothing (PVar a n) $ quote b (ii + 1) $ t $ vQuote n where
1155 n = qname ii
1156 (a, b) = case ty of
1157 Exp (Forall_ _ _ a b) -> (a, b)
1158 TWildcard -> (TWildcard, TWildcard)
1159 _ -> error $ "quote: " ++ ppShow ty
1160quote ty ii (VPi v f)
1161 = error $ "quote: " ++ "2"
1162quote ty ii (VNeutral n) = neutralQuote ty ii n
1163
1164neutralQuote :: Exp -> Int -> Neutral -> Exp
1165neutralQuote ty ii (NGlobal v) = Exp $ EVar_ ty v
1166neutralQuote ty ii (NQuote k)
1167 = error $ "nquote: " ++ "3"
1168neutralQuote ty ii (NApp_ n v)
1169 = error $ "nquote: " ++ "4"
1170neutralQuote ty ii (NCase ts x)
1171 = error $ "nquote: " ++ "5"
1172neutralQuote ty ii val@(NPrim t n vs) = Exp $ PrimFun ty n (mkApp t vs) 0
1173 where
1174 mkApp t@(Exp (Forall_ _ _ a b)) (x:xs) = quote a ii x: mkApp b xs
1175 mkApp t [] = []
1176 mkApp a c = error $ "mkApp2: " ++ ppShow t ++ "; " ++ show val
1177
1178arity :: Exp -> Int
1179arity (Exp a) = {-trace (ppShow a) $ -} case a of
1180 Forall_ Visible _ _ b -> 1 + arity b
1181 Forall_ Hidden _ _ b -> 1 + arity b
1182 Forall_ Irrelevant _ _ b -> error "arity" --0 + arity b
1183 _ -> 0
1184
1185primType ty l = foldr (~>) ty $ map tyOf l
1186tupleType es = foldr (~>) (tyOf $ ETuple es) $ map tyOf es
1187tupleTypes xs t = f xs t where
1188 f (_: xs) (Exp (Forall_ _ _ a b)) = a: f xs b
1189 f [] (TTuple _) = []
1190 f _ _ = error $ "tupleTypes: " ++ ppShow (xs, t)
1191
1192eEval :: [Name] -> Exp -> Env_ -> Value
1193eEval ne (Exp e) = case e of
1194 Star_ -> const VStar
1195 ELit_ l -> const $ VLit l
1196 EVar_ t v | isConstr v -> -- trace (show i ++ " " ++ ppShow v ++ " :: " ++ ppShow t) $
1197 \d -> ff i id
1198 where
1199 i = arity t
1200 ff :: Int -> ([Value] -> [Value]) -> Value
1201 ff 0 acc = {- trace (ppShow (v, t)) $ -} VCCon t (ConName v) (acc [])
1202 ff i acc = VLam_ $ \x -> ff (i-1) (acc . (x:))
1203 EVar_ _ v -> \d -> maybe (VNeutral $ NGlobal v) (d !!) $ findIndex (== v) ne
1204 TCon_ b v
1205 -> error $ "eEval" ++ "3"
1206 TWildcard_
1207 -> error $ "eEval" ++ "4"
1208 Forall_ v m a b-- Visibility (Maybe v) b b
1209 -> error $ "eEval" ++ "5"
1210 ELam_ _ (PVar _ n) b -> \d -> VLam_ (eEval (n: ne) b . (: d))
1211 ELam_ ty p b -> eEval ne $ Exp $ ELam_ ty (PVar (tyOfPat p) n) $ Case (tyOf b) (Exp $ EVar_ (tyOfPat p) n) [(p, b)]
1212 where n = ExpN "lamvar"
1213 EApp_ _ f x -> \d -> vapp_ (eEval ne f d) (eEval ne x d)
1214 ETyApp_ a b c-- b b b
1215 -> error $ "eEval" ++ "8"
1216 EPrec_ _ _ -- b [(b, b)] -- aux: used only before precedence calculation
1217 -> error $ "eEval" ++ "9"
1218 ELet_ p a b -> eEval ne $ Exp $ EApp_ (tyOf b) (Exp $ ELam_ Nothing p b) a -- TODO
1219 TRecord_ m -- (Map v b)
1220 -> error $ "eEval" ++ "11"
1221 ERecord_ l -- [(Name, b)]
1222 -> error $ "eEval" ++ "12"
1223 EFieldProj_ b n --b Name
1224 -> error $ "eEval" ++ "13"
1225 TTuple_ l -- [b]
1226 -> error $ "eEval" ++ "14"
1227 ETuple_ l -> \d -> VCCon (tupleType l) (TupleName $ length l) $ map ($ d) $ map (eEval ne) l
1228 ENamedRecord_ n l --Name [(Name, b)]
1229 -> error $ "eEval" ++ "16"
1230 WRefl_ b
1231 -> error $ "eEval" ++ "17"
1232 CEq_ b t -- b (TypeFun v b)
1233 -> error $ "eEval" ++ "18"
1234 CUnify_ a b-- b b
1235 -> error $ "eEval" ++ "19"
1236 Split_ a b c-- b b b
1237 -> error $ "eEval" ++ "20"
1238 ETypeSig_ a b --b b
1239 -> error $ "eEval" ++ "21"
1240 Case_ _ a l -> {-traceShow (length l) $ -} let
1241 l' = map ff l
1242 ne' ps = reverse (map fst $ foldMap patternVars ps) ++ ne
1243 ff (PCon _ c ps, x) = (ConName c, foldr llam (eEval (ne' ps) x) ps)
1244 ff (PTuple ps, x) = (TupleName $ length ps, foldr llam (eEval (reverse [n | PVar _ n <- ps] ++ ne) x) ps)
1245 in \d -> case eEval ne a d of
1246 VCCon _ con' args -> head [foldl vapp_ (x d) args | (c, x) <- l', c == con']
1247 VNeutral n -> VNeutral $ NCase (map (id *** ($ d)) l') n
1248 x -> error $ "eEval case: " ++ ppShow x
1249 where
1250 llam :: PatR -> (Env_ -> Value) -> Env_ -> Value
1251 llam (PVar _ n) e = \d -> VLam_ (e . (: d))
1252 llam (Wildcard _) e = e
1253 llam p e = error $ "llam: " ++ ppShow p
1254
1255
1256 WhereBlock_ l a-- [(Name{-v-}, b)] b
1257 -> error $ "eEval" ++ "23"
1258 PrimFun ty n@(ExpN s) l i -> \d -> ff i id d
1259 where
1260 l' = map (eEval ne) l
1261 ff :: Int -> ([Value] -> [Value]) -> Env_ -> Value
1262 ff 0 acc d = f s ({-reverse ??? -} (map ($ d) l') ++ acc [])
1263 ff i acc d = VLam_ $ \x -> ff (i-1) (acc . (x:)) d
1264
1265 f "primIntToFloat" [VInt i] = VFloat $ fromIntegral i
1266 f "primNegateFloat" [VFloat i] = VFloat $ negate i
1267 f "PrimSin" [VFloat i] = VFloat $ sin i
1268 f "PrimCos" [VFloat i] = VFloat $ cos i
1269 f "PrimExp" [VFloat i] = VFloat $ exp i
1270 f "PrimLog" [VFloat i] = VFloat $ log i
1271 f "PrimAbs" [VFloat i] = VFloat $ abs i
1272 f "PrimAddS" [VFloat i, VFloat j] = VFloat $ i + j
1273 f "PrimSubS" [VFloat i, VFloat j] = VFloat $ i - j
1274 f "PrimAddS" [VInt i, VInt j] = VInt $ i + j
1275 f "PrimSubS" [VInt i, VInt j] = VInt $ i - j
1276 f "PrimMulS" [VFloat i, VFloat j] = VFloat $ i * j
1277 f "PrimDivS" [VFloat i, VFloat j] = VFloat $ i / j
1278 f "PrimModS" [VInt i, VInt j] = VInt $ i `mod` j
1279 f "PrimSqrt" [VInt i] = VInt $ round $ sqrt $ fromInteger i
1280 f "PrimIfThenElse" [VTrue,t,_] = t
1281 f "PrimIfThenElse" [VFalse,_,e] = e
1282 f "PrimGreaterThan" [VFloat i, VFloat j] = vBool $ i > j
1283 f "primCompareInt" [VInt i,VInt j] = VOrdering (show $ compare i j)
1284 f "primCompareNat" [VNat i,VNat j] = VOrdering (show $ compare i j)
1285 f "primCompareFloat" [VFloat i,VFloat j] = VOrdering (show $ compare i j)
1286 f "primCompareString" [VString i,VString j] = VOrdering (show $ compare i j)
1287
1288 f s xs = VNeutral $ NPrim (primType ty l) n xs
1289
1290 FunAlts_ i l -- Int{-number of parameters-} [([ParPat b], GuardTree b)]
1291 -> error $ "eEval" ++ "25"
1292 -- TODO: remove
1293 EAlts_ l -- [b] -- function alternatives
1294 -> error $ "eEval" ++ "26"
1295 ENext_ d b --Doc b -- go to next alternative
1296 -> error $ "eEval" ++ "27"
1297
1298--------------------------------------------------------------------------------
1299
1300data Value
1301 = VLam_ (Value -> Value)
1302 | VPi Value (Value -> Value)
1303 | VStar
1304 | VCCon Exp{-constructor type-} ConName [Value]
1305-- | VCon IConName [Value] -- not used
1306 | VLit !Lit
1307 | VNeutral Neutral
1308
1309data Neutral
1310 = NGlobal Name
1311 | NLocal Int -- not used..
1312 | NQuote Int -- not used.. -- TODO
1313 | NApp_ Neutral Value
1314 | NCase [(ConName, Value)] Neutral
1315 | NPrim Exp PrimName [Value]
1316
1317type Env_ = [Value]
1318type NameEnv v = Map.Map N v
1319
1320type PrimName = N
1321
1322pattern VInt i = VLit (LInt i)
1323pattern VNat i = VLit (LNat i)
1324pattern VFloat i = VLit (LFloat i)
1325pattern VString i = VLit (LString i)
1326pattern VFalse = VCCon TBool (ConName (ExpN "False")) []
1327pattern VTrue = VCCon TBool (ConName (ExpN "True")) []
1328pattern VOrdering s = VCCon TOrdering (ConName (ExpN s)) []
1329
1330vBool False = VFalse
1331vBool True = VTrue
1332
1333vapp_ :: Value -> Value -> Value
1334vapp_ (VLam_ f) v = f v
1335vapp_ (VNeutral n) v = VNeutral (NApp_ n v)
1336
1337---------------------- TODO: remove
1338
1339instance Show Lit where show = ppShow
1340instance Show PatR where show = ppShow
1341
1342instance PShow Value where
1343 pShowPrec p = pShowPrec p . quote TWildcard 0
1344
1345instance Show Value where
1346 show = ppShow . quote TWildcard 0
1347instance Show Neutral where
1348 show = show . VNeutral
1349
1350instance Show N where show = ppShow
1351
1352--------------------------------------------------------------------------------
1353
1354type ReduceM = ExceptT String (State Int)
1355
1356isNext (Exp a) = case a of
1357 ENext_ _ _ -> Nothing
1358 e -> Just $ Exp e
1359
1360e &. f = maybe e f $ isNext e
1361e >>=. f = isNext e >>= f
1362
1363msum' (x: xs) = fromMaybe (msum' xs) $ isNext x
1364msum' _ = error "pattern match failure."
1365
1366reduceFail' msg = Nothing
1367
1368-- full reduction
1369-- TODO! reduction under lambda needs alpha-conversion!
1370reduce :: Exp -> Exp
1371reduce = reduce_ False
1372reduce_ lam e = reduceHNF_ lam e & \(Exp e) -> Exp $ case e of
1373-- ELam_ _ (PVar _ n) (EApp (Exp f) (EVar n')) | n == n' && n `Set.notMember` freeVars (Exp f) -> f
1374 ELam_ a b c -> ELam_ (reduce_ lam <$> a) b (reduce_ True c)
1375-- ELet_ p x e -> ELet_ p x e
1376-- Forall_ a b c d -> Forall_ a b (reduce_ lam c) (reduce_ True d)
1377 e -> reduce_ lam <$> e
1378
1379-- don't reduce under lambda
1380reduce' :: Exp -> Exp
1381reduce' e = reduceHNF e & \(Exp e) -> case e of
1382 ELam_ _ _ _ -> Exp e
1383 Forall_ a b c d -> Exp e -- TODO: reduce c?
1384 _ -> Exp $ reduce' <$> e
1385
1386reduceHNF :: Exp -> Exp -- Left: pattern match failure
1387reduceHNF = reduceHNF_ False
1388
1389isSTy = \case
1390{-
1391 TInt -> True
1392 TBool -> True
1393 TFloat -> True
1394 TVec n t -> n `elem` [2,3,4] && t `elem` [TFloat, TBool, TInt]
1395 TMat n m TFloat -> n `elem` [2,3,4] && n == m
1396-}
1397 _ -> False
1398
1399reduceHNF_ lam (Exp exp) = case exp of
1400
1401 ELet_ p x e
1402 | lam && isSTy (tyOf x) -> keep
1403 | otherwise -> reduceHNF $ TApp (tyOf e) (ELam p e) x
1404
1405 PrimFun k (ExpN f) acc 0 -> evalPrimFun keep id k f $ map reduceHNF (reverse acc)
1406
1407 EAlts_ (map reduceHNF -> es) -> msum' $ es ++ error ("pattern match failure: " ++ ppShow es)
1408 EApp_ _ f x -> reduceHNF f &. \(Exp f) -> case f of
1409
1410 PrimFun (TArr _ k) f acc i
1411 | i > 0 -> reduceHNF $ Exp $ PrimFun k f (x: acc) (i-1)
1412-- | otherwise -> error $ "too much argument for primfun " ++ ppShow f ++ ": " ++ ppShow exp
1413
1414 EFieldProj_ _ fi -> reduceHNF x &. \case
1415 ERecord fs -> case [e | (fi', e) <- fs, fi' == fi] of
1416 [e] -> reduceHNF e
1417 e -> case fi of
1418 ExpN "x" -> case e of
1419 A4 "V4" x y z w -> x
1420 A3 "V3" x y z -> x
1421 A2 "V2" x y -> x
1422 _ -> keep
1423 ExpN "y" -> case e of
1424 A4 "V4" x y z w -> y
1425 A3 "V3" x y z -> y
1426 A2 "V2" x y -> y
1427 _ -> keep
1428 ExpN "z" -> case e of
1429 A4 "V4" x y z w -> z
1430 A3 "V3" x y z -> z
1431 _ -> keep
1432 ExpN "w" -> case e of
1433 A4 "V4" x y z w -> w
1434 _ -> keep
1435 _ -> keep
1436
1437 ELam_ _ p e -> bind' (pShow (p, getTag e)) (matchPattern (reduce' x) p) $ \case
1438 Just m' -> reduceHNF $ subst m' e
1439 _ -> keep
1440 _ -> keep
1441 _ -> keep
1442 where
1443 reduceHNF = reduceHNF_ lam
1444
1445 keep = Exp exp
1446
1447 bind' err e f = maybe (Exp $ ENext_ err $ tyOf keep) f e
1448
1449 -- TODO: make this more efficient (memoize reduced expressions)
1450 matchPattern :: Exp -> Pat -> Maybe (Maybe Subst) -- Left: pattern match failure; Right Nothing: can't reduce
1451 matchPattern e = \case
1452 Wildcard _ -> return $ Just mempty
1453 PLit l -> e >>=. \case
1454 ELit l'
1455 | l == l' -> return $ Just mempty
1456 | otherwise -> reduceFail' $ "literals doesn't match:" <+> pShow (l, l')
1457 _ -> return Nothing
1458 PVar _ v -> return $ Just $ singSubst' v e
1459 PTuple ps -> e >>=. \e -> case e of
1460 ETuple xs -> fmap mconcat . sequence <$> sequence (zipWith matchPattern xs ps)
1461 _ -> return Nothing
1462 PCon t c ps -> getApp [] e >>= \case
1463 Just (c', xs)
1464 | c == c' && length xs == length ps -> fmap mconcat . sequence <$> sequence (zipWith matchPattern xs ps)
1465 | otherwise -> reduceFail' $ "constructors doesn't match:" <+> pShow (c, c')
1466 _ -> return Nothing
1467 p -> error $ "matchPattern: " ++ ppShow p
1468 where
1469 getApp acc e = e >>=. \e -> case e of
1470 EApp a b -> getApp (b: acc) a
1471 EVar n | isConstr n -> return $ Just (n, acc)
1472 _ -> return Nothing
1473
1474evalPrimFun :: Exp -> (Exp -> Exp) -> Exp -> String -> [Exp] -> Exp
1475evalPrimFun keep red k = f where
1476 f "primIntToFloat" [EInt i] = EFloat $ fromIntegral i
1477 f "primNegateFloat" [EFloat i] = EFloat $ negate i
1478 f "PrimSin" [EFloat i] = EFloat $ sin i
1479 f "PrimCos" [EFloat i] = EFloat $ cos i
1480 f "PrimExp" [EFloat i] = EFloat $ exp i
1481 f "PrimLog" [EFloat i] = EFloat $ log i
1482 f "PrimAbs" [EFloat i] = EFloat $ abs i
1483 f "PrimAddS" [EFloat i, EFloat j] = EFloat $ i + j
1484 f "PrimSubS" [EFloat i, EFloat j] = EFloat $ i - j
1485 f "PrimSubS" [EInt i, EInt j] = EInt $ i - j
1486 f "PrimMulS" [EFloat i, EFloat j] = EFloat $ i * j
1487 f "PrimDivS" [EFloat i, EFloat j] = EFloat $ i / j
1488 f "PrimModS" [EInt i, EInt j] = EInt $ i `mod` j
1489 f "PrimSqrt" [EInt i] = EInt $ round $ sqrt $ fromInteger i
1490 f "PrimIfThenElse" [A0 "True",t,_] = red t
1491 f "PrimIfThenElse" [A0 "False",_,e] = red e
1492 f "PrimGreaterThan" [EFloat i, EFloat j] = if i > j then TVar TBool (ExpN "True") else TVar TBool (ExpN "False")
1493 f "primCompareInt" [EInt i,EInt j] = Con0 Ordering (show $ compare i j)
1494 f "primCompareNat" [ENat i,ENat j] = Con0 Ordering (show $ compare i j)
1495 f "primCompareFloat" [EFloat i,EFloat j] = Con0 Ordering (show $ compare i j)
1496 f "primCompareString" [EString i,EString j] = Con0 Ordering (show $ compare i j)
1497 f _ _ = keep
1498
1499pattern Prim a b <- Exp (PrimFun _ (ExpN a) b 0)
1500pattern Prim1 a b <- Prim a [b]
1501pattern Prim2 a b c <- Prim a [c, b]
1502pattern Prim3 a b c d <- Prim a [d, c, b]
1503
1504-------------------------------------------------------------------------------- Pretty show instances
1505
1506-- TODO: eliminate
1507showN :: N -> String
1508showN (N _ qs s _) = show $ hcat (punctuate (pShow '.') $ map text $ qs ++ [s])
1509
1510showVar (N q _ n (NameInfo _ i)) = pShow q <> text n <> "{" <> i <> "}"
1511
1512instance PShow N where
1513 pShowPrec p = \case
1514 N _ qs s (NameInfo _ i) -> hcat (punctuate (pShow '.') $ map text $ qs ++ [s]) -- <> "{" <> i <> "}"
1515
1516instance PShow NameSpace where
1517 pShowPrec p = \case
1518 TypeNS -> "'"
1519 ExpNS -> ""
1520
1521instance Show ConName where show = ppShow
1522instance PShow ConName where
1523 pShowPrec p = \case
1524 ConName n -> pShow n
1525-- ConLit l -> pShow l
1526 TupleName i -> "Tuple" <> pShow i
1527
1528--instance PShow IdN where pShowPrec p (IdN n) = pShowPrec p n
1529
1530instance PShow Lit where
1531 pShowPrec p = \case
1532 LInt i -> pShow i
1533 LChar i -> text $ show i
1534 LString i -> text $ show i
1535 LFloat i -> pShow i
1536 LNat i -> pShow i
1537
1538-- Exp k i -> pInfix (-2) "::" p i k
1539instance (PShow v, PShow p, PShow b) => PShow (Exp_ v p b) where
1540 pShowPrec p = \case
1541 EPrec_ e es -> pApps p e $ concatMap (\(a, b) -> [a, b]) es
1542 ELit_ l -> pShowPrec p l
1543 EVar_ k v -> pShowPrec p v
1544 EApp_ k a b -> pApp p a b
1545 ETyApp_ k a b -> pTyApp p a b
1546 ETuple_ a -> tupled $ map pShow a
1547 ELam_ Nothing p b -> pParens True ("\\" <> pShow p </> "->" <+> pShow b)
1548 ELam_ _ p b -> pParens True ("\\" <> braces (pShow p) </> "->" <+> pShow b)
1549 ETypeSig_ b t -> pShow b </> "::" <+> pShow t
1550 ELet_ a b c -> "let" <+> pShow a </> "=" <+> pShow b </> "in" <+> pShow c
1551 ENamedRecord_ n xs -> pShow n <+> showRecord xs
1552 ERecord_ xs -> showRecord xs
1553 EFieldProj_ k n -> "." <> pShow n
1554 EAlts_ b -> braces (vcat $ punctuate (pShow ';') $ map pShow b)
1555 Case_ t x xs -> "case" <+> pShow x <+> "of" </> vcat [pShow p <+> "->" <+> pShow e | (p, e) <- xs]
1556 ENext_ info k -> "SKIP" <+> info
1557 PrimFun k a b c -> "primfun" <+> pShow a <+> pShow b <+> pShow c
1558
1559 Star_ -> "*"
1560 TCon_ k n -> pShow n
1561 Forall_ Visible Nothing a b -> pInfixr' (-1) "->" p a b
1562 Forall_ Irrelevant Nothing a b -> pInfixr' (-1) "==>" p a b
1563 Forall_ Hidden Nothing a b -> pInfixr' (-1) "=>" p a b
1564 Forall_ Visible (Just n) a b -> "forall" <+> pParens True (pShow n </> "::" <+> pShow a) <> "." <+> pShow b
1565 Forall_ Irrelevant (Just n) a b -> "forall" <+> "." <> braces (pShow n </> "::" <+> pShow a) <> "." <+> pShow b
1566 Forall_ Hidden (Just n) a b -> "forall" <+> braces (pShow n </> "::" <+> pShow a) <> "." <+> pShow b
1567 TTuple_ a -> tupled $ map pShow a
1568 TRecord_ m -> "Record" <+> showRecord (Map.toList m)
1569 CEq_ a b -> pShow a <+> "~" <+> pShow b
1570 CUnify_ a b -> pShow a <+> "~" <+> pShow b
1571 Split_ a b c -> pShow a <+> "<-" <+> "(" <> pShow b <> "," <+> pShow c <> ")"
1572 WRefl_ k -> "refl" <+> pShow k
1573 TWildcard_ -> "twildcard"
1574 FunAlts_ i as -> "alts" <+> pShow i </> vcat [hsep (map (hcat . intersperse "@" . map pShow) ps) <+> "->" <+> pShow t | (ps, t) <- as]
1575--- Int{-number of parameters-} [([ParPat b], GuardTree b)]
1576
1577getConstraints = \case
1578 Exp (Forall_ (hidden -> True) n c t) -> ((n, c):) *** id $ getConstraints t
1579 t -> ([], t)
1580
1581showConstraints cs x
1582 = (case cs of [(Nothing, c)] -> pShow c; _ -> tupled (map pShow' cs))
1583 </> "=>" <+> pShowPrec (-2) x
1584 where
1585 pShow' (Nothing, x) = pShow x
1586 pShow' (Just n, x) = pShow n <+> "::" <+> pShow x
1587
1588instance PShow e => PShow (Pat' e) where
1589 pShowPrec p = \case
1590 PatVar v -> pShow v
1591 PatLit l -> pShow l
1592 PatCon n ps -> hsep $ pShow n: map pShow ps
1593 PatPrec p ps -> hsep $ map pShow $ p: concatMap (\(x,y) -> [x,y]) ps
1594 -- | ViewPat e (ParPat e)
1595
1596instance PShow e => PShow (GuardTree e) where
1597 pShowPrec p = \case
1598 GuardCon e c ps t -> pShow (PatCon c ps) <+> "<-" <+> pShow e <+> "->" <+> pShow t
1599 GuardPat e p t -> pShow p <+> "<-" <+> pShow e <+> "->" <+> pShow t
1600 -- GuardWhere (Binds e) (GuardTree e)
1601 GuardAlts as -> braces $ vcat $ map pShow as
1602 GuardExp e -> pShow e
1603
1604instance PShow Exp where
1605 pShowPrec p = \case
1606 (getConstraints -> (cs@(_:_), t)) -> showConstraints cs t
1607 t -> case getLams t of
1608 ([], Exp e) -> pShowPrec p e
1609 (ps, Exp e) -> pParens (p > 0) $ "\\" <> hsep (map (pShowPrec 10) ps) </> "->" <+> pShow e
1610 where
1611 getLams (ELam p e) = (p:) *** id $ getLams e
1612 getLams e = ([], e)
1613
1614instance (PShow c, PShow v, PShow b) => PShow (Pat_ t c v b) where
1615 pShowPrec p = \case
1616 PLit_ l -> pShow l
1617 PVar_ t v -> pShow v
1618 PCon_ t s xs -> pApps p s xs
1619 PTuple_ a -> tupled $ map pShow a
1620 PRecord_ xs -> "Record" <+> showRecord xs
1621 PAt_ v p -> pShow v <> "@" <> pShow p
1622 Wildcard_ t -> "_"
1623 PPrec_ e es -> pApps p e $ concatMap (\(a, b) -> [a, b]) es
1624
1625instance PShow Pat where
1626 pShowPrec p (Pat e) = pShowPrec p e
1627
1628instance (PShow n, PShow a) => PShow (TypeFun n a) where
1629 pShowPrec p (TypeFun s xs) = pApps p s xs
1630
1631
1632instance PShow TEnv where
1633 pShowPrec p (TEnv e) = showRecord $ Map.toList e
1634
1635instance PShow Item where
1636 pShowPrec p = eitherItem (\r -> (("Subst" <> if r then "!" else "") <+>) . pShow) (\rigid -> (("Sig" <> if rigid then "!" else "") <+>) . pShow)
1637
1638instance PShow Range where
1639 pShowPrec p = \case
1640 Range a b -> text (show a) <+> "--" <+> text (show b)
1641 NoRange -> ""
1642
1643instance PShow Definition where
1644 pShowPrec p = \case
1645 DValueDef False (ValueDef False x _) -> "ValueDef" <+> pShow x
1646 DValueDef False (ValueDef rec x _) -> "ValueDef rec" <+> pShow x
1647 DValueDef True (ValueDef False x _) -> "ValueDef [instance]" <+> pShow x
1648 DAxiom (TypeSig x _) -> "axiom" <+> pShow x
1649 DDataDef n _ _ -> "data" <+> pShow n
1650 GADT n _ _ -> "gadt" <+> pShow n
1651 ClassDef _ n _ _ -> "class" <+> pShow n
1652 InstanceDef _ n _ _ -> "instance" <+> pShow n
1653 TypeFamilyDef n _ _ -> "type family" <+> pShow n
1654 -- used only during parsing
1655 PreValueDef (_, n) _ _ -> "pre valuedef" <+> pShow n
1656 DTypeSig (TypeSig n _) -> "typesig" <+> pShow n
1657 ForeignDef n _ -> "foreign" <+> pShow n
1658 PrecDef n p -> "precdef" <+> pShow n
1659
1660instance PShow FixityDir where
1661 pShowPrec p = \case
1662 FDLeft -> "infixl"
1663 FDRight -> "infixr"
1664
1665-------------------------------------------------------------------------------- WriterT'
1666
1667class Monoid' e where
1668 type MonoidConstraint e :: * -> *
1669 mempty' :: e
1670 mappend' :: e -> e -> MonoidConstraint e e
1671
1672newtype WriterT' e m a
1673 = WriterT' {runWriterT' :: m (e, a)}
1674 deriving (Functor,Foldable,Traversable)
1675
1676instance (Monoid' e) => MonadTrans (WriterT' e) where
1677 lift m = WriterT' $ (,) mempty' <$> m
1678
1679instance forall m e . (Monoid' e, MonoidConstraint e ~ m, Monad m) => Applicative (WriterT' e m) where
1680 pure a = WriterT' $ pure (mempty' :: e, a)
1681 a <*> b = join $ (<$> b) <$> a
1682
1683instance (Monoid' e, MonoidConstraint e ~ m, Monad m) => Monad (WriterT' e m) where
1684 WriterT' m >>= f = WriterT' $ do
1685 (e1, a) <- m
1686 (e2, b) <- runWriterT' $ f a
1687 e <- mappend' e1 e2
1688 return (e, b)
1689
1690instance (Monoid' e, MonoidConstraint e ~ m, MonadReader r m) => MonadReader r (WriterT' e m) where
1691 ask = lift ask
1692 local f (WriterT' m) = WriterT' $ local f m
1693
1694instance (Monoid' e, MonoidConstraint e ~ m, MonadWriter w m) => MonadWriter w (WriterT' e m) where
1695 tell = lift . tell
1696 listen = error "WriterT' listen"
1697 pass = error "WriterT' pass"
1698
1699instance (Monoid' e, MonoidConstraint e ~ m, MonadState s m) => MonadState s (WriterT' e m) where
1700 state f = lift $ state f
1701
1702instance (Monoid' e, MonoidConstraint e ~ m, MonadError err m) => MonadError err (WriterT' e m) where
1703 catchError (WriterT' m) f = WriterT' $ catchError m $ runWriterT' <$> f
1704 throwError e = lift $ throwError e
1705
1706mapWriterT' f (WriterT' m) = WriterT' $ f m
1707
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-30 00:15:14 +0000