+ Not_found -> empty_id_to_uris
+ in
+ aux 0
+ in
+ id_to_uris := dom,resolve_id
+;;
+
+let proveit () =
+ let module L = LogicalOperations in
+ let module G = Gdome in
+ let notebook = (rendering_window ())#notebook in
+ let output = (rendering_window ())#output in
+ let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
+ match (rendering_window ())#output#get_selection with
+ Some node ->
+ let xpath =
+ ((node : Gdome.element)#getAttributeNS
+ (*CSC: OCAML DIVERGE
+ ((element : G.element)#getAttributeNS
+ *)
+ ~namespaceURI:helmns
+ ~localName:(G.domString "xref"))#to_string
+ in
+ if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
+ else
+ begin
+ try
+ match !current_cic_infos with
+ Some (ids_to_terms, ids_to_father_ids, _, _) ->
+ let id = xpath in
+ L.to_sequent id ids_to_terms ids_to_father_ids ;
+ refresh_proof output ;
+ refresh_sequent notebook
+ | None -> assert false (* "ERROR: No current term!!!" *)
+ with
+ RefreshSequentException e ->
+ output_html outputhtml
+ ("<h1 color=\"red\">Exception raised during the refresh of the " ^
+ "sequent: " ^ Printexc.to_string e ^ "</h1>")
+ | RefreshProofException e ->
+ output_html outputhtml
+ ("<h1 color=\"red\">Exception raised during the refresh of the " ^
+ "proof: " ^ Printexc.to_string e ^ "</h1>")
+ | e ->
+ output_html outputhtml
+ ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
+ end
+ | None -> assert false (* "ERROR: No selection!!!" *)
+;;
+
+let focus () =
+ let module L = LogicalOperations in
+ let module G = Gdome in
+ let notebook = (rendering_window ())#notebook in
+ let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
+ match (rendering_window ())#output#get_selection with
+ Some node ->
+ let xpath =
+ ((node : Gdome.element)#getAttributeNS
+ (*CSC: OCAML DIVERGE
+ ((element : G.element)#getAttributeNS
+ *)
+ ~namespaceURI:helmns
+ ~localName:(G.domString "xref"))#to_string
+ in
+ if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
+ else
+ begin
+ try
+ match !current_cic_infos with
+ Some (ids_to_terms, ids_to_father_ids, _, _) ->
+ let id = xpath in
+ L.focus id ids_to_terms ids_to_father_ids ;
+ refresh_sequent notebook
+ | None -> assert false (* "ERROR: No current term!!!" *)
+ with
+ RefreshSequentException e ->
+ output_html outputhtml
+ ("<h1 color=\"red\">Exception raised during the refresh of the " ^
+ "sequent: " ^ Printexc.to_string e ^ "</h1>")
+ | RefreshProofException e ->
+ output_html outputhtml
+ ("<h1 color=\"red\">Exception raised during the refresh of the " ^
+ "proof: " ^ Printexc.to_string e ^ "</h1>")
+ | e ->
+ output_html outputhtml
+ ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
+ end
+ | None -> assert false (* "ERROR: No selection!!!" *)
+;;
+
+exception NoPrevGoal;;
+exception NoNextGoal;;
+
+let setgoal metano =
+ let module L = LogicalOperations in
+ let module G = Gdome in
+ let notebook = (rendering_window ())#notebook in
+ let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
+ let metasenv =
+ match !ProofEngine.proof with
+ None -> assert false
+ | Some (_,metasenv,_,_) -> metasenv
+ in
+ try
+ refresh_sequent ~empty_notebook:false notebook
+ with
+ RefreshSequentException e ->
+ output_html outputhtml
+ ("<h1 color=\"red\">Exception raised during the refresh of the " ^
+ "sequent: " ^ Printexc.to_string e ^ "</h1>")
+ | e ->
+ output_html outputhtml
+ ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
+;;
+
+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 =
+ GBin.scrolled_window ~border_width:10 ~packing:window#add () in
+ let mmlwidget =
+ GMathView.math_view ~packing:scrolled_window#add ~width:600 ~height:400 () in
+ let _ = window#event#connect#delete (fun _ -> window#misc#hide () ; true ) in
+ let href = Gdome.domString "href" in
+ let show_in_show_window_obj uri obj =
+ let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
+ try
+ let
+ (acic,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,
+ ids_to_inner_types,ids_to_conjectures,ids_to_hypotheses)
+ =
+ Cic2acic.acic_object_of_cic_object obj
+ in
+ let mml =
+ mml_of_cic_object ~explode_all:false uri acic ids_to_inner_sorts
+ ids_to_inner_types
+ in
+ window#set_title (UriManager.string_of_uri uri) ;
+ window#misc#hide () ; window#show () ;
+ mmlwidget#load_tree mml ;
+ with
+ e ->
+ output_html outputhtml
+ ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
+ 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_uri (UriManager.uri_of_string uri)
+ else
+ if mmlwidget#get_action <> None then
+ mmlwidget#action_toggle
+ in
+ let _ =
+ mmlwidget#connect#clicked (show_in_show_window_callback mmlwidget)
+ in
+ show_in_show_window_obj, show_in_show_window_uri,
+ show_in_show_window_callback
+;;
+
+exception NoObjectsLocated;;
+
+let user_uri_choice ~title ~msg uris =
+ let uri =
+ match uris with
+ [] -> raise NoObjectsLocated
+ | [uri] -> uri
+ | uris ->
+ match
+ interactive_user_uri_choice ~selection_mode:`SINGLE ~title ~msg uris
+ with
+ [uri] -> uri
+ | _ -> assert false
+ in
+ String.sub uri 4 (String.length uri - 4)
+;;
+
+let locate_callback id =
+ let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
+ let result = MQueryGenerator.locate id in
+ let uris =
+ List.map
+ (function uri,_ -> wrong_xpointer_format_from_wrong_xpointer_format' uri)
+ result in
+ let html =
+ (" <h1>Locate Query: </h1><pre>" ^ get_last_query result ^ "</pre>")
+ in
+ output_html outputhtml html ;
+ user_uri_choice ~title:"Ambiguous input."
+ ~msg:
+ ("Ambiguous input \"" ^ id ^
+ "\". Please, choose one interpetation:")
+ uris
+;;
+
+let locate () =
+ let inputt = ((rendering_window ())#inputt : term_editor) in
+ let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
+ try
+ match
+ GToolbox.input_string ~title:"Locate" "Enter an identifier to locate:"
+ with
+ None -> raise NoChoice
+ | Some input ->
+ let uri = locate_callback input in
+ inputt#set_term uri
+ with
+ e ->
+ output_html outputhtml
+ ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
+;;
+
+let input_or_locate_uri ~title =
+ let uri = ref None in
+ let window =
+ GWindow.window
+ ~width:400 ~modal:true ~title ~border_width:2 () in
+ let vbox = GPack.vbox ~packing:window#add () in
+ let hbox1 =
+ GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
+ let _ =
+ GMisc.label ~text:"Enter a valid URI:" ~packing:(hbox1#pack ~padding:5) () in
+ let manual_input =
+ GEdit.entry ~editable:true
+ ~packing:(hbox1#pack ~expand:true ~fill:true ~padding:5) () in
+ let checkb =
+ GButton.button ~label:"Check"
+ ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
+ let _ = checkb#misc#set_sensitive false in
+ let hbox2 =
+ GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
+ let _ =
+ GMisc.label ~text:"You can also enter an indentifier to locate:"
+ ~packing:(hbox2#pack ~padding:5) () in
+ let locate_input =
+ GEdit.entry ~editable:true
+ ~packing:(hbox2#pack ~expand:true ~fill:true ~padding:5) () in
+ let locateb =
+ GButton.button ~label:"Locate"
+ ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5) () in
+ let _ = locateb#misc#set_sensitive false in
+ let hbox3 =
+ GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
+ let okb =
+ GButton.button ~label:"Ok"
+ ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
+ let _ = okb#misc#set_sensitive false in
+ let cancelb =
+ GButton.button ~label:"Cancel"
+ ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) ()
+ in
+ ignore (window#connect#destroy GMain.Main.quit) ;
+ ignore
+ (cancelb#connect#clicked (function () -> uri := None ; window#destroy ())) ;
+ let check_callback () =
+ let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
+ let uri = "cic:" ^ manual_input#text in
+ try
+ ignore (Getter.resolve (UriManager.uri_of_string uri)) ;
+ output_html outputhtml "<h1 color=\"Green\">OK</h1>" ;
+ true
+ with
+ Getter.Unresolved ->
+ output_html outputhtml
+ ("<h1 color=\"Red\">URI " ^ uri ^
+ " does not correspond to any object.</h1>") ;
+ false
+ | UriManager.IllFormedUri _ ->
+ output_html outputhtml
+ ("<h1 color=\"Red\">URI " ^ uri ^ " is not well-formed.</h1>") ;
+ false
+ | e ->
+ output_html outputhtml
+ ("<h1 color=\"Red\">" ^ Printexc.to_string e ^ "</h1>") ;
+ false
+ in
+ ignore
+ (okb#connect#clicked
+ (function () ->
+ if check_callback () then
+ begin
+ uri := Some manual_input#text ;
+ window#destroy ()
+ end
+ )) ;
+ ignore (checkb#connect#clicked (function () -> ignore (check_callback ()))) ;
+ ignore
+ (manual_input#connect#changed
+ (fun _ ->
+ if manual_input#text = "" then
+ begin
+ checkb#misc#set_sensitive false ;
+ okb#misc#set_sensitive false
+ end
+ else
+ begin
+ checkb#misc#set_sensitive true ;
+ okb#misc#set_sensitive true
+ end));
+ ignore
+ (locate_input#connect#changed
+ (fun _ -> locateb#misc#set_sensitive (locate_input#text <> ""))) ;
+ ignore
+ (locateb#connect#clicked
+ (function () ->
+ let id = locate_input#text in
+ manual_input#set_text (locate_callback id) ;
+ locate_input#delete_text 0 (String.length id)
+ )) ;
+ window#show () ;
+ GMain.Main.main () ;
+ match !uri with
+ None -> raise NoChoice
+ | Some uri -> UriManager.uri_of_string ("cic:" ^ uri)
+;;
+
+let locate_one_id id =
+ let result = MQueryGenerator.locate id in
+ let uris =
+ List.map
+ (function uri,_ ->
+ wrong_xpointer_format_from_wrong_xpointer_format' uri
+ ) result in
+ let html= " <h1>Locate Query: </h1><pre>" ^ get_last_query result ^ "</pre>" in
+ output_html (rendering_window ())#outputhtml html ;
+ let uris' =
+ match uris with
+ [] ->
+ [UriManager.string_of_uri
+ (input_or_locate_uri ~title:("URI matching \"" ^ id ^ "\" unknown."))]
+ | [uri] -> [uri]
+ | _ ->
+ interactive_user_uri_choice
+ ~selection_mode:`EXTENDED
+ ~ok:"Try every selection."
+ ~enable_button_for_non_vars:true
+ ~title:"Ambiguous input."
+ ~msg:
+ ("Ambiguous input \"" ^ id ^
+ "\". Please, choose one or more interpretations:")
+ uris
+ in
+ List.map cic_textual_parser_uri_of_string uris'
+;;
+
+exception ThereDoesNotExistAnyWellTypedInterpretationOfTheInput;;
+exception AmbiguousInput;;
+
+let disambiguate_input context metasenv dom mk_metasenv_and_expr =
+ let known_ids,resolve_id = !id_to_uris in
+ let dom' =
+ let rec filter =
+ function
+ [] -> []
+ | he::tl ->
+ if List.mem he known_ids then filter tl else he::(filter tl)
+ in
+ filter dom
+ in
+ (* for each id in dom' we get the list of uris associated to it *)
+ let list_of_uris = List.map locate_one_id dom' in
+ (* and now we compute the list of all possible assignments from id to uris *)
+ let resolve_ids =
+ let rec aux ids list_of_uris =
+ match ids,list_of_uris with
+ [],[] -> [resolve_id]
+ | id::idtl,uris::uristl ->
+ let resolves = aux idtl uristl in
+ List.concat
+ (List.map
+ (function uri ->
+ List.map
+ (function f ->
+ function id' -> if id = id' then Some uri else f id'
+ ) resolves
+ ) uris
+ )
+ | _,_ -> assert false
+ in
+ aux dom' list_of_uris
+ in
+ let tests_no = List.length resolve_ids in
+ if tests_no > 1 then
+ output_html (outputhtml ())
+ ("<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 =
+ function
+ [] -> []
+ | resolve::tl ->
+ let metasenv',expr = mk_metasenv_and_expr resolve in
+ try
+(*CSC: Bug here: we do not try to typecheck also the metasenv' *)
+ ignore
+ (CicTypeChecker.type_of_aux' metasenv context expr) ;
+ resolve::(filter tl)
+ with
+ _ -> filter tl
+ in
+ filter resolve_ids
+ in
+ let resolve_id' =
+ match resolve_ids' with
+ [] -> raise ThereDoesNotExistAnyWellTypedInterpretationOfTheInput
+ | [resolve_id] -> resolve_id
+ | _ ->
+ let choices =
+ List.map
+ (function resolve ->
+ List.map
+ (function id ->
+ id,
+ match resolve id with
+ None -> assert false
+ | Some uri ->
+ match uri with
+ CicTextualParser0.ConUri uri
+ | CicTextualParser0.VarUri uri ->
+ UriManager.string_of_uri uri
+ | CicTextualParser0.IndTyUri (uri,tyno) ->
+ UriManager.string_of_uri uri ^ "#xpointer(1/" ^
+ string_of_int (tyno+1) ^ ")"
+ | CicTextualParser0.IndConUri (uri,tyno,consno) ->
+ UriManager.string_of_uri uri ^ "#xpointer(1/" ^
+ string_of_int (tyno+1) ^ "/" ^ string_of_int consno ^ ")"
+ ) dom
+ ) resolve_ids'
+ in
+ let index = interactive_interpretation_choice choices in
+ List.nth resolve_ids' index
+ in
+ id_to_uris := known_ids @ dom', resolve_id' ;
+ mk_metasenv_and_expr resolve_id'
+;;
+
+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 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
+ ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
+ ))
+ (* 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