From e07312820aa16f76e7584eb40d4e517c7d254667 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 14 Nov 2002 11:29:52 +0000 Subject: [PATCH] Interface improvement: - the pages of every notebook are now generated with lazy code - the interface to choose between several interpretations is now really nice --- helm/gTopLevel/gTopLevel.ml | 410 +++++++++++++++++++++--------------- 1 file changed, 238 insertions(+), 172 deletions(-) diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml index 40e60b47e..ff9396213 100644 --- a/helm/gTopLevel/gTopLevel.ml +++ b/helm/gTopLevel/gTopLevel.ml @@ -201,35 +201,48 @@ let output_html outputhtml msg = (* Check window *) -let check_window outputhtml uris_and_terms = +let check_window outputhtml uris = let window = GWindow.window ~width:800 ~modal:true ~title:"Check" ~border_width:2 () in let notebook = GPack.notebook ~scrollable:true ~packing:window#add () in - ignore ( + window#show () ; + let render_terms = List.map - (function (uri,expr) -> + (function uri -> let scrolled_window = GBin.scrolled_window ~border_width:10 ~packing: (notebook#append_page ~tab_label:((GMisc.label ~text:uri ())#coerce) ) - () in - let mmlwidget = - GMathView.math_view - ~packing:(scrolled_window#add) ~width:400 ~height:280 () in - try - let mml = !mml_of_cic_term_ref 111 expr in + () + in + lazy + (let mmlwidget = + GMathView.math_view + ~packing:scrolled_window#add ~width:400 ~height:280 () in + let expr = + let term = + term_of_cic_textual_parser_uri (cic_textual_parser_uri_of_string uri) + in + (Cic.Cast (term, CicTypeChecker.type_of_aux' [] [] term)) + in + try + let mml = !mml_of_cic_term_ref 111 expr in prerr_endline ("### " ^ CicPp.ppterm expr) ; - mmlwidget#load_tree ~dom:mml - with - e -> - output_html outputhtml - ("

" ^ Printexc.to_string e ^ "

") - ) uris_and_terms) ; - window#show () + mmlwidget#load_tree ~dom:mml + with + e -> + output_html outputhtml + ("

" ^ Printexc.to_string e ^ "

