Idris Development Notes

• Edwin’s paper, Idris, a General Purpose Dependently Typed Programming Language: Design and Implementation. Covers TT, the elaboration monad, tactic-based elaboration and more.

• Idris’ Internals

• “A Look at the Idris Internals” series by Paul Körbitz.

  • Part I: Overview and Parsing
  • Part II: Taking the Parser for a Spin
  • Part III: From Parsing to Elaboration
  • Part IV: From TT Onward

Backend/Codegen

• Edwin’s paper on backend/codegen: Cross-platform Compilers for Functional Languages.
• Edwin’s example backend/codegen: idris-php.
• Other backends/codegens:
  • mmhelloworld/idris-jvm
  • bamboo/idris-cil
• Idris-backend-IRs
• Levels of backend IR:
  • 1. (IR/case) = ??? FIXME: Does this exist?
  • 1. LDecl (IR/lift) = [Lambda] Lifted Decl = lambda-lifted untyped lambda calculus
  • 1. DDecl (IR/defunc) = Defunctionalised Decl = defunctionalised untyped lambda calculus
  • 1. SDecl (IR/ANF) = Simplified Decl = ANF

Abbreviations

PDecl

Program declaration. Essentially top of AST.

PTerm

Program Term. The parameter for PDecl. i.e. type PDecl = PDecl' PTerm.

FC

probably short for FileContext. Contains source positions produced by Parser.

Build times (iMac late 2009)

• Clean build but dependencies already built (Stack, GHC 8.0.1)
  • modularise-ast
    • 891.74 real 819.78 user 29.68 sys — (14.86 minutes)
    • 922.26 real 828.76 user 33.22 sys — (15.37 minutes)
    • 693.39 real 659.26 user 22.45 sys — (11.56 minutes)
    • 753.93 real 687.58 user 25.12 sys — (12.57 minutes)
  • master
    • 770.54 real 669.36 user 26.31 sys — (12.84 minutes)

AST (and perhaps Core) Refactoring

• [X] importing Idris.AbsSyntaxTree
  • [X] src/Idris/AbsSyntax.hs:import Idris.AbsSyntaxTree
  • [X] src/Idris/ASTUtils.hs:import Idris.AbsSyntaxTree
  • [X] src/Idris/CaseSplit.hs:import Idris.AbsSyntaxTree
  • [X] src/Idris/CmdOptions.hs:import Idris.AbsSyntaxTree
  • [X] src/Idris/Completion.hs:import Idris.AbsSyntaxTree
  • [X] src/Idris/Core/Execute.hs:import Idris.AbsSyntaxTree
  • [X] src/Idris/DataOpts.hs:import Idris.AbsSyntaxTree
  • [X] src/Idris/DeepSeq.hs:import Idris.AbsSyntaxTree
  • [X] src/Idris/Elab/Rewrite.hs:import Idris.AbsSyntaxTree
  • [X] src/Idris/Elab/Term.hs:import Idris.AbsSyntaxTree
  • [X] src/Idris/Package/Common.hs:import Idris.AbsSyntaxTree
  • [X] src/Idris/Package/Parser.hs:import Idris.AbsSyntaxTree
  • [X] src/Idris/Prover.hs:import Idris.AbsSyntaxTree
  • [X] src/Idris/Providers.hs:import Idris.AbsSyntaxTree
  • [X] src/Idris/Reflection.hs:import Idris.AbsSyntaxTree
  • [X] src/Idris/REPL/Browse.hs:import Idris.AbsSyntaxTree
  • [X] src/Idris/REPL/Commands.hs:import Idris.AbsSyntaxTree
  • [X] src/Idris/TypeSearch.hs:import Idris.AbsSyntaxTree
  • [X] src/IRTS/Compiler.hs:import Idris.AbsSyntaxTree
