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
96defaultOpts = IOption { opt_logLevel = 0
97 , opt_typecase = False
98 , opt_typeintype = False
100 , opt_showimp = False
101 , opt_errContext = False
104 , opt_nobanner = False
106 , opt_codegen = Via "c"
107 , opt_outputTy = Executable
109 , opt_importdirs = []
113 , opt_origerr = False
114 , opt_autoSolve = True
115 , opt_autoImport = []
116 , opt_optimise = defaultOptimise
117 , opt_printdepth = Just 5000
120data PPOption = PPOption {
121 ppopt_impl :: Bool -- ^^ whether to show implicits
122 , ppopt_depth :: Maybe Int
125data Optimisation = PETransform -- partial eval and associated transforms
128defaultOptimise = [PETransform]
130-- | Pretty printing options with default verbosity.
131defaultPPOption :: PPOption
132defaultPPOption = PPOption { ppopt_impl = False , ppopt_depth = Just 200 }
134-- | Pretty printing options with the most verbosity.
135verbosePPOption :: PPOption
136verbosePPOption = PPOption { ppopt_impl = True, ppopt_depth = Just 200 }
138-- | Get pretty printing options from the big options record.
139ppOption :: IOption -> PPOption
140ppOption opt = PPOption {
141 ppopt_impl = opt_showimp opt,
142 ppopt_depth = opt_printdepth opt
145-- | Get pretty printing options from an idris state record.
146ppOptionIst :: IState -> PPOption
147ppOptionIst = ppOption . idris_options
149data LanguageExt = TypeProviders | ErrorReflection deriving (Show, Eq, Read, Ord)
151-- | The output mode in use
152data OutputMode = RawOutput Handle -- ^ Print user output directly to the handle
153 | IdeMode Integer Handle -- ^ Send IDE output for some request ID to the handle
156-- | How wide is the console?
157data ConsoleWidth = InfinitelyWide -- ^ Have pretty-printer assume that lines should not be broken
158 | ColsWide Int -- ^ Manually specified - must be positive
159 | AutomaticWidth -- ^ Attempt to determine width, or 80 otherwise
163-- | The global state used in the Idris monad
164data IState = IState {
165 tt_ctxt :: Context, -- ^ All the currently defined names and their terms
166 idris_constraints :: S.Set ConstraintFC,
167 -- ^ A list of universe constraints and their corresponding source locations
168 idris_infixes :: [FixDecl], -- ^ Currently defined infix operators
169 idris_implicits :: Ctxt [PArg],
170 idris_statics :: Ctxt [Bool],
171 idris_classes :: Ctxt ClassInfo,
172 idris_dsls :: Ctxt DSL,
173 idris_optimisation :: Ctxt OptInfo,
174 idris_datatypes :: Ctxt TypeInfo,
175 idris_namehints :: Ctxt [Name],
176 idris_patdefs :: Ctxt ([([Name], Term, Term)], [PTerm]), -- not exported
177 -- ^ list of lhs/rhs, and a list of missing clauses
178 idris_flags :: Ctxt [FnOpt],
179 idris_callgraph :: Ctxt CGInfo, -- name, args used in each pos
180 idris_calledgraph :: Ctxt [Name],
181 idris_docstrings :: Ctxt (Docstring DocTerm, [(Name, Docstring DocTerm)]),
182 idris_moduledocs :: Ctxt (Docstring DocTerm),
183 -- ^ module documentation is saved in a special MN so the context
184 -- mechanism can be used for disambiguation
185 idris_tyinfodata :: Ctxt TIData,
186 idris_fninfo :: Ctxt FnInfo,
187 idris_transforms :: Ctxt [(Term, Term)],
188 idris_autohints :: Ctxt [Name],
189 idris_totcheck :: [(FC, Name)], -- names to check totality on
190 idris_defertotcheck :: [(FC, Name)], -- names to check at the end
191 idris_totcheckfail :: [(FC, String)],
192 idris_options :: IOption,
194 idris_lineapps :: [((FilePath, Int), PTerm)],
195 -- ^ Full application LHS on source line
196 idris_metavars :: [(Name, (Maybe Name, Int, Bool))],
197 -- ^ The currently defined but not proven metavariables. The Int
198 -- is the number of vars to display as a context, the Maybe Name
199 -- is its top-level function, and the Bool is whether :p is
201 idris_coercions :: [Name],
202 idris_errRev :: [(Term, Term)],
203 syntax_rules :: SyntaxRules,
204 syntax_keywords :: [String],
205 imported :: [FilePath], -- ^ The imported modules
206 idris_scprims :: [(Name, (Int, PrimFn))],
207 idris_objs :: [(Codegen, FilePath)],
208 idris_libs :: [(Codegen, String)],
209 idris_cgflags :: [(Codegen, String)],
210 idris_hdrs :: [(Codegen, String)],
211 idris_imported :: [(FilePath, Bool)], -- ^ Imported ibc file names, whether public
212 proof_list :: [(Name, (Bool, [String]))],
214 parserWarnings :: [(FC, Err)],
215 lastParse :: Maybe Name,
216 indent_stack :: [Int],
217 brace_stack :: [Maybe Int],
218 lastTokenSpan :: Maybe FC, -- ^ What was the span of the latest token parsed?
219 idris_parsedSpan :: Maybe FC,
220 hide_list :: [(Name, Maybe Accessibility)],
221 default_access :: Accessibility,
222 default_total :: Bool,
223 ibc_write :: [IBCWrite],
224 compiled_so :: Maybe String,
225 idris_dynamic_libs :: [DynamicLib],
226 idris_language_extensions :: [LanguageExt],
227 idris_outputmode :: OutputMode,
228 idris_colourRepl :: Bool,
229 idris_colourTheme :: ColourTheme,
230 idris_errorhandlers :: [Name], -- ^ Global error handlers
231 idris_nameIdx :: (Int, Ctxt (Int, Name)),
232 idris_function_errorhandlers :: Ctxt (M.Map Name (S.Set Name)), -- ^ Specific error handlers
233 module_aliases :: M.Map [T.Text] [T.Text],
234 idris_consolewidth :: ConsoleWidth, -- ^ How many chars wide is the console?
235 idris_postulates :: S.Set Name,
236 idris_externs :: S.Set (Name, Int),
237 idris_erasureUsed :: [(Name, Int)], -- ^ Function/constructor name, argument position is used
238 idris_whocalls :: Maybe (M.Map Name [Name]),
239 idris_callswho :: Maybe (M.Map Name [Name]),
240 idris_repl_defs :: [Name], -- ^ List of names that were defined in the repl, and can be re-/un-defined
241 elab_stack :: [(Name, Bool)], -- ^ Stack of names currently being elaborated, Bool set if it's an instance
242 -- (instances appear twice; also as a funtion name)
243 idris_symbols :: M.Map Name Name, -- ^ Symbol table (preserves sharing of names)
244 idris_exports :: [Name], -- ^ Functions with ExportList
245 idris_highlightedRegions :: [(FC, OutputAnnotation)], -- ^ Highlighting information to output
246 idris_parserHighlights :: [(FC, OutputAnnotation)] -- ^ Highlighting information from the parser
249-- Required for parsers library, and therefore trifecta
250instance Show IState where
251 show = const "{internal state}"
253data SizeChange = Smaller | Same | Bigger | Unknown
256deriving instance Binary SizeChange
257deriving instance NFData SizeChange
260type SCGEntry = (Name, [Maybe (Int, SizeChange)])
261type UsageReason = (Name, Int) -- fn_name, its_arg_number
263data CGInfo = CGInfo { argsdef :: [Name],
264 calls :: [(Name, [[Name]])],
267 usedpos :: [(Int, [UsageReason])] }
270deriving instance Binary CGInfo
271deriving instance NFData CGInfo
274primDefs = [sUN "unsafePerformPrimIO",
275 sUN "mkLazyForeignPrim",
279-- information that needs writing for the current module's .ibc file
280data IBCWrite = IBCFix FixDecl
284 | IBCInstance Bool Bool Name Name
291 | IBCImport (Bool, FilePath) -- True = import public
292 | IBCImportDir FilePath
293 | IBCObj Codegen FilePath
294 | IBCLib Codegen String
295 | IBCCGFlag Codegen String
297 | IBCHeader Codegen String
298 | IBCAccess Name Accessibility
299 | IBCMetaInformation Name MetaInformation
300 | IBCTotal Name Totality
301 | IBCFlags Name [FnOpt]
302 | IBCFnInfo Name FnInfo
303 | IBCTrans Name (Term, Term)
304 | IBCErrRev (Term, Term)
308 | IBCDef Name -- i.e. main context
309 | IBCNameHint (Name, Name)
310 | IBCLineApp FilePath Int PTerm
311 | IBCErrorHandler Name
312 | IBCFunctionErrorHandler Name Name Name
314 | IBCExtern (Name, Int)
315 | IBCTotCheckErr FC String
317 | IBCModDocs Name -- ^ The name is the special name used to track module docs
318 | IBCUsage (Name, Int)
320 | IBCAutoHint Name Name
323-- | The initial state for the compiler
325idrisInit = IState initContext S.empty []
326 emptyContext emptyContext emptyContext emptyContext
327 emptyContext emptyContext emptyContext emptyContext
328 emptyContext emptyContext emptyContext emptyContext
329 emptyContext emptyContext emptyContext emptyContext
331 [] [] [] defaultOpts 6 [] [] [] [] emptySyntaxRules [] [] [] [] [] [] []
332 [] [] Nothing [] Nothing [] [] Nothing Nothing [] Hidden False [] Nothing [] []
333 (RawOutput stdout) True defaultTheme [] (0, emptyContext) emptyContext M.empty
334 AutomaticWidth S.empty S.empty [] Nothing Nothing [] [] M.empty [] [] []
336-- | The monad for the main REPL - reading and processing files and updating
337-- global state (hence the IO inner monad).
338--type Idris = WriterT [Either String (IO ())] (State IState a))
339type Idris = StateT IState (ExceptT Err IO)
341catchError :: Idris a -> (Err -> Idris a) -> Idris a
342catchError = liftCatch catchE
344throwError :: Err -> Idris a
345throwError = Trans.lift . throwE
347-- Commands in the REPL
349data Codegen = Via String
358deriving instance NFData Codegen
361data HowMuchDocs = FullDocs | OverviewDocs
367 | NewDefn [PDecl] -- ^ Each 'PDecl' should be either a type declaration (at most one) or a clause defining the same name.
371 | DocStr (Either Name Const) HowMuchDocs
374 | Load FilePath (Maybe Int) -- up to maximum line number
375 | ChangeDirectory FilePath
378 | Compile Codegen String
382 | Prove Bool Name -- ^ If false, use prover, if true, use elab shell
383 | AddProof (Maybe Name)
394 | DynamicLink FilePath
397 | Search [String] PTerm
398 | CaseSplitAt Bool Int Name
399 | AddClauseFrom Bool Int Name
400 | AddProofClauseFrom Bool Int Name
401 | AddMissing Bool Int Name
402 | MakeWith Bool Int Name
403 | MakeLemma Bool Int Name
404 | DoProofSearch Bool Bool Int Name [Name]
405 -- ^ the first bool is whether to update,
406 -- the second is whether to search recursively (i.e. for the arguments)
410 | SetColour ColourType IdrisColour
414 | SetConsoleWidth ConsoleWidth
415 | SetPrinterDepth (Maybe Int)
416 | Apropos [String] String
420 | MakeDoc String -- IdrisDoc
423 | PPrint OutputFmt Int PTerm
425 -- Debugging commands
427 | DebugUnify PTerm PTerm
429data OutputFmt = HTMLOutput | LaTeXOutput
431data Opt = Filename String
443 | NoBuiltins -- only for the really primitive stuff!
458 | Port String -- REPL TCP port
466 | PkgMkDoc String -- IdrisDoc
476 | OutputTy OutputType
477 | Extension LanguageExt
478 | InterpretScript String
480 | TargetTriple String
483 | AddOpt Optimisation
484 | RemoveOpt Optimisation
487 | AutoWidth -- ^ Automatically adjust terminal width
488 | AutoSolve -- ^ Automatically issue "solve" tactic in interactive prover
489 | UseConsoleWidth ConsoleWidth
493data ElabShellCmd = EQED | EAbandon | EUndo | EProofState | EProofTerm
494 | EEval PTerm | ECheck PTerm | ESearch PTerm
495 | EDocStr (Either Name Const)
498-- Parsed declarations
500data Fixity = Infixl { prec :: Int }
501 | Infixr { prec :: Int }
502 | InfixN { prec :: Int }
503 | PrefixN { prec :: Int }
506deriving instance Binary Fixity
507deriving instance NFData Fixity
510instance Show Fixity where
511 show (Infixl i) = "infixl " ++ show i
512 show (Infixr i) = "infixr " ++ show i
513 show (InfixN i) = "infix " ++ show i
514 show (PrefixN i) = "prefix " ++ show i
516data FixDecl = Fix Fixity String
519instance Show FixDecl where
520 show (Fix f s) = show f ++ " " ++ s
523deriving instance Binary FixDecl
524deriving instance NFData FixDecl
527instance Ord FixDecl where
528 compare (Fix x _) (Fix y _) = compare (prec x) (prec y)
531data Static = Static | Dynamic
532 deriving (Show, Eq, Data, Typeable)
534deriving instance Binary Static
535deriving instance NFData Static
538-- Mark bindings with their explicitness, and laziness
539data Plicity = Imp { pargopts :: [ArgOpt],
542 pscoped :: Maybe ImplicitInfo -- Nothing, if top level
544 | Exp { pargopts :: [ArgOpt],
546 pparam :: Bool } -- this is a param (rather than index)
547 | Constraint { pargopts :: [ArgOpt],
549 | TacImp { pargopts :: [ArgOpt],
552 deriving (Show, Eq, Data, Typeable)
555deriving instance Binary Plicity
556deriving instance NFData Plicity
559is_scoped :: Plicity -> Maybe ImplicitInfo
560is_scoped (Imp _ _ _ s) = s
563impl = Imp [] Dynamic False Nothing
564forall_imp = Imp [] Dynamic False (Just (Impl False))
565forall_constraint = Imp [] Dynamic False (Just (Impl True))
566expl = Exp [] Dynamic False
567expl_param = Exp [] Dynamic True
568constraint = Constraint [] Static
569tacimpl t = TacImp [] Dynamic t
571data FnOpt = Inlinable -- always evaluate when simplifying
572 | TotalFn | PartialFn | CoveringFn
573 | Coinductive | AssertTotal
574 | Dictionary -- type class dictionary, eval only when
575 -- a function argument, and further evaluation resutls
576 | Implicit -- implicit coercion
577 | NoImplicit -- do not apply implicit coercions
578 | CExport String -- export, with a C name
579 | ErrorHandler -- ^^ an error handler for use with the ErrorReflection extension
580 | ErrorReverse -- ^^ attempt to reverse normalise before showing in error
581 | Reflection -- a reflecting function, compile-time only
582 | Specialise [(Name, Maybe Int)] -- specialise it, freeze these names
583 | Constructor -- Data constructor type
584 | AutoHint -- use in auto implicit search
585 | PEGenerated -- generated by partial evaluator
588deriving instance Binary FnOpt
589deriving instance NFData FnOpt
594inlinable :: FnOpts -> Bool
595inlinable = elem Inlinable
597dictionary :: FnOpts -> Bool
598dictionary = elem Dictionary
601-- | Type provider - what to provide
602data ProvideWhat' t = ProvTerm t t -- ^ the first is the goal type, the second is the term
603 | ProvPostulate t -- ^ goal type must be Type, so only term
604 deriving (Show, Eq, Functor)
606type ProvideWhat = ProvideWhat' PTerm
608-- | Top-level declarations such as compiler directives, definitions,
609-- datatypes and typeclasses.
611 = PFix FC Fixity [String] -- ^ Fixity declaration
612 | PTy (Docstring (Either Err PTerm)) [(Name, Docstring (Either Err PTerm))] SyntaxInfo FC FnOpts Name FC t -- ^ Type declaration (last FC is precise name location)
613 | PPostulate Bool -- external def if true
614 (Docstring (Either Err PTerm)) SyntaxInfo FC FC FnOpts Name t -- ^ Postulate, second FC is precise name location
615 | PClauses FC FnOpts Name [PClause' t] -- ^ Pattern clause
616 | PCAF FC Name t -- ^ Top level constant
617 | PData (Docstring (Either Err PTerm)) [(Name, Docstring (Either Err PTerm))] SyntaxInfo FC DataOpts (PData' t) -- ^ Data declaration.
618 | PParams FC [(Name, t)] [PDecl' t] -- ^ Params block
619 | PNamespace String FC [PDecl' t]
620 -- ^ New namespace, where FC is accurate location of the
621 -- namespace in the file
622 | PRecord (Docstring (Either Err PTerm)) SyntaxInfo FC DataOpts
624 FC -- Record name precise location
625 [(Name, FC, Plicity, t)] -- Parameters, where FC is precise name span
626 [(Name, Docstring (Either Err PTerm))] -- Param Docs
627 [((Maybe (Name, FC)), Plicity, t, Maybe (Docstring (Either Err PTerm)))] -- Fields
628 (Maybe (Name, FC)) -- Optional constructor name and location
629 (Docstring (Either Err PTerm)) -- Constructor doc
630 SyntaxInfo -- Constructor SyntaxInfo
631 -- ^ Record declaration
632 | PClass (Docstring (Either Err PTerm)) SyntaxInfo FC
633 [(Name, t)] -- constraints
635 FC -- accurate location of class name
636 [(Name, FC, t)] -- parameters and precise locations
637 [(Name, Docstring (Either Err PTerm))] -- parameter docstrings
638 [(Name, FC)] -- determining parameters and precise locations
639 [PDecl' t] -- declarations
640 (Maybe (Name, FC)) -- instance constructor name and location
641 (Docstring (Either Err PTerm)) -- instance constructor docs
642 -- ^ Type class: arguments are documentation, syntax info, source location, constraints,
643 -- class name, class name location, parameters, method declarations, optional constructor name
645 (Docstring (Either Err PTerm)) -- Instance docs
646 [(Name, Docstring (Either Err PTerm))] -- Parameter docs
648 FC [(Name, t)] -- constraints
650 FC -- precise location of class
652 t -- full instance type
653 (Maybe Name) -- explicit name
655 -- ^ Instance declaration: arguments are documentation, syntax info, source
656 -- location, constraints, class name, parameters, full instance
657 -- type, optional explicit name, and definitions
658 | PDSL Name (DSL' t) -- ^ DSL declaration
659 | PSyntax FC Syntax -- ^ Syntax definition
660 | PMutual FC [PDecl' t] -- ^ Mutual block
661 | PDirective Directive -- ^ Compiler directive.
662 | 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.
663 | PTransform FC Bool t t -- ^ Source-to-source transformation rule. If
664 -- bool is True, lhs and rhs must be convertible
667deriving instance Binary PDecl'
668deriving instance NFData PDecl'
671-- | The set of source directives
672data Directive = DLib Codegen String |
673 DLink Codegen String |
674 DFlag Codegen String |
675 DInclude Codegen String |
678 DAccess Accessibility |
681 DDynamicLibs [String] |
682 DNameHint Name FC [(Name, FC)] |
683 DErrorHandlers Name FC Name FC [(Name, FC)] |
684 DLanguage LanguageExt |
687-- | A set of instructions for things that need to happen in IState
688-- after a term elaboration when there's been reflected elaboration.
689data RDeclInstructions = RTyDeclInstrs Name FC [PArg] Type
690 | RClausesInstrs Name [([Name], Term, Term)]
691 | RAddInstance Name Name
693-- | For elaborator state
694data EState = EState {
695 case_decls :: [(Name, PDecl)],
696 delayed_elab :: [(Int, Elab' EState ())],
697 new_tyDecls :: [RDeclInstructions],
698 highlighting :: [(FC, OutputAnnotation)]
702initEState = EState [] [] [] []
704type ElabD a = Elab' EState a
706highlightSource :: FC -> OutputAnnotation -> ElabD ()
707highlightSource fc annot =
708 updateAux (\aux -> aux { highlighting = (fc, annot) : highlighting aux })
710-- | One clause of a top-level definition. Term arguments to constructors are:
712-- 1. The whole application (missing for PClauseR and PWithR because they're within a "with" clause)
714-- 2. The list of extra 'with' patterns
716-- 3. The right-hand side
718-- 4. The where block (PDecl' t)
720data PClause' t = PClause FC Name t [t] t [PDecl' t] -- ^ A normal top-level definition.
721 | PWith FC Name t [t] t (Maybe (Name, FC)) [PDecl' t]
722 | PClauseR FC [t] t [PDecl' t]
723 | PWithR FC [t] t (Maybe (Name, FC)) [PDecl' t]
726deriving instance Binary PClause'
727deriving instance NFData PClause'
731data PData' t = PDatadecl { d_name :: Name, -- ^ The name of the datatype
732 d_name_fc :: FC, -- ^ The precise location of the type constructor name
733 d_tcon :: t, -- ^ Type constructor
734 d_cons :: [(Docstring (Either Err PTerm), [(Name, Docstring (Either Err PTerm))], Name, FC, t, FC, [Name])] -- ^ Constructors
736 -- ^ Data declaration
737 | PLaterdecl { d_name :: Name, d_name_fc :: FC, d_tcon :: t }
738 -- ^ "Placeholder" for data whose constructors are defined later
741deriving instance Binary PData'
742deriving instance NFData PData'
745-- Handy to get a free function for applying PTerm -> PTerm functions
746-- across a program, by deriving Functor
748type PDecl = PDecl' PTerm
749type PData = PData' PTerm
750type PClause = PClause' PTerm
752-- get all the names declared in a decl
754declared :: PDecl -> [Name]
755declared (PFix _ _ _) = []
756declared (PTy _ _ _ _ _ n fc t) = [n]
757declared (PPostulate _ _ _ _ _ _ n t) = [n]
758declared (PClauses _ _ n _) = [] -- not a declaration
759declared (PCAF _ n _) = [n]
760declared (PData _ _ _ _ _ (PDatadecl n _ _ ts)) = n : map fstt ts
761 where fstt (_, _, a, _, _, _, _) = a
762declared (PData _ _ _ _ _ (PLaterdecl n _ _)) = [n]
763declared (PParams _ _ ds) = concatMap declared ds
764declared (PNamespace _ _ ds) = concatMap declared ds
765declared (PRecord _ _ _ _ n _ _ _ _ cn _ _) = n : map fst (maybeToList cn)
766declared (PClass _ _ _ _ n _ _ _ _ ms cn cd) = n : (map fst (maybeToList cn) ++ concatMap declared ms)
767declared (PInstance _ _ _ _ _ _ _ _ _ _ _) = []
768declared (PDSL n _) = [n]
769declared (PSyntax _ _) = []
770declared (PMutual _ ds) = concatMap declared ds
771declared (PDirective _) = []
774-- get the names declared, not counting nested parameter blocks
775tldeclared :: PDecl -> [Name]
776tldeclared (PFix _ _ _) = []
777tldeclared (PTy _ _ _ _ _ n _ t) = [n]
778tldeclared (PPostulate _ _ _ _ _ _ n t) = [n]
779tldeclared (PClauses _ _ n _) = [] -- not a declaration
780tldeclared (PRecord _ _ _ _ n _ _ _ _ cn _ _) = n : map fst (maybeToList cn)
781tldeclared (PData _ _ _ _ _ (PDatadecl n _ _ ts)) = n : map fstt ts
782 where fstt (_, _, a, _, _, _, _) = a
783tldeclared (PParams _ _ ds) = []
784tldeclared (PMutual _ ds) = concatMap tldeclared ds
785tldeclared (PNamespace _ _ ds) = concatMap tldeclared ds
786tldeclared (PClass _ _ _ _ n _ _ _ _ ms cn _) = n : (map fst (maybeToList cn) ++ concatMap tldeclared ms)
787tldeclared (PInstance _ _ _ _ _ _ _ _ _ _ _) = []
790defined :: PDecl -> [Name]
791defined (PFix _ _ _) = []
792defined (PTy _ _ _ _ _ n _ t) = []
793defined (PPostulate _ _ _ _ _ _ n t) = []
794defined (PClauses _ _ n _) = [n] -- not a declaration
795defined (PCAF _ n _) = [n]
796defined (PData _ _ _ _ _ (PDatadecl n _ _ ts)) = n : map fstt ts
797 where fstt (_, _, a, _, _, _, _) = a
798defined (PData _ _ _ _ _ (PLaterdecl n _ _)) = []
799defined (PParams _ _ ds) = concatMap defined ds
800defined (PNamespace _ _ ds) = concatMap defined ds
801defined (PRecord _ _ _ _ n _ _ _ _ cn _ _) = n : map fst (maybeToList cn)
802defined (PClass _ _ _ _ n _ _ _ _ ms cn _) = n : (map fst (maybeToList cn) ++ concatMap defined ms)
803defined (PInstance _ _ _ _ _ _ _ _ _ _ _) = []
804defined (PDSL n _) = [n]
805defined (PSyntax _ _) = []
806defined (PMutual _ ds) = concatMap defined ds
807defined (PDirective _) = []
810updateN :: [(Name, Name)] -> Name -> Name
811updateN ns n | Just n' <- lookup n ns = n'
814updateNs :: [(Name, Name)] -> PTerm -> PTerm
816updateNs ns t = mapPT updateRef t
817 where updateRef (PRef fc fcs f) = PRef fc fcs (updateN ns f)
820-- updateDNs :: [(Name, Name)] -> PDecl -> PDecl
822-- updateDNs ns (PTy s f n t) | Just n' <- lookup n ns = PTy s f n' t
823-- updateDNs ns (PClauses f n c) | Just n' <- lookup n ns = PClauses f n' (map updateCNs c)
824-- where updateCNs ns (PClause n l ts r ds)
825-- = PClause (updateN ns n) (fmap (updateNs ns) l)
826-- (map (fmap (updateNs ns)) ts)
827-- (fmap (updateNs ns) r)
828-- (map (updateDNs ns) ds)
831data PunInfo = IsType | IsTerm | TypeOrTerm deriving (Eq, Show, Data, Typeable)
833-- | High level language terms
834data PTerm = PQuote Raw -- ^ Inclusion of a core term into the high-level language
835 | 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.
836 | PInferRef FC [FC] Name -- ^ A name to be defined later
837 | PPatvar FC Name -- ^ A pattern variable
838 | PLam FC Name FC PTerm PTerm -- ^ A lambda abstraction. Second FC is name span.
839 | PPi Plicity Name FC PTerm PTerm -- ^ (n : t1) -> t2, where the FC is for the precise location of the variable
840 | PLet FC Name FC PTerm PTerm PTerm -- ^ A let binding (second FC is precise name location)
841 | PTyped PTerm PTerm -- ^ Term with explicit type
842 | PApp FC PTerm [PArg] -- ^ e.g. IO (), List Char, length x
843 | PAppImpl PTerm [ImplicitInfo] -- ^ Implicit argument application (introduced during elaboration only)
844 | PAppBind FC PTerm [PArg] -- ^ implicitly bound application
845 | PMatchApp FC Name -- ^ Make an application by type matching
846 | PIfThenElse FC PTerm PTerm PTerm -- ^ Conditional expressions - elaborated to an overloading of ifThenElse
847 | PCase FC PTerm [(PTerm, PTerm)] -- ^ A case expression. Args are source location, scrutinee, and a list of pattern/RHS pairs
848 | PTrue FC PunInfo -- ^ Unit type..?
849 | PResolveTC FC -- ^ Solve this dictionary by type class resolution
850 | PRewrite FC PTerm PTerm (Maybe PTerm) -- ^ "rewrite" syntax, with optional result type
851 | 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.
852 | 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.
853 | PAs FC Name PTerm -- ^ @-pattern, valid LHS only
854 | PAlternative [(Name, Name)] PAltType [PTerm] -- ^ (| A, B, C|). Includes unapplied unique name mappings for mkUniqueNames.
855 | PHidden PTerm -- ^ Irrelevant or hidden pattern
856 | PType FC -- ^ 'Type' type
857 | PUniverse Universe -- ^ Some universe
858 | PGoal FC PTerm Name PTerm -- ^ quoteGoal, used for %reflection functions
859 | PConstant FC Const -- ^ Builtin types
860 | Placeholder -- ^ Underscore
861 | PDoBlock [PDo] -- ^ Do notation
862 | PIdiom FC PTerm -- ^ Idiom brackets
864 | PMetavar FC Name -- ^ A metavariable, ?name, and its precise location
865 | PProof [PTactic] -- ^ Proof script
866 | PTactics [PTactic] -- ^ As PProof, but no auto solving
867 | PElabError Err -- ^ Error to report on elaboration
868 | PImpossible -- ^ Special case for declaring when an LHS can't typecheck
869 | PCoerced PTerm -- ^ To mark a coerced argument, so as not to coerce twice
870 | PDisamb [[T.Text]] PTerm -- ^ Preferences for explicit namespaces
871 | PUnifyLog PTerm -- ^ dump a trace of unifications when building term
872 | PNoImplicits PTerm -- ^ never run implicit converions on the term
873 | PQuasiquote PTerm (Maybe PTerm) -- ^ `(Term [: Term])
874 | PUnquote PTerm -- ^ ~Term
875 | PQuoteName Name FC -- ^ `{n} where the FC is the precise highlighting for the name in particular
876 | PRunElab FC PTerm [String] -- ^ %runElab tm - New-style proof script. Args are location, script, enclosing namespace.
877 | PConstSugar FC PTerm -- ^ A desugared constant. The FC is a precise source location that will be used to highlight it later.
878 deriving (Eq, Data, Typeable)
880data PAltType = ExactlyOne Bool -- ^ flag sets whether delay is allowed
883 deriving (Eq, Data, Typeable)
885-- | Transform the FCs in a PTerm. The first function transforms the
886-- general-purpose FCs, and the second transforms those that are used
887-- for semantic source highlighting, so they can be treated specially.
888mapPTermFC :: (FC -> FC) -> (FC -> FC) -> PTerm -> PTerm
889mapPTermFC f g (PQuote q) = PQuote q
890mapPTermFC f g (PRef fc fcs n) = PRef (g fc) (map g fcs) n
891mapPTermFC f g (PInferRef fc fcs n) = PInferRef (g fc) (map g fcs) n
892mapPTermFC f g (PPatvar fc n) = PPatvar (g fc) n
893mapPTermFC f g (PLam fc n fc' t1 t2) = PLam (f fc) n (g fc') (mapPTermFC f g t1) (mapPTermFC f g t2)
894mapPTermFC f g (PPi plic n fc t1 t2) = PPi plic n (g fc) (mapPTermFC f g t1) (mapPTermFC f g t2)
895mapPTermFC 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)
896mapPTermFC f g (PTyped t1 t2) = PTyped (mapPTermFC f g t1) (mapPTermFC f g t2)
897mapPTermFC f g (PApp fc t args) = PApp (f fc) (mapPTermFC f g t) (map (fmap (mapPTermFC f g)) args)
898mapPTermFC f g (PAppImpl t1 impls) = PAppImpl (mapPTermFC f g t1) impls
899mapPTermFC f g (PAppBind fc t args) = PAppBind (f fc) (mapPTermFC f g t) (map (fmap (mapPTermFC f g)) args)
900mapPTermFC f g (PMatchApp fc n) = PMatchApp (f fc) n
901mapPTermFC f g (PIfThenElse fc t1 t2 t3) = PIfThenElse (f fc) (mapPTermFC f g t1) (mapPTermFC f g t2) (mapPTermFC f g t3)
902mapPTermFC 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)
903mapPTermFC f g (PTrue fc info) = PTrue (f fc) info
904mapPTermFC f g (PResolveTC fc) = PResolveTC (f fc)
905mapPTermFC f g (PRewrite fc t1 t2 t3) = PRewrite (f fc) (mapPTermFC f g t1) (mapPTermFC f g t2) (fmap (mapPTermFC f g) t3)
906mapPTermFC f g (PPair fc hls info t1 t2) = PPair (f fc) (map g hls) info (mapPTermFC f g t1) (mapPTermFC f g t2)
907mapPTermFC 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)
908mapPTermFC f g (PAs fc n t) = PAs (f fc) n (mapPTermFC f g t)
909mapPTermFC f g (PAlternative ns ty ts) = PAlternative ns ty (map (mapPTermFC f g) ts)
910mapPTermFC f g (PHidden t) = PHidden (mapPTermFC f g t)
911mapPTermFC f g (PType fc) = PType (f fc)
912mapPTermFC f g (PUniverse u) = PUniverse u
913mapPTermFC f g (PGoal fc t1 n t2) = PGoal (f fc) (mapPTermFC f g t1) n (mapPTermFC f g t2)
914mapPTermFC f g (PConstant fc c) = PConstant (f fc) c
915mapPTermFC f g Placeholder = Placeholder
916mapPTermFC f g (PDoBlock dos) = PDoBlock (map mapPDoFC dos)
917 where mapPDoFC (DoExp fc t) = DoExp (f fc) (mapPTermFC f g t)
918 mapPDoFC (DoBind fc n nfc t) = DoBind (f fc) n (g nfc) (mapPTermFC f g t)
919 mapPDoFC (DoBindP fc t1 t2 alts) =
920 DoBindP (f fc) (mapPTermFC f g t1) (mapPTermFC f g t2) (map (\(l,r)-> (mapPTermFC f g l, mapPTermFC f g r)) alts)
921 mapPDoFC (DoLet fc n nfc t1 t2) = DoLet (f fc) n (g nfc) (mapPTermFC f g t1) (mapPTermFC f g t2)
922 mapPDoFC (DoLetP fc t1 t2) = DoLetP (f fc) (mapPTermFC f g t1) (mapPTermFC f g t2)
923mapPTermFC f g (PIdiom fc t) = PIdiom (f fc) (mapPTermFC f g t)
924mapPTermFC f g (PReturn fc) = PReturn (f fc)
925mapPTermFC f g (PMetavar fc n) = PMetavar (g fc) n
926mapPTermFC f g (PProof tacs) = PProof (map (fmap (mapPTermFC f g)) tacs)
927mapPTermFC f g (PTactics tacs) = PTactics (map (fmap (mapPTermFC f g)) tacs)
928mapPTermFC f g (PElabError err) = PElabError err
929mapPTermFC f g PImpossible = PImpossible
930mapPTermFC f g (PCoerced t) = PCoerced (mapPTermFC f g t)
931mapPTermFC f g (PDisamb msg t) = PDisamb msg (mapPTermFC f g t)
932mapPTermFC f g (PUnifyLog t) = PUnifyLog (mapPTermFC f g t)
933mapPTermFC f g (PNoImplicits t) = PNoImplicits (mapPTermFC f g t)
934mapPTermFC f g (PQuasiquote t1 t2) = PQuasiquote (mapPTermFC f g t1) (fmap (mapPTermFC f g) t2)
935mapPTermFC f g (PUnquote t) = PUnquote (mapPTermFC f g t)
936mapPTermFC f g (PRunElab fc tm ns) = PRunElab (f fc) (mapPTermFC f g tm) ns
937mapPTermFC f g (PConstSugar fc tm) = PConstSugar (g fc) (mapPTermFC f g tm)
938mapPTermFC f g (PQuoteName n fc) = PQuoteName n (g fc)
941dg instance Binary PTerm
942deriving instance NFData PTerm
945mapPT :: (PTerm -> PTerm) -> PTerm -> PTerm
946mapPT f t = f (mpt t) where
947 mpt (PLam fc n nfc t s) = PLam fc n nfc (mapPT f t) (mapPT f s)
948 mpt (PPi p n nfc t s) = PPi p n nfc (mapPT f t) (mapPT f s)
949 mpt (PLet fc n nfc ty v s) = PLet fc n nfc (mapPT f ty) (mapPT f v) (mapPT f s)
950 mpt (PRewrite fc t s g) = PRewrite fc (mapPT f t) (mapPT f s)
952 mpt (PApp fc t as) = PApp fc (mapPT f t) (map (fmap (mapPT f)) as)
953 mpt (PAppBind fc t as) = PAppBind fc (mapPT f t) (map (fmap (mapPT f)) as)
954 mpt (PCase fc c os) = PCase fc (mapPT f c) (map (pmap (mapPT f)) os)
955 mpt (PIfThenElse fc c t e) = PIfThenElse fc (mapPT f c) (mapPT f t) (mapPT f e)
956 mpt (PTyped l r) = PTyped (mapPT f l) (mapPT f r)
957 mpt (PPair fc hls p l r) = PPair fc hls p (mapPT f l) (mapPT f r)
958 mpt (PDPair fc hls p l t r) = PDPair fc hls p (mapPT f l) (mapPT f t) (mapPT f r)
959 mpt (PAlternative ns a as) = PAlternative ns a (map (mapPT f) as)
960 mpt (PHidden t) = PHidden (mapPT f t)
961 mpt (PDoBlock ds) = PDoBlock (map (fmap (mapPT f)) ds)
962 mpt (PProof ts) = PProof (map (fmap (mapPT f)) ts)
963 mpt (PTactics ts) = PTactics (map (fmap (mapPT f)) ts)
964 mpt (PUnifyLog tm) = PUnifyLog (mapPT f tm)
965 mpt (PDisamb ns tm) = PDisamb ns (mapPT f tm)
966 mpt (PNoImplicits tm) = PNoImplicits (mapPT f tm)
967 mpt (PGoal fc r n sc) = PGoal fc (mapPT f r) n (mapPT f sc)
971data PTactic' t = Intro [Name] | Intros | Focus Name
972 | Refine Name [Bool] | Rewrite t | DoUnify
979 | LetTac Name t | LetTacTy Name t t
980 | Exact t | Compute | Trivial | TCInstance
981 | ProofSearch Bool Bool Int (Maybe Name) [Name]
982 -- ^ the bool is whether to search recursively
985 | ProofState | ProofTerm | Undo
986 | Try (PTactic' t) (PTactic' t)
987 | TSeq (PTactic' t) (PTactic' t)
988 | ApplyTactic t -- see Language.Reflection module
992 | GoalType String (PTactic' t)
995 | TDocStr (Either Name Const)
998 | TFail [ErrorReportPart]
1001 deriving (Show, Eq, Functor, Foldable, Traversable, Data, Typeable)
1003deriving instance Binary PTactic'
1004deriving instance NFData PTactic'
1006instance Sized a => Sized (PTactic' a) where
1007 size (Intro nms) = 1 + size nms
1009 size (Focus nm) = 1 + size nm
1010 size (Refine nm bs) = 1 + size nm + length bs
1011 size (Rewrite t) = 1 + size t
1012 size (Induction t) = 1 + size t
1013 size (LetTac nm t) = 1 + size nm + size t
1014 size (Exact t) = 1 + size t
1022 size (Try l r) = 1 + size l + size r
1023 size (TSeq l r) = 1 + size l + size r
1024 size (ApplyTactic t) = 1 + size t
1025 size (Reflect t) = 1 + size t
1026 size (Fill t) = 1 + size t
1030 size (TFail ts) = 1 + size ts
1033 size (CaseTac x) = 1 + size x
1034 size (Equiv t) = 1 + size t
1035 size (Claim x y) = 1 + size x + size y
1037 size (MatchRefine x) = 1 + size x
1038 size (LetTacTy x y z) = 1 + size x + size y + size z
1041type PTactic = PTactic' PTerm
1043data PDo' t = DoExp FC t
1044 | DoBind FC Name FC t -- ^ second FC is precise name location
1045 | DoBindP FC t t [(t,t)]
1046 | DoLet FC Name FC t t -- ^ second FC is precise name location
1048 deriving (Eq, Functor, Data, Typeable)
1050deriving instance Binary PDo'
1051deriving instance NFData PDo'
1054instance Sized a => Sized (PDo' a) where
1055 size (DoExp fc t) = 1 + size fc + size t
1056 size (DoBind fc nm nfc t) = 1 + size fc + size nm + size nfc + size t
1057 size (DoBindP fc l r alts) = 1 + size fc + size l + size r + size alts
1058 size (DoLet fc nm nfc l r) = 1 + size fc + size nm + size l + size r
1059 size (DoLetP fc l r) = 1 + size fc + size l + size r
1061type PDo = PDo' PTerm
1063-- The priority gives a hint as to elaboration order. Best to elaborate
1064-- things early which will help give a more concrete type to other
1065-- variables, e.g. a before (interpTy a).
1067data PArg' t = PImp { priority :: Int,
1068 machine_inf :: Bool, -- true if the machine inferred it
1069 argopts :: [ArgOpt],
1072 | PExp { priority :: Int,
1073 argopts :: [ArgOpt],
1076 | PConstraint { priority :: Int,
1077 argopts :: [ArgOpt],
1080 | PTacImplicit { priority :: Int,
1081 argopts :: [ArgOpt],
1085 deriving (Show, Eq, Functor, Data, Typeable)
1087data ArgOpt = AlwaysShow | HideDisplay | InaccessibleArg | UnknownImp
1088 deriving (Show, Eq, Data, Typeable)
1090instance Sized a => Sized (PArg' a) where
1091 size (PImp p _ l nm trm) = 1 + size nm + size trm
1092 size (PExp p l nm trm) = 1 + size nm + size trm
1093 size (PConstraint p l nm trm) = 1 + size nm +size nm + size trm
1094 size (PTacImplicit p l nm scr trm) = 1 + size nm + size scr + size trm
1097deriving instance Binary PArg'
1098deriving instance NFData PArg'
1101pimp n t mach = PImp 1 mach [] n t
1102pexp t = PExp 1 [] (sMN 0 "arg") t
1103pconst t = PConstraint 1 [] (sMN 0 "carg") t
1104ptacimp n s t = PTacImplicit 2 [] n s t
1106type PArg = PArg' PTerm
1108-- | Get the highest FC in a term, if one exists
1109highestFC :: PTerm -> Maybe FC
1110highestFC (PQuote _) = Nothing
1111highestFC (PRef fc _ _) = Just fc
1112highestFC (PInferRef fc _ _) = Just fc
1113highestFC (PPatvar fc _) = Just fc
1114highestFC (PLam fc _ _ _ _) = Just fc
1115highestFC (PPi _ _ _ _ _) = Nothing
1116highestFC (PLet fc _ _ _ _ _) = Just fc
1117highestFC (PTyped tm ty) = highestFC tm <|> highestFC ty
1118highestFC (PApp fc _ _) = Just fc
1119highestFC (PAppBind fc _ _) = Just fc
1120highestFC (PMatchApp fc _) = Just fc
1121highestFC (PCase fc _ _) = Just fc
1122highestFC (PIfThenElse fc _ _ _) = Just fc
1123highestFC (PTrue fc _) = Just fc
1124highestFC (PResolveTC fc) = Just fc
1125highestFC (PRewrite fc _ _ _) = Just fc
1126highestFC (PPair fc _ _ _ _) = Just fc
1127highestFC (PDPair fc _ _ _ _ _) = Just fc
1128highestFC (PAs fc _ _) = Just fc
1129highestFC (PAlternative _ _ args) =
1130 case mapMaybe highestFC args of
1133highestFC (PHidden _) = Nothing
1134highestFC (PType fc) = Just fc
1135highestFC (PUniverse _) = Nothing
1136highestFC (PGoal fc _ _ _) = Just fc
1137highestFC (PConstant fc _) = Just fc
1138highestFC Placeholder = Nothing
1139highestFC (PDoBlock lines) =
1140 case map getDoFC lines of
1144 getDoFC (DoExp fc t) = fc
1145 getDoFC (DoBind fc nm nfc t) = fc
1146 getDoFC (DoBindP fc l r alts) = fc
1147 getDoFC (DoLet fc nm nfc l r) = fc
1148 getDoFC (DoLetP fc l r) = fc
1150highestFC (PIdiom fc _) = Just fc
1151highestFC (PReturn fc) = Just fc
1152highestFC (PMetavar fc _) = Just fc
1153highestFC (PProof _) = Nothing
1154highestFC (PTactics _) = Nothing
1155highestFC (PElabError _) = Nothing
1156highestFC PImpossible = Nothing
1157highestFC (PCoerced tm) = highestFC tm
1158highestFC (PDisamb _ opts) = highestFC opts
1159highestFC (PUnifyLog tm) = highestFC tm
1160highestFC (PNoImplicits tm) = highestFC tm
1161highestFC (PQuasiquote _ _) = Nothing
1162highestFC (PUnquote tm) = highestFC tm
1163highestFC (PQuoteName _ fc) = Just fc
1164highestFC (PRunElab fc _ _) = Just fc
1165highestFC (PConstSugar fc _) = Just fc
1166highestFC (PAppImpl t _) = highestFC t
1170data ClassInfo = CI { instanceCtorName :: Name,
1171 class_methods :: [(Name, (FnOpts, PTerm))],
1172 class_defaults :: [(Name, (Name, PDecl))], -- method name -> default impl
1173 class_default_superclasses :: [PDecl],
1174 class_params :: [Name],
1175 class_instances :: [(Name, Bool)], -- the Bool is whether to include in instance search, so named instances are excluded
1176 class_determiners :: [Int] }
1179deriving instance Binary ClassInfo
1180deriving instance NFData ClassInfo
1183-- Type inference data
1185data TIData = TIPartial -- ^ a function with a partially defined type
1186 | TISolution [Term] -- ^ possible solutions to a metavariable in a type
1189-- | Miscellaneous information about functions
1190data FnInfo = FnInfo { fn_params :: [Int] }
1193deriving instance Binary FnInfo
1194deriving instance NFData FnInfo
1197data OptInfo = Optimise { inaccessible :: [(Int,Name)], -- includes names for error reporting
1198 detaggable :: Bool }
1201deriving instance Binary OptInfo
1202deriving instance NFData OptInfo
1205-- | Syntactic sugar info
1206data DSL' t = DSL { dsl_bind :: t,
1211 index_first :: Maybe t,
1212 index_next :: Maybe t,
1213 dsl_lambda :: Maybe t,
1217 deriving (Show, Functor)
1219deriving instance Binary DSL'
1220deriving instance NFData DSL'
1223type DSL = DSL' PTerm
1225data SynContext = PatternSyntax | TermSyntax | AnySyntax
1228deriving instance Binary SynContext
1229deriving instance NFData SynContext
1232data Syntax = Rule [SSymbol] PTerm SynContext
1235syntaxNames :: Syntax -> [Name]
1236syntaxNames (Rule syms _ _) = mapMaybe ename syms
1237 where ename (Keyword n) = Just n
1240syntaxSymbols :: Syntax -> [SSymbol]
1241syntaxSymbols (Rule ss _ _) = ss
1243deriving instance Binary Syntax
1244deriving instance NFData Syntax
1247data SSymbol = Keyword Name
1256deriving instance Binary SSymbol
1257deriving instance NFData SSymbol
1260newtype SyntaxRules = SyntaxRules { syntaxRulesList :: [Syntax] }
1262emptySyntaxRules :: SyntaxRules
1263emptySyntaxRules = SyntaxRules []
1265updateSyntaxRules :: [Syntax] -> SyntaxRules -> SyntaxRules
1266updateSyntaxRules rules (SyntaxRules sr) = SyntaxRules newRules
1268 newRules = sortBy (ruleSort `on` syntaxSymbols) (rules ++ sr)
1273 ruleSort (s1:ss1) (s2:ss2) =
1274 case symCompare s1 s2 of
1275 EQ -> ruleSort ss1 ss2
1278 -- Better than creating Ord instance for SSymbol since
1279 -- in general this ordering does not really make sense.
1280 symCompare (Keyword n1) (Keyword n2) = compare n1 n2
1281 symCompare (Keyword _) _ = LT
1282 symCompare (Symbol _) (Keyword _) = GT
1283 symCompare (Symbol s1) (Symbol s2) = compare s1 s2
1284 symCompare (Symbol _) _ = LT
1285 symCompare (Binding _) (Keyword _) = GT
1286 symCompare (Binding _) (Symbol _) = GT
1287 symCompare (Binding b1) (Binding b2) = compare b1 b2
1288 symCompare (Binding _) _ = LT
1289 symCompare (Expr _) (Keyword _) = GT
1290 symCompare (Expr _) (Symbol _) = GT
1291 symCompare (Expr _) (Binding _) = GT
1292 symCompare (Expr e1) (Expr e2) = compare e1 e2
1293 symCompare (Expr _) _ = LT
1294 symCompare (SimpleExpr _) (Keyword _) = GT
1295 symCompare (SimpleExpr _) (Symbol _) = GT
1296 symCompare (SimpleExpr _) (Binding _) = GT
1297 symCompare (SimpleExpr _) (Expr _) = GT
1298 symCompare (SimpleExpr e1) (SimpleExpr e2) = compare e1 e2
1300initDSL = DSL (PRef f [] (sUN ">>="))
1301 (PRef f [] (sUN "return"))
1302 (PRef f [] (sUN "<*>"))
1303 (PRef f [] (sUN "pure"))
1310 where f = fileFC "(builtin)"
1312data Using = UImplicit Name PTerm
1313 | UConstraint Name [Name]
1314 deriving (Show, Eq, Data, Typeable)
1316deriving instance Binary Using
1317deriving instance NFData Using
1320data SyntaxInfo = Syn { using :: [Using],
1321 syn_params :: [(Name, PTerm)],
1322 syn_namespace :: [String],
1324 imp_methods :: [Name], -- class methods. When expanding
1325 -- implicits, these should be expanded even under
1327 decoration :: Name -> Name,
1329 implicitAllowed :: Bool,
1330 maxline :: Maybe Int,
1333 syn_in_quasiquote :: Int }
1336deriving instance NFData SyntaxInfo
1337deriving instance Binary SyntaxInfo
1340defaultSyntax = Syn [] [] [] [] [] id False False Nothing 0 initDSL 0
1342expandNS :: SyntaxInfo -> Name -> Name
1343expandNS syn n@(NS _ _) = n
1344expandNS syn n = case syn_namespace syn of
1349-- For inferring types of things
1351bi = fileFC "builtin"
1353inferTy = sMN 0 "__Infer"
1354inferCon = sMN 0 "__infer"
1355inferDecl = PDatadecl inferTy NoFC
1357 [(emptyDocstring, [], inferCon, NoFC, PPi impl (sMN 0 "iType") NoFC (PType bi) (
1358 PPi expl (sMN 0 "ival") NoFC (PRef bi [] (sMN 0 "iType"))
1359 (PRef bi [] inferTy)), bi, [])]
1362infTerm t = PApp bi (PRef bi [] inferCon) [pimp (sMN 0 "iType") Placeholder True, pexp t]
1363infP = P (TCon 6 0) inferTy (TType (UVal 0))
1365getInferTerm, getInferType :: Term -> Term
1366getInferTerm (Bind n b sc) = Bind n b $ getInferTerm sc
1367getInferTerm (App _ (App _ _ _) tm) = tm
1368getInferTerm tm = tm -- error ("getInferTerm " ++ show tm)
1370getInferType (Bind n b sc) = Bind n (toTy b) $ getInferType sc
1371 where toTy (Lam t) = Pi Nothing t (TType (UVar 0))
1372 toTy (PVar t) = PVTy t
1374getInferType (App _ (App _ _ ty) _) = ty
1378-- Handy primitives: Unit, False, Pair, MkPair, =, mkForeign
1380primNames = [inferTy, inferCon]
1383unitCon = sUN "MkUnit"
1385falseDoc = fmap (const $ Msg "") . parseDocstring . T.pack $
1386 "The empty type, also known as the trivially false proposition." ++
1388 "Use `void` or `absurd` to prove anything if you have a variable " ++
1389 "of type `Void` in scope."
1392pairTy = sNS (sUN "Pair") ["Builtins"]
1393pairCon = sNS (sUN "MkPair") ["Builtins"]
1395upairTy = sNS (sUN "UPair") ["Builtins"]
1396upairCon = sNS (sUN "MkUPair") ["Builtins"]
1400eqDoc = fmap (const (Left $ Msg "")) . parseDocstring . T.pack $
1401 "The propositional equality type. A proof that `x` = `y`." ++
1403 "To use such a proof, pattern-match on it, and the two equal things will " ++
1404 "then need to be the _same_ pattern." ++
1406 "**Note**: Idris's equality type is potentially _heterogeneous_, which means that it " ++
1407 "is possible to state equalities between values of potentially different " ++
1408 "types. However, Idris will attempt the homogeneous case unless it fails to typecheck." ++
1410 "You may need to use `(~=~)` to explicitly request heterogeneous equality."
1412eqDecl = PDatadecl eqTy NoFC (piBindp impl [(n "A", PType bi), (n "B", PType bi)]
1413 (piBind [(n "x", PRef bi [] (n "A")), (n "y", PRef bi [] (n "B"))]
1415 [(reflDoc, reflParamDoc,
1416 eqCon, NoFC, PPi impl (n "A") NoFC (PType bi) (
1417 PPi impl (n "x") NoFC (PRef bi [] (n "A"))
1418 (PApp bi (PRef bi [] eqTy) [pimp (n "A") Placeholder False,
1419 pimp (n "B") Placeholder False,
1420 pexp (PRef bi [] (n "x")),
1421 pexp (PRef bi [] (n "x"))])), bi, [])]
1423 reflDoc = annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $
1424 "A proof that `x` in fact equals `x`. To construct this, you must have already " ++
1425 "shown that both sides are in fact equal."
1426 reflParamDoc = [(n "A", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the type at which the equality is proven"),
1427 (n "x", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the element shown to be equal to itself.")]
1429eqParamDoc = [(n "A", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the type of the left side of the equality"),
1430 (n "B", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the type of the right side of the equality")
1436-- | The special name to be used in the module documentation context -
1437-- not for use in the main definition context. The namespace around it
1438-- will determine the module to which the docs adhere.
1440modDocName = sMN 0 "ModuleDocs"
1442-- Defined in builtins.idr
1443sigmaTy = sNS (sUN "Sigma") ["Builtins"]
1444sigmaCon = sNS (sUN "MkSigma") ["Builtins"]
1446piBind :: [(Name, PTerm)] -> PTerm -> PTerm
1447piBind = piBindp expl
1449piBindp :: Plicity -> [(Name, PTerm)] -> PTerm -> PTerm
1451piBindp p ((n, ty):ns) t = PPi p n NoFC ty (piBindp p ns t)
1454-- Pretty-printing declarations and terms
1456-- These "show" instances render to an absurdly wide screen because inserted line breaks
1457-- could interfere with interactive editing, which calls "show".
1459instance Show PTerm where
1460 showsPrec _ tm = (displayS . renderPretty 1.0 10000000 . prettyImp defaultPPOption) tm
1462instance Show PDecl where
1463 showsPrec _ d = (displayS . renderPretty 1.0 10000000 . showDeclImp verbosePPOption) d
1465instance Show PClause where
1466 showsPrec _ c = (displayS . renderPretty 1.0 10000000 . showCImp verbosePPOption) c
1468instance Show PData where
1469 showsPrec _ d = (displayS . renderPretty 1.0 10000000 . showDImp defaultPPOption) d
1471instance Pretty PTerm OutputAnnotation where
1472 pretty = prettyImp defaultPPOption
1474-- | Colourise annotations according to an Idris state. It ignores the names
1475-- in the annotation, as there's no good way to show extended information on a
1477consoleDecorate :: IState -> OutputAnnotation -> String -> String
1478consoleDecorate ist _ | not (idris_colourRepl ist) = id
1479consoleDecorate ist (AnnConst c) = let theme = idris_colourTheme ist
1481 then colouriseType theme
1482 else colouriseData theme
1483consoleDecorate ist (AnnData _ _) = colouriseData (idris_colourTheme ist)
1484consoleDecorate ist (AnnType _ _) = colouriseType (idris_colourTheme ist)
1485consoleDecorate ist (AnnBoundName _ True) = colouriseImplicit (idris_colourTheme ist)
1486consoleDecorate ist (AnnBoundName _ False) = colouriseBound (idris_colourTheme ist)
1487consoleDecorate ist AnnKeyword = colouriseKeyword (idris_colourTheme ist)
1488consoleDecorate ist (AnnName n _ _ _) = let ctxt = tt_ctxt ist
1489 theme = idris_colourTheme ist
1491 _ | isDConName n ctxt -> colouriseData theme
1492 _ | isFnName n ctxt -> colouriseFun theme
1493 _ | isTConName n ctxt -> colouriseType theme
1494 _ | isPostulateName n ist -> colourisePostulate theme
1495 _ | otherwise -> id -- don't colourise unknown names
1496consoleDecorate ist (AnnFC _) = id
1497consoleDecorate ist (AnnTextFmt fmt) = Idris.Colours.colourise (colour fmt)
1498 where colour BoldText = IdrisColour Nothing True False True False
1499 colour UnderlineText = IdrisColour Nothing True True False False
1500 colour ItalicText = IdrisColour Nothing True False False True
1501consoleDecorate ist (AnnTerm _ _) = id
1502consoleDecorate ist (AnnSearchResult _) = id
1503consoleDecorate ist (AnnErr _) = id
1504consoleDecorate ist (AnnNamespace _ _) = id
1505consoleDecorate ist (AnnLink url) =
1506 \txt -> Idris.Colours.colourise (IdrisColour Nothing True True False False) txt ++ " (" ++ url ++ ")"
1508isPostulateName :: Name -> IState -> Bool
1509isPostulateName n ist = S.member n (idris_postulates ist)
1511-- | Pretty-print a high-level closed Idris term with no information about precedence/associativity
1512prettyImp :: PPOption -- ^^ pretty printing options
1513 -> PTerm -- ^^ the term to pretty-print
1514 -> Doc OutputAnnotation
1515prettyImp impl = pprintPTerm impl [] [] []
1517-- | Serialise something to base64 using its Binary instance.
1519-- | Do the right thing for rendering a term in an IState
1520prettyIst :: IState -> PTerm -> Doc OutputAnnotation
1521prettyIst ist = pprintPTerm (ppOptionIst ist) [] [] (idris_infixes ist)
1523-- | Pretty-print a high-level Idris term in some bindings context with infix info
1524pprintPTerm :: PPOption -- ^^ pretty printing options
1525 -> [(Name, Bool)] -- ^^ the currently-bound names and whether they are implicit
1526 -> [Name] -- ^^ names to always show in pi, even if not used
1527 -> [FixDecl] -- ^^ Fixity declarations
1528 -> PTerm -- ^^ the term to pretty-print
1529 -> Doc OutputAnnotation
1530pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd
1535 prettySe :: Maybe Int -> Int -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation
1536 prettySe d p bnd (PQuote r) =
1537 text "![" <> pretty r <> text "]"
1538 prettySe d p bnd (PPatvar fc n) = pretty n
1540 | Just str <- slist d p bnd e = depth d $ str
1541 | Just n <- snat d p e = depth d $ annotate (AnnData "Nat" "") (text (show n))
1542 prettySe d p bnd (PRef fc _ n) = prettyName True (ppopt_impl ppo) bnd n
1543 prettySe d p bnd (PLam fc n nfc ty sc) =
1544 depth d . bracket p startPrec . group . align . hang 2 $
1545 text "\\" <> prettyBindingOf n False <+> text "=>" <$>
1546 prettySe (decD d) startPrec ((n, False):bnd) sc
1547 prettySe d p bnd (PLet fc n nfc ty v sc) =
1548 depth d . bracket p startPrec . group . align $
1549 kwd "let" <+> (group . align . hang 2 $ prettyBindingOf n False <+> text "=" <$> prettySe (decD d) startPrec bnd v) </>
1550 kwd "in" <+> (group . align . hang 2 $ prettySe (decD d) startPrec ((n, False):bnd) sc)
1551 prettySe d p bnd (PPi (Exp l s _) n _ ty sc)
1552 | n `elem` allNamesIn sc || ppopt_impl ppo || n `elem` docArgs =
1553 depth d . bracket p startPrec . group $
1554 enclose lparen rparen (group . align $ prettyBindingOf n False <+> colon <+> prettySe (decD d) startPrec bnd ty) <+>
1555 st <> text "->" <$> prettySe (decD d) startPrec ((n, False):bnd) sc
1557 depth d . bracket p startPrec . group $
1558 group (prettySe (decD d) (startPrec + 1) bnd ty <+> st) <> text "->" <$>
1559 group (prettySe (decD d) startPrec ((n, False):bnd) sc)
1563 Static -> text "[static]" <> space
1565 prettySe d p bnd (PPi (Imp l s _ fa) n _ ty sc)
1567 depth d . bracket p startPrec $
1568 lbrace <> prettyBindingOf n True <+> colon <+> prettySe (decD d) startPrec bnd ty <> rbrace <+>
1569 st <> text "->" </> prettySe (decD d) startPrec ((n, True):bnd) sc
1570 | otherwise = depth d $ prettySe (decD d) startPrec ((n, True):bnd) sc
1574 Static -> text "[static]" <> space
1576 prettySe d p bnd (PPi (Constraint _ _) n _ ty sc) =
1577 depth d . bracket p startPrec $
1578 prettySe (decD d) (startPrec + 1) bnd ty <+> text "=>" </> prettySe (decD d) startPrec ((n, True):bnd) sc
1579 prettySe d p bnd (PPi (TacImp _ _ (PTactics [ProofSearch _ _ _ _ _])) n _ ty sc) =
1580 lbrace <> kwd "auto" <+> pretty n <+> colon <+> prettySe (decD d) startPrec bnd ty <>
1581 rbrace <+> text "->" </> prettySe (decD d) startPrec ((n, True):bnd) sc
1582 prettySe d p bnd (PPi (TacImp _ _ s) n _ ty sc) =
1583 depth d . bracket p startPrec $
1584 lbrace <> kwd "default" <+> prettySe (decD d) (funcAppPrec + 1) bnd s <+> pretty n <+> colon <+> prettySe (decD d) startPrec bnd ty <>
1585 rbrace <+> text "->" </> prettySe (decD d) startPrec ((n, True):bnd) sc
1586 -- This case preserves the behavior of the former constructor PEq.
1587 -- It should be removed if feasible when the pretty-printing of infix
1588 -- operators in general is improved.
1589 prettySe d p bnd (PApp _ (PRef _ _ n) [lt, rt, l, r])
1590 | n == eqTy, ppopt_impl ppo =
1591 depth d . bracket p eqPrec $
1592 enclose lparen rparen eq <+>
1593 align (group (vsep (map (prettyArgS (decD d) bnd)
1596 depth d . bracket p eqPrec . align . group $
1597 prettyTerm (getTm l) <+> eq <$> group (prettyTerm (getTm r))
1598 where eq = annName eqTy (text "=")
1600 prettyTerm = prettySe (decD d) (eqPrec + 1) bnd
1601 prettySe d p bnd (PApp _ (PRef _ _ f) args) -- normal names, no explicit args
1602 | UN nm <- basename f
1603 , not (ppopt_impl ppo) && null (getShowArgs args) =
1604 prettyName True (ppopt_impl ppo) bnd f
1605 prettySe d p bnd (PAppBind _ (PRef _ _ f) [])
1606 | not (ppopt_impl ppo) = text "!" <> prettyName True (ppopt_impl ppo) bnd f
1607 prettySe d p bnd (PApp _ (PRef _ _ op) args) -- infix operators
1608 | UN nm <- basename op
1610 (not (ppopt_impl ppo)) && (not $ isAlpha (thead nm)) =
1611 case getShowArgs args of
1613 [x] -> group (opName True <$> group (prettySe (decD d) startPrec bnd (getTm x)))
1614 [l,r] -> let precedence = maybe (startPrec - 1) prec f
1615 in depth d . bracket p precedence $ inFix (getTm l) (getTm r)
1616 (l@(PExp _ _ _ _) : r@(PExp _ _ _ _) : rest) ->
1617 depth d . bracket p funcAppPrec $
1618 enclose lparen rparen (inFix (getTm l) (getTm r)) <+>
1619 align (group (vsep (map (prettyArgS d bnd) rest)))
1620 as -> opName True <+> align (vsep (map (prettyArgS d bnd) as))
1621 where opName isPrefix = prettyName isPrefix (ppopt_impl ppo) bnd op
1622 f = getFixity (opStr op)
1624 Nothing -> funcAppPrec + 1
1625 Just (Infixl p') -> p'
1626 Just f' -> prec f' + 1
1628 Nothing -> funcAppPrec + 1
1629 Just (Infixr p') -> p'
1630 Just f' -> prec f' + 1
1631 inFix l r = align . group $
1632 (prettySe (decD d) left bnd l <+> opName False) <$>
1633 group (prettySe (decD d) right bnd r)
1634 prettySe d p bnd (PApp _ hd@(PRef fc _ f) [tm]) -- symbols, like 'foo
1635 | PConstant NoFC (Idris.Core.TT.Str str) <- getTm tm,
1636 f == sUN "Symbol_" = annotate (AnnType ("'" ++ str) ("The symbol " ++ str)) $
1637 char '\'' <> prettySe (decD d) startPrec bnd (PRef fc [] (sUN str))
1638 prettySe d p bnd (PApp _ f as) = -- Normal prefix applications
1639 let args = getShowArgs as
1640 fp = prettySe (decD d) (startPrec + 1) bnd f
1641 shownArgs = if ppopt_impl ppo then as else args
1643 depth d . bracket p funcAppPrec . group $
1646 else fp <+> align (vsep (map (prettyArgS d bnd) shownArgs))
1647 prettySe d p bnd (PCase _ scr cases) =
1648 align $ kwd "case" <+> prettySe (decD d) startPrec bnd scr <+> kwd "of" <$>
1649 depth d (indent 2 (vsep (map ppcase cases)))
1651 ppcase (l, r) = let prettyCase = prettySe (decD d) startPrec
1652 ([(n, False) | n <- vars l] ++ bnd)
1653 in nest nestingSize $
1654 prettyCase l <+> text "=>" <+> prettyCase r
1655 -- Warning: this is a bit of a hack. At this stage, we don't have the
1656 -- global context, so we can't determine which names are constructors,
1657 -- which are types, and which are pattern variables on the LHS of the
1658 -- case pattern. We use the heuristic that names without a namespace
1659 -- are patvars, because right now case blocks in PTerms are always
1660 -- delaborated from TT before being sent to the pretty-printer. If they
1661 -- start getting printed directly, THIS WILL BREAK.
1662 -- Potential solution: add a list of known patvars to the cases in
1663 -- PCase, and have the delaborator fill it out, kind of like the pun
1664 -- disambiguation on PDPair.
1665 vars tm = filter noNS (allNamesIn tm)
1666 noNS (NS _ _) = False
1669 prettySe d p bnd (PIfThenElse _ c t f) =
1670 depth d . bracket p funcAppPrec . group . align . hang 2 . vsep $
1671 [ kwd "if" <+> prettySe (decD d) startPrec bnd c
1672 , kwd "then" <+> prettySe (decD d) startPrec bnd t
1673 , kwd "else" <+> prettySe (decD d) startPrec bnd f
1675 prettySe d p bnd (PHidden tm) = text "." <> prettySe (decD d) funcAppPrec bnd tm
1676 prettySe d p bnd (PResolveTC _) = kwd "%instance"
1677 prettySe d p bnd (PTrue _ IsType) = annName unitTy $ text "()"
1678 prettySe d p bnd (PTrue _ IsTerm) = annName unitCon $ text "()"
1679 prettySe d p bnd (PTrue _ TypeOrTerm) = text "()"
1680 prettySe d p bnd (PRewrite _ l r _) =
1681 depth d . bracket p startPrec $
1682 text "rewrite" <+> prettySe (decD d) (startPrec + 1) bnd l <+> text "in" <+> prettySe (decD d) startPrec bnd r
1683 prettySe d p bnd (PTyped l r) =
1684 lparen <> prettySe (decD d) startPrec bnd l <+> colon <+> prettySe (decD d) startPrec bnd r <> rparen
1685 prettySe d p bnd pair@(PPair _ _ pun _ _) -- flatten tuples to the right, like parser
1686 | Just elts <- pairElts pair = depth d . enclose (ann lparen) (ann rparen) .
1687 align . group . vsep . punctuate (ann comma) $
1688 map (prettySe (decD d) startPrec bnd) elts
1689 where ann = case pun of
1691 IsType -> annName pairTy
1692 IsTerm -> annName pairCon
1693 prettySe d p bnd (PDPair _ _ pun l t r) =
1697 annotated (text "**") <+>
1698 prettySe (decD d) startPrec (addBinding bnd) r <>
1700 where annotated = case pun of
1701 IsType -> annName sigmaTy
1702 IsTerm -> annName sigmaCon
1704 (left, addBinding) = case (l, pun) of
1705 (PRef _ _ n, IsType) -> (bindingOf n False <+> text ":" <+> prettySe (decD d) startPrec bnd t, ((n, False) :))
1706 _ -> (prettySe (decD d) startPrec bnd l, id)
1707 prettySe d p bnd (PAlternative ns a as) =
1708 lparen <> text "|" <> prettyAs <> text "|" <> rparen
1711 foldr (\l -> \r -> l <+> text "," <+> r) empty $ map (depth d . prettySe (decD d) startPrec bnd) as
1712 prettySe d p bnd (PType _) = annotate (AnnType "Type" "The type of types") $ text "Type"
1713 prettySe d p bnd (PUniverse u) = annotate (AnnType (show u) "The type of unique types") $ text (show u)
1714 prettySe d p bnd (PConstant _ c) = annotate (AnnConst c) (text (show c))
1715 -- XXX: add pretty for tactics
1716 prettySe d p bnd (PProof ts) =
1717 kwd "proof" <+> lbrace <> ellipsis <> rbrace
1718 prettySe d p bnd (PTactics ts) =
1719 kwd "tactics" <+> lbrace <> ellipsis <> rbrace
1720 prettySe d p bnd (PMetavar _ n) = annotate (AnnName n (Just MetavarOutput) Nothing Nothing) $ text "?" <> pretty n
1721 prettySe d p bnd (PReturn f) = kwd "return"
1722 prettySe d p bnd PImpossible = kwd "impossible"
1723 prettySe d p bnd Placeholder = text "_"
1724 prettySe d p bnd (PDoBlock dos) =
1725 bracket p startPrec $
1726 kwd "do" <+> align (vsep (map (group . align . hang 2) (ppdo bnd dos)))
1727 where ppdo bnd (DoExp _ tm:dos) = prettySe (decD d) startPrec bnd tm : ppdo bnd dos
1728 ppdo bnd (DoBind _ bn _ tm : dos) =
1729 (prettyBindingOf bn False <+> text "<-" <+>
1730 group (align (hang 2 (prettySe (decD d) startPrec bnd tm)))) :
1731 ppdo ((bn, False):bnd) dos
1732 ppdo bnd (DoBindP _ _ _ _ : dos) = -- ok because never made by delab
1733 text "no pretty printer for pattern-matching do binding" :
1735 ppdo bnd (DoLet _ ln _ ty v : dos) =
1736 (kwd "let" <+> prettyBindingOf ln False <+>
1737 (if ty /= Placeholder
1738 then colon <+> prettySe (decD d) startPrec bnd ty <+> text "="
1740 group (align (hang 2 (prettySe (decD d) startPrec bnd v)))) :
1741 ppdo ((ln, False):bnd) dos
1742 ppdo bnd (DoLetP _ _ _ : dos) = -- ok because never made by delab
1743 text "no pretty printer for pattern-matching do binding" :
1746 prettySe d p bnd (PCoerced t) = prettySe d p bnd t
1747 prettySe d p bnd (PElabError s) = pretty s
1748 -- Quasiquote pprinting ignores bound vars
1749 prettySe d p bnd (PQuasiquote t Nothing) = text "`(" <> prettySe (decD d) p [] t <> text ")"
1750 prettySe d p bnd (PQuasiquote t (Just g)) = text "`(" <> prettySe (decD d) p [] t <+> colon <+> prettySe (decD d) p [] g <> text ")"
1751 prettySe d p bnd (PUnquote t) = text "~" <> prettySe (decD d) p bnd t
1752 prettySe d p bnd (PQuoteName n _) = text "`{" <> prettyName True (ppopt_impl ppo) bnd n <> text "}"
1753 prettySe d p bnd (PRunElab _ tm _) =
1754 bracket p funcAppPrec . group . align . hang 2 $
1756 prettySe (decD d) funcAppPrec bnd tm
1757 prettySe d p bnd (PConstSugar fc tm) = prettySe d p bnd tm -- should never occur, but harmless
1759 prettySe d p bnd _ = text "missing pretty-printer for term"
1761 prettyBindingOf :: Name -> Bool -> Doc OutputAnnotation
1762 prettyBindingOf n imp = annotate (AnnBoundName n imp) (text (display n))
1763 where display (UN n) = T.unpack n
1764 display (MN _ n) = T.unpack n
1765 -- If a namespace is specified on a binding form, we'd better show it regardless of the implicits settings
1766 display (NS n ns) = (concat . intersperse "." . map T.unpack . reverse) ns ++ "." ++ display n
1769 prettyArgS d bnd (PImp _ _ _ n tm) = prettyArgSi d bnd (n, tm)
1770 prettyArgS d bnd (PExp _ _ _ tm) = prettyArgSe d bnd tm
1771 prettyArgS d bnd (PConstraint _ _ _ tm) = prettyArgSc d bnd tm
1772 prettyArgS d bnd (PTacImplicit _ _ n _ tm) = prettyArgSti d bnd (n, tm)
1774 prettyArgSe d bnd arg = prettySe d (funcAppPrec + 1) bnd arg
1775 prettyArgSi d bnd (n, val) = lbrace <> pretty n <+> text "=" <+> prettySe (decD d) startPrec bnd val <> rbrace
1776 prettyArgSc d bnd val = lbrace <> lbrace <> prettySe (decD d) startPrec bnd val <> rbrace <> rbrace
1777 prettyArgSti d bnd (n, val) = lbrace <> kwd "auto" <+> pretty n <+> text "=" <+> prettySe (decD d) startPrec bnd val <> rbrace
1779 annName :: Name -> Doc OutputAnnotation -> Doc OutputAnnotation
1780 annName n = annotate (AnnName n Nothing Nothing Nothing)
1782 opStr :: Name -> String
1783 opStr (NS n _) = opStr n
1784 opStr (UN n) = T.unpack n
1786 slist' :: Maybe Int -> Int -> [(Name, Bool)] -> PTerm -> Maybe [Doc OutputAnnotation]
1787 slist' (Just d) _ _ _ | d <= 0 = Nothing
1789 | containsHole e = Nothing
1790 slist' d p bnd (PApp _ (PRef _ _ nil) _)
1791 | not (ppopt_impl ppo) && nsroot nil == sUN "Nil" = Just []
1792 slist' d p bnd (PRef _ _ nil)
1793 | not (ppopt_impl ppo) && nsroot nil == sUN "Nil" = Just []
1794 slist' d p bnd (PApp _ (PRef _ _ cons) args)
1795 | nsroot cons == sUN "::",
1796 (PExp {getTm=tl}):(PExp {getTm=hd}):imps <- reverse args,
1798 Just tl' <- slist' (decD d) p bnd tl
1799 = Just (prettySe d startPrec bnd hd : tl')
1801 isImp (PImp {}) = True
1803 slist' _ _ _ tm = Nothing
1805 slist d p bnd e | Just es <- slist' d p bnd e = Just $
1807 [] -> annotate (AnnData "" "") $ text "[]"
1808 [x] -> enclose left right . group $ x
1809 xs -> enclose left right .
1810 align . group . vsep .
1811 punctuate comma $ xs
1812 where left = (annotate (AnnData "" "") (text "["))
1813 right = (annotate (AnnData "" "") (text "]"))
1814 comma = (annotate (AnnData "" "") (text ","))
1815 slist _ _ _ _ = Nothing
1817 pairElts :: PTerm -> Maybe [PTerm]
1818 pairElts (PPair _ _ _ x y) | Just elts <- pairElts y = Just (x:elts)
1819 | otherwise = Just [x, y]
1820 pairElts _ = Nothing
1822 natns = "Prelude.Nat."
1824 snat :: Maybe Int -> Int -> PTerm -> Maybe Integer
1825 snat (Just x) _ _ | x <= 0 = Nothing
1826 snat d p (PRef _ _ z)
1827 | show z == (natns++"Z") || show z == "Z" = Just 0
1828 snat d p (PApp _ s [PExp {getTm=n}])
1829 | show s == (natns++"S") || show s == "S",
1830 Just n' <- snat (decD d) p n
1832 snat _ _ _ = Nothing
1834 bracket outer inner doc
1835 | outer > inner = lparen <> doc <> rparen
1838 ellipsis = text "..."
1841 depth (Just d) = if d <= 0 then const (ellipsis) else id
1843 decD = fmap (\x -> x - 1)
1845 kwd = annotate AnnKeyword . text
1847 fixities :: M.Map String Fixity
1848 fixities = M.fromList [(s, f) | (Fix f s) <- infixes]
1850 getFixity :: String -> Maybe Fixity
1851 getFixity = flip M.lookup fixities
1853-- | Strip away namespace information
1854basename :: Name -> Name
1855basename (NS n _) = basename n
1858-- | Determine whether a name was the one inserted for a hole or
1859-- guess by the delaborator
1860isHoleName :: Name -> Bool
1861isHoleName (UN n) = n == T.pack "[__]"
1864-- | Check whether a PTerm has been delaborated from a Term containing a Hole or Guess
1865containsHole :: PTerm -> Bool
1866containsHole pterm = or [isHoleName n | PRef _ _ n <- take 1000 $ universe pterm]
1868-- | Pretty-printer helper for names that attaches the correct annotations
1870 :: Bool -- ^^ whether the name should be parenthesised if it is an infix operator
1871 -> Bool -- ^^ whether to show namespaces
1872 -> [(Name, Bool)] -- ^^ the current bound variables and whether they are implicit
1873 -> Name -- ^^ the name to pprint
1874 -> Doc OutputAnnotation
1875prettyName infixParen showNS bnd n
1876 | (MN _ s) <- n, isPrefixOf "_" $ T.unpack s = text "_"
1877 | (UN n') <- n, T.unpack n' == "_" = text "_"
1878 | Just imp <- lookup n bnd = annotate (AnnBoundName n imp) fullName
1879 | otherwise = annotate (AnnName n Nothing Nothing Nothing) fullName
1880 where fullName = text nameSpace <> parenthesise (text (baseName n))
1881 baseName (UN n) = T.unpack n
1882 baseName (NS n ns) = baseName n
1883 baseName (MN i s) = T.unpack s
1884 baseName other = show other
1885 nameSpace = case n of
1886 (NS n' ns) -> if showNS then (concatMap (++ ".") . map T.unpack . reverse) ns else ""
1888 isInfix = case baseName n of
1890 (c : _) -> not (isAlpha c)
1891 parenthesise = if isInfix && infixParen then enclose lparen rparen else id
1894showCImp :: PPOption -> PClause -> Doc OutputAnnotation
1895showCImp ppo (PClause _ n l ws r w)
1896 = prettyImp ppo l <+> showWs ws <+> text "=" <+> prettyImp ppo r
1897 <+> text "where" <+> text (show w)
1900 showWs (x : xs) = text "|" <+> prettyImp ppo x <+> showWs xs
1901showCImp ppo (PWith _ n l ws r pn w)
1902 = prettyImp ppo l <+> showWs ws <+> text "with" <+> prettyImp ppo r
1903 <+> braces (text (show w))
1906 showWs (x : xs) = text "|" <+> prettyImp ppo x <+> showWs xs
1909showDImp :: PPOption -> PData -> Doc OutputAnnotation
1910showDImp ppo (PDatadecl n nfc ty cons)
1911 = text "data" <+> text (show n) <+> colon <+> prettyImp ppo ty <+> text "where" <$>
1912 (indent 2 $ vsep (map (\ (_, _, n, _, t, _, _) -> pipe <+> prettyName True False [] n <+> colon <+> prettyImp ppo t) cons))
1914showDecls :: PPOption -> [PDecl] -> Doc OutputAnnotation
1915showDecls o ds = vsep (map (showDeclImp o) ds)
1917showDeclImp _ (PFix _ f ops) = text (show f) <+> cat (punctuate (text ",") (map text ops))
1918showDeclImp o (PTy _ _ _ _ _ n _ t) = text "tydecl" <+> text (showCG n) <+> colon <+> prettyImp o t
1919showDeclImp o (PClauses _ _ n cs) = text "pat" <+> text (showCG n) <+> text "\t" <+>
1920 indent 2 (vsep (map (showCImp o) cs))
1921showDeclImp o (PData _ _ _ _ _ d) = showDImp o { ppopt_impl = True } d
1922showDeclImp o (PParams _ ns ps) = text "params" <+> braces (text (show ns) <> line <> showDecls o ps <> line)
1923showDeclImp o (PNamespace n fc ps) = text "namespace" <+> text n <> braces (line <> showDecls o ps <> line)
1924showDeclImp _ (PSyntax _ syn) = text "syntax" <+> text (show syn)
1925showDeclImp o (PClass _ _ _ cs n _ ps _ _ ds _ _)
1926 = text "class" <+> text (show cs) <+> text (show n) <+> text (show ps) <> line <> showDecls o ds
1927showDeclImp o (PInstance _ _ _ _ cs n _ _ t _ ds)
1928 = text "instance" <+> text (show cs) <+> text (show n) <+> prettyImp o t <> line <> showDecls o ds
1929showDeclImp _ _ = text "..."
1930-- showDeclImp (PImport o) = "import " ++ o
1932getImps :: [PArg] -> [(Name, PTerm)]
1934getImps (PImp _ _ _ n tm : xs) = (n, tm) : getImps xs
1935getImps (_ : xs) = getImps xs
1937getExps :: [PArg] -> [PTerm]
1939getExps (PExp _ _ _ tm : xs) = tm : getExps xs
1940getExps (_ : xs) = getExps xs
1942getShowArgs :: [PArg] -> [PArg]
1944getShowArgs (e@(PExp _ _ _ tm) : xs) = e : getShowArgs xs
1945getShowArgs (e : xs) | AlwaysShow `elem` argopts e = e : getShowArgs xs
1946 | PImp _ _ _ _ tm <- e
1947 , containsHole tm = e : getShowArgs xs
1948getShowArgs (_ : xs) = getShowArgs xs
1950getConsts :: [PArg] -> [PTerm]
1952getConsts (PConstraint _ _ _ tm : xs) = tm : getConsts xs
1953getConsts (_ : xs) = getConsts xs
1955getAll :: [PArg] -> [PTerm]
1960showName :: Maybe IState -- ^^ the Idris state, for information about names and colours
1961 -> [(Name, Bool)] -- ^^ the bound variables and whether they're implicit
1962 -> PPOption -- ^^ pretty printing options
1963 -> Bool -- ^^ whether to colourise
1964 -> Name -- ^^ the term to show
1966showName ist bnd ppo colour n = case ist of
1967 Just i -> if colour then colourise n (idris_colourTheme i) else showbasic n
1968 Nothing -> showbasic n
1969 where name = if ppopt_impl ppo then show n else showbasic n
1970 showbasic n@(UN _) = showCG n
1971 showbasic (MN i s) = str s
1972 showbasic (NS n s) = showSep "." (map str (reverse s)) ++ "." ++ showbasic n
1973 showbasic (SN s) = show s
1975 colourise n t = let ctxt' = fmap tt_ctxt ist in
1978 Just ctxt | Just impl <- lookup n bnd -> if impl then colouriseImplicit t name
1979 else colouriseBound t name
1980 | isDConName n ctxt -> colouriseData t name
1981 | isFnName n ctxt -> colouriseFun t name
1982 | isTConName n ctxt -> colouriseType t name
1983 -- The assumption is that if a name is not bound and does not exist in the
1984 -- global context, then we're somewhere in which implicit info has been lost
1985 -- (like error messages). Thus, unknown vars are colourised as implicits.
1986 | otherwise -> colouriseImplicit t name
1988showTm :: IState -- ^^ the Idris state, for information about identifiers and colours
1989 -> PTerm -- ^^ the term to show
1991showTm ist = displayDecorated (consoleDecorate ist) .
1992 renderPretty 0.8 100000 .
1993 prettyImp (ppOptionIst ist)
1995-- | Show a term with implicits, no colours
1996showTmImpls :: PTerm -> String
1997showTmImpls = flip (displayS . renderCompact . prettyImp verbosePPOption) ""
2001instance Sized PTerm where
2002 size (PQuote rawTerm) = size rawTerm
2003 size (PRef fc _ name) = size name
2004 size (PLam fc name _ ty bdy) = 1 + size ty + size bdy
2005 size (PPi plicity name fc ty bdy) = 1 + size ty + size fc + size bdy
2006 size (PLet fc name nfc ty def bdy) = 1 + size ty + size def + size bdy
2007 size (PTyped trm ty) = 1 + size trm + size ty
2008 size (PApp fc name args) = 1 + size args
2009 size (PAppBind fc name args) = 1 + size args
2010 size (PCase fc trm bdy) = 1 + size trm + size bdy
2011 size (PIfThenElse fc c t f) = 1 + sum (map size [c, t, f])
2012 size (PTrue fc _) = 1
2013 size (PResolveTC fc) = 1
2014 size (PRewrite fc left right _) = 1 + size left + size right
2015 size (PPair fc _ _ left right) = 1 + size left + size right
2016 size (PDPair fs _ _ left ty right) = 1 + size left + size ty + size right
2017 size (PAlternative _ a alts) = 1 + size alts
2018 size (PHidden hidden) = size hidden
2019 size (PUnifyLog tm) = size tm
2020 size (PDisamb _ tm) = size tm
2021 size (PNoImplicits tm) = size tm
2023 size (PUniverse _) = 1
2024 size (PConstant fc const) = 1 + size fc + size const
2025 size Placeholder = 1
2026 size (PDoBlock dos) = 1 + size dos
2027 size (PIdiom fc term) = 1 + size term
2028 size (PReturn fc) = 1
2029 size (PMetavar _ name) = 1
2030 size (PProof tactics) = size tactics
2031 size (PElabError err) = size err
2032 size PImpossible = 1
2035getPArity :: PTerm -> Int
2036getPArity (PPi _ _ _ _ sc) = 1 + getPArity sc
2039-- Return all names, free or globally bound, in the given term.
2041allNamesIn :: PTerm -> [Name]
2042allNamesIn tm = nub $ ni [] tm
2043 where -- TODO THINK added niTacImp, but is it right?
2045 | not (n `elem` env) = [n]
2046 ni env (PPatvar _ n) = [n]
2047 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
2048 ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
2049 ni env (PCase _ c os) = ni env c ++ concatMap (ni env) (map snd os)
2050 ni env (PIfThenElse _ c t f) = ni env c ++ ni env t ++ ni env f
2051 ni env (PLam fc n _ ty sc) = ni env ty ++ ni (n:env) sc
2052 ni env (PPi p n _ ty sc) = niTacImp env p ++ ni env ty ++ ni (n:env) sc
2053 ni env (PLet _ n _ ty val sc) = ni env ty ++ ni env val ++ ni (n:env) sc
2054 ni env (PHidden tm) = ni env tm
2055 ni env (PRewrite _ l r _) = ni env l ++ ni env r
2056 ni env (PTyped l r) = ni env l ++ ni env r
2057 ni env (PPair _ _ _ l r) = ni env l ++ ni env r
2058 ni env (PDPair _ _ _ (PRef _ _ n) Placeholder r) = n : ni env r
2059 ni env (PDPair _ _ _ (PRef _ _ n) t r) = ni env t ++ ni (n:env) r
2060 ni env (PDPair _ _ _ l t r) = ni env l ++ ni env t ++ ni env r
2061 ni env (PAlternative ns a ls) = concatMap (ni env) ls
2062 ni env (PUnifyLog tm) = ni env tm
2063 ni env (PDisamb _ tm) = ni env tm
2064 ni env (PNoImplicits tm) = ni env tm
2067 niTacImp env (TacImp _ _ scr) = ni env scr
2071-- Return all names defined in binders in the given term
2072boundNamesIn :: PTerm -> [Name]
2073boundNamesIn tm = S.toList (ni S.empty tm)
2074 where -- TODO THINK Added niTacImp, but is it right?
2075 ni set (PApp _ f as) = niTms (ni set f) (map getTm as)
2076 ni set (PAppBind _ f as) = niTms (ni set f) (map getTm as)
2077 ni set (PCase _ c os) = niTms (ni set c) (map snd os)
2078 ni set (PIfThenElse _ c t f) = niTms set [c, t, f]
2079 ni set (PLam fc n _ ty sc) = S.insert n $ ni (ni set ty) sc
2080 ni set (PLet fc n nfc ty val sc) = S.insert n $ ni (ni (ni set ty) val) sc
2081 ni set (PPi p n _ ty sc) = niTacImp (S.insert n $ ni (ni set ty) sc) p
2082 ni set (PRewrite _ l r _) = ni (ni set l) r
2083 ni set (PTyped l r) = ni (ni set l) r
2084 ni set (PPair _ _ _ l r) = ni (ni set l) r
2085 ni set (PDPair _ _ _ (PRef _ _ n) t r) = ni (ni set t) r
2086 ni set (PDPair _ _ _ l t r) = ni (ni (ni set l) t) r
2087 ni set (PAlternative ns a as) = niTms set as
2088 ni set (PHidden tm) = ni set tm
2089 ni set (PUnifyLog tm) = ni set tm
2090 ni set (PDisamb _ tm) = ni set tm
2091 ni set (PNoImplicits tm) = ni set tm
2095 niTms set (x : xs) = niTms (ni set x) xs
2097 niTacImp set (TacImp _ _ scr) = ni set scr
2098 niTacImp set _ = set
2100-- Return names which are valid implicits in the given term (type).
2101implicitNamesIn :: [Name] -> IState -> PTerm -> [Name]
2102implicitNamesIn uvars ist tm = nub $ ni [] tm
2105 | not (n `elem` env)
2106 = case lookupTy n (tt_ctxt ist) of
2108 _ -> if n `elem` uvars then [n] else []
2109 ni env (PApp _ f@(PRef _ _ n) as)
2110 | n `elem` uvars = ni env f ++ concatMap (ni env) (map getTm as)
2111 | otherwise = concatMap (ni env) (map getTm as)
2112 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
2113 ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
2114 ni env (PCase _ c os) = ni env c ++
2115 -- names in 'os', not counting the names bound in the cases
2116 (nub (concatMap (ni env) (map snd os))
2117 \\ nub (concatMap (ni env) (map fst os)))
2118 ni env (PIfThenElse _ c t f) = concatMap (ni env) [c, t, f]
2119 ni env (PLam fc n _ ty sc) = ni env ty ++ ni (n:env) sc
2120 ni env (PPi p n _ ty sc) = ni env ty ++ ni (n:env) sc
2121 ni env (PRewrite _ l r _) = ni env l ++ ni env r
2122 ni env (PTyped l r) = ni env l ++ ni env r
2123 ni env (PPair _ _ _ l r) = ni env l ++ ni env r
2124 ni env (PDPair _ _ _ (PRef _ _ n) t r) = ni env t ++ ni (n:env) r
2125 ni env (PDPair _ _ _ l t r) = ni env l ++ ni env t ++ ni env r
2126 ni env (PAlternative ns a as) = concatMap (ni env) as
2127 ni env (PHidden tm) = ni env tm
2128 ni env (PUnifyLog tm) = ni env tm
2129 ni env (PDisamb _ tm) = ni env tm
2130 ni env (PNoImplicits tm) = ni env tm
2133-- Return names which are free in the given term.
2134namesIn :: [(Name, PTerm)] -> IState -> PTerm -> [Name]
2135namesIn uvars ist tm = nub $ ni [] tm
2138 | not (n `elem` env)
2139 = case lookupTy n (tt_ctxt ist) of
2141 _ -> if n `elem` (map fst uvars) then [n] else []
2142 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
2143 ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
2144 ni env (PCase _ c os) = ni env c ++
2145 -- names in 'os', not counting the names bound in the cases
2146 (nub (concatMap (ni env) (map snd os))
2147 \\ nub (concatMap (ni env) (map fst os)))
2148 ni env (PIfThenElse _ c t f) = concatMap (ni env) [c, t, f]
2149 ni env (PLam fc n nfc ty sc) = ni env ty ++ ni (n:env) sc
2150 ni env (PPi p n _ ty sc) = niTacImp env p ++ ni env ty ++ ni (n:env) sc
2151 ni env (PRewrite _ l r _) = ni env l ++ ni env r
2152 ni env (PTyped l r) = ni env l ++ ni env r
2153 ni env (PPair _ _ _ l r) = ni env l ++ ni env r
2154 ni env (PDPair _ _ _ (PRef _ _ n) t r) = ni env t ++ ni (n:env) r
2155 ni env (PDPair _ _ _ l t r) = ni env l ++ ni env t ++ ni env r
2156 ni env (PAlternative ns a as) = concatMap (ni env) as
2157 ni env (PHidden tm) = ni env tm
2158 ni env (PUnifyLog tm) = ni env tm
2159 ni env (PDisamb _ tm) = ni env tm
2160 ni env (PNoImplicits tm) = ni env tm
2163 niTacImp env (TacImp _ _ scr) = ni env scr
2166-- Return which of the given names are used in the given term.
2168usedNamesIn :: [Name] -> IState -> PTerm -> [Name]
2169usedNamesIn vars ist tm = nub $ ni [] tm
2170 where -- TODO THINK added niTacImp, but is it right?
2172 | n `elem` vars && not (n `elem` env)
2173 = case lookupDefExact n (tt_ctxt ist) of
2176 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
2177 ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
2178 ni env (PCase _ c os) = ni env c ++ concatMap (ni env) (map snd os)
2179 ni env (PIfThenElse _ c t f) = concatMap (ni env) [c, t, f]
2180 ni env (PLam fc n _ ty sc) = ni env ty ++ ni (n:env) sc
2181 ni env (PPi p n _ ty sc) = niTacImp env p ++ ni env ty ++ ni (n:env) sc
2182 ni env (PRewrite _ l r _) = ni env l ++ ni env r
2183 ni env (PTyped l r) = ni env l ++ ni env r
2184 ni env (PPair _ _ _ l r) = ni env l ++ ni env r
2185 ni env (PDPair _ _ _ (PRef _ _ n) t r) = ni env t ++ ni (n:env) r
2186 ni env (PDPair _ _ _ l t r) = ni env l ++ ni env t ++ ni env r
2187 ni env (PAlternative ns a as) = concatMap (ni env) as
2188 ni env (PHidden tm) = ni env tm
2189 ni env (PUnifyLog tm) = ni env tm
2190 ni env (PDisamb _ tm) = ni env tm
2191 ni env (PNoImplicits tm) = ni env tm
2194 niTacImp env (TacImp _ _ scr) = ni env scr
2197-- Return the list of inaccessible (= dotted) positions for a name.
2198getErasureInfo :: IState -> Name -> [Int]
2199getErasureInfo ist n =
2200 case lookupCtxtExact n (idris_optimisation ist) of
2201 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