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