move src/Experiments/NewPipeline/ to src/

1 files changed, 121 insertions, 0 deletions

diff --git a/src/StandaloneOCamlMain.v b/src/StandaloneOCamlMain.v
new file mode 100644
index 000000000..cb2a20904
--- /dev/null
+++ b/src/StandaloneOCamlMain.v
@@ -0,0 +1,121 @@
+Require Export Coq.extraction.Extraction.
+Require Export Coq.extraction.ExtrOcamlBasic.
+Require Export Coq.extraction.ExtrOcamlString.
+Require Import Coq.Lists.List.
+Require Import Coq.Strings.Ascii.
+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 Ocaml.
+Global Unset Extraction Optimize.
+
+Inductive int : Set := int_O | int_S (x : int).
+
+Axiom printf_char : Ascii.ascii -> unit.
+Axiom flush : unit -> unit.
+Axiom string : Set.
+Axiom string_length : string -> int.
+Axiom string_get : string -> int -> Ascii.ascii.
+Axiom sys_argv : list string.
+Axiom string_init : int -> (int -> Ascii.ascii) -> string.
+Axiom raise_Failure : forall A, string -> A.
+
+Extract Inductive int
+=> int [ "0" "Pervasives.succ" ]
+       "(fun fO fS n -> if n=0 then fO () else fS (n-1))".
+Extract Constant printf_char =>
+"fun c -> Printf.printf ""%c%!"" c".
+Extract Constant flush =>
+"fun () -> Printf.printf ""%!""".
+Extract Inlined Constant string => "string".
+Extract Inlined Constant string_length => "String.length".
+Extract Inlined Constant string_get => "String.get".
+Extract Constant sys_argv => "Array.to_list Sys.argv".
+Extract Inlined Constant string_init => "String.init".
+Extract Constant raise_Failure => "fun x -> raise (Failure x)".
+
+Fixpoint nat_of_int (x : int) : nat
+  := match x with
+     | int_O => O
+     | int_S x' => S (nat_of_int x')
+     end.
+Fixpoint int_of_nat (x : nat) : int
+  := match x with
+     | O => int_O
+     | S x' => int_S (int_of_nat x')
+     end.
+Coercion nat_of_int : int >-> nat.
+Coercion int_of_nat : nat >-> int.
+
+Definition string_of_Coq_string (s : String.string) : string
+  := let s := String.to_list s in
+     string_init
+       (List.length s)
+       (fun n => List.nth n s "?"%char).
+
+Definition string_to_Coq_string (s : string) : String.string
+  := String.of_list
+       (List.map (fun n:nat => string_get s n) (List.seq 0 (string_length s))).
+
+Definition seq {A B} (x : unit -> A) (f : A -> B) : B := let y := x tt in f y.
+Extraction NoInline seq.
+(*
+Axiom seq : forall A B, (unit -> A) -> (A -> B) -> B.
+Extract Inlined Constant seq => "(fun x f => let y = x () in f y)".
+*)
+
+Fixpoint list_iter {A} (f : A -> unit) (ls : list A) : unit
+  := match ls with
+     | cons x xs => seq (fun _ => f x) (fun _ => @list_iter A f xs)
+     | nil => tt
+     end.
+
+Definition printf_list_string (strs : list String.string) : unit
+  := list_iter
+       (fun ls
+        => list_iter printf_char (String.to_list ls))
+       strs.
+Definition printf_list_string_with_newlines (strs : list String.string) : unit
+  := match strs with
+     | nil => printf_list_string nil
+     | str :: strs => printf_list_string (str :: List.map (String.String Ascii.NewLine) strs
+                                              ++ [String.NewLine; String.NewLine])%list
+     end.
+
+Definition raise_failure {A} (msg : list String.string) : A
+  := seq (fun _ => printf_list_string_with_newlines msg)
+         (fun _ => raise_Failure _ (string_of_Coq_string "Synthesis failed")).
+
+Module UnsaturatedSolinas.
+  Definition main : unit
+    := let argv := List.map string_to_Coq_string sys_argv in
+       ForExtraction.UnsaturatedSolinas.PipelineMain
+         argv
+         printf_list_string
+         raise_failure.
+End UnsaturatedSolinas.
+
+Module WordByWordMontgomery.
+  Definition main : unit
+    := let argv := List.map string_to_Coq_string sys_argv in
+       ForExtraction.WordByWordMontgomery.PipelineMain
+         argv
+         printf_list_string
+         raise_failure.
+End WordByWordMontgomery.
+
+Module SaturatedSolinas.
+  Definition main : unit
+    := let argv := List.map string_to_Coq_string sys_argv in
+       ForExtraction.SaturatedSolinas.PipelineMain
+         argv
+         printf_list_string
+         raise_failure.
+End SaturatedSolinas.