helm/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://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   |  MQRVar rvar ->
  52       let {S.uri = uri} = List.assoc rvar env in
  53        uri
  54   |  MQSVar 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(" ^ 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 ;
  96         (try
  97           List.fold_left2 (fun b uri1 uri2 -> b && uri1=uri2) true ul1 ul2
  98          with
  99           _ -> false)
 100   |  MQSubset (q1,q2) ->
 101 (*CSC: codice cut&paste da sopra: ridurlo facendo un'unica funzione h.o. *)
 102       (* set_of_result returns an ordered list of uris without duplicates *)
 103       let rec set_of_result =
 104        function
 105           _,[] -> []
 106         | (Some olduri as v),{S.uri = uri}::tl when uri = olduri ->
 107             set_of_result (v,tl)
 108         | _,{S.uri = uri}::tl ->
 109             uri::(set_of_result (Some uri, tl))
 110       in
 111        let ul1 = set_of_result (None,!execute env q1) in
 112        let ul2 = set_of_result (None,!execute env q2) in
 113 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 ;
 114         let rec is_subset s1 s2 =
 115          match s1,s2 with
 116             [],_ -> true
 117           | _,[] -> false
 118           | uri1::tl1,uri2::tl2 when uri1 = uri2 ->
 119              is_subset tl1 tl2
 120           | uri1::_,uri2::tl2 when uri1 > uri2 ->
 121              is_subset s1 tl2
 122           | _,_ -> false
 123         in
 124          is_subset ul1 ul2
 125 ;;
 126
 127 (*
 128  * implementazione del comando SELECT
 129  *)
 130 let select_ex env avar alist abool =
 131  let _ = print_string ("SELECT = ")
 132  and t = Unix.time () in
 133   let result =
 134    List.filter (function entry -> is_good ((avar,entry)::env) abool) alist
 135   in
 136    print_string (string_of_int (List.length result) ^ ": ") ;
 137    print_endline (string_of_float (Unix.time () -. t) ^ "s") ;
 138    flush stdout ;
 139    result
 140 ;;