<div>Looks good—glad it worked out!</div><div><br></div><div>My main question: what happens if the whole string is matched but a particular subgroup isn't? This can happen with alt or star, for instance. I couldn't tell from the types. I would expect a return type for match to be something like `match r (option string)` instead of `option (match r string)`. I don't know the underlying regex library, so perhaps there's a good reason for this.</div><div><br></div><div>I also thought it may be useful if alt allowed the same group to be captured on either side, but I realize that takes further fiddling with subgroup indices and post-processing of the results (each group field name would map to a list of indices instead of a single index), so it can wait for version 2 :).</div><div><br></div><div><br><div class="gmail_quote"><div>On Tue, Mar 7, 2017 at 02:11 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">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] => [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 underlying<br class="gmail_msg">
> library requires explicit names for captured groups, you'll need 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 fact,<br class="gmail_msg">
> this way has another benefit: the internal representation of the type 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 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 know<br class="gmail_msg">
> for sure) that Ur/Web will be able to infer the extra stuff in any concrete<br class="gmail_msg">
> (that is, monomorphic) use, so the user code will still look pretty. Here's<br class="gmail_msg">
> how some of the functions look with this. The place weaken gets used is 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">
> [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 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 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 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 of<br class="gmail_msg">
>> regexps to an off-the-shelf library. The [compile] function would print and<br class="gmail_msg">
>> escape the AST to a regexp string, and the Ur/Web compiler might 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 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 :-)) 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">
>>> <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">
</blockquote></div></div>