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