diff options
Diffstat (limited to 'src/README.md')
| -rw-r--r-- | src/README.md | 197 |
1 files changed, 0 insertions, 197 deletions
diff --git a/src/README.md b/src/README.md deleted file mode 100644 index 400a2e005..000000000 --- a/src/README.md +++ /dev/null @@ -1,197 +0,0 @@ -The ordering of files (eliding `*Proofs.v` files) is: - -``` - Language.v ←──────────────────────────────────────────────────┬───────────────────────────────┐ - ↗ ↖ │ │ - ↗ ↖ │ │ - UnderLets.v GENERATEDIdentifiersWithoutTypes.v MiscCompilerPasses.v PushButtonSynthesis/ReificationCache.v - ↑ ↖ ↗ ↑ ↑ -AbstractInterpretation.v Rewriter.v │ │ - ↑ ↑ ┌────────────────────────────────────────────────────┘ │ -CStringification.v │ │ Arithmetic.v │ - ↑ ┌───────────────────┴─┘ ↑ │ -BoundsPipeline.v COperationSpecifications.v │ - ↑ ↑ │ - │ ┌────────────────────────────────────────┴────────────────────────────────────────────────────────────────┘ -PushButtonSynthesis.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: - + SubstVarFstSndPairOppCast - -- 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 - -- BoundsPipeline.v: Assemble the various compiler passes together into - a composed pipeline. It is the final interface for the compiler. - Also contains some tactics for applying the BoundsPipeline - correctness lemma. - -- COperationSpecifications.v: The specifications for the various - operations to be synthesized. - -- PushButtonSynthesis/ReificationCache.v: Defines the cache that holds - reified versions of operations, as well as the tactics that reify - and apply things from the cache. - -- PushButtonSynthesis.v: Reifies the various operations from - Arithmetic.v, definies the compositions of the BoundsPipeline with - these operations, proves that their interpretations satisfies the - specs from COperationSpecifications.v, assembles the reified - post-bounds operations into synthesis targets. 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 - - -Proofs files: -For Language.v, there is a semi-arbitrary split between two files -`LanguageInversion` and `LanguageWf`. -- LanguageInversion.v: - + classifies equality of type codes and exprs - + type codes have decidable equality - + correctness of the various type-transport definitions - + correctness lemmas for the various `expr.invert_*` definitions - + correctness lemmas for the various `reify_*` definitions in Language.v - + inversion_type, which inverts equality of type codes - + type_beq_to_eq, which converts boolean equality of types to - Leibniz equality - + rewrite_type_transport_correct, which rewrites with the - correctness lemmas of the various type-transport definitions - + `type.invert_one e` which does case analysis on any inductive type - indexed over type codes, in a way that preserves information - about the type of `e`, and generally works even when the goal is - dependently typed over `e` and/or its type - + ident.invert, which does case-anaylsis on idents whose type has - structure (i.e., is not a var) - + ident.invert_match, which does case-analysis on idents appearing as - the discriminee of a `match` in the goal or in any hypothesis - + expr.invert, which does case-anaylsis on exprs whose type has - structure (i.e., is not a var) - + expr.invert_match, which does case-analysis on exprs appearing as - the discriminee of a `match` in the goal or in any hypothesis - + expr.invert_subst, which does case-analysis on exprs which show up - in hypotheses of the form `expr.invert_* _ = Some _` - + expr.inversion_expr, which inverts equalities of exprs - -- LanguageWf.v: Depends on LanguageInversion.v - Defines: - + expr.wf, expr.Wf, expr.wf3, expr.Wf3 - + GeneralizeVar.Flat.wf - + expr.inversion_wf (and variants), which invert `wf` hypotheses - + expr.wf_t (and variants wf_unsafe_t and wf_safe_t) which make - progress on `wf` goals; `wf_safe_t` should never turn a provable - goal into an unprovable one, while `wf_unsafe_t` might. - + expr.interp_t (and variants), which should make progress on - equivalence-of-interp hypotheses and goals, but is not used much - (mainly because I forgot I had defined it) - + prove_Wf, which proves wf goals on concrete syntax trees in a more - optimized way than `repeat constructor` - Proves: - + funext → (type.eqv ↔ Logic.eq) (`eqv_iff_eq_of_funext`) - + type.related and type.eqv are PERs - + Proper instances for type.app_curried, type.and_for_each_lhs_of_arrow - + type.is_not_higher_order → Reflexive (type.and_for_each_lhs_of_arrow type.eqv) - + iff between type.related{,_hetero} and related of type.app_curried - + various properties of type.and{,b_bool}for_each_lhs_of_arrow - + various properties of type.eqv and ident.{gen_,}interp - + various properties of ident.cast - + various properties of expr.wf (particularly of things defined in Language.v) - + interp and wf proofs for the passes to/from Flat - -- UnderLetsProofs.v: wf and interp lemmas for the various passes defined in UnderLets.v -- MiscCompilerPassesProofs.v: wf and interp lemmas for the various passes defined in MiscCompilerPasses.v -- GENERATEDIdentifiersWithoutTypesProofs.v: various lemmas about the definitions in GENERATEDIdentifiersWithoutTypes.v -- AbstractInterpretationZRangeProofs.v: Proves correctness lemmas of the per-operation zrange-bounds-analysis functions -- AbstractInterpretationWf.v: wf lemmas for the AbstractInterpretation pass -- AbstractInterpretationProofs.v: interp lemmas for the - AbstractInterpretation pass, and also correctness lemmas that - combine Wf and interp -- RewriterWf1.v: a semi-arbitrary collection of proofs and definitions - that are mostly shared between the wf proofs and the interp proofs. - Importantly, this file defines everything needed to state and prove - that specific rewrite rules are correct. -- RewriterRulesGood.v: Proves that all specific rewriter rules are - good enough for wf proofs (as specified in RewriterWf1.v) -- RewriterRulesInterpGood.v: Proves that all specific rewriter rules - are good enough for interp proofs (as specified in RewriterWf1.v) -- RewriterWf2.v: Proves wf of the generic rewriter pass, taking in - specific-rewriter-rule-correctness as a hypothesis -- RewriterInterpProofs1.v: Proves interp-correctness of the generic - rewriter pass, taking in specific-rewriter-rule-correctness as a - hypothesis -- RewriterProofs.v: assembles the proofs from RewriterRulesGood.v, - RewriterRulesInterpGood.v, RewriterWf2.v, and - RewriterInterpProofs1.v into correctness lemmas for the overall - rewriter pass, specialized and pre-evaluated for specific rewrite - rules |