From 7fe29ab0adae7bbd2589630b1c5363daf62100c9 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 31 Jan 2003 10:10:21 +0000 Subject: [PATCH] Major module reorganization: - new module TermViewer: holds widgets to render and interact with sequents and proofs at the CIC level - new module ApplyStylesheets: functions to apply stylesheets and map terms and sequents to MathML Presentation - new module InvokeTactics: it is a functor that gives back a module that defines one callback function for every tactic --- helm/gTopLevel/.depend | 33 +- helm/gTopLevel/Makefile | 6 +- helm/gTopLevel/applyStylesheets.ml | 74 ++ helm/gTopLevel/applyStylesheets.mli | 15 + helm/gTopLevel/gTopLevel.ml | 1110 +++++++-------------------- helm/gTopLevel/invokeTactics.ml | 465 +++++++++++ helm/gTopLevel/invokeTactics.mli | 113 +++ helm/gTopLevel/termViewer.ml | 232 ++++++ helm/gTopLevel/termViewer.mli | 100 +++ 9 files changed, 1282 insertions(+), 866 deletions(-) create mode 100644 helm/gTopLevel/invokeTactics.ml create mode 100644 helm/gTopLevel/invokeTactics.mli create mode 100644 helm/gTopLevel/termViewer.ml create mode 100644 helm/gTopLevel/termViewer.mli diff --git a/helm/gTopLevel/.depend b/helm/gTopLevel/.depend index 25b8f4b54..f191fef7c 100644 --- a/helm/gTopLevel/.depend +++ b/helm/gTopLevel/.depend @@ -27,20 +27,23 @@ disambiguate.cmx: mQueryGenerator.cmx misc.cmx disambiguate.cmi termEditor.cmo: disambiguate.cmi termEditor.cmi termEditor.cmx: disambiguate.cmx termEditor.cmi termEditor.cmi: disambiguate.cmi -applyStylesheets.cmo: misc.cmi applyStylesheets.cmi -applyStylesheets.cmx: misc.cmx applyStylesheets.cmi -invokeTactics.cmo: cic2acic.cmi logicalOperations.cmi misc.cmi \ - proofEngine.cmi sequentPp.cmi termEditor.cmi xml2Gdome.cmi \ - invokeTactics.cmi -invokeTactics.cmx: cic2acic.cmx logicalOperations.cmx misc.cmx \ - proofEngine.cmx sequentPp.cmx termEditor.cmx xml2Gdome.cmx \ - invokeTactics.cmi -invokeTactics.cmi: cic2acic.cmi termEditor.cmi +applyStylesheets.cmo: cic2Xml.cmi misc.cmi proofEngine.cmi sequentPp.cmi \ + xml2Gdome.cmi applyStylesheets.cmi +applyStylesheets.cmx: cic2Xml.cmx misc.cmx proofEngine.cmx sequentPp.cmx \ + xml2Gdome.cmx applyStylesheets.cmi +applyStylesheets.cmi: cic2acic.cmi +termViewer.cmo: misc.cmi termViewer.cmi +termViewer.cmx: misc.cmx termViewer.cmi +invokeTactics.cmo: applyStylesheets.cmi logicalOperations.cmi misc.cmi \ + proofEngine.cmi termEditor.cmi termViewer.cmi invokeTactics.cmi +invokeTactics.cmx: applyStylesheets.cmx logicalOperations.cmx misc.cmx \ + proofEngine.cmx termEditor.cmx termViewer.cmx invokeTactics.cmi +invokeTactics.cmi: termEditor.cmi termViewer.cmi gTopLevel.cmo: applyStylesheets.cmi cic2Xml.cmi cic2acic.cmi \ - logicalOperations.cmi mQueryGenerator.cmi mQueryLevels.cmi \ - mQueryLevels2.cmi misc.cmi proofEngine.cmi sequentPp.cmi termEditor.cmi \ - xml2Gdome.cmi + invokeTactics.cmi logicalOperations.cmi mQueryGenerator.cmi \ + mQueryLevels.cmi mQueryLevels2.cmi misc.cmi proofEngine.cmi sequentPp.cmi \ + termEditor.cmi xml2Gdome.cmi gTopLevel.cmx: applyStylesheets.cmx cic2Xml.cmx cic2acic.cmx \ - logicalOperations.cmx mQueryGenerator.cmx mQueryLevels.cmx \ - mQueryLevels2.cmx misc.cmx proofEngine.cmx sequentPp.cmx termEditor.cmx \ - xml2Gdome.cmx + invokeTactics.cmx logicalOperations.cmx mQueryGenerator.cmx \ + mQueryLevels.cmx mQueryLevels2.cmx misc.cmx proofEngine.cmx sequentPp.cmx \ + termEditor.cmx xml2Gdome.cmx diff --git a/helm/gTopLevel/Makefile b/helm/gTopLevel/Makefile index c3626bcd0..34b0aec80 100644 --- a/helm/gTopLevel/Makefile +++ b/helm/gTopLevel/Makefile @@ -22,13 +22,15 @@ DEPOBJS = \ sequentPp.ml sequentPp.mli mQueryGenerator.mli mQueryLevels.ml \ mQueryLevels2.mli mQueryLevels2.ml mQueryGenerator.ml misc.ml misc.mli \ disambiguate.ml disambiguate.mli termEditor.ml termEditor.mli \ - applyStylesheets.ml applyStylesheets.mli gTopLevel.ml + applyStylesheets.ml applyStylesheets.mli termViewer.ml \ + termViewer.mli invokeTactics.ml invokeTactics.mli gTopLevel.ml TOPLEVELOBJS = \ xml2Gdome.cmo proofEngine.cmo doubleTypeInference.cmo cic2acic.cmo \ cic2Xml.cmo logicalOperations.cmo sequentPp.cmo mQueryLevels.cmo \ mQueryLevels2.cmo mQueryGenerator.cmo misc.cmo disambiguate.cmo \ - termEditor.cmo applyStylesheets.cmo gTopLevel.cmo + termEditor.cmo applyStylesheets.cmo termViewer.cmo invokeTactics.cmo \ + gTopLevel.cmo depend: $(OCAMLDEP) $(DEPOBJS) > .depend diff --git a/helm/gTopLevel/applyStylesheets.ml b/helm/gTopLevel/applyStylesheets.ml index 3eed6f493..61adcb42c 100644 --- a/helm/gTopLevel/applyStylesheets.ml +++ b/helm/gTopLevel/applyStylesheets.ml @@ -33,6 +33,8 @@ (* *) (******************************************************************************) +(** stylesheets and parameters list **) + let parseStyle name = let style = Misc.domImpl#createDocumentFromURI @@ -95,6 +97,8 @@ let sequent_args = "CICURI", "'cic:/Coq/Init/Datatypes/bool_ind.con'" ] ;; +(** Stylesheets application **) + let apply_stylesheets input styles args = List.fold_left (fun i style -> Gdome_xslt.applyStylesheet i style args) input styles @@ -107,3 +111,73 @@ let apply_proof_stylesheets proof_doc ~explode_all = let apply_sequent_stylesheets sequent_doc = apply_stylesheets sequent_doc sequent_styles sequent_args ;; + +(** Utility functions to map objects to MathML Presentation **) + +(*CSC: the getter should handle the innertypes, not the FS *) + +let innertypesfile = + try + Sys.getenv "GTOPLEVEL_INNERTYPESFILE" + with + Not_found -> "/public/innertypes" +;; + +let constanttypefile = + try + Sys.getenv "GTOPLEVEL_CONSTANTTYPEFILE" + with + Not_found -> "/public/constanttype" +;; + +let mml_of_cic_term metano term = + let metasenv = + match !ProofEngine.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 + let sequent_gdome,ids_to_terms,ids_to_father_ids,ids_to_hypotheses = + SequentPp.XmlPp.print_sequent metasenv (metano,context,term) + in + let sequent_doc = + Xml2Gdome.document_of_xml Misc.domImpl sequent_gdome + in + let res = apply_sequent_stylesheets sequent_doc in + res, (term,ids_to_terms,ids_to_father_ids,ids_to_hypotheses) +;; + +let + mml_of_cic_object ~explode_all uri annobj ids_to_inner_sorts ids_to_inner_types += +(*CSC: ????????????????? *) + let xml, bodyxml = + Cic2Xml.print_object uri ~ids_to_inner_sorts ~ask_dtd_to_the_getter:true + annobj + in + let xmlinnertypes = + Cic2Xml.print_inner_types uri ~ids_to_inner_sorts ~ids_to_inner_types + ~ask_dtd_to_the_getter:true + in + let input = + match bodyxml with + None -> Xml2Gdome.document_of_xml Misc.domImpl xml + | Some bodyxml' -> + Xml.pp xml (Some constanttypefile) ; + Xml2Gdome.document_of_xml Misc.domImpl bodyxml' + in +(*CSC: We save the innertypes to disk so that we can retrieve them in the *) +(*CSC: stylesheet. This DOES NOT work when UWOBO and/or the getter are not *) +(*CSC: local. *) + Xml.pp xmlinnertypes (Some innertypesfile) ; + let output = apply_proof_stylesheets input ~explode_all in + output +;; diff --git a/helm/gTopLevel/applyStylesheets.mli b/helm/gTopLevel/applyStylesheets.mli index e42944b86..ff76c45d5 100644 --- a/helm/gTopLevel/applyStylesheets.mli +++ b/helm/gTopLevel/applyStylesheets.mli @@ -33,6 +33,21 @@ (* *) (******************************************************************************) +(* Not exported: val apply_proof_stylesheets : Gdome.document -> explode_all:bool -> Gdome.document +*) val apply_sequent_stylesheets : Gdome.document -> Gdome.document + +val mml_of_cic_term : + int -> Cic.term -> + Gdome.document * + (Cic.term * (Cic.id, Cic.term) Hashtbl.t * + (Cic.id, Cic.id option) Hashtbl.t * (string, Cic.hypothesis) Hashtbl.t) + +val mml_of_cic_object : + explode_all:bool -> + UriManager.uri -> + Cic.annobj -> + (string, string) Hashtbl.t -> + (string, Cic2acic.anntypes) Hashtbl.t -> Gdome.document diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml index 4bef88816..5b0f3d6e7 100644 --- a/helm/gTopLevel/gTopLevel.ml +++ b/helm/gTopLevel/gTopLevel.ml @@ -62,22 +62,6 @@ let prooffiletype = Not_found -> "/public/currentprooftype" ;; -(*CSC: the getter should handle the innertypes, not the FS *) - -let innertypesfile = - try - Sys.getenv "GTOPLEVEL_INNERTYPESFILE" - with - Not_found -> "/public/innertypes" -;; - -let constanttypefile = - try - Sys.getenv "GTOPLEVEL_CONSTANTTYPEFILE" - with - Not_found -> "/public/constanttype" -;; - let postgresqlconnectionstring = try Sys.getenv "POSTGRESQL_CONNECTION_STRING" @@ -89,12 +73,9 @@ let postgresqlconnectionstring = let htmlheader_and_content = ref htmlheader;; -let current_cic_infos = ref None;; -let current_goal_infos = ref None;; -let current_scratch_infos = ref None;; +let current_scratch_infos = ref None let check_term = ref (fun _ _ _ -> assert false);; -let mml_of_cic_term_ref = ref (fun _ _ -> assert false);; exception RenderingWindowsNotInitialized;; @@ -220,7 +201,10 @@ let check_window outputhtml uris = (Cic.Cast (term, CicTypeChecker.type_of_aux' [] [] term)) in try - let mml = !mml_of_cic_term_ref 111 expr in + let mml,scratch_infos = + ApplyStylesheets.mml_of_cic_term 111 expr + in + current_scratch_infos := Some scratch_infos ; mmlwidget#load_doc ~dom:mml with e -> @@ -412,33 +396,6 @@ let get_last_query = function result -> !query ^ "

