]> matita.cs.unibo.it Git - helm.git/commitdiff
moved mquery generation in ../ocaml/mquery_generator/
authorStefano Zacchiroli <zack@upsilon.cc>
Thu, 20 Feb 2003 17:21:52 +0000 (17:21 +0000)
committerStefano Zacchiroli <zack@upsilon.cc>
Thu, 20 Feb 2003 17:21:52 +0000 (17:21 +0000)
helm/gTopLevel/mQueryGenerator.ml [deleted file]
helm/gTopLevel/mQueryGenerator.mli [deleted file]
helm/gTopLevel/mQueryLevels.ml [deleted file]
helm/gTopLevel/mQueryLevels.mli [deleted file]
helm/gTopLevel/mQueryLevels2.ml [deleted file]
helm/gTopLevel/mQueryLevels2.mli [deleted file]

diff --git a/helm/gTopLevel/mQueryGenerator.ml b/helm/gTopLevel/mQueryGenerator.ml
deleted file mode 100644 (file)
index ed52e55..0000000
+++ /dev/null
@@ -1,554 +0,0 @@
-(* Copyright (C) 2000, HELM Team.
- * 
- * This file is part of HELM, an Hypertextual, Electronic
- * Library of Mathematics, developed at the Computer Science
- * Department, University of Bologna, Italy.
- * 
- * HELM is free software; you can redistribute it and/or
- * modify it under the terms of the GNU General Public License
- * as published by the Free Software Foundation; either version 2
- * of the License, or (at your option) any later version.
- * 
- * HELM is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with HELM; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
- * MA  02111-1307, USA.
- * 
- * For details, see the HELM World-Wide-Web page,
- * http://cs.unibo.it/helm/.
- *)
-
-(******************************************************************************)
-(*                                                                            *)
-(*                               PROJECT HELM                                 *)
-(*                                                                            *)
-(*                     Ferruccio Guidi <fguidi@cs.unibo.it>                   *)
-(*                                 30/04/2002                                 *)
-(*                                                                            *)
-(*                                                                            *)
-(******************************************************************************)
-
-(* 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"
-
-let query_num = ref 1
-
-let log_file = ref ""
-
-let confirm_query = ref (fun _ -> true)
-
-let info = ref []
-
-let set_log_file f = 
-   log_file := f
-
-let set_confirm_query f =
-   confirm_query := f
-
-let get_query_info () = ! info
-
-let execute_query query =
-   let module Util = MQueryUtil in
-   let mode = [Open_wronly; Open_append; Open_creat; Open_text] in
-   let perm = 64 * 6 + 8 * 6 + 4 in
-   let time () =
-      let lt = Unix.localtime (Unix.time ()) in
-      "NEW LOG: " ^
-      string_of_int (lt.Unix.tm_mon + 1) ^ "-" ^
-      string_of_int (lt.Unix.tm_mday + 1) ^ "-" ^
-      string_of_int (lt.Unix.tm_year + 1900) ^ " " ^
-      string_of_int (lt.Unix.tm_hour) ^ ":" ^
-      string_of_int (lt.Unix.tm_min) ^ ":" ^
-      string_of_int (lt.Unix.tm_sec) 
-   in
-   let log q r = 
-      let och = open_out_gen mode perm ! log_file in
-      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 =
-      let r = Mqint.execute q in    
-      if ! log_file <> "" then log q r; 
-      info := string_of_int ! query_num :: ! info;
-      incr query_num;
-      r
-   in 
-   if ! confirm_query query then execute query else raise Discard
-                          
-(* Query building functions  ************************************************)   
-
-let locate s =
-   let module M = MathQL in
-   let q =
-    M.Ref (M.Property true M.RefineExact ("objectName", []) (M.Const [s]))
-   in
-    execute_query q
-
-let searchPattern must_use can_use =    
-   let module M = MathQL in
-   let in_path s = (s, []) in
-   let assign v p = (in_path v, in_path p) in 
-  
-(* 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 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)
diff --git a/helm/gTopLevel/mQueryGenerator.mli b/helm/gTopLevel/mQueryGenerator.mli
deleted file mode 100644 (file)
index b1db111..0000000
+++ /dev/null
@@ -1,64 +0,0 @@
-(* Copyright (C) 2000, HELM Team.
- * 
- * This file is part of HELM, an Hypertextual, Electronic
- * Library of Mathematics, developed at the Computer Science
- * Department, University of Bologna, Italy.
- * 
- * HELM is free software; you can redistribute it and/or
- * modify it under the terms of the GNU General Public License
- * as published by the Free Software Foundation; either version 2
- * of the License, or (at your option) any later version.
- * 
- * HELM is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with HELM; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
- * MA  02111-1307, USA.
- * 
- * For details, see the HELM World-Wide-Web page,
- * http://cs.unibo.it/helm/.
- *)
-
-(******************************************************************************)
-(*                                                                            *)
-(*                               PROJECT HELM                                 *)
-(*                                                                            *)
-(*                     Ferruccio Guidi <fguidi@cs.unibo.it>                   *)
-(*                                 30/04/2002                                 *)
-(*                                                                            *)
-(*                                                                            *)
-(******************************************************************************)
-
-exception Discard  
-
-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)
-
-
-
-val set_log_file      : string -> unit
-
-(* the callback function must return false iff the query must be skipped *)
-val set_confirm_query : (MathQL.query -> bool) -> unit
-
-val execute_query     : MathQL.query -> MathQL.result
-
-val locate            : string -> MathQL.result
-
-val searchPattern     : must_restrictions -> only_restrictions -> MathQL.result
-
-val get_query_info    : unit -> string list
diff --git a/helm/gTopLevel/mQueryLevels.ml b/helm/gTopLevel/mQueryLevels.ml
deleted file mode 100644 (file)
index 977638d..0000000
+++ /dev/null
@@ -1,148 +0,0 @@
-(* Copyright (C) 2000, HELM Team.
- * 
- * This file is part of HELM, an Hypertextual, Electronic
- * Library of Mathematics, developed at the Computer Science
- * Department, University of Bologna, Italy.
- * 
- * HELM is free software; you can redistribute it and/or
- * modify it under the terms of the GNU General Public License
- * as published by the Free Software Foundation; either version 2
- * of the License, or (at your option) any later version.
- * 
- * HELM is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with HELM; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
- * MA  02111-1307, USA.
- * 
- * For details, see the HELM World-Wide-Web page,
- * http://cs.unibo.it/helm/.
- *)
-
-(******************************************************************************)
-(*                                                                            *)
-(*                               PROJECT HELM                                 *)
-(*                                                                            *)
-(*                     Ferruccio Guidi <fguidi@cs.unibo.it>                   *)
-(*                                 30/04/2002                                 *)
-(*                                                                            *)
-(*                                                                            *)
-(******************************************************************************)
-
-let levels_of_term metasenv context term =
-   let module TC = CicTypeChecker in
-   let module Red = CicReduction in
-   let module Util = MQueryUtil in
-   let degree t =
-      let rec degree_aux = function
-         | Cic.Sort _         -> 1 
-         | Cic.Cast (u, _)    -> degree_aux u
-         | Cic.Prod (_, _, t) -> degree_aux t
-         | _                  -> 2
-      in 
-      let u = TC.type_of_aux' metasenv context t in
-      degree_aux (Red.whd context u)
-   in
-   let entry_eq (s1, b1, v1) (s2, b2, v2) =
-      s1 = s2 && b1 = b2 
-   in
-   let rec entry_in e = function
-      | []           -> [e]
-      | head :: tail -> 
-         head :: if entry_eq head e then tail else entry_in e tail
-   in
-   let inspect_uri main l uri tc v term =
-      let d = degree term in 
-      entry_in (Util.string_of_uriref (uri, tc), main, 2 * v + d - 1) l 
-   in
-   let rec inspect_term main l v term = match term with
-        Cic.Rel _                        -> l
-      | Cic.Meta _                       -> l
-      | Cic.Sort _                       -> l 
-      | Cic.Implicit                     -> l 
-      | Cic.Var (u,exp_named_subst)      ->
-         let l' = inspect_uri main l u [] v term in
-          inspect_exp_named_subst l' (v+1) exp_named_subst
-      | Cic.Const (u,exp_named_subst)    ->
-         let l' = inspect_uri main l u [] v term in
-          inspect_exp_named_subst l' (v+1) exp_named_subst
-      | Cic.MutInd (u, t, exp_named_subst) ->
-         let l' = inspect_uri main l u [t] v term in
-          inspect_exp_named_subst l' (v+1) exp_named_subst
-      | Cic.MutConstruct (u, t, c, exp_named_subst)    ->
-         let l' = inspect_uri main l u [t; c] v term in
-          inspect_exp_named_subst l' (v+1) exp_named_subst
-      | Cic.Cast (uu, _)                 -> 
-         inspect_term main l v uu
-      | Cic.Prod (_, uu, tt)             ->
-         let luu = inspect_term false l (v + 1) uu in
-         inspect_term main luu (v + 1) tt         
-      | Cic.Lambda (_, uu, tt)           ->
-         let luu = inspect_term false l (v + 1) uu in
-         inspect_term false luu (v + 1) tt 
-      | Cic.LetIn (_, uu, tt)            ->
-         let luu = inspect_term false l (v + 1) uu in
-         inspect_term false luu (v + 1) tt
-      | Cic.Appl m                       -> inspect_list main l true v m 
-      | Cic.MutCase (u, t, tt, uu, m) -> 
-         let lu = inspect_uri main l u [t] (v + 1) term in
-         let ltt = inspect_term false lu (v + 1) tt in
-         let luu = inspect_term false ltt (v + 1) uu in
-         inspect_list main luu false (v + 1) m
-      | Cic.Fix (_, m)                   -> inspect_ind l (v + 1) m 
-      | Cic.CoFix (_, m)                 -> inspect_coind l (v + 1) m 
-   and inspect_list main l head v = function
-      | []      -> l
-      | tt :: m -> 
-         let ltt = inspect_term main l (if head then v else v + 1) tt in
-         inspect_list false ltt false v m
-   and inspect_exp_named_subst l v = function
-        []      -> l
-      | (_,t) :: tl -> 
-         let l' = inspect_term false l v t in
-          inspect_exp_named_subst l' v tl
-   and inspect_ind l v = function
-      | []                  -> l
-      | (_, _, tt, uu) :: m ->  
-         let ltt = inspect_term false l v tt in
-         let luu = inspect_term false ltt v uu in
-         inspect_ind luu v m
-   and inspect_coind l v = function
-      | []               -> l
-      | (_, tt, uu) :: m ->
-         let ltt = inspect_term false l v tt in
-         let luu = inspect_term false ltt v uu in
-         inspect_coind luu v m
-   in
-   let rec inspect_backbone = function
-      | Cic.Cast (uu, _)      -> inspect_backbone uu
-      | Cic.Prod (_, _, tt)   -> inspect_backbone tt                
-      | Cic.LetIn (_, uu, tt) -> inspect_backbone tt
-      | t                     -> inspect_term true [] 0 t
-   in 
-   inspect_backbone term  
-
-let out_restr e c t =   
-  let can = levels_of_term e c t in  (* can restrictions *)
-prerr_endline "";
-prerr_endline
- ("#### IN LEVELS @@@@ lunghezza can: " ^ string_of_int (List.length can));
-prerr_endline "";
-(*  let rest = restrict level levels in   *)
-  let uri_pos (u,b,v) = (u,b) in
-  let can_use = List.map uri_pos can in
-  let lofl (u,b,v) = [(u,b)] in
-  let rec organize_restr rlist prev_r= 
-    match rlist with
-      [] -> []
-    | r::tl ->let curr_r = r@prev_r in
-                curr_r::(organize_restr tl curr_r)
-  in
-  let mrest = List.map lofl can in
-  let must_use = organize_restr mrest [] in (* must restrictions *)
-  (must_use,can_use)
-;;
diff --git a/helm/gTopLevel/mQueryLevels.mli b/helm/gTopLevel/mQueryLevels.mli
deleted file mode 100644 (file)
index 5b214b7..0000000
+++ /dev/null
@@ -1,36 +0,0 @@
-(* Copyright (C) 2000, HELM Team.
- * 
- * This file is part of HELM, an Hypertextual, Electronic
- * Library of Mathematics, developed at the Computer Science
- * Department, University of Bologna, Italy.
- * 
- * HELM is free software; you can redistribute it and/or
- * modify it under the terms of the GNU General Public License
- * as published by the Free Software Foundation; either version 2
- * of the License, or (at your option) any later version.
- * 
- * HELM is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with HELM; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
- * MA  02111-1307, USA.
- * 
- * For details, see the HELM World-Wide-Web page,
- * http://cs.unibo.it/helm/.
- *)
-
-(******************************************************************************)
-(*                                                                            *)
-(*                               PROJECT HELM                                 *)
-(*                                                                            *)
-(*                     Ferruccio Guidi <fguidi@cs.unibo.it>                   *)
-(*                                 30/04/2002                                 *)
-(*                                                                            *)
-(*                                                                            *)
-(******************************************************************************)
-
-val out_restr: Cic.metasenv -> Cic.context -> Cic.term -> ( ((string * bool) list) list * (string * bool) list)
diff --git a/helm/gTopLevel/mQueryLevels2.ml b/helm/gTopLevel/mQueryLevels2.ml
deleted file mode 100644 (file)
index 968d2a3..0000000
+++ /dev/null
@@ -1,200 +0,0 @@
-(* Copyright (C) 2000, HELM Team.
- * 
- * This file is part of HELM, an Hypertextual, Electronic
- * Library of Mathematics, developed at the Computer Science
- * Department, University of Bologna, Italy.
- * 
- * HELM is free software; you can redistribute it and/or
- * modify it under the terms of the GNU General Public License
- * as published by the Free Software Foundation; either version 2
- * of the License, or (at your option) any later version.
- * 
- * HELM is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with HELM; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
- * MA  02111-1307, USA.
- * 
- * For details, see the HELM World-Wide-Web page,
- * http://cs.unibo.it/helm/.
- *)
-
-(******************************************************************************)
-(*                                                                            *)
-(*                               PROJECT HELM                                 *)
-(*                                                                            *)
-(*                Claudio Sacerdoti Coen <sacerdot@cs.unibo.it>               *)
-(*                                 02/12/2002                                 *)
-(*                                                                            *)
-(*                            Missing description                             *)
-(*                                                                            *)
-(******************************************************************************)
-
-type classification =
-   Backbone of int
- | Branch of int
- | InConclusion
- | InHypothesis
-;;
-
-let soften_classification =
- function
-    Backbone _ -> InConclusion
-  | Branch _ -> InHypothesis
-  | k -> k
-;;
-
-let (!!) =
- function
-    Backbone n ->
-     "http://www.cs.unibo.it/helm/schemas/schema-helm#MainConclusion", Some n
-  | Branch n ->
-     "http://www.cs.unibo.it/helm/schemas/schema-helm#MainHypothesis", Some n
-  | InConclusion ->
-     "http://www.cs.unibo.it/helm/schemas/schema-helm#InConclusion", None
-  | InHypothesis ->
-     "http://www.cs.unibo.it/helm/schemas/schema-helm#InHypothesis", None
-;;
-
-let (@@) (l1,l2,l3) (l1',l2',l3') =
- let merge l1 l2 =
-  List.fold_left (fun i t -> if List.mem t l2 then i else t::i) l2 l1
- in
-  merge l1 l1', merge l2 l2', merge l3 l3'
-;;
-
-let get_constraints term =
- let module U = UriManager in
- let module C = Cic in
-  let rec process_type_aux kind =
-   function
-      C.Var (uri,expl_named_subst) ->
-       let kind',depth = !!kind in
-        ([UriManager.string_of_uri uri,kind',depth],[],[]) @@
-          (process_type_aux_expl_named_subst kind expl_named_subst)
-    | C.Rel _ ->
-       let kind',depth = !!kind in
-        (match depth with
-            None -> [],[],[]
-          | Some d -> [],[kind',Some d],[])
-    | C.Sort s ->
-       (match kind with
-           Backbone _
-         | Branch _ ->
-            let s' =
-             match s with
-                Cic.Prop ->
-                 "http://www.cs.unibo.it/helm/schemas/schema-helm#Prop"
-              | Cic.Set ->
-                 "http://www.cs.unibo.it/helm/schemas/schema-helm#Set"
-              | Cic.Type ->
-                 "http://www.cs.unibo.it/helm/schemas/schema-helm#Type"
-            in
-             let kind',depth = !!kind in
-              (match depth with
-                  None -> assert false
-                | Some d -> [],[],[kind',Some d,s'])
-         | _ -> [],[],[])
-    | C.Meta _
-    | C.Implicit -> assert false
-    | C.Cast (te,_) ->
-       (* type ignored *)
-       process_type_aux kind te
-    | C.Prod (_,sou,ta) ->
-       let (source_kind,target_kind) =
-        match kind with
-           Backbone n -> (Branch 0, Backbone (n+1))
-         | Branch n -> (InHypothesis, Branch (n+1))
-         | k -> (k,k)
-       in
-        process_type_aux source_kind sou @@
-        process_type_aux target_kind ta
-    | C.Lambda (_,sou,ta) ->
-        let kind' = soften_classification kind in
-         process_type_aux kind' sou @@
-         process_type_aux kind' ta
-    | C.LetIn (_,te,ta)->
-       let kind' = soften_classification kind in
-        process_type_aux kind' te @@
-        process_type_aux kind ta
-    | C.Appl (he::tl) ->
-       let kind' = soften_classification kind in
-        process_type_aux kind he @@
-        List.fold_left (fun i t -> i @@ process_type_aux kind' t) ([],[],[]) tl
-    | C.Appl _ -> assert false
-    | C.Const (uri,_) ->
-       let kind',depth = !!kind in
-        [UriManager.string_of_uri uri,kind',depth],[],[]
-    | C.MutInd (uri,typeno,expl_named_subst) ->
-       let kind',depth = !!kind in
-       ([U.string_of_uri uri ^ "#xpointer(1/" ^ string_of_int (typeno + 1) ^
-          ")", kind', depth],[],[]) @@
-         (process_type_aux_expl_named_subst kind expl_named_subst)
-    | C.MutConstruct (uri,typeno,consno,expl_named_subst) ->
-       let kind',depth = !!kind in
-        ([U.string_of_uri uri ^ "#xpointer(1/" ^ string_of_int (typeno + 1) ^
-          "/" ^ string_of_int consno ^ ")",kind',depth],[],[]) @@
-          (process_type_aux_expl_named_subst kind expl_named_subst)
-    | C.MutCase (_,_,_,term,patterns) ->
-       (* outtype ignored *)
-       let kind' = soften_classification kind in
-        process_type_aux kind' term @@
-        List.fold_left (fun i t -> i @@ process_type_aux kind' t)
-         ([],[],[]) patterns
-    | C.Fix (_,funs) ->
-       let kind' = soften_classification kind in
-        List.fold_left
-         (fun i (_,_,bo,ty) ->
-           i @@
-            process_type_aux kind' bo @@
-            process_type_aux kind' ty
-         ) ([],[],[]) funs
-    | C.CoFix (_,funs) ->
-       let kind' = soften_classification kind in
-        List.fold_left
-         (fun i (_,bo,ty) ->
-           i @@
-            process_type_aux kind' bo @@
-            process_type_aux kind' ty
-         ) ([],[],[]) funs
- and process_type_aux_expl_named_subst kind =
-  List.fold_left
-   (fun i (_,t) -> i @@ (process_type_aux (soften_classification kind) t))
-   ([],[],[])
-in
- let obj_constraints,rel_constraints,sort_constraints =
-  process_type_aux (Backbone 0) (CicMiniReduction.letin_nf term)
- in
-  (obj_constraints,rel_constraints,sort_constraints)
-;;
-
-(*CSC: Debugging only *)
-let get_constraints term =
- let res = get_constraints term in
- let (objs,rels,sorts) = res in
-  prerr_endline "Constraints on objs:" ;
-  List.iter
-   (function (s1,s2,n) ->
-     prerr_endline
-      (s1 ^ " " ^ s2 ^ " " ^
-        match n with None -> "NULL" | Some n -> string_of_int n)
-   ) objs ;
-  prerr_endline "Constraints on Rels:" ;
-  List.iter
-   (function (s,n) ->
-     prerr_endline
-      (s ^ " " ^ (match n with Some n' -> string_of_int n' | None -> "NULL"))
-   ) rels ;
-  prerr_endline "Constraints on Sorts:" ;
-  List.iter
-   (function (s1,n,s2) ->
-     prerr_endline
-      (s1 ^ " " ^ (match n with Some n' -> string_of_int n' | None -> "NULL") ^
-        " " ^ s2)
-   ) sorts ;
-  res
-;;
diff --git a/helm/gTopLevel/mQueryLevels2.mli b/helm/gTopLevel/mQueryLevels2.mli
deleted file mode 100644 (file)
index 805f106..0000000
+++ /dev/null
@@ -1,36 +0,0 @@
-(* Copyright (C) 2000, HELM Team.
- * 
- * This file is part of HELM, an Hypertextual, Electronic
- * Library of Mathematics, developed at the Computer Science
- * Department, University of Bologna, Italy.
- * 
- * HELM is free software; you can redistribute it and/or
- * modify it under the terms of the GNU General Public License
- * as published by the Free Software Foundation; either version 2
- * of the License, or (at your option) any later version.
- * 
- * HELM is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with HELM; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
- * MA  02111-1307, USA.
- * 
- * For details, see the HELM World-Wide-Web page,
- * http://cs.unibo.it/helm/.
- *)
-
-(******************************************************************************)
-(*                                                                            *)
-(*                               PROJECT HELM                                 *)
-(*                                                                            *)
-(*                     Ferruccio Guidi <fguidi@cs.unibo.it>                   *)
-(*                                 30/04/2002                                 *)
-(*                                                                            *)
-(*                                                                            *)
-(******************************************************************************)
-
-val get_constraints: Cic.term -> MQueryGenerator.must_restrictions