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