]> matita.cs.unibo.it Git - helm.git/commitdiff
* The new query language (now broken) works only on the new DB
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 27 Nov 2002 10:59:12 +0000 (10:59 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 27 Nov 2002 10:59:12 +0000 (10:59 +0000)
   helm_mowgli_new_schema.
* InConclusion, InHypothesis and so on are now inserted in the DB with their
  namespace.

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

index aca0fe12d5f50b7537a55e673ef532e04f59f764..0546d02b50f7feb12dd477498afbfedc31b3fbb1 100644 (file)
@@ -2635,7 +2635,8 @@ let _ =
   begin
    Mqint.set_database Mqint.postgres_db ;
    (* Mqint.init "dbname=helm_mowgli" ; *)
-   Mqint.init "host=mowgli.cs.unibo.it dbname=helm_mowgli user=helm" ;
+   (* Mqint.init "host=mowgli.cs.unibo.it dbname=helm_mowgli user=helm" ; *)
+   Mqint.init "host=mowgli.cs.unibo.it dbname=helm_mowgli_new_schema user=helm" ;
   end ;
  ignore (GtkMain.Main.init ()) ;
  initialize_everything () ;
index 75c23e837dc5f929c456ce4c767eec90380b0ac6..843eb96c050ee80174ca5c4ba630674daaccd15c 100644 (file)
@@ -99,9 +99,13 @@ let locate s =
 let searchPattern e c t level =
    let module M = MathQL in
    let module L = MQueryLevels in
+   let mainConclusion =
+    "http://www.cs.unibo.it/helm/schemas/schema-helm#MainConclusion" in
+   let inConclusion =
+    "http://www.cs.unibo.it/helm/schemas/schema-helm#InConclusion" in
    let in_path s = (s, []) in
    let assign v p = (in_path v, in_path p) in 
-   let v_pos = M.Const ["MainConclusion"; "InConclusion"] in
+   let v_pos = M.Const [mainConclusion; inConclusion] in
    let q_where =
     M.Sub
      (M.RefOf
@@ -125,7 +129,7 @@ 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 (false, M.RefineExact, ("backPointer", []),
@@ -144,4 +148,5 @@ let searchPattern e c t level =
    let universe = M.Const (List.map uri_of_entry levels) in
    let q_let_u = M.LetVVar ("universe", universe, q_select) in
    let q_let_p = M.LetVVar ("positions", v_pos, q_let_u) in
+prerr_endline ("### " ^ MQueryUtil.text_of_query q_let_p) ;
    execute_query q_let_p