X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FgTopLevel.ml;h=83d959ca38f77f4ed8b76ca31a24611a50971eba;hb=89262281b6e83bd2321150f81f1a0583645eb0c8;hp=d052040c5f8177502ac4e2a4c1cee1cb879cf3ea;hpb=b2b968e27508993b1716810c2c27ff532e284742;p=helm.git diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml index d052040c5..83d959ca3 100644 --- a/helm/gTopLevel/gTopLevel.ml +++ b/helm/gTopLevel/gTopLevel.ml @@ -1,4 +1,4 @@ -(* Copyright (C) 2000, HELM Team. +(* Copyright (C) 2000-2002, HELM Team. * * This file is part of HELM, an Hypertextual, Electronic * Library of Mathematics, developed at the Computer Science @@ -33,6 +33,18 @@ (* *) (******************************************************************************) + +(* 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";; @@ -47,6 +59,16 @@ let htmlfooter = "" ;; +(* +let prooffile = "/home/tassi/miohelm/tmp/currentproof";; +*) +let prooffile = "/public/sacerdot/currentproof";; +(*CSC: the getter should handle the innertypes, not the FS *) +(* +let innertypesfile = "/home/tassi/miohelm/tmp/innertypes";; +*) +let innertypesfile = "/public/sacerdot/innertypes";; + (* GLOBAL REFERENCES (USED BY CALLBACKS) *) let htmlheader_and_content = ref htmlheader;; @@ -55,6 +77,17 @@ let current_cic_infos = ref None;; let current_goal_infos = ref None;; let current_scratch_infos = ref None;; +(* COMMAND LINE OPTIONS *) + +let usedb = ref true + +let argspec = + [ + "-nodb", Arg.Clear usedb, "disable use of MathQL DB" + ] +in +Arg.parse argspec ignore "" + (* MISC FUNCTIONS *) @@ -141,17 +174,17 @@ let applyStylesheets input styles args = 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 + Cic2Xml.print_object uri ~ids_to_inner_sorts 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 in let input = Xml2Gdome.document_of_xml domImpl xml 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 "/public/sacerdot/innertypes") ; + Xml.pp xmlinnertypes (Some innertypesfile) ; let output = applyStylesheets input mml_styles mml_args in output ;; @@ -233,7 +266,7 @@ prerr_endline ("Offending sequent: " ^ SequentPp.TextualPp.print_sequent current (* 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 = @@ -326,10 +359,10 @@ let call_tactic_with_input tactic rendering_window () = None -> assert false | Some (curi,_,_,_) -> curi in - let metasenv = + let uri,metasenv,bo,ty = match !ProofEngine.proof with None -> assert false - | Some (_,metasenv,_,_) -> metasenv + | Some (uri,metasenv,bo,ty) -> uri,metasenv,bo,ty in let context = List.map @@ -348,10 +381,12 @@ let call_tactic_with_input tactic rendering_window () = try while true do match - CicTextualParserContext.main curi context CicTextualLexer.token lexbuf + CicTextualParserContext.main + curi context metasenv CicTextualLexer.token lexbuf with None -> () - | Some expr -> + | Some (metasenv',expr) -> + ProofEngine.proof := Some (uri,metasenv',bo,ty) ; tactic expr ; refresh_sequent proofw ; refresh_proof output @@ -466,10 +501,10 @@ let call_tactic_with_input_and_goal_input tactic rendering_window () = None -> assert false | Some (curi,_,_,_) -> curi in - let metasenv = + let uri,metasenv,bo,ty = match !ProofEngine.proof with None -> assert false - | Some (_,metasenv,_,_) -> metasenv + | Some (uri,metasenv,bo,ty) -> uri,metasenv,bo,ty in let context = List.map @@ -489,11 +524,12 @@ let call_tactic_with_input_and_goal_input tactic rendering_window () = try while true do match - CicTextualParserContext.main curi context + CicTextualParserContext.main curi context metasenv CicTextualLexer.token lexbuf with None -> () - | Some expr -> + | Some (metasenv',expr) -> + ProofEngine.proof := Some (uri,metasenv',bo,ty) ; tactic ~goal_input:(Hashtbl.find ids_to_terms id) ~input:expr ; refresh_sequent proofw ; @@ -632,6 +668,9 @@ let 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 ;; @@ -653,12 +692,20 @@ let 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 fourier rendering_window = + call_tactic ProofEngine.fourier rendering_window +;; +let rewritesimpl rendering_window = + call_tactic_with_input ProofEngine.rewrite_simpl rendering_window +;; + let whd_in_scratch scratch_window = @@ -717,7 +764,7 @@ let qed rendering_window () = (*???? let dtdname = "http://www.cs.unibo.it/helm/dtd/cic.dtd";; *) -let dtdname = "/projects/helm/V7/dtd/cic.dtd";; +let dtdname = "/home/tassi/miohelm/helm/dtd/cic.dtd";; let save rendering_window () = let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in @@ -730,7 +777,7 @@ let save rendering_window () = 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 = Cic2Xml.print_object uri ~ids_to_inner_sorts acurrentproof in let xml' = [< Xml.xml_cdata "\n" ; Xml.xml_cdata @@ -738,10 +785,10 @@ let save rendering_window () = xml >] in - Xml.pp ~quiet:true xml' (Some "/public/sacerdot/currentproof") ; + Xml.pp ~quiet:true xml' (Some prooffile) ; output_html outputhtml ("

Current proof saved to " ^ - "/public/sacerdot/currentproof

") + prooffile ^ "") ;; (* Used to typecheck the loaded proofs *) @@ -758,7 +805,7 @@ let load rendering_window () = 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 "/public/sacerdot/currentproof" uri with + match CicParser.obj_of_xml prooffile uri with Cic.CurrentProof (_,metasenv,bo,ty) -> typecheck_loaded_proof metasenv bo ty ; ProofEngine.proof := @@ -772,7 +819,7 @@ let load rendering_window () = refresh_sequent proofw ; output_html outputhtml ("

Current proof loaded from " ^ - "/public/sacerdot/currentproof

") + prooffile ^ "") | _ -> assert false with RefreshSequentException e -> @@ -1039,13 +1086,13 @@ let check rendering_window scratch_window () = while true do (* Execute the actions *) match - CicTextualParserContext.main curi names_context CicTextualLexer.token - lexbuf + CicTextualParserContext.main curi names_context metasenv + CicTextualLexer.token lexbuf with None -> () - | Some expr -> + | Some (metasenv',expr) -> try - let ty = CicTypeChecker.type_of_aux' metasenv context expr in + 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 @@ -1061,44 +1108,92 @@ let check rendering_window scratch_window () = ("

" ^ Printexc.to_string e ^ "

") ; ;; +exception NoObjectsLocated;; + +let user_uri_choice uris = + let uri = + match uris with + [] -> raise NoObjectsLocated + | [uri] -> uri + | uris -> + let choice = + GToolbox.question_box ~title:"Ambiguous result." + ~buttons:uris ~default:1 + "Ambiguous result. Please, choose one." + in + List.nth uris (choice-1) + in + String.sub uri 4 (String.length uri - 4) +;; + +(* 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 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 ^ "

" - ) + try + match Str.split (Str.regexp "[ \t]+") input with + [] -> () + | head :: tail -> + inputt#delete_text 0 inputlen ; + let result = MQueryGenerator.locate head 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 ; + let uri' = user_uri_choice uris in + ignore ((inputt#insert_text uri') ~pos:0) + with + e -> + output_html outputhtml + ("

" ^ 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 - let metasenv = - match !ProofEngine.proof with - None -> assert false - | Some (_,metasenv,_,_) -> metasenv - in - let result = - match !ProofEngine.goal with - | None -> "" - | Some metano -> - let (_,_,ty) = - List.find (function (m,_,_) -> m=metano) metasenv - in - MQueryGenerator.backward ty level - in - output_html outputhtml result + 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 + let metasenv = + match !ProofEngine.proof with + None -> assert false + | Some (_,metasenv,_,_) -> metasenv + in + try + match !ProofEngine.goal with + None -> () + | Some metano -> + let (_, ey ,ty) = List.find (function (m,_,_) -> m=metano) metasenv in + let result = MQueryGenerator.backward 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:

" ^ + MQueryGenerator.string_of_levels (MQueryGenerator.levels_of_term metasenv ey ty) "
" ^ + "
" ^ get_last_query result ^ "
" in + output_html outputhtml html ; + let uri' = user_uri_choice uris in + inputt#delete_text 0 inputlen ; + ignore ((inputt#insert_text uri') ~pos:0) + with + e -> + output_html outputhtml + ("

" ^ Printexc.to_string e ^ "

") +;; let choose_selection (mmlwidget : GMathView.math_view) (element : Gdome.element option) @@ -1370,6 +1465,9 @@ class rendering_window output proofw (label : GMisc.label) = 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 @@ -1388,17 +1486,26 @@ class rendering_window output proofw (label : GMisc.label) = 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 hbox4 = GPack.hbox ~packing:(vbox1#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 outputhtml = GHtml.xmhtml ~source:"" @@ -1441,6 +1548,7 @@ object(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)) ; @@ -1448,8 +1556,11 @@ object(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(fourierb#connect#clicked (fourier self)) ; + ignore(rewritesimplb#connect#clicked (rewritesimpl self)) ; ignore(introsb#connect#clicked (intros self)) ; Logger.log_callback := (Logger.log_to_html ~print_and_flush:(output_html outputhtml)) @@ -1457,22 +1568,86 @@ end;; (* MAIN *) +let rendering_window = ref None;; + let initialize_everything () = let module U = Unix in - let output = GMathView.math_view ~width:400 ~height:280 () + let output = GMathView.math_view ~width:350 ~height:280 () and proofw = GMathView.math_view ~width:400 ~height:275 () and label = GMisc.label ~text:"gTopLevel" () in - let rendering_window = + let rendering_window' = new rendering_window output proofw label in - rendering_window#show () ; + rendering_window := Some rendering_window' ; + rendering_window'#show () ; GMain.Main.main () ;; let _ = CicCooking.init () ; - MQueryGenerator.init () ; + if !usedb then + begin + Mqint.init "host=mowgli.cs.unibo.it dbname=helm user=helm" ; + CicTextualParser0.set_locate_object + (function 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 + begin + match !rendering_window with + None -> assert false + | Some rw -> output_html rw#outputhtml html ; + end ; + let uri = + match uris with + [] -> + (match + (GToolbox.input_string ~title:"Unknown input" + ("No URI matching \"" ^ id ^ "\" found. Please enter its URI")) + with + None -> None + | Some uri -> Some ("cic:" ^ uri) + ) + | [uri] -> Some uri + | _ -> + let choice = + GToolbox.question_box ~title:"Ambiguous input." + ~buttons:uris ~default:1 "Ambiguous input. Please, choose one." + in + if choice > 0 then + Some (List.nth uris (choice - 1)) + else + (* No choice from the user *) + None + in + match uri with + Some uri' -> + (* Constant *) + if String.sub uri' (String.length uri' - 4) 4 = ".con" then +(*CSC: what cooking number? Here I always use 0, which may be bugged *) + Some (Cic.Const (UriManager.uri_of_string uri',0)) + else + (try + (* Inductive Type *) + let uri'',typeno = CicTextualLexer.indtyuri_of_uri uri' in +(*CSC: what cooking number? Here I always use 0, which may be bugged *) + Some (Cic.MutInd (uri'',0,typeno)) + with + _ -> + (* Constructor of an Inductive Type *) + let uri'',typeno,consno = + CicTextualLexer.indconuri_of_uri uri' + in +(*CSC: what cooking number? Here I always use 0, which may be bugged *) + Some (Cic.MutConstruct (uri'',0,typeno,consno)) + ) + | None -> None + ) + end ; ignore (GtkMain.Main.init ()) ; initialize_everything () ; - MQueryGenerator.close () + if !usedb then Mqint.close (); ;;