Result:

" ^ MQueryUtil.text_of_result result "
" ;; -let - mml_of_cic_object ~explode_all uri annobj ids_to_inner_sorts ids_to_inner_types -= -(*CSC: ????????????????? *) - let xml, bodyxml = - Cic2Xml.print_object uri ~ids_to_inner_sorts ~ask_dtd_to_the_getter:true - annobj - in - let xmlinnertypes = - Cic2Xml.print_inner_types uri ~ids_to_inner_sorts ~ids_to_inner_types - ~ask_dtd_to_the_getter:true - in - let input = - match bodyxml with - None -> Xml2Gdome.document_of_xml Misc.domImpl xml - | Some bodyxml' -> - Xml.pp xml (Some constanttypefile) ; - Xml2Gdome.document_of_xml Misc.domImpl bodyxml' - in -(*CSC: We save the innertypes to disk so that we can retrieve them in the *) -(*CSC: stylesheet. This DOES NOT work when UWOBO and/or the getter are not *) -(*CSC: local. *) - Xml.pp xmlinnertypes (Some innertypesfile) ; - let output = ApplyStylesheets.apply_proof_stylesheets input ~explode_all in - output -;; - let save_object_to_disk uri annobj ids_to_inner_sorts ids_to_inner_types pathname = @@ -491,139 +448,11 @@ let (* CALLBACKS *) -exception RefreshSequentException of exn;; -exception RefreshProofException of exn;; - -let refresh_proof (output : GMathViewAux.single_selection_math_view) = - try - let uri,currentproof = - match !ProofEngine.proof with - None -> assert false - | Some (uri,metasenv,bo,ty) -> - !qed_set_sensitive (List.length metasenv = 0) ; - (*CSC: Wrong: [] is just plainly wrong *) - uri,(Cic.CurrentProof (UriManager.name_of_uri uri, metasenv, bo, ty, [])) - in - 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 currentproof - in - let mml = - mml_of_cic_object ~explode_all:true uri acic ids_to_inner_sorts - ids_to_inner_types - in - output#load_doc ~dom:mml ; - current_cic_infos := - Some (ids_to_terms,ids_to_father_ids,ids_to_conjectures,ids_to_hypotheses) - with - e -> - match !ProofEngine.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 (RefreshProofException e) -;; - -let refresh_sequent ?(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.proof with - None -> assert false - | Some (_,metasenv,_,_) -> metasenv - in - let currentsequent = List.find (function (m,_,_) -> m=metano) metasenv in - let sequent_gdome,ids_to_terms,ids_to_father_ids,ids_to_hypotheses = - SequentPp.XmlPp.print_sequent metasenv currentsequent - 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 - let sequent_doc = - Xml2Gdome.document_of_xml Misc.domImpl sequent_gdome in - let sequent_mml = - ApplyStylesheets.apply_sequent_stylesheets sequent_doc - in - notebook#set_current_page ~may_skip_switch_page_event:true metano; - notebook#proofw#load_doc ~dom:sequent_mml - end ; - current_goal_infos := - Some (ids_to_terms,ids_to_father_ids,ids_to_hypotheses) - with - e -> -let metano = - match !ProofEngine.goal with - None -> assert false - | Some m -> m -in -let metasenv = - match !ProofEngine.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 (RefreshSequentException e) -with Not_found -> prerr_endline ("Offending sequent " ^ string_of_int metano ^ " unkown."); raise (RefreshSequentException e) -;; - (* ignore(domImpl#saveDocumentToFile ~doc:sequent_doc ~name:"/home/galata/miohelm/guruguru1" ~indent:true ()) ; *) -let mml_of_cic_term metano term = - let metasenv = - match !ProofEngine.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 - let sequent_gdome,ids_to_terms,ids_to_father_ids,ids_to_hypotheses = - SequentPp.XmlPp.print_sequent metasenv (metano,context,term) - in - let sequent_doc = - Xml2Gdome.document_of_xml Misc.domImpl sequent_gdome - in - let res = ApplyStylesheets.apply_sequent_stylesheets sequent_doc in - current_scratch_infos := - Some (term,ids_to_terms,ids_to_father_ids,ids_to_hypotheses) ; - res -;; - exception OpenConjecturesStillThere;; exception WrongProof;; @@ -661,27 +490,15 @@ let qed () = begin (*CSC: Wrong: [] is just plainly wrong *) let proof = Cic.Constant (UriManager.name_of_uri uri,Some bo,ty,[]) in - 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 proof - in - let mml = - mml_of_cic_object ~explode_all:false uri acic ids_to_inner_sorts - ids_to_inner_types - in - ((rendering_window ())#output : GMathViewAux.single_selection_math_view)#load_doc mml ; - !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 ; - current_cic_infos := - Some - (ids_to_terms,ids_to_father_ids,ids_to_conjectures, - ids_to_hypotheses) + 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 @@ -731,9 +548,148 @@ let typecheck_loaded_proof metasenv bo 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 Misc.cic_textual_parser_uri_of_string uri with + CicTextualParser0.IndTyUri (uri,typeno) -> (uri,typeno,[]) + | _ -> assert false) + (interactive_user_uri_choice + ~selection_mode:`EXTENDED ~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.proof with + None -> assert false + | Some (uri,metasenv,bo,ty) -> + !qed_set_sensitive (List.length metasenv = 0) ; + (*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.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 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.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.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 : TermEditor.term_editor) + let get_current_scratch_infos () = !current_scratch_infos + let set_current_scratch_infos scratch_infos = + current_scratch_infos := scratch_infos + + 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 + end +;; + +module InvokeTactics' = InvokeTactics.Make(InvokeTacticsCallbacks);; + + let load () = let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in - let output = ((rendering_window ())#output : GMathViewAux.single_selection_math_view) in + let output = ((rendering_window ())#output : TermViewer.proof_viewer) in let notebook = (rendering_window ())#notebook in try match @@ -754,7 +710,7 @@ let load () = | (metano,_,_)::_ -> Some metano ) ; refresh_proof output ; - refresh_sequent notebook ; + refresh_goals notebook ; output_html outputhtml ("

Current proof type loaded from " ^ prooffiletype ^ "

") ; @@ -764,11 +720,11 @@ let load () = !save_set_sensitive true | _ -> assert false with - RefreshSequentException e -> + InvokeTactics.RefreshSequentException e -> output_html outputhtml ("

Exception raised during the refresh of the " ^ "sequent: " ^ Printexc.to_string e ^ "

") - | RefreshProofException e -> + | InvokeTactics.RefreshProofException e -> output_html outputhtml ("

Exception raised during the refresh of the " ^ "proof: " ^ Printexc.to_string e ^ "

") @@ -861,41 +817,22 @@ let proveit () = let notebook = (rendering_window ())#notebook in let output = (rendering_window ())#output in let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in - match (rendering_window ())#output#get_selection with - Some node -> - let xpath = - ((node : Gdome.element)#getAttributeNS - (*CSC: OCAML DIVERGE - ((element : G.element)#getAttributeNS - *) - ~namespaceURI:Misc.helmns - ~localName:(G.domString "xref"))#to_string - in - if xpath = "" then assert false (* "ERROR: No xref found!!!" *) - else - begin - try - match !current_cic_infos with - Some (ids_to_terms, ids_to_father_ids, _, _) -> - let id = xpath in - L.to_sequent id ids_to_terms ids_to_father_ids ; - refresh_proof output ; - refresh_sequent notebook - | None -> assert false (* "ERROR: No current term!!!" *) - with - RefreshSequentException e -> - output_html outputhtml - ("

