git.iko.soy/Idris-dev
on 1b71663 help sign in
Idris-dev/src/Idris/Core/TT.hs
1895 lines 75 kB history raw
1{-|
2Module : Idris.Core.TT
3Description : The core language of Idris, TT.
5License : BSD3
6Maintainer : The Idris Community.
8TT is the core language of Idris. The language has:
10 * Full dependent types
12 * A hierarchy of universes, with cumulativity: Type : Type1, Type1 : Type2, ...
14 * Pattern matching letrec binding
16 * (primitive types defined externally)
18 Some technical stuff:
20 * Typechecker is kept as simple as possible - no unification, just a checker for incomplete terms.
22 * We have a simple collection of tactics which we use to elaborate source
23 programs with implicit syntax into fully explicit terms.
24-}
25{-# LANGUAGE CPP, DeriveDataTypeable, DeriveFoldable, DeriveFunctor,
26 DeriveGeneric, DeriveTraversable, FlexibleContexts,
27 FlexibleInstances, FunctionalDependencies, MultiParamTypeClasses,
28 PatternGuards, TypeSynonymInstances #-}
29{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
30module Idris.Core.TT(
31 AppStatus(..), ArithTy(..), Binder(..), Const(..), Ctxt(..)
32 , ConstraintFC(..), DataOpt(..), DataOpts(..), Datatype(..)
33 , Env(..), EnvTT(..), Err(..), Err'(..), ErrorReportPart(..)
34 , FC(..), FC'(..), ImplicitInfo(..), IntTy(..), Name(..)
35 , NameOutput(..), NameType(..), NativeTy(..), OutputAnnotation(..)
36 , Provenance(..), Raw(..), RigCount(..), SpecialName(..), TC(..), Term(..)
37 , TermSize(..), TextFormatting(..), TT(..),Type(..), TypeInfo(..)
38 , UConstraint(..), UCs(..), UExp(..), Universe(..)
39 , addAlist, addBinder, addDef, allTTNames, arity, bindAll
40 , bindingOf, bindTyArgs, caseName, constDocs, constIsType, deleteDefExact
41 , discard, emptyContext, emptyFC, explicitNames, fc_end, fc_fname
42 , fc_start, fcIn, fileFC, finalise, fmapMB, forget, forgetEnv
43 , freeNames, getArgTys, getRetTy, substRetTy, implicitable, instantiate, internalNS
44 , intTyName, isInjective, isTypeConst, lookupCtxt
45 , lookupCtxtExact, lookupCtxtName, mapCtxt, mkApp, nativeTyWidth
46 , nextName, noOccurrence, nsroot, occurrences
47 , pEraseType, pmap, pprintRaw, pprintTT, pprintTTClause, prettyEnv, psubst
48 , pToV, pToVs, pureTerm, raw_apply, raw_unapply, refsIn, safeForget
49 , safeForgetEnv, showCG, showEnv, showEnvDbg, showSep
50 , sImplementationN, sMN, sNS, str, subst, substNames, substTerm
51 , substV, sUN, tcname, termSmallerThan, tfail, thead, tnull
52 , toAlist, traceWhen, txt, unApply, uniqueBinders, uniqueName
53 , uniqueNameFrom, uniqueNameSet, unList, updateDef, vToP, weakenTm
54 , rigPlus, rigMult, fstEnv, rigEnv, sndEnv, lookupBinder, envBinders
55 , envZero
56 ) where
58import Util.Pretty hiding (Str)
60-- Work around AMP without CPP
61import Prelude (Bool(..), Double, Enum(..), Eq(..), FilePath, Functor(..), Int,
62 Integer, Maybe(..), Monad(..), Monoid(..), Num(..), Ord(..),
63 Ordering(..), Show(..), String, div, error, fst, max, min, mod,
64 not, otherwise, read, snd, ($), (&&), (.), (||))
66#if (MIN_VERSION_base(4,11,0))
67import qualified Prelude as S (Semigroup(..))
68#endif
70import Control.Applicative (Alternative, Applicative(..))
71import qualified Control.Applicative as A (Alternative(..))
72import Control.DeepSeq (($!!))
73import Control.Monad.State.Strict
74import Data.Binary hiding (get, put)
75import Data.Char
76import Data.Data (Data)
77import Data.Foldable (Foldable)
78import Data.List hiding (group, insert)
79import qualified Data.Map.Strict as Map
80import Data.Maybe (listToMaybe)
81import Data.Set (Set, fromList, insert, member)
82import qualified Data.Text as T
83import Data.Traversable (Traversable)
84import Data.Typeable (Typeable)
85import Debug.Trace
86import GHC.Generics (Generic)
87import Numeric (showIntAtBase)
88import Numeric.IEEE (IEEE(identicalIEEE))
90data Option = TTypeInTType
91 | CheckConv
92 deriving Eq
94-- | Source location. These are typically produced by 'Idris.Parser.Stack.withExtent'
95data FC = FC { _fc_fname :: String, -- ^ Filename
96 _fc_start :: (Int, Int), -- ^ Line and column numbers for the start of the location span
97 _fc_end :: (Int, Int) -- ^ Line and column numbers for the end of the location span
98 }
99 | NoFC -- ^ Locations for machine-generated terms
100 | FileFC { _fc_fname :: String } -- ^ Locations with file only
101 deriving (Data, Generic, Typeable, Ord)
103-- TODO: find uses and destroy them, doing this case analysis at call sites
104-- | Give a notion of filename associated with an FC
105fc_fname :: FC -> String
106fc_fname (FC f _ _) = f
107fc_fname NoFC = "(no file)"
108fc_fname (FileFC f) = f
110-- TODO: find uses and destroy them, doing this case analysis at call sites
111-- | Give a notion of start location associated with an FC
112fc_start :: FC -> (Int, Int)
113fc_start (FC _ start _) = start
114fc_start NoFC = (0, 0)
115fc_start (FileFC f) = (0, 0)
117-- TODO: find uses and destroy them, doing this case analysis at call sites
118-- | Give a notion of end location associated with an FC
119fc_end :: FC -> (Int, Int)
120fc_end (FC _ _ end) = end
121fc_end NoFC = (0, 0)
122fc_end (FileFC f) = (0, 0)
124#if (MIN_VERSION_base(4,11,0))
125instance S.Semigroup FC where
126 (<>) = mappend
127#endif
129instance Monoid FC where
130 mempty = NoFC
132 -- | Get the largest span containing the two FCs
133 mappend (FC f start end) (FC f' start' end')
134 | f == f' = FC f (min start start') (max end end')
135 | otherwise = NoFC
136 mappend fc@(FC f _ _) (FileFC f') | f == f' = fc
137 | otherwise = NoFC
138 mappend (FileFC f') fc@(FC f _ _) | f == f' = fc
139 | otherwise = NoFC
140 mappend (FileFC f) (FileFC f') | f == f' = FileFC f
141 | otherwise = NoFC
142 mappend NoFC fc = fc
143 mappend fc NoFC = fc
146-- | Determine whether the first argument is completely contained in the second
147fcIn :: FC -> FC -> Bool
148fcIn NoFC _ = False
149fcIn (FileFC _) _ = False
150fcIn (FC {}) NoFC = False
151fcIn (FC {}) (FileFC _) = False
152fcIn (FC fn1 (sl1, sc1) (el1, ec1)) (FC fn2 (sl2, sc2) (el2, ec2)) =
153 fn1 == fn2 &&
154 (sl1 == sl2 && sc1 > sc2 || sl1 > sl2) &&
155 (el1 == el2 && ec1 < ec2 || el1 < el2)
157-- | Ignore source location equality (so deriving classes do not compare FCs)
158instance Eq FC where
159 _ == _ = True
161-- | FC with equality
162newtype FC' = FC' { unwrapFC :: FC } deriving (Data, Generic, Typeable, Ord)
164instance Eq FC' where
165 FC' fc == FC' fc' = fcEq fc fc'
166 where fcEq (FC n s e) (FC n' s' e') = n == n' && s == s' && e == e'
167 fcEq NoFC NoFC = True
168 fcEq (FileFC f) (FileFC f') = f == f'
169 fcEq _ _ = False
171instance Show FC' where
172 showsPrec d (FC' fc) = showsPrec d fc
174-- | Empty source location
175emptyFC :: FC
176emptyFC = NoFC
178-- | Source location with file only
179fileFC :: String -> FC
180fileFC s = FileFC s
182{-!
183deriving instance Binary FC
184!-}
186instance Sized FC where
187 size (FC f s e) = 4 + length f
188 size NoFC = 1
189 size (FileFC f) = length f
191instance Show FC where
192 show (FC f s e) = f ++ ":" ++ showLC s e
193 where showLC (sl, sc) (el, ec) | sl == el && sc == ec = show sl ++ ":" ++ show sc
194 | sl == el = show sl ++ ":" ++ show sc ++ "-" ++ show ec
195 | otherwise = show sl ++ ":" ++ show sc ++ "-" ++ show el ++ ":" ++ show ec
196 show NoFC = "No location"
197 show (FileFC f) = f
199-- | Output annotation for pretty-printed name - decides colour
200data NameOutput = TypeOutput | FunOutput | DataOutput | MetavarOutput | PostulateOutput deriving (Show, Eq, Ord, Generic)
202-- | Text formatting output
203data TextFormatting = BoldText | ItalicText | UnderlineText deriving (Show, Eq, Ord, Generic)
205-- | Output annotations for pretty-printing
206data OutputAnnotation = AnnName Name (Maybe NameOutput) (Maybe String) (Maybe String)
207 -- ^^ The name, classification, docs overview, and pretty-printed type
208 | AnnBoundName Name Bool
209 -- ^^ The name and whether it is implicit
210 | AnnConst Const
211 | AnnData String String -- ^ type, doc overview
212 | AnnType String String -- ^ name, doc overview
213 | AnnKeyword
214 | AnnFC FC
215 | AnnTextFmt TextFormatting
216 | AnnLink String -- ^ A link to this URL
217 | AnnTerm [(Name, Bool)] (TT Name) -- ^ pprint bound vars, original term
218 | AnnSearchResult Ordering -- ^ more general, isomorphic, or more specific
219 | AnnErr Err
220 | AnnNamespace [T.Text] (Maybe FilePath)
221 -- ^ A namespace (e.g. on an import line or in
222 -- a namespace declaration). Stored starting
223 -- at the root, with the hierarchy fully
224 -- resolved. If a file path is present, then
225 -- the namespace represents a module imported
226 -- from that file.
227 | AnnQuasiquote
228 | AnnAntiquote
229 | AnnSyntax String -- ^ type of syntax element: backslash or braces etc.
230 deriving (Show, Eq, Generic, Ord)
232-- | Used for error reflection
233data ErrorReportPart = TextPart String
234 | NamePart Name
235 | TermPart Term
236 | RawPart Raw
237 | SubReport [ErrorReportPart]
238 deriving (Show, Eq, Ord, Data, Generic, Typeable)
241data Provenance = ExpectedType
242 | TooManyArgs Term
243 | InferredVal
244 | GivenVal
245 | SourceTerm Term
246 deriving (Show, Eq, Ord, Data, Generic, Typeable)
247{-!
248deriving instance Binary Err
249!-}
252-- NB: Please remember to keep Err synchronised with
253-- Language.Reflection.Errors.Err in the stdlib!
255-- | Idris errors. Used as exceptions in the compiler, but reported to users
256-- if they reach the top level.
257data Err' t
258 = Msg String
259 | InternalMsg String
260 | CantUnify Bool (t, Maybe Provenance) -- Expected type, provenance
261 (t, Maybe Provenance) -- Actual type, provenance
262 (Err' t) [(Name, t)] Int
263 -- Int is 'score' - how much we did unify
264 -- Bool indicates recoverability, True indicates more info may make
265 -- unification succeed
266 | InfiniteUnify Name t [(Name, t)]
267 | CantConvert t t [(Name, t)]
268 | CantSolveGoal t [(Name, t)]
269 | UnifyScope Name Name t [(Name, t)]
270 | CantInferType String
271 | NonFunctionType t t
272 | NotEquality t t
273 | TooManyArguments Name
274 | CantIntroduce t
275 | NoSuchVariable Name
276 | WithFnType t
277 | NoTypeDecl Name
278 | NotInjective t t t
279 | CantResolve Bool -- True if postponed, False if fatal
280 t (Err' t) -- any further information
281 | InvalidTCArg Name t
282 | CantResolveAlts [Name]
283 | NoValidAlts [Name]
284 | IncompleteTerm t
285 | UniverseError FC UExp (Int, Int) (Int, Int) [ConstraintFC]
286 -- ^ Location, bad universe, old domain, new domain, suspects
287 | UniqueError Universe Name
288 | UniqueKindError Universe Name
289 | ProgramLineComment
290 | Inaccessible Name
291 | UnknownImplicit Name Name
292 | CantMatch t
293 | NonCollapsiblePostulate Name
294 | AlreadyDefined Name
295 | ProofSearchFail (Err' t)
296 | NoRewriting t t t
297 | At FC (Err' t)
298 | Elaborating String Name (Maybe t) (Err' t)
299 | ElaboratingArg Name Name [(Name, Name)] (Err' t)
300 | ProviderError String
301 | LoadingFailed String (Err' t)
302 | ReflectionError [[ErrorReportPart]] (Err' t)
303 | ReflectionFailed String (Err' t)
304 | ElabScriptDebug [ErrorReportPart] t [(Name, t, [(Name, Binder t)])]
305 -- ^ User-specified message, proof term, goals with context (first goal is focused)
306 | ElabScriptStuck t
307 | RunningElabScript (Err' t) -- ^ The error occurred during a top-level elaboration script
308 | ElabScriptStaging Name
309 | FancyMsg [ErrorReportPart]
310 deriving (Eq, Ord, Functor, Data, Generic, Typeable)
312type Err = Err' Term
314data TC a = OK !a
315 | Error Err
316 deriving (Eq, Functor)
318bindTC :: TC a -> (a -> TC b) -> TC b
319bindTC x k = case x of
320 OK v -> k v
321 Error e -> Error e
322{-# INLINE bindTC #-}
324instance Monad TC where
325 return x = OK x
326 x >>= k = bindTC x k
327 fail e = Error (InternalMsg e)
329instance MonadPlus TC where
330 mzero = fail "Unknown error"
331 (OK x) `mplus` _ = OK x
332 _ `mplus` (OK y) = OK y
333 err `mplus` _ = err
336instance Applicative TC where
337 pure = return
338 (<*>) = ap
340instance Alternative TC where
341 empty = mzero
342 (<|>) = mplus
344instance Sized ErrorReportPart where
345 size (TextPart msg) = 1 + length msg
346 size (TermPart t) = 1 + size t
347 size (RawPart r) = 1 + size r
348 size (NamePart n) = 1 + size n
349 size (SubReport rs) = 1 + size rs
351instance Sized Err where
352 size (Msg msg) = length msg
353 size (InternalMsg msg) = length msg
354 size (CantUnify _ left right err _ score) = size (fst left) + size (fst right) + size err
355 size (InfiniteUnify _ right _) = size right
356 size (CantConvert left right _) = size left + size right
357 size (UnifyScope _ _ right _) = size right
358 size (NoSuchVariable name) = size name
359 size (NoTypeDecl name) = size name
360 size (NotInjective l c r) = size l + size c + size r
361 size (CantResolve _ trm _) = size trm
362 size (NoRewriting l r t) = size l + size r + size t
363 size (CantResolveAlts _) = 1
364 size (IncompleteTerm trm) = size trm
365 size ProgramLineComment = 1
366 size (At fc err) = size fc + size err
367 size (Elaborating _ _ _ err) = size err
368 size (ElaboratingArg _ _ _ err) = size err
369 size (ProviderError msg) = length msg
370 size (LoadingFailed fn e) = 1 + length fn + size e
371 size _ = 1
373instance Show Err where
374 show (Msg s) = s
375 show (InternalMsg s) = "Internal error: " ++ show s
376 show (CantUnify rcv l r e sc i) = "CantUnify " ++ show rcv ++ " " ++
377 show l ++ " and " ++ show r ++ " " ++
378 show e ++ " in " ++ show sc ++ " " ++ show i
379 show (CantConvert l r sc) = "CantConvert " ++
380 show l ++ " and " ++ show r ++ " " ++
381 " in " ++ show sc
382 show (CantSolveGoal g _) = "CantSolve " ++ show g
383 show (Inaccessible n) = show n ++ " is not an accessible pattern variable"
384 show (UnknownImplicit n f) = show n ++ " is not an implicit argument of " ++ show f
385 show (ProviderError msg) = "Type provider error: " ++ msg
386 show (LoadingFailed fn e) = "Loading " ++ fn ++ " failed: (TT) " ++ show e
387 show ProgramLineComment = "Program line next to comment"
388 show (At f e) = show f ++ ":" ++ show e
389 show (ElaboratingArg f x prev e) = "Elaborating " ++ show f ++ " arg " ++
390 show x ++ ": " ++ show e
391 show (Elaborating what n ty e) = "Elaborating " ++ what ++ show n ++
392 showType ty ++ ":" ++ show e
393 where
394 showType Nothing = ""
395 showType (Just ty) = " with expected type " ++ show ty
396 show (ProofSearchFail e) = "Proof search fail: " ++ show e
397 show (InfiniteUnify _ _ _) = "InfiniteUnify"
398 show (UnifyScope _ _ _ _) = "UnifyScope"
399 show (NonFunctionType _ _) = "NonFunctionType"
400 show (NotEquality _ _) = "NotEquality"
401 show (TooManyArguments _) = "TooManyArguments"
402 show (CantIntroduce _) = "CantIntroduce"
403 show (NoSuchVariable n) = "NoSuchVariable " ++ show n
404 show (WithFnType _) = "WithFnType"
405 show (NoTypeDecl _) = "NoTypeDecl"
406 show (NotInjective _ _ _) = "NotInjective"
407 show (CantResolve _ _ _) = "CantResolve"
408 show (InvalidTCArg _ _) = "InvalidTCArg"
409 show (CantResolveAlts _) = "CantResolveAlts"
410 show (NoValidAlts _) = "NoValidAlts"
411 show (IncompleteTerm _) = "IncompleteTerm"
412 show _ = "Error"
414instance Pretty Err OutputAnnotation where
415 pretty (Msg m) = text m
416 pretty (CantUnify _ (l, _) (r, _) e _ i) =
417 text "Cannot unify" <+> colon <+> pretty l <+> text "and" <+> pretty r <+>
418 nest nestingSize (text "where" <+> pretty e <+> text "with" <+> (text . show $ i))
419 pretty (ProviderError msg) = text msg
420 pretty err@(LoadingFailed _ _) = text (show err)
421 pretty _ = text "Error"
423instance (Pretty a OutputAnnotation) => Pretty (TC a) OutputAnnotation where
424 pretty (OK ok) = pretty ok
425 pretty (Error err) =
426 text "Error" <+> colon <+> pretty err
428instance Show a => Show (TC a) where
429 show (OK x) = show x
430 show (Error str) = "Error: " ++ show str
432tfail :: Err -> TC a
433tfail e = Error e
435discard :: Monad m => m a -> m ()
436discard f = f >> return ()
438showSep :: String -> [String] -> String
439showSep sep [] = ""
440showSep sep [x] = x
441showSep sep (x:xs) = x ++ sep ++ showSep sep xs
443pmap f (x, y) = (f x, f y)
445traceWhen True msg a = trace msg a
446traceWhen False _ a = a
448-- RAW TERMS ----------------------------------------------------------------
450-- | Names are hierarchies of strings, describing scope (so no danger of
451-- duplicate names, but need to be careful on lookup).
452data Name = UN !T.Text -- ^ User-provided name
453 | NS !Name [T.Text] -- ^ Root, namespaces
454 | MN !Int !T.Text -- ^ Machine chosen names
455 | SN !SpecialName -- ^ Decorated function names
456 | SymRef Int -- ^ Reference to IBC file symbol table (used during serialisation)
457 deriving (Eq, Ord, Data, Generic, Typeable)
459txt :: String -> T.Text
460txt = T.pack
462str :: T.Text -> String
463str = T.unpack
465tnull :: T.Text -> Bool
466tnull = T.null
468thead :: T.Text -> Char
469thead = T.head
471-- Smart constructors for names, using old String style
472sUN :: String -> Name
473sUN s = UN (txt s)
475sNS :: Name -> [String] -> Name
476sNS n ss = NS n $!! (map txt ss)
478sMN :: Int -> String -> Name
479sMN i s = MN i (txt s)
481caseName (SN (CaseN _ _)) = True
482caseName (NS n _) = caseName n
483caseName _ = False
486{-!
487deriving instance Binary Name
488!-}
490data SpecialName = WhereN !Int !Name !Name
491 | WithN !Int !Name
492 | ImplementationN !Name [T.Text]
493 | ParentN !Name !T.Text
494 | MethodN !Name
495 | CaseN !FC' !Name
496 | ImplementationCtorN !Name
497 | MetaN !Name !Name
498 deriving (Eq, Ord, Data, Generic, Typeable)
499{-!
500deriving instance Binary SpecialName
501!-}
503sImplementationN :: Name -> [String] -> SpecialName
504sImplementationN n ss = ImplementationN n (map T.pack ss)
506instance Sized Name where
507 size (UN n) = 1
508 size (NS n els) = 1 + length els
509 size (MN i n) = 1
510 size _ = 1
512instance Pretty Name OutputAnnotation where
513 pretty n@(UN n') = annotate (AnnName n Nothing Nothing Nothing) $ text (T.unpack n')
514 pretty n@(NS un s) = annotate (AnnName n Nothing Nothing Nothing) . noAnnotate $ pretty un
515 pretty n@(MN i s) = annotate (AnnName n Nothing Nothing Nothing) $
516 lbrace <+> text (T.unpack s) <+> (text . show $ i) <+> rbrace
517 pretty n@(SN s) = annotate (AnnName n Nothing Nothing Nothing) $ text (show s)
518 pretty n@(SymRef i) = annotate (AnnName n Nothing Nothing Nothing) $
519 text $ "##symbol" ++ show i ++ "##"
521instance Pretty [Name] OutputAnnotation where
522 pretty = encloseSep empty empty comma . map pretty
524instance Show Name where
525 show (UN n) = str n
526 show (NS n s) = showSep "." (map T.unpack (reverse s)) ++ "." ++ show n
527 show (MN _ u) | u == txt "underscore" = "_"
528 show (MN i s) = "{" ++ str s ++ "_" ++ show i ++ "}"
529 show (SN s) = show s
530 show (SymRef i) = "##symbol" ++ show i ++ "##"
532instance Show SpecialName where
533 show (WhereN i p c) = show p ++ ", " ++ show c
534 show (WithN i n) = "with block in " ++ show n
535 show (ImplementationN cl impl) = showSep ", " (map T.unpack impl) ++ " implementation of " ++ show cl
536 show (MethodN m) = "method " ++ show m
537 show (ParentN p c) = show p ++ "#" ++ T.unpack c
538 show (CaseN fc n) = "case block in " ++ show n ++
539 if fc == FC' emptyFC then "" else " at " ++ show fc
540 show (ImplementationCtorN n) = "constructor of " ++ show n
541 show (MetaN parent meta) = "<<" ++ show parent ++ " " ++ show meta ++ ">>"
543-- Show a name in a way decorated for code generation, not human reading
544showCG :: Name -> String
545showCG (UN n) = T.unpack n
546showCG (NS n s) = showSep "." (map T.unpack (reverse s)) ++ "." ++ showCG n
547showCG (MN _ u) | u == txt "underscore" = "_"
548showCG (MN i s) = "{" ++ T.unpack s ++ "_" ++ show i ++ "}"
549showCG (SN s) = showCG' s
550 where showCG' (WhereN i p c) = showCG p ++ ":" ++ showCG c ++ ":" ++ show i
551 showCG' (WithN i n) = "_" ++ showCG n ++ "_with_" ++ show i
552 showCG' (ImplementationN cl impl) = '@':showCG cl ++ '$':showSep ":" (map T.unpack impl)
553 showCG' (MethodN m) = '!':showCG m
554 showCG' (ParentN p c) = showCG p ++ "#" ++ show c
555 showCG' (CaseN fc c) = showCG c ++ showFC' fc ++ "_case"
556 showCG' (ImplementationCtorN n) = showCG n ++ "_ictor"
557 showCG' (MetaN parent meta) = showCG parent ++ "_meta_" ++ showCG meta
558 showFC' (FC' NoFC) = ""
559 showFC' (FC' (FileFC f)) = "_" ++ cgFN f
560 showFC' (FC' (FC f s e))
561 | s == e = "_" ++ cgFN f ++
562 "_" ++ show (fst s) ++ "_" ++ show (snd s)
563 | otherwise = "_" ++ cgFN f ++
564 "_" ++ show (fst s) ++ "_" ++ show (snd s) ++
565 "_" ++ show (fst e) ++ "_" ++ show (snd e)
566 cgFN = concatMap (\c -> if not (isDigit c || isLetter c) then "__" else [c])
567showCG (SymRef i) = error "can't do codegen for a symbol reference"
570-- |Contexts allow us to map names to things. A root name maps to a collection
571-- of things in different namespaces with that name.
572type Ctxt a = Map.Map Name (Map.Map Name a)
573emptyContext = Map.empty
575mapCtxt :: (a -> b) -> Ctxt a -> Ctxt b
576mapCtxt = fmap . fmap
578-- |Return True if the argument 'Name' should be interpreted as the name of a
579-- interface.
580tcname (UN xs) = False
581tcname (NS n _) = tcname n
582tcname (SN (ImplementationN _ _)) = True
583tcname (SN (MethodN _)) = True
584tcname (SN (ParentN _ _)) = True
585tcname _ = False
587implicitable (NS n _) = False
588implicitable (UN xs) | T.null xs = False
589 | otherwise = isLower (T.head xs) ||
590 T.head xs == '_'
591implicitable (MN _ x) = not (tnull x) && thead x /= '_'
592implicitable _ = False
594nsroot (NS n _) = n
595nsroot n = n
597-- this will overwrite already existing definitions
598addDef :: Name -> a -> Ctxt a -> Ctxt a
599addDef n v ctxt = case Map.lookup (nsroot n) ctxt of
600 Nothing -> Map.insert (nsroot n)
601 (Map.insert n v Map.empty) ctxt
602 Just xs -> Map.insert (nsroot n)
603 (Map.insert n v xs) ctxt
605{-| Look up a name in the context, given an optional namespace.
606 The name (n) may itself have a (partial) namespace given.
608 Rules for resolution:
610 - if an explicit namespace is given, return the names which match it. If none
611 match, return all names.
613 - if the name has has explicit namespace given, return the names which match it
614 and ignore the given namespace.
616 - otherwise, return all names.
618-}
620lookupCtxtName :: Name -> Ctxt a -> [(Name, a)]
621lookupCtxtName n ctxt = case Map.lookup (nsroot n) ctxt of
622 Just xs -> filterNS (Map.toList xs)
623 Nothing -> []
624 where
625 filterNS [] = []
626 filterNS ((found, v) : xs)
627 | nsmatch n found = (found, v) : filterNS xs
628 | otherwise = filterNS xs
630 nsmatch (NS n ns) (NS p ps) = ns `isPrefixOf` ps
631 nsmatch (NS _ _) _ = False
632 nsmatch looking found = True
634lookupCtxt :: Name -> Ctxt a -> [a]
635lookupCtxt n ctxt = map snd (lookupCtxtName n ctxt)
637lookupCtxtExact :: Name -> Ctxt a -> Maybe a
638lookupCtxtExact n ctxt = listToMaybe [ v | (nm, v) <- lookupCtxtName n ctxt, nm == n]
640deleteDefExact :: Name -> Ctxt a -> Ctxt a
641deleteDefExact n = Map.adjust (Map.delete n) (nsroot n)
643updateDef :: Name -> (a -> a) -> Ctxt a -> Ctxt a
644updateDef n f ctxt
645 = case lookupCtxtExact n ctxt of
646 Just t -> addDef n (f t) ctxt
647 Nothing -> ctxt
649toAlist :: Ctxt a -> [(Name, a)]
650toAlist ctxt = let allns = map snd (Map.toList ctxt) in
651 concatMap (Map.toList) allns
653addAlist :: [(Name, a)] -> Ctxt a -> Ctxt a
654addAlist [] ctxt = ctxt
655addAlist ((n, tm) : ds) ctxt = addDef n tm (addAlist ds ctxt)
657data NativeTy = IT8 | IT16 | IT32 | IT64
658 deriving (Show, Eq, Ord, Enum, Data, Generic, Typeable)
660instance Pretty NativeTy OutputAnnotation where
661 pretty IT8 = text "Bits8"
662 pretty IT16 = text "Bits16"
663 pretty IT32 = text "Bits32"
664 pretty IT64 = text "Bits64"
666data IntTy = ITFixed NativeTy | ITNative | ITBig | ITChar
667 deriving (Show, Eq, Ord, Data, Generic, Typeable)
669intTyName :: IntTy -> String
670intTyName ITNative = "Int"
671intTyName ITBig = "BigInt"
672intTyName (ITFixed sized) = "B" ++ show (nativeTyWidth sized)
673intTyName (ITChar) = "Char"
675data ArithTy = ATInt IntTy | ATFloat -- TODO: Float vectors https://github.com/idris-lang/Idris-dev/issues/1723
676 deriving (Show, Eq, Ord, Data, Generic, Typeable)
678instance Pretty ArithTy OutputAnnotation where
679 pretty (ATInt ITNative) = text "Int"
680 pretty (ATInt ITBig) = text "BigInt"
681 pretty (ATInt ITChar) = text "Char"
682 pretty (ATInt (ITFixed n)) = pretty n
683 pretty ATFloat = text "Float"
685nativeTyWidth :: NativeTy -> Int
686nativeTyWidth IT8 = 8
687nativeTyWidth IT16 = 16
688nativeTyWidth IT32 = 32
689nativeTyWidth IT64 = 64
691data Const = I Int | BI Integer | Fl Double | Ch Char | Str String
692 | B8 Word8 | B16 Word16 | B32 Word32 | B64 Word64
693 | AType ArithTy | StrType
694 | WorldType | TheWorld
695 | VoidType | Forgot
696 deriving (Ord, Data, Generic, Typeable)
698-- We need to compare Double using bit-pattern identity rather than
699-- Haskell's Eq, which equates 0.0 and -0.0, leading to a
700-- contradiction in the type theory. Bit-pattern identity will also
701-- avoid similar problems for NaNs.
702instance Eq Const where
703 I i == I j = i == j
704 BI i == BI j = i == j
705 Fl i == Fl j = identicalIEEE i j
706 Ch i == Ch j = i == j
707 Str i == Str j = i == j
708 B8 i == B8 j = i == j
709 B16 i == B16 j = i == j
710 B32 i == B32 j = i == j
711 B64 i == B64 j = i == j
712 AType i == AType j = i == j
713 StrType == StrType = True
714 WorldType == WorldType = True
715 TheWorld == TheWorld = True
716 VoidType == VoidType = True
717 Forgot == Forgot = True
718 _ == _ = False
720{-!
721deriving instance Binary Const
722!-}
724isTypeConst :: Const -> Bool
725isTypeConst (AType _) = True
726isTypeConst StrType = True
727isTypeConst WorldType = True
728isTypeConst VoidType = True
729isTypeConst _ = False
731instance Sized Const where
732 size _ = 1
734instance Pretty Const OutputAnnotation where
735 pretty (I i) = text . show $ i
736 pretty (BI i) = text . show $ i
737 pretty (Fl f) = text . show $ f
738 pretty (Ch c) = text . show $ c
739 pretty (Str s) = text s
740 pretty (AType a) = pretty a
741 pretty StrType = text "String"
742 pretty TheWorld = text "%theWorld"
743 pretty WorldType = text "prim__World"
744 pretty VoidType = text "Void"
745 pretty Forgot = text "Forgot"
746 pretty (B8 w) = text . show $ w
747 pretty (B16 w) = text . show $ w
748 pretty (B32 w) = text . show $ w
749 pretty (B64 w) = text . show $ w
751-- | Determines whether the input constant represents a type
752constIsType :: Const -> Bool
753constIsType (I _) = False
754constIsType (BI _) = False
755constIsType (Fl _) = False
756constIsType (Ch _) = False
757constIsType (Str _) = False
758constIsType (B8 _) = False
759constIsType (B16 _) = False
760constIsType (B32 _) = False
761constIsType (B64 _) = False
762constIsType _ = True
764-- | Get the docstring for a Const
765constDocs :: Const -> String
766constDocs c@(AType (ATInt ITBig)) = "Arbitrary-precision integers"
767constDocs c@(AType (ATInt ITNative)) = "Fixed-precision integers of undefined size"
768constDocs c@(AType (ATInt ITChar)) = "Characters in some unspecified encoding"
769constDocs c@(AType ATFloat) = "Double-precision floating-point numbers"
770constDocs StrType = "Strings in some unspecified encoding"
771constDocs c@(AType (ATInt (ITFixed IT8))) = "Eight bits (unsigned)"
772constDocs c@(AType (ATInt (ITFixed IT16))) = "Sixteen bits (unsigned)"
773constDocs c@(AType (ATInt (ITFixed IT32))) = "Thirty-two bits (unsigned)"
774constDocs c@(AType (ATInt (ITFixed IT64))) = "Sixty-four bits (unsigned)"
775constDocs (Fl f) = "A float"
776constDocs (I i) = "A fixed-precision integer"
777constDocs (BI i) = "An arbitrary-precision integer"
778constDocs (Str s) = "A string of length " ++ show (length s)
779constDocs (Ch c) = "A character"
780constDocs (B8 w) = "The eight-bit value 0x" ++
781 showIntAtBase 16 intToDigit w ""
782constDocs (B16 w) = "The sixteen-bit value 0x" ++
783 showIntAtBase 16 intToDigit w ""
784constDocs (B32 w) = "The thirty-two-bit value 0x" ++
785 showIntAtBase 16 intToDigit w ""
786constDocs (B64 w) = "The sixty-four-bit value 0x" ++
787 showIntAtBase 16 intToDigit w ""
788constDocs prim = "Undocumented"
790data Universe = NullType | UniqueType | AllTypes
791 deriving (Eq, Ord, Data, Generic, Typeable)
793instance Show Universe where
794 show UniqueType = "UniqueType"
795 show NullType = "NullType"
796 show AllTypes = "AnyType"
798data Raw = Var Name
799 | RBind Name (Binder Raw) Raw
800 | RApp Raw Raw
801 | RType
802 | RUType Universe
803 | RConstant Const
804 deriving (Show, Eq, Ord, Data, Generic, Typeable)
806instance Sized Raw where
807 size (Var name) = 1
808 size (RBind name bind right) = 1 + size bind + size right
809 size (RApp left right) = 1 + size left + size right
810 size RType = 1
811 size (RUType _) = 1
812 size (RConstant const) = size const
814instance Pretty Raw OutputAnnotation where
815 pretty = text . show
817{-!
818deriving instance Binary Raw
819!-}
821data ImplicitInfo = Impl { tcimplementation :: Bool, toplevel_imp :: Bool,
822 machine_gen :: Bool }
823 deriving (Show, Eq, Ord, Data, Generic, Typeable)
825{-!
826deriving instance Binary ImplicitInfo
827!-}
829-- The type parameter `b` will normally be something like `TT Name` or just
830-- `Raw`. We do not make a type-level distinction between TT terms that happen
831-- to be TT types and TT terms that are not TT types.
832-- | All binding forms are represented in a uniform fashion. This type only represents
833-- the types of bindings (and their values, if any); the attached identifiers are part
834-- of the 'Bind' constructor for the 'TT' type.
835data Binder b = Lam { binderCount :: RigCount,
836 binderTy :: !b {-^ type annotation for bound variable-}}
837 -- ^ A function binding
838 | Pi { binderCount :: RigCount,
839 binderImpl :: Maybe ImplicitInfo,
840 binderTy :: !b,
841 binderKind :: !b }
842 -- ^ A binding that occurs in a function type
843 -- expression, e.g. @(x:Int) -> ...@ The 'binderImpl'
844 -- flag says whether it was a scoped implicit
845 -- (i.e. forall bound) in the high level Idris, but
846 -- otherwise has no relevance in TT.
847 | Let { binderCount :: RigCount,
848 binderTy :: !b,
849 binderVal :: b {-^ value for bound variable-}}
850 -- ^ A binding that occurs in a @let@ expression
851 | NLet { binderTy :: !b,
852 binderVal :: b }
853 -- ^ NLet is an intermediate product in the evaluator
854 -- that's used for temporarily naming locals during
855 -- reduction. It won't occur outside the evaluator.
856 | Hole { binderTy :: !b}
857 -- ^ A hole in a term under construction in the
858 -- elaborator. If this is not filled during
859 -- elaboration, it is an error.
860 | GHole { envlen :: Int,
861 localnames :: [Name],
862 binderTy :: !b}
863 -- ^ A saved TT hole that will later be converted to a
864 -- top-level Idris metavariable applied to all
865 -- elements of its local environment.
866 | Guess { binderTy :: !b,
867 binderVal :: b }
868 -- ^ A provided value for a hole. It will later be
869 -- substituted - the guess is to keep it
870 -- computationally inert while working on other things
871 -- if necessary.
872 | PVar { binderCount :: RigCount,
873 binderTy :: !b }
874 -- ^ A pattern variable (these are bound around terms
875 -- that make up pattern-match clauses)
876 | PVTy { binderTy :: !b }
877 -- ^ The type of a pattern binding
878 deriving (Show, Eq, Ord, Functor, Foldable, Traversable, Data, Generic, Typeable)
879{-!
880deriving instance Binary Binder
881!-}
883instance Sized a => Sized (Binder a) where
884 size (Lam _ ty) = 1 + size ty
885 size (Pi _ _ ty _) = 1 + size ty
886 size (Let _ ty val) = 1 + size ty + size val
887 size (NLet ty val) = 1 + size ty + size val
888 size (Hole ty) = 1 + size ty
889 size (GHole _ _ ty) = 1 + size ty
890 size (Guess ty val) = 1 + size ty + size val
891 size (PVar _ ty) = 1 + size ty
892 size (PVTy ty) = 1 + size ty
894fmapMB :: Monad m => (a -> m b) -> Binder a -> m (Binder b)
895fmapMB f (Let c t v) = liftM2 (Let c) (f t) (f v)
896fmapMB f (NLet t v) = liftM2 NLet (f t) (f v)
897fmapMB f (Guess t v) = liftM2 Guess (f t) (f v)
898fmapMB f (Lam c t) = liftM (Lam c) (f t)
899fmapMB f (Pi c i t k) = liftM2 (Pi c i) (f t) (f k)
900fmapMB f (Hole t) = liftM Hole (f t)
901fmapMB f (GHole i ns t) = liftM (GHole i ns) (f t)
902fmapMB f (PVar c t) = liftM (PVar c) (f t)
903fmapMB f (PVTy t) = liftM PVTy (f t)
905raw_apply :: Raw -> [Raw] -> Raw
906raw_apply f [] = f
907raw_apply f (a : as) = raw_apply (RApp f a) as
909raw_unapply :: Raw -> (Raw, [Raw])
910raw_unapply t = ua [] t where
911 ua args (RApp f a) = ua (a:args) f
912 ua args t = (t, args)
914-- WELL TYPED TERMS ---------------------------------------------------------
916internalNS :: String
917internalNS = "(internal)"
919-- | Universe expressions for universe checking
920data UExp = UVar String Int -- ^ universe variable, with source file to disambiguate
921 | UVal Int -- ^ explicit universe level
922 deriving (Eq, Ord, Data, Generic, Typeable)
924instance Sized UExp where
925 size _ = 1
927instance Show UExp where
928 show (UVar ns x)
929 | x < 26 = ns ++ "." ++ [toEnum (x + fromEnum 'a')]
930 | otherwise = ns ++ "." ++ toEnum ((x `mod` 26) + fromEnum 'a') : show (x `div` 26)
931 show (UVal x) = show x
932-- show (UMax l r) = "max(" ++ show l ++ ", " ++ show r ++")"
934-- | Universe constraints
935data UConstraint = ULT UExp UExp -- ^ Strictly less than
936 | ULE UExp UExp -- ^ Less than or equal to
937 deriving (Eq, Ord, Data, Generic, Typeable)
939data ConstraintFC = ConstraintFC { uconstraint :: UConstraint,
940 ufc :: FC }
941 deriving (Show, Data, Generic, Typeable)
943instance Eq ConstraintFC where
944 x == y = uconstraint x == uconstraint y
946instance Ord ConstraintFC where
947 compare x y = compare (uconstraint x) (uconstraint y)
949instance Show UConstraint where
950 show (ULT x y) = show x ++ " < " ++ show y
951 show (ULE x y) = show x ++ " <= " ++ show y
953type UCs = (Int, [UConstraint])
955data NameType = Bound
956 | Ref
957 | DCon {nt_tag :: Int, nt_arity :: Int, nt_unique :: Bool} -- ^ Data constructor
958 | TCon {nt_tag :: Int, nt_arity :: Int} -- ^ Type constructor
959 deriving (Show, Ord, Data, Generic, Typeable)
960{-!
961deriving instance Binary NameType
962!-}
964instance Sized NameType where
965 size _ = 1
967instance Pretty NameType OutputAnnotation where
968 pretty = text . show
970instance Eq NameType where
971 Bound == Bound = True
972 Ref == Ref = True
973 DCon _ a _ == DCon _ b _ = (a == b) -- ignore tag
974 TCon _ a == TCon _ b = (a == b) -- ignore tag
975 _ == _ = False
977data AppStatus n = Complete
978 | MaybeHoles
979 | Holes [n]
980 deriving (Eq, Ord, Functor, Data, Generic, Typeable, Show)
982-- | Terms in the core language. The type parameter is the type of
983-- identifiers used for bindings and explicit named references;
984-- usually we use @TT 'Name'@.
985data TT n = P NameType n (TT n) -- ^ named references with type
986 -- (P for "Parameter", motivated by McKinna and Pollack's
987 -- Pure Type Systems Formalized)
988 | V !Int -- ^ a resolved de Bruijn-indexed variable
989 | Bind n !(Binder (TT n)) (TT n) -- ^ a binding
990 | App (AppStatus n) !(TT n) (TT n) -- ^ function, function type, arg
991 | Constant Const -- ^ constant
992 | Proj (TT n) !Int -- ^ argument projection; runtime only
993 -- (-1) is a special case for 'subtract one from BI'
994 | Erased -- ^ an erased term
995 | Impossible -- ^ special case for totality checking
996 | Inferred (TT n) -- ^ For building case trees when coverage checkimg only.
997 -- Marks a term as being inferred by the machine, rather than
998 -- given by the programmer
999 | TType UExp -- ^ the type of types at some level
1000 | UType Universe -- ^ Uniqueness type universe (disjoint from TType)
1001 deriving (Ord, Functor, Data, Generic, Typeable)
1002{-!
1003deriving instance Binary TT
1004!-}
1006class TermSize a where
1007 termsize :: Name -> a -> Int
1009instance TermSize a => TermSize [a] where
1010 termsize n [] = 0
1011 termsize n (x : xs) = termsize n x + termsize n xs
1013instance TermSize (TT Name) where
1014 termsize n (P _ n' _)
1015 | n' == n = 1000000 -- recursive => really big
1016 | caseName n' = 1000000 -- case, not safe to inline for termination check
1017 | otherwise = 1
1018 termsize n (V _) = 1
1019 -- for `Bind` terms, we can erroneously declare a term
1020 -- "recursive => really big" if the name of the bound
1021 -- variable is the same as the name we're using
1022 -- So generate a different name in that case.
1023 termsize n (Bind n' (Let c t v) sc)
1024 = let rn = if n == n' then sMN 0 "noname" else n in
1025 termsize rn v + termsize rn sc
1026 termsize n (Bind n' b sc)
1027 = let rn = if n == n' then sMN 0 "noname" else n in
1028 termsize rn sc
1029 termsize n (App _ f a) = termsize n f + termsize n a
1030 termsize n (Proj t i) = termsize n t
1031 termsize n _ = 1
1033instance Sized Universe where
1034 size u = 1
1036instance Sized a => Sized (TT a) where
1037 size (P name n trm) = 1 + size name + size n + size trm
1038 size (V v) = 1
1039 size (Bind nm binder bdy) = 1 + size nm + size binder + size bdy
1040 size (App _ l r) = 1 + size l + size r
1041 size (Constant c) = size c
1042 size Erased = 1
1043 size (TType u) = 1 + size u
1044 size (Proj a _) = 1 + size a
1045 size Impossible = 1
1046 size (Inferred t) = size t
1047 size (UType u) = 1 + size u
1049instance Pretty a o => Pretty (TT a) o where
1050 pretty _ = text "test"
1052data RigCount = Rig0 | Rig1 | RigW
1053 deriving (Show, Eq, Ord, Data, Generic, Typeable)
1055rigPlus :: RigCount -> RigCount -> RigCount
1056rigPlus Rig0 Rig0 = Rig0
1057rigPlus Rig0 Rig1 = Rig1
1058rigPlus Rig0 RigW = RigW
1059rigPlus Rig1 Rig0 = Rig1
1060rigPlus Rig1 Rig1 = RigW
1061rigPlus Rig1 RigW = RigW
1062rigPlus RigW Rig0 = RigW
1063rigPlus RigW Rig1 = RigW
1064rigPlus RigW RigW = RigW
1066rigMult :: RigCount -> RigCount -> RigCount
1067rigMult Rig0 Rig0 = Rig0
1068rigMult Rig0 Rig1 = Rig0
1069rigMult Rig0 RigW = Rig0
1070rigMult Rig1 Rig0 = Rig0
1071rigMult Rig1 Rig1 = Rig1
1072rigMult Rig1 RigW = RigW
1073rigMult RigW Rig0 = Rig0
1074rigMult RigW Rig1 = RigW
1075rigMult RigW RigW = RigW
1077type EnvTT n = [(n, RigCount, Binder (TT n))]
1079fstEnv (n, c, b) = n
1080rigEnv (n, c, b) = c
1081sndEnv (n, c, b) = b
1083envBinders = map (\(n, _, b) -> (n, b))
1084envZero = map (\(n, _, b) -> (n, Rig0, b))
1086lookupBinder :: Eq n => n -> EnvTT n -> Maybe (Binder (TT n))
1087lookupBinder n = lookup n . envBinders
1089data Datatype n = Data { d_typename :: n,
1090 d_typetag :: Int,
1091 d_type :: (TT n),
1092 d_unique :: Bool,
1093 d_cons :: [(n, TT n)] }
1094 deriving (Show, Functor, Eq)
1096-- | Data declaration options
1097data DataOpt = Codata -- ^ Set if the the data-type is coinductive
1098 | DataErrRev
1099 deriving (Show, Eq, Generic)
1101type DataOpts = [DataOpt]
1103data TypeInfo = TI { con_names :: [Name],
1104 codata :: Bool,
1105 data_opts :: DataOpts,
1106 param_pos :: [Int],
1107 mutual_types :: [Name],
1108 linear_con :: Bool -- is there a linear argument?
1110 deriving (Show, Generic)
1111{-!
1112deriving instance Binary TypeInfo
1113!-}
1115instance Eq n => Eq (TT n) where
1116 (==) (P xt x _) (P yt y _) = x == y
1117 (==) (V x) (V y) = x == y
1118 (==) (Bind _ xb xs) (Bind _ yb ys) = xs == ys && xb == yb
1119 (==) (App _ fx ax) (App _ fy ay) = ax == ay && fx == fy
1120 (==) (TType _) (TType _) = True -- deal with constraints later
1121 (==) (Constant x) (Constant y) = x == y
1122 (==) (Proj x i) (Proj y j) = x == y && i == j
1123 (==) Erased _ = True
1124 (==) _ Erased = True
1125 (==) _ _ = False
1127-- * A few handy operations on well typed terms:
1129-- | A term is injective iff it is a data constructor, type constructor,
1130-- constant, the type Type, pi-binding, or an application of an injective
1131-- term.
1132isInjective :: TT n -> Bool
1133isInjective (P (DCon _ _ _) _ _) = True
1134isInjective (P (TCon _ _) _ _) = True
1135isInjective (Constant _) = True
1136isInjective (TType x) = True
1137isInjective (Bind _ (Pi _ _ _ _) sc) = True
1138isInjective (App _ f a) = isInjective f
1139isInjective _ = False
1141-- | Replace the outermost (index 0) de Bruijn variable with the given term
1142instantiate :: TT n -> TT n -> TT n
1143instantiate e = subst 0 where
1144 subst i (P nt x ty) = P nt x (subst i ty)
1145 subst i (V x) | i == x = e
1146 subst i (Bind x b sc) = Bind x (fmap (subst i) b) (subst (i+1) sc)
1147 subst i (App s f a) = App s (subst i f) (subst i a)
1148 subst i (Proj x idx) = Proj (subst i x) idx
1149 subst i t = t
1151-- | As 'instantiate', but also decrement the indices of all de Bruijn variables
1152-- remaining in the term, so that there are no more references to the variable
1153-- that has been substituted.
1154substV :: TT n -> TT n -> TT n
1155substV x tm = dropV 0 (instantiate x tm) where
1156 dropV i (P nt x ty) = P nt x (dropV i ty)
1157 dropV i (V x) | x > i = V (x - 1)
1158 | otherwise = V x
1159 dropV i (Bind x b sc) = Bind x (fmap (dropV i) b) (dropV (i+1) sc)
1160 dropV i (App s f a) = App s (dropV i f) (dropV i a)
1161 dropV i (Proj x idx) = Proj (dropV i x) idx
1162 dropV i t = t
1164-- | Replace all non-free de Bruijn references in the given term with references
1165-- to the name of their binding.
1166explicitNames :: TT n -> TT n
1167explicitNames (Bind x b sc) = let b' = fmap explicitNames b in
1168 Bind x b'
1169 (explicitNames (instantiate
1170 (P Bound x (binderTy b')) sc))
1171explicitNames (App s f a) = App s (explicitNames f) (explicitNames a)
1172explicitNames (Proj x idx) = Proj (explicitNames x) idx
1173explicitNames t = t
1175-- | Replace references to the given 'Name'-like id with references to
1176-- de Bruijn index 0.
1177pToV :: Eq n => n -> TT n -> TT n
1178pToV n = pToV' n 0
1179pToV' n i (P _ x _) | n == x = V i
1180pToV' n i (Bind x b sc)
1181-- We can assume the inner scope has been pToVed already, so continue to
1182-- resolve names from the *outer* scope which may happen to have the same id.
1183 | n == x = Bind x (fmap (pToV' n i) b) sc
1184 | otherwise = Bind x (fmap (pToV' n i) b) (pToV' n (i+1) sc)
1185pToV' n i (App s f a) = App s (pToV' n i f) (pToV' n i a)
1186pToV' n i (Proj t idx) = Proj (pToV' n i t) idx
1187pToV' n i t = t
1189-- increase de Bruijn indices, as if a binder has been added
1190addBinder :: TT n -> TT n
1191addBinder t = ab 0 t
1192 where
1193 ab top (V i) | i >= top = V (i + 1)
1194 | otherwise = V i
1195 ab top (Bind x b sc) = Bind x (fmap (ab top) b) (ab (top + 1) sc)
1196 ab top (App s f a) = App s (ab top f) (ab top a)
1197 ab top (Proj t idx) = Proj (ab top t) idx
1198 ab top t = t
1200-- | Convert several names. First in the list comes out as V 0
1201pToVs :: Eq n => [n] -> TT n -> TT n
1202pToVs ns tm = pToVs' ns tm 0 where
1203 pToVs' [] tm i = tm
1204 pToVs' (n:ns) tm i = pToV' n i (pToVs' ns tm (i+1))
1206-- | Replace de Bruijn indices in the given term with explicit references to
1207-- the names of the bindings they refer to. It is an error if the given term
1208-- contains free de Bruijn indices.
1209vToP :: TT n -> TT n
1210vToP = vToP' [] where
1211 vToP' env (V i) = let (n, b) = (env !! i) in
1212 P Bound n (binderTy b)
1213 vToP' env (Bind n b sc) = let b' = fmap (vToP' env) b in
1214 Bind n b' (vToP' ((n, b'):env) sc)
1215 vToP' env (App s f a) = App s (vToP' env f) (vToP' env a)
1216 vToP' env t = t
1218-- | Replace every non-free reference to the name of a binding in
1219-- the given term with a de Bruijn index.
1220finalise :: Eq n => TT n -> TT n
1221finalise (Bind x b sc) = Bind x (fmap finalise b) (pToV x (finalise sc))
1222finalise (App s f a) = App s (finalise f) (finalise a)
1223finalise t = t
1225-- Once we've finished checking everything about a term we no longer need
1226-- the type on the 'P' so erase it so save memory
1228pEraseType :: TT n -> TT n
1229pEraseType (P nt t _) = P nt t Erased
1230pEraseType (App s f a) = App s (pEraseType f) (pEraseType a)
1231pEraseType (Bind n b sc) = Bind n (fmap pEraseType b) (pEraseType sc)
1232pEraseType t = t
1234-- | As 'instantiate', but in addition to replacing @'V' 0@,
1235-- replace references to the given 'Name'-like id.
1236subst :: Eq n => n {-^ The id to replace -} ->
1237 TT n {-^ The replacement term -} ->
1238 TT n {-^ The term to replace in -} ->
1239 TT n
1240-- subst n v tm = instantiate v (pToV n tm)
1241subst n v tm = fst $ subst' 0 tm
1242 where
1243 -- keep track of updates to save allocations - this is a big win on
1244 -- large terms in particular
1245 -- ('Maybe' would be neater here, but >>= is not the right combinator.
1246 -- Feel free to tidy up, as long as it still saves allocating when no
1247 -- substitution happens...)
1248 subst' i (V x) | i == x = (v, True)
1249 subst' i (P _ x _) | n == x = (v, True)
1250 subst' i t@(P nt x ty)
1251 = let (ty', ut) = subst' i ty in
1252 if ut then (P nt x ty', True) else (t, False)
1253 subst' i t@(Bind x b sc) | x /= n
1254 = let (b', ub) = substB' i b
1255 (sc', usc) = subst' (i+1) sc in
1256 if ub || usc then (Bind x b' sc', True) else (t, False)
1257 subst' i t@(App s f a) = let (f', uf) = subst' i f
1258 (a', ua) = subst' i a in
1259 if uf || ua then (App s f' a', True) else (t, False)
1260 subst' i t@(Proj x idx) = let (x', u) = subst' i x in
1261 if u then (Proj x' idx, u) else (t, False)
1262 subst' i t = (t, False)
1264 substB' i b@(Let c t v) = let (t', ut) = subst' i t
1265 (v', uv) = subst' i v in
1266 if ut || uv then (Let c t' v', True)
1267 else (b, False)
1268 substB' i b@(Guess t v) = let (t', ut) = subst' i t
1269 (v', uv) = subst' i v in
1270 if ut || uv then (Guess t' v', True)
1271 else (b, False)
1272 substB' i b = let (ty', u) = subst' i (binderTy b) in
1273 if u then (b { binderTy = ty' }, u) else (b, False)
1275-- If there are no Vs in the term (i.e. in proof state)
1276psubst :: Eq n => n -> TT n -> TT n -> TT n
1277psubst n v tm = s' 0 tm where
1278 s' i (V x) | x > i = V (x - 1)
1279 | x == i = v
1280 | otherwise = V x
1281 s' i (P _ x _) | n == x = v
1282 s' i (Bind x b sc) | n == x = Bind x (fmap (s' i) b) sc
1283 | otherwise = Bind x (fmap (s' i) b) (s' (i+1) sc)
1284 s' i (App st f a) = App st (s' i f) (s' i a)
1285 s' i (Proj t idx) = Proj (s' i t) idx
1286 s' i t = t
1288-- | As 'subst', but takes a list of (name, substitution) pairs instead
1289-- of a single name and substitution
1290substNames :: Eq n => [(n, TT n)] -> TT n -> TT n
1291substNames [] t = t
1292substNames ((n, tm) : xs) t = subst n tm (substNames xs t)
1294-- | Replaces all terms equal (in the sense of @(==)@) to
1295-- the old term with the new term.
1296substTerm :: Eq n => TT n {-^ Old term -} ->
1297 TT n {-^ New term -} ->
1298 TT n {-^ template term -}
1299 -> TT n
1300substTerm old new = st where
1301 st t | eqAlpha [] t old = new
1302 st (App s f a) = App s (st f) (st a)
1303 st (Bind x b sc) = Bind x (fmap st b) (st sc)
1304 st t = t
1306 eqAlpha as (P _ x _) (P _ y _)
1307 = x == y || (x, y) `elem` as || (y, x) `elem` as
1308 eqAlpha as (V x) (V y) = x == y
1309 eqAlpha as (Bind x xb xs) (Bind y yb ys)
1310 = eqAlphaB as xb yb && eqAlpha ((x, y) : as) xs ys
1311 eqAlpha as (App _ fx ax) (App _ fy ay) = eqAlpha as fx fy && eqAlpha as ax ay
1312 eqAlpha as x y = x == y
1314 eqAlphaB as (Let xc xt xv) (Let yc yt yv)
1315 = eqAlpha as xt yt && eqAlpha as xv yv
1316 eqAlphaB as (Guess xt xv) (Guess yt yv)
1317 = eqAlpha as xt yt && eqAlpha as xv yv
1318 eqAlphaB as bx by = eqAlpha as (binderTy bx) (binderTy by)
1320-- | Return number of occurrences of V 0 or bound name i the term
1321occurrences :: Eq n => n -> TT n -> Int
1322occurrences n t = execState (no' 0 t) 0
1323 where
1324 no' i (V x) | i == x = do num <- get; put (num + 1)
1325 no' i (P Bound x _) | n == x = do num <- get; put (num + 1)
1326 no' i (Bind n b sc) = do noB' i b; no' (i+1) sc
1327 where noB' i (Let c t v) = do no' i t; no' i v
1328 noB' i (Guess t v) = do no' i t; no' i v
1329 noB' i b = no' i (binderTy b)
1330 no' i (App _ f a) = do no' i f; no' i a
1331 no' i (Proj x _) = no' i x
1332 no' i _ = return ()
1334-- | Returns true if V 0 and bound name n do not occur in the term
1335noOccurrence :: Eq n => n -> TT n -> Bool
1336noOccurrence n t = no' 0 t
1337 where
1338 no' i (V x) = not (i == x)
1339 no' i (P Bound x _) = not (n == x)
1340 no' i (Bind n b sc) = noB' i b && no' (i+1) sc
1341 where noB' i (Let c t v) = no' i t && no' i v
1342 noB' i (Guess t v) = no' i t && no' i v
1343 noB' i b = no' i (binderTy b)
1344 no' i (App _ f a) = no' i f && no' i a
1345 no' i (Proj x _) = no' i x
1346 no' i _ = True
1348-- | Returns all names used free in the term
1349freeNames :: Eq n => TT n -> [n]
1350freeNames t = nub $ freeNames' t
1351 where
1352 freeNames' (P _ n _) = [n]
1353 freeNames' (Bind n (Let c t v) sc) = freeNames' v ++ (freeNames' sc \\ [n])
1354 ++ freeNames' t
1355 freeNames' (Bind n b sc) = freeNames' (binderTy b) ++ (freeNames' sc \\ [n])
1356 freeNames' (App _ f a) = freeNames' f ++ freeNames' a
1357 freeNames' (Proj x i) = freeNames' x
1358 freeNames' _ = []
1360-- | Return the arity of a (normalised) type
1361arity :: TT n -> Int
1362arity (Bind n (Pi _ _ t _) sc) = 1 + arity sc
1363arity _ = 0
1365-- | Deconstruct an application; returns the function and a list of arguments
1366unApply :: TT n -> (TT n, [TT n])
1367unApply t = ua [] t where
1368 ua args (App _ f a) = ua (a:args) f
1369 ua args t = (t, args)
1371-- | Returns a term representing the application of the first argument
1372-- (a function) to every element of the second argument.
1373mkApp :: TT n -> [TT n] -> TT n
1374mkApp f [] = f
1375mkApp f (a:as) = mkApp (App MaybeHoles f a) as
1377unList :: Term -> Maybe [Term]
1378unList tm = case unApply tm of
1379 (nil, [_]) -> Just []
1380 (cons, ([_, x, xs])) ->
1381 do rest <- unList xs
1382 return $ x:rest
1383 (f, args) -> Nothing
1385-- | Hard-code a heuristic maximum term size, to prevent attempts to
1386-- serialize or force infinite or just gigantic terms
1387termSmallerThan :: Int -> Term -> Bool
1388termSmallerThan x tm | x <= 0 = False
1389termSmallerThan x (P _ _ ty) = termSmallerThan (x-1) ty
1390termSmallerThan x (Bind _ _ tm) = termSmallerThan (x-1) tm
1391termSmallerThan x (App _ f a) = termSmallerThan (x-1) f && termSmallerThan (x-1) a
1392termSmallerThan x (Proj tm _) = termSmallerThan (x-1) tm
1393termSmallerThan x (V i) = True
1394termSmallerThan x (Constant c) = True
1395termSmallerThan x Erased = True
1396termSmallerThan x Impossible = True
1397termSmallerThan x (Inferred t) = termSmallerThan x t
1398termSmallerThan x (TType u) = True
1399termSmallerThan x (UType u) = True
1402-- | Cast a 'TT' term to a 'Raw' value, discarding universe information and
1403-- the types of named references and replacing all de Bruijn indices
1404-- with the corresponding name. It is an error if there are free de
1405-- Bruijn indices.
1406forget :: TT Name -> Raw
1407forget tm = forgetEnv [] tm
1409safeForget :: TT Name -> Maybe Raw
1410safeForget tm = safeForgetEnv [] tm
1412forgetEnv :: [Name] -> TT Name -> Raw
1413forgetEnv env tm = case safeForgetEnv env tm of
1414 Just t' -> t'
1415 Nothing -> error $ "Scope error in " ++ show tm ++ show env
1418safeForgetEnv :: [Name] -> TT Name -> Maybe Raw
1419safeForgetEnv env (P _ n _) = Just $ Var n
1420safeForgetEnv env (V i) | i < length env = Just $ Var (env !! i)
1421 | otherwise = Nothing
1422safeForgetEnv env (Bind n b sc)
1423 = do let n' = uniqueName n env
1424 b' <- safeForgetEnvB env b
1425 sc' <- safeForgetEnv (n':env) sc
1426 Just $ RBind n' b' sc'
1427 where safeForgetEnvB env (Let c t v) = liftM2 (Let c) (safeForgetEnv env t)
1428 (safeForgetEnv env v)
1429 safeForgetEnvB env (Guess t v) = liftM2 Guess (safeForgetEnv env t)
1430 (safeForgetEnv env v)
1431 safeForgetEnvB env b = do ty' <- safeForgetEnv env (binderTy b)
1432 Just $ fmap (\_ -> ty') b
1433safeForgetEnv env (App _ f a) = liftM2 RApp (safeForgetEnv env f) (safeForgetEnv env a)
1434safeForgetEnv env (Constant c) = Just $ RConstant c
1435safeForgetEnv env (TType i) = Just RType
1436safeForgetEnv env (UType u) = Just $ RUType u
1437safeForgetEnv env Erased = Just $ RConstant Forgot
1438safeForgetEnv env (Proj tm i) = error "Don't know how to forget a projection"
1439safeForgetEnv env Impossible = error "Don't know how to forget Impossible"
1440safeForgetEnv env (Inferred t) = safeForgetEnv env t
1442-- | Introduce a 'Bind' into the given term for each element of the
1443-- given list of (name, binder) pairs.
1444bindAll :: [(n, Binder (TT n))] -> TT n -> TT n
1445bindAll [] t = t
1446bindAll ((n, b) : bs) t = Bind n b (bindAll bs t)
1448-- | Like 'bindAll', but the 'Binder's are 'TT' terms instead.
1449-- The first argument is a function to map @TT@ terms to @Binder@s.
1450-- This function might often be something like 'Lam', which directly
1451-- constructs a @Binder@ from a @TT@ term.
1452bindTyArgs :: (TT n -> Binder (TT n)) -> [(n, TT n)] -> TT n -> TT n
1453bindTyArgs b xs = bindAll (map (\ (n, ty) -> (n, b ty)) xs)
1455-- | Return a list of pairs of the names of the outermost 'Pi'-bound
1456-- variables in the given term, together with their types.
1457getArgTys :: TT n -> [(n, TT n)]
1458getArgTys (Bind n (PVar _ _) sc) = getArgTys sc
1459getArgTys (Bind n (PVTy _) sc) = getArgTys sc
1460getArgTys (Bind n (Pi _ _ t _) sc) = (n, t) : getArgTys sc
1461getArgTys _ = []
1463getRetTy :: TT n -> TT n
1464getRetTy (Bind n (PVar _ _) sc) = getRetTy sc
1465getRetTy (Bind n (PVTy _) sc) = getRetTy sc
1466getRetTy (Bind n (Pi _ _ _ _) sc) = getRetTy sc
1467getRetTy sc = sc
1469-- | As getRetTy but substitutes names for de Bruijn indices
1470substRetTy :: TT n -> TT n
1471substRetTy (Bind n (PVar _ ty) sc) = substRetTy (substV (P Ref n ty) sc)
1472substRetTy (Bind n (PVTy ty) sc) = substRetTy (substV (P Ref n ty) sc)
1473substRetTy (Bind n (Pi _ _ ty _) sc) = substRetTy (substV (P Ref n ty) sc)
1474substRetTy sc = sc
1477uniqueNameFrom :: [Name] -> [Name] -> Name
1478uniqueNameFrom [] hs = uniqueName (nextName (sUN "x")) hs
1479uniqueNameFrom (s : supply) hs
1480 | s `elem` hs = uniqueNameFrom supply hs
1481 | otherwise = s
1483uniqueName :: Name -> [Name] -> Name
1484uniqueName n hs | n `elem` hs = uniqueName (nextName n) hs
1485 | otherwise = n
1487uniqueNameSet :: Name -> Set Name -> Name
1488uniqueNameSet n hs | n `member` hs = uniqueNameSet (nextName n) hs
1489 | otherwise = n
1491uniqueBinders :: [Name] -> TT Name -> TT Name
1492uniqueBinders ns = ubSet (fromList ns) where
1493 ubSet ns (Bind n b sc)
1494 = let n' = uniqueNameSet n ns
1495 ns' = insert n' ns in
1496 Bind n' (fmap (ubSet ns') b) (ubSet ns' sc)
1497 ubSet ns (App s f a) = App s (ubSet ns f) (ubSet ns a)
1498 ubSet ns t = t
1501nextName :: Name -> Name
1502nextName (NS x s) = NS (nextName x) s
1503nextName (MN i n) = MN (i+1) n
1504nextName (UN x) = let (num', nm') = T.span isDigit (T.reverse x)
1505 nm = T.reverse nm'
1506 num = readN (T.reverse num') in
1507 UN (nm `T.append` txt (show (num+1)))
1508 where
1509 readN x | not (T.null x) = read (T.unpack x)
1510 readN x = 0
1511nextName (SN x) = SN (nextName' x)
1512 where
1513 nextName' (WhereN i f x) = WhereN i f (nextName x)
1514 nextName' (WithN i n) = WithN i (nextName n)
1515 nextName' (ImplementationN n ns) = ImplementationN (nextName n) ns
1516 nextName' (ParentN n ns) = ParentN (nextName n) ns
1517 nextName' (CaseN fc n) = CaseN fc (nextName n)
1518 nextName' (MethodN n) = MethodN (nextName n)
1519 nextName' (ImplementationCtorN n) = ImplementationCtorN (nextName n)
1520 nextName' (MetaN parent meta) = MetaN parent (nextName meta)
1521nextName (SymRef i) = error "Can't generate a name from a symbol reference"
1523type Term = TT Name
1524type Type = Term
1526type Env = EnvTT Name
1528-- | an environment with de Bruijn indices 'normalised' so that they all refer to
1529-- this environment
1531newtype WkEnvTT n = Wk (EnvTT n)
1532type WkEnv = WkEnvTT Name
1534instance (Eq n, Show n) => Show (TT n) where
1535 show t = showEnv [] t
1537itBitsName IT8 = "Bits8"
1538itBitsName IT16 = "Bits16"
1539itBitsName IT32 = "Bits32"
1540itBitsName IT64 = "Bits64"
1542instance Show Const where
1543 show (I i) = show i
1544 show (BI i) = show i
1545 show (Fl f) = show f
1546 show (Ch c) = show c
1547 show (Str s) = show s
1548 show (B8 x) = show x
1549 show (B16 x) = show x
1550 show (B32 x) = show x
1551 show (B64 x) = show x
1552 show (AType ATFloat) = "Double"
1553 show (AType (ATInt ITBig)) = "Integer"
1554 show (AType (ATInt ITNative)) = "Int"
1555 show (AType (ATInt ITChar)) = "Char"
1556 show (AType (ATInt (ITFixed it))) = itBitsName it
1557 show TheWorld = "prim__TheWorld"
1558 show WorldType = "prim__WorldType"
1559 show StrType = "String"
1560 show VoidType = "Void"
1561 show Forgot = "Forgot"
1563showEnv :: (Eq n, Show n) => EnvTT n -> TT n -> String
1564showEnv env t = showEnv' env t False
1565showEnvDbg env t = showEnv' env t True
1567prettyEnv :: Env -> Term -> Doc OutputAnnotation
1568prettyEnv env t = prettyEnv' env t False
1569 where
1570 prettyEnv' env t dbg = prettySe 10 env t dbg
1572 bracket outer inner p
1573 | inner > outer = lparen <> p <> rparen
1574 | otherwise = p
1576 prettySe p env (P nt n t) debug =
1577 pretty n <+>
1578 if debug then
1579 lbracket <+> pretty nt <+> colon <+> prettySe 10 env t debug <+> rbracket
1580 else
1581 empty
1582 prettySe p env (V i) debug
1583 | i < length env =
1584 if debug then
1585 text . show . fstEnv $ env!!i
1586 else
1587 lbracket <+> text (show i) <+> rbracket
1588 | otherwise = text "unbound" <+> text (show i) <+> text "!"
1589 prettySe p env (Bind n b@(Pi _ _ t _) sc) debug
1590 | noOccurrence n sc && not debug =
1591 bracket p 2 $ prettySb env n b debug <> prettySe 10 ((n, Rig0, b):env) sc debug
1592 prettySe p env (Bind n b sc) debug =
1593 bracket p 2 $ prettySb env n b debug <> prettySe 10 ((n, Rig0, b):env) sc debug
1594 prettySe p env (App _ f a) debug =
1595 bracket p 1 $ prettySe 1 env f debug <+> prettySe 0 env a debug
1596 prettySe p env (Proj x i) debug =
1597 prettySe 1 env x debug <+> text ("!" ++ show i)
1598 prettySe p env (Constant c) debug = pretty c
1599 prettySe p env Erased debug = text "[_]"
1600 prettySe p env (TType i) debug = text "Type" <+> (text . show $ i)
1601 prettySe p env Impossible debug = text "Impossible"
1602 prettySe p env (Inferred tm) debug = text "<" <+> prettySe p env tm debug <+> text ">"
1603 prettySe p env (UType u) debug = text (show u)
1605 -- Render a `Binder` and its name
1606 prettySb env n (Lam _ t) = prettyB env "λ" "=>" n t
1607 prettySb env n (Hole t) = prettyB env "?defer" "." n t
1608 prettySb env n (GHole _ _ t) = prettyB env "?gdefer" "." n t
1609 prettySb env n (Pi Rig0 _ t _) = prettyB env "(" ") ->" n t
1610 prettySb env n (Pi Rig1 _ t _) = prettyB env "(" ") -o" n t
1611 prettySb env n (Pi RigW _ t _) = prettyB env "(" ") ->" n t
1612 prettySb env n (PVar Rig1 t) = prettyB env "pat 1 " "." n t
1613 prettySb env n (PVar _ t) = prettyB env "pat" "." n t
1614 prettySb env n (PVTy t) = prettyB env "pty" "." n t
1615 prettySb env n (Let Rig1 t v) = prettyBv env "let 1 " "in" n t v
1616 prettySb env n (Let _ t v) = prettyBv env "let" "in" n t v
1617 prettySb env n (NLet t v) = prettyBv env "nlet" "in" n t v
1618 prettySb env n (Guess t v) = prettyBv env "??" "in" n t v
1620 -- Use `op` and `sc` to delimit `n` (a binding name) and its type
1621 -- declaration
1622 -- e.g. "λx : Int =>" for the Lam case
1623 prettyB env op sc n t debug =
1624 text op <> pretty n <+> colon <+> prettySe 10 env t debug <> text sc
1626 -- Like `prettyB`, but handle the bindings that have values in addition
1627 -- to names and types
1628 prettyBv env op sc n t v debug =
1629 text op <> pretty n <+> colon <+> prettySe 10 env t debug <+> text "=" <+>
1630 prettySe 10 env v debug <> text sc
1633showEnv' env t dbg = se 10 env t where
1634 se p env (P nt n t) = show n
1635 ++ if dbg then "{" ++ show nt ++ " : " ++ se 10 env t ++ "}" else ""
1636 se p env (V i) | i < length env && i >= 0
1637 = (show $ fstEnv $ env!!i) ++
1638 if dbg then "{" ++ show i ++ "}" else ""
1639 | otherwise = "!!V " ++ show i ++ "!!"
1640 se p env (Bind n b@(Pi rig (Just _) t k) sc)
1641 = bracket p 2 $ sb env n b ++ se 10 ((n, rig, b):env) sc
1642 se p env (Bind n b@(Pi rig _ t k) sc)
1643 | noOccurrence n sc && not dbg = bracket p 2 $ se 1 env t ++ arrow rig ++ se 10 ((n,Rig0,b):env) sc
1644 where arrow Rig0 = " 0-> "
1645 arrow Rig1 = " -o "
1646 arrow RigW = " -> "
1647 se p env (Bind n b sc) = bracket p 2 $ sb env n b ++ se 10 ((n,Rig0,b):env) sc
1648 se p env (App _ f a) = bracket p 1 $ se 1 env f ++ " " ++ se 0 env a
1649 se p env (Proj x i) = se 1 env x ++ "!" ++ show i
1650 se p env (Constant c) = show c
1651 se p env Erased = "[__]"
1652 se p env Impossible = "[impossible]"
1653 se p env (Inferred t) = "<" ++ se p env t ++ ">"
1654 se p env (TType i) = "Type " ++ show i
1655 se p env (UType u) = show u
1657 sb env n (Lam Rig1 t) = showb env "\\ 1 " " => " n t
1658 sb env n (Lam _ t) = showb env "\\ " " => " n t
1659 sb env n (Hole t) = showb env "? " ". " n t
1660 sb env n (GHole i ns t) = showb env "?defer " ". " n t
1661 sb env n (Pi Rig1 (Just _) t _) = showb env "{" "} -o " n t
1662 sb env n (Pi _ (Just _) t _) = showb env "{" "} -> " n t
1663 sb env n (Pi Rig1 _ t _) = showb env "(" ") -0 " n t
1664 sb env n (Pi _ _ t _) = showb env "(" ") -> " n t
1665 sb env n (PVar Rig0 t) = showb env "pat 0 " ". " n t
1666 sb env n (PVar Rig1 t) = showb env "pat 1 " ". " n t
1667 sb env n (PVar _ t) = showb env "pat " ". " n t
1668 sb env n (PVTy t) = showb env "pty " ". " n t
1669 sb env n (Let Rig0 t v) = showbv env "let 0 " " in " n t v
1670 sb env n (Let Rig1 t v) = showbv env "let 1 " " in " n t v
1671 sb env n (Let _ t v) = showbv env "let " " in " n t v
1672 sb env n (NLet t v) = showbv env "nlet " " in " n t v
1673 sb env n (Guess t v) = showbv env "?? " " in " n t v
1675 showb env op sc n t = op ++ show n ++ " : " ++ se 10 env t ++ sc
1676 showbv env op sc n t v = op ++ show n ++ " : " ++ se 10 env t ++ " = " ++
1677 se 10 env v ++ sc
1679 bracket outer inner str | inner > outer = "(" ++ str ++ ")"
1680 | otherwise = str
1682-- | Check whether a term has any hole bindings in it - impure if so
1683pureTerm :: TT Name -> Bool
1684pureTerm (App _ f a) = pureTerm f && pureTerm a
1685pureTerm (Bind n b sc) = notInterfaceName n && pureBinder b && pureTerm sc where
1686 pureBinder (Hole _) = False
1687 pureBinder (Guess _ _) = False
1688 pureBinder (Let c t v) = pureTerm t && pureTerm v
1689 pureBinder t = pureTerm (binderTy t)
1691 notInterfaceName (MN _ c) | c == txt "__interface" = False
1692 notInterfaceName _ = True
1694pureTerm _ = True
1696-- | Weaken a term by adding i to each de Bruijn index (i.e. lift it over i bindings)
1697weakenTm :: Int -> TT n -> TT n
1698weakenTm i t = wk i 0 t
1699 where wk i min (V x) | x >= min = V (i + x)
1700 wk i m (App s f a) = App s (wk i m f) (wk i m a)
1701 wk i m (Bind x b sc) = Bind x (wkb i m b) (wk i (m + 1) sc)
1702 wk i m t = t
1703 wkb i m t = fmap (wk i m) t
1705-- | Weaken an environment so that all the de Bruijn indices are correct according
1706-- to the latest bound variable
1708weakenEnv :: EnvTT n -> EnvTT n
1709weakenEnv env = wk (length env - 1) env
1710 where wk i [] = []
1711 wk i ((n, c, b) : bs) = (n, c, weakenTmB i b) : wk (i - 1) bs
1712 weakenTmB i (Let c t v) = Let c (weakenTm i t) (weakenTm i v)
1713 weakenTmB i (Guess t v) = Guess (weakenTm i t) (weakenTm i v)
1714 weakenTmB i t = t { binderTy = weakenTm i (binderTy t) }
1716-- | Weaken every term in the environment by the given amount
1717weakenTmEnv :: Int -> EnvTT n -> EnvTT n
1718weakenTmEnv i = map (\ (n, c, b) -> (n, c, fmap (weakenTm i) b))
1720refsIn :: TT Name -> [Name]
1721refsIn (P _ n _) = [n]
1722refsIn (Bind n b t) = nub $ nb b ++ refsIn t
1723 where nb (Let _ t v) = nub (refsIn t) ++ nub (refsIn v)
1724 nb (Guess t v) = nub (refsIn t) ++ nub (refsIn v)
1725 nb t = refsIn (binderTy t)
1726refsIn (App s f a) = nub (refsIn f ++ refsIn a)
1727refsIn _ = []
1729allTTNames :: Eq n => TT n -> [n]
1730allTTNames = nub . allNamesIn
1731 where allNamesIn (P _ n _) = [n]
1732 allNamesIn (Bind n b t) = [n] ++ nb b ++ allNamesIn t
1733 where nb (Let _ t v) = allNamesIn t ++ allNamesIn v
1734 nb (Guess t v) = allNamesIn t ++ allNamesIn v
1735 nb t = allNamesIn (binderTy t)
1736 allNamesIn (App _ f a) = allNamesIn f ++ allNamesIn a
1737 allNamesIn _ = []
1740-- | Pretty-print a term
1741pprintTT :: [Name] -- ^ The bound names (for highlighting and de Bruijn indices)
1742 -> TT Name -- ^ The term to be printed
1743 -> Doc OutputAnnotation
1744pprintTT bound tm = pp startPrec bound tm
1746 where
1747 startPrec = 0
1748 appPrec = 10
1750 pp p bound (P Bound n ty) = annotate (AnnBoundName n False) (text $ show n)
1751 pp p bound (P nt n ty) = annotate (AnnName n Nothing Nothing Nothing)
1752 (text $ show n)
1753 pp p bound (V i)
1754 | i < length bound = let n = bound !! i
1755 in annotate (AnnBoundName n False) (text $ show n)
1756 | otherwise = text ("{{{V" ++ show i ++ "}}}")
1757 pp p bound (Bind n b sc) = ppb p bound n b $
1758 pp startPrec (n:bound) sc
1759 pp p bound (App _ tm1 tm2) =
1760 bracket p appPrec . group . hang 2 $
1761 pp appPrec bound tm1 <> line <>
1762 pp (appPrec + 1) bound tm2
1763 pp p bound (Constant c) = annotate (AnnConst c) (text (show c))
1764 pp p bound (Proj tm i) =
1765 lparen <> pp startPrec bound tm <> rparen <>
1766 text "!" <> text (show i)
1767 pp p bound Erased = text "<<<erased>>>"
1768 pp p bound Impossible = text "<<<impossible>>>"
1769 pp p bound (Inferred t) = text "<" <+> pp p bound t <+> text ">"
1770 pp p bound (TType ue) = annotate (AnnType "Type" "The type of types") $
1771 text "Type"
1772 pp p bound (UType u) = text (show u)
1774 ppb p bound n (Lam rig ty) sc =
1775 bracket p startPrec . group . align . hang 2 $
1776 text "λ" <+> bindingOf n False <+> text "." <> line <> sc
1777 ppb p bound n (Pi rig _ ty k) sc =
1778 bracket p startPrec . group . align $
1779 lparen <> (bindingOf n False) <+> colon <+>
1780 (group . align) (pp startPrec bound ty) <>
1781 rparen <+> mkArrow rig <> line <> sc
1782 where mkArrow Rig1 = text "⇴"
1783 mkArrow Rig0 = text "⥛"
1784 mkArrow _ = text "→"
1785 ppb p bound n (Let _ ty val) sc =
1786 bracket p startPrec . group . align $
1787 (group . hang 2) (annotate AnnKeyword (text "let") <+>
1788 bindingOf n False <+> colon <+>
1789 pp startPrec bound ty <+>
1790 text "=" <> line <>
1791 pp startPrec bound val) <> line <>
1792 (group . hang 2) (annotate AnnKeyword (text "in") <+> sc)
1793 ppb p bound n (NLet ty val) sc =
1794 bracket p startPrec . group . align $
1795 (group . hang 2) (annotate AnnKeyword (text "nlet") <+>
1796 bindingOf n False <+> colon <+>
1797 pp startPrec bound ty <+>
1798 text "=" <> line <>
1799 pp startPrec bound val) <> line <>
1800 (group . hang 2) (annotate AnnKeyword (text "in") <+> sc)
1801 ppb p bound n (Hole ty) sc =
1802 bracket p startPrec . group . align . hang 2 $
1803 text "?" <+> bindingOf n False <+> text "." <> line <> sc
1804 ppb p bound n (GHole _ _ ty) sc =
1805 bracket p startPrec . group . align . hang 2 $
1806 text "¿" <+> bindingOf n False <+> text "." <> line <> sc
1807 ppb p bound n (Guess ty val) sc =
1808 bracket p startPrec . group . align . hang 2 $
1809 text "?" <> bindingOf n False <+>
1810 text "≈" <+> pp startPrec bound val <+>
1811 text "." <> line <> sc
1812 ppb p bound n (PVar _ ty) sc =
1813 bracket p startPrec . group . align . hang 2 $
1814 annotate AnnKeyword (text "pat") <+>
1815 bindingOf n False <+> colon <+> pp startPrec bound ty <+>
1816 text "." <> line <>
1817 sc
1818 ppb p bound n (PVTy ty) sc =
1819 bracket p startPrec . group . align . hang 2 $
1820 annotate AnnKeyword (text "patTy") <+>
1821 bindingOf n False <+> colon <+> pp startPrec bound ty <+>
1822 text "." <> line <>
1823 sc
1825 bracket outer inner doc
1826 | outer > inner = lparen <> doc <> rparen
1827 | otherwise = doc
1829pprintTTClause :: [(Name, Type)] -> Term -> Term -> Doc OutputAnnotation
1830pprintTTClause pvars lhs rhs =
1831 vars pvars . group . align $
1832 pprintTT (map fst pvars) lhs <$>
1833 text "↦" <$>
1834 (pprintTT (map fst pvars) rhs)
1835 where vars [] terms = terms
1836 vars (v:vs) terms =
1837 annotate AnnKeyword (text "var") <+>
1838 group (align (sep (punctuate comma (reverse (bindVars [] (v:vs)))))) <+>
1839 annotate AnnKeyword (text ".") <$>
1840 indent 2 terms
1841 bindVars _ [] = []
1842 bindVars ns ((n, ty):vs) =
1843 bindingOf n False <+> colon <+> pprintTT ns ty : bindVars (n:ns) vs
1846-- | Pretty-print a raw term.
1847pprintRaw :: [Name] -- ^ Bound names, for highlighting
1848 -> Raw -- ^ The term to pretty-print
1849 -> Doc OutputAnnotation
1850pprintRaw bound (Var n) =
1851 enclose lparen rparen . group . align . hang 2 $
1852 (text "Var") <$> annotate (if n `elem` bound
1853 then AnnBoundName n False
1854 else AnnName n Nothing Nothing Nothing)
1855 (text $ show n)
1856pprintRaw bound (RBind n b body) =
1857 enclose lparen rparen . group . align . hang 2 $
1858 vsep [ text "RBind"
1859 , annotate (AnnBoundName n False) (text $ show n)
1860 , ppb b
1861 , pprintRaw (n:bound) body]
1862 where
1863 ppb (Lam _ ty) = enclose lparen rparen . group . align . hang 2 $
1864 text "Lam" <$> pprintRaw bound ty
1865 ppb (Pi _ _ ty k) = enclose lparen rparen . group . align . hang 2 $
1866 vsep [text "Pi", pprintRaw bound ty, pprintRaw bound k]
1867 ppb (Let c ty v) = enclose lparen rparen . group . align . hang 2 $
1868 vsep [text "Let", pprintRaw bound ty, pprintRaw bound v]
1869 ppb (NLet ty v) = enclose lparen rparen . group . align . hang 2 $
1870 vsep [text "NLet", pprintRaw bound ty, pprintRaw bound v]
1871 ppb (Hole ty) = enclose lparen rparen . group . align . hang 2 $
1872 text "Hole" <$> pprintRaw bound ty
1873 ppb (GHole _ _ ty) = enclose lparen rparen . group . align . hang 2 $
1874 text "GHole" <$> pprintRaw bound ty
1875 ppb (Guess ty v) = enclose lparen rparen . group . align . hang 2 $
1876 vsep [text "Guess", pprintRaw bound ty, pprintRaw bound v]
1877 ppb (PVar _ ty) = enclose lparen rparen . group . align . hang 2 $
1878 text "PVar" <$> pprintRaw bound ty
1879 ppb (PVTy ty) = enclose lparen rparen . group . align . hang 2 $
1880 text "PVTy" <$> pprintRaw bound ty
1881pprintRaw bound (RApp f x) =
1882 enclose lparen rparen . group . align . hang 2 . vsep $
1883 [text "RApp", pprintRaw bound f, pprintRaw bound x]
1884pprintRaw bound RType = text "RType"
1885pprintRaw bound (RUType u) = enclose lparen rparen . group . align . hang 2 $
1886 text "RUType" <$> text (show u)
1887pprintRaw bound (RConstant c) =
1888 enclose lparen rparen . group . align . hang 2 $
1889 vsep [text "RConstant", annotate (AnnConst c) (text (show c))]
1891-- | Pretty-printer helper for the binding site of a name
1892bindingOf :: Name -- ^^ the bound name
1893 -> Bool -- ^^ whether the name is implicit
1894 -> Doc OutputAnnotation
1895bindingOf n imp = annotate (AnnBoundName n imp) (text (show n))