From 9e2a04f2b6880d930a0aff3a5d1728458860b3d3 Mon Sep 17 00:00:00 2001 From: Edward Pierzchalski Date: Fri, 1 Mar 2019 15:49:53 +1100 Subject: [PATCH] lib: add ML utilties 'bucket' file. The SML standard library is pretty bare-bones compared to that of other functional languages, so in a large enough SML project you end up with a bunch of reimplementations of basic combinators scattered all over the place. We'd be able to collect them if we had somewhere to collect them, so here it is. --- lib/ROOT | 1 + lib/ml-helpers/List.ML | 39 ++++++++++++++++++++++++ lib/ml-helpers/MLUtils.thy | 39 ++++++++++++++++++++++++ lib/ml-helpers/Method.ML | 28 +++++++++++++++++ lib/ml-helpers/String.ML | 62 ++++++++++++++++++++++++++++++++++++++ 5 files changed, 169 insertions(+) create mode 100644 lib/ml-helpers/List.ML create mode 100644 lib/ml-helpers/MLUtils.thy create mode 100644 lib/ml-helpers/Method.ML create mode 100644 lib/ml-helpers/String.ML diff --git a/lib/ROOT b/lib/ROOT index 7b8cc66c7..4dfffc712 100644 --- a/lib/ROOT +++ b/lib/ROOT @@ -52,6 +52,7 @@ session Lib (lib) = Word_Lib + HaskellLemmaBucket "ml-helpers/TermPatternAntiquote" "ml-helpers/TacticAntiquotation" + "ml-helpers/MLUtils" "subgoal_focus/Subgoal_Methods" Insulin ExtraCorres diff --git a/lib/ml-helpers/List.ML b/lib/ml-helpers/List.ML new file mode 100644 index 000000000..5c0f2d86a --- /dev/null +++ b/lib/ml-helpers/List.ML @@ -0,0 +1,39 @@ +(* + * Copyright 2019, Data61 + * Commonwealth Scientific and Industrial Research Organisation (CSIRO) + * ABN 41 687 119 230. + + * This software may be distributed and modified according to the terms of + * the BSD 2-Clause license. Note that NO WARRANTY is provided. + * See "LICENSE_BSD2.txt" for details. + + * @TAG(DATA61_BSD) + *) + +signature LIST = +sig + include LIST + + (* + `map_find_first f xs` applies `f` to each element of `xs`, returning + the first result that is `SOME _`, or `NONE` otherwise. For example: + + `map_find_first (try hd) [[], [1], [2]] = SOME 1` + + `map_find_first (try hd) [[], [], []] = NONE` + *) + val map_find_first: ('a -> 'b option) -> 'a list -> 'b option; +end + +structure List: LIST = +struct +open List + +fun map_find_first (f: 'a -> 'b option) (xs: 'a list): 'b option = + case xs of + [] => NONE + | x :: xs' => + (case f x of + SOME x' => SOME x' + | NONE => map_find_first f xs') +end diff --git a/lib/ml-helpers/MLUtils.thy b/lib/ml-helpers/MLUtils.thy new file mode 100644 index 000000000..78e5c91a1 --- /dev/null +++ b/lib/ml-helpers/MLUtils.thy @@ -0,0 +1,39 @@ +(* + * Copyright 2019, Data61 + * Commonwealth Scientific and Industrial Research Organisation (CSIRO) + * ABN 41 687 119 230. + + * This software may be distributed and modified according to the terms of + * the BSD 2-Clause license. Note that NO WARRANTY is provided. + * See "LICENSE_BSD2.txt" for details. + + * @TAG(DATA61_BSD) + *) + +\\ + MLUtils is a collection of 'basic' ML utilities (kind of like @{file + "~~/src/Pure/library.ML"}, but maintained by Trustworthy Systems). If you + find yourself implementing: + - A simple data-structure-shuffling task, + - Something that shows up in the standard library of other functional + languages, or + - Something that's "missing" from the general pattern of an Isabelle ML + library, + consider adding it here. + + When appropriate, you should consider *extending* an existing signature, + rather than creating a new one: `String.whatever` is more meaningful than + `TSStringLib.whatever`, and it doesn't damage the bindings to the "original" + signature in any way. Look at `String.ML` in this directory for an example. + + Some structures (like `Method`) can't be overridden this way. In these cases + name the new structure with a `Utils` suffix. +\ + +theory MLUtils +imports Main +begin +ML_file "String.ML" +ML_file "List.ML" +ML_file "Method.ML" +end diff --git a/lib/ml-helpers/Method.ML b/lib/ml-helpers/Method.ML new file mode 100644 index 000000000..7761f892c --- /dev/null +++ b/lib/ml-helpers/Method.ML @@ -0,0 +1,28 @@ +(* + * Copyright 2019, Data61 + * Commonwealth Scientific and Industrial Research Organisation (CSIRO) + * ABN 41 687 119 230. + + * This software may be distributed and modified according to the terms of + * the BSD 2-Clause license. Note that NO WARRANTY is provided. + * See "LICENSE_BSD2.txt" for details. + + * @TAG(DATA61_BSD) + *) + +signature METHOD_UTILS = +sig + include METHOD + + (* `then_all_new m1 m2` is equivalent to `(m1; m2)`. *) + val then_all_new: + (Proof.context -> method) * (Proof.context -> method) -> Proof.context -> method; +end + +structure MethodUtils: METHOD_UTILS = +struct +open Method + +fun then_all_new (m1, m2) = + Combinator (no_combinator_info, Then_All_New, [Basic m1, Basic m2]) |> evaluate +end diff --git a/lib/ml-helpers/String.ML b/lib/ml-helpers/String.ML new file mode 100644 index 000000000..bd37ddd15 --- /dev/null +++ b/lib/ml-helpers/String.ML @@ -0,0 +1,62 @@ +(* + * @TAG(OTHER_BSD) + *) +(* + * Copyright 2019, Data61 + * Commonwealth Scientific and Industrial Research Organisation (CSIRO) + * ABN 41 687 119 230. + + * This software may be distributed and modified according to the terms of + * the BSD 2-Clause license. Note that NO WARRANTY is provided. + * See "LICENSE_BSD2.txt" for details. + + * @TAG(DATA61_BSD) + *) +(* + * Includes code under BSD license, copyright 2001 John Hurd. + *) + +signature STRING = +sig + include STRING + + (* + `split sep s` returns the list of substrings of `s` that are + separated by `sep`. For example: + + `split ":" "hello:world" = ["hello", "world"]` + `split "foo" "barbaz" = ["barbaz"]` + *) + val split: string -> string -> string list +end + +structure String: STRING = +struct +open String + +\\ + Copied from @{file "~~/src/Tools/Metis/src/Useful.sml"}. +\ +local + fun match [] l = SOME l + | match _ [] = NONE + | match (x :: xs) (y :: ys) = if x = y then match xs ys else NONE; + + fun stringify acc [] = acc + | stringify acc (h :: t) = stringify (String.implode h :: acc) t; +in + fun split (sep: string) (s: string) = + let + val pat = String.explode sep + + fun div1 prev recent [] = stringify [] (List.rev recent :: prev) + | div1 prev recent (l as h :: t) = + case match pat l of + NONE => div1 prev (h :: recent) t + | SOME rest => div1 (List.rev recent :: prev) [] rest + in + div1 [] [] (String.explode s) + end; +end; + +end;