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