Exception raised during the refresh of the " ^ - "sequent: " ^ Printexc.to_string e ^ "

") - | RefreshProofException e -> - output_html outputhtml - ("

Exception raised during the refresh of the " ^ - "proof: " ^ Printexc.to_string e ^ "

") - | e -> - output_html outputhtml - ("

" ^ Printexc.to_string e ^ "

") - end - | None -> assert false (* "ERROR: No selection!!!" *) + try + output#make_sequent_of_selected_term ; + refresh_proof output ; + refresh_goals notebook + with + InvokeTactics.RefreshSequentException e -> + output_html outputhtml + ("

Exception raised during the refresh of the " ^ + "sequent: " ^ Printexc.to_string e ^ "

") + | InvokeTactics.RefreshProofException e -> + output_html outputhtml + ("

Exception raised during the refresh of the " ^ + "proof: " ^ Printexc.to_string e ^ "

") + | e -> + output_html outputhtml + ("

" ^ Printexc.to_string e ^ "

") ;; let focus () = @@ -903,40 +840,22 @@ let focus () = let module G = Gdome in let notebook = (rendering_window ())#notebook in let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in - match (rendering_window ())#output#get_selection with - Some node -> - let xpath = - ((node : Gdome.element)#getAttributeNS - (*CSC: OCAML DIVERGE - ((element : G.element)#getAttributeNS - *) - ~namespaceURI:Misc.helmns - ~localName:(G.domString "xref"))#to_string - in - if xpath = "" then assert false (* "ERROR: No xref found!!!" *) - else - begin - try - match !current_cic_infos with - Some (ids_to_terms, ids_to_father_ids, _, _) -> - let id = xpath in - L.focus id ids_to_terms ids_to_father_ids ; - refresh_sequent notebook - | None -> assert false (* "ERROR: No current term!!!" *) - with - RefreshSequentException e -> - output_html outputhtml - ("

Exception raised during the refresh of the " ^ - "sequent: " ^ Printexc.to_string e ^ "

") - | RefreshProofException e -> - output_html outputhtml - ("

Exception raised during the refresh of the " ^ - "proof: " ^ Printexc.to_string e ^ "

") - | e -> - output_html outputhtml - ("

" ^ Printexc.to_string e ^ "

") - end - | None -> assert false (* "ERROR: No selection!!!" *) + let output = (rendering_window ())#output in + try + output#focus_sequent_of_selected_term ; + refresh_goals notebook + with + InvokeTactics.RefreshSequentException e -> + output_html outputhtml + ("

Exception raised during the refresh of the " ^ + "sequent: " ^ Printexc.to_string e ^ "

") + | InvokeTactics.RefreshProofException e -> + output_html outputhtml + ("

Exception raised during the refresh of the " ^ + "proof: " ^ Printexc.to_string e ^ "

") + | e -> + output_html outputhtml + ("

" ^ Printexc.to_string e ^ "

") ;; exception NoPrevGoal;; @@ -953,9 +872,9 @@ let setgoal metano = | Some (_,metasenv,_,_) -> metasenv in try - refresh_sequent ~empty_notebook:false notebook + refresh_goals ~empty_notebook:false notebook with - RefreshSequentException e -> + InvokeTactics.RefreshSequentException e -> output_html outputhtml ("

Exception raised during the refresh of the " ^ "sequent: " ^ Printexc.to_string e ^ "

") @@ -985,8 +904,8 @@ let Cic2acic.acic_object_of_cic_object obj in let mml = - mml_of_cic_object ~explode_all:false uri acic ids_to_inner_sorts - ids_to_inner_types + 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 () ; @@ -1201,7 +1120,7 @@ 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 : GMathViewAux.single_selection_math_view) in + let output = ((rendering_window ())#output : TermViewer.proof_viewer) in let notebook = (rendering_window ())#notebook in let chosen = ref false in @@ -1528,26 +1447,10 @@ let new_inductive () = ("

" ^ Printexc.to_string e ^ "

") ; ;; -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 new_proof () = let inputt = ((rendering_window ())#inputt : TermEditor.term_editor) in let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in - let output = ((rendering_window ())#output : GMathViewAux.single_selection_math_view) in + let output = ((rendering_window ())#output : TermViewer.proof_viewer) in let notebook = (rendering_window ())#notebook in let chosen = ref false in @@ -1642,19 +1545,19 @@ let new_proof () = ProofEngine.proof := Some (!get_uri (), (1,[],expr)::metasenv, Cic.Meta (1,[]), expr) ; ProofEngine.goal := Some 1 ; - refresh_sequent notebook ; + refresh_goals notebook ; refresh_proof output ; !save_set_sensitive true ; inputt#reset ; ProofEngine.intros ~mk_fresh_name_callback () ; - refresh_sequent notebook ; + refresh_goals notebook ; refresh_proof output with - RefreshSequentException e -> + InvokeTactics.RefreshSequentException e -> output_html outputhtml ("

Exception raised during the refresh of the " ^ "sequent: " ^ Printexc.to_string e ^ "

") - | RefreshProofException e -> + | InvokeTactics.RefreshProofException e -> output_html outputhtml ("

Exception raised during the refresh of the " ^ "proof: " ^ Printexc.to_string e ^ "

") @@ -1666,7 +1569,10 @@ let new_proof () = let check_term_in_scratch scratch_window metasenv context expr = try let ty = CicTypeChecker.type_of_aux' metasenv context expr in - let mml = mml_of_cic_term 111 (Cic.Cast (expr,ty)) in + let mml,scratch_infos = + ApplyStylesheets.mml_of_cic_term 111 (Cic.Cast (expr,ty)) + in + current_scratch_infos := Some scratch_infos ; scratch_window#show () ; scratch_window#mmlwidget#load_doc ~dom:mml with @@ -1701,502 +1607,6 @@ let check scratch_window () = ("

" ^ Printexc.to_string e ^ "

") ; ;; -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 Misc.cic_textual_parser_uri_of_string uri with - CicTextualParser0.IndTyUri (uri,typeno) -> (uri,typeno,[]) - | _ -> assert false) - (interactive_user_uri_choice - ~selection_mode:`EXTENDED ~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) - ) -;; - -(***********************) -(* TACTICS *) -(***********************) - -let call_tactic tactic () = - let notebook = (rendering_window ())#notebook in - let output = ((rendering_window ())#output : GMathViewAux.single_selection_math_view) in - let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in - let savedproof = !ProofEngine.proof in - let savedgoal = !ProofEngine.goal in - begin - try - tactic () ; - refresh_sequent notebook ; - refresh_proof output - with - RefreshSequentException e -> - output_html outputhtml - ("

Exception raised during the refresh of the " ^ - "sequent: " ^ Printexc.to_string e ^ "

") ; - ProofEngine.proof := savedproof ; - ProofEngine.goal := savedgoal ; - refresh_sequent notebook - | RefreshProofException e -> - output_html outputhtml - ("

Exception raised during the refresh of the " ^ - "proof: " ^ Printexc.to_string e ^ "

") ; - ProofEngine.proof := savedproof ; - ProofEngine.goal := savedgoal ; - refresh_sequent notebook ; - refresh_proof output - | e -> - output_html outputhtml - ("

" ^ Printexc.to_string e ^ "

") ; - ProofEngine.proof := savedproof ; - ProofEngine.goal := savedgoal ; - end -;; - -let call_tactic_with_input tactic () = - let notebook = (rendering_window ())#notebook in - let output = ((rendering_window ())#output : GMathViewAux.single_selection_math_view) in - let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in - let inputt = ((rendering_window ())#inputt : TermEditor.term_editor) in - let savedproof = !ProofEngine.proof in - let savedgoal = !ProofEngine.goal in - let uri,metasenv,bo,ty = - match !ProofEngine.proof with - None -> assert false - | Some (uri,metasenv,bo,ty) -> uri,metasenv,bo,ty - in - let canonical_context = - match !ProofEngine.goal with - None -> assert false - | 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 canonical_context metasenv - in - ProofEngine.proof := Some (uri,metasenv',bo,ty) ; - tactic expr ; - refresh_sequent notebook ; - refresh_proof output ; - inputt#reset - with - RefreshSequentException e -> - output_html outputhtml - ("

Exception raised during the refresh of the " ^ - "sequent: " ^ Printexc.to_string e ^ "

") ; - ProofEngine.proof := savedproof ; - ProofEngine.goal := savedgoal ; - refresh_sequent notebook - | RefreshProofException e -> - output_html outputhtml - ("

Exception raised during the refresh of the " ^ - "proof: " ^ Printexc.to_string e ^ "

") ; - ProofEngine.proof := savedproof ; - ProofEngine.goal := savedgoal ; - refresh_sequent notebook ; - refresh_proof output - | e -> - output_html outputhtml - ("

" ^ Printexc.to_string e ^ "

