Idris.AbsSyntaxTree

Synopsis

• data ElabWhat
  • = ETypes
  • | EDefns
  • | EAll
• data ElabInfo = EInfo {
  • params :: [(Name, PTerm)]
  • inblock :: Ctxt [Name]
  • liftname :: Name -> Name
  • namespace :: Maybe [String]
  • elabFC :: Maybe FC
  • rhs_trans :: PTerm -> PTerm
  • rec_elabDecl :: ElabWhat -> ElabInfo -> PDecl -> Idris ()
  }
• toplevel :: ElabInfo
• eInfoNames :: ElabInfo -> [Name]
• data IOption = IOption {
  • opt_logLevel :: Int
  • opt_logcats :: [LogCat]
  • opt_typecase :: Bool
  • opt_typeintype :: Bool
  • opt_coverage :: Bool
  • opt_showimp :: Bool
  • opt_errContext :: Bool
  • opt_repl :: Bool
  • opt_verbose :: Bool
  • opt_nobanner :: Bool
  • opt_quiet :: Bool
  • opt_codegen :: Codegen
  • opt_outputTy :: OutputType
  • opt_ibcsubdir :: FilePath
  • opt_importdirs :: [FilePath]
  • opt_triple :: String
  • opt_cpu :: String
  • opt_cmdline :: [Opt]
  • opt_origerr :: Bool
  • opt_autoSolve :: Bool
  • opt_autoImport :: [FilePath]
  • opt_optimise :: [Optimisation]
  • opt_printdepth :: Maybe Int
  • opt_evaltypes :: Bool
  • opt_desugarnats :: Bool
  • opt_autoimpls :: Bool
  }
• defaultOpts :: IOption
• data PPOption = PPOption {
  • ppopt_impl :: Bool
  • ppopt_desugarnats :: Bool
  • ppopt_pinames :: Bool
  • ppopt_depth :: Maybe Int
  }
• data Optimisation = PETransform
• defaultOptimise :: [Optimisation]
• defaultPPOption :: PPOption
• verbosePPOption :: PPOption
• ppOption :: IOption -> PPOption
• ppOptionIst :: IState -> PPOption
• data LanguageExt
  • = TypeProviders
  • | ErrorReflection
• data OutputMode
  • = RawOutput Handle
  • | IdeMode Integer Handle
• data ConsoleWidth
  • = InfinitelyWide
  • | ColsWide Int
  • | AutomaticWidth
• data DefaultTotality
  • = DefaultCheckingTotal
  • | DefaultCheckingPartial
  • | DefaultCheckingCovering
