Add invert_Var

1 files changed, 10 insertions, 0 deletions

diff --git a/src/Reflection/Syntax.v b/src/Reflection/Syntax.v
index 80c487687..e693bb061 100644
--- a/src/Reflection/Syntax.v
+++ b/src/Reflection/Syntax.v
@@ -378,6 +378,15 @@ Section language.
     Section misc.
       Definition invert_Const {var t} (e : @exprf var t) : option (interp_type t)
         := match e with Const _ v => Some v | _ => None end.
+      Definition invert_Var {var t} (e : @exprf var (Tbase t)) : option (var t)
+        := match e in @exprf _ t' return option (var match t' with
+                                                     | Tbase t' => t'
+                                                     | _ => t
+                                                     end)
+           with
+           | Var _ v => Some v
+           | _ => None
+           end.
       Definition invert_Op {var t} (e : @exprf var t) : option { t1 : flat_type & op t1 t * exprf t1 }%type
         := match e with Op _ _ opc args => Some (existT _ _ (opc, args)) | _ => None end.
       Definition invert_LetIn {var A} (e : @exprf var A) : option { B : _ & exprf B * (interp_flat_type_gen var B -> exprf A) }%type
@@ -500,6 +509,7 @@ Global Arguments Interp {_ _ _} interp_op {t} _.
 Global Arguments interp {_ _ _} interp_op {t} _.
 Global Arguments interpf {_ _ _} interp_op {t} _.
 Global Arguments invert_Const {_ _ _ _ _} _.
+Global Arguments invert_Var {_ _ _ _ _} _.
 Global Arguments invert_Op {_ _ _ _ _} _.
 Global Arguments invert_LetIn {_ _ _ _ _} _.
 Global Arguments invert_Pair {_ _ _ _ _ _} _.