git.iko.soy/Idris-dev
on 30580db help sign in
Idris-dev/src/Idris/AbsSyntaxTree.hs
1807 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, mapMaybe)
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 DocTerm, [(Name, Docstring DocTerm)]),
162 idris_tyinfodata :: Ctxt TIData,
163 idris_fninfo :: Ctxt FnInfo,
164 idris_transforms :: Ctxt [(Term, Term)],
165 idris_totcheck :: [(FC, Name)], -- names to check totality on
166 idris_defertotcheck :: [(FC, Name)], -- names to check at the end
167 idris_totcheckfail :: [(FC, String)],
168 idris_options :: IOption,
169 idris_name :: Int,
170 idris_lineapps :: [((FilePath, Int), PTerm)],
171 -- ^ Full application LHS on source line
172 idris_metavars :: [(Name, (Maybe Name, Int, Bool))], -- ^ The currently defined but not proven metavariables
173 idris_coercions :: [Name],
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 "void"]
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 Name (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 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
367 | PPrint OutputFmt Int PTerm
368 | TransformInfo Name
370data OutputFmt = HTMLOutput | LaTeXOutput
372data Opt = Filename String
373 | Quiet
374 | NoBanner
375 | ColourREPL Bool
376 | Ideslave
377 | IdeslaveSocket
378 | ShowLibs
379 | ShowLibdir
380 | ShowIncs
381 | NoBasePkgs
382 | NoPrelude
383 | NoBuiltins -- only for the really primitive stuff!
384 | NoREPL
385 | OLogging Int
386 | Output String
387 | TypeCase
388 | TypeInType
389 | DefaultTotal
390 | DefaultPartial
391 | WarnPartial
392 | WarnReach
393 | NoCoverage
394 | ErrContext
395 | ShowImpl
396 | Verbose
397 | Port String -- REPL TCP port
398 | IBCSubDir String
399 | ImportDir String
400 | PkgBuild String
401 | PkgInstall String
402 | PkgClean String
403 | PkgCheck String
404 | PkgREPL String
405 | PkgMkDoc String -- IdrisDoc
406 | PkgTest String
407 | WarnOnly
408 | Pkg String
409 | BCAsm String
410 | DumpDefun String
411 | DumpCases String
412 | UseCodegen Codegen
413 | OutputTy OutputType
414 | Extension LanguageExt
415 | InterpretScript String
416 | EvalExpr String
417 | TargetTriple String
418 | TargetCPU String
419 | OptLevel Word
420 | Client String
421 | ShowOrigErr
422 | AutoWidth -- ^ Automatically adjust terminal width
423 | AutoSolve -- ^ Automatically issue "solve" tactic in interactive prover
424 deriving (Show, Eq)
426-- Parsed declarations
428data Fixity = Infixl { prec :: Int }
429 | Infixr { prec :: Int }
430 | InfixN { prec :: Int }
431 | PrefixN { prec :: Int }
432 deriving Eq
433{-!
434deriving instance Binary Fixity
435deriving instance NFData Fixity
436!-}
438instance Show Fixity where
439 show (Infixl i) = "infixl " ++ show i
440 show (Infixr i) = "infixr " ++ show i
441 show (InfixN i) = "infix " ++ show i
442 show (PrefixN i) = "prefix " ++ show i
444data FixDecl = Fix Fixity String
445 deriving Eq
447instance Show FixDecl where
448 show (Fix f s) = show f ++ " " ++ s
450{-!
451deriving instance Binary FixDecl
452deriving instance NFData FixDecl
453!-}
455instance Ord FixDecl where
456 compare (Fix x _) (Fix y _) = compare (prec x) (prec y)
459data Static = Static | Dynamic
460 deriving (Show, Eq)
461{-!
462deriving instance Binary Static
463deriving instance NFData Static
464!-}
466-- Mark bindings with their explicitness, and laziness
467data Plicity = Imp { pargopts :: [ArgOpt],
468 pstatic :: Static,
469 pparam :: Bool }
470 | Exp { pargopts :: [ArgOpt],
471 pstatic :: Static,
472 pparam :: Bool } -- this is a param (rather than index)
473 | Constraint { pargopts :: [ArgOpt],
474 pstatic :: Static }
475 | TacImp { pargopts :: [ArgOpt],
476 pstatic :: Static,
477 pscript :: PTerm }
478 deriving (Show, Eq)
480{-!
481deriving instance Binary Plicity
482deriving instance NFData Plicity
483!-}
485impl = Imp [] Dynamic False
486expl = Exp [] Dynamic False
487expl_param = Exp [] Dynamic True
488constraint = Constraint [] Dynamic
489tacimpl t = TacImp [] Dynamic t
491data FnOpt = Inlinable -- always evaluate when simplifying
492 | TotalFn | PartialFn | CoveringFn
493 | Coinductive | AssertTotal
494 | Dictionary -- type class dictionary, eval only when
495 -- a function argument, and further evaluation resutls
496 | Implicit -- implicit coercion
497 | NoImplicit -- do not apply implicit coercions
498 | CExport String -- export, with a C name
499 | ErrorHandler -- ^^ an error handler for use with the ErrorReflection extension
500 | ErrorReverse -- ^^ attempt to reverse normalise before showing in error
501 | Reflection -- a reflecting function, compile-time only
502 | Specialise [(Name, Maybe Int)] -- specialise it, freeze these names
503 | Constructor -- Data constructor type
504 deriving (Show, Eq)
505{-!
506deriving instance Binary FnOpt
507deriving instance NFData FnOpt
508!-}
510type FnOpts = [FnOpt]
512inlinable :: FnOpts -> Bool
513inlinable = elem Inlinable
515dictionary :: FnOpts -> Bool
516dictionary = elem Dictionary
519-- | Data declaration options
520data DataOpt = Codata -- ^ Set if the the data-type is coinductive
521 | DefaultEliminator -- ^ Set if an eliminator should be generated for data type
522 | DefaultCaseFun -- ^ Set if a case function should be generated for data type
523 | DataErrRev
524 deriving (Show, Eq)
526type DataOpts = [DataOpt]
528-- | Type provider - what to provide
529data ProvideWhat' t = ProvTerm t t -- ^ the first is the goal type, the second is the term
530 | ProvPostulate t -- ^ goal type must be Type, so only term
531 deriving (Show, Eq, Functor)
533type ProvideWhat = ProvideWhat' PTerm
535-- | Top-level declarations such as compiler directives, definitions,
536-- datatypes and typeclasses.
537data PDecl' t
538 = PFix FC Fixity [String] -- ^ Fixity declaration
539 | PTy (Docstring (Either Err PTerm)) [(Name, Docstring (Either Err PTerm))] SyntaxInfo FC FnOpts Name t -- ^ Type declaration
540 | PPostulate (Docstring (Either Err PTerm)) SyntaxInfo FC FnOpts Name t -- ^ Postulate
541 | PClauses FC FnOpts Name [PClause' t] -- ^ Pattern clause
542 | PCAF FC Name t -- ^ Top level constant
543 | PData (Docstring (Either Err PTerm)) [(Name, Docstring (Either Err PTerm))] SyntaxInfo FC DataOpts (PData' t) -- ^ Data declaration.
544 | PParams FC [(Name, t)] [PDecl' t] -- ^ Params block
545 | PNamespace String [PDecl' t] -- ^ New namespace
546 | PRecord (Docstring (Either Err PTerm)) SyntaxInfo FC Name t DataOpts (Docstring (Either Err PTerm)) Name t -- ^ Record declaration
547 | PClass (Docstring (Either Err PTerm)) SyntaxInfo FC
548 [t] -- constraints
549 Name
550 [(Name, t)] -- parameters
551 [(Name, Docstring (Either Err PTerm))] -- parameter docstrings
552 [PDecl' t] -- declarations
553 -- ^ Type class: arguments are documentation, syntax info, source location, constraints,
554 -- class name, parameters, method declarations
555 | PInstance SyntaxInfo FC [t] -- constraints
556 Name -- class
557 [t] -- parameters
558 t -- full instance type
559 (Maybe Name) -- explicit name
560 [PDecl' t]
561 -- ^ Instance declaration: arguments are syntax info, source location, constraints,
562 -- class name, parameters, full instance type, optional explicit name, and definitions
563 | PDSL Name (DSL' t) -- ^ DSL declaration
564 | PSyntax FC Syntax -- ^ Syntax definition
565 | PMutual FC [PDecl' t] -- ^ Mutual block
566 | PDirective (Idris ()) -- ^ Compiler directive. The parser inserts the corresponding action in the Idris monad.
567 | PProvider SyntaxInfo FC (ProvideWhat' t) Name -- ^ Type provider. The first t is the type, the second is the term
568 | PTransform FC Bool t t -- ^ Source-to-source transformation rule. If
569 -- bool is True, lhs and rhs must be convertible
570 deriving Functor
571{-!
572deriving instance Binary PDecl'
573deriving instance NFData PDecl'
574!-}
576-- For elaborator state
577type ElabD a = Elab' [PDecl] a
579-- | One clause of a top-level definition. Term arguments to constructors are:
580--
581-- 1. The whole application (missing for PClauseR and PWithR because they're within a "with" clause)
582--
583-- 2. The list of extra 'with' patterns
584--
585-- 3. The right-hand side
586--
587-- 4. The where block (PDecl' t)
589data PClause' t = PClause FC Name t [t] t [PDecl' t] -- ^ A normal top-level definition.
590 | PWith FC Name t [t] t [PDecl' t]
591 | PClauseR FC [t] t [PDecl' t]
592 | PWithR FC [t] t [PDecl' t]
593 deriving Functor
594{-!
595deriving instance Binary PClause'
596deriving instance NFData PClause'
597!-}
599-- | Data declaration
600data PData' t = PDatadecl { d_name :: Name, -- ^ The name of the datatype
601 d_tcon :: t, -- ^ Type constructor
602 d_cons :: [(Docstring (Either Err PTerm), [(Name, Docstring (Either Err PTerm))], Name, t, FC, [Name])] -- ^ Constructors
603 }
604 -- ^ Data declaration
605 | PLaterdecl { d_name :: Name, d_tcon :: t }
606 -- ^ "Placeholder" for data whose constructors are defined later
607 deriving Functor
608{-!
609deriving instance Binary PData'
610deriving instance NFData PData'
611!-}
613-- Handy to get a free function for applying PTerm -> PTerm functions
614-- across a program, by deriving Functor
616type PDecl = PDecl' PTerm
617type PData = PData' PTerm
618type PClause = PClause' PTerm
620-- get all the names declared in a decl
622declared :: PDecl -> [Name]
623declared (PFix _ _ _) = []
624declared (PTy _ _ _ _ _ n t) = [n]
625declared (PPostulate _ _ _ _ n t) = [n]
626declared (PClauses _ _ n _) = [] -- not a declaration
627declared (PCAF _ n _) = [n]
628declared (PData _ _ _ _ _ (PDatadecl n _ ts)) = n : map fstt ts
629 where fstt (_, _, a, _, _, _) = a
630declared (PData _ _ _ _ _ (PLaterdecl n _)) = [n]
631declared (PParams _ _ ds) = concatMap declared ds
632declared (PNamespace _ ds) = concatMap declared ds
633declared (PRecord _ _ _ n _ _ _ c _) = [n, c]
634declared (PClass _ _ _ _ n _ _ ms) = n : concatMap declared ms
635declared (PInstance _ _ _ _ _ _ _ _) = []
636declared (PDSL n _) = [n]
637declared (PSyntax _ _) = []
638declared (PMutual _ ds) = concatMap declared ds
639declared (PDirective _) = []
641-- get the names declared, not counting nested parameter blocks
642tldeclared :: PDecl -> [Name]
643tldeclared (PFix _ _ _) = []
644tldeclared (PTy _ _ _ _ _ n t) = [n]
645tldeclared (PPostulate _ _ _ _ n t) = [n]
646tldeclared (PClauses _ _ n _) = [] -- not a declaration
647tldeclared (PRecord _ _ _ n _ _ _ c _) = [n, c]
648tldeclared (PData _ _ _ _ _ (PDatadecl n _ ts)) = n : map fstt ts
649 where fstt (_, _, a, _, _, _) = a
650tldeclared (PParams _ _ ds) = []
651tldeclared (PMutual _ ds) = concatMap tldeclared ds
652tldeclared (PNamespace _ ds) = concatMap tldeclared ds
653tldeclared (PClass _ _ _ _ n _ _ ms) = concatMap tldeclared ms
654tldeclared (PInstance _ _ _ _ _ _ _ _) = []
655tldeclared _ = []
657defined :: PDecl -> [Name]
658defined (PFix _ _ _) = []
659defined (PTy _ _ _ _ _ n t) = []
660defined (PPostulate _ _ _ _ n t) = []
661defined (PClauses _ _ n _) = [n] -- not a declaration
662defined (PCAF _ n _) = [n]
663defined (PData _ _ _ _ _ (PDatadecl n _ ts)) = n : map fstt ts
664 where fstt (_, _, a, _, _, _) = a
665defined (PData _ _ _ _ _ (PLaterdecl n _)) = []
666defined (PParams _ _ ds) = concatMap defined ds
667defined (PNamespace _ ds) = concatMap defined ds
668defined (PRecord _ _ _ n _ _ _ c _) = [n, c]
669defined (PClass _ _ _ _ n _ _ ms) = n : concatMap defined ms
670defined (PInstance _ _ _ _ _ _ _ _) = []
671defined (PDSL n _) = [n]
672defined (PSyntax _ _) = []
673defined (PMutual _ ds) = concatMap defined ds
674defined (PDirective _) = []
675--defined _ = []
677updateN :: [(Name, Name)] -> Name -> Name
678updateN ns n | Just n' <- lookup n ns = n'
679updateN _ n = n
681updateNs :: [(Name, Name)] -> PTerm -> PTerm
682updateNs [] t = t
683updateNs ns t = mapPT updateRef t
684 where updateRef (PRef fc f) = PRef fc (updateN ns f)
685 updateRef t = t
687-- updateDNs :: [(Name, Name)] -> PDecl -> PDecl
688-- updateDNs [] t = t
689-- updateDNs ns (PTy s f n t) | Just n' <- lookup n ns = PTy s f n' t
690-- updateDNs ns (PClauses f n c) | Just n' <- lookup n ns = PClauses f n' (map updateCNs c)
691-- where updateCNs ns (PClause n l ts r ds)
692-- = PClause (updateN ns n) (fmap (updateNs ns) l)
693-- (map (fmap (updateNs ns)) ts)
694-- (fmap (updateNs ns) r)
695-- (map (updateDNs ns) ds)
696-- updateDNs ns c = c
698data PunInfo = IsType | IsTerm | TypeOrTerm deriving (Eq, Show)
700-- | High level language terms
701data PTerm = PQuote Raw -- ^ Inclusion of a core term into the high-level language
702 | PRef FC Name -- ^ A reference to a variable
703 | PInferRef FC Name -- ^ A name to be defined later
704 | PPatvar FC Name -- ^ A pattern variable
705 | PLam Name PTerm PTerm -- ^ A lambda abstraction
706 | PPi Plicity Name PTerm PTerm -- ^ (n : t1) -> t2
707 | PLet Name PTerm PTerm PTerm -- ^ A let binding
708 | PTyped PTerm PTerm -- ^ Term with explicit type
709 | PApp FC PTerm [PArg] -- ^ e.g. IO (), List Char, length x
710 | PAppBind FC PTerm [PArg] -- ^ implicitly bound application
711 | PMatchApp FC Name -- ^ Make an application by type matching
712 | PCase FC PTerm [(PTerm, PTerm)] -- ^ A case expression. Args are source location, scrutinee, and a list of pattern/RHS pairs
713 | PTrue FC PunInfo -- ^ Unit type..?
714 | PRefl FC PTerm -- ^ The canonical proof of the equality type
715 | PResolveTC FC -- ^ Solve this dictionary by type class resolution
716 | PEq FC PTerm PTerm PTerm PTerm -- ^ Heterogeneous equality type: A = B
717 | PRewrite FC PTerm PTerm (Maybe PTerm) -- ^ "rewrite" syntax, with optional result type
718 | PPair FC PunInfo PTerm PTerm -- ^ A pair (a, b) and whether it's a product type or a pair (solved by elaboration)
719 | PDPair FC PunInfo PTerm PTerm PTerm -- ^ A dependent pair (tm : a ** b) and whether it's a sigma type or a pair that inhabits one (solved by elaboration)
720 | PAlternative Bool [PTerm] -- ^ True if only one may work. (| A, B, C|)
721 | PHidden PTerm -- ^ Irrelevant or hidden pattern
722 | PType -- ^ 'Type' type
723 | PUniverse Universe -- ^ Some universe
724 | PGoal FC PTerm Name PTerm -- ^ quoteGoal, used for %reflection functions
725 | PConstant Const -- ^ Builtin types
726 | Placeholder -- ^ Underscore
727 | PDoBlock [PDo] -- ^ Do notation
728 | PIdiom FC PTerm -- ^ Idiom brackets
729 | PReturn FC
730 | PMetavar Name -- ^ A metavariable, ?name
731 | PProof [PTactic] -- ^ Proof script
732 | PTactics [PTactic] -- ^ As PProof, but no auto solving
733 | PElabError Err -- ^ Error to report on elaboration
734 | PImpossible -- ^ Special case for declaring when an LHS can't typecheck
735 | PCoerced PTerm -- ^ To mark a coerced argument, so as not to coerce twice
736 | PDisamb [[T.Text]] PTerm -- ^ Preferences for explicit namespaces
737 | PUnifyLog PTerm -- ^ dump a trace of unifications when building term
738 | PNoImplicits PTerm -- ^ never run implicit converions on the term
739 | PQuasiquote PTerm (Maybe PTerm) -- ^ `(Term [: Term])
740 | PUnquote PTerm -- ^ ,Term
741 deriving Eq
744{-!
745deriving instance Binary PTerm
746deriving instance NFData PTerm
747!-}
749mapPT :: (PTerm -> PTerm) -> PTerm -> PTerm
750mapPT f t = f (mpt t) where
751 mpt (PLam n t s) = PLam n (mapPT f t) (mapPT f s)
752 mpt (PPi p n t s) = PPi p n (mapPT f t) (mapPT f s)
753 mpt (PLet n ty v s) = PLet n (mapPT f ty) (mapPT f v) (mapPT f s)
754 mpt (PRewrite fc t s g) = PRewrite fc (mapPT f t) (mapPT f s)
755 (fmap (mapPT f) g)
756 mpt (PApp fc t as) = PApp fc (mapPT f t) (map (fmap (mapPT f)) as)
757 mpt (PAppBind fc t as) = PAppBind fc (mapPT f t) (map (fmap (mapPT f)) as)
758 mpt (PCase fc c os) = PCase fc (mapPT f c) (map (pmap (mapPT f)) os)
759 mpt (PEq fc lt rt l r) = PEq fc (mapPT f lt) (mapPT f rt) (mapPT f l) (mapPT f r)
760 mpt (PTyped l r) = PTyped (mapPT f l) (mapPT f r)
761 mpt (PPair fc p l r) = PPair fc p (mapPT f l) (mapPT f r)
762 mpt (PDPair fc p l t r) = PDPair fc p (mapPT f l) (mapPT f t) (mapPT f r)
763 mpt (PAlternative a as) = PAlternative a (map (mapPT f) as)
764 mpt (PHidden t) = PHidden (mapPT f t)
765 mpt (PDoBlock ds) = PDoBlock (map (fmap (mapPT f)) ds)
766 mpt (PProof ts) = PProof (map (fmap (mapPT f)) ts)
767 mpt (PTactics ts) = PTactics (map (fmap (mapPT f)) ts)
768 mpt (PUnifyLog tm) = PUnifyLog (mapPT f tm)
769 mpt (PDisamb ns tm) = PDisamb ns (mapPT f tm)
770 mpt (PNoImplicits tm) = PNoImplicits (mapPT f tm)
771 mpt (PGoal fc r n sc) = PGoal fc (mapPT f r) n (mapPT f sc)
772 mpt x = x
775data PTactic' t = Intro [Name] | Intros | Focus Name
776 | Refine Name [Bool] | Rewrite t | DoUnify
777 | Induction t
778 | CaseTac t
779 | Equiv t
780 | MatchRefine Name
781 | LetTac Name t | LetTacTy Name t t
782 | Exact t | Compute | Trivial | TCInstance
783 | ProofSearch Bool Bool Int (Maybe Name) [Name]
784 -- ^ the bool is whether to search recursively
785 | Solve
786 | Attack
787 | ProofState | ProofTerm | Undo
788 | Try (PTactic' t) (PTactic' t)
789 | TSeq (PTactic' t) (PTactic' t)
790 | ApplyTactic t -- see Language.Reflection module
791 | ByReflection t
792 | Reflect t
793 | Fill t
794 | GoalType String (PTactic' t)
795 | TCheck t
796 | TEval t
797 | TDocStr (Either Name Const)
798 | TSearch t
799 | Skip
800 | TFail [ErrorReportPart]
801 | Qed | Abandon
802 deriving (Show, Eq, Functor, Foldable, Traversable)
803{-!
804deriving instance Binary PTactic'
805deriving instance NFData PTactic'
806!-}
807instance Sized a => Sized (PTactic' a) where
808 size (Intro nms) = 1 + size nms
809 size Intros = 1
810 size (Focus nm) = 1 + size nm
811 size (Refine nm bs) = 1 + size nm + length bs
812 size (Rewrite t) = 1 + size t
813 size (Induction t) = 1 + size t
814 size (LetTac nm t) = 1 + size nm + size t
815 size (Exact t) = 1 + size t
816 size Compute = 1
817 size Trivial = 1
818 size Solve = 1
819 size Attack = 1
820 size ProofState = 1
821 size ProofTerm = 1
822 size Undo = 1
823 size (Try l r) = 1 + size l + size r
824 size (TSeq l r) = 1 + size l + size r
825 size (ApplyTactic t) = 1 + size t
826 size (Reflect t) = 1 + size t
827 size (Fill t) = 1 + size t
828 size Qed = 1
829 size Abandon = 1
830 size Skip = 1
831 size (TFail ts) = 1 + size ts
833type PTactic = PTactic' PTerm
835data PDo' t = DoExp FC t
836 | DoBind FC Name t
837 | DoBindP FC t t [(t,t)]
838 | DoLet FC Name t t
839 | DoLetP FC t t
840 deriving (Eq, Functor)
841{-!
842deriving instance Binary PDo'
843deriving instance NFData PDo'
844!-}
846instance Sized a => Sized (PDo' a) where
847 size (DoExp fc t) = 1 + size fc + size t
848 size (DoBind fc nm t) = 1 + size fc + size nm + size t
849 size (DoBindP fc l r alts) = 1 + size fc + size l + size r + size alts
850 size (DoLet fc nm l r) = 1 + size fc + size nm + size l + size r
851 size (DoLetP fc l r) = 1 + size fc + size l + size r
853type PDo = PDo' PTerm
855-- The priority gives a hint as to elaboration order. Best to elaborate
856-- things early which will help give a more concrete type to other
857-- variables, e.g. a before (interpTy a).
859data PArg' t = PImp { priority :: Int,
860 machine_inf :: Bool, -- true if the machine inferred it
861 argopts :: [ArgOpt],
862 pname :: Name, getTm :: t }
863 | PExp { priority :: Int,
864 argopts :: [ArgOpt],
865 pname :: Name,
866 getTm :: t }
867 | PConstraint { priority :: Int,
868 argopts :: [ArgOpt],
869 pname :: Name,
870 getTm :: t }
871 | PTacImplicit { priority :: Int,
872 argopts :: [ArgOpt],
873 pname :: Name,
874 getScript :: t,
875 getTm :: t }
876 deriving (Show, Eq, Functor)
878data ArgOpt = AlwaysShow | HideDisplay | InaccessibleArg
879 deriving (Show, Eq)
881instance Sized a => Sized (PArg' a) where
882 size (PImp p _ l nm trm) = 1 + size nm + size trm
883 size (PExp p l nm trm) = 1 + size nm + size trm
884 size (PConstraint p l nm trm) = 1 + size nm +size nm + size trm
885 size (PTacImplicit p l nm scr trm) = 1 + size nm + size scr + size trm
887{-!
888deriving instance Binary PArg'
889deriving instance NFData PArg'
890!-}
892pimp n t mach = PImp 1 mach [] n t
893pexp t = PExp 1 [] (sMN 0 "arg") t
894pconst t = PConstraint 1 [] (sMN 0 "carg") t
895ptacimp n s t = PTacImplicit 2 [] n s t
897type PArg = PArg' PTerm
899-- Type class data
901data ClassInfo = CI { instanceName :: Name,
902 class_methods :: [(Name, (FnOpts, PTerm))],
903 class_defaults :: [(Name, (Name, PDecl))], -- method name -> default impl
904 class_default_superclasses :: [PDecl],
905 class_params :: [Name],
906 class_instances :: [Name] }
907 deriving Show
908{-!
909deriving instance Binary ClassInfo
910deriving instance NFData ClassInfo
911!-}
913-- Type inference data
915data TIData = TIPartial -- ^ a function with a partially defined type
916 | TISolution [Term] -- ^ possible solutions to a metavariable in a type
917 deriving Show
919-- | Miscellaneous information about functions
920data FnInfo = FnInfo { fn_params :: [Int] }
921 deriving Show
922{-!
923deriving instance Binary FnInfo
924!-}
926data OptInfo = Optimise { inaccessible :: [(Int,Name)], -- includes names for error reporting
927 detaggable :: Bool }
928 deriving Show
929{-!
930deriving instance Binary OptInfo
931deriving instance NFData OptInfo
932!-}
935data TypeInfo = TI { con_names :: [Name],
936 codata :: Bool,
937 data_opts :: DataOpts,
938 param_pos :: [Int],
939 mutual_types :: [Name] }
940 deriving Show
941{-!
942deriving instance Binary TypeInfo
943deriving instance NFData TypeInfo
944!-}
946-- Syntactic sugar info
948data DSL' t = DSL { dsl_bind :: t,
949 dsl_return :: t,
950 dsl_apply :: t,
951 dsl_pure :: t,
952 dsl_var :: Maybe t,
953 index_first :: Maybe t,
954 index_next :: Maybe t,
955 dsl_lambda :: Maybe t,
956 dsl_let :: Maybe t,
957 dsl_pi :: Maybe t
958 }
959 deriving (Show, Functor)
960{-!
961deriving instance Binary DSL'
962deriving instance NFData DSL'
963!-}
965type DSL = DSL' PTerm
967data SynContext = PatternSyntax | TermSyntax | AnySyntax
968 deriving Show
969{-!
970deriving instance Binary SynContext
971deriving instance NFData SynContext
972!-}
974data Syntax = Rule [SSymbol] PTerm SynContext
975 deriving Show
977syntaxNames :: Syntax -> [Name]
978syntaxNames (Rule syms _ _) = mapMaybe ename syms
979 where ename (Keyword n) = Just n
980 ename _ = Nothing
981{-!
982deriving instance Binary Syntax
983deriving instance NFData Syntax
984!-}
986data SSymbol = Keyword Name
987 | Symbol String
988 | Binding Name
989 | Expr Name
990 | SimpleExpr Name
991 deriving Show
994{-!
995deriving instance Binary SSymbol
996deriving instance NFData SSymbol
997!-}
999initDSL = DSL (PRef f (sUN ">>="))
1000 (PRef f (sUN "return"))
1001 (PRef f (sUN "<$>"))
1002 (PRef f (sUN "pure"))
1003 Nothing
1004 Nothing
1005 Nothing
1006 Nothing
1007 Nothing
1008 Nothing
1009 where f = fileFC "(builtin)"
1011data Using = UImplicit Name PTerm
1012 | UConstraint Name [Name]
1013 deriving (Show, Eq)
1014{-!
1015deriving instance Binary Using
1016deriving instance NFData Using
1017!-}
1019data SyntaxInfo = Syn { using :: [Using],
1020 syn_params :: [(Name, PTerm)],
1021 syn_namespace :: [String],
1022 no_imp :: [Name],
1023 decoration :: Name -> Name,
1024 inPattern :: Bool,
1025 implicitAllowed :: Bool,
1026 maxline :: Maybe Int,
1027 mut_nesting :: Int,
1028 dsl_info :: DSL,
1029 syn_in_quasiquote :: Int }
1030 deriving Show
1031{-!
1032deriving instance NFData SyntaxInfo
1033deriving instance Binary SyntaxInfo
1034!-}
1036defaultSyntax = Syn [] [] [] [] id False False Nothing 0 initDSL 0
1038expandNS :: SyntaxInfo -> Name -> Name
1039expandNS syn n@(NS _ _) = n
1040expandNS syn n = case syn_namespace syn of
1041 [] -> n
1042 xs -> sNS n xs
1045-- For inferring types of things
1047bi = fileFC "builtin"
1049inferTy = sMN 0 "__Infer"
1050inferCon = sMN 0 "__infer"
1051inferDecl = PDatadecl inferTy
1052 PType
1053 [(emptyDocstring, [], inferCon, PPi impl (sMN 0 "iType") PType (
1054 PPi expl (sMN 0 "ival") (PRef bi (sMN 0 "iType"))
1055 (PRef bi inferTy)), bi, [])]
1056inferOpts = []
1058infTerm t = PApp bi (PRef bi inferCon) [pimp (sMN 0 "iType") Placeholder True, pexp t]
1059infP = P (TCon 6 0) inferTy (TType (UVal 0))
1061getInferTerm, getInferType :: Term -> Term
1062getInferTerm (Bind n b sc) = Bind n b $ getInferTerm sc
1063getInferTerm (App (App _ _) tm) = tm
1064getInferTerm tm = tm -- error ("getInferTerm " ++ show tm)
1066getInferType (Bind n b sc) = Bind n (toTy b) $ getInferType sc
1067 where toTy (Lam t) = Pi t (TType (UVar 0))
1068 toTy (PVar t) = PVTy t
1069 toTy b = b
1070getInferType (App (App _ ty) _) = ty
1074-- Handy primitives: Unit, False, Pair, MkPair, =, mkForeign
1076primNames = [eqTy, eqCon, inferTy, inferCon]
1078unitTy = sUN "Unit"
1079unitCon = sUN "MkUnit"
1081falseDoc = fmap (const $ Msg "") . parseDocstring . T.pack $
1082 "The empty type, also known as the trivially false proposition." ++
1083 "\n\n" ++
1084 "Use `void` or `absurd` to prove anything if you have a variable " ++
1085 "of type `Void` in scope."
1086falseTy = sUN "Void"
1088pairTy = sUN "Pair"
1089pairCon = sUN "MkPair"
1091eqTy = sUN "="
1092eqCon = sUN "Refl"
1093eqDoc = fmap (const (Left $ Msg "")) . parseDocstring . T.pack $
1094 "The propositional equality type. A proof that `x` = `y`." ++
1095 "\n\n" ++
1096 "To use such a proof, pattern-match on it, and the two equal things will " ++
1097 "then need to be the _same_ pattern." ++
1098 "\n\n" ++
1099 "**Note**: Idris's equality type is potentially _heterogeneous_, which means that it " ++
1100 "is possible to state equalities between values of potentially different " ++
1101 "types. However, Idris will attempt the homogeneous case unless it fails to typecheck." ++
1102 "\n\n" ++
1103 "You may need to use `(~=~)` to explicitly request heterogeneous equality."
1105eqDecl = PDatadecl eqTy (piBindp impl [(n "A", PType), (n "B", PType)]
1106 (piBind [(n "x", PRef bi (n "A")), (n "y", PRef bi (n "B"))]
1107 PType))
1108 [(reflDoc, reflParamDoc,
1109 eqCon, PPi impl (n "A") PType (
1110 PPi impl (n "x") (PRef bi (n "A"))
1111 (PApp bi (PRef bi eqTy) [pimp (n "A") Placeholder False,
1112 pimp (n "B") Placeholder False,
1113 pexp (PRef bi (n "x")),
1114 pexp (PRef bi (n "x"))])), bi, [])]
1115 where n a = sUN a
1116 reflDoc = annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $
1117 "A proof that `x` in fact equals `x`. To construct this, you must have already " ++
1118 "shown that both sides are in fact equal."
1119 reflParamDoc = [(n "A", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the type at which the equality is proven"),
1120 (n "x", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the element shown to be equal to itself.")]
1122eqParamDoc = [(n "A", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the type of the left side of the equality"),
1123 (n "B", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the type of the right side of the equality")
1125 where n a = sUN a
1127eqOpts = []
1129-- Defined in builtins.idr
1130sigmaTy = sUN "Sigma"
1131existsCon = sUN "MkSigma"
1133piBind :: [(Name, PTerm)] -> PTerm -> PTerm
1134piBind = piBindp expl
1136piBindp :: Plicity -> [(Name, PTerm)] -> PTerm -> PTerm
1137piBindp p [] t = t
1138piBindp p ((n, ty):ns) t = PPi p n ty (piBindp p ns t)
1141-- Pretty-printing declarations and terms
1143-- These "show" instances render to an absurdly wide screen because inserted line breaks
1144-- could interfere with interactive editing, which calls "show".
1146instance Show PTerm where
1147 showsPrec _ tm = (displayS . renderPretty 1.0 10000000 . prettyImp defaultPPOption) tm
1149instance Show PDecl where
1150 showsPrec _ d = (displayS . renderPretty 1.0 10000000 . showDeclImp verbosePPOption) d
1152instance Show PClause where
1153 showsPrec _ c = (displayS . renderPretty 1.0 10000000 . showCImp verbosePPOption) c
1155instance Show PData where
1156 showsPrec _ d = (displayS . renderPretty 1.0 10000000 . showDImp defaultPPOption) d
1158instance Pretty PTerm OutputAnnotation where
1159 pretty = prettyImp defaultPPOption
1161-- | Colourise annotations according to an Idris state. It ignores the names
1162-- in the annotation, as there's no good way to show extended information on a
1163-- terminal.
1164consoleDecorate :: IState -> OutputAnnotation -> String -> String
1165consoleDecorate ist _ | not (idris_colourRepl ist) = id
1166consoleDecorate ist (AnnConst c) = let theme = idris_colourTheme ist
1167 in if constIsType c
1168 then colouriseType theme
1169 else colouriseData theme
1170consoleDecorate ist (AnnData _ _) = colouriseData (idris_colourTheme ist)
1171consoleDecorate ist (AnnType _ _) = colouriseType (idris_colourTheme ist)
1172consoleDecorate ist (AnnBoundName _ True) = colouriseImplicit (idris_colourTheme ist)
1173consoleDecorate ist (AnnBoundName _ False) = colouriseBound (idris_colourTheme ist)
1174consoleDecorate ist AnnKeyword = colouriseKeyword (idris_colourTheme ist)
1175consoleDecorate ist (AnnName n _ _ _) = let ctxt = tt_ctxt ist
1176 theme = idris_colourTheme ist
1177 in case () of
1178 _ | isDConName n ctxt -> colouriseData theme
1179 _ | isFnName n ctxt -> colouriseFun theme
1180 _ | isTConName n ctxt -> colouriseType theme
1181 _ | isPostulateName n ist -> colourisePostulate theme
1182 _ | otherwise -> id -- don't colourise unknown names
1183consoleDecorate ist (AnnFC _) = id
1184consoleDecorate ist (AnnTextFmt fmt) = Idris.Colours.colourise (colour fmt)
1185 where colour BoldText = IdrisColour Nothing True False True False
1186 colour UnderlineText = IdrisColour Nothing True True False False
1187 colour ItalicText = IdrisColour Nothing True False False True
1188consoleDecorate ist (AnnTerm _ _) = id
1189consoleDecorate ist (AnnSearchResult _) = id
1190consoleDecorate ist (AnnErr _) = id
1192isPostulateName :: Name -> IState -> Bool
1193isPostulateName n ist = S.member n (idris_postulates ist)
1195-- | Pretty-print a high-level closed Idris term with no information about precedence/associativity
1196prettyImp :: PPOption -- ^^ pretty printing options
1197 -> PTerm -- ^^ the term to pretty-print
1198 -> Doc OutputAnnotation
1199prettyImp impl = pprintPTerm impl [] [] []
1201-- | Serialise something to base64 using its Binary instance.
1203-- | Do the right thing for rendering a term in an IState
1204prettyIst :: IState -> PTerm -> Doc OutputAnnotation
1205prettyIst ist = pprintPTerm (ppOptionIst ist) [] [] (idris_infixes ist)
1207-- | Pretty-print a high-level Idris term in some bindings context with infix info
1208pprintPTerm :: PPOption -- ^^ pretty printing options
1209 -> [(Name, Bool)] -- ^^ the currently-bound names and whether they are implicit
1210 -> [Name] -- ^^ names to always show in pi, even if not used
1211 -> [FixDecl] -- ^^ Fixity declarations
1212 -> PTerm -- ^^ the term to pretty-print
1213 -> Doc OutputAnnotation
1214pprintPTerm ppo bnd docArgs infixes = prettySe 10 bnd
1215 where
1216 prettySe :: Int -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation
1217 prettySe p bnd (PQuote r) =
1218 text "![" <> pretty r <> text "]"
1219 prettySe p bnd (PPatvar fc n) = pretty n
1220 prettySe p bnd e
1221 | Just str <- slist p bnd e = str
1222 | Just n <- snat p e = annotate (AnnData "Nat" "") (text (show n))
1223 prettySe p bnd (PRef fc n) = prettyName True (ppopt_impl ppo) bnd n
1224 prettySe p bnd (PLam n ty sc) =
1225 bracket p 2 . group . align . hang 2 $
1226 text "\\" <> bindingOf n False <+> text "=>" <$>
1227 prettySe 10 ((n, False):bnd) sc
1228 prettySe p bnd (PLet n ty v sc) =
1229 bracket p 2 . group . align $
1230 kwd "let" <+> (group . align . hang 2 $ bindingOf n False <+> text "=" <$> prettySe 10 bnd v) </>
1231 kwd "in" <+> (group . align . hang 2 $ prettySe 10 ((n, False):bnd) sc)
1232 prettySe p bnd (PPi (Exp l s _) n ty sc)
1233 | n `elem` allNamesIn sc || ppopt_impl ppo || n `elem` docArgs =
1234 bracket p 2 . group $
1235 enclose lparen rparen (group . align $ bindingOf n False <+> colon <+> prettySe 10 bnd ty) <+>
1236 st <> text "->" <$> prettySe 10 ((n, False):bnd) sc
1237 | otherwise =
1238 bracket p 2 . group $
1239 group (prettySe 1 bnd ty <+> st) <> text "->" <$> group (prettySe 10 ((n, False):bnd) sc)
1240 where
1241 st =
1242 case s of
1243 Static -> text "[static]" <> space
1244 _ -> empty
1245 prettySe p bnd (PPi (Imp l s _) n ty sc)
1246 | ppopt_impl ppo =
1247 bracket p 2 $
1248 lbrace <> bindingOf n True <+> colon <+> prettySe 10 bnd ty <> rbrace <+>
1249 st <> text "->" </> prettySe 10 ((n, True):bnd) sc
1250 | otherwise = prettySe 10 ((n, True):bnd) sc
1251 where
1252 st =
1253 case s of
1254 Static -> text "[static]" <> space
1255 _ -> empty
1256 prettySe p bnd (PPi (Constraint _ _) n ty sc) =
1257 bracket p 2 $
1258 prettySe 10 bnd ty <+> text "=>" </> prettySe 10 ((n, True):bnd) sc
1259 prettySe p bnd (PPi (TacImp _ _ s) n ty sc) =
1260 bracket p 2 $
1261 lbrace <> kwd "tacimp" <+> pretty n <+> colon <+> prettySe 10 bnd ty <>
1262 rbrace <+> text "->" </> prettySe 10 ((n, True):bnd) sc
1263 prettySe p bnd (PApp _ (PRef _ f) args) -- normal names, no explicit args
1264 | UN nm <- basename f
1265 , not (ppopt_impl ppo) && null (getShowArgs args) =
1266 prettyName True (ppopt_impl ppo) bnd f
1267 prettySe p bnd (PAppBind _ (PRef _ f) [])
1268 | not (ppopt_impl ppo) = text "!" <> prettyName True (ppopt_impl ppo) bnd f
1269 prettySe p bnd (PApp _ (PRef _ op) args) -- infix operators
1270 | UN nm <- basename op
1271 , not (tnull nm) &&
1272 (not (ppopt_impl ppo)) && (not $ isAlpha (thead nm)) =
1273 case getShowArgs args of
1274 [] -> opName True
1275 [x] -> group (opName True <$> group (prettySe 0 bnd (getTm x)))
1276 [l,r] -> let precedence = fromMaybe 20 (fmap prec f)
1277 in bracket p precedence $ inFix (getTm l) (getTm r)
1278 (l@(PExp _ _ _ _) : r@(PExp _ _ _ _) : rest) ->
1279 bracket p 1 $
1280 enclose lparen rparen (inFix (getTm l) (getTm r)) <+>
1281 align (group (vsep (map (prettyArgS bnd) rest)))
1282 as -> opName True <+> align (vsep (map (prettyArgS bnd) as))
1283 where opName isPrefix = prettyName isPrefix (ppopt_impl ppo) bnd op
1284 f = getFixity (opStr op)
1285 left l = case f of
1286 Nothing -> prettySe (-1) bnd l
1287 Just (Infixl p') -> prettySe p' bnd l
1288 Just f' -> prettySe (prec f'-1) bnd l
1289 right r = case f of
1290 Nothing -> prettySe (-1) bnd r
1291 Just (Infixr p') -> prettySe p' bnd r
1292 Just f' -> prettySe (prec f'-1) bnd r
1293 inFix l r = align . group $
1294 (left l <+> opName False) <$> group (right r)
1295 prettySe p bnd (PApp _ hd@(PRef fc f) [tm]) -- symbols, like 'foo
1296 | PConstant (Idris.Core.TT.Str str) <- getTm tm,
1297 f == sUN "Symbol_" = annotate (AnnType ("'" ++ str) ("The symbol " ++ str)) $
1298 char '\'' <> prettySe 10 bnd (PRef fc (sUN str))
1299 prettySe p bnd (PApp _ f as) = -- Normal prefix applications
1300 let args = getShowArgs as
1301 fp = prettySe 1 bnd f
1302 in
1303 bracket p 1 . group $
1304 if ppopt_impl ppo
1305 then if null as
1306 then fp
1307 else fp <+> align (vsep (map (prettyArgS bnd) as))
1308 else if null args
1309 then fp
1310 else fp <+> align (vsep (map (prettyArgS bnd) args))
1311 prettySe p bnd (PCase _ scr opts) =
1312 kwd "case" <+> prettySe 10 bnd scr <+> kwd "of" <> prettyBody
1313 where
1314 prettyBody = foldr (<>) empty $ intersperse (text "|") $ map sc opts
1316 sc (l, r) = nest nestingSize $ prettySe 10 bnd l <+> text "=>" <+> prettySe 10 bnd r
1317 prettySe p bnd (PHidden tm) = text "." <> prettySe 0 bnd tm
1318 prettySe p bnd (PRefl _ _) = annName eqCon $ text "Refl"
1319 prettySe p bnd (PResolveTC _) = text "resolvetc"
1320 prettySe p bnd (PTrue _ IsType) = annName unitTy $ text "()"
1321 prettySe p bnd (PTrue _ IsTerm) = annName unitCon $ text "()"
1322 prettySe p bnd (PTrue _ TypeOrTerm) = text "()"
1323 prettySe p bnd (PEq _ lt rt l r)
1324 | ppopt_impl ppo =
1325 bracket p 1 $
1326 enclose lparen rparen eq <+>
1327 align (group (vsep (map (prettyArgS bnd)
1328 [PImp 0 False [] (sUN "A") lt,
1329 PImp 0 False [] (sUN "B") rt,
1330 PExp 0 [] (sUN "x") l,
1331 PExp 0 [] (sUN "y") r])))
1332 | otherwise =
1333 bracket p 2 . align . group $
1334 prettySe 10 bnd l <+> eq <$> group (prettySe 10 bnd r)
1335 where eq = annName eqTy (text "=")
1336 prettySe p bnd (PRewrite _ l r _) =
1337 bracket p 2 $
1338 text "rewrite" <+> prettySe 10 bnd l <+> text "in" <+> prettySe 10 bnd r
1339 prettySe p bnd (PTyped l r) =
1340 lparen <> prettySe 10 bnd l <+> colon <+> prettySe 10 bnd r <> rparen
1341 prettySe p bnd pair@(PPair _ pun _ _) -- flatten tuples to the right, like parser
1342 | Just elts <- pairElts pair = enclose (ann lparen) (ann rparen) .
1343 align . group . vsep . punctuate (ann comma) $
1344 map (prettySe 10 bnd) elts
1345 where ann = case pun of
1346 TypeOrTerm -> id
1347 IsType -> annName pairTy
1348 IsTerm -> annName pairCon
1349 prettySe p bnd (PDPair _ TypeOrTerm l t r) =
1350 lparen <> prettySe 10 bnd l <+> text "**" <+> prettySe 10 bnd r <> rparen
1351 prettySe p bnd (PDPair _ IsType (PRef _ n) t r) =
1352 annName sigmaTy lparen <>
1353 bindingOf n False <+>
1354 annName sigmaTy (text "**") <+>
1355 prettySe 10 ((n, False):bnd) r <>
1356 annName sigmaTy rparen
1357 prettySe p bnd (PDPair _ IsType l t r) =
1358 annName sigmaTy lparen <>
1359 prettySe 10 bnd l <+>
1360 annName sigmaTy (text "**") <+>
1361 prettySe 10 bnd r <>
1362 annName sigmaTy rparen
1363 prettySe p bnd (PDPair _ IsTerm l t r) =
1364 annName existsCon lparen <>
1365 prettySe 10 bnd l <+>
1366 annName existsCon (text "**") <+>
1367 prettySe 10 bnd r <>
1368 annName existsCon rparen
1369 prettySe p bnd (PAlternative a as) =
1370 lparen <> text "|" <> prettyAs <> text "|" <> rparen
1371 where
1372 prettyAs =
1373 foldr (\l -> \r -> l <+> text "," <+> r) empty $ map (prettySe 10 bnd) as
1374 prettySe p bnd PType = annotate (AnnType "Type" "The type of types") $ text "Type"
1375 prettySe p bnd (PUniverse u) = annotate (AnnType (show u) "The type of unique types") $ text (show u)
1376 prettySe p bnd (PConstant c) = annotate (AnnConst c) (text (show c))
1377 -- XXX: add pretty for tactics
1378 prettySe p bnd (PProof ts) =
1379 text "proof" <+> lbrace <> nest nestingSize (text . show $ ts) <> rbrace
1380 prettySe p bnd (PTactics ts) =
1381 text "tactics" <+> lbrace <> nest nestingSize (text . show $ ts) <> rbrace
1382 prettySe p bnd (PMetavar n) = text "?" <> pretty n
1383 prettySe p bnd (PReturn f) = kwd "return"
1384 prettySe p bnd PImpossible = kwd "impossible"
1385 prettySe p bnd Placeholder = text "_"
1386 prettySe p bnd (PDoBlock _) = text "do block pretty not implemented"
1387 prettySe p bnd (PCoerced t) = prettySe p bnd t
1388 prettySe p bnd (PElabError s) = pretty s
1389 -- Quasiquote pprinting ignores bound vars
1390 prettySe p bnd (PQuasiquote t Nothing) = text "`(" <> prettySe p [] t <> text ")"
1391 prettySe p bnd (PQuasiquote t (Just g)) = text "`(" <> prettySe p [] t <+> colon <+> prettySe p [] g <> text ")"
1392 prettySe p bnd (PUnquote t) = text "~" <> prettySe p bnd t
1394 prettySe p bnd _ = text "missing pretty-printer for term"
1396 prettyArgS bnd (PImp _ _ _ n tm) = prettyArgSi bnd (n, tm)
1397 prettyArgS bnd (PExp _ _ _ tm) = prettyArgSe bnd tm
1398 prettyArgS bnd (PConstraint _ _ _ tm) = prettyArgSc bnd tm
1399 prettyArgS bnd (PTacImplicit _ _ n _ tm) = prettyArgSti bnd (n, tm)
1401 prettyArgSe bnd arg = prettySe 0 bnd arg
1402 prettyArgSi bnd (n, val) = lbrace <> pretty n <+> text "=" <+> prettySe 10 bnd val <> rbrace
1403 prettyArgSc bnd val = lbrace <> lbrace <> prettySe 10 bnd val <> rbrace <> rbrace
1404 prettyArgSti bnd (n, val) = lbrace <> kwd "auto" <+> pretty n <+> text "=" <+> prettySe 10 bnd val <> rbrace
1406 annName :: Name -> Doc OutputAnnotation -> Doc OutputAnnotation
1407 annName n = annotate (AnnName n Nothing Nothing Nothing)
1409 opStr :: Name -> String
1410 opStr (NS n _) = opStr n
1411 opStr (UN n) = T.unpack n
1413 basename :: Name -> Name
1414 basename (NS n _) = basename n
1415 basename n = n
1417 slist' p bnd (PApp _ (PRef _ nil) _)
1418 | not (ppopt_impl ppo) && nsroot nil == sUN "Nil" = Just []
1419 slist' p bnd (PRef _ nil)
1420 | not (ppopt_impl ppo) && nsroot nil == sUN "Nil" = Just []
1421 slist' p bnd (PApp _ (PRef _ cons) args)
1422 | nsroot cons == sUN "::",
1423 (PExp {getTm=tl}):(PExp {getTm=hd}):imps <- reverse args,
1424 all isImp imps,
1425 Just tl' <- slist' p bnd tl
1426 = Just (hd:tl')
1427 where
1428 isImp (PImp {}) = True
1429 isImp _ = False
1430 slist' _ _ tm = Nothing
1432 slist p bnd e | Just es <- slist' p bnd e = Just $
1433 case es of [] -> annotate (AnnData "" "") $ text "[]"
1434 [x] -> enclose left right . group $
1435 prettySe p bnd x
1436 xs -> (enclose left right .
1437 align . group . vsep .
1438 punctuate comma .
1439 map (prettySe p bnd)) xs
1440 where left = (annotate (AnnData "" "") (text "["))
1441 right = (annotate (AnnData "" "") (text "]"))
1442 comma = (annotate (AnnData "" "") (text ","))
1443 slist _ _ _ = Nothing
1445 pairElts :: PTerm -> Maybe [PTerm]
1446 pairElts (PPair _ _ x y) | Just elts <- pairElts y = Just (x:elts)
1447 | otherwise = Just [x, y]
1448 pairElts _ = Nothing
1450 natns = "Prelude.Nat."
1452 snat p (PRef _ z)
1453 | show z == (natns++"Z") || show z == "Z" = Just 0
1454 snat p (PApp _ s [PExp {getTm=n}])
1455 | show s == (natns++"S") || show s == "S",
1456 Just n' <- snat p n
1457 = Just $ 1 + n'
1458 snat _ _ = Nothing
1460 bracket outer inner doc
1461 | inner > outer = lparen <> doc <> rparen
1462 | otherwise = doc
1464 kwd = annotate AnnKeyword . text
1466 fixities :: M.Map String Fixity
1467 fixities = M.fromList [(s, f) | (Fix f s) <- infixes]
1469 getFixity :: String -> Maybe Fixity
1470 getFixity = flip M.lookup fixities
1472-- | Pretty-printer helper for the binding site of a name
1473bindingOf :: Name -- ^^ the bound name
1474 -> Bool -- ^^ whether the name is implicit
1475 -> Doc OutputAnnotation
1476bindingOf n imp = annotate (AnnBoundName n imp) (text (show n))
1478-- | Pretty-printer helper for names that attaches the correct annotations
1479prettyName
1480 :: Bool -- ^^ whether the name should be parenthesised if it is an infix operator
1481 -> Bool -- ^^ whether to show namespaces
1482 -> [(Name, Bool)] -- ^^ the current bound variables and whether they are implicit
1483 -> Name -- ^^ the name to pprint
1484 -> Doc OutputAnnotation
1485prettyName infixParen showNS bnd n
1486 | Just imp <- lookup n bnd = annotate (AnnBoundName n imp) fullName
1487 | otherwise = annotate (AnnName n Nothing Nothing Nothing) fullName
1488 where fullName = text nameSpace <> parenthesise (text (baseName n))
1489 baseName (UN n) = T.unpack n
1490 baseName (NS n ns) = baseName n
1491 baseName (MN i s) = T.unpack s
1492 baseName other = show other
1493 nameSpace = case n of
1494 (NS n' ns) -> if showNS then (concatMap (++ ".") . map T.unpack . reverse) ns else ""
1495 _ -> ""
1496 isInfix = case baseName n of
1497 "" -> False
1498 (c : _) -> not (isAlpha c)
1499 parenthesise = if isInfix && infixParen then enclose lparen rparen else id
1502showCImp :: PPOption -> PClause -> Doc OutputAnnotation
1503showCImp ppo (PClause _ n l ws r w)
1504 = prettyImp ppo l <+> showWs ws <+> text "=" <+> prettyImp ppo r
1505 <+> text "where" <+> text (show w)
1506 where
1507 showWs [] = empty
1508 showWs (x : xs) = text "|" <+> prettyImp ppo x <+> showWs xs
1509showCImp ppo (PWith _ n l ws r w)
1510 = prettyImp ppo l <+> showWs ws <+> text "with" <+> prettyImp ppo r
1511 <+> braces (text (show w))
1512 where
1513 showWs [] = empty
1514 showWs (x : xs) = text "|" <+> prettyImp ppo x <+> showWs xs
1517showDImp :: PPOption -> PData -> Doc OutputAnnotation
1518showDImp ppo (PDatadecl n ty cons)
1519 = text "data" <+> text (show n) <+> colon <+> prettyImp ppo ty <+> text "where" <$>
1520 (indent 2 $ vsep (map (\ (_, _, n, t, _, _) -> pipe <+> prettyName True False [] n <+> colon <+> prettyImp ppo t) cons))
1522showDecls :: PPOption -> [PDecl] -> Doc OutputAnnotation
1523showDecls o ds = vsep (map (showDeclImp o) ds)
1525showDeclImp _ (PFix _ f ops) = text (show f) <+> cat (punctuate (text ",") (map text ops))
1526showDeclImp o (PTy _ _ _ _ _ n t) = text "tydecl" <+> text (showCG n) <+> colon <+> prettyImp o t
1527showDeclImp o (PClauses _ _ n cs) = text "pat" <+> text (showCG n) <+> text "\t" <+>
1528 indent 2 (vsep (map (showCImp o) cs))
1529showDeclImp o (PData _ _ _ _ _ d) = showDImp o { ppopt_impl = True } d
1530showDeclImp o (PParams _ ns ps) = text "params" <+> braces (text (show ns) <> line <> showDecls o ps <> line)
1531showDeclImp o (PNamespace n ps) = text "namespace" <+> text n <> braces (line <> showDecls o ps <> line)
1532showDeclImp _ (PSyntax _ syn) = text "syntax" <+> text (show syn)
1533showDeclImp o (PClass _ _ _ cs n ps _ ds)
1534 = text "class" <+> text (show cs) <+> text (show n) <+> text (show ps) <> line <> showDecls o ds
1535showDeclImp o (PInstance _ _ cs n _ t _ ds)
1536 = text "instance" <+> text (show cs) <+> text (show n) <+> prettyImp o t <> line <> showDecls o ds
1537showDeclImp _ _ = text "..."
1538-- showDeclImp (PImport o) = "import " ++ o
1540instance Show (Doc OutputAnnotation) where
1541 show = flip (displayS . renderCompact) ""
1543getImps :: [PArg] -> [(Name, PTerm)]
1544getImps [] = []
1545getImps (PImp _ _ _ n tm : xs) = (n, tm) : getImps xs
1546getImps (_ : xs) = getImps xs
1548getExps :: [PArg] -> [PTerm]
1549getExps [] = []
1550getExps (PExp _ _ _ tm : xs) = tm : getExps xs
1551getExps (_ : xs) = getExps xs
1553getShowArgs :: [PArg] -> [PArg]
1554getShowArgs [] = []
1555getShowArgs (e@(PExp _ _ _ tm) : xs) = e : getShowArgs xs
1556getShowArgs (e : xs) | AlwaysShow `elem` argopts e = e : getShowArgs xs
1557getShowArgs (_ : xs) = getShowArgs xs
1559getConsts :: [PArg] -> [PTerm]
1560getConsts [] = []
1561getConsts (PConstraint _ _ _ tm : xs) = tm : getConsts xs
1562getConsts (_ : xs) = getConsts xs
1564getAll :: [PArg] -> [PTerm]
1565getAll = map getTm
1568-- | Show Idris name
1569showName :: Maybe IState -- ^^ the Idris state, for information about names and colours
1570 -> [(Name, Bool)] -- ^^ the bound variables and whether they're implicit
1571 -> PPOption -- ^^ pretty printing options
1572 -> Bool -- ^^ whether to colourise
1573 -> Name -- ^^ the term to show
1574 -> String
1575showName ist bnd ppo colour n = case ist of
1576 Just i -> if colour then colourise n (idris_colourTheme i) else showbasic n
1577 Nothing -> showbasic n
1578 where name = if ppopt_impl ppo then show n else showbasic n
1579 showbasic n@(UN _) = showCG n
1580 showbasic (MN i s) = str s
1581 showbasic (NS n s) = showSep "." (map str (reverse s)) ++ "." ++ showbasic n
1582 showbasic (SN s) = show s
1583 fst3 (x, _, _) = x
1584 colourise n t = let ctxt' = fmap tt_ctxt ist in
1585 case ctxt' of
1586 Nothing -> name
1587 Just ctxt | Just impl <- lookup n bnd -> if impl then colouriseImplicit t name
1588 else colouriseBound t name
1589 | isDConName n ctxt -> colouriseData t name
1590 | isFnName n ctxt -> colouriseFun t name
1591 | isTConName n ctxt -> colouriseType t name
1592 -- The assumption is that if a name is not bound and does not exist in the
1593 -- global context, then we're somewhere in which implicit info has been lost
1594 -- (like error messages). Thus, unknown vars are colourised as implicits.
1595 | otherwise -> colouriseImplicit t name
1597showTm :: IState -- ^^ the Idris state, for information about identifiers and colours
1598 -> PTerm -- ^^ the term to show
1599 -> String
1600showTm ist = displayDecorated (consoleDecorate ist) .
1601 renderPretty 0.8 100000 .
1602 prettyImp (ppOptionIst ist)
1604-- | Show a term with implicits, no colours
1605showTmImpls :: PTerm -> String
1606showTmImpls = flip (displayS . renderCompact . prettyImp verbosePPOption) ""
1610instance Sized PTerm where
1611 size (PQuote rawTerm) = size rawTerm
1612 size (PRef fc name) = size name
1613 size (PLam name ty bdy) = 1 + size ty + size bdy
1614 size (PPi plicity name ty bdy) = 1 + size ty + size bdy
1615 size (PLet name ty def bdy) = 1 + size ty + size def + size bdy
1616 size (PTyped trm ty) = 1 + size trm + size ty
1617 size (PApp fc name args) = 1 + size args
1618 size (PAppBind fc name args) = 1 + size args
1619 size (PCase fc trm bdy) = 1 + size trm + size bdy
1620 size (PTrue fc _) = 1
1621 size (PRefl fc _) = 1
1622 size (PResolveTC fc) = 1
1623 size (PEq fc _ _ left right) = 1 + size left + size right
1624 size (PRewrite fc left right _) = 1 + size left + size right
1625 size (PPair fc _ left right) = 1 + size left + size right
1626 size (PDPair fs _ left ty right) = 1 + size left + size ty + size right
1627 size (PAlternative a alts) = 1 + size alts
1628 size (PHidden hidden) = size hidden
1629 size (PUnifyLog tm) = size tm
1630 size (PDisamb _ tm) = size tm
1631 size (PNoImplicits tm) = size tm
1632 size PType = 1
1633 size (PUniverse _) = 1
1634 size (PConstant const) = 1 + size const
1635 size Placeholder = 1
1636 size (PDoBlock dos) = 1 + size dos
1637 size (PIdiom fc term) = 1 + size term
1638 size (PReturn fc) = 1
1639 size (PMetavar name) = 1
1640 size (PProof tactics) = size tactics
1641 size (PElabError err) = size err
1642 size PImpossible = 1
1643 size _ = 0
1645getPArity :: PTerm -> Int
1646getPArity (PPi _ _ _ sc) = 1 + getPArity sc
1647getPArity _ = 0
1649-- Return all names, free or globally bound, in the given term.
1651allNamesIn :: PTerm -> [Name]
1652allNamesIn tm = nub $ ni [] tm
1653 where -- TODO THINK added niTacImp, but is it right?
1654 ni env (PRef _ n)
1655 | not (n `elem` env) = [n]
1656 ni env (PPatvar _ n) = [n]
1657 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
1658 ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
1659 ni env (PCase _ c os) = ni env c ++ concatMap (ni env) (map snd os)
1660 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc
1661 ni env (PPi p n ty sc) = niTacImp env p ++ ni env ty ++ ni (n:env) sc
1662 ni env (PHidden tm) = ni env tm
1663 ni env (PEq _ _ _ l r) = ni env l ++ ni env r
1664 ni env (PRewrite _ l r _) = ni env l ++ ni env r
1665 ni env (PTyped l r) = ni env l ++ ni env r
1666 ni env (PPair _ _ l r) = ni env l ++ ni env r
1667 ni env (PDPair _ _ (PRef _ n) t r) = ni env t ++ ni (n:env) r
1668 ni env (PDPair _ _ l t r) = ni env l ++ ni env t ++ ni env r
1669 ni env (PAlternative a ls) = concatMap (ni env) ls
1670 ni env (PUnifyLog tm) = ni env tm
1671 ni env (PDisamb _ tm) = ni env tm
1672 ni env (PNoImplicits tm) = ni env tm
1673 ni env _ = []
1675 niTacImp env (TacImp _ _ scr) = ni env scr
1676 niTacImp _ _ = []
1678-- Return all names defined in binders in the given term
1679boundNamesIn :: PTerm -> [Name]
1680boundNamesIn tm = nub $ ni tm
1681 where -- TODO THINK Added niTacImp, but is it right?
1682 ni (PApp _ f as) = ni f ++ concatMap (ni) (map getTm as)
1683 ni (PAppBind _ f as) = ni f ++ concatMap (ni) (map getTm as)
1684 ni (PCase _ c os) = ni c ++ concatMap (ni) (map snd os)
1685 ni (PLam n ty sc) = n : (ni ty ++ ni sc)
1686 ni (PLet n ty val sc) = n : (ni ty ++ ni val ++ ni sc)
1687 ni (PPi p n ty sc) = niTacImp p ++ (n : (ni ty ++ ni sc))
1688 ni (PEq _ _ _ l r) = ni l ++ ni r
1689 ni (PRewrite _ l r _) = ni l ++ ni r
1690 ni (PTyped l r) = ni l ++ ni r
1691 ni (PPair _ _ l r) = ni l ++ ni r
1692 ni (PDPair _ _ (PRef _ n) t r) = ni t ++ ni r
1693 ni (PDPair _ _ l t r) = ni l ++ ni t ++ ni r
1694 ni (PAlternative a as) = concatMap (ni) as
1695 ni (PHidden tm) = ni tm
1696 ni (PUnifyLog tm) = ni tm
1697 ni (PDisamb _ tm) = ni tm
1698 ni (PNoImplicits tm) = ni tm
1699 ni _ = []
1701 niTacImp (TacImp _ _ scr) = ni scr
1702 niTacImp _ = []
1704-- Return names which are valid implicits in the given term (type).
1705implicitNamesIn :: [Name] -> IState -> PTerm -> [Name]
1706implicitNamesIn uvars ist tm = nub $ ni [] tm
1707 where
1708 ni env (PRef _ n)
1709 | not (n `elem` env)
1710 = case lookupTy n (tt_ctxt ist) of
1711 [] -> [n]
1712 _ -> if n `elem` uvars then [n] else []
1713 ni env (PApp _ f@(PRef _ n) as)
1714 | n `elem` uvars = ni env f ++ concatMap (ni env) (map getTm as)
1715 | otherwise = concatMap (ni env) (map getTm as)
1716 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
1717 ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
1718 ni env (PCase _ c os) = ni env c ++
1719 -- names in 'os', not counting the names bound in the cases
1720 (nub (concatMap (ni env) (map snd os))
1721 \\ nub (concatMap (ni env) (map fst os)))
1722 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc
1723 ni env (PPi p n ty sc) = ni env ty ++ ni (n:env) sc
1724 ni env (PEq _ _ _ l r) = ni env l ++ ni env r
1725 ni env (PRewrite _ l r _) = ni env l ++ ni env r
1726 ni env (PTyped l r) = ni env l ++ ni env r
1727 ni env (PPair _ _ l r) = ni env l ++ ni env r
1728 ni env (PDPair _ _ (PRef _ n) t r) = ni env t ++ ni (n:env) r
1729 ni env (PDPair _ _ l t r) = ni env l ++ ni env t ++ ni env r
1730 ni env (PAlternative a as) = concatMap (ni env) as
1731 ni env (PHidden tm) = ni env tm
1732 ni env (PUnifyLog tm) = ni env tm
1733 ni env (PDisamb _ tm) = ni env tm
1734 ni env (PNoImplicits tm) = ni env tm
1735 ni env _ = []
1737-- Return names which are free in the given term.
1738namesIn :: [(Name, PTerm)] -> IState -> PTerm -> [Name]
1739namesIn uvars ist tm = nub $ ni [] tm
1740 where
1741 ni env (PRef _ n)
1742 | not (n `elem` env)
1743 = case lookupTy n (tt_ctxt ist) of
1744 [] -> [n]
1745 _ -> if n `elem` (map fst uvars) then [n] else []
1746 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
1747 ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
1748 ni env (PCase _ c os) = ni env c ++
1749 -- names in 'os', not counting the names bound in the cases
1750 (nub (concatMap (ni env) (map snd os))
1751 \\ nub (concatMap (ni env) (map fst os)))
1752 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc
1753 ni env (PPi p n ty sc) = niTacImp env p ++ ni env ty ++ ni (n:env) sc
1754 ni env (PEq _ _ _ l r) = ni env l ++ ni env r
1755 ni env (PRewrite _ l r _) = ni env l ++ ni env r
1756 ni env (PTyped l r) = ni env l ++ ni env r
1757 ni env (PPair _ _ l r) = ni env l ++ ni env r
1758 ni env (PDPair _ _ (PRef _ n) t r) = ni env t ++ ni (n:env) r
1759 ni env (PDPair _ _ l t r) = ni env l ++ ni env t ++ ni env r
1760 ni env (PAlternative a as) = concatMap (ni env) as
1761 ni env (PHidden tm) = ni env tm
1762 ni env (PUnifyLog tm) = ni env tm
1763 ni env (PDisamb _ tm) = ni env tm
1764 ni env (PNoImplicits tm) = ni env tm
1765 ni env _ = []
1767 niTacImp env (TacImp _ _ scr) = ni env scr
1768 niTacImp _ _ = []
1770-- Return which of the given names are used in the given term.
1772usedNamesIn :: [Name] -> IState -> PTerm -> [Name]
1773usedNamesIn vars ist tm = nub $ ni [] tm
1774 where -- TODO THINK added niTacImp, but is it right?
1775 ni env (PRef _ n)
1776 | n `elem` vars && not (n `elem` env)
1777 = case lookupDefExact n (tt_ctxt ist) of
1778 Nothing -> [n]
1779 _ -> []
1780 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
1781 ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
1782 ni env (PCase _ c os) = ni env c ++ concatMap (ni env) (map snd os)
1783 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc
1784 ni env (PPi p n ty sc) = niTacImp env p ++ ni env ty ++ ni (n:env) sc
1785 ni env (PEq _ _ _ l r) = ni env l ++ ni env r
1786 ni env (PRewrite _ l r _) = ni env l ++ ni env r
1787 ni env (PTyped l r) = ni env l ++ ni env r
1788 ni env (PPair _ _ l r) = ni env l ++ ni env r
1789 ni env (PDPair _ _ (PRef _ n) t r) = ni env t ++ ni (n:env) r
1790 ni env (PDPair _ _ l t r) = ni env l ++ ni env t ++ ni env r
1791 ni env (PAlternative a as) = concatMap (ni env) as
1792 ni env (PHidden tm) = ni env tm
1793 ni env (PUnifyLog tm) = ni env tm
1794 ni env (PDisamb _ tm) = ni env tm
1795 ni env (PNoImplicits tm) = ni env tm
1796 ni env _ = []
1798 niTacImp env (TacImp _ _ scr) = ni env scr
1799 niTacImp _ _ = []
1801-- Return the list of inaccessible (= dotted) positions for a name.
1802getErasureInfo :: IState -> Name -> [Int]
1803getErasureInfo ist n =
1804 case lookupCtxtExact n (idris_optimisation ist) of
1805 Just (Optimise inacc detagg) -> map fst inacc
1806 Nothing -> []