]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/gTopLevel/mQueryGenerator.ml
- added and exposed get_current_status_as_xml
[helm.git] / helm / gTopLevel / mQueryGenerator.ml
index c925e27a69cecbd62d53041bd5a8a54b78952197..ed52e55bda7e11825d8299628fcb2c6369d990c8 100644 (file)
 
 (* Query issuing functions **************************************************)
 
+
+
+type uri = string
+type position = string
+type depth = int option
+type sort = string 
+
+type r_obj = (uri * position * depth)  
+type r_rel = (position* depth) 
+type r_sort = (position* depth * sort) 
+
+type must_restrictions = (r_obj list * r_rel list * r_sort list)
+type only_restrictions =
+ (r_obj list option * r_rel list option * r_sort list option)
+
 exception Discard  
 
 let nl = " <p>\n"
@@ -71,11 +86,10 @@ let execute_query query =
    in
    let log q r = 
       let och = open_out_gen mode perm ! log_file in
-      if ! query_num = 1 then output_string och (time () ^ nl);
-      let str =
-       "Query: " ^ string_of_int ! query_num ^ nl ^ Util.text_of_query q ^ nl ^ 
-       "Result:" ^ nl ^ Util.text_of_result r nl in
-      output_string och str; 
+      let out = output_string och in
+      if ! query_num = 1 then out (time () ^ nl);
+      out ("Query: " ^ string_of_int ! query_num ^ nl); Util.text_of_query out q nl; 
+      out ("Result:" ^ nl); Util.text_of_result out r nl; 
       flush och 
    in
    let execute q =
@@ -96,59 +110,445 @@ let locate s =
    in
     execute_query q
 
-let searchPattern e c t must_use can_use =
+let searchPattern must_use can_use =    
    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 q_where =
