1{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, DeriveFunctor,
2 DeriveDataTypeable, TypeSynonymInstances, PatternGuards #-}
4module Idris.AbsSyntaxTree where
7import Idris.Core.Evaluate
8import Idris.Core.Elaborate hiding (Tactic(..))
9import Idris.Core.Typecheck
10import Idris.Docstrings
12import IRTS.CodegenCommon
14import Util.DynamicLinker
18import System.Console.Haskeline
21import Prelude hiding ((<$>))
23import Control.Applicative ((<|>))
25import Control.Monad.Trans.State.Strict
26import Control.Monad.Trans.Except
27import qualified Control.Monad.Trans.Class as Trans (lift)
29import Data.Data (Data)
30import Data.Function (on)
31import Data.Generics.Uniplate.Data (universe)
32import Data.List hiding (group)
34import qualified Data.Map.Strict as M
35import qualified Data.Text as T
37import qualified Data.Set as S
38import Data.Word (Word)
39import Data.Maybe (fromMaybe, mapMaybe, maybeToList)
40import Data.Traversable (Traversable)
42import Data.Foldable (Foldable)
46import Text.PrettyPrint.Annotated.Leijen
48data ElabWhat = ETypes | EDefns | EAll
51-- Data to pass to recursively called elaborators; e.g. for where blocks,
52-- paramaterised declarations, etc.
54-- rec_elabDecl is used to pass the top level elaborator into other elaborators,
55-- so that we can have mutually recursive elaborators in separate modules without
56-- having to muck about with cyclic modules.
57data ElabInfo = EInfo { params :: [(Name, PTerm)],
58 inblock :: Ctxt [Name], -- names in the block, and their params
59 liftname :: Name -> Name,
60 namespace :: Maybe [String],
62 rec_elabDecl :: ElabWhat -> ElabInfo -> PDecl ->
66toplevel = EInfo [] emptyContext id Nothing Nothing (\_ _ _ -> fail "Not implemented")
68eInfoNames :: ElabInfo -> [Name]
69eInfoNames info = map fst (params info) ++ M.keys (inblock info)
71data IOption = IOption { opt_logLevel :: Int,
73 opt_typeintype :: Bool,
75 opt_showimp :: Bool, -- ^^ show implicits
76 opt_errContext :: Bool,
81 opt_codegen :: Codegen,
82 opt_outputTy :: OutputType,
83 opt_ibcsubdir :: FilePath,
84 opt_importdirs :: [FilePath],
87 opt_cmdline :: [Opt], -- remember whole command line
89 opt_autoSolve :: Bool, -- ^ automatically apply "solve" tactic in prover
90 opt_autoImport :: [FilePath], -- ^ e.g. Builtins+Prelude
91 opt_optimise :: [Optimisation],
92 opt_printdepth :: Maybe Int,
93 opt_evaltypes :: Bool -- ^ normalise types in :t
97defaultOpts = IOption { opt_logLevel = 0
98 , opt_typecase = False
99 , opt_typeintype = False
100 , opt_coverage = True
101 , opt_showimp = False
102 , opt_errContext = False
105 , opt_nobanner = False
107 , opt_codegen = Via "c"
108 , opt_outputTy = Executable
110 , opt_importdirs = []
114 , opt_origerr = False
115 , opt_autoSolve = True
116 , opt_autoImport = []
117 , opt_optimise = defaultOptimise
118 , opt_printdepth = Just 5000
119 , opt_evaltypes = True
122data PPOption = PPOption {
123 ppopt_impl :: Bool -- ^^ whether to show implicits
124 , ppopt_depth :: Maybe Int
127data Optimisation = PETransform -- partial eval and associated transforms
130defaultOptimise = [PETransform]
132-- | Pretty printing options with default verbosity.
133defaultPPOption :: PPOption
134defaultPPOption = PPOption { ppopt_impl = False , ppopt_depth = Just 200 }
136-- | Pretty printing options with the most verbosity.
137verbosePPOption :: PPOption
138verbosePPOption = PPOption { ppopt_impl = True, ppopt_depth = Just 200 }
140-- | Get pretty printing options from the big options record.
141ppOption :: IOption -> PPOption
142ppOption opt = PPOption {
143 ppopt_impl = opt_showimp opt,
144 ppopt_depth = opt_printdepth opt
147-- | Get pretty printing options from an idris state record.
148ppOptionIst :: IState -> PPOption
149ppOptionIst = ppOption . idris_options
151data LanguageExt = TypeProviders | ErrorReflection deriving (Show, Eq, Read, Ord)
153-- | The output mode in use
154data OutputMode = RawOutput Handle -- ^ Print user output directly to the handle
155 | IdeMode Integer Handle -- ^ Send IDE output for some request ID to the handle
158-- | How wide is the console?
159data ConsoleWidth = InfinitelyWide -- ^ Have pretty-printer assume that lines should not be broken
160 | ColsWide Int -- ^ Manually specified - must be positive
161 | AutomaticWidth -- ^ Attempt to determine width, or 80 otherwise
165-- | The global state used in the Idris monad
166data IState = IState {
167 tt_ctxt :: Context, -- ^ All the currently defined names and their terms
168 idris_constraints :: S.Set ConstraintFC,
169 -- ^ A list of universe constraints and their corresponding source locations
170 idris_infixes :: [FixDecl], -- ^ Currently defined infix operators
171 idris_implicits :: Ctxt [PArg],
172 idris_statics :: Ctxt [Bool],
173 idris_classes :: Ctxt ClassInfo,
174 idris_dsls :: Ctxt DSL,
175 idris_optimisation :: Ctxt OptInfo,
176 idris_datatypes :: Ctxt TypeInfo,
177 idris_namehints :: Ctxt [Name],
178 idris_patdefs :: Ctxt ([([Name], Term, Term)], [PTerm]), -- not exported
179 -- ^ list of lhs/rhs, and a list of missing clauses
180 idris_flags :: Ctxt [FnOpt],
181 idris_callgraph :: Ctxt CGInfo, -- name, args used in each pos
182 idris_calledgraph :: Ctxt [Name],
183 idris_docstrings :: Ctxt (Docstring DocTerm, [(Name, Docstring DocTerm)]),
184 idris_moduledocs :: Ctxt (Docstring DocTerm),
185 -- ^ module documentation is saved in a special MN so the context
186 -- mechanism can be used for disambiguation
187 idris_tyinfodata :: Ctxt TIData,
188 idris_fninfo :: Ctxt FnInfo,
189 idris_transforms :: Ctxt [(Term, Term)],
190 idris_autohints :: Ctxt [Name],
191 idris_totcheck :: [(FC, Name)], -- names to check totality on
192 idris_defertotcheck :: [(FC, Name)], -- names to check at the end
193 idris_totcheckfail :: [(FC, String)],
194 idris_options :: IOption,
196 idris_lineapps :: [((FilePath, Int), PTerm)],
197 -- ^ Full application LHS on source line
198 idris_metavars :: [(Name, (Maybe Name, Int, Bool))],
199 -- ^ The currently defined but not proven metavariables. The Int
200 -- is the number of vars to display as a context, the Maybe Name
201 -- is its top-level function, and the Bool is whether :p is
203 idris_coercions :: [Name],
204 idris_errRev :: [(Term, Term)],
205 syntax_rules :: SyntaxRules,
206 syntax_keywords :: [String],
207 imported :: [FilePath], -- ^ The imported modules
208 idris_scprims :: [(Name, (Int, PrimFn))],
209 idris_objs :: [(Codegen, FilePath)],
210 idris_libs :: [(Codegen, String)],
211 idris_cgflags :: [(Codegen, String)],
212 idris_hdrs :: [(Codegen, String)],
213 idris_imported :: [(FilePath, Bool)], -- ^ Imported ibc file names, whether public
214 proof_list :: [(Name, (Bool, [String]))],
216 parserWarnings :: [(FC, Err)],
217 lastParse :: Maybe Name,
218 indent_stack :: [Int],
219 brace_stack :: [Maybe Int],
220 lastTokenSpan :: Maybe FC, -- ^ What was the span of the latest token parsed?
221 idris_parsedSpan :: Maybe FC,
222 hide_list :: [(Name, Maybe Accessibility)],
223 default_access :: Accessibility,
224 default_total :: Bool,
225 ibc_write :: [IBCWrite],
226 compiled_so :: Maybe String,
227 idris_dynamic_libs :: [DynamicLib],
228 idris_language_extensions :: [LanguageExt],
229 idris_outputmode :: OutputMode,
230 idris_colourRepl :: Bool,
231 idris_colourTheme :: ColourTheme,
232 idris_errorhandlers :: [Name], -- ^ Global error handlers
233 idris_nameIdx :: (Int, Ctxt (Int, Name)),
234 idris_function_errorhandlers :: Ctxt (M.Map Name (S.Set Name)), -- ^ Specific error handlers
235 module_aliases :: M.Map [T.Text] [T.Text],
236 idris_consolewidth :: ConsoleWidth, -- ^ How many chars wide is the console?
237 idris_postulates :: S.Set Name,
238 idris_externs :: S.Set (Name, Int),
239 idris_erasureUsed :: [(Name, Int)], -- ^ Function/constructor name, argument position is used
240 idris_whocalls :: Maybe (M.Map Name [Name]),
241 idris_callswho :: Maybe (M.Map Name [Name]),
242 idris_repl_defs :: [Name], -- ^ List of names that were defined in the repl, and can be re-/un-defined
243 elab_stack :: [(Name, Bool)], -- ^ Stack of names currently being elaborated, Bool set if it's an instance
244 -- (instances appear twice; also as a funtion name)
245 idris_symbols :: M.Map Name Name, -- ^ Symbol table (preserves sharing of names)
246 idris_exports :: [Name], -- ^ Functions with ExportList
247 idris_highlightedRegions :: [(FC, OutputAnnotation)], -- ^ Highlighting information to output
248 idris_parserHighlights :: [(FC, OutputAnnotation)] -- ^ Highlighting information from the parser
251-- Required for parsers library, and therefore trifecta
252instance Show IState where
253 show = const "{internal state}"
255data SizeChange = Smaller | Same | Bigger | Unknown
258deriving instance Binary SizeChange
259deriving instance NFData SizeChange
262type SCGEntry = (Name, [Maybe (Int, SizeChange)])
263type UsageReason = (Name, Int) -- fn_name, its_arg_number
265data CGInfo = CGInfo { argsdef :: [Name],
266 calls :: [(Name, [[Name]])],
269 usedpos :: [(Int, [UsageReason])] }
272deriving instance Binary CGInfo
273deriving instance NFData CGInfo
276primDefs = [sUN "unsafePerformPrimIO",
277 sUN "mkLazyForeignPrim",
281-- information that needs writing for the current module's .ibc file
282data IBCWrite = IBCFix FixDecl
286 | IBCInstance Bool Bool Name Name
293 | IBCImport (Bool, FilePath) -- True = import public
294 | IBCImportDir FilePath
295 | IBCObj Codegen FilePath
296 | IBCLib Codegen String
297 | IBCCGFlag Codegen String
299 | IBCHeader Codegen String
300 | IBCAccess Name Accessibility
301 | IBCMetaInformation Name MetaInformation
302 | IBCTotal Name Totality
303 | IBCFlags Name [FnOpt]
304 | IBCFnInfo Name FnInfo
305 | IBCTrans Name (Term, Term)
306 | IBCErrRev (Term, Term)
310 | IBCDef Name -- i.e. main context
311 | IBCNameHint (Name, Name)
312 | IBCLineApp FilePath Int PTerm
313 | IBCErrorHandler Name
314 | IBCFunctionErrorHandler Name Name Name
316 | IBCExtern (Name, Int)
317 | IBCTotCheckErr FC String
319 | IBCModDocs Name -- ^ The name is the special name used to track module docs
320 | IBCUsage (Name, Int)
322 | IBCAutoHint Name Name
325-- | The initial state for the compiler
327idrisInit = IState initContext S.empty []
328 emptyContext emptyContext emptyContext emptyContext
329 emptyContext emptyContext emptyContext emptyContext
330 emptyContext emptyContext emptyContext emptyContext
331 emptyContext emptyContext emptyContext emptyContext
333 [] [] [] defaultOpts 6 [] [] [] [] emptySyntaxRules [] [] [] [] [] [] []
334 [] [] Nothing [] Nothing [] [] Nothing Nothing [] Hidden False [] Nothing [] []
335 (RawOutput stdout) True defaultTheme [] (0, emptyContext) emptyContext M.empty
336 AutomaticWidth S.empty S.empty [] Nothing Nothing [] [] M.empty [] [] []
338-- | The monad for the main REPL - reading and processing files and updating
339-- global state (hence the IO inner monad).
340--type Idris = WriterT [Either String (IO ())] (State IState a))
341type Idris = StateT IState (ExceptT Err IO)
343catchError :: Idris a -> (Err -> Idris a) -> Idris a
344catchError = liftCatch catchE
346throwError :: Err -> Idris a
347throwError = Trans.lift . throwE
349-- Commands in the REPL
351data Codegen = Via String
360deriving instance NFData Codegen
363data HowMuchDocs = FullDocs | OverviewDocs
369 | NewDefn [PDecl] -- ^ Each 'PDecl' should be either a type declaration (at most one) or a clause defining the same name.
373 | DocStr (Either Name Const) HowMuchDocs
376 | Load FilePath (Maybe Int) -- up to maximum line number
377 | ChangeDirectory FilePath
380 | Compile Codegen String
384 | Prove Bool Name -- ^ If false, use prover, if true, use elab shell
385 | AddProof (Maybe Name)
396 | DynamicLink FilePath
399 | Search [String] PTerm
400 | CaseSplitAt Bool Int Name
401 | AddClauseFrom Bool Int Name
402 | AddProofClauseFrom Bool Int Name
403 | AddMissing Bool Int Name
404 | MakeWith Bool Int Name
405 | MakeLemma Bool Int Name
406 | DoProofSearch Bool Bool Int Name [Name]
407 -- ^ the first bool is whether to update,
408 -- the second is whether to search recursively (i.e. for the arguments)
412 | SetColour ColourType IdrisColour
416 | SetConsoleWidth ConsoleWidth
417 | SetPrinterDepth (Maybe Int)
418 | Apropos [String] String
422 | MakeDoc String -- IdrisDoc
425 | PPrint OutputFmt Int PTerm
427 -- Debugging commands
429 | DebugUnify PTerm PTerm
431data OutputFmt = HTMLOutput | LaTeXOutput
433data Opt = Filename String
445 | NoBuiltins -- only for the really primitive stuff!
461 | Port String -- REPL TCP port
469 | PkgMkDoc String -- IdrisDoc
479 | OutputTy OutputType
480 | Extension LanguageExt
481 | InterpretScript String
483 | TargetTriple String
486 | AddOpt Optimisation
487 | RemoveOpt Optimisation
490 | AutoWidth -- ^ Automatically adjust terminal width
491 | AutoSolve -- ^ Automatically issue "solve" tactic in interactive prover
492 | UseConsoleWidth ConsoleWidth
496data ElabShellCmd = EQED | EAbandon | EUndo | EProofState | EProofTerm
497 | EEval PTerm | ECheck PTerm | ESearch PTerm
498 | EDocStr (Either Name Const)
501-- Parsed declarations
503data Fixity = Infixl { prec :: Int }
504 | Infixr { prec :: Int }
505 | InfixN { prec :: Int }
506 | PrefixN { prec :: Int }
509deriving instance Binary Fixity
510deriving instance NFData Fixity
513instance Show Fixity where
514 show (Infixl i) = "infixl " ++ show i
515 show (Infixr i) = "infixr " ++ show i
516 show (InfixN i) = "infix " ++ show i
517 show (PrefixN i) = "prefix " ++ show i
519data FixDecl = Fix Fixity String
522instance Show FixDecl where
523 show (Fix f s) = show f ++ " " ++ s
526deriving instance Binary FixDecl
527deriving instance NFData FixDecl
530instance Ord FixDecl where
531 compare (Fix x _) (Fix y _) = compare (prec x) (prec y)
534data Static = Static | Dynamic
535 deriving (Show, Eq, Data, Typeable)
537deriving instance Binary Static
538deriving instance NFData Static
541-- Mark bindings with their explicitness, and laziness
542data Plicity = Imp { pargopts :: [ArgOpt],
545 pscoped :: Maybe ImplicitInfo -- Nothing, if top level
547 | Exp { pargopts :: [ArgOpt],
549 pparam :: Bool } -- this is a param (rather than index)
550 | Constraint { pargopts :: [ArgOpt],
552 | TacImp { pargopts :: [ArgOpt],
555 deriving (Show, Eq, Data, Typeable)
558deriving instance Binary Plicity
559deriving instance NFData Plicity
562is_scoped :: Plicity -> Maybe ImplicitInfo
563is_scoped (Imp _ _ _ s) = s
566impl = Imp [] Dynamic False Nothing
567forall_imp = Imp [] Dynamic False (Just (Impl False))
568forall_constraint = Imp [] Dynamic False (Just (Impl True))
569expl = Exp [] Dynamic False
570expl_param = Exp [] Dynamic True
571constraint = Constraint [] Static
572tacimpl t = TacImp [] Dynamic t
574data FnOpt = Inlinable -- always evaluate when simplifying
575 | TotalFn | PartialFn | CoveringFn
576 | Coinductive | AssertTotal
577 | Dictionary -- type class dictionary, eval only when
578 -- a function argument, and further evaluation resutls
579 | Implicit -- implicit coercion
580 | NoImplicit -- do not apply implicit coercions
581 | CExport String -- export, with a C name
582 | ErrorHandler -- ^^ an error handler for use with the ErrorReflection extension
583 | ErrorReverse -- ^^ attempt to reverse normalise before showing in error
584 | Reflection -- a reflecting function, compile-time only
585 | Specialise [(Name, Maybe Int)] -- specialise it, freeze these names
586 | Constructor -- Data constructor type
587 | AutoHint -- use in auto implicit search
588 | PEGenerated -- generated by partial evaluator
591deriving instance Binary FnOpt
592deriving instance NFData FnOpt
597inlinable :: FnOpts -> Bool
598inlinable = elem Inlinable
600dictionary :: FnOpts -> Bool
601dictionary = elem Dictionary
604-- | Type provider - what to provide
605data ProvideWhat' t = ProvTerm t t -- ^ the first is the goal type, the second is the term
606 | ProvPostulate t -- ^ goal type must be Type, so only term
607 deriving (Show, Eq, Functor)
609type ProvideWhat = ProvideWhat' PTerm
611-- | Top-level declarations such as compiler directives, definitions,
612-- datatypes and typeclasses.
614 = PFix FC Fixity [String] -- ^ Fixity declaration
615 | PTy (Docstring (Either Err PTerm)) [(Name, Docstring (Either Err PTerm))] SyntaxInfo FC FnOpts Name FC t -- ^ Type declaration (last FC is precise name location)
616 | PPostulate Bool -- external def if true
617 (Docstring (Either Err PTerm)) SyntaxInfo FC FC FnOpts Name t -- ^ Postulate, second FC is precise name location
618 | PClauses FC FnOpts Name [PClause' t] -- ^ Pattern clause
619 | PCAF FC Name t -- ^ Top level constant
620 | PData (Docstring (Either Err PTerm)) [(Name, Docstring (Either Err PTerm))] SyntaxInfo FC DataOpts (PData' t) -- ^ Data declaration.
621 | PParams FC [(Name, t)] [PDecl' t] -- ^ Params block
622 | PNamespace String FC [PDecl' t]
623 -- ^ New namespace, where FC is accurate location of the
624 -- namespace in the file
625 | PRecord (Docstring (Either Err PTerm)) SyntaxInfo FC DataOpts
627 FC -- Record name precise location
628 [(Name, FC, Plicity, t)] -- Parameters, where FC is precise name span
629 [(Name, Docstring (Either Err PTerm))] -- Param Docs
630 [((Maybe (Name, FC)), Plicity, t, Maybe (Docstring (Either Err PTerm)))] -- Fields
631 (Maybe (Name, FC)) -- Optional constructor name and location
632 (Docstring (Either Err PTerm)) -- Constructor doc
633 SyntaxInfo -- Constructor SyntaxInfo
634 -- ^ Record declaration
635 | PClass (Docstring (Either Err PTerm)) SyntaxInfo FC
636 [(Name, t)] -- constraints
638 FC -- accurate location of class name
639 [(Name, FC, t)] -- parameters and precise locations
640 [(Name, Docstring (Either Err PTerm))] -- parameter docstrings
641 [(Name, FC)] -- determining parameters and precise locations
642 [PDecl' t] -- declarations
643 (Maybe (Name, FC)) -- instance constructor name and location
644 (Docstring (Either Err PTerm)) -- instance constructor docs
645 -- ^ Type class: arguments are documentation, syntax info, source location, constraints,
646 -- class name, class name location, parameters, method declarations, optional constructor name
648 (Docstring (Either Err PTerm)) -- Instance docs
649 [(Name, Docstring (Either Err PTerm))] -- Parameter docs
651 FC [(Name, t)] -- constraints
653 FC -- precise location of class
655 t -- full instance type
656 (Maybe Name) -- explicit name
658 -- ^ Instance declaration: arguments are documentation, syntax info, source
659 -- location, constraints, class name, parameters, full instance
660 -- type, optional explicit name, and definitions
661 | PDSL Name (DSL' t) -- ^ DSL declaration
662 | PSyntax FC Syntax -- ^ Syntax definition
663 | PMutual FC [PDecl' t] -- ^ Mutual block
664 | PDirective Directive -- ^ Compiler directive.
665 | PProvider (Docstring (Either Err PTerm)) SyntaxInfo FC FC (ProvideWhat' t) Name -- ^ Type provider. The first t is the type, the second is the term. The second FC is precise highlighting location.
666 | PTransform FC Bool t t -- ^ Source-to-source transformation rule. If
667 -- bool is True, lhs and rhs must be convertible
670deriving instance Binary PDecl'
671deriving instance NFData PDecl'
674-- | The set of source directives
675data Directive = DLib Codegen String |
676 DLink Codegen String |
677 DFlag Codegen String |
678 DInclude Codegen String |
681 DAccess Accessibility |
684 DDynamicLibs [String] |
685 DNameHint Name FC [(Name, FC)] |
686 DErrorHandlers Name FC Name FC [(Name, FC)] |
687 DLanguage LanguageExt |
690-- | A set of instructions for things that need to happen in IState
691-- after a term elaboration when there's been reflected elaboration.
692data RDeclInstructions = RTyDeclInstrs Name FC [PArg] Type
693 | RClausesInstrs Name [([Name], Term, Term)]
694 | RAddInstance Name Name
696-- | For elaborator state
697data EState = EState {
698 case_decls :: [(Name, PDecl)],
699 delayed_elab :: [(Int, Elab' EState ())],
700 new_tyDecls :: [RDeclInstructions],
701 highlighting :: [(FC, OutputAnnotation)]
705initEState = EState [] [] [] []
707type ElabD a = Elab' EState a
709highlightSource :: FC -> OutputAnnotation -> ElabD ()
710highlightSource fc annot =
711 updateAux (\aux -> aux { highlighting = (fc, annot) : highlighting aux })
713-- | One clause of a top-level definition. Term arguments to constructors are:
715-- 1. The whole application (missing for PClauseR and PWithR because they're within a "with" clause)
717-- 2. The list of extra 'with' patterns
719-- 3. The right-hand side
721-- 4. The where block (PDecl' t)
723data PClause' t = PClause FC Name t [t] t [PDecl' t] -- ^ A normal top-level definition.
724 | PWith FC Name t [t] t (Maybe (Name, FC)) [PDecl' t]
725 | PClauseR FC [t] t [PDecl' t]
726 | PWithR FC [t] t (Maybe (Name, FC)) [PDecl' t]
729deriving instance Binary PClause'
730deriving instance NFData PClause'
734data PData' t = PDatadecl { d_name :: Name, -- ^ The name of the datatype
735 d_name_fc :: FC, -- ^ The precise location of the type constructor name
736 d_tcon :: t, -- ^ Type constructor
737 d_cons :: [(Docstring (Either Err PTerm), [(Name, Docstring (Either Err PTerm))], Name, FC, t, FC, [Name])] -- ^ Constructors
739 -- ^ Data declaration
740 | PLaterdecl { d_name :: Name, d_name_fc :: FC, d_tcon :: t }
741 -- ^ "Placeholder" for data whose constructors are defined later
744deriving instance Binary PData'
745deriving instance NFData PData'
748-- Handy to get a free function for applying PTerm -> PTerm functions
749-- across a program, by deriving Functor
751type PDecl = PDecl' PTerm
752type PData = PData' PTerm
753type PClause = PClause' PTerm
755-- get all the names declared in a decl
757declared :: PDecl -> [Name]
758declared (PFix _ _ _) = []
759declared (PTy _ _ _ _ _ n fc t) = [n]
760declared (PPostulate _ _ _ _ _ _ n t) = [n]
761declared (PClauses _ _ n _) = [] -- not a declaration
762declared (PCAF _ n _) = [n]
763declared (PData _ _ _ _ _ (PDatadecl n _ _ ts)) = n : map fstt ts
764 where fstt (_, _, a, _, _, _, _) = a
765declared (PData _ _ _ _ _ (PLaterdecl n _ _)) = [n]
766declared (PParams _ _ ds) = concatMap declared ds
767declared (PNamespace _ _ ds) = concatMap declared ds
768declared (PRecord _ _ _ _ n _ _ _ _ cn _ _) = n : map fst (maybeToList cn)
769declared (PClass _ _ _ _ n _ _ _ _ ms cn cd) = n : (map fst (maybeToList cn) ++ concatMap declared ms)
770declared (PInstance _ _ _ _ _ _ _ _ _ _ _) = []
771declared (PDSL n _) = [n]
772declared (PSyntax _ _) = []
773declared (PMutual _ ds) = concatMap declared ds
774declared (PDirective _) = []
777-- get the names declared, not counting nested parameter blocks
778tldeclared :: PDecl -> [Name]
779tldeclared (PFix _ _ _) = []
780tldeclared (PTy _ _ _ _ _ n _ t) = [n]
781tldeclared (PPostulate _ _ _ _ _ _ n t) = [n]
782tldeclared (PClauses _ _ n _) = [] -- not a declaration
783tldeclared (PRecord _ _ _ _ n _ _ _ _ cn _ _) = n : map fst (maybeToList cn)
784tldeclared (PData _ _ _ _ _ (PDatadecl n _ _ ts)) = n : map fstt ts
785 where fstt (_, _, a, _, _, _, _) = a
786tldeclared (PParams _ _ ds) = []
787tldeclared (PMutual _ ds) = concatMap tldeclared ds
788tldeclared (PNamespace _ _ ds) = concatMap tldeclared ds
789tldeclared (PClass _ _ _ _ n _ _ _ _ ms cn _) = n : (map fst (maybeToList cn) ++ concatMap tldeclared ms)
790tldeclared (PInstance _ _ _ _ _ _ _ _ _ _ _) = []
793defined :: PDecl -> [Name]
794defined (PFix _ _ _) = []
795defined (PTy _ _ _ _ _ n _ t) = []
796defined (PPostulate _ _ _ _ _ _ n t) = []
797defined (PClauses _ _ n _) = [n] -- not a declaration
798defined (PCAF _ n _) = [n]
799defined (PData _ _ _ _ _ (PDatadecl n _ _ ts)) = n : map fstt ts
800 where fstt (_, _, a, _, _, _, _) = a
801defined (PData _ _ _ _ _ (PLaterdecl n _ _)) = []
802defined (PParams _ _ ds) = concatMap defined ds
803defined (PNamespace _ _ ds) = concatMap defined ds
804defined (PRecord _ _ _ _ n _ _ _ _ cn _ _) = n : map fst (maybeToList cn)
805defined (PClass _ _ _ _ n _ _ _ _ ms cn _) = n : (map fst (maybeToList cn) ++ concatMap defined ms)
806defined (PInstance _ _ _ _ _ _ _ _ _ _ _) = []
807defined (PDSL n _) = [n]
808defined (PSyntax _ _) = []
809defined (PMutual _ ds) = concatMap defined ds
810defined (PDirective _) = []
813updateN :: [(Name, Name)] -> Name -> Name
814updateN ns n | Just n' <- lookup n ns = n'
817updateNs :: [(Name, Name)] -> PTerm -> PTerm
819updateNs ns t = mapPT updateRef t
820 where updateRef (PRef fc fcs f) = PRef fc fcs (updateN ns f)
823-- updateDNs :: [(Name, Name)] -> PDecl -> PDecl
825-- updateDNs ns (PTy s f n t) | Just n' <- lookup n ns = PTy s f n' t
826-- updateDNs ns (PClauses f n c) | Just n' <- lookup n ns = PClauses f n' (map updateCNs c)
827-- where updateCNs ns (PClause n l ts r ds)
828-- = PClause (updateN ns n) (fmap (updateNs ns) l)
829-- (map (fmap (updateNs ns)) ts)
830-- (fmap (updateNs ns) r)
831-- (map (updateDNs ns) ds)
834data PunInfo = IsType | IsTerm | TypeOrTerm deriving (Eq, Show, Data, Typeable)
836-- | High level language terms
837data PTerm = PQuote Raw -- ^ Inclusion of a core term into the high-level language
838 | PRef FC [FC] Name -- ^ A reference to a variable. The FC is its precise source location for highlighting. The list of FCs is a collection of additional highlighting locations.
839 | PInferRef FC [FC] Name -- ^ A name to be defined later
840 | PPatvar FC Name -- ^ A pattern variable
841 | PLam FC Name FC PTerm PTerm -- ^ A lambda abstraction. Second FC is name span.
842 | PPi Plicity Name FC PTerm PTerm -- ^ (n : t1) -> t2, where the FC is for the precise location of the variable
843 | PLet FC Name FC PTerm PTerm PTerm -- ^ A let binding (second FC is precise name location)
844 | PTyped PTerm PTerm -- ^ Term with explicit type
845 | PApp FC PTerm [PArg] -- ^ e.g. IO (), List Char, length x
846 | PAppImpl PTerm [ImplicitInfo] -- ^ Implicit argument application (introduced during elaboration only)
847 | PAppBind FC PTerm [PArg] -- ^ implicitly bound application
848 | PMatchApp FC Name -- ^ Make an application by type matching
849 | PIfThenElse FC PTerm PTerm PTerm -- ^ Conditional expressions - elaborated to an overloading of ifThenElse
850 | PCase FC PTerm [(PTerm, PTerm)] -- ^ A case expression. Args are source location, scrutinee, and a list of pattern/RHS pairs
851 | PTrue FC PunInfo -- ^ Unit type..?
852 | PResolveTC FC -- ^ Solve this dictionary by type class resolution
853 | PRewrite FC PTerm PTerm (Maybe PTerm) -- ^ "rewrite" syntax, with optional result type
854 | PPair FC [FC] PunInfo PTerm PTerm -- ^ A pair (a, b) and whether it's a product type or a pair (solved by elaboration). The list of FCs is its punctuation.
855 | PDPair FC [FC] PunInfo PTerm PTerm PTerm -- ^ A dependent pair (tm : a ** b) and whether it's a sigma type or a pair that inhabits one (solved by elaboration). The [FC] is its punctuation.
856 | PAs FC Name PTerm -- ^ @-pattern, valid LHS only
857 | PAlternative [(Name, Name)] PAltType [PTerm] -- ^ (| A, B, C|). Includes unapplied unique name mappings for mkUniqueNames.
858 | PHidden PTerm -- ^ Irrelevant or hidden pattern
859 | PType FC -- ^ 'Type' type
860 | PUniverse Universe -- ^ Some universe
861 | PGoal FC PTerm Name PTerm -- ^ quoteGoal, used for %reflection functions
862 | PConstant FC Const -- ^ Builtin types
863 | Placeholder -- ^ Underscore
864 | PDoBlock [PDo] -- ^ Do notation
865 | PIdiom FC PTerm -- ^ Idiom brackets
867 | PMetavar FC Name -- ^ A metavariable, ?name, and its precise location
868 | PProof [PTactic] -- ^ Proof script
869 | PTactics [PTactic] -- ^ As PProof, but no auto solving
870 | PElabError Err -- ^ Error to report on elaboration
871 | PImpossible -- ^ Special case for declaring when an LHS can't typecheck
872 | PCoerced PTerm -- ^ To mark a coerced argument, so as not to coerce twice
873 | PDisamb [[T.Text]] PTerm -- ^ Preferences for explicit namespaces
874 | PUnifyLog PTerm -- ^ dump a trace of unifications when building term
875 | PNoImplicits PTerm -- ^ never run implicit converions on the term
876 | PQuasiquote PTerm (Maybe PTerm) -- ^ `(Term [: Term])
877 | PUnquote PTerm -- ^ ~Term
878 | PQuoteName Name FC -- ^ `{n} where the FC is the precise highlighting for the name in particular
879 | PRunElab FC PTerm [String] -- ^ %runElab tm - New-style proof script. Args are location, script, enclosing namespace.
880 | PConstSugar FC PTerm -- ^ A desugared constant. The FC is a precise source location that will be used to highlight it later.
881 deriving (Eq, Data, Typeable)
883data PAltType = ExactlyOne Bool -- ^ flag sets whether delay is allowed
886 deriving (Eq, Data, Typeable)
888-- | Transform the FCs in a PTerm. The first function transforms the
889-- general-purpose FCs, and the second transforms those that are used
890-- for semantic source highlighting, so they can be treated specially.
891mapPTermFC :: (FC -> FC) -> (FC -> FC) -> PTerm -> PTerm
892mapPTermFC f g (PQuote q) = PQuote q
893mapPTermFC f g (PRef fc fcs n) = PRef (g fc) (map g fcs) n
894mapPTermFC f g (PInferRef fc fcs n) = PInferRef (g fc) (map g fcs) n
895mapPTermFC f g (PPatvar fc n) = PPatvar (g fc) n
896mapPTermFC f g (PLam fc n fc' t1 t2) = PLam (f fc) n (g fc') (mapPTermFC f g t1) (mapPTermFC f g t2)
897mapPTermFC f g (PPi plic n fc t1 t2) = PPi plic n (g fc) (mapPTermFC f g t1) (mapPTermFC f g t2)
898mapPTermFC f g (PLet fc n fc' t1 t2 t3) = PLet (f fc) n (g fc') (mapPTermFC f g t1) (mapPTermFC f g t2) (mapPTermFC f g t3)
899mapPTermFC f g (PTyped t1 t2) = PTyped (mapPTermFC f g t1) (mapPTermFC f g t2)
900mapPTermFC f g (PApp fc t args) = PApp (f fc) (mapPTermFC f g t) (map (fmap (mapPTermFC f g)) args)
901mapPTermFC f g (PAppImpl t1 impls) = PAppImpl (mapPTermFC f g t1) impls
902mapPTermFC f g (PAppBind fc t args) = PAppBind (f fc) (mapPTermFC f g t) (map (fmap (mapPTermFC f g)) args)
903mapPTermFC f g (PMatchApp fc n) = PMatchApp (f fc) n
904mapPTermFC f g (PIfThenElse fc t1 t2 t3) = PIfThenElse (f fc) (mapPTermFC f g t1) (mapPTermFC f g t2) (mapPTermFC f g t3)
905mapPTermFC f g (PCase fc t cases) = PCase (f fc) (mapPTermFC f g t) (map (\(l,r) -> (mapPTermFC f g l, mapPTermFC f g r)) cases)
906mapPTermFC f g (PTrue fc info) = PTrue (f fc) info
907mapPTermFC f g (PResolveTC fc) = PResolveTC (f fc)
908mapPTermFC f g (PRewrite fc t1 t2 t3) = PRewrite (f fc) (mapPTermFC f g t1) (mapPTermFC f g t2) (fmap (mapPTermFC f g) t3)
909mapPTermFC f g (PPair fc hls info t1 t2) = PPair (f fc) (map g hls) info (mapPTermFC f g t1) (mapPTermFC f g t2)
910mapPTermFC f g (PDPair fc hls info t1 t2 t3) = PDPair (f fc) (map g hls) info (mapPTermFC f g t1) (mapPTermFC f g t2) (mapPTermFC f g t3)
911mapPTermFC f g (PAs fc n t) = PAs (f fc) n (mapPTermFC f g t)
912mapPTermFC f g (PAlternative ns ty ts) = PAlternative ns ty (map (mapPTermFC f g) ts)
913mapPTermFC f g (PHidden t) = PHidden (mapPTermFC f g t)
914mapPTermFC f g (PType fc) = PType (f fc)
915mapPTermFC f g (PUniverse u) = PUniverse u
916mapPTermFC f g (PGoal fc t1 n t2) = PGoal (f fc) (mapPTermFC f g t1) n (mapPTermFC f g t2)
917mapPTermFC f g (PConstant fc c) = PConstant (f fc) c
918mapPTermFC f g Placeholder = Placeholder
919mapPTermFC f g (PDoBlock dos) = PDoBlock (map mapPDoFC dos)
920 where mapPDoFC (DoExp fc t) = DoExp (f fc) (mapPTermFC f g t)
921 mapPDoFC (DoBind fc n nfc t) = DoBind (f fc) n (g nfc) (mapPTermFC f g t)
922 mapPDoFC (DoBindP fc t1 t2 alts) =
923 DoBindP (f fc) (mapPTermFC f g t1) (mapPTermFC f g t2) (map (\(l,r)-> (mapPTermFC f g l, mapPTermFC f g r)) alts)
924 mapPDoFC (DoLet fc n nfc t1 t2) = DoLet (f fc) n (g nfc) (mapPTermFC f g t1) (mapPTermFC f g t2)
925 mapPDoFC (DoLetP fc t1 t2) = DoLetP (f fc) (mapPTermFC f g t1) (mapPTermFC f g t2)
926mapPTermFC f g (PIdiom fc t) = PIdiom (f fc) (mapPTermFC f g t)
927mapPTermFC f g (PReturn fc) = PReturn (f fc)
928mapPTermFC f g (PMetavar fc n) = PMetavar (g fc) n
929mapPTermFC f g (PProof tacs) = PProof (map (fmap (mapPTermFC f g)) tacs)
930mapPTermFC f g (PTactics tacs) = PTactics (map (fmap (mapPTermFC f g)) tacs)
931mapPTermFC f g (PElabError err) = PElabError err
932mapPTermFC f g PImpossible = PImpossible
933mapPTermFC f g (PCoerced t) = PCoerced (mapPTermFC f g t)
934mapPTermFC f g (PDisamb msg t) = PDisamb msg (mapPTermFC f g t)
935mapPTermFC f g (PUnifyLog t) = PUnifyLog (mapPTermFC f g t)
936mapPTermFC f g (PNoImplicits t) = PNoImplicits (mapPTermFC f g t)
937mapPTermFC f g (PQuasiquote t1 t2) = PQuasiquote (mapPTermFC f g t1) (fmap (mapPTermFC f g) t2)
938mapPTermFC f g (PUnquote t) = PUnquote (mapPTermFC f g t)
939mapPTermFC f g (PRunElab fc tm ns) = PRunElab (f fc) (mapPTermFC f g tm) ns
940mapPTermFC f g (PConstSugar fc tm) = PConstSugar (g fc) (mapPTermFC f g tm)
941mapPTermFC f g (PQuoteName n fc) = PQuoteName n (g fc)
944dg instance Binary PTerm
945deriving instance NFData PTerm
948mapPT :: (PTerm -> PTerm) -> PTerm -> PTerm
949mapPT f t = f (mpt t) where
950 mpt (PLam fc n nfc t s) = PLam fc n nfc (mapPT f t) (mapPT f s)
951 mpt (PPi p n nfc t s) = PPi p n nfc (mapPT f t) (mapPT f s)
952 mpt (PLet fc n nfc ty v s) = PLet fc n nfc (mapPT f ty) (mapPT f v) (mapPT f s)
953 mpt (PRewrite fc t s g) = PRewrite fc (mapPT f t) (mapPT f s)
955 mpt (PApp fc t as) = PApp fc (mapPT f t) (map (fmap (mapPT f)) as)
956 mpt (PAppBind fc t as) = PAppBind fc (mapPT f t) (map (fmap (mapPT f)) as)
957 mpt (PCase fc c os) = PCase fc (mapPT f c) (map (pmap (mapPT f)) os)
958 mpt (PIfThenElse fc c t e) = PIfThenElse fc (mapPT f c) (mapPT f t) (mapPT f e)
959 mpt (PTyped l r) = PTyped (mapPT f l) (mapPT f r)
960 mpt (PPair fc hls p l r) = PPair fc hls p (mapPT f l) (mapPT f r)
961 mpt (PDPair fc hls p l t r) = PDPair fc hls p (mapPT f l) (mapPT f t) (mapPT f r)
962 mpt (PAlternative ns a as) = PAlternative ns a (map (mapPT f) as)
963 mpt (PHidden t) = PHidden (mapPT f t)
964 mpt (PDoBlock ds) = PDoBlock (map (fmap (mapPT f)) ds)
965 mpt (PProof ts) = PProof (map (fmap (mapPT f)) ts)
966 mpt (PTactics ts) = PTactics (map (fmap (mapPT f)) ts)
967 mpt (PUnifyLog tm) = PUnifyLog (mapPT f tm)
968 mpt (PDisamb ns tm) = PDisamb ns (mapPT f tm)
969 mpt (PNoImplicits tm) = PNoImplicits (mapPT f tm)
970 mpt (PGoal fc r n sc) = PGoal fc (mapPT f r) n (mapPT f sc)
974data PTactic' t = Intro [Name] | Intros | Focus Name
975 | Refine Name [Bool] | Rewrite t | DoUnify
982 | LetTac Name t | LetTacTy Name t t
983 | Exact t | Compute | Trivial | TCInstance
984 | ProofSearch Bool Bool Int (Maybe Name) [Name]
985 -- ^ the bool is whether to search recursively
988 | ProofState | ProofTerm | Undo
989 | Try (PTactic' t) (PTactic' t)
990 | TSeq (PTactic' t) (PTactic' t)
991 | ApplyTactic t -- see Language.Reflection module
995 | GoalType String (PTactic' t)
998 | TDocStr (Either Name Const)
1001 | TFail [ErrorReportPart]
1004 deriving (Show, Eq, Functor, Foldable, Traversable, Data, Typeable)
1006deriving instance Binary PTactic'
1007deriving instance NFData PTactic'
1009instance Sized a => Sized (PTactic' a) where
1010 size (Intro nms) = 1 + size nms
1012 size (Focus nm) = 1 + size nm
1013 size (Refine nm bs) = 1 + size nm + length bs
1014 size (Rewrite t) = 1 + size t
1015 size (Induction t) = 1 + size t
1016 size (LetTac nm t) = 1 + size nm + size t
1017 size (Exact t) = 1 + size t
1025 size (Try l r) = 1 + size l + size r
1026 size (TSeq l r) = 1 + size l + size r
1027 size (ApplyTactic t) = 1 + size t
1028 size (Reflect t) = 1 + size t
1029 size (Fill t) = 1 + size t
1033 size (TFail ts) = 1 + size ts
1036 size (CaseTac x) = 1 + size x
1037 size (Equiv t) = 1 + size t
1038 size (Claim x y) = 1 + size x + size y
1040 size (MatchRefine x) = 1 + size x
1041 size (LetTacTy x y z) = 1 + size x + size y + size z
1044type PTactic = PTactic' PTerm
1046data PDo' t = DoExp FC t
1047 | DoBind FC Name FC t -- ^ second FC is precise name location
1048 | DoBindP FC t t [(t,t)]
1049 | DoLet FC Name FC t t -- ^ second FC is precise name location
1051 deriving (Eq, Functor, Data, Typeable)
1053deriving instance Binary PDo'
1054deriving instance NFData PDo'
1057instance Sized a => Sized (PDo' a) where
1058 size (DoExp fc t) = 1 + size fc + size t
1059 size (DoBind fc nm nfc t) = 1 + size fc + size nm + size nfc + size t
1060 size (DoBindP fc l r alts) = 1 + size fc + size l + size r + size alts
1061 size (DoLet fc nm nfc l r) = 1 + size fc + size nm + size l + size r
1062 size (DoLetP fc l r) = 1 + size fc + size l + size r
1064type PDo = PDo' PTerm
1066-- The priority gives a hint as to elaboration order. Best to elaborate
1067-- things early which will help give a more concrete type to other
1068-- variables, e.g. a before (interpTy a).
1070data PArg' t = PImp { priority :: Int,
1071 machine_inf :: Bool, -- true if the machine inferred it
1072 argopts :: [ArgOpt],
1075 | PExp { priority :: Int,
1076 argopts :: [ArgOpt],
1079 | PConstraint { priority :: Int,
1080 argopts :: [ArgOpt],
1083 | PTacImplicit { priority :: Int,
1084 argopts :: [ArgOpt],
1088 deriving (Show, Eq, Functor, Data, Typeable)
1090data ArgOpt = AlwaysShow | HideDisplay | InaccessibleArg | UnknownImp
1091 deriving (Show, Eq, Data, Typeable)
1093instance Sized a => Sized (PArg' a) where
1094 size (PImp p _ l nm trm) = 1 + size nm + size trm
1095 size (PExp p l nm trm) = 1 + size nm + size trm
1096 size (PConstraint p l nm trm) = 1 + size nm +size nm + size trm
1097 size (PTacImplicit p l nm scr trm) = 1 + size nm + size scr + size trm
1100deriving instance Binary PArg'
1101deriving instance NFData PArg'
1104pimp n t mach = PImp 1 mach [] n t
1105pexp t = PExp 1 [] (sMN 0 "arg") t
1106pconst t = PConstraint 1 [] (sMN 0 "carg") t
1107ptacimp n s t = PTacImplicit 2 [] n s t
1109type PArg = PArg' PTerm
1111-- | Get the highest FC in a term, if one exists
1112highestFC :: PTerm -> Maybe FC
1113highestFC (PQuote _) = Nothing
1114highestFC (PRef fc _ _) = Just fc
1115highestFC (PInferRef fc _ _) = Just fc
1116highestFC (PPatvar fc _) = Just fc
1117highestFC (PLam fc _ _ _ _) = Just fc
1118highestFC (PPi _ _ _ _ _) = Nothing
1119highestFC (PLet fc _ _ _ _ _) = Just fc
1120highestFC (PTyped tm ty) = highestFC tm <|> highestFC ty
1121highestFC (PApp fc _ _) = Just fc
1122highestFC (PAppBind fc _ _) = Just fc
1123highestFC (PMatchApp fc _) = Just fc
1124highestFC (PCase fc _ _) = Just fc
1125highestFC (PIfThenElse fc _ _ _) = Just fc
1126highestFC (PTrue fc _) = Just fc
1127highestFC (PResolveTC fc) = Just fc
1128highestFC (PRewrite fc _ _ _) = Just fc
1129highestFC (PPair fc _ _ _ _) = Just fc
1130highestFC (PDPair fc _ _ _ _ _) = Just fc
1131highestFC (PAs fc _ _) = Just fc
1132highestFC (PAlternative _ _ args) =
1133 case mapMaybe highestFC args of
1136highestFC (PHidden _) = Nothing
1137highestFC (PType fc) = Just fc
1138highestFC (PUniverse _) = Nothing
1139highestFC (PGoal fc _ _ _) = Just fc
1140highestFC (PConstant fc _) = Just fc
1141highestFC Placeholder = Nothing
1142highestFC (PDoBlock lines) =
1143 case map getDoFC lines of
1147 getDoFC (DoExp fc t) = fc
1148 getDoFC (DoBind fc nm nfc t) = fc
1149 getDoFC (DoBindP fc l r alts) = fc
1150 getDoFC (DoLet fc nm nfc l r) = fc
1151 getDoFC (DoLetP fc l r) = fc
1153highestFC (PIdiom fc _) = Just fc
1154highestFC (PReturn fc) = Just fc
1155highestFC (PMetavar fc _) = Just fc
1156highestFC (PProof _) = Nothing
1157highestFC (PTactics _) = Nothing
1158highestFC (PElabError _) = Nothing
1159highestFC PImpossible = Nothing
1160highestFC (PCoerced tm) = highestFC tm
1161highestFC (PDisamb _ opts) = highestFC opts
1162highestFC (PUnifyLog tm) = highestFC tm
1163highestFC (PNoImplicits tm) = highestFC tm
1164highestFC (PQuasiquote _ _) = Nothing
1165highestFC (PUnquote tm) = highestFC tm
1166highestFC (PQuoteName _ fc) = Just fc
1167highestFC (PRunElab fc _ _) = Just fc
1168highestFC (PConstSugar fc _) = Just fc
1169highestFC (PAppImpl t _) = highestFC t
1173data ClassInfo = CI { instanceCtorName :: Name,
1174 class_methods :: [(Name, (FnOpts, PTerm))],
1175 class_defaults :: [(Name, (Name, PDecl))], -- method name -> default impl
1176 class_default_superclasses :: [PDecl],
1177 class_params :: [Name],
1178 class_instances :: [(Name, Bool)], -- the Bool is whether to include in instance search, so named instances are excluded
1179 class_determiners :: [Int] }
1182deriving instance Binary ClassInfo
1183deriving instance NFData ClassInfo
1186-- Type inference data
1188data TIData = TIPartial -- ^ a function with a partially defined type
1189 | TISolution [Term] -- ^ possible solutions to a metavariable in a type
1192-- | Miscellaneous information about functions
1193data FnInfo = FnInfo { fn_params :: [Int] }
1196deriving instance Binary FnInfo
1197deriving instance NFData FnInfo
1200data OptInfo = Optimise { inaccessible :: [(Int,Name)], -- includes names for error reporting
1201 detaggable :: Bool }
1204deriving instance Binary OptInfo
1205deriving instance NFData OptInfo
1208-- | Syntactic sugar info
1209data DSL' t = DSL { dsl_bind :: t,
1214 index_first :: Maybe t,
1215 index_next :: Maybe t,
1216 dsl_lambda :: Maybe t,
1220 deriving (Show, Functor)
1222deriving instance Binary DSL'
1223deriving instance NFData DSL'
1226type DSL = DSL' PTerm
1228data SynContext = PatternSyntax | TermSyntax | AnySyntax
1231deriving instance Binary SynContext
1232deriving instance NFData SynContext
1235data Syntax = Rule [SSymbol] PTerm SynContext
1238syntaxNames :: Syntax -> [Name]
1239syntaxNames (Rule syms _ _) = mapMaybe ename syms
1240 where ename (Keyword n) = Just n
1243syntaxSymbols :: Syntax -> [SSymbol]
1244syntaxSymbols (Rule ss _ _) = ss
1246deriving instance Binary Syntax
1247deriving instance NFData Syntax
1250data SSymbol = Keyword Name
1259deriving instance Binary SSymbol
1260deriving instance NFData SSymbol
1263newtype SyntaxRules = SyntaxRules { syntaxRulesList :: [Syntax] }
1265emptySyntaxRules :: SyntaxRules
1266emptySyntaxRules = SyntaxRules []
1268updateSyntaxRules :: [Syntax] -> SyntaxRules -> SyntaxRules
1269updateSyntaxRules rules (SyntaxRules sr) = SyntaxRules newRules
1271 newRules = sortBy (ruleSort `on` syntaxSymbols) (rules ++ sr)
1276 ruleSort (s1:ss1) (s2:ss2) =
1277 case symCompare s1 s2 of
1278 EQ -> ruleSort ss1 ss2
1281 -- Better than creating Ord instance for SSymbol since
1282 -- in general this ordering does not really make sense.
1283 symCompare (Keyword n1) (Keyword n2) = compare n1 n2
1284 symCompare (Keyword _) _ = LT
1285 symCompare (Symbol _) (Keyword _) = GT
1286 symCompare (Symbol s1) (Symbol s2) = compare s1 s2
1287 symCompare (Symbol _) _ = LT
1288 symCompare (Binding _) (Keyword _) = GT
1289 symCompare (Binding _) (Symbol _) = GT
1290 symCompare (Binding b1) (Binding b2) = compare b1 b2
1291 symCompare (Binding _) _ = LT
1292 symCompare (Expr _) (Keyword _) = GT
1293 symCompare (Expr _) (Symbol _) = GT
1294 symCompare (Expr _) (Binding _) = GT
1295 symCompare (Expr e1) (Expr e2) = compare e1 e2
1296 symCompare (Expr _) _ = LT
1297 symCompare (SimpleExpr _) (Keyword _) = GT
1298 symCompare (SimpleExpr _) (Symbol _) = GT
1299 symCompare (SimpleExpr _) (Binding _) = GT
1300 symCompare (SimpleExpr _) (Expr _) = GT
1301 symCompare (SimpleExpr e1) (SimpleExpr e2) = compare e1 e2
1303initDSL = DSL (PRef f [] (sUN ">>="))
1304 (PRef f [] (sUN "return"))
1305 (PRef f [] (sUN "<*>"))
1306 (PRef f [] (sUN "pure"))
1313 where f = fileFC "(builtin)"
1315data Using = UImplicit Name PTerm
1316 | UConstraint Name [Name]
1317 deriving (Show, Eq, Data, Typeable)
1319deriving instance Binary Using
1320deriving instance NFData Using
1323data SyntaxInfo = Syn { using :: [Using],
1324 syn_params :: [(Name, PTerm)],
1325 syn_namespace :: [String],
1327 imp_methods :: [Name], -- class methods. When expanding
1328 -- implicits, these should be expanded even under
1330 decoration :: Name -> Name,
1332 implicitAllowed :: Bool,
1333 maxline :: Maybe Int,
1336 syn_in_quasiquote :: Int }
1339deriving instance NFData SyntaxInfo
1340deriving instance Binary SyntaxInfo
1343defaultSyntax = Syn [] [] [] [] [] id False False Nothing 0 initDSL 0
1345expandNS :: SyntaxInfo -> Name -> Name
1346expandNS syn n@(NS _ _) = n
1347expandNS syn n = case syn_namespace syn of
1352-- For inferring types of things
1354bi = fileFC "builtin"
1356inferTy = sMN 0 "__Infer"
1357inferCon = sMN 0 "__infer"
1358inferDecl = PDatadecl inferTy NoFC
1360 [(emptyDocstring, [], inferCon, NoFC, PPi impl (sMN 0 "iType") NoFC (PType bi) (
1361 PPi expl (sMN 0 "ival") NoFC (PRef bi [] (sMN 0 "iType"))
1362 (PRef bi [] inferTy)), bi, [])]
1365infTerm t = PApp bi (PRef bi [] inferCon) [pimp (sMN 0 "iType") Placeholder True, pexp t]
1366infP = P (TCon 6 0) inferTy (TType (UVal 0))
1368getInferTerm, getInferType :: Term -> Term
1369getInferTerm (Bind n b sc) = Bind n b $ getInferTerm sc
1370getInferTerm (App _ (App _ _ _) tm) = tm
1371getInferTerm tm = tm -- error ("getInferTerm " ++ show tm)
1373getInferType (Bind n b sc) = Bind n (toTy b) $ getInferType sc
1374 where toTy (Lam t) = Pi Nothing t (TType (UVar 0))
1375 toTy (PVar t) = PVTy t
1377getInferType (App _ (App _ _ ty) _) = ty
1381-- Handy primitives: Unit, False, Pair, MkPair, =, mkForeign
1383primNames = [inferTy, inferCon]
1386unitCon = sUN "MkUnit"
1388falseDoc = fmap (const $ Msg "") . parseDocstring . T.pack $
1389 "The empty type, also known as the trivially false proposition." ++
1391 "Use `void` or `absurd` to prove anything if you have a variable " ++
1392 "of type `Void` in scope."
1395pairTy = sNS (sUN "Pair") ["Builtins"]
1396pairCon = sNS (sUN "MkPair") ["Builtins"]
1398upairTy = sNS (sUN "UPair") ["Builtins"]
1399upairCon = sNS (sUN "MkUPair") ["Builtins"]
1403eqDoc = fmap (const (Left $ Msg "")) . parseDocstring . T.pack $
1404 "The propositional equality type. A proof that `x` = `y`." ++
1406 "To use such a proof, pattern-match on it, and the two equal things will " ++
1407 "then need to be the _same_ pattern." ++
1409 "**Note**: Idris's equality type is potentially _heterogeneous_, which means that it " ++
1410 "is possible to state equalities between values of potentially different " ++
1411 "types. However, Idris will attempt the homogeneous case unless it fails to typecheck." ++
1413 "You may need to use `(~=~)` to explicitly request heterogeneous equality."
1415eqDecl = PDatadecl eqTy NoFC (piBindp impl [(n "A", PType bi), (n "B", PType bi)]
1416 (piBind [(n "x", PRef bi [] (n "A")), (n "y", PRef bi [] (n "B"))]
1418 [(reflDoc, reflParamDoc,
1419 eqCon, NoFC, PPi impl (n "A") NoFC (PType bi) (
1420 PPi impl (n "x") NoFC (PRef bi [] (n "A"))
1421 (PApp bi (PRef bi [] eqTy) [pimp (n "A") Placeholder False,
1422 pimp (n "B") Placeholder False,
1423 pexp (PRef bi [] (n "x")),
1424 pexp (PRef bi [] (n "x"))])), bi, [])]
1426 reflDoc = annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $
1427 "A proof that `x` in fact equals `x`. To construct this, you must have already " ++
1428 "shown that both sides are in fact equal."
1429 reflParamDoc = [(n "A", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the type at which the equality is proven"),
1430 (n "x", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the element shown to be equal to itself.")]
1432eqParamDoc = [(n "A", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the type of the left side of the equality"),
1433 (n "B", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the type of the right side of the equality")
1439-- | The special name to be used in the module documentation context -
1440-- not for use in the main definition context. The namespace around it
1441-- will determine the module to which the docs adhere.
1443modDocName = sMN 0 "ModuleDocs"
1445-- Defined in builtins.idr
1446sigmaTy = sNS (sUN "Sigma") ["Builtins"]
1447sigmaCon = sNS (sUN "MkSigma") ["Builtins"]
1449piBind :: [(Name, PTerm)] -> PTerm -> PTerm
1450piBind = piBindp expl
1452piBindp :: Plicity -> [(Name, PTerm)] -> PTerm -> PTerm
1454piBindp p ((n, ty):ns) t = PPi p n NoFC ty (piBindp p ns t)
1457-- Pretty-printing declarations and terms
1459-- These "show" instances render to an absurdly wide screen because inserted line breaks
1460-- could interfere with interactive editing, which calls "show".
1462instance Show PTerm where
1463 showsPrec _ tm = (displayS . renderPretty 1.0 10000000 . prettyImp defaultPPOption) tm
1465instance Show PDecl where
1466 showsPrec _ d = (displayS . renderPretty 1.0 10000000 . showDeclImp verbosePPOption) d
1468instance Show PClause where
1469 showsPrec _ c = (displayS . renderPretty 1.0 10000000 . showCImp verbosePPOption) c
1471instance Show PData where
1472 showsPrec _ d = (displayS . renderPretty 1.0 10000000 . showDImp defaultPPOption) d
1474instance Pretty PTerm OutputAnnotation where
1475 pretty = prettyImp defaultPPOption
1477-- | Colourise annotations according to an Idris state. It ignores the names
1478-- in the annotation, as there's no good way to show extended information on a
1480consoleDecorate :: IState -> OutputAnnotation -> String -> String
1481consoleDecorate ist _ | not (idris_colourRepl ist) = id
1482consoleDecorate ist (AnnConst c) = let theme = idris_colourTheme ist
1484 then colouriseType theme
1485 else colouriseData theme
1486consoleDecorate ist (AnnData _ _) = colouriseData (idris_colourTheme ist)
1487consoleDecorate ist (AnnType _ _) = colouriseType (idris_colourTheme ist)
1488consoleDecorate ist (AnnBoundName _ True) = colouriseImplicit (idris_colourTheme ist)
1489consoleDecorate ist (AnnBoundName _ False) = colouriseBound (idris_colourTheme ist)
1490consoleDecorate ist AnnKeyword = colouriseKeyword (idris_colourTheme ist)
1491consoleDecorate ist (AnnName n _ _ _) = let ctxt = tt_ctxt ist
1492 theme = idris_colourTheme ist
1494 _ | isDConName n ctxt -> colouriseData theme
1495 _ | isFnName n ctxt -> colouriseFun theme
1496 _ | isTConName n ctxt -> colouriseType theme
1497 _ | isPostulateName n ist -> colourisePostulate theme
1498 _ | otherwise -> id -- don't colourise unknown names
1499consoleDecorate ist (AnnFC _) = id
1500consoleDecorate ist (AnnTextFmt fmt) = Idris.Colours.colourise (colour fmt)
1501 where colour BoldText = IdrisColour Nothing True False True False
1502 colour UnderlineText = IdrisColour Nothing True True False False
1503 colour ItalicText = IdrisColour Nothing True False False True
1504consoleDecorate ist (AnnTerm _ _) = id
1505consoleDecorate ist (AnnSearchResult _) = id
1506consoleDecorate ist (AnnErr _) = id
1507consoleDecorate ist (AnnNamespace _ _) = id
1508consoleDecorate ist (AnnLink url) =
1509 \txt -> Idris.Colours.colourise (IdrisColour Nothing True True False False) txt ++ " (" ++ url ++ ")"
1511isPostulateName :: Name -> IState -> Bool
1512isPostulateName n ist = S.member n (idris_postulates ist)
1514-- | Pretty-print a high-level closed Idris term with no information about precedence/associativity
1515prettyImp :: PPOption -- ^^ pretty printing options
1516 -> PTerm -- ^^ the term to pretty-print
1517 -> Doc OutputAnnotation
1518prettyImp impl = pprintPTerm impl [] [] []
1520-- | Serialise something to base64 using its Binary instance.
1522-- | Do the right thing for rendering a term in an IState
1523prettyIst :: IState -> PTerm -> Doc OutputAnnotation
1524prettyIst ist = pprintPTerm (ppOptionIst ist) [] [] (idris_infixes ist)
1526-- | Pretty-print a high-level Idris term in some bindings context with infix info
1527pprintPTerm :: PPOption -- ^^ pretty printing options
1528 -> [(Name, Bool)] -- ^^ the currently-bound names and whether they are implicit
1529 -> [Name] -- ^^ names to always show in pi, even if not used
1530 -> [FixDecl] -- ^^ Fixity declarations
1531 -> PTerm -- ^^ the term to pretty-print
1532 -> Doc OutputAnnotation
1533pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd
1538 prettySe :: Maybe Int -> Int -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation
1539 prettySe d p bnd (PQuote r) =
1540 text "![" <> pretty r <> text "]"
1541 prettySe d p bnd (PPatvar fc n) = pretty n
1543 | Just str <- slist d p bnd e = depth d $ str
1544 | Just n <- snat d p e = depth d $ annotate (AnnData "Nat" "") (text (show n))
1545 prettySe d p bnd (PRef fc _ n) = prettyName True (ppopt_impl ppo) bnd n
1546 prettySe d p bnd (PLam fc n nfc ty sc) =
1547 depth d . bracket p startPrec . group . align . hang 2 $
1548 text "\\" <> prettyBindingOf n False <+> text "=>" <$>
1549 prettySe (decD d) startPrec ((n, False):bnd) sc
1550 prettySe d p bnd (PLet fc n nfc ty v sc) =
1551 depth d . bracket p startPrec . group . align $
1552 kwd "let" <+> (group . align . hang 2 $ prettyBindingOf n False <+> text "=" <$> prettySe (decD d) startPrec bnd v) </>
1553 kwd "in" <+> (group . align . hang 2 $ prettySe (decD d) startPrec ((n, False):bnd) sc)
1554 prettySe d p bnd (PPi (Exp l s _) n _ ty sc)
1555 | n `elem` allNamesIn sc || ppopt_impl ppo || n `elem` docArgs =
1556 depth d . bracket p startPrec . group $
1557 enclose lparen rparen (group . align $ prettyBindingOf n False <+> colon <+> prettySe (decD d) startPrec bnd ty) <+>
1558 st <> text "->" <$> prettySe (decD d) startPrec ((n, False):bnd) sc
1560 depth d . bracket p startPrec . group $
1561 group (prettySe (decD d) (startPrec + 1) bnd ty <+> st) <> text "->" <$>
1562 group (prettySe (decD d) startPrec ((n, False):bnd) sc)
1566 Static -> text "[static]" <> space
1568 prettySe d p bnd (PPi (Imp l s _ fa) n _ ty sc)
1570 depth d . bracket p startPrec $
1571 lbrace <> prettyBindingOf n True <+> colon <+> prettySe (decD d) startPrec bnd ty <> rbrace <+>
1572 st <> text "->" </> prettySe (decD d) startPrec ((n, True):bnd) sc
1573 | otherwise = depth d $ prettySe (decD d) startPrec ((n, True):bnd) sc
1577 Static -> text "[static]" <> space
1579 prettySe d p bnd (PPi (Constraint _ _) n _ ty sc) =
1580 depth d . bracket p startPrec $
1581 prettySe (decD d) (startPrec + 1) bnd ty <+> text "=>" </> prettySe (decD d) startPrec ((n, True):bnd) sc
1582 prettySe d p bnd (PPi (TacImp _ _ (PTactics [ProofSearch _ _ _ _ _])) n _ ty sc) =
1583 lbrace <> kwd "auto" <+> pretty n <+> colon <+> prettySe (decD d) startPrec bnd ty <>
1584 rbrace <+> text "->" </> prettySe (decD d) startPrec ((n, True):bnd) sc
1585 prettySe d p bnd (PPi (TacImp _ _ s) n _ ty sc) =
1586 depth d . bracket p startPrec $
1587 lbrace <> kwd "default" <+> prettySe (decD d) (funcAppPrec + 1) bnd s <+> pretty n <+> colon <+> prettySe (decD d) startPrec bnd ty <>
1588 rbrace <+> text "->" </> prettySe (decD d) startPrec ((n, True):bnd) sc
1589 -- This case preserves the behavior of the former constructor PEq.
1590 -- It should be removed if feasible when the pretty-printing of infix
1591 -- operators in general is improved.
1592 prettySe d p bnd (PApp _ (PRef _ _ n) [lt, rt, l, r])
1593 | n == eqTy, ppopt_impl ppo =
1594 depth d . bracket p eqPrec $
1595 enclose lparen rparen eq <+>
1596 align (group (vsep (map (prettyArgS (decD d) bnd)
1599 depth d . bracket p eqPrec . align . group $
1600 prettyTerm (getTm l) <+> eq <$> group (prettyTerm (getTm r))
1601 where eq = annName eqTy (text "=")
1603 prettyTerm = prettySe (decD d) (eqPrec + 1) bnd
1604 prettySe d p bnd (PApp _ (PRef _ _ f) args) -- normal names, no explicit args
1605 | UN nm <- basename f
1606 , not (ppopt_impl ppo) && null (getShowArgs args) =
1607 prettyName True (ppopt_impl ppo) bnd f
1608 prettySe d p bnd (PAppBind _ (PRef _ _ f) [])
1609 | not (ppopt_impl ppo) = text "!" <> prettyName True (ppopt_impl ppo) bnd f
1610 prettySe d p bnd (PApp _ (PRef _ _ op) args) -- infix operators
1611 | UN nm <- basename op
1613 (not (ppopt_impl ppo)) && (not $ isAlpha (thead nm)) =
1614 case getShowArgs args of
1616 [x] -> group (opName True <$> group (prettySe (decD d) startPrec bnd (getTm x)))
1617 [l,r] -> let precedence = maybe (startPrec - 1) prec f
1618 in depth d . bracket p precedence $ inFix (getTm l) (getTm r)
1619 (l@(PExp _ _ _ _) : r@(PExp _ _ _ _) : rest) ->
1620 depth d . bracket p funcAppPrec $
1621 enclose lparen rparen (inFix (getTm l) (getTm r)) <+>
1622 align (group (vsep (map (prettyArgS d bnd) rest)))
1623 as -> opName True <+> align (vsep (map (prettyArgS d bnd) as))
1624 where opName isPrefix = prettyName isPrefix (ppopt_impl ppo) bnd op
1625 f = getFixity (opStr op)
1627 Nothing -> funcAppPrec + 1
1628 Just (Infixl p') -> p'
1629 Just f' -> prec f' + 1
1631 Nothing -> funcAppPrec + 1
1632 Just (Infixr p') -> p'
1633 Just f' -> prec f' + 1
1634 inFix l r = align . group $
1635 (prettySe (decD d) left bnd l <+> opName False) <$>
1636 group (prettySe (decD d) right bnd r)
1637 prettySe d p bnd (PApp _ hd@(PRef fc _ f) [tm]) -- symbols, like 'foo
1638 | PConstant NoFC (Idris.Core.TT.Str str) <- getTm tm,
1639 f == sUN "Symbol_" = annotate (AnnType ("'" ++ str) ("The symbol " ++ str)) $
1640 char '\'' <> prettySe (decD d) startPrec bnd (PRef fc [] (sUN str))
1641 prettySe d p bnd (PApp _ f as) = -- Normal prefix applications
1642 let args = getShowArgs as
1643 fp = prettySe (decD d) (startPrec + 1) bnd f
1644 shownArgs = if ppopt_impl ppo then as else args
1646 depth d . bracket p funcAppPrec . group $
1649 else fp <+> align (vsep (map (prettyArgS d bnd) shownArgs))
1650 prettySe d p bnd (PCase _ scr cases) =
1651 align $ kwd "case" <+> prettySe (decD d) startPrec bnd scr <+> kwd "of" <$>
1652 depth d (indent 2 (vsep (map ppcase cases)))
1654 ppcase (l, r) = let prettyCase = prettySe (decD d) startPrec
1655 ([(n, False) | n <- vars l] ++ bnd)
1656 in nest nestingSize $
1657 prettyCase l <+> text "=>" <+> prettyCase r
1658 -- Warning: this is a bit of a hack. At this stage, we don't have the
1659 -- global context, so we can't determine which names are constructors,
1660 -- which are types, and which are pattern variables on the LHS of the
1661 -- case pattern. We use the heuristic that names without a namespace
1662 -- are patvars, because right now case blocks in PTerms are always
1663 -- delaborated from TT before being sent to the pretty-printer. If they
1664 -- start getting printed directly, THIS WILL BREAK.
1665 -- Potential solution: add a list of known patvars to the cases in
1666 -- PCase, and have the delaborator fill it out, kind of like the pun
1667 -- disambiguation on PDPair.
1668 vars tm = filter noNS (allNamesIn tm)
1669 noNS (NS _ _) = False
1672 prettySe d p bnd (PIfThenElse _ c t f) =
1673 depth d . bracket p funcAppPrec . group . align . hang 2 . vsep $
1674 [ kwd "if" <+> prettySe (decD d) startPrec bnd c
1675 , kwd "then" <+> prettySe (decD d) startPrec bnd t
1676 , kwd "else" <+> prettySe (decD d) startPrec bnd f
1678 prettySe d p bnd (PHidden tm) = text "." <> prettySe (decD d) funcAppPrec bnd tm
1679 prettySe d p bnd (PResolveTC _) = kwd "%instance"
1680 prettySe d p bnd (PTrue _ IsType) = annName unitTy $ text "()"
1681 prettySe d p bnd (PTrue _ IsTerm) = annName unitCon $ text "()"
1682 prettySe d p bnd (PTrue _ TypeOrTerm) = text "()"
1683 prettySe d p bnd (PRewrite _ l r _) =
1684 depth d . bracket p startPrec $
1685 text "rewrite" <+> prettySe (decD d) (startPrec + 1) bnd l <+> text "in" <+> prettySe (decD d) startPrec bnd r
1686 prettySe d p bnd (PTyped l r) =
1687 lparen <> prettySe (decD d) startPrec bnd l <+> colon <+> prettySe (decD d) startPrec bnd r <> rparen
1688 prettySe d p bnd pair@(PPair _ _ pun _ _) -- flatten tuples to the right, like parser
1689 | Just elts <- pairElts pair = depth d . enclose (ann lparen) (ann rparen) .
1690 align . group . vsep . punctuate (ann comma) $
1691 map (prettySe (decD d) startPrec bnd) elts
1692 where ann = case pun of
1694 IsType -> annName pairTy
1695 IsTerm -> annName pairCon
1696 prettySe d p bnd (PDPair _ _ pun l t r) =
1700 annotated (text "**") <+>
1701 prettySe (decD d) startPrec (addBinding bnd) r <>
1703 where annotated = case pun of
1704 IsType -> annName sigmaTy
1705 IsTerm -> annName sigmaCon
1707 (left, addBinding) = case (l, pun) of
1708 (PRef _ _ n, IsType) -> (bindingOf n False <+> text ":" <+> prettySe (decD d) startPrec bnd t, ((n, False) :))
1709 _ -> (prettySe (decD d) startPrec bnd l, id)
1710 prettySe d p bnd (PAlternative ns a as) =
1711 lparen <> text "|" <> prettyAs <> text "|" <> rparen
1714 foldr (\l -> \r -> l <+> text "," <+> r) empty $ map (depth d . prettySe (decD d) startPrec bnd) as
1715 prettySe d p bnd (PType _) = annotate (AnnType "Type" "The type of types") $ text "Type"
1716 prettySe d p bnd (PUniverse u) = annotate (AnnType (show u) "The type of unique types") $ text (show u)
1717 prettySe d p bnd (PConstant _ c) = annotate (AnnConst c) (text (show c))
1718 -- XXX: add pretty for tactics
1719 prettySe d p bnd (PProof ts) =
1720 kwd "proof" <+> lbrace <> ellipsis <> rbrace
1721 prettySe d p bnd (PTactics ts) =
1722 kwd "tactics" <+> lbrace <> ellipsis <> rbrace
1723 prettySe d p bnd (PMetavar _ n) = annotate (AnnName n (Just MetavarOutput) Nothing Nothing) $ text "?" <> pretty n
1724 prettySe d p bnd (PReturn f) = kwd "return"
1725 prettySe d p bnd PImpossible = kwd "impossible"
1726 prettySe d p bnd Placeholder = text "_"
1727 prettySe d p bnd (PDoBlock dos) =
1728 bracket p startPrec $
1729 kwd "do" <+> align (vsep (map (group . align . hang 2) (ppdo bnd dos)))
1730 where ppdo bnd (DoExp _ tm:dos) = prettySe (decD d) startPrec bnd tm : ppdo bnd dos
1731 ppdo bnd (DoBind _ bn _ tm : dos) =
1732 (prettyBindingOf bn False <+> text "<-" <+>
1733 group (align (hang 2 (prettySe (decD d) startPrec bnd tm)))) :
1734 ppdo ((bn, False):bnd) dos
1735 ppdo bnd (DoBindP _ _ _ _ : dos) = -- ok because never made by delab
1736 text "no pretty printer for pattern-matching do binding" :
1738 ppdo bnd (DoLet _ ln _ ty v : dos) =
1739 (kwd "let" <+> prettyBindingOf ln False <+>
1740 (if ty /= Placeholder
1741 then colon <+> prettySe (decD d) startPrec bnd ty <+> text "="
1743 group (align (hang 2 (prettySe (decD d) startPrec bnd v)))) :
1744 ppdo ((ln, False):bnd) dos
1745 ppdo bnd (DoLetP _ _ _ : dos) = -- ok because never made by delab
1746 text "no pretty printer for pattern-matching do binding" :
1749 prettySe d p bnd (PCoerced t) = prettySe d p bnd t
1750 prettySe d p bnd (PElabError s) = pretty s
1751 -- Quasiquote pprinting ignores bound vars
1752 prettySe d p bnd (PQuasiquote t Nothing) = text "`(" <> prettySe (decD d) p [] t <> text ")"
1753 prettySe d p bnd (PQuasiquote t (Just g)) = text "`(" <> prettySe (decD d) p [] t <+> colon <+> prettySe (decD d) p [] g <> text ")"
1754 prettySe d p bnd (PUnquote t) = text "~" <> prettySe (decD d) p bnd t
1755 prettySe d p bnd (PQuoteName n _) = text "`{" <> prettyName True (ppopt_impl ppo) bnd n <> text "}"
1756 prettySe d p bnd (PRunElab _ tm _) =
1757 bracket p funcAppPrec . group . align . hang 2 $
1759 prettySe (decD d) funcAppPrec bnd tm
1760 prettySe d p bnd (PConstSugar fc tm) = prettySe d p bnd tm -- should never occur, but harmless
1762 prettySe d p bnd _ = text "missing pretty-printer for term"
1764 prettyBindingOf :: Name -> Bool -> Doc OutputAnnotation
1765 prettyBindingOf n imp = annotate (AnnBoundName n imp) (text (display n))
1766 where display (UN n) = T.unpack n
1767 display (MN _ n) = T.unpack n
1768 -- If a namespace is specified on a binding form, we'd better show it regardless of the implicits settings
1769 display (NS n ns) = (concat . intersperse "." . map T.unpack . reverse) ns ++ "." ++ display n
1772 prettyArgS d bnd (PImp _ _ _ n tm) = prettyArgSi d bnd (n, tm)
1773 prettyArgS d bnd (PExp _ _ _ tm) = prettyArgSe d bnd tm
1774 prettyArgS d bnd (PConstraint _ _ _ tm) = prettyArgSc d bnd tm
1775 prettyArgS d bnd (PTacImplicit _ _ n _ tm) = prettyArgSti d bnd (n, tm)
1777 prettyArgSe d bnd arg = prettySe d (funcAppPrec + 1) bnd arg
1778 prettyArgSi d bnd (n, val) = lbrace <> pretty n <+> text "=" <+> prettySe (decD d) startPrec bnd val <> rbrace
1779 prettyArgSc d bnd val = lbrace <> lbrace <> prettySe (decD d) startPrec bnd val <> rbrace <> rbrace
1780 prettyArgSti d bnd (n, val) = lbrace <> kwd "auto" <+> pretty n <+> text "=" <+> prettySe (decD d) startPrec bnd val <> rbrace
1782 annName :: Name -> Doc OutputAnnotation -> Doc OutputAnnotation
1783 annName n = annotate (AnnName n Nothing Nothing Nothing)
1785 opStr :: Name -> String
1786 opStr (NS n _) = opStr n
1787 opStr (UN n) = T.unpack n
1789 slist' :: Maybe Int -> Int -> [(Name, Bool)] -> PTerm -> Maybe [Doc OutputAnnotation]
1790 slist' (Just d) _ _ _ | d <= 0 = Nothing
1792 | containsHole e = Nothing
1793 slist' d p bnd (PApp _ (PRef _ _ nil) _)
1794 | not (ppopt_impl ppo) && nsroot nil == sUN "Nil" = Just []
1795 slist' d p bnd (PRef _ _ nil)
1796 | not (ppopt_impl ppo) && nsroot nil == sUN "Nil" = Just []
1797 slist' d p bnd (PApp _ (PRef _ _ cons) args)
1798 | nsroot cons == sUN "::",
1799 (PExp {getTm=tl}):(PExp {getTm=hd}):imps <- reverse args,
1801 Just tl' <- slist' (decD d) p bnd tl
1802 = Just (prettySe d startPrec bnd hd : tl')
1804 isImp (PImp {}) = True
1806 slist' _ _ _ tm = Nothing
1808 slist d p bnd e | Just es <- slist' d p bnd e = Just $
1810 [] -> annotate (AnnData "" "") $ text "[]"
1811 [x] -> enclose left right . group $ x
1812 xs -> enclose left right .
1813 align . group . vsep .
1814 punctuate comma $ xs
1815 where left = (annotate (AnnData "" "") (text "["))
1816 right = (annotate (AnnData "" "") (text "]"))
1817 comma = (annotate (AnnData "" "") (text ","))
1818 slist _ _ _ _ = Nothing
1820 pairElts :: PTerm -> Maybe [PTerm]
1821 pairElts (PPair _ _ _ x y) | Just elts <- pairElts y = Just (x:elts)
1822 | otherwise = Just [x, y]
1823 pairElts _ = Nothing
1825 natns = "Prelude.Nat."
1827 snat :: Maybe Int -> Int -> PTerm -> Maybe Integer
1828 snat (Just x) _ _ | x <= 0 = Nothing
1829 snat d p (PRef _ _ z)
1830 | show z == (natns++"Z") || show z == "Z" = Just 0
1831 snat d p (PApp _ s [PExp {getTm=n}])
1832 | show s == (natns++"S") || show s == "S",
1833 Just n' <- snat (decD d) p n
1835 snat _ _ _ = Nothing
1837 bracket outer inner doc
1838 | outer > inner = lparen <> doc <> rparen
1841 ellipsis = text "..."
1844 depth (Just d) = if d <= 0 then const (ellipsis) else id
1846 decD = fmap (\x -> x - 1)
1848 kwd = annotate AnnKeyword . text
1850 fixities :: M.Map String Fixity
1851 fixities = M.fromList [(s, f) | (Fix f s) <- infixes]
1853 getFixity :: String -> Maybe Fixity
1854 getFixity = flip M.lookup fixities
1856-- | Strip away namespace information
1857basename :: Name -> Name
1858basename (NS n _) = basename n
1861-- | Determine whether a name was the one inserted for a hole or
1862-- guess by the delaborator
1863isHoleName :: Name -> Bool
1864isHoleName (UN n) = n == T.pack "[__]"
1867-- | Check whether a PTerm has been delaborated from a Term containing a Hole or Guess
1868containsHole :: PTerm -> Bool
1869containsHole pterm = or [isHoleName n | PRef _ _ n <- take 1000 $ universe pterm]
1871-- | Pretty-printer helper for names that attaches the correct annotations
1873 :: Bool -- ^^ whether the name should be parenthesised if it is an infix operator
1874 -> Bool -- ^^ whether to show namespaces
1875 -> [(Name, Bool)] -- ^^ the current bound variables and whether they are implicit
1876 -> Name -- ^^ the name to pprint
1877 -> Doc OutputAnnotation
1878prettyName infixParen showNS bnd n
1879 | (MN _ s) <- n, isPrefixOf "_" $ T.unpack s = text "_"
1880 | (UN n') <- n, T.unpack n' == "_" = text "_"
1881 | Just imp <- lookup n bnd = annotate (AnnBoundName n imp) fullName
1882 | otherwise = annotate (AnnName n Nothing Nothing Nothing) fullName
1883 where fullName = text nameSpace <> parenthesise (text (baseName n))
1884 baseName (UN n) = T.unpack n
1885 baseName (NS n ns) = baseName n
1886 baseName (MN i s) = T.unpack s
1887 baseName other = show other
1888 nameSpace = case n of
1889 (NS n' ns) -> if showNS then (concatMap (++ ".") . map T.unpack . reverse) ns else ""
1891 isInfix = case baseName n of
1893 (c : _) -> not (isAlpha c)
1894 parenthesise = if isInfix && infixParen then enclose lparen rparen else id
1897showCImp :: PPOption -> PClause -> Doc OutputAnnotation
1898showCImp ppo (PClause _ n l ws r w)
1899 = prettyImp ppo l <+> showWs ws <+> text "=" <+> prettyImp ppo r
1900 <+> text "where" <+> text (show w)
1903 showWs (x : xs) = text "|" <+> prettyImp ppo x <+> showWs xs
1904showCImp ppo (PWith _ n l ws r pn w)
1905 = prettyImp ppo l <+> showWs ws <+> text "with" <+> prettyImp ppo r
1906 <+> braces (text (show w))
1909 showWs (x : xs) = text "|" <+> prettyImp ppo x <+> showWs xs
1912showDImp :: PPOption -> PData -> Doc OutputAnnotation
1913showDImp ppo (PDatadecl n nfc ty cons)
1914 = text "data" <+> text (show n) <+> colon <+> prettyImp ppo ty <+> text "where" <$>
1915 (indent 2 $ vsep (map (\ (_, _, n, _, t, _, _) -> pipe <+> prettyName True False [] n <+> colon <+> prettyImp ppo t) cons))
1917showDecls :: PPOption -> [PDecl] -> Doc OutputAnnotation
1918showDecls o ds = vsep (map (showDeclImp o) ds)
1920showDeclImp _ (PFix _ f ops) = text (show f) <+> cat (punctuate (text ",") (map text ops))
1921showDeclImp o (PTy _ _ _ _ _ n _ t) = text "tydecl" <+> text (showCG n) <+> colon <+> prettyImp o t
1922showDeclImp o (PClauses _ _ n cs) = text "pat" <+> text (showCG n) <+> text "\t" <+>
1923 indent 2 (vsep (map (showCImp o) cs))
1924showDeclImp o (PData _ _ _ _ _ d) = showDImp o { ppopt_impl = True } d
1925showDeclImp o (PParams _ ns ps) = text "params" <+> braces (text (show ns) <> line <> showDecls o ps <> line)
1926showDeclImp o (PNamespace n fc ps) = text "namespace" <+> text n <> braces (line <> showDecls o ps <> line)
1927showDeclImp _ (PSyntax _ syn) = text "syntax" <+> text (show syn)
1928showDeclImp o (PClass _ _ _ cs n _ ps _ _ ds _ _)
1929 = text "class" <+> text (show cs) <+> text (show n) <+> text (show ps) <> line <> showDecls o ds
1930showDeclImp o (PInstance _ _ _ _ cs n _ _ t _ ds)
1931 = text "instance" <+> text (show cs) <+> text (show n) <+> prettyImp o t <> line <> showDecls o ds
1932showDeclImp _ _ = text "..."
1933-- showDeclImp (PImport o) = "import " ++ o
1935getImps :: [PArg] -> [(Name, PTerm)]
1937getImps (PImp _ _ _ n tm : xs) = (n, tm) : getImps xs
1938getImps (_ : xs) = getImps xs
1940getExps :: [PArg] -> [PTerm]
1942getExps (PExp _ _ _ tm : xs) = tm : getExps xs
1943getExps (_ : xs) = getExps xs
1945getShowArgs :: [PArg] -> [PArg]
1947getShowArgs (e@(PExp _ _ _ tm) : xs) = e : getShowArgs xs
1948getShowArgs (e : xs) | AlwaysShow `elem` argopts e = e : getShowArgs xs
1949 | PImp _ _ _ _ tm <- e
1950 , containsHole tm = e : getShowArgs xs
1951getShowArgs (_ : xs) = getShowArgs xs
1953getConsts :: [PArg] -> [PTerm]
1955getConsts (PConstraint _ _ _ tm : xs) = tm : getConsts xs
1956getConsts (_ : xs) = getConsts xs
1958getAll :: [PArg] -> [PTerm]
1963showName :: Maybe IState -- ^^ the Idris state, for information about names and colours
1964 -> [(Name, Bool)] -- ^^ the bound variables and whether they're implicit
1965 -> PPOption -- ^^ pretty printing options
1966 -> Bool -- ^^ whether to colourise
1967 -> Name -- ^^ the term to show
1969showName ist bnd ppo colour n = case ist of
1970 Just i -> if colour then colourise n (idris_colourTheme i) else showbasic n
1971 Nothing -> showbasic n
1972 where name = if ppopt_impl ppo then show n else showbasic n
1973 showbasic n@(UN _) = showCG n
1974 showbasic (MN i s) = str s
1975 showbasic (NS n s) = showSep "." (map str (reverse s)) ++ "." ++ showbasic n
1976 showbasic (SN s) = show s
1978 colourise n t = let ctxt' = fmap tt_ctxt ist in
1981 Just ctxt | Just impl <- lookup n bnd -> if impl then colouriseImplicit t name
1982 else colouriseBound t name
1983 | isDConName n ctxt -> colouriseData t name
1984 | isFnName n ctxt -> colouriseFun t name
1985 | isTConName n ctxt -> colouriseType t name
1986 -- The assumption is that if a name is not bound and does not exist in the
1987 -- global context, then we're somewhere in which implicit info has been lost
1988 -- (like error messages). Thus, unknown vars are colourised as implicits.
1989 | otherwise -> colouriseImplicit t name
1991showTm :: IState -- ^^ the Idris state, for information about identifiers and colours
1992 -> PTerm -- ^^ the term to show
1994showTm ist = displayDecorated (consoleDecorate ist) .
1995 renderPretty 0.8 100000 .
1996 prettyImp (ppOptionIst ist)
1998-- | Show a term with implicits, no colours
1999showTmImpls :: PTerm -> String
2000showTmImpls = flip (displayS . renderCompact . prettyImp verbosePPOption) ""
2004instance Sized PTerm where
2005 size (PQuote rawTerm) = size rawTerm
2006 size (PRef fc _ name) = size name
2007 size (PLam fc name _ ty bdy) = 1 + size ty + size bdy
2008 size (PPi plicity name fc ty bdy) = 1 + size ty + size fc + size bdy
2009 size (PLet fc name nfc ty def bdy) = 1 + size ty + size def + size bdy
2010 size (PTyped trm ty) = 1 + size trm + size ty
2011 size (PApp fc name args) = 1 + size args
2012 size (PAppBind fc name args) = 1 + size args
2013 size (PCase fc trm bdy) = 1 + size trm + size bdy
2014 size (PIfThenElse fc c t f) = 1 + sum (map size [c, t, f])
2015 size (PTrue fc _) = 1
2016 size (PResolveTC fc) = 1
2017 size (PRewrite fc left right _) = 1 + size left + size right
2018 size (PPair fc _ _ left right) = 1 + size left + size right
2019 size (PDPair fs _ _ left ty right) = 1 + size left + size ty + size right
2020 size (PAlternative _ a alts) = 1 + size alts
2021 size (PHidden hidden) = size hidden
2022 size (PUnifyLog tm) = size tm
2023 size (PDisamb _ tm) = size tm
2024 size (PNoImplicits tm) = size tm
2026 size (PUniverse _) = 1
2027 size (PConstant fc const) = 1 + size fc + size const
2028 size Placeholder = 1
2029 size (PDoBlock dos) = 1 + size dos
2030 size (PIdiom fc term) = 1 + size term
2031 size (PReturn fc) = 1
2032 size (PMetavar _ name) = 1
2033 size (PProof tactics) = size tactics
2034 size (PElabError err) = size err
2035 size PImpossible = 1
2038getPArity :: PTerm -> Int
2039getPArity (PPi _ _ _ _ sc) = 1 + getPArity sc
2042-- Return all names, free or globally bound, in the given term.
2044allNamesIn :: PTerm -> [Name]
2045allNamesIn tm = nub $ ni [] tm
2046 where -- TODO THINK added niTacImp, but is it right?
2048 | not (n `elem` env) = [n]
2049 ni env (PPatvar _ n) = [n]
2050 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
2051 ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
2052 ni env (PCase _ c os) = ni env c ++ concatMap (ni env) (map snd os)
2053 ni env (PIfThenElse _ c t f) = ni env c ++ ni env t ++ ni env f
2054 ni env (PLam fc n _ ty sc) = ni env ty ++ ni (n:env) sc
2055 ni env (PPi p n _ ty sc) = niTacImp env p ++ ni env ty ++ ni (n:env) sc
2056 ni env (PLet _ n _ ty val sc) = ni env ty ++ ni env val ++ ni (n:env) sc
2057 ni env (PHidden tm) = ni env tm
2058 ni env (PRewrite _ l r _) = ni env l ++ ni env r
2059 ni env (PTyped l r) = ni env l ++ ni env r
2060 ni env (PPair _ _ _ l r) = ni env l ++ ni env r
2061 ni env (PDPair _ _ _ (PRef _ _ n) Placeholder r) = n : ni env r
2062 ni env (PDPair _ _ _ (PRef _ _ n) t r) = ni env t ++ ni (n:env) r
2063 ni env (PDPair _ _ _ l t r) = ni env l ++ ni env t ++ ni env r
2064 ni env (PAlternative ns a ls) = concatMap (ni env) ls
2065 ni env (PUnifyLog tm) = ni env tm
2066 ni env (PDisamb _ tm) = ni env tm
2067 ni env (PNoImplicits tm) = ni env tm
2070 niTacImp env (TacImp _ _ scr) = ni env scr
2074-- Return all names defined in binders in the given term
2075boundNamesIn :: PTerm -> [Name]
2076boundNamesIn tm = S.toList (ni S.empty tm)
2077 where -- TODO THINK Added niTacImp, but is it right?
2078 ni set (PApp _ f as) = niTms (ni set f) (map getTm as)
2079 ni set (PAppBind _ f as) = niTms (ni set f) (map getTm as)
2080 ni set (PCase _ c os) = niTms (ni set c) (map snd os)
2081 ni set (PIfThenElse _ c t f) = niTms set [c, t, f]
2082 ni set (PLam fc n _ ty sc) = S.insert n $ ni (ni set ty) sc
2083 ni set (PLet fc n nfc ty val sc) = S.insert n $ ni (ni (ni set ty) val) sc
2084 ni set (PPi p n _ ty sc) = niTacImp (S.insert n $ ni (ni set ty) sc) p
2085 ni set (PRewrite _ l r _) = ni (ni set l) r
2086 ni set (PTyped l r) = ni (ni set l) r
2087 ni set (PPair _ _ _ l r) = ni (ni set l) r
2088 ni set (PDPair _ _ _ (PRef _ _ n) t r) = ni (ni set t) r
2089 ni set (PDPair _ _ _ l t r) = ni (ni (ni set l) t) r
2090 ni set (PAlternative ns a as) = niTms set as
2091 ni set (PHidden tm) = ni set tm
2092 ni set (PUnifyLog tm) = ni set tm
2093 ni set (PDisamb _ tm) = ni set tm
2094 ni set (PNoImplicits tm) = ni set tm
2098 niTms set (x : xs) = niTms (ni set x) xs
2100 niTacImp set (TacImp _ _ scr) = ni set scr
2101 niTacImp set _ = set
2103-- Return names which are valid implicits in the given term (type).
2104implicitNamesIn :: [Name] -> IState -> PTerm -> [Name]
2105implicitNamesIn uvars ist tm = nub $ ni [] tm
2108 | not (n `elem` env)
2109 = case lookupTy n (tt_ctxt ist) of
2111 _ -> if n `elem` uvars then [n] else []
2112 ni env (PApp _ f@(PRef _ _ n) as)
2113 | n `elem` uvars = ni env f ++ concatMap (ni env) (map getTm as)
2114 | otherwise = concatMap (ni env) (map getTm as)
2115 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
2116 ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
2117 ni env (PCase _ c os) = ni env c ++
2118 -- names in 'os', not counting the names bound in the cases
2119 (nub (concatMap (ni env) (map snd os))
2120 \\ nub (concatMap (ni env) (map fst os)))
2121 ni env (PIfThenElse _ c t f) = concatMap (ni env) [c, t, f]
2122 ni env (PLam fc n _ ty sc) = ni env ty ++ ni (n:env) sc
2123 ni env (PPi p n _ ty sc) = ni env ty ++ ni (n:env) sc
2124 ni env (PRewrite _ l r _) = ni env l ++ ni env r
2125 ni env (PTyped l r) = ni env l ++ ni env r
2126 ni env (PPair _ _ _ l r) = ni env l ++ ni env r
2127 ni env (PDPair _ _ _ (PRef _ _ n) t r) = ni env t ++ ni (n:env) r
2128 ni env (PDPair _ _ _ l t r) = ni env l ++ ni env t ++ ni env r
2129 ni env (PAlternative ns a as) = concatMap (ni env) as
2130 ni env (PHidden tm) = ni env tm
2131 ni env (PUnifyLog tm) = ni env tm
2132 ni env (PDisamb _ tm) = ni env tm
2133 ni env (PNoImplicits tm) = ni env tm
2136-- Return names which are free in the given term.
2137namesIn :: [(Name, PTerm)] -> IState -> PTerm -> [Name]
2138namesIn uvars ist tm = nub $ ni [] tm
2141 | not (n `elem` env)
2142 = case lookupTy n (tt_ctxt ist) of
2144 _ -> if n `elem` (map fst uvars) then [n] else []
2145 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
2146 ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
2147 ni env (PCase _ c os) = ni env c ++
2148 -- names in 'os', not counting the names bound in the cases
2149 (nub (concatMap (ni env) (map snd os))
2150 \\ nub (concatMap (ni env) (map fst os)))
2151 ni env (PIfThenElse _ c t f) = concatMap (ni env) [c, t, f]
2152 ni env (PLam fc n nfc ty sc) = ni env ty ++ ni (n:env) sc
2153 ni env (PPi p n _ ty sc) = niTacImp env p ++ ni env ty ++ ni (n:env) sc
2154 ni env (PRewrite _ l r _) = ni env l ++ ni env r
2155 ni env (PTyped l r) = ni env l ++ ni env r
2156 ni env (PPair _ _ _ l r) = ni env l ++ ni env r
2157 ni env (PDPair _ _ _ (PRef _ _ n) t r) = ni env t ++ ni (n:env) r
2158 ni env (PDPair _ _ _ l t r) = ni env l ++ ni env t ++ ni env r
2159 ni env (PAlternative ns a as) = concatMap (ni env) as
2160 ni env (PHidden tm) = ni env tm
2161 ni env (PUnifyLog tm) = ni env tm
2162 ni env (PDisamb _ tm) = ni env tm
2163 ni env (PNoImplicits tm) = ni env tm
2166 niTacImp env (TacImp _ _ scr) = ni env scr
2169-- Return which of the given names are used in the given term.
2171usedNamesIn :: [Name] -> IState -> PTerm -> [Name]
2172usedNamesIn vars ist tm = nub $ ni [] tm
2173 where -- TODO THINK added niTacImp, but is it right?
2175 | n `elem` vars && not (n `elem` env)
2176 = case lookupDefExact n (tt_ctxt ist) of
2179 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
2180 ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
2181 ni env (PCase _ c os) = ni env c ++ concatMap (ni env) (map snd os)
2182 ni env (PIfThenElse _ c t f) = concatMap (ni env) [c, t, f]
2183 ni env (PLam fc n _ ty sc) = ni env ty ++ ni (n:env) sc
2184 ni env (PPi p n _ ty sc) = niTacImp env p ++ ni env ty ++ ni (n:env) sc
2185 ni env (PRewrite _ l r _) = ni env l ++ ni env r
2186 ni env (PTyped l r) = ni env l ++ ni env r
2187 ni env (PPair _ _ _ l r) = ni env l ++ ni env r
2188 ni env (PDPair _ _ _ (PRef _ _ n) t r) = ni env t ++ ni (n:env) r
2189 ni env (PDPair _ _ _ l t r) = ni env l ++ ni env t ++ ni env r
2190 ni env (PAlternative ns a as) = concatMap (ni env) as
2191 ni env (PHidden tm) = ni env tm
2192 ni env (PUnifyLog tm) = ni env tm
2193 ni env (PDisamb _ tm) = ni env tm
2194 ni env (PNoImplicits tm) = ni env tm
2197 niTacImp env (TacImp _ _ scr) = ni env scr
2200-- Return the list of inaccessible (= dotted) positions for a name.
2201getErasureInfo :: IState -> Name -> [Int]
2202getErasureInfo ist n =
2203 case lookupCtxtExact n (idris_optimisation ist) of
2204 Just (Optimise inacc detagg) -> map fst inacc
keysesc to close
- j k
- move down, up
- enter
- open
- esc
- back, or up a level
- 1 2 3 4
- readme, files, commits, refs
- /
- filter
- y
- copy the clone command
- c
- compare the chosen commit with another (or shift-click both)
- ?
- show or hide this list