aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Jason Gross <jgross@mit.edu>2019-03-31 09:35:54 -0400
committerGravatar Jason Gross <jasongross9@gmail.com>2019-03-31 09:36:16 -0400
commit25761f294d165487bec8832272c58dae82038b95 (patch)
tree8d7003035213995ce958079b79af95858cdc0804
parent8a0fc29222cd90a2c33014d4bed754241e8fdd59 (diff)
Add some comments based on CR requests
-rw-r--r--src/Rewriter.v10
-rw-r--r--src/RewriterWf1.v3
2 files changed, 13 insertions, 0 deletions
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.