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