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