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