• Andrei Paskevich's avatar
    Term: do not store t_vars in terms · 7abeba05
    Andrei Paskevich authored
    we still keep bv_vars in the binders, so calculating the set
    of free variables only has to descend to the topmost binders.
    The difference on an example from BWare is quite striking:
    
    /usr/bin/time why3-replayer : with t_vars
    
    505.14user 15.58system 8:40.45elapsed 100%CPU (0avgtext+0avgdata 3140336maxresident)k
    
    /usr/bin/time why3-replayer : without t_vars
    
    242.96user 12.04system 4:16.31elapsed 99%CPU (0avgtext+0avgdata 2007184maxresident)k
    
    Not only we take 2/3 of memory, but we also gain in speed (less work
    for the GC, most probably).
    
    This patch should be tested on big WhyML examples,
    since src/whyml/mlw_*.ml are big users of t_vars.
    
    Thanks to Guillaume for the suggestion.
    7abeba05
tptp_typing.ml 25.1 KB