("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
;;
+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
| 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
) result in
let html =
" <h1>Backward Query: </h1>" ^
- " <h2>Levels: </h2> " ^
- MQueryLevels.string_of_levels
- (MQueryLevels.levels_of_term metasenv ey ty) "<br>" ^
" <pre>" ^ get_last_query result ^ "</pre>"
in
output_html outputhtml html ;
(* *)
(******************************************************************************)
-(* 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
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
let mrest = List.map lofl can in
let must_use = organize_restr mrest [] in (* must restrictions *)
(must_use,can_use)
-
-
+;;
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
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";
| ("-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
projects / helm.git / commitdiff