git.iko.soy/Idris-dev
on 7d081b0 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 idris_repl_defs :: [Name] -- ^ List of names that were defined in the repl, and can be re-/un-defined
196 }
198data SizeChange = Smaller | Same | Bigger | Unknown
199 deriving (Show, Eq)
200{-!
201deriving instance Binary SizeChange
202deriving instance NFData SizeChange
203!-}
205type SCGEntry = (Name, [Maybe (Int, SizeChange)])
206type UsageReason = (Name, Int) -- fn_name, its_arg_number
208data CGInfo = CGInfo { argsdef :: [Name],
209 calls :: [(Name, [[Name]])],
210 scg :: [SCGEntry],
211 argsused :: [Name],
212 usedpos :: [(Int, [UsageReason])] }
213 deriving Show
214{-!
215deriving instance Binary CGInfo
216deriving instance NFData CGInfo
217!-}
219primDefs = [sUN "unsafePerformPrimIO",
220 sUN "mkLazyForeignPrim",
221 sUN "mkForeignPrim",
222 sUN "FalseElim"]
224-- information that needs writing for the current module's .ibc file
225data IBCWrite = IBCFix FixDecl
226 | IBCImp Name
227 | IBCStatic Name
228 | IBCClass Name
229 | IBCInstance Bool Name Name
230 | IBCDSL Name
231 | IBCData Name
232 | IBCOpt Name
233 | IBCMetavar Name
234 | IBCSyntax Syntax
235 | IBCKeyword String
236 | IBCImport FilePath
237 | IBCObj Codegen FilePath
238 | IBCLib Codegen String
239 | IBCCGFlag Codegen String
240 | IBCDyLib String
241 | IBCHeader Codegen String
242 | IBCAccess Name Accessibility
243 | IBCMetaInformation Name MetaInformation
244 | IBCTotal Name Totality
245 | IBCFlags Name [FnOpt]
246 | IBCTrans (Term, Term)
247 | IBCErrRev (Term, Term)
248 | IBCCG Name
249 | IBCDoc Name
250 | IBCCoercion Name
251 | IBCDef Name -- i.e. main context
252 | IBCNameHint (Name, Name)
253 | IBCLineApp FilePath Int PTerm
254 | IBCErrorHandler Name
255 | IBCFunctionErrorHandler Name Name Name
256 | IBCPostulate Name
257 | IBCTotCheckErr FC String
258 | IBCParsedRegion FC
259 deriving Show
261-- | The initial state for the compiler
262idrisInit :: IState
263idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext
264 emptyContext emptyContext emptyContext emptyContext
265 emptyContext emptyContext emptyContext emptyContext
266 emptyContext emptyContext
267 [] [] [] defaultOpts 6 [] [] [] [] [] [] [] [] [] [] [] [] []
268 [] [] Nothing [] Nothing [] [] Nothing Nothing [] Hidden False [] Nothing [] [] RawOutput
269 True defaultTheme stdout [] (0, emptyContext) emptyContext M.empty
270 AutomaticWidth S.empty Nothing Nothing []
272-- | The monad for the main REPL - reading and processing files and updating
273-- global state (hence the IO inner monad).
274--type Idris = WriterT [Either String (IO ())] (State IState a))
275type Idris = StateT IState (ErrorT Err IO)
277-- Commands in the REPL
279data Codegen = ViaC
280 | ViaJava
281 | ViaNode
282 | ViaJavaScript
283 | ViaLLVM
284 | Bytecode
285 deriving (Show, Eq)
287-- | REPL commands
288data Command = Quit
289 | Help
290 | Eval PTerm
291 | NewDefn [PDecl] -- ^ Each 'PDecl' should be either a type declaration (at most one) or a clause defining the same name.
292 | Undefine [Name]
293 | Check PTerm
294 | DocStr (Either Name Const)
295 | TotCheck Name
296 | Reload
297 | Load FilePath (Maybe Int) -- up to maximum line number
298 | ChangeDirectory FilePath
299 | ModImport String
300 | Edit
301 | Compile Codegen String
302 | Execute
303 | ExecVal PTerm
304 | Metavars
305 | Prove Name
306 | AddProof (Maybe Name)
307 | RmProof Name
308 | ShowProof Name
309 | Proofs
310 | Universes
311 | LogLvl Int
312 | Spec PTerm
313 | HNF PTerm
314 | TestInline PTerm
315 | Defn Name
316 | Missing Name
317 | DynamicLink FilePath
318 | ListDynamic
319 | Pattelab PTerm
320 | DebugInfo Name
321 | Search PTerm
322 | CaseSplitAt Bool Int Name
323 | AddClauseFrom Bool Int Name
324 | AddProofClauseFrom Bool Int Name
325 | AddMissing Bool Int Name
326 | MakeWith Bool Int Name
327 | MakeLemma Bool Int Name
328 | DoProofSearch Bool Bool Int Name [Name]
329 -- ^ the first bool is whether to update,
330 -- the second is whether to search recursively (i.e. for the arguments)
331 | SetOpt Opt
332 | UnsetOpt Opt
333 | NOP
334 | SetColour ColourType IdrisColour
335 | ColourOn
336 | ColourOff
337 | ListErrorHandlers
338 | SetConsoleWidth ConsoleWidth
339 | Apropos String
340 | WhoCalls Name
341 | CallsWho Name
342 | MakeDoc String -- IdrisDoc
343 | Warranty
345data Opt = Filename String
346 | Quiet
347 | NoBanner
348 | ColourREPL Bool
349 | Ideslave
350 | ShowLibs
351 | ShowLibdir
352 | ShowIncs
353 | NoBasePkgs
354 | NoPrelude
355 | NoBuiltins -- only for the really primitive stuff!
356 | NoREPL
357 | OLogging Int
358 | Output String
359 | TypeCase
360 | TypeInType
361 | DefaultTotal
362 | DefaultPartial
363 | WarnPartial
364 | WarnReach
365 | NoCoverage
366 | ErrContext
367 | ShowImpl
368 | Verbose
369 | IBCSubDir String
370 | ImportDir String
371 | PkgBuild String
372 | PkgInstall String
373 | PkgClean String
374 | PkgCheck String
375 | PkgREPL String
376 | PkgMkDoc String -- IdrisDoc
377 | PkgTest String
378 | WarnOnly
379 | Pkg String
380 | BCAsm String
381 | DumpDefun String
382 | DumpCases String
383 | UseCodegen Codegen
384 | OutputTy OutputType
385 | Extension LanguageExt
386 | InterpretScript String
387 | EvalExpr String
388 | TargetTriple String
389 | TargetCPU String
390 | OptLevel Word
391 | Client String
392 | ShowOrigErr
393 | AutoWidth -- ^ Automatically adjust terminal width
394 | AutoSolve -- ^ Automatically issue "solve" tactic in interactive prover
395 deriving (Show, Eq)
397-- Parsed declarations
399data Fixity = Infixl { prec :: Int }
400 | Infixr { prec :: Int }
401 | InfixN { prec :: Int }
402 | PrefixN { prec :: Int }
403 deriving Eq
404{-!
405deriving instance Binary Fixity
406deriving instance NFData Fixity
407!-}
409instance Show Fixity where
410 show (Infixl i) = "infixl " ++ show i
411 show (Infixr i) = "infixr " ++ show i
412 show (InfixN i) = "infix " ++ show i
413 show (PrefixN i) = "prefix " ++ show i
415data FixDecl = Fix Fixity String
416 deriving Eq
418instance Show FixDecl where
419 show (Fix f s) = show f ++ " " ++ s
421{-!
422deriving instance Binary FixDecl
423deriving instance NFData FixDecl
424!-}
426instance Ord FixDecl where
427 compare (Fix x _) (Fix y _) = compare (prec x) (prec y)
430data Static = Static | Dynamic
431 deriving (Show, Eq)
432{-!
433deriving instance Binary Static
434deriving instance NFData Static
435!-}
437-- Mark bindings with their explicitness, and laziness
438data Plicity = Imp { pargopts :: [ArgOpt],
439 pstatic :: Static,
440 pparam :: Bool }
441 | Exp { pargopts :: [ArgOpt],
442 pstatic :: Static,
443 pparam :: Bool } -- this is a param (rather than index)
444 | Constraint { pargopts :: [ArgOpt],
445 pstatic :: Static }
446 | TacImp { pargopts :: [ArgOpt],
447 pstatic :: Static,
448 pscript :: PTerm }
449 deriving (Show, Eq)
451{-!
452deriving instance Binary Plicity
453deriving instance NFData Plicity
454!-}
456impl = Imp [] Dynamic False
457expl = Exp [] Dynamic False
458expl_param = Exp [] Dynamic True
459constraint = Constraint [] Dynamic
460tacimpl t = TacImp [] Dynamic t
462data FnOpt = Inlinable -- always evaluate when simplifying
463 | TotalFn | PartialFn | CoveringFn
464 | Coinductive | AssertTotal
465 | Dictionary -- type class dictionary, eval only when
466 -- a function argument, and further evaluation resutls
467 | Implicit -- implicit coercion
468 | CExport String -- export, with a C name
469 | ErrorHandler -- ^^ an error handler for use with the ErrorReflection extension
470 | ErrorReverse -- ^^ attempt to reverse normalise before showing in error
471 | Reflection -- a reflecting function, compile-time only
472 | Specialise [(Name, Maybe Int)] -- specialise it, freeze these names
473 deriving (Show, Eq)
474{-!
475deriving instance Binary FnOpt
476deriving instance NFData FnOpt
477!-}
479type FnOpts = [FnOpt]
481inlinable :: FnOpts -> Bool
482inlinable = elem Inlinable
484dictionary :: FnOpts -> Bool
485dictionary = elem Dictionary
488-- | Data declaration options
489data DataOpt = Codata -- ^ Set if the the data-type is coinductive
490 | DefaultEliminator -- ^ Set if an eliminator should be generated for data type
491 | DefaultCaseFun -- ^ Set if a case function should be generated for data type
492 | DataErrRev
493 deriving (Show, Eq)
495type DataOpts = [DataOpt]
497-- | Type provider - what to provide
498data ProvideWhat' t = ProvTerm t t -- ^ the first is the goal type, the second is the term
499 | ProvPostulate t -- ^ goal type must be Type, so only term
500 deriving (Show, Eq, Functor)
502type ProvideWhat = ProvideWhat' PTerm
504-- | Top-level declarations such as compiler directives, definitions,
505-- datatypes and typeclasses.
506data PDecl' t
507 = PFix FC Fixity [String] -- ^ Fixity declaration
508 | PTy Docstring [(Name, Docstring)] SyntaxInfo FC FnOpts Name t -- ^ Type declaration
509 | PPostulate Docstring SyntaxInfo FC FnOpts Name t -- ^ Postulate
510 | PClauses FC FnOpts Name [PClause' t] -- ^ Pattern clause
511 | PCAF FC Name t -- ^ Top level constant
512 | PData Docstring [(Name, Docstring)] SyntaxInfo FC DataOpts (PData' t) -- ^ Data declaration.
513 | PParams FC [(Name, t)] [PDecl' t] -- ^ Params block
514 | PNamespace String [PDecl' t] -- ^ New namespace
515 | PRecord Docstring SyntaxInfo FC Name t DataOpts Docstring Name t -- ^ Record declaration
516 | PClass Docstring SyntaxInfo FC
517 [t] -- constraints
518 Name
519 [(Name, t)] -- parameters
520 [(Name, Docstring)] -- parameter docstrings
521 [PDecl' t] -- declarations
522 -- ^ Type class: arguments are documentation, syntax info, source location, constraints,
523 -- class name, parameters, method declarations
524 | PInstance SyntaxInfo FC [t] -- constraints
525 Name -- class
526 [t] -- parameters
527 t -- full instance type
528 (Maybe Name) -- explicit name
529 [PDecl' t]
530 -- ^ Instance declaration: arguments are syntax info, source location, constraints,
531 -- class name, parameters, full instance type, optional explicit name, and definitions
532 | PDSL Name (DSL' t) -- ^ DSL declaration
533 | PSyntax FC Syntax -- ^ Syntax definition
534 | PMutual FC [PDecl' t] -- ^ Mutual block
535 | PDirective (Idris ()) -- ^ Compiler directive. The parser inserts the corresponding action in the Idris monad.
536 | PProvider SyntaxInfo FC (ProvideWhat' t) Name -- ^ Type provider. The first t is the type, the second is the term
537 | PTransform FC Bool t t -- ^ Source-to-source transformation rule. If
538 -- bool is True, lhs and rhs must be convertible
539 deriving Functor
540{-!
541deriving instance Binary PDecl'
542deriving instance NFData PDecl'
543!-}
545-- For elaborator state
546type ElabD a = Elab' [PDecl] a
548-- | One clause of a top-level definition. Term arguments to constructors are:
549--
550-- 1. The whole application (missing for PClauseR and PWithR because they're within a "with" clause)
551--
552-- 2. The list of extra 'with' patterns
553--
554-- 3. The right-hand side
555--
556-- 4. The where block (PDecl' t)
558data PClause' t = PClause FC Name t [t] t [PDecl' t] -- ^ A normal top-level definition.
559 | PWith FC Name t [t] t [PDecl' t]
560 | PClauseR FC [t] t [PDecl' t]
561 | PWithR FC [t] t [PDecl' t]
562 deriving Functor
563{-!
564deriving instance Binary PClause'
565deriving instance NFData PClause'
566!-}
568-- | Data declaration
569data PData' t = PDatadecl { d_name :: Name, -- ^ The name of the datatype
570 d_tcon :: t, -- ^ Type constructor
571 d_cons :: [(Docstring, [(Name, Docstring)], Name, t, FC, [Name])] -- ^ Constructors
572 }
573 -- ^ Data declaration
574 | PLaterdecl { d_name :: Name, d_tcon :: t }
575 -- ^ "Placeholder" for data whose constructors are defined later
576 deriving Functor
577{-!
578deriving instance Binary PData'
579deriving instance NFData PData'
580!-}
582-- Handy to get a free function for applying PTerm -> PTerm functions
583-- across a program, by deriving Functor
585type PDecl = PDecl' PTerm
586type PData = PData' PTerm
587type PClause = PClause' PTerm
589-- get all the names declared in a decl
591declared :: PDecl -> [Name]
592declared (PFix _ _ _) = []
593declared (PTy _ _ _ _ _ n t) = [n]
594declared (PPostulate _ _ _ _ n t) = [n]
595declared (PClauses _ _ n _) = [] -- not a declaration
596declared (PCAF _ n _) = [n]
597declared (PData _ _ _ _ _ (PDatadecl n _ ts)) = n : map fstt ts
598 where fstt (_, _, a, _, _, _) = a
599declared (PData _ _ _ _ _ (PLaterdecl n _)) = [n]
600declared (PParams _ _ ds) = concatMap declared ds
601declared (PNamespace _ ds) = concatMap declared ds
602declared (PRecord _ _ _ n _ _ _ c _) = [n, c]
603declared (PClass _ _ _ _ n _ _ ms) = n : concatMap declared ms
604declared (PInstance _ _ _ _ _ _ _ _) = []
605declared (PDSL n _) = [n]
606declared (PSyntax _ _) = []
607declared (PMutual _ ds) = concatMap declared ds
608declared (PDirective _) = []
610-- get the names declared, not counting nested parameter blocks
611tldeclared :: PDecl -> [Name]
612tldeclared (PFix _ _ _) = []
613tldeclared (PTy _ _ _ _ _ n t) = [n]
614tldeclared (PPostulate _ _ _ _ n t) = [n]
615tldeclared (PClauses _ _ n _) = [] -- not a declaration
616tldeclared (PRecord _ _ _ n _ _ _ c _) = [n, c]
617tldeclared (PData _ _ _ _ _ (PDatadecl n _ ts)) = n : map fstt ts
618 where fstt (_, _, a, _, _, _) = a
619tldeclared (PParams _ _ ds) = []
620tldeclared (PMutual _ ds) = concatMap tldeclared ds
621tldeclared (PNamespace _ ds) = concatMap tldeclared ds
622tldeclared (PClass _ _ _ _ n _ _ ms) = concatMap tldeclared ms
623tldeclared (PInstance _ _ _ _ _ _ _ _) = []
624tldeclared _ = []
626defined :: PDecl -> [Name]
627defined (PFix _ _ _) = []
628defined (PTy _ _ _ _ _ n t) = []
629defined (PPostulate _ _ _ _ n t) = []
630defined (PClauses _ _ n _) = [n] -- not a declaration
631defined (PCAF _ n _) = [n]
632defined (PData _ _ _ _ _ (PDatadecl n _ ts)) = n : map fstt ts
633 where fstt (_, _, a, _, _, _) = a
634defined (PData _ _ _ _ _ (PLaterdecl n _)) = []
635defined (PParams _ _ ds) = concatMap defined ds
636defined (PNamespace _ ds) = concatMap defined ds
637defined (PRecord _ _ _ n _ _ _ c _) = [n, c]
638defined (PClass _ _ _ _ n _ _ ms) = n : concatMap defined ms
639defined (PInstance _ _ _ _ _ _ _ _) = []
640defined (PDSL n _) = [n]
641defined (PSyntax _ _) = []
642defined (PMutual _ ds) = concatMap defined ds
643defined (PDirective _) = []
644--defined _ = []
646updateN :: [(Name, Name)] -> Name -> Name
647updateN ns n | Just n' <- lookup n ns = n'
648updateN _ n = n
650updateNs :: [(Name, Name)] -> PTerm -> PTerm
651updateNs [] t = t
652updateNs ns t = mapPT updateRef t
653 where updateRef (PRef fc f) = PRef fc (updateN ns f)
654 updateRef t = t
656-- updateDNs :: [(Name, Name)] -> PDecl -> PDecl
657-- updateDNs [] t = t
658-- updateDNs ns (PTy s f n t) | Just n' <- lookup n ns = PTy s f n' t
659-- updateDNs ns (PClauses f n c) | Just n' <- lookup n ns = PClauses f n' (map updateCNs c)
660-- where updateCNs ns (PClause n l ts r ds)
661-- = PClause (updateN ns n) (fmap (updateNs ns) l)
662-- (map (fmap (updateNs ns)) ts)
663-- (fmap (updateNs ns) r)
664-- (map (updateDNs ns) ds)
665-- updateDNs ns c = c
667data PunInfo = IsType | IsTerm | TypeOrTerm deriving (Eq, Show)
669-- | High level language terms
670data PTerm = PQuote Raw
671 | PRef FC Name
672 | PInferRef FC Name -- ^ A name to be defined later
673 | PPatvar FC Name
674 | PLam Name PTerm PTerm
675 | PPi Plicity Name PTerm PTerm -- ^ (n : t1) -> t2
676 | PLet Name PTerm PTerm PTerm
677 | PTyped PTerm PTerm -- ^ Term with explicit type
678 | PApp FC PTerm [PArg] -- ^ e.g. IO (), List Char, length x
679 | PAppBind FC PTerm [PArg] -- ^ implicitly bound application
680 | PMatchApp FC Name -- ^ Make an application by type matching
681 | PCase FC PTerm [(PTerm, PTerm)]
682 | PTrue FC PunInfo -- ^ Unit type..?
683 | PFalse FC -- ^ _|_
684 | PRefl FC PTerm
685 | PResolveTC FC
686 | PEq FC PTerm PTerm PTerm PTerm -- ^ Heterogeneous equality type: A = B
687 | PRewrite FC PTerm PTerm (Maybe PTerm)
688 | PPair FC PunInfo PTerm PTerm
689 | PDPair FC PunInfo PTerm PTerm PTerm
690 | PAlternative Bool [PTerm] -- True if only one may work
691 | PHidden PTerm -- ^ Irrelevant or hidden pattern
692 | PType -- ^ 'Type' type
693 | PGoal FC PTerm Name PTerm
694 | PConstant Const -- ^ Builtin types
695 | Placeholder
696 | PDoBlock [PDo]
697 | PIdiom FC PTerm
698 | PReturn FC
699 | PMetavar Name
700 | PProof [PTactic] -- ^ Proof script
701 | PTactics [PTactic] -- ^ As PProof, but no auto solving
702 | PElabError Err -- ^ Error to report on elaboration
703 | PImpossible -- ^ Special case for declaring when an LHS can't typecheck
704 | PCoerced PTerm -- ^ To mark a coerced argument, so as not to coerce twice
705 | PDisamb [[T.Text]] PTerm -- ^ Preferences for explicit namespaces
706 | PUnifyLog PTerm -- ^ dump a trace of unifications when building term
707 | PNoImplicits PTerm -- ^ never run implicit converions on the term
708 | PQuasiquote PTerm (Maybe PTerm) -- ^ `(Term [: Term])
709 | PUnquote PTerm -- ^ ,Term
710 deriving Eq
713{-!
714deriving instance Binary PTerm
715deriving instance NFData PTerm
716!-}
718mapPT :: (PTerm -> PTerm) -> PTerm -> PTerm
719mapPT f t = f (mpt t) where
720 mpt (PLam n t s) = PLam n (mapPT f t) (mapPT f s)
721 mpt (PPi p n t s) = PPi p n (mapPT f t) (mapPT f s)
722 mpt (PLet n ty v s) = PLet n (mapPT f ty) (mapPT f v) (mapPT f s)
723 mpt (PRewrite fc t s g) = PRewrite fc (mapPT f t) (mapPT f s)
724 (fmap (mapPT f) g)
725 mpt (PApp fc t as) = PApp fc (mapPT f t) (map (fmap (mapPT f)) as)
726 mpt (PAppBind fc t as) = PAppBind fc (mapPT f t) (map (fmap (mapPT f)) as)
727 mpt (PCase fc c os) = PCase fc (mapPT f c) (map (pmap (mapPT f)) os)
728 mpt (PEq fc lt rt l r) = PEq fc (mapPT f lt) (mapPT f rt) (mapPT f l) (mapPT f r)
729 mpt (PTyped l r) = PTyped (mapPT f l) (mapPT f r)
730 mpt (PPair fc p l r) = PPair fc p (mapPT f l) (mapPT f r)
731 mpt (PDPair fc p l t r) = PDPair fc p (mapPT f l) (mapPT f t) (mapPT f r)
732 mpt (PAlternative a as) = PAlternative a (map (mapPT f) as)
733 mpt (PHidden t) = PHidden (mapPT f t)
734 mpt (PDoBlock ds) = PDoBlock (map (fmap (mapPT f)) ds)
735 mpt (PProof ts) = PProof (map (fmap (mapPT f)) ts)
736 mpt (PTactics ts) = PTactics (map (fmap (mapPT f)) ts)
737 mpt (PUnifyLog tm) = PUnifyLog (mapPT f tm)
738 mpt (PDisamb ns tm) = PDisamb ns (mapPT f tm)
739 mpt (PNoImplicits tm) = PNoImplicits (mapPT f tm)
740 mpt (PGoal fc r n sc) = PGoal fc (mapPT f r) n (mapPT f sc)
741 mpt x = x
744data PTactic' t = Intro [Name] | Intros | Focus Name
745 | Refine Name [Bool] | Rewrite t | DoUnify
746 | Induction t
747 | CaseTac t
748 | Equiv t
749 | MatchRefine Name
750 | LetTac Name t | LetTacTy Name t t
751 | Exact t | Compute | Trivial | TCInstance
752 | ProofSearch Bool Bool Int (Maybe Name) [Name]
753 -- ^ the bool is whether to search recursively
754 | Solve
755 | Attack
756 | ProofState | ProofTerm | Undo
757 | Try (PTactic' t) (PTactic' t)
758 | TSeq (PTactic' t) (PTactic' t)
759 | ApplyTactic t -- see Language.Reflection module
760 | ByReflection t
761 | Reflect t
762 | Fill t
763 | GoalType String (PTactic' t)
764 | TCheck t
765 | TEval t
766 | TDocStr (Either Name Const)
767 | TSearch t
768 | Qed | Abandon
769 deriving (Show, Eq, Functor)
770{-!
771deriving instance Binary PTactic'
772deriving instance NFData PTactic'
773!-}
774instance Sized a => Sized (PTactic' a) where
775 size (Intro nms) = 1 + size nms
776 size Intros = 1
777 size (Focus nm) = 1 + size nm
778 size (Refine nm bs) = 1 + size nm + length bs
779 size (Rewrite t) = 1 + size t
780 size (Induction t) = 1 + size t
781 size (LetTac nm t) = 1 + size nm + size t
782 size (Exact t) = 1 + size t
783 size Compute = 1
784 size Trivial = 1
785 size Solve = 1
786 size Attack = 1
787 size ProofState = 1
788 size ProofTerm = 1
789 size Undo = 1
790 size (Try l r) = 1 + size l + size r
791 size (TSeq l r) = 1 + size l + size r
792 size (ApplyTactic t) = 1 + size t
793 size (Reflect t) = 1 + size t
794 size (Fill t) = 1 + size t
795 size Qed = 1
796 size Abandon = 1
798type PTactic = PTactic' PTerm
800data PDo' t = DoExp FC t
801 | DoBind FC Name t
802 | DoBindP FC t t [(t,t)]
803 | DoLet FC Name t t
804 | DoLetP FC t t
805 deriving (Eq, Functor)
806{-!
807deriving instance Binary PDo'
808deriving instance NFData PDo'
809!-}
811instance Sized a => Sized (PDo' a) where
812 size (DoExp fc t) = 1 + size fc + size t
813 size (DoBind fc nm t) = 1 + size fc + size nm + size t
814 size (DoBindP fc l r alts) = 1 + size fc + size l + size r + size alts
815 size (DoLet fc nm l r) = 1 + size fc + size nm + size l + size r
816 size (DoLetP fc l r) = 1 + size fc + size l + size r
818type PDo = PDo' PTerm
820-- The priority gives a hint as to elaboration order. Best to elaborate
821-- things early which will help give a more concrete type to other
822-- variables, e.g. a before (interpTy a).
824data PArg' t = PImp { priority :: Int,
825 machine_inf :: Bool, -- true if the machine inferred it
826 argopts :: [ArgOpt],
827 pname :: Name, getTm :: t }
828 | PExp { priority :: Int,
829 argopts :: [ArgOpt],
830 pname :: Name,
831 getTm :: t }
832 | PConstraint { priority :: Int,
833 argopts :: [ArgOpt],
834 pname :: Name,
835 getTm :: t }
836 | PTacImplicit { priority :: Int,
837 argopts :: [ArgOpt],
838 pname :: Name,
839 getScript :: t,
840 getTm :: t }
841 deriving (Show, Eq, Functor)
843data ArgOpt = AlwaysShow | HideDisplay | InaccessibleArg
844 deriving (Show, Eq)
846instance Sized a => Sized (PArg' a) where
847 size (PImp p _ l nm trm) = 1 + size nm + size trm
848 size (PExp p l nm trm) = 1 + size nm + size trm
849 size (PConstraint p l nm trm) = 1 + size nm +size nm + size trm
850 size (PTacImplicit p l nm scr trm) = 1 + size nm + size scr + size trm
852{-!
853deriving instance Binary PArg'
854deriving instance NFData PArg'
855!-}
857pimp n t mach = PImp 1 mach [] n t
858pexp t = PExp 1 [] (sMN 0 "arg") t
859pconst t = PConstraint 1 [] (sMN 0 "carg") t
860ptacimp n s t = PTacImplicit 2 [] n s t
862type PArg = PArg' PTerm
864-- Type class data
866data ClassInfo = CI { instanceName :: Name,
867 class_methods :: [(Name, (FnOpts, PTerm))],
868 class_defaults :: [(Name, (Name, PDecl))], -- method name -> default impl
869 class_default_superclasses :: [PDecl],
870 class_params :: [Name],
871 class_instances :: [Name] }
872 deriving Show
873{-!
874deriving instance Binary ClassInfo
875deriving instance NFData ClassInfo
876!-}
878-- Type inference data
880data TIData = TIPartial -- ^ a function with a partially defined type
881 | TISolution [Term] -- ^ possible solutions to a metavariable in a type
882 deriving Show
884data OptInfo = Optimise { inaccessible :: [(Int,Name)], -- includes names for error reporting
885 detaggable :: Bool }
886 deriving Show
887{-!
888deriving instance Binary OptInfo
889deriving instance NFData OptInfo
890!-}
893data TypeInfo = TI { con_names :: [Name],
894 codata :: Bool,
895 data_opts :: DataOpts,
896 param_pos :: [Int],
897 mutual_types :: [Name] }
898 deriving Show
899{-!
900deriving instance Binary TypeInfo
901deriving instance NFData TypeInfo
902!-}
904-- Syntactic sugar info
906data DSL' t = DSL { dsl_bind :: t,
907 dsl_return :: t,
908 dsl_apply :: t,
909 dsl_pure :: t,
910 dsl_var :: Maybe t,
911 index_first :: Maybe t,
912 index_next :: Maybe t,
913 dsl_lambda :: Maybe t,
914 dsl_let :: Maybe t,
915 dsl_pi :: Maybe t
916 }
917 deriving (Show, Functor)
918{-!
919deriving instance Binary DSL'
920deriving instance NFData DSL'
921!-}
923type DSL = DSL' PTerm
925data SynContext = PatternSyntax | TermSyntax | AnySyntax
926 deriving Show
927{-!
928deriving instance Binary SynContext
929deriving instance NFData SynContext
930!-}
932data Syntax = Rule [SSymbol] PTerm SynContext
933 deriving Show
934{-!
935deriving instance Binary Syntax
936deriving instance NFData Syntax
937!-}
939data SSymbol = Keyword Name
940 | Symbol String
941 | Binding Name
942 | Expr Name
943 | SimpleExpr Name
944 deriving Show
945{-!
946deriving instance Binary SSymbol
947deriving instance NFData SSymbol
948!-}
950initDSL = DSL (PRef f (sUN ">>="))
951 (PRef f (sUN "return"))
952 (PRef f (sUN "<$>"))
953 (PRef f (sUN "pure"))
954 Nothing
955 Nothing
956 Nothing
957 Nothing
958 Nothing
959 Nothing
960 where f = fileFC "(builtin)"
962data Using = UImplicit Name PTerm
963 | UConstraint Name [Name]
964 deriving (Show, Eq)
965{-!
966deriving instance Binary Using
967deriving instance NFData Using
968!-}
970data SyntaxInfo = Syn { using :: [Using],
971 syn_params :: [(Name, PTerm)],
972 syn_namespace :: [String],
973 no_imp :: [Name],
974 decoration :: Name -> Name,
975 inPattern :: Bool,
976 implicitAllowed :: Bool,
977 maxline :: Maybe Int,
978 mut_nesting :: Int,
979 dsl_info :: DSL,
980 syn_in_quasiquote :: Bool }
981 deriving Show
982{-!
983deriving instance NFData SyntaxInfo
984deriving instance Binary SyntaxInfo
985!-}
987defaultSyntax = Syn [] [] [] [] id False False Nothing 0 initDSL False
989expandNS :: SyntaxInfo -> Name -> Name
990expandNS syn n@(NS _ _) = n
991expandNS syn n = case syn_namespace syn of
992 [] -> n
993 xs -> sNS n xs
996-- For inferring types of things
998bi = fileFC "builtin"
1000inferTy = sMN 0 "__Infer"
1001inferCon = sMN 0 "__infer"
1002inferDecl = PDatadecl inferTy
1003 PType
1004 [(emptyDocstring, [], inferCon, PPi impl (sMN 0 "iType") PType (
1005 PPi expl (sMN 0 "ival") (PRef bi (sMN 0 "iType"))
1006 (PRef bi inferTy)), bi, [])]
1007inferOpts = []
1009infTerm t = PApp bi (PRef bi inferCon) [pimp (sMN 0 "iType") Placeholder True, pexp t]
1010infP = P (TCon 6 0) inferTy (TType (UVal 0))
1012getInferTerm, getInferType :: Term -> Term
1013getInferTerm (Bind n b sc) = Bind n b $ getInferTerm sc
1014getInferTerm (App (App _ _) tm) = tm
1015getInferTerm tm = tm -- error ("getInferTerm " ++ show tm)
1017getInferType (Bind n b sc) = Bind n (toTy b) $ getInferType sc
1018 where toTy (Lam t) = Pi t
1019 toTy (PVar t) = PVTy t
1020 toTy b = b
1021getInferType (App (App _ ty) _) = ty
1025-- Handy primitives: Unit, False, Pair, MkPair, =, mkForeign, Elim type class
1027primNames = [unitTy, unitCon,
1028 falseTy, pairTy, pairCon,
1029 eqTy, eqCon, inferTy, inferCon]
1031unitDoc = parseDocstring . T.pack $ "The canonical single-element type, also known as the trivially true proposition."
1032unitTy = sMN 0 "__Unit"
1033unitCon = sMN 0 "__II"
1034unitDecl = PDatadecl unitTy PType
1035 [(parseDocstring . T.pack $ "The trivial constructor for `()`. ", [], unitCon, PRef bi unitTy, bi, [])]
1036unitOpts = [DefaultEliminator]
1038falseDoc = parseDocstring . T.pack $
1039 "The empty type, also known as the trivially false proposition." ++
1040 "\n\n" ++
1041 "Use `FalseElim` or `absurd` to prove anything if you have a variable " ++
1042 "of type `_|_` in scope."
1043falseTy = sMN 0 "__False"
1044falseDecl = PDatadecl falseTy PType []
1045falseOpts = []
1047pairDoc = parseDocstring . T.pack $ "The non-dependent pair type, also known as conjunction."
1048pairTy = sMN 0 "__Pair"
1049pairCon = sMN 0 "__MkPair"
1050pairDecl = PDatadecl pairTy (piBind [(n "A", PType), (n "B", PType)] PType)
1051 [(pairConDoc, pairConParamDoc,
1052 pairCon, PPi impl (n "A") PType (
1053 PPi impl (n "B") PType (
1054 PPi expl (n "a") (PRef bi (n "A")) (
1055 PPi expl (n "b") (PRef bi (n "B"))
1056 (PApp bi (PRef bi pairTy) [pexp (PRef bi (n "A")),
1057 pexp (PRef bi (n "B"))])))), bi, [])]
1058 where n a = sMN 0 a
1059 pairConDoc = parseDocstring . T.pack $ "A pair of elements"
1060 pairConParamDoc = [(n "a", parseDocstring . T.pack $ "the left element of the pair"),
1061 (n "b", parseDocstring . T.pack $ "the right element of the pair")]
1062pairOpts = []
1063pairParamDoc = [(n "A", parseDocstring . T.pack $ "the type of the left elements in the pair"),
1064 (n "B", parseDocstring . T.pack $ "the type of the left elements in the pair")]
1065 where n a = sMN 0 a
1067eqTy = sUN "="
1068eqCon = sUN "refl"
1069eqDoc = parseDocstring . T.pack $
1070 "The propositional equality type. A proof that `x` = `y`." ++
1071 "\n\n" ++
1072 "To use such a proof, pattern-match on it, and the two equal things will " ++
1073 "then need to be the _same_ pattern." ++
1074 "\n\n" ++
1075 "**Note**: Idris's equality type is potentially _heterogeneous_, which means that it " ++
1076 "is possible to state equalities between values of potentially different " ++
1077 "types. However, Idris will attempt the homogeneous case unless it fails to typecheck." ++
1078 "\n\n" ++
1079 "You may need to use `(~=~)` to explicitly request heterogeneous equality."
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 -> []