diff options
Diffstat (limited to 'src/StandaloneHaskellMain.v')
-rw-r--r-- | src/StandaloneHaskellMain.v | 74 |
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. |