Idris.AbsSyntaxTree

Synopsis

• data IOption = IOption {
  • opt_logLevel :: Int
  • 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_optLevel :: Word
  • opt_cmdline :: [Opt]
  }
• defaultOpts :: IOption
• data LanguageExt
  • = TypeProviders
  • | ErrorReflection
• data OutputMode
  • = RawOutput
  • | IdeSlave Integer
• data IState = IState {
  • tt_ctxt :: Context
  • idris_constraints :: [(UConstraint, FC)]
  • idris_infixes :: [FixDecl]
  • idris_implicits :: Ctxt [PArg]
  • idris_statics :: Ctxt [Bool]
  • idris_classes :: Ctxt ClassInfo
  • idris_dsls :: Ctxt DSL
  • idris_optimisation :: Ctxt OptInfo
  • idris_datatypes :: Ctxt TypeInfo
  • idris_patdefs :: Ctxt ([([Name], Term, Term)], [PTerm])
  • idris_flags :: Ctxt [FnOpt]
  • idris_callgraph :: Ctxt CGInfo
  • idris_calledgraph :: Ctxt [Name]
  • idris_docstrings :: Ctxt String
  • idris_totcheck :: [(FC, Name)]
  • idris_defertotcheck :: [(FC, Name)]
  • idris_options :: IOption
  • idris_name :: Int
  • idris_lineapps :: [((FilePath, Int), PTerm)]
  • idris_metavars :: [(Name, (Maybe Name, Int, Bool))]
  • idris_coercions :: [Name]
  • idris_transforms :: [(Term, Term)]
  • syntax_rules :: [Syntax]
  • 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)]
  • proof_list :: [(Name, [String])]
  • errLine :: Maybe Int
  • lastParse :: Maybe Name
  • indent_stack :: [Int]
  • brace_stack :: [Maybe Int]
  • hide_list :: [(Name, Maybe Accessibility)]
  • default_access :: Accessibility
  • default_total :: Bool
  • 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_outh :: Handle
  }
• data SizeChange
  • = Smaller
  • | Same
  • | Bigger
  • | Unknown
• type SCGEntry = (Name, [Maybe (Int, SizeChange)])
• data CGInfo = CGInfo {
  • argsdef :: [Name]
  • calls :: [(Name, [[Name]])]
  • scg :: [SCGEntry]
  • argsused :: [Name]
  • unusedpos :: [Int]
  }
• primDefs :: [Name]
• data IBCWrite
  • = IBCFix FixDecl
  • | IBCImp Name
  • | IBCStatic Name
  • | IBCClass Name
  • | IBCInstance Bool Name Name
  • | IBCDSL Name
  • | IBCData Name
  • | IBCOpt Name
  • | IBCSyntax Syntax
  • | IBCKeyword String
  • | IBCImport FilePath
  • | IBCObj Codegen FilePath
  • | IBCLib Codegen String
  • | IBCCGFlag Codegen String
  • | IBCDyLib String
  • | IBCHeader Codegen String
  • | IBCAccess Name Accessibility
  • | IBCTotal Name Totality
  • | IBCFlags Name [FnOpt]
  • | IBCTrans (Term, Term)
  • | IBCCG Name
  • | IBCDoc Name
  • | IBCCoercion Name
  • | IBCDef Name
  • | IBCLineApp FilePath Int PTerm
• idrisInit :: IState
• type Idris = StateT IState (ErrorT Err IO)
• data Codegen
  • = ViaC
  • | ViaJava
  • | ViaNode
  • | ViaJavaScript
  • | ViaLLVM
  • | Bytecode
• data Command
  • = Quit
  • | Help
  • | Eval PTerm
  • | Check PTerm
  • | DocStr Name
  • | TotCheck Name
  • | Reload
  • | Load FilePath
  • | ChangeDirectory FilePath
  • | ModImport String
  • | Edit
  • | Compile Codegen String
  • | Execute
  • | ExecVal PTerm
  • | Metavars
  • | Prove Name
  • | AddProof (Maybe Name)
  • | RmProof Name
  • | ShowProof Name
  • | Proofs
  • | Universes
  • | LogLvl Int
  • | Spec PTerm
  • | HNF PTerm
  • | TestInline PTerm
  • | Defn Name
  • | Info Name
  • | Missing Name
  • | DynamicLink FilePath
  • | ListDynamic
  • | Pattelab PTerm
  • | DebugInfo Name
  • | Search PTerm
  • | CaseSplitAt Bool Int Name
  • | AddClauseFrom Bool Int Name
  • | AddProofClauseFrom Bool Int Name
  • | AddMissing Bool Int Name
  • | MakeWith Bool Int Name
  • | DoProofSearch Bool Int Name [Name]
  • | SetOpt Opt
  • | UnsetOpt Opt
  • | NOP
  • | SetColour ColourType IdrisColour
  • | ColourOn
  • | ColourOff
