git.iko.soy/Idris-dev
on 222d593 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 (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
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 | WarnOnly
375 | Pkg String
376 | BCAsm String
377 | DumpDefun String
378 | DumpCases String
379 | UseCodegen Codegen
380 | OutputTy OutputType
381 | Extension LanguageExt
382 | InterpretScript String
383 | EvalExpr String
384 | TargetTriple String
385 | TargetCPU String
386 | OptLevel Word
387 | Client String
388 | ShowOrigErr
389 | AutoWidth -- ^ Automatically adjust terminal width
390 | AutoSolve -- ^ Automatically issue "solve" tactic in interactive prover
391 deriving (Show, Eq)
393-- Parsed declarations
395data Fixity = Infixl { prec :: Int }
396 | Infixr { prec :: Int }
397 | InfixN { prec :: Int }
398 | PrefixN { prec :: Int }
399 deriving Eq
400{-!
401deriving instance Binary Fixity
402deriving instance NFData Fixity
403!-}
405instance Show Fixity where
406 show (Infixl i) = "infixl " ++ show i
407 show (Infixr i) = "infixr " ++ show i
408 show (InfixN i) = "infix " ++ show i
409 show (PrefixN i) = "prefix " ++ show i
411data FixDecl = Fix Fixity String
412 deriving Eq
414instance Show FixDecl where
415 show (Fix f s) = show f ++ " " ++ s
417{-!
418deriving instance Binary FixDecl
419deriving instance NFData FixDecl
420!-}
422instance Ord FixDecl where
423 compare (Fix x _) (Fix y _) = compare (prec x) (prec y)
426data Static = Static | Dynamic
427 deriving (Show, Eq)
428{-!
429deriving instance Binary Static
430deriving instance NFData Static
431!-}
433-- Mark bindings with their explicitness, and laziness
434data Plicity = Imp { pargopts :: [ArgOpt],
435 pstatic :: Static,
436 pparam :: Bool }
437 | Exp { pargopts :: [ArgOpt],
438 pstatic :: Static,
439 pparam :: Bool } -- this is a param (rather than index)
440 | Constraint { pargopts :: [ArgOpt],
441 pstatic :: Static }
442 | TacImp { pargopts :: [ArgOpt],
443 pstatic :: Static,
444 pscript :: PTerm }
445 deriving (Show, Eq)
447{-!
448deriving instance Binary Plicity
449deriving instance NFData Plicity
450!-}
452impl = Imp [] Dynamic False
453expl = Exp [] Dynamic False
454expl_param = Exp [] Dynamic True
455constraint = Constraint [] Dynamic
456tacimpl t = TacImp [] Dynamic t
458data FnOpt = Inlinable -- always evaluate when simplifying
459 | TotalFn | PartialFn | CoveringFn
460 | Coinductive | AssertTotal
461 | Dictionary -- type class dictionary, eval only when
462 -- a function argument, and further evaluation resutls
463 | Implicit -- implicit coercion
464 | CExport String -- export, with a C name
465 | ErrorHandler -- ^^ an error handler for use with the ErrorReflection extension
466 | ErrorReverse -- ^^ attempt to reverse normalise before showing in error
467 | Reflection -- a reflecting function, compile-time only
468 | Specialise [(Name, Maybe Int)] -- specialise it, freeze these names
469 deriving (Show, Eq)
470{-!
471deriving instance Binary FnOpt
472deriving instance NFData FnOpt
473!-}
475type FnOpts = [FnOpt]
477inlinable :: FnOpts -> Bool
478inlinable = elem Inlinable
480dictionary :: FnOpts -> Bool
481dictionary = elem Dictionary
484-- | Data declaration options
485data DataOpt = Codata -- Set if the the data-type is coinductive
486 | DefaultEliminator -- Set if an eliminator should be generated for data type
487 | DataErrRev
488 deriving (Show, Eq)
490type DataOpts = [DataOpt]
492-- | Type provider - what to provide
493data ProvideWhat = ProvTerm -- ^ only allow providing terms
494 | ProvPostulate -- ^ only allow postulates
495 | ProvAny -- ^ either is ok
496 deriving (Show, Eq)
498-- | Top-level declarations such as compiler directives, definitions,
499-- datatypes and typeclasses.
500data PDecl' t
501 = PFix FC Fixity [String] -- ^ Fixity declaration
502 | PTy Docstring [(Name, Docstring)] SyntaxInfo FC FnOpts Name t -- ^ Type declaration
503 | PPostulate Docstring SyntaxInfo FC FnOpts Name t -- ^ Postulate
504 | PClauses FC FnOpts Name [PClause' t] -- ^ Pattern clause
505 | PCAF FC Name t -- ^ Top level constant
506 | PData Docstring [(Name, Docstring)] SyntaxInfo FC DataOpts (PData' t) -- ^ Data declaration.
507 | PParams FC [(Name, t)] [PDecl' t] -- ^ Params block
508 | PNamespace String [PDecl' t] -- ^ New namespace
509 | PRecord Docstring SyntaxInfo FC Name t DataOpts Docstring Name t -- ^ Record declaration
510 | PClass Docstring SyntaxInfo FC
511 [t] -- constraints
512 Name
513 [(Name, t)] -- parameters
514 [(Name, Docstring)] -- parameter docstrings
515 [PDecl' t] -- declarations
516 -- ^ Type class: arguments are documentation, syntax info, source location, constraints,
517 -- class name, parameters, method declarations
518 | PInstance SyntaxInfo FC [t] -- constraints
519 Name -- class
520 [t] -- parameters
521 t -- full instance type
522 (Maybe Name) -- explicit name
523 [PDecl' t]
524 -- ^ Instance declaration: arguments are syntax info, source location, constraints,
525 -- class name, parameters, full instance type, optional explicit name, and definitions
526 | PDSL Name (DSL' t) -- ^ DSL declaration
527 | PSyntax FC Syntax -- ^ Syntax definition
528 | PMutual FC [PDecl' t] -- ^ Mutual block
529 | PDirective (Idris ()) -- ^ Compiler directive. The parser inserts the corresponding action in the Idris monad.
530 | PProvider SyntaxInfo FC ProvideWhat Name t t -- ^ Type provider. The first t is the type, the second is the term
531 | PTransform FC Bool t t -- ^ Source-to-source transformation rule. If
532 -- bool is True, lhs and rhs must be convertible
533 deriving Functor
534{-!
535deriving instance Binary PDecl'
536deriving instance NFData PDecl'
537!-}
539-- For elaborator state
540type ElabD a = Elab' [PDecl] a
542-- | One clause of a top-level definition. Term arguments to constructors are:
543--
544-- 1. The whole application (missing for PClauseR and PWithR because they're within a "with" clause)
545--
546-- 2. The list of extra 'with' patterns
547--
548-- 3. The right-hand side
549--
550-- 4. The where block (PDecl' t)
552data PClause' t = PClause FC Name t [t] t [PDecl' t] -- ^ A normal top-level definition.
553 | PWith FC Name t [t] t [PDecl' t]
554 | PClauseR FC [t] t [PDecl' t]
555 | PWithR FC [t] t [PDecl' t]
556 deriving Functor
557{-!
558deriving instance Binary PClause'
559deriving instance NFData PClause'
560!-}
562-- | Data declaration
563data PData' t = PDatadecl { d_name :: Name, -- ^ The name of the datatype
564 d_tcon :: t, -- ^ Type constructor
565 d_cons :: [(Docstring, [(Name, Docstring)], Name, t, FC, [Name])] -- ^ Constructors
566 }
567 -- ^ Data declaration
568 | PLaterdecl { d_name :: Name, d_tcon :: t }
569 -- ^ "Placeholder" for data whose constructors are defined later
570 deriving Functor
571{-!
572deriving instance Binary PData'
573deriving instance NFData PData'
574!-}
576-- Handy to get a free function for applying PTerm -> PTerm functions
577-- across a program, by deriving Functor
579type PDecl = PDecl' PTerm
580type PData = PData' PTerm
581type PClause = PClause' PTerm
583-- get all the names declared in a decl
585declared :: PDecl -> [Name]
586declared (PFix _ _ _) = []
587declared (PTy _ _ _ _ _ n t) = [n]
588declared (PPostulate _ _ _ _ n t) = [n]
589declared (PClauses _ _ n _) = [] -- not a declaration
590declared (PCAF _ n _) = [n]
591declared (PData _ _ _ _ _ (PDatadecl n _ ts)) = n : map fstt ts
592 where fstt (_, _, a, _, _, _) = a
593declared (PData _ _ _ _ _ (PLaterdecl n _)) = [n]
594declared (PParams _ _ ds) = concatMap declared ds
595declared (PNamespace _ ds) = concatMap declared ds
596declared (PRecord _ _ _ n _ _ _ c _) = [n, c]
597declared (PClass _ _ _ _ n _ _ ms) = n : concatMap declared ms
598declared (PInstance _ _ _ _ _ _ _ _) = []
599declared (PDSL n _) = [n]
600declared (PSyntax _ _) = []
601declared (PMutual _ ds) = concatMap declared ds
602declared (PDirective _) = []
604-- get the names declared, not counting nested parameter blocks
605tldeclared :: PDecl -> [Name]
606tldeclared (PFix _ _ _) = []
607tldeclared (PTy _ _ _ _ _ n t) = [n]
608tldeclared (PPostulate _ _ _ _ n t) = [n]
609tldeclared (PClauses _ _ n _) = [] -- not a declaration
610tldeclared (PRecord _ _ _ n _ _ _ c _) = [n, c]
611tldeclared (PData _ _ _ _ _ (PDatadecl n _ ts)) = n : map fstt ts
612 where fstt (_, _, a, _, _, _) = a
613tldeclared (PParams _ _ ds) = []
614tldeclared (PMutual _ ds) = concatMap tldeclared ds
615tldeclared (PNamespace _ ds) = concatMap tldeclared ds
616tldeclared (PClass _ _ _ _ n _ _ ms) = concatMap tldeclared ms
617tldeclared (PInstance _ _ _ _ _ _ _ _) = []
618tldeclared _ = []
620defined :: PDecl -> [Name]
621defined (PFix _ _ _) = []
622defined (PTy _ _ _ _ _ n t) = []
623defined (PPostulate _ _ _ _ n t) = []
624defined (PClauses _ _ n _) = [n] -- not a declaration
625defined (PCAF _ n _) = [n]
626defined (PData _ _ _ _ _ (PDatadecl n _ ts)) = n : map fstt ts
627 where fstt (_, _, a, _, _, _) = a
628defined (PData _ _ _ _ _ (PLaterdecl n _)) = []
629defined (PParams _ _ ds) = concatMap defined ds
630defined (PNamespace _ ds) = concatMap defined ds
631defined (PRecord _ _ _ n _ _ _ c _) = [n, c]
632defined (PClass _ _ _ _ n _ _ ms) = n : concatMap defined ms
633defined (PInstance _ _ _ _ _ _ _ _) = []
634defined (PDSL n _) = [n]
635defined (PSyntax _ _) = []
636defined (PMutual _ ds) = concatMap defined ds
637defined (PDirective _) = []
638--defined _ = []
640updateN :: [(Name, Name)] -> Name -> Name
641updateN ns n | Just n' <- lookup n ns = n'
642updateN _ n = n
644updateNs :: [(Name, Name)] -> PTerm -> PTerm
645updateNs [] t = t
646updateNs ns t = mapPT updateRef t
647 where updateRef (PRef fc f) = PRef fc (updateN ns f)
648 updateRef t = t
650-- updateDNs :: [(Name, Name)] -> PDecl -> PDecl
651-- updateDNs [] t = t
652-- updateDNs ns (PTy s f n t) | Just n' <- lookup n ns = PTy s f n' t
653-- updateDNs ns (PClauses f n c) | Just n' <- lookup n ns = PClauses f n' (map updateCNs c)
654-- where updateCNs ns (PClause n l ts r ds)
655-- = PClause (updateN ns n) (fmap (updateNs ns) l)
656-- (map (fmap (updateNs ns)) ts)
657-- (fmap (updateNs ns) r)
658-- (map (updateDNs ns) ds)
659-- updateDNs ns c = c
661data PunInfo = IsType | IsTerm | TypeOrTerm deriving (Eq, Show)
663-- | High level language terms
664data PTerm = PQuote Raw
665 | PRef FC Name
666 | PInferRef FC Name -- ^ A name to be defined later
667 | PPatvar FC Name
668 | PLam Name PTerm PTerm
669 | PPi Plicity Name PTerm PTerm -- ^ (n : t1) -> t2
670 | PLet Name PTerm PTerm PTerm
671 | PTyped PTerm PTerm -- ^ Term with explicit type
672 | PApp FC PTerm [PArg] -- ^ e.g. IO (), List Char, length x
673 | PAppBind FC PTerm [PArg] -- ^ implicitly bound application
674 | PMatchApp FC Name -- ^ Make an application by type matching
675 | PCase FC PTerm [(PTerm, PTerm)]
676 | PTrue FC PunInfo -- ^ Unit type..?
677 | PFalse FC -- ^ _|_
678 | PRefl FC PTerm
679 | PResolveTC FC
680 | PEq FC PTerm PTerm -- ^ Equality type: A = B
681 | PRewrite FC PTerm PTerm (Maybe PTerm)
682 | PPair FC PunInfo PTerm PTerm
683 | PDPair FC PunInfo PTerm PTerm PTerm
684 | PAlternative Bool [PTerm] -- True if only one may work
685 | PHidden PTerm -- ^ Irrelevant or hidden pattern
686 | PType -- ^ 'Type' type
687 | PGoal FC PTerm Name PTerm
688 | PConstant Const -- ^ Builtin types
689 | Placeholder
690 | PDoBlock [PDo]
691 | PIdiom FC PTerm
692 | PReturn FC
693 | PMetavar Name
694 | PProof [PTactic] -- ^ Proof script
695 | PTactics [PTactic] -- ^ As PProof, but no auto solving
696 | PElabError Err -- ^ Error to report on elaboration
697 | PImpossible -- ^ Special case for declaring when an LHS can't typecheck
698 | PCoerced PTerm -- ^ To mark a coerced argument, so as not to coerce twice
699 | PDisamb [[T.Text]] PTerm -- ^ Preferences for explicit namespaces
700 | PUnifyLog PTerm -- ^ dump a trace of unifications when building term
701 | PNoImplicits PTerm -- ^ never run implicit converions on the term
702 deriving Eq
705{-!
706deriving instance Binary PTerm
707deriving instance NFData PTerm
708!-}
710mapPT :: (PTerm -> PTerm) -> PTerm -> PTerm
711mapPT f t = f (mpt t) where
712 mpt (PLam n t s) = PLam n (mapPT f t) (mapPT f s)
713 mpt (PPi p n t s) = PPi p n (mapPT f t) (mapPT f s)
714 mpt (PLet n ty v s) = PLet n (mapPT f ty) (mapPT f v) (mapPT f s)
715 mpt (PRewrite fc t s g) = PRewrite fc (mapPT f t) (mapPT f s)
716 (fmap (mapPT f) g)
717 mpt (PApp fc t as) = PApp fc (mapPT f t) (map (fmap (mapPT f)) as)
718 mpt (PAppBind fc t as) = PAppBind fc (mapPT f t) (map (fmap (mapPT f)) as)
719 mpt (PCase fc c os) = PCase fc (mapPT f c) (map (pmap (mapPT f)) os)
720 mpt (PEq fc l r) = PEq fc (mapPT f l) (mapPT f r)
721 mpt (PTyped l r) = PTyped (mapPT f l) (mapPT f r)
722 mpt (PPair fc p l r) = PPair fc p (mapPT f l) (mapPT f r)
723 mpt (PDPair fc p l t r) = PDPair fc p (mapPT f l) (mapPT f t) (mapPT f r)
724 mpt (PAlternative a as) = PAlternative a (map (mapPT f) as)
725 mpt (PHidden t) = PHidden (mapPT f t)
726 mpt (PDoBlock ds) = PDoBlock (map (fmap (mapPT f)) ds)
727 mpt (PProof ts) = PProof (map (fmap (mapPT f)) ts)
728 mpt (PTactics ts) = PTactics (map (fmap (mapPT f)) ts)
729 mpt (PUnifyLog tm) = PUnifyLog (mapPT f tm)
730 mpt (PDisamb ns tm) = PDisamb ns (mapPT f tm)
731 mpt (PNoImplicits tm) = PNoImplicits (mapPT f tm)
732 mpt (PGoal fc r n sc) = PGoal fc (mapPT f r) n (mapPT f sc)
733 mpt x = x
736data PTactic' t = Intro [Name] | Intros | Focus Name
737 | Refine Name [Bool] | Rewrite t | DoUnify
738 | Induction Name
739 | Equiv t
740 | MatchRefine Name
741 | LetTac Name t | LetTacTy Name t t
742 | Exact t | Compute | Trivial | TCInstance
743 | ProofSearch Bool Bool Int (Maybe Name) [Name]
744 -- ^ the bool is whether to search recursively
745 | Solve
746 | Attack
747 | ProofState | ProofTerm | Undo
748 | Try (PTactic' t) (PTactic' t)
749 | TSeq (PTactic' t) (PTactic' t)
750 | ApplyTactic t -- see Language.Reflection module
751 | ByReflection t
752 | Reflect t
753 | Fill t
754 | GoalType String (PTactic' t)
755 | TCheck t
756 | TEval t
757 | Qed | Abandon
758 deriving (Show, Eq, Functor)
759{-!
760deriving instance Binary PTactic'
761deriving instance NFData PTactic'
762!-}
763instance Sized a => Sized (PTactic' a) where
764 size (Intro nms) = 1 + size nms
765 size Intros = 1
766 size (Focus nm) = 1 + size nm
767 size (Refine nm bs) = 1 + size nm + length bs
768 size (Rewrite t) = 1 + size t
769 size (Induction t) = 1 + size t
770 size (LetTac nm t) = 1 + size nm + size t
771 size (Exact t) = 1 + size t
772 size Compute = 1
773 size Trivial = 1
774 size Solve = 1
775 size Attack = 1
776 size ProofState = 1
777 size ProofTerm = 1
778 size Undo = 1
779 size (Try l r) = 1 + size l + size r
780 size (TSeq l r) = 1 + size l + size r
781 size (ApplyTactic t) = 1 + size t
782 size (Reflect t) = 1 + size t
783 size (Fill t) = 1 + size t
784 size Qed = 1
785 size Abandon = 1
787type PTactic = PTactic' PTerm
789data PDo' t = DoExp FC t
790 | DoBind FC Name t
791 | DoBindP FC t t [(t,t)]
792 | DoLet FC Name t t
793 | DoLetP FC t t
794 deriving (Eq, Functor)
795{-!
796deriving instance Binary PDo'
797deriving instance NFData PDo'
798!-}
800instance Sized a => Sized (PDo' a) where
801 size (DoExp fc t) = 1 + size fc + size t
802 size (DoBind fc nm t) = 1 + size fc + size nm + size t
803 size (DoBindP fc l r alts) = 1 + size fc + size l + size r + size alts
804 size (DoLet fc nm l r) = 1 + size fc + size nm + size l + size r
805 size (DoLetP fc l r) = 1 + size fc + size l + size r
807type PDo = PDo' PTerm
809-- The priority gives a hint as to elaboration order. Best to elaborate
810-- things early which will help give a more concrete type to other
811-- variables, e.g. a before (interpTy a).
813data PArg' t = PImp { priority :: Int,
814 machine_inf :: Bool, -- true if the machine inferred it
815 argopts :: [ArgOpt],
816 pname :: Name, getTm :: t }
817 | PExp { priority :: Int,
818 argopts :: [ArgOpt],
819 pname :: Name,
820 getTm :: t }
821 | PConstraint { priority :: Int,
822 argopts :: [ArgOpt],
823 pname :: Name,
824 getTm :: t }
825 | PTacImplicit { priority :: Int,
826 argopts :: [ArgOpt],
827 pname :: Name,
828 getScript :: t,
829 getTm :: t }
830 deriving (Show, Eq, Functor)
832data ArgOpt = HideDisplay | InaccessibleArg
833 deriving (Show, Eq)
835instance Sized a => Sized (PArg' a) where
836 size (PImp p _ l nm trm) = 1 + size nm + size trm
837 size (PExp p l nm trm) = 1 + size nm + size trm
838 size (PConstraint p l nm trm) = 1 + size nm +size nm + size trm
839 size (PTacImplicit p l nm scr trm) = 1 + size nm + size scr + size trm
841{-!
842deriving instance Binary PArg'
843deriving instance NFData PArg'
844!-}
846pimp n t mach = PImp 1 mach [] n t
847pexp t = PExp 1 [] (sMN 0 "arg") t
848pconst t = PConstraint 1 [] (sMN 0 "carg") t
849ptacimp n s t = PTacImplicit 2 [] n s t
851type PArg = PArg' PTerm
853-- Type class data
855data ClassInfo = CI { instanceName :: Name,
856 class_methods :: [(Name, (FnOpts, PTerm))],
857 class_defaults :: [(Name, (Name, PDecl))], -- method name -> default impl
858 class_default_superclasses :: [PDecl],
859 class_params :: [Name],
860 class_instances :: [Name] }
861 deriving Show
862{-!
863deriving instance Binary ClassInfo
864deriving instance NFData ClassInfo
865!-}
867-- Type inference data
869data TIData = TIPartial -- ^ a function with a partially defined type
870 | TISolution [Term] -- ^ possible solutions to a metavariable in a type
871 deriving Show
873data OptInfo = Optimise { inaccessible :: [(Int,Name)], -- includes names for error reporting
874 detaggable :: Bool }
875 deriving Show
876{-!
877deriving instance Binary OptInfo
878deriving instance NFData OptInfo
879!-}
882data TypeInfo = TI { con_names :: [Name],
883 codata :: Bool,
884 data_opts :: DataOpts,
885 param_pos :: [Int] }
886 deriving Show
887{-!
888deriving instance Binary TypeInfo
889deriving instance NFData TypeInfo
890!-}
892-- Syntactic sugar info
894data DSL' t = DSL { dsl_bind :: t,
895 dsl_return :: t,
896 dsl_apply :: t,
897 dsl_pure :: t,
898 dsl_var :: Maybe t,
899 index_first :: Maybe t,
900 index_next :: Maybe t,
901 dsl_lambda :: Maybe t,
902 dsl_let :: Maybe t
903 }
904 deriving (Show, Functor)
905{-!
906deriving instance Binary DSL'
907deriving instance NFData DSL'
908!-}
910type DSL = DSL' PTerm
912data SynContext = PatternSyntax | TermSyntax | AnySyntax
913 deriving Show
914{-!
915deriving instance Binary SynContext
916deriving instance NFData SynContext
917!-}
919data Syntax = Rule [SSymbol] PTerm SynContext
920 deriving Show
921{-!
922deriving instance Binary Syntax
923deriving instance NFData Syntax
924!-}
926data SSymbol = Keyword Name
927 | Symbol String
928 | Binding Name
929 | Expr Name
930 | SimpleExpr Name
931 deriving Show
932{-!
933deriving instance Binary SSymbol
934deriving instance NFData SSymbol
935!-}
937initDSL = DSL (PRef f (sUN ">>="))
938 (PRef f (sUN "return"))
939 (PRef f (sUN "<$>"))
940 (PRef f (sUN "pure"))
941 Nothing
942 Nothing
943 Nothing
944 Nothing
945 Nothing
946 where f = fileFC "(builtin)"
948data Using = UImplicit Name PTerm
949 | UConstraint Name [Name]
950 deriving (Show, Eq)
951{-!
952deriving instance Binary Using
953deriving instance NFData Using
954!-}
956data SyntaxInfo = Syn { using :: [Using],
957 syn_params :: [(Name, PTerm)],
958 syn_namespace :: [String],
959 no_imp :: [Name],
960 decoration :: Name -> Name,
961 inPattern :: Bool,
962 implicitAllowed :: Bool,
963 maxline :: Maybe Int,
964 dsl_info :: DSL }
965 deriving Show
966{-!
967deriving instance NFData SyntaxInfo
968deriving instance Binary SyntaxInfo
969!-}
971defaultSyntax = Syn [] [] [] [] id False False Nothing 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 _ _ = []