From cae32e92127664318d52b0cc8884a69a2892f6ba Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 18 Jun 2002 13:00:43 +0000 Subject: [PATCH] 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 | 28 +++++++++++++++++----------- 1 file changed, 17 insertions(+), 11 deletions(-) diff --git a/helm/gTopLevel/mquery.ml b/helm/gTopLevel/mquery.ml index 093f0228c..f31fccd07 100644 --- a/helm/gTopLevel/mquery.ml +++ b/helm/gTopLevel/mquery.ml @@ -99,6 +99,9 @@ and out_list = function | MQUnion (l1, l2) -> sep "(" ^ out_list l1 ^ key "union" ^ out_list l2 ^ sep ")" | MQIntersect (l1, l2) -> sep "(" ^ out_list l1 ^ key "intersect" ^ out_list l2 ^ sep ")" | MQLRVar v -> key "rvaroccur" ^ v + | MQLetIn (v, l1, l2) -> + key "let " ^ out_rvar v ^ " = " ^ out_list l1 ^ key " in " ^ out_list l2 + | MQLetRef v -> out_rvar v let out_query = function | MQList l -> out_list l @@ -269,18 +272,21 @@ let restrict_universe query = in compose_universe !universe in - MQSelect ( - "uri", query, - MQSubset ( - MQSelect ( - "uri2", - MQUsedBy (MQLRVar "uri", "pos"), - MQOr ( - MQIs (MQSSVar "pos", MQConclusion), - MQIs (MQSSVar "pos", MQMConclusion) + MQLetIn ( + "universe",universe, + MQSelect ( + "uri", query, + MQSubset ( + MQSelect ( + "uri2", + MQUsedBy (MQLRVar "uri", "pos"), + MQOr ( + MQIs (MQSSVar "pos", MQConclusion), + MQIs (MQSSVar "pos", MQMConclusion) + ) + ), + MQLetRef "universe" ) - ), - universe ) ) ;; -- 2.39.2