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