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@516
|
35 fun liftConInCon by =
|
adamc@516
|
36 U.Con.mapB {kind = fn k => k,
|
adamc@516
|
37 con = fn bound => fn c =>
|
adamc@516
|
38 case c of
|
adamc@516
|
39 CRel xn =>
|
adamc@516
|
40 if xn < bound then
|
adamc@516
|
41 c
|
adamc@516
|
42 else
|
adamc@516
|
43 CRel (xn + by)
|
adamc@516
|
44 (*| CUnif _ => raise SynUnif*)
|
adamc@516
|
45 | _ => c,
|
adamc@516
|
46 bind = fn (bound, U.Con.Rel _) => bound + 1
|
adamc@516
|
47 | (bound, _) => bound}
|
adamc@81
|
48
|
adamc@516
|
49 fun subConInCon' rep =
|
adamc@81
|
50 U.Con.mapB {kind = fn k => k,
|
adamc@516
|
51 con = fn (by, xn) => fn c =>
|
adamc@516
|
52 case c of
|
adamc@516
|
53 CRel xn' =>
|
adamc@516
|
54 (case Int.compare (xn', xn) of
|
adamc@516
|
55 EQUAL => #1 (liftConInCon by 0 rep)
|
adamc@516
|
56 | GREATER => CRel (xn' - 1)
|
adamc@516
|
57 | LESS => c)
|
adamc@516
|
58 (*| CUnif _ => raise SynUnif*)
|
adamc@516
|
59 | _ => c,
|
adamc@516
|
60 bind = fn ((by, xn), U.Con.Rel _) => (by+1, xn+1)
|
adamc@81
|
61 | (ctx, _) => ctx}
|
adamc@81
|
62
|
adamc@516
|
63 val liftConInCon = liftConInCon 1
|
adamc@516
|
64
|
adamc@516
|
65 fun subConInCon (xn, rep) = subConInCon' rep (0, xn)
|
adamc@516
|
66
|
adamc@81
|
67 fun subStrInSgn (m1, m2) =
|
adamc@81
|
68 U.Sgn.map {kind = fn k => k,
|
adamc@81
|
69 con = fn c as CModProj (m1', ms, x) =>
|
adamc@81
|
70 if m1 = m1' then
|
adamc@81
|
71 CModProj (m2, ms, x)
|
adamc@81
|
72 else
|
adamc@81
|
73 c
|
adamc@81
|
74 | c => c,
|
adamc@81
|
75 sgn_item = fn sgi => sgi,
|
adamc@81
|
76 sgn = fn sgn => sgn}
|
adamc@81
|
77
|
adamc@81
|
78
|
adamc@81
|
79 fun hnormCon env (cAll as (c, loc)) =
|
adamc@81
|
80 case c of
|
adamc@81
|
81 CUnif (_, _, _, ref (SOME c)) => hnormCon env c
|
adamc@81
|
82
|
adamc@81
|
83 | CNamed xn =>
|
adamc@81
|
84 (case E.lookupCNamed env xn of
|
adamc@81
|
85 (_, _, SOME c') => hnormCon env c'
|
adamc@81
|
86 | _ => cAll)
|
adamc@81
|
87
|
adamc@81
|
88 | CModProj (n, ms, x) =>
|
adamc@81
|
89 let
|
adamc@81
|
90 val (_, sgn) = E.lookupStrNamed env n
|
adamc@81
|
91 val (str, sgn) = foldl (fn (m, (str, sgn)) =>
|
adamc@81
|
92 case E.projectStr env {sgn = sgn, str = str, field = m} of
|
adamc@81
|
93 NONE => raise Fail "hnormCon: Unknown substructure"
|
adamc@81
|
94 | SOME sgn => ((StrProj (str, m), loc), sgn))
|
adamc@81
|
95 ((StrVar n, loc), sgn) ms
|
adamc@81
|
96 in
|
adamc@81
|
97 case E.projectCon env {sgn = sgn, str = str, field = x} of
|
adamc@81
|
98 NONE => raise Fail "kindof: Unknown con in structure"
|
adamc@81
|
99 | SOME (_, NONE) => cAll
|
adamc@81
|
100 | SOME (_, SOME c) => hnormCon env c
|
adamc@81
|
101 end
|
adamc@81
|
102
|
adamc@81
|
103 | CApp (c1, c2) =>
|
adamc@81
|
104 (case #1 (hnormCon env c1) of
|
adamc@81
|
105 CAbs (x, k, cb) =>
|
adamc@81
|
106 let
|
adamc@81
|
107 val sc = (hnormCon env (subConInCon (0, c2) cb))
|
adamc@81
|
108 handle SynUnif => cAll
|
adamc@81
|
109 (*val env' = E.pushCRel env x k*)
|
adamc@81
|
110 in
|
adamc@328
|
111 (*Print.eprefaces "Subst" [("x", Print.PD.string x),
|
adamc@328
|
112 ("cb", ElabPrint.p_con env' cb),
|
adamc@328
|
113 ("c2", ElabPrint.p_con env c2),
|
adamc@328
|
114 ("sc", ElabPrint.p_con env sc)];*)
|
adamc@81
|
115 sc
|
adamc@81
|
116 end
|
adamc@621
|
117 | c1' as CApp (c', f) =>
|
adamc@326
|
118 let
|
adamc@326
|
119 fun default () = (CApp ((c1', loc), hnormCon env c2), loc)
|
adamc@326
|
120 in
|
adamc@326
|
121 case #1 (hnormCon env c') of
|
adamc@621
|
122 CMap (ks as (k1, k2)) =>
|
adamc@621
|
123 (case #1 (hnormCon env c2) of
|
adamc@621
|
124 CRecord (_, []) => (CRecord (k2, []), loc)
|
adamc@621
|
125 | CRecord (_, (x, c) :: rest) =>
|
adamc@621
|
126 hnormCon env
|
adamc@621
|
127 (CConcat ((CRecord (k2, [(x, (CApp (f, c), loc))]), loc),
|
adamc@621
|
128 (CApp (c1, (CRecord (k2, rest), loc)), loc)), loc)
|
adamc@621
|
129 | CConcat ((CRecord (k, (x, c) :: rest), _), rest') =>
|
adamc@621
|
130 let
|
adamc@621
|
131 val rest'' = (CConcat ((CRecord (k, rest), loc), rest'), loc)
|
adamc@621
|
132 in
|
adamc@621
|
133 hnormCon env
|
adamc@621
|
134 (CConcat ((CRecord (k2, [(x, (CApp (f, c), loc))]), loc),
|
adamc@621
|
135 (CApp (c1, rest''), loc)), loc)
|
adamc@621
|
136 end
|
adamc@621
|
137 | _ =>
|
adamc@621
|
138 let
|
adamc@621
|
139 fun unconstraint c =
|
adamc@621
|
140 case hnormCon env c of
|
adamc@621
|
141 (CDisjoint (_, _, _, c), _) => unconstraint c
|
adamc@621
|
142 | c => c
|
adamc@81
|
143
|
adamc@621
|
144 fun tryDistributivity () =
|
adamc@621
|
145 case hnormCon env c2 of
|
adamc@621
|
146 (CConcat (c1, c2'), _) =>
|
adamc@621
|
147 let
|
adamc@621
|
148 val c = (CMap ks, loc)
|
adamc@621
|
149 val c = (CApp (c, f), loc)
|
adamc@621
|
150
|
adamc@621
|
151 val c1 = (CApp (c, c1), loc)
|
adamc@621
|
152 val c2 = (CApp (c, c2'), loc)
|
adamc@621
|
153 val c = (CConcat (c1, c2), loc)
|
adamc@621
|
154 in
|
adamc@621
|
155 hnormCon env c
|
adamc@621
|
156 end
|
adamc@621
|
157 | _ => default ()
|
adamc@329
|
158
|
adamc@621
|
159 fun tryFusion () =
|
adamc@621
|
160 case #1 (hnormCon env c2) of
|
adamc@621
|
161 CApp (f', r') =>
|
adamc@621
|
162 (case #1 (hnormCon env f') of
|
adamc@621
|
163 CApp (f', inner_f) =>
|
adamc@621
|
164 (case #1 (hnormCon env f') of
|
adamc@621
|
165 CMap (dom, _) =>
|
adamc@621
|
166 let
|
adamc@621
|
167 val f' = (CApp (inner_f, (CRel 0, loc)), loc)
|
adamc@621
|
168 val f' = (CApp (f, f'), loc)
|
adamc@621
|
169 val f' = (CAbs ("v", dom, f'), loc)
|
adamc@329
|
170
|
adamc@621
|
171 val c = (CMap (dom, k2), loc)
|
adamc@621
|
172 val c = (CApp (c, f'), loc)
|
adamc@621
|
173 val c = (CApp (c, r'), loc)
|
adamc@621
|
174 in
|
adamc@621
|
175 hnormCon env c
|
adamc@621
|
176 end
|
adamc@621
|
177 | _ => tryDistributivity ())
|
adamc@621
|
178 | _ => tryDistributivity ())
|
adamc@621
|
179 | _ => tryDistributivity ()
|
adamc@339
|
180
|
adamc@621
|
181 fun tryIdentity () =
|
adamc@621
|
182 let
|
adamc@621
|
183 fun cunif () =
|
adamc@621
|
184 let
|
adamc@621
|
185 val r = ref NONE
|
adamc@621
|
186 in
|
adamc@621
|
187 (r, (CUnif (loc, (KType, loc), "_", r), loc))
|
adamc@621
|
188 end
|
adamc@621
|
189
|
adamc@621
|
190 val (vR, v) = cunif ()
|
adamc@494
|
191
|
adamc@621
|
192 val c = (CApp (f, v), loc)
|
adamc@621
|
193 in
|
adamc@621
|
194 case unconstraint c of
|
adamc@621
|
195 (CUnif (_, _, _, vR'), _) =>
|
adamc@621
|
196 if vR' = vR then
|
adamc@621
|
197 hnormCon env c2
|
adamc@621
|
198 else
|
adamc@621
|
199 tryFusion ()
|
adamc@621
|
200 | _ => tryFusion ()
|
adamc@621
|
201 end
|
adamc@621
|
202 in
|
adamc@621
|
203 tryIdentity ()
|
adamc@621
|
204 end)
|
adamc@326
|
205 | _ => default ()
|
adamc@326
|
206 end
|
adamc@326
|
207 | c1' => (CApp ((c1', loc), hnormCon env c2), loc))
|
adamc@621
|
208
|
adamc@81
|
209 | CConcat (c1, c2) =>
|
adamc@81
|
210 (case (hnormCon env c1, hnormCon env c2) of
|
adamc@81
|
211 ((CRecord (k, xcs1), loc), (CRecord (_, xcs2), _)) =>
|
adamc@81
|
212 (CRecord (k, xcs1 @ xcs2), loc)
|
adamc@81
|
213 | ((CRecord (_, []), _), c2') => c2'
|
adamc@81
|
214 | ((CConcat (c11, c12), loc), c2') =>
|
adamc@81
|
215 hnormCon env (CConcat (c11, (CConcat (c12, c2'), loc)), loc)
|
adamc@209
|
216 | (c1', (CRecord (_, []), _)) => c1'
|
adamc@329
|
217 | (c1', c2') => (CConcat (c1', c2'), loc))
|
adamc@81
|
218
|
adamc@207
|
219 | CProj (c, n) =>
|
adamc@207
|
220 (case hnormCon env c of
|
adamc@207
|
221 (CTuple cs, _) => hnormCon env (List.nth (cs, n - 1))
|
adamc@207
|
222 | _ => cAll)
|
adamc@207
|
223
|
adamc@81
|
224 | _ => cAll
|
adamc@81
|
225
|
adamc@81
|
226 end
|