X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fmathql_interpreter%2Fselect.ml;h=ee9f329ba36ec61971784eb3f2ab6d9b1f876b22;hb=b1fb6b8e1767d775bc452303629e95941d142bea;hp=6f60a3e313949c7a5a944f7ac005ff88749bb709;hpb=6a1d05b388683befc860b48b4f2bbaf42f58a112;p=helm.git diff --git a/helm/ocaml/mathql_interpreter/select.ml b/helm/ocaml/mathql_interpreter/select.ml index 6f60a3e31..ee9f329ba 100644 --- a/helm/ocaml/mathql_interpreter/select.ml +++ b/helm/ocaml/mathql_interpreter/select.ml @@ -1,143 +1,153 @@ +(* 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 MathQL;; 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 + | 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 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 + print_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 stdout ; + (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 + print_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 stdout ; + 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 = Sys.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 (Sys.time () -. t) ^ "s") ; + flush stdout ; + result +;; *) + +let select_ex rvar rset bexp