From 97361ee59354e573e5df31bba78e8e6cda67906d Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 18 Nov 2002 09:58:46 +0000 Subject: [PATCH] Major interface improvements. The aim is to substitute the GEdit widget to input text with a widget to input Cic terms. --- helm/gTopLevel/gTopLevel.ml | 1524 ++++++++++++++++++++--------------- 1 file changed, 859 insertions(+), 665 deletions(-) diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml index 58e785dec..808caac08 100644 --- a/helm/gTopLevel/gTopLevel.ml +++ b/helm/gTopLevel/gTopLevel.ml @@ -48,6 +48,7 @@ let wrong_xpointer_format_from_wrong_xpointer_format' 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 = "" ^ @@ -399,6 +400,7 @@ let interactive_interpretation_choice interpretations = | Some n -> n ;; + (* MISC FUNCTIONS *) (* CSC: IMPERATIVE AND NOT VERY CLEAN, TO GET THE LAST ISSUED QUERY *) @@ -416,131 +418,6 @@ let register_alias (id,uri) = function id' -> if id' = id then Some uri else resolve_id id' ;; -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 - [] -> - (match - (GToolbox.input_string ~title:"Unknown input" - ("No URI matching \"" ^ id ^ "\" found. Please enter its URI")) - with - None -> raise NoChoice - | Some uri -> ["cic:" ^ uri] - ) - | [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' -;; - let domImpl = Gdome.domImplementation ();; let parseStyle name = @@ -568,22 +445,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];; @@ -600,7 +478,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'" ] ;; @@ -622,7 +501,9 @@ let applyStylesheets input styles args = input styles ;; -let mml_of_cic_object uri annobj ids_to_inner_sorts ids_to_inner_types = +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 annobj @@ -642,7 +523,7 @@ let mml_of_cic_object uri annobj ids_to_inner_sorts ids_to_inner_types = (*CSC: stylesheet. This DOES NOT work when UWOBO and/or the getter are not *) (*CSC: local. *) Xml.pp xmlinnertypes (Some innertypesfile) ; - let output = applyStylesheets input mml_styles mml_args in + let output = applyStylesheets input mml_styles (mml_args ~explode_all) in output ;; @@ -669,7 +550,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 := @@ -771,17 +653,703 @@ let mml_of_cic_term metano term = let sequent_gdome,ids_to_terms,ids_to_father_ids,ids_to_hypotheses = SequentPp.XmlPp.print_sequent metasenv (metano,context,term) in - let sequent_doc = - Xml2Gdome.document_of_xml domImpl sequent_gdome - in - let res = - applyStylesheets sequent_doc sequent_styles sequent_args ; - in - current_scratch_infos := - Some (term,ids_to_terms,ids_to_father_ids,ids_to_hypotheses) ; - res + let sequent_doc = + Xml2Gdome.document_of_xml domImpl sequent_gdome + in + let res = + applyStylesheets sequent_doc sequent_styles sequent_args ; + in + current_scratch_infos := + Some (term,ids_to_terms,ids_to_father_ids,ids_to_hypotheses) ; + res +;; + +exception OpenConjecturesStillThere;; +exception WrongProof;; + +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 ; + 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/tassi/miohelm/helm/dtd/cic.dtd";; +*) +let dtdname = "/projects/helm/V7_mowgli/dtd/cic.dtd";; + +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 + 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 acurrentproof with + 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 + let uri = UriManager.uri_of_string "cic:/dummy.con" 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 inputt = ((rendering_window ())#inputt : GEdit.text) in + let dom,resolve_id = !id_to_uris in + let inputlen = inputt#length in + inputt#delete_text 0 inputlen ; + let _ = + inputt#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)) + in + id_to_uris := empty_id_to_uris +;; + +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 : GEdit.text) 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#delete_text 0 inputt#length ; + ignore ((inputt#insert_text uri) ~pos:0) + 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' +;; + +let state () = + 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 notebook = (rendering_window ())#notebook 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 + CicTextualParserContext.main [] [] CicTextualLexer.token + lexbuf register_alias + with + None -> () + | Some (dom,mk_metasenv_and_expr) -> + let metasenv,expr = + disambiguate_input [] [] dom mk_metasenv_and_expr + in + let _ = CicTypeChecker.type_of_aux' metasenv [] expr in + ProofEngine.proof := + Some (UriManager.uri_of_string "cic:/dummy.con", + (1,[],expr)::metasenv, Cic.Meta (1,[]), expr) ; + ProofEngine.goal := Some 1 ; + refresh_sequent notebook ; + refresh_proof output ; + !save_set_sensitive true + 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 ^ "

") + | 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 : GEdit.text) in + let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) 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 + let lexbuf = Lexing.from_string input in + try + while true do + (* Execute the actions *) + match + CicTextualParserContext.main names_context metasenv CicTextualLexer.token + lexbuf register_alias + with + None -> () + | Some (dom,mk_metasenv_and_expr) -> + let (metasenv',expr) = + disambiguate_input context metasenv dom mk_metasenv_and_expr + in + check_term_in_scratch scratch_window metasenv' context expr + done + with + CicTextualParser0.Eof -> () + | e -> + output_html outputhtml + ("

" ^ Printexc.to_string e ^ "

") ; ;; + (***********************) (* TACTICS *) (***********************) @@ -1164,294 +1732,51 @@ 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 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 () = - 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 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/tassi/miohelm/helm/dtd/cic.dtd";; -*) -let dtdname = "/projects/helm/V7_mowgli/dtd/cic.dtd";; - -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 - 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 acurrentproof with - 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 - let uri = UriManager.uri_of_string "cic:/dummy.con" 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 inputt = ((rendering_window ())#inputt : GEdit.text) in - let dom,resolve_id = !id_to_uris in - let inputlen = inputt#length in - inputt#delete_text 0 inputlen ; - let _ = - inputt#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)) - in - id_to_uris := empty_id_to_uris -;; - -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 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 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!!!" *) +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 ;; -exception NoPrevGoal;; -exception NoNextGoal;; -let setgoal metano = - let module L = LogicalOperations in - let module G = Gdome in - let notebook = (rendering_window ())#notebook in + +(**********************) +(* END OF TACTICS *) +(**********************) + + +let show () = 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 ^ "

") + try + show_in_show_window (input_or_locate_uri ~title:"Show") + with + e -> + output_html outputhtml + ("

" ^ Printexc.to_string e ^ "

") ; ;; exception NotADefinition;; let open_ () = - 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 notebook = (rendering_window ())#notebook in - let inputlen = inputt#length in - let input = inputt#get_chars 0 inputlen 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 with @@ -1465,8 +1790,7 @@ let open_ () = Some (uri, metasenv, bo, ty) ; ProofEngine.goal := None ; refresh_sequent notebook ; - refresh_proof output ; - inputt#delete_text 0 inputlen + refresh_proof output with RefreshSequentException e -> output_html outputhtml @@ -1481,236 +1805,99 @@ let open_ () = ("

" ^ Printexc.to_string e ^ "

") ; ;; -let state () = - 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 notebook = (rendering_window ())#notebook 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 - CicTextualParserContext.main [] [] CicTextualLexer.token - lexbuf register_alias - with - None -> () - | Some (dom,mk_metasenv_and_expr) -> - let metasenv,expr = - disambiguate_input [] [] dom mk_metasenv_and_expr - in - let _ = CicTypeChecker.type_of_aux' metasenv [] expr in - ProofEngine.proof := - Some (UriManager.uri_of_string "cic:/dummy.con", - (1,[],expr)::metasenv, Cic.Meta (1,[]), expr) ; - ProofEngine.goal := Some 1 ; - refresh_sequent notebook ; - refresh_proof output ; - !save_set_sensitive true - 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 ^ "

") - | 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 searchPattern () = 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 ^ "\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 - let lexbuf = Lexing.from_string input in - try - while true do - (* Execute the actions *) - match - CicTextualParserContext.main names_context metasenv CicTextualLexer.token - lexbuf register_alias - with - None -> () - | Some (dom,mk_metasenv_and_expr) -> - let (metasenv',expr) = - disambiguate_input context metasenv dom mk_metasenv_and_expr - in - check_term_in_scratch scratch_window metasenv' context expr - done + 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 ^ "

") ; -;; - -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 () = - 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 - 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 ~title:"Ambiguous input." - ~msg: - ("Ambiguous input \"" ^ head ^ - "\". Please, choose one interpetation:") - uris - in - ignore ((inputt#insert_text uri') ~pos:0) - with - e -> - output_html outputhtml - ("

" ^ Printexc.to_string e ^ "

") -;; - -let searchPattern () = - 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.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:

" ^ - MQueryGenerator.string_of_levels + 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 + 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:

" ^ + MQueryGenerator.string_of_levels (MQueryGenerator.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') ^ "

" + 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 - output_html outputhtml html' ; - let uri' = - user_uri_choice ~title:"Ambiguous input." - ~msg:"Many lemmas can be successfully applied. Please, choose one:" - uris' + 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 - inputt#delete_text 0 inputlen ; - ignore ((inputt#insert_text uri') ~pos:0) - with - e -> - output_html outputhtml - ("

" ^ Printexc.to_string e ^ "

") + output_html outputhtml html' ; + let uri' = + user_uri_choice ~title:"Ambiguous input." + ~msg: + "Many lemmas can be successfully applied. Please, choose one:" + uris' + in + inputt#delete_text 0 inputt#length ; + ignore ((inputt#insert_text uri') ~pos:0) ; + apply () + with + e -> + output_html outputhtml + ("

" ^ Printexc.to_string e ^ "

") ;; let choose_selection @@ -2002,6 +2189,9 @@ object(self) 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) ; @@ -2025,6 +2215,7 @@ object(self) 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 @@ -2122,6 +2313,10 @@ class rendering_window output (notebook : notebook) = let save_menu_item = factory1#add_item "Save Unfinished Proof" ~key:GdkKeysyms._S ~callback:save 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._Q ~callback:qed in ignore @@ -2139,7 +2334,7 @@ class rendering_window output (notebook : notebook) = export_to_postscript_menu_item end in (* edit menu *) - let edit_menu = factory0#add_submenu "Edit" in + 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 = @@ -2157,6 +2352,15 @@ class rendering_window output (notebook : notebook) = focus_menu_item#misc#set_sensitive b in let _ = !focus_and_proveit_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 @@ -2180,7 +2384,8 @@ class rendering_window output (notebook : notebook) = ~packing:(vbox#pack ~expand:true ~padding:5) () in let _ = scrolled_window0#add output#coerce in let frame = - GBin.frame ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in + GBin.frame ~label:"Term input" + ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in let vbox' = GPack.vbox ~packing:frame#add () in let hbox4 = @@ -2188,18 +2393,9 @@ class rendering_window output (notebook : notebook) = 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 searchpatternb = - GButton.button ~label:"SearchPattern" - ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in let scrolled_window1 = GBin.scrolled_window ~border_width:5 ~packing:(vbox'#pack ~expand:true ~padding:0) () in @@ -2237,16 +2433,14 @@ object 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 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) ; - ignore(openb#connect#clicked open_) ; ignore(checkb#connect#clicked (check scratch_window)) ; - ignore(locateb#connect#clicked locate) ; - ignore(searchpatternb#connect#clicked searchPattern) ; Logger.log_callback := (Logger.log_to_html ~print_and_flush:(output_html outputhtml)) end;; -- 2.39.2