git.iko.soy/Idris-dev
on 6faa1ab help sign in
Idris-dev/src/Idris/AbsSyntaxTree.hs
1808 lines 73 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
1068primNames = [falseTy, eqTy, eqCon, inferTy, inferCon]
1070unitTy = sUN "Unit"
1071unitCon = sUN "MkUnit"
1073falseDoc = parseDocstring . T.pack $
1074 "The empty type, also known as the trivially false proposition." ++
1075 "\n\n" ++
1076 "Use `FalseElim` or `absurd` to prove anything if you have a variable " ++
1077 "of type `_|_` in scope."
1078falseTy = sMN 0 "__False"
1079falseDecl = PDatadecl falseTy PType []
1080falseOpts = []
1082pairTy = sUN "Pair"
1083pairCon = sUN "MkPair"
1085eqTy = sUN "="
1086eqCon = sUN "Refl"
1087eqDoc = parseDocstring . T.pack $
1088 "The propositional equality type. A proof that `x` = `y`." ++
1089 "\n\n" ++
1090 "To use such a proof, pattern-match on it, and the two equal things will " ++
1091 "then need to be the _same_ pattern." ++
1092 "\n\n" ++
1093 "**Note**: Idris's equality type is potentially _heterogeneous_, which means that it " ++
1094 "is possible to state equalities between values of potentially different " ++
1095 "types. However, Idris will attempt the homogeneous case unless it fails to typecheck." ++
1096 "\n\n" ++
1097 "You may need to use `(~=~)` to explicitly request heterogeneous equality."
1099eqDecl = PDatadecl eqTy (piBindp impl [(n "A", PType), (n "B", PType)]
1100 (piBind [(n "x", PRef bi (n "A")), (n "y", PRef bi (n "B"))]
1101 PType))
1102 [(reflDoc, reflParamDoc,
1103 eqCon, PPi impl (n "A") PType (
1104 PPi impl (n "x") (PRef bi (n "A"))
1105 (PApp bi (PRef bi eqTy) [pimp (n "A") Placeholder False,
1106 pimp (n "B") Placeholder False,
1107 pexp (PRef bi (n "x")),
1108 pexp (PRef bi (n "x"))])), bi, [])]
1109 where n a = sUN a
1110 reflDoc = parseDocstring . T.pack $
1111 "A proof that `x` in fact equals `x`. To construct this, you must have already " ++
1112 "shown that both sides are in fact equal."
1113 reflParamDoc = [(n "A", parseDocstring . T.pack $ "the type at which the equality is proven"),
1114 (n "x", parseDocstring . T.pack $ "the element shown to be equal to itself.")]
1116eqParamDoc = [(n "A", parseDocstring . T.pack $ "the type of the left side of the equality"),
1117 (n "B", parseDocstring . T.pack $ "the type of the right side of the equality")
1119 where n a = sUN a
1121eqOpts = []
1123-- Defined in builtins.idr
1124sigmaTy = sUN "Sigma"
1125existsCon = sUN "MkSigma"
1127piBind :: [(Name, PTerm)] -> PTerm -> PTerm
1128piBind = piBindp expl
1130piBindp :: Plicity -> [(Name, PTerm)] -> PTerm -> PTerm
1131piBindp p [] t = t
1132piBindp p ((n, ty):ns) t = PPi p n ty (piBindp p ns t)
1135-- Pretty-printing declarations and terms
1137-- These "show" instances render to an absurdly wide screen because inserted line breaks
1138-- could interfere with interactive editing, which calls "show".
1140instance Show PTerm where
1141 showsPrec _ tm = (displayS . renderPretty 1.0 10000000 . prettyImp defaultPPOption) tm
1143instance Show PDecl where
1144 showsPrec _ d = (displayS . renderPretty 1.0 10000000 . showDeclImp verbosePPOption) d
1146instance Show PClause where
1147 showsPrec _ c = (displayS . renderPretty 1.0 10000000 . showCImp verbosePPOption) c
1149instance Show PData where
1150 showsPrec _ d = (displayS . renderPretty 1.0 10000000 . showDImp defaultPPOption) d
1152instance Pretty PTerm OutputAnnotation where
1153 pretty = prettyImp defaultPPOption
1155-- | Colourise annotations according to an Idris state. It ignores the names
1156-- in the annotation, as there's no good way to show extended information on a
1157-- terminal.
1158consoleDecorate :: IState -> OutputAnnotation -> String -> String
1159consoleDecorate ist _ | not (idris_colourRepl ist) = id
1160consoleDecorate ist (AnnConst c) = let theme = idris_colourTheme ist
1161 in if constIsType c
1162 then colouriseType theme
1163 else colouriseData theme
1164consoleDecorate ist (AnnData _ _) = colouriseData (idris_colourTheme ist)
1165consoleDecorate ist (AnnType _ _) = colouriseType (idris_colourTheme ist)
1166consoleDecorate ist (AnnBoundName _ True) = colouriseImplicit (idris_colourTheme ist)
1167consoleDecorate ist (AnnBoundName _ False) = colouriseBound (idris_colourTheme ist)
1168consoleDecorate ist AnnKeyword = colouriseKeyword (idris_colourTheme ist)
1169consoleDecorate ist (AnnName n _ _ _) = let ctxt = tt_ctxt ist
1170 theme = idris_colourTheme ist
1171 in case () of
1172 _ | isDConName n ctxt -> colouriseData theme
1173 _ | isFnName n ctxt -> colouriseFun theme
1174 _ | isTConName n ctxt -> colouriseType theme
1175 _ | isPostulateName n ist -> colourisePostulate theme
1176 _ | otherwise -> id -- don't colourise unknown names
1177consoleDecorate ist (AnnFC _) = id
1178consoleDecorate ist (AnnTextFmt fmt) = Idris.Colours.colourise (colour fmt)
1179 where colour BoldText = IdrisColour Nothing True False True False
1180 colour UnderlineText = IdrisColour Nothing True True False False
1181 colour ItalicText = IdrisColour Nothing True False False True
1182consoleDecorate ist (AnnTerm _ _) = id
1183consoleDecorate ist (AnnSearchResult _) = id
1185isPostulateName :: Name -> IState -> Bool
1186isPostulateName n ist = S.member n (idris_postulates ist)
1188-- | Pretty-print a high-level closed Idris term with no information about precedence/associativity
1189prettyImp :: PPOption -- ^^ pretty printing options
1190 -> PTerm -- ^^ the term to pretty-print
1191 -> Doc OutputAnnotation
1192prettyImp impl = pprintPTerm impl [] [] []
1194-- | Serialise something to base64 using its Binary instance.
1196-- | Do the right thing for rendering a term in an IState
1197prettyIst :: IState -> PTerm -> Doc OutputAnnotation
1198prettyIst ist = pprintPTerm (ppOptionIst ist) [] [] (idris_infixes ist)
1200-- | Pretty-print a high-level Idris term in some bindings context with infix info
1201pprintPTerm :: PPOption -- ^^ pretty printing options
1202 -> [(Name, Bool)] -- ^^ the currently-bound names and whether they are implicit
1203 -> [Name] -- ^^ names to always show in pi, even if not used
1204 -> [FixDecl] -- ^^ Fixity declarations
1205 -> PTerm -- ^^ the term to pretty-print
1206 -> Doc OutputAnnotation
1207pprintPTerm ppo bnd docArgs infixes = prettySe 10 bnd
1208 where
1209 prettySe :: Int -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation
1210 prettySe p bnd (PQuote r) =
1211 text "![" <> pretty r <> text "]"
1212 prettySe p bnd (PPatvar fc n) = pretty n
1213 prettySe p bnd e
1214 | Just str <- slist p bnd e = str
1215 | Just n <- snat p e = annotate (AnnData "Nat" "") (text (show n))
1216 prettySe p bnd (PRef fc n) = prettyName True (ppopt_impl ppo) bnd n
1217 prettySe p bnd (PLam n ty sc) =
1218 bracket p 2 . group . align . hang 2 $
1219 text "\\" <> bindingOf n False <+> text "=>" <$>
1220 prettySe 10 ((n, False):bnd) sc
1221 prettySe p bnd (PLet n ty v sc) =
1222 bracket p 2 . group . align $
1223 kwd "let" <+> (group . align . hang 2 $ bindingOf n False <+> text "=" <$> prettySe 10 bnd v) </>
1224 kwd "in" <+> (group . align . hang 2 $ prettySe 10 ((n, False):bnd) sc)
1225 prettySe p bnd (PPi (Exp l s _) n ty sc)
1226 | n `elem` allNamesIn sc || ppopt_impl ppo || n `elem` docArgs =
1227 bracket p 2 . group $
1228 enclose lparen rparen (group . align $ bindingOf n False <+> colon <+> prettySe 10 bnd ty) <+>
1229 st <> text "->" <$> prettySe 10 ((n, False):bnd) sc
1230 | otherwise =
1231 bracket p 2 . group $
1232 group (prettySe 1 bnd ty <+> st) <> text "->" <$> group (prettySe 10 ((n, False):bnd) sc)
1233 where
1234 st =
1235 case s of
1236 Static -> text "[static]" <> space
1237 _ -> empty
1238 prettySe p bnd (PPi (Imp l s _) n ty sc)
1239 | ppopt_impl ppo =
1240 bracket p 2 $
1241 lbrace <> bindingOf n True <+> colon <+> prettySe 10 bnd ty <> rbrace <+>
1242 st <> text "->" </> prettySe 10 ((n, True):bnd) sc
1243 | otherwise = prettySe 10 ((n, True):bnd) sc
1244 where
1245 st =
1246 case s of
1247 Static -> text "[static]" <> space
1248 _ -> empty
1249 prettySe p bnd (PPi (Constraint _ _) n ty sc) =
1250 bracket p 2 $
1251 prettySe 10 bnd ty <+> text "=>" </> prettySe 10 ((n, True):bnd) sc
1252 prettySe p bnd (PPi (TacImp _ _ s) n ty sc) =
1253 bracket p 2 $
1254 lbrace <> kwd "tacimp" <+> pretty n <+> colon <+> prettySe 10 bnd ty <>
1255 rbrace <+> text "->" </> prettySe 10 ((n, True):bnd) sc
1256 prettySe p bnd (PApp _ (PRef _ f) args) -- normal names, no explicit args
1257 | UN nm <- basename f
1258 , not (ppopt_impl ppo) && null (getShowArgs args) =
1259 prettyName True (ppopt_impl ppo) bnd f
1260 prettySe p bnd (PAppBind _ (PRef _ f) [])
1261 | not (ppopt_impl ppo) = text "!" <> prettyName True (ppopt_impl ppo) bnd f
1262 prettySe p bnd (PApp _ (PRef _ op) args) -- infix operators
1263 | UN nm <- basename op
1264 , not (tnull nm) &&
1265 (not (ppopt_impl ppo)) && (not $ isAlpha (thead nm)) =
1266 case getShowArgs args of
1267 [] -> opName True
1268 [x] -> group (opName True <$> group (prettySe 0 bnd (getTm x)))
1269 [l,r] -> let precedence = fromMaybe 20 (fmap prec f)
1270 in bracket p precedence $ inFix (getTm l) (getTm r)
1271 (l@(PExp _ _ _ _) : r@(PExp _ _ _ _) : rest) ->
1272 bracket p 1 $
1273 enclose lparen rparen (inFix (getTm l) (getTm r)) <+>
1274 align (group (vsep (map (prettyArgS bnd) rest)))
1275 as -> opName True <+> align (vsep (map (prettyArgS bnd) as))
1276 where opName isPrefix = prettyName isPrefix (ppopt_impl ppo) bnd op
1277 f = getFixity (opStr op)
1278 left l = case f of
1279 Nothing -> prettySe (-1) bnd l
1280 Just (Infixl p') -> prettySe p' bnd l
1281 Just f' -> prettySe (prec f'-1) bnd l
1282 right r = case f of
1283 Nothing -> prettySe (-1) bnd r
1284 Just (Infixr p') -> prettySe p' bnd r
1285 Just f' -> prettySe (prec f'-1) bnd r
1286 inFix l r = align . group $
1287 (left l <+> opName False) <$> group (right r)
1288 prettySe p bnd (PApp _ hd@(PRef fc f) [tm]) -- symbols, like 'foo
1289 | PConstant (Idris.Core.TT.Str str) <- getTm tm,
1290 f == sUN "Symbol_" = annotate (AnnType ("'" ++ str) ("The symbol " ++ str)) $
1291 char '\'' <> prettySe 10 bnd (PRef fc (sUN str))
1292 prettySe p bnd (PApp _ f as) = -- Normal prefix applications
1293 let args = getShowArgs as
1294 fp = prettySe 1 bnd f
1295 in
1296 bracket p 1 . group $
1297 if ppopt_impl ppo
1298 then if null as
1299 then fp
1300 else fp <+> align (vsep (map (prettyArgS bnd) as))
1301 else if null args
1302 then fp
1303 else fp <+> align (vsep (map (prettyArgS bnd) args))
1304 prettySe p bnd (PCase _ scr opts) =
1305 kwd "case" <+> prettySe 10 bnd scr <+> kwd "of" <> prettyBody
1306 where
1307 prettyBody = foldr (<>) empty $ intersperse (text "|") $ map sc opts
1309 sc (l, r) = nest nestingSize $ prettySe 10 bnd l <+> text "=>" <+> prettySe 10 bnd r
1310 prettySe p bnd (PHidden tm) = text "." <> prettySe 0 bnd tm
1311 prettySe p bnd (PRefl _ _) = annName eqCon $ text "Refl"
1312 prettySe p bnd (PResolveTC _) = text "resolvetc"
1313 prettySe p bnd (PTrue _ IsType) = annName unitTy $ text "()"
1314 prettySe p bnd (PTrue _ IsTerm) = annName unitCon $ text "()"
1315 prettySe p bnd (PTrue _ TypeOrTerm) = text "()"
1316 prettySe p bnd (PFalse _) = annName falseTy $ text "_|_"
1317 prettySe p bnd (PEq _ lt rt l r)
1318 | ppopt_impl ppo =
1319 bracket p 1 $
1320 enclose lparen rparen eq <+>
1321 align (group (vsep (map (prettyArgS bnd)
1322 [PImp 0 False [] (sUN "A") lt,
1323 PImp 0 False [] (sUN "B") rt,
1324 PExp 0 [] (sUN "x") l,
1325 PExp 0 [] (sUN "y") r])))
1326 | otherwise =
1327 bracket p 2 . align . group $
1328 prettySe 10 bnd l <+> eq <$> group (prettySe 10 bnd r)
1329 where eq = annName eqTy (text "=")
1330 prettySe p bnd (PRewrite _ l r _) =
1331 bracket p 2 $
1332 text "rewrite" <+> prettySe 10 bnd l <+> text "in" <+> prettySe 10 bnd r
1333 prettySe p bnd (PTyped l r) =
1334 lparen <> prettySe 10 bnd l <+> colon <+> prettySe 10 bnd r <> rparen
1335 prettySe p bnd pair@(PPair _ pun _ _) -- flatten tuples to the right, like parser
1336 | Just elts <- pairElts pair = enclose (ann lparen) (ann rparen) .
1337 align . group . vsep . punctuate (ann comma) $
1338 map (prettySe 10 bnd) elts
1339 where ann = case pun of
1340 TypeOrTerm -> id
1341 IsType -> annName pairTy
1342 IsTerm -> annName pairCon
1343 prettySe p bnd (PDPair _ TypeOrTerm l t r) =
1344 lparen <> prettySe 10 bnd l <+> text "**" <+> prettySe 10 bnd r <> rparen
1345 prettySe p bnd (PDPair _ IsType (PRef _ n) t r) =
1346 annName sigmaTy lparen <>
1347 bindingOf n False <+>
1348 annName sigmaTy (text "**") <+>
1349 prettySe 10 ((n, False):bnd) r <>
1350 annName sigmaTy rparen
1351 prettySe p bnd (PDPair _ IsType l t r) =
1352 annName sigmaTy lparen <>
1353 prettySe 10 bnd l <+>
1354 annName sigmaTy (text "**") <+>
1355 prettySe 10 bnd r <>
1356 annName sigmaTy rparen
1357 prettySe p bnd (PDPair _ IsTerm l t r) =
1358 annName existsCon lparen <>
1359 prettySe 10 bnd l <+>
1360 annName existsCon (text "**") <+>
1361 prettySe 10 bnd r <>
1362 annName existsCon rparen
1363 prettySe p bnd (PAlternative a as) =
1364 lparen <> text "|" <> prettyAs <> text "|" <> rparen
1365 where
1366 prettyAs =
1367 foldr (\l -> \r -> l <+> text "," <+> r) empty $ map (prettySe 10 bnd) as
1368 prettySe p bnd PType = annotate (AnnType "Type" "The type of types") $ text "Type"
1369 prettySe p bnd (PUniverse u) = annotate (AnnType (show u) "The type of unique types") $ text (show u)
1370 prettySe p bnd (PConstant c) = annotate (AnnConst c) (text (show c))
1371 -- XXX: add pretty for tactics
1372 prettySe p bnd (PProof ts) =
1373 text "proof" <+> lbrace <> nest nestingSize (text . show $ ts) <> rbrace
1374 prettySe p bnd (PTactics ts) =
1375 text "tactics" <+> lbrace <> nest nestingSize (text . show $ ts) <> rbrace
1376 prettySe p bnd (PMetavar n) = text "?" <> pretty n
1377 prettySe p bnd (PReturn f) = kwd "return"
1378 prettySe p bnd PImpossible = kwd "impossible"
1379 prettySe p bnd Placeholder = text "_"
1380 prettySe p bnd (PDoBlock _) = text "do block pretty not implemented"
1381 prettySe p bnd (PCoerced t) = prettySe p bnd t
1382 prettySe p bnd (PElabError s) = pretty s
1383 -- Quasiquote pprinting ignores bound vars
1384 prettySe p bnd (PQuasiquote t Nothing) = text "`(" <> prettySe p [] t <> text ")"
1385 prettySe p bnd (PQuasiquote t (Just g)) = text "`(" <> prettySe p [] t <+> colon <+> prettySe p [] g <> text ")"
1386 prettySe p bnd (PUnquote t) = text "~" <> prettySe p bnd t
1388 prettySe p bnd _ = text "missing pretty-printer for term"
1390 prettyArgS bnd (PImp _ _ _ n tm) = prettyArgSi bnd (n, tm)
1391 prettyArgS bnd (PExp _ _ _ tm) = prettyArgSe bnd tm
1392 prettyArgS bnd (PConstraint _ _ _ tm) = prettyArgSc bnd tm
1393 prettyArgS bnd (PTacImplicit _ _ n _ tm) = prettyArgSti bnd (n, tm)
1395 prettyArgSe bnd arg = prettySe 0 bnd arg
1396 prettyArgSi bnd (n, val) = lbrace <> pretty n <+> text "=" <+> prettySe 10 bnd val <> rbrace
1397 prettyArgSc bnd val = lbrace <> lbrace <> prettySe 10 bnd val <> rbrace <> rbrace
1398 prettyArgSti bnd (n, val) = lbrace <> kwd "auto" <+> pretty n <+> text "=" <+> prettySe 10 bnd val <> rbrace
1400 annName :: Name -> Doc OutputAnnotation -> Doc OutputAnnotation
1401 annName n = annotate (AnnName n Nothing Nothing Nothing)
1403 opStr :: Name -> String
1404 opStr (NS n _) = opStr n
1405 opStr (UN n) = T.unpack n
1407 basename :: Name -> Name
1408 basename (NS n _) = basename n
1409 basename n = n
1411 slist' p bnd (PApp _ (PRef _ nil) _)
1412 | not (ppopt_impl ppo) && nsroot nil == sUN "Nil" = Just []
1413 slist' p bnd (PRef _ nil)
1414 | not (ppopt_impl ppo) && nsroot nil == sUN "Nil" = Just []
1415 slist' p bnd (PApp _ (PRef _ cons) args)
1416 | nsroot cons == sUN "::",
1417 (PExp {getTm=tl}):(PExp {getTm=hd}):imps <- reverse args,
1418 all isImp imps,
1419 Just tl' <- slist' p bnd tl
1420 = Just (hd:tl')
1421 where
1422 isImp (PImp {}) = True
1423 isImp _ = False
1424 slist' _ _ tm = Nothing
1426 slist p bnd e | Just es <- slist' p bnd e = Just $
1427 case es of [] -> annotate (AnnData "" "") $ text "[]"
1428 [x] -> enclose left right . group $
1429 prettySe p bnd x
1430 xs -> (enclose left right .
1431 align . group . vsep .
1432 punctuate comma .
1433 map (prettySe p bnd)) xs
1434 where left = (annotate (AnnData "" "") (text "["))
1435 right = (annotate (AnnData "" "") (text "]"))
1436 comma = (annotate (AnnData "" "") (text ","))
1437 slist _ _ _ = Nothing
1439 pairElts :: PTerm -> Maybe [PTerm]
1440 pairElts (PPair _ _ x y) | Just elts <- pairElts y = Just (x:elts)
1441 | otherwise = Just [x, y]
1442 pairElts _ = Nothing
1444 natns = "Prelude.Nat."
1446 snat p (PRef _ z)
1447 | show z == (natns++"Z") || show z == "Z" = Just 0
1448 snat p (PApp _ s [PExp {getTm=n}])
1449 | show s == (natns++"S") || show s == "S",
1450 Just n' <- snat p n
1451 = Just $ 1 + n'
1452 snat _ _ = Nothing
1454 bracket outer inner doc
1455 | inner > outer = lparen <> doc <> rparen
1456 | otherwise = doc
1458 kwd = annotate AnnKeyword . text
1460 fixities :: M.Map String Fixity
1461 fixities = M.fromList [(s, f) | (Fix f s) <- infixes]
1463 getFixity :: String -> Maybe Fixity
1464 getFixity = flip M.lookup fixities
1466prettyDocumentedIst :: IState -> (Name, PTerm, Maybe Docstring) -> Doc OutputAnnotation
1467prettyDocumentedIst ist (name, ty, docs) =
1468 prettyName True True [] name <+> colon <+> align (prettyIst ist ty) <$>
1469 fromMaybe empty (fmap (\d -> renderDocstring d <> line) docs)
1471-- | Pretty-printer helper for the binding site of a name
1472bindingOf :: Name -- ^^ the bound name
1473 -> Bool -- ^^ whether the name is implicit
1474 -> Doc OutputAnnotation
1475bindingOf n imp = annotate (AnnBoundName n imp) (text (show n))
1477-- | Pretty-printer helper for names that attaches the correct annotations
1478prettyName
1479 :: Bool -- ^^ whether the name should be parenthesised if it is an infix operator
1480 -> Bool -- ^^ whether to show namespaces
1481 -> [(Name, Bool)] -- ^^ the current bound variables and whether they are implicit
1482 -> Name -- ^^ the name to pprint
1483 -> Doc OutputAnnotation
1484prettyName infixParen showNS bnd n
1485 | Just imp <- lookup n bnd = annotate (AnnBoundName n imp) fullName
1486 | otherwise = annotate (AnnName n Nothing Nothing Nothing) fullName
1487 where fullName = text nameSpace <> parenthesise (text (baseName n))
1488 baseName (UN n) = T.unpack n
1489 baseName (NS n ns) = baseName n
1490 baseName (MN i s) = T.unpack s
1491 baseName n | n == falseTy = "_|_"
1492 baseName other = show other
1493 nameSpace = case n of
1494 (NS n' ns) -> if showNS then (concatMap (++ ".") . map T.unpack . reverse) ns else ""
1495 _ -> ""
1496 isInfix = case baseName n of
1497 "" -> False
1498 (c : _) -> not (isAlpha c)
1499 parenthesise = if isInfix && infixParen then enclose lparen rparen else id
1502showCImp :: PPOption -> PClause -> Doc OutputAnnotation
1503showCImp ppo (PClause _ n l ws r w)
1504 = prettyImp ppo l <+> showWs ws <+> text "=" <+> prettyImp ppo r
1505 <+> text "where" <+> text (show w)
1506 where
1507 showWs [] = empty
1508 showWs (x : xs) = text "|" <+> prettyImp ppo x <+> showWs xs
1509showCImp ppo (PWith _ n l ws r w)
1510 = prettyImp ppo l <+> showWs ws <+> text "with" <+> prettyImp ppo r
1511 <+> braces (text (show w))
1512 where
1513 showWs [] = empty
1514 showWs (x : xs) = text "|" <+> prettyImp ppo x <+> showWs xs
1517showDImp :: PPOption -> PData -> Doc OutputAnnotation
1518showDImp ppo (PDatadecl n ty cons)
1519 = text "data" <+> text (show n) <+> colon <+> prettyImp ppo ty <+> text "where" <$>
1520 (indent 2 $ vsep (map (\ (_, _, n, t, _, _) -> pipe <+> prettyName True False [] n <+> colon <+> prettyImp ppo t) cons))
1522showDecls :: PPOption -> [PDecl] -> Doc OutputAnnotation
1523showDecls o ds = vsep (map (showDeclImp o) ds)
1525showDeclImp _ (PFix _ f ops) = text (show f) <+> cat (punctuate (text ",") (map text ops))
1526showDeclImp o (PTy _ _ _ _ _ n t) = text "tydecl" <+> text (showCG n) <+> colon <+> prettyImp o t
1527showDeclImp o (PClauses _ _ n cs) = text "pat" <+> text (showCG n) <+> text "\t" <+>
1528 indent 2 (vsep (map (showCImp o) cs))
1529showDeclImp o (PData _ _ _ _ _ d) = showDImp o { ppopt_impl = True } d
1530showDeclImp o (PParams _ ns ps) = text "params" <+> braces (text (show ns) <> line <> showDecls o ps <> line)
1531showDeclImp o (PNamespace n ps) = text "namespace" <+> text n <> braces (line <> showDecls o ps <> line)
1532showDeclImp _ (PSyntax _ syn) = text "syntax" <+> text (show syn)
1533showDeclImp o (PClass _ _ _ cs n ps _ ds)
1534 = text "class" <+> text (show cs) <+> text (show n) <+> text (show ps) <> line <> showDecls o ds
1535showDeclImp o (PInstance _ _ cs n _ t _ ds)
1536 = text "instance" <+> text (show cs) <+> text (show n) <+> prettyImp o t <> line <> showDecls o ds
1537showDeclImp _ _ = text "..."
1538-- showDeclImp (PImport o) = "import " ++ o
1540instance Show (Doc OutputAnnotation) where
1541 show = flip (displayS . renderCompact) ""
1543getImps :: [PArg] -> [(Name, PTerm)]
1544getImps [] = []
1545getImps (PImp _ _ _ n tm : xs) = (n, tm) : getImps xs
1546getImps (_ : xs) = getImps xs
1548getExps :: [PArg] -> [PTerm]
1549getExps [] = []
1550getExps (PExp _ _ _ tm : xs) = tm : getExps xs
1551getExps (_ : xs) = getExps xs
1553getShowArgs :: [PArg] -> [PArg]
1554getShowArgs [] = []
1555getShowArgs (e@(PExp _ _ _ tm) : xs) = e : getShowArgs xs
1556getShowArgs (e : xs) | AlwaysShow `elem` argopts e = e : getShowArgs xs
1557getShowArgs (_ : xs) = getShowArgs xs
1559getConsts :: [PArg] -> [PTerm]
1560getConsts [] = []
1561getConsts (PConstraint _ _ _ tm : xs) = tm : getConsts xs
1562getConsts (_ : xs) = getConsts xs
1564getAll :: [PArg] -> [PTerm]
1565getAll = map getTm
1568-- | Show Idris name
1569showName :: Maybe IState -- ^^ the Idris state, for information about names and colours
1570 -> [(Name, Bool)] -- ^^ the bound variables and whether they're implicit
1571 -> PPOption -- ^^ pretty printing options
1572 -> Bool -- ^^ whether to colourise
1573 -> Name -- ^^ the term to show
1574 -> String
1575showName ist bnd ppo colour n = case ist of
1576 Just i -> if colour then colourise n (idris_colourTheme i) else showbasic n
1577 Nothing -> showbasic n
1578 where name = if ppopt_impl ppo then show n else showbasic n
1579 showbasic n@(UN _) = showCG n
1580 showbasic (MN i s) = str s
1581 showbasic (NS n s) = showSep "." (map str (reverse s)) ++ "." ++ showbasic n
1582 showbasic (SN s) = show s
1583 fst3 (x, _, _) = x
1584 colourise n t = let ctxt' = fmap tt_ctxt ist in
1585 case ctxt' of
1586 Nothing -> name
1587 Just ctxt | Just impl <- lookup n bnd -> if impl then colouriseImplicit t name
1588 else colouriseBound t name
1589 | isDConName n ctxt -> colouriseData t name
1590 | isFnName n ctxt -> colouriseFun t name
1591 | isTConName n ctxt -> colouriseType t name
1592 -- The assumption is that if a name is not bound and does not exist in the
1593 -- global context, then we're somewhere in which implicit info has been lost
1594 -- (like error messages). Thus, unknown vars are colourised as implicits.
1595 | otherwise -> colouriseImplicit t name
1597showTm :: IState -- ^^ the Idris state, for information about identifiers and colours
1598 -> PTerm -- ^^ the term to show
1599 -> String
1600showTm ist = displayDecorated (consoleDecorate ist) .
1601 renderPretty 0.8 100000 .
1602 prettyImp (ppOptionIst ist)
1604-- | Show a term with implicits, no colours
1605showTmImpls :: PTerm -> String
1606showTmImpls = flip (displayS . renderCompact . prettyImp verbosePPOption) ""
1610instance Sized PTerm where
1611 size (PQuote rawTerm) = size rawTerm
1612 size (PRef fc name) = size name
1613 size (PLam name ty bdy) = 1 + size ty + size bdy
1614 size (PPi plicity name ty bdy) = 1 + size ty + size bdy
1615 size (PLet name ty def bdy) = 1 + size ty + size def + size bdy
1616 size (PTyped trm ty) = 1 + size trm + size ty
1617 size (PApp fc name args) = 1 + size args
1618 size (PAppBind fc name args) = 1 + size args
1619 size (PCase fc trm bdy) = 1 + size trm + size bdy
1620 size (PTrue fc _) = 1
1621 size (PFalse fc) = 1
1622 size (PRefl fc _) = 1
1623 size (PResolveTC fc) = 1
1624 size (PEq fc _ _ left right) = 1 + size left + size right
1625 size (PRewrite fc left right _) = 1 + size left + size right
1626 size (PPair fc _ left right) = 1 + size left + size right
1627 size (PDPair fs _ left ty right) = 1 + size left + size ty + size right
1628 size (PAlternative a alts) = 1 + size alts
1629 size (PHidden hidden) = size hidden
1630 size (PUnifyLog tm) = size tm
1631 size (PDisamb _ tm) = size tm
1632 size (PNoImplicits tm) = size tm
1633 size PType = 1
1634 size (PUniverse _) = 1
1635 size (PConstant const) = 1 + size const
1636 size Placeholder = 1
1637 size (PDoBlock dos) = 1 + size dos
1638 size (PIdiom fc term) = 1 + size term
1639 size (PReturn fc) = 1
1640 size (PMetavar name) = 1
1641 size (PProof tactics) = size tactics
1642 size (PElabError err) = size err
1643 size PImpossible = 1
1644 size _ = 0
1646getPArity :: PTerm -> Int
1647getPArity (PPi _ _ _ sc) = 1 + getPArity sc
1648getPArity _ = 0
1650-- Return all names, free or globally bound, in the given term.
1652allNamesIn :: PTerm -> [Name]
1653allNamesIn tm = nub $ ni [] tm
1654 where -- TODO THINK added niTacImp, but is it right?
1655 ni env (PRef _ n)
1656 | not (n `elem` env) = [n]
1657 ni env (PPatvar _ n) = [n]
1658 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
1659 ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
1660 ni env (PCase _ c os) = ni env c ++ concatMap (ni env) (map snd os)
1661 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc
1662 ni env (PPi p n ty sc) = niTacImp env p ++ ni env ty ++ ni (n:env) sc
1663 ni env (PHidden tm) = ni env tm
1664 ni env (PEq _ _ _ l r) = ni env l ++ ni env r
1665 ni env (PRewrite _ l r _) = ni env l ++ ni env r
1666 ni env (PTyped l r) = ni env l ++ ni env r
1667 ni env (PPair _ _ l r) = ni env l ++ ni env r
1668 ni env (PDPair _ _ (PRef _ n) t r) = ni env t ++ ni (n:env) r
1669 ni env (PDPair _ _ l t r) = ni env l ++ ni env t ++ ni env r
1670 ni env (PAlternative a ls) = concatMap (ni env) ls
1671 ni env (PUnifyLog tm) = ni env tm
1672 ni env (PDisamb _ tm) = ni env tm
1673 ni env (PNoImplicits tm) = ni env tm
1674 ni env _ = []
1676 niTacImp env (TacImp _ _ scr) = ni env scr
1677 niTacImp _ _ = []
1679-- Return all names defined in binders in the given term
1680boundNamesIn :: PTerm -> [Name]
1681boundNamesIn tm = nub $ ni tm
1682 where -- TODO THINK Added niTacImp, but is it right?
1683 ni (PApp _ f as) = ni f ++ concatMap (ni) (map getTm as)
1684 ni (PAppBind _ f as) = ni f ++ concatMap (ni) (map getTm as)
1685 ni (PCase _ c os) = ni c ++ concatMap (ni) (map snd os)
1686 ni (PLam n ty sc) = n : (ni ty ++ ni sc)
1687 ni (PLet n ty val sc) = n : (ni ty ++ ni val ++ ni sc)
1688 ni (PPi p n ty sc) = niTacImp p ++ (n : (ni ty ++ ni sc))
1689 ni (PEq _ _ _ l r) = ni l ++ ni r
1690 ni (PRewrite _ l r _) = ni l ++ ni r
1691 ni (PTyped l r) = ni l ++ ni r
1692 ni (PPair _ _ l r) = ni l ++ ni r
1693 ni (PDPair _ _ (PRef _ n) t r) = ni t ++ ni r
1694 ni (PDPair _ _ l t r) = ni l ++ ni t ++ ni r
1695 ni (PAlternative a as) = concatMap (ni) as
1696 ni (PHidden tm) = ni tm
1697 ni (PUnifyLog tm) = ni tm
1698 ni (PDisamb _ tm) = ni tm
1699 ni (PNoImplicits tm) = ni tm
1700 ni _ = []
1702 niTacImp (TacImp _ _ scr) = ni scr
1703 niTacImp _ = []
1705-- Return names which are valid implicits in the given term (type).
1706implicitNamesIn :: [Name] -> IState -> PTerm -> [Name]
1707implicitNamesIn uvars ist tm = nub $ ni [] tm
1708 where
1709 ni env (PRef _ n)
1710 | not (n `elem` env)
1711 = case lookupTy n (tt_ctxt ist) of
1712 [] -> [n]
1713 _ -> if n `elem` uvars then [n] else []
1714 ni env (PApp _ f@(PRef _ n) as)
1715 | n `elem` uvars = ni env f ++ concatMap (ni env) (map getTm as)
1716 | otherwise = concatMap (ni env) (map getTm as)
1717 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
1718 ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
1719 ni env (PCase _ c os) = ni env c ++
1720 -- names in 'os', not counting the names bound in the cases
1721 (nub (concatMap (ni env) (map snd os))
1722 \\ nub (concatMap (ni env) (map fst os)))
1723 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc
1724 ni env (PPi p n ty sc) = ni env ty ++ ni (n:env) sc
1725 ni env (PEq _ _ _ l r) = ni env l ++ ni env r
1726 ni env (PRewrite _ l r _) = ni env l ++ ni env r
1727 ni env (PTyped l r) = ni env l ++ ni env r
1728 ni env (PPair _ _ l r) = ni env l ++ ni env r
1729 ni env (PDPair _ _ (PRef _ n) t r) = ni env t ++ ni (n:env) r
1730 ni env (PDPair _ _ l t r) = ni env l ++ ni env t ++ ni env r
1731 ni env (PAlternative a as) = concatMap (ni env) as
1732 ni env (PHidden tm) = ni env tm
1733 ni env (PUnifyLog tm) = ni env tm
1734 ni env (PDisamb _ tm) = ni env tm
1735 ni env (PNoImplicits tm) = ni env tm
1736 ni env _ = []
1738-- Return names which are free in the given term.
1739namesIn :: [(Name, PTerm)] -> IState -> PTerm -> [Name]
1740namesIn uvars ist tm = nub $ ni [] tm
1741 where
1742 ni env (PRef _ n)
1743 | not (n `elem` env)
1744 = case lookupTy n (tt_ctxt ist) of
1745 [] -> [n]
1746 _ -> if n `elem` (map fst uvars) then [n] else []
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) = niTacImp env p ++ 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 niTacImp env (TacImp _ _ scr) = ni env scr
1769 niTacImp _ _ = []
1771-- Return which of the given names are used in the given term.
1773usedNamesIn :: [Name] -> IState -> PTerm -> [Name]
1774usedNamesIn vars ist tm = nub $ ni [] tm
1775 where -- TODO THINK added niTacImp, but is it right?
1776 ni env (PRef _ n)
1777 | n `elem` vars && not (n `elem` env)
1778 = case lookupDefExact n (tt_ctxt ist) of
1779 Nothing -> [n]
1780 _ -> []
1781 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
1782 ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
1783 ni env (PCase _ c os) = ni env c ++ concatMap (ni env) (map snd os)
1784 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc
1785 ni env (PPi p n ty sc) = niTacImp env p ++ ni env ty ++ ni (n:env) sc
1786 ni env (PEq _ _ _ l r) = ni env l ++ ni env r
1787 ni env (PRewrite _ l r _) = ni env l ++ ni env r
1788 ni env (PTyped l r) = ni env l ++ ni env r
1789 ni env (PPair _ _ l r) = ni env l ++ ni env r
1790 ni env (PDPair _ _ (PRef _ n) t r) = ni env t ++ ni (n:env) r
1791 ni env (PDPair _ _ l t r) = ni env l ++ ni env t ++ ni env r
1792 ni env (PAlternative a as) = concatMap (ni env) as
1793 ni env (PHidden tm) = ni env tm
1794 ni env (PUnifyLog tm) = ni env tm
1795 ni env (PDisamb _ tm) = ni env tm
1796 ni env (PNoImplicits tm) = ni env tm
1797 ni env _ = []
1799 niTacImp env (TacImp _ _ scr) = ni env scr
1800 niTacImp _ _ = []
1802-- Return the list of inaccessible (= dotted) positions for a name.
1803getErasureInfo :: IState -> Name -> [Int]
1804getErasureInfo ist n =
1805 case lookupCtxtExact n (idris_optimisation ist) of
1806 Just (Optimise inacc detagg) -> map fst inacc
1807 Nothing -> []