diff --git a/.gitignore b/.gitignore index 20857e3f68..f35597ecb9 100644 --- a/.gitignore +++ b/.gitignore @@ -223,7 +223,6 @@ src/ExtractionOCaml/perf_word_by_word_montgomery.exe src/ExtractionOCaml/*.cmi src/ExtractionOCaml/*.cmx src/ExtractionOCaml/*.ml -src/ExtractionOCaml/*.mli src/ExtractionOCaml/*.o src/Rewriter/PerfTesting/Specific/generated/*.v src/Rewriter/PerfTesting/Specific/generated/*.log diff --git a/Makefile b/Makefile index de8b952dc1..5e3af75627 100644 --- a/Makefile +++ b/Makefile @@ -609,25 +609,20 @@ $(BEDROCK2_STANDALONE:%=src/ExtractionHaskell/%.hs): src/Bedrock/Standalone/Stan pre-standalone-extracted: $(STANDALONE_OCAML:%=src/ExtractionOCaml/%.ml) $(STANDALONE_HASKELL:%=src/ExtractionHaskell/%.hs) $(STANDALONE_OCAML:%=src/ExtractionOCaml/%.ml) : %.ml : %.v - $(SHOW)'COQC $<' - $(HIDE)$(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) $< - $(HIDE)cat $*.tmp.ml | tr -d '\r' > $@ && rm $*.tmp.ml - $(HIDE)cat $*.tmp.mli | tr -d '\r' > $*.mli && rm $*.tmp.mli + $(SHOW)'COQC $< > $@' + $(HIDE)$(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) $< > $@.tmp + $(HIDE)cat $@.tmp | tr -d '\r' > $@ && rm -f $@.tmp $(STANDALONE_HASKELL:%=src/ExtractionHaskell/%.hs) : %.hs : %.v src/haskell.sed $(SHOW)'COQC $< > $@' $(HIDE)$(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) $< > $@.tmp - $(HIDE)cat $@.tmp | tr -d '\r' | sed -f src/haskell.sed > $@ && rm $@.tmp + $(HIDE)cat $@.tmp | tr -d '\r' | sed -f src/haskell.sed > $@ && rm -f $@.tmp # pass -w -20 to disable the unused argument warning # unix package needed for Unix.gettimeofday for the perf_* binaries -$(STANDALONE_OCAML:%=src/ExtractionOCaml/%.cmi) : %.cmi : %.ml - $(SHOW)'$(CAMLOPT_PERF_SHOW) $*.mli' - $(HIDE)$(TIMER) $(CAMLOPT_PERF) -package unix -w -20 -g $*.mli - -$(STANDALONE_OCAML:%=src/ExtractionOCaml/%) : % : %.ml %.cmi +$(STANDALONE_OCAML:%=src/ExtractionOCaml/%) : % : %.ml $(SHOW)'$(CAMLOPT_PERF_SHOW) $< -o $@' - $(HIDE)$(TIMER) $(CAMLOPT_PERF) -package unix -linkpkg -w -20 -g -I src/ExtractionOCaml/ -o $@ $< + $(HIDE)$(TIMER) $(CAMLOPT_PERF) -package unix -linkpkg -w -20 -g -o $@ $< $(STANDALONE_HASKELL:%=src/ExtractionHaskell/%) : % : %.hs $(SHOW)'GHC $< -o $@' diff --git a/src/ExtractionOCaml/base_conversion.v b/src/ExtractionOCaml/base_conversion.v index d0674952d2..e59ade8dd9 100644 --- a/src/ExtractionOCaml/base_conversion.v +++ b/src/ExtractionOCaml/base_conversion.v @@ -1,3 +1,3 @@ Require Import Crypto.StandaloneOCamlMain. -Extraction "src/ExtractionOCaml/base_conversion.tmp" BaseConversion.main. +(*Redirect "/tmp/base_conversion.ml"*) Recursive Extraction BaseConversion.main. diff --git a/src/ExtractionOCaml/bedrock2_base_conversion.v b/src/ExtractionOCaml/bedrock2_base_conversion.v index 75f344ca66..32686ff312 100644 --- a/src/ExtractionOCaml/bedrock2_base_conversion.v +++ b/src/ExtractionOCaml/bedrock2_base_conversion.v @@ -1,4 +1,4 @@ Require Import Crypto.Bedrock.Standalone.StandaloneOCamlMain. Import Bedrock2First. -Extraction "src/ExtractionOCaml/bedrock2_base_conversion.tmp" BaseConversion.main. +(*Redirect "/tmp/bedrock2_base_conversion.ml"*) Recursive Extraction BaseConversion.main. diff --git a/src/ExtractionOCaml/bedrock2_saturated_solinas.v b/src/ExtractionOCaml/bedrock2_saturated_solinas.v index 907b3ec60c..02aa4fe94f 100644 --- a/src/ExtractionOCaml/bedrock2_saturated_solinas.v +++ b/src/ExtractionOCaml/bedrock2_saturated_solinas.v @@ -1,4 +1,4 @@ Require Import Crypto.Bedrock.Standalone.StandaloneOCamlMain. Import Bedrock2First. -Extraction "src/ExtractionOCaml/bedrock2_saturated_solinas.tmp" SaturatedSolinas.main. +(*Redirect "/tmp/bedrock2_saturated_solinas.ml"*) Recursive Extraction SaturatedSolinas.main. diff --git a/src/ExtractionOCaml/bedrock2_unsaturated_solinas.v b/src/ExtractionOCaml/bedrock2_unsaturated_solinas.v index 8742315d1b..90ad60fed1 100644 --- a/src/ExtractionOCaml/bedrock2_unsaturated_solinas.v +++ b/src/ExtractionOCaml/bedrock2_unsaturated_solinas.v @@ -1,4 +1,4 @@ Require Import Crypto.Bedrock.Standalone.StandaloneOCamlMain. Import Bedrock2First. -Extraction "src/ExtractionOCaml/bedrock2_unsaturated_solinas.tmp" UnsaturatedSolinas.main. +(*Redirect "/tmp/bedrock2_unsaturated_solinas.ml"*) Recursive Extraction UnsaturatedSolinas.main. diff --git a/src/ExtractionOCaml/bedrock2_word_by_word_montgomery.v b/src/ExtractionOCaml/bedrock2_word_by_word_montgomery.v index 2a6e0c5638..a8af9714d2 100644 --- a/src/ExtractionOCaml/bedrock2_word_by_word_montgomery.v +++ b/src/ExtractionOCaml/bedrock2_word_by_word_montgomery.v @@ -1,4 +1,4 @@ Require Import Crypto.Bedrock.Standalone.StandaloneOCamlMain. Import Bedrock2First. -Extraction "src/ExtractionOCaml/bedrock2_word_by_word_montgomery.tmp" WordByWordMontgomery.main. +(*Redirect "/tmp/bedrock2_word_by_word_montgomery.ml"*) Recursive Extraction WordByWordMontgomery.main. diff --git a/src/ExtractionOCaml/perf_unsaturated_solinas.v b/src/ExtractionOCaml/perf_unsaturated_solinas.v index 90e2334c9e..8782b1e275 100644 --- a/src/ExtractionOCaml/perf_unsaturated_solinas.v +++ b/src/ExtractionOCaml/perf_unsaturated_solinas.v @@ -1,3 +1,3 @@ Require Import Crypto.Rewriter.PerfTesting.StandaloneOCamlMain. -Extraction "src/ExtractionOCaml/perf_unsaturated_solinas.tmp" UnsaturatedSolinas.main. +(*Redirect "/tmp/perf_unsaturated_solinas.ml"*) Recursive Extraction UnsaturatedSolinas.main. diff --git a/src/ExtractionOCaml/perf_word_by_word_montgomery.v b/src/ExtractionOCaml/perf_word_by_word_montgomery.v index 4f1c678772..b479af2c9b 100644 --- a/src/ExtractionOCaml/perf_word_by_word_montgomery.v +++ b/src/ExtractionOCaml/perf_word_by_word_montgomery.v @@ -1,3 +1,3 @@ Require Import Crypto.Rewriter.PerfTesting.StandaloneOCamlMain. -Extraction "src/ExtractionOCaml/perf_word_by_word_montgomery.tmp" WordByWordMontgomery.main. +(*Redirect "/tmp/perf_word_by_word_montgomery.ml"*) Recursive Extraction WordByWordMontgomery.main. diff --git a/src/ExtractionOCaml/saturated_solinas.v b/src/ExtractionOCaml/saturated_solinas.v index 792e1cb835..3664b34e3b 100644 --- a/src/ExtractionOCaml/saturated_solinas.v +++ b/src/ExtractionOCaml/saturated_solinas.v @@ -1,3 +1,3 @@ Require Import Crypto.StandaloneOCamlMain. -Extraction "src/ExtractionOCaml/saturated_solinas.tmp" SaturatedSolinas.main. +(*Redirect "/tmp/saturated_solinas.ml"*) Recursive Extraction SaturatedSolinas.main. diff --git a/src/ExtractionOCaml/unsaturated_solinas.v b/src/ExtractionOCaml/unsaturated_solinas.v index 8e957a8b45..50de2615bb 100644 --- a/src/ExtractionOCaml/unsaturated_solinas.v +++ b/src/ExtractionOCaml/unsaturated_solinas.v @@ -1,3 +1,3 @@ Require Import Crypto.StandaloneOCamlMain. -Extraction "src/ExtractionOCaml/unsaturated_solinas.tmp" UnsaturatedSolinas.main. +(*Redirect "/tmp/unsaturated_solinas.ml"*) Recursive Extraction UnsaturatedSolinas.main. diff --git a/src/ExtractionOCaml/with_bedrock2_base_conversion.v b/src/ExtractionOCaml/with_bedrock2_base_conversion.v index 622e5c3862..c91bc936a7 100644 --- a/src/ExtractionOCaml/with_bedrock2_base_conversion.v +++ b/src/ExtractionOCaml/with_bedrock2_base_conversion.v @@ -1,4 +1,4 @@ Require Import Crypto.Bedrock.Standalone.StandaloneOCamlMain. Import Bedrock2Later. -Extraction "src/ExtractionOCaml/with_bedrock2_base_conversion.tmp" BaseConversion.main. +(*Redirect "/tmp/with_bedrock2_base_conversion.ml"*) Recursive Extraction BaseConversion.main. diff --git a/src/ExtractionOCaml/with_bedrock2_saturated_solinas.v b/src/ExtractionOCaml/with_bedrock2_saturated_solinas.v index 9b2547df48..76d2c4068d 100644 --- a/src/ExtractionOCaml/with_bedrock2_saturated_solinas.v +++ b/src/ExtractionOCaml/with_bedrock2_saturated_solinas.v @@ -1,4 +1,4 @@ Require Import Crypto.Bedrock.Standalone.StandaloneOCamlMain. Import Bedrock2Later. -Extraction "src/ExtractionOCaml/with_bedrock2_saturated_solinas.tmp" SaturatedSolinas.main. +(*Redirect "/tmp/with_bedrock2_saturated_solinas.ml"*) Recursive Extraction SaturatedSolinas.main. diff --git a/src/ExtractionOCaml/with_bedrock2_unsaturated_solinas.v b/src/ExtractionOCaml/with_bedrock2_unsaturated_solinas.v index 74d3b13e81..7badb744ce 100644 --- a/src/ExtractionOCaml/with_bedrock2_unsaturated_solinas.v +++ b/src/ExtractionOCaml/with_bedrock2_unsaturated_solinas.v @@ -1,4 +1,4 @@ Require Import Crypto.Bedrock.Standalone.StandaloneOCamlMain. Import Bedrock2Later. -Extraction "src/ExtractionOCaml/with_bedrock2_unsaturated_solinas.tmp" UnsaturatedSolinas.main. +(*Redirect "/tmp/with_bedrock2_unsaturated_solinas.ml"*) Recursive Extraction UnsaturatedSolinas.main. diff --git a/src/ExtractionOCaml/with_bedrock2_word_by_word_montgomery.v b/src/ExtractionOCaml/with_bedrock2_word_by_word_montgomery.v index b31bef8c15..f6f4e68624 100644 --- a/src/ExtractionOCaml/with_bedrock2_word_by_word_montgomery.v +++ b/src/ExtractionOCaml/with_bedrock2_word_by_word_montgomery.v @@ -1,4 +1,4 @@ Require Import Crypto.Bedrock.Standalone.StandaloneOCamlMain. Import Bedrock2Later. -Extraction "src/ExtractionOCaml/with_bedrock2_word_by_word_montgomery.tmp" WordByWordMontgomery.main. +(*Redirect "/tmp/with_bedrock2_word_by_word_montgomery.ml"*) Recursive Extraction WordByWordMontgomery.main. diff --git a/src/ExtractionOCaml/word_by_word_montgomery.v b/src/ExtractionOCaml/word_by_word_montgomery.v index 916c30ff95..01f8bdcfd3 100644 --- a/src/ExtractionOCaml/word_by_word_montgomery.v +++ b/src/ExtractionOCaml/word_by_word_montgomery.v @@ -1,3 +1,3 @@ Require Import Crypto.StandaloneOCamlMain. -Extraction "src/ExtractionOCaml/word_by_word_montgomery.tmp" WordByWordMontgomery.main. +(*Redirect "/tmp/word_by_word_montgomery.ml"*) Recursive Extraction WordByWordMontgomery.main. diff --git a/src/Rewriter/PerfTesting/StandaloneOCamlMain.v b/src/Rewriter/PerfTesting/StandaloneOCamlMain.v index edbef9d3e3..7cb713c977 100644 --- a/src/Rewriter/PerfTesting/StandaloneOCamlMain.v +++ b/src/Rewriter/PerfTesting/StandaloneOCamlMain.v @@ -7,8 +7,7 @@ Import ListNotations. Local Open Scope list_scope. (** We pull a hack to get coqchk to not report these as axioms; for this, all we care about is that there exists a model. *) Module Type OCamlPrimitivesT. - Axiom OCaml_float : Set. - Notation float := OCaml_float. + Axiom float : Set. Axiom Unix_gettimeofday : unit -> float. Axiom Sys_time : unit -> float. Axiom fsub : float -> float -> float. @@ -16,19 +15,17 @@ Module Type OCamlPrimitivesT. End OCamlPrimitivesT. Module Export OCamlPrimitives : OCamlPrimitivesT. - Definition OCaml_float : Set := unit. - Notation float := OCaml_float. + Definition float : Set := unit. Definition Unix_gettimeofday : unit -> float := fun 'tt => tt. Definition Sys_time : unit -> float := fun 'tt => tt. Definition fsub : float -> float -> float := fun _ _ => tt. Definition printf_float : float -> unit := fun _ => tt. End OCamlPrimitives. -(* We cannot inline these constants due to COQBUG(https://github.com/coq/coq/issues/16169) *) -Extract (*Inlined*) Constant float => "float". -Extract (*Inlined*) Constant Unix_gettimeofday => "Unix.gettimeofday". -Extract (*Inlined*) Constant Sys_time => "Sys.time". -Extract (*Inlined*) Constant fsub => "(-.)". +Extract Inlined Constant float => "float". +Extract Inlined Constant Unix_gettimeofday => "Unix.gettimeofday". +Extract Inlined Constant Sys_time => "Sys.time". +Extract Inlined Constant fsub => "(-.)". Extract Constant printf_float => "fun f -> Printf.printf ""%f%!"" f". diff --git a/src/StandaloneOCamlMain.v b/src/StandaloneOCamlMain.v index 2bf75629c1..505063a0e9 100644 --- a/src/StandaloneOCamlMain.v +++ b/src/StandaloneOCamlMain.v @@ -22,79 +22,66 @@ Inductive int : Set := int_O | int_S (x : int). this, all we care about is that there exists a model. *) Module Type OCamlPrimitivesT. - Axiom OCaml_in_channel : Set. - Notation in_channel := OCaml_in_channel. - Axiom OCaml_out_channel : Set. - Notation out_channel := OCaml_out_channel. + Axiom in_channel : Set. + Axiom out_channel : Set. Axiom fprintf_char : out_channel -> Ascii.ascii -> unit. Axiom flush : out_channel -> unit. - Axiom OCaml_stdin : in_channel. - Notation stdin := OCaml_stdin. - Axiom OCaml_stdout : out_channel. - Notation stdout := OCaml_stdout. - Axiom OCaml_string : Set. - Notation string := OCaml_string. + Axiom stdin : in_channel. + Axiom stdout : out_channel. + 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 : string -> unit. - Axiom OCaml_open_in : string -> in_channel. - Notation open_in := OCaml_open_in. - Axiom OCaml_open_out : string -> out_channel. - Notation open_out := OCaml_open_out. - Axiom OCaml_close_in : in_channel -> unit. - Notation close_in := OCaml_close_in. - Axiom OCaml_close_out : out_channel -> unit. - Notation close_out := OCaml_close_out. + Axiom open_in : string -> in_channel. + Axiom open_out : string -> out_channel. + Axiom close_in : in_channel -> unit. + Axiom close_out : out_channel -> unit. Axiom read_channel_rev : in_channel -> list string. End OCamlPrimitivesT. Module Export OCamlPrimitives : OCamlPrimitivesT. - Definition OCaml_in_channel : Set := unit. - Notation in_channel := OCaml_in_channel. - Definition OCaml_out_channel : Set := unit. - Notation out_channel := OCaml_out_channel. + Definition in_channel : Set := unit. + Definition out_channel : Set := unit. Definition fprintf_char : out_channel -> Ascii.ascii -> unit := fun _ _ => tt. Definition flush : out_channel -> unit := fun _ => tt. - Definition OCaml_stdin : in_channel := tt. - Definition OCaml_stdout : out_channel := tt. - Definition OCaml_string : Set := unit. - Notation string := OCaml_string. + Definition stdin : in_channel := tt. + Definition stdout : out_channel := tt. + Definition string : Set := unit. Definition string_length : string -> int := fun _ => int_O. Definition string_get : string -> int -> Ascii.ascii := fun _ _ => "000"%char. Definition sys_argv : list string := nil. Definition string_init : int -> (int -> Ascii.ascii) -> string := fun _ _ => tt. Definition raise_Failure : string -> unit := fun _ => tt. - Definition OCaml_open_in : string -> in_channel := fun _ => tt. - Definition OCaml_open_out : string -> out_channel := fun _ => tt. - Definition OCaml_close_in : in_channel -> unit := fun _ => tt. - Definition OCaml_close_out : out_channel -> unit := fun _ => tt. + Definition open_in : string -> in_channel := fun _ => tt. + Definition open_out : string -> out_channel := fun _ => tt. + Definition close_in : in_channel -> unit := fun _ => tt. + Definition close_out : out_channel -> unit := fun _ => tt. Definition read_channel_rev : in_channel -> list string := fun _ => nil. End OCamlPrimitives. Extract Inductive int - => "Int.t" [ "0" "Pervasives.succ" ] - "(fun fO fS n -> if n=0 then fO () else fS (n-1))". -(* We cannot inline these constants due to COQBUG(https://github.com/coq/coq/issues/16169) *) -Extract (*Inlined*) Constant in_channel => "in_channel". -Extract (*Inlined*) Constant out_channel => "out_channel". +=> int [ "0" "Pervasives.succ" ] + "(fun fO fS n -> if n=0 then fO () else fS (n-1))". +Extract Inlined Constant in_channel => "in_channel". +Extract Inlined Constant out_channel => "out_channel". Extract Constant fprintf_char => "fun chan c -> Printf.fprintf chan ""%c%!"" c". Extract Constant flush => "fun chan -> Printf.fprintf chan ""%!""". -Extract (*Inlined*) Constant stdin => "stdin". -Extract (*Inlined*) Constant stdout => "stdout". -Extract (*Inlined*) Constant string => "string". -Extract (*Inlined*) Constant string_length => "String.length". -Extract (*Inlined*) Constant string_get => "String.get". +Extract Inlined Constant stdin => "stdin". +Extract Inlined Constant stdout => "stdout". +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 Inlined Constant string_init => "String.init". Extract Constant raise_Failure => "fun x -> raise (Failure x)". -Extract (*Inlined*) Constant open_in => "open_in". -Extract (*Inlined*) Constant open_out => "open_out". -Extract (*Inlined*) Constant close_in => "close_in". -Extract (*Inlined*) Constant close_out => "close_out". +Extract Inlined Constant open_in => "open_in". +Extract Inlined Constant open_out => "open_out". +Extract Inlined Constant close_in => "close_in". +Extract Inlined Constant close_out => "close_out". Extract Constant read_channel_rev => "fun chan -> let lines = ref [] in