• data IState = IState {
  • tt_ctxt :: Context
  • idris_constraints :: Set ConstraintFC
  • idris_infixes :: [FixDecl]
  • idris_implicits :: Ctxt [PArg]
  • idris_statics :: Ctxt [Bool]
  • idris_classes :: Ctxt ClassInfo
  • idris_openimpls :: [Name]
  • idris_records :: Ctxt RecordInfo
  • idris_dsls :: Ctxt DSL
  • idris_optimisation :: Ctxt OptInfo
  • idris_datatypes :: Ctxt TypeInfo
  • idris_namehints :: Ctxt [Name]
  • idris_patdefs :: Ctxt ([([(Name, Term)], Term, Term)], [PTerm])
  • idris_flags :: Ctxt [FnOpt]
  • idris_callgraph :: Ctxt CGInfo
  • idris_docstrings :: Ctxt (Docstring DocTerm, [(Name, Docstring DocTerm)])
  • idris_moduledocs :: Ctxt (Docstring DocTerm)
  • idris_tyinfodata :: Ctxt TIData
  • idris_fninfo :: Ctxt FnInfo
  • idris_transforms :: Ctxt [(Term, Term)]
  • idris_autohints :: Ctxt [Name]
  • idris_totcheck :: [(FC, Name)]
  • idris_defertotcheck :: [(FC, Name)]
  • idris_totcheckfail :: [(FC, String)]
  • idris_options :: IOption
  • idris_name :: Int
  • idris_lineapps :: [((FilePath, Int), PTerm)]
  • idris_metavars :: [(Name, (Maybe Name, Int, [Name], Bool, Bool))]
  • idris_coercions :: [Name]
  • idris_errRev :: [(Term, Term)]
  • syntax_rules :: SyntaxRules
  • syntax_keywords :: [String]
  • imported :: [FilePath]
  • idris_scprims :: [(Name, (Int, PrimFn))]
  • idris_objs :: [(Codegen, FilePath)]
  • idris_libs :: [(Codegen, String)]
  • idris_cgflags :: [(Codegen, String)]
  • idris_hdrs :: [(Codegen, String)]
  • idris_imported :: [(FilePath, Bool)]
  • proof_list :: [(Name, (Bool, [String]))]
  • errSpan :: Maybe FC
  • parserWarnings :: [(FC, Err)]
  • lastParse :: Maybe Name
  • indent_stack :: [Int]
  • brace_stack :: [Maybe Int]
  • lastTokenSpan :: Maybe FC
  • idris_parsedSpan :: Maybe FC
  • hide_list :: Ctxt Accessibility
  • default_access :: Accessibility
  • default_total :: DefaultTotality
  • ibc_write :: [IBCWrite]
  • compiled_so :: Maybe String
  • idris_dynamic_libs :: [DynamicLib]
  • idris_language_extensions :: [LanguageExt]
  • idris_outputmode :: OutputMode
  • idris_colourRepl :: Bool
  • idris_colourTheme :: ColourTheme
  • idris_errorhandlers :: [Name]
  • idris_nameIdx :: (Int, Ctxt (Int, Name))
  • idris_function_errorhandlers :: Ctxt (Map Name (Set Name))
  • module_aliases :: Map [Text] [Text]
  • idris_consolewidth :: ConsoleWidth
  • idris_postulates :: Set Name
  • idris_externs :: Set (Name, Int)
  • idris_erasureUsed :: [(Name, Int)]
  • idris_whocalls :: Maybe (Map Name [Name])
  • idris_callswho :: Maybe (Map Name [Name])
  • idris_repl_defs :: [Name]
  • elab_stack :: [(Name, Bool)]
  • idris_symbols :: Map Name Name
  • idris_exports :: [Name]
  • idris_highlightedRegions :: [(FC, OutputAnnotation)]
  • idris_parserHighlights :: [(FC, OutputAnnotation)]
  • idris_deprecated :: Ctxt String
  • idris_inmodule :: Set Name
  • idris_ttstats :: Map Term (Int, Term)
  • idris_fragile :: Ctxt String
  }
• data SizeChange
  • = Smaller
  • | Same
  • | Bigger
  • | Unknown
• type SCGEntry = (Name, [Maybe (Int, SizeChange)])
• type UsageReason = (Name, Int)
• data CGInfo = CGInfo {
  • calls :: [Name]
  • scg :: [SCGEntry]
  • usedpos :: [(Int, [UsageReason])]
  }
