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