blob: e2bc9e6e08371dc19ba634e612451aeaa97cf4c8 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
|
Require Import Coq.ZArith.ZArith Coq.ZArith.BinIntDef.
Require Import Crypto.Arithmetic.Core. Import B.
Require Import Crypto.Util.ZUtil.ModInv.
Require Import Crypto.Util.Tactics.CacheTerm.
Require Crypto.Util.Tuple.
Local Notation tuple := Tuple.tuple.
Local Open Scope list_scope.
Local Open Scope Z_scope.
Ltac if_cond_else cond tac default id :=
lazymatch (eval compute in cond) with
| true => tac id
| false => default
end.
Ltac if_cond cond tac id := if_cond_else cond tac (0%Z) id.
Ltac pose_modinv modinv_fuel a modulus modinv :=
let v := constr:(Option.invert_Some (Z.modinv_fueled modinv_fuel a modulus)) in
let v := (eval vm_compute in v) in
let v := (eval vm_compute in (v : Z)) in
cache_term v modinv.
Ltac pose_correct_if_Z v mkeqn id :=
let T := type of v in
let eqn :=
lazymatch (eval vm_compute in T) with
| Z => mkeqn ()
| ?T
=> let v := (eval vm_compute in v) in
lazymatch T with
| option _
=> lazymatch v with
| None => constr:(v = v)
end
| unit
=> lazymatch v with
| tt => constr:(tt = tt)
end
end
end in
cache_proof_with_type_by
eqn
ltac:(vm_compute; reflexivity)
id.
Ltac pose_proof_tuple ls :=
lazymatch ls with
| pair ?x ?y => pose_proof_tuple x; pose_proof_tuple y
| ?ls => pose proof ls
end.
Ltac make_chained_carries_cps' sz wt s c a carry_chains :=
lazymatch carry_chains with
| ?carry_chain :: nil
=> constr:(Positional.chained_carries_cps (n:=sz) (div:=div) (modulo:=modulo) wt a carry_chain id)
| ?carry_chain :: ?carry_chains
=> let r := fresh "r" in
let r' := fresh r in
constr:(Positional.chained_carries_cps (n:=sz) (div:=div) (modulo:=modulo) wt a carry_chain
(fun r => Positional.carry_reduce_cps (n:=sz) (div:=div) (modulo:=modulo) wt s c r
(fun r' => ltac:(let v := make_chained_carries_cps' sz wt s c r' carry_chains in exact v))))
end.
Ltac make_chained_carries_cps sz wt s c a carry_chains :=
let carry_chains := (eval cbv delta [carry_chains] in carry_chains) in
make_chained_carries_cps' sz wt s c a carry_chains.
|
