* mQueryLevel2.get_constraints now gives back only the "must" constraints.

* the "refine constraints" interface has been improved. It can now handle
  also constraints on Sorts and constants.

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index 890f5d75fd4071f5482c5fd00dfec2e530ef669c..2e9c702dcef5724c8402f0410acd4133595bcf9d 100644 (file)
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -2414,14 +2414,13 @@ let show_query_results results =
   window#show ()
 ;;
 
-let
- refine_constraints (must_obj,must_rel,must_sort) (only_obj,only_rel,only_sort)
-=
+let refine_constraints (must_obj,must_rel,must_sort) =
  let chosen = ref false in
  let use_only = ref false in
  let window =
   GWindow.window
-   ~modal:true ~title:"Constraints refinement." ~border_width:2 () in
+   ~modal:true ~title:"Constraints refinement."
+   ~width:800 ~border_width:2 () in
  let vbox = GPack.vbox ~packing:window#add () in
  let hbox =
   GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
@@ -2431,23 +2430,32 @@ let
    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
  let onlyb =
   GButton.toggle_button ~label:"Enforce \"only\" constraints"
-   ~active:false ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5)
-   ()
+   ~active:false ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) ()
  in
   ignore
    (onlyb#connect#toggled (function () -> use_only := onlyb#active)) ;
+ (* Notebook for the constraints choice *)
+ let notebook =
+  GPack.notebook ~scrollable:true
+   ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in
+ (* Rel constraints *)
+ let label =
+  GMisc.label
+   ~text: "Constraints on Rels" () in
+ let vbox' =
+  GPack.vbox ~packing:(notebook#append_page ~tab_label:label#coerce)
+   () in
  let hbox =
-  GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
+  GPack.hbox ~packing:(vbox'#pack ~expand:false ~fill:false ~padding:5) () in
  let lMessage =
   GMisc.label
    ~text: "You can now specify the constraints on Rels."
    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
- (* Rel constraints *)
  let expected_height = 25 * (List.length must_rel + 2) in
  let height = if expected_height > 400 then 400 else expected_height in
  let scrolled_window =
   GBin.scrolled_window ~border_width:10 ~height ~width:600
-   ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in
+   ~packing:(vbox'#pack ~expand:true ~fill:true ~padding:5) () in
  let scrolled_vbox = GPack.vbox ~packing:scrolled_window#add_with_viewport () in
  let rel_constraints =
   List.map
@@ -2464,9 +2472,9 @@ let
       | Some depth' ->
          let mutable_ref = ref (Some depth') in
          let depthb =
-          GButton.toggle_button ~label:(string_of_int depth')
-           ~active:true ~packing:(hbox#pack ~expand:true ~fill:true ~padding:5)
-           ()
+          GButton.toggle_button
+           ~label:("depth = " ^ string_of_int depth') ~active:true
+           ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) ()
          in
           ignore
            (depthb#connect#toggled
@@ -2476,6 +2484,99 @@ let
             )) ;
           position, mutable_ref
    ) must_rel in
+ (* Sort constraints *)
+ let label =
+  GMisc.label
+   ~text: "Constraints on Sorts" () in
+ let vbox' =
+  GPack.vbox ~packing:(notebook#append_page ~tab_label:label#coerce)
+   () in
+ let hbox =
+  GPack.hbox ~packing:(vbox'#pack ~expand:false ~fill:false ~padding:5) () in
+ let lMessage =
+  GMisc.label
+   ~text: "You can now specify the constraints on Sorts."
+   ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
+ let expected_height = 25 * (List.length must_sort + 2) in
+ let height = if expected_height > 400 then 400 else expected_height in
+ let scrolled_window =
+  GBin.scrolled_window ~border_width:10 ~height ~width:600
+   ~packing:(vbox'#pack ~expand:true ~fill:true ~padding:5) () in
+ let scrolled_vbox = GPack.vbox ~packing:scrolled_window#add_with_viewport () in
+ let sort_constraints =
+  List.map
+   (function (position,depth,sort) ->
+     let hbox =
+      GPack.hbox
+       ~packing:(scrolled_vbox#pack ~expand:false ~fill:false ~padding:5) () in
+     let lMessage =
+      GMisc.label
+       ~text:(sort ^ " " ^ position)
+       ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
+     match depth with
+        None -> position, ref None, sort
+      | Some depth' ->
+         let mutable_ref = ref (Some depth') in
+         let depthb =
+          GButton.toggle_button ~label:("depth = " ^ string_of_int depth')
+           ~active:true
+           ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) ()
+         in
+          ignore
+           (depthb#connect#toggled
+             (function () ->
+               let sel_depth = if depthb#active then Some depth' else None in
+                mutable_ref := sel_depth
+            )) ;
+          position, mutable_ref, sort
+   ) must_sort in
+ (* Obj constraints *)
+ let label =
+  GMisc.label
+   ~text: "Constraints on constants" () in
+ let vbox' =
+  GPack.vbox ~packing:(notebook#append_page ~tab_label:label#coerce)
+   () in
+ let hbox =
+  GPack.hbox ~packing:(vbox'#pack ~expand:false ~fill:false ~padding:5) () in
+ let lMessage =
+  GMisc.label
+   ~text: "You can now specify the constraints on constants."
+   ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
+ let expected_height = 25 * (List.length must_obj + 2) in
+ let height = if expected_height > 400 then 400 else expected_height in
+ let scrolled_window =
+  GBin.scrolled_window ~border_width:10 ~height ~width:600
+   ~packing:(vbox'#pack ~expand:true ~fill:true ~padding:5) () in
+ let scrolled_vbox = GPack.vbox ~packing:scrolled_window#add_with_viewport () in
+ let obj_constraints =
+  List.map
+   (function (uri,position,depth) ->
+     let hbox =
+      GPack.hbox
+       ~packing:(scrolled_vbox#pack ~expand:false ~fill:false ~padding:5) () in
+     let lMessage =
+      GMisc.label
+       ~text:(uri ^ " " ^ position)
+       ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
+     match depth with
+        None -> uri, position, ref None
+      | Some depth' ->
+         let mutable_ref = ref (Some depth') in
+         let depthb =
+          GButton.toggle_button ~label:("depth = " ^ string_of_int depth')
+           ~active:true
+           ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) ()
+         in
+          ignore
+           (depthb#connect#toggled
+             (function () ->
+               let sel_depth = if depthb#active then Some depth' else None in
+                mutable_ref := sel_depth
+            )) ;
+          uri, position, mutable_ref
+   ) must_obj in
+ (* Confirm/abort buttons *)
  let hbox =
   GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
  let okb =
@@ -2495,18 +2596,24 @@ let
   if !chosen then
    let chosen_must_rel =
     List.map
-(*
-     (function (position,ref_depth) -> position,!ref_depth) rel_constraints
-*)
-(function (position,ref_depth) -> prerr_endline ("### " ^ position ^ " " ^ match !ref_depth with None -> "NULL" | Some d -> string_of_int d) ; position,!ref_depth) rel_constraints
+     (function (position,ref_depth) -> position,!ref_depth) rel_constraints in
+   let chosen_must_sort =
+    List.map
+     (function (position,ref_depth,sort) -> position,!ref_depth,sort)
+     sort_constraints
+   in
+   let chosen_must_obj =
+    List.map
+     (function (uri,position,ref_depth) -> uri,position,!ref_depth)
+     obj_constraints
    in
-   (must_obj,chosen_must_rel,must_sort),
-    (if !use_only then
+    (chosen_must_obj,chosen_must_rel,chosen_must_sort),
+     (if !use_only then
 (*CSC: ???????????????????????? I assume that must and only are the same... *)
-      only_obj,Some chosen_must_rel,only_sort
-     else
-      None,None,None
-    )
+       Some chosen_must_obj,Some chosen_must_rel,Some chosen_must_sort
+      else
+       None,None,None
+     )
   else
    raise NoChoice
 ;;
@@ -2517,9 +2624,9 @@ let completeSearchPattern () =
   try
    let dom,mk_metasenv_and_expr = inputt#get_term ~context:[] ~metasenv:[] in
    let metasenv,expr = disambiguate_input [] [] dom mk_metasenv_and_expr in
-   let must,only = MQueryLevels2.get_constraints expr in
-   let must',only' = refine_constraints must only in
-   let results = MQueryGenerator.searchPattern must' only' in 
+   let must = MQueryLevels2.get_constraints expr in
+   let must',only = refine_constraints must in
+   let results = MQueryGenerator.searchPattern must' only in 
     show_query_results results
   with
    e ->

diff --git a/helm/gTopLevel/mQueryLevels2.ml b/helm/gTopLevel/mQueryLevels2.ml
index afd0ee42b957c4bb6311003c35e2185cdb5fc09c..968d2a35e8d6439c65c0549bc35d7f58c372f383 100644 (file)
--- a/helm/gTopLevel/mQueryLevels2.ml
+++ b/helm/gTopLevel/mQueryLevels2.ml
@@ -169,14 +169,13 @@ in
  let obj_constraints,rel_constraints,sort_constraints =
   process_type_aux (Backbone 0) (CicMiniReduction.letin_nf term)
  in
-  (obj_constraints,rel_constraints,sort_constraints),
-   (Some obj_constraints,Some rel_constraints,Some sort_constraints)
+  (obj_constraints,rel_constraints,sort_constraints)
 ;;
 
 (*CSC: Debugging only *)
 let get_constraints term =
  let res = get_constraints term in
- let ((objs,rels,sorts),can) = res in
+ let (objs,rels,sorts) = res in
   prerr_endline "Constraints on objs:" ;
   List.iter
    (function (s1,s2,n) ->
@@ -197,6 +196,5 @@ let get_constraints term =
       (s1 ^ " " ^ (match n with Some n' -> string_of_int n' | None -> "NULL") ^
         " " ^ s2)
    ) sorts ;
-  prerr_endline "The \"only\" constraints are the same." ;
   res
 ;;

diff --git a/helm/gTopLevel/mQueryLevels2.mli b/helm/gTopLevel/mQueryLevels2.mli
index 584ec6909477d66af4a9a15db547725ac461a900..805f1064da2517efbe5a5a962f1ef7cf2844f614 100644 (file)
--- a/helm/gTopLevel/mQueryLevels2.mli
+++ b/helm/gTopLevel/mQueryLevels2.mli
@@ -33,6 +33,4 @@
 (*                                                                            *)
 (******************************************************************************)
 
-val get_constraints:
- Cic.term ->
-  MQueryGenerator.must_restrictions * MQueryGenerator.only_restrictions
+val get_constraints: Cic.term -> MQueryGenerator.must_restrictions