") + ) + ) uris + in + ignore + (notebook#connect#switch_page + (function i -> Lazy.force (List.nth render_terms i))) ;; exception NoChoice;; @@ -248,7 +261,7 @@ let GBin.scrolled_window ~border_width:10 ~packing:(window#vbox#pack ~expand:true ~fill:true ~padding:5) () in let clist = - let expected_height = 8 * List.length uris in + let expected_height = 18 * List.length uris in let height = if expected_height > 400 then 400 else expected_height in GList.clist ~columns:1 ~packing:scrolled_window#add ~height ~selection_mode () in @@ -278,16 +291,7 @@ let (* actions *) let check_callback () = assert (List.length !choices > 0) ; - check_window (outputhtml ()) - (List.map - (function uri -> - let term = - term_of_cic_textual_parser_uri - (cic_textual_parser_uri_of_string uri) - in - uri, - (Cic.Cast (term, CicTypeChecker.type_of_aux' [] [] term)) - ) !choices) + check_window (outputhtml ()) !choices in ignore (window#connect#destroy GMain.Main.quit) ; ignore (cancelb#connect#clicked window#destroy) ; @@ -326,12 +330,67 @@ let window#set_position `CENTER ; window#show () ; GMain.Main.main () ; - if !chosen or List.length !choices > 0 then + if !chosen && List.length !choices > 0 then !choices else raise NoChoice ;; +let interactive_interpretation_choice interpretations = + let chosen = ref None in + let window = + GWindow.window + ~modal:true ~title:"Ambiguous well-typed input." ~border_width:2 () in + let vbox = GPack.vbox ~packing:window#add () in + let lMessage = + GMisc.label + ~text: + ("Ambiguous input since there are many well-typed interpretations." ^ + " Please, choose one of them.") + ~packing:(vbox#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 _ = + List.map + (function interpretation -> + let clist = + let expected_height = 18 * List.length interpretation in + let height = if expected_height > 400 then 400 else expected_height in + GList.clist ~columns:2 ~packing:notebook#append_page ~height + ~titles:["id" ; "URI"] () + in + ignore + (List.map + (function (id,uri) -> + let n = clist#append [id;uri] in + clist#set_row ~selectable:false n + ) interpretation + ) ; + clist#columns_autosize () + ) interpretations 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 -> n +;; + (* MISC FUNCTIONS *) (* CSC: IMPERATIVE AND NOT VERY CLEAN, TO GET THE LAST ISSUED QUERY *) @@ -372,7 +431,7 @@ let locate_one_id id = | _ -> interactive_user_uri_choice ~selection_mode:`EXTENDED - ~ok:"Try all the sections." + ~ok:"Try every selection." ~title:"Ambiguous input." ~msg: ("Ambiguous input \"" ^ id ^ @@ -418,7 +477,9 @@ let disambiguate_input context metasenv dom mk_metasenv_and_expr = in aux dom' list_of_uris in -prerr_endline ("##### NE DISAMBIGUO: " ^ string_of_int (List.length resolve_ids)) ; + 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 = @@ -444,37 +505,27 @@ prerr_endline ("##### NE DISAMBIGUO: " ^ string_of_int (List.length resolve_ids) let choices = List.map (function resolve -> - String.concat " ; " - (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 - ) + 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 choice = - GToolbox.question_box ~title:"Ambiguous input." - ~buttons:choices - ~default:1 "Ambiguous input. Please, choose one interpretation." - in - if choice > 0 then - List.nth resolve_ids' (choice - 1) - else - (* No choice from the user *) - raise NoChoice + 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' @@ -1829,116 +1880,129 @@ end;; class page () = let vbox1 = GPack.vbox () in - let scrolled_window1 = - GBin.scrolled_window ~border_width:10 - ~packing:(vbox1#pack ~expand:true ~padding:5) () in - let proofw = - GMathView.math_view ~width:400 ~height:275 - ~packing:(scrolled_window1#add) () in - let hbox3 = - GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in - let exactb = - GButton.button ~label:"Exact" - ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in - let introsb = - GButton.button ~label:"Intros" - ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in - let applyb = - GButton.button ~label:"Apply" - ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in - let elimsimplintrosb = - GButton.button ~label:"ElimSimplIntros" - ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in - let elimtypeb = - GButton.button ~label:"ElimType" - ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in - let whdb = - GButton.button ~label:"Whd" - ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in - let reduceb = - GButton.button ~label:"Reduce" - ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in - 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" - ~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 changeb = - GButton.button ~label:"Change" - ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in - let letinb = - GButton.button ~label:"Let ... In" - ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in - let ringb = - GButton.button ~label:"Ring" - ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in - let clearbodyb = - GButton.button ~label:"ClearBody" - ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in - let clearb = - GButton.button ~label:"Clear" - ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in - let fourierb = - GButton.button ~label:"Fourier" - ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in - let rewritesimplb = - GButton.button ~label:"RewriteSimpl ->" - ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in - let 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 - 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 leftb = - GButton.button ~label:"Left" - ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in - let rightb = - GButton.button ~label:"Right" - ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in - let assumptionb = - GButton.button ~label:"Assumption" - ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in -object - method proofw = proofw +object(self) + val mutable proofw_ref = None + val mutable compute_ref = None + method proofw = + Lazy.force self#compute ; + match proofw_ref with + None -> assert false + | Some proofw -> proofw method content = vbox1 + method compute = + match compute_ref with + None -> assert false + | Some compute -> compute initializer - ignore(exactb#connect#clicked exact) ; - ignore(applyb#connect#clicked apply) ; - ignore(elimsimplintrosb#connect#clicked elimsimplintros) ; - 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(cutb#connect#clicked cut) ; - ignore(changeb#connect#clicked change) ; - ignore(letinb#connect#clicked letin) ; - ignore(ringb#connect#clicked ring) ; - ignore(clearbodyb#connect#clicked clearbody) ; - ignore(clearb#connect#clicked clear) ; - ignore(fourierb#connect#clicked fourier) ; - ignore(rewritesimplb#connect#clicked rewritesimpl) ; - ignore(reflexivityb#connect#clicked reflexivity) ; - ignore(symmetryb#connect#clicked symmetry) ; - ignore(transitivityb#connect#clicked transitivity) ; - ignore(leftb#connect#clicked left) ; - ignore(rightb#connect#clicked right) ; - ignore(assumptionb#connect#clicked assumption) ; - ignore(introsb#connect#clicked intros) ; - initializer - ignore(proofw#connect#selection_changed (choose_selection proofw)) ; + compute_ref <- + Some (lazy ( + let scrolled_window1 = + GBin.scrolled_window ~border_width:10 + ~packing:(vbox1#pack ~expand:true ~padding:5) () in + let proofw = + GMathView.math_view ~width:400 ~height:275 + ~packing:(scrolled_window1#add) () in + let _ = proofw_ref <- Some proofw in + let hbox3 = + GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in + let exactb = + GButton.button ~label:"Exact" + ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in + let introsb = + GButton.button ~label:"Intros" + ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in + let applyb = + GButton.button ~label:"Apply" + ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in + let elimsimplintrosb = + GButton.button ~label:"ElimSimplIntros" + ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in + let elimtypeb = + GButton.button ~label:"ElimType" + ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in + let whdb = + GButton.button ~label:"Whd" + ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in + let reduceb = + GButton.button ~label:"Reduce" + ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in + 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" + ~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 changeb = + GButton.button ~label:"Change" + ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in + let letinb = + GButton.button ~label:"Let ... In" + ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in + let ringb = + GButton.button ~label:"Ring" + ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in + let clearbodyb = + GButton.button ~label:"ClearBody" + ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in + let clearb = + GButton.button ~label:"Clear" + ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in + let fourierb = + GButton.button ~label:"Fourier" + ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in + let rewritesimplb = + GButton.button ~label:"RewriteSimpl ->" + ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in + let 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 + 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 leftb = + GButton.button ~label:"Left" + ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in + let rightb = + GButton.button ~label:"Right" + ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in + let assumptionb = + GButton.button ~label:"Assumption" + ~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) ; + 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(cutb#connect#clicked cut) ; + ignore(changeb#connect#clicked change) ; + ignore(letinb#connect#clicked letin) ; + ignore(ringb#connect#clicked ring) ; + ignore(clearbodyb#connect#clicked clearbody) ; + ignore(clearb#connect#clicked clear) ; + ignore(fourierb#connect#clicked fourier) ; + ignore(rewritesimplb#connect#clicked rewritesimpl) ; + ignore(reflexivityb#connect#clicked reflexivity) ; + ignore(symmetryb#connect#clicked symmetry) ; + ignore(transitivityb#connect#clicked transitivity) ; + ignore(leftb#connect#clicked left) ; + ignore(rightb#connect#clicked right) ; + ignore(assumptionb#connect#clicked assumption) ; + ignore(introsb#connect#clicked intros) ; + ignore(proofw#connect#selection_changed (choose_selection proofw)) ; + )) end ;; @@ -1950,7 +2014,7 @@ object(self) method notebook = notebook method add_page n = let new_page = new page () in - pages := !pages @ [n,new_page] ; + pages := !pages @ [n,lazy (setgoal n),new_page] ; notebook#append_page ~tab_label:((GMisc.label ~text:("?" ^ string_of_int n) ())#coerce) new_page#content#coerce @@ -1958,14 +2022,15 @@ object(self) List.iter (function _ -> notebook#remove_page 0) !pages ; pages := [] ; method set_current_page n = - let (_,page) = List.find (function (m,_) -> m=n) !pages in + let (_,_,page) = List.find (function (m,_,_) -> m=n) !pages in let new_page = notebook#page_num page#content#coerce in if new_page <> notebook#current_page then skip_switch_page_event <- true ; notebook#goto_page new_page method set_empty_page = self#add_page (-1) method proofw = - (snd (List.nth !pages notebook#current_page))#proofw + let (_,_,page) = List.nth !pages notebook#current_page in + page#proofw initializer ignore (notebook#connect#switch_page @@ -1974,8 +2039,9 @@ object(self) skip_switch_page_event <- false ; if not skip then try - let metano = fst (List.nth !pages i) in - setgoal metano + let (_,setgoal,page) = List.nth !pages i in + Lazy.force (page#compute) ; + Lazy.force setgoal with _ -> () )) end -- 2.39.2