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