From ecfb73d655601e9aed736b0083a6f6b4682a2083 Mon Sep 17 00:00:00 2001 From: Paul Steckler 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 From 79da97a3e02a079e3d91f04fd012886c57d4c1e8 Mon Sep 17 00:00:00 2001 From: Paul Steckler Date: Wed, 22 Nov 2017 14:48:04 -0500 Subject: allow whitespace around infix op --- plugins/extraction/ocaml.ml | 6 ++++-- test-suite/output/Extraction_infix.out | 4 ++++ test-suite/output/Extraction_infix.v | 5 +++++ 3 files changed, 13 insertions(+), 2 deletions(-) diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml index eea5968ce..fb8dfb459 100644 --- a/plugins/extraction/ocaml.ml +++ b/plugins/extraction/ocaml.ml @@ -122,11 +122,13 @@ let is_infix r = len >= 3 && (* parenthesized *) (s.[0] == '(' && s.[len-1] == ')' && + let inparens = String.trim (String.sub s 1 (len - 2)) in + let inparens_len = String.length inparens in (* either, begins with infix symbol, any remainder is all operator chars *) - (List.mem s.[1] infix_symbols && substring_all_opchars s 2 (len-1)) + (List.mem inparens.[0] infix_symbols && substring_all_opchars inparens 1 inparens_len) || (* or, starts with #, at least one more char, all are operator chars *) - (s.[1] == '#' && len >= 4 && substring_all_opchars s 2 (len-1)))) + (inparens.[0] == '#' && inparens_len >= 2 && substring_all_opchars inparens 1 inparens_len))) 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 index 35ded8013..29d50775a 100644 --- a/test-suite/output/Extraction_infix.out +++ b/test-suite/output/Extraction_infix.out @@ -14,3 +14,7 @@ let test = 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 index bc0ddb3e1..fe5926a36 100644 --- a/test-suite/output/Extraction_infix.v +++ b/test-suite/output/Extraction_infix.v @@ -19,3 +19,8 @@ Extraction test. Extract Inductive I => "foo" [ "(@?:::)" ]. Extraction test. + +(* allow whitespace around infix operator *) + +Extract Inductive I => "foo" [ "( @?::: )" ]. +Extraction test. -- cgit v1.2.3 From f228c2eb94346fb3b538d63d95fdd8ab2c0f8795 Mon Sep 17 00:00:00 2001 From: Paul Steckler Date: Mon, 27 Nov 2017 15:05:14 -0500 Subject: allow :: and , as infix ops --- plugins/extraction/ocaml.ml | 24 +++++++++++++++--------- 1 file changed, 15 insertions(+), 9 deletions(-) diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml index fb8dfb459..5d0f9c167 100644 --- a/plugins/extraction/ocaml.ml +++ b/plugins/extraction/ocaml.ml @@ -107,6 +107,11 @@ let infix_symbols = let operator_chars = [ '!' ; '$' ; '%' ; '&' ; '*' ; '+' ; '-' ; '.' ; '/' ; ':' ; '<' ; '=' ; '>' ; '?' ; '@' ; '^' ; '|' ; '~' ] +(* infix ops in OCaml, but disallowed by preceding grammar *) + +let builtin_infixes = + [ "::" ; "," ] + let substring_all_opchars s start stop = let rec check_char i = if i >= stop then true @@ -120,15 +125,16 @@ let is_infix r = (let s = find_custom r in let len = String.length s in len >= 3 && - (* parenthesized *) - (s.[0] == '(' && s.[len-1] == ')' && - let inparens = String.trim (String.sub s 1 (len - 2)) in - let inparens_len = String.length inparens in - (* either, begins with infix symbol, any remainder is all operator chars *) - (List.mem inparens.[0] infix_symbols && substring_all_opchars inparens 1 inparens_len) - || - (* or, starts with #, at least one more char, all are operator chars *) - (inparens.[0] == '#' && inparens_len >= 2 && substring_all_opchars inparens 1 inparens_len))) + (* parenthesized *) + (s.[0] == '(' && s.[len-1] == ')' && + let inparens = String.trim (String.sub s 1 (len - 2)) in + let inparens_len = String.length inparens in + (* either, begins with infix symbol, any remainder is all operator chars *) + (List.mem inparens.[0] infix_symbols && substring_all_opchars inparens 1 inparens_len) || + (* or, starts with #, at least one more char, all are operator chars *) + (inparens.[0] == '#' && inparens_len >= 2 && substring_all_opchars inparens 1 inparens_len) || + (* or, is an OCaml built-in infix *) + (List.mem inparens builtin_infixes))) let get_infix r = let s = find_custom r in -- cgit v1.2.3 From 6cb9ab00a62b87587b00147d4abd82e684220b03 Mon Sep 17 00:00:00 2001 From: Paul Steckler Date: Tue, 28 Nov 2017 15:45:42 -0500 Subject: use \ocaml macro in new text --- doc/refman/Extraction.tex | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/doc/refman/Extraction.tex b/doc/refman/Extraction.tex index c263ecc48..79060e606 100644 --- a/doc/refman/Extraction.tex +++ b/doc/refman/Extraction.tex @@ -391,9 +391,9 @@ Extract Inductive bool => "bool" [ "true" "false" ]. Extract Inductive sumbool => "bool" [ "true" "false" ]. \end{coq_example} -\noindent When extracting to Ocaml, if an inductive 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, +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} -- cgit v1.2.3