summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/compiler.sml7
-rw-r--r--src/core_print.sml3
-rw-r--r--src/core_util.sig6
-rw-r--r--src/core_util.sml7
-rw-r--r--src/especialize.sml236
-rw-r--r--src/reduce_local.sig34
-rw-r--r--src/reduce_local.sml69
-rw-r--r--src/sources3
-rw-r--r--src/tag.sml2
9 files changed, 267 insertions, 100 deletions
diff --git a/src/compiler.sml b/src/compiler.sml
index bde16fd3..9705cfaf 100644
--- a/src/compiler.sml
+++ b/src/compiler.sml
@@ -411,6 +411,13 @@ val corify = {
val toCorify = transform corify "corify" o toExplify
+(*val reduce_local = {
+ func = ReduceLocal.reduce,
+ print = CorePrint.p_file CoreEnv.empty
+}
+
+val toReduce_local = transform reduce_local "reduce_local" o toCorify*)
+
val especialize = {
func = ESpecialize.specialize,
print = CorePrint.p_file CoreEnv.empty
diff --git a/src/core_print.sml b/src/core_print.sml
index c4341e51..af43e401 100644
--- a/src/core_print.sml
+++ b/src/core_print.sml
@@ -482,7 +482,8 @@ fun p_decl env (dAll as (d, _) : decl) =
space,
string "as",
space,
- p_con env (#2 (E.lookupENamed env n))]
+ (p_con env (#2 (E.lookupENamed env n))
+ handle E.UnboundNamed _ => string "UNBOUND")]
| DTable (x, n, c, s) => box [string "table",
space,
p_named x n,
diff --git a/src/core_util.sig b/src/core_util.sig
index 51dee8f4..e435aeaf 100644
--- a/src/core_util.sig
+++ b/src/core_util.sig
@@ -175,6 +175,12 @@ structure File : sig
bind : 'context * binder -> 'context}
-> 'context -> Core.file -> Core.file
+ val map : {kind : Core.kind' -> Core.kind',
+ con : Core.con' -> Core.con',
+ exp : Core.exp' -> Core.exp',
+ decl : Core.decl' -> Core.decl'}
+ -> Core.file -> Core.file
+
val fold : {kind : Core.kind' * 'state -> 'state,
con : Core.con' * 'state -> 'state,
exp : Core.exp' * 'state -> 'state,
diff --git a/src/core_util.sml b/src/core_util.sml
index 2352a849..4d72f57e 100644
--- a/src/core_util.sml
+++ b/src/core_util.sml
@@ -953,6 +953,13 @@ fun mapB {kind, con, exp, decl, bind} ctx ds =
S.Continue (ds, ()) => ds
| S.Return _ => raise Fail "CoreUtil.File.mapB: Impossible"
+fun map {kind, con, exp, decl} ds =
+ mapB {kind = kind,
+ con = fn () => con,
+ exp = fn () => exp,
+ decl = fn () => decl,
+ bind = fn _ => ()} () ds
+
fun fold {kind, con, exp, decl} s d =
case mapfold {kind = fn k => fn s => S.Continue (k, kind (k, s)),
con = fn c => fn s => S.Continue (c, con (c, s)),
diff --git a/src/especialize.sml b/src/especialize.sml
index 92e29da3..cc583044 100644
--- a/src/especialize.sml
+++ b/src/especialize.sml
@@ -41,6 +41,7 @@ end
structure KM = BinaryMapFn(K)
structure IM = IntBinaryMap
+structure IS = IntBinarySet
val sizeOf = U.Exp.fold {kind = fn (_, n) => n,
con = fn (_, n) => n,
@@ -101,109 +102,148 @@ type state = {
fun kind (k, st) = (k, st)
fun con (c, st) = (c, st)
-fun exp (e, st : state) =
+fun specialize' file =
let
- fun getApp e =
+ fun default (_, fs) = fs
+
+ fun actionableExp (e, fs) =
case e of
- ENamed f => SOME (f, [], [])
- | EField ((ERecord xes, _), (CName x, _), _) =>
- (case List.find (fn ((CName x', _), _,_) => x' = x
- | _ => false) xes of
- NONE => NONE
- | SOME (_, (e, _), _) => getApp e)
- | EApp (e1, e2) =>
- (case getApp (#1 e1) of
- NONE => NONE
- | SOME (f, xs, xs') =>
- let
- val k =
- if List.null xs' then
- skeyIn e2
+ ERecord xes =>
+ foldl (fn (((CName s, _), e, _), fs) =>
+ if s = "Action" orelse s = "Link" then
+ let
+ fun findHead (e, _) =
+ case e of
+ ENamed n => IS.add (fs, n)
+ | EApp (e, _) => findHead e
+ | _ => fs
+ in
+ findHead e
+ end
+ else
+ fs
+ | (_, fs) => fs)
+ fs xes
+ | _ => fs
+
+ val actionable =
+ U.File.fold {kind = default,
+ con = default,
+ exp = actionableExp,
+ decl = default}
+ IS.empty file
+
+ fun exp (e, st : state) =
+ let
+ fun getApp e =
+ case e of
+ ENamed f => SOME (f, [], [])
+ | EApp (e1, e2) =>
+ (case getApp (#1 e1) of
+ NONE => NONE
+ | SOME (f, xs, xs') =>
+ let
+ val k =
+ if List.null xs' then
+ skeyIn e2
+ else
+ NONE
+ in
+ case k of
+ NONE => SOME (f, xs, xs' @ [e2])
+ | SOME k => SOME (f, xs @ [k], xs')
+ end)
+ | _ => NONE
+ in
+ case getApp e of
+ NONE => (e, st)
+ | SOME (f, [], []) => (e, st)
+ | SOME (f, [], xs') =>
+ (case IM.find (#funcs st, f) of
+ NONE => (e, st)
+ | SOME {typ, body, ...} =>
+ let
+ val functionInside = U.Con.exists {kind = fn _ => false,
+ con = fn TFun _ => true
+ | CFfi ("Basis", "transaction") => true
+ | _ => false}
+
+ fun hasFunarg (t, xs) =
+ case (t, xs) of
+ ((TFun (dom, ran), _), _ :: xs) =>
+ functionInside dom
+ orelse hasFunarg (ran, xs)
+ | _ => false
+ in
+ if List.all (fn (ERel _, _) => false | _ => true) xs'
+ andalso not (IS.member (actionable, f))
+ andalso hasFunarg (typ, xs') then
+ (#1 (foldl (fn (arg, e) => (EApp (e, arg), ErrorMsg.dummySpan))
+ body xs'),
+ st)
else
- NONE
- in
- case k of
- NONE => SOME (f, xs, xs' @ [e2])
- | SOME k => SOME (f, xs @ [k], xs')
- end)
- | _ => NONE
- in
- case getApp e of
- NONE => (e, st)
- | SOME (f, [], xs') => (#1 (foldl (fn (arg, e) => (EApp (e, arg), ErrorMsg.dummySpan))
- (ENamed f, ErrorMsg.dummySpan) xs'), st)
- | SOME (f, xs, xs') =>
- case IM.find (#funcs st, f) of
- NONE =>
- let
- val e = foldl (fn (arg, e) => (EApp (e, skeyOut arg), ErrorMsg.dummySpan))
- (ENamed f, ErrorMsg.dummySpan) xs
- in
- (#1 (foldl (fn (arg, e) => (EApp (e, arg), ErrorMsg.dummySpan))
- e xs'), st)
- end
- | SOME {name, args, body, typ, tag} =>
- case KM.find (args, xs) of
- SOME f' => ((*Print.prefaces "Pre-existing" [("e", CorePrint.p_exp CoreEnv.empty (e, ErrorMsg.dummySpan))];*)
- (#1 (foldl (fn (e, arg) => (EApp (e, arg), ErrorMsg.dummySpan))
- (ENamed f', ErrorMsg.dummySpan) xs'),
- st))
- | NONE =>
- let
- (*val () = Print.prefaces "New" [("e", CorePrint.p_exp CoreEnv.empty (e, ErrorMsg.dummySpan))]*)
-
- fun subBody (body, typ, xs) =
- case (#1 body, #1 typ, xs) of
- (_, _, []) => SOME (body, typ)
- | (EAbs (_, _, _, body'), TFun (_, typ'), x :: xs) =>
- let
- val body'' = E.subExpInExp (0, skeyOut x) body'
- in
- (*Print.prefaces "espec" [("body'", CorePrint.p_exp CoreEnv.empty body'),
- ("body''", CorePrint.p_exp CoreEnv.empty body'')];*)
- subBody (body'',
- typ',
- xs)
- end
- | _ => NONE
- in
- case subBody (body, typ, xs) of
- NONE => (e, st)
- | SOME (body', typ') =>
- let
- val f' = #maxName st
- (*val () = print ("f' = " ^ Int.toString f' ^ "\n")*)
- val funcs = IM.insert (#funcs st, f, {name = name,
- args = KM.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) :: #decls st})
- end
- end
- end
+ (e, st)
+ end)
+ | SOME (f, xs, xs') =>
+ case IM.find (#funcs st, f) of
+ NONE => (e, st)
+ | SOME {name, args, body, typ, tag} =>
+ case KM.find (args, xs) of
+ SOME f' => (#1 (foldl (fn (arg, e) => (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) =>
+ let
+ val body'' = E.subExpInExp (0, skeyOut x) body'
+ in
+ subBody (body'',
+ typ',
+ xs)
+ end
+ | _ => 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 = KM.insert (args,
+ xs, f'),
+ body = body,
+ typ = typ,
+ tag = tag})
+ val st = {
+ maxName = f' + 1,
+ funcs = funcs,
+ decls = #decls st
+ }
-and specExp st = U.Exp.foldMap {kind = kind, con = con, exp = exp} st
+ val (body', st) = specExp st body'
+ val e' = foldl (fn (arg, e) => (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) :: #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 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 : state, changed)) =
let
val funcs = #funcs st
@@ -223,7 +263,9 @@ fun specialize' file =
funcs = funcs,
decls = []}
+ (*val () = Print.prefaces "decl" [("d", CorePrint.p_decl CoreEnv.empty d)]*)
val (d', st) = specDecl st d
+ (*val () = print "/decl\n"*)
val funcs = #funcs st
val funcs =
@@ -267,7 +309,7 @@ fun specialize file =
val (changed, file) = specialize' file
in
if changed then
- specialize file
+ specialize (ReduceLocal.reduce file)
else
file
end
diff --git a/src/reduce_local.sig b/src/reduce_local.sig
new file mode 100644
index 00000000..3c76263a
--- /dev/null
+++ b/src/reduce_local.sig
@@ -0,0 +1,34 @@
+(* 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.
+ *)
+
+(* Simplify a Core program algebraically, without unfolding definitions *)
+
+signature REDUCE_LOCAL = sig
+
+ val reduce : Core.file -> Core.file
+
+end
diff --git a/src/reduce_local.sml b/src/reduce_local.sml
new file mode 100644
index 00000000..6a6d80a8
--- /dev/null
+++ b/src/reduce_local.sml
@@ -0,0 +1,69 @@
+(* 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.
+ *)
+
+(* Simplify a Core program algebraically, without unfolding definitions *)
+
+structure ReduceLocal :> REDUCE_LOCAL = struct
+
+open Core
+
+structure E = CoreEnv
+structure U = CoreUtil
+
+val subExpInExp = E.subExpInExp
+
+fun default x = x
+
+fun exp (e : exp') =
+ let
+ (*val () = Print.prefaces "exp" [("e", CorePrint.p_exp env (e, ErrorMsg.dummySpan))]*)
+
+ val r = case e of
+ EApp ((EAbs (x, t, _, e1), loc), e2) =>
+ ((*Print.prefaces "Substitute" [("x", Print.PD.string x),
+ ("t", CorePrint.p_con CoreEnv.empty t)];*)
+ #1 (reduceExp (subExpInExp (0, e2) e1)))
+
+ | EField ((ERecord xes, _), (CName x, _), _) =>
+ (case List.find (fn ((CName x', _), _, _) => x' = x
+ | _ => false) xes of
+ SOME (_, (e, _), _) => e
+ | NONE => e)
+
+ | _ => 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 e = U.Exp.map {kind = default, con = default, exp = exp} e
+
+val reduce = U.File.map {kind = default, con = default, exp = exp, decl = default}
+
+end
diff --git a/src/sources b/src/sources
index 9fd90e8c..252ffe44 100644
--- a/src/sources
+++ b/src/sources
@@ -96,6 +96,9 @@ unpoly.sml
specialize.sig
specialize.sml
+reduce_local.sig
+reduce_local.sml
+
especialize.sig
especialize.sml
diff --git a/src/tag.sml b/src/tag.sml
index 34595732..b19a0544 100644
--- a/src/tag.sml
+++ b/src/tag.sml
@@ -80,8 +80,6 @@ fun exp env (e, s) =
| _ => (ErrorMsg.errorAt loc "Invalid link expression";
(0, []))
-
-
val (f, args) = unravel e
val (cn, count, tags, newTags) =
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-15 17:01:56 +0000