") ; - ProofEngine.proof := savedproof ; - ProofEngine.goal := savedgoal ; -;; - -let call_tactic_with_goal_input tactic () = - let module L = LogicalOperations in - let module G = Gdome in - let notebook = (rendering_window ())#notebook in - let output = ((rendering_window ())#output : GMathViewAux.single_selection_math_view) in - let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in - let savedproof = !ProofEngine.proof in - let savedgoal = !ProofEngine.goal in - match notebook#proofw#get_selections with - [node] -> - let xpath = - ((node : Gdome.element)#getAttributeNS - ~namespaceURI:Misc.helmns - ~localName:(G.domString "xref"))#to_string - in - if xpath = "" then assert false (* "ERROR: No xref found!!!" *) - else - begin - try - match !current_goal_infos with - Some (ids_to_terms, ids_to_father_ids,_) -> - let id = xpath in - tactic (Hashtbl.find ids_to_terms id) ; - refresh_sequent notebook ; - refresh_proof output - | None -> assert false (* "ERROR: No current term!!!" *) - with - RefreshSequentException e -> - output_html outputhtml - ("

Exception raised during the refresh of the " ^ - "sequent: " ^ Printexc.to_string e ^ "

") ; - ProofEngine.proof := savedproof ; - ProofEngine.goal := savedgoal ; - refresh_sequent notebook - | RefreshProofException e -> - output_html outputhtml - ("

Exception raised during the refresh of the " ^ - "proof: " ^ Printexc.to_string e ^ "

") ; - ProofEngine.proof := savedproof ; - ProofEngine.goal := savedgoal ; - refresh_sequent notebook ; - refresh_proof output - | e -> - output_html outputhtml - ("

" ^ Printexc.to_string e ^ "

") ; - ProofEngine.proof := savedproof ; - ProofEngine.goal := savedgoal ; - end - | [] -> - output_html outputhtml - ("

No term selected

") - | _ -> - output_html outputhtml - ("

Many terms selected

") -;; - -let call_tactic_with_goal_inputs tactic () = - let module L = LogicalOperations in - let module G = Gdome in - let notebook = (rendering_window ())#notebook in - let output = - ((rendering_window ())#output : GMathViewAux.single_selection_math_view) in - let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in - let savedproof = !ProofEngine.proof in - let savedgoal = !ProofEngine.goal in - try - let term_of_node node = - let xpath = - ((node : Gdome.element)#getAttributeNS - ~namespaceURI:Misc.helmns - ~localName:(G.domString "xref"))#to_string - in - if xpath = "" then assert false (* "ERROR: No xref found!!!" *) - else - match !current_goal_infos with - Some (ids_to_terms, ids_to_father_ids,_) -> - let id = xpath in - (Hashtbl.find ids_to_terms id) - | None -> assert false (* "ERROR: No current term!!!" *) - in - match notebook#proofw#get_selections with - [] -> - output_html outputhtml - ("

No term selected

") - | l -> - let terms = List.map term_of_node l in - match !current_goal_infos with - Some (ids_to_terms, ids_to_father_ids,_) -> - tactic terms ; - refresh_sequent notebook ; - refresh_proof output - | None -> assert false (* "ERROR: No current term!!!" *) - with - RefreshSequentException e -> - output_html outputhtml - ("

Exception raised during the refresh of the " ^ - "sequent: " ^ Printexc.to_string e ^ "

") ; - ProofEngine.proof := savedproof ; - ProofEngine.goal := savedgoal ; - refresh_sequent notebook - | RefreshProofException e -> - output_html outputhtml - ("

Exception raised during the refresh of the " ^ - "proof: " ^ Printexc.to_string e ^ "

") ; - ProofEngine.proof := savedproof ; - ProofEngine.goal := savedgoal ; - refresh_sequent notebook ; - refresh_proof output - | e -> - output_html outputhtml - ("

" ^ Printexc.to_string e ^ "

") ; - ProofEngine.proof := savedproof ; - ProofEngine.goal := savedgoal -;; - -let call_tactic_with_input_and_goal_input tactic () = - let module L = LogicalOperations in - let module G = Gdome in - let notebook = (rendering_window ())#notebook in - let output = ((rendering_window ())#output : GMathViewAux.single_selection_math_view) in - let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in - let inputt = ((rendering_window ())#inputt : TermEditor.term_editor) in - let savedproof = !ProofEngine.proof in - let savedgoal = !ProofEngine.goal in - match notebook#proofw#get_selections with - [node] -> - let xpath = - ((node : Gdome.element)#getAttributeNS - ~namespaceURI:Misc.helmns - ~localName:(G.domString "xref"))#to_string - in - if xpath = "" then assert false (* "ERROR: No xref found!!!" *) - else - begin - try - match !current_goal_infos with - Some (ids_to_terms, ids_to_father_ids,_) -> - let id = xpath in - let uri,metasenv,bo,ty = - match !ProofEngine.proof with - None -> assert false - | Some (uri,metasenv,bo,ty) -> uri,metasenv,bo,ty - in - let canonical_context = - match !ProofEngine.goal with - None -> assert false - | Some metano -> - let (_,canonical_context,_) = - List.find (function (m,_,_) -> m=metano) metasenv - in - canonical_context in - let (metasenv',expr) = - inputt#get_metasenv_and_term canonical_context metasenv - in - ProofEngine.proof := Some (uri,metasenv',bo,ty) ; - tactic ~goal_input:(Hashtbl.find ids_to_terms id) - ~input:expr ; - refresh_sequent notebook ; - refresh_proof output ; - inputt#reset - | None -> assert false (* "ERROR: No current term!!!" *) - with - RefreshSequentException e -> - output_html outputhtml - ("

Exception raised during the refresh of the " ^ - "sequent: " ^ Printexc.to_string e ^ "

") ; - ProofEngine.proof := savedproof ; - ProofEngine.goal := savedgoal ; - refresh_sequent notebook - | RefreshProofException e -> - output_html outputhtml - ("

Exception raised during the refresh of the " ^ - "proof: " ^ Printexc.to_string e ^ "

") ; - ProofEngine.proof := savedproof ; - ProofEngine.goal := savedgoal ; - refresh_sequent notebook ; - refresh_proof output - | e -> - output_html outputhtml - ("

" ^ Printexc.to_string e ^ "

") ; - ProofEngine.proof := savedproof ; - ProofEngine.goal := savedgoal ; - end - | [] -> - output_html outputhtml - ("

No term selected

") - | _ -> - output_html outputhtml - ("

Many terms selected

") -;; - -let call_tactic_with_goal_input_in_scratch tactic scratch_window () = - let module L = LogicalOperations in - let module G = Gdome in - let mmlwidget = - (scratch_window#mmlwidget : GMathViewAux.multi_selection_math_view) in - let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in - let savedproof = !ProofEngine.proof in - let savedgoal = !ProofEngine.goal in - match mmlwidget#get_selections with - [node] -> - let xpath = - ((node : Gdome.element)#getAttributeNS - ~namespaceURI:Misc.helmns - ~localName:(G.domString "xref"))#to_string - in - if xpath = "" then assert false (* "ERROR: No xref found!!!" *) - else - begin - try - match !current_scratch_infos with - (* term is the whole goal in the scratch_area *) - Some (term,ids_to_terms, ids_to_father_ids,_) -> - let id = xpath in - let expr = tactic term (Hashtbl.find ids_to_terms id) in - let mml = mml_of_cic_term 111 expr in - scratch_window#show () ; - scratch_window#mmlwidget#load_doc ~dom:mml - | None -> assert false (* "ERROR: No current term!!!" *) - with - e -> - output_html outputhtml - ("

" ^ Printexc.to_string e ^ "

") - end - | [] -> - output_html outputhtml - ("

No term selected

") - | _ -> - output_html outputhtml - ("

Many terms selected

") -;; - -let call_tactic_with_goal_inputs_in_scratch tactic scratch_window () = - let module L = LogicalOperations in - let module G = Gdome in - let mmlwidget = - (scratch_window#mmlwidget : GMathViewAux.multi_selection_math_view) in - let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in - let savedproof = !ProofEngine.proof in - let savedgoal = !ProofEngine.goal in - match mmlwidget#get_selections with - [] -> - output_html outputhtml - ("

No term selected

") - | l -> - try - match !current_scratch_infos with - (* term is the whole goal in the scratch_area *) - Some (term,ids_to_terms, ids_to_father_ids,_) -> - let term_of_node node = - let xpath = - ((node : Gdome.element)#getAttributeNS - ~namespaceURI:Misc.helmns - ~localName:(G.domString "xref"))#to_string - in - if xpath = "" then assert false (* "ERROR: No xref found!!!" *) - else - let id = xpath in - Hashtbl.find ids_to_terms id - in - let terms = List.map term_of_node l in - let expr = tactic terms term in - let mml = mml_of_cic_term 111 expr in - scratch_window#show () ; - scratch_window#mmlwidget#load_doc ~dom:mml - | None -> assert false (* "ERROR: No current term!!!" *) - with - e -> - output_html outputhtml - ("

" ^ Printexc.to_string e ^ "

") -;; - -let call_tactic_with_hypothesis_input tactic () = - let module L = LogicalOperations in - let module G = Gdome in - let notebook = (rendering_window ())#notebook in - let output = ((rendering_window ())#output : GMathViewAux.single_selection_math_view) in - let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in - let savedproof = !ProofEngine.proof in - let savedgoal = !ProofEngine.goal in - match notebook#proofw#get_selections with - [node] -> - let xpath = - ((node : Gdome.element)#getAttributeNS - ~namespaceURI:Misc.helmns - ~localName:(G.domString "xref"))#to_string - in - if xpath = "" then assert false (* "ERROR: No xref found!!!" *) - else - begin - try - match !current_goal_infos with - Some (_,_,ids_to_hypotheses) -> - let id = xpath in - tactic (Hashtbl.find ids_to_hypotheses id) ; - refresh_sequent notebook ; - refresh_proof output - | None -> assert false (* "ERROR: No current term!!!" *) - with - RefreshSequentException e -> - output_html outputhtml - ("

