<div>I agree we probably don't want to do fancy things that are only available the server. However, I think it's still possible to support nice behavior for alt just by postprocessing on the Ur/Web side.</div><div><br></div><div><div>Let's say "names" are capture groups from the library user's perspective and "indices" are capture groups from the FFI's perspective. Right now, each name corresponds to exactly one index. You could support alt by having each name correspond to multiple indices, each of which is matched at most once.</div></div><div><br></div><div>Concrete example: say you have (#X:a)(#Y:b)|(#X:c)(#Z:d)—that is, abusing notation somewhat, an expression that captures names either X and Y or X and Z. You could represent this using the record of index lists {X = [1,3], Y = [2], Z = [4]}. When you get the result list back from the FFI, you have to check groups 1 and 3 to see if X was matched. If you only ever concatenate index lists as part of alt, you ensure that you never have two non-null matches for the same name: given a match, in each name's index list, all but at most one of the indices is from an alt branch that wasn't taken.</div><div><br></div><div>You could take these ideas further to track statically when a group is guaranteed to be matched (like X above) or not (like Y or Z above). The easiest way is probably to have two record parameters for the type—one for guaranteed match names, another for optional match names. For example (leaving out folders and disjoitedness constraints):</div><div><br></div><div>star : r ::: Unit -> s ::: Unit -> t r s -> t [] (r + s)</div><div><br></div><div>plus : r ::: Unit -> s ::: Unit -> t r s -> t r s<br></div><div><br></div><div>capture : r ::: Unit -> s ::: Unit -> nm :: Name -> t r s -> t (r ++ [nm]) s.<br></div><div><br></div><div>The left record has the names of guaranteed matches, and the right record has the names of optional ones. You can see that plus keeps guaranteed matches guaranteed, star makes all of them optional. The most complicated type would, of course, be alt.</div><div><br></div><div>alt : r ::: Unit -> r1 ::: Unit -> r2 ::: Unit s1 ::: Unit -> s2 ::: Unit</div><div> -> t (r ++ r1) s1 -> t (r ++ r2) s2</div><div> -> t r (r1 ++ r2 ++ s1 ++ s2)</div><div><br></div><div>That is, the only groups that are guaranteed to be matched are those guaranteed in both of the branches; all others are optional.</div><div><br></div><div><br><div class="gmail_quote"><div>On Thu, Mar 9, 2017 at 09:17 Artyom Shalkhakov <<a href="mailto:artyom.shalkhakov@gmail.com">artyom.shalkhakov@gmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">2017-03-09 19:39 GMT+06:00 Ziv Scully <<a href="mailto:zivscully@gmail.com" class="gmail_msg" target="_blank">zivscully@gmail.com</a>>:<br class="gmail_msg">
> Looks good—glad it worked out!<br class="gmail_msg">
><br class="gmail_msg">
> My main question: what happens if the whole string is matched but a<br class="gmail_msg">
> particular subgroup isn't? This can happen with alt or star, for instance. I<br class="gmail_msg">
> couldn't tell from the types. I would expect a return type for match to be<br class="gmail_msg">
> something like `match r (option string)` instead of `option (match r<br class="gmail_msg">
> string)`. I don't know the underlying regex library, so perhaps there's a<br class="gmail_msg">
> good reason for this.<br class="gmail_msg">
<br class="gmail_msg">
I think a test is in order; I don't know what happens in that case (do<br class="gmail_msg">
you have an example handy?). From JS RegExp object documentation, it<br class="gmail_msg">
seems that subgroups are always present (but, indeed, the strings<br class="gmail_msg">
might be nulls or something else entirely, this is JS, after all).<br class="gmail_msg">
Good catch!<br class="gmail_msg">
<br class="gmail_msg">
><br class="gmail_msg">
> I also thought it may be useful if alt allowed the same group to be captured<br class="gmail_msg">
> on either side, but I realize that takes further fiddling with subgroup<br class="gmail_msg">
> indices and post-processing of the results (each group field name would map<br class="gmail_msg">
> to a list of indices instead of a single index), so it can wait for version<br class="gmail_msg">
> 2 :).<br class="gmail_msg">
><br class="gmail_msg">
<br class="gmail_msg">
I was a bit puzzled about the type you gave for [alt], it only dawned<br class="gmail_msg">
on me later what you meant with it. :-)<br class="gmail_msg">
<br class="gmail_msg">
I can see two questions here:<br class="gmail_msg">
<br class="gmail_msg">
1. say we have an expression like [a(b)*c], if matched against<br class="gmail_msg">
[abbbbbbc] in JS, it will only capture the *first* b -- I guess<br class="gmail_msg">
Boost.Regex which is used on the server behaves the same (Benjamin,<br class="gmail_msg">
could you help out on this?)<br class="gmail_msg">
<br class="gmail_msg">
2. say we have an expression like [(a)|(b)], in JS the groups will be<br class="gmail_msg">
1 and 2. PCRE and some other engines support a "group reset" feature,<br class="gmail_msg">
so that we can indeed capture both alternatives with one group. This<br class="gmail_msg">
is unsupported in JS, so I decided to leave it as is, for now.<br class="gmail_msg">
<br class="gmail_msg">
><br class="gmail_msg">
> On Tue, Mar 7, 2017 at 02:11 Artyom Shalkhakov <<a href="mailto:artyom.shalkhakov@gmail.com" class="gmail_msg" target="_blank">artyom.shalkhakov@gmail.com</a>><br class="gmail_msg">
> wrote:<br class="gmail_msg">
>><br class="gmail_msg">
>> Hello Ziv,<br class="gmail_msg">
>><br class="gmail_msg">
>> I've implemented your idea [1], and it works. Looking for feedback.<br class="gmail_msg">
>><br class="gmail_msg">
>> 2017-02-20 15:48 GMT+06:00 Ziv Scully <<a href="mailto:zivscully@gmail.com" class="gmail_msg" target="_blank">zivscully@gmail.com</a>>:<br class="gmail_msg">
>> > By parametrizing over a type-level record, you can encode the names of<br class="gmail_msg">
>> > matched subgroups in the type of the regular expression. The interface<br class="gmail_msg">
>> > probably looks something like:<br class="gmail_msg">
>> ><br class="gmail_msg">
>> > (* Abstract type of uncompiled regular expressions. *)<br class="gmail_msg">
>> > con t :: {Unit} (* names of captured subgroups *) -> Type<br class="gmail_msg">
>> ><br class="gmail_msg">
>> > val literal :<br class="gmail_msg">
>> > string -> t []<br class="gmail_msg">
>> > val any : t []<br class="gmail_msg">
>> > val concat : r1 ::: {Unit} -> r2 ::: {Unit} -> [r1 ~ r2] =><br class="gmail_msg">
>> > t r1 -> t r2 -> t (r1 ++ r2)<br class="gmail_msg">
>> > val star : r ::: {Unit} -><br class="gmail_msg">
>> > t r -> t r<br class="gmail_msg">
>> > val alt : r ::: {Unit} -> s1 ::: {Unit} -> s2 ::: {Unit} -> [r ~ s1] =><br class="gmail_msg">
>> > [r ~<br class="gmail_msg">
>> > s2] => [s1 ~ s2] =><br class="gmail_msg">
>> > t (r ++ s1) -> t (r ++ s2) -> t (r ++ s1 ++ s2)<br class="gmail_msg">
>> > val capture : r ::: {Unit} -><br class="gmail_msg">
>> > nm :: Name -> [r ~ [nm]] => t r -> t (r ++ [nm])<br class="gmail_msg">
>> ><br class="gmail_msg">
>> > (* Abstract type of compiled regular expressions *)<br class="gmail_msg">
>> > con compiled :: {Unit} -> Type<br class="gmail_msg">
>> ><br class="gmail_msg">
>> > val compile : r ::: {Unit} -><br class="gmail_msg">
>> > t r -> compiled r<br class="gmail_msg">
>> ><br class="gmail_msg">
>> > Obviously this probably won't exactly work. For instance, if the<br class="gmail_msg">
>> > underlying<br class="gmail_msg">
>> > library requires explicit names for captured groups, you'll need<br class="gmail_msg">
>> > something<br class="gmail_msg">
>> > more like<br class="gmail_msg">
>> ><br class="gmail_msg">
>> > val capture : r ::: {Unit} -> nm :: Name -> [r ~ [nm]] =><br class="gmail_msg">
>> > {nm : string} -> t r -> t (r ++ [nm])<br class="gmail_msg">
>> ><br class="gmail_msg">
>> > because there's no way to extract a string from a type-level Name. In<br class="gmail_msg">
>> > fact,<br class="gmail_msg">
>> > this way has another benefit: the internal representation of the type<br class="gmail_msg">
>> > can<br class="gmail_msg">
>> > just be a string! All the tracking of subgroups can happen at the type<br class="gmail_msg">
>> > level. You may not even need compile.<br class="gmail_msg">
>> ><br class="gmail_msg">
>> > This interface assumes each subgroup may appear 0 or 1 times. You could<br class="gmail_msg">
>> > maybe keep track of the number of matches more precisely by using {Type}<br class="gmail_msg">
>> > instead of {Unit} and using a type class to implement type-level<br class="gmail_msg">
>> > functions.<br class="gmail_msg">
>> ><br class="gmail_msg">
>> > con t : {Type} (* maps names of captured subgroups to type-level<br class="gmail_msg">
>> > representation of number of matched fields *) -> Type<br class="gmail_msg">
>> ><br class="gmail_msg">
>> > type one<br class="gmail_msg">
>> > type oneOrNone<br class="gmail_msg">
>> ><br class="gmail_msg">
>> > class meet : Type -> Type -> Type<br class="gmail_msg">
>> > val meet_one_oneOrNone : weaken one oneOrNone oneOrNone<br class="gmail_msg">
>> > val meet_oneOrNone_one : weaken oneOrNone one oneOrNone<br class="gmail_msg">
>> > val meet_oneOrNone_oneOrNone : weaken oneOrNone oneOrNone oneOrNone<br class="gmail_msg">
>> ><br class="gmail_msg">
>> > This makes the types more complicated, but I suspect (though I don't<br class="gmail_msg">
>> > know<br class="gmail_msg">
>> > for sure) that Ur/Web will be able to infer the extra stuff in any<br class="gmail_msg">
>> > concrete<br class="gmail_msg">
>> > (that is, monomorphic) use, so the user code will still look pretty.<br class="gmail_msg">
>> > Here's<br class="gmail_msg">
>> > how some of the functions look with this. The place weaken gets used is<br class="gmail_msg">
>> > alt.<br class="gmail_msg">
>> ><br class="gmail_msg">
>> > val star : r ::: {Type} -><br class="gmail_msg">
>> > t r -> t (map (fn _ => oneOrNo) r)<br class="gmail_msg">
>> ><br class="gmail_msg">
>> > val alt : r ::: {Type * Type * Type} -> s1 ::: {Type} -> s2 ::: {Type}<br class="gmail_msg">
>> > -><br class="gmail_msg">
>> > [map fst3 r ~ s1] => [map snd3 r ~ s2] => [s1 ~ s2] =><br class="gmail_msg">
>> > $(map (fn (t1, t2, t3) => weaken t1 t2 t3) r)<br class="gmail_msg">
>> > t (map fst3 r ++ s1) -> t (map snd3 r ++ s2)<br class="gmail_msg">
>> > -> t (map thd3 r ++ map (fn _ => oneOrNo) (s1 ++ s2))<br class="gmail_msg">
>> ><br class="gmail_msg">
>> > You could extend the same sort of idea to types like oneOrMore and<br class="gmail_msg">
>> > noneOrMore—useful if the underlying library can return a list of matches<br class="gmail_msg">
>> > inside a + or *—by adding more cases to weaken.<br class="gmail_msg">
>> ><br class="gmail_msg">
>> > Here's a Haskell library that takes basically this approach:<br class="gmail_msg">
>> > <a href="https://github.com/sweirich/dth/tree/master/popl17/src" rel="noreferrer" class="gmail_msg" target="_blank">https://github.com/sweirich/dth/tree/master/popl17/src</a><br class="gmail_msg">
>> ><br class="gmail_msg">
>> > Hope this helps!<br class="gmail_msg">
>> > Ziv<br class="gmail_msg">
>> ><br class="gmail_msg">
>> ><br class="gmail_msg">
>> > On Mon, Feb 20, 2017 at 12:00 AM, Artyom Shalkhakov<br class="gmail_msg">
>> > <<a href="mailto:artyom.shalkhakov@gmail.com" class="gmail_msg" target="_blank">artyom.shalkhakov@gmail.com</a>> wrote:<br class="gmail_msg">
>> >><br class="gmail_msg">
>> >> 2017-02-20 10:47 GMT+06:00 <<a href="mailto:fold@tuta.io" class="gmail_msg" target="_blank">fold@tuta.io</a>>:<br class="gmail_msg">
>> >>><br class="gmail_msg">
>> >>> Maybe just define another attribute in basis.urs?<br class="gmail_msg">
>> >>><br class="gmail_msg">
>> >>> It would be much interesting to define a DSEL though. I have not seen<br class="gmail_msg">
>> >>> any<br class="gmail_msg">
>> >>> attempts to create a DSEL for regular expressions.<br class="gmail_msg">
>> >>><br class="gmail_msg">
>> >><br class="gmail_msg">
>> >> Indeed! And it seems like it would be a nice exercise as well having<br class="gmail_msg">
>> >> some<br class="gmail_msg">
>> >> practical uses to it.<br class="gmail_msg">
>> >><br class="gmail_msg">
>> >> I envision something along the lines of:<br class="gmail_msg">
>> >><br class="gmail_msg">
>> >> datatype RegExp = ... (* constructors *)<br class="gmail_msg">
>> >><br class="gmail_msg">
>> >> type t (* abstract, not exported outside the module *)<br class="gmail_msg">
>> >> val compile : RegExp -> t (* the trusted function *)<br class="gmail_msg">
>> >> val matches : string -> t -> bool (* check if passed-in string matches<br class="gmail_msg">
>> >> the<br class="gmail_msg">
>> >> expression *)<br class="gmail_msg">
>> >><br class="gmail_msg">
>> >> And the implementation might use something unsafe (like a string, or an<br class="gmail_msg">
>> >> actual regexp object in JS). Then we could offload the interpretation<br class="gmail_msg">
>> >> of<br class="gmail_msg">
>> >> regexps to an off-the-shelf library. The [compile] function would print<br class="gmail_msg">
>> >> and<br class="gmail_msg">
>> >> escape the AST to a regexp string, and the Ur/Web compiler might<br class="gmail_msg">
>> >> actually<br class="gmail_msg">
>> >> optimize all of this away.<br class="gmail_msg">
>> >><br class="gmail_msg">
>> >> If we are to take care of matching subgroups, that would require a more<br class="gmail_msg">
>> >> complicated type. I guess that should be doable as well, but I don't<br class="gmail_msg">
>> >> see<br class="gmail_msg">
>> >> immediately how to handle this.<br class="gmail_msg">
>> >><br class="gmail_msg">
>> >>><br class="gmail_msg">
>> >>><br class="gmail_msg">
>> >>><br class="gmail_msg">
>> >>> 20. Feb 2017 16:28 by <a href="mailto:artyom.shalkhakov@gmail.com" class="gmail_msg" target="_blank">artyom.shalkhakov@gmail.com</a>:<br class="gmail_msg">
>> >>><br class="gmail_msg">
>> >>><br class="gmail_msg">
>> >>> Hello all,<br class="gmail_msg">
>> >>><br class="gmail_msg">
>> >>> 'm doing form validation stuff, following examples on MDN. [1]<br class="gmail_msg">
>> >>><br class="gmail_msg">
>> >>> It seems like Ur/Web doesn't handle regular expressions?<br class="gmail_msg">
>> >>><br class="gmail_msg">
>> >>> I guess it should not be too diffcult to define a DSEL in Ur/Web (just<br class="gmail_msg">
>> >>> AST constructors and a few trusted functions: e.g. [compile : AST -><br class="gmail_msg">
>> >>> regexp], where [regexp] is an abstract type, or maybe just a string<br class="gmail_msg">
>> >>> :-)) and<br class="gmail_msg">
>> >>> have it work at least in the browser.<br class="gmail_msg">
>> >>><br class="gmail_msg">
>> >>> Could somebody point me in the right direction here?<br class="gmail_msg">
>> >>><br class="gmail_msg">
>> >>> --<br class="gmail_msg">
>> >>> Cheers,<br class="gmail_msg">
>> >>> Artyom Shalkhakov<br class="gmail_msg">
>> >>><br class="gmail_msg">
>> >>> [1]<br class="gmail_msg">
>> >>><br class="gmail_msg">
>> >>> <a href="https://developer.mozilla.org/en-US/docs/Web/Guide/HTML/HTML5/Constraint_validation" rel="noreferrer" class="gmail_msg" target="_blank">https://developer.mozilla.org/en-US/docs/Web/Guide/HTML/HTML5/Constraint_validation</a><br class="gmail_msg">
>> >>><br class="gmail_msg">
>> >><br class="gmail_msg">
>> >><br class="gmail_msg">
>> >><br class="gmail_msg">
>> >> --<br class="gmail_msg">
>> >> Cheers,<br class="gmail_msg">
>> >> Artyom Shalkhakov<br class="gmail_msg">
>> >><br class="gmail_msg">
>> >> _______________________________________________<br class="gmail_msg">
>> >> Ur mailing list<br class="gmail_msg">
>> >> <a href="mailto:Ur@impredicative.com" class="gmail_msg" target="_blank">Ur@impredicative.com</a><br class="gmail_msg">
>> >> <a href="http://www.impredicative.com/cgi-bin/mailman/listinfo/ur" rel="noreferrer" class="gmail_msg" target="_blank">http://www.impredicative.com/cgi-bin/mailman/listinfo/ur</a><br class="gmail_msg">
>> >><br class="gmail_msg">
>> ><br class="gmail_msg">
>> ><br class="gmail_msg">
>> > _______________________________________________<br class="gmail_msg">
>> > Ur mailing list<br class="gmail_msg">
>> > <a href="mailto:Ur@impredicative.com" class="gmail_msg" target="_blank">Ur@impredicative.com</a><br class="gmail_msg">
>> > <a href="http://www.impredicative.com/cgi-bin/mailman/listinfo/ur" rel="noreferrer" class="gmail_msg" target="_blank">http://www.impredicative.com/cgi-bin/mailman/listinfo/ur</a><br class="gmail_msg">
>> ><br class="gmail_msg">
>><br class="gmail_msg">
>> --<br class="gmail_msg">
>> Cheers,<br class="gmail_msg">
>> Artyom Shalkhakov<br class="gmail_msg">
>><br class="gmail_msg">
>> [1] <a href="https://github.com/bbarenblat/urweb-regex/pull/1" rel="noreferrer" class="gmail_msg" target="_blank">https://github.com/bbarenblat/urweb-regex/pull/1</a><br class="gmail_msg">
>><br class="gmail_msg">
>> _______________________________________________<br class="gmail_msg">
>> Ur mailing list<br class="gmail_msg">
>> <a href="mailto:Ur@impredicative.com" class="gmail_msg" target="_blank">Ur@impredicative.com</a><br class="gmail_msg">
>> <a href="http://www.impredicative.com/cgi-bin/mailman/listinfo/ur" rel="noreferrer" class="gmail_msg" target="_blank">http://www.impredicative.com/cgi-bin/mailman/listinfo/ur</a><br class="gmail_msg">
><br class="gmail_msg">
><br class="gmail_msg">
> _______________________________________________<br class="gmail_msg">
> Ur mailing list<br class="gmail_msg">
> <a href="mailto:Ur@impredicative.com" class="gmail_msg" target="_blank">Ur@impredicative.com</a><br class="gmail_msg">
> <a href="http://www.impredicative.com/cgi-bin/mailman/listinfo/ur" rel="noreferrer" class="gmail_msg" target="_blank">http://www.impredicative.com/cgi-bin/mailman/listinfo/ur</a><br class="gmail_msg">
><br class="gmail_msg">
<br class="gmail_msg">
<br class="gmail_msg">
<br class="gmail_msg">
--<br class="gmail_msg">
Cheers,<br class="gmail_msg">
Artyom Shalkhakov<br class="gmail_msg">
<br class="gmail_msg">
_______________________________________________<br class="gmail_msg">
Ur mailing list<br class="gmail_msg">
<a href="mailto:Ur@impredicative.com" class="gmail_msg" target="_blank">Ur@impredicative.com</a><br class="gmail_msg">
<a href="http://www.impredicative.com/cgi-bin/mailman/listinfo/ur" rel="noreferrer" class="gmail_msg" target="_blank">http://www.impredicative.com/cgi-bin/mailman/listinfo/ur</a><br class="gmail_msg">
</blockquote></div></div>