]> matita.cs.unibo.it Git - helm.git/blob - helm/ocaml/mathql_interpreter/mqint.ml
Debugging Sub and Meet
[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 Sub;;
41 open Context;;
42 open Diff;;
43 open Relation;;
44
45
46 let init connection_param = Dbconn.init connection_param 
47
48 let close () = Dbconn.close ()
49
50 let check () = Dbconn.pgc ()
51
52 exception BooleExpTrue
53
54 (* valuta una MathQL.set_exp e ritorna un MathQL.resource_set *)
55
56 let rec exec_set_exp c = function
57    |MathQL.SVar svar -> List.assoc svar c.svars
58    |MathQL.RVar rvar -> [List.assoc rvar c.rvars]  
59    | MathQL.Ref vexp -> List.map (fun s -> (s,[])) (exec_val_exp c vexp)
60    | MathQL.Intersect (sexp1, sexp2) -> intersect_ex (exec_set_exp c sexp1) (exec_set_exp c sexp2)    
61    | MathQL.Union (sexp1, sexp2) -> 
62         let before = Sys.time () in
63         let res = union_ex (exec_set_exp c sexp1) (exec_set_exp c sexp2) in
64         let after = Sys.time () in
65         let diff = string_of_float (after -. before) in
66         print_endline ("UNION: " ^ diff ^ "s") ;
67         flush stdout ;
68         res                     
69    | MathQL.LetSVar (svar, sexp1, sexp2) ->
70         let before = Sys.time () in
71         let c1 = upd_svars c ((svar, exec_set_exp c sexp1) :: c.svars) in 
72         let res = exec_set_exp c1 sexp2 in
73         print_string ("LETIN " ^ svar ^ " = " ^ string_of_int (List.length res) ^ ": ") ;
74         print_endline (string_of_float (Sys.time () -. before) ^ "s") ;
75         flush stdout ; res                      
76    | MathQL.LetVVar (vvar, vexp, sexp) ->
77         let before = Sys.time () in
78         let c1 = upd_vvars c ((vvar, exec_val_exp c vexp) :: c.vvars) in
79         let res = exec_set_exp c1 sexp in
80         print_string ("LETIN " ^ vvar ^ " = " ^ string_of_int (List.length res) ^ ": ") ;
81         print_endline (string_of_float (Sys.time () -. before) ^ "s") ;
82         flush stdout ; res
83    | MathQL.Relation (rop, path, sexp, attl) -> relation_ex rop path (exec_set_exp c sexp) attl
84    | MathQL.Select (rvar, sexp, bexp) ->
85         let before = Sys.time () in
86         let rset = (exec_set_exp c sexp) in
87         let rec select_ex rset =
88         match rset with 
89           [] -> []
90         | r::tl -> let c1 = upd_rvars c ((rvar,r)::c.rvars) in                      
91                    if (exec_boole_exp c1 bexp) then r::(select_ex tl)
92                    else select_ex tl
93         in 
94         let res = select_ex rset in
95         print_string ("SELECT " ^ rvar ^ " = " ^ string_of_int (List.length res) ^ ": ") ;
96         print_endline (string_of_float (Sys.time () -. before) ^ "s") ;
97         flush stdout ; res
98    | MathQL.Diff (sexp1, sexp2) -> diff_ex (exec_set_exp c sexp1) (exec_set_exp c sexp2)
99    | _ -> assert false
100    
101 (* valuta una MathQL.boole_exp e ritorna un boole *)
102
103 and exec_boole_exp c = function
104    | MathQL.False      -> false
105    | MathQL.True       -> true
106    | MathQL.Not x      -> not (exec_boole_exp c x)
107    | MathQL.And (x, y) -> (exec_boole_exp c x) && (exec_boole_exp c y)
108    | MathQL.Or (x, y)  -> (exec_boole_exp c x) || (exec_boole_exp c y)
109    | MathQL.Sub (vexp1, vexp2) -> let res = sub_ex (exec_val_exp c vexp1) (exec_val_exp c vexp2)
110                                   in
111                                    if res then (print_endline"SUB: TRUE";flush stdout)
112                                    else (print_endline"SUB: FALSE";flush stdout);
113                                    res
114    | MathQL.Meet (vexp1, vexp2) -> let res = meet_ex (exec_val_exp c vexp1) (exec_val_exp c vexp2)
115                                    in
116                                    if res then (print_endline"MEET: TRUE";flush stdout)
117                                    else (print_endline"MEET: FALSE";flush stdout);
118                                    res
119                                    
120    | MathQL.Eq (vexp1, vexp2) -> (exec_val_exp c vexp1) = (exec_val_exp c vexp2)
121    | MathQL.Ex l bexp -> 
122         let res = 
123         if l = [] then (print_endline"LISTA VUOTA!";flush stdout;(exec_boole_exp c bexp))
124         else
125          let latt = List.map (fun uri -> 
126                                 let (r,attl) = List.assoc uri c.rvars in (uri,attl)) l (*latt = l + attributi*)
127          in
128          try
129          let rec prod c = function
130               [] -> if (exec_boole_exp c bexp) then raise BooleExpTrue 
131             | (uri,attl)::tail1 -> let rec sub_prod attl =
132                                       match attl with
133 (*per ogni el. di attl  *)              [] -> () 
134 (*devo andare in ric. su tail1*)      | att::tail2 -> let c1 = upd_groups c ((uri,att)::c.groups) in             
135                                                        prod c1 tail1; sub_prod tail2 
136                                      in       
137                                       sub_prod attl 
138          in
139          prod c latt; print_endline"SONO ARRIVATO ALLA FINE!"; flush stdout;false
140          with BooleExpTrue -> true
141         in if res then (print_endline"TRUE"; flush stdout)
142            else (print_endline"FALSE"; flush stdout);
143            res
144    | _ -> assert false    
145
146 (* valuta una MathQL.val_exp e ritorna un MathQL.value *)
147
148 and exec_val_exp c = function
149    | MathQL.Const x -> let
150         ol = List.sort compare x in 
151                         let rec edup = function
152                         
153                            [] -> [] 
154                          | s::tl -> if tl <> [] then  
155                                                  if s = (List.hd tl) then edup tl
156                                                  else s::(edup tl)
157                                     else s::[]
158                         in
159                          edup ol
160    | MathQL.Record (rvar, vvar) -> List.assoc vvar (List.assoc rvar c.groups) 
161                                   
162    | MathQL.VVar s -> List.assoc s c.vvars                                
163    | MathQL.RefOf sexp -> List.map (fun (s,_) -> s) (exec_set_exp c sexp)
164    
165    | _ -> assert false
166
167
168 (* valuta una MathQL.set_exp nel contesto vuoto e ritorna un MathQL.resource_set *)
169
170 and execute x =
171    exec_set_exp {svars = []; rvars = []; groups = []; vvars = []} x