git.iko.soy/Idris-dev
on 79a43c8 help sign in
Idris-dev/src/Idris/AbsSyntaxTree.hs
1733 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 | PQuasiquote PTerm -- ^ `(Term)
708 | PUnquote PTerm -- ^ ,Term
709 deriving Eq
712{-!
713deriving instance Binary PTerm
714deriving instance NFData PTerm
715!-}
717mapPT :: (PTerm -> PTerm) -> PTerm -> PTerm
718mapPT f t = f (mpt t) where
719 mpt (PLam n t s) = PLam n (mapPT f t) (mapPT f s)
720 mpt (PPi p n t s) = PPi p n (mapPT f t) (mapPT f s)
721 mpt (PLet n ty v s) = PLet n (mapPT f ty) (mapPT f v) (mapPT f s)
722 mpt (PRewrite fc t s g) = PRewrite fc (mapPT f t) (mapPT f s)
723 (fmap (mapPT f) g)
724 mpt (PApp fc t as) = PApp fc (mapPT f t) (map (fmap (mapPT f)) as)
725 mpt (PAppBind fc t as) = PAppBind fc (mapPT f t) (map (fmap (mapPT f)) as)
726 mpt (PCase fc c os) = PCase fc (mapPT f c) (map (pmap (mapPT f)) os)
727 mpt (PEq fc l r) = PEq fc (mapPT f l) (mapPT f r)
728 mpt (PTyped l r) = PTyped (mapPT f l) (mapPT f r)
729 mpt (PPair fc p l r) = PPair fc p (mapPT f l) (mapPT f r)
730 mpt (PDPair fc p l t r) = PDPair fc p (mapPT f l) (mapPT f t) (mapPT f r)
731 mpt (PAlternative a as) = PAlternative a (map (mapPT f) as)
732 mpt (PHidden t) = PHidden (mapPT f t)
733 mpt (PDoBlock ds) = PDoBlock (map (fmap (mapPT f)) ds)
734 mpt (PProof ts) = PProof (map (fmap (mapPT f)) ts)
735 mpt (PTactics ts) = PTactics (map (fmap (mapPT f)) ts)
736 mpt (PUnifyLog tm) = PUnifyLog (mapPT f tm)
737 mpt (PDisamb ns tm) = PDisamb ns (mapPT f tm)
738 mpt (PNoImplicits tm) = PNoImplicits (mapPT f tm)
739 mpt (PGoal fc r n sc) = PGoal fc (mapPT f r) n (mapPT f sc)
740 mpt x = x
743data PTactic' t = Intro [Name] | Intros | Focus Name
744 | Refine Name [Bool] | Rewrite t | DoUnify
745 | Induction t
746 | CaseTac t
747 | Equiv t
748 | MatchRefine Name
749 | LetTac Name t | LetTacTy Name t t
750 | Exact t | Compute | Trivial | TCInstance
751 | ProofSearch Bool Bool Int (Maybe Name) [Name]
752 -- ^ the bool is whether to search recursively
753 | Solve
754 | Attack
755 | ProofState | ProofTerm | Undo
756 | Try (PTactic' t) (PTactic' t)
757 | TSeq (PTactic' t) (PTactic' t)
758 | ApplyTactic t -- see Language.Reflection module
759 | ByReflection t
760 | Reflect t
761 | Fill t
762 | GoalType String (PTactic' t)
763 | TCheck t
764 | TEval t
765 | Qed | Abandon
766 deriving (Show, Eq, Functor)
767{-!
768deriving instance Binary PTactic'
769deriving instance NFData PTactic'
770!-}
771instance Sized a => Sized (PTactic' a) where
772 size (Intro nms) = 1 + size nms
773 size Intros = 1
774 size (Focus nm) = 1 + size nm
775 size (Refine nm bs) = 1 + size nm + length bs
776 size (Rewrite t) = 1 + size t
777 size (Induction t) = 1 + size t
778 size (LetTac nm t) = 1 + size nm + size t
779 size (Exact t) = 1 + size t
780 size Compute = 1
781 size Trivial = 1
782 size Solve = 1
783 size Attack = 1
784 size ProofState = 1
785 size ProofTerm = 1
786 size Undo = 1
787 size (Try l r) = 1 + size l + size r
788 size (TSeq l r) = 1 + size l + size r
789 size (ApplyTactic t) = 1 + size t
790 size (Reflect t) = 1 + size t
791 size (Fill t) = 1 + size t
792 size Qed = 1
793 size Abandon = 1
795type PTactic = PTactic' PTerm
797data PDo' t = DoExp FC t
798 | DoBind FC Name t
799 | DoBindP FC t t [(t,t)]
800 | DoLet FC Name t t
801 | DoLetP FC t t
802 deriving (Eq, Functor)
803{-!
804deriving instance Binary PDo'
805deriving instance NFData PDo'
806!-}
808instance Sized a => Sized (PDo' a) where
809 size (DoExp fc t) = 1 + size fc + size t
810 size (DoBind fc nm t) = 1 + size fc + size nm + size t
811 size (DoBindP fc l r alts) = 1 + size fc + size l + size r + size alts
812 size (DoLet fc nm l r) = 1 + size fc + size nm + size l + size r
813 size (DoLetP fc l r) = 1 + size fc + size l + size r
815type PDo = PDo' PTerm
817-- The priority gives a hint as to elaboration order. Best to elaborate
818-- things early which will help give a more concrete type to other
819-- variables, e.g. a before (interpTy a).
821data PArg' t = PImp { priority :: Int,
822 machine_inf :: Bool, -- true if the machine inferred it
823 argopts :: [ArgOpt],
824 pname :: Name, getTm :: t }
825 | PExp { priority :: Int,
826 argopts :: [ArgOpt],
827 pname :: Name,
828 getTm :: t }
829 | PConstraint { priority :: Int,
830 argopts :: [ArgOpt],
831 pname :: Name,
832 getTm :: t }
833 | PTacImplicit { priority :: Int,
834 argopts :: [ArgOpt],
835 pname :: Name,
836 getScript :: t,
837 getTm :: t }
838 deriving (Show, Eq, Functor)
840data ArgOpt = HideDisplay | InaccessibleArg
841 deriving (Show, Eq)
843instance Sized a => Sized (PArg' a) where
844 size (PImp p _ l nm trm) = 1 + size nm + size trm
845 size (PExp p l nm trm) = 1 + size nm + size trm
846 size (PConstraint p l nm trm) = 1 + size nm +size nm + size trm
847 size (PTacImplicit p l nm scr trm) = 1 + size nm + size scr + size trm
849{-!
850deriving instance Binary PArg'
851deriving instance NFData PArg'
852!-}
854pimp n t mach = PImp 1 mach [] n t
855pexp t = PExp 1 [] (sMN 0 "arg") t
856pconst t = PConstraint 1 [] (sMN 0 "carg") t
857ptacimp n s t = PTacImplicit 2 [] n s t
859type PArg = PArg' PTerm
861-- Type class data
863data ClassInfo = CI { instanceName :: Name,
864 class_methods :: [(Name, (FnOpts, PTerm))],
865 class_defaults :: [(Name, (Name, PDecl))], -- method name -> default impl
866 class_default_superclasses :: [PDecl],
867 class_params :: [Name],
868 class_instances :: [Name] }
869 deriving Show
870{-!
871deriving instance Binary ClassInfo
872deriving instance NFData ClassInfo
873!-}
875-- Type inference data
877data TIData = TIPartial -- ^ a function with a partially defined type
878 | TISolution [Term] -- ^ possible solutions to a metavariable in a type
879 deriving Show
881data OptInfo = Optimise { inaccessible :: [(Int,Name)], -- includes names for error reporting
882 detaggable :: Bool }
883 deriving Show
884{-!
885deriving instance Binary OptInfo
886deriving instance NFData OptInfo
887!-}
890data TypeInfo = TI { con_names :: [Name],
891 codata :: Bool,
892 data_opts :: DataOpts,
893 param_pos :: [Int],
894 mutual_types :: [Name] }
895 deriving Show
896{-!
897deriving instance Binary TypeInfo
898deriving instance NFData TypeInfo
899!-}
901-- Syntactic sugar info
903data DSL' t = DSL { dsl_bind :: t,
904 dsl_return :: t,
905 dsl_apply :: t,
906 dsl_pure :: t,
907 dsl_var :: Maybe t,
908 index_first :: Maybe t,
909 index_next :: Maybe t,
910 dsl_lambda :: Maybe t,
911 dsl_let :: Maybe t,
912 dsl_pi :: Maybe t
913 }
914 deriving (Show, Functor)
915{-!
916deriving instance Binary DSL'
917deriving instance NFData DSL'
918!-}
920type DSL = DSL' PTerm
922data SynContext = PatternSyntax | TermSyntax | AnySyntax
923 deriving Show
924{-!
925deriving instance Binary SynContext
926deriving instance NFData SynContext
927!-}
929data Syntax = Rule [SSymbol] PTerm SynContext
930 deriving Show
931{-!
932deriving instance Binary Syntax
933deriving instance NFData Syntax
934!-}
936data SSymbol = Keyword Name
937 | Symbol String
938 | Binding Name
939 | Expr Name
940 | SimpleExpr Name
941 deriving Show
942{-!
943deriving instance Binary SSymbol
944deriving instance NFData SSymbol
945!-}
947initDSL = DSL (PRef f (sUN ">>="))
948 (PRef f (sUN "return"))
949 (PRef f (sUN "<$>"))
950 (PRef f (sUN "pure"))
951 Nothing
952 Nothing
953 Nothing
954 Nothing
955 Nothing
956 Nothing
957 where f = fileFC "(builtin)"
959data Using = UImplicit Name PTerm
960 | UConstraint Name [Name]
961 deriving (Show, Eq)
962{-!
963deriving instance Binary Using
964deriving instance NFData Using
965!-}
967data SyntaxInfo = Syn { using :: [Using],
968 syn_params :: [(Name, PTerm)],
969 syn_namespace :: [String],
970 no_imp :: [Name],
971 decoration :: Name -> Name,
972 inPattern :: Bool,
973 implicitAllowed :: Bool,
974 maxline :: Maybe Int,
975 mut_nesting :: Int,
976 dsl_info :: DSL,
977 syn_in_quasiquote :: Bool }
978 deriving Show
979{-!
980deriving instance NFData SyntaxInfo
981deriving instance Binary SyntaxInfo
982!-}
984defaultSyntax = Syn [] [] [] [] id False False Nothing 0 initDSL False
986expandNS :: SyntaxInfo -> Name -> Name
987expandNS syn n@(NS _ _) = n
988expandNS syn n = case syn_namespace syn of
989 [] -> n
990 xs -> sNS n xs
993-- For inferring types of things
995bi = fileFC "builtin"
997inferTy = sMN 0 "__Infer"
998inferCon = sMN 0 "__infer"
999inferDecl = PDatadecl inferTy
1000 PType
1001 [(emptyDocstring, [], inferCon, PPi impl (sMN 0 "iType") PType (
1002 PPi expl (sMN 0 "ival") (PRef bi (sMN 0 "iType"))
1003 (PRef bi inferTy)), bi, [])]
1004inferOpts = []
1006infTerm t = PApp bi (PRef bi inferCon) [pimp (sMN 0 "iType") Placeholder True, pexp t]
1007infP = P (TCon 6 0) inferTy (TType (UVal 0))
1009getInferTerm, getInferType :: Term -> Term
1010getInferTerm (Bind n b sc) = Bind n b $ getInferTerm sc
1011getInferTerm (App (App _ _) tm) = tm
1012getInferTerm tm = tm -- error ("getInferTerm " ++ show tm)
1014getInferType (Bind n b sc) = Bind n (toTy b) $ getInferType sc
1015 where toTy (Lam t) = Pi t
1016 toTy (PVar t) = PVTy t
1017 toTy b = b
1018getInferType (App (App _ ty) _) = ty
1022-- Handy primitives: Unit, False, Pair, MkPair, =, mkForeign, Elim type class
1024primNames = [unitTy, unitCon,
1025 falseTy, pairTy, pairCon,
1026 eqTy, eqCon, inferTy, inferCon]
1028unitDoc = parseDocstring . T.pack $ "The canonical single-element type, also known as the trivially true proposition."
1029unitTy = sMN 0 "__Unit"
1030unitCon = sMN 0 "__II"
1031unitDecl = PDatadecl unitTy PType
1032 [(parseDocstring . T.pack $ "The trivial constructor for `()`. ", [], unitCon, PRef bi unitTy, bi, [])]
1033unitOpts = [DefaultEliminator]
1035falseDoc = parseDocstring . T.pack $
1036 "The empty type, also known as the trivially false proposition." ++
1037 "\n\n" ++
1038 "Use `FalseElim` or `absurd` to prove anything if you have a variable " ++
1039 "of type `_|_` in scope."
1040falseTy = sMN 0 "__False"
1041falseDecl = PDatadecl falseTy PType []
1042falseOpts = []
1044pairDoc = parseDocstring . T.pack $ "The non-dependent pair type, also known as conjunction."
1045pairTy = sMN 0 "__Pair"
1046pairCon = sMN 0 "__MkPair"
1047pairDecl = PDatadecl pairTy (piBind [(n "A", PType), (n "B", PType)] PType)
1048 [(pairConDoc, pairConParamDoc,
1049 pairCon, PPi impl (n "A") PType (
1050 PPi impl (n "B") PType (
1051 PPi expl (n "a") (PRef bi (n "A")) (
1052 PPi expl (n "b") (PRef bi (n "B"))
1053 (PApp bi (PRef bi pairTy) [pexp (PRef bi (n "A")),
1054 pexp (PRef bi (n "B"))])))), bi, [])]
1055 where n a = sMN 0 a
1056 pairConDoc = parseDocstring . T.pack $ "A pair of elements"
1057 pairConParamDoc = [(n "a", parseDocstring . T.pack $ "the left element of the pair"),
1058 (n "b", parseDocstring . T.pack $ "the right element of the pair")]
1059pairOpts = []
1060pairParamDoc = [(n "A", parseDocstring . T.pack $ "the type of the left elements in the pair"),
1061 (n "B", parseDocstring . T.pack $ "the type of the left elements in the pair")]
1062 where n a = sMN 0 a
1064eqTy = sUN "="
1065eqCon = sUN "refl"
1066eqDoc = parseDocstring . T.pack $
1067 "The propositional equality type. A proof that `x` = `y`." ++
1068 "\n\n" ++
1069 "To use such a proof, pattern-match on it, and the two equal things will " ++
1070 "then need to be the _same_ pattern." ++
1071 "\n\n" ++
1072 "**Note**: Idris's equality type is _heterogeneous_, which means that it " ++
1073 "is possible to state equalities between values of potentially different " ++
1074 "types. This is sometimes referred to in the literature as \"John Major\" " ++
1075 "equality." ++
1076 "\n\n" ++
1077 "Thus, if Idris can't infer the type of one side of the equality, then " ++
1078 "you may need to annotate it. See the function `the`."
1080eqDecl = PDatadecl eqTy (piBindp impl [(n "A", PType), (n "B", PType)]
1081 (piBind [(n "x", PRef bi (n "A")), (n "y", PRef bi (n "B"))]
1082 PType))
1083 [(reflDoc, reflParamDoc,
1084 eqCon, PPi impl (n "A") PType (
1085 PPi impl (n "x") (PRef bi (n "A"))
1086 (PApp bi (PRef bi eqTy) [pimp (n "A") Placeholder False,
1087 pimp (n "B") Placeholder False,
1088 pexp (PRef bi (n "x")),
1089 pexp (PRef bi (n "x"))])), bi, [])]
1090 where n a = sMN 0 a
1091 reflDoc = parseDocstring . T.pack $
1092 "A proof that `x` in fact equals `x`. To construct this, you must have already " ++
1093 "shown that both sides are in fact equal."
1094 reflParamDoc = [(n "A", parseDocstring . T.pack $ "the type at which the equality is proven"),
1095 (n "x", parseDocstring . T.pack $ "the element shown to be equal to itself.")]
1097eqParamDoc = [(n "A", parseDocstring . T.pack $ "the type of the left side of the equality"),
1098 (n "B", parseDocstring . T.pack $ "the type of the right side of the equality")
1100 where n a = sMN 0 a
1102eqOpts = []
1104elimName = sUN "__Elim"
1105elimMethElimTy = sUN "__elimTy"
1106elimMethElim = sUN "elim"
1107elimDecl = PClass (parseDocstring . T.pack $ "Type class for eliminators") defaultSyntax bi [] elimName [(sUN "scrutineeType", PType)] []
1108 [PTy emptyDocstring [] defaultSyntax bi [TotalFn] elimMethElimTy PType,
1109 PTy emptyDocstring [] defaultSyntax bi [TotalFn] elimMethElim (PRef bi elimMethElimTy)]
1111-- Defined in builtins.idr
1112sigmaTy = sUN "Sigma"
1113existsCon = sUN "Sg_intro"
1115piBind :: [(Name, PTerm)] -> PTerm -> PTerm
1116piBind = piBindp expl
1118piBindp :: Plicity -> [(Name, PTerm)] -> PTerm -> PTerm
1119piBindp p [] t = t
1120piBindp p ((n, ty):ns) t = PPi p n ty (piBindp p ns t)
1123-- Pretty-printing declarations and terms
1125-- These "show" instances render to an absurdly wide screen because inserted line breaks
1126-- could interfere with interactive editing, which calls "show".
1128instance Show PTerm where
1129 showsPrec _ tm = (displayS . renderPretty 1.0 10000000 . prettyImp defaultPPOption) tm
1131instance Show PDecl where
1132 showsPrec _ d = (displayS . renderPretty 1.0 10000000 . showDeclImp defaultPPOption) d
1134instance Show PClause where
1135 showsPrec _ c = (displayS . renderPretty 1.0 10000000 . showCImp verbosePPOption) c
1137instance Show PData where
1138 showsPrec _ d = (displayS . renderPretty 1.0 10000000 . showDImp defaultPPOption) d
1140instance Pretty PTerm OutputAnnotation where
1141 pretty = prettyImp defaultPPOption
1143-- | Colourise annotations according to an Idris state. It ignores the names
1144-- in the annotation, as there's no good way to show extended information on a
1145-- terminal.
1146consoleDecorate :: IState -> OutputAnnotation -> String -> String
1147consoleDecorate ist _ | not (idris_colourRepl ist) = id
1148consoleDecorate ist (AnnConst c) = let theme = idris_colourTheme ist
1149 in if constIsType c
1150 then colouriseType theme
1151 else colouriseData theme
1152consoleDecorate ist (AnnData _ _) = colouriseData (idris_colourTheme ist)
1153consoleDecorate ist (AnnType _ _) = colouriseType (idris_colourTheme ist)
1154consoleDecorate ist (AnnBoundName _ True) = colouriseImplicit (idris_colourTheme ist)
1155consoleDecorate ist (AnnBoundName _ False) = colouriseBound (idris_colourTheme ist)
1156consoleDecorate ist AnnKeyword = colouriseKeyword (idris_colourTheme ist)
1157consoleDecorate ist (AnnName n _ _ _) = let ctxt = tt_ctxt ist
1158 theme = idris_colourTheme ist
1159 in case () of
1160 _ | isDConName n ctxt -> colouriseData theme
1161 _ | isFnName n ctxt -> colouriseFun theme
1162 _ | isTConName n ctxt -> colouriseType theme
1163 _ | isPostulateName n ist -> colourisePostulate theme
1164 _ | otherwise -> id -- don't colourise unknown names
1165consoleDecorate ist (AnnFC _) = id
1166consoleDecorate ist (AnnTextFmt fmt) = Idris.Colours.colourise (colour fmt)
1167 where colour BoldText = IdrisColour Nothing True False True False
1168 colour UnderlineText = IdrisColour Nothing True True False False
1169 colour ItalicText = IdrisColour Nothing True False False True
1170consoleDecorate ist (AnnTerm _ _) = id
1172isPostulateName :: Name -> IState -> Bool
1173isPostulateName n ist = S.member n (idris_postulates ist)
1175-- | Pretty-print a high-level closed Idris term with no information about precedence/associativity
1176prettyImp :: PPOption -- ^^ pretty printing options
1177 -> PTerm -- ^^ the term to pretty-print
1178 -> Doc OutputAnnotation
1179prettyImp impl = pprintPTerm impl [] [] []
1181-- | Serialise something to base64 using its Binary instance.
1183-- | Do the right thing for rendering a term in an IState
1184prettyIst :: IState -> PTerm -> Doc OutputAnnotation
1185prettyIst ist = pprintPTerm (ppOptionIst ist) [] [] (idris_infixes ist)
1187-- | Pretty-print a high-level Idris term in some bindings context with infix info
1188pprintPTerm :: PPOption -- ^^ pretty printing options
1189 -> [(Name, Bool)] -- ^^ the currently-bound names and whether they are implicit
1190 -> [Name] -- ^^ names to always show in pi, even if not used
1191 -> [FixDecl] -- ^^ Fixity declarations
1192 -> PTerm -- ^^ the term to pretty-print
1193 -> Doc OutputAnnotation
1194pprintPTerm ppo bnd docArgs infixes = prettySe 10 bnd
1195 where
1196 prettySe :: Int -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation
1197 prettySe p bnd (PQuote r) =
1198 text "![" <> pretty r <> text "]"
1199 prettySe p bnd (PPatvar fc n) = pretty n
1200 prettySe p bnd e
1201 | Just str <- slist p bnd e = str
1202 | Just n <- snat p e = annotate (AnnData "Nat" "") (text (show n))
1203 prettySe p bnd (PRef fc n) = prettyName True (ppopt_impl ppo) bnd n
1204 prettySe p bnd (PLam n ty sc) =
1205 bracket p 2 . group . align . hang 2 $
1206 text "\\" <> bindingOf n False <+> text "=>" <$>
1207 prettySe 10 ((n, False):bnd) sc
1208 prettySe p bnd (PLet n ty v sc) =
1209 bracket p 2 $
1210 kwd "let" <+> bindingOf n False <+> text "=" </>
1211 prettySe 10 bnd v <+> kwd "in" </>
1212 prettySe 10 ((n, False):bnd) sc
1213 prettySe p bnd (PPi (Exp l s _) n ty sc)
1214 | n `elem` allNamesIn sc || ppopt_impl ppo || n `elem` docArgs =
1215 bracket p 2 . group $
1216 enclose lparen rparen (group . align $ bindingOf n False <+> colon <+> prettySe 10 bnd ty) <+>
1217 st <> text "->" <$> prettySe 10 ((n, False):bnd) sc
1218 | otherwise =
1219 bracket p 2 . group $
1220 group (prettySe 1 bnd ty <+> st) <> text "->" <$> group (prettySe 10 ((n, False):bnd) sc)
1221 where
1222 st =
1223 case s of
1224 Static -> text "[static]" <> space
1225 _ -> empty
1226 prettySe p bnd (PPi (Imp l s _) n ty sc)
1227 | ppopt_impl ppo =
1228 bracket p 2 $
1229 lbrace <> bindingOf n True <+> colon <+> prettySe 10 bnd ty <> rbrace <+>
1230 st <> text "->" </> prettySe 10 ((n, True):bnd) sc
1231 | otherwise = prettySe 10 ((n, True):bnd) sc
1232 where
1233 st =
1234 case s of
1235 Static -> text "[static]" <> space
1236 _ -> empty
1237 prettySe p bnd (PPi (Constraint _ _) n ty sc) =
1238 bracket p 2 $
1239 prettySe 10 bnd ty <+> text "=>" </> prettySe 10 ((n, True):bnd) sc
1240 prettySe p bnd (PPi (TacImp _ _ s) n ty sc) =
1241 bracket p 2 $
1242 lbrace <> kwd "tacimp" <+> pretty n <+> colon <+> prettySe 10 bnd ty <>
1243 rbrace <+> text "->" </> prettySe 10 ((n, True):bnd) sc
1244 prettySe p bnd (PApp _ (PRef _ f) args) -- normal names, no explicit args
1245 | UN nm <- basename f
1246 , not (ppopt_impl ppo) && null (getExps args) =
1247 prettyName True (ppopt_impl ppo) bnd f
1248 prettySe p bnd (PAppBind _ (PRef _ f) [])
1249 | not (ppopt_impl ppo) = text "!" <> prettyName True (ppopt_impl ppo) bnd f
1250 prettySe p bnd (PApp _ (PRef _ op) args) -- infix operators
1251 | UN nm <- basename op
1252 , not (tnull nm) &&
1253 (not (ppopt_impl ppo)) && (not $ isAlpha (thead nm)) =
1254 case getExps args of
1255 [] -> opName True
1256 [x] -> group (opName True <$> group (prettySe 0 bnd x))
1257 [l,r] -> let precedence = fromMaybe 20 (fmap prec f)
1258 in bracket p precedence $ inFix l r
1259 (l:r:rest) -> bracket p 1 $
1260 enclose lparen rparen (inFix l r) <+>
1261 align (group (vsep (map (prettyArgSe bnd) rest)))
1262 where opName isPrefix = prettyName isPrefix (ppopt_impl ppo) bnd op
1263 f = getFixity (opStr op)
1264 left l = case f of
1265 Nothing -> prettySe (-1) bnd l
1266 Just (Infixl p') -> prettySe p' bnd l
1267 Just f' -> prettySe (prec f'-1) bnd l
1268 right r = case f of
1269 Nothing -> prettySe (-1) bnd r
1270 Just (Infixr p') -> prettySe p' bnd r
1271 Just f' -> prettySe (prec f'-1) bnd r
1272 inFix l r = align . group $
1273 (left l <+> opName False) <$> group (right r)
1274 prettySe p bnd (PApp _ hd@(PRef fc f) [tm]) -- symbols, like 'foo
1275 | PConstant (Idris.Core.TT.Str str) <- getTm tm,
1276 f == sUN "Symbol_" = annotate (AnnType ("'" ++ str) ("The symbol " ++ str)) $
1277 char '\'' <> prettySe 10 bnd (PRef fc (sUN str))
1278 prettySe p bnd (PApp _ f as) = -- Normal prefix applications
1279 let args = getExps as
1280 fp = prettySe 1 bnd f
1281 in
1282 bracket p 1 . group $
1283 if ppopt_impl ppo
1284 then if null as
1285 then fp
1286 else fp <+> align (vsep (map (prettyArgS bnd) as))
1287 else if null args
1288 then fp
1289 else fp <+> align (vsep (map (prettyArgSe bnd) args))
1290 prettySe p bnd (PCase _ scr opts) =
1291 kwd "case" <+> prettySe 10 bnd scr <+> kwd "of" <> prettyBody
1292 where
1293 prettyBody = foldr (<>) empty $ intersperse (text "|") $ map sc opts
1295 sc (l, r) = nest nestingSize $ prettySe 10 bnd l <+> text "=>" <+> prettySe 10 bnd r
1296 prettySe p bnd (PHidden tm) = text "." <> prettySe 0 bnd tm
1297 prettySe p bnd (PRefl _ _) = annName eqCon $ text "refl"
1298 prettySe p bnd (PResolveTC _) = text "resolvetc"
1299 prettySe p bnd (PTrue _ IsType) = annName unitTy $ text "()"
1300 prettySe p bnd (PTrue _ IsTerm) = annName unitCon $ text "()"
1301 prettySe p bnd (PTrue _ TypeOrTerm) = text "()"
1302 prettySe p bnd (PFalse _) = annName falseTy $ text "_|_"
1303 prettySe p bnd (PEq _ l r) =
1304 bracket p 2 . align . group $
1305 prettySe 10 bnd l <+> eq <$> group (prettySe 10 bnd r)
1306 where eq = annName eqTy (text "=")
1307 prettySe p bnd (PRewrite _ l r _) =
1308 bracket p 2 $
1309 text "rewrite" <+> prettySe 10 bnd l <+> text "in" <+> prettySe 10 bnd r
1310 prettySe p bnd (PTyped l r) =
1311 lparen <> prettySe 10 bnd l <+> colon <+> prettySe 10 bnd r <> rparen
1312 prettySe p bnd pair@(PPair _ pun _ _) -- flatten tuples to the right, like parser
1313 | Just elts <- pairElts pair = enclose (ann lparen) (ann rparen) .
1314 align . group . vsep . punctuate (ann comma) $
1315 map (prettySe 10 bnd) elts
1316 where ann = case pun of
1317 TypeOrTerm -> id
1318 IsType -> annName pairTy
1319 IsTerm -> annName pairCon
1320 prettySe p bnd (PDPair _ TypeOrTerm l t r) =
1321 lparen <> prettySe 10 bnd l <+> text "**" <+> prettySe 10 bnd r <> rparen
1322 prettySe p bnd (PDPair _ IsType (PRef _ n) t r) =
1323 annName sigmaTy lparen <>
1324 bindingOf n False <+>
1325 annName sigmaTy (text "**") <+>
1326 prettySe 10 ((n, False):bnd) r <>
1327 annName sigmaTy rparen
1328 prettySe p bnd (PDPair _ IsType l t r) =
1329 annName sigmaTy lparen <>
1330 prettySe 10 bnd l <+>
1331 annName sigmaTy (text "**") <+>
1332 prettySe 10 bnd r <>
1333 annName sigmaTy rparen
1334 prettySe p bnd (PDPair _ IsTerm l t r) =
1335 annName existsCon lparen <>
1336 prettySe 10 bnd l <+>
1337 annName existsCon (text "**") <+>
1338 prettySe 10 bnd r <>
1339 annName existsCon rparen
1340 prettySe p bnd (PAlternative a as) =
1341 lparen <> text "|" <> prettyAs <> text "|" <> rparen
1342 where
1343 prettyAs =
1344 foldr (\l -> \r -> l <+> text "," <+> r) empty $ map (prettySe 10 bnd) as
1345 prettySe p bnd PType = annotate (AnnType "Type" "The type of types") $ text "Type"
1346 prettySe p bnd (PConstant c) = annotate (AnnConst c) (text (show c))
1347 -- XXX: add pretty for tactics
1348 prettySe p bnd (PProof ts) =
1349 text "proof" <+> lbrace <> nest nestingSize (text . show $ ts) <> rbrace
1350 prettySe p bnd (PTactics ts) =
1351 text "tactics" <+> lbrace <> nest nestingSize (text . show $ ts) <> rbrace
1352 prettySe p bnd (PMetavar n) = text "?" <> pretty n
1353 prettySe p bnd (PReturn f) = kwd "return"
1354 prettySe p bnd PImpossible = kwd "impossible"
1355 prettySe p bnd Placeholder = text "_"
1356 prettySe p bnd (PDoBlock _) = text "do block pretty not implemented"
1357 prettySe p bnd (PCoerced t) = prettySe p bnd t
1358 prettySe p bnd (PElabError s) = pretty s
1359 prettySe p bnd (PQuasiquote t) = text "`(" <> prettySe p bnd t <> text ")"
1360 prettySe p bnd (PUnquote t) = text "~" <> prettySe p bnd t
1362 prettySe p bnd _ = text "missing pretty-printer for term"
1364 prettyArgS bnd (PImp _ _ _ n tm) = prettyArgSi bnd (n, tm)
1365 prettyArgS bnd (PExp _ _ _ tm) = prettyArgSe bnd tm
1366 prettyArgS bnd (PConstraint _ _ _ tm) = prettyArgSc bnd tm
1367 prettyArgS bnd (PTacImplicit _ _ n _ tm) = prettyArgSti bnd (n, tm)
1369 prettyArgSe bnd arg = prettySe 0 bnd arg
1370 prettyArgSi bnd (n, val) = lbrace <> pretty n <+> text "=" <+> prettySe 10 bnd val <> rbrace
1371 prettyArgSc bnd val = lbrace <> lbrace <> prettySe 10 bnd val <> rbrace <> rbrace
1372 prettyArgSti bnd (n, val) = lbrace <> kwd "auto" <+> pretty n <+> text "=" <+> prettySe 10 bnd val <> rbrace
1374 annName :: Name -> Doc OutputAnnotation -> Doc OutputAnnotation
1375 annName n = annotate (AnnName n Nothing Nothing Nothing)
1377 opStr :: Name -> String
1378 opStr (NS n _) = opStr n
1379 opStr (UN n) = T.unpack n
1381 basename :: Name -> Name
1382 basename (NS n _) = basename n
1383 basename n = n
1385 slist' p bnd (PApp _ (PRef _ nil) _)
1386 | not (ppopt_impl ppo) && nsroot nil == sUN "Nil" = Just []
1387 slist' p bnd (PRef _ nil)
1388 | not (ppopt_impl ppo) && nsroot nil == sUN "Nil" = Just []
1389 slist' p bnd (PApp _ (PRef _ cons) args)
1390 | nsroot cons == sUN "::",
1391 (PExp {getTm=tl}):(PExp {getTm=hd}):imps <- reverse args,
1392 all isImp imps,
1393 Just tl' <- slist' p bnd tl
1394 = Just (hd:tl')
1395 where
1396 isImp (PImp {}) = True
1397 isImp _ = False
1398 slist' _ _ tm = Nothing
1400 slist p bnd e | Just es <- slist' p bnd e = Just $
1401 case es of [] -> annotate (AnnData "" "") $ text "[]"
1402 [x] -> enclose left right . group $
1403 prettySe p bnd x
1404 xs -> (enclose left right .
1405 align . group . vsep .
1406 punctuate comma .
1407 map (prettySe p bnd)) xs
1408 where left = (annotate (AnnData "" "") (text "["))
1409 right = (annotate (AnnData "" "") (text "]"))
1410 comma = (annotate (AnnData "" "") (text ","))
1411 slist _ _ _ = Nothing
1413 pairElts :: PTerm -> Maybe [PTerm]
1414 pairElts (PPair _ _ x y) | Just elts <- pairElts y = Just (x:elts)
1415 | otherwise = Just [x, y]
1416 pairElts _ = Nothing
1418 natns = "Prelude.Nat."
1420 snat p (PRef _ z)
1421 | show z == (natns++"Z") || show z == "Z" = Just 0
1422 snat p (PApp _ s [PExp {getTm=n}])
1423 | show s == (natns++"S") || show s == "S",
1424 Just n' <- snat p n
1425 = Just $ 1 + n'
1426 snat _ _ = Nothing
1428 bracket outer inner doc
1429 | inner > outer = lparen <> doc <> rparen
1430 | otherwise = doc
1432 kwd = annotate AnnKeyword . text
1434 fixities :: M.Map String Fixity
1435 fixities = M.fromList [(s, f) | (Fix f s) <- infixes]
1437 getFixity :: String -> Maybe Fixity
1438 getFixity = flip M.lookup fixities
1440prettyDocumentedIst :: IState -> (Name, PTerm, Maybe Docstring) -> Doc OutputAnnotation
1441prettyDocumentedIst ist (name, ty, docs) =
1442 prettyName True True [] name <+> colon <+> align (prettyIst ist ty) <$>
1443 fromMaybe empty (fmap (\d -> renderDocstring d <> line) docs)
1445-- | Pretty-printer helper for the binding site of a name
1446bindingOf :: Name -- ^^ the bound name
1447 -> Bool -- ^^ whether the name is implicit
1448 -> Doc OutputAnnotation
1449bindingOf n imp = annotate (AnnBoundName n imp) (text (show n))
1451-- | Pretty-printer helper for names that attaches the correct annotations
1452prettyName
1453 :: Bool -- ^^ whether the name should be parenthesised if it is an infix operator
1454 -> Bool -- ^^ whether to show namespaces
1455 -> [(Name, Bool)] -- ^^ the current bound variables and whether they are implicit
1456 -> Name -- ^^ the name to pprint
1457 -> Doc OutputAnnotation
1458prettyName infixParen showNS bnd n
1459 | Just imp <- lookup n bnd = annotate (AnnBoundName n imp) fullName
1460 | otherwise = annotate (AnnName n Nothing Nothing Nothing) fullName
1461 where fullName = text nameSpace <> parenthesise (text (baseName n))
1462 baseName (UN n) = T.unpack n
1463 baseName (NS n ns) = baseName n
1464 baseName (MN i s) = T.unpack s
1465 baseName n | n == falseTy = "_|_"
1466 baseName other = show other
1467 nameSpace = case n of
1468 (NS n' ns) -> if showNS then (concatMap (++ ".") . map T.unpack . reverse) ns else ""
1469 _ -> ""
1470 isInfix = case baseName n of
1471 "" -> False
1472 (c : _) -> not (isAlpha c)
1473 parenthesise = if isInfix && infixParen then enclose lparen rparen else id
1476showCImp :: PPOption -> PClause -> Doc OutputAnnotation
1477showCImp ppo (PClause _ n l ws r w)
1478 = prettyImp ppo l <+> showWs ws <+> text "=" <+> prettyImp ppo r
1479 <+> text "where" <+> text (show w)
1480 where
1481 showWs [] = empty
1482 showWs (x : xs) = text "|" <+> prettyImp ppo x <+> showWs xs
1483showCImp ppo (PWith _ n l ws r w)
1484 = prettyImp ppo l <+> showWs ws <+> text "with" <+> prettyImp ppo r
1485 <+> braces (text (show w))
1486 where
1487 showWs [] = empty
1488 showWs (x : xs) = text "|" <+> prettyImp ppo x <+> showWs xs
1491showDImp :: PPOption -> PData -> Doc OutputAnnotation
1492showDImp ppo (PDatadecl n ty cons)
1493 = text "data" <+> text (show n) <+> colon <+> prettyImp ppo ty <+> text "where" <$>
1494 (indent 2 $ vsep (map (\ (_, _, n, t, _, _) -> pipe <+> prettyName True False [] n <+> colon <+> prettyImp ppo t) cons))
1496showDecls :: PPOption -> [PDecl] -> Doc OutputAnnotation
1497showDecls o ds = vsep (map (showDeclImp o) ds)
1499showDeclImp _ (PFix _ f ops) = text (show f) <+> cat (punctuate (text ",") (map text ops))
1500showDeclImp o (PTy _ _ _ _ _ n t) = text "tydecl" <+> text (showCG n) <+> colon <+> prettyImp o t
1501showDeclImp o (PClauses _ _ n cs) = text "pat" <+> text (showCG n) <+> text "\t" <+>
1502 indent 2 (vsep (map (showCImp o) cs))
1503showDeclImp o (PData _ _ _ _ _ d) = showDImp o { ppopt_impl = True } d
1504showDeclImp o (PParams _ ns ps) = text "params" <+> braces (text (show ns) <> line <> showDecls o ps <> line)
1505showDeclImp o (PNamespace n ps) = text "namespace" <+> text n <> braces (line <> showDecls o ps <> line)
1506showDeclImp _ (PSyntax _ syn) = text "syntax" <+> text (show syn)
1507showDeclImp o (PClass _ _ _ cs n ps _ ds)
1508 = text "class" <+> text (show cs) <+> text (show n) <+> text (show ps) <> line <> showDecls o ds
1509showDeclImp o (PInstance _ _ cs n _ t _ ds)
1510 = text "instance" <+> text (show cs) <+> text (show n) <+> prettyImp o t <> line <> showDecls o ds
1511showDeclImp _ _ = text "..."
1512-- showDeclImp (PImport o) = "import " ++ o
1514instance Show (Doc OutputAnnotation) where
1515 show = flip (displayS . renderCompact) ""
1517getImps :: [PArg] -> [(Name, PTerm)]
1518getImps [] = []
1519getImps (PImp _ _ _ n tm : xs) = (n, tm) : getImps xs
1520getImps (_ : xs) = getImps xs
1522getExps :: [PArg] -> [PTerm]
1523getExps [] = []
1524getExps (PExp _ _ _ tm : xs) = tm : getExps xs
1525getExps (_ : xs) = getExps xs
1527getConsts :: [PArg] -> [PTerm]
1528getConsts [] = []
1529getConsts (PConstraint _ _ _ tm : xs) = tm : getConsts xs
1530getConsts (_ : xs) = getConsts xs
1532getAll :: [PArg] -> [PTerm]
1533getAll = map getTm
1536-- | Show Idris name
1537showName :: Maybe IState -- ^^ the Idris state, for information about names and colours
1538 -> [(Name, Bool)] -- ^^ the bound variables and whether they're implicit
1539 -> PPOption -- ^^ pretty printing options
1540 -> Bool -- ^^ whether to colourise
1541 -> Name -- ^^ the term to show
1542 -> String
1543showName ist bnd ppo colour n = case ist of
1544 Just i -> if colour then colourise n (idris_colourTheme i) else showbasic n
1545 Nothing -> showbasic n
1546 where name = if ppopt_impl ppo then show n else showbasic n
1547 showbasic n@(UN _) = showCG n
1548 showbasic (MN _ s) = str s
1549 showbasic (NS n s) = showSep "." (map str (reverse s)) ++ "." ++ showbasic n
1550 showbasic (SN s) = show s
1551 fst3 (x, _, _) = x
1552 colourise n t = let ctxt' = fmap tt_ctxt ist in
1553 case ctxt' of
1554 Nothing -> name
1555 Just ctxt | Just impl <- lookup n bnd -> if impl then colouriseImplicit t name
1556 else colouriseBound t name
1557 | isDConName n ctxt -> colouriseData t name
1558 | isFnName n ctxt -> colouriseFun t name
1559 | isTConName n ctxt -> colouriseType t name
1560 -- The assumption is that if a name is not bound and does not exist in the
1561 -- global context, then we're somewhere in which implicit info has been lost
1562 -- (like error messages). Thus, unknown vars are colourised as implicits.
1563 | otherwise -> colouriseImplicit t name
1565showTm :: IState -- ^^ the Idris state, for information about identifiers and colours
1566 -> PTerm -- ^^ the term to show
1567 -> String
1568showTm ist = displayDecorated (consoleDecorate ist) .
1569 renderPretty 0.8 100000 .
1570 prettyImp (ppOptionIst ist)
1572-- | Show a term with implicits, no colours
1573showTmImpls :: PTerm -> String
1574showTmImpls = flip (displayS . renderCompact . prettyImp verbosePPOption) ""
1578instance Sized PTerm where
1579 size (PQuote rawTerm) = size rawTerm
1580 size (PRef fc name) = size name
1581 size (PLam name ty bdy) = 1 + size ty + size bdy
1582 size (PPi plicity name ty bdy) = 1 + size ty + size bdy
1583 size (PLet name ty def bdy) = 1 + size ty + size def + size bdy
1584 size (PTyped trm ty) = 1 + size trm + size ty
1585 size (PApp fc name args) = 1 + size args
1586 size (PAppBind fc name args) = 1 + size args
1587 size (PCase fc trm bdy) = 1 + size trm + size bdy
1588 size (PTrue fc _) = 1
1589 size (PFalse fc) = 1
1590 size (PRefl fc _) = 1
1591 size (PResolveTC fc) = 1
1592 size (PEq fc left right) = 1 + size left + size right
1593 size (PRewrite fc left right _) = 1 + size left + size right
1594 size (PPair fc _ left right) = 1 + size left + size right
1595 size (PDPair fs _ left ty right) = 1 + size left + size ty + size right
1596 size (PAlternative a alts) = 1 + size alts
1597 size (PHidden hidden) = size hidden
1598 size (PUnifyLog tm) = size tm
1599 size (PDisamb _ tm) = size tm
1600 size (PNoImplicits tm) = size tm
1601 size PType = 1
1602 size (PConstant const) = 1 + size const
1603 size Placeholder = 1
1604 size (PDoBlock dos) = 1 + size dos
1605 size (PIdiom fc term) = 1 + size term
1606 size (PReturn fc) = 1
1607 size (PMetavar name) = 1
1608 size (PProof tactics) = size tactics
1609 size (PElabError err) = size err
1610 size PImpossible = 1
1612getPArity :: PTerm -> Int
1613getPArity (PPi _ _ _ sc) = 1 + getPArity sc
1614getPArity _ = 0
1616-- Return all names, free or globally bound, in the given term.
1618allNamesIn :: PTerm -> [Name]
1619allNamesIn tm = nub $ ni [] tm
1620 where -- TODO THINK added niTacImp, but is it right?
1621 ni env (PRef _ n)
1622 | not (n `elem` env) = [n]
1623 ni env (PPatvar _ n) = [n]
1624 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
1625 ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
1626 ni env (PCase _ c os) = ni env c ++ concatMap (ni env) (map snd os)
1627 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc
1628 ni env (PPi p n ty sc) = niTacImp env p ++ ni env ty ++ ni (n:env) sc
1629 ni env (PHidden tm) = ni env tm
1630 ni env (PEq _ l r) = ni env l ++ ni env r
1631 ni env (PRewrite _ l r _) = ni env l ++ ni env r
1632 ni env (PTyped l r) = ni env l ++ ni env r
1633 ni env (PPair _ _ l r) = ni env l ++ ni env r
1634 ni env (PDPair _ _ (PRef _ n) t r) = ni env t ++ ni (n:env) r
1635 ni env (PDPair _ _ l t r) = ni env l ++ ni env t ++ ni env r
1636 ni env (PAlternative a ls) = concatMap (ni env) ls
1637 ni env (PUnifyLog tm) = ni env tm
1638 ni env (PDisamb _ tm) = ni env tm
1639 ni env (PNoImplicits tm) = ni env tm
1640 ni env _ = []
1642 niTacImp env (TacImp _ _ scr) = ni env scr
1643 niTacImp _ _ = []
1645-- Return all names defined in binders in the given term
1646boundNamesIn :: PTerm -> [Name]
1647boundNamesIn tm = nub $ ni tm
1648 where -- TODO THINK Added niTacImp, but is it right?
1649 ni (PApp _ f as) = ni f ++ concatMap (ni) (map getTm as)
1650 ni (PAppBind _ f as) = ni f ++ concatMap (ni) (map getTm as)
1651 ni (PCase _ c os) = ni c ++ concatMap (ni) (map snd os)
1652 ni (PLam n ty sc) = n : (ni ty ++ ni sc)
1653 ni (PLet n ty val sc) = n : (ni ty ++ ni val ++ ni sc)
1654 ni (PPi p n ty sc) = niTacImp p ++ (n : (ni ty ++ ni sc))
1655 ni (PEq _ l r) = ni l ++ ni r
1656 ni (PRewrite _ l r _) = ni l ++ ni r
1657 ni (PTyped l r) = ni l ++ ni r
1658 ni (PPair _ _ l r) = ni l ++ ni r
1659 ni (PDPair _ _ (PRef _ n) t r) = ni t ++ ni r
1660 ni (PDPair _ _ l t r) = ni l ++ ni t ++ ni r
1661 ni (PAlternative a as) = concatMap (ni) as
1662 ni (PHidden tm) = ni tm
1663 ni (PUnifyLog tm) = ni tm
1664 ni (PDisamb _ tm) = ni tm
1665 ni (PNoImplicits tm) = ni tm
1666 ni _ = []
1668 niTacImp (TacImp _ _ scr) = ni scr
1669 niTacImp _ = []
1671-- Return names which are free in the given term.
1672namesIn :: [(Name, PTerm)] -> IState -> PTerm -> [Name]
1673namesIn uvars ist tm = nub $ ni [] tm
1674 where
1675 ni env (PRef _ n)
1676 | not (n `elem` env)
1677 = case lookupTy n (tt_ctxt ist) of
1678 [] -> [n]
1679 _ -> if n `elem` (map fst uvars) then [n] else []
1680 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
1681 ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
1682 ni env (PCase _ c os) = ni env c ++
1683 -- names in 'os', not counting the names bound in the cases
1684 (nub (concatMap (ni env) (map snd os))
1685 \\ nub (concatMap (ni env) (map fst os)))
1686 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc
1687 ni env (PPi p n ty sc) = niTacImp env p ++ ni env ty ++ ni (n:env) sc
1688 ni env (PEq _ l r) = ni env l ++ ni env r
1689 ni env (PRewrite _ l r _) = ni env l ++ ni env r
1690 ni env (PTyped l r) = ni env l ++ ni env r
1691 ni env (PPair _ _ l r) = ni env l ++ ni env r
1692 ni env (PDPair _ _ (PRef _ n) t r) = ni env t ++ ni (n:env) r
1693 ni env (PDPair _ _ l t r) = ni env l ++ ni env t ++ ni env r
1694 ni env (PAlternative a as) = concatMap (ni env) as
1695 ni env (PHidden tm) = ni env tm
1696 ni env (PUnifyLog tm) = ni env tm
1697 ni env (PDisamb _ tm) = ni env tm
1698 ni env (PNoImplicits tm) = ni env tm
1699 ni env _ = []
1701 niTacImp env (TacImp _ _ scr) = ni env scr
1702 niTacImp _ _ = []
1704-- Return which of the given names are used in the given term.
1706usedNamesIn :: [Name] -> IState -> PTerm -> [Name]
1707usedNamesIn vars ist tm = nub $ ni [] tm
1708 where -- TODO THINK added niTacImp, but is it right?
1709 ni env (PRef _ n)
1710 | n `elem` vars && not (n `elem` env)
1711 = case lookupDefExact n (tt_ctxt ist) of
1712 Nothing -> [n]
1713 _ -> []
1714 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
1715 ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
1716 ni env (PCase _ c os) = ni env c ++ concatMap (ni env) (map snd os)
1717 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc
1718 ni env (PPi p n ty sc) = niTacImp env p ++ ni env ty ++ ni (n:env) sc
1719 ni env (PEq _ l r) = ni env l ++ ni env r
1720 ni env (PRewrite _ l r _) = ni env l ++ ni env r
1721 ni env (PTyped l r) = ni env l ++ ni env r
1722 ni env (PPair _ _ l r) = ni env l ++ ni env r
1723 ni env (PDPair _ _ (PRef _ n) t r) = ni env t ++ ni (n:env) r
1724 ni env (PDPair _ _ l t r) = ni env l ++ ni env t ++ ni env r
1725 ni env (PAlternative a as) = concatMap (ni env) as
1726 ni env (PHidden tm) = ni env tm
1727 ni env (PUnifyLog tm) = ni env tm
1728 ni env (PDisamb _ tm) = ni env tm
1729 ni env (PNoImplicits tm) = ni env tm
1730 ni env _ = []
1732 niTacImp env (TacImp _ _ scr) = ni env scr
1733 niTacImp _ _ = []