-    M.Sub
-     (M.RefOf
-       (M.Select
-         ("uri", 
-           M.Relation
-            (false, M.RefineExact, in_path "refObj", 
-            M.Ref (M.RefOf (M.RVar "uri0")), 
-            [assign "pos" "position"]),
-           M.Ex ["uri"]
-            (M.Meet (M.VVar "positions", M.Record ("uri", in_path "pos")))
-         )
-       ),
-       M.VVar "universe"
-     ) in
-   let uri_of_entry (r, b) = r in
-   (*let rec restrict level = function
-      | []                -> []
-      | (u, b, v) :: tail ->
-         if v <= level then (u, b, v) :: restrict level tail
-         else restrict level tail
-   in*)
-   let build_select (r, b) =
-    print_endline (">>>>LA URI: "^r);
-    let pos = if b then mainConclusion else inConclusion in
-      M.Select
-       ("uri", 
-        M.Relation (false, M.RefineExact, ("backPointer", []),
-                   M.Ref (M.Const [r]), [assign "pos" "position"]),
-        M.Ex ["uri"] (M.Sub (M.Const [pos], M.Record ("uri", in_path "pos")))) in 
-   let rec build_intersect = function
-      | []       -> M.Pattern (M.Const ["[.]*"])
-      | [hd]     -> build_select hd
-      | hd :: tl -> M.Intersect (build_select hd, build_intersect tl)
-   in
-
-  (* let levels = L.levels_of_term e c t in
-   let rest = restrict level levels in
-   info := [string_of_int (List.length rest)];*)
+  
+(* can restrictions *)  
+   
+   let (cr_o,cr_r,cr_s) = can_use in
+   
+   let uri_of_entry (r, p, d) = r in
+   
+   let universe = 
+     match cr_o with
+       None -> []
+     | Some cr_o -> List.map uri_of_entry cr_o 
+   in
+  
+   let tfst (a,b,c) = a in
+   let tsnd (a,b,c) = b in
+   let trd (a,b,c) = c in
+   
+   let to_int_list l d =
+   match d with
+     None -> l
+   | Some d -> l@[d]
+   in
+
+   let opos =
+     match cr_o with
+       None -> []
+     | Some cr_o -> (List.map tsnd cr_o) in
+   
+   let odep = 
+     match cr_o with
+       None -> []
+     | Some cr_o -> List.map trd cr_o
+                  (*  let odep_option_list = List.map trd cr_o in
+                   let lo_dep_int = List.fold_left to_int_list [] odep_option_list in
+                     List.map string_of_int lo_dep_int*)
+   in
+   print_string "#### LUNGHEZZA ODEP: "; print_int (List.length odep); flush stdout;
+   print_endline"";
+   let rpos = 
+     match cr_r with
+       None -> []
+     | Some cr_r -> (List.map fst cr_r) in
+   
+   let rdep = 
+     match cr_r with
+       None -> []
+     | Some cr_r -> List.map snd cr_r 
+                   (* let rdep_option_list = List.map snd cr_r in
+                    let lr_dep_int = List.fold_left to_int_list [] rdep_option_list in
+                      List.map string_of_int lr_dep_int *)
+   in 
+   
+
+   let spos = 
+     match cr_s with
+       None -> []
+     | Some cr_s -> (List.map tfst cr_s) in
+   
+      
+   let sdep = 
+     match cr_s with
+       None -> []
+     | Some cr_s -> List.map tsnd cr_s
+                   (* let sdep_option_list = List.map tsnd cr_s in
+                    let ls_dep_int = List.fold_left to_int_list [] sdep_option_list in
+                      List.map string_of_int ls_dep_int*)
+   in  
+   
+   
+   let sor = 
+     match cr_s with
+       None -> []
+     | Some cr_s -> List.map trd cr_s in 
+
+  (* let q_where_obj = function
+       Some l ->
+         if odep = [] then
+           M.Sub
+           (M.RefOf
+           (M.Select
+              ("uri", 
+              M.Relation (false, M.RefineExact, in_path "refObj", M.Ref (M.RefOf (M.RVar "uri0")), [assign "pos" "position"]),
+              M.Ex ["uri"]
+              (M.Meet (M.VVar "obj_positions", M.Record ("uri", in_path "pos"))))), 
+          M.VVar "universe")
+        else
+          M.Sub
+           (M.RefOf
+            (M.Select
+              ("uri", 
+                M.Relation
+                 (false, M.RefineExact, in_path "refObj",
+                   M.Ref (M.RefOf (M.RVar "uri0")),
+                   [assign "p" "position"; assign "d" "depth"]
+                 ),
+                M.Ex ["uri"]
+                (M.And
+                  ((M.Meet(M.VVar "obj_positions",M.Record("uri",in_path "p"))),
+                   (M.Meet(M.VVar "obj_depths", M.Record("uri",in_path "d")))))
+              )
+            ), 
+           M.VVar "universe"
+           )
+        
+     | None -> M.True           
+   in*) 
+  
+
+
+   let q_where_obj n = function
+       Some l ->
+         let rec q_ex n = function
+            [] -> M.True 
+          | [(u,p,None)] ->
+                            M.Meet (M.VVar ("obj_position" ^ string_of_int n), M.Record ("uri", in_path "p"))
+                            
+          | [(u,p,d)] ->
+                         print_string "@@@@@ IN-WHERE-OBJ"; flush stdout;
+                                                         print_endline"";
+                         M.And
+                            (M.Meet(M.VVar ("obj_position" ^ string_of_int n),M.Record("uri",in_path "p")),
+                             M.Meet(M.VVar ("obj_depth" ^ string_of_int n), M.Record("uri",in_path "d")))
+           | (u,p,None)::tl ->
+                              M.Or
+                                (M.Meet (M.VVar ("obj_position" ^ string_of_int n), M.Record ("uri", in_path "p")),
+                                q_ex (n+1) tl)
+          | (u,p,d)::tl ->
+                            print_string "@@@@@ IN-WHERE-OBJ"; flush stdout;
+                               print_endline"";
+                            M.Or
+                            ((M.And
+                               ((M.Meet(M.VVar ("obj_position" ^ string_of_int n),M.Record("uri",in_path "p"))),
+                                (M.Meet(M.VVar ("obj_depth" ^ string_of_int n), M.Record("uri",in_path "d"))))),
+                            q_ex (n+1) tl)
+        in    
+         M.Sub
+           (M.RefOf
+            (M.Select
+              ("uri", 
+                M.Relation
+                 (false, M.RefineExact, in_path "refObj",
+                   M.Ref (M.RefOf (M.RVar "uri0")),
+                   [assign "p" "position"; assign "d" "depth"]
+                 ),
+                M.Ex ["uri"]
+               (q_ex 1 l))),
+            M.VVar "universe")
+       | None -> M.True
+   in
+
+
+
+  
+   let rec q_where_rel n cr_r= (*function*)
+     (*  Some l ->*)
+        let q0 =
+          M.Sub
+           (M.Property
+             (false, M.RefineExact, ("refRel", ["position"]),
+               M.RefOf(M.RVar "uri0")),
+            M.VVar ("rel_position" ^ string_of_int n))
+          in
+          match cr_r with
+            Some [] -> M.True
+          | Some [(p,None)] -> q0
+          | Some [(p,d)] ->
+                       M.And  
+                        (q0,
+                          M.Sub
+                           (M.Property
+                             (false, M.RefineExact, ("refRel", ["depth"]),
+                              M.RefOf(M.RVar "uri0")),
+                            M.VVar ("rel_depth" ^ string_of_int n)))
+           | Some ((p,None)::tl) -> 
+                              M.Or
+                               (q0,
+                                q_where_rel (n+1) (Some tl))
+           | Some ((p,d)::tl) -> 
+                           M.Or
+                            (M.And
+                              (q0,
+                               M.Sub
+                                 (M.Property
+                                   (false, M.RefineExact, ("refRel", ["depth"]),
+                                    M.RefOf(M.RVar "uri0")),
+                                  M.VVar ("rel_depth" ^ string_of_int n))),
+                             q_where_rel (n+1) (Some tl))
+           | None -> M.True            
+   in
+
+   let rec q_where_sort n cr_s = (*function *)
+     (*  Some l ->*)
+        let q0 =
+        M.And
+          (M.Sub
+            (M.Property
+              (false, M.RefineExact, ("refSort", ["position"]),
+                M.RefOf(M.RVar "uri0")
+               ),
+             M.VVar ("sort_position" ^ string_of_int n)),
+           M.Sub
+            (M.Property
+              (false, M.RefineExact, ("refSort", ["sort"]),
+                M.RefOf(M.RVar "uri0")),
+             M.VVar ("sort" ^ string_of_int n))) 
+        in
+       match cr_s with
+          Some [] -> M.True
+       | Some [(p,None,s)] -> q0
+             
+        | Some [(p,d,s)] ->
+                      M.And
+                        (q0,
+                         M.Sub
+                          (M.Property
+                            (false, M.RefineExact, ("refSort", ["depth"]),
+                             M.RefOf(M.RVar "uri0")),
+                           M.VVar ("sort_depth" ^ string_of_int n))) 
+             
+        | Some ((p,None,s)::tl) ->
+                           M.Or
+                            (q0,
+                             q_where_sort (n+1) (Some tl))
+             
+        | Some((p,d,s)::tl) ->
+                          M.Or
+                           (M.And
+                              (q0,
+                               M.Sub
+                                (M.Property
+                                  (false, M.RefineExact, ("refSort", ["depth"]),
+                                   M.RefOf(M.RVar "uri0")),
+                                 M.VVar ("sort_depth" ^ string_of_int n))),
+                            q_where_sort (n+1) (Some tl))
+        | None -> M.True
+   in
+           
+
+
+  
+   let q_where cr =
+     let (cr_o,cr_r,cr_s) = cr in
+     M.And(M.And(q_where_obj 1 cr_o, (q_where_rel 1 cr_r)), (q_where_sort 1 cr_s))     
+   
+       in
+  
+(* must restrictions *)   
+   
+   let build_select_obj (r, pos, dep) =
+     match dep with
+       None -> M.Select
+                 ("uri", 
+                  M.Relation (false, M.RefineExact, ("backPointer", []),
+                             M.Ref (M.Const [r]), [assign "p" "position"]),
+                  M.Ex ["uri"] 
+                  ((M.Sub (M.Const [pos], M.Record ("uri", in_path "p")))))
+     | Some dep -> let string_dep = string_of_int dep in
+                   M.Select
+                     ("uri", 
+                      M.Relation (false, M.RefineExact, ("backPointer", []),
+                                 M.Ref (M.Const [r]), [assign "p" "position";assign "d" "depth"]),
+                      M.Ex ["uri"] 
+                      (M.And
+                     ((M.Sub (M.Const [pos], M.Record ("uri", in_path "p"))),
+                     (M.Sub (M.Const [string_dep], M.Record ("uri", in_path "d"))))))  
+   in 
+  
+   let build_select_rel (pos, dep) = 
+     match dep with 
+       None -> M.Select                               
+                 ("uri", 
+                  M.Relation (true, M.RefineExact, ("refRel", []), M.Ref (M.Const [""]), [assign "p" "position";assign "d" "depth"]), 
+                  M.Ex ["uri"]
+                  (M.Sub (M.Const [pos], M.Record ("uri", in_path "p")))) 
+     | Some dep -> let string_dep = string_of_int dep in 
+                   M.Select                               
+                     ("uri", 
+                      M.Relation (true, M.RefineExact, ("refRel", []), M.Ref (M.Const [""]), [assign "p" "position";assign "d" "depth"]), 
+                      M.Ex ["uri"] 
+                      (M.And
+                     ((M.Sub (M.Const [pos], M.Record ("uri", in_path "p"))),
+                     (M.Sub (M.Const [string_dep], M.Record ("uri", in_path "d"))))))
+   in 
+
+   let build_select_sort (pos, dep, sor) =  
+     match dep with
+       None -> M.Select                               
+                 ("uri", 
+                  M.Relation (true, M.RefineExact, ("refSort", []), M.Ref (M.Const [""]), [assign "p" "position";assign "d" "depth";assign "s" "sort"]), 
+                  M.Ex ["uri"] 
+                  (M.And
+                 ((M.Sub (M.Const [pos], M.Record ("uri", in_path "p"))),
+                  (M.Sub (M.Const [sor], M.Record ("uri", in_path "s"))))))
+   
+     | Some dep -> let string_dep = string_of_int dep in
+                   M.Select                               
+                     ("uri", 
+                      M.Relation (true, M.RefineExact, ("refSort", []), M.Ref (M.Const [""]), [assign "p" "position";assign "d" "depth";assign "s" "sort"]), 
+                      M.Ex ["uri"] 
+                      (M.And
+                     ((M.And
+                     ((M.Sub (M.Const [pos], M.Record ("uri", in_path "p"))),
+                     (M.Sub (M.Const [string_dep], M.Record ("uri", in_path "d"))))),
+                      (M.Sub (M.Const [sor], M.Record ("uri", in_path "s"))))))
+   in 
+
+   let rec build_intersect_obj = function
+       []       -> M.Pattern (M.Const ["[.]*"])
+     | [hd]     -> build_select_obj hd
+     | hd :: tl -> M.Intersect (build_select_obj hd, build_intersect_obj tl)
+   in
+   
+   let rec build_intersect_rel = function
+       []       -> M.Ref(M.Const [])                      
+     | [hd]     -> build_select_rel hd
+     | hd :: tl -> M.Intersect (build_select_rel hd, build_intersect_rel tl)
+   in
+
+   let rec build_intersect_sort = function
+       []       -> M.Ref(M.Const [])                         
+     | [hd]     -> build_select_sort hd
+     | hd :: tl -> M.Intersect (build_select_sort hd, build_intersect_sort tl)
+   in
+   
+   let build_intersect = function
+(*      let tostring_sort (a,b,c) = 
+        let b1 = string_of_int b in 
+          (a,b1,c)
+      in
+      let tostring_rel (a,b) = 
+        let b1 = string_of_int b in 
+          (a,b1)
+      in*)
+
+(*      let (l1,l2,l3) = must in
+      match (l1,l2,l3) with *)
+        l1,[],[] -> build_intersect_obj l1
+      |        [],l2,[] -> (*let lrel = List.map tostring_rel l2 in*)
+                      build_intersect_rel l2
+      | [],[],l3 ->(* let lsort = List.map tostring_sort l3 in*)
+                      build_intersect_sort l3
+      | l1,l2,[] -> (*let lrel = List.map tostring_rel l2 in*)
+                      M.Intersect (build_intersect_obj l1, build_intersect_rel l2)
+      | l1,[],l3 ->(* let lsort = List.map tostring_sort l3 in               *)
+                      M.Intersect (build_intersect_obj l1, build_intersect_sort l3)
+      | [],l2,l3 ->(* let lrel = List.map tostring_rel l2 in
+                    let lsort = List.map tostring_sort l3 in*)
+                     M.Intersect (build_intersect_rel l2, build_intersect_sort l3)
+      | l1,l2,l3 ->(* let lrel = List.map tostring_rel l2 in
+             let lsort = List.map tostring_sort l3 in *)                         
+              M.Intersect (M.Intersect (build_intersect_obj l1, build_intersect_rel l2), build_intersect_sort l3)
+   in  
+
    let q_in = build_intersect must_use in
