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