Mercurial > urweb
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 |