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