History log of /seL4-l4v-10.1.1/HOL4/tools/Holmake/parse_glob.sml
Revision Date Author Comments
# 6ea4d07b 27-Oct-2014 Michael Norrish <michael.norrish@nicta.com.au>

Adjust parse_glob to isolate "pure" characters.

Need this to isolate path components when doing matches like

*/*.c


# 8308dd1e 26-Oct-2014 Michael Norrish <michael.norrish@nicta.com.au>

Parse shell-style globs into regular expressions.

Features include meta-chars *, ? and [..], along with POSIX style
character classes, character class negation with ^ or !, character
ranges with hyphens, and quoting of meta-characters with \.

Doesn't handle bash's

[=c=]

and

[.c.]

syntax for character classes, which depend on collation notions that I
don't see a good way of emulating.

Character classes are complicated, but it does handle things like

[[:digit]ade-i]

which would match any of

0123456789adefghi

Note also that every possible string really does correspond to a
regular expression.

With test-cases. Assuming that you are in tools/Holmake, run

poly < parse_retest.ML