Changes from 2.1 (alpha84) to alpha84b Bug fixes ========== (1) A bug where upModule() generated the wrong meta-hooks for special operators of classes ACU_NumberOpSymbol and CUI_NumberOpSymbol. This also shows up with the "show all" command. Reported by Nathalie Sznajder and Paco. (2) A bug whether certain legal label names such as sort could not be parsed in label renamings. (3) The situation where two ad hoc overloaded operators have the same domain kinds but different ranges now causes a warning to be emitted as does the case where the arities differ but might look the same because of associativity: fmod FOO is sorts Foo Bar . op f : Foo -> Foo . op f : Foo -> Bar . endfm fmod BAR is sorts Foo Bar . op f : Foo Foo -> Foo [assoc] . op f : Foo Foo Foo -> Bar . endfm These cases are illegal but are handled correctly at the object level. They always break the metalevel because of ambiguity and this needs to be made clear in the manual. This inconsistancy was reported by Nathalie Sznajder and Olaf Owe. (4) There is now rudimentary checking of the consistancy for bubble hooks since users are expected write these themselves; Thanks to Fabricio Chalub for pointing out that the previous version crashes on (bad) examples from the manual. (5) A bug where an module with a missing identity could be imported, causing an internal error: fmod M is sort S . op __ : S S -> S [assoc id: ] . endfm fmod N is pr M . endfm Reported by Kazuhiro Ogata. Other changes ============== (1) Symmetric with set include FOO on/off . we now have set protect FOO on/off . and set extend FOO on/off . A module may only be auto-imported in one mode. Furthermore the prelude is changed so that BOOL is now auto-protected rather than auto-included. (2) Syntax for theories is supported. Currently this is mostly syntactic sugar except that the rules for importation that we agreed upon in Barcelona are now enforced by warnings and the module type of a summation is correctly calculated. Basically we have a lattice: th / \ fth mod \ / fmod where summation corresponds to join and a module may only import a module of less or equal type. Furthermore theories may only be imported via the including importation mode. Theories are reflected by constructors: fth_is_sorts_.____endfth and th_is_sorts_._____endth The are now extra subsorts: SModule FTheory STheory. Module is now used as the top sort rather than to represent system modules. This choice was made to avoid breaking stuff that expects Module to be the most general sort. The subsort relations are: subsorts FModule < SModule < Module . subsorts FTheory < STheory < Module . op [_] : Qid -> Module . is redefined so that it works with all kinds of modules without producing warnings. (3) The surface parser now supports overparsing - i.e. it deliberately parses more than the legal syntax in order to recover gracefully from common errors. Currently it recognizes rls/crls in fmods/fths, theories and modules terminated with the wrong keyword and the missing space before the period ending a statement. In order to make this possible there are minor restrictions on the legal syntax which should only affect pathological examples: < -> ~> are prohibited as sort names. Tokens ending in a period in the rhs of a eq/rl/mb or the condition of a ceq/crl/cmb cannot be followed by a keyword unless they are inside of parentheses; eg the following is not allowed: eq c = d. eq . It must be rewritten as eq c = (d. eq) . Changes from alpha84b to alpha84b.1 This version is a slightly patched version of Alpha84b to fix a critical bug in the AU sort calculation code reported by Jon Haugsand. A simplified version of his example that exposes the problem is fmod SORT-INT is pr INT . sorts Seq Pseq Tree . subsorts Int < Pseq < Seq . op ntree : -> Tree [ctor] . op tree : Tree Int Tree -> Tree [ctor] . op nil : -> Seq . op __ : Seq Seq -> Seq [assoc id: nil ctor] . op __ : Pseq Pseq -> Pseq [assoc id: nil ctor] . vars M N : Int . vars S : Seq . vars F G : Tree . op downto : Nat Nat -> Seq . eq downto(M, N) = if M <= N then downto(M + 1,N) M else nil fi . op itree : Tree Int -> Tree . eq itree(ntree,N) = tree(ntree,N,ntree) . eq itree(tree(F,M,G),N) = if M >= N then tree(itree(F,N),M,G) else tree(F,M,itree(G,N)) fi . op seqtotree : Seq -> Tree . eq seqtotree(N) = tree(ntree,N,ntree) . eq seqtotree(N S) = itree(seqtotree(S),N) . endfm red seqtotree(downto(1,6)) . Changes from alpha84b.1 to alpha84b.2 This release is a slightly patched version of Alpha84b.1 to fix a critical bug in the operator renaming reported by Paco: fmod FOO is sorts Bar Foo . subsorts Bar < Foo . op foo : Foo -> Foo . op foo : -> Foo . endfm fmod BAZ is inc FOO * (op foo : Bar -> Bar to bar). endfm show all . show modules .