comparison src/elaborate.sml @ 280:fdd7a698be01

Compiling a parametrized query the inefficient way
author Adam Chlipala <adamc@hcoop.net>
date Tue, 02 Sep 2008 17:31:45 -0400
parents 42dfb0d61cf0
children 77a28e7430bf
comparison
equal deleted inserted replaced
279:8bb46d87b074 280:fdd7a698be01
1480 end 1480 end
1481 | _ => ((c, loc), []) 1481 | _ => ((c, loc), [])
1482 1482
1483 fun elabExp (env, denv) (eAll as (e, loc)) = 1483 fun elabExp (env, denv) (eAll as (e, loc)) =
1484 let 1484 let
1485 1485 (*val () = eprefaces "elabExp" [("eAll", SourcePrint.p_exp eAll)];*)
1486 in 1486
1487 (*eprefaces "elabExp" [("eAll", SourcePrint.p_exp eAll)];*) 1487 val r = case e of
1488
1489 case e of
1490 L.EAnnot (e, t) => 1488 L.EAnnot (e, t) =>
1491 let 1489 let
1492 val (e', et, gs1) = elabExp (env, denv) e 1490 val (e', et, gs1) = elabExp (env, denv) e
1493 val (t', _, gs2) = elabCon (env, denv) t 1491 val (t', _, gs2) = elabCon (env, denv) t
1494 val gs3 = checkCon (env, denv) e' et t' 1492 val gs3 = checkCon (env, denv) e' et t'
1754 else 1752 else
1755 expError env (Inexhaustive loc); 1753 expError env (Inexhaustive loc);
1756 1754
1757 ((L'.ECase (e', pes', {disc = et, result = result}), loc), result, enD gs' @ gs) 1755 ((L'.ECase (e', pes', {disc = et, result = result}), loc), result, enD gs' @ gs)
1758 end 1756 end
1757
1758 (*val tcs = List.filter (fn TypeClass _ => true | _ => false) (#3 r)*)
1759 in
1760 (*prefaces "elabExp" [("e", SourcePrint.p_exp eAll),
1761 ("|tcs|", PD.string (Int.toString (length tcs)))];*)
1762 r
1759 end 1763 end
1760 1764
1761 1765
1762 datatype decl_error = 1766 datatype decl_error =
1763 KunifsRemain of L'.decl list 1767 KunifsRemain of L'.decl list
2729 end 2733 end
2730 2734
2731 | _ => sgnError env (SgnWrongForm (sgn1, sgn2)) 2735 | _ => sgnError env (SgnWrongForm (sgn1, sgn2))
2732 2736
2733 2737
2734 fun elabDecl ((d, loc), (env, denv, gs : constraint list)) = 2738 fun elabDecl (dAll as (d, loc), (env, denv, gs : constraint list)) =
2735 let 2739 let
2736 (*val () = preface ("elabDecl", SourcePrint.p_decl (d, loc))*) 2740 (*val () = preface ("elabDecl", SourcePrint.p_decl (d, loc))*)
2737 2741
2738 val r = 2742 val r =
2739 case d of 2743 case d of
2871 val (c', _, gs1) = case co of 2875 val (c', _, gs1) = case co of
2872 NONE => (cunif (loc, ktype), ktype, []) 2876 NONE => (cunif (loc, ktype), ktype, [])
2873 | SOME c => elabCon (env, denv) c 2877 | SOME c => elabCon (env, denv) c
2874 in 2878 in
2875 ((x, c', e), enD gs1 @ gs) 2879 ((x, c', e), enD gs1 @ gs)
2876 end) [] vis 2880 end) gs vis
2877 2881
2878 val (vis, env) = ListUtil.foldlMap (fn ((x, c', e), env) => 2882 val (vis, env) = ListUtil.foldlMap (fn ((x, c', e), env) =>
2879 let 2883 let
2880 val (env, n) = E.pushENamed env x c' 2884 val (env, n) = E.pushENamed env x c'
2881 in 2885 in
3101 end 3105 end
3102 3106
3103 | L.DClass (x, c) => 3107 | L.DClass (x, c) =>
3104 let 3108 let
3105 val k = (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc) 3109 val k = (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc)
3106 val (c', ck, gs) = elabCon (env, denv) c 3110 val (c', ck, gs') = elabCon (env, denv) c
3107 val (env, n) = E.pushCNamed env x k (SOME c') 3111 val (env, n) = E.pushCNamed env x k (SOME c')
3108 val env = E.pushClass env n 3112 val env = E.pushClass env n
3109 in 3113 in
3110 checkKind env c' ck k; 3114 checkKind env c' ck k;
3111 ([(L'.DClass (x, n, c'), loc)], (env, denv, [])) 3115 ([(L'.DClass (x, n, c'), loc)], (env, denv, enD gs' @ gs))
3112 end 3116 end
3113 3117
3114 | L.DDatabase s => ([(L'.DDatabase s, loc)], (env, denv, [])) 3118 | L.DDatabase s => ([(L'.DDatabase s, loc)], (env, denv, gs))
3119
3120 (*val tcs = List.filter (fn TypeClass _ => true | _ => false) (#3 (#2 r))*)
3115 in 3121 in
3122 (*prefaces "elabDecl" [("e", SourcePrint.p_decl dAll),
3123 ("|tcs|", PD.string (Int.toString (length tcs)))];*)
3124
3116 r 3125 r
3117 end 3126 end
3118 3127
3119 and elabStr (env, denv) (str, loc) = 3128 and elabStr (env, denv) (str, loc) =
3120 case str of 3129 case str of