Now MQueryGenerator generates the query and MQueryLevels produces the restrictions...

diff --git a/helm/gTopLevel/.depend b/helm/gTopLevel/.depend
index 7dce2d61fc542e07f05ea9151214926acbf082f8..fa76e97ae76d8f9a53f4334c3a6328013325e3e2 100644 (file)
--- a/helm/gTopLevel/.depend
+++ b/helm/gTopLevel/.depend
@@ -61,9 +61,11 @@ sequentPp.cmo: cic2Xml.cmi cic2acic.cmi proofEngine.cmi sequentPp.cmi
 sequentPp.cmx: cic2Xml.cmx cic2acic.cmx proofEngine.cmx sequentPp.cmi 
 mQueryLevels.cmo: mQueryLevels.cmi 
 mQueryLevels.cmx: mQueryLevels.cmi 
-mQueryGenerator.cmo: mQueryGenerator.cmi 
-mQueryGenerator.cmx: mQueryGenerator.cmi 
+mQueryGenerator.cmo: mQueryLevels.cmi mQueryGenerator.cmi 
+mQueryGenerator.cmx: mQueryLevels.cmx mQueryGenerator.cmi 
 gTopLevel.cmo: cic2Xml.cmi cic2acic.cmi logicalOperations.cmi \
-    mQueryGenerator.cmi proofEngine.cmi sequentPp.cmi xml2Gdome.cmi 
+    mQueryGenerator.cmi mQueryLevels.cmi proofEngine.cmi sequentPp.cmi \
+    xml2Gdome.cmi 
 gTopLevel.cmx: cic2Xml.cmx cic2acic.cmx logicalOperations.cmx \
-    mQueryGenerator.cmx proofEngine.cmx sequentPp.cmx xml2Gdome.cmx 
+    mQueryGenerator.cmx mQueryLevels.cmx proofEngine.cmx sequentPp.cmx \
+    xml2Gdome.cmx 

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index 0546d02b50f7feb12dd477498afbfedc31b3fbb1..5ad73d2be17dda7a9b151b7afa030dac88693756 100644 (file)
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -65,8 +65,8 @@ let prooffile = "/home/tassi/miohelm/tmp/currentproof";;
 let prooffiletype = "/home/tassi/miohelm/tmp/currentprooftype";;
 *)
 
-let prooffile = "/public/sacerdot/currentproof";;
-let prooffiletype = "/public/sacerdot/currentprooftype";;
+let prooffile = "/public/natile/currentproof";;
+let prooffiletype = "/public/natile/currentprooftype";;
 
 (*CSC: the getter should handle the innertypes, not the FS *)
 
@@ -75,8 +75,8 @@ let innertypesfile = "/home/tassi/miohelm/tmp/innertypes";;
 let constanttypefile = "/home/tassi/miohelm/tmp/constanttype";;
 *)
 
-let innertypesfile = "/public/sacerdot/innertypes";;
-let constanttypefile = "/public/sacerdot/constanttype";;
+let innertypesfile = "/public/natile/innertypes";;
+let constanttypefile = "/public/natile/constanttype";;
 
 let empty_id_to_uris = ([],function _ -> None);;
 
@@ -2008,7 +2008,10 @@ let searchPattern () =
         None -> ()
       | Some metano ->
          let (_, ey ,ty) = List.find (function (m,_,_) -> m=metano) metasenv in
-          let result = MQueryGenerator.searchPattern metasenv ey ty level in
+          let list_of_must,can = MQueryLevels.out_restr metasenv ey ty in
+         let len = List.length list_of_must in
+         let must = if level < len then List.nth list_of_must level else can in
+         let result = MQueryGenerator.searchPattern metasenv ey ty must can in
           let uris =
            List.map
             (function uri,_ ->

diff --git a/helm/gTopLevel/mQueryGenerator.ml b/helm/gTopLevel/mQueryGenerator.ml
index 843eb96c050ee80174ca5c4ba630674daaccd15c..c925e27a69cecbd62d53041bd5a8a54b78952197 100644 (file)
--- a/helm/gTopLevel/mQueryGenerator.ml
+++ b/helm/gTopLevel/mQueryGenerator.ml
@@ -96,7 +96,7 @@ let locate s =
    in
     execute_query q
 
-let searchPattern e c t level =
+let searchPattern e c t must_use can_use =
    let module M = MathQL in
    let module L = MQueryLevels in
    let mainConclusion =
@@ -121,14 +121,15 @@ let searchPattern e c t level =
        ),
        M.VVar "universe"
      ) in
