search

nick8325 / quickspec

Equational laws for free
BSD 3-Clause "New" or "Revised" License
250 stars 24 forks source link

Background predicates don't appear as conditionals in laws #46

Open isovector opened 4 years ago

isovector commented 4 years ago

Consider the original sig, with _contains in the signature proper:

== Functions ==                                                                                                 
withReply :: Thread -> Thread -> Thread                                                                         
     True :: Bool                                                                                               

== Functions ==                                                                                                 
  comment :: Post -> Thread                                                                                     
     lock :: Thread -> Thread                                                                                   
  replyTo :: Post -> Thread -> Thread -> Thread                                                                 
_contains :: Post -> Thread -> Bool                                                                             

== Laws ==                                                                                                      
  1. lock (lock t) = lock t                                                                                     
  2. _contains p (comment p2) = _contains p2 (comment p)                                                        
  3. _contains p (comment p)                                                                                    
  4. _contains p (lock t) = _contains p t                                                                       
  5. withReply (lock t) t2 = lock t                                                                             
  6. _contains p (withReply t t) = _contains p t                                                                
  7. replyTo p t (comment p) = withReply (comment p) t                                                          
  8. replyTo p t (lock t2) = lock t2                                                                            
  9. _contains p t => _contains p (withReply t t2)                                                              
 10. _contains p (replyTo p2 t t2) = _contains p t2                                                             
 11. replyTo p (comment p2) (comment p2) = replyTo p (comment p) (comment p2)                                   
 12. _contains p t2 => replyTo p t (withReply t2 t) = withReply (replyTo p t t2) t                              
 13. _contains p (withReply t (lock t2)) = _contains p (withReply t t2)                                         
 14. _contains p3 t & _contains p2 t2 => _contains p (withReply t (comment p2)) = _contains p (withReply t t2)  
 15. _contains p t2 => _contains p (withReply t (comment p)) = _contains p (withReply t t2)                     
 16. _contains p t4 => replyTo p t (replyTo p2 t2 t3) = replyTo p2 t2 (replyTo p t t3)                          
 17. _contains p2 t5 & _contains p3 t2 => replyTo p (replyTo p2 t t2) t3 = replyTo p (replyTo p2 t4 t2) t3      
 18. _contains p2 t4 & _contains p4 t2 & _contains p3 t5 => replyTo p (replyTo p2 t t2) t3 = replyTo p (replyTo 
p3 t t2) t3                                                                                                     
 19. _contains p (withReply t (withReply t t2)) = _contains p (withReply t t2)                                  
 20. _contains p (withReply t (withReply t2 t)) = _contains p (withReply t t2)                                  
 21. _contains p (withReply t (withReply t2 t2)) = _contains p (withReply t t2)                                 
 22. _contains p (withReply (withReply t t2) t3) = _contains p (withReply t (withReply t3 t2))                  
 23. replyTo p t (withReply (comment p) t2) = withReply (withReply (comment p) t2) t                            
 24. replyTo p (lock (comment p2)) (comment p2) = replyTo p (lock (comment p)) (comment p2

but when it's moved to the background, we no longer see law 12 or similar laws with a _contains p t => precondition:

== Functions ==
withReply :: Thread -> Thread -> Thread
     True :: Bool
_contains :: Post -> Thread -> Bool

== Functions ==                    
comment :: Post -> Thread
   lock :: Thread -> Thread
replyTo :: Post -> Thread -> Thread -> Thread

== Laws ==
  1. lock (lock t) = lock t        
  2. _contains p (comment p2) = _contains p2 (comment p)
  3. _contains p (comment p)
  4. _contains p (lock t) = _contains p t
  5. withReply (lock t) t2 = lock t
  6. replyTo p t (comment p) = withReply (comment p) t
  7. replyTo p t (lock t2) = lock t2
  8. _contains p (replyTo p2 t t2) = _contains p t2
  9. replyTo p (comment p2) (comment p2) = replyTo p (comment p) (comment p2)
 10. _contains p (withReply t (lock t2)) = _contains p (withReply t t2)
 11. replyTo p t (withReply (comment p) t2) = withReply (withReply (comment p) t2) t
 12. replyTo p (lock (comment p2)) (comment p2) = replyTo p (lock (comment p)) (comment p2)