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