git.iko.soy/Idris-dev
on ee32989 help sign in
Idris-dev/src/Idris/AbsSyntaxTree.hs
1886 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 elab_stack :: [Name] -- ^ Stack of names currently being elaborated
219 }
221-- Required for parsers library, and therefore trifecta
222instance Show IState where
223 show = const "{internal state}"
225data SizeChange = Smaller | Same | Bigger | Unknown
226 deriving (Show, Eq)
227{-!
228deriving instance Binary SizeChange
229deriving instance NFData SizeChange
230!-}
232type SCGEntry = (Name, [Maybe (Int, SizeChange)])
233type UsageReason = (Name, Int) -- fn_name, its_arg_number
235data CGInfo = CGInfo { argsdef :: [Name],
236 calls :: [(Name, [[Name]])],
237 scg :: [SCGEntry],
238 argsused :: [Name],
239 usedpos :: [(Int, [UsageReason])] }
240 deriving Show
241{-!
242deriving instance Binary CGInfo
243deriving instance NFData CGInfo
244!-}
246primDefs = [sUN "unsafePerformPrimIO",
247 sUN "mkLazyForeignPrim",
248 sUN "mkForeignPrim",
249 sUN "void"]
251-- information that needs writing for the current module's .ibc file
252data IBCWrite = IBCFix FixDecl
253 | IBCImp Name
254 | IBCStatic Name
255 | IBCClass Name
256 | IBCInstance Bool Name Name
257 | IBCDSL Name
258 | IBCData Name
259 | IBCOpt Name
260 | IBCMetavar Name
261 | IBCSyntax Syntax
262 | IBCKeyword String
263 | IBCImport (Bool, FilePath) -- True = import public
264 | IBCImportDir FilePath
265 | IBCObj Codegen FilePath
266 | IBCLib Codegen String
267 | IBCCGFlag Codegen String
268 | IBCDyLib String
269 | IBCHeader Codegen String
270 | IBCAccess Name Accessibility
271 | IBCMetaInformation Name MetaInformation
272 | IBCTotal Name Totality
273 | IBCFlags Name [FnOpt]
274 | IBCFnInfo Name FnInfo
275 | IBCTrans Name (Term, Term)
276 | IBCErrRev (Term, Term)
277 | IBCCG Name
278 | IBCDoc Name
279 | IBCCoercion Name
280 | IBCDef Name -- i.e. main context
281 | IBCNameHint (Name, Name)
282 | IBCLineApp FilePath Int PTerm
283 | IBCErrorHandler Name
284 | IBCFunctionErrorHandler Name Name Name
285 | IBCPostulate Name
286 | IBCTotCheckErr FC String
287 | IBCParsedRegion FC
288 deriving Show
290-- | The initial state for the compiler
291idrisInit :: IState
292idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext
293 emptyContext emptyContext emptyContext emptyContext
294 emptyContext emptyContext emptyContext emptyContext
295 emptyContext emptyContext emptyContext emptyContext
296 [] [] [] defaultOpts 6 [] [] [] [] emptySyntaxRules [] [] [] [] [] [] []
297 [] [] Nothing [] Nothing [] [] Nothing Nothing [] Hidden False [] Nothing [] []
298 (RawOutput stdout) True defaultTheme [] (0, emptyContext) emptyContext M.empty
299 AutomaticWidth S.empty Nothing Nothing [] []
301-- | The monad for the main REPL - reading and processing files and updating
302-- global state (hence the IO inner monad).
303--type Idris = WriterT [Either String (IO ())] (State IState a))
304type Idris = StateT IState (ExceptT Err IO)
306-- Commands in the REPL
308data Codegen = Via String
309-- | ViaC
310-- | ViaJava
311-- | ViaNode
312-- | ViaJavaScript
313-- | ViaLLVM
314 | Bytecode
315 deriving (Show, Eq)
317-- | REPL commands
318data Command = Quit
319 | Help
320 | Eval PTerm
321 | NewDefn [PDecl] -- ^ Each 'PDecl' should be either a type declaration (at most one) or a clause defining the same name.
322 | Undefine [Name]
323 | Check PTerm
324 | DocStr (Either Name Const)
325 | TotCheck Name
326 | Reload
327 | Load FilePath (Maybe Int) -- up to maximum line number
328 | ChangeDirectory FilePath
329 | ModImport String
330 | Edit
331 | Compile Codegen String
332 | Execute
333 | ExecVal PTerm
334 | Metavars
335 | Prove Name
336 | AddProof (Maybe Name)
337 | RmProof Name
338 | ShowProof Name
339 | Proofs
340 | Universes
341 | LogLvl Int
342 | Spec PTerm
343 | HNF PTerm
344 | TestInline PTerm
345 | Defn Name
346 | Missing Name
347 | DynamicLink FilePath
348 | ListDynamic
349 | Pattelab PTerm
350 | Search [String] PTerm
351 | CaseSplitAt Bool Int Name
352 | AddClauseFrom Bool Int Name
353 | AddProofClauseFrom Bool Int Name
354 | AddMissing Bool Int Name
355 | MakeWith Bool Int Name
356 | MakeLemma Bool Int Name
357 | DoProofSearch Bool Bool Int Name [Name]
358 -- ^ the first bool is whether to update,
359 -- the second is whether to search recursively (i.e. for the arguments)
360 | SetOpt Opt
361 | UnsetOpt Opt
362 | NOP
363 | SetColour ColourType IdrisColour
364 | ColourOn
365 | ColourOff
366 | ListErrorHandlers
367 | SetConsoleWidth ConsoleWidth
368 | Apropos [String] String
369 | WhoCalls Name
370 | CallsWho Name
371 | MakeDoc String -- IdrisDoc
372 | Warranty
373 | PrintDef Name
374 | PPrint OutputFmt Int PTerm
375 | TransformInfo Name
376 -- Debugging commands
377 | DebugInfo Name
378 | DebugUnify PTerm PTerm
380data OutputFmt = HTMLOutput | LaTeXOutput
382data Opt = Filename String
383 | Quiet
384 | NoBanner
385 | ColourREPL Bool
386 | Ideslave
387 | IdeslaveSocket
388 | ShowLibs
389 | ShowLibdir
390 | ShowIncs
391 | NoBasePkgs
392 | NoPrelude
393 | NoBuiltins -- only for the really primitive stuff!
394 | NoREPL
395 | OLogging Int
396 | Output String
397 | TypeCase
398 | TypeInType
399 | DefaultTotal
400 | DefaultPartial
401 | WarnPartial
402 | WarnReach
403 | NoCoverage
404 | ErrContext
405 | ShowImpl
406 | Verbose
407 | Port String -- REPL TCP port
408 | IBCSubDir String
409 | ImportDir String
410 | PkgBuild String
411 | PkgInstall String
412 | PkgClean String
413 | PkgCheck String
414 | PkgREPL String
415 | PkgMkDoc String -- IdrisDoc
416 | PkgTest String
417 | PkgIndex FilePath
418 | WarnOnly
419 | Pkg String
420 | BCAsm String
421 | DumpDefun String
422 | DumpCases String
423 | UseCodegen Codegen
424 | OutputTy OutputType
425 | Extension LanguageExt
426 | InterpretScript String
427 | EvalExpr String
428 | TargetTriple String
429 | TargetCPU String
430 | OptLevel Int
431 | AddOpt Optimisation
432 | RemoveOpt Optimisation
433 | Client String
434 | ShowOrigErr
435 | AutoWidth -- ^ Automatically adjust terminal width
436 | AutoSolve -- ^ Automatically issue "solve" tactic in interactive prover
437 deriving (Show, Eq)
439-- Parsed declarations
441data Fixity = Infixl { prec :: Int }
442 | Infixr { prec :: Int }
443 | InfixN { prec :: Int }
444 | PrefixN { prec :: Int }
445 deriving Eq
446{-!
447deriving instance Binary Fixity
448deriving instance NFData Fixity
449!-}
451instance Show Fixity where
452 show (Infixl i) = "infixl " ++ show i
453 show (Infixr i) = "infixr " ++ show i
454 show (InfixN i) = "infix " ++ show i
455 show (PrefixN i) = "prefix " ++ show i
457data FixDecl = Fix Fixity String
458 deriving Eq
460instance Show FixDecl where
461 show (Fix f s) = show f ++ " " ++ s
463{-!
464deriving instance Binary FixDecl
465deriving instance NFData FixDecl
466!-}
468instance Ord FixDecl where
469 compare (Fix x _) (Fix y _) = compare (prec x) (prec y)
472data Static = Static | Dynamic
473 deriving (Show, Eq)
474{-!
475deriving instance Binary Static
476deriving instance NFData Static
477!-}
479-- Mark bindings with their explicitness, and laziness
480data Plicity = Imp { pargopts :: [ArgOpt],
481 pstatic :: Static,
482 pparam :: Bool }
483 | Exp { pargopts :: [ArgOpt],
484 pstatic :: Static,
485 pparam :: Bool } -- this is a param (rather than index)
486 | Constraint { pargopts :: [ArgOpt],
487 pstatic :: Static }
488 | TacImp { pargopts :: [ArgOpt],
489 pstatic :: Static,
490 pscript :: PTerm }
491 deriving (Show, Eq)
493{-!
494deriving instance Binary Plicity
495deriving instance NFData Plicity
496!-}
498impl = Imp [] Dynamic False
499expl = Exp [] Dynamic False
500expl_param = Exp [] Dynamic True
501constraint = Constraint [] Static
502tacimpl t = TacImp [] Dynamic t
504data FnOpt = Inlinable -- always evaluate when simplifying
505 | TotalFn | PartialFn | CoveringFn
506 | Coinductive | AssertTotal
507 | Dictionary -- type class dictionary, eval only when
508 -- a function argument, and further evaluation resutls
509 | Implicit -- implicit coercion
510 | NoImplicit -- do not apply implicit coercions
511 | CExport String -- export, with a C name
512 | ErrorHandler -- ^^ an error handler for use with the ErrorReflection extension
513 | ErrorReverse -- ^^ attempt to reverse normalise before showing in error
514 | Reflection -- a reflecting function, compile-time only
515 | Specialise [(Name, Maybe Int)] -- specialise it, freeze these names
516 | Constructor -- Data constructor type
517 deriving (Show, Eq)
518{-!
519deriving instance Binary FnOpt
520deriving instance NFData FnOpt
521!-}
523type FnOpts = [FnOpt]
525inlinable :: FnOpts -> Bool
526inlinable = elem Inlinable
528dictionary :: FnOpts -> Bool
529dictionary = elem Dictionary
532-- | Data declaration options
533data DataOpt = Codata -- ^ Set if the the data-type is coinductive
534 | DefaultEliminator -- ^ Set if an eliminator should be generated for data type
535 | DefaultCaseFun -- ^ Set if a case function should be generated for data type
536 | DataErrRev
537 deriving (Show, Eq)
539type DataOpts = [DataOpt]
541-- | Type provider - what to provide
542data ProvideWhat' t = ProvTerm t t -- ^ the first is the goal type, the second is the term
543 | ProvPostulate t -- ^ goal type must be Type, so only term
544 deriving (Show, Eq, Functor)
546type ProvideWhat = ProvideWhat' PTerm
548-- | Top-level declarations such as compiler directives, definitions,
549-- datatypes and typeclasses.
550data PDecl' t
551 = PFix FC Fixity [String] -- ^ Fixity declaration
552 | PTy (Docstring (Either Err PTerm)) [(Name, Docstring (Either Err PTerm))] SyntaxInfo FC FnOpts Name t -- ^ Type declaration
553 | PPostulate (Docstring (Either Err PTerm)) SyntaxInfo FC FnOpts Name t -- ^ Postulate
554 | PClauses FC FnOpts Name [PClause' t] -- ^ Pattern clause
555 | PCAF FC Name t -- ^ Top level constant
556 | PData (Docstring (Either Err PTerm)) [(Name, Docstring (Either Err PTerm))] SyntaxInfo FC DataOpts (PData' t) -- ^ Data declaration.
557 | PParams FC [(Name, t)] [PDecl' t] -- ^ Params block
558 | PNamespace String [PDecl' t] -- ^ New namespace
559 | PRecord (Docstring (Either Err PTerm)) SyntaxInfo FC Name t DataOpts (Docstring (Either Err PTerm)) Name t -- ^ Record declaration
560 | PClass (Docstring (Either Err PTerm)) SyntaxInfo FC
561 [t] -- constraints
562 Name
563 [(Name, t)] -- parameters
564 [(Name, Docstring (Either Err PTerm))] -- parameter docstrings
565 [PDecl' t] -- declarations
566 -- ^ Type class: arguments are documentation, syntax info, source location, constraints,
567 -- class name, parameters, method declarations
568 | PInstance SyntaxInfo FC [t] -- constraints
569 Name -- class
570 [t] -- parameters
571 t -- full instance type
572 (Maybe Name) -- explicit name
573 [PDecl' t]
574 -- ^ Instance declaration: arguments are syntax info, source location, constraints,
575 -- class name, parameters, full instance type, optional explicit name, and definitions
576 | PDSL Name (DSL' t) -- ^ DSL declaration
577 | PSyntax FC Syntax -- ^ Syntax definition
578 | PMutual FC [PDecl' t] -- ^ Mutual block
579 | PDirective (Idris ()) -- ^ Compiler directive. The parser inserts the corresponding action in the Idris monad.
580 | PProvider SyntaxInfo FC (ProvideWhat' t) Name -- ^ Type provider. The first t is the type, the second is the term
581 | PTransform FC Bool t t -- ^ Source-to-source transformation rule. If
582 -- bool is True, lhs and rhs must be convertible
583 deriving Functor
584{-!
585deriving instance Binary PDecl'
586deriving instance NFData PDecl'
587!-}
589-- For elaborator state
590data EState = EState {
591 case_decls :: [PDecl],
592 delayed_elab :: [Elab' EState ()]
593 }
595initEState = EState [] []
597type ElabD a = Elab' EState a
599-- | One clause of a top-level definition. Term arguments to constructors are:
600--
601-- 1. The whole application (missing for PClauseR and PWithR because they're within a "with" clause)
602--
603-- 2. The list of extra 'with' patterns
604--
605-- 3. The right-hand side
606--
607-- 4. The where block (PDecl' t)
609data PClause' t = PClause FC Name t [t] t [PDecl' t] -- ^ A normal top-level definition.
610 | PWith FC Name t [t] t [PDecl' t]
611 | PClauseR FC [t] t [PDecl' t]
612 | PWithR FC [t] t [PDecl' t]
613 deriving Functor
614{-!
615deriving instance Binary PClause'
616deriving instance NFData PClause'
617!-}
619-- | Data declaration
620data PData' t = PDatadecl { d_name :: Name, -- ^ The name of the datatype
621 d_tcon :: t, -- ^ Type constructor
622 d_cons :: [(Docstring (Either Err PTerm), [(Name, Docstring (Either Err PTerm))], Name, t, FC, [Name])] -- ^ Constructors
623 }
624 -- ^ Data declaration
625 | PLaterdecl { d_name :: Name, d_tcon :: t }
626 -- ^ "Placeholder" for data whose constructors are defined later
627 deriving Functor
628{-!
629deriving instance Binary PData'
630deriving instance NFData PData'
631!-}
633-- Handy to get a free function for applying PTerm -> PTerm functions
634-- across a program, by deriving Functor
636type PDecl = PDecl' PTerm
637type PData = PData' PTerm
638type PClause = PClause' PTerm
640-- get all the names declared in a decl
642declared :: PDecl -> [Name]
643declared (PFix _ _ _) = []
644declared (PTy _ _ _ _ _ n t) = [n]
645declared (PPostulate _ _ _ _ n t) = [n]
646declared (PClauses _ _ n _) = [] -- not a declaration
647declared (PCAF _ n _) = [n]
648declared (PData _ _ _ _ _ (PDatadecl n _ ts)) = n : map fstt ts
649 where fstt (_, _, a, _, _, _) = a
650declared (PData _ _ _ _ _ (PLaterdecl n _)) = [n]
651declared (PParams _ _ ds) = concatMap declared ds
652declared (PNamespace _ ds) = concatMap declared ds
653declared (PRecord _ _ _ n _ _ _ c _) = [n, c]
654declared (PClass _ _ _ _ n _ _ ms) = n : concatMap declared ms
655declared (PInstance _ _ _ _ _ _ _ _) = []
656declared (PDSL n _) = [n]
657declared (PSyntax _ _) = []
658declared (PMutual _ ds) = concatMap declared ds
659declared (PDirective _) = []
661-- get the names declared, not counting nested parameter blocks
662tldeclared :: PDecl -> [Name]
663tldeclared (PFix _ _ _) = []
664tldeclared (PTy _ _ _ _ _ n t) = [n]
665tldeclared (PPostulate _ _ _ _ n t) = [n]
666tldeclared (PClauses _ _ n _) = [] -- not a declaration
667tldeclared (PRecord _ _ _ n _ _ _ c _) = [n, c]
668tldeclared (PData _ _ _ _ _ (PDatadecl n _ ts)) = n : map fstt ts
669 where fstt (_, _, a, _, _, _) = a
670tldeclared (PParams _ _ ds) = []
671tldeclared (PMutual _ ds) = concatMap tldeclared ds
672tldeclared (PNamespace _ ds) = concatMap tldeclared ds
673tldeclared (PClass _ _ _ _ n _ _ ms) = concatMap tldeclared ms
674tldeclared (PInstance _ _ _ _ _ _ _ _) = []
675tldeclared _ = []
677defined :: PDecl -> [Name]
678defined (PFix _ _ _) = []
679defined (PTy _ _ _ _ _ n t) = []
680defined (PPostulate _ _ _ _ n t) = []
681defined (PClauses _ _ n _) = [n] -- not a declaration
682defined (PCAF _ n _) = [n]
683defined (PData _ _ _ _ _ (PDatadecl n _ ts)) = n : map fstt ts
684 where fstt (_, _, a, _, _, _) = a
685defined (PData _ _ _ _ _ (PLaterdecl n _)) = []
686defined (PParams _ _ ds) = concatMap defined ds
687defined (PNamespace _ ds) = concatMap defined ds
688defined (PRecord _ _ _ n _ _ _ c _) = [n, c]
689defined (PClass _ _ _ _ n _ _ ms) = n : concatMap defined ms
690defined (PInstance _ _ _ _ _ _ _ _) = []
691defined (PDSL n _) = [n]
692defined (PSyntax _ _) = []
693defined (PMutual _ ds) = concatMap defined ds
694defined (PDirective _) = []
695--defined _ = []
697updateN :: [(Name, Name)] -> Name -> Name
698updateN ns n | Just n' <- lookup n ns = n'
699updateN _ n = n
701updateNs :: [(Name, Name)] -> PTerm -> PTerm
702updateNs [] t = t
703updateNs ns t = mapPT updateRef t
704 where updateRef (PRef fc f) = PRef fc (updateN ns f)
705 updateRef t = t
707-- updateDNs :: [(Name, Name)] -> PDecl -> PDecl
708-- updateDNs [] t = t
709-- updateDNs ns (PTy s f n t) | Just n' <- lookup n ns = PTy s f n' t
710-- updateDNs ns (PClauses f n c) | Just n' <- lookup n ns = PClauses f n' (map updateCNs c)
711-- where updateCNs ns (PClause n l ts r ds)
712-- = PClause (updateN ns n) (fmap (updateNs ns) l)
713-- (map (fmap (updateNs ns)) ts)
714-- (fmap (updateNs ns) r)
715-- (map (updateDNs ns) ds)
716-- updateDNs ns c = c
718data PunInfo = IsType | IsTerm | TypeOrTerm deriving (Eq, Show)
720-- | High level language terms
721data PTerm = PQuote Raw -- ^ Inclusion of a core term into the high-level language
722 | PRef FC Name -- ^ A reference to a variable
723 | PInferRef FC Name -- ^ A name to be defined later
724 | PPatvar FC Name -- ^ A pattern variable
725 | PLam FC Name PTerm PTerm -- ^ A lambda abstraction
726 | PPi Plicity Name PTerm PTerm -- ^ (n : t1) -> t2
727 | PLet FC Name PTerm PTerm PTerm -- ^ A let binding
728 | PTyped PTerm PTerm -- ^ Term with explicit type
729 | PApp FC PTerm [PArg] -- ^ e.g. IO (), List Char, length x
730 | PAppBind FC PTerm [PArg] -- ^ implicitly bound application
731 | PMatchApp FC Name -- ^ Make an application by type matching
732 | PCase FC PTerm [(PTerm, PTerm)] -- ^ A case expression. Args are source location, scrutinee, and a list of pattern/RHS pairs
733 | PTrue FC PunInfo -- ^ Unit type..?
734 | PRefl FC PTerm -- ^ The canonical proof of the equality type
735 | PResolveTC FC -- ^ Solve this dictionary by type class resolution
736 | PEq FC PTerm PTerm PTerm PTerm -- ^ Heterogeneous equality type: A = B
737 | PRewrite FC PTerm PTerm (Maybe PTerm) -- ^ "rewrite" syntax, with optional result type
738 | PPair FC PunInfo PTerm PTerm -- ^ A pair (a, b) and whether it's a product type or a pair (solved by elaboration)
739 | 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)
740 | PAs FC Name PTerm -- ^ @-pattern, valid LHS only
741 | PAlternative Bool [PTerm] -- ^ True if only one may work. (| A, B, C|)
742 | PHidden PTerm -- ^ Irrelevant or hidden pattern
743 | PType -- ^ 'Type' type
744 | PUniverse Universe -- ^ Some universe
745 | PGoal FC PTerm Name PTerm -- ^ quoteGoal, used for %reflection functions
746 | PConstant Const -- ^ Builtin types
747 | Placeholder -- ^ Underscore
748 | PDoBlock [PDo] -- ^ Do notation
749 | PIdiom FC PTerm -- ^ Idiom brackets
750 | PReturn FC
751 | PMetavar Name -- ^ A metavariable, ?name
752 | PProof [PTactic] -- ^ Proof script
753 | PTactics [PTactic] -- ^ As PProof, but no auto solving
754 | PElabError Err -- ^ Error to report on elaboration
755 | PImpossible -- ^ Special case for declaring when an LHS can't typecheck
756 | PCoerced PTerm -- ^ To mark a coerced argument, so as not to coerce twice
757 | PDisamb [[T.Text]] PTerm -- ^ Preferences for explicit namespaces
758 | PUnifyLog PTerm -- ^ dump a trace of unifications when building term
759 | PNoImplicits PTerm -- ^ never run implicit converions on the term
760 | PQuasiquote PTerm (Maybe PTerm) -- ^ `(Term [: Term])
761 | PUnquote PTerm -- ^ ,Term
762 deriving Eq
765{-!
766deriving instance Binary PTerm
767deriving instance NFData PTerm
768!-}
770mapPT :: (PTerm -> PTerm) -> PTerm -> PTerm
771mapPT f t = f (mpt t) where
772 mpt (PLam fc n t s) = PLam fc n (mapPT f t) (mapPT f s)
773 mpt (PPi p n t s) = PPi p n (mapPT f t) (mapPT f s)
774 mpt (PLet fc n ty v s) = PLet fc n (mapPT f ty) (mapPT f v) (mapPT f s)
775 mpt (PRewrite fc t s g) = PRewrite fc (mapPT f t) (mapPT f s)
776 (fmap (mapPT f) g)
777 mpt (PApp fc t as) = PApp fc (mapPT f t) (map (fmap (mapPT f)) as)
778 mpt (PAppBind fc t as) = PAppBind fc (mapPT f t) (map (fmap (mapPT f)) as)
779 mpt (PCase fc c os) = PCase fc (mapPT f c) (map (pmap (mapPT f)) os)
780 mpt (PEq fc lt rt l r) = PEq fc (mapPT f lt) (mapPT f rt) (mapPT f l) (mapPT f r)
781 mpt (PTyped l r) = PTyped (mapPT f l) (mapPT f r)
782 mpt (PPair fc p l r) = PPair fc p (mapPT f l) (mapPT f r)
783 mpt (PDPair fc p l t r) = PDPair fc p (mapPT f l) (mapPT f t) (mapPT f r)
784 mpt (PAlternative a as) = PAlternative a (map (mapPT f) as)
785 mpt (PHidden t) = PHidden (mapPT f t)
786 mpt (PDoBlock ds) = PDoBlock (map (fmap (mapPT f)) ds)
787 mpt (PProof ts) = PProof (map (fmap (mapPT f)) ts)
788 mpt (PTactics ts) = PTactics (map (fmap (mapPT f)) ts)
789 mpt (PUnifyLog tm) = PUnifyLog (mapPT f tm)
790 mpt (PDisamb ns tm) = PDisamb ns (mapPT f tm)
791 mpt (PNoImplicits tm) = PNoImplicits (mapPT f tm)
792 mpt (PGoal fc r n sc) = PGoal fc (mapPT f r) n (mapPT f sc)
793 mpt x = x
796data PTactic' t = Intro [Name] | Intros | Focus Name
797 | Refine Name [Bool] | Rewrite t | DoUnify
798 | Induction t
799 | CaseTac t
800 | Equiv t
801 | MatchRefine Name
802 | LetTac Name t | LetTacTy Name t t
803 | Exact t | Compute | Trivial | TCInstance
804 | ProofSearch Bool Bool Int (Maybe Name) [Name]
805 -- ^ the bool is whether to search recursively
806 | Solve
807 | Attack
808 | ProofState | ProofTerm | Undo
809 | Try (PTactic' t) (PTactic' t)
810 | TSeq (PTactic' t) (PTactic' t)
811 | ApplyTactic t -- see Language.Reflection module
812 | ByReflection t
813 | Reflect t
814 | Fill t
815 | GoalType String (PTactic' t)
816 | TCheck t
817 | TEval t
818 | TDocStr (Either Name Const)
819 | TSearch t
820 | Skip
821 | TFail [ErrorReportPart]
822 | Qed | Abandon
823 | SourceFC
824 deriving (Show, Eq, Functor, Foldable, Traversable)
825{-!
826deriving instance Binary PTactic'
827deriving instance NFData PTactic'
828!-}
829instance Sized a => Sized (PTactic' a) where
830 size (Intro nms) = 1 + size nms
831 size Intros = 1
832 size (Focus nm) = 1 + size nm
833 size (Refine nm bs) = 1 + size nm + length bs
834 size (Rewrite t) = 1 + size t
835 size (Induction t) = 1 + size t
836 size (LetTac nm t) = 1 + size nm + size t
837 size (Exact t) = 1 + size t
838 size Compute = 1
839 size Trivial = 1
840 size Solve = 1
841 size Attack = 1
842 size ProofState = 1
843 size ProofTerm = 1
844 size Undo = 1
845 size (Try l r) = 1 + size l + size r
846 size (TSeq l r) = 1 + size l + size r
847 size (ApplyTactic t) = 1 + size t
848 size (Reflect t) = 1 + size t
849 size (Fill t) = 1 + size t
850 size Qed = 1
851 size Abandon = 1
852 size Skip = 1
853 size (TFail ts) = 1 + size ts
854 size SourceFC = 1
856type PTactic = PTactic' PTerm
858data PDo' t = DoExp FC t
859 | DoBind FC Name t
860 | DoBindP FC t t [(t,t)]
861 | DoLet FC Name t t
862 | DoLetP FC t t
863 deriving (Eq, Functor)
864{-!
865deriving instance Binary PDo'
866deriving instance NFData PDo'
867!-}
869instance Sized a => Sized (PDo' a) where
870 size (DoExp fc t) = 1 + size fc + size t
871 size (DoBind fc nm t) = 1 + size fc + size nm + size t
872 size (DoBindP fc l r alts) = 1 + size fc + size l + size r + size alts
873 size (DoLet fc nm l r) = 1 + size fc + size nm + size l + size r
874 size (DoLetP fc l r) = 1 + size fc + size l + size r
876type PDo = PDo' PTerm
878-- The priority gives a hint as to elaboration order. Best to elaborate
879-- things early which will help give a more concrete type to other
880-- variables, e.g. a before (interpTy a).
882data PArg' t = PImp { priority :: Int,
883 machine_inf :: Bool, -- true if the machine inferred it
884 argopts :: [ArgOpt],
885 pname :: Name, getTm :: t }
886 | PExp { priority :: Int,
887 argopts :: [ArgOpt],
888 pname :: Name,
889 getTm :: t }
890 | PConstraint { priority :: Int,
891 argopts :: [ArgOpt],
892 pname :: Name,
893 getTm :: t }
894 | PTacImplicit { priority :: Int,
895 argopts :: [ArgOpt],
896 pname :: Name,
897 getScript :: t,
898 getTm :: t }
899 deriving (Show, Eq, Functor)
901data ArgOpt = AlwaysShow | HideDisplay | InaccessibleArg
902 deriving (Show, Eq)
904instance Sized a => Sized (PArg' a) where
905 size (PImp p _ l nm trm) = 1 + size nm + size trm
906 size (PExp p l nm trm) = 1 + size nm + size trm
907 size (PConstraint p l nm trm) = 1 + size nm +size nm + size trm
908 size (PTacImplicit p l nm scr trm) = 1 + size nm + size scr + size trm
910{-!
911deriving instance Binary PArg'
912deriving instance NFData PArg'
913!-}
915pimp n t mach = PImp 1 mach [] n t
916pexp t = PExp 1 [] (sMN 0 "arg") t
917pconst t = PConstraint 1 [] (sMN 0 "carg") t
918ptacimp n s t = PTacImplicit 2 [] n s t
920type PArg = PArg' PTerm
922-- Type class data
924data ClassInfo = CI { instanceName :: Name,
925 class_methods :: [(Name, (FnOpts, PTerm))],
926 class_defaults :: [(Name, (Name, PDecl))], -- method name -> default impl
927 class_default_superclasses :: [PDecl],
928 class_params :: [Name],
929 class_instances :: [Name] }
930 deriving Show
931{-!
932deriving instance Binary ClassInfo
933deriving instance NFData ClassInfo
934!-}
936-- Type inference data
938data TIData = TIPartial -- ^ a function with a partially defined type
939 | TISolution [Term] -- ^ possible solutions to a metavariable in a type
940 deriving Show
942-- | Miscellaneous information about functions
943data FnInfo = FnInfo { fn_params :: [Int] }
944 deriving Show
945{-!
946deriving instance Binary FnInfo
947!-}
949data OptInfo = Optimise { inaccessible :: [(Int,Name)], -- includes names for error reporting
950 detaggable :: Bool }
951 deriving Show
952{-!
953deriving instance Binary OptInfo
954deriving instance NFData OptInfo
955!-}
958data TypeInfo = TI { con_names :: [Name],
959 codata :: Bool,
960 data_opts :: DataOpts,
961 param_pos :: [Int],
962 mutual_types :: [Name] }
963 deriving Show
964{-!
965deriving instance Binary TypeInfo
966deriving instance NFData TypeInfo
967!-}
969-- Syntactic sugar info
971data DSL' t = DSL { dsl_bind :: t,
972 dsl_return :: t,
973 dsl_apply :: t,
974 dsl_pure :: t,
975 dsl_var :: Maybe t,
976 index_first :: Maybe t,
977 index_next :: Maybe t,
978 dsl_lambda :: Maybe t,
979 dsl_let :: Maybe t,
980 dsl_pi :: Maybe t
981 }
982 deriving (Show, Functor)
983{-!
984deriving instance Binary DSL'
985deriving instance NFData DSL'
986!-}
988type DSL = DSL' PTerm
990data SynContext = PatternSyntax | TermSyntax | AnySyntax
991 deriving Show
992{-!
993deriving instance Binary SynContext
994deriving instance NFData SynContext
995!-}
997data Syntax = Rule [SSymbol] PTerm SynContext
998 deriving Show
1000syntaxNames :: Syntax -> [Name]
1001syntaxNames (Rule syms _ _) = mapMaybe ename syms
1002 where ename (Keyword n) = Just n
1003 ename _ = Nothing
1005syntaxSymbols :: Syntax -> [SSymbol]
1006syntaxSymbols (Rule ss _ _) = ss
1007{-!
1008deriving instance Binary Syntax
1009deriving instance NFData Syntax
1010!-}
1012data SSymbol = Keyword Name
1013 | Symbol String
1014 | Binding Name
1015 | Expr Name
1016 | SimpleExpr Name
1017 deriving (Show, Eq)
1020{-!
1021deriving instance Binary SSymbol
1022deriving instance NFData SSymbol
1023!-}
1025newtype SyntaxRules = SyntaxRules { syntaxRulesList :: [Syntax] }
1027emptySyntaxRules :: SyntaxRules
1028emptySyntaxRules = SyntaxRules []
1030updateSyntaxRules :: [Syntax] -> SyntaxRules -> SyntaxRules
1031updateSyntaxRules rules (SyntaxRules sr) = SyntaxRules newRules
1032 where
1033 newRules = sortBy (ruleSort `on` syntaxSymbols) (rules ++ sr)
1035 ruleSort [] [] = EQ
1036 ruleSort [] _ = LT
1037 ruleSort _ [] = GT
1038 ruleSort (s1:ss1) (s2:ss2) =
1039 case symCompare s1 s2 of
1040 EQ -> ruleSort ss1 ss2
1041 r -> r
1043 -- Better than creating Ord instance for SSymbol since
1044 -- in general this ordering does not really make sense.
1045 symCompare (Keyword n1) (Keyword n2) = compare n1 n2
1046 symCompare (Keyword _) _ = LT
1047 symCompare (Symbol _) (Keyword _) = GT
1048 symCompare (Symbol s1) (Symbol s2) = compare s1 s2
1049 symCompare (Symbol _) _ = LT
1050 symCompare (Binding _) (Keyword _) = GT
1051 symCompare (Binding _) (Symbol _) = GT
1052 symCompare (Binding b1) (Binding b2) = compare b1 b2
1053 symCompare (Binding _) _ = LT
1054 symCompare (Expr _) (Keyword _) = GT
1055 symCompare (Expr _) (Symbol _) = GT
1056 symCompare (Expr _) (Binding _) = GT
1057 symCompare (Expr e1) (Expr e2) = compare e1 e2
1058 symCompare (Expr _) _ = LT
1059 symCompare (SimpleExpr _) (Keyword _) = GT
1060 symCompare (SimpleExpr _) (Symbol _) = GT
1061 symCompare (SimpleExpr _) (Binding _) = GT
1062 symCompare (SimpleExpr _) (Expr _) = GT
1063 symCompare (SimpleExpr e1) (SimpleExpr e2) = compare e1 e2
1065initDSL = DSL (PRef f (sUN ">>="))
1066 (PRef f (sUN "return"))
1067 (PRef f (sUN "<$>"))
1068 (PRef f (sUN "pure"))
1069 Nothing
1070 Nothing
1071 Nothing
1072 Nothing
1073 Nothing
1074 Nothing
1075 where f = fileFC "(builtin)"
1077data Using = UImplicit Name PTerm
1078 | UConstraint Name [Name]
1079 deriving (Show, Eq)
1080{-!
1081deriving instance Binary Using
1082deriving instance NFData Using
1083!-}
1085data SyntaxInfo = Syn { using :: [Using],
1086 syn_params :: [(Name, PTerm)],
1087 syn_namespace :: [String],
1088 no_imp :: [Name],
1089 decoration :: Name -> Name,
1090 inPattern :: Bool,
1091 implicitAllowed :: Bool,
1092 maxline :: Maybe Int,
1093 mut_nesting :: Int,
1094 dsl_info :: DSL,
1095 syn_in_quasiquote :: Int }
1096 deriving Show
1097{-!
1098deriving instance NFData SyntaxInfo
1099deriving instance Binary SyntaxInfo
1100!-}
1102defaultSyntax = Syn [] [] [] [] id False False Nothing 0 initDSL 0
1104expandNS :: SyntaxInfo -> Name -> Name
1105expandNS syn n@(NS _ _) = n
1106expandNS syn n = case syn_namespace syn of
1107 [] -> n
1108 xs -> sNS n xs
1111-- For inferring types of things
1113bi = fileFC "builtin"
1115inferTy = sMN 0 "__Infer"
1116inferCon = sMN 0 "__infer"
1117inferDecl = PDatadecl inferTy
1118 PType
1119 [(emptyDocstring, [], inferCon, PPi impl (sMN 0 "iType") PType (
1120 PPi expl (sMN 0 "ival") (PRef bi (sMN 0 "iType"))
1121 (PRef bi inferTy)), bi, [])]
1122inferOpts = []
1124infTerm t = PApp bi (PRef bi inferCon) [pimp (sMN 0 "iType") Placeholder True, pexp t]
1125infP = P (TCon 6 0) inferTy (TType (UVal 0))
1127getInferTerm, getInferType :: Term -> Term
1128getInferTerm (Bind n b sc) = Bind n b $ getInferTerm sc
1129getInferTerm (App (App _ _) tm) = tm
1130getInferTerm tm = tm -- error ("getInferTerm " ++ show tm)
1132getInferType (Bind n b sc) = Bind n (toTy b) $ getInferType sc
1133 where toTy (Lam t) = Pi t (TType (UVar 0))
1134 toTy (PVar t) = PVTy t
1135 toTy b = b
1136getInferType (App (App _ ty) _) = ty
1140-- Handy primitives: Unit, False, Pair, MkPair, =, mkForeign
1142primNames = [eqTy, eqCon, inferTy, inferCon]
1144unitTy = sUN "Unit"
1145unitCon = sUN "MkUnit"
1147falseDoc = fmap (const $ Msg "") . parseDocstring . T.pack $
1148 "The empty type, also known as the trivially false proposition." ++
1149 "\n\n" ++
1150 "Use `void` or `absurd` to prove anything if you have a variable " ++
1151 "of type `Void` in scope."
1152falseTy = sUN "Void"
1154pairTy = sNS (sUN "Pair") ["Builtins"]
1155pairCon = sNS (sUN "MkPair") ["Builtins"]
1157eqTy = sUN "="
1158eqCon = sUN "Refl"
1159eqDoc = fmap (const (Left $ Msg "")) . parseDocstring . T.pack $
1160 "The propositional equality type. A proof that `x` = `y`." ++
1161 "\n\n" ++
1162 "To use such a proof, pattern-match on it, and the two equal things will " ++
1163 "then need to be the _same_ pattern." ++
1164 "\n\n" ++
1165 "**Note**: Idris's equality type is potentially _heterogeneous_, which means that it " ++
1166 "is possible to state equalities between values of potentially different " ++
1167 "types. However, Idris will attempt the homogeneous case unless it fails to typecheck." ++
1168 "\n\n" ++
1169 "You may need to use `(~=~)` to explicitly request heterogeneous equality."
1171eqDecl = PDatadecl eqTy (piBindp impl [(n "A", PType), (n "B", PType)]
1172 (piBind [(n "x", PRef bi (n "A")), (n "y", PRef bi (n "B"))]
1173 PType))
1174 [(reflDoc, reflParamDoc,
1175 eqCon, PPi impl (n "A") PType (
1176 PPi impl (n "x") (PRef bi (n "A"))
1177 (PApp bi (PRef bi eqTy) [pimp (n "A") Placeholder False,
1178 pimp (n "B") Placeholder False,
1179 pexp (PRef bi (n "x")),
1180 pexp (PRef bi (n "x"))])), bi, [])]
1181 where n a = sUN a
1182 reflDoc = annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $
1183 "A proof that `x` in fact equals `x`. To construct this, you must have already " ++
1184 "shown that both sides are in fact equal."
1185 reflParamDoc = [(n "A", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the type at which the equality is proven"),
1186 (n "x", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the element shown to be equal to itself.")]
1188eqParamDoc = [(n "A", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the type of the left side of the equality"),
1189 (n "B", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the type of the right side of the equality")
1191 where n a = sUN a
1193eqOpts = []
1195-- Defined in builtins.idr
1196sigmaTy = sNS (sUN "Sigma") ["Builtins"]
1197existsCon = sNS (sUN "MkSigma") ["Builtins"]
1199piBind :: [(Name, PTerm)] -> PTerm -> PTerm
1200piBind = piBindp expl
1202piBindp :: Plicity -> [(Name, PTerm)] -> PTerm -> PTerm
1203piBindp p [] t = t
1204piBindp p ((n, ty):ns) t = PPi p n ty (piBindp p ns t)
1207-- Pretty-printing declarations and terms
1209-- These "show" instances render to an absurdly wide screen because inserted line breaks
1210-- could interfere with interactive editing, which calls "show".
1212instance Show PTerm where
1213 showsPrec _ tm = (displayS . renderPretty 1.0 10000000 . prettyImp defaultPPOption) tm
1215instance Show PDecl where
1216 showsPrec _ d = (displayS . renderPretty 1.0 10000000 . showDeclImp verbosePPOption) d
1218instance Show PClause where
1219 showsPrec _ c = (displayS . renderPretty 1.0 10000000 . showCImp verbosePPOption) c
1221instance Show PData where
1222 showsPrec _ d = (displayS . renderPretty 1.0 10000000 . showDImp defaultPPOption) d
1224instance Pretty PTerm OutputAnnotation where
1225 pretty = prettyImp defaultPPOption
1227-- | Colourise annotations according to an Idris state. It ignores the names
1228-- in the annotation, as there's no good way to show extended information on a
1229-- terminal.
1230consoleDecorate :: IState -> OutputAnnotation -> String -> String
1231consoleDecorate ist _ | not (idris_colourRepl ist) = id
1232consoleDecorate ist (AnnConst c) = let theme = idris_colourTheme ist
1233 in if constIsType c
1234 then colouriseType theme
1235 else colouriseData theme
1236consoleDecorate ist (AnnData _ _) = colouriseData (idris_colourTheme ist)
1237consoleDecorate ist (AnnType _ _) = colouriseType (idris_colourTheme ist)
1238consoleDecorate ist (AnnBoundName _ True) = colouriseImplicit (idris_colourTheme ist)
1239consoleDecorate ist (AnnBoundName _ False) = colouriseBound (idris_colourTheme ist)
1240consoleDecorate ist AnnKeyword = colouriseKeyword (idris_colourTheme ist)
1241consoleDecorate ist (AnnName n _ _ _) = let ctxt = tt_ctxt ist
1242 theme = idris_colourTheme ist
1243 in case () of
1244 _ | isDConName n ctxt -> colouriseData theme
1245 _ | isFnName n ctxt -> colouriseFun theme
1246 _ | isTConName n ctxt -> colouriseType theme
1247 _ | isPostulateName n ist -> colourisePostulate theme
1248 _ | otherwise -> id -- don't colourise unknown names
1249consoleDecorate ist (AnnFC _) = id
1250consoleDecorate ist (AnnTextFmt fmt) = Idris.Colours.colourise (colour fmt)
1251 where colour BoldText = IdrisColour Nothing True False True False
1252 colour UnderlineText = IdrisColour Nothing True True False False
1253 colour ItalicText = IdrisColour Nothing True False False True
1254consoleDecorate ist (AnnTerm _ _) = id
1255consoleDecorate ist (AnnSearchResult _) = id
1256consoleDecorate ist (AnnErr _) = id
1258isPostulateName :: Name -> IState -> Bool
1259isPostulateName n ist = S.member n (idris_postulates ist)
1261-- | Pretty-print a high-level closed Idris term with no information about precedence/associativity
1262prettyImp :: PPOption -- ^^ pretty printing options
1263 -> PTerm -- ^^ the term to pretty-print
1264 -> Doc OutputAnnotation
1265prettyImp impl = pprintPTerm impl [] [] []
1267-- | Serialise something to base64 using its Binary instance.
1269-- | Do the right thing for rendering a term in an IState
1270prettyIst :: IState -> PTerm -> Doc OutputAnnotation
1271prettyIst ist = pprintPTerm (ppOptionIst ist) [] [] (idris_infixes ist)
1273-- | Pretty-print a high-level Idris term in some bindings context with infix info
1274pprintPTerm :: PPOption -- ^^ pretty printing options
1275 -> [(Name, Bool)] -- ^^ the currently-bound names and whether they are implicit
1276 -> [Name] -- ^^ names to always show in pi, even if not used
1277 -> [FixDecl] -- ^^ Fixity declarations
1278 -> PTerm -- ^^ the term to pretty-print
1279 -> Doc OutputAnnotation
1280pprintPTerm ppo bnd docArgs infixes = prettySe startPrec bnd
1281 where
1282 startPrec = 0
1283 funcAppPrec = 10
1284 prettySe :: Int -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation
1285 prettySe p bnd (PQuote r) =
1286 text "![" <> pretty r <> text "]"
1287 prettySe p bnd (PPatvar fc n) = pretty n
1288 prettySe p bnd e
1289 | Just str <- slist p bnd e = str
1290 | Just n <- snat p e = annotate (AnnData "Nat" "") (text (show n))
1291 prettySe p bnd (PRef fc n) = prettyName True (ppopt_impl ppo) bnd n
1292 prettySe p bnd (PLam fc n ty sc) =
1293 bracket p startPrec . group . align . hang 2 $
1294 text "\\" <> bindingOf n False <+> text "=>" <$>
1295 prettySe startPrec ((n, False):bnd) sc
1296 prettySe p bnd (PLet fc n ty v sc) =
1297 bracket p startPrec . group . align $
1298 kwd "let" <+> (group . align . hang 2 $ bindingOf n False <+> text "=" <$> prettySe startPrec bnd v) </>
1299 kwd "in" <+> (group . align . hang 2 $ prettySe startPrec ((n, False):bnd) sc)
1300 prettySe p bnd (PPi (Exp l s _) n ty sc)
1301 | n `elem` allNamesIn sc || ppopt_impl ppo || n `elem` docArgs =
1302 bracket p startPrec . group $
1303 enclose lparen rparen (group . align $ bindingOf n False <+> colon <+> prettySe startPrec bnd ty) <+>
1304 st <> text "->" <$> prettySe startPrec ((n, False):bnd) sc
1305 | otherwise =
1306 bracket p startPrec . group $
1307 group (prettySe (startPrec + 1) bnd ty <+> st) <> text "->" <$> group (prettySe startPrec ((n, False):bnd) sc)
1308 where
1309 st =
1310 case s of
1311 Static -> text "[static]" <> space
1312 _ -> empty
1313 prettySe p bnd (PPi (Imp l s _) n ty sc)
1314 | ppopt_impl ppo =
1315 bracket p startPrec $
1316 lbrace <> bindingOf n True <+> colon <+> prettySe startPrec bnd ty <> rbrace <+>
1317 st <> text "->" </> prettySe startPrec ((n, True):bnd) sc
1318 | otherwise = prettySe startPrec ((n, True):bnd) sc
1319 where
1320 st =
1321 case s of
1322 Static -> text "[static]" <> space
1323 _ -> empty
1324 prettySe p bnd (PPi (Constraint _ _) n ty sc) =
1325 bracket p startPrec $
1326 prettySe (startPrec + 1) bnd ty <+> text "=>" </> prettySe startPrec ((n, True):bnd) sc
1327 prettySe p bnd (PPi (TacImp _ _ s) n ty sc) =
1328 bracket p startPrec $
1329 lbrace <> kwd "tacimp" <+> pretty n <+> colon <+> prettySe startPrec bnd ty <>
1330 rbrace <+> text "->" </> prettySe startPrec ((n, True):bnd) sc
1331 prettySe p bnd (PApp _ (PRef _ f) args) -- normal names, no explicit args
1332 | UN nm <- basename f
1333 , not (ppopt_impl ppo) && null (getShowArgs args) =
1334 prettyName True (ppopt_impl ppo) bnd f
1335 prettySe p bnd (PAppBind _ (PRef _ f) [])
1336 | not (ppopt_impl ppo) = text "!" <> prettyName True (ppopt_impl ppo) bnd f
1337 prettySe p bnd (PApp _ (PRef _ op) args) -- infix operators
1338 | UN nm <- basename op
1339 , not (tnull nm) &&
1340 (not (ppopt_impl ppo)) && (not $ isAlpha (thead nm)) =
1341 case getShowArgs args of
1342 [] -> opName True
1343 [x] -> group (opName True <$> group (prettySe startPrec bnd (getTm x)))
1344 [l,r] -> let precedence = maybe (startPrec - 1) prec f
1345 in bracket p precedence $ inFix (getTm l) (getTm r)
1346 (l@(PExp _ _ _ _) : r@(PExp _ _ _ _) : rest) ->
1347 bracket p funcAppPrec $
1348 enclose lparen rparen (inFix (getTm l) (getTm r)) <+>
1349 align (group (vsep (map (prettyArgS bnd) rest)))
1350 as -> opName True <+> align (vsep (map (prettyArgS bnd) as))
1351 where opName isPrefix = prettyName isPrefix (ppopt_impl ppo) bnd op
1352 f = getFixity (opStr op)
1353 left = case f of
1354 Nothing -> funcAppPrec + 1
1355 Just (Infixl p') -> p'
1356 Just f' -> prec f' + 1
1357 right = case f of
1358 Nothing -> funcAppPrec + 1
1359 Just (Infixr p') -> p'
1360 Just f' -> prec f' + 1
1361 inFix l r = align . group $
1362 (prettySe left bnd l <+> opName False) <$>
1363 group (prettySe right bnd r)
1364 prettySe p bnd (PApp _ hd@(PRef fc f) [tm]) -- symbols, like 'foo
1365 | PConstant (Idris.Core.TT.Str str) <- getTm tm,
1366 f == sUN "Symbol_" = annotate (AnnType ("'" ++ str) ("The symbol " ++ str)) $
1367 char '\'' <> prettySe startPrec bnd (PRef fc (sUN str))
1368 prettySe p bnd (PApp _ f as) = -- Normal prefix applications
1369 let args = getShowArgs as
1370 fp = prettySe (startPrec + 1) bnd f
1371 shownArgs = if ppopt_impl ppo then as else args
1372 in
1373 bracket p funcAppPrec . group $
1374 if null shownArgs
1375 then fp
1376 else fp <+> align (vsep (map (prettyArgS bnd) shownArgs))
1377 prettySe p bnd (PCase _ scr cases) =
1378 align $ kwd "case" <+> prettySe startPrec bnd scr <+> kwd "of" <$>
1379 indent 2 (vsep (map ppcase cases))
1380 where
1381 ppcase (l, r) = let prettyCase = prettySe startPrec
1382 ([(n, False) | n <- vars l] ++ bnd)
1383 in nest nestingSize $
1384 prettyCase l <+> text "=>" <+> prettyCase r
1385 -- Warning: this is a bit of a hack. At this stage, we don't have the
1386 -- global context, so we can't determine which names are constructors,
1387 -- which are types, and which are pattern variables on the LHS of the
1388 -- case pattern. We use the heuristic that names without a namespace
1389 -- are patvars, because right now case blocks in PTerms are always
1390 -- delaborated from TT before being sent to the pretty-printer. If they
1391 -- start getting printed directly, THIS WILL BREAK.
1392 -- Potential solution: add a list of known patvars to the cases in
1393 -- PCase, and have the delaborator fill it out, kind of like the pun
1394 -- disambiguation on PDPair.
1395 vars tm = filter noNS (allNamesIn tm)
1396 noNS (NS _ _) = False
1397 noNS _ = True
1399 prettySe p bnd (PHidden tm) = text "." <> prettySe funcAppPrec bnd tm
1400 prettySe p bnd (PRefl _ _) = annName eqCon $ text "Refl"
1401 prettySe p bnd (PResolveTC _) = text "resolvetc"
1402 prettySe p bnd (PTrue _ IsType) = annName unitTy $ text "()"
1403 prettySe p bnd (PTrue _ IsTerm) = annName unitCon $ text "()"
1404 prettySe p bnd (PTrue _ TypeOrTerm) = text "()"
1405 prettySe p bnd (PEq _ lt rt l r)
1406 | ppopt_impl ppo =
1407 bracket p eqPrec $
1408 enclose lparen rparen eq <+>
1409 align (group (vsep (map (prettyArgS bnd)
1410 [PImp 0 False [] (sUN "A") lt,
1411 PImp 0 False [] (sUN "B") rt,
1412 PExp 0 [] (sUN "x") l,
1413 PExp 0 [] (sUN "y") r])))
1414 | otherwise =
1415 bracket p eqPrec . align . group $
1416 prettyTerm l <+> eq <$> group (prettyTerm r)
1417 where eq = annName eqTy (text "=")
1418 eqPrec = startPrec
1419 prettyTerm = prettySe (eqPrec + 1) bnd
1420 prettySe p bnd (PRewrite _ l r _) =
1421 bracket p startPrec $
1422 text "rewrite" <+> prettySe (startPrec + 1) bnd l <+> text "in" <+> prettySe startPrec bnd r
1423 prettySe p bnd (PTyped l r) =
1424 lparen <> prettySe startPrec bnd l <+> colon <+> prettySe startPrec bnd r <> rparen
1425 prettySe p bnd pair@(PPair _ pun _ _) -- flatten tuples to the right, like parser
1426 | Just elts <- pairElts pair = enclose (ann lparen) (ann rparen) .
1427 align . group . vsep . punctuate (ann comma) $
1428 map (prettySe startPrec bnd) elts
1429 where ann = case pun of
1430 TypeOrTerm -> id
1431 IsType -> annName pairTy
1432 IsTerm -> annName pairCon
1433 prettySe p bnd (PDPair _ pun l t r) =
1434 annotated lparen <>
1435 left <+>
1436 annotated (text "**") <+>
1437 prettySe startPrec (addBinding bnd) r <>
1438 annotated rparen
1439 where annotated = case pun of
1440 IsType -> annName sigmaTy
1441 IsTerm -> annName existsCon
1442 TypeOrTerm -> id
1443 (left, addBinding) = case (l, pun) of
1444 (PRef _ n, IsType) -> (bindingOf n False, ((n, False) :))
1445 _ -> (prettySe startPrec bnd l, id )
1446 prettySe p bnd (PAlternative a as) =
1447 lparen <> text "|" <> prettyAs <> text "|" <> rparen
1448 where
1449 prettyAs =
1450 foldr (\l -> \r -> l <+> text "," <+> r) empty $ map (prettySe startPrec bnd) as
1451 prettySe p bnd PType = annotate (AnnType "Type" "The type of types") $ text "Type"
1452 prettySe p bnd (PUniverse u) = annotate (AnnType (show u) "The type of unique types") $ text (show u)
1453 prettySe p bnd (PConstant c) = annotate (AnnConst c) (text (show c))
1454 -- XXX: add pretty for tactics
1455 prettySe p bnd (PProof ts) =
1456 text "proof" <+> lbrace <> nest nestingSize (text . show $ ts) <> rbrace
1457 prettySe p bnd (PTactics ts) =
1458 text "tactics" <+> lbrace <> nest nestingSize (text . show $ ts) <> rbrace
1459 prettySe p bnd (PMetavar n) = text "?" <> pretty n
1460 prettySe p bnd (PReturn f) = kwd "return"
1461 prettySe p bnd PImpossible = kwd "impossible"
1462 prettySe p bnd Placeholder = text "_"
1463 prettySe p bnd (PDoBlock _) = text "do block pretty not implemented"
1464 prettySe p bnd (PCoerced t) = prettySe p bnd t
1465 prettySe p bnd (PElabError s) = pretty s
1466 -- Quasiquote pprinting ignores bound vars
1467 prettySe p bnd (PQuasiquote t Nothing) = text "`(" <> prettySe p [] t <> text ")"
1468 prettySe p bnd (PQuasiquote t (Just g)) = text "`(" <> prettySe p [] t <+> colon <+> prettySe p [] g <> text ")"
1469 prettySe p bnd (PUnquote t) = text "~" <> prettySe p bnd t
1471 prettySe p bnd _ = text "missing pretty-printer for term"
1473 prettyArgS bnd (PImp _ _ _ n tm) = prettyArgSi bnd (n, tm)
1474 prettyArgS bnd (PExp _ _ _ tm) = prettyArgSe bnd tm
1475 prettyArgS bnd (PConstraint _ _ _ tm) = prettyArgSc bnd tm
1476 prettyArgS bnd (PTacImplicit _ _ n _ tm) = prettyArgSti bnd (n, tm)
1478 prettyArgSe bnd arg = prettySe (funcAppPrec + 1) bnd arg
1479 prettyArgSi bnd (n, val) = lbrace <> pretty n <+> text "=" <+> prettySe startPrec bnd val <> rbrace
1480 prettyArgSc bnd val = lbrace <> lbrace <> prettySe startPrec bnd val <> rbrace <> rbrace
1481 prettyArgSti bnd (n, val) = lbrace <> kwd "auto" <+> pretty n <+> text "=" <+> prettySe startPrec bnd val <> rbrace
1483 annName :: Name -> Doc OutputAnnotation -> Doc OutputAnnotation
1484 annName n = annotate (AnnName n Nothing Nothing Nothing)
1486 opStr :: Name -> String
1487 opStr (NS n _) = opStr n
1488 opStr (UN n) = T.unpack n
1490 basename :: Name -> Name
1491 basename (NS n _) = basename n
1492 basename n = n
1494 slist' p bnd (PApp _ (PRef _ nil) _)
1495 | not (ppopt_impl ppo) && nsroot nil == sUN "Nil" = Just []
1496 slist' p bnd (PRef _ nil)
1497 | not (ppopt_impl ppo) && nsroot nil == sUN "Nil" = Just []
1498 slist' p bnd (PApp _ (PRef _ cons) args)
1499 | nsroot cons == sUN "::",
1500 (PExp {getTm=tl}):(PExp {getTm=hd}):imps <- reverse args,
1501 all isImp imps,
1502 Just tl' <- slist' p bnd tl
1503 = Just (hd:tl')
1504 where
1505 isImp (PImp {}) = True
1506 isImp _ = False
1507 slist' _ _ tm = Nothing
1509 slist p bnd e | Just es <- slist' p bnd e = Just $
1510 case es of [] -> annotate (AnnData "" "") $ text "[]"
1511 [x] -> enclose left right . group $
1512 prettySe p bnd x
1513 xs -> (enclose left right .
1514 align . group . vsep .
1515 punctuate comma .
1516 map (prettySe p bnd)) xs
1517 where left = (annotate (AnnData "" "") (text "["))
1518 right = (annotate (AnnData "" "") (text "]"))
1519 comma = (annotate (AnnData "" "") (text ","))
1520 slist _ _ _ = Nothing
1522 pairElts :: PTerm -> Maybe [PTerm]
1523 pairElts (PPair _ _ x y) | Just elts <- pairElts y = Just (x:elts)
1524 | otherwise = Just [x, y]
1525 pairElts _ = Nothing
1527 natns = "Prelude.Nat."
1529 snat p (PRef _ z)
1530 | show z == (natns++"Z") || show z == "Z" = Just 0
1531 snat p (PApp _ s [PExp {getTm=n}])
1532 | show s == (natns++"S") || show s == "S",
1533 Just n' <- snat p n
1534 = Just $ 1 + n'
1535 snat _ _ = Nothing
1537 bracket outer inner doc
1538 | outer > inner = lparen <> doc <> rparen
1539 | otherwise = doc
1541 kwd = annotate AnnKeyword . text
1543 fixities :: M.Map String Fixity
1544 fixities = M.fromList [(s, f) | (Fix f s) <- infixes]
1546 getFixity :: String -> Maybe Fixity
1547 getFixity = flip M.lookup fixities
1549-- | Pretty-printer helper for the binding site of a name
1550bindingOf :: Name -- ^^ the bound name
1551 -> Bool -- ^^ whether the name is implicit
1552 -> Doc OutputAnnotation
1553bindingOf n imp = annotate (AnnBoundName n imp) (text (show n))
1555-- | Pretty-printer helper for names that attaches the correct annotations
1556prettyName
1557 :: Bool -- ^^ whether the name should be parenthesised if it is an infix operator
1558 -> Bool -- ^^ whether to show namespaces
1559 -> [(Name, Bool)] -- ^^ the current bound variables and whether they are implicit
1560 -> Name -- ^^ the name to pprint
1561 -> Doc OutputAnnotation
1562prettyName infixParen showNS bnd n
1563 | (MN _ s) <- n, isPrefixOf "_" $ T.unpack s = text "_"
1564 | (UN n') <- n, isPrefixOf "_" $ T.unpack n' = text "_"
1565 | Just imp <- lookup n bnd = annotate (AnnBoundName n imp) fullName
1566 | otherwise = annotate (AnnName n Nothing Nothing Nothing) fullName
1567 where fullName = text nameSpace <> parenthesise (text (baseName n))
1568 baseName (UN n) = T.unpack n
1569 baseName (NS n ns) = baseName n
1570 baseName (MN i s) = T.unpack s
1571 baseName other = show other
1572 nameSpace = case n of
1573 (NS n' ns) -> if showNS then (concatMap (++ ".") . map T.unpack . reverse) ns else ""
1574 _ -> ""
1575 isInfix = case baseName n of
1576 "" -> False
1577 (c : _) -> not (isAlpha c)
1578 parenthesise = if isInfix && infixParen then enclose lparen rparen else id
1581showCImp :: PPOption -> PClause -> Doc OutputAnnotation
1582showCImp ppo (PClause _ n l ws r w)
1583 = prettyImp ppo l <+> showWs ws <+> text "=" <+> prettyImp ppo r
1584 <+> text "where" <+> text (show w)
1585 where
1586 showWs [] = empty
1587 showWs (x : xs) = text "|" <+> prettyImp ppo x <+> showWs xs
1588showCImp ppo (PWith _ n l ws r w)
1589 = prettyImp ppo l <+> showWs ws <+> text "with" <+> prettyImp ppo r
1590 <+> braces (text (show w))
1591 where
1592 showWs [] = empty
1593 showWs (x : xs) = text "|" <+> prettyImp ppo x <+> showWs xs
1596showDImp :: PPOption -> PData -> Doc OutputAnnotation
1597showDImp ppo (PDatadecl n ty cons)
1598 = text "data" <+> text (show n) <+> colon <+> prettyImp ppo ty <+> text "where" <$>
1599 (indent 2 $ vsep (map (\ (_, _, n, t, _, _) -> pipe <+> prettyName True False [] n <+> colon <+> prettyImp ppo t) cons))
1601showDecls :: PPOption -> [PDecl] -> Doc OutputAnnotation
1602showDecls o ds = vsep (map (showDeclImp o) ds)
1604showDeclImp _ (PFix _ f ops) = text (show f) <+> cat (punctuate (text ",") (map text ops))
1605showDeclImp o (PTy _ _ _ _ _ n t) = text "tydecl" <+> text (showCG n) <+> colon <+> prettyImp o t
1606showDeclImp o (PClauses _ _ n cs) = text "pat" <+> text (showCG n) <+> text "\t" <+>
1607 indent 2 (vsep (map (showCImp o) cs))
1608showDeclImp o (PData _ _ _ _ _ d) = showDImp o { ppopt_impl = True } d
1609showDeclImp o (PParams _ ns ps) = text "params" <+> braces (text (show ns) <> line <> showDecls o ps <> line)
1610showDeclImp o (PNamespace n ps) = text "namespace" <+> text n <> braces (line <> showDecls o ps <> line)
1611showDeclImp _ (PSyntax _ syn) = text "syntax" <+> text (show syn)
1612showDeclImp o (PClass _ _ _ cs n ps _ ds)
1613 = text "class" <+> text (show cs) <+> text (show n) <+> text (show ps) <> line <> showDecls o ds
1614showDeclImp o (PInstance _ _ cs n _ t _ ds)
1615 = text "instance" <+> text (show cs) <+> text (show n) <+> prettyImp o t <> line <> showDecls o ds
1616showDeclImp _ _ = text "..."
1617-- showDeclImp (PImport o) = "import " ++ o
1619instance Show (Doc OutputAnnotation) where
1620 show = flip (displayS . renderCompact) ""
1622getImps :: [PArg] -> [(Name, PTerm)]
1623getImps [] = []
1624getImps (PImp _ _ _ n tm : xs) = (n, tm) : getImps xs
1625getImps (_ : xs) = getImps xs
1627getExps :: [PArg] -> [PTerm]
1628getExps [] = []
1629getExps (PExp _ _ _ tm : xs) = tm : getExps xs
1630getExps (_ : xs) = getExps xs
1632getShowArgs :: [PArg] -> [PArg]
1633getShowArgs [] = []
1634getShowArgs (e@(PExp _ _ _ tm) : xs) = e : getShowArgs xs
1635getShowArgs (e : xs) | AlwaysShow `elem` argopts e = e : getShowArgs xs
1636getShowArgs (_ : xs) = getShowArgs xs
1638getConsts :: [PArg] -> [PTerm]
1639getConsts [] = []
1640getConsts (PConstraint _ _ _ tm : xs) = tm : getConsts xs
1641getConsts (_ : xs) = getConsts xs
1643getAll :: [PArg] -> [PTerm]
1644getAll = map getTm
1647-- | Show Idris name
1648showName :: Maybe IState -- ^^ the Idris state, for information about names and colours
1649 -> [(Name, Bool)] -- ^^ the bound variables and whether they're implicit
1650 -> PPOption -- ^^ pretty printing options
1651 -> Bool -- ^^ whether to colourise
1652 -> Name -- ^^ the term to show
1653 -> String
1654showName ist bnd ppo colour n = case ist of
1655 Just i -> if colour then colourise n (idris_colourTheme i) else showbasic n
1656 Nothing -> showbasic n
1657 where name = if ppopt_impl ppo then show n else showbasic n
1658 showbasic n@(UN _) = showCG n
1659 showbasic (MN i s) = str s
1660 showbasic (NS n s) = showSep "." (map str (reverse s)) ++ "." ++ showbasic n
1661 showbasic (SN s) = show s
1662 fst3 (x, _, _) = x
1663 colourise n t = let ctxt' = fmap tt_ctxt ist in
1664 case ctxt' of
1665 Nothing -> name
1666 Just ctxt | Just impl <- lookup n bnd -> if impl then colouriseImplicit t name
1667 else colouriseBound t name
1668 | isDConName n ctxt -> colouriseData t name
1669 | isFnName n ctxt -> colouriseFun t name
1670 | isTConName n ctxt -> colouriseType t name
1671 -- The assumption is that if a name is not bound and does not exist in the
1672 -- global context, then we're somewhere in which implicit info has been lost
1673 -- (like error messages). Thus, unknown vars are colourised as implicits.
1674 | otherwise -> colouriseImplicit t name
1676showTm :: IState -- ^^ the Idris state, for information about identifiers and colours
1677 -> PTerm -- ^^ the term to show
1678 -> String
1679showTm ist = displayDecorated (consoleDecorate ist) .
1680 renderPretty 0.8 100000 .
1681 prettyImp (ppOptionIst ist)
1683-- | Show a term with implicits, no colours
1684showTmImpls :: PTerm -> String
1685showTmImpls = flip (displayS . renderCompact . prettyImp verbosePPOption) ""
1689instance Sized PTerm where
1690 size (PQuote rawTerm) = size rawTerm
1691 size (PRef fc name) = size name
1692 size (PLam fc name ty bdy) = 1 + size ty + size bdy
1693 size (PPi plicity name ty bdy) = 1 + size ty + size bdy
1694 size (PLet fc name ty def bdy) = 1 + size ty + size def + size bdy
1695 size (PTyped trm ty) = 1 + size trm + size ty
1696 size (PApp fc name args) = 1 + size args
1697 size (PAppBind fc name args) = 1 + size args
1698 size (PCase fc trm bdy) = 1 + size trm + size bdy
1699 size (PTrue fc _) = 1
1700 size (PRefl fc _) = 1
1701 size (PResolveTC fc) = 1
1702 size (PEq fc _ _ left right) = 1 + size left + size right
1703 size (PRewrite fc left right _) = 1 + size left + size right
1704 size (PPair fc _ left right) = 1 + size left + size right
1705 size (PDPair fs _ left ty right) = 1 + size left + size ty + size right
1706 size (PAlternative a alts) = 1 + size alts
1707 size (PHidden hidden) = size hidden
1708 size (PUnifyLog tm) = size tm
1709 size (PDisamb _ tm) = size tm
1710 size (PNoImplicits tm) = size tm
1711 size PType = 1
1712 size (PUniverse _) = 1
1713 size (PConstant const) = 1 + size const
1714 size Placeholder = 1
1715 size (PDoBlock dos) = 1 + size dos
1716 size (PIdiom fc term) = 1 + size term
1717 size (PReturn fc) = 1
1718 size (PMetavar name) = 1
1719 size (PProof tactics) = size tactics
1720 size (PElabError err) = size err
1721 size PImpossible = 1
1722 size _ = 0
1724getPArity :: PTerm -> Int
1725getPArity (PPi _ _ _ sc) = 1 + getPArity sc
1726getPArity _ = 0
1728-- Return all names, free or globally bound, in the given term.
1730allNamesIn :: PTerm -> [Name]
1731allNamesIn tm = nub $ ni [] tm
1732 where -- TODO THINK added niTacImp, but is it right?
1733 ni env (PRef _ n)
1734 | not (n `elem` env) = [n]
1735 ni env (PPatvar _ n) = [n]
1736 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
1737 ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
1738 ni env (PCase _ c os) = ni env c ++ concatMap (ni env) (map snd os)
1739 ni env (PLam fc n ty sc) = ni env ty ++ ni (n:env) sc
1740 ni env (PPi p n ty sc) = niTacImp env p ++ ni env ty ++ ni (n:env) sc
1741 ni env (PHidden tm) = ni env tm
1742 ni env (PEq _ _ _ l r) = ni env l ++ ni env r
1743 ni env (PRewrite _ l r _) = ni env l ++ ni env r
1744 ni env (PTyped l r) = ni env l ++ ni env r
1745 ni env (PPair _ _ l r) = ni env l ++ ni env r
1746 ni env (PDPair _ _ (PRef _ n) t r) = ni env t ++ ni (n:env) r
1747 ni env (PDPair _ _ l t r) = ni env l ++ ni env t ++ ni env r
1748 ni env (PAlternative a ls) = concatMap (ni env) ls
1749 ni env (PUnifyLog tm) = ni env tm
1750 ni env (PDisamb _ tm) = ni env tm
1751 ni env (PNoImplicits tm) = ni env tm
1752 ni env _ = []
1754 niTacImp env (TacImp _ _ scr) = ni env scr
1755 niTacImp _ _ = []
1757-- Return all names defined in binders in the given term
1758boundNamesIn :: PTerm -> [Name]
1759boundNamesIn tm = nub $ ni tm
1760 where -- TODO THINK Added niTacImp, but is it right?
1761 ni (PApp _ f as) = ni f ++ concatMap (ni) (map getTm as)
1762 ni (PAppBind _ f as) = ni f ++ concatMap (ni) (map getTm as)
1763 ni (PCase _ c os) = ni c ++ concatMap (ni) (map snd os)
1764 ni (PLam fc n ty sc) = n : (ni ty ++ ni sc)
1765 ni (PLet fc n ty val sc) = n : (ni ty ++ ni val ++ ni sc)
1766 ni (PPi p n ty sc) = niTacImp p ++ (n : (ni ty ++ ni sc))
1767 ni (PEq _ _ _ l r) = ni l ++ ni r
1768 ni (PRewrite _ l r _) = ni l ++ ni r
1769 ni (PTyped l r) = ni l ++ ni r
1770 ni (PPair _ _ l r) = ni l ++ ni r
1771 ni (PDPair _ _ (PRef _ n) t r) = ni t ++ ni r
1772 ni (PDPair _ _ l t r) = ni l ++ ni t ++ ni r
1773 ni (PAlternative a as) = concatMap (ni) as
1774 ni (PHidden tm) = ni tm
1775 ni (PUnifyLog tm) = ni tm
1776 ni (PDisamb _ tm) = ni tm
1777 ni (PNoImplicits tm) = ni tm
1778 ni _ = []
1780 niTacImp (TacImp _ _ scr) = ni scr
1781 niTacImp _ = []
1783-- Return names which are valid implicits in the given term (type).
1784implicitNamesIn :: [Name] -> IState -> PTerm -> [Name]
1785implicitNamesIn uvars ist tm = nub $ ni [] tm
1786 where
1787 ni env (PRef _ n)
1788 | not (n `elem` env)
1789 = case lookupTy n (tt_ctxt ist) of
1790 [] -> [n]
1791 _ -> if n `elem` uvars then [n] else []
1792 ni env (PApp _ f@(PRef _ n) as)
1793 | n `elem` uvars = ni env f ++ concatMap (ni env) (map getTm as)
1794 | otherwise = concatMap (ni env) (map getTm as)
1795 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
1796 ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
1797 ni env (PCase _ c os) = ni env c ++
1798 -- names in 'os', not counting the names bound in the cases
1799 (nub (concatMap (ni env) (map snd os))
1800 \\ nub (concatMap (ni env) (map fst os)))
1801 ni env (PLam fc n ty sc) = ni env ty ++ ni (n:env) sc
1802 ni env (PPi p n ty sc) = ni env ty ++ ni (n:env) sc
1803 ni env (PEq _ _ _ l r) = ni env l ++ ni env r
1804 ni env (PRewrite _ l r _) = ni env l ++ ni env r
1805 ni env (PTyped l r) = ni env l ++ ni env r
1806 ni env (PPair _ _ l r) = ni env l ++ ni env r
1807 ni env (PDPair _ _ (PRef _ n) t r) = ni env t ++ ni (n:env) r
1808 ni env (PDPair _ _ l t r) = ni env l ++ ni env t ++ ni env r
1809 ni env (PAlternative a as) = concatMap (ni env) as
1810 ni env (PHidden tm) = ni env tm
1811 ni env (PUnifyLog tm) = ni env tm
1812 ni env (PDisamb _ tm) = ni env tm
1813 ni env (PNoImplicits tm) = ni env tm
1814 ni env _ = []
1816-- Return names which are free in the given term.
1817namesIn :: [(Name, PTerm)] -> IState -> PTerm -> [Name]
1818namesIn uvars ist tm = nub $ ni [] tm
1819 where
1820 ni env (PRef _ n)
1821 | not (n `elem` env)
1822 = case lookupTy n (tt_ctxt ist) of
1823 [] -> [n]
1824 _ -> if n `elem` (map fst uvars) then [n] else []
1825 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
1826 ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
1827 ni env (PCase _ c os) = ni env c ++
1828 -- names in 'os', not counting the names bound in the cases
1829 (nub (concatMap (ni env) (map snd os))
1830 \\ nub (concatMap (ni env) (map fst os)))
1831 ni env (PLam fc n ty sc) = ni env ty ++ ni (n:env) sc
1832 ni env (PPi p n ty sc) = niTacImp env p ++ ni env ty ++ ni (n:env) sc
1833 ni env (PEq _ _ _ l r) = ni env l ++ ni env r
1834 ni env (PRewrite _ l r _) = ni env l ++ ni env r
1835 ni env (PTyped l r) = ni env l ++ ni env r
1836 ni env (PPair _ _ l r) = ni env l ++ ni env r
1837 ni env (PDPair _ _ (PRef _ n) t r) = ni env t ++ ni (n:env) r
1838 ni env (PDPair _ _ l t r) = ni env l ++ ni env t ++ ni env r
1839 ni env (PAlternative a as) = concatMap (ni env) as
1840 ni env (PHidden tm) = ni env tm
1841 ni env (PUnifyLog tm) = ni env tm
1842 ni env (PDisamb _ tm) = ni env tm
1843 ni env (PNoImplicits tm) = ni env tm
1844 ni env _ = []
1846 niTacImp env (TacImp _ _ scr) = ni env scr
1847 niTacImp _ _ = []
1849-- Return which of the given names are used in the given term.
1851usedNamesIn :: [Name] -> IState -> PTerm -> [Name]
1852usedNamesIn vars ist tm = nub $ ni [] tm
1853 where -- TODO THINK added niTacImp, but is it right?
1854 ni env (PRef _ n)
1855 | n `elem` vars && not (n `elem` env)
1856 = case lookupDefExact n (tt_ctxt ist) of
1857 Nothing -> [n]
1858 _ -> []
1859 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
1860 ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
1861 ni env (PCase _ c os) = ni env c ++ concatMap (ni env) (map snd os)
1862 ni env (PLam fc n ty sc) = ni env ty ++ ni (n:env) sc
1863 ni env (PPi p n ty sc) = niTacImp env p ++ ni env ty ++ ni (n:env) sc
1864 ni env (PEq _ _ _ l r) = ni env l ++ ni env r
1865 ni env (PRewrite _ l r _) = ni env l ++ ni env r
1866 ni env (PTyped l r) = ni env l ++ ni env r
1867 ni env (PPair _ _ l r) = ni env l ++ ni env r
1868 ni env (PDPair _ _ (PRef _ n) t r) = ni env t ++ ni (n:env) r
1869 ni env (PDPair _ _ l t r) = ni env l ++ ni env t ++ ni env r
1870 ni env (PAlternative a as) = concatMap (ni env) as
1871 ni env (PHidden tm) = ni env tm
1872 ni env (PUnifyLog tm) = ni env tm
1873 ni env (PDisamb _ tm) = ni env tm
1874 ni env (PNoImplicits tm) = ni env tm
1875 ni env _ = []
1877 niTacImp env (TacImp _ _ scr) = ni env scr
1878 niTacImp _ _ = []
1880-- Return the list of inaccessible (= dotted) positions for a name.
1881getErasureInfo :: IState -> Name -> [Int]
1882getErasureInfo ist n =
1883 case lookupCtxtExact n (idris_optimisation ist) of
1884 Just (Optimise inacc detagg) -> map fst inacc
1885 Nothing -> []