--- /dev/null
+(* Copyright (C) 2000, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://www.cs.unibo.it/helm/.
+ *)
+
+(*
+ * implementazione del comando SELECT
+ *)
+
+open MathQL;;
+open Func;;
+
+
+exception ExecuteFunctionNotInitialized;;
+let execute =
+ ref
+ (function _ -> raise ExecuteFunctionNotInitialized)
+;;
+
+(*
+ * valutazione di una stringa
+ *)
+let stringeval env =
+ let module S = Mathql_semantics in
+ function
+ MQCons s ->
+ s
+ | MQFunc (f, rvar) ->
+ let {S.uri = uri} = List.assoc rvar env in
+ apply_func f uri
+ | MQStringRVar rvar ->
+ let {S.uri = uri} = List.assoc rvar env in
+ uri
+ | MQStringSVar svar ->
+ let (_,{S.attributes = attributes}) = List.hd env in
+ List.assoc svar attributes
+ | MQMConclusion ->
+ "MainConclusion"
+ | MQConclusion ->
+ "InConclusion"
+;;
+
+
+
+
+let rec is_good env =
+ let module S = Mathql_semantics in
+ function
+ MQAnd (b1, b2) ->
+ (is_good env b1) && (is_good env b2)
+ | MQOr (b1, b2) ->
+ (is_good env b1) || (is_good env b2)
+ | MQNot b1 ->
+ not (is_good env b1)
+ | MQTrue ->
+ true
+ | MQFalse ->
+ false
+ | MQIs (s1, s2) ->
+ (stringeval env s1) = (stringeval env s2)
+(*CSC: magari le prossime funzioni dovrebbero andare in un file a parte, *)
+(*CSC: insieme alla [execute] che utilizzano *)
+ | MQSetEqual (q1,q2) ->
+ (* set_of_result returns an ordered list of uris without duplicates *)
+ let rec set_of_result =
+ function
+ _,[] -> []
+ | (Some olduri as v),{S.uri = uri}::tl when uri = olduri ->
+ set_of_result (v,tl)
+ | _,{S.uri = uri}::tl ->
+ uri::(set_of_result (Some uri, tl))
+ in
+ let ul1 = set_of_result (None,!execute env q1) in
+ let ul2 = set_of_result (None,!execute env q2) in
+prerr_endline ("MQSETEQUAL(" ^ string_of_int (List.length (!execute env q1)) ^ ">" ^ string_of_int (List.length ul1) ^ "," ^ string_of_int (List.length (!execute env q2)) ^ ">" ^ string_of_int (List.length ul2) ^ ")") ; flush stderr ;
+ (try
+ List.fold_left2 (fun b uri1 uri2 -> b && uri1=uri2) true ul1 ul2
+ with
+ _ -> false)
+ | MQSubset (q1,q2) ->
+(*CSC: codice cut&paste da sopra: ridurlo facendo un'unica funzione h.o. *)
+ (* set_of_result returns an ordered list of uris without duplicates *)
+ let rec set_of_result =
+ function
+ _,[] -> []
+ | (Some olduri as v),{S.uri = uri}::tl when uri = olduri ->
+ set_of_result (v,tl)
+ | _,{S.uri = uri}::tl ->
+ uri::(set_of_result (Some uri, tl))
+ in
+ let ul1 = set_of_result (None,!execute env q1) in
+ let ul2 = set_of_result (None,!execute env q2) in
+prerr_endline ("MQSUBSET(" ^ string_of_int (List.length (!execute env q1)) ^ ">" ^ string_of_int (List.length ul1) ^ "," ^ string_of_int (List.length (!execute env q2)) ^ ">" ^ string_of_int (List.length ul2) ^ ")") ; flush stderr ;
+ let rec is_subset s1 s2 =
+ match s1,s2 with
+ [],_ -> true
+ | _,[] -> false
+ | uri1::tl1,uri2::tl2 when uri1 = uri2 ->
+ is_subset tl1 tl2
+ | uri1::_,uri2::tl2 when uri1 > uri2 ->
+ is_subset s1 tl2
+ | _,_ -> false
+ in
+ is_subset ul1 ul2
+;;
+
+
+(*
+ * implementazione del comando SELECT
+ *)
+
+
+let select_ex env avar alist abool =
+ let _ = print_string ("SELECT = ")
+ and t = Unix.time () in
+ let result =
+ List.filter (function entry -> is_good ((avar,entry)::env) abool) alist
+ in
+ print_string (string_of_int (List.length result) ^ ": ") ;
+ print_endline (string_of_float (Unix.time () -. t) ^ "s") ;
+ flush stdout ;
+ result
+;;
+
+