From ecfb73d655601e9aed736b0083a6f6b4682a2083 Mon Sep 17 00:00:00 2001
From: Paul Steckler <psteck@mit.edu>
Date: Wed, 22 Nov 2017 12:33:02 -0500
Subject: use OCaml criteria for infix ops, #6212

---
 doc/refman/Extraction.tex              |  8 +++++---
 plugins/extraction/ocaml.ml            | 26 ++++++++++++++++++++++++--
 test-suite/output/Extraction_infix.out | 16 ++++++++++++++++
 test-suite/output/Extraction_infix.v   | 21 +++++++++++++++++++++
 4 files changed, 66 insertions(+), 5 deletions(-)
 create mode 100644 test-suite/output/Extraction_infix.out
 create mode 100644 test-suite/output/Extraction_infix.v

diff --git a/doc/refman/Extraction.tex b/doc/refman/Extraction.tex
index 83e866e9f..c263ecc48 100644
--- a/doc/refman/Extraction.tex
+++ b/doc/refman/Extraction.tex
@@ -391,9 +391,11 @@ Extract Inductive bool => "bool" [ "true" "false" ].
 Extract Inductive sumbool => "bool" [ "true" "false" ].
 \end{coq_example}
 
-\noindent If an inductive constructor or type has arity 2 and the corresponding 
-string is enclosed by parenthesis, then the rest of the string is used
-as infix constructor or type. 
+\noindent When extracting to Ocaml, if an inductive constructor or type
+has arity 2 and the corresponding string is enclosed by parentheses,
+and the string meets Ocaml's lexical criteria for an infix symbol,
+then the rest of the string is used as infix constructor or type.
+
 \begin{coq_example}
 Extract Inductive list => "list" [ "[]" "(::)" ].
 Extract Inductive prod => "(*)"  [ "(,)" ].
diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml
index 9cbc3fd71..eea5968ce 100644
--- a/plugins/extraction/ocaml.ml
+++ b/plugins/extraction/ocaml.ml
@@ -100,11 +100,33 @@ let pp_global k r = str (str_global k r)
 
 let pp_modname mp = str (Common.pp_module mp)
 
+(* grammar from OCaml 4.06 manual, "Prefix and infix symbols" *)
+
+let infix_symbols =
+  ['=' ; '<' ; '>' ; '@' ; '^' ; ';' ; '&' ; '+' ; '-' ; '*' ; '/' ; '$' ; '%' ]
+let operator_chars =
+  [ '!' ; '$' ; '%' ; '&' ; '*' ; '+' ; '-' ; '.' ; '/' ; ':' ; '<' ; '=' ; '>' ; '?' ; '@' ; '^' ; '|' ; '~' ]
+
+let substring_all_opchars s start stop =
+  let rec check_char i =
+    if i >= stop then true
+    else
+      List.mem s.[i] operator_chars && check_char (i+1)
+  in
+  check_char start
+
 let is_infix r =
   is_inline_custom r &&
   (let s = find_custom r in
-   let l = String.length s in
-   l >= 2 && s.[0] == '(' && s.[l-1] == ')')
+   let len = String.length s in
+   len >= 3 &&
+     (* parenthesized *)
+     (s.[0] == '(' && s.[len-1] == ')' &&
+        (* either, begins with infix symbol, any remainder is all operator chars *)
+        (List.mem s.[1] infix_symbols && substring_all_opchars s 2 (len-1))
+      ||
+        (* or, starts with #, at least one more char, all are operator chars *)
+        (s.[1] == '#' && len >= 4 && substring_all_opchars s 2 (len-1))))
 
 let get_infix r =
   let s = find_custom r in
diff --git a/test-suite/output/Extraction_infix.out b/test-suite/output/Extraction_infix.out
new file mode 100644
index 000000000..35ded8013
--- /dev/null
+++ b/test-suite/output/Extraction_infix.out
@@ -0,0 +1,16 @@
+(** val test : foo **)
+
+let test =
+  (fun (b, p) -> bar) (True, False)
+(** val test : foo **)
+
+let test =
+  True@@?False
+(** val test : foo **)
+
+let test =
+  True#^^False
+(** val test : foo **)
+
+let test =
+  True@?:::False
diff --git a/test-suite/output/Extraction_infix.v b/test-suite/output/Extraction_infix.v
new file mode 100644
index 000000000..bc0ddb3e1
--- /dev/null
+++ b/test-suite/output/Extraction_infix.v
@@ -0,0 +1,21 @@
+(* @herbelin's example for issue #6212 *)
+
+Require Import Extraction.
+Inductive I := C : bool -> bool -> I.
+Definition test := C true false.
+
+(* the parentheses around the function wrong signalled an infix operator *)
+
+Extract Inductive I => "foo" [ "(fun (b, p) -> bar)" ].
+Extraction test.
+
+(* some bonafide infix operators *)
+
+Extract Inductive I => "foo" [ "(@@?)" ].
+Extraction test.
+
+Extract Inductive I => "foo" [ "(#^^)" ].
+Extraction test.
+
+Extract Inductive I => "foo" [ "(@?:::)" ].
+Extraction test.
-- 
cgit v1.2.3