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