================================================================================
 TALT                                                                           
================================================================================


Twelf.Timers.reset()
Twelf.make "/Users/seanmcl/save/projects/twelf/test/lf/sources-chk.cfg"
Twelf.Timers.show()

- Parsing       : Real =   0.946, Run =   0.423 (  0.397 usr,  0.034 gc)
Reconstruction: Real =   1.310, Run =   0.744 (  0.709 usr,  0.078 gc)
Abstraction   : Real =   2.834, Run =   1.259 (  1.119 usr,  0.447 gc)
Checking      : Real =   0.000, Run =   0.000 (  0.000 usr,  0.000 gc)
Modes         : Real =   0.306, Run =   0.082 (  0.070 usr,  0.000 gc)
Subordination : Real =   0.686, Run =   0.292 (  0.270 usr,  0.037 gc)
Termination   : Real =   0.000, Run =   0.000 (  0.000 usr,  0.000 gc)
Printing      : Real =   2.361, Run =   1.408 (  1.300 usr,  0.344 gc)
Compiling     : Real =   0.169, Run =   0.024 (  0.016 usr,  0.000 gc)
Solving       : Real =   0.318, Run =   0.158 (  0.148 usr,  0.033 gc)
Coverage      : Real =   0.000, Run =   0.000 (  0.000 usr,  0.000 gc)
Worlds        : Real =   0.000, Run =   0.000 (  0.000 usr,  0.000 gc)
ProofRecon    : Real =   0.000, Run =   0.000 (  0.000 usr,  0.000 gc)
Filling       : Real =   0.000, Run =   0.000 (  0.000 usr,  0.000 gc)
Filling Tabled: Real =   0.000, Run =   0.000 (  0.000 usr,  0.000 gc)
Splitting     : Real =   0.000, Run =   0.000 (  0.000 usr,  0.000 gc)
Recursion     : Real =   0.000, Run =   0.000 (  0.000 usr,  0.000 gc)
Inference     : Real =   0.000, Run =   0.000 (  0.000 usr,  0.000 gc)
Delphin       : Real =   0.000, Run =   0.000 (  0.000 usr,  0.000 gc)
Total         : Real =   8.930, Run =   4.389 (  4.029 usr,  0.972 gc)
Remember that the success continuation counts into Solving!
val it = () : unit
- 

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

val center = Timing.newCenter "checker"
Timing.time center Translate.translate_signature ()
Timing.toString center

- val it = "checker: Real =  13.711, Run =   1.032 (  0.938 usr,  0.159 gc)\n"
  : string



================================================================================
 Type soundness of SML                                                          
================================================================================

- Twelf.Timers.show()
;
= Parsing       : Real =  13.302, Run =   6.228 (  5.696 usr,  1.292 gc)
Reconstruction: Real =  12.031, Run =   9.486 (  9.136 usr,  1.088 gc)
Abstraction   : Real =   6.090, Run =   4.534 (  4.271 usr,  0.864 gc)
Checking      : Real =   0.000, Run =   0.000 (  0.000 usr,  0.000 gc)
Modes         : Real =   1.713, Run =   0.928 (  0.849 usr,  0.025 gc)
Subordination : Real =  15.091, Run =  10.218 (  9.921 usr,  0.461 gc)
Termination   : Real =   1.770, Run =   1.067 (  1.017 usr,  0.049 gc)
Printing      : Real =  15.144, Run =  13.851 ( 13.050 usr,  2.726 gc)
Compiling     : Real =   0.556, Run =   0.132 (  0.091 usr,  0.000 gc)
Solving       : Real =   0.333, Run =   0.342 (  0.322 usr,  0.086 gc)
Coverage      : Real =  37.931, Run =  25.238 ( 24.173 usr,  2.885 gc)
Worlds        : Real =   9.770, Run =   5.142 (  5.007 usr,  0.183 gc)
ProofRecon    : Real =   0.000, Run =   0.000 (  0.000 usr,  0.000 gc)
Filling       : Real =   0.000, Run =   0.000 (  0.000 usr,  0.000 gc)
Filling Tabled: Real =   0.000, Run =   0.000 (  0.000 usr,  0.000 gc)
Splitting     : Real =   0.000, Run =   0.000 (  0.000 usr,  0.000 gc)
Recursion     : Real =   0.000, Run =   0.000 (  0.000 usr,  0.000 gc)
Inference     : Real =   0.000, Run =   0.000 (  0.000 usr,  0.000 gc)
Delphin       : Real =   0.000, Run =   0.000 (  0.000 usr,  0.000 gc)
Total         : Real = 113.732, Run =  77.166 ( 73.532 usr,  9.660 gc)
Remember that the success continuation counts into Solving!
val it = () : unit
- 

val center = Timing.newCenter "checker"
Timing.time center Translate.translate_signature ()
Timing.toString center

val it = "checker: Real =  21.487, Run =  29.699 ( 26.485 usr, 10.897 gc)\n"
  : string
- 

Twelf.doubleCheck := true;
Twelf.Timers.reset()
Twelf.Print.depth := SOME 0
Twelf.Print.length := SOME 0
Twelf.make "../../../test/sml-sound/sources.cfg";

- Parsing       : Real =   8.750, Run =   2.871 (  2.703 usr,  0.261 gc)
Reconstruction: Real =  18.085, Run =   7.865 (  7.579 usr,  0.982 gc)
Abstraction   : Real =   6.597, Run =   3.231 (  3.110 usr,  0.500 gc)
Checking      : Real =  11.145, Run =   4.221 (  4.057 usr,  0.491 gc)
Modes         : Real =   2.353, Run =   0.654 (  0.622 usr,  0.038 gc)
Subordination : Real =  25.816, Run =  11.122 ( 10.779 usr,  0.707 gc)
Termination   : Real =   2.130, Run =   1.014 (  0.975 usr,  0.026 gc)
Printing      : Real =   1.298, Run =   0.422 (  0.385 usr,  0.035 gc)
Compiling     : Real =   0.568, Run =   0.078 (  0.054 usr,  0.008 gc)
Solving       : Real =   0.000, Run =   0.000 (  0.000 usr,  0.000 gc)
Coverage      : Real =  56.313, Run =  38.461 ( 37.159 usr,  3.491 gc)
Worlds        : Real =  10.577, Run =   5.514 (  5.374 usr,  0.209 gc)
ProofRecon    : Real =   0.000, Run =   0.000 (  0.000 usr,  0.000 gc)
Filling       : Real =   0.000, Run =   0.000 (  0.000 usr,  0.000 gc)
Filling Tabled: Real =   0.000, Run =   0.000 (  0.000 usr,  0.000 gc)
Splitting     : Real =   0.000, Run =   0.000 (  0.000 usr,  0.000 gc)
Recursion     : Real =   0.000, Run =   0.000 (  0.000 usr,  0.000 gc)
Inference     : Real =   0.000, Run =   0.000 (  0.000 usr,  0.000 gc)
Delphin       : Real =   0.000, Run =   0.000 (  0.000 usr,  0.000 gc)
Total         : Real = 143.633, Run =  75.452 ( 72.797 usr,  6.747 gc)
Remember that the success continuation counts into Solving!
val it = () : unit
- 

val it = "checker: Real =  23.248, Run =  32.431 ( 28.856 usr, 12.077 gc)\n"
  : string