<commit_before>***********************
Implementation Overview
***********************

These are some unsorted notes on aspects of the implementation. Sketchy, and
not always completely up to date, but hopefully give some hints as to what's
going on and some ideas where to look in the code to see how certain features
work.

Introduction
------------

Core language TT (defined in Core.TT), based on quantitative type theory
(see https://bentnib.org/quantitative-type-theory.html). Binders have
"multiplicities" which are either 0, 1 or unlimited.

Terms are indexed over the names in scope so that we know terms are always well
scoped. Values (i.e. normal forms) are defined in Core.Value as NF;
constructors do not evaluate their arguments until explicitly requested.

Elaborate to TT from a higher level language TTImp (defined in ``TTImp.TTImp``),
which is TT with implicit arguments, local function definitions, case blocks,
as patterns, qualified names with automatic type-directed disambiguation, and
proof search.

Elaboration relies on unification (in ``Core.Unify``), which allows postponing
of unification problems. Essentially works the same way as Agda as described
in Ulf Norell's thesis.

General idea is that high level languages will provide a translation to TT.
In the ``Idris/`` namespace we define the high level syntax for Idris, which
translates to TTImp by desugaring operators, do notation, etc.

There is a separate linearity check after elaboration, which updates types of
holes (and is aware of case blocks). This is implemented in
``Core.LinearCheck``. During this check, we also recalculate the multiplicities
in hole applications so that they are displayed appropriately (e.g. if a
linear variable is unused elsewhere, it will always appear with multiplicity
1 in holes).


Where to find things:

* ``Core/`` -- anything related to the core TT, typechecking and unification
* ``TTImp/`` -- anything related to the implicit TT and its elaboration

  + ``TTImp/Elab/`` -- Elaboration state and elaboration of terms 
  + ``TTImp/Interactive/`` -- Interactive editing infrastructure

* ``Parser/`` -- various utilities for parsing and lexing TT and TTImp (and other things)
* ``Utils/`` -- some generally useful utilities
* ``Idris/`` -- anything relating to the high level language, translating to TTImp

  + ``Idris/Elab/`` -- High level construct elaboration machinery (e.g. interfaces)

* ``Compiler/`` -- back ends

The Core Type, and Ref
----------------------
Core is a "monad" (not really, for efficiency reasons, at the moment...)
supporting Errors and IO (I did originally plan to allow restricting this to
some specific IO operations, but haven't yet).  The raw syntax is defined by a
type ``RawImp`` which has a source location at each node, and any errors in
elaboration note the location at the point where the error occurred, as
a file context ``FC``.

``Ref`` is essentially an ``IORef``. Typically we pass them implicitly and use
labels to disambiguate which one we mean. See Core.Core for their
definition. Again, ``IORef`` is for efficiency - even if it would be neater to
use a state monad this turned out to be about 2-3 times faster, so I'm
going with the "ugly" choice...

Term representation
-------------------

Terms in the core language are indexed by a list of the names in scope,
most recently defined first:

::

    data Term : List Name -> Type

This means that terms are always well scoped, and we can use the type system
to keep us right when manipulating names. For example, we have:

::
    Local : FC -> (isLet : Maybe Bool) ->
            (idx : Nat) -> (0 p : IsVar name idx vars) -> Term vars

So local variables are represented by an index into the local context (a de
Bruijn index, ``idx``), and a proof, erased at run time, that the index 
is valid. So everything is de Bruijn indexed, but the type checker still
keeps track of the indices so that we don't have to think too hard!

``Core.TT`` contains various handy tools for manipulating terms with their
indices, such as:

::
    weaken : Term vars -> Term (n :: vars) -- actually in an interface, Weaken
    embed : Term vars -> Term (ns ++ vars) 
    refToLocal : (x : Name) -> -- explicit name of a reference
                 (new : Name) -> -- name to bind as
                 Term vars -> Term (new :: vars)

Note that the types are explicit about when the ``vars`` needs to be passed at
run time, and when it isn't. Mostly where it's needed it's to help with
displaying names, or name generation, rather than any fundamental reason in
the core. In general, this isn't expensive at run time.

Environments, defined in ``Core.Env``, map local variables to binders:

::
    data Env : (tm : List Name -> Type) -> List Name -> Type

A binders is typically a lambda, a pi, or a let (with a value), but can
also be a pattern variable. See the definition of ``TT`` for more details.
Where we have a term, we usually also need an ``Env``.

We also have values, which are in head normal form, and defined in
``Core.Value``:

::
    data NF : List Name -> Type

We can convert a term to a value by normalising...

::
    nf : {vars : _} ->
         Defs -> Env Term vars -> Term vars -> Core (NF vars)

...and back again, by quoting:

::
    quote : {vars : _} ->
            Defs -> Env Term vars -> tm vars -> Core (Term vars)

Both ``nf`` and ``quote`` are defined in ``Core.Normalise``. We don't
always know whether we'll need to work with ``NF`` or ``Term``, so
we also have a "glued" representation, ``Glued vars``, again defined in
``Core.Normalise``, which lazily computes either a ``NF`` or ``Term`` as
required. Elaborating a term returns the type as a ``Glued vars``.

``Term`` separates ``Ref`` (global user defined names) from ``Meta``, which
are globally defined metavariables. For efficiency, metavariables are only
substituted into terms if they have non-0 multiplicity, to preserve sharing as
much as possible.

Unification
-----------
Unification is probably the most important part of the elaboration process,
and infers values for implicit arguments. That is, it finds values for the
things which are referred to by ``Meta`` in ``Term``. It is defined in
``Core.Unify``, as the top level unification function has the following
type:

::
    unify : Unify tm =>
            {vars : _} ->
            {auto c : Ref Ctxt Defs} ->
            {auto u : Ref UST UState} ->
            UnifyInfo ->
            FC -> Env Term vars ->
            tm vars -> tm vars ->
            Core UnifyResult

The ``Unify`` interface is there because it is convenient to be able to
define unification on ``Term`` and ``NF``, as well as ``Closure`` (which
is part of ``NF`` to represent unevaluated arguments to constructors).

This is one place where indexing over ``vars`` is extremely valuable: we
have to keep the environment consistent, so unification won't accidentally
introduce any scoping bugs!

Idris 2 implements pattern unification - see Adam Gundry's thesis for an
accessible introduction.

Context
-------
``Core.Context`` defines all the things needed for TT. Most importantly: Def 
gives definitions of names (case trees, builtins, constructors and
holes, mostly); ``GlobalDef`` is a definition with all the other information
about it (type, visibility, totality, etc); ``Context`` is a context mapping names
to ``GlobalDef``, and ``Defs`` is the core data structure with everything needed to
typecheck more definitions.<commit_msg>Fix formatting<commit_after>***********************
Implementation Overview
***********************

These are some unsorted notes on aspects of the implementation. Sketchy, and
not always completely up to date, but hopefully give some hints as to what's
going on and some ideas where to look in the code to see how certain features
work.

Introduction
------------

Core language TT (defined in Core.TT), based on quantitative type theory
(see https://bentnib.org/quantitative-type-theory.html). Binders have
"multiplicities" which are either 0, 1 or unlimited.

Terms are indexed over the names in scope so that we know terms are always well
scoped. Values (i.e. normal forms) are defined in Core.Value as NF;
constructors do not evaluate their arguments until explicitly requested.

Elaborate to TT from a higher level language TTImp (defined in ``TTImp.TTImp``),
which is TT with implicit arguments, local function definitions, case blocks,
as patterns, qualified names with automatic type-directed disambiguation, and
proof search.

Elaboration relies on unification (in ``Core.Unify``), which allows postponing
of unification problems. Essentially works the same way as Agda as described
in Ulf Norell's thesis.

General idea is that high level languages will provide a translation to TT.
In the ``Idris/`` namespace we define the high level syntax for Idris, which
translates to TTImp by desugaring operators, do notation, etc.

There is a separate linearity check after elaboration, which updates types of
holes (and is aware of case blocks). This is implemented in
``Core.LinearCheck``. During this check, we also recalculate the multiplicities
in hole applications so that they are displayed appropriately (e.g. if a
linear variable is unused elsewhere, it will always appear with multiplicity
1 in holes).


Where to find things:

* ``Core/`` -- anything related to the core TT, typechecking and unification
* ``TTImp/`` -- anything related to the implicit TT and its elaboration

  + ``TTImp/Elab/`` -- Elaboration state and elaboration of terms 
  + ``TTImp/Interactive/`` -- Interactive editing infrastructure

* ``Parser/`` -- various utilities for parsing and lexing TT and TTImp (and other things)
* ``Utils/`` -- some generally useful utilities
* ``Idris/`` -- anything relating to the high level language, translating to TTImp

  + ``Idris/Elab/`` -- High level construct elaboration machinery (e.g. interfaces)

* ``Compiler/`` -- back ends

The Core Type, and Ref
----------------------
Core is a "monad" (not really, for efficiency reasons, at the moment...)
supporting Errors and IO (I did originally plan to allow restricting this to
some specific IO operations, but haven't yet).  The raw syntax is defined by a
type ``RawImp`` which has a source location at each node, and any errors in
elaboration note the location at the point where the error occurred, as
a file context ``FC``.

``Ref`` is essentially an ``IORef``. Typically we pass them implicitly and use
labels to disambiguate which one we mean. See Core.Core for their
definition. Again, ``IORef`` is for efficiency - even if it would be neater to
use a state monad this turned out to be about 2-3 times faster, so I'm
going with the "ugly" choice...

Term representation
-------------------

Terms in the core language are indexed by a list of the names in scope,
most recently defined first:

::

    data Term : List Name -> Type

This means that terms are always well scoped, and we can use the type system
to keep us right when manipulating names. For example, we have:

::

    Local : FC -> (isLet : Maybe Bool) ->
            (idx : Nat) -> (0 p : IsVar name idx vars) -> Term vars

So local variables are represented by an index into the local context (a de
Bruijn index, ``idx``), and a proof, erased at run time, that the index 
is valid. So everything is de Bruijn indexed, but the type checker still
keeps track of the indices so that we don't have to think too hard!

``Core.TT`` contains various handy tools for manipulating terms with their
indices, such as:

::

    weaken : Term vars -> Term (n :: vars) -- actually in an interface, Weaken
    embed : Term vars -> Term (ns ++ vars) 
    refToLocal : (x : Name) -> -- explicit name of a reference
                 (new : Name) -> -- name to bind as
                 Term vars -> Term (new :: vars)

Note that the types are explicit about when the ``vars`` needs to be passed at
run time, and when it isn't. Mostly where it's needed it's to help with
displaying names, or name generation, rather than any fundamental reason in
the core. In general, this isn't expensive at run time.

Environments, defined in ``Core.Env``, map local variables to binders:

::

    data Env : (tm : List Name -> Type) -> List Name -> Type

A binders is typically a lambda, a pi, or a let (with a value), but can
also be a pattern variable. See the definition of ``TT`` for more details.
Where we have a term, we usually also need an ``Env``.

We also have values, which are in head normal form, and defined in
``Core.Value``:

::

    data NF : List Name -> Type

We can convert a term to a value by normalising...

::

    nf : {vars : _} ->
         Defs -> Env Term vars -> Term vars -> Core (NF vars)

...and back again, by quoting:

::

    quote : {vars : _} ->
            Defs -> Env Term vars -> tm vars -> Core (Term vars)

Both ``nf`` and ``quote`` are defined in ``Core.Normalise``. We don't
always know whether we'll need to work with ``NF`` or ``Term``, so
we also have a "glued" representation, ``Glued vars``, again defined in
``Core.Normalise``, which lazily computes either a ``NF`` or ``Term`` as
required. Elaborating a term returns the type as a ``Glued vars``.

``Term`` separates ``Ref`` (global user defined names) from ``Meta``, which
are globally defined metavariables. For efficiency, metavariables are only
substituted into terms if they have non-0 multiplicity, to preserve sharing as
much as possible.

Unification
-----------
Unification is probably the most important part of the elaboration process,
and infers values for implicit arguments. That is, it finds values for the
things which are referred to by ``Meta`` in ``Term``. It is defined in
``Core.Unify``, as the top level unification function has the following
type:

::

    unify : Unify tm =>
            {vars : _} ->
            {auto c : Ref Ctxt Defs} ->
            {auto u : Ref UST UState} ->
            UnifyInfo ->
            FC -> Env Term vars ->
            tm vars -> tm vars ->
            Core UnifyResult

The ``Unify`` interface is there because it is convenient to be able to
define unification on ``Term`` and ``NF``, as well as ``Closure`` (which
is part of ``NF`` to represent unevaluated arguments to constructors).

This is one place where indexing over ``vars`` is extremely valuable: we
have to keep the environment consistent, so unification won't accidentally
introduce any scoping bugs!

Idris 2 implements pattern unification - see Adam Gundry's thesis for an
accessible introduction.

Context
-------
``Core.Context`` defines all the things needed for TT. Most importantly: Def 
gives definitions of names (case trees, builtins, constructors and
holes, mostly); ``GlobalDef`` is a definition with all the other information
about it (type, visibility, totality, etc); ``Context`` is a context mapping names
to ``GlobalDef``, and ``Defs`` is the core data structure with everything needed to
typecheck more definitions.
{'fraction_non_alphanumeric': 0.09795262946607788, 'fraction_numerical': 0.001070520540612873, 'mean_word_length': 3.514346118997282, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 65, 'https://': 2, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '1199567', 'n_tokens_mistral': 4053, 'n_tokens_neox': 3854, 'n_words': 2184}