• data Opt
  • = Filename String
  • | Ver
  • | Usage
  • | Quiet
  • | NoBanner
  • | ColourREPL Bool
  • | Ideslave
  • | ShowLibs
  • | ShowLibdir
  • | ShowIncs
  • | NoBasePkgs
  • | NoPrelude
  • | NoBuiltins
  • | NoREPL
  • | OLogging Int
  • | Output String
  • | TypeCase
  • | TypeInType
  • | DefaultTotal
  • | DefaultPartial
  • | WarnPartial
  • | NoCoverage
  • | ErrContext
  • | ShowImpl
  • | Verbose
  • | IBCSubDir String
  • | ImportDir String
  • | PkgBuild String
  • | PkgInstall String
  • | PkgClean String
  • | WarnOnly
  • | Pkg String
  • | BCAsm String
  • | DumpDefun String
  • | DumpCases String
  • | UseCodegen Codegen
  • | OutputTy OutputType
  • | Extension LanguageExt
  • | InterpretScript String
  • | TargetTriple String
  • | TargetCPU String
  • | OptLevel Word
  • | Client String
• 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 {
    • plazy :: Bool
    • pstatic :: Static
    • pdocstr :: String
    • pparam :: Bool
    }
  • | Exp {
    • plazy :: Bool
    • pstatic :: Static
    • pdocstr :: String
    • pparam :: Bool
    }
  • | Constraint {
    • plazy :: Bool
    • pstatic :: Static
    • pdocstr :: String
    }
  • | TacImp {
    • plazy :: Bool
    • pstatic :: Static
    • pscript :: PTerm
    • pdocstr :: String
    }
• impl :: Plicity
• expl :: Plicity
• expl_param :: Plicity
• constraint :: Plicity
• tacimpl :: PTerm -> Plicity
• data FnOpt
  • = Inlinable
  • | TotalFn
  • | PartialFn
  • | Coinductive
  • | AssertTotal
  • | Dictionary
  • | Implicit
  • | CExport String
  • | Reflection
  • | Specialise [(Name, Maybe Int)]
