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