From 0fa422bfaf3931aacff958cb73d44ebfa4191f4a Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Thu, 23 Oct 2008 12:58:35 -0400 Subject: Fix nasty de Bruijn substitution bug; TcSum demo --- src/reduce.sml | 115 +++++++++++++++++++++++++++++++-------------------------- 1 file changed, 63 insertions(+), 52 deletions(-) (limited to 'src/reduce.sml') diff --git a/src/reduce.sml b/src/reduce.sml index 0250175f..927c8ff1 100644 --- a/src/reduce.sml +++ b/src/reduce.sml @@ -36,6 +36,7 @@ structure U = CoreUtil val liftConInCon = E.liftConInCon val subConInCon = E.subConInCon +val liftConInExp = E.liftConInExp val liftExpInExp = U.Exp.mapB {kind = fn k => k, @@ -63,6 +64,7 @@ val subExpInExp = | LESS => e) | _ => e, bind = fn ((xn, rep), U.Exp.RelE _) => (xn+1, liftExpInExp 0 rep) + | ((xn, rep), U.Exp.RelC _) => (xn, liftConInExp 0 rep) | (ctx, _) => ctx} val liftConInExp = E.liftConInExp @@ -106,58 +108,67 @@ fun con env c = and reduceCon env = U.Con.mapB {kind = kind, con = con, bind = bindC} env fun exp env e = - case e of - ENamed n => - (case E.lookupENamed env n of - (_, _, SOME e', _) => #1 e' - | _ => e) - - | ECApp ((EApp ((EApp ((ECApp ((EFold ks, _), ran), _), f), _), i), _), (CRecord (k, xcs), loc)) => - (case xcs of - [] => #1 i - | (n, v) :: rest => - #1 (reduceExp env (EApp ((ECApp ((ECApp ((ECApp (f, n), loc), v), loc), (CRecord (k, rest), loc)), loc), - (ECApp ((EApp ((EApp ((ECApp ((EFold ks, loc), ran), loc), f), loc), i), loc), - (CRecord (k, rest), loc)), loc)), loc))) - - | EApp ((EAbs (_, _, _, e1), loc), e2) => - #1 (reduceExp env (subExpInExp (0, e2) e1)) - | ECApp ((ECAbs (_, _, e1), loc), c) => - #1 (reduceExp env (subConInExp (0, c) e1)) - - | EField ((ERecord xes, _), (CName x, _), _) => - (case List.find (fn ((CName x', _), _, _) => x' = x - | _ => false) xes of - SOME (_, e, _) => #1 e - | NONE => e) - | EWith (r as (_, loc), x, e, {rest = (CRecord (k, xts), _), field}) => - let - fun fields (remaining, passed) = - case remaining of - [] => [] - | (x, t) :: rest => - (x, - (EField (r, x, {field = t, - rest = (CRecord (k, List.revAppend (passed, rest)), loc)}), loc), - t) :: fields (rest, (x, t) :: passed) - in - #1 (reduceExp env (ERecord ((x, e, field) :: fields (xts, [])), loc)) - end - | ECut (r as (_, loc), _, {rest = (CRecord (k, xts), _), ...}) => - let - fun fields (remaining, passed) = - case remaining of - [] => [] - | (x, t) :: rest => - (x, - (EField (r, x, {field = t, - rest = (CRecord (k, List.revAppend (passed, rest)), loc)}), loc), - t) :: fields (rest, (x, t) :: passed) - in - #1 (reduceExp env (ERecord (fields (xts, [])), loc)) - end - - | _ => e + let + (*val () = Print.prefaces "exp" [("e", CorePrint.p_exp env (e, ErrorMsg.dummySpan))]*) + + val r = case e of + ENamed n => + (case E.lookupENamed env n of + (_, _, SOME e', _) => #1 e' + | _ => e) + + | ECApp ((EApp ((EApp ((ECApp ((EFold ks, _), ran), _), f), _), i), _), (CRecord (k, xcs), loc)) => + (case xcs of + [] => #1 i + | (n, v) :: rest => + #1 (reduceExp env (EApp ((ECApp ((ECApp ((ECApp (f, n), loc), v), loc), (CRecord (k, rest), loc)), loc), + (ECApp ((EApp ((EApp ((ECApp ((EFold ks, loc), ran), loc), f), loc), i), loc), + (CRecord (k, rest), loc)), loc)), loc))) + + | EApp ((EAbs (_, _, _, e1), loc), e2) => + #1 (reduceExp env (subExpInExp (0, e2) e1)) + | ECApp ((ECAbs (_, _, e1), loc), c) => + #1 (reduceExp env (subConInExp (0, c) e1)) + + | EField ((ERecord xes, _), (CName x, _), _) => + (case List.find (fn ((CName x', _), _, _) => x' = x + | _ => false) xes of + SOME (_, e, _) => #1 e + | NONE => e) + | EWith (r as (_, loc), x, e, {rest = (CRecord (k, xts), _), field}) => + let + fun fields (remaining, passed) = + case remaining of + [] => [] + | (x, t) :: rest => + (x, + (EField (r, x, {field = t, + rest = (CRecord (k, List.revAppend (passed, rest)), loc)}), loc), + t) :: fields (rest, (x, t) :: passed) + in + #1 (reduceExp env (ERecord ((x, e, field) :: fields (xts, [])), loc)) + end + | ECut (r as (_, loc), _, {rest = (CRecord (k, xts), _), ...}) => + let + fun fields (remaining, passed) = + case remaining of + [] => [] + | (x, t) :: rest => + (x, + (EField (r, x, {field = t, + rest = (CRecord (k, List.revAppend (passed, rest)), loc)}), loc), + t) :: fields (rest, (x, t) :: passed) + in + #1 (reduceExp env (ERecord (fields (xts, [])), loc)) + end + + | _ => e + in + (*Print.prefaces "exp'" [("e", CorePrint.p_exp env (e, ErrorMsg.dummySpan)), + ("r", CorePrint.p_exp env (r, ErrorMsg.dummySpan))];*) + + r + end and reduceExp env = U.Exp.mapB {kind = kind, con = con, exp = exp, bind = bind} env -- cgit v1.2.3 From 0e88aba4fcbcf9587c289a555315ec30a112a2f0 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Thu, 30 Oct 2008 16:58:54 -0400 Subject: Especialize --- lib/basis.urs | 3 + src/compiler.sig | 2 + src/compiler.sml | 9 ++- src/core_env.sig | 3 + src/core_env.sml | 29 +++++++++ src/core_util.sig | 5 ++ src/core_util.sml | 7 +++ src/especialize.sig | 32 ++++++++++ src/especialize.sml | 176 ++++++++++++++++++++++++++++++++++++++++++++++++++++ src/reduce.sml | 32 +--------- src/sources | 3 + 11 files changed, 270 insertions(+), 31 deletions(-) create mode 100644 src/especialize.sig create mode 100644 src/especialize.sml (limited to 'src/reduce.sml') diff --git a/lib/basis.urs b/lib/basis.urs index 8992bc8c..0e6b9988 100644 --- a/lib/basis.urs +++ b/lib/basis.urs @@ -352,6 +352,9 @@ val tt : bodyTag [] val font : bodyTag [Size = int, Face = string] val h1 : bodyTag [] +val h2 : bodyTag [] +val h3 : bodyTag [] +val h4 : bodyTag [] val li : bodyTag [] val hr : bodyTag [] diff --git a/src/compiler.sig b/src/compiler.sig index 0c95934a..e26ec13c 100644 --- a/src/compiler.sig +++ b/src/compiler.sig @@ -61,6 +61,7 @@ signature COMPILER = sig val termination : (Elab.file, Elab.file) phase val explify : (Elab.file, Expl.file) phase val corify : (Expl.file, Core.file) phase + val especialize : (Core.file, Core.file) phase val shake : (Core.file, Core.file) phase val tag : (Core.file, Core.file) phase val reduce : (Core.file, Core.file) phase @@ -82,6 +83,7 @@ signature COMPILER = sig val toTermination : (string, Elab.file) transform val toExplify : (string, Expl.file) transform val toCorify : (string, Core.file) transform + val toEspecialize : (string, Core.file) transform val toShake1 : (string, Core.file) transform val toTag : (string, Core.file) transform val toReduce : (string, Core.file) transform diff --git a/src/compiler.sml b/src/compiler.sml index 1f88705c..4f1bce11 100644 --- a/src/compiler.sml +++ b/src/compiler.sml @@ -404,12 +404,19 @@ val corify = { val toCorify = transform corify "corify" o toExplify +val especialize = { + func = ESpecialize.specialize, + print = CorePrint.p_file CoreEnv.empty +} + +val toEspecialize = transform especialize "especialize" o toCorify + val shake = { func = Shake.shake, print = CorePrint.p_file CoreEnv.empty } -val toShake1 = transform shake "shake1" o toCorify +val toShake1 = transform shake "shake1" o toEspecialize val tag = { func = Tag.tag, diff --git a/src/core_env.sig b/src/core_env.sig index cdbf5946..98e345cc 100644 --- a/src/core_env.sig +++ b/src/core_env.sig @@ -33,6 +33,9 @@ signature CORE_ENV = sig val liftConInExp : int -> Core.exp -> Core.exp val subConInExp : (int * Core.con) -> Core.exp -> Core.exp + val liftExpInExp : int -> Core.exp -> Core.exp + val subExpInExp : (int * Core.exp) -> Core.exp -> Core.exp + type env val empty : env diff --git a/src/core_env.sml b/src/core_env.sml index b399f62f..0faf5aab 100644 --- a/src/core_env.sml +++ b/src/core_env.sml @@ -93,6 +93,35 @@ val subConInExp = bind = fn ((xn, rep), U.Exp.RelC _) => (xn+1, liftConInCon 0 rep) | (ctx, _) => ctx} +val liftExpInExp = + U.Exp.mapB {kind = fn k => k, + con = fn _ => fn c => c, + exp = fn bound => fn e => + case e of + ERel xn => + if xn < bound then + e + else + ERel (xn + 1) + | _ => e, + bind = fn (bound, U.Exp.RelE _) => bound + 1 + | (bound, _) => bound} + +val subExpInExp = + U.Exp.mapB {kind = fn k => k, + con = fn _ => fn c => c, + exp = fn (xn, rep) => fn e => + case e of + ERel xn' => + (case Int.compare (xn', xn) of + EQUAL => #1 rep + | GREATER=> ERel (xn' - 1) + | LESS => e) + | _ => e, + bind = fn ((xn, rep), U.Exp.RelE _) => (xn+1, liftExpInExp 0 rep) + | ((xn, rep), U.Exp.RelC _) => (xn, liftConInExp 0 rep) + | (ctx, _) => ctx} + (* Back to environments *) exception UnboundRel of int diff --git a/src/core_util.sig b/src/core_util.sig index 43750698..2ae75305 100644 --- a/src/core_util.sig +++ b/src/core_util.sig @@ -107,6 +107,11 @@ structure Exp : sig val exists : {kind : Core.kind' -> bool, con : Core.con' -> bool, exp : Core.exp' -> bool} -> Core.exp -> bool + + val foldMap : {kind : Core.kind' * 'state -> Core.kind' * 'state, + con : Core.con' * 'state -> Core.con' * 'state, + exp : Core.exp' * 'state -> Core.exp' * 'state} + -> 'state -> Core.exp -> Core.exp * 'state end structure Decl : sig diff --git a/src/core_util.sml b/src/core_util.sml index 49182c09..df8465ae 100644 --- a/src/core_util.sml +++ b/src/core_util.sml @@ -578,6 +578,13 @@ fun exists {kind, con, exp} k = S.Return _ => true | S.Continue _ => false +fun foldMap {kind, con, exp} s e = + case mapfold {kind = fn k => fn s => S.Continue (kind (k, s)), + con = fn c => fn s => S.Continue (con (c, s)), + exp = fn e => fn s => S.Continue (exp (e, s))} e s of + S.Continue v => v + | S.Return _ => raise Fail "CoreUtil.Exp.foldMap: Impossible" + end structure Decl = struct diff --git a/src/especialize.sig b/src/especialize.sig new file mode 100644 index 00000000..df83e81b --- /dev/null +++ b/src/especialize.sig @@ -0,0 +1,32 @@ +(* Copyright (c) 2008, Adam Chlipala + * All rights reserved. + * + * Redistribution and use in source and binary forms, with or without + * modification, are permitted provided that the following conditions are met: + * + * - Redistributions of source code must retain the above copyright notice, + * this list of conditions and the following disclaimer. + * - Redistributions in binary form must reproduce the above copyright notice, + * this list of conditions and the following disclaimer in the documentation + * and/or other materials provided with the distribution. + * - The names of contributors may not be used to endorse or promote products + * derived from this software without specific prior written permission. + * + * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" + * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE + * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE + * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE + * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR + * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF + * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS + * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN + * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) + * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE + * POSSIBILITY OF SUCH DAMAGE. + *) + +signature ESPECIALIZE = sig + + val specialize : Core.file -> Core.file + +end diff --git a/src/especialize.sml b/src/especialize.sml new file mode 100644 index 00000000..a316ffaa --- /dev/null +++ b/src/especialize.sml @@ -0,0 +1,176 @@ +(* Copyright (c) 2008, Adam Chlipala + * All rights reserved. + * + * Redistribution and use in source and binary forms, with or without + * modification, are permitted provided that the following conditions are met: + * + * - Redistributions of source code must retain the above copyright notice, + * this list of conditions and the following disclaimer. + * - Redistributions in binary form must reproduce the above copyright notice, + * this list of conditions and the following disclaimer in the documentation + * and/or other materials provided with the distribution. + * - The names of contributors may not be used to endorse or promote products + * derived from this software without specific prior written permission. + * + * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" + * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE + * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE + * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE + * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR + * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF + * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS + * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN + * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) + * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE + * POSSIBILITY OF SUCH DAMAGE. + *) + +structure ESpecialize :> ESPECIALIZE = struct + +open Core + +structure E = CoreEnv +structure U = CoreUtil + +structure ILK = struct +type ord_key = int list +val compare = Order.joinL Int.compare +end + +structure ILM = BinaryMapFn(ILK) +structure IM = IntBinaryMap + +type func = { + name : string, + args : int ILM.map, + body : exp, + typ : con, + tag : string +} + +type state = { + maxName : int, + funcs : func IM.map, + decls : (string * int * con * exp * string) list +} + +fun kind (k, st) = (k, st) +fun con (c, st) = (c, st) + +fun exp (e, st : state) = + let + fun getApp e = + case e of + ENamed f => SOME (f, [], []) + | EApp (e1, (ENamed x, _)) => + (case getApp (#1 e1) of + NONE => NONE + | SOME (f, xs, xs') => SOME (f, xs @ [x], xs')) + | EApp (e1, e2) => + (case getApp (#1 e1) of + NONE => NONE + | SOME (f, xs, xs') => SOME (f, xs, xs' @ [e2])) + | _ => NONE + in + case getApp e of + NONE => (e, st) + | SOME (_, [], _) => (e, st) + | SOME (f, xs, xs') => + case IM.find (#funcs st, f) of + NONE => (e, st) + | SOME {name, args, body, typ, tag} => + case ILM.find (args, xs) of + SOME f' => (#1 (foldl (fn (e, arg) => (EApp (e, arg), ErrorMsg.dummySpan)) + (ENamed f', ErrorMsg.dummySpan) xs'), + st) + | NONE => + let + fun subBody (body, typ, xs) = + case (#1 body, #1 typ, xs) of + (_, _, []) => SOME (body, typ) + | (EAbs (_, _, _, body'), TFun (_, typ'), x :: xs) => + subBody (E.subExpInExp (0, (ENamed x, ErrorMsg.dummySpan)) body', + typ', + xs) + | _ => NONE + in + case subBody (body, typ, xs) of + NONE => (e, st) + | SOME (body', typ') => + let + val f' = #maxName st + val funcs = IM.insert (#funcs st, f, {name = name, + args = ILM.insert (args, xs, f'), + body = body, + typ = typ, + tag = tag}) + val st = { + maxName = f' + 1, + funcs = funcs, + decls = #decls st + } + + val (body', st) = specExp st body' + val e' = foldl (fn (e, arg) => (EApp (e, arg), ErrorMsg.dummySpan)) + (ENamed f', ErrorMsg.dummySpan) xs' + in + (#1 e', + {maxName = #maxName st, + funcs = #funcs st, + decls = (name, f', typ', body', tag ^ "_espec") :: #decls st}) + end + end + end + +and specExp st = U.Exp.foldMap {kind = kind, con = con, exp = exp} st + +fun decl (d, st) = (d, st) + +val specDecl = U.Decl.foldMap {kind = kind, con = con, exp = exp, decl = decl} + +fun specialize file = + let + fun doDecl (d, st) = + let + val (d', st) = specDecl st d + + val funcs = #funcs st + val funcs = + case #1 d of + DVal (x, n, c, e as (EAbs _, _), tag) => + IM.insert (funcs, n, {name = x, + args = ILM.empty, + body = e, + typ = c, + tag = tag}) + | DValRec vis => + foldl (fn ((x, n, c, e, tag), funcs) => + IM.insert (funcs, n, {name = x, + args = ILM.empty, + body = e, + typ = c, + tag = tag})) + funcs vis + | _ => funcs + + val ds = + case #decls st of + [] => [d'] + | vis => [(DValRec vis, ErrorMsg.dummySpan), d'] + in + (ds, {maxName = #maxName st, + funcs = funcs, + decls = []}) + end + + val (ds, _) = ListUtil.foldlMapConcat doDecl + {maxName = U.File.maxName file + 1, + funcs = IM.empty, + decls = []} + file + in + ds + end + + +end diff --git a/src/reduce.sml b/src/reduce.sml index 927c8ff1..8dc4527f 100644 --- a/src/reduce.sml +++ b/src/reduce.sml @@ -37,36 +37,8 @@ structure U = CoreUtil val liftConInCon = E.liftConInCon val subConInCon = E.subConInCon val liftConInExp = E.liftConInExp - -val liftExpInExp = - U.Exp.mapB {kind = fn k => k, - con = fn _ => fn c => c, - exp = fn bound => fn e => - case e of - ERel xn => - if xn < bound then - e - else - ERel (xn + 1) - | _ => e, - bind = fn (bound, U.Exp.RelE _) => bound + 1 - | (bound, _) => bound} - -val subExpInExp = - U.Exp.mapB {kind = fn k => k, - con = fn _ => fn c => c, - exp = fn (xn, rep) => fn e => - case e of - ERel xn' => - (case Int.compare (xn', xn) of - EQUAL => #1 rep - | GREATER=> ERel (xn' - 1) - | LESS => e) - | _ => e, - bind = fn ((xn, rep), U.Exp.RelE _) => (xn+1, liftExpInExp 0 rep) - | ((xn, rep), U.Exp.RelC _) => (xn, liftConInExp 0 rep) - | (ctx, _) => ctx} - +val liftExpInExp = E.liftExpInExp +val subExpInExp = E.subExpInExp val liftConInExp = E.liftConInExp val subConInExp = E.subConInExp diff --git a/src/sources b/src/sources index 3568279c..ebf71d9e 100644 --- a/src/sources +++ b/src/sources @@ -93,6 +93,9 @@ unpoly.sml specialize.sig specialize.sml +especialize.sig +especialize.sml + tag.sig tag.sml -- cgit v1.2.3 From 389aae9254a3bdee3e79bb75b7355de270f2e8dd Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Fri, 31 Oct 2008 09:30:22 -0400 Subject: Replace 'with' with '++' --- lib/top.ur | 50 +++++++++++++++++++++++++++++++++++++ lib/top.urs | 35 ++++++++++++++++++++++++++ src/core.sml | 2 +- src/core_print.sml | 23 +++++++---------- src/core_util.sml | 16 ++++++------ src/corify.sml | 4 +-- src/elab.sml | 2 +- src/elab_print.sml | 25 +++++++------------ src/elab_util.sml | 16 ++++++------ src/elaborate.sml | 70 ++++++++++++++++++++++++++-------------------------- src/expl.sml | 2 +- src/expl_print.sml | 23 +++++++---------- src/expl_util.sml | 16 ++++++------ src/explify.sml | 4 +-- src/monoize.sml | 2 +- src/reduce.sml | 8 +++--- src/source.sml | 2 +- src/source_print.sml | 12 ++++----- src/termination.sml | 2 +- src/urweb.grm | 5 ++-- src/urweb.lex | 1 - 21 files changed, 189 insertions(+), 131 deletions(-) (limited to 'src/reduce.sml') diff --git a/lib/top.ur b/lib/top.ur index d36af3f3..347b2a35 100644 --- a/lib/top.ur +++ b/lib/top.ur @@ -4,6 +4,9 @@ con idT (t :: Type) = t con record (t :: {Type}) = $t con fstTT (t :: (Type * Type)) = t.1 con sndTT (t :: (Type * Type)) = t.2 +con fstTTT (t :: (Type * Type * Type)) = t.1 +con sndTTT (t :: (Type * Type * Type)) = t.2 +con thdTTT (t :: (Type * Type * Type)) = t.3 con mapTT (f :: Type -> Type) = fold (fn nm t acc [[nm] ~ acc] => [nm = f t] ++ acc) [] @@ -14,6 +17,9 @@ con mapUT = fn f :: Type => fold (fn nm t acc [[nm] ~ acc] => con mapT2T (f :: (Type * Type) -> Type) = fold (fn nm t acc [[nm] ~ acc] => [nm = f t] ++ acc) [] +con mapT3T (f :: (Type * Type * Type) -> Type) = fold (fn nm t acc [[nm] ~ acc] => + [nm = f t] ++ acc) [] + con ex = fn tf :: (Type -> Type) => res ::: Type -> (choice :: Type -> tf choice -> res) -> res @@ -80,6 +86,17 @@ fun foldT2R (tf :: (Type * Type) -> Type) (tr :: {(Type * Type)} -> Type) f [nm] [t] [rest] r.nm (acc (r -- nm))) (fn _ => i) +fun foldT3R (tf :: (Type * Type * Type) -> Type) (tr :: {(Type * Type * Type)} -> Type) + (f : nm :: Name -> t :: (Type * Type * Type) -> rest :: {(Type * Type * Type)} + -> fn [[nm] ~ rest] => + tf t -> tr rest -> tr ([nm = t] ++ rest)) + (i : tr []) = + fold [fn r :: {(Type * Type * Type)} => $(mapT3T tf r) -> tr r] + (fn (nm :: Name) (t :: (Type * Type * Type)) (rest :: {(Type * Type * Type)}) + (acc : _ -> tr rest) [[nm] ~ rest] r => + f [nm] [t] [rest] r.nm (acc (r -- nm))) + (fn _ => i) + fun foldTR2 (tf1 :: Type -> Type) (tf2 :: Type -> Type) (tr :: {Type} -> Type) (f : nm :: Name -> t :: Type -> rest :: {Type} -> fn [[nm] ~ rest] => @@ -103,6 +120,18 @@ fun foldT2R2 (tf1 :: (Type * Type) -> Type) (tf2 :: (Type * Type) -> Type) f [nm] [t] [rest] r1.nm r2.nm (acc (r1 -- nm) (r2 -- nm))) (fn _ _ => i) +fun foldT3R2 (tf1 :: (Type * Type * Type) -> Type) (tf2 :: (Type * Type * Type) -> Type) + (tr :: {(Type * Type * Type)} -> Type) + (f : nm :: Name -> t :: (Type * Type * Type) -> rest :: {(Type * Type * Type)} + -> fn [[nm] ~ rest] => + tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest)) + (i : tr []) = + fold [fn r :: {(Type * Type * Type)} => $(mapT3T tf1 r) -> $(mapT3T tf2 r) -> tr r] + (fn (nm :: Name) (t :: (Type * Type * Type)) (rest :: {(Type * Type * Type)}) + (acc : _ -> _ -> tr rest) [[nm] ~ rest] r1 r2 => + f [nm] [t] [rest] r1.nm r2.nm (acc (r1 -- nm) (r2 -- nm))) + (fn _ _ => i) + fun foldTRX (tf :: Type -> Type) (ctx :: {Unit}) (f : nm :: Name -> t :: Type -> rest :: {Type} -> fn [[nm] ~ rest] => @@ -122,6 +151,16 @@ fun foldT2RX (tf :: (Type * Type) -> Type) (ctx :: {Unit}) {f [nm] [t] [rest] r}{acc}) +fun foldT3RX (tf :: (Type * Type * Type) -> Type) (ctx :: {Unit}) + (f : nm :: Name -> t :: (Type * Type * Type) -> rest :: {(Type * Type * Type)} + -> fn [[nm] ~ rest] => + tf t -> xml ctx [] []) = + foldT3R [tf] [fn _ => xml ctx [] []] + (fn (nm :: Name) (t :: (Type * Type * Type)) (rest :: {(Type * Type * Type)}) + [[nm] ~ rest] r acc => + {f [nm] [t] [rest] r}{acc}) + + fun foldTRX2 (tf1 :: Type -> Type) (tf2 :: Type -> Type) (ctx :: {Unit}) (f : nm :: Name -> t :: Type -> rest :: {Type} -> fn [[nm] ~ rest] => @@ -143,6 +182,17 @@ fun foldT2RX2 (tf1 :: (Type * Type) -> Type) (tf2 :: (Type * Type) -> Type) {f [nm] [t] [rest] r1 r2}{acc}) +fun foldT3RX2 (tf1 :: (Type * Type * Type) -> Type) (tf2 :: (Type * Type * Type) -> Type) + (ctx :: {Unit}) + (f : nm :: Name -> t :: (Type * Type * Type) -> rest :: {(Type * Type * Type)} + -> fn [[nm] ~ rest] => + tf1 t -> tf2 t -> xml ctx [] []) = + foldT3R2 [tf1] [tf2] [fn _ => xml ctx [] []] + (fn (nm :: Name) (t :: (Type * Type * Type)) (rest :: {(Type * Type * Type)}) + [[nm] ~ rest] r1 r2 acc => + {f [nm] [t] [rest] r1 r2}{acc}) + + fun queryX (tables ::: {{Type}}) (exps ::: {Type}) (ctx ::: {Unit}) (q : sql_query tables exps) [tables ~ exps] (f : $(exps ++ fold (fn nm (fields :: {Type}) acc [[nm] ~ acc] => diff --git a/lib/top.urs b/lib/top.urs index 6e9dda4e..d52ec9d7 100644 --- a/lib/top.urs +++ b/lib/top.urs @@ -4,6 +4,9 @@ con idT = fn t :: Type => t con record = fn t :: {Type} => $t con fstTT = fn t :: (Type * Type) => t.1 con sndTT = fn t :: (Type * Type) => t.2 +con fstTTT = fn t :: (Type * Type * Type) => t.1 +con sndTTT = fn t :: (Type * Type * Type) => t.2 +con thdTTT = fn t :: (Type * Type * Type) => t.3 con mapTT = fn f :: Type -> Type => fold (fn nm t acc [[nm] ~ acc] => [nm = f t] ++ acc) [] @@ -14,6 +17,9 @@ con mapUT = fn f :: Type => fold (fn nm t acc [[nm] ~ acc] => con mapT2T = fn f :: (Type * Type) -> Type => fold (fn nm t acc [[nm] ~ acc] => [nm = f t] ++ acc) [] +con mapT3T = fn f :: (Type * Type * Type) -> Type => fold (fn nm t acc [[nm] ~ acc] => + [nm = f t] ++ acc) [] + con ex = fn tf :: (Type -> Type) => res ::: Type -> (choice :: Type -> tf choice -> res) -> res @@ -55,6 +61,12 @@ val foldT2R : tf :: ((Type * Type) -> Type) -> tr :: ({(Type * Type)} -> Type) tf t -> tr rest -> tr ([nm = t] ++ rest)) -> tr [] -> r :: {(Type * Type)} -> $(mapT2T tf r) -> tr r +val foldT3R : tf :: ((Type * Type * Type) -> Type) -> tr :: ({(Type * Type * Type)} -> Type) + -> (nm :: Name -> t :: (Type * Type * Type) -> rest :: {(Type * Type * Type)} + -> fn [[nm] ~ rest] => + tf t -> tr rest -> tr ([nm = t] ++ rest)) + -> tr [] -> r :: {(Type * Type * Type)} -> $(mapT3T tf r) -> tr r + val foldTR2 : tf1 :: (Type -> Type) -> tf2 :: (Type -> Type) -> tr :: ({Type} -> Type) -> (nm :: Name -> t :: Type -> rest :: {Type} @@ -71,6 +83,14 @@ val foldT2R2 : tf1 :: ((Type * Type) -> Type) -> tf2 :: ((Type * Type) -> Type) -> tr [] -> r :: {(Type * Type)} -> $(mapT2T tf1 r) -> $(mapT2T tf2 r) -> tr r +val foldT3R2 : tf1 :: ((Type * Type * Type) -> Type) -> tf2 :: ((Type * Type * Type) -> Type) + -> tr :: ({(Type * Type * Type)} -> Type) + -> (nm :: Name -> t :: (Type * Type * Type) -> rest :: {(Type * Type * Type)} + -> fn [[nm] ~ rest] => + tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest)) + -> tr [] -> r :: {(Type * Type * Type)} + -> $(mapT3T tf1 r) -> $(mapT3T tf2 r) -> tr r + val foldTRX : tf :: (Type -> Type) -> ctx :: {Unit} -> (nm :: Name -> t :: Type -> rest :: {Type} -> fn [[nm] ~ rest] => @@ -83,6 +103,12 @@ val foldT2RX : tf :: ((Type * Type) -> Type) -> ctx :: {Unit} tf t -> xml ctx [] []) -> r :: {(Type * Type)} -> $(mapT2T tf r) -> xml ctx [] [] +val foldT3RX : tf :: ((Type * Type * Type) -> Type) -> ctx :: {Unit} + -> (nm :: Name -> t :: (Type * Type * Type) -> rest :: {(Type * Type * Type)} + -> fn [[nm] ~ rest] => + tf t -> xml ctx [] []) + -> r :: {(Type * Type * Type)} -> $(mapT3T tf r) -> xml ctx [] [] + val foldTRX2 : tf1 :: (Type -> Type) -> tf2 :: (Type -> Type) -> ctx :: {Unit} -> (nm :: Name -> t :: Type -> rest :: {Type} -> fn [[nm] ~ rest] => @@ -98,6 +124,15 @@ val foldT2RX2 : tf1 :: ((Type * Type) -> Type) -> tf2 :: ((Type * Type) -> Type) -> r :: {(Type * Type)} -> $(mapT2T tf1 r) -> $(mapT2T tf2 r) -> xml ctx [] [] + +val foldT3RX2 : tf1 :: ((Type * Type * Type) -> Type) -> tf2 :: ((Type * Type * Type) -> Type) + -> ctx :: {Unit} + -> (nm :: Name -> t :: (Type * Type * Type) -> rest :: {(Type * Type * Type)} + -> fn [[nm] ~ rest] => + tf1 t -> tf2 t -> xml ctx [] []) + -> r :: {(Type * Type * Type)} + -> $(mapT3T tf1 r) -> $(mapT3T tf2 r) -> xml ctx [] [] + val queryX : tables ::: {{Type}} -> exps ::: {Type} -> ctx ::: {Unit} -> sql_query tables exps -> fn [tables ~ exps] => diff --git a/src/core.sml b/src/core.sml index 11055aa4..baec6e41 100644 --- a/src/core.sml +++ b/src/core.sml @@ -93,7 +93,7 @@ datatype exp' = | ERecord of (con * exp * con) list | EField of exp * con * { field : con, rest : con } - | EWith of exp * con * exp * { field : con, rest : con } + | EConcat of exp * con * exp * con | ECut of exp * con * { field : con, rest : con } | EFold of kind diff --git a/src/core_print.sml b/src/core_print.sml index 0d470d39..1214a54f 100644 --- a/src/core_print.sml +++ b/src/core_print.sml @@ -283,31 +283,26 @@ fun p_exp' par env (e, _) = box [p_exp' true env e, string ".", p_con' true env c] - | EWith (e1, c, e2, {field, rest}) => + | EConcat (e1, c1, e2, c2) => parenIf par (if !debug then - box [p_exp env e1, + box [p_exp' true env e1, space, - string "with", + string ":", space, - p_con' true env c, + p_con env c1, + space, + string "++", space, - string "=", p_exp' true env e2, space, - string "[", - p_con env field, + string ":", space, - string " in ", - space, - p_con env rest, - string "]"] + p_con env c2] else - box [p_exp env e1, + box [p_exp' true env e1, space, string "with", space, - p_con' true env c, - space, p_exp' true env e2]) | ECut (e, c, {field, rest}) => parenIf par (if !debug then diff --git a/src/core_util.sml b/src/core_util.sml index df8465ae..f0697183 100644 --- a/src/core_util.sml +++ b/src/core_util.sml @@ -424,19 +424,17 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, bind} = S.map2 (mfc ctx rest, fn rest' => (EField (e', c', {field = field', rest = rest'}), loc))))) - | EWith (e1, c, e2, {field, rest}) => + | EConcat (e1, c1, e2, c2) => S.bind2 (mfe ctx e1, fn e1' => - S.bind2 (mfc ctx c, - fn c' => + S.bind2 (mfc ctx c1, + fn c1' => S.bind2 (mfe ctx e2, fn e2' => - S.bind2 (mfc ctx field, - fn field' => - S.map2 (mfc ctx rest, - fn rest' => - (EWith (e1', c', e2', {field = field', rest = rest'}), - loc)))))) + S.map2 (mfc ctx c2, + fn c2' => + (EConcat (e1', c1', e2', c2'), + loc))))) | ECut (e, c, {field, rest}) => S.bind2 (mfe ctx e, fn e' => diff --git a/src/corify.sml b/src/corify.sml index 89d1e63f..ff9506fd 100644 --- a/src/corify.sml +++ b/src/corify.sml @@ -566,8 +566,8 @@ fun corifyExp st (e, loc) = (corifyCon st c, corifyExp st e, corifyCon st t)) xes), loc) | L.EField (e1, c, {field, rest}) => (L'.EField (corifyExp st e1, corifyCon st c, {field = corifyCon st field, rest = corifyCon st rest}), loc) - | L.EWith (e1, c, e2, {field, rest}) => (L'.EWith (corifyExp st e1, corifyCon st c, corifyExp st e2, - {field = corifyCon st field, rest = corifyCon st rest}), loc) + | L.EConcat (e1, c1, e2, c2) => (L'.EConcat (corifyExp st e1, corifyCon st c1, corifyExp st e2, + corifyCon st c2), loc) | L.ECut (e1, c, {field, rest}) => (L'.ECut (corifyExp st e1, corifyCon st c, {field = corifyCon st field, rest = corifyCon st rest}), loc) | L.EFold k => (L'.EFold (corifyKind k), loc) diff --git a/src/elab.sml b/src/elab.sml index 9bb609bf..4202d367 100644 --- a/src/elab.sml +++ b/src/elab.sml @@ -108,7 +108,7 @@ datatype exp' = | ERecord of (con * exp * con) list | EField of exp * con * { field : con, rest : con } - | EWith of exp * con * exp * { field : con, rest : con } + | EConcat of exp * con * exp * con | ECut of exp * con * { field : con, rest : con } | EFold of kind diff --git a/src/elab_print.sml b/src/elab_print.sml index c1bc5938..8c0b41f7 100644 --- a/src/elab_print.sml +++ b/src/elab_print.sml @@ -317,33 +317,26 @@ fun p_exp' par env (e, _) = box [p_exp' true env e, string ".", p_con' true env c] - | EWith (e1, c, e2, {field, rest}) => + | EConcat (e1, c1, e2, c2) => parenIf par (if !debug then - box [p_exp env e1, + box [p_exp' true env e1, space, - string "with", + string ":", space, - p_con' true env c, + p_con env c1, space, - string "=", - p_exp' true env e2, + string "++", space, - string "[", - p_con env field, + p_exp' true env e2, space, - string " in ", + string ":", space, - p_con env rest, - string "]"] + p_con env c2] else - box [p_exp env e1, + box [p_exp' true env e1, space, string "with", space, - p_con' true env c, - space, - string "=", - space, p_exp' true env e2]) | ECut (e, c, {field, rest}) => parenIf par (if !debug then diff --git a/src/elab_util.sml b/src/elab_util.sml index 69ed3248..247e2b3a 100644 --- a/src/elab_util.sml +++ b/src/elab_util.sml @@ -309,19 +309,17 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, bind} = S.map2 (mfc ctx rest, fn rest' => (EField (e', c', {field = field', rest = rest'}), loc))))) - | EWith (e1, c, e2, {field, rest}) => + | EConcat (e1, c1, e2, c2) => S.bind2 (mfe ctx e1, fn e1' => - S.bind2 (mfc ctx c, - fn c' => + S.bind2 (mfc ctx c1, + fn c1' => S.bind2 (mfe ctx e2, fn e2' => - S.bind2 (mfc ctx field, - fn field' => - S.map2 (mfc ctx rest, - fn rest' => - (EWith (e1', c', e2', {field = field', rest = rest'}), - loc)))))) + S.map2 (mfc ctx c2, + fn c2' => + (EConcat (e1', c1', e2', c2'), + loc))))) | ECut (e, c, {field, rest}) => S.bind2 (mfe ctx e, fn e' => diff --git a/src/elaborate.sml b/src/elaborate.sml index 6e23c760..4927e37d 100644 --- a/src/elaborate.sml +++ b/src/elaborate.sml @@ -1,29 +1,29 @@ (* Copyright (c) 2008, Adam Chlipala - * All rights reserved. - * - * Redistribution and use in source and binary forms, with or without - * modification, are permitted provided that the following conditions are met: - * - * - Redistributions of source code must retain the above copyright notice, - * this list of conditions and the following disclaimer. - * - Redistributions in binary form must reproduce the above copyright notice, - * this list of conditions and the following disclaimer in the documentation - * and/or other materials provided with the distribution. - * - The names of contributors may not be used to endorse or promote products - * derived from this software without specific prior written permission. - * - * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" - * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE - * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE - * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE - * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR - * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF - * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS - * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN - * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) - * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE - * POSSIBILITY OF SUCH DAMAGE. - *) + * All rights reserved. + * + * Redistribution and use in source and binary forms, with or without + * modification, are permitted provided that the following conditions are met: + * + * - Redistributions of source code must retain the above copyright notice, + * this list of conditions and the following disclaimer. + * - Redistributions in binary form must reproduce the above copyright notice, + * this list of conditions and the following disclaimer in the documentation + * and/or other materials provided with the distribution. + * - The names of contributors may not be used to endorse or promote products + * derived from this software without specific prior written permission. + * + * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" + * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE + * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE + * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE + * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR + * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF + * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS + * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN + * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) + * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE + * POSSIBILITY OF SUCH DAMAGE. + *) structure Elaborate :> ELABORATE = struct @@ -1603,21 +1603,21 @@ fun elabExp (env, denv) (eAll as (e, loc)) = ((L'.EField (e', c', {field = ft, rest = rest}), loc), ft, gs1 @ enD gs2 @ enD gs3 @ enD gs4) end - | L.EWith (e1, c, e2) => + | L.EConcat (e1, e2) => let val (e1', e1t, gs1) = elabExp (env, denv) e1 - val (c', ck, gs2) = elabCon (env, denv) c - val (e2', e2t, gs3) = elabExp (env, denv) e2 + val (e2', e2t, gs2) = elabExp (env, denv) e2 - val rest = cunif (loc, ktype_record) - val first = (L'.CRecord (ktype, [(c', e2t)]), loc) + val r1 = cunif (loc, ktype_record) + val r2 = cunif (loc, ktype_record) - val gs4 = checkCon (env, denv) e1' e1t (L'.TRecord rest, loc) - val gs5 = D.prove env denv (first, rest, loc) + val gs3 = checkCon (env, denv) e1' e1t (L'.TRecord r1, loc) + val gs4 = checkCon (env, denv) e2' e2t (L'.TRecord r2, loc) + val gs5 = D.prove env denv (r1, r2, loc) in - ((L'.EWith (e1', c', e2', {field = e2t, rest = rest}), loc), - (L'.TRecord ((L'.CConcat (first, rest), loc)), loc), - gs1 @ enD gs2 @ gs3 @ enD gs4 @ enD gs5) + ((L'.EConcat (e1', r1, e2', r2), loc), + (L'.TRecord ((L'.CConcat (r1, r2), loc)), loc), + gs1 @ gs2 @ enD gs3 @ enD gs4 @ enD gs5) end | L.ECut (e, c) => let diff --git a/src/expl.sml b/src/expl.sml index 9e35d674..2e96db54 100644 --- a/src/expl.sml +++ b/src/expl.sml @@ -90,7 +90,7 @@ datatype exp' = | ERecord of (con * exp * con) list | EField of exp * con * { field : con, rest : con } - | EWith of exp * con * exp * { field : con, rest : con } + | EConcat of exp * con * exp * con | ECut of exp * con * { field : con, rest : con } | EFold of kind diff --git a/src/expl_print.sml b/src/expl_print.sml index 39df4e3f..d19edeae 100644 --- a/src/expl_print.sml +++ b/src/expl_print.sml @@ -289,31 +289,26 @@ fun p_exp' par env (e, loc) = box [p_exp' true env e, string ".", p_con' true env c] - | EWith (e1, c, e2, {field, rest}) => + | EConcat (e1, c1, e2, c2) => parenIf par (if !debug then - box [p_exp env e1, + box [p_exp' true env e1, space, - string "with", + string ":", space, - p_con' true env c, + p_con env c1, + space, + string "++", space, - string "=", p_exp' true env e2, space, - string "[", - p_con env field, + string ":", space, - string " in ", - space, - p_con env rest, - string "]"] + p_con env c2] else - box [p_exp env e1, + box [p_exp' true env e1, space, string "with", space, - p_con' true env c, - space, p_exp' true env e2]) | ECut (e, c, {field, rest}) => parenIf par (if !debug then diff --git a/src/expl_util.sml b/src/expl_util.sml index 8dec2687..bda602d3 100644 --- a/src/expl_util.sml +++ b/src/expl_util.sml @@ -282,19 +282,17 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, bind} = S.map2 (mfc ctx rest, fn rest' => (EField (e', c', {field = field', rest = rest'}), loc))))) - | EWith (e1, c, e2, {field, rest}) => + | EConcat (e1, c1, e2, c2) => S.bind2 (mfe ctx e1, fn e1' => - S.bind2 (mfc ctx c, - fn c' => + S.bind2 (mfc ctx c1, + fn c1' => S.bind2 (mfe ctx e2, fn e2' => - S.bind2 (mfc ctx field, - fn field' => - S.map2 (mfc ctx rest, - fn rest' => - (EWith (e1', c', e2', {field = field', rest = rest'}), - loc)))))) + S.map2 (mfc ctx c2, + fn c2' => + (EConcat (e1', c1', e2', c2'), + loc))))) | ECut (e, c, {field, rest}) => S.bind2 (mfe ctx e, fn e' => diff --git a/src/explify.sml b/src/explify.sml index 72531d7a..1bca49c3 100644 --- a/src/explify.sml +++ b/src/explify.sml @@ -101,8 +101,8 @@ fun explifyExp (e, loc) = | L.ERecord xes => (L'.ERecord (map (fn (c, e, t) => (explifyCon c, explifyExp e, explifyCon t)) xes), loc) | L.EField (e1, c, {field, rest}) => (L'.EField (explifyExp e1, explifyCon c, {field = explifyCon field, rest = explifyCon rest}), loc) - | L.EWith (e1, c, e2, {field, rest}) => (L'.EWith (explifyExp e1, explifyCon c, explifyExp e2, - {field = explifyCon field, rest = explifyCon rest}), loc) + | L.EConcat (e1, c1, e2, c2) => (L'.EConcat (explifyExp e1, explifyCon c1, explifyExp e2, explifyCon c2), + loc) | L.ECut (e1, c, {field, rest}) => (L'.ECut (explifyExp e1, explifyCon c, {field = explifyCon field, rest = explifyCon rest}), loc) | L.EFold k => (L'.EFold (explifyKind k), loc) diff --git a/src/monoize.sml b/src/monoize.sml index df775554..17e28034 100644 --- a/src/monoize.sml +++ b/src/monoize.sml @@ -1920,7 +1920,7 @@ fun monoExp (env, st, fm) (all as (e, loc)) = in ((L'.EField (e, monoName env x), loc), fm) end - | L.EWith _ => poly () + | L.EConcat _ => poly () | L.ECut _ => poly () | L.EFold _ => poly () diff --git a/src/reduce.sml b/src/reduce.sml index 8dc4527f..1404b598 100644 --- a/src/reduce.sml +++ b/src/reduce.sml @@ -107,18 +107,18 @@ fun exp env e = | _ => false) xes of SOME (_, e, _) => #1 e | NONE => e) - | EWith (r as (_, loc), x, e, {rest = (CRecord (k, xts), _), field}) => + | EConcat (r1 as (_, loc), (CRecord (k, xts1), _), r2, (CRecord (_, xts2), _)) => let - fun fields (remaining, passed) = + fun fields (r, remaining, passed) = case remaining of [] => [] | (x, t) :: rest => (x, (EField (r, x, {field = t, rest = (CRecord (k, List.revAppend (passed, rest)), loc)}), loc), - t) :: fields (rest, (x, t) :: passed) + t) :: fields (r, rest, (x, t) :: passed) in - #1 (reduceExp env (ERecord ((x, e, field) :: fields (xts, [])), loc)) + #1 (reduceExp env (ERecord (fields (r1, xts1, []) @ fields (r2, xts2, [])), loc)) end | ECut (r as (_, loc), _, {rest = (CRecord (k, xts), _), ...}) => let diff --git a/src/source.sml b/src/source.sml index 23d2089f..386b1a83 100644 --- a/src/source.sml +++ b/src/source.sml @@ -123,7 +123,7 @@ datatype exp' = | ERecord of (con * exp) list | EField of exp * con - | EWith of exp * con * exp + | EConcat of exp * exp | ECut of exp * con | EFold diff --git a/src/source_print.sml b/src/source_print.sml index f9fc8a53..a25be2d4 100644 --- a/src/source_print.sml +++ b/src/source_print.sml @@ -258,13 +258,11 @@ fun p_exp' par (e, _) = | EField (e, c) => box [p_exp' true e, string ".", p_con' true c] - | EWith (e1, c, e2) => parenIf par (box [p_exp e1, - space, - string "with", - space, - p_con' true c, - space, - p_exp' true e2]) + | EConcat (e1, e2) => parenIf par (box [p_exp' true e1, + space, + string "++", + space, + p_exp' true e2]) | ECut (e, c) => parenIf par (box [p_exp' true e, space, string "--", diff --git a/src/termination.sml b/src/termination.sml index 1bae7592..b0716eca 100644 --- a/src/termination.sml +++ b/src/termination.sml @@ -265,7 +265,7 @@ fun declOk' env (d, loc) = in (Rabble, calls) end - | EWith (e1, _, e2, _) => + | EConcat (e1, _, e2, _) => let val (_, calls) = exp parent (penv, calls) e1 val (_, calls) = exp parent (penv, calls) e2 diff --git a/src/urweb.grm b/src/urweb.grm index 3f56cb94..143b6935 100644 --- a/src/urweb.grm +++ b/src/urweb.grm @@ -198,7 +198,7 @@ fun tagIn bt = | TYPE | NAME | ARROW | LARROW | DARROW | STAR | SEMI | FN | PLUSPLUS | MINUSMINUS | DOLLAR | TWIDDLE - | STRUCTURE | SIGNATURE | STRUCT | SIG | END | FUNCTOR | WHERE | EXTERN | WITH | SQL + | STRUCTURE | SIGNATURE | STRUCT | SIG | END | FUNCTOR | WHERE | EXTERN | SQL | INCLUDE | OPEN | CONSTRAINT | CONSTRAINTS | EXPORT | TABLE | SEQUENCE | CASE | IF | THEN | ELSE @@ -344,7 +344,6 @@ fun tagIn bt = %right CAND %nonassoc EQ NE LT LE GT GE %right ARROW -%left WITH %right PLUSPLUS MINUSMINUS %left PLUS MINUS %left STAR DIVIDE MOD @@ -699,7 +698,7 @@ eexp : eapps (eapps) | eexp GT eexp (native_op ("gt", eexp1, eexp2, s (eexp1left, eexp2right))) | eexp GE eexp (native_op ("ge", eexp1, eexp2, s (eexp1left, eexp2right))) - | eexp WITH cterm EQ eexp (EWith (eexp1, cterm, eexp2), s (eexp1left, eexp2right)) + | eexp PLUSPLUS eexp (EConcat (eexp1, eexp2), s (eexp1left, eexp2right)) bind : SYMBOL LARROW eapps (SYMBOL, NONE, eapps) | UNIT LARROW eapps (let diff --git a/src/urweb.lex b/src/urweb.lex index fc8db17f..cc0f5b7c 100644 --- a/src/urweb.lex +++ b/src/urweb.lex @@ -311,7 +311,6 @@ notags = [^<{\n]+; "table" => (Tokens.TABLE (pos yypos, pos yypos + size yytext)); "sequence" => (Tokens.SEQUENCE (pos yypos, pos yypos + size yytext)); "class" => (Tokens.CLASS (pos yypos, pos yypos + size yytext)); - "with" => (Tokens.WITH (pos yypos, pos yypos + size yytext)); "Type" => (Tokens.TYPE (pos yypos, pos yypos + size yytext)); "Name" => (Tokens.NAME (pos yypos, pos yypos + size yytext)); -- cgit v1.2.3 From 887af944c67e3395679a750a205ef114234c61a0 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Tue, 11 Nov 2008 19:20:37 -0500 Subject: Add CutMulti --- include/urweb.h | 1 + src/c/urweb.c | 7 ++++++ src/cjr_print.sml | 2 +- src/core.sml | 1 + src/core_print.sml | 17 +++++++++++++ src/core_util.sml | 16 ++++++++++++- src/corify.sml | 2 ++ src/elab.sml | 1 + src/elab_print.sml | 18 ++++++++++++++ src/elab_util.sml | 9 +++++++ src/elaborate.sml | 67 +++++++++++++++++++++++++++++++++++++++++++++------- src/expl.sml | 1 + src/expl_print.sml | 17 +++++++++++++ src/expl_util.sml | 8 +++++++ src/explify.sml | 2 ++ src/monoize.sml | 1 + src/reduce.sml | 13 ++++++++++ src/source.sml | 1 + src/source_print.sml | 5 ++++ src/termination.sml | 6 +++++ src/urweb.grm | 5 ++-- src/urweb.lex | 1 + tests/cut.ur | 7 +++--- tests/cut.urp | 3 +++ 24 files changed, 195 insertions(+), 16 deletions(-) create mode 100644 tests/cut.urp (limited to 'src/reduce.sml') diff --git a/include/urweb.h b/include/urweb.h index d148654f..ad08c811 100644 --- a/include/urweb.h +++ b/include/urweb.h @@ -75,6 +75,7 @@ uw_Basis_time uw_Basis_unurlifyTime(uw_context, char **); uw_Basis_string uw_Basis_strcat(uw_context, uw_Basis_string, uw_Basis_string); uw_Basis_string uw_Basis_strdup(uw_context, uw_Basis_string); +uw_Basis_string uw_Basis_maybe_strdup(uw_context, uw_Basis_string); uw_Basis_string uw_Basis_sqlifyInt(uw_context, uw_Basis_int); uw_Basis_string uw_Basis_sqlifyFloat(uw_context, uw_Basis_float); diff --git a/src/c/urweb.c b/src/c/urweb.c index a347dd45..253cda87 100644 --- a/src/c/urweb.c +++ b/src/c/urweb.c @@ -869,6 +869,13 @@ uw_Basis_string uw_Basis_strdup(uw_context ctx, uw_Basis_string s1) { return s; } +uw_Basis_string uw_Basis_maybe_strdup(uw_context ctx, uw_Basis_string s1) { + if (s1) + return uw_Basis_strdup(ctx, s1); + else + return NULL; +} + char *uw_Basis_sqlifyInt(uw_context ctx, uw_Basis_int n) { int len; diff --git a/src/cjr_print.sml b/src/cjr_print.sml index 1c750b33..8c3c3d86 100644 --- a/src/cjr_print.sml +++ b/src/cjr_print.sml @@ -1481,7 +1481,7 @@ fun p_exp' par env (e, loc) = in box [string "({", newline, - string "uw_Basis_string request = uw_Basis_strdup(ctx, ", + string "uw_Basis_string request = uw_Basis_maybe_strdup(ctx, ", p_exp env e, string ");", newline, diff --git a/src/core.sml b/src/core.sml index 1a181a68..4623bb49 100644 --- a/src/core.sml +++ b/src/core.sml @@ -95,6 +95,7 @@ datatype exp' = | EField of exp * con * { field : con, rest : con } | EConcat of exp * con * exp * con | ECut of exp * con * { field : con, rest : con } + | ECutMulti of exp * con * { rest : con } | EFold of kind | ECase of exp * (pat * exp) list * { disc : con, result : con } diff --git a/src/core_print.sml b/src/core_print.sml index f209b84f..53922936 100644 --- a/src/core_print.sml +++ b/src/core_print.sml @@ -325,6 +325,23 @@ fun p_exp' par env (e, _) = string "--", space, p_con' true env c]) + | ECutMulti (e, c, {rest}) => + parenIf par (if !debug then + box [p_exp' true env e, + space, + string "---", + space, + p_con' true env c, + space, + string "[", + p_con env rest, + string "]"] + else + box [p_exp' true env e, + space, + string "---", + space, + p_con' true env c]) | EFold _ => string "fold" | ECase (e, pes, {disc, result}) => diff --git a/src/core_util.sml b/src/core_util.sml index 38004f74..71efe16e 100644 --- a/src/core_util.sml +++ b/src/core_util.sml @@ -444,10 +444,16 @@ fun compare ((e1, _), (e2, _)) = | (ECut (e1, c1, _), ECut (e2, c2, _)) => join (compare (e1, e2), - fn () => Con.compare (c1, c2)) + fn () => Con.compare (c1, c2)) | (ECut _, _) => LESS | (_, ECut _) => GREATER + | (ECutMulti (e1, c1, _), ECutMulti (e2, c2, _)) => + join (compare (e1, e2), + fn () => Con.compare (c1, c2)) + | (ECutMulti _, _) => LESS + | (_, ECutMulti _) => GREATER + | (EFold _, EFold _) => EQUAL | (EFold _, _) => LESS | (_, EFold _) => GREATER @@ -588,6 +594,14 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, bind} = S.map2 (mfc ctx rest, fn rest' => (ECut (e', c', {field = field', rest = rest'}), loc))))) + | ECutMulti (e, c, {rest}) => + S.bind2 (mfe ctx e, + fn e' => + S.bind2 (mfc ctx c, + fn c' => + S.map2 (mfc ctx rest, + fn rest' => + (ECutMulti (e', c', {rest = rest'}), loc)))) | EFold k => S.map2 (mfk k, fn k' => diff --git a/src/corify.sml b/src/corify.sml index fdb4e7b7..8bb1a925 100644 --- a/src/corify.sml +++ b/src/corify.sml @@ -590,6 +590,8 @@ fun corifyExp st (e, loc) = corifyCon st c2), loc) | L.ECut (e1, c, {field, rest}) => (L'.ECut (corifyExp st e1, corifyCon st c, {field = corifyCon st field, rest = corifyCon st rest}), loc) + | L.ECutMulti (e1, c, {rest}) => (L'.ECutMulti (corifyExp st e1, corifyCon st c, + {rest = corifyCon st rest}), loc) | L.EFold k => (L'.EFold (corifyKind k), loc) | L.ECase (e, pes, {disc, result}) => diff --git a/src/elab.sml b/src/elab.sml index d00d1f1a..d997b7ec 100644 --- a/src/elab.sml +++ b/src/elab.sml @@ -110,6 +110,7 @@ datatype exp' = | EField of exp * con * { field : con, rest : con } | EConcat of exp * con * exp * con | ECut of exp * con * { field : con, rest : con } + | ECutMulti of exp * con * { rest : con } | EFold of kind | ECase of exp * (pat * exp) list * { disc : con, result : con } diff --git a/src/elab_print.sml b/src/elab_print.sml index 2afedef1..62b1ea02 100644 --- a/src/elab_print.sml +++ b/src/elab_print.sml @@ -359,6 +359,24 @@ fun p_exp' par env (e, _) = string "--", space, p_con' true env c]) + | ECutMulti (e, c, {rest}) => + parenIf par (if !debug then + box [p_exp' true env e, + space, + string "---", + space, + p_con' true env c, + space, + string "[", + p_con env rest, + string "]"] + else + box [p_exp' true env e, + space, + string "---", + space, + p_con' true env c]) + | EFold _ => string "fold" | ECase (e, pes, _) => parenIf par (box [string "case", diff --git a/src/elab_util.sml b/src/elab_util.sml index 9c25ae86..6e2c76f6 100644 --- a/src/elab_util.sml +++ b/src/elab_util.sml @@ -338,6 +338,15 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, bind} = fn rest' => (ECut (e', c', {field = field', rest = rest'}), loc))))) + | ECutMulti (e, c, {rest}) => + S.bind2 (mfe ctx e, + fn e' => + S.bind2 (mfc ctx c, + fn c' => + S.map2 (mfc ctx rest, + fn rest' => + (ECutMulti (e', c', {rest = rest'}), loc)))) + | EFold k => S.map2 (mfk k, fn k' => diff --git a/src/elaborate.sml b/src/elaborate.sml index 70429c1b..e3d334eb 100644 --- a/src/elaborate.sml +++ b/src/elaborate.sml @@ -1664,6 +1664,21 @@ fun elabExp (env, denv) (eAll as (e, loc)) = ((L'.ECut (e', c', {field = ft, rest = rest}), loc), (L'.TRecord rest, loc), gs1 @ enD gs2 @ enD gs3 @ enD gs4) end + | L.ECutMulti (e, c) => + let + val (e', et, gs1) = elabExp (env, denv) e + val (c', ck, gs2) = elabCon (env, denv) c + + val rest = cunif (loc, ktype_record) + + val gs3 = + checkCon (env, denv) e' et + (L'.TRecord (L'.CConcat (c', rest), loc), loc) + val gs4 = D.prove env denv (c', rest, loc) + in + ((L'.ECutMulti (e', c', {rest = rest}), loc), (L'.TRecord rest, loc), + gs1 @ enD gs2 @ enD gs3 @ enD gs4) + end | L.EFold => let @@ -2694,6 +2709,33 @@ fun wildifyStr env (str, sgn) = (case #1 str of L.StrConst ds => let + fun decompileKind (k, loc) = + case k of + L'.KType => SOME (L.KType, loc) + | L'.KArrow (k1, k2) => + (case (decompileKind k1, decompileKind k2) of + (SOME k1, SOME k2) => SOME (L.KArrow (k1, k2), loc) + | _ => NONE) + | L'.KName => SOME (L.KName, loc) + | L'.KRecord k => + (case decompileKind k of + SOME k => SOME (L.KRecord k, loc) + | _ => NONE) + | L'.KUnit => SOME (L.KUnit, loc) + | L'.KTuple ks => + let + val ks' = List.mapPartial decompileKind ks + in + if length ks' = length ks then + SOME (L.KTuple ks', loc) + else + NONE + end + + | L'.KError => NONE + | L'.KUnif (_, _, ref (SOME k)) => decompileKind k + | L'.KUnif _ => NONE + fun decompileCon env (c, loc) = case c of L'.CRel i => @@ -2741,7 +2783,7 @@ fun wildifyStr env (str, sgn) = let val (needed, constraints, neededV) = case sgi of - L'.SgiConAbs (x, _, _) => (SS.add (neededC, x), constraints, neededV) + L'.SgiConAbs (x, _, k) => (SM.insert (neededC, x, k), constraints, neededV) | L'.SgiConstraint cs => (neededC, (env', cs, loc) :: constraints, neededV) | L'.SgiVal (x, _, t) => @@ -2764,18 +2806,18 @@ fun wildifyStr env (str, sgn) = in (needed, constraints, neededV, E.sgiBinds env' (sgi, loc)) end) - (SS.empty, [], SS.empty, env) sgis + (SM.empty, [], SS.empty, env) sgis val (neededC, neededV) = foldl (fn ((d, _), needed as (neededC, neededV)) => case d of - L.DCon (x, _, _) => ((SS.delete (neededC, x), neededV) + L.DCon (x, _, _) => ((#1 (SM.remove (neededC, x)), neededV) handle NotFound => needed) - | L.DClass (x, _) => ((SS.delete (neededC, x), neededV) + | L.DClass (x, _) => ((#1 (SM.remove (neededC, x)), neededV) handle NotFound => needed) | L.DVal (x, _, _) => ((neededC, SS.delete (neededV, x)) handle NotFound => needed) - | L.DOpen _ => (SS.empty, SS.empty) + | L.DOpen _ => (SM.empty, SS.empty) | _ => needed) (neededC, neededV) ds @@ -2797,13 +2839,20 @@ fun wildifyStr env (str, sgn) = end val ds' = - case SS.listItems neededC of + case SM.listItemsi neededC of [] => ds' | xs => let - val kwild = (L.KWild, #2 str) - val cwild = (L.CWild kwild, #2 str) - val ds'' = map (fn x => (L.DCon (x, NONE, cwild), #2 str)) xs + val ds'' = map (fn (x, k) => + let + val k = + case decompileKind k of + NONE => (L.KWild, #2 str) + | SOME k => k + val cwild = (L.CWild k, #2 str) + in + (L.DCon (x, NONE, cwild), #2 str) + end) xs in ds'' @ ds' end diff --git a/src/expl.sml b/src/expl.sml index 57396684..cce0fc22 100644 --- a/src/expl.sml +++ b/src/expl.sml @@ -92,6 +92,7 @@ datatype exp' = | EField of exp * con * { field : con, rest : con } | EConcat of exp * con * exp * con | ECut of exp * con * { field : con, rest : con } + | ECutMulti of exp * con * { rest : con } | EFold of kind | ECase of exp * (pat * exp) list * { disc : con, result : con } diff --git a/src/expl_print.sml b/src/expl_print.sml index e3153ef2..2ce0c5e2 100644 --- a/src/expl_print.sml +++ b/src/expl_print.sml @@ -334,6 +334,23 @@ fun p_exp' par env (e, loc) = string "--", space, p_con' true env c]) + | ECutMulti (e, c, {rest}) => + parenIf par (if !debug then + box [p_exp' true env e, + space, + string "---", + space, + p_con' true env c, + space, + string "[", + p_con env rest, + string "]"] + else + box [p_exp' true env e, + space, + string "---", + space, + p_con' true env c]) | EFold _ => string "fold" | EWrite e => box [string "write(", diff --git a/src/expl_util.sml b/src/expl_util.sml index 2bd9eabd..d2073a23 100644 --- a/src/expl_util.sml +++ b/src/expl_util.sml @@ -303,6 +303,14 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, bind} = S.map2 (mfc ctx rest, fn rest' => (ECut (e', c', {field = field', rest = rest'}), loc))))) + | ECutMulti (e, c, {rest}) => + S.bind2 (mfe ctx e, + fn e' => + S.bind2 (mfc ctx c, + fn c' => + S.map2 (mfc ctx rest, + fn rest' => + (ECutMulti (e', c', {rest = rest'}), loc)))) | EFold k => S.map2 (mfk k, fn k' => diff --git a/src/explify.sml b/src/explify.sml index 4115476b..e3c22f20 100644 --- a/src/explify.sml +++ b/src/explify.sml @@ -105,6 +105,8 @@ fun explifyExp (e, loc) = loc) | L.ECut (e1, c, {field, rest}) => (L'.ECut (explifyExp e1, explifyCon c, {field = explifyCon field, rest = explifyCon rest}), loc) + | L.ECutMulti (e1, c, {rest}) => (L'.ECutMulti (explifyExp e1, explifyCon c, + {rest = explifyCon rest}), loc) | L.EFold k => (L'.EFold (explifyKind k), loc) | L.ECase (e, pes, {disc, result}) => diff --git a/src/monoize.sml b/src/monoize.sml index a4f38dc6..28ea5946 100644 --- a/src/monoize.sml +++ b/src/monoize.sml @@ -2014,6 +2014,7 @@ fun monoExp (env, st, fm) (all as (e, loc)) = end | L.EConcat _ => poly () | L.ECut _ => poly () + | L.ECutMulti _ => poly () | L.EFold _ => poly () | L.ECase (e, pes, {disc, result}) => diff --git a/src/reduce.sml b/src/reduce.sml index 1404b598..e480dea2 100644 --- a/src/reduce.sml +++ b/src/reduce.sml @@ -133,6 +133,19 @@ fun exp env e = in #1 (reduceExp env (ERecord (fields (xts, [])), loc)) end + | ECutMulti (r as (_, loc), _, {rest = (CRecord (k, xts), _), ...}) => + let + fun fields (remaining, passed) = + case remaining of + [] => [] + | (x, t) :: rest => + (x, + (EField (r, x, {field = t, + rest = (CRecord (k, List.revAppend (passed, rest)), loc)}), loc), + t) :: fields (rest, (x, t) :: passed) + in + #1 (reduceExp env (ERecord (fields (xts, [])), loc)) + end | _ => e in diff --git a/src/source.sml b/src/source.sml index 2a348338..7685bb2f 100644 --- a/src/source.sml +++ b/src/source.sml @@ -123,6 +123,7 @@ datatype exp' = | EField of exp * con | EConcat of exp * exp | ECut of exp * con + | ECutMulti of exp * con | EFold | EWild diff --git a/src/source_print.sml b/src/source_print.sml index 3c26812f..77f2d749 100644 --- a/src/source_print.sml +++ b/src/source_print.sml @@ -268,6 +268,11 @@ fun p_exp' par (e, _) = string "--", space, p_con' true c]) + | ECutMulti (e, c) => parenIf par (box [p_exp' true e, + space, + string "---", + space, + p_con' true c]) | EFold => string "fold" | ECase (e, pes) => parenIf par (box [string "case", diff --git a/src/termination.sml b/src/termination.sml index 2db5bb11..e89f329e 100644 --- a/src/termination.sml +++ b/src/termination.sml @@ -265,6 +265,12 @@ fun declOk' env (d, loc) = in (Rabble, calls) end + | ECutMulti (e, _, _) => + let + val (_, calls) = exp parent (penv, calls) e + in + (Rabble, calls) + end | EConcat (e1, _, e2, _) => let val (_, calls) = exp parent (penv, calls) e1 diff --git a/src/urweb.grm b/src/urweb.grm index 5241ed20..8a3bee7f 100644 --- a/src/urweb.grm +++ b/src/urweb.grm @@ -197,7 +197,7 @@ fun tagIn bt = | DATATYPE | OF | TYPE | NAME | ARROW | LARROW | DARROW | STAR | SEMI - | FN | PLUSPLUS | MINUSMINUS | DOLLAR | TWIDDLE + | FN | PLUSPLUS | MINUSMINUS | MINUSMINUSMINUS | DOLLAR | TWIDDLE | LET | IN | STRUCTURE | SIGNATURE | STRUCT | SIG | END | FUNCTOR | WHERE | EXTERN | SQL | INCLUDE | OPEN | CONSTRAINT | CONSTRAINTS | EXPORT | TABLE | SEQUENCE @@ -348,7 +348,7 @@ fun tagIn bt = %right CAND %nonassoc EQ NE LT LE GT GE IS %right ARROW -%right PLUSPLUS MINUSMINUS +%right PLUSPLUS MINUSMINUS MINUSMINUSMINUS %left PLUS MINUS %left STAR DIVIDE MOD %left NOT @@ -692,6 +692,7 @@ eexp : eapps (eapps) end) | eexp COLON cexp (EAnnot (eexp, cexp), s (eexpleft, cexpright)) | eexp MINUSMINUS cexp (ECut (eexp, cexp), s (eexpleft, cexpright)) + | eexp MINUSMINUSMINUS cexp (ECutMulti (eexp, cexp), s (eexpleft, cexpright)) | CASE eexp OF barOpt branch branchs (ECase (eexp, branch :: branchs), s (CASEleft, branchsright)) | IF eexp THEN eexp ELSE eexp (let val loc = s (IFleft, eexp3right) diff --git a/src/urweb.lex b/src/urweb.lex index 642282ec..aef68ad1 100644 --- a/src/urweb.lex +++ b/src/urweb.lex @@ -251,6 +251,7 @@ notags = [^<{\n]+; "=>" => (Tokens.DARROW (pos yypos, pos yypos + size yytext)); "++" => (Tokens.PLUSPLUS (pos yypos, pos yypos + size yytext)); "--" => (Tokens.MINUSMINUS (pos yypos, pos yypos + size yytext)); + "---" => (Tokens.MINUSMINUSMINUS (pos yypos, pos yypos + size yytext)); "=" => (Tokens.EQ (pos yypos, pos yypos + size yytext)); "<>" => (Tokens.NE (pos yypos, pos yypos + size yytext)); diff --git a/tests/cut.ur b/tests/cut.ur index 6b7b4ef3..7d0ee77a 100644 --- a/tests/cut.ur +++ b/tests/cut.ur @@ -1,6 +1,7 @@ val r = {A = 1, B = "Hi", C = 0.0} val rA = r -- #A +val rB = r --- [A = _, C = _] -val main : unit -> page = fn () => - {cdata rA.B} - +fun main () : transaction page = return + {cdata rA.B}, {cdata rB.B} + diff --git a/tests/cut.urp b/tests/cut.urp new file mode 100644 index 00000000..5c9c3e81 --- /dev/null +++ b/tests/cut.urp @@ -0,0 +1,3 @@ +debug + +cut -- cgit v1.2.3 From 125bd1380f059c9ee3541df4cbf0e12e2b6dcc70 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Wed, 26 Nov 2008 12:13:00 -0500 Subject: Start of new Reduce --- src/reduce.sml | 274 ++++++++++++++++++++++++++++----------------------------- 1 file changed, 133 insertions(+), 141 deletions(-) (limited to 'src/reduce.sml') diff --git a/src/reduce.sml b/src/reduce.sml index e480dea2..7531e0ca 100644 --- a/src/reduce.sml +++ b/src/reduce.sml @@ -31,150 +31,142 @@ structure Reduce :> REDUCE = struct open Core -structure E = CoreEnv -structure U = CoreUtil - -val liftConInCon = E.liftConInCon -val subConInCon = E.subConInCon -val liftConInExp = E.liftConInExp -val liftExpInExp = E.liftExpInExp -val subExpInExp = E.subExpInExp -val liftConInExp = E.liftConInExp -val subConInExp = E.subConInExp - -fun bindC (env, b) = - case b of - U.Con.Rel (x, k) => E.pushCRel env x k - | U.Con.Named (x, n, k, co) => E.pushCNamed env x n k co - -fun bind (env, b) = - case b of - U.Decl.RelC (x, k) => E.pushCRel env x k - | U.Decl.NamedC (x, n, k, co) => E.pushCNamed env x n k co - | U.Decl.RelE (x, t) => E.pushERel env x t - | U.Decl.NamedE (x, n, t, eo, s) => E.pushENamed env x n t eo s - -fun kind k = k - -fun con env c = - case c of - CApp ((CApp ((CApp ((CFold ks, _), f), _), i), loc), (CRecord (k, xcs), _)) => - (case xcs of - [] => #1 i - | (n, v) :: rest => - #1 (reduceCon env (CApp ((CApp ((CApp (f, n), loc), v), loc), - (CApp ((CApp ((CApp ((CFold ks, loc), f), loc), i), loc), - (CRecord (k, rest), loc)), loc)), loc))) - | CApp ((CAbs (_, _, c1), loc), c2) => - #1 (reduceCon env (subConInCon (0, c2) c1)) - | CNamed n => - (case E.lookupCNamed env n of - (_, _, SOME c') => #1 c' - | _ => c) - | CConcat ((CRecord (k, xcs1), loc), (CRecord (_, xcs2), _)) => CRecord (k, xcs1 @ xcs2) - - | CProj ((CTuple cs, _), n) => #1 (List.nth (cs, n - 1)) - - | _ => c - -and reduceCon env = U.Con.mapB {kind = kind, con = con, bind = bindC} env - -fun exp env e = +structure IM = IntBinaryMap + +datatype env_item = + UnknownC + | KnownC of con + + | UnknownE + | KnownE of exp + + | Lift of int * int + +type env = env_item list + +fun conAndExp (namedC, namedE) = let - (*val () = Print.prefaces "exp" [("e", CorePrint.p_exp env (e, ErrorMsg.dummySpan))]*) - - val r = case e of - ENamed n => - (case E.lookupENamed env n of - (_, _, SOME e', _) => #1 e' - | _ => e) - - | ECApp ((EApp ((EApp ((ECApp ((EFold ks, _), ran), _), f), _), i), _), (CRecord (k, xcs), loc)) => - (case xcs of - [] => #1 i - | (n, v) :: rest => - #1 (reduceExp env (EApp ((ECApp ((ECApp ((ECApp (f, n), loc), v), loc), (CRecord (k, rest), loc)), loc), - (ECApp ((EApp ((EApp ((ECApp ((EFold ks, loc), ran), loc), f), loc), i), loc), - (CRecord (k, rest), loc)), loc)), loc))) - - | EApp ((EAbs (_, _, _, e1), loc), e2) => - #1 (reduceExp env (subExpInExp (0, e2) e1)) - | ECApp ((ECAbs (_, _, e1), loc), c) => - #1 (reduceExp env (subConInExp (0, c) e1)) - - | EField ((ERecord xes, _), (CName x, _), _) => - (case List.find (fn ((CName x', _), _, _) => x' = x - | _ => false) xes of - SOME (_, e, _) => #1 e - | NONE => e) - | EConcat (r1 as (_, loc), (CRecord (k, xts1), _), r2, (CRecord (_, xts2), _)) => - let - fun fields (r, remaining, passed) = - case remaining of - [] => [] - | (x, t) :: rest => - (x, - (EField (r, x, {field = t, - rest = (CRecord (k, List.revAppend (passed, rest)), loc)}), loc), - t) :: fields (r, rest, (x, t) :: passed) - in - #1 (reduceExp env (ERecord (fields (r1, xts1, []) @ fields (r2, xts2, [])), loc)) - end - | ECut (r as (_, loc), _, {rest = (CRecord (k, xts), _), ...}) => - let - fun fields (remaining, passed) = - case remaining of - [] => [] - | (x, t) :: rest => - (x, - (EField (r, x, {field = t, - rest = (CRecord (k, List.revAppend (passed, rest)), loc)}), loc), - t) :: fields (rest, (x, t) :: passed) - in - #1 (reduceExp env (ERecord (fields (xts, [])), loc)) - end - | ECutMulti (r as (_, loc), _, {rest = (CRecord (k, xts), _), ...}) => - let - fun fields (remaining, passed) = - case remaining of - [] => [] - | (x, t) :: rest => - (x, - (EField (r, x, {field = t, - rest = (CRecord (k, List.revAppend (passed, rest)), loc)}), loc), - t) :: fields (rest, (x, t) :: passed) - in - #1 (reduceExp env (ERecord (fields (xts, [])), loc)) - end - - | _ => e + fun con env (all as (c, loc)) = + case c of + TFun (c1, c2) => (TFun (con env c1, con env c2), loc) + | TCFun (x, k, c2) => (TCFun (x, k, con (UnknownC :: env) c2), loc) + | TRecord c => (TRecord (con env c), loc) + + | CRel n => + let + fun find (n', env, lift) = + if n' = 0 then + case env of + UnknownC :: _ => (CRel (n + lift), loc) + | KnownC c :: _ => con (Lift (lift, 0) :: env) c + | _ => raise Fail "Reduce.con: CRel [1]" + else + case env of + UnknownC :: rest => find (n' - 1, rest, lift + 1) + | KnownC _ :: rest => find (n' - 1, rest, lift) + | UnknownE :: rest => find (n' - 1, rest, lift) + | KnownE _ :: rest => find (n' - 1, rest, lift) + | Lift (lift', _) :: rest => find (n' - 1, rest, lift + lift') + | [] => raise Fail "Reduce.con: CRel [2]" + in + find (n, env, 0) + end + | CNamed n => + (case IM.find (namedC, n) of + NONE => all + | SOME c => c) + | CFfi _ => all + | CApp (c1, c2) => + let + val c1 = con env c1 + val c2 = con env c2 + in + case #1 c1 of + CAbs (_, _, b) => + con (KnownC c2 :: env) b + + | CApp ((CApp (fold as (CFold _, _), f), _), i) => + (case #1 c2 of + CRecord (_, []) => i + | CRecord (k, (x, c) :: rest) => + con env (CApp ((CApp ((CApp (f, x), loc), c), loc), + (CApp ((CApp ((CApp (fold, f), loc), i), loc), + (CRecord (k, rest), loc)), loc)), loc) + | _ => (CApp (c1, c2), loc)) + + | _ => (CApp (c1, c2), loc) + end + | CAbs (x, k, b) => (CAbs (x, k, con (UnknownC :: env) b), loc) + + | CName _ => all + + | CRecord (k, xcs) => (CRecord (k, map (fn (x, c) => (con env x, con env c)) xcs), loc) + | CConcat (c1, c2) => + let + val c1 = con env c1 + val c2 = con env c2 + in + case (#1 c1, #1 c2) of + (CRecord (k, xcs1), CRecord (_, xcs2)) => + (CRecord (k, xcs1 @ xcs2), loc) + | _ => (CConcat (c1, c2), loc) + end + | CFold _ => all + + | CUnit => all + + | CTuple cs => (CTuple (map (con env) cs), loc) + | CProj (c, n) => + let + val c = con env c + in + case #1 c of + CTuple cs => List.nth (cs, n - 1) + | _ => (CProj (c, n), loc) + end + + fun exp env e = e in - (*Print.prefaces "exp'" [("e", CorePrint.p_exp env (e, ErrorMsg.dummySpan)), - ("r", CorePrint.p_exp env (r, ErrorMsg.dummySpan))];*) - - r + {con = con, exp = exp} end -and reduceExp env = U.Exp.mapB {kind = kind, con = con, exp = exp, bind = bind} env - -fun decl env d = - case d of - DValRec [vi as (_, n, _, e, _)] => - let - fun kind _ = false - fun con _ = false - fun exp e = - case e of - ENamed n' => n' = n - | _ => false - in - if U.Exp.exists {kind = kind, con = con, exp = exp} e then - d - else - DVal vi - end - | _ => d - -val reduce = U.File.mapB {kind = kind, con = con, exp = exp, decl = decl, bind = bind} E.empty +fun con namedC c = #con (conAndExp (namedC, IM.empty)) [] c +fun exp (namedC, namedE) e = #exp (conAndExp (namedC, namedE)) [] e + +fun reduce file = + let + fun doDecl (d as (_, loc), st as (namedC, namedE)) = + case #1 d of + DCon (x, n, k, c) => + let + val c = con namedC c + in + ((DCon (x, n, k, c), loc), + (IM.insert (namedC, n, c), namedE)) + end + | DDatatype (x, n, ps, cs) => + ((DDatatype (x, n, ps, map (fn (x, n, co) => (x, n, Option.map (con namedC) co)) cs), loc), + st) + | DVal (x, n, t, e, s) => + let + val t = con namedC t + val e = exp (namedC, namedE) e + in + ((DVal (x, n, t, e, s), loc), + (namedC, IM.insert (namedE, n, e))) + end + | DValRec vis => + ((DValRec (map (fn (x, n, t, e, s) => (x, n, con namedC t, exp (namedC, namedE) e, s)) vis), loc), + st) + | DExport _ => (d, st) + | DTable (s, n, c, s') => ((DTable (s, n, con namedC c, s'), loc), st) + | DSequence _ => (d, st) + | DDatabase _ => (d, st) + | DCookie (s, n, c, s') => ((DCookie (s, n, con namedC c, s'), loc), st) + + val (file, _) = ListUtil.foldlMap doDecl (IM.empty, IM.empty) file + in + file + end end -- cgit v1.2.3 From c767386f0b9d6af9ac3e306f73ea0608cb521c7b Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Wed, 26 Nov 2008 12:59:32 -0500 Subject: Most exp rules for new Reduce --- src/reduce.sml | 231 ++++++++++++++++++++++++++++++++++++++++++++++++++++++--- 1 file changed, 219 insertions(+), 12 deletions(-) (limited to 'src/reduce.sml') diff --git a/src/reduce.sml b/src/reduce.sml index 7531e0ca..3d117fb5 100644 --- a/src/reduce.sml +++ b/src/reduce.sml @@ -59,6 +59,7 @@ fun conAndExp (namedC, namedE) = case env of UnknownC :: _ => (CRel (n + lift), loc) | KnownC c :: _ => con (Lift (lift, 0) :: env) c + | Lift (lift', _) :: rest => find (0, rest, lift + lift') | _ => raise Fail "Reduce.con: CRel [1]" else case env of @@ -66,7 +67,7 @@ fun conAndExp (namedC, namedE) = | KnownC _ :: rest => find (n' - 1, rest, lift) | UnknownE :: rest => find (n' - 1, rest, lift) | KnownE _ :: rest => find (n' - 1, rest, lift) - | Lift (lift', _) :: rest => find (n' - 1, rest, lift + lift') + | Lift (lift', _) :: rest => find (n', rest, lift + lift') | [] => raise Fail "Reduce.con: CRel [2]" in find (n, env, 0) @@ -125,13 +126,215 @@ fun conAndExp (namedC, namedE) = | _ => (CProj (c, n), loc) end - fun exp env e = e + fun patCon pc = + case pc of + PConVar _ => pc + | PConFfi {mod = m, datatyp, params, con = c, arg, kind} => + PConFfi {mod = m, datatyp = datatyp, params = params, con = c, + arg = Option.map (con (map (fn _ => UnknownC) params)) arg, + kind = kind} + + + val k = (KType, ErrorMsg.dummySpan) + fun doPart e (this as (x, t), rest) = + ((x, (EField (e, x, {field = t, rest = (CRecord (k, rest), #2 t)}), #2 t), t), + this :: rest) + + fun exp env (all as (e, loc)) = + case e of + EPrim _ => all + | ERel n => + let + fun find (n', env, liftC, liftE) = + if n' = 0 then + case env of + UnknownE :: _ => (ERel (n + liftE), loc) + | KnownE e :: _ => exp (Lift (liftC, liftE) :: env) e + | Lift (liftC', liftE') :: rest => find (0, rest, liftC + liftC', liftE + liftE') + | _ => raise Fail "Reduce.exp: ERel [1]" + else + case env of + UnknownC :: rest => find (n' - 1, rest, liftC + 1, liftE) + | KnownC _ :: rest => find (n' - 1, rest, liftC, liftE) + | UnknownE :: rest => find (n' - 1, rest, liftC, liftE + 1) + | KnownE _ :: rest => find (n' - 1, rest, liftC, liftE) + | Lift (liftC', liftE') :: rest => find (n', rest, liftC + liftC', liftE + liftE') + | [] => raise Fail "Reduce.exp: ERel [2]" + in + find (n, env, 0, 0) + end + | ENamed n => + (case IM.find (namedE, n) of + NONE => all + | SOME e => e) + | ECon (dk, pc, cs, eo) => (ECon (dk, patCon pc, + map (con env) cs, Option.map (exp env) eo), loc) + | EFfi _ => all + | EFfiApp (m, f, es) => (EFfiApp (m, f, map (exp env) es), loc) + + | EApp (e1, e2) => + let + val e1 = exp env e1 + val e2 = exp env e2 + in + case #1 e1 of + EAbs (_, _, _, b) => exp (KnownE e2 :: env) b + | _ => (EApp (e1, e2), loc) + end + + | EAbs (x, dom, ran, e) => (EAbs (x, con env dom, con env ran, exp (UnknownE :: env) e), loc) + + | ECApp (e, c) => + let + val e = exp env e + val c = con env c + in + case #1 e of + ECAbs (_, _, b) => exp (KnownC c :: env) b + | _ => (ECApp (e, c), loc) + end + + | ECAbs (x, k, e) => (ECAbs (x, k, exp (UnknownC :: env) e), loc) + + | ERecord xcs => (ERecord (map (fn (x, e, t) => (con env x, exp env e, con env t)) xcs), loc) + | EField (e, c, {field, rest}) => + let + val e = exp env e + val c = con env c + + fun default () = (EField (e, c, {field = con env field, rest = con env rest}), loc) + in + case (#1 e, #1 c) of + (ERecord xcs, CName x) => + (case List.find (fn ((CName x', _), _, _) => x' = x | _ => false) xcs of + NONE => default () + | SOME (_, e, _) => e) + | _ => default () + end + + | EConcat (e1, c1, e2, c2) => + let + val e1 = exp env e1 + val e2 = exp env e2 + in + case (#1 e1, #1 e2) of + (ERecord xes1, ERecord xes2) => (ERecord (xes1 @ xes2), loc) + | _ => + let + val c1 = con env c1 + val c2 = con env c2 + in + case (#1 c1, #1 c2) of + (CRecord (k, xcs1), CRecord (_, xcs2)) => + let + val (xes1, rest) = ListUtil.foldlMap (doPart e1) [] xcs1 + val (xes2, _) = ListUtil.foldlMap (doPart e2) rest xcs2 + in + exp env (ERecord (xes1 @ xes2), loc) + end + | _ => (EConcat (e1, c1, e2, c2), loc) + end + end + + | ECut (e, c, {field, rest}) => + let + val e = exp env e + val c = con env c + + fun default () = + let + val rest = con env rest + in + case #1 rest of + CRecord (k, xcs) => + let + val (xes, _) = ListUtil.foldlMap (doPart e) [] xcs + in + exp env (ERecord xes, loc) + end + | _ => (ECut (e, c, {field = con env field, rest = rest}), loc) + end + in + case (#1 e, #1 c) of + (ERecord xes, CName x) => + if List.all (fn ((CName _, _), _, _) => true | _ => false) xes then + (ERecord (List.filter (fn ((CName x', _), _, _) => x' <> x + | _ => raise Fail "Reduce: ECut") xes), loc) + else + default () + | _ => default () + end + + | ECutMulti (e, c, {rest}) => + let + val e = exp env e + val c = con env c + + fun default () = + let + val rest = con env rest + in + case #1 rest of + CRecord (k, xcs) => + let + val (xes, _) = ListUtil.foldlMap (doPart e) [] xcs + in + exp env (ERecord xes, loc) + end + | _ => (ECutMulti (e, c, {rest = rest}), loc) + end + in + case (#1 e, #1 c) of + (ERecord xes, CRecord (_, xcs)) => + if List.all (fn ((CName _, _), _, _) => true | _ => false) xes + andalso List.all (fn ((CName _, _), _) => true | _ => false) xcs then + (ERecord (List.filter (fn ((CName x', _), _, _) => + List.all (fn ((CName x, _), _) => x' <> x + | _ => raise Fail "Reduce: ECutMulti [1]") xcs + | _ => raise Fail "Reduce: ECutMulti [2]") xes), loc) + else + default () + | _ => default () + end + + | EFold _ => all + + | ECase (e, pes, {disc, result}) => + let + fun patBinds (p, _) = + case p of + PWild => 0 + | PVar _ => 1 + | PPrim _ => 0 + | PCon (_, _, _, NONE) => 0 + | PCon (_, _, _, SOME p) => patBinds p + | PRecord xpts => foldl (fn ((_, p, _), n) => n + patBinds p) 0 xpts + + fun pat (all as (p, loc)) = + case p of + PWild => all + | PVar (x, t) => (PVar (x, con env t), loc) + | PPrim _ => all + | PCon (dk, pc, cs, po) => + (PCon (dk, patCon pc, map (con env) cs, Option.map pat po), loc) + | PRecord xpts => (PRecord (map (fn (x, p, t) => (x, pat p, con env t)) xpts), loc) + in + (ECase (exp env e, + map (fn (p, e) => (pat p, + exp (List.tabulate (patBinds p, fn _ => UnknownE) @ env) e)) + pes, {disc = con env disc, result = con env result}), loc) + end + + | EWrite e => (EWrite (exp env e), loc) + | EClosure (n, es) => (EClosure (n, map (exp env) es), loc) + + | ELet (x, t, e1, e2) => (ELet (x, con env t, exp env e1, exp (UnknownE :: env) e2), loc) in {con = con, exp = exp} end -fun con namedC c = #con (conAndExp (namedC, IM.empty)) [] c -fun exp (namedC, namedE) e = #exp (conAndExp (namedC, namedE)) [] e +fun con namedC env c = #con (conAndExp (namedC, IM.empty)) env c +fun exp (namedC, namedE) env e = #exp (conAndExp (namedC, namedE)) env e fun reduce file = let @@ -139,30 +342,34 @@ fun reduce file = case #1 d of DCon (x, n, k, c) => let - val c = con namedC c + val c = con namedC [] c in ((DCon (x, n, k, c), loc), (IM.insert (namedC, n, c), namedE)) end | DDatatype (x, n, ps, cs) => - ((DDatatype (x, n, ps, map (fn (x, n, co) => (x, n, Option.map (con namedC) co)) cs), loc), - st) + let + val env = map (fn _ => UnknownC) ps + in + ((DDatatype (x, n, ps, map (fn (x, n, co) => (x, n, Option.map (con namedC env) co)) cs), loc), + st) + end | DVal (x, n, t, e, s) => let - val t = con namedC t - val e = exp (namedC, namedE) e + val t = con namedC [] t + val e = exp (namedC, namedE) [] e in ((DVal (x, n, t, e, s), loc), (namedC, IM.insert (namedE, n, e))) end | DValRec vis => - ((DValRec (map (fn (x, n, t, e, s) => (x, n, con namedC t, exp (namedC, namedE) e, s)) vis), loc), + ((DValRec (map (fn (x, n, t, e, s) => (x, n, con namedC [] t, exp (namedC, namedE) [] e, s)) vis), loc), st) | DExport _ => (d, st) - | DTable (s, n, c, s') => ((DTable (s, n, con namedC c, s'), loc), st) + | DTable (s, n, c, s') => ((DTable (s, n, con namedC [] c, s'), loc), st) | DSequence _ => (d, st) | DDatabase _ => (d, st) - | DCookie (s, n, c, s') => ((DCookie (s, n, con namedC c, s'), loc), st) + | DCookie (s, n, c, s') => ((DCookie (s, n, con namedC [] c, s'), loc), st) val (file, _) = ListUtil.foldlMap doDecl (IM.empty, IM.empty) file in -- cgit v1.2.3 From 879bb7d5c760d277348a4ab9f799143013680f08 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Wed, 26 Nov 2008 14:51:52 -0500 Subject: Fix environments for repeat visits for exp reduction --- src/reduce.sml | 110 +++++++++++++++++++++++++++++++++++---------------------- 1 file changed, 67 insertions(+), 43 deletions(-) (limited to 'src/reduce.sml') diff --git a/src/reduce.sml b/src/reduce.sml index 3d117fb5..5b4d7a49 100644 --- a/src/reduce.sml +++ b/src/reduce.sml @@ -44,9 +44,24 @@ datatype env_item = type env = env_item list +fun ei2s ei = + case ei of + UnknownC => "UC" + | KnownC _ => "KC" + | UnknownE => "UE" + | KnownE _ => "KE" + | Lift (n1, n2) => "(" ^ Int.toString n1 ^ ", " ^ Int.toString n2 ^ ")" + +fun e2s env = String.concatWith " " (map ei2s env) + +val deKnown = List.filter (fn KnownC _ => false + | KnownE _ => false + | _ => true) + fun conAndExp (namedC, namedE) = let fun con env (all as (c, loc)) = + ((*Print.prefaces "con" [("c", CorePrint.p_con CoreEnv.empty all)];*) case c of TFun (c1, c2) => (TFun (con env c1, con env c2), loc) | TCFun (x, k, c2) => (TCFun (x, k, con (UnknownC :: env) c2), loc) @@ -54,23 +69,25 @@ fun conAndExp (namedC, namedE) = | CRel n => let - fun find (n', env, lift) = - if n' = 0 then - case env of - UnknownC :: _ => (CRel (n + lift), loc) - | KnownC c :: _ => con (Lift (lift, 0) :: env) c - | Lift (lift', _) :: rest => find (0, rest, lift + lift') - | _ => raise Fail "Reduce.con: CRel [1]" - else - case env of - UnknownC :: rest => find (n' - 1, rest, lift + 1) - | KnownC _ :: rest => find (n' - 1, rest, lift) - | UnknownE :: rest => find (n' - 1, rest, lift) - | KnownE _ :: rest => find (n' - 1, rest, lift) - | Lift (lift', _) :: rest => find (n', rest, lift + lift') - | [] => raise Fail "Reduce.con: CRel [2]" + fun find (n', env, nudge, lift) = + case env of + [] => raise Fail "Reduce.con: CRel" + | UnknownE :: rest => find (n', rest, nudge, lift) + | KnownE _ :: rest => find (n', rest, nudge, lift) + | Lift (lift', _) :: rest => find (n', rest, nudge + lift', lift + lift') + | UnknownC :: rest => + if n' = 0 then + (CRel (n + nudge), loc) + else + find (n' - 1, rest, nudge, lift + 1) + | KnownC c :: rest => + if n' = 0 then + con (Lift (lift, 0) :: rest) c + else + find (n' - 1, rest, nudge - 1, lift) in - find (n, env, 0) + (*print (Int.toString n ^ ": " ^ e2s env ^ "\n");*) + find (n, env, 0, 0) end | CNamed n => (case IM.find (namedC, n) of @@ -84,15 +101,16 @@ fun conAndExp (namedC, namedE) = in case #1 c1 of CAbs (_, _, b) => - con (KnownC c2 :: env) b + con (KnownC c2 :: deKnown env) b | CApp ((CApp (fold as (CFold _, _), f), _), i) => (case #1 c2 of CRecord (_, []) => i | CRecord (k, (x, c) :: rest) => - con env (CApp ((CApp ((CApp (f, x), loc), c), loc), - (CApp ((CApp ((CApp (fold, f), loc), i), loc), - (CRecord (k, rest), loc)), loc)), loc) + con (deKnown env) + (CApp ((CApp ((CApp (f, x), loc), c), loc), + (CApp ((CApp ((CApp (fold, f), loc), i), loc), + (CRecord (k, rest), loc)), loc)), loc) | _ => (CApp (c1, c2), loc)) | _ => (CApp (c1, c2), loc) @@ -124,7 +142,7 @@ fun conAndExp (namedC, namedE) = case #1 c of CTuple cs => List.nth (cs, n - 1) | _ => (CProj (c, n), loc) - end + end) fun patCon pc = case pc of @@ -141,27 +159,33 @@ fun conAndExp (namedC, namedE) = this :: rest) fun exp env (all as (e, loc)) = + ((*Print.prefaces "exp" [("e", CorePrint.p_exp CoreEnv.empty all), + ("env", Print.PD.string (e2s env))];*) case e of EPrim _ => all | ERel n => let - fun find (n', env, liftC, liftE) = - if n' = 0 then - case env of - UnknownE :: _ => (ERel (n + liftE), loc) - | KnownE e :: _ => exp (Lift (liftC, liftE) :: env) e - | Lift (liftC', liftE') :: rest => find (0, rest, liftC + liftC', liftE + liftE') - | _ => raise Fail "Reduce.exp: ERel [1]" - else - case env of - UnknownC :: rest => find (n' - 1, rest, liftC + 1, liftE) - | KnownC _ :: rest => find (n' - 1, rest, liftC, liftE) - | UnknownE :: rest => find (n' - 1, rest, liftC, liftE + 1) - | KnownE _ :: rest => find (n' - 1, rest, liftC, liftE) - | Lift (liftC', liftE') :: rest => find (n', rest, liftC + liftC', liftE + liftE') - | [] => raise Fail "Reduce.exp: ERel [2]" + fun find (n', env, nudge, liftC, liftE) = + case env of + [] => raise Fail "Reduce.exp: ERel" + | UnknownC :: rest => find (n', rest, nudge, liftC + 1, liftE) + | KnownC _ :: rest => find (n', rest, nudge, liftC, liftE) + | Lift (liftC', liftE') :: rest => find (n', rest, nudge + liftE', + liftC + liftC', liftE + liftE') + | UnknownE :: rest => + if n' = 0 then + (ERel (n + nudge), loc) + else + find (n' - 1, rest, nudge, liftC, liftE + 1) + | KnownE e :: rest => + if n' = 0 then + ((*print "SUBSTITUTING\n";*) + exp (Lift (liftC, liftE) :: rest) e) + else + find (n' - 1, rest, nudge - 1, liftC, liftE) in - find (n, env, 0, 0) + (*print (Int.toString n ^ ": " ^ e2s env ^ "\n");*) + find (n, env, 0, 0, 0) end | ENamed n => (case IM.find (namedE, n) of @@ -178,7 +202,7 @@ fun conAndExp (namedC, namedE) = val e2 = exp env e2 in case #1 e1 of - EAbs (_, _, _, b) => exp (KnownE e2 :: env) b + EAbs (_, _, _, b) => exp (KnownE e2 :: deKnown env) b | _ => (EApp (e1, e2), loc) end @@ -190,7 +214,7 @@ fun conAndExp (namedC, namedE) = val c = con env c in case #1 e of - ECAbs (_, _, b) => exp (KnownC c :: env) b + ECAbs (_, _, b) => exp (KnownC c :: deKnown env) b | _ => (ECApp (e, c), loc) end @@ -230,7 +254,7 @@ fun conAndExp (namedC, namedE) = val (xes1, rest) = ListUtil.foldlMap (doPart e1) [] xcs1 val (xes2, _) = ListUtil.foldlMap (doPart e2) rest xcs2 in - exp env (ERecord (xes1 @ xes2), loc) + exp (deKnown env) (ERecord (xes1 @ xes2), loc) end | _ => (EConcat (e1, c1, e2, c2), loc) end @@ -250,7 +274,7 @@ fun conAndExp (namedC, namedE) = let val (xes, _) = ListUtil.foldlMap (doPart e) [] xcs in - exp env (ERecord xes, loc) + exp (deKnown env) (ERecord xes, loc) end | _ => (ECut (e, c, {field = con env field, rest = rest}), loc) end @@ -279,7 +303,7 @@ fun conAndExp (namedC, namedE) = let val (xes, _) = ListUtil.foldlMap (doPart e) [] xcs in - exp env (ERecord xes, loc) + exp (deKnown env) (ERecord xes, loc) end | _ => (ECutMulti (e, c, {rest = rest}), loc) end @@ -328,7 +352,7 @@ fun conAndExp (namedC, namedE) = | EWrite e => (EWrite (exp env e), loc) | EClosure (n, es) => (EClosure (n, map (exp env) es), loc) - | ELet (x, t, e1, e2) => (ELet (x, con env t, exp env e1, exp (UnknownE :: env) e2), loc) + | ELet (x, t, e1, e2) => (ELet (x, con env t, exp env e1, exp (UnknownE :: env) e2), loc)) in {con = con, exp = exp} end -- cgit v1.2.3 From 9d6ca0836f8b54c672449d1100da3d0d36e07611 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Wed, 26 Nov 2008 15:03:45 -0500 Subject: crud1 compiles with new Reduce --- src/reduce.sml | 18 ++++++++++++++++-- 1 file changed, 16 insertions(+), 2 deletions(-) (limited to 'src/reduce.sml') diff --git a/src/reduce.sml b/src/reduce.sml index 5b4d7a49..a08feb26 100644 --- a/src/reduce.sml +++ b/src/reduce.sml @@ -103,13 +103,13 @@ fun conAndExp (namedC, namedE) = CAbs (_, _, b) => con (KnownC c2 :: deKnown env) b - | CApp ((CApp (fold as (CFold _, _), f), _), i) => + | CApp ((CApp ((CFold _, _), f), _), i) => (case #1 c2 of CRecord (_, []) => i | CRecord (k, (x, c) :: rest) => con (deKnown env) (CApp ((CApp ((CApp (f, x), loc), c), loc), - (CApp ((CApp ((CApp (fold, f), loc), i), loc), + (CApp (c1, (CRecord (k, rest), loc)), loc)), loc) | _ => (CApp (c1, c2), loc)) @@ -215,6 +215,20 @@ fun conAndExp (namedC, namedE) = in case #1 e of ECAbs (_, _, b) => exp (KnownC c :: deKnown env) b + + | EApp ((EApp ((ECApp ((EFold _, _), _), _), f), _), i) => + (case #1 c of + CRecord (_, []) => i + | CRecord (k, (nm, v) :: rest) => + let + val rest = (CRecord (k, rest), loc) + in + exp (deKnown env) + (EApp ((ECApp ((ECApp ((ECApp (f, nm), loc), v), loc), rest), loc), + (ECApp (e, rest), loc)), loc) + end + | _ => (ECApp (e, c), loc)) + | _ => (ECApp (e, c), loc) end -- cgit v1.2.3 From f7db36644bdbde7b0ed48daffeb760bd5418bd2e Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Sat, 14 Feb 2009 14:07:56 -0500 Subject: Start of RPCification --- demo/crud2.sql | 6 --- src/compiler.sig | 2 + src/compiler.sml | 9 +++- src/core.sml | 2 + src/core_print.sml | 9 ++++ src/core_util.sml | 14 +++++ src/monoize.sml | 2 + src/reduce.sml | 4 +- src/reduce_local.sml | 2 + src/rpcify.sig | 32 +++++++++++ src/rpcify.sml | 149 +++++++++++++++++++++++++++++++++++++++++++++++++++ src/shake.sml | 45 +++++++++------- src/sources | 3 ++ tests/rpc.ur | 13 +++++ tests/rpc.urp | 5 ++ 15 files changed, 269 insertions(+), 28 deletions(-) delete mode 100644 demo/crud2.sql create mode 100644 src/rpcify.sig create mode 100644 src/rpcify.sml create mode 100644 tests/rpc.ur create mode 100644 tests/rpc.urp (limited to 'src/reduce.sml') diff --git a/demo/crud2.sql b/demo/crud2.sql deleted file mode 100644 index 88568f2a..00000000 --- a/demo/crud2.sql +++ /dev/null @@ -1,6 +0,0 @@ -CREATE TABLE uw_Crud2_t(uw_id int8 NOT NULL, uw_nam text NOT NULL, - uw_ready bool NOT NULL); - - CREATE SEQUENCE uw_Crud2_Crud_Make_seq; - - \ No newline at end of file diff --git a/src/compiler.sig b/src/compiler.sig index b126fb51..1b4995ee 100644 --- a/src/compiler.sig +++ b/src/compiler.sig @@ -66,6 +66,7 @@ signature COMPILER = sig val especialize : (Core.file, Core.file) phase val core_untangle : (Core.file, Core.file) phase val shake : (Core.file, Core.file) phase + val rpcify : (Core.file, Core.file) phase val tag : (Core.file, Core.file) phase val reduce : (Core.file, Core.file) phase val unpoly : (Core.file, Core.file) phase @@ -92,6 +93,7 @@ signature COMPILER = sig val toEspecialize : (string, Core.file) transform val toCore_untangle : (string, Core.file) transform val toShake1 : (string, Core.file) transform + val toRpcify : (string, Core.file) transform val toTag : (string, Core.file) transform val toReduce : (string, Core.file) transform val toUnpoly : (string, Core.file) transform diff --git a/src/compiler.sml b/src/compiler.sml index 52181401..aecefbcf 100644 --- a/src/compiler.sml +++ b/src/compiler.sml @@ -446,12 +446,19 @@ val shake = { val toShake1 = transform shake "shake1" o toCore_untangle +val rpcify = { + func = Rpcify.frob, + print = CorePrint.p_file CoreEnv.empty +} + +val toRpcify = transform rpcify "rpcify" o toShake1 + val tag = { func = Tag.tag, print = CorePrint.p_file CoreEnv.empty } -val toTag = transform tag "tag" o toShake1 +val toTag = transform tag "tag" o toRpcify val reduce = { func = Reduce.reduce, diff --git a/src/core.sml b/src/core.sml index 4623bb49..fbe150c1 100644 --- a/src/core.sml +++ b/src/core.sml @@ -106,6 +106,8 @@ datatype exp' = | ELet of string * con * exp * exp + | EServerCall of int * exp list * exp + withtype exp = exp' located datatype export_kind = diff --git a/src/core_print.sml b/src/core_print.sml index 53922936..64cead70 100644 --- a/src/core_print.sml +++ b/src/core_print.sml @@ -394,6 +394,15 @@ fun p_exp' par env (e, _) = newline, p_exp (E.pushERel env x t) e2] + | EServerCall (n, es, e) => box [string "Server(", + p_enamed env n, + string ",", + space, + p_list (p_exp env) es, + string ")[", + p_exp env e, + string "]"] + and p_exp env = p_exp' false env fun p_named x n = diff --git a/src/core_util.sml b/src/core_util.sml index 02cb86ca..3d6808f9 100644 --- a/src/core_util.sml +++ b/src/core_util.sml @@ -479,6 +479,13 @@ fun compare ((e1, _), (e2, _)) = | (ELet (_, _, x1, e1), ELet (_, _, x2, e2)) => join (compare (x1, x2), fn () => compare (e1, e2)) + | (ELet _, _) => LESS + | (_, ELet _) => GREATER + + | (EServerCall (n1, es1, e1), EServerCall (n2, es2, e2)) => + join (Int.compare (n1, n2), + fn () => join (joinL compare (es1, es2), + fn () => compare (e1, e2))) datatype binder = RelC of string * kind @@ -653,6 +660,13 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, bind} = fn e2' => (ELet (x, t', e1', e2'), loc)))) + | EServerCall (n, es, e) => + S.bind2 (ListUtil.mapfold (mfe ctx) es, + fn es' => + S.map2 (mfe ctx e, + fn e' => + (EServerCall (n, es', e'), loc))) + and mfp ctx (pAll as (p, loc)) = case p of PWild => S.return2 pAll diff --git a/src/monoize.sml b/src/monoize.sml index 80661d03..a1f61143 100644 --- a/src/monoize.sml +++ b/src/monoize.sml @@ -2224,6 +2224,8 @@ fun monoExp (env, st, fm) (all as (e, loc)) = in ((L'.ELet (x, t', e1, e2), loc), fm) end + + | L.EServerCall _ => raise Fail "Monoize EServerCall" end fun monoDecl (env, fm) (all as (d, loc)) = diff --git a/src/reduce.sml b/src/reduce.sml index a08feb26..89fce664 100644 --- a/src/reduce.sml +++ b/src/reduce.sml @@ -366,7 +366,9 @@ fun conAndExp (namedC, namedE) = | EWrite e => (EWrite (exp env e), loc) | EClosure (n, es) => (EClosure (n, map (exp env) es), loc) - | ELet (x, t, e1, e2) => (ELet (x, con env t, exp env e1, exp (UnknownE :: env) e2), loc)) + | ELet (x, t, e1, e2) => (ELet (x, con env t, exp env e1, exp (UnknownE :: env) e2), loc) + + | EServerCall (n, es, e) => (EServerCall (n, map (exp env) es, exp env e), loc)) in {con = con, exp = exp} end diff --git a/src/reduce_local.sml b/src/reduce_local.sml index d80d5770..55bb5198 100644 --- a/src/reduce_local.sml +++ b/src/reduce_local.sml @@ -131,6 +131,8 @@ fun exp env (all as (e, loc)) = | ELet (x, t, e1, e2) => (ELet (x, t, exp env e1, exp (Unknown :: env) e2), loc) + | EServerCall (n, es, e) => (EServerCall (n, map (exp env) es, exp env e), loc) + fun reduce file = let fun doDecl (d as (_, loc)) = diff --git a/src/rpcify.sig b/src/rpcify.sig new file mode 100644 index 00000000..7da53b79 --- /dev/null +++ b/src/rpcify.sig @@ -0,0 +1,32 @@ +(* Copyright (c) 2009, Adam Chlipala + * All rights reserved. + * + * Redistribution and use in source and binary forms, with or without + * modification, are permitted provided that the following conditions are met: + * + * - Redistributions of source code must retain the above copyright notice, + * this list of conditions and the following disclaimer. + * - Redistributions in binary form must reproduce the above copyright notice, + * this list of conditions and the following disclaimer in the documentation + * and/or other materials provided with the distribution. + * - The names of contributors may not be used to endorse or promote products + * derived from this software without specific prior written permission. + * + * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" + * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE + * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE + * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE + * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR + * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF + * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS + * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN + * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) + * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE + * POSSIBILITY OF SUCH DAMAGE. + *) + +signature RPCIFY = sig + + val frob : Core.file -> Core.file + +end diff --git a/src/rpcify.sml b/src/rpcify.sml new file mode 100644 index 00000000..dec8dc18 --- /dev/null +++ b/src/rpcify.sml @@ -0,0 +1,149 @@ +(* Copyright (c) 2009, Adam Chlipala + * All rights reserved. + * + * Redistribution and use in source and binary forms, with or without + * modification, are permitted provided that the following conditions are met: + * + * - Redistributions of source code must retain the above copyright notice, + * this list of conditions and the following disclaimer. + * - Redistributions in binary form must reproduce the above copyright notice, + * this list of conditions and the following disclaimer in the documentation + * and/or other materials provided with the distribution. + * - The names of contributors may not be used to endorse or promote products + * derived from this software without specific prior written permission. + * + * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" + * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE + * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE + * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE + * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR + * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF + * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS + * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN + * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) + * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE + * POSSIBILITY OF SUCH DAMAGE. + *) + +structure Rpcify :> RPCIFY = struct + +open Core + +structure U = CoreUtil +structure E = CoreEnv + +structure IS = IntBinarySet +structure IM = IntBinaryMap + +structure SS = BinarySetFn(struct + type ord_key = string + val compare = String.compare + end) + +val ssBasis = SS.addList (SS.empty, + ["requestHeader", + "query", + "dml", + "nextval"]) + +val csBasis = SS.addList (SS.empty, + ["source", + "get", + "set", + "alert"]) + +type state = { + exps : int IM.map, + decls : (string * int * con * exp * string) list +} + +fun frob file = + let + fun sideish (basis, ssids) = + U.Exp.exists {kind = fn _ => false, + con = fn _ => false, + exp = fn ENamed n => IS.member (ssids, n) + | EFfi ("Basis", x) => SS.member (basis, x) + | EFfiApp ("Basis", x, _) => SS.member (basis, x) + | _ => false} + + fun whichIds basis = + let + fun decl ((d, _), ssids) = + let + val impure = sideish (basis, ssids) + in + case d of + DVal (_, n, _, e, _) => if impure e then + IS.add (ssids, n) + else + ssids + | DValRec xes => if List.exists (fn (_, _, _, e, _) => impure e) xes then + foldl (fn ((_, n, _, _, _), ssids) => IS.add (ssids, n)) + ssids xes + else + ssids + | _ => ssids + end + in + foldl decl IS.empty file + end + + val ssids = whichIds ssBasis + val csids = whichIds csBasis + + val serverSide = sideish (ssBasis, ssids) + val clientSide = sideish (csBasis, csids) + + fun exp (e, st) = + case e of + EApp ( + (EApp + ((EApp ((ECApp ((ECApp ((ECApp ((EFfi ("Basis", "bind"), loc), _), _), t1), _), t2), _), + (EFfi ("Basis", "transaction_monad"), _)), _), + trans1), _), + trans2) => + (case (serverSide trans1, clientSide trans1, serverSide trans2, clientSide trans2) of + (true, false, false, _) => + let + fun getApp (e, args) = + case #1 e of + ENamed n => (n, args) + | EApp (e1, e2) => getApp (e1, e2 :: args) + | _ => (ErrorMsg.errorAt loc "Mixed client/server code doesn't use a named function for server part"; + (0, [])) + + val (n, args) = getApp (trans1, []) + in + (EServerCall (n, args, trans2), st) + end + | _ => (e, st)) + | _ => (e, st) + + fun decl (d, st : state) = + let + val (d, st) = U.Decl.foldMap {kind = fn x => x, + con = fn x => x, + exp = exp, + decl = fn x => x} + st d + in + (case #decls st of + [] => [d] + | ds => + case d of + (DValRec vis, loc) => [(DValRec (ds @ vis), loc)] + | (_, loc) => [(DValRec ds, loc), d], + {decls = [], + exps = #exps st}) + end + + val (file, _) = ListUtil.foldlMapConcat decl + {decls = [], + exps = IM.empty} + file + in + file + end + +end diff --git a/src/shake.sml b/src/shake.sml index e062743d..58c1d2c6 100644 --- a/src/shake.sml +++ b/src/shake.sml @@ -94,26 +94,31 @@ fun shake file = and shakeCon s = U.Con.fold {kind = kind, con = con} s fun exp (e, s) = - case e of - ENamed n => - if IS.member (#exp s, n) then - s - else - let - val s' = {exp = IS.add (#exp s, n), - con = #con s} - in - (*print ("Need " ^ Int.toString n ^ "\n");*) - case IM.find (edef, n) of - NONE => s' - | SOME (ns, t, e) => - let - val s' = shakeExp (shakeCon s' t) e - in - foldl (fn (n, s') => exp (ENamed n, s')) s' ns - end - end - | _ => s + let + fun check n = + if IS.member (#exp s, n) then + s + else + let + val s' = {exp = IS.add (#exp s, n), + con = #con s} + in + (*print ("Need " ^ Int.toString n ^ "\n");*) + case IM.find (edef, n) of + NONE => s' + | SOME (ns, t, e) => + let + val s' = shakeExp (shakeCon s' t) e + in + foldl (fn (n, s') => exp (ENamed n, s')) s' ns + end + end + in + case e of + ENamed n => check n + | EServerCall (n, _, _) => check n + | _ => s + end and shakeExp s = U.Exp.fold {kind = kind, con = con, exp = exp} s diff --git a/src/sources b/src/sources index 05b1cc54..f5574365 100644 --- a/src/sources +++ b/src/sources @@ -108,6 +108,9 @@ especialize.sml defunc.sig defunc.sml +rpcify.sig +rpcify.sml + tag.sig tag.sml diff --git a/tests/rpc.ur b/tests/rpc.ur new file mode 100644 index 00000000..85191229 --- /dev/null +++ b/tests/rpc.ur @@ -0,0 +1,13 @@ +sequence s + +fun main () : transaction page = + let + fun getNext () = nextval s + in + s <- source 0; + return +