git.iko.soy/Idris-dev
on cdff1db help sign in
Idris-dev/src/Idris/AbsSyntaxTree.hs
1815 lines 74 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.List hiding (group)
25import Data.Char
26import qualified Data.Map as M
27import qualified Data.Text as T
28import qualified Data.Map as M
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 much 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 rec_elabDecl :: ElabWhat -> ElabInfo -> PDecl ->
54 Idris () }
56toplevel :: ElabInfo
57toplevel = EInfo [] emptyContext id Nothing (\_ _ _ -> fail "Not implemented")
59eInfoNames :: ElabInfo -> [Name]
60eInfoNames info = map fst (params info) ++ M.keys (inblock info)
62data IOption = IOption { opt_logLevel :: Int,
63 opt_typecase :: Bool,
64 opt_typeintype :: Bool,
65 opt_coverage :: Bool,
66 opt_showimp :: Bool, -- ^^ show implicits
67 opt_errContext :: Bool,
68 opt_repl :: Bool,
69 opt_verbose :: Bool,
70 opt_nobanner :: Bool,
71 opt_quiet :: Bool,
72 opt_codegen :: Codegen,
73 opt_outputTy :: OutputType,
74 opt_ibcsubdir :: FilePath,
75 opt_importdirs :: [FilePath],
76 opt_triple :: String,
77 opt_cpu :: String,
78 opt_cmdline :: [Opt], -- remember whole command line
79 opt_origerr :: Bool,
80 opt_autoSolve :: Bool, -- ^ automatically apply "solve" tactic in prover
81 opt_autoImport :: [FilePath], -- ^ e.g. Builtins+Prelude
82 opt_optimise :: [Optimisation]
83 }
84 deriving (Show, Eq)
86defaultOpts = IOption { opt_logLevel = 0
87 , opt_typecase = False
88 , opt_typeintype = False
89 , opt_coverage = True
90 , opt_showimp = False
91 , opt_errContext = False
92 , opt_repl = True
93 , opt_verbose = True
94 , opt_nobanner = False
95 , opt_quiet = False
96 , opt_codegen = Via "c"
97 , opt_outputTy = Executable
98 , opt_ibcsubdir = ""
99 , opt_importdirs = []
100 , opt_triple = ""
101 , opt_cpu = ""
102 , opt_cmdline = []
103 , opt_origerr = False
104 , opt_autoSolve = True
105 , opt_autoImport = []
106 , opt_optimise = defaultOptimise
107 }
109data PPOption = PPOption {
110 ppopt_impl :: Bool -- ^^ whether to show implicits
111} deriving (Show)
113data Optimisation = PETransform -- partial eval and associated transforms
114 deriving (Show, Eq)
116defaultOptimise = [PETransform]
118-- | Pretty printing options with default verbosity.
119defaultPPOption :: PPOption
120defaultPPOption = PPOption { ppopt_impl = False }
122-- | Pretty printing options with the most verbosity.
123verbosePPOption :: PPOption
124verbosePPOption = PPOption { ppopt_impl = True }
126-- | Get pretty printing options from the big options record.
127ppOption :: IOption -> PPOption
128ppOption opt = PPOption {
129 ppopt_impl = opt_showimp opt
132-- | Get pretty printing options from an idris state record.
133ppOptionIst :: IState -> PPOption
134ppOptionIst = ppOption . idris_options
136data LanguageExt = TypeProviders | ErrorReflection deriving (Show, Eq, Read, Ord)
138-- | The output mode in use
139data OutputMode = RawOutput Handle -- ^ Print user output directly to the handle
140 | IdeSlave Integer Handle -- ^ Send IDE output for some request ID to the handle
141 deriving Show
143-- | How wide is the console?
144data ConsoleWidth = InfinitelyWide -- ^ Have pretty-printer assume that lines should not be broken
145 | ColsWide Int -- ^ Manually specified - must be positive
146 | AutomaticWidth -- ^ Attempt to determine width, or 80 otherwise
148-- | The global state used in the Idris monad
149data IState = IState {
150 tt_ctxt :: Context, -- ^ All the currently defined names and their terms
151 idris_constraints :: [(UConstraint, FC)],
152 -- ^ A list of universe constraints and their corresponding source locations
153 idris_infixes :: [FixDecl], -- ^ Currently defined infix operators
154 idris_implicits :: Ctxt [PArg],
155 idris_statics :: Ctxt [Bool],
156 idris_classes :: Ctxt ClassInfo,
157 idris_dsls :: Ctxt DSL,
158 idris_optimisation :: Ctxt OptInfo,
159 idris_datatypes :: Ctxt TypeInfo,
160 idris_namehints :: Ctxt [Name],
161 idris_patdefs :: Ctxt ([([Name], Term, Term)], [PTerm]), -- not exported
162 -- ^ list of lhs/rhs, and a list of missing clauses
163 idris_flags :: Ctxt [FnOpt],
164 idris_callgraph :: Ctxt CGInfo, -- name, args used in each pos
165 idris_calledgraph :: Ctxt [Name],
166 idris_docstrings :: Ctxt (Docstring DocTerm, [(Name, Docstring DocTerm)]),
167 idris_tyinfodata :: Ctxt TIData,
168 idris_fninfo :: Ctxt FnInfo,
169 idris_transforms :: Ctxt [(Term, Term)],
170 idris_totcheck :: [(FC, Name)], -- names to check totality on
171 idris_defertotcheck :: [(FC, Name)], -- names to check at the end
172 idris_totcheckfail :: [(FC, String)],
173 idris_options :: IOption,
174 idris_name :: Int,
175 idris_lineapps :: [((FilePath, Int), PTerm)],
176 -- ^ Full application LHS on source line
177 idris_metavars :: [(Name, (Maybe Name, Int, Bool))], -- ^ The currently defined but not proven metavariables
178 idris_coercions :: [Name],
179 idris_errRev :: [(Term, Term)],
180 syntax_rules :: [Syntax],
181 syntax_keywords :: [String],
182 imported :: [FilePath], -- ^ The imported modules
183 idris_scprims :: [(Name, (Int, PrimFn))],
184 idris_objs :: [(Codegen, FilePath)],
185 idris_libs :: [(Codegen, String)],
186 idris_cgflags :: [(Codegen, String)],
187 idris_hdrs :: [(Codegen, String)],
188 idris_imported :: [FilePath], -- ^ Imported ibc file names
189 proof_list :: [(Name, [String])],
190 errSpan :: Maybe FC,
191 parserWarnings :: [(FC, Err)],
192 lastParse :: Maybe Name,
193 indent_stack :: [Int],
194 brace_stack :: [Maybe Int],
195 lastTokenSpan :: Maybe FC, -- ^ What was the span of the latest token parsed?
196 idris_parsedSpan :: Maybe FC,
197 hide_list :: [(Name, Maybe Accessibility)],
198 default_access :: Accessibility,
199 default_total :: Bool,
200 ibc_write :: [IBCWrite],
201 compiled_so :: Maybe String,
202 idris_dynamic_libs :: [DynamicLib],
203 idris_language_extensions :: [LanguageExt],
204 idris_outputmode :: OutputMode,
205 idris_colourRepl :: Bool,
206 idris_colourTheme :: ColourTheme,
207 idris_errorhandlers :: [Name], -- ^ Global error handlers
208 idris_nameIdx :: (Int, Ctxt (Int, Name)),
209 idris_function_errorhandlers :: Ctxt (M.Map Name (S.Set Name)), -- ^ Specific error handlers
210 module_aliases :: M.Map [T.Text] [T.Text],
211 idris_consolewidth :: ConsoleWidth, -- ^ How many chars wide is the console?
212 idris_postulates :: S.Set Name,
213 idris_whocalls :: Maybe (M.Map Name [Name]),
214 idris_callswho :: Maybe (M.Map Name [Name]),
215 idris_repl_defs :: [Name] -- ^ List of names that were defined in the repl, and can be re-/un-defined
216 }
218-- Required for parsers library, and therefore trifecta
219instance Show IState where
220 show = const "{internal state}"
222data SizeChange = Smaller | Same | Bigger | Unknown
223 deriving (Show, Eq)
224{-!
225deriving instance Binary SizeChange
226deriving instance NFData SizeChange
227!-}
229type SCGEntry = (Name, [Maybe (Int, SizeChange)])
230type UsageReason = (Name, Int) -- fn_name, its_arg_number
232data CGInfo = CGInfo { argsdef :: [Name],
233 calls :: [(Name, [[Name]])],
234 scg :: [SCGEntry],
235 argsused :: [Name],
236 usedpos :: [(Int, [UsageReason])] }
237 deriving Show
238{-!
239deriving instance Binary CGInfo
240deriving instance NFData CGInfo
241!-}
243primDefs = [sUN "unsafePerformPrimIO",
244 sUN "mkLazyForeignPrim",
245 sUN "mkForeignPrim",
246 sUN "void"]
248-- information that needs writing for the current module's .ibc file
249data IBCWrite = IBCFix FixDecl
250 | IBCImp Name
251 | IBCStatic Name
252 | IBCClass Name
253 | IBCInstance Bool Name Name
254 | IBCDSL Name
255 | IBCData Name
256 | IBCOpt Name
257 | IBCMetavar Name
258 | IBCSyntax Syntax
259 | IBCKeyword String
260 | IBCImport FilePath
261 | IBCImportDir FilePath
262 | IBCObj Codegen FilePath
263 | IBCLib Codegen String
264 | IBCCGFlag Codegen String
265 | IBCDyLib String
266 | IBCHeader Codegen String
267 | IBCAccess Name Accessibility
268 | IBCMetaInformation Name MetaInformation
269 | IBCTotal Name Totality
270 | IBCFlags Name [FnOpt]
271 | IBCFnInfo Name FnInfo
272 | IBCTrans Name (Term, Term)
273 | IBCErrRev (Term, Term)
274 | IBCCG Name
275 | IBCDoc Name
276 | IBCCoercion Name
277 | IBCDef Name -- i.e. main context
278 | IBCNameHint (Name, Name)
279 | IBCLineApp FilePath Int PTerm
280 | IBCErrorHandler Name
281 | IBCFunctionErrorHandler Name Name Name
282 | IBCPostulate Name
283 | IBCTotCheckErr FC String
284 | IBCParsedRegion FC
285 deriving Show
287-- | The initial state for the compiler
288idrisInit :: IState
289idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext
290 emptyContext emptyContext emptyContext emptyContext
291 emptyContext emptyContext emptyContext emptyContext
292 emptyContext emptyContext emptyContext emptyContext
293 [] [] [] defaultOpts 6 [] [] [] [] [] [] [] [] [] [] [] []
294 [] [] Nothing [] Nothing [] [] Nothing Nothing [] Hidden False [] Nothing [] []
295 (RawOutput stdout) True defaultTheme [] (0, emptyContext) emptyContext M.empty
296 AutomaticWidth S.empty Nothing Nothing []
298-- | The monad for the main REPL - reading and processing files and updating
299-- global state (hence the IO inner monad).
300--type Idris = WriterT [Either String (IO ())] (State IState a))
301type Idris = StateT IState (ErrorT Err IO)
303-- Commands in the REPL
305data Codegen = Via String
306-- | ViaC
307-- | ViaJava
308-- | ViaNode
309-- | ViaJavaScript
310-- | ViaLLVM
311 | Bytecode
312 deriving (Show, Eq)
314-- | REPL commands
315data Command = Quit
316 | Help
317 | Eval PTerm
318 | NewDefn [PDecl] -- ^ Each 'PDecl' should be either a type declaration (at most one) or a clause defining the same name.
319 | Undefine [Name]
320 | Check PTerm
321 | DocStr (Either Name Const)
322 | TotCheck Name
323 | Reload
324 | Load FilePath (Maybe Int) -- up to maximum line number
325 | ChangeDirectory FilePath
326 | ModImport String
327 | Edit
328 | Compile Codegen String
329 | Execute
330 | ExecVal PTerm
331 | Metavars
332 | Prove Name
333 | AddProof (Maybe Name)
334 | RmProof Name
335 | ShowProof Name
336 | Proofs
337 | Universes
338 | LogLvl Int
339 | Spec PTerm
340 | HNF PTerm
341 | TestInline PTerm
342 | Defn Name
343 | Missing Name
344 | DynamicLink FilePath
345 | ListDynamic
346 | Pattelab PTerm
347 | DebugInfo Name
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
375data OutputFmt = HTMLOutput | LaTeXOutput
377data Opt = Filename String
378 | Quiet
379 | NoBanner
380 | ColourREPL Bool
381 | Ideslave
382 | IdeslaveSocket
383 | ShowLibs
384 | ShowLibdir
385 | ShowIncs
386 | NoBasePkgs
387 | NoPrelude
388 | NoBuiltins -- only for the really primitive stuff!
389 | NoREPL
390 | OLogging Int
391 | Output String
392 | TypeCase
393 | TypeInType
394 | DefaultTotal
395 | DefaultPartial
396 | WarnPartial
397 | WarnReach
398 | NoCoverage
399 | ErrContext
400 | ShowImpl
401 | Verbose
402 | Port String -- REPL TCP port
403 | IBCSubDir String
404 | ImportDir String
405 | PkgBuild String
406 | PkgInstall String
407 | PkgClean String
408 | PkgCheck String
409 | PkgREPL String
410 | PkgMkDoc String -- IdrisDoc
411 | PkgTest String
412 | WarnOnly
413 | Pkg String
414 | BCAsm String
415 | DumpDefun String
416 | DumpCases String
417 | UseCodegen Codegen
418 | OutputTy OutputType
419 | Extension LanguageExt
420 | InterpretScript String
421 | EvalExpr String
422 | TargetTriple String
423 | TargetCPU String
424 | OptLevel Int
425 | AddOpt Optimisation
426 | RemoveOpt Optimisation
427 | Client String
428 | ShowOrigErr
429 | AutoWidth -- ^ Automatically adjust terminal width
430 | AutoSolve -- ^ Automatically issue "solve" tactic in interactive prover
431 deriving (Show, Eq)
433-- Parsed declarations
435data Fixity = Infixl { prec :: Int }
436 | Infixr { prec :: Int }
437 | InfixN { prec :: Int }
438 | PrefixN { prec :: Int }
439 deriving Eq
440{-!
441deriving instance Binary Fixity
442deriving instance NFData Fixity
443!-}
445instance Show Fixity where
446 show (Infixl i) = "infixl " ++ show i
447 show (Infixr i) = "infixr " ++ show i
448 show (InfixN i) = "infix " ++ show i
449 show (PrefixN i) = "prefix " ++ show i
451data FixDecl = Fix Fixity String
452 deriving Eq
454instance Show FixDecl where
455 show (Fix f s) = show f ++ " " ++ s
457{-!
458deriving instance Binary FixDecl
459deriving instance NFData FixDecl
460!-}
462instance Ord FixDecl where
463 compare (Fix x _) (Fix y _) = compare (prec x) (prec y)
466data Static = Static | Dynamic
467 deriving (Show, Eq)
468{-!
469deriving instance Binary Static
470deriving instance NFData Static
471!-}
473-- Mark bindings with their explicitness, and laziness
474data Plicity = Imp { pargopts :: [ArgOpt],
475 pstatic :: Static,
476 pparam :: Bool }
477 | Exp { pargopts :: [ArgOpt],
478 pstatic :: Static,
479 pparam :: Bool } -- this is a param (rather than index)
480 | Constraint { pargopts :: [ArgOpt],
481 pstatic :: Static }
482 | TacImp { pargopts :: [ArgOpt],
483 pstatic :: Static,
484 pscript :: PTerm }
485 deriving (Show, Eq)
487{-!
488deriving instance Binary Plicity
489deriving instance NFData Plicity
490!-}
492impl = Imp [] Dynamic False
493expl = Exp [] Dynamic False
494expl_param = Exp [] Dynamic True
495constraint = Constraint [] Static
496tacimpl t = TacImp [] Dynamic t
498data FnOpt = Inlinable -- always evaluate when simplifying
499 | TotalFn | PartialFn | CoveringFn
500 | Coinductive | AssertTotal
501 | Dictionary -- type class dictionary, eval only when
502 -- a function argument, and further evaluation resutls
503 | Implicit -- implicit coercion
504 | NoImplicit -- do not apply implicit coercions
505 | CExport String -- export, with a C name
506 | ErrorHandler -- ^^ an error handler for use with the ErrorReflection extension
507 | ErrorReverse -- ^^ attempt to reverse normalise before showing in error
508 | Reflection -- a reflecting function, compile-time only
509 | Specialise [(Name, Maybe Int)] -- specialise it, freeze these names
510 | Constructor -- Data constructor type
511 deriving (Show, Eq)
512{-!
513deriving instance Binary FnOpt
514deriving instance NFData FnOpt
515!-}
517type FnOpts = [FnOpt]
519inlinable :: FnOpts -> Bool
520inlinable = elem Inlinable
522dictionary :: FnOpts -> Bool
523dictionary = elem Dictionary
526-- | Data declaration options
527data DataOpt = Codata -- ^ Set if the the data-type is coinductive
528 | DefaultEliminator -- ^ Set if an eliminator should be generated for data type
529 | DefaultCaseFun -- ^ Set if a case function should be generated for data type
530 | DataErrRev
531 deriving (Show, Eq)
533type DataOpts = [DataOpt]
535-- | Type provider - what to provide
536data ProvideWhat' t = ProvTerm t t -- ^ the first is the goal type, the second is the term
537 | ProvPostulate t -- ^ goal type must be Type, so only term
538 deriving (Show, Eq, Functor)
540type ProvideWhat = ProvideWhat' PTerm
542-- | Top-level declarations such as compiler directives, definitions,
543-- datatypes and typeclasses.
544data PDecl' t
545 = PFix FC Fixity [String] -- ^ Fixity declaration
546 | PTy (Docstring (Either Err PTerm)) [(Name, Docstring (Either Err PTerm))] SyntaxInfo FC FnOpts Name t -- ^ Type declaration
547 | PPostulate (Docstring (Either Err PTerm)) SyntaxInfo FC FnOpts Name t -- ^ Postulate
548 | PClauses FC FnOpts Name [PClause' t] -- ^ Pattern clause
549 | PCAF FC Name t -- ^ Top level constant
550 | PData (Docstring (Either Err PTerm)) [(Name, Docstring (Either Err PTerm))] SyntaxInfo FC DataOpts (PData' t) -- ^ Data declaration.
551 | PParams FC [(Name, t)] [PDecl' t] -- ^ Params block
552 | PNamespace String [PDecl' t] -- ^ New namespace
553 | PRecord (Docstring (Either Err PTerm)) SyntaxInfo FC Name t DataOpts (Docstring (Either Err PTerm)) Name t -- ^ Record declaration
554 | PClass (Docstring (Either Err PTerm)) SyntaxInfo FC
555 [t] -- constraints
556 Name
557 [(Name, t)] -- parameters
558 [(Name, Docstring (Either Err PTerm))] -- parameter docstrings
559 [PDecl' t] -- declarations
560 -- ^ Type class: arguments are documentation, syntax info, source location, constraints,
561 -- class name, parameters, method declarations
562 | PInstance SyntaxInfo FC [t] -- constraints
563 Name -- class
564 [t] -- parameters
565 t -- full instance type
566 (Maybe Name) -- explicit name
567 [PDecl' t]
568 -- ^ Instance declaration: arguments are syntax info, source location, constraints,
569 -- class name, parameters, full instance type, optional explicit name, and definitions
570 | PDSL Name (DSL' t) -- ^ DSL declaration
571 | PSyntax FC Syntax -- ^ Syntax definition
572 | PMutual FC [PDecl' t] -- ^ Mutual block
573 | PDirective (Idris ()) -- ^ Compiler directive. The parser inserts the corresponding action in the Idris monad.
574 | PProvider SyntaxInfo FC (ProvideWhat' t) Name -- ^ Type provider. The first t is the type, the second is the term
575 | PTransform FC Bool t t -- ^ Source-to-source transformation rule. If
576 -- bool is True, lhs and rhs must be convertible
577 deriving Functor
578{-!
579deriving instance Binary PDecl'
580deriving instance NFData PDecl'
581!-}
583-- For elaborator state
584type ElabD a = Elab' [PDecl] a
586-- | One clause of a top-level definition. Term arguments to constructors are:
587--
588-- 1. The whole application (missing for PClauseR and PWithR because they're within a "with" clause)
589--
590-- 2. The list of extra 'with' patterns
591--
592-- 3. The right-hand side
593--
594-- 4. The where block (PDecl' t)
596data PClause' t = PClause FC Name t [t] t [PDecl' t] -- ^ A normal top-level definition.
597 | PWith FC Name t [t] t [PDecl' t]
598 | PClauseR FC [t] t [PDecl' t]
599 | PWithR FC [t] t [PDecl' t]
600 deriving Functor
601{-!
602deriving instance Binary PClause'
603deriving instance NFData PClause'
604!-}
606-- | Data declaration
607data PData' t = PDatadecl { d_name :: Name, -- ^ The name of the datatype
608 d_tcon :: t, -- ^ Type constructor
609 d_cons :: [(Docstring (Either Err PTerm), [(Name, Docstring (Either Err PTerm))], Name, t, FC, [Name])] -- ^ Constructors
610 }
611 -- ^ Data declaration
612 | PLaterdecl { d_name :: Name, d_tcon :: t }
613 -- ^ "Placeholder" for data whose constructors are defined later
614 deriving Functor
615{-!
616deriving instance Binary PData'
617deriving instance NFData PData'
618!-}
620-- Handy to get a free function for applying PTerm -> PTerm functions
621-- across a program, by deriving Functor
623type PDecl = PDecl' PTerm
624type PData = PData' PTerm
625type PClause = PClause' PTerm
627-- get all the names declared in a decl
629declared :: PDecl -> [Name]
630declared (PFix _ _ _) = []
631declared (PTy _ _ _ _ _ n t) = [n]
632declared (PPostulate _ _ _ _ n t) = [n]
633declared (PClauses _ _ n _) = [] -- not a declaration
634declared (PCAF _ n _) = [n]
635declared (PData _ _ _ _ _ (PDatadecl n _ ts)) = n : map fstt ts
636 where fstt (_, _, a, _, _, _) = a
637declared (PData _ _ _ _ _ (PLaterdecl n _)) = [n]
638declared (PParams _ _ ds) = concatMap declared ds
639declared (PNamespace _ ds) = concatMap declared ds
640declared (PRecord _ _ _ n _ _ _ c _) = [n, c]
641declared (PClass _ _ _ _ n _ _ ms) = n : concatMap declared ms
642declared (PInstance _ _ _ _ _ _ _ _) = []
643declared (PDSL n _) = [n]
644declared (PSyntax _ _) = []
645declared (PMutual _ ds) = concatMap declared ds
646declared (PDirective _) = []
648-- get the names declared, not counting nested parameter blocks
649tldeclared :: PDecl -> [Name]
650tldeclared (PFix _ _ _) = []
651tldeclared (PTy _ _ _ _ _ n t) = [n]
652tldeclared (PPostulate _ _ _ _ n t) = [n]
653tldeclared (PClauses _ _ n _) = [] -- not a declaration
654tldeclared (PRecord _ _ _ n _ _ _ c _) = [n, c]
655tldeclared (PData _ _ _ _ _ (PDatadecl n _ ts)) = n : map fstt ts
656 where fstt (_, _, a, _, _, _) = a
657tldeclared (PParams _ _ ds) = []
658tldeclared (PMutual _ ds) = concatMap tldeclared ds
659tldeclared (PNamespace _ ds) = concatMap tldeclared ds
660tldeclared (PClass _ _ _ _ n _ _ ms) = concatMap tldeclared ms
661tldeclared (PInstance _ _ _ _ _ _ _ _) = []
662tldeclared _ = []
664defined :: PDecl -> [Name]
665defined (PFix _ _ _) = []
666defined (PTy _ _ _ _ _ n t) = []
667defined (PPostulate _ _ _ _ n t) = []
668defined (PClauses _ _ n _) = [n] -- not a declaration
669defined (PCAF _ n _) = [n]
670defined (PData _ _ _ _ _ (PDatadecl n _ ts)) = n : map fstt ts
671 where fstt (_, _, a, _, _, _) = a
672defined (PData _ _ _ _ _ (PLaterdecl n _)) = []
673defined (PParams _ _ ds) = concatMap defined ds
674defined (PNamespace _ ds) = concatMap defined ds
675defined (PRecord _ _ _ n _ _ _ c _) = [n, c]
676defined (PClass _ _ _ _ n _ _ ms) = n : concatMap defined ms
677defined (PInstance _ _ _ _ _ _ _ _) = []
678defined (PDSL n _) = [n]
679defined (PSyntax _ _) = []
680defined (PMutual _ ds) = concatMap defined ds
681defined (PDirective _) = []
682--defined _ = []
684updateN :: [(Name, Name)] -> Name -> Name
685updateN ns n | Just n' <- lookup n ns = n'
686updateN _ n = n
688updateNs :: [(Name, Name)] -> PTerm -> PTerm
689updateNs [] t = t
690updateNs ns t = mapPT updateRef t
691 where updateRef (PRef fc f) = PRef fc (updateN ns f)
692 updateRef t = t
694-- updateDNs :: [(Name, Name)] -> PDecl -> PDecl
695-- updateDNs [] t = t
696-- updateDNs ns (PTy s f n t) | Just n' <- lookup n ns = PTy s f n' t
697-- updateDNs ns (PClauses f n c) | Just n' <- lookup n ns = PClauses f n' (map updateCNs c)
698-- where updateCNs ns (PClause n l ts r ds)
699-- = PClause (updateN ns n) (fmap (updateNs ns) l)
700-- (map (fmap (updateNs ns)) ts)
701-- (fmap (updateNs ns) r)
702-- (map (updateDNs ns) ds)
703-- updateDNs ns c = c
705data PunInfo = IsType | IsTerm | TypeOrTerm deriving (Eq, Show)
707-- | High level language terms
708data PTerm = PQuote Raw -- ^ Inclusion of a core term into the high-level language
709 | PRef FC Name -- ^ A reference to a variable
710 | PInferRef FC Name -- ^ A name to be defined later
711 | PPatvar FC Name -- ^ A pattern variable
712 | PLam Name PTerm PTerm -- ^ A lambda abstraction
713 | PPi Plicity Name PTerm PTerm -- ^ (n : t1) -> t2
714 | PLet Name PTerm PTerm PTerm -- ^ A let binding
715 | PTyped PTerm PTerm -- ^ Term with explicit type
716 | PApp FC PTerm [PArg] -- ^ e.g. IO (), List Char, length x
717 | PAppBind FC PTerm [PArg] -- ^ implicitly bound application
718 | PMatchApp FC Name -- ^ Make an application by type matching
719 | PCase FC PTerm [(PTerm, PTerm)] -- ^ A case expression. Args are source location, scrutinee, and a list of pattern/RHS pairs
720 | PTrue FC PunInfo -- ^ Unit type..?
721 | PRefl FC PTerm -- ^ The canonical proof of the equality type
722 | PResolveTC FC -- ^ Solve this dictionary by type class resolution
723 | PEq FC PTerm PTerm PTerm PTerm -- ^ Heterogeneous equality type: A = B
724 | PRewrite FC PTerm PTerm (Maybe PTerm) -- ^ "rewrite" syntax, with optional result type
725 | PPair FC PunInfo PTerm PTerm -- ^ A pair (a, b) and whether it's a product type or a pair (solved by elaboration)
726 | 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)
727 | PAlternative Bool [PTerm] -- ^ True if only one may work. (| A, B, C|)
728 | PHidden PTerm -- ^ Irrelevant or hidden pattern
729 | PType -- ^ 'Type' type
730 | PUniverse Universe -- ^ Some universe
731 | PGoal FC PTerm Name PTerm -- ^ quoteGoal, used for %reflection functions
732 | PConstant Const -- ^ Builtin types
733 | Placeholder -- ^ Underscore
734 | PDoBlock [PDo] -- ^ Do notation
735 | PIdiom FC PTerm -- ^ Idiom brackets
736 | PReturn FC
737 | PMetavar Name -- ^ A metavariable, ?name
738 | PProof [PTactic] -- ^ Proof script
739 | PTactics [PTactic] -- ^ As PProof, but no auto solving
740 | PElabError Err -- ^ Error to report on elaboration
741 | PImpossible -- ^ Special case for declaring when an LHS can't typecheck
742 | PCoerced PTerm -- ^ To mark a coerced argument, so as not to coerce twice
743 | PDisamb [[T.Text]] PTerm -- ^ Preferences for explicit namespaces
744 | PUnifyLog PTerm -- ^ dump a trace of unifications when building term
745 | PNoImplicits PTerm -- ^ never run implicit converions on the term
746 | PQuasiquote PTerm (Maybe PTerm) -- ^ `(Term [: Term])
747 | PUnquote PTerm -- ^ ,Term
748 deriving Eq
751{-!
752deriving instance Binary PTerm
753deriving instance NFData PTerm
754!-}
756mapPT :: (PTerm -> PTerm) -> PTerm -> PTerm
757mapPT f t = f (mpt t) where
758 mpt (PLam n t s) = PLam n (mapPT f t) (mapPT f s)
759 mpt (PPi p n t s) = PPi p n (mapPT f t) (mapPT f s)
760 mpt (PLet n ty v s) = PLet n (mapPT f ty) (mapPT f v) (mapPT f s)
761 mpt (PRewrite fc t s g) = PRewrite fc (mapPT f t) (mapPT f s)
762 (fmap (mapPT f) g)
763 mpt (PApp fc t as) = PApp fc (mapPT f t) (map (fmap (mapPT f)) as)
764 mpt (PAppBind fc t as) = PAppBind fc (mapPT f t) (map (fmap (mapPT f)) as)
765 mpt (PCase fc c os) = PCase fc (mapPT f c) (map (pmap (mapPT f)) os)
766 mpt (PEq fc lt rt l r) = PEq fc (mapPT f lt) (mapPT f rt) (mapPT f l) (mapPT f r)
767 mpt (PTyped l r) = PTyped (mapPT f l) (mapPT f r)
768 mpt (PPair fc p l r) = PPair fc p (mapPT f l) (mapPT f r)
769 mpt (PDPair fc p l t r) = PDPair fc p (mapPT f l) (mapPT f t) (mapPT f r)
770 mpt (PAlternative a as) = PAlternative a (map (mapPT f) as)
771 mpt (PHidden t) = PHidden (mapPT f t)
772 mpt (PDoBlock ds) = PDoBlock (map (fmap (mapPT f)) ds)
773 mpt (PProof ts) = PProof (map (fmap (mapPT f)) ts)
774 mpt (PTactics ts) = PTactics (map (fmap (mapPT f)) ts)
775 mpt (PUnifyLog tm) = PUnifyLog (mapPT f tm)
776 mpt (PDisamb ns tm) = PDisamb ns (mapPT f tm)
777 mpt (PNoImplicits tm) = PNoImplicits (mapPT f tm)
778 mpt (PGoal fc r n sc) = PGoal fc (mapPT f r) n (mapPT f sc)
779 mpt x = x
782data PTactic' t = Intro [Name] | Intros | Focus Name
783 | Refine Name [Bool] | Rewrite t | DoUnify
784 | Induction t
785 | CaseTac t
786 | Equiv t
787 | MatchRefine Name
788 | LetTac Name t | LetTacTy Name t t
789 | Exact t | Compute | Trivial | TCInstance
790 | ProofSearch Bool Bool Int (Maybe Name) [Name]
791 -- ^ the bool is whether to search recursively
792 | Solve
793 | Attack
794 | ProofState | ProofTerm | Undo
795 | Try (PTactic' t) (PTactic' t)
796 | TSeq (PTactic' t) (PTactic' t)
797 | ApplyTactic t -- see Language.Reflection module
798 | ByReflection t
799 | Reflect t
800 | Fill t
801 | GoalType String (PTactic' t)
802 | TCheck t
803 | TEval t
804 | TDocStr (Either Name Const)
805 | TSearch t
806 | Skip
807 | TFail [ErrorReportPart]
808 | Qed | Abandon
809 deriving (Show, Eq, Functor, Foldable, Traversable)
810{-!
811deriving instance Binary PTactic'
812deriving instance NFData PTactic'
813!-}
814instance Sized a => Sized (PTactic' a) where
815 size (Intro nms) = 1 + size nms
816 size Intros = 1
817 size (Focus nm) = 1 + size nm
818 size (Refine nm bs) = 1 + size nm + length bs
819 size (Rewrite t) = 1 + size t
820 size (Induction t) = 1 + size t
821 size (LetTac nm t) = 1 + size nm + size t
822 size (Exact t) = 1 + size t
823 size Compute = 1
824 size Trivial = 1
825 size Solve = 1
826 size Attack = 1
827 size ProofState = 1
828 size ProofTerm = 1
829 size Undo = 1
830 size (Try l r) = 1 + size l + size r
831 size (TSeq l r) = 1 + size l + size r
832 size (ApplyTactic t) = 1 + size t
833 size (Reflect t) = 1 + size t
834 size (Fill t) = 1 + size t
835 size Qed = 1
836 size Abandon = 1
837 size Skip = 1
838 size (TFail ts) = 1 + size ts
840type PTactic = PTactic' PTerm
842data PDo' t = DoExp FC t
843 | DoBind FC Name t
844 | DoBindP FC t t [(t,t)]
845 | DoLet FC Name t t
846 | DoLetP FC t t
847 deriving (Eq, Functor)
848{-!
849deriving instance Binary PDo'
850deriving instance NFData PDo'
851!-}
853instance Sized a => Sized (PDo' a) where
854 size (DoExp fc t) = 1 + size fc + size t
855 size (DoBind fc nm t) = 1 + size fc + size nm + size t
856 size (DoBindP fc l r alts) = 1 + size fc + size l + size r + size alts
857 size (DoLet fc nm l r) = 1 + size fc + size nm + size l + size r
858 size (DoLetP fc l r) = 1 + size fc + size l + size r
860type PDo = PDo' PTerm
862-- The priority gives a hint as to elaboration order. Best to elaborate
863-- things early which will help give a more concrete type to other
864-- variables, e.g. a before (interpTy a).
866data PArg' t = PImp { priority :: Int,
867 machine_inf :: Bool, -- true if the machine inferred it
868 argopts :: [ArgOpt],
869 pname :: Name, getTm :: t }
870 | PExp { priority :: Int,
871 argopts :: [ArgOpt],
872 pname :: Name,
873 getTm :: t }
874 | PConstraint { priority :: Int,
875 argopts :: [ArgOpt],
876 pname :: Name,
877 getTm :: t }
878 | PTacImplicit { priority :: Int,
879 argopts :: [ArgOpt],
880 pname :: Name,
881 getScript :: t,
882 getTm :: t }
883 deriving (Show, Eq, Functor)
885data ArgOpt = AlwaysShow | HideDisplay | InaccessibleArg
886 deriving (Show, Eq)
888instance Sized a => Sized (PArg' a) where
889 size (PImp p _ l nm trm) = 1 + size nm + size trm
890 size (PExp p l nm trm) = 1 + size nm + size trm
891 size (PConstraint p l nm trm) = 1 + size nm +size nm + size trm
892 size (PTacImplicit p l nm scr trm) = 1 + size nm + size scr + size trm
894{-!
895deriving instance Binary PArg'
896deriving instance NFData PArg'
897!-}
899pimp n t mach = PImp 1 mach [] n t
900pexp t = PExp 1 [] (sMN 0 "arg") t
901pconst t = PConstraint 1 [] (sMN 0 "carg") t
902ptacimp n s t = PTacImplicit 2 [] n s t
904type PArg = PArg' PTerm
906-- Type class data
908data ClassInfo = CI { instanceName :: Name,
909 class_methods :: [(Name, (FnOpts, PTerm))],
910 class_defaults :: [(Name, (Name, PDecl))], -- method name -> default impl
911 class_default_superclasses :: [PDecl],
912 class_params :: [Name],
913 class_instances :: [Name] }
914 deriving Show
915{-!
916deriving instance Binary ClassInfo
917deriving instance NFData ClassInfo
918!-}
920-- Type inference data
922data TIData = TIPartial -- ^ a function with a partially defined type
923 | TISolution [Term] -- ^ possible solutions to a metavariable in a type
924 deriving Show
926-- | Miscellaneous information about functions
927data FnInfo = FnInfo { fn_params :: [Int] }
928 deriving Show
929{-!
930deriving instance Binary FnInfo
931!-}
933data OptInfo = Optimise { inaccessible :: [(Int,Name)], -- includes names for error reporting
934 detaggable :: Bool }
935 deriving Show
936{-!
937deriving instance Binary OptInfo
938deriving instance NFData OptInfo
939!-}
942data TypeInfo = TI { con_names :: [Name],
943 codata :: Bool,
944 data_opts :: DataOpts,
945 param_pos :: [Int],
946 mutual_types :: [Name] }
947 deriving Show
948{-!
949deriving instance Binary TypeInfo
950deriving instance NFData TypeInfo
951!-}
953-- Syntactic sugar info
955data DSL' t = DSL { dsl_bind :: t,
956 dsl_return :: t,
957 dsl_apply :: t,
958 dsl_pure :: t,
959 dsl_var :: Maybe t,
960 index_first :: Maybe t,
961 index_next :: Maybe t,
962 dsl_lambda :: Maybe t,
963 dsl_let :: Maybe t,
964 dsl_pi :: Maybe t
965 }
966 deriving (Show, Functor)
967{-!
968deriving instance Binary DSL'
969deriving instance NFData DSL'
970!-}
972type DSL = DSL' PTerm
974data SynContext = PatternSyntax | TermSyntax | AnySyntax
975 deriving Show
976{-!
977deriving instance Binary SynContext
978deriving instance NFData SynContext
979!-}
981data Syntax = Rule [SSymbol] PTerm SynContext
982 deriving Show
984syntaxNames :: Syntax -> [Name]
985syntaxNames (Rule syms _ _) = mapMaybe ename syms
986 where ename (Keyword n) = Just n
987 ename _ = Nothing
988{-!
989deriving instance Binary Syntax
990deriving instance NFData Syntax
991!-}
993data SSymbol = Keyword Name
994 | Symbol String
995 | Binding Name
996 | Expr Name
997 | SimpleExpr Name
998 deriving Show
1001{-!
1002deriving instance Binary SSymbol
1003deriving instance NFData SSymbol
1004!-}
1006initDSL = DSL (PRef f (sUN ">>="))
1007 (PRef f (sUN "return"))
1008 (PRef f (sUN "<$>"))
1009 (PRef f (sUN "pure"))
1010 Nothing
1011 Nothing
1012 Nothing
1013 Nothing
1014 Nothing
1015 Nothing
1016 where f = fileFC "(builtin)"
1018data Using = UImplicit Name PTerm
1019 | UConstraint Name [Name]
1020 deriving (Show, Eq)
1021{-!
1022deriving instance Binary Using
1023deriving instance NFData Using
1024!-}
1026data SyntaxInfo = Syn { using :: [Using],
1027 syn_params :: [(Name, PTerm)],
1028 syn_namespace :: [String],
1029 no_imp :: [Name],
1030 decoration :: Name -> Name,
1031 inPattern :: Bool,
1032 implicitAllowed :: Bool,
1033 maxline :: Maybe Int,
1034 mut_nesting :: Int,
1035 dsl_info :: DSL,
1036 syn_in_quasiquote :: Int }
1037 deriving Show
1038{-!
1039deriving instance NFData SyntaxInfo
1040deriving instance Binary SyntaxInfo
1041!-}
1043defaultSyntax = Syn [] [] [] [] id False False Nothing 0 initDSL 0
1045expandNS :: SyntaxInfo -> Name -> Name
1046expandNS syn n@(NS _ _) = n
1047expandNS syn n = case syn_namespace syn of
1048 [] -> n
1049 xs -> sNS n xs
1052-- For inferring types of things
1054bi = fileFC "builtin"
1056inferTy = sMN 0 "__Infer"
1057inferCon = sMN 0 "__infer"
1058inferDecl = PDatadecl inferTy
1059 PType
1060 [(emptyDocstring, [], inferCon, PPi impl (sMN 0 "iType") PType (
1061 PPi expl (sMN 0 "ival") (PRef bi (sMN 0 "iType"))
1062 (PRef bi inferTy)), bi, [])]
1063inferOpts = []
1065infTerm t = PApp bi (PRef bi inferCon) [pimp (sMN 0 "iType") Placeholder True, pexp t]
1066infP = P (TCon 6 0) inferTy (TType (UVal 0))
1068getInferTerm, getInferType :: Term -> Term
1069getInferTerm (Bind n b sc) = Bind n b $ getInferTerm sc
1070getInferTerm (App (App _ _) tm) = tm
1071getInferTerm tm = tm -- error ("getInferTerm " ++ show tm)
1073getInferType (Bind n b sc) = Bind n (toTy b) $ getInferType sc
1074 where toTy (Lam t) = Pi t (TType (UVar 0))
1075 toTy (PVar t) = PVTy t
1076 toTy b = b
1077getInferType (App (App _ ty) _) = ty
1081-- Handy primitives: Unit, False, Pair, MkPair, =, mkForeign
1083primNames = [eqTy, eqCon, inferTy, inferCon]
1085unitTy = sUN "Unit"
1086unitCon = sUN "MkUnit"
1088-- TODO: elaborate the code samples in the docstring
1089falseDoc = fmap (const $ Msg "") . parseDocstring . T.pack $
1090 "The empty type, also known as the trivially false proposition." ++
1091 "\n\n" ++
1092 "Use `void` or `absurd` to prove anything if you have a variable " ++
1093 "of type `Void` in scope."
1094falseTy = sUN "Void"
1096pairTy = sUN "Pair"
1097pairCon = sUN "MkPair"
1099eqTy = sUN "="
1100eqCon = sUN "Refl"
1101eqDoc = fmap (const (Left $ Msg "")) . parseDocstring . T.pack $
1102 "The propositional equality type. A proof that `x` = `y`." ++
1103 "\n\n" ++
1104 "To use such a proof, pattern-match on it, and the two equal things will " ++
1105 "then need to be the _same_ pattern." ++
1106 "\n\n" ++
1107 "**Note**: Idris's equality type is potentially _heterogeneous_, which means that it " ++
1108 "is possible to state equalities between values of potentially different " ++
1109 "types. However, Idris will attempt the homogeneous case unless it fails to typecheck." ++
1110 "\n\n" ++
1111 "You may need to use `(~=~)` to explicitly request heterogeneous equality."
1113eqDecl = PDatadecl eqTy (piBindp impl [(n "A", PType), (n "B", PType)]
1114 (piBind [(n "x", PRef bi (n "A")), (n "y", PRef bi (n "B"))]
1115 PType))
1116 [(reflDoc, reflParamDoc,
1117 eqCon, PPi impl (n "A") PType (
1118 PPi impl (n "x") (PRef bi (n "A"))
1119 (PApp bi (PRef bi eqTy) [pimp (n "A") Placeholder False,
1120 pimp (n "B") Placeholder False,
1121 pexp (PRef bi (n "x")),
1122 pexp (PRef bi (n "x"))])), bi, [])]
1123 where n a = sUN a
1124 reflDoc = annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $
1125 "A proof that `x` in fact equals `x`. To construct this, you must have already " ++
1126 "shown that both sides are in fact equal."
1127 reflParamDoc = [(n "A", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the type at which the equality is proven"),
1128 (n "x", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the element shown to be equal to itself.")]
1130eqParamDoc = [(n "A", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the type of the left side of the equality"),
1131 (n "B", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the type of the right side of the equality")
1133 where n a = sUN a
1135eqOpts = []
1137-- Defined in builtins.idr
1138sigmaTy = sUN "Sigma"
1139existsCon = sUN "MkSigma"
1141piBind :: [(Name, PTerm)] -> PTerm -> PTerm
1142piBind = piBindp expl
1144piBindp :: Plicity -> [(Name, PTerm)] -> PTerm -> PTerm
1145piBindp p [] t = t
1146piBindp p ((n, ty):ns) t = PPi p n ty (piBindp p ns t)
1149-- Pretty-printing declarations and terms
1151-- These "show" instances render to an absurdly wide screen because inserted line breaks
1152-- could interfere with interactive editing, which calls "show".
1154instance Show PTerm where
1155 showsPrec _ tm = (displayS . renderPretty 1.0 10000000 . prettyImp defaultPPOption) tm
1157instance Show PDecl where
1158 showsPrec _ d = (displayS . renderPretty 1.0 10000000 . showDeclImp verbosePPOption) d
1160instance Show PClause where
1161 showsPrec _ c = (displayS . renderPretty 1.0 10000000 . showCImp verbosePPOption) c
1163instance Show PData where
1164 showsPrec _ d = (displayS . renderPretty 1.0 10000000 . showDImp defaultPPOption) d
1166instance Pretty PTerm OutputAnnotation where
1167 pretty = prettyImp defaultPPOption
1169-- | Colourise annotations according to an Idris state. It ignores the names
1170-- in the annotation, as there's no good way to show extended information on a
1171-- terminal.
1172consoleDecorate :: IState -> OutputAnnotation -> String -> String
1173consoleDecorate ist _ | not (idris_colourRepl ist) = id
1174consoleDecorate ist (AnnConst c) = let theme = idris_colourTheme ist
1175 in if constIsType c
1176 then colouriseType theme
1177 else colouriseData theme
1178consoleDecorate ist (AnnData _ _) = colouriseData (idris_colourTheme ist)
1179consoleDecorate ist (AnnType _ _) = colouriseType (idris_colourTheme ist)
1180consoleDecorate ist (AnnBoundName _ True) = colouriseImplicit (idris_colourTheme ist)
1181consoleDecorate ist (AnnBoundName _ False) = colouriseBound (idris_colourTheme ist)
1182consoleDecorate ist AnnKeyword = colouriseKeyword (idris_colourTheme ist)
1183consoleDecorate ist (AnnName n _ _ _) = let ctxt = tt_ctxt ist
1184 theme = idris_colourTheme ist
1185 in case () of
1186 _ | isDConName n ctxt -> colouriseData theme
1187 _ | isFnName n ctxt -> colouriseFun theme
1188 _ | isTConName n ctxt -> colouriseType theme
1189 _ | isPostulateName n ist -> colourisePostulate theme
1190 _ | otherwise -> id -- don't colourise unknown names
1191consoleDecorate ist (AnnFC _) = id
1192consoleDecorate ist (AnnTextFmt fmt) = Idris.Colours.colourise (colour fmt)
1193 where colour BoldText = IdrisColour Nothing True False True False
1194 colour UnderlineText = IdrisColour Nothing True True False False
1195 colour ItalicText = IdrisColour Nothing True False False True
1196consoleDecorate ist (AnnTerm _ _) = id
1197consoleDecorate ist (AnnSearchResult _) = id
1198consoleDecorate ist (AnnErr _) = id
1200isPostulateName :: Name -> IState -> Bool
1201isPostulateName n ist = S.member n (idris_postulates ist)
1203-- | Pretty-print a high-level closed Idris term with no information about precedence/associativity
1204prettyImp :: PPOption -- ^^ pretty printing options
1205 -> PTerm -- ^^ the term to pretty-print
1206 -> Doc OutputAnnotation
1207prettyImp impl = pprintPTerm impl [] [] []
1209-- | Serialise something to base64 using its Binary instance.
1211-- | Do the right thing for rendering a term in an IState
1212prettyIst :: IState -> PTerm -> Doc OutputAnnotation
1213prettyIst ist = pprintPTerm (ppOptionIst ist) [] [] (idris_infixes ist)
1215-- | Pretty-print a high-level Idris term in some bindings context with infix info
1216pprintPTerm :: PPOption -- ^^ pretty printing options
1217 -> [(Name, Bool)] -- ^^ the currently-bound names and whether they are implicit
1218 -> [Name] -- ^^ names to always show in pi, even if not used
1219 -> [FixDecl] -- ^^ Fixity declarations
1220 -> PTerm -- ^^ the term to pretty-print
1221 -> Doc OutputAnnotation
1222pprintPTerm ppo bnd docArgs infixes = prettySe 10 bnd
1223 where
1224 prettySe :: Int -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation
1225 prettySe p bnd (PQuote r) =
1226 text "![" <> pretty r <> text "]"
1227 prettySe p bnd (PPatvar fc n) = pretty n
1228 prettySe p bnd e
1229 | Just str <- slist p bnd e = str
1230 | Just n <- snat p e = annotate (AnnData "Nat" "") (text (show n))
1231 prettySe p bnd (PRef fc n) = prettyName True (ppopt_impl ppo) bnd n
1232 prettySe p bnd (PLam n ty sc) =
1233 bracket p 2 . group . align . hang 2 $
1234 text "\\" <> bindingOf n False <+> text "=>" <$>
1235 prettySe 10 ((n, False):bnd) sc
1236 prettySe p bnd (PLet n ty v sc) =
1237 bracket p 2 . group . align $
1238 kwd "let" <+> (group . align . hang 2 $ bindingOf n False <+> text "=" <$> prettySe 10 bnd v) </>
1239 kwd "in" <+> (group . align . hang 2 $ prettySe 10 ((n, False):bnd) sc)
1240 prettySe p bnd (PPi (Exp l s _) n ty sc)
1241 | n `elem` allNamesIn sc || ppopt_impl ppo || n `elem` docArgs =
1242 bracket p 2 . group $
1243 enclose lparen rparen (group . align $ bindingOf n False <+> colon <+> prettySe 10 bnd ty) <+>
1244 st <> text "->" <$> prettySe 10 ((n, False):bnd) sc
1245 | otherwise =
1246 bracket p 2 . group $
1247 group (prettySe 1 bnd ty <+> st) <> text "->" <$> group (prettySe 10 ((n, False):bnd) sc)
1248 where
1249 st =
1250 case s of
1251 Static -> text "[static]" <> space
1252 _ -> empty
1253 prettySe p bnd (PPi (Imp l s _) n ty sc)
1254 | ppopt_impl ppo =
1255 bracket p 2 $
1256 lbrace <> bindingOf n True <+> colon <+> prettySe 10 bnd ty <> rbrace <+>
1257 st <> text "->" </> prettySe 10 ((n, True):bnd) sc
1258 | otherwise = prettySe 10 ((n, True):bnd) sc
1259 where
1260 st =
1261 case s of
1262 Static -> text "[static]" <> space
1263 _ -> empty
1264 prettySe p bnd (PPi (Constraint _ _) n ty sc) =
1265 bracket p 2 $
1266 prettySe 10 bnd ty <+> text "=>" </> prettySe 10 ((n, True):bnd) sc
1267 prettySe p bnd (PPi (TacImp _ _ s) n ty sc) =
1268 bracket p 2 $
1269 lbrace <> kwd "tacimp" <+> pretty n <+> colon <+> prettySe 10 bnd ty <>
1270 rbrace <+> text "->" </> prettySe 10 ((n, True):bnd) sc
1271 prettySe p bnd (PApp _ (PRef _ f) args) -- normal names, no explicit args
1272 | UN nm <- basename f
1273 , not (ppopt_impl ppo) && null (getShowArgs args) =
1274 prettyName True (ppopt_impl ppo) bnd f
1275 prettySe p bnd (PAppBind _ (PRef _ f) [])
1276 | not (ppopt_impl ppo) = text "!" <> prettyName True (ppopt_impl ppo) bnd f
1277 prettySe p bnd (PApp _ (PRef _ op) args) -- infix operators
1278 | UN nm <- basename op
1279 , not (tnull nm) &&
1280 (not (ppopt_impl ppo)) && (not $ isAlpha (thead nm)) =
1281 case getShowArgs args of
1282 [] -> opName True
1283 [x] -> group (opName True <$> group (prettySe 0 bnd (getTm x)))
1284 [l,r] -> let precedence = fromMaybe 20 (fmap prec f)
1285 in bracket p precedence $ inFix (getTm l) (getTm r)
1286 (l@(PExp _ _ _ _) : r@(PExp _ _ _ _) : rest) ->
1287 bracket p 1 $
1288 enclose lparen rparen (inFix (getTm l) (getTm r)) <+>
1289 align (group (vsep (map (prettyArgS bnd) rest)))
1290 as -> opName True <+> align (vsep (map (prettyArgS bnd) as))
1291 where opName isPrefix = prettyName isPrefix (ppopt_impl ppo) bnd op
1292 f = getFixity (opStr op)
1293 left l = case f of
1294 Nothing -> prettySe (-1) bnd l
1295 Just (Infixl p') -> prettySe p' bnd l
1296 Just f' -> prettySe (prec f'-1) bnd l
1297 right r = case f of
1298 Nothing -> prettySe (-1) bnd r
1299 Just (Infixr p') -> prettySe p' bnd r
1300 Just f' -> prettySe (prec f'-1) bnd r
1301 inFix l r = align . group $
1302 (left l <+> opName False) <$> group (right r)
1303 prettySe p bnd (PApp _ hd@(PRef fc f) [tm]) -- symbols, like 'foo
1304 | PConstant (Idris.Core.TT.Str str) <- getTm tm,
1305 f == sUN "Symbol_" = annotate (AnnType ("'" ++ str) ("The symbol " ++ str)) $
1306 char '\'' <> prettySe 10 bnd (PRef fc (sUN str))
1307 prettySe p bnd (PApp _ f as) = -- Normal prefix applications
1308 let args = getShowArgs as
1309 fp = prettySe 1 bnd f
1310 in
1311 bracket p 1 . group $
1312 if ppopt_impl ppo
1313 then if null as
1314 then fp
1315 else fp <+> align (vsep (map (prettyArgS bnd) as))
1316 else if null args
1317 then fp
1318 else fp <+> align (vsep (map (prettyArgS bnd) args))
1319 prettySe p bnd (PCase _ scr opts) =
1320 kwd "case" <+> prettySe 10 bnd scr <+> kwd "of" <> prettyBody
1321 where
1322 prettyBody = foldr (<>) empty $ intersperse (text "|") $ map sc opts
1324 sc (l, r) = nest nestingSize $ prettySe 10 bnd l <+> text "=>" <+> prettySe 10 bnd r
1325 prettySe p bnd (PHidden tm) = text "." <> prettySe 0 bnd tm
1326 prettySe p bnd (PRefl _ _) = annName eqCon $ text "Refl"
1327 prettySe p bnd (PResolveTC _) = text "resolvetc"
1328 prettySe p bnd (PTrue _ IsType) = annName unitTy $ text "()"
1329 prettySe p bnd (PTrue _ IsTerm) = annName unitCon $ text "()"
1330 prettySe p bnd (PTrue _ TypeOrTerm) = text "()"
1331 prettySe p bnd (PEq _ lt rt l r)
1332 | ppopt_impl ppo =
1333 bracket p 1 $
1334 enclose lparen rparen eq <+>
1335 align (group (vsep (map (prettyArgS bnd)
1336 [PImp 0 False [] (sUN "A") lt,
1337 PImp 0 False [] (sUN "B") rt,
1338 PExp 0 [] (sUN "x") l,
1339 PExp 0 [] (sUN "y") r])))
1340 | otherwise =
1341 bracket p 2 . align . group $
1342 prettySe 10 bnd l <+> eq <$> group (prettySe 10 bnd r)
1343 where eq = annName eqTy (text "=")
1344 prettySe p bnd (PRewrite _ l r _) =
1345 bracket p 2 $
1346 text "rewrite" <+> prettySe 10 bnd l <+> text "in" <+> prettySe 10 bnd r
1347 prettySe p bnd (PTyped l r) =
1348 lparen <> prettySe 10 bnd l <+> colon <+> prettySe 10 bnd r <> rparen
1349 prettySe p bnd pair@(PPair _ pun _ _) -- flatten tuples to the right, like parser
1350 | Just elts <- pairElts pair = enclose (ann lparen) (ann rparen) .
1351 align . group . vsep . punctuate (ann comma) $
1352 map (prettySe 10 bnd) elts
1353 where ann = case pun of
1354 TypeOrTerm -> id
1355 IsType -> annName pairTy
1356 IsTerm -> annName pairCon
1357 prettySe p bnd (PDPair _ TypeOrTerm l t r) =
1358 lparen <> prettySe 10 bnd l <+> text "**" <+> prettySe 10 bnd r <> rparen
1359 prettySe p bnd (PDPair _ IsType (PRef _ n) t r) =
1360 annName sigmaTy lparen <>
1361 bindingOf n False <+>
1362 annName sigmaTy (text "**") <+>
1363 prettySe 10 ((n, False):bnd) r <>
1364 annName sigmaTy rparen
1365 prettySe p bnd (PDPair _ IsType l t r) =
1366 annName sigmaTy lparen <>
1367 prettySe 10 bnd l <+>
1368 annName sigmaTy (text "**") <+>
1369 prettySe 10 bnd r <>
1370 annName sigmaTy rparen
1371 prettySe p bnd (PDPair _ IsTerm l t r) =
1372 annName existsCon lparen <>
1373 prettySe 10 bnd l <+>
1374 annName existsCon (text "**") <+>
1375 prettySe 10 bnd r <>
1376 annName existsCon rparen
1377 prettySe p bnd (PAlternative a as) =
1378 lparen <> text "|" <> prettyAs <> text "|" <> rparen
1379 where
1380 prettyAs =
1381 foldr (\l -> \r -> l <+> text "," <+> r) empty $ map (prettySe 10 bnd) as
1382 prettySe p bnd PType = annotate (AnnType "Type" "The type of types") $ text "Type"
1383 prettySe p bnd (PUniverse u) = annotate (AnnType (show u) "The type of unique types") $ text (show u)
1384 prettySe p bnd (PConstant c) = annotate (AnnConst c) (text (show c))
1385 -- XXX: add pretty for tactics
1386 prettySe p bnd (PProof ts) =
1387 text "proof" <+> lbrace <> nest nestingSize (text . show $ ts) <> rbrace
1388 prettySe p bnd (PTactics ts) =
1389 text "tactics" <+> lbrace <> nest nestingSize (text . show $ ts) <> rbrace
1390 prettySe p bnd (PMetavar n) = text "?" <> pretty n
1391 prettySe p bnd (PReturn f) = kwd "return"
1392 prettySe p bnd PImpossible = kwd "impossible"
1393 prettySe p bnd Placeholder = text "_"
1394 prettySe p bnd (PDoBlock _) = text "do block pretty not implemented"
1395 prettySe p bnd (PCoerced t) = prettySe p bnd t
1396 prettySe p bnd (PElabError s) = pretty s
1397 -- Quasiquote pprinting ignores bound vars
1398 prettySe p bnd (PQuasiquote t Nothing) = text "`(" <> prettySe p [] t <> text ")"
1399 prettySe p bnd (PQuasiquote t (Just g)) = text "`(" <> prettySe p [] t <+> colon <+> prettySe p [] g <> text ")"
1400 prettySe p bnd (PUnquote t) = text "~" <> prettySe p bnd t
1402 prettySe p bnd _ = text "missing pretty-printer for term"
1404 prettyArgS bnd (PImp _ _ _ n tm) = prettyArgSi bnd (n, tm)
1405 prettyArgS bnd (PExp _ _ _ tm) = prettyArgSe bnd tm
1406 prettyArgS bnd (PConstraint _ _ _ tm) = prettyArgSc bnd tm
1407 prettyArgS bnd (PTacImplicit _ _ n _ tm) = prettyArgSti bnd (n, tm)
1409 prettyArgSe bnd arg = prettySe 0 bnd arg
1410 prettyArgSi bnd (n, val) = lbrace <> pretty n <+> text "=" <+> prettySe 10 bnd val <> rbrace
1411 prettyArgSc bnd val = lbrace <> lbrace <> prettySe 10 bnd val <> rbrace <> rbrace
1412 prettyArgSti bnd (n, val) = lbrace <> kwd "auto" <+> pretty n <+> text "=" <+> prettySe 10 bnd val <> rbrace
1414 annName :: Name -> Doc OutputAnnotation -> Doc OutputAnnotation
1415 annName n = annotate (AnnName n Nothing Nothing Nothing)
1417 opStr :: Name -> String
1418 opStr (NS n _) = opStr n
1419 opStr (UN n) = T.unpack n
1421 basename :: Name -> Name
1422 basename (NS n _) = basename n
1423 basename n = n
1425 slist' p bnd (PApp _ (PRef _ nil) _)
1426 | not (ppopt_impl ppo) && nsroot nil == sUN "Nil" = Just []
1427 slist' p bnd (PRef _ nil)
1428 | not (ppopt_impl ppo) && nsroot nil == sUN "Nil" = Just []
1429 slist' p bnd (PApp _ (PRef _ cons) args)
1430 | nsroot cons == sUN "::",
1431 (PExp {getTm=tl}):(PExp {getTm=hd}):imps <- reverse args,
1432 all isImp imps,
1433 Just tl' <- slist' p bnd tl
1434 = Just (hd:tl')
1435 where
1436 isImp (PImp {}) = True
1437 isImp _ = False
1438 slist' _ _ tm = Nothing
1440 slist p bnd e | Just es <- slist' p bnd e = Just $
1441 case es of [] -> annotate (AnnData "" "") $ text "[]"
1442 [x] -> enclose left right . group $
1443 prettySe p bnd x
1444 xs -> (enclose left right .
1445 align . group . vsep .
1446 punctuate comma .
1447 map (prettySe p bnd)) xs
1448 where left = (annotate (AnnData "" "") (text "["))
1449 right = (annotate (AnnData "" "") (text "]"))
1450 comma = (annotate (AnnData "" "") (text ","))
1451 slist _ _ _ = Nothing
1453 pairElts :: PTerm -> Maybe [PTerm]
1454 pairElts (PPair _ _ x y) | Just elts <- pairElts y = Just (x:elts)
1455 | otherwise = Just [x, y]
1456 pairElts _ = Nothing
1458 natns = "Prelude.Nat."
1460 snat p (PRef _ z)
1461 | show z == (natns++"Z") || show z == "Z" = Just 0
1462 snat p (PApp _ s [PExp {getTm=n}])
1463 | show s == (natns++"S") || show s == "S",
1464 Just n' <- snat p n
1465 = Just $ 1 + n'
1466 snat _ _ = Nothing
1468 bracket outer inner doc
1469 | inner > outer = lparen <> doc <> rparen
1470 | otherwise = doc
1472 kwd = annotate AnnKeyword . text
1474 fixities :: M.Map String Fixity
1475 fixities = M.fromList [(s, f) | (Fix f s) <- infixes]
1477 getFixity :: String -> Maybe Fixity
1478 getFixity = flip M.lookup fixities
1480-- | Pretty-printer helper for the binding site of a name
1481bindingOf :: Name -- ^^ the bound name
1482 -> Bool -- ^^ whether the name is implicit
1483 -> Doc OutputAnnotation
1484bindingOf n imp = annotate (AnnBoundName n imp) (text (show n))
1486-- | Pretty-printer helper for names that attaches the correct annotations
1487prettyName
1488 :: Bool -- ^^ whether the name should be parenthesised if it is an infix operator
1489 -> Bool -- ^^ whether to show namespaces
1490 -> [(Name, Bool)] -- ^^ the current bound variables and whether they are implicit
1491 -> Name -- ^^ the name to pprint
1492 -> Doc OutputAnnotation
1493prettyName infixParen showNS bnd n
1494 | Just imp <- lookup n bnd = annotate (AnnBoundName n imp) fullName
1495 | otherwise = annotate (AnnName n Nothing Nothing Nothing) fullName
1496 where fullName = text nameSpace <> parenthesise (text (baseName n))
1497 baseName (UN n) = T.unpack n
1498 baseName (NS n ns) = baseName n
1499 baseName (MN i s) = T.unpack s
1500 baseName other = show other
1501 nameSpace = case n of
1502 (NS n' ns) -> if showNS then (concatMap (++ ".") . map T.unpack . reverse) ns else ""
1503 _ -> ""
1504 isInfix = case baseName n of
1505 "" -> False
1506 (c : _) -> not (isAlpha c)
1507 parenthesise = if isInfix && infixParen then enclose lparen rparen else id
1510showCImp :: PPOption -> PClause -> Doc OutputAnnotation
1511showCImp ppo (PClause _ n l ws r w)
1512 = prettyImp ppo l <+> showWs ws <+> text "=" <+> prettyImp ppo r
1513 <+> text "where" <+> text (show w)
1514 where
1515 showWs [] = empty
1516 showWs (x : xs) = text "|" <+> prettyImp ppo x <+> showWs xs
1517showCImp ppo (PWith _ n l ws r w)
1518 = prettyImp ppo l <+> showWs ws <+> text "with" <+> prettyImp ppo r
1519 <+> braces (text (show w))
1520 where
1521 showWs [] = empty
1522 showWs (x : xs) = text "|" <+> prettyImp ppo x <+> showWs xs
1525showDImp :: PPOption -> PData -> Doc OutputAnnotation
1526showDImp ppo (PDatadecl n ty cons)
1527 = text "data" <+> text (show n) <+> colon <+> prettyImp ppo ty <+> text "where" <$>
1528 (indent 2 $ vsep (map (\ (_, _, n, t, _, _) -> pipe <+> prettyName True False [] n <+> colon <+> prettyImp ppo t) cons))
1530showDecls :: PPOption -> [PDecl] -> Doc OutputAnnotation
1531showDecls o ds = vsep (map (showDeclImp o) ds)
1533showDeclImp _ (PFix _ f ops) = text (show f) <+> cat (punctuate (text ",") (map text ops))
1534showDeclImp o (PTy _ _ _ _ _ n t) = text "tydecl" <+> text (showCG n) <+> colon <+> prettyImp o t
1535showDeclImp o (PClauses _ _ n cs) = text "pat" <+> text (showCG n) <+> text "\t" <+>
1536 indent 2 (vsep (map (showCImp o) cs))
1537showDeclImp o (PData _ _ _ _ _ d) = showDImp o { ppopt_impl = True } d
1538showDeclImp o (PParams _ ns ps) = text "params" <+> braces (text (show ns) <> line <> showDecls o ps <> line)
1539showDeclImp o (PNamespace n ps) = text "namespace" <+> text n <> braces (line <> showDecls o ps <> line)
1540showDeclImp _ (PSyntax _ syn) = text "syntax" <+> text (show syn)
1541showDeclImp o (PClass _ _ _ cs n ps _ ds)
1542 = text "class" <+> text (show cs) <+> text (show n) <+> text (show ps) <> line <> showDecls o ds
1543showDeclImp o (PInstance _ _ cs n _ t _ ds)
1544 = text "instance" <+> text (show cs) <+> text (show n) <+> prettyImp o t <> line <> showDecls o ds
1545showDeclImp _ _ = text "..."
1546-- showDeclImp (PImport o) = "import " ++ o
1548instance Show (Doc OutputAnnotation) where
1549 show = flip (displayS . renderCompact) ""
1551getImps :: [PArg] -> [(Name, PTerm)]
1552getImps [] = []
1553getImps (PImp _ _ _ n tm : xs) = (n, tm) : getImps xs
1554getImps (_ : xs) = getImps xs
1556getExps :: [PArg] -> [PTerm]
1557getExps [] = []
1558getExps (PExp _ _ _ tm : xs) = tm : getExps xs
1559getExps (_ : xs) = getExps xs
1561getShowArgs :: [PArg] -> [PArg]
1562getShowArgs [] = []
1563getShowArgs (e@(PExp _ _ _ tm) : xs) = e : getShowArgs xs
1564getShowArgs (e : xs) | AlwaysShow `elem` argopts e = e : getShowArgs xs
1565getShowArgs (_ : xs) = getShowArgs xs
1567getConsts :: [PArg] -> [PTerm]
1568getConsts [] = []
1569getConsts (PConstraint _ _ _ tm : xs) = tm : getConsts xs
1570getConsts (_ : xs) = getConsts xs
1572getAll :: [PArg] -> [PTerm]
1573getAll = map getTm
1576-- | Show Idris name
1577showName :: Maybe IState -- ^^ the Idris state, for information about names and colours
1578 -> [(Name, Bool)] -- ^^ the bound variables and whether they're implicit
1579 -> PPOption -- ^^ pretty printing options
1580 -> Bool -- ^^ whether to colourise
1581 -> Name -- ^^ the term to show
1582 -> String
1583showName ist bnd ppo colour n = case ist of
1584 Just i -> if colour then colourise n (idris_colourTheme i) else showbasic n
1585 Nothing -> showbasic n
1586 where name = if ppopt_impl ppo then show n else showbasic n
1587 showbasic n@(UN _) = showCG n
1588 showbasic (MN i s) = str s
1589 showbasic (NS n s) = showSep "." (map str (reverse s)) ++ "." ++ showbasic n
1590 showbasic (SN s) = show s
1591 fst3 (x, _, _) = x
1592 colourise n t = let ctxt' = fmap tt_ctxt ist in
1593 case ctxt' of
1594 Nothing -> name
1595 Just ctxt | Just impl <- lookup n bnd -> if impl then colouriseImplicit t name
1596 else colouriseBound t name
1597 | isDConName n ctxt -> colouriseData t name
1598 | isFnName n ctxt -> colouriseFun t name
1599 | isTConName n ctxt -> colouriseType t name
1600 -- The assumption is that if a name is not bound and does not exist in the
1601 -- global context, then we're somewhere in which implicit info has been lost
1602 -- (like error messages). Thus, unknown vars are colourised as implicits.
1603 | otherwise -> colouriseImplicit t name
1605showTm :: IState -- ^^ the Idris state, for information about identifiers and colours
1606 -> PTerm -- ^^ the term to show
1607 -> String
1608showTm ist = displayDecorated (consoleDecorate ist) .
1609 renderPretty 0.8 100000 .
1610 prettyImp (ppOptionIst ist)
1612-- | Show a term with implicits, no colours
1613showTmImpls :: PTerm -> String
1614showTmImpls = flip (displayS . renderCompact . prettyImp verbosePPOption) ""
1618instance Sized PTerm where
1619 size (PQuote rawTerm) = size rawTerm
1620 size (PRef fc name) = size name
1621 size (PLam name ty bdy) = 1 + size ty + size bdy
1622 size (PPi plicity name ty bdy) = 1 + size ty + size bdy
1623 size (PLet name ty def bdy) = 1 + size ty + size def + size bdy
1624 size (PTyped trm ty) = 1 + size trm + size ty
1625 size (PApp fc name args) = 1 + size args
1626 size (PAppBind fc name args) = 1 + size args
1627 size (PCase fc trm bdy) = 1 + size trm + size bdy
1628 size (PTrue fc _) = 1
1629 size (PRefl fc _) = 1
1630 size (PResolveTC fc) = 1
1631 size (PEq fc _ _ left right) = 1 + size left + size right
1632 size (PRewrite fc left right _) = 1 + size left + size right
1633 size (PPair fc _ left right) = 1 + size left + size right
1634 size (PDPair fs _ left ty right) = 1 + size left + size ty + size right
1635 size (PAlternative a alts) = 1 + size alts
1636 size (PHidden hidden) = size hidden
1637 size (PUnifyLog tm) = size tm
1638 size (PDisamb _ tm) = size tm
1639 size (PNoImplicits tm) = size tm
1640 size PType = 1
1641 size (PUniverse _) = 1
1642 size (PConstant const) = 1 + size const
1643 size Placeholder = 1
1644 size (PDoBlock dos) = 1 + size dos
1645 size (PIdiom fc term) = 1 + size term
1646 size (PReturn fc) = 1
1647 size (PMetavar name) = 1
1648 size (PProof tactics) = size tactics
1649 size (PElabError err) = size err
1650 size PImpossible = 1
1651 size _ = 0
1653getPArity :: PTerm -> Int
1654getPArity (PPi _ _ _ sc) = 1 + getPArity sc
1655getPArity _ = 0
1657-- Return all names, free or globally bound, in the given term.
1659allNamesIn :: PTerm -> [Name]
1660allNamesIn tm = nub $ ni [] tm
1661 where -- TODO THINK added niTacImp, but is it right?
1662 ni env (PRef _ n)
1663 | not (n `elem` env) = [n]
1664 ni env (PPatvar _ n) = [n]
1665 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
1666 ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
1667 ni env (PCase _ c os) = ni env c ++ concatMap (ni env) (map snd os)
1668 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc
1669 ni env (PPi p n ty sc) = niTacImp env p ++ ni env ty ++ ni (n:env) sc
1670 ni env (PHidden tm) = ni env tm
1671 ni env (PEq _ _ _ l r) = ni env l ++ ni env r
1672 ni env (PRewrite _ l r _) = ni env l ++ ni env r
1673 ni env (PTyped l r) = ni env l ++ ni env r
1674 ni env (PPair _ _ l r) = ni env l ++ ni env r
1675 ni env (PDPair _ _ (PRef _ n) t r) = ni env t ++ ni (n:env) r
1676 ni env (PDPair _ _ l t r) = ni env l ++ ni env t ++ ni env r
1677 ni env (PAlternative a ls) = concatMap (ni env) ls
1678 ni env (PUnifyLog tm) = ni env tm
1679 ni env (PDisamb _ tm) = ni env tm
1680 ni env (PNoImplicits tm) = ni env tm
1681 ni env _ = []
1683 niTacImp env (TacImp _ _ scr) = ni env scr
1684 niTacImp _ _ = []
1686-- Return all names defined in binders in the given term
1687boundNamesIn :: PTerm -> [Name]
1688boundNamesIn tm = nub $ ni tm
1689 where -- TODO THINK Added niTacImp, but is it right?
1690 ni (PApp _ f as) = ni f ++ concatMap (ni) (map getTm as)
1691 ni (PAppBind _ f as) = ni f ++ concatMap (ni) (map getTm as)
1692 ni (PCase _ c os) = ni c ++ concatMap (ni) (map snd os)
1693 ni (PLam n ty sc) = n : (ni ty ++ ni sc)
1694 ni (PLet n ty val sc) = n : (ni ty ++ ni val ++ ni sc)
1695 ni (PPi p n ty sc) = niTacImp p ++ (n : (ni ty ++ ni sc))
1696 ni (PEq _ _ _ l r) = ni l ++ ni r
1697 ni (PRewrite _ l r _) = ni l ++ ni r
1698 ni (PTyped l r) = ni l ++ ni r
1699 ni (PPair _ _ l r) = ni l ++ ni r
1700 ni (PDPair _ _ (PRef _ n) t r) = ni t ++ ni r
1701 ni (PDPair _ _ l t r) = ni l ++ ni t ++ ni r
1702 ni (PAlternative a as) = concatMap (ni) as
1703 ni (PHidden tm) = ni tm
1704 ni (PUnifyLog tm) = ni tm
1705 ni (PDisamb _ tm) = ni tm
1706 ni (PNoImplicits tm) = ni tm
1707 ni _ = []
1709 niTacImp (TacImp _ _ scr) = ni scr
1710 niTacImp _ = []
1712-- Return names which are valid implicits in the given term (type).
1713implicitNamesIn :: [Name] -> IState -> PTerm -> [Name]
1714implicitNamesIn uvars ist tm = nub $ ni [] tm
1715 where
1716 ni env (PRef _ n)
1717 | not (n `elem` env)
1718 = case lookupTy n (tt_ctxt ist) of
1719 [] -> [n]
1720 _ -> if n `elem` uvars then [n] else []
1721 ni env (PApp _ f@(PRef _ n) as)
1722 | n `elem` uvars = ni env f ++ concatMap (ni env) (map getTm as)
1723 | otherwise = concatMap (ni env) (map getTm as)
1724 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
1725 ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
1726 ni env (PCase _ c os) = ni env c ++
1727 -- names in 'os', not counting the names bound in the cases
1728 (nub (concatMap (ni env) (map snd os))
1729 \\ nub (concatMap (ni env) (map fst os)))
1730 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc
1731 ni env (PPi p n ty sc) = ni env ty ++ ni (n:env) sc
1732 ni env (PEq _ _ _ l r) = ni env l ++ ni env r
1733 ni env (PRewrite _ l r _) = ni env l ++ ni env r
1734 ni env (PTyped l r) = ni env l ++ ni env r
1735 ni env (PPair _ _ l r) = ni env l ++ ni env r
1736 ni env (PDPair _ _ (PRef _ n) t r) = ni env t ++ ni (n:env) r
1737 ni env (PDPair _ _ l t r) = ni env l ++ ni env t ++ ni env r
1738 ni env (PAlternative a as) = concatMap (ni env) as
1739 ni env (PHidden tm) = ni env tm
1740 ni env (PUnifyLog tm) = ni env tm
1741 ni env (PDisamb _ tm) = ni env tm
1742 ni env (PNoImplicits tm) = ni env tm
1743 ni env _ = []
1745-- Return names which are free in the given term.
1746namesIn :: [(Name, PTerm)] -> IState -> PTerm -> [Name]
1747namesIn uvars ist tm = nub $ ni [] tm
1748 where
1749 ni env (PRef _ n)
1750 | not (n `elem` env)
1751 = case lookupTy n (tt_ctxt ist) of
1752 [] -> [n]
1753 _ -> if n `elem` (map fst uvars) then [n] else []
1754 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
1755 ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
1756 ni env (PCase _ c os) = ni env c ++
1757 -- names in 'os', not counting the names bound in the cases
1758 (nub (concatMap (ni env) (map snd os))
1759 \\ nub (concatMap (ni env) (map fst os)))
1760 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc
1761 ni env (PPi p n ty sc) = niTacImp env p ++ ni env ty ++ ni (n:env) sc
1762 ni env (PEq _ _ _ l r) = ni env l ++ ni env r
1763 ni env (PRewrite _ l r _) = ni env l ++ ni env r
1764 ni env (PTyped l r) = ni env l ++ ni env r
1765 ni env (PPair _ _ l r) = ni env l ++ ni env r
1766 ni env (PDPair _ _ (PRef _ n) t r) = ni env t ++ ni (n:env) r
1767 ni env (PDPair _ _ l t r) = ni env l ++ ni env t ++ ni env r
1768 ni env (PAlternative a as) = concatMap (ni env) as
1769 ni env (PHidden tm) = ni env tm
1770 ni env (PUnifyLog tm) = ni env tm
1771 ni env (PDisamb _ tm) = ni env tm
1772 ni env (PNoImplicits tm) = ni env tm
1773 ni env _ = []
1775 niTacImp env (TacImp _ _ scr) = ni env scr
1776 niTacImp _ _ = []
1778-- Return which of the given names are used in the given term.
1780usedNamesIn :: [Name] -> IState -> PTerm -> [Name]
1781usedNamesIn vars ist tm = nub $ ni [] tm
1782 where -- TODO THINK added niTacImp, but is it right?
1783 ni env (PRef _ n)
1784 | n `elem` vars && not (n `elem` env)
1785 = case lookupDefExact n (tt_ctxt ist) of
1786 Nothing -> [n]
1787 _ -> []
1788 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
1789 ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
1790 ni env (PCase _ c os) = ni env c ++ concatMap (ni env) (map snd os)
1791 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc
1792 ni env (PPi p n ty sc) = niTacImp env p ++ ni env ty ++ ni (n:env) sc
1793 ni env (PEq _ _ _ l r) = ni env l ++ ni env r
1794 ni env (PRewrite _ l r _) = ni env l ++ ni env r
1795 ni env (PTyped l r) = ni env l ++ ni env r
1796 ni env (PPair _ _ l r) = ni env l ++ ni env r
1797 ni env (PDPair _ _ (PRef _ n) t r) = ni env t ++ ni (n:env) r
1798 ni env (PDPair _ _ l t r) = ni env l ++ ni env t ++ ni env r
1799 ni env (PAlternative a as) = concatMap (ni env) as
1800 ni env (PHidden tm) = ni env tm
1801 ni env (PUnifyLog tm) = ni env tm
1802 ni env (PDisamb _ tm) = ni env tm
1803 ni env (PNoImplicits tm) = ni env tm
1804 ni env _ = []
1806 niTacImp env (TacImp _ _ scr) = ni env scr
1807 niTacImp _ _ = []
1809-- Return the list of inaccessible (= dotted) positions for a name.
1810getErasureInfo :: IState -> Name -> [Int]
1811getErasureInfo ist n =
1812 case lookupCtxtExact n (idris_optimisation ist) of
1813 Just (Optimise inacc detagg) -> map fst inacc
1814 Nothing -> []