• type FnOpts = [FnOpt]
• inlinable :: FnOpts -> Bool
• dictionary :: FnOpts -> Bool
• data PDecl' t
  • = PFix FC Fixity [String]
  • | PTy String SyntaxInfo FC FnOpts Name t
  • | PPostulate String SyntaxInfo FC FnOpts Name t
  • | PClauses FC FnOpts Name [PClause' t]
  • | PCAF FC Name t
  • | PData String SyntaxInfo FC Bool (PData' t)
  • | PParams FC [(Name, t)] [PDecl' t]
  • | PNamespace String [PDecl' t]
  • | PRecord String SyntaxInfo FC Name t String Name t
  • | PClass String SyntaxInfo FC [t] Name [(Name, t)] [PDecl' t]
  • | PInstance SyntaxInfo FC [t] Name [t] t (Maybe Name) [PDecl' t]
  • | PDSL Name (DSL' t)
  • | PSyntax FC Syntax
  • | PMutual FC [PDecl' t]
  • | PDirective (Idris ())
  • | PProvider SyntaxInfo FC Name t t
  • | PTransform FC Bool t t
• type ElabD a = Elab' [PDecl] a
• data PClause' t
  • = PClause FC Name t [t] t [PDecl' t]
  • | PWith FC Name t [t] t [PDecl' t]
  • | PClauseR FC [t] t [PDecl' t]
  • | PWithR FC [t] t [PDecl' t]
• data PData' t
  • = PDatadecl {
    • d_name :: Name
    • d_tcon :: t
    • d_cons :: [(String, Name, t, FC)]
    }
  • | PLaterdecl {
    • d_name :: Name
    • d_tcon :: t
    }
• type PDecl = PDecl' PTerm
• type PData = PData' PTerm
• type PClause = PClause' PTerm
• declared :: PDecl -> [Name]
• tldeclared :: PDecl -> [Name]
• defined :: PDecl -> [Name]
• updateN :: [(Name, Name)] -> Name -> Name
• updateNs :: [(Name, Name)] -> PTerm -> PTerm
• data PTerm
  • = PQuote Raw
  • | PRef FC Name
  • | PInferRef FC Name
  • | PPatvar FC Name
  • | PLam Name PTerm PTerm
  • | PPi Plicity Name PTerm PTerm
  • | PLet Name PTerm PTerm PTerm
  • | PTyped PTerm PTerm
  • | PApp FC PTerm [PArg]
  • | PAppBind FC PTerm [PArg]
  • | PMatchApp FC Name
  • | PCase FC PTerm [(PTerm, PTerm)]
  • | PTrue FC
  • | PFalse FC
  • | PRefl FC PTerm
  • | PResolveTC FC
  • | PEq FC PTerm PTerm
  • | PRewrite FC PTerm PTerm (Maybe PTerm)
  • | PPair FC PTerm PTerm
  • | PDPair FC PTerm PTerm PTerm
  • | PAlternative Bool [PTerm]
  • | PHidden PTerm
  • | PType
  • | PGoal FC PTerm Name PTerm
  • | PConstant Const
  • | Placeholder
  • | PDoBlock [PDo]
  • | PIdiom FC PTerm
  • | PReturn FC
  • | PMetavar Name
  • | PProof [PTactic]
  • | PTactics [PTactic]
  • | PElabError Err
  • | PImpossible
  • | PCoerced PTerm
  • | PUnifyLog PTerm
  • | PNoImplicits PTerm
• mapPT :: (PTerm -> PTerm) -> PTerm -> PTerm
• data PTactic' t
  • = Intro [Name]
  • | Intros
  • | Focus Name
  • | Refine Name [Bool]
  • | Rewrite t
  • | Equiv t
  • | MatchRefine Name
  • | LetTac Name t
  • | LetTacTy Name t t
  • | Exact t
  • | Compute
  • | Trivial
  • | ProofSearch (Maybe Name) Name [Name]
  • | Solve
  • | Attack
  • | ProofState
  • | ProofTerm
  • | Undo
  • | Try (PTactic' t) (PTactic' t)
  • | TSeq (PTactic' t) (PTactic' t)
  • | ApplyTactic t
  • | Reflect t
  • | Fill t
  • | GoalType String (PTactic' t)
  • | Qed
  • | Abandon
• type PTactic = PTactic' PTerm
• data PDo' t
  • = DoExp FC t
  • | DoBind FC Name t
  • | DoBindP FC t t
  • | DoLet FC Name t t
  • | DoLetP FC t t
• type PDo = PDo' PTerm
• data PArg' t
  • = PImp {
    • priority :: Int
    • machine_inf :: Bool
    • lazyarg :: Bool
    • pname :: Name
    • getTm :: t
    • pargdoc :: String
    }
  • | PExp {
    • priority :: Int
    • lazyarg :: Bool
    • getTm :: t
    • pargdoc :: String
    }
  • | PConstraint {
    • priority :: Int
    • lazyarg :: Bool
    • getTm :: t
    • pargdoc :: String
    }
  • | PTacImplicit {
    • priority :: Int
    • lazyarg :: Bool
    • pname :: Name
    • getScript :: t
    • getTm :: t
    • pargdoc :: String
    }
• pimp :: Name -> t -> Bool -> PArg' t
• pexp :: t -> PArg' t
• pconst :: t -> PArg' t
• ptacimp :: Name -> t -> t -> PArg' t
• type PArg = PArg' PTerm
• data ClassInfo = CI {
  • instanceName :: Name
  • class_methods :: [(Name, (FnOpts, PTerm))]
  • class_defaults :: [(Name, (Name, PDecl))]
  • class_params :: [Name]
  • class_instances :: [Name]
  }
• data OptInfo = Optimise {
  • collapsible :: Bool
  • isnewtype :: Bool
  • forceable :: [Int]
  • recursive :: [Int]
  }
• data TypeInfo = TI {
  • con_names :: [Name]
  • codata :: Bool
  • param_pos :: [Int]
  }
• 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
  }
• type DSL = DSL' PTerm
• data SynContext
  • = PatternSyntax
  • | TermSyntax
  • | AnySyntax
• data Syntax = Rule [SSymbol] PTerm SynContext
• data SSymbol
  • = Keyword Name
  • | Symbol String
  • | Binding Name
  • | Expr Name
  • | SimpleExpr Name
• 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]
  • decoration :: Name -> Name
  • inPattern :: Bool
  • implicitAllowed :: Bool
  • dsl_info :: DSL
  }
• defaultSyntax :: SyntaxInfo
• expandNS :: SyntaxInfo -> Name -> Name
• showDeclImp :: Bool -> PDecl' PTerm -> [Char]
• showCImp :: Bool -> PClause -> String
• showDImp :: Bool -> PData -> String
• getImps :: [PArg] -> [(Name, PTerm)]
• getExps :: [PArg] -> [PTerm]
• getConsts :: [PArg] -> [PTerm]
• getAll :: [PArg] -> [PTerm]
• prettyImp :: Bool -> PTerm -> Doc
• showName :: Maybe IState -> [(Name, Bool)] -> Bool -> Bool -> Name -> String
• showImp :: Maybe IState -> Bool -> Bool -> PTerm -> String
• getPArity :: PTerm -> Int
• allNamesIn :: PTerm -> [Name]
• namesIn :: [(Name, PTerm)] -> IState -> PTerm -> [Name]
• usedNamesIn :: [Name] -> IState -> PTerm -> [Name]

Documentation