From 2bdf5f214317e2d9960bd796efc234a8762eda61 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 6 Dec 2002 18:43:09 +0000 Subject: [PATCH] * 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. --- helm/gTopLevel/gTopLevel.ml | 157 ++++++++++++++++++++++++++----- helm/gTopLevel/mQueryLevels2.ml | 6 +- helm/gTopLevel/mQueryLevels2.mli | 4 +- 3 files changed, 135 insertions(+), 32 deletions(-) diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml index 890f5d75f..2e9c702dc 100644 --- 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 afd0ee42b..968d2a35e 100644 --- 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 584ec6909..805f1064d 100644 --- 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 -- 2.39.2