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