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