diff options
| -rw-r--r-- | demo/list.ur | 15 | ||||
| -rw-r--r-- | demo/list.urs | 5 | ||||
| -rw-r--r-- | demo/listFun.ur | 2 | ||||
| -rw-r--r-- | demo/listFun.urs | 1 | ||||
| -rw-r--r-- | demo/listShop.ur | 16 | ||||
| -rw-r--r-- | demo/listShop.urp | 4 | ||||
| -rw-r--r-- | demo/listShop.urs | 1 | ||||
| -rw-r--r-- | src/elaborate.sml | 7 |
8 files changed, 48 insertions, 3 deletions
diff --git a/demo/list.ur b/demo/list.ur new file mode 100644 index 00000000..c2dfce22 --- /dev/null +++ b/demo/list.ur @@ -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 --git a/demo/list.urs b/demo/list.urs new file mode 100644 index 00000000..e09f5118 --- /dev/null +++ b/demo/list.urs @@ -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 --git a/demo/listFun.ur b/demo/listFun.ur index 7a3459aa..833aee51 100644 --- a/demo/listFun.ur +++ b/demo/listFun.ur @@ -1,5 +1,5 @@ functor Make(M : sig type t end) = struct - val x = 6 + fun main () = return <xml/> end diff --git a/demo/listFun.urs b/demo/listFun.urs index ce4acafc..8fd6eb0d 100644 --- a/demo/listFun.urs +++ b/demo/listFun.urs @@ -3,4 +3,3 @@ functor Make(M : sig end) : sig val main : unit -> transaction page end - diff --git a/demo/listShop.ur b/demo/listShop.ur new file mode 100644 index 00000000..04386349 --- /dev/null +++ b/demo/listShop.ur @@ -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> diff --git a/demo/listShop.urp b/demo/listShop.urp new file mode 100644 index 00000000..85d318d4 --- /dev/null +++ b/demo/listShop.urp @@ -0,0 +1,4 @@ + +list +listFun +listShop diff --git a/demo/listShop.urs b/demo/listShop.urs new file mode 100644 index 00000000..6ac44e0b --- /dev/null +++ b/demo/listShop.urs @@ -0,0 +1 @@ +val main : unit -> transaction page diff --git a/src/elaborate.sml b/src/elaborate.sml index 035b95f6..9107f29a 100644 --- a/src/elaborate.sml +++ b/src/elaborate.sml @@ -2292,11 +2292,16 @@ fun subSgn (env, denv) sgn1 (sgn2 as (_, loc2)) = 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 |