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