Exception raised during the refresh of the " ^ - "sequent: " ^ Printexc.to_string e ^ "

") ; - ProofEngine.proof := savedproof ; - ProofEngine.goal := savedgoal ; - refresh_sequent notebook - | RefreshProofException e -> - output_html outputhtml - ("

Exception raised during the refresh of the " ^ - "proof: " ^ Printexc.to_string e ^ "

") ; - ProofEngine.proof := savedproof ; - ProofEngine.goal := savedgoal ; - refresh_sequent notebook ; - refresh_proof output - | e -> - output_html outputhtml - ("

" ^ Printexc.to_string e ^ "

") ; - ProofEngine.proof := savedproof ; - ProofEngine.goal := savedgoal ; - end - | [] -> - output_html outputhtml - ("

No term selected

") - | _ -> - output_html outputhtml - ("

Many terms selected

") -;; - - -let intros = call_tactic (ProofEngine.intros ~mk_fresh_name_callback);; -let exact = call_tactic_with_input ProofEngine.exact;; -let apply = call_tactic_with_input ProofEngine.apply;; -let elimintrossimpl = call_tactic_with_input ProofEngine.elim_intros_simpl;; -let elimtype = call_tactic_with_input ProofEngine.elim_type;; -let whd = call_tactic_with_goal_inputs ProofEngine.whd;; -let reduce = call_tactic_with_goal_inputs ProofEngine.reduce;; -let simpl = call_tactic_with_goal_inputs ProofEngine.simpl;; -let fold_whd = call_tactic_with_input ProofEngine.fold_whd;; -let fold_reduce = call_tactic_with_input ProofEngine.fold_reduce;; -let fold_simpl = call_tactic_with_input ProofEngine.fold_simpl;; -let cut = call_tactic_with_input (ProofEngine.cut ~mk_fresh_name_callback);; -let change = call_tactic_with_input_and_goal_input ProofEngine.change;; -let letin = call_tactic_with_input (ProofEngine.letin ~mk_fresh_name_callback);; -let ring = call_tactic ProofEngine.ring;; -let clearbody = call_tactic_with_hypothesis_input ProofEngine.clearbody;; -let clear = call_tactic_with_hypothesis_input ProofEngine.clear;; -let fourier = call_tactic ProofEngine.fourier;; -let rewritesimpl = call_tactic_with_input ProofEngine.rewrite_simpl;; -let rewritebacksimpl = call_tactic_with_input ProofEngine.rewrite_back_simpl;; -let replace = call_tactic_with_input_and_goal_input ProofEngine.replace;; -let reflexivity = call_tactic ProofEngine.reflexivity;; -let symmetry = call_tactic ProofEngine.symmetry;; -let transitivity = call_tactic_with_input ProofEngine.transitivity;; -let exists = call_tactic ProofEngine.exists;; -let split = call_tactic ProofEngine.split;; -let left = call_tactic ProofEngine.left;; -let right = call_tactic ProofEngine.right;; -let assumption = call_tactic ProofEngine.assumption;; -let generalize = - call_tactic_with_goal_inputs (ProofEngine.generalize ~mk_fresh_name_callback);; -let absurd = call_tactic_with_input ProofEngine.absurd;; -let contradiction = call_tactic ProofEngine.contradiction;; -let decompose = - call_tactic_with_input - (ProofEngine.decompose ~uris_choice_callback:decompose_uris_choice_callback);; - -let whd_in_scratch scratch_window = - call_tactic_with_goal_inputs_in_scratch ProofEngine.whd_in_scratch - scratch_window -;; -let reduce_in_scratch scratch_window = - call_tactic_with_goal_inputs_in_scratch ProofEngine.reduce_in_scratch - scratch_window -;; -let simpl_in_scratch scratch_window = - call_tactic_with_goal_inputs_in_scratch ProofEngine.simpl_in_scratch - scratch_window -;; - - - -(**********************) -(* END OF TACTICS *) -(**********************) - - let show () = let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in try @@ -2211,7 +1621,7 @@ exception NotADefinition;; let open_ () = let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in - let output = ((rendering_window ())#output : GMathViewAux.single_selection_math_view) 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 @@ -2227,14 +1637,14 @@ let open_ () = ProofEngine.proof := Some (uri, metasenv, bo, ty) ; ProofEngine.goal := None ; - refresh_sequent notebook ; + refresh_goals notebook ; refresh_proof output with - RefreshSequentException e -> + InvokeTactics.RefreshSequentException e -> output_html outputhtml ("

Exception raised during the refresh of the " ^ "sequent: " ^ Printexc.to_string e ^ "

") - | RefreshProofException e -> + | InvokeTactics.RefreshProofException e -> output_html outputhtml ("

Exception raised during the refresh of the " ^ "proof: " ^ Printexc.to_string e ^ "

") @@ -2779,7 +2189,7 @@ let searchPattern () = uris' in inputt#set_term uri' ; - apply () + InvokeTactics'.apply () with e -> output_html outputhtml @@ -2816,7 +2226,7 @@ let choose_selection mmlwidget (element : Gdome.element option) = (* Stuff for the widget settings *) -let export_to_postscript (output : GMathViewAux.single_selection_math_view) = +let export_to_postscript output = let lastdir = ref (Unix.getcwd ()) in function () -> match @@ -2825,16 +2235,17 @@ let export_to_postscript (output : GMathViewAux.single_selection_math_view) = with None -> () | Some filename -> - output#export_to_postscript ~filename:filename (); + (output :> GMathView.math_view)#export_to_postscript + ~filename:filename (); ;; -let activate_t1 (output : GMathViewAux.single_selection_math_view) button_set_anti_aliasing +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 - (if is_set then `font_manager_t1 else `font_manager_gtk) ; + ~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 ; @@ -2865,7 +2276,7 @@ let set_log_verbosity output log_verbosity_spinb () = output#set_log_verbosity log_verbosity_spinb#value_as_int ;; -class settings_window (output : GMathViewAux.single_selection_math_view) sw +class settings_window output sw export_to_postscript_menu_item selection_changed_callback = let settings_window = GWindow.window ~title:"GtkMathView settings" () in @@ -2960,9 +2371,9 @@ object(self) initializer ignore(mmlwidget#connect#selection_changed (choose_selection mmlwidget)) ; ignore(window#event#connect#delete (fun _ -> window#misc#hide () ; true )) ; - ignore(whdb#connect#clicked (whd_in_scratch self)) ; - ignore(reduceb#connect#clicked (reduce_in_scratch self)) ; - ignore(simplb#connect#clicked (simpl_in_scratch self)) + ignore(whdb#connect#clicked (InvokeTactics'.whd_in_scratch self)) ; + ignore(reduceb#connect#clicked (InvokeTactics'.reduce_in_scratch self)) ; + ignore(simplb#connect#clicked (InvokeTactics'.simpl_in_scratch self)) end;; let open_contextual_menu_for_selected_terms mmlwidget infos = @@ -2974,19 +2385,21 @@ let open_contextual_menu_for_selected_terms mmlwidget infos = let menu = GMenu.menu () in let f = new GMenu.factory menu in let whd_menu_item = - f#add_item "Whd" ~key:GdkKeysyms._W ~callback:whd in + f#add_item "Whd" ~key:GdkKeysyms._W ~callback:InvokeTactics'.whd in let reduce_menu_item = - f#add_item "Reduce" ~key:GdkKeysyms._R ~callback:reduce in + f#add_item "Reduce" ~key:GdkKeysyms._R ~callback:InvokeTactics'.reduce in let simpl_menu_item = - f#add_item "Simpl" ~key:GdkKeysyms._S ~callback:simpl in + 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:generalize in + 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:clear in + f#add_item "Clear" ~key:GdkKeysyms._C ~callback:InvokeTactics'.clear in let clearbody_menu_item = - f#add_item "ClearBody" ~key:GdkKeysyms._B ~callback:clearbody + 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 ; @@ -3021,7 +2434,7 @@ object(self) GBin.scrolled_window ~border_width:10 ~packing:(vbox1#pack ~expand:true ~padding:5) () in let proofw = - GMathViewAux.multi_selection_math_view ~width:400 ~height:275 + TermViewer.sequent_viewer ~width:400 ~height:275 ~packing:(scrolled_window1#add) () in let _ = proofw_ref <- Some proofw in let hbox3 = @@ -3139,38 +2552,34 @@ object(self) ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in *) - ignore(exactb#connect#clicked exact) ; - ignore(applyb#connect#clicked apply) ; - ignore(elimintrossimplb#connect#clicked elimintrossimpl) ; - ignore(elimtypeb#connect#clicked elimtype) ; - ignore(foldwhdb#connect#clicked fold_whd) ; - ignore(foldreduceb#connect#clicked fold_reduce) ; - ignore(foldsimplb#connect#clicked fold_simpl) ; - ignore(cutb#connect#clicked cut) ; - ignore(changeb#connect#clicked change) ; - ignore(letinb#connect#clicked letin) ; - ignore(ringb#connect#clicked ring) ; - ignore(fourierb#connect#clicked fourier) ; - ignore(rewritesimplb#connect#clicked rewritesimpl) ; - ignore(rewritebacksimplb#connect#clicked rewritebacksimpl) ; - ignore(replaceb#connect#clicked replace) ; - ignore(reflexivityb#connect#clicked reflexivity) ; - ignore(symmetryb#connect#clicked symmetry) ; - ignore(transitivityb#connect#clicked transitivity) ; - ignore(existsb#connect#clicked exists) ; - ignore(splitb#connect#clicked split) ; - ignore(leftb#connect#clicked left) ; - ignore(rightb#connect#clicked right) ; - ignore(assumptionb#connect#clicked assumption) ; - ignore(absurdb#connect#clicked absurd) ; - ignore(contradictionb#connect#clicked contradiction) ; - ignore(introsb#connect#clicked intros) ; + 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(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)) ; - ignore(decomposeb#connect#clicked decompose) ; (* Zack: spostare in una toolbar ignore(whdb#connect#clicked whd) ; ignore(reduceb#connect#clicked reduce) ; @@ -3179,6 +2588,10 @@ object(self) 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 ;; @@ -3189,10 +2602,10 @@ class empty_page = GBin.scrolled_window ~border_width:10 ~packing:(vbox1#pack ~expand:true ~padding:5) () in let proofw = - GMathViewAux.single_selection_math_view ~width:400 ~height:275 + TermViewer.sequent_viewer ~width:400 ~height:275 ~packing:(scrolled_window1#add) () in object(self) - method proofw = (assert false : GMathViewAux.single_selection_math_view) + method proofw = (assert false : TermViewer.sequent_viewer) method content = vbox1 method compute = (assert false : unit) end @@ -3401,7 +2814,7 @@ class rendering_window output (notebook : notebook) = object method outputhtml = outputhtml method inputt = inputt - method output = (output : GMathViewAux.single_selection_math_view) + method output = (output : TermViewer.proof_viewer) method notebook = notebook method show = window#show initializer @@ -3429,11 +2842,10 @@ end;; let initialize_everything () = let module U = Unix in - let output = GMathViewAux.single_selection_math_view ~width:350 ~height:280 () 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' ; - mml_of_cic_term_ref := mml_of_cic_term ; rendering_window'#show () ; GMain.Main.main () ;; diff --git a/helm/gTopLevel/invokeTactics.ml b/helm/gTopLevel/invokeTactics.ml new file mode 100644 index 000000000..0d6f75d99 --- /dev/null +++ b/helm/gTopLevel/invokeTactics.ml @@ -0,0 +1,465 @@ +(* Copyright (C) 2000-2002, 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 *) +(* 29/01/2003 *) +(* *) +(* *) +(******************************************************************************) + +exception RefreshSequentException of exn;; +exception RefreshProofException of exn;; + +module type Callbacks = + sig + val sequent_viewer : unit -> TermViewer.sequent_viewer + val term_editor : unit -> TermEditor.term_editor + val get_current_scratch_infos : + unit -> + (Cic.term * + (Cic.id, Cic.term) Hashtbl.t * + (Cic.id, Cic.id option) Hashtbl.t * + (string, Cic.hypothesis) Hashtbl.t + ) option + val set_current_scratch_infos : + (Cic.term * + (Cic.id, Cic.term) Hashtbl.t * + (Cic.id, Cic.id option) Hashtbl.t * + (string, Cic.hypothesis) Hashtbl.t + ) option -> unit + val refresh_proof : unit -> unit + val refresh_goals : unit -> unit + val decompose_uris_choice_callback : + (UriManager.uri * int * 'a) list -> + (UriManager.uri * int * 'b list) list + val mk_fresh_name_callback : + Cic.context -> Cic.name -> typ:Cic.term -> Cic.name + val output_html : string -> unit + end +;; + +module Make(C:Callbacks) = + struct + + let call_tactic tactic () = + let savedproof = !ProofEngine.proof in + let savedgoal = !ProofEngine.goal in + begin + try + tactic () ; + C.refresh_goals () ; + C.refresh_proof () + with + RefreshSequentException e -> + C.output_html + ("

