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