(* Copyright (C) 2000-2003, HELM Team. * * This file is part of HELM, an Hypertextual, Electronic * Library of Mathematics, developed at the Computer Science * Department, University of Bologna, Italy. * * HELM is free software; you can redistribute it and/or * modify it under the terms of the GNU General Public License * as published by the Free Software Foundation; either version 2 * of the License, or (at your option) any later version. * * HELM is distributed in the hope that it will be useful, * but WITHOUT ANY WARRANTY; without even the implied warranty of * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the * GNU General Public License for more details. * * You should have received a copy of the GNU General Public License * along with HELM; if not, write to the Free Software * Foundation, Inc., 59 Temple Place - Suite 330, Boston, * MA 02111-1307, USA. * * For details, see the HELM World-Wide-Web page, * http://cs.unibo.it/helm/. *) (******************************************************************************) (* *) (* PROJECT HELM *) (* *) (* Claudio Sacerdoti Coen *) (* 06/01/2002 *) (* *) (* *) (******************************************************************************) open Printf;; (* DEBUGGING *) module MQI = MQueryInterpreter module MQIC = MQIConn module MQGT = MQGTypes module MQGU = MQGUtil module MQG = MQueryGenerator (* GLOBAL CONSTANTS *) let mqi_flags = [MQIC.Postgres ; MQIC.Stat ; MQIC.Warn ; MQIC.Log] (* default MathQL interpreter options *) (* let mqi_flags = [] (* default MathQL interpreter options *) *) let mqi_handle = MQIC.init mqi_flags prerr_string let xlinkns = Gdome.domString "http://www.w3.org/1999/xlink";; let htmlheader = "" ^ " " ;; let htmlfooter = " " ^ "" ;; let prooffile = try Sys.getenv "GTOPLEVEL_PROOFFILE" with Not_found -> "/public/currentproof" ;; let prooffiletype = try Sys.getenv "GTOPLEVEL_PROOFFILETYPE" with Not_found -> "/public/currentprooftype" ;; let environmentfile = try Sys.getenv "GTOPLEVEL_ENVIRONMENTFILE" with Not_found -> "/public/environment" ;; let restore_environment_on_boot = true ;; let notify_hbugs_on_goal_change = false ;; (* GLOBAL REFERENCES (USED BY CALLBACKS) *) let htmlheader_and_content = ref htmlheader;; let check_term = ref (fun _ _ _ -> assert false);; exception RenderingWindowsNotInitialized;; let set_rendering_window,rendering_window = let rendering_window_ref = ref None in (function rw -> rendering_window_ref := Some rw), (function () -> match !rendering_window_ref with None -> raise RenderingWindowsNotInitialized | Some rw -> rw ) ;; exception SettingsWindowsNotInitialized;; let set_settings_window,settings_window = let settings_window_ref = ref None in (function rw -> settings_window_ref := Some rw), (function () -> match !settings_window_ref with None -> raise SettingsWindowsNotInitialized | Some rw -> rw ) ;; exception OutputHtmlNotInitialized;; let set_outputhtml,outputhtml = let outputhtml_ref = ref None in (function rw -> outputhtml_ref := Some rw), (function () -> match !outputhtml_ref with None -> raise OutputHtmlNotInitialized | Some outputhtml -> outputhtml ) ;; exception QedSetSensitiveNotInitialized;; let qed_set_sensitive = ref (function _ -> raise QedSetSensitiveNotInitialized) ;; exception SaveSetSensitiveNotInitialized;; let save_set_sensitive = ref (function _ -> raise SaveSetSensitiveNotInitialized) ;; (* COMMAND LINE OPTIONS *) let usedb = ref true let argspec = [ "-nodb", Arg.Clear usedb, "disable use of MathQL DB" ] in Arg.parse argspec ignore "" (* MISC FUNCTIONS *) let term_of_cic_textual_parser_uri uri = let module C = Cic in let module CTP = CicTextualParser0 in match uri with CTP.ConUri uri -> C.Const (uri,[]) | CTP.VarUri uri -> C.Var (uri,[]) | CTP.IndTyUri (uri,tyno) -> C.MutInd (uri,tyno,[]) | CTP.IndConUri (uri,tyno,consno) -> C.MutConstruct (uri,tyno,consno,[]) ;; let string_of_cic_textual_parser_uri uri = let module C = Cic in let module CTP = CicTextualParser0 in let uri' = match uri with CTP.ConUri uri -> UriManager.string_of_uri uri | CTP.VarUri uri -> UriManager.string_of_uri uri | CTP.IndTyUri (uri,tyno) -> UriManager.string_of_uri uri ^ "#1/" ^ string_of_int (tyno + 1) | CTP.IndConUri (uri,tyno,consno) -> UriManager.string_of_uri uri ^ "#1/" ^ string_of_int (tyno + 1) ^ "/" ^ string_of_int consno in (* 4 = String.length "cic:" *) String.sub uri' 4 (String.length uri' - 4) ;; let output_html outputhtml msg = outputhtml#log msg ;; (* UTILITY FUNCTIONS TO DISAMBIGUATE AN URI *) (* Check window *) let check_window outputhtml uris = let window = GWindow.window ~width:800 ~modal:true ~title:"Check" ~border_width:2 () in let notebook = GPack.notebook ~scrollable:true ~packing:window#add () in window#show () ; let render_terms = List.map (function uri -> let scrolled_window = GBin.scrolled_window ~border_width:10 ~packing: (notebook#append_page ~tab_label:((GMisc.label ~text:uri ())#coerce)) () in lazy (let mmlwidget = TermViewer.sequent_viewer ~packing:scrolled_window#add ~width:400 ~height:280 () in let expr = let term = term_of_cic_textual_parser_uri (MQueryMisc.cic_textual_parser_uri_of_string uri) in (Cic.Cast (term, CicTypeChecker.type_of_aux' [] [] term)) in try mmlwidget#load_sequent [] (111,[],expr) with e -> output_html outputhtml (`Error (`T (Printexc.to_string e))) ) ) uris in ignore (notebook#connect#switch_page (function i -> Lazy.force (List.nth render_terms i))) ;; exception NoChoice;; let interactive_user_uri_choice ~(selection_mode:[`MULTIPLE|`SINGLE]) ?(ok="Ok") ?(enable_button_for_non_vars=false) ~title ~msg uris = let choices = ref [] in let chosen = ref false in let use_only_constants = ref false in let window = GWindow.dialog ~modal:true ~title ~width:600 () in let lMessage = GMisc.label ~text:msg ~packing:(window#vbox#pack ~expand:false ~fill:false ~padding:5) () in let scrolled_window = GBin.scrolled_window ~border_width:10 ~packing:(window#vbox#pack ~expand:true ~fill:true ~padding:5) () in let clist = let expected_height = 18 * List.length uris in let height = if expected_height > 400 then 400 else expected_height in GList.clist ~columns:1 ~packing:scrolled_window#add ~height ~selection_mode:(selection_mode :> Gtk.Tags.selection_mode) () in let _ = List.map (function x -> clist#append [x]) uris in let hbox2 = GPack.hbox ~border_width:0 ~packing:(window#vbox#pack ~expand:false ~fill:false ~padding:5) () in let explain_label = GMisc.label ~text:"None of the above. Try this one:" ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5) () in let manual_input = GEdit.entry ~editable:true ~packing:(hbox2#pack ~expand:true ~fill:true ~padding:5) () in let hbox = GPack.hbox ~border_width:0 ~packing:window#action_area#add () in let okb = GButton.button ~label:ok ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in let _ = okb#misc#set_sensitive false in let nonvarsb = GButton.button ~packing: (function w -> if enable_button_for_non_vars then hbox#pack ~expand:false ~fill:false ~padding:5 w) ~label:"Try constants only" () in let checkb = GButton.button ~label:"Check" ~packing:(hbox#pack ~padding:5) () in let _ = checkb#misc#set_sensitive false in let cancelb = GButton.button ~label:"Abort" ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in (* actions *) let check_callback () = assert (List.length !choices > 0) ; check_window (outputhtml ()) !choices in ignore (window#connect#destroy GMain.Main.quit) ; ignore (cancelb#connect#clicked window#destroy) ; ignore (okb#connect#clicked (function () -> chosen := true ; window#destroy ())) ; ignore (nonvarsb#connect#clicked (function () -> use_only_constants := true ; chosen := true ; window#destroy () )) ; ignore (checkb#connect#clicked check_callback) ; ignore (clist#connect#select_row (fun ~row ~column ~event -> checkb#misc#set_sensitive true ; okb#misc#set_sensitive true ; choices := (List.nth uris row)::!choices)) ; ignore (clist#connect#unselect_row (fun ~row ~column ~event -> choices := List.filter (function uri -> uri != (List.nth uris row)) !choices)) ; ignore (manual_input#connect#changed (fun _ -> if manual_input#text = "" then begin choices := [] ; checkb#misc#set_sensitive false ; okb#misc#set_sensitive false ; clist#misc#set_sensitive true end else begin choices := [manual_input#text] ; clist#unselect_all () ; checkb#misc#set_sensitive true ; okb#misc#set_sensitive true ; clist#misc#set_sensitive false end)); window#set_position `CENTER ; window#show () ; GtkThread.main (); if !chosen then if !use_only_constants then List.filter (function uri -> not (String.sub uri (String.length uri - 4) 4 = ".var")) uris else if List.length !choices > 0 then !choices else raise NoChoice else raise NoChoice ;; let interactive_interpretation_choice interpretations = let chosen = ref None in let window = GWindow.window ~modal:true ~title:"Ambiguous well-typed input." ~border_width:2 () in let vbox = GPack.vbox ~packing:window#add () in let lMessage = GMisc.label ~text: ("Ambiguous input since there are many well-typed interpretations." ^ " Please, choose one of them.") ~packing:(vbox#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 _ = List.map (function interpretation -> let clist = let expected_height = 18 * List.length interpretation in let height = if expected_height > 400 then 400 else expected_height in GList.clist ~columns:2 ~packing:notebook#append_page ~height ~titles:["id" ; "URI"] () in ignore (List.map (function (id,uri) -> let n = clist#append [id;uri] in clist#set_row ~selectable:false n ) interpretation ) ; clist#columns_autosize () ) interpretations 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 -> n ;; (* MISC FUNCTIONS *) let save_object_to_disk uri annobj ids_to_inner_sorts ids_to_inner_types pathname = let name = let struri = UriManager.string_of_uri uri in let idx = (String.rindex struri '/') + 1 in String.sub struri idx (String.length struri - idx) in let path = pathname ^ "/" ^ name in let xml, bodyxml = Cic2Xml.print_object uri ~ids_to_inner_sorts ~ask_dtd_to_the_getter:false annobj in let xmlinnertypes = Cic2Xml.print_inner_types uri ~ids_to_inner_sorts ~ids_to_inner_types ~ask_dtd_to_the_getter:false in (* innertypes *) let innertypesuri = UriManager.innertypesuri_of_uri uri in Xml.pp ~quiet:true xmlinnertypes (Some (path ^ ".types.xml")) ; Getter.register innertypesuri (Configuration.annotations_url ^ Str.replace_first (Str.regexp "^cic:") "" (UriManager.string_of_uri innertypesuri) ^ ".xml" ) ; (* constant type / variable / mutual inductive types definition *) Xml.pp ~quiet:true xml (Some (path ^ ".xml")) ; Getter.register uri (Configuration.annotations_url ^ Str.replace_first (Str.regexp "^cic:") "" (UriManager.string_of_uri uri) ^ ".xml" ) ; match bodyxml with None -> () | Some bodyxml' -> (* constant body *) let bodyuri = match UriManager.bodyuri_of_uri uri with None -> assert false | Some bodyuri -> bodyuri in Xml.pp ~quiet:true bodyxml' (Some (path ^ ".body.xml")) ; Getter.register bodyuri (Configuration.annotations_url ^ Str.replace_first (Str.regexp "^cic:") "" (UriManager.string_of_uri bodyuri) ^ ".xml" ) ;; (* CALLBACKS *) exception OpenConjecturesStillThere;; exception WrongProof;; let pathname_of_annuri uristring = Configuration.annotations_dir ^ Str.replace_first (Str.regexp "^cic:") "" uristring ;; let make_dirs dirpath = ignore (Unix.system ("mkdir -p " ^ dirpath)) ;; let save_obj uri obj = let (acic,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts, ids_to_inner_types,ids_to_conjectures,ids_to_hypotheses) = Cic2acic.acic_object_of_cic_object obj in (* let's save the theorem and register it to the getter *) let pathname = pathname_of_annuri (UriManager.buri_of_uri uri) in make_dirs pathname ; save_object_to_disk uri acic ids_to_inner_sorts ids_to_inner_types pathname ;; let qed () = match ProofEngine.get_proof () with None -> assert false | Some (uri,[],bo,ty) -> if CicReduction.are_convertible [] (CicTypeChecker.type_of_aux' [] [] bo) ty then begin (*CSC: Wrong: [] is just plainly wrong *) let proof = Cic.Constant (UriManager.name_of_uri uri,Some bo,ty,[]) in let (acic,ids_to_inner_types,ids_to_inner_sorts) = (rendering_window ())#output#load_proof uri proof in !qed_set_sensitive false ; (* let's save the theorem and register it to the getter *) let pathname = pathname_of_annuri (UriManager.buri_of_uri uri) in make_dirs pathname ; save_object_to_disk uri acic ids_to_inner_sorts ids_to_inner_types pathname end else raise WrongProof | _ -> raise OpenConjecturesStillThere ;; (** save an unfinished proof on the filesystem *) let save_unfinished_proof () = let outputhtml = ((rendering_window ())#outputhtml(* : GHtml.xmhtml*)) in let (xml, bodyxml) = ProofEngine.get_current_status_as_xml () in Xml.pp ~quiet:true xml (Some prooffiletype) ; output_html outputhtml (`Msg (`T ("Current proof type saved to " ^ prooffiletype))) ; Xml.pp ~quiet:true bodyxml (Some prooffile) ; output_html outputhtml (`Msg (`T ("Current proof body saved to " ^ prooffile))) ;; (* Used to typecheck the loaded proofs *) let typecheck_loaded_proof metasenv bo ty = let module T = CicTypeChecker in ignore ( List.fold_left (fun metasenv ((_,context,ty) as conj) -> ignore (T.type_of_aux' metasenv context ty) ; metasenv @ [conj] ) [] metasenv) ; ignore (T.type_of_aux' metasenv [] ty) ; ignore (T.type_of_aux' metasenv [] bo) ;; let decompose_uris_choice_callback uris = (* N.B.: in questo passaggio perdo l'informazione su exp_named_subst !!!! *) let module U = UriManager in List.map (function uri -> match MQueryMisc.cic_textual_parser_uri_of_string uri with CicTextualParser0.IndTyUri (uri,typeno) -> (uri,typeno,[]) | _ -> assert false) (interactive_user_uri_choice ~selection_mode:`MULTIPLE ~ok:"Ok" ~enable_button_for_non_vars:false ~title:"Decompose" ~msg:"Please, select the Inductive Types to decompose" (List.map (function (uri,typeno,_) -> U.string_of_uri uri ^ "#1/" ^ string_of_int (typeno+1) ) uris) ) ;; let mk_fresh_name_callback context name ~typ = let fresh_name = match ProofEngineHelpers.mk_fresh_name context name ~typ with Cic.Name fresh_name -> fresh_name | Cic.Anonymous -> assert false in match GToolbox.input_string ~title:"Enter a fresh hypothesis name" ~text:fresh_name ("Enter a fresh name for the hypothesis " ^ CicPp.pp typ (List.map (function None -> None | Some (n,_) -> Some n) context)) with Some fresh_name' -> Cic.Name fresh_name' | None -> raise NoChoice ;; let refresh_proof (output : TermViewer.proof_viewer) = try let uri,currentproof = match ProofEngine.get_proof () with None -> assert false | Some (uri,metasenv,bo,ty) -> ProofEngine.set_proof (Some (uri,metasenv,bo,ty)) ; if List.length metasenv = 0 then begin !qed_set_sensitive true ; (*Hbugs.clear*) () end else (*Hbugs.notify*) () ; (*CSC: Wrong: [] is just plainly wrong *) uri, (Cic.CurrentProof (UriManager.name_of_uri uri, metasenv, bo, ty, [])) in ignore (output#load_proof uri currentproof) with e -> match ProofEngine.get_proof () with None -> assert false | Some (uri,metasenv,bo,ty) -> prerr_endline ("Offending proof: " ^ CicPp.ppobj (Cic.CurrentProof ("questa",metasenv,bo,ty,[]))) ; flush stderr ; raise (InvokeTactics.RefreshProofException e) let set_proof_engine_goal g = ProofEngine.goal := g ;; let refresh_goals ?(empty_notebook=true) notebook = try match !ProofEngine.goal with None -> if empty_notebook then begin notebook#remove_all_pages ~skip_switch_page_event:false ; notebook#set_empty_page end else notebook#proofw#unload | Some metano -> let metasenv = match ProofEngine.get_proof () with None -> assert false | Some (_,metasenv,_,_) -> metasenv in let currentsequent = List.find (function (m,_,_) -> m=metano) metasenv in let regenerate_notebook () = let skip_switch_page_event = match metasenv with (m,_,_)::_ when m = metano -> false | _ -> true in notebook#remove_all_pages ~skip_switch_page_event ; List.iter (function (m,_,_) -> notebook#add_page m) metasenv ; in if empty_notebook then begin regenerate_notebook () ; notebook#set_current_page ~may_skip_switch_page_event:false metano end else begin notebook#set_current_page ~may_skip_switch_page_event:true metano ; notebook#proofw#load_sequent metasenv currentsequent end with e -> let metano = match !ProofEngine.goal with None -> assert false | Some m -> m in let metasenv = match ProofEngine.get_proof () with None -> assert false | Some (_,metasenv,_,_) -> metasenv in try let currentsequent = List.find (function (m,_,_) -> m=metano) metasenv in prerr_endline ("Offending sequent: " ^ SequentPp.TextualPp.print_sequent currentsequent) ; flush stderr ; raise (InvokeTactics.RefreshSequentException e) with Not_found -> prerr_endline ("Offending sequent " ^ string_of_int metano ^ " unknown."); raise (InvokeTactics.RefreshSequentException e) module InvokeTacticsCallbacks = struct let sequent_viewer () = (rendering_window ())#notebook#proofw let term_editor () = (rendering_window ())#inputt let scratch_window () = (rendering_window ())#scratch_window let refresh_proof () = let output = ((rendering_window ())#output : TermViewer.proof_viewer) in refresh_proof output let refresh_goals () = let notebook = (rendering_window ())#notebook in refresh_goals notebook let decompose_uris_choice_callback = decompose_uris_choice_callback let mk_fresh_name_callback = mk_fresh_name_callback let output_html msg = output_html (outputhtml ()) (`Msg (`T msg)) end ;; module InvokeTactics' = InvokeTactics.Make (InvokeTacticsCallbacks);; (* Just to initialize the Hbugs module *) (* module Ignore = Hbugs.Initialize (InvokeTactics');; Hbugs.set_describe_hint_callback (fun hint -> match hint with | Hbugs_types.Use_apply_Luke term -> let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in check_window outputhtml [term] | _ -> ()) ;; *) let dummy_uri = "/dummy.con" (** load an unfinished proof from filesystem *) let load_unfinished_proof () = let outputhtml = ((rendering_window ())#outputhtml(* : GHtml.xmhtml*)) in let output = ((rendering_window ())#output : TermViewer.proof_viewer) in let notebook = (rendering_window ())#notebook in try match GToolbox.input_string ~title:"Load Unfinished Proof" ~text:dummy_uri "Choose an URI:" with None -> raise NoChoice | Some uri0 -> let uri = UriManager.uri_of_string ("cic:" ^ uri0) in match CicParser.obj_of_xml prooffiletype (Some prooffile) with Cic.CurrentProof (_,metasenv,bo,ty,_) -> typecheck_loaded_proof metasenv bo ty ; ProofEngine.set_proof (Some (uri, metasenv, bo, ty)) ; refresh_proof output ; set_proof_engine_goal (match metasenv with [] -> None | (metano,_,_)::_ -> Some metano ) ; refresh_goals notebook ; output_html outputhtml (`Msg (`T ("Current proof type loaded from " ^ prooffiletype))) ; output_html outputhtml (`Msg (`T ("Current proof body loaded from " ^ prooffile))) ; !save_set_sensitive true; | _ -> assert false with InvokeTactics.RefreshSequentException e -> output_html outputhtml (`Error (`T ("Exception raised during the refresh of the " ^ "sequent: " ^ Printexc.to_string e))) | InvokeTactics.RefreshProofException e -> output_html outputhtml (`Error (`T ("Exception raised during the refresh of the " ^ "proof: " ^ Printexc.to_string e))) | e -> output_html outputhtml (`Error (`T (Printexc.to_string e))) ;; let edit_aliases () = let inputt = ((rendering_window ())#inputt : TermEditor.term_editor) in let id_to_uris = inputt#id_to_uris in let chosen = ref false in let window = GWindow.window ~width:400 ~modal:true ~title:"Edit Aliases..." ~border_width:2 () in let vbox = GPack.vbox ~border_width:0 ~packing:window#add () in let scrolled_window = GBin.scrolled_window ~border_width:10 ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in let input = GText.view ~editable:true ~width:400 ~height:100 ~packing:scrolled_window#add () in let hbox = GPack.hbox ~border_width:0 ~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:"Cancel" ~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 ())) ; let dom,resolve_id = !id_to_uris in ignore (input#buffer#insert ~iter:(input#buffer#get_iter_at_char 0) (String.concat "\n" (List.map (function v -> let uri = match resolve_id v with None -> assert false | Some (CicTextualParser0.Uri uri) -> uri | Some (CicTextualParser0.Term _) | Some CicTextualParser0.Implicit -> assert false in "alias " ^ (match v with CicTextualParser0.Id id -> id | CicTextualParser0.Symbol (descr,_) -> (* CSC: To be implemented *) assert false )^ " " ^ (string_of_cic_textual_parser_uri uri) ) dom))) ; window#show () ; GtkThread.main (); if !chosen then let dom,resolve_id = let inputtext = input#buffer#get_text () in let regexpr = let alfa = "[a-zA-Z_-]" in let digit = "[0-9]" in let ident = alfa ^ "\(" ^ alfa ^ "\|" ^ digit ^ "\)*" in let blanks = "\( \|\t\|\n\)+" in let nonblanks = "[^ \t\n]+" in let uri = "/\(" ^ ident ^ "/\)*" ^ nonblanks in (* not very strict check *) Str.regexp ("alias" ^ blanks ^ "\(" ^ ident ^ "\)" ^ blanks ^ "\(" ^ uri ^ "\)") in let rec aux n = try let n' = Str.search_forward regexpr inputtext n in let id = CicTextualParser0.Id (Str.matched_group 2 inputtext) in let uri = MQueryMisc.cic_textual_parser_uri_of_string ("cic:" ^ (Str.matched_group 5 inputtext)) in let dom,resolve_id = aux (n' + 1) in if List.mem id dom then dom,resolve_id else id::dom, (function id' -> if id = id' then Some (CicTextualParser0.Uri uri) else resolve_id id') with Not_found -> TermEditor.empty_id_to_uris in aux 0 in id_to_uris := (dom,resolve_id) ;; let proveit () = let module L = LogicalOperations in let module G = Gdome in let notebook = (rendering_window ())#notebook in let output = (rendering_window ())#output in let outputhtml = ((rendering_window ())#outputhtml (*: GHtml.xmhtml*)) in try output#make_sequent_of_selected_term ; refresh_proof output ; refresh_goals notebook with InvokeTactics.RefreshSequentException e -> output_html outputhtml (`Error (`T ("Exception raised during the refresh of the " ^ "sequent: " ^ Printexc.to_string e))) | InvokeTactics.RefreshProofException e -> output_html outputhtml (`Error (`T ("Exception raised during the refresh of the " ^ "proof: " ^ Printexc.to_string e))) | e -> output_html outputhtml (`Error (`T (Printexc.to_string e))) ;; let focus () = let module L = LogicalOperations in let module G = Gdome in let notebook = (rendering_window ())#notebook in let outputhtml = ((rendering_window ())#outputhtml(* : GHtml.xmhtml*)) in let output = (rendering_window ())#output in try output#focus_sequent_of_selected_term ; refresh_goals notebook with InvokeTactics.RefreshSequentException e -> output_html outputhtml (`Error (`T ("Exception raised during the refresh of the " ^ "sequent: " ^ Printexc.to_string e))) | InvokeTactics.RefreshProofException e -> output_html outputhtml (`Error (`T ("Exception raised during the refresh of the " ^ "proof: " ^ Printexc.to_string e))) | e -> output_html outputhtml (`Error (`T (Printexc.to_string e))) ;; exception NoPrevGoal;; exception NoNextGoal;; let setgoal metano = let module L = LogicalOperations in let module G = Gdome in let notebook = (rendering_window ())#notebook in let output = (rendering_window ())#output in let outputhtml = (rendering_window ())#outputhtml in let metasenv = match ProofEngine.get_proof () with None -> assert false | Some (_,metasenv,_,_) -> metasenv in try refresh_goals ~empty_notebook:false notebook with InvokeTactics.RefreshSequentException e -> output_html outputhtml (`Error (`T ("Exception raised during the refresh of the " ^ "sequent: " ^ Printexc.to_string e))) | e -> output_html outputhtml (`Error (`T (Printexc.to_string e))) ;; let show_in_show_window_obj, show_in_show_window_uri, show_in_show_window_callback = let window = GWindow.window ~width:800 ~border_width:2 () in let scrolled_window = GBin.scrolled_window ~border_width:10 ~packing:window#add () in let mmlwidget = GMathViewAux.single_selection_math_view ~packing:scrolled_window#add ~width:600 ~height:400 () in let _ = window#event#connect#delete (fun _ -> window#misc#hide () ; true ) in let href = Gdome.domString "href" in let show_in_show_window_obj uri obj = let outputhtml = ((rendering_window ())#outputhtml(* : GHtml.xmhtml*)) in try let (acic,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts, ids_to_inner_types,ids_to_conjectures,ids_to_hypotheses) = Cic2acic.acic_object_of_cic_object obj in let mml = ApplyStylesheets.mml_of_cic_object ~explode_all:false uri acic ids_to_inner_sorts ids_to_inner_types in window#set_title (UriManager.string_of_uri uri) ; window#misc#hide () ; window#show () ; mmlwidget#load_doc mml ; with e -> output_html outputhtml (`Error (`T (Printexc.to_string e))) in let show_in_show_window_uri uri = let obj = CicEnvironment.get_obj uri in show_in_show_window_obj uri obj in let show_in_show_window_callback mmlwidget (n : Gdome.element option) _ = match n with None -> () | Some n' -> if n'#hasAttributeNS ~namespaceURI:xlinkns ~localName:href then let uri = (n'#getAttributeNS ~namespaceURI:xlinkns ~localName:href)#to_string in show_in_show_window_uri (UriManager.uri_of_string uri) else ignore (mmlwidget#action_toggle n') in let _ = mmlwidget#connect#click (show_in_show_window_callback mmlwidget) in show_in_show_window_obj, show_in_show_window_uri, show_in_show_window_callback ;; exception NoObjectsLocated;; let user_uri_choice ~title ~msg uris = let uri = match uris with [] -> raise NoObjectsLocated | [uri] -> uri | uris -> match interactive_user_uri_choice ~selection_mode:`SINGLE ~title ~msg uris with [uri] -> uri | _ -> assert false in String.sub uri 4 (String.length uri - 4) ;; let locate_callback id = let outputhtml = ((rendering_window ())#outputhtml(* : GHtml.xmhtml*)) in let out = output_html outputhtml in let query = MQG.locate id in let result = MQI.execute mqi_handle query in let uris = List.map (function uri,_ -> MQueryMisc.wrong_xpointer_format_from_wrong_xpointer_format' uri) result in out (`Msg (`T "Locate Query:")) ; MQueryUtil.text_of_query (fun m -> out (`Msg (`T m))) "" query; out (`Msg (`T "Result:")) ; MQueryUtil.text_of_result (fun m -> out (`Msg (`T m))) "" result; user_uri_choice ~title:"Ambiguous input." ~msg: ("Ambiguous input \"" ^ id ^ "\". Please, choose one interpetation:") uris ;; let input_or_locate_uri ~title = let uri = ref None in let window = GWindow.window ~width:400 ~modal:true ~title ~border_width:2 () in let vbox = GPack.vbox ~packing:window#add () in let hbox1 = GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in let _ = GMisc.label ~text:"Enter a valid URI:" ~packing:(hbox1#pack ~padding:5) () in let manual_input = GEdit.entry ~editable:true ~packing:(hbox1#pack ~expand:true ~fill:true ~padding:5) () in let checkb = GButton.button ~label:"Check" ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in let _ = checkb#misc#set_sensitive false in let hbox2 = GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in let _ = GMisc.label ~text:"You can also enter an indentifier to locate:" ~packing:(hbox2#pack ~padding:5) () in let locate_input = GEdit.entry ~editable:true ~packing:(hbox2#pack ~expand:true ~fill:true ~padding:5) () in let locateb = GButton.button ~label:"Locate" ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5) () in let _ = locateb#misc#set_sensitive false in let hbox3 = GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in let okb = GButton.button ~label:"Ok" ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in let _ = okb#misc#set_sensitive false in let cancelb = GButton.button ~label:"Cancel" ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in ignore (window#connect#destroy GMain.Main.quit) ; ignore (cancelb#connect#clicked (function () -> uri := None ; window#destroy ())) ; let check_callback () = let outputhtml = ((rendering_window ())#outputhtml(* : GHtml.xmhtml*)) in let uri = "cic:" ^ manual_input#text in try ignore (Getter.resolve (UriManager.uri_of_string uri)) ; output_html outputhtml (`Msg (`T "OK")) ; true with Getter.Unresolved -> output_html outputhtml (`Error (`T ("URI " ^ uri ^ " does not correspond to any object."))) ; false | UriManager.IllFormedUri _ -> output_html outputhtml (`Error (`T ("URI " ^ uri ^ " is not well-formed."))) ; false | e -> output_html outputhtml (`Error (`T (Printexc.to_string e))) ; false in ignore (okb#connect#clicked (function () -> if check_callback () then begin uri := Some manual_input#text ; window#destroy () end )) ; ignore (checkb#connect#clicked (function () -> ignore (check_callback ()))) ; ignore (manual_input#connect#changed (fun _ -> if manual_input#text = "" then begin checkb#misc#set_sensitive false ; okb#misc#set_sensitive false end else begin checkb#misc#set_sensitive true ; okb#misc#set_sensitive true end)); ignore (locate_input#connect#changed (fun _ -> locateb#misc#set_sensitive (locate_input#text <> ""))) ; ignore (locateb#connect#clicked (function () -> let id = locate_input#text in manual_input#set_text (locate_callback id) ; locate_input#delete_text 0 (String.length id) )) ; window#show () ; GtkThread.main (); match !uri with None -> raise NoChoice | Some uri -> UriManager.uri_of_string ("cic:" ^ uri) ;; exception AmbiguousInput;; (* A WIDGET TO ENTER CIC TERMS *) module ChosenTermEditor = TexTermEditor;; module ChosenTextualParser0 = TexCicTextualParser0;; (* module ChosenTermEditor = TermEditor;; module ChosenTextualParser0 = CicTextualParser0;; *) module Callbacks = struct let get_metasenv () = !ChosenTextualParser0.metasenv let set_metasenv metasenv = ChosenTextualParser0.metasenv := metasenv let output_html msg = output_html (outputhtml ()) (`Msg (`T msg));; let interactive_user_uri_choice = fun ~selection_mode ?ok ?enable_button_for_non_vars ~title ~msg ~id -> interactive_user_uri_choice ~selection_mode ?ok ?enable_button_for_non_vars ~title ~msg;; let interactive_interpretation_choice = interactive_interpretation_choice;; let input_or_locate_uri = input_or_locate_uri;; end ;; module TexTermEditor' = ChosenTermEditor.Make(Callbacks);; (* OTHER FUNCTIONS *) let locate () = let inputt = ((rendering_window ())#inputt : TermEditor.term_editor) in let outputhtml = ((rendering_window ())#outputhtml(* : GHtml.xmhtml*)) in try match GToolbox.input_string ~title:"Locate" "Enter an identifier to locate:" with None -> raise NoChoice | Some input -> let uri = locate_callback input in inputt#set_term uri with e -> output_html outputhtml (`Error (`T (Printexc.to_string e))) ;; exception UriAlreadyInUse;; exception NotAUriToAConstant;; let new_inductive () = let inputt = ((rendering_window ())#inputt : TermEditor.term_editor) in let outputhtml = ((rendering_window ())#outputhtml(* : GHtml.xmhtml*)) in let output = ((rendering_window ())#output : TermViewer.proof_viewer) in let notebook = (rendering_window ())#notebook in let chosen = ref false in let inductive = ref true in let paramsno = ref 0 in let get_uri = ref (function _ -> assert false) in let get_base_uri = ref (function _ -> assert false) in let get_names = ref (function _ -> assert false) in let get_types_and_cons = ref (function _ -> assert false) in let get_context_and_subst = ref (function _ -> assert false) in let window = GWindow.window ~width:600 ~modal:true ~position:`CENTER ~title:"New Block of Mutual (Co)Inductive Definitions" ~border_width:2 () in let vbox = GPack.vbox ~packing:window#add () in let hbox = GPack.hbox ~border_width:0 ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in let _ = GMisc.label ~text:"Enter the URI for the new block:" ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in let uri_entry = GEdit.entry ~editable:true ~packing:(hbox#pack ~expand:true ~fill:true ~padding:5) () in let hbox0 = GPack.hbox ~border_width:0 ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in let _ = GMisc.label ~text: "Enter the number of left parameters in every arity and constructor type:" ~packing:(hbox0#pack ~expand:false ~fill:false ~padding:5) () in let paramsno_entry = GEdit.entry ~editable:true ~text:"0" ~packing:(hbox0#pack ~expand:true ~fill:true ~padding:5) () in let hbox1 = GPack.hbox ~border_width:0 ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in let _ = GMisc.label ~text:"Are the definitions inductive or coinductive?" ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in let inductiveb = GButton.radio_button ~label:"Inductive" ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in let coinductiveb = GButton.radio_button ~label:"Coinductive" ~group:inductiveb#group ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in let hbox2 = GPack.hbox ~border_width:0 ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in let _ = GMisc.label ~text:"Enter the list of the names of the types:" ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5) () in let names_entry = GEdit.entry ~editable:true ~packing:(hbox2#pack ~expand:true ~fill:true ~padding:5) () in let hboxn = GPack.hbox ~border_width:0 ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in let okb = GButton.button ~label:"> Next" ~packing:(hboxn#pack ~expand:false ~fill:false ~padding:5) () in let _ = okb#misc#set_sensitive true in let cancelb = GButton.button ~label:"Abort" ~packing:(hboxn#pack ~expand:false ~fill:false ~padding:5) () in ignore (window#connect#destroy GMain.Main.quit) ; ignore (cancelb#connect#clicked window#destroy) ; (* First phase *) let rec phase1 () = ignore (okb#connect#clicked (function () -> try let uristr = "cic:" ^ uri_entry#text in let namesstr = names_entry#text in let paramsno' = int_of_string (paramsno_entry#text) in match Str.split (Str.regexp " +") namesstr with [] -> assert false | (he::tl) as names -> let uri = UriManager.uri_of_string (uristr ^ "/" ^ he ^ ".ind") in begin try ignore (Getter.resolve uri) ; raise UriAlreadyInUse with Getter.Unresolved -> get_uri := (function () -> uri) ; get_names := (function () -> names) ; inductive := inductiveb#active ; paramsno := paramsno' ; phase2 () end with e -> output_html outputhtml (`Error (`T (Printexc.to_string e))) )) (* Second phase *) and phase2 () = let type_widgets = List.map (function name -> let frame = GBin.frame ~label:name ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in let vbox = GPack.vbox ~packing:frame#add () in let hbox = GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false) () in let _ = GMisc.label ~text:("Enter its type:") ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in let scrolled_window = GBin.scrolled_window ~border_width:5 ~packing:(vbox#pack ~expand:true ~padding:0) () in let newinputt = TexTermEditor'.term_editor mqi_handle ~width:400 ~height:20 ~packing:scrolled_window#add ~share_id_to_uris_with:inputt () ~isnotempty_callback: (function b -> (*non_empty_type := b ;*) okb#misc#set_sensitive true) (*(b && uri_entry#text <> ""))*) in let hbox = GPack.hbox ~border_width:0 ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in let _ = GMisc.label ~text:("Enter the list of its constructors:") ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in let cons_names_entry = GEdit.entry ~editable:true ~packing:(hbox#pack ~expand:true ~fill:true ~padding:5) () in (newinputt,cons_names_entry) ) (!get_names ()) in vbox#remove hboxn#coerce ; let hboxn = GPack.hbox ~border_width:0 ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in let okb = GButton.button ~label:"> Next" ~packing:(hboxn#pack ~expand:false ~fill:false ~padding:5) () in let cancelb = GButton.button ~label:"Abort" ~packing:(hboxn#pack ~expand:false ~fill:false ~padding:5) () in ignore (cancelb#connect#clicked window#destroy) ; ignore (okb#connect#clicked (function () -> try let names = !get_names () in let types_and_cons = List.map2 (fun name (newinputt,cons_names_entry) -> let consnamesstr = cons_names_entry#text in let cons_names = Str.split (Str.regexp " +") consnamesstr in let metasenv,expr = newinputt#get_metasenv_and_term ~context:[] ~metasenv:[] in match metasenv with [] -> expr,cons_names | _ -> raise AmbiguousInput ) names type_widgets in let uri = !get_uri () in let _ = (* Let's see if so far the definition is well-typed *) let params = [] in let paramsno = 0 in (* To test if the arities of the inductive types are well *) (* typed, we check the inductive block definition where *) (* no constructor is given to each type. *) let tys = List.map2 (fun name (ty,cons) -> (name, !inductive, ty, [])) names types_and_cons in CicTypeChecker.typecheck_mutual_inductive_defs uri (tys,params,paramsno) in get_context_and_subst := (function () -> let i = ref 0 in List.fold_left2 (fun (context,subst) name (ty,_) -> let res = (Some (Cic.Name name, Cic.Decl ty))::context, (Cic.MutInd (uri,!i,[]))::subst in incr i ; res ) ([],[]) names types_and_cons) ; let types_and_cons' = List.map2 (fun name (ty,cons) -> (name, !inductive, ty, phase3 name cons)) names types_and_cons in get_types_and_cons := (function () -> types_and_cons') ; chosen := true ; window#destroy () with e -> output_html outputhtml (`Error (`T (Printexc.to_string e))) )) (* Third phase *) and phase3 name cons = let get_cons_types = ref (function () -> assert false) in let window2 = GWindow.window ~width:600 ~modal:true ~position:`CENTER ~title:(name ^ " Constructors") ~border_width:2 () in let vbox = GPack.vbox ~packing:window2#add () in let cons_type_widgets = List.map (function consname -> let hbox = GPack.hbox ~border_width:0 ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in let _ = GMisc.label ~text:("Enter the type of " ^ consname ^ ":") ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in let scrolled_window = GBin.scrolled_window ~border_width:5 ~packing:(vbox#pack ~expand:true ~padding:0) () in let newinputt = TexTermEditor'.term_editor mqi_handle ~width:400 ~height:20 ~packing:scrolled_window#add ~share_id_to_uris_with:inputt () ~isnotempty_callback: (function b -> (* (*non_empty_type := b ;*) okb#misc#set_sensitive true) (*(b && uri_entry#text <> ""))*) *)()) in newinputt ) cons in let hboxn = GPack.hbox ~border_width:0 ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in let okb = GButton.button ~label:"> Next" ~packing:(hboxn#pack ~expand:false ~fill:false ~padding:5) () in let _ = okb#misc#set_sensitive true in let cancelb = GButton.button ~label:"Abort" ~packing:(hboxn#pack ~expand:false ~fill:false ~padding:5) () in ignore (window2#connect#destroy GMain.Main.quit) ; ignore (cancelb#connect#clicked window2#destroy) ; ignore (okb#connect#clicked (function () -> try chosen := true ; let context,subst= !get_context_and_subst () in let cons_types = List.map2 (fun name inputt -> let metasenv,expr = inputt#get_metasenv_and_term ~context ~metasenv:[] in match metasenv with [] -> let undebrujined_expr = List.fold_left (fun expr t -> CicSubstitution.subst t expr) expr subst in name, undebrujined_expr | _ -> raise AmbiguousInput ) cons cons_type_widgets in get_cons_types := (function () -> cons_types) ; window2#destroy () with e -> output_html outputhtml (`Error (`T (Printexc.to_string e))) )) ; window2#show () ; GtkThread.main (); let okb_pressed = !chosen in chosen := false ; if (not okb_pressed) then begin window#destroy () ; assert false (* The control never reaches this point *) end else (!get_cons_types ()) in phase1 () ; (* No more phases left or Abort pressed *) window#show () ; GtkThread.main (); window#destroy () ; if !chosen then try let uri = !get_uri () in (*CSC: Da finire *) let params = [] in let tys = !get_types_and_cons () in let obj = Cic.InductiveDefinition(tys,params,!paramsno) in begin try prerr_endline (CicPp.ppobj obj) ; CicTypeChecker.typecheck_mutual_inductive_defs uri (tys,params,!paramsno) ; with e -> prerr_endline "Offending mutual (co)inductive type declaration:" ; prerr_endline (CicPp.ppobj obj) ; end ; (* We already know that obj is well-typed. We need to add it to the *) (* environment in order to compute the inner-types without having to *) (* debrujin it or having to modify lots of other functions to avoid *) (* asking the environment for the MUTINDs we are defining now. *) CicEnvironment.put_inductive_definition uri obj ; save_obj uri obj ; show_in_show_window_obj uri obj with e -> output_html outputhtml (`Error (`T (Printexc.to_string e))) ;; let new_proof () = let inputt = ((rendering_window ())#inputt : TermEditor.term_editor) in let outputhtml = ((rendering_window ())#outputhtml(* : GHtml.xmhtml*)) in let output = ((rendering_window ())#output : TermViewer.proof_viewer) in let notebook = (rendering_window ())#notebook in let chosen = ref false in let get_metasenv_and_term = ref (function _ -> assert false) in let get_uri = ref (function _ -> assert false) in let non_empty_type = ref false in let window = GWindow.window ~width:600 ~modal:true ~title:"New Proof or Definition" ~border_width:2 () in let vbox = GPack.vbox ~packing:window#add () in let hbox = GPack.hbox ~border_width:0 ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in let _ = GMisc.label ~text:"Enter the URI for the new theorem or definition:" ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in let uri_entry = GEdit.entry ~editable:true ~packing:(hbox#pack ~expand:true ~fill:true ~padding:5) () in uri_entry#set_text dummy_uri; uri_entry#select_region ~start:1 ~stop:(String.length dummy_uri); let hbox1 = GPack.hbox ~border_width:0 ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in let _ = GMisc.label ~text:"Enter the theorem or definition type:" ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in let scrolled_window = GBin.scrolled_window ~border_width:5 ~packing:(vbox#pack ~expand:true ~padding:0) () in (* the content of the scrolled_window is moved below (see comment) *) let hbox = GPack.hbox ~border_width:0 ~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 _ = okb#misc#set_sensitive false in let cancelb = GButton.button ~label:"Cancel" ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in (* moved here to have visibility of the ok button *) let newinputt = TexTermEditor'.term_editor mqi_handle ~width:400 ~height:100 ~packing:scrolled_window#add ~share_id_to_uris_with:inputt () ~isnotempty_callback: (function b -> non_empty_type := b ; okb#misc#set_sensitive (b && uri_entry#text <> "")) in let _ = let xxx = inputt#get_as_string in prerr_endline ("######################## " ^ xxx) ; newinputt#set_term xxx ; (* newinputt#set_term inputt#get_as_string ; *) inputt#reset in let _ = uri_entry#connect#changed (function () -> okb#misc#set_sensitive (!non_empty_type && uri_entry#text <> "")) in ignore (window#connect#destroy GMain.Main.quit) ; ignore (cancelb#connect#clicked window#destroy) ; ignore (okb#connect#clicked (function () -> chosen := true ; try let metasenv,parsed = newinputt#get_metasenv_and_term [] [] in let uristr = "cic:" ^ uri_entry#text in let uri = UriManager.uri_of_string uristr in if String.sub uristr (String.length uristr - 4) 4 <> ".con" then raise NotAUriToAConstant else begin try ignore (Getter.resolve uri) ; raise UriAlreadyInUse with Getter.Unresolved -> get_metasenv_and_term := (function () -> metasenv,parsed) ; get_uri := (function () -> uri) ; window#destroy () end with e -> output_html outputhtml (`Error (`T (Printexc.to_string e))) )) ; window#show () ; GtkThread.main (); if !chosen then try let metasenv,expr = !get_metasenv_and_term () in let _ = CicTypeChecker.type_of_aux' metasenv [] expr in ProofEngine.set_proof (Some (!get_uri (), (1,[],expr)::metasenv, Cic.Meta (1,[]), expr)) ; set_proof_engine_goal (Some 1) ; refresh_goals notebook ; refresh_proof output ; !save_set_sensitive true ; inputt#reset ; ProofEngine.intros ~mk_fresh_name_callback () ; refresh_goals notebook ; refresh_proof output with InvokeTactics.RefreshSequentException e -> output_html outputhtml (`Error (`T ("Exception raised during the refresh of the " ^ "sequent: " ^ Printexc.to_string e))) | InvokeTactics.RefreshProofException e -> output_html outputhtml (`Error (`T ("Exception raised during the refresh of the " ^ "proof: " ^ Printexc.to_string e))) | e -> output_html outputhtml (`Error (`T (Printexc.to_string e))) ;; let check_term_in_scratch scratch_window metasenv context expr = try let ty = CicTypeChecker.type_of_aux' metasenv context expr in let expr = Cic.Cast (expr,ty) in scratch_window#show () ; scratch_window#set_term expr ; scratch_window#set_context context ; scratch_window#set_metasenv metasenv ; scratch_window#sequent_viewer#load_sequent metasenv (111,context,expr) with e -> print_endline ("? " ^ CicPp.ppterm expr) ; raise e ;; let check scratch_window () = let inputt = ((rendering_window ())#inputt : TermEditor.term_editor) in let outputhtml = ((rendering_window ())#outputhtml(* : GHtml.xmhtml*)) in let metasenv = match ProofEngine.get_proof () with None -> [] | Some (_,metasenv,_,_) -> metasenv in let context = match !ProofEngine.goal with None -> [] | Some metano -> let (_,canonical_context,_) = List.find (function (m,_,_) -> m=metano) metasenv in canonical_context in try let metasenv',expr = inputt#get_metasenv_and_term context metasenv in check_term_in_scratch scratch_window metasenv' context expr with e -> output_html outputhtml (`Error (`T (Printexc.to_string e))) ;; let show () = let outputhtml = ((rendering_window ())#outputhtml(* : GHtml.xmhtml*)) in try show_in_show_window_uri (input_or_locate_uri ~title:"Show") with e -> output_html outputhtml (`Error (`T (Printexc.to_string e))) ;; exception NotADefinition;; let open_ () = let outputhtml = ((rendering_window ())#outputhtml(* : GHtml.xmhtml*)) in 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 CicTypeChecker.typecheck uri ; let metasenv,bo,ty = match CicEnvironment.get_cooked_obj 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 (uri, metasenv, bo, ty)) ; set_proof_engine_goal None ; refresh_goals notebook ; refresh_proof output ; !save_set_sensitive true with InvokeTactics.RefreshSequentException e -> output_html outputhtml (`Error (`T ("Exception raised during the refresh of the " ^ "sequent: " ^ Printexc.to_string e))) | InvokeTactics.RefreshProofException e -> output_html outputhtml (`Error (`T ("Exception raised during the refresh of the " ^ "proof: " ^ Printexc.to_string e))) | e -> output_html outputhtml (`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 MQueryMisc.cic_textual_parser_uri_of_string (MQueryMisc.wrong_xpointer_format_from_wrong_xpointer_format' uristr) with CicTextualParser0.ConUri uri | CicTextualParser0.VarUri uri | CicTextualParser0.IndTyUri (uri,_) | CicTextualParser0.IndConUri (uri,_,_) -> show_in_show_window_uri uri ) ) ; 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 let outputhtml = ((rendering_window ())#outputhtml(* : GHtml.xmhtml*)) in try let metasenv,expr = 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 -> output_html outputhtml (`Error (`T (Printexc.to_string e))) ;; let insertQuery () = let outputhtml = ((rendering_window ())#outputhtml(* : GHtml.xmhtml*)) in 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 -> output_html outputhtml (`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 else List.nth list_of_must n ;; let searchPattern () = let inputt = ((rendering_window ())#inputt : TermEditor.term_editor) in let outputhtml = ((rendering_window ())#outputhtml(* : GHtml.xmhtml*)) in try let proof = match ProofEngine.get_proof () with None -> assert false | Some proof -> proof in match !ProofEngine.goal with | None -> () | Some metano -> let uris' = TacticChaser.matchConclusion mqi_handle ~output_html:(fun m -> output_html outputhtml (`Msg (`T m))) ~choose_must () ~status:(proof, metano) in let uri' = user_uri_choice ~title:"Ambiguous input." ~msg: "Many lemmas can be successfully applied. Please, choose one:" uris' in inputt#set_term uri' ; InvokeTactics'.apply () with e -> output_html outputhtml (`Error (`T (Printexc.to_string e))) ;; let choose_selection mmlwidget (element : Gdome.element option) = let module G = Gdome in prerr_endline "Il bandolo" ; let rec aux element = if element#hasAttributeNS ~namespaceURI:Misc.helmns ~localName:(G.domString "xref") then mmlwidget#set_selection (Some element) else try match element#get_parentNode with None -> assert false (*CSC: OCAML DIVERGES! | Some p -> aux (new G.element_of_node p) *) | Some p -> aux (new Gdome.element_of_node p) with GdomeInit.DOMCastException _ -> prerr_endline "******* trying to select above the document root ********" in match element with Some x -> aux x | None -> mmlwidget#set_selection None ;; (* STUFF TO BUILD THE GTK INTERFACE *) (* Stuff for the widget settings *) (* let export_to_postscript output = let lastdir = ref (Unix.getcwd ()) in function () -> match GToolbox.select_file ~title:"Export to PostScript" ~dir:lastdir ~filename:"screenshot.ps" () with None -> () | Some filename -> (output :> GMathView.math_view)#export_to_postscript ~filename:filename (); ;; *) (* let activate_t1 output button_set_anti_aliasing button_set_transparency export_to_postscript_menu_item button_t1 () = let is_set = button_t1#active in output#set_font_manager_type ~fm_type:(if is_set then `font_manager_t1 else `font_manager_gtk) ; if is_set then begin button_set_anti_aliasing#misc#set_sensitive true ; button_set_transparency#misc#set_sensitive true ; export_to_postscript_menu_item#misc#set_sensitive true ; end else begin button_set_anti_aliasing#misc#set_sensitive false ; button_set_transparency#misc#set_sensitive false ; export_to_postscript_menu_item#misc#set_sensitive false ; end ;; let set_anti_aliasing output button_set_anti_aliasing () = output#set_anti_aliasing button_set_anti_aliasing#active ;; let set_transparency output button_set_transparency () = output#set_transparency button_set_transparency#active ;; *) let changefont output font_size_spinb () = output#set_font_size font_size_spinb#value_as_int ;; let set_log_verbosity output log_verbosity_spinb () = output#set_log_verbosity log_verbosity_spinb#value_as_int ;; class settings_window output sw export_to_postscript_menu_item selection_changed_callback = let settings_window = GWindow.window ~title:"GtkMathView settings" () in let vbox = GPack.vbox ~packing:settings_window#add () in let table = GPack.table ~rows:1 ~columns:3 ~homogeneous:false ~row_spacings:5 ~col_spacings:5 ~border_width:5 ~packing:vbox#add () in let button_t1 = GButton.toggle_button ~label:"activate t1 fonts" ~packing:(table#attach ~left:0 ~top:0) () in let button_set_anti_aliasing = GButton.toggle_button ~label:"set_anti_aliasing" ~packing:(table#attach ~left:0 ~top:1) () in let button_set_transparency = GButton.toggle_button ~label:"set_transparency" ~packing:(table#attach ~left:2 ~top:1) () in let table = GPack.table ~rows:2 ~columns:2 ~homogeneous:false ~row_spacings:5 ~col_spacings:5 ~border_width:5 ~packing:vbox#add () in let font_size_label = GMisc.label ~text:"font size:" ~packing:(table#attach ~left:0 ~top:0 ~expand:`NONE) () in let font_size_spinb = let sadj = GData.adjustment ~value:(float_of_int output#get_font_size) ~lower:5.0 ~upper:50.0 ~step_incr:1.0 () in GEdit.spin_button ~adjustment:sadj ~packing:(table#attach ~left:1 ~top:0 ~fill:`NONE) () in let log_verbosity_label = GMisc.label ~text:"log verbosity:" ~packing:(table#attach ~left:0 ~top:1) () in let log_verbosity_spinb = let sadj = GData.adjustment ~value:0.0 ~lower:0.0 ~upper:3.0 ~step_incr:1.0 () in GEdit.spin_button ~adjustment:sadj ~packing:(table#attach ~left:1 ~top:1) () in let hbox = GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in let closeb = GButton.button ~label:"Close" ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in object(self) method show = settings_window#show initializer button_set_anti_aliasing#misc#set_sensitive false ; button_set_transparency#misc#set_sensitive false ; (* Signals connection *) (* ignore(button_t1#connect#clicked (activate_t1 output button_set_anti_aliasing button_set_transparency export_to_postscript_menu_item button_t1)) ; *) ignore(font_size_spinb#connect#changed (changefont output font_size_spinb)) ; (* ignore(button_set_anti_aliasing#connect#toggled (set_anti_aliasing output button_set_anti_aliasing)); ignore(button_set_transparency#connect#toggled (set_transparency output button_set_transparency)) ; *) ignore(log_verbosity_spinb#connect#changed (set_log_verbosity output log_verbosity_spinb)) ; ignore(closeb#connect#clicked settings_window#misc#hide) end;; (* Scratch window *) class scratch_window = let window = GWindow.window ~title:"MathML viewer" ~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 whdb = GButton.button ~label:"Whd" ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in let reduceb = GButton.button ~label:"Reduce" ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in let simplb = GButton.button ~label:"Simpl" ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in let scrolled_window = GBin.scrolled_window ~border_width:10 ~packing:(vbox#pack ~expand:true ~padding:5) () in let sequent_viewer = TermViewer.sequent_viewer ~packing:(scrolled_window#add) ~width:400 ~height:280 () in object(self) val mutable term = Cic.Rel 1 (* dummy value *) val mutable context = ([] : Cic.context) (* dummy value *) val mutable metasenv = ([] : Cic.metasenv) (* dummy value *) method sequent_viewer = sequent_viewer method show () = window#misc#hide () ; window#show () method term = term method set_term t = term <- t method context = context method set_context t = context <- t method metasenv = metasenv method set_metasenv t = metasenv <- t initializer ignore (sequent_viewer#connect#selection_changed (choose_selection sequent_viewer)); ignore(window#event#connect#delete (fun _ -> window#misc#hide () ; true )) ; ignore(whdb#connect#clicked InvokeTactics'.whd_in_scratch) ; ignore(reduceb#connect#clicked InvokeTactics'.reduce_in_scratch) ; ignore(simplb#connect#clicked InvokeTactics'.simpl_in_scratch) end;; let open_contextual_menu_for_selected_terms mmlwidget infos = let button = GdkEvent.Button.button infos in let terms_selected = List.length mmlwidget#get_selections > 0 in if button = 3 then begin let time = GdkEvent.Button.time infos in let menu = GMenu.menu () in let f = new GMenu.factory menu in let whd_menu_item = f#add_item "Whd" ~key:GdkKeysyms._W ~callback:InvokeTactics'.whd in let reduce_menu_item = f#add_item "Reduce" ~key:GdkKeysyms._R ~callback:InvokeTactics'.reduce in let simpl_menu_item = f#add_item "Simpl" ~key:GdkKeysyms._S ~callback:InvokeTactics'.simpl in let _ = f#add_separator () in let generalize_menu_item = f#add_item "Generalize" ~key:GdkKeysyms._G ~callback:InvokeTactics'.generalize in let _ = f#add_separator () in let clear_menu_item = f#add_item "Clear" ~key:GdkKeysyms._C ~callback:InvokeTactics'.clear in let clearbody_menu_item = f#add_item "ClearBody" ~key:GdkKeysyms._B ~callback:InvokeTactics'.clearbody in whd_menu_item#misc#set_sensitive terms_selected ; reduce_menu_item#misc#set_sensitive terms_selected ; simpl_menu_item#misc#set_sensitive terms_selected ; generalize_menu_item#misc#set_sensitive terms_selected ; clear_menu_item#misc#set_sensitive terms_selected ; clearbody_menu_item#misc#set_sensitive terms_selected ; menu#popup ~button ~time end ; true ;; class page () = let vbox1 = GPack.vbox () in object(self) val mutable proofw_ref = None val mutable compute_ref = None method proofw = Lazy.force self#compute ; match proofw_ref with None -> assert false | Some proofw -> proofw method content = vbox1 method compute = match compute_ref with None -> assert false | Some compute -> compute initializer compute_ref <- Some (lazy ( let scrolled_window1 = GBin.scrolled_window ~border_width:10 ~packing:(vbox1#pack ~expand:true ~padding:5) () in let proofw = TermViewer.sequent_viewer ~width:400 ~height:275 ~packing:(scrolled_window1#add) () in let _ = proofw_ref <- Some proofw in let hbox3 = GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in let ringb = GButton.button ~label:"Ring" ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in let fourierb = GButton.button ~label:"Fourier" ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in let reflexivityb = GButton.button ~label:"Reflexivity" ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in let symmetryb = GButton.button ~label:"Symmetry" ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in let assumptionb = GButton.button ~label:"Assumption" ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in let contradictionb = GButton.button ~label:"Contradiction" ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in let hbox4 = GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in let existsb = GButton.button ~label:"Exists" ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in let splitb = GButton.button ~label:"Split" ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in let leftb = GButton.button ~label:"Left" ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in let rightb = GButton.button ~label:"Right" ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in let searchpatternb = GButton.button ~label:"SearchPattern_Apply" ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in let hbox5 = GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in let exactb = GButton.button ~label:"Exact" ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in let introsb = GButton.button ~label:"Intros" ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in let applyb = GButton.button ~label:"Apply" ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in let elimintrossimplb = GButton.button ~label:"ElimIntrosSimpl" ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in let elimtypeb = GButton.button ~label:"ElimType" ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in let foldwhdb = GButton.button ~label:"Fold_whd" ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in let foldreduceb = GButton.button ~label:"Fold_reduce" ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in let hbox6 = GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in let foldsimplb = GButton.button ~label:"Fold_simpl" ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in let cutb = GButton.button ~label:"Cut" ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in let changeb = GButton.button ~label:"Change" ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in let letinb = GButton.button ~label:"Let ... In" ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in let rewritesimplb = GButton.button ~label:"RewriteSimpl ->" ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in let rewritebacksimplb = GButton.button ~label:"RewriteSimpl <-" ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in let hbox7 = GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in let absurdb = GButton.button ~label:"Absurd" ~packing:(hbox7#pack ~expand:false ~fill:false ~padding:5) () in let decomposeb = GButton.button ~label:"Decompose" ~packing:(hbox7#pack ~expand:false ~fill:false ~padding:5) () in let transitivityb = GButton.button ~label:"Transitivity" ~packing:(hbox7#pack ~expand:false ~fill:false ~padding:5) () in let replaceb = GButton.button ~label:"Replace" ~packing:(hbox7#pack ~expand:false ~fill:false ~padding:5) () in let injectionb = GButton.button ~label:"Injection" ~packing:(hbox7#pack ~expand:false ~fill:false ~padding:5) () in let discriminateb = GButton.button ~label:"Discriminate" ~packing:(hbox7#pack ~expand:false ~fill:false ~padding:5) () in (* Zack: spostare in una toolbar let generalizeb = GButton.button ~label:"Generalize" ~packing:(hbox7#pack ~expand:false ~fill:false ~padding:5) () in let clearbodyb = GButton.button ~label:"ClearBody" ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in let clearb = GButton.button ~label:"Clear" ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in let whdb = GButton.button ~label:"Whd" ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in let reduceb = GButton.button ~label:"Reduce" ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in let simplb = GButton.button ~label:"Simpl" ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in *) ignore(exactb#connect#clicked InvokeTactics'.exact) ; ignore(applyb#connect#clicked InvokeTactics'.apply) ; ignore(elimintrossimplb#connect#clicked InvokeTactics'.elimintrossimpl) ; ignore(elimtypeb#connect#clicked InvokeTactics'.elimtype) ; ignore(foldwhdb#connect#clicked InvokeTactics'.fold_whd) ; ignore(foldreduceb#connect#clicked InvokeTactics'.fold_reduce) ; ignore(foldsimplb#connect#clicked InvokeTactics'.fold_simpl) ; ignore(cutb#connect#clicked InvokeTactics'.cut) ; ignore(changeb#connect#clicked InvokeTactics'.change) ; ignore(letinb#connect#clicked InvokeTactics'.letin) ; ignore(ringb#connect#clicked InvokeTactics'.ring) ; ignore(fourierb#connect#clicked InvokeTactics'.fourier) ; ignore(rewritesimplb#connect#clicked InvokeTactics'.rewritesimpl) ; ignore(rewritebacksimplb#connect#clicked InvokeTactics'.rewritebacksimpl) ; ignore(replaceb#connect#clicked InvokeTactics'.replace) ; ignore(reflexivityb#connect#clicked InvokeTactics'.reflexivity) ; ignore(symmetryb#connect#clicked InvokeTactics'.symmetry) ; ignore(transitivityb#connect#clicked InvokeTactics'.transitivity) ; ignore(existsb#connect#clicked InvokeTactics'.exists) ; ignore(splitb#connect#clicked InvokeTactics'.split) ; ignore(leftb#connect#clicked InvokeTactics'.left) ; ignore(rightb#connect#clicked InvokeTactics'.right) ; ignore(assumptionb#connect#clicked InvokeTactics'.assumption) ; ignore(absurdb#connect#clicked InvokeTactics'.absurd) ; ignore(contradictionb#connect#clicked InvokeTactics'.contradiction) ; ignore(introsb#connect#clicked InvokeTactics'.intros) ; ignore(decomposeb#connect#clicked InvokeTactics'.decompose) ; ignore(searchpatternb#connect#clicked searchPattern) ; ignore(injectionb#connect#clicked InvokeTactics'.injection) ; ignore(discriminateb#connect#clicked InvokeTactics'.discriminate) ; (* Zack: spostare in una toolbar ignore(whdb#connect#clicked whd) ; ignore(reduceb#connect#clicked reduce) ; ignore(simplb#connect#clicked simpl) ; ignore(clearbodyb#connect#clicked clearbody) ; ignore(clearb#connect#clicked clear) ; ignore(generalizeb#connect#clicked generalize) ; *) ignore(proofw#connect#selection_changed (choose_selection proofw)) ; ignore ((new GObj.event_ops proofw#as_widget)#connect#button_press (open_contextual_menu_for_selected_terms proofw)) ; )) end ;; class empty_page = let vbox1 = GPack.vbox () in let scrolled_window1 = GBin.scrolled_window ~border_width:10 ~packing:(vbox1#pack ~expand:true ~padding:5) () in let proofw = TermViewer.sequent_viewer ~width:400 ~height:275 ~packing:(scrolled_window1#add) () in object(self) method proofw = (assert false : TermViewer.sequent_viewer) method content = vbox1 method compute = (assert false : unit) end ;; let empty_page = new empty_page;; class notebook = object(self) val notebook = GPack.notebook () val pages = ref [] val mutable skip_switch_page_event = false val mutable empty = true method notebook = notebook method add_page n = let new_page = new page () in empty <- false ; pages := !pages @ [n,lazy (setgoal n),new_page] ; notebook#append_page ~tab_label:((GMisc.label ~text:("?" ^ string_of_int n) ())#coerce) new_page#content#coerce method remove_all_pages ~skip_switch_page_event:skip = if empty then notebook#remove_page 0 (* let's remove the empty page *) else List.iter (function _ -> notebook#remove_page 0) !pages ; pages := [] ; skip_switch_page_event <- skip method set_current_page ~may_skip_switch_page_event n = let (_,_,page) = List.find (function (m,_,_) -> m=n) !pages in let new_page = notebook#page_num page#content#coerce in if may_skip_switch_page_event && new_page <> notebook#current_page then skip_switch_page_event <- true ; notebook#goto_page new_page method set_empty_page = empty <- true ; pages := [] ; notebook#append_page ~tab_label:((GMisc.label ~text:"No proof in progress" ())#coerce) empty_page#content#coerce method proofw = let (_,_,page) = List.nth !pages notebook#current_page in page#proofw initializer ignore (notebook#connect#switch_page (function i -> let skip = skip_switch_page_event in skip_switch_page_event <- false ; if not skip then try let (metano,setgoal,page) = List.nth !pages i in set_proof_engine_goal (Some metano) ; Lazy.force (page#compute) ; Lazy.force setgoal; if notify_hbugs_on_goal_change then (*Hbugs.notify *) () with _ -> () )) end ;; let dump_environment () = try let oc = open_out environmentfile in output_html (outputhtml ()) (`Msg (`T "Dumping environment ...")); CicEnvironment.dump_to_channel ~callback:(fun uri -> output_html (outputhtml ()) (`Msg (`T uri))) oc; output_html (outputhtml ()) (`Msg (`T "... done!")) ; close_out oc with exc -> output_html (outputhtml ()) (`Error (`T (Printf.sprintf "

Dump failure, uncaught exception:%s

" (Printexc.to_string exc)))) ;; let restore_environment () = try let ic = open_in environmentfile in output_html (outputhtml ()) (`Msg (`L [`T "Restoring environment ... " ; `BR])); CicEnvironment.restore_from_channel ~callback:(fun uri -> output_html (outputhtml ()) (`Msg (`L [`T uri ; `BR]))) ic; output_html (outputhtml ()) (`Msg (`T "... done!")); close_in ic with exc -> output_html (outputhtml ()) (`Error (`T (Printf.sprintf "

Restore failure, uncaught exception:%s

" (Printexc.to_string exc)))) ;; (* HTML simulator (first in its kind) *) type log_msg = [ `T of string | `L of log_msg list | `BR ] ;; class logger ~width ~height ~packing ~show () = let scrolled_window = GBin.scrolled_window ~packing ~show () in let vadj = scrolled_window#vadjustment in let tv = GText.view ~editable:false ~cursor_visible:false ~width ~height ~packing:(scrolled_window#add) () in let green = tv#buffer#create_tag [`FOREGROUND_SET true ; `FOREGROUND_GDK (Gdk.Color.alloc (Gdk.Color.get_system_colormap ()) (`NAME "green"))] in let red = tv#buffer#create_tag [`FOREGROUND_SET true ; `FOREGROUND_GDK (Gdk.Color.alloc (Gdk.Color.get_system_colormap ()) (`NAME "red"))] in object method log (m : [`Msg of log_msg | `Error of log_msg]) = let process_msg tags = let rec aux = function `T s -> tv#buffer#insert ~tags s | `L l -> List.iter aux l | `BR -> tv#buffer#insert ~tags "\n" in aux in begin match m with `Msg m -> process_msg [green] m | `Error m -> process_msg [red] m end ; vadj#set_value (vadj#upper) end ;; (* Main window *) class rendering_window output (notebook : notebook) = let scratch_window = new scratch_window in let window = GWindow.window ~title:"gTopLevel - Helm's Proof Assistant" ~border_width:0 ~allow_shrink:false () in let vbox_for_menu = GPack.vbox ~packing:window#add () in (* menus *) let handle_box = GBin.handle_box ~border_width:2 ~packing:(vbox_for_menu#pack ~padding:0) () in let menubar = GMenu.menu_bar ~packing:handle_box#add () in let factory0 = new GMenu.factory menubar in let accel_group = factory0#accel_group in (* file menu *) let file_menu = factory0#add_submenu "File" in let factory1 = new GMenu.factory file_menu ~accel_group in (* let export_to_postscript_menu_item = *) let _ = begin let _ = factory1#add_item "New Block of (Co)Inductive Definitions..." ~key:GdkKeysyms._B ~callback:new_inductive in let _ = factory1#add_item "New Proof or Definition..." ~key:GdkKeysyms._N ~callback:new_proof in let reopen_menu_item = factory1#add_item "Reopen a Finished Proof..." ~key:GdkKeysyms._R ~callback:open_ in let qed_menu_item = factory1#add_item "Qed" ~key:GdkKeysyms._E ~callback:qed in ignore (factory1#add_separator ()) ; ignore (factory1#add_item "Load Unfinished Proof..." ~key:GdkKeysyms._L ~callback:load_unfinished_proof) ; let save_menu_item = factory1#add_item "Save Unfinished Proof" ~key:GdkKeysyms._S ~callback:save_unfinished_proof in ignore (factory1#add_separator ()) ; ignore (factory1#add_item "Clear Environment" ~callback:CicEnvironment.empty); ignore (factory1#add_item "Dump Environment" ~callback:dump_environment); ignore (factory1#add_item "Restore Environment" ~callback:restore_environment); ignore (save_set_sensitive := function b -> save_menu_item#misc#set_sensitive b); ignore (!save_set_sensitive false); ignore (qed_set_sensitive:=function b -> qed_menu_item#misc#set_sensitive b); ignore (!qed_set_sensitive false); ignore (factory1#add_separator ()) ; (* let export_to_postscript_menu_item = factory1#add_item "Export to PostScript..." ~callback:(export_to_postscript output) in *) ignore (factory1#add_separator ()) ; ignore (factory1#add_item "Exit" ~key:GdkKeysyms._Q ~callback:GMain.Main.quit) (*; export_to_postscript_menu_item *) end in (* edit menu *) let edit_menu = factory0#add_submenu "Edit Current Proof" in let factory2 = new GMenu.factory edit_menu ~accel_group in let focus_and_proveit_set_sensitive = ref (function _ -> assert false) in let proveit_menu_item = factory2#add_item "Prove It" ~key:GdkKeysyms._I ~callback:(function () -> proveit ();!focus_and_proveit_set_sensitive false) in let focus_menu_item = factory2#add_item "Focus" ~key:GdkKeysyms._F ~callback:(function () -> focus () ; !focus_and_proveit_set_sensitive false) in let _ = focus_and_proveit_set_sensitive := function b -> proveit_menu_item#misc#set_sensitive b ; focus_menu_item#misc#set_sensitive b in let _ = !focus_and_proveit_set_sensitive false in (* edit term menu *) let edit_term_menu = factory0#add_submenu "Edit Term" in let factory5 = new GMenu.factory edit_term_menu ~accel_group in let check_menu_item = factory5#add_item "Check Term" ~key:GdkKeysyms._C ~callback:(check scratch_window) in let _ = check_menu_item#misc#set_sensitive false in (* search menu *) let search_menu = factory0#add_submenu "Search" in let factory4 = new GMenu.factory search_menu ~accel_group in let _ = factory4#add_item "Locate..." ~key:GdkKeysyms._T ~callback:locate in let searchPattern_menu_item = factory4#add_item "SearchPattern..." ~key:GdkKeysyms._D ~callback:completeSearchPattern in let _ = searchPattern_menu_item#misc#set_sensitive false in let show_menu_item = factory4#add_item "Show..." ~key:GdkKeysyms._H ~callback:show in let insert_query_item = factory4#add_item "Insert Query (Experts Only)..." ~key:GdkKeysyms._Y ~callback:insertQuery in (* hbugs menu *) let hbugs_menu = factory0#add_submenu "HBugs" in let factory6 = new GMenu.factory hbugs_menu ~accel_group in let _ = factory6#add_check_item ~active:false ~key:GdkKeysyms._F5 ~callback:(*Hbugs.toggle*)(fun _ -> ()) "HBugs enabled" in let _ = factory6#add_item ~key:GdkKeysyms._Return ~callback:(*Hbugs.notify*)(fun _ -> ()) "(Re)Submit status!" in let _ = factory6#add_separator () in let _ = factory6#add_item ~callback:(*Hbugs.start_web_services*)(fun _ -> ()) "Start Web Services" in let _ = factory6#add_item ~callback:(*Hbugs.stop_web_services*)(fun _ -> ()) "Stop Web Services" in (* settings menu *) let settings_menu = factory0#add_submenu "Settings" in let factory3 = new GMenu.factory settings_menu ~accel_group in let _ = factory3#add_item "Edit Aliases..." ~key:GdkKeysyms._A ~callback:edit_aliases in let _ = factory3#add_separator () in let _ = factory3#add_item "MathML Widget Preferences..." ~key:GdkKeysyms._P ~callback:(function _ -> (settings_window ())#show ()) in let _ = factory3#add_separator () in let _ = factory3#add_item "Reload Stylesheets" ~callback: (function _ -> ApplyStylesheets.reload_stylesheets () ; if ProofEngine.get_proof () <> None then try refresh_goals notebook ; refresh_proof output with InvokeTactics.RefreshSequentException e -> output_html (outputhtml ()) (`Error (`T ("An error occurred while refreshing the " ^ "sequent: " ^ Printexc.to_string e))) ; (*notebook#remove_all_pages ~skip_switch_page_event:false ;*) notebook#set_empty_page | InvokeTactics.RefreshProofException e -> output_html (outputhtml ()) (`Error (`T ("An error occurred while refreshing the proof: " ^ Printexc.to_string e))) ; output#unload ) in (* accel group *) let _ = window#add_accel_group accel_group in (* end of menus *) let hbox0 = GPack.hbox ~packing:(vbox_for_menu#pack ~expand:true ~fill:true ~padding:5) () in let vbox = GPack.vbox ~packing:(hbox0#pack ~expand:true ~fill:true ~padding:5) () in let scrolled_window0 = GBin.scrolled_window ~border_width:10 ~packing:(vbox#pack ~expand:true ~padding:5) () in let _ = scrolled_window0#add output#coerce in let frame = GBin.frame ~label:"Insert Term" ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in let scrolled_window1 = GBin.scrolled_window ~border_width:5 ~packing:frame#add () in let inputt = TexTermEditor'.term_editor mqi_handle ~width:400 ~height:100 ~packing:scrolled_window1#add () ~isnotempty_callback: (function b -> check_menu_item#misc#set_sensitive b ; searchPattern_menu_item#misc#set_sensitive b) in let vboxl = GPack.vbox ~packing:(hbox0#pack ~expand:true ~fill:true ~padding:5) () in let _ = vboxl#pack ~expand:true ~fill:true ~padding:5 notebook#notebook#coerce in let frame = GBin.frame ~shadow_type:`IN ~packing:(vboxl#pack ~expand:true ~padding:5) () in let outputhtml = new logger ~width:400 ~height: 100 ~packing:frame#add ~show:true () in object method outputhtml = outputhtml method inputt = inputt method output = (output : TermViewer.proof_viewer) method scratch_window = scratch_window method notebook = notebook method show = window#show initializer notebook#set_empty_page ; (*export_to_postscript_menu_item#misc#set_sensitive false ;*) check_term := (check_term_in_scratch scratch_window) ; (* signal handlers here *) ignore(output#connect#selection_changed (function elem -> choose_selection output elem ; !focus_and_proveit_set_sensitive true )) ; ignore (output#connect#click (show_in_show_window_callback output)) ; let settings_window = new settings_window output scrolled_window0 (*export_to_postscript_menu_item*)() (choose_selection output) in set_settings_window settings_window ; set_outputhtml outputhtml ; ignore(window#event#connect#delete (fun _ -> GMain.Main.quit () ; true )) ; Logger.log_callback := (Logger.log_to_html ~print_and_flush:(fun m -> (output_html outputhtml (`Msg (`T m))))) end;; (* MAIN *) let initialize_everything () = let module U = Unix in let output = TermViewer.proof_viewer ~width:350 ~height:280 () in let notebook = new notebook in let rendering_window' = new rendering_window output notebook in set_rendering_window rendering_window' ; let print_error_as_html prefix msg = output_html (outputhtml ()) (`Error (`T (prefix ^ msg))) in Gdome_xslt.setErrorCallback (Some (print_error_as_html "XSLT Error: ")); Gdome_xslt.setDebugCallback (Some (print_error_as_html "XSLT Debug Message: ")); rendering_window'#show () ; if restore_environment_on_boot && Sys.file_exists environmentfile then restore_environment (); GtkThread.main () ;; let main () = ignore (GtkMain.Main.init ()) ; initialize_everything () ; MQIC.close mqi_handle(*; Hbugs.quit ()*) ;; try Sys.catch_break true; main (); with Sys.Break -> () (* exit nicely, invoking at_exit functions *)