• primDefs :: [Name]
• data IBCWrite
  • = IBCFix FixDecl
  • | IBCImp Name
  • | IBCStatic Name
  • | IBCClass Name
  • | IBCRecord Name
  • | IBCInstance Bool Bool Name Name
  • | IBCDSL Name
  • | IBCData Name
  • | IBCOpt Name
  • | IBCMetavar Name
  • | IBCSyntax Syntax
  • | IBCKeyword String
  • | IBCImport (Bool, FilePath)
  • | IBCImportDir FilePath
  • | IBCObj Codegen FilePath
  • | IBCLib Codegen String
  • | IBCCGFlag Codegen String
  • | IBCDyLib String
  • | IBCHeader Codegen String
  • | IBCAccess Name Accessibility
  • | IBCMetaInformation Name MetaInformation
  • | IBCTotal Name Totality
  • | IBCInjective Name Injectivity
  • | IBCFlags Name [FnOpt]
  • | IBCFnInfo Name FnInfo
  • | IBCTrans Name (Term, Term)
  • | IBCErrRev (Term, Term)
  • | IBCCG Name
  • | IBCDoc Name
  • | IBCCoercion Name
  • | IBCDef Name
  • | IBCNameHint (Name, Name)
  • | IBCLineApp FilePath Int PTerm
  • | IBCErrorHandler Name
  • | IBCFunctionErrorHandler Name Name Name
  • | IBCPostulate Name
  • | IBCExtern (Name, Int)
  • | IBCTotCheckErr FC String
  • | IBCParsedRegion FC
  • | IBCModDocs Name
  • | IBCUsage (Name, Int)
  • | IBCExport Name
  • | IBCAutoHint Name Name
  • | IBCDeprecate Name String
  • | IBCFragile Name String
• idrisInit :: IState
• type Idris = StateT IState (ExceptT Err IO)
• catchError :: Idris a -> (Err -> Idris a) -> Idris a
• throwError :: Err -> Idris a
• data Codegen
  • = Via IRFormat String
  • | Bytecode
• data IRFormat
  • = IBCFormat
  • | JSONFormat
• data HowMuchDocs
  • = FullDocs
  • | OverviewDocs
• data Command
  • = Quit
  • | Help
  • | Eval PTerm
  • | NewDefn [PDecl]
  • | Undefine [Name]
  • | Check PTerm
  • | Core PTerm
  • | DocStr (Either Name Const) HowMuchDocs
  • | TotCheck Name
  • | Reload
  • | Watch
  • | Load FilePath (Maybe Int)
  • | ChangeDirectory FilePath
  • | ModImport String
  • | Edit
  • | Compile Codegen String
  • | Execute PTerm
  • | ExecVal PTerm
  • | Metavars
  • | Prove Bool Name
  • | AddProof (Maybe Name)
  • | RmProof Name
  • | ShowProof Name
  • | Proofs
  • | Universes
  • | LogLvl Int
  • | LogCategory [LogCat]
  • | Spec PTerm
  • | WHNF PTerm
  • | TestInline PTerm
  • | Defn Name
  • | Missing Name
  • | DynamicLink FilePath
  • | ListDynamic
  • | Pattelab PTerm
  • | Search [String] PTerm
  • | CaseSplitAt Bool Int Name
  • | AddClauseFrom Bool Int Name
  • | AddProofClauseFrom Bool Int Name
  • | AddMissing Bool Int Name
  • | MakeWith Bool Int Name
  • | MakeCase Bool Int Name
  • | MakeLemma Bool Int Name
  • | DoProofSearch Bool Bool Int Name [Name]
  • | SetOpt Opt
  • | UnsetOpt Opt
  • | NOP
  • | SetColour ColourType IdrisColour
  • | ColourOn
  • | ColourOff
  • | ListErrorHandlers
  • | SetConsoleWidth ConsoleWidth
  • | SetPrinterDepth (Maybe Int)
  • | Apropos [String] String
  • | WhoCalls Name
  • | CallsWho Name
  • | Browse [String]
  • | MakeDoc String
  • | Warranty
  • | PrintDef Name
  • | PPrint OutputFmt Int PTerm
  • | TransformInfo Name
  • | DebugInfo Name
  • | DebugUnify PTerm PTerm
• data OutputFmt
  • = HTMLOutput
  • | LaTeXOutput
• data LogCat
  • = IParse
  • | IElab
  • | ICodeGen
  • | IErasure
  • | ICoverage
  • | IIBC
