5Note: this is still a fairly raw set of notes taken by David
6Christiansen at Edwin's presentation at the 2013 Idris Developers
7Meeting. They're in the process of turning into a useful guide - feel
10This document assumes that you are already familiar with Idris. It is
11intended for those who want to work on the internals.
13People looking to develop new back ends may want to look at [[Idris back
14end IRs\|Idris-back-end-IRs]]
19Idris is compiled to a simple, explicit core language. This core
20language is called TT because it looks a bit like a Π. It's a minimal
21language, with a locally nameless representation. That is, local
22variables are represented with de Bruijn indices and globally-defined
23constants are represented with names.
25The ``TT`` datatype uses a trick that is common in the Idris code: it is
26polymorphic over the type of names stored in it, and it derives
27``Functor``. This allows ``fmap`` to be used as a general-purpose
30There is a general construction for binders, used for λ, Π, and
31let-bindings. These are distinguished using a ``BinderType``.
33During compilation, some terms (especially types) will be erased. This
34is represented using the ``Erased`` constructor of ``TT``. A handy trick
35when generating TT terms is to insert ``Erased`` where a term is
36uniquely determined, as the typechecker will fill it out.
38The constructor ``Proj`` is a result of the optimizer. It is used to
39extract a specific constructor argument, in a more economical way than
40defining a new pattern-matching operation.
42The datatype ``Raw`` represents terms that have not yet been
43typechecked. The typechecker converts a ``Raw`` to a ``TT`` if it can.
48Case trees are used to represent top-level pattern-matching definitions
51Just as with the ``TT`` datatype, the ``deriving Functor`` trick is used
52with ``SC`` and ``CaseAlt`` to get GHC to generate a function for
53mapping over contained terms.
55Constructor cases (``ConCase`` in ``CaseAlt``) refer to numbered
56constructors. Every constructor is numbered 0,1,2,…. At this stage in
57the compiler, the tags are datatype-local. After defunctionalization,
58however, they are made globally unique.
60The ``n+1`` patterns (``SucCase``) and hacky-seeming things are to make
61code fast -- please ask before "cleaning up" the representation.
66This module contains the main evaluator for Idris. The evaluator is used
67both at the REPL and during type checking, where normalised terms need
68to be compared for equality.
70A key datatype in the evaluator is a *context*. Contexts are mappings
71from global names to their values, but they are organized to make
72type-directed disambiguation quick. In particular, the main part of a
73name that a user might type is used as the key, and its values are maps
74from namespaces to actual values.
76The datatype ``Def`` represents a definition in the global context. All
77global names map to this structure.
79``Type`` and ``Term`` are both synonyms for ``TT``.
81Datatypes are represented by a ``TyDecl`` with the appropriate
82``NameType``. A ``Function`` is a global constant term with an annotated
83type, ``Operator`` represents primitives implemented in Haskell, and
84``CaseOp`` represents ordinary pattern-matching definitions. ``CaseOp``
85has four versions for different purposes, and all are saved because
88``CaseInfo``: the ``tc_dictionary`` is because it's a type class
89dictionary which makes totality checking easier.
91The ``normalise*`` functions give different behaviors - but
92``normalise`` is the most common.
94``normaliseC`` - "resolved" means with names converted to de Bruijn
95indices as appropriate.
97``normaliseAll`` - reduce everything, even if it's non-total
99``normaliseTrace`` - special-purpose for debugging
101``simplify`` - reduce the things that are small - the list argument is
102the things to not reduce.
107Standard stuff. Hopefully no changes are necessary.
112Idris definitions are elaborated one by one and turned into the
113corresponding TT. This is done with a tactic language as an EDSL in the
114Elab monad (or Elab' when there's a custom state).
116Lots of plumbing for errors.
118All elaboration is relative to a global context.
120The string in the pair returned by elaborate is log information.
122See JFP paper, but the names don't necessarily map to each other. The
123paper is the "idealized version" without logging, additional state, etc.
125All the tactics take Raws, typechecking happens there.
127claim (x : t) assumes a new x : t.
129PLEASE TIDY THINGS UP!
131proofSearch flag to try' is whether the failure came from a human (so
132fail) or from a machine (so continue)
134Idris-level syntax for providing alternatives explicitly: (\| x, y, z
135\|) try x, y, z in order, and take the first that succeeds.
143Deals with unification. Unification can reply with: - this works - this
144can never work - this will work if these other unification problems work
145out (eg unifying f x with 1)
147match\_unify: same thing as unification except it's just matching name
148against name, term against term. x + y matches to 0 + y with x = 0. Used
149for <== syntax as well as type class resolution.
151Idris/AbsSyntaxTree.hs
152======================
154PTerm is the datatype of Idris syntax. P is for Program. Each PTerm
155turns into a TT term by applying a series of tactics.
157IState is the major interpreter state. The global context is the
160Ctxt maps possibly ambiguous names to their referents.
165This is where the actual elaboration from PTerm to TT happens.
170build is the function that creates a Raw. All the "junk" is to deal with
171things like metavars and so forth. It has to remember what names are
172still to be defined, and it doesn't yet know the type (filled in by
173unificaiton later). Also case expressions have to turn into top-level
176resolveTC is type class resolution.
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