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