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_pinames :: Bool -- ^^ whether to show names in pi bindings
125 , ppopt_depth :: Maybe Int
128data Optimisation = PETransform -- partial eval and associated transforms
131defaultOptimise = [PETransform]
133-- | Pretty printing options with default verbosity.
134defaultPPOption :: PPOption
135defaultPPOption = PPOption { ppopt_impl = False,
136 ppopt_pinames = False,
137 ppopt_depth = Just 200 }
139-- | Pretty printing options with the most verbosity.
140verbosePPOption :: PPOption
141verbosePPOption = PPOption { ppopt_impl = True,
142 ppopt_pinames = True,
143 ppopt_depth = Just 200 }
145-- | Get pretty printing options from the big options record.
146ppOption :: IOption -> PPOption
147ppOption opt = PPOption {
148 ppopt_impl = opt_showimp opt,
149 ppopt_pinames = False,
150 ppopt_depth = opt_printdepth opt
153-- | Get pretty printing options from an idris state record.
154ppOptionIst :: IState -> PPOption
155ppOptionIst = ppOption . idris_options
157data LanguageExt = TypeProviders | ErrorReflection deriving (Show, Eq, Read, Ord)
159-- | The output mode in use
160data OutputMode = RawOutput Handle -- ^ Print user output directly to the handle
161 | IdeMode Integer Handle -- ^ Send IDE output for some request ID to the handle
164-- | How wide is the console?
165data ConsoleWidth = InfinitelyWide -- ^ Have pretty-printer assume that lines should not be broken
166 | ColsWide Int -- ^ Manually specified - must be positive
167 | AutomaticWidth -- ^ Attempt to determine width, or 80 otherwise
171-- | The global state used in the Idris monad
172data IState = IState {
173 tt_ctxt :: Context, -- ^ All the currently defined names and their terms
174 idris_constraints :: S.Set ConstraintFC,
175 -- ^ A list of universe constraints and their corresponding source locations
176 idris_infixes :: [FixDecl], -- ^ Currently defined infix operators
177 idris_implicits :: Ctxt [PArg],
178 idris_statics :: Ctxt [Bool],
179 idris_classes :: Ctxt ClassInfo,
180 idris_dsls :: Ctxt DSL,
181 idris_optimisation :: Ctxt OptInfo,
182 idris_datatypes :: Ctxt TypeInfo,
183 idris_namehints :: Ctxt [Name],
184 idris_patdefs :: Ctxt ([([Name], Term, Term)], [PTerm]), -- not exported
185 -- ^ list of lhs/rhs, and a list of missing clauses
186 idris_flags :: Ctxt [FnOpt],
187 idris_callgraph :: Ctxt CGInfo, -- name, args used in each pos
188 idris_calledgraph :: Ctxt [Name],
189 idris_docstrings :: Ctxt (Docstring DocTerm, [(Name, Docstring DocTerm)]),
190 idris_moduledocs :: Ctxt (Docstring DocTerm),
191 -- ^ module documentation is saved in a special MN so the context
192 -- mechanism can be used for disambiguation
193 idris_tyinfodata :: Ctxt TIData,
194 idris_fninfo :: Ctxt FnInfo,
195 idris_transforms :: Ctxt [(Term, Term)],
196 idris_autohints :: Ctxt [Name],
197 idris_totcheck :: [(FC, Name)], -- names to check totality on
198 idris_defertotcheck :: [(FC, Name)], -- names to check at the end
199 idris_totcheckfail :: [(FC, String)],
200 idris_options :: IOption,
202 idris_lineapps :: [((FilePath, Int), PTerm)],
203 -- ^ Full application LHS on source line
204 idris_metavars :: [(Name, (Maybe Name, Int, [Name], Bool))],
205 -- ^ The currently defined but not proven metavariables. The Int
206 -- is the number of vars to display as a context, the Maybe Name
207 -- is its top-level function, the [Name] is the list of local variables
208 -- available for proof search and the Bool is whether :p is
210 idris_coercions :: [Name],
211 idris_errRev :: [(Term, Term)],
212 syntax_rules :: SyntaxRules,
213 syntax_keywords :: [String],
214 imported :: [FilePath], -- ^ The imported modules
215 idris_scprims :: [(Name, (Int, PrimFn))],
216 idris_objs :: [(Codegen, FilePath)],
217 idris_libs :: [(Codegen, String)],
218 idris_cgflags :: [(Codegen, String)],
219 idris_hdrs :: [(Codegen, String)],
220 idris_imported :: [(FilePath, Bool)], -- ^ Imported ibc file names, whether public
221 proof_list :: [(Name, (Bool, [String]))],
223 parserWarnings :: [(FC, Err)],
224 lastParse :: Maybe Name,
225 indent_stack :: [Int],
226 brace_stack :: [Maybe Int],
227 lastTokenSpan :: Maybe FC, -- ^ What was the span of the latest token parsed?
228 idris_parsedSpan :: Maybe FC,
229 hide_list :: [(Name, Maybe Accessibility)],
230 default_access :: Accessibility,
231 default_total :: Bool,
232 ibc_write :: [IBCWrite],
233 compiled_so :: Maybe String,
234 idris_dynamic_libs :: [DynamicLib],
235 idris_language_extensions :: [LanguageExt],
236 idris_outputmode :: OutputMode,
237 idris_colourRepl :: Bool,
238 idris_colourTheme :: ColourTheme,
239 idris_errorhandlers :: [Name], -- ^ Global error handlers
240 idris_nameIdx :: (Int, Ctxt (Int, Name)),
241 idris_function_errorhandlers :: Ctxt (M.Map Name (S.Set Name)), -- ^ Specific error handlers
242 module_aliases :: M.Map [T.Text] [T.Text],
243 idris_consolewidth :: ConsoleWidth, -- ^ How many chars wide is the console?
244 idris_postulates :: S.Set Name,
245 idris_externs :: S.Set (Name, Int),
246 idris_erasureUsed :: [(Name, Int)], -- ^ Function/constructor name, argument position is used
247 idris_whocalls :: Maybe (M.Map Name [Name]),
248 idris_callswho :: Maybe (M.Map Name [Name]),
249 idris_repl_defs :: [Name], -- ^ List of names that were defined in the repl, and can be re-/un-defined
250 elab_stack :: [(Name, Bool)], -- ^ Stack of names currently being elaborated, Bool set if it's an instance
251 -- (instances appear twice; also as a funtion name)
252 idris_symbols :: M.Map Name Name, -- ^ Symbol table (preserves sharing of names)
253 idris_exports :: [Name], -- ^ Functions with ExportList
254 idris_highlightedRegions :: [(FC, OutputAnnotation)], -- ^ Highlighting information to output
255 idris_parserHighlights :: [(FC, OutputAnnotation)] -- ^ Highlighting information from the parser
258-- Required for parsers library, and therefore trifecta
259instance Show IState where
260 show = const "{internal state}"
262data SizeChange = Smaller | Same | Bigger | Unknown
265deriving instance Binary SizeChange
266deriving instance NFData SizeChange
269type SCGEntry = (Name, [Maybe (Int, SizeChange)])
270type UsageReason = (Name, Int) -- fn_name, its_arg_number
272data CGInfo = CGInfo { argsdef :: [Name],
273 calls :: [(Name, [[Name]])],
276 usedpos :: [(Int, [UsageReason])] }
279deriving instance Binary CGInfo
280deriving instance NFData CGInfo
283primDefs = [sUN "unsafePerformPrimIO",
284 sUN "mkLazyForeignPrim",
288-- information that needs writing for the current module's .ibc file
289data IBCWrite = IBCFix FixDecl
293 | IBCInstance Bool Bool Name Name
300 | IBCImport (Bool, FilePath) -- True = import public
301 | IBCImportDir FilePath
302 | IBCObj Codegen FilePath
303 | IBCLib Codegen String
304 | IBCCGFlag Codegen String
306 | IBCHeader Codegen String
307 | IBCAccess Name Accessibility
308 | IBCMetaInformation Name MetaInformation
309 | IBCTotal Name Totality
310 | IBCFlags Name [FnOpt]
311 | IBCFnInfo Name FnInfo
312 | IBCTrans Name (Term, Term)
313 | IBCErrRev (Term, Term)
317 | IBCDef Name -- i.e. main context
318 | IBCNameHint (Name, Name)
319 | IBCLineApp FilePath Int PTerm
320 | IBCErrorHandler Name
321 | IBCFunctionErrorHandler Name Name Name
323 | IBCExtern (Name, Int)
324 | IBCTotCheckErr FC String
326 | IBCModDocs Name -- ^ The name is the special name used to track module docs
327 | IBCUsage (Name, Int)
329 | IBCAutoHint Name Name
332-- | The initial state for the compiler
334idrisInit = IState initContext S.empty []
335 emptyContext emptyContext emptyContext emptyContext
336 emptyContext emptyContext emptyContext emptyContext
337 emptyContext emptyContext emptyContext emptyContext
338 emptyContext emptyContext emptyContext emptyContext
340 [] [] [] defaultOpts 6 [] [] [] [] emptySyntaxRules [] [] [] [] [] [] []
341 [] [] Nothing [] Nothing [] [] Nothing Nothing [] Hidden False [] Nothing [] []
342 (RawOutput stdout) True defaultTheme [] (0, emptyContext) emptyContext M.empty
343 AutomaticWidth S.empty S.empty [] Nothing Nothing [] [] M.empty [] [] []
345-- | The monad for the main REPL - reading and processing files and updating
346-- global state (hence the IO inner monad).
347--type Idris = WriterT [Either String (IO ())] (State IState a))
348type Idris = StateT IState (ExceptT Err IO)
350catchError :: Idris a -> (Err -> Idris a) -> Idris a
351catchError = liftCatch catchE
353throwError :: Err -> Idris a
354throwError = Trans.lift . throwE
356-- Commands in the REPL
358data Codegen = Via String
367deriving instance NFData Codegen
370data HowMuchDocs = FullDocs | OverviewDocs
376 | NewDefn [PDecl] -- ^ Each 'PDecl' should be either a type declaration (at most one) or a clause defining the same name.
380 | DocStr (Either Name Const) HowMuchDocs
383 | Load FilePath (Maybe Int) -- up to maximum line number
384 | ChangeDirectory FilePath
387 | Compile Codegen String
391 | Prove Bool Name -- ^ If false, use prover, if true, use elab shell
392 | AddProof (Maybe Name)
403 | DynamicLink FilePath
406 | Search [String] PTerm
407 | CaseSplitAt Bool Int Name
408 | AddClauseFrom Bool Int Name
409 | AddProofClauseFrom Bool Int Name
410 | AddMissing Bool Int Name
411 | MakeWith Bool Int Name
412 | MakeCase Bool Int Name
413 | MakeLemma Bool Int Name
414 | DoProofSearch Bool -- update file
415 Bool -- recursive search
417 Name -- top level name
422 | SetColour ColourType IdrisColour
426 | SetConsoleWidth ConsoleWidth
427 | SetPrinterDepth (Maybe Int)
428 | Apropos [String] String
432 | MakeDoc String -- IdrisDoc
435 | PPrint OutputFmt Int PTerm
437 -- Debugging commands
439 | DebugUnify PTerm PTerm
441data OutputFmt = HTMLOutput | LaTeXOutput
443data Opt = Filename String
455 | NoBuiltins -- only for the really primitive stuff!
471 | Port String -- REPL TCP port
479 | PkgMkDoc String -- IdrisDoc
489 | OutputTy OutputType
490 | Extension LanguageExt
491 | InterpretScript String
493 | TargetTriple String
496 | AddOpt Optimisation
497 | RemoveOpt Optimisation
500 | AutoWidth -- ^ Automatically adjust terminal width
501 | AutoSolve -- ^ Automatically issue "solve" tactic in interactive prover
502 | UseConsoleWidth ConsoleWidth
506data ElabShellCmd = EQED | EAbandon | EUndo | EProofState | EProofTerm
507 | EEval PTerm | ECheck PTerm | ESearch PTerm
508 | EDocStr (Either Name Const)
511-- Parsed declarations
513data Fixity = Infixl { prec :: Int }
514 | Infixr { prec :: Int }
515 | InfixN { prec :: Int }
516 | PrefixN { prec :: Int }
519deriving instance Binary Fixity
520deriving instance NFData Fixity
523instance Show Fixity where
524 show (Infixl i) = "infixl " ++ show i
525 show (Infixr i) = "infixr " ++ show i
526 show (InfixN i) = "infix " ++ show i
527 show (PrefixN i) = "prefix " ++ show i
529data FixDecl = Fix Fixity String
532instance Show FixDecl where
533 show (Fix f s) = show f ++ " " ++ s
536deriving instance Binary FixDecl
537deriving instance NFData FixDecl
540instance Ord FixDecl where
541 compare (Fix x _) (Fix y _) = compare (prec x) (prec y)
544data Static = Static | Dynamic
545 deriving (Show, Eq, Data, Typeable)
547deriving instance Binary Static
548deriving instance NFData Static
551-- Mark bindings with their explicitness, and laziness
552data Plicity = Imp { pargopts :: [ArgOpt],
555 pscoped :: Maybe ImplicitInfo -- Nothing, if top level
557 | Exp { pargopts :: [ArgOpt],
559 pparam :: Bool } -- this is a param (rather than index)
560 | Constraint { pargopts :: [ArgOpt],
562 | TacImp { pargopts :: [ArgOpt],
565 deriving (Show, Eq, Data, Typeable)
568deriving instance Binary Plicity
569deriving instance NFData Plicity
572is_scoped :: Plicity -> Maybe ImplicitInfo
573is_scoped (Imp _ _ _ s) = s
576impl = Imp [] Dynamic False Nothing
577forall_imp = Imp [] Dynamic False (Just (Impl False))
578forall_constraint = Imp [] Dynamic False (Just (Impl True))
579expl = Exp [] Dynamic False
580expl_param = Exp [] Dynamic True
581constraint = Constraint [] Static
582tacimpl t = TacImp [] Dynamic t
584data FnOpt = Inlinable -- always evaluate when simplifying
585 | TotalFn | PartialFn | CoveringFn
586 | Coinductive | AssertTotal
587 | Dictionary -- type class dictionary, eval only when
588 -- a function argument, and further evaluation resutls
589 | Implicit -- implicit coercion
590 | NoImplicit -- do not apply implicit coercions
591 | CExport String -- export, with a C name
592 | ErrorHandler -- ^^ an error handler for use with the ErrorReflection extension
593 | ErrorReverse -- ^^ attempt to reverse normalise before showing in error
594 | Reflection -- a reflecting function, compile-time only
595 | Specialise [(Name, Maybe Int)] -- specialise it, freeze these names
596 | Constructor -- Data constructor type
597 | AutoHint -- use in auto implicit search
598 | PEGenerated -- generated by partial evaluator
601deriving instance Binary FnOpt
602deriving instance NFData FnOpt
607inlinable :: FnOpts -> Bool
608inlinable = elem Inlinable
610dictionary :: FnOpts -> Bool
611dictionary = elem Dictionary
614-- | Type provider - what to provide
615data ProvideWhat' t = ProvTerm t t -- ^ the first is the goal type, the second is the term
616 | ProvPostulate t -- ^ goal type must be Type, so only term
617 deriving (Show, Eq, Functor)
619type ProvideWhat = ProvideWhat' PTerm
621-- | Top-level declarations such as compiler directives, definitions,
622-- datatypes and typeclasses.
624 = PFix FC Fixity [String] -- ^ Fixity declaration
625 | PTy (Docstring (Either Err PTerm)) [(Name, Docstring (Either Err PTerm))] SyntaxInfo FC FnOpts Name FC t -- ^ Type declaration (last FC is precise name location)
626 | PPostulate Bool -- external def if true
627 (Docstring (Either Err PTerm)) SyntaxInfo FC FC FnOpts Name t -- ^ Postulate, second FC is precise name location
628 | PClauses FC FnOpts Name [PClause' t] -- ^ Pattern clause
629 | PCAF FC Name t -- ^ Top level constant
630 | PData (Docstring (Either Err PTerm)) [(Name, Docstring (Either Err PTerm))] SyntaxInfo FC DataOpts (PData' t) -- ^ Data declaration.
631 | PParams FC [(Name, t)] [PDecl' t] -- ^ Params block
632 | PNamespace String FC [PDecl' t]
633 -- ^ New namespace, where FC is accurate location of the
634 -- namespace in the file
635 | PRecord (Docstring (Either Err PTerm)) SyntaxInfo FC DataOpts
637 FC -- Record name precise location
638 [(Name, FC, Plicity, t)] -- Parameters, where FC is precise name span
639 [(Name, Docstring (Either Err PTerm))] -- Param Docs
640 [((Maybe (Name, FC)), Plicity, t, Maybe (Docstring (Either Err PTerm)))] -- Fields
641 (Maybe (Name, FC)) -- Optional constructor name and location
642 (Docstring (Either Err PTerm)) -- Constructor doc
643 SyntaxInfo -- Constructor SyntaxInfo
644 -- ^ Record declaration
645 | PClass (Docstring (Either Err PTerm)) SyntaxInfo FC
646 [(Name, t)] -- constraints
648 FC -- accurate location of class name
649 [(Name, FC, t)] -- parameters and precise locations
650 [(Name, Docstring (Either Err PTerm))] -- parameter docstrings
651 [(Name, FC)] -- determining parameters and precise locations
652 [PDecl' t] -- declarations
653 (Maybe (Name, FC)) -- instance constructor name and location
654 (Docstring (Either Err PTerm)) -- instance constructor docs
655 -- ^ Type class: arguments are documentation, syntax info, source location, constraints,
656 -- class name, class name location, parameters, method declarations, optional constructor name
658 (Docstring (Either Err PTerm)) -- Instance docs
659 [(Name, Docstring (Either Err PTerm))] -- Parameter docs
661 FC [(Name, t)] -- constraints
663 FC -- precise location of class
665 t -- full instance type
666 (Maybe Name) -- explicit name
668 -- ^ Instance declaration: arguments are documentation, syntax info, source
669 -- location, constraints, class name, parameters, full instance
670 -- type, optional explicit name, and definitions
671 | PDSL Name (DSL' t) -- ^ DSL declaration
672 | PSyntax FC Syntax -- ^ Syntax definition
673 | PMutual FC [PDecl' t] -- ^ Mutual block
674 | PDirective Directive -- ^ Compiler directive.
675 | 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.
676 | PTransform FC Bool t t -- ^ Source-to-source transformation rule. If
677 -- bool is True, lhs and rhs must be convertible
680deriving instance Binary PDecl'
681deriving instance NFData PDecl'
684-- | The set of source directives
685data Directive = DLib Codegen String |
686 DLink Codegen String |
687 DFlag Codegen String |
688 DInclude Codegen String |
691 DAccess Accessibility |
694 DDynamicLibs [String] |
695 DNameHint Name FC [(Name, FC)] |
696 DErrorHandlers Name FC Name FC [(Name, FC)] |
697 DLanguage LanguageExt |
700-- | A set of instructions for things that need to happen in IState
701-- after a term elaboration when there's been reflected elaboration.
702data RDeclInstructions = RTyDeclInstrs Name FC [PArg] Type
703 | RClausesInstrs Name [([Name], Term, Term)]
704 | RAddInstance Name Name
706-- | For elaborator state
707data EState = EState {
708 case_decls :: [(Name, PDecl)],
709 delayed_elab :: [(Int, Elab' EState ())],
710 new_tyDecls :: [RDeclInstructions],
711 highlighting :: [(FC, OutputAnnotation)]
715initEState = EState [] [] [] []
717type ElabD a = Elab' EState a
719highlightSource :: FC -> OutputAnnotation -> ElabD ()
720highlightSource fc annot =
721 updateAux (\aux -> aux { highlighting = (fc, annot) : highlighting aux })
723-- | One clause of a top-level definition. Term arguments to constructors are:
725-- 1. The whole application (missing for PClauseR and PWithR because they're within a "with" clause)
727-- 2. The list of extra 'with' patterns
729-- 3. The right-hand side
731-- 4. The where block (PDecl' t)
733data PClause' t = PClause FC Name t [t] t [PDecl' t] -- ^ A normal top-level definition.
734 | PWith FC Name t [t] t (Maybe (Name, FC)) [PDecl' t]
735 | PClauseR FC [t] t [PDecl' t]
736 | PWithR FC [t] t (Maybe (Name, FC)) [PDecl' t]
739deriving instance Binary PClause'
740deriving instance NFData PClause'
744data PData' t = PDatadecl { d_name :: Name, -- ^ The name of the datatype
745 d_name_fc :: FC, -- ^ The precise location of the type constructor name
746 d_tcon :: t, -- ^ Type constructor
747 d_cons :: [(Docstring (Either Err PTerm), [(Name, Docstring (Either Err PTerm))], Name, FC, t, FC, [Name])] -- ^ Constructors
749 -- ^ Data declaration
750 | PLaterdecl { d_name :: Name, d_name_fc :: FC, d_tcon :: t }
751 -- ^ "Placeholder" for data whose constructors are defined later
754deriving instance Binary PData'
755deriving instance NFData PData'
758-- Handy to get a free function for applying PTerm -> PTerm functions
759-- across a program, by deriving Functor
761type PDecl = PDecl' PTerm
762type PData = PData' PTerm
763type PClause = PClause' PTerm
765-- get all the names declared in a decl
767declared :: PDecl -> [Name]
768declared (PFix _ _ _) = []
769declared (PTy _ _ _ _ _ n fc t) = [n]
770declared (PPostulate _ _ _ _ _ _ n t) = [n]
771declared (PClauses _ _ n _) = [] -- not a declaration
772declared (PCAF _ n _) = [n]
773declared (PData _ _ _ _ _ (PDatadecl n _ _ ts)) = n : map fstt ts
774 where fstt (_, _, a, _, _, _, _) = a
775declared (PData _ _ _ _ _ (PLaterdecl n _ _)) = [n]
776declared (PParams _ _ ds) = concatMap declared ds
777declared (PNamespace _ _ ds) = concatMap declared ds
778declared (PRecord _ _ _ _ n _ _ _ _ cn _ _) = n : map fst (maybeToList cn)
779declared (PClass _ _ _ _ n _ _ _ _ ms cn cd) = n : (map fst (maybeToList cn) ++ concatMap declared ms)
780declared (PInstance _ _ _ _ _ _ _ _ _ _ _) = []
781declared (PDSL n _) = [n]
782declared (PSyntax _ _) = []
783declared (PMutual _ ds) = concatMap declared ds
784declared (PDirective _) = []
787-- get the names declared, not counting nested parameter blocks
788tldeclared :: PDecl -> [Name]
789tldeclared (PFix _ _ _) = []
790tldeclared (PTy _ _ _ _ _ n _ t) = [n]
791tldeclared (PPostulate _ _ _ _ _ _ n t) = [n]
792tldeclared (PClauses _ _ n _) = [] -- not a declaration
793tldeclared (PRecord _ _ _ _ n _ _ _ _ cn _ _) = n : map fst (maybeToList cn)
794tldeclared (PData _ _ _ _ _ (PDatadecl n _ _ ts)) = n : map fstt ts
795 where fstt (_, _, a, _, _, _, _) = a
796tldeclared (PParams _ _ ds) = []
797tldeclared (PMutual _ ds) = concatMap tldeclared ds
798tldeclared (PNamespace _ _ ds) = concatMap tldeclared ds
799tldeclared (PClass _ _ _ _ n _ _ _ _ ms cn _) = n : (map fst (maybeToList cn) ++ concatMap tldeclared ms)
800tldeclared (PInstance _ _ _ _ _ _ _ _ _ _ _) = []
803defined :: PDecl -> [Name]
804defined (PFix _ _ _) = []
805defined (PTy _ _ _ _ _ n _ t) = []
806defined (PPostulate _ _ _ _ _ _ n t) = []
807defined (PClauses _ _ n _) = [n] -- not a declaration
808defined (PCAF _ n _) = [n]
809defined (PData _ _ _ _ _ (PDatadecl n _ _ ts)) = n : map fstt ts
810 where fstt (_, _, a, _, _, _, _) = a
811defined (PData _ _ _ _ _ (PLaterdecl n _ _)) = []
812defined (PParams _ _ ds) = concatMap defined ds
813defined (PNamespace _ _ ds) = concatMap defined ds
814defined (PRecord _ _ _ _ n _ _ _ _ cn _ _) = n : map fst (maybeToList cn)
815defined (PClass _ _ _ _ n _ _ _ _ ms cn _) = n : (map fst (maybeToList cn) ++ concatMap defined ms)
816defined (PInstance _ _ _ _ _ _ _ _ _ _ _) = []
817defined (PDSL n _) = [n]
818defined (PSyntax _ _) = []
819defined (PMutual _ ds) = concatMap defined ds
820defined (PDirective _) = []
823updateN :: [(Name, Name)] -> Name -> Name
824updateN ns n | Just n' <- lookup n ns = n'
827updateNs :: [(Name, Name)] -> PTerm -> PTerm
829updateNs ns t = mapPT updateRef t
830 where updateRef (PRef fc fcs f) = PRef fc fcs (updateN ns f)
833-- updateDNs :: [(Name, Name)] -> PDecl -> PDecl
835-- updateDNs ns (PTy s f n t) | Just n' <- lookup n ns = PTy s f n' t
836-- updateDNs ns (PClauses f n c) | Just n' <- lookup n ns = PClauses f n' (map updateCNs c)
837-- where updateCNs ns (PClause n l ts r ds)
838-- = PClause (updateN ns n) (fmap (updateNs ns) l)
839-- (map (fmap (updateNs ns)) ts)
840-- (fmap (updateNs ns) r)
841-- (map (updateDNs ns) ds)
844data PunInfo = IsType | IsTerm | TypeOrTerm deriving (Eq, Show, Data, Typeable)
846-- | High level language terms
847data PTerm = PQuote Raw -- ^ Inclusion of a core term into the high-level language
848 | 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.
849 | PInferRef FC [FC] Name -- ^ A name to be defined later
850 | PPatvar FC Name -- ^ A pattern variable
851 | PLam FC Name FC PTerm PTerm -- ^ A lambda abstraction. Second FC is name span.
852 | PPi Plicity Name FC PTerm PTerm -- ^ (n : t1) -> t2, where the FC is for the precise location of the variable
853 | PLet FC Name FC PTerm PTerm PTerm -- ^ A let binding (second FC is precise name location)
854 | PTyped PTerm PTerm -- ^ Term with explicit type
855 | PApp FC PTerm [PArg] -- ^ e.g. IO (), List Char, length x
856 | PAppImpl PTerm [ImplicitInfo] -- ^ Implicit argument application (introduced during elaboration only)
857 | PAppBind FC PTerm [PArg] -- ^ implicitly bound application
858 | PMatchApp FC Name -- ^ Make an application by type matching
859 | PIfThenElse FC PTerm PTerm PTerm -- ^ Conditional expressions - elaborated to an overloading of ifThenElse
860 | PCase FC PTerm [(PTerm, PTerm)] -- ^ A case expression. Args are source location, scrutinee, and a list of pattern/RHS pairs
861 | PTrue FC PunInfo -- ^ Unit type..?
862 | PResolveTC FC -- ^ Solve this dictionary by type class resolution
863 | PRewrite FC PTerm PTerm (Maybe PTerm) -- ^ "rewrite" syntax, with optional result type
864 | 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.
865 | 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.
866 | PAs FC Name PTerm -- ^ @-pattern, valid LHS only
867 | PAlternative [(Name, Name)] PAltType [PTerm] -- ^ (| A, B, C|). Includes unapplied unique name mappings for mkUniqueNames.
868 | PHidden PTerm -- ^ Irrelevant or hidden pattern
869 | PType FC -- ^ 'Type' type
870 | PUniverse Universe -- ^ Some universe
871 | PGoal FC PTerm Name PTerm -- ^ quoteGoal, used for %reflection functions
872 | PConstant FC Const -- ^ Builtin types
873 | Placeholder -- ^ Underscore
874 | PDoBlock [PDo] -- ^ Do notation
875 | PIdiom FC PTerm -- ^ Idiom brackets
877 | PMetavar FC Name -- ^ A metavariable, ?name, and its precise location
878 | PProof [PTactic] -- ^ Proof script
879 | PTactics [PTactic] -- ^ As PProof, but no auto solving
880 | PElabError Err -- ^ Error to report on elaboration
881 | PImpossible -- ^ Special case for declaring when an LHS can't typecheck
882 | PCoerced PTerm -- ^ To mark a coerced argument, so as not to coerce twice
883 | PDisamb [[T.Text]] PTerm -- ^ Preferences for explicit namespaces
884 | PUnifyLog PTerm -- ^ dump a trace of unifications when building term
885 | PNoImplicits PTerm -- ^ never run implicit converions on the term
886 | PQuasiquote PTerm (Maybe PTerm) -- ^ `(Term [: Term])
887 | PUnquote PTerm -- ^ ~Term
888 | PQuoteName Name FC -- ^ `{n} where the FC is the precise highlighting for the name in particular
889 | PRunElab FC PTerm [String] -- ^ %runElab tm - New-style proof script. Args are location, script, enclosing namespace.
890 | PConstSugar FC PTerm -- ^ A desugared constant. The FC is a precise source location that will be used to highlight it later.
891 deriving (Eq, Data, Typeable)
893data PAltType = ExactlyOne Bool -- ^ flag sets whether delay is allowed
896 deriving (Eq, Data, Typeable)
898-- | Transform the FCs in a PTerm. The first function transforms the
899-- general-purpose FCs, and the second transforms those that are used
900-- for semantic source highlighting, so they can be treated specially.
901mapPTermFC :: (FC -> FC) -> (FC -> FC) -> PTerm -> PTerm
902mapPTermFC f g (PQuote q) = PQuote q
903mapPTermFC f g (PRef fc fcs n) = PRef (g fc) (map g fcs) n
904mapPTermFC f g (PInferRef fc fcs n) = PInferRef (g fc) (map g fcs) n
905mapPTermFC f g (PPatvar fc n) = PPatvar (g fc) n
906mapPTermFC f g (PLam fc n fc' t1 t2) = PLam (f fc) n (g fc') (mapPTermFC f g t1) (mapPTermFC f g t2)
907mapPTermFC f g (PPi plic n fc t1 t2) = PPi plic n (g fc) (mapPTermFC f g t1) (mapPTermFC f g t2)
908mapPTermFC 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)
909mapPTermFC f g (PTyped t1 t2) = PTyped (mapPTermFC f g t1) (mapPTermFC f g t2)
910mapPTermFC f g (PApp fc t args) = PApp (f fc) (mapPTermFC f g t) (map (fmap (mapPTermFC f g)) args)
911mapPTermFC f g (PAppImpl t1 impls) = PAppImpl (mapPTermFC f g t1) impls
912mapPTermFC f g (PAppBind fc t args) = PAppBind (f fc) (mapPTermFC f g t) (map (fmap (mapPTermFC f g)) args)
913mapPTermFC f g (PMatchApp fc n) = PMatchApp (f fc) n
914mapPTermFC f g (PIfThenElse fc t1 t2 t3) = PIfThenElse (f fc) (mapPTermFC f g t1) (mapPTermFC f g t2) (mapPTermFC f g t3)
915mapPTermFC 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)
916mapPTermFC f g (PTrue fc info) = PTrue (f fc) info
917mapPTermFC f g (PResolveTC fc) = PResolveTC (f fc)
918mapPTermFC f g (PRewrite fc t1 t2 t3) = PRewrite (f fc) (mapPTermFC f g t1) (mapPTermFC f g t2) (fmap (mapPTermFC f g) t3)
919mapPTermFC f g (PPair fc hls info t1 t2) = PPair (f fc) (map g hls) info (mapPTermFC f g t1) (mapPTermFC f g t2)
920mapPTermFC 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)
921mapPTermFC f g (PAs fc n t) = PAs (f fc) n (mapPTermFC f g t)
922mapPTermFC f g (PAlternative ns ty ts) = PAlternative ns ty (map (mapPTermFC f g) ts)
923mapPTermFC f g (PHidden t) = PHidden (mapPTermFC f g t)
924mapPTermFC f g (PType fc) = PType (f fc)
925mapPTermFC f g (PUniverse u) = PUniverse u
926mapPTermFC f g (PGoal fc t1 n t2) = PGoal (f fc) (mapPTermFC f g t1) n (mapPTermFC f g t2)
927mapPTermFC f g (PConstant fc c) = PConstant (f fc) c
928mapPTermFC f g Placeholder = Placeholder
929mapPTermFC f g (PDoBlock dos) = PDoBlock (map mapPDoFC dos)
930 where mapPDoFC (DoExp fc t) = DoExp (f fc) (mapPTermFC f g t)
931 mapPDoFC (DoBind fc n nfc t) = DoBind (f fc) n (g nfc) (mapPTermFC f g t)
932 mapPDoFC (DoBindP fc t1 t2 alts) =
933 DoBindP (f fc) (mapPTermFC f g t1) (mapPTermFC f g t2) (map (\(l,r)-> (mapPTermFC f g l, mapPTermFC f g r)) alts)
934 mapPDoFC (DoLet fc n nfc t1 t2) = DoLet (f fc) n (g nfc) (mapPTermFC f g t1) (mapPTermFC f g t2)
935 mapPDoFC (DoLetP fc t1 t2) = DoLetP (f fc) (mapPTermFC f g t1) (mapPTermFC f g t2)
936mapPTermFC f g (PIdiom fc t) = PIdiom (f fc) (mapPTermFC f g t)
937mapPTermFC f g (PReturn fc) = PReturn (f fc)
938mapPTermFC f g (PMetavar fc n) = PMetavar (g fc) n
939mapPTermFC f g (PProof tacs) = PProof (map (fmap (mapPTermFC f g)) tacs)
940mapPTermFC f g (PTactics tacs) = PTactics (map (fmap (mapPTermFC f g)) tacs)
941mapPTermFC f g (PElabError err) = PElabError err
942mapPTermFC f g PImpossible = PImpossible
943mapPTermFC f g (PCoerced t) = PCoerced (mapPTermFC f g t)
944mapPTermFC f g (PDisamb msg t) = PDisamb msg (mapPTermFC f g t)
945mapPTermFC f g (PUnifyLog t) = PUnifyLog (mapPTermFC f g t)
946mapPTermFC f g (PNoImplicits t) = PNoImplicits (mapPTermFC f g t)
947mapPTermFC f g (PQuasiquote t1 t2) = PQuasiquote (mapPTermFC f g t1) (fmap (mapPTermFC f g) t2)
948mapPTermFC f g (PUnquote t) = PUnquote (mapPTermFC f g t)
949mapPTermFC f g (PRunElab fc tm ns) = PRunElab (f fc) (mapPTermFC f g tm) ns
950mapPTermFC f g (PConstSugar fc tm) = PConstSugar (g fc) (mapPTermFC f g tm)
951mapPTermFC f g (PQuoteName n fc) = PQuoteName n (g fc)
954dg instance Binary PTerm
955deriving instance NFData PTerm
958mapPT :: (PTerm -> PTerm) -> PTerm -> PTerm
959mapPT f t = f (mpt t) where
960 mpt (PLam fc n nfc t s) = PLam fc n nfc (mapPT f t) (mapPT f s)
961 mpt (PPi p n nfc t s) = PPi p n nfc (mapPT f t) (mapPT f s)
962 mpt (PLet fc n nfc ty v s) = PLet fc n nfc (mapPT f ty) (mapPT f v) (mapPT f s)
963 mpt (PRewrite fc t s g) = PRewrite fc (mapPT f t) (mapPT f s)
965 mpt (PApp fc t as) = PApp fc (mapPT f t) (map (fmap (mapPT f)) as)
966 mpt (PAppBind fc t as) = PAppBind fc (mapPT f t) (map (fmap (mapPT f)) as)
967 mpt (PCase fc c os) = PCase fc (mapPT f c) (map (pmap (mapPT f)) os)
968 mpt (PIfThenElse fc c t e) = PIfThenElse fc (mapPT f c) (mapPT f t) (mapPT f e)
969 mpt (PTyped l r) = PTyped (mapPT f l) (mapPT f r)
970 mpt (PPair fc hls p l r) = PPair fc hls p (mapPT f l) (mapPT f r)
971 mpt (PDPair fc hls p l t r) = PDPair fc hls p (mapPT f l) (mapPT f t) (mapPT f r)
972 mpt (PAlternative ns a as) = PAlternative ns a (map (mapPT f) as)
973 mpt (PHidden t) = PHidden (mapPT f t)
974 mpt (PDoBlock ds) = PDoBlock (map (fmap (mapPT f)) ds)
975 mpt (PProof ts) = PProof (map (fmap (mapPT f)) ts)
976 mpt (PTactics ts) = PTactics (map (fmap (mapPT f)) ts)
977 mpt (PUnifyLog tm) = PUnifyLog (mapPT f tm)
978 mpt (PDisamb ns tm) = PDisamb ns (mapPT f tm)
979 mpt (PNoImplicits tm) = PNoImplicits (mapPT f tm)
980 mpt (PGoal fc r n sc) = PGoal fc (mapPT f r) n (mapPT f sc)
984data PTactic' t = Intro [Name] | Intros | Focus Name
985 | Refine Name [Bool] | Rewrite t | DoUnify
992 | LetTac Name t | LetTacTy Name t t
993 | Exact t | Compute | Trivial | TCInstance
994 | ProofSearch Bool Bool Int (Maybe Name)
995 [Name] -- allowed local names
997 -- ^ the bool is whether to search recursively
1000 | ProofState | ProofTerm | Undo
1001 | Try (PTactic' t) (PTactic' t)
1002 | TSeq (PTactic' t) (PTactic' t)
1003 | ApplyTactic t -- see Language.Reflection module
1007 | GoalType String (PTactic' t)
1010 | TDocStr (Either Name Const)
1013 | TFail [ErrorReportPart]
1016 deriving (Show, Eq, Functor, Foldable, Traversable, Data, Typeable)
1018deriving instance Binary PTactic'
1019deriving instance NFData PTactic'
1021instance Sized a => Sized (PTactic' a) where
1022 size (Intro nms) = 1 + size nms
1024 size (Focus nm) = 1 + size nm
1025 size (Refine nm bs) = 1 + size nm + length bs
1026 size (Rewrite t) = 1 + size t
1027 size (Induction t) = 1 + size t
1028 size (LetTac nm t) = 1 + size nm + size t
1029 size (Exact t) = 1 + size t
1037 size (Try l r) = 1 + size l + size r
1038 size (TSeq l r) = 1 + size l + size r
1039 size (ApplyTactic t) = 1 + size t
1040 size (Reflect t) = 1 + size t
1041 size (Fill t) = 1 + size t
1045 size (TFail ts) = 1 + size ts
1048 size (CaseTac x) = 1 + size x
1049 size (Equiv t) = 1 + size t
1050 size (Claim x y) = 1 + size x + size y
1052 size (MatchRefine x) = 1 + size x
1053 size (LetTacTy x y z) = 1 + size x + size y + size z
1056type PTactic = PTactic' PTerm
1058data PDo' t = DoExp FC t
1059 | DoBind FC Name FC t -- ^ second FC is precise name location
1060 | DoBindP FC t t [(t,t)]
1061 | DoLet FC Name FC t t -- ^ second FC is precise name location
1063 deriving (Eq, Functor, Data, Typeable)
1065deriving instance Binary PDo'
1066deriving instance NFData PDo'
1069instance Sized a => Sized (PDo' a) where
1070 size (DoExp fc t) = 1 + size fc + size t
1071 size (DoBind fc nm nfc t) = 1 + size fc + size nm + size nfc + size t
1072 size (DoBindP fc l r alts) = 1 + size fc + size l + size r + size alts
1073 size (DoLet fc nm nfc l r) = 1 + size fc + size nm + size l + size r
1074 size (DoLetP fc l r) = 1 + size fc + size l + size r
1076type PDo = PDo' PTerm
1078-- The priority gives a hint as to elaboration order. Best to elaborate
1079-- things early which will help give a more concrete type to other
1080-- variables, e.g. a before (interpTy a).
1082data PArg' t = PImp { priority :: Int,
1083 machine_inf :: Bool, -- true if the machine inferred it
1084 argopts :: [ArgOpt],
1087 | PExp { priority :: Int,
1088 argopts :: [ArgOpt],
1091 | PConstraint { priority :: Int,
1092 argopts :: [ArgOpt],
1095 | PTacImplicit { priority :: Int,
1096 argopts :: [ArgOpt],
1100 deriving (Show, Eq, Functor, Data, Typeable)
1102data ArgOpt = AlwaysShow | HideDisplay | InaccessibleArg | UnknownImp
1103 deriving (Show, Eq, Data, Typeable)
1105instance Sized a => Sized (PArg' a) where
1106 size (PImp p _ l nm trm) = 1 + size nm + size trm
1107 size (PExp p l nm trm) = 1 + size nm + size trm
1108 size (PConstraint p l nm trm) = 1 + size nm +size nm + size trm
1109 size (PTacImplicit p l nm scr trm) = 1 + size nm + size scr + size trm
1112deriving instance Binary PArg'
1113deriving instance NFData PArg'
1116pimp n t mach = PImp 1 mach [] n t
1117pexp t = PExp 1 [] (sMN 0 "arg") t
1118pconst t = PConstraint 1 [] (sMN 0 "carg") t
1119ptacimp n s t = PTacImplicit 2 [] n s t
1121type PArg = PArg' PTerm
1123-- | Get the highest FC in a term, if one exists
1124highestFC :: PTerm -> Maybe FC
1125highestFC (PQuote _) = Nothing
1126highestFC (PRef fc _ _) = Just fc
1127highestFC (PInferRef fc _ _) = Just fc
1128highestFC (PPatvar fc _) = Just fc
1129highestFC (PLam fc _ _ _ _) = Just fc
1130highestFC (PPi _ _ _ _ _) = Nothing
1131highestFC (PLet fc _ _ _ _ _) = Just fc
1132highestFC (PTyped tm ty) = highestFC tm <|> highestFC ty
1133highestFC (PApp fc _ _) = Just fc
1134highestFC (PAppBind fc _ _) = Just fc
1135highestFC (PMatchApp fc _) = Just fc
1136highestFC (PCase fc _ _) = Just fc
1137highestFC (PIfThenElse fc _ _ _) = Just fc
1138highestFC (PTrue fc _) = Just fc
1139highestFC (PResolveTC fc) = Just fc
1140highestFC (PRewrite fc _ _ _) = Just fc
1141highestFC (PPair fc _ _ _ _) = Just fc
1142highestFC (PDPair fc _ _ _ _ _) = Just fc
1143highestFC (PAs fc _ _) = Just fc
1144highestFC (PAlternative _ _ args) =
1145 case mapMaybe highestFC args of
1148highestFC (PHidden _) = Nothing
1149highestFC (PType fc) = Just fc
1150highestFC (PUniverse _) = Nothing
1151highestFC (PGoal fc _ _ _) = Just fc
1152highestFC (PConstant fc _) = Just fc
1153highestFC Placeholder = Nothing
1154highestFC (PDoBlock lines) =
1155 case map getDoFC lines of
1159 getDoFC (DoExp fc t) = fc
1160 getDoFC (DoBind fc nm nfc t) = fc
1161 getDoFC (DoBindP fc l r alts) = fc
1162 getDoFC (DoLet fc nm nfc l r) = fc
1163 getDoFC (DoLetP fc l r) = fc
1165highestFC (PIdiom fc _) = Just fc
1166highestFC (PReturn fc) = Just fc
1167highestFC (PMetavar fc _) = Just fc
1168highestFC (PProof _) = Nothing
1169highestFC (PTactics _) = Nothing
1170highestFC (PElabError _) = Nothing
1171highestFC PImpossible = Nothing
1172highestFC (PCoerced tm) = highestFC tm
1173highestFC (PDisamb _ opts) = highestFC opts
1174highestFC (PUnifyLog tm) = highestFC tm
1175highestFC (PNoImplicits tm) = highestFC tm
1176highestFC (PQuasiquote _ _) = Nothing
1177highestFC (PUnquote tm) = highestFC tm
1178highestFC (PQuoteName _ fc) = Just fc
1179highestFC (PRunElab fc _ _) = Just fc
1180highestFC (PConstSugar fc _) = Just fc
1181highestFC (PAppImpl t _) = highestFC t
1185data ClassInfo = CI { instanceCtorName :: Name,
1186 class_methods :: [(Name, (FnOpts, PTerm))],
1187 class_defaults :: [(Name, (Name, PDecl))], -- method name -> default impl
1188 class_default_superclasses :: [PDecl],
1189 class_params :: [Name],
1190 class_instances :: [(Name, Bool)], -- the Bool is whether to include in instance search, so named instances are excluded
1191 class_determiners :: [Int] }
1194deriving instance Binary ClassInfo
1195deriving instance NFData ClassInfo
1198-- Type inference data
1200data TIData = TIPartial -- ^ a function with a partially defined type
1201 | TISolution [Term] -- ^ possible solutions to a metavariable in a type
1204-- | Miscellaneous information about functions
1205data FnInfo = FnInfo { fn_params :: [Int] }
1208deriving instance Binary FnInfo
1209deriving instance NFData FnInfo
1212data OptInfo = Optimise { inaccessible :: [(Int,Name)], -- includes names for error reporting
1213 detaggable :: Bool }
1216deriving instance Binary OptInfo
1217deriving instance NFData OptInfo
1220-- | Syntactic sugar info
1221data DSL' t = DSL { dsl_bind :: t,
1226 index_first :: Maybe t,
1227 index_next :: Maybe t,
1228 dsl_lambda :: Maybe t,
1232 deriving (Show, Functor)
1234deriving instance Binary DSL'
1235deriving instance NFData DSL'
1238type DSL = DSL' PTerm
1240data SynContext = PatternSyntax | TermSyntax | AnySyntax
1243deriving instance Binary SynContext
1244deriving instance NFData SynContext
1247data Syntax = Rule [SSymbol] PTerm SynContext
1250syntaxNames :: Syntax -> [Name]
1251syntaxNames (Rule syms _ _) = mapMaybe ename syms
1252 where ename (Keyword n) = Just n
1255syntaxSymbols :: Syntax -> [SSymbol]
1256syntaxSymbols (Rule ss _ _) = ss
1258deriving instance Binary Syntax
1259deriving instance NFData Syntax
1262data SSymbol = Keyword Name
1271deriving instance Binary SSymbol
1272deriving instance NFData SSymbol
1275newtype SyntaxRules = SyntaxRules { syntaxRulesList :: [Syntax] }
1277emptySyntaxRules :: SyntaxRules
1278emptySyntaxRules = SyntaxRules []
1280updateSyntaxRules :: [Syntax] -> SyntaxRules -> SyntaxRules
1281updateSyntaxRules rules (SyntaxRules sr) = SyntaxRules newRules
1283 newRules = sortBy (ruleSort `on` syntaxSymbols) (rules ++ sr)
1288 ruleSort (s1:ss1) (s2:ss2) =
1289 case symCompare s1 s2 of
1290 EQ -> ruleSort ss1 ss2
1293 -- Better than creating Ord instance for SSymbol since
1294 -- in general this ordering does not really make sense.
1295 symCompare (Keyword n1) (Keyword n2) = compare n1 n2
1296 symCompare (Keyword _) _ = LT
1297 symCompare (Symbol _) (Keyword _) = GT
1298 symCompare (Symbol s1) (Symbol s2) = compare s1 s2
1299 symCompare (Symbol _) _ = LT
1300 symCompare (Binding _) (Keyword _) = GT
1301 symCompare (Binding _) (Symbol _) = GT
1302 symCompare (Binding b1) (Binding b2) = compare b1 b2
1303 symCompare (Binding _) _ = LT
1304 symCompare (Expr _) (Keyword _) = GT
1305 symCompare (Expr _) (Symbol _) = GT
1306 symCompare (Expr _) (Binding _) = GT
1307 symCompare (Expr e1) (Expr e2) = compare e1 e2
1308 symCompare (Expr _) _ = LT
1309 symCompare (SimpleExpr _) (Keyword _) = GT
1310 symCompare (SimpleExpr _) (Symbol _) = GT
1311 symCompare (SimpleExpr _) (Binding _) = GT
1312 symCompare (SimpleExpr _) (Expr _) = GT
1313 symCompare (SimpleExpr e1) (SimpleExpr e2) = compare e1 e2
1315initDSL = DSL (PRef f [] (sUN ">>="))
1316 (PRef f [] (sUN "return"))
1317 (PRef f [] (sUN "<*>"))
1318 (PRef f [] (sUN "pure"))
1325 where f = fileFC "(builtin)"
1327data Using = UImplicit Name PTerm
1328 | UConstraint Name [Name]
1329 deriving (Show, Eq, Data, Typeable)
1331deriving instance Binary Using
1332deriving instance NFData Using
1335data SyntaxInfo = Syn { using :: [Using],
1336 syn_params :: [(Name, PTerm)],
1337 syn_namespace :: [String],
1339 imp_methods :: [Name], -- class methods. When expanding
1340 -- implicits, these should be expanded even under
1342 decoration :: Name -> Name,
1344 implicitAllowed :: Bool,
1345 maxline :: Maybe Int,
1348 syn_in_quasiquote :: Int }
1351deriving instance NFData SyntaxInfo
1352deriving instance Binary SyntaxInfo
1355defaultSyntax = Syn [] [] [] [] [] id False False Nothing 0 initDSL 0
1357expandNS :: SyntaxInfo -> Name -> Name
1358expandNS syn n@(NS _ _) = n
1359expandNS syn n = case syn_namespace syn of
1364-- For inferring types of things
1366bi = fileFC "builtin"
1368inferTy = sMN 0 "__Infer"
1369inferCon = sMN 0 "__infer"
1370inferDecl = PDatadecl inferTy NoFC
1372 [(emptyDocstring, [], inferCon, NoFC, PPi impl (sMN 0 "iType") NoFC (PType bi) (
1373 PPi expl (sMN 0 "ival") NoFC (PRef bi [] (sMN 0 "iType"))
1374 (PRef bi [] inferTy)), bi, [])]
1377infTerm t = PApp bi (PRef bi [] inferCon) [pimp (sMN 0 "iType") Placeholder True, pexp t]
1378infP = P (TCon 6 0) inferTy (TType (UVal 0))
1380getInferTerm, getInferType :: Term -> Term
1381getInferTerm (Bind n b sc) = Bind n b $ getInferTerm sc
1382getInferTerm (App _ (App _ _ _) tm) = tm
1383getInferTerm tm = tm -- error ("getInferTerm " ++ show tm)
1385getInferType (Bind n b sc) = Bind n (toTy b) $ getInferType sc
1386 where toTy (Lam t) = Pi Nothing t (TType (UVar 0))
1387 toTy (PVar t) = PVTy t
1389getInferType (App _ (App _ _ ty) _) = ty
1393-- Handy primitives: Unit, False, Pair, MkPair, =, mkForeign
1395primNames = [inferTy, inferCon]
1398unitCon = sUN "MkUnit"
1400falseDoc = fmap (const $ Msg "") . parseDocstring . T.pack $
1401 "The empty type, also known as the trivially false proposition." ++
1403 "Use `void` or `absurd` to prove anything if you have a variable " ++
1404 "of type `Void` in scope."
1407pairTy = sNS (sUN "Pair") ["Builtins"]
1408pairCon = sNS (sUN "MkPair") ["Builtins"]
1410upairTy = sNS (sUN "UPair") ["Builtins"]
1411upairCon = sNS (sUN "MkUPair") ["Builtins"]
1415eqDoc = fmap (const (Left $ Msg "")) . parseDocstring . T.pack $
1416 "The propositional equality type. A proof that `x` = `y`." ++
1418 "To use such a proof, pattern-match on it, and the two equal things will " ++
1419 "then need to be the _same_ pattern." ++
1421 "**Note**: Idris's equality type is potentially _heterogeneous_, which means that it " ++
1422 "is possible to state equalities between values of potentially different " ++
1423 "types. However, Idris will attempt the homogeneous case unless it fails to typecheck." ++
1425 "You may need to use `(~=~)` to explicitly request heterogeneous equality."
1427eqDecl = PDatadecl eqTy NoFC (piBindp impl [(n "A", PType bi), (n "B", PType bi)]
1428 (piBind [(n "x", PRef bi [] (n "A")), (n "y", PRef bi [] (n "B"))]
1430 [(reflDoc, reflParamDoc,
1431 eqCon, NoFC, PPi impl (n "A") NoFC (PType bi) (
1432 PPi impl (n "x") NoFC (PRef bi [] (n "A"))
1433 (PApp bi (PRef bi [] eqTy) [pimp (n "A") Placeholder False,
1434 pimp (n "B") Placeholder False,
1435 pexp (PRef bi [] (n "x")),
1436 pexp (PRef bi [] (n "x"))])), bi, [])]
1438 reflDoc = annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $
1439 "A proof that `x` in fact equals `x`. To construct this, you must have already " ++
1440 "shown that both sides are in fact equal."
1441 reflParamDoc = [(n "A", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the type at which the equality is proven"),
1442 (n "x", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the element shown to be equal to itself.")]
1444eqParamDoc = [(n "A", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the type of the left side of the equality"),
1445 (n "B", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the type of the right side of the equality")
1451-- | The special name to be used in the module documentation context -
1452-- not for use in the main definition context. The namespace around it
1453-- will determine the module to which the docs adhere.
1455modDocName = sMN 0 "ModuleDocs"
1457-- Defined in builtins.idr
1458sigmaTy = sNS (sUN "Sigma") ["Builtins"]
1459sigmaCon = sNS (sUN "MkSigma") ["Builtins"]
1461piBind :: [(Name, PTerm)] -> PTerm -> PTerm
1462piBind = piBindp expl
1464piBindp :: Plicity -> [(Name, PTerm)] -> PTerm -> PTerm
1466piBindp p ((n, ty):ns) t = PPi p n NoFC ty (piBindp p ns t)
1469-- Pretty-printing declarations and terms
1471-- These "show" instances render to an absurdly wide screen because inserted line breaks
1472-- could interfere with interactive editing, which calls "show".
1474instance Show PTerm where
1475 showsPrec _ tm = (displayS . renderPretty 1.0 10000000 . prettyImp defaultPPOption) tm
1477instance Show PDecl where
1478 showsPrec _ d = (displayS . renderPretty 1.0 10000000 . showDeclImp verbosePPOption) d
1480instance Show PClause where
1481 showsPrec _ c = (displayS . renderPretty 1.0 10000000 . showCImp verbosePPOption) c
1483instance Show PData where
1484 showsPrec _ d = (displayS . renderPretty 1.0 10000000 . showDImp defaultPPOption) d
1486instance Pretty PTerm OutputAnnotation where
1487 pretty = prettyImp defaultPPOption
1489-- | Colourise annotations according to an Idris state. It ignores the names
1490-- in the annotation, as there's no good way to show extended information on a
1492consoleDecorate :: IState -> OutputAnnotation -> String -> String
1493consoleDecorate ist _ | not (idris_colourRepl ist) = id
1494consoleDecorate ist (AnnConst c) = let theme = idris_colourTheme ist
1496 then colouriseType theme
1497 else colouriseData theme
1498consoleDecorate ist (AnnData _ _) = colouriseData (idris_colourTheme ist)
1499consoleDecorate ist (AnnType _ _) = colouriseType (idris_colourTheme ist)
1500consoleDecorate ist (AnnBoundName _ True) = colouriseImplicit (idris_colourTheme ist)
1501consoleDecorate ist (AnnBoundName _ False) = colouriseBound (idris_colourTheme ist)
1502consoleDecorate ist AnnKeyword = colouriseKeyword (idris_colourTheme ist)
1503consoleDecorate ist (AnnName n _ _ _) = let ctxt = tt_ctxt ist
1504 theme = idris_colourTheme ist
1506 _ | isDConName n ctxt -> colouriseData theme
1507 _ | isFnName n ctxt -> colouriseFun theme
1508 _ | isTConName n ctxt -> colouriseType theme
1509 _ | isPostulateName n ist -> colourisePostulate theme
1510 _ | otherwise -> id -- don't colourise unknown names
1511consoleDecorate ist (AnnFC _) = id
1512consoleDecorate ist (AnnTextFmt fmt) = Idris.Colours.colourise (colour fmt)
1513 where colour BoldText = IdrisColour Nothing True False True False
1514 colour UnderlineText = IdrisColour Nothing True True False False
1515 colour ItalicText = IdrisColour Nothing True False False True
1516consoleDecorate ist (AnnTerm _ _) = id
1517consoleDecorate ist (AnnSearchResult _) = id
1518consoleDecorate ist (AnnErr _) = id
1519consoleDecorate ist (AnnNamespace _ _) = id
1520consoleDecorate ist (AnnLink url) =
1521 \txt -> Idris.Colours.colourise (IdrisColour Nothing True True False False) txt ++ " (" ++ url ++ ")"
1523isPostulateName :: Name -> IState -> Bool
1524isPostulateName n ist = S.member n (idris_postulates ist)
1526-- | Pretty-print a high-level closed Idris term with no information about precedence/associativity
1527prettyImp :: PPOption -- ^^ pretty printing options
1528 -> PTerm -- ^^ the term to pretty-print
1529 -> Doc OutputAnnotation
1530prettyImp impl = pprintPTerm impl [] [] []
1532-- | Serialise something to base64 using its Binary instance.
1534-- | Do the right thing for rendering a term in an IState
1535prettyIst :: IState -> PTerm -> Doc OutputAnnotation
1536prettyIst ist = pprintPTerm (ppOptionIst ist) [] [] (idris_infixes ist)
1538-- | Pretty-print a high-level Idris term in some bindings context with infix info
1539pprintPTerm :: PPOption -- ^^ pretty printing options
1540 -> [(Name, Bool)] -- ^^ the currently-bound names and whether they are implicit
1541 -> [Name] -- ^^ names to always show in pi, even if not used
1542 -> [FixDecl] -- ^^ Fixity declarations
1543 -> PTerm -- ^^ the term to pretty-print
1544 -> Doc OutputAnnotation
1545pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd
1550 prettySe :: Maybe Int -> Int -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation
1551 prettySe d p bnd (PQuote r) =
1552 text "![" <> pretty r <> text "]"
1553 prettySe d p bnd (PPatvar fc n) = pretty n
1555 | Just str <- slist d p bnd e = depth d $ str
1556 | Just n <- snat d p e = depth d $ annotate (AnnData "Nat" "") (text (show n))
1557 prettySe d p bnd (PRef fc _ n) = prettyName True (ppopt_impl ppo) bnd n
1558 prettySe d p bnd (PLam fc n nfc ty sc) =
1559 depth d . bracket p startPrec . group . align . hang 2 $
1560 text "\\" <> prettyBindingOf n False <+> text "=>" <$>
1561 prettySe (decD d) startPrec ((n, False):bnd) sc
1562 prettySe d p bnd (PLet fc n nfc ty v sc) =
1563 depth d . bracket p startPrec . group . align $
1564 kwd "let" <+> (group . align . hang 2 $ prettyBindingOf n False <+> text "=" <$> prettySe (decD d) startPrec bnd v) </>
1565 kwd "in" <+> (group . align . hang 2 $ prettySe (decD d) startPrec ((n, False):bnd) sc)
1566 prettySe d p bnd (PPi (Exp l s _) n _ ty sc)
1567 | n `elem` allNamesIn sc || ppopt_impl ppo || n `elem` docArgs
1568 || ppopt_pinames ppo && uname n =
1569 depth d . bracket p startPrec . group $
1570 enclose lparen rparen (group . align $ prettyBindingOf n False <+> colon <+> prettySe (decD d) startPrec bnd ty) <+>
1571 st <> text "->" <$> prettySe (decD d) startPrec ((n, False):bnd) sc
1573 depth d . bracket p startPrec . group $
1574 group (prettySe (decD d) (startPrec + 1) bnd ty <+> st) <> text "->" <$>
1575 group (prettySe (decD d) startPrec ((n, False):bnd) sc)
1577 uname (UN n) = case str n of
1584 Static -> text "[static]" <> space
1586 prettySe d p bnd (PPi (Imp l s _ fa) n _ ty sc)
1588 depth d . bracket p startPrec $
1589 lbrace <> prettyBindingOf n True <+> colon <+> prettySe (decD d) startPrec bnd ty <> rbrace <+>
1590 st <> text "->" </> prettySe (decD d) startPrec ((n, True):bnd) sc
1591 | otherwise = depth d $ prettySe (decD d) startPrec ((n, True):bnd) sc
1595 Static -> text "[static]" <> space
1597 prettySe d p bnd (PPi (Constraint _ _) n _ ty sc) =
1598 depth d . bracket p startPrec $
1599 prettySe (decD d) (startPrec + 1) bnd ty <+> text "=>" </> prettySe (decD d) startPrec ((n, True):bnd) sc
1600 prettySe d p bnd (PPi (TacImp _ _ (PTactics [ProofSearch _ _ _ _ _ _])) n _ ty sc) =
1601 lbrace <> kwd "auto" <+> pretty n <+> colon <+> prettySe (decD d) startPrec bnd ty <>
1602 rbrace <+> text "->" </> prettySe (decD d) startPrec ((n, True):bnd) sc
1603 prettySe d p bnd (PPi (TacImp _ _ s) n _ ty sc) =
1604 depth d . bracket p startPrec $
1605 lbrace <> kwd "default" <+> prettySe (decD d) (funcAppPrec + 1) bnd s <+> pretty n <+> colon <+> prettySe (decD d) startPrec bnd ty <>
1606 rbrace <+> text "->" </> prettySe (decD d) startPrec ((n, True):bnd) sc
1607 -- This case preserves the behavior of the former constructor PEq.
1608 -- It should be removed if feasible when the pretty-printing of infix
1609 -- operators in general is improved.
1610 prettySe d p bnd (PApp _ (PRef _ _ n) [lt, rt, l, r])
1611 | n == eqTy, ppopt_impl ppo =
1612 depth d . bracket p eqPrec $
1613 enclose lparen rparen eq <+>
1614 align (group (vsep (map (prettyArgS (decD d) bnd)
1617 depth d . bracket p eqPrec . align . group $
1618 prettyTerm (getTm l) <+> eq <$> group (prettyTerm (getTm r))
1619 where eq = annName eqTy (text "=")
1621 prettyTerm = prettySe (decD d) (eqPrec + 1) bnd
1622 prettySe d p bnd (PApp _ (PRef _ _ f) args) -- normal names, no explicit args
1623 | UN nm <- basename f
1624 , not (ppopt_impl ppo) && null (getShowArgs args) =
1625 prettyName True (ppopt_impl ppo) bnd f
1626 prettySe d p bnd (PAppBind _ (PRef _ _ f) [])
1627 | not (ppopt_impl ppo) = text "!" <> prettyName True (ppopt_impl ppo) bnd f
1628 prettySe d p bnd (PApp _ (PRef _ _ op) args) -- infix operators
1629 | UN nm <- basename op
1631 (not (ppopt_impl ppo)) && (not $ isAlpha (thead nm)) =
1632 case getShowArgs args of
1634 [x] -> group (opName True <$> group (prettySe (decD d) startPrec bnd (getTm x)))
1635 [l,r] -> let precedence = maybe (startPrec - 1) prec f
1636 in depth d . bracket p precedence $ inFix (getTm l) (getTm r)
1637 (l@(PExp _ _ _ _) : r@(PExp _ _ _ _) : rest) ->
1638 depth d . bracket p funcAppPrec $
1639 enclose lparen rparen (inFix (getTm l) (getTm r)) <+>
1640 align (group (vsep (map (prettyArgS d bnd) rest)))
1641 as -> opName True <+> align (vsep (map (prettyArgS d bnd) as))
1642 where opName isPrefix = prettyName isPrefix (ppopt_impl ppo) bnd op
1643 f = getFixity (opStr op)
1645 Nothing -> funcAppPrec + 1
1646 Just (Infixl p') -> p'
1647 Just f' -> prec f' + 1
1649 Nothing -> funcAppPrec + 1
1650 Just (Infixr p') -> p'
1651 Just f' -> prec f' + 1
1652 inFix l r = align . group $
1653 (prettySe (decD d) left bnd l <+> opName False) <$>
1654 group (prettySe (decD d) right bnd r)
1655 prettySe d p bnd (PApp _ hd@(PRef fc _ f) [tm]) -- symbols, like 'foo
1656 | PConstant NoFC (Idris.Core.TT.Str str) <- getTm tm,
1657 f == sUN "Symbol_" = annotate (AnnType ("'" ++ str) ("The symbol " ++ str)) $
1658 char '\'' <> prettySe (decD d) startPrec bnd (PRef fc [] (sUN str))
1659 prettySe d p bnd (PApp _ f as) = -- Normal prefix applications
1660 let args = getShowArgs as
1661 fp = prettySe (decD d) (startPrec + 1) bnd f
1662 shownArgs = if ppopt_impl ppo then as else args
1664 depth d . bracket p funcAppPrec . group $
1667 else fp <+> align (vsep (map (prettyArgS d bnd) shownArgs))
1668 prettySe d p bnd (PCase _ scr cases) =
1669 align $ kwd "case" <+> prettySe (decD d) startPrec bnd scr <+> kwd "of" <$>
1670 depth d (indent 2 (vsep (map ppcase cases)))
1672 ppcase (l, r) = let prettyCase = prettySe (decD d) startPrec
1673 ([(n, False) | n <- vars l] ++ bnd)
1674 in nest nestingSize $
1675 prettyCase l <+> text "=>" <+> prettyCase r
1676 -- Warning: this is a bit of a hack. At this stage, we don't have the
1677 -- global context, so we can't determine which names are constructors,
1678 -- which are types, and which are pattern variables on the LHS of the
1679 -- case pattern. We use the heuristic that names without a namespace
1680 -- are patvars, because right now case blocks in PTerms are always
1681 -- delaborated from TT before being sent to the pretty-printer. If they
1682 -- start getting printed directly, THIS WILL BREAK.
1683 -- Potential solution: add a list of known patvars to the cases in
1684 -- PCase, and have the delaborator fill it out, kind of like the pun
1685 -- disambiguation on PDPair.
1686 vars tm = filter noNS (allNamesIn tm)
1687 noNS (NS _ _) = False
1690 prettySe d p bnd (PIfThenElse _ c t f) =
1691 depth d . bracket p funcAppPrec . group . align . hang 2 . vsep $
1692 [ kwd "if" <+> prettySe (decD d) startPrec bnd c
1693 , kwd "then" <+> prettySe (decD d) startPrec bnd t
1694 , kwd "else" <+> prettySe (decD d) startPrec bnd f
1696 prettySe d p bnd (PHidden tm) = text "." <> prettySe (decD d) funcAppPrec bnd tm
1697 prettySe d p bnd (PResolveTC _) = kwd "%instance"
1698 prettySe d p bnd (PTrue _ IsType) = annName unitTy $ text "()"
1699 prettySe d p bnd (PTrue _ IsTerm) = annName unitCon $ text "()"
1700 prettySe d p bnd (PTrue _ TypeOrTerm) = text "()"
1701 prettySe d p bnd (PRewrite _ l r _) =
1702 depth d . bracket p startPrec $
1703 text "rewrite" <+> prettySe (decD d) (startPrec + 1) bnd l <+> text "in" <+> prettySe (decD d) startPrec bnd r
1704 prettySe d p bnd (PTyped l r) =
1705 lparen <> prettySe (decD d) startPrec bnd l <+> colon <+> prettySe (decD d) startPrec bnd r <> rparen
1706 prettySe d p bnd pair@(PPair _ _ pun _ _) -- flatten tuples to the right, like parser
1707 | Just elts <- pairElts pair = depth d . enclose (ann lparen) (ann rparen) .
1708 align . group . vsep . punctuate (ann comma) $
1709 map (prettySe (decD d) startPrec bnd) elts
1710 where ann = case pun of
1712 IsType -> annName pairTy
1713 IsTerm -> annName pairCon
1714 prettySe d p bnd (PDPair _ _ pun l t r) =
1718 annotated (text "**") <+>
1719 prettySe (decD d) startPrec (addBinding bnd) r <>
1721 where annotated = case pun of
1722 IsType -> annName sigmaTy
1723 IsTerm -> annName sigmaCon
1725 (left, addBinding) = case (l, pun) of
1726 (PRef _ _ n, IsType) -> (bindingOf n False <+> text ":" <+> prettySe (decD d) startPrec bnd t, ((n, False) :))
1727 _ -> (prettySe (decD d) startPrec bnd l, id)
1728 prettySe d p bnd (PAlternative ns a as) =
1729 lparen <> text "|" <> prettyAs <> text "|" <> rparen
1732 foldr (\l -> \r -> l <+> text "," <+> r) empty $ map (depth d . prettySe (decD d) startPrec bnd) as
1733 prettySe d p bnd (PType _) = annotate (AnnType "Type" "The type of types") $ text "Type"
1734 prettySe d p bnd (PUniverse u) = annotate (AnnType (show u) "The type of unique types") $ text (show u)
1735 prettySe d p bnd (PConstant _ c) = annotate (AnnConst c) (text (show c))
1736 -- XXX: add pretty for tactics
1737 prettySe d p bnd (PProof ts) =
1738 kwd "proof" <+> lbrace <> ellipsis <> rbrace
1739 prettySe d p bnd (PTactics ts) =
1740 kwd "tactics" <+> lbrace <> ellipsis <> rbrace
1741 prettySe d p bnd (PMetavar _ n) = annotate (AnnName n (Just MetavarOutput) Nothing Nothing) $ text "?" <> pretty n
1742 prettySe d p bnd (PReturn f) = kwd "return"
1743 prettySe d p bnd PImpossible = kwd "impossible"
1744 prettySe d p bnd Placeholder = text "_"
1745 prettySe d p bnd (PDoBlock dos) =
1746 bracket p startPrec $
1747 kwd "do" <+> align (vsep (map (group . align . hang 2) (ppdo bnd dos)))
1748 where ppdo bnd (DoExp _ tm:dos) = prettySe (decD d) startPrec bnd tm : ppdo bnd dos
1749 ppdo bnd (DoBind _ bn _ tm : dos) =
1750 (prettyBindingOf bn False <+> text "<-" <+>
1751 group (align (hang 2 (prettySe (decD d) startPrec bnd tm)))) :
1752 ppdo ((bn, False):bnd) dos
1753 ppdo bnd (DoBindP _ _ _ _ : dos) = -- ok because never made by delab
1754 text "no pretty printer for pattern-matching do binding" :
1756 ppdo bnd (DoLet _ ln _ ty v : dos) =
1757 (kwd "let" <+> prettyBindingOf ln False <+>
1758 (if ty /= Placeholder
1759 then colon <+> prettySe (decD d) startPrec bnd ty <+> text "="
1761 group (align (hang 2 (prettySe (decD d) startPrec bnd v)))) :
1762 ppdo ((ln, False):bnd) dos
1763 ppdo bnd (DoLetP _ _ _ : dos) = -- ok because never made by delab
1764 text "no pretty printer for pattern-matching do binding" :
1767 prettySe d p bnd (PCoerced t) = prettySe d p bnd t
1768 prettySe d p bnd (PElabError s) = pretty s
1769 -- Quasiquote pprinting ignores bound vars
1770 prettySe d p bnd (PQuasiquote t Nothing) = text "`(" <> prettySe (decD d) p [] t <> text ")"
1771 prettySe d p bnd (PQuasiquote t (Just g)) = text "`(" <> prettySe (decD d) p [] t <+> colon <+> prettySe (decD d) p [] g <> text ")"
1772 prettySe d p bnd (PUnquote t) = text "~" <> prettySe (decD d) p bnd t
1773 prettySe d p bnd (PQuoteName n _) = text "`{" <> prettyName True (ppopt_impl ppo) bnd n <> text "}"
1774 prettySe d p bnd (PRunElab _ tm _) =
1775 bracket p funcAppPrec . group . align . hang 2 $
1777 prettySe (decD d) funcAppPrec bnd tm
1778 prettySe d p bnd (PConstSugar fc tm) = prettySe d p bnd tm -- should never occur, but harmless
1780 prettySe d p bnd _ = text "missing pretty-printer for term"
1782 prettyBindingOf :: Name -> Bool -> Doc OutputAnnotation
1783 prettyBindingOf n imp = annotate (AnnBoundName n imp) (text (display n))
1784 where display (UN n) = T.unpack n
1785 display (MN _ n) = T.unpack n
1786 -- If a namespace is specified on a binding form, we'd better show it regardless of the implicits settings
1787 display (NS n ns) = (concat . intersperse "." . map T.unpack . reverse) ns ++ "." ++ display n
1790 prettyArgS d bnd (PImp _ _ _ n tm) = prettyArgSi d bnd (n, tm)
1791 prettyArgS d bnd (PExp _ _ _ tm) = prettyArgSe d bnd tm
1792 prettyArgS d bnd (PConstraint _ _ _ tm) = prettyArgSc d bnd tm
1793 prettyArgS d bnd (PTacImplicit _ _ n _ tm) = prettyArgSti d bnd (n, tm)
1795 prettyArgSe d bnd arg = prettySe d (funcAppPrec + 1) bnd arg
1796 prettyArgSi d bnd (n, val) = lbrace <> pretty n <+> text "=" <+> prettySe (decD d) startPrec bnd val <> rbrace
1797 prettyArgSc d bnd val = lbrace <> lbrace <> prettySe (decD d) startPrec bnd val <> rbrace <> rbrace
1798 prettyArgSti d bnd (n, val) = lbrace <> kwd "auto" <+> pretty n <+> text "=" <+> prettySe (decD d) startPrec bnd val <> rbrace
1800 annName :: Name -> Doc OutputAnnotation -> Doc OutputAnnotation
1801 annName n = annotate (AnnName n Nothing Nothing Nothing)
1803 opStr :: Name -> String
1804 opStr (NS n _) = opStr n
1805 opStr (UN n) = T.unpack n
1807 slist' :: Maybe Int -> Int -> [(Name, Bool)] -> PTerm -> Maybe [Doc OutputAnnotation]
1808 slist' (Just d) _ _ _ | d <= 0 = Nothing
1810 | containsHole e = Nothing
1811 slist' d p bnd (PApp _ (PRef _ _ nil) _)
1812 | not (ppopt_impl ppo) && nsroot nil == sUN "Nil" = Just []
1813 slist' d p bnd (PRef _ _ nil)
1814 | not (ppopt_impl ppo) && nsroot nil == sUN "Nil" = Just []
1815 slist' d p bnd (PApp _ (PRef _ _ cons) args)
1816 | nsroot cons == sUN "::",
1817 (PExp {getTm=tl}):(PExp {getTm=hd}):imps <- reverse args,
1819 Just tl' <- slist' (decD d) p bnd tl
1820 = Just (prettySe d startPrec bnd hd : tl')
1822 isImp (PImp {}) = True
1824 slist' _ _ _ tm = Nothing
1826 slist d p bnd e | Just es <- slist' d p bnd e = Just $
1828 [] -> annotate (AnnData "" "") $ text "[]"
1829 [x] -> enclose left right . group $ x
1830 xs -> enclose left right .
1831 align . group . vsep .
1832 punctuate comma $ xs
1833 where left = (annotate (AnnData "" "") (text "["))
1834 right = (annotate (AnnData "" "") (text "]"))
1835 comma = (annotate (AnnData "" "") (text ","))
1836 slist _ _ _ _ = Nothing
1838 pairElts :: PTerm -> Maybe [PTerm]
1839 pairElts (PPair _ _ _ x y) | Just elts <- pairElts y = Just (x:elts)
1840 | otherwise = Just [x, y]
1841 pairElts _ = Nothing
1843 natns = "Prelude.Nat."
1845 snat :: Maybe Int -> Int -> PTerm -> Maybe Integer
1846 snat (Just x) _ _ | x <= 0 = Nothing
1847 snat d p (PRef _ _ z)
1848 | show z == (natns++"Z") || show z == "Z" = Just 0
1849 snat d p (PApp _ s [PExp {getTm=n}])
1850 | show s == (natns++"S") || show s == "S",
1851 Just n' <- snat (decD d) p n
1853 snat _ _ _ = Nothing
1855 bracket outer inner doc
1856 | outer > inner = lparen <> doc <> rparen
1859 ellipsis = text "..."
1862 depth (Just d) = if d <= 0 then const (ellipsis) else id
1864 decD = fmap (\x -> x - 1)
1866 kwd = annotate AnnKeyword . text
1868 fixities :: M.Map String Fixity
1869 fixities = M.fromList [(s, f) | (Fix f s) <- infixes]
1871 getFixity :: String -> Maybe Fixity
1872 getFixity = flip M.lookup fixities
1874-- | Strip away namespace information
1875basename :: Name -> Name
1876basename (NS n _) = basename n
1879-- | Determine whether a name was the one inserted for a hole or
1880-- guess by the delaborator
1881isHoleName :: Name -> Bool
1882isHoleName (UN n) = n == T.pack "[__]"
1885-- | Check whether a PTerm has been delaborated from a Term containing a Hole or Guess
1886containsHole :: PTerm -> Bool
1887containsHole pterm = or [isHoleName n | PRef _ _ n <- take 1000 $ universe pterm]
1889-- | Pretty-printer helper for names that attaches the correct annotations
1891 :: Bool -- ^^ whether the name should be parenthesised if it is an infix operator
1892 -> Bool -- ^^ whether to show namespaces
1893 -> [(Name, Bool)] -- ^^ the current bound variables and whether they are implicit
1894 -> Name -- ^^ the name to pprint
1895 -> Doc OutputAnnotation
1896prettyName infixParen showNS bnd n
1897 | (MN _ s) <- n, isPrefixOf "_" $ T.unpack s = text "_"
1898 | (UN n') <- n, T.unpack n' == "_" = text "_"
1899 | Just imp <- lookup n bnd = annotate (AnnBoundName n imp) fullName
1900 | otherwise = annotate (AnnName n Nothing Nothing Nothing) fullName
1901 where fullName = text nameSpace <> parenthesise (text (baseName n))
1902 baseName (UN n) = T.unpack n
1903 baseName (NS n ns) = baseName n
1904 baseName (MN i s) = T.unpack s
1905 baseName other = show other
1906 nameSpace = case n of
1907 (NS n' ns) -> if showNS then (concatMap (++ ".") . map T.unpack . reverse) ns else ""
1909 isInfix = case baseName n of
1911 (c : _) -> not (isAlpha c)
1912 parenthesise = if isInfix && infixParen then enclose lparen rparen else id
1915showCImp :: PPOption -> PClause -> Doc OutputAnnotation
1916showCImp ppo (PClause _ n l ws r w)
1917 = prettyImp ppo l <+> showWs ws <+> text "=" <+> prettyImp ppo r
1918 <+> text "where" <+> text (show w)
1921 showWs (x : xs) = text "|" <+> prettyImp ppo x <+> showWs xs
1922showCImp ppo (PWith _ n l ws r pn w)
1923 = prettyImp ppo l <+> showWs ws <+> text "with" <+> prettyImp ppo r
1924 <+> braces (text (show w))
1927 showWs (x : xs) = text "|" <+> prettyImp ppo x <+> showWs xs
1930showDImp :: PPOption -> PData -> Doc OutputAnnotation
1931showDImp ppo (PDatadecl n nfc ty cons)
1932 = text "data" <+> text (show n) <+> colon <+> prettyImp ppo ty <+> text "where" <$>
1933 (indent 2 $ vsep (map (\ (_, _, n, _, t, _, _) -> pipe <+> prettyName True False [] n <+> colon <+> prettyImp ppo t) cons))
1935showDecls :: PPOption -> [PDecl] -> Doc OutputAnnotation
1936showDecls o ds = vsep (map (showDeclImp o) ds)
1938showDeclImp _ (PFix _ f ops) = text (show f) <+> cat (punctuate (text ",") (map text ops))
1939showDeclImp o (PTy _ _ _ _ _ n _ t) = text "tydecl" <+> text (showCG n) <+> colon <+> prettyImp o t
1940showDeclImp o (PClauses _ _ n cs) = text "pat" <+> text (showCG n) <+> text "\t" <+>
1941 indent 2 (vsep (map (showCImp o) cs))
1942showDeclImp o (PData _ _ _ _ _ d) = showDImp o { ppopt_impl = True } d
1943showDeclImp o (PParams _ ns ps) = text "params" <+> braces (text (show ns) <> line <> showDecls o ps <> line)
1944showDeclImp o (PNamespace n fc ps) = text "namespace" <+> text n <> braces (line <> showDecls o ps <> line)
1945showDeclImp _ (PSyntax _ syn) = text "syntax" <+> text (show syn)
1946showDeclImp o (PClass _ _ _ cs n _ ps _ _ ds _ _)
1947 = text "class" <+> text (show cs) <+> text (show n) <+> text (show ps) <> line <> showDecls o ds
1948showDeclImp o (PInstance _ _ _ _ cs n _ _ t _ ds)
1949 = text "instance" <+> text (show cs) <+> text (show n) <+> prettyImp o t <> line <> showDecls o ds
1950showDeclImp _ _ = text "..."
1951-- showDeclImp (PImport o) = "import " ++ o
1953getImps :: [PArg] -> [(Name, PTerm)]
1955getImps (PImp _ _ _ n tm : xs) = (n, tm) : getImps xs
1956getImps (_ : xs) = getImps xs
1958getExps :: [PArg] -> [PTerm]
1960getExps (PExp _ _ _ tm : xs) = tm : getExps xs
1961getExps (_ : xs) = getExps xs
1963getShowArgs :: [PArg] -> [PArg]
1965getShowArgs (e@(PExp _ _ _ tm) : xs) = e : getShowArgs xs
1966getShowArgs (e : xs) | AlwaysShow `elem` argopts e = e : getShowArgs xs
1967 | PImp _ _ _ _ tm <- e
1968 , containsHole tm = e : getShowArgs xs
1969getShowArgs (_ : xs) = getShowArgs xs
1971getConsts :: [PArg] -> [PTerm]
1973getConsts (PConstraint _ _ _ tm : xs) = tm : getConsts xs
1974getConsts (_ : xs) = getConsts xs
1976getAll :: [PArg] -> [PTerm]
1981showName :: Maybe IState -- ^^ the Idris state, for information about names and colours
1982 -> [(Name, Bool)] -- ^^ the bound variables and whether they're implicit
1983 -> PPOption -- ^^ pretty printing options
1984 -> Bool -- ^^ whether to colourise
1985 -> Name -- ^^ the term to show
1987showName ist bnd ppo colour n = case ist of
1988 Just i -> if colour then colourise n (idris_colourTheme i) else showbasic n
1989 Nothing -> showbasic n
1990 where name = if ppopt_impl ppo then show n else showbasic n
1991 showbasic n@(UN _) = showCG n
1992 showbasic (MN i s) = str s
1993 showbasic (NS n s) = showSep "." (map str (reverse s)) ++ "." ++ showbasic n
1994 showbasic (SN s) = show s
1996 colourise n t = let ctxt' = fmap tt_ctxt ist in
1999 Just ctxt | Just impl <- lookup n bnd -> if impl then colouriseImplicit t name
2000 else colouriseBound t name
2001 | isDConName n ctxt -> colouriseData t name
2002 | isFnName n ctxt -> colouriseFun t name
2003 | isTConName n ctxt -> colouriseType t name
2004 -- The assumption is that if a name is not bound and does not exist in the
2005 -- global context, then we're somewhere in which implicit info has been lost
2006 -- (like error messages). Thus, unknown vars are colourised as implicits.
2007 | otherwise -> colouriseImplicit t name
2009showTm :: IState -- ^^ the Idris state, for information about identifiers and colours
2010 -> PTerm -- ^^ the term to show
2012showTm ist = displayDecorated (consoleDecorate ist) .
2013 renderPretty 0.8 100000 .
2014 prettyImp (ppOptionIst ist)
2016-- | Show a term with implicits, no colours
2017showTmImpls :: PTerm -> String
2018showTmImpls = flip (displayS . renderCompact . prettyImp verbosePPOption) ""
2020-- | Show a term with specific options
2021showTmOpts :: PPOption -> PTerm -> String
2022showTmOpts opt = flip (displayS . renderPretty 1.0 10000000 . prettyImp opt) ""
2025instance Sized PTerm where
2026 size (PQuote rawTerm) = size rawTerm
2027 size (PRef fc _ name) = size name
2028 size (PLam fc name _ ty bdy) = 1 + size ty + size bdy
2029 size (PPi plicity name fc ty bdy) = 1 + size ty + size fc + size bdy
2030 size (PLet fc name nfc ty def bdy) = 1 + size ty + size def + size bdy
2031 size (PTyped trm ty) = 1 + size trm + size ty
2032 size (PApp fc name args) = 1 + size args
2033 size (PAppBind fc name args) = 1 + size args
2034 size (PCase fc trm bdy) = 1 + size trm + size bdy
2035 size (PIfThenElse fc c t f) = 1 + sum (map size [c, t, f])
2036 size (PTrue fc _) = 1
2037 size (PResolveTC fc) = 1
2038 size (PRewrite fc left right _) = 1 + size left + size right
2039 size (PPair fc _ _ left right) = 1 + size left + size right
2040 size (PDPair fs _ _ left ty right) = 1 + size left + size ty + size right
2041 size (PAlternative _ a alts) = 1 + size alts
2042 size (PHidden hidden) = size hidden
2043 size (PUnifyLog tm) = size tm
2044 size (PDisamb _ tm) = size tm
2045 size (PNoImplicits tm) = size tm
2047 size (PUniverse _) = 1
2048 size (PConstant fc const) = 1 + size fc + size const
2049 size Placeholder = 1
2050 size (PDoBlock dos) = 1 + size dos
2051 size (PIdiom fc term) = 1 + size term
2052 size (PReturn fc) = 1
2053 size (PMetavar _ name) = 1
2054 size (PProof tactics) = size tactics
2055 size (PElabError err) = size err
2056 size PImpossible = 1
2059getPArity :: PTerm -> Int
2060getPArity (PPi _ _ _ _ sc) = 1 + getPArity sc
2063-- Return all names, free or globally bound, in the given term.
2065allNamesIn :: PTerm -> [Name]
2066allNamesIn tm = nub $ ni [] tm
2067 where -- TODO THINK added niTacImp, but is it right?
2069 | not (n `elem` env) = [n]
2070 ni env (PPatvar _ n) = [n]
2071 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
2072 ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
2073 ni env (PCase _ c os) = ni env c ++ concatMap (ni env) (map snd os)
2074 ni env (PIfThenElse _ c t f) = ni env c ++ ni env t ++ ni env f
2075 ni env (PLam fc n _ ty sc) = ni env ty ++ ni (n:env) sc
2076 ni env (PPi p n _ ty sc) = niTacImp env p ++ ni env ty ++ ni (n:env) sc
2077 ni env (PLet _ n _ ty val sc) = ni env ty ++ ni env val ++ ni (n:env) sc
2078 ni env (PHidden tm) = ni env tm
2079 ni env (PRewrite _ l r _) = ni env l ++ ni env r
2080 ni env (PTyped l r) = ni env l ++ ni env r
2081 ni env (PPair _ _ _ l r) = ni env l ++ ni env r
2082 ni env (PDPair _ _ _ (PRef _ _ n) Placeholder r) = n : ni env r
2083 ni env (PDPair _ _ _ (PRef _ _ n) t r) = ni env t ++ ni (n:env) r
2084 ni env (PDPair _ _ _ l t r) = ni env l ++ ni env t ++ ni env r
2085 ni env (PAlternative ns a ls) = concatMap (ni env) ls
2086 ni env (PUnifyLog tm) = ni env tm
2087 ni env (PDisamb _ tm) = ni env tm
2088 ni env (PNoImplicits tm) = ni env tm
2091 niTacImp env (TacImp _ _ scr) = ni env scr
2095-- Return all names defined in binders in the given term
2096boundNamesIn :: PTerm -> [Name]
2097boundNamesIn tm = S.toList (ni S.empty tm)
2098 where -- TODO THINK Added niTacImp, but is it right?
2099 ni set (PApp _ f as) = niTms (ni set f) (map getTm as)
2100 ni set (PAppBind _ f as) = niTms (ni set f) (map getTm as)
2101 ni set (PCase _ c os) = niTms (ni set c) (map snd os)
2102 ni set (PIfThenElse _ c t f) = niTms set [c, t, f]
2103 ni set (PLam fc n _ ty sc) = S.insert n $ ni (ni set ty) sc
2104 ni set (PLet fc n nfc ty val sc) = S.insert n $ ni (ni (ni set ty) val) sc
2105 ni set (PPi p n _ ty sc) = niTacImp (S.insert n $ ni (ni set ty) sc) p
2106 ni set (PRewrite _ l r _) = ni (ni set l) r
2107 ni set (PTyped l r) = ni (ni set l) r
2108 ni set (PPair _ _ _ l r) = ni (ni set l) r
2109 ni set (PDPair _ _ _ (PRef _ _ n) t r) = ni (ni set t) r
2110 ni set (PDPair _ _ _ l t r) = ni (ni (ni set l) t) r
2111 ni set (PAlternative ns a as) = niTms set as
2112 ni set (PHidden tm) = ni set tm
2113 ni set (PUnifyLog tm) = ni set tm
2114 ni set (PDisamb _ tm) = ni set tm
2115 ni set (PNoImplicits tm) = ni set tm
2119 niTms set (x : xs) = niTms (ni set x) xs
2121 niTacImp set (TacImp _ _ scr) = ni set scr
2122 niTacImp set _ = set
2124-- Return names which are valid implicits in the given term (type).
2125implicitNamesIn :: [Name] -> IState -> PTerm -> [Name]
2126implicitNamesIn uvars ist tm = nub $ ni [] tm
2129 | not (n `elem` env)
2130 = case lookupTy n (tt_ctxt ist) of
2132 _ -> if n `elem` uvars then [n] else []
2133 ni env (PApp _ f@(PRef _ _ n) as)
2134 | n `elem` uvars = ni env f ++ concatMap (ni env) (map getTm as)
2135 | otherwise = concatMap (ni env) (map getTm as)
2136 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
2137 ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
2138 ni env (PCase _ c os) = ni env c ++
2139 -- names in 'os', not counting the names bound in the cases
2140 (nub (concatMap (ni env) (map snd os))
2141 \\ nub (concatMap (ni env) (map fst os)))
2142 ni env (PIfThenElse _ c t f) = concatMap (ni env) [c, t, f]
2143 ni env (PLam fc n _ ty sc) = ni env ty ++ ni (n:env) sc
2144 ni env (PPi p n _ ty sc) = ni env ty ++ ni (n:env) sc
2145 ni env (PRewrite _ l r _) = ni env l ++ ni env r
2146 ni env (PTyped l r) = ni env l ++ ni env r
2147 ni env (PPair _ _ _ l r) = ni env l ++ ni env r
2148 ni env (PDPair _ _ _ (PRef _ _ n) t r) = ni env t ++ ni (n:env) r
2149 ni env (PDPair _ _ _ l t r) = ni env l ++ ni env t ++ ni env r
2150 ni env (PAlternative ns a as) = concatMap (ni env) as
2151 ni env (PHidden tm) = ni env tm
2152 ni env (PUnifyLog tm) = ni env tm
2153 ni env (PDisamb _ tm) = ni env tm
2154 ni env (PNoImplicits tm) = ni env tm
2157-- Return names which are free in the given term.
2158namesIn :: [(Name, PTerm)] -> IState -> PTerm -> [Name]
2159namesIn uvars ist tm = nub $ ni [] tm
2162 | not (n `elem` env)
2163 = case lookupTy n (tt_ctxt ist) of
2165 _ -> if n `elem` (map fst uvars) then [n] else []
2166 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
2167 ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
2168 ni env (PCase _ c os) = ni env c ++
2169 -- names in 'os', not counting the names bound in the cases
2170 (nub (concatMap (ni env) (map snd os))
2171 \\ nub (concatMap (ni env) (map fst os)))
2172 ni env (PIfThenElse _ c t f) = concatMap (ni env) [c, t, f]
2173 ni env (PLam fc n nfc ty sc) = ni env ty ++ ni (n:env) sc
2174 ni env (PPi p n _ ty sc) = niTacImp env p ++ ni env ty ++ ni (n:env) sc
2175 ni env (PRewrite _ l r _) = ni env l ++ ni env r
2176 ni env (PTyped l r) = ni env l ++ ni env r
2177 ni env (PPair _ _ _ l r) = ni env l ++ ni env r
2178 ni env (PDPair _ _ _ (PRef _ _ n) t r) = ni env t ++ ni (n:env) r
2179 ni env (PDPair _ _ _ l t r) = ni env l ++ ni env t ++ ni env r
2180 ni env (PAlternative ns a as) = concatMap (ni env) as
2181 ni env (PHidden tm) = ni env tm
2182 ni env (PUnifyLog tm) = ni env tm
2183 ni env (PDisamb _ tm) = ni env tm
2184 ni env (PNoImplicits tm) = ni env tm
2187 niTacImp env (TacImp _ _ scr) = ni env scr
2190-- Return which of the given names are used in the given term.
2192usedNamesIn :: [Name] -> IState -> PTerm -> [Name]
2193usedNamesIn vars ist tm = nub $ ni [] tm
2194 where -- TODO THINK added niTacImp, but is it right?
2196 | n `elem` vars && not (n `elem` env)
2197 = case lookupDefExact n (tt_ctxt ist) of
2200 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
2201 ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
2202 ni env (PCase _ c os) = ni env c ++ concatMap (ni env) (map snd os)
2203 ni env (PIfThenElse _ c t f) = concatMap (ni env) [c, t, f]
2204 ni env (PLam fc n _ ty sc) = ni env ty ++ ni (n:env) sc
2205 ni env (PPi p n _ ty sc) = niTacImp env p ++ ni env ty ++ ni (n:env) sc
2206 ni env (PRewrite _ l r _) = ni env l ++ ni env r
2207 ni env (PTyped l r) = ni env l ++ ni env r
2208 ni env (PPair _ _ _ l r) = ni env l ++ ni env r
2209 ni env (PDPair _ _ _ (PRef _ _ n) t r) = ni env t ++ ni (n:env) r
2210 ni env (PDPair _ _ _ l t r) = ni env l ++ ni env t ++ ni env r
2211 ni env (PAlternative ns a as) = concatMap (ni env) as
2212 ni env (PHidden tm) = ni env tm
2213 ni env (PUnifyLog tm) = ni env tm
2214 ni env (PDisamb _ tm) = ni env tm
2215 ni env (PNoImplicits tm) = ni env tm
2218 niTacImp env (TacImp _ _ scr) = ni env scr
2221-- Return the list of inaccessible (= dotted) positions for a name.
2222getErasureInfo :: IState -> Name -> [Int]
2223getErasureInfo ist n =
2224 case lookupCtxtExact n (idris_optimisation ist) of
2225 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