Mercurial > urweb
comparison src/elaborate.sml @ 140:f214c535d253
A simpler context encoding
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Sun, 20 Jul 2008 10:40:25 -0400 |
parents | adfa2c7a75da |
children | 63c699450281 |
comparison
equal
deleted
inserted
replaced
139:adfa2c7a75da | 140:f214c535d253 |
---|---|
961 | SOME t => t | 961 | SOME t => t |
962 in | 962 in |
963 ((L'.EModProj (n, ms, s), loc), t, []) | 963 ((L'.EModProj (n, ms, s), loc), t, []) |
964 end) | 964 end) |
965 | 965 |
966 | L.EApp (arg as ((L.EApp ((L.ECApp ((L.EVar (["Basis"], "join"), _), (L.CWild _, _)), _), xml1), _), xml2)) => | 966 (*| L.EApp (arg as ((L.EApp ((L.ECApp ((L.EVar (["Basis"], "join"), _), (L.CWild _, _)), _), xml1), _), xml2)) => |
967 let | 967 let |
968 val (xml1', t1, gs1) = elabExp (env, denv) xml1 | 968 val (xml1', t1, gs1) = elabExp (env, denv) xml1 |
969 val (xml2', t2, gs2) = elabExp (env, denv) xml2 | 969 val (xml2', t2, gs2) = elabExp (env, denv) xml2 |
970 | 970 |
971 val kunit = (L'.KUnit, loc) | 971 val kunit = (L'.KUnit, loc) |
1065 (e, t, (loc, env, denv, shared, ctx1) | 1065 (e, t, (loc, env, denv, shared, ctx1) |
1066 :: (loc, env, denv, shared, ctx2) | 1066 :: (loc, env, denv, shared, ctx2) |
1067 :: (loc, env, denv, use1, use2) | 1067 :: (loc, env, denv, use1, use2) |
1068 :: (loc, env, denv, bind1, bind2) | 1068 :: (loc, env, denv, bind1, bind2) |
1069 :: gs1 @ gs2 @ gs3 @ gs4 @ gs5 @ gs6 @ gs7 @ gs8) | 1069 :: gs1 @ gs2 @ gs3 @ gs4 @ gs5 @ gs6 @ gs7 @ gs8) |
1070 end | 1070 end*) |
1071 | 1071 |
1072 | L.EApp (e1, e2) => | 1072 | L.EApp (e1, e2) => |
1073 let | 1073 let |
1074 val (e1', t1, gs1) = elabExp (env, denv) e1 | 1074 val (e1', t1, gs1) = elabExp (env, denv) e1 |
1075 val (e1', t1, gs2) = elabHead (env, denv) e1' t1 | 1075 val (e1', t1, gs2) = elabHead (env, denv) e1' t1 |