git.iko.soy/Idris-dev
on 9d804b5 help sign in
Idris-dev/src/Idris/AbsSyntaxTree.hs
1818 lines 74 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
15import {-# SOURCE #-} Idris.ParseExpr (SyntaxRules, emptySyntaxRules)
17import Idris.Colours
19import System.Console.Haskeline
20import System.IO
22import Control.Monad.Trans.State.Strict
23import Control.Monad.Trans.Error
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!-}
1010initDSL = DSL (PRef f (sUN ">>="))
1011 (PRef f (sUN "return"))
1012 (PRef f (sUN "<$>"))
1013 (PRef f (sUN "pure"))
1014 Nothing
1015 Nothing
1016 Nothing
1017 Nothing
1018 Nothing
1019 Nothing
1020 where f = fileFC "(builtin)"
1022data Using = UImplicit Name PTerm
1023 | UConstraint Name [Name]
1024 deriving (Show, Eq)
1025{-!
1026deriving instance Binary Using
1027deriving instance NFData Using
1028!-}
1030data SyntaxInfo = Syn { using :: [Using],
1031 syn_params :: [(Name, PTerm)],
1032 syn_namespace :: [String],
1033 no_imp :: [Name],
1034 decoration :: Name -> Name,
1035 inPattern :: Bool,
1036 implicitAllowed :: Bool,
1037 maxline :: Maybe Int,
1038 mut_nesting :: Int,
1039 dsl_info :: DSL,
1040 syn_in_quasiquote :: Int }
1041 deriving Show
1042{-!
1043deriving instance NFData SyntaxInfo
1044deriving instance Binary SyntaxInfo
1045!-}
1047defaultSyntax = Syn [] [] [] [] id False False Nothing 0 initDSL 0
1049expandNS :: SyntaxInfo -> Name -> Name
1050expandNS syn n@(NS _ _) = n
1051expandNS syn n = case syn_namespace syn of
1052 [] -> n
1053 xs -> sNS n xs
1056-- For inferring types of things
1058bi = fileFC "builtin"
1060inferTy = sMN 0 "__Infer"
1061inferCon = sMN 0 "__infer"
1062inferDecl = PDatadecl inferTy
1063 PType
1064 [(emptyDocstring, [], inferCon, PPi impl (sMN 0 "iType") PType (
1065 PPi expl (sMN 0 "ival") (PRef bi (sMN 0 "iType"))
1066 (PRef bi inferTy)), bi, [])]
1067inferOpts = []
1069infTerm t = PApp bi (PRef bi inferCon) [pimp (sMN 0 "iType") Placeholder True, pexp t]
1070infP = P (TCon 6 0) inferTy (TType (UVal 0))
1072getInferTerm, getInferType :: Term -> Term
1073getInferTerm (Bind n b sc) = Bind n b $ getInferTerm sc
1074getInferTerm (App (App _ _) tm) = tm
1075getInferTerm tm = tm -- error ("getInferTerm " ++ show tm)
1077getInferType (Bind n b sc) = Bind n (toTy b) $ getInferType sc
1078 where toTy (Lam t) = Pi t (TType (UVar 0))
1079 toTy (PVar t) = PVTy t
1080 toTy b = b
1081getInferType (App (App _ ty) _) = ty
1085-- Handy primitives: Unit, False, Pair, MkPair, =, mkForeign
1087primNames = [eqTy, eqCon, inferTy, inferCon]
1089unitTy = sUN "Unit"
1090unitCon = sUN "MkUnit"
1092falseDoc = fmap (const $ Msg "") . parseDocstring . T.pack $
1093 "The empty type, also known as the trivially false proposition." ++
1094 "\n\n" ++
1095 "Use `void` or `absurd` to prove anything if you have a variable " ++
1096 "of type `Void` in scope."
1097falseTy = sUN "Void"
1099pairTy = sUN "Pair"
1100pairCon = sUN "MkPair"
1102eqTy = sUN "="
1103eqCon = sUN "Refl"
1104eqDoc = fmap (const (Left $ Msg "")) . parseDocstring . T.pack $
1105 "The propositional equality type. A proof that `x` = `y`." ++
1106 "\n\n" ++
1107 "To use such a proof, pattern-match on it, and the two equal things will " ++
1108 "then need to be the _same_ pattern." ++
1109 "\n\n" ++
1110 "**Note**: Idris's equality type is potentially _heterogeneous_, which means that it " ++
1111 "is possible to state equalities between values of potentially different " ++
1112 "types. However, Idris will attempt the homogeneous case unless it fails to typecheck." ++
1113 "\n\n" ++
1114 "You may need to use `(~=~)` to explicitly request heterogeneous equality."
1116eqDecl = PDatadecl eqTy (piBindp impl [(n "A", PType), (n "B", PType)]
1117 (piBind [(n "x", PRef bi (n "A")), (n "y", PRef bi (n "B"))]
1118 PType))
1119 [(reflDoc, reflParamDoc,
1120 eqCon, PPi impl (n "A") PType (
1121 PPi impl (n "x") (PRef bi (n "A"))
1122 (PApp bi (PRef bi eqTy) [pimp (n "A") Placeholder False,
1123 pimp (n "B") Placeholder False,
1124 pexp (PRef bi (n "x")),
1125 pexp (PRef bi (n "x"))])), bi, [])]
1126 where n a = sUN a
1127 reflDoc = annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $
1128 "A proof that `x` in fact equals `x`. To construct this, you must have already " ++
1129 "shown that both sides are in fact equal."
1130 reflParamDoc = [(n "A", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the type at which the equality is proven"),
1131 (n "x", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the element shown to be equal to itself.")]
1133eqParamDoc = [(n "A", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the type of the left side of the equality"),
1134 (n "B", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the type of the right side of the equality")
1136 where n a = sUN a
1138eqOpts = []
1140-- Defined in builtins.idr
1141sigmaTy = sUN "Sigma"
1142existsCon = sUN "MkSigma"
1144piBind :: [(Name, PTerm)] -> PTerm -> PTerm
1145piBind = piBindp expl
1147piBindp :: Plicity -> [(Name, PTerm)] -> PTerm -> PTerm
1148piBindp p [] t = t
1149piBindp p ((n, ty):ns) t = PPi p n ty (piBindp p ns t)
1152-- Pretty-printing declarations and terms
1154-- These "show" instances render to an absurdly wide screen because inserted line breaks
1155-- could interfere with interactive editing, which calls "show".
1157instance Show PTerm where
1158 showsPrec _ tm = (displayS . renderPretty 1.0 10000000 . prettyImp defaultPPOption) tm
1160instance Show PDecl where
1161 showsPrec _ d = (displayS . renderPretty 1.0 10000000 . showDeclImp verbosePPOption) d
1163instance Show PClause where
1164 showsPrec _ c = (displayS . renderPretty 1.0 10000000 . showCImp verbosePPOption) c
1166instance Show PData where
1167 showsPrec _ d = (displayS . renderPretty 1.0 10000000 . showDImp defaultPPOption) d
1169instance Pretty PTerm OutputAnnotation where
1170 pretty = prettyImp defaultPPOption
1172-- | Colourise annotations according to an Idris state. It ignores the names
1173-- in the annotation, as there's no good way to show extended information on a
1174-- terminal.
1175consoleDecorate :: IState -> OutputAnnotation -> String -> String
1176consoleDecorate ist _ | not (idris_colourRepl ist) = id
1177consoleDecorate ist (AnnConst c) = let theme = idris_colourTheme ist
1178 in if constIsType c
1179 then colouriseType theme
1180 else colouriseData theme
1181consoleDecorate ist (AnnData _ _) = colouriseData (idris_colourTheme ist)
1182consoleDecorate ist (AnnType _ _) = colouriseType (idris_colourTheme ist)
1183consoleDecorate ist (AnnBoundName _ True) = colouriseImplicit (idris_colourTheme ist)
1184consoleDecorate ist (AnnBoundName _ False) = colouriseBound (idris_colourTheme ist)
1185consoleDecorate ist AnnKeyword = colouriseKeyword (idris_colourTheme ist)
1186consoleDecorate ist (AnnName n _ _ _) = let ctxt = tt_ctxt ist
1187 theme = idris_colourTheme ist
1188 in case () of
1189 _ | isDConName n ctxt -> colouriseData theme
1190 _ | isFnName n ctxt -> colouriseFun theme
1191 _ | isTConName n ctxt -> colouriseType theme
1192 _ | isPostulateName n ist -> colourisePostulate theme
1193 _ | otherwise -> id -- don't colourise unknown names
1194consoleDecorate ist (AnnFC _) = id
1195consoleDecorate ist (AnnTextFmt fmt) = Idris.Colours.colourise (colour fmt)
1196 where colour BoldText = IdrisColour Nothing True False True False
1197 colour UnderlineText = IdrisColour Nothing True True False False
1198 colour ItalicText = IdrisColour Nothing True False False True
1199consoleDecorate ist (AnnTerm _ _) = id
1200consoleDecorate ist (AnnSearchResult _) = id
1201consoleDecorate ist (AnnErr _) = id
1203isPostulateName :: Name -> IState -> Bool
1204isPostulateName n ist = S.member n (idris_postulates ist)
1206-- | Pretty-print a high-level closed Idris term with no information about precedence/associativity
1207prettyImp :: PPOption -- ^^ pretty printing options
1208 -> PTerm -- ^^ the term to pretty-print
1209 -> Doc OutputAnnotation
1210prettyImp impl = pprintPTerm impl [] [] []
1212-- | Serialise something to base64 using its Binary instance.
1214-- | Do the right thing for rendering a term in an IState
1215prettyIst :: IState -> PTerm -> Doc OutputAnnotation
1216prettyIst ist = pprintPTerm (ppOptionIst ist) [] [] (idris_infixes ist)
1218-- | Pretty-print a high-level Idris term in some bindings context with infix info
1219pprintPTerm :: PPOption -- ^^ pretty printing options
1220 -> [(Name, Bool)] -- ^^ the currently-bound names and whether they are implicit
1221 -> [Name] -- ^^ names to always show in pi, even if not used
1222 -> [FixDecl] -- ^^ Fixity declarations
1223 -> PTerm -- ^^ the term to pretty-print
1224 -> Doc OutputAnnotation
1225pprintPTerm ppo bnd docArgs infixes = prettySe 10 bnd
1226 where
1227 prettySe :: Int -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation
1228 prettySe p bnd (PQuote r) =
1229 text "![" <> pretty r <> text "]"
1230 prettySe p bnd (PPatvar fc n) = pretty n
1231 prettySe p bnd e
1232 | Just str <- slist p bnd e = str
1233 | Just n <- snat p e = annotate (AnnData "Nat" "") (text (show n))
1234 prettySe p bnd (PRef fc n) = prettyName True (ppopt_impl ppo) bnd n
1235 prettySe p bnd (PLam n ty sc) =
1236 bracket p 2 . group . align . hang 2 $
1237 text "\\" <> bindingOf n False <+> text "=>" <$>
1238 prettySe 10 ((n, False):bnd) sc
1239 prettySe p bnd (PLet n ty v sc) =
1240 bracket p 2 . group . align $
1241 kwd "let" <+> (group . align . hang 2 $ bindingOf n False <+> text "=" <$> prettySe 10 bnd v) </>
1242 kwd "in" <+> (group . align . hang 2 $ prettySe 10 ((n, False):bnd) sc)
1243 prettySe p bnd (PPi (Exp l s _) n ty sc)
1244 | n `elem` allNamesIn sc || ppopt_impl ppo || n `elem` docArgs =
1245 bracket p 2 . group $
1246 enclose lparen rparen (group . align $ bindingOf n False <+> colon <+> prettySe 10 bnd ty) <+>
1247 st <> text "->" <$> prettySe 10 ((n, False):bnd) sc
1248 | otherwise =
1249 bracket p 2 . group $
1250 group (prettySe 1 bnd ty <+> st) <> text "->" <$> group (prettySe 10 ((n, False):bnd) sc)
1251 where
1252 st =
1253 case s of
1254 Static -> text "[static]" <> space
1255 _ -> empty
1256 prettySe p bnd (PPi (Imp l s _) n ty sc)
1257 | ppopt_impl ppo =
1258 bracket p 2 $
1259 lbrace <> bindingOf n True <+> colon <+> prettySe 10 bnd ty <> rbrace <+>
1260 st <> text "->" </> prettySe 10 ((n, True):bnd) sc
1261 | otherwise = prettySe 10 ((n, True):bnd) sc
1262 where
1263 st =
1264 case s of
1265 Static -> text "[static]" <> space
1266 _ -> empty
1267 prettySe p bnd (PPi (Constraint _ _) n ty sc) =
1268 bracket p 2 $
1269 prettySe 10 bnd ty <+> text "=>" </> prettySe 10 ((n, True):bnd) sc
1270 prettySe p bnd (PPi (TacImp _ _ s) n ty sc) =
1271 bracket p 2 $
1272 lbrace <> kwd "tacimp" <+> pretty n <+> colon <+> prettySe 10 bnd ty <>
1273 rbrace <+> text "->" </> prettySe 10 ((n, True):bnd) sc
1274 prettySe p bnd (PApp _ (PRef _ f) args) -- normal names, no explicit args
1275 | UN nm <- basename f
1276 , not (ppopt_impl ppo) && null (getShowArgs args) =
1277 prettyName True (ppopt_impl ppo) bnd f
1278 prettySe p bnd (PAppBind _ (PRef _ f) [])
1279 | not (ppopt_impl ppo) = text "!" <> prettyName True (ppopt_impl ppo) bnd f
1280 prettySe p bnd (PApp _ (PRef _ op) args) -- infix operators
1281 | UN nm <- basename op
1282 , not (tnull nm) &&
1283 (not (ppopt_impl ppo)) && (not $ isAlpha (thead nm)) =
1284 case getShowArgs args of
1285 [] -> opName True
1286 [x] -> group (opName True <$> group (prettySe 0 bnd (getTm x)))
1287 [l,r] -> let precedence = fromMaybe 20 (fmap prec f)
1288 in bracket p precedence $ inFix (getTm l) (getTm r)
1289 (l@(PExp _ _ _ _) : r@(PExp _ _ _ _) : rest) ->
1290 bracket p 1 $
1291 enclose lparen rparen (inFix (getTm l) (getTm r)) <+>
1292 align (group (vsep (map (prettyArgS bnd) rest)))
1293 as -> opName True <+> align (vsep (map (prettyArgS bnd) as))
1294 where opName isPrefix = prettyName isPrefix (ppopt_impl ppo) bnd op
1295 f = getFixity (opStr op)
1296 left l = case f of
1297 Nothing -> prettySe (-1) bnd l
1298 Just (Infixl p') -> prettySe p' bnd l
1299 Just f' -> prettySe (prec f'-1) bnd l
1300 right r = case f of
1301 Nothing -> prettySe (-1) bnd r
1302 Just (Infixr p') -> prettySe p' bnd r
1303 Just f' -> prettySe (prec f'-1) bnd r
1304 inFix l r = align . group $
1305 (left l <+> opName False) <$> group (right r)
1306 prettySe p bnd (PApp _ hd@(PRef fc f) [tm]) -- symbols, like 'foo
1307 | PConstant (Idris.Core.TT.Str str) <- getTm tm,
1308 f == sUN "Symbol_" = annotate (AnnType ("'" ++ str) ("The symbol " ++ str)) $
1309 char '\'' <> prettySe 10 bnd (PRef fc (sUN str))
1310 prettySe p bnd (PApp _ f as) = -- Normal prefix applications
1311 let args = getShowArgs as
1312 fp = prettySe 1 bnd f
1313 in
1314 bracket p 1 . group $
1315 if ppopt_impl ppo
1316 then if null as
1317 then fp
1318 else fp <+> align (vsep (map (prettyArgS bnd) as))
1319 else if null args
1320 then fp
1321 else fp <+> align (vsep (map (prettyArgS bnd) args))
1322 prettySe p bnd (PCase _ scr opts) =
1323 kwd "case" <+> prettySe 10 bnd scr <+> kwd "of" <> prettyBody
1324 where
1325 prettyBody = foldr (<>) empty $ intersperse (text "|") $ map sc opts
1327 sc (l, r) = nest nestingSize $ prettySe 10 bnd l <+> text "=>" <+> prettySe 10 bnd r
1328 prettySe p bnd (PHidden tm) = text "." <> prettySe 0 bnd tm
1329 prettySe p bnd (PRefl _ _) = annName eqCon $ text "Refl"
1330 prettySe p bnd (PResolveTC _) = text "resolvetc"
1331 prettySe p bnd (PTrue _ IsType) = annName unitTy $ text "()"
1332 prettySe p bnd (PTrue _ IsTerm) = annName unitCon $ text "()"
1333 prettySe p bnd (PTrue _ TypeOrTerm) = text "()"
1334 prettySe p bnd (PEq _ lt rt l r)
1335 | ppopt_impl ppo =
1336 bracket p 1 $
1337 enclose lparen rparen eq <+>
1338 align (group (vsep (map (prettyArgS bnd)
1339 [PImp 0 False [] (sUN "A") lt,
1340 PImp 0 False [] (sUN "B") rt,
1341 PExp 0 [] (sUN "x") l,
1342 PExp 0 [] (sUN "y") r])))
1343 | otherwise =
1344 bracket p 2 . align . group $
1345 prettySe 10 bnd l <+> eq <$> group (prettySe 10 bnd r)
1346 where eq = annName eqTy (text "=")
1347 prettySe p bnd (PRewrite _ l r _) =
1348 bracket p 2 $
1349 text "rewrite" <+> prettySe 10 bnd l <+> text "in" <+> prettySe 10 bnd r
1350 prettySe p bnd (PTyped l r) =
1351 lparen <> prettySe 10 bnd l <+> colon <+> prettySe 10 bnd r <> rparen
1352 prettySe p bnd pair@(PPair _ pun _ _) -- flatten tuples to the right, like parser
1353 | Just elts <- pairElts pair = enclose (ann lparen) (ann rparen) .
1354 align . group . vsep . punctuate (ann comma) $
1355 map (prettySe 10 bnd) elts
1356 where ann = case pun of
1357 TypeOrTerm -> id
1358 IsType -> annName pairTy
1359 IsTerm -> annName pairCon
1360 prettySe p bnd (PDPair _ TypeOrTerm l t r) =
1361 lparen <> prettySe 10 bnd l <+> text "**" <+> prettySe 10 bnd r <> rparen
1362 prettySe p bnd (PDPair _ IsType (PRef _ n) t r) =
1363 annName sigmaTy lparen <>
1364 bindingOf n False <+>
1365 annName sigmaTy (text "**") <+>
1366 prettySe 10 ((n, False):bnd) r <>
1367 annName sigmaTy rparen
1368 prettySe p bnd (PDPair _ IsType l t r) =
1369 annName sigmaTy lparen <>
1370 prettySe 10 bnd l <+>
1371 annName sigmaTy (text "**") <+>
1372 prettySe 10 bnd r <>
1373 annName sigmaTy rparen
1374 prettySe p bnd (PDPair _ IsTerm l t r) =
1375 annName existsCon lparen <>
1376 prettySe 10 bnd l <+>
1377 annName existsCon (text "**") <+>
1378 prettySe 10 bnd r <>
1379 annName existsCon rparen
1380 prettySe p bnd (PAlternative a as) =
1381 lparen <> text "|" <> prettyAs <> text "|" <> rparen
1382 where
1383 prettyAs =
1384 foldr (\l -> \r -> l <+> text "," <+> r) empty $ map (prettySe 10 bnd) as
1385 prettySe p bnd PType = annotate (AnnType "Type" "The type of types") $ text "Type"
1386 prettySe p bnd (PUniverse u) = annotate (AnnType (show u) "The type of unique types") $ text (show u)
1387 prettySe p bnd (PConstant c) = annotate (AnnConst c) (text (show c))
1388 -- XXX: add pretty for tactics
1389 prettySe p bnd (PProof ts) =
1390 text "proof" <+> lbrace <> nest nestingSize (text . show $ ts) <> rbrace
1391 prettySe p bnd (PTactics ts) =
1392 text "tactics" <+> lbrace <> nest nestingSize (text . show $ ts) <> rbrace
1393 prettySe p bnd (PMetavar n) = text "?" <> pretty n
1394 prettySe p bnd (PReturn f) = kwd "return"
1395 prettySe p bnd PImpossible = kwd "impossible"
1396 prettySe p bnd Placeholder = text "_"
1397 prettySe p bnd (PDoBlock _) = text "do block pretty not implemented"
1398 prettySe p bnd (PCoerced t) = prettySe p bnd t
1399 prettySe p bnd (PElabError s) = pretty s
1400 -- Quasiquote pprinting ignores bound vars
1401 prettySe p bnd (PQuasiquote t Nothing) = text "`(" <> prettySe p [] t <> text ")"
1402 prettySe p bnd (PQuasiquote t (Just g)) = text "`(" <> prettySe p [] t <+> colon <+> prettySe p [] g <> text ")"
1403 prettySe p bnd (PUnquote t) = text "~" <> prettySe p bnd t
1405 prettySe p bnd _ = text "missing pretty-printer for term"
1407 prettyArgS bnd (PImp _ _ _ n tm) = prettyArgSi bnd (n, tm)
1408 prettyArgS bnd (PExp _ _ _ tm) = prettyArgSe bnd tm
1409 prettyArgS bnd (PConstraint _ _ _ tm) = prettyArgSc bnd tm
1410 prettyArgS bnd (PTacImplicit _ _ n _ tm) = prettyArgSti bnd (n, tm)
1412 prettyArgSe bnd arg = prettySe 0 bnd arg
1413 prettyArgSi bnd (n, val) = lbrace <> pretty n <+> text "=" <+> prettySe 10 bnd val <> rbrace
1414 prettyArgSc bnd val = lbrace <> lbrace <> prettySe 10 bnd val <> rbrace <> rbrace
1415 prettyArgSti bnd (n, val) = lbrace <> kwd "auto" <+> pretty n <+> text "=" <+> prettySe 10 bnd val <> rbrace
1417 annName :: Name -> Doc OutputAnnotation -> Doc OutputAnnotation
1418 annName n = annotate (AnnName n Nothing Nothing Nothing)
1420 opStr :: Name -> String
1421 opStr (NS n _) = opStr n
1422 opStr (UN n) = T.unpack n
1424 basename :: Name -> Name
1425 basename (NS n _) = basename n
1426 basename n = n
1428 slist' p bnd (PApp _ (PRef _ nil) _)
1429 | not (ppopt_impl ppo) && nsroot nil == sUN "Nil" = Just []
1430 slist' p bnd (PRef _ nil)
1431 | not (ppopt_impl ppo) && nsroot nil == sUN "Nil" = Just []
1432 slist' p bnd (PApp _ (PRef _ cons) args)
1433 | nsroot cons == sUN "::",
1434 (PExp {getTm=tl}):(PExp {getTm=hd}):imps <- reverse args,
1435 all isImp imps,
1436 Just tl' <- slist' p bnd tl
1437 = Just (hd:tl')
1438 where
1439 isImp (PImp {}) = True
1440 isImp _ = False
1441 slist' _ _ tm = Nothing
1443 slist p bnd e | Just es <- slist' p bnd e = Just $
1444 case es of [] -> annotate (AnnData "" "") $ text "[]"
1445 [x] -> enclose left right . group $
1446 prettySe p bnd x
1447 xs -> (enclose left right .
1448 align . group . vsep .
1449 punctuate comma .
1450 map (prettySe p bnd)) xs
1451 where left = (annotate (AnnData "" "") (text "["))
1452 right = (annotate (AnnData "" "") (text "]"))
1453 comma = (annotate (AnnData "" "") (text ","))
1454 slist _ _ _ = Nothing
1456 pairElts :: PTerm -> Maybe [PTerm]
1457 pairElts (PPair _ _ x y) | Just elts <- pairElts y = Just (x:elts)
1458 | otherwise = Just [x, y]
1459 pairElts _ = Nothing
1461 natns = "Prelude.Nat."
1463 snat p (PRef _ z)
1464 | show z == (natns++"Z") || show z == "Z" = Just 0
1465 snat p (PApp _ s [PExp {getTm=n}])
1466 | show s == (natns++"S") || show s == "S",
1467 Just n' <- snat p n
1468 = Just $ 1 + n'
1469 snat _ _ = Nothing
1471 bracket outer inner doc
1472 | inner > outer = lparen <> doc <> rparen
1473 | otherwise = doc
1475 kwd = annotate AnnKeyword . text
1477 fixities :: M.Map String Fixity
1478 fixities = M.fromList [(s, f) | (Fix f s) <- infixes]
1480 getFixity :: String -> Maybe Fixity
1481 getFixity = flip M.lookup fixities
1483-- | Pretty-printer helper for the binding site of a name
1484bindingOf :: Name -- ^^ the bound name
1485 -> Bool -- ^^ whether the name is implicit
1486 -> Doc OutputAnnotation
1487bindingOf n imp = annotate (AnnBoundName n imp) (text (show n))
1489-- | Pretty-printer helper for names that attaches the correct annotations
1490prettyName
1491 :: Bool -- ^^ whether the name should be parenthesised if it is an infix operator
1492 -> Bool -- ^^ whether to show namespaces
1493 -> [(Name, Bool)] -- ^^ the current bound variables and whether they are implicit
1494 -> Name -- ^^ the name to pprint
1495 -> Doc OutputAnnotation
1496prettyName infixParen showNS bnd n
1497 | Just imp <- lookup n bnd = annotate (AnnBoundName n imp) fullName
1498 | otherwise = annotate (AnnName n Nothing Nothing Nothing) fullName
1499 where fullName = text nameSpace <> parenthesise (text (baseName n))
1500 baseName (UN n) = T.unpack n
1501 baseName (NS n ns) = baseName n
1502 baseName (MN i s) = T.unpack s
1503 baseName other = show other
1504 nameSpace = case n of
1505 (NS n' ns) -> if showNS then (concatMap (++ ".") . map T.unpack . reverse) ns else ""
1506 _ -> ""
1507 isInfix = case baseName n of
1508 "" -> False
1509 (c : _) -> not (isAlpha c)
1510 parenthesise = if isInfix && infixParen then enclose lparen rparen else id
1513showCImp :: PPOption -> PClause -> Doc OutputAnnotation
1514showCImp ppo (PClause _ n l ws r w)
1515 = prettyImp ppo l <+> showWs ws <+> text "=" <+> prettyImp ppo r
1516 <+> text "where" <+> text (show w)
1517 where
1518 showWs [] = empty
1519 showWs (x : xs) = text "|" <+> prettyImp ppo x <+> showWs xs
1520showCImp ppo (PWith _ n l ws r w)
1521 = prettyImp ppo l <+> showWs ws <+> text "with" <+> prettyImp ppo r
1522 <+> braces (text (show w))
1523 where
1524 showWs [] = empty
1525 showWs (x : xs) = text "|" <+> prettyImp ppo x <+> showWs xs
1528showDImp :: PPOption -> PData -> Doc OutputAnnotation
1529showDImp ppo (PDatadecl n ty cons)
1530 = text "data" <+> text (show n) <+> colon <+> prettyImp ppo ty <+> text "where" <$>
1531 (indent 2 $ vsep (map (\ (_, _, n, t, _, _) -> pipe <+> prettyName True False [] n <+> colon <+> prettyImp ppo t) cons))
1533showDecls :: PPOption -> [PDecl] -> Doc OutputAnnotation
1534showDecls o ds = vsep (map (showDeclImp o) ds)
1536showDeclImp _ (PFix _ f ops) = text (show f) <+> cat (punctuate (text ",") (map text ops))
1537showDeclImp o (PTy _ _ _ _ _ n t) = text "tydecl" <+> text (showCG n) <+> colon <+> prettyImp o t
1538showDeclImp o (PClauses _ _ n cs) = text "pat" <+> text (showCG n) <+> text "\t" <+>
1539 indent 2 (vsep (map (showCImp o) cs))
1540showDeclImp o (PData _ _ _ _ _ d) = showDImp o { ppopt_impl = True } d
1541showDeclImp o (PParams _ ns ps) = text "params" <+> braces (text (show ns) <> line <> showDecls o ps <> line)
1542showDeclImp o (PNamespace n ps) = text "namespace" <+> text n <> braces (line <> showDecls o ps <> line)
1543showDeclImp _ (PSyntax _ syn) = text "syntax" <+> text (show syn)
1544showDeclImp o (PClass _ _ _ cs n ps _ ds)
1545 = text "class" <+> text (show cs) <+> text (show n) <+> text (show ps) <> line <> showDecls o ds
1546showDeclImp o (PInstance _ _ cs n _ t _ ds)
1547 = text "instance" <+> text (show cs) <+> text (show n) <+> prettyImp o t <> line <> showDecls o ds
1548showDeclImp _ _ = text "..."
1549-- showDeclImp (PImport o) = "import " ++ o
1551instance Show (Doc OutputAnnotation) where
1552 show = flip (displayS . renderCompact) ""
1554getImps :: [PArg] -> [(Name, PTerm)]
1555getImps [] = []
1556getImps (PImp _ _ _ n tm : xs) = (n, tm) : getImps xs
1557getImps (_ : xs) = getImps xs
1559getExps :: [PArg] -> [PTerm]
1560getExps [] = []
1561getExps (PExp _ _ _ tm : xs) = tm : getExps xs
1562getExps (_ : xs) = getExps xs
1564getShowArgs :: [PArg] -> [PArg]
1565getShowArgs [] = []
1566getShowArgs (e@(PExp _ _ _ tm) : xs) = e : getShowArgs xs
1567getShowArgs (e : xs) | AlwaysShow `elem` argopts e = e : getShowArgs xs
1568getShowArgs (_ : xs) = getShowArgs xs
1570getConsts :: [PArg] -> [PTerm]
1571getConsts [] = []
1572getConsts (PConstraint _ _ _ tm : xs) = tm : getConsts xs
1573getConsts (_ : xs) = getConsts xs
1575getAll :: [PArg] -> [PTerm]
1576getAll = map getTm
1579-- | Show Idris name
1580showName :: Maybe IState -- ^^ the Idris state, for information about names and colours
1581 -> [(Name, Bool)] -- ^^ the bound variables and whether they're implicit
1582 -> PPOption -- ^^ pretty printing options
1583 -> Bool -- ^^ whether to colourise
1584 -> Name -- ^^ the term to show
1585 -> String
1586showName ist bnd ppo colour n = case ist of
1587 Just i -> if colour then colourise n (idris_colourTheme i) else showbasic n
1588 Nothing -> showbasic n
1589 where name = if ppopt_impl ppo then show n else showbasic n
1590 showbasic n@(UN _) = showCG n
1591 showbasic (MN i s) = str s
1592 showbasic (NS n s) = showSep "." (map str (reverse s)) ++ "." ++ showbasic n
1593 showbasic (SN s) = show s
1594 fst3 (x, _, _) = x
1595 colourise n t = let ctxt' = fmap tt_ctxt ist in
1596 case ctxt' of
1597 Nothing -> name
1598 Just ctxt | Just impl <- lookup n bnd -> if impl then colouriseImplicit t name
1599 else colouriseBound t name
1600 | isDConName n ctxt -> colouriseData t name
1601 | isFnName n ctxt -> colouriseFun t name
1602 | isTConName n ctxt -> colouriseType t name
1603 -- The assumption is that if a name is not bound and does not exist in the
1604 -- global context, then we're somewhere in which implicit info has been lost
1605 -- (like error messages). Thus, unknown vars are colourised as implicits.
1606 | otherwise -> colouriseImplicit t name
1608showTm :: IState -- ^^ the Idris state, for information about identifiers and colours
1609 -> PTerm -- ^^ the term to show
1610 -> String
1611showTm ist = displayDecorated (consoleDecorate ist) .
1612 renderPretty 0.8 100000 .
1613 prettyImp (ppOptionIst ist)
1615-- | Show a term with implicits, no colours
1616showTmImpls :: PTerm -> String
1617showTmImpls = flip (displayS . renderCompact . prettyImp verbosePPOption) ""
1621instance Sized PTerm where
1622 size (PQuote rawTerm) = size rawTerm
1623 size (PRef fc name) = size name
1624 size (PLam name ty bdy) = 1 + size ty + size bdy
1625 size (PPi plicity name ty bdy) = 1 + size ty + size bdy
1626 size (PLet name ty def bdy) = 1 + size ty + size def + size bdy
1627 size (PTyped trm ty) = 1 + size trm + size ty
1628 size (PApp fc name args) = 1 + size args
1629 size (PAppBind fc name args) = 1 + size args
1630 size (PCase fc trm bdy) = 1 + size trm + size bdy
1631 size (PTrue fc _) = 1
1632 size (PRefl fc _) = 1
1633 size (PResolveTC fc) = 1
1634 size (PEq fc _ _ left right) = 1 + size left + size right
1635 size (PRewrite fc left right _) = 1 + size left + size right
1636 size (PPair fc _ left right) = 1 + size left + size right
1637 size (PDPair fs _ left ty right) = 1 + size left + size ty + size right
1638 size (PAlternative a alts) = 1 + size alts
1639 size (PHidden hidden) = size hidden
1640 size (PUnifyLog tm) = size tm
1641 size (PDisamb _ tm) = size tm
1642 size (PNoImplicits tm) = size tm
1643 size PType = 1
1644 size (PUniverse _) = 1
1645 size (PConstant const) = 1 + size const
1646 size Placeholder = 1
1647 size (PDoBlock dos) = 1 + size dos
1648 size (PIdiom fc term) = 1 + size term
1649 size (PReturn fc) = 1
1650 size (PMetavar name) = 1
1651 size (PProof tactics) = size tactics
1652 size (PElabError err) = size err
1653 size PImpossible = 1
1654 size _ = 0
1656getPArity :: PTerm -> Int
1657getPArity (PPi _ _ _ sc) = 1 + getPArity sc
1658getPArity _ = 0
1660-- Return all names, free or globally bound, in the given term.
1662allNamesIn :: PTerm -> [Name]
1663allNamesIn tm = nub $ ni [] tm
1664 where -- TODO THINK added niTacImp, but is it right?
1665 ni env (PRef _ n)
1666 | not (n `elem` env) = [n]
1667 ni env (PPatvar _ n) = [n]
1668 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
1669 ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
1670 ni env (PCase _ c os) = ni env c ++ concatMap (ni env) (map snd os)
1671 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc
1672 ni env (PPi p n ty sc) = niTacImp env p ++ ni env ty ++ ni (n:env) sc
1673 ni env (PHidden tm) = ni env tm
1674 ni env (PEq _ _ _ l r) = ni env l ++ ni env r
1675 ni env (PRewrite _ l r _) = ni env l ++ ni env r
1676 ni env (PTyped l r) = ni env l ++ ni env r
1677 ni env (PPair _ _ l r) = ni env l ++ ni env r
1678 ni env (PDPair _ _ (PRef _ n) t r) = ni env t ++ ni (n:env) r
1679 ni env (PDPair _ _ l t r) = ni env l ++ ni env t ++ ni env r
1680 ni env (PAlternative a ls) = concatMap (ni env) ls
1681 ni env (PUnifyLog tm) = ni env tm
1682 ni env (PDisamb _ tm) = ni env tm
1683 ni env (PNoImplicits tm) = ni env tm
1684 ni env _ = []
1686 niTacImp env (TacImp _ _ scr) = ni env scr
1687 niTacImp _ _ = []
1689-- Return all names defined in binders in the given term
1690boundNamesIn :: PTerm -> [Name]
1691boundNamesIn tm = nub $ ni tm
1692 where -- TODO THINK Added niTacImp, but is it right?
1693 ni (PApp _ f as) = ni f ++ concatMap (ni) (map getTm as)
1694 ni (PAppBind _ f as) = ni f ++ concatMap (ni) (map getTm as)
1695 ni (PCase _ c os) = ni c ++ concatMap (ni) (map snd os)
1696 ni (PLam n ty sc) = n : (ni ty ++ ni sc)
1697 ni (PLet n ty val sc) = n : (ni ty ++ ni val ++ ni sc)
1698 ni (PPi p n ty sc) = niTacImp p ++ (n : (ni ty ++ ni sc))
1699 ni (PEq _ _ _ l r) = ni l ++ ni r
1700 ni (PRewrite _ l r _) = ni l ++ ni r
1701 ni (PTyped l r) = ni l ++ ni r
1702 ni (PPair _ _ l r) = ni l ++ ni r
1703 ni (PDPair _ _ (PRef _ n) t r) = ni t ++ ni r
1704 ni (PDPair _ _ l t r) = ni l ++ ni t ++ ni r
1705 ni (PAlternative a as) = concatMap (ni) as
1706 ni (PHidden tm) = ni tm
1707 ni (PUnifyLog tm) = ni tm
1708 ni (PDisamb _ tm) = ni tm
1709 ni (PNoImplicits tm) = ni tm
1710 ni _ = []
1712 niTacImp (TacImp _ _ scr) = ni scr
1713 niTacImp _ = []
1715-- Return names which are valid implicits in the given term (type).
1716implicitNamesIn :: [Name] -> IState -> PTerm -> [Name]
1717implicitNamesIn uvars ist tm = nub $ ni [] tm
1718 where
1719 ni env (PRef _ n)
1720 | not (n `elem` env)
1721 = case lookupTy n (tt_ctxt ist) of
1722 [] -> [n]
1723 _ -> if n `elem` uvars then [n] else []
1724 ni env (PApp _ f@(PRef _ n) as)
1725 | n `elem` uvars = ni env f ++ concatMap (ni env) (map getTm as)
1726 | otherwise = concatMap (ni env) (map getTm as)
1727 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
1728 ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
1729 ni env (PCase _ c os) = ni env c ++
1730 -- names in 'os', not counting the names bound in the cases
1731 (nub (concatMap (ni env) (map snd os))
1732 \\ nub (concatMap (ni env) (map fst os)))
1733 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc
1734 ni env (PPi p n ty sc) = ni env ty ++ ni (n:env) sc
1735 ni env (PEq _ _ _ l r) = ni env l ++ ni env r
1736 ni env (PRewrite _ l r _) = ni env l ++ ni env r
1737 ni env (PTyped l r) = ni env l ++ ni env r
1738 ni env (PPair _ _ l r) = ni env l ++ ni env r
1739 ni env (PDPair _ _ (PRef _ n) t r) = ni env t ++ ni (n:env) r
1740 ni env (PDPair _ _ l t r) = ni env l ++ ni env t ++ ni env r
1741 ni env (PAlternative a as) = concatMap (ni env) as
1742 ni env (PHidden tm) = ni env tm
1743 ni env (PUnifyLog tm) = ni env tm
1744 ni env (PDisamb _ tm) = ni env tm
1745 ni env (PNoImplicits tm) = ni env tm
1746 ni env _ = []
1748-- Return names which are free in the given term.
1749namesIn :: [(Name, PTerm)] -> IState -> PTerm -> [Name]
1750namesIn uvars ist tm = nub $ ni [] tm
1751 where
1752 ni env (PRef _ n)
1753 | not (n `elem` env)
1754 = case lookupTy n (tt_ctxt ist) of
1755 [] -> [n]
1756 _ -> if n `elem` (map fst uvars) then [n] else []
1757 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
1758 ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
1759 ni env (PCase _ c os) = ni env c ++
1760 -- names in 'os', not counting the names bound in the cases
1761 (nub (concatMap (ni env) (map snd os))
1762 \\ nub (concatMap (ni env) (map fst os)))
1763 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc
1764 ni env (PPi p n ty sc) = niTacImp env p ++ ni env ty ++ ni (n:env) sc
1765 ni env (PEq _ _ _ l r) = ni env l ++ ni env r
1766 ni env (PRewrite _ l r _) = ni env l ++ ni env r
1767 ni env (PTyped l r) = ni env l ++ ni env r
1768 ni env (PPair _ _ l r) = ni env l ++ ni env r
1769 ni env (PDPair _ _ (PRef _ n) t r) = ni env t ++ ni (n:env) r
1770 ni env (PDPair _ _ l t r) = ni env l ++ ni env t ++ ni env r
1771 ni env (PAlternative a as) = concatMap (ni env) as
1772 ni env (PHidden tm) = ni env tm
1773 ni env (PUnifyLog tm) = ni env tm
1774 ni env (PDisamb _ tm) = ni env tm
1775 ni env (PNoImplicits tm) = ni env tm
1776 ni env _ = []
1778 niTacImp env (TacImp _ _ scr) = ni env scr
1779 niTacImp _ _ = []
1781-- Return which of the given names are used in the given term.
1783usedNamesIn :: [Name] -> IState -> PTerm -> [Name]
1784usedNamesIn vars ist tm = nub $ ni [] tm
1785 where -- TODO THINK added niTacImp, but is it right?
1786 ni env (PRef _ n)
1787 | n `elem` vars && not (n `elem` env)
1788 = case lookupDefExact n (tt_ctxt ist) of
1789 Nothing -> [n]
1790 _ -> []
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 ++ concatMap (ni env) (map snd os)
1794 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc
1795 ni env (PPi p n ty sc) = niTacImp env p ++ ni env ty ++ ni (n:env) sc
1796 ni env (PEq _ _ _ l r) = ni env l ++ ni env r
1797 ni env (PRewrite _ l r _) = ni env l ++ ni env r
1798 ni env (PTyped l r) = ni env l ++ ni env r
1799 ni env (PPair _ _ l r) = ni env l ++ ni env r
1800 ni env (PDPair _ _ (PRef _ n) t r) = ni env t ++ ni (n:env) r
1801 ni env (PDPair _ _ l t r) = ni env l ++ ni env t ++ ni env r
1802 ni env (PAlternative a as) = concatMap (ni env) as
1803 ni env (PHidden tm) = ni env tm
1804 ni env (PUnifyLog tm) = ni env tm
1805 ni env (PDisamb _ tm) = ni env tm
1806 ni env (PNoImplicits tm) = ni env tm
1807 ni env _ = []
1809 niTacImp env (TacImp _ _ scr) = ni env scr
1810 niTacImp _ _ = []
1812-- Return the list of inaccessible (= dotted) positions for a name.
1813getErasureInfo :: IState -> Name -> [Int]
1814getErasureInfo ist n =
1815 case lookupCtxtExact n (idris_optimisation ist) of
1816 Just (Optimise inacc detagg) -> map fst inacc
1817 Nothing -> []