From 90dfc7504b401b3b8b8964bb0725db20f31675e1 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Thu, 8 Jan 2009 09:57:45 -0500 Subject: Injected an enumeration --- tests/jsinj.ur | 24 +++++++++++++++++++++--- 1 file changed, 21 insertions(+), 3 deletions(-) (limited to 'tests/jsinj.ur') diff --git a/tests/jsinj.ur b/tests/jsinj.ur index 632a2839..518748d8 100644 --- a/tests/jsinj.ur +++ b/tests/jsinj.ur @@ -3,12 +3,23 @@ fun getOpt (t ::: Type) (o : option t) (v : t) : t = None => v | Some x => x +datatype color = Red | White | Blue + +fun colorToString c = + case c of + Red => "R" + | White => "W" + | Blue => "B" + +val show_color = mkShow colorToString + cookie int : int cookie float : float cookie string : string cookie bool : bool cookie pair : int * float cookie option : option int +cookie color : color fun main () : transaction page = n <- getCookie int; @@ -33,7 +44,11 @@ fun main () : transaction page = o <- getCookie option; o <- return (getOpt o (Some 1)); - op <- source None; + so <- source None; + + c <- getCookie color; + c <- return (getOpt c White); + sc <- source Blue; return {[n]}}/> @@ -51,8 +66,11 @@ fun main () : transaction page = {[p.1]}, {[p.2]}}/> CHANGE
- return None | Some x => return {[x]}}/> - CHANGE
+ CHANGE
+ + {[c]}}/> + CHANGE
-- cgit v1.2.3