Mercurial > urweb

comparison src/elaborate.sml @ 149:7420fa18d657

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Record cut
author Adam Chlipala <adamc@hcoop.net>
date Thu, 24 Jul 2008 10:09:21 -0400
parents eb16f2aadbe9
children 67ab26888839
comparison
equal deleted inserted replaced
148:15e8b9775539 149:7420fa18d657
893 | _ => raise Fail "typeof: Bad ECApp") 893 | _ => raise Fail "typeof: Bad ECApp")
894 | L'.ECAbs (expl, x, k, e1) => (L'.TCFun (expl, x, k, typeof (E.pushCRel env x k) e1), loc) 894 | L'.ECAbs (expl, x, k, e1) => (L'.TCFun (expl, x, k, typeof (E.pushCRel env x k) e1), loc)
895 895
896 | L'.ERecord xes => (L'.TRecord (L'.CRecord (ktype, map (fn (x, _, t) => (x, t)) xes), loc), loc) 896 | L'.ERecord xes => (L'.TRecord (L'.CRecord (ktype, map (fn (x, _, t) => (x, t)) xes), loc), loc)
897 | L'.EField (_, _, {field, ...}) => field 897 | L'.EField (_, _, {field, ...}) => field
898 | L'.ECut (_, _, {rest, ...}) => (L'.TRecord rest, loc)
898 | L'.EFold dom => foldType (dom, loc) 899 | L'.EFold dom => foldType (dom, loc)
899 900
900 | L'.EError => cerror 901 | L'.EError => cerror
901 902
902 fun elabHead (env, denv) (e as (_, loc)) t = 903 fun elabHead (env, denv) (e as (_, loc)) t =
1104 checkCon (env, denv) e' et 1105 checkCon (env, denv) e' et
1105 (L'.TRecord (L'.CConcat (first, rest), loc), loc) 1106 (L'.TRecord (L'.CConcat (first, rest), loc), loc)
1106 val gs4 = D.prove env denv (first, rest, loc) 1107 val gs4 = D.prove env denv (first, rest, loc)
1107 in 1108 in
1108 ((L'.EField (e', c', {field = ft, rest = rest}), loc), ft, gs1 @ gs2 @ gs3 @ gs4) 1109 ((L'.EField (e', c', {field = ft, rest = rest}), loc), ft, gs1 @ gs2 @ gs3 @ gs4)
1110 end
1111
1112 | L.ECut (e, c) =>
1113 let
1114 val (e', et, gs1) = elabExp (env, denv) e
1115 val (c', ck, gs2) = elabCon (env, denv) c
1116
1117 val ft = cunif (loc, ktype)
1118 val rest = cunif (loc, ktype_record)
1119 val first = (L'.CRecord (ktype, [(c', ft)]), loc)
1120
1121 val gs3 =
1122 checkCon (env, denv) e' et
1123 (L'.TRecord (L'.CConcat (first, rest), loc), loc)
1124 val gs4 = D.prove env denv (first, rest, loc)
1125 in
1126 ((L'.ECut (e', c', {field = ft, rest = rest}), loc), (L'.TRecord rest, loc), gs1 @ gs2 @ gs3 @ gs4)
1109 end 1127 end
1110 1128
1111 | L.EFold => 1129 | L.EFold =>
1112 let 1130 let
1113 val dom = kunif loc 1131 val dom = kunif loc