Mercurial > urweb

comparison src/elaborate.sml @ 171:c7a6e6dbc318

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Elaborating some basic pattern matching
author Adam Chlipala <adamc@hcoop.net>
date Thu, 31 Jul 2008 10:06:27 -0400
parents a158f8c5aa55
children 021f5beb6f8d
comparison
equal deleted inserted replaced
170:a158f8c5aa55 171:c7a6e6dbc318
807 | UnboundStrInExp of ErrorMsg.span * string 807 | UnboundStrInExp of ErrorMsg.span * string
808 | Unify of L'.exp * L'.con * L'.con * cunify_error 808 | Unify of L'.exp * L'.con * L'.con * cunify_error
809 | Unif of string * L'.con 809 | Unif of string * L'.con
810 | WrongForm of string * L'.exp * L'.con 810 | WrongForm of string * L'.exp * L'.con
811 | IncompatibleCons of L'.con * L'.con 811 | IncompatibleCons of L'.con * L'.con
812 | DuplicatePatternVariable of ErrorMsg.span * string
813 | PatUnify of L'.pat * L'.con * L'.con * cunify_error
814 | UnboundConstructor of ErrorMsg.span * string
815 | PatHasArg of ErrorMsg.span
816 | PatHasNoArg of ErrorMsg.span
812 817
813 fun expError env err = 818 fun expError env err =
814 case err of 819 case err of
815 UnboundExp (loc, s) => 820 UnboundExp (loc, s) =>
816 ErrorMsg.errorAt loc ("Unbound expression variable " ^ s) 821 ErrorMsg.errorAt loc ("Unbound expression variable " ^ s)
831 ("Type", p_con env t)]) 836 ("Type", p_con env t)])
832 | IncompatibleCons (c1, c2) => 837 | IncompatibleCons (c1, c2) =>
833 (ErrorMsg.errorAt (#2 c1) "Incompatible constructors"; 838 (ErrorMsg.errorAt (#2 c1) "Incompatible constructors";
834 eprefaces' [("Con 1", p_con env c1), 839 eprefaces' [("Con 1", p_con env c1),
835 ("Con 2", p_con env c2)]) 840 ("Con 2", p_con env c2)])
841 | DuplicatePatternVariable (loc, s) =>
842 ErrorMsg.errorAt loc ("Duplicate pattern variable " ^ s)
843 | PatUnify (p, c1, c2, uerr) =>
844 (ErrorMsg.errorAt (#2 p) "Unification failure for pattern";
845 eprefaces' [("Pattern", p_pat env p),
846 ("Have con", p_con env c1),
847 ("Need con", p_con env c2)];
848 cunifyError env uerr)
849 | UnboundConstructor (loc, s) =>
850 ErrorMsg.errorAt loc ("Unbound constructor " ^ s ^ " in pattern")
851 | PatHasArg loc =>
852 ErrorMsg.errorAt loc "Constructor expects no argument but is used with argument"
853 | PatHasNoArg loc =>
854 ErrorMsg.errorAt loc "Constructor expects argument but is used with no argument"
836 855
837 fun checkCon (env, denv) e c1 c2 = 856 fun checkCon (env, denv) e c1 c2 =
838 unifyCons (env, denv) c1 c2 857 unifyCons (env, denv) c1 c2
839 handle CUnify (c1, c2, err) => 858 handle CUnify (c1, c2, err) =>
840 (expError env (Unify (e, c1, c2, err)); 859 (expError env (Unify (e, c1, c2, err));
860 [])
861
862 fun checkPatCon (env, denv) p c1 c2 =
863 unifyCons (env, denv) c1 c2
864 handle CUnify (c1, c2, err) =>
865 (expError env (PatUnify (p, c1, c2, err));
841 []) 866 [])
842 867
843 fun primType env p = 868 fun primType env p =
844 case p of 869 case p of
845 P.Int _ => !int 870 P.Int _ => !int
901 | L'.ERecord xes => (L'.TRecord (L'.CRecord (ktype, map (fn (x, _, t) => (x, t)) xes), loc), loc) 926 | L'.ERecord xes => (L'.TRecord (L'.CRecord (ktype, map (fn (x, _, t) => (x, t)) xes), loc), loc)
902 | L'.EField (_, _, {field, ...}) => field 927 | L'.EField (_, _, {field, ...}) => field
903 | L'.ECut (_, _, {rest, ...}) => (L'.TRecord rest, loc) 928 | L'.ECut (_, _, {rest, ...}) => (L'.TRecord rest, loc)
904 | L'.EFold dom => foldType (dom, loc) 929 | L'.EFold dom => foldType (dom, loc)
905 930
931 | L'.ECase (_, _, t) => t
932
906 | L'.EError => cerror 933 | L'.EError => cerror
907 934
908 fun elabHead (env, denv) (e as (_, loc)) t = 935 fun elabHead (env, denv) (e as (_, loc)) t =
909 let 936 let
910 fun unravel (t, e) = 937 fun unravel (t, e) =
923 end 950 end
924 | _ => (e, t, gs) 951 | _ => (e, t, gs)
925 end 952 end
926 in 953 in
927 unravel (t, e) 954 unravel (t, e)
955 end
956
957 fun elabPat (pAll as (p, loc), (env, bound)) =
958 let
959 val perror = (L'.PWild, loc)
960 val terror = (L'.CError, loc)
961 val pterror = (perror, terror)
962 val rerror = (pterror, (env, bound))
963
964 fun pcon (pc, po, to, dn) =
965
966 case (po, to) of
967 (NONE, SOME _) => (expError env (PatHasNoArg loc);
968 rerror)
969 | (SOME _, NONE) => (expError env (PatHasArg loc);
970 rerror)
971 | (NONE, NONE) => (((L'.PCon (pc, NONE), loc), (L'.CNamed dn, loc)),
972 (env, bound))
973 | (SOME p, SOME t) =>
974 let
975 val ((p', pt), (env, bound)) = elabPat (p, (env, bound))
976 in
977 (((L'.PCon (pc, SOME p'), loc), (L'.CNamed dn, loc)),
978 (env, bound))
979 end
980 in
981 case p of
982 L.PWild => (((L'.PWild, loc), cunif (loc, (L'.KType, loc))),
983 (env, bound))
984 | L.PVar x =>
985 let
986 val t = if SS.member (bound, x) then
987 (expError env (DuplicatePatternVariable (loc, x));
988 terror)
989 else
990 cunif (loc, (L'.KType, loc))
991 in
992 (((L'.PVar x, loc), t),
993 (E.pushERel env x t, SS.add (bound, x)))
994 end
995 | L.PCon ([], x, po) =>
996 (case E.lookupConstructor env x of
997 NONE => (expError env (UnboundConstructor (loc, x));
998 rerror)
999 | SOME (n, to, dn) => pcon (L'.PConVar n, po, to, dn))
1000 | L.PCon _ => raise Fail "uhoh"
928 end 1001 end
929 1002
930 fun elabExp (env, denv) (eAll as (e, loc)) = 1003 fun elabExp (env, denv) (eAll as (e, loc)) =
931 let 1004 let
932 1005
1136 val dom = kunif loc 1209 val dom = kunif loc
1137 in 1210 in
1138 ((L'.EFold dom, loc), foldType (dom, loc), []) 1211 ((L'.EFold dom, loc), foldType (dom, loc), [])
1139 end 1212 end
1140 1213
1141 | L.ECase _ => raise Fail "Elaborate ECase" 1214 | L.ECase (e, pes) =>
1215 let
1216 val (e', et, gs1) = elabExp (env, denv) e
1217 val result = cunif (loc, (L'.KType, loc))
1218 val (pes', gs) = ListUtil.foldlMap
1219 (fn ((p, e), gs) =>
1220 let
1221 val ((p', pt), (env, _)) = elabPat (p, (env, SS.empty))
1222
1223 val gs1 = checkPatCon (env, denv) p' pt et
1224 val (e', et, gs2) = elabExp (env, denv) e
1225 val gs3 = checkCon (env, denv) e' et result
1226 in
1227 ((p', e'), gs1 @ gs2 @ gs3 @ gs)
1228 end)
1229 gs1 pes
1230 in
1231 ((L'.ECase (e', pes', result), loc), result, gs)
1232 end
1142 end 1233 end
1143 1234
1144 1235
1145 datatype decl_error = 1236 datatype decl_error =
1146 KunifsRemain of L'.decl list 1237 KunifsRemain of L'.decl list
1959 else 2050 else
1960 (); 2051 ();
1961 ((x, n', to), (SS.add (used, x), env, gs')) 2052 ((x, n', to), (SS.add (used, x), env, gs'))
1962 end) 2053 end)
1963 (SS.empty, env, []) xcs 2054 (SS.empty, env, []) xcs
2055
2056 val env = E.pushDatatype env n xcs
1964 in 2057 in
1965 ([(L'.DDatatype (x, n, xcs), loc)], (env, denv, gs)) 2058 ([(L'.DDatatype (x, n, xcs), loc)], (env, denv, gs))
1966 end 2059 end
1967 2060
1968 | L.DDatatypeImp (_, [], _) => raise Fail "Empty DDatatypeImp" 2061 | L.DDatatypeImp (_, [], _) => raise Fail "Empty DDatatypeImp"