X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FgTopLevel.ml;h=d3e39351c04804cf06a3c0fe8cfdbd21668fd6b7;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=fa1ad6ea8e242ace2968b1a72659f348d0a034f2;hpb=ee35ccaff9728ecba44c83eed9cb703d9a1f131e;p=helm.git diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml index fa1ad6ea8..d3e39351c 100644 --- a/helm/gTopLevel/gTopLevel.ml +++ b/helm/gTopLevel/gTopLevel.ml @@ -1,4 +1,4 @@ -(* Copyright (C) 2000-2003, HELM Team. +(* Copyright (C) 2000-2004, HELM Team. * * This file is part of HELM, an Hypertextual, Electronic * Library of Mathematics, developed at the Computer Science @@ -20,22 +20,25 @@ * MA 02111-1307, USA. * * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. + * http://helm.cs.unibo.it/ *) -(******************************************************************************) -(* *) -(* PROJECT HELM *) -(* *) -(* Claudio Sacerdoti Coen *) -(* 06/01/2002 *) -(* *) -(* *) -(******************************************************************************) +(*****************************************************************************) +(* *) +(* PROJECT HELM *) +(* *) +(* Claudio Sacerdoti Coen *) +(* 06/01/2002 *) +(* *) +(* *) +(*****************************************************************************) -open Printf;; +let debug_level = ref 1 +let debug_print ?(level = 1) s = if !debug_level >= level then prerr_endline s +let error s = prerr_endline ("E: " ^ s) +let warning s = prerr_endline ("W: " ^ s) -(* DEBUGGING *) +open Printf module MQI = MQueryInterpreter module MQIC = MQIConn @@ -43,40 +46,32 @@ 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 prooffile = - try - Sys.getenv "GTOPLEVEL_PROOFFILE" - with - Not_found -> "/public/currentproof" +(* first of all let's initialize the Helm_registry *) +let _ = + let configuration_file = "gTopLevel.conf.xml" in + if not (Sys.file_exists configuration_file) then begin + eprintf "E: Can't find configuration file '%s'\n" configuration_file; + exit 2 + end; + Helm_registry.load_from configuration_file ;; -let prooffiletype = - try - Sys.getenv "GTOPLEVEL_PROOFFILETYPE" - with - Not_found -> "/public/currentprooftype" -;; +(* GLOBAL CONSTANTS *) -let environmentfile = - try - Sys.getenv "GTOPLEVEL_ENVIRONMENTFILE" - with - Not_found -> "/public/environment" -;; +let mqi_handle = MQIC.init_if_connected () + +let dbd = + Mysql.quick_connect + ~host:(Helm_registry.get "db.host") + ~user:(Helm_registry.get "db.user") + ~database:(Helm_registry.get "db.database") + () let restore_environment_on_boot = true ;; let notify_hbugs_on_goal_change = false ;; +let auto_disambiguation = ref true ;; + (* GLOBAL REFERENCES (USED BY CALLBACKS) *) let check_term = ref (fun _ _ _ -> assert false);; @@ -105,18 +100,6 @@ let set_settings_window,settings_window = ) ;; -exception OutputHtmlNotInitialized;; - -let set_outputhtml,outputhtml = - let outputhtml_ref = ref None in - (function (rw: Ui_logger.html_logger) -> outputhtml_ref := Some rw), - (function () -> - match !outputhtml_ref with - | None -> raise OutputHtmlNotInitialized - | Some outputhtml -> (outputhtml: Ui_logger.html_logger) - ) -;; - exception QedSetSensitiveNotInitialized;; let qed_set_sensitive = ref (function _ -> raise QedSetSensitiveNotInitialized) @@ -138,43 +121,11 @@ let argspec = 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 ?(append_NL = true) (outputhtml: Ui_logger.html_logger) = - outputhtml#log ~append_NL - (* UTILITY FUNCTIONS TO DISAMBIGUATE AN URI *) (* Check window *) -let check_window (outputhtml: Ui_logger.html_logger) uris = +let check_window uris = let window = GWindow.window ~width:800 ~modal:true ~title:"Check" ~border_width:2 () in @@ -193,19 +144,18 @@ let check_window (outputhtml: Ui_logger.html_logger) uris = lazy (let mmlwidget = TermViewer.sequent_viewer + ~mml_of_cic_sequent:ApplyTransformation.mml_of_cic_sequent ~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)) + let term = CicUtil.term_of_uri uri in + (Cic.Cast (term, fst(CicTypeChecker.type_of_aux' [] [] term + CicUniv.empty_ugraph ))) in try mmlwidget#load_sequent [] (111,[],expr) with e -> - output_html outputhtml (`Error (`T (Printexc.to_string e))) + HelmLogger.log (`Error (`T (Printexc.to_string e))) ) ) uris in @@ -217,114 +167,135 @@ let check_window (outputhtml: Ui_logger.html_logger) uris = exception NoChoice;; -let - interactive_user_uri_choice ~(selection_mode:[`MULTIPLE|`SINGLE]) ?(ok="Ok") - ?(enable_button_for_non_vars=false) ~title ~msg uris +let interactive_user_uri_choice + ~(selection_mode:[ `SINGLE | `MULTIPLE ]) + ?(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 + let only_constant_choices = + lazy + (List.filter + (fun uri -> not (String.sub uri (String.length uri - 4) 4 = ".var")) + uris) 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 () ; + if selection_mode <> `SINGLE && !auto_disambiguation then + Lazy.force only_constant_choices + else begin + 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 autob = + GButton.button + ~packing: + (fun w -> + if enable_button_for_non_vars then + hbox#pack ~expand:false ~fill:false ~padding:5 w) + ~label:"Auto" () 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 !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 (autob#connect#clicked (fun () -> + auto_disambiguation := true; + (rendering_window ())#set_auto_disambiguation true; + 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 ; - 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 + 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 + Lazy.force only_constant_choices + else + if List.length !choices > 0 then !choices else raise NoChoice + else + raise NoChoice + end ;; let interactive_interpretation_choice interpretations = @@ -379,7 +350,7 @@ let interactive_interpretation_choice interpretations = GtkThread.main (); match !chosen with None -> raise NoChoice - | Some n -> n + | Some n -> [n] ;; @@ -404,16 +375,16 @@ let 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 ^ + Xml.pp ~gzip:false xmlinnertypes (Some (path ^ ".types.xml")) ; + Http_getter.register' innertypesuri + (Helm_registry.get "local_library.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 ^ + Xml.pp ~gzip:false xml (Some (path ^ ".xml")) ; + Http_getter.register' uri + (Helm_registry.get "local_library.url" ^ Str.replace_first (Str.regexp "^cic:") "" (UriManager.string_of_uri uri) ^ ".xml" ) ; @@ -426,9 +397,9 @@ let None -> assert false | Some bodyuri -> bodyuri in - Xml.pp ~quiet:true bodyxml' (Some (path ^ ".body.xml")) ; - Getter.register bodyuri - (Configuration.annotations_url ^ + Xml.pp ~gzip:false bodyxml' (Some (path ^ ".body.xml")) ; + Http_getter.register' bodyuri + (Helm_registry.get "local_library.url" ^ Str.replace_first (Str.regexp "^cic:") "" (UriManager.string_of_uri bodyuri) ^ ".xml" ) @@ -441,7 +412,7 @@ exception OpenConjecturesStillThere;; exception WrongProof;; let pathname_of_annuri uristring = - Configuration.annotations_dir ^ + Helm_registry.get "local_library.dir" ^ Str.replace_first (Str.regexp "^cic:") "" uristring ;; @@ -454,7 +425,7 @@ let save_obj uri obj = (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 + Cic2acic.acic_object_of_cic_object ~eta_fix:false obj in (* let's save the theorem and register it to the getter *) let pathname = pathname_of_annuri (UriManager.buri_of_uri uri) in @@ -464,41 +435,67 @@ let save_obj uri obj = ;; 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 + match ProofEngine.get_proof () with + None -> assert false + | Some (uri,[],bo,ty) -> + let uri = match uri with Some uri -> uri | _ -> assert false in + (* we want to typecheck in the ENV *) + prerr_endline "-------------> QED"; + let ty_bo,u = + CicTypeChecker.type_of_aux' [] [] bo CicUniv.empty_ugraph in + let b,u1 = CicReduction.are_convertible [] ty_bo ty u in + if b 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 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 + let list_of_universes = + CicUnivUtils.universes_of_obj uri + (Cic.Constant ("",None,ty,[],[])) + in + let u1_clean = CicUniv.clean_ugraph u1 list_of_universes in + let u2 = CicUniv.fill_empty_nodes_with_uri u1_clean uri in + (********************************************** + TASSI: to uncomment whe universes will be ON + ***********************************************) + (* + make_dirs pathname ; + save_object_to_disk uri acic ids_to_inner_sorts + ids_to_inner_types pathname; + *) + (* save the universe graph u2 *) + (* add the object to the env *) + CicEnvironment.add_type_checked_term uri (( + Cic.Constant ((UriManager.name_of_uri uri), + (Some bo),ty,[],[])),u2); + (* FIXME: the variable list!! *) + prerr_endline "-------------> FINE"; + 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))) + let proof_file_type = Helm_registry.get "gtoplevel.proof_file_type" in + let proof_file = Helm_registry.get "gtoplevel.proof_file" in + Xml.pp ~gzip:false xml (Some proof_file_type) ; + HelmLogger.log + (`Msg (`T ("Current proof type saved to " ^ proof_file_type))) ; + Xml.pp ~gzip:false bodyxml (Some proof_file) ; + HelmLogger.log + (`Msg (`T ("Current proof body saved to " ^ proof_file))) ;; (* Used to typecheck the loaded proofs *) @@ -507,11 +504,11 @@ let typecheck_loaded_proof metasenv bo ty = ignore ( List.fold_left (fun metasenv ((_,context,ty) as conj) -> - ignore (T.type_of_aux' metasenv context ty) ; + ignore (T.type_of_aux' metasenv context ty CicUniv.empty_ugraph) ; metasenv @ [conj] ) [] metasenv) ; - ignore (T.type_of_aux' metasenv [] ty) ; - ignore (T.type_of_aux' metasenv [] bo) + ignore (T.type_of_aux' metasenv [] ty CicUniv.empty_ugraph) ; + ignore (T.type_of_aux' metasenv [] bo CicUniv.empty_ugraph) ;; let decompose_uris_choice_callback uris = @@ -519,9 +516,9 @@ let decompose_uris_choice_callback uris = 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) + match CicUtil.term_of_uri uri with + | Cic.MutInd (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" @@ -532,9 +529,9 @@ let decompose_uris_choice_callback uris = ) ;; -let mk_fresh_name_callback context name ~typ = +let mk_fresh_name_callback metasenv context name ~typ = let fresh_name = - match ProofEngineHelpers.mk_fresh_name context name ~typ with + match FreshNamesGenerator.mk_fresh_name ~subst:[] metasenv context name ~typ with Cic.Name fresh_name -> fresh_name | Cic.Anonymous -> assert false in @@ -563,17 +560,19 @@ let refresh_proof (output : TermViewer.proof_viewer) = else Hbugs.notify () ; (*CSC: Wrong: [] is just plainly wrong *) - uri, - (Cic.CurrentProof (UriManager.name_of_uri uri, metasenv, bo, ty, [])) + let uri = match uri with Some uri -> uri | _ -> assert false in + (uri, + Cic.CurrentProof (UriManager.name_of_uri uri,metasenv,bo,ty,[],[])) in - ignore (output#load_proof uri currentproof) + ignore (output#load_proof 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) + debug_print ("Offending proof: " ^ + CicPp.ppobj (Cic.CurrentProof ("questa",metasenv,bo,ty,[],[]))); + raise (InvokeTactics.RefreshProofException e) let set_proof_engine_goal g = ProofEngine.goal := g @@ -618,7 +617,7 @@ let refresh_goals ?(empty_notebook=true) notebook = begin notebook#set_current_page ~may_skip_switch_page_event:true metano ; - notebook#proofw#load_sequent metasenv currentsequent + notebook#proofw#load_sequent metasenv currentsequent ; end with e -> @@ -633,10 +632,13 @@ let metasenv = | 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) + let currentsequent = List.find (function (m,_,_) -> m=metano) metasenv in + debug_print + ("Offending sequent: " ^ SequentPp.TextualPp.print_sequent currentsequent); + raise (InvokeTactics.RefreshSequentException e) +with Not_found -> + debug_print ("Offending sequent " ^ string_of_int metano ^ " unknown."); + raise (InvokeTactics.RefreshSequentException e) module InvokeTacticsCallbacks = struct @@ -654,7 +656,8 @@ module InvokeTacticsCallbacks = 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 + let mqi_handle = mqi_handle + let dbd = dbd end ;; module InvokeTactics' = InvokeTactics.Make (InvokeTacticsCallbacks);; @@ -663,9 +666,7 @@ module InvokeTactics' = InvokeTactics.Make (InvokeTacticsCallbacks);; 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] + | Hbugs_types.Use_apply_Luke term -> check_window [term] | _ -> ()) ;; *) @@ -673,7 +674,6 @@ 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 @@ -684,10 +684,12 @@ let load_unfinished_proof () = 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,_) -> + let proof_file_type = Helm_registry.get "gtoplevel.proof_file_type" in + let proof_file = Helm_registry.get "gtoplevel.proof_file" in + match CicParser.obj_of_xml proof_file_type (Some proof_file) with + Cic.CurrentProof (_,metasenv,bo,ty,_,_) -> typecheck_loaded_proof metasenv bo ty ; - ProofEngine.set_proof (Some (uri, metasenv, bo, ty)) ; + ProofEngine.set_proof (Some (Some uri, metasenv, bo, ty)); refresh_proof output ; set_proof_engine_goal (match metasenv with @@ -695,32 +697,37 @@ let load_unfinished_proof () = | (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))) ; + HelmLogger.log + (`Msg (`T ("Current proof type loaded from " ^ proof_file_type))); + HelmLogger.log + (`Msg (`T ("Current proof body loaded from " ^ proof_file))) ; !save_set_sensitive true; | _ -> assert false with InvokeTactics.RefreshSequentException e -> - output_html outputhtml + HelmLogger.log (`Error (`T ("Exception raised during the refresh of the " ^ "sequent: " ^ Printexc.to_string e))) | InvokeTactics.RefreshProofException e -> - output_html outputhtml + HelmLogger.log (`Error (`T ("Exception raised during the refresh of the " ^ "proof: " ^ Printexc.to_string e))) | e -> - output_html outputhtml + HelmLogger.log (`Error (`T (Printexc.to_string e))) ;; +let clear_aliases () = + let inputt = ((rendering_window ())#inputt : TermEditor.term_editor) in + inputt#environment := + DisambiguatingParser.EnvironmentP3.of_string + DisambiguatingParser.EnvironmentP3.empty +;; + 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 disambiguation_env = inputt#environment in + let chosen_aliases = ref None in let window = GWindow.window ~width:400 ~modal:true ~title:"Edit Aliases..." ~border_width:2 () in @@ -737,72 +744,37 @@ let edit_aliases () = let okb = GButton.button ~label:"Ok" ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in + let clearb = + GButton.button ~label:"Clear" + ~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 (clearb#connect#clicked (fun () -> + input#buffer#set_text DisambiguatingParser.EnvironmentP3.empty)) ; + ignore (okb#connect#clicked (fun () -> + chosen_aliases := Some (input#buffer#get_text ()); + window#destroy ())); 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))) ; + (DisambiguatingParser.EnvironmentP3.to_string !disambiguation_env ^ "\n")); 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) + match !chosen_aliases with + | None -> () + | Some raw_aliases -> + let new_disambiguation_env = + (try + DisambiguatingParser.EnvironmentP3.of_string raw_aliases + with e -> + HelmLogger.log + (`Error (`T + ("Error while parsing aliases: " ^ Printexc.to_string e))); + !disambiguation_env) + in + disambiguation_env := new_disambiguation_env ;; let proveit () = @@ -810,22 +782,21 @@ let proveit () = 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 + HelmLogger.log (`Error (`T ("Exception raised during the refresh of the " ^ "sequent: " ^ Printexc.to_string e))) | InvokeTactics.RefreshProofException e -> - output_html outputhtml + HelmLogger.log (`Error (`T ("Exception raised during the refresh of the " ^ "proof: " ^ Printexc.to_string e))) | e -> - output_html outputhtml + HelmLogger.log (`Error (`T (Printexc.to_string e))) ;; @@ -833,22 +804,21 @@ 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 + HelmLogger.log (`Error (`T ("Exception raised during the refresh of the " ^ "sequent: " ^ Printexc.to_string e))) | InvokeTactics.RefreshProofException e -> - output_html outputhtml + HelmLogger.log (`Error (`T ("Exception raised during the refresh of the " ^ "proof: " ^ Printexc.to_string e))) | e -> - output_html outputhtml + HelmLogger.log (`Error (`T (Printexc.to_string e))) ;; @@ -860,7 +830,6 @@ let setgoal metano = 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 @@ -870,11 +839,11 @@ let setgoal metano = refresh_goals ~empty_notebook:false notebook with InvokeTactics.RefreshSequentException e -> - output_html outputhtml + HelmLogger.log (`Error (`T ("Exception raised during the refresh of the " ^ "sequent: " ^ Printexc.to_string e))) | e -> - output_html outputhtml + HelmLogger.log (`Error (`T (Printexc.to_string e))) ;; @@ -892,37 +861,30 @@ let 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 + let mml,(_,(ids_to_terms,ids_to_father_ids,ids_to_conjectures, + ids_to_hypotheses,_,_)) = + ApplyTransformation.mml_of_cic_object obj in window#set_title (UriManager.string_of_uri uri) ; window#misc#hide () ; window#show () ; - mmlwidget#load_doc mml ; + mmlwidget#load_root mml#get_documentElement ; with e -> - output_html outputhtml + HelmLogger.log (`Error (`T (Printexc.to_string e))) in let show_in_show_window_uri uri = - let obj = CicEnvironment.get_obj uri in + let obj,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in show_in_show_window_obj uri obj in - let show_in_show_window_callback mmlwidget (n : Gdome.element option) _ = + 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 + if n'#hasAttributeNS ~namespaceURI:Misc.xlink_ns ~localName:href then let uri = - (n'#getAttributeNS ~namespaceURI:xlinkns ~localName:href)#to_string + (n'#getAttributeNS ~namespaceURI:Misc.xlink_ns ~localName:href)#to_string in show_in_show_window_uri (UriManager.uri_of_string uri) else @@ -953,23 +915,12 @@ let user_uri_choice ~title ~msg uris = ;; 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; + let uris = MetadataQuery.locate ~dbd id in + HelmLogger.log (`Msg (`T ("Locate Query: " ^ id))) ; + HelmLogger.log (`Msg (`T "Result:")) ; + List.iter (fun uri -> HelmLogger.log (`Msg (`T uri))) uris; user_uri_choice ~title:"Ambiguous input." - ~msg: - ("Ambiguous input \"" ^ id ^ - "\". Please, choose one interpetation:") + ~msg:(sprintf "Ambiguous input \"%s\". Please, choose one interpetation:" id) uris ;; @@ -1017,24 +968,23 @@ let input_or_locate_uri ~title = 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")) ; + ignore (Http_getter.resolve' (UriManager.uri_of_string uri)) ; + HelmLogger.log (`Msg (`T "OK")) ; true with - Getter.Unresolved -> - output_html outputhtml + Http_getter_types.Key_not_found _ -> + HelmLogger.log (`Error (`T ("URI " ^ uri ^ " does not correspond to any object."))) ; false | UriManager.IllFormedUri _ -> - output_html outputhtml + HelmLogger.log (`Error (`T ("URI " ^ uri ^ " is not well-formed."))) ; false | e -> - output_html outputhtml + HelmLogger.log (`Error (`T (Printexc.to_string e))) ; false in @@ -1082,35 +1032,23 @@ exception AmbiguousInput;; (* A WIDGET TO ENTER CIC TERMS *) -module ChosenTermEditor = TexTermEditor;; -module ChosenTextualParser0 = TexCicTextualParser0;; -(* -module ChosenTermEditor = TermEditor;; -module ChosenTextualParser0 = CicTextualParser0;; -*) - -module Callbacks = +module DisambiguateCallbacks = struct - let get_metasenv () = !ChosenTextualParser0.metasenv - let set_metasenv metasenv = ChosenTextualParser0.metasenv := metasenv - - let output_html ?append_NL = output_html ?append_NL (outputhtml ()) 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 + let input_or_locate_uri ~title ?id () = input_or_locate_uri ~title end ;; -module TexTermEditor' = ChosenTermEditor.Make(Callbacks);; +module TermEditor' = ChosenTermEditor.Make (DisambiguateCallbacks);; (* 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:" @@ -1121,7 +1059,7 @@ let locate () = inputt#set_term uri with e -> - output_html outputhtml + HelmLogger.log (`Error (`T (Printexc.to_string e))) ;; @@ -1131,7 +1069,6 @@ 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 @@ -1218,10 +1155,9 @@ let new_inductive () = let uri = UriManager.uri_of_string (uristr ^ "/" ^ he ^ ".ind") in begin try - ignore (Getter.resolve uri) ; + ignore (Http_getter.resolve' uri) ; raise UriAlreadyInUse - with - Getter.Unresolved -> + with Http_getter_types.Key_not_found _ -> get_uri := (function () -> uri) ; get_names := (function () -> names) ; inductive := inductiveb#active ; @@ -1230,7 +1166,7 @@ let new_inductive () = end with e -> - output_html outputhtml + HelmLogger.log (`Error (`T (Printexc.to_string e))) )) (* Second phase *) @@ -1250,10 +1186,10 @@ let new_inductive () = GBin.scrolled_window ~border_width:5 ~packing:(vbox#pack ~expand:true ~padding:0) () in let newinputt = - TexTermEditor'.term_editor - mqi_handle + TermEditor'.term_editor + ~dbd ~width:400 ~height:20 ~packing:scrolled_window#add - ~share_id_to_uris_with:inputt () + ~share_environment_with:inputt () ~isnotempty_callback: (function b -> (*non_empty_type := b ;*) @@ -1292,7 +1228,7 @@ let new_inductive () = (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 = + let metasenv,expr,ugraph = newinputt#get_metasenv_and_term ~context:[] ~metasenv:[] in match metasenv with @@ -1337,7 +1273,7 @@ let new_inductive () = window#destroy () with e -> - output_html outputhtml + HelmLogger.log (`Error (`T (Printexc.to_string e))) )) (* Third phase *) @@ -1362,10 +1298,10 @@ let new_inductive () = GBin.scrolled_window ~border_width:5 ~packing:(vbox#pack ~expand:true ~padding:0) () in let newinputt = - TexTermEditor'.term_editor - mqi_handle + TermEditor'.term_editor + ~dbd ~width:400 ~height:20 ~packing:scrolled_window#add - ~share_id_to_uris_with:inputt () + ~share_environment_with:inputt () ~isnotempty_callback: (function b -> (* (*non_empty_type := b ;*) @@ -1394,7 +1330,7 @@ let new_inductive () = let cons_types = List.map2 (fun name inputt -> - let metasenv,expr = + let metasenv,expr,ugraph = inputt#get_metasenv_and_term ~context ~metasenv:[] in match metasenv with @@ -1411,7 +1347,7 @@ let new_inductive () = window2#destroy () with e -> - output_html outputhtml + HelmLogger.log (`Error (`T (Printexc.to_string e))) )) ; window2#show () ; @@ -1437,33 +1373,39 @@ let new_inductive () = (*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 ; + let obj = Cic.InductiveDefinition(tys,params,!paramsno,[]) in + let u = + begin + try + debug_print (CicPp.ppobj obj); + CicTypeChecker.typecheck_mutual_inductive_defs uri + (tys,params,!paramsno) CicUniv.empty_ugraph + with + e -> + debug_print "Offending mutual (co)inductive type declaration:" ; + debug_print (CicPp.ppobj obj) ; + (* I think we should fail here! *) + CicUniv.empty_ugraph + end + in (* 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 ; + + (* u should be cleaned before adding it to the env *) + CicEnvironment.put_inductive_definition uri (obj,u) ; save_obj uri obj ; + (* TASSI: FIXME we should save the cleaned u here *) show_in_show_window_obj uri obj with e -> - output_html outputhtml + HelmLogger.log (`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 @@ -1509,22 +1451,17 @@ let new_proof () = ~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 + TermEditor'.term_editor + ~dbd ~width:400 ~height:100 ~packing:scrolled_window#add - ~share_id_to_uris_with:inputt () + ~share_environment_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 ; -*) + newinputt#set_term inputt#get_as_string ; inputt#reset in let _ = uri_entry#connect#changed @@ -1538,7 +1475,7 @@ prerr_endline ("######################## " ^ xxx) ; (function () -> chosen := true ; try - let metasenv,parsed = newinputt#get_metasenv_and_term [] [] in + let metasenv,parsed,ugraph = 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 @@ -1546,17 +1483,16 @@ prerr_endline ("######################## " ^ xxx) ; else begin try - ignore (Getter.resolve uri) ; + ignore (Http_getter.resolve' uri) ; raise UriAlreadyInUse - with - Getter.Unresolved -> + with Http_getter_types.Key_not_found _ -> get_metasenv_and_term := (function () -> metasenv,parsed) ; get_uri := (function () -> uri) ; window#destroy () end with e -> - output_html outputhtml + HelmLogger.log (`Error (`T (Printexc.to_string e))) )) ; window#show () ; @@ -1566,7 +1502,7 @@ prerr_endline ("######################## " ^ xxx) ; 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)) ; + (Some (Some (!get_uri ()), (1,[],expr)::metasenv, Cic.Meta (1,[]), expr)); set_proof_engine_goal (Some 1) ; refresh_goals notebook ; refresh_proof output ; @@ -1577,21 +1513,23 @@ prerr_endline ("######################## " ^ xxx) ; refresh_proof output with InvokeTactics.RefreshSequentException e -> - output_html outputhtml + HelmLogger.log (`Error (`T ("Exception raised during the refresh of the " ^ "sequent: " ^ Printexc.to_string e))) | InvokeTactics.RefreshProofException e -> - output_html outputhtml + HelmLogger.log (`Error (`T ("Exception raised during the refresh of the " ^ "proof: " ^ Printexc.to_string e))) | e -> - output_html outputhtml + HelmLogger.log (`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 ty,ugraph = + CicTypeChecker.type_of_aux' metasenv context expr CicUniv.empty_ugraph + in let expr = Cic.Cast (expr,ty) in scratch_window#show () ; scratch_window#set_term expr ; @@ -1606,7 +1544,6 @@ let check_term_in_scratch scratch_window metasenv context expr = 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 -> [] @@ -1622,57 +1559,58 @@ let check scratch_window () = canonical_context in try - let metasenv',expr = inputt#get_metasenv_and_term context metasenv in - check_term_in_scratch scratch_window metasenv' context expr + let metasenv',expr,ugraph = + inputt#get_metasenv_and_term context metasenv + in + check_term_in_scratch scratch_window metasenv' context expr with e -> - output_html outputhtml + HelmLogger.log (`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 + HelmLogger.log (`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 ; + ignore(CicTypeChecker.typecheck uri CicUniv.empty_ugraph); + (* TASSI: typecheck mette la uri nell'env... cosa fa la open_ ?*) 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 + 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 (uri, metasenv, bo, ty)) ; + 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 -> - output_html outputhtml + HelmLogger.log (`Error (`T ("Exception raised during the refresh of the " ^ "sequent: " ^ Printexc.to_string e))) | InvokeTactics.RefreshProofException e -> - output_html outputhtml + HelmLogger.log (`Error (`T ("Exception raised during the refresh of the " ^ "proof: " ^ Printexc.to_string e))) | e -> - output_html outputhtml + HelmLogger.log (`Error (`T (Printexc.to_string e))) ;; @@ -1705,16 +1643,13 @@ let show_query_results results = (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,_,_) -> + 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 () @@ -1914,9 +1849,9 @@ let refine_constraints (must_obj,must_rel,must_sort) = 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 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 = @@ -1926,12 +1861,11 @@ let completeSearchPattern () = show_query_results results with e -> - output_html outputhtml + HelmLogger.log (`Error (`T (Printexc.to_string e))) ;; let insertQuery () = - let outputhtml = ((rendering_window ())#outputhtml(* : GHtml.xmhtml*)) in try let chosen = ref None in let window = @@ -1994,7 +1928,7 @@ let insertQuery () = show_query_results results with e -> - output_html outputhtml + HelmLogger.log (`Error (`T (Printexc.to_string e))) ;; @@ -2125,7 +2059,6 @@ let choose_must list_of_must only = 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 @@ -2135,12 +2068,7 @@ let searchPattern () = 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 uris' = List.map fst (MetadataQuery.hint ~dbd (proof, metano)) in let uri' = user_uri_choice ~title:"Ambiguous input." ~msg: "Many lemmas can be successfully applied. Please, choose one:" @@ -2150,16 +2078,15 @@ let searchPattern () = InvokeTactics'.apply () with e -> - output_html outputhtml + HelmLogger.log (`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 + ~namespaceURI:Misc.helm_ns ~localName:(G.domString "xref") then mmlwidget#set_selection (Some element) @@ -2173,7 +2100,7 @@ let choose_selection mmlwidget (element : Gdome.element option) = | Some p -> aux (new Gdome.element_of_node p) with GdomeInit.DOMCastException _ -> - prerr_endline + debug_print "******* trying to select above the document root ********" in match element with @@ -2334,6 +2261,7 @@ class scratch_window = ~packing:(vbox#pack ~expand:true ~padding:5) () in let sequent_viewer = TermViewer.sequent_viewer + ~mml_of_cic_sequent:ApplyTransformation.mml_of_cic_sequent ~packing:(scrolled_window#add) ~width:400 ~height:280 () in object(self) val mutable term = Cic.Rel 1 (* dummy value *) @@ -2414,8 +2342,9 @@ object(self) 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 + TermViewer.sequent_viewer + ~mml_of_cic_sequent:ApplyTransformation.mml_of_cic_sequent + ~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 @@ -2437,6 +2366,9 @@ object(self) let contradictionb = GButton.button ~label:"Contradiction" ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in + let autob= + GButton.button ~label:"Auto" + ~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 = @@ -2568,6 +2500,7 @@ object(self) ignore(searchpatternb#connect#clicked searchPattern) ; ignore(injectionb#connect#clicked InvokeTactics'.injection) ; ignore(discriminateb#connect#clicked InvokeTactics'.discriminate) ; + ignore(autob#connect#clicked InvokeTactics'.auto) ; (* Zack: spostare in una toolbar ignore(whdb#connect#clicked whd) ; ignore(reduceb#connect#clicked reduce) ; @@ -2590,8 +2523,9 @@ class empty_page = 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 + TermViewer.sequent_viewer + ~mml_of_cic_sequent:ApplyTransformation.mml_of_cic_sequent + ~width:400 ~height:275 ~packing:(scrolled_window1#add) () in object(self) method proofw = (assert false : TermViewer.sequent_viewer) method content = vbox1 @@ -2658,29 +2592,25 @@ 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!")) ; + let oc = open_out (Helm_registry.get "gtoplevel.environment_file") in + HelmLogger.log (`Msg (`T "Dumping environment ...")); + CicEnvironment.dump_to_channel oc; + HelmLogger.log (`Msg (`T "... done!")) ; close_out oc with exc -> - output_html (outputhtml ()) + HelmLogger.log (`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 (`T "Restoring environment ... ")); - CicEnvironment.restore_from_channel - ~callback:(fun uri -> output_html (outputhtml ()) (`Msg (`T uri))) - ic; - output_html (outputhtml ()) (`Msg (`T "... done!")); + let ic = open_in (Helm_registry.get "gtoplevel.environment_file") in + HelmLogger.log (`Msg (`T "Restoring environment ... ")); + CicEnvironment.restore_from_channel ic; + HelmLogger.log (`Msg (`T "... done!")); close_in ic with exc -> - output_html (outputhtml ()) + HelmLogger.log (`Error (`T (Printf.sprintf "Restore failure, uncaught exception:%s" (Printexc.to_string exc)))) ;; @@ -2815,6 +2745,12 @@ class rendering_window output (notebook : notebook) = let _ = factory3#add_item "Edit Aliases..." ~key:GdkKeysyms._A ~callback:edit_aliases in + let _ = + factory3#add_item "Clear Aliases" ~key:GdkKeysyms._K + ~callback:clear_aliases in + let autoitem = + factory3#add_check_item "Auto disambiguation" + ~callback:(fun checked -> auto_disambiguation := checked) in let _ = factory3#add_separator () in let _ = factory3#add_item "MathML Widget Preferences..." ~key:GdkKeysyms._P @@ -2824,20 +2760,19 @@ class rendering_window output (notebook : notebook) = 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 ()) + HelmLogger.log (`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 ()) + HelmLogger.log (`Error (`T ("An error occurred while refreshing the proof: " ^ Printexc.to_string e))) ; output#unload ) in @@ -2860,8 +2795,8 @@ class rendering_window output (notebook : notebook) = GBin.scrolled_window ~border_width:5 ~packing:frame#add () in let inputt = - TexTermEditor'.term_editor - mqi_handle + TermEditor'.term_editor + ~dbd ~width:400 ~height:100 ~packing:scrolled_window1#add () ~isnotempty_callback: (function b -> @@ -2874,18 +2809,17 @@ class rendering_window output (notebook : notebook) = let frame = GBin.frame ~shadow_type:`IN ~packing:(vboxl#pack ~expand:true ~padding:5) () in - let outputhtml = - new Ui_logger.html_logger - ~width:400 ~height: 100 - ~packing:frame#add - ~show:true () in + let _ = + new HelmGtkLogger.html_logger + ~width:400 ~height: 100 ~show:true ~packing:frame#add () + 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 + method set_auto_disambiguation set = autoitem#set_active set initializer notebook#set_empty_page ; (*export_to_postscript_menu_item#misc#set_sensitive false ;*) @@ -2901,29 +2835,33 @@ object 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 )) ; - CicLogger.log_callback := (outputhtml#log_cic_msg ~append_NL:true) + ignore(window#event#connect#delete (fun _ -> GMain.Main.quit () ; true )) end (* MAIN *) let initialize_everything () = - let module U = Unix in - let output = TermViewer.proof_viewer ~width:350 ~height:280 () in + let output = + TermViewer.proof_viewer + ~mml_of_cic_object:ApplyTransformation.mml_of_cic_object + ~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 rendering_window' = new rendering_window output notebook in + rendering_window'#set_auto_disambiguation !auto_disambiguation; + set_rendering_window rendering_window'; + let print_error_as_html prefix msg = + HelmLogger.log (`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 (Helm_registry.get "gtoplevel.environment_file") + then + restore_environment (); + GtkThread.main () ;; let main () = @@ -2934,6 +2872,7 @@ let main () = ;; try +(* CicEnvironment.set_trust (fun _ -> false); *) Sys.catch_break true; main (); with Sys.Break -> () (* exit nicely, invoking at_exit functions *)