+(* 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://cs.unibo.it/helm/.
+ *)
(*
* implementazione del comando SELECT
open Func;;
open Utility;;
-(*
- * valutazione di una stringa
- *)
-let stringeval s l =
- match s with
- MQCons s ->
- s
- | MQFunc (f, rvar) ->
- (
- match f with
- MQName -> func_name (List.assoc rvar l)
- )
- | MQRVar rvar ->
- List.assoc rvar l
- | MQSVar svar ->
- List.assoc svar l
- | MQMConclusion ->
- "MainConclusion"
- | MQConclusion ->
- "InConclusion"
+exception ExecuteFunctionNotInitialized;;
+let execute =
+ ref
+ (function _ -> raise ExecuteFunctionNotInitialized)
;;
(*
- *
+ * valutazione di una stringa
*)
-let rec is_good l abool =
- match abool with
- MQAnd (b1, b2) ->
- (is_good l b1) && (is_good l b2)
- | MQOr (b1, b2) ->
- (is_good l b1) || (is_good l b2)
- | MQNot b1 ->
- not (is_good l b1)
- | MQTrue ->
- true
- | MQFalse ->
- false
- | MQIs (s1, s2) ->
- (stringeval s1 l) = (stringeval s2 l)
+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
+ | MQRVar rvar ->
+ let {S.uri = uri} = List.assoc rvar env in
+ uri
+ | MQSVar svar ->
+ let (_,{S.attributes = attributes}) = List.hd env in
+ List.assoc svar attributes
+ | MQMConclusion ->
+ "MainConclusion"
+ | MQConclusion ->
+ "InConclusion"
;;
(*
*
*)
-let rec replace avar newval l =
- match l with
- MQAnd (b1, b2) -> MQAnd (replace avar newval b1, replace avar newval b2)
- | MQOr (b1, b2) -> MQOr (replace avar newval b1, replace avar newval b2)
- | MQNot b1 -> MQNot (replace avar newval b1)
- | MQIs (s1, s2) ->
- let ns1 = (
- match s1 with
- MQRVar v when v = avar -> MQRVar newval
- | MQFunc (f, v) when v = avar -> MQFunc (f, newval)
- | _ -> s1
- )
- and ns2 = (
- match s2 with
- MQRVar v when v = avar -> MQRVar newval
- | MQFunc (f, v) when v = avar -> MQFunc (f, newval)
- | _ -> s2
- )
- in
- MQIs (ns1, ns2)
- | _ -> l (* i casi non compresi sono MQTrue e MQFalse *)
-;;
-
-let rec print_booltree b =
- match b with
- MQAnd (b1, b2) ->
- let i = print_booltree b1 in
- let j = print_string " AND " in
- print_booltree b2
- | MQOr (b1, b2) ->
- let i = print_booltree b1 in
- let j = print_string " OR " in
- print_booltree b2
- | MQNot b1 ->
- let j = print_string " NOT " in
- print_booltree b1
- | MQTrue ->
- print_string " TRUE "
- | MQFalse ->
- print_string " FALSE "
- | MQIs (s1, s2) ->
- let s1v = match s1 with
- MQCons s ->
- "'" ^ s ^ "'"
- | MQFunc (f, rvar) ->
- (
- match f with
- MQName -> "NAME " ^ rvar
- )
- | MQRVar rvar ->
- rvar
- | MQSVar svar ->
- svar
- | MQMConclusion ->
- "MainConclusion"
- | MQConclusion ->
- "InConclusion"
- and s2v = match s2 with
- MQCons s ->
- s
- | MQFunc (f, rvar) ->
- (
- match f with
- MQName -> "NAME " ^ rvar
- )
- | MQRVar rvar ->
- rvar
- | MQSVar svar ->
- svar
- | MQMConclusion ->
- "MainConclusion"
- | MQConclusion ->
- "InConclusion"
- in
- print_string (s1v ^ " = " ^ s2v)
+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 avar alist abool =
- let wrt = replace avar "retVal" abool in
- (*let j = print_booltree wrt in*)
- [List.hd alist]
- @
- List.find_all
- (fun l -> is_good (List.combine (List.hd alist) l) wrt)
- (List.tl alist)
+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
;;
-
projects / helm.git / blobdiff