blob: 7c3ed70e6a1824a88902e15e0b3a02d0d5eee56c (
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
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
|
Require Import Crypto.Compilers.SmartMap.
Require Import Crypto.Compilers.ExprInversion.
Require Import Crypto.Compilers.Syntax.
Require Import Crypto.Compilers.Z.Syntax.
Require Import Crypto.Compilers.ZExtended.Syntax.
Definition unextend_base_type (t : ZExtended.Syntax.base_type) : Z.Syntax.base_type
:= match t with
| TZ => Z.Syntax.TZ
| TBool => Z.Syntax.TZ
end.
Definition invert_Const s d (opc : op s d) : option (interp_flat_type interp_base_type d)
:= match opc with
| ConstZ v => Some v
| ConstBool v => Some v
| AddWithGetCarry
| SubWithGetBorrow
| MulSplitAtBitwidth
| AddWithGetCarryZ _
| SubWithGetBorrowZ _
| MulSplitAtBitwidthZ _
| IdWithAlt _
| Zselect
| Zmul
| Zadd
| Zsub
| Zopp
| Zshiftr
| Zshiftl
| Zland
| Zlor
| Zmodulo
| Zdiv
| Zlog2
| Zpow
| Zones
| Zeqb
| BoolCase _
=> None
end.
Definition unextend_op {s d} (opc : ZExtended.Syntax.op s d)
: option (Z.Syntax.op (lift_flat_type unextend_base_type s)
(lift_flat_type unextend_base_type d))
:= match opc in ZExtended.Syntax.op s d
return option (Z.Syntax.op (lift_flat_type unextend_base_type s)
(lift_flat_type unextend_base_type d))
with
| AddWithGetCarry => None
| AddWithGetCarryZ bitwidth
=> Some (Z.Syntax.AddWithGetCarry bitwidth _ _ _ _ _)
| SubWithGetBorrow => None
| SubWithGetBorrowZ bitwidth
=> Some (Z.Syntax.SubWithGetBorrow bitwidth _ _ _ _ _)
| MulSplitAtBitwidth => None
| MulSplitAtBitwidthZ bitwidth
=> Some (Z.Syntax.MulSplit bitwidth _ _ _ _)
| IdWithAlt (Tbase _)
=> Some (Z.Syntax.IdWithAlt _ _ _)
| IdWithAlt _
=> None
| Zselect => Some (Z.Syntax.Zselect _ _ _ _)
| Zmul => Some (Z.Syntax.Mul _ _ _)
| Zadd => Some (Z.Syntax.Add _ _ _)
| Zsub => Some (Z.Syntax.Sub _ _ _)
| Zopp => Some (Z.Syntax.Opp _ _)
| Zshiftr => Some (Z.Syntax.Shr _ _ _)
| Zshiftl => Some (Z.Syntax.Shl _ _ _)
| Zland => Some (Z.Syntax.Land _ _ _)
| Zlor => Some (Z.Syntax.Lor _ _ _)
| Zmodulo => None
| Zdiv => None
| Zlog2 => None
| Zpow => None
| Zones => None
| Zeqb => None
| ConstZ v => Some (OpConst v)
| ConstBool v => None
| BoolCase T => None
end.
|
