X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FgTopLevel.ml;h=89e56bafc266310c0335985d7f61c19d95cc8b4d;hb=7ff85e55518d06d96b9abbea4aa68d83e6be35b0;hp=808caac082c692b0c6dade5159730e6b283d4be7;hpb=97361ee59354e573e5df31bba78e8e6cda67906d;p=helm.git diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml index 808caac08..89e56bafc 100644 --- a/helm/gTopLevel/gTopLevel.ml +++ b/helm/gTopLevel/gTopLevel.ml @@ -27,7 +27,7 @@ (* *) (* PROJECT HELM *) (* *) -(* Claudio Sacerdoti Coen *) +(* Claudio Sacerdoti Coen *) (* 06/01/2002 *) (* *) (* *) @@ -60,22 +60,53 @@ let htmlfooter = "" ;; -(* -let prooffile = "/home/tassi/miohelm/tmp/currentproof";; -let prooffile = "/public/sacerdot/currentproof";; -*) +let prooffile = "/public/natile/currentproof";; +let prooffiletype = "/public/natile/currentprooftype";; +(* SACERDOT 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";; +(* NATILE +let prooffile = "/public/natile/currentproof";; +let prooffiletype = "/public/natile/currentprooftype";; *) +(* TASSI +let prooffile = "//miohelm/tmp/currentproof";; +let prooffiletype = "/home/tassi/miohelm/tmp/currentprooftype";; +*) + +(* GALATA +let prooffile = "/home/galata/miohelm/currentproof";; +let prooffiletype = "/home/galata/miohelm/currentprooftype";; +*) + +(*CSC: the getter should handle the innertypes, not the FS *) + +let innertypesfile = "/public/natile/innertypes";; +let constanttypefile = "/public/natile/constanttype";; + +(* SACERDOT let innertypesfile = "/public/sacerdot/innertypes";; let constanttypefile = "/public/sacerdot/constanttype";; +*) + +(* NATILE +let innertypesfile = "/public/natile/innertypes";; +let constanttypefile = "/public/natile/constanttype";; +*) + +(* TASSI +let innertypesfile = "/home/tassi/miohelm/tmp/innertypes";; +let constanttypefile = "/home/tassi/miohelm/tmp/constanttype";; +*) + +(* GALATA +let innertypesfile = "/home/galata/miohelm/innertypes";; +let constanttypefile = "/home/galata/miohelm/constanttype";; +*) let empty_id_to_uris = ([],function _ -> None);; @@ -150,29 +181,60 @@ 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' = - (* 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') + try + (* Constant *) + if String.sub uri' (String.length uri' - 4) 4 = ".con" then + CicTextualParser0.ConUri (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) - ) + 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 = @@ -257,10 +319,12 @@ prerr_endline ("### " ^ CicPp.ppterm expr) ; exception NoChoice;; let - interactive_user_uri_choice ~selection_mode ?(ok="Ok") ~title ~msg uris + interactive_user_uri_choice ~selection_mode ?(ok="Ok") + ?(enable_button_for_non_vars=false) ~title ~msg uris = let choices = ref [] in let chosen = ref false in + let use_only_constants = ref false in let window = GWindow.dialog ~modal:true ~title ~width:600 () in let lMessage = @@ -290,6 +354,13 @@ let GButton.button ~label:ok ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in let _ = okb#misc#set_sensitive false in + let nonvarsb = + GButton.button + ~packing: + (function w -> + if enable_button_for_non_vars then + hbox#pack ~expand:false ~fill:false ~padding:5 w) + ~label:"Try constants only" () in let checkb = GButton.button ~label:"Check" ~packing:(hbox#pack ~padding:5) () in @@ -306,6 +377,13 @@ let ignore (cancelb#connect#clicked window#destroy) ; ignore (okb#connect#clicked (function () -> chosen := true ; window#destroy ())) ; + ignore + (nonvarsb#connect#clicked + (function () -> + use_only_constants := true ; + chosen := true ; + window#destroy () + )) ; ignore (checkb#connect#clicked check_callback) ; ignore (clist#connect#select_row @@ -339,8 +417,13 @@ let window#set_position `CENTER ; window#show () ; GMain.Main.main () ; - if !chosen && List.length !choices > 0 then - !choices + if !chosen then + if !use_only_constants then + List.filter + (function uri -> not (String.sub uri (String.length uri - 4) 4 = ".var")) + uris + else + if List.length !choices > 0 then !choices else raise NoChoice else raise NoChoice ;; @@ -411,13 +494,6 @@ let get_last_query = function result -> !query ^ "

Result:

" ^ MQueryUtil.text_of_result result "
" ;; -let register_alias (id,uri) = - let dom,resolve_id = !id_to_uris in - id_to_uris := - (if List.mem id dom then dom else id::dom), - function id' -> if id' = id then Some uri else resolve_id id' -;; - let domImpl = Gdome.domImplementation ();; let parseStyle name = @@ -506,11 +582,12 @@ let = (*CSC: ????????????????? *) let xml, bodyxml = - Cic2Xml.print_object uri ~ids_to_inner_sorts annobj + 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 = match bodyxml with @@ -527,6 +604,55 @@ let output ;; +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 xmlinnertypes = + Cic2Xml.print_inner_types uri ~ids_to_inner_sorts ~ids_to_inner_types + ~ask_dtd_to_the_getter:false + in + (* 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 *) @@ -667,6 +793,29 @@ let mml_of_cic_term metano term = exception OpenConjecturesStillThere;; exception WrongProof;; +let pathname_of_annuri uristring = + Configuration.annotations_dir ^ + Str.replace_first (Str.regexp "^cic:") "" uristring +;; + +let make_dirs dirpath = + ignore (Unix.system ("mkdir -p " ^ dirpath)) +;; + +let save_obj uri obj = + 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'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 +;; + let qed () = match !ProofEngine.proof with None -> assert false @@ -689,6 +838,12 @@ let qed () = 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, @@ -699,12 +854,6 @@ let qed () = | _ -> 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 @@ -718,7 +867,10 @@ let save () = Cic2acic.acic_object_of_cic_object currentproof in let xml, bodyxml = - match Cic2Xml.print_object uri ~ids_to_inner_sorts acurrentproof with + match + Cic2Xml.print_object uri ~ids_to_inner_sorts + ~ask_dtd_to_the_getter:true acurrentproof + with xml,Some bodyxml -> xml,bodyxml | _,None -> assert false in @@ -750,27 +902,33 @@ let load () = 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 + 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 @@ -786,25 +944,79 @@ let load () = ;; let edit_aliases () = - let inputt = ((rendering_window ())#inputt : GEdit.text) in + 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 - 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)) + 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 := empty_id_to_uris + id_to_uris := dom,resolve_id ;; let proveit () = @@ -916,7 +1128,9 @@ let setgoal metano = ("

" ^ Printexc.to_string e ^ "

") ;; -let show_in_show_window, show_in_show_window_callback = +let + show_in_show_window_obj, show_in_show_window_uri, show_in_show_window_callback += let window = GWindow.window ~width:800 ~border_width:2 () in let scrolled_window = @@ -925,35 +1139,37 @@ let show_in_show_window, show_in_show_window_callback = 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 show_in_show_window_obj uri obj = 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 + 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 - 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 ; + 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_uri uri = + let obj = CicEnvironment.get_obj uri in + show_in_show_window_obj uri obj 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) + show_in_show_window_uri (UriManager.uri_of_string uri) else if mmlwidget#get_action <> None then mmlwidget#action_toggle @@ -961,7 +1177,8 @@ let show_in_show_window, show_in_show_window_callback = let _ = mmlwidget#connect#clicked (show_in_show_window_callback mmlwidget) in - show_in_show_window, show_in_show_window_callback + show_in_show_window_obj, show_in_show_window_uri, + show_in_show_window_callback ;; exception NoObjectsLocated;; @@ -1000,7 +1217,7 @@ let locate_callback id = ;; let locate () = - let inputt = ((rendering_window ())#inputt : GEdit.text) in + let inputt = ((rendering_window ())#inputt : term_editor) in let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in try match @@ -1009,8 +1226,7 @@ let locate () = None -> raise NoChoice | Some input -> let uri = locate_callback input in - inputt#delete_text 0 inputt#length ; - ignore ((inputt#insert_text uri) ~pos:0) + inputt#set_term uri with e -> output_html outputhtml @@ -1140,6 +1356,7 @@ let locate_one_id id = interactive_user_uri_choice ~selection_mode:`EXTENDED ~ok:"Try every selection." + ~enable_button_for_non_vars:true ~title:"Ambiguous input." ~msg: ("Ambiguous input \"" ^ id ^ @@ -1241,50 +1458,461 @@ let disambiguate_input context metasenv dom mk_metasenv_and_expr = mk_metasenv_and_expr resolve_id' ;; -let state () = - let inputt = ((rendering_window ())#inputt : GEdit.text) in +exception UriAlreadyInUse;; +exception NotAUriToAConstant;; + +let new_inductive () = 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 + + let chosen = ref false in + let inductive = ref true in + let paramsno = ref 0 in + let get_uri = ref (function _ -> assert false) in + let get_base_uri = ref (function _ -> assert false) in + let get_names = ref (function _ -> assert false) in + let get_types_and_cons = ref (function _ -> assert false) in + let get_name_context_context_and_subst = ref (function _ -> assert false) in + let window = + GWindow.window + ~width:600 ~modal:true ~position:`CENTER + ~title:"New Block of Mutual (Co)Inductive Definitions" + ~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 block:" + ~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 hbox0 = + GPack.hbox ~border_width:0 + ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in + let _ = + GMisc.label + ~text: + "Enter the number of left parameters in every arity and constructor type:" + ~packing:(hbox0#pack ~expand:false ~fill:false ~padding:5) () in + let paramsno_entry = + GEdit.entry ~editable:true ~text:"0" + ~packing:(hbox0#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:"Are the definitions inductive or coinductive?" + ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in + let inductiveb = + GButton.radio_button ~label:"Inductive" + ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in + let coinductiveb = + GButton.radio_button ~label:"Coinductive" + ~group:inductiveb#group + ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in + let hbox2 = + GPack.hbox ~border_width:0 + ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in + let _ = + GMisc.label ~text:"Enter the list of the names of the types:" + ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5) () in + let names_entry = + GEdit.entry ~editable:true + ~packing:(hbox2#pack ~expand:true ~fill:true ~padding:5) () in + let hboxn = + GPack.hbox ~border_width:0 + ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in + let okb = + GButton.button ~label:"> Next" + ~packing:(hboxn#pack ~expand:false ~fill:false ~padding:5) () in + let _ = okb#misc#set_sensitive true in + let cancelb = + GButton.button ~label:"Abort" + ~packing:(hboxn#pack ~expand:false ~fill:false ~padding:5) () in + ignore (window#connect#destroy GMain.Main.quit) ; + ignore (cancelb#connect#clicked window#destroy) ; + (* First phase *) + let rec phase1 () = + ignore + (okb#connect#clicked + (function () -> + try + let uristr = "cic:" ^ uri_entry#text in + let namesstr = names_entry#text in + let paramsno' = int_of_string (paramsno_entry#text) in + match Str.split (Str.regexp " +") namesstr with + [] -> assert false + | (he::tl) as names -> + let uri = UriManager.uri_of_string (uristr ^ "/" ^ he ^ ".ind") in + begin + try + ignore (Getter.resolve uri) ; + raise UriAlreadyInUse + with + Getter.Unresolved -> + get_uri := (function () -> uri) ; + get_names := (function () -> names) ; + inductive := inductiveb#active ; + paramsno := paramsno' ; + phase2 () + end + with + e -> + output_html outputhtml + ("

" ^ Printexc.to_string e ^ "

") ; + )) + (* Second phase *) + and phase2 () = + let type_widgets = + List.map + (function name -> + let frame = + GBin.frame ~label:name + ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in + let vbox = GPack.vbox ~packing:frame#add () in + let hbox = GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false) () in + let _ = + GMisc.label ~text:("Enter its type:") + ~packing:(hbox#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 + let newinputt = + new term_editor ~width:400 ~height:20 ~packing:scrolled_window#add () + ~isnotempty_callback: + (function b -> + (*non_empty_type := b ;*) + okb#misc#set_sensitive true) (*(b && uri_entry#text <> ""))*) + in + let hbox = + GPack.hbox ~border_width:0 + ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in + let _ = + GMisc.label ~text:("Enter the list of its constructors:") + ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in + let cons_names_entry = + GEdit.entry ~editable:true + ~packing:(hbox#pack ~expand:true ~fill:true ~padding:5) () in + (newinputt,cons_names_entry) + ) (!get_names ()) + in + vbox#remove hboxn#coerce ; + let hboxn = + GPack.hbox ~border_width:0 + ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in + let okb = + GButton.button ~label:"> Next" + ~packing:(hboxn#pack ~expand:false ~fill:false ~padding:5) () in + let cancelb = + GButton.button ~label:"Abort" + ~packing:(hboxn#pack ~expand:false ~fill:false ~padding:5) () in + ignore (cancelb#connect#clicked window#destroy) ; + ignore + (okb#connect#clicked + (function () -> + try + let names = !get_names () in + let types_and_cons = + List.map2 + (fun name (newinputt,cons_names_entry) -> + let dom,mk_metasenv_and_expr = + newinputt#get_term ~context:[] ~metasenv:[] in + let consnamesstr = cons_names_entry#text in + let cons_names = Str.split (Str.regexp " +") consnamesstr in + let metasenv,expr = + disambiguate_input [] [] dom mk_metasenv_and_expr + in + match metasenv with + [] -> expr,cons_names + | _ -> raise AmbiguousInput + ) names type_widgets + in + (* Let's see if so far the definition is well-typed *) + let uri = !get_uri () in + let params = [] in + let paramsno = 0 in + let tys = + let i = ref 0 in + List.map2 + (fun name (ty,cons) -> + let cons' = + List.map + (function consname -> consname, Cic.MutInd (uri,!i,[])) cons in + let res = (name, !inductive, ty, cons') in + incr i ; + res + ) names types_and_cons 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 -> +(*CSC: test momentaneamente disattivato. Debbo generare dei costruttori validi + anche quando paramsno > 0 ;-(((( + CicTypeChecker.typecheck_mutual_inductive_defs uri + (tys,params,paramsno) ; +*) + get_name_context_context_and_subst := + (function () -> + let i = ref 0 in + List.fold_left2 + (fun (namecontext,context,subst) name (ty,_) -> + let res = + (Some (Cic.Name name))::namecontext, + (Some (Cic.Name name, Cic.Decl ty))::context, + (Cic.MutInd (uri,!i,[]))::subst + in + incr i ; res + ) ([],[],[]) names types_and_cons) ; + let types_and_cons' = + List.map2 + (fun name (ty,cons) -> (name, !inductive, ty, phase3 name cons)) + names types_and_cons + in + get_types_and_cons := (function () -> types_and_cons') ; + chosen := true ; + window#destroy () + with + e -> + output_html outputhtml + ("

" ^ Printexc.to_string e ^ "

") ; + )) + (* Third phase *) + and phase3 name cons = + let get_cons_types = ref (function () -> assert false) in + let window2 = + GWindow.window + ~width:600 ~modal:true ~position:`CENTER + ~title:(name ^ " Constructors") + ~border_width:2 () in + let vbox = GPack.vbox ~packing:window2#add () in + let cons_type_widgets = + List.map + (function consname -> + let hbox = + GPack.hbox ~border_width:0 + ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in + let _ = + GMisc.label ~text:("Enter the type of " ^ consname ^ ":") + ~packing:(hbox#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 + let newinputt = + new term_editor ~width:400 ~height:20 ~packing:scrolled_window#add () + ~isnotempty_callback: + (function b -> + (* (*non_empty_type := b ;*) + okb#misc#set_sensitive true) (*(b && uri_entry#text <> ""))*) *)()) + in + newinputt + ) cons in + let hboxn = + GPack.hbox ~border_width:0 + ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in + let okb = + GButton.button ~label:"> Next" + ~packing:(hboxn#pack ~expand:false ~fill:false ~padding:5) () in + let _ = okb#misc#set_sensitive true in + let cancelb = + GButton.button ~label:"Abort" + ~packing:(hboxn#pack ~expand:false ~fill:false ~padding:5) () in + ignore (window2#connect#destroy GMain.Main.quit) ; + ignore (cancelb#connect#clicked window2#destroy) ; + ignore + (okb#connect#clicked + (function () -> + try + chosen := true ; + let namecontext,context,subst= !get_name_context_context_and_subst () in + let cons_types = + List.map2 + (fun name inputt -> + let dom,mk_metasenv_and_expr = + inputt#get_term ~context:namecontext ~metasenv:[] + in + let metasenv,expr = + disambiguate_input context [] dom mk_metasenv_and_expr + in + match metasenv with + [] -> + let undebrujined_expr = + List.fold_left + (fun expr t -> CicSubstitution.subst t expr) expr subst + in + name, undebrujined_expr + | _ -> raise AmbiguousInput + ) cons cons_type_widgets + in + get_cons_types := (function () -> cons_types) ; + window2#destroy () + with + e -> + output_html outputhtml + ("

" ^ Printexc.to_string e ^ "

") ; + )) ; + window2#show () ; + GMain.Main.main () ; + let okb_pressed = !chosen in + chosen := false ; + if (not okb_pressed) then + begin + window#destroy () ; + assert false (* The control never reaches this point *) + end + else + (!get_cons_types ()) + in + phase1 () ; + (* No more phases left or Abort pressed *) + window#show () ; + GMain.Main.main () ; + window#destroy () ; + if !chosen then + try + let uri = !get_uri () in +(*CSC: Da finire *) + let params = [] in + let tys = !get_types_and_cons () in + let obj = Cic.InductiveDefinition tys params !paramsno in + begin + try + prerr_endline (CicPp.ppobj obj) ; + CicTypeChecker.typecheck_mutual_inductive_defs uri + (tys,params,!paramsno) ; + with + e -> + prerr_endline "Offending mutual (co)inductive type declaration:" ; + prerr_endline (CicPp.ppobj obj) ; + end ; + (* We already know that obj is well-typed. We need to add it to the *) + (* environment in order to compute the inner-types without having to *) + (* debrujin it or having to modify lots of other functions to avoid *) + (* asking the environment for the MUTINDs we are defining now. *) + CicEnvironment.put_inductive_definition uri obj ; + save_obj uri obj ; + show_in_show_window_obj uri obj + with + e -> + output_html outputhtml + ("

" ^ Printexc.to_string e ^ "

") ; +;; + +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 = @@ -1301,14 +1929,12 @@ prerr_endline ("### " ^ CicPp.ppterm expr ^ " ==> " ^ CicPp.ppterm ty) ; ;; let check scratch_window () = - let inputt = ((rendering_window ())#inputt : GEdit.text) in + let inputt = ((rendering_window ())#inputt : term_editor) 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 = + let metasenv = match !ProofEngine.proof with - None -> UriManager.uri_of_string "cic:/dummy.con", [] - | Some (curi,metasenv,_,_) -> curi,metasenv + None -> [] + | Some (_,metasenv,_,_) -> metasenv in let context,names_context = let context = @@ -1327,26 +1953,16 @@ let check scratch_window () = | 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 ^ "

") ; + 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 ^ "

") ; ;; @@ -1393,23 +2009,14 @@ 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 : GEdit.text) in + let inputt = ((rendering_window ())#inputt : term_editor) 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 uri,metasenv,bo,ty = - match !ProofEngine.proof with - None -> assert false - | Some (uri,metasenv,bo,ty) -> uri,metasenv,bo,ty - 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 @@ -1427,26 +2034,17 @@ let call_tactic_with_input tactic () = ) canonical_context in try - while true do - match - CicTextualParserContext.main context metasenv CicTextualLexer.token - lexbuf register_alias - with - None -> () - | Some (dom,mk_metasenv_and_expr) -> - 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 - done + 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 - CicTextualParser0.Eof -> - inputt#delete_text 0 inputlen - | RefreshSequentException e -> + RefreshSequentException e -> output_html outputhtml ("

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

") ; @@ -1527,7 +2125,7 @@ let call_tactic_with_input_and_goal_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 : GEdit.text) in + let inputt = ((rendering_window ())#inputt : term_editor) in let savedproof = !ProofEngine.proof in let savedgoal = !ProofEngine.goal in match notebook#proofw#get_selection with @@ -1544,20 +2142,11 @@ let call_tactic_with_input_and_goal_input tactic () = 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 - None -> assert false - | Some (curi,_,_,_) -> curi - in - let uri,metasenv,bo,ty = - match !ProofEngine.proof with - None -> assert false - | Some (uri,metasenv,bo,ty) -> uri,metasenv,bo,ty - 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 @@ -1573,29 +2162,18 @@ let call_tactic_with_input_and_goal_input tactic () = | None -> None ) canonical_context in - begin - try - while true do - match - CicTextualParserContext.main context metasenv - CicTextualLexer.token lexbuf register_alias - with - None -> () - | Some (dom,mk_metasenv_and_expr) -> - 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 - 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 -> @@ -1628,7 +2206,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 @@ -1718,12 +2296,14 @@ let call_tactic_with_hypothesis_input tactic () = 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 elimintrossimpl = call_tactic_with_input ProofEngine.elim_intros_simpl;; 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 fold_whd = call_tactic_with_input ProofEngine.fold_whd;; +let fold_reduce = call_tactic_with_input ProofEngine.fold_reduce;; +let fold_simpl = call_tactic_with_input ProofEngine.fold_simpl;; 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;; @@ -1735,9 +2315,17 @@ 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 exists = call_tactic ProofEngine.exists;; +let split = call_tactic ProofEngine.split;; let left = call_tactic ProofEngine.left;; let right = call_tactic ProofEngine.right;; let assumption = call_tactic ProofEngine.assumption;; +let generalize = call_tactic_with_goal_input ProofEngine.generalize;; +let absurd = call_tactic_with_input ProofEngine.absurd;; +let contradiction = call_tactic ProofEngine.contradiction;; +(* Galla: come dare alla tattica la lista di termini da decomporre? +let decompose = call_tactic_with_input_and_goal_input ProofEngine.decompose;; +*) let whd_in_scratch scratch_window = call_tactic_with_goal_input_in_scratch ProofEngine.whd_in_scratch @@ -1762,7 +2350,7 @@ let simpl_in_scratch scratch_window = let show () = let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in try - show_in_show_window (input_or_locate_uri ~title:"Show") + show_in_show_window_uri (input_or_locate_uri ~title:"Show") with e -> output_html outputhtml @@ -1805,29 +2393,398 @@ let open_ () = ("

" ^ Printexc.to_string e ^ "

") ; ;; +let show_query_results results = + let window = + GWindow.window + ~modal:false ~title:"Query results." ~border_width:2 () in + let vbox = GPack.vbox ~packing:window#add () in + let hbox = + GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in + let lMessage = + GMisc.label + ~text:"Click on a URI to show that object" + ~packing:hbox#add () in + let scrolled_window = + GBin.scrolled_window ~border_width:10 ~height:400 ~width:600 + ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in + let clist = GList.clist ~columns:1 ~packing:scrolled_window#add () in + ignore + (List.map + (function (uri,_) -> + let n = + clist#append [uri] + in + clist#set_row ~selectable:false n + ) results + ) ; + clist#columns_autosize () ; + ignore + (clist#connect#select_row + (fun ~row ~column ~event -> + let (uristr,_) = List.nth results row in + match + cic_textual_parser_uri_of_string + (wrong_xpointer_format_from_wrong_xpointer_format' uristr) + with + CicTextualParser0.ConUri uri + | CicTextualParser0.VarUri uri + | CicTextualParser0.IndTyUri (uri,_) + | CicTextualParser0.IndConUri (uri,_,_) -> + show_in_show_window_uri uri + ) + ) ; + window#show () +;; + +let refine_constraints (must_obj,must_rel,must_sort) = + let chosen = ref false in + let use_only = ref false in + let window = + GWindow.window + ~modal:true ~title:"Constraints refinement." + ~width:800 ~border_width:2 () in + let vbox = GPack.vbox ~packing:window#add () in + let hbox = + GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in + let lMessage = + GMisc.label + ~text: "\"Only\" constraints can be enforced or not." + ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in + let onlyb = + GButton.toggle_button ~label:"Enforce \"only\" constraints" + ~active:false ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () + in + ignore + (onlyb#connect#toggled (function () -> use_only := onlyb#active)) ; + (* Notebook for the constraints choice *) + let notebook = + GPack.notebook ~scrollable:true + ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in + (* Rel constraints *) + let label = + GMisc.label + ~text: "Constraints on Rels" () in + let vbox' = + GPack.vbox ~packing:(notebook#append_page ~tab_label:label#coerce) + () in + let hbox = + GPack.hbox ~packing:(vbox'#pack ~expand:false ~fill:false ~padding:5) () in + let lMessage = + GMisc.label + ~text: "You can now specify the constraints on Rels." + ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in + let expected_height = 25 * (List.length must_rel + 2) in + let height = if expected_height > 400 then 400 else expected_height in + let scrolled_window = + GBin.scrolled_window ~border_width:10 ~height ~width:600 + ~packing:(vbox'#pack ~expand:true ~fill:true ~padding:5) () in + let scrolled_vbox = GPack.vbox ~packing:scrolled_window#add_with_viewport () in + let rel_constraints = + List.map + (function (position,depth) -> + let hbox = + GPack.hbox + ~packing:(scrolled_vbox#pack ~expand:false ~fill:false ~padding:5) () in + let lMessage = + GMisc.label + ~text:position + ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in + match depth with + None -> position, ref None + | Some depth' -> + let mutable_ref = ref (Some depth') in + let depthb = + GButton.toggle_button + ~label:("depth = " ^ string_of_int depth') ~active:true + ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () + in + ignore + (depthb#connect#toggled + (function () -> + let sel_depth = if depthb#active then Some depth' else None in + mutable_ref := sel_depth + )) ; + position, mutable_ref + ) must_rel in + (* Sort constraints *) + let label = + GMisc.label + ~text: "Constraints on Sorts" () in + let vbox' = + GPack.vbox ~packing:(notebook#append_page ~tab_label:label#coerce) + () in + let hbox = + GPack.hbox ~packing:(vbox'#pack ~expand:false ~fill:false ~padding:5) () in + let lMessage = + GMisc.label + ~text: "You can now specify the constraints on Sorts." + ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in + let expected_height = 25 * (List.length must_sort + 2) in + let height = if expected_height > 400 then 400 else expected_height in + let scrolled_window = + GBin.scrolled_window ~border_width:10 ~height ~width:600 + ~packing:(vbox'#pack ~expand:true ~fill:true ~padding:5) () in + let scrolled_vbox = GPack.vbox ~packing:scrolled_window#add_with_viewport () in + let sort_constraints = + List.map + (function (position,depth,sort) -> + let hbox = + GPack.hbox + ~packing:(scrolled_vbox#pack ~expand:false ~fill:false ~padding:5) () in + let lMessage = + GMisc.label + ~text:(sort ^ " " ^ position) + ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in + match depth with + None -> position, ref None, sort + | Some depth' -> + let mutable_ref = ref (Some depth') in + let depthb = + GButton.toggle_button ~label:("depth = " ^ string_of_int depth') + ~active:true + ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () + in + ignore + (depthb#connect#toggled + (function () -> + let sel_depth = if depthb#active then Some depth' else None in + mutable_ref := sel_depth + )) ; + position, mutable_ref, sort + ) must_sort in + (* Obj constraints *) + let label = + GMisc.label + ~text: "Constraints on constants" () in + let vbox' = + GPack.vbox ~packing:(notebook#append_page ~tab_label:label#coerce) + () in + let hbox = + GPack.hbox ~packing:(vbox'#pack ~expand:false ~fill:false ~padding:5) () in + let lMessage = + GMisc.label + ~text: "You can now specify the constraints on constants." + ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in + let expected_height = 25 * (List.length must_obj + 2) in + let height = if expected_height > 400 then 400 else expected_height in + let scrolled_window = + GBin.scrolled_window ~border_width:10 ~height ~width:600 + ~packing:(vbox'#pack ~expand:true ~fill:true ~padding:5) () in + let scrolled_vbox = GPack.vbox ~packing:scrolled_window#add_with_viewport () in + let obj_constraints = + List.map + (function (uri,position,depth) -> + let hbox = + GPack.hbox + ~packing:(scrolled_vbox#pack ~expand:false ~fill:false ~padding:5) () in + let lMessage = + GMisc.label + ~text:(uri ^ " " ^ position) + ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in + match depth with + None -> uri, position, ref None + | Some depth' -> + let mutable_ref = ref (Some depth') in + let depthb = + GButton.toggle_button ~label:("depth = " ^ string_of_int depth') + ~active:true + ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () + in + ignore + (depthb#connect#toggled + (function () -> + let sel_depth = if depthb#active then Some depth' else None in + mutable_ref := sel_depth + )) ; + uri, position, mutable_ref + ) must_obj in + (* Confirm/abort buttons *) + 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 + ignore (window#connect#destroy GMain.Main.quit) ; + ignore (cancelb#connect#clicked window#destroy) ; + ignore + (okb#connect#clicked (function () -> chosen := true ; window#destroy ())); + window#set_position `CENTER ; + window#show () ; + GMain.Main.main () ; + if !chosen then + let chosen_must_rel = + List.map + (function (position,ref_depth) -> position,!ref_depth) rel_constraints in + let chosen_must_sort = + List.map + (function (position,ref_depth,sort) -> position,!ref_depth,sort) + sort_constraints + in + let chosen_must_obj = + List.map + (function (uri,position,ref_depth) -> uri,position,!ref_depth) + obj_constraints + in + (chosen_must_obj,chosen_must_rel,chosen_must_sort), + (if !use_only then +(*CSC: ???????????????????????? I assume that must and only are the same... *) + Some chosen_must_obj,Some chosen_must_rel,Some chosen_must_sort + else + None,None,None + ) + else + raise NoChoice +;; + +let completeSearchPattern () = + let inputt = ((rendering_window ())#inputt : term_editor) in + let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in + try + let dom,mk_metasenv_and_expr = inputt#get_term ~context:[] ~metasenv:[] in + let metasenv,expr = disambiguate_input [] [] dom mk_metasenv_and_expr in + let must = MQueryLevels2.get_constraints expr in + let must',only = refine_constraints must in + let results = MQueryGenerator.searchPattern must' only in + show_query_results results + with + e -> + output_html outputhtml + ("

" ^ Printexc.to_string e ^ "

") ; +;; + +let choose_must list_of_must only = + let chosen = ref None in + let user_constraints = ref [] in + let window = + GWindow.window + ~modal:true ~title:"Query refinement." ~border_width:2 () in + let vbox = GPack.vbox ~packing:window#add () in + let hbox = + GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in + let lMessage = + GMisc.label + ~text: + ("You can now specify the genericity of the query. " ^ + "The more generic the slower.") + ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in + let hbox = + GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in + let lMessage = + GMisc.label + ~text: + "Suggestion: start with faster queries before moving to more generic ones." + ~packing:(hbox#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 _ = + let page = ref 0 in + let last = List.length list_of_must in + List.map + (function must -> + incr page ; + let label = + GMisc.label ~text: + (if !page = 1 then "More generic" else + if !page = last then "More precise" else " ") () in + let expected_height = 25 * (List.length must + 2) in + let height = if expected_height > 400 then 400 else expected_height in + let scrolled_window = + GBin.scrolled_window ~border_width:10 ~height ~width:600 + ~packing:(notebook#append_page ~tab_label:label#coerce) () in + let clist = + GList.clist ~columns:2 ~packing:scrolled_window#add + ~titles:["URI" ; "Position"] () + in + ignore + (List.map + (function (uri,position) -> + let n = + clist#append + [uri; if position then "MainConclusion" else "Conclusion"] + in + clist#set_row ~selectable:false n + ) must + ) ; + clist#columns_autosize () + ) list_of_must in + let _ = + let label = GMisc.label ~text:"User provided" () in + let vbox = + GPack.vbox ~packing:(notebook#append_page ~tab_label:label#coerce) () in + let hbox = + GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in + let lMessage = + GMisc.label + ~text:"Select the constraints that must be satisfied and press OK." + ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in + let expected_height = 25 * (List.length only + 2) in + let height = if expected_height > 400 then 400 else expected_height in + let scrolled_window = + GBin.scrolled_window ~border_width:10 ~height ~width:600 + ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in + let clist = + GList.clist ~columns:2 ~packing:scrolled_window#add + ~selection_mode:`EXTENDED + ~titles:["URI" ; "Position"] () + in + ignore + (List.map + (function (uri,position) -> + let n = + clist#append + [uri; if position then "MainConclusion" else "Conclusion"] + in + clist#set_row ~selectable:true n + ) only + ) ; + clist#columns_autosize () ; + ignore + (clist#connect#select_row + (fun ~row ~column ~event -> + user_constraints := (List.nth only row)::!user_constraints)) ; + ignore + (clist#connect#unselect_row + (fun ~row ~column ~event -> + user_constraints := + List.filter + (function uri -> uri != (List.nth only row)) !user_constraints)) ; + 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 -> + if n = List.length list_of_must then + (* user provided constraints *) + !user_constraints + else + List.nth list_of_must n +;; let searchPattern () = - let inputt = ((rendering_window ())#inputt : GEdit.text) in + 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 - 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 @@ -1837,7 +2794,22 @@ let searchPattern () = None -> () | Some metano -> let (_, ey ,ty) = List.find (function (m,_,_) -> m=metano) metasenv in - let result = MQueryGenerator.searchPattern metasenv ey ty level in + let list_of_must,only = MQueryLevels.out_restr metasenv ey ty in + let must = choose_must list_of_must only in + let torigth_restriction (u,b) = + let p = + if b then + "http://www.cs.unibo.it/helm/schemas/schema-helm#MainConclusion" + else + "http://www.cs.unibo.it/helm/schemas/schema-helm#InConclusion" + in + (u,p,None) + in + let rigth_must = List.map torigth_restriction must in + let rigth_only = Some (List.map torigth_restriction only) in + let result = + MQueryGenerator.searchPattern + (rigth_must,[],[]) (rigth_only,None,None) in let uris = List.map (function uri,_ -> @@ -1845,9 +2817,6 @@ let searchPattern () = ) 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 ; @@ -1891,8 +2860,7 @@ let searchPattern () = "Many lemmas can be successfully applied. Please, choose one:" uris' in - inputt#delete_text 0 inputt#length ; - ignore ((inputt#insert_text uri') ~pos:0) ; + inputt#set_term uri' ; apply () with e -> @@ -2055,7 +3023,7 @@ end;; (* Scratch window *) -class scratch_window outputhtml = +class scratch_window = let window = GWindow.window ~title:"MathML viewer" ~border_width:2 () in let vbox = @@ -2078,7 +3046,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 @@ -2125,8 +3092,8 @@ object(self) let applyb = GButton.button ~label:"Apply" ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in - let elimsimplintrosb = - GButton.button ~label:"ElimSimplIntros" + let elimintrossimplb = + GButton.button ~label:"ElimIntrosSimpl" ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in let elimtypeb = GButton.button ~label:"ElimType" @@ -2140,14 +3107,20 @@ object(self) 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" + let foldwhdb = + GButton.button ~label:"Fold_whd" ~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 foldreduceb = + GButton.button ~label:"Fold_reduce" + ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in + let foldsimplb = + GButton.button ~label:"Fold_simpl" + ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in + let cutb = + GButton.button ~label:"Cut" + ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in let changeb = GButton.button ~label:"Change" ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in @@ -2163,43 +3136,63 @@ object(self) let clearb = GButton.button ~label:"Clear" ~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 fourierb = GButton.button ~label:"Fourier" - ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in + ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in let rewritesimplb = GButton.button ~label:"RewriteSimpl ->" - ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in + ~packing:(hbox5#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 + ~packing:(hbox5#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 existsb = + GButton.button ~label:"Exists" + ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in + let splitb = + GButton.button ~label:"Split" + ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in + let hbox6 = + GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in let leftb = GButton.button ~label:"Left" - ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in + ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in let rightb = GButton.button ~label:"Right" - ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in + ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in let assumptionb = GButton.button ~label:"Assumption" - ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in + ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in + let generalizeb = + GButton.button ~label:"Generalize" + ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in + let absurdb = + GButton.button ~label:"Absurd" + ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in + let contradictionb = + GButton.button ~label:"Contradiction" + ~packing:(hbox6#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 + ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in + ignore(exactb#connect#clicked exact) ; ignore(applyb#connect#clicked apply) ; - ignore(elimsimplintrosb#connect#clicked elimsimplintros) ; + ignore(elimintrossimplb#connect#clicked elimintrossimpl) ; 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(foldwhdb#connect#clicked fold_whd) ; + ignore(foldreduceb#connect#clicked fold_reduce) ; + ignore(foldsimplb#connect#clicked fold_simpl) ; ignore(cutb#connect#clicked cut) ; ignore(changeb#connect#clicked change) ; ignore(letinb#connect#clicked letin) ; @@ -2211,9 +3204,14 @@ object(self) ignore(reflexivityb#connect#clicked reflexivity) ; ignore(symmetryb#connect#clicked symmetry) ; ignore(transitivityb#connect#clicked transitivity) ; + ignore(existsb#connect#clicked exists) ; + ignore(splitb#connect#clicked split) ; ignore(leftb#connect#clicked left) ; ignore(rightb#connect#clicked right) ; ignore(assumptionb#connect#clicked assumption) ; + ignore(generalizeb#connect#clicked generalize) ; + ignore(absurdb#connect#clicked absurd) ; + ignore(contradictionb#connect#clicked contradiction) ; ignore(introsb#connect#clicked intros) ; ignore(searchpatternb#connect#clicked searchPattern) ; ignore(proofw#connect#selection_changed (choose_selection proofw)) ; @@ -2294,12 +3292,15 @@ end (* Main window *) class rendering_window output (notebook : notebook) = + let scratch_window = new scratch_window in let window = - GWindow.window ~title:"MathML viewer" ~border_width:2 + GWindow.window ~title:"MathML viewer" ~border_width:0 ~allow_shrink:false () in let vbox_for_menu = GPack.vbox ~packing:window#add () in (* menus *) - let menubar = GMenu.menu_bar ~packing:vbox_for_menu#pack () in + 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 *) @@ -2307,18 +3308,27 @@ class rendering_window output (notebook : notebook) = let factory1 = new GMenu.factory file_menu ~accel_group in let export_to_postscript_menu_item = begin - 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 + let _ = + factory1#add_item "New Block of (Co)Inductive Definitions..." + ~key:GdkKeysyms._B ~callback:new_inductive + in + 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._Q ~callback:qed in + 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); @@ -2326,15 +3336,15 @@ class rendering_window output (notebook : notebook) = ignore (!qed_set_sensitive false); ignore (factory1#add_separator ()) ; let export_to_postscript_menu_item = - factory1#add_item "Export to PostScript..." ~key:GdkKeysyms._E + factory1#add_item "Export to PostScript..." ~callback:(export_to_postscript output) in ignore (factory1#add_separator ()) ; ignore - (factory1#add_item "Exit" ~key:GdkKeysyms._C ~callback:GMain.Main.quit) ; + (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 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 = @@ -2352,12 +3362,23 @@ class rendering_window output (notebook : notebook) = 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 searchPattern_menu_item = + factory4#add_item "SearchPattern..." ~key:GdkKeysyms._D + ~callback:completeSearchPattern in + let _ = searchPattern_menu_item#misc#set_sensitive false in let show_menu_item = factory4#add_item "Show..." ~key:GdkKeysyms._H ~callback:show in @@ -2384,23 +3405,17 @@ 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 ~label:"Term input" + GBin.frame ~label:"Insert Term" ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in - let vbox' = - GPack.vbox ~packing:frame#add () in - let hbox4 = - GPack.hbox ~border_width:5 ~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 checkb = - GButton.button ~label:"Check" - ~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 - let inputt = GEdit.text ~editable:true ~width:400 ~height:100 - ~packing:scrolled_window1#add () in + ~packing:frame#add () in + let inputt = + new term_editor ~width:400 ~height:100 ~packing:scrolled_window1#add () + ~isnotempty_callback: + (function b -> + check_menu_item#misc#set_sensitive b ; + searchPattern_menu_item#misc#set_sensitive b) in let vboxl = GPack.vbox ~packing:(hbox0#pack ~expand:true ~fill:true ~padding:5) () in let _ = @@ -2415,7 +3430,6 @@ class rendering_window output (notebook : notebook) = ~border_width:20 ~packing:frame#add ~show:true () in - let scratch_window = new scratch_window outputhtml in object method outputhtml = outputhtml method inputt = inputt @@ -2439,8 +3453,6 @@ object set_settings_window settings_window ; set_outputhtml outputhtml ; ignore(window#event#connect#delete (fun _ -> GMain.Main.quit () ; true )) ; - ignore(stateb#connect#clicked state) ; - ignore(checkb#connect#clicked (check scratch_window)) ; Logger.log_callback := (Logger.log_to_html ~print_and_flush:(output_html outputhtml)) end;; @@ -2460,8 +3472,12 @@ let initialize_everything () = let _ = if !usedb then - Mqint.init "dbname=helm_mowgli" ; -(* Mqint.init "host=mowgli.cs.unibo.it dbname=helm_mowgli user=helm" ; *) + begin + Mqint.set_database Mqint.postgres_db ; + (* Mqint.init "dbname=helm_mowgli" ; *) + (* Mqint.init "host=mowgli.cs.unibo.it dbname=helm_mowgli user=helm" ; *) + Mqint.init "host=mowgli.cs.unibo.it dbname=helm_mowgli_new_schema user=helm"; + end ; ignore (GtkMain.Main.init ()) ; initialize_everything () ; if !usedb then Mqint.close ();