Mercurial > urweb
changeset 29:537db4ee89f4
Translation to Cjr
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Tue, 10 Jun 2008 18:28:43 -0400 |
| parents | 104d43266b33 |
| children | e6ccf961d8a3 |
| files | src/cjr.sml src/cjr_env.sig src/cjr_env.sml src/cjr_print.sig src/cjr_print.sml src/cjrize.sig src/cjrize.sml 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_print.sig src/flat_print.sml src/flat_util.sml src/mono.sml src/mono_print.sml src/mono_util.sml src/monoize.sml src/print.sig src/reduce.sml src/sources |
| diffstat | 29 files changed, 814 insertions(+), 50 deletions(-) [+] |
line wrap: on
line diff
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/cjr.sml Tue Jun 10 18:28:43 2008 -0400 @@ -0,0 +1,64 @@ +(* 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 Cjr = struct + +type 'a located = 'a ErrorMsg.located + +datatype typ' = + TTop + | TFun + | TCode of typ * typ + | TRecord of int + | 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 int * (string * exp) list + | EField of exp * string + + | ELet of (string * typ * exp) list * exp + +withtype exp = exp' located + +datatype decl' = + DStruct of int * (string * typ) list + | 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/cjr_env.sig Tue Jun 10 18:28:43 2008 -0400 @@ -0,0 +1,55 @@ +(* 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 CJR_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 -> Cjr.typ option -> env + val lookupTNamed : env -> int -> string * Cjr.typ option + + val pushERel : env -> string -> Cjr.typ -> env + val lookupERel : env -> int -> string * Cjr.typ + val listERels : env -> (string * Cjr.typ) list + val countERels : env -> int + + val pushENamed : env -> string -> int -> Cjr.typ -> env + val lookupENamed : env -> int -> string * Cjr.typ + + val pushF : env -> int -> string -> Cjr.typ -> Cjr.typ -> env + val lookupF : env -> int -> string * Cjr.typ * Cjr.typ + + val declBinds : env -> Cjr.decl -> env + +end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/cjr_env.sml Tue Jun 10 18:28:43 2008 -0400 @@ -0,0 +1,135 @@ +(* 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 CjrEnv :> CJR_ENV = struct + +open Cjr + +structure IM = IntBinaryMap + + +exception UnboundRel of int +exception UnboundNamed of int +exception UnboundF of int + +type env = { + namedT : (string * typ option) IM.map, + + numRelE : int, + relE : (string * typ) list, + namedE : (string * typ) IM.map, + + F : (string * typ * typ) IM.map +} + +val empty = { + namedT = IM.empty, + + numRelE = 0, + relE = [], + namedE = IM.empty, + + F = IM.empty +} + +fun pushTNamed (env : env) x n co = + {namedT = IM.insert (#namedT env, n, (x, co)), + + numRelE = #numRelE env, + 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, + + numRelE = #numRelE env + 1, + 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 countERels (env : env) = #numRelE env + +fun listERels (env : env) = #relE env + +fun pushENamed (env : env) x n t = + {namedT = #namedT env, + + numRelE = #numRelE 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, + + numRelE = #numRelE 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 + | DStruct _ => env + +fun bbind env x = + case ElabEnv.lookupC ElabEnv.basis x of + ElabEnv.NotBound => raise Fail "CjrEnv.bbind: Not bound" + | ElabEnv.Rel _ => raise Fail "CjrEnv.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/cjr_print.sig Tue Jun 10 18:28:43 2008 -0400 @@ -0,0 +1,37 @@ +(* 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 C jr. language *) + +signature CJR_PRINT = sig + val p_typ : CjrEnv.env -> Cjr.typ Print.printer + val p_exp : CjrEnv.env -> Cjr.exp Print.printer + val p_decl : CjrEnv.env -> Cjr.decl Print.printer + val p_file : CjrEnv.env -> Cjr.file Print.printer + + val debug : bool ref +end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/cjr_print.sml Tue Jun 10 18:28:43 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 C jr. *) + +structure CjrPrint :> CJR_PRINT = struct + +open Print.PD +open Print + +open Cjr + +structure E = CjrEnv +structure EM = ErrorMsg + +val debug = ref false + +val dummyTyp = (TNamed 0, ErrorMsg.dummySpan) + +fun p_typ' par env (t, loc) = + case t of + TTop => + (EM.errorAt loc "Undetermined type"; + string "?") + | TFun => + (EM.errorAt loc "Undetermined function type"; + string "?->") + | TCode (t1, t2) => parenIf par (box [p_typ' true env t2, + space, + string "(*)", + space, + string "(", + p_typ env t1, + string ")"]) + | TRecord i => box [string "struct", + space, + string "__lws_", + string (Int.toString i)] + | TNamed n => + (string ("__lwt_" ^ #1 (E.lookupTNamed env n) ^ "_" ^ Int.toString n) + handle CjrEnv.UnboundNamed _ => string ("__lwt_UNBOUND__" ^ Int.toString n)) + +and p_typ env = p_typ' false env + +fun p_rel env n = string ("__lwr_" ^ #1 (E.lookupERel env n) ^ "_" ^ Int.toString (E.countERels env - n - 1)) + handle CjrEnv.UnboundRel _ => string ("__lwr_UNBOUND_" ^ Int.toString (E.countERels env - n - 1)) + +fun p_exp' par env (e, _) = + case e of + EPrim p => Prim.p_t p + | ERel n => p_rel env n + | ENamed n => + (string ("__lwn_" ^ #1 (E.lookupENamed env n) ^ "_" ^ Int.toString n) + handle CjrEnv.UnboundNamed _ => string ("__lwn_UNBOUND_" ^ Int.toString n)) + | ECode n => string ("__lwc_" ^ Int.toString n) + | EApp (e1, e2) => parenIf par (box [p_exp' true env e1, + string "(", + p_exp env e2, + string ")"]) + + | ERecord (i, xes) => box [string "({", + space, + string "struct", + space, + string ("__lws_" ^ Int.toString i), + space, + string "__lw_tmp", + space, + string "=", + space, + string "{", + p_list (fn (_, e) => + p_exp env e) xes, + string "};", + space, + string "__lw_tmp;", + space, + string "})" ] + | EField (e, x) => + box [p_exp' true env e, + string ".", + string x] + + | ELet (xes, e) => + let + val (env, pps) = foldl (fn ((x, t, e), (env, pps)) => + let + val env' = E.pushERel env x t + in + (env', + List.revAppend ([p_typ env t, + space, + p_rel env' 0, + space, + string "=", + space, + p_exp env e, + string ";", + newline], + pps)) + end) + (env, []) xes + in + box [string "({", + newline, + box (rev pps), + p_exp env e, + space, + string ";", + newline, + string "})"] + end + +and p_exp env = p_exp' false env + +fun p_decl env ((d, _) : decl) = + case d of + DStruct (n, xts) => + box [string "struct", + space, + string ("__lws_" ^ Int.toString n), + space, + string "{", + newline, + p_list_sep (box []) (fn (x, t) => box [p_typ env t, + space, + string x, + string ";", + newline]) xts, + string "};"] + + | DVal (x, n, t, e) => + box [p_typ env t, + space, + string ("__lwn_" ^ x ^ "_" ^ Int.toString n), + space, + string "=", + space, + p_exp env e, + string ";"] + | DFun (n, x, dom, ran, e) => + let + val env' = E.pushERel env x dom + in + box [p_typ env ran, + space, + string ("__lwc_" ^ Int.toString n), + string "(", + p_typ env dom, + space, + p_rel env' 0, + string ")", + space, + string "{", + newline, + box[string "return(", + p_exp env' e, + string ")"], + newline, + string "}"] + 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/cjrize.sig Tue Jun 10 18:28:43 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 CJRIZE = sig + + val cjrize : Flat.file -> Cjr.file + +end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/cjrize.sml Tue Jun 10 18:28:43 2008 -0400 @@ -0,0 +1,179 @@ +(* 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 Cjrize :> CJRIZE = struct + +structure L = Flat +structure L' = Cjr + +structure Sm :> sig + type t + + val empty : t + val find : t * (string * L.typ) list * (string * L'.typ) list -> t * int + + val declares : t -> (int * (string * L'.typ) list) list +end = struct + +structure FM = BinaryMapFn(struct + type ord_key = L.typ + val compare = FlatUtil.Typ.compare + end) + +type t = int * int FM.map * (int * (string * L'.typ) list) list + +val empty = (0, FM.empty, []) + +fun find ((n, m, ds), xts, xts') = + let + val t = (L.TRecord xts, ErrorMsg.dummySpan) + in + case FM.find (m, t) of + NONE => ((n+1, FM.insert (m, t, n), (n, xts') :: ds), n) + | SOME i => ((n, m, ds), i) + end + +fun declares (_, _, ds) = ds + +end + +fun cifyTyp ((t, loc), sm) = + case t of + L.TTop => ((L'.TTop, loc), sm) + | L.TFun (t1, t2) => + let + val (_, sm) = cifyTyp (t1, sm) + val (_, sm) = cifyTyp (t2, sm) + in + ((L'.TFun, loc), sm) + end + | L.TCode (t1, t2) => + let + val (t1, sm) = cifyTyp (t1, sm) + val (t2, sm) = cifyTyp (t2, sm) + in + ((L'.TCode (t1, t2), loc), sm) + end + | L.TRecord xts => + let + val old_xts = xts + val (xts, sm) = ListUtil.foldlMap (fn ((x, t), sm) => + let + val (t, sm) = cifyTyp (t, sm) + in + ((x, t), sm) + end) + sm xts + val (sm, si) = Sm.find (sm, old_xts, xts) + in + ((L'.TRecord si, loc), sm) + end + | L.TNamed n => ((L'.TNamed n, loc), sm) + +fun cifyExp ((e, loc), sm) = + case e of + L.EPrim p => ((L'.EPrim p, loc), sm) + | L.ERel n => ((L'.ERel n, loc), sm) + | L.ENamed n => ((L'.ENamed n, loc), sm) + | L.ECode n => ((L'.ECode n, loc), sm) + | L.EApp (e1, e2) => + let + val (e1, sm) = cifyExp (e1, sm) + val (e2, sm) = cifyExp (e2, sm) + in + ((L'.EApp (e1, e2), loc), sm) + end + + | L.ERecord xes => + let + val old_xts = map (fn (x, _, t) => (x, t)) xes + + val (xets, sm) = ListUtil.foldlMap (fn ((x, e, t), sm) => + let + val (e, sm) = cifyExp (e, sm) + val (t, sm) = cifyTyp (t, sm) + in + ((x, e, t), sm) + end) + sm xes + + val (sm, si) = Sm.find (sm, old_xts, map (fn (x, _, t) => (x, t)) xets) + + val xes = map (fn (x, e, _) => (x, e)) xets + val xes = ListMergeSort.sort (fn ((x1, _), (x2, _)) => String.compare (x1, x2) = GREATER) xes + in + ((L'.ERecord (si, xes), loc), sm) + end + | L.EField (e, x) => + let + val (e, sm) = cifyExp (e, sm) + in + ((L'.EField (e, x), loc), sm) + end + + | L.ELet (xes, e) => + let + val (xes, sm) = ListUtil.foldlMap (fn ((x, t, e), sm) => + let + val (t, sm) = cifyTyp (t, sm) + val (e, sm) = cifyExp (e, sm) + in + ((x, t, e), sm) + end) + sm xes + val (e, sm) = cifyExp (e, sm) + in + ((L'.ELet (xes, e), loc), sm) + end + +fun cifyDecl ((d, loc), sm) = + case d of + L.DVal (x, n, t, e) => + let + val (t, sm) = cifyTyp (t, sm) + val (e, sm) = cifyExp (e, sm) + in + ((L'.DVal (x, n, t, e), loc), sm) + end + | L.DFun (n, x, dom, ran, e) => + let + val (dom, sm) = cifyTyp (dom, sm) + val (ran, sm) = cifyTyp (ran, sm) + val (e, sm) = cifyExp (e, sm) + in + ((L'.DFun (n, x, dom, ran, e), loc), sm) + end + +fun cjrize ds = + let + val (ds, sm) = ListUtil.foldlMap cifyDecl Sm.empty ds + in + List.revAppend (map (fn v => (L'.DStruct v, ErrorMsg.dummySpan)) (Sm.declares sm), + ds) + end + +end
--- a/src/cloconv.sml Tue Jun 10 16:22:46 2008 -0400 +++ b/src/cloconv.sml Tue Jun 10 18:28:43 2008 -0400 @@ -115,13 +115,13 @@ 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'.ELet ([("closure", (L'.TTop, loc), e1), + ("arg", (L'.TTop, loc), liftExpInExp 0 e2), + ("code", (L'.TTop, loc), (L'.EField ((L'.ERel 1, loc), "func"), loc)), + ("env", (L'.TTop, loc), (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) + (L'.ERecord [("env", (L'.ERel 0, loc), (L'.TTop, loc)), + ("arg", (L'.ERel 2, loc), (L'.TTop, loc))], loc)), loc)), loc), D) end | L.EAbs (x, dom, ran, e) => let @@ -145,25 +145,27 @@ 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))], + val body = (L'.ELet ([("env", (L'.TTop, loc), (L'.EField ((L'.ERel 0, loc), "env"), loc)), + ("arg", (L'.TTop, loc), (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)), + ((L'.ERecord [("code", (L'.ECode fi, loc), (L'.TTop, loc)), ("env", (L'.ERecord (map (fn n => ("fv" ^ Int.toString n, - (L'.ERel (n-1), loc))) ns), loc))], loc), D) + (L'.ERel (n-1), loc), + #2 (E.lookupERel env (n-1)))) ns), loc), + envT)], loc), D) end | L.ERecord xes => let - val (xes, D) = ListUtil.foldlMap (fn ((x, e), D) => + val (xes, D) = ListUtil.foldlMap (fn ((x, e, t), D) => let val (e, D) = ccExp env (e, D) in - ((x, e), D) + ((x, e, ccTyp t), D) end) D xes in ((L'.ERecord xes, loc), D)
--- a/src/compiler.sig Tue Jun 10 16:22:46 2008 -0400 +++ b/src/compiler.sig Tue Jun 10 18:28:43 2008 -0400 @@ -29,6 +29,8 @@ signature COMPILER = sig + val compile : string -> unit + 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 @@ -36,6 +38,7 @@ 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 cjrize : ElabEnv.env -> CoreEnv.env -> string -> Cjr.file option val testParse : string -> unit val testElaborate : string -> unit @@ -44,5 +47,6 @@ val testShake : string -> unit val testMonoize : string -> unit val testCloconv : string -> unit + val testCjrize : string -> unit end
--- a/src/compiler.sml Tue Jun 10 16:22:46 2008 -0400 +++ b/src/compiler.sml Tue Jun 10 18:28:43 2008 -0400 @@ -112,6 +112,15 @@ else SOME (Cloconv.cloconv file) +fun cjrize eenv cenv filename = + case cloconv eenv cenv filename of + NONE => NONE + | SOME file => + if ErrorMsg.anyErrors () then + NONE + else + SOME (Cjrize.cjrize file) + fun testParse filename = case parse filename of NONE => print "Failed\n" @@ -173,4 +182,25 @@ handle FlatEnv.UnboundNamed n => print ("Unbound named " ^ Int.toString n ^ "\n") +fun testCjrize filename = + (case cjrize ElabEnv.basis CoreEnv.basis filename of + NONE => print "Failed\n" + | SOME file => + (Print.print (CjrPrint.p_file CjrEnv.basis file); + print "\n")) + handle CjrEnv.UnboundNamed n => + print ("Unbound named " ^ Int.toString n ^ "\n") + +fun compile filename = + case cjrize ElabEnv.basis CoreEnv.basis filename of + NONE => () + | SOME file => + let + val outf = TextIO.openOut "/tmp/lacweb.c" + val s = TextIOPP.openOut {dst = outf, wid = 80} + in + Print.fprint s (CjrPrint.p_file CjrEnv.basis file); + TextIO.closeOut outf + end + end
--- a/src/core.sml Tue Jun 10 16:22:46 2008 -0400 +++ b/src/core.sml Tue Jun 10 18:28:43 2008 -0400 @@ -63,7 +63,7 @@ | ECApp of exp * con | ECAbs of string * kind * exp - | ERecord of (con * exp) list + | ERecord of (con * exp * con) list | EField of exp * con * { field : con, rest : con } withtype exp = exp' located
--- a/src/core_print.sml Tue Jun 10 16:22:46 2008 -0400 +++ b/src/core_print.sml Tue Jun 10 18:28:43 2008 -0400 @@ -184,7 +184,7 @@ p_exp (E.pushCRel env x k) e]) | ERecord xes => box [string "{", - p_list (fn (x, e) => + p_list (fn (x, e, _) => box [p_name env x, space, string "=",
--- a/src/core_util.sml Tue Jun 10 16:22:46 2008 -0400 +++ b/src/core_util.sml Tue Jun 10 18:28:43 2008 -0400 @@ -245,12 +245,14 @@ (ECAbs (x, k', e'), loc))) | ERecord xes => - S.map2 (ListUtil.mapfold (fn (x, e) => + S.map2 (ListUtil.mapfold (fn (x, e, t) => S.bind2 (mfc ctx x, fn x' => - S.map2 (mfe ctx e, - fn e' => - (x', e')))) + S.bind2 (mfe ctx e, + fn e' => + S.map2 (mfc ctx t, + fn t' => + (x', e', t'))))) xes, fn xes' => (ERecord xes', loc))
--- a/src/corify.sml Tue Jun 10 16:22:46 2008 -0400 +++ b/src/corify.sml Tue Jun 10 18:28:43 2008 -0400 @@ -72,7 +72,7 @@ | L.ECApp (e1, c) => (L'.ECApp (corifyExp e1, corifyCon c), loc) | L.ECAbs (_, x, k, e1) => (L'.ECAbs (x, corifyKind k, corifyExp e1), loc) - | L.ERecord xes => (L'.ERecord (map (fn (c, e) => (corifyCon c, corifyExp e)) xes), loc) + | L.ERecord xes => (L'.ERecord (map (fn (c, e, t) => (corifyCon c, corifyExp e, corifyCon t)) xes), loc) | L.EField (e1, c, {field, rest}) => (L'.EField (corifyExp e1, corifyCon c, {field = corifyCon field, rest = corifyCon rest}), loc)
--- a/src/elab.sml Tue Jun 10 16:22:46 2008 -0400 +++ b/src/elab.sml Tue Jun 10 18:28:43 2008 -0400 @@ -73,7 +73,7 @@ | ECApp of exp * con | ECAbs of explicitness * string * kind * exp - | ERecord of (con * exp) list + | ERecord of (con * exp * con) list | EField of exp * con * { field : con, rest : con } | EError
--- a/src/elab_print.sml Tue Jun 10 16:22:46 2008 -0400 +++ b/src/elab_print.sml Tue Jun 10 18:28:43 2008 -0400 @@ -199,7 +199,7 @@ p_exp (E.pushCRel env x k) e]) | ERecord xes => box [string "{", - p_list (fn (x, e) => + p_list (fn (x, e, _) => box [p_name env x, space, string "=",
--- a/src/elab_util.sml Tue Jun 10 16:22:46 2008 -0400 +++ b/src/elab_util.sml Tue Jun 10 18:28:43 2008 -0400 @@ -237,12 +237,14 @@ (ECAbs (expl, x, k', e'), loc))) | ERecord xes => - S.map2 (ListUtil.mapfold (fn (x, e) => + S.map2 (ListUtil.mapfold (fn (x, e, t) => S.bind2 (mfc ctx x, fn x' => - S.map2 (mfe ctx e, + S.bind2 (mfe ctx e, fn e' => - (x', e')))) + S.map2 (mfc ctx t, + fn t' => + (x', e', t'))))) xes, fn xes' => (ERecord xes', loc))
--- a/src/elaborate.sml Tue Jun 10 16:22:46 2008 -0400 +++ b/src/elaborate.sml Tue Jun 10 18:28:43 2008 -0400 @@ -704,7 +704,7 @@ | _ => raise Fail "typeof: Bad ECApp") | L'.ECAbs (expl, x, k, e1) => (L'.TCFun (expl, x, k, typeof (E.pushCRel env x k) e1), loc) - | L'.ERecord xes => (L'.TRecord (L'.CRecord (ktype, map (fn (x, e) => (x, typeof env e)) xes), loc), loc) + | L'.ERecord xes => (L'.TRecord (L'.CRecord (ktype, map (fn (x, _, t) => (x, t)) xes), loc), loc) | L'.EField (_, _, {field, ...}) => field | L'.EError => cerror @@ -821,7 +821,7 @@ (x', e', et) end) xes in - ((L'.ERecord (map (fn (x', e', _) => (x', e')) xes'), loc), + ((L'.ERecord xes', loc), (L'.TRecord (L'.CRecord (ktype, map (fn (x', _, et) => (x', et)) xes'), loc), loc)) end
--- a/src/flat.sml Tue Jun 10 16:22:46 2008 -0400 +++ b/src/flat.sml Tue Jun 10 18:28:43 2008 -0400 @@ -30,7 +30,8 @@ type 'a located = 'a ErrorMsg.located datatype typ' = - TFun of typ * typ + TTop + | TFun of typ * typ | TCode of typ * typ | TRecord of (string * typ) list | TNamed of int @@ -44,10 +45,10 @@ | ECode of int | EApp of exp * exp - | ERecord of (string * exp) list + | ERecord of (string * exp * typ) list | EField of exp * string - | ELet of (string * exp) list * exp + | ELet of (string * typ * exp) list * exp withtype exp = exp' located
--- a/src/flat_print.sig Tue Jun 10 16:22:46 2008 -0400 +++ b/src/flat_print.sig Tue Jun 10 18:28:43 2008 -0400 @@ -35,4 +35,3 @@ val debug : bool ref end -
--- a/src/flat_print.sml Tue Jun 10 16:22:46 2008 -0400 +++ b/src/flat_print.sml Tue Jun 10 18:28:43 2008 -0400 @@ -42,7 +42,8 @@ fun p_typ' par env (t, _) = case t of - TFun (t1, t2) => parenIf par (box [p_typ' true env t1, + TTop => string "?" + | TFun (t1, t2) => parenIf par (box [p_typ' true env t1, space, string "->", space, @@ -88,7 +89,7 @@ p_exp' true env e2]) | ERecord xes => box [string "{", - p_list (fn (x, e) => + p_list (fn (x, e, _) => box [string x, space, string "=", @@ -102,7 +103,7 @@ | ELet (xes, e) => let - val (env, pps) = foldl (fn ((x, e), (env, pps)) => + val (env, pps) = foldl (fn ((x, _, e), (env, pps)) => (E.pushERel env x dummyTyp, List.revAppend ([space, string "val",
--- a/src/flat_util.sml Tue Jun 10 16:22:46 2008 -0400 +++ b/src/flat_util.sml Tue Jun 10 18:28:43 2008 -0400 @@ -48,7 +48,8 @@ fun compare ((t1, _), (t2, _)) = case (t1, t2) of - (TFun (d1, r1), TFun (d2, r2)) => + (TTop, TTop) => EQUAL + | (TFun (d1, r1), TFun (d2, r2)) => join (compare (d1, d2), fn () => compare (r1, r2)) | (TCode (d1, r1), TCode (d2, r2)) => join (compare (d1, d2), fn () => compare (r1, r2)) @@ -61,6 +62,9 @@ end | (TNamed n1, TNamed n2) => Int.compare (n1, n2) + | (TTop, _) => LESS + | (_, TTop) => GREATER + | (TFun _, _) => LESS | (_, TFun _) => GREATER @@ -83,7 +87,8 @@ and mft' (cAll as (c, loc)) = case c of - TFun (t1, t2) => + TTop => S.return2 cAll + | TFun (t1, t2) => S.bind2 (mft t1, fn t1' => S.map2 (mft t2, @@ -156,10 +161,12 @@ (EApp (e1', e2'), loc))) | ERecord xes => - S.map2 (ListUtil.mapfold (fn (x, e) => - S.map2 (mfe ctx e, + S.map2 (ListUtil.mapfold (fn (x, e, t) => + S.bind2 (mfe ctx e, fn e' => - (x, e'))) + S.map2 (mft t, + fn t' => + (x, e', t')))) xes, fn xes' => (ERecord xes', loc)) @@ -169,10 +176,12 @@ (EField (e', x), loc)) | ELet (xes, e) => - S.bind2 (ListUtil.mapfold (fn (x, e) => - S.map2 (mfe ctx e, - fn e' => - (x, e'))) + S.bind2 (ListUtil.mapfold (fn (x, t, e) => + S.bind2 (mft t, + fn t' => + S.map2 (mfe ctx e, + fn e' => + (x, t', e')))) xes, fn xes' => S.map2 (mfe ctx e,
--- a/src/mono.sml Tue Jun 10 16:22:46 2008 -0400 +++ b/src/mono.sml Tue Jun 10 18:28:43 2008 -0400 @@ -43,7 +43,7 @@ | EApp of exp * exp | EAbs of string * typ * typ * exp - | ERecord of (string * exp) list + | ERecord of (string * exp * typ) list | EField of exp * string withtype exp = exp' located
--- a/src/mono_print.sml Tue Jun 10 16:22:46 2008 -0400 +++ b/src/mono_print.sml Tue Jun 10 18:28:43 2008 -0400 @@ -90,7 +90,7 @@ p_exp (E.pushERel env x t) e]) | ERecord xes => box [string "{", - p_list (fn (x, e) => + p_list (fn (x, e, _) => box [string x, space, string "=",
--- a/src/mono_util.sml Tue Jun 10 16:22:46 2008 -0400 +++ b/src/mono_util.sml Tue Jun 10 18:28:43 2008 -0400 @@ -114,10 +114,12 @@ (EAbs (x, dom', ran', e'), loc)))) | ERecord xes => - S.map2 (ListUtil.mapfold (fn (x, e) => - S.map2 (mfe ctx e, + S.map2 (ListUtil.mapfold (fn (x, e, t) => + S.bind2 (mfe ctx e, fn e' => - (x, e'))) + S.map2 (mft t, + fn t' => + (x, e', t')))) xes, fn xes' => (ERecord xes', loc))
--- a/src/monoize.sml Tue Jun 10 16:22:46 2008 -0400 +++ b/src/monoize.sml Tue Jun 10 18:28:43 2008 -0400 @@ -91,7 +91,7 @@ | L.ECApp _ => poly () | L.ECAbs _ => poly () - | L.ERecord xes => (L'.ERecord (map (fn (x, e) => (monoName env x, monoExp env e)) xes), loc) + | L.ERecord xes => (L'.ERecord (map (fn (x, e, t) => (monoName env x, monoExp env e, monoType env t)) xes), loc) | L.EField (e, x, _) => (L'.EField (monoExp env e, monoName env x), loc) end
--- a/src/print.sig Tue Jun 10 16:22:46 2008 -0400 +++ b/src/print.sig Tue Jun 10 18:28:43 2008 -0400 @@ -30,6 +30,8 @@ signature PRINT = sig structure PD : PP_DESC where type PPS.token = string + and type PPS.device = TextIOPP.device + and type PPS.stream = TextIOPP.stream type 'a printer = 'a -> PD.pp_desc
--- a/src/reduce.sml Tue Jun 10 16:22:46 2008 -0400 +++ b/src/reduce.sml Tue Jun 10 18:28:43 2008 -0400 @@ -145,9 +145,9 @@ #1 (reduceExp env (subConInExp (0, c) e1)) | EField ((ERecord xes, _), (CName x, _), _) => - (case List.find (fn ((CName x', _), _) => x' = x + (case List.find (fn ((CName x', _), _, _) => x' = x | _ => false) xes of - SOME (_, e) => #1 e + SOME (_, e, _) => #1 e | NONE => e) | _ => e