git.iko.soy/Idris-dev
on 7afa310 help sign in
Idris-dev/src/Idris/Core/TT.hs
1421 lines 54 kB history raw
1{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, DeriveFunctor #-}
3{-| TT is the core language of Idris. The language has:
5 * Full dependent types
7 * A hierarchy of universes, with cumulativity: Type : Type1, Type1 : Type2, ...
9 * Pattern matching letrec binding
11 * (primitive types defined externally)
13 Some technical stuff:
15 * Typechecker is kept as simple as possible - no unification, just a checker for incomplete terms.
17 * We have a simple collection of tactics which we use to elaborate source
18 programs with implicit syntax into fully explicit terms.
19-}
21module Idris.Core.TT(module Idris.Core.TT, module Idris.Core.TC) where
23import Idris.Core.TC
25import Control.Monad.State.Strict
26import Control.Monad.Trans.Error (Error(..))
27import Debug.Trace
28import qualified Data.Map.Strict as Map
29import Data.Char
30import Numeric (showIntAtBase)
31import qualified Data.Text as T
32import Data.List
33import Data.Maybe (listToMaybe)
34import Data.Foldable (Foldable)
35import Data.Traversable (Traversable)
36import Data.Vector.Unboxed (Vector)
37import qualified Data.Vector.Unboxed as V
38import qualified Data.Binary as B
39import Data.Binary hiding (get, put)
40import Foreign.Storable (sizeOf)
42import Util.Pretty hiding (Str)
44data Option = TTypeInTType
45 | CheckConv
46 deriving Eq
48-- | Source location. These are typically produced by the parser 'Idris.Parser.getFC'
49data FC = FC { fc_fname :: String, -- ^ Filename
50 fc_start :: (Int, Int), -- ^ Line and column numbers for the start of the location span
51 fc_end :: (Int, Int) -- ^ Line and column numbers for the end of the location span
52 }
54-- | Ignore source location equality (so deriving classes do not compare FCs)
55instance Eq FC where
56 _ == _ = True
58-- | FC with equality
59newtype FC' = FC' { unwrapFC :: FC }
61instance Eq FC' where
62 FC' fc == FC' fc' = fcEq fc fc'
63 where fcEq (FC n s e) (FC n' s' e') = n == n' && s == s' && e == e'
65-- | Empty source location
66emptyFC :: FC
67emptyFC = fileFC ""
69-- | Source location with file only
70fileFC :: String -> FC
71fileFC s = FC s (0, 0) (0, 0)
73{-!
74deriving instance Binary FC
75deriving instance NFData FC
76!-}
78instance Sized FC where
79 size (FC f s e) = 4 + length f
81instance Show FC where
82 show (FC f s e) = f ++ ":" ++ showLC s e
83 where showLC (sl, sc) (el, ec) | sl == el && sc == ec = show sl ++ ":" ++ show sc
84 | sl == el = show sl ++ ":" ++ show sc ++ "-" ++ show ec
85 | otherwise = show sl ++ ":" ++ show sc ++ "-" ++ show el ++ ":" ++ show ec
87-- | Output annotation for pretty-printed name - decides colour
88data NameOutput = TypeOutput | FunOutput | DataOutput | MetavarOutput | PostulateOutput
90-- | Text formatting output
91data TextFormatting = BoldText | ItalicText | UnderlineText
93-- | Output annotations for pretty-printing
94data OutputAnnotation = AnnName Name (Maybe NameOutput) (Maybe String) (Maybe String)
95 -- ^^ The name, classification, docs overview, and pretty-printed type
96 | AnnBoundName Name Bool
97 -- ^^ The name and whether it is implicit
98 | AnnConst Const
99 | AnnData String String -- ^ type, doc overview
100 | AnnType String String -- ^ name, doc overview
101 | AnnKeyword
102 | AnnFC FC
103 | AnnTextFmt TextFormatting
104 | AnnTerm [(Name, Bool)] (TT Name) -- ^ pprint bound vars, original term
105 | AnnSearchResult Ordering -- ^ more general, isomorphic, or more specific
107-- | Used for error reflection
108data ErrorReportPart = TextPart String
109 | NamePart Name
110 | TermPart Term
111 | SubReport [ErrorReportPart]
112 deriving (Show, Eq)
115-- Please remember to keep Err synchronised with
116-- Language.Reflection.Errors.Err in the stdlib!
118-- | Idris errors. Used as exceptions in the compiler, but reported to users
119-- if they reach the top level.
120data Err' t
121 = Msg String
122 | InternalMsg String
123 | CantUnify Bool t t (Err' t) [(Name, t)] Int
124 -- Int is 'score' - how much we did unify
125 -- Bool indicates recoverability, True indicates more info may make
126 -- unification succeed
127 | InfiniteUnify Name t [(Name, t)]
128 | CantConvert t t [(Name, t)]
129 | CantSolveGoal t [(Name, t)]
130 | UnifyScope Name Name t [(Name, t)]
131 | CantInferType String
132 | NonFunctionType t t
133 | NotEquality t t
134 | TooManyArguments Name
135 | CantIntroduce t
136 | NoSuchVariable Name
137 | NoTypeDecl Name
138 | NotInjective t t t
139 | CantResolve t
140 | CantResolveAlts [Name]
141 | IncompleteTerm t
142 | UniverseError
143 | UniqueError Universe Name
144 | UniqueKindError Universe Name
145 | ProgramLineComment
146 | Inaccessible Name
147 | NonCollapsiblePostulate Name
148 | AlreadyDefined Name
149 | ProofSearchFail (Err' t)
150 | NoRewriting t
151 | At FC (Err' t)
152 | Elaborating String Name (Err' t)
153 | ElaboratingArg Name Name [(Name, Name)] (Err' t)
154 | ProviderError String
155 | LoadingFailed String (Err' t)
156 | ReflectionError [[ErrorReportPart]] (Err' t)
157 | ReflectionFailed String (Err' t)
158 deriving (Eq, Functor)
160type Err = Err' Term
162{-!
163deriving instance NFData Err
164!-}
166instance Sized ErrorReportPart where
167 size (TextPart msg) = 1 + length msg
168 size (TermPart t) = 1 + size t
169 size (NamePart n) = 1 + size n
170 size (SubReport rs) = 1 + size rs
172instance Sized Err where
173 size (Msg msg) = length msg
174 size (InternalMsg msg) = length msg
175 size (CantUnify _ left right err _ score) = size left + size right + size err
176 size (InfiniteUnify _ right _) = size right
177 size (CantConvert left right _) = size left + size right
178 size (UnifyScope _ _ right _) = size right
179 size (NoSuchVariable name) = size name
180 size (NoTypeDecl name) = size name
181 size (NotInjective l c r) = size l + size c + size r
182 size (CantResolve trm) = size trm
183 size (NoRewriting trm) = size trm
184 size (CantResolveAlts _) = 1
185 size (IncompleteTerm trm) = size trm
186 size UniverseError = 1
187 size ProgramLineComment = 1
188 size (At fc err) = size fc + size err
189 size (Elaborating _ n err) = size err
190 size (ElaboratingArg _ _ _ err) = size err
191 size (ProviderError msg) = length msg
192 size (LoadingFailed fn e) = 1 + length fn + size e
193 size _ = 1
195score :: Err -> Int
196score (CantUnify _ _ _ m _ s) = s + score m
197score (CantResolve _) = 20
198score (NoSuchVariable _) = 1000
199score (ProofSearchFail e) = score e
200score (CantSolveGoal _ _) = 100000
201score (InternalMsg _) = -1
202score (At _ e) = score e
203score (ElaboratingArg _ _ _ e) = score e
204score (Elaborating _ _ e) = score e
205score _ = 0
207instance Show Err where
208 show (Msg s) = s
209 show (InternalMsg s) = "Internal error: " ++ show s
210 show (CantUnify rec l r e sc i) = "CantUnify " ++ show rec ++ " " ++
211 show l ++ " " ++ show r ++ " " ++
212 show e ++ " in " ++ show sc ++ " " ++ show i
213 show (CantSolveGoal g _) = "CantSolve " ++ show g
214 show (Inaccessible n) = show n ++ " is not an accessible pattern variable"
215 show (ProviderError msg) = "Type provider error: " ++ msg
216 show (LoadingFailed fn e) = "Loading " ++ fn ++ " failed: (TT) " ++ show e
217 show ProgramLineComment = "Program line next to comment"
218 show (At f e) = show f ++ ":" ++ show e
219 show (ElaboratingArg f x prev e) = "Elaborating " ++ show f ++ " arg " ++
220 show x ++ ": " ++ show e
221 show (Elaborating what n e) = "Elaborating " ++ what ++ show n ++ ":" ++ show e
222 show (ProofSearchFail e) = "Proof search fail: " ++ show e
223 show _ = "Error"
225instance Pretty Err OutputAnnotation where
226 pretty (Msg m) = text m
227 pretty (CantUnify _ l r e _ i) =
228 text "Cannot unify" <+> colon <+> pretty l <+> text "and" <+> pretty r <+>
229 nest nestingSize (text "where" <+> pretty e <+> text "with" <+> (text . show $ i))
230 pretty (ProviderError msg) = text msg
231 pretty err@(LoadingFailed _ _) = text (show err)
232 pretty _ = text "Error"
234instance Error Err where
235 strMsg = InternalMsg
237type TC = TC' Err
239instance (Pretty a OutputAnnotation) => Pretty (TC a) OutputAnnotation where
240 pretty (OK ok) = pretty ok
241 pretty (Error err) =
242 text "Error" <+> colon <+> pretty err
244instance Show a => Show (TC a) where
245 show (OK x) = show x
246 show (Error str) = "Error: " ++ show str
248tfail :: Err -> TC a
249tfail e = Error e
251failMsg :: String -> TC a
252failMsg str = Error (Msg str)
254trun :: FC -> TC a -> TC a
255trun fc (OK a) = OK a
256trun fc (Error e) = Error (At fc e)
258discard :: Monad m => m a -> m ()
259discard f = f >> return ()
261showSep :: String -> [String] -> String
262showSep sep [] = ""
263showSep sep [x] = x
264showSep sep (x:xs) = x ++ sep ++ showSep sep xs
266pmap f (x, y) = (f x, f y)
268traceWhen True msg a = trace msg a
269traceWhen False _ a = a
271-- RAW TERMS ----------------------------------------------------------------
273-- | Names are hierarchies of strings, describing scope (so no danger of
274-- duplicate names, but need to be careful on lookup).
275data Name = UN T.Text -- ^ User-provided name
276 | NS Name [T.Text] -- ^ Root, namespaces
277 | MN Int T.Text -- ^ Machine chosen names
278 | NErased -- ^ Name of something which is never used in scope
279 | SN SpecialName -- ^ Decorated function names
280 | SymRef Int -- ^ Reference to IBC file symbol table (used during serialisation)
281 deriving (Eq, Ord)
283txt :: String -> T.Text
284txt = T.pack
286str :: T.Text -> String
287str = T.unpack
289tnull :: T.Text -> Bool
290tnull = T.null
292thead :: T.Text -> Char
293thead = T.head
295-- Smart constructors for names, using old String style
296sUN :: String -> Name
297sUN s = UN (txt s)
299sNS :: Name -> [String] -> Name
300sNS n ss = NS n (map txt ss)
302sMN :: Int -> String -> Name
303sMN i s = MN i (txt s)
305{-!
306deriving instance Binary Name
307deriving instance NFData Name
308!-}
310data SpecialName = WhereN Int Name Name
311 | WithN Int Name
312 | InstanceN Name [T.Text]
313 | ParentN Name T.Text
314 | MethodN Name
315 | CaseN Name
316 | ElimN Name
317 | InstanceCtorN Name
318 deriving (Eq, Ord)
319{-!
320deriving instance Binary SpecialName
321deriving instance NFData SpecialName
322!-}
324sInstanceN :: Name -> [String] -> SpecialName
325sInstanceN n ss = InstanceN n (map T.pack ss)
327sParentN :: Name -> String -> SpecialName
328sParentN n s = ParentN n (T.pack s)
330instance Sized Name where
331 size (UN n) = 1
332 size (NS n els) = 1 + length els
333 size (MN i n) = 1
334 size _ = 1
336instance Pretty Name OutputAnnotation where
337 pretty n@(UN n') = annotate (AnnName n Nothing Nothing Nothing) $ text (T.unpack n')
338 pretty n@(NS un s) = annotate (AnnName n Nothing Nothing Nothing) . noAnnotate $ pretty un
339 pretty n@(MN i s) = annotate (AnnName n Nothing Nothing Nothing) $
340 lbrace <+> text (T.unpack s) <+> (text . show $ i) <+> rbrace
341 pretty n@(SN s) = annotate (AnnName n Nothing Nothing Nothing) $ text (show s)
343instance Pretty [Name] OutputAnnotation where
344 pretty = encloseSep empty empty comma . map pretty
346instance Show Name where
347 show (UN n) = str n
348 show (NS n s) = showSep "." (map T.unpack (reverse s)) ++ "." ++ show n
349 show (MN _ u) | u == txt "underscore" = "_"
350 show (MN i s) = "{" ++ str s ++ show i ++ "}"
351 show (SN s) = show s
352 show NErased = "_"
354instance Show SpecialName where
355 show (WhereN i p c) = show p ++ ", " ++ show c
356 show (WithN i n) = "with block in " ++ show n
357 show (InstanceN cl inst) = showSep ", " (map T.unpack inst) ++ " instance of " ++ show cl
358 show (MethodN m) = "method " ++ show m
359 show (ParentN p c) = show p ++ "#" ++ T.unpack c
360 show (CaseN n) = "case block in " ++ show n
361 show (ElimN n) = "<<" ++ show n ++ " eliminator>>"
362 show (InstanceCtorN n) = "constructor of " ++ show n
364-- Show a name in a way decorated for code generation, not human reading
365showCG :: Name -> String
366showCG (UN n) = T.unpack n
367showCG (NS n s) = showSep "." (map T.unpack (reverse s)) ++ "." ++ showCG n
368showCG (MN _ u) | u == txt "underscore" = "_"
369showCG (MN i s) = "{" ++ T.unpack s ++ show i ++ "}"
370showCG (SN s) = showCG' s
371 where showCG' (WhereN i p c) = showCG p ++ ":" ++ showCG c ++ ":" ++ show i
372 showCG' (WithN i n) = "_" ++ showCG n ++ "_with_" ++ show i
373 showCG' (InstanceN cl inst) = '@':showCG cl ++ '$':showSep ":" (map T.unpack inst)
374 showCG' (MethodN m) = '!':showCG m
375 showCG' (ParentN p c) = showCG p ++ "#" ++ show c
376 showCG' (CaseN c) = showCG c ++ "_case"
377 showCG' (ElimN sn) = showCG sn ++ "_elim"
378showCG NErased = "_"
381-- |Contexts allow us to map names to things. A root name maps to a collection
382-- of things in different namespaces with that name.
383type Ctxt a = Map.Map Name (Map.Map Name a)
384emptyContext = Map.empty
386mapCtxt :: (a -> b) -> Ctxt a -> Ctxt b
387mapCtxt = fmap . fmap
389-- |Return True if the argument 'Name' should be interpreted as the name of a
390-- typeclass.
391tcname (UN xs) | T.null xs = False
392 | otherwise = T.head xs == '@'
393tcname (NS n _) = tcname n
394tcname (SN (InstanceN _ _)) = True
395tcname (SN (MethodN _)) = True
396tcname (SN (ParentN _ _)) = True
397tcname _ = False
399implicitable (NS n _) = implicitable n
400implicitable (UN xs) | T.null xs = False
401 | otherwise = isLower (T.head xs) || T.head xs == '_'
402implicitable (MN _ x) = not (tnull x) && thead x /= '_'
403implicitable _ = False
405nsroot (NS n _) = n
406nsroot n = n
408-- this will overwrite already existing definitions
409addDef :: Name -> a -> Ctxt a -> Ctxt a
410addDef n v ctxt = case Map.lookup (nsroot n) ctxt of
411 Nothing -> Map.insert (nsroot n)
412 (Map.insert n v Map.empty) ctxt
413 Just xs -> Map.insert (nsroot n)
414 (Map.insert n v xs) ctxt
416{-| Look up a name in the context, given an optional namespace.
417 The name (n) may itself have a (partial) namespace given.
419 Rules for resolution:
421 - if an explicit namespace is given, return the names which match it. If none
422 match, return all names.
424 - if the name has has explicit namespace given, return the names which match it
425 and ignore the given namespace.
427 - otherwise, return all names.
429-}
431lookupCtxtName :: Name -> Ctxt a -> [(Name, a)]
432lookupCtxtName n ctxt = case Map.lookup (nsroot n) ctxt of
433 Just xs -> filterNS (Map.toList xs)
434 Nothing -> []
435 where
436 filterNS [] = []
437 filterNS ((found, v) : xs)
438 | nsmatch n found = (found, v) : filterNS xs
439 | otherwise = filterNS xs
441 nsmatch (NS n ns) (NS p ps) = ns `isPrefixOf` ps
442 nsmatch (NS _ _) _ = False
443 nsmatch looking found = True
445lookupCtxt :: Name -> Ctxt a -> [a]
446lookupCtxt n ctxt = map snd (lookupCtxtName n ctxt)
448lookupCtxtExact :: Name -> Ctxt a -> Maybe a
449lookupCtxtExact n ctxt = listToMaybe [ v | (nm, v) <- lookupCtxtName n ctxt, nm == n]
451deleteDefExact :: Name -> Ctxt a -> Ctxt a
452deleteDefExact n = Map.adjust (Map.delete n) (nsroot n)
454updateDef :: Name -> (a -> a) -> Ctxt a -> Ctxt a
455updateDef n f ctxt
456 = let ds = lookupCtxtName n ctxt in
457 foldr (\ (n, t) c -> addDef n (f t) c) ctxt ds
459toAlist :: Ctxt a -> [(Name, a)]
460toAlist ctxt = let allns = map snd (Map.toList ctxt) in
461 concatMap (Map.toList) allns
463addAlist :: Show a => [(Name, a)] -> Ctxt a -> Ctxt a
464addAlist [] ctxt = ctxt
465addAlist ((n, tm) : ds) ctxt = addDef n tm (addAlist ds ctxt)
467data NativeTy = IT8 | IT16 | IT32 | IT64
468 deriving (Show, Eq, Ord, Enum)
470instance Pretty NativeTy OutputAnnotation where
471 pretty IT8 = text "Bits8"
472 pretty IT16 = text "Bits16"
473 pretty IT32 = text "Bits32"
474 pretty IT64 = text "Bits64"
476data IntTy = ITFixed NativeTy | ITNative | ITBig | ITChar
477 | ITVec NativeTy Int
478 deriving (Show, Eq, Ord)
480intTyName :: IntTy -> String
481intTyName ITNative = "Int"
482intTyName ITBig = "BigInt"
483intTyName (ITFixed sized) = "B" ++ show (nativeTyWidth sized)
484intTyName (ITChar) = "Char"
485intTyName (ITVec ity count) = "B" ++ show (nativeTyWidth ity) ++ "x" ++ show count
487data ArithTy = ATInt IntTy | ATFloat -- TODO: Float vectors
488 deriving (Show, Eq, Ord)
489{-!
490deriving instance NFData IntTy
491deriving instance NFData NativeTy
492deriving instance NFData ArithTy
493!-}
495instance Pretty ArithTy OutputAnnotation where
496 pretty (ATInt ITNative) = text "Int"
497 pretty (ATInt ITBig) = text "BigInt"
498 pretty (ATInt ITChar) = text "Char"
499 pretty (ATInt (ITFixed n)) = pretty n
500 pretty (ATInt (ITVec e c)) = pretty e <> text "x" <> (text . show $ c)
501 pretty ATFloat = text "Float"
503nativeTyWidth :: NativeTy -> Int
504nativeTyWidth IT8 = 8
505nativeTyWidth IT16 = 16
506nativeTyWidth IT32 = 32
507nativeTyWidth IT64 = 64
509{-# DEPRECATED intTyWidth "Non-total function, use nativeTyWidth and appropriate casing" #-}
510intTyWidth :: IntTy -> Int
511intTyWidth (ITFixed n) = nativeTyWidth n
512intTyWidth ITNative = 8 * sizeOf (0 :: Int)
513intTyWidth ITChar = error "IRTS.Lang.intTyWidth: Characters have platform and backend dependent width"
514intTyWidth ITBig = error "IRTS.Lang.intTyWidth: Big integers have variable width"
516data Const = I Int | BI Integer | Fl Double | Ch Char | Str String
517 | B8 Word8 | B16 Word16 | B32 Word32 | B64 Word64
518 | B8V (Vector Word8) | B16V (Vector Word16)
519 | B32V (Vector Word32) | B64V (Vector Word64)
520 | AType ArithTy | StrType
521 | PtrType | ManagedPtrType | BufferType | VoidType | Forgot
522 deriving (Eq, Ord)
523{-!
524deriving instance Binary Const
525deriving instance NFData Const
526!-}
528instance Sized Const where
529 size _ = 1
531instance Pretty Const OutputAnnotation where
532 pretty (I i) = text . show $ i
533 pretty (BI i) = text . show $ i
534 pretty (Fl f) = text . show $ f
535 pretty (Ch c) = text . show $ c
536 pretty (Str s) = text s
537 pretty (AType a) = pretty a
538 pretty StrType = text "String"
539 pretty BufferType = text "prim__UnsafeBuffer"
540 pretty PtrType = text "Ptr"
541 pretty ManagedPtrType = text "Ptr"
542 pretty VoidType = text "Void"
543 pretty Forgot = text "Forgot"
544 pretty (B8 w) = text . show $ w
545 pretty (B16 w) = text . show $ w
546 pretty (B32 w) = text . show $ w
547 pretty (B64 w) = text . show $ w
549-- | Determines whether the input constant represents a type
550constIsType :: Const -> Bool
551constIsType (I _) = False
552constIsType (BI _) = False
553constIsType (Fl _) = False
554constIsType (Ch _) = False
555constIsType (Str _) = False
556constIsType (B8 _) = False
557constIsType (B16 _) = False
558constIsType (B32 _) = False
559constIsType (B64 _) = False
560constIsType (B8V _) = False
561constIsType (B16V _) = False
562constIsType (B32V _) = False
563constIsType (B64V _) = False
564constIsType _ = True
566-- | Get the docstring for a Const
567constDocs :: Const -> String
568constDocs c@(AType (ATInt ITBig)) = "Arbitrary-precision integers"
569constDocs c@(AType (ATInt ITNative)) = "Fixed-precision integers of undefined size"
570constDocs c@(AType (ATInt ITChar)) = "Characters in some unspecified encoding"
571constDocs c@(AType ATFloat) = "Double-precision floating-point numbers"
572constDocs StrType = "Strings in some unspecified encoding"
573constDocs PtrType = "Foreign pointers"
574constDocs ManagedPtrType = "Managed pointers"
575constDocs BufferType = "Copy-on-write buffers"
576constDocs c@(AType (ATInt (ITFixed IT8))) = "Eight bits (unsigned)"
577constDocs c@(AType (ATInt (ITFixed IT16))) = "Sixteen bits (unsigned)"
578constDocs c@(AType (ATInt (ITFixed IT32))) = "Thirty-two bits (unsigned)"
579constDocs c@(AType (ATInt (ITFixed IT64))) = "Sixty-four bits (unsigned)"
580constDocs c@(AType (ATInt (ITVec IT8 16))) = "Vectors of sixteen eight-bit values"
581constDocs c@(AType (ATInt (ITVec IT16 8))) = "Vectors of eight sixteen-bit values"
582constDocs c@(AType (ATInt (ITVec IT32 4))) = "Vectors of four thirty-two-bit values"
583constDocs c@(AType (ATInt (ITVec IT64 2))) = "Vectors of two sixty-four-bit values"
584constDocs (Fl f) = "A float"
585constDocs (I i) = "A fixed-precision integer"
586constDocs (BI i) = "An arbitrary-precision integer"
587constDocs (Str s) = "A string of length " ++ show (length s)
588constDocs (Ch c) = "A character"
589constDocs (B8 w) = "The eight-bit value 0x" ++
590 showIntAtBase 16 intToDigit w ""
591constDocs (B16 w) = "The sixteen-bit value 0x" ++
592 showIntAtBase 16 intToDigit w ""
593constDocs (B32 w) = "The thirty-two-bit value 0x" ++
594 showIntAtBase 16 intToDigit w ""
595constDocs (B64 w) = "The sixty-four-bit value 0x" ++
596 showIntAtBase 16 intToDigit w ""
597constDocs (B8V v) = "A vector of eight-bit values"
598constDocs (B16V v) = "A vector of sixteen-bit values"
599constDocs (B32V v) = "A vector of thirty-two-bit values"
600constDocs (B64V v) = "A vector of sixty-four-bit values"
601constDocs prim = "Undocumented"
603data Universe = NullType | UniqueType | AllTypes
604 deriving (Eq, Ord)
606instance Show Universe where
607 show UniqueType = "UniqueType"
608 show NullType = "NullType"
609 show AllTypes = "Type*"
611data Raw = Var Name
612 | RBind Name (Binder Raw) Raw
613 | RApp Raw Raw
614 | RType
615 | RUType Universe
616 | RForce Raw
617 | RConstant Const
618 deriving (Show, Eq)
620instance Sized Raw where
621 size (Var name) = 1
622 size (RBind name bind right) = 1 + size bind + size right
623 size (RApp left right) = 1 + size left + size right
624 size RType = 1
625 size (RUType _) = 1
626 size (RForce raw) = 1 + size raw
627 size (RConstant const) = size const
629instance Pretty Raw OutputAnnotation where
630 pretty = text . show
632{-!
633deriving instance Binary Raw
634deriving instance NFData Raw
635!-}
637-- The type parameter `b` will normally be something like `TT Name` or just
638-- `Raw`. We do not make a type-level distinction between TT terms that happen
639-- to be TT types and TT terms that are not TT types.
640-- | All binding forms are represented in a uniform fashion. This type only represents
641-- the types of bindings (and their values, if any); the attached identifiers are part
642-- of the 'Bind' constructor for the 'TT' type.
643data Binder b = Lam { binderTy :: !b {-^ type annotation for bound variable-}}
644 | Pi { binderTy :: !b,
645 binderKind :: !b }
646 {-^ A binding that occurs in a function type expression, e.g. @(x:Int) -> ...@ -}
647 | Let { binderTy :: !b,
648 binderVal :: b {-^ value for bound variable-}}
649 -- ^ A binding that occurs in a @let@ expression
650 | NLet { binderTy :: !b,
651 binderVal :: b }
652 | Hole { binderTy :: !b}
653 | GHole { envlen :: Int,
654 binderTy :: !b}
655 | Guess { binderTy :: !b,
656 binderVal :: b }
657 | PVar { binderTy :: !b }
658 -- ^ A pattern variable
659 | PVTy { binderTy :: !b }
660 deriving (Show, Eq, Ord, Functor, Foldable, Traversable)
661{-!
662deriving instance Binary Binder
663deriving instance NFData Binder
664!-}
666instance Sized a => Sized (Binder a) where
667 size (Lam ty) = 1 + size ty
668 size (Pi ty _) = 1 + size ty
669 size (Let ty val) = 1 + size ty + size val
670 size (NLet ty val) = 1 + size ty + size val
671 size (Hole ty) = 1 + size ty
672 size (GHole _ ty) = 1 + size ty
673 size (Guess ty val) = 1 + size ty + size val
674 size (PVar ty) = 1 + size ty
675 size (PVTy ty) = 1 + size ty
677fmapMB :: Monad m => (a -> m b) -> Binder a -> m (Binder b)
678fmapMB f (Let t v) = liftM2 Let (f t) (f v)
679fmapMB f (NLet t v) = liftM2 NLet (f t) (f v)
680fmapMB f (Guess t v) = liftM2 Guess (f t) (f v)
681fmapMB f (Lam t) = liftM Lam (f t)
682fmapMB f (Pi t k) = liftM2 Pi (f t) (f k)
683fmapMB f (Hole t) = liftM Hole (f t)
684fmapMB f (GHole i t) = liftM (GHole i) (f t)
685fmapMB f (PVar t) = liftM PVar (f t)
686fmapMB f (PVTy t) = liftM PVTy (f t)
688raw_apply :: Raw -> [Raw] -> Raw
689raw_apply f [] = f
690raw_apply f (a : as) = raw_apply (RApp f a) as
692raw_unapply :: Raw -> (Raw, [Raw])
693raw_unapply t = ua [] t where
694 ua args (RApp f a) = ua (a:args) f
695 ua args t = (t, args)
697-- WELL TYPED TERMS ---------------------------------------------------------
699-- | Universe expressions for universe checking
700data UExp = UVar Int -- ^ universe variable
701 | UVal Int -- ^ explicit universe level
702 deriving (Eq, Ord)
703{-!
704deriving instance NFData UExp
705!-}
707instance Sized UExp where
708 size _ = 1
710-- We assume that universe levels have been checked, so anything external
711-- can just have the same universe variable and we won't get any new
712-- cycles.
714instance Binary UExp where
715 put x = return ()
716 get = return (UVar (-1))
718instance Show UExp where
719 show (UVar x) | x < 26 = [toEnum (x + fromEnum 'a')]
720 | otherwise = toEnum ((x `mod` 26) + fromEnum 'a') : show (x `div` 26)
721 show (UVal x) = show x
722-- show (UMax l r) = "max(" ++ show l ++ ", " ++ show r ++")"
724-- | Universe constraints
725data UConstraint = ULT UExp UExp -- ^ Strictly less than
726 | ULE UExp UExp -- ^ Less than or equal to
727 deriving Eq
729instance Show UConstraint where
730 show (ULT x y) = show x ++ " < " ++ show y
731 show (ULE x y) = show x ++ " <= " ++ show y
733type UCs = (Int, [UConstraint])
735data NameType = Bound
736 | Ref
737 | DCon {nt_tag :: Int, nt_arity :: Int, nt_unique :: Bool} -- ^ Data constructor
738 | TCon {nt_tag :: Int, nt_arity :: Int} -- ^ Type constructor
739 deriving (Show, Ord)
740{-!
741deriving instance Binary NameType
742deriving instance NFData NameType
743!-}
745instance Sized NameType where
746 size _ = 1
748instance Pretty NameType OutputAnnotation where
749 pretty = text . show
751instance Eq NameType where
752 Bound == Bound = True
753 Ref == Ref = True
754 DCon _ a _ == DCon _ b _ = (a == b) -- ignore tag
755 TCon _ a == TCon _ b = (a == b) -- ignore tag
756 _ == _ = False
758-- | Terms in the core language. The type parameter is the type of
759-- identifiers used for bindings and explicit named references;
760-- usually we use @TT 'Name'@.
761data TT n = P NameType n (TT n) -- ^ named references with type
762 -- (P for "Parameter", motivated by McKinna and Pollack's
763 -- Pure Type Systems Formalized)
764 | V !Int -- ^ a resolved de Bruijn-indexed variable
765 | Bind n !(Binder (TT n)) (TT n) -- ^ a binding
766 | App !(TT n) (TT n) -- ^ function, function type, arg
767 | Constant Const -- ^ constant
768 | Proj (TT n) !Int -- ^ argument projection; runtime only
769 -- (-1) is a special case for 'subtract one from BI'
770 | Erased -- ^ an erased term
771 | Impossible -- ^ special case for totality checking
772 | TType UExp -- ^ the type of types at some level
773 | UType Universe -- ^ Uniqueness type universe (disjoint from TType)
774 deriving (Ord, Functor)
775{-!
776deriving instance Binary TT
777deriving instance NFData TT
778!-}
780class TermSize a where
781 termsize :: Name -> a -> Int
783instance TermSize a => TermSize [a] where
784 termsize n [] = 0
785 termsize n (x : xs) = termsize n x + termsize n xs
787instance TermSize (TT Name) where
788 termsize n (P _ n' _)
789 | n' == n = 1000000 -- recursive => really big
790 | otherwise = 1
791 termsize n (V _) = 1
792 -- for `Bind` terms, we can erroneously declare a term
793 -- "recursive => really big" if the name of the bound
794 -- variable is the same as the name we're using
795 -- So generate a different name in that case.
796 termsize n (Bind n' (Let t v) sc)
797 = let rn = if n == n' then sMN 0 "noname" else n in
798 termsize rn v + termsize rn sc
799 termsize n (Bind n' b sc)
800 = let rn = if n == n' then sMN 0 "noname" else n in
801 termsize rn sc
802 termsize n (App f a) = termsize n f + termsize n a
803 termsize n (Proj t i) = termsize n t
804 termsize n _ = 1
806instance Sized a => Sized (TT a) where
807 size (P name n trm) = 1 + size name + size n + size trm
808 size (V v) = 1
809 size (Bind nm binder bdy) = 1 + size nm + size binder + size bdy
810 size (App l r) = 1 + size l + size r
811 size (Constant c) = size c
812 size Erased = 1
813 size (TType u) = 1 + size u
815instance Pretty a o => Pretty (TT a) o where
816 pretty _ = text "test"
818type EnvTT n = [(n, Binder (TT n))]
820data Datatype n = Data { d_typename :: n,
821 d_typetag :: Int,
822 d_type :: (TT n),
823 d_unique :: Bool,
824 d_cons :: [(n, TT n)] }
825 deriving (Show, Functor, Eq)
827instance Eq n => Eq (TT n) where
828 (==) (P xt x _) (P yt y _) = x == y
829 (==) (V x) (V y) = x == y
830 (==) (Bind _ xb xs) (Bind _ yb ys) = xs == ys && xb == yb
831 (==) (App fx ax) (App fy ay) = ax == ay && fx == fy
832 (==) (TType _) (TType _) = True -- deal with constraints later
833 (==) (Constant x) (Constant y) = x == y
834 (==) (Proj x i) (Proj y j) = x == y && i == j
835 (==) Erased _ = True
836 (==) _ Erased = True
837 (==) _ _ = False
839-- * A few handy operations on well typed terms:
841-- | A term is injective iff it is a data constructor, type constructor,
842-- constant, the type Type, pi-binding, or an application of an injective
843-- term.
844isInjective :: TT n -> Bool
845isInjective (P (DCon _ _ _) _ _) = True
846isInjective (P (TCon _ _) _ _) = True
847isInjective (Constant _) = True
848isInjective (TType x) = True
849isInjective (Bind _ (Pi _ _) sc) = True
850isInjective (App f a) = isInjective f
851isInjective _ = False
853-- | Count the number of instances of a de Bruijn index in a term
854vinstances :: Int -> TT n -> Int
855vinstances i (V x) | i == x = 1
856vinstances i (App f a) = vinstances i f + vinstances i a
857vinstances i (Bind x b sc) = instancesB b + vinstances (i + 1) sc
858 where instancesB (Let t v) = vinstances i v
859 instancesB _ = 0
860vinstances i t = 0
862-- | Replace the outermost (index 0) de Bruijn variable with the given term
863instantiate :: TT n -> TT n -> TT n
864instantiate e = subst 0 where
865 subst i (V x) | i == x = e
866 subst i (Bind x b sc) = Bind x (fmap (subst i) b) (subst (i+1) sc)
867 subst i (App f a) = App (subst i f) (subst i a)
868 subst i (Proj x idx) = Proj (subst i x) idx
869 subst i t = t
871-- | As 'instantiate', but also decrement the indices of all de Bruijn variables
872-- remaining in the term, so that there are no more references to the variable
873-- that has been substituted.
874substV :: TT n -> TT n -> TT n
875substV x tm = dropV 0 (instantiate x tm) where
876 dropV i (V x) | x > i = V (x - 1)
877 | otherwise = V x
878 dropV i (Bind x b sc) = Bind x (fmap (dropV i) b) (dropV (i+1) sc)
879 dropV i (App f a) = App (dropV i f) (dropV i a)
880 dropV i (Proj x idx) = Proj (dropV i x) idx
881 dropV i t = t
883-- | Replace all non-free de Bruijn references in the given term with references
884-- to the name of their binding.
885explicitNames :: TT n -> TT n
886explicitNames (Bind x b sc) = let b' = fmap explicitNames b in
887 Bind x b'
888 (explicitNames (instantiate
889 (P Bound x (binderTy b')) sc))
890explicitNames (App f a) = App (explicitNames f) (explicitNames a)
891explicitNames (Proj x idx) = Proj (explicitNames x) idx
892explicitNames t = t
894-- | Replace references to the given 'Name'-like id with references to
895-- de Bruijn index 0.
896pToV :: Eq n => n -> TT n -> TT n
897pToV n = pToV' n 0
898pToV' n i (P _ x _) | n == x = V i
899pToV' n i (Bind x b sc)
900-- We can assume the inner scope has been pToVed already, so continue to
901-- resolve names from the *outer* scope which may happen to have the same id.
902 | n == x = Bind x (fmap (pToV' n i) b) sc
903 | otherwise = Bind x (fmap (pToV' n i) b) (pToV' n (i+1) sc)
904pToV' n i (App f a) = App (pToV' n i f) (pToV' n i a)
905pToV' n i (Proj t idx) = Proj (pToV' n i t) idx
906pToV' n i t = t
908-- increase de Bruijn indices, as if a binder has been added
909addBinder :: TT n -> TT n
910addBinder t = ab 0 t
911 where
912 ab top (V i) | i >= top = V (i + 1)
913 | otherwise = V i
914 ab top (Bind x b sc) = Bind x (fmap (ab top) b) (ab (top + 1) sc)
915 ab top (App f a) = App (ab top f) (ab top a)
916 ab top (Proj t idx) = Proj (ab top t) idx
917 ab top t = t
919-- | Convert several names. First in the list comes out as V 0
920pToVs :: Eq n => [n] -> TT n -> TT n
921pToVs ns tm = pToVs' ns tm 0 where
922 pToVs' [] tm i = tm
923 pToVs' (n:ns) tm i = pToV' n i (pToVs' ns tm (i+1))
925-- | Replace de Bruijn indices in the given term with explicit references to
926-- the names of the bindings they refer to. It is an error if the given term
927-- contains free de Bruijn indices.
928vToP :: TT n -> TT n
929vToP = vToP' [] where
930 vToP' env (V i) = let (n, b) = (env !! i) in
931 P Bound n (binderTy b)
932 vToP' env (Bind n b sc) = let b' = fmap (vToP' env) b in
933 Bind n b' (vToP' ((n, b'):env) sc)
934 vToP' env (App f a) = App (vToP' env f) (vToP' env a)
935 vToP' env t = t
937-- | Replace every non-free reference to the name of a binding in
938-- the given term with a de Bruijn index.
939finalise :: Eq n => TT n -> TT n
940finalise (Bind x b sc) = Bind x (fmap finalise b) (pToV x (finalise sc))
941finalise (App f a) = App (finalise f) (finalise a)
942finalise t = t
944-- Once we've finished checking everything about a term we no longer need
945-- the type on the 'P' so erase it so save memory
947pEraseType :: TT n -> TT n
948pEraseType (P nt t _) = P nt t Erased
949pEraseType (App f a) = App (pEraseType f) (pEraseType a)
950pEraseType (Bind n b sc) = Bind n (fmap pEraseType b) (pEraseType sc)
951pEraseType t = t
953-- | As 'instantiate', but in addition to replacing @'V' 0@,
954-- replace references to the given 'Name'-like id.
955subst :: Eq n => n {-^ The id to replace -} ->
956 TT n {-^ The replacement term -} ->
957 TT n {-^ The term to replace in -} ->
958 TT n
959-- subst n v tm = instantiate v (pToV n tm)
960subst n v tm = fst $ subst' 0 tm
961 where
962 -- keep track of updates to save allocations - this is a big win on
963 -- large terms in particular
964 -- ('Maybe' would be neater here, but >>= is not the right combinator.
965 -- Feel free to tidy up, as long as it still saves allocating when no
966 -- substitution happens...)
967 subst' i (V x) | i == x = (v, True)
968 subst' i (P _ x _) | n == x = (v, True)
969 subst' i t@(Bind x b sc) | x /= n
970 = let (b', ub) = substB' i b
971 (sc', usc) = subst' (i+1) sc in
972 if ub || usc then (Bind x b' sc', True) else (t, False)
973 subst' i t@(App f a) = let (f', uf) = subst' i f
974 (a', ua) = subst' i a in
975 if uf || ua then (App f' a', True) else (t, False)
976 subst' i t@(Proj x idx) = let (x', u) = subst' i x in
977 if u then (Proj x' idx, u) else (t, False)
978 subst' i t = (t, False)
980 substB' i b@(Let t v) = let (t', ut) = subst' i t
981 (v', uv) = subst' i v in
982 if ut || uv then (Let t' v', True)
983 else (b, False)
984 substB' i b@(Guess t v) = let (t', ut) = subst' i t
985 (v', uv) = subst' i v in
986 if ut || uv then (Guess t' v', True)
987 else (b, False)
988 substB' i b = let (ty', u) = subst' i (binderTy b) in
989 if u then (b { binderTy = ty' }, u) else (b, False)
991-- If there are no Vs in the term (i.e. in proof state)
992psubst :: Eq n => n -> TT n -> TT n -> TT n
993psubst n v tm = s' 0 tm where
994 s' i (V x) | x > i = V (x - 1)
995 | x == i = v
996 | otherwise = V x
997 s' i (P _ x _) | n == x = v
998 s' i (Bind x b sc) | n == x = Bind x (fmap (s' i) b) sc
999 | otherwise = Bind x (fmap (s' i) b) (s' (i+1) sc)
1000 s' i (App f a) = App (s' i f) (s' i a)
1001 s' i (Proj t idx) = Proj (s' i t) idx
1002 s' i t = t
1004-- | As 'subst', but takes a list of (name, substitution) pairs instead
1005-- of a single name and substitution
1006substNames :: Eq n => [(n, TT n)] -> TT n -> TT n
1007substNames [] t = t
1008substNames ((n, tm) : xs) t = subst n tm (substNames xs t)
1010-- | Replaces all terms equal (in the sense of @(==)@) to
1011-- the old term with the new term.
1012substTerm :: Eq n => TT n {-^ Old term -} ->
1013 TT n {-^ New term -} ->
1014 TT n {-^ template term -}
1015 -> TT n
1016substTerm old new = st where
1017 st t | t == old = new
1018 st (App f a) = App (st f) (st a)
1019 st (Bind x b sc) = Bind x (fmap st b) (st sc)
1020 st t = t
1022-- | Return number of occurrences of V 0 or bound name i the term
1023occurrences :: Eq n => n -> TT n -> Int
1024occurrences n t = execState (no' 0 t) 0
1025 where
1026 no' i (V x) | i == x = do num <- get; put (num + 1)
1027 no' i (P Bound x _) | n == x = do num <- get; put (num + 1)
1028 no' i (Bind n b sc) = do noB' i b; no' (i+1) sc
1029 where noB' i (Let t v) = do no' i t; no' i v
1030 noB' i (Guess t v) = do no' i t; no' i v
1031 noB' i b = no' i (binderTy b)
1032 no' i (App f a) = do no' i f; no' i a
1033 no' i (Proj x _) = no' i x
1034 no' i _ = return ()
1036-- | Returns true if V 0 and bound name n do not occur in the term
1037noOccurrence :: Eq n => n -> TT n -> Bool
1038noOccurrence n t = no' 0 t
1039 where
1040 no' i (V x) = not (i == x)
1041 no' i (P Bound x _) = not (n == x)
1042 no' i (Bind n b sc) = noB' i b && no' (i+1) sc
1043 where noB' i (Let t v) = no' i t && no' i v
1044 noB' i (Guess t v) = no' i t && no' i v
1045 noB' i b = no' i (binderTy b)
1046 no' i (App f a) = no' i f && no' i a
1047 no' i (Proj x _) = no' i x
1048 no' i _ = True
1050-- | Returns all names used free in the term
1051freeNames :: Eq n => TT n -> [n]
1052freeNames (P _ n _) = [n]
1053freeNames (Bind n (Let t v) sc) = nub $ freeNames v ++ (freeNames sc \\ [n])
1054 ++ freeNames t
1055freeNames (Bind n b sc) = nub $ freeNames (binderTy b) ++ (freeNames sc \\ [n])
1056freeNames (App f a) = nub $ freeNames f ++ freeNames a
1057freeNames (Proj x i) = nub $ freeNames x
1058freeNames _ = []
1060-- | Return the arity of a (normalised) type
1061arity :: TT n -> Int
1062arity (Bind n (Pi t _) sc) = 1 + arity sc
1063arity _ = 0
1065-- | Deconstruct an application; returns the function and a list of arguments
1066unApply :: TT n -> (TT n, [TT n])
1067unApply t = ua [] t where
1068 ua args (App f a) = ua (a:args) f
1069 ua args t = (t, args)
1071-- | Returns a term representing the application of the first argument
1072-- (a function) to every element of the second argument.
1073mkApp :: TT n -> [TT n] -> TT n
1074mkApp f [] = f
1075mkApp f (a:as) = mkApp (App f a) as
1077unList :: Term -> Maybe [Term]
1078unList tm = case unApply tm of
1079 (nil, [_]) -> Just []
1080 (cons, ([_, x, xs])) ->
1081 do rest <- unList xs
1082 return $ x:rest
1083 (f, args) -> Nothing
1085-- | Cast a 'TT' term to a 'Raw' value, discarding universe information and
1086-- the types of named references and replacing all de Bruijn indices
1087-- with the corresponding name. It is an error if there are free de
1088-- Bruijn indices.
1089forget :: TT Name -> Raw
1090forget tm = forgetEnv [] tm
1092forgetEnv :: [Name] -> TT Name -> Raw
1093forgetEnv env (P _ n _) = Var n
1094forgetEnv env (V i) = Var (env !! i)
1095forgetEnv env (Bind n b sc) = let n' = uniqueName n env in
1096 RBind n' (fmap (forgetEnv env) b)
1097 (forgetEnv (n':env) sc)
1098forgetEnv env (App f a) = RApp (forgetEnv env f) (forgetEnv env a)
1099forgetEnv env (Constant c) = RConstant c
1100forgetEnv env (TType i) = RType
1101forgetEnv env (UType u) = RUType u
1102forgetEnv env Erased = RConstant Forgot
1104-- | Introduce a 'Bind' into the given term for each element of the
1105-- given list of (name, binder) pairs.
1106bindAll :: [(n, Binder (TT n))] -> TT n -> TT n
1107bindAll [] t = t
1108bindAll ((n, b) : bs) t = Bind n b (bindAll bs t)
1110-- | Like 'bindAll', but the 'Binder's are 'TT' terms instead.
1111-- The first argument is a function to map @TT@ terms to @Binder@s.
1112-- This function might often be something like 'Lam', which directly
1113-- constructs a @Binder@ from a @TT@ term.
1114bindTyArgs :: (TT n -> Binder (TT n)) -> [(n, TT n)] -> TT n -> TT n
1115bindTyArgs b xs = bindAll (map (\ (n, ty) -> (n, b ty)) xs)
1117-- | Return a list of pairs of the names of the outermost 'Pi'-bound
1118-- variables in the given term, together with their types.
1119getArgTys :: TT n -> [(n, TT n)]
1120getArgTys (Bind n (Pi t _) sc) = (n, t) : getArgTys sc
1121getArgTys _ = []
1123getRetTy :: TT n -> TT n
1124getRetTy (Bind n (PVar _) sc) = getRetTy sc
1125getRetTy (Bind n (PVTy _) sc) = getRetTy sc
1126getRetTy (Bind n (Pi _ _) sc) = getRetTy sc
1127getRetTy sc = sc
1129uniqueNameFrom :: [Name] -> [Name] -> Name
1130uniqueNameFrom (s : supply) hs
1131 | s `elem` hs = uniqueNameFrom supply hs
1132 | otherwise = s
1134uniqueName :: Name -> [Name] -> Name
1135uniqueName n hs | n `elem` hs = uniqueName (nextName n) hs
1136 | otherwise = n
1138uniqueBinders :: [Name] -> TT Name -> TT Name
1139uniqueBinders ns (Bind n b sc)
1140 = let n' = uniqueName n ns
1141 ns' = n' : ns in
1142 Bind n' (fmap (uniqueBinders ns') b) (uniqueBinders ns' sc)
1143uniqueBinders ns (App f a) = App (uniqueBinders ns f) (uniqueBinders ns a)
1144uniqueBinders ns t = t
1147nextName (NS x s) = NS (nextName x) s
1148nextName (MN i n) = MN (i+1) n
1149nextName (UN x) = let (num', nm') = T.span isDigit (T.reverse x)
1150 nm = T.reverse nm'
1151 num = readN (T.reverse num') in
1152 UN (nm `T.append` txt (show (num+1)))
1153 where
1154 readN x | not (T.null x) = read (T.unpack x)
1155 readN x = 0
1156nextName (SN x) = SN (nextName' x)
1157 where
1158 nextName' (WhereN i f x) = WhereN i f (nextName x)
1159 nextName' (WithN i n) = WithN i (nextName n)
1160 nextName' (CaseN n) = CaseN (nextName n)
1161 nextName' (MethodN n) = MethodN (nextName n)
1163type Term = TT Name
1164type Type = Term
1166type Env = EnvTT Name
1168-- | an environment with de Bruijn indices 'normalised' so that they all refer to
1169-- this environment
1171newtype WkEnvTT n = Wk (EnvTT n)
1172type WkEnv = WkEnvTT Name
1174instance (Eq n, Show n) => Show (TT n) where
1175 show t = showEnv [] t
1177itBitsName IT8 = "Bits8"
1178itBitsName IT16 = "Bits16"
1179itBitsName IT32 = "Bits32"
1180itBitsName IT64 = "Bits64"
1182instance Show Const where
1183 show (I i) = show i
1184 show (BI i) = show i
1185 show (Fl f) = show f
1186 show (Ch c) = show c
1187 show (Str s) = show s
1188 show (B8 x) = show x
1189 show (B16 x) = show x
1190 show (B32 x) = show x
1191 show (B64 x) = show x
1192 show (B8V x) = "<" ++ intercalate "," (map show (V.toList x)) ++ ">"
1193 show (B16V x) = "<" ++ intercalate "," (map show (V.toList x)) ++ ">"
1194 show (B32V x) = "<" ++ intercalate "," (map show (V.toList x)) ++ ">"
1195 show (B64V x) = "<" ++ intercalate "," (map show (V.toList x)) ++ ">"
1196 show (AType ATFloat) = "Float"
1197 show (AType (ATInt ITBig)) = "Integer"
1198 show (AType (ATInt ITNative)) = "Int"
1199 show (AType (ATInt ITChar)) = "Char"
1200 show (AType (ATInt (ITFixed it))) = itBitsName it
1201 show (AType (ATInt (ITVec it c))) = itBitsName it ++ "x" ++ show c
1202 show StrType = "String"
1203 show BufferType = "prim__UnsafeBuffer"
1204 show PtrType = "Ptr"
1205 show ManagedPtrType = "ManagedPtr"
1206 show VoidType = "Void"
1208showEnv :: (Eq n, Show n) => EnvTT n -> TT n -> String
1209showEnv env t = showEnv' env t False
1210showEnvDbg env t = showEnv' env t True
1212prettyEnv env t = prettyEnv' env t False
1213 where
1214 prettyEnv' env t dbg = prettySe 10 env t dbg
1216 bracket outer inner p
1217 | inner > outer = lparen <> p <> rparen
1218 | otherwise = p
1220 prettySe p env (P nt n t) debug =
1221 pretty n <+>
1222 if debug then
1223 lbracket <+> pretty nt <+> colon <+> prettySe 10 env t debug <+> rbracket
1224 else
1225 empty
1226 prettySe p env (V i) debug
1227 | i < length env =
1228 if debug then
1229 text . show . fst $ env!!i
1230 else
1231 lbracket <+> text (show i) <+> rbracket
1232 | otherwise = text "unbound" <+> text (show i) <+> text "!"
1233 prettySe p env (Bind n b@(Pi t _) sc) debug
1234 | noOccurrence n sc && not debug =
1235 bracket p 2 $ prettySb env n b debug <> prettySe 10 ((n, b):env) sc debug
1236 prettySe p env (Bind n b sc) debug =
1237 bracket p 2 $ prettySb env n b debug <> prettySe 10 ((n, b):env) sc debug
1238 prettySe p env (App f a) debug =
1239 bracket p 1 $ prettySe 1 env f debug <+> prettySe 0 env a debug
1240 prettySe p env (Proj x i) debug =
1241 prettySe 1 env x debug <+> text ("!" ++ show i)
1242 prettySe p env (Constant c) debug = pretty c
1243 prettySe p env Erased debug = text "[_]"
1244 prettySe p env (TType i) debug = text "Type" <+> (text . show $ i)
1246 -- Render a `Binder` and its name
1247 prettySb env n (Lam t) = prettyB env "λ" "=>" n t
1248 prettySb env n (Hole t) = prettyB env "?defer" "." n t
1249 prettySb env n (Pi t _) = prettyB env "(" ") ->" n t
1250 prettySb env n (PVar t) = prettyB env "pat" "." n t
1251 prettySb env n (PVTy t) = prettyB env "pty" "." n t
1252 prettySb env n (Let t v) = prettyBv env "let" "in" n t v
1253 prettySb env n (Guess t v) = prettyBv env "??" "in" n t v
1255 -- Use `op` and `sc` to delimit `n` (a binding name) and its type
1256 -- declaration
1257 -- e.g. "λx : Int =>" for the Lam case
1258 prettyB env op sc n t debug =
1259 text op <> pretty n <+> colon <+> prettySe 10 env t debug <> text sc
1261 -- Like `prettyB`, but handle the bindings that have values in addition
1262 -- to names and types
1263 prettyBv env op sc n t v debug =
1264 text op <> pretty n <+> colon <+> prettySe 10 env t debug <+> text "=" <+>
1265 prettySe 10 env v debug <> text sc
1268showEnv' env t dbg = se 10 env t where
1269 se p env (P nt n t) = show n
1270 ++ if dbg then "{" ++ show nt ++ " : " ++ se 10 env t ++ "}" else ""
1271 se p env (V i) | i < length env && i >= 0
1272 = (show $ fst $ env!!i) ++
1273 if dbg then "{" ++ show i ++ "}" else ""
1274 | otherwise = "!!V " ++ show i ++ "!!"
1275 se p env (Bind n b@(Pi t k) sc)
1276 | noOccurrence n sc && not dbg = bracket p 2 $ se 1 env t ++ arrow k ++ se 10 ((n,b):env) sc
1277 where arrow (TType _) = " -> "
1278 arrow u = " [" ++ show u ++ "] -> "
1279 se p env (Bind n b sc) = bracket p 2 $ sb env n b ++ se 10 ((n,b):env) sc
1280 se p env (App f a) = bracket p 1 $ se 1 env f ++ " " ++ se 0 env a
1281 se p env (Proj x i) = se 1 env x ++ "!" ++ show i
1282 se p env (Constant c) = show c
1283 se p env Erased = "[__]"
1284 se p env Impossible = "[impossible]"
1285 se p env (TType i) = "Type " ++ show i
1286 se p env (UType u) = show u
1288 sb env n (Lam t) = showb env "\\ " " => " n t
1289 sb env n (Hole t) = showb env "? " ". " n t
1290 sb env n (GHole i t) = showb env "?defer " ". " n t
1291 sb env n (Pi t _) = showb env "(" ") -> " n t
1292 sb env n (PVar t) = showb env "pat " ". " n t
1293 sb env n (PVTy t) = showb env "pty " ". " n t
1294 sb env n (Let t v) = showbv env "let " " in " n t v
1295 sb env n (Guess t v) = showbv env "?? " " in " n t v
1297 showb env op sc n t = op ++ show n ++ " : " ++ se 10 env t ++ sc
1298 showbv env op sc n t v = op ++ show n ++ " : " ++ se 10 env t ++ " = " ++
1299 se 10 env v ++ sc
1301 bracket outer inner str | inner > outer = "(" ++ str ++ ")"
1302 | otherwise = str
1304-- | Check whether a term has any holes in it - impure if so
1305pureTerm :: TT Name -> Bool
1306pureTerm (App f a) = pureTerm f && pureTerm a
1307pureTerm (Bind n b sc) = notClassName n && pureBinder b && pureTerm sc where
1308 pureBinder (Hole _) = False
1309 pureBinder (Guess _ _) = False
1310 pureBinder (Let t v) = pureTerm t && pureTerm v
1311 pureBinder t = pureTerm (binderTy t)
1313 notClassName (MN _ c) | c == txt "class" = False
1314 notClassName _ = True
1316pureTerm _ = True
1318-- | Weaken a term by adding i to each de Bruijn index (i.e. lift it over i bindings)
1319weakenTm :: Int -> TT n -> TT n
1320weakenTm i t = wk i 0 t
1321 where wk i min (V x) | x >= min = V (i + x)
1322 wk i m (App f a) = App (wk i m f) (wk i m a)
1323 wk i m (Bind x b sc) = Bind x (wkb i m b) (wk i (m + 1) sc)
1324 wk i m t = t
1325 wkb i m t = fmap (wk i m) t
1327-- | Weaken an environment so that all the de Bruijn indices are correct according
1328-- to the latest bound variable
1330weakenEnv :: EnvTT n -> EnvTT n
1331weakenEnv env = wk (length env - 1) env
1332 where wk i [] = []
1333 wk i ((n, b) : bs) = (n, weakenTmB i b) : wk (i - 1) bs
1334 weakenTmB i (Let t v) = Let (weakenTm i t) (weakenTm i v)
1335 weakenTmB i (Guess t v) = Guess (weakenTm i t) (weakenTm i v)
1336 weakenTmB i t = t { binderTy = weakenTm i (binderTy t) }
1338-- | Weaken every term in the environment by the given amount
1339weakenTmEnv :: Int -> EnvTT n -> EnvTT n
1340weakenTmEnv i = map (\ (n, b) -> (n, fmap (weakenTm i) b))
1342-- | Gather up all the outer 'PVar's and 'Hole's in an expression and reintroduce
1343-- them in a canonical order
1344orderPats :: Term -> Term
1345orderPats tm = op [] tm
1346 where
1347 op [] (App f a) = App f (op [] a) -- for Infer terms
1349 op ps (Bind n (PVar t) sc) = op ((n, PVar t) : ps) sc
1350 op ps (Bind n (Hole t) sc) = op ((n, Hole t) : ps) sc
1351 op ps (Bind n (Pi t k) sc) = op ((n, Pi t k) : ps) sc
1352 op ps sc = bindAll (sortP ps) sc
1354 sortP ps = pick [] (reverse ps)
1356 namesIn (P _ n _) = [n]
1357 namesIn (Bind n b t) = nub $ nb b ++ (namesIn t \\ [n])
1358 where nb (Let t v) = nub (namesIn t) ++ nub (namesIn v)
1359 nb (Guess t v) = nub (namesIn t) ++ nub (namesIn v)
1360 nb t = namesIn (binderTy t)
1361 namesIn (App f a) = nub (namesIn f ++ namesIn a)
1362 namesIn _ = []
1364 pick acc [] = reverse acc
1365 pick acc ((n, t) : ps) = pick (insert n t acc) ps
1367 insert n t [] = [(n, t)]
1368 insert n t ((n',t') : ps)
1369 | n `elem` (namesIn (binderTy t') ++
1370 concatMap namesIn (map (binderTy . snd) ps))
1371 = (n', t') : insert n t ps
1372 | otherwise = (n,t):(n',t'):ps
1374-- Make sure all the pattern bindings are as far out as possible
1375liftPats :: Term -> Term
1376liftPats tm = let (tm', ps) = runState (getPats tm) [] in
1377 orderPats $ bindPats (reverse ps) tm'
1378 where
1379 bindPats [] tm = tm
1380 bindPats ((n, t):ps) tm
1381 | n `notElem` map fst ps = Bind n (PVar t) (bindPats ps tm)
1382 | otherwise = bindPats ps tm
1384 getPats :: Term -> State [(Name, Type)] Term
1385 getPats (Bind n (PVar t) sc) = do ps <- get
1386 put ((n, t) : ps)
1387 getPats sc
1388 getPats (Bind n (Guess t v) sc) = do t' <- getPats t
1389 v' <- getPats v
1390 sc' <- getPats sc
1391 return (Bind n (Guess t' v') sc')
1392 getPats (Bind n (Let t v) sc) = do t' <- getPats t
1393 v' <- getPats v
1394 sc' <- getPats sc
1395 return (Bind n (Let t' v') sc')
1396 getPats (Bind n (Pi t k) sc) = do t' <- getPats t
1397 k' <- getPats k
1398 sc' <- getPats sc
1399 return (Bind n (Pi t' k') sc')
1400 getPats (Bind n (Lam t) sc) = do t' <- getPats t
1401 sc' <- getPats sc
1402 return (Bind n (Lam t') sc')
1403 getPats (Bind n (Hole t) sc) = do t' <- getPats t
1404 sc' <- getPats sc
1405 return (Bind n (Hole t') sc')
1408 getPats (App f a) = do f' <- getPats f
1409 a' <- getPats a
1410 return (App f' a')
1411 getPats t = return t
1413allTTNames :: Eq n => TT n -> [n]
1414allTTNames = nub . allNamesIn
1415 where allNamesIn (P _ n _) = [n]
1416 allNamesIn (Bind n b t) = [n] ++ nb b ++ allNamesIn t
1417 where nb (Let t v) = allNamesIn t ++ allNamesIn v
1418 nb (Guess t v) = allNamesIn t ++ allNamesIn v
1419 nb t = allNamesIn (binderTy t)
1420 allNamesIn (App f a) = allNamesIn f ++ allNamesIn a
1421 allNamesIn _ = []