From bb8f766778192902cc0d36c1f4e339ece8cbbac5 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 4 Mar 2016 09:29:46 +0100
Subject: [PATCH] some more comments
---
heap_lang/lang.v | 15 +++++++++++++++
1 file changed, 15 insertions(+)
diff --git a/heap_lang/lang.v b/heap_lang/lang.v
index ecc53ff13..1b934de7b 100644
--- a/heap_lang/lang.v
+++ b/heap_lang/lang.v
@@ -32,8 +32,16 @@ Proof.
destruct mx; rewrite /= ?elem_of_cons; naive_solver.
Qed.
+(** A typeclass for whether a variable is bound in a given
+ context. Making this a typeclass means we can use tpeclass search
+ to program solving these constraints, so this becomes extensible.
+ Also, since typeclass search runs *after* unification, Coq has already
+ inferred the X for us; if we were to go for embedded proof terms ot
+ tactics, Coq would do things in the wrong order. *)
Class VarBound (x : string) (X : list string) :=
var_bound : bool_decide (x ∈ X).
+(* FIXME shouldn't this have this Hint to only perfom search of x and X
+ are not evars? *)
Hint Extern 0 (VarBound _ _) => vm_compute; exact I : typeclass_instances.
Instance var_bound_proof_irrel x X : ProofIrrel (VarBound x X).
@@ -46,6 +54,13 @@ Qed.
Inductive expr (X : list string) :=
(* Base lambda calculus *)
+ (* Var is the only place where the terms contain a proof. The fact that they
+ contain a proof at all is suboptimal, since this means two seeminlgy
+ convertible terms could differ in their proofs. However, this also has
+ some advantages:
+ * We can make the [X] an index, so we can do non-dependent match.
+ * In expr_weaken, we can push the proof all the way into Var, making
+ sure that proofs never block computation. *)
| Var (x : string) `{VarBound x X}
| Rec (f x : binder) (e : expr (f :b: x :b: X))
| App (e1 e2 : expr X)
--
GitLab