/[mojave]/metaprl/BUGS
ViewVC logotype

Diff of /metaprl/BUGS

Parent Directory Parent Directory | Revision Log Revision Log | View Patch Patch

revision 2923 by jyh, Thu Feb 24 01:42:53 2000 UTC revision 2924 by nogin, Fri Mar 17 09:35:28 2000 UTC
# Line 91  Line 91 
91  test{x.test{y.'C['x; 'y]}} <--> 'C[1; 2]  test{x.test{y.'C['x; 'y]}} <--> 'C[1; 2]
92  rewrites <<test{x.test{x.'x}}>> to 1 instead of 2.  rewrites <<test{x.test{x.'x}}>> to 1 instead of 2.
93    
 <<<<<<< BUGS  
 3.5) (Confirmed on 1999.10.16 by nogin)  
 Rewriter should support "strict" matching - in a redex, when a bound variable  
 is not explicity mentioned as an argument of a SO variable, the matching term should  
 not have free occurences of the correspondent variable.  
 <<<<<<< BUGS  
 =======  
   
 The "strict" mode would also eliminate the bug no 4.3  
 >>>>>>> 1.25  
   
 <<<<<<< BUGS  
 The "strict" mode would also eliminate the problem rhw bug mentioned below in the REFINER  
 section.  
 =======  
 (1999.10.16, nogin) Currently the "strict" mode is implemented in rewriter,  
 but not yet enambled in the refiner.  
 >>>>>>> 1.25  
   
 <<<<<<< BUGS  
 *) Rewriter does not prevent capturing. It should, at least in the "strict" mode.  
   
 *) Currently rewriter does not enforce building contractum to be against the same redex  
 =======  
 =======  
 >>>>>>> 1.26  
94  3.6) Rewriter does not prevent capturing. It should, at least in the "strict" mode.  3.6) Rewriter does not prevent capturing. It should, at least in the "strict" mode.
95    
96  3.7) Currently rewriter does not enforce building contractum to be against the same redex  3.7) Currently rewriter does not enforce building contractum to be against the same redex
 >>>>>>> 1.25  
97  the contractum was compiled against. Hopefully we never do this wrong, but we still  the contractum was compiled against. Hopefully we never do this wrong, but we still
98  should enforce it.  should enforce it.
99    
# Line 170  Line 143 
143    
144    --jyh: the tactic _is_ defined, but not (yet) added to Mptop toploop.    --jyh: the tactic _is_ defined, but not (yet) added to Mptop toploop.
145    
 *) Some times parser requires too many brackets.  
   
 <<<<<<< BUGS  
 *) Parsing or printing bug that can be seen using ASCII files:  
    sometimes string arguments in params gets unquoted too many times.  
    Reproduce this bug by loading an old ASCII file, then saving it  
    and seeing that some parameters have been unquoted.  
 =======  
146  5.3) Some times parser requires too many brackets.  5.3) Some times parser requires too many brackets.
 >>>>>>> 1.25  
147    
 <<<<<<< BUGS  
 *) Toploop_resource seems to be added into .p4 file even if  
    base_theory is not included.  
 =======  
148  5.4) Parsing or printing bug that can be seen using ASCII files:  5.4) Parsing or printing bug that can be seen using ASCII files:
149       sometimes string arguments in params gets unquoted too many times.       sometimes string arguments in params gets unquoted too many times.
150       Reproduce this bug by loading an old ASCII file, then saving it       Reproduce this bug by loading an old ASCII file, then saving it
151       and seeing that some parameters have been unquoted.       and seeing that some parameters have been unquoted.
152  >>>>>>> 1.25  
153    5.5) Toploop_resource seems to be added into .p4 file even if
154       base_theory is not included.
155    
156  RULES & REWRITES  RULES & REWRITES
157    

Legend:
Removed from v.2923  
changed lines
  Added in v.2924

  ViewVC Help
Powered by ViewVC 1.1.26