2006-10-?? Small bug fix in pfesetup. (It could create a symbolic link to the libraries in the wrong place.) Some internal changes to make the tools compile with GHC 6.6 2006-05-23 Made the QuickCheck certificate server compatible with the May 2006 release of Hugs. 2006-03-01 Added anonymous abstractions (\ X1 ... Xn . P) to the P-logic predicate syntax. 2005-10-10 Bug fix: dependency analysis ignored expression type-signatures. This could cause needed definitions to be omitted from slices created by the QuickCheck certificate server. Changed the pattern match simplifier to produce fewer redundant abstractions and case branches for newtype constructors and other single contructor data types. (This affects the translations for Plover and Alfa.) 2005-09-02 pfe and pfebrowser now remember the plogic/noplogic option between runs. The syntax of the file hi/options has changed, so delete it after upgrading pfe. The command 'pfe options' displays remembered options, which now are - prelude/noprelude: implicitly import Prelude in every module. - plogic/noplogic: recognize plogic syntax - nocpp/cpp[=cmd]: if/how to invoke the C preprocessor. 2005-08-01 The 'pfe stratego' and 'pfe strategoslice' commands now apply the dictionary translation to resolve overloading. (The old behavior can be obtained by using the flag -untyped.) Plover should now in principle be able to prove assertions involving overloaded functions. Parser bug fix: expressions containing operators that have special meaning in Plogic weren't parsed correctly (e.g, "a = b /\ c" caused a parse error.) 2005-07-14 A new version of Plover is included Bug fix: the translation of Plogic disjunctions to Plover was wrong (P \/ Q was translated to Q \/ Q). 2005-07-06 Plogic: added the operator e1=/=e2 as syntactic sugar for -/(e1===e2). Prettier printing of module interface information with the 'pfe iface' command and in the interface window in pfebrowser. Added checks that the superclass relation is not cyclic (Haskell 98 report, section 4.3.1). 2005-05-20 A new version of Plover is included. There is now support for functional dependencies in the type checker in PFE. (Functional dependencies have been recognized by the parser since way back, but until now they were ignored by the type checker.) This still a bit preliminary: it has not been tested thoroughly and there is one known omission compared to how GHC & Hugs handles functional dependencies. 2005-05-05 - Plogic changes: - Added syntactic sugar for predicate definitions, allowing property P x = ... as an alternative to property P = {| x | ... |} To avoid a syntactic ambiguity, constructors now need to be enclosed in braces, e.g., you need to write x==={Nothing} instead of x===Nothing. - The logical operators (/\, \/, ==>, <==>, -/) have been generalized to work with arbitrary arity predicates, not just propositions and unary predicates. - The Alfa and QuickCheck certificate servers have been updated to support this. - Plover should continue to work, but might need to be updated to do the right thing with operators lifted to higher arity predicates. - Gfp, Lfp, (->) and lifted data constructors could be generalized in the same way, but this has not been implemented yet... - pfebrowser usability: source locations in scoping error messages are now clickable. Additionally, undefined/ambiguous identifiers are underlined in red. - Scoping bug fix: while data constructors should be allowed as predicates in Plogic formulas, Plogic predicates should not be allowed as constructors in normal Haskell code. 2005-04-28 pfebrowser usability: - Source locations in type error messages are now clickable links to the corresponding locations in the source code. (But note that PFE is not better than other Haskell implementation at providing accurate locations for type errors...) - Added status indicators to the right of the menu bar. For three levels of checking (Syntax, Scoping and Typing), they indicate whether the status is unknown (not checked), in progress, in error or good. - Type errors no longer cause the Type Info setting in the View menu to be turned off. - The error message window is cleared when the error has been resolved. 2005-04-18 A new version of Plover is included. Parser bug fix: type signatures of the formed "() => ..." were parsed in the wrong way and gave rise to obscure error messages from the type checker. Pretty printer bug fix: added missing back quotes around constructors used as infix operators in patterns (x `C` y was printed as x C y). 2005-03-29 Bug fix: fixed a dependency info cache inconcistency that caused problems when using 'pfe server' to speed up certificate validation. HTML renderer: improved treatment of literate style code. Fixed an old layout problem with indented code after comment blocks. 2005-03-17 - Eliminated the superfluous dependency on the readline library (but the Mac OS X executables still refer to the readline library for some reason). 2005-03-03 pfebrowser: - Certificate icons are now automatically displayed next to assertions. Certificate annotation can still be used for manual placement of certificate icons. For certificates that aren't associated with an assertion (currenly only TestCase certificates) you still need a certificate annotion to get an icon. - Added a window displaying pending certificate commands. 2005-03-02 A new version of Plover is included. The translation to Plover now desugars the labelled field syntax, allowing Plover to make sense of such expressions and patterns. 'cert new -all ' now adds new certitificates of the given type to all assertions, irrespective of whether they already have other certiticates. This also applies to the "Add certificate to all assertions" command in pfebrowser. pfebrowser: - When clicking on an assertion name, the link to create a new certificate is available even if the assertion already has other certiticates. - Better feedback for queued certificate server commands (e.g. when using the "Validate All" command). Bug fix: 'cert new ...' (for creating a single certificate) stopped working when 'cert new -all ...' was added. 2005-02-25 pfebrowser: - Literate style source code is now presented in its original form. (Before, literate comments were preserved by converting them to nested comments before lexical analysis. Now they are handled separately.) - Added a menu command to validate all certificates. - Added a menu command to add certificates of a given type to all assertions that lack certificates. - Certificate manipulation now works under Mac OS X. - Assertion names in the Evidence window are now hyperlinked to their definitions. - A message "Type checking..." is shown during type checking to make it easier to see when it is done. (The cursor still also changes to an hourglass or something similar.) Command line: - Added the command 'cert new -all {}' to add certificates of a given type to all assertions that lack certificates. Bug fix: I_say_so certificates stopped working after the command line syntax changes in the 2005-02-08 release. 2005-02-18 Added support for overlapping instances. It should now be similar to what Hugs provides. Improved support for the use of type synonyms in class and instance declarations. (Haskell 98 does not allow type synonyms in these places.) Bug fix: types/classes/instances declared in the same module were not taken into account when resolving top level ambiguities, resulting in obscure error messages. 2005-02-08 pfebrowser usability: The history buttons now remember both ends of hyperlinks. (They do not remember scrolling.) When a module is loaded, pfebrowser now reports the number of scoping errors (undefined/ambiguous identifiers). The user can click on the message to get the list of scoping errors. Scoping errors do not prevent continued browsing. pfe command line usability: Supressed misleading warnings about missing modules in the output from pfesetup. Added option -quiet to pfe commands 'new', 'add' and 'remove'. Combined some similar commands into one command with options. The command line parsing as been redone (with my new grammar combinators), so the usage message and syntax error messages might be a bit different. Addded checks that Plogic predicate definitions aren't recursive. (You have to use the operators Lfp & Gfp to define recursive predicates.) Added checks that type synonyms aren't recursive (Haskell 98 report, section 4.2.2). 2005-01-24 In literate style source files, lines starting with a ! are now treated as code lines, providing an alternative to the {-P: ... -} for hiding assertions from Haskell implementations that don't know about Plogic. Plogic syntax: "All x,y. ..." is now accepted as syntactic sugar for "All x . All y . ..." (and analogously for the existential quantifier). Bug fix: adjacent code and comment lines in literate style source files no longer cause pfebrowser (or pfe server) to quit. (They were reported by calls to Prelude.error.) Bug fix (sort of): added a workaround for a Haskell 98 Report bug that prevents the insertion of an implicit right brace before an explicit right brace when that is needed to avoid a syntax error. Example: the following was rejected by pfe, but is now accepted: property Com = {| c, c' | {do c ; c'} === {do c' ; c} |} 2005-01-18 Added version information: - From the command line 'pfe version' displays a version number. - pfebrowser displays a version number at startup, in the title bar and as part of the welcome message in the info display. - The certicicate server descriptions output by the 'cert types' command now includes a version number. - When a new certificate is created, the version number of the certificate server is included in the certificate attributes. Evidence management (work in progress): - Alfa certificate can now have other assertions as assumptions. ".." (meaning all definitions) is still a compulsory assumption. - A certificate server for cut elimination is provided. A new version of Plover is included. Translation of type declarations to Plover. 2004-12-21 Work in progress on support for the Hierachical Libraries in addition to the Haskell 98 libraries previously supplied with PFE. (The Hierachical Libraries were borrowed from Hugs.) To test this, run pfesetup with the flag +h (or hierarchical) to setup a project using the hierarchical libraries. (Note: PFE can parse all of the hierarchical modules, but some modules require type system extensions not (yet) supported in PFE.) Added a new transformation pass to deal with field labels (Haskell 98 report, section 3.15). This means that - field labels are now fully supported in the Plover and Alfa translators - type checking of field updates is improved: an update can now change the type of the record being updated. The 'pfe stratego' command now invents names for unnamed assertions so that they can be translated instead of being ignored. This makes no difference for 'pfe strategoslice' command, which is what the Plover certificate server uses. 2004-12-06 Work in progress: support for overlapping instances. If this breaks any plain Haskell 98 code, let me know. Hugs compatibility: reintroduced support for Hugs' syntax for declaration of primitives. "primitive" is a reserved keyword in this version of PFE. Added support for n+k patterns. (There is currently a parser bug because of this: definitions of the form "(a+b) x = ..." are rejected.) Efficiency: more efficient representation of the instance database speeds up the typechecking of the Prelude by 12%. removed some repeated computations in the module system code. eliminated a temporary space leak in the type checker, making it use significantly less memory, but run slightly slower. Added a source location to the error message generated for type errors in unnamed assertions. The translation to Stratego has been updated to support predicates applied to Haskell terms (in addition to predicate formulas). The new AST is incompatible with the old Plover, but a new version of Plover is not available yet. 2004-11-11 pfebrowser usability: type error messages are now displayed in an auxiliary window instead of a modal popup window, allowing the user to continue to browse while the error message is displayed. Bug fix: defining occurences of identifiers can never be ambiguous. Pfe did the wrong thing with identifiers in type signatures and fixity declarations. (See section 5.5.2 of the Haskell 98 report.) pfe usability: pfe unused & pfe prune now checks that the set of root modules is non-empty, to avoid treating all modules as unused. 2004-10-29 The command 'pfe chase', and hence pfesetup, now support the GHC/Hugs/Nhc convention for locating files for modules with hierarchical names. (A module called A.B.C is assumed to be in a file called A/B/C.hs or A/B/C.lhs) (TODO: add the hierarchical libraries and change pfesetup to automatically search them.) pfe command line syntax: to support projects containing more than one Main module, the syntax "Main{-filename.hs-}" is now recoginized when module names and qualified names are specified on the command line. pfebrowser: certificate icons in the source code and in the evidence window are now automatically updated when the status of a certificate changes. When validating a certificate, if there is an error computing the dependency info after a successful validation, the error message is now recorded rather than being silently ignored. Bug fix: the parser reported errors for patterns like x@R{...} in contexts where patterns have to be parsed as expressions (e.g. in the do-notation) Bug fix: the standard library functions List.maximumBy and List.minimumBy had the wrong types. 2004-07-15 Allow predicates as arguments to other predicates in the P-Logic assertion syntax. (This makes it consistent with the predicate syntax. TODO: allow quantified predicate variables?) pfebrowser usability: more streamlined certificate manipulation (less clicking required, fewer window opening and closing) The command 'pfe slice' now include all instance declarations in the output, allowing a usable (but coarser) slice to be obtained without the need for type checking. The command 'pfe qcslide' also uses this kind of slice, preventing the QuickCheck certificate server from failing when the translation of a P-Logic assertion introduces dependencies on user-defined instances. Added the commands 'pfe typeof' and 'pfe kindof' to retrieve the type or kind of a given identifier. The QuickCheck certificate server now consults the environment variable HUGS for the path of hugs. 2004-04-10 Added a text editor popup window to pfebrowser, allowing you to make quick changes to a module and reload it. This is a modal popup, so the main browser window is blocked while you edit. Disabled the use of Unicode output based on the LANG environment variable. You now have to ask for it explicitly with the +utf8 flag. (To avoid confusing certificate validation scripts and pfebrowser...) Disabled the use of escape codes to highlight output on stderr, since it can confuse (and look ugly in) pfebrowser. 2004-04-08 Added a simple TestCase certificate server. 2004-04-06 Added the command "cert setattr " to set certificate attributes from the command line. Added the boolean attribute SimplePatterns to the Alfa certificate server. This switch enables a simpler pattern match transformation that results in more compact code, but some Haskell patterns are not supported, e.g. numeric literals. 2004-04-02 Recompiled everything with GHC 6.2.1. pfe: Improved the command "pfe uses": in case a name refers to entities in different name spaces (typically both a data constructor and a type constructor), you can now add a keyword to restrict output to uses of one selected entity. For example pfe uses con SrcLoc.SrcLoc finds uses of the data constructor SrcLoc, but not the type of the same name. Changed the pretty printer for expressions to print fewer parenthesis and adjusted the translation to QuickCheck to add some extra explicit parentheses. This shouldn't make any difference, but let me know if the QuickCheck certificate server suddenly reports type/syntax errors for things that were OK before. 2004-01-26 pfe: added some experimental code metrics commands that display totals, averages, medians, top 10, bottom 10 and histograms for the measured variable: - sizemetrics: number of lines of source text per module (includes comments and blank lines) - locmetrics: number of lines of code per module (excludes comments and blank lines) - importmetrics: number of imports per module - exportmetrics: number of exports (importers) per module - classmetrics: number of instances per class pfebrowser: added a "View diagnostic output" link in the certificate info window. pfe: added the commands dirgraph and dotdirgraph to display source directory dependency graphs. 2003-11-14 Bug fix: mentioning data constructors in an import hiding clause caused false "not in scope" errors. (This bug was introduced on 2003-05-27 when improving the error messages for ambiguous names.) Work in progress: changes to support projects containing more than one Main module. It mostly works, but some things might be broken at the moment because of this. (Note: do 'pfe clean' to remove old incompatible cached data) 2003-11-07 pfebrowser: some small certificate validation popup window usability improvements The Plover certificate server now uses a slicing translation of Haskell to the Stratego AST. I've also made some changes to the abstract syntax so some things might be broken until the corresponding changes have been made in Plover. 2003-10-13 Pfebrowser: added a quick certificate status check so that the status indicated by the certificate icons is a conservative approximation of the true status. In the Cert menu, there is a new command Revalidate, that does a slower more thorough check to see which certificates are still valid. A newer version of Plover is included. 2003-09-26 Added a trial version of "pfe server". To use it, set up a project in the usual way (e.g., with pfesetup) then start a server for the project in the background: pfe server & When the server is running, the pfe command just acts as a proxy, passing commands to the server and printing results. Since cert calls pfe a number of times during certificate validation, this should speed up the validation process considerably. (pfebrowser is not yet modified to make use of the server, but will continue to work as before.) A newer version of Plover (that Dick announced on Sept 16) is included. The Alfa translator is now included in the main pfe command, making the separate command apfe obsolete. Lexer grammar: corrected the definition of varsym. Lexer generator: reduced the number of case branches required in the generated functions, by capturing as many cases as possible in the default branch. (This roughly halves the size of code for the Haskell lexer.) 2003-09-12 Added the command "pfe help" that produces the usage message. On errors, brief messages are shown instead of the long usage message. Added "pfe interactive", which reads pfe commands interactively and caches data internally between commands. (I am planning to make use of something like this to speed up certificate validation.) Hierarchical module names are now parsed correctly, but pfesetup and 'pfe chase' have not yet been improved to do import chasing in the same way as other Haskell implementations. Prettier printing of the type String (it is no longer printed as [Char] or [Prelude.Char]). Fixed a lexer bug: A... is now parsed in accordance with the Haskell Report. This was done by reimplementing the regular expression compiler from scratch and adding support for the difference operator, denoted r1 in the Haskell Report. No other Haskell implementation gets this right, AFAIK. 2003-09-04 Added "cert validate -all" to (re)validate all certificates. (TODO: make this a lot faster.) Added "cert recreate" to generate scripts of "cert new" commands to recreate all certificates. Certificate attributes other than the name, type, conclusion and hypotheses are currently ignored. Work in progress on support for hierarchical module names might affect some programs, e.g., A.B.C is no longer the same as A.B . C. 2003-08-12 Added a demo version of Plover, Dick's new Plogic Verifier. The translation to Alfa is now good enough to translate the standard Prelude and libraries. Made some small changes in Alfa, so Alfa version 2003-08-09 or later is needed. Loading the translated Prelude into Alfa takes some time and requires a lot of memory. For the time being, the Plogic fixed point operators Lfp & Gfp are restricted to unary predicates (like the other connectives). 2003-07-29 Added some more missing parentheses in the Stratego translation. P-Logic syntax: Made the ==> connective right associative. Fixed some bugs in the Haskell-to-Alfa translation. Also changed the format of the output, so a new version of Alfa is needed to parse it. Fixed some other minor bugs. 2003-06-27 Added some missing parentheses in the Stratego translation. 2003-06-26 Added the command 'pfe stratego', which does a preliminary translation of into Dick's Stratego representation of Haskell code. Added the (useless) certificate server Mono (for proof by monotonicity). Extended the syntax to allow existentially quantified data types (with GHC compatible syntax, see section 7.4.13 in the GHC User's Guide). TODO: add skolemization & escape checks in the type checker. TODO: add support *qualified* existential types in the type checker. 2003-06-06 pfebrowser: the shape of the mouse pointer now changes when it moves over a hyperlink. pfebrowser: added links in the Evidence window to create new certicates for assertions that don't have any. Bug fix: with nested local bindings, an identifier was associated with the outermost binding of the same identifier, rather than the innermost one. (This bug was probably introduced on 2003-01-15, but went unnoticed until now...) 2003-05-30 Usability: pfebrowser: instead of just popping up an error message and refusing to do anything when there is a problem parsing or reading a source file, pfebrowser instead continues, displaying (if possible) the raw source text of the selected module. Note that pfebrowser displays the module you asked for, which is not necessarily the module containing the error. Usability: improved error messages for ambiguous identifiers. (Before, they were reported as "not in scope"). Usability: pfe now complains when unknown module names are mentioned on the command line. (Before, they were silently ignored.) Bug fix: when computing slices, dependency information is computed only for the modules reachable from the root of the slice (instead of for all modules in the project). This means that a type error in an irrelevant module no longer prevents a QuickCheck certificate from being validated. Bug fix: property/assertion names in import/export specifications weren't linked to their definitions in pfebrowser and the HTML renderer. 2003-05-22 QuickCheck server: added support for tuples and logical connectives lifted to unary predicates. pfebrowser: you can now edit certificate attributes: click on a certificate icon to open the certificate info window. In addition to the "Validate" and "Remove" links, there is now an "Edit" link. (Attributes are specified in the /server.attr files.) Supported attributes: I say so: Conclusion, Comment QuickCheck: Conclusion, Comment, maxTest, maxFail, verbose Alfa: Conclusion, Comment, file/proof, proof pfebrowser: you can now click on the module name in an import declaration to jump to that module. pfebrowser and the HTML renderer: the special identifiers "qualified", "as" and "hiding" are now highlighted as keywords when they are used with their special meaning in import declarations. 2003-05-05 P-logic syntax: Added support for logical connectives lifted to unary predicates. You can for example now write property Finite = Lfp X . [] \/ Univ:X For backwards compatibility, the logical connectives have lower precedence than the ::: operator, so the parentheses can not be omitted from the following example: All x . x:::(Even \/ Odd) pfebrowser: the menu command "File/Reload Module" now makes pfebrowser update its internal representation of the module dependency graph, so it can be used instead of restarting pfebrowser after adding new imports to a module. (Adding new files to a project, e.g. with "pfe add", still requires restarting pfebrowser.) 2003-04-25 pfe type checker: finally added support for derived instances for mutually recursive data types. Fixed a related bug causing derived instances to be computed in the wrong order. pfebrowser usability: - the Import/Imported By menus now use the left mouse button, like the other menus. - the Back/Forward buttons now have popup menus showing the modules you can reach. Haskell parser bug fixes (by Iavor): - the parser didn't allow superfluous semicolons between declarations - the parser didn't allow infix constructors to be defined in prefix form, e.g. "data T a = (:+:) a a" was rejected. Bug fix: pfesetup didn't work if the prelude or noprelude option was given. 2003-04-14 Recompiled pfebrowser with a newer version of the fudget library to fix a problem with the border width of menus with certain window managers (KDE, X11 under Mac OS X). The QuickCheck certificate server has been modified to make more of more of the original QuickCheck library. This puts some restrictions on quantifiers in assertions, but also allows us to add support for custom test data generators... 2003-03-28 P-logic syntax: - Added support for tuple predicates: (P,Q) is true for pairs (x,y) where x:::P and y:::Q. The notation (,) P Q is also supported. Added support for Alfa certificates. However, the Haskell-to-Alfa translator is not quite in good enough shape to be useful on arbitrary Haskell code yet. Validation of Alfa certificates requires a recent version of Alfa (>=2003-03-26). Added the command 'pfe clean', which removes various files pfe caches in the hi/ subdirectory. It can be useful e.g. after upgrading pfe. 2003-02-28 P-logic syntax: - Quantifiers are no longer restricted to the outside of an assertion. - Lfp and Gfp now have lower precedence than other predicate operators. Pfebrowser: added some certificate management functionality: - Clicking on a certificate opens a new "Certificate Info" window, which displays detailed information, including reliable status information (whether it is new, valid, invalid, needs revalidation). - The new "Evidence" window lists all named assertions and certificates. There are also links that open the detailed "Certificate Info" window. - A button to (re)validate a certificate appears in the "Certificate Info" window when appropriate. There is also a button to remove the certificate. - The new "Cert" menu contains a command for creating new certificates. A button to create a new certificate also appears when clicking on an assertion that lacks a certificate. - ... Pfebrowser: various GUI changes: - A menu bar has been added. The File menu contains the Reload, which has the keyboard shortcut R. - To get information about an identifier, you have to click on it, it is no longer enough to just mouse over it. The mouse buttons have the following functions: Button 1: jump to the definition of an identifier, show detailed information about a certificate. Button 2: display information about a particular occurrence of an identifier Button 3: highlight all occurrences of an identifier - ... 2003-02-06 Bug fix: The "cert todo" list included assertions that had already been certified. Bug fix: the QuickCheck translation omitted type signatures from translated definitions, leading to unexpected type ambiguities when validating QuickCheck certificates. "cert validate" for I_say_so certificates now displays the sequent being certified. "cert validate" for QuickCheck certificates now translates the required parts of all relevant modules, allowing assertions to refer to predicates (including lifted constructors) defined in other modules. (This hasn't been tested much yet.) The new command "pfe slice M.x" extracts the slice of a program needed to define M.x. The new command "pfe qcslice M.x" also applies the QuickCheck translation to the extracted slice. The generated modules are placed in a subdirectory called "slice". Identifiers in import and export specifications are now tagged, so that pfebrowser and the HTML converter can display info and hyperlink them. (TODO: one identifier can sometimes denote two entities...) The type checker now handles "deriving Ix". pfebrowser now uses syntax highlighting when displaying inferred types. There is also a new auxiliary window Pretty, which displays a pretty printed version of the current module. The layout will be OK even if a proportional font is used. (To support this, a new abstraction layer has been added to the pretty printing combinators. Underneath this layer, there is a new, simple back-end based on the graphics/layout support in the fudget library.) 2003-01-21 Names of assertions and predicates can now be mentioned in export and import specifications. (Put them in {-P: ... -} to hide them from Hugs/GHC...) cert ls now adds a "?" in the Status column if the certificate might be out of date. The only way to be sure is to run "cert validate". pfebrowser shows when certificates were last marked (in)valid and uses different icons for certificates with valid/invalid/unknown status. Added the command 'pfe dotgraph', that outputs the module dependency graph in "dot" format, allowing it to be visualized with tools from the graphviz package, freely available from www.graphviz.org. (Code for this was contributed by Claus Reinke.) Example usage: pfe dotgraph | dotty - Also added 'cert dotgraph' and 'pfe dotdeps'... The QuickCheck certificate server now only translates the part of the module needed for the assertion to be checked, eliminating problems caused by other assertions that give rise to ambiguous overloadings when translated to QuickCheck. Dependency tracking in the I_say_so server (and the QuickCheck server) is now based on dependencies computed after type checking, and thus includes dependencies on instances. The dependency analysis has also become coarser, so some more irrelevant stuff may appear in the list of things that an assertion depends on. Also, since type checking is now involved, validating certificates of these types is often slower. Added support for overloaded predicates and assertions (through the dictionary translation). 2002-12-17 A first version of the QuickCheck certificate server is included. (It has various limitations. Talk to Iavor for details.) Assertion syntax fix: "e ::: P {x}" can now be written "e :: P x" (i.e., you can skip the braces around variables). Type checker bug fix: \x->(x::Int) was assigned the type a->Int rather than Int->Int. The problem occurred when matching explicit type signatures against inferred types containing non-generic type variables. The output of "cert ls" now has a Status column, which shows the result of the last "cert validate" command. (For the time being, cert ls continues to show Valid, even if code affecting the assertion has been changed after the certificate was validated. The only way to be sure that the certificate is still valid is to rerun the "cert validate" command.) 2002-12-12 Reenabled certificate icons in pfebrowser. (The were commented out for some reason.) Some efficiency improvements. Type checking the Prelude and the modules it depends on is 36% faster. Generating HTML for pfe is 46% faster. Improved kind information. Type schemes now contain the kinds of the quantified variables. The type checker also keeps track of "ambiguous" type variables (e.g. the type of the list in the expression "length []"). New windows in pfebrowser, to display additional module info, e.g. modules interfaces. (This is work in progress.) 2002-11-27 The commands p0pfe and p0pfesetup have been removed. Instead, pfe, pfebrowser and pfesetup accept the flags "plogic" and "noplogic" to turn on/off the P-logic extension. The default is on. Introduced a special form of comments: {-P: ... -}. These allow you to hide assertions and predicate definitions from Haskell implementations, like GHC and Hugs, that don't know about the P-logic extension. PFE parses the contents of such comments as if the "{-P:" and "-}" delimiters were blank space. Typical usage: const x y = x filter p xs = ... {-P: assert All xs . {filter (const True) xs}===xs assert All xs . {filter (const False) xs}:::[] -} Added the command "cert" providing preliminary support for evidence management. One certificate type is supported: "I say so". pfebrowser now displays icons for certificates. pfebrowser does not yet know how to distinguish valid from invalid certificates. pfebrowser and the HTML converter now knows the difference between field labels and class methods, so it can say e.g. that "return is a method of the class Monad" instead of "return is a field/method of Monad". pfebrowser can now display the types of all bound variables, not just variables introduced in declarations. Also, pfebrowser displays both its general type scheme and the particular instance an identifier is used at. (TODO: make the names of free type variables agree with the names used in the type schemes where they are quantified...) The type checker now generates code for derived instances. During context reduction, superclasses are assumed to be accessible via special superclass projection functions, e.g., super1_Ord to get the Eq a dictionary from a Ord a dictionary. The type checker now also adds definitions of these projections to instance declarations. Some internal changes to the type checker (to support better kind checking and other things). 2002-06-21 pfebrowser accepts the flag "noplogic", so that you can browse plain Haskell files (where "assert" and "property" are used as identifiers) again. Added the command "iface", to display the interface of a module, i.e., the kind of all exported types and classes, and the types of all exported values. (TODO: distinguish between methods, field names and ordinary values in the output.) Added the command "pragmas" that extract {-#pragmas#-} from modules. Added the command "certscan" to p0pfe. It extracts named assertions and creates the directories where certificates for the assertions are to be stored. (TODO: complement this with functionality to create and manipulate certificates, and to present icons for them in pfebrowser.) Added back/forward buttons to pfebrowser. Improved the dictionary translation by making use of substitution in expressions. 2002-06-10 Generalized the types of Lfp and Gfp from one-place predicates to arbitrary relations Prettier printing of types with special syntax (functions, tuples and lists), e.g., [(a,[b])] instead of [] ((,) a ([] b)) pfebrowser has switched to the base + P logic syntax. pfebrowser displays a tree view of modules and files, instead of just an alphabetical list of modules. Changed the color of special characters (parentheses, brackets, etc) in pfebrowser Support for the +utf8 option (to use Unicode characters when displaying types) in pfebrowser. 2002-06-07 Addition of implication and equivalence operators (==> and <==>) to the assertion syntax Generalization of the predicate comprehension syntax to {| p_1, p_2, ..., p_n | |} where p_i are patterns. Addition of the command 'pfe types' 2002-06-05 More efficient pfebrowser, in particular the type checking feature is now usable. Customizable colors in pfebrowser 2002-05-14 First announced (internal) release of the PFE tools with P logic support