From 963a070d153f7b8e20176340f65b278d8e1f3965 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 7 Apr 2016 15:43:53 +0200
Subject: [PATCH] Function to break a string up into words.
---
theories/strings.v | 16 +++++++++++++++-
1 file changed, 15 insertions(+), 1 deletion(-)
diff --git a/theories/strings.v b/theories/strings.v
index 355e966a..31334218 100644
--- a/theories/strings.v
+++ b/theories/strings.v
@@ -25,6 +25,21 @@ Fixpoint string_rev_app (s1 s2 : string) : string :=
end.
Definition string_rev (s : string) : string := string_rev_app s "".
+(* Break a string up into lists of words, delimited by white space *)
+Fixpoint words_go (cur : option string) (s : string) : list string :=
+ match s with
+ | "" => option_list (string_rev <$> cur)
+ | String " " s => option_list (string_rev <$> cur) ++ words_go None s
+ | String a s => words_go (Some (default (String a "") cur (String a))) s
+ end.
+Definition words : string → list string := words_go None.
+
+Ltac words s :=
+ match type of s with
+ | list string => s
+ | string => eval vm_compute in (words s)
+ end.
+
(** * Encoding and decoding *)
(** In order to reuse or existing implementation of radix-2 search trees over
positive binary naturals [positive], we define an injection [string_to_pos]
@@ -71,4 +86,3 @@ Program Instance string_countable : Countable string := {|
encode := string_to_pos; decode p := Some (string_of_pos p)
|}.
Solve Obligations with naive_solver eauto using string_of_to_pos with f_equal.
-
--
GitLab