Mercurial > urweb

comparison src/elaborate.sml @ 238:44a1663ad893

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Checking for well-formed 'val rec'
author Adam Chlipala <adamc@hcoop.net>
date Thu, 28 Aug 2008 13:13:16 -0400
parents c466678af854
children 2b9dfaffb008
comparison
equal deleted inserted replaced
237:9182068c9d7c 238:44a1663ad893
1031 | PatHasNoArg of ErrorMsg.span 1031 | PatHasNoArg of ErrorMsg.span
1032 | Inexhaustive of ErrorMsg.span 1032 | Inexhaustive of ErrorMsg.span
1033 | DuplicatePatField of ErrorMsg.span * string 1033 | DuplicatePatField of ErrorMsg.span * string
1034 | Unresolvable of ErrorMsg.span * L'.con 1034 | Unresolvable of ErrorMsg.span * L'.con
1035 | OutOfContext of ErrorMsg.span * (L'.exp * L'.con) option 1035 | OutOfContext of ErrorMsg.span * (L'.exp * L'.con) option
1036 | IllegalRec of string * L'.exp
1036 1037
1037 fun expError env err = 1038 fun expError env err =
1038 case err of 1039 case err of
1039 UnboundExp (loc, s) => 1040 UnboundExp (loc, s) =>
1040 ErrorMsg.errorAt loc ("Unbound expression variable " ^ s) 1041 ErrorMsg.errorAt loc ("Unbound expression variable " ^ s)
1080 Option.app (fn (e, c) => eprefaces' [("Function", p_exp env e), 1081 Option.app (fn (e, c) => eprefaces' [("Function", p_exp env e),
1081 ("Type", p_con env c)]) co) 1082 ("Type", p_con env c)]) co)
1082 | Unresolvable (loc, c) => 1083 | Unresolvable (loc, c) =>
1083 (ErrorMsg.errorAt loc "Can't resolve type class instance"; 1084 (ErrorMsg.errorAt loc "Can't resolve type class instance";
1084 eprefaces' [("Class constraint", p_con env c)]) 1085 eprefaces' [("Class constraint", p_con env c)])
1086 | IllegalRec (x, e) =>
1087 (ErrorMsg.errorAt (#2 e) "Illegal 'val rec' righthand side (must be a function abstraction)";
1088 eprefaces' [("Variable", PD.string x),
1089 ("Expression", p_exp env e)])
1085 1090
1086 fun checkCon (env, denv) e c1 c2 = 1091 fun checkCon (env, denv) e c1 c2 =
1087 unifyCons (env, denv) c1 c2 1092 unifyCons (env, denv) c1 c2
1088 handle CUnify (c1, c2, err) => 1093 handle CUnify (c1, c2, err) =>
1089 (expError env (Unify (e, c1, c2, err)); 1094 (expError env (Unify (e, c1, c2, err));
2824 ("c'", p_con env c')];*) 2829 ("c'", p_con env c')];*)
2825 ([(L'.DVal (x, n, c', e'), loc)], (env', denv, enD gs1 @ gs2 @ enD gs3 @ enD gs4 @ gs)) 2830 ([(L'.DVal (x, n, c', e'), loc)], (env', denv, enD gs1 @ gs2 @ enD gs3 @ enD gs4 @ gs))
2826 end 2831 end
2827 | L.DValRec vis => 2832 | L.DValRec vis =>
2828 let 2833 let
2834 fun allowable (e, _) =
2835 case e of
2836 L.EAbs _ => true
2837 | L.ECAbs (_, _, _, e) => allowable e
2838 | L.EDisjoint (_, _, e) => allowable e
2839 | _ => false
2840
2829 val (vis, gs) = ListUtil.foldlMap 2841 val (vis, gs) = ListUtil.foldlMap
2830 (fn ((x, co, e), gs) => 2842 (fn ((x, co, e), gs) =>
2831 let 2843 let
2832 val (c', _, gs1) = case co of 2844 val (c', _, gs1) = case co of
2833 NONE => (cunif (loc, ktype), ktype, []) 2845 NONE => (cunif (loc, ktype), ktype, [])
2847 let 2859 let
2848 val (e', et, gs1) = elabExp (env, denv) e 2860 val (e', et, gs1) = elabExp (env, denv) e
2849 2861
2850 val gs2 = checkCon (env, denv) e' et c' 2862 val gs2 = checkCon (env, denv) e' et c'
2851 in 2863 in
2864 if allowable e then
2865 ()
2866 else
2867 expError env (IllegalRec (x, e'));
2852 ((x, n, c', e'), gs1 @ enD gs2 @ gs) 2868 ((x, n, c', e'), gs1 @ enD gs2 @ gs)
2853 end) gs vis 2869 end) gs vis
2854 in 2870 in
2855 ([(L'.DValRec vis, loc)], (env, denv, gs)) 2871 ([(L'.DValRec vis, loc)], (env, denv, gs))
2856 end 2872 end