git.iko.soy/Idris-dev
on e6bbd1f help sign in
Idris-dev/src/Idris/AbsSyntaxTree.hs
1808 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"
1081-- TODO: elaborate the code samples in the docstring
1082falseDoc = fmap (const $ Msg "") . parseDocstring . T.pack $
1083 "The empty type, also known as the trivially false proposition." ++
1084 "\n\n" ++
1085 "Use `void` or `absurd` to prove anything if you have a variable " ++
1086 "of type `Void` in scope."
1087falseTy = sUN "Void"
1089pairTy = sUN "Pair"
1090pairCon = sUN "MkPair"
1092eqTy = sUN "="
1093eqCon = sUN "Refl"
1094eqDoc = fmap (const (Left $ Msg "")) . parseDocstring . T.pack $
1095 "The propositional equality type. A proof that `x` = `y`." ++
1096 "\n\n" ++
1097 "To use such a proof, pattern-match on it, and the two equal things will " ++
1098 "then need to be the _same_ pattern." ++
1099 "\n\n" ++
1100 "**Note**: Idris's equality type is potentially _heterogeneous_, which means that it " ++
1101 "is possible to state equalities between values of potentially different " ++
1102 "types. However, Idris will attempt the homogeneous case unless it fails to typecheck." ++
1103 "\n\n" ++
1104 "You may need to use `(~=~)` to explicitly request heterogeneous equality."
1106eqDecl = PDatadecl eqTy (piBindp impl [(n "A", PType), (n "B", PType)]
1107 (piBind [(n "x", PRef bi (n "A")), (n "y", PRef bi (n "B"))]
1108 PType))
1109 [(reflDoc, reflParamDoc,
1110 eqCon, PPi impl (n "A") PType (
1111 PPi impl (n "x") (PRef bi (n "A"))
1112 (PApp bi (PRef bi eqTy) [pimp (n "A") Placeholder False,
1113 pimp (n "B") Placeholder False,
1114 pexp (PRef bi (n "x")),
1115 pexp (PRef bi (n "x"))])), bi, [])]
1116 where n a = sUN a
1117 reflDoc = annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $
1118 "A proof that `x` in fact equals `x`. To construct this, you must have already " ++
1119 "shown that both sides are in fact equal."
1120 reflParamDoc = [(n "A", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the type at which the equality is proven"),
1121 (n "x", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the element shown to be equal to itself.")]
1123eqParamDoc = [(n "A", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the type of the left side of the equality"),
1124 (n "B", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the type of the right side of the equality")
1126 where n a = sUN a
1128eqOpts = []
1130-- Defined in builtins.idr
1131sigmaTy = sUN "Sigma"
1132existsCon = sUN "MkSigma"
1134piBind :: [(Name, PTerm)] -> PTerm -> PTerm
1135piBind = piBindp expl
1137piBindp :: Plicity -> [(Name, PTerm)] -> PTerm -> PTerm
1138piBindp p [] t = t
1139piBindp p ((n, ty):ns) t = PPi p n ty (piBindp p ns t)
1142-- Pretty-printing declarations and terms
1144-- These "show" instances render to an absurdly wide screen because inserted line breaks
1145-- could interfere with interactive editing, which calls "show".
1147instance Show PTerm where
1148 showsPrec _ tm = (displayS . renderPretty 1.0 10000000 . prettyImp defaultPPOption) tm
1150instance Show PDecl where
1151 showsPrec _ d = (displayS . renderPretty 1.0 10000000 . showDeclImp verbosePPOption) d
1153instance Show PClause where
1154 showsPrec _ c = (displayS . renderPretty 1.0 10000000 . showCImp verbosePPOption) c
1156instance Show PData where
1157 showsPrec _ d = (displayS . renderPretty 1.0 10000000 . showDImp defaultPPOption) d
1159instance Pretty PTerm OutputAnnotation where
1160 pretty = prettyImp defaultPPOption
1162-- | Colourise annotations according to an Idris state. It ignores the names
1163-- in the annotation, as there's no good way to show extended information on a
1164-- terminal.
1165consoleDecorate :: IState -> OutputAnnotation -> String -> String
1166consoleDecorate ist _ | not (idris_colourRepl ist) = id
1167consoleDecorate ist (AnnConst c) = let theme = idris_colourTheme ist
1168 in if constIsType c
1169 then colouriseType theme
1170 else colouriseData theme
1171consoleDecorate ist (AnnData _ _) = colouriseData (idris_colourTheme ist)
1172consoleDecorate ist (AnnType _ _) = colouriseType (idris_colourTheme ist)
1173consoleDecorate ist (AnnBoundName _ True) = colouriseImplicit (idris_colourTheme ist)
1174consoleDecorate ist (AnnBoundName _ False) = colouriseBound (idris_colourTheme ist)
1175consoleDecorate ist AnnKeyword = colouriseKeyword (idris_colourTheme ist)
1176consoleDecorate ist (AnnName n _ _ _) = let ctxt = tt_ctxt ist
1177 theme = idris_colourTheme ist
1178 in case () of
1179 _ | isDConName n ctxt -> colouriseData theme
1180 _ | isFnName n ctxt -> colouriseFun theme
1181 _ | isTConName n ctxt -> colouriseType theme
1182 _ | isPostulateName n ist -> colourisePostulate theme
1183 _ | otherwise -> id -- don't colourise unknown names
1184consoleDecorate ist (AnnFC _) = id
1185consoleDecorate ist (AnnTextFmt fmt) = Idris.Colours.colourise (colour fmt)
1186 where colour BoldText = IdrisColour Nothing True False True False
1187 colour UnderlineText = IdrisColour Nothing True True False False
1188 colour ItalicText = IdrisColour Nothing True False False True
1189consoleDecorate ist (AnnTerm _ _) = id
1190consoleDecorate ist (AnnSearchResult _) = id
1191consoleDecorate ist (AnnErr _) = id
1193isPostulateName :: Name -> IState -> Bool
1194isPostulateName n ist = S.member n (idris_postulates ist)
1196-- | Pretty-print a high-level closed Idris term with no information about precedence/associativity
1197prettyImp :: PPOption -- ^^ pretty printing options
1198 -> PTerm -- ^^ the term to pretty-print
1199 -> Doc OutputAnnotation
1200prettyImp impl = pprintPTerm impl [] [] []
1202-- | Serialise something to base64 using its Binary instance.
1204-- | Do the right thing for rendering a term in an IState
1205prettyIst :: IState -> PTerm -> Doc OutputAnnotation
1206prettyIst ist = pprintPTerm (ppOptionIst ist) [] [] (idris_infixes ist)
1208-- | Pretty-print a high-level Idris term in some bindings context with infix info
1209pprintPTerm :: PPOption -- ^^ pretty printing options
1210 -> [(Name, Bool)] -- ^^ the currently-bound names and whether they are implicit
1211 -> [Name] -- ^^ names to always show in pi, even if not used
1212 -> [FixDecl] -- ^^ Fixity declarations
1213 -> PTerm -- ^^ the term to pretty-print
1214 -> Doc OutputAnnotation
1215pprintPTerm ppo bnd docArgs infixes = prettySe 10 bnd
1216 where
1217 prettySe :: Int -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation
1218 prettySe p bnd (PQuote r) =
1219 text "![" <> pretty r <> text "]"
1220 prettySe p bnd (PPatvar fc n) = pretty n
1221 prettySe p bnd e
1222 | Just str <- slist p bnd e = str
1223 | Just n <- snat p e = annotate (AnnData "Nat" "") (text (show n))
1224 prettySe p bnd (PRef fc n) = prettyName True (ppopt_impl ppo) bnd n
1225 prettySe p bnd (PLam n ty sc) =
1226 bracket p 2 . group . align . hang 2 $
1227 text "\\" <> bindingOf n False <+> text "=>" <$>
1228 prettySe 10 ((n, False):bnd) sc
1229 prettySe p bnd (PLet n ty v sc) =
1230 bracket p 2 . group . align $
1231 kwd "let" <+> (group . align . hang 2 $ bindingOf n False <+> text "=" <$> prettySe 10 bnd v) </>
1232 kwd "in" <+> (group . align . hang 2 $ prettySe 10 ((n, False):bnd) sc)
1233 prettySe p bnd (PPi (Exp l s _) n ty sc)
1234 | n `elem` allNamesIn sc || ppopt_impl ppo || n `elem` docArgs =
1235 bracket p 2 . group $
1236 enclose lparen rparen (group . align $ bindingOf n False <+> colon <+> prettySe 10 bnd ty) <+>
1237 st <> text "->" <$> prettySe 10 ((n, False):bnd) sc
1238 | otherwise =
1239 bracket p 2 . group $
1240 group (prettySe 1 bnd ty <+> st) <> text "->" <$> group (prettySe 10 ((n, False):bnd) sc)
1241 where
1242 st =
1243 case s of
1244 Static -> text "[static]" <> space
1245 _ -> empty
1246 prettySe p bnd (PPi (Imp l s _) n ty sc)
1247 | ppopt_impl ppo =
1248 bracket p 2 $
1249 lbrace <> bindingOf n True <+> colon <+> prettySe 10 bnd ty <> rbrace <+>
1250 st <> text "->" </> prettySe 10 ((n, True):bnd) sc
1251 | otherwise = prettySe 10 ((n, True):bnd) sc
1252 where
1253 st =
1254 case s of
1255 Static -> text "[static]" <> space
1256 _ -> empty
1257 prettySe p bnd (PPi (Constraint _ _) n ty sc) =
1258 bracket p 2 $
1259 prettySe 10 bnd ty <+> text "=>" </> prettySe 10 ((n, True):bnd) sc
1260 prettySe p bnd (PPi (TacImp _ _ s) n ty sc) =
1261 bracket p 2 $
1262 lbrace <> kwd "tacimp" <+> pretty n <+> colon <+> prettySe 10 bnd ty <>
1263 rbrace <+> text "->" </> prettySe 10 ((n, True):bnd) sc
1264 prettySe p bnd (PApp _ (PRef _ f) args) -- normal names, no explicit args
1265 | UN nm <- basename f
1266 , not (ppopt_impl ppo) && null (getShowArgs args) =
1267 prettyName True (ppopt_impl ppo) bnd f
1268 prettySe p bnd (PAppBind _ (PRef _ f) [])
1269 | not (ppopt_impl ppo) = text "!" <> prettyName True (ppopt_impl ppo) bnd f
1270 prettySe p bnd (PApp _ (PRef _ op) args) -- infix operators
1271 | UN nm <- basename op
1272 , not (tnull nm) &&
1273 (not (ppopt_impl ppo)) && (not $ isAlpha (thead nm)) =
1274 case getShowArgs args of
1275 [] -> opName True
1276 [x] -> group (opName True <$> group (prettySe 0 bnd (getTm x)))
1277 [l,r] -> let precedence = fromMaybe 20 (fmap prec f)
1278 in bracket p precedence $ inFix (getTm l) (getTm r)
1279 (l@(PExp _ _ _ _) : r@(PExp _ _ _ _) : rest) ->
1280 bracket p 1 $
1281 enclose lparen rparen (inFix (getTm l) (getTm r)) <+>
1282 align (group (vsep (map (prettyArgS bnd) rest)))
1283 as -> opName True <+> align (vsep (map (prettyArgS bnd) as))
1284 where opName isPrefix = prettyName isPrefix (ppopt_impl ppo) bnd op
1285 f = getFixity (opStr op)
1286 left l = case f of
1287 Nothing -> prettySe (-1) bnd l
1288 Just (Infixl p') -> prettySe p' bnd l
1289 Just f' -> prettySe (prec f'-1) bnd l
1290 right r = case f of
1291 Nothing -> prettySe (-1) bnd r
1292 Just (Infixr p') -> prettySe p' bnd r
1293 Just f' -> prettySe (prec f'-1) bnd r
1294 inFix l r = align . group $
1295 (left l <+> opName False) <$> group (right r)
1296 prettySe p bnd (PApp _ hd@(PRef fc f) [tm]) -- symbols, like 'foo
1297 | PConstant (Idris.Core.TT.Str str) <- getTm tm,
1298 f == sUN "Symbol_" = annotate (AnnType ("'" ++ str) ("The symbol " ++ str)) $
1299 char '\'' <> prettySe 10 bnd (PRef fc (sUN str))
1300 prettySe p bnd (PApp _ f as) = -- Normal prefix applications
1301 let args = getShowArgs as
1302 fp = prettySe 1 bnd f
1303 in
1304 bracket p 1 . group $
1305 if ppopt_impl ppo
1306 then if null as
1307 then fp
1308 else fp <+> align (vsep (map (prettyArgS bnd) as))
1309 else if null args
1310 then fp
1311 else fp <+> align (vsep (map (prettyArgS bnd) args))
1312 prettySe p bnd (PCase _ scr opts) =
1313 kwd "case" <+> prettySe 10 bnd scr <+> kwd "of" <> prettyBody
1314 where
1315 prettyBody = foldr (<>) empty $ intersperse (text "|") $ map sc opts
1317 sc (l, r) = nest nestingSize $ prettySe 10 bnd l <+> text "=>" <+> prettySe 10 bnd r
1318 prettySe p bnd (PHidden tm) = text "." <> prettySe 0 bnd tm
1319 prettySe p bnd (PRefl _ _) = annName eqCon $ text "Refl"
1320 prettySe p bnd (PResolveTC _) = text "resolvetc"
1321 prettySe p bnd (PTrue _ IsType) = annName unitTy $ text "()"
1322 prettySe p bnd (PTrue _ IsTerm) = annName unitCon $ text "()"
1323 prettySe p bnd (PTrue _ TypeOrTerm) = text "()"
1324 prettySe p bnd (PEq _ lt rt l r)
1325 | ppopt_impl ppo =
1326 bracket p 1 $
1327 enclose lparen rparen eq <+>
1328 align (group (vsep (map (prettyArgS bnd)
1329 [PImp 0 False [] (sUN "A") lt,
1330 PImp 0 False [] (sUN "B") rt,
1331 PExp 0 [] (sUN "x") l,
1332 PExp 0 [] (sUN "y") r])))
1333 | otherwise =
1334 bracket p 2 . align . group $
1335 prettySe 10 bnd l <+> eq <$> group (prettySe 10 bnd r)
1336 where eq = annName eqTy (text "=")
1337 prettySe p bnd (PRewrite _ l r _) =
1338 bracket p 2 $
1339 text "rewrite" <+> prettySe 10 bnd l <+> text "in" <+> prettySe 10 bnd r
1340 prettySe p bnd (PTyped l r) =
1341 lparen <> prettySe 10 bnd l <+> colon <+> prettySe 10 bnd r <> rparen
1342 prettySe p bnd pair@(PPair _ pun _ _) -- flatten tuples to the right, like parser
1343 | Just elts <- pairElts pair = enclose (ann lparen) (ann rparen) .
1344 align . group . vsep . punctuate (ann comma) $
1345 map (prettySe 10 bnd) elts
1346 where ann = case pun of
1347 TypeOrTerm -> id
1348 IsType -> annName pairTy
1349 IsTerm -> annName pairCon
1350 prettySe p bnd (PDPair _ TypeOrTerm l t r) =
1351 lparen <> prettySe 10 bnd l <+> text "**" <+> prettySe 10 bnd r <> rparen
1352 prettySe p bnd (PDPair _ IsType (PRef _ n) t r) =
1353 annName sigmaTy lparen <>
1354 bindingOf n False <+>
1355 annName sigmaTy (text "**") <+>
1356 prettySe 10 ((n, False):bnd) r <>
1357 annName sigmaTy rparen
1358 prettySe p bnd (PDPair _ IsType l t r) =
1359 annName sigmaTy lparen <>
1360 prettySe 10 bnd l <+>
1361 annName sigmaTy (text "**") <+>
1362 prettySe 10 bnd r <>
1363 annName sigmaTy rparen
1364 prettySe p bnd (PDPair _ IsTerm l t r) =
1365 annName existsCon lparen <>
1366 prettySe 10 bnd l <+>
1367 annName existsCon (text "**") <+>
1368 prettySe 10 bnd r <>
1369 annName existsCon rparen
1370 prettySe p bnd (PAlternative a as) =
1371 lparen <> text "|" <> prettyAs <> text "|" <> rparen
1372 where
1373 prettyAs =
1374 foldr (\l -> \r -> l <+> text "," <+> r) empty $ map (prettySe 10 bnd) as
1375 prettySe p bnd PType = annotate (AnnType "Type" "The type of types") $ text "Type"
1376 prettySe p bnd (PUniverse u) = annotate (AnnType (show u) "The type of unique types") $ text (show u)
1377 prettySe p bnd (PConstant c) = annotate (AnnConst c) (text (show c))
1378 -- XXX: add pretty for tactics
1379 prettySe p bnd (PProof ts) =
1380 text "proof" <+> lbrace <> nest nestingSize (text . show $ ts) <> rbrace
1381 prettySe p bnd (PTactics ts) =
1382 text "tactics" <+> lbrace <> nest nestingSize (text . show $ ts) <> rbrace
1383 prettySe p bnd (PMetavar n) = text "?" <> pretty n
1384 prettySe p bnd (PReturn f) = kwd "return"
1385 prettySe p bnd PImpossible = kwd "impossible"
1386 prettySe p bnd Placeholder = text "_"
1387 prettySe p bnd (PDoBlock _) = text "do block pretty not implemented"
1388 prettySe p bnd (PCoerced t) = prettySe p bnd t
1389 prettySe p bnd (PElabError s) = pretty s
1390 -- Quasiquote pprinting ignores bound vars
1391 prettySe p bnd (PQuasiquote t Nothing) = text "`(" <> prettySe p [] t <> text ")"
1392 prettySe p bnd (PQuasiquote t (Just g)) = text "`(" <> prettySe p [] t <+> colon <+> prettySe p [] g <> text ")"
1393 prettySe p bnd (PUnquote t) = text "~" <> prettySe p bnd t
1395 prettySe p bnd _ = text "missing pretty-printer for term"
1397 prettyArgS bnd (PImp _ _ _ n tm) = prettyArgSi bnd (n, tm)
1398 prettyArgS bnd (PExp _ _ _ tm) = prettyArgSe bnd tm
1399 prettyArgS bnd (PConstraint _ _ _ tm) = prettyArgSc bnd tm
1400 prettyArgS bnd (PTacImplicit _ _ n _ tm) = prettyArgSti bnd (n, tm)
1402 prettyArgSe bnd arg = prettySe 0 bnd arg
1403 prettyArgSi bnd (n, val) = lbrace <> pretty n <+> text "=" <+> prettySe 10 bnd val <> rbrace
1404 prettyArgSc bnd val = lbrace <> lbrace <> prettySe 10 bnd val <> rbrace <> rbrace
1405 prettyArgSti bnd (n, val) = lbrace <> kwd "auto" <+> pretty n <+> text "=" <+> prettySe 10 bnd val <> rbrace
1407 annName :: Name -> Doc OutputAnnotation -> Doc OutputAnnotation
1408 annName n = annotate (AnnName n Nothing Nothing Nothing)
1410 opStr :: Name -> String
1411 opStr (NS n _) = opStr n
1412 opStr (UN n) = T.unpack n
1414 basename :: Name -> Name
1415 basename (NS n _) = basename n
1416 basename n = n
1418 slist' p bnd (PApp _ (PRef _ nil) _)
1419 | not (ppopt_impl ppo) && nsroot nil == sUN "Nil" = Just []
1420 slist' p bnd (PRef _ nil)
1421 | not (ppopt_impl ppo) && nsroot nil == sUN "Nil" = Just []
1422 slist' p bnd (PApp _ (PRef _ cons) args)
1423 | nsroot cons == sUN "::",
1424 (PExp {getTm=tl}):(PExp {getTm=hd}):imps <- reverse args,
1425 all isImp imps,
1426 Just tl' <- slist' p bnd tl
1427 = Just (hd:tl')
1428 where
1429 isImp (PImp {}) = True
1430 isImp _ = False
1431 slist' _ _ tm = Nothing
1433 slist p bnd e | Just es <- slist' p bnd e = Just $
1434 case es of [] -> annotate (AnnData "" "") $ text "[]"
1435 [x] -> enclose left right . group $
1436 prettySe p bnd x
1437 xs -> (enclose left right .
1438 align . group . vsep .
1439 punctuate comma .
1440 map (prettySe p bnd)) xs
1441 where left = (annotate (AnnData "" "") (text "["))
1442 right = (annotate (AnnData "" "") (text "]"))
1443 comma = (annotate (AnnData "" "") (text ","))
1444 slist _ _ _ = Nothing
1446 pairElts :: PTerm -> Maybe [PTerm]
1447 pairElts (PPair _ _ x y) | Just elts <- pairElts y = Just (x:elts)
1448 | otherwise = Just [x, y]
1449 pairElts _ = Nothing
1451 natns = "Prelude.Nat."
1453 snat p (PRef _ z)
1454 | show z == (natns++"Z") || show z == "Z" = Just 0
1455 snat p (PApp _ s [PExp {getTm=n}])
1456 | show s == (natns++"S") || show s == "S",
1457 Just n' <- snat p n
1458 = Just $ 1 + n'
1459 snat _ _ = Nothing
1461 bracket outer inner doc
1462 | inner > outer = lparen <> doc <> rparen
1463 | otherwise = doc
1465 kwd = annotate AnnKeyword . text
1467 fixities :: M.Map String Fixity
1468 fixities = M.fromList [(s, f) | (Fix f s) <- infixes]
1470 getFixity :: String -> Maybe Fixity
1471 getFixity = flip M.lookup fixities
1473-- | Pretty-printer helper for the binding site of a name
1474bindingOf :: Name -- ^^ the bound name
1475 -> Bool -- ^^ whether the name is implicit
1476 -> Doc OutputAnnotation
1477bindingOf n imp = annotate (AnnBoundName n imp) (text (show n))
1479-- | Pretty-printer helper for names that attaches the correct annotations
1480prettyName
1481 :: Bool -- ^^ whether the name should be parenthesised if it is an infix operator
1482 -> Bool -- ^^ whether to show namespaces
1483 -> [(Name, Bool)] -- ^^ the current bound variables and whether they are implicit
1484 -> Name -- ^^ the name to pprint
1485 -> Doc OutputAnnotation
1486prettyName infixParen showNS bnd n
1487 | Just imp <- lookup n bnd = annotate (AnnBoundName n imp) fullName
1488 | otherwise = annotate (AnnName n Nothing Nothing Nothing) fullName
1489 where fullName = text nameSpace <> parenthesise (text (baseName n))
1490 baseName (UN n) = T.unpack n
1491 baseName (NS n ns) = baseName n
1492 baseName (MN i s) = T.unpack s
1493 baseName other = show other
1494 nameSpace = case n of
1495 (NS n' ns) -> if showNS then (concatMap (++ ".") . map T.unpack . reverse) ns else ""
1496 _ -> ""
1497 isInfix = case baseName n of
1498 "" -> False
1499 (c : _) -> not (isAlpha c)
1500 parenthesise = if isInfix && infixParen then enclose lparen rparen else id
1503showCImp :: PPOption -> PClause -> Doc OutputAnnotation
1504showCImp ppo (PClause _ n l ws r w)
1505 = prettyImp ppo l <+> showWs ws <+> text "=" <+> prettyImp ppo r
1506 <+> text "where" <+> text (show w)
1507 where
1508 showWs [] = empty
1509 showWs (x : xs) = text "|" <+> prettyImp ppo x <+> showWs xs
1510showCImp ppo (PWith _ n l ws r w)
1511 = prettyImp ppo l <+> showWs ws <+> text "with" <+> prettyImp ppo r
1512 <+> braces (text (show w))
1513 where
1514 showWs [] = empty
1515 showWs (x : xs) = text "|" <+> prettyImp ppo x <+> showWs xs
1518showDImp :: PPOption -> PData -> Doc OutputAnnotation
1519showDImp ppo (PDatadecl n ty cons)
1520 = text "data" <+> text (show n) <+> colon <+> prettyImp ppo ty <+> text "where" <$>
1521 (indent 2 $ vsep (map (\ (_, _, n, t, _, _) -> pipe <+> prettyName True False [] n <+> colon <+> prettyImp ppo t) cons))
1523showDecls :: PPOption -> [PDecl] -> Doc OutputAnnotation
1524showDecls o ds = vsep (map (showDeclImp o) ds)
1526showDeclImp _ (PFix _ f ops) = text (show f) <+> cat (punctuate (text ",") (map text ops))
1527showDeclImp o (PTy _ _ _ _ _ n t) = text "tydecl" <+> text (showCG n) <+> colon <+> prettyImp o t
1528showDeclImp o (PClauses _ _ n cs) = text "pat" <+> text (showCG n) <+> text "\t" <+>
1529 indent 2 (vsep (map (showCImp o) cs))
1530showDeclImp o (PData _ _ _ _ _ d) = showDImp o { ppopt_impl = True } d
1531showDeclImp o (PParams _ ns ps) = text "params" <+> braces (text (show ns) <> line <> showDecls o ps <> line)
1532showDeclImp o (PNamespace n ps) = text "namespace" <+> text n <> braces (line <> showDecls o ps <> line)
1533showDeclImp _ (PSyntax _ syn) = text "syntax" <+> text (show syn)
1534showDeclImp o (PClass _ _ _ cs n ps _ ds)
1535 = text "class" <+> text (show cs) <+> text (show n) <+> text (show ps) <> line <> showDecls o ds
1536showDeclImp o (PInstance _ _ cs n _ t _ ds)
1537 = text "instance" <+> text (show cs) <+> text (show n) <+> prettyImp o t <> line <> showDecls o ds
1538showDeclImp _ _ = text "..."
1539-- showDeclImp (PImport o) = "import " ++ o
1541instance Show (Doc OutputAnnotation) where
1542 show = flip (displayS . renderCompact) ""
1544getImps :: [PArg] -> [(Name, PTerm)]
1545getImps [] = []
1546getImps (PImp _ _ _ n tm : xs) = (n, tm) : getImps xs
1547getImps (_ : xs) = getImps xs
1549getExps :: [PArg] -> [PTerm]
1550getExps [] = []
1551getExps (PExp _ _ _ tm : xs) = tm : getExps xs
1552getExps (_ : xs) = getExps xs
1554getShowArgs :: [PArg] -> [PArg]
1555getShowArgs [] = []
1556getShowArgs (e@(PExp _ _ _ tm) : xs) = e : getShowArgs xs
1557getShowArgs (e : xs) | AlwaysShow `elem` argopts e = e : getShowArgs xs
1558getShowArgs (_ : xs) = getShowArgs xs
1560getConsts :: [PArg] -> [PTerm]
1561getConsts [] = []
1562getConsts (PConstraint _ _ _ tm : xs) = tm : getConsts xs
1563getConsts (_ : xs) = getConsts xs
1565getAll :: [PArg] -> [PTerm]
1566getAll = map getTm
1569-- | Show Idris name
1570showName :: Maybe IState -- ^^ the Idris state, for information about names and colours
1571 -> [(Name, Bool)] -- ^^ the bound variables and whether they're implicit
1572 -> PPOption -- ^^ pretty printing options
1573 -> Bool -- ^^ whether to colourise
1574 -> Name -- ^^ the term to show
1575 -> String
1576showName ist bnd ppo colour n = case ist of
1577 Just i -> if colour then colourise n (idris_colourTheme i) else showbasic n
1578 Nothing -> showbasic n
1579 where name = if ppopt_impl ppo then show n else showbasic n
1580 showbasic n@(UN _) = showCG n
1581 showbasic (MN i s) = str s
1582 showbasic (NS n s) = showSep "." (map str (reverse s)) ++ "." ++ showbasic n
1583 showbasic (SN s) = show s
1584 fst3 (x, _, _) = x
1585 colourise n t = let ctxt' = fmap tt_ctxt ist in
1586 case ctxt' of
1587 Nothing -> name
1588 Just ctxt | Just impl <- lookup n bnd -> if impl then colouriseImplicit t name
1589 else colouriseBound t name
1590 | isDConName n ctxt -> colouriseData t name
1591 | isFnName n ctxt -> colouriseFun t name
1592 | isTConName n ctxt -> colouriseType t name
1593 -- The assumption is that if a name is not bound and does not exist in the
1594 -- global context, then we're somewhere in which implicit info has been lost
1595 -- (like error messages). Thus, unknown vars are colourised as implicits.
1596 | otherwise -> colouriseImplicit t name
1598showTm :: IState -- ^^ the Idris state, for information about identifiers and colours
1599 -> PTerm -- ^^ the term to show
1600 -> String
1601showTm ist = displayDecorated (consoleDecorate ist) .
1602 renderPretty 0.8 100000 .
1603 prettyImp (ppOptionIst ist)
1605-- | Show a term with implicits, no colours
1606showTmImpls :: PTerm -> String
1607showTmImpls = flip (displayS . renderCompact . prettyImp verbosePPOption) ""
1611instance Sized PTerm where
1612 size (PQuote rawTerm) = size rawTerm
1613 size (PRef fc name) = size name
1614 size (PLam name ty bdy) = 1 + size ty + size bdy
1615 size (PPi plicity name ty bdy) = 1 + size ty + size bdy
1616 size (PLet name ty def bdy) = 1 + size ty + size def + size bdy
1617 size (PTyped trm ty) = 1 + size trm + size ty
1618 size (PApp fc name args) = 1 + size args
1619 size (PAppBind fc name args) = 1 + size args
1620 size (PCase fc trm bdy) = 1 + size trm + size bdy
1621 size (PTrue fc _) = 1
1622 size (PRefl fc _) = 1
1623 size (PResolveTC fc) = 1
1624 size (PEq fc _ _ left right) = 1 + size left + size right
1625 size (PRewrite fc left right _) = 1 + size left + size right
1626 size (PPair fc _ left right) = 1 + size left + size right
1627 size (PDPair fs _ left ty right) = 1 + size left + size ty + size right
1628 size (PAlternative a alts) = 1 + size alts
1629 size (PHidden hidden) = size hidden
1630 size (PUnifyLog tm) = size tm
1631 size (PDisamb _ tm) = size tm
1632 size (PNoImplicits tm) = size tm
1633 size PType = 1
1634 size (PUniverse _) = 1
1635 size (PConstant const) = 1 + size const
1636 size Placeholder = 1
1637 size (PDoBlock dos) = 1 + size dos
1638 size (PIdiom fc term) = 1 + size term
1639 size (PReturn fc) = 1
1640 size (PMetavar name) = 1
1641 size (PProof tactics) = size tactics
1642 size (PElabError err) = size err
1643 size PImpossible = 1
1644 size _ = 0
1646getPArity :: PTerm -> Int
1647getPArity (PPi _ _ _ sc) = 1 + getPArity sc
1648getPArity _ = 0
1650-- Return all names, free or globally bound, in the given term.
1652allNamesIn :: PTerm -> [Name]
1653allNamesIn tm = nub $ ni [] tm
1654 where -- TODO THINK added niTacImp, but is it right?
1655 ni env (PRef _ n)
1656 | not (n `elem` env) = [n]
1657 ni env (PPatvar _ n) = [n]
1658 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
1659 ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
1660 ni env (PCase _ c os) = ni env c ++ concatMap (ni env) (map snd os)
1661 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc
1662 ni env (PPi p n ty sc) = niTacImp env p ++ ni env ty ++ ni (n:env) sc
1663 ni env (PHidden tm) = ni env tm
1664 ni env (PEq _ _ _ l r) = ni env l ++ ni env r
1665 ni env (PRewrite _ l r _) = ni env l ++ ni env r
1666 ni env (PTyped l r) = ni env l ++ ni env r
1667 ni env (PPair _ _ l r) = ni env l ++ ni env r
1668 ni env (PDPair _ _ (PRef _ n) t r) = ni env t ++ ni (n:env) r
1669 ni env (PDPair _ _ l t r) = ni env l ++ ni env t ++ ni env r
1670 ni env (PAlternative a ls) = concatMap (ni env) ls
1671 ni env (PUnifyLog tm) = ni env tm
1672 ni env (PDisamb _ tm) = ni env tm
1673 ni env (PNoImplicits tm) = ni env tm
1674 ni env _ = []
1676 niTacImp env (TacImp _ _ scr) = ni env scr
1677 niTacImp _ _ = []
1679-- Return all names defined in binders in the given term
1680boundNamesIn :: PTerm -> [Name]
1681boundNamesIn tm = nub $ ni tm
1682 where -- TODO THINK Added niTacImp, but is it right?
1683 ni (PApp _ f as) = ni f ++ concatMap (ni) (map getTm as)
1684 ni (PAppBind _ f as) = ni f ++ concatMap (ni) (map getTm as)
1685 ni (PCase _ c os) = ni c ++ concatMap (ni) (map snd os)
1686 ni (PLam n ty sc) = n : (ni ty ++ ni sc)
1687 ni (PLet n ty val sc) = n : (ni ty ++ ni val ++ ni sc)
1688 ni (PPi p n ty sc) = niTacImp p ++ (n : (ni ty ++ ni sc))
1689 ni (PEq _ _ _ l r) = ni l ++ ni r
1690 ni (PRewrite _ l r _) = ni l ++ ni r
1691 ni (PTyped l r) = ni l ++ ni r
1692 ni (PPair _ _ l r) = ni l ++ ni r
1693 ni (PDPair _ _ (PRef _ n) t r) = ni t ++ ni r
1694 ni (PDPair _ _ l t r) = ni l ++ ni t ++ ni r
1695 ni (PAlternative a as) = concatMap (ni) as
1696 ni (PHidden tm) = ni tm
1697 ni (PUnifyLog tm) = ni tm
1698 ni (PDisamb _ tm) = ni tm
1699 ni (PNoImplicits tm) = ni tm
1700 ni _ = []
1702 niTacImp (TacImp _ _ scr) = ni scr
1703 niTacImp _ = []
1705-- Return names which are valid implicits in the given term (type).
1706implicitNamesIn :: [Name] -> IState -> PTerm -> [Name]
1707implicitNamesIn uvars ist tm = nub $ ni [] tm
1708 where
1709 ni env (PRef _ n)
1710 | not (n `elem` env)
1711 = case lookupTy n (tt_ctxt ist) of
1712 [] -> [n]
1713 _ -> if n `elem` uvars then [n] else []
1714 ni env (PApp _ f@(PRef _ n) as)
1715 | n `elem` uvars = ni env f ++ concatMap (ni env) (map getTm as)
1716 | otherwise = concatMap (ni env) (map getTm as)
1717 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
1718 ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
1719 ni env (PCase _ c os) = ni env c ++
1720 -- names in 'os', not counting the names bound in the cases
1721 (nub (concatMap (ni env) (map snd os))
1722 \\ nub (concatMap (ni env) (map fst os)))
1723 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc
1724 ni env (PPi p n ty sc) = ni env ty ++ ni (n:env) sc
1725 ni env (PEq _ _ _ l r) = ni env l ++ ni env r
1726 ni env (PRewrite _ l r _) = ni env l ++ ni env r
1727 ni env (PTyped l r) = ni env l ++ ni env r
1728 ni env (PPair _ _ l r) = ni env l ++ ni env r
1729 ni env (PDPair _ _ (PRef _ n) t r) = ni env t ++ ni (n:env) r
1730 ni env (PDPair _ _ l t r) = ni env l ++ ni env t ++ ni env r
1731 ni env (PAlternative a as) = concatMap (ni env) as
1732 ni env (PHidden tm) = ni env tm
1733 ni env (PUnifyLog tm) = ni env tm
1734 ni env (PDisamb _ tm) = ni env tm
1735 ni env (PNoImplicits tm) = ni env tm
1736 ni env _ = []
1738-- Return names which are free in the given term.
1739namesIn :: [(Name, PTerm)] -> IState -> PTerm -> [Name]
1740namesIn uvars ist tm = nub $ ni [] tm
1741 where
1742 ni env (PRef _ n)
1743 | not (n `elem` env)
1744 = case lookupTy n (tt_ctxt ist) of
1745 [] -> [n]
1746 _ -> if n `elem` (map fst uvars) then [n] else []
1747 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
1748 ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
1749 ni env (PCase _ c os) = ni env c ++
1750 -- names in 'os', not counting the names bound in the cases
1751 (nub (concatMap (ni env) (map snd os))
1752 \\ nub (concatMap (ni env) (map fst os)))
1753 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc
1754 ni env (PPi p n ty sc) = niTacImp env p ++ ni env ty ++ ni (n:env) sc
1755 ni env (PEq _ _ _ l r) = ni env l ++ ni env r
1756 ni env (PRewrite _ l r _) = ni env l ++ ni env r
1757 ni env (PTyped l r) = ni env l ++ ni env r
1758 ni env (PPair _ _ l r) = ni env l ++ ni env r
1759 ni env (PDPair _ _ (PRef _ n) t r) = ni env t ++ ni (n:env) r
1760 ni env (PDPair _ _ l t r) = ni env l ++ ni env t ++ ni env r
1761 ni env (PAlternative a as) = concatMap (ni env) as
1762 ni env (PHidden tm) = ni env tm
1763 ni env (PUnifyLog tm) = ni env tm
1764 ni env (PDisamb _ tm) = ni env tm
1765 ni env (PNoImplicits tm) = ni env tm
1766 ni env _ = []
1768 niTacImp env (TacImp _ _ scr) = ni env scr
1769 niTacImp _ _ = []
1771-- Return which of the given names are used in the given term.
1773usedNamesIn :: [Name] -> IState -> PTerm -> [Name]
1774usedNamesIn vars ist tm = nub $ ni [] tm
1775 where -- TODO THINK added niTacImp, but is it right?
1776 ni env (PRef _ n)
1777 | n `elem` vars && not (n `elem` env)
1778 = case lookupDefExact n (tt_ctxt ist) of
1779 Nothing -> [n]
1780 _ -> []
1781 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
1782 ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
1783 ni env (PCase _ c os) = ni env c ++ concatMap (ni env) (map snd os)
1784 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc
1785 ni env (PPi p n ty sc) = niTacImp env p ++ ni env ty ++ ni (n:env) sc
1786 ni env (PEq _ _ _ l r) = ni env l ++ ni env r
1787 ni env (PRewrite _ l r _) = ni env l ++ ni env r
1788 ni env (PTyped l r) = ni env l ++ ni env r
1789 ni env (PPair _ _ l r) = ni env l ++ ni env r
1790 ni env (PDPair _ _ (PRef _ n) t r) = ni env t ++ ni (n:env) r
1791 ni env (PDPair _ _ l t r) = ni env l ++ ni env t ++ ni env r
1792 ni env (PAlternative a as) = concatMap (ni env) as
1793 ni env (PHidden tm) = ni env tm
1794 ni env (PUnifyLog tm) = ni env tm
1795 ni env (PDisamb _ tm) = ni env tm
1796 ni env (PNoImplicits tm) = ni env tm
1797 ni env _ = []
1799 niTacImp env (TacImp _ _ scr) = ni env scr
1800 niTacImp _ _ = []
1802-- Return the list of inaccessible (= dotted) positions for a name.
1803getErasureInfo :: IState -> Name -> [Int]
1804getErasureInfo ist n =
1805 case lookupCtxtExact n (idris_optimisation ist) of
1806 Just (Optimise inacc detagg) -> map fst inacc
1807 Nothing -> []