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