git.iko.soy/Idris-dev
on 2d0cc49 help sign in
Idris-dev/src/Idris/AbsSyntaxTree.hs
1858 lines 75 kB history raw
1{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, DeriveFunctor,
2 TypeSynonymInstances, PatternGuards #-}
4module Idris.AbsSyntaxTree where
6import Idris.Core.TT
7import Idris.Core.Evaluate
8import Idris.Core.Elaborate hiding (Tactic(..))
9import Idris.Core.Typecheck
10import Idris.Docstrings
11import IRTS.Lang
12import IRTS.CodegenCommon
13import Util.Pretty
14import Util.DynamicLinker
16import Idris.Colours
18import System.Console.Haskeline
19import System.IO
21import Control.Monad.Trans.State.Strict
22import Control.Monad.Trans.Error
24import Data.Function (on)
25import Data.List hiding (group)
26import Data.Char
27import qualified Data.Map as M
28import qualified Data.Text as T
29import qualified Data.Map as M
30import Data.Either
31import qualified Data.Set as S
32import Data.Word (Word)
33import Data.Maybe (fromMaybe, mapMaybe)
34import Data.Traversable (Traversable)
35import Data.Foldable (Foldable)
37import Debug.Trace
39import Text.PrettyPrint.Annotated.Leijen
41data ElabWhat = ETypes | EDefns | EAll
42 deriving (Show, Eq)
44-- Data to pass to recursively called elaborators; e.g. for where blocks,
45-- paramaterised declarations, etc.
47-- rec_elabDecl is used to pass the top level elaborator into other elaborators,
48-- so that we can have mutually recursive elaborators in separate modules without
49-- having to much about with cyclic modules.
50data ElabInfo = EInfo { params :: [(Name, PTerm)],
51 inblock :: Ctxt [Name], -- names in the block, and their params
52 liftname :: Name -> Name,
53 namespace :: Maybe [String],
54 rec_elabDecl :: ElabWhat -> ElabInfo -> PDecl ->
55 Idris () }
57toplevel :: ElabInfo
58toplevel = EInfo [] emptyContext id Nothing (\_ _ _ -> fail "Not implemented")
60eInfoNames :: ElabInfo -> [Name]
61eInfoNames info = map fst (params info) ++ M.keys (inblock info)
63data IOption = IOption { opt_logLevel :: Int,
64 opt_typecase :: Bool,
65 opt_typeintype :: Bool,
66 opt_coverage :: Bool,
67 opt_showimp :: Bool, -- ^^ show implicits
68 opt_errContext :: Bool,
69 opt_repl :: Bool,
70 opt_verbose :: Bool,
71 opt_nobanner :: Bool,
72 opt_quiet :: Bool,
73 opt_codegen :: Codegen,
74 opt_outputTy :: OutputType,
75 opt_ibcsubdir :: FilePath,
76 opt_importdirs :: [FilePath],
77 opt_triple :: String,
78 opt_cpu :: String,
79 opt_cmdline :: [Opt], -- remember whole command line
80 opt_origerr :: Bool,
81 opt_autoSolve :: Bool, -- ^ automatically apply "solve" tactic in prover
82 opt_autoImport :: [FilePath], -- ^ e.g. Builtins+Prelude
83 opt_optimise :: [Optimisation]
84 }
85 deriving (Show, Eq)
87defaultOpts = IOption { opt_logLevel = 0
88 , opt_typecase = False
89 , opt_typeintype = False
90 , opt_coverage = True
91 , opt_showimp = False
92 , opt_errContext = False
93 , opt_repl = True
94 , opt_verbose = True
95 , opt_nobanner = False
96 , opt_quiet = False
97 , opt_codegen = Via "c"
98 , opt_outputTy = Executable
99 , opt_ibcsubdir = ""
100 , opt_importdirs = []
101 , opt_triple = ""
102 , opt_cpu = ""
103 , opt_cmdline = []
104 , opt_origerr = False
105 , opt_autoSolve = True
106 , opt_autoImport = []
107 , opt_optimise = defaultOptimise
108 }
110data PPOption = PPOption {
111 ppopt_impl :: Bool -- ^^ whether to show implicits
112} deriving (Show)
114data Optimisation = PETransform -- partial eval and associated transforms
115 deriving (Show, Eq)
117defaultOptimise = [PETransform]
119-- | Pretty printing options with default verbosity.
120defaultPPOption :: PPOption
121defaultPPOption = PPOption { ppopt_impl = False }
123-- | Pretty printing options with the most verbosity.
124verbosePPOption :: PPOption
125verbosePPOption = PPOption { ppopt_impl = True }
127-- | Get pretty printing options from the big options record.
128ppOption :: IOption -> PPOption
129ppOption opt = PPOption {
130 ppopt_impl = opt_showimp opt
133-- | Get pretty printing options from an idris state record.
134ppOptionIst :: IState -> PPOption
135ppOptionIst = ppOption . idris_options
137data LanguageExt = TypeProviders | ErrorReflection deriving (Show, Eq, Read, Ord)
139-- | The output mode in use
140data OutputMode = RawOutput Handle -- ^ Print user output directly to the handle
141 | IdeSlave Integer Handle -- ^ Send IDE output for some request ID to the handle
142 deriving Show
144-- | How wide is the console?
145data ConsoleWidth = InfinitelyWide -- ^ Have pretty-printer assume that lines should not be broken
146 | ColsWide Int -- ^ Manually specified - must be positive
147 | AutomaticWidth -- ^ Attempt to determine width, or 80 otherwise
149-- | The global state used in the Idris monad
150data IState = IState {
151 tt_ctxt :: Context, -- ^ All the currently defined names and their terms
152 idris_constraints :: [(UConstraint, FC)],
153 -- ^ A list of universe constraints and their corresponding source locations
154 idris_infixes :: [FixDecl], -- ^ Currently defined infix operators
155 idris_implicits :: Ctxt [PArg],
156 idris_statics :: Ctxt [Bool],
157 idris_classes :: Ctxt ClassInfo,
158 idris_dsls :: Ctxt DSL,
159 idris_optimisation :: Ctxt OptInfo,
160 idris_datatypes :: Ctxt TypeInfo,
161 idris_namehints :: Ctxt [Name],
162 idris_patdefs :: Ctxt ([([Name], Term, Term)], [PTerm]), -- not exported
163 -- ^ list of lhs/rhs, and a list of missing clauses
164 idris_flags :: Ctxt [FnOpt],
165 idris_callgraph :: Ctxt CGInfo, -- name, args used in each pos
166 idris_calledgraph :: Ctxt [Name],
167 idris_docstrings :: Ctxt (Docstring DocTerm, [(Name, Docstring DocTerm)]),
168 idris_tyinfodata :: Ctxt TIData,
169 idris_fninfo :: Ctxt FnInfo,
170 idris_transforms :: Ctxt [(Term, Term)],
171 idris_totcheck :: [(FC, Name)], -- names to check totality on
172 idris_defertotcheck :: [(FC, Name)], -- names to check at the end
173 idris_totcheckfail :: [(FC, String)],
174 idris_options :: IOption,
175 idris_name :: Int,
176 idris_lineapps :: [((FilePath, Int), PTerm)],
177 -- ^ Full application LHS on source line
178 idris_metavars :: [(Name, (Maybe Name, Int, Bool))], -- ^ The currently defined but not proven metavariables
179 idris_coercions :: [Name],
180 idris_errRev :: [(Term, Term)],
181 syntax_rules :: SyntaxRules,
182 syntax_keywords :: [String],
183 imported :: [FilePath], -- ^ The imported modules
184 idris_scprims :: [(Name, (Int, PrimFn))],
185 idris_objs :: [(Codegen, FilePath)],
186 idris_libs :: [(Codegen, String)],
187 idris_cgflags :: [(Codegen, String)],
188 idris_hdrs :: [(Codegen, String)],
189 idris_imported :: [FilePath], -- ^ Imported ibc file names
190 proof_list :: [(Name, [String])],
191 errSpan :: Maybe FC,
192 parserWarnings :: [(FC, Err)],
193 lastParse :: Maybe Name,
194 indent_stack :: [Int],
195 brace_stack :: [Maybe Int],
196 lastTokenSpan :: Maybe FC, -- ^ What was the span of the latest token parsed?
197 idris_parsedSpan :: Maybe FC,
198 hide_list :: [(Name, Maybe Accessibility)],
199 default_access :: Accessibility,
200 default_total :: Bool,
201 ibc_write :: [IBCWrite],
202 compiled_so :: Maybe String,
203 idris_dynamic_libs :: [DynamicLib],
204 idris_language_extensions :: [LanguageExt],
205 idris_outputmode :: OutputMode,
206 idris_colourRepl :: Bool,
207 idris_colourTheme :: ColourTheme,
208 idris_errorhandlers :: [Name], -- ^ Global error handlers
209 idris_nameIdx :: (Int, Ctxt (Int, Name)),
210 idris_function_errorhandlers :: Ctxt (M.Map Name (S.Set Name)), -- ^ Specific error handlers
211 module_aliases :: M.Map [T.Text] [T.Text],
212 idris_consolewidth :: ConsoleWidth, -- ^ How many chars wide is the console?
213 idris_postulates :: S.Set Name,
214 idris_whocalls :: Maybe (M.Map Name [Name]),
215 idris_callswho :: Maybe (M.Map Name [Name]),
216 idris_repl_defs :: [Name] -- ^ List of names that were defined in the repl, and can be re-/un-defined
217 }
219-- Required for parsers library, and therefore trifecta
220instance Show IState where
221 show = const "{internal state}"
223data SizeChange = Smaller | Same | Bigger | Unknown
224 deriving (Show, Eq)
225{-!
226deriving instance Binary SizeChange
227deriving instance NFData SizeChange
228!-}
230type SCGEntry = (Name, [Maybe (Int, SizeChange)])
231type UsageReason = (Name, Int) -- fn_name, its_arg_number
233data CGInfo = CGInfo { argsdef :: [Name],
234 calls :: [(Name, [[Name]])],
235 scg :: [SCGEntry],
236 argsused :: [Name],
237 usedpos :: [(Int, [UsageReason])] }
238 deriving Show
239{-!
240deriving instance Binary CGInfo
241deriving instance NFData CGInfo
242!-}
244primDefs = [sUN "unsafePerformPrimIO",
245 sUN "mkLazyForeignPrim",
246 sUN "mkForeignPrim",
247 sUN "void"]
249-- information that needs writing for the current module's .ibc file
250data IBCWrite = IBCFix FixDecl
251 | IBCImp Name
252 | IBCStatic Name
253 | IBCClass Name
254 | IBCInstance Bool Name Name
255 | IBCDSL Name
256 | IBCData Name
257 | IBCOpt Name
258 | IBCMetavar Name
259 | IBCSyntax Syntax
260 | IBCKeyword String
261 | IBCImport FilePath
262 | IBCImportDir FilePath
263 | IBCObj Codegen FilePath
264 | IBCLib Codegen String
265 | IBCCGFlag Codegen String
266 | IBCDyLib String
267 | IBCHeader Codegen String
268 | IBCAccess Name Accessibility
269 | IBCMetaInformation Name MetaInformation
270 | IBCTotal Name Totality
271 | IBCFlags Name [FnOpt]
272 | IBCFnInfo Name FnInfo
273 | IBCTrans Name (Term, Term)
274 | IBCErrRev (Term, Term)
275 | IBCCG Name
276 | IBCDoc Name
277 | IBCCoercion Name
278 | IBCDef Name -- i.e. main context
279 | IBCNameHint (Name, Name)
280 | IBCLineApp FilePath Int PTerm
281 | IBCErrorHandler Name
282 | IBCFunctionErrorHandler Name Name Name
283 | IBCPostulate Name
284 | IBCTotCheckErr FC String
285 | IBCParsedRegion FC
286 deriving Show
288-- | The initial state for the compiler
289idrisInit :: IState
290idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext
291 emptyContext emptyContext emptyContext emptyContext
292 emptyContext emptyContext emptyContext emptyContext
293 emptyContext emptyContext emptyContext emptyContext
294 [] [] [] defaultOpts 6 [] [] [] [] emptySyntaxRules [] [] [] [] [] [] []
295 [] [] Nothing [] Nothing [] [] Nothing Nothing [] Hidden False [] Nothing [] []
296 (RawOutput stdout) True defaultTheme [] (0, emptyContext) emptyContext M.empty
297 AutomaticWidth S.empty Nothing Nothing []
299-- | The monad for the main REPL - reading and processing files and updating
300-- global state (hence the IO inner monad).
301--type Idris = WriterT [Either String (IO ())] (State IState a))
302type Idris = StateT IState (ErrorT Err IO)
304-- Commands in the REPL
306data Codegen = Via String
307-- | ViaC
308-- | ViaJava
309-- | ViaNode
310-- | ViaJavaScript
311-- | ViaLLVM
312 | Bytecode
313 deriving (Show, Eq)
315-- | REPL commands
316data Command = Quit
317 | Help
318 | Eval PTerm
319 | NewDefn [PDecl] -- ^ Each 'PDecl' should be either a type declaration (at most one) or a clause defining the same name.
320 | Undefine [Name]
321 | Check PTerm
322 | DocStr (Either Name Const)
323 | TotCheck Name
324 | Reload
325 | Load FilePath (Maybe Int) -- up to maximum line number
326 | ChangeDirectory FilePath
327 | ModImport String
328 | Edit
329 | Compile Codegen String
330 | Execute
331 | ExecVal PTerm
332 | Metavars
333 | Prove Name
334 | AddProof (Maybe Name)
335 | RmProof Name
336 | ShowProof Name
337 | Proofs
338 | Universes
339 | LogLvl Int
340 | Spec PTerm
341 | HNF PTerm
342 | TestInline PTerm
343 | Defn Name
344 | Missing Name
345 | DynamicLink FilePath
346 | ListDynamic
347 | Pattelab PTerm
348 | DebugInfo Name
349 | Search PTerm
350 | CaseSplitAt Bool Int Name
351 | AddClauseFrom Bool Int Name
352 | AddProofClauseFrom Bool Int Name
353 | AddMissing Bool Int Name
354 | MakeWith Bool Int Name
355 | MakeLemma Bool Int Name
356 | DoProofSearch Bool Bool Int Name [Name]
357 -- ^ the first bool is whether to update,
358 -- the second is whether to search recursively (i.e. for the arguments)
359 | SetOpt Opt
360 | UnsetOpt Opt
361 | NOP
362 | SetColour ColourType IdrisColour
363 | ColourOn
364 | ColourOff
365 | ListErrorHandlers
366 | SetConsoleWidth ConsoleWidth
367 | Apropos String
368 | WhoCalls Name
369 | CallsWho Name
370 | MakeDoc String -- IdrisDoc
371 | Warranty
372 | PrintDef Name
373 | PPrint OutputFmt Int PTerm
374 | TransformInfo Name
376data OutputFmt = HTMLOutput | LaTeXOutput
378data Opt = Filename String
379 | Quiet
380 | NoBanner
381 | ColourREPL Bool
382 | Ideslave
383 | IdeslaveSocket
384 | ShowLibs
385 | ShowLibdir
386 | ShowIncs
387 | NoBasePkgs
388 | NoPrelude
389 | NoBuiltins -- only for the really primitive stuff!
390 | NoREPL
391 | OLogging Int
392 | Output String
393 | TypeCase
394 | TypeInType
395 | DefaultTotal
396 | DefaultPartial
397 | WarnPartial
398 | WarnReach
399 | NoCoverage
400 | ErrContext
401 | ShowImpl
402 | Verbose
403 | Port String -- REPL TCP port
404 | IBCSubDir String
405 | ImportDir String
406 | PkgBuild String
407 | PkgInstall String
408 | PkgClean String
409 | PkgCheck String
410 | PkgREPL String
411 | PkgMkDoc String -- IdrisDoc
412 | PkgTest String
413 | WarnOnly
414 | Pkg String
415 | BCAsm String
416 | DumpDefun String
417 | DumpCases String
418 | UseCodegen Codegen
419 | OutputTy OutputType
420 | Extension LanguageExt
421 | InterpretScript String
422 | EvalExpr String
423 | TargetTriple String
424 | TargetCPU String
425 | OptLevel Int
426 | AddOpt Optimisation
427 | RemoveOpt Optimisation
428 | Client String
429 | ShowOrigErr
430 | AutoWidth -- ^ Automatically adjust terminal width
431 | AutoSolve -- ^ Automatically issue "solve" tactic in interactive prover
432 deriving (Show, Eq)
434-- Parsed declarations
436data Fixity = Infixl { prec :: Int }
437 | Infixr { prec :: Int }
438 | InfixN { prec :: Int }
439 | PrefixN { prec :: Int }
440 deriving Eq
441{-!
442deriving instance Binary Fixity
443deriving instance NFData Fixity
444!-}
446instance Show Fixity where
447 show (Infixl i) = "infixl " ++ show i
448 show (Infixr i) = "infixr " ++ show i
449 show (InfixN i) = "infix " ++ show i
450 show (PrefixN i) = "prefix " ++ show i
452data FixDecl = Fix Fixity String
453 deriving Eq
455instance Show FixDecl where
456 show (Fix f s) = show f ++ " " ++ s
458{-!
459deriving instance Binary FixDecl
460deriving instance NFData FixDecl
461!-}
463instance Ord FixDecl where
464 compare (Fix x _) (Fix y _) = compare (prec x) (prec y)
467data Static = Static | Dynamic
468 deriving (Show, Eq)
469{-!
470deriving instance Binary Static
471deriving instance NFData Static
472!-}
474-- Mark bindings with their explicitness, and laziness
475data Plicity = Imp { pargopts :: [ArgOpt],
476 pstatic :: Static,
477 pparam :: Bool }
478 | Exp { pargopts :: [ArgOpt],
479 pstatic :: Static,
480 pparam :: Bool } -- this is a param (rather than index)
481 | Constraint { pargopts :: [ArgOpt],
482 pstatic :: Static }
483 | TacImp { pargopts :: [ArgOpt],
484 pstatic :: Static,
485 pscript :: PTerm }
486 deriving (Show, Eq)
488{-!
489deriving instance Binary Plicity
490deriving instance NFData Plicity
491!-}
493impl = Imp [] Dynamic False
494expl = Exp [] Dynamic False
495expl_param = Exp [] Dynamic True
496constraint = Constraint [] Static
497tacimpl t = TacImp [] Dynamic t
499data FnOpt = Inlinable -- always evaluate when simplifying
500 | TotalFn | PartialFn | CoveringFn
501 | Coinductive | AssertTotal
502 | Dictionary -- type class dictionary, eval only when
503 -- a function argument, and further evaluation resutls
504 | Implicit -- implicit coercion
505 | NoImplicit -- do not apply implicit coercions
506 | CExport String -- export, with a C name
507 | ErrorHandler -- ^^ an error handler for use with the ErrorReflection extension
508 | ErrorReverse -- ^^ attempt to reverse normalise before showing in error
509 | Reflection -- a reflecting function, compile-time only
510 | Specialise [(Name, Maybe Int)] -- specialise it, freeze these names
511 | Constructor -- Data constructor type
512 deriving (Show, Eq)
513{-!
514deriving instance Binary FnOpt
515deriving instance NFData FnOpt
516!-}
518type FnOpts = [FnOpt]
520inlinable :: FnOpts -> Bool
521inlinable = elem Inlinable
523dictionary :: FnOpts -> Bool
524dictionary = elem Dictionary
527-- | Data declaration options
528data DataOpt = Codata -- ^ Set if the the data-type is coinductive
529 | DefaultEliminator -- ^ Set if an eliminator should be generated for data type
530 | DefaultCaseFun -- ^ Set if a case function should be generated for data type
531 | DataErrRev
532 deriving (Show, Eq)
534type DataOpts = [DataOpt]
536-- | Type provider - what to provide
537data ProvideWhat' t = ProvTerm t t -- ^ the first is the goal type, the second is the term
538 | ProvPostulate t -- ^ goal type must be Type, so only term
539 deriving (Show, Eq, Functor)
541type ProvideWhat = ProvideWhat' PTerm
543-- | Top-level declarations such as compiler directives, definitions,
544-- datatypes and typeclasses.
545data PDecl' t
546 = PFix FC Fixity [String] -- ^ Fixity declaration
547 | PTy (Docstring (Either Err PTerm)) [(Name, Docstring (Either Err PTerm))] SyntaxInfo FC FnOpts Name t -- ^ Type declaration
548 | PPostulate (Docstring (Either Err PTerm)) SyntaxInfo FC FnOpts Name t -- ^ Postulate
549 | PClauses FC FnOpts Name [PClause' t] -- ^ Pattern clause
550 | PCAF FC Name t -- ^ Top level constant
551 | PData (Docstring (Either Err PTerm)) [(Name, Docstring (Either Err PTerm))] SyntaxInfo FC DataOpts (PData' t) -- ^ Data declaration.
552 | PParams FC [(Name, t)] [PDecl' t] -- ^ Params block
553 | PNamespace String [PDecl' t] -- ^ New namespace
554 | PRecord (Docstring (Either Err PTerm)) SyntaxInfo FC Name t DataOpts (Docstring (Either Err PTerm)) Name t -- ^ Record declaration
555 | PClass (Docstring (Either Err PTerm)) SyntaxInfo FC
556 [t] -- constraints
557 Name
558 [(Name, t)] -- parameters
559 [(Name, Docstring (Either Err PTerm))] -- parameter docstrings
560 [PDecl' t] -- declarations
561 -- ^ Type class: arguments are documentation, syntax info, source location, constraints,
562 -- class name, parameters, method declarations
563 | PInstance SyntaxInfo FC [t] -- constraints
564 Name -- class
565 [t] -- parameters
566 t -- full instance type
567 (Maybe Name) -- explicit name
568 [PDecl' t]
569 -- ^ Instance declaration: arguments are syntax info, source location, constraints,
570 -- class name, parameters, full instance type, optional explicit name, and definitions
571 | PDSL Name (DSL' t) -- ^ DSL declaration
572 | PSyntax FC Syntax -- ^ Syntax definition
573 | PMutual FC [PDecl' t] -- ^ Mutual block
574 | PDirective (Idris ()) -- ^ Compiler directive. The parser inserts the corresponding action in the Idris monad.
575 | PProvider SyntaxInfo FC (ProvideWhat' t) Name -- ^ Type provider. The first t is the type, the second is the term
576 | PTransform FC Bool t t -- ^ Source-to-source transformation rule. If
577 -- bool is True, lhs and rhs must be convertible
578 deriving Functor
579{-!
580deriving instance Binary PDecl'
581deriving instance NFData PDecl'
582!-}
584-- For elaborator state
585type ElabD a = Elab' [PDecl] a
587-- | One clause of a top-level definition. Term arguments to constructors are:
588--
589-- 1. The whole application (missing for PClauseR and PWithR because they're within a "with" clause)
590--
591-- 2. The list of extra 'with' patterns
592--
593-- 3. The right-hand side
594--
595-- 4. The where block (PDecl' t)
597data PClause' t = PClause FC Name t [t] t [PDecl' t] -- ^ A normal top-level definition.
598 | PWith FC Name t [t] t [PDecl' t]
599 | PClauseR FC [t] t [PDecl' t]
600 | PWithR FC [t] t [PDecl' t]
601 deriving Functor
602{-!
603deriving instance Binary PClause'
604deriving instance NFData PClause'
605!-}
607-- | Data declaration
608data PData' t = PDatadecl { d_name :: Name, -- ^ The name of the datatype
609 d_tcon :: t, -- ^ Type constructor
610 d_cons :: [(Docstring (Either Err PTerm), [(Name, Docstring (Either Err PTerm))], Name, t, FC, [Name])] -- ^ Constructors
611 }
612 -- ^ Data declaration
613 | PLaterdecl { d_name :: Name, d_tcon :: t }
614 -- ^ "Placeholder" for data whose constructors are defined later
615 deriving Functor
616{-!
617deriving instance Binary PData'
618deriving instance NFData PData'
619!-}
621-- Handy to get a free function for applying PTerm -> PTerm functions
622-- across a program, by deriving Functor
624type PDecl = PDecl' PTerm
625type PData = PData' PTerm
626type PClause = PClause' PTerm
628-- get all the names declared in a decl
630declared :: PDecl -> [Name]
631declared (PFix _ _ _) = []
632declared (PTy _ _ _ _ _ n t) = [n]
633declared (PPostulate _ _ _ _ n t) = [n]
634declared (PClauses _ _ n _) = [] -- not a declaration
635declared (PCAF _ n _) = [n]
636declared (PData _ _ _ _ _ (PDatadecl n _ ts)) = n : map fstt ts
637 where fstt (_, _, a, _, _, _) = a
638declared (PData _ _ _ _ _ (PLaterdecl n _)) = [n]
639declared (PParams _ _ ds) = concatMap declared ds
640declared (PNamespace _ ds) = concatMap declared ds
641declared (PRecord _ _ _ n _ _ _ c _) = [n, c]
642declared (PClass _ _ _ _ n _ _ ms) = n : concatMap declared ms
643declared (PInstance _ _ _ _ _ _ _ _) = []
644declared (PDSL n _) = [n]
645declared (PSyntax _ _) = []
646declared (PMutual _ ds) = concatMap declared ds
647declared (PDirective _) = []
649-- get the names declared, not counting nested parameter blocks
650tldeclared :: PDecl -> [Name]
651tldeclared (PFix _ _ _) = []
652tldeclared (PTy _ _ _ _ _ n t) = [n]
653tldeclared (PPostulate _ _ _ _ n t) = [n]
654tldeclared (PClauses _ _ n _) = [] -- not a declaration
655tldeclared (PRecord _ _ _ n _ _ _ c _) = [n, c]
656tldeclared (PData _ _ _ _ _ (PDatadecl n _ ts)) = n : map fstt ts
657 where fstt (_, _, a, _, _, _) = a
658tldeclared (PParams _ _ ds) = []
659tldeclared (PMutual _ ds) = concatMap tldeclared ds
660tldeclared (PNamespace _ ds) = concatMap tldeclared ds
661tldeclared (PClass _ _ _ _ n _ _ ms) = concatMap tldeclared ms
662tldeclared (PInstance _ _ _ _ _ _ _ _) = []
663tldeclared _ = []
665defined :: PDecl -> [Name]
666defined (PFix _ _ _) = []
667defined (PTy _ _ _ _ _ n t) = []
668defined (PPostulate _ _ _ _ n t) = []
669defined (PClauses _ _ n _) = [n] -- not a declaration
670defined (PCAF _ n _) = [n]
671defined (PData _ _ _ _ _ (PDatadecl n _ ts)) = n : map fstt ts
672 where fstt (_, _, a, _, _, _) = a
673defined (PData _ _ _ _ _ (PLaterdecl n _)) = []
674defined (PParams _ _ ds) = concatMap defined ds
675defined (PNamespace _ ds) = concatMap defined ds
676defined (PRecord _ _ _ n _ _ _ c _) = [n, c]
677defined (PClass _ _ _ _ n _ _ ms) = n : concatMap defined ms
678defined (PInstance _ _ _ _ _ _ _ _) = []
679defined (PDSL n _) = [n]
680defined (PSyntax _ _) = []
681defined (PMutual _ ds) = concatMap defined ds
682defined (PDirective _) = []
683--defined _ = []
685updateN :: [(Name, Name)] -> Name -> Name
686updateN ns n | Just n' <- lookup n ns = n'
687updateN _ n = n
689updateNs :: [(Name, Name)] -> PTerm -> PTerm
690updateNs [] t = t
691updateNs ns t = mapPT updateRef t
692 where updateRef (PRef fc f) = PRef fc (updateN ns f)
693 updateRef t = t
695-- updateDNs :: [(Name, Name)] -> PDecl -> PDecl
696-- updateDNs [] t = t
697-- updateDNs ns (PTy s f n t) | Just n' <- lookup n ns = PTy s f n' t
698-- updateDNs ns (PClauses f n c) | Just n' <- lookup n ns = PClauses f n' (map updateCNs c)
699-- where updateCNs ns (PClause n l ts r ds)
700-- = PClause (updateN ns n) (fmap (updateNs ns) l)
701-- (map (fmap (updateNs ns)) ts)
702-- (fmap (updateNs ns) r)
703-- (map (updateDNs ns) ds)
704-- updateDNs ns c = c
706data PunInfo = IsType | IsTerm | TypeOrTerm deriving (Eq, Show)
708-- | High level language terms
709data PTerm = PQuote Raw -- ^ Inclusion of a core term into the high-level language
710 | PRef FC Name -- ^ A reference to a variable
711 | PInferRef FC Name -- ^ A name to be defined later
712 | PPatvar FC Name -- ^ A pattern variable
713 | PLam Name PTerm PTerm -- ^ A lambda abstraction
714 | PPi Plicity Name PTerm PTerm -- ^ (n : t1) -> t2
715 | PLet Name PTerm PTerm PTerm -- ^ A let binding
716 | PTyped PTerm PTerm -- ^ Term with explicit type
717 | PApp FC PTerm [PArg] -- ^ e.g. IO (), List Char, length x
718 | PAppBind FC PTerm [PArg] -- ^ implicitly bound application
719 | PMatchApp FC Name -- ^ Make an application by type matching
720 | PCase FC PTerm [(PTerm, PTerm)] -- ^ A case expression. Args are source location, scrutinee, and a list of pattern/RHS pairs
721 | PTrue FC PunInfo -- ^ Unit type..?
722 | PRefl FC PTerm -- ^ The canonical proof of the equality type
723 | PResolveTC FC -- ^ Solve this dictionary by type class resolution
724 | PEq FC PTerm PTerm PTerm PTerm -- ^ Heterogeneous equality type: A = B
725 | PRewrite FC PTerm PTerm (Maybe PTerm) -- ^ "rewrite" syntax, with optional result type
726 | PPair FC PunInfo PTerm PTerm -- ^ A pair (a, b) and whether it's a product type or a pair (solved by elaboration)
727 | PDPair FC PunInfo PTerm PTerm PTerm -- ^ A dependent pair (tm : a ** b) and whether it's a sigma type or a pair that inhabits one (solved by elaboration)
728 | PAlternative Bool [PTerm] -- ^ True if only one may work. (| A, B, C|)
729 | PHidden PTerm -- ^ Irrelevant or hidden pattern
730 | PType -- ^ 'Type' type
731 | PUniverse Universe -- ^ Some universe
732 | PGoal FC PTerm Name PTerm -- ^ quoteGoal, used for %reflection functions
733 | PConstant Const -- ^ Builtin types
734 | Placeholder -- ^ Underscore
735 | PDoBlock [PDo] -- ^ Do notation
736 | PIdiom FC PTerm -- ^ Idiom brackets
737 | PReturn FC
738 | PMetavar Name -- ^ A metavariable, ?name
739 | PProof [PTactic] -- ^ Proof script
740 | PTactics [PTactic] -- ^ As PProof, but no auto solving
741 | PElabError Err -- ^ Error to report on elaboration
742 | PImpossible -- ^ Special case for declaring when an LHS can't typecheck
743 | PCoerced PTerm -- ^ To mark a coerced argument, so as not to coerce twice
744 | PDisamb [[T.Text]] PTerm -- ^ Preferences for explicit namespaces
745 | PUnifyLog PTerm -- ^ dump a trace of unifications when building term
746 | PNoImplicits PTerm -- ^ never run implicit converions on the term
747 | PQuasiquote PTerm (Maybe PTerm) -- ^ `(Term [: Term])
748 | PUnquote PTerm -- ^ ,Term
749 deriving Eq
752{-!
753deriving instance Binary PTerm
754deriving instance NFData PTerm
755!-}
757mapPT :: (PTerm -> PTerm) -> PTerm -> PTerm
758mapPT f t = f (mpt t) where
759 mpt (PLam n t s) = PLam n (mapPT f t) (mapPT f s)
760 mpt (PPi p n t s) = PPi p n (mapPT f t) (mapPT f s)
761 mpt (PLet n ty v s) = PLet n (mapPT f ty) (mapPT f v) (mapPT f s)
762 mpt (PRewrite fc t s g) = PRewrite fc (mapPT f t) (mapPT f s)
763 (fmap (mapPT f) g)
764 mpt (PApp fc t as) = PApp fc (mapPT f t) (map (fmap (mapPT f)) as)
765 mpt (PAppBind fc t as) = PAppBind fc (mapPT f t) (map (fmap (mapPT f)) as)
766 mpt (PCase fc c os) = PCase fc (mapPT f c) (map (pmap (mapPT f)) os)
767 mpt (PEq fc lt rt l r) = PEq fc (mapPT f lt) (mapPT f rt) (mapPT f l) (mapPT f r)
768 mpt (PTyped l r) = PTyped (mapPT f l) (mapPT f r)
769 mpt (PPair fc p l r) = PPair fc p (mapPT f l) (mapPT f r)
770 mpt (PDPair fc p l t r) = PDPair fc p (mapPT f l) (mapPT f t) (mapPT f r)
771 mpt (PAlternative a as) = PAlternative a (map (mapPT f) as)
772 mpt (PHidden t) = PHidden (mapPT f t)
773 mpt (PDoBlock ds) = PDoBlock (map (fmap (mapPT f)) ds)
774 mpt (PProof ts) = PProof (map (fmap (mapPT f)) ts)
775 mpt (PTactics ts) = PTactics (map (fmap (mapPT f)) ts)
776 mpt (PUnifyLog tm) = PUnifyLog (mapPT f tm)
777 mpt (PDisamb ns tm) = PDisamb ns (mapPT f tm)
778 mpt (PNoImplicits tm) = PNoImplicits (mapPT f tm)
779 mpt (PGoal fc r n sc) = PGoal fc (mapPT f r) n (mapPT f sc)
780 mpt x = x
783data PTactic' t = Intro [Name] | Intros | Focus Name
784 | Refine Name [Bool] | Rewrite t | DoUnify
785 | Induction t
786 | CaseTac t
787 | Equiv t
788 | MatchRefine Name
789 | LetTac Name t | LetTacTy Name t t
790 | Exact t | Compute | Trivial | TCInstance
791 | ProofSearch Bool Bool Int (Maybe Name) [Name]
792 -- ^ the bool is whether to search recursively
793 | Solve
794 | Attack
795 | ProofState | ProofTerm | Undo
796 | Try (PTactic' t) (PTactic' t)
797 | TSeq (PTactic' t) (PTactic' t)
798 | ApplyTactic t -- see Language.Reflection module
799 | ByReflection t
800 | Reflect t
801 | Fill t
802 | GoalType String (PTactic' t)
803 | TCheck t
804 | TEval t
805 | TDocStr (Either Name Const)
806 | TSearch t
807 | Skip
808 | TFail [ErrorReportPart]
809 | Qed | Abandon
810 deriving (Show, Eq, Functor, Foldable, Traversable)
811{-!
812deriving instance Binary PTactic'
813deriving instance NFData PTactic'
814!-}
815instance Sized a => Sized (PTactic' a) where
816 size (Intro nms) = 1 + size nms
817 size Intros = 1
818 size (Focus nm) = 1 + size nm
819 size (Refine nm bs) = 1 + size nm + length bs
820 size (Rewrite t) = 1 + size t
821 size (Induction t) = 1 + size t
822 size (LetTac nm t) = 1 + size nm + size t
823 size (Exact t) = 1 + size t
824 size Compute = 1
825 size Trivial = 1
826 size Solve = 1
827 size Attack = 1
828 size ProofState = 1
829 size ProofTerm = 1
830 size Undo = 1
831 size (Try l r) = 1 + size l + size r
832 size (TSeq l r) = 1 + size l + size r
833 size (ApplyTactic t) = 1 + size t
834 size (Reflect t) = 1 + size t
835 size (Fill t) = 1 + size t
836 size Qed = 1
837 size Abandon = 1
838 size Skip = 1
839 size (TFail ts) = 1 + size ts
841type PTactic = PTactic' PTerm
843data PDo' t = DoExp FC t
844 | DoBind FC Name t
845 | DoBindP FC t t [(t,t)]
846 | DoLet FC Name t t
847 | DoLetP FC t t
848 deriving (Eq, Functor)
849{-!
850deriving instance Binary PDo'
851deriving instance NFData PDo'
852!-}
854instance Sized a => Sized (PDo' a) where
855 size (DoExp fc t) = 1 + size fc + size t
856 size (DoBind fc nm t) = 1 + size fc + size nm + size t
857 size (DoBindP fc l r alts) = 1 + size fc + size l + size r + size alts
858 size (DoLet fc nm l r) = 1 + size fc + size nm + size l + size r
859 size (DoLetP fc l r) = 1 + size fc + size l + size r
861type PDo = PDo' PTerm
863-- The priority gives a hint as to elaboration order. Best to elaborate
864-- things early which will help give a more concrete type to other
865-- variables, e.g. a before (interpTy a).
867data PArg' t = PImp { priority :: Int,
868 machine_inf :: Bool, -- true if the machine inferred it
869 argopts :: [ArgOpt],
870 pname :: Name, getTm :: t }
871 | PExp { priority :: Int,
872 argopts :: [ArgOpt],
873 pname :: Name,
874 getTm :: t }
875 | PConstraint { priority :: Int,
876 argopts :: [ArgOpt],
877 pname :: Name,
878 getTm :: t }
879 | PTacImplicit { priority :: Int,
880 argopts :: [ArgOpt],
881 pname :: Name,
882 getScript :: t,
883 getTm :: t }
884 deriving (Show, Eq, Functor)
886data ArgOpt = AlwaysShow | HideDisplay | InaccessibleArg
887 deriving (Show, Eq)
889instance Sized a => Sized (PArg' a) where
890 size (PImp p _ l nm trm) = 1 + size nm + size trm
891 size (PExp p l nm trm) = 1 + size nm + size trm
892 size (PConstraint p l nm trm) = 1 + size nm +size nm + size trm
893 size (PTacImplicit p l nm scr trm) = 1 + size nm + size scr + size trm
895{-!
896deriving instance Binary PArg'
897deriving instance NFData PArg'
898!-}
900pimp n t mach = PImp 1 mach [] n t
901pexp t = PExp 1 [] (sMN 0 "arg") t
902pconst t = PConstraint 1 [] (sMN 0 "carg") t
903ptacimp n s t = PTacImplicit 2 [] n s t
905type PArg = PArg' PTerm
907-- Type class data
909data ClassInfo = CI { instanceName :: Name,
910 class_methods :: [(Name, (FnOpts, PTerm))],
911 class_defaults :: [(Name, (Name, PDecl))], -- method name -> default impl
912 class_default_superclasses :: [PDecl],
913 class_params :: [Name],
914 class_instances :: [Name] }
915 deriving Show
916{-!
917deriving instance Binary ClassInfo
918deriving instance NFData ClassInfo
919!-}
921-- Type inference data
923data TIData = TIPartial -- ^ a function with a partially defined type
924 | TISolution [Term] -- ^ possible solutions to a metavariable in a type
925 deriving Show
927-- | Miscellaneous information about functions
928data FnInfo = FnInfo { fn_params :: [Int] }
929 deriving Show
930{-!
931deriving instance Binary FnInfo
932!-}
934data OptInfo = Optimise { inaccessible :: [(Int,Name)], -- includes names for error reporting
935 detaggable :: Bool }
936 deriving Show
937{-!
938deriving instance Binary OptInfo
939deriving instance NFData OptInfo
940!-}
943data TypeInfo = TI { con_names :: [Name],
944 codata :: Bool,
945 data_opts :: DataOpts,
946 param_pos :: [Int],
947 mutual_types :: [Name] }
948 deriving Show
949{-!
950deriving instance Binary TypeInfo
951deriving instance NFData TypeInfo
952!-}
954-- Syntactic sugar info
956data DSL' t = DSL { dsl_bind :: t,
957 dsl_return :: t,
958 dsl_apply :: t,
959 dsl_pure :: t,
960 dsl_var :: Maybe t,
961 index_first :: Maybe t,
962 index_next :: Maybe t,
963 dsl_lambda :: Maybe t,
964 dsl_let :: Maybe t,
965 dsl_pi :: Maybe t
966 }
967 deriving (Show, Functor)
968{-!
969deriving instance Binary DSL'
970deriving instance NFData DSL'
971!-}
973type DSL = DSL' PTerm
975data SynContext = PatternSyntax | TermSyntax | AnySyntax
976 deriving Show
977{-!
978deriving instance Binary SynContext
979deriving instance NFData SynContext
980!-}
982data Syntax = Rule [SSymbol] PTerm SynContext
983 deriving Show
985syntaxNames :: Syntax -> [Name]
986syntaxNames (Rule syms _ _) = mapMaybe ename syms
987 where ename (Keyword n) = Just n
988 ename _ = Nothing
990syntaxSymbols :: Syntax -> [SSymbol]
991syntaxSymbols (Rule ss _ _) = ss
992{-!
993deriving instance Binary Syntax
994deriving instance NFData Syntax
995!-}
997data SSymbol = Keyword Name
998 | Symbol String
999 | Binding Name
1000 | Expr Name
1001 | SimpleExpr Name
1002 deriving (Show, Eq)
1005{-!
1006deriving instance Binary SSymbol
1007deriving instance NFData SSymbol
1008!-}
1010newtype SyntaxRules = SyntaxRules { syntaxRulesList :: [Syntax] }
1012emptySyntaxRules :: SyntaxRules
1013emptySyntaxRules = SyntaxRules []
1015updateSyntaxRules :: [Syntax] -> SyntaxRules -> SyntaxRules
1016updateSyntaxRules rules (SyntaxRules sr) = SyntaxRules newRules
1017 where
1018 newRules = sortBy (ruleSort `on` syntaxSymbols) (rules ++ sr)
1020 ruleSort [] [] = EQ
1021 ruleSort [] _ = LT
1022 ruleSort _ [] = GT
1023 ruleSort (s1:ss1) (s2:ss2) =
1024 case symCompare s1 s2 of
1025 EQ -> ruleSort ss1 ss2
1026 r -> r
1028 -- Better than creating Ord instance for SSymbol since
1029 -- in general this ordering does not really make sense.
1030 symCompare (Keyword n1) (Keyword n2) = compare n1 n2
1031 symCompare (Keyword _) _ = LT
1032 symCompare (Symbol _) (Keyword _) = GT
1033 symCompare (Symbol s1) (Symbol s2) = compare s1 s2
1034 symCompare (Symbol _) _ = LT
1035 symCompare (Binding _) (Keyword _) = GT
1036 symCompare (Binding _) (Symbol _) = GT
1037 symCompare (Binding b1) (Binding b2) = compare b1 b2
1038 symCompare (Binding _) _ = LT
1039 symCompare (Expr _) (Keyword _) = GT
1040 symCompare (Expr _) (Symbol _) = GT
1041 symCompare (Expr _) (Binding _) = GT
1042 symCompare (Expr e1) (Expr e2) = compare e1 e2
1043 symCompare (Expr _) _ = LT
1044 symCompare (SimpleExpr _) (Keyword _) = GT
1045 symCompare (SimpleExpr _) (Symbol _) = GT
1046 symCompare (SimpleExpr _) (Binding _) = GT
1047 symCompare (SimpleExpr _) (Expr _) = GT
1048 symCompare (SimpleExpr e1) (SimpleExpr e2) = compare e1 e2
1050initDSL = DSL (PRef f (sUN ">>="))
1051 (PRef f (sUN "return"))
1052 (PRef f (sUN "<$>"))
1053 (PRef f (sUN "pure"))
1054 Nothing
1055 Nothing
1056 Nothing
1057 Nothing
1058 Nothing
1059 Nothing
1060 where f = fileFC "(builtin)"
1062data Using = UImplicit Name PTerm
1063 | UConstraint Name [Name]
1064 deriving (Show, Eq)
1065{-!
1066deriving instance Binary Using
1067deriving instance NFData Using
1068!-}
1070data SyntaxInfo = Syn { using :: [Using],
1071 syn_params :: [(Name, PTerm)],
1072 syn_namespace :: [String],
1073 no_imp :: [Name],
1074 decoration :: Name -> Name,
1075 inPattern :: Bool,
1076 implicitAllowed :: Bool,
1077 maxline :: Maybe Int,
1078 mut_nesting :: Int,
1079 dsl_info :: DSL,
1080 syn_in_quasiquote :: Int }
1081 deriving Show
1082{-!
1083deriving instance NFData SyntaxInfo
1084deriving instance Binary SyntaxInfo
1085!-}
1087defaultSyntax = Syn [] [] [] [] id False False Nothing 0 initDSL 0
1089expandNS :: SyntaxInfo -> Name -> Name
1090expandNS syn n@(NS _ _) = n
1091expandNS syn n = case syn_namespace syn of
1092 [] -> n
1093 xs -> sNS n xs
1096-- For inferring types of things
1098bi = fileFC "builtin"
1100inferTy = sMN 0 "__Infer"
1101inferCon = sMN 0 "__infer"
1102inferDecl = PDatadecl inferTy
1103 PType
1104 [(emptyDocstring, [], inferCon, PPi impl (sMN 0 "iType") PType (
1105 PPi expl (sMN 0 "ival") (PRef bi (sMN 0 "iType"))
1106 (PRef bi inferTy)), bi, [])]
1107inferOpts = []
1109infTerm t = PApp bi (PRef bi inferCon) [pimp (sMN 0 "iType") Placeholder True, pexp t]
1110infP = P (TCon 6 0) inferTy (TType (UVal 0))
1112getInferTerm, getInferType :: Term -> Term
1113getInferTerm (Bind n b sc) = Bind n b $ getInferTerm sc
1114getInferTerm (App (App _ _) tm) = tm
1115getInferTerm tm = tm -- error ("getInferTerm " ++ show tm)
1117getInferType (Bind n b sc) = Bind n (toTy b) $ getInferType sc
1118 where toTy (Lam t) = Pi t (TType (UVar 0))
1119 toTy (PVar t) = PVTy t
1120 toTy b = b
1121getInferType (App (App _ ty) _) = ty
1125-- Handy primitives: Unit, False, Pair, MkPair, =, mkForeign
1127primNames = [eqTy, eqCon, inferTy, inferCon]
1129unitTy = sUN "Unit"
1130unitCon = sUN "MkUnit"
1132falseDoc = fmap (const $ Msg "") . parseDocstring . T.pack $
1133 "The empty type, also known as the trivially false proposition." ++
1134 "\n\n" ++
1135 "Use `void` or `absurd` to prove anything if you have a variable " ++
1136 "of type `Void` in scope."
1137falseTy = sUN "Void"
1139pairTy = sUN "Pair"
1140pairCon = sUN "MkPair"
1142eqTy = sUN "="
1143eqCon = sUN "Refl"
1144eqDoc = fmap (const (Left $ Msg "")) . parseDocstring . T.pack $
1145 "The propositional equality type. A proof that `x` = `y`." ++
1146 "\n\n" ++
1147 "To use such a proof, pattern-match on it, and the two equal things will " ++
1148 "then need to be the _same_ pattern." ++
1149 "\n\n" ++
1150 "**Note**: Idris's equality type is potentially _heterogeneous_, which means that it " ++
1151 "is possible to state equalities between values of potentially different " ++
1152 "types. However, Idris will attempt the homogeneous case unless it fails to typecheck." ++
1153 "\n\n" ++
1154 "You may need to use `(~=~)` to explicitly request heterogeneous equality."
1156eqDecl = PDatadecl eqTy (piBindp impl [(n "A", PType), (n "B", PType)]
1157 (piBind [(n "x", PRef bi (n "A")), (n "y", PRef bi (n "B"))]
1158 PType))
1159 [(reflDoc, reflParamDoc,
1160 eqCon, PPi impl (n "A") PType (
1161 PPi impl (n "x") (PRef bi (n "A"))
1162 (PApp bi (PRef bi eqTy) [pimp (n "A") Placeholder False,
1163 pimp (n "B") Placeholder False,
1164 pexp (PRef bi (n "x")),
1165 pexp (PRef bi (n "x"))])), bi, [])]
1166 where n a = sUN a
1167 reflDoc = annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $
1168 "A proof that `x` in fact equals `x`. To construct this, you must have already " ++
1169 "shown that both sides are in fact equal."
1170 reflParamDoc = [(n "A", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the type at which the equality is proven"),
1171 (n "x", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the element shown to be equal to itself.")]
1173eqParamDoc = [(n "A", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the type of the left side of the equality"),
1174 (n "B", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the type of the right side of the equality")
1176 where n a = sUN a
1178eqOpts = []
1180-- Defined in builtins.idr
1181sigmaTy = sUN "Sigma"
1182existsCon = sUN "MkSigma"
1184piBind :: [(Name, PTerm)] -> PTerm -> PTerm
1185piBind = piBindp expl
1187piBindp :: Plicity -> [(Name, PTerm)] -> PTerm -> PTerm
1188piBindp p [] t = t
1189piBindp p ((n, ty):ns) t = PPi p n ty (piBindp p ns t)
1192-- Pretty-printing declarations and terms
1194-- These "show" instances render to an absurdly wide screen because inserted line breaks
1195-- could interfere with interactive editing, which calls "show".
1197instance Show PTerm where
1198 showsPrec _ tm = (displayS . renderPretty 1.0 10000000 . prettyImp defaultPPOption) tm
1200instance Show PDecl where
1201 showsPrec _ d = (displayS . renderPretty 1.0 10000000 . showDeclImp verbosePPOption) d
1203instance Show PClause where
1204 showsPrec _ c = (displayS . renderPretty 1.0 10000000 . showCImp verbosePPOption) c
1206instance Show PData where
1207 showsPrec _ d = (displayS . renderPretty 1.0 10000000 . showDImp defaultPPOption) d
1209instance Pretty PTerm OutputAnnotation where
1210 pretty = prettyImp defaultPPOption
1212-- | Colourise annotations according to an Idris state. It ignores the names
1213-- in the annotation, as there's no good way to show extended information on a
1214-- terminal.
1215consoleDecorate :: IState -> OutputAnnotation -> String -> String
1216consoleDecorate ist _ | not (idris_colourRepl ist) = id
1217consoleDecorate ist (AnnConst c) = let theme = idris_colourTheme ist
1218 in if constIsType c
1219 then colouriseType theme
1220 else colouriseData theme
1221consoleDecorate ist (AnnData _ _) = colouriseData (idris_colourTheme ist)
1222consoleDecorate ist (AnnType _ _) = colouriseType (idris_colourTheme ist)
1223consoleDecorate ist (AnnBoundName _ True) = colouriseImplicit (idris_colourTheme ist)
1224consoleDecorate ist (AnnBoundName _ False) = colouriseBound (idris_colourTheme ist)
1225consoleDecorate ist AnnKeyword = colouriseKeyword (idris_colourTheme ist)
1226consoleDecorate ist (AnnName n _ _ _) = let ctxt = tt_ctxt ist
1227 theme = idris_colourTheme ist
1228 in case () of
1229 _ | isDConName n ctxt -> colouriseData theme
1230 _ | isFnName n ctxt -> colouriseFun theme
1231 _ | isTConName n ctxt -> colouriseType theme
1232 _ | isPostulateName n ist -> colourisePostulate theme
1233 _ | otherwise -> id -- don't colourise unknown names
1234consoleDecorate ist (AnnFC _) = id
1235consoleDecorate ist (AnnTextFmt fmt) = Idris.Colours.colourise (colour fmt)
1236 where colour BoldText = IdrisColour Nothing True False True False
1237 colour UnderlineText = IdrisColour Nothing True True False False
1238 colour ItalicText = IdrisColour Nothing True False False True
1239consoleDecorate ist (AnnTerm _ _) = id
1240consoleDecorate ist (AnnSearchResult _) = id
1241consoleDecorate ist (AnnErr _) = id
1243isPostulateName :: Name -> IState -> Bool
1244isPostulateName n ist = S.member n (idris_postulates ist)
1246-- | Pretty-print a high-level closed Idris term with no information about precedence/associativity
1247prettyImp :: PPOption -- ^^ pretty printing options
1248 -> PTerm -- ^^ the term to pretty-print
1249 -> Doc OutputAnnotation
1250prettyImp impl = pprintPTerm impl [] [] []
1252-- | Serialise something to base64 using its Binary instance.
1254-- | Do the right thing for rendering a term in an IState
1255prettyIst :: IState -> PTerm -> Doc OutputAnnotation
1256prettyIst ist = pprintPTerm (ppOptionIst ist) [] [] (idris_infixes ist)
1258-- | Pretty-print a high-level Idris term in some bindings context with infix info
1259pprintPTerm :: PPOption -- ^^ pretty printing options
1260 -> [(Name, Bool)] -- ^^ the currently-bound names and whether they are implicit
1261 -> [Name] -- ^^ names to always show in pi, even if not used
1262 -> [FixDecl] -- ^^ Fixity declarations
1263 -> PTerm -- ^^ the term to pretty-print
1264 -> Doc OutputAnnotation
1265pprintPTerm ppo bnd docArgs infixes = prettySe 10 bnd
1266 where
1267 prettySe :: Int -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation
1268 prettySe p bnd (PQuote r) =
1269 text "![" <> pretty r <> text "]"
1270 prettySe p bnd (PPatvar fc n) = pretty n
1271 prettySe p bnd e
1272 | Just str <- slist p bnd e = str
1273 | Just n <- snat p e = annotate (AnnData "Nat" "") (text (show n))
1274 prettySe p bnd (PRef fc n) = prettyName True (ppopt_impl ppo) bnd n
1275 prettySe p bnd (PLam n ty sc) =
1276 bracket p 2 . group . align . hang 2 $
1277 text "\\" <> bindingOf n False <+> text "=>" <$>
1278 prettySe 10 ((n, False):bnd) sc
1279 prettySe p bnd (PLet n ty v sc) =
1280 bracket p 2 . group . align $
1281 kwd "let" <+> (group . align . hang 2 $ bindingOf n False <+> text "=" <$> prettySe 10 bnd v) </>
1282 kwd "in" <+> (group . align . hang 2 $ prettySe 10 ((n, False):bnd) sc)
1283 prettySe p bnd (PPi (Exp l s _) n ty sc)
1284 | n `elem` allNamesIn sc || ppopt_impl ppo || n `elem` docArgs =
1285 bracket p 2 . group $
1286 enclose lparen rparen (group . align $ bindingOf n False <+> colon <+> prettySe 10 bnd ty) <+>
1287 st <> text "->" <$> prettySe 10 ((n, False):bnd) sc
1288 | otherwise =
1289 bracket p 2 . group $
1290 group (prettySe 1 bnd ty <+> st) <> text "->" <$> group (prettySe 10 ((n, False):bnd) sc)
1291 where
1292 st =
1293 case s of
1294 Static -> text "[static]" <> space
1295 _ -> empty
1296 prettySe p bnd (PPi (Imp l s _) n ty sc)
1297 | ppopt_impl ppo =
1298 bracket p 2 $
1299 lbrace <> bindingOf n True <+> colon <+> prettySe 10 bnd ty <> rbrace <+>
1300 st <> text "->" </> prettySe 10 ((n, True):bnd) sc
1301 | otherwise = prettySe 10 ((n, True):bnd) sc
1302 where
1303 st =
1304 case s of
1305 Static -> text "[static]" <> space
1306 _ -> empty
1307 prettySe p bnd (PPi (Constraint _ _) n ty sc) =
1308 bracket p 2 $
1309 prettySe 10 bnd ty <+> text "=>" </> prettySe 10 ((n, True):bnd) sc
1310 prettySe p bnd (PPi (TacImp _ _ s) n ty sc) =
1311 bracket p 2 $
1312 lbrace <> kwd "tacimp" <+> pretty n <+> colon <+> prettySe 10 bnd ty <>
1313 rbrace <+> text "->" </> prettySe 10 ((n, True):bnd) sc
1314 prettySe p bnd (PApp _ (PRef _ f) args) -- normal names, no explicit args
1315 | UN nm <- basename f
1316 , not (ppopt_impl ppo) && null (getShowArgs args) =
1317 prettyName True (ppopt_impl ppo) bnd f
1318 prettySe p bnd (PAppBind _ (PRef _ f) [])
1319 | not (ppopt_impl ppo) = text "!" <> prettyName True (ppopt_impl ppo) bnd f
1320 prettySe p bnd (PApp _ (PRef _ op) args) -- infix operators
1321 | UN nm <- basename op
1322 , not (tnull nm) &&
1323 (not (ppopt_impl ppo)) && (not $ isAlpha (thead nm)) =
1324 case getShowArgs args of
1325 [] -> opName True
1326 [x] -> group (opName True <$> group (prettySe 0 bnd (getTm x)))
1327 [l,r] -> let precedence = fromMaybe 20 (fmap prec f)
1328 in bracket p precedence $ inFix (getTm l) (getTm r)
1329 (l@(PExp _ _ _ _) : r@(PExp _ _ _ _) : rest) ->
1330 bracket p 1 $
1331 enclose lparen rparen (inFix (getTm l) (getTm r)) <+>
1332 align (group (vsep (map (prettyArgS bnd) rest)))
1333 as -> opName True <+> align (vsep (map (prettyArgS bnd) as))
1334 where opName isPrefix = prettyName isPrefix (ppopt_impl ppo) bnd op
1335 f = getFixity (opStr op)
1336 left l = case f of
1337 Nothing -> prettySe (-1) bnd l
1338 Just (Infixl p') -> prettySe p' bnd l
1339 Just f' -> prettySe (prec f'-1) bnd l
1340 right r = case f of
1341 Nothing -> prettySe (-1) bnd r
1342 Just (Infixr p') -> prettySe p' bnd r
1343 Just f' -> prettySe (prec f'-1) bnd r
1344 inFix l r = align . group $
1345 (left l <+> opName False) <$> group (right r)
1346 prettySe p bnd (PApp _ hd@(PRef fc f) [tm]) -- symbols, like 'foo
1347 | PConstant (Idris.Core.TT.Str str) <- getTm tm,
1348 f == sUN "Symbol_" = annotate (AnnType ("'" ++ str) ("The symbol " ++ str)) $
1349 char '\'' <> prettySe 10 bnd (PRef fc (sUN str))
1350 prettySe p bnd (PApp _ f as) = -- Normal prefix applications
1351 let args = getShowArgs as
1352 fp = prettySe 1 bnd f
1353 in
1354 bracket p 1 . group $
1355 if ppopt_impl ppo
1356 then if null as
1357 then fp
1358 else fp <+> align (vsep (map (prettyArgS bnd) as))
1359 else if null args
1360 then fp
1361 else fp <+> align (vsep (map (prettyArgS bnd) args))
1362 prettySe p bnd (PCase _ scr opts) =
1363 kwd "case" <+> prettySe 10 bnd scr <+> kwd "of" <> prettyBody
1364 where
1365 prettyBody = foldr (<>) empty $ intersperse (text "|") $ map sc opts
1367 sc (l, r) = nest nestingSize $ prettySe 10 bnd l <+> text "=>" <+> prettySe 10 bnd r
1368 prettySe p bnd (PHidden tm) = text "." <> prettySe 0 bnd tm
1369 prettySe p bnd (PRefl _ _) = annName eqCon $ text "Refl"
1370 prettySe p bnd (PResolveTC _) = text "resolvetc"
1371 prettySe p bnd (PTrue _ IsType) = annName unitTy $ text "()"
1372 prettySe p bnd (PTrue _ IsTerm) = annName unitCon $ text "()"
1373 prettySe p bnd (PTrue _ TypeOrTerm) = text "()"
1374 prettySe p bnd (PEq _ lt rt l r)
1375 | ppopt_impl ppo =
1376 bracket p 1 $
1377 enclose lparen rparen eq <+>
1378 align (group (vsep (map (prettyArgS bnd)
1379 [PImp 0 False [] (sUN "A") lt,
1380 PImp 0 False [] (sUN "B") rt,
1381 PExp 0 [] (sUN "x") l,
1382 PExp 0 [] (sUN "y") r])))
1383 | otherwise =
1384 bracket p 2 . align . group $
1385 prettySe 10 bnd l <+> eq <$> group (prettySe 10 bnd r)
1386 where eq = annName eqTy (text "=")
1387 prettySe p bnd (PRewrite _ l r _) =
1388 bracket p 2 $
1389 text "rewrite" <+> prettySe 10 bnd l <+> text "in" <+> prettySe 10 bnd r
1390 prettySe p bnd (PTyped l r) =
1391 lparen <> prettySe 10 bnd l <+> colon <+> prettySe 10 bnd r <> rparen
1392 prettySe p bnd pair@(PPair _ pun _ _) -- flatten tuples to the right, like parser
1393 | Just elts <- pairElts pair = enclose (ann lparen) (ann rparen) .
1394 align . group . vsep . punctuate (ann comma) $
1395 map (prettySe 10 bnd) elts
1396 where ann = case pun of
1397 TypeOrTerm -> id
1398 IsType -> annName pairTy
1399 IsTerm -> annName pairCon
1400 prettySe p bnd (PDPair _ TypeOrTerm l t r) =
1401 lparen <> prettySe 10 bnd l <+> text "**" <+> prettySe 10 bnd r <> rparen
1402 prettySe p bnd (PDPair _ IsType (PRef _ n) t r) =
1403 annName sigmaTy lparen <>
1404 bindingOf n False <+>
1405 annName sigmaTy (text "**") <+>
1406 prettySe 10 ((n, False):bnd) r <>
1407 annName sigmaTy rparen
1408 prettySe p bnd (PDPair _ IsType l t r) =
1409 annName sigmaTy lparen <>
1410 prettySe 10 bnd l <+>
1411 annName sigmaTy (text "**") <+>
1412 prettySe 10 bnd r <>
1413 annName sigmaTy rparen
1414 prettySe p bnd (PDPair _ IsTerm l t r) =
1415 annName existsCon lparen <>
1416 prettySe 10 bnd l <+>
1417 annName existsCon (text "**") <+>
1418 prettySe 10 bnd r <>
1419 annName existsCon rparen
1420 prettySe p bnd (PAlternative a as) =
1421 lparen <> text "|" <> prettyAs <> text "|" <> rparen
1422 where
1423 prettyAs =
1424 foldr (\l -> \r -> l <+> text "," <+> r) empty $ map (prettySe 10 bnd) as
1425 prettySe p bnd PType = annotate (AnnType "Type" "The type of types") $ text "Type"
1426 prettySe p bnd (PUniverse u) = annotate (AnnType (show u) "The type of unique types") $ text (show u)
1427 prettySe p bnd (PConstant c) = annotate (AnnConst c) (text (show c))
1428 -- XXX: add pretty for tactics
1429 prettySe p bnd (PProof ts) =
1430 text "proof" <+> lbrace <> nest nestingSize (text . show $ ts) <> rbrace
1431 prettySe p bnd (PTactics ts) =
1432 text "tactics" <+> lbrace <> nest nestingSize (text . show $ ts) <> rbrace
1433 prettySe p bnd (PMetavar n) = text "?" <> pretty n
1434 prettySe p bnd (PReturn f) = kwd "return"
1435 prettySe p bnd PImpossible = kwd "impossible"
1436 prettySe p bnd Placeholder = text "_"
1437 prettySe p bnd (PDoBlock _) = text "do block pretty not implemented"
1438 prettySe p bnd (PCoerced t) = prettySe p bnd t
1439 prettySe p bnd (PElabError s) = pretty s
1440 -- Quasiquote pprinting ignores bound vars
1441 prettySe p bnd (PQuasiquote t Nothing) = text "`(" <> prettySe p [] t <> text ")"
1442 prettySe p bnd (PQuasiquote t (Just g)) = text "`(" <> prettySe p [] t <+> colon <+> prettySe p [] g <> text ")"
1443 prettySe p bnd (PUnquote t) = text "~" <> prettySe p bnd t
1445 prettySe p bnd _ = text "missing pretty-printer for term"
1447 prettyArgS bnd (PImp _ _ _ n tm) = prettyArgSi bnd (n, tm)
1448 prettyArgS bnd (PExp _ _ _ tm) = prettyArgSe bnd tm
1449 prettyArgS bnd (PConstraint _ _ _ tm) = prettyArgSc bnd tm
1450 prettyArgS bnd (PTacImplicit _ _ n _ tm) = prettyArgSti bnd (n, tm)
1452 prettyArgSe bnd arg = prettySe 0 bnd arg
1453 prettyArgSi bnd (n, val) = lbrace <> pretty n <+> text "=" <+> prettySe 10 bnd val <> rbrace
1454 prettyArgSc bnd val = lbrace <> lbrace <> prettySe 10 bnd val <> rbrace <> rbrace
1455 prettyArgSti bnd (n, val) = lbrace <> kwd "auto" <+> pretty n <+> text "=" <+> prettySe 10 bnd val <> rbrace
1457 annName :: Name -> Doc OutputAnnotation -> Doc OutputAnnotation
1458 annName n = annotate (AnnName n Nothing Nothing Nothing)
1460 opStr :: Name -> String
1461 opStr (NS n _) = opStr n
1462 opStr (UN n) = T.unpack n
1464 basename :: Name -> Name
1465 basename (NS n _) = basename n
1466 basename n = n
1468 slist' p bnd (PApp _ (PRef _ nil) _)
1469 | not (ppopt_impl ppo) && nsroot nil == sUN "Nil" = Just []
1470 slist' p bnd (PRef _ nil)
1471 | not (ppopt_impl ppo) && nsroot nil == sUN "Nil" = Just []
1472 slist' p bnd (PApp _ (PRef _ cons) args)
1473 | nsroot cons == sUN "::",
1474 (PExp {getTm=tl}):(PExp {getTm=hd}):imps <- reverse args,
1475 all isImp imps,
1476 Just tl' <- slist' p bnd tl
1477 = Just (hd:tl')
1478 where
1479 isImp (PImp {}) = True
1480 isImp _ = False
1481 slist' _ _ tm = Nothing
1483 slist p bnd e | Just es <- slist' p bnd e = Just $
1484 case es of [] -> annotate (AnnData "" "") $ text "[]"
1485 [x] -> enclose left right . group $
1486 prettySe p bnd x
1487 xs -> (enclose left right .
1488 align . group . vsep .
1489 punctuate comma .
1490 map (prettySe p bnd)) xs
1491 where left = (annotate (AnnData "" "") (text "["))
1492 right = (annotate (AnnData "" "") (text "]"))
1493 comma = (annotate (AnnData "" "") (text ","))
1494 slist _ _ _ = Nothing
1496 pairElts :: PTerm -> Maybe [PTerm]
1497 pairElts (PPair _ _ x y) | Just elts <- pairElts y = Just (x:elts)
1498 | otherwise = Just [x, y]
1499 pairElts _ = Nothing
1501 natns = "Prelude.Nat."
1503 snat p (PRef _ z)
1504 | show z == (natns++"Z") || show z == "Z" = Just 0
1505 snat p (PApp _ s [PExp {getTm=n}])
1506 | show s == (natns++"S") || show s == "S",
1507 Just n' <- snat p n
1508 = Just $ 1 + n'
1509 snat _ _ = Nothing
1511 bracket outer inner doc
1512 | inner > outer = lparen <> doc <> rparen
1513 | otherwise = doc
1515 kwd = annotate AnnKeyword . text
1517 fixities :: M.Map String Fixity
1518 fixities = M.fromList [(s, f) | (Fix f s) <- infixes]
1520 getFixity :: String -> Maybe Fixity
1521 getFixity = flip M.lookup fixities
1523-- | Pretty-printer helper for the binding site of a name
1524bindingOf :: Name -- ^^ the bound name
1525 -> Bool -- ^^ whether the name is implicit
1526 -> Doc OutputAnnotation
1527bindingOf n imp = annotate (AnnBoundName n imp) (text (show n))
1529-- | Pretty-printer helper for names that attaches the correct annotations
1530prettyName
1531 :: Bool -- ^^ whether the name should be parenthesised if it is an infix operator
1532 -> Bool -- ^^ whether to show namespaces
1533 -> [(Name, Bool)] -- ^^ the current bound variables and whether they are implicit
1534 -> Name -- ^^ the name to pprint
1535 -> Doc OutputAnnotation
1536prettyName infixParen showNS bnd n
1537 | Just imp <- lookup n bnd = annotate (AnnBoundName n imp) fullName
1538 | otherwise = annotate (AnnName n Nothing Nothing Nothing) fullName
1539 where fullName = text nameSpace <> parenthesise (text (baseName n))
1540 baseName (UN n) = T.unpack n
1541 baseName (NS n ns) = baseName n
1542 baseName (MN i s) = T.unpack s
1543 baseName other = show other
1544 nameSpace = case n of
1545 (NS n' ns) -> if showNS then (concatMap (++ ".") . map T.unpack . reverse) ns else ""
1546 _ -> ""
1547 isInfix = case baseName n of
1548 "" -> False
1549 (c : _) -> not (isAlpha c)
1550 parenthesise = if isInfix && infixParen then enclose lparen rparen else id
1553showCImp :: PPOption -> PClause -> Doc OutputAnnotation
1554showCImp ppo (PClause _ n l ws r w)
1555 = prettyImp ppo l <+> showWs ws <+> text "=" <+> prettyImp ppo r
1556 <+> text "where" <+> text (show w)
1557 where
1558 showWs [] = empty
1559 showWs (x : xs) = text "|" <+> prettyImp ppo x <+> showWs xs
1560showCImp ppo (PWith _ n l ws r w)
1561 = prettyImp ppo l <+> showWs ws <+> text "with" <+> prettyImp ppo r
1562 <+> braces (text (show w))
1563 where
1564 showWs [] = empty
1565 showWs (x : xs) = text "|" <+> prettyImp ppo x <+> showWs xs
1568showDImp :: PPOption -> PData -> Doc OutputAnnotation
1569showDImp ppo (PDatadecl n ty cons)
1570 = text "data" <+> text (show n) <+> colon <+> prettyImp ppo ty <+> text "where" <$>
1571 (indent 2 $ vsep (map (\ (_, _, n, t, _, _) -> pipe <+> prettyName True False [] n <+> colon <+> prettyImp ppo t) cons))
1573showDecls :: PPOption -> [PDecl] -> Doc OutputAnnotation
1574showDecls o ds = vsep (map (showDeclImp o) ds)
1576showDeclImp _ (PFix _ f ops) = text (show f) <+> cat (punctuate (text ",") (map text ops))
1577showDeclImp o (PTy _ _ _ _ _ n t) = text "tydecl" <+> text (showCG n) <+> colon <+> prettyImp o t
1578showDeclImp o (PClauses _ _ n cs) = text "pat" <+> text (showCG n) <+> text "\t" <+>
1579 indent 2 (vsep (map (showCImp o) cs))
1580showDeclImp o (PData _ _ _ _ _ d) = showDImp o { ppopt_impl = True } d
1581showDeclImp o (PParams _ ns ps) = text "params" <+> braces (text (show ns) <> line <> showDecls o ps <> line)
1582showDeclImp o (PNamespace n ps) = text "namespace" <+> text n <> braces (line <> showDecls o ps <> line)
1583showDeclImp _ (PSyntax _ syn) = text "syntax" <+> text (show syn)
1584showDeclImp o (PClass _ _ _ cs n ps _ ds)
1585 = text "class" <+> text (show cs) <+> text (show n) <+> text (show ps) <> line <> showDecls o ds
1586showDeclImp o (PInstance _ _ cs n _ t _ ds)
1587 = text "instance" <+> text (show cs) <+> text (show n) <+> prettyImp o t <> line <> showDecls o ds
1588showDeclImp _ _ = text "..."
1589-- showDeclImp (PImport o) = "import " ++ o
1591instance Show (Doc OutputAnnotation) where
1592 show = flip (displayS . renderCompact) ""
1594getImps :: [PArg] -> [(Name, PTerm)]
1595getImps [] = []
1596getImps (PImp _ _ _ n tm : xs) = (n, tm) : getImps xs
1597getImps (_ : xs) = getImps xs
1599getExps :: [PArg] -> [PTerm]
1600getExps [] = []
1601getExps (PExp _ _ _ tm : xs) = tm : getExps xs
1602getExps (_ : xs) = getExps xs
1604getShowArgs :: [PArg] -> [PArg]
1605getShowArgs [] = []
1606getShowArgs (e@(PExp _ _ _ tm) : xs) = e : getShowArgs xs
1607getShowArgs (e : xs) | AlwaysShow `elem` argopts e = e : getShowArgs xs
1608getShowArgs (_ : xs) = getShowArgs xs
1610getConsts :: [PArg] -> [PTerm]
1611getConsts [] = []
1612getConsts (PConstraint _ _ _ tm : xs) = tm : getConsts xs
1613getConsts (_ : xs) = getConsts xs
1615getAll :: [PArg] -> [PTerm]
1616getAll = map getTm
1619-- | Show Idris name
1620showName :: Maybe IState -- ^^ the Idris state, for information about names and colours
1621 -> [(Name, Bool)] -- ^^ the bound variables and whether they're implicit
1622 -> PPOption -- ^^ pretty printing options
1623 -> Bool -- ^^ whether to colourise
1624 -> Name -- ^^ the term to show
1625 -> String
1626showName ist bnd ppo colour n = case ist of
1627 Just i -> if colour then colourise n (idris_colourTheme i) else showbasic n
1628 Nothing -> showbasic n
1629 where name = if ppopt_impl ppo then show n else showbasic n
1630 showbasic n@(UN _) = showCG n
1631 showbasic (MN i s) = str s
1632 showbasic (NS n s) = showSep "." (map str (reverse s)) ++ "." ++ showbasic n
1633 showbasic (SN s) = show s
1634 fst3 (x, _, _) = x
1635 colourise n t = let ctxt' = fmap tt_ctxt ist in
1636 case ctxt' of
1637 Nothing -> name
1638 Just ctxt | Just impl <- lookup n bnd -> if impl then colouriseImplicit t name
1639 else colouriseBound t name
1640 | isDConName n ctxt -> colouriseData t name
1641 | isFnName n ctxt -> colouriseFun t name
1642 | isTConName n ctxt -> colouriseType t name
1643 -- The assumption is that if a name is not bound and does not exist in the
1644 -- global context, then we're somewhere in which implicit info has been lost
1645 -- (like error messages). Thus, unknown vars are colourised as implicits.
1646 | otherwise -> colouriseImplicit t name
1648showTm :: IState -- ^^ the Idris state, for information about identifiers and colours
1649 -> PTerm -- ^^ the term to show
1650 -> String
1651showTm ist = displayDecorated (consoleDecorate ist) .
1652 renderPretty 0.8 100000 .
1653 prettyImp (ppOptionIst ist)
1655-- | Show a term with implicits, no colours
1656showTmImpls :: PTerm -> String
1657showTmImpls = flip (displayS . renderCompact . prettyImp verbosePPOption) ""
1661instance Sized PTerm where
1662 size (PQuote rawTerm) = size rawTerm
1663 size (PRef fc name) = size name
1664 size (PLam name ty bdy) = 1 + size ty + size bdy
1665 size (PPi plicity name ty bdy) = 1 + size ty + size bdy
1666 size (PLet name ty def bdy) = 1 + size ty + size def + size bdy
1667 size (PTyped trm ty) = 1 + size trm + size ty
1668 size (PApp fc name args) = 1 + size args
1669 size (PAppBind fc name args) = 1 + size args
1670 size (PCase fc trm bdy) = 1 + size trm + size bdy
1671 size (PTrue fc _) = 1
1672 size (PRefl fc _) = 1
1673 size (PResolveTC fc) = 1
1674 size (PEq fc _ _ left right) = 1 + size left + size right
1675 size (PRewrite fc left right _) = 1 + size left + size right
1676 size (PPair fc _ left right) = 1 + size left + size right
1677 size (PDPair fs _ left ty right) = 1 + size left + size ty + size right
1678 size (PAlternative a alts) = 1 + size alts
1679 size (PHidden hidden) = size hidden
1680 size (PUnifyLog tm) = size tm
1681 size (PDisamb _ tm) = size tm
1682 size (PNoImplicits tm) = size tm
1683 size PType = 1
1684 size (PUniverse _) = 1
1685 size (PConstant const) = 1 + size const
1686 size Placeholder = 1
1687 size (PDoBlock dos) = 1 + size dos
1688 size (PIdiom fc term) = 1 + size term
1689 size (PReturn fc) = 1
1690 size (PMetavar name) = 1
1691 size (PProof tactics) = size tactics
1692 size (PElabError err) = size err
1693 size PImpossible = 1
1694 size _ = 0
1696getPArity :: PTerm -> Int
1697getPArity (PPi _ _ _ sc) = 1 + getPArity sc
1698getPArity _ = 0
1700-- Return all names, free or globally bound, in the given term.
1702allNamesIn :: PTerm -> [Name]
1703allNamesIn tm = nub $ ni [] tm
1704 where -- TODO THINK added niTacImp, but is it right?
1705 ni env (PRef _ n)
1706 | not (n `elem` env) = [n]
1707 ni env (PPatvar _ n) = [n]
1708 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
1709 ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
1710 ni env (PCase _ c os) = ni env c ++ concatMap (ni env) (map snd os)
1711 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc
1712 ni env (PPi p n ty sc) = niTacImp env p ++ ni env ty ++ ni (n:env) sc
1713 ni env (PHidden tm) = ni env tm
1714 ni env (PEq _ _ _ l r) = ni env l ++ ni env r
1715 ni env (PRewrite _ l r _) = ni env l ++ ni env r
1716 ni env (PTyped l r) = ni env l ++ ni env r
1717 ni env (PPair _ _ l r) = ni env l ++ ni env r
1718 ni env (PDPair _ _ (PRef _ n) t r) = ni env t ++ ni (n:env) r
1719 ni env (PDPair _ _ l t r) = ni env l ++ ni env t ++ ni env r
1720 ni env (PAlternative a ls) = concatMap (ni env) ls
1721 ni env (PUnifyLog tm) = ni env tm
1722 ni env (PDisamb _ tm) = ni env tm
1723 ni env (PNoImplicits tm) = ni env tm
1724 ni env _ = []
1726 niTacImp env (TacImp _ _ scr) = ni env scr
1727 niTacImp _ _ = []
1729-- Return all names defined in binders in the given term
1730boundNamesIn :: PTerm -> [Name]
1731boundNamesIn tm = nub $ ni tm
1732 where -- TODO THINK Added niTacImp, but is it right?
1733 ni (PApp _ f as) = ni f ++ concatMap (ni) (map getTm as)
1734 ni (PAppBind _ f as) = ni f ++ concatMap (ni) (map getTm as)
1735 ni (PCase _ c os) = ni c ++ concatMap (ni) (map snd os)
1736 ni (PLam n ty sc) = n : (ni ty ++ ni sc)
1737 ni (PLet n ty val sc) = n : (ni ty ++ ni val ++ ni sc)
1738 ni (PPi p n ty sc) = niTacImp p ++ (n : (ni ty ++ ni sc))
1739 ni (PEq _ _ _ l r) = ni l ++ ni r
1740 ni (PRewrite _ l r _) = ni l ++ ni r
1741 ni (PTyped l r) = ni l ++ ni r
1742 ni (PPair _ _ l r) = ni l ++ ni r
1743 ni (PDPair _ _ (PRef _ n) t r) = ni t ++ ni r
1744 ni (PDPair _ _ l t r) = ni l ++ ni t ++ ni r
1745 ni (PAlternative a as) = concatMap (ni) as
1746 ni (PHidden tm) = ni tm
1747 ni (PUnifyLog tm) = ni tm
1748 ni (PDisamb _ tm) = ni tm
1749 ni (PNoImplicits tm) = ni tm
1750 ni _ = []
1752 niTacImp (TacImp _ _ scr) = ni scr
1753 niTacImp _ = []
1755-- Return names which are valid implicits in the given term (type).
1756implicitNamesIn :: [Name] -> IState -> PTerm -> [Name]
1757implicitNamesIn uvars ist tm = nub $ ni [] tm
1758 where
1759 ni env (PRef _ n)
1760 | not (n `elem` env)
1761 = case lookupTy n (tt_ctxt ist) of
1762 [] -> [n]
1763 _ -> if n `elem` uvars then [n] else []
1764 ni env (PApp _ f@(PRef _ n) as)
1765 | n `elem` uvars = ni env f ++ concatMap (ni env) (map getTm as)
1766 | otherwise = concatMap (ni env) (map getTm as)
1767 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
1768 ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
1769 ni env (PCase _ c os) = ni env c ++
1770 -- names in 'os', not counting the names bound in the cases
1771 (nub (concatMap (ni env) (map snd os))
1772 \\ nub (concatMap (ni env) (map fst os)))
1773 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc
1774 ni env (PPi p n ty sc) = ni env ty ++ ni (n:env) sc
1775 ni env (PEq _ _ _ l r) = ni env l ++ ni env r
1776 ni env (PRewrite _ l r _) = ni env l ++ ni env r
1777 ni env (PTyped l r) = ni env l ++ ni env r
1778 ni env (PPair _ _ l r) = ni env l ++ ni env r
1779 ni env (PDPair _ _ (PRef _ n) t r) = ni env t ++ ni (n:env) r
1780 ni env (PDPair _ _ l t r) = ni env l ++ ni env t ++ ni env r
1781 ni env (PAlternative a as) = concatMap (ni env) as
1782 ni env (PHidden tm) = ni env tm
1783 ni env (PUnifyLog tm) = ni env tm
1784 ni env (PDisamb _ tm) = ni env tm
1785 ni env (PNoImplicits tm) = ni env tm
1786 ni env _ = []
1788-- Return names which are free in the given term.
1789namesIn :: [(Name, PTerm)] -> IState -> PTerm -> [Name]
1790namesIn uvars ist tm = nub $ ni [] tm
1791 where
1792 ni env (PRef _ n)
1793 | not (n `elem` env)
1794 = case lookupTy n (tt_ctxt ist) of
1795 [] -> [n]
1796 _ -> if n `elem` (map fst uvars) then [n] else []
1797 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
1798 ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
1799 ni env (PCase _ c os) = ni env c ++
1800 -- names in 'os', not counting the names bound in the cases
1801 (nub (concatMap (ni env) (map snd os))
1802 \\ nub (concatMap (ni env) (map fst os)))
1803 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc
1804 ni env (PPi p n ty sc) = niTacImp env p ++ ni env ty ++ ni (n:env) sc
1805 ni env (PEq _ _ _ l r) = ni env l ++ ni env r
1806 ni env (PRewrite _ l r _) = ni env l ++ ni env r
1807 ni env (PTyped l r) = ni env l ++ ni env r
1808 ni env (PPair _ _ l r) = ni env l ++ ni env r
1809 ni env (PDPair _ _ (PRef _ n) t r) = ni env t ++ ni (n:env) r
1810 ni env (PDPair _ _ l t r) = ni env l ++ ni env t ++ ni env r
1811 ni env (PAlternative a as) = concatMap (ni env) as
1812 ni env (PHidden tm) = ni env tm
1813 ni env (PUnifyLog tm) = ni env tm
1814 ni env (PDisamb _ tm) = ni env tm
1815 ni env (PNoImplicits tm) = ni env tm
1816 ni env _ = []
1818 niTacImp env (TacImp _ _ scr) = ni env scr
1819 niTacImp _ _ = []
1821-- Return which of the given names are used in the given term.
1823usedNamesIn :: [Name] -> IState -> PTerm -> [Name]
1824usedNamesIn vars ist tm = nub $ ni [] tm
1825 where -- TODO THINK added niTacImp, but is it right?
1826 ni env (PRef _ n)
1827 | n `elem` vars && not (n `elem` env)
1828 = case lookupDefExact n (tt_ctxt ist) of
1829 Nothing -> [n]
1830 _ -> []
1831 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
1832 ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
1833 ni env (PCase _ c os) = ni env c ++ concatMap (ni env) (map snd os)
1834 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc
1835 ni env (PPi p n ty sc) = niTacImp env p ++ ni env ty ++ ni (n:env) sc
1836 ni env (PEq _ _ _ l r) = ni env l ++ ni env r
1837 ni env (PRewrite _ l r _) = ni env l ++ ni env r
1838 ni env (PTyped l r) = ni env l ++ ni env r
1839 ni env (PPair _ _ l r) = ni env l ++ ni env r
1840 ni env (PDPair _ _ (PRef _ n) t r) = ni env t ++ ni (n:env) r
1841 ni env (PDPair _ _ l t r) = ni env l ++ ni env t ++ ni env r
1842 ni env (PAlternative a as) = concatMap (ni env) as
1843 ni env (PHidden tm) = ni env tm
1844 ni env (PUnifyLog tm) = ni env tm
1845 ni env (PDisamb _ tm) = ni env tm
1846 ni env (PNoImplicits tm) = ni env tm
1847 ni env _ = []
1849 niTacImp env (TacImp _ _ scr) = ni env scr
1850 niTacImp _ _ = []
1852-- Return the list of inaccessible (= dotted) positions for a name.
1853getErasureInfo :: IState -> Name -> [Int]
1854getErasureInfo ist n =
1855 case lookupCtxtExact n (idris_optimisation ist) of
1856 Just (Optimise inacc detagg) -> map fst inacc
1857 Nothing -> []