git.iko.soy/Idris-dev
on 8407c27 help sign in
Idris-dev/src/Idris/AbsSyntaxTree.hs
1802 lines 73 kB history raw
1{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, DeriveFunctor,
2 TypeSynonymInstances, PatternGuards #-}
4module Idris.AbsSyntaxTree where
6import Idris.Core.TT
7import Idris.Core.Evaluate
8import Idris.Core.Elaborate hiding (Tactic(..))
9import Idris.Core.Typecheck
10import Idris.Docstrings
11import IRTS.Lang
12import IRTS.CodegenCommon
13import Util.Pretty
14import Util.DynamicLinker
16import Idris.Colours
18import System.Console.Haskeline
19import System.IO
21import Control.Monad.Trans.State.Strict
22import Control.Monad.Trans.Error
24import Data.List hiding (group)
25import Data.Char
26import qualified Data.Map as M
27import qualified Data.Text as T
28import qualified Data.Map as M
29import Data.Either
30import qualified Data.Set as S
31import Data.Word (Word)
32import Data.Maybe (fromMaybe)
34import Debug.Trace
36import Text.PrettyPrint.Annotated.Leijen
38data ElabWhat = ETypes | EDefns | EAll
39 deriving (Show, Eq)
41-- Data to pass to recursively called elaborators; e.g. for where blocks,
42-- paramaterised declarations, etc.
44-- rec_elabDecl is used to pass the top level elaborator into other elaborators,
45-- so that we can have mutually recursive elaborators in separate modules without
46-- having to much about with cyclic modules.
47data ElabInfo = EInfo { params :: [(Name, PTerm)],
48 inblock :: Ctxt [Name], -- names in the block, and their params
49 liftname :: Name -> Name,
50 namespace :: Maybe [String],
51 rec_elabDecl :: ElabWhat -> ElabInfo -> PDecl ->
52 Idris () }
54toplevel :: ElabInfo
55toplevel = EInfo [] emptyContext id Nothing (\_ _ _ -> fail "Not implemented")
57eInfoNames :: ElabInfo -> [Name]
58eInfoNames info = map fst (params info) ++ M.keys (inblock info)
60data IOption = IOption { opt_logLevel :: Int,
61 opt_typecase :: Bool,
62 opt_typeintype :: Bool,
63 opt_coverage :: Bool,
64 opt_showimp :: Bool, -- ^^ show implicits
65 opt_errContext :: Bool,
66 opt_repl :: Bool,
67 opt_verbose :: Bool,
68 opt_nobanner :: Bool,
69 opt_quiet :: Bool,
70 opt_codegen :: Codegen,
71 opt_outputTy :: OutputType,
72 opt_ibcsubdir :: FilePath,
73 opt_importdirs :: [FilePath],
74 opt_triple :: String,
75 opt_cpu :: String,
76 opt_optLevel :: Word,
77 opt_cmdline :: [Opt], -- remember whole command line
78 opt_origerr :: Bool,
79 opt_autoSolve :: Bool -- ^ automatically apply "solve" tactic in prover
80 }
81 deriving (Show, Eq)
83defaultOpts = IOption { opt_logLevel = 0
84 , opt_typecase = False
85 , opt_typeintype = False
86 , opt_coverage = True
87 , opt_showimp = False
88 , opt_errContext = False
89 , opt_repl = True
90 , opt_verbose = True
91 , opt_nobanner = False
92 , opt_quiet = False
93 , opt_codegen = ViaC
94 , opt_outputTy = Executable
95 , opt_ibcsubdir = ""
96 , opt_importdirs = []
97 , opt_triple = ""
98 , opt_cpu = ""
99 , opt_optLevel = 2
100 , opt_cmdline = []
101 , opt_origerr = False
102 , opt_autoSolve = True
103 }
105data PPOption = PPOption {
106 ppopt_impl :: Bool -- ^^ whether to show implicits
107} deriving (Show)
109-- | Pretty printing options with default verbosity.
110defaultPPOption :: PPOption
111defaultPPOption = PPOption { ppopt_impl = False }
113-- | Pretty printing options with the most verbosity.
114verbosePPOption :: PPOption
115verbosePPOption = PPOption { ppopt_impl = True }
117-- | Get pretty printing options from the big options record.
118ppOption :: IOption -> PPOption
119ppOption opt = PPOption {
120 ppopt_impl = opt_showimp opt
123-- | Get pretty printing options from an idris state record.
124ppOptionIst :: IState -> PPOption
125ppOptionIst = ppOption . idris_options
127data LanguageExt = TypeProviders | ErrorReflection deriving (Show, Eq, Read, Ord)
129-- | The output mode in use
130data OutputMode = RawOutput | IdeSlave Integer deriving Show
132-- | How wide is the console?
133data ConsoleWidth = InfinitelyWide -- ^ Have pretty-printer assume that lines should not be broken
134 | ColsWide Int -- ^ Manually specified - must be positive
135 | AutomaticWidth -- ^ Attempt to determine width, or 80 otherwise
137-- | The global state used in the Idris monad
138data IState = IState {
139 tt_ctxt :: Context, -- ^ All the currently defined names and their terms
140 idris_constraints :: [(UConstraint, FC)],
141 -- ^ A list of universe constraints and their corresponding source locations
142 idris_infixes :: [FixDecl], -- ^ Currently defined infix operators
143 idris_implicits :: Ctxt [PArg],
144 idris_statics :: Ctxt [Bool],
145 idris_classes :: Ctxt ClassInfo,
146 idris_dsls :: Ctxt DSL,
147 idris_optimisation :: Ctxt OptInfo,
148 idris_datatypes :: Ctxt TypeInfo,
149 idris_namehints :: Ctxt [Name],
150 idris_patdefs :: Ctxt ([([Name], Term, Term)], [PTerm]), -- not exported
151 -- ^ list of lhs/rhs, and a list of missing clauses
152 idris_flags :: Ctxt [FnOpt],
153 idris_callgraph :: Ctxt CGInfo, -- name, args used in each pos
154 idris_calledgraph :: Ctxt [Name],
155 idris_docstrings :: Ctxt (Docstring, [(Name, Docstring)]),
156 idris_tyinfodata :: Ctxt TIData,
157 idris_totcheck :: [(FC, Name)], -- names to check totality on
158 idris_defertotcheck :: [(FC, Name)], -- names to check at the end
159 idris_totcheckfail :: [(FC, String)],
160 idris_options :: IOption,
161 idris_name :: Int,
162 idris_lineapps :: [((FilePath, Int), PTerm)],
163 -- ^ Full application LHS on source line
164 idris_metavars :: [(Name, (Maybe Name, Int, Bool))], -- ^ The currently defined but not proven metavariables
165 idris_coercions :: [Name],
166 idris_transforms :: [(Term, Term)],
167 idris_errRev :: [(Term, Term)],
168 syntax_rules :: [Syntax],
169 syntax_keywords :: [String],
170 imported :: [FilePath], -- ^ The imported modules
171 idris_scprims :: [(Name, (Int, PrimFn))],
172 idris_objs :: [(Codegen, FilePath)],
173 idris_libs :: [(Codegen, String)],
174 idris_cgflags :: [(Codegen, String)],
175 idris_hdrs :: [(Codegen, String)],
176 idris_imported :: [FilePath], -- ^ Imported ibc file names
177 proof_list :: [(Name, [String])],
178 errSpan :: Maybe FC,
179 parserWarnings :: [(FC, Err)],
180 lastParse :: Maybe Name,
181 indent_stack :: [Int],
182 brace_stack :: [Maybe Int],
183 lastTokenSpan :: Maybe FC, -- ^ What was the span of the latest token parsed?
184 idris_parsedSpan :: Maybe FC,
185 hide_list :: [(Name, Maybe Accessibility)],
186 default_access :: Accessibility,
187 default_total :: Bool,
188 ibc_write :: [IBCWrite],
189 compiled_so :: Maybe String,
190 idris_dynamic_libs :: [DynamicLib],
191 idris_language_extensions :: [LanguageExt],
192 idris_outputmode :: OutputMode,
193 idris_colourRepl :: Bool,
194 idris_colourTheme :: ColourTheme,
195 idris_outh :: Handle,
196 idris_errorhandlers :: [Name], -- ^ Global error handlers
197 idris_nameIdx :: (Int, Ctxt (Int, Name)),
198 idris_function_errorhandlers :: Ctxt (M.Map Name (S.Set Name)), -- ^ Specific error handlers
199 module_aliases :: M.Map [T.Text] [T.Text],
200 idris_consolewidth :: ConsoleWidth, -- ^ How many chars wide is the console?
201 idris_postulates :: S.Set Name,
202 idris_whocalls :: Maybe (M.Map Name [Name]),
203 idris_callswho :: Maybe (M.Map Name [Name])
204 }
206-- Required for parsers library, and therefore trifecta
207instance Show IState where
208 show = const "{internal state}"
210data SizeChange = Smaller | Same | Bigger | Unknown
211 deriving (Show, Eq)
212{-!
213deriving instance Binary SizeChange
214deriving instance NFData SizeChange
215!-}
217type SCGEntry = (Name, [Maybe (Int, SizeChange)])
218type UsageReason = (Name, Int) -- fn_name, its_arg_number
220data CGInfo = CGInfo { argsdef :: [Name],
221 calls :: [(Name, [[Name]])],
222 scg :: [SCGEntry],
223 argsused :: [Name],
224 usedpos :: [(Int, [UsageReason])] }
225 deriving Show
226{-!
227deriving instance Binary CGInfo
228deriving instance NFData CGInfo
229!-}
231primDefs = [sUN "unsafePerformPrimIO",
232 sUN "mkLazyForeignPrim",
233 sUN "mkForeignPrim",
234 sUN "FalseElim"]
236-- information that needs writing for the current module's .ibc file
237data IBCWrite = IBCFix FixDecl
238 | IBCImp Name
239 | IBCStatic Name
240 | IBCClass Name
241 | IBCInstance Bool Name Name
242 | IBCDSL Name
243 | IBCData Name
244 | IBCOpt Name
245 | IBCMetavar Name
246 | IBCSyntax Syntax
247 | IBCKeyword String
248 | IBCImport FilePath
249 | IBCObj Codegen FilePath
250 | IBCLib Codegen String
251 | IBCCGFlag Codegen String
252 | IBCDyLib String
253 | IBCHeader Codegen String
254 | IBCAccess Name Accessibility
255 | IBCMetaInformation Name MetaInformation
256 | IBCTotal Name Totality
257 | IBCFlags Name [FnOpt]
258 | IBCTrans (Term, Term)
259 | IBCErrRev (Term, Term)
260 | IBCCG Name
261 | IBCDoc Name
262 | IBCCoercion Name
263 | IBCDef Name -- i.e. main context
264 | IBCNameHint (Name, Name)
265 | IBCLineApp FilePath Int PTerm
266 | IBCErrorHandler Name
267 | IBCFunctionErrorHandler Name Name Name
268 | IBCPostulate Name
269 | IBCTotCheckErr FC String
270 | IBCParsedRegion FC
271 deriving Show
273-- | The initial state for the compiler
274idrisInit :: IState
275idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext
276 emptyContext emptyContext emptyContext emptyContext
277 emptyContext emptyContext emptyContext emptyContext
278 emptyContext emptyContext
279 [] [] [] defaultOpts 6 [] [] [] [] [] [] [] [] [] [] [] [] []
280 [] [] Nothing [] Nothing [] [] Nothing Nothing [] Hidden False [] Nothing [] [] RawOutput
281 True defaultTheme stdout [] (0, emptyContext) emptyContext M.empty
282 AutomaticWidth S.empty Nothing Nothing
284-- | The monad for the main REPL - reading and processing files and updating
285-- global state (hence the IO inner monad).
286--type Idris = WriterT [Either String (IO ())] (State IState a))
287type Idris = StateT IState (ErrorT Err IO)
289-- Commands in the REPL
291data Codegen = ViaC
292 | ViaJava
293 | ViaNode
294 | ViaJavaScript
295 | ViaLLVM
296 | Bytecode
297 deriving (Show, Eq)
299-- | REPL commands
300data Command = Quit
301 | Help
302 | Eval PTerm
303 | NewDefn [PDecl] -- ^ Each 'PDecl' should be either a type declaration (at most one) or a clause defining the same name.
304 | Check PTerm
305 | DocStr (Either Name Const)
306 | TotCheck Name
307 | Reload
308 | Load FilePath (Maybe Int) -- up to maximum line number
309 | ChangeDirectory FilePath
310 | ModImport String
311 | Edit
312 | Compile Codegen String
313 | Execute
314 | ExecVal PTerm
315 | Metavars
316 | Prove Name
317 | AddProof (Maybe Name)
318 | RmProof Name
319 | ShowProof Name
320 | Proofs
321 | Universes
322 | LogLvl Int
323 | Spec PTerm
324 | HNF PTerm
325 | TestInline PTerm
326 | Defn Name
327 | Missing Name
328 | DynamicLink FilePath
329 | ListDynamic
330 | Pattelab PTerm
331 | DebugInfo Name
332 | Search PTerm
333 | CaseSplitAt Bool Int Name
334 | AddClauseFrom Bool Int Name
335 | AddProofClauseFrom Bool Int Name
336 | AddMissing Bool Int Name
337 | MakeWith Bool Int Name
338 | MakeLemma Bool Int Name
339 | DoProofSearch Bool Bool Int Name [Name]
340 -- ^ the first bool is whether to update,
341 -- the second is whether to search recursively (i.e. for the arguments)
342 | SetOpt Opt
343 | UnsetOpt Opt
344 | NOP
345 | SetColour ColourType IdrisColour
346 | ColourOn
347 | ColourOff
348 | ListErrorHandlers
349 | SetConsoleWidth ConsoleWidth
350 | Apropos String
351 | WhoCalls Name
352 | CallsWho Name
353 | MakeDoc String -- IdrisDoc
354 | Warranty
356data Opt = Filename String
357 | Quiet
358 | NoBanner
359 | ColourREPL Bool
360 | Ideslave
361 | ShowLibs
362 | ShowLibdir
363 | ShowIncs
364 | NoBasePkgs
365 | NoPrelude
366 | NoBuiltins -- only for the really primitive stuff!
367 | NoREPL
368 | OLogging Int
369 | Output String
370 | TypeCase
371 | TypeInType
372 | DefaultTotal
373 | DefaultPartial
374 | WarnPartial
375 | WarnReach
376 | NoCoverage
377 | ErrContext
378 | ShowImpl
379 | Verbose
380 | IBCSubDir String
381 | ImportDir String
382 | PkgBuild String
383 | PkgInstall String
384 | PkgClean String
385 | PkgCheck String
386 | PkgREPL String
387 | PkgMkDoc String -- IdrisDoc
388 | PkgTest String
389 | WarnOnly
390 | Pkg String
391 | BCAsm String
392 | DumpDefun String
393 | DumpCases String
394 | UseCodegen Codegen
395 | OutputTy OutputType
396 | Extension LanguageExt
397 | InterpretScript String
398 | EvalExpr String
399 | TargetTriple String
400 | TargetCPU String
401 | OptLevel Word
402 | Client String
403 | ShowOrigErr
404 | AutoWidth -- ^ Automatically adjust terminal width
405 | AutoSolve -- ^ Automatically issue "solve" tactic in interactive prover
406 deriving (Show, Eq)
408-- Parsed declarations
410data Fixity = Infixl { prec :: Int }
411 | Infixr { prec :: Int }
412 | InfixN { prec :: Int }
413 | PrefixN { prec :: Int }
414 deriving Eq
415{-!
416deriving instance Binary Fixity
417deriving instance NFData Fixity
418!-}
420instance Show Fixity where
421 show (Infixl i) = "infixl " ++ show i
422 show (Infixr i) = "infixr " ++ show i
423 show (InfixN i) = "infix " ++ show i
424 show (PrefixN i) = "prefix " ++ show i
426data FixDecl = Fix Fixity String
427 deriving Eq
429instance Show FixDecl where
430 show (Fix f s) = show f ++ " " ++ s
432{-!
433deriving instance Binary FixDecl
434deriving instance NFData FixDecl
435!-}
437instance Ord FixDecl where
438 compare (Fix x _) (Fix y _) = compare (prec x) (prec y)
441data Static = Static | Dynamic
442 deriving (Show, Eq)
443{-!
444deriving instance Binary Static
445deriving instance NFData Static
446!-}
448-- Mark bindings with their explicitness, and laziness
449data Plicity = Imp { pargopts :: [ArgOpt],
450 pstatic :: Static,
451 pparam :: Bool }
452 | Exp { pargopts :: [ArgOpt],
453 pstatic :: Static,
454 pparam :: Bool } -- this is a param (rather than index)
455 | Constraint { pargopts :: [ArgOpt],
456 pstatic :: Static }
457 | TacImp { pargopts :: [ArgOpt],
458 pstatic :: Static,
459 pscript :: PTerm }
460 deriving (Show, Eq)
462{-!
463deriving instance Binary Plicity
464deriving instance NFData Plicity
465!-}
467impl = Imp [] Dynamic False
468expl = Exp [] Dynamic False
469expl_param = Exp [] Dynamic True
470constraint = Constraint [] Dynamic
471tacimpl t = TacImp [] Dynamic t
473data FnOpt = Inlinable -- always evaluate when simplifying
474 | TotalFn | PartialFn | CoveringFn
475 | Coinductive | AssertTotal
476 | Dictionary -- type class dictionary, eval only when
477 -- a function argument, and further evaluation resutls
478 | Implicit -- implicit coercion
479 | CExport String -- export, with a C name
480 | ErrorHandler -- ^^ an error handler for use with the ErrorReflection extension
481 | ErrorReverse -- ^^ attempt to reverse normalise before showing in error
482 | Reflection -- a reflecting function, compile-time only
483 | Specialise [(Name, Maybe Int)] -- specialise it, freeze these names
484 deriving (Show, Eq)
485{-!
486deriving instance Binary FnOpt
487deriving instance NFData FnOpt
488!-}
490type FnOpts = [FnOpt]
492inlinable :: FnOpts -> Bool
493inlinable = elem Inlinable
495dictionary :: FnOpts -> Bool
496dictionary = elem Dictionary
499-- | Data declaration options
500data DataOpt = Codata -- ^ Set if the the data-type is coinductive
501 | DefaultEliminator -- ^ Set if an eliminator should be generated for data type
502 | DefaultCaseFun -- ^ Set if a case function should be generated for data type
503 | DataErrRev
504 deriving (Show, Eq)
506type DataOpts = [DataOpt]
508-- | Type provider - what to provide
509data ProvideWhat' t = ProvTerm t t -- ^ the first is the goal type, the second is the term
510 | ProvPostulate t -- ^ goal type must be Type, so only term
511 deriving (Show, Eq, Functor)
513type ProvideWhat = ProvideWhat' PTerm
515-- | Top-level declarations such as compiler directives, definitions,
516-- datatypes and typeclasses.
517data PDecl' t
518 = PFix FC Fixity [String] -- ^ Fixity declaration
519 | PTy Docstring [(Name, Docstring)] SyntaxInfo FC FnOpts Name t -- ^ Type declaration
520 | PPostulate Docstring SyntaxInfo FC FnOpts Name t -- ^ Postulate
521 | PClauses FC FnOpts Name [PClause' t] -- ^ Pattern clause
522 | PCAF FC Name t -- ^ Top level constant
523 | PData Docstring [(Name, Docstring)] SyntaxInfo FC DataOpts (PData' t) -- ^ Data declaration.
524 | PParams FC [(Name, t)] [PDecl' t] -- ^ Params block
525 | PNamespace String [PDecl' t] -- ^ New namespace
526 | PRecord Docstring SyntaxInfo FC Name t DataOpts Docstring Name t -- ^ Record declaration
527 | PClass Docstring SyntaxInfo FC
528 [t] -- constraints
529 Name
530 [(Name, t)] -- parameters
531 [(Name, Docstring)] -- parameter docstrings
532 [PDecl' t] -- declarations
533 -- ^ Type class: arguments are documentation, syntax info, source location, constraints,
534 -- class name, parameters, method declarations
535 | PInstance SyntaxInfo FC [t] -- constraints
536 Name -- class
537 [t] -- parameters
538 t -- full instance type
539 (Maybe Name) -- explicit name
540 [PDecl' t]
541 -- ^ Instance declaration: arguments are syntax info, source location, constraints,
542 -- class name, parameters, full instance type, optional explicit name, and definitions
543 | PDSL Name (DSL' t) -- ^ DSL declaration
544 | PSyntax FC Syntax -- ^ Syntax definition
545 | PMutual FC [PDecl' t] -- ^ Mutual block
546 | PDirective (Idris ()) -- ^ Compiler directive. The parser inserts the corresponding action in the Idris monad.
547 | PProvider SyntaxInfo FC (ProvideWhat' t) Name -- ^ Type provider. The first t is the type, the second is the term
548 | PTransform FC Bool t t -- ^ Source-to-source transformation rule. If
549 -- bool is True, lhs and rhs must be convertible
550 deriving Functor
551{-!
552deriving instance Binary PDecl'
553deriving instance NFData PDecl'
554!-}
556-- For elaborator state
557type ElabD a = Elab' [PDecl] a
559-- | One clause of a top-level definition. Term arguments to constructors are:
560--
561-- 1. The whole application (missing for PClauseR and PWithR because they're within a "with" clause)
562--
563-- 2. The list of extra 'with' patterns
564--
565-- 3. The right-hand side
566--
567-- 4. The where block (PDecl' t)
569data PClause' t = PClause FC Name t [t] t [PDecl' t] -- ^ A normal top-level definition.
570 | PWith FC Name t [t] t [PDecl' t]
571 | PClauseR FC [t] t [PDecl' t]
572 | PWithR FC [t] t [PDecl' t]
573 deriving Functor
574{-!
575deriving instance Binary PClause'
576deriving instance NFData PClause'
577!-}
579-- | Data declaration
580data PData' t = PDatadecl { d_name :: Name, -- ^ The name of the datatype
581 d_tcon :: t, -- ^ Type constructor
582 d_cons :: [(Docstring, [(Name, Docstring)], Name, t, FC, [Name])] -- ^ Constructors
583 }
584 -- ^ Data declaration
585 | PLaterdecl { d_name :: Name, d_tcon :: t }
586 -- ^ "Placeholder" for data whose constructors are defined later
587 deriving Functor
588{-!
589deriving instance Binary PData'
590deriving instance NFData PData'
591!-}
593-- Handy to get a free function for applying PTerm -> PTerm functions
594-- across a program, by deriving Functor
596type PDecl = PDecl' PTerm
597type PData = PData' PTerm
598type PClause = PClause' PTerm
600-- get all the names declared in a decl
602declared :: PDecl -> [Name]
603declared (PFix _ _ _) = []
604declared (PTy _ _ _ _ _ n t) = [n]
605declared (PPostulate _ _ _ _ n t) = [n]
606declared (PClauses _ _ n _) = [] -- not a declaration
607declared (PCAF _ n _) = [n]
608declared (PData _ _ _ _ _ (PDatadecl n _ ts)) = n : map fstt ts
609 where fstt (_, _, a, _, _, _) = a
610declared (PData _ _ _ _ _ (PLaterdecl n _)) = [n]
611declared (PParams _ _ ds) = concatMap declared ds
612declared (PNamespace _ ds) = concatMap declared ds
613declared (PRecord _ _ _ n _ _ _ c _) = [n, c]
614declared (PClass _ _ _ _ n _ _ ms) = n : concatMap declared ms
615declared (PInstance _ _ _ _ _ _ _ _) = []
616declared (PDSL n _) = [n]
617declared (PSyntax _ _) = []
618declared (PMutual _ ds) = concatMap declared ds
619declared (PDirective _) = []
621-- get the names declared, not counting nested parameter blocks
622tldeclared :: PDecl -> [Name]
623tldeclared (PFix _ _ _) = []
624tldeclared (PTy _ _ _ _ _ n t) = [n]
625tldeclared (PPostulate _ _ _ _ n t) = [n]
626tldeclared (PClauses _ _ n _) = [] -- not a declaration
627tldeclared (PRecord _ _ _ n _ _ _ c _) = [n, c]
628tldeclared (PData _ _ _ _ _ (PDatadecl n _ ts)) = n : map fstt ts
629 where fstt (_, _, a, _, _, _) = a
630tldeclared (PParams _ _ ds) = []
631tldeclared (PMutual _ ds) = concatMap tldeclared ds
632tldeclared (PNamespace _ ds) = concatMap tldeclared ds
633tldeclared (PClass _ _ _ _ n _ _ ms) = concatMap tldeclared ms
634tldeclared (PInstance _ _ _ _ _ _ _ _) = []
635tldeclared _ = []
637defined :: PDecl -> [Name]
638defined (PFix _ _ _) = []
639defined (PTy _ _ _ _ _ n t) = []
640defined (PPostulate _ _ _ _ n t) = []
641defined (PClauses _ _ n _) = [n] -- not a declaration
642defined (PCAF _ n _) = [n]
643defined (PData _ _ _ _ _ (PDatadecl n _ ts)) = n : map fstt ts
644 where fstt (_, _, a, _, _, _) = a
645defined (PData _ _ _ _ _ (PLaterdecl n _)) = []
646defined (PParams _ _ ds) = concatMap defined ds
647defined (PNamespace _ ds) = concatMap defined ds
648defined (PRecord _ _ _ n _ _ _ c _) = [n, c]
649defined (PClass _ _ _ _ n _ _ ms) = n : concatMap defined ms
650defined (PInstance _ _ _ _ _ _ _ _) = []
651defined (PDSL n _) = [n]
652defined (PSyntax _ _) = []
653defined (PMutual _ ds) = concatMap defined ds
654defined (PDirective _) = []
655--defined _ = []
657updateN :: [(Name, Name)] -> Name -> Name
658updateN ns n | Just n' <- lookup n ns = n'
659updateN _ n = n
661updateNs :: [(Name, Name)] -> PTerm -> PTerm
662updateNs [] t = t
663updateNs ns t = mapPT updateRef t
664 where updateRef (PRef fc f) = PRef fc (updateN ns f)
665 updateRef t = t
667-- updateDNs :: [(Name, Name)] -> PDecl -> PDecl
668-- updateDNs [] t = t
669-- updateDNs ns (PTy s f n t) | Just n' <- lookup n ns = PTy s f n' t
670-- updateDNs ns (PClauses f n c) | Just n' <- lookup n ns = PClauses f n' (map updateCNs c)
671-- where updateCNs ns (PClause n l ts r ds)
672-- = PClause (updateN ns n) (fmap (updateNs ns) l)
673-- (map (fmap (updateNs ns)) ts)
674-- (fmap (updateNs ns) r)
675-- (map (updateDNs ns) ds)
676-- updateDNs ns c = c
678data PunInfo = IsType | IsTerm | TypeOrTerm deriving (Eq, Show)
680-- | High level language terms
681data PTerm = PQuote Raw
682 | PRef FC Name
683 | PInferRef FC Name -- ^ A name to be defined later
684 | PPatvar FC Name
685 | PLam Name PTerm PTerm
686 | PPi Plicity Name PTerm PTerm -- ^ (n : t1) -> t2
687 | PLet Name PTerm PTerm PTerm
688 | PTyped PTerm PTerm -- ^ Term with explicit type
689 | PApp FC PTerm [PArg] -- ^ e.g. IO (), List Char, length x
690 | PAppBind FC PTerm [PArg] -- ^ implicitly bound application
691 | PMatchApp FC Name -- ^ Make an application by type matching
692 | PCase FC PTerm [(PTerm, PTerm)]
693 | PTrue FC PunInfo -- ^ Unit type..?
694 | PFalse FC -- ^ _|_
695 | PRefl FC PTerm
696 | PResolveTC FC
697 | PEq FC PTerm PTerm PTerm PTerm -- ^ Heterogeneous equality type: A = B
698 | PRewrite FC PTerm PTerm (Maybe PTerm)
699 | PPair FC PunInfo PTerm PTerm
700 | PDPair FC PunInfo PTerm PTerm PTerm
701 | PAlternative Bool [PTerm] -- True if only one may work
702 | PHidden PTerm -- ^ Irrelevant or hidden pattern
703 | PType -- ^ 'Type' type
704 | PGoal FC PTerm Name PTerm
705 | PConstant Const -- ^ Builtin types
706 | Placeholder
707 | PDoBlock [PDo]
708 | PIdiom FC PTerm
709 | PReturn FC
710 | PMetavar Name
711 | PProof [PTactic] -- ^ Proof script
712 | PTactics [PTactic] -- ^ As PProof, but no auto solving
713 | PElabError Err -- ^ Error to report on elaboration
714 | PImpossible -- ^ Special case for declaring when an LHS can't typecheck
715 | PCoerced PTerm -- ^ To mark a coerced argument, so as not to coerce twice
716 | PDisamb [[T.Text]] PTerm -- ^ Preferences for explicit namespaces
717 | PUnifyLog PTerm -- ^ dump a trace of unifications when building term
718 | PNoImplicits PTerm -- ^ never run implicit converions on the term
719 | PQuasiquote PTerm (Maybe PTerm) -- ^ `(Term [: Term])
720 | PUnquote PTerm -- ^ ,Term
721 deriving Eq
724{-!
725deriving instance Binary PTerm
726deriving instance NFData PTerm
727!-}
729mapPT :: (PTerm -> PTerm) -> PTerm -> PTerm
730mapPT f t = f (mpt t) where
731 mpt (PLam n t s) = PLam n (mapPT f t) (mapPT f s)
732 mpt (PPi p n t s) = PPi p n (mapPT f t) (mapPT f s)
733 mpt (PLet n ty v s) = PLet n (mapPT f ty) (mapPT f v) (mapPT f s)
734 mpt (PRewrite fc t s g) = PRewrite fc (mapPT f t) (mapPT f s)
735 (fmap (mapPT f) g)
736 mpt (PApp fc t as) = PApp fc (mapPT f t) (map (fmap (mapPT f)) as)
737 mpt (PAppBind fc t as) = PAppBind fc (mapPT f t) (map (fmap (mapPT f)) as)
738 mpt (PCase fc c os) = PCase fc (mapPT f c) (map (pmap (mapPT f)) os)
739 mpt (PEq fc lt rt l r) = PEq fc (mapPT f lt) (mapPT f rt) (mapPT f l) (mapPT f r)
740 mpt (PTyped l r) = PTyped (mapPT f l) (mapPT f r)
741 mpt (PPair fc p l r) = PPair fc p (mapPT f l) (mapPT f r)
742 mpt (PDPair fc p l t r) = PDPair fc p (mapPT f l) (mapPT f t) (mapPT f r)
743 mpt (PAlternative a as) = PAlternative a (map (mapPT f) as)
744 mpt (PHidden t) = PHidden (mapPT f t)
745 mpt (PDoBlock ds) = PDoBlock (map (fmap (mapPT f)) ds)
746 mpt (PProof ts) = PProof (map (fmap (mapPT f)) ts)
747 mpt (PTactics ts) = PTactics (map (fmap (mapPT f)) ts)
748 mpt (PUnifyLog tm) = PUnifyLog (mapPT f tm)
749 mpt (PDisamb ns tm) = PDisamb ns (mapPT f tm)
750 mpt (PNoImplicits tm) = PNoImplicits (mapPT f tm)
751 mpt (PGoal fc r n sc) = PGoal fc (mapPT f r) n (mapPT f sc)
752 mpt x = x
755data PTactic' t = Intro [Name] | Intros | Focus Name
756 | Refine Name [Bool] | Rewrite t | DoUnify
757 | Induction t
758 | CaseTac t
759 | Equiv t
760 | MatchRefine Name
761 | LetTac Name t | LetTacTy Name t t
762 | Exact t | Compute | Trivial | TCInstance
763 | ProofSearch Bool Bool Int (Maybe Name) [Name]
764 -- ^ the bool is whether to search recursively
765 | Solve
766 | Attack
767 | ProofState | ProofTerm | Undo
768 | Try (PTactic' t) (PTactic' t)
769 | TSeq (PTactic' t) (PTactic' t)
770 | ApplyTactic t -- see Language.Reflection module
771 | ByReflection t
772 | Reflect t
773 | Fill t
774 | GoalType String (PTactic' t)
775 | TCheck t
776 | TEval t
777 | TDocStr (Either Name Const)
778 | TSearch t
779 | Skip
780 | TFail [ErrorReportPart]
781 | Qed | Abandon
782 deriving (Show, Eq, Functor)
783{-!
784deriving instance Binary PTactic'
785deriving instance NFData PTactic'
786!-}
787instance Sized a => Sized (PTactic' a) where
788 size (Intro nms) = 1 + size nms
789 size Intros = 1
790 size (Focus nm) = 1 + size nm
791 size (Refine nm bs) = 1 + size nm + length bs
792 size (Rewrite t) = 1 + size t
793 size (Induction t) = 1 + size t
794 size (LetTac nm t) = 1 + size nm + size t
795 size (Exact t) = 1 + size t
796 size Compute = 1
797 size Trivial = 1
798 size Solve = 1
799 size Attack = 1
800 size ProofState = 1
801 size ProofTerm = 1
802 size Undo = 1
803 size (Try l r) = 1 + size l + size r
804 size (TSeq l r) = 1 + size l + size r
805 size (ApplyTactic t) = 1 + size t
806 size (Reflect t) = 1 + size t
807 size (Fill t) = 1 + size t
808 size Qed = 1
809 size Abandon = 1
810 size Skip = 1
811 size (TFail ts) = 1 + size ts
813type PTactic = PTactic' PTerm
815data PDo' t = DoExp FC t
816 | DoBind FC Name t
817 | DoBindP FC t t [(t,t)]
818 | DoLet FC Name t t
819 | DoLetP FC t t
820 deriving (Eq, Functor)
821{-!
822deriving instance Binary PDo'
823deriving instance NFData PDo'
824!-}
826instance Sized a => Sized (PDo' a) where
827 size (DoExp fc t) = 1 + size fc + size t
828 size (DoBind fc nm t) = 1 + size fc + size nm + size t
829 size (DoBindP fc l r alts) = 1 + size fc + size l + size r + size alts
830 size (DoLet fc nm l r) = 1 + size fc + size nm + size l + size r
831 size (DoLetP fc l r) = 1 + size fc + size l + size r
833type PDo = PDo' PTerm
835-- The priority gives a hint as to elaboration order. Best to elaborate
836-- things early which will help give a more concrete type to other
837-- variables, e.g. a before (interpTy a).
839data PArg' t = PImp { priority :: Int,
840 machine_inf :: Bool, -- true if the machine inferred it
841 argopts :: [ArgOpt],
842 pname :: Name, getTm :: t }
843 | PExp { priority :: Int,
844 argopts :: [ArgOpt],
845 pname :: Name,
846 getTm :: t }
847 | PConstraint { priority :: Int,
848 argopts :: [ArgOpt],
849 pname :: Name,
850 getTm :: t }
851 | PTacImplicit { priority :: Int,
852 argopts :: [ArgOpt],
853 pname :: Name,
854 getScript :: t,
855 getTm :: t }
856 deriving (Show, Eq, Functor)
858data ArgOpt = AlwaysShow | HideDisplay | InaccessibleArg
859 deriving (Show, Eq)
861instance Sized a => Sized (PArg' a) where
862 size (PImp p _ l nm trm) = 1 + size nm + size trm
863 size (PExp p l nm trm) = 1 + size nm + size trm
864 size (PConstraint p l nm trm) = 1 + size nm +size nm + size trm
865 size (PTacImplicit p l nm scr trm) = 1 + size nm + size scr + size trm
867{-!
868deriving instance Binary PArg'
869deriving instance NFData PArg'
870!-}
872pimp n t mach = PImp 1 mach [] n t
873pexp t = PExp 1 [] (sMN 0 "arg") t
874pconst t = PConstraint 1 [] (sMN 0 "carg") t
875ptacimp n s t = PTacImplicit 2 [] n s t
877type PArg = PArg' PTerm
879-- Type class data
881data ClassInfo = CI { instanceName :: Name,
882 class_methods :: [(Name, (FnOpts, PTerm))],
883 class_defaults :: [(Name, (Name, PDecl))], -- method name -> default impl
884 class_default_superclasses :: [PDecl],
885 class_params :: [Name],
886 class_instances :: [Name] }
887 deriving Show
888{-!
889deriving instance Binary ClassInfo
890deriving instance NFData ClassInfo
891!-}
893-- Type inference data
895data TIData = TIPartial -- ^ a function with a partially defined type
896 | TISolution [Term] -- ^ possible solutions to a metavariable in a type
897 deriving Show
899data OptInfo = Optimise { inaccessible :: [(Int,Name)], -- includes names for error reporting
900 detaggable :: Bool }
901 deriving Show
902{-!
903deriving instance Binary OptInfo
904deriving instance NFData OptInfo
905!-}
908data TypeInfo = TI { con_names :: [Name],
909 codata :: Bool,
910 data_opts :: DataOpts,
911 param_pos :: [Int],
912 mutual_types :: [Name] }
913 deriving Show
914{-!
915deriving instance Binary TypeInfo
916deriving instance NFData TypeInfo
917!-}
919-- Syntactic sugar info
921data DSL' t = DSL { dsl_bind :: t,
922 dsl_return :: t,
923 dsl_apply :: t,
924 dsl_pure :: t,
925 dsl_var :: Maybe t,
926 index_first :: Maybe t,
927 index_next :: Maybe t,
928 dsl_lambda :: Maybe t,
929 dsl_let :: Maybe t,
930 dsl_pi :: Maybe t
931 }
932 deriving (Show, Functor)
933{-!
934deriving instance Binary DSL'
935deriving instance NFData DSL'
936!-}
938type DSL = DSL' PTerm
940data SynContext = PatternSyntax | TermSyntax | AnySyntax
941 deriving Show
942{-!
943deriving instance Binary SynContext
944deriving instance NFData SynContext
945!-}
947data Syntax = Rule [SSymbol] PTerm SynContext
948 deriving Show
949{-!
950deriving instance Binary Syntax
951deriving instance NFData Syntax
952!-}
954data SSymbol = Keyword Name
955 | Symbol String
956 | Binding Name
957 | Expr Name
958 | SimpleExpr Name
959 deriving Show
960{-!
961deriving instance Binary SSymbol
962deriving instance NFData SSymbol
963!-}
965initDSL = DSL (PRef f (sUN ">>="))
966 (PRef f (sUN "return"))
967 (PRef f (sUN "<$>"))
968 (PRef f (sUN "pure"))
969 Nothing
970 Nothing
971 Nothing
972 Nothing
973 Nothing
974 Nothing
975 where f = fileFC "(builtin)"
977data Using = UImplicit Name PTerm
978 | UConstraint Name [Name]
979 deriving (Show, Eq)
980{-!
981deriving instance Binary Using
982deriving instance NFData Using
983!-}
985data SyntaxInfo = Syn { using :: [Using],
986 syn_params :: [(Name, PTerm)],
987 syn_namespace :: [String],
988 no_imp :: [Name],
989 decoration :: Name -> Name,
990 inPattern :: Bool,
991 implicitAllowed :: Bool,
992 maxline :: Maybe Int,
993 mut_nesting :: Int,
994 dsl_info :: DSL,
995 syn_in_quasiquote :: Bool }
996 deriving Show
997{-!
998deriving instance NFData SyntaxInfo
999deriving instance Binary SyntaxInfo
1000!-}
1002defaultSyntax = Syn [] [] [] [] id False False Nothing 0 initDSL False
1004expandNS :: SyntaxInfo -> Name -> Name
1005expandNS syn n@(NS _ _) = n
1006expandNS syn n = case syn_namespace syn of
1007 [] -> n
1008 xs -> sNS n xs
1011-- For inferring types of things
1013bi = fileFC "builtin"
1015inferTy = sMN 0 "__Infer"
1016inferCon = sMN 0 "__infer"
1017inferDecl = PDatadecl inferTy
1018 PType
1019 [(emptyDocstring, [], inferCon, PPi impl (sMN 0 "iType") PType (
1020 PPi expl (sMN 0 "ival") (PRef bi (sMN 0 "iType"))
1021 (PRef bi inferTy)), bi, [])]
1022inferOpts = []
1024infTerm t = PApp bi (PRef bi inferCon) [pimp (sMN 0 "iType") Placeholder True, pexp t]
1025infP = P (TCon 6 0) inferTy (TType (UVal 0))
1027getInferTerm, getInferType :: Term -> Term
1028getInferTerm (Bind n b sc) = Bind n b $ getInferTerm sc
1029getInferTerm (App (App _ _) tm) = tm
1030getInferTerm tm = tm -- error ("getInferTerm " ++ show tm)
1032getInferType (Bind n b sc) = Bind n (toTy b) $ getInferType sc
1033 where toTy (Lam t) = Pi t
1034 toTy (PVar t) = PVTy t
1035 toTy b = b
1036getInferType (App (App _ ty) _) = ty
1040-- Handy primitives: Unit, False, Pair, MkPair, =, mkForeign, Elim type class
1042primNames = [unitTy, unitCon,
1043 falseTy, pairTy, pairCon,
1044 eqTy, eqCon, inferTy, inferCon]
1046unitDoc = parseDocstring . T.pack $ "The canonical single-element type, also known as the trivially true proposition."
1047unitTy = sMN 0 "__Unit"
1048unitCon = sMN 0 "__II"
1049unitDecl = PDatadecl unitTy PType
1050 [(parseDocstring . T.pack $ "The trivial constructor for `()`. ", [], unitCon, PRef bi unitTy, bi, [])]
1051unitOpts = [DefaultEliminator]
1053falseDoc = parseDocstring . T.pack $
1054 "The empty type, also known as the trivially false proposition." ++
1055 "\n\n" ++
1056 "Use `FalseElim` or `absurd` to prove anything if you have a variable " ++
1057 "of type `_|_` in scope."
1058falseTy = sMN 0 "__False"
1059falseDecl = PDatadecl falseTy PType []
1060falseOpts = []
1062pairDoc = parseDocstring . T.pack $ "The non-dependent pair type, also known as conjunction."
1063pairTy = sMN 0 "__Pair"
1064pairCon = sMN 0 "__MkPair"
1065pairDecl = PDatadecl pairTy (piBind [(n "A", PType), (n "B", PType)] PType)
1066 [(pairConDoc, pairConParamDoc,
1067 pairCon, PPi impl (n "A") PType (
1068 PPi impl (n "B") PType (
1069 PPi expl (n "a") (PRef bi (n "A")) (
1070 PPi expl (n "b") (PRef bi (n "B"))
1071 (PApp bi (PRef bi pairTy) [pexp (PRef bi (n "A")),
1072 pexp (PRef bi (n "B"))])))), bi, [])]
1073 where n a = sMN 0 a
1074 pairConDoc = parseDocstring . T.pack $ "A pair of elements"
1075 pairConParamDoc = [(n "a", parseDocstring . T.pack $ "the left element of the pair"),
1076 (n "b", parseDocstring . T.pack $ "the right element of the pair")]
1077pairOpts = []
1078pairParamDoc = [(n "A", parseDocstring . T.pack $ "the type of the left elements in the pair"),
1079 (n "B", parseDocstring . T.pack $ "the type of the left elements in the pair")]
1080 where n a = sMN 0 a
1082eqTy = sUN "="
1083eqCon = sUN "refl"
1084eqDoc = parseDocstring . T.pack $
1085 "The propositional equality type. A proof that `x` = `y`." ++
1086 "\n\n" ++
1087 "To use such a proof, pattern-match on it, and the two equal things will " ++
1088 "then need to be the _same_ pattern." ++
1089 "\n\n" ++
1090 "**Note**: Idris's equality type is potentially _heterogeneous_, which means that it " ++
1091 "is possible to state equalities between values of potentially different " ++
1092 "types. However, Idris will attempt the homogeneous case unless it fails to typecheck." ++
1093 "\n\n" ++
1094 "You may need to use `(~=~)` to explicitly request heterogeneous equality."
1096eqDecl = PDatadecl eqTy (piBindp impl [(n "A", PType), (n "B", PType)]
1097 (piBind [(n "x", PRef bi (n "A")), (n "y", PRef bi (n "B"))]
1098 PType))
1099 [(reflDoc, reflParamDoc,
1100 eqCon, PPi impl (n "A") PType (
1101 PPi impl (n "x") (PRef bi (n "A"))
1102 (PApp bi (PRef bi eqTy) [pimp (n "A") Placeholder False,
1103 pimp (n "B") Placeholder False,
1104 pexp (PRef bi (n "x")),
1105 pexp (PRef bi (n "x"))])), bi, [])]
1106 where n a = sUN a
1107 reflDoc = parseDocstring . T.pack $
1108 "A proof that `x` in fact equals `x`. To construct this, you must have already " ++
1109 "shown that both sides are in fact equal."
1110 reflParamDoc = [(n "A", parseDocstring . T.pack $ "the type at which the equality is proven"),
1111 (n "x", parseDocstring . T.pack $ "the element shown to be equal to itself.")]
1113eqParamDoc = [(n "A", parseDocstring . T.pack $ "the type of the left side of the equality"),
1114 (n "B", parseDocstring . T.pack $ "the type of the right side of the equality")
1116 where n a = sUN a
1118eqOpts = []
1120elimName = sUN "__Elim"
1121elimMethElimTy = sUN "__elimTy"
1122elimMethElim = sUN "elim"
1123elimDecl = PClass (parseDocstring . T.pack $ "Type class for eliminators") defaultSyntax bi [] elimName [(sUN "scrutineeType", PType)] []
1124 [PTy emptyDocstring [] defaultSyntax bi [TotalFn] elimMethElimTy PType,
1125 PTy emptyDocstring [] defaultSyntax bi [TotalFn] elimMethElim (PRef bi elimMethElimTy)]
1127-- Defined in builtins.idr
1128sigmaTy = sUN "Sigma"
1129existsCon = sUN "Sg_intro"
1131piBind :: [(Name, PTerm)] -> PTerm -> PTerm
1132piBind = piBindp expl
1134piBindp :: Plicity -> [(Name, PTerm)] -> PTerm -> PTerm
1135piBindp p [] t = t
1136piBindp p ((n, ty):ns) t = PPi p n ty (piBindp p ns t)
1139-- Pretty-printing declarations and terms
1141-- These "show" instances render to an absurdly wide screen because inserted line breaks
1142-- could interfere with interactive editing, which calls "show".
1144instance Show PTerm where
1145 showsPrec _ tm = (displayS . renderPretty 1.0 10000000 . prettyImp defaultPPOption) tm
1147instance Show PDecl where
1148 showsPrec _ d = (displayS . renderPretty 1.0 10000000 . showDeclImp verbosePPOption) d
1150instance Show PClause where
1151 showsPrec _ c = (displayS . renderPretty 1.0 10000000 . showCImp verbosePPOption) c
1153instance Show PData where
1154 showsPrec _ d = (displayS . renderPretty 1.0 10000000 . showDImp defaultPPOption) d
1156instance Pretty PTerm OutputAnnotation where
1157 pretty = prettyImp defaultPPOption
1159-- | Colourise annotations according to an Idris state. It ignores the names
1160-- in the annotation, as there's no good way to show extended information on a
1161-- terminal.
1162consoleDecorate :: IState -> OutputAnnotation -> String -> String
1163consoleDecorate ist _ | not (idris_colourRepl ist) = id
1164consoleDecorate ist (AnnConst c) = let theme = idris_colourTheme ist
1165 in if constIsType c
1166 then colouriseType theme
1167 else colouriseData theme
1168consoleDecorate ist (AnnData _ _) = colouriseData (idris_colourTheme ist)
1169consoleDecorate ist (AnnType _ _) = colouriseType (idris_colourTheme ist)
1170consoleDecorate ist (AnnBoundName _ True) = colouriseImplicit (idris_colourTheme ist)
1171consoleDecorate ist (AnnBoundName _ False) = colouriseBound (idris_colourTheme ist)
1172consoleDecorate ist AnnKeyword = colouriseKeyword (idris_colourTheme ist)
1173consoleDecorate ist (AnnName n _ _ _) = let ctxt = tt_ctxt ist
1174 theme = idris_colourTheme ist
1175 in case () of
1176 _ | isDConName n ctxt -> colouriseData theme
1177 _ | isFnName n ctxt -> colouriseFun theme
1178 _ | isTConName n ctxt -> colouriseType theme
1179 _ | isPostulateName n ist -> colourisePostulate theme
1180 _ | otherwise -> id -- don't colourise unknown names
1181consoleDecorate ist (AnnFC _) = id
1182consoleDecorate ist (AnnTextFmt fmt) = Idris.Colours.colourise (colour fmt)
1183 where colour BoldText = IdrisColour Nothing True False True False
1184 colour UnderlineText = IdrisColour Nothing True True False False
1185 colour ItalicText = IdrisColour Nothing True False False True
1186consoleDecorate ist (AnnTerm _ _) = id
1188isPostulateName :: Name -> IState -> Bool
1189isPostulateName n ist = S.member n (idris_postulates ist)
1191-- | Pretty-print a high-level closed Idris term with no information about precedence/associativity
1192prettyImp :: PPOption -- ^^ pretty printing options
1193 -> PTerm -- ^^ the term to pretty-print
1194 -> Doc OutputAnnotation
1195prettyImp impl = pprintPTerm impl [] [] []
1197-- | Serialise something to base64 using its Binary instance.
1199-- | Do the right thing for rendering a term in an IState
1200prettyIst :: IState -> PTerm -> Doc OutputAnnotation
1201prettyIst ist = pprintPTerm (ppOptionIst ist) [] [] (idris_infixes ist)
1203-- | Pretty-print a high-level Idris term in some bindings context with infix info
1204pprintPTerm :: PPOption -- ^^ pretty printing options
1205 -> [(Name, Bool)] -- ^^ the currently-bound names and whether they are implicit
1206 -> [Name] -- ^^ names to always show in pi, even if not used
1207 -> [FixDecl] -- ^^ Fixity declarations
1208 -> PTerm -- ^^ the term to pretty-print
1209 -> Doc OutputAnnotation
1210pprintPTerm ppo bnd docArgs infixes = prettySe 10 bnd
1211 where
1212 prettySe :: Int -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation
1213 prettySe p bnd (PQuote r) =
1214 text "![" <> pretty r <> text "]"
1215 prettySe p bnd (PPatvar fc n) = pretty n
1216 prettySe p bnd e
1217 | Just str <- slist p bnd e = str
1218 | Just n <- snat p e = annotate (AnnData "Nat" "") (text (show n))
1219 prettySe p bnd (PRef fc n) = prettyName True (ppopt_impl ppo) bnd n
1220 prettySe p bnd (PLam n ty sc) =
1221 bracket p 2 . group . align . hang 2 $
1222 text "\\" <> bindingOf n False <+> text "=>" <$>
1223 prettySe 10 ((n, False):bnd) sc
1224 prettySe p bnd (PLet n ty v sc) =
1225 bracket p 2 $
1226 kwd "let" <+> bindingOf n False <+> text "=" </>
1227 prettySe 10 bnd v <+> kwd "in" </>
1228 prettySe 10 ((n, False):bnd) sc
1229 prettySe p bnd (PPi (Exp l s _) n ty sc)
1230 | n `elem` allNamesIn sc || ppopt_impl ppo || n `elem` docArgs =
1231 bracket p 2 . group $
1232 enclose lparen rparen (group . align $ bindingOf n False <+> colon <+> prettySe 10 bnd ty) <+>
1233 st <> text "->" <$> prettySe 10 ((n, False):bnd) sc
1234 | otherwise =
1235 bracket p 2 . group $
1236 group (prettySe 1 bnd ty <+> st) <> text "->" <$> group (prettySe 10 ((n, False):bnd) sc)
1237 where
1238 st =
1239 case s of
1240 Static -> text "[static]" <> space
1241 _ -> empty
1242 prettySe p bnd (PPi (Imp l s _) n ty sc)
1243 | ppopt_impl ppo =
1244 bracket p 2 $
1245 lbrace <> bindingOf n True <+> colon <+> prettySe 10 bnd ty <> rbrace <+>
1246 st <> text "->" </> prettySe 10 ((n, True):bnd) sc
1247 | otherwise = prettySe 10 ((n, True):bnd) sc
1248 where
1249 st =
1250 case s of
1251 Static -> text "[static]" <> space
1252 _ -> empty
1253 prettySe p bnd (PPi (Constraint _ _) n ty sc) =
1254 bracket p 2 $
1255 prettySe 10 bnd ty <+> text "=>" </> prettySe 10 ((n, True):bnd) sc
1256 prettySe p bnd (PPi (TacImp _ _ s) n ty sc) =
1257 bracket p 2 $
1258 lbrace <> kwd "tacimp" <+> pretty n <+> colon <+> prettySe 10 bnd ty <>
1259 rbrace <+> text "->" </> prettySe 10 ((n, True):bnd) sc
1260 prettySe p bnd (PApp _ (PRef _ f) args) -- normal names, no explicit args
1261 | UN nm <- basename f
1262 , not (ppopt_impl ppo) && null (getShowArgs args) =
1263 prettyName True (ppopt_impl ppo) bnd f
1264 prettySe p bnd (PAppBind _ (PRef _ f) [])
1265 | not (ppopt_impl ppo) = text "!" <> prettyName True (ppopt_impl ppo) bnd f
1266 prettySe p bnd (PApp _ (PRef _ op) args) -- infix operators
1267 | UN nm <- basename op
1268 , not (tnull nm) &&
1269 (not (ppopt_impl ppo)) && (not $ isAlpha (thead nm)) =
1270 case getShowArgs args of
1271 [] -> opName True
1272 [x] -> group (opName True <$> group (prettySe 0 bnd (getTm x)))
1273 [l,r] -> let precedence = fromMaybe 20 (fmap prec f)
1274 in bracket p precedence $ inFix (getTm l) (getTm r)
1275 (l@(PExp _ _ _ _) : r@(PExp _ _ _ _) : rest) ->
1276 bracket p 1 $
1277 enclose lparen rparen (inFix (getTm l) (getTm r)) <+>
1278 align (group (vsep (map (prettyArgS bnd) rest)))
1279 as -> opName True <+> align (vsep (map (prettyArgS bnd) as))
1280 where opName isPrefix = prettyName isPrefix (ppopt_impl ppo) bnd op
1281 f = getFixity (opStr op)
1282 left l = case f of
1283 Nothing -> prettySe (-1) bnd l
1284 Just (Infixl p') -> prettySe p' bnd l
1285 Just f' -> prettySe (prec f'-1) bnd l
1286 right r = case f of
1287 Nothing -> prettySe (-1) bnd r
1288 Just (Infixr p') -> prettySe p' bnd r
1289 Just f' -> prettySe (prec f'-1) bnd r
1290 inFix l r = align . group $
1291 (left l <+> opName False) <$> group (right r)
1292 prettySe p bnd (PApp _ hd@(PRef fc f) [tm]) -- symbols, like 'foo
1293 | PConstant (Idris.Core.TT.Str str) <- getTm tm,
1294 f == sUN "Symbol_" = annotate (AnnType ("'" ++ str) ("The symbol " ++ str)) $
1295 char '\'' <> prettySe 10 bnd (PRef fc (sUN str))
1296 prettySe p bnd (PApp _ f as) = -- Normal prefix applications
1297 let args = getShowArgs as
1298 fp = prettySe 1 bnd f
1299 in
1300 bracket p 1 . group $
1301 if ppopt_impl ppo
1302 then if null as
1303 then fp
1304 else fp <+> align (vsep (map (prettyArgS bnd) as))
1305 else if null args
1306 then fp
1307 else fp <+> align (vsep (map (prettyArgS bnd) args))
1308 prettySe p bnd (PCase _ scr opts) =
1309 kwd "case" <+> prettySe 10 bnd scr <+> kwd "of" <> prettyBody
1310 where
1311 prettyBody = foldr (<>) empty $ intersperse (text "|") $ map sc opts
1313 sc (l, r) = nest nestingSize $ prettySe 10 bnd l <+> text "=>" <+> prettySe 10 bnd r
1314 prettySe p bnd (PHidden tm) = text "." <> prettySe 0 bnd tm
1315 prettySe p bnd (PRefl _ _) = annName eqCon $ text "refl"
1316 prettySe p bnd (PResolveTC _) = text "resolvetc"
1317 prettySe p bnd (PTrue _ IsType) = annName unitTy $ text "()"
1318 prettySe p bnd (PTrue _ IsTerm) = annName unitCon $ text "()"
1319 prettySe p bnd (PTrue _ TypeOrTerm) = text "()"
1320 prettySe p bnd (PFalse _) = annName falseTy $ text "_|_"
1321 prettySe p bnd (PEq _ _ _ l r) =
1322 bracket p 2 . align . group $
1323 prettySe 10 bnd l <+> eq <$> group (prettySe 10 bnd r)
1324 where eq = annName eqTy (text "=")
1325 prettySe p bnd (PRewrite _ l r _) =
1326 bracket p 2 $
1327 text "rewrite" <+> prettySe 10 bnd l <+> text "in" <+> prettySe 10 bnd r
1328 prettySe p bnd (PTyped l r) =
1329 lparen <> prettySe 10 bnd l <+> colon <+> prettySe 10 bnd r <> rparen
1330 prettySe p bnd pair@(PPair _ pun _ _) -- flatten tuples to the right, like parser
1331 | Just elts <- pairElts pair = enclose (ann lparen) (ann rparen) .
1332 align . group . vsep . punctuate (ann comma) $
1333 map (prettySe 10 bnd) elts
1334 where ann = case pun of
1335 TypeOrTerm -> id
1336 IsType -> annName pairTy
1337 IsTerm -> annName pairCon
1338 prettySe p bnd (PDPair _ TypeOrTerm l t r) =
1339 lparen <> prettySe 10 bnd l <+> text "**" <+> prettySe 10 bnd r <> rparen
1340 prettySe p bnd (PDPair _ IsType (PRef _ n) t r) =
1341 annName sigmaTy lparen <>
1342 bindingOf n False <+>
1343 annName sigmaTy (text "**") <+>
1344 prettySe 10 ((n, False):bnd) r <>
1345 annName sigmaTy rparen
1346 prettySe p bnd (PDPair _ IsType l t r) =
1347 annName sigmaTy lparen <>
1348 prettySe 10 bnd l <+>
1349 annName sigmaTy (text "**") <+>
1350 prettySe 10 bnd r <>
1351 annName sigmaTy rparen
1352 prettySe p bnd (PDPair _ IsTerm l t r) =
1353 annName existsCon lparen <>
1354 prettySe 10 bnd l <+>
1355 annName existsCon (text "**") <+>
1356 prettySe 10 bnd r <>
1357 annName existsCon rparen
1358 prettySe p bnd (PAlternative a as) =
1359 lparen <> text "|" <> prettyAs <> text "|" <> rparen
1360 where
1361 prettyAs =
1362 foldr (\l -> \r -> l <+> text "," <+> r) empty $ map (prettySe 10 bnd) as
1363 prettySe p bnd PType = annotate (AnnType "Type" "The type of types") $ text "Type"
1364 prettySe p bnd (PConstant c) = annotate (AnnConst c) (text (show c))
1365 -- XXX: add pretty for tactics
1366 prettySe p bnd (PProof ts) =
1367 text "proof" <+> lbrace <> nest nestingSize (text . show $ ts) <> rbrace
1368 prettySe p bnd (PTactics ts) =
1369 text "tactics" <+> lbrace <> nest nestingSize (text . show $ ts) <> rbrace
1370 prettySe p bnd (PMetavar n) = text "?" <> pretty n
1371 prettySe p bnd (PReturn f) = kwd "return"
1372 prettySe p bnd PImpossible = kwd "impossible"
1373 prettySe p bnd Placeholder = text "_"
1374 prettySe p bnd (PDoBlock _) = text "do block pretty not implemented"
1375 prettySe p bnd (PCoerced t) = prettySe p bnd t
1376 prettySe p bnd (PElabError s) = pretty s
1377 -- Quasiquote pprinting ignores bound vars
1378 prettySe p bnd (PQuasiquote t Nothing) = text "`(" <> prettySe p [] t <> text ")"
1379 prettySe p bnd (PQuasiquote t (Just g)) = text "`(" <> prettySe p [] t <+> colon <+> prettySe p [] g <> text ")"
1380 prettySe p bnd (PUnquote t) = text "~" <> prettySe p bnd t
1382 prettySe p bnd _ = text "missing pretty-printer for term"
1384 prettyArgS bnd (PImp _ _ _ n tm) = prettyArgSi bnd (n, tm)
1385 prettyArgS bnd (PExp _ _ _ tm) = prettyArgSe bnd tm
1386 prettyArgS bnd (PConstraint _ _ _ tm) = prettyArgSc bnd tm
1387 prettyArgS bnd (PTacImplicit _ _ n _ tm) = prettyArgSti bnd (n, tm)
1389 prettyArgSe bnd arg = prettySe 0 bnd arg
1390 prettyArgSi bnd (n, val) = lbrace <> pretty n <+> text "=" <+> prettySe 10 bnd val <> rbrace
1391 prettyArgSc bnd val = lbrace <> lbrace <> prettySe 10 bnd val <> rbrace <> rbrace
1392 prettyArgSti bnd (n, val) = lbrace <> kwd "auto" <+> pretty n <+> text "=" <+> prettySe 10 bnd val <> rbrace
1394 annName :: Name -> Doc OutputAnnotation -> Doc OutputAnnotation
1395 annName n = annotate (AnnName n Nothing Nothing Nothing)
1397 opStr :: Name -> String
1398 opStr (NS n _) = opStr n
1399 opStr (UN n) = T.unpack n
1401 basename :: Name -> Name
1402 basename (NS n _) = basename n
1403 basename n = n
1405 slist' p bnd (PApp _ (PRef _ nil) _)
1406 | not (ppopt_impl ppo) && nsroot nil == sUN "Nil" = Just []
1407 slist' p bnd (PRef _ nil)
1408 | not (ppopt_impl ppo) && nsroot nil == sUN "Nil" = Just []
1409 slist' p bnd (PApp _ (PRef _ cons) args)
1410 | nsroot cons == sUN "::",
1411 (PExp {getTm=tl}):(PExp {getTm=hd}):imps <- reverse args,
1412 all isImp imps,
1413 Just tl' <- slist' p bnd tl
1414 = Just (hd:tl')
1415 where
1416 isImp (PImp {}) = True
1417 isImp _ = False
1418 slist' _ _ tm = Nothing
1420 slist p bnd e | Just es <- slist' p bnd e = Just $
1421 case es of [] -> annotate (AnnData "" "") $ text "[]"
1422 [x] -> enclose left right . group $
1423 prettySe p bnd x
1424 xs -> (enclose left right .
1425 align . group . vsep .
1426 punctuate comma .
1427 map (prettySe p bnd)) xs
1428 where left = (annotate (AnnData "" "") (text "["))
1429 right = (annotate (AnnData "" "") (text "]"))
1430 comma = (annotate (AnnData "" "") (text ","))
1431 slist _ _ _ = Nothing
1433 pairElts :: PTerm -> Maybe [PTerm]
1434 pairElts (PPair _ _ x y) | Just elts <- pairElts y = Just (x:elts)
1435 | otherwise = Just [x, y]
1436 pairElts _ = Nothing
1438 natns = "Prelude.Nat."
1440 snat p (PRef _ z)
1441 | show z == (natns++"Z") || show z == "Z" = Just 0
1442 snat p (PApp _ s [PExp {getTm=n}])
1443 | show s == (natns++"S") || show s == "S",
1444 Just n' <- snat p n
1445 = Just $ 1 + n'
1446 snat _ _ = Nothing
1448 bracket outer inner doc
1449 | inner > outer = lparen <> doc <> rparen
1450 | otherwise = doc
1452 kwd = annotate AnnKeyword . text
1454 fixities :: M.Map String Fixity
1455 fixities = M.fromList [(s, f) | (Fix f s) <- infixes]
1457 getFixity :: String -> Maybe Fixity
1458 getFixity = flip M.lookup fixities
1460prettyDocumentedIst :: IState -> (Name, PTerm, Maybe Docstring) -> Doc OutputAnnotation
1461prettyDocumentedIst ist (name, ty, docs) =
1462 prettyName True True [] name <+> colon <+> align (prettyIst ist ty) <$>
1463 fromMaybe empty (fmap (\d -> renderDocstring d <> line) docs)
1465-- | Pretty-printer helper for the binding site of a name
1466bindingOf :: Name -- ^^ the bound name
1467 -> Bool -- ^^ whether the name is implicit
1468 -> Doc OutputAnnotation
1469bindingOf n imp = annotate (AnnBoundName n imp) (text (show n))
1471-- | Pretty-printer helper for names that attaches the correct annotations
1472prettyName
1473 :: Bool -- ^^ whether the name should be parenthesised if it is an infix operator
1474 -> Bool -- ^^ whether to show namespaces
1475 -> [(Name, Bool)] -- ^^ the current bound variables and whether they are implicit
1476 -> Name -- ^^ the name to pprint
1477 -> Doc OutputAnnotation
1478prettyName infixParen showNS bnd n
1479 | Just imp <- lookup n bnd = annotate (AnnBoundName n imp) fullName
1480 | otherwise = annotate (AnnName n Nothing Nothing Nothing) fullName
1481 where fullName = text nameSpace <> parenthesise (text (baseName n))
1482 baseName (UN n) = T.unpack n
1483 baseName (NS n ns) = baseName n
1484 baseName (MN i s) = T.unpack s
1485 baseName n | n == falseTy = "_|_"
1486 baseName other = show other
1487 nameSpace = case n of
1488 (NS n' ns) -> if showNS then (concatMap (++ ".") . map T.unpack . reverse) ns else ""
1489 _ -> ""
1490 isInfix = case baseName n of
1491 "" -> False
1492 (c : _) -> not (isAlpha c)
1493 parenthesise = if isInfix && infixParen then enclose lparen rparen else id
1496showCImp :: PPOption -> PClause -> Doc OutputAnnotation
1497showCImp ppo (PClause _ n l ws r w)
1498 = prettyImp ppo l <+> showWs ws <+> text "=" <+> prettyImp ppo r
1499 <+> text "where" <+> text (show w)
1500 where
1501 showWs [] = empty
1502 showWs (x : xs) = text "|" <+> prettyImp ppo x <+> showWs xs
1503showCImp ppo (PWith _ n l ws r w)
1504 = prettyImp ppo l <+> showWs ws <+> text "with" <+> prettyImp ppo r
1505 <+> braces (text (show w))
1506 where
1507 showWs [] = empty
1508 showWs (x : xs) = text "|" <+> prettyImp ppo x <+> showWs xs
1511showDImp :: PPOption -> PData -> Doc OutputAnnotation
1512showDImp ppo (PDatadecl n ty cons)
1513 = text "data" <+> text (show n) <+> colon <+> prettyImp ppo ty <+> text "where" <$>
1514 (indent 2 $ vsep (map (\ (_, _, n, t, _, _) -> pipe <+> prettyName True False [] n <+> colon <+> prettyImp ppo t) cons))
1516showDecls :: PPOption -> [PDecl] -> Doc OutputAnnotation
1517showDecls o ds = vsep (map (showDeclImp o) ds)
1519showDeclImp _ (PFix _ f ops) = text (show f) <+> cat (punctuate (text ",") (map text ops))
1520showDeclImp o (PTy _ _ _ _ _ n t) = text "tydecl" <+> text (showCG n) <+> colon <+> prettyImp o t
1521showDeclImp o (PClauses _ _ n cs) = text "pat" <+> text (showCG n) <+> text "\t" <+>
1522 indent 2 (vsep (map (showCImp o) cs))
1523showDeclImp o (PData _ _ _ _ _ d) = showDImp o { ppopt_impl = True } d
1524showDeclImp o (PParams _ ns ps) = text "params" <+> braces (text (show ns) <> line <> showDecls o ps <> line)
1525showDeclImp o (PNamespace n ps) = text "namespace" <+> text n <> braces (line <> showDecls o ps <> line)
1526showDeclImp _ (PSyntax _ syn) = text "syntax" <+> text (show syn)
1527showDeclImp o (PClass _ _ _ cs n ps _ ds)
1528 = text "class" <+> text (show cs) <+> text (show n) <+> text (show ps) <> line <> showDecls o ds
1529showDeclImp o (PInstance _ _ cs n _ t _ ds)
1530 = text "instance" <+> text (show cs) <+> text (show n) <+> prettyImp o t <> line <> showDecls o ds
1531showDeclImp _ _ = text "..."
1532-- showDeclImp (PImport o) = "import " ++ o
1534instance Show (Doc OutputAnnotation) where
1535 show = flip (displayS . renderCompact) ""
1537getImps :: [PArg] -> [(Name, PTerm)]
1538getImps [] = []
1539getImps (PImp _ _ _ n tm : xs) = (n, tm) : getImps xs
1540getImps (_ : xs) = getImps xs
1542getExps :: [PArg] -> [PTerm]
1543getExps [] = []
1544getExps (PExp _ _ _ tm : xs) = tm : getExps xs
1545getExps (_ : xs) = getExps xs
1547getShowArgs :: [PArg] -> [PArg]
1548getShowArgs [] = []
1549getShowArgs (e@(PExp _ _ _ tm) : xs) = e : getShowArgs xs
1550getShowArgs (e : xs) | AlwaysShow `elem` argopts e = e : getShowArgs xs
1551getShowArgs (_ : xs) = getShowArgs xs
1553getConsts :: [PArg] -> [PTerm]
1554getConsts [] = []
1555getConsts (PConstraint _ _ _ tm : xs) = tm : getConsts xs
1556getConsts (_ : xs) = getConsts xs
1558getAll :: [PArg] -> [PTerm]
1559getAll = map getTm
1562-- | Show Idris name
1563showName :: Maybe IState -- ^^ the Idris state, for information about names and colours
1564 -> [(Name, Bool)] -- ^^ the bound variables and whether they're implicit
1565 -> PPOption -- ^^ pretty printing options
1566 -> Bool -- ^^ whether to colourise
1567 -> Name -- ^^ the term to show
1568 -> String
1569showName ist bnd ppo colour n = case ist of
1570 Just i -> if colour then colourise n (idris_colourTheme i) else showbasic n
1571 Nothing -> showbasic n
1572 where name = if ppopt_impl ppo then show n else showbasic n
1573 showbasic n@(UN _) = showCG n
1574 showbasic (MN i s) = str s
1575 showbasic (NS n s) = showSep "." (map str (reverse s)) ++ "." ++ showbasic n
1576 showbasic (SN s) = show s
1577 fst3 (x, _, _) = x
1578 colourise n t = let ctxt' = fmap tt_ctxt ist in
1579 case ctxt' of
1580 Nothing -> name
1581 Just ctxt | Just impl <- lookup n bnd -> if impl then colouriseImplicit t name
1582 else colouriseBound t name
1583 | isDConName n ctxt -> colouriseData t name
1584 | isFnName n ctxt -> colouriseFun t name
1585 | isTConName n ctxt -> colouriseType t name
1586 -- The assumption is that if a name is not bound and does not exist in the
1587 -- global context, then we're somewhere in which implicit info has been lost
1588 -- (like error messages). Thus, unknown vars are colourised as implicits.
1589 | otherwise -> colouriseImplicit t name
1591showTm :: IState -- ^^ the Idris state, for information about identifiers and colours
1592 -> PTerm -- ^^ the term to show
1593 -> String
1594showTm ist = displayDecorated (consoleDecorate ist) .
1595 renderPretty 0.8 100000 .
1596 prettyImp (ppOptionIst ist)
1598-- | Show a term with implicits, no colours
1599showTmImpls :: PTerm -> String
1600showTmImpls = flip (displayS . renderCompact . prettyImp verbosePPOption) ""
1604instance Sized PTerm where
1605 size (PQuote rawTerm) = size rawTerm
1606 size (PRef fc name) = size name
1607 size (PLam name ty bdy) = 1 + size ty + size bdy
1608 size (PPi plicity name ty bdy) = 1 + size ty + size bdy
1609 size (PLet name ty def bdy) = 1 + size ty + size def + size bdy
1610 size (PTyped trm ty) = 1 + size trm + size ty
1611 size (PApp fc name args) = 1 + size args
1612 size (PAppBind fc name args) = 1 + size args
1613 size (PCase fc trm bdy) = 1 + size trm + size bdy
1614 size (PTrue fc _) = 1
1615 size (PFalse fc) = 1
1616 size (PRefl fc _) = 1
1617 size (PResolveTC fc) = 1
1618 size (PEq fc _ _ left right) = 1 + size left + size right
1619 size (PRewrite fc left right _) = 1 + size left + size right
1620 size (PPair fc _ left right) = 1 + size left + size right
1621 size (PDPair fs _ left ty right) = 1 + size left + size ty + size right
1622 size (PAlternative a alts) = 1 + size alts
1623 size (PHidden hidden) = size hidden
1624 size (PUnifyLog tm) = size tm
1625 size (PDisamb _ tm) = size tm
1626 size (PNoImplicits tm) = size tm
1627 size PType = 1
1628 size (PConstant const) = 1 + size const
1629 size Placeholder = 1
1630 size (PDoBlock dos) = 1 + size dos
1631 size (PIdiom fc term) = 1 + size term
1632 size (PReturn fc) = 1
1633 size (PMetavar name) = 1
1634 size (PProof tactics) = size tactics
1635 size (PElabError err) = size err
1636 size PImpossible = 1
1638getPArity :: PTerm -> Int
1639getPArity (PPi _ _ _ sc) = 1 + getPArity sc
1640getPArity _ = 0
1642-- Return all names, free or globally bound, in the given term.
1644allNamesIn :: PTerm -> [Name]
1645allNamesIn tm = nub $ ni [] tm
1646 where -- TODO THINK added niTacImp, but is it right?
1647 ni env (PRef _ n)
1648 | not (n `elem` env) = [n]
1649 ni env (PPatvar _ n) = [n]
1650 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
1651 ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
1652 ni env (PCase _ c os) = ni env c ++ concatMap (ni env) (map snd os)
1653 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc
1654 ni env (PPi p n ty sc) = niTacImp env p ++ ni env ty ++ ni (n:env) sc
1655 ni env (PHidden tm) = ni env tm
1656 ni env (PEq _ _ _ l r) = ni env l ++ ni env r
1657 ni env (PRewrite _ l r _) = ni env l ++ ni env r
1658 ni env (PTyped l r) = ni env l ++ ni env r
1659 ni env (PPair _ _ l r) = ni env l ++ ni env r
1660 ni env (PDPair _ _ (PRef _ n) t r) = ni env t ++ ni (n:env) r
1661 ni env (PDPair _ _ l t r) = ni env l ++ ni env t ++ ni env r
1662 ni env (PAlternative a ls) = concatMap (ni env) ls
1663 ni env (PUnifyLog tm) = ni env tm
1664 ni env (PDisamb _ tm) = ni env tm
1665 ni env (PNoImplicits tm) = ni env tm
1666 ni env _ = []
1668 niTacImp env (TacImp _ _ scr) = ni env scr
1669 niTacImp _ _ = []
1671-- Return all names defined in binders in the given term
1672boundNamesIn :: PTerm -> [Name]
1673boundNamesIn tm = nub $ ni tm
1674 where -- TODO THINK Added niTacImp, but is it right?
1675 ni (PApp _ f as) = ni f ++ concatMap (ni) (map getTm as)
1676 ni (PAppBind _ f as) = ni f ++ concatMap (ni) (map getTm as)
1677 ni (PCase _ c os) = ni c ++ concatMap (ni) (map snd os)
1678 ni (PLam n ty sc) = n : (ni ty ++ ni sc)
1679 ni (PLet n ty val sc) = n : (ni ty ++ ni val ++ ni sc)
1680 ni (PPi p n ty sc) = niTacImp p ++ (n : (ni ty ++ ni sc))
1681 ni (PEq _ _ _ l r) = ni l ++ ni r
1682 ni (PRewrite _ l r _) = ni l ++ ni r
1683 ni (PTyped l r) = ni l ++ ni r
1684 ni (PPair _ _ l r) = ni l ++ ni r
1685 ni (PDPair _ _ (PRef _ n) t r) = ni t ++ ni r
1686 ni (PDPair _ _ l t r) = ni l ++ ni t ++ ni r
1687 ni (PAlternative a as) = concatMap (ni) as
1688 ni (PHidden tm) = ni tm
1689 ni (PUnifyLog tm) = ni tm
1690 ni (PDisamb _ tm) = ni tm
1691 ni (PNoImplicits tm) = ni tm
1692 ni _ = []
1694 niTacImp (TacImp _ _ scr) = ni scr
1695 niTacImp _ = []
1697-- Return names which are valid implicits in the given term (type).
1698implicitNamesIn :: [Name] -> IState -> PTerm -> [Name]
1699implicitNamesIn uvars ist tm = nub $ ni [] tm
1700 where
1701 ni env (PRef _ n)
1702 | not (n `elem` env)
1703 = case lookupTy n (tt_ctxt ist) of
1704 [] -> [n]
1705 _ -> if n `elem` uvars then [n] else []
1706 ni env (PApp _ f@(PRef _ n) as)
1707 | n `elem` uvars = ni env f ++ concatMap (ni env) (map getTm as)
1708 | otherwise = concatMap (ni env) (map getTm as)
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 ++
1712 -- names in 'os', not counting the names bound in the cases
1713 (nub (concatMap (ni env) (map snd os))
1714 \\ nub (concatMap (ni env) (map fst os)))
1715 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc
1716 ni env (PPi p n ty sc) = niTacImp env p ++ ni env ty ++ ni (n:env) sc
1717 ni env (PEq _ _ _ l r) = ni env l ++ ni env r
1718 ni env (PRewrite _ l r _) = ni env l ++ ni env r
1719 ni env (PTyped l r) = ni env l ++ ni env r
1720 ni env (PPair _ _ l r) = ni env l ++ ni env r
1721 ni env (PDPair _ _ (PRef _ n) t r) = ni env t ++ ni (n:env) r
1722 ni env (PDPair _ _ l t r) = ni env l ++ ni env t ++ ni env r
1723 ni env (PAlternative a as) = concatMap (ni env) as
1724 ni env (PHidden tm) = ni env tm
1725 ni env (PUnifyLog tm) = ni env tm
1726 ni env (PDisamb _ tm) = ni env tm
1727 ni env (PNoImplicits tm) = ni env tm
1728 ni env _ = []
1730 niTacImp env (TacImp _ _ scr) = ni env scr
1731 niTacImp _ _ = []
1733-- Return names which are free in the given term.
1734namesIn :: [(Name, PTerm)] -> IState -> PTerm -> [Name]
1735namesIn uvars ist tm = nub $ ni [] tm
1736 where
1737 ni env (PRef _ n)
1738 | not (n `elem` env)
1739 = case lookupTy n (tt_ctxt ist) of
1740 [] -> [n]
1741 _ -> if n `elem` (map fst uvars) then [n] else []
1742 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
1743 ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
1744 ni env (PCase _ c os) = ni env c ++
1745 -- names in 'os', not counting the names bound in the cases
1746 (nub (concatMap (ni env) (map snd os))
1747 \\ nub (concatMap (ni env) (map fst os)))
1748 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc
1749 ni env (PPi p n ty sc) = niTacImp env p ++ ni env ty ++ ni (n:env) sc
1750 ni env (PEq _ _ _ l r) = ni env l ++ ni env r
1751 ni env (PRewrite _ l r _) = ni env l ++ ni env r
1752 ni env (PTyped l r) = ni env l ++ ni env r
1753 ni env (PPair _ _ l r) = ni env l ++ ni env r
1754 ni env (PDPair _ _ (PRef _ n) t r) = ni env t ++ ni (n:env) r
1755 ni env (PDPair _ _ l t r) = ni env l ++ ni env t ++ ni env r
1756 ni env (PAlternative a as) = concatMap (ni env) as
1757 ni env (PHidden tm) = ni env tm
1758 ni env (PUnifyLog tm) = ni env tm
1759 ni env (PDisamb _ tm) = ni env tm
1760 ni env (PNoImplicits tm) = ni env tm
1761 ni env _ = []
1763 niTacImp env (TacImp _ _ scr) = ni env scr
1764 niTacImp _ _ = []
1766-- Return which of the given names are used in the given term.
1768usedNamesIn :: [Name] -> IState -> PTerm -> [Name]
1769usedNamesIn vars ist tm = nub $ ni [] tm
1770 where -- TODO THINK added niTacImp, but is it right?
1771 ni env (PRef _ n)
1772 | n `elem` vars && not (n `elem` env)
1773 = case lookupDefExact n (tt_ctxt ist) of
1774 Nothing -> [n]
1775 _ -> []
1776 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
1777 ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
1778 ni env (PCase _ c os) = ni env c ++ concatMap (ni env) (map snd os)
1779 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc
1780 ni env (PPi p n ty sc) = niTacImp env p ++ ni env ty ++ ni (n:env) sc
1781 ni env (PEq _ _ _ l r) = ni env l ++ ni env r
1782 ni env (PRewrite _ l r _) = ni env l ++ ni env r
1783 ni env (PTyped l r) = ni env l ++ ni env r
1784 ni env (PPair _ _ l r) = ni env l ++ ni env r
1785 ni env (PDPair _ _ (PRef _ n) t r) = ni env t ++ ni (n:env) r
1786 ni env (PDPair _ _ l t r) = ni env l ++ ni env t ++ ni env r
1787 ni env (PAlternative a as) = concatMap (ni env) as
1788 ni env (PHidden tm) = ni env tm
1789 ni env (PUnifyLog tm) = ni env tm
1790 ni env (PDisamb _ tm) = ni env tm
1791 ni env (PNoImplicits tm) = ni env tm
1792 ni env _ = []
1794 niTacImp env (TacImp _ _ scr) = ni env scr
1795 niTacImp _ _ = []
1797-- Return the list of inaccessible (= dotted) positions for a name.
1798getErasureInfo :: IState -> Name -> [Int]
1799getErasureInfo ist n =
1800 case lookupCtxtExact n (idris_optimisation ist) of
1801 Just (Optimise inacc detagg) -> map fst inacc
1802 Nothing -> []