NOTES

			    LSL Notes, 26 May 1994
			    ======================


Work to be done on LSL Checker
------------------------------

finish making term grammar correspond to LP's
  currently implemented grammar is (close to) Doc/lsl3_1.y
  desired grammar is (close to) Doc/lsl3_2.y
    this grammar removes ambiguity in parsing a:s[t]
    it contains several minor ambiguities that can be resolved by parser
      ambiguity 1: asserts \forall x: S [T] 0 = 1
        preferred parse: asserts \forall x: S[T] (0 = 1)
        alternate parse: asserts \forall x: S ([T]0 = 1)
        user must supply parentheses to get parse 2
      ambiguity 2: includes 0: -> N [__]: N -> S
        yacc complains about a shift-reduce conflict when it sees [
        the parser already resolves this conflict by a longer lookahead
  need to change parser, update lsl3_1.y, lsl.lex, lslinit.cfg
        
implement assertion "well founded R"

insert parentheses when printing unqualified a => b => c

follow implication chains
  strengthen T_Theorems.lp
    Test/Results/semImplies1_Theorems.lp should assert a, b, c
  generate lemmas for T_Checks.lp
  see semantics.h for notes
  special handling for generated-by
    omit when generated sort, domain sort of generator collapse to same sort
    necessitated by translation of generated-by into first-order logic
    suppose T |= "S generated by 0: -> S, f: S1 -> S"
      this means T |= [P(0) & forall x:S1 P(f(x))] => forall x:S P(x)
    suppose r renames S1 to S
    then we cannot conclude r(T) |= "S generated by 0: -> S, f: S -> S"
      this means 
        r(T) |= [P(0) & forall x:S (P(x) => P(f(x)))] => forall x:S P(x)
      which is a stronger statement (because its hypothesis is weaker)
  do we need special handling for partitioned-by?

check for textually discharged proof obligations
  assumption of trait discharged by explicit assumption or inclusion
  implication of trait discharged by explicit assumption or inclusion
    Test/Results/semImplies2_Checks.lp check for "implies semImplies1a"
  implication of formula discharged by explicit asssertion
    Test/Results/semImplies2_Checks.lp for "implies equations b"
  assumption, implication of DecimalLiterals
    see Test/semLit*.lsl

detect as duplicates individual assumptions that match individual assertions

change bound variable in traitRef that clashes with constant in parent trait

add command-line options
  -v (verbose) to display comments in lp translations
  -? to generate implication checks
  -? to generate assumption checks
  -? to generate conversion checks

fix proof obligations for "converts" (in lsl2lp.c)
  fix convert_op to generate new names for [, other bracketing notations
  Test/Results/semCvts_Checks.lp should contain "prove a' = a"
  remove duplicate conversion checks

fix output: qed sometimes appears in column 1, sometimes in column 3

recheck implications



OTHER POSSIBLE ENHANCEMENTS
---------------------------

generate dummy props for shorthands
   use to label following equations in output
   use to optimize duplicate detection
      check dummy prop for duplication
      skip following props (without checking) if a duplicate

classify operator lists as similar if they have the same elements in any order
   this will catch some more duplicate genBys and partBys

generate dependencies for makefile (command-line option)
   trait depends on all included/assumed traits
   trait A depends on implied trait B if B does not also imply A
      if B also implies A, it suffices to recheck B when B changes
         (because A will be checked as part of the checks on B)
      this prevents cycles in dependencies
   makefile entries
      A_Axioms.lp: A.lsl
	 lsl -lp A
   printed dependencies must involve file names, not just trait names
      use SPEC_PATH?

print nicer declarations in .lp files
   collect variables with same sorts
   collect operators with same signatures
   alphabetize lists

proving converts
   don't redeclare \neq operators for sorts in domains of converted ops

generate .lp files for traits that passed checks (when other traits failed)
prettyprint .lp files

fix bug wrt ambiguous output for LP (or remove -tr option)
  sample trait
    translate: trait
      introduces
        a: B -> A
        B: C -> A
      asserts A generated by a
  sample translation file
    b for a:B->A
  lsl needs to qualify generated-by, but does not

supply registry hints (low priority)
  literals
  shorthand operators

implement new LSL/LP strategy for rechecking proofs (superceded by new scheme)
  lsl2lp generates T_Checks.lp, which looks like
    execute T_Axioms
    prove ...
      qed
    prove ...
      qed
    % converts <, >
    clear				% This is a change from what's done now
    execute T_Converts1
    prove ...
      qed
    prove ...
      qed
    % converts <=, >=
    clear
    execute T_Converts2
    prove ...
      qed
    prove ...
      qed
  user rearranges, enlarges this file to obtain T_User_Checks.lp
  separate program compares T_Checks.lp with T_User_Checks.lp
    each conjecture in T_Checks.lp must have proof in T_User_Checks.lp
      this proof must occur at top-level (i.e., not nested in another proof)
      must also occur following the appropriate "execute" command
    warnings if T_User_Checks contains assert, declare, thaw, other executes
  rechecking after changes to traits
    copy *.lsl, *_User_Checks.lp to clean directory
    rerun lsl2lp to regenerate T_Axioms, T_Converts, T_Checks
    check that *_User_Checks.lp still succeed
    check *_User_Checks.lp against new *_Checks.lp
  to work out
    better identification than Converts1, Converts2, ...
    making theorems of implied traits available after implication is checked


LSL Problems
------------

search path problems
  suppose: trait A references trait B, which references trait C
           writer of B presumed that C.lsl is in some directory 
           checker of A has another trait named C earlier on search path
  how should checker find the "right" copy of C?
  how can it provide better error messages if it uses the "wrong" copy?
    e.g., if B provides "bad" parameters for the C found by the checker
    the checker could identify which C.lsl caused the error
    at present, it only identifies which B.lsl caused the error

init file problems
  how should checker find the "right" copy of lslinit.lsi?
    e.g., when checking a referenced trait in another directory
  using the "wrong" init file can
    (1) make it impossible to parse a trait (e.g., because of token class
        definitions for openSyms, closeSyms)
    (2) introduce subtle inconsistencies (e.g., by making two tokens be
        synonyms, when the user intended them to have different meanings)


ENHANCMENTS TO EFFICIENCY
-------------------------

assign hash key to signatures, use to optimize equality check
deallocate temporary storage


SCAFFOLDING
-----------

redo .h files
fix mutual references of symtable, renaming operations
lack of gcc support for gdb on DECstations
lack of gcc support for gprof on DECstations
C abstractions
   coding for iterators
   type checking for lists (e.g., OpList, operatorNodeList should differ)


DONE
----

detected and fixed previously unnoticed bugs
   bug: unparenthesized x - (y - z) on output
   bug: "converts a exempting a" -> "exempted term lacks converted operator"
	occurs when checking conversions of nullary operators
   bug: "implies (T1, T2)" was not allowed
implemented further context-sensitive checks
   operators in implied trait are declared in parent trait
changed command-line interface to allow -lp, multiple files
changed grammar to allow an optional trailing eqSepSym in an eqSeq
fixed segmentation fault in unparse_parameters
  caused when record component was extracted from null n->attr
added diagnostics to print sorts of sides when equation does not sort check
improved error message for undeclared operator
set_log -> set log						fixed Aug. 14
checker now finds files with absolute path names		fixed Sept. 16
allow A$T tuple of ...						fixed Oct. 28
added immediate consequences of subsidiary traits to axioms	fixed Jan. 7
"lsl -lp" translates "a \neq b" into "not(a = b)"		fixed March 8
  needed until LP recognizes \neq
  also removed \neq from list of declared operators
  also fixed printing to retain parens in "(p /\ q) = r"
fixed message "% Renaming for -: N -> N"			fixed April 9
  corrected to "% Renaming for -__: N -> N"
  problem was that checker had flag to suppress __ for LP declarations
  solution was to temporarily set and reset flag
changed output for LP to use = instead of ==
added quantifiers						fixed Nov 10
fixed bug wrt ambiguous output for LP				fixed Nov 11
  qual: trait
    introduces f: A -> B
    asserts \forall x:A x == x
    implies \forall x:B x == x
  lsl did not qualify output in qual_Theorems.lp
  because it did not combine variable tables
changed composite sort notation	to A[B, C]			fixed 23 May 94
  abstract.h
    redefined rep for sortNode
    redefined interface to makeSortNode
  abstract.c
    changed to conform to new abstract.h
  checking.c
    fixed invocations makeSortNode
    fixed tagSortNode
  parse.h
    changed grammar for sort
  parse.c
    changed parsing for sort
    changed lookahead for sort symbol
      old: assert S$E generated by {}, insert
           assert S generated by {}, insert
      new: assert sort S[E] generated by {}, insert
	   assert sort S generated by {}, insert
	   assert S generated by {}, insert
  reduce.c
    changed to correspond to parse.c
  renaming.c
    changed renaming_mapSort to allow 
    renamings of subsorts by arbitrary sorts
    renaming of sort identifier by arbitrary identifier
    cached sort renamings for efficiency
  scanline.c
    changed initialization to correspond to new token.h
  symtable.c
    changed symtable_sortExists
    routine returns TRUE if sort exists or is the identifier of some sort
  token.h
    removed COMPOSESYM
    added sortTOKEN
    defined LBRACK, RBRACK (changed code for opensyms, closesyms)
  unparse.c
    changed unparse_sort
segmentation fault caused by bad memory reference		fixed 23 Jan 95
  added +1 in "if (stackSize + 1 >= stackAlloc)" in recheckTraitRegs
incorrect -lp output for AC, Commutative traits			fixed 27 Jan 98
  assertion made about equality operator, not the desired operator
  problem seems to have been caused by new version of traits
  fixed printOpTheory in propSet.c to look for non-equality operator

CAUSES OF BUGS
--------------

bug in checking whether two finite functions were identical
   wanted  for (x, y) in f.pairs do if y ~= g(x) then return false
   mistake for (x, y) in f.pairs do if x ~= g(y) then return false
wrote EQUALSTOKEN instead of EQTOKEN
incremented count outside iterator rather than inside
cut "f(i, i+1)", forgot to change to "f(i, j)" when pasting in nested loop
misuse of "default" case in "switch" statement
   should be used to catch errors, not supposedly common cases
misuse of C strings
   code tried to insert string terminator in string argument
   this failed (on Sparc, but not DECstation) when argument was a literal
   fixed by making a copy of the string
mistakes about first, last on path in tree meaning bottom, top or vice versa


Notes on renamed generated-by's and partitioned-by's
----------------------------------------------------

foo(B, b1, b2): trait
  introduces
    a1, a2:      -> A
    b1, b2:      -> B
    f     : A    -> B
    g     : A, B -> Bool
  asserts
    A generated by a1, a2
    B generated by b1, b2
    \forall a: A
      f(a1) == b1
      f(a2) == b2
      g(a, b1) == true
      g(a, b2) == false
  implies
    B generated by f
    B generated by f, b1	% no harm in adding b1
    B partitioned by g

Now consider foo(A, a1, a2):

renamedFoo(A, a1, a2): trait
  introduces
    a1, a2:      -> A
    f     : A    -> A
    g     : A, A -> Bool
  asserts
    A generated by a1, a2
    \forall a: A
      f(a1) == a1
      f(a2) == a2
      g(a, a1) == true
      g(a, a2) == false
  DOES NOT IMPLY
    A generated by f		% no basis generator
    A generated by f, a1	% f does not reach a2
    A partitioned by g		% because g(a1, a) = g(a2, a)



Changes to LSL (Version 2.3) Report
===================================


Section 2.2: Simple Traits

No simpleId may occur more than once with the same sort in any quantifier.
                                     *******************


Section 2.3: Externals

The variable mapping associated with a traitRef is defined as follows:

     If id:->S is in the operator list of the enclosing trait and id:S is in 
     the variable list of an eqPart of one of the referenced traits, then 
     replace all occurrences of that variable in the referenced traits by a
     new variable id1:S such that id1:->S does not occur in the operator list
     of the enclosing trait.

The normalization of a traitRef is the image, under its name and variable
mapping, of the union of the normalizations of the referenced traits.


Section 2.4: Consequences

<<Define normalization?  For use as lemmas in checking?>>