]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 80569b9) | patch
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
tree590de7a191533bf7fa4926d41f2d585b6a1baf3dtree | snapshot
parent80569b93b7cc484b40d7cba33f3d8255db66fe65commit | diff
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 diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.