annotate tests/tryRpc.ur @ 2094:0d898b086bbe

Improve wildify heuristic for finding record type-class witnesses
author Adam Chlipala <adam@chlipala.net>
date Tue, 23 Dec 2014 13:42:20 -0500
parents e15234fbb163
children
rev   line source
adam@1848 1 fun isBeppo (s : string) : transaction string =
adam@1848 2 case s of
adam@1848 3 "Beppo" => return "Yup, that's him!"
adam@1848 4 | "Mephisto" => error <xml>Great googely moogely!</xml>
adam@1848 5 | _ => return "Who's that?"
adam@1848 6
adam@1848 7 fun listOf (n : int) =
adam@1848 8 if n < 0 then
adam@1848 9 error <xml>Negative!</xml>
adam@1848 10 else if n = 0 then
adam@1848 11 return []
adam@1848 12 else
adam@1848 13 ls <- listOf (n - 1);
adam@1848 14 return (n :: ls)
adam@1848 15
adam@1848 16 fun length ls =
adam@1848 17 case ls of
adam@1848 18 [] => 0
adam@1848 19 | _ :: ls' => 1 + length ls'
adam@1848 20
adam@1848 21 fun main () : transaction page =
adam@1848 22 s <- source "";
adam@1848 23 ns <- source "";
adam@1848 24 return <xml><body>
adam@1848 25 <ctextbox source={s}/>
adam@1848 26 <button value="rpc" onclick={fn _ => v <- get s;
adam@1848 27 r <- rpc (isBeppo v);
adam@1848 28 alert r}/>
adam@1848 29 <button value="tryRpc" onclick={fn _ => v <- get s;
adam@1848 30 r <- tryRpc (isBeppo v);
adam@1848 31 case r of
adam@1848 32 None => alert "Faaaaaailure."
adam@1848 33 | Some r => alert ("Success: " ^ r)}/>
adam@1848 34
adam@1848 35 <hr/>
adam@1848 36
adam@1848 37 <ctextbox source={ns}/>
adam@1848 38 <button value="rpc" onclick={fn _ => v <- get ns;
adam@1848 39 r <- rpc (listOf (readError v));
adam@1848 40 alert (show (length r))}/>
adam@1848 41 <button value="tryRpc" onclick={fn _ => v <- get ns;
adam@1848 42 r <- tryRpc (listOf (readError v));
adam@1848 43 case r of
adam@1848 44 None => alert "Faaaaaailure."
adam@1848 45 | Some r => alert ("Success: " ^ show (length r))}/>
adam@1848 46 </body></xml>