From 9480dccb77f9e9312c9159a4c7fca8814bc73433 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 15 May 2017 22:37:02 -0400 Subject: Add Named.ExprInversion --- src/Compilers/Named/ExprInversion.v | 21 +++++++++++++++++++++ 1 file changed, 21 insertions(+) create mode 100644 src/Compilers/Named/ExprInversion.v (limited to 'src/Compilers') diff --git a/src/Compilers/Named/ExprInversion.v b/src/Compilers/Named/ExprInversion.v new file mode 100644 index 000000000..783341f26 --- /dev/null +++ b/src/Compilers/Named/ExprInversion.v @@ -0,0 +1,21 @@ +Require Import Crypto.Compilers.TypeInversion. +Require Import Crypto.Compilers.Syntax. +Require Import Crypto.Compilers.Named.Syntax. + +Module Export Named. + Ltac invert_one_expr e := + preinvert_one_type e; + intros ? e; + destruct e; + try exact I. + + Ltac invert_expr_step := + match goal with + | [ e : Named.exprf _ _ _ (Tbase _) |- _ ] => invert_one_expr e + | [ e : Named.exprf _ _ _ (Prod _ _) |- _ ] => invert_one_expr e + | [ e : Named.exprf _ _ _ Unit |- _ ] => invert_one_expr e + | [ e : Named.expr _ _ _ (Arrow _ _) |- _ ] => invert_one_expr e + end. + + Ltac invert_expr := repeat invert_expr_step. +End Named. -- cgit v1.2.3