diff options
author | Jason Gross <jgross@mit.edu> | 2017-04-02 02:04:38 -0400 |
---|---|---|
committer | Jason Gross <jasongross9@gmail.com> | 2017-04-02 10:27:49 -0400 |
commit | 39423861f916252b9d42eb40c3198a65d31ee410 (patch) | |
tree | d4267cef765b735e0d68648aaba2b83a854feb18 | |
parent | 83d035c40eb8f4f66097c003f90fab0a58fa25d8 (diff) |
More extensive comment in NewBaseSystem
As per Andres' request on #138.
-rw-r--r-- | src/NewBaseSystem.v | 20 |
1 files changed, 19 insertions, 1 deletions
diff --git a/src/NewBaseSystem.v b/src/NewBaseSystem.v index 9f7a327bc..3afc1d8b8 100644 --- a/src/NewBaseSystem.v +++ b/src/NewBaseSystem.v @@ -907,7 +907,25 @@ Positional.to_associational_cps Positional.to_associational Positional.eval Posi (https://coq.inria.fr/bugs/show_bug.cgi?id=5434), that [vm_compute] breaks an invariant in pretyping/constr_matching.ml. So we refresh all of the names in match statements in the goal by - crawling it. *) + crawling it. + + In particular, [replace_with_vm_compute] creates a [vm_compute]d + term which has anonymous binders where pretyping expects there to + be named binders. This shows up when you try to match on the + function (the branch statement of the match) with an Ltac pattern + like [(fun x : ?T => ?C)] rather than [(fun x : ?T => @?C x)]; we + use the former in reification to save the cost of many extra + invocations of [cbv beta]. Luckily, patterns like [(fun x : ?T => + @?C x)] don't trigger this anomaly, so we can walk the term, + fixing all match statements whose branches are functions whose + binder names were eaten by [vm_compute] (note that in a match, + every branch where the corresponding constructor takes arguments + is represented internally as a function (lambda term)). We fix + the match statements by pulling out the branch with the [@?] + pattern that doesn't trigger the anomaly, and then recreating the + match with a destructuring [let] that hasn't been through + [vm_compute], and therefore has name information that + constr_matching is happy with. *) Ltac replace_match_with_destructuring_match T := match T with | ?F ?X |