Mercurial > urweb
changeset 846:0d30e6338c65
Some standard library reorgs and additions; handle mutual datatypes better in Specialize
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Tue, 09 Jun 2009 18:11:59 -0400 |
| parents | 6725d73c3c31 |
| children | 0f7e2cca6d9b |
| files | lib/ur/basis.urs lib/ur/list.ur lib/ur/list.urs lib/ur/listPair.ur lib/ur/listPair.urs lib/ur/option.ur lib/ur/option.urs src/monoize.sml src/specialize.sml |
| diffstat | 9 files changed, 85 insertions(+), 60 deletions(-) [+] |
line wrap: on
line diff
--- a/lib/ur/basis.urs Tue Jun 09 11:12:34 2009 -0400 +++ b/lib/ur/basis.urs Tue Jun 09 18:11:59 2009 -0400 @@ -25,7 +25,6 @@ val eq_char : eq char val eq_bool : eq bool val eq_time : eq time -val eq_option : t ::: Type -> eq t -> eq (option t) val mkEq : t ::: Type -> (t -> t -> bool) -> eq t class num
--- a/lib/ur/list.ur Tue Jun 09 11:12:34 2009 -0400 +++ b/lib/ur/list.ur Tue Jun 09 18:11:59 2009 -0400 @@ -10,6 +10,17 @@ mkShow show' end +val eq = fn [a] (_ : eq a) => + let + fun eq' (ls1 : list a) ls2 = + case (ls1, ls2) of + ([], []) => True + | (x1 :: ls1, x2 :: ls2) => x1 = x2 && eq' ls1 ls2 + | _ => False + in + mkEq eq' + end + fun foldl [a] [b] f = let fun foldl' acc ls = @@ -20,6 +31,19 @@ foldl' end +fun foldlPartial [a] [b] f = + let + fun foldlPartial' acc ls = + case ls of + [] => Some acc + | x :: ls => + case f x acc of + None => None + | Some acc' => foldlPartial' acc' ls + in + foldlPartial' + end + val rev = fn [a] => let fun rev' acc (ls : list a) =
--- a/lib/ur/list.urs Tue Jun 09 11:12:34 2009 -0400 +++ b/lib/ur/list.urs Tue Jun 09 18:11:59 2009 -0400 @@ -1,8 +1,10 @@ datatype t = datatype Basis.list -val show : a ::: Type -> show a -> show (list a) +val show : a ::: Type -> show a -> show (t a) +val eq : a ::: Type -> eq a -> eq (t a) val foldl : a ::: Type -> b ::: Type -> (a -> b -> b) -> b -> t a -> b +val foldlPartial : a ::: Type -> b ::: Type -> (a -> b -> option b) -> b -> t a -> option b val rev : a ::: Type -> t a -> t a
--- a/lib/ur/listPair.ur Tue Jun 09 11:12:34 2009 -0400 +++ b/lib/ur/listPair.ur Tue Jun 09 18:11:59 2009 -0400 @@ -1,3 +1,17 @@ +fun foldlPartial [a] [b] [c] f = + let + fun foldlPartial' acc ls1 ls2 = + case (ls1, ls2) of + ([], []) => Some acc + | (x1 :: ls1, x2 :: ls2) => + (case f x1 x2 acc of + None => None + | Some acc' => foldlPartial' acc' ls1 ls2) + | _ => None + in + foldlPartial' + end + fun mapX [a] [b] [ctx ::: {Unit}] f = let fun mapX' ls1 ls2 =
--- a/lib/ur/listPair.urs Tue Jun 09 11:12:34 2009 -0400 +++ b/lib/ur/listPair.urs Tue Jun 09 18:11:59 2009 -0400 @@ -1,3 +1,6 @@ +val foldlPartial : a ::: Type -> b ::: Type -> c ::: Type + -> (a -> b -> c -> option c) -> c -> list a -> list b -> option c + val mapX : a ::: Type -> b ::: Type -> ctx ::: {Unit} -> (a -> b -> xml ctx [] []) -> list a -> list b -> xml ctx [] []
--- a/lib/ur/option.ur Tue Jun 09 11:12:34 2009 -0400 +++ b/lib/ur/option.ur Tue Jun 09 18:11:59 2009 -0400 @@ -1,5 +1,12 @@ datatype t = datatype Basis.option +fun eq [a] (_ : eq a) = + mkEq (fn x y => + case (x, y) of + (None, None) => True + | (Some x, Some y) => x = y + | _ => False) + fun isSome [a] x = case x of None => False @@ -9,3 +16,8 @@ case x of None => None | Some y => Some (f y) + +fun bind [a] [b] f x = + case x of + None => None + | Some y => f y
--- a/lib/ur/option.urs Tue Jun 09 11:12:34 2009 -0400 +++ b/lib/ur/option.urs Tue Jun 09 18:11:59 2009 -0400 @@ -1,5 +1,8 @@ datatype t = datatype Basis.option +val eq : a ::: Type -> eq a -> eq (t a) + val isSome : a ::: Type -> t a -> bool val mp : a ::: Type -> b ::: Type -> (a -> b) -> t a -> t b +val bind : a ::: Type -> b ::: Type -> (a -> option b) -> t a -> t b
--- a/src/monoize.sml Tue Jun 09 11:12:34 2009 -0400 +++ b/src/monoize.sml Tue Jun 09 18:11:59 2009 -0400 @@ -778,47 +778,6 @@ (L'.TFfi ("Basis", "bool"), loc), (L'.EBinop ("==", (L'.ERel 1, loc), (L'.ERel 0, loc)), loc)), loc)), loc), fm) - | L.ECApp ((L.EFfi ("Basis", "eq_option"), _), t) => - let - val t = monoType env t - val t' = (L'.TOption t, loc) - val bool = (L'.TFfi ("Basis", "bool"), loc) - in - ((L'.EAbs ("f", (L'.TFun (t, (L'.TFun (t, bool), loc)), loc), - (L'.TFun (t', (L'.TFun (t', bool), loc)), loc), - (L'.EAbs ("x", t', (L'.TFun (t', bool), loc), - (L'.EAbs ("y", t', bool, - (L'.ECase ((L'.ERecord [("1", (L'.ERel 1, loc), t'), - ("2", (L'.ERel 0, loc), t')], loc), - [((L'.PRecord [("1", (L'.PNone t, loc), t'), - ("2", (L'.PNone t, loc), t')], loc), - (L'.ECon (L'.Enum, L'.PConFfi {mod = "Basis", - datatyp = "bool", - con = "True", - arg = NONE}, - NONE), loc)), - ((L'.PRecord [("1", (L'.PSome (t, - (L'.PVar ("x1", - t), loc)), - loc), t'), - ("2", (L'.PSome (t, - (L'.PVar ("x2", - t), loc)), - loc), t')], loc), - (L'.EApp ((L'.EApp ((L'.ERel 4, loc), - (L'.ERel 1, loc)), loc), - (L'.ERel 0, loc)), loc)), - ((L'.PWild, loc), - (L'.ECon (L'.Enum, L'.PConFfi {mod = "Basis", - datatyp = "bool", - con = "False", - arg = NONE}, - NONE), loc))], - {disc = (L'.TRecord [("1", t'), ("2", t')], loc), - result = (L'.TFfi ("Basis", "bool"), loc)}), - loc)), loc)), loc)), loc), - fm) - end | L.ECApp ((L.EFfi ("Basis", "mkEq"), _), t) => let
--- a/src/specialize.sml Tue Jun 09 11:12:34 2009 -0400 +++ b/src/specialize.sml Tue Jun 09 18:11:59 2009 -0400 @@ -61,7 +61,7 @@ count : int, datatypes : datatyp IM.map, constructors : int IM.map, - decls : decl list + decls : (string * int * string list * (string * int * con option) list) list } fun kind (k, st) = (k, st) @@ -115,15 +115,15 @@ ((x, n, SOME t), st) end) st cons - val d = (DDatatype [(#name dt ^ "_s", - n', - [], - cons)], #2 (List.hd args)) + val dt = (#name dt ^ "_s", + n', + [], + cons) in (n', cmap, {count = #count st, datatypes = #datatypes st, constructors = #constructors st, - decls = d :: #decls st}) + decls = dt :: #decls st}) end and con (c, st : state) = @@ -246,22 +246,31 @@ let (*val () = Print.preface ("decl:", CorePrint.p_decl CoreEnv.empty all)*) val (d, st) = specDecl st d + + val ds = + case #decls st of + [] => [] + | dts => [(DDatatype dts, #2 d)] in case #1 d of - DDatatype [(x, n, xs, xnts)] => - (rev (d :: #decls st), + DDatatype dts => + (rev (d :: ds), {count = #count st, - datatypes = IM.insert (#datatypes st, n, - {name = x, - params = length xs, - constructors = xnts, - specializations = CM.empty}), - constructors = foldl (fn ((_, n', _), constructors) => - IM.insert (constructors, n', n)) - (#constructors st) xnts, + datatypes = foldl (fn ((x, n, xs, xnts), dts) => + IM.insert (dts, n, + {name = x, + params = length xs, + constructors = xnts, + specializations = CM.empty})) + (#datatypes st) dts, + constructors = foldl (fn ((x, n, xs, xnts), cs) => + foldl (fn ((_, n', _), constructors) => + IM.insert (constructors, n', n)) + cs xnts) + (#constructors st) dts, decls = []}) | _ => - (rev (d :: #decls st), + (rev (d :: ds), {count = #count st, datatypes = #datatypes st, constructors = #constructors st,