Mercurial > urweb

annotate src/elab_ops.sml @ 305:55eedecb6c50

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Remove need to mention table name in expressions for UPDATE and DELETE
author Adam Chlipala <adamc@hcoop.net>
date Sun, 07 Sep 2008 14:30:32 -0400
parents 1487c712eb12
children 950320f33232
rev   line source
adamc@81 1 (* Copyright (c) 2008, Adam Chlipala
adamc@81 2 * All rights reserved.
adamc@81 3 *
adamc@81 4 * Redistribution and use in source and binary forms, with or without
adamc@81 5 * modification, are permitted provided that the following conditions are met:
adamc@81 6 *
adamc@81 7 * - Redistributions of source code must retain the above copyright notice,
adamc@81 8 * this list of conditions and the following disclaimer.
adamc@81 9 * - Redistributions in binary form must reproduce the above copyright notice,
adamc@81 10 * this list of conditions and the following disclaimer in the documentation
adamc@81 11 * and/or other materials provided with the distribution.
adamc@81 12 * - The names of contributors may not be used to endorse or promote products
adamc@81 13 * derived from this software without specific prior written permission.
adamc@81 14 *
adamc@81 15 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
adamc@81 16 * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
adamc@81 17 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
adamc@81 18 * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
adamc@81 19 * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
adamc@81 20 * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
adamc@81 21 * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
adamc@81 22 * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
adamc@81 23 * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
adamc@81 24 * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
adamc@81 25 * POSSIBILITY OF SUCH DAMAGE.
adamc@81 26 *)
adamc@81 27
adamc@81 28 structure ElabOps :> ELAB_OPS = struct
adamc@81 29
adamc@81 30 open Elab
adamc@81 31
adamc@81 32 structure E = ElabEnv
adamc@81 33 structure U = ElabUtil
adamc@81 34
adamc@81 35 val liftConInCon = E.liftConInCon
adamc@81 36
adamc@81 37 val subConInCon =
adamc@81 38 U.Con.mapB {kind = fn k => k,
adamc@81 39 con = fn (xn, rep) => fn c =>
adamc@81 40 case c of
adamc@81 41 CRel xn' =>
adamc@81 42 (case Int.compare (xn', xn) of
adamc@81 43 EQUAL => #1 rep
adamc@81 44 | GREATER => CRel (xn' - 1)
adamc@81 45 | LESS => c)
adamc@81 46 (*| CUnif _ => raise SynUnif*)
adamc@81 47 | _ => c,
adamc@81 48 bind = fn ((xn, rep), U.Con.Rel _) => (xn+1, liftConInCon 0 rep)
adamc@81 49 | (ctx, _) => ctx}
adamc@81 50
adamc@81 51 fun subStrInSgn (m1, m2) =
adamc@81 52 U.Sgn.map {kind = fn k => k,
adamc@81 53 con = fn c as CModProj (m1', ms, x) =>
adamc@81 54 if m1 = m1' then
adamc@81 55 CModProj (m2, ms, x)
adamc@81 56 else
adamc@81 57 c
adamc@81 58 | c => c,
adamc@81 59 sgn_item = fn sgi => sgi,
adamc@81 60 sgn = fn sgn => sgn}
adamc@81 61
adamc@81 62
adamc@81 63 fun hnormCon env (cAll as (c, loc)) =
adamc@81 64 case c of
adamc@81 65 CUnif (_, _, _, ref (SOME c)) => hnormCon env c
adamc@81 66
adamc@81 67 | CNamed xn =>
adamc@81 68 (case E.lookupCNamed env xn of
adamc@81 69 (_, _, SOME c') => hnormCon env c'
adamc@81 70 | _ => cAll)
adamc@81 71
adamc@81 72 | CModProj (n, ms, x) =>
adamc@81 73 let
adamc@81 74 val (_, sgn) = E.lookupStrNamed env n
adamc@81 75 val (str, sgn) = foldl (fn (m, (str, sgn)) =>
adamc@81 76 case E.projectStr env {sgn = sgn, str = str, field = m} of
adamc@81 77 NONE => raise Fail "hnormCon: Unknown substructure"
adamc@81 78 | SOME sgn => ((StrProj (str, m), loc), sgn))
adamc@81 79 ((StrVar n, loc), sgn) ms
adamc@81 80 in
adamc@81 81 case E.projectCon env {sgn = sgn, str = str, field = x} of
adamc@81 82 NONE => raise Fail "kindof: Unknown con in structure"
adamc@81 83 | SOME (_, NONE) => cAll
adamc@81 84 | SOME (_, SOME c) => hnormCon env c
adamc@81 85 end
adamc@81 86
adamc@81 87 | CApp (c1, c2) =>
adamc@81 88 (case #1 (hnormCon env c1) of
adamc@81 89 CAbs (x, k, cb) =>
adamc@81 90 let
adamc@81 91 val sc = (hnormCon env (subConInCon (0, c2) cb))
adamc@81 92 handle SynUnif => cAll
adamc@81 93 (*val env' = E.pushCRel env x k*)
adamc@81 94 in
adamc@81 95 (*eprefaces "Subst" [("x", Print.PD.string x),
adamc@81 96 ("cb", p_con env' cb),
adamc@81 97 ("c2", p_con env c2),
adamc@81 98 ("sc", p_con env sc)];*)
adamc@81 99 sc
adamc@81 100 end
adamc@81 101 | CApp (c', i) =>
adamc@81 102 (case #1 (hnormCon env c') of
adamc@81 103 CApp (c', f) =>
adamc@81 104 (case #1 (hnormCon env c') of
adamc@81 105 CFold ks =>
adamc@81 106 (case #1 (hnormCon env c2) of
adamc@81 107 CRecord (_, []) => hnormCon env i
adamc@81 108 | CRecord (k, (x, c) :: rest) =>
adamc@81 109 hnormCon env
adamc@81 110 (CApp ((CApp ((CApp (f, x), loc), c), loc),
adamc@81 111 (CApp ((CApp ((CApp ((CFold ks, loc), f), loc), i), loc),
adamc@81 112 (CRecord (k, rest), loc)), loc)), loc)
adamc@81 113 | CConcat ((CRecord (k, (x, c) :: rest), _), rest') =>
adamc@81 114 let
adamc@81 115 val rest'' = (CConcat ((CRecord (k, rest), loc), rest'), loc)
adamc@81 116
adamc@81 117 (*val ccc = (CApp ((CApp ((CApp (f, x), loc), c), loc),
adamc@81 118 (CApp ((CApp ((CApp ((CFold ks, loc), f), loc), i), loc),
adamc@81 119 rest''), loc)), loc)*)
adamc@81 120 in
adamc@81 121 (*eprefaces "Red to" [("ccc", p_con env ccc), ("ccc'", p_con env (hnormCon env ccc))];*)
adamc@81 122 hnormCon env
adamc@81 123 (CApp ((CApp ((CApp (f, x), loc), c), loc),
adamc@81 124 (CApp ((CApp ((CApp ((CFold ks, loc), f), loc), i), loc),
adamc@81 125 rest''), loc)), loc)
adamc@81 126 end
adamc@81 127 | _ => cAll)
adamc@81 128 | _ => cAll)
adamc@81 129 | _ => cAll)
adamc@81 130 | _ => cAll)
adamc@81 131
adamc@81 132 | CConcat (c1, c2) =>
adamc@81 133 (case (hnormCon env c1, hnormCon env c2) of
adamc@81 134 ((CRecord (k, xcs1), loc), (CRecord (_, xcs2), _)) =>
adamc@81 135 (CRecord (k, xcs1 @ xcs2), loc)
adamc@81 136 | ((CRecord (_, []), _), c2') => c2'
adamc@81 137 | ((CConcat (c11, c12), loc), c2') =>
adamc@81 138 hnormCon env (CConcat (c11, (CConcat (c12, c2'), loc)), loc)
adamc@209 139 | (c1', (CRecord (_, []), _)) => c1'
adamc@81 140 | _ => cAll)
adamc@81 141
adamc@207 142 | CProj (c, n) =>
adamc@207 143 (case hnormCon env c of
adamc@207 144 (CTuple cs, _) => hnormCon env (List.nth (cs, n - 1))
adamc@207 145 | _ => cAll)
adamc@207 146
adamc@81 147 | _ => cAll
adamc@81 148
adamc@81 149 end