]> matita.cs.unibo.it Git - helm.git/blob - helm/ocaml/mathql_interpreter/mqint.ml
Relation patched, property added.
[helm.git] / helm / ocaml / mathql_interpreter / mqint.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
28
29 (*
30  * implementazione del'interprete MathQL
31  *)
32
33
34
35
36 open Dbconn;;
37 open Union;;
38 open Intersect;;
39 open Meet;;
40 open Property;;
41 open Sub;;
42 open Context;;
43 open Diff;;
44 open Relation;;
45 open Func;;
46 open Pattern;;
47
48 exception BooleExpTrue
49
50 let init connection_param = Dbconn.init connection_param 
51
52 let close () = Dbconn.close ()
53
54 let check () = 
55    let status = Dbconn.pgc () 
56    in ()
57
58 let stat = ref true
59
60 let set_stat b = stat := b
61
62 let get_stat () = ! stat
63
64 let postgres_db = "postgres"
65
66 let galax_db = "galax"
67
68 let dbname = ref galax_db
69
70 let set_database s = 
71     if s = postgres_db || s = galax_db then dbname := s
72     else raise (Invalid_argument s)
73
74 let get_database () = ! dbname
75
76 (* valuta una MathQL.set_exp e ritorna un MathQL.resource_set *)
77
78 let rec exec_set_exp c = function
79      MathQL.SVar svar -> List.assoc svar c.svars
80    | MathQL.RVar rvar -> [List.assoc rvar c.rvars]  
81    | MathQL.Ref vexp -> List.map (fun s -> (s,[])) (exec_val_exp c vexp)
82    | MathQL.Pattern vexp -> pattern_ex (exec_val_exp c vexp)
83    | MathQL.Intersect (sexp1, sexp2) ->    
84         let before = Sys.time() in
85         let rs1 = exec_set_exp c sexp1 in
86         let rs2 = exec_set_exp c sexp2 in
87         let res = intersect_ex rs1 rs2 in
88         let after = Sys.time() in
89         let ll1 = string_of_int (List.length rs1) in
90         let ll2 = string_of_int (List.length rs2) in
91         let diff = string_of_float (after -. before) in
92         if !stat then
93         (print_endline("INTERSECT(" ^ ll1 ^ "," ^ ll2 ^ ") = " ^ string_of_int (List.length res) ^
94          ": " ^ diff ^ "s");
95          flush stdout);
96         res
97    | MathQL.Union (sexp1, sexp2) -> 
98         let before = Sys.time () in
99         let res = union_ex (exec_set_exp c sexp1) (exec_set_exp c sexp2) in
100         let after = Sys.time() in
101         let diff = string_of_float (after -. before) in
102         if !stat then
103         (print_endline ("UNION: " ^ diff ^ "s");
104          flush stdout);
105         res                     
106    | MathQL.LetSVar (svar, sexp1, sexp2) ->
107         let before = Sys.time() in
108         let c1 = upd_svars c ((svar, exec_set_exp c sexp1) :: c.svars) in 
109         let res = exec_set_exp c1 sexp2 in
110         if ! stat then
111         (print_string ("LETIN " ^ svar ^ " = " ^ string_of_int (List.length res) ^ ": ");
112          print_endline (string_of_float (Sys.time() -. before) ^ "s");
113          flush stdout); 
114         res                     
115    | MathQL.LetVVar (vvar, vexp, sexp) ->
116         let before = Sys.time() in
117         let c1 = upd_vvars c ((vvar, exec_val_exp c vexp) :: c.vvars) in
118         let res = exec_set_exp c1 sexp in
119         if ! stat then
120         (print_string ("LETIN " ^ vvar ^ " = " ^ string_of_int (List.length res) ^ ": ");
121          print_endline (string_of_float (Sys.time() -. before) ^ "s");
122          flush stdout); 
123         res
124    | MathQL.Relation (inv, rop, path, sexp, assl) -> 
125         let before = Sys.time() in
126         if ! dbname = postgres_db then
127         (let res = relation_ex inv rop path (exec_set_exp c sexp) assl in
128          if ! stat then 
129          (print_string ("RELATION " ^ (fst path) ^ " = " ^ string_of_int(List.length res) ^ ": ");
130           print_endline (string_of_float (Sys.time() -. before) ^ "s");
131           flush stdout);
132          res)
133         
134         else
135         (let res = relation_galax_ex inv rop path (exec_set_exp c sexp) assl in
136          if !stat then
137          (print_string ("RELATION-GALAX " ^ (fst path) ^ " = " ^ string_of_int(List.length res) ^ ": ");
138           print_endline (string_of_float (Sys.time() -. before) ^ "s");
139           flush stdout);
140          res) 
141         
142         
143    | MathQL.Select (rvar, sexp, bexp) ->
144         let before = Sys.time() in
145         let rset = (exec_set_exp c sexp) in
146         let rec select_ex rset =
147         match rset with 
148           [] -> []
149         | r::tl -> let c1 = upd_rvars c ((rvar,r)::c.rvars) in                      
150                    if (exec_boole_exp c1 bexp) then r::(select_ex tl)
151                    else select_ex tl
152         in 
153         let res = select_ex rset in
154         if ! stat then
155         (print_string ("SELECT " ^ rvar ^ " = " ^ string_of_int (List.length res) ^ ": ");
156          print_endline (string_of_float (Sys.time() -. before) ^ "s");
157          flush stdout); 
158         res
159    | MathQL.Diff (sexp1, sexp2) -> diff_ex (exec_set_exp c sexp1) (exec_set_exp c sexp2)
160    
161 (* valuta una MathQL.boole_exp e ritorna un boole *)
162
163 and exec_boole_exp c = function
164      MathQL.False      -> false
165    | MathQL.True       -> true
166    | MathQL.Not x      -> not (exec_boole_exp c x)
167    | MathQL.And (x, y) -> (exec_boole_exp c x) && (exec_boole_exp c y)
168    | MathQL.Or (x, y)  -> (exec_boole_exp c x) || (exec_boole_exp c y)
169    | MathQL.Sub (vexp1, vexp2) -> sub_ex (exec_val_exp c vexp1) (exec_val_exp c vexp2)
170    | MathQL.Meet (vexp1, vexp2) -> meet_ex (exec_val_exp c vexp1) (exec_val_exp c vexp2)
171    | MathQL.Eq (vexp1, vexp2) -> (exec_val_exp c vexp1) = (exec_val_exp c vexp2)
172    | MathQL.Ex l bexp -> 
173         if l = [] then (exec_boole_exp c bexp)
174         else
175          let latt = List.map (fun uri -> 
176                                 let (r,attl) = List.assoc uri c.rvars in (uri,attl)) l (*latt = l + attributi*)
177          in
178          try
179          let rec prod c = function
180               [] -> if (exec_boole_exp c bexp) then raise BooleExpTrue 
181             | (uri,attl)::tail1 -> let rec sub_prod attl =
182                                       match attl with
183 (*per ogni el. di attl  *)              [] -> () 
184 (*devo andare in ric. su tail1*)      | att::tail2 -> let c1 = upd_groups c ((uri,att)::c.groups) in             
185                                                        prod c1 tail1; sub_prod tail2 
186                                      in       
187                                       sub_prod attl 
188          in
189          prod c latt; false
190          with BooleExpTrue -> true
191
192 (* valuta una MathQL.val_exp e ritorna un MathQL.value *)
193
194 and exec_val_exp c = function
195      MathQL.Const x -> let
196         ol = List.sort compare x in 
197                         let rec edup = function
198                         
199                            [] -> [] 
200                          | s::tl -> if tl <> [] then  
201                                                  if s = (List.hd tl) then edup tl
202                                                  else s::(edup tl)
203                                     else s::[]
204                         in
205                          edup ol
206    | MathQL.Record (rvar, path) -> List.assoc path (List.assoc rvar c.groups) 
207                                   
208    | MathQL.VVar s -> List.assoc s c.vvars                                
209    | MathQL.RefOf sexp -> List.map (fun (s,_) -> s) (exec_set_exp c sexp)
210    | MathQL.Fun (s, vexp) -> fun_ex s (exec_val_exp c vexp)
211    | MathQL.Property (inv, rop, path, vexp) -> property_ex rop path inv (exec_val_exp c vexp) 
212
213 (* valuta una MathQL.set_exp nel contesto vuoto e ritorna un MathQL.resource_set *)
214 and execute x =
215    exec_set_exp {svars = []; rvars = []; groups = []; vvars = []} x