diff options
| -rw-r--r-- | _CoqProject | 1 | ||||
| -rw-r--r-- | src/Compilers/StripExpr.v | 35 |
2 files changed, 36 insertions, 0 deletions
diff --git a/_CoqProject b/_CoqProject index 20e7f7ba2..53fe6dff8 100644 --- a/_CoqProject +++ b/_CoqProject @@ -87,6 +87,7 @@ src/Compilers/Rewriter.v src/Compilers/RewriterInterp.v src/Compilers/RewriterWf.v src/Compilers/SmartMap.v +src/Compilers/StripExpr.v src/Compilers/Syntax.v src/Compilers/TestCase.v src/Compilers/Tuple.v diff --git a/src/Compilers/StripExpr.v b/src/Compilers/StripExpr.v new file mode 100644 index 000000000..57b3e2365 --- /dev/null +++ b/src/Compilers/StripExpr.v @@ -0,0 +1,35 @@ +Require Import Crypto.Compilers.Syntax. +Require Import Crypto.Compilers.SmartMap. + +Section language. + Context {base_type_code : Type} + {op : flat_type base_type_code -> flat_type base_type_code -> Type}. + Local Notation Expr := (@Expr base_type_code op). + Local Notation expr := (@expr base_type_code op). + Local Notation exprf := (@exprf base_type_code op). + + Section with_var. + Context {var : base_type_code -> Type}. + + Fixpoint strip_exprf {T} (e : @exprf (fun t => @exprf var (Tbase t)) T) + : @exprf var T + := match e with + | TT => TT + | Var t v + => v + | Op src dst opv args + => Op opv (strip_exprf args) + | LetIn tx ex tC eC + => LetIn (strip_exprf ex) + (fun v => strip_exprf (eC (SmartVarVarf v))) + | Pair tx ex ty ey + => Pair (strip_exprf ex) (strip_exprf ey) + end. + + Definition strip_expr {T} (e : @expr (fun t => @exprf var (Tbase t)) T) + : @expr var T + := match e with + | Abs src dst f => Abs (fun x => strip_exprf (f (SmartVarVarf x))) + end. + End with_var. +End language. |