summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2008-06-08 15:47:44 -0400
committerGravatar Adam Chlipala <adamc@hcoop.net>2008-06-08 15:47:44 -0400
commite18863bcabc5d185b7fe1fc750bdf0bbdb5a4f78 (patch)
tree180c8271605929d6c902c4dda9b8b756ff0e1fda /src
parentb0bf85209e8ddd4937393908d953f451556e73e9 (diff)
Some con reducing
Diffstat (limited to 'src')
-rw-r--r--src/compiler.sig2
-rw-r--r--src/compiler.sml14
-rw-r--r--src/core_env.sig6
-rw-r--r--src/core_env.sml10
-rw-r--r--src/core_print.sml7
-rw-r--r--src/core_util.sig35
-rw-r--r--src/core_util.sml91
-rw-r--r--src/elab_print.sml7
-rw-r--r--src/main.mlton.sml2
-rw-r--r--src/reduce.sig34
-rw-r--r--src/reduce.sml85
-rw-r--r--src/source_print.sml7
-rw-r--r--src/sources3
13 files changed, 285 insertions, 18 deletions
diff --git a/src/compiler.sig b/src/compiler.sig
index 6a4fa466..cafb3d20 100644
--- a/src/compiler.sig
+++ b/src/compiler.sig
@@ -32,9 +32,11 @@ signature COMPILER = sig
val parse : string -> Source.file option
val elaborate : ElabEnv.env -> string -> (ElabEnv.env * Elab.file) option
val corify : ElabEnv.env -> CoreEnv.env -> string -> Core.file option
+ val reduce : ElabEnv.env -> CoreEnv.env -> string -> Core.file option
val testParse : string -> unit
val testElaborate : string -> unit
val testCorify : string -> unit
+ val testReduce : string -> unit
end
diff --git a/src/compiler.sml b/src/compiler.sml
index 51fef453..28b92ac8 100644
--- a/src/compiler.sml
+++ b/src/compiler.sml
@@ -72,6 +72,11 @@ fun corify eenv cenv filename =
NONE => NONE
| SOME (_, file) => SOME (Corify.corify file)
+fun reduce eenv cenv filename =
+ case corify eenv cenv filename of
+ NONE => NONE
+ | SOME file => SOME (Reduce.reduce file)
+
fun testParse filename =
case parse filename of
NONE => print "Failed\n"
@@ -97,4 +102,13 @@ fun testCorify filename =
handle CoreEnv.UnboundNamed n =>
print ("Unbound named " ^ Int.toString n ^ "\n")
+fun testReduce filename =
+ (case reduce ElabEnv.basis CoreEnv.basis filename of
+ NONE => print "Failed\n"
+ | SOME file =>
+ (Print.print (CorePrint.p_file CoreEnv.basis file);
+ print "\n"))
+ handle CoreEnv.UnboundNamed n =>
+ print ("Unbound named " ^ Int.toString n ^ "\n")
+
end
diff --git a/src/core_env.sig b/src/core_env.sig
index 88cb253b..1766b3d1 100644
--- a/src/core_env.sig
+++ b/src/core_env.sig
@@ -27,6 +27,8 @@
signature CORE_ENV = sig
+ val liftConInCon : int -> Core.con -> Core.con
+
type env
val empty : env
@@ -44,8 +46,8 @@ signature CORE_ENV = sig
val pushERel : env -> string -> Core.con -> env
val lookupERel : env -> int -> string * Core.con
- val pushENamed : env -> string -> int -> Core.con -> env
- val lookupENamed : env -> int -> string * Core.con
+ val pushENamed : env -> string -> int -> Core.con -> Core.exp option -> env
+ val lookupENamed : env -> int -> string * Core.con * Core.exp option
val declBinds : env -> Core.decl -> env
diff --git a/src/core_env.sml b/src/core_env.sml
index e123c9a9..904c71f5 100644
--- a/src/core_env.sml
+++ b/src/core_env.sml
@@ -62,7 +62,7 @@ type env = {
namedC : (string * kind * con option) IM.map,
relE : (string * con) list,
- namedE : (string * con) IM.map
+ namedE : (string * con * exp option) IM.map
}
val empty = {
@@ -78,7 +78,7 @@ fun pushCRel (env : env) x k =
namedC = IM.map (fn (x, k, co) => (x, k, Option.map lift co)) (#namedC env),
relE = map (fn (x, c) => (x, lift c)) (#relE env),
- namedE = IM.map (fn (x, c) => (x, lift c)) (#namedE env)}
+ namedE = IM.map (fn (x, c, eo) => (x, lift c, eo)) (#namedE env)}
fun lookupCRel (env : env) n =
(List.nth (#relC env, n))
@@ -107,12 +107,12 @@ fun lookupERel (env : env) n =
(List.nth (#relE env, n))
handle Subscript => raise UnboundRel n
-fun pushENamed (env : env) x n t =
+fun pushENamed (env : env) x n t eo =
{relC = #relC env,
namedC = #namedC env,
relE = #relE env,
- namedE = IM.insert (#namedE env, n, (x, t))}
+ namedE = IM.insert (#namedE env, n, (x, t, eo))}
fun lookupENamed (env : env) n =
case IM.find (#namedE env, n) of
@@ -122,7 +122,7 @@ fun lookupENamed (env : env) n =
fun declBinds env (d, _) =
case d of
DCon (x, n, k, c) => pushCNamed env x n k (SOME c)
- | DVal (x, n, t, _) => pushENamed env x n t
+ | DVal (x, n, t, e) => pushENamed env x n t (SOME e)
val ktype = (KType, ErrorMsg.dummySpan)
diff --git a/src/core_print.sml b/src/core_print.sml
index 1e254862..c035ceef 100644
--- a/src/core_print.sml
+++ b/src/core_print.sml
@@ -69,7 +69,7 @@ fun p_con' par env (c, _) =
p_con (E.pushCRel env x k) c])
| TRecord (CRecord (_, xcs), _) => box [string "{",
p_list (fn (x, c) =>
- box [p_con env x,
+ box [p_name env x,
space,
string ":",
space,
@@ -134,6 +134,11 @@ fun p_con' par env (c, _) =
and p_con env = p_con' false env
+and p_name env (all as (c, _)) =
+ case c of
+ CName s => string s
+ | _ => p_con env all
+
fun p_exp' par env (e, _) =
case e of
EPrim p => Prim.p_t p
diff --git a/src/core_util.sig b/src/core_util.sig
index a40e0664..07350798 100644
--- a/src/core_util.sig
+++ b/src/core_util.sig
@@ -37,7 +37,7 @@ end
structure Con : sig
datatype binder =
Rel of string * Core.kind
- | Named of string * Core.kind
+ | Named of string * int * Core.kind * Core.con option
val mapfoldB : {kind : (Core.kind', 'state, 'abort) Search.mapfolder,
con : ('context, Core.con', 'state, 'abort) Search.mapfolderB,
@@ -62,9 +62,9 @@ end
structure Exp : sig
datatype binder =
RelC of string * Core.kind
- | NamedC of string * Core.kind
+ | NamedC of string * int * Core.kind * Core.con option
| RelE of string * Core.con
- | NamedE of string * Core.con
+ | NamedE of string * int * Core.con * Core.exp option
val mapfoldB : {kind : (Core.kind', 'state, 'abort) Search.mapfolder,
con : ('context, Core.con', 'state, 'abort) Search.mapfolderB,
@@ -85,4 +85,33 @@ structure Exp : sig
exp : Core.exp' -> bool} -> Core.exp -> bool
end
+structure Decl : sig
+ datatype binder = datatype Exp.binder
+
+ val mapfoldB : {kind : (Core.kind', 'state, 'abort) Search.mapfolder,
+ con : ('context, Core.con', 'state, 'abort) Search.mapfolderB,
+ exp : ('context, Core.exp', 'state, 'abort) Search.mapfolderB,
+ decl : ('context, Core.decl', 'state, 'abort) Search.mapfolderB,
+ bind : 'context * binder -> 'context}
+ -> ('context, Core.decl, 'state, 'abort) Search.mapfolderB
+end
+
+structure File : sig
+ datatype binder = datatype Exp.binder
+
+ val mapfoldB : {kind : (Core.kind', 'state, 'abort) Search.mapfolder,
+ con : ('context, Core.con', 'state, 'abort) Search.mapfolderB,
+ exp : ('context, Core.exp', 'state, 'abort) Search.mapfolderB,
+ decl : ('context, Core.decl', 'state, 'abort) Search.mapfolderB,
+ bind : 'context * binder -> 'context}
+ -> ('context, Core.file, 'state, 'abort) Search.mapfolderB
+
+ val mapB : {kind : Core.kind' -> Core.kind',
+ con : 'context -> Core.con' -> Core.con',
+ exp : 'context -> Core.exp' -> Core.exp',
+ decl : 'context -> Core.decl' -> Core.decl',
+ bind : 'context * binder -> 'context}
+ -> 'context -> Core.file -> Core.file
+end
+
end
diff --git a/src/core_util.sml b/src/core_util.sml
index 0f7df403..c3e8250b 100644
--- a/src/core_util.sml
+++ b/src/core_util.sml
@@ -79,7 +79,7 @@ structure Con = struct
datatype binder =
Rel of string * kind
- | Named of string * kind
+ | Named of string * int * kind * con option
fun mapfoldB {kind = fk, con = fc, bind} =
let
@@ -162,7 +162,7 @@ fun mapB {kind, con, bind} ctx c =
con = fn ctx => fn c => fn () => S.Continue (con ctx c, ()),
bind = bind} ctx c () of
S.Continue (c, ()) => c
- | S.Return _ => raise Fail "Con.mapB: Impossible"
+ | S.Return _ => raise Fail "CoreUtil.Con.mapB: Impossible"
fun exists {kind, con} k =
case mapfold {kind = fn k => fn () =>
@@ -184,9 +184,9 @@ structure Exp = struct
datatype binder =
RelC of string * kind
- | NamedC of string * kind
+ | NamedC of string * int * kind * con option
| RelE of string * con
- | NamedE of string * con
+ | NamedE of string * int * con * exp option
fun mapfoldB {kind = fk, con = fc, exp = fe, bind} =
let
@@ -294,4 +294,87 @@ fun exists {kind, con, exp} k =
end
+structure Decl = struct
+
+datatype binder = datatype Exp.binder
+
+fun mapfoldB {kind = fk, con = fc, exp = fe, decl = fd, bind} =
+ let
+ val mfk = Kind.mapfold fk
+
+ fun bind' (ctx, b) =
+ let
+ val b' = case b of
+ Con.Rel x => RelC x
+ | Con.Named x => NamedC x
+ in
+ bind (ctx, b')
+ end
+ val mfc = Con.mapfoldB {kind = fk, con = fc, bind = bind'}
+
+ val mfe = Exp.mapfoldB {kind = fk, con = fc, exp = fe, bind = bind}
+
+ fun mfd ctx d acc =
+ S.bindP (mfd' ctx d acc, fd ctx)
+
+ and mfd' ctx (dAll as (d, loc)) =
+ case d of
+ DCon (x, n, k, c) =>
+ S.bind2 (mfk k,
+ fn k' =>
+ S.map2 (mfc ctx c,
+ fn c' =>
+ (DCon (x, n, k', c'), loc)))
+ | DVal (x, n, t, e) =>
+ S.bind2 (mfc ctx t,
+ fn t' =>
+ S.map2 (mfe ctx e,
+ fn e' =>
+ (DVal (x, n, t', e'), loc)))
+ in
+ mfd
+ end
+
+end
+
+structure File = struct
+
+datatype binder = datatype Exp.binder
+
+fun mapfoldB (all as {bind, ...}) =
+ let
+ val mfd = Decl.mapfoldB all
+
+ fun mff ctx ds =
+ case ds of
+ nil => S.return2 nil
+ | d :: ds' =>
+ S.bind2 (mfd ctx d,
+ fn d' =>
+ let
+ val b =
+ case #1 d' of
+ DCon (x, n, k, c) => NamedC (x, n, k, SOME c)
+ | DVal (x, n, t, e) => NamedE (x, n, t, SOME e)
+ val ctx' = bind (ctx, b)
+ in
+ S.map2 (mff ctx' ds',
+ fn ds' =>
+ d' :: ds')
+ end)
+ in
+ mff
+ end
+
+fun mapB {kind, con, exp, decl, bind} ctx ds =
+ case mapfoldB {kind = fn k => fn () => S.Continue (kind k, ()),
+ con = fn ctx => fn c => fn () => S.Continue (con ctx c, ()),
+ exp = fn ctx => fn e => fn () => S.Continue (exp ctx e, ()),
+ decl = fn ctx => fn d => fn () => S.Continue (decl ctx d, ()),
+ bind = bind} ctx ds () of
+ S.Continue (ds, ()) => ds
+ | S.Return _ => raise Fail "CoreUtil.File.mapB: Impossible"
+
+end
+
end
diff --git a/src/elab_print.sml b/src/elab_print.sml
index fcf5e747..6f1c0148 100644
--- a/src/elab_print.sml
+++ b/src/elab_print.sml
@@ -78,7 +78,7 @@ fun p_con' par env (c, _) =
p_con (E.pushCRel env x k) c])
| TRecord (CRecord (_, xcs), _) => box [string "{",
p_list (fn (x, c) =>
- box [p_con env x,
+ box [p_name env x,
space,
string ":",
space,
@@ -149,6 +149,11 @@ fun p_con' par env (c, _) =
and p_con env = p_con' false env
+and p_name env (all as (c, _)) =
+ case c of
+ CName s => string s
+ | _ => p_con env all
+
fun p_exp' par env (e, _) =
case e of
EPrim p => Prim.p_t p
diff --git a/src/main.mlton.sml b/src/main.mlton.sml
index 433b19f2..46824ab9 100644
--- a/src/main.mlton.sml
+++ b/src/main.mlton.sml
@@ -26,5 +26,5 @@
*)
val () = case CommandLine.arguments () of
- [filename] => Compiler.testElaborate filename
+ [filename] => Compiler.testReduce filename
| _ => print "Bad arguments"
diff --git a/src/reduce.sig b/src/reduce.sig
new file mode 100644
index 00000000..0a28a59a
--- /dev/null
+++ b/src/reduce.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 *)
+
+signature REDUCE = sig
+
+ val reduce : Core.file -> Core.file
+
+end
diff --git a/src/reduce.sml b/src/reduce.sml
new file mode 100644
index 00000000..a558778c
--- /dev/null
+++ b/src/reduce.sml
@@ -0,0 +1,85 @@
+(* 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 *)
+
+structure Reduce :> REDUCE = struct
+
+open Core
+
+structure E = CoreEnv
+structure U = CoreUtil
+
+val liftConInCon = E.liftConInCon
+
+val subConInCon =
+ U.Con.mapB {kind = fn k => k,
+ con = fn (xn, rep) => fn c =>
+ case c of
+ CRel xn' =>
+ if xn = xn' then
+ #1 rep
+ else
+ c
+ | _ => c,
+ bind = fn ((xn, rep), U.Con.Rel _) => (xn+1, liftConInCon 0 rep)
+ | (ctx, _) => ctx}
+
+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) => E.pushENamed env x n t eo
+
+fun kind k = k
+
+fun con env c =
+ case c of
+ 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)
+ | _ => c
+
+and reduceCon env = U.Con.mapB {kind = kind, con = con, bind = bindC} env
+
+fun exp env e = e
+
+fun decl env d = d
+
+val reduce = U.File.mapB {kind = kind, con = con, exp = exp, decl = decl, bind = bind} CoreEnv.basis
+
+end
diff --git a/src/source_print.sml b/src/source_print.sml
index 90524241..9c3b870b 100644
--- a/src/source_print.sml
+++ b/src/source_print.sml
@@ -79,7 +79,7 @@ fun p_con' par (c, _) =
p_con c])
| TRecord (CRecord xcs, _) => box [string "{",
p_list (fn (x, c) =>
- box [p_con x,
+ box [p_name x,
space,
string ":",
space,
@@ -127,6 +127,11 @@ fun p_con' par (c, _) =
and p_con c = p_con' false c
+and p_name (all as (c, _)) =
+ case c of
+ CName s => string s
+ | _ => p_con all
+
fun p_exp' par (e, _) =
case e of
EAnnot (e, t) => box [string "(",
diff --git a/src/sources b/src/sources
index 8c72870f..71ad71de 100644
--- a/src/sources
+++ b/src/sources
@@ -49,5 +49,8 @@ core_print.sml
corify.sig
corify.sml
+reduce.sig
+reduce.sml
+
compiler.sig
compiler.sml