<commit_before>TODO
====

* predicate-aliases 
* record invariants
* parse predicate signatures for tuples 
* Blogging 
* benchmarks: Data.List (foldr)
* self-invariants        (tests/todo/maybe4.hs)

* benchmarks: Data.List (foldr) -- needs sets
* benchmarks: Data.Bytestring
* benchmarks: stackset-core
* benchmarks: Data.Text

* benchmarks: mcbrides stack machine
* remove `toType` and  generalize `typeSort` to work for all RefTypables

Predicate Aliases
=================

Then clean up the spec blowup in containers/Data/Map/Base.hs ?

    {-@ maybeGe(lo, v)     = ((isJustS(lo)) => (v >= fromJustS(lo))) @-}
    {-@ maybeLe(hi, v)     = ((isJustS(lo)) => (v <= fromJustS(hi))) @-}
    {-@ inRange(lo, hi, v) = maybeGe(lo, v) && maybeLe(hi, v)        @-}

How about this instead?

    {-@ refinement maybeGe lo v    = ((isJustS lo) => (v >= (fromJustS lo))) @-}
    {-@ refinement maybeLe hi v    = ((isJustS lo) => (v <= (fromJustS hi))) @-}
    {-@ refinement inRange lo hi v = (maybeGe lo v) && (maybeLe hi v)        @-}

Instead of the grisly

    inRange(lo, hi, v) = {v:k | (((isJustS(lo)) => (v >= fromJustS(lo))) && (((isJustS(hi)) => (v <= fromJustS(hi)))))} v @-}

Benchmarks
==========

                    time(O|N|C)    TOTAL(O|N)   solve (O|N)      refines       iterfreq
Map.hs          :    54/50/32/10    21/15/8.7      14/8/4.3    9100/4900/2700    16/28/7
ListSort.hs     :   */7.5/5.5/2    */2.5/1.8     */1.5/1.0      */1100/600       */9/7
GhcListSort.hs  :    23/22/17/5    7.3/7.8/5   4.5/5.0/2.7    3700/4400/1900   10/23/6
LambdaEval.hs   :    36/32/25/12    17/12/10     11.7/6.0/5    8500/3100/2400   12/5/5
Base.hs         :        26mi/2m


Self-Invariants
===============

Hack binders to allow things like this:

    invariant z:: { v : Maybe {isJust(v) && (v = fromJust(z))}  } 
    invariant z:: { v : List {v:a | (v in listElts(z))}         } 



Currently hacked by "copying variables", 

see tests/pos/maybe3.hs [hack which works]
    tests/pos/maybe4.hs [deal with devil which doesn't work]



Tuple Refinements (DONE: by Niki)
=================================

- Add/Parse predicate signatures for tuples<p>     

    (x1, x2, x3)<p1, p2, p3>

- pos/deptup.hs (type signature: for constructor wrapper)


    data [a]<p :: a -> a -> Bool> 
      = []
      | (:) (h :: a) (t :: [a<p h>]<p>)  
    
    data (a1, a2) 
      < p1 :: a1 -> Bool
      , p2 :: a1 -> a2 -> Bool
      > 
      = (,) (x1 :: a1<p1>) (x2 :: a2<p2 x1>)
    
    data (a1, a2, a3) 
      < p1 :: a1 -> Bool
      , p2 :: a1 -> a2 -> Bool
      , p3 :: a1 -> a2 -> a3 -> Bool
      > <commit_msg>flerp<commit_after>TODO
====

* self-invariants        (tests/todo/maybe4.hs) <----------------------- HEREHEREHERE

* predicate-aliases 
* record invariants
* parse predicate signatures for tuples 
* Blogging 
* benchmarks: Data.List (foldr)

* benchmarks: Data.List (foldr) 
* benchmarks: Data.Bytestring
* benchmarks: stackset-core
* benchmarks: Data.Text

* benchmarks: mcbrides stack machine
* remove `toType` and  generalize `typeSort` to work for all RefTypables

Self-Invariants
===============

get tests/pos/maybe4.hs to work     <----------------------- HEREHEREHEREHERE


Hack binders to allow things like this:

    invariant z:: { v : Maybe {isJust(v) && (v = fromJust(z))}  } 
    invariant z:: { v : List {v:a | (v in listElts(z))}         } 

Currently hacked by "copying variables", 

see tests/pos/maybe3.hs [hack which works]
    tests/pos/maybe4.hs [deal with devil which doesnt work]


Predicate Aliases
=================

Write a test for this.

Then clean up the spec blowup in containers/Data/Map/Base.hs ?

    {-@ pred maybeGe lo v    = (isJustS lo) => (v >= (fromJustS lo)) @-}
    {-@ pred maybeLe hi v    = (isJustS lo) => (v <= (fromJustS hi)) @-}
    {-@ pred inRange lo hi v = (maybeGe lo v) && (maybeLe hi v)      @-}

How about this instead?
        
    {-@ pred maybeGe lo v    = ((isJustS lo) => (v >= (fromJustS lo))) @-}
    {-@ pred maybeLe hi v    = ((isJustS lo) => (v <= (fromJustS hi))) @-}
    {-@ pred inRange lo hi v = (maybeGe lo v) && (maybeLe hi v)        @-}

Instead of the grisly

    inRange(lo, hi, v) = {v:k | (((isJustS(lo)) => (v >= fromJustS(lo))) && (((isJustS(hi)) => (v <= fromJustS(hi)))))} v @-}

Benchmarks
==========

                        time(O|N|C)    TOTAL(O|N)   solve (O|N)      refines       iterfreq
    Map.hs          :    54/50/32/10    21/15/8.7      14/8/4.3    9100/4900/2700    16/28/7
    ListSort.hs     :   */7.5/5.5/2    */2.5/1.8     */1.5/1.0      */1100/600       */9/7
    GhcListSort.hs  :    23/22/17/5    7.3/7.8/5   4.5/5.0/2.7    3700/4400/1900   10/23/6
    LambdaEval.hs   :    36/32/25/12    17/12/10     11.7/6.0/5    8500/3100/2400   12/5/5
    Base.hs         :        26mi/2m




Tuple Refinements (DONE: by Niki)
=================================

- Add/Parse predicate signatures for tuples<p>     

    (x1, x2, x3)<p1, p2, p3>

- pos/deptup.hs (type signature: for constructor wrapper)


    data [a]<p :: a -> a -> Bool> 
      = []
      | (:) (h :: a) (t :: [a<p h>]<p>)  
    
    data (a1, a2) 
      < p1 :: a1 -> Bool
      , p2 :: a1 -> a2 -> Bool
      > 
      = (,) (x1 :: a1<p1>) (x2 :: a2<p2 x1>)
    
    data (a1, a2, a3) 
      < p1 :: a1 -> Bool
      , p2 :: a1 -> a2 -> Bool
      , p3 :: a1 -> a2 -> a3 -> Bool
      > 
{'fraction_non_alphanumeric': 0.2039179104477612, 'fraction_numerical': 0.0625, 'mean_word_length': 2.068689181453921, 'pattern_counts': {'":': 0, '<': 29, '<?xml version=': 0, '>': 61, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '3758129', 'n_tokens_mistral': 2292, 'n_tokens_neox': 2077, 'n_words': 521}