X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FgTopLevel.ml;h=83d959ca38f77f4ed8b76ca31a24611a50971eba;hb=89262281b6e83bd2321150f81f1a0583645eb0c8;hp=2b476a6745c278a7fe07953c747507344f630956;hpb=e34305aa0b9c8c9095e811b7ab720ffd4d283081;p=helm.git diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml index 2b476a674..83d959ca3 100644 --- a/helm/gTopLevel/gTopLevel.ml +++ b/helm/gTopLevel/gTopLevel.ml @@ -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,8 +59,14 @@ 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) *) @@ -681,8 +699,13 @@ let 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 fourier rendering_window = call_tactic ProofEngine.fourier rendering_window;; let whd_in_scratch scratch_window = @@ -741,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 @@ -1085,44 +1108,91 @@ 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_html 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 (_, ey ,ty) = - List.find (function (m,_,_) -> m=metano) metasenv - in - MQueryGenerator.backward metasenv ey 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 @@ -1433,6 +1503,9 @@ class rendering_window output proofw (label : GMisc.label) = 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:"" @@ -1487,6 +1560,7 @@ object(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)) @@ -1494,15 +1568,18 @@ 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 () ;; @@ -1510,15 +1587,30 @@ let _ = CicCooking.init () ; if !usedb then begin - MQueryGenerator.init () ; + Mqint.init "host=mowgli.cs.unibo.it dbname=helm user=helm" ; CicTextualParser0.set_locate_object (function id -> - let MathQL.MQRefs uris = MQueryGenerator.locate id 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 + begin + match !rendering_window with + None -> assert false + | Some rw -> output_html rw#outputhtml html ; + end ; let uri = match uris with [] -> - (GToolbox.input_string ~title:"Unknown input" - ("No URI matching \"" ^ id ^ "\" found. Please enter its URI")) + (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 = @@ -1557,5 +1649,5 @@ let _ = end ; ignore (GtkMain.Main.init ()) ; initialize_everything () ; - if !usedb then MQueryGenerator.close (); + if !usedb then Mqint.close (); ;;