]> matita.cs.unibo.it Git - helm.git/commitdiff
WARNING!!!
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 21 Nov 2002 18:16:50 +0000 (18:16 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 21 Nov 2002 18:16:50 +0000 (18:16 +0000)
From now on the V7_3_new_exportation branches of ocaml/mathql and
ocaml/mathql_interpreter are DEPRECATED!!! You must switch back to
the main branch.

helm/gTopLevel/gTopLevel.ml
helm/gTopLevel/mQueryGenerator.ml

index 8ec91964edff51159a58bb197e2d57f5bdc31aa2..4a2fdc561428f8924689839f0128e859f5d556cf 100644 (file)
@@ -2631,8 +2631,11 @@ let initialize_everything () =
 
 let _ =
  if !usedb then
- Mqint.init "dbname=helm_mowgli" ; 
-(* Mqint.init "host=mowgli.cs.unibo.it dbname=helm_mowgli user=helm" ; *)
+  begin
+   Mqint.set_database Mqint.postgres_db ;
+   (* Mqint.init "dbname=helm_mowgli" ; *)
+   Mqint.init "host=mowgli.cs.unibo.it dbname=helm_mowgli user=helm" ;
+  end ;
  ignore (GtkMain.Main.init ()) ;
  initialize_everything () ;
  if !usedb then Mqint.close ();
index 8616cf9d2c9d04ff6fac696fae466d67e1586d88..b91261c07769a32d09de650dfa460bb87f6ec518 100644 (file)
@@ -199,19 +199,27 @@ let execute_query query =
 
 let locate s =
    let module M = MathQL in
-   let q = M.Ref (M.Fun "objectName" (M.Const [s])) in
-   execute_query q
+   let q =
+    M.Ref (M.Attribute true M.RefineExact ("objectName", []) (M.Const [s]))
+   in
+    execute_query q
 
 let searchPattern e c t level =
    let module M = MathQL in
    let v_pos = M.Const ["MainConclusion"; "InConclusion"] in
-   let q_where = M.Sub (M.RefOf (
-      M.Select ("uri", 
-                M.Relation (M.ExactOp, ["refObj"], M.RVar "uri0", ["pos"]),
-                M.Ex ["uri"] (M.Meet (M.VVar "positions", M.Record ("uri", "pos"))) 
-              )),      M.VVar "universe"
-                      )
-   in
+   let q_where =
+    M.Sub
+     (M.RefOf
+       (M.Select
+         ("uri", 
+           M.Relation
+            (false, M.RefineExact, ("refObj", []), M.RVar "uri0", ["pos"]),
+           M.Ex ["uri"]
+            (M.Meet (M.VVar "positions", M.Record ("uri", ("pos", []))))
+         )
+       ),
+       M.VVar "universe"
+     ) in
    let uri_of_entry (r, b, v) = r in
    let rec restrict level = function
       | []                -> []
@@ -220,13 +228,16 @@ let searchPattern e c t level =
          else restrict level tail
    in
    let build_select (r, b, v) =
-      let pos = if b then "MainConclusion" else "InConclusion" in
+    let pos = if b then "MainConclusion" else "InConclusion" in
       M.Select
        ("uri", 
-        M.Relation (M.ExactOp, ["backPointer"], M.Ref (M.Const [r]), ["pos"]),
-        M.Ex ["uri"] (M.Sub (M.Const [pos], M.Record ("uri", "pos")))
-       )
-   in 
+        M.Relation
+         (false,
+          M.RefineExact,
+          ("backPointer", []),
+          M.Ref (M.Const [r]),
+          ["pos"]),
+        M.Ex ["uri"] (M.Sub (M.Const [pos], M.Record ("uri", ("pos", []))))) in 
    let rec build_intersect = function
       | []       -> M.Pattern (M.Const [".*"])
       | [hd]     -> build_select hd