git.iko.soy/Idris-dev
on 0c1bc8d help sign in
Idris-dev/src/Idris/AbsSyntaxTree.hs
1695 lines 67 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 Paths_idris
20import System.Console.Haskeline
21import System.IO
23import Control.Monad.Trans.State.Strict
24import Control.Monad.Trans.Error
26import Data.List hiding (group)
27import Data.Char
28import qualified Data.Map as M
29import qualified Data.Text as T
30import qualified Data.Map as M
31import Data.Either
32import qualified Data.Set as S
33import Data.Word (Word)
34import Data.Maybe (fromMaybe)
36import Debug.Trace
38import Text.PrettyPrint.Annotated.Leijen
40-- Data to pass to recursively called elaborators; e.g. for where blocks,
41-- paramaterised declarations, etc.
43data ElabInfo = EInfo { params :: [(Name, PTerm)],
44 inblock :: Ctxt [Name], -- names in the block, and their params
45 liftname :: Name -> Name,
46 namespace :: Maybe [String] }
48toplevel = EInfo [] emptyContext id Nothing
50eInfoNames :: ElabInfo -> [Name]
51eInfoNames info = map fst (params info) ++ M.keys (inblock info)
53data IOption = IOption { opt_logLevel :: Int,
54 opt_typecase :: Bool,
55 opt_typeintype :: Bool,
56 opt_coverage :: Bool,
57 opt_showimp :: Bool, -- ^^ show implicits
58 opt_errContext :: Bool,
59 opt_repl :: Bool,
60 opt_verbose :: Bool,
61 opt_nobanner :: Bool,
62 opt_quiet :: Bool,
63 opt_codegen :: Codegen,
64 opt_outputTy :: OutputType,
65 opt_ibcsubdir :: FilePath,
66 opt_importdirs :: [FilePath],
67 opt_triple :: String,
68 opt_cpu :: String,
69 opt_optLevel :: Word,
70 opt_cmdline :: [Opt], -- remember whole command line
71 opt_origerr :: Bool,
72 opt_autoSolve :: Bool -- ^ automatically apply "solve" tactic in prover
73 }
74 deriving (Show, Eq)
76defaultOpts = IOption { opt_logLevel = 0
77 , opt_typecase = False
78 , opt_typeintype = False
79 , opt_coverage = True
80 , opt_showimp = False
81 , opt_errContext = False
82 , opt_repl = True
83 , opt_verbose = True
84 , opt_nobanner = False
85 , opt_quiet = False
86 , opt_codegen = ViaC
87 , opt_outputTy = Executable
88 , opt_ibcsubdir = ""
89 , opt_importdirs = []
90 , opt_triple = ""
91 , opt_cpu = ""
92 , opt_optLevel = 2
93 , opt_cmdline = []
94 , opt_origerr = False
95 , opt_autoSolve = True
96 }
98data PPOption = PPOption {
99 ppopt_impl :: Bool -- ^^ whether to show implicits
100} deriving (Show)
102-- | Pretty printing options with default verbosity.
103defaultPPOption :: PPOption
104defaultPPOption = PPOption { ppopt_impl = False }
106-- | Pretty printing options with the most verbosity.
107verbosePPOption :: PPOption
108verbosePPOption = PPOption { ppopt_impl = True }
110-- | Get pretty printing options from the big options record.
111ppOption :: IOption -> PPOption
112ppOption opt = PPOption {
113 ppopt_impl = opt_showimp opt
116-- | Get pretty printing options from an idris state record.
117ppOptionIst :: IState -> PPOption
118ppOptionIst = ppOption . idris_options
120data LanguageExt = TypeProviders | ErrorReflection deriving (Show, Eq, Read, Ord)
122-- | The output mode in use
123data OutputMode = RawOutput | IdeSlave Integer deriving Show
125-- | How wide is the console?
126data ConsoleWidth = InfinitelyWide -- ^ Have pretty-printer assume that lines should not be broken
127 | ColsWide Int -- ^ Manually specified - must be positive
128 | AutomaticWidth -- ^ Attempt to determine width, or 80 otherwise
130-- | The global state used in the Idris monad
131data IState = IState {
132 tt_ctxt :: Context, -- ^ All the currently defined names and their terms
133 idris_constraints :: [(UConstraint, FC)],
134 -- ^ A list of universe constraints and their corresponding source locations
135 idris_infixes :: [FixDecl], -- ^ Currently defined infix operators
136 idris_implicits :: Ctxt [PArg],
137 idris_statics :: Ctxt [Bool],
138 idris_classes :: Ctxt ClassInfo,
139 idris_dsls :: Ctxt DSL,
140 idris_optimisation :: Ctxt OptInfo,
141 idris_datatypes :: Ctxt TypeInfo,
142 idris_namehints :: Ctxt [Name],
143 idris_patdefs :: Ctxt ([([Name], Term, Term)], [PTerm]), -- not exported
144 -- ^ list of lhs/rhs, and a list of missing clauses
145 idris_flags :: Ctxt [FnOpt],
146 idris_callgraph :: Ctxt CGInfo, -- name, args used in each pos
147 idris_calledgraph :: Ctxt [Name],
148 idris_docstrings :: Ctxt (Docstring, [(Name, Docstring)]),
149 idris_tyinfodata :: Ctxt TIData,
150 idris_totcheck :: [(FC, Name)], -- names to check totality on
151 idris_defertotcheck :: [(FC, Name)], -- names to check at the end
152 idris_totcheckfail :: [(FC, String)],
153 idris_options :: IOption,
154 idris_name :: Int,
155 idris_lineapps :: [((FilePath, Int), PTerm)],
156 -- ^ Full application LHS on source line
157 idris_metavars :: [(Name, (Maybe Name, Int, Bool))], -- ^ The currently defined but not proven metavariables
158 idris_coercions :: [Name],
159 idris_transforms :: [(Term, Term)],
160 idris_errRev :: [(Term, Term)],
161 syntax_rules :: [Syntax],
162 syntax_keywords :: [String],
163 imported :: [FilePath], -- ^ The imported modules
164 idris_scprims :: [(Name, (Int, PrimFn))],
165 idris_objs :: [(Codegen, FilePath)],
166 idris_libs :: [(Codegen, String)],
167 idris_cgflags :: [(Codegen, String)],
168 idris_hdrs :: [(Codegen, String)],
169 idris_imported :: [FilePath], -- ^ Imported ibc file names
170 proof_list :: [(Name, [String])],
171 errSpan :: Maybe FC,
172 parserWarnings :: [(FC, Err)],
173 lastParse :: Maybe Name,
174 indent_stack :: [Int],
175 brace_stack :: [Maybe Int],
176 lastTokenSpan :: Maybe FC, -- ^ What was the span of the latest token parsed?
177 hide_list :: [(Name, Maybe Accessibility)],
178 default_access :: Accessibility,
179 default_total :: Bool,
180 ibc_write :: [IBCWrite],
181 compiled_so :: Maybe String,
182 idris_dynamic_libs :: [DynamicLib],
183 idris_language_extensions :: [LanguageExt],
184 idris_outputmode :: OutputMode,
185 idris_colourRepl :: Bool,
186 idris_colourTheme :: ColourTheme,
187 idris_outh :: Handle,
188 idris_errorhandlers :: [Name], -- ^ Global error handlers
189 idris_nameIdx :: (Int, Ctxt (Int, Name)),
190 idris_function_errorhandlers :: Ctxt (M.Map Name (S.Set Name)), -- ^ Specific error handlers
191 module_aliases :: M.Map [T.Text] [T.Text],
192 idris_consolewidth :: ConsoleWidth, -- ^ How many chars wide is the console?
193 idris_postulates :: S.Set Name,
194 idris_whocalls :: Maybe (M.Map Name [Name]),
195 idris_callswho :: Maybe (M.Map Name [Name])
196 }
198data SizeChange = Smaller | Same | Bigger | Unknown
199 deriving (Show, Eq)
200{-!
201deriving instance Binary SizeChange
202deriving instance NFData SizeChange
203!-}
205type SCGEntry = (Name, [Maybe (Int, SizeChange)])
206type UsageReason = (Name, Int) -- fn_name, its_arg_number
208data CGInfo = CGInfo { argsdef :: [Name],
209 calls :: [(Name, [[Name]])],
210 scg :: [SCGEntry],
211 argsused :: [Name],
212 usedpos :: [(Int, [UsageReason])] }
213 deriving Show
214{-!
215deriving instance Binary CGInfo
216deriving instance NFData CGInfo
217!-}
219primDefs = [sUN "unsafePerformPrimIO",
220 sUN "mkLazyForeignPrim",
221 sUN "mkForeignPrim",
222 sUN "FalseElim"]
224-- information that needs writing for the current module's .ibc file
225data IBCWrite = IBCFix FixDecl
226 | IBCImp Name
227 | IBCStatic Name
228 | IBCClass Name
229 | IBCInstance Bool Name Name
230 | IBCDSL Name
231 | IBCData Name
232 | IBCOpt Name
233 | IBCMetavar Name
234 | IBCSyntax Syntax
235 | IBCKeyword String
236 | IBCImport FilePath
237 | IBCObj Codegen FilePath
238 | IBCLib Codegen String
239 | IBCCGFlag Codegen String
240 | IBCDyLib String
241 | IBCHeader Codegen String
242 | IBCAccess Name Accessibility
243 | IBCMetaInformation Name MetaInformation
244 | IBCTotal Name Totality
245 | IBCFlags Name [FnOpt]
246 | IBCTrans (Term, Term)
247 | IBCErrRev (Term, Term)
248 | IBCCG Name
249 | IBCDoc Name
250 | IBCCoercion Name
251 | IBCDef Name -- i.e. main context
252 | IBCNameHint (Name, Name)
253 | IBCLineApp FilePath Int PTerm
254 | IBCErrorHandler Name
255 | IBCFunctionErrorHandler Name Name Name
256 | IBCPostulate Name
257 | IBCTotCheckErr FC String
258 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 [] 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
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 | DoProofSearch Bool Bool Int Name [Name]
325 -- ^ the first bool is whether to update,
326 -- the second is whether to search recursively (i.e. for the arguments)
327 | SetOpt Opt
328 | UnsetOpt Opt
329 | NOP
330 | SetColour ColourType IdrisColour
331 | ColourOn
332 | ColourOff
333 | ListErrorHandlers
334 | SetConsoleWidth ConsoleWidth
335 | Apropos String
336 | WhoCalls Name
337 | CallsWho Name
338 | MakeDoc String -- IdrisDoc
341data Opt = Filename String
342 | Ver
343 | Usage
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 | 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 | DataErrRev
489 deriving (Show, Eq)
491type DataOpts = [DataOpt]
493-- | Type provider - what to provide
494data ProvideWhat = ProvTerm -- ^ only allow providing terms
495 | ProvPostulate -- ^ only allow postulates
496 | ProvAny -- ^ either is ok
497 deriving (Show, Eq)
499-- | Top-level declarations such as compiler directives, definitions,
500-- datatypes and typeclasses.
501data PDecl' t
502 = PFix FC Fixity [String] -- ^ Fixity declaration
503 | PTy Docstring [(Name, Docstring)] SyntaxInfo FC FnOpts Name t -- ^ Type declaration
504 | PPostulate Docstring SyntaxInfo FC FnOpts Name t -- ^ Postulate
505 | PClauses FC FnOpts Name [PClause' t] -- ^ Pattern clause
506 | PCAF FC Name t -- ^ Top level constant
507 | PData Docstring [(Name, Docstring)] SyntaxInfo FC DataOpts (PData' t) -- ^ Data declaration.
508 | PParams FC [(Name, t)] [PDecl' t] -- ^ Params block
509 | PNamespace String [PDecl' t] -- ^ New namespace
510 | PRecord Docstring SyntaxInfo FC Name t DataOpts Docstring Name t -- ^ Record declaration
511 | PClass Docstring SyntaxInfo FC
512 [t] -- constraints
513 Name
514 [(Name, t)] -- parameters
515 [(Name, Docstring)] -- parameter docstrings
516 [PDecl' t] -- declarations
517 -- ^ Type class: arguments are documentation, syntax info, source location, constraints,
518 -- class name, parameters, method declarations
519 | PInstance SyntaxInfo FC [t] -- constraints
520 Name -- class
521 [t] -- parameters
522 t -- full instance type
523 (Maybe Name) -- explicit name
524 [PDecl' t]
525 -- ^ Instance declaration: arguments are syntax info, source location, constraints,
526 -- class name, parameters, full instance type, optional explicit name, and definitions
527 | PDSL Name (DSL' t) -- ^ DSL declaration
528 | PSyntax FC Syntax -- ^ Syntax definition
529 | PMutual FC [PDecl' t] -- ^ Mutual block
530 | PDirective (Idris ()) -- ^ Compiler directive. The parser inserts the corresponding action in the Idris monad.
531 | PProvider SyntaxInfo FC ProvideWhat Name t t -- ^ Type provider. The first t is the type, the second is the term
532 | PTransform FC Bool t t -- ^ Source-to-source transformation rule. If
533 -- bool is True, lhs and rhs must be convertible
534 deriving Functor
535{-!
536deriving instance Binary PDecl'
537deriving instance NFData PDecl'
538!-}
540-- For elaborator state
541type ElabD a = Elab' [PDecl] a
543-- | One clause of a top-level definition. Term arguments to constructors are:
544--
545-- 1. The whole application (missing for PClauseR and PWithR because they're within a "with" clause)
546--
547-- 2. The list of extra 'with' patterns
548--
549-- 3. The right-hand side
550--
551-- 4. The where block (PDecl' t)
553data PClause' t = PClause FC Name t [t] t [PDecl' t] -- ^ A normal top-level definition.
554 | PWith FC Name t [t] t [PDecl' t]
555 | PClauseR FC [t] t [PDecl' t]
556 | PWithR FC [t] t [PDecl' t]
557 deriving Functor
558{-!
559deriving instance Binary PClause'
560deriving instance NFData PClause'
561!-}
563-- | Data declaration
564data PData' t = PDatadecl { d_name :: Name, -- ^ The name of the datatype
565 d_tcon :: t, -- ^ Type constructor
566 d_cons :: [(Docstring, [(Name, Docstring)], Name, t, FC, [Name])] -- ^ Constructors
567 }
568 -- ^ Data declaration
569 | PLaterdecl { d_name :: Name, d_tcon :: t }
570 -- ^ "Placeholder" for data whose constructors are defined later
571 deriving Functor
572{-!
573deriving instance Binary PData'
574deriving instance NFData PData'
575!-}
577-- Handy to get a free function for applying PTerm -> PTerm functions
578-- across a program, by deriving Functor
580type PDecl = PDecl' PTerm
581type PData = PData' PTerm
582type PClause = PClause' PTerm
584-- get all the names declared in a decl
586declared :: PDecl -> [Name]
587declared (PFix _ _ _) = []
588declared (PTy _ _ _ _ _ n t) = [n]
589declared (PPostulate _ _ _ _ n t) = [n]
590declared (PClauses _ _ n _) = [] -- not a declaration
591declared (PCAF _ n _) = [n]
592declared (PData _ _ _ _ _ (PDatadecl n _ ts)) = n : map fstt ts
593 where fstt (_, _, a, _, _, _) = a
594declared (PData _ _ _ _ _ (PLaterdecl n _)) = [n]
595declared (PParams _ _ ds) = concatMap declared ds
596declared (PNamespace _ ds) = concatMap declared ds
597declared (PRecord _ _ _ n _ _ _ c _) = [n, c]
598declared (PClass _ _ _ _ n _ _ ms) = n : concatMap declared ms
599declared (PInstance _ _ _ _ _ _ _ _) = []
600declared (PDSL n _) = [n]
601declared (PSyntax _ _) = []
602declared (PMutual _ ds) = concatMap declared ds
603declared (PDirective _) = []
605-- get the names declared, not counting nested parameter blocks
606tldeclared :: PDecl -> [Name]
607tldeclared (PFix _ _ _) = []
608tldeclared (PTy _ _ _ _ _ n t) = [n]
609tldeclared (PPostulate _ _ _ _ n t) = [n]
610tldeclared (PClauses _ _ n _) = [] -- not a declaration
611tldeclared (PRecord _ _ _ n _ _ _ c _) = [n, c]
612tldeclared (PData _ _ _ _ _ (PDatadecl n _ ts)) = n : map fstt ts
613 where fstt (_, _, a, _, _, _) = a
614tldeclared (PParams _ _ ds) = []
615tldeclared (PMutual _ ds) = concatMap tldeclared ds
616tldeclared (PNamespace _ ds) = concatMap tldeclared ds
617tldeclared (PClass _ _ _ _ n _ _ ms) = concatMap tldeclared ms
618tldeclared (PInstance _ _ _ _ _ _ _ _) = []
619tldeclared _ = []
621defined :: PDecl -> [Name]
622defined (PFix _ _ _) = []
623defined (PTy _ _ _ _ _ n t) = []
624defined (PPostulate _ _ _ _ n t) = []
625defined (PClauses _ _ n _) = [n] -- not a declaration
626defined (PCAF _ n _) = [n]
627defined (PData _ _ _ _ _ (PDatadecl n _ ts)) = n : map fstt ts
628 where fstt (_, _, a, _, _, _) = a
629defined (PData _ _ _ _ _ (PLaterdecl n _)) = []
630defined (PParams _ _ ds) = concatMap defined ds
631defined (PNamespace _ ds) = concatMap defined ds
632defined (PRecord _ _ _ n _ _ _ c _) = [n, c]
633defined (PClass _ _ _ _ n _ _ ms) = n : concatMap defined ms
634defined (PInstance _ _ _ _ _ _ _ _) = []
635defined (PDSL n _) = [n]
636defined (PSyntax _ _) = []
637defined (PMutual _ ds) = concatMap defined ds
638defined (PDirective _) = []
639--defined _ = []
641updateN :: [(Name, Name)] -> Name -> Name
642updateN ns n | Just n' <- lookup n ns = n'
643updateN _ n = n
645updateNs :: [(Name, Name)] -> PTerm -> PTerm
646updateNs [] t = t
647updateNs ns t = mapPT updateRef t
648 where updateRef (PRef fc f) = PRef fc (updateN ns f)
649 updateRef t = t
651-- updateDNs :: [(Name, Name)] -> PDecl -> PDecl
652-- updateDNs [] t = t
653-- updateDNs ns (PTy s f n t) | Just n' <- lookup n ns = PTy s f n' t
654-- updateDNs ns (PClauses f n c) | Just n' <- lookup n ns = PClauses f n' (map updateCNs c)
655-- where updateCNs ns (PClause n l ts r ds)
656-- = PClause (updateN ns n) (fmap (updateNs ns) l)
657-- (map (fmap (updateNs ns)) ts)
658-- (fmap (updateNs ns) r)
659-- (map (updateDNs ns) ds)
660-- updateDNs ns c = c
662data PunInfo = IsType | IsTerm | TypeOrTerm deriving (Eq, Show)
664-- | High level language terms
665data PTerm = PQuote Raw
666 | PRef FC Name
667 | PInferRef FC Name -- ^ A name to be defined later
668 | PPatvar FC Name
669 | PLam Name PTerm PTerm
670 | PPi Plicity Name PTerm PTerm -- ^ (n : t1) -> t2
671 | PLet Name PTerm PTerm PTerm
672 | PTyped PTerm PTerm -- ^ Term with explicit type
673 | PApp FC PTerm [PArg] -- ^ e.g. IO (), List Char, length x
674 | PAppBind FC PTerm [PArg] -- ^ implicitly bound application
675 | PMatchApp FC Name -- ^ Make an application by type matching
676 | PCase FC PTerm [(PTerm, PTerm)]
677 | PTrue FC PunInfo -- ^ Unit type..?
678 | PFalse FC -- ^ _|_
679 | PRefl FC PTerm
680 | PResolveTC FC
681 | PEq FC PTerm PTerm -- ^ Equality type: A = B
682 | PRewrite FC PTerm PTerm (Maybe PTerm)
683 | PPair FC PunInfo PTerm PTerm
684 | PDPair FC PunInfo PTerm PTerm PTerm
685 | PAlternative Bool [PTerm] -- True if only one may work
686 | PHidden PTerm -- ^ Irrelevant or hidden pattern
687 | PType -- ^ 'Type' type
688 | PGoal FC PTerm Name PTerm
689 | PConstant Const -- ^ Builtin types
690 | Placeholder
691 | PDoBlock [PDo]
692 | PIdiom FC PTerm
693 | PReturn FC
694 | PMetavar Name
695 | PProof [PTactic] -- ^ Proof script
696 | PTactics [PTactic] -- ^ As PProof, but no auto solving
697 | PElabError Err -- ^ Error to report on elaboration
698 | PImpossible -- ^ Special case for declaring when an LHS can't typecheck
699 | PCoerced PTerm -- ^ To mark a coerced argument, so as not to coerce twice
700 | PDisamb [[T.Text]] PTerm -- ^ Preferences for explicit namespaces
701 | PUnifyLog PTerm -- ^ dump a trace of unifications when building term
702 | PNoImplicits PTerm -- ^ never run implicit converions on the term
703 deriving Eq
706{-!
707deriving instance Binary PTerm
708deriving instance NFData PTerm
709!-}
711mapPT :: (PTerm -> PTerm) -> PTerm -> PTerm
712mapPT f t = f (mpt t) where
713 mpt (PLam n t s) = PLam n (mapPT f t) (mapPT f s)
714 mpt (PPi p n t s) = PPi p n (mapPT f t) (mapPT f s)
715 mpt (PLet n ty v s) = PLet n (mapPT f ty) (mapPT f v) (mapPT f s)
716 mpt (PRewrite fc t s g) = PRewrite fc (mapPT f t) (mapPT f s)
717 (fmap (mapPT f) g)
718 mpt (PApp fc t as) = PApp fc (mapPT f t) (map (fmap (mapPT f)) as)
719 mpt (PAppBind fc t as) = PAppBind fc (mapPT f t) (map (fmap (mapPT f)) as)
720 mpt (PCase fc c os) = PCase fc (mapPT f c) (map (pmap (mapPT f)) os)
721 mpt (PEq fc l r) = PEq fc (mapPT f l) (mapPT f r)
722 mpt (PTyped l r) = PTyped (mapPT f l) (mapPT f r)
723 mpt (PPair fc p l r) = PPair fc p (mapPT f l) (mapPT f r)
724 mpt (PDPair fc p l t r) = PDPair fc p (mapPT f l) (mapPT f t) (mapPT f r)
725 mpt (PAlternative a as) = PAlternative a (map (mapPT f) as)
726 mpt (PHidden t) = PHidden (mapPT f t)
727 mpt (PDoBlock ds) = PDoBlock (map (fmap (mapPT f)) ds)
728 mpt (PProof ts) = PProof (map (fmap (mapPT f)) ts)
729 mpt (PTactics ts) = PTactics (map (fmap (mapPT f)) ts)
730 mpt (PUnifyLog tm) = PUnifyLog (mapPT f tm)
731 mpt (PDisamb ns tm) = PDisamb ns (mapPT f tm)
732 mpt (PNoImplicits tm) = PNoImplicits (mapPT f tm)
733 mpt (PGoal fc r n sc) = PGoal fc (mapPT f r) n (mapPT f sc)
734 mpt x = x
737data PTactic' t = Intro [Name] | Intros | Focus Name
738 | Refine Name [Bool] | Rewrite t | DoUnify
739 | Induction Name
740 | Equiv t
741 | MatchRefine Name
742 | LetTac Name t | LetTacTy Name t t
743 | Exact t | Compute | Trivial | TCInstance
744 | ProofSearch Bool (Maybe Name) [Name]
745 -- ^ the bool is whether to search recursively
746 | Solve
747 | Attack
748 | ProofState | ProofTerm | Undo
749 | Try (PTactic' t) (PTactic' t)
750 | TSeq (PTactic' t) (PTactic' t)
751 | ApplyTactic t -- see Language.Reflection module
752 | ByReflection t
753 | Reflect t
754 | Fill t
755 | GoalType String (PTactic' t)
756 | TCheck t
757 | TEval t
758 | Qed | Abandon
759 deriving (Show, Eq, Functor)
760{-!
761deriving instance Binary PTactic'
762deriving instance NFData PTactic'
763!-}
764instance Sized a => Sized (PTactic' a) where
765 size (Intro nms) = 1 + size nms
766 size Intros = 1
767 size (Focus nm) = 1 + size nm
768 size (Refine nm bs) = 1 + size nm + length bs
769 size (Rewrite t) = 1 + size t
770 size (Induction t) = 1 + size t
771 size (LetTac nm t) = 1 + size nm + size t
772 size (Exact t) = 1 + size t
773 size Compute = 1
774 size Trivial = 1
775 size Solve = 1
776 size Attack = 1
777 size ProofState = 1
778 size ProofTerm = 1
779 size Undo = 1
780 size (Try l r) = 1 + size l + size r
781 size (TSeq l r) = 1 + size l + size r
782 size (ApplyTactic t) = 1 + size t
783 size (Reflect t) = 1 + size t
784 size (Fill t) = 1 + size t
785 size Qed = 1
786 size Abandon = 1
788type PTactic = PTactic' PTerm
790data PDo' t = DoExp FC t
791 | DoBind FC Name t
792 | DoBindP FC t t [(t,t)]
793 | DoLet FC Name t t
794 | DoLetP FC t t
795 deriving (Eq, Functor)
796{-!
797deriving instance Binary PDo'
798deriving instance NFData PDo'
799!-}
801instance Sized a => Sized (PDo' a) where
802 size (DoExp fc t) = 1 + size fc + size t
803 size (DoBind fc nm t) = 1 + size fc + size nm + size t
804 size (DoBindP fc l r alts) = 1 + size fc + size l + size r + size alts
805 size (DoLet fc nm l r) = 1 + size fc + size nm + size l + size r
806 size (DoLetP fc l r) = 1 + size fc + size l + size r
808type PDo = PDo' PTerm
810-- The priority gives a hint as to elaboration order. Best to elaborate
811-- things early which will help give a more concrete type to other
812-- variables, e.g. a before (interpTy a).
814data PArg' t = PImp { priority :: Int,
815 machine_inf :: Bool, -- true if the machine inferred it
816 argopts :: [ArgOpt],
817 pname :: Name, getTm :: t }
818 | PExp { priority :: Int,
819 argopts :: [ArgOpt],
820 pname :: Name,
821 getTm :: t }
822 | PConstraint { priority :: Int,
823 argopts :: [ArgOpt],
824 pname :: Name,
825 getTm :: t }
826 | PTacImplicit { priority :: Int,
827 argopts :: [ArgOpt],
828 pname :: Name,
829 getScript :: t,
830 getTm :: t }
831 deriving (Show, Eq, Functor)
833data ArgOpt = HideDisplay | InaccessibleArg
834 deriving (Show, Eq)
836instance Sized a => Sized (PArg' a) where
837 size (PImp p _ l nm trm) = 1 + size nm + size trm
838 size (PExp p l nm trm) = 1 + size nm + size trm
839 size (PConstraint p l nm trm) = 1 + size nm +size nm + size trm
840 size (PTacImplicit p l nm scr trm) = 1 + size nm + size scr + size trm
842{-!
843deriving instance Binary PArg'
844deriving instance NFData PArg'
845!-}
847pimp n t mach = PImp 1 mach [] n t
848pexp t = PExp 1 [] (sMN 0 "arg") t
849pconst t = PConstraint 1 [] (sMN 0 "carg") t
850ptacimp n s t = PTacImplicit 2 [] n s t
852type PArg = PArg' PTerm
854-- Type class data
856data ClassInfo = CI { instanceName :: Name,
857 class_methods :: [(Name, (FnOpts, PTerm))],
858 class_defaults :: [(Name, (Name, PDecl))], -- method name -> default impl
859 class_default_superclasses :: [PDecl],
860 class_params :: [Name],
861 class_instances :: [Name] }
862 deriving Show
863{-!
864deriving instance Binary ClassInfo
865deriving instance NFData ClassInfo
866!-}
868-- Type inference data
870data TIData = TIPartial -- ^ a function with a partially defined type
871 | TISolution [Term] -- ^ possible solutions to a metavariable in a type
872 deriving Show
874data OptInfo = Optimise { inaccessible :: [(Int,Name)], -- includes names for error reporting
875 detaggable :: Bool }
876 deriving Show
877{-!
878deriving instance Binary OptInfo
879deriving instance NFData OptInfo
880!-}
883data TypeInfo = TI { con_names :: [Name],
884 codata :: Bool,
885 data_opts :: DataOpts,
886 param_pos :: [Int] }
887 deriving Show
888{-!
889deriving instance Binary TypeInfo
890deriving instance NFData TypeInfo
891!-}
893-- Syntactic sugar info
895data DSL' t = DSL { dsl_bind :: t,
896 dsl_return :: t,
897 dsl_apply :: t,
898 dsl_pure :: t,
899 dsl_var :: Maybe t,
900 index_first :: Maybe t,
901 index_next :: Maybe t,
902 dsl_lambda :: Maybe t,
903 dsl_let :: Maybe t
904 }
905 deriving (Show, Functor)
906{-!
907deriving instance Binary DSL'
908deriving instance NFData DSL'
909!-}
911type DSL = DSL' PTerm
913data SynContext = PatternSyntax | TermSyntax | AnySyntax
914 deriving Show
915{-!
916deriving instance Binary SynContext
917deriving instance NFData SynContext
918!-}
920data Syntax = Rule [SSymbol] PTerm SynContext
921 deriving Show
922{-!
923deriving instance Binary Syntax
924deriving instance NFData Syntax
925!-}
927data SSymbol = Keyword Name
928 | Symbol String
929 | Binding Name
930 | Expr Name
931 | SimpleExpr Name
932 deriving Show
933{-!
934deriving instance Binary SSymbol
935deriving instance NFData SSymbol
936!-}
938initDSL = DSL (PRef f (sUN ">>="))
939 (PRef f (sUN "return"))
940 (PRef f (sUN "<$>"))
941 (PRef f (sUN "pure"))
942 Nothing
943 Nothing
944 Nothing
945 Nothing
946 Nothing
947 where f = fileFC "(builtin)"
949data Using = UImplicit Name PTerm
950 | UConstraint Name [Name]
951 deriving (Show, Eq)
952{-!
953deriving instance Binary Using
954deriving instance NFData Using
955!-}
957data SyntaxInfo = Syn { using :: [Using],
958 syn_params :: [(Name, PTerm)],
959 syn_namespace :: [String],
960 no_imp :: [Name],
961 decoration :: Name -> Name,
962 inPattern :: Bool,
963 implicitAllowed :: Bool,
964 dsl_info :: DSL }
965 deriving Show
966{-!
967deriving instance NFData SyntaxInfo
968deriving instance Binary SyntaxInfo
969!-}
971defaultSyntax = Syn [] [] [] [] id False False initDSL
973expandNS :: SyntaxInfo -> Name -> Name
974expandNS syn n@(NS _ _) = n
975expandNS syn n = case syn_namespace syn of
976 [] -> n
977 xs -> sNS n xs
980-- For inferring types of things
982bi = fileFC "builtin"
984inferTy = sMN 0 "__Infer"
985inferCon = sMN 0 "__infer"
986inferDecl = PDatadecl inferTy
987 PType
988 [(emptyDocstring, [], inferCon, PPi impl (sMN 0 "iType") PType (
989 PPi expl (sMN 0 "ival") (PRef bi (sMN 0 "iType"))
990 (PRef bi inferTy)), bi, [])]
991inferOpts = []
993infTerm t = PApp bi (PRef bi inferCon) [pimp (sMN 0 "iType") Placeholder True, pexp t]
994infP = P (TCon 6 0) inferTy (TType (UVal 0))
996getInferTerm, getInferType :: Term -> Term
997getInferTerm (Bind n b sc) = Bind n b $ getInferTerm sc
998getInferTerm (App (App _ _) tm) = tm
999getInferTerm tm = tm -- error ("getInferTerm " ++ show tm)
1001getInferType (Bind n b sc) = Bind n (toTy b) $ getInferType sc
1002 where toTy (Lam t) = Pi t
1003 toTy (PVar t) = PVTy t
1004 toTy b = b
1005getInferType (App (App _ ty) _) = ty
1009-- Handy primitives: Unit, False, Pair, MkPair, =, mkForeign, Elim type class
1011primNames = [unitTy, unitCon,
1012 falseTy, pairTy, pairCon,
1013 eqTy, eqCon, inferTy, inferCon]
1015unitDoc = parseDocstring . T.pack $ "The canonical single-element type, also known as the trivially true proposition."
1016unitTy = sMN 0 "__Unit"
1017unitCon = sMN 0 "__II"
1018unitDecl = PDatadecl unitTy PType
1019 [(parseDocstring . T.pack $ "The trivial constructor for `()`. ", [], unitCon, PRef bi unitTy, bi, [])]
1020unitOpts = [DefaultEliminator]
1022falseDoc = parseDocstring . T.pack $
1023 "The empty type, also known as the trivially false proposition." ++
1024 "\n\n" ++
1025 "Use `FalseElim` or `absurd` to prove anything if you have a variable " ++
1026 "of type `_|_` in scope."
1027falseTy = sMN 0 "__False"
1028falseDecl = PDatadecl falseTy PType []
1029falseOpts = []
1031pairDoc = parseDocstring . T.pack $ "The non-dependent pair type, also known as conjunction."
1032pairTy = sMN 0 "__Pair"
1033pairCon = sMN 0 "__MkPair"
1034pairDecl = PDatadecl pairTy (piBind [(n "A", PType), (n "B", PType)] PType)
1035 [(pairConDoc, pairConParamDoc,
1036 pairCon, PPi impl (n "A") PType (
1037 PPi impl (n "B") PType (
1038 PPi expl (n "a") (PRef bi (n "A")) (
1039 PPi expl (n "b") (PRef bi (n "B"))
1040 (PApp bi (PRef bi pairTy) [pexp (PRef bi (n "A")),
1041 pexp (PRef bi (n "B"))])))), bi, [])]
1042 where n a = sMN 0 a
1043 pairConDoc = parseDocstring . T.pack $ "A pair of elements"
1044 pairConParamDoc = [(n "a", parseDocstring . T.pack $ "the left element of the pair"),
1045 (n "b", parseDocstring . T.pack $ "the right element of the pair")]
1046pairOpts = []
1047pairParamDoc = [(n "A", parseDocstring . T.pack $ "the type of the left elements in the pair"),
1048 (n "B", parseDocstring . T.pack $ "the type of the left elements in the pair")]
1049 where n a = sMN 0 a
1051eqTy = sUN "="
1052eqCon = sUN "refl"
1053eqDoc = parseDocstring . T.pack $
1054 "The propositional equality type. A proof that `x` = `y`." ++
1055 "\n\n" ++
1056 "To use such a proof, pattern-match on it, and the two equal things will " ++
1057 "then need to be the _same_ pattern." ++
1058 "\n\n" ++
1059 "**Note**: Idris's equality type is _heterogeneous_, which means that it " ++
1060 "is possible to state equalities between values of potentially different " ++
1061 "types. This is sometimes referred to in the literature as \"John Major\" " ++
1062 "equality." ++
1063 "\n\n" ++
1064 "Thus, if Idris can't infer the type of one side of the equality, then " ++
1065 "you may need to annotate it. See the function `the`."
1067eqDecl = PDatadecl eqTy (piBind [(n "A", PType), (n "B", PType),
1068 (n "x", PRef bi (n "A")), (n "y", PRef bi (n "B"))]
1069 PType)
1070 [(reflDoc, reflParamDoc,
1071 eqCon, PPi impl (n "A") PType (
1072 PPi impl (n "x") (PRef bi (n "A"))
1073 (PApp bi (PRef bi eqTy) [pimp (n "A") Placeholder False,
1074 pimp (n "B") Placeholder False,
1075 pexp (PRef bi (n "x")),
1076 pexp (PRef bi (n "x"))])), bi, [])]
1077 where n a = sMN 0 a
1078 reflDoc = parseDocstring . T.pack $
1079 "A proof that `x` in fact equals `x`. To construct this, you must have already " ++
1080 "shown that both sides are in fact equal."
1081 reflParamDoc = [(n "A", parseDocstring . T.pack $ "the type at which the equality is proven"),
1082 (n "x", parseDocstring . T.pack $ "the element shown to be equal to itself.")]
1084eqParamDoc = [(n "A", parseDocstring . T.pack $ "the type of the left side of the equality"),
1085 (n "B", parseDocstring . T.pack $ "the type of the right side of the equality")
1087 where n a = sMN 0 a
1089eqOpts = []
1091elimName = sUN "__Elim"
1092elimMethElimTy = sUN "__elimTy"
1093elimMethElim = sUN "elim"
1094elimDecl = PClass (parseDocstring . T.pack $ "Type class for eliminators") defaultSyntax bi [] elimName [(sUN "scrutineeType", PType)] []
1095 [PTy emptyDocstring [] defaultSyntax bi [TotalFn] elimMethElimTy PType,
1096 PTy emptyDocstring [] defaultSyntax bi [TotalFn] elimMethElim (PRef bi elimMethElimTy)]
1098-- Defined in builtins.idr
1099sigmaTy = sUN "Exists"
1100existsCon = sUN "Ex_intro"
1102piBind :: [(Name, PTerm)] -> PTerm -> PTerm
1103piBind = piBindp expl
1105piBindp :: Plicity -> [(Name, PTerm)] -> PTerm -> PTerm
1106piBindp p [] t = t
1107piBindp p ((n, ty):ns) t = PPi p n ty (piBindp p ns t)
1110-- Pretty-printing declarations and terms
1112-- These "show" instances render to an absurdly wide screen because inserted line breaks
1113-- could interfere with interactive editing, which calls "show".
1115instance Show PTerm where
1116 showsPrec _ tm = (displayS . renderPretty 1.0 10000000 . prettyImp defaultPPOption) tm
1118instance Show PDecl where
1119 showsPrec _ d = (displayS . renderPretty 1.0 10000000 . showDeclImp defaultPPOption) d
1121instance Show PClause where
1122 showsPrec _ c = (displayS . renderPretty 1.0 10000000 . showCImp verbosePPOption) c
1124instance Show PData where
1125 showsPrec _ d = (displayS . renderPretty 1.0 10000000 . showDImp defaultPPOption) d
1127instance Pretty PTerm OutputAnnotation where
1128 pretty = prettyImp defaultPPOption
1130-- | Colourise annotations according to an Idris state. It ignores the names
1131-- in the annotation, as there's no good way to show extended information on a
1132-- terminal.
1133consoleDecorate :: IState -> OutputAnnotation -> String -> String
1134consoleDecorate ist _ | not (idris_colourRepl ist) = id
1135consoleDecorate ist (AnnConst c) = let theme = idris_colourTheme ist
1136 in if constIsType c
1137 then colouriseType theme
1138 else colouriseData theme
1139consoleDecorate ist (AnnData _ _) = colouriseData (idris_colourTheme ist)
1140consoleDecorate ist (AnnType _ _) = colouriseType (idris_colourTheme ist)
1141consoleDecorate ist (AnnBoundName _ True) = colouriseImplicit (idris_colourTheme ist)
1142consoleDecorate ist (AnnBoundName _ False) = colouriseBound (idris_colourTheme ist)
1143consoleDecorate ist AnnKeyword = colouriseKeyword (idris_colourTheme ist)
1144consoleDecorate ist (AnnName n _ _ _) = let ctxt = tt_ctxt ist
1145 theme = idris_colourTheme ist
1146 in case () of
1147 _ | isDConName n ctxt -> colouriseData theme
1148 _ | isFnName n ctxt -> colouriseFun theme
1149 _ | isTConName n ctxt -> colouriseType theme
1150 _ | otherwise -> id -- don't colourise unknown names
1151consoleDecorate ist (AnnFC _) = id
1152consoleDecorate ist (AnnTextFmt fmt) = Idris.Colours.colourise (colour fmt)
1153 where colour BoldText = IdrisColour Nothing True False True False
1154 colour UnderlineText = IdrisColour Nothing True True False False
1155 colour ItalicText = IdrisColour Nothing True False False True
1157-- | Pretty-print a high-level closed Idris term with no information about precedence/associativity
1158prettyImp :: PPOption -- ^^ pretty printing options
1159 -> PTerm -- ^^ the term to pretty-print
1160 -> Doc OutputAnnotation
1161prettyImp impl = pprintPTerm impl [] [] []
1163-- | Do the right thing for rendering a term in an IState
1164prettyIst :: IState -> PTerm -> Doc OutputAnnotation
1165prettyIst ist = pprintPTerm (ppOptionIst ist) [] [] (idris_infixes ist)
1167-- | Pretty-print a high-level Idris term in some bindings context with infix info
1168pprintPTerm :: PPOption -- ^^ pretty printing options
1169 -> [(Name, Bool)] -- ^^ the currently-bound names and whether they are implicit
1170 -> [Name] -- ^^ names to always show in pi, even if not used
1171 -> [FixDecl] -- ^^ Fixity declarations
1172 -> PTerm -- ^^ the term to pretty-print
1173 -> Doc OutputAnnotation
1174pprintPTerm ppo bnd docArgs infixes = prettySe 10 bnd
1175 where
1176 prettySe :: Int -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation
1177 prettySe p bnd (PQuote r) =
1178 text "![" <> pretty r <> text "]"
1179 prettySe p bnd (PPatvar fc n) = pretty n
1180 prettySe p bnd e
1181 | Just str <- slist p bnd e = str
1182 | Just n <- snat p e = annotate (AnnData "Nat" "") (text (show n))
1183 prettySe p bnd (PRef fc n) = prettyName (ppopt_impl ppo) bnd n
1184 prettySe p bnd (PLam n ty sc) =
1185 bracket p 2 . group . align . hang 2 $
1186 text "\\" <> bindingOf n False <+> text "=>" <$>
1187 prettySe 10 ((n, False):bnd) sc
1188 prettySe p bnd (PLet n ty v sc) =
1189 bracket p 2 $
1190 kwd "let" <+> bindingOf n False <+> text "=" </>
1191 prettySe 10 bnd v <+> kwd "in" </>
1192 prettySe 10 ((n, False):bnd) sc
1193 prettySe p bnd (PPi (Exp l s _) n ty sc)
1194 | n `elem` allNamesIn sc || ppopt_impl ppo || n `elem` docArgs =
1195 bracket p 2 . group $
1196 enclose lparen rparen (group . align $ bindingOf n False <+> colon <+> prettySe 10 bnd ty) <+>
1197 st <> text "->" <$> prettySe 10 ((n, False):bnd) sc
1198 | otherwise =
1199 bracket p 2 . group $
1200 group (prettySe 1 bnd ty <+> st) <> text "->" <$> group (prettySe 10 ((n, False):bnd) sc)
1201 where
1202 st =
1203 case s of
1204 Static -> text "[static]" <> space
1205 _ -> empty
1206 prettySe p bnd (PPi (Imp l s _) n ty sc)
1207 | ppopt_impl ppo =
1208 bracket p 2 $
1209 lbrace <> bindingOf n True <+> colon <+> prettySe 10 bnd ty <> rbrace <+>
1210 st <> text "->" </> prettySe 10 ((n, True):bnd) sc
1211 | otherwise = prettySe 10 ((n, True):bnd) sc
1212 where
1213 st =
1214 case s of
1215 Static -> text "[static]" <> space
1216 _ -> empty
1217 prettySe p bnd (PPi (Constraint _ _) n ty sc) =
1218 bracket p 2 $
1219 prettySe 10 bnd ty <+> text "=>" </> prettySe 10 ((n, True):bnd) sc
1220 prettySe p bnd (PPi (TacImp _ _ s) n ty sc) =
1221 bracket p 2 $
1222 lbrace <> kwd "tacimp" <+> pretty n <+> colon <+> prettySe 10 bnd ty <>
1223 rbrace <+> text "->" </> prettySe 10 ((n, True):bnd) sc
1224 prettySe p bnd (PApp _ (PRef _ f) args) -- normal names, no explicit args
1225 | UN nm <- basename f
1226 , not (ppopt_impl ppo) && null (getExps args) =
1227 if isAlpha (thead nm)
1228 then prettyName (ppopt_impl ppo) bnd f
1229 else enclose lparen rparen $ prettyName (ppopt_impl ppo) bnd f
1230 prettySe p bnd (PAppBind _ (PRef _ f) [])
1231 | not (ppopt_impl ppo) = text "!" <> prettyName (ppopt_impl ppo) bnd f
1232 prettySe p bnd (PApp _ (PRef _ op) args) -- infix operators
1233 | UN nm <- basename op
1234 , not (tnull nm) &&
1235 (not (ppopt_impl ppo)) && (not $ isAlpha (thead nm)) =
1236 case getExps args of
1237 [] -> enclose lparen rparen opName
1238 [x] -> group (enclose lparen rparen opName <$> group (prettySe 0 bnd x))
1239 [l,r] -> let precedence = fromMaybe 20 (fmap prec f)
1240 in bracket p precedence $ inFix l r
1241 (l:r:rest) -> bracket p 1 $
1242 enclose lparen rparen (inFix l r) <+>
1243 align (group (vsep (map (prettyArgSe bnd) rest)))
1244 where opName = prettyName (ppopt_impl ppo) bnd op
1245 f = getFixity (opStr op)
1246 left l = case f of
1247 Nothing -> prettySe (-1) bnd l
1248 Just (Infixl p') -> prettySe p' bnd l
1249 Just f' -> prettySe (prec f'-1) bnd l
1250 right r = case f of
1251 Nothing -> prettySe (-1) bnd r
1252 Just (Infixr p') -> prettySe p' bnd r
1253 Just f' -> prettySe (prec f'-1) bnd r
1254 inFix l r = align . group $
1255 (left l <+> opName) <$> group (right r)
1256 prettySe p bnd (PApp _ hd@(PRef fc f) [tm]) -- symbols, like 'foo
1257 | PConstant (Idris.Core.TT.Str str) <- getTm tm,
1258 f == sUN "Symbol_" = annotate (AnnType ("'" ++ str) ("The symbol " ++ str)) $
1259 char '\'' <> prettySe 10 bnd (PRef fc (sUN str))
1260 prettySe p bnd (PApp _ f as) = -- Normal prefix applications
1261 let args = getExps as
1262 fp = prettySe 1 bnd f
1263 in
1264 bracket p 1 . group $
1265 if ppopt_impl ppo
1266 then if null as
1267 then fp
1268 else fp <+> align (vsep (map (prettyArgS bnd) as))
1269 else if null args
1270 then fp
1271 else fp <+> align (vsep (map (prettyArgSe bnd) args))
1272 prettySe p bnd (PCase _ scr opts) =
1273 kwd "case" <+> prettySe 10 bnd scr <+> kwd "of" <> prettyBody
1274 where
1275 prettyBody = foldr (<>) empty $ intersperse (text "|") $ map sc opts
1277 sc (l, r) = nest nestingSize $ prettySe 10 bnd l <+> text "=>" <+> prettySe 10 bnd r
1278 prettySe p bnd (PHidden tm) = text "." <> prettySe 0 bnd tm
1279 prettySe p bnd (PRefl _ _) = annName eqCon $ text "refl"
1280 prettySe p bnd (PResolveTC _) = text "resolvetc"
1281 prettySe p bnd (PTrue _ IsType) = annName unitTy $ text "()"
1282 prettySe p bnd (PTrue _ IsTerm) = annName unitCon $ text "()"
1283 prettySe p bnd (PTrue _ TypeOrTerm) = text "()"
1284 prettySe p bnd (PFalse _) = annName falseTy $ text "_|_"
1285 prettySe p bnd (PEq _ l r) =
1286 bracket p 2 . align . group $
1287 prettySe 10 bnd l <+> eq <$> group (prettySe 10 bnd r)
1288 where eq = annName eqTy (text "=")
1289 prettySe p bnd (PRewrite _ l r _) =
1290 bracket p 2 $
1291 text "rewrite" <+> prettySe 10 bnd l <+> text "in" <+> prettySe 10 bnd r
1292 prettySe p bnd (PTyped l r) =
1293 lparen <> prettySe 10 bnd l <+> colon <+> prettySe 10 bnd r <> rparen
1294 prettySe p bnd pair@(PPair _ pun _ _) -- flatten tuples to the right, like parser
1295 | Just elts <- pairElts pair = enclose (ann lparen) (ann rparen) .
1296 align . group . vsep . punctuate (ann comma) $
1297 map (prettySe 10 bnd) elts
1298 where ann = case pun of
1299 TypeOrTerm -> id
1300 IsType -> annName pairTy
1301 IsTerm -> annName pairCon
1302 prettySe p bnd (PDPair _ TypeOrTerm l t r) =
1303 lparen <> prettySe 10 bnd l <+> text "**" <+> prettySe 10 bnd r <> rparen
1304 prettySe p bnd (PDPair _ IsType (PRef _ n) t r) =
1305 annName sigmaTy lparen <>
1306 bindingOf n False <+>
1307 annName sigmaTy (text "**") <+>
1308 prettySe 10 ((n, False):bnd) r <>
1309 annName sigmaTy rparen
1310 prettySe p bnd (PDPair _ IsType l t r) =
1311 annName sigmaTy lparen <>
1312 prettySe 10 bnd l <+>
1313 annName sigmaTy (text "**") <+>
1314 prettySe 10 bnd r <>
1315 annName sigmaTy rparen
1316 prettySe p bnd (PDPair _ IsTerm l t r) =
1317 annName existsCon lparen <>
1318 prettySe 10 bnd l <+>
1319 annName existsCon (text "**") <+>
1320 prettySe 10 bnd r <>
1321 annName existsCon rparen
1322 prettySe p bnd (PAlternative a as) =
1323 lparen <> text "|" <> prettyAs <> text "|" <> rparen
1324 where
1325 prettyAs =
1326 foldr (\l -> \r -> l <+> text "," <+> r) empty $ map (prettySe 10 bnd) as
1327 prettySe p bnd PType = annotate (AnnType "Type" "The type of types") $ text "Type"
1328 prettySe p bnd (PConstant c) = annotate (AnnConst c) (text (show c))
1329 -- XXX: add pretty for tactics
1330 prettySe p bnd (PProof ts) =
1331 text "proof" <+> lbrace <> nest nestingSize (text . show $ ts) <> rbrace
1332 prettySe p bnd (PTactics ts) =
1333 text "tactics" <+> lbrace <> nest nestingSize (text . show $ ts) <> rbrace
1334 prettySe p bnd (PMetavar n) = text "?" <> pretty n
1335 prettySe p bnd (PReturn f) = kwd "return"
1336 prettySe p bnd PImpossible = kwd "impossible"
1337 prettySe p bnd Placeholder = text "_"
1338 prettySe p bnd (PDoBlock _) = text "do block pretty not implemented"
1339 prettySe p bnd (PElabError s) = pretty s
1341 prettySe p bnd _ = text "test"
1343 prettyArgS bnd (PImp _ _ _ n tm) = prettyArgSi bnd (n, tm)
1344 prettyArgS bnd (PExp _ _ _ tm) = prettyArgSe bnd tm
1345 prettyArgS bnd (PConstraint _ _ _ tm) = prettyArgSc bnd tm
1346 prettyArgS bnd (PTacImplicit _ _ n _ tm) = prettyArgSti bnd (n, tm)
1348 prettyArgSe bnd arg = prettySe 0 bnd arg
1349 prettyArgSi bnd (n, val) = lbrace <> pretty n <+> text "=" <+> prettySe 10 bnd val <> rbrace
1350 prettyArgSc bnd val = lbrace <> lbrace <> prettySe 10 bnd val <> rbrace <> rbrace
1351 prettyArgSti bnd (n, val) = lbrace <> kwd "auto" <+> pretty n <+> text "=" <+> prettySe 10 bnd val <> rbrace
1353 annName :: Name -> Doc OutputAnnotation -> Doc OutputAnnotation
1354 annName n = annotate (AnnName n Nothing Nothing Nothing)
1356 opStr :: Name -> String
1357 opStr (NS n _) = opStr n
1358 opStr (UN n) = T.unpack n
1360 basename :: Name -> Name
1361 basename (NS n _) = basename n
1362 basename n = n
1364 slist' p bnd (PApp _ (PRef _ nil) _)
1365 | not (ppopt_impl ppo) && nsroot nil == sUN "Nil" = Just []
1366 slist' p bnd (PRef _ nil)
1367 | not (ppopt_impl ppo) && nsroot nil == sUN "Nil" = Just []
1368 slist' p bnd (PApp _ (PRef _ cons) args)
1369 | nsroot cons == sUN "::",
1370 (PExp {getTm=tl}):(PExp {getTm=hd}):imps <- reverse args,
1371 all isImp imps,
1372 Just tl' <- slist' p bnd tl
1373 = Just (hd:tl')
1374 where
1375 isImp (PImp {}) = True
1376 isImp _ = False
1377 slist' _ _ tm = Nothing
1379 slist p bnd e | Just es <- slist' p bnd e = Just $
1380 case es of [] -> annotate (AnnData "" "") $ text "[]"
1381 [x] -> enclose left right . group $
1382 prettySe p bnd x
1383 xs -> (enclose left right .
1384 align . group . vsep .
1385 punctuate comma .
1386 map (prettySe p bnd)) xs
1387 where left = (annotate (AnnData "" "") (text "["))
1388 right = (annotate (AnnData "" "") (text "]"))
1389 comma = (annotate (AnnData "" "") (text ","))
1390 slist _ _ _ = Nothing
1392 pairElts :: PTerm -> Maybe [PTerm]
1393 pairElts (PPair _ _ x y) | Just elts <- pairElts y = Just (x:elts)
1394 | otherwise = Just [x, y]
1395 pairElts _ = Nothing
1397 natns = "Prelude.Nat."
1399 snat p (PRef _ z)
1400 | show z == (natns++"Z") || show z == "Z" = Just 0
1401 snat p (PApp _ s [PExp {getTm=n}])
1402 | show s == (natns++"S") || show s == "S",
1403 Just n' <- snat p n
1404 = Just $ 1 + n'
1405 snat _ _ = Nothing
1407 bracket outer inner doc
1408 | inner > outer = lparen <> doc <> rparen
1409 | otherwise = doc
1411 kwd = annotate AnnKeyword . text
1413 fixities :: M.Map String Fixity
1414 fixities = M.fromList [(s, f) | (Fix f s) <- infixes]
1416 getFixity :: String -> Maybe Fixity
1417 getFixity = flip M.lookup fixities
1419-- | Pretty-printer helper for the binding site of a name
1420bindingOf :: Name -- ^^ the bound name
1421 -> Bool -- ^^ whether the name is implicit
1422 -> Doc OutputAnnotation
1423bindingOf n imp = annotate (AnnBoundName n imp) (text (show n))
1425-- | Pretty-printer helper for names that attaches the correct annotations
1426prettyName :: Bool -- ^^ whether to show namespaces
1427 -> [(Name, Bool)] -- ^^ the current bound variables and whether they are implicit
1428 -> Name -- ^^ the name to pprint
1429 -> Doc OutputAnnotation
1430prettyName showNS bnd n | Just imp <- lookup n bnd = annotate (AnnBoundName n imp) (text (strName n))
1431 | otherwise = annotate (AnnName n Nothing Nothing Nothing) (text (strName n))
1432 where strName (UN n) = T.unpack n
1433 strName (NS n ns) | showNS = (concatMap (++ ".") . map T.unpack . reverse) ns ++ strName n
1434 | otherwise = strName n
1435 strName n | n == falseTy = "_|_"
1436 strName (MN i s) = T.unpack s
1437 strName other = show other
1440showCImp :: PPOption -> PClause -> Doc OutputAnnotation
1441showCImp ppo (PClause _ n l ws r w)
1442 = prettyImp ppo l <+> showWs ws <+> text "=" <+> prettyImp ppo r
1443 <+> text "where" <+> text (show w)
1444 where
1445 showWs [] = empty
1446 showWs (x : xs) = text "|" <+> prettyImp ppo x <+> showWs xs
1447showCImp ppo (PWith _ n l ws r w)
1448 = prettyImp ppo l <+> showWs ws <+> text "with" <+> prettyImp ppo r
1449 <+> braces (text (show w))
1450 where
1451 showWs [] = empty
1452 showWs (x : xs) = text "|" <+> prettyImp ppo x <+> showWs xs
1455showDImp :: PPOption -> PData -> Doc OutputAnnotation
1456showDImp ppo (PDatadecl n ty cons)
1457 = text "data" <+> text (show n) <+> colon <+> prettyImp ppo ty <+> text "where" <$>
1458 (indent 2 $ vsep (map (\ (_, _, n, t, _, _) -> pipe <+> prettyName False [] n <+> colon <+> prettyImp ppo t) cons))
1460showDecls :: PPOption -> [PDecl] -> Doc OutputAnnotation
1461showDecls o ds = vsep (map (showDeclImp o) ds)
1463showDeclImp _ (PFix _ f ops) = text (show f) <+> cat (punctuate (text ",") (map text ops))
1464showDeclImp o (PTy _ _ _ _ _ n t) = text "tydecl" <+> text (showCG n) <+> colon <+> prettyImp o t
1465showDeclImp o (PClauses _ _ n cs) = text "pat" <+> text (showCG n) <+> text "\t" <+>
1466 indent 2 (vsep (map (showCImp o) cs))
1467showDeclImp o (PData _ _ _ _ _ d) = showDImp o { ppopt_impl = True } d
1468showDeclImp o (PParams _ ns ps) = text "params" <+> braces (text (show ns) <> line <> showDecls o ps <> line)
1469showDeclImp o (PNamespace n ps) = text "namespace" <+> text n <> braces (line <> showDecls o ps <> line)
1470showDeclImp _ (PSyntax _ syn) = text "syntax" <+> text (show syn)
1471showDeclImp o (PClass _ _ _ cs n ps _ ds)
1472 = text "class" <+> text (show cs) <+> text (show n) <+> text (show ps) <> line <> showDecls o ds
1473showDeclImp o (PInstance _ _ cs n _ t _ ds)
1474 = text "instance" <+> text (show cs) <+> text (show n) <+> prettyImp o t <> line <> showDecls o ds
1475showDeclImp _ _ = text "..."
1476-- showDeclImp (PImport o) = "import " ++ o
1478instance Show (Doc OutputAnnotation) where
1479 show = flip (displayS . renderCompact) ""
1481getImps :: [PArg] -> [(Name, PTerm)]
1482getImps [] = []
1483getImps (PImp _ _ _ n tm : xs) = (n, tm) : getImps xs
1484getImps (_ : xs) = getImps xs
1486getExps :: [PArg] -> [PTerm]
1487getExps [] = []
1488getExps (PExp _ _ _ tm : xs) = tm : getExps xs
1489getExps (_ : xs) = getExps xs
1491getConsts :: [PArg] -> [PTerm]
1492getConsts [] = []
1493getConsts (PConstraint _ _ _ tm : xs) = tm : getConsts xs
1494getConsts (_ : xs) = getConsts xs
1496getAll :: [PArg] -> [PTerm]
1497getAll = map getTm
1500-- | Show Idris name
1501showName :: Maybe IState -- ^^ the Idris state, for information about names and colours
1502 -> [(Name, Bool)] -- ^^ the bound variables and whether they're implicit
1503 -> PPOption -- ^^ pretty printing options
1504 -> Bool -- ^^ whether to colourise
1505 -> Name -- ^^ the term to show
1506 -> String
1507showName ist bnd ppo colour n = case ist of
1508 Just i -> if colour then colourise n (idris_colourTheme i) else showbasic n
1509 Nothing -> showbasic n
1510 where name = if ppopt_impl ppo then show n else showbasic n
1511 showbasic n@(UN _) = showCG n
1512 showbasic (MN _ s) = str s
1513 showbasic (NS n s) = showSep "." (map str (reverse s)) ++ "." ++ showbasic n
1514 showbasic (SN s) = show s
1515 fst3 (x, _, _) = x
1516 colourise n t = let ctxt' = fmap tt_ctxt ist in
1517 case ctxt' of
1518 Nothing -> name
1519 Just ctxt | Just impl <- lookup n bnd -> if impl then colouriseImplicit t name
1520 else colouriseBound t name
1521 | isDConName n ctxt -> colouriseData t name
1522 | isFnName n ctxt -> colouriseFun t name
1523 | isTConName n ctxt -> colouriseType t name
1524 -- The assumption is that if a name is not bound and does not exist in the
1525 -- global context, then we're somewhere in which implicit info has been lost
1526 -- (like error messages). Thus, unknown vars are colourised as implicits.
1527 | otherwise -> colouriseImplicit t name
1529showTm :: IState -- ^^ the Idris state, for information about identifiers and colours
1530 -> PTerm -- ^^ the term to show
1531 -> String
1532showTm ist = displayDecorated (consoleDecorate ist) .
1533 renderPretty 0.8 100000 .
1534 prettyImp (ppOptionIst ist)
1536-- | Show a term with implicits, no colours
1537showTmImpls :: PTerm -> String
1538showTmImpls = flip (displayS . renderCompact . prettyImp verbosePPOption) ""
1542instance Sized PTerm where
1543 size (PQuote rawTerm) = size rawTerm
1544 size (PRef fc name) = size name
1545 size (PLam name ty bdy) = 1 + size ty + size bdy
1546 size (PPi plicity name ty bdy) = 1 + size ty + size bdy
1547 size (PLet name ty def bdy) = 1 + size ty + size def + size bdy
1548 size (PTyped trm ty) = 1 + size trm + size ty
1549 size (PApp fc name args) = 1 + size args
1550 size (PAppBind fc name args) = 1 + size args
1551 size (PCase fc trm bdy) = 1 + size trm + size bdy
1552 size (PTrue fc _) = 1
1553 size (PFalse fc) = 1
1554 size (PRefl fc _) = 1
1555 size (PResolveTC fc) = 1
1556 size (PEq fc left right) = 1 + size left + size right
1557 size (PRewrite fc left right _) = 1 + size left + size right
1558 size (PPair fc _ left right) = 1 + size left + size right
1559 size (PDPair fs _ left ty right) = 1 + size left + size ty + size right
1560 size (PAlternative a alts) = 1 + size alts
1561 size (PHidden hidden) = size hidden
1562 size (PUnifyLog tm) = size tm
1563 size (PDisamb _ tm) = size tm
1564 size (PNoImplicits tm) = size tm
1565 size PType = 1
1566 size (PConstant const) = 1 + size const
1567 size Placeholder = 1
1568 size (PDoBlock dos) = 1 + size dos
1569 size (PIdiom fc term) = 1 + size term
1570 size (PReturn fc) = 1
1571 size (PMetavar name) = 1
1572 size (PProof tactics) = size tactics
1573 size (PElabError err) = size err
1574 size PImpossible = 1
1576getPArity :: PTerm -> Int
1577getPArity (PPi _ _ _ sc) = 1 + getPArity sc
1578getPArity _ = 0
1580-- Return all names, free or globally bound, in the given term.
1582allNamesIn :: PTerm -> [Name]
1583allNamesIn tm = nub $ ni [] tm
1584 where -- TODO THINK added niTacImp, but is it right?
1585 ni env (PRef _ n)
1586 | not (n `elem` env) = [n]
1587 ni env (PPatvar _ n) = [n]
1588 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
1589 ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
1590 ni env (PCase _ c os) = ni env c ++ concatMap (ni env) (map snd os)
1591 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc
1592 ni env (PPi p n ty sc) = niTacImp env p ++ ni env ty ++ ni (n:env) sc
1593 ni env (PHidden tm) = ni env tm
1594 ni env (PEq _ l r) = ni env l ++ ni env r
1595 ni env (PRewrite _ l r _) = ni env l ++ ni env r
1596 ni env (PTyped l r) = ni env l ++ ni env r
1597 ni env (PPair _ _ l r) = ni env l ++ ni env r
1598 ni env (PDPair _ _ (PRef _ n) t r) = ni env t ++ ni (n:env) r
1599 ni env (PDPair _ _ l t r) = ni env l ++ ni env t ++ ni env r
1600 ni env (PAlternative a ls) = concatMap (ni env) ls
1601 ni env (PUnifyLog tm) = ni env tm
1602 ni env (PDisamb _ tm) = ni env tm
1603 ni env (PNoImplicits tm) = ni env tm
1604 ni env _ = []
1606 niTacImp env (TacImp _ _ scr) = ni env scr
1607 niTacImp _ _ = []
1609-- Return all names defined in binders in the given term
1610boundNamesIn :: PTerm -> [Name]
1611boundNamesIn tm = nub $ ni tm
1612 where -- TODO THINK Added niTacImp, but is it right?
1613 ni (PApp _ f as) = ni f ++ concatMap (ni) (map getTm as)
1614 ni (PAppBind _ f as) = ni f ++ concatMap (ni) (map getTm as)
1615 ni (PCase _ c os) = ni c ++ concatMap (ni) (map snd os)
1616 ni (PLam n ty sc) = n : (ni ty ++ ni sc)
1617 ni (PLet n ty val sc) = n : (ni ty ++ ni val ++ ni sc)
1618 ni (PPi p n ty sc) = niTacImp p ++ (n : (ni ty ++ ni sc))
1619 ni (PEq _ l r) = ni l ++ ni r
1620 ni (PRewrite _ l r _) = ni l ++ ni r
1621 ni (PTyped l r) = ni l ++ ni r
1622 ni (PPair _ _ l r) = ni l ++ ni r
1623 ni (PDPair _ _ (PRef _ n) t r) = ni t ++ ni r
1624 ni (PDPair _ _ l t r) = ni l ++ ni t ++ ni r
1625 ni (PAlternative a as) = concatMap (ni) as
1626 ni (PHidden tm) = ni tm
1627 ni (PUnifyLog tm) = ni tm
1628 ni (PDisamb _ tm) = ni tm
1629 ni (PNoImplicits tm) = ni tm
1630 ni _ = []
1632 niTacImp (TacImp _ _ scr) = ni scr
1633 niTacImp _ = []
1635-- Return names which are free in the given term.
1636namesIn :: [(Name, PTerm)] -> IState -> PTerm -> [Name]
1637namesIn uvars ist tm = nub $ ni [] tm
1638 where
1639 ni env (PRef _ n)
1640 | not (n `elem` env)
1641 = case lookupTy n (tt_ctxt ist) of
1642 [] -> [n]
1643 _ -> if n `elem` (map fst uvars) then [n] else []
1644 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
1645 ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
1646 ni env (PCase _ c os) = ni env c ++ concatMap (ni env) (map snd os)
1647 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc
1648 ni env (PPi p n ty sc) = niTacImp env p ++ ni env ty ++ ni (n:env) sc
1649 ni env (PEq _ l r) = ni env l ++ ni env r
1650 ni env (PRewrite _ l r _) = ni env l ++ ni env r
1651 ni env (PTyped l r) = ni env l ++ ni env r
1652 ni env (PPair _ _ l r) = ni env l ++ ni env r
1653 ni env (PDPair _ _ (PRef _ n) t r) = ni env t ++ ni (n:env) r
1654 ni env (PDPair _ _ l t r) = ni env l ++ ni env t ++ ni env r
1655 ni env (PAlternative a as) = concatMap (ni env) as
1656 ni env (PHidden tm) = ni env tm
1657 ni env (PUnifyLog tm) = ni env tm
1658 ni env (PDisamb _ tm) = ni env tm
1659 ni env (PNoImplicits tm) = ni env tm
1660 ni env _ = []
1662 niTacImp env (TacImp _ _ scr) = ni env scr
1663 niTacImp _ _ = []
1665-- Return which of the given names are used in the given term.
1667usedNamesIn :: [Name] -> IState -> PTerm -> [Name]
1668usedNamesIn vars ist tm = nub $ ni [] tm
1669 where -- TODO THINK added niTacImp, but is it right?
1670 ni env (PRef _ n)
1671 | n `elem` vars && not (n `elem` env)
1672 = case lookupDefExact n (tt_ctxt ist) of
1673 Nothing -> [n]
1674 _ -> []
1675 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
1676 ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
1677 ni env (PCase _ c os) = ni env c ++ concatMap (ni env) (map snd os)
1678 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc
1679 ni env (PPi p n ty sc) = niTacImp env p ++ ni env ty ++ ni (n:env) sc
1680 ni env (PEq _ l r) = ni env l ++ ni env r
1681 ni env (PRewrite _ l r _) = ni env l ++ ni env r
1682 ni env (PTyped l r) = ni env l ++ ni env r
1683 ni env (PPair _ _ l r) = ni env l ++ ni env r
1684 ni env (PDPair _ _ (PRef _ n) t r) = ni env t ++ ni (n:env) r
1685 ni env (PDPair _ _ l t r) = ni env l ++ ni env t ++ ni env r
1686 ni env (PAlternative a as) = concatMap (ni env) as
1687 ni env (PHidden tm) = ni env tm
1688 ni env (PUnifyLog tm) = ni env tm
1689 ni env (PDisamb _ tm) = ni env tm
1690 ni env (PNoImplicits tm) = ni env tm
1691 ni env _ = []
1693 niTacImp env (TacImp _ _ scr) = ni env scr
1694 niTacImp _ _ = []