<commit_before>TODO
====

* parse predicate signatures for tuples 
* predicate-aliases 
* Blogging 
* benchmarks: Data.List (foldr)
* predicate-aliases 
* self-invariants        (tests/todo/maybe4.hs)
* fixpoint profile (how much performance hit from -nosimple?)
* Set Theory
* benchmarks: Data.List (foldr) -- needs sets
* benchmarks: Data.Bytestring
* benchmarks: stackset-core
* benchmarks: Data.Text
* benchmarks: mcbrides stack machine
* alpha-renaming of predicate params is VERY SHAKY. see tests/pos/deptupW.hs
* remove `toType` and  generalize `typeSort` to work for all RefTypables


Set Theory
==========

HEREWEARE

(tests/pos/meas9.hs)

1. fixpoint/theories.ml [DONE]
   see fixpoint/tests/sets.fq

2. embed

 Spec   :  ++ EmbedTyCon a = Embed a Fixpoint.Tycon
   
 Parser : parse in the above from specs

 Bare   : EmbedTyCon String -> EmbedTyCon GHC.TyCon

 typeSort : Map GHC.TyCon Fixpoint.Tycon -> Type -> Sort

 Fixpoint: 

    intTC  = "int"
    boolTC = "bool"

 include/Prelude.spec
 
    embed Int       as int
    embed Integer   as int
    embed Bool      as bool
    
 include/Data/Set.spec
    
    embed Set       as Set_Set

------------------------------------------------------------



    measure emp :: Set a 
    measure mem :: a     -> Set a -> Bool<commit_msg>next: meas9.hs<commit_after>TODO
====

* parse predicate signatures for tuples 
* predicate-aliases 
* Blogging 
* benchmarks: Data.List (foldr)
* predicate-aliases 
* self-invariants        (tests/todo/maybe4.hs)
* fixpoint profile (how much performance hit from -nosimple?)
* Set Theory
* benchmarks: Data.List (foldr) -- needs sets
* benchmarks: Data.Bytestring
* benchmarks: stackset-core
* benchmarks: Data.Text
* benchmarks: mcbrides stack machine
* alpha-renaming of predicate params is VERY SHAKY. see tests/pos/deptupW.hs
* remove `toType` and  generalize `typeSort` to work for all RefTypables


Set Theory
==========


(tests/pos/meas9.hs)

1. fixpoint/theories.ml [DONE]
   see fixpoint/tests/sets.fq

2. embed

 Spec   :  ++ EmbedTyCon a = Embed a Fixpoint.Tycon
   
 Parser : parse in the above from specs

 Bare   : EmbedTyCon String -> EmbedTyCon GHC.TyCon

 typeSort : Map GHC.TyCon Fixpoint.Tycon -> Type -> Sort

 Fixpoint: 

    intTC  = "int"
    boolTC = "bool"

 include/Prelude.spec
 
    embed Int       as int
    embed Integer   as int
    embed Bool      as bool
    
 include/Data/Set.spec
    
    embed Set       as Set_Set


3. get tests/pos/meas9.hs to pass!      <---------------- HEREHEREHEREHERE

------------------------------------------------------------



    measure emp :: Set a 
    measure mem :: a     -> Set a -> Bool
{'fraction_non_alphanumeric': 0.14511278195488722, 'fraction_numerical': 0.004135338345864661, 'mean_word_length': 2.342964824120603, 'pattern_counts': {'":': 0, '<': 4, '<?xml version=': 0, '>': 13, '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': '7667147', 'n_tokens_mistral': 902, 'n_tokens_neox': 838, 'n_words': 257}