diff options
-rw-r--r-- | _CoqProject | 1 | ||||
-rw-r--r-- | src/Reflection/Application.v | 64 |
2 files changed, 65 insertions, 0 deletions
diff --git a/_CoqProject b/_CoqProject index 0489e1b0f..48d7d72b0 100644 --- a/_CoqProject +++ b/_CoqProject @@ -90,6 +90,7 @@ src/ModularArithmetic/BarrettReduction/ZHandbook.v src/ModularArithmetic/Montgomery/Z.v src/ModularArithmetic/Montgomery/ZBounded.v src/ModularArithmetic/Montgomery/ZProofs.v +src/Reflection/Application.v src/Reflection/CommonSubexpressionElimination.v src/Reflection/Conversion.v src/Reflection/CountLets.v diff --git a/src/Reflection/Application.v b/src/Reflection/Application.v new file mode 100644 index 000000000..21c0dea71 --- /dev/null +++ b/src/Reflection/Application.v @@ -0,0 +1,64 @@ +Require Import Crypto.Reflection.Syntax. + +Section language. + Context {base_type : Type} + {interp_base_type : base_type -> Type} + {op : flat_type base_type -> flat_type base_type -> Type}. + Fixpoint count_binders (t : type base_type) : nat + := match t with + | Arrow A B => S (count_binders B) + | Tflat _ => 0 + end. + + Fixpoint remove_binders' (n : nat) (t : type base_type) {struct t} : type base_type + := match t, n with + | Tflat _, _ => t + | Arrow _ B, 0 => B + | Arrow A B, S n' + => remove_binders' n' B + end. + + Definition remove_binders (n : nat) (t : type base_type) : type base_type + := match n with + | 0 => t + | S n' => remove_binders' n' t + end. + + Fixpoint binders_for' (n : nat) (t : type base_type) (var : base_type -> Type) {struct t} + := match n, t return Type with + | 0, Arrow A B => var A + | S n', Arrow A B => var A * binders_for' n' B var + | _, _ => unit + end%type. + Definition binders_for (n : nat) (t : type base_type) (var : base_type -> Type) + := match n return Type with + | 0 => unit + | S n' => binders_for' n' t var + end. + + Definition all_binders_for (t : type base_type) (var : base_type -> Type) + := binders_for (count_binders t) t var. + + Fixpoint Apply' n {var t} (x : @expr base_type interp_base_type op var t) + : forall (args : binders_for' n t var), + @expr base_type interp_base_type op var (remove_binders' n t) + := match x in (@expr _ _ _ _ t), n return (binders_for' n t var -> @expr _ _ _ _ (remove_binders' n t)) with + | Return _ _ as y, _ => fun _ => y + | Abs _ _ f, 0 => f + | Abs src dst f, S n' => fun args => @Apply' n' var dst (f (fst args)) (snd args) + end. + + Definition Apply n {var t} (x : @expr base_type interp_base_type op var t) + : forall (args : binders_for n t var), + @expr base_type interp_base_type op var (remove_binders n t) + := match n return binders_for n t var -> @expr _ _ _ _ (remove_binders n t) with + | 0 => fun _ => x + | S n' => @Apply' n' var t x + end. +End language. + +Arguments all_binders_for {_} !_ _ / . +Arguments count_binders {_} !_ / . +Arguments binders_for {_} !_ !_ _ / . +Arguments remove_binders {_} !_ !_ / . +Arguments Apply {_ _ _ !_ _ _} !_ !_ / , {_ _ _} !_ {_ _} !_ !_ / . |