syntax1 3.7 KB

123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144
  1. Ticks for Basics
  2. max-open-constraints = 0
  3. pointers = 0
  4. pointers (reused) = 0
  5. max-open-metas = 1
  6. unequal terms = 2
  7. metas = 13
  8. equal terms = 23
  9. Ticks for Pr
  10. max-open-constraints = 0
  11. pointers = 0
  12. pointers (reused) = 0
  13. max-open-metas = 3
  14. unequal terms = 17
  15. metas = 88
  16. equal terms = 172
  17. Ticks for Nom
  18. pointers = 0
  19. pointers (reused) = 0
  20. max-open-constraints = 2
  21. max-open-metas = 4
  22. attempted-constraints = 8
  23. unequal terms = 75
  24. metas = 87
  25. equal terms = 216
  26. Ticks for Kind
  27. max-open-constraints = 0
  28. pointers = 0
  29. pointers (reused) = 0
  30. max-open-metas = 1
  31. metas = 10
  32. equal terms = 20
  33. Ticks for Cxt
  34. max-open-constraints = 0
  35. pointers = 0
  36. pointers (reused) = 0
  37. max-open-metas = 1
  38. unequal terms = 5
  39. metas = 59
  40. equal terms = 190
  41. Ticks for Loc
  42. max-open-constraints = 0
  43. pointers = 0
  44. pointers (reused) = 0
  45. max-open-metas = 6
  46. metas = 145
  47. unequal terms = 145
  48. equal terms = 335
  49. Ticks for Term
  50. pointers = 0
  51. pointers (reused) = 0
  52. max-open-constraints = 2
  53. attempted-constraints = 4
  54. max-open-metas = 10
  55. unequal terms = 158
  56. metas = 241
  57. equal terms = 615
  58. Ticks for Shift
  59. pointers = 0
  60. pointers (reused) = 0
  61. max-open-constraints = 2
  62. max-open-metas = 14
  63. attempted-constraints = 16
  64. metas = 230
  65. unequal terms = 412
  66. equal terms = 639
  67. Ticks for Eta
  68. pointers = 0
  69. pointers (reused) = 0
  70. max-open-constraints = 2
  71. attempted-constraints = 12
  72. max-open-metas = 18
  73. metas = 185
  74. unequal terms = 270
  75. equal terms = 487
  76. Ticks for Inst
  77. pointers = 0
  78. pointers (reused) = 0
  79. max-open-constraints = 2
  80. attempted-constraints = 9
  81. max-open-metas = 16
  82. metas = 276
  83. unequal terms = 534
  84. equal terms = 948
  85. Ticks for Subst
  86. pointers = 0
  87. pointers (reused) = 0
  88. max-open-constraints = 2
  89. attempted-constraints = 8
  90. max-open-metas = 13
  91. metas = 202
  92. unequal terms = 315
  93. equal terms = 576
  94. Ticks for Syntacticosmos
  95. max-open-constraints = 0
  96. pointers = 0
  97. pointers (reused) = 0
  98. max-open-metas = 1
  99. metas = 1
  100. equal terms = 21
  101. Ticks for UntypedLambda
  102. pointers = 0
  103. pointers (reused) = 0
  104. max-open-constraints = 2
  105. attempted-constraints = 20
  106. max-open-metas = 23
  107. metas = 101
  108. unequal terms = 124
  109. equal terms = 180
  110. agda -v0 -v profile:100 Syntacticosmos/UntypedLambda.agda --ignore-interfaces -iSyntacticosmos +RTS -K32M -slogs/.tmp (null)
  111. 1,729,921,352 bytes allocated in the heap
  112. 330,880,688 bytes copied during GC
  113. 13,587,564 bytes maximum residency (33 sample(s))
  114. 238,368 bytes maximum slop
  115. 34 MB total memory in use (0 MB lost due to fragmentation)
  116. Tot time (elapsed) Avg pause Max pause
  117. Gen 0 3273 colls, 0 par 0.94s 1.00s 0.0003s 0.0200s
  118. Gen 1 33 colls, 0 par 0.64s 0.71s 0.0216s 0.0660s
  119. INIT time 0.00s ( 0.00s elapsed)
  120. MUT time 3.87s ( 4.05s elapsed)
  121. GC time 1.59s ( 1.72s elapsed)
  122. EXIT time 0.00s ( 0.00s elapsed)
  123. Total time 5.46s ( 5.77s elapsed)
  124. %GC time 29.1% (29.7% elapsed)
  125. Alloc rate 446,915,138 bytes per MUT second
  126. Productivity 70.9% of total user, 67.1% of total elapsed
  127. ──────────────────────────────────────────────────────────────────
  128. Mach kernel version:
  129. Darwin Kernel Version 10.8.0: Tue Jun 7 16:33:36 PDT 2011; root:xnu-1504.15.3~1/RELEASE_I386
  130. Kernel configured for up to 2 processors.
  131. 2 processors are physically available.
  132. 2 processors are logically available.
  133. Processor type: i486 (Intel 80486)
  134. Processors active: 0 1
  135. Primary memory available: 2.00 gigabytes
  136. Default processor set: 112 tasks, 504 threads, 2 processors
  137. Load average: 1.14, Mach factor: 0.88