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