Mercurial > urweb

comparison src/elab_ops.sml @ 81:60d97de1bbe8

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