git.iko.soy/Idris-dev
on 17e042b help sign in
Idris-dev/src/Idris/AbsSyntaxTree.hs
1805 lines 73 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)
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_totcheck :: [(FC, Name)], -- names to check totality on
165 idris_defertotcheck :: [(FC, Name)], -- names to check at the end
166 idris_totcheckfail :: [(FC, String)],
167 idris_options :: IOption,
168 idris_name :: Int,
169 idris_lineapps :: [((FilePath, Int), PTerm)],
170 -- ^ Full application LHS on source line
171 idris_metavars :: [(Name, (Maybe Name, Int, Bool))], -- ^ The currently defined but not proven metavariables
172 idris_coercions :: [Name],
173 idris_transforms :: [(Term, Term)],
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 (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
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
369data OutputFmt = HTMLOutput | LaTeXOutput
371data Opt = Filename String
372 | Quiet
373 | NoBanner
374 | ColourREPL Bool
375 | Ideslave
376 | IdeslaveSocket
377 | ShowLibs
378 | ShowLibdir
379 | ShowIncs
380 | NoBasePkgs
381 | NoPrelude
382 | NoBuiltins -- only for the really primitive stuff!
383 | NoREPL
384 | OLogging Int
385 | Output String
386 | TypeCase
387 | TypeInType
388 | DefaultTotal
389 | DefaultPartial
390 | WarnPartial
391 | WarnReach
392 | NoCoverage
393 | ErrContext
394 | ShowImpl
395 | Verbose
396 | Port String -- REPL TCP port
397 | IBCSubDir String
398 | ImportDir String
399 | PkgBuild String
400 | PkgInstall String
401 | PkgClean String
402 | PkgCheck String
403 | PkgREPL String
404 | PkgMkDoc String -- IdrisDoc
405 | PkgTest String
406 | WarnOnly
407 | Pkg String
408 | BCAsm String
409 | DumpDefun String
410 | DumpCases String
411 | UseCodegen Codegen
412 | OutputTy OutputType
413 | Extension LanguageExt
414 | InterpretScript String
415 | EvalExpr String
416 | TargetTriple String
417 | TargetCPU String
418 | OptLevel Word
419 | Client String
420 | ShowOrigErr
421 | AutoWidth -- ^ Automatically adjust terminal width
422 | AutoSolve -- ^ Automatically issue "solve" tactic in interactive prover
423 deriving (Show, Eq)
425-- Parsed declarations
427data Fixity = Infixl { prec :: Int }
428 | Infixr { prec :: Int }
429 | InfixN { prec :: Int }
430 | PrefixN { prec :: Int }
431 deriving Eq
432{-!
433deriving instance Binary Fixity
434deriving instance NFData Fixity
435!-}
437instance Show Fixity where
438 show (Infixl i) = "infixl " ++ show i
439 show (Infixr i) = "infixr " ++ show i
440 show (InfixN i) = "infix " ++ show i
441 show (PrefixN i) = "prefix " ++ show i
443data FixDecl = Fix Fixity String
444 deriving Eq
446instance Show FixDecl where
447 show (Fix f s) = show f ++ " " ++ s
449{-!
450deriving instance Binary FixDecl
451deriving instance NFData FixDecl
452!-}
454instance Ord FixDecl where
455 compare (Fix x _) (Fix y _) = compare (prec x) (prec y)
458data Static = Static | Dynamic
459 deriving (Show, Eq)
460{-!
461deriving instance Binary Static
462deriving instance NFData Static
463!-}
465-- Mark bindings with their explicitness, and laziness
466data Plicity = Imp { pargopts :: [ArgOpt],
467 pstatic :: Static,
468 pparam :: Bool }
469 | Exp { pargopts :: [ArgOpt],
470 pstatic :: Static,
471 pparam :: Bool } -- this is a param (rather than index)
472 | Constraint { pargopts :: [ArgOpt],
473 pstatic :: Static }
474 | TacImp { pargopts :: [ArgOpt],
475 pstatic :: Static,
476 pscript :: PTerm }
477 deriving (Show, Eq)
479{-!
480deriving instance Binary Plicity
481deriving instance NFData Plicity
482!-}
484impl = Imp [] Dynamic False
485expl = Exp [] Dynamic False
486expl_param = Exp [] Dynamic True
487constraint = Constraint [] Dynamic
488tacimpl t = TacImp [] Dynamic t
490data FnOpt = Inlinable -- always evaluate when simplifying
491 | TotalFn | PartialFn | CoveringFn
492 | Coinductive | AssertTotal
493 | Dictionary -- type class dictionary, eval only when
494 -- a function argument, and further evaluation resutls
495 | Implicit -- implicit coercion
496 | NoImplicit -- do not apply implicit coercions
497 | CExport String -- export, with a C name
498 | ErrorHandler -- ^^ an error handler for use with the ErrorReflection extension
499 | ErrorReverse -- ^^ attempt to reverse normalise before showing in error
500 | Reflection -- a reflecting function, compile-time only
501 | Specialise [(Name, Maybe Int)] -- specialise it, freeze these names
502 | Constructor -- Data constructor type
503 deriving (Show, Eq)
504{-!
505deriving instance Binary FnOpt
506deriving instance NFData FnOpt
507!-}
509type FnOpts = [FnOpt]
511inlinable :: FnOpts -> Bool
512inlinable = elem Inlinable
514dictionary :: FnOpts -> Bool
515dictionary = elem Dictionary
518-- | Data declaration options
519data DataOpt = Codata -- ^ Set if the the data-type is coinductive
520 | DefaultEliminator -- ^ Set if an eliminator should be generated for data type
521 | DefaultCaseFun -- ^ Set if a case function should be generated for data type
522 | DataErrRev
523 deriving (Show, Eq)
525type DataOpts = [DataOpt]
527-- | Type provider - what to provide
528data ProvideWhat' t = ProvTerm t t -- ^ the first is the goal type, the second is the term
529 | ProvPostulate t -- ^ goal type must be Type, so only term
530 deriving (Show, Eq, Functor)
532type ProvideWhat = ProvideWhat' PTerm
534-- | Top-level declarations such as compiler directives, definitions,
535-- datatypes and typeclasses.
536data PDecl' t
537 = PFix FC Fixity [String] -- ^ Fixity declaration
538 | PTy (Docstring (Maybe PTerm)) [(Name, Docstring (Maybe PTerm))] SyntaxInfo FC FnOpts Name t -- ^ Type declaration
539 | PPostulate (Docstring (Maybe PTerm)) SyntaxInfo FC FnOpts Name t -- ^ Postulate
540 | PClauses FC FnOpts Name [PClause' t] -- ^ Pattern clause
541 | PCAF FC Name t -- ^ Top level constant
542 | PData (Docstring (Maybe PTerm)) [(Name, Docstring (Maybe PTerm))] SyntaxInfo FC DataOpts (PData' t) -- ^ Data declaration.
543 | PParams FC [(Name, t)] [PDecl' t] -- ^ Params block
544 | PNamespace String [PDecl' t] -- ^ New namespace
545 | PRecord (Docstring (Maybe PTerm)) SyntaxInfo FC Name t DataOpts (Docstring (Maybe PTerm)) Name t -- ^ Record declaration
546 | PClass (Docstring (Maybe PTerm)) SyntaxInfo FC
547 [t] -- constraints
548 Name
549 [(Name, t)] -- parameters
550 [(Name, Docstring (Maybe PTerm))] -- parameter docstrings
551 [PDecl' t] -- declarations
552 -- ^ Type class: arguments are documentation, syntax info, source location, constraints,
553 -- class name, parameters, method declarations
554 | PInstance SyntaxInfo FC [t] -- constraints
555 Name -- class
556 [t] -- parameters
557 t -- full instance type
558 (Maybe Name) -- explicit name
559 [PDecl' t]
560 -- ^ Instance declaration: arguments are syntax info, source location, constraints,
561 -- class name, parameters, full instance type, optional explicit name, and definitions
562 | PDSL Name (DSL' t) -- ^ DSL declaration
563 | PSyntax FC Syntax -- ^ Syntax definition
564 | PMutual FC [PDecl' t] -- ^ Mutual block
565 | PDirective (Idris ()) -- ^ Compiler directive. The parser inserts the corresponding action in the Idris monad.
566 | PProvider SyntaxInfo FC (ProvideWhat' t) Name -- ^ Type provider. The first t is the type, the second is the term
567 | PTransform FC Bool t t -- ^ Source-to-source transformation rule. If
568 -- bool is True, lhs and rhs must be convertible
569 deriving Functor
570{-!
571deriving instance Binary PDecl'
572deriving instance NFData PDecl'
573!-}
575-- For elaborator state
576type ElabD a = Elab' [PDecl] a
578-- | One clause of a top-level definition. Term arguments to constructors are:
579--
580-- 1. The whole application (missing for PClauseR and PWithR because they're within a "with" clause)
581--
582-- 2. The list of extra 'with' patterns
583--
584-- 3. The right-hand side
585--
586-- 4. The where block (PDecl' t)
588data PClause' t = PClause FC Name t [t] t [PDecl' t] -- ^ A normal top-level definition.
589 | PWith FC Name t [t] t [PDecl' t]
590 | PClauseR FC [t] t [PDecl' t]
591 | PWithR FC [t] t [PDecl' t]
592 deriving Functor
593{-!
594deriving instance Binary PClause'
595deriving instance NFData PClause'
596!-}
598-- | Data declaration
599data PData' t = PDatadecl { d_name :: Name, -- ^ The name of the datatype
600 d_tcon :: t, -- ^ Type constructor
601 d_cons :: [(Docstring (Maybe PTerm), [(Name, Docstring (Maybe PTerm))], Name, t, FC, [Name])] -- ^ Constructors
602 }
603 -- ^ Data declaration
604 | PLaterdecl { d_name :: Name, d_tcon :: t }
605 -- ^ "Placeholder" for data whose constructors are defined later
606 deriving Functor
607{-!
608deriving instance Binary PData'
609deriving instance NFData PData'
610!-}
612-- Handy to get a free function for applying PTerm -> PTerm functions
613-- across a program, by deriving Functor
615type PDecl = PDecl' PTerm
616type PData = PData' PTerm
617type PClause = PClause' PTerm
619-- get all the names declared in a decl
621declared :: PDecl -> [Name]
622declared (PFix _ _ _) = []
623declared (PTy _ _ _ _ _ n t) = [n]
624declared (PPostulate _ _ _ _ n t) = [n]
625declared (PClauses _ _ n _) = [] -- not a declaration
626declared (PCAF _ n _) = [n]
627declared (PData _ _ _ _ _ (PDatadecl n _ ts)) = n : map fstt ts
628 where fstt (_, _, a, _, _, _) = a
629declared (PData _ _ _ _ _ (PLaterdecl n _)) = [n]
630declared (PParams _ _ ds) = concatMap declared ds
631declared (PNamespace _ ds) = concatMap declared ds
632declared (PRecord _ _ _ n _ _ _ c _) = [n, c]
633declared (PClass _ _ _ _ n _ _ ms) = n : concatMap declared ms
634declared (PInstance _ _ _ _ _ _ _ _) = []
635declared (PDSL n _) = [n]
636declared (PSyntax _ _) = []
637declared (PMutual _ ds) = concatMap declared ds
638declared (PDirective _) = []
640-- get the names declared, not counting nested parameter blocks
641tldeclared :: PDecl -> [Name]
642tldeclared (PFix _ _ _) = []
643tldeclared (PTy _ _ _ _ _ n t) = [n]
644tldeclared (PPostulate _ _ _ _ n t) = [n]
645tldeclared (PClauses _ _ n _) = [] -- not a declaration
646tldeclared (PRecord _ _ _ n _ _ _ c _) = [n, c]
647tldeclared (PData _ _ _ _ _ (PDatadecl n _ ts)) = n : map fstt ts
648 where fstt (_, _, a, _, _, _) = a
649tldeclared (PParams _ _ ds) = []
650tldeclared (PMutual _ ds) = concatMap tldeclared ds
651tldeclared (PNamespace _ ds) = concatMap tldeclared ds
652tldeclared (PClass _ _ _ _ n _ _ ms) = concatMap tldeclared ms
653tldeclared (PInstance _ _ _ _ _ _ _ _) = []
654tldeclared _ = []
656defined :: PDecl -> [Name]
657defined (PFix _ _ _) = []
658defined (PTy _ _ _ _ _ n t) = []
659defined (PPostulate _ _ _ _ n t) = []
660defined (PClauses _ _ n _) = [n] -- not a declaration
661defined (PCAF _ n _) = [n]
662defined (PData _ _ _ _ _ (PDatadecl n _ ts)) = n : map fstt ts
663 where fstt (_, _, a, _, _, _) = a
664defined (PData _ _ _ _ _ (PLaterdecl n _)) = []
665defined (PParams _ _ ds) = concatMap defined ds
666defined (PNamespace _ ds) = concatMap defined ds
667defined (PRecord _ _ _ n _ _ _ c _) = [n, c]
668defined (PClass _ _ _ _ n _ _ ms) = n : concatMap defined ms
669defined (PInstance _ _ _ _ _ _ _ _) = []
670defined (PDSL n _) = [n]
671defined (PSyntax _ _) = []
672defined (PMutual _ ds) = concatMap defined ds
673defined (PDirective _) = []
674--defined _ = []
676updateN :: [(Name, Name)] -> Name -> Name
677updateN ns n | Just n' <- lookup n ns = n'
678updateN _ n = n
680updateNs :: [(Name, Name)] -> PTerm -> PTerm
681updateNs [] t = t
682updateNs ns t = mapPT updateRef t
683 where updateRef (PRef fc f) = PRef fc (updateN ns f)
684 updateRef t = t
686-- updateDNs :: [(Name, Name)] -> PDecl -> PDecl
687-- updateDNs [] t = t
688-- updateDNs ns (PTy s f n t) | Just n' <- lookup n ns = PTy s f n' t
689-- updateDNs ns (PClauses f n c) | Just n' <- lookup n ns = PClauses f n' (map updateCNs c)
690-- where updateCNs ns (PClause n l ts r ds)
691-- = PClause (updateN ns n) (fmap (updateNs ns) l)
692-- (map (fmap (updateNs ns)) ts)
693-- (fmap (updateNs ns) r)
694-- (map (updateDNs ns) ds)
695-- updateDNs ns c = c
697data PunInfo = IsType | IsTerm | TypeOrTerm deriving (Eq, Show)
699-- | High level language terms
700data PTerm = PQuote Raw -- ^ Inclusion of a core term into the high-level language
701 | PRef FC Name -- ^ A reference to a variable
702 | PInferRef FC Name -- ^ A name to be defined later
703 | PPatvar FC Name -- ^ A pattern variable
704 | PLam Name PTerm PTerm -- ^ A lambda abstraction
705 | PPi Plicity Name PTerm PTerm -- ^ (n : t1) -> t2
706 | PLet Name PTerm PTerm PTerm -- ^ A let binding
707 | PTyped PTerm PTerm -- ^ Term with explicit type
708 | PApp FC PTerm [PArg] -- ^ e.g. IO (), List Char, length x
709 | PAppBind FC PTerm [PArg] -- ^ implicitly bound application
710 | PMatchApp FC Name -- ^ Make an application by type matching
711 | PCase FC PTerm [(PTerm, PTerm)] -- ^ A case expression. Args are source location, scrutinee, and a list of pattern/RHS pairs
712 | PTrue FC PunInfo -- ^ Unit type..?
713 | PFalse FC -- ^ _|_
714 | PRefl FC PTerm -- ^ The canonical proof of the equality type
715 | PResolveTC FC -- ^ Solve this dictionary by type class resolution
716 | PEq FC PTerm PTerm PTerm PTerm -- ^ Heterogeneous equality type: A = B
717 | PRewrite FC PTerm PTerm (Maybe PTerm) -- ^ "rewrite" syntax, with optional result type
718 | PPair FC PunInfo PTerm PTerm -- ^ A pair (a, b) and whether it's a product type or a pair (solved by elaboration)
719 | 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)
720 | PAlternative Bool [PTerm] -- ^ True if only one may work. (| A, B, C|)
721 | PHidden PTerm -- ^ Irrelevant or hidden pattern
722 | PType -- ^ 'Type' type
723 | PUniverse Universe -- ^ Some universe
724 | PGoal FC PTerm Name PTerm -- ^ quoteGoal, used for %reflection functions
725 | PConstant Const -- ^ Builtin types
726 | Placeholder -- ^ Underscore
727 | PDoBlock [PDo] -- ^ Do notation
728 | PIdiom FC PTerm -- ^ Idiom brackets
729 | PReturn FC
730 | PMetavar Name -- ^ A metavariable, ?name
731 | PProof [PTactic] -- ^ Proof script
732 | PTactics [PTactic] -- ^ As PProof, but no auto solving
733 | PElabError Err -- ^ Error to report on elaboration
734 | PImpossible -- ^ Special case for declaring when an LHS can't typecheck
735 | PCoerced PTerm -- ^ To mark a coerced argument, so as not to coerce twice
736 | PDisamb [[T.Text]] PTerm -- ^ Preferences for explicit namespaces
737 | PUnifyLog PTerm -- ^ dump a trace of unifications when building term
738 | PNoImplicits PTerm -- ^ never run implicit converions on the term
739 | PQuasiquote PTerm (Maybe PTerm) -- ^ `(Term [: Term])
740 | PUnquote PTerm -- ^ ,Term
741 deriving Eq
744{-!
745deriving instance Binary PTerm
746deriving instance NFData PTerm
747!-}
749mapPT :: (PTerm -> PTerm) -> PTerm -> PTerm
750mapPT f t = f (mpt t) where
751 mpt (PLam n t s) = PLam n (mapPT f t) (mapPT f s)
752 mpt (PPi p n t s) = PPi p n (mapPT f t) (mapPT f s)
753 mpt (PLet n ty v s) = PLet n (mapPT f ty) (mapPT f v) (mapPT f s)
754 mpt (PRewrite fc t s g) = PRewrite fc (mapPT f t) (mapPT f s)
755 (fmap (mapPT f) g)
756 mpt (PApp fc t as) = PApp fc (mapPT f t) (map (fmap (mapPT f)) as)
757 mpt (PAppBind fc t as) = PAppBind fc (mapPT f t) (map (fmap (mapPT f)) as)
758 mpt (PCase fc c os) = PCase fc (mapPT f c) (map (pmap (mapPT f)) os)
759 mpt (PEq fc lt rt l r) = PEq fc (mapPT f lt) (mapPT f rt) (mapPT f l) (mapPT f r)
760 mpt (PTyped l r) = PTyped (mapPT f l) (mapPT f r)
761 mpt (PPair fc p l r) = PPair fc p (mapPT f l) (mapPT f r)
762 mpt (PDPair fc p l t r) = PDPair fc p (mapPT f l) (mapPT f t) (mapPT f r)
763 mpt (PAlternative a as) = PAlternative a (map (mapPT f) as)
764 mpt (PHidden t) = PHidden (mapPT f t)
765 mpt (PDoBlock ds) = PDoBlock (map (fmap (mapPT f)) ds)
766 mpt (PProof ts) = PProof (map (fmap (mapPT f)) ts)
767 mpt (PTactics ts) = PTactics (map (fmap (mapPT f)) ts)
768 mpt (PUnifyLog tm) = PUnifyLog (mapPT f tm)
769 mpt (PDisamb ns tm) = PDisamb ns (mapPT f tm)
770 mpt (PNoImplicits tm) = PNoImplicits (mapPT f tm)
771 mpt (PGoal fc r n sc) = PGoal fc (mapPT f r) n (mapPT f sc)
772 mpt x = x
775data PTactic' t = Intro [Name] | Intros | Focus Name
776 | Refine Name [Bool] | Rewrite t | DoUnify
777 | Induction t
778 | CaseTac t
779 | Equiv t
780 | MatchRefine Name
781 | LetTac Name t | LetTacTy Name t t
782 | Exact t | Compute | Trivial | TCInstance
783 | ProofSearch Bool Bool Int (Maybe Name) [Name]
784 -- ^ the bool is whether to search recursively
785 | Solve
786 | Attack
787 | ProofState | ProofTerm | Undo
788 | Try (PTactic' t) (PTactic' t)
789 | TSeq (PTactic' t) (PTactic' t)
790 | ApplyTactic t -- see Language.Reflection module
791 | ByReflection t
792 | Reflect t
793 | Fill t
794 | GoalType String (PTactic' t)
795 | TCheck t
796 | TEval t
797 | TDocStr (Either Name Const)
798 | TSearch t
799 | Skip
800 | TFail [ErrorReportPart]
801 | Qed | Abandon
802 deriving (Show, Eq, Functor, Foldable, Traversable)
803{-!
804deriving instance Binary PTactic'
805deriving instance NFData PTactic'
806!-}
807instance Sized a => Sized (PTactic' a) where
808 size (Intro nms) = 1 + size nms
809 size Intros = 1
810 size (Focus nm) = 1 + size nm
811 size (Refine nm bs) = 1 + size nm + length bs
812 size (Rewrite t) = 1 + size t
813 size (Induction t) = 1 + size t
814 size (LetTac nm t) = 1 + size nm + size t
815 size (Exact t) = 1 + size t
816 size Compute = 1
817 size Trivial = 1
818 size Solve = 1
819 size Attack = 1
820 size ProofState = 1
821 size ProofTerm = 1
822 size Undo = 1
823 size (Try l r) = 1 + size l + size r
824 size (TSeq l r) = 1 + size l + size r
825 size (ApplyTactic t) = 1 + size t
826 size (Reflect t) = 1 + size t
827 size (Fill t) = 1 + size t
828 size Qed = 1
829 size Abandon = 1
830 size Skip = 1
831 size (TFail ts) = 1 + size ts
833type PTactic = PTactic' PTerm
835data PDo' t = DoExp FC t
836 | DoBind FC Name t
837 | DoBindP FC t t [(t,t)]
838 | DoLet FC Name t t
839 | DoLetP FC t t
840 deriving (Eq, Functor)
841{-!
842deriving instance Binary PDo'
843deriving instance NFData PDo'
844!-}
846instance Sized a => Sized (PDo' a) where
847 size (DoExp fc t) = 1 + size fc + size t
848 size (DoBind fc nm t) = 1 + size fc + size nm + size t
849 size (DoBindP fc l r alts) = 1 + size fc + size l + size r + size alts
850 size (DoLet fc nm l r) = 1 + size fc + size nm + size l + size r
851 size (DoLetP fc l r) = 1 + size fc + size l + size r
853type PDo = PDo' PTerm
855-- The priority gives a hint as to elaboration order. Best to elaborate
856-- things early which will help give a more concrete type to other
857-- variables, e.g. a before (interpTy a).
859data PArg' t = PImp { priority :: Int,
860 machine_inf :: Bool, -- true if the machine inferred it
861 argopts :: [ArgOpt],
862 pname :: Name, getTm :: t }
863 | PExp { priority :: Int,
864 argopts :: [ArgOpt],
865 pname :: Name,
866 getTm :: t }
867 | PConstraint { priority :: Int,
868 argopts :: [ArgOpt],
869 pname :: Name,
870 getTm :: t }
871 | PTacImplicit { priority :: Int,
872 argopts :: [ArgOpt],
873 pname :: Name,
874 getScript :: t,
875 getTm :: t }
876 deriving (Show, Eq, Functor)
878data ArgOpt = AlwaysShow | HideDisplay | InaccessibleArg
879 deriving (Show, Eq)
881instance Sized a => Sized (PArg' a) where
882 size (PImp p _ l nm trm) = 1 + size nm + size trm
883 size (PExp p l nm trm) = 1 + size nm + size trm
884 size (PConstraint p l nm trm) = 1 + size nm +size nm + size trm
885 size (PTacImplicit p l nm scr trm) = 1 + size nm + size scr + size trm
887{-!
888deriving instance Binary PArg'
889deriving instance NFData PArg'
890!-}
892pimp n t mach = PImp 1 mach [] n t
893pexp t = PExp 1 [] (sMN 0 "arg") t
894pconst t = PConstraint 1 [] (sMN 0 "carg") t
895ptacimp n s t = PTacImplicit 2 [] n s t
897type PArg = PArg' PTerm
899-- Type class data
901data ClassInfo = CI { instanceName :: Name,
902 class_methods :: [(Name, (FnOpts, PTerm))],
903 class_defaults :: [(Name, (Name, PDecl))], -- method name -> default impl
904 class_default_superclasses :: [PDecl],
905 class_params :: [Name],
906 class_instances :: [Name] }
907 deriving Show
908{-!
909deriving instance Binary ClassInfo
910deriving instance NFData ClassInfo
911!-}
913-- Type inference data
915data TIData = TIPartial -- ^ a function with a partially defined type
916 | TISolution [Term] -- ^ possible solutions to a metavariable in a type
917 deriving Show
919-- | Miscellaneous information about functions
920data FnInfo = FnInfo { fn_params :: [Int] }
921 deriving Show
922{-!
923deriving instance Binary FnInfo
924!-}
926data OptInfo = Optimise { inaccessible :: [(Int,Name)], -- includes names for error reporting
927 detaggable :: Bool }
928 deriving Show
929{-!
930deriving instance Binary OptInfo
931deriving instance NFData OptInfo
932!-}
935data TypeInfo = TI { con_names :: [Name],
936 codata :: Bool,
937 data_opts :: DataOpts,
938 param_pos :: [Int],
939 mutual_types :: [Name] }
940 deriving Show
941{-!
942deriving instance Binary TypeInfo
943deriving instance NFData TypeInfo
944!-}
946-- Syntactic sugar info
948data DSL' t = DSL { dsl_bind :: t,
949 dsl_return :: t,
950 dsl_apply :: t,
951 dsl_pure :: t,
952 dsl_var :: Maybe t,
953 index_first :: Maybe t,
954 index_next :: Maybe t,
955 dsl_lambda :: Maybe t,
956 dsl_let :: Maybe t,
957 dsl_pi :: Maybe t
958 }
959 deriving (Show, Functor)
960{-!
961deriving instance Binary DSL'
962deriving instance NFData DSL'
963!-}
965type DSL = DSL' PTerm
967data SynContext = PatternSyntax | TermSyntax | AnySyntax
968 deriving Show
969{-!
970deriving instance Binary SynContext
971deriving instance NFData SynContext
972!-}
974data Syntax = Rule [SSymbol] PTerm SynContext
975 deriving Show
976{-!
977deriving instance Binary Syntax
978deriving instance NFData Syntax
979!-}
981data SSymbol = Keyword Name
982 | Symbol String
983 | Binding Name
984 | Expr Name
985 | SimpleExpr Name
986 deriving Show
987{-!
988deriving instance Binary SSymbol
989deriving instance NFData SSymbol
990!-}
992initDSL = DSL (PRef f (sUN ">>="))
993 (PRef f (sUN "return"))
994 (PRef f (sUN "<$>"))
995 (PRef f (sUN "pure"))
996 Nothing
997 Nothing
998 Nothing
999 Nothing
1000 Nothing
1001 Nothing
1002 where f = fileFC "(builtin)"
1004data Using = UImplicit Name PTerm
1005 | UConstraint Name [Name]
1006 deriving (Show, Eq)
1007{-!
1008deriving instance Binary Using
1009deriving instance NFData Using
1010!-}
1012data SyntaxInfo = Syn { using :: [Using],
1013 syn_params :: [(Name, PTerm)],
1014 syn_namespace :: [String],
1015 no_imp :: [Name],
1016 decoration :: Name -> Name,
1017 inPattern :: Bool,
1018 implicitAllowed :: Bool,
1019 maxline :: Maybe Int,
1020 mut_nesting :: Int,
1021 dsl_info :: DSL,
1022 syn_in_quasiquote :: Int }
1023 deriving Show
1024{-!
1025deriving instance NFData SyntaxInfo
1026deriving instance Binary SyntaxInfo
1027!-}
1029defaultSyntax = Syn [] [] [] [] id False False Nothing 0 initDSL 0
1031expandNS :: SyntaxInfo -> Name -> Name
1032expandNS syn n@(NS _ _) = n
1033expandNS syn n = case syn_namespace syn of
1034 [] -> n
1035 xs -> sNS n xs
1038-- For inferring types of things
1040bi = fileFC "builtin"
1042inferTy = sMN 0 "__Infer"
1043inferCon = sMN 0 "__infer"
1044inferDecl = PDatadecl inferTy
1045 PType
1046 [(emptyDocstring, [], inferCon, PPi impl (sMN 0 "iType") PType (
1047 PPi expl (sMN 0 "ival") (PRef bi (sMN 0 "iType"))
1048 (PRef bi inferTy)), bi, [])]
1049inferOpts = []
1051infTerm t = PApp bi (PRef bi inferCon) [pimp (sMN 0 "iType") Placeholder True, pexp t]
1052infP = P (TCon 6 0) inferTy (TType (UVal 0))
1054getInferTerm, getInferType :: Term -> Term
1055getInferTerm (Bind n b sc) = Bind n b $ getInferTerm sc
1056getInferTerm (App (App _ _) tm) = tm
1057getInferTerm tm = tm -- error ("getInferTerm " ++ show tm)
1059getInferType (Bind n b sc) = Bind n (toTy b) $ getInferType sc
1060 where toTy (Lam t) = Pi t (TType (UVar 0))
1061 toTy (PVar t) = PVTy t
1062 toTy b = b
1063getInferType (App (App _ ty) _) = ty
1067-- Handy primitives: Unit, False, Pair, MkPair, =, mkForeign
1069primNames = [falseTy, eqTy, eqCon, inferTy, inferCon]
1071unitTy = sUN "Unit"
1072unitCon = sUN "MkUnit"
1074-- TODO: elaborate the code samples in the docstring
1075falseDoc = fmap (const Nothing) . parseDocstring . T.pack $
1076 "The empty type, also known as the trivially false proposition." ++
1077 "\n\n" ++
1078 "Use `FalseElim` or `absurd` to prove anything if you have a variable " ++
1079 "of type `_|_` in scope."
1080falseTy = sMN 0 "__False"
1081falseDecl = PDatadecl falseTy PType []
1082falseOpts = []
1084pairTy = sUN "Pair"
1085pairCon = sUN "MkPair"
1087eqTy = sUN "="
1088eqCon = sUN "Refl"
1089eqDoc = fmap (const Nothing) . parseDocstring . T.pack $
1090 "The propositional equality type. A proof that `x` = `y`." ++
1091 "\n\n" ++
1092 "To use such a proof, pattern-match on it, and the two equal things will " ++
1093 "then need to be the _same_ pattern." ++
1094 "\n\n" ++
1095 "**Note**: Idris's equality type is potentially _heterogeneous_, which means that it " ++
1096 "is possible to state equalities between values of potentially different " ++
1097 "types. However, Idris will attempt the homogeneous case unless it fails to typecheck." ++
1098 "\n\n" ++
1099 "You may need to use `(~=~)` to explicitly request heterogeneous equality."
1101eqDecl = PDatadecl eqTy (piBindp impl [(n "A", PType), (n "B", PType)]
1102 (piBind [(n "x", PRef bi (n "A")), (n "y", PRef bi (n "B"))]
1103 PType))
1104 [(reflDoc, reflParamDoc,
1105 eqCon, PPi impl (n "A") PType (
1106 PPi impl (n "x") (PRef bi (n "A"))
1107 (PApp bi (PRef bi eqTy) [pimp (n "A") Placeholder False,
1108 pimp (n "B") Placeholder False,
1109 pexp (PRef bi (n "x")),
1110 pexp (PRef bi (n "x"))])), bi, [])]
1111 where n a = sUN a
1112 reflDoc = annotCode (const Nothing) . parseDocstring . T.pack $
1113 "A proof that `x` in fact equals `x`. To construct this, you must have already " ++
1114 "shown that both sides are in fact equal."
1115 reflParamDoc = [(n "A", annotCode (const Nothing) . parseDocstring . T.pack $ "the type at which the equality is proven"),
1116 (n "x", annotCode (const Nothing) . parseDocstring . T.pack $ "the element shown to be equal to itself.")]
1118eqParamDoc = [(n "A", annotCode (const Nothing) . parseDocstring . T.pack $ "the type of the left side of the equality"),
1119 (n "B", annotCode (const Nothing) . parseDocstring . T.pack $ "the type of the right side of the equality")
1121 where n a = sUN a
1123eqOpts = []
1125-- Defined in builtins.idr
1126sigmaTy = sUN "Sigma"
1127existsCon = sUN "MkSigma"
1129piBind :: [(Name, PTerm)] -> PTerm -> PTerm
1130piBind = piBindp expl
1132piBindp :: Plicity -> [(Name, PTerm)] -> PTerm -> PTerm
1133piBindp p [] t = t
1134piBindp p ((n, ty):ns) t = PPi p n ty (piBindp p ns t)
1137-- Pretty-printing declarations and terms
1139-- These "show" instances render to an absurdly wide screen because inserted line breaks
1140-- could interfere with interactive editing, which calls "show".
1142instance Show PTerm where
1143 showsPrec _ tm = (displayS . renderPretty 1.0 10000000 . prettyImp defaultPPOption) tm
1145instance Show PDecl where
1146 showsPrec _ d = (displayS . renderPretty 1.0 10000000 . showDeclImp verbosePPOption) d
1148instance Show PClause where
1149 showsPrec _ c = (displayS . renderPretty 1.0 10000000 . showCImp verbosePPOption) c
1151instance Show PData where
1152 showsPrec _ d = (displayS . renderPretty 1.0 10000000 . showDImp defaultPPOption) d
1154instance Pretty PTerm OutputAnnotation where
1155 pretty = prettyImp defaultPPOption
1157-- | Colourise annotations according to an Idris state. It ignores the names
1158-- in the annotation, as there's no good way to show extended information on a
1159-- terminal.
1160consoleDecorate :: IState -> OutputAnnotation -> String -> String
1161consoleDecorate ist _ | not (idris_colourRepl ist) = id
1162consoleDecorate ist (AnnConst c) = let theme = idris_colourTheme ist
1163 in if constIsType c
1164 then colouriseType theme
1165 else colouriseData theme
1166consoleDecorate ist (AnnData _ _) = colouriseData (idris_colourTheme ist)
1167consoleDecorate ist (AnnType _ _) = colouriseType (idris_colourTheme ist)
1168consoleDecorate ist (AnnBoundName _ True) = colouriseImplicit (idris_colourTheme ist)
1169consoleDecorate ist (AnnBoundName _ False) = colouriseBound (idris_colourTheme ist)
1170consoleDecorate ist AnnKeyword = colouriseKeyword (idris_colourTheme ist)
1171consoleDecorate ist (AnnName n _ _ _) = let ctxt = tt_ctxt ist
1172 theme = idris_colourTheme ist
1173 in case () of
1174 _ | isDConName n ctxt -> colouriseData theme
1175 _ | isFnName n ctxt -> colouriseFun theme
1176 _ | isTConName n ctxt -> colouriseType theme
1177 _ | isPostulateName n ist -> colourisePostulate theme
1178 _ | otherwise -> id -- don't colourise unknown names
1179consoleDecorate ist (AnnFC _) = id
1180consoleDecorate ist (AnnTextFmt fmt) = Idris.Colours.colourise (colour fmt)
1181 where colour BoldText = IdrisColour Nothing True False True False
1182 colour UnderlineText = IdrisColour Nothing True True False False
1183 colour ItalicText = IdrisColour Nothing True False False True
1184consoleDecorate ist (AnnTerm _ _) = id
1185consoleDecorate ist (AnnSearchResult _) = id
1187isPostulateName :: Name -> IState -> Bool
1188isPostulateName n ist = S.member n (idris_postulates ist)
1190-- | Pretty-print a high-level closed Idris term with no information about precedence/associativity
1191prettyImp :: PPOption -- ^^ pretty printing options
1192 -> PTerm -- ^^ the term to pretty-print
1193 -> Doc OutputAnnotation
1194prettyImp impl = pprintPTerm impl [] [] []
1196-- | Serialise something to base64 using its Binary instance.
1198-- | Do the right thing for rendering a term in an IState
1199prettyIst :: IState -> PTerm -> Doc OutputAnnotation
1200prettyIst ist = pprintPTerm (ppOptionIst ist) [] [] (idris_infixes ist)
1202-- | Pretty-print a high-level Idris term in some bindings context with infix info
1203pprintPTerm :: PPOption -- ^^ pretty printing options
1204 -> [(Name, Bool)] -- ^^ the currently-bound names and whether they are implicit
1205 -> [Name] -- ^^ names to always show in pi, even if not used
1206 -> [FixDecl] -- ^^ Fixity declarations
1207 -> PTerm -- ^^ the term to pretty-print
1208 -> Doc OutputAnnotation
1209pprintPTerm ppo bnd docArgs infixes = prettySe 10 bnd
1210 where
1211 prettySe :: Int -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation
1212 prettySe p bnd (PQuote r) =
1213 text "![" <> pretty r <> text "]"
1214 prettySe p bnd (PPatvar fc n) = pretty n
1215 prettySe p bnd e
1216 | Just str <- slist p bnd e = str
1217 | Just n <- snat p e = annotate (AnnData "Nat" "") (text (show n))
1218 prettySe p bnd (PRef fc n) = prettyName True (ppopt_impl ppo) bnd n
1219 prettySe p bnd (PLam n ty sc) =
1220 bracket p 2 . group . align . hang 2 $
1221 text "\\" <> bindingOf n False <+> text "=>" <$>
1222 prettySe 10 ((n, False):bnd) sc
1223 prettySe p bnd (PLet n ty v sc) =
1224 bracket p 2 . group . align $
1225 kwd "let" <+> (group . align . hang 2 $ bindingOf n False <+> text "=" <$> prettySe 10 bnd v) </>
1226 kwd "in" <+> (group . align . hang 2 $ prettySe 10 ((n, False):bnd) sc)
1227 prettySe p bnd (PPi (Exp l s _) n ty sc)
1228 | n `elem` allNamesIn sc || ppopt_impl ppo || n `elem` docArgs =
1229 bracket p 2 . group $
1230 enclose lparen rparen (group . align $ bindingOf n False <+> colon <+> prettySe 10 bnd ty) <+>
1231 st <> text "->" <$> prettySe 10 ((n, False):bnd) sc
1232 | otherwise =
1233 bracket p 2 . group $
1234 group (prettySe 1 bnd ty <+> st) <> text "->" <$> group (prettySe 10 ((n, False):bnd) sc)
1235 where
1236 st =
1237 case s of
1238 Static -> text "[static]" <> space
1239 _ -> empty
1240 prettySe p bnd (PPi (Imp l s _) n ty sc)
1241 | ppopt_impl ppo =
1242 bracket p 2 $
1243 lbrace <> bindingOf n True <+> colon <+> prettySe 10 bnd ty <> rbrace <+>
1244 st <> text "->" </> prettySe 10 ((n, True):bnd) sc
1245 | otherwise = prettySe 10 ((n, True):bnd) sc
1246 where
1247 st =
1248 case s of
1249 Static -> text "[static]" <> space
1250 _ -> empty
1251 prettySe p bnd (PPi (Constraint _ _) n ty sc) =
1252 bracket p 2 $
1253 prettySe 10 bnd ty <+> text "=>" </> prettySe 10 ((n, True):bnd) sc
1254 prettySe p bnd (PPi (TacImp _ _ s) n ty sc) =
1255 bracket p 2 $
1256 lbrace <> kwd "tacimp" <+> pretty n <+> colon <+> prettySe 10 bnd ty <>
1257 rbrace <+> text "->" </> prettySe 10 ((n, True):bnd) sc
1258 prettySe p bnd (PApp _ (PRef _ f) args) -- normal names, no explicit args
1259 | UN nm <- basename f
1260 , not (ppopt_impl ppo) && null (getShowArgs args) =
1261 prettyName True (ppopt_impl ppo) bnd f
1262 prettySe p bnd (PAppBind _ (PRef _ f) [])
1263 | not (ppopt_impl ppo) = text "!" <> prettyName True (ppopt_impl ppo) bnd f
1264 prettySe p bnd (PApp _ (PRef _ op) args) -- infix operators
1265 | UN nm <- basename op
1266 , not (tnull nm) &&
1267 (not (ppopt_impl ppo)) && (not $ isAlpha (thead nm)) =
1268 case getShowArgs args of
1269 [] -> opName True
1270 [x] -> group (opName True <$> group (prettySe 0 bnd (getTm x)))
1271 [l,r] -> let precedence = fromMaybe 20 (fmap prec f)
1272 in bracket p precedence $ inFix (getTm l) (getTm r)
1273 (l@(PExp _ _ _ _) : r@(PExp _ _ _ _) : rest) ->
1274 bracket p 1 $
1275 enclose lparen rparen (inFix (getTm l) (getTm r)) <+>
1276 align (group (vsep (map (prettyArgS bnd) rest)))
1277 as -> opName True <+> align (vsep (map (prettyArgS bnd) as))
1278 where opName isPrefix = prettyName isPrefix (ppopt_impl ppo) bnd op
1279 f = getFixity (opStr op)
1280 left l = case f of
1281 Nothing -> prettySe (-1) bnd l
1282 Just (Infixl p') -> prettySe p' bnd l
1283 Just f' -> prettySe (prec f'-1) bnd l
1284 right r = case f of
1285 Nothing -> prettySe (-1) bnd r
1286 Just (Infixr p') -> prettySe p' bnd r
1287 Just f' -> prettySe (prec f'-1) bnd r
1288 inFix l r = align . group $
1289 (left l <+> opName False) <$> group (right r)
1290 prettySe p bnd (PApp _ hd@(PRef fc f) [tm]) -- symbols, like 'foo
1291 | PConstant (Idris.Core.TT.Str str) <- getTm tm,
1292 f == sUN "Symbol_" = annotate (AnnType ("'" ++ str) ("The symbol " ++ str)) $
1293 char '\'' <> prettySe 10 bnd (PRef fc (sUN str))
1294 prettySe p bnd (PApp _ f as) = -- Normal prefix applications
1295 let args = getShowArgs as
1296 fp = prettySe 1 bnd f
1297 in
1298 bracket p 1 . group $
1299 if ppopt_impl ppo
1300 then if null as
1301 then fp
1302 else fp <+> align (vsep (map (prettyArgS bnd) as))
1303 else if null args
1304 then fp
1305 else fp <+> align (vsep (map (prettyArgS bnd) args))
1306 prettySe p bnd (PCase _ scr opts) =
1307 kwd "case" <+> prettySe 10 bnd scr <+> kwd "of" <> prettyBody
1308 where
1309 prettyBody = foldr (<>) empty $ intersperse (text "|") $ map sc opts
1311 sc (l, r) = nest nestingSize $ prettySe 10 bnd l <+> text "=>" <+> prettySe 10 bnd r
1312 prettySe p bnd (PHidden tm) = text "." <> prettySe 0 bnd tm
1313 prettySe p bnd (PRefl _ _) = annName eqCon $ text "Refl"
1314 prettySe p bnd (PResolveTC _) = text "resolvetc"
1315 prettySe p bnd (PTrue _ IsType) = annName unitTy $ text "()"
1316 prettySe p bnd (PTrue _ IsTerm) = annName unitCon $ text "()"
1317 prettySe p bnd (PTrue _ TypeOrTerm) = text "()"
1318 prettySe p bnd (PFalse _) = annName falseTy $ text "_|_"
1319 prettySe p bnd (PEq _ lt rt l r)
1320 | ppopt_impl ppo =
1321 bracket p 1 $
1322 enclose lparen rparen eq <+>
1323 align (group (vsep (map (prettyArgS bnd)
1324 [PImp 0 False [] (sUN "A") lt,
1325 PImp 0 False [] (sUN "B") rt,
1326 PExp 0 [] (sUN "x") l,
1327 PExp 0 [] (sUN "y") r])))
1328 | otherwise =
1329 bracket p 2 . align . group $
1330 prettySe 10 bnd l <+> eq <$> group (prettySe 10 bnd r)
1331 where eq = annName eqTy (text "=")
1332 prettySe p bnd (PRewrite _ l r _) =
1333 bracket p 2 $
1334 text "rewrite" <+> prettySe 10 bnd l <+> text "in" <+> prettySe 10 bnd r
1335 prettySe p bnd (PTyped l r) =
1336 lparen <> prettySe 10 bnd l <+> colon <+> prettySe 10 bnd r <> rparen
1337 prettySe p bnd pair@(PPair _ pun _ _) -- flatten tuples to the right, like parser
1338 | Just elts <- pairElts pair = enclose (ann lparen) (ann rparen) .
1339 align . group . vsep . punctuate (ann comma) $
1340 map (prettySe 10 bnd) elts
1341 where ann = case pun of
1342 TypeOrTerm -> id
1343 IsType -> annName pairTy
1344 IsTerm -> annName pairCon
1345 prettySe p bnd (PDPair _ TypeOrTerm l t r) =
1346 lparen <> prettySe 10 bnd l <+> text "**" <+> prettySe 10 bnd r <> rparen
1347 prettySe p bnd (PDPair _ IsType (PRef _ n) t r) =
1348 annName sigmaTy lparen <>
1349 bindingOf n False <+>
1350 annName sigmaTy (text "**") <+>
1351 prettySe 10 ((n, False):bnd) r <>
1352 annName sigmaTy rparen
1353 prettySe p bnd (PDPair _ IsType l t r) =
1354 annName sigmaTy lparen <>
1355 prettySe 10 bnd l <+>
1356 annName sigmaTy (text "**") <+>
1357 prettySe 10 bnd r <>
1358 annName sigmaTy rparen
1359 prettySe p bnd (PDPair _ IsTerm l t r) =
1360 annName existsCon lparen <>
1361 prettySe 10 bnd l <+>
1362 annName existsCon (text "**") <+>
1363 prettySe 10 bnd r <>
1364 annName existsCon rparen
1365 prettySe p bnd (PAlternative a as) =
1366 lparen <> text "|" <> prettyAs <> text "|" <> rparen
1367 where
1368 prettyAs =
1369 foldr (\l -> \r -> l <+> text "," <+> r) empty $ map (prettySe 10 bnd) as
1370 prettySe p bnd PType = annotate (AnnType "Type" "The type of types") $ text "Type"
1371 prettySe p bnd (PUniverse u) = annotate (AnnType (show u) "The type of unique types") $ text (show u)
1372 prettySe p bnd (PConstant c) = annotate (AnnConst c) (text (show c))
1373 -- XXX: add pretty for tactics
1374 prettySe p bnd (PProof ts) =
1375 text "proof" <+> lbrace <> nest nestingSize (text . show $ ts) <> rbrace
1376 prettySe p bnd (PTactics ts) =
1377 text "tactics" <+> lbrace <> nest nestingSize (text . show $ ts) <> rbrace
1378 prettySe p bnd (PMetavar n) = text "?" <> pretty n
1379 prettySe p bnd (PReturn f) = kwd "return"
1380 prettySe p bnd PImpossible = kwd "impossible"
1381 prettySe p bnd Placeholder = text "_"
1382 prettySe p bnd (PDoBlock _) = text "do block pretty not implemented"
1383 prettySe p bnd (PCoerced t) = prettySe p bnd t
1384 prettySe p bnd (PElabError s) = pretty s
1385 -- Quasiquote pprinting ignores bound vars
1386 prettySe p bnd (PQuasiquote t Nothing) = text "`(" <> prettySe p [] t <> text ")"
1387 prettySe p bnd (PQuasiquote t (Just g)) = text "`(" <> prettySe p [] t <+> colon <+> prettySe p [] g <> text ")"
1388 prettySe p bnd (PUnquote t) = text "~" <> prettySe p bnd t
1390 prettySe p bnd _ = text "missing pretty-printer for term"
1392 prettyArgS bnd (PImp _ _ _ n tm) = prettyArgSi bnd (n, tm)
1393 prettyArgS bnd (PExp _ _ _ tm) = prettyArgSe bnd tm
1394 prettyArgS bnd (PConstraint _ _ _ tm) = prettyArgSc bnd tm
1395 prettyArgS bnd (PTacImplicit _ _ n _ tm) = prettyArgSti bnd (n, tm)
1397 prettyArgSe bnd arg = prettySe 0 bnd arg
1398 prettyArgSi bnd (n, val) = lbrace <> pretty n <+> text "=" <+> prettySe 10 bnd val <> rbrace
1399 prettyArgSc bnd val = lbrace <> lbrace <> prettySe 10 bnd val <> rbrace <> rbrace
1400 prettyArgSti bnd (n, val) = lbrace <> kwd "auto" <+> pretty n <+> text "=" <+> prettySe 10 bnd val <> rbrace
1402 annName :: Name -> Doc OutputAnnotation -> Doc OutputAnnotation
1403 annName n = annotate (AnnName n Nothing Nothing Nothing)
1405 opStr :: Name -> String
1406 opStr (NS n _) = opStr n
1407 opStr (UN n) = T.unpack n
1409 basename :: Name -> Name
1410 basename (NS n _) = basename n
1411 basename n = n
1413 slist' p bnd (PApp _ (PRef _ nil) _)
1414 | not (ppopt_impl ppo) && nsroot nil == sUN "Nil" = Just []
1415 slist' p bnd (PRef _ nil)
1416 | not (ppopt_impl ppo) && nsroot nil == sUN "Nil" = Just []
1417 slist' p bnd (PApp _ (PRef _ cons) args)
1418 | nsroot cons == sUN "::",
1419 (PExp {getTm=tl}):(PExp {getTm=hd}):imps <- reverse args,
1420 all isImp imps,
1421 Just tl' <- slist' p bnd tl
1422 = Just (hd:tl')
1423 where
1424 isImp (PImp {}) = True
1425 isImp _ = False
1426 slist' _ _ tm = Nothing
1428 slist p bnd e | Just es <- slist' p bnd e = Just $
1429 case es of [] -> annotate (AnnData "" "") $ text "[]"
1430 [x] -> enclose left right . group $
1431 prettySe p bnd x
1432 xs -> (enclose left right .
1433 align . group . vsep .
1434 punctuate comma .
1435 map (prettySe p bnd)) xs
1436 where left = (annotate (AnnData "" "") (text "["))
1437 right = (annotate (AnnData "" "") (text "]"))
1438 comma = (annotate (AnnData "" "") (text ","))
1439 slist _ _ _ = Nothing
1441 pairElts :: PTerm -> Maybe [PTerm]
1442 pairElts (PPair _ _ x y) | Just elts <- pairElts y = Just (x:elts)
1443 | otherwise = Just [x, y]
1444 pairElts _ = Nothing
1446 natns = "Prelude.Nat."
1448 snat p (PRef _ z)
1449 | show z == (natns++"Z") || show z == "Z" = Just 0
1450 snat p (PApp _ s [PExp {getTm=n}])
1451 | show s == (natns++"S") || show s == "S",
1452 Just n' <- snat p n
1453 = Just $ 1 + n'
1454 snat _ _ = Nothing
1456 bracket outer inner doc
1457 | inner > outer = lparen <> doc <> rparen
1458 | otherwise = doc
1460 kwd = annotate AnnKeyword . text
1462 fixities :: M.Map String Fixity
1463 fixities = M.fromList [(s, f) | (Fix f s) <- infixes]
1465 getFixity :: String -> Maybe Fixity
1466 getFixity = flip M.lookup fixities
1468-- | Pretty-printer helper for the binding site of a name
1469bindingOf :: Name -- ^^ the bound name
1470 -> Bool -- ^^ whether the name is implicit
1471 -> Doc OutputAnnotation
1472bindingOf n imp = annotate (AnnBoundName n imp) (text (show n))
1474-- | Pretty-printer helper for names that attaches the correct annotations
1475prettyName
1476 :: Bool -- ^^ whether the name should be parenthesised if it is an infix operator
1477 -> Bool -- ^^ whether to show namespaces
1478 -> [(Name, Bool)] -- ^^ the current bound variables and whether they are implicit
1479 -> Name -- ^^ the name to pprint
1480 -> Doc OutputAnnotation
1481prettyName infixParen showNS bnd n
1482 | Just imp <- lookup n bnd = annotate (AnnBoundName n imp) fullName
1483 | otherwise = annotate (AnnName n Nothing Nothing Nothing) fullName
1484 where fullName = text nameSpace <> parenthesise (text (baseName n))
1485 baseName (UN n) = T.unpack n
1486 baseName (NS n ns) = baseName n
1487 baseName (MN i s) = T.unpack s
1488 baseName n | n == falseTy = "_|_"
1489 baseName other = show other
1490 nameSpace = case n of
1491 (NS n' ns) -> if showNS then (concatMap (++ ".") . map T.unpack . reverse) ns else ""
1492 _ -> ""
1493 isInfix = case baseName n of
1494 "" -> False
1495 (c : _) -> not (isAlpha c)
1496 parenthesise = if isInfix && infixParen then enclose lparen rparen else id
1499showCImp :: PPOption -> PClause -> Doc OutputAnnotation
1500showCImp ppo (PClause _ n l ws r w)
1501 = prettyImp ppo l <+> showWs ws <+> text "=" <+> prettyImp ppo r
1502 <+> text "where" <+> text (show w)
1503 where
1504 showWs [] = empty
1505 showWs (x : xs) = text "|" <+> prettyImp ppo x <+> showWs xs
1506showCImp ppo (PWith _ n l ws r w)
1507 = prettyImp ppo l <+> showWs ws <+> text "with" <+> prettyImp ppo r
1508 <+> braces (text (show w))
1509 where
1510 showWs [] = empty
1511 showWs (x : xs) = text "|" <+> prettyImp ppo x <+> showWs xs
1514showDImp :: PPOption -> PData -> Doc OutputAnnotation
1515showDImp ppo (PDatadecl n ty cons)
1516 = text "data" <+> text (show n) <+> colon <+> prettyImp ppo ty <+> text "where" <$>
1517 (indent 2 $ vsep (map (\ (_, _, n, t, _, _) -> pipe <+> prettyName True False [] n <+> colon <+> prettyImp ppo t) cons))
1519showDecls :: PPOption -> [PDecl] -> Doc OutputAnnotation
1520showDecls o ds = vsep (map (showDeclImp o) ds)
1522showDeclImp _ (PFix _ f ops) = text (show f) <+> cat (punctuate (text ",") (map text ops))
1523showDeclImp o (PTy _ _ _ _ _ n t) = text "tydecl" <+> text (showCG n) <+> colon <+> prettyImp o t
1524showDeclImp o (PClauses _ _ n cs) = text "pat" <+> text (showCG n) <+> text "\t" <+>
1525 indent 2 (vsep (map (showCImp o) cs))
1526showDeclImp o (PData _ _ _ _ _ d) = showDImp o { ppopt_impl = True } d
1527showDeclImp o (PParams _ ns ps) = text "params" <+> braces (text (show ns) <> line <> showDecls o ps <> line)
1528showDeclImp o (PNamespace n ps) = text "namespace" <+> text n <> braces (line <> showDecls o ps <> line)
1529showDeclImp _ (PSyntax _ syn) = text "syntax" <+> text (show syn)
1530showDeclImp o (PClass _ _ _ cs n ps _ ds)
1531 = text "class" <+> text (show cs) <+> text (show n) <+> text (show ps) <> line <> showDecls o ds
1532showDeclImp o (PInstance _ _ cs n _ t _ ds)
1533 = text "instance" <+> text (show cs) <+> text (show n) <+> prettyImp o t <> line <> showDecls o ds
1534showDeclImp _ _ = text "..."
1535-- showDeclImp (PImport o) = "import " ++ o
1537instance Show (Doc OutputAnnotation) where
1538 show = flip (displayS . renderCompact) ""
1540getImps :: [PArg] -> [(Name, PTerm)]
1541getImps [] = []
1542getImps (PImp _ _ _ n tm : xs) = (n, tm) : getImps xs
1543getImps (_ : xs) = getImps xs
1545getExps :: [PArg] -> [PTerm]
1546getExps [] = []
1547getExps (PExp _ _ _ tm : xs) = tm : getExps xs
1548getExps (_ : xs) = getExps xs
1550getShowArgs :: [PArg] -> [PArg]
1551getShowArgs [] = []
1552getShowArgs (e@(PExp _ _ _ tm) : xs) = e : getShowArgs xs
1553getShowArgs (e : xs) | AlwaysShow `elem` argopts e = e : getShowArgs xs
1554getShowArgs (_ : xs) = getShowArgs xs
1556getConsts :: [PArg] -> [PTerm]
1557getConsts [] = []
1558getConsts (PConstraint _ _ _ tm : xs) = tm : getConsts xs
1559getConsts (_ : xs) = getConsts xs
1561getAll :: [PArg] -> [PTerm]
1562getAll = map getTm
1565-- | Show Idris name
1566showName :: Maybe IState -- ^^ the Idris state, for information about names and colours
1567 -> [(Name, Bool)] -- ^^ the bound variables and whether they're implicit
1568 -> PPOption -- ^^ pretty printing options
1569 -> Bool -- ^^ whether to colourise
1570 -> Name -- ^^ the term to show
1571 -> String
1572showName ist bnd ppo colour n = case ist of
1573 Just i -> if colour then colourise n (idris_colourTheme i) else showbasic n
1574 Nothing -> showbasic n
1575 where name = if ppopt_impl ppo then show n else showbasic n
1576 showbasic n@(UN _) = showCG n
1577 showbasic (MN i s) = str s
1578 showbasic (NS n s) = showSep "." (map str (reverse s)) ++ "." ++ showbasic n
1579 showbasic (SN s) = show s
1580 fst3 (x, _, _) = x
1581 colourise n t = let ctxt' = fmap tt_ctxt ist in
1582 case ctxt' of
1583 Nothing -> name
1584 Just ctxt | Just impl <- lookup n bnd -> if impl then colouriseImplicit t name
1585 else colouriseBound t name
1586 | isDConName n ctxt -> colouriseData t name
1587 | isFnName n ctxt -> colouriseFun t name
1588 | isTConName n ctxt -> colouriseType t name
1589 -- The assumption is that if a name is not bound and does not exist in the
1590 -- global context, then we're somewhere in which implicit info has been lost
1591 -- (like error messages). Thus, unknown vars are colourised as implicits.
1592 | otherwise -> colouriseImplicit t name
1594showTm :: IState -- ^^ the Idris state, for information about identifiers and colours
1595 -> PTerm -- ^^ the term to show
1596 -> String
1597showTm ist = displayDecorated (consoleDecorate ist) .
1598 renderPretty 0.8 100000 .
1599 prettyImp (ppOptionIst ist)
1601-- | Show a term with implicits, no colours
1602showTmImpls :: PTerm -> String
1603showTmImpls = flip (displayS . renderCompact . prettyImp verbosePPOption) ""
1607instance Sized PTerm where
1608 size (PQuote rawTerm) = size rawTerm
1609 size (PRef fc name) = size name
1610 size (PLam name ty bdy) = 1 + size ty + size bdy
1611 size (PPi plicity name ty bdy) = 1 + size ty + size bdy
1612 size (PLet name ty def bdy) = 1 + size ty + size def + size bdy
1613 size (PTyped trm ty) = 1 + size trm + size ty
1614 size (PApp fc name args) = 1 + size args
1615 size (PAppBind fc name args) = 1 + size args
1616 size (PCase fc trm bdy) = 1 + size trm + size bdy
1617 size (PTrue fc _) = 1
1618 size (PFalse fc) = 1
1619 size (PRefl fc _) = 1
1620 size (PResolveTC fc) = 1
1621 size (PEq fc _ _ left right) = 1 + size left + size right
1622 size (PRewrite fc left right _) = 1 + size left + size right
1623 size (PPair fc _ left right) = 1 + size left + size right
1624 size (PDPair fs _ left ty right) = 1 + size left + size ty + size right
1625 size (PAlternative a alts) = 1 + size alts
1626 size (PHidden hidden) = size hidden
1627 size (PUnifyLog tm) = size tm
1628 size (PDisamb _ tm) = size tm
1629 size (PNoImplicits tm) = size tm
1630 size PType = 1
1631 size (PUniverse _) = 1
1632 size (PConstant const) = 1 + size const
1633 size Placeholder = 1
1634 size (PDoBlock dos) = 1 + size dos
1635 size (PIdiom fc term) = 1 + size term
1636 size (PReturn fc) = 1
1637 size (PMetavar name) = 1
1638 size (PProof tactics) = size tactics
1639 size (PElabError err) = size err
1640 size PImpossible = 1
1641 size _ = 0
1643getPArity :: PTerm -> Int
1644getPArity (PPi _ _ _ sc) = 1 + getPArity sc
1645getPArity _ = 0
1647-- Return all names, free or globally bound, in the given term.
1649allNamesIn :: PTerm -> [Name]
1650allNamesIn tm = nub $ ni [] tm
1651 where -- TODO THINK added niTacImp, but is it right?
1652 ni env (PRef _ n)
1653 | not (n `elem` env) = [n]
1654 ni env (PPatvar _ n) = [n]
1655 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
1656 ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
1657 ni env (PCase _ c os) = ni env c ++ concatMap (ni env) (map snd os)
1658 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc
1659 ni env (PPi p n ty sc) = niTacImp env p ++ ni env ty ++ ni (n:env) sc
1660 ni env (PHidden tm) = ni env tm
1661 ni env (PEq _ _ _ l r) = ni env l ++ ni env r
1662 ni env (PRewrite _ l r _) = ni env l ++ ni env r
1663 ni env (PTyped l r) = ni env l ++ ni env r
1664 ni env (PPair _ _ l r) = ni env l ++ ni env r
1665 ni env (PDPair _ _ (PRef _ n) t r) = ni env t ++ ni (n:env) r
1666 ni env (PDPair _ _ l t r) = ni env l ++ ni env t ++ ni env r
1667 ni env (PAlternative a ls) = concatMap (ni env) ls
1668 ni env (PUnifyLog tm) = ni env tm
1669 ni env (PDisamb _ tm) = ni env tm
1670 ni env (PNoImplicits tm) = ni env tm
1671 ni env _ = []
1673 niTacImp env (TacImp _ _ scr) = ni env scr
1674 niTacImp _ _ = []
1676-- Return all names defined in binders in the given term
1677boundNamesIn :: PTerm -> [Name]
1678boundNamesIn tm = nub $ ni tm
1679 where -- TODO THINK Added niTacImp, but is it right?
1680 ni (PApp _ f as) = ni f ++ concatMap (ni) (map getTm as)
1681 ni (PAppBind _ f as) = ni f ++ concatMap (ni) (map getTm as)
1682 ni (PCase _ c os) = ni c ++ concatMap (ni) (map snd os)
1683 ni (PLam n ty sc) = n : (ni ty ++ ni sc)
1684 ni (PLet n ty val sc) = n : (ni ty ++ ni val ++ ni sc)
1685 ni (PPi p n ty sc) = niTacImp p ++ (n : (ni ty ++ ni sc))
1686 ni (PEq _ _ _ l r) = ni l ++ ni r
1687 ni (PRewrite _ l r _) = ni l ++ ni r
1688 ni (PTyped l r) = ni l ++ ni r
1689 ni (PPair _ _ l r) = ni l ++ ni r
1690 ni (PDPair _ _ (PRef _ n) t r) = ni t ++ ni r
1691 ni (PDPair _ _ l t r) = ni l ++ ni t ++ ni r
1692 ni (PAlternative a as) = concatMap (ni) as
1693 ni (PHidden tm) = ni tm
1694 ni (PUnifyLog tm) = ni tm
1695 ni (PDisamb _ tm) = ni tm
1696 ni (PNoImplicits tm) = ni tm
1697 ni _ = []
1699 niTacImp (TacImp _ _ scr) = ni scr
1700 niTacImp _ = []
1702-- Return names which are valid implicits in the given term (type).
1703implicitNamesIn :: [Name] -> IState -> PTerm -> [Name]
1704implicitNamesIn uvars ist tm = nub $ ni [] tm
1705 where
1706 ni env (PRef _ n)
1707 | not (n `elem` env)
1708 = case lookupTy n (tt_ctxt ist) of
1709 [] -> [n]
1710 _ -> if n `elem` uvars then [n] else []
1711 ni env (PApp _ f@(PRef _ n) as)
1712 | n `elem` uvars = ni env f ++ concatMap (ni env) (map getTm as)
1713 | otherwise = concatMap (ni env) (map getTm as)
1714 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
1715 ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
1716 ni env (PCase _ c os) = ni env c ++
1717 -- names in 'os', not counting the names bound in the cases
1718 (nub (concatMap (ni env) (map snd os))
1719 \\ nub (concatMap (ni env) (map fst os)))
1720 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc
1721 ni env (PPi p n ty sc) = ni env ty ++ ni (n:env) sc
1722 ni env (PEq _ _ _ l r) = ni env l ++ ni env r
1723 ni env (PRewrite _ l r _) = ni env l ++ ni env r
1724 ni env (PTyped l r) = ni env l ++ ni env r
1725 ni env (PPair _ _ l r) = ni env l ++ ni env r
1726 ni env (PDPair _ _ (PRef _ n) t r) = ni env t ++ ni (n:env) r
1727 ni env (PDPair _ _ l t r) = ni env l ++ ni env t ++ ni env r
1728 ni env (PAlternative a as) = concatMap (ni env) as
1729 ni env (PHidden tm) = ni env tm
1730 ni env (PUnifyLog tm) = ni env tm
1731 ni env (PDisamb _ tm) = ni env tm
1732 ni env (PNoImplicits tm) = ni env tm
1733 ni env _ = []
1735-- Return names which are free in the given term.
1736namesIn :: [(Name, PTerm)] -> IState -> PTerm -> [Name]
1737namesIn uvars ist tm = nub $ ni [] tm
1738 where
1739 ni env (PRef _ n)
1740 | not (n `elem` env)
1741 = case lookupTy n (tt_ctxt ist) of
1742 [] -> [n]
1743 _ -> if n `elem` (map fst uvars) then [n] else []
1744 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
1745 ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
1746 ni env (PCase _ c os) = ni env c ++
1747 -- names in 'os', not counting the names bound in the cases
1748 (nub (concatMap (ni env) (map snd os))
1749 \\ nub (concatMap (ni env) (map fst os)))
1750 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc
1751 ni env (PPi p n ty sc) = niTacImp env p ++ ni env ty ++ ni (n:env) sc
1752 ni env (PEq _ _ _ l r) = ni env l ++ ni env r
1753 ni env (PRewrite _ l r _) = ni env l ++ ni env r
1754 ni env (PTyped l r) = ni env l ++ ni env r
1755 ni env (PPair _ _ l r) = ni env l ++ ni env r
1756 ni env (PDPair _ _ (PRef _ n) t r) = ni env t ++ ni (n:env) r
1757 ni env (PDPair _ _ l t r) = ni env l ++ ni env t ++ ni env r
1758 ni env (PAlternative a as) = concatMap (ni env) as
1759 ni env (PHidden tm) = ni env tm
1760 ni env (PUnifyLog tm) = ni env tm
1761 ni env (PDisamb _ tm) = ni env tm
1762 ni env (PNoImplicits tm) = ni env tm
1763 ni env _ = []
1765 niTacImp env (TacImp _ _ scr) = ni env scr
1766 niTacImp _ _ = []
1768-- Return which of the given names are used in the given term.
1770usedNamesIn :: [Name] -> IState -> PTerm -> [Name]
1771usedNamesIn vars ist tm = nub $ ni [] tm
1772 where -- TODO THINK added niTacImp, but is it right?
1773 ni env (PRef _ n)
1774 | n `elem` vars && not (n `elem` env)
1775 = case lookupDefExact n (tt_ctxt ist) of
1776 Nothing -> [n]
1777 _ -> []
1778 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
1779 ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
1780 ni env (PCase _ c os) = ni env c ++ concatMap (ni env) (map snd os)
1781 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc
1782 ni env (PPi p n ty sc) = niTacImp env p ++ ni env ty ++ ni (n:env) sc
1783 ni env (PEq _ _ _ l r) = ni env l ++ ni env r
1784 ni env (PRewrite _ l r _) = ni env l ++ ni env r
1785 ni env (PTyped l r) = ni env l ++ ni env r
1786 ni env (PPair _ _ l r) = ni env l ++ ni env r
1787 ni env (PDPair _ _ (PRef _ n) t r) = ni env t ++ ni (n:env) r
1788 ni env (PDPair _ _ l t r) = ni env l ++ ni env t ++ ni env r
1789 ni env (PAlternative a as) = concatMap (ni env) as
1790 ni env (PHidden tm) = ni env tm
1791 ni env (PUnifyLog tm) = ni env tm
1792 ni env (PDisamb _ tm) = ni env tm
1793 ni env (PNoImplicits tm) = ni env tm
1794 ni env _ = []
1796 niTacImp env (TacImp _ _ scr) = ni env scr
1797 niTacImp _ _ = []
1799-- Return the list of inaccessible (= dotted) positions for a name.
1800getErasureInfo :: IState -> Name -> [Int]
1801getErasureInfo ist n =
1802 case lookupCtxtExact n (idris_optimisation ist) of
1803 Just (Optimise inacc detagg) -> map fst inacc
1804 Nothing -> []