git.iko.soy/Idris-dev
on ef36111 help sign in
Idris-dev/src/Idris/AbsSyntaxTree.hs
1805 lines 73 kB history raw
1{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, DeriveFunctor,
2 TypeSynonymInstances, PatternGuards #-}
4module Idris.AbsSyntaxTree where
6import Idris.Core.TT
7import Idris.Core.Evaluate
8import Idris.Core.Elaborate hiding (Tactic(..))
9import Idris.Core.Typecheck
10import Idris.Docstrings
11import IRTS.Lang
12import IRTS.CodegenCommon
13import Util.Pretty
14import Util.DynamicLinker
16import Idris.Colours
18import System.Console.Haskeline
19import System.IO
21import Control.Monad.Trans.State.Strict
22import Control.Monad.Trans.Error
24import Data.List hiding (group)
25import Data.Char
26import qualified Data.Map as M
27import qualified Data.Text as T
28import qualified Data.Map as M
29import Data.Either
30import qualified Data.Set as S
31import Data.Word (Word)
32import Data.Maybe (fromMaybe)
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 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 idris_repl_defs :: [Name] -- ^ List of names that were defined in the repl, and can be re-/un-defined
205 }
207-- Required for parsers library, and therefore trifecta
208instance Show IState where
209 show = const "{internal state}"
211data SizeChange = Smaller | Same | Bigger | Unknown
212 deriving (Show, Eq)
213{-!
214deriving instance Binary SizeChange
215deriving instance NFData SizeChange
216!-}
218type SCGEntry = (Name, [Maybe (Int, SizeChange)])
219type UsageReason = (Name, Int) -- fn_name, its_arg_number
221data CGInfo = CGInfo { argsdef :: [Name],
222 calls :: [(Name, [[Name]])],
223 scg :: [SCGEntry],
224 argsused :: [Name],
225 usedpos :: [(Int, [UsageReason])] }
226 deriving Show
227{-!
228deriving instance Binary CGInfo
229deriving instance NFData CGInfo
230!-}
232primDefs = [sUN "unsafePerformPrimIO",
233 sUN "mkLazyForeignPrim",
234 sUN "mkForeignPrim",
235 sUN "FalseElim"]
237-- information that needs writing for the current module's .ibc file
238data IBCWrite = IBCFix FixDecl
239 | IBCImp Name
240 | IBCStatic Name
241 | IBCClass Name
242 | IBCInstance Bool Name Name
243 | IBCDSL Name
244 | IBCData Name
245 | IBCOpt Name
246 | IBCMetavar Name
247 | IBCSyntax Syntax
248 | IBCKeyword String
249 | IBCImport FilePath
250 | IBCObj Codegen FilePath
251 | IBCLib Codegen String
252 | IBCCGFlag Codegen String
253 | IBCDyLib String
254 | IBCHeader Codegen String
255 | IBCAccess Name Accessibility
256 | IBCMetaInformation Name MetaInformation
257 | IBCTotal Name Totality
258 | IBCFlags Name [FnOpt]
259 | IBCTrans (Term, Term)
260 | IBCErrRev (Term, Term)
261 | IBCCG Name
262 | IBCDoc Name
263 | IBCCoercion Name
264 | IBCDef Name -- i.e. main context
265 | IBCNameHint (Name, Name)
266 | IBCLineApp FilePath Int PTerm
267 | IBCErrorHandler Name
268 | IBCFunctionErrorHandler Name Name Name
269 | IBCPostulate Name
270 | IBCTotCheckErr FC String
271 | IBCParsedRegion FC
272 deriving Show
274-- | The initial state for the compiler
275idrisInit :: IState
276idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext
277 emptyContext emptyContext emptyContext emptyContext
278 emptyContext emptyContext emptyContext emptyContext
279 emptyContext emptyContext
280 [] [] [] defaultOpts 6 [] [] [] [] [] [] [] [] [] [] [] [] []
281 [] [] Nothing [] Nothing [] [] Nothing Nothing [] Hidden False [] Nothing [] [] RawOutput
282 True defaultTheme stdout [] (0, emptyContext) emptyContext M.empty
283 AutomaticWidth S.empty Nothing Nothing []
285-- | The monad for the main REPL - reading and processing files and updating
286-- global state (hence the IO inner monad).
287--type Idris = WriterT [Either String (IO ())] (State IState a))
288type Idris = StateT IState (ErrorT Err IO)
290-- Commands in the REPL
292data Codegen = ViaC
293 | ViaJava
294 | ViaNode
295 | ViaJavaScript
296 | ViaLLVM
297 | Bytecode
298 deriving (Show, Eq)
300-- | REPL commands
301data Command = Quit
302 | Help
303 | Eval PTerm
304 | NewDefn [PDecl] -- ^ Each 'PDecl' should be either a type declaration (at most one) or a clause defining the same name.
305 | Undefine [Name]
306 | Check PTerm
307 | DocStr (Either Name Const)
308 | TotCheck Name
309 | Reload
310 | Load FilePath (Maybe Int) -- up to maximum line number
311 | ChangeDirectory FilePath
312 | ModImport String
313 | Edit
314 | Compile Codegen String
315 | Execute
316 | ExecVal PTerm
317 | Metavars
318 | Prove Name
319 | AddProof (Maybe Name)
320 | RmProof Name
321 | ShowProof Name
322 | Proofs
323 | Universes
324 | LogLvl Int
325 | Spec PTerm
326 | HNF PTerm
327 | TestInline PTerm
328 | Defn Name
329 | Missing Name
330 | DynamicLink FilePath
331 | ListDynamic
332 | Pattelab PTerm
333 | DebugInfo Name
334 | Search PTerm
335 | CaseSplitAt Bool Int Name
336 | AddClauseFrom Bool Int Name
337 | AddProofClauseFrom Bool Int Name
338 | AddMissing Bool Int Name
339 | MakeWith Bool Int Name
340 | MakeLemma Bool Int Name
341 | DoProofSearch Bool Bool Int Name [Name]
342 -- ^ the first bool is whether to update,
343 -- the second is whether to search recursively (i.e. for the arguments)
344 | SetOpt Opt
345 | UnsetOpt Opt
346 | NOP
347 | SetColour ColourType IdrisColour
348 | ColourOn
349 | ColourOff
350 | ListErrorHandlers
351 | SetConsoleWidth ConsoleWidth
352 | Apropos String
353 | WhoCalls Name
354 | CallsWho Name
355 | MakeDoc String -- IdrisDoc
356 | Warranty
358data Opt = Filename String
359 | Quiet
360 | NoBanner
361 | ColourREPL Bool
362 | Ideslave
363 | ShowLibs
364 | ShowLibdir
365 | ShowIncs
366 | NoBasePkgs
367 | NoPrelude
368 | NoBuiltins -- only for the really primitive stuff!
369 | NoREPL
370 | OLogging Int
371 | Output String
372 | TypeCase
373 | TypeInType
374 | DefaultTotal
375 | DefaultPartial
376 | WarnPartial
377 | WarnReach
378 | NoCoverage
379 | ErrContext
380 | ShowImpl
381 | Verbose
382 | IBCSubDir String
383 | ImportDir String
384 | PkgBuild String
385 | PkgInstall String
386 | PkgClean String
387 | PkgCheck String
388 | PkgREPL String
389 | PkgMkDoc String -- IdrisDoc
390 | PkgTest String
391 | WarnOnly
392 | Pkg String
393 | BCAsm String
394 | DumpDefun String
395 | DumpCases String
396 | UseCodegen Codegen
397 | OutputTy OutputType
398 | Extension LanguageExt
399 | InterpretScript String
400 | EvalExpr String
401 | TargetTriple String
402 | TargetCPU String
403 | OptLevel Word
404 | Client String
405 | ShowOrigErr
406 | AutoWidth -- ^ Automatically adjust terminal width
407 | AutoSolve -- ^ Automatically issue "solve" tactic in interactive prover
408 deriving (Show, Eq)
410-- Parsed declarations
412data Fixity = Infixl { prec :: Int }
413 | Infixr { prec :: Int }
414 | InfixN { prec :: Int }
415 | PrefixN { prec :: Int }
416 deriving Eq
417{-!
418deriving instance Binary Fixity
419deriving instance NFData Fixity
420!-}
422instance Show Fixity where
423 show (Infixl i) = "infixl " ++ show i
424 show (Infixr i) = "infixr " ++ show i
425 show (InfixN i) = "infix " ++ show i
426 show (PrefixN i) = "prefix " ++ show i
428data FixDecl = Fix Fixity String
429 deriving Eq
431instance Show FixDecl where
432 show (Fix f s) = show f ++ " " ++ s
434{-!
435deriving instance Binary FixDecl
436deriving instance NFData FixDecl
437!-}
439instance Ord FixDecl where
440 compare (Fix x _) (Fix y _) = compare (prec x) (prec y)
443data Static = Static | Dynamic
444 deriving (Show, Eq)
445{-!
446deriving instance Binary Static
447deriving instance NFData Static
448!-}
450-- Mark bindings with their explicitness, and laziness
451data Plicity = Imp { pargopts :: [ArgOpt],
452 pstatic :: Static,
453 pparam :: Bool }
454 | Exp { pargopts :: [ArgOpt],
455 pstatic :: Static,
456 pparam :: Bool } -- this is a param (rather than index)
457 | Constraint { pargopts :: [ArgOpt],
458 pstatic :: Static }
459 | TacImp { pargopts :: [ArgOpt],
460 pstatic :: Static,
461 pscript :: PTerm }
462 deriving (Show, Eq)
464{-!
465deriving instance Binary Plicity
466deriving instance NFData Plicity
467!-}
469impl = Imp [] Dynamic False
470expl = Exp [] Dynamic False
471expl_param = Exp [] Dynamic True
472constraint = Constraint [] Dynamic
473tacimpl t = TacImp [] Dynamic t
475data FnOpt = Inlinable -- always evaluate when simplifying
476 | TotalFn | PartialFn | CoveringFn
477 | Coinductive | AssertTotal
478 | Dictionary -- type class dictionary, eval only when
479 -- a function argument, and further evaluation resutls
480 | Implicit -- implicit coercion
481 | NoImplicit -- do not apply implicit coercions
482 | CExport String -- export, with a C name
483 | ErrorHandler -- ^^ an error handler for use with the ErrorReflection extension
484 | ErrorReverse -- ^^ attempt to reverse normalise before showing in error
485 | Reflection -- a reflecting function, compile-time only
486 | Specialise [(Name, Maybe Int)] -- specialise it, freeze these names
487 deriving (Show, Eq)
488{-!
489deriving instance Binary FnOpt
490deriving instance NFData FnOpt
491!-}
493type FnOpts = [FnOpt]
495inlinable :: FnOpts -> Bool
496inlinable = elem Inlinable
498dictionary :: FnOpts -> Bool
499dictionary = elem Dictionary
502-- | Data declaration options
503data DataOpt = Codata -- ^ Set if the the data-type is coinductive
504 | DefaultEliminator -- ^ Set if an eliminator should be generated for data type
505 | DefaultCaseFun -- ^ Set if a case function should be generated for data type
506 | DataErrRev
507 deriving (Show, Eq)
509type DataOpts = [DataOpt]
511-- | Type provider - what to provide
512data ProvideWhat' t = ProvTerm t t -- ^ the first is the goal type, the second is the term
513 | ProvPostulate t -- ^ goal type must be Type, so only term
514 deriving (Show, Eq, Functor)
516type ProvideWhat = ProvideWhat' PTerm
518-- | Top-level declarations such as compiler directives, definitions,
519-- datatypes and typeclasses.
520data PDecl' t
521 = PFix FC Fixity [String] -- ^ Fixity declaration
522 | PTy Docstring [(Name, Docstring)] SyntaxInfo FC FnOpts Name t -- ^ Type declaration
523 | PPostulate Docstring SyntaxInfo FC FnOpts Name t -- ^ Postulate
524 | PClauses FC FnOpts Name [PClause' t] -- ^ Pattern clause
525 | PCAF FC Name t -- ^ Top level constant
526 | PData Docstring [(Name, Docstring)] SyntaxInfo FC DataOpts (PData' t) -- ^ Data declaration.
527 | PParams FC [(Name, t)] [PDecl' t] -- ^ Params block
528 | PNamespace String [PDecl' t] -- ^ New namespace
529 | PRecord Docstring SyntaxInfo FC Name t DataOpts Docstring Name t -- ^ Record declaration
530 | PClass Docstring SyntaxInfo FC
531 [t] -- constraints
532 Name
533 [(Name, t)] -- parameters
534 [(Name, Docstring)] -- parameter docstrings
535 [PDecl' t] -- declarations
536 -- ^ Type class: arguments are documentation, syntax info, source location, constraints,
537 -- class name, parameters, method declarations
538 | PInstance SyntaxInfo FC [t] -- constraints
539 Name -- class
540 [t] -- parameters
541 t -- full instance type
542 (Maybe Name) -- explicit name
543 [PDecl' t]
544 -- ^ Instance declaration: arguments are syntax info, source location, constraints,
545 -- class name, parameters, full instance type, optional explicit name, and definitions
546 | PDSL Name (DSL' t) -- ^ DSL declaration
547 | PSyntax FC Syntax -- ^ Syntax definition
548 | PMutual FC [PDecl' t] -- ^ Mutual block
549 | PDirective (Idris ()) -- ^ Compiler directive. The parser inserts the corresponding action in the Idris monad.
550 | PProvider SyntaxInfo FC (ProvideWhat' t) Name -- ^ Type provider. The first t is the type, the second is the term
551 | PTransform FC Bool t t -- ^ Source-to-source transformation rule. If
552 -- bool is True, lhs and rhs must be convertible
553 deriving Functor
554{-!
555deriving instance Binary PDecl'
556deriving instance NFData PDecl'
557!-}
559-- For elaborator state
560type ElabD a = Elab' [PDecl] a
562-- | One clause of a top-level definition. Term arguments to constructors are:
563--
564-- 1. The whole application (missing for PClauseR and PWithR because they're within a "with" clause)
565--
566-- 2. The list of extra 'with' patterns
567--
568-- 3. The right-hand side
569--
570-- 4. The where block (PDecl' t)
572data PClause' t = PClause FC Name t [t] t [PDecl' t] -- ^ A normal top-level definition.
573 | PWith FC Name t [t] t [PDecl' t]
574 | PClauseR FC [t] t [PDecl' t]
575 | PWithR FC [t] t [PDecl' t]
576 deriving Functor
577{-!
578deriving instance Binary PClause'
579deriving instance NFData PClause'
580!-}
582-- | Data declaration
583data PData' t = PDatadecl { d_name :: Name, -- ^ The name of the datatype
584 d_tcon :: t, -- ^ Type constructor
585 d_cons :: [(Docstring, [(Name, Docstring)], Name, t, FC, [Name])] -- ^ Constructors
586 }
587 -- ^ Data declaration
588 | PLaterdecl { d_name :: Name, d_tcon :: t }
589 -- ^ "Placeholder" for data whose constructors are defined later
590 deriving Functor
591{-!
592deriving instance Binary PData'
593deriving instance NFData PData'
594!-}
596-- Handy to get a free function for applying PTerm -> PTerm functions
597-- across a program, by deriving Functor
599type PDecl = PDecl' PTerm
600type PData = PData' PTerm
601type PClause = PClause' PTerm
603-- get all the names declared in a decl
605declared :: PDecl -> [Name]
606declared (PFix _ _ _) = []
607declared (PTy _ _ _ _ _ n t) = [n]
608declared (PPostulate _ _ _ _ n t) = [n]
609declared (PClauses _ _ n _) = [] -- not a declaration
610declared (PCAF _ n _) = [n]
611declared (PData _ _ _ _ _ (PDatadecl n _ ts)) = n : map fstt ts
612 where fstt (_, _, a, _, _, _) = a
613declared (PData _ _ _ _ _ (PLaterdecl n _)) = [n]
614declared (PParams _ _ ds) = concatMap declared ds
615declared (PNamespace _ ds) = concatMap declared ds
616declared (PRecord _ _ _ n _ _ _ c _) = [n, c]
617declared (PClass _ _ _ _ n _ _ ms) = n : concatMap declared ms
618declared (PInstance _ _ _ _ _ _ _ _) = []
619declared (PDSL n _) = [n]
620declared (PSyntax _ _) = []
621declared (PMutual _ ds) = concatMap declared ds
622declared (PDirective _) = []
624-- get the names declared, not counting nested parameter blocks
625tldeclared :: PDecl -> [Name]
626tldeclared (PFix _ _ _) = []
627tldeclared (PTy _ _ _ _ _ n t) = [n]
628tldeclared (PPostulate _ _ _ _ n t) = [n]
629tldeclared (PClauses _ _ n _) = [] -- not a declaration
630tldeclared (PRecord _ _ _ n _ _ _ c _) = [n, c]
631tldeclared (PData _ _ _ _ _ (PDatadecl n _ ts)) = n : map fstt ts
632 where fstt (_, _, a, _, _, _) = a
633tldeclared (PParams _ _ ds) = []
634tldeclared (PMutual _ ds) = concatMap tldeclared ds
635tldeclared (PNamespace _ ds) = concatMap tldeclared ds
636tldeclared (PClass _ _ _ _ n _ _ ms) = concatMap tldeclared ms
637tldeclared (PInstance _ _ _ _ _ _ _ _) = []
638tldeclared _ = []
640defined :: PDecl -> [Name]
641defined (PFix _ _ _) = []
642defined (PTy _ _ _ _ _ n t) = []
643defined (PPostulate _ _ _ _ n t) = []
644defined (PClauses _ _ n _) = [n] -- not a declaration
645defined (PCAF _ n _) = [n]
646defined (PData _ _ _ _ _ (PDatadecl n _ ts)) = n : map fstt ts
647 where fstt (_, _, a, _, _, _) = a
648defined (PData _ _ _ _ _ (PLaterdecl n _)) = []
649defined (PParams _ _ ds) = concatMap defined ds
650defined (PNamespace _ ds) = concatMap defined ds
651defined (PRecord _ _ _ n _ _ _ c _) = [n, c]
652defined (PClass _ _ _ _ n _ _ ms) = n : concatMap defined ms
653defined (PInstance _ _ _ _ _ _ _ _) = []
654defined (PDSL n _) = [n]
655defined (PSyntax _ _) = []
656defined (PMutual _ ds) = concatMap defined ds
657defined (PDirective _) = []
658--defined _ = []
660updateN :: [(Name, Name)] -> Name -> Name
661updateN ns n | Just n' <- lookup n ns = n'
662updateN _ n = n
664updateNs :: [(Name, Name)] -> PTerm -> PTerm
665updateNs [] t = t
666updateNs ns t = mapPT updateRef t
667 where updateRef (PRef fc f) = PRef fc (updateN ns f)
668 updateRef t = t
670-- updateDNs :: [(Name, Name)] -> PDecl -> PDecl
671-- updateDNs [] t = t
672-- updateDNs ns (PTy s f n t) | Just n' <- lookup n ns = PTy s f n' t
673-- updateDNs ns (PClauses f n c) | Just n' <- lookup n ns = PClauses f n' (map updateCNs c)
674-- where updateCNs ns (PClause n l ts r ds)
675-- = PClause (updateN ns n) (fmap (updateNs ns) l)
676-- (map (fmap (updateNs ns)) ts)
677-- (fmap (updateNs ns) r)
678-- (map (updateDNs ns) ds)
679-- updateDNs ns c = c
681data PunInfo = IsType | IsTerm | TypeOrTerm deriving (Eq, Show)
683-- | High level language terms
684data PTerm = PQuote Raw
685 | PRef FC Name
686 | PInferRef FC Name -- ^ A name to be defined later
687 | PPatvar FC Name
688 | PLam Name PTerm PTerm
689 | PPi Plicity Name PTerm PTerm -- ^ (n : t1) -> t2
690 | PLet Name PTerm PTerm PTerm
691 | PTyped PTerm PTerm -- ^ Term with explicit type
692 | PApp FC PTerm [PArg] -- ^ e.g. IO (), List Char, length x
693 | PAppBind FC PTerm [PArg] -- ^ implicitly bound application
694 | PMatchApp FC Name -- ^ Make an application by type matching
695 | PCase FC PTerm [(PTerm, PTerm)]
696 | PTrue FC PunInfo -- ^ Unit type..?
697 | PFalse FC -- ^ _|_
698 | PRefl FC PTerm
699 | PResolveTC FC
700 | PEq FC PTerm PTerm PTerm PTerm -- ^ Heterogeneous equality type: A = B
701 | PRewrite FC PTerm PTerm (Maybe PTerm)
702 | PPair FC PunInfo PTerm PTerm
703 | PDPair FC PunInfo PTerm PTerm PTerm
704 | PAlternative Bool [PTerm] -- True if only one may work
705 | PHidden PTerm -- ^ Irrelevant or hidden pattern
706 | PType -- ^ 'Type' type
707 | PGoal FC PTerm Name PTerm
708 | PConstant Const -- ^ Builtin types
709 | Placeholder
710 | PDoBlock [PDo]
711 | PIdiom FC PTerm
712 | PReturn FC
713 | PMetavar Name
714 | PProof [PTactic] -- ^ Proof script
715 | PTactics [PTactic] -- ^ As PProof, but no auto solving
716 | PElabError Err -- ^ Error to report on elaboration
717 | PImpossible -- ^ Special case for declaring when an LHS can't typecheck
718 | PCoerced PTerm -- ^ To mark a coerced argument, so as not to coerce twice
719 | PDisamb [[T.Text]] PTerm -- ^ Preferences for explicit namespaces
720 | PUnifyLog PTerm -- ^ dump a trace of unifications when building term
721 | PNoImplicits PTerm -- ^ never run implicit converions on the term
722 | PQuasiquote PTerm (Maybe PTerm) -- ^ `(Term [: Term])
723 | PUnquote PTerm -- ^ ,Term
724 deriving Eq
727{-!
728deriving instance Binary PTerm
729deriving instance NFData PTerm
730!-}
732mapPT :: (PTerm -> PTerm) -> PTerm -> PTerm
733mapPT f t = f (mpt t) where
734 mpt (PLam n t s) = PLam n (mapPT f t) (mapPT f s)
735 mpt (PPi p n t s) = PPi p n (mapPT f t) (mapPT f s)
736 mpt (PLet n ty v s) = PLet n (mapPT f ty) (mapPT f v) (mapPT f s)
737 mpt (PRewrite fc t s g) = PRewrite fc (mapPT f t) (mapPT f s)
738 (fmap (mapPT f) g)
739 mpt (PApp fc t as) = PApp fc (mapPT f t) (map (fmap (mapPT f)) as)
740 mpt (PAppBind fc t as) = PAppBind fc (mapPT f t) (map (fmap (mapPT f)) as)
741 mpt (PCase fc c os) = PCase fc (mapPT f c) (map (pmap (mapPT f)) os)
742 mpt (PEq fc lt rt l r) = PEq fc (mapPT f lt) (mapPT f rt) (mapPT f l) (mapPT f r)
743 mpt (PTyped l r) = PTyped (mapPT f l) (mapPT f r)
744 mpt (PPair fc p l r) = PPair fc p (mapPT f l) (mapPT f r)
745 mpt (PDPair fc p l t r) = PDPair fc p (mapPT f l) (mapPT f t) (mapPT f r)
746 mpt (PAlternative a as) = PAlternative a (map (mapPT f) as)
747 mpt (PHidden t) = PHidden (mapPT f t)
748 mpt (PDoBlock ds) = PDoBlock (map (fmap (mapPT f)) ds)
749 mpt (PProof ts) = PProof (map (fmap (mapPT f)) ts)
750 mpt (PTactics ts) = PTactics (map (fmap (mapPT f)) ts)
751 mpt (PUnifyLog tm) = PUnifyLog (mapPT f tm)
752 mpt (PDisamb ns tm) = PDisamb ns (mapPT f tm)
753 mpt (PNoImplicits tm) = PNoImplicits (mapPT f tm)
754 mpt (PGoal fc r n sc) = PGoal fc (mapPT f r) n (mapPT f sc)
755 mpt x = x
758data PTactic' t = Intro [Name] | Intros | Focus Name
759 | Refine Name [Bool] | Rewrite t | DoUnify
760 | Induction t
761 | CaseTac t
762 | Equiv t
763 | MatchRefine Name
764 | LetTac Name t | LetTacTy Name t t
765 | Exact t | Compute | Trivial | TCInstance
766 | ProofSearch Bool Bool Int (Maybe Name) [Name]
767 -- ^ the bool is whether to search recursively
768 | Solve
769 | Attack
770 | ProofState | ProofTerm | Undo
771 | Try (PTactic' t) (PTactic' t)
772 | TSeq (PTactic' t) (PTactic' t)
773 | ApplyTactic t -- see Language.Reflection module
774 | ByReflection t
775 | Reflect t
776 | Fill t
777 | GoalType String (PTactic' t)
778 | TCheck t
779 | TEval t
780 | TDocStr (Either Name Const)
781 | TSearch t
782 | Skip
783 | TFail [ErrorReportPart]
784 | Qed | Abandon
785 deriving (Show, Eq, Functor)
786{-!
787deriving instance Binary PTactic'
788deriving instance NFData PTactic'
789!-}
790instance Sized a => Sized (PTactic' a) where
791 size (Intro nms) = 1 + size nms
792 size Intros = 1
793 size (Focus nm) = 1 + size nm
794 size (Refine nm bs) = 1 + size nm + length bs
795 size (Rewrite t) = 1 + size t
796 size (Induction t) = 1 + size t
797 size (LetTac nm t) = 1 + size nm + size t
798 size (Exact t) = 1 + size t
799 size Compute = 1
800 size Trivial = 1
801 size Solve = 1
802 size Attack = 1
803 size ProofState = 1
804 size ProofTerm = 1
805 size Undo = 1
806 size (Try l r) = 1 + size l + size r
807 size (TSeq l r) = 1 + size l + size r
808 size (ApplyTactic t) = 1 + size t
809 size (Reflect t) = 1 + size t
810 size (Fill t) = 1 + size t
811 size Qed = 1
812 size Abandon = 1
813 size Skip = 1
814 size (TFail ts) = 1 + size ts
816type PTactic = PTactic' PTerm
818data PDo' t = DoExp FC t
819 | DoBind FC Name t
820 | DoBindP FC t t [(t,t)]
821 | DoLet FC Name t t
822 | DoLetP FC t t
823 deriving (Eq, Functor)
824{-!
825deriving instance Binary PDo'
826deriving instance NFData PDo'
827!-}
829instance Sized a => Sized (PDo' a) where
830 size (DoExp fc t) = 1 + size fc + size t
831 size (DoBind fc nm t) = 1 + size fc + size nm + size t
832 size (DoBindP fc l r alts) = 1 + size fc + size l + size r + size alts
833 size (DoLet fc nm l r) = 1 + size fc + size nm + size l + size r
834 size (DoLetP fc l r) = 1 + size fc + size l + size r
836type PDo = PDo' PTerm
838-- The priority gives a hint as to elaboration order. Best to elaborate
839-- things early which will help give a more concrete type to other
840-- variables, e.g. a before (interpTy a).
842data PArg' t = PImp { priority :: Int,
843 machine_inf :: Bool, -- true if the machine inferred it
844 argopts :: [ArgOpt],
845 pname :: Name, getTm :: t }
846 | PExp { priority :: Int,
847 argopts :: [ArgOpt],
848 pname :: Name,
849 getTm :: t }
850 | PConstraint { priority :: Int,
851 argopts :: [ArgOpt],
852 pname :: Name,
853 getTm :: t }
854 | PTacImplicit { priority :: Int,
855 argopts :: [ArgOpt],
856 pname :: Name,
857 getScript :: t,
858 getTm :: t }
859 deriving (Show, Eq, Functor)
861data ArgOpt = AlwaysShow | HideDisplay | InaccessibleArg
862 deriving (Show, Eq)
864instance Sized a => Sized (PArg' a) where
865 size (PImp p _ l nm trm) = 1 + size nm + size trm
866 size (PExp p l nm trm) = 1 + size nm + size trm
867 size (PConstraint p l nm trm) = 1 + size nm +size nm + size trm
868 size (PTacImplicit p l nm scr trm) = 1 + size nm + size scr + size trm
870{-!
871deriving instance Binary PArg'
872deriving instance NFData PArg'
873!-}
875pimp n t mach = PImp 1 mach [] n t
876pexp t = PExp 1 [] (sMN 0 "arg") t
877pconst t = PConstraint 1 [] (sMN 0 "carg") t
878ptacimp n s t = PTacImplicit 2 [] n s t
880type PArg = PArg' PTerm
882-- Type class data
884data ClassInfo = CI { instanceName :: Name,
885 class_methods :: [(Name, (FnOpts, PTerm))],
886 class_defaults :: [(Name, (Name, PDecl))], -- method name -> default impl
887 class_default_superclasses :: [PDecl],
888 class_params :: [Name],
889 class_instances :: [Name] }
890 deriving Show
891{-!
892deriving instance Binary ClassInfo
893deriving instance NFData ClassInfo
894!-}
896-- Type inference data
898data TIData = TIPartial -- ^ a function with a partially defined type
899 | TISolution [Term] -- ^ possible solutions to a metavariable in a type
900 deriving Show
902data OptInfo = Optimise { inaccessible :: [(Int,Name)], -- includes names for error reporting
903 detaggable :: Bool }
904 deriving Show
905{-!
906deriving instance Binary OptInfo
907deriving instance NFData OptInfo
908!-}
911data TypeInfo = TI { con_names :: [Name],
912 codata :: Bool,
913 data_opts :: DataOpts,
914 param_pos :: [Int],
915 mutual_types :: [Name] }
916 deriving Show
917{-!
918deriving instance Binary TypeInfo
919deriving instance NFData TypeInfo
920!-}
922-- Syntactic sugar info
924data DSL' t = DSL { dsl_bind :: t,
925 dsl_return :: t,
926 dsl_apply :: t,
927 dsl_pure :: t,
928 dsl_var :: Maybe t,
929 index_first :: Maybe t,
930 index_next :: Maybe t,
931 dsl_lambda :: Maybe t,
932 dsl_let :: Maybe t,
933 dsl_pi :: Maybe t
934 }
935 deriving (Show, Functor)
936{-!
937deriving instance Binary DSL'
938deriving instance NFData DSL'
939!-}
941type DSL = DSL' PTerm
943data SynContext = PatternSyntax | TermSyntax | AnySyntax
944 deriving Show
945{-!
946deriving instance Binary SynContext
947deriving instance NFData SynContext
948!-}
950data Syntax = Rule [SSymbol] PTerm SynContext
951 deriving Show
952{-!
953deriving instance Binary Syntax
954deriving instance NFData Syntax
955!-}
957data SSymbol = Keyword Name
958 | Symbol String
959 | Binding Name
960 | Expr Name
961 | SimpleExpr Name
962 deriving Show
963{-!
964deriving instance Binary SSymbol
965deriving instance NFData SSymbol
966!-}
968initDSL = DSL (PRef f (sUN ">>="))
969 (PRef f (sUN "return"))
970 (PRef f (sUN "<$>"))
971 (PRef f (sUN "pure"))
972 Nothing
973 Nothing
974 Nothing
975 Nothing
976 Nothing
977 Nothing
978 where f = fileFC "(builtin)"
980data Using = UImplicit Name PTerm
981 | UConstraint Name [Name]
982 deriving (Show, Eq)
983{-!
984deriving instance Binary Using
985deriving instance NFData Using
986!-}
988data SyntaxInfo = Syn { using :: [Using],
989 syn_params :: [(Name, PTerm)],
990 syn_namespace :: [String],
991 no_imp :: [Name],
992 decoration :: Name -> Name,
993 inPattern :: Bool,
994 implicitAllowed :: Bool,
995 maxline :: Maybe Int,
996 mut_nesting :: Int,
997 dsl_info :: DSL,
998 syn_in_quasiquote :: Bool }
999 deriving Show
1000{-!
1001deriving instance NFData SyntaxInfo
1002deriving instance Binary SyntaxInfo
1003!-}
1005defaultSyntax = Syn [] [] [] [] id False False Nothing 0 initDSL False
1007expandNS :: SyntaxInfo -> Name -> Name
1008expandNS syn n@(NS _ _) = n
1009expandNS syn n = case syn_namespace syn of
1010 [] -> n
1011 xs -> sNS n xs
1014-- For inferring types of things
1016bi = fileFC "builtin"
1018inferTy = sMN 0 "__Infer"
1019inferCon = sMN 0 "__infer"
1020inferDecl = PDatadecl inferTy
1021 PType
1022 [(emptyDocstring, [], inferCon, PPi impl (sMN 0 "iType") PType (
1023 PPi expl (sMN 0 "ival") (PRef bi (sMN 0 "iType"))
1024 (PRef bi inferTy)), bi, [])]
1025inferOpts = []
1027infTerm t = PApp bi (PRef bi inferCon) [pimp (sMN 0 "iType") Placeholder True, pexp t]
1028infP = P (TCon 6 0) inferTy (TType (UVal 0))
1030getInferTerm, getInferType :: Term -> Term
1031getInferTerm (Bind n b sc) = Bind n b $ getInferTerm sc
1032getInferTerm (App (App _ _) tm) = tm
1033getInferTerm tm = tm -- error ("getInferTerm " ++ show tm)
1035getInferType (Bind n b sc) = Bind n (toTy b) $ getInferType sc
1036 where toTy (Lam t) = Pi t
1037 toTy (PVar t) = PVTy t
1038 toTy b = b
1039getInferType (App (App _ ty) _) = ty
1043-- Handy primitives: Unit, False, Pair, MkPair, =, mkForeign, Elim type class
1045primNames = [unitTy, unitCon,
1046 falseTy, pairTy, pairCon,
1047 eqTy, eqCon, inferTy, inferCon]
1049unitDoc = parseDocstring . T.pack $ "The canonical single-element type, also known as the trivially true proposition."
1050unitTy = sMN 0 "__Unit"
1051unitCon = sMN 0 "__II"
1052unitDecl = PDatadecl unitTy PType
1053 [(parseDocstring . T.pack $ "The trivial constructor for `()`. ", [], unitCon, PRef bi unitTy, bi, [])]
1054unitOpts = [DefaultEliminator]
1056falseDoc = parseDocstring . T.pack $
1057 "The empty type, also known as the trivially false proposition." ++
1058 "\n\n" ++
1059 "Use `FalseElim` or `absurd` to prove anything if you have a variable " ++
1060 "of type `_|_` in scope."
1061falseTy = sMN 0 "__False"
1062falseDecl = PDatadecl falseTy PType []
1063falseOpts = []
1065pairDoc = parseDocstring . T.pack $ "The non-dependent pair type, also known as conjunction."
1066pairTy = sMN 0 "__Pair"
1067pairCon = sMN 0 "__MkPair"
1068pairDecl = PDatadecl pairTy (piBind [(n "A", PType), (n "B", PType)] PType)
1069 [(pairConDoc, pairConParamDoc,
1070 pairCon, PPi impl (n "A") PType (
1071 PPi impl (n "B") PType (
1072 PPi expl (n "a") (PRef bi (n "A")) (
1073 PPi expl (n "b") (PRef bi (n "B"))
1074 (PApp bi (PRef bi pairTy) [pexp (PRef bi (n "A")),
1075 pexp (PRef bi (n "B"))])))), bi, [])]
1076 where n a = sMN 0 a
1077 pairConDoc = parseDocstring . T.pack $ "A pair of elements"
1078 pairConParamDoc = [(n "a", parseDocstring . T.pack $ "the left element of the pair"),
1079 (n "b", parseDocstring . T.pack $ "the right element of the pair")]
1080pairOpts = []
1081pairParamDoc = [(n "A", parseDocstring . T.pack $ "the type of the left elements in the pair"),
1082 (n "B", parseDocstring . T.pack $ "the type of the left elements in the pair")]
1083 where n a = sMN 0 a
1085eqTy = sUN "="
1086eqCon = sUN "refl"
1087eqDoc = parseDocstring . T.pack $
1088 "The propositional equality type. A proof that `x` = `y`." ++
1089 "\n\n" ++
1090 "To use such a proof, pattern-match on it, and the two equal things will " ++
1091 "then need to be the _same_ pattern." ++
1092 "\n\n" ++
1093 "**Note**: Idris's equality type is potentially _heterogeneous_, which means that it " ++
1094 "is possible to state equalities between values of potentially different " ++
1095 "types. However, Idris will attempt the homogeneous case unless it fails to typecheck." ++
1096 "\n\n" ++
1097 "You may need to use `(~=~)` to explicitly request heterogeneous equality."
1099eqDecl = PDatadecl eqTy (piBindp impl [(n "A", PType), (n "B", PType)]
1100 (piBind [(n "x", PRef bi (n "A")), (n "y", PRef bi (n "B"))]
1101 PType))
1102 [(reflDoc, reflParamDoc,
1103 eqCon, PPi impl (n "A") PType (
1104 PPi impl (n "x") (PRef bi (n "A"))
1105 (PApp bi (PRef bi eqTy) [pimp (n "A") Placeholder False,
1106 pimp (n "B") Placeholder False,
1107 pexp (PRef bi (n "x")),
1108 pexp (PRef bi (n "x"))])), bi, [])]
1109 where n a = sUN a
1110 reflDoc = parseDocstring . T.pack $
1111 "A proof that `x` in fact equals `x`. To construct this, you must have already " ++
1112 "shown that both sides are in fact equal."
1113 reflParamDoc = [(n "A", parseDocstring . T.pack $ "the type at which the equality is proven"),
1114 (n "x", parseDocstring . T.pack $ "the element shown to be equal to itself.")]
1116eqParamDoc = [(n "A", parseDocstring . T.pack $ "the type of the left side of the equality"),
1117 (n "B", parseDocstring . T.pack $ "the type of the right side of the equality")
1119 where n a = sUN a
1121eqOpts = []
1123elimName = sUN "__Elim"
1124elimMethElimTy = sUN "__elimTy"
1125elimMethElim = sUN "elim"
1126elimDecl = PClass (parseDocstring . T.pack $ "Type class for eliminators") defaultSyntax bi [] elimName [(sUN "scrutineeType", PType)] []
1127 [PTy emptyDocstring [] defaultSyntax bi [TotalFn] elimMethElimTy PType,
1128 PTy emptyDocstring [] defaultSyntax bi [TotalFn] elimMethElim (PRef bi elimMethElimTy)]
1130-- Defined in builtins.idr
1131sigmaTy = sUN "Sigma"
1132existsCon = sUN "Sg_intro"
1134piBind :: [(Name, PTerm)] -> PTerm -> PTerm
1135piBind = piBindp expl
1137piBindp :: Plicity -> [(Name, PTerm)] -> PTerm -> PTerm
1138piBindp p [] t = t
1139piBindp p ((n, ty):ns) t = PPi p n ty (piBindp p ns t)
1142-- Pretty-printing declarations and terms
1144-- These "show" instances render to an absurdly wide screen because inserted line breaks
1145-- could interfere with interactive editing, which calls "show".
1147instance Show PTerm where
1148 showsPrec _ tm = (displayS . renderPretty 1.0 10000000 . prettyImp defaultPPOption) tm
1150instance Show PDecl where
1151 showsPrec _ d = (displayS . renderPretty 1.0 10000000 . showDeclImp verbosePPOption) d
1153instance Show PClause where
1154 showsPrec _ c = (displayS . renderPretty 1.0 10000000 . showCImp verbosePPOption) c
1156instance Show PData where
1157 showsPrec _ d = (displayS . renderPretty 1.0 10000000 . showDImp defaultPPOption) d
1159instance Pretty PTerm OutputAnnotation where
1160 pretty = prettyImp defaultPPOption
1162-- | Colourise annotations according to an Idris state. It ignores the names
1163-- in the annotation, as there's no good way to show extended information on a
1164-- terminal.
1165consoleDecorate :: IState -> OutputAnnotation -> String -> String
1166consoleDecorate ist _ | not (idris_colourRepl ist) = id
1167consoleDecorate ist (AnnConst c) = let theme = idris_colourTheme ist
1168 in if constIsType c
1169 then colouriseType theme
1170 else colouriseData theme
1171consoleDecorate ist (AnnData _ _) = colouriseData (idris_colourTheme ist)
1172consoleDecorate ist (AnnType _ _) = colouriseType (idris_colourTheme ist)
1173consoleDecorate ist (AnnBoundName _ True) = colouriseImplicit (idris_colourTheme ist)
1174consoleDecorate ist (AnnBoundName _ False) = colouriseBound (idris_colourTheme ist)
1175consoleDecorate ist AnnKeyword = colouriseKeyword (idris_colourTheme ist)
1176consoleDecorate ist (AnnName n _ _ _) = let ctxt = tt_ctxt ist
1177 theme = idris_colourTheme ist
1178 in case () of
1179 _ | isDConName n ctxt -> colouriseData theme
1180 _ | isFnName n ctxt -> colouriseFun theme
1181 _ | isTConName n ctxt -> colouriseType theme
1182 _ | isPostulateName n ist -> colourisePostulate theme
1183 _ | otherwise -> id -- don't colourise unknown names
1184consoleDecorate ist (AnnFC _) = id
1185consoleDecorate ist (AnnTextFmt fmt) = Idris.Colours.colourise (colour fmt)
1186 where colour BoldText = IdrisColour Nothing True False True False
1187 colour UnderlineText = IdrisColour Nothing True True False False
1188 colour ItalicText = IdrisColour Nothing True False False True
1189consoleDecorate ist (AnnTerm _ _) = id
1191isPostulateName :: Name -> IState -> Bool
1192isPostulateName n ist = S.member n (idris_postulates ist)
1194-- | Pretty-print a high-level closed Idris term with no information about precedence/associativity
1195prettyImp :: PPOption -- ^^ pretty printing options
1196 -> PTerm -- ^^ the term to pretty-print
1197 -> Doc OutputAnnotation
1198prettyImp impl = pprintPTerm impl [] [] []
1200-- | Serialise something to base64 using its Binary instance.
1202-- | Do the right thing for rendering a term in an IState
1203prettyIst :: IState -> PTerm -> Doc OutputAnnotation
1204prettyIst ist = pprintPTerm (ppOptionIst ist) [] [] (idris_infixes ist)
1206-- | Pretty-print a high-level Idris term in some bindings context with infix info
1207pprintPTerm :: PPOption -- ^^ pretty printing options
1208 -> [(Name, Bool)] -- ^^ the currently-bound names and whether they are implicit
1209 -> [Name] -- ^^ names to always show in pi, even if not used
1210 -> [FixDecl] -- ^^ Fixity declarations
1211 -> PTerm -- ^^ the term to pretty-print
1212 -> Doc OutputAnnotation
1213pprintPTerm ppo bnd docArgs infixes = prettySe 10 bnd
1214 where
1215 prettySe :: Int -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation
1216 prettySe p bnd (PQuote r) =
1217 text "![" <> pretty r <> text "]"
1218 prettySe p bnd (PPatvar fc n) = pretty n
1219 prettySe p bnd e
1220 | Just str <- slist p bnd e = str
1221 | Just n <- snat p e = annotate (AnnData "Nat" "") (text (show n))
1222 prettySe p bnd (PRef fc n) = prettyName True (ppopt_impl ppo) bnd n
1223 prettySe p bnd (PLam n ty sc) =
1224 bracket p 2 . group . align . hang 2 $
1225 text "\\" <> bindingOf n False <+> text "=>" <$>
1226 prettySe 10 ((n, False):bnd) sc
1227 prettySe p bnd (PLet n ty v sc) =
1228 bracket p 2 $
1229 kwd "let" <+> bindingOf n False <+> text "=" </>
1230 prettySe 10 bnd v <+> kwd "in" </>
1231 prettySe 10 ((n, False):bnd) sc
1232 prettySe p bnd (PPi (Exp l s _) n ty sc)
1233 | n `elem` allNamesIn sc || ppopt_impl ppo || n `elem` docArgs =
1234 bracket p 2 . group $
1235 enclose lparen rparen (group . align $ bindingOf n False <+> colon <+> prettySe 10 bnd ty) <+>
1236 st <> text "->" <$> prettySe 10 ((n, False):bnd) sc
1237 | otherwise =
1238 bracket p 2 . group $
1239 group (prettySe 1 bnd ty <+> st) <> text "->" <$> group (prettySe 10 ((n, False):bnd) sc)
1240 where
1241 st =
1242 case s of
1243 Static -> text "[static]" <> space
1244 _ -> empty
1245 prettySe p bnd (PPi (Imp l s _) n ty sc)
1246 | ppopt_impl ppo =
1247 bracket p 2 $
1248 lbrace <> bindingOf n True <+> colon <+> prettySe 10 bnd ty <> rbrace <+>
1249 st <> text "->" </> prettySe 10 ((n, True):bnd) sc
1250 | otherwise = prettySe 10 ((n, True):bnd) sc
1251 where
1252 st =
1253 case s of
1254 Static -> text "[static]" <> space
1255 _ -> empty
1256 prettySe p bnd (PPi (Constraint _ _) n ty sc) =
1257 bracket p 2 $
1258 prettySe 10 bnd ty <+> text "=>" </> prettySe 10 ((n, True):bnd) sc
1259 prettySe p bnd (PPi (TacImp _ _ s) n ty sc) =
1260 bracket p 2 $
1261 lbrace <> kwd "tacimp" <+> pretty n <+> colon <+> prettySe 10 bnd ty <>
1262 rbrace <+> text "->" </> prettySe 10 ((n, True):bnd) sc
1263 prettySe p bnd (PApp _ (PRef _ f) args) -- normal names, no explicit args
1264 | UN nm <- basename f
1265 , not (ppopt_impl ppo) && null (getShowArgs args) =
1266 prettyName True (ppopt_impl ppo) bnd f
1267 prettySe p bnd (PAppBind _ (PRef _ f) [])
1268 | not (ppopt_impl ppo) = text "!" <> prettyName True (ppopt_impl ppo) bnd f
1269 prettySe p bnd (PApp _ (PRef _ op) args) -- infix operators
1270 | UN nm <- basename op
1271 , not (tnull nm) &&
1272 (not (ppopt_impl ppo)) && (not $ isAlpha (thead nm)) =
1273 case getShowArgs args of
1274 [] -> opName True
1275 [x] -> group (opName True <$> group (prettySe 0 bnd (getTm x)))
1276 [l,r] -> let precedence = fromMaybe 20 (fmap prec f)
1277 in bracket p precedence $ inFix (getTm l) (getTm r)
1278 (l@(PExp _ _ _ _) : r@(PExp _ _ _ _) : rest) ->
1279 bracket p 1 $
1280 enclose lparen rparen (inFix (getTm l) (getTm r)) <+>
1281 align (group (vsep (map (prettyArgS bnd) rest)))
1282 as -> opName True <+> align (vsep (map (prettyArgS bnd) as))
1283 where opName isPrefix = prettyName isPrefix (ppopt_impl ppo) bnd op
1284 f = getFixity (opStr op)
1285 left l = case f of
1286 Nothing -> prettySe (-1) bnd l
1287 Just (Infixl p') -> prettySe p' bnd l
1288 Just f' -> prettySe (prec f'-1) bnd l
1289 right r = case f of
1290 Nothing -> prettySe (-1) bnd r
1291 Just (Infixr p') -> prettySe p' bnd r
1292 Just f' -> prettySe (prec f'-1) bnd r
1293 inFix l r = align . group $
1294 (left l <+> opName False) <$> group (right r)
1295 prettySe p bnd (PApp _ hd@(PRef fc f) [tm]) -- symbols, like 'foo
1296 | PConstant (Idris.Core.TT.Str str) <- getTm tm,
1297 f == sUN "Symbol_" = annotate (AnnType ("'" ++ str) ("The symbol " ++ str)) $
1298 char '\'' <> prettySe 10 bnd (PRef fc (sUN str))
1299 prettySe p bnd (PApp _ f as) = -- Normal prefix applications
1300 let args = getShowArgs as
1301 fp = prettySe 1 bnd f
1302 in
1303 bracket p 1 . group $
1304 if ppopt_impl ppo
1305 then if null as
1306 then fp
1307 else fp <+> align (vsep (map (prettyArgS bnd) as))
1308 else if null args
1309 then fp
1310 else fp <+> align (vsep (map (prettyArgS bnd) args))
1311 prettySe p bnd (PCase _ scr opts) =
1312 kwd "case" <+> prettySe 10 bnd scr <+> kwd "of" <> prettyBody
1313 where
1314 prettyBody = foldr (<>) empty $ intersperse (text "|") $ map sc opts
1316 sc (l, r) = nest nestingSize $ prettySe 10 bnd l <+> text "=>" <+> prettySe 10 bnd r
1317 prettySe p bnd (PHidden tm) = text "." <> prettySe 0 bnd tm
1318 prettySe p bnd (PRefl _ _) = annName eqCon $ text "refl"
1319 prettySe p bnd (PResolveTC _) = text "resolvetc"
1320 prettySe p bnd (PTrue _ IsType) = annName unitTy $ text "()"
1321 prettySe p bnd (PTrue _ IsTerm) = annName unitCon $ text "()"
1322 prettySe p bnd (PTrue _ TypeOrTerm) = text "()"
1323 prettySe p bnd (PFalse _) = annName falseTy $ text "_|_"
1324 prettySe p bnd (PEq _ _ _ l r) =
1325 bracket p 2 . align . group $
1326 prettySe 10 bnd l <+> eq <$> group (prettySe 10 bnd r)
1327 where eq = annName eqTy (text "=")
1328 prettySe p bnd (PRewrite _ l r _) =
1329 bracket p 2 $
1330 text "rewrite" <+> prettySe 10 bnd l <+> text "in" <+> prettySe 10 bnd r
1331 prettySe p bnd (PTyped l r) =
1332 lparen <> prettySe 10 bnd l <+> colon <+> prettySe 10 bnd r <> rparen
1333 prettySe p bnd pair@(PPair _ pun _ _) -- flatten tuples to the right, like parser
1334 | Just elts <- pairElts pair = enclose (ann lparen) (ann rparen) .
1335 align . group . vsep . punctuate (ann comma) $
1336 map (prettySe 10 bnd) elts
1337 where ann = case pun of
1338 TypeOrTerm -> id
1339 IsType -> annName pairTy
1340 IsTerm -> annName pairCon
1341 prettySe p bnd (PDPair _ TypeOrTerm l t r) =
1342 lparen <> prettySe 10 bnd l <+> text "**" <+> prettySe 10 bnd r <> rparen
1343 prettySe p bnd (PDPair _ IsType (PRef _ n) t r) =
1344 annName sigmaTy lparen <>
1345 bindingOf n False <+>
1346 annName sigmaTy (text "**") <+>
1347 prettySe 10 ((n, False):bnd) r <>
1348 annName sigmaTy rparen
1349 prettySe p bnd (PDPair _ IsType l t r) =
1350 annName sigmaTy lparen <>
1351 prettySe 10 bnd l <+>
1352 annName sigmaTy (text "**") <+>
1353 prettySe 10 bnd r <>
1354 annName sigmaTy rparen
1355 prettySe p bnd (PDPair _ IsTerm l t r) =
1356 annName existsCon lparen <>
1357 prettySe 10 bnd l <+>
1358 annName existsCon (text "**") <+>
1359 prettySe 10 bnd r <>
1360 annName existsCon rparen
1361 prettySe p bnd (PAlternative a as) =
1362 lparen <> text "|" <> prettyAs <> text "|" <> rparen
1363 where
1364 prettyAs =
1365 foldr (\l -> \r -> l <+> text "," <+> r) empty $ map (prettySe 10 bnd) as
1366 prettySe p bnd PType = annotate (AnnType "Type" "The type of types") $ text "Type"
1367 prettySe p bnd (PConstant c) = annotate (AnnConst c) (text (show c))
1368 -- XXX: add pretty for tactics
1369 prettySe p bnd (PProof ts) =
1370 text "proof" <+> lbrace <> nest nestingSize (text . show $ ts) <> rbrace
1371 prettySe p bnd (PTactics ts) =
1372 text "tactics" <+> lbrace <> nest nestingSize (text . show $ ts) <> rbrace
1373 prettySe p bnd (PMetavar n) = text "?" <> pretty n
1374 prettySe p bnd (PReturn f) = kwd "return"
1375 prettySe p bnd PImpossible = kwd "impossible"
1376 prettySe p bnd Placeholder = text "_"
1377 prettySe p bnd (PDoBlock _) = text "do block pretty not implemented"
1378 prettySe p bnd (PCoerced t) = prettySe p bnd t
1379 prettySe p bnd (PElabError s) = pretty s
1380 -- Quasiquote pprinting ignores bound vars
1381 prettySe p bnd (PQuasiquote t Nothing) = text "`(" <> prettySe p [] t <> text ")"
1382 prettySe p bnd (PQuasiquote t (Just g)) = text "`(" <> prettySe p [] t <+> colon <+> prettySe p [] g <> text ")"
1383 prettySe p bnd (PUnquote t) = text "~" <> prettySe p bnd t
1385 prettySe p bnd _ = text "missing pretty-printer for term"
1387 prettyArgS bnd (PImp _ _ _ n tm) = prettyArgSi bnd (n, tm)
1388 prettyArgS bnd (PExp _ _ _ tm) = prettyArgSe bnd tm
1389 prettyArgS bnd (PConstraint _ _ _ tm) = prettyArgSc bnd tm
1390 prettyArgS bnd (PTacImplicit _ _ n _ tm) = prettyArgSti bnd (n, tm)
1392 prettyArgSe bnd arg = prettySe 0 bnd arg
1393 prettyArgSi bnd (n, val) = lbrace <> pretty n <+> text "=" <+> prettySe 10 bnd val <> rbrace
1394 prettyArgSc bnd val = lbrace <> lbrace <> prettySe 10 bnd val <> rbrace <> rbrace
1395 prettyArgSti bnd (n, val) = lbrace <> kwd "auto" <+> pretty n <+> text "=" <+> prettySe 10 bnd val <> rbrace
1397 annName :: Name -> Doc OutputAnnotation -> Doc OutputAnnotation
1398 annName n = annotate (AnnName n Nothing Nothing Nothing)
1400 opStr :: Name -> String
1401 opStr (NS n _) = opStr n
1402 opStr (UN n) = T.unpack n
1404 basename :: Name -> Name
1405 basename (NS n _) = basename n
1406 basename n = n
1408 slist' p bnd (PApp _ (PRef _ nil) _)
1409 | not (ppopt_impl ppo) && nsroot nil == sUN "Nil" = Just []
1410 slist' p bnd (PRef _ nil)
1411 | not (ppopt_impl ppo) && nsroot nil == sUN "Nil" = Just []
1412 slist' p bnd (PApp _ (PRef _ cons) args)
1413 | nsroot cons == sUN "::",
1414 (PExp {getTm=tl}):(PExp {getTm=hd}):imps <- reverse args,
1415 all isImp imps,
1416 Just tl' <- slist' p bnd tl
1417 = Just (hd:tl')
1418 where
1419 isImp (PImp {}) = True
1420 isImp _ = False
1421 slist' _ _ tm = Nothing
1423 slist p bnd e | Just es <- slist' p bnd e = Just $
1424 case es of [] -> annotate (AnnData "" "") $ text "[]"
1425 [x] -> enclose left right . group $
1426 prettySe p bnd x
1427 xs -> (enclose left right .
1428 align . group . vsep .
1429 punctuate comma .
1430 map (prettySe p bnd)) xs
1431 where left = (annotate (AnnData "" "") (text "["))
1432 right = (annotate (AnnData "" "") (text "]"))
1433 comma = (annotate (AnnData "" "") (text ","))
1434 slist _ _ _ = Nothing
1436 pairElts :: PTerm -> Maybe [PTerm]
1437 pairElts (PPair _ _ x y) | Just elts <- pairElts y = Just (x:elts)
1438 | otherwise = Just [x, y]
1439 pairElts _ = Nothing
1441 natns = "Prelude.Nat."
1443 snat p (PRef _ z)
1444 | show z == (natns++"Z") || show z == "Z" = Just 0
1445 snat p (PApp _ s [PExp {getTm=n}])
1446 | show s == (natns++"S") || show s == "S",
1447 Just n' <- snat p n
1448 = Just $ 1 + n'
1449 snat _ _ = Nothing
1451 bracket outer inner doc
1452 | inner > outer = lparen <> doc <> rparen
1453 | otherwise = doc
1455 kwd = annotate AnnKeyword . text
1457 fixities :: M.Map String Fixity
1458 fixities = M.fromList [(s, f) | (Fix f s) <- infixes]
1460 getFixity :: String -> Maybe Fixity
1461 getFixity = flip M.lookup fixities
1463prettyDocumentedIst :: IState -> (Name, PTerm, Maybe Docstring) -> Doc OutputAnnotation
1464prettyDocumentedIst ist (name, ty, docs) =
1465 prettyName True True [] name <+> colon <+> align (prettyIst ist ty) <$>
1466 fromMaybe empty (fmap (\d -> renderDocstring d <> line) docs)
1468-- | Pretty-printer helper for the binding site of a name
1469bindingOf :: Name -- ^^ the bound name
1470 -> Bool -- ^^ whether the name is implicit
1471 -> Doc OutputAnnotation
1472bindingOf n imp = annotate (AnnBoundName n imp) (text (show n))
1474-- | Pretty-printer helper for names that attaches the correct annotations
1475prettyName
1476 :: Bool -- ^^ whether the name should be parenthesised if it is an infix operator
1477 -> Bool -- ^^ whether to show namespaces
1478 -> [(Name, Bool)] -- ^^ the current bound variables and whether they are implicit
1479 -> Name -- ^^ the name to pprint
1480 -> Doc OutputAnnotation
1481prettyName infixParen showNS bnd n
1482 | Just imp <- lookup n bnd = annotate (AnnBoundName n imp) fullName
1483 | otherwise = annotate (AnnName n Nothing Nothing Nothing) fullName
1484 where fullName = text nameSpace <> parenthesise (text (baseName n))
1485 baseName (UN n) = T.unpack n
1486 baseName (NS n ns) = baseName n
1487 baseName (MN i s) = T.unpack s
1488 baseName n | n == falseTy = "_|_"
1489 baseName other = show other
1490 nameSpace = case n of
1491 (NS n' ns) -> if showNS then (concatMap (++ ".") . map T.unpack . reverse) ns else ""
1492 _ -> ""
1493 isInfix = case baseName n of
1494 "" -> False
1495 (c : _) -> not (isAlpha c)
1496 parenthesise = if isInfix && infixParen then enclose lparen rparen else id
1499showCImp :: PPOption -> PClause -> Doc OutputAnnotation
1500showCImp ppo (PClause _ n l ws r w)
1501 = prettyImp ppo l <+> showWs ws <+> text "=" <+> prettyImp ppo r
1502 <+> text "where" <+> text (show w)
1503 where
1504 showWs [] = empty
1505 showWs (x : xs) = text "|" <+> prettyImp ppo x <+> showWs xs
1506showCImp ppo (PWith _ n l ws r w)
1507 = prettyImp ppo l <+> showWs ws <+> text "with" <+> prettyImp ppo r
1508 <+> braces (text (show w))
1509 where
1510 showWs [] = empty
1511 showWs (x : xs) = text "|" <+> prettyImp ppo x <+> showWs xs
1514showDImp :: PPOption -> PData -> Doc OutputAnnotation
1515showDImp ppo (PDatadecl n ty cons)
1516 = text "data" <+> text (show n) <+> colon <+> prettyImp ppo ty <+> text "where" <$>
1517 (indent 2 $ vsep (map (\ (_, _, n, t, _, _) -> pipe <+> prettyName True False [] n <+> colon <+> prettyImp ppo t) cons))
1519showDecls :: PPOption -> [PDecl] -> Doc OutputAnnotation
1520showDecls o ds = vsep (map (showDeclImp o) ds)
1522showDeclImp _ (PFix _ f ops) = text (show f) <+> cat (punctuate (text ",") (map text ops))
1523showDeclImp o (PTy _ _ _ _ _ n t) = text "tydecl" <+> text (showCG n) <+> colon <+> prettyImp o t
1524showDeclImp o (PClauses _ _ n cs) = text "pat" <+> text (showCG n) <+> text "\t" <+>
1525 indent 2 (vsep (map (showCImp o) cs))
1526showDeclImp o (PData _ _ _ _ _ d) = showDImp o { ppopt_impl = True } d
1527showDeclImp o (PParams _ ns ps) = text "params" <+> braces (text (show ns) <> line <> showDecls o ps <> line)
1528showDeclImp o (PNamespace n ps) = text "namespace" <+> text n <> braces (line <> showDecls o ps <> line)
1529showDeclImp _ (PSyntax _ syn) = text "syntax" <+> text (show syn)
1530showDeclImp o (PClass _ _ _ cs n ps _ ds)
1531 = text "class" <+> text (show cs) <+> text (show n) <+> text (show ps) <> line <> showDecls o ds
1532showDeclImp o (PInstance _ _ cs n _ t _ ds)
1533 = text "instance" <+> text (show cs) <+> text (show n) <+> prettyImp o t <> line <> showDecls o ds
1534showDeclImp _ _ = text "..."
1535-- showDeclImp (PImport o) = "import " ++ o
1537instance Show (Doc OutputAnnotation) where
1538 show = flip (displayS . renderCompact) ""
1540getImps :: [PArg] -> [(Name, PTerm)]
1541getImps [] = []
1542getImps (PImp _ _ _ n tm : xs) = (n, tm) : getImps xs
1543getImps (_ : xs) = getImps xs
1545getExps :: [PArg] -> [PTerm]
1546getExps [] = []
1547getExps (PExp _ _ _ tm : xs) = tm : getExps xs
1548getExps (_ : xs) = getExps xs
1550getShowArgs :: [PArg] -> [PArg]
1551getShowArgs [] = []
1552getShowArgs (e@(PExp _ _ _ tm) : xs) = e : getShowArgs xs
1553getShowArgs (e : xs) | AlwaysShow `elem` argopts e = e : getShowArgs xs
1554getShowArgs (_ : xs) = getShowArgs xs
1556getConsts :: [PArg] -> [PTerm]
1557getConsts [] = []
1558getConsts (PConstraint _ _ _ tm : xs) = tm : getConsts xs
1559getConsts (_ : xs) = getConsts xs
1561getAll :: [PArg] -> [PTerm]
1562getAll = map getTm
1565-- | Show Idris name
1566showName :: Maybe IState -- ^^ the Idris state, for information about names and colours
1567 -> [(Name, Bool)] -- ^^ the bound variables and whether they're implicit
1568 -> PPOption -- ^^ pretty printing options
1569 -> Bool -- ^^ whether to colourise
1570 -> Name -- ^^ the term to show
1571 -> String
1572showName ist bnd ppo colour n = case ist of
1573 Just i -> if colour then colourise n (idris_colourTheme i) else showbasic n
1574 Nothing -> showbasic n
1575 where name = if ppopt_impl ppo then show n else showbasic n
1576 showbasic n@(UN _) = showCG n
1577 showbasic (MN i s) = str s
1578 showbasic (NS n s) = showSep "." (map str (reverse s)) ++ "." ++ showbasic n
1579 showbasic (SN s) = show s
1580 fst3 (x, _, _) = x
1581 colourise n t = let ctxt' = fmap tt_ctxt ist in
1582 case ctxt' of
1583 Nothing -> name
1584 Just ctxt | Just impl <- lookup n bnd -> if impl then colouriseImplicit t name
1585 else colouriseBound t name
1586 | isDConName n ctxt -> colouriseData t name
1587 | isFnName n ctxt -> colouriseFun t name
1588 | isTConName n ctxt -> colouriseType t name
1589 -- The assumption is that if a name is not bound and does not exist in the
1590 -- global context, then we're somewhere in which implicit info has been lost
1591 -- (like error messages). Thus, unknown vars are colourised as implicits.
1592 | otherwise -> colouriseImplicit t name
1594showTm :: IState -- ^^ the Idris state, for information about identifiers and colours
1595 -> PTerm -- ^^ the term to show
1596 -> String
1597showTm ist = displayDecorated (consoleDecorate ist) .
1598 renderPretty 0.8 100000 .
1599 prettyImp (ppOptionIst ist)
1601-- | Show a term with implicits, no colours
1602showTmImpls :: PTerm -> String
1603showTmImpls = flip (displayS . renderCompact . prettyImp verbosePPOption) ""
1607instance Sized PTerm where
1608 size (PQuote rawTerm) = size rawTerm
1609 size (PRef fc name) = size name
1610 size (PLam name ty bdy) = 1 + size ty + size bdy
1611 size (PPi plicity name ty bdy) = 1 + size ty + size bdy
1612 size (PLet name ty def bdy) = 1 + size ty + size def + size bdy
1613 size (PTyped trm ty) = 1 + size trm + size ty
1614 size (PApp fc name args) = 1 + size args
1615 size (PAppBind fc name args) = 1 + size args
1616 size (PCase fc trm bdy) = 1 + size trm + size bdy
1617 size (PTrue fc _) = 1
1618 size (PFalse fc) = 1
1619 size (PRefl fc _) = 1
1620 size (PResolveTC fc) = 1
1621 size (PEq fc _ _ left right) = 1 + size left + size right
1622 size (PRewrite fc left right _) = 1 + size left + size right
1623 size (PPair fc _ left right) = 1 + size left + size right
1624 size (PDPair fs _ left ty right) = 1 + size left + size ty + size right
1625 size (PAlternative a alts) = 1 + size alts
1626 size (PHidden hidden) = size hidden
1627 size (PUnifyLog tm) = size tm
1628 size (PDisamb _ tm) = size tm
1629 size (PNoImplicits tm) = size tm
1630 size PType = 1
1631 size (PConstant const) = 1 + size const
1632 size Placeholder = 1
1633 size (PDoBlock dos) = 1 + size dos
1634 size (PIdiom fc term) = 1 + size term
1635 size (PReturn fc) = 1
1636 size (PMetavar name) = 1
1637 size (PProof tactics) = size tactics
1638 size (PElabError err) = size err
1639 size PImpossible = 1
1641getPArity :: PTerm -> Int
1642getPArity (PPi _ _ _ sc) = 1 + getPArity sc
1643getPArity _ = 0
1645-- Return all names, free or globally bound, in the given term.
1647allNamesIn :: PTerm -> [Name]
1648allNamesIn tm = nub $ ni [] tm
1649 where -- TODO THINK added niTacImp, but is it right?
1650 ni env (PRef _ n)
1651 | not (n `elem` env) = [n]
1652 ni env (PPatvar _ n) = [n]
1653 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
1654 ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
1655 ni env (PCase _ c os) = ni env c ++ concatMap (ni env) (map snd os)
1656 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc
1657 ni env (PPi p n ty sc) = niTacImp env p ++ ni env ty ++ ni (n:env) sc
1658 ni env (PHidden tm) = ni env tm
1659 ni env (PEq _ _ _ l r) = ni env l ++ ni env r
1660 ni env (PRewrite _ l r _) = ni env l ++ ni env r
1661 ni env (PTyped l r) = ni env l ++ ni env r
1662 ni env (PPair _ _ l r) = ni env l ++ ni env r
1663 ni env (PDPair _ _ (PRef _ n) t r) = ni env t ++ ni (n:env) r
1664 ni env (PDPair _ _ l t r) = ni env l ++ ni env t ++ ni env r
1665 ni env (PAlternative a ls) = concatMap (ni env) ls
1666 ni env (PUnifyLog tm) = ni env tm
1667 ni env (PDisamb _ tm) = ni env tm
1668 ni env (PNoImplicits tm) = ni env tm
1669 ni env _ = []
1671 niTacImp env (TacImp _ _ scr) = ni env scr
1672 niTacImp _ _ = []
1674-- Return all names defined in binders in the given term
1675boundNamesIn :: PTerm -> [Name]
1676boundNamesIn tm = nub $ ni tm
1677 where -- TODO THINK Added niTacImp, but is it right?
1678 ni (PApp _ f as) = ni f ++ concatMap (ni) (map getTm as)
1679 ni (PAppBind _ f as) = ni f ++ concatMap (ni) (map getTm as)
1680 ni (PCase _ c os) = ni c ++ concatMap (ni) (map snd os)
1681 ni (PLam n ty sc) = n : (ni ty ++ ni sc)
1682 ni (PLet n ty val sc) = n : (ni ty ++ ni val ++ ni sc)
1683 ni (PPi p n ty sc) = niTacImp p ++ (n : (ni ty ++ ni sc))
1684 ni (PEq _ _ _ l r) = ni l ++ ni r
1685 ni (PRewrite _ l r _) = ni l ++ ni r
1686 ni (PTyped l r) = ni l ++ ni r
1687 ni (PPair _ _ l r) = ni l ++ ni r
1688 ni (PDPair _ _ (PRef _ n) t r) = ni t ++ ni r
1689 ni (PDPair _ _ l t r) = ni l ++ ni t ++ ni r
1690 ni (PAlternative a as) = concatMap (ni) as
1691 ni (PHidden tm) = ni tm
1692 ni (PUnifyLog tm) = ni tm
1693 ni (PDisamb _ tm) = ni tm
1694 ni (PNoImplicits tm) = ni tm
1695 ni _ = []
1697 niTacImp (TacImp _ _ scr) = ni scr
1698 niTacImp _ = []
1700-- Return names which are valid implicits in the given term (type).
1701implicitNamesIn :: [Name] -> IState -> PTerm -> [Name]
1702implicitNamesIn uvars ist tm = nub $ ni [] tm
1703 where
1704 ni env (PRef _ n)
1705 | not (n `elem` env)
1706 = case lookupTy n (tt_ctxt ist) of
1707 [] -> [n]
1708 _ -> if n `elem` uvars then [n] else []
1709 ni env (PApp _ f@(PRef _ n) as)
1710 | n `elem` uvars = ni env f ++ concatMap (ni env) (map getTm as)
1711 | otherwise = concatMap (ni env) (map getTm as)
1712 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
1713 ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
1714 ni env (PCase _ c os) = ni env c ++
1715 -- names in 'os', not counting the names bound in the cases
1716 (nub (concatMap (ni env) (map snd os))
1717 \\ nub (concatMap (ni env) (map fst os)))
1718 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc
1719 ni env (PPi p n ty sc) = niTacImp env p ++ ni env ty ++ ni (n:env) sc
1720 ni env (PEq _ _ _ l r) = ni env l ++ ni env r
1721 ni env (PRewrite _ l r _) = ni env l ++ ni env r
1722 ni env (PTyped l r) = ni env l ++ ni env r
1723 ni env (PPair _ _ l r) = ni env l ++ ni env r
1724 ni env (PDPair _ _ (PRef _ n) t r) = ni env t ++ ni (n:env) r
1725 ni env (PDPair _ _ l t r) = ni env l ++ ni env t ++ ni env r
1726 ni env (PAlternative a as) = concatMap (ni env) as
1727 ni env (PHidden tm) = ni env tm
1728 ni env (PUnifyLog tm) = ni env tm
1729 ni env (PDisamb _ tm) = ni env tm
1730 ni env (PNoImplicits tm) = ni env tm
1731 ni env _ = []
1733 niTacImp env (TacImp _ _ scr) = ni env scr
1734 niTacImp _ _ = []
1736-- Return names which are free in the given term.
1737namesIn :: [(Name, PTerm)] -> IState -> PTerm -> [Name]
1738namesIn uvars ist tm = nub $ ni [] tm
1739 where
1740 ni env (PRef _ n)
1741 | not (n `elem` env)
1742 = case lookupTy n (tt_ctxt ist) of
1743 [] -> [n]
1744 _ -> if n `elem` (map fst uvars) then [n] else []
1745 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
1746 ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
1747 ni env (PCase _ c os) = ni env c ++
1748 -- names in 'os', not counting the names bound in the cases
1749 (nub (concatMap (ni env) (map snd os))
1750 \\ nub (concatMap (ni env) (map fst os)))
1751 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc
1752 ni env (PPi p n ty sc) = niTacImp env p ++ ni env ty ++ ni (n:env) sc
1753 ni env (PEq _ _ _ l r) = ni env l ++ ni env r
1754 ni env (PRewrite _ l r _) = ni env l ++ ni env r
1755 ni env (PTyped l r) = ni env l ++ ni env r
1756 ni env (PPair _ _ l r) = ni env l ++ ni env r
1757 ni env (PDPair _ _ (PRef _ n) t r) = ni env t ++ ni (n:env) r
1758 ni env (PDPair _ _ l t r) = ni env l ++ ni env t ++ ni env r
1759 ni env (PAlternative a as) = concatMap (ni env) as
1760 ni env (PHidden tm) = ni env tm
1761 ni env (PUnifyLog tm) = ni env tm
1762 ni env (PDisamb _ tm) = ni env tm
1763 ni env (PNoImplicits tm) = ni env tm
1764 ni env _ = []
1766 niTacImp env (TacImp _ _ scr) = ni env scr
1767 niTacImp _ _ = []
1769-- Return which of the given names are used in the given term.
1771usedNamesIn :: [Name] -> IState -> PTerm -> [Name]
1772usedNamesIn vars ist tm = nub $ ni [] tm
1773 where -- TODO THINK added niTacImp, but is it right?
1774 ni env (PRef _ n)
1775 | n `elem` vars && not (n `elem` env)
1776 = case lookupDefExact n (tt_ctxt ist) of
1777 Nothing -> [n]
1778 _ -> []
1779 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
1780 ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
1781 ni env (PCase _ c os) = ni env c ++ concatMap (ni env) (map snd os)
1782 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc
1783 ni env (PPi p n ty sc) = niTacImp env p ++ ni env ty ++ ni (n:env) sc
1784 ni env (PEq _ _ _ l r) = ni env l ++ ni env r
1785 ni env (PRewrite _ l r _) = ni env l ++ ni env r
1786 ni env (PTyped l r) = ni env l ++ ni env r
1787 ni env (PPair _ _ l r) = ni env l ++ ni env r
1788 ni env (PDPair _ _ (PRef _ n) t r) = ni env t ++ ni (n:env) r
1789 ni env (PDPair _ _ l t r) = ni env l ++ ni env t ++ ni env r
1790 ni env (PAlternative a as) = concatMap (ni env) as
1791 ni env (PHidden tm) = ni env tm
1792 ni env (PUnifyLog tm) = ni env tm
1793 ni env (PDisamb _ tm) = ni env tm
1794 ni env (PNoImplicits tm) = ni env tm
1795 ni env _ = []
1797 niTacImp env (TacImp _ _ scr) = ni env scr
1798 niTacImp _ _ = []
1800-- Return the list of inaccessible (= dotted) positions for a name.
1801getErasureInfo :: IState -> Name -> [Int]
1802getErasureInfo ist n =
1803 case lookupCtxtExact n (idris_optimisation ist) of
1804 Just (Optimise inacc detagg) -> map fst inacc
1805 Nothing -> []