X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fmathql_interpreter%2Fselect.ml;fp=helm%2Focaml%2Fmathql_interpreter%2Fselect.ml;h=4b2c264027b69651637bc2fb92b1c89cf20d8dd4;hb=7f510b2df638258669d6539861a3f06ed5fab773;hp=f408b8bfe582ec6521fe9894f2009aef0df4155b;hpb=9f45f8febfade5e1dca7a022154f2635be2af9b2;p=helm.git diff --git a/helm/ocaml/mathql_interpreter/select.ml b/helm/ocaml/mathql_interpreter/select.ml index f408b8bfe..4b2c26402 100644 --- a/helm/ocaml/mathql_interpreter/select.ml +++ b/helm/ocaml/mathql_interpreter/select.ml @@ -31,180 +31,110 @@ open Mathql;; open Func;; open Utility;; -(* - * valutazione di una stringa - *) -let stringeval s l = - match s with - MQCons s -> - s - | MQFunc (f, rvar) -> - apply_func f (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 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 ;; -(*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 - | MQTheory -> "THEORY" ^ rvar - | MQTitle -> "TITLE" ^ rvar - | MQContributor -> "contributor" ^ rvar - | MQCreator -> "creator" ^ rvar - | MQPublisher -> "publisher" ^ rvar - | MQSubject -> "subject" ^ rvar - | MQDescription -> "description" ^ rvar - | MQDate -> "date" ^ rvar - | MQType -> "type" ^ rvar - | MQFormat -> "format" ^ rvar - | MQIdentifier -> "identifier" ^ rvar - | MQLanguage -> "language" ^ rvar - | MQRelation -> "relation" ^ rvar - | MQSource -> "source" ^ rvar - | MQCoverage -> "coverage" ^ rvar - | MQRights -> "rights" ^ rvar - | MQInstitution -> "institution" ^ rvar - | MQContact -> "contact" ^ rvar - | MQFirstVersion -> "firstversion" ^ rvar - | MQModified -> "modified" ^ 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 - | MQTheory -> "THEORY" ^ rvar - | MQTitle -> "TITLE" ^ rvar - | MQContributor -> "contributor" ^ rvar - | MQCreator -> "creator" ^ rvar - | MQPublisher -> "publisher" ^ rvar - | MQSubject -> "subject" ^ rvar - | MQDescription -> "description" ^ rvar - | MQDate -> "date" ^ rvar - | MQType -> "type" ^ rvar - | MQFormat -> "format" ^ rvar - | MQIdentifier -> "identifier" ^ rvar - | MQLanguage -> "language" ^ rvar - | MQRelation -> "relation" ^ rvar - | MQSource -> "source" ^ rvar - | MQCoverage -> "coverage" ^ rvar - | MQRights -> "rights" ^ rvar - | MQInstitution -> "institution" ^ rvar - | MQContact -> "contact" ^ rvar - | MQFirstVersion -> "firstversion" ^ rvar - | MQModified -> "modified" ^ rvar - ) - | MQRVar rvar -> - rvar - | MQSVar svar -> - svar - | MQMConclusion -> - "MainConclusion" - | MQConclusion -> - "InConclusion" - in - print_string (s1v ^ " = " ^ s2v) -;; -*) (* * implementazione del comando SELECT *) -let select_ex avar alist abool = - let _ = print_string ("SELECT ") +let select_ex env avar alist abool = + let _ = print_string ("SELECT = ") and t = Unix.time () in let result = - 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) + List.filter (function entry -> is_good ((avar,entry)::env) abool) alist in - let _ = print_endline (string_of_float (Unix.time () -. t)); flush stdout in - result + print_string (string_of_int (List.length result) ^ ": ") ; + print_endline (string_of_float (Unix.time () -. t) ^ "s") ; + flush stdout ; + result ;; -