Mercurial > urweb

comparison src/elaborate.sml @ 329:eec65c11d3e2

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
foldTR2
author Adam Chlipala <adamc@hcoop.net>
date Sat, 13 Sep 2008 10:30:45 -0400
parents 58f1260f293f
children 9601c717d2f3
comparison
equal deleted inserted replaced
328:58f1260f293f 329:eec65c11d3e2
34 structure U = ElabUtil 34 structure U = ElabUtil
35 structure D = Disjoint 35 structure D = Disjoint
36 36
37 open Print 37 open Print
38 open ElabPrint 38 open ElabPrint
39 open ElabErr
39 40
40 structure IM = IntBinaryMap 41 structure IM = IntBinaryMap
41 42
42 structure SK = struct 43 structure SK = struct
43 type ord_key = string 44 type ord_key = string
56 57
57 fun occursKind r = 58 fun occursKind r =
58 U.Kind.exists (fn L'.KUnif (_, _, r') => r = r' 59 U.Kind.exists (fn L'.KUnif (_, _, r') => r = r'
59 | _ => false) 60 | _ => false)
60 61
61 datatype kunify_error =
62 KOccursCheckFailed of L'.kind * L'.kind
63 | KIncompatible of L'.kind * L'.kind
64
65 exception KUnify' of kunify_error 62 exception KUnify' of kunify_error
66
67 fun kunifyError err =
68 case err of
69 KOccursCheckFailed (k1, k2) =>
70 eprefaces "Kind occurs check failed"
71 [("Kind 1", p_kind k1),
72 ("Kind 2", p_kind k2)]
73 | KIncompatible (k1, k2) =>
74 eprefaces "Incompatible kinds"
75 [("Kind 1", p_kind k1),
76 ("Kind 2", p_kind k2)]
77 63
78 fun unifyKinds' (k1All as (k1, _)) (k2All as (k2, _)) = 64 fun unifyKinds' (k1All as (k1, _)) (k2All as (k2, _)) =
79 let 65 let
80 fun err f = raise KUnify' (f (k1All, k2All)) 66 fun err f = raise KUnify' (f (k1All, k2All))
81 in 67 in
121 exception KUnify of L'.kind * L'.kind * kunify_error 107 exception KUnify of L'.kind * L'.kind * kunify_error
122 108
123 fun unifyKinds k1 k2 = 109 fun unifyKinds k1 k2 =
124 unifyKinds' k1 k2 110 unifyKinds' k1 k2
125 handle KUnify' err => raise KUnify (k1, k2, err) 111 handle KUnify' err => raise KUnify (k1, k2, err)
126
127 datatype con_error =
128 UnboundCon of ErrorMsg.span * string
129 | UnboundDatatype of ErrorMsg.span * string
130 | UnboundStrInCon of ErrorMsg.span * string
131 | WrongKind of L'.con * L'.kind * L'.kind * kunify_error
132 | DuplicateField of ErrorMsg.span * string
133 | ProjBounds of L'.con * int
134 | ProjMismatch of L'.con * L'.kind
135
136 fun conError env err =
137 case err of
138 UnboundCon (loc, s) =>
139 ErrorMsg.errorAt loc ("Unbound constructor variable " ^ s)
140 | UnboundDatatype (loc, s) =>
141 ErrorMsg.errorAt loc ("Unbound datatype " ^ s)
142 | UnboundStrInCon (loc, s) =>
143 ErrorMsg.errorAt loc ("Unbound structure " ^ s)
144 | WrongKind (c, k1, k2, kerr) =>
145 (ErrorMsg.errorAt (#2 c) "Wrong kind";
146 eprefaces' [("Constructor", p_con env c),
147 ("Have kind", p_kind k1),
148 ("Need kind", p_kind k2)];
149 kunifyError kerr)
150 | DuplicateField (loc, s) =>
151 ErrorMsg.errorAt loc ("Duplicate record field " ^ s)
152 | ProjBounds (c, n) =>
153 (ErrorMsg.errorAt (#2 c) "Out of bounds constructor projection";
154 eprefaces' [("Constructor", p_con env c),
155 ("Index", Print.PD.string (Int.toString n))])
156 | ProjMismatch (c, k) =>
157 (ErrorMsg.errorAt (#2 c) "Projection from non-tuple constructor";
158 eprefaces' [("Constructor", p_con env c),
159 ("Kind", p_kind k)])
160 112
161 fun checkKind env c k1 k2 = 113 fun checkKind env c k1 k2 =
162 unifyKinds k1 k2 114 unifyKinds k1 k2
163 handle KUnify (k1, k2, err) => 115 handle KUnify (k1, k2, err) =>
164 conError env (WrongKind (c, k1, k2, err)) 116 conError env (WrongKind (c, k1, k2, err))
493 fun occursCon r = 445 fun occursCon r =
494 U.Con.exists {kind = fn _ => false, 446 U.Con.exists {kind = fn _ => false,
495 con = fn L'.CUnif (_, _, _, r') => r = r' 447 con = fn L'.CUnif (_, _, _, r') => r = r'
496 | _ => false} 448 | _ => false}
497 449
498 datatype cunify_error =
499 CKind of L'.kind * L'.kind * kunify_error
500 | COccursCheckFailed of L'.con * L'.con
501 | CIncompatible of L'.con * L'.con
502 | CExplicitness of L'.con * L'.con
503 | CKindof of L'.kind * L'.con
504 | CRecordFailure of PD.pp_desc * PD.pp_desc
505
506 exception CUnify' of cunify_error 450 exception CUnify' of cunify_error
507
508 fun cunifyError env err =
509 case err of
510 CKind (k1, k2, kerr) =>
511 (eprefaces "Kind unification failure"
512 [("Kind 1", p_kind k1),
513 ("Kind 2", p_kind k2)];
514 kunifyError kerr)
515 | COccursCheckFailed (c1, c2) =>
516 eprefaces "Constructor occurs check failed"
517 [("Con 1", p_con env c1),
518 ("Con 2", p_con env c2)]
519 | CIncompatible (c1, c2) =>
520 eprefaces "Incompatible constructors"
521 [("Con 1", p_con env c1),
522 ("Con 2", p_con env c2)]
523 | CExplicitness (c1, c2) =>
524 eprefaces "Differing constructor function explicitness"
525 [("Con 1", p_con env c1),
526 ("Con 2", p_con env c2)]
527 | CKindof (k, c) =>
528 eprefaces "Unexpected kind for kindof calculation"
529 [("Kind", p_kind k),
530 ("Con", p_con env c)]
531 | CRecordFailure (s1, s2) =>
532 eprefaces "Can't unify record constructors"
533 [("Summary 1", s1),
534 ("Summary 2", s2)]
535 451
536 exception SynUnif = E.SynUnif 452 exception SynUnif = E.SynUnif
537 453
538 open ElabOps 454 open ElabOps
539 455
799 val clear = case (fs1, others1, fs2, others2) of 715 val clear = case (fs1, others1, fs2, others2) of
800 ([], [], [], []) => true 716 ([], [], [], []) => true
801 | _ => false 717 | _ => false
802 val empty = (L'.CRecord (k, []), dummy) 718 val empty = (L'.CRecord (k, []), dummy)
803 719
720 fun unsummarize {fields, unifs, others} =
721 let
722 val c = (L'.CRecord (k, fields), loc)
723
724 val c = foldl (fn ((c1, _), c2) => (L'.CConcat (c1, c2), loc))
725 c unifs
726 in
727 foldl (fn (c1, c2) => (L'.CConcat (c1, c2), loc))
728 c others
729 end
730
804 fun pairOffUnifs (unifs1, unifs2) = 731 fun pairOffUnifs (unifs1, unifs2) =
805 case (unifs1, unifs2) of 732 case (unifs1, unifs2) of
806 ([], _) => 733 ([], _) =>
807 if clear then 734 if clear then
808 List.app (fn (_, r) => r := SOME empty) unifs2 735 List.app (fn (_, r) => r := SOME empty) unifs2
809 else 736 else
810 raise CUnify' (CRecordFailure (p_summary env s1, p_summary env s2)) 737 raise CUnify' (CRecordFailure (unsummarize s1, unsummarize s2))
811 | (_, []) => 738 | (_, []) =>
812 if clear then 739 if clear then
813 List.app (fn (_, r) => r := SOME empty) unifs1 740 List.app (fn (_, r) => r := SOME empty) unifs1
814 else 741 else
815 raise CUnify' (CRecordFailure (p_summary env s1, p_summary env s2)) 742 raise CUnify' (CRecordFailure (unsummarize s1, unsummarize s2))
816 | ((c1, _) :: rest1, (_, r2) :: rest2) => 743 | ((c1, _) :: rest1, (_, r2) :: rest2) =>
817 (r2 := SOME c1; 744 (r2 := SOME c1;
818 pairOffUnifs (rest1, rest2)) 745 pairOffUnifs (rest1, rest2))
819 in 746 in
820 pairOffUnifs (unifs1, unifs2) 747 pairOffUnifs (unifs1, unifs2)
1025 952
1026 and unifyCons (env, denv) c1 c2 = 953 and unifyCons (env, denv) c1 c2 =
1027 unifyCons' (env, denv) c1 c2 954 unifyCons' (env, denv) c1 c2
1028 handle CUnify' err => raise CUnify (c1, c2, err) 955 handle CUnify' err => raise CUnify (c1, c2, err)
1029 | KUnify args => raise CUnify (c1, c2, CKind args) 956 | KUnify args => raise CUnify (c1, c2, CKind args)
1030
1031 datatype exp_error =
1032 UnboundExp of ErrorMsg.span * string
1033 | UnboundStrInExp of ErrorMsg.span * string
1034 | Unify of L'.exp * L'.con * L'.con * cunify_error
1035 | Unif of string * L'.con
1036 | WrongForm of string * L'.exp * L'.con
1037 | IncompatibleCons of L'.con * L'.con
1038 | DuplicatePatternVariable of ErrorMsg.span * string
1039 | PatUnify of L'.pat * L'.con * L'.con * cunify_error
1040 | UnboundConstructor of ErrorMsg.span * string list * string
1041 | PatHasArg of ErrorMsg.span
1042 | PatHasNoArg of ErrorMsg.span
1043 | Inexhaustive of ErrorMsg.span
1044 | DuplicatePatField of ErrorMsg.span * string
1045 | Unresolvable of ErrorMsg.span * L'.con
1046 | OutOfContext of ErrorMsg.span * (L'.exp * L'.con) option
1047 | IllegalRec of string * L'.exp
1048
1049 fun expError env err =
1050 case err of
1051 UnboundExp (loc, s) =>
1052 ErrorMsg.errorAt loc ("Unbound expression variable " ^ s)
1053 | UnboundStrInExp (loc, s) =>
1054 ErrorMsg.errorAt loc ("Unbound structure " ^ s)
1055 | Unify (e, c1, c2, uerr) =>
1056 (ErrorMsg.errorAt (#2 e) "Unification failure";
1057 eprefaces' [("Expression", p_exp env e),
1058 ("Have con", p_con env c1),
1059 ("Need con", p_con env c2)];
1060 cunifyError env uerr)
1061 | Unif (action, c) =>
1062 (ErrorMsg.errorAt (#2 c) ("Unification variable blocks " ^ action);
1063 eprefaces' [("Con", p_con env c)])
1064 | WrongForm (variety, e, t) =>
1065 (ErrorMsg.errorAt (#2 e) ("Expression is not a " ^ variety);
1066 eprefaces' [("Expression", p_exp env e),
1067 ("Type", p_con env t)])
1068 | IncompatibleCons (c1, c2) =>
1069 (ErrorMsg.errorAt (#2 c1) "Incompatible constructors";
1070 eprefaces' [("Con 1", p_con env c1),
1071 ("Con 2", p_con env c2)])
1072 | DuplicatePatternVariable (loc, s) =>
1073 ErrorMsg.errorAt loc ("Duplicate pattern variable " ^ s)
1074 | PatUnify (p, c1, c2, uerr) =>
1075 (ErrorMsg.errorAt (#2 p) "Unification failure for pattern";
1076 eprefaces' [("Pattern", p_pat env p),
1077 ("Have con", p_con env c1),
1078 ("Need con", p_con env c2)];
1079 cunifyError env uerr)
1080 | UnboundConstructor (loc, ms, s) =>
1081 ErrorMsg.errorAt loc ("Unbound constructor " ^ String.concatWith "." (ms @ [s]) ^ " in pattern")
1082 | PatHasArg loc =>
1083 ErrorMsg.errorAt loc "Constructor expects no argument but is used with argument"
1084 | PatHasNoArg loc =>
1085 ErrorMsg.errorAt loc "Constructor expects argument but is used with no argument"
1086 | Inexhaustive loc =>
1087 ErrorMsg.errorAt loc "Inexhaustive 'case'"
1088 | DuplicatePatField (loc, s) =>
1089 ErrorMsg.errorAt loc ("Duplicate record field " ^ s ^ " in pattern")
1090 | OutOfContext (loc, co) =>
1091 (ErrorMsg.errorAt loc "Type class wildcard occurs out of context";
1092 Option.app (fn (e, c) => eprefaces' [("Function", p_exp env e),
1093 ("Type", p_con env c)]) co)
1094 | Unresolvable (loc, c) =>
1095 (ErrorMsg.errorAt loc "Can't resolve type class instance";
1096 eprefaces' [("Class constraint", p_con env c)])
1097 | IllegalRec (x, e) =>
1098 (ErrorMsg.errorAt (#2 e) "Illegal 'val rec' righthand side (must be a function abstraction)";
1099 eprefaces' [("Variable", PD.string x),
1100 ("Expression", p_exp env e)])
1101 957
1102 fun checkCon (env, denv) e c1 c2 = 958 fun checkCon (env, denv) e c1 c2 =
1103 unifyCons (env, denv) c1 c2 959 unifyCons (env, denv) c1 c2
1104 handle CUnify (c1, c2, err) => 960 handle CUnify (c1, c2, err) =>
1105 (expError env (Unify (e, c1, c2, err)); 961 (expError env (Unify (e, c1, c2, err));
1785 in 1641 in
1786 (*prefaces "elabExp" [("e", SourcePrint.p_exp eAll), 1642 (*prefaces "elabExp" [("e", SourcePrint.p_exp eAll),
1787 ("|tcs|", PD.string (Int.toString (length tcs)))];*) 1643 ("|tcs|", PD.string (Int.toString (length tcs)))];*)
1788 r 1644 r
1789 end 1645 end
1790
1791
1792 datatype decl_error =
1793 KunifsRemain of L'.decl list
1794 | CunifsRemain of L'.decl list
1795 | Nonpositive of L'.decl
1796
1797 fun lspan [] = ErrorMsg.dummySpan
1798 | lspan ((_, loc) :: _) = loc
1799
1800 fun declError env err =
1801 case err of
1802 KunifsRemain ds =>
1803 (ErrorMsg.errorAt (lspan ds) "Some kind unification variables are undetermined in declaration";
1804 eprefaces' [("Decl", p_list_sep PD.newline (p_decl env) ds)])
1805 | CunifsRemain ds =>
1806 (ErrorMsg.errorAt (lspan ds) "Some constructor unification variables are undetermined in declaration";
1807 eprefaces' [("Decl", p_list_sep PD.newline (p_decl env) ds)])
1808 | Nonpositive d =>
1809 (ErrorMsg.errorAt (#2 d) "Non-strictly-positive datatype declaration (could allow non-termination)";
1810 eprefaces' [("Decl", p_decl env d)])
1811
1812 datatype sgn_error =
1813 UnboundSgn of ErrorMsg.span * string
1814 | UnmatchedSgi of L'.sgn_item
1815 | SgiWrongKind of L'.sgn_item * L'.kind * L'.sgn_item * L'.kind * kunify_error
1816 | SgiWrongCon of L'.sgn_item * L'.con * L'.sgn_item * L'.con * cunify_error
1817 | SgiMismatchedDatatypes of L'.sgn_item * L'.sgn_item * (L'.con * L'.con * cunify_error) option
1818 | SgnWrongForm of L'.sgn * L'.sgn
1819 | UnWhereable of L'.sgn * string
1820 | WhereWrongKind of L'.kind * L'.kind * kunify_error
1821 | NotIncludable of L'.sgn
1822 | DuplicateCon of ErrorMsg.span * string
1823 | DuplicateVal of ErrorMsg.span * string
1824 | DuplicateSgn of ErrorMsg.span * string
1825 | DuplicateStr of ErrorMsg.span * string
1826 | NotConstraintsable of L'.sgn
1827
1828 fun sgnError env err =
1829 case err of
1830 UnboundSgn (loc, s) =>
1831 ErrorMsg.errorAt loc ("Unbound signature variable " ^ s)
1832 | UnmatchedSgi (sgi as (_, loc)) =>
1833 (ErrorMsg.errorAt loc "Unmatched signature item";
1834 eprefaces' [("Item", p_sgn_item env sgi)])
1835 | SgiWrongKind (sgi1, k1, sgi2, k2, kerr) =>
1836 (ErrorMsg.errorAt (#2 sgi1) "Kind unification failure in signature matching:";
1837 eprefaces' [("Have", p_sgn_item env sgi1),
1838 ("Need", p_sgn_item env sgi2),
1839 ("Kind 1", p_kind k1),
1840 ("Kind 2", p_kind k2)];
1841 kunifyError kerr)
1842 | SgiWrongCon (sgi1, c1, sgi2, c2, cerr) =>
1843 (ErrorMsg.errorAt (#2 sgi1) "Constructor unification failure in signature matching:";
1844 eprefaces' [("Have", p_sgn_item env sgi1),
1845 ("Need", p_sgn_item env sgi2),
1846 ("Con 1", p_con env c1),
1847 ("Con 2", p_con env c2)];
1848 cunifyError env cerr)
1849 | SgiMismatchedDatatypes (sgi1, sgi2, cerro) =>
1850 (ErrorMsg.errorAt (#2 sgi1) "Mismatched 'datatype' specifications:";
1851 eprefaces' [("Have", p_sgn_item env sgi1),
1852 ("Need", p_sgn_item env sgi2)];
1853 Option.app (fn (c1, c2, ue) =>
1854 (eprefaces "Unification error"
1855 [("Con 1", p_con env c1),
1856 ("Con 2", p_con env c2)];
1857 cunifyError env ue)) cerro)
1858 | SgnWrongForm (sgn1, sgn2) =>
1859 (ErrorMsg.errorAt (#2 sgn1) "Incompatible signatures:";
1860 eprefaces' [("Sig 1", p_sgn env sgn1),
1861 ("Sig 2", p_sgn env sgn2)])
1862 | UnWhereable (sgn, x) =>
1863 (ErrorMsg.errorAt (#2 sgn) "Unavailable field for 'where'";
1864 eprefaces' [("Signature", p_sgn env sgn),
1865 ("Field", PD.string x)])
1866 | WhereWrongKind (k1, k2, kerr) =>
1867 (ErrorMsg.errorAt (#2 k1) "Wrong kind for 'where'";
1868 eprefaces' [("Have", p_kind k1),
1869 ("Need", p_kind k2)];
1870 kunifyError kerr)
1871 | NotIncludable sgn =>
1872 (ErrorMsg.errorAt (#2 sgn) "Invalid signature to 'include'";
1873 eprefaces' [("Signature", p_sgn env sgn)])
1874 | DuplicateCon (loc, s) =>
1875 ErrorMsg.errorAt loc ("Duplicate constructor " ^ s ^ " in signature")
1876 | DuplicateVal (loc, s) =>
1877 ErrorMsg.errorAt loc ("Duplicate value " ^ s ^ " in signature")
1878 | DuplicateSgn (loc, s) =>
1879 ErrorMsg.errorAt loc ("Duplicate signature " ^ s ^ " in signature")
1880 | DuplicateStr (loc, s) =>
1881 ErrorMsg.errorAt loc ("Duplicate structure " ^ s ^ " in signature")
1882 | NotConstraintsable sgn =>
1883 (ErrorMsg.errorAt (#2 sgn) "Invalid signature for 'open constraints'";
1884 eprefaces' [("Signature", p_sgn env sgn)])
1885
1886 datatype str_error =
1887 UnboundStr of ErrorMsg.span * string
1888 | NotFunctor of L'.sgn
1889 | FunctorRebind of ErrorMsg.span
1890 | UnOpenable of L'.sgn
1891 | NotType of L'.kind * (L'.kind * L'.kind * kunify_error)
1892 | DuplicateConstructor of string * ErrorMsg.span
1893 | NotDatatype of ErrorMsg.span
1894
1895 fun strError env err =
1896 case err of
1897 UnboundStr (loc, s) =>
1898 ErrorMsg.errorAt loc ("Unbound structure variable " ^ s)
1899 | NotFunctor sgn =>
1900 (ErrorMsg.errorAt (#2 sgn) "Application of non-functor";
1901 eprefaces' [("Signature", p_sgn env sgn)])
1902 | FunctorRebind loc =>
1903 ErrorMsg.errorAt loc "Attempt to rebind functor"
1904 | UnOpenable sgn =>
1905 (ErrorMsg.errorAt (#2 sgn) "Un-openable structure";
1906 eprefaces' [("Signature", p_sgn env sgn)])
1907 | NotType (k, (k1, k2, ue)) =>
1908 (ErrorMsg.errorAt (#2 k) "'val' type kind is not 'Type'";
1909 eprefaces' [("Kind", p_kind k),
1910 ("Subkind 1", p_kind k1),
1911 ("Subkind 2", p_kind k2)];
1912 kunifyError ue)
1913 | DuplicateConstructor (x, loc) =>
1914 ErrorMsg.errorAt loc ("Duplicate datatype constructor " ^ x)
1915 | NotDatatype loc =>
1916 ErrorMsg.errorAt loc "Trying to import non-datatype as a datatype"
1917 1646
1918 val hnormSgn = E.hnormSgn 1647 val hnormSgn = E.hnormSgn
1919 1648
1920 fun tableOf () = (L'.CModProj (!basis_r, [], "sql_table"), ErrorMsg.dummySpan) 1649 fun tableOf () = (L'.CModProj (!basis_r, [], "sql_table"), ErrorMsg.dummySpan)
1921 1650
3525 [] => () 3254 [] => ()
3526 | _ => raise Fail "Unresolved disjointness constraints in top.urs" 3255 | _ => raise Fail "Unresolved disjointness constraints in top.urs"
3527 val (topStr, topSgn', gs) = elabStr (env', D.empty) (L.StrConst topStr, ErrorMsg.dummySpan) 3256 val (topStr, topSgn', gs) = elabStr (env', D.empty) (L.StrConst topStr, ErrorMsg.dummySpan)
3528 val () = case gs of 3257 val () = case gs of
3529 [] => () 3258 [] => ()
3530 | _ => (app (fn Disjoint (_, env, _, c1, c2) => 3259 | _ => app (fn Disjoint (loc, env, denv, c1, c2) =>
3531 prefaces "Unresolved" 3260 (case D.prove env denv (c1, c2, loc) of
3532 [("c1", p_con env c1), 3261 [] => ()
3533 ("c2", p_con env c2)] 3262 | _ =>
3534 | TypeClass _ => TextIO.print "Type class\n") gs; 3263 (prefaces "Unresolved constraint in top.ur"
3535 raise Fail "Unresolved constraints in top.ur") 3264 [("loc", PD.string (ErrorMsg.spanToString loc)),
3265 ("c1", p_con env c1),
3266 ("c2", p_con env c2)];
3267 raise Fail "Unresolve constraint in top.ur"))
3268 | TypeClass _ => raise Fail "Unresolved type class constraint in top.ur") gs
3536 val () = subSgn (env', D.empty) topSgn' topSgn 3269 val () = subSgn (env', D.empty) topSgn' topSgn
3537 3270
3538 val (env', top_n) = E.pushStrNamed env' "Top" topSgn 3271 val (env', top_n) = E.pushStrNamed env' "Top" topSgn
3539 3272
3540 val (ds', (env', _)) = dopen (env', D.empty) {str = top_n, strs = [], sgn = topSgn} 3273 val (ds', (env', _)) = dopen (env', D.empty) {str = top_n, strs = [], sgn = topSgn}