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