-   let q_select = M.Select ("uri0", q_in, q_where) in
-   let universe = M.Const (List.map uri_of_entry can_use) 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
-print_endline ("### " ^ MQueryUtil.text_of_query q_let_p) ; flush stdout;
-   execute_query q_let_p
+   let q_select = M.Select ("uri0", q_in, q_where can_use) in
+
+(* variables for can restrictions *)
+
+   let q_let_u = M.LetVVar ("universe", M.Const universe, q_select) in
+   
+   let rec q_let_s sor n =
+     match sor with
+       [] -> q_let_u
+     | [s] -> M.LetVVar ("sort" ^ (string_of_int n), M.Const [s], q_let_u)
+     | s::tl -> M.LetVVar ("sort" ^ (string_of_int n), M.Const [s], q_let_s tl (n+1))
+   in
+
+(*   let q_let_s = M.LetVVar ("sorts", M.Const sor, q_let_u) in *)
+   
+   let rec q_let_ds sdep n =
+     match sdep with
+       [] 
+     | [None] -> q_let_s sor 1  
+     | (None)::tl -> q_let_ds tl (n+1)
+     | [Some d] -> M.LetVVar ("sort_depth" ^ (string_of_int n), M.Const [(string_of_int d)], q_let_s sor 1)
+     | (Some d)::tl -> M.LetVVar ("sort_depth" ^ (string_of_int n), M.Const [(string_of_int d)], q_let_ds tl (n+1))
+   in  
+   
+(*   let q_let_ds = M.LetVVar ("sort_depths", M.Const sdep, q_let_s) in   *)
+   
+   let rec q_let_dr rdep n =
+     match rdep with
+       [] 
+     | [None] -> q_let_ds sdep 1 
+     | (None)::tl -> q_let_dr tl (n+1)
+     | [Some d] -> M.LetVVar ("rel_depth" ^ (string_of_int n), M.Const [(string_of_int d)], q_let_ds sdep 1)
+     | (Some d)::tl -> M.LetVVar ("rel_depth" ^ (string_of_int n), M.Const [(string_of_int d)], q_let_dr tl (n+1))
+   in
+  
+   
+   (*let q_let_dr = M.LetVVar ("rel_depths", M.Const rdep, q_let_ds) in*)
+   
+   let rec q_let_do odep n =
+     match odep with
+       [] 
+     | [None] -> q_let_dr rdep 1
+     | (None)::tl -> q_let_do tl (n+1)  
+     |  [Some d] -> M.LetVVar ("obj_depth" ^ (string_of_int n), M.Const [(string_of_int d)], q_let_dr rdep 1)
+     | (Some d)::tl -> M.LetVVar ("obj_depth" ^ (string_of_int n), M.Const [(string_of_int d)], q_let_do tl (n+1))
+   in
+
+
+(*   let q_let_do = M.LetVVar ("obj_depths", M.Const odep, q_let_dr) in  *)
+   
+   
+   let rec q_let_ps spos n =
+     match spos with
+       [] -> q_let_do odep 1
+     | [p] -> M.LetVVar ("sort_position" ^ (string_of_int n), M.Const [p], q_let_do odep 1)
+     | p::tl -> M.LetVVar ("sort_position" ^ (string_of_int n), M.Const [p], q_let_ps tl (n+1))
+   in
+   
+   
+(*   let q_let_ps = M.LetVVar ("sort_positions", M.Const spos, q_let_do) in *)
+   
+   
+   let rec q_let_pr rpos n =
+     match rpos with
+       [] -> q_let_ps spos 1
+     | [p] -> M.LetVVar ("rel_position" ^ (string_of_int n), M.Const [p], q_let_ps spos 1)
+     | p::tl -> M.LetVVar ("rel_position" ^ (string_of_int n), M.Const [p], q_let_pr tl (n+1))
+   in
+   
+   
+   
+(*   let q_let_pr = M.LetVVar ("rel_positions", M.Const rpos, q_let_ps) in *)
+
+   let rec q_let_po opos n =
+     match opos with
+       [] -> q_let_pr rpos 1
+     | [p] -> M.LetVVar ("obj_position" ^ (string_of_int n), M.Const [p], q_let_pr rpos 1)
+     | p::tl -> M.LetVVar ("obj_position" ^ (string_of_int n), M.Const [p], q_let_po tl (n+1))
+   in
+   
+   (*let q_let_po = M.LetVVar ("obj_positions", M.Const opos, q_let_pr) in*)
+
+print_endline "### ";  MQueryUtil.text_of_query print_string (q_let_po opos 1) "\n"; flush stdout;
+   execute_query (q_let_po opos 1)