-   let uri_of_entry (r, b, v) = r in
-   let rec restrict level = function
+   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, v) =
+   in*)
+   let build_select (r, b) =
+    print_endline (">>>>LA URI: "^r);
     let pos = if b then mainConclusion else inConclusion in
       M.Select
        ("uri", 
@@ -140,13 +141,14 @@ let searchPattern e c t level =
       | [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 levels = L.levels_of_term e c t in
    let rest = restrict level levels in
-   info := [string_of_int (List.length rest)];
-   let q_in = build_intersect rest in
+   info := [string_of_int (List.length rest)];*)
+   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 levels) 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
-prerr_endline ("### " ^ MQueryUtil.text_of_query q_let_p) ;
+print_endline ("### " ^ MQueryUtil.text_of_query q_let_p) ; flush stdout;
    execute_query q_let_p

diff --git a/helm/gTopLevel/mQueryGenerator.mli b/helm/gTopLevel/mQueryGenerator.mli
index 68c2ea2570859d7600719949b161d04fc3e2e729..8723f9c9f002cb52559bdec40fa57b1cb754a564 100644 (file)
--- a/helm/gTopLevel/mQueryGenerator.mli
+++ b/helm/gTopLevel/mQueryGenerator.mli
@@ -44,6 +44,6 @@ val execute_query     : MathQL.query -> MathQL.result
 
 val locate            : string -> MathQL.result
 
-val searchPattern     : Cic.metasenv -> Cic.context -> Cic.term -> int -> MathQL.result
+val searchPattern     : Cic.metasenv -> Cic.context -> Cic.term -> (string * bool) list -> (string * bool) list -> MathQL.result
 
 val get_query_info    : unit -> string list

diff --git a/helm/gTopLevel/mQueryLevels.ml b/helm/gTopLevel/mQueryLevels.ml
index f50d94c2c4d62acdd8768bda3a0bc503910d2420..ecadbd84bf48898aaf89d97cbcb8441e04ca1893 100644 (file)
--- a/helm/gTopLevel/mQueryLevels.ml
+++ b/helm/gTopLevel/mQueryLevels.ml
@@ -141,3 +141,32 @@ let string_of_levels l sep =
    in
    levels_out l
 
+
+let out_restr e c t =   
+(*  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 can = levels_of_term e c t in  (* can restrictions *)
+print_endline "";
+         print_string "#### IN LEVELS @@@@ lunghezza can:";
+         print_int (List.length can); flush stdout;
+         print_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
index bc1dc74149fa03284c1960b1485eba58511b964b..82fb7c69998d4d56d67ca5f6b7accc19462b51fd 100644 (file)
--- a/helm/gTopLevel/mQueryLevels.mli
+++ b/helm/gTopLevel/mQueryLevels.mli
@@ -33,8 +33,14 @@
 (*                                                                            *)
 (******************************************************************************)
 
+(*type can_restrictions = (string * bool) list
+
+type must_restrictions = ((string * bool) list) list*)
+
 type levels_spec = (string * bool * int) list
 
-val levels_of_term    : Cic.metasenv -> Cic.context -> Cic.term -> levels_spec
+val levels_of_term: Cic.metasenv -> Cic.context -> Cic.term -> levels_spec
+
+val out_restr: Cic.metasenv -> Cic.context -> Cic.term -> ( ((string * bool) list) list * (string * bool) list)
 
 val string_of_levels  : levels_spec -> string -> string

diff --git a/helm/gTopLevel/topLevel/topLevel.ml b/helm/gTopLevel/topLevel/topLevel.ml
index 4825c5b36c28a7f7ab47e2b679117797f674b560..cb7c7fca161eda84702293a64c61c0dc6144e761 100644 (file)
--- a/helm/gTopLevel/topLevel/topLevel.ml
+++ b/helm/gTopLevel/topLevel/topLevel.ml
@@ -120,7 +120,10 @@ let mbackward n m l =
            if Mqint.get_stat () then 
               print_string ("? " ^ CicPp.ppterm term ^ nl);
            let t0 = Sys.time () in
-            let r = Gen.searchPattern [] [] term level in
+           let list_of_must,can = MQueryLevels.out_restr [] [] term in
+           let len = List.length list_of_must in
+           let must = if level < len then List.nth list_of_must level else can in
+           let r = Gen.searchPattern [] [] term must can in
            let t1 = Sys.time () -. t0 in
            let info = Gen.get_query_info () in
            let num = List.nth info 0 in