Mercurial > urweb

annotate src/explify.sml @ 2258:b1ba35ce2613

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Fix bug where pure caching didn't treat FFI applications as effectful.
author Ziv Scully <ziv@mit.edu>
date Sun, 27 Sep 2015 17:02:14 -0400
parents 403f0cc65b9c
children 22117edf8fd3
rev   line source
adam@1294 1 (* Copyright (c) 2008-2010, Adam Chlipala
adamc@38 2 * All rights reserved.
adamc@38 3 *
adamc@38 4 * Redistribution and use in source and binary forms, with or without
adamc@38 5 * modification, are permitted provided that the following conditions are met:
adamc@38 6 *
adamc@38 7 * - Redistributions of source code must retain the above copyright notice,
adamc@38 8 * this list of conditions and the following disclaimer.
adamc@38 9 * - Redistributions in binary form must reproduce the above copyright notice,
adamc@38 10 * this list of conditions and the following disclaimer in the documentation
adamc@38 11 * and/or other materials provided with the distribution.
adamc@38 12 * - The names of contributors may not be used to endorse or promote products
adamc@38 13 * derived from this software without specific prior written permission.
adamc@38 14 *
adamc@38 15 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
adamc@38 16 * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
adamc@38 17 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
adamc@38 18 * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
adamc@38 19 * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
adamc@38 20 * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
adamc@38 21 * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
adamc@38 22 * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
adamc@38 23 * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
adamc@38 24 * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
adamc@38 25 * POSSIBILITY OF SUCH DAMAGE.
adamc@38 26 *)
adamc@38 27
adamc@38 28 structure Explify :> EXPLIFY = struct
adamc@38 29
adamc@38 30 structure EM = ErrorMsg
adamc@38 31 structure L = Elab
adamc@38 32 structure L' = Expl
adamc@38 33
adamc@38 34 fun explifyKind (k, loc) =
adamc@38 35 case k of
adamc@38 36 L.KType => (L'.KType, loc)
adamc@38 37 | L.KArrow (k1, k2) => (L'.KArrow (explifyKind k1, explifyKind k2), loc)
adamc@38 38 | L.KName => (L'.KName, loc)
adamc@38 39 | L.KRecord k => (L'.KRecord (explifyKind k), loc)
adamc@38 40
adamc@87 41 | L.KUnit => (L'.KUnit, loc)
adamc@213 42 | L.KTuple ks => (L'.KTuple (map explifyKind ks), loc)
adamc@82 43
adamc@38 44 | L.KError => raise Fail ("explifyKind: KError at " ^ EM.spanToString loc)
adam@1639 45 | L.KUnif (_, _, ref (L.KKnown k)) => explifyKind k
adamc@38 46 | L.KUnif _ => raise Fail ("explifyKind: KUnif at " ^ EM.spanToString loc)
adam@1639 47 | L.KTupleUnif (loc, _, ref (L.KKnown k)) => explifyKind k
adam@1302 48 | L.KTupleUnif _ => raise Fail ("explifyKind: KTupleUnif at " ^ EM.spanToString loc)
adamc@38 49
adamc@624 50 | L.KRel n => (L'.KRel n, loc)
adamc@624 51 | L.KFun (x, k) => (L'.KFun (x, explifyKind k), loc)
adamc@624 52
adamc@38 53 fun explifyCon (c, loc) =
adamc@38 54 case c of
adamc@38 55 L.TFun (t1, t2) => (L'.TFun (explifyCon t1, explifyCon t2), loc)
adamc@38 56 | L.TCFun (_, x, k, t) => (L'.TCFun (x, explifyKind k, explifyCon t), loc)
adamc@628 57 | L.TDisjoint (_, _, t) => explifyCon t
adamc@38 58 | L.TRecord c => (L'.TRecord (explifyCon c), loc)
adamc@38 59
adamc@38 60 | L.CRel n => (L'.CRel n, loc)
adamc@38 61 | L.CNamed n => (L'.CNamed n, loc)
adamc@38 62 | L.CModProj (m, ms, x) => (L'.CModProj (m, ms, x), loc)
adamc@38 63
adamc@38 64 | L.CApp (c1, c2) => (L'.CApp (explifyCon c1, explifyCon c2), loc)
adamc@38 65 | L.CAbs (x, k, c) => (L'.CAbs (x, explifyKind k, explifyCon c), loc)
adamc@38 66
adamc@38 67 | L.CName s => (L'.CName s, loc)
adamc@38 68
adamc@38 69 | L.CRecord (k, xcs) => (L'.CRecord (explifyKind k, map (fn (c1, c2) => (explifyCon c1, explifyCon c2)) xcs), loc)
adamc@38 70 | L.CConcat (c1, c2) => (L'.CConcat (explifyCon c1, explifyCon c2), loc)
adamc@621 71 | L.CMap (dom, ran) => (L'.CMap (explifyKind dom, explifyKind ran), loc)
adamc@38 72
adamc@87 73 | L.CUnit => (L'.CUnit, loc)
adamc@82 74
adamc@213 75 | L.CTuple cs => (L'.CTuple (map explifyCon cs), loc)
adamc@213 76 | L.CProj (c, n) => (L'.CProj (explifyCon c, n), loc)
adamc@208 77
adamc@38 78 | L.CError => raise Fail ("explifyCon: CError at " ^ EM.spanToString loc)
adam@1639 79 | L.CUnif (nl, _, _, _, ref (L.Known c)) => explifyCon (ElabEnv.mliftConInCon nl c)
adamc@38 80 | L.CUnif _ => raise Fail ("explifyCon: CUnif at " ^ EM.spanToString loc)
adamc@38 81
adamc@624 82 | L.CKAbs (x, c) => (L'.CKAbs (x, explifyCon c), loc)
adamc@624 83 | L.CKApp (c, k) => (L'.CKApp (explifyCon c, explifyKind k), loc)
adamc@624 84 | L.TKFun (x, c) => (L'.TKFun (x, explifyCon c), loc)
adamc@624 85
adamc@176 86 fun explifyPatCon pc =
adamc@176 87 case pc of
adamc@176 88 L.PConVar n => L'.PConVar n
adamc@176 89 | L.PConProj x => L'.PConProj x
adamc@176 90
adamc@176 91 fun explifyPat (p, loc) =
adamc@176 92 case p of
adamc@176 93 L.PWild => (L'.PWild, loc)
adamc@182 94 | L.PVar (x, t) => (L'.PVar (x, explifyCon t), loc)
adamc@176 95 | L.PPrim p => (L'.PPrim p, loc)
adamc@191 96 | L.PCon (dk, pc, cs, po) => (L'.PCon (dk, explifyPatCon pc, map explifyCon cs, Option.map explifyPat po), loc)
adamc@182 97 | L.PRecord xps => (L'.PRecord (map (fn (x, p, t) => (x, explifyPat p, explifyCon t)) xps), loc)
adamc@176 98
adamc@38 99 fun explifyExp (e, loc) =
adamc@38 100 case e of
adamc@38 101 L.EPrim p => (L'.EPrim p, loc)
adamc@38 102 | L.ERel n => (L'.ERel n, loc)
adamc@38 103 | L.ENamed n => (L'.ENamed n, loc)
adamc@38 104 | L.EModProj (m, ms, x) => (L'.EModProj (m, ms, x), loc)
adamc@38 105 | L.EApp (e1, e2) => (L'.EApp (explifyExp e1, explifyExp e2), loc)
adamc@38 106 | L.EAbs (x, dom, ran, e1) => (L'.EAbs (x, explifyCon dom, explifyCon ran, explifyExp e1), loc)
adamc@38 107 | L.ECApp (e1, c) => (L'.ECApp (explifyExp e1, explifyCon c), loc)
adamc@38 108 | L.ECAbs (_, x, k, e1) => (L'.ECAbs (x, explifyKind k, explifyExp e1), loc)
adamc@38 109
adamc@38 110 | L.ERecord xes => (L'.ERecord (map (fn (c, e, t) => (explifyCon c, explifyExp e, explifyCon t)) xes), loc)
adamc@38 111 | L.EField (e1, c, {field, rest}) => (L'.EField (explifyExp e1, explifyCon c,
adamc@38 112 {field = explifyCon field, rest = explifyCon rest}), loc)
adamc@445 113 | L.EConcat (e1, c1, e2, c2) => (L'.EConcat (explifyExp e1, explifyCon c1, explifyExp e2, explifyCon c2),
adamc@445 114 loc)
adamc@149 115 | L.ECut (e1, c, {field, rest}) => (L'.ECut (explifyExp e1, explifyCon c,
adamc@149 116 {field = explifyCon field, rest = explifyCon rest}), loc)
adamc@493 117 | L.ECutMulti (e1, c, {rest}) => (L'.ECutMulti (explifyExp e1, explifyCon c,
adamc@493 118 {rest = explifyCon rest}), loc)
adamc@182 119 | L.ECase (e, pes, {disc, result}) =>
adamc@182 120 (L'.ECase (explifyExp e,
adamc@182 121 map (fn (p, e) => (explifyPat p, explifyExp e)) pes,
adamc@182 122 {disc = explifyCon disc, result = explifyCon result}), loc)
adamc@171 123
adamc@38 124 | L.EError => raise Fail ("explifyExp: EError at " ^ EM.spanToString loc)
adamc@228 125 | L.EUnif (ref (SOME e)) => explifyExp e
adamc@228 126 | L.EUnif _ => raise Fail ("explifyExp: Undetermined EUnif at " ^ EM.spanToString loc)
adamc@38 127
adamc@825 128 | L.ELet (des, e, t) =>
adamc@449 129 foldr (fn ((de, loc), e) =>
adamc@449 130 case de of
adamc@449 131 L.EDValRec _ => raise Fail "explifyExp: Local 'val rec' remains"
adamc@825 132 | L.EDVal ((L.PVar (x, _), _), t', e') => (L'.ELet (x, explifyCon t', explifyExp e', e), loc)
adamc@825 133 | L.EDVal (p, t', e') => (L'.ECase (explifyExp e',
adamc@825 134 [(explifyPat p, e)],
adamc@825 135 {disc = explifyCon t', result = explifyCon t}), loc))
adamc@449 136 (explifyExp e) des
adamc@449 137
adamc@624 138 | L.EKAbs (x, e) => (L'.EKAbs (x, explifyExp e), loc)
adamc@624 139 | L.EKApp (e, k) => (L'.EKApp (explifyExp e, explifyKind k), loc)
adamc@624 140
adamc@38 141 fun explifySgi (sgi, loc) =
adamc@38 142 case sgi of
adamc@88 143 L.SgiConAbs (x, n, k) => SOME (L'.SgiConAbs (x, n, explifyKind k), loc)
adamc@88 144 | L.SgiCon (x, n, k, c) => SOME (L'.SgiCon (x, n, explifyKind k, explifyCon c), loc)
adamc@806 145 | L.SgiDatatype dts => SOME (L'.SgiDatatype (map (fn (x, n, xs, xncs) =>
adamc@806 146 (x, n, xs,
adamc@806 147 map (fn (x, n, co) =>
adamc@806 148 (x, n, Option.map explifyCon co)) xncs)) dts), loc)
adamc@191 149 | L.SgiDatatypeImp (x, n, m1, ms, s, xs, xncs) =>
adamc@191 150 SOME (L'.SgiDatatypeImp (x, n, m1, ms, s, xs, map (fn (x, n, co) =>
adamc@191 151 (x, n, Option.map explifyCon co)) xncs), loc)
adamc@88 152 | L.SgiVal (x, n, c) => SOME (L'.SgiVal (x, n, explifyCon c), loc)
adamc@88 153 | L.SgiStr (x, n, sgn) => SOME (L'.SgiStr (x, n, explifySgn sgn), loc)
adamc@88 154 | L.SgiSgn (x, n, sgn) => SOME (L'.SgiSgn (x, n, explifySgn sgn), loc)
adamc@88 155 | L.SgiConstraint _ => NONE
adamc@563 156 | L.SgiClassAbs (x, n, k) => SOME (L'.SgiConAbs (x, n, (L'.KArrow (explifyKind k, (L'.KType, loc)), loc)), loc)
adamc@563 157 | L.SgiClass (x, n, k, c) => SOME (L'.SgiCon (x, n, (L'.KArrow (explifyKind k, (L'.KType, loc)), loc),
adamc@563 158 explifyCon c), loc)
adamc@38 159
adamc@38 160 and explifySgn (sgn, loc) =
adamc@38 161 case sgn of
adamc@88 162 L.SgnConst sgis => (L'.SgnConst (List.mapPartial explifySgi sgis), loc)
adamc@38 163 | L.SgnVar n => (L'.SgnVar n, loc)
adamc@45 164 | L.SgnFun (m, n, dom, ran) => (L'.SgnFun (m, n, explifySgn dom, explifySgn ran), loc)
adam@1864 165 | L.SgnWhere (sgn, ms, x, c) => (L'.SgnWhere (explifySgn sgn, ms, x, explifyCon c), loc)
adamc@64 166 | L.SgnProj x => (L'.SgnProj x, loc)
adamc@38 167 | L.SgnError => raise Fail ("explifySgn: SgnError at " ^ EM.spanToString loc)
adamc@38 168
adamc@38 169 fun explifyDecl (d, loc : EM.span) =
adamc@38 170 case d of
adamc@88 171 L.DCon (x, n, k, c) => SOME (L'.DCon (x, n, explifyKind k, explifyCon c), loc)
adamc@806 172 | L.DDatatype dts => SOME (L'.DDatatype (map (fn (x, n, xs, xncs) =>
adamc@806 173 (x, n, xs,
adamc@806 174 map (fn (x, n, co) =>
adamc@806 175 (x, n, Option.map explifyCon co)) xncs)) dts), loc)
adamc@191 176 | L.DDatatypeImp (x, n, m1, ms, s, xs, xncs) =>
adamc@191 177 SOME (L'.DDatatypeImp (x, n, m1, ms, s, xs,
adamc@191 178 map (fn (x, n, co) =>
adamc@191 179 (x, n, Option.map explifyCon co)) xncs), loc)
adamc@88 180 | L.DVal (x, n, t, e) => SOME (L'.DVal (x, n, explifyCon t, explifyExp e), loc)
adamc@124 181 | L.DValRec vis => SOME (L'.DValRec (map (fn (x, n, t, e) => (x, n, explifyCon t, explifyExp e)) vis), loc)
adamc@38 182
adamc@88 183 | L.DSgn (x, n, sgn) => SOME (L'.DSgn (x, n, explifySgn sgn), loc)
adamc@88 184 | L.DStr (x, n, sgn, str) => SOME (L'.DStr (x, n, explifySgn sgn, explifyStr str), loc)
adamc@88 185 | L.DFfiStr (x, n, sgn) => SOME (L'.DFfiStr (x, n, explifySgn sgn), loc)
adamc@88 186 | L.DConstraint (c1, c2) => NONE
adamc@109 187 | L.DExport (en, sgn, str) => SOME (L'.DExport (en, explifySgn sgn, explifyStr str), loc)
adamc@707 188 | L.DTable (nt, x, n, c, pe, pc, ce, cc) =>
adamc@707 189 SOME (L'.DTable (nt, x, n, explifyCon c,
adamc@707 190 explifyExp pe, explifyCon pc,
adamc@707 191 explifyExp ce, explifyCon cc), loc)
adamc@754 192 | L.DView (nt, x, n, e, c) =>
adamc@754 193 SOME (L'.DView (nt, x, n, explifyExp e, explifyCon c), loc)
adamc@338 194 | L.DSequence (nt, x, n) => SOME (L'.DSequence (nt, x, n), loc)
adamc@271 195 | L.DDatabase s => SOME (L'.DDatabase s, loc)
adamc@460 196 | L.DCookie (nt, x, n, c) => SOME (L'.DCookie (nt, x, n, explifyCon c), loc)
adamc@720 197 | L.DStyle (nt, x, n) => SOME (L'.DStyle (nt, x, n), loc)
adamc@1075 198 | L.DTask (e1, e2) => SOME (L'.DTask (explifyExp e1, explifyExp e2), loc)
adamc@1199 199 | L.DPolicy e1 => SOME (L'.DPolicy (explifyExp e1), loc)
adam@1294 200 | L.DOnError v => SOME (L'.DOnError v, loc)
adam@2010 201 | L.DFfi (x, n, modes, t) => SOME (L'.DFfi (x, n, modes, explifyCon t), loc)
adamc@38 202
adamc@38 203 and explifyStr (str, loc) =
adamc@38 204 case str of
adamc@88 205 L.StrConst ds => (L'.StrConst (List.mapPartial explifyDecl ds), loc)
adamc@38 206 | L.StrVar n => (L'.StrVar n, loc)
adamc@38 207 | L.StrProj (str, s) => (L'.StrProj (explifyStr str, s), loc)
adamc@45 208 | L.StrFun (m, n, dom, ran, str) => (L'.StrFun (m, n, explifySgn dom, explifySgn ran, explifyStr str), loc)
adamc@45 209 | L.StrApp (str1, str2) => (L'.StrApp (explifyStr str1, explifyStr str2), loc)
adamc@38 210 | L.StrError => raise Fail ("explifyStr: StrError at " ^ EM.spanToString loc)
adamc@38 211
adamc@88 212 val explify = List.mapPartial explifyDecl
adamc@38 213
adamc@38 214 end