Fix src/Experiments/Ed25519.v for Coq 8.4

Using very dubious module hackery.

2 files changed, 97 insertions, 45 deletions

diff --git a/src/Experiments/Ed25519.v b/src/Experiments/Ed25519.v
index dd6d4d4b8..0961aa77d 100644
--- a/src/Experiments/Ed25519.v
+++ b/src/Experiments/Ed25519.v
@@ -290,12 +290,12 @@ Axiom ERepGroup :
               (@ModularBaseSystem.decode GF25519.modulus GF25519.params25519 x)
               (@ModularBaseSystem.decode GF25519.modulus GF25519.params25519 y))) ErepAdd
         (@ExtendedCoordinates.Extended.zero GF25519.fe25519
-           (@ModularBaseSystem.eq GF25519.modulus GF25519.params25519) GF25519.zero_ GF25519.one_ 
+           (@ModularBaseSystem.eq GF25519.modulus GF25519.params25519) GF25519.zero_ GF25519.one_
            _ GF25519.add _ GF25519.mul _
            (@ModularBaseSystem.div GF25519.modulus GF25519.params25519) a d GF25519.field25519
            twedprm_ERep _)
         (@ExtendedCoordinates.Extended.opp GF25519.fe25519
-           (@ModularBaseSystem.eq GF25519.modulus GF25519.params25519) GF25519.zero_ GF25519.one_ 
+           (@ModularBaseSystem.eq GF25519.modulus GF25519.params25519) GF25519.zero_ GF25519.one_
            _ GF25519.add _ GF25519.mul _
            (@ModularBaseSystem.div GF25519.modulus GF25519.params25519) a d GF25519.field25519
           twedprm_ERep _).
@@ -580,49 +580,7 @@ Extract Inductive unit => "()" ["()"].
 
 (** nat *)
 
-Extract Inductive nat => "Prelude.Integer" [ "0" "Prelude.succ" ]
-  "(\fO fS n -> {- match_on_nat -} if n Prelude.== 0 then fO () else fS (n Prelude.- 1))".
-
-Extract Inlined Constant Nat.add => "(Prelude.+)".
-Extract Inlined Constant Nat.mul => "(Prelude.*)".
-Extract Inlined Constant Nat.pow => "(Prelude.^)".
-Extract Inlined Constant Nat.max => "Prelude.max".
-Extract Inlined Constant Nat.min => "Prelude.min".
-Extract Inlined Constant Nat.gcd => "Prelude.gcd".
-Extract Inlined Constant Nat.lcm => "Prelude.lcm".
-Extract Inlined Constant Nat.land => "(Data.Bits..&.)".
-Extract Inlined Constant Init.Nat.add => "(Prelude.+)".
-Extract Inlined Constant Init.Nat.mul => "(Prelude.*)".
-Extract Inlined Constant Init.Nat.max => "Prelude.max".
-Extract Inlined Constant Init.Nat.min => "Prelude.min".
-Extract Inlined Constant PeanoNat.Nat.add => "(Prelude.+)".
-Extract Inlined Constant PeanoNat.Nat.mul => "(Prelude.*)".
-Extract Inlined Constant PeanoNat.Nat.max => "Prelude.max".
-Extract Inlined Constant PeanoNat.Nat.min => "Prelude.min".
-Extract Inlined Constant Nat.compare => "Prelude.compare".
-Extract Inlined Constant PeanoNat.Nat.compare => "Prelude.compare".
-Extract Inlined Constant nat_compare_alt => "Prelude.compare".
-Extract Inlined Constant Nat.ltb => "(Prelude.<)".
-Extract Inlined Constant Compare_dec.lt_dec => "(Prelude.<)".
-Extract Inlined Constant Nat.leb => "(Prelude.<=)".
-Extract Inlined Constant Compare_dec.leb => "(Prelude.<=)".
-Extract Inlined Constant Compare_dec.le_lt_dec => "(Prelude.<=)".
-Extract Inlined Constant EqNat.beq_nat => "(Prelude.==)".
-Extract Inlined Constant Nat.eqb => "(Prelude.==)".
-Extract Inlined Constant EqNat.eq_nat_decide => "(Prelude.==)".
-Extract Inlined Constant Peano_dec.eq_nat_dec => "(Prelude.==)".
-Extract Inlined Constant Nat.odd => "Prelude.odd".
-Extract Inlined Constant Nat.even => "Prelude.even".
-
-Extract Constant Nat.pred => "(\n -> Prelude.max 0 (Prelude.pred n))".
-Extract Constant Nat.sub => "(\n m -> Prelude.max 0 (n Prelude.- m))".
-Extract Constant Init.Nat.pred => "(\n -> Prelude.max 0 (Prelude.pred n))".
-Extract Constant Init.Nat.sub => "(\n m -> Prelude.max 0 (n Prelude.- m))".
-
-Extract Constant Nat.div => "(\n m -> if m Prelude.== 0 then 0 else Prelude.div n m)".
-Extract Constant Nat.modulo => "(\n m -> if m Prelude.== 0 then 0 else Prelude.mod n m)".
-Extract Constant Init.Nat.div => "(\n m -> if m Prelude.== 0 then 0 else Prelude.div n m)".
-Extract Constant Init.Nat.modulo => "(\n m -> if m Prelude.== 0 then 0 else Prelude.mod n m)".
+Require Import Crypto.Experiments.ExtrHaskellNats.
 
 (** positive *)
 Require Import BinPos.
