diff options
| -rw-r--r-- | src/Reflection/Application.v | 15 | ||||
| -rw-r--r-- | src/Specific/GF25519Reflective/Common.v | 12 |
2 files changed, 14 insertions, 13 deletions
diff --git a/src/Reflection/Application.v b/src/Reflection/Application.v index 31f84e0fa..4274b3b3f 100644 --- a/src/Reflection/Application.v +++ b/src/Reflection/Application.v @@ -56,7 +56,7 @@ Section language. end%ctype (all_binders_for B) end. - Definition interp_all_binders_for var T + Definition interp_all_binders_for T var := match T return Type with | Tflat _ => unit | Arrow A B => interp_flat_type var (all_binders_for (Arrow A B)) @@ -68,9 +68,9 @@ Section language. | Arrow _ _ => fun x => fst x end args. Definition snd_binder {A B var} (args : interp_flat_type var (all_binders_for (Arrow A B))) - : interp_all_binders_for var B + : interp_all_binders_for B var := match B return interp_flat_type var (all_binders_for (Arrow A B)) - -> interp_all_binders_for var B + -> interp_all_binders_for B var with | Tflat _ => fun _ => tt | Arrow _ _ => fun x => snd x @@ -94,10 +94,10 @@ Section language. end. Fixpoint ApplyAll {var t} (x : @expr base_type interp_base_type op var t) - : forall (args : interp_all_binders_for var t), + : forall (args : interp_all_binders_for t var), @exprf base_type interp_base_type op var (remove_all_binders t) := match x in @expr _ _ _ _ t - return (forall (args : interp_all_binders_for var t), + return (forall (args : interp_all_binders_for t var), @exprf base_type interp_base_type op var (remove_all_binders t)) with | Return _ x => fun _ => x @@ -126,10 +126,10 @@ Section language. Fixpoint ApplyInterpedAll {t} : forall (x : interp_type interp_base_type t) - (args : interp_all_binders_for interp_base_type t), + (args : interp_all_binders_for t interp_base_type), interp_flat_type interp_base_type (remove_all_binders t) := match t return (forall (x : interp_type _ t) - (args : interp_all_binders_for _ t), + (args : interp_all_binders_for t _), interp_flat_type _ (remove_all_binders t)) with | Tflat _ => fun x _ => x @@ -138,6 +138,7 @@ Section language. End language. Arguments all_binders_for {_} !_ / . +Arguments interp_all_binders_for {_} !_ _ / . Arguments count_binders {_} !_ / . Arguments binders_for {_} !_ !_ _ / . Arguments remove_binders {_} !_ !_ / . diff --git a/src/Specific/GF25519Reflective/Common.v b/src/Specific/GF25519Reflective/Common.v index f554d6708..d42388b75 100644 --- a/src/Specific/GF25519Reflective/Common.v +++ b/src/Specific/GF25519Reflective/Common.v @@ -53,15 +53,15 @@ Local Ltac make_bounds ls := let v := (eval compute in v) in exact v. -Definition ExprBinOp_bounds : all_binders_for ExprBinOpT ZBounds.interp_base_type. +Definition ExprBinOp_bounds : interp_all_binders_for ExprBinOpT ZBounds.interp_base_type. Proof. make_bounds (Tuple.to_list _ bounds ++ Tuple.to_list _ bounds)%list. Defined. -Definition ExprUnOp_bounds : all_binders_for ExprUnOpT ZBounds.interp_base_type. +Definition ExprUnOp_bounds : interp_all_binders_for ExprUnOpT ZBounds.interp_base_type. Proof. make_bounds (Tuple.to_list _ bounds). Defined. -Definition ExprUnOpFEToZ_bounds : all_binders_for ExprUnOpFEToZT ZBounds.interp_base_type. +Definition ExprUnOpFEToZ_bounds : interp_all_binders_for ExprUnOpFEToZT ZBounds.interp_base_type. Proof. make_bounds (Tuple.to_list _ bounds). Defined. -Definition ExprUnOpFEToWire_bounds : all_binders_for ExprUnOpFEToWireT ZBounds.interp_base_type. +Definition ExprUnOpFEToWire_bounds : interp_all_binders_for ExprUnOpFEToWireT ZBounds.interp_base_type. Proof. make_bounds (Tuple.to_list _ bounds). Defined. -Definition ExprUnOpWireToFE_bounds : all_binders_for ExprUnOpWireToFET ZBounds.interp_base_type. +Definition ExprUnOpWireToFE_bounds : interp_all_binders_for ExprUnOpWireToFET ZBounds.interp_base_type. Proof. make_bounds (Tuple.to_list _ wire_digit_bounds). Defined. Definition interp_bexpr : ExprBinOp -> Specific.GF25519BoundedCommon.fe25519W -> Specific.GF25519BoundedCommon.fe25519W -> Specific.GF25519BoundedCommon.fe25519W @@ -138,7 +138,7 @@ Ltac rexpr_correct := Notation rword_of_Z rexprZ_sig := (MapInterp Word64.of_Z (proj1_sig rexprZ_sig)) (only parsing). Notation compute_bounds opW bounds - := (ApplyInterped (Interp (@ZBounds.interp_op) (MapInterp (@ZBounds.of_word64) opW)) bounds) + := (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp (@ZBounds.of_word64) opW)) bounds) (only parsing). |