]> matita.cs.unibo.it Git - helm.git/commit
New query implementation using LetIn.
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 18 Jun 2002 13:00:43 +0000 (13:00 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 18 Jun 2002 13:00:43 +0000 (13:00 +0000)
commitcae32e92127664318d52b0cc8884a69a2892f6ba
tree590de7a191533bf7fa4926d41f2d585b6a1baf3d
parent80569b93b7cc484b40d7cba33f3d8255db66fe65
New query implementation using LetIn.
Some benchmarks:

Query: 2*n <= 2*m

Results:

  No-LetIn     LetIn  Output
 1: 23s   >>>>  3s    9uri        uri/s: 3
 0: 276s  >>>> 14s   48uri        uri/s: 3.42

Open BUGs:
 the implementation of the LetIn scope is surely not correct. The whole
 semantics is wrong in case of repeated names.
helm/gTopLevel/mquery.ml