diff options
| author | Alasdair Armstrong | 2017-07-05 17:42:06 +0100 |
|---|---|---|
| committer | Alasdair Armstrong | 2017-07-05 17:42:06 +0100 |
| commit | cd3f299735d11241f064e9832c177830b78dcca4 (patch) | |
| tree | 68371a087d7700c3d63834c3cc39e1c3ff970fc3 | |
| parent | 5f46cb01ed07fbca390535440f77f1816cb61684 (diff) | |
Added split_on_char as a utility function in Util.ml, and replaced usage in sail.ml
Current REMS install script and Jenkins CI server is on an older ocaml
which doesn't have this function in String.
| -rw-r--r-- | src/sail.ml | 2 | ||||
| -rw-r--r-- | src/util.ml | 9 | ||||
| -rw-r--r-- | src/util.mli | 2 |
3 files changed, 11 insertions, 2 deletions
diff --git a/src/sail.ml b/src/sail.ml index 41c42fe4..d84144e1 100644 --- a/src/sail.ml +++ b/src/sail.ml @@ -89,7 +89,7 @@ let options = Arg.align ([ " (debug) skip constraint resolution in type-checking"); ( "-mono-split", Arg.String (fun s -> - let l = String.split_on_char ':' s in + let l = Util.split_on_char ':' s in match l with | [fname;line;var] -> opt_mono_split := ((fname,int_of_string line),var)::!opt_mono_split | _ -> raise (Arg.Bad (s ^ " not of form <filename>:<line>:<variable>"))), diff --git a/src/util.ml b/src/util.ml index bb277016..9b76c118 100644 --- a/src/util.ml +++ b/src/util.ml @@ -144,7 +144,14 @@ let rec compare_list f l1 l2 = compare_list f l1 l2 else c - + +let rec split_on_char sep str = + try + let sep_pos = String.index str sep in + String.sub str 0 sep_pos :: split_on_char sep (String.sub str (sep_pos + 1) (String.length str - (sep_pos + 1))) + with + | Not_found -> [str] + let map_changed_default d f l = let rec g = function | [] -> ([],false) diff --git a/src/util.mli b/src/util.mli index 496c63cf..099839bb 100644 --- a/src/util.mli +++ b/src/util.mli @@ -198,3 +198,5 @@ module ExtraSet : functor (S : Set.S) -> (*Formatting functions*) val string_of_list : string -> ('a -> string) -> 'a list -> string + +val split_on_char : char -> string -> string list |