diff --git a/.gitmodules b/.gitmodules deleted file mode 100644 index 789d001f..00000000 --- a/.gitmodules +++ /dev/null @@ -1,3 +0,0 @@ -[submodule "examples/shor/externals/euler"] - path = examples/shor/externals/euler - url = git@github.com:taorunz/euler.git diff --git a/Makefile b/Makefile index 3a4c221a..f06939e2 100644 --- a/Makefile +++ b/Makefile @@ -1,8 +1,6 @@ .DEFAULT_GOAL := sqir all: - git submodule init; - git submodule update; @dune build sqir: FORCE @@ -12,12 +10,11 @@ voqc: FORCE @dune build VOQC examples: FORCE - @dune build examples + @dune build examples/examples + @dune build examples/ghz shor: - git submodule init; - git submodule update; - @dune build shor + @dune build examples/shor clean: @dune clean diff --git a/README.md b/README.md index bfc5e12c..eed50266 100644 --- a/README.md +++ b/README.md @@ -14,14 +14,13 @@ If you are interested in learning more about formal verification of quantum prog ## Table of Contents -- [SQIR & VOQC](#sqir--voqc) +- [SQIR \& VOQC](#sqir--voqc) - [Table of Contents](#table-of-contents) - [Setup](#setup) - [Compilation](#compilation) - - [Using With Other Projects]() + - [Using With Other Projects](#using-with-other-projects) - [Directory Contents](#directory-contents) - [SQIR](#sqir) - - [externals](#externals) - [VOQC](#voqc) - [examples](#examples) - [Acknowledgements](#acknowledgements) @@ -29,7 +28,7 @@ If you are interested in learning more about formal verification of quantum prog ## Setup -To compile SQIR and VOQC, you will need [Coq](https://coq.inria.fr/), [QuantumLib](https://github.com/inQWIRE/QuantumLib) (version 1.1.0), and the [Coq Interval package](http://coq-interval.gforge.inria.fr/). We strongly recommend using [opam](https://opam.ocaml.org/doc/Install.html) to install Coq and `opam switch` to manage Coq versions. We currently support Coq **versions 8.12-8.15**. If you run into errors when compiling our proofs, first check your version of Coq (`coqc -v`). +To compile SQIR and VOQC, you will need [Coq](https://coq.inria.fr/) and [QuantumLib](https://github.com/inQWIRE/QuantumLib) (version 1.1.0). In order to build the Shor proof, you will also need the [Coq Interval package](http://coq-interval.gforge.inria.fr/) and the [coq-euler](https://github.com/taorunz/euler) library. We strongly recommend using [opam](https://opam.ocaml.org/doc/Install.html) to install Coq and `opam switch` to manage Coq versions. We currently support Coq **versions 8.12-8.16**. If you run into errors when compiling our proofs, first check your version of Coq (`coqc -v`). Assuming you have opam installed (following the instructions in the link above), follow the steps below to set up your environment. ``` @@ -44,16 +43,14 @@ eval $(opam env) # install Coq -- this will take a while! opam install coq -# install dune -opam install dune - # install the QuantumLib library opam repo add coq-released https://coq.inria.fr/opam/released opam update opam install coq-quantumlib.1.1.0 -# install Interval package (optional, needed to compile proofs in examples/shor) +# Optional, if you want to compile the proofs in examples/shor opam install coq-interval +opam pin coq-euler https://github.com/taorunz/euler.git ``` *Notes*: @@ -93,10 +90,6 @@ Definition of the SQIR language. - UnitaryOps.v : Utilities for manipulating unitary SQIR programs. - UnitarySem.v : Semantics for unitary SQIR programs. -### externals - -External dependencies linked as git submodules. Currently, our proof of Shor's algorithm depends on the number theory in the [euler](https://github.com/taorunz/euler) development. - ### VOQC Verified transformations of SQIR programs. The optimizations and mapping routines extracted to our OCaml library ([inQWIRE/mlvoqc](https://github.com/inQWIRE/mlvoqc)) are all listed in **Main.v**. So this file is a good starting point for getting familiar with VOQC. @@ -128,6 +121,7 @@ The rest of the files in the VOQC directory can be split into the following cate - GreedyLayout.v : Generate a layout based on the input program and architecture. - Layouts.v : Utilities for describing a physical <-> logical qubit mapping (i.e., layout). - MappingConstraints.v : Utilities for describing a program that satisfies architecture constraints. + - MappingGateSet.v : Mapping gate set U + {CX, SWAP}, where U is an arbitrary set of single-qubit gates. - MappingValidation.v : Check whether two programs (which differ only in SWAP placement) are equivalent. - SwapRoute.v: Simple mapping for an architecture described by a directed graph. @@ -166,10 +160,6 @@ This project is the result of the efforts of many people. The primary contacts f * Runzhou Tao * Finn Voichick -Maintainers: -* Kesha Hietala (@khieta) -* Robert Rand (@rnrand) - This project is supported by the U.S. Department of Energy, Office of Science, Office of Advanced Scientific Computing Research, Quantum Testbed Pathfinder Program under Award Number DE-SC0019040 and the Air Force Office of Scientific Research under Grant Number FA95502110051. ## Citations diff --git a/VOQC/dune b/VOQC/dune index 891d42d6..db75cf24 100644 --- a/VOQC/dune +++ b/VOQC/dune @@ -1,3 +1,4 @@ (coq.theory (name VOQC) - (package coq-voqc)) + (package coq-voqc) + (theories SQIR)) diff --git a/_CoqProject b/_CoqProject index dd18a256..2c1ddb67 100644 --- a/_CoqProject +++ b/_CoqProject @@ -2,4 +2,3 @@ -R _build/default/examples/examples Examples -R _build/default/examples/shor Shor -R _build/default/VOQC VOQC --R _build/default/examples/shor/externals/euler Shor.externals.euler diff --git a/coq-sqir.opam b/coq-sqir.opam index 3c6c6cbd..380ddde2 100644 --- a/coq-sqir.opam +++ b/coq-sqir.opam @@ -3,7 +3,7 @@ opam-version: "2.0" version: "1.1.0" synopsis: "Coq library for reasoning about quantum circuits" description: """ -inQWIRE's VOQC is a Coq library for reasoning +inQWIRE's SQIR is a Coq library for reasoning about quantum circuits """ maintainer: ["inQWIRE Developers"] @@ -13,7 +13,6 @@ homepage: "https://github.com/inQWIRE/SQIR" bug-reports: "https://github.com/inQWIRE/SQIR/issues" depends: [ "dune" {>= "2.8"} - "coq-interval" {>= "4.6.1"} "coq-quantumlib" {>= "1.1.0"} "coq" {>= "8.12"} "odoc" {with-doc} diff --git a/coq-voqc.opam b/coq-voqc.opam index ad4f8f3f..dffc163f 100644 --- a/coq-voqc.opam +++ b/coq-voqc.opam @@ -3,8 +3,8 @@ opam-version: "2.0" version: "1.1.0" synopsis: "A verified optimizer for quantum compilation" description: """ -inQWIRE's VOQC is a Coq tool for verified - compilation of quantum circuits, with some common gate sets +inQWIRE's VOQC is a Coq library for verified + optimization of quantum circuits """ maintainer: ["inQWIRE Developers"] authors: ["inQWIRE"] @@ -13,7 +13,6 @@ homepage: "https://github.com/inQWIRE/SQIR" bug-reports: "https://github.com/inQWIRE/SQIR/issues" depends: [ "dune" {>= "2.8"} - "coq-interval" {>= "4.6.1"} "coq-quantumlib" {>= "1.1.0"} "coq-sqir" {>= "1.1.0"} "coq" {>= "8.12"} diff --git a/dune-project b/dune-project index fe1cd2ae..366aa0c8 100644 --- a/dune-project +++ b/dune-project @@ -1,5 +1,5 @@ (lang dune 2.8) -(name coq-sqirvoqc) +(name coq-sqir-voqc) (version 1.1.0) (using coq 0.2) @@ -13,22 +13,20 @@ (package (name coq-sqir) (synopsis "Coq library for reasoning about quantum circuits") - (description "\| inQWIRE's VOQC is a Coq library for reasoning + (description "\| inQWIRE's SQIR is a Coq library for reasoning "\| about quantum circuits ) (depends - (coq-interval (>= 4.6.1)) (coq-quantumlib (>= 1.1.0)) (coq (>= 8.12)))) (package (name coq-voqc) (synopsis "A verified optimizer for quantum compilation") - (description "\| inQWIRE's VOQC is a Coq tool for verified - "\| compilation of quantum circuits, with some common gate sets + (description "\| inQWIRE's VOQC is a Coq library for verified + "\| optimization of quantum circuits ) (depends - (coq-interval (>= 4.6.1)) (coq-quantumlib (>= 1.1.0)) (coq-sqir (>= 1.1.0)) (coq (>= 8.12)))) diff --git a/examples/examples/dune b/examples/examples/dune index d4b98065..1741c207 100644 --- a/examples/examples/dune +++ b/examples/examples/dune @@ -2,4 +2,4 @@ (coq.theory (name Examples) - (theories SQIR ghz)) + (theories SQIR)) diff --git a/examples/examples/ghz/README.md b/examples/examples/ghz/README.md deleted file mode 100644 index b703aca7..00000000 --- a/examples/examples/ghz/README.md +++ /dev/null @@ -1,8 +0,0 @@ -# GHZ Example - -This directory contains an implementation and proof of GHZ state preparation, plus an example for how to extract Coq/SQIR programs to OCaml/OpenQASM 2.0. You can use this as a model for extracting other SQIR programs. - -How to "run" GHZ: -1. Run `make ghz` in the top-level directory (`../..`). This compiles the GHZ Coq definitions and proofs. -2. Run `./extract.sh` in this directory. This extracts our Coq definitions to OCaml. -3. Run `dune exec --root extraction -- ./ghz.exe N` where N is the number of qubits you want in the GHZ state. This runs our OCaml executable (`ghz.exe`) on the input `N`. It will produce a file called `ghz.qasm` that contains the generated OpenQASM code. diff --git a/examples/examples/ghz/extraction/dune b/examples/examples/ghz/extraction/dune deleted file mode 100644 index af36341b..00000000 --- a/examples/examples/ghz/extraction/dune +++ /dev/null @@ -1,3 +0,0 @@ -(executable - (name ghz) - (libraries ml unix)) diff --git a/examples/examples/ghz/extraction/dune-project b/examples/examples/ghz/extraction/dune-project deleted file mode 100644 index 45acd3f0..00000000 --- a/examples/examples/ghz/extraction/dune-project +++ /dev/null @@ -1 +0,0 @@ -(lang dune 2.7) diff --git a/examples/examples/ghz/ExtrGHZ.v b/examples/ghz/ExtrGHZ.v similarity index 100% rename from examples/examples/ghz/ExtrGHZ.v rename to examples/ghz/ExtrGHZ.v diff --git a/examples/examples/ghz/GHZ.v b/examples/ghz/GHZ.v similarity index 100% rename from examples/examples/ghz/GHZ.v rename to examples/ghz/GHZ.v diff --git a/examples/ghz/README.md b/examples/ghz/README.md new file mode 100644 index 00000000..8db3d18c --- /dev/null +++ b/examples/ghz/README.md @@ -0,0 +1,9 @@ +# GHZ Example + +This directory contains an implementation and proof of GHZ state preparation, plus an example for how to extract Coq/SQIR programs to OCaml/OpenQASM 2.0. You can use this as a model for extracting other SQIR programs. + +How to "run" GHZ: +1. Run `make examples` in the top-level directory (`../..`). This compiles the GHZ Coq definitions and proofs (along with several other examples) and the extracted OCaml code in the `extraction/` directory. +2. In the current directory, run `dune exec --root extraction -- ./ghz.exe N` where N is the number of qubits you want in the GHZ state. This runs our OCaml executable (`ghz.exe`) on the input `N`. It will produce a file called `ghz.qasm` that contains the generated OpenQASM code. + +The code in the `extraction/` directory was generated using the `./extract.sh` script. You can re-generate the extracted code using this script. Note that it was last tested with Coq version 8.15.2. Other versions of Coq will likely require modifications. \ No newline at end of file diff --git a/examples/examples/ghz/dune b/examples/ghz/dune similarity index 97% rename from examples/examples/ghz/dune rename to examples/ghz/dune index 723719c0..d3a428b4 100644 --- a/examples/examples/ghz/dune +++ b/examples/ghz/dune @@ -1,4 +1,3 @@ - (coq.theory (name ghz) (theories SQIR)) diff --git a/examples/examples/ghz/extract.sh b/examples/ghz/extract.sh similarity index 75% rename from examples/examples/ghz/extract.sh rename to examples/ghz/extract.sh index 9f2a035a..c14240fa 100755 --- a/examples/examples/ghz/extract.sh +++ b/examples/ghz/extract.sh @@ -5,10 +5,10 @@ cd extraction # Perform extraction. echo "Extracting code..." -coqc -R ../../.. Top ../../shor/extraction/ExtrOcamlList.v -coqc -R ../../.. Top ../../shor/extraction/ExtrOcamlR.v -coqc -R ../../.. Top ../../shor/extraction/ExtrOcamlNatZ.v -coqc -R ../../.. Top Extraction.v +coqc ExtrOcamlList.v +coqc ExtrOcamlNatZ.v +coqc -R ../../../_build/default/SQIR SQIR ExtrOcamlR.v +coqc -R ../../../_build/default/SQIR SQIR -R ../../../_build/default/examples/ghz ghz Extraction.v # Remove unneeded files. echo "Deleting unneeded files..." diff --git a/examples/ghz/extraction/ExtrOcamlList.v b/examples/ghz/extraction/ExtrOcamlList.v new file mode 100644 index 00000000..21dc5148 --- /dev/null +++ b/examples/ghz/extraction/ExtrOcamlList.v @@ -0,0 +1,13 @@ +Require Coq.extraction.Extraction. +Require Export List. + +(* A few common list functions *) +Extract Constant length => "(fun l -> Z.of_int (List.length l))". +Extract Inlined Constant app => "List.append". +Extract Inlined Constant rev => "List.rev". +Extract Inlined Constant rev_append => "List.rev_append". +Extract Inlined Constant List.map => "List.map". +Extract Inlined Constant fold_right => "(fun f a l -> List.fold_right f l a)". +Extract Inlined Constant forallb => "List.for_all". +Extract Inlined Constant List.tl => "List.tl". +Extract Inlined Constant List.hd_error => "(fun l -> List.nth_opt l 0)". \ No newline at end of file diff --git a/examples/ghz/extraction/ExtrOcamlNatZ.v b/examples/ghz/extraction/ExtrOcamlNatZ.v new file mode 100644 index 00000000..c78e78cf --- /dev/null +++ b/examples/ghz/extraction/ExtrOcamlNatZ.v @@ -0,0 +1,18 @@ +Require Coq.extraction.Extraction. +Require Import ZArith. + +(* Custom extraction from nat -> OCaml Z (arbitrary precision integers) *) +Extract Inductive nat => "Z.t" [ "Z.zero" "Z.succ" ] + "(fun fO fS n -> if Z.equal n Z.zero then fO () else fS (Z.pred n))". +Extract Constant Nat.pred => "(fun a -> Z.max (Z.pred a) Z.zero)". +Extract Inlined Constant Nat.add => "Z.add". +Extract Constant Nat.sub => "(fun a b -> Z.max (Z.sub a b) Z.zero)". +Extract Inlined Constant Nat.mul => "Z.mul". +Extract Inlined Constant Nat.div => "Z.div". +Extract Inlined Constant Nat.modulo => "Z.rem". +Extract Constant Nat.pow => "(fun a b -> Z.pow a (Z.to_int b))". +Extract Inlined Constant Nat.gcd => "Z.gcd". +Extract Constant Nat.log2 => "fun n -> (Z.of_int (Z.log2 n))". +Extract Inlined Constant Nat.eqb => "Z.equal". +Extract Inlined Constant Nat.leb => "Z.leq". +Extract Inlined Constant Nat.ltb => "Z.lt". \ No newline at end of file diff --git a/examples/ghz/extraction/ExtrOcamlR.v b/examples/ghz/extraction/ExtrOcamlR.v new file mode 100644 index 00000000..c0e49007 --- /dev/null +++ b/examples/ghz/extraction/ExtrOcamlR.v @@ -0,0 +1,29 @@ +Require Coq.extraction.Extraction. +Require Export Reals. +Require Import ExtractionGateSet. + +(* Custom extraction from R -> OCaml float. *) +Extract Inlined Constant R => "float". +Extract Inlined Constant R0 => "0.0". +Extract Inlined Constant R1 => "1.0". +Extract Inlined Constant R2 => "2.0". +Extract Inlined Constant R4 => "4.0". +Extract Inlined Constant Rplus => "( +. )". +Extract Inlined Constant Rmult => "( *. )". +Extract Inlined Constant Ropp => "((-.) 0.0)". +Extract Inlined Constant Rinv => "((/.) 1.0)". +Extract Inlined Constant Rminus => "( -. )". +Extract Inlined Constant Rdiv => "( /. )". +Extract Inlined Constant pow => "(fun a b -> a ** Z.to_float b)". +Extract Inlined Constant cos => "cos". +Extract Inlined Constant sin => "sin". +Extract Inlined Constant tan => "tan". +Extract Inlined Constant atan => "atan". +Extract Inlined Constant acos => "acos". +Extract Inlined Constant PI => "Float.pi". +Extract Inlined Constant IZR => "Z.to_float". +Extract Inlined Constant INR => "Z.to_float". + +(* Extracting the following to dummy values to supress warnings *) +Extract Constant ClassicalDedekindReals.sig_forall_dec => "failwith ""Invalid extracted value"" ". +Extract Constant ClassicalDedekindReals.DRealRepr => "failwith ""Invalid extracted value"" ". \ No newline at end of file diff --git a/examples/examples/ghz/extraction/Extraction.v b/examples/ghz/extraction/Extraction.v similarity index 100% rename from examples/examples/ghz/extraction/Extraction.v rename to examples/ghz/extraction/Extraction.v diff --git a/examples/ghz/extraction/dune b/examples/ghz/extraction/dune new file mode 100644 index 00000000..cb6a3469 --- /dev/null +++ b/examples/ghz/extraction/dune @@ -0,0 +1,3 @@ +(executable + (name ghz) + (libraries Ghz_ml unix)) diff --git a/examples/examples/ghz/extraction/ghz.ml b/examples/ghz/extraction/ghz.ml similarity index 100% rename from examples/examples/ghz/extraction/ghz.ml rename to examples/ghz/extraction/ghz.ml diff --git a/examples/examples/ghz/extraction/ml/ExtrGHZ.ml b/examples/ghz/extraction/ml/ExtrGHZ.ml similarity index 100% rename from examples/examples/ghz/extraction/ml/ExtrGHZ.ml rename to examples/ghz/extraction/ml/ExtrGHZ.ml diff --git a/examples/examples/ghz/extraction/ml/ExtractionGateSet.ml b/examples/ghz/extraction/ml/ExtractionGateSet.ml similarity index 100% rename from examples/examples/ghz/extraction/ml/ExtractionGateSet.ml rename to examples/ghz/extraction/ml/ExtractionGateSet.ml diff --git a/examples/examples/ghz/extraction/ml/Qasm.ml b/examples/ghz/extraction/ml/Qasm.ml similarity index 100% rename from examples/examples/ghz/extraction/ml/Qasm.ml rename to examples/ghz/extraction/ml/Qasm.ml diff --git a/examples/examples/ghz/extraction/ml/dune b/examples/ghz/extraction/ml/dune similarity index 85% rename from examples/examples/ghz/extraction/ml/dune rename to examples/ghz/extraction/ml/dune index 2a15689a..5ff7b3d6 100644 --- a/examples/examples/ghz/extraction/ml/dune +++ b/examples/ghz/extraction/ml/dune @@ -1,5 +1,5 @@ (library - (name ml) + (name Ghz_ml) (wrapped false) (flags (:standard -w -3-32-33-34-39)) (libraries zarith unix)) \ No newline at end of file diff --git a/examples/shor/README.md b/examples/shor/README.md index 5c8ec386..e70ae654 100644 --- a/examples/shor/README.md +++ b/examples/shor/README.md @@ -16,7 +16,7 @@ Core formalization Utilities * ContFrac.v - Results about continued fractions. -* EulerTotient.v - Re-statement of Euler's totient function from externals/euler. +* EulerTotient.v - Re-statement of Euler's totient function from the [coq-euler](https://github.com/taorunz/euler) library. * ExtrShor.v - Shor's algorithm defined in a gate set amenable to extraction; proofs that the new definition is equivalent to the original. * NumTheory.v - General number theory results. * Reduction.v - Proof of the reduction from factorization to order finding. @@ -30,16 +30,17 @@ Compiling the extracted code requires dune and zarith (`opam install dune zarith Our extracted code uses the [ddsim simulator](https://github.com/iic-jku/ddsim) (through its Qiskit interface) to execute Shor's order finding circuit so running our extracted code requires **Python version >= 3.6, qiskit, and ddsim**. Once you have a suitable version of Python, you can install the latter two with `pip install qiskit jkq.ddsim`. If you run into trouble with your Python environment, then consider using anaconda per [these directions for installing Qiskit](https://qiskit.org/documentation/getting_started.html). -To test your Python setup, run `python run_circuit.py test.qasm`. You should see the output 7, which corresponds to measuring '111'. Our OCaml code runs this command with a generated order finding circuit as input. If you find that you need to run a different command on your system (e.g., `python3.9 ...`), then you can modify line 45 of [extraction/ml/Run.ml](extraction/ml/Run.ml). +To test your Python setup, run `python run_circuit.py test.qasm`. You should see the output 7, which corresponds to measuring '111'. Our OCaml code runs this command with a generated order finding circuit as input. If you find that you need to run a different command on your system (e.g., `python3.9 ...`), then you can modify line 47 of [extraction/ml/Run.ml](extraction/ml/Run.ml). ### Extraction to OCaml -The first step is to compile the Coq code. You can do this by running `make shor` in the top-level (`../..`) directory. The next step is to extract the compiled Coq code to OCaml by running `./extract.sh` in the current directory. This will produce a bunch of .ml files in `extraction/ml` and compile them into an executable in `extraction/_build`. +You can compile the Coq code and extracted OCaml code in the `extraction/` directory by running `make shor` in the top-level (`../..`) directory. + +The code in the `extraction/` directory was generated using the `./extract.sh` script. You can re-generate and re-build the extracted code using this script. Note that it was last tested with Coq version 8.15.2. Other versions of Coq will likely require modifications. If you are on MacOS, you may see the following warnings: ``` ld: warning: directory not found for option '-L/opt/local/lib' -ld: warning: directory not found for option '-L/opt/homebrew/lib' ``` This is caused by our use of zarith, and seems to be safe to ignore. diff --git a/examples/shor/dune b/examples/shor/dune index e9f5eb9a..2604a132 100644 --- a/examples/shor/dune +++ b/examples/shor/dune @@ -1,5 +1,3 @@ -(include_subdirs qualified) - (coq.theory (name Shor) (theories SQIR Examples)) diff --git a/examples/shor/externals/euler b/examples/shor/externals/euler deleted file mode 160000 index 74df6940..00000000 --- a/examples/shor/externals/euler +++ /dev/null @@ -1 +0,0 @@ -Subproject commit 74df69402ab5346c2b016f0ac7ed64cd805100ed diff --git a/examples/shor/extract.sh b/examples/shor/extract.sh index a4c5dd29..97c86483 100755 --- a/examples/shor/extract.sh +++ b/examples/shor/extract.sh @@ -5,10 +5,10 @@ cd extraction # Perform extraction. echo "Extracting code..." -coqc -R ../../.. Top ExtrOcamlList.v -coqc -R ../../.. Top ExtrOcamlR.v -coqc -R ../../.. Top ExtrOcamlNatZ.v -coqc -R ../../.. Top Extraction.v +coqc ExtrOcamlList.v +coqc ExtrOcamlNatZ.v +coqc -R ../../../_build/default/SQIR SQIR ExtrOcamlR.v +coqc -R ../../../_build/default/SQIR SQIR -R ../../../_build/default/examples/examples Examples -R ../../../_build/default/examples/shor Shor Extraction.v # Remove unneeded files. echo "Deleting unneeded files..." @@ -23,7 +23,7 @@ rm -f Bin* ClassicalDedekindReals.ml ConstructiveCauchyReals.ml NumTheory.ml \ echo "Moving generated files to ml/..." mv ExtractionGateSet.ml ContFrac.ml Datatypes.ml DiscreteProb.ml ExtrShor.ml \ List0.ml Main.ml ModMult.ml Nat.ml PeanoNat.ml RCIR.ml RealAux.ml \ - Rfunctions.ml Shor.ml \ + Shor.ml Summation.ml \ ml # Build extracted code. diff --git a/examples/shor/extraction/Extraction.v b/examples/shor/extraction/Extraction.v index 7ed558f4..4b91c6d0 100644 --- a/examples/shor/extraction/Extraction.v +++ b/examples/shor/extraction/Extraction.v @@ -1,5 +1,5 @@ Require Coq.extraction.Extraction. -Require Import DiscreteProb. +Require Import QuantumLib.DiscreteProb. Require Import Shor. Require Import Main. diff --git a/examples/shor/extraction/dune b/examples/shor/extraction/dune index bab2826f..442d72b9 100644 --- a/examples/shor/extraction/dune +++ b/examples/shor/extraction/dune @@ -1,3 +1,4 @@ (executable (name run_shor) - (libraries ml unix)) + (flags (:standard -w -32)) + (libraries Shor_ml unix)) diff --git a/examples/shor/extraction/dune-project b/examples/shor/extraction/dune-project deleted file mode 100644 index 45acd3f0..00000000 --- a/examples/shor/extraction/dune-project +++ /dev/null @@ -1 +0,0 @@ -(lang dune 2.7) diff --git a/examples/shor/extraction/ml/DiscreteProb.ml b/examples/shor/extraction/ml/DiscreteProb.ml index 4620f91e..93b45702 100644 --- a/examples/shor/extraction/ml/DiscreteProb.ml +++ b/examples/shor/extraction/ml/DiscreteProb.ml @@ -2,11 +2,12 @@ open Datatypes open List0 open Nat open RealAux +open Summation (** val sum_over_list : float list -> float **) let sum_over_list l = - coq_Rsum (length l) (fun i -> nth i l (Z.to_float Z.zero)) + big_sum coq_R_is_monoid (fun i -> nth i l (Z.to_float Z.zero)) (length l) (** val sample : float list -> float -> Z.t **) diff --git a/examples/shor/extraction/ml/NumTheory.ml b/examples/shor/extraction/ml/NumTheory.ml deleted file mode 100644 index 139597f9..00000000 --- a/examples/shor/extraction/ml/NumTheory.ml +++ /dev/null @@ -1,2 +0,0 @@ - - diff --git a/examples/shor/extraction/ml/RealAux.ml b/examples/shor/extraction/ml/RealAux.ml index ea8f382f..e41ed22e 100644 --- a/examples/shor/extraction/ml/RealAux.ml +++ b/examples/shor/extraction/ml/RealAux.ml @@ -1,9 +1,6 @@ -open Rfunctions +open Summation -(** val coq_Rsum : Z.t -> (Z.t -> float) -> float **) +(** val coq_R_is_monoid : float coq_Monoid **) -let coq_Rsum n f = - (fun fO fS n -> if Z.equal n Z.zero then fO () else fS (Z.pred n)) - (fun _ -> Z.to_float Z.zero) - (fun n0 -> sum_f_R0 f n0) - n +let coq_R_is_monoid = + { coq_Gzero = (Z.to_float Z.zero); coq_Gplus = ( +. ) } diff --git a/examples/shor/extraction/ml/Rfunctions.ml b/examples/shor/extraction/ml/Rfunctions.ml deleted file mode 100644 index 2059ba14..00000000 --- a/examples/shor/extraction/ml/Rfunctions.ml +++ /dev/null @@ -1,8 +0,0 @@ - -(** val sum_f_R0 : (Z.t -> float) -> Z.t -> float **) - -let rec sum_f_R0 f n = - (fun fO fS n -> if Z.equal n Z.zero then fO () else fS (Z.pred n)) - (fun _ -> f Z.zero) - (fun i -> ( +. ) (sum_f_R0 f i) (f (Z.succ i))) - n diff --git a/examples/shor/extraction/ml/Summation.ml b/examples/shor/extraction/ml/Summation.ml new file mode 100644 index 00000000..c9b4962f --- /dev/null +++ b/examples/shor/extraction/ml/Summation.ml @@ -0,0 +1,10 @@ + +type 'g coq_Monoid = { coq_Gzero : 'g; coq_Gplus : ('g -> 'g -> 'g) } + +(** val big_sum : 'a1 coq_Monoid -> (Z.t -> 'a1) -> Z.t -> 'a1 **) + +let rec big_sum h f n = + (fun fO fS n -> if Z.equal n Z.zero then fO () else fS (Z.pred n)) + (fun _ -> h.coq_Gzero) + (fun n' -> h.coq_Gplus (big_sum h f n') (f n')) + n diff --git a/examples/shor/extraction/ml/dune b/examples/shor/extraction/ml/dune index 2a15689a..0bebec13 100644 --- a/examples/shor/extraction/ml/dune +++ b/examples/shor/extraction/ml/dune @@ -1,5 +1,5 @@ (library - (name ml) + (name Shor_ml) (wrapped false) (flags (:standard -w -3-32-33-34-39)) (libraries zarith unix)) \ No newline at end of file