diff options
| -rw-r--r-- | src/compiler.sig | 2 | ||||
| -rw-r--r-- | src/compiler.sml | 15 | ||||
| -rw-r--r-- | src/core.sml | 79 | ||||
| -rw-r--r-- | src/core_env.sig | 52 | ||||
| -rw-r--r-- | src/core_env.sml | 140 | ||||
| -rw-r--r-- | src/core_print.sig | 39 | ||||
| -rw-r--r-- | src/core_print.sml | 264 | ||||
| -rw-r--r-- | src/core_util.sig | 88 | ||||
| -rw-r--r-- | src/core_util.sml | 297 | ||||
| -rw-r--r-- | src/corify.sig | 32 | ||||
| -rw-r--r-- | src/corify.sml | 88 | ||||
| -rw-r--r-- | src/elab_env.sml | 7 | ||||
| -rw-r--r-- | src/sources | 14 |
13 files changed, 1112 insertions, 5 deletions
diff --git a/src/compiler.sig b/src/compiler.sig index 612933b7..6a4fa466 100644 --- a/src/compiler.sig +++ b/src/compiler.sig @@ -31,8 +31,10 @@ signature COMPILER = sig val parse : string -> Source.file option val elaborate : ElabEnv.env -> string -> (ElabEnv.env * Elab.file) option + val corify : ElabEnv.env -> CoreEnv.env -> string -> Core.file option val testParse : string -> unit val testElaborate : string -> unit + val testCorify : string -> unit end diff --git a/src/compiler.sml b/src/compiler.sml index 6ea5f1dc..51fef453 100644 --- a/src/compiler.sml +++ b/src/compiler.sml @@ -66,7 +66,11 @@ fun elaborate env filename = else SOME out end - + +fun corify eenv cenv filename = + case elaborate eenv filename of + NONE => NONE + | SOME (_, file) => SOME (Corify.corify file) fun testParse filename = case parse filename of @@ -84,4 +88,13 @@ fun testElaborate filename = handle ElabEnv.UnboundNamed n => print ("Unbound named " ^ Int.toString n ^ "\n") +fun testCorify filename = + (case corify ElabEnv.basis CoreEnv.basis filename of + NONE => print "Failed\n" + | SOME file => + (Print.print (CorePrint.p_file CoreEnv.basis file); + print "\n")) + handle CoreEnv.UnboundNamed n => + print ("Unbound named " ^ Int.toString n ^ "\n") + end diff --git a/src/core.sml b/src/core.sml new file mode 100644 index 00000000..20b1bba8 --- /dev/null +++ b/src/core.sml @@ -0,0 +1,79 @@ +(* 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 Core = struct + +type 'a located = 'a ErrorMsg.located + +datatype kind' = + KType + | KArrow of kind * kind + | KName + | KRecord of kind + +withtype kind = kind' located + +datatype con' = + TFun of con * con + | TCFun of string * kind * con + | TRecord of con + + | CRel of int + | CNamed of int + | CApp of con * con + | CAbs of string * kind * con + + | CName of string + + | CRecord of kind * (con * con) list + | CConcat of con * con + +withtype con = con' located + +datatype exp' = + EPrim of Prim.t + | ERel of int + | ENamed of int + | EApp of exp * exp + | EAbs of string * con * exp + | ECApp of exp * con + | ECAbs of string * kind * exp + + | ERecord of (con * exp) list + | EField of exp * con * { field : con, rest : con } + +withtype exp = exp' located + +datatype decl' = + DCon of string * int * kind * con + | DVal of string * int * con * exp + +withtype decl = decl' located + +type file = decl list + +end diff --git a/src/core_env.sig b/src/core_env.sig new file mode 100644 index 00000000..88cb253b --- /dev/null +++ b/src/core_env.sig @@ -0,0 +1,52 @@ +(* 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 CORE_ENV = sig + + type env + + val empty : env + val basis : env + + exception UnboundRel of int + exception UnboundNamed of int + + val pushCRel : env -> string -> Core.kind -> env + val lookupCRel : env -> int -> string * Core.kind + + val pushCNamed : env -> string -> int -> Core.kind -> Core.con option -> env + val lookupCNamed : env -> int -> string * Core.kind * Core.con option + + 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 declBinds : env -> Core.decl -> env + +end diff --git a/src/core_env.sml b/src/core_env.sml new file mode 100644 index 00000000..e123c9a9 --- /dev/null +++ b/src/core_env.sml @@ -0,0 +1,140 @@ +(* 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 CoreEnv :> CORE_ENV = struct + +open Core + +structure U = CoreUtil + +structure IM = IntBinaryMap + + +(* AST utility functions *) + +val liftConInCon = + U.Con.mapB {kind = fn k => k, + con = fn bound => fn c => + case c of + CRel xn => + if xn < bound then + c + else + CRel (xn + 1) + | _ => c, + bind = fn (bound, U.Con.Rel _) => bound + 1 + | (bound, _) => bound} + +val lift = liftConInCon 0 + + +(* Back to environments *) + +exception UnboundRel of int +exception UnboundNamed of int + +type env = { + relC : (string * kind) list, + namedC : (string * kind * con option) IM.map, + + relE : (string * con) list, + namedE : (string * con) IM.map +} + +val empty = { + relC = [], + namedC = IM.empty, + + relE = [], + namedE = IM.empty +} + +fun pushCRel (env : env) x k = + {relC = (x, k) :: #relC env, + 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)} + +fun lookupCRel (env : env) n = + (List.nth (#relC env, n)) + handle Subscript => raise UnboundRel n + +fun pushCNamed (env : env) x n k co = + {relC = #relC env, + namedC = IM.insert (#namedC env, n, (x, k, co)), + + relE = #relE env, + namedE = #namedE env} + +fun lookupCNamed (env : env) n = + case IM.find (#namedC env, n) of + NONE => raise UnboundNamed n + | SOME x => x + +fun pushERel (env : env) x t = + {relC = #relC env, + namedC = #namedC env, + + relE = (x, t) :: #relE env, + namedE = #namedE env} + +fun lookupERel (env : env) n = + (List.nth (#relE env, n)) + handle Subscript => raise UnboundRel n + +fun pushENamed (env : env) x n t = + {relC = #relC env, + namedC = #namedC env, + + relE = #relE env, + namedE = IM.insert (#namedE env, n, (x, t))} + +fun lookupENamed (env : env) n = + case IM.find (#namedE env, n) of + NONE => raise UnboundNamed n + | SOME x => x + +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 + +val ktype = (KType, ErrorMsg.dummySpan) + +fun bbind env x = + case ElabEnv.lookupC ElabEnv.basis x of + ElabEnv.NotBound => raise Fail "CoreEnv.bbind: Not bound" + | ElabEnv.Rel _ => raise Fail "CoreEnv.bbind: Rel" + | ElabEnv.Named (n, _) => pushCNamed env x n ktype NONE + +val basis = empty +val basis = bbind basis "int" +val basis = bbind basis "float" +val basis = bbind basis "string" + +end diff --git a/src/core_print.sig b/src/core_print.sig new file mode 100644 index 00000000..ecc7fdeb --- /dev/null +++ b/src/core_print.sig @@ -0,0 +1,39 @@ +(* 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 internal language *) + +signature CORE_PRINT = sig + val p_kind : Core.kind Print.printer + val p_con : CoreEnv.env -> Core.con Print.printer + val p_exp : CoreEnv.env -> Core.exp Print.printer + val p_decl : CoreEnv.env -> Core.decl Print.printer + val p_file : CoreEnv.env -> Core.file Print.printer + + val debug : bool ref +end + diff --git a/src/core_print.sml b/src/core_print.sml new file mode 100644 index 00000000..1e254862 --- /dev/null +++ b/src/core_print.sml @@ -0,0 +1,264 @@ +(* 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 core Laconic/Web *) + +structure CorePrint :> CORE_PRINT = struct + +open Print.PD +open Print + +open Core + +structure E = CoreEnv + +val debug = ref false + +fun p_kind' par (k, _) = + case k of + KType => string "Type" + | KArrow (k1, k2) => parenIf par (box [p_kind' true k1, + space, + string "->", + space, + p_kind k2]) + | KName => string "Name" + | KRecord k => box [string "{", p_kind k, string "}"] + +and p_kind k = p_kind' false k + +fun p_con' par env (c, _) = + case c of + TFun (t1, t2) => parenIf par (box [p_con' true env t1, + space, + string "->", + space, + p_con env t2]) + | TCFun (x, k, c) => parenIf par (box [string x, + space, + string "::", + space, + p_kind k, + space, + string "->", + space, + p_con (E.pushCRel env x k) c]) + | TRecord (CRecord (_, xcs), _) => box [string "{", + p_list (fn (x, c) => + box [p_con env x, + space, + string ":", + space, + p_con env c]) xcs, + string "}"] + | TRecord c => box [string "$", + p_con' true env c] + + | CRel n => + if !debug then + string (#1 (E.lookupCRel env n) ^ "_" ^ Int.toString n) + else + string (#1 (E.lookupCRel env n)) + | CNamed n => + if !debug then + string (#1 (E.lookupCNamed env n) ^ "__" ^ Int.toString n) + else + string (#1 (E.lookupCNamed env n)) + + | CApp (c1, c2) => parenIf par (box [p_con env c1, + space, + p_con' true env c2]) + | CAbs (x, k, c) => parenIf par (box [string "fn", + space, + string x, + space, + string "::", + space, + p_kind k, + space, + string "=>", + space, + p_con (E.pushCRel env x k) c]) + + | CName s => box [string "#", string s] + + | CRecord (k, xcs) => + if !debug then + parenIf par (box [string "[", + p_list (fn (x, c) => + box [p_con env x, + space, + string "=", + space, + p_con env c]) xcs, + string "]::", + p_kind k]) + else + parenIf par (box [string "[", + p_list (fn (x, c) => + box [p_con env x, + space, + string "=", + space, + p_con env c]) xcs, + string "]"]) + | CConcat (c1, c2) => parenIf par (box [p_con' true env c1, + space, + string "++", + space, + p_con env c2]) + +and p_con env = p_con' 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)) + | ENamed n => + if !debug then + string (#1 (E.lookupENamed env n) ^ "__" ^ Int.toString n) + else + string (#1 (E.lookupENamed env n)) + | 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]) + | ECApp (e, c) => parenIf par (box [p_exp env e, + space, + string "[", + p_con env c, + string "]"]) + | ECAbs (x, k, e) => parenIf par (box [string "fn", + space, + string x, + space, + string "::", + space, + p_kind k, + space, + string "=>", + space, + p_exp (E.pushCRel env x k) e]) + + | ERecord xes => box [string "{", + p_list (fn (x, e) => + box [p_con env x, + space, + string "=", + space, + p_exp env e]) xes, + string "}"] + | EField (e, c, {field, rest}) => + if !debug then + box [p_exp' true env e, + string ".", + p_con' true env c, + space, + string "[", + p_con env field, + space, + string " in ", + space, + p_con env rest, + string "]"] + else + box [p_exp' true env e, + string ".", + p_con' true env c] + +and p_exp env = p_exp' false env + +fun p_decl env ((d, _) : decl) = + case d of + DCon (x, n, k, c) => + let + val xp = if !debug then + box [string x, + string "__", + string (Int.toString n)] + else + string x + in + box [string "con", + space, + xp, + space, + string "::", + space, + p_kind k, + space, + string "=", + space, + p_con env c] + end + | 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_con env t, + space, + string "=", + space, + p_exp env 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 diff --git a/src/core_util.sig b/src/core_util.sig new file mode 100644 index 00000000..a40e0664 --- /dev/null +++ b/src/core_util.sig @@ -0,0 +1,88 @@ +(* 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 CORE_UTIL = sig + +structure Kind : sig + val mapfold : (Core.kind', 'state, 'abort) Search.mapfolder + -> (Core.kind, 'state, 'abort) Search.mapfolder + val map : (Core.kind' -> Core.kind') -> Core.kind -> Core.kind + val exists : (Core.kind' -> bool) -> Core.kind -> bool +end + +structure Con : sig + datatype binder = + Rel of string * Core.kind + | Named of string * Core.kind + + val mapfoldB : {kind : (Core.kind', 'state, 'abort) Search.mapfolder, + con : ('context, Core.con', 'state, 'abort) Search.mapfolderB, + bind : 'context * binder -> 'context} + -> ('context, Core.con, 'state, 'abort) Search.mapfolderB + val mapfold : {kind : (Core.kind', 'state, 'abort) Search.mapfolder, + con : (Core.con', 'state, 'abort) Search.mapfolder} + -> (Core.con, 'state, 'abort) Search.mapfolder + + val map : {kind : Core.kind' -> Core.kind', + con : Core.con' -> Core.con'} + -> Core.con -> Core.con + + val mapB : {kind : Core.kind' -> Core.kind', + con : 'context -> Core.con' -> Core.con', + bind : 'context * binder -> 'context} + -> 'context -> (Core.con -> Core.con) + val exists : {kind : Core.kind' -> bool, + con : Core.con' -> bool} -> Core.con -> bool +end + +structure Exp : sig + datatype binder = + RelC of string * Core.kind + | NamedC of string * Core.kind + | RelE of string * Core.con + | NamedE of string * Core.con + + 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, + bind : 'context * binder -> 'context} + -> ('context, Core.exp, 'state, 'abort) Search.mapfolderB + val mapfold : {kind : (Core.kind', 'state, 'abort) Search.mapfolder, + con : (Core.con', 'state, 'abort) Search.mapfolder, + exp : (Core.exp', 'state, 'abort) Search.mapfolder} + -> (Core.exp, 'state, 'abort) Search.mapfolder + + val map : {kind : Core.kind' -> Core.kind', + con : Core.con' -> Core.con', + exp : Core.exp' -> Core.exp'} + -> Core.exp -> Core.exp + val exists : {kind : Core.kind' -> bool, + con : Core.con' -> bool, + exp : Core.exp' -> bool} -> Core.exp -> bool +end + +end diff --git a/src/core_util.sml b/src/core_util.sml new file mode 100644 index 00000000..0f7df403 --- /dev/null +++ b/src/core_util.sml @@ -0,0 +1,297 @@ +(* 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 CoreUtil :> CORE_UTIL = struct + +open Core + +structure S = Search + +structure Kind = struct + +fun mapfold f = + let + fun mfk k acc = + S.bindP (mfk' k acc, f) + + and mfk' (kAll as (k, loc)) = + case k of + KType => S.return2 kAll + + | KArrow (k1, k2) => + S.bind2 (mfk k1, + fn k1' => + S.map2 (mfk k2, + fn k2' => + (KArrow (k1', k2'), loc))) + + | KName => S.return2 kAll + + | KRecord k => + S.map2 (mfk k, + fn k' => + (KRecord k', loc)) + in + mfk + end + +fun map f k = + case mapfold (fn k => fn () => S.Continue (f k, ())) k () of + S.Return () => raise Fail "Core_util.Kind.map" + | S.Continue (k, ()) => k + +fun exists f k = + case mapfold (fn k => fn () => + if f k then + S.Return () + else + S.Continue (k, ())) k () of + S.Return _ => true + | S.Continue _ => false + +end + +structure Con = struct + +datatype binder = + Rel of string * kind + | Named of string * kind + +fun mapfoldB {kind = fk, con = fc, bind} = + let + val mfk = Kind.mapfold fk + + fun mfc ctx c acc = + S.bindP (mfc' ctx c acc, fc ctx) + + and mfc' ctx (cAll as (c, loc)) = + case c of + TFun (c1, c2) => + S.bind2 (mfc ctx c1, + fn c1' => + S.map2 (mfc ctx c2, + fn c2' => + (TFun (c1', c2'), loc))) + | TCFun (x, k, c) => + S.bind2 (mfk k, + fn k' => + S.map2 (mfc (bind (ctx, Rel (x, k))) c, + fn c' => + (TCFun (x, k', c'), loc))) + | TRecord c => + S.map2 (mfc ctx c, + fn c' => + (TRecord c', loc)) + + | CRel _ => S.return2 cAll + | CNamed _ => S.return2 cAll + | CApp (c1, c2) => + S.bind2 (mfc ctx c1, + fn c1' => + S.map2 (mfc ctx c2, + fn c2' => + (CApp (c1', c2'), loc))) + | CAbs (x, k, c) => + S.bind2 (mfk k, + fn k' => + S.map2 (mfc (bind (ctx, Rel (x, k))) c, + fn c' => + (CAbs (x, k', c'), loc))) + + | CName _ => S.return2 cAll + + | CRecord (k, xcs) => + S.bind2 (mfk k, + fn k' => + S.map2 (ListUtil.mapfold (fn (x, c) => + S.bind2 (mfc ctx x, + fn x' => + S.map2 (mfc ctx c, + fn c' => + (x', c')))) + xcs, + fn xcs' => + (CRecord (k', xcs'), loc))) + | CConcat (c1, c2) => + S.bind2 (mfc ctx c1, + fn c1' => + S.map2 (mfc ctx c2, + fn c2' => + (CConcat (c1', c2'), loc))) + in + mfc + end + +fun mapfold {kind = fk, con = fc} = + mapfoldB {kind = fk, + con = fn () => fc, + bind = fn ((), _) => ()} () + +fun map {kind, con} c = + case mapfold {kind = fn k => fn () => S.Continue (kind k, ()), + con = fn c => fn () => S.Continue (con c, ())} c () of + S.Return () => raise Fail "Core_util.Con.map" + | S.Continue (c, ()) => c + +fun mapB {kind, con, bind} ctx c = + case mapfoldB {kind = fn k => fn () => S.Continue (kind k, ()), + 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" + +fun exists {kind, con} k = + case mapfold {kind = fn k => fn () => + if kind k then + S.Return () + else + S.Continue (k, ()), + con = fn c => fn () => + if con c then + S.Return () + else + S.Continue (c, ())} k () of + S.Return _ => true + | S.Continue _ => false + +end + +structure Exp = struct + +datatype binder = + RelC of string * kind + | NamedC of string * kind + | RelE of string * con + | NamedE of string * con + +fun mapfoldB {kind = fk, con = fc, exp = fe, 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'} + + 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, 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))) + + | ECApp (e, c) => + S.bind2 (mfe ctx e, + fn e' => + S.map2 (mfc ctx c, + fn c' => + (ECApp (e', c'), loc))) + | ECAbs (x, k, e) => + S.bind2 (mfk k, + fn k' => + S.map2 (mfe (bind (ctx, RelC (x, k))) e, + fn e' => + (ECAbs (x, k', e'), loc))) + + | ERecord xes => + S.map2 (ListUtil.mapfold (fn (x, e) => + S.bind2 (mfc ctx x, + fn x' => + S.map2 (mfe ctx e, + fn e' => + (x', e')))) + xes, + fn xes' => + (ERecord xes', loc)) + | EField (e, c, {field, rest}) => + S.bind2 (mfe ctx e, + fn e' => + S.bind2 (mfc ctx c, + fn c' => + S.bind2 (mfc ctx field, + fn field' => + S.map2 (mfc ctx rest, + fn rest' => + (EField (e', c', {field = field', rest = rest'}), loc))))) + in + mfe + end + +fun mapfold {kind = fk, con = fc, exp = fe} = + mapfoldB {kind = fk, + con = fn () => fc, + exp = fn () => fe, + bind = fn ((), _) => ()} () + +fun map {kind, con, exp} e = + case mapfold {kind = fn k => fn () => S.Continue (kind k, ()), + con = fn c => fn () => S.Continue (con c, ()), + exp = fn e => fn () => S.Continue (exp e, ())} e () of + S.Return () => raise Fail "Core_util.Exp.map" + | S.Continue (e, ()) => e + +fun exists {kind, con, exp} k = + case mapfold {kind = fn k => fn () => + if kind k then + S.Return () + else + S.Continue (k, ()), + con = fn c => fn () => + if con 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 + +end diff --git a/src/corify.sig b/src/corify.sig new file mode 100644 index 00000000..8cd197ce --- /dev/null +++ b/src/corify.sig @@ -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 CORIFY = sig + + val corify : Elab.file -> Core.file + +end diff --git a/src/corify.sml b/src/corify.sml new file mode 100644 index 00000000..12972163 --- /dev/null +++ b/src/corify.sml @@ -0,0 +1,88 @@ +(* 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 Corify :> CORIFY = struct + +structure EM = ErrorMsg +structure L = Elab +structure L' = Core + +fun corifyKind (k, loc) = + case k of + L.KType => (L'.KType, loc) + | L.KArrow (k1, k2) => (L'.KArrow (corifyKind k1, corifyKind k2), loc) + | L.KName => (L'.KName, loc) + | L.KRecord k => (L'.KRecord (corifyKind k), loc) + + | L.KError => raise Fail ("corifyKind: KError at " ^ EM.spanToString loc) + | L.KUnif (_, ref (SOME k)) => corifyKind k + | L.KUnif _ => raise Fail ("corifyKind: KUnif at " ^ EM.spanToString loc) + +fun corifyCon (c, loc) = + case c of + L.TFun (t1, t2) => (L'.TFun (corifyCon t1, corifyCon t2), loc) + | L.TCFun (_, x, k, t) => (L'.TCFun (x, corifyKind k, corifyCon t), loc) + | L.TRecord c => (L'.TRecord (corifyCon c), loc) + + | L.CRel n => (L'.CRel n, loc) + | L.CNamed n => (L'.CNamed n, loc) + | L.CApp (c1, c2) => (L'.CApp (corifyCon c1, corifyCon c2), loc) + | L.CAbs (x, k, c) => (L'.CAbs (x, corifyKind k, corifyCon c), loc) + + | L.CName s => (L'.CName s, loc) + + | L.CRecord (k, xcs) => (L'.CRecord (corifyKind k, map (fn (c1, c2) => (corifyCon c1, corifyCon c2)) xcs), loc) + | L.CConcat (c1, c2) => (L'.CConcat (corifyCon c1, corifyCon c2), loc) + + | L.CError => raise Fail ("corifyCon: CError at " ^ EM.spanToString loc) + | L.CUnif (_, _, ref (SOME c)) => corifyCon c + | L.CUnif _ => raise Fail ("corifyCon: CUnif at " ^ EM.spanToString loc) + +fun corifyExp (e, loc) = + case e of + L.EPrim p => (L'.EPrim p, loc) + | 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.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.EField (e1, c, {field, rest}) => (L'.EField (corifyExp e1, corifyCon c, + {field = corifyCon field, rest = corifyCon rest}), loc) + + | L.EError => raise Fail ("corifyExp: EError at " ^ EM.spanToString loc) + +fun corifyDecl (d, loc : EM.span) = + case d of + L.DCon (x, n, k, c) => (L'.DCon (x, n, corifyKind k, corifyCon c), loc) + | L.DVal (x, n, t, e) => (L'.DVal (x, n, corifyCon t, corifyExp e), loc) + +val corify = map corifyDecl + +end diff --git a/src/elab_env.sml b/src/elab_env.sml index 2308fbb6..b7264fc7 100644 --- a/src/elab_env.sml +++ b/src/elab_env.sml @@ -29,7 +29,6 @@ structure ElabEnv :> ELAB_ENV = struct open Elab -structure L' = Elab structure U = ElabUtil structure IM = IntBinaryMap @@ -50,12 +49,12 @@ val liftConInCon = U.Con.mapB {kind = fn k => k, con = fn bound => fn c => case c of - L'.CRel xn => + CRel xn => if xn < bound then c else - L'.CRel (xn + 1) - | L'.CUnif _ => raise SynUnif + CRel (xn + 1) + | CUnif _ => raise SynUnif | _ => c, bind = fn (bound, U.Con.Rel _) => bound + 1 | (bound, _) => bound} diff --git a/src/sources b/src/sources index b9c22fd3..8c72870f 100644 --- a/src/sources +++ b/src/sources @@ -35,5 +35,19 @@ elab_print.sml elaborate.sig elaborate.sml +core.sml + +core_util.sig +core_util.sml + +core_env.sig +core_env.sml + +core_print.sig +core_print.sml + +corify.sig +corify.sml + compiler.sig compiler.sml |