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