• strLogCat :: LogCat -> String
• codegenCats :: [LogCat]
• parserCats :: [LogCat]
• elabCats :: [LogCat]
• loggingCatsStr :: String
• data Opt
  • = Filename String
  • | Quiet
  • | NoBanner
  • | ColourREPL Bool
  • | Idemode
  • | IdemodeSocket
  • | ShowLibs
  • | ShowLibdir
  • | ShowIncs
  • | ShowPkgs
  • | ShowLoggingCats
  • | NoBasePkgs
  • | NoPrelude
  • | NoBuiltins
  • | NoREPL
  • | OLogging Int
  • | OLogCats [LogCat]
  • | Output String
  • | Interface
  • | TypeCase
  • | TypeInType
  • | DefaultTotal
  • | DefaultPartial
  • | WarnPartial
  • | WarnReach
  • | EvalTypes
  • | NoCoverage
  • | ErrContext
  • | ShowImpl
  • | Verbose
  • | Port String
  • | IBCSubDir String
  • | ImportDir String
  • | PkgBuild String
  • | PkgInstall String
  • | PkgClean String
  • | PkgCheck String
  • | PkgREPL String
  • | PkgMkDoc String
  • | PkgTest String
  • | PkgIndex FilePath
  • | WarnOnly
  • | Pkg String
  • | BCAsm String
  • | DumpDefun String
  • | DumpCases String
  • | UseCodegen Codegen
  • | CodegenArgs String
  • | OutputTy OutputType
  • | Extension LanguageExt
  • | InterpretScript String
  • | EvalExpr String
  • | TargetTriple String
  • | TargetCPU String
  • | OptLevel Int
  • | AddOpt Optimisation
  • | RemoveOpt Optimisation
  • | Client String
  • | ShowOrigErr
  • | AutoWidth
  • | AutoSolve
  • | UseConsoleWidth ConsoleWidth
  • | DumpHighlights
  • | DesugarNats
  • | NoElimDeprecationWarnings
  • | NoOldTacticDeprecationWarnings
• data ElabShellCmd
  • = EQED
  • | EAbandon
  • | EUndo
  • | EProofState
  • | EProofTerm
  • | EEval PTerm
  • | ECheck PTerm
  • | ESearch PTerm
  • | EDocStr (Either Name Const)
• data Fixity
  • = Infixl {
    • prec :: Int
    }
  • | Infixr {
    • prec :: Int
    }
  • | InfixN {
    • prec :: Int
    }
  • | PrefixN {
    • prec :: Int
    }
• data FixDecl = Fix Fixity String
• data Static
  • = Static
  • | Dynamic
• data Plicity
  • = Imp {
    • pargopts :: [ArgOpt]
    • pstatic :: Static
    • pparam :: Bool
    • pscoped :: Maybe ImplicitInfo
    • pinsource :: Bool
    }
  • | Exp {
    • pargopts :: [ArgOpt]
    • pstatic :: Static
    • pparam :: Bool
    }
  • | Constraint {
    • pargopts :: [ArgOpt]
    • pstatic :: Static
    }
  • | TacImp {
    • pargopts :: [ArgOpt]
    • pstatic :: Static
    • pscript :: PTerm
    }
• is_scoped :: Plicity -> Maybe ImplicitInfo
• impl :: Plicity
• forall_imp :: Plicity
• forall_constraint :: Plicity
• expl :: Plicity
• expl_param :: Plicity
• constraint :: Plicity
• tacimpl :: PTerm -> Plicity
• data FnOpt
  • = Inlinable
  • | TotalFn
  • | PartialFn
  • | CoveringFn
  • | Coinductive
  • | AssertTotal
  • | Dictionary
  • | Implicit
  • | NoImplicit
  • | CExport String
  • | ErrorHandler
  • | ErrorReverse
  • | Reflection
  • | Specialise [(Name, Maybe Int)]
  • | Constructor
  • | AutoHint
  • | PEGenerated
• type FnOpts = [FnOpt]
• inlinable :: FnOpts -> Bool
• dictionary :: FnOpts -> Bool
• data ProvideWhat' t
  • = ProvTerm t t
  • | ProvPostulate t
