Mercurial > urweb
changeset 397:4d519baf357c
ListShop skeleton
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Tue, 21 Oct 2008 12:06:35 -0400 |
| parents | 040edfade639 |
| children | ab3177746c78 |
| files | demo/list.ur demo/list.urs demo/listFun.ur demo/listFun.urs demo/listShop.ur demo/listShop.urp demo/listShop.urs src/elaborate.sml |
| diffstat | 8 files changed, 48 insertions(+), 3 deletions(-) [+] |
line wrap: on
line diff
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/demo/list.ur Tue Oct 21 12:06:35 2008 -0400 @@ -0,0 +1,15 @@ +datatype list t = Nil | Cons of t * list t + +fun length' (t ::: Type) (ls : list t) (acc : int) = + case ls of + Nil => acc + | Cons (_, ls') => length' ls' (acc + 1) + +fun length (t ::: Type) (ls : list t) = length' ls 0 + +fun rev' (t ::: Type) (ls : list t) (acc : list t) = + case ls of + Nil => acc + | Cons (x, ls') => rev' ls' (Cons (x, acc)) + +fun rev (t ::: Type) (ls : list t) = rev' ls Nil
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/demo/list.urs Tue Oct 21 12:06:35 2008 -0400 @@ -0,0 +1,5 @@ +datatype list t = Nil | Cons of t * list t + +val length : t ::: Type -> list t -> int + +val rev : t ::: Type -> list t -> list t
--- a/demo/listFun.ur Tue Oct 21 11:39:13 2008 -0400 +++ b/demo/listFun.ur Tue Oct 21 12:06:35 2008 -0400 @@ -1,5 +1,5 @@ functor Make(M : sig type t end) = struct - val x = 6 + fun main () = return <xml/> end
--- a/demo/listFun.urs Tue Oct 21 11:39:13 2008 -0400 +++ b/demo/listFun.urs Tue Oct 21 12:06:35 2008 -0400 @@ -3,4 +3,3 @@ end) : sig val main : unit -> transaction page end -
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/demo/listShop.ur Tue Oct 21 12:06:35 2008 -0400 @@ -0,0 +1,16 @@ +structure I = struct + type t = int +end + +structure S = struct + type t = string +end + +structure IL = ListFun.Make(I) +structure SL = ListFun.Make(S) + +fun main () = return <xml><body> + Pick your poison:<br/> + <li> <a link={IL.main ()}>Integers</a></li> + <li> <a link={SL.main ()}>Strings</a></li> +</body></xml>
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/demo/listShop.urp Tue Oct 21 12:06:35 2008 -0400 @@ -0,0 +1,4 @@ + +list +listFun +listShop
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/demo/listShop.urs Tue Oct 21 12:06:35 2008 -0400 @@ -0,0 +1,1 @@ +val main : unit -> transaction page
--- a/src/elaborate.sml Tue Oct 21 11:39:13 2008 -0400 +++ b/src/elaborate.sml Tue Oct 21 12:06:35 2008 -0400 @@ -2292,11 +2292,16 @@ env else E.pushCNamedAs env x n1 (L'.KType, loc) - (SOME (L'.CNamed n1, loc)) + (SOME (L'.CNamed n2, loc)) in SOME (env, denv) end + val env = E.pushCNamedAs env x n1 k' NONE + val env = if n1 = n2 then + env + else + E.pushCNamedAs env x n2 k' (SOME (L'.CNamed n1, loc)) val env = foldl (fn (x, env) => E.pushCRel env x k) env xs1 fun xncBad ((x1, _, t1), (x2, _, t2)) = String.compare (x1, x2) <> EQUAL