move src/Experiments/NewPipeline/ to src/

1 files changed, 74 insertions, 0 deletions

diff --git a/src/StandaloneHaskellMain.v b/src/StandaloneHaskellMain.v
new file mode 100644
index 000000000..1a07b827f
--- /dev/null
+++ b/src/StandaloneHaskellMain.v
@@ -0,0 +1,74 @@
+Require Export Coq.extraction.Extraction.
+Require Export Coq.extraction.ExtrHaskellBasic.
+Require Export Coq.extraction.ExtrHaskellString.
+Require Import Coq.Lists.List.
+Require Import Coq.Strings.String.
+Require Crypto.Util.Strings.String.
+Require Import Crypto.Util.Strings.Decimal.
+Require Import Crypto.Util.Strings.HexString.
+Require Import Crypto.PushButtonSynthesis.
+Require Import Crypto.CLI.
+Require Import Crypto.Util.Notations.
+Import ListNotations. Local Open Scope string_scope.
+
+Global Set Warnings Append "-extraction-opaque-accessed".
+Extraction Language Haskell.
+Global Unset Extraction Optimize.
+
+Axiom IO_unit : Set.
+Axiom _IO : Set -> Set.
+Axiom printf_string : string -> _IO unit.
+Axiom getArgs : _IO (list string).
+Axiom getProgName : _IO string.
+Axiom raise_failure : forall A, string -> A.
+Axiom _IO_bind : forall A B, _IO A -> (A -> _IO B) -> _IO B.
+Axiom _IO_return : forall A : Set, A -> _IO A.
+Axiom cast_io : _IO unit -> IO_unit.
+Extract Constant printf_string =>
+"\s -> Text.Printf.printf ""%s"" s".
+Extract Constant _IO "a" => "GHC.Base.IO a".
+Extract Inlined Constant getArgs => "System.Environment.getArgs".
+Extract Inlined Constant getProgName => "System.Environment.getProgName".
+Extract Constant raise_failure => "\x -> Prelude.error x".
+Extract Inlined Constant _IO_bind => "(Prelude.>>=)".
+Extract Inlined Constant _IO_return => "return".
+Extract Inlined Constant IO_unit => "GHC.Base.IO ()".
+Extract Inlined Constant cast_io => "".
+
+Local Notation "x <- y ; f" := (_IO_bind _ _ y (fun x => f)).
+
+Module UnsaturatedSolinas.
+  Definition main : IO_unit
+    := cast_io
+         (argv <- getArgs;
+            prog <- getProgName;
+            ForExtraction.UnsaturatedSolinas.PipelineMain
+              (prog::argv)
+              (fun res => printf_string
+                         (String.concat "" res))
+              (fun err => raise_failure _ (String.concat String.NewLine err))).
+End UnsaturatedSolinas.
+
+Module WordByWordMontgomery.
+  Definition main : IO_unit
+    := cast_io
+         (argv <- getArgs;
+            prog <- getProgName;
+            ForExtraction.WordByWordMontgomery.PipelineMain
+              (prog::argv)
+              (fun res => printf_string
+                         (String.concat "" res))
+              (fun err => raise_failure _ (String.concat String.NewLine err))).
+End WordByWordMontgomery.
+
+Module SaturatedSolinas.
+  Definition main : IO_unit
+    := cast_io
+         (argv <- getArgs;
+            prog <- getProgName;
+            ForExtraction.SaturatedSolinas.PipelineMain
+              (prog::argv)
+              (fun res => printf_string
+                         (String.concat "" res))
+              (fun err => raise_failure _ (String.concat String.NewLine err))).
+End SaturatedSolinas.