X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FgTopLevel.ml;h=8aa9e828875c13a969005edbdcc30ab4976b704d;hb=7e9ee837f75f38bf01240cdc03dd51c764c2665f;hp=15cfdcd103813cbb0f5f71ba77c2794f19204785;hpb=76cb30ecd0159512548aee0ba7085ab17c6fd5bd;p=helm.git diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml index 15cfdcd10..8aa9e8288 100644 --- a/helm/gTopLevel/gTopLevel.ml +++ b/helm/gTopLevel/gTopLevel.ml @@ -33,9 +33,22 @@ (* *) (******************************************************************************) + +(* CSC: quick fix: a function from [uri#xpointer(path)] to [uri#path] *) +let wrong_xpointer_format_from_wrong_xpointer_format' uri = + try + let index_sharp = String.index uri '#' in + let index_rest = index_sharp + 10 in + let baseuri = String.sub uri 0 index_sharp in + let rest = String.sub uri index_rest (String.length uri - index_rest - 1) in + baseuri ^ "#" ^ rest + with Not_found -> uri +;; + (* GLOBAL CONSTANTS *) let helmns = Gdome.domString "http://www.cs.unibo.it/helm";; +let xlinkns = Gdome.domString "http://www.w3.org/1999/xlink";; let htmlheader = "" ^ @@ -47,7 +60,25 @@ let htmlfooter = "" ;; -let prooffile = "/home/zack/dati/HELM/currentproof.gTopLevel" +(* +let prooffile = "/home/tassi/miohelm/tmp/currentproof";; +let prooffile = "/public/sacerdot/currentproof";; +*) + +let prooffile = "/public/sacerdot/currentproof";; +let prooffiletype = "/public/sacerdot/currentprooftype";; + +(*CSC: the getter should handle the innertypes, not the FS *) +(* +let innertypesfile = "/home/tassi/miohelm/tmp/innertypes";; +let innertypesfile = "/public/sacerdot/innertypes";; +*) + +let innertypesfile = "/public/sacerdot/innertypes";; +let constanttypefile = "/public/sacerdot/constanttype";; + +let empty_id_to_uris = ([],function _ -> None);; + (* GLOBAL REFERENCES (USED BY CALLBACKS) *) @@ -57,6 +88,57 @@ let current_cic_infos = ref None;; let current_goal_infos = ref None;; let current_scratch_infos = ref None;; +let id_to_uris = ref empty_id_to_uris;; + +let check_term = ref (fun _ _ _ -> assert false);; +let mml_of_cic_term_ref = ref (fun _ _ -> assert false);; + +exception RenderingWindowsNotInitialized;; + +let set_rendering_window,rendering_window = + let rendering_window_ref = ref None in + (function rw -> rendering_window_ref := Some rw), + (function () -> + match !rendering_window_ref with + None -> raise RenderingWindowsNotInitialized + | Some rw -> rw + ) +;; + +exception SettingsWindowsNotInitialized;; + +let set_settings_window,settings_window = + let settings_window_ref = ref None in + (function rw -> settings_window_ref := Some rw), + (function () -> + match !settings_window_ref with + None -> raise SettingsWindowsNotInitialized + | Some rw -> rw + ) +;; + +exception OutputHtmlNotInitialized;; + +let set_outputhtml,outputhtml = + let outputhtml_ref = ref None in + (function rw -> outputhtml_ref := Some rw), + (function () -> + match !outputhtml_ref with + None -> raise OutputHtmlNotInitialized + | Some outputhtml -> outputhtml + ) +;; + +exception QedSetSensitiveNotInitialized;; +let qed_set_sensitive = + ref (function _ -> raise QedSetSensitiveNotInitialized) +;; + +exception SaveSetSensitiveNotInitialized;; +let save_set_sensitive = + ref (function _ -> raise SaveSetSensitiveNotInitialized) +;; + (* COMMAND LINE OPTIONS *) let usedb = ref true @@ -68,8 +150,298 @@ let argspec = in Arg.parse argspec ignore "" +(* A WIDGET TO ENTER CIC TERMS *) + +class term_editor ?packing ?width ?height ?isnotempty_callback () = + let input = GEdit.text ~editable:true ?width ?height ?packing () in + let _ = + match isnotempty_callback with + None -> () + | Some callback -> + ignore(input#connect#changed (function () -> callback (input#length > 0))) + in +object(self) + method coerce = input#coerce + method reset = + input#delete_text 0 input#length + (* CSC: txt is now a string, but should be of type Cic.term *) + method set_term txt = + self#reset ; + ignore ((input#insert_text txt) ~pos:0) + (* CSC: this method should disappear *) + method get_as_string = + input#get_chars 0 input#length + method get_term ~context ~metasenv = + let lexbuf = Lexing.from_string (input#get_chars 0 input#length) in + CicTextualParserContext.main ~context ~metasenv CicTextualLexer.token lexbuf +end +;; + +(* MISC FUNCTIONS *) + +exception IllFormedUri of string;; + +let cic_textual_parser_uri_of_string uri' = + try + (* Constant *) + if String.sub uri' (String.length uri' - 4) 4 = ".con" then + CicTextualParser0.ConUri (UriManager.uri_of_string uri') + else + if String.sub uri' (String.length uri' - 4) 4 = ".var" then + CicTextualParser0.VarUri (UriManager.uri_of_string uri') + else + (try + (* Inductive Type *) + let uri'',typeno = CicTextualLexer.indtyuri_of_uri uri' in + CicTextualParser0.IndTyUri (uri'',typeno) + with + _ -> + (* Constructor of an Inductive Type *) + let uri'',typeno,consno = + CicTextualLexer.indconuri_of_uri uri' + in + CicTextualParser0.IndConUri (uri'',typeno,consno) + ) + with + _ -> raise (IllFormedUri uri') +;; + +let term_of_cic_textual_parser_uri uri = + let module C = Cic in + let module CTP = CicTextualParser0 in + match uri with + CTP.ConUri uri -> C.Const (uri,[]) + | CTP.VarUri uri -> C.Var (uri,[]) + | CTP.IndTyUri (uri,tyno) -> C.MutInd (uri,tyno,[]) + | CTP.IndConUri (uri,tyno,consno) -> C.MutConstruct (uri,tyno,consno,[]) +;; + +let string_of_cic_textual_parser_uri uri = + let module C = Cic in + let module CTP = CicTextualParser0 in + let uri' = + match uri with + CTP.ConUri uri -> UriManager.string_of_uri uri + | CTP.VarUri uri -> UriManager.string_of_uri uri + | CTP.IndTyUri (uri,tyno) -> + UriManager.string_of_uri uri ^ "#1/" ^ string_of_int (tyno + 1) + | CTP.IndConUri (uri,tyno,consno) -> + UriManager.string_of_uri uri ^ "#1/" ^ string_of_int (tyno + 1) ^ "/" ^ + string_of_int consno + in + (* 4 = String.length "cic:" *) + String.sub uri' 4 (String.length uri' - 4) +;; + +let output_html outputhtml msg = + htmlheader_and_content := !htmlheader_and_content ^ msg ; + outputhtml#source (!htmlheader_and_content ^ htmlfooter) ; + outputhtml#set_topline (-1) +;; + +(* UTILITY FUNCTIONS TO DISAMBIGUATE AN URI *) + +(* Check window *) + +let check_window outputhtml uris = + let window = + GWindow.window + ~width:800 ~modal:true ~title:"Check" ~border_width:2 () in + let notebook = + GPack.notebook ~scrollable:true ~packing:window#add () in + window#show () ; + let render_terms = + List.map + (function uri -> + let scrolled_window = + GBin.scrolled_window ~border_width:10 + ~packing: + (notebook#append_page ~tab_label:((GMisc.label ~text:uri ())#coerce)) + () + in + lazy + (let mmlwidget = + GMathView.math_view + ~packing:scrolled_window#add ~width:400 ~height:280 () in + let expr = + let term = + term_of_cic_textual_parser_uri (cic_textual_parser_uri_of_string uri) + in + (Cic.Cast (term, CicTypeChecker.type_of_aux' [] [] term)) + in + try + let mml = !mml_of_cic_term_ref 111 expr in +prerr_endline ("### " ^ CicPp.ppterm expr) ; + mmlwidget#load_tree ~dom:mml + with + e -> + output_html outputhtml + ("

" ^ Printexc.to_string e ^ "

") + ) + ) uris + in + ignore + (notebook#connect#switch_page + (function i -> Lazy.force (List.nth render_terms i))) +;; + +exception NoChoice;; + +let + interactive_user_uri_choice ~selection_mode ?(ok="Ok") ~title ~msg uris += + let choices = ref [] in + let chosen = 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 () 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 checkb = + GButton.button ~label:"Check" + ~packing:(hbox#pack ~padding:5) () in + let _ = checkb#misc#set_sensitive false in + let cancelb = + GButton.button ~label:"Abort" + ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in + (* actions *) + let check_callback () = + assert (List.length !choices > 0) ; + check_window (outputhtml ()) !choices + in + ignore (window#connect#destroy GMain.Main.quit) ; + ignore (cancelb#connect#clicked window#destroy) ; + ignore + (okb#connect#clicked (function () -> chosen := true ; window#destroy ())) ; + ignore (checkb#connect#clicked check_callback) ; + ignore + (clist#connect#select_row + (fun ~row ~column ~event -> + checkb#misc#set_sensitive true ; + okb#misc#set_sensitive true ; + choices := (List.nth uris row)::!choices)) ; + ignore + (clist#connect#unselect_row + (fun ~row ~column ~event -> + choices := + List.filter (function uri -> uri != (List.nth uris row)) !choices)) ; + ignore + (manual_input#connect#changed + (fun _ -> + if manual_input#text = "" then + begin + choices := [] ; + checkb#misc#set_sensitive false ; + okb#misc#set_sensitive false ; + clist#misc#set_sensitive true + end + else + begin + choices := [manual_input#text] ; + clist#unselect_all () ; + checkb#misc#set_sensitive true ; + okb#misc#set_sensitive true ; + clist#misc#set_sensitive false + end)); + window#set_position `CENTER ; + window#show () ; + GMain.Main.main () ; + if !chosen && List.length !choices > 0 then + !choices + else + raise NoChoice +;; + +let interactive_interpretation_choice interpretations = + let chosen = ref None in + let window = + GWindow.window + ~modal:true ~title:"Ambiguous well-typed input." ~border_width:2 () in + let vbox = GPack.vbox ~packing:window#add () in + let lMessage = + GMisc.label + ~text: + ("Ambiguous input since there are many well-typed interpretations." ^ + " Please, choose one of them.") + ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in + let notebook = + GPack.notebook ~scrollable:true + ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in + let _ = + List.map + (function interpretation -> + let clist = + let expected_height = 18 * List.length interpretation in + let height = if expected_height > 400 then 400 else expected_height in + GList.clist ~columns:2 ~packing:notebook#append_page ~height + ~titles:["id" ; "URI"] () + in + ignore + (List.map + (function (id,uri) -> + let n = clist#append [id;uri] in + clist#set_row ~selectable:false n + ) interpretation + ) ; + clist#columns_autosize () + ) interpretations in + let hbox = + GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in + let okb = + GButton.button ~label:"Ok" + ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in + let cancelb = + GButton.button ~label:"Abort" + ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in + (* actions *) + ignore (window#connect#destroy GMain.Main.quit) ; + ignore (cancelb#connect#clicked window#destroy) ; + ignore + (okb#connect#clicked + (function () -> chosen := Some notebook#current_page ; window#destroy ())) ; + window#set_position `CENTER ; + window#show () ; + GMain.Main.main () ; + match !chosen with + None -> raise NoChoice + | Some n -> n +;; + + (* MISC FUNCTIONS *) +(* CSC: IMPERATIVE AND NOT VERY CLEAN, TO GET THE LAST ISSUED QUERY *) +let get_last_query = + let query = ref "" in + MQueryGenerator.set_confirm_query + (function q -> query := MQueryUtil.text_of_query q ; true) ; + function result -> !query ^ "

Result:

" ^ MQueryUtil.text_of_result result "
" +;; + let domImpl = Gdome.domImplementation ();; let parseStyle name = @@ -97,22 +469,23 @@ let getterURL = Configuration.getter_url;; let processorURL = Configuration.processor_url;; let mml_styles = [d_c ; c1 ; g ; c2 ; l];; -let mml_args = - ["processorURL", "'" ^ processorURL ^ "'" ; - "getterURL", "'" ^ getterURL ^ "'" ; - "draw_graphURL", "'http%3A//phd.cs.unibo.it%3A8083/'" ; - "uri_set_queueURL", "'http%3A//phd.cs.unibo.it%3A8084/'" ; - "UNICODEvsSYMBOL", "'symbol'" ; - "doctype-public", "'-//W3C//DTD%20XHTML%201.0%20Transitional//EN'" ; - "encoding", "'iso-8859-1'" ; - "media-type", "'text/html'" ; - "keys", "'d_c%2CC1%2CG%2CC2%2CL'" ; - "interfaceURL", "'http%3A//phd.cs.unibo.it/helm/html/cic/index.html'" ; - "naturalLanguage", "'yes'" ; - "annotations", "'no'" ; - "explodeall", "'true()'" ; - "topurl", "'http://phd.cs.unibo.it/helm'" ; - "CICURI", "'cic:/Coq/Init/Datatypes/bool_ind.con'" ] +let mml_args ~explode_all = + ("explodeall",(if explode_all then "true()" else "false()")):: + ["processorURL", "'" ^ processorURL ^ "'" ; + "getterURL", "'" ^ getterURL ^ "'" ; + "draw_graphURL", "'http%3A//phd.cs.unibo.it%3A8083/'" ; + "uri_set_queueURL", "'http%3A//phd.cs.unibo.it%3A8084/'" ; + "UNICODEvsSYMBOL", "'symbol'" ; + "doctype-public", "'-//W3C//DTD%20XHTML%201.0%20Transitional//EN'" ; + "encoding", "'iso-8859-1'" ; + "media-type", "'text/html'" ; + "keys", "'d_c%2CC1%2CG%2CC2%2CL'" ; + "interfaceURL", "'http%3A//phd.cs.unibo.it/helm/html/cic/index.html'" ; + "naturalLanguage", "'yes'" ; + "annotations", "'no'" ; + "URLs_or_URIs", "'URIs'" ; + "topurl", "'http://phd.cs.unibo.it/helm'" ; + "CICURI", "'cic:/Coq/Init/Datatypes/bool_ind.con'" ] ;; let sequent_styles = [d_c ; c1 ; g ; c2 ; l];; @@ -129,7 +502,8 @@ let sequent_args = "interfaceURL", "'http%3A//phd.cs.unibo.it/helm/html/cic/index.html'" ; "naturalLanguage", "'no'" ; "annotations", "'no'" ; - "explodeall", "'true()'" ; + "explodeall", "true()" ; + "URLs_or_URIs", "'URIs'" ; "topurl", "'http://phd.cs.unibo.it/helm'" ; "CICURI", "'cic:/Coq/Init/Datatypes/bool_ind.con'" ] ;; @@ -151,42 +525,83 @@ let applyStylesheets input styles args = input styles ;; -let mml_of_cic_object uri annobj ids_to_inner_sorts ids_to_inner_types = - let xml = - Cic2Xml.print_object uri ids_to_inner_sorts annobj +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 + Cic2Xml.print_inner_types uri ~ids_to_inner_sorts ~ids_to_inner_types + ~ask_dtd_to_the_getter:true in - let input = Xml2Gdome.document_of_xml domImpl xml in + let input = + match bodyxml with + None -> Xml2Gdome.document_of_xml domImpl xml + | Some bodyxml' -> + Xml.pp xml (Some constanttypefile) ; + Xml2Gdome.document_of_xml 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 "/tmp/innertypes") ; - let output = applyStylesheets input mml_styles mml_args in + Xml.pp xmlinnertypes (Some innertypesfile) ; + let output = applyStylesheets input mml_styles (mml_args ~explode_all) in output ;; - (* pretty print on standard output the current sequent *) -let dumpsequent () = - let metasenv = - match !ProofEngine.proof with - | None -> assert false - | Some (_, metasenv, _, _) -> metasenv +let + save_object_to_disk uri annobj ids_to_inner_sorts ids_to_inner_types pathname += + let name = + let struri = UriManager.string_of_uri uri in + let idx = (String.rindex struri '/') + 1 in + String.sub struri idx (String.length struri - idx) + in + let path = pathname ^ "/" ^ name in + let xml, bodyxml = + Cic2Xml.print_object uri ~ids_to_inner_sorts ~ask_dtd_to_the_getter:false + annobj in - let seq = - match !ProofEngine.goal with - | None -> assert false - | Some metano -> List.find (function (m,_,_) -> m=metano) metasenv + let xmlinnertypes = + Cic2Xml.print_inner_types uri ~ids_to_inner_sorts ~ids_to_inner_types + ~ask_dtd_to_the_getter:false in - print_string ( - "\n" ^ - (SequentPp.TextualPp.print_sequent seq) ^ - "\n"); - print_newline () + (* innertypes *) + let innertypesuri = UriManager.innertypesuri_of_uri uri in + Xml.pp ~quiet:true xmlinnertypes (Some (path ^ ".types.xml")) ; + Getter.register innertypesuri + (Configuration.annotations_url ^ + Str.replace_first (Str.regexp "^cic:") "" + (UriManager.string_of_uri innertypesuri) ^ ".xml" + ) ; + (* constant type / variable / mutual inductive types definition *) + Xml.pp ~quiet:true xml (Some (path ^ ".xml")) ; + Getter.register uri + (Configuration.annotations_url ^ + Str.replace_first (Str.regexp "^cic:") "" + (UriManager.string_of_uri uri) ^ ".xml" + ) ; + match bodyxml with + None -> () + | Some bodyxml' -> + (* constant body *) + let bodyuri = + match UriManager.bodyuri_of_uri uri with + None -> assert false + | Some bodyuri -> bodyuri + in + Xml.pp ~quiet:true bodyxml' (Some (path ^ ".body.xml")) ; + Getter.register bodyuri + (Configuration.annotations_url ^ + Str.replace_first (Str.regexp "^cic:") "" + (UriManager.string_of_uri bodyuri) ^ ".xml" + ) ;; + (* CALLBACKS *) exception RefreshSequentException of exn;; @@ -198,7 +613,9 @@ let refresh_proof (output : GMathView.math_view) = match !ProofEngine.proof with None -> assert false | Some (uri,metasenv,bo,ty) -> - uri,(Cic.CurrentProof (UriManager.name_of_uri 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, @@ -207,7 +624,8 @@ let refresh_proof (output : GMathView.math_view) = Cic2acic.acic_object_of_cic_object currentproof in let mml = - mml_of_cic_object uri acic ids_to_inner_sorts ids_to_inner_types + mml_of_cic_object ~explode_all:true uri acic ids_to_inner_sorts + ids_to_inner_types in output#load_tree mml ; current_cic_infos := @@ -217,14 +635,21 @@ let refresh_proof (output : GMathView.math_view) = 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 ; +prerr_endline ("Offending proof: " ^ CicPp.ppobj (Cic.CurrentProof ("questa",metasenv,bo,ty,[]))) ; flush stderr ; raise (RefreshProofException e) ;; -let refresh_sequent (proofw : GMathView.math_view) = +let refresh_sequent ?(empty_notebook=true) notebook = try match !ProofEngine.goal with - None -> proofw#unload + 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 @@ -235,13 +660,29 @@ let refresh_sequent (proofw : GMathView.math_view) = let sequent_gdome,ids_to_terms,ids_to_father_ids,ids_to_hypotheses = SequentPp.XmlPp.print_sequent metasenv currentsequent in - let sequent_doc = - Xml2Gdome.document_of_xml domImpl sequent_gdome - in - let sequent_mml = - applyStylesheets sequent_doc sequent_styles sequent_args + let regenerate_notebook () = + let skip_switch_page_event = + match metasenv with + (m,_,_)::_ when m = metano -> false + | _ -> true in - proofw#load_tree ~dom:sequent_mml ; + 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 domImpl sequent_gdome in + let sequent_mml = + applyStylesheets sequent_doc sequent_styles sequent_args + in + notebook#set_current_page ~may_skip_switch_page_event:true metano; + notebook#proofw#load_tree ~dom:sequent_mml + end ; current_goal_infos := Some (ids_to_terms,ids_to_father_ids,ids_to_hypotheses) with @@ -256,14 +697,16 @@ let metasenv = 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:"/public/sacerdot/guruguru1" ~indent:true ()) ; + ~name:"/home/galata/miohelm/guruguru1" ~indent:true ()) ; *) let mml_of_cic_term metano term = @@ -295,163 +738,967 @@ let mml_of_cic_term metano term = res ;; -let output_html outputhtml msg = - htmlheader_and_content := !htmlheader_and_content ^ msg ; - outputhtml#source (!htmlheader_and_content ^ htmlfooter) ; - outputhtml#set_topline (-1) -;; +exception OpenConjecturesStillThere;; +exception WrongProof;; -(***********************) -(* TACTICS *) -(***********************) +let pathname_of_annuri uristring = + Configuration.annotations_dir ^ + Str.replace_first (Str.regexp "^cic:") "" uristring +;; -let call_tactic tactic rendering_window () = - let proofw = (rendering_window#proofw : GMathView.math_view) in - let output = (rendering_window#output : GMathView.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 proofw ; - 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 proofw - | 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 proofw ; - refresh_proof output - | e -> - output_html outputhtml - ("

" ^ Printexc.to_string e ^ "

") ; - ProofEngine.proof := savedproof ; - ProofEngine.goal := savedgoal ; - end +let make_dirs dirpath = + ignore (Unix.system ("mkdir -p " ^ dirpath)) ;; -let call_tactic_with_input tactic rendering_window () = - let proofw = (rendering_window#proofw : GMathView.math_view) in - let output = (rendering_window#output : GMathView.math_view) in - let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in - let inputt = (rendering_window#inputt : GEdit.text) in - let savedproof = !ProofEngine.proof in - let savedgoal = !ProofEngine.goal in -(*CSC: Gran cut&paste da sotto... *) - let inputlen = inputt#length in - let input = inputt#get_chars 0 inputlen ^ "\n" in - let lexbuf = Lexing.from_string input in - let curi = - match !ProofEngine.proof with - None -> assert false - | Some (curi,_,_,_) -> curi - in - let metasenv = - match !ProofEngine.proof with - None -> assert false - | Some (_,metasenv,_,_) -> metasenv - in - let context = - List.map - (function - Some (n,_) -> Some n - | None -> None) - (match !ProofEngine.goal with - None -> assert false - | Some metano -> - let (_,canonical_context,_) = - List.find (function (m,_,_) -> m=metano) metasenv - in - canonical_context - ) - in - try - while true do - match - CicTextualParserContext.main curi context CicTextualLexer.token lexbuf - with - None -> () - | Some expr -> - tactic expr ; - refresh_sequent proofw ; - refresh_proof output - done - with - CicTextualParser0.Eof -> - inputt#delete_text 0 inputlen - | 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 proofw - | 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 proofw ; - refresh_proof output - | e -> - output_html outputhtml - ("

" ^ Printexc.to_string e ^ "

") ; - ProofEngine.proof := savedproof ; - ProofEngine.goal := savedgoal ; +let qed () = + match !ProofEngine.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_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 : GMathView.math_view)#load_tree 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) + end + else + raise WrongProof + | _ -> raise OpenConjecturesStillThere ;; -let call_tactic_with_goal_input tactic rendering_window () = - let module L = LogicalOperations in - let module G = Gdome in - let proofw = (rendering_window#proofw : GMathView.math_view) in - let output = (rendering_window#output : GMathView.math_view) in - let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in - let savedproof = !ProofEngine.proof in - let savedgoal = !ProofEngine.goal in - match proofw#get_selection with - Some node -> - let xpath = - ((node : Gdome.element)#getAttributeNS - ~namespaceURI:helmns - ~localName:(G.domString "xref"))#to_string +let save () = + let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in + match !ProofEngine.proof with + None -> assert false + | Some (uri, metasenv, bo, ty) -> + let currentproof = + (*CSC: Wrong: [] is just plainly wrong *) + Cic.CurrentProof (UriManager.name_of_uri uri,metasenv,bo,ty,[]) 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 rendering_window#proofw ; - refresh_proof rendering_window#output - | None -> assert false (* "ERROR: No current term!!!" *) + let (acurrentproof,_,_,ids_to_inner_sorts,_,_,_) = + Cic2acic.acic_object_of_cic_object currentproof + in + let xml, bodyxml = + match + Cic2Xml.print_object uri ~ids_to_inner_sorts + ~ask_dtd_to_the_getter:true acurrentproof with - RefreshSequentException e -> - output_html outputhtml - ("

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

") ; - ProofEngine.proof := savedproof ; + xml,Some bodyxml -> xml,bodyxml + | _,None -> assert false + in + Xml.pp ~quiet:true xml (Some prooffiletype) ; + output_html outputhtml + ("

Current proof type saved to " ^ + prooffiletype ^ "

") ; + Xml.pp ~quiet:true bodyxml (Some prooffile) ; + output_html outputhtml + ("

Current proof body saved to " ^ + prooffile ^ "

") +;; + +(* Used to typecheck the loaded proofs *) +let typecheck_loaded_proof metasenv bo ty = + let module T = CicTypeChecker in + ignore ( + List.fold_left + (fun metasenv ((_,context,ty) as conj) -> + ignore (T.type_of_aux' metasenv context ty) ; + metasenv @ [conj] + ) [] metasenv) ; + ignore (T.type_of_aux' metasenv [] ty) ; + ignore (T.type_of_aux' metasenv [] bo) +;; + +let load () = + let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in + let output = ((rendering_window ())#output : GMathView.math_view) in + let notebook = (rendering_window ())#notebook in + try + match + GToolbox.input_string ~title:"Load Unfinished Proof" ~text:"/dummy.con" + "Choose an URI:" + with + None -> raise NoChoice + | Some uri0 -> + let uri = UriManager.uri_of_string ("cic:" ^ uri0) in + match CicParser.obj_of_xml prooffiletype (Some prooffile) with + Cic.CurrentProof (_,metasenv,bo,ty,_) -> + typecheck_loaded_proof metasenv bo ty ; + ProofEngine.proof := + Some (uri, metasenv, bo, ty) ; + ProofEngine.goal := + (match metasenv with + [] -> None + | (metano,_,_)::_ -> Some metano + ) ; + refresh_proof output ; + refresh_sequent notebook ; + output_html outputhtml + ("

Current proof type loaded from " ^ + prooffiletype ^ "

") ; + output_html outputhtml + ("

Current proof body loaded from " ^ + prooffile ^ "

") ; + !save_set_sensitive true + | _ -> assert false + 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 ^ "

") ; +;; + +let edit_aliases () = + let chosen = ref false in + let window = + GWindow.window + ~width:400 ~modal:true ~title:"Edit Aliases..." ~border_width:2 () in + let vbox = + GPack.vbox ~border_width:0 ~packing:window#add () in + let scrolled_window = + GBin.scrolled_window ~border_width:10 + ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in + let input = GEdit.text ~editable:true ~width:400 ~height:100 + ~packing:scrolled_window#add () in + let hbox = + GPack.hbox ~border_width:0 + ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in + let okb = + GButton.button ~label:"Ok" + ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in + let cancelb = + GButton.button ~label:"Cancel" + ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in + ignore (window#connect#destroy GMain.Main.quit) ; + ignore (cancelb#connect#clicked window#destroy) ; + ignore + (okb#connect#clicked (function () -> chosen := true ; window#destroy ())) ; + let dom,resolve_id = !id_to_uris in + ignore + (input#insert_text ~pos:0 + (String.concat "\n" + (List.map + (function v -> + let uri = + match resolve_id v with + None -> assert false + | Some uri -> uri + in + "alias " ^ v ^ " " ^ + (string_of_cic_textual_parser_uri uri) + ) dom))) ; + window#show () ; + GMain.Main.main () ; + if !chosen then + let dom,resolve_id = + let inputtext = input#get_chars 0 input#length 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 = Str.matched_group 2 inputtext in + let uri = + 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 uri else resolve_id id') + with + Not_found -> empty_id_to_uris + in + aux 0 + in + id_to_uris := dom,resolve_id +;; + +let proveit () = + let module L = LogicalOperations in + let module G = Gdome in + let notebook = (rendering_window ())#notebook in + let output = (rendering_window ())#output in + let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in + match (rendering_window ())#output#get_selection with + Some node -> + let xpath = + ((node : Gdome.element)#getAttributeNS + (*CSC: OCAML DIVERGE + ((element : G.element)#getAttributeNS + *) + ~namespaceURI: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!!!" *) +;; + +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 + match (rendering_window ())#output#get_selection with + Some node -> + let xpath = + ((node : Gdome.element)#getAttributeNS + (*CSC: OCAML DIVERGE + ((element : G.element)#getAttributeNS + *) + ~namespaceURI: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!!!" *) +;; + +exception NoPrevGoal;; +exception NoNextGoal;; + +let setgoal metano = + 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 metasenv = + match !ProofEngine.proof with + None -> assert false + | Some (_,metasenv,_,_) -> metasenv + in + try + refresh_sequent ~empty_notebook:false notebook + with + RefreshSequentException e -> + output_html outputhtml + ("

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

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

" ^ Printexc.to_string e ^ "

") +;; + +let show_in_show_window, show_in_show_window_callback = + let window = + GWindow.window ~width:800 ~border_width:2 () in + let scrolled_window = + GBin.scrolled_window ~border_width:10 ~packing:window#add () in + let mmlwidget = + GMathView.math_view ~packing:scrolled_window#add ~width:600 ~height:400 () in + let _ = window#event#connect#delete (fun _ -> window#misc#hide () ; true ) in + let href = Gdome.domString "href" in + let show_in_show_window uri = + let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in + try + CicTypeChecker.typecheck uri ; + let obj = CicEnvironment.get_cooked_obj uri 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 obj + in + let mml = + mml_of_cic_object ~explode_all:false uri acic ids_to_inner_sorts + ids_to_inner_types + in + window#set_title (UriManager.string_of_uri uri) ; + window#misc#hide () ; window#show () ; + mmlwidget#load_tree mml ; + with + e -> + output_html outputhtml + ("

" ^ Printexc.to_string e ^ "

") ; + in + let show_in_show_window_callback mmlwidget (n : Gdome.element) = + if n#hasAttributeNS ~namespaceURI:xlinkns ~localName:href then + let uri = + (n#getAttributeNS ~namespaceURI:xlinkns ~localName:href)#to_string + in + show_in_show_window (UriManager.uri_of_string uri) + else + if mmlwidget#get_action <> None then + mmlwidget#action_toggle + in + let _ = + mmlwidget#connect#clicked (show_in_show_window_callback mmlwidget) + in + show_in_show_window, show_in_show_window_callback +;; + +exception NoObjectsLocated;; + +let user_uri_choice ~title ~msg uris = + let uri = + match uris with + [] -> raise NoObjectsLocated + | [uri] -> uri + | uris -> + match + interactive_user_uri_choice ~selection_mode:`SINGLE ~title ~msg uris + with + [uri] -> uri + | _ -> assert false + in + String.sub uri 4 (String.length uri - 4) +;; + +let locate_callback id = + let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in + let result = MQueryGenerator.locate id in + let uris = + List.map + (function uri,_ -> wrong_xpointer_format_from_wrong_xpointer_format' uri) + result in + let html = + ("

Locate Query: 

" ^ get_last_query result ^ "
") + in + output_html outputhtml html ; + user_uri_choice ~title:"Ambiguous input." + ~msg: + ("Ambiguous input \"" ^ id ^ + "\". Please, choose one interpetation:") + uris +;; + +let locate () = + let inputt = ((rendering_window ())#inputt : term_editor) in + let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in + try + match + GToolbox.input_string ~title:"Locate" "Enter an identifier to locate:" + with + None -> raise NoChoice + | Some input -> + let uri = locate_callback input in + inputt#set_term uri + with + e -> + output_html outputhtml + ("

" ^ Printexc.to_string e ^ "

") +;; + +let input_or_locate_uri ~title = + let uri = ref None in + let window = + GWindow.window + ~width:400 ~modal:true ~title ~border_width:2 () in + let vbox = GPack.vbox ~packing:window#add () in + let hbox1 = + GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in + let _ = + GMisc.label ~text:"Enter a valid URI:" ~packing:(hbox1#pack ~padding:5) () in + let manual_input = + GEdit.entry ~editable:true + ~packing:(hbox1#pack ~expand:true ~fill:true ~padding:5) () in + let checkb = + GButton.button ~label:"Check" + ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in + let _ = checkb#misc#set_sensitive false in + let hbox2 = + GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in + let _ = + GMisc.label ~text:"You can also enter an indentifier to locate:" + ~packing:(hbox2#pack ~padding:5) () in + let locate_input = + GEdit.entry ~editable:true + ~packing:(hbox2#pack ~expand:true ~fill:true ~padding:5) () in + let locateb = + GButton.button ~label:"Locate" + ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5) () in + let _ = locateb#misc#set_sensitive false in + let hbox3 = + GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in + let okb = + GButton.button ~label:"Ok" + ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in + let _ = okb#misc#set_sensitive false in + let cancelb = + GButton.button ~label:"Cancel" + ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () + in + ignore (window#connect#destroy GMain.Main.quit) ; + ignore + (cancelb#connect#clicked (function () -> uri := None ; window#destroy ())) ; + let check_callback () = + let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in + let uri = "cic:" ^ manual_input#text in + try + ignore (Getter.resolve (UriManager.uri_of_string uri)) ; + output_html outputhtml "

OK

" ; + true + with + Getter.Unresolved -> + output_html outputhtml + ("

URI " ^ uri ^ + " does not correspond to any object.

") ; + false + | UriManager.IllFormedUri _ -> + output_html outputhtml + ("

URI " ^ uri ^ " is not well-formed.

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

" ^ Printexc.to_string e ^ "

") ; + false + in + ignore + (okb#connect#clicked + (function () -> + if check_callback () then + begin + uri := Some manual_input#text ; + window#destroy () + end + )) ; + ignore (checkb#connect#clicked (function () -> ignore (check_callback ()))) ; + ignore + (manual_input#connect#changed + (fun _ -> + if manual_input#text = "" then + begin + checkb#misc#set_sensitive false ; + okb#misc#set_sensitive false + end + else + begin + checkb#misc#set_sensitive true ; + okb#misc#set_sensitive true + end)); + ignore + (locate_input#connect#changed + (fun _ -> locateb#misc#set_sensitive (locate_input#text <> ""))) ; + ignore + (locateb#connect#clicked + (function () -> + let id = locate_input#text in + manual_input#set_text (locate_callback id) ; + locate_input#delete_text 0 (String.length id) + )) ; + window#show () ; + GMain.Main.main () ; + match !uri with + None -> raise NoChoice + | Some uri -> UriManager.uri_of_string ("cic:" ^ uri) +;; + +let locate_one_id id = + let result = MQueryGenerator.locate id in + let uris = + List.map + (function uri,_ -> + wrong_xpointer_format_from_wrong_xpointer_format' uri + ) result in + let html= "

Locate Query: 

" ^ get_last_query result ^ "
" in + output_html (rendering_window ())#outputhtml html ; + let uris' = + match uris with + [] -> + [UriManager.string_of_uri + (input_or_locate_uri ~title:("URI matching \"" ^ id ^ "\" unknown."))] + | [uri] -> [uri] + | _ -> + interactive_user_uri_choice + ~selection_mode:`EXTENDED + ~ok:"Try every selection." + ~title:"Ambiguous input." + ~msg: + ("Ambiguous input \"" ^ id ^ + "\". Please, choose one or more interpretations:") + uris + in + List.map cic_textual_parser_uri_of_string uris' +;; + +exception ThereDoesNotExistAnyWellTypedInterpretationOfTheInput;; +exception AmbiguousInput;; + +let disambiguate_input context metasenv dom mk_metasenv_and_expr = + let known_ids,resolve_id = !id_to_uris in + let dom' = + let rec filter = + function + [] -> [] + | he::tl -> + if List.mem he known_ids then filter tl else he::(filter tl) + in + filter dom + in + (* for each id in dom' we get the list of uris associated to it *) + let list_of_uris = List.map locate_one_id dom' in + (* and now we compute the list of all possible assignments from id to uris *) + let resolve_ids = + let rec aux ids list_of_uris = + match ids,list_of_uris with + [],[] -> [resolve_id] + | id::idtl,uris::uristl -> + let resolves = aux idtl uristl in + List.concat + (List.map + (function uri -> + List.map + (function f -> + function id' -> if id = id' then Some uri else f id' + ) resolves + ) uris + ) + | _,_ -> assert false + in + aux dom' list_of_uris + in + let tests_no = List.length resolve_ids in + if tests_no > 1 then + output_html (outputhtml ()) + ("

Disambiguation phase started: " ^ + string_of_int (List.length resolve_ids) ^ " cases will be tried.") ; + (* now we select only the ones that generates well-typed terms *) + let resolve_ids' = + let rec filter = + function + [] -> [] + | resolve::tl -> + let metasenv',expr = mk_metasenv_and_expr resolve in + try +(*CSC: Bug here: we do not try to typecheck also the metasenv' *) + ignore + (CicTypeChecker.type_of_aux' metasenv context expr) ; + resolve::(filter tl) + with + _ -> filter tl + in + filter resolve_ids + in + let resolve_id' = + match resolve_ids' with + [] -> raise ThereDoesNotExistAnyWellTypedInterpretationOfTheInput + | [resolve_id] -> resolve_id + | _ -> + let choices = + List.map + (function resolve -> + List.map + (function id -> + id, + match resolve id with + None -> assert false + | Some uri -> + match uri with + CicTextualParser0.ConUri uri + | CicTextualParser0.VarUri uri -> + UriManager.string_of_uri uri + | CicTextualParser0.IndTyUri (uri,tyno) -> + UriManager.string_of_uri uri ^ "#xpointer(1/" ^ + string_of_int (tyno+1) ^ ")" + | CicTextualParser0.IndConUri (uri,tyno,consno) -> + UriManager.string_of_uri uri ^ "#xpointer(1/" ^ + string_of_int (tyno+1) ^ "/" ^ string_of_int consno ^ ")" + ) dom + ) resolve_ids' + in + let index = interactive_interpretation_choice choices in + List.nth resolve_ids' index + in + id_to_uris := known_ids @ dom', resolve_id' ; + mk_metasenv_and_expr resolve_id' +;; + +exception UriAlreadyInUse;; +exception NotAUriToAConstant;; + +let new_proof () = + let inputt = ((rendering_window ())#inputt : term_editor) in + let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in + let output = ((rendering_window ())#output : GMathView.math_view) in + let notebook = (rendering_window ())#notebook in + + let chosen = ref false in + let get_parsed = ref (function _ -> assert false) in + let get_uri = ref (function _ -> assert false) in + let non_empty_type = ref false in + let window = + GWindow.window + ~width:600 ~modal:true ~title:"New Proof or Definition" + ~border_width:2 () in + let vbox = GPack.vbox ~packing:window#add () in + let hbox = + GPack.hbox ~border_width:0 + ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in + let _ = + GMisc.label ~text:"Enter the URI for the new theorem or definition:" + ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in + let uri_entry = + GEdit.entry ~editable:true + ~packing:(hbox#pack ~expand:true ~fill:true ~padding:5) () in + let hbox1 = + GPack.hbox ~border_width:0 + ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in + let _ = + GMisc.label ~text:"Enter the theorem or definition type:" + ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in + let scrolled_window = + GBin.scrolled_window ~border_width:5 + ~packing:(vbox#pack ~expand:true ~padding:0) () in + (* the content of the scrolled_window is moved below (see comment) *) + let hbox = + GPack.hbox ~border_width:0 + ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in + let okb = + GButton.button ~label:"Ok" + ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in + let _ = okb#misc#set_sensitive false in + let cancelb = + GButton.button ~label:"Cancel" + ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in + (* moved here to have visibility of the ok button *) + let newinputt = + new term_editor ~width:400 ~height:100 ~packing:scrolled_window#add () + ~isnotempty_callback: + (function b -> + non_empty_type := b ; + okb#misc#set_sensitive (b && uri_entry#text <> "")) + in + let _ = + newinputt#set_term inputt#get_as_string ; + inputt#reset in + let _ = + uri_entry#connect#changed + (function () -> + okb#misc#set_sensitive (!non_empty_type && uri_entry#text <> "")) + in + ignore (window#connect#destroy GMain.Main.quit) ; + ignore (cancelb#connect#clicked window#destroy) ; + ignore + (okb#connect#clicked + (function () -> + chosen := true ; + try + let parsed = newinputt#get_term [] [] in + let uristr = "cic:" ^ uri_entry#text in + let uri = UriManager.uri_of_string uristr in + if String.sub uristr (String.length uristr - 4) 4 <> ".con" then + raise NotAUriToAConstant + else + begin + try + ignore (Getter.resolve uri) ; + raise UriAlreadyInUse + with + Getter.Unresolved -> + get_parsed := (function () -> parsed) ; + get_uri := (function () -> uri) ; + window#destroy () + end + with + e -> + output_html outputhtml + ("

" ^ Printexc.to_string e ^ "

") ; + )) ; + window#show () ; + GMain.Main.main () ; + if !chosen then + try + let dom,mk_metasenv_and_expr = !get_parsed () in + let metasenv,expr = + disambiguate_input [] [] dom mk_metasenv_and_expr + in + let _ = CicTypeChecker.type_of_aux' metasenv [] expr in + ProofEngine.proof := + Some (!get_uri (), (1,[],expr)::metasenv, Cic.Meta (1,[]), expr) ; + ProofEngine.goal := Some 1 ; + refresh_sequent notebook ; + refresh_proof output ; + !save_set_sensitive true ; + inputt#reset + 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 ^ "

") ; +;; + +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 +prerr_endline ("### " ^ CicPp.ppterm expr ^ " ==> " ^ CicPp.ppterm ty) ; + scratch_window#show () ; + scratch_window#mmlwidget#load_tree ~dom:mml + with + e -> + print_endline ("? " ^ CicPp.ppterm expr) ; + raise e +;; + +let check scratch_window () = + let inputt = ((rendering_window ())#inputt : term_editor) in + let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in + let metasenv = + match !ProofEngine.proof with + None -> [] + | Some (_,metasenv,_,_) -> metasenv + in + let context,names_context = + let context = + match !ProofEngine.goal with + None -> [] + | Some metano -> + let (_,canonical_context,_) = + List.find (function (m,_,_) -> m=metano) metasenv + in + canonical_context + in + context, + List.map + (function + Some (n,_) -> Some n + | None -> None + ) context + in + try + let dom,mk_metasenv_and_expr = inputt#get_term names_context metasenv in + let (metasenv',expr) = + disambiguate_input context metasenv dom mk_metasenv_and_expr + in + check_term_in_scratch scratch_window metasenv' context expr + with + e -> + output_html outputhtml + ("

" ^ Printexc.to_string e ^ "

") ; +;; + + +(***********************) +(* TACTICS *) +(***********************) + +let call_tactic tactic () = + let notebook = (rendering_window ())#notebook in + let output = ((rendering_window ())#output : GMathView.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 : GMathView.math_view) in + let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in + let inputt = ((rendering_window ())#inputt : 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 + let context = + List.map + (function + Some (n,_) -> Some n + | None -> None + ) canonical_context + in + try + let dom,mk_metasenv_and_expr = inputt#get_term context metasenv in + let (metasenv',expr) = + disambiguate_input canonical_context metasenv dom mk_metasenv_and_expr + 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 : GMathView.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_selection with + Some node -> + let xpath = + ((node : Gdome.element)#getAttributeNS + ~namespaceURI: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 proofw + 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 proofw ; + refresh_sequent notebook ; refresh_proof output | e -> output_html outputhtml @@ -464,16 +1711,16 @@ let call_tactic_with_goal_input tactic rendering_window () = ("

No term selected

") ;; -let call_tactic_with_input_and_goal_input tactic rendering_window () = +let call_tactic_with_input_and_goal_input tactic () = let module L = LogicalOperations in let module G = Gdome in - let proofw = (rendering_window#proofw : GMathView.math_view) in - let output = (rendering_window#output : GMathView.math_view) in - let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in - let inputt = (rendering_window#inputt : GEdit.text) in + let notebook = (rendering_window ())#notebook in + let output = ((rendering_window ())#output : GMathView.math_view) in + let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in + let inputt = ((rendering_window ())#inputt : term_editor) in let savedproof = !ProofEngine.proof in let savedgoal = !ProofEngine.goal in - match proofw#get_selection with + match notebook#proofw#get_selection with Some node -> let xpath = ((node : Gdome.element)#getAttributeNS @@ -487,52 +1734,38 @@ let call_tactic_with_input_and_goal_input tactic rendering_window () = match !current_goal_infos with Some (ids_to_terms, ids_to_father_ids,_) -> let id = xpath in - (* Let's parse the input *) - let inputlen = inputt#length in - let input = inputt#get_chars 0 inputlen ^ "\n" in - let lexbuf = Lexing.from_string input in - let curi = - match !ProofEngine.proof with + 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 (curi,_,_,_) -> curi - in - let metasenv = - match !ProofEngine.proof with - None -> assert false - | Some (_,metasenv,_,_) -> metasenv - in + | Some metano -> + let (_,canonical_context,_) = + List.find (function (m,_,_) -> m=metano) metasenv + in + canonical_context in let context = List.map (function Some (n,_) -> Some n - | None -> None) - (match !ProofEngine.goal with - None -> assert false - | Some metano -> - let (_,canonical_context,_) = - List.find (function (m,_,_) -> m=metano) metasenv - in - canonical_context - ) + | None -> None + ) canonical_context in - begin - try - while true do - match - CicTextualParserContext.main curi context - CicTextualLexer.token lexbuf - with - None -> () - | Some expr -> - tactic ~goal_input:(Hashtbl.find ids_to_terms id) - ~input:expr ; - refresh_sequent proofw ; - refresh_proof output - done - with - CicTextualParser0.Eof -> - inputt#delete_text 0 inputlen - end + let dom,mk_metasenv_and_expr = inputt#get_term context metasenv + in + let (metasenv',expr) = + disambiguate_input canonical_context metasenv dom + mk_metasenv_and_expr + 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 -> @@ -541,14 +1774,14 @@ let call_tactic_with_input_and_goal_input tactic rendering_window () = "sequent: " ^ Printexc.to_string e ^ "") ; ProofEngine.proof := savedproof ; ProofEngine.goal := savedgoal ; - refresh_sequent proofw + 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 proofw ; + refresh_sequent notebook ; refresh_proof output | e -> output_html outputhtml @@ -565,7 +1798,7 @@ 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 : GMathView.math_view) in - let outputhtml = (scratch_window#outputhtml : GHtml.xmhtml) in + let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in let savedproof = !ProofEngine.proof in let savedgoal = !ProofEngine.goal in match mmlwidget#get_selection with @@ -586,404 +1819,148 @@ let call_tactic_with_goal_input_in_scratch tactic scratch_window () = 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_tree ~dom:mml - | None -> assert false (* "ERROR: No current term!!!" *) - with - e -> - output_html outputhtml - ("

" ^ Printexc.to_string e ^ "

") - end - | None -> - output_html outputhtml - ("

No term selected

") -;; - -let call_tactic_with_hypothesis_input tactic rendering_window () = - let module L = LogicalOperations in - let module G = Gdome in - let proofw = (rendering_window#proofw : GMathView.math_view) in - let output = (rendering_window#output : GMathView.math_view) in - let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in - let savedproof = !ProofEngine.proof in - let savedgoal = !ProofEngine.goal in - match proofw#get_selection with - Some node -> - let xpath = - ((node : Gdome.element)#getAttributeNS - ~namespaceURI: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 rendering_window#proofw ; - refresh_proof rendering_window#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 proofw - | 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 proofw ; - refresh_proof output - | e -> - output_html outputhtml - ("

" ^ Printexc.to_string e ^ "

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

No term selected

") -;; - - -let intros rendering_window = call_tactic ProofEngine.intros rendering_window;; -let exact rendering_window = - call_tactic_with_input ProofEngine.exact rendering_window -;; -let apply rendering_window = - call_tactic_with_input ProofEngine.apply rendering_window -;; -let elimintrossimpl rendering_window = - call_tactic_with_input ProofEngine.elim_intros_simpl rendering_window -;; -let elimtype rendering_window = - call_tactic_with_input ProofEngine.elim_type rendering_window -;; -let whd rendering_window = - call_tactic_with_goal_input ProofEngine.whd rendering_window -;; -let reduce rendering_window = - call_tactic_with_goal_input ProofEngine.reduce rendering_window -;; -let simpl rendering_window = - call_tactic_with_goal_input ProofEngine.simpl rendering_window -;; -let fold rendering_window = - call_tactic_with_input ProofEngine.fold rendering_window -;; -let cut rendering_window = - call_tactic_with_input ProofEngine.cut rendering_window -;; -let change rendering_window = - call_tactic_with_input_and_goal_input ProofEngine.change rendering_window -;; -let letin rendering_window = - call_tactic_with_input ProofEngine.letin rendering_window -;; -let ring rendering_window = call_tactic ProofEngine.ring rendering_window;; -let clearbody rendering_window = - call_tactic_with_hypothesis_input ProofEngine.clearbody rendering_window -;; -let clear rendering_window = - call_tactic_with_hypothesis_input ProofEngine.clear rendering_window -;; - - -let whd_in_scratch scratch_window = - call_tactic_with_goal_input_in_scratch ProofEngine.whd_in_scratch - scratch_window -;; -let reduce_in_scratch scratch_window = - call_tactic_with_goal_input_in_scratch ProofEngine.reduce_in_scratch - scratch_window -;; -let simpl_in_scratch scratch_window = - call_tactic_with_goal_input_in_scratch ProofEngine.simpl_in_scratch - scratch_window -;; - - - -(**********************) -(* END OF TACTICS *) -(**********************) - -exception OpenConjecturesStillThere;; -exception WrongProof;; - -let qed rendering_window () = - match !ProofEngine.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.Definition (UriManager.name_of_uri uri,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 uri acic ids_to_inner_sorts ids_to_inner_types - in - (rendering_window#output : GMathView.math_view)#load_tree mml ; - current_cic_infos := - Some - (ids_to_terms,ids_to_father_ids,ids_to_conjectures, - ids_to_hypotheses) - end - else - raise WrongProof - | _ -> raise OpenConjecturesStillThere -;; - -(*???? -let dtdname = "http://www.cs.unibo.it/helm/dtd/cic.dtd";; -*) -(* let dtdname = "/home/zack/dati/HELM/V7/dtd/cic.dtd";; *) -let dtdname = "/public/helm-cvs/helm/dtd/cic.dtd";; - -let save rendering_window () = - let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in - match !ProofEngine.proof with - None -> assert false - | Some (uri, metasenv, bo, ty) -> - let currentproof = - Cic.CurrentProof (UriManager.name_of_uri uri,metasenv,bo,ty) - in - let (acurrentproof,_,_,ids_to_inner_sorts,_,_,_) = - Cic2acic.acic_object_of_cic_object currentproof - in - let xml = Cic2Xml.print_object uri ids_to_inner_sorts acurrentproof in - let xml' = - [< Xml.xml_cdata "\n" ; - Xml.xml_cdata - ("\n\n") ; - xml - >] - in - Xml.pp ~quiet:true xml' (Some prooffile) ; - output_html outputhtml - ("

Current proof saved to " ^ - prooffile ^ "

") -;; - -(* Used to typecheck the loaded proofs *) -let typecheck_loaded_proof metasenv bo ty = - let module T = CicTypeChecker in - (*CSC: bisogna controllare anche il metasenv!!! *) - ignore (T.type_of_aux' metasenv [] ty) ; - ignore (T.type_of_aux' metasenv [] bo) -;; - -let load rendering_window () = - let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in - let output = (rendering_window#output : GMathView.math_view) in - let proofw = (rendering_window#proofw : GMathView.math_view) in - try - let uri = UriManager.uri_of_string "cic:/dummy.con" in - match CicParser.obj_of_xml prooffile uri with - Cic.CurrentProof (_,metasenv,bo,ty) -> - typecheck_loaded_proof metasenv bo ty ; - ProofEngine.proof := - Some (uri, metasenv, bo, ty) ; - ProofEngine.goal := - (match metasenv with - [] -> None - | (metano,_,_)::_ -> Some metano - ) ; - refresh_proof output ; - refresh_sequent proofw ; - output_html outputhtml - ("

Current proof loaded from " ^ - prooffile ^ "

") - | _ -> assert false - 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 ^ "

") ; -;; - -let proveit rendering_window () = - let module L = LogicalOperations in - let module G = Gdome 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: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 rendering_window#output ; - refresh_sequent rendering_window#proofw - | 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!!!" *) + scratch_window#mmlwidget#load_tree ~dom:mml + | None -> assert false (* "ERROR: No current term!!!" *) + with + e -> + output_html outputhtml + ("

" ^ Printexc.to_string e ^ "

") + end + | None -> + output_html outputhtml + ("

No term selected

") ;; -let focus rendering_window () = +let call_tactic_with_hypothesis_input tactic () = let module L = LogicalOperations in let module G = Gdome 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: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 rendering_window#proofw - | 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 notebook = (rendering_window ())#notebook in + let output = ((rendering_window ())#output : GMathView.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_selection with + Some node -> + let xpath = + ((node : Gdome.element)#getAttributeNS + ~namespaceURI: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 + | None -> + output_html outputhtml + ("

No term selected

") ;; -exception NoPrevGoal;; -exception NoNextGoal;; -let prevgoal metasenv metano = - let rec aux = - function - [] -> assert false - | [(m,_,_)] -> raise NoPrevGoal - | (n,_,_)::(m,_,_)::_ when m=metano -> n - | _::tl -> aux tl - in - aux metasenv -;; +let intros = call_tactic ProofEngine.intros;; +let exact = call_tactic_with_input ProofEngine.exact;; +let apply = call_tactic_with_input ProofEngine.apply;; +let elimsimplintros = call_tactic_with_input ProofEngine.elim_simpl_intros;; +let elimtype = call_tactic_with_input ProofEngine.elim_type;; +let whd = call_tactic_with_goal_input ProofEngine.whd;; +let reduce = call_tactic_with_goal_input ProofEngine.reduce;; +let simpl = call_tactic_with_goal_input ProofEngine.simpl;; +let fold = call_tactic_with_input ProofEngine.fold;; +let cut = call_tactic_with_input ProofEngine.cut;; +let change = call_tactic_with_input_and_goal_input ProofEngine.change;; +let letin = call_tactic_with_input ProofEngine.letin;; +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 reflexivity = call_tactic ProofEngine.reflexivity;; +let symmetry = call_tactic ProofEngine.symmetry;; +let transitivity = call_tactic_with_input ProofEngine.transitivity;; +let left = call_tactic ProofEngine.left;; +let right = call_tactic ProofEngine.right;; +let assumption = call_tactic ProofEngine.assumption;; -let nextgoal metasenv metano = - let rec aux = - function - [] -> assert false - | [(m,_,_)] when m = metano -> raise NoNextGoal - | (m,_,_)::(n,_,_)::_ when m=metano -> n - | _::tl -> aux tl - in - aux metasenv +let whd_in_scratch scratch_window = + call_tactic_with_goal_input_in_scratch ProofEngine.whd_in_scratch + scratch_window +;; +let reduce_in_scratch scratch_window = + call_tactic_with_goal_input_in_scratch ProofEngine.reduce_in_scratch + scratch_window +;; +let simpl_in_scratch scratch_window = + call_tactic_with_goal_input_in_scratch ProofEngine.simpl_in_scratch + scratch_window ;; -let prev_or_next_goal select_goal rendering_window () = - let module L = LogicalOperations in - let module G = Gdome in - let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in - let metasenv = - match !ProofEngine.proof with - None -> assert false - | Some (_,metasenv,_,_) -> metasenv - in - let metano = - match !ProofEngine.goal with - None -> assert false - | Some m -> m - in - try - ProofEngine.goal := Some (select_goal metasenv metano) ; - refresh_sequent rendering_window#proofw - with - RefreshSequentException e -> - output_html outputhtml - ("

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

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

" ^ Printexc.to_string e ^ "

") + + +(**********************) +(* END OF TACTICS *) +(**********************) + + +let show () = + let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in + try + show_in_show_window (input_or_locate_uri ~title:"Show") + with + e -> + output_html outputhtml + ("

" ^ Printexc.to_string e ^ "

") ; ;; exception NotADefinition;; -let open_ rendering_window () = - let inputt = (rendering_window#inputt : GEdit.text) in - let oldinputt = (rendering_window#oldinputt : GEdit.text) in - let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in - let output = (rendering_window#output : GMathView.math_view) in - let proofw = (rendering_window#proofw : GMathView.math_view) in - let inputlen = inputt#length in - let input = inputt#get_chars 0 inputlen ^ "\n" in +let open_ () = + let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in + let output = ((rendering_window ())#output : GMathView.math_view) in + let notebook = (rendering_window ())#notebook in try - let uri = UriManager.uri_of_string ("cic:" ^ input) in + let uri = input_or_locate_uri ~title:"Open" in CicTypeChecker.typecheck uri ; let metasenv,bo,ty = - match CicEnvironment.get_cooked_obj uri 0 with - Cic.Definition (_,bo,ty,_) -> [],bo,ty - | Cic.CurrentProof (_,metasenv,bo,ty) -> metasenv,bo,ty - | Cic.Axiom _ + match CicEnvironment.get_cooked_obj uri with + Cic.Constant (_,Some bo,ty,_) -> [],bo,ty + | Cic.CurrentProof (_,metasenv,bo,ty,_) -> metasenv,bo,ty + | Cic.Constant _ | Cic.Variable _ | Cic.InductiveDefinition _ -> raise NotADefinition in ProofEngine.proof := Some (uri, metasenv, bo, ty) ; ProofEngine.goal := None ; - refresh_sequent proofw ; - refresh_proof output ; - inputt#delete_text 0 inputlen ; - ignore(oldinputt#insert_text input oldinputt#length) + refresh_sequent notebook ; + refresh_proof output with RefreshSequentException e -> output_html outputhtml @@ -998,142 +1975,99 @@ let open_ rendering_window () = ("

" ^ Printexc.to_string e ^ "

") ; ;; -let state rendering_window () = - let inputt = (rendering_window#inputt : GEdit.text) in - let oldinputt = (rendering_window#oldinputt : GEdit.text) in - let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in - let output = (rendering_window#output : GMathView.math_view) in - let proofw = (rendering_window#proofw : GMathView.math_view) in - let inputlen = inputt#length in - let input = inputt#get_chars 0 inputlen ^ "\n" in - (* Do something interesting *) - let lexbuf = Lexing.from_string input in - try - while true do - (* Execute the actions *) - match CicTextualParser.main CicTextualLexer.token lexbuf with - None -> () - | Some expr -> - let _ = CicTypeChecker.type_of_aux' [] [] expr in - ProofEngine.proof := - Some (UriManager.uri_of_string "cic:/dummy.con", - [1,[],expr], Cic.Meta (1,[]), expr) ; - ProofEngine.goal := Some 1 ; - refresh_sequent proofw ; - refresh_proof output ; - done - with - CicTextualParser0.Eof -> - inputt#delete_text 0 inputlen ; - ignore(oldinputt#insert_text input oldinputt#length) - | 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 ^ "

") ; -;; -let check rendering_window scratch_window () = - let inputt = (rendering_window#inputt : GEdit.text) in - let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in - let output = (rendering_window#output : GMathView.math_view) in - let proofw = (rendering_window#proofw : GMathView.math_view) in - let inputlen = inputt#length in - let input = inputt#get_chars 0 inputlen ^ "\n" in - let curi,metasenv = - match !ProofEngine.proof with - None -> UriManager.uri_of_string "cic:/dummy.con", [] - | Some (curi,metasenv,_,_) -> curi,metasenv - in - let context,names_context = - let context = - match !ProofEngine.goal with - None -> [] - | Some metano -> - let (_,canonical_context,_) = - List.find (function (m,_,_) -> m=metano) metasenv - in - canonical_context - in - context, - List.map - (function - Some (n,_) -> Some n - | None -> None - ) context - in - (* Do something interesting *) - let lexbuf = Lexing.from_string input in - try - while true do - (* Execute the actions *) - match - CicTextualParserContext.main curi names_context CicTextualLexer.token - lexbuf - with - None -> () - | Some expr -> - try - let ty = CicTypeChecker.type_of_aux' metasenv context expr in - let mml = mml_of_cic_term 111 (Cic.Cast (expr,ty)) in - scratch_window#show () ; - scratch_window#mmlwidget#load_tree ~dom:mml - with - e -> - print_endline ("? " ^ CicPp.ppterm expr) ; - raise e - done +let searchPattern () = + let inputt = ((rendering_window ())#inputt : term_editor) in + let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in + try + let rec get_level ?(last_invalid=false) () = + match + GToolbox.input_string + ~title:"Insert the strictness parameter for the query:" + ((if last_invalid then + "Invalid input (must be a non-negative natural number). Insert again " + else + "Insert " + ) ^ "the strictness parameter for the query:") with - CicTextualParser0.Eof -> () - | e -> - output_html outputhtml - ("

" ^ Printexc.to_string e ^ "

") ; -;; - -let locate rendering_window () = - let inputt = (rendering_window#inputt : GEdit.text) in - let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in - let inputlen = inputt#length in - let input = inputt#get_chars 0 inputlen in - output_html outputhtml ( - try - match Str.split (Str.regexp "[ \t]+") input with - | [] -> "" - | head :: tail -> - inputt#delete_text 0 inputlen; - MQueryGenerator.locate head - with - e -> "

" ^ Printexc.to_string e ^ "

" - ) -;; - -let backward rendering_window () = - let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in - let inputt = (rendering_window#inputt : GEdit.text) in - let inputlen = inputt#length in - let input = inputt#get_chars 0 inputlen in - let level = int_of_string input in + None -> raise NoChoice + | Some n -> + try + int_of_string n + with + _ -> get_level ~last_invalid:true () + in + let level = get_level () in let metasenv = match !ProofEngine.proof with None -> assert false | Some (_,metasenv,_,_) -> metasenv in - let result = - match !ProofEngine.goal with - | None -> "" - | Some metano -> - let (_, ey ,ty) = - List.find (function (m,_,_) -> m=metano) metasenv + match !ProofEngine.goal with + None -> () + | Some metano -> + let (_, ey ,ty) = List.find (function (m,_,_) -> m=metano) metasenv in + let result = MQueryGenerator.searchPattern metasenv ey ty level in + let uris = + List.map + (function uri,_ -> + wrong_xpointer_format_from_wrong_xpointer_format' uri + ) result in + let html = + "

Backward Query:

" ^ + "

Levels:

" ^ + MQueryLevels.string_of_levels + (MQueryLevels.levels_of_term metasenv ey ty) "
" ^ + " 
" ^ get_last_query result ^ "
" + in + output_html outputhtml html ; + let uris',exc = + let rec filter_out = + function + [] -> [],"" + | uri::tl -> + let tl',exc = filter_out tl in + try + if + ProofEngine.can_apply + (term_of_cic_textual_parser_uri + (cic_textual_parser_uri_of_string uri)) + then + uri::tl',exc + else + tl',exc + with + e -> + let exc' = + "

^ Exception raised trying to apply " ^ + uri ^ ": " ^ Printexc.to_string e ^ "

" ^ exc + in + tl',exc' + in + filter_out uris + in + let html' = + "

Objects that can actually be applied:

" ^ + String.concat "
" uris' ^ exc ^ + "

Number of false matches: " ^ + string_of_int (List.length uris - List.length uris') ^ "

" ^ + "

Number of good matches: " ^ + string_of_int (List.length uris') ^ "

" + in + output_html outputhtml html' ; + let uri' = + user_uri_choice ~title:"Ambiguous input." + ~msg: + "Many lemmas can be successfully applied. Please, choose one:" + uris' in - MQueryGenerator.backward metasenv ey ty level - in - output_html outputhtml result + inputt#set_term uri' ; + apply () + with + e -> + output_html outputhtml + ("

" ^ Printexc.to_string e ^ "

") +;; let choose_selection (mmlwidget : GMathView.math_view) (element : Gdome.element option) @@ -1162,12 +2096,20 @@ let choose_selection (* Stuff for the widget settings *) -let export_to_postscript (output : GMathView.math_view) () = - output#export_to_postscript ~filename:"output.ps" (); +let export_to_postscript (output : GMathView.math_view) = + let lastdir = ref (Unix.getcwd ()) in + function () -> + match + GToolbox.select_file ~title:"Export to PostScript" + ~dir:lastdir ~filename:"screenshot.ps" () + with + None -> () + | Some filename -> + output#export_to_postscript ~filename:filename (); ;; let activate_t1 (output : GMathView.math_view) button_set_anti_aliasing - button_set_kerning button_set_transparency button_export_to_postscript + button_set_kerning button_set_transparency export_to_postscript_menu_item button_t1 () = let is_set = button_t1#active in @@ -1178,14 +2120,14 @@ let activate_t1 (output : GMathView.math_view) button_set_anti_aliasing button_set_anti_aliasing#misc#set_sensitive true ; button_set_kerning#misc#set_sensitive true ; button_set_transparency#misc#set_sensitive true ; - button_export_to_postscript#misc#set_sensitive true ; + export_to_postscript_menu_item#misc#set_sensitive true ; end else begin button_set_anti_aliasing#misc#set_sensitive false ; button_set_kerning#misc#set_sensitive false ; button_set_transparency#misc#set_sensitive false ; - button_export_to_postscript#misc#set_sensitive false ; + export_to_postscript_menu_item#misc#set_sensitive false ; end ;; @@ -1210,7 +2152,7 @@ let set_log_verbosity output log_verbosity_spinb () = ;; class settings_window (output : GMathView.math_view) sw - button_export_to_postscript selection_changed_callback + export_to_postscript_menu_item selection_changed_callback = let settings_window = GWindow.window ~title:"GtkMathView settings" () in let vbox = @@ -1267,7 +2209,7 @@ object(self) (* Signals connection *) ignore(button_t1#connect#clicked (activate_t1 output button_set_anti_aliasing button_set_kerning - button_set_transparency button_export_to_postscript button_t1)) ; + button_set_transparency export_to_postscript_menu_item button_t1)) ; ignore(font_size_spinb#connect#changed (changefont output font_size_spinb)) ; ignore(button_set_anti_aliasing#connect#toggled (set_anti_aliasing output button_set_anti_aliasing)); @@ -1282,7 +2224,7 @@ end;; (* Scratch window *) -class scratch_window outputhtml = +class scratch_window = let window = GWindow.window ~title:"MathML viewer" ~border_width:2 () in let vbox = @@ -1305,7 +2247,6 @@ class scratch_window outputhtml = GMathView.math_view ~packing:(scrolled_window#add) ~width:400 ~height:280 () in object(self) - method outputhtml = outputhtml method mmlwidget = mmlwidget method show () = window#misc#hide () ; window#show () initializer @@ -1316,188 +2257,361 @@ object(self) ignore(simplb#connect#clicked (simpl_in_scratch self)) end;; +class page () = + let vbox1 = GPack.vbox () in +object(self) + val mutable proofw_ref = None + val mutable compute_ref = None + method proofw = + Lazy.force self#compute ; + match proofw_ref with + None -> assert false + | Some proofw -> proofw + method content = vbox1 + method compute = + match compute_ref with + None -> assert false + | Some compute -> compute + initializer + compute_ref <- + Some (lazy ( + let scrolled_window1 = + GBin.scrolled_window ~border_width:10 + ~packing:(vbox1#pack ~expand:true ~padding:5) () in + let proofw = + GMathView.math_view ~width:400 ~height:275 + ~packing:(scrolled_window1#add) () in + let _ = proofw_ref <- Some proofw in + let hbox3 = + GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in + let exactb = + GButton.button ~label:"Exact" + ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in + let introsb = + GButton.button ~label:"Intros" + ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in + let applyb = + GButton.button ~label:"Apply" + ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in + let elimsimplintrosb = + GButton.button ~label:"ElimSimplIntros" + ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in + let elimtypeb = + GButton.button ~label:"ElimType" + ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in + let whdb = + GButton.button ~label:"Whd" + ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in + let reduceb = + GButton.button ~label:"Reduce" + ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in + let simplb = + GButton.button ~label:"Simpl" + ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in + let foldb = + GButton.button ~label:"Fold" + ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in + let cutb = + GButton.button ~label:"Cut" + ~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 changeb = + GButton.button ~label:"Change" + ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in + let letinb = + GButton.button ~label:"Let ... In" + ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in + let ringb = + GButton.button ~label:"Ring" + ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in + let clearbodyb = + GButton.button ~label:"ClearBody" + ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in + let clearb = + GButton.button ~label:"Clear" + ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in + let fourierb = + GButton.button ~label:"Fourier" + ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in + let rewritesimplb = + GButton.button ~label:"RewriteSimpl ->" + ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in + let reflexivityb = + GButton.button ~label:"Reflexivity" + ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in + let hbox5 = + GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in + let symmetryb = + GButton.button ~label:"Symmetry" + ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in + let transitivityb = + GButton.button ~label:"Transitivity" + ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in + let leftb = + GButton.button ~label:"Left" + ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in + let rightb = + GButton.button ~label:"Right" + ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in + let assumptionb = + GButton.button ~label:"Assumption" + ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in + let searchpatternb = + GButton.button ~label:"SearchPattern_Apply" + ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in + ignore(exactb#connect#clicked exact) ; + ignore(applyb#connect#clicked apply) ; + ignore(elimsimplintrosb#connect#clicked elimsimplintros) ; + ignore(elimtypeb#connect#clicked elimtype) ; + ignore(whdb#connect#clicked whd) ; + ignore(reduceb#connect#clicked reduce) ; + ignore(simplb#connect#clicked simpl) ; + ignore(foldb#connect#clicked fold) ; + ignore(cutb#connect#clicked cut) ; + ignore(changeb#connect#clicked change) ; + ignore(letinb#connect#clicked letin) ; + ignore(ringb#connect#clicked ring) ; + ignore(clearbodyb#connect#clicked clearbody) ; + ignore(clearb#connect#clicked clear) ; + ignore(fourierb#connect#clicked fourier) ; + ignore(rewritesimplb#connect#clicked rewritesimpl) ; + ignore(reflexivityb#connect#clicked reflexivity) ; + ignore(symmetryb#connect#clicked symmetry) ; + ignore(transitivityb#connect#clicked transitivity) ; + ignore(leftb#connect#clicked left) ; + ignore(rightb#connect#clicked right) ; + ignore(assumptionb#connect#clicked assumption) ; + ignore(introsb#connect#clicked intros) ; + ignore(searchpatternb#connect#clicked searchPattern) ; + ignore(proofw#connect#selection_changed (choose_selection proofw)) ; + )) +end +;; + +class empty_page = + let vbox1 = GPack.vbox () in + let scrolled_window1 = + GBin.scrolled_window ~border_width:10 + ~packing:(vbox1#pack ~expand:true ~padding:5) () in + let proofw = + GMathView.math_view ~width:400 ~height:275 + ~packing:(scrolled_window1#add) () in +object(self) + method proofw = (assert false : GMathView.math_view) + method content = vbox1 + method compute = (assert false : unit) +end +;; + +let empty_page = new empty_page;; + +class notebook = +object(self) + val notebook = GPack.notebook () + val pages = ref [] + val mutable skip_switch_page_event = false + val mutable empty = true + method notebook = notebook + method add_page n = + let new_page = new page () in + empty <- false ; + pages := !pages @ [n,lazy (setgoal n),new_page] ; + notebook#append_page + ~tab_label:((GMisc.label ~text:("?" ^ string_of_int n) ())#coerce) + new_page#content#coerce + method remove_all_pages ~skip_switch_page_event:skip = + if empty then + notebook#remove_page 0 (* let's remove the empty page *) + else + List.iter (function _ -> notebook#remove_page 0) !pages ; + pages := [] ; + skip_switch_page_event <- skip + method set_current_page ~may_skip_switch_page_event n = + let (_,_,page) = List.find (function (m,_,_) -> m=n) !pages in + let new_page = notebook#page_num page#content#coerce in + if may_skip_switch_page_event && new_page <> notebook#current_page then + skip_switch_page_event <- true ; + notebook#goto_page new_page + method set_empty_page = + empty <- true ; + pages := [] ; + notebook#append_page + ~tab_label:((GMisc.label ~text:"No proof in progress" ())#coerce) + empty_page#content#coerce + method proofw = + let (_,_,page) = List.nth !pages notebook#current_page in + page#proofw + initializer + ignore + (notebook#connect#switch_page + (function i -> + let skip = skip_switch_page_event in + skip_switch_page_event <- false ; + if not skip then + try + let (metano,setgoal,page) = List.nth !pages i in + ProofEngine.goal := Some metano ; + Lazy.force (page#compute) ; + Lazy.force setgoal + with _ -> () + )) +end +;; + (* Main window *) -class rendering_window output proofw (label : GMisc.label) = +class rendering_window output (notebook : notebook) = + let scratch_window = new scratch_window in let window = - GWindow.window ~title:"MathML viewer" ~border_width:2 () in + GWindow.window ~title:"MathML viewer" ~border_width:0 + ~allow_shrink:false () in + let vbox_for_menu = GPack.vbox ~packing:window#add () in + (* menus *) + let handle_box = GBin.handle_box ~border_width:2 + ~packing:(vbox_for_menu#pack ~padding:0) () in + let menubar = GMenu.menu_bar ~packing:handle_box#add () in + let factory0 = new GMenu.factory menubar in + let accel_group = factory0#accel_group in + (* file menu *) + let file_menu = factory0#add_submenu "File" in + let factory1 = new GMenu.factory file_menu ~accel_group in + let export_to_postscript_menu_item = + begin + let _ = + factory1#add_item "New Proof or Definition..." ~key:GdkKeysyms._N + ~callback:new_proof + in + let reopen_menu_item = + factory1#add_item "Reopen a Finished Proof..." ~key:GdkKeysyms._R + ~callback:open_ + in + let qed_menu_item = + factory1#add_item "Qed" ~key:GdkKeysyms._E ~callback:qed in + ignore (factory1#add_separator ()) ; + ignore + (factory1#add_item "Load Unfinished Proof..." ~key:GdkKeysyms._L + ~callback:load) ; + let save_menu_item = + factory1#add_item "Save Unfinished Proof" ~key:GdkKeysyms._S ~callback:save + in + ignore + (save_set_sensitive := function b -> save_menu_item#misc#set_sensitive b); + ignore (!save_set_sensitive false); + ignore (qed_set_sensitive:=function b -> qed_menu_item#misc#set_sensitive b); + ignore (!qed_set_sensitive false); + ignore (factory1#add_separator ()) ; + let export_to_postscript_menu_item = + factory1#add_item "Export to PostScript..." + ~callback:(export_to_postscript output) in + ignore (factory1#add_separator ()) ; + ignore + (factory1#add_item "Exit" ~key:GdkKeysyms._Q ~callback:GMain.Main.quit) ; + export_to_postscript_menu_item + end in + (* edit menu *) + let edit_menu = factory0#add_submenu "Edit Current Proof" in + let factory2 = new GMenu.factory edit_menu ~accel_group in + let focus_and_proveit_set_sensitive = ref (function _ -> assert false) in + let proveit_menu_item = + factory2#add_item "Prove It" ~key:GdkKeysyms._I + ~callback:(function () -> proveit ();!focus_and_proveit_set_sensitive false) + in + let focus_menu_item = + factory2#add_item "Focus" ~key:GdkKeysyms._F + ~callback:(function () -> focus () ; !focus_and_proveit_set_sensitive false) + in + let _ = + focus_and_proveit_set_sensitive := + function b -> + proveit_menu_item#misc#set_sensitive b ; + focus_menu_item#misc#set_sensitive b + in + let _ = !focus_and_proveit_set_sensitive false in + (* edit term menu *) + let edit_term_menu = factory0#add_submenu "Edit Term" in + let factory5 = new GMenu.factory edit_term_menu ~accel_group in + let check_menu_item = + factory5#add_item "Check Term" ~key:GdkKeysyms._C + ~callback:(check scratch_window) in + let _ = check_menu_item#misc#set_sensitive false in + (* search menu *) + let settings_menu = factory0#add_submenu "Search" in + let factory4 = new GMenu.factory settings_menu ~accel_group in + let _ = + factory4#add_item "Locate..." ~key:GdkKeysyms._T + ~callback:locate in + let show_menu_item = + factory4#add_item "Show..." ~key:GdkKeysyms._H ~callback:show + in + (* settings menu *) + let settings_menu = factory0#add_submenu "Settings" in + let factory3 = new GMenu.factory settings_menu ~accel_group in + let _ = + factory3#add_item "Edit Aliases" ~key:GdkKeysyms._A + ~callback:edit_aliases in + let _ = factory3#add_separator () in + let _ = + factory3#add_item "MathML Widget Preferences..." ~key:GdkKeysyms._P + ~callback:(function _ -> (settings_window ())#show ()) in + (* accel group *) + let _ = window#add_accel_group accel_group in + (* end of menus *) let hbox0 = - GPack.hbox ~packing:window#add () in + GPack.hbox + ~packing:(vbox_for_menu#pack ~expand:true ~fill:true ~padding:5) () in let vbox = - GPack.vbox ~packing:(hbox0#pack ~expand:false ~fill:false ~padding:5) () in - let _ = vbox#pack ~expand:false ~fill:false ~padding:5 label#coerce in + GPack.vbox ~packing:(hbox0#pack ~expand:true ~fill:true ~padding:5) () in let scrolled_window0 = GBin.scrolled_window ~border_width:10 ~packing:(vbox#pack ~expand:true ~padding:5) () in let _ = scrolled_window0#add output#coerce in - let hbox1 = - GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in - let settingsb = - GButton.button ~label:"Settings" - ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in - let button_export_to_postscript = - GButton.button ~label:"export_to_postscript" - ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in - let qedb = - GButton.button ~label:"Qed" - ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in - let saveb = - GButton.button ~label:"Save" - ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in - let loadb = - GButton.button ~label:"Load" - ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in - let closeb = - GButton.button ~label:"Close" - ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in - let hbox2 = - GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in - let proveitb = - GButton.button ~label:"Prove It" - ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5) () in - let focusb = - GButton.button ~label:"Focus" - ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5) () in - let prevgoalb = - GButton.button ~label:"<" - ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5) () in - let nextgoalb = - GButton.button ~label:">" - ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5) () in - let oldinputt = GEdit.text ~editable:false ~width:400 ~height:180 - ~packing:(vbox#pack ~padding:5) () in - let hbox4 = - GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in - let stateb = - GButton.button ~label:"State" - ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in - let openb = - GButton.button ~label:"Open" - ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in - let checkb = - GButton.button ~label:"Check" - ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in - let locateb = - GButton.button ~label:"Locate" - ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in - let backwardb = - GButton.button ~label:"Backward" - ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in - let inputt = GEdit.text ~editable:true ~width:400 ~height: 100 - ~packing:(vbox#pack ~padding:5) () in - let vbox1 = - GPack.vbox ~packing:(hbox0#pack ~expand:false ~fill:false ~padding:5) () in + let frame = + GBin.frame ~label:"Insert Term" + ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in let scrolled_window1 = - GBin.scrolled_window ~border_width:10 - ~packing:(vbox1#pack ~expand:true ~padding:5) () in - let _ = scrolled_window1#add proofw#coerce in - let hbox3 = - GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in - let exactb = - GButton.button ~label:"Exact" - ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in - let introsb = - GButton.button ~label:"Intros" - ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in - let applyb = - GButton.button ~label:"Apply" - ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in - let elimintrossimplb = - GButton.button ~label:"ElimIntrosSimpl" - ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in - let elimtypeb = - GButton.button ~label:"ElimType" - ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in - let whdb = - GButton.button ~label:"Whd" - ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in - let reduceb = - GButton.button ~label:"Reduce" - ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in - let simplb = - GButton.button ~label:"Simpl" - ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in - let foldb = - GButton.button ~label:"Fold" - ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in - let cutb = - GButton.button ~label:"Cut" - ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in - let changeb = - GButton.button ~label:"Change" - ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in - let letinb = - GButton.button ~label:"Let ... In" - ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in - let ringb = - GButton.button ~label:"Ring" - ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in - let hbox4 = - GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in - let clearbodyb = - GButton.button ~label:"ClearBody" - ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in - let clearb = - GButton.button ~label:"Clear" - ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in - let dumpb = - GButton.button ~label:"Dump" - ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in + GBin.scrolled_window ~border_width:5 + ~packing:frame#add () in + let inputt = + new term_editor ~width:400 ~height:100 ~packing:scrolled_window1#add () + ~isnotempty_callback:check_menu_item#misc#set_sensitive in + let vboxl = + GPack.vbox ~packing:(hbox0#pack ~expand:true ~fill:true ~padding:5) () in + let _ = + vboxl#pack ~expand:true ~fill:true ~padding:5 notebook#notebook#coerce in + let frame = + GBin.frame ~shadow_type:`IN ~packing:(vboxl#pack ~expand:true ~padding:5) () + in let outputhtml = GHtml.xmhtml ~source:"" - ~width:400 ~height: 200 - ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) + ~width:400 ~height: 100 + ~border_width:20 + ~packing:frame#add ~show:true () in - let scratch_window = new scratch_window outputhtml in -object(self) +object method outputhtml = outputhtml - method oldinputt = oldinputt method inputt = inputt method output = (output : GMathView.math_view) - method proofw = (proofw : GMathView.math_view) + method notebook = notebook method show = window#show initializer - button_export_to_postscript#misc#set_sensitive false ; + notebook#set_empty_page ; + export_to_postscript_menu_item#misc#set_sensitive false ; + check_term := (check_term_in_scratch scratch_window) ; (* signal handlers here *) ignore(output#connect#selection_changed - (function elem -> proofw#unload ; choose_selection output elem)) ; - ignore(proofw#connect#selection_changed (choose_selection proofw)) ; - ignore(closeb#connect#clicked (fun _ -> GMain.Main.quit ())) ; + (function elem -> + choose_selection output elem ; + !focus_and_proveit_set_sensitive true + )) ; + ignore (output#connect#clicked (show_in_show_window_callback output)) ; let settings_window = new settings_window output scrolled_window0 - button_export_to_postscript (choose_selection output) in - ignore(settingsb#connect#clicked settings_window#show) ; - ignore(button_export_to_postscript#connect#clicked (export_to_postscript output)) ; - ignore(qedb#connect#clicked (qed self)) ; - ignore(saveb#connect#clicked (save self)) ; - ignore(loadb#connect#clicked (load self)) ; - ignore(proveitb#connect#clicked (proveit self)) ; - ignore(focusb#connect#clicked (focus self)) ; - ignore(prevgoalb#connect#clicked (prev_or_next_goal prevgoal self)) ; - ignore(nextgoalb#connect#clicked (prev_or_next_goal nextgoal self)) ; + 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 )) ; - ignore(stateb#connect#clicked (state self)) ; - ignore(openb#connect#clicked (open_ self)) ; - ignore(checkb#connect#clicked (check self scratch_window)) ; - ignore(locateb#connect#clicked (locate self)) ; - ignore(backwardb#connect#clicked (backward self)) ; - ignore(exactb#connect#clicked (exact self)) ; - ignore(applyb#connect#clicked (apply self)) ; - ignore(elimintrossimplb#connect#clicked (elimintrossimpl self)) ; - ignore(elimtypeb#connect#clicked (elimtype self)) ; - ignore(whdb#connect#clicked (whd self)) ; - ignore(reduceb#connect#clicked (reduce self)) ; - ignore(simplb#connect#clicked (simpl self)) ; - ignore(foldb#connect#clicked (fold self)) ; - ignore(cutb#connect#clicked (cut self)) ; - ignore(changeb#connect#clicked (change self)) ; - ignore(letinb#connect#clicked (letin self)) ; - ignore(ringb#connect#clicked (ring self)) ; - ignore(clearbodyb#connect#clicked (clearbody self)) ; - ignore(clearb#connect#clicked (clear self)) ; - ignore(dumpb#connect#clicked dumpsequent); - ignore(introsb#connect#clicked (intros self)) ; Logger.log_callback := (Logger.log_to_html ~print_and_flush:(output_html outputhtml)) end;; @@ -1506,22 +2620,23 @@ end;; let initialize_everything () = let module U = Unix in - let output = GMathView.math_view ~width:400 ~height:280 () - and proofw = GMathView.math_view ~width:400 ~height:275 () - and label = GMisc.label ~text:"gTopLevel" () in - let rendering_window = - new rendering_window output proofw label - in - rendering_window#show () ; - GMain.Main.main () + let output = GMathView.math_view ~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 () ;; let _ = - CicCooking.init () ; - if !usedb then MQueryGenerator.init () ; + if !usedb then + begin + Mqint.set_database Mqint.postgres_db ; + (* Mqint.init "dbname=helm_mowgli" ; *) + Mqint.init "host=mowgli.cs.unibo.it dbname=helm_mowgli user=helm" ; + end ; ignore (GtkMain.Main.init ()) ; initialize_everything () ; - if !usedb then MQueryGenerator.close (); - MQueryGenerator.close () + if !usedb then Mqint.close (); ;; -