The ordering of files (eliding `*Proofs.v` files) is:

```
                    Arithmetic.v
                         ↑
                     Language.v ←──────────────────────────────────────────────────┐
                     ↗           ↖                                                 │
                  ↗                  ↖                                             │
                 UnderLets.v          GENERATEDIdentifiersWithoutTypes.v     MiscCompilerPasses.v
                    ↑       ↖        ↗                                             ↑
AbstractInterpretation.v    Rewriter.v                                             │
         ↑                  ↑ ┌────────────────────────────────────────────────────┘
CStringification.v          │ │
   ↑    ┌───────────────────┴─┘
Toplevel1.v ←── Toplevel2.v ←───────────┐
   ↑                                    │
CLI.v                         SlowPrimeSynthesisExamples.v
↑  ↑
│  └────────────────────────────┐
StandaloneHaskellMain.v   StandaloneOCamlMain.v
        ↑                           ↑
ExtractionHaskell.v          ExtractionOCaml.v
```

The files contain:

- Arithmetic.v: All of the high-level field arithmetic stuff

- Language.v:
  + PHOAS
  + reification
  + denotation/intepretation
  + utilities for inverting PHOAS exprs
  + default/dummy values of PHOAS exprs
  + default instantiation of generic PHOAS types
  + gallina reification of ground terms
  + Flat/indexed syntax trees, and conversions to and from PHOAS
  Defines the passes:
  + ToFlat
  + FromFlat
  + GeneralizeVar

- UnderLets.v: the UnderLets monad, a pass that does substitution of var-like
  things, a pass that inserts let-binders in the next-to-last line of code,
  substituting away var-like things (this is used to ensure that when we output
  C code, aliasing the input and the output arrays doesn't cause issues).
  Defines the passes:
  + SubstVarFstSndPairOpp

- AbstractInterpretation.v: type-code-based ZRange definitions, abstract
  interpretation of identifiers (which does let-lifting, for historical reasons,
  and the dependency on UnderLets should probably be removed), defines the
  passes:
  + PartialEvaluateWithBounds
  + PartialEvaluateWithListInfoFromBounds
  + CheckPartialEvaluateWithBounds

- GENERATEDIdentifiersWithoutTypes.v: generated by a python script which is
  included in a comment in the file, this is an untyped version of identifiers
  for the rewriter

- Rewriter.v: rewrite rules, rewriting.  Defines the passes:
  + Rewrite
  + RewriteToFancy
  + PartialEvaluate (which is just a synonym for Rewrite)

- MiscCompilerPasses.v: Defines the passes:
  + EliminateDead (dead code elimination)
  + Subst01 (substitute let-binders used 0 or 1 times)

- CStringification.v: conversion to C code as strings.  (Depends on
  AbstractInterpretation.v for ZRange utilities.)  Defines the passes:
  + ToString.ToFunctionLines
  + ToString.ToFunctionString
  + ToString.LinesToString

- CompilersTestCases.v: Various test cases to ensure everything is working

- Toplevel1.v: Ring Goal (which SHOULD NOT depend on compilers) + pipeline + a couple of examples
  pipeline + most of the stuff that uses compilers + arithmetic.  This is the file that CLI.v depends on.

- Toplevel2.v: Some not-quite-finished-but-kind-of-slow pipeline stuff
  + all the stuff that uses compilers + arithmetic, together with more
  examples.  Also has semi-broken fancy-machine stuff.  This should
  probably be merged into Toplevel1.v when working on the pipeline.

- SlowPrimeSynthesisExamples.v: Additional uses of the pipeline for
  primes that are kind-of slow, which I don't want extraction blocking
  on.

- CLI.v: Setting up all of the language-independent parts of extraction; relies
  on having a list of strings-or-error-messages for each pipeline, and on the
  arguments to that pipeline, and builds a parser for command line arguments for
  that.

- StandaloneHaskellMain.v, StandaloneOCamlMain.v, ExtractionHaskell.v,
  ExtractionOCaml.v: Extraction of pipeline to various languages