Exception raised during the refresh of the " ^ + "sequent: " ^ Printexc.to_string e ^ "

") ; + ProofEngine.proof := savedproof ; + ProofEngine.goal := savedgoal ; + C.refresh_goals () + | RefreshProofException e -> + C.output_html + ("

Exception raised during the refresh of the " ^ + "proof: " ^ Printexc.to_string e ^ "

") ; + ProofEngine.proof := savedproof ; + ProofEngine.goal := savedgoal ; + C.refresh_goals () ; + C.refresh_proof () + | e -> + C.output_html + ("

" ^ Printexc.to_string e ^ "

") ; + ProofEngine.proof := savedproof ; + ProofEngine.goal := savedgoal + end + + let call_tactic_with_input tactic () = + let savedproof = !ProofEngine.proof in + let savedgoal = !ProofEngine.goal in + let uri,metasenv,bo,ty = + match !ProofEngine.proof with + None -> assert false + | Some (uri,metasenv,bo,ty) -> uri,metasenv,bo,ty + in + let canonical_context = + match !ProofEngine.goal with + None -> assert false + | Some metano -> + let (_,canonical_context,_) = + List.find (function (m,_,_) -> m=metano) metasenv + in + canonical_context + in + try + let metasenv',expr = + (C.term_editor ())#get_metasenv_and_term canonical_context metasenv + in + ProofEngine.proof := Some (uri,metasenv',bo,ty) ; + tactic expr ; + C.refresh_goals () ; + C.refresh_proof () ; + (C.term_editor ())#reset + with + RefreshSequentException e -> + C.output_html + ("

Exception raised during the refresh of the " ^ + "sequent: " ^ Printexc.to_string e ^ "

") ; + ProofEngine.proof := savedproof ; + ProofEngine.goal := savedgoal ; + C.refresh_goals () + | RefreshProofException e -> + C.output_html + ("

Exception raised during the refresh of the " ^ + "proof: " ^ Printexc.to_string e ^ "

") ; + ProofEngine.proof := savedproof ; + ProofEngine.goal := savedgoal ; + C.refresh_goals () ; + C.refresh_proof () + | e -> + C.output_html + ("

" ^ Printexc.to_string e ^ "

") ; + ProofEngine.proof := savedproof ; + ProofEngine.goal := savedgoal + + let call_tactic_with_goal_input tactic () = + let module L = LogicalOperations in + let module G = Gdome in + let savedproof = !ProofEngine.proof in + let savedgoal = !ProofEngine.goal in + match (C.sequent_viewer ())#get_selected_terms with + [term] -> + begin + try + tactic term ; + C.refresh_goals () ; + C.refresh_proof () + with + RefreshSequentException e -> + C.output_html + ("

Exception raised during the refresh of " ^ + "the sequent: " ^ Printexc.to_string e ^ "

") ; + ProofEngine.proof := savedproof ; + ProofEngine.goal := savedgoal ; + C.refresh_goals () + | RefreshProofException e -> + C.output_html + ("

Exception raised during the refresh of " ^ + "the proof: " ^ Printexc.to_string e ^ "

") ; + ProofEngine.proof := savedproof ; + ProofEngine.goal := savedgoal ; + C.refresh_goals () ; + C.refresh_proof () + | e -> + C.output_html + ("

" ^ Printexc.to_string e ^ "

") ; + ProofEngine.proof := savedproof ; + ProofEngine.goal := savedgoal ; + end + | [] -> + C.output_html + ("

No term selected

") + | _ -> + C.output_html + ("

Many terms selected

") + + let call_tactic_with_goal_inputs tactic () = + let module L = LogicalOperations in + let module G = Gdome in + let savedproof = !ProofEngine.proof in + let savedgoal = !ProofEngine.goal in + try + match (C.sequent_viewer ())#get_selected_terms with + [] -> + C.output_html + ("

No term selected

") + | terms -> + tactic terms ; + C.refresh_goals () ; + C.refresh_proof () + with + RefreshSequentException e -> + C.output_html + ("

Exception raised during the refresh of the " ^ + "sequent: " ^ Printexc.to_string e ^ "

") ; + ProofEngine.proof := savedproof ; + ProofEngine.goal := savedgoal ; + C.refresh_goals () + | RefreshProofException e -> + C.output_html + ("

Exception raised during the refresh of the " ^ + "proof: " ^ Printexc.to_string e ^ "

") ; + ProofEngine.proof := savedproof ; + ProofEngine.goal := savedgoal ; + C.refresh_goals () ; + C.refresh_proof () + | e -> + C.output_html + ("

" ^ Printexc.to_string e ^ "

") ; + ProofEngine.proof := savedproof ; + ProofEngine.goal := savedgoal + + let call_tactic_with_input_and_goal_input tactic () = + let module L = LogicalOperations in + let module G = Gdome in + let savedproof = !ProofEngine.proof in + let savedgoal = !ProofEngine.goal in + match (C.sequent_viewer ())#get_selected_terms with + [term] -> + begin + try + let uri,metasenv,bo,ty = + match !ProofEngine.proof with + None -> assert false + | Some (uri,metasenv,bo,ty) -> uri,metasenv,bo,ty + in + let canonical_context = + match !ProofEngine.goal with + None -> assert false + | Some metano -> + let (_,canonical_context,_) = + List.find (function (m,_,_) -> m=metano) metasenv + in + canonical_context in + let (metasenv',expr) = + (C.term_editor ())#get_metasenv_and_term canonical_context metasenv + in + ProofEngine.proof := Some (uri,metasenv',bo,ty) ; + tactic ~goal_input:term ~input:expr ; + C.refresh_goals () ; + C.refresh_proof () ; + (C.term_editor ())#reset + with + RefreshSequentException e -> + C.output_html + ("

Exception raised during the refresh of " ^ + "the sequent: " ^ Printexc.to_string e ^ "

") ; + ProofEngine.proof := savedproof ; + ProofEngine.goal := savedgoal ; + C.refresh_goals () + | RefreshProofException e -> + C.output_html + ("

