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 --- plugins/extraction/ocaml.ml | 26 ++++++++++++++++++++++++-- 1 file changed, 24 insertions(+), 2 deletions(-) (limited to 'plugins/extraction') 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 -- 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(-) (limited to 'plugins/extraction') 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(-) (limited to 'plugins/extraction') 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