Mercurial > urweb

comparison src/elaborate.sml @ 898:d1d0b18afd3d

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Working on Grid; have gone from one dynamic table bizareness to another
author Adam Chlipala <adamc@hcoop.net>
date Sun, 19 Jul 2009 17:45:02 -0400
parents e571fb150a9f
children 6d9538ce94d8
comparison
equal deleted inserted replaced
897:2faf558b2d05 898:d1d0b18afd3d
1114 | _ => false) 1114 | _ => false)
1115 | _ => false 1115 | _ => false
1116 1116
1117 fun elabHead (env, denv) infer (e as (_, loc)) t = 1117 fun elabHead (env, denv) infer (e as (_, loc)) t =
1118 let 1118 let
1119 fun unravelKind (t, e) =
1120 case hnormCon env t of
1121 (L'.TKFun (x, t'), _) =>
1122 let
1123 val u = kunif loc
1124
1125 val t'' = subKindInCon (0, u) t'
1126 in
1127 unravelKind (t'', (L'.EKApp (e, u), loc))
1128 end
1129 | t => (e, t, [])
1130
1119 fun unravel (t, e) = 1131 fun unravel (t, e) =
1120 case hnormCon env t of 1132 case hnormCon env t of
1121 (L'.TKFun (x, t'), _) => 1133 (L'.TKFun (x, t'), _) =>
1122 let 1134 let
1123 val u = kunif loc 1135 val u = kunif loc
1182 else 1194 else
1183 (e, t, []) 1195 (e, t, [])
1184 | t => (e, t, []) 1196 | t => (e, t, [])
1185 in 1197 in
1186 case infer of 1198 case infer of
1187 L.DontInfer => (e, t, []) 1199 L.DontInfer => unravelKind (t, e)
1188 | _ => unravel (t, e) 1200 | _ => unravel (t, e)
1189 end 1201 end
1190 1202
1191 fun elabPat (pAll as (p, loc), (env, bound)) = 1203 fun elabPat (pAll as (p, loc), (env, bound)) =
1192 let 1204 let