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