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