git.iko.soy/Idris-dev
on 54e4e41 help sign in
Idris-dev/src/Idris/Core/TT.hs
1819 lines 71 kB history raw
1{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, DeriveFunctor,
2 DeriveDataTypeable, PatternGuards #-}
3{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
4{-| TT is the core language of Idris. The language has:
6 * Full dependent types
8 * A hierarchy of universes, with cumulativity: Type : Type1, Type1 : Type2, ...
10 * Pattern matching letrec binding
12 * (primitive types defined externally)
14 Some technical stuff:
16 * Typechecker is kept as simple as possible - no unification, just a checker for incomplete terms.
18 * We have a simple collection of tactics which we use to elaborate source
19 programs with implicit syntax into fully explicit terms.
20-}
22module Idris.Core.TT(AppStatus(..), ArithTy(..), Binder(..), Const(..), Ctxt(..),
23 ConstraintFC(..), DataOpt(..), DataOpts(..), Datatype(..),
24 Env(..), EnvTT(..), Err(..), Err'(..), ErrorReportPart(..),
25 FC(..), FC'(..), ImplicitInfo(..), IntTy(..), Name(..),
26 NameOutput(..), NameType(..), NativeTy(..), OutputAnnotation(..),
27 Provenance(..), Raw(..), SpecialName(..), TC(..), Term(..),
28 TermSize(..), TextFormatting(..), TT(..),Type(..), TypeInfo(..),
29 UConstraint(..), UCs(..), UExp(..), Universe(..),
30 addAlist, addBinder, addDef, allTTNames, arity, bindAll,
31 bindingOf, bindTyArgs, constDocs, constIsType, deleteDefExact,
32 discard, emptyContext, emptyFC, explicitNames, fc_end, fc_fname,
33 fc_start, fcIn, fileFC, finalise, fmapMB, forget, forgetEnv,
34 freeNames, getArgTys, getRetTy, implicitable, instantiate,
35 intTyName, isInjective, isTypeConst, liftPats, lookupCtxt,
36 lookupCtxtExact, lookupCtxtName, mapCtxt, mkApp, nativeTyWidth,
37 nextName, noOccurrence, nsroot, occurrences, orderPats,
38 pEraseType, pmap, pprintRaw, pprintTT, prettyEnv, psubst, pToV,
39 pToVs, pureTerm, raw_apply, raw_unapply, refsIn, safeForget,
40 safeForgetEnv, showCG, showEnv, showEnvDbg, showSep,
41 sInstanceN, sMN, sNS, spanFC, str, subst, substNames, substTerm,
42 substV, sUN, tcname, termSmallerThan, tfail, thead, tnull,
43 toAlist, traceWhen, txt, unApply, uniqueBinders, uniqueName,
44 uniqueNameFrom, uniqueNameSet, unList, updateDef, vToP, weakenTm) where
46-- Work around AMP without CPP
47import Prelude (Eq(..), Show(..), Ord(..), Functor(..), Monad(..), String, Int,
48 Integer, Ordering(..), Maybe(..), Num(..), Bool(..), Enum(..),
49 Read(..), FilePath, Double, (&&), (||), ($), (.), div, error, fst,
50 snd, not, mod, read, otherwise)
52import Control.Applicative (Applicative (..), Alternative)
53import qualified Control.Applicative as A (Alternative (..))
54import Control.Monad.State.Strict
55import Control.Monad.Trans.Except (Except (..))
56import Debug.Trace
57import qualified Data.Map.Strict as Map
58import Data.Char
59import Data.Data (Data)
60import Numeric (showIntAtBase)
61import qualified Data.Text as T
62import Data.List hiding (group, insert)
63import Data.Set(Set, member, fromList, insert)
64import Data.Maybe (listToMaybe)
65import Data.Foldable (Foldable)
66import Data.Traversable (Traversable)
67import Data.Typeable (Typeable)
68import Data.Vector.Unboxed (Vector)
69import qualified Data.Vector.Unboxed as V
70import qualified Data.Binary as B
71import Data.Binary hiding (get, put)
72import Foreign.Storable (sizeOf)
74import Util.Pretty hiding (Str)
76data Option = TTypeInTType
77 | CheckConv
78 deriving Eq
80-- | Source location. These are typically produced by the parser 'Idris.Parser.getFC'
81data FC = FC { _fc_fname :: String, -- ^ Filename
82 _fc_start :: (Int, Int), -- ^ Line and column numbers for the start of the location span
83 _fc_end :: (Int, Int) -- ^ Line and column numbers for the end of the location span
84 }
85 | NoFC -- ^ Locations for machine-generated terms
86 | FileFC { _fc_fname :: String } -- ^ Locations with file only
87 deriving (Data, Typeable, Ord)
89-- TODO: find uses and destroy them, doing this case analysis at call sites
90-- | Give a notion of filename associated with an FC
91fc_fname :: FC -> String
92fc_fname (FC f _ _) = f
93fc_fname NoFC = "(no file)"
94fc_fname (FileFC f) = f
96-- TODO: find uses and destroy them, doing this case analysis at call sites
97-- | Give a notion of start location associated with an FC
98fc_start :: FC -> (Int, Int)
99fc_start (FC _ start _) = start
100fc_start NoFC = (0, 0)
101fc_start (FileFC f) = (0, 0)
103-- TODO: find uses and destroy them, doing this case analysis at call sites
104-- | Give a notion of end location associated with an FC
105fc_end :: FC -> (Int, Int)
106fc_end (FC _ _ end) = end
107fc_end NoFC = (0, 0)
108fc_end (FileFC f) = (0, 0)
110-- | Get the largest span containing the two FCs
111spanFC :: FC -> FC -> FC
112spanFC (FC f start end) (FC f' start' end')
113 | f == f' = FC f (minLocation start start') (maxLocation end end')
114 | otherwise = NoFC
115 where minLocation (l, c) (l', c') =
116 case compare l l' of
117 LT -> (l, c)
118 EQ -> (l, min c c')
119 GT -> (l', c')
120 maxLocation (l, c) (l', c') =
121 case compare l l' of
122 LT -> (l', c')
123 EQ -> (l, max c c')
124 GT -> (l, c)
125spanFC fc@(FC f _ _) (FileFC f') | f == f' = fc
126 | otherwise = NoFC
127spanFC (FileFC f') fc@(FC f _ _) | f == f' = fc
128 | otherwise = NoFC
129spanFC (FileFC f) (FileFC f') | f == f' = FileFC f
130 | otherwise = NoFC
131spanFC NoFC fc = fc
132spanFC fc NoFC = fc
134-- | Determine whether the first argument is completely contained in the second
135fcIn :: FC -> FC -> Bool
136fcIn NoFC _ = False
137fcIn (FileFC _) _ = False
138fcIn (FC {}) NoFC = False
139fcIn (FC {}) (FileFC _) = False
140fcIn (FC fn1 (sl1, sc1) (el1, ec1)) (FC fn2 (sl2, sc2) (el2, ec2)) =
141 fn1 == fn2 &&
142 (sl1 == sl2 && sc1 > sc2 || sl1 > sl2) &&
143 (el1 == el2 && ec1 < ec2 || el1 < el2)
145-- | Ignore source location equality (so deriving classes do not compare FCs)
146instance Eq FC where
147 _ == _ = True
149-- | FC with equality
150newtype FC' = FC' { unwrapFC :: FC }
152instance Eq FC' where
153 FC' fc == FC' fc' = fcEq fc fc'
154 where fcEq (FC n s e) (FC n' s' e') = n == n' && s == s' && e == e'
155 fcEq NoFC NoFC = True
156 fcEq (FileFC f) (FileFC f') = f == f'
157 fcEq _ _ = False
159-- | Empty source location
160emptyFC :: FC
161emptyFC = NoFC
163-- | Source location with file only
164fileFC :: String -> FC
165fileFC s = FileFC s
167{-!
168deriving instance Binary FC
169deriving instance NFData FC
170!-}
172instance Sized FC where
173 size (FC f s e) = 4 + length f
174 size NoFC = 1
175 size (FileFC f) = length f
177instance Show FC where
178 show (FC f s e) = f ++ ":" ++ showLC s e
179 where showLC (sl, sc) (el, ec) | sl == el && sc == ec = show sl ++ ":" ++ show sc
180 | sl == el = show sl ++ ":" ++ show sc ++ "-" ++ show ec
181 | otherwise = show sl ++ ":" ++ show sc ++ "-" ++ show el ++ ":" ++ show ec
182 show NoFC = "No location"
183 show (FileFC f) = f
185-- | Output annotation for pretty-printed name - decides colour
186data NameOutput = TypeOutput | FunOutput | DataOutput | MetavarOutput | PostulateOutput deriving (Show, Eq)
188-- | Text formatting output
189data TextFormatting = BoldText | ItalicText | UnderlineText deriving (Show, Eq)
191-- | Output annotations for pretty-printing
192data OutputAnnotation = AnnName Name (Maybe NameOutput) (Maybe String) (Maybe String)
193 -- ^^ The name, classification, docs overview, and pretty-printed type
194 | AnnBoundName Name Bool
195 -- ^^ The name and whether it is implicit
196 | AnnConst Const
197 | AnnData String String -- ^ type, doc overview
198 | AnnType String String -- ^ name, doc overview
199 | AnnKeyword
200 | AnnFC FC
201 | AnnTextFmt TextFormatting
202 | AnnLink String -- ^ A link to this URL
203 | AnnTerm [(Name, Bool)] (TT Name) -- ^ pprint bound vars, original term
204 | AnnSearchResult Ordering -- ^ more general, isomorphic, or more specific
205 | AnnErr Err
206 | AnnNamespace [T.Text] (Maybe FilePath)
207 -- ^ A namespace (e.g. on an import line or in
208 -- a namespace declaration). Stored starting
209 -- at the root, with the hierarchy fully
210 -- resolved. If a file path is present, then
211 -- the namespace represents a module imported
212 -- from that file.
213 | AnnQuasiquote
214 | AnnAntiquote
215 deriving (Show, Eq)
217-- | Used for error reflection
218data ErrorReportPart = TextPart String
219 | NamePart Name
220 | TermPart Term
221 | RawPart Raw
222 | SubReport [ErrorReportPart]
223 deriving (Show, Eq, Data, Typeable)
226data Provenance = ExpectedType
227 | TooManyArgs Term
228 | InferredVal
229 | GivenVal
230 | SourceTerm Term
231 deriving (Show, Eq, Data, Typeable)
232{-!
233deriving instance NFData Err
234deriving instance Binary Err
235!-}
238-- NB: Please remember to keep Err synchronised with
239-- Language.Reflection.Errors.Err in the stdlib!
241-- | Idris errors. Used as exceptions in the compiler, but reported to users
242-- if they reach the top level.
243data Err' t
244 = Msg String
245 | InternalMsg String
246 | CantUnify Bool (t, Maybe Provenance) -- Expected type, provenance
247 (t, Maybe Provenance) -- Actual type, provenance
248 (Err' t) [(Name, t)] Int
249 -- Int is 'score' - how much we did unify
250 -- Bool indicates recoverability, True indicates more info may make
251 -- unification succeed
252 | InfiniteUnify Name t [(Name, t)]
253 | CantConvert t t [(Name, t)]
254 | CantSolveGoal t [(Name, t)]
255 | UnifyScope Name Name t [(Name, t)]
256 | CantInferType String
257 | NonFunctionType t t
258 | NotEquality t t
259 | TooManyArguments Name
260 | CantIntroduce t
261 | NoSuchVariable Name
262 | WithFnType t
263 | NoTypeDecl Name
264 | NotInjective t t t
265 | CantResolve Bool -- True if postponed, False if fatal
266 t
267 | InvalidTCArg Name t
268 | CantResolveAlts [Name]
269 | NoValidAlts [Name]
270 | IncompleteTerm t
271 | NoEliminator String t
272 | UniverseError FC UExp (Int, Int) (Int, Int) [ConstraintFC]
273 -- ^ Location, bad universe, old domain, new domain, suspects
274 | UniqueError Universe Name
275 | UniqueKindError Universe Name
276 | ProgramLineComment
277 | Inaccessible Name
278 | UnknownImplicit Name Name
279 | CantMatch t
280 | NonCollapsiblePostulate Name
281 | AlreadyDefined Name
282 | ProofSearchFail (Err' t)
283 | NoRewriting t
284 | At FC (Err' t)
285 | Elaborating String Name (Err' t)
286 | ElaboratingArg Name Name [(Name, Name)] (Err' t)
287 | ProviderError String
288 | LoadingFailed String (Err' t)
289 | ReflectionError [[ErrorReportPart]] (Err' t)
290 | ReflectionFailed String (Err' t)
291 | ElabScriptDebug [ErrorReportPart] t [(Name, t, [(Name, Binder t)])]
292 -- ^ User-specified message, proof term, goals with context (first goal is focused)
293 | ElabScriptStuck t
294 deriving (Eq, Functor, Data, Typeable)
296type Err = Err' Term
298data TC a = OK !a
299 | Error Err
300 deriving (Eq, Functor)
302bindTC :: TC a -> (a -> TC b) -> TC b
303bindTC x k = case x of
304 OK v -> k v
305 Error e -> Error e
306{-# INLINE bindTC #-}
308instance Monad TC where
309 return x = OK x
310 x >>= k = bindTC x k
311 fail e = Error (InternalMsg e)
313instance MonadPlus TC where
314 mzero = fail "Unknown error"
315 (OK x) `mplus` _ = OK x
316 _ `mplus` (OK y) = OK y
317 err `mplus` _ = err
320instance Applicative TC where
321 pure = return
322 (<*>) = ap
324instance Alternative TC where
325 empty = mzero
326 (<|>) = mplus
328{-!
329deriving instance NFData Err
330!-}
332instance Sized ErrorReportPart where
333 size (TextPart msg) = 1 + length msg
334 size (TermPart t) = 1 + size t
335 size (RawPart r) = 1 + size r
336 size (NamePart n) = 1 + size n
337 size (SubReport rs) = 1 + size rs
339instance Sized Err where
340 size (Msg msg) = length msg
341 size (InternalMsg msg) = length msg
342 size (CantUnify _ left right err _ score) = size (fst left) + size (fst right) + size err
343 size (InfiniteUnify _ right _) = size right
344 size (CantConvert left right _) = size left + size right
345 size (UnifyScope _ _ right _) = size right
346 size (NoSuchVariable name) = size name
347 size (NoTypeDecl name) = size name
348 size (NotInjective l c r) = size l + size c + size r
349 size (CantResolve _ trm) = size trm
350 size (NoRewriting trm) = size trm
351 size (CantResolveAlts _) = 1
352 size (IncompleteTerm trm) = size trm
353 size ProgramLineComment = 1
354 size (At fc err) = size fc + size err
355 size (Elaborating _ n err) = size err
356 size (ElaboratingArg _ _ _ err) = size err
357 size (ProviderError msg) = length msg
358 size (LoadingFailed fn e) = 1 + length fn + size e
359 size _ = 1
361instance Show Err where
362 show (Msg s) = s
363 show (InternalMsg s) = "Internal error: " ++ show s
364 show (CantUnify rcv l r e sc i) = "CantUnify " ++ show rcv ++ " " ++
365 show l ++ " " ++ show r ++ " " ++
366 show e ++ " in " ++ show sc ++ " " ++ show i
367 show (CantSolveGoal g _) = "CantSolve " ++ show g
368 show (Inaccessible n) = show n ++ " is not an accessible pattern variable"
369 show (UnknownImplicit n f) = show n ++ " is not an implicit argument of " ++ show f
370 show (ProviderError msg) = "Type provider error: " ++ msg
371 show (LoadingFailed fn e) = "Loading " ++ fn ++ " failed: (TT) " ++ show e
372 show ProgramLineComment = "Program line next to comment"
373 show (At f e) = show f ++ ":" ++ show e
374 show (ElaboratingArg f x prev e) = "Elaborating " ++ show f ++ " arg " ++
375 show x ++ ": " ++ show e
376 show (Elaborating what n e) = "Elaborating " ++ what ++ show n ++ ":" ++ show e
377 show (ProofSearchFail e) = "Proof search fail: " ++ show e
378 show _ = "Error"
380instance Pretty Err OutputAnnotation where
381 pretty (Msg m) = text m
382 pretty (CantUnify _ (l, _) (r, _) e _ i) =
383 text "Cannot unify" <+> colon <+> pretty l <+> text "and" <+> pretty r <+>
384 nest nestingSize (text "where" <+> pretty e <+> text "with" <+> (text . show $ i))
385 pretty (ProviderError msg) = text msg
386 pretty err@(LoadingFailed _ _) = text (show err)
387 pretty _ = text "Error"
389instance (Pretty a OutputAnnotation) => Pretty (TC a) OutputAnnotation where
390 pretty (OK ok) = pretty ok
391 pretty (Error err) =
392 text "Error" <+> colon <+> pretty err
394instance Show a => Show (TC a) where
395 show (OK x) = show x
396 show (Error str) = "Error: " ++ show str
398tfail :: Err -> TC a
399tfail e = Error e
401failMsg :: String -> TC a
402failMsg str = Error (Msg str)
404trun :: FC -> TC a -> TC a
405trun fc (OK a) = OK a
406trun fc (Error e) = Error (At fc e)
408discard :: Monad m => m a -> m ()
409discard f = f >> return ()
411showSep :: String -> [String] -> String
412showSep sep [] = ""
413showSep sep [x] = x
414showSep sep (x:xs) = x ++ sep ++ showSep sep xs
416pmap f (x, y) = (f x, f y)
418traceWhen True msg a = trace msg a
419traceWhen False _ a = a
421-- RAW TERMS ----------------------------------------------------------------
423-- | Names are hierarchies of strings, describing scope (so no danger of
424-- duplicate names, but need to be careful on lookup).
425data Name = UN T.Text -- ^ User-provided name
426 | NS Name [T.Text] -- ^ Root, namespaces
427 | MN Int T.Text -- ^ Machine chosen names
428 | NErased -- ^ Name of something which is never used in scope
429 | SN SpecialName -- ^ Decorated function names
430 | SymRef Int -- ^ Reference to IBC file symbol table (used during serialisation)
431 deriving (Eq, Ord, Data, Typeable)
433txt :: String -> T.Text
434txt = T.pack
436str :: T.Text -> String
437str = T.unpack
439tnull :: T.Text -> Bool
440tnull = T.null
442thead :: T.Text -> Char
443thead = T.head
445-- Smart constructors for names, using old String style
446sUN :: String -> Name
447sUN s = UN (txt s)
449sNS :: Name -> [String] -> Name
450sNS n ss = NS n (map txt ss)
452sMN :: Int -> String -> Name
453sMN i s = MN i (txt s)
455{-!
456deriving instance Binary Name
457deriving instance NFData Name
458!-}
460data SpecialName = WhereN Int Name Name
461 | WithN Int Name
462 | InstanceN Name [T.Text]
463 | ParentN Name T.Text
464 | MethodN Name
465 | CaseN Name
466 | ElimN Name
467 | InstanceCtorN Name
468 | MetaN Name Name
469 deriving (Eq, Ord, Data, Typeable)
470{-!
471deriving instance Binary SpecialName
472deriving instance NFData SpecialName
473!-}
475sInstanceN :: Name -> [String] -> SpecialName
476sInstanceN n ss = InstanceN n (map T.pack ss)
478sParentN :: Name -> String -> SpecialName
479sParentN n s = ParentN n (T.pack s)
481instance Sized Name where
482 size (UN n) = 1
483 size (NS n els) = 1 + length els
484 size (MN i n) = 1
485 size _ = 1
487instance Pretty Name OutputAnnotation where
488 pretty n@(UN n') = annotate (AnnName n Nothing Nothing Nothing) $ text (T.unpack n')
489 pretty n@(NS un s) = annotate (AnnName n Nothing Nothing Nothing) . noAnnotate $ pretty un
490 pretty n@(MN i s) = annotate (AnnName n Nothing Nothing Nothing) $
491 lbrace <+> text (T.unpack s) <+> (text . show $ i) <+> rbrace
492 pretty n@(SN s) = annotate (AnnName n Nothing Nothing Nothing) $ text (show s)
493 pretty n@(SymRef i) = annotate (AnnName n Nothing Nothing Nothing) $
494 text $ "##symbol" ++ show i ++ "##"
495 pretty NErased = annotate (AnnName NErased Nothing Nothing Nothing) $ text "_"
497instance Pretty [Name] OutputAnnotation where
498 pretty = encloseSep empty empty comma . map pretty
500instance Show Name where
501 show (UN n) = str n
502 show (NS n s) = showSep "." (map T.unpack (reverse s)) ++ "." ++ show n
503 show (MN _ u) | u == txt "underscore" = "_"
504 show (MN i s) = "{" ++ str s ++ show i ++ "}"
505 show (SN s) = show s
506 show (SymRef i) = "##symbol" ++ show i ++ "##"
507 show NErased = "_"
509instance Show SpecialName where
510 show (WhereN i p c) = show p ++ ", " ++ show c
511 show (WithN i n) = "with block in " ++ show n
512 show (InstanceN cl inst) = showSep ", " (map T.unpack inst) ++ " instance of " ++ show cl
513 show (MethodN m) = "method " ++ show m
514 show (ParentN p c) = show p ++ "#" ++ T.unpack c
515 show (CaseN n) = "case block in " ++ show n
516 show (ElimN n) = "<<" ++ show n ++ " eliminator>>"
517 show (InstanceCtorN n) = "constructor of " ++ show n
518 show (MetaN parent meta) = "<<" ++ show parent ++ " " ++ show meta ++ ">>"
520-- Show a name in a way decorated for code generation, not human reading
521showCG :: Name -> String
522showCG (UN n) = T.unpack n
523showCG (NS n s) = showSep "." (map T.unpack (reverse s)) ++ "." ++ showCG n
524showCG (MN _ u) | u == txt "underscore" = "_"
525showCG (MN i s) = "{" ++ T.unpack s ++ show i ++ "}"
526showCG (SN s) = showCG' s
527 where showCG' (WhereN i p c) = showCG p ++ ":" ++ showCG c ++ ":" ++ show i
528 showCG' (WithN i n) = "_" ++ showCG n ++ "_with_" ++ show i
529 showCG' (InstanceN cl inst) = '@':showCG cl ++ '$':showSep ":" (map T.unpack inst)
530 showCG' (MethodN m) = '!':showCG m
531 showCG' (ParentN p c) = showCG p ++ "#" ++ show c
532 showCG' (CaseN c) = showCG c ++ "_case"
533 showCG' (ElimN sn) = showCG sn ++ "_elim"
534 showCG' (InstanceCtorN n) = showCG n ++ "_ictor"
535 showCG' (MetaN parent meta) = showCG parent ++ "_meta_" ++ showCG meta
536showCG (SymRef i) = error "can't do codegen for a symbol reference"
537showCG NErased = "_"
540-- |Contexts allow us to map names to things. A root name maps to a collection
541-- of things in different namespaces with that name.
542type Ctxt a = Map.Map Name (Map.Map Name a)
543emptyContext = Map.empty
545mapCtxt :: (a -> b) -> Ctxt a -> Ctxt b
546mapCtxt = fmap . fmap
548-- |Return True if the argument 'Name' should be interpreted as the name of a
549-- typeclass.
550tcname (UN xs) | T.null xs = False
551 | otherwise = T.head xs == '@'
552tcname (NS n _) = tcname n
553tcname (SN (InstanceN _ _)) = True
554tcname (SN (MethodN _)) = True
555tcname (SN (ParentN _ _)) = True
556tcname _ = False
558implicitable (NS n _) = implicitable n
559implicitable (UN xs) | T.null xs = False
560 | otherwise = isLower (T.head xs) || T.head xs == '_'
561implicitable (MN _ x) = not (tnull x) && thead x /= '_'
562implicitable _ = False
564nsroot (NS n _) = n
565nsroot n = n
567-- this will overwrite already existing definitions
568addDef :: Name -> a -> Ctxt a -> Ctxt a
569addDef n v ctxt = case Map.lookup (nsroot n) ctxt of
570 Nothing -> Map.insert (nsroot n)
571 (Map.insert n v Map.empty) ctxt
572 Just xs -> Map.insert (nsroot n)
573 (Map.insert n v xs) ctxt
575{-| Look up a name in the context, given an optional namespace.
576 The name (n) may itself have a (partial) namespace given.
578 Rules for resolution:
580 - if an explicit namespace is given, return the names which match it. If none
581 match, return all names.
583 - if the name has has explicit namespace given, return the names which match it
584 and ignore the given namespace.
586 - otherwise, return all names.
588-}
590lookupCtxtName :: Name -> Ctxt a -> [(Name, a)]
591lookupCtxtName n ctxt = case Map.lookup (nsroot n) ctxt of
592 Just xs -> filterNS (Map.toList xs)
593 Nothing -> []
594 where
595 filterNS [] = []
596 filterNS ((found, v) : xs)
597 | nsmatch n found = (found, v) : filterNS xs
598 | otherwise = filterNS xs
600 nsmatch (NS n ns) (NS p ps) = ns `isPrefixOf` ps
601 nsmatch (NS _ _) _ = False
602 nsmatch looking found = True
604lookupCtxt :: Name -> Ctxt a -> [a]
605lookupCtxt n ctxt = map snd (lookupCtxtName n ctxt)
607lookupCtxtExact :: Name -> Ctxt a -> Maybe a
608lookupCtxtExact n ctxt = listToMaybe [ v | (nm, v) <- lookupCtxtName n ctxt, nm == n]
610deleteDefExact :: Name -> Ctxt a -> Ctxt a
611deleteDefExact n = Map.adjust (Map.delete n) (nsroot n)
613updateDef :: Name -> (a -> a) -> Ctxt a -> Ctxt a
614updateDef n f ctxt
615 = let ds = lookupCtxtName n ctxt in
616 foldr (\ (n, t) c -> addDef n (f t) c) ctxt ds
618toAlist :: Ctxt a -> [(Name, a)]
619toAlist ctxt = let allns = map snd (Map.toList ctxt) in
620 concatMap (Map.toList) allns
622addAlist :: [(Name, a)] -> Ctxt a -> Ctxt a
623addAlist [] ctxt = ctxt
624addAlist ((n, tm) : ds) ctxt = addDef n tm (addAlist ds ctxt)
626data NativeTy = IT8 | IT16 | IT32 | IT64
627 deriving (Show, Eq, Ord, Enum, Data, Typeable)
629instance Pretty NativeTy OutputAnnotation where
630 pretty IT8 = text "Bits8"
631 pretty IT16 = text "Bits16"
632 pretty IT32 = text "Bits32"
633 pretty IT64 = text "Bits64"
635data IntTy = ITFixed NativeTy | ITNative | ITBig | ITChar
636 deriving (Show, Eq, Ord, Data, Typeable)
638intTyName :: IntTy -> String
639intTyName ITNative = "Int"
640intTyName ITBig = "BigInt"
641intTyName (ITFixed sized) = "B" ++ show (nativeTyWidth sized)
642intTyName (ITChar) = "Char"
644data ArithTy = ATInt IntTy | ATFloat -- TODO: Float vectors https://github.com/idris-lang/Idris-dev/issues/1723
645 deriving (Show, Eq, Ord, Data, Typeable)
646{-!
647deriving instance NFData IntTy
648deriving instance NFData NativeTy
649deriving instance NFData ArithTy
650!-}
652instance Pretty ArithTy OutputAnnotation where
653 pretty (ATInt ITNative) = text "Int"
654 pretty (ATInt ITBig) = text "BigInt"
655 pretty (ATInt ITChar) = text "Char"
656 pretty (ATInt (ITFixed n)) = pretty n
657 pretty ATFloat = text "Float"
659nativeTyWidth :: NativeTy -> Int
660nativeTyWidth IT8 = 8
661nativeTyWidth IT16 = 16
662nativeTyWidth IT32 = 32
663nativeTyWidth IT64 = 64
665{-# DEPRECATED intTyWidth "Non-total function, use nativeTyWidth and appropriate casing" #-}
666intTyWidth :: IntTy -> Int
667intTyWidth (ITFixed n) = nativeTyWidth n
668intTyWidth ITNative = 8 * sizeOf (0 :: Int)
669intTyWidth ITChar = error "IRTS.Lang.intTyWidth: Characters have platform and backend dependent width"
670intTyWidth ITBig = error "IRTS.Lang.intTyWidth: Big integers have variable width"
672data Const = I Int | BI Integer | Fl Double | Ch Char | Str String
673 | B8 Word8 | B16 Word16 | B32 Word32 | B64 Word64
674 | AType ArithTy | StrType
675 | WorldType | TheWorld
676 | VoidType | Forgot
677 deriving (Eq, Ord, Data, Typeable)
678{-!
679deriving instance Binary Const
680deriving instance NFData Const
681!-}
683isTypeConst :: Const -> Bool
684isTypeConst (AType _) = True
685isTypeConst StrType = True
686isTypeConst WorldType = True
687isTypeConst VoidType = True
688isTypeConst _ = False
690instance Sized Const where
691 size _ = 1
693instance Pretty Const OutputAnnotation where
694 pretty (I i) = text . show $ i
695 pretty (BI i) = text . show $ i
696 pretty (Fl f) = text . show $ f
697 pretty (Ch c) = text . show $ c
698 pretty (Str s) = text s
699 pretty (AType a) = pretty a
700 pretty StrType = text "String"
701 pretty TheWorld = text "%theWorld"
702 pretty WorldType = text "prim__World"
703 pretty VoidType = text "Void"
704 pretty Forgot = text "Forgot"
705 pretty (B8 w) = text . show $ w
706 pretty (B16 w) = text . show $ w
707 pretty (B32 w) = text . show $ w
708 pretty (B64 w) = text . show $ w
710-- | Determines whether the input constant represents a type
711constIsType :: Const -> Bool
712constIsType (I _) = False
713constIsType (BI _) = False
714constIsType (Fl _) = False
715constIsType (Ch _) = False
716constIsType (Str _) = False
717constIsType (B8 _) = False
718constIsType (B16 _) = False
719constIsType (B32 _) = False
720constIsType (B64 _) = False
721constIsType _ = True
723-- | Get the docstring for a Const
724constDocs :: Const -> String
725constDocs c@(AType (ATInt ITBig)) = "Arbitrary-precision integers"
726constDocs c@(AType (ATInt ITNative)) = "Fixed-precision integers of undefined size"
727constDocs c@(AType (ATInt ITChar)) = "Characters in some unspecified encoding"
728constDocs c@(AType ATFloat) = "Double-precision floating-point numbers"
729constDocs StrType = "Strings in some unspecified encoding"
730constDocs c@(AType (ATInt (ITFixed IT8))) = "Eight bits (unsigned)"
731constDocs c@(AType (ATInt (ITFixed IT16))) = "Sixteen bits (unsigned)"
732constDocs c@(AType (ATInt (ITFixed IT32))) = "Thirty-two bits (unsigned)"
733constDocs c@(AType (ATInt (ITFixed IT64))) = "Sixty-four bits (unsigned)"
734constDocs (Fl f) = "A float"
735constDocs (I i) = "A fixed-precision integer"
736constDocs (BI i) = "An arbitrary-precision integer"
737constDocs (Str s) = "A string of length " ++ show (length s)
738constDocs (Ch c) = "A character"
739constDocs (B8 w) = "The eight-bit value 0x" ++
740 showIntAtBase 16 intToDigit w ""
741constDocs (B16 w) = "The sixteen-bit value 0x" ++
742 showIntAtBase 16 intToDigit w ""
743constDocs (B32 w) = "The thirty-two-bit value 0x" ++
744 showIntAtBase 16 intToDigit w ""
745constDocs (B64 w) = "The sixty-four-bit value 0x" ++
746 showIntAtBase 16 intToDigit w ""
747constDocs prim = "Undocumented"
749data Universe = NullType | UniqueType | AllTypes
750 deriving (Eq, Ord, Data, Typeable)
752instance Show Universe where
753 show UniqueType = "UniqueType"
754 show NullType = "NullType"
755 show AllTypes = "AnyType"
757data Raw = Var Name
758 | RBind Name (Binder Raw) Raw
759 | RApp Raw Raw
760 | RType
761 | RUType Universe
762 | RForce Raw
763 | RConstant Const
764 deriving (Show, Eq, Data, Typeable)
766instance Sized Raw where
767 size (Var name) = 1
768 size (RBind name bind right) = 1 + size bind + size right
769 size (RApp left right) = 1 + size left + size right
770 size RType = 1
771 size (RUType _) = 1
772 size (RForce raw) = 1 + size raw
773 size (RConstant const) = size const
775instance Pretty Raw OutputAnnotation where
776 pretty = text . show
778{-!
779deriving instance Binary Raw
780deriving instance NFData Raw
781!-}
783data ImplicitInfo = Impl { tcinstance :: Bool }
784 deriving (Show, Eq, Ord, Data, Typeable)
786{-!
787deriving instance Binary ImplicitInfo
788deriving instance NFData ImplicitInfo
789!-}
791-- The type parameter `b` will normally be something like `TT Name` or just
792-- `Raw`. We do not make a type-level distinction between TT terms that happen
793-- to be TT types and TT terms that are not TT types.
794-- | All binding forms are represented in a uniform fashion. This type only represents
795-- the types of bindings (and their values, if any); the attached identifiers are part
796-- of the 'Bind' constructor for the 'TT' type.
797data Binder b = Lam { binderTy :: !b {-^ type annotation for bound variable-}}
798 | Pi { binderImpl :: Maybe ImplicitInfo,
799 binderTy :: !b,
800 binderKind :: !b }
801 {-^ A binding that occurs in a function type expression, e.g. @(x:Int) -> ...@
802 The 'binderImpl' flag says whether it was a scoped implicit
803 (i.e. forall bound) in the high level Idris, but otherwise
804 has no relevance in TT. -}
805 | Let { binderTy :: !b,
806 binderVal :: b {-^ value for bound variable-}}
807 -- ^ A binding that occurs in a @let@ expression
808 | NLet { binderTy :: !b,
809 binderVal :: b }
810 | Hole { binderTy :: !b}
811 | GHole { envlen :: Int,
812 binderTy :: !b}
813 | Guess { binderTy :: !b,
814 binderVal :: b }
815 | PVar { binderTy :: !b }
816 -- ^ A pattern variable
817 | PVTy { binderTy :: !b }
818 deriving (Show, Eq, Ord, Functor, Foldable, Traversable, Data, Typeable)
819{-!
820deriving instance Binary Binder
821deriving instance NFData Binder
822!-}
824instance Sized a => Sized (Binder a) where
825 size (Lam ty) = 1 + size ty
826 size (Pi _ ty _) = 1 + size ty
827 size (Let ty val) = 1 + size ty + size val
828 size (NLet ty val) = 1 + size ty + size val
829 size (Hole ty) = 1 + size ty
830 size (GHole _ ty) = 1 + size ty
831 size (Guess ty val) = 1 + size ty + size val
832 size (PVar ty) = 1 + size ty
833 size (PVTy ty) = 1 + size ty
835fmapMB :: Monad m => (a -> m b) -> Binder a -> m (Binder b)
836fmapMB f (Let t v) = liftM2 Let (f t) (f v)
837fmapMB f (NLet t v) = liftM2 NLet (f t) (f v)
838fmapMB f (Guess t v) = liftM2 Guess (f t) (f v)
839fmapMB f (Lam t) = liftM Lam (f t)
840fmapMB f (Pi i t k) = liftM2 (Pi i) (f t) (f k)
841fmapMB f (Hole t) = liftM Hole (f t)
842fmapMB f (GHole i t) = liftM (GHole i) (f t)
843fmapMB f (PVar t) = liftM PVar (f t)
844fmapMB f (PVTy t) = liftM PVTy (f t)
846raw_apply :: Raw -> [Raw] -> Raw
847raw_apply f [] = f
848raw_apply f (a : as) = raw_apply (RApp f a) as
850raw_unapply :: Raw -> (Raw, [Raw])
851raw_unapply t = ua [] t where
852 ua args (RApp f a) = ua (a:args) f
853 ua args t = (t, args)
855-- WELL TYPED TERMS ---------------------------------------------------------
857-- | Universe expressions for universe checking
858data UExp = UVar Int -- ^ universe variable
859 | UVal Int -- ^ explicit universe level
860 deriving (Eq, Ord, Data, Typeable)
861{-!
862deriving instance NFData UExp
863!-}
865instance Sized UExp where
866 size _ = 1
868instance Show UExp where
869 show (UVar x) | x < 26 = [toEnum (x + fromEnum 'a')]
870 | otherwise = toEnum ((x `mod` 26) + fromEnum 'a') : show (x `div` 26)
871 show (UVal x) = show x
872-- show (UMax l r) = "max(" ++ show l ++ ", " ++ show r ++")"
874-- | Universe constraints
875data UConstraint = ULT UExp UExp -- ^ Strictly less than
876 | ULE UExp UExp -- ^ Less than or equal to
877 deriving (Eq, Ord, Data, Typeable)
879data ConstraintFC = ConstraintFC { uconstraint :: UConstraint,
880 ufc :: FC }
881 deriving (Show, Data, Typeable)
883instance Eq ConstraintFC where
884 x == y = uconstraint x == uconstraint y
886instance Ord ConstraintFC where
887 compare x y = compare (uconstraint x) (uconstraint y)
889instance Show UConstraint where
890 show (ULT x y) = show x ++ " < " ++ show y
891 show (ULE x y) = show x ++ " <= " ++ show y
893type UCs = (Int, [UConstraint])
895data NameType = Bound
896 | Ref
897 | DCon {nt_tag :: Int, nt_arity :: Int, nt_unique :: Bool} -- ^ Data constructor
898 | TCon {nt_tag :: Int, nt_arity :: Int} -- ^ Type constructor
899 deriving (Show, Ord, Data, Typeable)
900{-!
901deriving instance Binary NameType
902deriving instance NFData NameType
903!-}
905instance Sized NameType where
906 size _ = 1
908instance Pretty NameType OutputAnnotation where
909 pretty = text . show
911instance Eq NameType where
912 Bound == Bound = True
913 Ref == Ref = True
914 DCon _ a _ == DCon _ b _ = (a == b) -- ignore tag
915 TCon _ a == TCon _ b = (a == b) -- ignore tag
916 _ == _ = False
918data AppStatus n = Complete
919 | MaybeHoles
920 | Holes [n]
921 deriving (Eq, Ord, Functor, Data, Typeable, Show)
923-- | Terms in the core language. The type parameter is the type of
924-- identifiers used for bindings and explicit named references;
925-- usually we use @TT 'Name'@.
926data TT n = P NameType n (TT n) -- ^ named references with type
927 -- (P for "Parameter", motivated by McKinna and Pollack's
928 -- Pure Type Systems Formalized)
929 | V !Int -- ^ a resolved de Bruijn-indexed variable
930 | Bind n !(Binder (TT n)) (TT n) -- ^ a binding
931 | App (AppStatus n) !(TT n) (TT n) -- ^ function, function type, arg
932 | Constant Const -- ^ constant
933 | Proj (TT n) !Int -- ^ argument projection; runtime only
934 -- (-1) is a special case for 'subtract one from BI'
935 | Erased -- ^ an erased term
936 | Impossible -- ^ special case for totality checking
937 | TType UExp -- ^ the type of types at some level
938 | UType Universe -- ^ Uniqueness type universe (disjoint from TType)
939 deriving (Ord, Functor, Data, Typeable)
940{-!
941deriving instance Binary TT
942deriving instance NFData TT
943!-}
945class TermSize a where
946 termsize :: Name -> a -> Int
948instance TermSize a => TermSize [a] where
949 termsize n [] = 0
950 termsize n (x : xs) = termsize n x + termsize n xs
952instance TermSize (TT Name) where
953 termsize n (P _ n' _)
954 | n' == n = 1000000 -- recursive => really big
955 | otherwise = 1
956 termsize n (V _) = 1
957 -- for `Bind` terms, we can erroneously declare a term
958 -- "recursive => really big" if the name of the bound
959 -- variable is the same as the name we're using
960 -- So generate a different name in that case.
961 termsize n (Bind n' (Let t v) sc)
962 = let rn = if n == n' then sMN 0 "noname" else n in
963 termsize rn v + termsize rn sc
964 termsize n (Bind n' b sc)
965 = let rn = if n == n' then sMN 0 "noname" else n in
966 termsize rn sc
967 termsize n (App _ f a) = termsize n f + termsize n a
968 termsize n (Proj t i) = termsize n t
969 termsize n _ = 1
971instance Sized Universe where
972 size u = 1
974instance Sized a => Sized (TT a) where
975 size (P name n trm) = 1 + size name + size n + size trm
976 size (V v) = 1
977 size (Bind nm binder bdy) = 1 + size nm + size binder + size bdy
978 size (App _ l r) = 1 + size l + size r
979 size (Constant c) = size c
980 size Erased = 1
981 size (TType u) = 1 + size u
982 size (Proj a _) = 1 + size a
983 size Impossible = 1
984 size (UType u) = 1 + size u
986instance Pretty a o => Pretty (TT a) o where
987 pretty _ = text "test"
989type EnvTT n = [(n, Binder (TT n))]
991data Datatype n = Data { d_typename :: n,
992 d_typetag :: Int,
993 d_type :: (TT n),
994 d_unique :: Bool,
995 d_cons :: [(n, TT n)] }
996 deriving (Show, Functor, Eq)
998-- | Data declaration options
999data DataOpt = Codata -- ^ Set if the the data-type is coinductive
1000 | DefaultEliminator -- ^ Set if an eliminator should be generated for data type
1001 | DefaultCaseFun -- ^ Set if a case function should be generated for data type
1002 | DataErrRev
1003 deriving (Show, Eq)
1005type DataOpts = [DataOpt]
1007data TypeInfo = TI { con_names :: [Name],
1008 codata :: Bool,
1009 data_opts :: DataOpts,
1010 param_pos :: [Int],
1011 mutual_types :: [Name] }
1012 deriving Show
1013{-!
1014deriving instance Binary TypeInfo
1015deriving instance NFData TypeInfo
1016!-}
1018instance Eq n => Eq (TT n) where
1019 (==) (P xt x _) (P yt y _) = x == y
1020 (==) (V x) (V y) = x == y
1021 (==) (Bind _ xb xs) (Bind _ yb ys) = xs == ys && xb == yb
1022 (==) (App _ fx ax) (App _ fy ay) = ax == ay && fx == fy
1023 (==) (TType _) (TType _) = True -- deal with constraints later
1024 (==) (Constant x) (Constant y) = x == y
1025 (==) (Proj x i) (Proj y j) = x == y && i == j
1026 (==) Erased _ = True
1027 (==) _ Erased = True
1028 (==) _ _ = False
1030-- * A few handy operations on well typed terms:
1032-- | A term is injective iff it is a data constructor, type constructor,
1033-- constant, the type Type, pi-binding, or an application of an injective
1034-- term.
1035isInjective :: TT n -> Bool
1036isInjective (P (DCon _ _ _) _ _) = True
1037isInjective (P (TCon _ _) _ _) = True
1038isInjective (Constant _) = True
1039isInjective (TType x) = True
1040isInjective (Bind _ (Pi _ _ _) sc) = True
1041isInjective (App _ f a) = isInjective f
1042isInjective _ = False
1044-- | Count the number of instances of a de Bruijn index in a term
1045vinstances :: Int -> TT n -> Int
1046vinstances i (V x) | i == x = 1
1047vinstances i (App _ f a) = vinstances i f + vinstances i a
1048vinstances i (Bind x b sc) = instancesB b + vinstances (i + 1) sc
1049 where instancesB (Let t v) = vinstances i v
1050 instancesB _ = 0
1051vinstances i t = 0
1053-- | Replace the outermost (index 0) de Bruijn variable with the given term
1054instantiate :: TT n -> TT n -> TT n
1055instantiate e = subst 0 where
1056 subst i (P nt x ty) = P nt x (subst i ty)
1057 subst i (V x) | i == x = e
1058 subst i (Bind x b sc) = Bind x (fmap (subst i) b) (subst (i+1) sc)
1059 subst i (App s f a) = App s (subst i f) (subst i a)
1060 subst i (Proj x idx) = Proj (subst i x) idx
1061 subst i t = t
1063-- | As 'instantiate', but also decrement the indices of all de Bruijn variables
1064-- remaining in the term, so that there are no more references to the variable
1065-- that has been substituted.
1066substV :: TT n -> TT n -> TT n
1067substV x tm = dropV 0 (instantiate x tm) where
1068 dropV i (P nt x ty) = P nt x (dropV i ty)
1069 dropV i (V x) | x > i = V (x - 1)
1070 | otherwise = V x
1071 dropV i (Bind x b sc) = Bind x (fmap (dropV i) b) (dropV (i+1) sc)
1072 dropV i (App s f a) = App s (dropV i f) (dropV i a)
1073 dropV i (Proj x idx) = Proj (dropV i x) idx
1074 dropV i t = t
1076-- | Replace all non-free de Bruijn references in the given term with references
1077-- to the name of their binding.
1078explicitNames :: TT n -> TT n
1079explicitNames (Bind x b sc) = let b' = fmap explicitNames b in
1080 Bind x b'
1081 (explicitNames (instantiate
1082 (P Bound x (binderTy b')) sc))
1083explicitNames (App s f a) = App s (explicitNames f) (explicitNames a)
1084explicitNames (Proj x idx) = Proj (explicitNames x) idx
1085explicitNames t = t
1087-- | Replace references to the given 'Name'-like id with references to
1088-- de Bruijn index 0.
1089pToV :: Eq n => n -> TT n -> TT n
1090pToV n = pToV' n 0
1091pToV' n i (P _ x _) | n == x = V i
1092pToV' n i (Bind x b sc)
1093-- We can assume the inner scope has been pToVed already, so continue to
1094-- resolve names from the *outer* scope which may happen to have the same id.
1095 | n == x = Bind x (fmap (pToV' n i) b) sc
1096 | otherwise = Bind x (fmap (pToV' n i) b) (pToV' n (i+1) sc)
1097pToV' n i (App s f a) = App s (pToV' n i f) (pToV' n i a)
1098pToV' n i (Proj t idx) = Proj (pToV' n i t) idx
1099pToV' n i t = t
1101-- increase de Bruijn indices, as if a binder has been added
1102addBinder :: TT n -> TT n
1103addBinder t = ab 0 t
1104 where
1105 ab top (V i) | i >= top = V (i + 1)
1106 | otherwise = V i
1107 ab top (Bind x b sc) = Bind x (fmap (ab top) b) (ab (top + 1) sc)
1108 ab top (App s f a) = App s (ab top f) (ab top a)
1109 ab top (Proj t idx) = Proj (ab top t) idx
1110 ab top t = t
1112-- | Convert several names. First in the list comes out as V 0
1113pToVs :: Eq n => [n] -> TT n -> TT n
1114pToVs ns tm = pToVs' ns tm 0 where
1115 pToVs' [] tm i = tm
1116 pToVs' (n:ns) tm i = pToV' n i (pToVs' ns tm (i+1))
1118-- | Replace de Bruijn indices in the given term with explicit references to
1119-- the names of the bindings they refer to. It is an error if the given term
1120-- contains free de Bruijn indices.
1121vToP :: TT n -> TT n
1122vToP = vToP' [] where
1123 vToP' env (V i) = let (n, b) = (env !! i) in
1124 P Bound n (binderTy b)
1125 vToP' env (Bind n b sc) = let b' = fmap (vToP' env) b in
1126 Bind n b' (vToP' ((n, b'):env) sc)
1127 vToP' env (App s f a) = App s (vToP' env f) (vToP' env a)
1128 vToP' env t = t
1130-- | Replace every non-free reference to the name of a binding in
1131-- the given term with a de Bruijn index.
1132finalise :: Eq n => TT n -> TT n
1133finalise (Bind x b sc) = Bind x (fmap finalise b) (pToV x (finalise sc))
1134finalise (App s f a) = App s (finalise f) (finalise a)
1135finalise t = t
1137-- Once we've finished checking everything about a term we no longer need
1138-- the type on the 'P' so erase it so save memory
1140pEraseType :: TT n -> TT n
1141pEraseType (P nt t _) = P nt t Erased
1142pEraseType (App s f a) = App s (pEraseType f) (pEraseType a)
1143pEraseType (Bind n b sc) = Bind n (fmap pEraseType b) (pEraseType sc)
1144pEraseType t = t
1146-- | As 'instantiate', but in addition to replacing @'V' 0@,
1147-- replace references to the given 'Name'-like id.
1148subst :: Eq n => n {-^ The id to replace -} ->
1149 TT n {-^ The replacement term -} ->
1150 TT n {-^ The term to replace in -} ->
1151 TT n
1152-- subst n v tm = instantiate v (pToV n tm)
1153subst n v tm = fst $ subst' 0 tm
1154 where
1155 -- keep track of updates to save allocations - this is a big win on
1156 -- large terms in particular
1157 -- ('Maybe' would be neater here, but >>= is not the right combinator.
1158 -- Feel free to tidy up, as long as it still saves allocating when no
1159 -- substitution happens...)
1160 subst' i (V x) | i == x = (v, True)
1161 subst' i (P _ x _) | n == x = (v, True)
1162 subst' i t@(P nt x ty)
1163 = let (ty', ut) = subst' i ty in
1164 if ut then (P nt x ty', True) else (t, False)
1165 subst' i t@(Bind x b sc) | x /= n
1166 = let (b', ub) = substB' i b
1167 (sc', usc) = subst' (i+1) sc in
1168 if ub || usc then (Bind x b' sc', True) else (t, False)
1169 subst' i t@(App s f a) = let (f', uf) = subst' i f
1170 (a', ua) = subst' i a in
1171 if uf || ua then (App s f' a', True) else (t, False)
1172 subst' i t@(Proj x idx) = let (x', u) = subst' i x in
1173 if u then (Proj x' idx, u) else (t, False)
1174 subst' i t = (t, False)
1176 substB' i b@(Let t v) = let (t', ut) = subst' i t
1177 (v', uv) = subst' i v in
1178 if ut || uv then (Let t' v', True)
1179 else (b, False)
1180 substB' i b@(Guess t v) = let (t', ut) = subst' i t
1181 (v', uv) = subst' i v in
1182 if ut || uv then (Guess t' v', True)
1183 else (b, False)
1184 substB' i b = let (ty', u) = subst' i (binderTy b) in
1185 if u then (b { binderTy = ty' }, u) else (b, False)
1187-- If there are no Vs in the term (i.e. in proof state)
1188psubst :: Eq n => n -> TT n -> TT n -> TT n
1189psubst n v tm = s' 0 tm where
1190 s' i (V x) | x > i = V (x - 1)
1191 | x == i = v
1192 | otherwise = V x
1193 s' i (P _ x _) | n == x = v
1194 s' i (Bind x b sc) | n == x = Bind x (fmap (s' i) b) sc
1195 | otherwise = Bind x (fmap (s' i) b) (s' (i+1) sc)
1196 s' i (App st f a) = App st (s' i f) (s' i a)
1197 s' i (Proj t idx) = Proj (s' i t) idx
1198 s' i t = t
1200-- | As 'subst', but takes a list of (name, substitution) pairs instead
1201-- of a single name and substitution
1202substNames :: Eq n => [(n, TT n)] -> TT n -> TT n
1203substNames [] t = t
1204substNames ((n, tm) : xs) t = subst n tm (substNames xs t)
1206-- | Replaces all terms equal (in the sense of @(==)@) to
1207-- the old term with the new term.
1208substTerm :: Eq n => TT n {-^ Old term -} ->
1209 TT n {-^ New term -} ->
1210 TT n {-^ template term -}
1211 -> TT n
1212substTerm old new = st where
1213 st t | t == old = new
1214 st (App s f a) = App s (st f) (st a)
1215 st (Bind x b sc) = Bind x (fmap st b) (st sc)
1216 st t = t
1218-- | Return number of occurrences of V 0 or bound name i the term
1219occurrences :: Eq n => n -> TT n -> Int
1220occurrences n t = execState (no' 0 t) 0
1221 where
1222 no' i (V x) | i == x = do num <- get; put (num + 1)
1223 no' i (P Bound x _) | n == x = do num <- get; put (num + 1)
1224 no' i (Bind n b sc) = do noB' i b; no' (i+1) sc
1225 where noB' i (Let t v) = do no' i t; no' i v
1226 noB' i (Guess t v) = do no' i t; no' i v
1227 noB' i b = no' i (binderTy b)
1228 no' i (App _ f a) = do no' i f; no' i a
1229 no' i (Proj x _) = no' i x
1230 no' i _ = return ()
1232-- | Returns true if V 0 and bound name n do not occur in the term
1233noOccurrence :: Eq n => n -> TT n -> Bool
1234noOccurrence n t = no' 0 t
1235 where
1236 no' i (V x) = not (i == x)
1237 no' i (P Bound x _) = not (n == x)
1238 no' i (Bind n b sc) = noB' i b && no' (i+1) sc
1239 where noB' i (Let t v) = no' i t && no' i v
1240 noB' i (Guess t v) = no' i t && no' i v
1241 noB' i b = no' i (binderTy b)
1242 no' i (App _ f a) = no' i f && no' i a
1243 no' i (Proj x _) = no' i x
1244 no' i _ = True
1246-- | Returns all names used free in the term
1247freeNames :: Eq n => TT n -> [n]
1248freeNames t = nub $ freeNames' t
1249 where
1250 freeNames' (P _ n _) = [n]
1251 freeNames' (Bind n (Let t v) sc) = freeNames' v ++ (freeNames' sc \\ [n])
1252 ++ freeNames' t
1253 freeNames' (Bind n b sc) = freeNames' (binderTy b) ++ (freeNames' sc \\ [n])
1254 freeNames' (App _ f a) = freeNames' f ++ freeNames' a
1255 freeNames' (Proj x i) = freeNames' x
1256 freeNames' _ = []
1258-- | Return the arity of a (normalised) type
1259arity :: TT n -> Int
1260arity (Bind n (Pi _ t _) sc) = 1 + arity sc
1261arity _ = 0
1263-- | Deconstruct an application; returns the function and a list of arguments
1264unApply :: TT n -> (TT n, [TT n])
1265unApply t = ua [] t where
1266 ua args (App _ f a) = ua (a:args) f
1267 ua args t = (t, args)
1269-- | Returns a term representing the application of the first argument
1270-- (a function) to every element of the second argument.
1271mkApp :: TT n -> [TT n] -> TT n
1272mkApp f [] = f
1273mkApp f (a:as) = mkApp (App MaybeHoles f a) as
1275unList :: Term -> Maybe [Term]
1276unList tm = case unApply tm of
1277 (nil, [_]) -> Just []
1278 (cons, ([_, x, xs])) ->
1279 do rest <- unList xs
1280 return $ x:rest
1281 (f, args) -> Nothing
1283-- | Hard-code a heuristic maximum term size, to prevent attempts to
1284-- serialize or force infinite or just gigantic terms
1285termSmallerThan :: Int -> Term -> Bool
1286termSmallerThan x tm | x <= 0 = False
1287termSmallerThan x (P _ _ ty) = termSmallerThan (x-1) ty
1288termSmallerThan x (Bind _ _ tm) = termSmallerThan (x-1) tm
1289termSmallerThan x (App _ f a) = termSmallerThan (x-1) f && termSmallerThan (x-1) a
1290termSmallerThan x (Proj tm _) = termSmallerThan (x-1) tm
1291termSmallerThan x (V i) = True
1292termSmallerThan x (Constant c) = True
1293termSmallerThan x Erased = True
1294termSmallerThan x Impossible = True
1295termSmallerThan x (TType u) = True
1296termSmallerThan x (UType u) = True
1299-- | Cast a 'TT' term to a 'Raw' value, discarding universe information and
1300-- the types of named references and replacing all de Bruijn indices
1301-- with the corresponding name. It is an error if there are free de
1302-- Bruijn indices.
1303forget :: TT Name -> Raw
1304forget tm = forgetEnv [] tm
1306safeForget :: TT Name -> Maybe Raw
1307safeForget tm = safeForgetEnv [] tm
1309forgetEnv :: [Name] -> TT Name -> Raw
1310forgetEnv env tm = case safeForgetEnv env tm of
1311 Just t' -> t'
1312 Nothing -> error $ "Scope error in " ++ show tm ++ show env
1315safeForgetEnv :: [Name] -> TT Name -> Maybe Raw
1316safeForgetEnv env (P _ n _) = Just $ Var n
1317safeForgetEnv env (V i) | i < length env = Just $ Var (env !! i)
1318 | otherwise = Nothing
1319safeForgetEnv env (Bind n b sc)
1320 = do let n' = uniqueName n env
1321 b' <- safeForgetEnvB env b
1322 sc' <- safeForgetEnv (n':env) sc
1323 Just $ RBind n' b' sc'
1324 where safeForgetEnvB env (Let t v) = liftM2 Let (safeForgetEnv env t)
1325 (safeForgetEnv env v)
1326 safeForgetEnvB env (Guess t v) = liftM2 Guess (safeForgetEnv env t)
1327 (safeForgetEnv env v)
1328 safeForgetEnvB env b = do ty' <- safeForgetEnv env (binderTy b)
1329 Just $ fmap (\_ -> ty') b
1330safeForgetEnv env (App _ f a) = liftM2 RApp (safeForgetEnv env f) (safeForgetEnv env a)
1331safeForgetEnv env (Constant c) = Just $ RConstant c
1332safeForgetEnv env (TType i) = Just RType
1333safeForgetEnv env (UType u) = Just $ RUType u
1334safeForgetEnv env Erased = Just $ RConstant Forgot
1335safeForgetEnv env (Proj tm i) = error "Don't know how to forget a projection"
1336safeForgetEnv env Impossible = error "Don't know how to forget Impossible"
1338-- | Introduce a 'Bind' into the given term for each element of the
1339-- given list of (name, binder) pairs.
1340bindAll :: [(n, Binder (TT n))] -> TT n -> TT n
1341bindAll [] t = t
1342bindAll ((n, b) : bs) t = Bind n b (bindAll bs t)
1344-- | Like 'bindAll', but the 'Binder's are 'TT' terms instead.
1345-- The first argument is a function to map @TT@ terms to @Binder@s.
1346-- This function might often be something like 'Lam', which directly
1347-- constructs a @Binder@ from a @TT@ term.
1348bindTyArgs :: (TT n -> Binder (TT n)) -> [(n, TT n)] -> TT n -> TT n
1349bindTyArgs b xs = bindAll (map (\ (n, ty) -> (n, b ty)) xs)
1351-- | Return a list of pairs of the names of the outermost 'Pi'-bound
1352-- variables in the given term, together with their types.
1353getArgTys :: TT n -> [(n, TT n)]
1354getArgTys (Bind n (PVar _) sc) = getArgTys sc
1355getArgTys (Bind n (PVTy _) sc) = getArgTys sc
1356getArgTys (Bind n (Pi _ t _) sc) = (n, t) : getArgTys sc
1357getArgTys _ = []
1359getRetTy :: TT n -> TT n
1360getRetTy (Bind n (PVar _) sc) = getRetTy sc
1361getRetTy (Bind n (PVTy _) sc) = getRetTy sc
1362getRetTy (Bind n (Pi _ _ _) sc) = getRetTy sc
1363getRetTy sc = sc
1365uniqueNameFrom :: [Name] -> [Name] -> Name
1366uniqueNameFrom [] hs = uniqueName (nextName (sUN "x")) hs
1367uniqueNameFrom (s : supply) hs
1368 | s `elem` hs = uniqueNameFrom supply hs
1369 | otherwise = s
1371uniqueName :: Name -> [Name] -> Name
1372uniqueName n hs | n `elem` hs = uniqueName (nextName n) hs
1373 | otherwise = n
1375uniqueNameSet :: Name -> Set Name -> Name
1376uniqueNameSet n hs | n `member` hs = uniqueNameSet (nextName n) hs
1377 | otherwise = n
1379uniqueBinders :: [Name] -> TT Name -> TT Name
1380uniqueBinders ns = ubSet (fromList ns) where
1381 ubSet ns (Bind n b sc)
1382 = let n' = uniqueNameSet n ns
1383 ns' = insert n' ns in
1384 Bind n' (fmap (ubSet ns') b) (ubSet ns' sc)
1385 ubSet ns (App s f a) = App s (ubSet ns f) (ubSet ns a)
1386 ubSet ns t = t
1389nextName :: Name -> Name
1390nextName (NS x s) = NS (nextName x) s
1391nextName (MN i n) = MN (i+1) n
1392nextName (UN x) = let (num', nm') = T.span isDigit (T.reverse x)
1393 nm = T.reverse nm'
1394 num = readN (T.reverse num') in
1395 UN (nm `T.append` txt (show (num+1)))
1396 where
1397 readN x | not (T.null x) = read (T.unpack x)
1398 readN x = 0
1399nextName (SN x) = SN (nextName' x)
1400 where
1401 nextName' (WhereN i f x) = WhereN i f (nextName x)
1402 nextName' (WithN i n) = WithN i (nextName n)
1403 nextName' (InstanceN n ns) = InstanceN (nextName n) ns
1404 nextName' (ParentN n ns) = ParentN (nextName n) ns
1405 nextName' (CaseN n) = CaseN (nextName n)
1406 nextName' (ElimN n) = ElimN (nextName n)
1407 nextName' (MethodN n) = MethodN (nextName n)
1408 nextName' (InstanceCtorN n) = InstanceCtorN (nextName n)
1409 nextName' (MetaN parent meta) = MetaN parent (nextName meta)
1410nextName NErased = NErased
1411nextName (SymRef i) = error "Can't generate a name from a symbol reference"
1413type Term = TT Name
1414type Type = Term
1416type Env = EnvTT Name
1418-- | an environment with de Bruijn indices 'normalised' so that they all refer to
1419-- this environment
1421newtype WkEnvTT n = Wk (EnvTT n)
1422type WkEnv = WkEnvTT Name
1424instance (Eq n, Show n) => Show (TT n) where
1425 show t = showEnv [] t
1427itBitsName IT8 = "Bits8"
1428itBitsName IT16 = "Bits16"
1429itBitsName IT32 = "Bits32"
1430itBitsName IT64 = "Bits64"
1432instance Show Const where
1433 show (I i) = show i
1434 show (BI i) = show i
1435 show (Fl f) = show f
1436 show (Ch c) = show c
1437 show (Str s) = show s
1438 show (B8 x) = show x
1439 show (B16 x) = show x
1440 show (B32 x) = show x
1441 show (B64 x) = show x
1442 show (AType ATFloat) = "Double"
1443 show (AType (ATInt ITBig)) = "Integer"
1444 show (AType (ATInt ITNative)) = "Int"
1445 show (AType (ATInt ITChar)) = "Char"
1446 show (AType (ATInt (ITFixed it))) = itBitsName it
1447 show TheWorld = "prim__TheWorld"
1448 show WorldType = "prim__WorldType"
1449 show StrType = "String"
1450 show VoidType = "Void"
1451 show Forgot = "Forgot"
1453showEnv :: (Eq n, Show n) => EnvTT n -> TT n -> String
1454showEnv env t = showEnv' env t False
1455showEnvDbg env t = showEnv' env t True
1457prettyEnv :: Env -> Term -> Doc OutputAnnotation
1458prettyEnv env t = prettyEnv' env t False
1459 where
1460 prettyEnv' env t dbg = prettySe 10 env t dbg
1462 bracket outer inner p
1463 | inner > outer = lparen <> p <> rparen
1464 | otherwise = p
1466 prettySe p env (P nt n t) debug =
1467 pretty n <+>
1468 if debug then
1469 lbracket <+> pretty nt <+> colon <+> prettySe 10 env t debug <+> rbracket
1470 else
1471 empty
1472 prettySe p env (V i) debug
1473 | i < length env =
1474 if debug then
1475 text . show . fst $ env!!i
1476 else
1477 lbracket <+> text (show i) <+> rbracket
1478 | otherwise = text "unbound" <+> text (show i) <+> text "!"
1479 prettySe p env (Bind n b@(Pi _ t _) sc) debug
1480 | noOccurrence n sc && not debug =
1481 bracket p 2 $ prettySb env n b debug <> prettySe 10 ((n, b):env) sc debug
1482 prettySe p env (Bind n b sc) debug =
1483 bracket p 2 $ prettySb env n b debug <> prettySe 10 ((n, b):env) sc debug
1484 prettySe p env (App _ f a) debug =
1485 bracket p 1 $ prettySe 1 env f debug <+> prettySe 0 env a debug
1486 prettySe p env (Proj x i) debug =
1487 prettySe 1 env x debug <+> text ("!" ++ show i)
1488 prettySe p env (Constant c) debug = pretty c
1489 prettySe p env Erased debug = text "[_]"
1490 prettySe p env (TType i) debug = text "Type" <+> (text . show $ i)
1491 prettySe p env Impossible debug = text "Impossible"
1492 prettySe p env (UType u) debug = text (show u)
1494 -- Render a `Binder` and its name
1495 prettySb env n (Lam t) = prettyB env "λ" "=>" n t
1496 prettySb env n (Hole t) = prettyB env "?defer" "." n t
1497 prettySb env n (GHole _ t) = prettyB env "?gdefer" "." n t
1498 prettySb env n (Pi _ t _) = prettyB env "(" ") ->" n t
1499 prettySb env n (PVar t) = prettyB env "pat" "." n t
1500 prettySb env n (PVTy t) = prettyB env "pty" "." n t
1501 prettySb env n (Let t v) = prettyBv env "let" "in" n t v
1502 prettySb env n (NLet t v) = prettyBv env "nlet" "in" n t v
1503 prettySb env n (Guess t v) = prettyBv env "??" "in" n t v
1505 -- Use `op` and `sc` to delimit `n` (a binding name) and its type
1506 -- declaration
1507 -- e.g. "λx : Int =>" for the Lam case
1508 prettyB env op sc n t debug =
1509 text op <> pretty n <+> colon <+> prettySe 10 env t debug <> text sc
1511 -- Like `prettyB`, but handle the bindings that have values in addition
1512 -- to names and types
1513 prettyBv env op sc n t v debug =
1514 text op <> pretty n <+> colon <+> prettySe 10 env t debug <+> text "=" <+>
1515 prettySe 10 env v debug <> text sc
1518showEnv' env t dbg = se 10 env t where
1519 se p env (P nt n t) = show n
1520 ++ if dbg then "{" ++ show nt ++ " : " ++ se 10 env t ++ "}" else ""
1521 se p env (V i) | i < length env && i >= 0
1522 = (show $ fst $ env!!i) ++
1523 if dbg then "{" ++ show i ++ "}" else ""
1524 | otherwise = "!!V " ++ show i ++ "!!"
1525 se p env (Bind n b@(Pi (Just _) t k) sc)
1526 = bracket p 2 $ sb env n b ++ se 10 ((n,b):env) sc
1527 se p env (Bind n b@(Pi _ t k) sc)
1528 | noOccurrence n sc && not dbg = bracket p 2 $ se 1 env t ++ arrow k ++ se 10 ((n,b):env) sc
1529 where arrow (TType _) = " -> "
1530 arrow u = " [" ++ show u ++ "] -> "
1531 se p env (Bind n b sc) = bracket p 2 $ sb env n b ++ se 10 ((n,b):env) sc
1532 se p env (App _ f a) = bracket p 1 $ se 1 env f ++ " " ++ se 0 env a
1533 se p env (Proj x i) = se 1 env x ++ "!" ++ show i
1534 se p env (Constant c) = show c
1535 se p env Erased = "[__]"
1536 se p env Impossible = "[impossible]"
1537 se p env (TType i) = "Type " ++ show i
1538 se p env (UType u) = show u
1540 sb env n (Lam t) = showb env "\\ " " => " n t
1541 sb env n (Hole t) = showb env "? " ". " n t
1542 sb env n (GHole i t) = showb env "?defer " ". " n t
1543 sb env n (Pi (Just _) t _) = showb env "{" "} -> " n t
1544 sb env n (Pi _ t _) = showb env "(" ") -> " n t
1545 sb env n (PVar t) = showb env "pat " ". " n t
1546 sb env n (PVTy t) = showb env "pty " ". " n t
1547 sb env n (Let t v) = showbv env "let " " in " n t v
1548 sb env n (NLet t v) = showbv env "nlet " " in " n t v
1549 sb env n (Guess t v) = showbv env "?? " " in " n t v
1551 showb env op sc n t = op ++ show n ++ " : " ++ se 10 env t ++ sc
1552 showbv env op sc n t v = op ++ show n ++ " : " ++ se 10 env t ++ " = " ++
1553 se 10 env v ++ sc
1555 bracket outer inner str | inner > outer = "(" ++ str ++ ")"
1556 | otherwise = str
1558-- | Check whether a term has any hole bindings in it - impure if so
1559pureTerm :: TT Name -> Bool
1560pureTerm (App _ f a) = pureTerm f && pureTerm a
1561pureTerm (Bind n b sc) = notClassName n && pureBinder b && pureTerm sc where
1562 pureBinder (Hole _) = False
1563 pureBinder (Guess _ _) = False
1564 pureBinder (Let t v) = pureTerm t && pureTerm v
1565 pureBinder t = pureTerm (binderTy t)
1567 notClassName (MN _ c) | c == txt "class" = False
1568 notClassName _ = True
1570pureTerm _ = True
1572-- | Weaken a term by adding i to each de Bruijn index (i.e. lift it over i bindings)
1573weakenTm :: Int -> TT n -> TT n
1574weakenTm i t = wk i 0 t
1575 where wk i min (V x) | x >= min = V (i + x)
1576 wk i m (App s f a) = App s (wk i m f) (wk i m a)
1577 wk i m (Bind x b sc) = Bind x (wkb i m b) (wk i (m + 1) sc)
1578 wk i m t = t
1579 wkb i m t = fmap (wk i m) t
1581-- | Weaken an environment so that all the de Bruijn indices are correct according
1582-- to the latest bound variable
1584weakenEnv :: EnvTT n -> EnvTT n
1585weakenEnv env = wk (length env - 1) env
1586 where wk i [] = []
1587 wk i ((n, b) : bs) = (n, weakenTmB i b) : wk (i - 1) bs
1588 weakenTmB i (Let t v) = Let (weakenTm i t) (weakenTm i v)
1589 weakenTmB i (Guess t v) = Guess (weakenTm i t) (weakenTm i v)
1590 weakenTmB i t = t { binderTy = weakenTm i (binderTy t) }
1592-- | Weaken every term in the environment by the given amount
1593weakenTmEnv :: Int -> EnvTT n -> EnvTT n
1594weakenTmEnv i = map (\ (n, b) -> (n, fmap (weakenTm i) b))
1596-- | Gather up all the outer 'PVar's and 'Hole's in an expression and reintroduce
1597-- them in a canonical order
1598orderPats :: Term -> Term
1599orderPats tm = op [] tm
1600 where
1601 op [] (App s f a) = App s f (op [] a) -- for Infer terms
1603 op ps (Bind n (PVar t) sc) = op ((n, PVar t) : ps) sc
1604 op ps (Bind n (Hole t) sc) = op ((n, Hole t) : ps) sc
1605 op ps (Bind n (Pi i t k) sc) = op ((n, Pi i t k) : ps) sc
1606 op ps sc = bindAll (sortP ps) sc
1608 sortP ps = pick [] (reverse ps)
1610 pick acc [] = reverse acc
1611 pick acc ((n, t) : ps) = pick (insert n t acc) ps
1613 insert n t [] = [(n, t)]
1614 insert n t ((n',t') : ps)
1615 | n `elem` (refsIn (binderTy t') ++
1616 concatMap refsIn (map (binderTy . snd) ps))
1617 = (n', t') : insert n t ps
1618 | otherwise = (n,t):(n',t'):ps
1620refsIn :: TT Name -> [Name]
1621refsIn (P _ n _) = [n]
1622refsIn (Bind n b t) = nub $ nb b ++ refsIn t
1623 where nb (Let t v) = nub (refsIn t) ++ nub (refsIn v)
1624 nb (Guess t v) = nub (refsIn t) ++ nub (refsIn v)
1625 nb t = refsIn (binderTy t)
1626refsIn (App s f a) = nub (refsIn f ++ refsIn a)
1627refsIn _ = []
1629-- Make sure all the pattern bindings are as far out as possible
1630liftPats :: Term -> Term
1631liftPats tm = let (tm', ps) = runState (getPats tm) [] in
1632 orderPats $ bindPats (reverse ps) tm'
1633 where
1634 bindPats [] tm = tm
1635 bindPats ((n, t):ps) tm
1636 | n `notElem` map fst ps = Bind n (PVar t) (bindPats ps tm)
1637 | otherwise = bindPats ps tm
1639 getPats :: Term -> State [(Name, Type)] Term
1640 getPats (Bind n (PVar t) sc) = do ps <- get
1641 put ((n, t) : ps)
1642 getPats sc
1643 getPats (Bind n (Guess t v) sc) = do t' <- getPats t
1644 v' <- getPats v
1645 sc' <- getPats sc
1646 return (Bind n (Guess t' v') sc')
1647 getPats (Bind n (Let t v) sc) = do t' <- getPats t
1648 v' <- getPats v
1649 sc' <- getPats sc
1650 return (Bind n (Let t' v') sc')
1651 getPats (Bind n (Pi i t k) sc) = do t' <- getPats t
1652 k' <- getPats k
1653 sc' <- getPats sc
1654 return (Bind n (Pi i t' k') sc')
1655 getPats (Bind n (Lam t) sc) = do t' <- getPats t
1656 sc' <- getPats sc
1657 return (Bind n (Lam t') sc')
1658 getPats (Bind n (Hole t) sc) = do t' <- getPats t
1659 sc' <- getPats sc
1660 return (Bind n (Hole t') sc')
1663 getPats (App s f a) = do f' <- getPats f
1664 a' <- getPats a
1665 return (App s f' a')
1666 getPats t = return t
1668allTTNames :: Eq n => TT n -> [n]
1669allTTNames = nub . allNamesIn
1670 where allNamesIn (P _ n _) = [n]
1671 allNamesIn (Bind n b t) = [n] ++ nb b ++ allNamesIn t
1672 where nb (Let t v) = allNamesIn t ++ allNamesIn v
1673 nb (Guess t v) = allNamesIn t ++ allNamesIn v
1674 nb t = allNamesIn (binderTy t)
1675 allNamesIn (App _ f a) = allNamesIn f ++ allNamesIn a
1676 allNamesIn _ = []
1679-- | Pretty-print a term
1680pprintTT :: [Name] -- ^ The bound names (for highlighting and de Bruijn indices)
1681 -> TT Name -- ^ The term to be printed
1682 -> Doc OutputAnnotation
1683pprintTT bound tm = pp startPrec bound tm
1685 where
1686 startPrec = 0
1687 appPrec = 10
1689 pp p bound (P Bound n ty) = annotate (AnnBoundName n False) (text $ show n)
1690 pp p bound (P nt n ty) = annotate (AnnName n Nothing Nothing Nothing)
1691 (text $ show n)
1692 pp p bound (V i)
1693 | i < length bound = let n = bound !! i
1694 in annotate (AnnBoundName n False) (text $ show n)
1695 | otherwise = text ("{{{V" ++ show i ++ "}}}")
1696 pp p bound (Bind n b sc) = ppb p bound n b $
1697 pp startPrec (n:bound) sc
1698 pp p bound (App _ tm1 tm2) =
1699 bracket p appPrec . group . hang 2 $
1700 pp appPrec bound tm1 <> line <>
1701 pp (appPrec + 1) bound tm2
1702 pp p bound (Constant c) = annotate (AnnConst c) (text (show c))
1703 pp p bound (Proj tm i) =
1704 lparen <> pp startPrec bound tm <> rparen <>
1705 text "!" <> text (show i)
1706 pp p bound Erased = text "<<<erased>>>"
1707 pp p bound Impossible = text "<<<impossible>>>"
1708 pp p bound (TType ue) = annotate (AnnType "Type" "The type of types") $
1709 text "Type"
1710 pp p bound (UType u) = text (show u)
1712 ppb p bound n (Lam ty) sc =
1713 bracket p startPrec . group . align . hang 2 $
1714 text "λ" <+> bindingOf n False <+> text "." <> line <> sc
1715 ppb p bound n (Pi _ ty k) sc =
1716 bracket p startPrec . group . align $
1717 lparen <> (bindingOf n False) <+> colon <+>
1718 (group . align) (pp startPrec bound ty) <>
1719 rparen <+> mkArrow k <> line <> sc
1720 where mkArrow (UType UniqueType) = text "⇴"
1721 mkArrow (UType NullType) = text "⥛"
1722 mkArrow _ = text "→"
1723 ppb p bound n (Let ty val) sc =
1724 bracket p startPrec . group . align $
1725 (group . hang 2) (annotate AnnKeyword (text "let") <+>
1726 bindingOf n False <+> colon <+>
1727 pp startPrec bound ty <+>
1728 text "=" <> line <>
1729 pp startPrec bound val) <> line <>
1730 (group . hang 2) (annotate AnnKeyword (text "in") <+> sc)
1731 ppb p bound n (NLet ty val) sc =
1732 bracket p startPrec . group . align $
1733 (group . hang 2) (annotate AnnKeyword (text "nlet") <+>
1734 bindingOf n False <+> colon <+>
1735 pp startPrec bound ty <+>
1736 text "=" <> line <>
1737 pp startPrec bound val) <> line <>
1738 (group . hang 2) (annotate AnnKeyword (text "in") <+> sc)
1739 ppb p bound n (Hole ty) sc =
1740 bracket p startPrec . group . align . hang 2 $
1741 text "?" <+> bindingOf n False <+> text "." <> line <> sc
1742 ppb p bound n (GHole _ ty) sc =
1743 bracket p startPrec . group . align . hang 2 $
1744 text "¿" <+> bindingOf n False <+> text "." <> line <> sc
1745 ppb p bound n (Guess ty val) sc =
1746 bracket p startPrec . group . align . hang 2 $
1747 text "?" <> bindingOf n False <+>
1748 text "≈" <+> pp startPrec bound val <+>
1749 text "." <> line <> sc
1750 ppb p bound n (PVar ty) sc =
1751 bracket p startPrec . group . align . hang 2 $
1752 annotate AnnKeyword (text "pat") <+>
1753 bindingOf n False <+> colon <+> pp startPrec bound ty <+>
1754 text "." <> line <>
1755 sc
1756 ppb p bound n (PVTy ty) sc =
1757 bracket p startPrec . group . align . hang 2 $
1758 annotate AnnKeyword (text "patTy") <+>
1759 bindingOf n False <+> colon <+> pp startPrec bound ty <+>
1760 text "." <> line <>
1761 sc
1763 bracket outer inner doc
1764 | outer > inner = lparen <> doc <> rparen
1765 | otherwise = doc
1767-- | Pretty-print a raw term.
1768pprintRaw :: [Name] -- ^ Bound names, for highlighting
1769 -> Raw -- ^ The term to pretty-print
1770 -> Doc OutputAnnotation
1771pprintRaw bound (Var n) =
1772 enclose lparen rparen . group . align . hang 2 $
1773 (text "Var") <$> annotate (if n `elem` bound
1774 then AnnBoundName n False
1775 else AnnName n Nothing Nothing Nothing)
1776 (text $ show n)
1777pprintRaw bound (RBind n b body) =
1778 enclose lparen rparen . group . align . hang 2 $
1779 vsep [ text "RBind"
1780 , annotate (AnnBoundName n False) (text $ show n)
1781 , ppb b
1782 , pprintRaw (n:bound) body]
1783 where
1784 ppb (Lam ty) = enclose lparen rparen . group . align . hang 2 $
1785 text "Lam" <$> pprintRaw bound ty
1786 ppb (Pi _ ty k) = enclose lparen rparen . group . align . hang 2 $
1787 vsep [text "Pi", pprintRaw bound ty, pprintRaw bound k]
1788 ppb (Let ty v) = enclose lparen rparen . group . align . hang 2 $
1789 vsep [text "Let", pprintRaw bound ty, pprintRaw bound v]
1790 ppb (NLet ty v) = enclose lparen rparen . group . align . hang 2 $
1791 vsep [text "NLet", pprintRaw bound ty, pprintRaw bound v]
1792 ppb (Hole ty) = enclose lparen rparen . group . align . hang 2 $
1793 text "Hole" <$> pprintRaw bound ty
1794 ppb (GHole _ ty) = enclose lparen rparen . group . align . hang 2 $
1795 text "GHole" <$> pprintRaw bound ty
1796 ppb (Guess ty v) = enclose lparen rparen . group . align . hang 2 $
1797 vsep [text "Guess", pprintRaw bound ty, pprintRaw bound v]
1798 ppb (PVar ty) = enclose lparen rparen . group . align . hang 2 $
1799 text "PVar" <$> pprintRaw bound ty
1800 ppb (PVTy ty) = enclose lparen rparen . group . align . hang 2 $
1801 text "PVTy" <$> pprintRaw bound ty
1802pprintRaw bound (RApp f x) =
1803 enclose lparen rparen . group . align . hang 2 . vsep $
1804 [text "RApp", pprintRaw bound f, pprintRaw bound x]
1805pprintRaw bound RType = text "RType"
1806pprintRaw bound (RUType u) = enclose lparen rparen . group . align . hang 2 $
1807 text "RUType" <$> text (show u)
1808pprintRaw bound (RForce r) =
1809 enclose lparen rparen . group . align . hang 2 $
1810 vsep [text "RForce", pprintRaw bound r]
1811pprintRaw bound (RConstant c) =
1812 enclose lparen rparen . group . align . hang 2 $
1813 vsep [text "RConstant", annotate (AnnConst c) (text (show c))]
1815-- | Pretty-printer helper for the binding site of a name
1816bindingOf :: Name -- ^^ the bound name
1817 -> Bool -- ^^ whether the name is implicit
1818 -> Doc OutputAnnotation
1819bindingOf n imp = annotate (AnnBoundName n imp) (text (show n))