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