summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adam@chlipala.net>2012-04-22 09:08:45 -0400
committerGravatar Adam Chlipala <adam@chlipala.net>2012-04-22 09:08:45 -0400
commit210ec59c8cc28038d18edd14022af5726dbaf93e (patch)
treec1200c981efceb399de0c4380b6886215a4d50aa
parentc298750a0ec5f17f3ab4d3734d981ddfa2617aa8 (diff)
-unifyMore
-rw-r--r--doc/manual.tex2
-rw-r--r--src/elaborate.sig6
-rw-r--r--src/elaborate.sml14
-rw-r--r--src/main.mlton.sml3
-rw-r--r--tests/league.ur3
5 files changed, 20 insertions, 8 deletions
diff --git a/doc/manual.tex b/doc/manual.tex
index 9f3e44a8..ee4fdd0c 100644
--- a/doc/manual.tex
+++ b/doc/manual.tex
@@ -202,6 +202,8 @@ It is often worthwhile to run \cd{urweb} in this mode, because later phases of c
A related option is \cd{-dumpTypes}, which, as long as parsing succeeds, outputs to stdout a summary of the kinds of all identifiers declared with \cd{con} and the types of all identifiers declared with \cd{val} or \cd{val rec}. This information is dumped even if there are errors during type inference. Compiler error messages go to stderr, not stdout, so it is easy to distinguish the two kinds of output programmatically.
+It may be useful to combine another option \cd{-unifyMore} with \cd{-dumpTypes}. Ur/Web type inference proceeds in a series of stages, where the first is standard Hindley-Milner type inference as in ML, and the later phases add more complex aspects. By default, an error detected in one phase cuts off the execution of later phases. However, the later phases might still determine more values of unification variables. These value choices might be ``misguided,'' since earlier phases have not come up with reasonable types at a coarser detail level; but the unification decisions may still be useful for debugging and program understanding. So, if a run with \cd{-dumpTypes} leaves unification variables undetermined in positions where you would like to see best-effort guesses instead, consider \cd{-unifyMore}. Note that \cd{-unifyMore} has no effect when type inference succeeds fully, but it may lead to many more error messages when inference fails.
+
To output information relevant to CSS stylesheets (and not finish regular compilation), run
\begin{verbatim}
urweb -css P
diff --git a/src/elaborate.sig b/src/elaborate.sig
index 6d1583a4..cc83b213 100644
--- a/src/elaborate.sig
+++ b/src/elaborate.sig
@@ -1,4 +1,4 @@
-(* Copyright (c) 2008, Adam Chlipala
+(* Copyright (c) 2008, 2012, Adam Chlipala
* All rights reserved.
*
* Redistribution and use in source and binary forms, with or without
@@ -36,4 +36,8 @@ signature ELABORATE = sig
(* After elaboration (successful or failed), should I output a mapping from
* all identifiers to their kinds/types? *)
+ val unifyMore : bool ref
+ (* Run all phases of type inference, even if an error is detected by an
+ * early phase. *)
+
end
diff --git a/src/elaborate.sml b/src/elaborate.sml
index 1923390a..71f5196f 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -39,6 +39,7 @@
open ElabErr
val dumpTypes = ref false
+ val unifyMore = ref false
structure IS = IntBinarySet
structure IM = IntBinaryMap
@@ -4519,10 +4520,11 @@ fun elabFile basis topStr topSgn env file =
end
val checkConstraintErrors = ref (fn () => ())
+ fun stopHere () = not (!unifyMore) andalso ErrorMsg.anyErrors ()
in
oneSummaryRound ();
- if ErrorMsg.anyErrors () then
+ if stopHere () then
()
else
let
@@ -4625,7 +4627,7 @@ fun elabFile basis topStr topSgn env file =
mayDelay := false;
- if ErrorMsg.anyErrors () then
+ if stopHere () then
()
else
(app (fn (loc, env, k, s1, s2) =>
@@ -4641,7 +4643,7 @@ fun elabFile basis topStr topSgn env file =
(!delayedUnifs);
delayedUnifs := []);
- if ErrorMsg.anyErrors () then
+ if stopHere () then
()
else
if List.exists kunifsInDecl file then
@@ -4651,7 +4653,7 @@ fun elabFile basis topStr topSgn env file =
else
();
- if ErrorMsg.anyErrors () then
+ if stopHere () then
()
else
if List.exists cunifsInDecl file then
@@ -4661,7 +4663,7 @@ fun elabFile basis topStr topSgn env file =
else
();
- if ErrorMsg.anyErrors () then
+ if stopHere () then
()
else
app (fn all as (env, _, _, loc) =>
@@ -4670,7 +4672,7 @@ fun elabFile basis topStr topSgn env file =
| SOME p => expError env (Inexhaustive (loc, p)))
(!delayedExhaustives);
- if ErrorMsg.anyErrors () then
+ if stopHere () then
()
else
!checkConstraintErrors ();
diff --git a/src/main.mlton.sml b/src/main.mlton.sml
index 57927258..00cb40b0 100644
--- a/src/main.mlton.sml
+++ b/src/main.mlton.sml
@@ -85,6 +85,9 @@ fun doArgs args =
| "-dumpTypes" :: rest =>
(Elaborate.dumpTypes := true;
doArgs rest)
+ | "-unifyMore" :: rest =>
+ (Elaborate.unifyMore := true;
+ doArgs rest)
| "-dumpSource" :: rest =>
(Compiler.dumpSource := true;
doArgs rest)
diff --git a/tests/league.ur b/tests/league.ur
index 7edd5f42..5364c977 100644
--- a/tests/league.ur
+++ b/tests/league.ur
@@ -4,4 +4,5 @@ type league = string
table team : { Id : team,
League : league }
-val foo:int = queryL(SELECT * FROM team)
+val foo = queryL(SELECT * FROM team)
+val bar : int = "hi"