Exception raised during the refresh of " ^ + "the proof: " ^ Printexc.to_string e ^ "

") ; + ProofEngine.proof := savedproof ; + ProofEngine.goal := savedgoal ; + C.refresh_goals () ; + C.refresh_proof () + | e -> + C.output_html + ("

" ^ Printexc.to_string e ^ "

") ; + ProofEngine.proof := savedproof ; + ProofEngine.goal := savedgoal ; + end + | [] -> + C.output_html + ("

No term selected

") + | _ -> + C.output_html + ("

Many terms selected

") + + let call_tactic_with_goal_input_in_scratch tactic scratch_window () = + let module L = LogicalOperations in + let module G = Gdome in + let mmlwidget = + (scratch_window#mmlwidget : GMathViewAux.multi_selection_math_view) in + let savedproof = !ProofEngine.proof in + let savedgoal = !ProofEngine.goal in + match mmlwidget#get_selections with + [node] -> + let xpath = + ((node : Gdome.element)#getAttributeNS + ~namespaceURI:Misc.helmns + ~localName:(G.domString "xref"))#to_string + in + if xpath = "" then assert false (* "ERROR: No xref found!!!" *) + else + begin + try + match C.get_current_scratch_infos () with + (* term is the whole goal in the scratch_area *) + Some (term,ids_to_terms, ids_to_father_ids,_) -> + let id = xpath in + let expr = tactic term (Hashtbl.find ids_to_terms id) in + let mml,scratch_infos = + ApplyStylesheets.mml_of_cic_term 111 expr + in + C.set_current_scratch_infos (Some scratch_infos) ; + scratch_window#show () ; + scratch_window#mmlwidget#load_doc ~dom:mml + | None -> assert false (* "ERROR: No current term!!!" *) + with + e -> + C.output_html + ("

" ^ Printexc.to_string e ^ "

") + end + | [] -> + C.output_html + ("

No term selected

") + | _ -> + C.output_html + ("

Many terms selected

") + + let call_tactic_with_goal_inputs_in_scratch tactic scratch_window () = + let module L = LogicalOperations in + let module G = Gdome in + let mmlwidget = + (scratch_window#mmlwidget : GMathViewAux.multi_selection_math_view) in + let savedproof = !ProofEngine.proof in + let savedgoal = !ProofEngine.goal in + match mmlwidget#get_selections with + [] -> + C.output_html + ("

No term selected

") + | l -> + try + match C.get_current_scratch_infos () with + (* term is the whole goal in the scratch_area *) + Some (term,ids_to_terms, ids_to_father_ids,_) -> + let term_of_node node = + let xpath = + ((node : Gdome.element)#getAttributeNS + ~namespaceURI:Misc.helmns + ~localName:(G.domString "xref"))#to_string + in + if xpath = "" then assert false (* "ERROR: No xref found!!!" *) + else + let id = xpath in + Hashtbl.find ids_to_terms id + in + let terms = List.map term_of_node l in + let expr = tactic terms term in + let mml,scratch_infos = + ApplyStylesheets.mml_of_cic_term 111 expr + in + C.set_current_scratch_infos (Some scratch_infos) ; + scratch_window#show () ; + scratch_window#mmlwidget#load_doc ~dom:mml + | None -> assert false (* "ERROR: No current term!!!" *) + with + e -> + C.output_html + ("

" ^ Printexc.to_string e ^ "

") + + let call_tactic_with_hypothesis_input tactic () = + let module L = LogicalOperations in + let module G = Gdome in + let savedproof = !ProofEngine.proof in + let savedgoal = !ProofEngine.goal in + match (C.sequent_viewer ())#get_selected_hypotheses with + [hypothesis] -> + begin + try + tactic hypothesis ; + C.refresh_goals () ; + C.refresh_proof () + with + RefreshSequentException e -> + C.output_html + ("

Exception raised during the refresh of " ^ + "the sequent: " ^ Printexc.to_string e ^ "

") ; + ProofEngine.proof := savedproof ; + ProofEngine.goal := savedgoal ; + C.refresh_goals () + | RefreshProofException e -> + C.output_html + ("

Exception raised during the refresh of " ^ + "the proof: " ^ Printexc.to_string e ^ "

") ; + ProofEngine.proof := savedproof ; + ProofEngine.goal := savedgoal ; + C.refresh_goals () ; + C.refresh_proof () + | e -> + C.output_html + ("

" ^ Printexc.to_string e ^ "

") ; + ProofEngine.proof := savedproof ; + ProofEngine.goal := savedgoal ; + end + | [] -> + C.output_html + ("

No hypothesis selected

") + | _ -> + C.output_html + ("

Many hypothesis selected

