1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
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
|
