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