X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FgTopLevel.ml;h=eeda38e492d4a49bc0d93c7dba9c6add00897f3d;hb=d1d5f6ee41209f05c072ba20e3cd50bc774ebff4;hp=7c01b4d75879b95771bbeea27b51278cdf0ad07d;hpb=2329c7fd13fb6c88f9f82ccad6b25a67c9ce7acf;p=helm.git diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml index 7c01b4d75..eeda38e49 100644 --- a/helm/gTopLevel/gTopLevel.ml +++ b/helm/gTopLevel/gTopLevel.ml @@ -51,8 +51,6 @@ let htmlfooter = let htmlheader_and_content = ref htmlheader;; -let filename4uwobo = "/public/sacerdot/prova.xml";; - let current_cic_infos = ref None;; @@ -80,12 +78,15 @@ let c1 = parseStyle "rootcontent.xsl";; let g = parseStyle "genmmlid.xsl";; let c2 = parseStyle "annotatedpres.xsl";; + +let getterURL = Configuration.getter_url;; +let processorURL = Configuration.processor_url;; (* let processorURL = "http://phd.cs.unibo.it:8080/helm/servelt/uwobo/";; let getterURL = "http://phd.cs.unibo.it:8081/";; -*) let processorURL = "http://localhost:8080/helm/servelt/uwobo/";; let getterURL = "http://localhost:8081/";; +*) let mml_styles = [d_c ; c1 ; g ; c2 ; l];; let mml_args = @@ -140,59 +141,142 @@ let applyStylesheets input styles args = input styles ;; -let mml_of_cic acic = -prerr_endline "BBB CREAZIONE" ; +let mml_of_cic_object annobj ids_to_inner_sorts = let xml = - Cic2Xml.print_term (UriManager.uri_of_string "cic:/dummy.con") acic + Cic2Xml.print_object + (UriManager.uri_of_string "cic:/dummy.con") ids_to_inner_sorts annobj in - Xml.pp ~quiet:true xml (Some filename4uwobo) ; -prerr_endline "BBB PARSING" ; - let input = domImpl#createDocumentFromURI ~uri:filename4uwobo () in -prerr_endline "BBB STYLESHEETS" ; + let input = + Xml2Gdome.document_of_xml domImpl xml + in let output = applyStylesheets input mml_styles mml_args in -prerr_endline "BBB RESA" ; -ignore(domImpl#saveDocumentToFile ~doc:output ~name:"/tmp/xxxyyyzzz" ()) ; - output + output ;; (* CALLBACKS *) +let refresh_proof (output : GMathView.math_view) = + let currentproof = + match !ProofEngine.proof with + None -> assert false + | Some (metasenv,bo,ty) -> Cic.CurrentProof ("unnamed", metasenv, bo, ty) + in + let (acic, ids_to_terms, ids_to_father_ids, ids_to_inner_sorts) = + Cic2acic.acic_object_of_cic_object currentproof + in + let mml = mml_of_cic_object acic ids_to_inner_sorts in + output#load_tree mml ; + current_cic_infos := Some (ids_to_terms,ids_to_father_ids) +;; + +let refresh_sequent (proofw : GMathView.math_view) = + let metasenv = + match !ProofEngine.proof with + None -> assert false + | Some (metasenv,_,_) -> metasenv + in + let currentsequent = + match !ProofEngine.goal with + None -> assert false + | Some (_,sequent) -> sequent + in + let sequent_gdome = 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 + in + proofw#load_tree ~dom:sequent_mml +(* +ignore(domImpl#saveDocumentToFile ~doc:sequent_doc + ~name:"/public/sacerdot/guruguru1" ~indent:true ()) ; +ignore(domImpl#saveDocumentToFile ~doc:sequent_mml + ~name:"/public/sacerdot/guruguru2" ~indent:true ()) +*) +;; + let exact rendering_window () = + let proofw = (rendering_window#proofw : GMathView.math_view) in + let output = (rendering_window#output : GMathView.math_view) in let inputt = (rendering_window#inputt : GEdit.text) 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 context = + List.map + (function (_,n,_) -> n) + (match !ProofEngine.goal with + None -> assert false + | Some (_,(ctx,_)) -> ctx + ) + in try while true do (* Execute the actions *) - match CicTextualParser.main CicTextualLexer.token lexbuf with + match + CicTextualParserContext.main context CicTextualLexer.token lexbuf + with None -> () | Some expr -> try -(*??? Ma servira' da qualche parte! - let ty = CicTypeChecker.type_of_aux' [] expr in -*) - let (acic, ids_to_terms, ids_to_father_ids) = - Cic2acic.acic_of_cic expr - in -(*CSC: chiamare la vera tattica exact qui! *) - () + ProofEngine.exact expr ; + proofw#unload ; + refresh_proof output with e -> - print_endline ("? " ^ CicPp.ppterm expr) ; + print_endline ("? " ^ CicPp.ppterm expr) ; flush stdout ; raise e done with CicTextualParser0.Eof -> inputt#delete_text 0 inputlen -(*CSC: fare qualcosa di utile *) | e -> print_endline ("Error: " ^ Printexc.to_string e) ; flush stdout ;; +let intros rendering_window () = + let proofw = (rendering_window#proofw : GMathView.math_view) in + let output = (rendering_window#output : GMathView.math_view) in + begin + try + ProofEngine.intros () ; + with + e -> + print_endline "? Intros " ; + raise e + end ; + refresh_sequent proofw ; + refresh_proof output +;; + +exception OpenConjecturesStillThere;; +exception WrongProof;; + +let save rendering_window () = + match !ProofEngine.proof with + None -> assert false + | Some ([],bo,ty) -> + if CicReduction.are_convertible (CicTypeChecker.type_of_aux' [] [] bo) ty then + begin + (*CSC: Wrong: [] is just plainly wrong *) + let proof = Cic.Definition ("unnamed",bo,ty,[]) in + let (acic, ids_to_terms, ids_to_father_ids, ids_to_inner_sorts) = + Cic2acic.acic_object_of_cic_object proof + in + let mml = mml_of_cic_object acic ids_to_inner_sorts in + (rendering_window#output : GMathView.math_view)#load_tree mml ; + current_cic_infos := Some (ids_to_terms,ids_to_father_ids) + end + else + raise WrongProof + | _ -> raise OpenConjecturesStillThere +;; + let proveit rendering_window () = + let module L = LogicalOperations in let module G = Gdome in match rendering_window#output#get_selection with Some node -> @@ -207,26 +291,16 @@ let proveit rendering_window () = if xpath = "" then assert false (* "ERROR: No xref found!!!" *) else begin - match !current_cic_infos with - Some (ids_to_terms, ids_to_father_ids) -> - let id = xpath in - let sequent = - LogicalOperations.to_sequent id ids_to_terms ids_to_father_ids - in - SequentPp.TextualPp.print_sequent sequent ; - let sequent_gdome = SequentPp.XmlPp.print_sequent sequent in - let sequent_doc = - Xml2Gdome.document_of_xml domImpl sequent_gdome - in - let sequent_mml = - applyStylesheets sequent_doc sequent_styles sequent_args - in - rendering_window#proofw#load_tree ~dom:sequent_mml ; -ignore(domImpl#saveDocumentToFile ~doc:sequent_doc - ~name:"/public/sacerdot/guruguru1" ~indent:true ()) ; -ignore(domImpl#saveDocumentToFile ~doc:sequent_mml - ~name:"/public/sacerdot/guruguru2" ~indent:true ()) - | None -> assert false (* "ERROR: No current term!!!" *) + try + match !current_cic_infos with + Some (ids_to_terms, ids_to_father_ids) -> + let id = xpath in + if L.to_sequent id ids_to_terms ids_to_father_ids then + refresh_proof rendering_window#output ; + refresh_sequent rendering_window#proofw + | None -> assert false (* "ERROR: No current term!!!" *) + with + e -> print_endline ("Error: " ^ Printexc.to_string e) ; flush stdout end | None -> assert false (* "ERROR: No selection!!!" *) ;; @@ -236,7 +310,7 @@ let output_html outputhtml msg = outputhtml#source (!htmlheader_and_content ^ htmlfooter) ;; -let execute rendering_window () = +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 @@ -253,20 +327,11 @@ let execute rendering_window () = None -> () | Some expr -> try - let ty = CicTypeChecker.type_of_aux' [] expr in - let whd = CicReduction.whd expr in - - let (acic, ids_to_terms, ids_to_father_ids) = - Cic2acic.acic_of_cic expr - in - let mml = mml_of_cic acic in - output#load_tree mml ; -prerr_endline "BBB FINE RESA" ; - current_cic_infos := Some (ids_to_terms,ids_to_father_ids) ; -print_endline ("? " ^ CicPp.ppterm expr) ; -print_endline (">> " ^ CicPp.ppterm whd) ; -print_endline (": " ^ CicPp.ppterm ty) ; -flush stdout ; + let _ = CicTypeChecker.type_of_aux' [] [] expr in + ProofEngine.proof := Some ([1,expr], Cic.Meta 1, expr) ; + ProofEngine.goal := Some (1,([],expr)) ; + refresh_sequent proofw ; + refresh_proof output ; with e -> print_endline ("? " ^ CicPp.ppterm expr) ; @@ -447,6 +512,9 @@ class rendering_window output proofw (label : GMisc.label) = let button_export_to_postscript = GButton.button ~label:"export_to_postscript" ~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 closeb = GButton.button ~label:"Close" ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in @@ -457,8 +525,8 @@ class rendering_window output proofw (label : GMisc.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 executeb = - GButton.button ~label:"Execute" + let stateb = + GButton.button ~label:"State" ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in let inputt = GEdit.text ~editable:true ~width:400 ~height: 100 ~packing:(vbox#pack ~padding:5) () in @@ -473,6 +541,9 @@ class rendering_window output proofw (label : GMisc.label) = 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 outputhtml = GHtml.xmhtml ~source:"" @@ -498,10 +569,12 @@ object(self) 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(saveb#connect#clicked (save self)) ; ignore(proveitb#connect#clicked (proveit self)) ; ignore(window#event#connect#delete (fun _ -> GMain.Main.quit () ; true )) ; - ignore(executeb#connect#clicked (execute self)) ; + ignore(stateb#connect#clicked (state self)) ; ignore(exactb#connect#clicked (exact self)) ; + ignore(introsb#connect#clicked (intros self)) ; Logger.log_callback := (Logger.log_to_html ~print_and_flush:(output_html outputhtml)) end;;