Mercurial > urweb
changeset 26:4ab19c19665f
Closure conversion
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Tue, 10 Jun 2008 15:56:33 -0400 |
| parents | 0a762c73824d |
| children | 145b536fc702 |
| files | src/cloconv.sig src/cloconv.sml src/compiler.sig src/compiler.sml src/core.sml src/core_print.sml src/core_util.sml src/corify.sml src/elab.sml src/elab_print.sml src/elab_util.sml src/elaborate.sml src/flat.sml src/flat_env.sig src/flat_env.sml src/flat_print.sig src/flat_print.sml src/flat_util.sig src/flat_util.sml src/list_util.sig src/list_util.sml src/mono.sml src/mono_print.sml src/mono_util.sig src/mono_util.sml src/monoize.sml src/reduce.sml src/sources tests/cloconv.lac tests/curry.lac tests/curry3.lac |
| diffstat | 31 files changed, 1609 insertions(+), 55 deletions(-) [+] |
line wrap: on
line diff
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/cloconv.sig Tue Jun 10 15:56:33 2008 -0400 @@ -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 CLOCONV = sig + + val cloconv : Mono.file -> Flat.file + +end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/cloconv.sml Tue Jun 10 15:56:33 2008 -0400 @@ -0,0 +1,195 @@ +(* 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 Cloconv :> CLOCONV = struct + +structure L = Mono +structure L' = Flat + +structure IS = IntBinarySet + +structure U = FlatUtil +structure E = FlatEnv + +open Print.PD +open Print + +val liftExpInExp = + U.Exp.mapB {typ = fn t => t, + exp = fn bound => fn e => + case e of + L'.ERel xn => + if xn < bound then + e + else + L'.ERel (xn + 1) + | _ => e, + bind = fn (bound, U.Exp.RelE _) => bound + 1 + | (bound, _) => bound} +val subExpInExp = + U.Exp.mapB {typ = fn t => t, + exp = fn (xn, rep) => fn e => + case e of + L'.ERel xn' => + if xn = xn' then + #1 rep + else + e + | _ => e, + bind = fn ((xn, rep), U.Exp.RelE _) => (xn+1, liftExpInExp 0 rep) + | (ctx, _) => ctx} + + +fun ccTyp (t, loc) = + case t of + L.TFun (t1, t2) => (L'.TFun (ccTyp t1, ccTyp t2), loc) + | L.TRecord xts => (L'.TRecord (map (fn (x, t) => (x, ccTyp t)) xts), loc) + | L.TNamed n => (L'.TNamed n, loc) + +structure Ds :> sig + type t + + val empty : t + + val exp : t -> string * int * L'.typ * L'.exp -> t + val func : t -> string * L'.typ * L'.typ * L'.exp -> t * int + val decls : t -> L'.decl list + + val enter : t -> t + val used : t * int -> t + val leave : t -> t + val listUsed : t -> int list +end = struct + +type t = int * L'.decl list * IS.set + +val empty = (0, [], IS.empty) + +fun exp (fc, ds, vm) (v as (_, _, _, (_, loc))) = (fc, (L'.DVal v, loc) :: ds, vm) + +fun func (fc, ds, vm) (x, dom, ran, e as (_, loc)) = + ((fc+1, (L'.DFun (fc, x, dom, ran, e), loc) :: ds, vm), fc) + +fun decls (_, ds, _) = rev ds + +fun enter (fc, ds, vm) = (fc, ds, IS.map (fn n => n + 1) vm) +fun used ((fc, ds, vm), n) = (fc, ds, IS.add (vm, n)) +fun leave (fc, ds, vm) = (fc, ds, IS.map (fn n => n - 1) (IS.delete (vm, 0) handle NotFound => vm)) + +fun listUsed (_, _, vm) = IS.listItems vm + +end + + +fun ccExp env ((e, loc), D) = + case e of + L.EPrim p => ((L'.EPrim p, loc), D) + | L.ERel n => ((L'.ERel n, loc), Ds.used (D, n)) + | L.ENamed n => ((L'.ENamed n, loc), D) + | L.EApp (e1, e2) => + let + val (e1, D) = ccExp env (e1, D) + val (e2, D) = ccExp env (e2, D) + in + ((L'.ELet ([("closure", e1), + ("arg", liftExpInExp 0 e2), + ("code", (L'.EField ((L'.ERel 1, loc), "func"), loc)), + ("env", (L'.EField ((L'.ERel 2, loc), "env"), loc))], + (L'.EApp ((L'.ERel 1, loc), + (L'.ERecord [("env", (L'.ERel 0, loc)), + ("arg", (L'.ERel 2, loc))], loc)), loc)), loc), D) + end + | L.EAbs (x, dom, ran, e) => + let + val dom = ccTyp dom + val ran = ccTyp ran + val (e, D) = ccExp (E.pushERel env x dom) (e, Ds.enter D) + val ns = Ds.listUsed D + val ns = List.filter (fn n => n <> 0) ns + val D = Ds.leave D + + (*val () = Print.preface ("Before", FlatPrint.p_exp FlatEnv.basis e) + val () = List.app (fn (x, t) => preface ("Bound", box [string x, + space, + string ":", + space, + FlatPrint.p_typ env t])) + (E.listERels env) + val () = List.app (fn n => preface ("Free", FlatPrint.p_exp (E.pushERel env x dom) + (L'.ERel n, loc))) ns*) + val body = foldl (fn (n, e) => + subExpInExp (n, (L'.EField ((L'.ERel 1, loc), "fv" ^ Int.toString n), loc)) e) + e ns + (*val () = Print.preface (" After", FlatPrint.p_exp FlatEnv.basis body)*) + val body = (L'.ELet ([("env", (L'.EField ((L'.ERel 0, loc), "env"), loc)), + ("arg", (L'.EField ((L'.ERel 1, loc), "arg"), loc))], + body), loc) + + val envT = (L'.TRecord (map (fn n => ("fv" ^ Int.toString n, #2 (E.lookupERel env (n-1)))) ns), loc) + val (D, fi) = Ds.func D (x, (L'.TRecord [("env", envT), ("arg", dom)], loc), ran, body) + in + ((L'.ERecord [("code", (L'.ECode fi, loc)), + ("env", (L'.ERecord (map (fn n => ("fv" ^ Int.toString n, + (L'.ERel (n-1), loc))) ns), loc))], loc), D) + end + + | L.ERecord xes => + let + val (xes, D) = ListUtil.foldlMap (fn ((x, e), D) => + let + val (e, D) = ccExp env (e, D) + in + ((x, e), D) + end) D xes + in + ((L'.ERecord xes, loc), D) + end + | L.EField (e1, x) => + let + val (e1, D) = ccExp env (e1, D) + in + ((L'.EField (e1, x), loc), D) + end + +fun ccDecl ((d, loc), D) = + case d of + L.DVal (x, n, t, e) => + let + val t = ccTyp t + val (e, D) = ccExp E.basis (e, D) + in + Ds.exp D (x, n, t, e) + end + +fun cloconv ds = + let + val D = foldl ccDecl Ds.empty ds + in + Ds.decls D + end + +end
--- a/src/compiler.sig Tue Jun 10 13:14:45 2008 -0400 +++ b/src/compiler.sig Tue Jun 10 15:56:33 2008 -0400 @@ -35,6 +35,7 @@ val reduce : ElabEnv.env -> CoreEnv.env -> string -> Core.file option val shake : ElabEnv.env -> CoreEnv.env -> string -> Core.file option val monoize : ElabEnv.env -> CoreEnv.env -> string -> Mono.file option + val cloconv : ElabEnv.env -> CoreEnv.env -> string -> Flat.file option val testParse : string -> unit val testElaborate : string -> unit @@ -42,5 +43,6 @@ val testReduce : string -> unit val testShake : string -> unit val testMonoize : string -> unit + val testCloconv : string -> unit end
--- a/src/compiler.sml Tue Jun 10 13:14:45 2008 -0400 +++ b/src/compiler.sml Tue Jun 10 15:56:33 2008 -0400 @@ -103,6 +103,15 @@ else SOME (Monoize.monoize cenv file) +fun cloconv eenv cenv filename = + case monoize eenv cenv filename of + NONE => NONE + | SOME file => + if ErrorMsg.anyErrors () then + NONE + else + SOME (Cloconv.cloconv file) + fun testParse filename = case parse filename of NONE => print "Failed\n" @@ -155,4 +164,13 @@ handle MonoEnv.UnboundNamed n => print ("Unbound named " ^ Int.toString n ^ "\n") +fun testCloconv filename = + (case cloconv ElabEnv.basis CoreEnv.basis filename of + NONE => print "Failed\n" + | SOME file => + (Print.print (FlatPrint.p_file FlatEnv.basis file); + print "\n")) + handle FlatEnv.UnboundNamed n => + print ("Unbound named " ^ Int.toString n ^ "\n") + end
--- a/src/core.sml Tue Jun 10 13:14:45 2008 -0400 +++ b/src/core.sml Tue Jun 10 15:56:33 2008 -0400 @@ -59,7 +59,7 @@ | ERel of int | ENamed of int | EApp of exp * exp - | EAbs of string * con * exp + | EAbs of string * con * con * exp | ECApp of exp * con | ECAbs of string * kind * exp
--- a/src/core_print.sml Tue Jun 10 13:14:45 2008 -0400 +++ b/src/core_print.sml Tue Jun 10 15:56:33 2008 -0400 @@ -155,17 +155,17 @@ | EApp (e1, e2) => parenIf par (box [p_exp env e1, space, p_exp' true env e2]) - | EAbs (x, t, e) => parenIf par (box [string "fn", - space, - string x, - space, - string ":", - space, - p_con env t, - space, - string "=>", - space, - p_exp (E.pushERel env x t) e]) + | EAbs (x, t, _, e) => parenIf par (box [string "fn", + space, + string x, + space, + string ":", + space, + p_con env t, + space, + string "=>", + space, + p_exp (E.pushERel env x t) e]) | ECApp (e, c) => parenIf par (box [p_exp env e, space, string "[",
--- a/src/core_util.sml Tue Jun 10 13:14:45 2008 -0400 +++ b/src/core_util.sml Tue Jun 10 15:56:33 2008 -0400 @@ -222,12 +222,14 @@ S.map2 (mfe ctx e2, fn e2' => (EApp (e1', e2'), loc))) - | EAbs (x, t, e) => - S.bind2 (mfc ctx t, - fn t' => - S.map2 (mfe (bind (ctx, RelE (x, t))) e, - fn e' => - (EAbs (x, t', e'), loc))) + | EAbs (x, dom, ran, e) => + S.bind2 (mfc ctx dom, + fn dom' => + S.bind2 (mfc ctx ran, + fn ran' => + S.map2 (mfe (bind (ctx, RelE (x, dom'))) e, + fn e' => + (EAbs (x, dom', ran', e'), loc)))) | ECApp (e, c) => S.bind2 (mfe ctx e,
--- a/src/corify.sml Tue Jun 10 13:14:45 2008 -0400 +++ b/src/corify.sml Tue Jun 10 15:56:33 2008 -0400 @@ -68,7 +68,7 @@ | L.ERel n => (L'.ERel n, loc) | L.ENamed n => (L'.ENamed n, loc) | L.EApp (e1, e2) => (L'.EApp (corifyExp e1, corifyExp e2), loc) - | L.EAbs (x, t, e1) => (L'.EAbs (x, corifyCon t, corifyExp e1), loc) + | L.EAbs (x, dom, ran, e1) => (L'.EAbs (x, corifyCon dom, corifyCon ran, corifyExp e1), loc) | L.ECApp (e1, c) => (L'.ECApp (corifyExp e1, corifyCon c), loc) | L.ECAbs (_, x, k, e1) => (L'.ECAbs (x, corifyKind k, corifyExp e1), loc)
--- a/src/elab.sml Tue Jun 10 13:14:45 2008 -0400 +++ b/src/elab.sml Tue Jun 10 15:56:33 2008 -0400 @@ -69,7 +69,7 @@ | ERel of int | ENamed of int | EApp of exp * exp - | EAbs of string * con * exp + | EAbs of string * con * con * exp | ECApp of exp * con | ECAbs of explicitness * string * kind * exp
--- a/src/elab_print.sml Tue Jun 10 13:14:45 2008 -0400 +++ b/src/elab_print.sml Tue Jun 10 15:56:33 2008 -0400 @@ -170,17 +170,17 @@ | EApp (e1, e2) => parenIf par (box [p_exp env e1, space, p_exp' true env e2]) - | EAbs (x, t, e) => parenIf par (box [string "fn", - space, - string x, - space, - string ":", - space, - p_con env t, - space, - string "=>", - space, - p_exp (E.pushERel env x t) e]) + | EAbs (x, t, _, e) => parenIf par (box [string "fn", + space, + string x, + space, + string ":", + space, + p_con env t, + space, + string "=>", + space, + p_exp (E.pushERel env x t) e]) | ECApp (e, c) => parenIf par (box [p_exp env e, space, string "[",
--- a/src/elab_util.sml Tue Jun 10 13:14:45 2008 -0400 +++ b/src/elab_util.sml Tue Jun 10 15:56:33 2008 -0400 @@ -214,13 +214,15 @@ S.map2 (mfe ctx e2, fn e2' => (EApp (e1', e2'), loc))) - | EAbs (x, t, e) => - S.bind2 (mfc ctx t, - fn t' => - S.map2 (mfe (bind (ctx, RelE (x, t))) e, - fn e' => - (EAbs (x, t', e'), loc))) - + | EAbs (x, dom, ran, e) => + S.bind2 (mfc ctx dom, + fn dom' => + S.bind2 (mfc ctx ran, + fn ran' => + S.map2 (mfe (bind (ctx, RelE (x, dom'))) e, + fn e' => + (EAbs (x, dom', ran', e'), loc)))) + | ECApp (e, c) => S.bind2 (mfe ctx e, fn e' =>
--- a/src/elaborate.sml Tue Jun 10 13:14:45 2008 -0400 +++ b/src/elaborate.sml Tue Jun 10 15:56:33 2008 -0400 @@ -697,7 +697,7 @@ (case #1 (typeof env e1) of L'.TFun (_, c) => c | _ => raise Fail "typeof: Bad EApp") - | L'.EAbs (x, t, e1) => (L'.TFun (t, typeof (E.pushERel env x t) e1), loc) + | L'.EAbs (_, _, ran, _) => ran | L'.ECApp (e1, c) => (case #1 (typeof env e1) of L'.TCFun (_, _, _, c1) => subConInCon (0, c) c1 @@ -771,7 +771,7 @@ end val (e', et) = elabExp (E.pushERel env x t') e in - ((L'.EAbs (x, t', e'), loc), + ((L'.EAbs (x, t', et, e'), loc), (L'.TFun (t', et), loc)) end | L.ECApp (e, c) =>
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/flat.sml Tue Jun 10 15:56:33 2008 -0400 @@ -0,0 +1,62 @@ +(* 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 Flat = struct + +type 'a located = 'a ErrorMsg.located + +datatype typ' = + TFun of typ * typ + | TCode of typ * typ + | TRecord of (string * typ) list + | TNamed of int + +withtype typ = typ' located + +datatype exp' = + EPrim of Prim.t + | ERel of int + | ENamed of int + | ECode of int + | EApp of exp * exp + + | ERecord of (string * exp) list + | EField of exp * string + + | ELet of (string * exp) list * exp + +withtype exp = exp' located + +datatype decl' = + DVal of string * int * typ * exp + | DFun of int * string * typ * typ * exp + +withtype decl = decl' located + +type file = decl list + +end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/flat_env.sig Tue Jun 10 15:56:33 2008 -0400 @@ -0,0 +1,54 @@ +(* 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 FLAT_ENV = sig + + type env + + val empty : env + val basis : env + + exception UnboundRel of int + exception UnboundNamed of int + exception UnboundF of int + + val pushTNamed : env -> string -> int -> Flat.typ option -> env + val lookupTNamed : env -> int -> string * Flat.typ option + + val pushERel : env -> string -> Flat.typ -> env + val lookupERel : env -> int -> string * Flat.typ + val listERels : env -> (string * Flat.typ) list + + val pushENamed : env -> string -> int -> Flat.typ -> env + val lookupENamed : env -> int -> string * Flat.typ + + val pushF : env -> int -> string -> Flat.typ -> Flat.typ -> env + val lookupF : env -> int -> string * Flat.typ * Flat.typ + + val declBinds : env -> Flat.decl -> env + +end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/flat_env.sml Tue Jun 10 15:56:33 2008 -0400 @@ -0,0 +1,126 @@ +(* 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 FlatEnv :> FLAT_ENV = struct + +open Flat + +structure IM = IntBinaryMap + + +exception UnboundRel of int +exception UnboundNamed of int +exception UnboundF of int + +type env = { + namedT : (string * typ option) IM.map, + + relE : (string * typ) list, + namedE : (string * typ) IM.map, + + F : (string * typ * typ) IM.map +} + +val empty = { + namedT = IM.empty, + + relE = [], + namedE = IM.empty, + + F = IM.empty +} + +fun pushTNamed (env : env) x n co = + {namedT = IM.insert (#namedT env, n, (x, co)), + + relE = #relE env, + namedE = #namedE env, + + F = #F env} + +fun lookupTNamed (env : env) n = + case IM.find (#namedT env, n) of + NONE => raise UnboundNamed n + | SOME x => x + +fun pushERel (env : env) x t = + {namedT = #namedT env, + + relE = (x, t) :: #relE env, + namedE = #namedE env, + + F = #F env} + +fun lookupERel (env : env) n = + (List.nth (#relE env, n)) + handle Subscript => raise UnboundRel n + +fun listERels (env : env) = #relE env + +fun pushENamed (env : env) x n t = + {namedT = #namedT env, + + relE = #relE env, + namedE = IM.insert (#namedE env, n, (x, t)), + + F = #F env} + +fun lookupENamed (env : env) n = + case IM.find (#namedE env, n) of + NONE => raise UnboundNamed n + | SOME x => x + +fun pushF (env : env) n x dom ran = + {namedT = #namedT env, + + relE = #relE env, + namedE = #namedE env, + + F = IM.insert (#F env, n, (x, dom, ran))} + +fun lookupF (env : env) n = + case IM.find (#F env, n) of + NONE => raise UnboundF n + | SOME x => x + +fun declBinds env (d, _) = + case d of + DVal (x, n, t, _) => pushENamed env x n t + | DFun (n, x, dom, ran, _) => pushF env n x dom ran + +fun bbind env x = + case ElabEnv.lookupC ElabEnv.basis x of + ElabEnv.NotBound => raise Fail "FlatEnv.bbind: Not bound" + | ElabEnv.Rel _ => raise Fail "FlatEnv.bbind: Rel" + | ElabEnv.Named (n, _) => pushTNamed env x n NONE + +val basis = empty +val basis = bbind basis "int" +val basis = bbind basis "float" +val basis = bbind basis "string" + +end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/flat_print.sig Tue Jun 10 15:56:33 2008 -0400 @@ -0,0 +1,38 @@ +(* 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. + *) + +(* Pretty-printing Laconic/Web flat-code language *) + +signature FLAT_PRINT = sig + val p_typ : FlatEnv.env -> Flat.typ Print.printer + val p_exp : FlatEnv.env -> Flat.exp Print.printer + val p_decl : FlatEnv.env -> Flat.decl Print.printer + val p_file : FlatEnv.env -> Flat.file Print.printer + + val debug : bool ref +end +
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/flat_print.sml Tue Jun 10 15:56:33 2008 -0400 @@ -0,0 +1,197 @@ +(* 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. + *) + +(* Pretty-printing flat-code Laconic/Web *) + +structure FlatPrint :> FLAT_PRINT = struct + +open Print.PD +open Print + +open Flat + +structure E = FlatEnv + +val debug = ref false + +val dummyTyp = (TNamed 0, ErrorMsg.dummySpan) + +fun p_typ' par env (t, _) = + case t of + TFun (t1, t2) => parenIf par (box [p_typ' true env t1, + space, + string "->", + space, + p_typ env t2]) + | TCode (t1, t2) => parenIf par (box [p_typ' true env t1, + space, + string "-->", + space, + p_typ env t2]) + | TRecord xcs => box [string "{", + p_list (fn (x, t) => + box [string x, + space, + string ":", + space, + p_typ env t]) xcs, + string "}"] + | TNamed n => + if !debug then + string (#1 (E.lookupTNamed env n) ^ "__" ^ Int.toString n) + else + string (#1 (E.lookupTNamed env n)) + +and p_typ env = p_typ' false env + +fun p_exp' par env (e, _) = + case e of + EPrim p => Prim.p_t p + | ERel n => + ((if !debug then + string (#1 (E.lookupERel env n) ^ "_" ^ Int.toString n) + else + string (#1 (E.lookupERel env n))) + handle E.UnboundRel _ => string ("UNBOUND" ^ Int.toString n)) + | ENamed n => + if !debug then + string (#1 (E.lookupENamed env n) ^ "__" ^ Int.toString n) + else + string (#1 (E.lookupENamed env n)) + | ECode n => string ("code$" ^ Int.toString n) + | EApp (e1, e2) => parenIf par (box [p_exp env e1, + space, + p_exp' true env e2]) + + | ERecord xes => box [string "{", + p_list (fn (x, e) => + box [string x, + space, + string "=", + space, + p_exp env e]) xes, + string "}"] + | EField (e, x) => + box [p_exp' true env e, + string ".", + string x] + + | ELet (xes, e) => + let + val (env, pps) = foldl (fn ((x, e), (env, pps)) => + (E.pushERel env x dummyTyp, + List.revAppend ([space, + string "val", + space, + string x, + space, + string "=", + space, + p_exp env e], + pps))) + (env, []) xes + in + box [string "let", + space, + box (rev pps), + space, + string "in", + space, + p_exp env e, + space, + string "end"] + end + +and p_exp env = p_exp' false env + +fun p_decl env ((d, _) : decl) = + case d of + DVal (x, n, t, e) => + let + val xp = if !debug then + box [string x, + string "__", + string (Int.toString n)] + else + string x + in + box [string "val", + space, + xp, + space, + string ":", + space, + p_typ env t, + space, + string "=", + space, + p_exp env e] + + end + | DFun (n, x, dom, ran, e) => + let + val xp = if !debug then + box [string x, + string "__", + string (Int.toString n)] + else + string x + in + box [string "fun", + space, + string "code$", + string (Int.toString n), + space, + string "(", + xp, + space, + string ":", + space, + p_typ env dom, + string ")", + space, + string ":", + space, + p_typ env ran, + space, + string "=", + space, + p_exp (E.pushERel env x dom) e] + + end + +fun p_file env file = + let + val (_, pds) = ListUtil.mapfoldl (fn (d, env) => + (E.declBinds env d, + p_decl env d)) + env file + in + p_list_sep newline (fn x => x) pds + end + +end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/flat_util.sig Tue Jun 10 15:56:33 2008 -0400 @@ -0,0 +1,122 @@ +(* 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 FLAT_UTIL = sig + +structure Typ : sig + val mapfold : (Flat.typ', 'state, 'abort) Search.mapfolder + -> (Flat.typ, 'state, 'abort) Search.mapfolder + + val map : (Flat.typ' -> Flat.typ') + -> Flat.typ -> Flat.typ + + val fold : (Flat.typ' * 'state -> 'state) + -> 'state -> Flat.typ -> 'state + + val exists : (Flat.typ' -> bool) -> Flat.typ -> bool +end + +structure Exp : sig + datatype binder = + NamedT of string * int * Flat.typ option + | RelE of string * Flat.typ + | NamedE of string * int * Flat.typ * Flat.exp option + + val mapfoldB : {typ : (Flat.typ', 'state, 'abort) Search.mapfolder, + exp : ('typtext, Flat.exp', 'state, 'abort) Search.mapfolderB, + bind : 'typtext * binder -> 'typtext} + -> ('typtext, Flat.exp, 'state, 'abort) Search.mapfolderB + val mapfold : {typ : (Flat.typ', 'state, 'abort) Search.mapfolder, + exp : (Flat.exp', 'state, 'abort) Search.mapfolder} + -> (Flat.exp, 'state, 'abort) Search.mapfolder + + val map : {typ : Flat.typ' -> Flat.typ', + exp : Flat.exp' -> Flat.exp'} + -> Flat.exp -> Flat.exp + val mapB : {typ : Flat.typ' -> Flat.typ', + exp : 'typtext -> Flat.exp' -> Flat.exp', + bind : 'typtext * binder -> 'typtext} + -> 'typtext -> (Flat.exp -> Flat.exp) + + val fold : {typ : Flat.typ' * 'state -> 'state, + exp : Flat.exp' * 'state -> 'state} + -> 'state -> Flat.exp -> 'state + + val exists : {typ : Flat.typ' -> bool, + exp : Flat.exp' -> bool} -> Flat.exp -> bool +end + +structure Decl : sig + datatype binder = datatype Exp.binder + + val mapfoldB : {typ : (Flat.typ', 'state, 'abort) Search.mapfolder, + exp : ('typtext, Flat.exp', 'state, 'abort) Search.mapfolderB, + decl : ('typtext, Flat.decl', 'state, 'abort) Search.mapfolderB, + bind : 'typtext * binder -> 'typtext} + -> ('typtext, Flat.decl, 'state, 'abort) Search.mapfolderB + val mapfold : {typ : (Flat.typ', 'state, 'abort) Search.mapfolder, + exp : (Flat.exp', 'state, 'abort) Search.mapfolder, + decl : (Flat.decl', 'state, 'abort) Search.mapfolder} + -> (Flat.decl, 'state, 'abort) Search.mapfolder + + val fold : {typ : Flat.typ' * 'state -> 'state, + exp : Flat.exp' * 'state -> 'state, + decl : Flat.decl' * 'state -> 'state} + -> 'state -> Flat.decl -> 'state +end + +structure File : sig + datatype binder = + NamedT of string * int * Flat.typ option + | RelE of string * Flat.typ + | NamedE of string * int * Flat.typ * Flat.exp option + | F of int * string * Flat.typ * Flat.typ * Flat.exp + + val mapfoldB : {typ : (Flat.typ', 'state, 'abort) Search.mapfolder, + exp : ('typtext, Flat.exp', 'state, 'abort) Search.mapfolderB, + decl : ('typtext, Flat.decl', 'state, 'abort) Search.mapfolderB, + bind : 'typtext * binder -> 'typtext} + -> ('typtext, Flat.file, 'state, 'abort) Search.mapfolderB + + val mapfold : {typ : (Flat.typ', 'state, 'abort) Search.mapfolder, + exp : (Flat.exp', 'state, 'abort) Search.mapfolder, + decl : (Flat.decl', 'state, 'abort) Search.mapfolder} + -> (Flat.file, 'state, 'abort) Search.mapfolder + + val mapB : {typ : Flat.typ' -> Flat.typ', + exp : 'typtext -> Flat.exp' -> Flat.exp', + decl : 'typtext -> Flat.decl' -> Flat.decl', + bind : 'typtext * binder -> 'typtext} + -> 'typtext -> Flat.file -> Flat.file + + val fold : {typ : Flat.typ' * 'state -> 'state, + exp : Flat.exp' * 'state -> 'state, + decl : Flat.decl' * 'state -> 'state} + -> 'state -> Flat.file -> 'state +end + +end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/flat_util.sml Tue Jun 10 15:56:33 2008 -0400 @@ -0,0 +1,286 @@ +(* 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 FlatUtil :> FLAT_UTIL = struct + +open Flat + +structure S = Search + +structure Typ = struct + +fun mapfold fc = + let + fun mft c acc = + S.bindP (mft' c acc, fc) + + and mft' (cAll as (c, loc)) = + case c of + TFun (t1, t2) => + S.bind2 (mft t1, + fn t1' => + S.map2 (mft t2, + fn t2' => + (TFun (t1', t2'), loc))) + | TCode (t1, t2) => + S.bind2 (mft t1, + fn t1' => + S.map2 (mft t2, + fn t2' => + (TCode (t1', t2'), loc))) + | TRecord xts => + S.map2 (ListUtil.mapfold (fn (x, t) => + S.map2 (mft t, + fn t' => + (x, t'))) + xts, + fn xts' => (TRecord xts', loc)) + | TNamed _ => S.return2 cAll + in + mft + end + +fun map typ c = + case mapfold (fn c => fn () => S.Continue (typ c, ())) c () of + S.Return () => raise Fail "Flat_util.Typ.map" + | S.Continue (c, ()) => c + +fun fold typ s c = + case mapfold (fn c => fn s => S.Continue (c, typ (c, s))) c s of + S.Continue (_, s) => s + | S.Return _ => raise Fail "FlatUtil.Typ.fold: Impossible" + +fun exists typ k = + case mapfold (fn c => fn () => + if typ c then + S.Return () + else + S.Continue (c, ())) k () of + S.Return _ => true + | S.Continue _ => false + +end + +structure Exp = struct + +datatype binder = + NamedT of string * int * typ option + | RelE of string * typ + | NamedE of string * int * typ * exp option + +fun mapfoldB {typ = fc, exp = fe, bind} = + let + val mft = Typ.mapfold fc + + fun mfe ctx e acc = + S.bindP (mfe' ctx e acc, fe ctx) + + and mfe' ctx (eAll as (e, loc)) = + case e of + EPrim _ => S.return2 eAll + | ERel _ => S.return2 eAll + | ENamed _ => S.return2 eAll + | ECode _ => S.return2 eAll + | EApp (e1, e2) => + S.bind2 (mfe ctx e1, + fn e1' => + S.map2 (mfe ctx e2, + fn e2' => + (EApp (e1', e2'), loc))) + + | ERecord xes => + S.map2 (ListUtil.mapfold (fn (x, e) => + S.map2 (mfe ctx e, + fn e' => + (x, e'))) + xes, + fn xes' => + (ERecord xes', loc)) + | EField (e, x) => + S.map2 (mfe ctx e, + fn e' => + (EField (e', x), loc)) + + | ELet (xes, e) => + S.bind2 (ListUtil.mapfold (fn (x, e) => + S.map2 (mfe ctx e, + fn e' => + (x, e'))) + xes, + fn xes' => + S.map2 (mfe ctx e, + fn e' => + (ELet (xes', e'), loc))) + in + mfe + end + +fun mapfold {typ = fc, exp = fe} = + mapfoldB {typ = fc, + exp = fn () => fe, + bind = fn ((), _) => ()} () + +fun mapB {typ, exp, bind} ctx e = + case mapfoldB {typ = fn c => fn () => S.Continue (typ c, ()), + exp = fn ctx => fn e => fn () => S.Continue (exp ctx e, ()), + bind = bind} ctx e () of + S.Continue (e, ()) => e + | S.Return _ => raise Fail "FlatUtil.Exp.mapB: Impossible" + +fun map {typ, exp} e = + case mapfold {typ = fn c => fn () => S.Continue (typ c, ()), + exp = fn e => fn () => S.Continue (exp e, ())} e () of + S.Return () => raise Fail "Flat_util.Exp.map" + | S.Continue (e, ()) => e + +fun fold {typ, exp} s e = + case mapfold {typ = fn c => fn s => S.Continue (c, typ (c, s)), + exp = fn e => fn s => S.Continue (e, exp (e, s))} e s of + S.Continue (_, s) => s + | S.Return _ => raise Fail "FlatUtil.Exp.fold: Impossible" + +fun exists {typ, exp} k = + case mapfold {typ = fn c => fn () => + if typ c then + S.Return () + else + S.Continue (c, ()), + exp = fn e => fn () => + if exp e then + S.Return () + else + S.Continue (e, ())} k () of + S.Return _ => true + | S.Continue _ => false + +end + +structure Decl = struct + +datatype binder = datatype Exp.binder + +fun mapfoldB {typ = fc, exp = fe, decl = fd, bind} = + let + val mft = Typ.mapfold fc + + val mfe = Exp.mapfoldB {typ = 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 + DVal (x, n, t, e) => + S.bind2 (mft t, + fn t' => + S.map2 (mfe ctx e, + fn e' => + (DVal (x, n, t', e'), loc))) + | DFun (n, x, dom, ran, e) => + S.bind2 (mft dom, + fn dom' => + S.bind2 (mft ran, + fn ran' => + S.map2 (mfe ctx e, + fn e' => + (DFun (n, x, dom', ran', e'), loc)))) + in + mfd + end + +fun mapfold {typ = fc, exp = fe, decl = fd} = + mapfoldB {typ = fc, + exp = fn () => fe, + decl = fn () => fd, + bind = fn ((), _) => ()} () + +fun fold {typ, exp, decl} s d = + case mapfold {typ = fn c => fn s => S.Continue (c, typ (c, s)), + exp = fn e => fn s => S.Continue (e, exp (e, s)), + decl = fn d => fn s => S.Continue (d, decl (d, s))} d s of + S.Continue (_, s) => s + | S.Return _ => raise Fail "FlatUtil.Decl.fold: Impossible" + +end + +structure File = struct + +datatype binder = + NamedT of string * int * typ option + | RelE of string * typ + | NamedE of string * int * typ * exp option + | F of int * string * Flat.typ * Flat.typ * Flat.exp + +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 + DVal (x, n, t, e) => NamedE (x, n, t, SOME e) + | DFun v => F v + val ctx' = bind (ctx, b) + in + S.map2 (mff ctx' ds', + fn ds' => + d' :: ds') + end) + in + mff + end + +fun mapfold {typ = fc, exp = fe, decl = fd} = + mapfoldB {typ = fc, + exp = fn () => fe, + decl = fn () => fd, + bind = fn ((), _) => ()} () + +fun mapB {typ, exp, decl, bind} ctx ds = + case mapfoldB {typ = fn c => fn () => S.Continue (typ 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 "FlatUtil.File.mapB: Impossible" + +fun fold {typ, exp, decl} s d = + case mapfold {typ = fn c => fn s => S.Continue (c, typ (c, s)), + exp = fn e => fn s => S.Continue (e, exp (e, s)), + decl = fn d => fn s => S.Continue (d, decl (d, s))} d s of + S.Continue (_, s) => s + | S.Return _ => raise Fail "FlatUtil.File.fold: Impossible" + +end + +end
--- a/src/list_util.sig Tue Jun 10 13:14:45 2008 -0400 +++ b/src/list_util.sig Tue Jun 10 15:56:33 2008 -0400 @@ -33,6 +33,8 @@ val mapfold : ('data, 'state, 'abort) Search.mapfolder -> ('data list, 'state, 'abort) Search.mapfolder + val foldlMap : ('data1 * 'state -> 'data2 * 'state) -> 'state -> 'data1 list -> 'data2 list * 'state + val search : ('a -> 'b option) -> 'a list -> 'b option end
--- a/src/list_util.sml Tue Jun 10 13:14:45 2008 -0400 +++ b/src/list_util.sml Tue Jun 10 15:56:33 2008 -0400 @@ -60,6 +60,21 @@ mf end +fun foldlMap f s = + let + fun fm (ls', s) ls = + case ls of + nil => (rev ls', s) + | h :: t => + let + val (h', s') = f (h, s) + in + fm (h' :: ls', s') t + end + in + fm ([], s) + end + fun search f = let fun s ls =
--- a/src/mono.sml Tue Jun 10 13:14:45 2008 -0400 +++ b/src/mono.sml Tue Jun 10 15:56:33 2008 -0400 @@ -41,7 +41,7 @@ | ERel of int | ENamed of int | EApp of exp * exp - | EAbs of string * typ * exp + | EAbs of string * typ * typ * exp | ERecord of (string * exp) list | EField of exp * string
--- a/src/mono_print.sml Tue Jun 10 13:14:45 2008 -0400 +++ b/src/mono_print.sml Tue Jun 10 15:56:33 2008 -0400 @@ -77,17 +77,17 @@ | EApp (e1, e2) => parenIf par (box [p_exp env e1, space, p_exp' true env e2]) - | EAbs (x, t, e) => parenIf par (box [string "fn", - space, - string x, - space, - string ":", - space, - p_typ env t, - space, - string "=>", - space, - p_exp (E.pushERel env x t) e]) + | EAbs (x, t, _, e) => parenIf par (box [string "fn", + space, + string x, + space, + string ":", + space, + p_typ env t, + space, + string "=>", + space, + p_exp (E.pushERel env x t) e]) | ERecord xes => box [string "{", p_list (fn (x, e) =>
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/mono_util.sig Tue Jun 10 15:56:33 2008 -0400 @@ -0,0 +1,118 @@ +(* 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 MONO_UTIL = sig + +structure Typ : sig + val mapfold : (Mono.typ', 'state, 'abort) Search.mapfolder + -> (Mono.typ, 'state, 'abort) Search.mapfolder + + val map : (Mono.typ' -> Mono.typ') + -> Mono.typ -> Mono.typ + + val fold : (Mono.typ' * 'state -> 'state) + -> 'state -> Mono.typ -> 'state + + val exists : (Mono.typ' -> bool) -> Mono.typ -> bool +end + +structure Exp : sig + datatype binder = + NamedT of string * int * Mono.typ option + | RelE of string * Mono.typ + | NamedE of string * int * Mono.typ * Mono.exp option + + val mapfoldB : {typ : (Mono.typ', 'state, 'abort) Search.mapfolder, + exp : ('typtext, Mono.exp', 'state, 'abort) Search.mapfolderB, + bind : 'typtext * binder -> 'typtext} + -> ('typtext, Mono.exp, 'state, 'abort) Search.mapfolderB + val mapfold : {typ : (Mono.typ', 'state, 'abort) Search.mapfolder, + exp : (Mono.exp', 'state, 'abort) Search.mapfolder} + -> (Mono.exp, 'state, 'abort) Search.mapfolder + + val map : {typ : Mono.typ' -> Mono.typ', + exp : Mono.exp' -> Mono.exp'} + -> Mono.exp -> Mono.exp + val mapB : {typ : Mono.typ' -> Mono.typ', + exp : 'typtext -> Mono.exp' -> Mono.exp', + bind : 'typtext * binder -> 'typtext} + -> 'typtext -> (Mono.exp -> Mono.exp) + + val fold : {typ : Mono.typ' * 'state -> 'state, + exp : Mono.exp' * 'state -> 'state} + -> 'state -> Mono.exp -> 'state + + val exists : {typ : Mono.typ' -> bool, + exp : Mono.exp' -> bool} -> Mono.exp -> bool +end + +structure Decl : sig + datatype binder = datatype Exp.binder + + val mapfoldB : {typ : (Mono.typ', 'state, 'abort) Search.mapfolder, + exp : ('typtext, Mono.exp', 'state, 'abort) Search.mapfolderB, + decl : ('typtext, Mono.decl', 'state, 'abort) Search.mapfolderB, + bind : 'typtext * binder -> 'typtext} + -> ('typtext, Mono.decl, 'state, 'abort) Search.mapfolderB + val mapfold : {typ : (Mono.typ', 'state, 'abort) Search.mapfolder, + exp : (Mono.exp', 'state, 'abort) Search.mapfolder, + decl : (Mono.decl', 'state, 'abort) Search.mapfolder} + -> (Mono.decl, 'state, 'abort) Search.mapfolder + + val fold : {typ : Mono.typ' * 'state -> 'state, + exp : Mono.exp' * 'state -> 'state, + decl : Mono.decl' * 'state -> 'state} + -> 'state -> Mono.decl -> 'state +end + +structure File : sig + datatype binder = datatype Exp.binder + + val mapfoldB : {typ : (Mono.typ', 'state, 'abort) Search.mapfolder, + exp : ('typtext, Mono.exp', 'state, 'abort) Search.mapfolderB, + decl : ('typtext, Mono.decl', 'state, 'abort) Search.mapfolderB, + bind : 'typtext * binder -> 'typtext} + -> ('typtext, Mono.file, 'state, 'abort) Search.mapfolderB + + val mapfold : {typ : (Mono.typ', 'state, 'abort) Search.mapfolder, + exp : (Mono.exp', 'state, 'abort) Search.mapfolder, + decl : (Mono.decl', 'state, 'abort) Search.mapfolder} + -> (Mono.file, 'state, 'abort) Search.mapfolder + + val mapB : {typ : Mono.typ' -> Mono.typ', + exp : 'typtext -> Mono.exp' -> Mono.exp', + decl : 'typtext -> Mono.decl' -> Mono.decl', + bind : 'typtext * binder -> 'typtext} + -> 'typtext -> Mono.file -> Mono.file + + val fold : {typ : Mono.typ' * 'state -> 'state, + exp : Mono.exp' * 'state -> 'state, + decl : Mono.decl' * 'state -> 'state} + -> 'state -> Mono.file -> 'state +end + +end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/mono_util.sml Tue Jun 10 15:56:33 2008 -0400 @@ -0,0 +1,263 @@ +(* 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 MonoUtil :> MONO_UTIL = struct + +open Mono + +structure S = Search + +structure Typ = struct + +fun mapfold fc = + let + fun mft c acc = + S.bindP (mft' c acc, fc) + + and mft' (cAll as (c, loc)) = + case c of + TFun (t1, t2) => + S.bind2 (mft t1, + fn t1' => + S.map2 (mft t2, + fn t2' => + (TFun (t1', t2'), loc))) + | TRecord xts => + S.map2 (ListUtil.mapfold (fn (x, t) => + S.map2 (mft t, + fn t' => + (x, t'))) + xts, + fn xts' => (TRecord xts', loc)) + | TNamed _ => S.return2 cAll + in + mft + end + +fun map typ c = + case mapfold (fn c => fn () => S.Continue (typ c, ())) c () of + S.Return () => raise Fail "Mono_util.Typ.map" + | S.Continue (c, ()) => c + +fun fold typ s c = + case mapfold (fn c => fn s => S.Continue (c, typ (c, s))) c s of + S.Continue (_, s) => s + | S.Return _ => raise Fail "MonoUtil.Typ.fold: Impossible" + +fun exists typ k = + case mapfold (fn c => fn () => + if typ c then + S.Return () + else + S.Continue (c, ())) k () of + S.Return _ => true + | S.Continue _ => false + +end + +structure Exp = struct + +datatype binder = + NamedT of string * int * typ option + | RelE of string * typ + | NamedE of string * int * typ * exp option + +fun mapfoldB {typ = fc, exp = fe, bind} = + let + val mft = Typ.mapfold fc + + fun mfe ctx e acc = + S.bindP (mfe' ctx e acc, fe ctx) + + and mfe' ctx (eAll as (e, loc)) = + case e of + EPrim _ => S.return2 eAll + | ERel _ => S.return2 eAll + | ENamed _ => S.return2 eAll + | EApp (e1, e2) => + S.bind2 (mfe ctx e1, + fn e1' => + S.map2 (mfe ctx e2, + fn e2' => + (EApp (e1', e2'), loc))) + | EAbs (x, dom, ran, e) => + S.bind2 (mft dom, + fn dom' => + S.bind2 (mft ran, + fn ran' => + S.map2 (mfe (bind (ctx, RelE (x, dom'))) e, + fn e' => + (EAbs (x, dom', ran', e'), loc)))) + + | ERecord xes => + S.map2 (ListUtil.mapfold (fn (x, e) => + S.map2 (mfe ctx e, + fn e' => + (x, e'))) + xes, + fn xes' => + (ERecord xes', loc)) + | EField (e, x) => + S.map2 (mfe ctx e, + fn e' => + (EField (e', x), loc)) + in + mfe + end + +fun mapfold {typ = fc, exp = fe} = + mapfoldB {typ = fc, + exp = fn () => fe, + bind = fn ((), _) => ()} () + +fun mapB {typ, exp, bind} ctx e = + case mapfoldB {typ = fn c => fn () => S.Continue (typ c, ()), + exp = fn ctx => fn e => fn () => S.Continue (exp ctx e, ()), + bind = bind} ctx e () of + S.Continue (e, ()) => e + | S.Return _ => raise Fail "MonoUtil.Exp.mapB: Impossible" + +fun map {typ, exp} e = + case mapfold {typ = fn c => fn () => S.Continue (typ c, ()), + exp = fn e => fn () => S.Continue (exp e, ())} e () of + S.Return () => raise Fail "Mono_util.Exp.map" + | S.Continue (e, ()) => e + +fun fold {typ, exp} s e = + case mapfold {typ = fn c => fn s => S.Continue (c, typ (c, s)), + exp = fn e => fn s => S.Continue (e, exp (e, s))} e s of + S.Continue (_, s) => s + | S.Return _ => raise Fail "MonoUtil.Exp.fold: Impossible" + +fun exists {typ, exp} k = + case mapfold {typ = fn c => fn () => + if typ c then + S.Return () + else + S.Continue (c, ()), + exp = fn e => fn () => + if exp e then + S.Return () + else + S.Continue (e, ())} k () of + S.Return _ => true + | S.Continue _ => false + +end + +structure Decl = struct + +datatype binder = datatype Exp.binder + +fun mapfoldB {typ = fc, exp = fe, decl = fd, bind} = + let + val mft = Typ.mapfold fc + + val mfe = Exp.mapfoldB {typ = 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 + DVal (x, n, t, e) => + S.bind2 (mft t, + fn t' => + S.map2 (mfe ctx e, + fn e' => + (DVal (x, n, t', e'), loc))) + in + mfd + end + +fun mapfold {typ = fc, exp = fe, decl = fd} = + mapfoldB {typ = fc, + exp = fn () => fe, + decl = fn () => fd, + bind = fn ((), _) => ()} () + +fun fold {typ, exp, decl} s d = + case mapfold {typ = fn c => fn s => S.Continue (c, typ (c, s)), + exp = fn e => fn s => S.Continue (e, exp (e, s)), + decl = fn d => fn s => S.Continue (d, decl (d, s))} d s of + S.Continue (_, s) => s + | S.Return _ => raise Fail "MonoUtil.Decl.fold: Impossible" + +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 + 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 mapfold {typ = fc, exp = fe, decl = fd} = + mapfoldB {typ = fc, + exp = fn () => fe, + decl = fn () => fd, + bind = fn ((), _) => ()} () + +fun mapB {typ, exp, decl, bind} ctx ds = + case mapfoldB {typ = fn c => fn () => S.Continue (typ 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 "MonoUtil.File.mapB: Impossible" + +fun fold {typ, exp, decl} s d = + case mapfold {typ = fn c => fn s => S.Continue (c, typ (c, s)), + exp = fn e => fn s => S.Continue (e, exp (e, s)), + decl = fn d => fn s => S.Continue (d, decl (d, s))} d s of + S.Continue (_, s) => s + | S.Return _ => raise Fail "MonoUtil.File.fold: Impossible" + +end + +end
--- a/src/monoize.sml Tue Jun 10 13:14:45 2008 -0400 +++ b/src/monoize.sml Tue Jun 10 15:56:33 2008 -0400 @@ -86,8 +86,8 @@ | L.ERel n => (L'.ERel n, loc) | L.ENamed n => (L'.ENamed n, loc) | L.EApp (e1, e2) => (L'.EApp (monoExp env e1, monoExp env e2), loc) - | L.EAbs (x, t, e) => - (L'.EAbs (x, monoType env t, monoExp (Env.pushERel env x t) e), loc) + | L.EAbs (x, dom, ran, e) => + (L'.EAbs (x, monoType env dom, monoType env ran, monoExp (Env.pushERel env x dom) e), loc) | L.ECApp _ => poly () | L.ECAbs _ => poly ()
--- a/src/reduce.sml Tue Jun 10 13:14:45 2008 -0400 +++ b/src/reduce.sml Tue Jun 10 15:56:33 2008 -0400 @@ -139,7 +139,7 @@ (_, _, SOME e') => #1 e' | _ => e) - | EApp ((EAbs (_, _, e1), loc), e2) => + | EApp ((EAbs (_, _, _, e1), loc), e2) => #1 (reduceExp env (subExpInExp (0, e2) e1)) | ECApp ((ECAbs (_, _, e1), loc), c) => #1 (reduceExp env (subConInExp (0, c) e1))
--- a/src/sources Tue Jun 10 13:14:45 2008 -0400 +++ b/src/sources Tue Jun 10 15:56:33 2008 -0400 @@ -60,11 +60,28 @@ monoize.sig monoize.sml +mono_util.sig +mono_util.sml + mono_env.sig mono_env.sml mono_print.sig mono_print.sml +flat.sml + +flat_util.sig +flat_util.sml + +flat_env.sig +flat_env.sml + +flat_print.sig +flat_print.sml + +cloconv.sig +cloconv.sml + compiler.sig compiler.sml
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/tests/cloconv.lac Tue Jun 10 15:56:33 2008 -0400 @@ -0,0 +1,1 @@ +val main = fn x : int => x