Mercurial > urweb

comparison src/elab_ops.sml @ 623:588b9d16b00a

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Start of kind polymorphism, up to the point where demo/hello elaborates with updated Basis/Top
author Adam Chlipala <adamc@hcoop.net>
date Sun, 22 Feb 2009 16:10:25 -0500
parents 8998114760c1
children 12b73f3c108e
comparison
equal deleted inserted replaced
622:d64533157f40 623:588b9d16b00a
30 open Elab 30 open Elab
31 31
32 structure E = ElabEnv 32 structure E = ElabEnv
33 structure U = ElabUtil 33 structure U = ElabUtil
34 34
35 fun liftKindInKind' by =
36 U.Kind.mapB {kind = fn bound => fn k =>
37 case k of
38 KRel xn =>
39 if xn < bound then
40 k
41 else
42 KRel (xn + by)
43 | _ => k,
44 bind = fn (bound, _) => bound + 1}
45
46 fun subKindInKind' rep =
47 U.Kind.mapB {kind = fn (by, xn) => fn k =>
48 case k of
49 KRel xn' =>
50 (case Int.compare (xn', xn) of
51 EQUAL => #1 (liftKindInKind' by 0 rep)
52 | GREATER => KRel (xn' - 1)
53 | LESS => k)
54 | _ => k,
55 bind = fn ((by, xn), _) => (by+1, xn+1)}
56
57 val liftKindInKind = liftKindInKind' 1
58
59 fun subKindInKind (xn, rep) = subKindInKind' rep (0, xn)
60
61 fun liftKindInCon by =
62 U.Con.mapB {kind = fn bound => fn k =>
63 case k of
64 KRel xn =>
65 if xn < bound then
66 k
67 else
68 KRel (xn + by)
69 | _ => k,
70 con = fn _ => fn c => c,
71 bind = fn (bound, U.Con.RelK _) => bound + 1
72 | (bound, _) => bound}
73
74 fun subKindInCon' rep =
75 U.Con.mapB {kind = fn (by, xn) => fn k =>
76 case k of
77 KRel xn' =>
78 (case Int.compare (xn', xn) of
79 EQUAL => #1 (liftKindInKind' by 0 rep)
80 | GREATER => KRel (xn' - 1)
81 | LESS => k)
82 | _ => k,
83 con = fn _ => fn c => c,
84 bind = fn ((by, xn), U.Con.RelK _) => (by+1, xn+1)
85 | (st, _) => st}
86
87 val liftKindInCon = liftKindInCon 1
88
89 fun subKindInCon (xn, rep) = subKindInCon' rep (0, xn)
90
35 fun liftConInCon by = 91 fun liftConInCon by =
36 U.Con.mapB {kind = fn k => k, 92 U.Con.mapB {kind = fn _ => fn k => k,
37 con = fn bound => fn c => 93 con = fn bound => fn c =>
38 case c of 94 case c of
39 CRel xn => 95 CRel xn =>
40 if xn < bound then 96 if xn < bound then
41 c 97 c
42 else 98 else
43 CRel (xn + by) 99 CRel (xn + by)
44 (*| CUnif _ => raise SynUnif*) 100 (*| CUnif _ => raise SynUnif*)
45 | _ => c, 101 | _ => c,
46 bind = fn (bound, U.Con.Rel _) => bound + 1 102 bind = fn (bound, U.Con.RelC _) => bound + 1
47 | (bound, _) => bound} 103 | (bound, _) => bound}
48 104
49 fun subConInCon' rep = 105 fun subConInCon' rep =
50 U.Con.mapB {kind = fn k => k, 106 U.Con.mapB {kind = fn _ => fn k => k,
51 con = fn (by, xn) => fn c => 107 con = fn (by, xn) => fn c =>
52 case c of 108 case c of
53 CRel xn' => 109 CRel xn' =>
54 (case Int.compare (xn', xn) of 110 (case Int.compare (xn', xn) of
55 EQUAL => #1 (liftConInCon by 0 rep) 111 EQUAL => #1 (liftConInCon by 0 rep)
56 | GREATER => CRel (xn' - 1) 112 | GREATER => CRel (xn' - 1)
57 | LESS => c) 113 | LESS => c)
58 (*| CUnif _ => raise SynUnif*) 114 (*| CUnif _ => raise SynUnif*)
59 | _ => c, 115 | _ => c,
60 bind = fn ((by, xn), U.Con.Rel _) => (by+1, xn+1) 116 bind = fn ((by, xn), U.Con.RelC _) => (by+1, xn+1)
61 | (ctx, _) => ctx} 117 | (ctx, _) => ctx}
62 118
63 val liftConInCon = liftConInCon 1 119 val liftConInCon = liftConInCon 1
64 120
65 fun subConInCon (xn, rep) = subConInCon' rep (0, xn) 121 fun subConInCon (xn, rep) = subConInCon' rep (0, xn)
203 tryIdentity () 259 tryIdentity ()
204 end) 260 end)
205 | _ => default () 261 | _ => default ()
206 end 262 end
207 | c1' => (CApp ((c1', loc), hnormCon env c2), loc)) 263 | c1' => (CApp ((c1', loc), hnormCon env c2), loc))
264
265 | CKApp (c1, k) =>
266 (case hnormCon env c1 of
267 (CKAbs (_, body), _) => hnormCon env (subKindInCon (0, k) body)
268 | _ => cAll)
208 269
209 | CConcat (c1, c2) => 270 | CConcat (c1, c2) =>
210 (case (hnormCon env c1, hnormCon env c2) of 271 (case (hnormCon env c1, hnormCon env c2) of
211 ((CRecord (k, xcs1), loc), (CRecord (_, xcs2), _)) => 272 ((CRecord (k, xcs1), loc), (CRecord (_, xcs2), _)) =>
212 (CRecord (k, xcs1 @ xcs2), loc) 273 (CRecord (k, xcs1 @ xcs2), loc)