diff --git a/src/Experiments/ExtrHaskellNats.v b/src/Experiments/ExtrHaskellNats.v
new file mode 100644
index 000000000..ef9fd06d9
--- /dev/null
+++ b/src/Experiments/ExtrHaskellNats.v
@@ -0,0 +1,94 @@
+(** * Extraction Directives for [nat] in Haskell *)
+(** [nat] is really complicated, so we jump through many hoops to get
+    code that compiles in 8.4 and 8.5 at the same time. *)
+Require Coq.Numbers.Natural.Peano.NPeano.
+Require Coq.Arith.Compare_dec Coq.Arith.EqNat Coq.Arith.Peano_dec.
+
+Extract Inductive nat => "Prelude.Integer" [ "0" "Prelude.succ" ]
+  "(\fO fS n -> {- match_on_nat -} if n Prelude.== 0 then fO () else fS (n Prelude.- 1))".
+
+
+(** We rely on the fact that Coq forbids masking absolute names.  Hopefully we can drop support for 8.4 before this is changed. *)
+Module Coq.
+  Module M. Export NPeano.Nat. End M.
+  Module Init.
+    Module Nat.
+      Export M.
+    End Nat.
+  End Init.
+  Module Numbers.
+    Module Natural.
+      Module Peano.
+        Module NPeano.
+          Module Nat.
+            Export M.
+          End Nat.
+        End NPeano.
+      End Peano.
+    End Natural.
+  End Numbers.
+  Module Arith.
+    Module PeanoNat.
+      Module Nat.
+        Export M.
+      End Nat.
+    End PeanoNat.
+  End Arith.
+End Coq.
+
+Module Export Import_NPeano_Nat.
+  Import Coq.Numbers.Natural.Peano.NPeano.Nat.
+
+  Extract Inlined Constant add => "(Prelude.+)".
+  Extract Inlined Constant mul => "(Prelude.*)".
+  Extract Inlined Constant pow => "(Prelude.^)".
+  Extract Inlined Constant max => "Prelude.max".
+  Extract Inlined Constant min => "Prelude.min".
+  Extract Inlined Constant gcd => "Prelude.gcd".
+  Extract Inlined Constant lcm => "Prelude.lcm".
+  Extract Inlined Constant land => "(Data.Bits..&.)".
+  Extract Inlined Constant compare => "Prelude.compare".
+  Extract Inlined Constant ltb => "(Prelude.<)".
+  Extract Inlined Constant leb => "(Prelude.<=)".
+  Extract Inlined Constant eqb => "(Prelude.==)".
+  Extract Inlined Constant odd => "Prelude.odd".
+  Extract Inlined Constant even => "Prelude.even".
+  Extract Constant pred => "(\n -> Prelude.max 0 (Prelude.pred n))".
+  Extract Constant sub => "(\n m -> Prelude.max 0 (n Prelude.- m))".
+  Extract Constant div => "(\n m -> if m Prelude.== 0 then 0 else Prelude.div n m)".
+  Extract Constant modulo => "(\n m -> if m Prelude.== 0 then 0 else Prelude.mod n m)".
+End Import_NPeano_Nat.
+
+
+Module Export Import_Init_Nat.
+  Import Coq.Init.Nat.
+
+  Extract Inlined Constant add => "(Prelude.+)".
+  Extract Inlined Constant mul => "(Prelude.*)".
+  Extract Inlined Constant max => "Prelude.max".
+  Extract Inlined Constant min => "Prelude.min".
+  Extract Constant pred => "(\n -> Prelude.max 0 (Prelude.pred n))".
+  Extract Constant sub => "(\n m -> Prelude.max 0 (n Prelude.- m))".
+
+  Extract Constant div => "(\n m -> if m Prelude.== 0 then 0 else Prelude.div n m)".
+  Extract Constant modulo => "(\n m -> if m Prelude.== 0 then 0 else Prelude.mod n m)".
+End Import_Init_Nat.
+
+
+Module Export Import_PeanoNat_Nat.
+  Import Coq.Arith.PeanoNat.Nat.
+
+  Extract Inlined Constant add => "(Prelude.+)".
+  Extract Inlined Constant mul => "(Prelude.*)".
+  Extract Inlined Constant max => "Prelude.max".
+  Extract Inlined Constant min => "Prelude.min".
+  Extract Inlined Constant compare => "Prelude.compare".
+End Import_PeanoNat_Nat.
+
+Extract Inlined Constant Compare_dec.nat_compare_alt => "Prelude.compare".
+Extract Inlined Constant Compare_dec.lt_dec => "(Prelude.<)".
+Extract Inlined Constant Compare_dec.leb => "(Prelude.<=)".
+Extract Inlined Constant Compare_dec.le_lt_dec => "(Prelude.<=)".
+Extract Inlined Constant EqNat.beq_nat => "(Prelude.==)".
+Extract Inlined Constant EqNat.eq_nat_decide => "(Prelude.==)".
+Extract Inlined Constant Peano_dec.eq_nat_dec => "(Prelude.==)".