# HG changeset patch # User Adam Chlipala # Date 1213884419 14400 # Node ID d16ef24de78b7d547c3ac698126ec01783696bf2 # Parent 367f058aba23573a71cc58249191720e4521179a Explify diff -r 367f058aba23 -r d16ef24de78b src/compiler.sig --- a/src/compiler.sig Tue Jun 17 17:14:21 2008 -0400 +++ b/src/compiler.sig Thu Jun 19 10:06:59 2008 -0400 @@ -33,15 +33,17 @@ val parse : string -> Source.file option val elaborate : ElabEnv.env -> string -> (Elab.file * ElabEnv.env) option - val corify : ElabEnv.env -> CoreEnv.env -> string -> Core.file option - val reduce : ElabEnv.env -> CoreEnv.env -> string -> Core.file option - val shake : ElabEnv.env -> CoreEnv.env -> string -> Core.file option + val explify : ElabEnv.env -> string -> Expl.file option + val corify : ElabEnv.env -> string -> Core.file option + val reduce : ElabEnv.env -> string -> Core.file option + val shake : ElabEnv.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 + val testExplify : string -> unit val testCorify : string -> unit val testReduce : string -> unit val testShake : string -> unit diff -r 367f058aba23 -r d16ef24de78b src/compiler.sml --- a/src/compiler.sml Tue Jun 17 17:14:21 2008 -0400 +++ b/src/compiler.sml Thu Jun 19 10:06:59 2008 -0400 @@ -67,7 +67,16 @@ SOME out end -fun corify eenv cenv filename = +fun explify eenv filename = + case elaborate eenv filename of + NONE => NONE + | SOME (file, _) => + if ErrorMsg.anyErrors () then + NONE + else + SOME (Explify.explify file) + +fun corify eenv filename = case elaborate eenv filename of NONE => NONE | SOME (file, _) => @@ -76,8 +85,8 @@ else SOME (Corify.corify file) -fun reduce eenv cenv filename = - case corify eenv cenv filename of +fun reduce eenv filename = + case corify eenv filename of NONE => NONE | SOME file => if ErrorMsg.anyErrors () then @@ -85,8 +94,8 @@ else SOME (Reduce.reduce (Shake.shake file)) -fun shake eenv cenv filename = - case reduce eenv cenv filename of +fun shake eenv filename = + case reduce eenv filename of NONE => NONE | SOME file => if ErrorMsg.anyErrors () then @@ -95,7 +104,7 @@ SOME (Shake.shake file) fun monoize eenv cenv filename = - case shake eenv cenv filename of + case shake eenv filename of NONE => NONE | SOME file => if ErrorMsg.anyErrors () then @@ -138,8 +147,17 @@ handle ElabEnv.UnboundNamed n => print ("Unbound named " ^ Int.toString n ^ "\n") +fun testExplify filename = + (case explify ElabEnv.basis filename of + NONE => print "Failed\n" + | SOME file => + (Print.print (ExplPrint.p_file ExplEnv.basis file); + print "\n")) + handle ExplEnv.UnboundNamed n => + print ("Unbound named " ^ Int.toString n ^ "\n") + fun testCorify filename = - (case corify ElabEnv.basis CoreEnv.basis filename of + (case corify ElabEnv.basis filename of NONE => print "Failed\n" | SOME file => (Print.print (CorePrint.p_file CoreEnv.basis file); @@ -148,7 +166,7 @@ print ("Unbound named " ^ Int.toString n ^ "\n") fun testReduce filename = - (case reduce ElabEnv.basis CoreEnv.basis filename of + (case reduce ElabEnv.basis filename of NONE => print "Failed\n" | SOME file => (Print.print (CorePrint.p_file CoreEnv.basis file); @@ -157,7 +175,7 @@ print ("Unbound named " ^ Int.toString n ^ "\n") fun testShake filename = - (case shake ElabEnv.basis CoreEnv.basis filename of + (case shake ElabEnv.basis filename of NONE => print "Failed\n" | SOME file => (Print.print (CorePrint.p_file CoreEnv.basis file); diff -r 367f058aba23 -r d16ef24de78b src/expl.sml --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/expl.sml Thu Jun 19 10:06:59 2008 -0400 @@ -0,0 +1,102 @@ +(* 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 Expl = 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 + | CModProj of int * string list * string + | 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 + | EModProj of int * string list * string + | EApp of exp * exp + | EAbs of string * con * con * exp + | ECApp of exp * con + | ECAbs of string * kind * exp + + | ERecord of (con * exp * con) list + | EField of exp * con * { field : con, rest : con } + +withtype exp = exp' located + +datatype sgn_item' = + SgiConAbs of string * int * kind + | SgiCon of string * int * kind * con + | SgiVal of string * int * con + | SgiStr of string * int * sgn + +and sgn' = + SgnConst of sgn_item list + | SgnVar of int + +withtype sgn_item = sgn_item' located +and sgn = sgn' located + +datatype decl' = + DCon of string * int * kind * con + | DVal of string * int * con * exp + | DSgn of string * int * sgn + | DStr of string * int * sgn * str + + and str' = + StrConst of decl list + | StrVar of int + | StrProj of str * string + +withtype decl = decl' located + and str = str' located + +type file = decl list + +end diff -r 367f058aba23 -r d16ef24de78b src/expl_env.sig --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/expl_env.sig Thu Jun 19 10:06:59 2008 -0400 @@ -0,0 +1,67 @@ +(* 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 EXPL_ENV = sig + + exception SynUnif + val liftConInCon : int -> Expl.con -> Expl.con + + type env + + val empty : env + val basis : env + + exception UnboundRel of int + exception UnboundNamed of int + + datatype 'a var = + NotBound + | Rel of int * 'a + | Named of int * 'a + + val pushCRel : env -> string -> Expl.kind -> env + val lookupCRel : env -> int -> string * Expl.kind + + val pushCNamed : env -> string -> int -> Expl.kind -> Expl.con option -> env + val lookupCNamed : env -> int -> string * Expl.kind * Expl.con option + + val pushERel : env -> string -> Expl.con -> env + val lookupERel : env -> int -> string * Expl.con + + val pushENamed : env -> string -> int -> Expl.con -> env + val lookupENamed : env -> int -> string * Expl.con + + val pushSgnNamed : env -> string -> int -> Expl.sgn -> env + val lookupSgnNamed : env -> int -> string * Expl.sgn + + val pushStrNamed : env -> string -> int -> Expl.sgn -> env + val lookupStrNamed : env -> int -> string * Expl.sgn + + val declBinds : env -> Expl.decl -> env + val sgiBinds : env -> Expl.sgn_item -> env + +end diff -r 367f058aba23 -r d16ef24de78b src/expl_env.sml --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/expl_env.sml Thu Jun 19 10:06:59 2008 -0400 @@ -0,0 +1,267 @@ +(* 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 ExplEnv :> EXPL_ENV = struct + +open Expl + +structure U = ExplUtil + +structure IM = IntBinaryMap +structure SM = BinaryMapFn(struct + type ord_key = string + val compare = String.compare + end) + +exception UnboundRel of int +exception UnboundNamed of int + + +(* AST utility functions *) + +exception SynUnif + +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) + (*| CUnif _ => raise SynUnif*) + | _ => c, + bind = fn (bound, U.Con.Rel _) => bound + 1 + | (bound, _) => bound} + +val lift = liftConInCon 0 + + +(* Back to environments *) + +datatype 'a var' = + Rel' of int * 'a + | Named' of int * 'a + +datatype 'a var = + NotBound + | Rel of int * 'a + | Named of int * 'a + +type env = { + renameC : kind var' SM.map, + relC : (string * kind) list, + namedC : (string * kind * con option) IM.map, + + renameE : con var' SM.map, + relE : (string * con) list, + namedE : (string * con) IM.map, + + renameSgn : (int * sgn) SM.map, + sgn : (string * sgn) IM.map, + + renameStr : (int * sgn) SM.map, + str : (string * sgn) IM.map +} + +val namedCounter = ref 0 + +val empty = { + renameC = SM.empty, + relC = [], + namedC = IM.empty, + + renameE = SM.empty, + relE = [], + namedE = IM.empty, + + renameSgn = SM.empty, + sgn = IM.empty, + + renameStr = SM.empty, + str = IM.empty +} + +fun pushCRel (env : env) x k = + let + val renameC = SM.map (fn Rel' (n, k) => Rel' (n+1, k) + | x => x) (#renameC env) + in + {renameC = SM.insert (renameC, x, Rel' (0, k)), + relC = (x, k) :: #relC env, + namedC = IM.map (fn (x, k, co) => (x, k, Option.map lift co)) (#namedC env), + + renameE = #renameE env, + relE = map (fn (x, c) => (x, lift c)) (#relE env), + namedE = IM.map (fn (x, c) => (x, lift c)) (#namedE env), + + renameSgn = #renameSgn env, + sgn = #sgn env, + + renameStr = #renameStr env, + str = #str env + } + end + +fun lookupCRel (env : env) n = + (List.nth (#relC env, n)) + handle Subscript => raise UnboundRel n + +fun pushCNamed (env : env) x n k co = + {renameC = SM.insert (#renameC env, x, Named' (n, k)), + relC = #relC env, + namedC = IM.insert (#namedC env, n, (x, k, co)), + + renameE = #renameE env, + relE = #relE env, + namedE = #namedE env, + + renameSgn = #renameSgn env, + sgn = #sgn env, + + renameStr = #renameStr env, + str = #str 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 = + let + val renameE = SM.map (fn Rel' (n, t) => Rel' (n+1, t) + | x => x) (#renameE env) + in + {renameC = #renameC env, + relC = #relC env, + namedC = #namedC env, + + renameE = SM.insert (renameE, x, Rel' (0, t)), + relE = (x, t) :: #relE env, + namedE = #namedE env, + + renameSgn = #renameSgn env, + sgn = #sgn env, + + renameStr = #renameStr env, + str = #str env} + end + +fun lookupERel (env : env) n = + (List.nth (#relE env, n)) + handle Subscript => raise UnboundRel n + +fun pushENamed (env : env) x n t = + {renameC = #renameC env, + relC = #relC env, + namedC = #namedC env, + + renameE = SM.insert (#renameE env, x, Named' (n, t)), + relE = #relE env, + namedE = IM.insert (#namedE env, n, (x, t)), + + renameSgn = #renameSgn env, + sgn = #sgn env, + + renameStr = #renameStr env, + str = #str env} + +fun lookupENamed (env : env) n = + case IM.find (#namedE env, n) of + NONE => raise UnboundNamed n + | SOME x => x + +fun pushSgnNamed (env : env) x n sgis = + {renameC = #renameC env, + relC = #relC env, + namedC = #namedC env, + + renameE = #renameE env, + relE = #relE env, + namedE = #namedE env, + + renameSgn = SM.insert (#renameSgn env, x, (n, sgis)), + sgn = IM.insert (#sgn env, n, (x, sgis)), + + renameStr = #renameStr env, + str = #str env} + +fun lookupSgnNamed (env : env) n = + case IM.find (#sgn env, n) of + NONE => raise UnboundNamed n + | SOME x => x + +fun pushStrNamed (env : env) x n sgis = + {renameC = #renameC env, + relC = #relC env, + namedC = #namedC env, + + renameE = #renameE env, + relE = #relE env, + namedE = #namedE env, + + renameSgn = #renameSgn env, + sgn = #sgn env, + + renameStr = SM.insert (#renameStr env, x, (n, sgis)), + str = IM.insert (#str env, n, (x, sgis))} + +fun lookupStrNamed (env : env) n = + case IM.find (#str 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 + | DSgn (x, n, sgn) => pushSgnNamed env x n sgn + | DStr (x, n, sgn, _) => pushStrNamed env x n sgn + +fun sgiBinds env (sgi, _) = + case sgi of + SgiConAbs (x, n, k) => pushCNamed env x n k NONE + | SgiCon (x, n, k, c) => pushCNamed env x n k (SOME c) + | SgiVal (x, n, t) => pushENamed env x n t + | SgiStr (x, n, sgn) => pushStrNamed env x n sgn + + +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 -r 367f058aba23 -r d16ef24de78b src/expl_print.sig --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/expl_print.sig Thu Jun 19 10:06:59 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. + *) + +signature EXPL_PRINT = sig + val p_kind : Expl.kind Print.printer + val p_con : ExplEnv.env -> Expl.con Print.printer + val p_exp : ExplEnv.env -> Expl.exp Print.printer + val p_decl : ExplEnv.env -> Expl.decl Print.printer + val p_sgn_item : ExplEnv.env -> Expl.sgn_item Print.printer + val p_file : ExplEnv.env -> Expl.file Print.printer + + val debug : bool ref +end + diff -r 367f058aba23 -r d16ef24de78b src/expl_print.sml --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/expl_print.sml Thu Jun 19 10:06:59 2008 -0400 @@ -0,0 +1,363 @@ +(* 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 elaborated Laconic/Web *) + +structure ExplPrint :> EXPL_PRINT = struct + +open Print.PD +open Print + +open Expl + +structure E = ExplEnv + +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_name 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))) + handle E.UnboundNamed _ => string ("UNBOUND_NAMED" ^ Int.toString n)) + | CModProj (m1, ms, x) => + let + val (m1x, sgn) = E.lookupStrNamed env m1 + + val m1s = if !debug then + m1x ^ "__" ^ Int.toString m1 + else + m1x + in + p_list_sep (string ".") string (m1x :: ms @ [x]) + end + + | 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 + +and p_name env (all as (c, _)) = + case c of + CName s => string s + | _ => p_con env all + +fun p_exp' par env (e, _) = + case e of + EPrim p => Prim.p_t p + | 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)) + | EModProj (m1, ms, x) => + let + val (m1x, sgn) = E.lookupStrNamed env m1 + + val m1s = if !debug then + m1x ^ "__" ^ Int.toString m1 + else + m1x + in + p_list_sep (string ".") string (m1x :: ms @ [x]) + end + + | 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_name 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_named x n = + if !debug then + box [string x, + string "__", + string (Int.toString n)] + else + string x + +fun p_sgn_item env (sgi, _) = + case sgi of + SgiConAbs (x, n, k) => box [string "con", + space, + p_named x n, + space, + string "::", + space, + p_kind k] + | SgiCon (x, n, k, c) => box [string "con", + space, + p_named x n, + space, + string "::", + space, + p_kind k, + space, + string "=", + space, + p_con env c] + | SgiVal (x, n, c) => box [string "val", + space, + p_named x n, + space, + string ":", + space, + p_con env c] + | SgiStr (x, n, sgn) => box [string "structure", + space, + p_named x n, + space, + string ":", + space, + p_sgn env sgn] + +and p_sgn env (sgn, _) = + case sgn of + SgnConst sgis => box [string "sig", + newline, + let + val (psgis, _) = ListUtil.foldlMap (fn (sgi, env) => + (p_sgn_item env sgi, + E.sgiBinds env sgi)) + env sgis + in + p_list_sep newline (fn x => x) psgis + end, + newline, + string "end"] + | SgnVar n => string (#1 (E.lookupSgnNamed env n)) + +fun p_decl env ((d, _) : decl) = + case d of + DCon (x, n, k, c) => box [string "con", + space, + p_named x n, + space, + string "::", + space, + p_kind k, + space, + string "=", + space, + p_con env c] + | DVal (x, n, t, e) => box [string "val", + space, + p_named x n, + space, + string ":", + space, + p_con env t, + space, + string "=", + space, + p_exp env e] + + | DSgn (x, n, sgn) => box [string "signature", + space, + p_named x n, + space, + string "=", + space, + p_sgn env sgn] + | DStr (x, n, sgn, str) => box [string "structure", + space, + p_named x n, + space, + string ":", + space, + p_sgn env sgn, + space, + string "=", + space, + p_str env str] + +and p_str env (str, _) = + case str of + StrConst ds => box [string "struct", + newline, + p_file env ds, + newline, + string "end"] + | StrVar n => string (#1 (E.lookupStrNamed env n)) + | StrProj (str, s) => box [p_str env str, + string ".", + string s] + +and p_file env file = + let + val (pds, _) = ListUtil.foldlMap (fn (d, env) => + (p_decl env d, + E.declBinds env d)) + env file + in + p_list_sep newline (fn x => x) pds + end + +end diff -r 367f058aba23 -r d16ef24de78b src/expl_util.sig --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/expl_util.sig Thu Jun 19 10:06:59 2008 -0400 @@ -0,0 +1,109 @@ +(* 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 EXPL_UTIL = sig + +structure Kind : sig + val mapfold : (Expl.kind', 'state, 'abort) Search.mapfolder + -> (Expl.kind, 'state, 'abort) Search.mapfolder + val exists : (Expl.kind' -> bool) -> Expl.kind -> bool +end + +structure Con : sig + datatype binder = + Rel of string * Expl.kind + | Named of string * Expl.kind + + val mapfoldB : {kind : (Expl.kind', 'state, 'abort) Search.mapfolder, + con : ('context, Expl.con', 'state, 'abort) Search.mapfolderB, + bind : 'context * binder -> 'context} + -> ('context, Expl.con, 'state, 'abort) Search.mapfolderB + val mapfold : {kind : (Expl.kind', 'state, 'abort) Search.mapfolder, + con : (Expl.con', 'state, 'abort) Search.mapfolder} + -> (Expl.con, 'state, 'abort) Search.mapfolder + + val mapB : {kind : Expl.kind' -> Expl.kind', + con : 'context -> Expl.con' -> Expl.con', + bind : 'context * binder -> 'context} + -> 'context -> (Expl.con -> Expl.con) + val map : {kind : Expl.kind' -> Expl.kind', + con : Expl.con' -> Expl.con'} + -> Expl.con -> Expl.con + val exists : {kind : Expl.kind' -> bool, + con : Expl.con' -> bool} -> Expl.con -> bool +end + +structure Exp : sig + datatype binder = + RelC of string * Expl.kind + | NamedC of string * Expl.kind + | RelE of string * Expl.con + | NamedE of string * Expl.con + + val mapfoldB : {kind : (Expl.kind', 'state, 'abort) Search.mapfolder, + con : ('context, Expl.con', 'state, 'abort) Search.mapfolderB, + exp : ('context, Expl.exp', 'state, 'abort) Search.mapfolderB, + bind : 'context * binder -> 'context} + -> ('context, Expl.exp, 'state, 'abort) Search.mapfolderB + val mapfold : {kind : (Expl.kind', 'state, 'abort) Search.mapfolder, + con : (Expl.con', 'state, 'abort) Search.mapfolder, + exp : (Expl.exp', 'state, 'abort) Search.mapfolder} + -> (Expl.exp, 'state, 'abort) Search.mapfolder + val exists : {kind : Expl.kind' -> bool, + con : Expl.con' -> bool, + exp : Expl.exp' -> bool} -> Expl.exp -> bool +end + +structure Sgn : sig + datatype binder = + RelC of string * Expl.kind + | NamedC of string * Expl.kind + | Str of string * Expl.sgn + + val mapfoldB : {kind : (Expl.kind', 'state, 'abort) Search.mapfolder, + con : ('context, Expl.con', 'state, 'abort) Search.mapfolderB, + sgn_item : ('context, Expl.sgn_item', 'state, 'abort) Search.mapfolderB, + sgn : ('context, Expl.sgn', 'state, 'abort) Search.mapfolderB, + bind : 'context * binder -> 'context} + -> ('context, Expl.sgn, 'state, 'abort) Search.mapfolderB + + + val mapfold : {kind : (Expl.kind', 'state, 'abort) Search.mapfolder, + con : (Expl.con', 'state, 'abort) Search.mapfolder, + sgn_item : (Expl.sgn_item', 'state, 'abort) Search.mapfolder, + sgn : (Expl.sgn', 'state, 'abort) Search.mapfolder} + -> (Expl.sgn, 'state, 'abort) Search.mapfolder + + val map : {kind : Expl.kind' -> Expl.kind', + con : Expl.con' -> Expl.con', + sgn_item : Expl.sgn_item' -> Expl.sgn_item', + sgn : Expl.sgn' -> Expl.sgn'} + -> Expl.sgn -> Expl.sgn + +end + +end diff -r 367f058aba23 -r d16ef24de78b src/expl_util.sml --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/expl_util.sml Thu Jun 19 10:06:59 2008 -0400 @@ -0,0 +1,377 @@ +(* 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 ExplUtil :> EXPL_UTIL = struct + +open Expl + +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 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 * Expl.kind + | Named of string * Expl.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 + | CModProj _ => 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 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 "ExplUtil.Con.mapB: Impossible" + +fun map {kind, con} s = + case mapfold {kind = fn k => fn () => S.Continue (kind k, ()), + con = fn c => fn () => S.Continue (con c, ())} s () of + S.Return () => raise Fail "ExplUtil.Con.map: Impossible" + | S.Continue (s, ()) => s + +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 * Expl.kind + | NamedC of string * Expl.kind + | RelE of string * Expl.con + | NamedE of string * Expl.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 + | EModProj _ => 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 (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' => + 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, t) => + S.bind2 (mfc ctx x, + fn x' => + S.bind2 (mfe ctx e, + fn e' => + S.map2 (mfc ctx t, + fn t' => + (x', e', t'))))) + 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 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 + +structure Sgn = struct + +datatype binder = + RelC of string * Expl.kind + | NamedC of string * Expl.kind + | Str of string * Expl.sgn + +fun mapfoldB {kind, con, sgn_item, sgn, bind} = + let + 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 con = Con.mapfoldB {kind = kind, con = con, bind = bind'} + + val kind = Kind.mapfold kind + + fun sgi ctx si acc = + S.bindP (sgi' ctx si acc, sgn_item ctx) + + and sgi' ctx (si, loc) = + case si of + SgiConAbs (x, n, k) => + S.map2 (kind k, + fn k' => + (SgiConAbs (x, n, k'), loc)) + | SgiCon (x, n, k, c) => + S.bind2 (kind k, + fn k' => + S.map2 (con ctx c, + fn c' => + (SgiCon (x, n, k', c'), loc))) + | SgiVal (x, n, c) => + S.map2 (con ctx c, + fn c' => + (SgiVal (x, n, c'), loc)) + | SgiStr (x, n, s) => + S.map2 (sg ctx s, + fn s' => + (SgiStr (x, n, s'), loc)) + + and sg ctx s acc = + S.bindP (sg' ctx s acc, sgn ctx) + + and sg' ctx (sAll as (s, loc)) = + case s of + SgnConst sgis => + S.map2 (ListUtil.mapfoldB (fn (ctx, si) => + (case #1 si of + SgiConAbs (x, _, k) => + bind (ctx, NamedC (x, k)) + | SgiCon (x, _, k, _) => + bind (ctx, NamedC (x, k)) + | SgiVal _ => ctx + | SgiStr (x, _, sgn) => + bind (ctx, Str (x, sgn)), + sgi ctx si)) ctx sgis, + fn sgis' => + (SgnConst sgis', loc)) + + | SgnVar _ => S.return2 sAll + in + sg + end + +fun mapfold {kind, con, sgn_item, sgn} = + mapfoldB {kind = kind, + con = fn () => con, + sgn_item = fn () => sgn_item, + sgn = fn () => sgn, + bind = fn ((), _) => ()} () + +fun map {kind, con, sgn_item, sgn} s = + case mapfold {kind = fn k => fn () => S.Continue (kind k, ()), + con = fn c => fn () => S.Continue (con c, ()), + sgn_item = fn si => fn () => S.Continue (sgn_item si, ()), + sgn = fn s => fn () => S.Continue (sgn s, ())} s () of + S.Return () => raise Fail "Expl_util.Sgn.map" + | S.Continue (s, ()) => s + +end + +end diff -r 367f058aba23 -r d16ef24de78b src/explify.sig --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/explify.sig Thu Jun 19 10:06:59 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 EXPLIFY = sig + + val explify : Elab.file -> Expl.file + +end diff -r 367f058aba23 -r d16ef24de78b src/explify.sml --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/explify.sml Thu Jun 19 10:06:59 2008 -0400 @@ -0,0 +1,114 @@ +(* 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 Explify :> EXPLIFY = struct + +structure EM = ErrorMsg +structure L = Elab +structure L' = Expl + +fun explifyKind (k, loc) = + case k of + L.KType => (L'.KType, loc) + | L.KArrow (k1, k2) => (L'.KArrow (explifyKind k1, explifyKind k2), loc) + | L.KName => (L'.KName, loc) + | L.KRecord k => (L'.KRecord (explifyKind k), loc) + + | L.KError => raise Fail ("explifyKind: KError at " ^ EM.spanToString loc) + | L.KUnif (_, ref (SOME k)) => explifyKind k + | L.KUnif _ => raise Fail ("explifyKind: KUnif at " ^ EM.spanToString loc) + +fun explifyCon (c, loc) = + case c of + L.TFun (t1, t2) => (L'.TFun (explifyCon t1, explifyCon t2), loc) + | L.TCFun (_, x, k, t) => (L'.TCFun (x, explifyKind k, explifyCon t), loc) + | L.TRecord c => (L'.TRecord (explifyCon c), loc) + + | L.CRel n => (L'.CRel n, loc) + | L.CNamed n => (L'.CNamed n, loc) + | L.CModProj (m, ms, x) => (L'.CModProj (m, ms, x), loc) + + | L.CApp (c1, c2) => (L'.CApp (explifyCon c1, explifyCon c2), loc) + | L.CAbs (x, k, c) => (L'.CAbs (x, explifyKind k, explifyCon c), loc) + + | L.CName s => (L'.CName s, loc) + + | L.CRecord (k, xcs) => (L'.CRecord (explifyKind k, map (fn (c1, c2) => (explifyCon c1, explifyCon c2)) xcs), loc) + | L.CConcat (c1, c2) => (L'.CConcat (explifyCon c1, explifyCon c2), loc) + + | L.CError => raise Fail ("explifyCon: CError at " ^ EM.spanToString loc) + | L.CUnif (_, _, ref (SOME c)) => explifyCon c + | L.CUnif _ => raise Fail ("explifyCon: CUnif at " ^ EM.spanToString loc) + +fun explifyExp (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.EModProj (m, ms, x) => (L'.EModProj (m, ms, x), loc) + | L.EApp (e1, e2) => (L'.EApp (explifyExp e1, explifyExp e2), loc) + | L.EAbs (x, dom, ran, e1) => (L'.EAbs (x, explifyCon dom, explifyCon ran, explifyExp e1), loc) + | L.ECApp (e1, c) => (L'.ECApp (explifyExp e1, explifyCon c), loc) + | L.ECAbs (_, x, k, e1) => (L'.ECAbs (x, explifyKind k, explifyExp e1), loc) + + | L.ERecord xes => (L'.ERecord (map (fn (c, e, t) => (explifyCon c, explifyExp e, explifyCon t)) xes), loc) + | L.EField (e1, c, {field, rest}) => (L'.EField (explifyExp e1, explifyCon c, + {field = explifyCon field, rest = explifyCon rest}), loc) + + | L.EError => raise Fail ("explifyExp: EError at " ^ EM.spanToString loc) + +fun explifySgi (sgi, loc) = + case sgi of + L.SgiConAbs (x, n, k) => (L'.SgiConAbs (x, n, explifyKind k), loc) + | L.SgiCon (x, n, k, c) => (L'.SgiCon (x, n, explifyKind k, explifyCon c), loc) + | L.SgiVal (x, n, c) => (L'.SgiVal (x, n, explifyCon c), loc) + | L.SgiStr (x, n, sgn) => (L'.SgiStr (x, n, explifySgn sgn), loc) + +and explifySgn (sgn, loc) = + case sgn of + L.SgnConst sgis => (L'.SgnConst (map explifySgi sgis), loc) + | L.SgnVar n => (L'.SgnVar n, loc) + | L.SgnError => raise Fail ("explifySgn: SgnError at " ^ EM.spanToString loc) + +fun explifyDecl (d, loc : EM.span) = + case d of + L.DCon (x, n, k, c) => (L'.DCon (x, n, explifyKind k, explifyCon c), loc) + | L.DVal (x, n, t, e) => (L'.DVal (x, n, explifyCon t, explifyExp e), loc) + + | L.DSgn (x, n, sgn) => (L'.DSgn (x, n, explifySgn sgn), loc) + | L.DStr (x, n, sgn, str) => (L'.DStr (x, n, explifySgn sgn, explifyStr str), loc) + +and explifyStr (str, loc) = + case str of + L.StrConst ds => (L'.StrConst (map explifyDecl ds), loc) + | L.StrVar n => (L'.StrVar n, loc) + | L.StrProj (str, s) => (L'.StrProj (explifyStr str, s), loc) + | L.StrError => raise Fail ("explifyStr: StrError at " ^ EM.spanToString loc) + +val explify = map explifyDecl + +end diff -r 367f058aba23 -r d16ef24de78b src/sources --- a/src/sources Tue Jun 17 17:14:21 2008 -0400 +++ b/src/sources Thu Jun 19 10:06:59 2008 -0400 @@ -35,6 +35,20 @@ elaborate.sig elaborate.sml +expl.sml + +expl_util.sig +expl_util.sml + +expl_env.sig +expl_env.sml + +expl_print.sig +expl_print.sml + +explify.sig +explify.sml + core.sml core_util.sig