# HG changeset patch # User Adam Chlipala # Date 1224605195 14400 # Node ID 4d519baf357c941c02807a3fbee8f4cbd5b7a89d # Parent 040edfade639cc5853c71419f099642a886f596d ListShop skeleton diff -r 040edfade639 -r 4d519baf357c demo/list.ur --- /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 diff -r 040edfade639 -r 4d519baf357c demo/list.urs --- /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 diff -r 040edfade639 -r 4d519baf357c demo/listFun.ur --- 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 end diff -r 040edfade639 -r 4d519baf357c demo/listFun.urs --- 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 - diff -r 040edfade639 -r 4d519baf357c demo/listShop.ur --- /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 + Pick your poison:
+
  • Integers
    • +
  • Strings
    • +     diff -r 040edfade639 -r 4d519baf357c demo/listShop.urp --- /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 diff -r 040edfade639 -r 4d519baf357c demo/listShop.urs --- /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 diff -r 040edfade639 -r 4d519baf357c src/elaborate.sml --- 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