+
+(* MISC FUNCTIONS *)
+
+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')
+ 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)
+ )
+;;
+
+let term_of_cic_textual_parser_uri uri =
+ let module C = Cic in
+ let module CTP = CicTextualParser0 in
+ match uri with
+ CTP.ConUri uri -> C.Const (uri,[])
+ | CTP.VarUri uri -> C.Var (uri,[])
+ | CTP.IndTyUri (uri,tyno) -> C.MutInd (uri,tyno,[])
+ | CTP.IndConUri (uri,tyno,consno) -> C.MutConstruct (uri,tyno,consno,[])
+;;
+
+let string_of_cic_textual_parser_uri uri =
+ let module C = Cic in
+ let module CTP = CicTextualParser0 in
+ let uri' =
+ match uri with
+ CTP.ConUri uri -> UriManager.string_of_uri uri
+ | CTP.VarUri uri -> UriManager.string_of_uri uri
+ | CTP.IndTyUri (uri,tyno) ->
+ UriManager.string_of_uri uri ^ "#1/" ^ string_of_int (tyno + 1)
+ | CTP.IndConUri (uri,tyno,consno) ->
+ UriManager.string_of_uri uri ^ "#1/" ^ string_of_int (tyno + 1) ^ "/" ^
+ string_of_int consno
+ in
+ (* 4 = String.length "cic:" *)
+ String.sub uri' 4 (String.length uri' - 4)
+;;
+
+let output_html outputhtml msg =
+ htmlheader_and_content := !htmlheader_and_content ^ msg ;
+ outputhtml#source (!htmlheader_and_content ^ htmlfooter) ;
+ outputhtml#set_topline (-1)
+;;
+
+(* UTILITY FUNCTIONS TO DISAMBIGUATE AN URI *)
+
+(* Check window *)
+
+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
+ window#show () ;
+ let render_terms =
+ List.map
+ (function uri ->
+ let scrolled_window =
+ GBin.scrolled_window ~border_width:10
+ ~packing:
+ (notebook#append_page ~tab_label:((GMisc.label ~text:uri ())#coerce))
+ ()
+ 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
+ in
+ ignore
+ (notebook#connect#switch_page
+ (function i -> Lazy.force (List.nth render_terms i)))
+;;
+
+exception NoChoice;;
+
+let
+ interactive_user_uri_choice ~selection_mode ?(ok="Ok") ~title ~msg uris
+=
+ let choices = ref [] in
+ let chosen = ref false in
+ let window =
+ GWindow.dialog ~modal:true ~title ~width:600 () in
+ let lMessage =
+ GMisc.label ~text:msg
+ ~packing:(window#vbox#pack ~expand:false ~fill:false ~padding:5) () in
+ let scrolled_window =
+ GBin.scrolled_window ~border_width:10
+ ~packing:(window#vbox#pack ~expand:true ~fill:true ~padding:5) () in
+ let clist =
+ 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
+ let _ = List.map (function x -> clist#append [x]) uris in
+ let hbox2 =
+ GPack.hbox ~border_width:0
+ ~packing:(window#vbox#pack ~expand:false ~fill:false ~padding:5) () in
+ let explain_label =
+ GMisc.label ~text:"None of the above. Try this one:"
+ ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5) () in
+ let manual_input =
+ GEdit.entry ~editable:true
+ ~packing:(hbox2#pack ~expand:true ~fill:true ~padding:5) () in
+ let hbox =
+ GPack.hbox ~border_width:0 ~packing:window#action_area#add () 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 checkb =
+ GButton.button ~label:"Check"
+ ~packing:(hbox#pack ~padding:5) () in
+ let _ = checkb#misc#set_sensitive false in
+ let cancelb =
+ GButton.button ~label:"Abort"
+ ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
+ (* actions *)
+ let check_callback () =
+ assert (List.length !choices > 0) ;
+ check_window (outputhtml ()) !choices
+ in
+ ignore (window#connect#destroy GMain.Main.quit) ;
+ ignore (cancelb#connect#clicked window#destroy) ;
+ ignore
+ (okb#connect#clicked (function () -> chosen := true ; window#destroy ())) ;
+ ignore (checkb#connect#clicked check_callback) ;
+ ignore
+ (clist#connect#select_row
+ (fun ~row ~column ~event ->
+ checkb#misc#set_sensitive true ;
+ okb#misc#set_sensitive true ;
+ choices := (List.nth uris row)::!choices)) ;
+ ignore
+ (clist#connect#unselect_row
+ (fun ~row ~column ~event ->
+ choices :=
+ List.filter (function uri -> uri != (List.nth uris row)) !choices)) ;
+ ignore
+ (manual_input#connect#changed
+ (fun _ ->
+ if manual_input#text = "" then
+ begin
+ choices := [] ;
+ checkb#misc#set_sensitive false ;
+ okb#misc#set_sensitive false ;
+ clist#misc#set_sensitive true
+ end
+ else
+ begin
+ choices := [manual_input#text] ;
+ clist#unselect_all () ;
+ checkb#misc#set_sensitive true ;
+ okb#misc#set_sensitive true ;
+ clist#misc#set_sensitive false
+ end));
+ window#set_position `CENTER ;
+ window#show () ;
+ GMain.Main.main () ;
+ 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
+;;
+