changeset 1738:1a35e75b6967

Catch duplicate top-level module names; fix dropping of constraints during incremental elaboration; document treatment of record types as type class instance types
author Adam Chlipala <adam@chlipala.net>
date Thu, 03 May 2012 09:56:41 -0400
parents 78d7cc9c9b18
children c414850f206f
files doc/manual.tex src/compiler.sml src/elaborate.sml
diffstat 3 files changed, 15 insertions(+), 3 deletions(-) [+]
line wrap: on
line diff
--- a/doc/manual.tex	Wed May 02 08:56:19 2012 -0400
+++ b/doc/manual.tex	Thu May 03 09:56:41 2012 -0400
@@ -579,7 +579,7 @@
 
 A signature item or declaration $\mt{class} \; x = \lambda y \Rightarrow c$ may be abbreviated $\mt{class} \; x \; y = c$.
 
-Handling of implicit and explicit constructor arguments may be tweaked with some prefixes to variable references.  An expression $@x$ is a version of $x$ where all type class instance and disjointness arguments have been made explicit.  (For the purposes of this paragraph, the type family $\mt{Top.folder}$ is a type class, though it isn't marked as one by the usual means.)  An expression $@@x$ achieves the same effect, additionally making explicit all implicit constructor arguments.  The default is that implicit arguments are inserted automatically after any reference to a variable, or after any application of a variable to one or more arguments.  For such an expression, implicit wildcard arguments are added for the longest prefix of the expression's type consisting only of implicit polymorphism, type class instances, and disjointness obligations.  The same syntax works for variables projected out of modules and for capitalized variables (datatype constructors).
+Handling of implicit and explicit constructor arguments may be tweaked with some prefixes to variable references.  An expression $@x$ is a version of $x$ where all type class instance and disjointness arguments have been made explicit.  (For the purposes of this paragraph, the type family $\mt{Top.folder}$ is a type class, though it isn't marked as one by the usual means; and any record type is considered to be a type class instance type when every field's type is a type class instance type.)  An expression $@@x$ achieves the same effect, additionally making explicit all implicit constructor arguments.  The default is that implicit arguments are inserted automatically after any reference to a variable, or after any application of a variable to one or more arguments.  For such an expression, implicit wildcard arguments are added for the longest prefix of the expression's type consisting only of implicit polymorphism, type class instances, and disjointness obligations.  The same syntax works for variables projected out of modules and for capitalized variables (datatype constructors).
 
 At the expression level, an analogue is available of the composite $\lambda$ form for constructors.  We define the language of binders as $b ::= p \mid [x] \mid [x \; ? \; \kappa] \mid X \mid [c \sim c]$.  A lone variable $[x]$ stands for an implicit constructor variable of unspecified kind.  The standard value-level function binder is recovered as the type-annotated pattern form $x : \tau$.  It is a compile-time error to include a pattern $p$ that does not match every value of the appropriate type.
 
--- a/src/compiler.sml	Wed May 02 08:56:19 2012 -0400
+++ b/src/compiler.sml	Thu May 03 09:56:41 2012 -0400
@@ -943,8 +943,11 @@
                                      first = ErrorMsg.dummyPos,
                                      last = ErrorMsg.dummyPos}
 
+                          val urt = OS.FileSys.modTime ur
+                          val urst = (OS.FileSys.modTime urs) handle _ => urt
+
                           val ds = #func parseUr ur
-                          val d = (Source.DStr (mname, sgnO, if !Elaborate.incremental then SOME (OS.FileSys.modTime ur) else NONE,
+                          val d = (Source.DStr (mname, sgnO, if !Elaborate.incremental then SOME (if Time.> (urt, urst) then urt else urst) else NONE,
                                                 (Source.StrConst ds, loc)), loc)
 
                           val fname = OS.Path.mkCanonical fname
@@ -1078,6 +1081,15 @@
                                    NONE => ds
                                  | SOME v => ds @ [(Source.DOnError v, loc)]
                   in
+                      ignore (List.foldl (fn (d, used) =>
+                                             case #1 d of
+                                                 Source.DStr (x, _, _, _) =>
+                                                 if SS.member (used, x) then
+                                                     (ErrorMsg.errorAt (#2 d) ("Duplicate top-level module name " ^ x);
+                                                      used)
+                                                 else
+                                                     SS.add (used, x)
+                                               | _ => used) SS.empty ds);
                       ds
                   end handle Empty => ds
               end,
--- a/src/elaborate.sml	Wed May 02 08:56:19 2012 -0400
+++ b/src/elaborate.sml	Thu May 03 09:56:41 2012 -0400
@@ -3934,7 +3934,7 @@
                          val env' = E.declBinds env d
                          val denv' = dopenConstraints (loc, env', denv) {str = x, strs = []}
                      in
-                         ([d], (env', denv', []))
+                         ([d], (env', denv', gs))
                      end
                    | NONE =>
                      let