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