-
Notifications
You must be signed in to change notification settings - Fork 0
/
SqirExtraction.v
35 lines (29 loc) · 1016 Bytes
/
SqirExtraction.v
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
Require Coq.extraction.Extraction.
Require Import SQIR.SQIR.
Require Import Reals.
Require Coq.extraction.ExtrOcamlNatInt.
Require Coq.extraction.ExtrOcamlZInt.
(* From Leo's ExtractReal *)
Extract Constant R => "float".
Extract Constant R0 => "0.0".
Extract Constant R1 => "1.0".
Extract Constant Rinv => "(fun r -> 1.0 /. r)".
Extract Constant Ropp => "(fun r -> 0.0 -. r)".
Extract Constant Rmult => "(fun r1 r2 -> r1 *. r2)".
Extract Constant Rplus => "(+.)".
Extract Constant PI => "Float.pi".
Extraction Implicit H [dim].
Extraction Implicit X [dim].
Extraction Implicit Y [dim].
Extraction Implicit SQIR.Z [dim].
Extraction Implicit ID [dim].
Extraction Implicit SKIP [dim].
Extraction Implicit Rz [dim].
Extraction Implicit T [dim].
Extraction Implicit TDAG [dim].
Extraction Implicit P [dim].
Extraction Implicit PDAG [dim].
Extraction Implicit CNOT [dim].
Extraction Implicit CZ [dim].
Extraction Implicit SWAP [dim].
Extraction "SqirGates.ml" com H X Y SQIR.Z ID SKIP Rz T TDAG P PDAG CNOT CZ SWAP.