From 037df57566b1108af0d13cfcafe9b0f8fdd5937b Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Sun, 6 May 2018 22:17:10 -0400
Subject: New pipeline, split among files

---
 src/Experiments/NewPipeline/README.md | 100 ++++++++++++++++++++++++++++++++++
 1 file changed, 100 insertions(+)
 create mode 100644 src/Experiments/NewPipeline/README.md

(limited to 'src/Experiments/NewPipeline/README.md')

diff --git a/src/Experiments/NewPipeline/README.md b/src/Experiments/NewPipeline/README.md
new file mode 100644
index 000000000..27c350ec8
--- /dev/null
+++ b/src/Experiments/NewPipeline/README.md
@@ -0,0 +1,100 @@
+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)
+  + ReassociateSmallConstants.Reassociate:
+     * (turn expressions of the form ((x * y) * ##v) into (x * (y * ##v)) for
+       small values of v)
+
+- 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
-- 
cgit v1.2.3