") + + + let intros = + call_tactic + (ProofEngine.intros ~mk_fresh_name_callback:C.mk_fresh_name_callback) + let exact = call_tactic_with_input ProofEngine.exact + let apply = call_tactic_with_input ProofEngine.apply + let elimintrossimpl = call_tactic_with_input ProofEngine.elim_intros_simpl + let elimtype = call_tactic_with_input ProofEngine.elim_type + let whd = call_tactic_with_goal_inputs ProofEngine.whd + let reduce = call_tactic_with_goal_inputs ProofEngine.reduce + let simpl = call_tactic_with_goal_inputs ProofEngine.simpl + let fold_whd = call_tactic_with_input ProofEngine.fold_whd + let fold_reduce = call_tactic_with_input ProofEngine.fold_reduce + let fold_simpl = call_tactic_with_input ProofEngine.fold_simpl + let cut = + call_tactic_with_input + (ProofEngine.cut ~mk_fresh_name_callback:C.mk_fresh_name_callback) + let change = call_tactic_with_input_and_goal_input ProofEngine.change + let letin = + call_tactic_with_input + (ProofEngine.letin ~mk_fresh_name_callback:C.mk_fresh_name_callback) + let ring = call_tactic ProofEngine.ring + let clearbody = call_tactic_with_hypothesis_input ProofEngine.clearbody + let clear = call_tactic_with_hypothesis_input ProofEngine.clear + let fourier = call_tactic ProofEngine.fourier + let rewritesimpl = call_tactic_with_input ProofEngine.rewrite_simpl + let rewritebacksimpl = call_tactic_with_input ProofEngine.rewrite_back_simpl + let replace = call_tactic_with_input_and_goal_input ProofEngine.replace + let reflexivity = call_tactic ProofEngine.reflexivity + let symmetry = call_tactic ProofEngine.symmetry + let transitivity = call_tactic_with_input ProofEngine.transitivity + let exists = call_tactic ProofEngine.exists + let split = call_tactic ProofEngine.split + let left = call_tactic ProofEngine.left + let right = call_tactic ProofEngine.right + let assumption = call_tactic ProofEngine.assumption + let generalize = + call_tactic_with_goal_inputs + (ProofEngine.generalize ~mk_fresh_name_callback:C.mk_fresh_name_callback) + let absurd = call_tactic_with_input ProofEngine.absurd + let contradiction = call_tactic ProofEngine.contradiction + let decompose = + call_tactic_with_input + (ProofEngine.decompose + ~uris_choice_callback:C.decompose_uris_choice_callback) + let whd_in_scratch scratch_window = + call_tactic_with_goal_inputs_in_scratch ProofEngine.whd_in_scratch + scratch_window + let reduce_in_scratch scratch_window = + call_tactic_with_goal_inputs_in_scratch ProofEngine.reduce_in_scratch + scratch_window + let simpl_in_scratch scratch_window = + call_tactic_with_goal_inputs_in_scratch ProofEngine.simpl_in_scratch + scratch_window + +end +;; diff --git a/helm/gTopLevel/invokeTactics.mli b/helm/gTopLevel/invokeTactics.mli new file mode 100644 index 000000000..df911a02f --- /dev/null +++ b/helm/gTopLevel/invokeTactics.mli @@ -0,0 +1,113 @@ +(* Copyright (C) 2000-2002, 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 *) +(* 30/01/2003 *) +(* *) +(* *) +(******************************************************************************) + +exception RefreshSequentException of exn +exception RefreshProofException of exn + +module type Callbacks = + sig + val sequent_viewer : unit -> TermViewer.sequent_viewer + val term_editor : unit -> TermEditor.term_editor + val get_current_scratch_infos : + unit -> + (Cic.term * + (Cic.id, Cic.term) Hashtbl.t * + (Cic.id, Cic.id option) Hashtbl.t * + (string, Cic.hypothesis) Hashtbl.t + ) option + val set_current_scratch_infos : + (Cic.term * + (Cic.id, Cic.term) Hashtbl.t * + (Cic.id, Cic.id option) Hashtbl.t * + (string, Cic.hypothesis) Hashtbl.t + ) option -> unit + val refresh_proof : unit -> unit + val refresh_goals : unit -> unit + val decompose_uris_choice_callback : + (UriManager.uri * int * 'a) list -> + (UriManager.uri * int * 'b list) list + val mk_fresh_name_callback : + Cic.context -> Cic.name -> typ:Cic.term -> Cic.name + val output_html : string -> unit + end + +module Make (C : Callbacks) : + sig + val intros : unit -> unit + val exact : unit -> unit + val apply : unit -> unit + val elimintrossimpl : unit -> unit + val elimtype : unit -> unit + val whd : unit -> unit + val reduce : unit -> unit + val simpl : unit -> unit + val fold_whd : unit -> unit + val fold_reduce : unit -> unit + val fold_simpl : unit -> unit + val cut : unit -> unit + val change : unit -> unit + val letin : unit -> unit + val ring : unit -> unit + val clearbody : unit -> unit + val clear : unit -> unit + val fourier : unit -> unit + val rewritesimpl : unit -> unit + val rewritebacksimpl : unit -> unit + val replace : unit -> unit + val reflexivity : unit -> unit + val symmetry : unit -> unit + val transitivity : unit -> unit + val exists : unit -> unit + val split : unit -> unit + val left : unit -> unit + val right : unit -> unit + val assumption : unit -> unit + val generalize : unit -> unit + val absurd : unit -> unit + val contradiction : unit -> unit + val decompose : unit -> unit + val whd_in_scratch : + < mmlwidget : GMathViewAux.multi_selection_math_view; + show : unit -> 'a; .. > -> + unit -> unit + val reduce_in_scratch : + < mmlwidget : GMathViewAux.multi_selection_math_view; + show : unit -> 'a; .. > -> + unit -> unit + val simpl_in_scratch : + < mmlwidget : GMathViewAux.multi_selection_math_view; + show : unit -> 'a; .. > -> + unit -> unit + end diff --git a/helm/gTopLevel/termViewer.ml b/helm/gTopLevel/termViewer.ml new file mode 100644 index 000000000..cb3b23a00 --- /dev/null +++ b/helm/gTopLevel/termViewer.ml @@ -0,0 +1,232 @@ +(* Copyright (C) 2000-2002, 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 *) +(* 29/01/2003 *) +(* *) +(* *) +(******************************************************************************) + +(* List utility functions *) +exception Skip;; + +let list_map_fail f = + let rec aux = + function + [] -> [] + | he::tl -> + try + let he' = f he in + he'::(aux tl) + with Skip -> + (aux tl) + in + aux +;; +(* End of the list utility functions *) + +(** A widget to render sequents **) + +class sequent_viewer obj = + object(self) + + inherit GMathViewAux.multi_selection_math_view obj + + val mutable current_infos = None + + (* returns the list of selected terms *) + (* selections which are not terms are ignored *) + method get_selected_terms = + let selections = self#get_selections in + list_map_fail + (function node -> + let xpath = + ((node : Gdome.element)#getAttributeNS + ~namespaceURI:Misc.helmns + ~localName:(Gdome.domString "xref"))#to_string + in + if xpath = "" then assert false (* "ERROR: No xref found!!!" *) + else + match current_infos with + Some (ids_to_terms,_,_) -> + let id = xpath in + (try + Hashtbl.find ids_to_terms id + with _ -> raise Skip) + | None -> assert false (* "ERROR: No current term!!!" *) + ) selections + + (* returns the list of selected hypotheses *) + (* selections which are not hypotheses are ignored *) + method get_selected_hypotheses = + let selections = self#get_selections in + list_map_fail + (function node -> + let xpath = + ((node : Gdome.element)#getAttributeNS + ~namespaceURI:Misc.helmns + ~localName:(Gdome.domString "xref"))#to_string + in + if xpath = "" then assert false (* "ERROR: No xref found!!!" *) + else + match current_infos with + Some (_,_,ids_to_hypotheses) -> + let id = xpath in + (try + Hashtbl.find ids_to_hypotheses id + with _ -> raise Skip) + | None -> assert false (* "ERROR: No current term!!!" *) + ) selections + + method load_sequent metasenv sequent = + let sequent_gdome,ids_to_terms,ids_to_father_ids,ids_to_hypotheses = + SequentPp.XmlPp.print_sequent metasenv sequent in + let sequent_doc = + Xml2Gdome.document_of_xml Misc.domImpl sequent_gdome in + let sequent_mml = + ApplyStylesheets.apply_sequent_stylesheets sequent_doc + in + self#load_doc ~dom:sequent_mml ; + current_infos <- + Some (ids_to_terms,ids_to_father_ids,ids_to_hypotheses) + end +;; + +let sequent_viewer ?adjustmenth ?adjustmentv ?font_size ?font_manager + ?border_width ?width ?height ?packing ?show () = + let w = + GtkMathView.MathView.create + ?adjustmenth:(Gaux.may_map ~f:GData.as_adjustment adjustmenth) + ?adjustmentv:(Gaux.may_map ~f:GData.as_adjustment adjustmentv) + () + in + GtkBase.Container.set w ?border_width ?width ?height; + let mathview = GObj.pack_return (new sequent_viewer w) ~packing ~show in + begin + match font_size with + | Some size -> mathview#set_font_size size + | None -> () + end; + begin + match font_manager with + | Some manager -> mathview#set_font_manager_type ~fm_type:manager + | None -> () + end; + mathview +;; + + +(** A widget to render proofs **) + +class proof_viewer obj = + object(self) + + inherit GMathViewAux.single_selection_math_view obj + + val mutable current_infos = None + + method make_sequent_of_selected_term = + match self#get_selection with + Some node -> + let xpath = + ((node : Gdome.element)#getAttributeNS + ~namespaceURI:Misc.helmns + ~localName:(Gdome.domString "xref"))#to_string + in + if xpath = "" then assert false (* "ERROR: No xref found!!!" *) + else + begin + match current_infos with + Some (ids_to_terms, ids_to_father_ids, _, _) -> + let id = xpath in + LogicalOperations.to_sequent id ids_to_terms ids_to_father_ids + | None -> assert false (* "ERROR: No current term!!!" *) + end + | None -> assert false (* "ERROR: No selection!!!" *) + + method focus_sequent_of_selected_term = + match self#get_selection with + Some node -> + let xpath = + ((node : Gdome.element)#getAttributeNS + ~namespaceURI:Misc.helmns + ~localName:(Gdome.domString "xref"))#to_string + in + if xpath = "" then assert false (* "ERROR: No xref found!!!" *) + else + begin + match current_infos with + Some (ids_to_terms, ids_to_father_ids, _, _) -> + let id = xpath in + LogicalOperations.focus id ids_to_terms ids_to_father_ids + | None -> assert false (* "ERROR: No current term!!!" *) + end + | None -> assert false (* "ERROR: No selection!!!" *) + + method load_proof uri currentproof = + 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 currentproof + in + let mml = + ApplyStylesheets.mml_of_cic_object + ~explode_all:true uri acic ids_to_inner_sorts ids_to_inner_types + in + self#load_doc ~dom:mml ; + current_infos <- + Some + (ids_to_terms,ids_to_father_ids,ids_to_conjectures,ids_to_hypotheses) ; + (acic, ids_to_inner_types, ids_to_inner_sorts) + end +;; + +let proof_viewer ?adjustmenth ?adjustmentv ?font_size ?font_manager + ?border_width ?width ?height ?packing ?show () = + let w = + GtkMathView.MathView.create + ?adjustmenth:(Gaux.may_map ~f:GData.as_adjustment adjustmenth) + ?adjustmentv:(Gaux.may_map ~f:GData.as_adjustment adjustmentv) + () + in + GtkBase.Container.set w ?border_width ?width ?height; + let mathview = GObj.pack_return (new proof_viewer w) ~packing ~show in + begin + match font_size with + | Some size -> mathview#set_font_size size + | None -> () + end; + begin + match font_manager with + | Some manager -> mathview#set_font_manager_type ~fm_type:manager + | None -> () + end; + mathview +;; diff --git a/helm/gTopLevel/termViewer.mli b/helm/gTopLevel/termViewer.mli new file mode 100644 index 000000000..c043f5cb6 --- /dev/null +++ b/helm/gTopLevel/termViewer.mli @@ -0,0 +1,100 @@ +(* Copyright (C) 2000-2002, 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 *) +(* 29/01/2003 *) +(* *) +(* *) +(******************************************************************************) + +(** A widget to render sequents **) + +class sequent_viewer : + Gtk_mathview.math_view Gtk.obj -> + object + inherit GMathViewAux.multi_selection_math_view + + (* returns the list of selected terms *) + (* selections which are not terms are ignored *) + method get_selected_terms : Cic.term list + + (* returns the list of selected hypotheses *) + (* selections which are not hypotheses are ignored *) + method get_selected_hypotheses : Cic.hypothesis list + + method load_sequent : Cic.metasenv -> Cic.conjecture -> unit + end + +val sequent_viewer : + ?adjustmenth:GData.adjustment -> + ?adjustmentv:GData.adjustment -> + ?font_size:int -> + ?font_manager:[ `font_manager_gtk | `font_manager_t1] -> + ?border_width:int -> + ?width:int -> + ?height:int -> + ?packing:(GObj.widget -> unit) -> + ?show:bool -> + unit -> sequent_viewer + +(** A widget to render proofs **) + +class proof_viewer : + Gtk_mathview.math_view Gtk.obj -> + object + inherit GMathViewAux.single_selection_math_view + + (* the new current sequent becomes the one obtained *) + (* perforating the proof where the selection is *) + method make_sequent_of_selected_term : unit + + (* the new current sequent becomes the one obtained *) + (* focusing the proof on the selected metavariable *) + method focus_sequent_of_selected_term : unit + + (* load_proof also returns the annotated cic term and the *) + (* ids_to_inner_types and ids_to_inner_sorts maps. *) + method load_proof : + UriManager.uri -> Cic.obj -> + Cic.annobj * (Cic.id, Cic2acic.anntypes) Hashtbl.t * + (Cic.id, string) Hashtbl.t + + end + +val proof_viewer : + ?adjustmenth:GData.adjustment -> + ?adjustmentv:GData.adjustment -> + ?font_size:int -> + ?font_manager:[ `font_manager_gtk | `font_manager_t1] -> + ?border_width:int -> + ?width:int -> + ?height:int -> + ?packing:(GObj.widget -> unit) -> + ?show:bool -> + unit -> proof_viewer -- 2.39.2