Revert "Generate .mli files: { => Recursive} Extraction (#1292)"

.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

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) $< > [email protected]
+	$(HIDE)cat [email protected] | tr -d '\r' > $@ && rm -f [email protected]
 
 $(STANDALONE_HASKELL:%=src/ExtractionHaskell/%.hs) : %.hs : %.v src/haskell.sed
 	$(SHOW)'COQC $< > $@'
 	$(HIDE)$(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) $< > [email protected]
-	$(HIDE)cat [email protected] | tr -d '\r' | sed -f src/haskell.sed > $@ && rm [email protected]
+	$(HIDE)cat [email protected] | tr -d '\r' | sed -f src/haskell.sed > $@ && rm -f [email protected]
 
 # 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 $@'

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

src/Rewriter/PerfTesting/StandaloneOCamlMain.v

@@ -7,28 +7,25 @@ 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.
   Axiom printf_float : float -> unit.
 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".
 

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