]> matita.cs.unibo.it Git - helm.git/blob - ocaml/mathql_interpreter/select.ml
made executable again
[helm.git] / ocaml / mathql_interpreter / select.ml
1 (* Copyright (C) 2000, HELM Team.
2  * 
3  * This file is part of HELM, an Hypertextual, Electronic
4  * Library of Mathematics, developed at the Computer Science
5  * Department, University of Bologna, Italy.
6  * 
7  * HELM is free software; you can redistribute it and/or
8  * modify it under the terms of the GNU General Public License
9  * as published by the Free Software Foundation; either version 2
10  * of the License, or (at your option) any later version.
11  * 
12  * HELM is distributed in the hope that it will be useful,
13  * but WITHOUT ANY WARRANTY; without even the implied warranty of
14  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
15  * GNU General Public License for more details.
16  *
17  * You should have received a copy of the GNU General Public License
18  * along with HELM; if not, write to the Free Software
19  * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
20  * MA  02111-1307, USA.
21  * 
22  * For details, see the HELM World-Wide-Web page,
23  * http://www.cs.unibo.it/helm/.
24  *)
25
26 (*
27  * implementazione del comando SELECT
28  *)
29 (*
30 open MathQL;;
31 open Func;;
32 open Utility;;
33
34 exception ExecuteFunctionNotInitialized;;
35 let execute =
36  ref
37   (function _ -> raise ExecuteFunctionNotInitialized)
38 ;;
39
40 (*
41  * valutazione di una stringa
42  *)
43 let stringeval env =
44  let module S = Mathql_semantics in
45   function
46      MQCons s ->
47       s
48   |  MQFunc (f, rvar) ->
49       let {S.uri = uri} = List.assoc rvar env in
50        apply_func f uri
51   |  MQStringRVar rvar ->
52       let {S.uri = uri} = List.assoc rvar env in
53        uri
54   |  MQStringSVar svar ->
55       let (_,{S.attributes = attributes}) = List.hd env in
56        List.assoc svar attributes
57   |  MQMConclusion ->
58       "MainConclusion"
59   |  MQConclusion ->
60       "InConclusion"
61 ;;
62
63 (*
64  *
65  *)
66 let rec is_good env =
67  let module S = Mathql_semantics in
68   function
69      MQAnd (b1, b2) ->
70       (is_good env b1) && (is_good env b2)
71   |  MQOr (b1, b2) ->
72       (is_good env b1) || (is_good env b2)
73   |  MQNot b1 ->
74       not (is_good env b1)
75   |  MQTrue ->
76       true
77   |  MQFalse ->
78       false
79   |  MQIs (s1, s2) ->
80       (stringeval env s1) = (stringeval env s2)
81 (*CSC: magari le prossime funzioni dovrebbero  andare in un file a parte, *)
82 (*CSC: insieme alla [execute] che utilizzano                              *)
83   |  MQSetEqual (q1,q2) ->
84       (* set_of_result returns an ordered list of uris without duplicates *)
85       let rec set_of_result =
86        function
87           _,[] -> []
88         | (Some olduri as v),{S.uri = uri}::tl when uri = olduri ->
89             set_of_result (v,tl)
90         | _,{S.uri = uri}::tl ->
91             uri::(set_of_result (Some uri, tl))
92       in
93        let ul1 = set_of_result (None,!execute env q1) in
94        let ul2 = set_of_result (None,!execute env q2) in
95        prerr_endline ("MQSETEQUAL(" ^ 
96            string_of_int (List.length (!execute env q1)) ^ ">" ^
97            string_of_int (List.length ul1) ^ "," ^
98            string_of_int (List.length (!execute env q2)) ^ ">" ^
99            string_of_int (List.length ul2) ^ ")") ;
100        flush stdout ;
101         (try
102           List.fold_left2 (fun b uri1 uri2 -> b && uri1=uri2) true ul1 ul2
103          with
104           _ -> false)
105   |  MQSubset (q1,q2) ->
106 (*CSC: codice cut&paste da sopra: ridurlo facendo un'unica funzione h.o. *)
107       (* set_of_result returns an ordered list of uris without duplicates *)
108       let rec set_of_result =
109        function
110           _,[] -> []
111         | (Some olduri as v),{S.uri = uri}::tl when uri = olduri ->
112             set_of_result (v,tl)
113         | _,{S.uri = uri}::tl ->
114             uri::(set_of_result (Some uri, tl))
115       in
116        let ul1 = set_of_result (None,!execute env q1) in
117        let ul2 = set_of_result (None,!execute env q2) in
118         prerr_endline ("MQSUBSET(" ^ 
119         string_of_int (List.length (!execute env q1)) ^ ">" ^
120         string_of_int (List.length ul1) ^ "," ^
121         string_of_int (List.length (!execute env q2)) ^ ">" ^
122         string_of_int (List.length ul2) ^ ")") ;
123         flush stdout ;
124         let rec is_subset s1 s2 =
125          match s1,s2 with
126             [],_ -> true
127           | _,[] -> false
128           | uri1::tl1,uri2::tl2 when uri1 = uri2 ->
129              is_subset tl1 tl2
130           | uri1::_,uri2::tl2 when uri1 > uri2 ->
131              is_subset s1 tl2
132           | _,_ -> false
133         in
134          is_subset ul1 ul2
135 ;;
136
137 (*
138  * implementazione del comando SELECT
139  *)
140 let select_ex env avar alist abool =
141  let _ = prerr_string ("SELECT = ")
142  and t = Sys.time () in
143   let result = 
144    List.filter (function entry -> is_good ((avar,entry)::env) abool) alist
145   in
146    prerr_string (string_of_int (List.length result) ^ ": ") ;
147    prerr_endline (string_of_float (Sys.time () -. t) ^ "s") ;
148    flush stdout ;
149    result
150 ;; *)
151
152 let select_ex rvar rset bexp
153