# HG changeset patch # User Adam Chlipala # Date 1212954464 14400 # Node ID 1ab48e37d0eff1fff090605d5495fb657b9bdd3f # Parent e634ae817a8ec35c62857f771701d27f593b33da Some con reducing diff -r e634ae817a8e -r 1ab48e37d0ef src/compiler.sig --- a/src/compiler.sig Sun Jun 08 14:42:12 2008 -0400 +++ b/src/compiler.sig Sun Jun 08 15:47:44 2008 -0400 @@ -32,9 +32,11 @@ 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 -r e634ae817a8e -r 1ab48e37d0ef src/compiler.sml --- a/src/compiler.sml Sun Jun 08 14:42:12 2008 -0400 +++ b/src/compiler.sml Sun Jun 08 15:47:44 2008 -0400 @@ -72,6 +72,11 @@ 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 @@ 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 -r e634ae817a8e -r 1ab48e37d0ef src/core_env.sig --- a/src/core_env.sig Sun Jun 08 14:42:12 2008 -0400 +++ b/src/core_env.sig Sun Jun 08 15:47:44 2008 -0400 @@ -27,6 +27,8 @@ signature CORE_ENV = sig + val liftConInCon : int -> Core.con -> Core.con + type env val empty : env @@ -44,8 +46,8 @@ 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 -r e634ae817a8e -r 1ab48e37d0ef src/core_env.sml --- a/src/core_env.sml Sun Jun 08 14:42:12 2008 -0400 +++ b/src/core_env.sml Sun Jun 08 15:47:44 2008 -0400 @@ -62,7 +62,7 @@ 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 @@ 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 @@ (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 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 -r e634ae817a8e -r 1ab48e37d0ef src/core_print.sml --- a/src/core_print.sml Sun Jun 08 14:42:12 2008 -0400 +++ b/src/core_print.sml Sun Jun 08 15:47:44 2008 -0400 @@ -69,7 +69,7 @@ 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 @@ 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 -r e634ae817a8e -r 1ab48e37d0ef src/core_util.sig --- a/src/core_util.sig Sun Jun 08 14:42:12 2008 -0400 +++ b/src/core_util.sig Sun Jun 08 15:47:44 2008 -0400 @@ -37,7 +37,7 @@ 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 @@ 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 @@ 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 -r e634ae817a8e -r 1ab48e37d0ef src/core_util.sml --- a/src/core_util.sml Sun Jun 08 14:42:12 2008 -0400 +++ b/src/core_util.sml Sun Jun 08 15:47:44 2008 -0400 @@ -79,7 +79,7 @@ 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 @@ 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 @@ 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 @@ 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 -r e634ae817a8e -r 1ab48e37d0ef src/elab_print.sml --- a/src/elab_print.sml Sun Jun 08 14:42:12 2008 -0400 +++ b/src/elab_print.sml Sun Jun 08 15:47:44 2008 -0400 @@ -78,7 +78,7 @@ 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 @@ 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 -r e634ae817a8e -r 1ab48e37d0ef src/main.mlton.sml --- a/src/main.mlton.sml Sun Jun 08 14:42:12 2008 -0400 +++ b/src/main.mlton.sml Sun Jun 08 15:47:44 2008 -0400 @@ -26,5 +26,5 @@ *) val () = case CommandLine.arguments () of - [filename] => Compiler.testElaborate filename + [filename] => Compiler.testReduce filename | _ => print "Bad arguments" diff -r e634ae817a8e -r 1ab48e37d0ef src/reduce.sig --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/reduce.sig Sun Jun 08 15:47:44 2008 -0400 @@ -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 -r e634ae817a8e -r 1ab48e37d0ef src/reduce.sml --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/reduce.sml Sun Jun 08 15:47:44 2008 -0400 @@ -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 -r e634ae817a8e -r 1ab48e37d0ef src/source_print.sml --- a/src/source_print.sml Sun Jun 08 14:42:12 2008 -0400 +++ b/src/source_print.sml Sun Jun 08 15:47:44 2008 -0400 @@ -79,7 +79,7 @@ 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 @@ 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 -r e634ae817a8e -r 1ab48e37d0ef src/sources --- a/src/sources Sun Jun 08 14:42:12 2008 -0400 +++ b/src/sources Sun Jun 08 15:47:44 2008 -0400 @@ -49,5 +49,8 @@ corify.sig corify.sml +reduce.sig +reduce.sml + compiler.sig compiler.sml diff -r e634ae817a8e -r 1ab48e37d0ef tests/reduce.lac --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/tests/reduce.lac Sun Jun 08 15:47:44 2008 -0400 @@ -0,0 +1,19 @@ +con c1 = int +con c2 = (fn t :: Type => t) int + +con id = fn t :: Type => t +con c3 = id int + +con fst = fn t1 :: Type => fn t2 :: Type => t1 +con c4 = fst int string + +con snd = fn t1 :: Type => fn t2 :: Type => t2 +con c5 = snd int string + +con apply = fn f :: Type -> Type => fn t :: Type => f t +con c6 = apply id int +con c7 = apply (fst int) string + +val grab = fn n :: Name => fn t :: Type => fn fs :: {Type} => + fn x : $([n = t] ++ fs) => x +val grabA = grab[#A][int][[B = string]]