(* 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
- ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
- ) uris_and_terms) ;
- window#show ()
+ mmlwidget#load_tree ~dom:mml
+ with
+ e ->
+ output_html outputhtml
+ ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
+ )
+ ) uris
+ in
+ ignore
+ (notebook#connect#switch_page
+ (function i -> Lazy.force (List.nth render_terms i)))
;;
exception NoChoice;;
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
(* 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) ;
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 *)
| _ ->
interactive_user_uri_choice
~selection_mode:`EXTENDED
- ~ok:"Try all the sections."
+ ~ok:"Try every selection."
~title:"Ambiguous input."
~msg:
("Ambiguous input \"" ^ id ^
in
aux dom' list_of_uris
in
-prerr_endline ("##### NE DISAMBIGUO: " ^ string_of_int (List.length resolve_ids)) ;
+ output_html (outputhtml ())
+ ("<h1>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 =
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'
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
;;
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
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
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
projects / helm.git / commitdiff