+ check_term_in_scratch scratch_window metasenv' context expr
+ with
+ e ->
+ HelmLogger.log
+ (`Error (`T (Printexc.to_string e)))
+;;
+
+let show () =
+ try
+ show_in_show_window_uri (input_or_locate_uri ~title:"Show")
+ with
+ e ->
+ HelmLogger.log
+ (`Error (`T (Printexc.to_string e)))
+;;
+
+exception NotADefinition;;
+
+let open_ () =
+ let output = ((rendering_window ())#output : TermViewer.proof_viewer) in
+ let notebook = (rendering_window ())#notebook in
+ try
+ let uri = input_or_locate_uri ~title:"Open" in
+ ignore(CicTypeChecker.typecheck uri CicUniv.empty_ugraph);
+ (* TASSI: typecheck mette la uri nell'env... cosa fa la open_ ?*)
+ let metasenv,bo,ty =
+ match fst(CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri ) with
+ Cic.Constant (_,Some bo,ty,_,_) -> [],bo,ty
+ | Cic.CurrentProof (_,metasenv,bo,ty,_,_) -> metasenv,bo,ty
+ | Cic.Constant _
+ | Cic.Variable _
+ | Cic.InductiveDefinition _ -> raise NotADefinition
+ in
+ ProofEngine.set_proof (Some (Some uri, metasenv, bo, ty)) ;
+ set_proof_engine_goal None ;
+ refresh_goals notebook ;
+ refresh_proof output ;
+ !save_set_sensitive true
+ with
+ InvokeTactics.RefreshSequentException e ->
+ HelmLogger.log
+ (`Error (`T ("Exception raised during the refresh of the " ^
+ "sequent: " ^ Printexc.to_string e)))
+ | InvokeTactics.RefreshProofException e ->
+ HelmLogger.log
+ (`Error (`T ("Exception raised during the refresh of the " ^
+ "proof: " ^ Printexc.to_string e)))
+ | e ->
+ HelmLogger.log
+ (`Error (`T (Printexc.to_string e)))
+;;
+
+let show_query_results results =
+ let window =
+ GWindow.window
+ ~modal:false ~title:"Query results." ~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:"Click on a URI to show that object"
+ ~packing:hbox#add () in
+ let scrolled_window =
+ GBin.scrolled_window ~border_width:10 ~height:400 ~width:600
+ ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in
+ let clist = GList.clist ~columns:1 ~packing:scrolled_window#add () in
+ ignore
+ (List.map
+ (function (uri,_) ->
+ let n =
+ clist#append [uri]
+ in
+ clist#set_row ~selectable:false n
+ ) results
+ ) ;
+ clist#columns_autosize () ;
+ ignore
+ (clist#connect#select_row
+ (fun ~row ~column ~event ->
+ let (uristr,_) = List.nth results row in
+ match CicUtil.term_of_uri uristr with
+ | Cic.Const (uri, _)
+ | Cic.Var (uri, _)
+ | Cic.MutInd (uri, _, _)
+ | Cic.MutConstruct (uri, _, _, _) ->
+ show_in_show_window_uri uri
+ | _ -> assert false
+ )
+ ) ;
+ window#show ()
+;;
+
+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."
+ ~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
+ let lMessage =
+ GMisc.label
+ ~text: "\"Only\" constraints can be enforced or not."
+ ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
+ let onlyb =
+ GButton.toggle_button ~label:"Enforce \"only\" constraints"
+ ~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
+ let lMessage =
+ GMisc.label
+ ~text: "You can now specify the constraints on Rels."
+ ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
+ 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
+ let scrolled_vbox = GPack.vbox ~packing:scrolled_window#add_with_viewport () in
+ let mk_depth_button (hbox:GPack.box) d =
+ let mutable_ref = ref (Some d) in
+ let depthb =
+ GButton.toggle_button
+ ~label:("depth = " ^ string_of_int d)
+ ~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 d else None in
+ mutable_ref := sel_depth
+ )) ; mutable_ref
+ in
+ let rel_constraints =
+ List.map
+ (function p ->
+ let hbox =
+ GPack.hbox
+ ~packing:(scrolled_vbox#pack ~expand:false ~fill:false ~padding:5) () in
+ let lMessage =
+ GMisc.label
+ ~text:(MQGU.text_of_position (p:>MQGT.full_position))
+ ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
+ match p with
+ | `MainHypothesis None
+ | `MainConclusion None -> p, ref None
+ | `MainHypothesis (Some depth')
+ | `MainConclusion (Some depth') -> p, mk_depth_button hbox depth'
+ ) 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 (p, sort) ->
+ let hbox =
+ GPack.hbox
+ ~packing:(scrolled_vbox#pack ~expand:false ~fill:false ~padding:5) () in
+ let lMessage =
+ GMisc.label
+ ~text:(MQGU.text_of_sort sort ^ " " ^ MQGU.text_of_position (p:>MQGT.full_position))
+ ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
+ match p with
+ | `MainHypothesis None
+ | `MainConclusion None -> p, ref None, sort
+ | `MainHypothesis (Some depth')
+ | `MainConclusion (Some depth') -> p, mk_depth_button hbox depth', 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 (p, uri) ->
+ let hbox =
+ GPack.hbox
+ ~packing:(scrolled_vbox#pack ~expand:false ~fill:false ~padding:5) () in
+ let lMessage =
+ GMisc.label
+ ~text:(uri ^ " " ^ (MQGU.text_of_position p))
+ ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
+ match p with
+ | `InBody
+ | `InHypothesis
+ | `InConclusion
+ | `MainHypothesis None
+ | `MainConclusion None -> p, ref None, uri
+ | `MainHypothesis (Some depth')
+ | `MainConclusion (Some depth') -> p, mk_depth_button hbox depth', uri
+ ) must_obj in
+ (* Confirm/abort buttons *)
+ 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
+ ignore (window#connect#destroy GMain.Main.quit) ;
+ ignore (cancelb#connect#clicked window#destroy) ;
+ ignore
+ (okb#connect#clicked (function () -> chosen := true ; window#destroy ()));
+ window#set_position `CENTER ;
+ window#show () ;
+ GtkThread.main ();
+ if !chosen then
+ let chosen_must_rel =
+ List.map
+ (function (position, ref_depth) -> MQGU.set_main_position position !ref_depth)
+ rel_constraints
+ in
+ let chosen_must_sort =
+ List.map
+ (function (position, ref_depth, sort) ->
+ MQGU.set_main_position position !ref_depth,sort)
+ sort_constraints
+ in
+ let chosen_must_obj =
+ List.map
+ (function (position, ref_depth, uri) -> MQGU.set_full_position position !ref_depth, uri)
+ obj_constraints
+ in
+ (chosen_must_obj,chosen_must_rel,chosen_must_sort),
+ (if !use_only then
+(*CSC: ???????????????????????? I assume that must and only are the same... *)
+ Some chosen_must_obj,Some chosen_must_rel,Some chosen_must_sort
+ else
+ None,None,None
+ )
+ else
+ raise NoChoice
+;;
+
+let completeSearchPattern () =
+ let inputt = ((rendering_window ())#inputt : TermEditor.term_editor) in
+ try
+ let metasenv,expr,ugraph =
+ inputt#get_metasenv_and_term ~context:[] ~metasenv:[] in
+ let must = CGSearchPattern.get_constraints expr in
+ let must',only = refine_constraints must in
+ let query =
+ MQG.query_of_constraints (Some CGSearchPattern.universe) must' only
+ in
+ let results = MQI.execute mqi_handle query in
+ show_query_results results
+ with
+ e ->
+ HelmLogger.log
+ (`Error (`T (Printexc.to_string e)))
+;;
+
+let insertQuery () =
+ try
+ let chosen = ref None in
+ let window =
+ GWindow.window
+ ~modal:true ~title:"Insert Query (Experts Only)" ~border_width:2 () in
+ let vbox = GPack.vbox ~packing:window#add () in
+ let label =
+ GMisc.label ~text:"Insert Query. For Experts Only."
+ ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
+ let scrolled_window =
+ GBin.scrolled_window ~border_width:10 ~height:400 ~width:600
+ ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in
+ let input = GText.view ~editable:true
+ ~packing:scrolled_window#add () 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 loadb =
+ GButton.button ~label:"Load from file..."
+ ~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
+ ignore (window#connect#destroy GMain.Main.quit) ;
+ ignore (cancelb#connect#clicked window#destroy) ;
+ ignore
+ (okb#connect#clicked
+ (function () ->
+ chosen := Some (input#buffer#get_text ()) ; window#destroy ())) ;
+ ignore
+ (loadb#connect#clicked
+ (function () ->
+ match
+ GToolbox.select_file ~title:"Select Query File" ()
+ with
+ None -> ()
+ | Some filename ->
+ let inch = open_in filename in
+ let rec read_file () =
+ try
+ let line = input_line inch in
+ line ^ "\n" ^ read_file ()
+ with
+ End_of_file -> ""
+ in
+ let text = read_file () in
+ input#buffer#delete input#buffer#start_iter input#buffer#end_iter ;
+ ignore (input#buffer#insert text))) ;
+ window#set_position `CENTER ;
+ window#show () ;
+ GtkThread.main ();
+ match !chosen with
+ None -> ()
+ | Some q ->
+ let results =
+ MQI.execute mqi_handle (MQueryUtil.query_of_text (Lexing.from_string q))
+ in
+ show_query_results results
+ with
+ e ->
+ HelmLogger.log
+ (`Error (`T (Printexc.to_string e)))
+;;
+
+let choose_must list_of_must only =
+ let chosen = ref None in
+ let user_constraints = ref [] 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 expected_height = 25 * (List.length must + 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:(notebook#append_page ~tab_label:label#coerce) () in
+ let clist =
+ GList.clist ~columns:2 ~packing:scrolled_window#add
+ ~titles:["URI" ; "Position"] ()
+ in
+ ignore
+ (List.map
+ (function (position, uri) ->
+ let n =
+ clist#append
+ [uri; MQGUtil.text_of_position position]
+ in
+ clist#set_row ~selectable:false n
+ ) must
+ ) ;
+ clist#columns_autosize ()
+ ) list_of_must in
+ let _ =
+ let label = GMisc.label ~text:"User provided" () 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:"Select the constraints that must be satisfied and press OK."
+ ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
+ let expected_height = 25 * (List.length only + 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 clist =
+ GList.clist ~columns:2 ~packing:scrolled_window#add
+ ~selection_mode:`MULTIPLE
+ ~titles:["URI" ; "Position"] ()
+ in
+ ignore
+ (List.map
+ (function (position, uri) ->
+ let n =
+ clist#append
+ [uri; MQGUtil.text_of_position position]
+ in
+ clist#set_row ~selectable:true n
+ ) only
+ ) ;
+ clist#columns_autosize () ;
+ ignore
+ (clist#connect#select_row
+ (fun ~row ~column ~event ->
+ user_constraints := (List.nth only row)::!user_constraints)) ;
+ ignore
+ (clist#connect#unselect_row
+ (fun ~row ~column ~event ->
+ user_constraints :=
+ List.filter
+ (function uri -> uri != (List.nth only row)) !user_constraints)) ;
+ 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 () ;
+ GtkThread.main ();
+ match !chosen with
+ None -> raise NoChoice
+ | Some n ->
+ if n = List.length list_of_must then
+ (* user provided constraints *)
+ !user_constraints