• [X] importing Idris.AbsSyntax
  • [X] src/Idris/Apropos.hs:import Idris.AbsSyntax
  • [X] src/Idris/CaseSplit.hs:import Idris.AbsSyntax (
  • [X] src/Idris/Chaser.hs:import Idris.AbsSyntax
  • [X] src/Idris/CmdOptions.hs:import Idris.AbsSyntax (
  • [X] src/Idris/Completion.hs:import Idris.AbsSyntax (runIO)
  • [X] src/Idris/Core/Execute.hs:import Idris.AbsSyntax (getIState, getContext)
  • [X] src/Idris/Coverage.hs:import Idris.AbsSyntax
  • [X] src/Idris/DataOpts.hs:import Idris.AbsSyntax ()
  • [X] src/Idris/Delaborate.hs:import Idris.AbsSyntax
  • [X] src/Idris/Directives.hs:import Idris.AbsSyntax
  • [X] src/Idris/Docs.hs:import Idris.AbsSyntax (
  • [X] src/Idris/DSL.hs:import Idris.AbsSyntax
  • [X] src/Idris/Elab/AsPat.hs:import Idris.AbsSyntax
  • [X] src/Idris/Elab/Clause.hs:import Idris.AbsSyntax
  • [X] src/Idris/Elab/Data.hs:import Idris.AbsSyntax
  • [X] src/Idris/Elab/Implementation.hs:import Idris.AbsSyntax
  • [X] src/Idris/Elab/Interface.hs:import Idris.AbsSyntax
  • [X] src/Idris/Elab/Provider.hs:import Idris.AbsSyntax
  • [X] src/Idris/Elab/Quasiquote.hs:import Idris.AbsSyntax
  • [X] src/Idris/Elab/Record.hs:import Idris.AbsSyntax
  • [X] src/Idris/Elab/Rewrite.hs:import Idris.AbsSyntax (addImplBound, getIState)
  • [X] src/Idris/Elab/RunElab.hs:import Idris.AbsSyntax
  • [X] src/Idris/Elab/Term.hs:import Idris.AbsSyntax (
  • [X] src/Idris/Elab/Transform.hs:import Idris.AbsSyntax
  • [X] src/Idris/Elab/Type.hs:import Idris.AbsSyntax
  • [X] src/Idris/Elab/Utils.hs:import Idris.AbsSyntax
  • [X] src/Idris/Elab/Value.hs:import Idris.AbsSyntax
  • [X] src/Idris/ElabDecls.hs:import Idris.AbsSyntax
  • [X] src/Idris/Erasure.hs:import Idris.AbsSyntax
  • [X] src/Idris/Error.hs:import Idris.AbsSyntax
  • [X] src/Idris/ErrReverse.hs:import Idris.AbsSyntax
  • [X] src/Idris/IBC.hs:import Idris.AbsSyntax
  • [X] src/Idris/IdrisDoc.hs:import Idris.AbsSyntax
  • [X] src/Idris/Imports.hs:import Idris.AbsSyntax
  • [X] src/Idris/Info.hs:import Idris.AbsSyntax (loggingCatsStr)
  • [X] src/Idris/Inliner.hs:import Idris.AbsSyntax
  • [X] src/Idris/Interactive.hs:import Idris.AbsSyntax
  • [X] src/Idris/Main.hs:import Idris.AbsSyntax
  • [X] src/Idris/ModeCommon.hs:import Idris.AbsSyntax
  • [X] src/Idris/Output.hs:import Idris.AbsSyntax
  • [X] src/Idris/Package.hs:import Idris.AbsSyntax
  • [X] src/Idris/Parser/Data.hs:import Idris.AbsSyntax
  • [X] src/Idris/Parser/Expr.hs:import Idris.AbsSyntax
  • [X] src/Idris/Parser/Helpers.hs:import Idris.AbsSyntax
  • [X] src/Idris/Parser/Ops.hs:import Idris.AbsSyntax
  • [X] src/Idris/Parser.hs:import Idris.AbsSyntax hiding (namespace, params)
  • [X] src/Idris/PartialEval.hs:import Idris.AbsSyntax
  • [X] src/Idris/Primitives.hs:import Idris.AbsSyntax
  • [X] src/Idris/ProofSearch.hs:import Idris.AbsSyntax
  • [X] src/Idris/Prover.hs:import Idris.AbsSyntax
  • [X] src/Idris/REPL/Browse.hs:import Idris.AbsSyntax (getContext)
  • [X] src/Idris/REPL/Parser.hs:import Idris.AbsSyntax
  • [X] src/Idris/REPL.hs:import Idris.AbsSyntax
  • [X] src/Idris/Transforms.hs:import Idris.AbsSyntax
  • [X] src/Idris/TypeSearch.hs:import Idris.AbsSyntax (addUsingConstraints, addImpl, getIState, putIState, implicit)
  • [X] src/Idris/WhoCalls.hs:import Idris.AbsSyntax
  • [X] src/IRTS/CodegenC.hs:import Idris.AbsSyntax
  • [X] src/IRTS/CodegenJavaScript.hs:import Idris.AbsSyntax hiding (TypeCase)
  • [X] src/IRTS/Compiler.hs:import Idris.AbsSyntax
  • [X] src/IRTS/Compiler.hs:import qualified Idris.AbsSyntax as AbsSyntax
  • [X] src/IRTS/Exports.hs:import Idris.AbsSyntax

Potential refactorings:

• Can we lift Opt and option processing functions from AbsSyntax?
  • made obvious in Idris.Main.
• Can we lift OutputAnnotations from Core.TT?
• Can we lift Name and associated functions from Core.TT?

Errors

See if this happens on master.

OK (5.88s) ffi009: Error: test/ffi009 idris: Foreign Function calls cannot be partially applied, without being inlined. CallStack (from HasCallStack): error, called at src/IRTS/CodegenC.hs:343:36 in idris-0.12.3-LoUXGyrDJU677RY2CaNGaq:IRTS.CodegenC clang: warning: argument unused during compilation: ‘-fno-strict-overflow’

OK (6.91s) Folding folding001: OK (4.73s)