From 25761f294d165487bec8832272c58dae82038b95 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Sun, 31 Mar 2019 09:35:54 -0400 Subject: Add some comments based on CR requests --- src/Rewriter.v | 10 ++++++++++ src/RewriterWf1.v | 3 +++ 2 files changed, 13 insertions(+) diff --git a/src/Rewriter.v b/src/Rewriter.v index f03cf69d2..99201e27d 100644 --- a/src/Rewriter.v +++ b/src/Rewriter.v @@ -1288,6 +1288,16 @@ Module Compilers. Let type_base := @type.base base.type. Local Coercion type_base : base.type >-> type.type. + (** This definition takes in an identifier. If the identifier + is not meant to be evaluated eagerly, [None] is + returned. Otherwise, a value-thunk is returned. This + value-thunk takes in all of the arguments to which the + identifer will eventually be applied. If there is enough + structure for eager evaluation, then the identifier is + "evaluated" in Gallina (e.g., [eager_list_rect] turns into + [list_rect] over a concrete list of cons cells holding + PHOAS expressions), and the result of this evaluation is + returned." *) (* N.B. the [with_lets] argument to [reflect] doesn't matter here because [value' true (_ → _) ≡ value' false (_ → _)] *) Definition reflect_ident_iota {t} (idc : ident t) : option (value t) diff --git a/src/RewriterWf1.v b/src/RewriterWf1.v index e22c8155b..420b5dc90 100644 --- a/src/RewriterWf1.v +++ b/src/RewriterWf1.v @@ -2571,6 +2571,9 @@ Module Compilers. End with_var. End Compile. + (** Now we prove the [wf] properties about definitions used only + in reification of rewrite rules, which are used to make proving + [wf] of concrete rewrite rules easier. *) Module Reify. Import Compile. Import Rewriter.Compilers.RewriteRules.Compile. -- cgit v1.2.3