• type ProvideWhat = ProvideWhat' PTerm
• data PDecl' t
  • = PFix FC Fixity [String]
  • | PTy (Docstring (Either Err t)) [(Name, Docstring (Either Err t))] SyntaxInfo FC FnOpts Name FC t
  • | PPostulate Bool (Docstring (Either Err t)) SyntaxInfo FC FC FnOpts Name t
  • | PClauses FC FnOpts Name [PClause' t]
  • | PCAF FC Name t
  • | PData (Docstring (Either Err t)) [(Name, Docstring (Either Err t))] SyntaxInfo FC DataOpts (PData' t)
  • | PParams FC [(Name, t)] [PDecl' t]
  • | POpenInterfaces FC [Name] [PDecl' t]
  • | PNamespace String FC [PDecl' t]
  • | PRecord (Docstring (Either Err t)) SyntaxInfo FC DataOpts Name FC [(Name, FC, Plicity, t)] [(Name, Docstring (Either Err t))] [(Maybe (Name, FC), Plicity, t, Maybe (Docstring (Either Err t)))] (Maybe (Name, FC)) (Docstring (Either Err t)) SyntaxInfo
  • | PClass (Docstring (Either Err t)) SyntaxInfo FC [(Name, t)] Name FC [(Name, FC, t)] [(Name, Docstring (Either Err t))] [(Name, FC)] [PDecl' t] (Maybe (Name, FC)) (Docstring (Either Err t))
  • | PInstance (Docstring (Either Err t)) [(Name, Docstring (Either Err t))] SyntaxInfo FC [(Name, t)] [Name] Accessibility FnOpts Name FC [t] [(Name, t)] t (Maybe Name) [PDecl' t]
  • | PDSL Name (DSL' t)
  • | PSyntax FC Syntax
  • | PMutual FC [PDecl' t]
  • | PDirective Directive
  • | PProvider (Docstring (Either Err t)) SyntaxInfo FC FC (ProvideWhat' t) Name
  • | PTransform FC Bool t t
  • | PRunElabDecl FC t [String]
• data Directive
  • = DLib Codegen String
  • | DLink Codegen String
  • | DFlag Codegen String
  • | DInclude Codegen String
  • | DHide Name
  • | DFreeze Name
  • | DInjective Name
  • | DAccess Accessibility
  • | DDefault DefaultTotality
  • | DLogging Integer
  • | DDynamicLibs [String]
  • | DNameHint Name FC [(Name, FC)]
  • | DErrorHandlers Name FC Name FC [(Name, FC)]
  • | DLanguage LanguageExt
  • | DDeprecate Name String
  • | DFragile Name String
  • | DAutoImplicits Bool
  • | DUsed FC Name Name
• data RDeclInstructions
  • = RTyDeclInstrs Name FC [PArg] Type
  • | RClausesInstrs Name [([(Name, Term)], Term, Term)]
  • | RAddInstance Name Name
  • | RDatatypeDeclInstrs Name [PArg]
  • | RDatatypeDefnInstrs Name Type [(Name, [PArg], Type)]
• data EState = EState {
  • case_decls :: [(Name, PDecl)]
  • delayed_elab :: [(Int, Elab' EState ())]
  • new_tyDecls :: [RDeclInstructions]
  • highlighting :: [(FC, OutputAnnotation)]
  • auto_binds :: [Name]
  • implicit_warnings :: [(FC, Name)]
  }
• initEState :: EState
• type ElabD a = Elab' EState a
• highlightSource :: FC -> OutputAnnotation -> ElabD ()
• data PClause' t
  • = PClause FC Name t [t] t [PDecl' t]
  • | PWith FC Name t [t] t (Maybe (Name, FC)) [PDecl' t]
  • | PClauseR FC [t] t [PDecl' t]
  • | PWithR FC [t] t (Maybe (Name, FC)) [PDecl' t]
• data PData' t
  • = PDatadecl {
    • d_name :: Name
    • d_name_fc :: FC
    • d_tcon :: t
    • d_cons :: [(Docstring (Either Err PTerm), [(Name, Docstring (Either Err PTerm))], Name, FC, t, FC, [Name])]
    }
  • | PLaterdecl {
    • d_name :: Name
    • d_name_fc :: FC
    • d_tcon :: t
    }
• mapPDataFC :: (FC -> FC) -> (FC -> FC) -> PData -> PData
• type PDecl = PDecl' PTerm
• type PData = PData' PTerm
• type PClause = PClause' PTerm
• mapPDeclFC :: (FC -> FC) -> (FC -> FC) -> PDecl -> PDecl
• declared :: PDecl -> [Name]
• tldeclared :: PDecl -> [Name]
• defined :: PDecl -> [Name]
• updateN :: [(Name, Name)] -> Name -> Name
• updateNs :: [(Name, Name)] -> PTerm -> PTerm
• data PunInfo
  • = IsType
  • | IsTerm
  • | TypeOrTerm
• data PTerm
  • = PQuote Raw
  • | PRef FC [FC] Name
  • | PInferRef FC [FC] Name
  • | PPatvar FC Name
  • | PLam FC Name FC PTerm PTerm
  • | PPi Plicity Name FC PTerm PTerm
  • | PLet FC Name FC PTerm PTerm PTerm
  • | PTyped PTerm PTerm
  • | PApp FC PTerm [PArg]
  • | PWithApp FC PTerm PTerm
  • | PAppImpl PTerm [ImplicitInfo]
  • | PAppBind FC PTerm [PArg]
  • | PMatchApp FC Name
  • | PIfThenElse FC PTerm PTerm PTerm
  • | PCase FC PTerm [(PTerm, PTerm)]
  • | PTrue FC PunInfo
  • | PResolveTC FC
  • | PRewrite FC (Maybe Name) PTerm PTerm (Maybe PTerm)
  • | PPair FC [FC] PunInfo PTerm PTerm
  • | PDPair FC [FC] PunInfo PTerm PTerm PTerm
  • | PAs FC Name PTerm
  • | PAlternative [(Name, Name)] PAltType [PTerm]
  • | PHidden PTerm
  • | PType FC
  • | PUniverse Universe
  • | PGoal FC PTerm Name PTerm
  • | PConstant FC Const
  • | Placeholder
  • | PDoBlock [PDo]
  • | PIdiom FC PTerm
  • | PReturn FC
  • | PMetavar FC Name
  • | PProof [PTactic]
  • | PTactics [PTactic]
  • | PElabError Err
  • | PImpossible
  • | PCoerced PTerm
  • | PDisamb [[Text]] PTerm
  • | PUnifyLog PTerm
  • | PNoImplicits PTerm
  • | PQuasiquote PTerm (Maybe PTerm)
  • | PUnquote PTerm
  • | PQuoteName Name Bool FC
  • | PRunElab FC PTerm [String]
  • | PConstSugar FC PTerm
• data PAltType
  • = ExactlyOne Bool
  • | FirstSuccess
  • | TryImplicit
• mapPTermFC :: (FC -> FC) -> (FC -> FC) -> PTerm -> PTerm
• mapPT :: (PTerm -> PTerm) -> PTerm -> PTerm
• data PTactic' t
  • = Intro [Name]
  • | Intros
  • | Focus Name
  • | Refine Name [Bool]
  • | Rewrite t
  • | DoUnify
  • | Induction t
  • | CaseTac t
  • | Equiv t
  • | Claim Name t
  • | Unfocus
  • | MatchRefine Name
  • | LetTac Name t
  • | LetTacTy Name t t
  • | Exact t
  • | Compute
  • | Trivial
  • | TCInstance
  • | ProofSearch Bool Bool Int (Maybe Name) [Name] [Name]
  • | Solve
  • | Attack
  • | ProofState
  • | ProofTerm
  • | Undo
  • | Try (PTactic' t) (PTactic' t)
  • | TSeq (PTactic' t) (PTactic' t)
  • | ApplyTactic t
  • | ByReflection t
  • | Reflect t
  • | Fill t
  • | GoalType String (PTactic' t)
  • | TCheck t
  • | TEval t
  • | TDocStr (Either Name Const)
  • | TSearch t
  • | Skip
  • | TFail [ErrorReportPart]
  • | Qed
  • | Abandon
  • | SourceFC
• type PTactic = PTactic' PTerm
• data PDo' t
  • = DoExp FC t
  • | DoBind FC Name FC t
  • | DoBindP FC t t [(t, t)]
  • | DoLet FC Name FC t t
  • | DoLetP FC t t
• type PDo = PDo' PTerm
• data PArg' t
  • = PImp {
    • priority :: Int
    • machine_inf :: Bool
    • argopts :: [ArgOpt]
    • pname :: Name
    • getTm :: t
    }
  • | PExp {
    • priority :: Int
    • argopts :: [ArgOpt]
    • pname :: Name
    • getTm :: t
    }
  • | PConstraint {
    • priority :: Int
    • argopts :: [ArgOpt]
    • pname :: Name
    • getTm :: t
    }
  • | PTacImplicit {
    • priority :: Int
    • argopts :: [ArgOpt]
    • pname :: Name
    • getScript :: t
    • getTm :: t
    }
• data ArgOpt
  • = AlwaysShow
  • | HideDisplay
  • | InaccessibleArg
  • | UnknownImp
• pimp :: Name -> t -> Bool -> PArg' t
• pexp :: t -> PArg' t
• pconst :: t -> PArg' t
• ptacimp :: Name -> t -> t -> PArg' t
• type PArg = PArg' PTerm
• highestFC :: PTerm -> Maybe FC
• data ClassInfo = CI {
  • instanceCtorName :: Name
  • class_methods :: [(Name, (Bool, FnOpts, PTerm))]
  • class_defaults :: [(Name, (Name, PDecl))]
  • class_default_superclasses :: [PDecl]
  • class_params :: [Name]
  • class_instances :: [(Name, Bool)]
  • class_determiners :: [Int]
  }
• data RecordInfo = RI {
  • record_parameters :: [(Name, PTerm)]
  • record_constructor :: Name
  • record_projections :: [Name]
  }
• data TIData
  • = TIPartial
  • | TISolution [Term]
• data FnInfo = FnInfo {
  • fn_params :: [Int]
  }
• data OptInfo = Optimise {
  • inaccessible :: [(Int, Name)]
  • detaggable :: Bool
  }
• data DSL' t = DSL {
  • dsl_bind :: t
  • dsl_return :: t
  • dsl_apply :: t
  • dsl_pure :: t
  • dsl_var :: Maybe t
  • index_first :: Maybe t
  • index_next :: Maybe t
  • dsl_lambda :: Maybe t
  • dsl_let :: Maybe t
  • dsl_pi :: Maybe t
  }
• type DSL = DSL' PTerm
• data SynContext
  • = PatternSyntax
  • | TermSyntax
  • | AnySyntax
• data Syntax
  • = Rule [SSymbol] PTerm SynContext
  • | DeclRule [SSymbol] [PDecl]
• syntaxNames :: Syntax -> [Name]
• syntaxSymbols :: Syntax -> [SSymbol]
• data SSymbol
  • = Keyword Name
  • | Symbol String
  • | Binding Name
  • | Expr Name
  • | SimpleExpr Name
• newtype SyntaxRules = SyntaxRules {
  • syntaxRulesList :: [Syntax]
  }
• emptySyntaxRules :: SyntaxRules
• updateSyntaxRules :: [Syntax] -> SyntaxRules -> SyntaxRules
• initDSL :: DSL' PTerm
• data Using
  • = UImplicit Name PTerm
  • | UConstraint Name [Name]
• data SyntaxInfo = Syn {
  • using :: [Using]
  • syn_params :: [(Name, PTerm)]
  • syn_namespace :: [String]
  • no_imp :: [Name]
  • imp_methods :: [Name]
  • decoration :: Name -> Name
  • inPattern :: Bool
  • implicitAllowed :: Bool
  • constraintAllowed :: Bool
  • maxline :: Maybe Int
  • mut_nesting :: Int
  • dsl_info :: DSL
  • syn_in_quasiquote :: Int
  • syn_toplevel :: Bool
  • withAppAllowed :: Bool
  }
• defaultSyntax :: SyntaxInfo
• expandNS :: SyntaxInfo -> Name -> Name
• bi :: FC
• inferTy :: Name
• inferCon :: Name
• inferDecl :: PData' PTerm
• inferOpts :: [t]
• infTerm :: PTerm -> PTerm
• infP :: TT Name
• getInferTerm :: Term -> Term
• getInferType :: Term -> Term
• primNames :: [Name]
• unitTy :: Name
• unitCon :: Name
• falseDoc :: Docstring (Err' t)
• falseTy :: Name
• pairTy :: Name
• pairCon :: Name
• upairTy :: Name
• upairCon :: Name
• eqTy :: Name
• eqCon :: Name
• eqDoc :: Docstring (Either (Err' t) b)
• eqDecl :: PData' PTerm
• eqParamDoc :: [(Name, Docstring (Either (Err' t) b))]
• eqOpts :: [t]
• modDocName :: Name
• sigmaTy :: Name
• sigmaCon :: Name
• piBind :: [(Name, PTerm)] -> PTerm -> PTerm
• piBindp :: Plicity -> [(Name, PTerm)] -> PTerm -> PTerm
• annotationColour :: IState -> OutputAnnotation -> Maybe IdrisColour
• consoleDecorate :: IState -> OutputAnnotation -> String -> String
• isPostulateName :: Name -> IState -> Bool
• prettyImp :: PPOption -> PTerm -> Doc OutputAnnotation
• prettyIst :: IState -> PTerm -> Doc OutputAnnotation
• pprintPTerm :: PPOption -> [(Name, Bool)] -> [Name] -> [FixDecl] -> PTerm -> Doc OutputAnnotation
• basename :: Name -> Name
• isHoleName :: Name -> Bool
• containsHole :: PTerm -> Bool
• prettyName :: Bool -> Bool -> [(Name, Bool)] -> Name -> Doc OutputAnnotation
• showCImp :: PPOption -> PClause -> Doc OutputAnnotation
• showDImp :: PPOption -> PData -> Doc OutputAnnotation
• showDecls :: PPOption -> [PDecl] -> Doc OutputAnnotation
• showDeclImp :: PPOption -> PDecl' PTerm -> Doc OutputAnnotation
• getImps :: [PArg] -> [(Name, PTerm)]
• getExps :: [PArg] -> [PTerm]
• getShowArgs :: [PArg] -> [PArg]
• getConsts :: [PArg] -> [PTerm]
• getAll :: [PArg] -> [PTerm]
• showName :: Maybe IState -> [(Name, Bool)] -> PPOption -> Bool -> Name -> String
• showTm :: IState -> PTerm -> String
• showTmImpls :: PTerm -> String
• showTmOpts :: PPOption -> PTerm -> String
• getPArity :: PTerm -> Int
• allNamesIn :: PTerm -> [Name]
• boundNamesIn :: PTerm -> [Name]
• implicitNamesIn :: [Name] -> IState -> PTerm -> [Name]
• namesIn :: [(Name, PTerm)] -> IState -> PTerm -> [Name]
• usedNamesIn :: [Name] -> IState -> PTerm -> [Name]
• getErasureInfo :: IState -> Name -> [Int]

Documentation