git.iko.soy/Idris-dev
on 348ddce help sign in
Idris-dev/src/Idris/AbsSyntaxTree.hs
1889 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 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
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 | WarnOnly
417 | Pkg String
418 | BCAsm String
419 | DumpDefun String
420 | DumpCases String
421 | UseCodegen Codegen
422 | OutputTy OutputType
423 | Extension LanguageExt
424 | InterpretScript String
425 | EvalExpr String
426 | TargetTriple String
427 | TargetCPU String
428 | OptLevel Int
429 | AddOpt Optimisation
430 | RemoveOpt Optimisation
431 | Client String
432 | ShowOrigErr
433 | AutoWidth -- ^ Automatically adjust terminal width
434 | AutoSolve -- ^ Automatically issue "solve" tactic in interactive prover
435 deriving (Show, Eq)
437-- Parsed declarations
439data Fixity = Infixl { prec :: Int }
440 | Infixr { prec :: Int }
441 | InfixN { prec :: Int }
442 | PrefixN { prec :: Int }
443 deriving Eq
444{-!
445deriving instance Binary Fixity
446deriving instance NFData Fixity
447!-}
449instance Show Fixity where
450 show (Infixl i) = "infixl " ++ show i
451 show (Infixr i) = "infixr " ++ show i
452 show (InfixN i) = "infix " ++ show i
453 show (PrefixN i) = "prefix " ++ show i
455data FixDecl = Fix Fixity String
456 deriving Eq
458instance Show FixDecl where
459 show (Fix f s) = show f ++ " " ++ s
461{-!
462deriving instance Binary FixDecl
463deriving instance NFData FixDecl
464!-}
466instance Ord FixDecl where
467 compare (Fix x _) (Fix y _) = compare (prec x) (prec y)
470data Static = Static | Dynamic
471 deriving (Show, Eq)
472{-!
473deriving instance Binary Static
474deriving instance NFData Static
475!-}
477-- Mark bindings with their explicitness, and laziness
478data Plicity = Imp { pargopts :: [ArgOpt],
479 pstatic :: Static,
480 pparam :: Bool }
481 | Exp { pargopts :: [ArgOpt],
482 pstatic :: Static,
483 pparam :: Bool } -- this is a param (rather than index)
484 | Constraint { pargopts :: [ArgOpt],
485 pstatic :: Static }
486 | TacImp { pargopts :: [ArgOpt],
487 pstatic :: Static,
488 pscript :: PTerm }
489 deriving (Show, Eq)
491{-!
492deriving instance Binary Plicity
493deriving instance NFData Plicity
494!-}
496impl = Imp [] Dynamic False
497expl = Exp [] Dynamic False
498expl_param = Exp [] Dynamic True
499constraint = Constraint [] Static
500tacimpl t = TacImp [] Dynamic t
502data FnOpt = Inlinable -- always evaluate when simplifying
503 | TotalFn | PartialFn | CoveringFn
504 | Coinductive | AssertTotal
505 | Dictionary -- type class dictionary, eval only when
506 -- a function argument, and further evaluation resutls
507 | Implicit -- implicit coercion
508 | NoImplicit -- do not apply implicit coercions
509 | CExport String -- export, with a C name
510 | ErrorHandler -- ^^ an error handler for use with the ErrorReflection extension
511 | ErrorReverse -- ^^ attempt to reverse normalise before showing in error
512 | Reflection -- a reflecting function, compile-time only
513 | Specialise [(Name, Maybe Int)] -- specialise it, freeze these names
514 | Constructor -- Data constructor type
515 deriving (Show, Eq)
516{-!
517deriving instance Binary FnOpt
518deriving instance NFData FnOpt
519!-}
521type FnOpts = [FnOpt]
523inlinable :: FnOpts -> Bool
524inlinable = elem Inlinable
526dictionary :: FnOpts -> Bool
527dictionary = elem Dictionary
530-- | Data declaration options
531data DataOpt = Codata -- ^ Set if the the data-type is coinductive
532 | DefaultEliminator -- ^ Set if an eliminator should be generated for data type
533 | DefaultCaseFun -- ^ Set if a case function should be generated for data type
534 | DataErrRev
535 deriving (Show, Eq)
537type DataOpts = [DataOpt]
539-- | Type provider - what to provide
540data ProvideWhat' t = ProvTerm t t -- ^ the first is the goal type, the second is the term
541 | ProvPostulate t -- ^ goal type must be Type, so only term
542 deriving (Show, Eq, Functor)
544type ProvideWhat = ProvideWhat' PTerm
546-- | Top-level declarations such as compiler directives, definitions,
547-- datatypes and typeclasses.
548data PDecl' t
549 = PFix FC Fixity [String] -- ^ Fixity declaration
550 | PTy (Docstring (Either Err PTerm)) [(Name, Docstring (Either Err PTerm))] SyntaxInfo FC FnOpts Name t -- ^ Type declaration
551 | PPostulate (Docstring (Either Err PTerm)) SyntaxInfo FC FnOpts Name t -- ^ Postulate
552 | PClauses FC FnOpts Name [PClause' t] -- ^ Pattern clause
553 | PCAF FC Name t -- ^ Top level constant
554 | PData (Docstring (Either Err PTerm)) [(Name, Docstring (Either Err PTerm))] SyntaxInfo FC DataOpts (PData' t) -- ^ Data declaration.
555 | PParams FC [(Name, t)] [PDecl' t] -- ^ Params block
556 | PNamespace String [PDecl' t] -- ^ New namespace
557 | PRecord (Docstring (Either Err PTerm)) SyntaxInfo FC Name t DataOpts (Docstring (Either Err PTerm)) Name t -- ^ Record declaration
558 | PClass (Docstring (Either Err PTerm)) SyntaxInfo FC
559 [t] -- constraints
560 Name
561 [(Name, t)] -- parameters
562 [(Name, Docstring (Either Err PTerm))] -- parameter docstrings
563 [PDecl' t] -- declarations
564 -- ^ Type class: arguments are documentation, syntax info, source location, constraints,
565 -- class name, parameters, method declarations
566 | PInstance SyntaxInfo FC [t] -- constraints
567 Name -- class
568 [t] -- parameters
569 t -- full instance type
570 (Maybe Name) -- explicit name
571 [PDecl' t]
572 -- ^ Instance declaration: arguments are syntax info, source location, constraints,
573 -- class name, parameters, full instance type, optional explicit name, and definitions
574 | PDSL Name (DSL' t) -- ^ DSL declaration
575 | PSyntax FC Syntax -- ^ Syntax definition
576 | PMutual FC [PDecl' t] -- ^ Mutual block
577 | PDirective (Idris ()) -- ^ Compiler directive. The parser inserts the corresponding action in the Idris monad.
578 | PProvider SyntaxInfo FC (ProvideWhat' t) Name -- ^ Type provider. The first t is the type, the second is the term
579 | PTransform FC Bool t t -- ^ Source-to-source transformation rule. If
580 -- bool is True, lhs and rhs must be convertible
581 deriving Functor
582{-!
583deriving instance Binary PDecl'
584deriving instance NFData PDecl'
585!-}
587-- For elaborator state
588data EState = EState {
589 case_decls :: [PDecl],
590 delayed_elab :: [Elab' EState ()]
591 }
593initEState = EState [] []
595type ElabD a = Elab' EState a
597-- | One clause of a top-level definition. Term arguments to constructors are:
598--
599-- 1. The whole application (missing for PClauseR and PWithR because they're within a "with" clause)
600--
601-- 2. The list of extra 'with' patterns
602--
603-- 3. The right-hand side
604--
605-- 4. The where block (PDecl' t)
607data PClause' t = PClause FC Name t [t] t [PDecl' t] -- ^ A normal top-level definition.
608 | PWith FC Name t [t] t [PDecl' t]
609 | PClauseR FC [t] t [PDecl' t]
610 | PWithR FC [t] t [PDecl' t]
611 deriving Functor
612{-!
613deriving instance Binary PClause'
614deriving instance NFData PClause'
615!-}
617-- | Data declaration
618data PData' t = PDatadecl { d_name :: Name, -- ^ The name of the datatype
619 d_tcon :: t, -- ^ Type constructor
620 d_cons :: [(Docstring (Either Err PTerm), [(Name, Docstring (Either Err PTerm))], Name, t, FC, [Name])] -- ^ Constructors
621 }
622 -- ^ Data declaration
623 | PLaterdecl { d_name :: Name, d_tcon :: t }
624 -- ^ "Placeholder" for data whose constructors are defined later
625 deriving Functor
626{-!
627deriving instance Binary PData'
628deriving instance NFData PData'
629!-}
631-- Handy to get a free function for applying PTerm -> PTerm functions
632-- across a program, by deriving Functor
634type PDecl = PDecl' PTerm
635type PData = PData' PTerm
636type PClause = PClause' PTerm
638-- get all the names declared in a decl
640declared :: PDecl -> [Name]
641declared (PFix _ _ _) = []
642declared (PTy _ _ _ _ _ n t) = [n]
643declared (PPostulate _ _ _ _ n t) = [n]
644declared (PClauses _ _ n _) = [] -- not a declaration
645declared (PCAF _ n _) = [n]
646declared (PData _ _ _ _ _ (PDatadecl n _ ts)) = n : map fstt ts
647 where fstt (_, _, a, _, _, _) = a
648declared (PData _ _ _ _ _ (PLaterdecl n _)) = [n]
649declared (PParams _ _ ds) = concatMap declared ds
650declared (PNamespace _ ds) = concatMap declared ds
651declared (PRecord _ _ _ n _ _ _ c _) = [n, c]
652declared (PClass _ _ _ _ n _ _ ms) = n : concatMap declared ms
653declared (PInstance _ _ _ _ _ _ _ _) = []
654declared (PDSL n _) = [n]
655declared (PSyntax _ _) = []
656declared (PMutual _ ds) = concatMap declared ds
657declared (PDirective _) = []
659-- get the names declared, not counting nested parameter blocks
660tldeclared :: PDecl -> [Name]
661tldeclared (PFix _ _ _) = []
662tldeclared (PTy _ _ _ _ _ n t) = [n]
663tldeclared (PPostulate _ _ _ _ n t) = [n]
664tldeclared (PClauses _ _ n _) = [] -- not a declaration
665tldeclared (PRecord _ _ _ n _ _ _ c _) = [n, c]
666tldeclared (PData _ _ _ _ _ (PDatadecl n _ ts)) = n : map fstt ts
667 where fstt (_, _, a, _, _, _) = a
668tldeclared (PParams _ _ ds) = []
669tldeclared (PMutual _ ds) = concatMap tldeclared ds
670tldeclared (PNamespace _ ds) = concatMap tldeclared ds
671tldeclared (PClass _ _ _ _ n _ _ ms) = concatMap tldeclared ms
672tldeclared (PInstance _ _ _ _ _ _ _ _) = []
673tldeclared _ = []
675defined :: PDecl -> [Name]
676defined (PFix _ _ _) = []
677defined (PTy _ _ _ _ _ n t) = []
678defined (PPostulate _ _ _ _ n t) = []
679defined (PClauses _ _ n _) = [n] -- not a declaration
680defined (PCAF _ n _) = [n]
681defined (PData _ _ _ _ _ (PDatadecl n _ ts)) = n : map fstt ts
682 where fstt (_, _, a, _, _, _) = a
683defined (PData _ _ _ _ _ (PLaterdecl n _)) = []
684defined (PParams _ _ ds) = concatMap defined ds
685defined (PNamespace _ ds) = concatMap defined ds
686defined (PRecord _ _ _ n _ _ _ c _) = [n, c]
687defined (PClass _ _ _ _ n _ _ ms) = n : concatMap defined ms
688defined (PInstance _ _ _ _ _ _ _ _) = []
689defined (PDSL n _) = [n]
690defined (PSyntax _ _) = []
691defined (PMutual _ ds) = concatMap defined ds
692defined (PDirective _) = []
693--defined _ = []
695updateN :: [(Name, Name)] -> Name -> Name
696updateN ns n | Just n' <- lookup n ns = n'
697updateN _ n = n
699updateNs :: [(Name, Name)] -> PTerm -> PTerm
700updateNs [] t = t
701updateNs ns t = mapPT updateRef t
702 where updateRef (PRef fc f) = PRef fc (updateN ns f)
703 updateRef t = t
705-- updateDNs :: [(Name, Name)] -> PDecl -> PDecl
706-- updateDNs [] t = t
707-- updateDNs ns (PTy s f n t) | Just n' <- lookup n ns = PTy s f n' t
708-- updateDNs ns (PClauses f n c) | Just n' <- lookup n ns = PClauses f n' (map updateCNs c)
709-- where updateCNs ns (PClause n l ts r ds)
710-- = PClause (updateN ns n) (fmap (updateNs ns) l)
711-- (map (fmap (updateNs ns)) ts)
712-- (fmap (updateNs ns) r)
713-- (map (updateDNs ns) ds)
714-- updateDNs ns c = c
716data PunInfo = IsType | IsTerm | TypeOrTerm deriving (Eq, Show)
718-- | High level language terms
719data PTerm = PQuote Raw -- ^ Inclusion of a core term into the high-level language
720 | PRef FC Name -- ^ A reference to a variable
721 | PInferRef FC Name -- ^ A name to be defined later
722 | PPatvar FC Name -- ^ A pattern variable
723 | PLam FC Name PTerm PTerm -- ^ A lambda abstraction
724 | PPi Plicity Name PTerm PTerm -- ^ (n : t1) -> t2
725 | PLet FC Name PTerm PTerm PTerm -- ^ A let binding
726 | PTyped PTerm PTerm -- ^ Term with explicit type
727 | PApp FC PTerm [PArg] -- ^ e.g. IO (), List Char, length x
728 | PAppBind FC PTerm [PArg] -- ^ implicitly bound application
729 | PMatchApp FC Name -- ^ Make an application by type matching
730 | PCase FC PTerm [(PTerm, PTerm)] -- ^ A case expression. Args are source location, scrutinee, and a list of pattern/RHS pairs
731 | PTrue FC PunInfo -- ^ Unit type..?
732 | PRefl FC PTerm -- ^ The canonical proof of the equality type
733 | PResolveTC FC -- ^ Solve this dictionary by type class resolution
734 | PEq FC PTerm PTerm PTerm PTerm -- ^ Heterogeneous equality type: A = B
735 | PRewrite FC PTerm PTerm (Maybe PTerm) -- ^ "rewrite" syntax, with optional result type
736 | PPair FC PunInfo PTerm PTerm -- ^ A pair (a, b) and whether it's a product type or a pair (solved by elaboration)
737 | 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)
738 | PAs FC Name PTerm -- ^ @-pattern, valid LHS only
739 | PAlternative Bool [PTerm] -- ^ True if only one may work. (| A, B, C|)
740 | PHidden PTerm -- ^ Irrelevant or hidden pattern
741 | PType -- ^ 'Type' type
742 | PUniverse Universe -- ^ Some universe
743 | PGoal FC PTerm Name PTerm -- ^ quoteGoal, used for %reflection functions
744 | PConstant Const -- ^ Builtin types
745 | Placeholder -- ^ Underscore
746 | PDoBlock [PDo] -- ^ Do notation
747 | PIdiom FC PTerm -- ^ Idiom brackets
748 | PReturn FC
749 | PMetavar Name -- ^ A metavariable, ?name
750 | PProof [PTactic] -- ^ Proof script
751 | PTactics [PTactic] -- ^ As PProof, but no auto solving
752 | PElabError Err -- ^ Error to report on elaboration
753 | PImpossible -- ^ Special case for declaring when an LHS can't typecheck
754 | PCoerced PTerm -- ^ To mark a coerced argument, so as not to coerce twice
755 | PDisamb [[T.Text]] PTerm -- ^ Preferences for explicit namespaces
756 | PUnifyLog PTerm -- ^ dump a trace of unifications when building term
757 | PNoImplicits PTerm -- ^ never run implicit converions on the term
758 | PQuasiquote PTerm (Maybe PTerm) -- ^ `(Term [: Term])
759 | PUnquote PTerm -- ^ ,Term
760 deriving Eq
763{-!
764deriving instance Binary PTerm
765deriving instance NFData PTerm
766!-}
768mapPT :: (PTerm -> PTerm) -> PTerm -> PTerm
769mapPT f t = f (mpt t) where
770 mpt (PLam fc n t s) = PLam fc n (mapPT f t) (mapPT f s)
771 mpt (PPi p n t s) = PPi p n (mapPT f t) (mapPT f s)
772 mpt (PLet fc n ty v s) = PLet fc n (mapPT f ty) (mapPT f v) (mapPT f s)
773 mpt (PRewrite fc t s g) = PRewrite fc (mapPT f t) (mapPT f s)
774 (fmap (mapPT f) g)
775 mpt (PApp fc t as) = PApp fc (mapPT f t) (map (fmap (mapPT f)) as)
776 mpt (PAppBind fc t as) = PAppBind fc (mapPT f t) (map (fmap (mapPT f)) as)
777 mpt (PCase fc c os) = PCase fc (mapPT f c) (map (pmap (mapPT f)) os)
778 mpt (PEq fc lt rt l r) = PEq fc (mapPT f lt) (mapPT f rt) (mapPT f l) (mapPT f r)
779 mpt (PTyped l r) = PTyped (mapPT f l) (mapPT f r)
780 mpt (PPair fc p l r) = PPair fc p (mapPT f l) (mapPT f r)
781 mpt (PDPair fc p l t r) = PDPair fc p (mapPT f l) (mapPT f t) (mapPT f r)
782 mpt (PAlternative a as) = PAlternative a (map (mapPT f) as)
783 mpt (PHidden t) = PHidden (mapPT f t)
784 mpt (PDoBlock ds) = PDoBlock (map (fmap (mapPT f)) ds)
785 mpt (PProof ts) = PProof (map (fmap (mapPT f)) ts)
786 mpt (PTactics ts) = PTactics (map (fmap (mapPT f)) ts)
787 mpt (PUnifyLog tm) = PUnifyLog (mapPT f tm)
788 mpt (PDisamb ns tm) = PDisamb ns (mapPT f tm)
789 mpt (PNoImplicits tm) = PNoImplicits (mapPT f tm)
790 mpt (PGoal fc r n sc) = PGoal fc (mapPT f r) n (mapPT f sc)
791 mpt x = x
794data PTactic' t = Intro [Name] | Intros | Focus Name
795 | Refine Name [Bool] | Rewrite t | DoUnify
796 | Induction t
797 | CaseTac t
798 | Equiv t
799 | MatchRefine Name
800 | LetTac Name t | LetTacTy Name t t
801 | Exact t | Compute | Trivial | TCInstance
802 | ProofSearch Bool Bool Int (Maybe Name) [Name]
803 -- ^ the bool is whether to search recursively
804 | Solve
805 | Attack
806 | ProofState | ProofTerm | Undo
807 | Try (PTactic' t) (PTactic' t)
808 | TSeq (PTactic' t) (PTactic' t)
809 | ApplyTactic t -- see Language.Reflection module
810 | ByReflection t
811 | Reflect t
812 | Fill t
813 | GoalType String (PTactic' t)
814 | TCheck t
815 | TEval t
816 | TDocStr (Either Name Const)
817 | TSearch t
818 | Skip
819 | TFail [ErrorReportPart]
820 | Qed | Abandon
821 | SourceFC
822 deriving (Show, Eq, Functor, Foldable, Traversable)
823{-!
824deriving instance Binary PTactic'
825deriving instance NFData PTactic'
826!-}
827instance Sized a => Sized (PTactic' a) where
828 size (Intro nms) = 1 + size nms
829 size Intros = 1
830 size (Focus nm) = 1 + size nm
831 size (Refine nm bs) = 1 + size nm + length bs
832 size (Rewrite t) = 1 + size t
833 size (Induction t) = 1 + size t
834 size (LetTac nm t) = 1 + size nm + size t
835 size (Exact t) = 1 + size t
836 size Compute = 1
837 size Trivial = 1
838 size Solve = 1
839 size Attack = 1
840 size ProofState = 1
841 size ProofTerm = 1
842 size Undo = 1
843 size (Try l r) = 1 + size l + size r
844 size (TSeq l r) = 1 + size l + size r
845 size (ApplyTactic t) = 1 + size t
846 size (Reflect t) = 1 + size t
847 size (Fill t) = 1 + size t
848 size Qed = 1
849 size Abandon = 1
850 size Skip = 1
851 size (TFail ts) = 1 + size ts
852 size SourceFC = 1
854type PTactic = PTactic' PTerm
856data PDo' t = DoExp FC t
857 | DoBind FC Name t
858 | DoBindP FC t t [(t,t)]
859 | DoLet FC Name t t
860 | DoLetP FC t t
861 deriving (Eq, Functor)
862{-!
863deriving instance Binary PDo'
864deriving instance NFData PDo'
865!-}
867instance Sized a => Sized (PDo' a) where
868 size (DoExp fc t) = 1 + size fc + size t
869 size (DoBind fc nm t) = 1 + size fc + size nm + size t
870 size (DoBindP fc l r alts) = 1 + size fc + size l + size r + size alts
871 size (DoLet fc nm l r) = 1 + size fc + size nm + size l + size r
872 size (DoLetP fc l r) = 1 + size fc + size l + size r
874type PDo = PDo' PTerm
876-- The priority gives a hint as to elaboration order. Best to elaborate
877-- things early which will help give a more concrete type to other
878-- variables, e.g. a before (interpTy a).
880data PArg' t = PImp { priority :: Int,
881 machine_inf :: Bool, -- true if the machine inferred it
882 argopts :: [ArgOpt],
883 pname :: Name, getTm :: t }
884 | PExp { priority :: Int,
885 argopts :: [ArgOpt],
886 pname :: Name,
887 getTm :: t }
888 | PConstraint { priority :: Int,
889 argopts :: [ArgOpt],
890 pname :: Name,
891 getTm :: t }
892 | PTacImplicit { priority :: Int,
893 argopts :: [ArgOpt],
894 pname :: Name,
895 getScript :: t,
896 getTm :: t }
897 deriving (Show, Eq, Functor)
899data ArgOpt = AlwaysShow | HideDisplay | InaccessibleArg
900 deriving (Show, Eq)
902instance Sized a => Sized (PArg' a) where
903 size (PImp p _ l nm trm) = 1 + size nm + size trm
904 size (PExp p l nm trm) = 1 + size nm + size trm
905 size (PConstraint p l nm trm) = 1 + size nm +size nm + size trm
906 size (PTacImplicit p l nm scr trm) = 1 + size nm + size scr + size trm
908{-!
909deriving instance Binary PArg'
910deriving instance NFData PArg'
911!-}
913pimp n t mach = PImp 1 mach [] n t
914pexp t = PExp 1 [] (sMN 0 "arg") t
915pconst t = PConstraint 1 [] (sMN 0 "carg") t
916ptacimp n s t = PTacImplicit 2 [] n s t
918type PArg = PArg' PTerm
920-- Type class data
922data ClassInfo = CI { instanceName :: Name,
923 class_methods :: [(Name, (FnOpts, PTerm))],
924 class_defaults :: [(Name, (Name, PDecl))], -- method name -> default impl
925 class_default_superclasses :: [PDecl],
926 class_params :: [Name],
927 class_instances :: [Name] }
928 deriving Show
929{-!
930deriving instance Binary ClassInfo
931deriving instance NFData ClassInfo
932!-}
934-- Type inference data
936data TIData = TIPartial -- ^ a function with a partially defined type
937 | TISolution [Term] -- ^ possible solutions to a metavariable in a type
938 deriving Show
940-- | Miscellaneous information about functions
941data FnInfo = FnInfo { fn_params :: [Int] }
942 deriving Show
943{-!
944deriving instance Binary FnInfo
945!-}
947data OptInfo = Optimise { inaccessible :: [(Int,Name)], -- includes names for error reporting
948 detaggable :: Bool }
949 deriving Show
950{-!
951deriving instance Binary OptInfo
952deriving instance NFData OptInfo
953!-}
956data TypeInfo = TI { con_names :: [Name],
957 codata :: Bool,
958 data_opts :: DataOpts,
959 param_pos :: [Int],
960 mutual_types :: [Name] }
961 deriving Show
962{-!
963deriving instance Binary TypeInfo
964deriving instance NFData TypeInfo
965!-}
967-- Syntactic sugar info
969data DSL' t = DSL { dsl_bind :: t,
970 dsl_return :: t,
971 dsl_apply :: t,
972 dsl_pure :: t,
973 dsl_var :: Maybe t,
974 index_first :: Maybe t,
975 index_next :: Maybe t,
976 dsl_lambda :: Maybe t,
977 dsl_let :: Maybe t,
978 dsl_pi :: Maybe t
979 }
980 deriving (Show, Functor)
981{-!
982deriving instance Binary DSL'
983deriving instance NFData DSL'
984!-}
986type DSL = DSL' PTerm
988data SynContext = PatternSyntax | TermSyntax | AnySyntax
989 deriving Show
990{-!
991deriving instance Binary SynContext
992deriving instance NFData SynContext
993!-}
995data Syntax = Rule [SSymbol] PTerm SynContext
996 deriving Show
998syntaxNames :: Syntax -> [Name]
999syntaxNames (Rule syms _ _) = mapMaybe ename syms
1000 where ename (Keyword n) = Just n
1001 ename _ = Nothing
1003syntaxSymbols :: Syntax -> [SSymbol]
1004syntaxSymbols (Rule ss _ _) = ss
1005{-!
1006deriving instance Binary Syntax
1007deriving instance NFData Syntax
1008!-}
1010data SSymbol = Keyword Name
1011 | Symbol String
1012 | Binding Name
1013 | Expr Name
1014 | SimpleExpr Name
1015 deriving (Show, Eq)
1018{-!
1019deriving instance Binary SSymbol
1020deriving instance NFData SSymbol
1021!-}
1023newtype SyntaxRules = SyntaxRules { syntaxRulesList :: [Syntax] }
1025emptySyntaxRules :: SyntaxRules
1026emptySyntaxRules = SyntaxRules []
1028updateSyntaxRules :: [Syntax] -> SyntaxRules -> SyntaxRules
1029updateSyntaxRules rules (SyntaxRules sr) = SyntaxRules newRules
1030 where
1031 newRules = sortBy (ruleSort `on` syntaxSymbols) (rules ++ sr)
1033 ruleSort [] [] = EQ
1034 ruleSort [] _ = LT
1035 ruleSort _ [] = GT
1036 ruleSort (s1:ss1) (s2:ss2) =
1037 case symCompare s1 s2 of
1038 EQ -> ruleSort ss1 ss2
1039 r -> r
1041 -- Better than creating Ord instance for SSymbol since
1042 -- in general this ordering does not really make sense.
1043 symCompare (Keyword n1) (Keyword n2) = compare n1 n2
1044 symCompare (Keyword _) _ = LT
1045 symCompare (Symbol _) (Keyword _) = GT
1046 symCompare (Symbol s1) (Symbol s2) = compare s1 s2
1047 symCompare (Symbol _) _ = LT
1048 symCompare (Binding _) (Keyword _) = GT
1049 symCompare (Binding _) (Symbol _) = GT
1050 symCompare (Binding b1) (Binding b2) = compare b1 b2
1051 symCompare (Binding _) _ = LT
1052 symCompare (Expr _) (Keyword _) = GT
1053 symCompare (Expr _) (Symbol _) = GT
1054 symCompare (Expr _) (Binding _) = GT
1055 symCompare (Expr e1) (Expr e2) = compare e1 e2
1056 symCompare (Expr _) _ = LT
1057 symCompare (SimpleExpr _) (Keyword _) = GT
1058 symCompare (SimpleExpr _) (Symbol _) = GT
1059 symCompare (SimpleExpr _) (Binding _) = GT
1060 symCompare (SimpleExpr _) (Expr _) = GT
1061 symCompare (SimpleExpr e1) (SimpleExpr e2) = compare e1 e2
1063initDSL = DSL (PRef f (sUN ">>="))
1064 (PRef f (sUN "return"))
1065 (PRef f (sUN "<$>"))
1066 (PRef f (sUN "pure"))
1067 Nothing
1068 Nothing
1069 Nothing
1070 Nothing
1071 Nothing
1072 Nothing
1073 where f = fileFC "(builtin)"
1075data Using = UImplicit Name PTerm
1076 | UConstraint Name [Name]
1077 deriving (Show, Eq)
1078{-!
1079deriving instance Binary Using
1080deriving instance NFData Using
1081!-}
1083data SyntaxInfo = Syn { using :: [Using],
1084 syn_params :: [(Name, PTerm)],
1085 syn_namespace :: [String],
1086 no_imp :: [Name],
1087 decoration :: Name -> Name,
1088 inPattern :: Bool,
1089 implicitAllowed :: Bool,
1090 maxline :: Maybe Int,
1091 mut_nesting :: Int,
1092 dsl_info :: DSL,
1093 syn_in_quasiquote :: Int }
1094 deriving Show
1095{-!
1096deriving instance NFData SyntaxInfo
1097deriving instance Binary SyntaxInfo
1098!-}
1100defaultSyntax = Syn [] [] [] [] id False False Nothing 0 initDSL 0
1102expandNS :: SyntaxInfo -> Name -> Name
1103expandNS syn n@(NS _ _) = n
1104expandNS syn n = case syn_namespace syn of
1105 [] -> n
1106 xs -> sNS n xs
1109-- For inferring types of things
1111bi = fileFC "builtin"
1113inferTy = sMN 0 "__Infer"
1114inferCon = sMN 0 "__infer"
1115inferDecl = PDatadecl inferTy
1116 PType
1117 [(emptyDocstring, [], inferCon, PPi impl (sMN 0 "iType") PType (
1118 PPi expl (sMN 0 "ival") (PRef bi (sMN 0 "iType"))
1119 (PRef bi inferTy)), bi, [])]
1120inferOpts = []
1122infTerm t = PApp bi (PRef bi inferCon) [pimp (sMN 0 "iType") Placeholder True, pexp t]
1123infP = P (TCon 6 0) inferTy (TType (UVal 0))
1125getInferTerm, getInferType :: Term -> Term
1126getInferTerm (Bind n b sc) = Bind n b $ getInferTerm sc
1127getInferTerm (App (App _ _) tm) = tm
1128getInferTerm tm = tm -- error ("getInferTerm " ++ show tm)
1130getInferType (Bind n b sc) = Bind n (toTy b) $ getInferType sc
1131 where toTy (Lam t) = Pi t (TType (UVar 0))
1132 toTy (PVar t) = PVTy t
1133 toTy b = b
1134getInferType (App (App _ ty) _) = ty
1138-- Handy primitives: Unit, False, Pair, MkPair, =, mkForeign
1140primNames = [eqTy, eqCon, inferTy, inferCon]
1142unitTy = sUN "Unit"
1143unitCon = sUN "MkUnit"
1145falseDoc = fmap (const $ Msg "") . parseDocstring . T.pack $
1146 "The empty type, also known as the trivially false proposition." ++
1147 "\n\n" ++
1148 "Use `void` or `absurd` to prove anything if you have a variable " ++
1149 "of type `Void` in scope."
1150falseTy = sUN "Void"
1152pairTy = sNS (sUN "Pair") ["Builtins"]
1153pairCon = sNS (sUN "MkPair") ["Builtins"]
1155eqTy = sUN "="
1156eqCon = sUN "Refl"
1157eqDoc = fmap (const (Left $ Msg "")) . parseDocstring . T.pack $
1158 "The propositional equality type. A proof that `x` = `y`." ++
1159 "\n\n" ++
1160 "To use such a proof, pattern-match on it, and the two equal things will " ++
1161 "then need to be the _same_ pattern." ++
1162 "\n\n" ++
1163 "**Note**: Idris's equality type is potentially _heterogeneous_, which means that it " ++
1164 "is possible to state equalities between values of potentially different " ++
1165 "types. However, Idris will attempt the homogeneous case unless it fails to typecheck." ++
1166 "\n\n" ++
1167 "You may need to use `(~=~)` to explicitly request heterogeneous equality."
1169eqDecl = PDatadecl eqTy (piBindp impl [(n "A", PType), (n "B", PType)]
1170 (piBind [(n "x", PRef bi (n "A")), (n "y", PRef bi (n "B"))]
1171 PType))
1172 [(reflDoc, reflParamDoc,
1173 eqCon, PPi impl (n "A") PType (
1174 PPi impl (n "x") (PRef bi (n "A"))
1175 (PApp bi (PRef bi eqTy) [pimp (n "A") Placeholder False,
1176 pimp (n "B") Placeholder False,
1177 pexp (PRef bi (n "x")),
1178 pexp (PRef bi (n "x"))])), bi, [])]
1179 where n a = sUN a
1180 reflDoc = annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $
1181 "A proof that `x` in fact equals `x`. To construct this, you must have already " ++
1182 "shown that both sides are in fact equal."
1183 reflParamDoc = [(n "A", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the type at which the equality is proven"),
1184 (n "x", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the element shown to be equal to itself.")]
1186eqParamDoc = [(n "A", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the type of the left side of the equality"),
1187 (n "B", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the type of the right side of the equality")
1189 where n a = sUN a
1191eqOpts = []
1193-- Defined in builtins.idr
1194sigmaTy = sNS (sUN "Sigma") ["Builtins"]
1195existsCon = sNS (sUN "MkSigma") ["Builtins"]
1197piBind :: [(Name, PTerm)] -> PTerm -> PTerm
1198piBind = piBindp expl
1200piBindp :: Plicity -> [(Name, PTerm)] -> PTerm -> PTerm
1201piBindp p [] t = t
1202piBindp p ((n, ty):ns) t = PPi p n ty (piBindp p ns t)
1205-- Pretty-printing declarations and terms
1207-- These "show" instances render to an absurdly wide screen because inserted line breaks
1208-- could interfere with interactive editing, which calls "show".
1210instance Show PTerm where
1211 showsPrec _ tm = (displayS . renderPretty 1.0 10000000 . prettyImp defaultPPOption) tm
1213instance Show PDecl where
1214 showsPrec _ d = (displayS . renderPretty 1.0 10000000 . showDeclImp verbosePPOption) d
1216instance Show PClause where
1217 showsPrec _ c = (displayS . renderPretty 1.0 10000000 . showCImp verbosePPOption) c
1219instance Show PData where
1220 showsPrec _ d = (displayS . renderPretty 1.0 10000000 . showDImp defaultPPOption) d
1222instance Pretty PTerm OutputAnnotation where
1223 pretty = prettyImp defaultPPOption
1225-- | Colourise annotations according to an Idris state. It ignores the names
1226-- in the annotation, as there's no good way to show extended information on a
1227-- terminal.
1228consoleDecorate :: IState -> OutputAnnotation -> String -> String
1229consoleDecorate ist _ | not (idris_colourRepl ist) = id
1230consoleDecorate ist (AnnConst c) = let theme = idris_colourTheme ist
1231 in if constIsType c
1232 then colouriseType theme
1233 else colouriseData theme
1234consoleDecorate ist (AnnData _ _) = colouriseData (idris_colourTheme ist)
1235consoleDecorate ist (AnnType _ _) = colouriseType (idris_colourTheme ist)
1236consoleDecorate ist (AnnBoundName _ True) = colouriseImplicit (idris_colourTheme ist)
1237consoleDecorate ist (AnnBoundName _ False) = colouriseBound (idris_colourTheme ist)
1238consoleDecorate ist AnnKeyword = colouriseKeyword (idris_colourTheme ist)
1239consoleDecorate ist (AnnName n _ _ _) = let ctxt = tt_ctxt ist
1240 theme = idris_colourTheme ist
1241 in case () of
1242 _ | isDConName n ctxt -> colouriseData theme
1243 _ | isFnName n ctxt -> colouriseFun theme
1244 _ | isTConName n ctxt -> colouriseType theme
1245 _ | isPostulateName n ist -> colourisePostulate theme
1246 _ | otherwise -> id -- don't colourise unknown names
1247consoleDecorate ist (AnnFC _) = id
1248consoleDecorate ist (AnnTextFmt fmt) = Idris.Colours.colourise (colour fmt)
1249 where colour BoldText = IdrisColour Nothing True False True False
1250 colour UnderlineText = IdrisColour Nothing True True False False
1251 colour ItalicText = IdrisColour Nothing True False False True
1252consoleDecorate ist (AnnTerm _ _) = id
1253consoleDecorate ist (AnnSearchResult _) = id
1254consoleDecorate ist (AnnErr _) = id
1256isPostulateName :: Name -> IState -> Bool
1257isPostulateName n ist = S.member n (idris_postulates ist)
1259-- | Pretty-print a high-level closed Idris term with no information about precedence/associativity
1260prettyImp :: PPOption -- ^^ pretty printing options
1261 -> PTerm -- ^^ the term to pretty-print
1262 -> Doc OutputAnnotation
1263prettyImp impl = pprintPTerm impl [] [] []
1265-- | Serialise something to base64 using its Binary instance.
1267-- | Do the right thing for rendering a term in an IState
1268prettyIst :: IState -> PTerm -> Doc OutputAnnotation
1269prettyIst ist = pprintPTerm (ppOptionIst ist) [] [] (idris_infixes ist)
1271-- | Pretty-print a high-level Idris term in some bindings context with infix info
1272pprintPTerm :: PPOption -- ^^ pretty printing options
1273 -> [(Name, Bool)] -- ^^ the currently-bound names and whether they are implicit
1274 -> [Name] -- ^^ names to always show in pi, even if not used
1275 -> [FixDecl] -- ^^ Fixity declarations
1276 -> PTerm -- ^^ the term to pretty-print
1277 -> Doc OutputAnnotation
1278pprintPTerm ppo bnd docArgs infixes = prettySe 10 bnd
1279 where
1280 prettySe :: Int -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation
1281 prettySe p bnd (PQuote r) =
1282 text "![" <> pretty r <> text "]"
1283 prettySe p bnd (PPatvar fc n) = pretty n
1284 prettySe p bnd e
1285 | Just str <- slist p bnd e = str
1286 | Just n <- snat p e = annotate (AnnData "Nat" "") (text (show n))
1287 prettySe p bnd (PRef fc n) = prettyName True (ppopt_impl ppo) bnd n
1288 prettySe p bnd (PLam fc n ty sc) =
1289 bracket p 2 . group . align . hang 2 $
1290 text "\\" <> bindingOf n False <+> text "=>" <$>
1291 prettySe 10 ((n, False):bnd) sc
1292 prettySe p bnd (PLet fc n ty v sc) =
1293 bracket p 2 . group . align $
1294 kwd "let" <+> (group . align . hang 2 $ bindingOf n False <+> text "=" <$> prettySe 10 bnd v) </>
1295 kwd "in" <+> (group . align . hang 2 $ prettySe 10 ((n, False):bnd) sc)
1296 prettySe p bnd (PPi (Exp l s _) n ty sc)
1297 | n `elem` allNamesIn sc || ppopt_impl ppo || n `elem` docArgs =
1298 bracket p 2 . group $
1299 enclose lparen rparen (group . align $ bindingOf n False <+> colon <+> prettySe 10 bnd ty) <+>
1300 st <> text "->" <$> prettySe 10 ((n, False):bnd) sc
1301 | otherwise =
1302 bracket p 2 . group $
1303 group (prettySe 1 bnd ty <+> st) <> text "->" <$> group (prettySe 10 ((n, False):bnd) sc)
1304 where
1305 st =
1306 case s of
1307 Static -> text "[static]" <> space
1308 _ -> empty
1309 prettySe p bnd (PPi (Imp l s _) n ty sc)
1310 | ppopt_impl ppo =
1311 bracket p 2 $
1312 lbrace <> bindingOf n True <+> colon <+> prettySe 10 bnd ty <> rbrace <+>
1313 st <> text "->" </> prettySe 10 ((n, True):bnd) sc
1314 | otherwise = prettySe 10 ((n, True):bnd) sc
1315 where
1316 st =
1317 case s of
1318 Static -> text "[static]" <> space
1319 _ -> empty
1320 prettySe p bnd (PPi (Constraint _ _) n ty sc) =
1321 bracket p 2 $
1322 prettySe 10 bnd ty <+> text "=>" </> prettySe 10 ((n, True):bnd) sc
1323 prettySe p bnd (PPi (TacImp _ _ s) n ty sc) =
1324 bracket p 2 $
1325 lbrace <> kwd "tacimp" <+> pretty n <+> colon <+> prettySe 10 bnd ty <>
1326 rbrace <+> text "->" </> prettySe 10 ((n, True):bnd) sc
1327 prettySe p bnd (PApp _ (PRef _ f) args) -- normal names, no explicit args
1328 | UN nm <- basename f
1329 , not (ppopt_impl ppo) && null (getShowArgs args) =
1330 prettyName True (ppopt_impl ppo) bnd f
1331 prettySe p bnd (PAppBind _ (PRef _ f) [])
1332 | not (ppopt_impl ppo) = text "!" <> prettyName True (ppopt_impl ppo) bnd f
1333 prettySe p bnd (PApp _ (PRef _ op) args) -- infix operators
1334 | UN nm <- basename op
1335 , not (tnull nm) &&
1336 (not (ppopt_impl ppo)) && (not $ isAlpha (thead nm)) =
1337 case getShowArgs args of
1338 [] -> opName True
1339 [x] -> group (opName True <$> group (prettySe 0 bnd (getTm x)))
1340 [l,r] -> let precedence = fromMaybe 20 (fmap prec f)
1341 in bracket p precedence $ inFix (getTm l) (getTm r)
1342 (l@(PExp _ _ _ _) : r@(PExp _ _ _ _) : rest) ->
1343 bracket p 1 $
1344 enclose lparen rparen (inFix (getTm l) (getTm r)) <+>
1345 align (group (vsep (map (prettyArgS bnd) rest)))
1346 as -> opName True <+> align (vsep (map (prettyArgS bnd) as))
1347 where opName isPrefix = prettyName isPrefix (ppopt_impl ppo) bnd op
1348 f = getFixity (opStr op)
1349 left l = case f of
1350 Nothing -> prettySe (-1) bnd l
1351 Just (Infixl p') -> prettySe p' bnd l
1352 Just f' -> prettySe (prec f'-1) bnd l
1353 right r = case f of
1354 Nothing -> prettySe (-1) bnd r
1355 Just (Infixr p') -> prettySe p' bnd r
1356 Just f' -> prettySe (prec f'-1) bnd r
1357 inFix l r = align . group $
1358 (left l <+> opName False) <$> group (right r)
1359 prettySe p bnd (PApp _ hd@(PRef fc f) [tm]) -- symbols, like 'foo
1360 | PConstant (Idris.Core.TT.Str str) <- getTm tm,
1361 f == sUN "Symbol_" = annotate (AnnType ("'" ++ str) ("The symbol " ++ str)) $
1362 char '\'' <> prettySe 10 bnd (PRef fc (sUN str))
1363 prettySe p bnd (PApp _ f as) = -- Normal prefix applications
1364 let args = getShowArgs as
1365 fp = prettySe 1 bnd f
1366 in
1367 bracket p 1 . group $
1368 if ppopt_impl ppo
1369 then if null as
1370 then fp
1371 else fp <+> align (vsep (map (prettyArgS bnd) as))
1372 else if null args
1373 then fp
1374 else fp <+> align (vsep (map (prettyArgS bnd) args))
1375 prettySe p bnd (PCase _ scr cases) =
1376 align $ kwd "case" <+> prettySe 10 bnd scr <+> kwd "of" <$>
1377 indent 2 (vsep (map ppcase cases))
1378 where
1379 ppcase (l, r) = nest nestingSize $
1380 prettySe 10 ([(n, False) | n <- vars l] ++ bnd) l <+>
1381 text "=>" <+>
1382 prettySe 10 ([(n, False) | n <- vars l] ++ bnd) r
1383 -- Warning: this is a bit of a hack. At this stage, we don't have the
1384 -- global context, so we can't determine which names are constructors,
1385 -- which are types, and which are pattern variables on the LHS of the
1386 -- case pattern. We use the heuristic that names without a namespace
1387 -- are patvars, because right now case blocks in PTerms are always
1388 -- delaborated from TT before being sent to the pretty-printer. If they
1389 -- start getting printed directly, THIS WILL BREAK.
1390 -- Potential solution: add a list of known patvars to the cases in
1391 -- PCase, and have the delaborator fill it out, kind of like the pun
1392 -- disambiguation on PDPair.
1393 vars tm = filter noNS (allNamesIn tm)
1394 noNS (NS _ _) = False
1395 noNS _ = True
1397 prettySe p bnd (PHidden tm) = text "." <> prettySe 0 bnd tm
1398 prettySe p bnd (PRefl _ _) = annName eqCon $ text "Refl"
1399 prettySe p bnd (PResolveTC _) = text "resolvetc"
1400 prettySe p bnd (PTrue _ IsType) = annName unitTy $ text "()"
1401 prettySe p bnd (PTrue _ IsTerm) = annName unitCon $ text "()"
1402 prettySe p bnd (PTrue _ TypeOrTerm) = text "()"
1403 prettySe p bnd (PEq _ lt rt l r)
1404 | ppopt_impl ppo =
1405 bracket p 1 $
1406 enclose lparen rparen eq <+>
1407 align (group (vsep (map (prettyArgS bnd)
1408 [PImp 0 False [] (sUN "A") lt,
1409 PImp 0 False [] (sUN "B") rt,
1410 PExp 0 [] (sUN "x") l,
1411 PExp 0 [] (sUN "y") r])))
1412 | otherwise =
1413 bracket p 2 . align . group $
1414 prettySe 10 bnd l <+> eq <$> group (prettySe 10 bnd r)
1415 where eq = annName eqTy (text "=")
1416 prettySe p bnd (PRewrite _ l r _) =
1417 bracket p 2 $
1418 text "rewrite" <+> prettySe 10 bnd l <+> text "in" <+> prettySe 10 bnd r
1419 prettySe p bnd (PTyped l r) =
1420 lparen <> prettySe 10 bnd l <+> colon <+> prettySe 10 bnd r <> rparen
1421 prettySe p bnd pair@(PPair _ pun _ _) -- flatten tuples to the right, like parser
1422 | Just elts <- pairElts pair = enclose (ann lparen) (ann rparen) .
1423 align . group . vsep . punctuate (ann comma) $
1424 map (prettySe 10 bnd) elts
1425 where ann = case pun of
1426 TypeOrTerm -> id
1427 IsType -> annName pairTy
1428 IsTerm -> annName pairCon
1429 prettySe p bnd (PDPair _ TypeOrTerm l t r) =
1430 lparen <> prettySe 10 bnd l <+> text "**" <+> prettySe 10 bnd r <> rparen
1431 prettySe p bnd (PDPair _ IsType (PRef _ n) t r) =
1432 annName sigmaTy lparen <>
1433 bindingOf n False <+>
1434 annName sigmaTy (text "**") <+>
1435 prettySe 10 ((n, False):bnd) r <>
1436 annName sigmaTy rparen
1437 prettySe p bnd (PDPair _ IsType l t r) =
1438 annName sigmaTy lparen <>
1439 prettySe 10 bnd l <+>
1440 annName sigmaTy (text "**") <+>
1441 prettySe 10 bnd r <>
1442 annName sigmaTy rparen
1443 prettySe p bnd (PDPair _ IsTerm l t r) =
1444 annName existsCon lparen <>
1445 prettySe 10 bnd l <+>
1446 annName existsCon (text "**") <+>
1447 prettySe 10 bnd r <>
1448 annName existsCon rparen
1449 prettySe p bnd (PAlternative a as) =
1450 lparen <> text "|" <> prettyAs <> text "|" <> rparen
1451 where
1452 prettyAs =
1453 foldr (\l -> \r -> l <+> text "," <+> r) empty $ map (prettySe 10 bnd) as
1454 prettySe p bnd PType = annotate (AnnType "Type" "The type of types") $ text "Type"
1455 prettySe p bnd (PUniverse u) = annotate (AnnType (show u) "The type of unique types") $ text (show u)
1456 prettySe p bnd (PConstant c) = annotate (AnnConst c) (text (show c))
1457 -- XXX: add pretty for tactics
1458 prettySe p bnd (PProof ts) =
1459 text "proof" <+> lbrace <> nest nestingSize (text . show $ ts) <> rbrace
1460 prettySe p bnd (PTactics ts) =
1461 text "tactics" <+> lbrace <> nest nestingSize (text . show $ ts) <> rbrace
1462 prettySe p bnd (PMetavar n) = text "?" <> pretty n
1463 prettySe p bnd (PReturn f) = kwd "return"
1464 prettySe p bnd PImpossible = kwd "impossible"
1465 prettySe p bnd Placeholder = text "_"
1466 prettySe p bnd (PDoBlock _) = text "do block pretty not implemented"
1467 prettySe p bnd (PCoerced t) = prettySe p bnd t
1468 prettySe p bnd (PElabError s) = pretty s
1469 -- Quasiquote pprinting ignores bound vars
1470 prettySe p bnd (PQuasiquote t Nothing) = text "`(" <> prettySe p [] t <> text ")"
1471 prettySe p bnd (PQuasiquote t (Just g)) = text "`(" <> prettySe p [] t <+> colon <+> prettySe p [] g <> text ")"
1472 prettySe p bnd (PUnquote t) = text "~" <> prettySe p bnd t
1474 prettySe p bnd _ = text "missing pretty-printer for term"
1476 prettyArgS bnd (PImp _ _ _ n tm) = prettyArgSi bnd (n, tm)
1477 prettyArgS bnd (PExp _ _ _ tm) = prettyArgSe bnd tm
1478 prettyArgS bnd (PConstraint _ _ _ tm) = prettyArgSc bnd tm
1479 prettyArgS bnd (PTacImplicit _ _ n _ tm) = prettyArgSti bnd (n, tm)
1481 prettyArgSe bnd arg = prettySe 0 bnd arg
1482 prettyArgSi bnd (n, val) = lbrace <> pretty n <+> text "=" <+> prettySe 10 bnd val <> rbrace
1483 prettyArgSc bnd val = lbrace <> lbrace <> prettySe 10 bnd val <> rbrace <> rbrace
1484 prettyArgSti bnd (n, val) = lbrace <> kwd "auto" <+> pretty n <+> text "=" <+> prettySe 10 bnd val <> rbrace
1486 annName :: Name -> Doc OutputAnnotation -> Doc OutputAnnotation
1487 annName n = annotate (AnnName n Nothing Nothing Nothing)
1489 opStr :: Name -> String
1490 opStr (NS n _) = opStr n
1491 opStr (UN n) = T.unpack n
1493 basename :: Name -> Name
1494 basename (NS n _) = basename n
1495 basename n = n
1497 slist' p bnd (PApp _ (PRef _ nil) _)
1498 | not (ppopt_impl ppo) && nsroot nil == sUN "Nil" = Just []
1499 slist' p bnd (PRef _ nil)
1500 | not (ppopt_impl ppo) && nsroot nil == sUN "Nil" = Just []
1501 slist' p bnd (PApp _ (PRef _ cons) args)
1502 | nsroot cons == sUN "::",
1503 (PExp {getTm=tl}):(PExp {getTm=hd}):imps <- reverse args,
1504 all isImp imps,
1505 Just tl' <- slist' p bnd tl
1506 = Just (hd:tl')
1507 where
1508 isImp (PImp {}) = True
1509 isImp _ = False
1510 slist' _ _ tm = Nothing
1512 slist p bnd e | Just es <- slist' p bnd e = Just $
1513 case es of [] -> annotate (AnnData "" "") $ text "[]"
1514 [x] -> enclose left right . group $
1515 prettySe p bnd x
1516 xs -> (enclose left right .
1517 align . group . vsep .
1518 punctuate comma .
1519 map (prettySe p bnd)) xs
1520 where left = (annotate (AnnData "" "") (text "["))
1521 right = (annotate (AnnData "" "") (text "]"))
1522 comma = (annotate (AnnData "" "") (text ","))
1523 slist _ _ _ = Nothing
1525 pairElts :: PTerm -> Maybe [PTerm]
1526 pairElts (PPair _ _ x y) | Just elts <- pairElts y = Just (x:elts)
1527 | otherwise = Just [x, y]
1528 pairElts _ = Nothing
1530 natns = "Prelude.Nat."
1532 snat p (PRef _ z)
1533 | show z == (natns++"Z") || show z == "Z" = Just 0
1534 snat p (PApp _ s [PExp {getTm=n}])
1535 | show s == (natns++"S") || show s == "S",
1536 Just n' <- snat p n
1537 = Just $ 1 + n'
1538 snat _ _ = Nothing
1540 bracket outer inner doc
1541 | inner > outer = lparen <> doc <> rparen
1542 | otherwise = doc
1544 kwd = annotate AnnKeyword . text
1546 fixities :: M.Map String Fixity
1547 fixities = M.fromList [(s, f) | (Fix f s) <- infixes]
1549 getFixity :: String -> Maybe Fixity
1550 getFixity = flip M.lookup fixities
1552-- | Pretty-printer helper for the binding site of a name
1553bindingOf :: Name -- ^^ the bound name
1554 -> Bool -- ^^ whether the name is implicit
1555 -> Doc OutputAnnotation
1556bindingOf n imp = annotate (AnnBoundName n imp) (text (show n))
1558-- | Pretty-printer helper for names that attaches the correct annotations
1559prettyName
1560 :: Bool -- ^^ whether the name should be parenthesised if it is an infix operator
1561 -> Bool -- ^^ whether to show namespaces
1562 -> [(Name, Bool)] -- ^^ the current bound variables and whether they are implicit
1563 -> Name -- ^^ the name to pprint
1564 -> Doc OutputAnnotation
1565prettyName infixParen showNS bnd n
1566 | (MN _ s) <- n, isPrefixOf "_" $ T.unpack s = text "_"
1567 | (UN n') <- n, isPrefixOf "_" $ T.unpack n' = text "_"
1568 | Just imp <- lookup n bnd = annotate (AnnBoundName n imp) fullName
1569 | otherwise = annotate (AnnName n Nothing Nothing Nothing) fullName
1570 where fullName = text nameSpace <> parenthesise (text (baseName n))
1571 baseName (UN n) = T.unpack n
1572 baseName (NS n ns) = baseName n
1573 baseName (MN i s) = T.unpack s
1574 baseName other = show other
1575 nameSpace = case n of
1576 (NS n' ns) -> if showNS then (concatMap (++ ".") . map T.unpack . reverse) ns else ""
1577 _ -> ""
1578 isInfix = case baseName n of
1579 "" -> False
1580 (c : _) -> not (isAlpha c)
1581 parenthesise = if isInfix && infixParen then enclose lparen rparen else id
1584showCImp :: PPOption -> PClause -> Doc OutputAnnotation
1585showCImp ppo (PClause _ n l ws r w)
1586 = prettyImp ppo l <+> showWs ws <+> text "=" <+> prettyImp ppo r
1587 <+> text "where" <+> text (show w)
1588 where
1589 showWs [] = empty
1590 showWs (x : xs) = text "|" <+> prettyImp ppo x <+> showWs xs
1591showCImp ppo (PWith _ n l ws r w)
1592 = prettyImp ppo l <+> showWs ws <+> text "with" <+> prettyImp ppo r
1593 <+> braces (text (show w))
1594 where
1595 showWs [] = empty
1596 showWs (x : xs) = text "|" <+> prettyImp ppo x <+> showWs xs
1599showDImp :: PPOption -> PData -> Doc OutputAnnotation
1600showDImp ppo (PDatadecl n ty cons)
1601 = text "data" <+> text (show n) <+> colon <+> prettyImp ppo ty <+> text "where" <$>
1602 (indent 2 $ vsep (map (\ (_, _, n, t, _, _) -> pipe <+> prettyName True False [] n <+> colon <+> prettyImp ppo t) cons))
1604showDecls :: PPOption -> [PDecl] -> Doc OutputAnnotation
1605showDecls o ds = vsep (map (showDeclImp o) ds)
1607showDeclImp _ (PFix _ f ops) = text (show f) <+> cat (punctuate (text ",") (map text ops))
1608showDeclImp o (PTy _ _ _ _ _ n t) = text "tydecl" <+> text (showCG n) <+> colon <+> prettyImp o t
1609showDeclImp o (PClauses _ _ n cs) = text "pat" <+> text (showCG n) <+> text "\t" <+>
1610 indent 2 (vsep (map (showCImp o) cs))
1611showDeclImp o (PData _ _ _ _ _ d) = showDImp o { ppopt_impl = True } d
1612showDeclImp o (PParams _ ns ps) = text "params" <+> braces (text (show ns) <> line <> showDecls o ps <> line)
1613showDeclImp o (PNamespace n ps) = text "namespace" <+> text n <> braces (line <> showDecls o ps <> line)
1614showDeclImp _ (PSyntax _ syn) = text "syntax" <+> text (show syn)
1615showDeclImp o (PClass _ _ _ cs n ps _ ds)
1616 = text "class" <+> text (show cs) <+> text (show n) <+> text (show ps) <> line <> showDecls o ds
1617showDeclImp o (PInstance _ _ cs n _ t _ ds)
1618 = text "instance" <+> text (show cs) <+> text (show n) <+> prettyImp o t <> line <> showDecls o ds
1619showDeclImp _ _ = text "..."
1620-- showDeclImp (PImport o) = "import " ++ o
1622instance Show (Doc OutputAnnotation) where
1623 show = flip (displayS . renderCompact) ""
1625getImps :: [PArg] -> [(Name, PTerm)]
1626getImps [] = []
1627getImps (PImp _ _ _ n tm : xs) = (n, tm) : getImps xs
1628getImps (_ : xs) = getImps xs
1630getExps :: [PArg] -> [PTerm]
1631getExps [] = []
1632getExps (PExp _ _ _ tm : xs) = tm : getExps xs
1633getExps (_ : xs) = getExps xs
1635getShowArgs :: [PArg] -> [PArg]
1636getShowArgs [] = []
1637getShowArgs (e@(PExp _ _ _ tm) : xs) = e : getShowArgs xs
1638getShowArgs (e : xs) | AlwaysShow `elem` argopts e = e : getShowArgs xs
1639getShowArgs (_ : xs) = getShowArgs xs
1641getConsts :: [PArg] -> [PTerm]
1642getConsts [] = []
1643getConsts (PConstraint _ _ _ tm : xs) = tm : getConsts xs
1644getConsts (_ : xs) = getConsts xs
1646getAll :: [PArg] -> [PTerm]
1647getAll = map getTm
1650-- | Show Idris name
1651showName :: Maybe IState -- ^^ the Idris state, for information about names and colours
1652 -> [(Name, Bool)] -- ^^ the bound variables and whether they're implicit
1653 -> PPOption -- ^^ pretty printing options
1654 -> Bool -- ^^ whether to colourise
1655 -> Name -- ^^ the term to show
1656 -> String
1657showName ist bnd ppo colour n = case ist of
1658 Just i -> if colour then colourise n (idris_colourTheme i) else showbasic n
1659 Nothing -> showbasic n
1660 where name = if ppopt_impl ppo then show n else showbasic n
1661 showbasic n@(UN _) = showCG n
1662 showbasic (MN i s) = str s
1663 showbasic (NS n s) = showSep "." (map str (reverse s)) ++ "." ++ showbasic n
1664 showbasic (SN s) = show s
1665 fst3 (x, _, _) = x
1666 colourise n t = let ctxt' = fmap tt_ctxt ist in
1667 case ctxt' of
1668 Nothing -> name
1669 Just ctxt | Just impl <- lookup n bnd -> if impl then colouriseImplicit t name
1670 else colouriseBound t name
1671 | isDConName n ctxt -> colouriseData t name
1672 | isFnName n ctxt -> colouriseFun t name
1673 | isTConName n ctxt -> colouriseType t name
1674 -- The assumption is that if a name is not bound and does not exist in the
1675 -- global context, then we're somewhere in which implicit info has been lost
1676 -- (like error messages). Thus, unknown vars are colourised as implicits.
1677 | otherwise -> colouriseImplicit t name
1679showTm :: IState -- ^^ the Idris state, for information about identifiers and colours
1680 -> PTerm -- ^^ the term to show
1681 -> String
1682showTm ist = displayDecorated (consoleDecorate ist) .
1683 renderPretty 0.8 100000 .
1684 prettyImp (ppOptionIst ist)
1686-- | Show a term with implicits, no colours
1687showTmImpls :: PTerm -> String
1688showTmImpls = flip (displayS . renderCompact . prettyImp verbosePPOption) ""
1692instance Sized PTerm where
1693 size (PQuote rawTerm) = size rawTerm
1694 size (PRef fc name) = size name
1695 size (PLam fc name ty bdy) = 1 + size ty + size bdy
1696 size (PPi plicity name ty bdy) = 1 + size ty + size bdy
1697 size (PLet fc name ty def bdy) = 1 + size ty + size def + size bdy
1698 size (PTyped trm ty) = 1 + size trm + size ty
1699 size (PApp fc name args) = 1 + size args
1700 size (PAppBind fc name args) = 1 + size args
1701 size (PCase fc trm bdy) = 1 + size trm + size bdy
1702 size (PTrue fc _) = 1
1703 size (PRefl fc _) = 1
1704 size (PResolveTC fc) = 1
1705 size (PEq fc _ _ left right) = 1 + size left + size right
1706 size (PRewrite fc left right _) = 1 + size left + size right
1707 size (PPair fc _ left right) = 1 + size left + size right
1708 size (PDPair fs _ left ty right) = 1 + size left + size ty + size right
1709 size (PAlternative a alts) = 1 + size alts
1710 size (PHidden hidden) = size hidden
1711 size (PUnifyLog tm) = size tm
1712 size (PDisamb _ tm) = size tm
1713 size (PNoImplicits tm) = size tm
1714 size PType = 1
1715 size (PUniverse _) = 1
1716 size (PConstant const) = 1 + size const
1717 size Placeholder = 1
1718 size (PDoBlock dos) = 1 + size dos
1719 size (PIdiom fc term) = 1 + size term
1720 size (PReturn fc) = 1
1721 size (PMetavar name) = 1
1722 size (PProof tactics) = size tactics
1723 size (PElabError err) = size err
1724 size PImpossible = 1
1725 size _ = 0
1727getPArity :: PTerm -> Int
1728getPArity (PPi _ _ _ sc) = 1 + getPArity sc
1729getPArity _ = 0
1731-- Return all names, free or globally bound, in the given term.
1733allNamesIn :: PTerm -> [Name]
1734allNamesIn tm = nub $ ni [] tm
1735 where -- TODO THINK added niTacImp, but is it right?
1736 ni env (PRef _ n)
1737 | not (n `elem` env) = [n]
1738 ni env (PPatvar _ n) = [n]
1739 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
1740 ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
1741 ni env (PCase _ c os) = ni env c ++ concatMap (ni env) (map snd os)
1742 ni env (PLam fc n ty sc) = ni env ty ++ ni (n:env) sc
1743 ni env (PPi p n ty sc) = niTacImp env p ++ ni env ty ++ ni (n:env) sc
1744 ni env (PHidden tm) = ni env tm
1745 ni env (PEq _ _ _ l r) = ni env l ++ ni env r
1746 ni env (PRewrite _ l r _) = ni env l ++ ni env r
1747 ni env (PTyped l r) = ni env l ++ ni env r
1748 ni env (PPair _ _ l r) = ni env l ++ ni env r
1749 ni env (PDPair _ _ (PRef _ n) t r) = ni env t ++ ni (n:env) r
1750 ni env (PDPair _ _ l t r) = ni env l ++ ni env t ++ ni env r
1751 ni env (PAlternative a ls) = concatMap (ni env) ls
1752 ni env (PUnifyLog tm) = ni env tm
1753 ni env (PDisamb _ tm) = ni env tm
1754 ni env (PNoImplicits tm) = ni env tm
1755 ni env _ = []
1757 niTacImp env (TacImp _ _ scr) = ni env scr
1758 niTacImp _ _ = []
1760-- Return all names defined in binders in the given term
1761boundNamesIn :: PTerm -> [Name]
1762boundNamesIn tm = nub $ ni tm
1763 where -- TODO THINK Added niTacImp, but is it right?
1764 ni (PApp _ f as) = ni f ++ concatMap (ni) (map getTm as)
1765 ni (PAppBind _ f as) = ni f ++ concatMap (ni) (map getTm as)
1766 ni (PCase _ c os) = ni c ++ concatMap (ni) (map snd os)
1767 ni (PLam fc n ty sc) = n : (ni ty ++ ni sc)
1768 ni (PLet fc n ty val sc) = n : (ni ty ++ ni val ++ ni sc)
1769 ni (PPi p n ty sc) = niTacImp p ++ (n : (ni ty ++ ni sc))
1770 ni (PEq _ _ _ l r) = ni l ++ ni r
1771 ni (PRewrite _ l r _) = ni l ++ ni r
1772 ni (PTyped l r) = ni l ++ ni r
1773 ni (PPair _ _ l r) = ni l ++ ni r
1774 ni (PDPair _ _ (PRef _ n) t r) = ni t ++ ni r
1775 ni (PDPair _ _ l t r) = ni l ++ ni t ++ ni r
1776 ni (PAlternative a as) = concatMap (ni) as
1777 ni (PHidden tm) = ni tm
1778 ni (PUnifyLog tm) = ni tm
1779 ni (PDisamb _ tm) = ni tm
1780 ni (PNoImplicits tm) = ni tm
1781 ni _ = []
1783 niTacImp (TacImp _ _ scr) = ni scr
1784 niTacImp _ = []
1786-- Return names which are valid implicits in the given term (type).
1787implicitNamesIn :: [Name] -> IState -> PTerm -> [Name]
1788implicitNamesIn uvars ist tm = nub $ ni [] tm
1789 where
1790 ni env (PRef _ n)
1791 | not (n `elem` env)
1792 = case lookupTy n (tt_ctxt ist) of
1793 [] -> [n]
1794 _ -> if n `elem` uvars then [n] else []
1795 ni env (PApp _ f@(PRef _ n) as)
1796 | n `elem` uvars = ni env f ++ concatMap (ni env) (map getTm as)
1797 | otherwise = concatMap (ni env) (map getTm as)
1798 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
1799 ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
1800 ni env (PCase _ c os) = ni env c ++
1801 -- names in 'os', not counting the names bound in the cases
1802 (nub (concatMap (ni env) (map snd os))
1803 \\ nub (concatMap (ni env) (map fst os)))
1804 ni env (PLam fc n ty sc) = ni env ty ++ ni (n:env) sc
1805 ni env (PPi p n ty sc) = ni env ty ++ ni (n:env) sc
1806 ni env (PEq _ _ _ l r) = ni env l ++ ni env r
1807 ni env (PRewrite _ l r _) = ni env l ++ ni env r
1808 ni env (PTyped l r) = ni env l ++ ni env r
1809 ni env (PPair _ _ l r) = ni env l ++ ni env r
1810 ni env (PDPair _ _ (PRef _ n) t r) = ni env t ++ ni (n:env) r
1811 ni env (PDPair _ _ l t r) = ni env l ++ ni env t ++ ni env r
1812 ni env (PAlternative a as) = concatMap (ni env) as
1813 ni env (PHidden tm) = ni env tm
1814 ni env (PUnifyLog tm) = ni env tm
1815 ni env (PDisamb _ tm) = ni env tm
1816 ni env (PNoImplicits tm) = ni env tm
1817 ni env _ = []
1819-- Return names which are free in the given term.
1820namesIn :: [(Name, PTerm)] -> IState -> PTerm -> [Name]
1821namesIn uvars ist tm = nub $ ni [] tm
1822 where
1823 ni env (PRef _ n)
1824 | not (n `elem` env)
1825 = case lookupTy n (tt_ctxt ist) of
1826 [] -> [n]
1827 _ -> if n `elem` (map fst uvars) then [n] else []
1828 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
1829 ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
1830 ni env (PCase _ c os) = ni env c ++
1831 -- names in 'os', not counting the names bound in the cases
1832 (nub (concatMap (ni env) (map snd os))
1833 \\ nub (concatMap (ni env) (map fst os)))
1834 ni env (PLam fc n ty sc) = ni env ty ++ ni (n:env) sc
1835 ni env (PPi p n ty sc) = niTacImp env p ++ ni env ty ++ ni (n:env) sc
1836 ni env (PEq _ _ _ l r) = ni env l ++ ni env r
1837 ni env (PRewrite _ l r _) = ni env l ++ ni env r
1838 ni env (PTyped l r) = ni env l ++ ni env r
1839 ni env (PPair _ _ l r) = ni env l ++ ni env r
1840 ni env (PDPair _ _ (PRef _ n) t r) = ni env t ++ ni (n:env) r
1841 ni env (PDPair _ _ l t r) = ni env l ++ ni env t ++ ni env r
1842 ni env (PAlternative a as) = concatMap (ni env) as
1843 ni env (PHidden tm) = ni env tm
1844 ni env (PUnifyLog tm) = ni env tm
1845 ni env (PDisamb _ tm) = ni env tm
1846 ni env (PNoImplicits tm) = ni env tm
1847 ni env _ = []
1849 niTacImp env (TacImp _ _ scr) = ni env scr
1850 niTacImp _ _ = []
1852-- Return which of the given names are used in the given term.
1854usedNamesIn :: [Name] -> IState -> PTerm -> [Name]
1855usedNamesIn vars ist tm = nub $ ni [] tm
1856 where -- TODO THINK added niTacImp, but is it right?
1857 ni env (PRef _ n)
1858 | n `elem` vars && not (n `elem` env)
1859 = case lookupDefExact n (tt_ctxt ist) of
1860 Nothing -> [n]
1861 _ -> []
1862 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
1863 ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
1864 ni env (PCase _ c os) = ni env c ++ concatMap (ni env) (map snd os)
1865 ni env (PLam fc n ty sc) = ni env ty ++ ni (n:env) sc
1866 ni env (PPi p n ty sc) = niTacImp env p ++ ni env ty ++ ni (n:env) sc
1867 ni env (PEq _ _ _ l r) = ni env l ++ ni env r
1868 ni env (PRewrite _ l r _) = ni env l ++ ni env r
1869 ni env (PTyped l r) = ni env l ++ ni env r
1870 ni env (PPair _ _ l r) = ni env l ++ ni env r
1871 ni env (PDPair _ _ (PRef _ n) t r) = ni env t ++ ni (n:env) r
1872 ni env (PDPair _ _ l t r) = ni env l ++ ni env t ++ ni env r
1873 ni env (PAlternative a as) = concatMap (ni env) as
1874 ni env (PHidden tm) = ni env tm
1875 ni env (PUnifyLog tm) = ni env tm
1876 ni env (PDisamb _ tm) = ni env tm
1877 ni env (PNoImplicits tm) = ni env tm
1878 ni env _ = []
1880 niTacImp env (TacImp _ _ scr) = ni env scr
1881 niTacImp _ _ = []
1883-- Return the list of inaccessible (= dotted) positions for a name.
1884getErasureInfo :: IState -> Name -> [Int]
1885getErasureInfo ist n =
1886 case lookupCtxtExact n (idris_optimisation ist) of
1887 Just (Optimise inacc detagg) -> map fst inacc
1888 Nothing -> []