From: Claudio Sacerdoti Coen Date: Wed, 4 Dec 2002 15:38:47 +0000 (+0000) Subject: * mQueryLevels interface clean-up X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=ce1d4b008a076daf4737f33d57a6c5873aa88813;p=helm.git * mQueryLevels interface clean-up * gui improvement: the precision level of the SearchPattern query is now chosen by the user. Previously it was guessed. --- diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml index afbbc1439..32599cd61 100644 --- a/helm/gTopLevel/gTopLevel.ml +++ b/helm/gTopLevel/gTopLevel.ml @@ -2376,28 +2376,89 @@ let completeSearchPattern () = ("

" ^ Printexc.to_string e ^ "

") ; ;; +let choose_must list_of_must = + let chosen = ref None in + let window = + GWindow.window + ~modal:true ~title:"Query refinement." ~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 + let lMessage = + GMisc.label + ~text: + ("You can now specify the genericity of the query. " ^ + "The more generic the slower.") + ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in + let hbox = + GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in + let lMessage = + GMisc.label + ~text: + "Suggestion: start with faster queries before moving to more generic ones." + ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in + let notebook = + GPack.notebook ~scrollable:true + ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in + let _ = + let page = ref 0 in + let last = List.length list_of_must in + List.map + (function must -> + incr page ; + let label = + GMisc.label ~text: + (if !page = 1 then "More generic" else + if !page = last then "More precise" else " ") () + in + let clist = + let expected_height = 25 * (List.length must + 1) 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:(notebook#append_page ~tab_label:label#coerce) () + in + GList.clist ~columns:2 ~packing:scrolled_window#add + ~titles:["URI" ; "Position"] () + in + ignore + (List.map + (function (uri,position) -> + let n = + clist#append + [uri; if position then "MainConclusion" else "Conclusion"] + in + clist#set_row ~selectable:false n + ) must + ) ; + clist#columns_autosize () + ) list_of_must in + let hbox = + GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in + let okb = + GButton.button ~label:"Ok" + ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in + let cancelb = + GButton.button ~label:"Abort" + ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in + (* actions *) + ignore (window#connect#destroy GMain.Main.quit) ; + ignore (cancelb#connect#clicked window#destroy) ; + ignore + (okb#connect#clicked + (function () -> chosen := Some notebook#current_page ; window#destroy ())) ; + window#set_position `CENTER ; + window#show () ; + GMain.Main.main () ; + match !chosen with + None -> raise NoChoice + | Some n -> List.nth list_of_must n +;; + let searchPattern () = let inputt = ((rendering_window ())#inputt : term_editor) in let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in try - let rec get_level ?(last_invalid=false) () = - match - GToolbox.input_string - ~title:"Insert the strictness parameter for the query:" - ((if last_invalid then - "Invalid input (must be a non-negative natural number). Insert again " - else - "Insert " - ) ^ "the strictness parameter for the query:") - with - None -> raise NoChoice - | Some n -> - try - int_of_string n - with - _ -> get_level ~last_invalid:true () - in - let level = get_level () in let metasenv = match !ProofEngine.proof with None -> assert false @@ -2408,8 +2469,7 @@ let searchPattern () = | Some metano -> let (_, ey ,ty) = List.find (function (m,_,_) -> m=metano) metasenv 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 must = choose_must list_of_must in let result = MQueryGenerator.searchPattern metasenv ey ty must can in let uris = List.map @@ -2418,9 +2478,6 @@ let searchPattern () = ) result in let html = "

Backward Query:

" ^ - "

Levels:

" ^ - MQueryLevels.string_of_levels - (MQueryLevels.levels_of_term metasenv ey ty) "
" ^ " 
" ^ get_last_query result ^ "
" in output_html outputhtml html ; diff --git a/helm/gTopLevel/mQueryLevels.ml b/helm/gTopLevel/mQueryLevels.ml index ecadbd84b..977638dba 100644 --- a/helm/gTopLevel/mQueryLevels.ml +++ b/helm/gTopLevel/mQueryLevels.ml @@ -33,10 +33,6 @@ (* *) (******************************************************************************) -(* level managing functions *************************************************) - -type levels_spec = (string * bool * int) list - let levels_of_term metasenv context term = let module TC = CicTypeChecker in let module Red = CicReduction in @@ -130,31 +126,12 @@ let levels_of_term metasenv context term = in inspect_backbone term -let string_of_levels l sep = - let entry_out (s, b, v) = - let pos = if b then " HEAD: " else " TAIL: " in - string_of_int v ^ pos ^ s ^ sep - in - let rec levels_out = function - | [] -> "" - | head :: tail -> entry_out head ^ levels_out tail - 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 ""; +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 @@ -168,5 +145,4 @@ print_endline ""; 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 82fb7c699..5b214b733 100644 --- a/helm/gTopLevel/mQueryLevels.mli +++ b/helm/gTopLevel/mQueryLevels.mli @@ -33,14 +33,4 @@ (* *) (******************************************************************************) -(*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 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 cb7c7fca1..745be0767 100644 --- a/helm/gTopLevel/topLevel/topLevel.ml +++ b/helm/gTopLevel/topLevel/topLevel.ml @@ -73,18 +73,6 @@ let rec display = function print_string ("? " ^ CicPp.ppterm term ^ nl); flush stdout -let levels l = - let module Lev = MQueryLevels in - let rec levels_aux = function - | [] -> () - | term :: tail -> - levels_aux tail; - print_string ("? " ^ CicPp.ppterm term ^ nl); - print_string (Lev.string_of_levels (Lev.levels_of_term [] [] term) nl); - flush stdout - in - levels_aux l - let execute ich = let module Util = MQueryUtil in let module Gen = MQueryGenerator in @@ -159,7 +147,6 @@ let prerr_help () = prerr_endline "-t -typeof URI outputs the CIC type of the given HELM object"; prerr_endline "-x -execute issues a query given in the input file"; prerr_endline "-d -disply outputs the CIC terms given in the input file"; - prerr_endline "-l -levels outputs the cut levels of the CIC terms given in the input file"; prerr_endline "-L -locate ALIAS issues the \"Locate\" query for the given alias"; prerr_endline "-B -backward LEVEL issues the \"Backward\" query for the given level on all CIC terms"; prerr_endline " in the input file"; @@ -175,7 +162,6 @@ let parse_args () = | ("-h"|"-help") :: rem -> prerr_help () | ("-d"|"-display") :: rem -> display (get_terms ()) | ("-t"|"-typeof") :: arg :: rem -> pp_type_of arg; parse rem - | ("-l"|"-levels") :: rem -> levels (get_terms ()) | ("-x"|"-execute") :: rem -> execute stdin; parse rem | ("-q"|"-show-queries") :: rem -> show_queries := true; parse rem | ("-s"|"-stat") :: rem -> Mqint.set_stat true; parse rem