Mercurial > urweb

comparison src/elaborate.sml @ 30:e6ccf961d8a3

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Parsing and printing basic module system
author Adam Chlipala <adamc@hcoop.net>
date Thu, 12 Jun 2008 14:04:22 -0400
parents 537db4ee89f4
children 1c91c5e6840f
comparison
equal deleted inserted replaced
29:537db4ee89f4 30:e6ccf961d8a3
863 | CunifsRemainExp (loc, e) => 863 | CunifsRemainExp (loc, e) =>
864 (ErrorMsg.errorAt loc "Some constructor unification variables are undetermined in expression"; 864 (ErrorMsg.errorAt loc "Some constructor unification variables are undetermined in expression";
865 eprefaces' [("Expression", p_exp env e)]) 865 eprefaces' [("Expression", p_exp env e)])
866 866
867 fun elabDecl env (d, loc) = 867 fun elabDecl env (d, loc) =
868 (resetKunif (); 868 let
869 resetCunif (); 869
870 case d of 870 in
871 L.DCon (x, ko, c) => 871 resetKunif ();
872 let 872 resetCunif ();
873 val k' = case ko of 873 case d of
874 NONE => kunif () 874 L.DCon (x, ko, c) =>
875 | SOME k => elabKind k 875 let
876 876 val k' = case ko of
877 val (c', ck) = elabCon env c 877 NONE => kunif ()
878 val (env', n) = E.pushCNamed env x k' (SOME c') 878 | SOME k => elabKind k
879 in 879
880 checkKind env c' ck k'; 880 val (c', ck) = elabCon env c
881 881 val (env', n) = E.pushCNamed env x k' (SOME c')
882 if ErrorMsg.anyErrors () then 882 in
883 () 883 checkKind env c' ck k';
884 else ( 884
885 if kunifsInKind k' then 885 if ErrorMsg.anyErrors () then
886 declError env (KunifsRemainKind (loc, k')) 886 ()
887 else 887 else (
888 (); 888 if kunifsInKind k' then
889 889 declError env (KunifsRemainKind (loc, k'))
890 if kunifsInCon c' then 890 else
891 declError env (KunifsRemainCon (loc, c')) 891 ();
892 else 892
893 () 893 if kunifsInCon c' then
894 ); 894 declError env (KunifsRemainCon (loc, c'))
895 895 else
896 (env', 896 ()
897 (L'.DCon (x, n, k', c'), loc)) 897 );
898 end 898
899 | L.DVal (x, co, e) => 899 (env',
900 let 900 (L'.DCon (x, n, k', c'), loc))
901 val (c', ck) = case co of 901 end
902 NONE => (cunif ktype, ktype) 902 | L.DVal (x, co, e) =>
903 | SOME c => elabCon env c 903 let
904 904 val (c', ck) = case co of
905 val (e', et) = elabExp env e 905 NONE => (cunif ktype, ktype)
906 val (env', n) = E.pushENamed env x c' 906 | SOME c => elabCon env c
907 in 907
908 checkCon env e' et c'; 908 val (e', et) = elabExp env e
909 909 val (env', n) = E.pushENamed env x c'
910 if ErrorMsg.anyErrors () then 910 in
911 () 911 checkCon env e' et c';
912 else ( 912
913 if kunifsInCon c' then 913 if ErrorMsg.anyErrors () then
914 declError env (KunifsRemainCon (loc, c')) 914 ()
915 else 915 else (
916 (); 916 if kunifsInCon c' then
917 917 declError env (KunifsRemainCon (loc, c'))
918 if cunifsInCon c' then 918 else
919 declError env (CunifsRemainCon (loc, c')) 919 ();
920 else 920
921 (); 921 if cunifsInCon c' then
922 922 declError env (CunifsRemainCon (loc, c'))
923 if kunifsInExp e' then 923 else
924 declError env (KunifsRemainExp (loc, e')) 924 ();
925 else 925
926 (); 926 if kunifsInExp e' then
927 927 declError env (KunifsRemainExp (loc, e'))
928 if cunifsInExp e' then 928 else
929 declError env (CunifsRemainExp (loc, e')) 929 ();
930 else 930
931 ()); 931 if cunifsInExp e' then
932 932 declError env (CunifsRemainExp (loc, e'))
933 (env', 933 else
934 (L'.DVal (x, n, c', e'), loc)) 934 ());
935 end) 935
936 (env',
937 (L'.DVal (x, n, c', e'), loc))
938 end
939
940 | L.DSgn _ => raise Fail "Not ready to elaborate signature"
941 | L.DStr _ => raise Fail "Not ready to elaborate structure"
942 end
936 943
937 fun elabFile env ds = 944 fun elabFile env ds =
938 ListUtil.mapfoldl (fn (d, env) => elabDecl env d) env ds 945 ListUtil.mapfoldl (fn (d, env) => elabDecl env d) env ds
939 946
940 end 947 end