From fdfcadc111fb5618a8e4a769c50607dc920b7dec Mon Sep 17 00:00:00 2001
From: Pierre Roux
Date: Sat, 20 Oct 2018 23:43:07 +0200
Subject: Parsing primitive float constants

---
 Makefile.common                           |  1 +
 plugins/syntax/float_syntax.ml            | 50 +++++++++++++++++++++++++++++++
 plugins/syntax/float_syntax_plugin.mlpack |  1 +
 plugins/syntax/plugin_base.dune           |  7 +++++
 test-suite/primitive/float/syntax.v       | 13 ++++++++
 theories/Floats/PrimFloat.v               |  2 ++
 6 files changed, 74 insertions(+)
 create mode 100644 plugins/syntax/float_syntax.ml
 create mode 100644 plugins/syntax/float_syntax_plugin.mlpack
 create mode 100644 test-suite/primitive/float/syntax.v

diff --git a/Makefile.common b/Makefile.common
index 1ad255d156..e392e51153 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -149,6 +149,7 @@ RTAUTOCMO:=plugins/rtauto/rtauto_plugin.cmo
 SYNTAXCMO:=$(addprefix plugins/syntax/, \
         r_syntax_plugin.cmo \
 	int63_syntax_plugin.cmo \
+	float_syntax_plugin.cmo \
 	numeral_notation_plugin.cmo \
 	string_notation_plugin.cmo)
 DERIVECMO:=plugins/derive/derive_plugin.cmo
diff --git a/plugins/syntax/float_syntax.ml b/plugins/syntax/float_syntax.ml
new file mode 100644
index 0000000000..3c2e217d1c
--- /dev/null
+++ b/plugins/syntax/float_syntax.ml
@@ -0,0 +1,50 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Names
+open Glob_term
+
+(* Poor's man DECLARE PLUGIN *)
+let __coq_plugin_name = "float_syntax_plugin"
+let () = Mltop.add_known_module __coq_plugin_name
+
+(*** Constants for locating float constructors ***)
+
+let make_dir l = DirPath.make (List.rev_map Id.of_string l)
+let make_path dir id = Libnames.make_path (make_dir dir) (Id.of_string id)
+
+(*** Parsing for float in digital notation ***)
+
+let interp_float ?loc (sign,n) =
+  let sign = Constrexpr.(match sign with SPlus -> "" | SMinus -> "-") in
+  DAst.make ?loc (GFloat (Float64.of_string (sign ^ NumTok.to_string n)))
+
+(* Pretty printing is already handled in constrextern.ml *)
+
+let uninterp_float _ = None
+
+(* Actually declares the interpreter for float *)
+
+open Notation
+
+let at_declare_ml_module f x =
+  Mltop.declare_cache_obj (fun () -> f x) __coq_plugin_name
+
+let float_module = ["Coq"; "Floats"; "PrimFloat"]
+let float_path = make_path float_module "float"
+let float_scope = "float_scope"
+
+let _ =
+  register_rawnumeral_interpretation float_scope (interp_float,uninterp_float);
+  at_declare_ml_module enable_prim_token_interpretation
+    { pt_local = false;
+      pt_scope = float_scope;
+      pt_interp_info = Uid float_scope;
+      pt_required = (float_path,float_module);
+      pt_refs = [];
+      pt_in_match = false }
diff --git a/plugins/syntax/float_syntax_plugin.mlpack b/plugins/syntax/float_syntax_plugin.mlpack
new file mode 100644
index 0000000000..d69f49bcfe
--- /dev/null
+++ b/plugins/syntax/float_syntax_plugin.mlpack
@@ -0,0 +1 @@
+Float_syntax
diff --git a/plugins/syntax/plugin_base.dune b/plugins/syntax/plugin_base.dune
index 7a23581768..512752135d 100644
--- a/plugins/syntax/plugin_base.dune
+++ b/plugins/syntax/plugin_base.dune
@@ -25,3 +25,10 @@
  (synopsis "Coq syntax plugin: int63")
  (modules int63_syntax)
  (libraries coq.vernac))
+
+(library
+ (name float_syntax_plugin)
+ (public_name coq.plugins.float_syntax)
+ (synopsis "Coq syntax plugin: float")
+ (modules float_syntax)
+ (libraries coq.vernac))
diff --git a/test-suite/primitive/float/syntax.v b/test-suite/primitive/float/syntax.v
new file mode 100644
index 0000000000..cc0bbcf628
--- /dev/null
+++ b/test-suite/primitive/float/syntax.v
@@ -0,0 +1,13 @@
+Require Import Floats.
+
+Open Scope float_scope.
+
+Definition two := Eval compute in one + one.
+Definition half := Eval compute in one / two.
+
+Check (eq_refl : 1.5 = one + half).
+Check (eq_refl : 15e-1 = one + half).
+Check (eq_refl : 150e-2 = one + half).
+Check (eq_refl : 0.15e+1 = one + half).
+Check (eq_refl : 0.15e1 = one + half).
+Check (eq_refl : 0.0015e3 = one + half).
diff --git a/theories/Floats/PrimFloat.v b/theories/Floats/PrimFloat.v
index b84965a11a..c3c35486d9 100644
--- a/theories/Floats/PrimFloat.v
+++ b/theories/Floats/PrimFloat.v
@@ -11,6 +11,8 @@ Declare Scope float_scope.
 Delimit Scope float_scope with float.
 Bind Scope float_scope with float.
 
+Declare ML Module "float_syntax_plugin".
+
 Primitive opp := #float64_opp.
 Notation "- x" := (opp x) : float_scope.
 
-- 
cgit v1.2.3