From 9623c283c29bb3f36b18bf47cdea3dc2cec2ddb0 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 19 May 2017 16:24:13 -0400 Subject: Also reify Z.sub_with_get_borrow After | File Name | Before || Change -------------------------------------------------------------------------------- 4m01.69s | Total | 4m00.89s || +0m00.80s -------------------------------------------------------------------------------- 2m18.60s | Specific/IntegrationTestLadderstep | 2m18.52s || +0m00.07s 0m54.16s | Specific/IntegrationTestLadderstep130 | 0m53.85s || +0m00.30s 0m15.24s | Specific/IntegrationTestFreeze | 0m15.10s || +0m00.14s 0m11.70s | Specific/IntegrationTestMul | 0m11.76s || -0m00.06s 0m10.55s | Specific/IntegrationTestSub | 0m10.40s || +0m00.15s 0m09.10s | Specific/IntegrationTestSquare | 0m09.02s || +0m00.08s 0m00.79s | Compilers/Z/Bounds/Pipeline/ReflectiveTactics | 0m00.68s || +0m00.10s 0m00.54s | Compilers/Z/Bounds/Pipeline | 0m00.58s || -0m00.03s 0m00.52s | Compilers/Z/Reify | 0m00.54s || -0m00.02s 0m00.50s | Compilers/Z/Bounds/Pipeline/Glue | 0m00.44s || +0m00.06s --- src/Compilers/Z/Reify.v | 11 +++++++++-- 1 file changed, 9 insertions(+), 2 deletions(-) (limited to 'src') diff --git a/src/Compilers/Z/Reify.v b/src/Compilers/Z/Reify.v index 6d41df19e..d3a86dde1 100644 --- a/src/Compilers/Z/Reify.v +++ b/src/Compilers/Z/Reify.v @@ -22,22 +22,29 @@ Ltac base_reify_op op op_head extra ::= | @Z.opp => constr:(reify_op op op_head 1 (Opp TZ TZ)) | @Z.zselect => constr:(reify_op op op_head 3 (Zselect TZ TZ TZ TZ)) | @Z.add_with_carry => constr:(reify_op op op_head 3 (AddWithCarry TZ TZ TZ TZ)) + | @Z.sub_with_borrow => constr:(reify_op op op_head 3 (SubWithBorrow TZ TZ TZ TZ)) | @Z.add_with_get_carry => lazymatch extra with | @Z.add_with_get_carry ?bit_width _ _ _ => constr:(reify_op op op_head 3 (AddWithGetCarry bit_width TZ TZ TZ TZ TZ)) | _ => fail 100 "Anomaly: In Reflection.Z.base_reify_op: head is Z.add_with_get_carry but body is wrong:" extra end + | @Z.sub_with_get_borrow + => lazymatch extra with + | @Z.sub_with_get_borrow ?bit_width _ _ _ + => constr:(reify_op op op_head 3 (SubWithGetBorrow bit_width TZ TZ TZ TZ TZ)) + | _ => fail 100 "Anomaly: In Reflection.Z.base_reify_op: head is Z.sub_with_get_borrow but body is wrong:" extra + end end. Ltac base_reify_type T ::= lazymatch T with | Z => TZ end. Ltac Reify' e := - let e := (eval cbv beta delta [Z.add_get_carry] in e) in + let e := (eval cbv beta delta [Z.add_get_carry Z.sub_get_borrow] in e) in Compilers.Reify.Reify' base_type interp_base_type op e. Ltac Reify e := - let e := (eval cbv beta delta [Z.add_get_carry] in e) in + let e := (eval cbv beta delta [Z.add_get_carry Z.sub_get_borrow] in e) in let v := Compilers.Reify.Reify base_type interp_base_type op make_const e in constr:(ExprEta v). Ltac prove_ExprEta_Compile_correct := -- cgit v1.2.3