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