* MA 02111-1307, USA.
*
* For details, see the HELM World-Wide-Web page,
- * http://cs.unibo.it/helm/.
+ * http://helm.cs.unibo.it/
*)
-(******************************************************************************)
-(* *)
-(* PROJECT HELM *)
-(* *)
-(* Claudio Sacerdoti Coen <sacerdot@cs.unibo.it> *)
-(* 06/01/2002 *)
-(* *)
-(* *)
-(******************************************************************************)
+(*****************************************************************************)
+(* *)
+(* PROJECT HELM *)
+(* *)
+(* Claudio Sacerdoti Coen <sacerdot@cs.unibo.it> *)
+(* 06/01/2002 *)
+(* *)
+(* *)
+(*****************************************************************************)
let debug_level = ref 1
let debug_print ?(level = 1) s = if !debug_level >= level then prerr_endline s
+let error s = prerr_endline ("E: " ^ s)
+let warning s = prerr_endline ("W: " ^ s)
open Printf
-(* DEBUGGING *)
-
module MQI = MQueryInterpreter
module MQIC = MQIConn
module MQGT = MQGTypes
module MQGU = MQGUtil
module MQG = MQueryGenerator
-(* GLOBAL CONSTANTS *)
-
-let mqi_debug_fun s = debug_print ~level:2 s
-let mqi_flags = [MQIC.Postgres ; MQIC.Stat ; MQIC.Warn ; MQIC.Log]
-let mqi_handle = MQIC.init mqi_flags mqi_debug_fun
-
-let xlinkns = Gdome.domString "http://www.w3.org/1999/xlink";;
-
-let prooffile =
- try
- Sys.getenv "GTOPLEVEL_PROOFFILE"
- with
- Not_found -> "/public/currentproof"
+(* first of all let's initialize the Helm_registry *)
+let _ =
+ let configuration_file = "gTopLevel.conf.xml" in
+ if not (Sys.file_exists configuration_file) then begin
+ eprintf "E: Can't find configuration file '%s'\n" configuration_file;
+ exit 2
+ end;
+ Helm_registry.load_from configuration_file
;;
-let prooffiletype =
- try
- Sys.getenv "GTOPLEVEL_PROOFFILETYPE"
- with
- Not_found -> "/public/currentprooftype"
-;;
+(* GLOBAL CONSTANTS *)
-let environmentfile =
- try
- Sys.getenv "GTOPLEVEL_ENVIRONMENTFILE"
- with
- Not_found -> "/public/environment"
-;;
+let mqi_handle = MQIC.init_if_connected ()
+
+let dbd =
+ Mysql.quick_connect
+ ~host:(Helm_registry.get "db.host")
+ ~user:(Helm_registry.get "db.user")
+ ~database:(Helm_registry.get "db.database")
+ ()
let restore_environment_on_boot = true ;;
let notify_hbugs_on_goal_change = false ;;
)
;;
-exception OutputHtmlNotInitialized;;
-
-let set_outputhtml,outputhtml =
- let outputhtml_ref = ref None in
- (function (rw: Ui_logger.html_logger) -> outputhtml_ref := Some rw),
- (function () ->
- match !outputhtml_ref with
- | None -> raise OutputHtmlNotInitialized
- | Some outputhtml -> (outputhtml: Ui_logger.html_logger)
- )
-;;
-
exception QedSetSensitiveNotInitialized;;
let qed_set_sensitive =
ref (function _ -> raise QedSetSensitiveNotInitialized)
in
Arg.parse argspec ignore ""
-(* MISC FUNCTIONS *)
-
-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 ?(append_NL = true) (outputhtml: Ui_logger.html_logger) =
- outputhtml#log ~append_NL
-
(* UTILITY FUNCTIONS TO DISAMBIGUATE AN URI *)
(* Check window *)
-let check_window (outputhtml: Ui_logger.html_logger) uris =
+let check_window uris =
let window =
GWindow.window
~width:800 ~modal:true ~title:"Check" ~border_width:2 () in
lazy
(let mmlwidget =
TermViewer.sequent_viewer
+ ~mml_of_cic_sequent:ApplyTransformation.mml_of_cic_sequent
~packing:scrolled_window#add ~width:400 ~height:280 () in
let expr =
- let term =
- term_of_cic_textual_parser_uri
- (MQueryMisc.cic_textual_parser_uri_of_string uri)
- in
- (Cic.Cast (term, CicTypeChecker.type_of_aux' [] [] term))
+ let term = CicUtil.term_of_uri uri in
+ (Cic.Cast (term, fst(CicTypeChecker.type_of_aux' [] [] term
+ CicUniv.empty_ugraph )))
in
try
mmlwidget#load_sequent [] (111,[],expr)
with
e ->
- output_html outputhtml (`Error (`T (Printexc.to_string e)))
+ HelmLogger.log (`Error (`T (Printexc.to_string e)))
)
) uris
in
exception NoChoice;;
-let
- interactive_user_uri_choice ~(selection_mode:[`MULTIPLE|`SINGLE]) ?(ok="Ok")
- ?(enable_button_for_non_vars=false) ~title ~msg uris
+let interactive_user_uri_choice
+ ~(selection_mode:[ `SINGLE | `MULTIPLE ])
+ ?(ok="Ok") ?(enable_button_for_non_vars=false) ~title ~msg uris
=
let only_constant_choices =
lazy
(fun uri -> not (String.sub uri (String.length uri - 4) 4 = ".var"))
uris)
in
- if !auto_disambiguation then
+ if selection_mode <> `SINGLE && !auto_disambiguation then
Lazy.force only_constant_choices
else begin
let choices = ref [] in
(* actions *)
let check_callback () =
assert (List.length !choices > 0) ;
- check_window (outputhtml ()) !choices
+ check_window !choices
in
ignore (window#connect#destroy GMain.Main.quit) ;
ignore (cancelb#connect#clicked window#destroy) ;
GtkThread.main ();
match !chosen with
None -> raise NoChoice
- | Some n -> n
+ | Some n -> [n]
;;
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 ^
+ Xml.pp ~gzip:false xmlinnertypes (Some (path ^ ".types.xml")) ;
+ Http_getter.register' innertypesuri
+ (Helm_registry.get "local_library.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 ^
+ Xml.pp ~gzip:false xml (Some (path ^ ".xml")) ;
+ Http_getter.register' uri
+ (Helm_registry.get "local_library.url" ^
Str.replace_first (Str.regexp "^cic:") ""
(UriManager.string_of_uri uri) ^ ".xml"
) ;
None -> assert false
| Some bodyuri -> bodyuri
in
- Xml.pp ~quiet:true bodyxml' (Some (path ^ ".body.xml")) ;
- Getter.register bodyuri
- (Configuration.annotations_url ^
+ Xml.pp ~gzip:false bodyxml' (Some (path ^ ".body.xml")) ;
+ Http_getter.register' bodyuri
+ (Helm_registry.get "local_library.url" ^
Str.replace_first (Str.regexp "^cic:") ""
(UriManager.string_of_uri bodyuri) ^ ".xml"
)
exception WrongProof;;
let pathname_of_annuri uristring =
- Configuration.annotations_dir ^
+ Helm_registry.get "local_library.dir" ^
Str.replace_first (Str.regexp "^cic:") "" uristring
;;
;;
let qed () =
- match ProofEngine.get_proof () with
- None -> assert false
- | Some (uri,[],bo,ty) ->
- if
- CicReduction.are_convertible []
- (CicTypeChecker.type_of_aux' [] [] bo) ty
- then
- begin
- (*CSC: Wrong: [] is just plainly wrong *)
- let proof = Cic.Constant (UriManager.name_of_uri uri,Some bo,ty,[]) in
- let (acic,ids_to_inner_types,ids_to_inner_sorts) =
- (rendering_window ())#output#load_proof uri proof
- in
- !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
- end
- else
- raise WrongProof
- | _ -> raise OpenConjecturesStillThere
+ match ProofEngine.get_proof () with
+ None -> assert false
+ | Some (uri,[],bo,ty) ->
+ let uri = match uri with Some uri -> uri | _ -> assert false in
+ (* we want to typecheck in the ENV *)
+ prerr_endline "-------------> QED";
+ let ty_bo,u =
+ CicTypeChecker.type_of_aux' [] [] bo CicUniv.empty_ugraph in
+ let b,u1 = CicReduction.are_convertible [] ty_bo ty u in
+ if b then
+ begin
+ (*CSC: Wrong: [] is just plainly wrong *)
+ let proof =
+ Cic.Constant (UriManager.name_of_uri uri,Some bo,ty,[],[])
+ in
+ let (acic,ids_to_inner_types,ids_to_inner_sorts) =
+ (rendering_window ())#output#load_proof proof
+ in
+ !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
+ let list_of_universes =
+ CicUnivUtils.universes_of_obj uri
+ (Cic.Constant ("",None,ty,[],[]))
+ in
+ let u1_clean = CicUniv.clean_ugraph u1 list_of_universes in
+ let u2 = CicUniv.fill_empty_nodes_with_uri u1_clean uri in
+ (**********************************************
+ TASSI: to uncomment whe universes will be ON
+ ***********************************************)
+ (*
+ make_dirs pathname ;
+ save_object_to_disk uri acic ids_to_inner_sorts
+ ids_to_inner_types pathname;
+ *)
+ (* save the universe graph u2 *)
+ (* add the object to the env *)
+ CicEnvironment.add_type_checked_term uri ((
+ Cic.Constant ((UriManager.name_of_uri uri),
+ (Some bo),ty,[],[])),u2);
+ (* FIXME: the variable list!! *)
+ prerr_endline "-------------> FINE";
+ end
+ else
+ raise WrongProof
+ | _ -> raise OpenConjecturesStillThere
;;
(** save an unfinished proof on the filesystem *)
let save_unfinished_proof () =
- let outputhtml = ((rendering_window ())#outputhtml(* : GHtml.xmhtml*)) in
let (xml, bodyxml) = ProofEngine.get_current_status_as_xml () in
- Xml.pp ~quiet:true xml (Some prooffiletype) ;
- output_html outputhtml
- (`Msg (`T ("Current proof type saved to " ^ prooffiletype))) ;
- Xml.pp ~quiet:true bodyxml (Some prooffile) ;
- output_html outputhtml
- (`Msg (`T ("Current proof body saved to " ^ prooffile)))
+ let proof_file_type = Helm_registry.get "gtoplevel.proof_file_type" in
+ let proof_file = Helm_registry.get "gtoplevel.proof_file" in
+ Xml.pp ~gzip:false xml (Some proof_file_type) ;
+ HelmLogger.log
+ (`Msg (`T ("Current proof type saved to " ^ proof_file_type))) ;
+ Xml.pp ~gzip:false bodyxml (Some proof_file) ;
+ HelmLogger.log
+ (`Msg (`T ("Current proof body saved to " ^ proof_file)))
;;
(* Used to typecheck the loaded proofs *)
ignore (
List.fold_left
(fun metasenv ((_,context,ty) as conj) ->
- ignore (T.type_of_aux' metasenv context ty) ;
+ ignore (T.type_of_aux' metasenv context ty CicUniv.empty_ugraph) ;
metasenv @ [conj]
) [] metasenv) ;
- ignore (T.type_of_aux' metasenv [] ty) ;
- ignore (T.type_of_aux' metasenv [] bo)
+ ignore (T.type_of_aux' metasenv [] ty CicUniv.empty_ugraph) ;
+ ignore (T.type_of_aux' metasenv [] bo CicUniv.empty_ugraph)
;;
let decompose_uris_choice_callback uris =
let module U = UriManager in
List.map
(function uri ->
- match MQueryMisc.cic_textual_parser_uri_of_string uri with
- CicTextualParser0.IndTyUri (uri,typeno) -> (uri,typeno,[])
- | _ -> assert false)
+ match CicUtil.term_of_uri uri with
+ | Cic.MutInd (uri, typeno, _) -> (uri, typeno, [])
+ | _ -> assert false)
(interactive_user_uri_choice
~selection_mode:`MULTIPLE ~ok:"Ok" ~enable_button_for_non_vars:false
~title:"Decompose" ~msg:"Please, select the Inductive Types to decompose"
let mk_fresh_name_callback metasenv context name ~typ =
let fresh_name =
- match FreshNamesGenerator.mk_fresh_name metasenv context name ~typ with
+ match FreshNamesGenerator.mk_fresh_name ~subst:[] metasenv context name ~typ with
Cic.Name fresh_name -> fresh_name
| Cic.Anonymous -> assert false
in
else
Hbugs.notify () ;
(*CSC: Wrong: [] is just plainly wrong *)
- uri,
- (Cic.CurrentProof (UriManager.name_of_uri uri, metasenv, bo, ty, []))
+ let uri = match uri with Some uri -> uri | _ -> assert false in
+ (uri,
+ Cic.CurrentProof (UriManager.name_of_uri uri,metasenv,bo,ty,[],[]))
in
- ignore (output#load_proof uri currentproof)
+ ignore (output#load_proof currentproof)
with
e ->
match ProofEngine.get_proof () with
None -> assert false
| Some (uri,metasenv,bo,ty) ->
- debug_print ("Offending proof: " ^ CicPp.ppobj (Cic.CurrentProof ("questa",metasenv,bo,ty,[])));
+ debug_print ("Offending proof: " ^
+ CicPp.ppobj (Cic.CurrentProof ("questa",metasenv,bo,ty,[],[])));
raise (InvokeTactics.RefreshProofException e)
let set_proof_engine_goal g =
begin
notebook#set_current_page
~may_skip_switch_page_event:true metano ;
- notebook#proofw#load_sequent metasenv currentsequent
+ notebook#proofw#load_sequent metasenv currentsequent ;
end
with
e ->
let decompose_uris_choice_callback = decompose_uris_choice_callback
let mk_fresh_name_callback = mk_fresh_name_callback
- let output_html msg = output_html (outputhtml ()) msg
+ let mqi_handle = mqi_handle
+ let dbd = dbd
end
;;
module InvokeTactics' = InvokeTactics.Make (InvokeTacticsCallbacks);;
module Ignore = Hbugs.Initialize (InvokeTactics');;
Hbugs.set_describe_hint_callback (fun hint ->
match hint with
- | Hbugs_types.Use_apply_Luke term ->
- let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
- check_window outputhtml [term]
+ | Hbugs_types.Use_apply_Luke term -> check_window [term]
| _ -> ())
;;
*)
(** load an unfinished proof from filesystem *)
let load_unfinished_proof () =
- let outputhtml = ((rendering_window ())#outputhtml(* : GHtml.xmhtml*)) in
let output = ((rendering_window ())#output : TermViewer.proof_viewer) in
let notebook = (rendering_window ())#notebook in
try
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,_) ->
+ let proof_file_type = Helm_registry.get "gtoplevel.proof_file_type" in
+ let proof_file = Helm_registry.get "gtoplevel.proof_file" in
+ match CicParser.obj_of_xml proof_file_type (Some proof_file) with
+ Cic.CurrentProof (_,metasenv,bo,ty,_,_) ->
typecheck_loaded_proof metasenv bo ty ;
- ProofEngine.set_proof (Some (uri, metasenv, bo, ty)) ;
+ ProofEngine.set_proof (Some (Some uri, metasenv, bo, ty));
refresh_proof output ;
set_proof_engine_goal
(match metasenv with
| (metano,_,_)::_ -> Some metano
) ;
refresh_goals notebook ;
- output_html outputhtml
- (`Msg (`T ("Current proof type loaded from " ^
- prooffiletype))) ;
- output_html outputhtml
- (`Msg (`T ("Current proof body loaded from " ^
- prooffile))) ;
+ HelmLogger.log
+ (`Msg (`T ("Current proof type loaded from " ^ proof_file_type)));
+ HelmLogger.log
+ (`Msg (`T ("Current proof body loaded from " ^ proof_file))) ;
!save_set_sensitive true;
| _ -> assert false
with
InvokeTactics.RefreshSequentException e ->
- output_html outputhtml
+ HelmLogger.log
(`Error (`T ("Exception raised during the refresh of the " ^
"sequent: " ^ Printexc.to_string e)))
| InvokeTactics.RefreshProofException e ->
- output_html outputhtml
+ HelmLogger.log
(`Error (`T ("Exception raised during the refresh of the " ^
"proof: " ^ Printexc.to_string e)))
| e ->
- output_html outputhtml
+ HelmLogger.log
(`Error (`T (Printexc.to_string e)))
;;
(try
DisambiguatingParser.EnvironmentP3.of_string raw_aliases
with e ->
- output_html (outputhtml ())
+ HelmLogger.log
(`Error (`T
("Error while parsing aliases: " ^ Printexc.to_string e)));
!disambiguation_env)
let module G = Gdome in
let notebook = (rendering_window ())#notebook in
let output = (rendering_window ())#output in
- let outputhtml = (rendering_window ())#outputhtml in
try
output#make_sequent_of_selected_term ;
refresh_proof output ;
refresh_goals notebook
with
InvokeTactics.RefreshSequentException e ->
- output_html outputhtml
+ HelmLogger.log
(`Error (`T ("Exception raised during the refresh of the " ^
"sequent: " ^ Printexc.to_string e)))
| InvokeTactics.RefreshProofException e ->
- output_html outputhtml
+ HelmLogger.log
(`Error (`T ("Exception raised during the refresh of the " ^
"proof: " ^ Printexc.to_string e)))
| e ->
- output_html outputhtml
+ HelmLogger.log
(`Error (`T (Printexc.to_string e)))
;;
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 output = (rendering_window ())#output in
try
output#focus_sequent_of_selected_term ;
refresh_goals notebook
with
InvokeTactics.RefreshSequentException e ->
- output_html outputhtml
+ HelmLogger.log
(`Error (`T ("Exception raised during the refresh of the " ^
"sequent: " ^ Printexc.to_string e)))
| InvokeTactics.RefreshProofException e ->
- output_html outputhtml
+ HelmLogger.log
(`Error (`T ("Exception raised during the refresh of the " ^
"proof: " ^ Printexc.to_string e)))
| e ->
- output_html outputhtml
+ HelmLogger.log
(`Error (`T (Printexc.to_string e)))
;;
let module G = Gdome in
let notebook = (rendering_window ())#notebook in
let output = (rendering_window ())#output in
- let outputhtml = (rendering_window ())#outputhtml in
let metasenv =
match ProofEngine.get_proof () with
None -> assert false
refresh_goals ~empty_notebook:false notebook
with
InvokeTactics.RefreshSequentException e ->
- output_html outputhtml
+ HelmLogger.log
(`Error (`T ("Exception raised during the refresh of the " ^
"sequent: " ^ Printexc.to_string e)))
| e ->
- output_html outputhtml
+ HelmLogger.log
(`Error (`T (Printexc.to_string e)))
;;
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 =
- ChosenTransformer.mml_of_cic_object
- ~explode_all:false uri acic ids_to_inner_sorts ids_to_inner_types
+ let mml,(_,(ids_to_terms,ids_to_father_ids,ids_to_conjectures,
+ ids_to_hypotheses,_,_)) =
+ ApplyTransformation.mml_of_cic_object obj
in
window#set_title (UriManager.string_of_uri uri) ;
window#misc#hide () ; window#show () ;
- mmlwidget#load_doc mml ;
+ mmlwidget#load_root mml#get_documentElement ;
with
e ->
- output_html outputhtml
+ HelmLogger.log
(`Error (`T (Printexc.to_string e)))
in
let show_in_show_window_uri uri =
- let obj = CicEnvironment.get_obj uri in
+ let obj,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
show_in_show_window_obj uri obj
in
- let show_in_show_window_callback mmlwidget (n : Gdome.element option) _ =
+ let show_in_show_window_callback mmlwidget ((n : Gdome.element option),_,_,_) =
match n with
None -> ()
| Some n' ->
- if n'#hasAttributeNS ~namespaceURI:xlinkns ~localName:href then
+ if n'#hasAttributeNS ~namespaceURI:Misc.xlink_ns ~localName:href then
let uri =
- (n'#getAttributeNS ~namespaceURI:xlinkns ~localName:href)#to_string
+ (n'#getAttributeNS ~namespaceURI:Misc.xlink_ns ~localName:href)#to_string
in
show_in_show_window_uri (UriManager.uri_of_string uri)
else
;;
let locate_callback id =
- let outputhtml = ((rendering_window ())#outputhtml(* : GHtml.xmhtml*)) in
- let out = output_html outputhtml in
- let query = MQG.locate id in
- let result = MQI.execute mqi_handle query in
- let uris =
- List.map
- (function uri,_ ->
- MQueryMisc.wrong_xpointer_format_from_wrong_xpointer_format' uri)
- result in
- out (`Msg (`T "Locate Query:")) ;
- MQueryUtil.text_of_query (fun m -> out (`Msg (`T m))) "" query;
- out (`Msg (`T "Result:")) ;
- MQueryUtil.text_of_result (fun m -> out (`Msg (`T m))) "" result;
+ let uris = MetadataQuery.locate ~dbd id in
+ HelmLogger.log (`Msg (`T ("Locate Query: " ^ id))) ;
+ HelmLogger.log (`Msg (`T "Result:")) ;
+ List.iter (fun uri -> HelmLogger.log (`Msg (`T uri))) uris;
user_uri_choice ~title:"Ambiguous input."
- ~msg:
- ("Ambiguous input \"" ^ id ^
- "\". Please, choose one interpetation:")
+ ~msg:(sprintf "Ambiguous input \"%s\". Please, choose one interpetation:" id)
uris
;;
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 (`Msg (`T "OK")) ;
+ ignore (Http_getter.resolve' (UriManager.uri_of_string uri)) ;
+ HelmLogger.log (`Msg (`T "OK")) ;
true
with
- Getter.Unresolved ->
- output_html outputhtml
+ Http_getter_types.Key_not_found _ ->
+ HelmLogger.log
(`Error (`T ("URI " ^ uri ^
" does not correspond to any object."))) ;
false
| UriManager.IllFormedUri _ ->
- output_html outputhtml
+ HelmLogger.log
(`Error (`T ("URI " ^ uri ^ " is not well-formed."))) ;
false
| e ->
- output_html outputhtml
+ HelmLogger.log
(`Error (`T (Printexc.to_string e))) ;
false
in
module DisambiguateCallbacks =
struct
- let output_html ?append_NL = output_html ?append_NL (outputhtml ())
let interactive_user_uri_choice =
fun ~selection_mode ?ok ?enable_button_for_non_vars ~title ~msg ~id ->
interactive_user_uri_choice ~selection_mode ?ok
?enable_button_for_non_vars ~title ~msg
let interactive_interpretation_choice = interactive_interpretation_choice
- let input_or_locate_uri = input_or_locate_uri
+ let input_or_locate_uri ~title ?id () = input_or_locate_uri ~title
end
;;
let locate () =
let inputt = ((rendering_window ())#inputt : TermEditor.term_editor) in
- let outputhtml = ((rendering_window ())#outputhtml(* : GHtml.xmhtml*)) in
try
match
GToolbox.input_string ~title:"Locate" "Enter an identifier to locate:"
inputt#set_term uri
with
e ->
- output_html outputhtml
+ HelmLogger.log
(`Error (`T (Printexc.to_string e)))
;;
let new_inductive () =
let inputt = ((rendering_window ())#inputt : TermEditor.term_editor) in
- let outputhtml = ((rendering_window ())#outputhtml(* : GHtml.xmhtml*)) in
let output = ((rendering_window ())#output : TermViewer.proof_viewer) in
let notebook = (rendering_window ())#notebook in
let uri = UriManager.uri_of_string (uristr ^ "/" ^ he ^ ".ind") in
begin
try
- ignore (Getter.resolve uri) ;
+ ignore (Http_getter.resolve' uri) ;
raise UriAlreadyInUse
- with
- Getter.Unresolved ->
+ with Http_getter_types.Key_not_found _ ->
get_uri := (function () -> uri) ;
get_names := (function () -> names) ;
inductive := inductiveb#active ;
end
with
e ->
- output_html outputhtml
+ HelmLogger.log
(`Error (`T (Printexc.to_string e)))
))
(* Second phase *)
~packing:(vbox#pack ~expand:true ~padding:0) () in
let newinputt =
TermEditor'.term_editor
- mqi_handle
+ ~dbd
~width:400 ~height:20 ~packing:scrolled_window#add
~share_environment_with:inputt ()
~isnotempty_callback:
(fun name (newinputt,cons_names_entry) ->
let consnamesstr = cons_names_entry#text in
let cons_names = Str.split (Str.regexp " +") consnamesstr in
- let metasenv,expr =
+ let metasenv,expr,ugraph =
newinputt#get_metasenv_and_term ~context:[] ~metasenv:[]
in
match metasenv with
window#destroy ()
with
e ->
- output_html outputhtml
+ HelmLogger.log
(`Error (`T (Printexc.to_string e)))
))
(* Third phase *)
~packing:(vbox#pack ~expand:true ~padding:0) () in
let newinputt =
TermEditor'.term_editor
- mqi_handle
+ ~dbd
~width:400 ~height:20 ~packing:scrolled_window#add
~share_environment_with:inputt ()
~isnotempty_callback:
let cons_types =
List.map2
(fun name inputt ->
- let metasenv,expr =
+ let metasenv,expr,ugraph =
inputt#get_metasenv_and_term ~context ~metasenv:[]
in
match metasenv with
window2#destroy ()
with
e ->
- output_html outputhtml
+ HelmLogger.log
(`Error (`T (Printexc.to_string e)))
)) ;
window2#show () ;
(*CSC: Da finire *)
let params = [] in
let tys = !get_types_and_cons () in
- let obj = Cic.InductiveDefinition(tys,params,!paramsno) in
- begin
- try
- debug_print (CicPp.ppobj obj);
- CicTypeChecker.typecheck_mutual_inductive_defs uri
- (tys,params,!paramsno) ;
- with
- e ->
- debug_print "Offending mutual (co)inductive type declaration:" ;
- debug_print (CicPp.ppobj obj) ;
- end ;
+ let obj = Cic.InductiveDefinition(tys,params,!paramsno,[]) in
+ let u =
+ begin
+ try
+ debug_print (CicPp.ppobj obj);
+ CicTypeChecker.typecheck_mutual_inductive_defs uri
+ (tys,params,!paramsno) CicUniv.empty_ugraph
+ with
+ e ->
+ debug_print "Offending mutual (co)inductive type declaration:" ;
+ debug_print (CicPp.ppobj obj) ;
+ (* I think we should fail here! *)
+ CicUniv.empty_ugraph
+ end
+ in
(* 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 ;
+
+ (* u should be cleaned before adding it to the env *)
+ CicEnvironment.put_inductive_definition uri (obj,u) ;
save_obj uri obj ;
+ (* TASSI: FIXME we should save the cleaned u here *)
show_in_show_window_obj uri obj
with
e ->
- output_html outputhtml
+ HelmLogger.log
(`Error (`T (Printexc.to_string e)))
;;
let new_proof () =
let inputt = ((rendering_window ())#inputt : TermEditor.term_editor) in
- let outputhtml = ((rendering_window ())#outputhtml(* : GHtml.xmhtml*)) in
let output = ((rendering_window ())#output : TermViewer.proof_viewer) in
let notebook = (rendering_window ())#notebook in
(* moved here to have visibility of the ok button *)
let newinputt =
TermEditor'.term_editor
- mqi_handle
+ ~dbd
~width:400 ~height:100 ~packing:scrolled_window#add
~share_environment_with:inputt ()
~isnotempty_callback:
(function () ->
chosen := true ;
try
- let metasenv,parsed = newinputt#get_metasenv_and_term [] [] in
+ let metasenv,parsed,ugraph = newinputt#get_metasenv_and_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
else
begin
try
- ignore (Getter.resolve uri) ;
+ ignore (Http_getter.resolve' uri) ;
raise UriAlreadyInUse
- with
- Getter.Unresolved ->
+ with Http_getter_types.Key_not_found _ ->
get_metasenv_and_term := (function () -> metasenv,parsed) ;
get_uri := (function () -> uri) ;
window#destroy ()
end
with
e ->
- output_html outputhtml
+ HelmLogger.log
(`Error (`T (Printexc.to_string e)))
)) ;
window#show () ;
let metasenv,expr = !get_metasenv_and_term () in
let _ = CicTypeChecker.type_of_aux' metasenv [] expr in
ProofEngine.set_proof
- (Some (!get_uri (), (1,[],expr)::metasenv, Cic.Meta (1,[]), expr)) ;
+ (Some (Some (!get_uri ()), (1,[],expr)::metasenv, Cic.Meta (1,[]), expr));
set_proof_engine_goal (Some 1) ;
refresh_goals notebook ;
refresh_proof output ;
refresh_proof output
with
InvokeTactics.RefreshSequentException e ->
- output_html outputhtml
+ HelmLogger.log
(`Error (`T ("Exception raised during the refresh of the " ^
"sequent: " ^ Printexc.to_string e)))
| InvokeTactics.RefreshProofException e ->
- output_html outputhtml
+ HelmLogger.log
(`Error (`T ("Exception raised during the refresh of the " ^
"proof: " ^ Printexc.to_string e)))
| e ->
- output_html outputhtml
+ HelmLogger.log
(`Error (`T (Printexc.to_string e)))
;;
let check_term_in_scratch scratch_window metasenv context expr =
try
- let ty = CicTypeChecker.type_of_aux' metasenv context expr in
+ let ty,ugraph =
+ CicTypeChecker.type_of_aux' metasenv context expr CicUniv.empty_ugraph
+ in
let expr = Cic.Cast (expr,ty) in
scratch_window#show () ;
scratch_window#set_term expr ;
let check scratch_window () =
let inputt = ((rendering_window ())#inputt : TermEditor.term_editor) in
- let outputhtml = ((rendering_window ())#outputhtml(* : GHtml.xmhtml*)) in
let metasenv =
match ProofEngine.get_proof () with
None -> []
canonical_context
in
try
- let metasenv',expr = inputt#get_metasenv_and_term context metasenv in
- check_term_in_scratch scratch_window metasenv' context expr
+ let metasenv',expr,ugraph =
+ inputt#get_metasenv_and_term context metasenv
+ in
+ check_term_in_scratch scratch_window metasenv' context expr
with
e ->
- output_html outputhtml
+ HelmLogger.log
(`Error (`T (Printexc.to_string e)))
;;
let show () =
- let outputhtml = ((rendering_window ())#outputhtml(* : GHtml.xmhtml*)) in
try
show_in_show_window_uri (input_or_locate_uri ~title:"Show")
with
e ->
- output_html outputhtml
+ HelmLogger.log
(`Error (`T (Printexc.to_string e)))
;;
exception NotADefinition;;
let open_ () =
- let outputhtml = ((rendering_window ())#outputhtml(* : GHtml.xmhtml*)) in
let output = ((rendering_window ())#output : TermViewer.proof_viewer) in
let notebook = (rendering_window ())#notebook in
try
let uri = input_or_locate_uri ~title:"Open" in
- CicTypeChecker.typecheck uri ;
+ ignore(CicTypeChecker.typecheck uri CicUniv.empty_ugraph);
+ (* TASSI: typecheck mette la uri nell'env... cosa fa la open_ ?*)
let metasenv,bo,ty =
- match CicEnvironment.get_cooked_obj uri with
- Cic.Constant (_,Some bo,ty,_) -> [],bo,ty
- | Cic.CurrentProof (_,metasenv,bo,ty,_) -> metasenv,bo,ty
+ match fst(CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri ) with
+ Cic.Constant (_,Some bo,ty,_,_) -> [],bo,ty
+ | Cic.CurrentProof (_,metasenv,bo,ty,_,_) -> metasenv,bo,ty
| Cic.Constant _
| Cic.Variable _
| Cic.InductiveDefinition _ -> raise NotADefinition
in
- ProofEngine.set_proof (Some (uri, metasenv, bo, ty)) ;
+ ProofEngine.set_proof (Some (Some uri, metasenv, bo, ty)) ;
set_proof_engine_goal None ;
refresh_goals notebook ;
refresh_proof output ;
!save_set_sensitive true
with
InvokeTactics.RefreshSequentException e ->
- output_html outputhtml
+ HelmLogger.log
(`Error (`T ("Exception raised during the refresh of the " ^
"sequent: " ^ Printexc.to_string e)))
| InvokeTactics.RefreshProofException e ->
- output_html outputhtml
+ HelmLogger.log
(`Error (`T ("Exception raised during the refresh of the " ^
"proof: " ^ Printexc.to_string e)))
| e ->
- output_html outputhtml
+ HelmLogger.log
(`Error (`T (Printexc.to_string e)))
;;
(clist#connect#select_row
(fun ~row ~column ~event ->
let (uristr,_) = List.nth results row in
- match
- MQueryMisc.cic_textual_parser_uri_of_string
- (MQueryMisc.wrong_xpointer_format_from_wrong_xpointer_format'
- uristr)
- with
- CicTextualParser0.ConUri uri
- | CicTextualParser0.VarUri uri
- | CicTextualParser0.IndTyUri (uri,_)
- | CicTextualParser0.IndConUri (uri,_,_) ->
+ match CicUtil.term_of_uri uristr with
+ | Cic.Const (uri, _)
+ | Cic.Var (uri, _)
+ | Cic.MutInd (uri, _, _)
+ | Cic.MutConstruct (uri, _, _, _) ->
show_in_show_window_uri uri
+ | _ -> assert false
)
) ;
window#show ()
let completeSearchPattern () =
let inputt = ((rendering_window ())#inputt : TermEditor.term_editor) in
- let outputhtml = ((rendering_window ())#outputhtml(* : GHtml.xmhtml*)) in
try
- let metasenv,expr = inputt#get_metasenv_and_term ~context:[] ~metasenv:[] in
+ let metasenv,expr,ugraph =
+ inputt#get_metasenv_and_term ~context:[] ~metasenv:[] in
let must = CGSearchPattern.get_constraints expr in
let must',only = refine_constraints must in
let query =
show_query_results results
with
e ->
- output_html outputhtml
+ HelmLogger.log
(`Error (`T (Printexc.to_string e)))
;;
let insertQuery () =
- let outputhtml = ((rendering_window ())#outputhtml(* : GHtml.xmhtml*)) in
try
let chosen = ref None in
let window =
show_query_results results
with
e ->
- output_html outputhtml
+ HelmLogger.log
(`Error (`T (Printexc.to_string e)))
;;
let searchPattern () =
let inputt = ((rendering_window ())#inputt : TermEditor.term_editor) in
- let outputhtml = ((rendering_window ())#outputhtml(* : GHtml.xmhtml*)) in
try
let proof =
match ProofEngine.get_proof () with
match !ProofEngine.goal with
| None -> ()
| Some metano ->
- let uris' =
- TacticChaser.matchConclusion
- mqi_handle
- ~output_html:(fun m -> output_html outputhtml (`Msg (`T m)))
- ~choose_must () ~status:(proof, metano)
- in
+ let uris' = List.map fst (MetadataQuery.hint ~dbd (proof, metano)) in
let uri' =
user_uri_choice ~title:"Ambiguous input."
~msg: "Many lemmas can be successfully applied. Please, choose one:"
InvokeTactics'.apply ()
with
e ->
- output_html outputhtml
+ HelmLogger.log
(`Error (`T (Printexc.to_string e)))
;;
let module G = Gdome in
let rec aux element =
if element#hasAttributeNS
- ~namespaceURI:Misc.helmns
+ ~namespaceURI:Misc.helm_ns
~localName:(G.domString "xref")
then
mmlwidget#set_selection (Some element)
~packing:(vbox#pack ~expand:true ~padding:5) () in
let sequent_viewer =
TermViewer.sequent_viewer
+ ~mml_of_cic_sequent:ApplyTransformation.mml_of_cic_sequent
~packing:(scrolled_window#add) ~width:400 ~height:280 () in
object(self)
val mutable term = Cic.Rel 1 (* dummy value *)
GBin.scrolled_window ~border_width:10
~packing:(vbox1#pack ~expand:true ~padding:5) () in
let proofw =
- TermViewer.sequent_viewer ~width:400 ~height:275
- ~packing:(scrolled_window1#add) () in
+ TermViewer.sequent_viewer
+ ~mml_of_cic_sequent:ApplyTransformation.mml_of_cic_sequent
+ ~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 contradictionb =
GButton.button ~label:"Contradiction"
~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
+ let autob=
+ GButton.button ~label:"Auto"
+ ~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 existsb =
ignore(searchpatternb#connect#clicked searchPattern) ;
ignore(injectionb#connect#clicked InvokeTactics'.injection) ;
ignore(discriminateb#connect#clicked InvokeTactics'.discriminate) ;
+ ignore(autob#connect#clicked InvokeTactics'.auto) ;
(* Zack: spostare in una toolbar
ignore(whdb#connect#clicked whd) ;
ignore(reduceb#connect#clicked reduce) ;
GBin.scrolled_window ~border_width:10
~packing:(vbox1#pack ~expand:true ~padding:5) () in
let proofw =
- TermViewer.sequent_viewer ~width:400 ~height:275
- ~packing:(scrolled_window1#add) () in
+ TermViewer.sequent_viewer
+ ~mml_of_cic_sequent:ApplyTransformation.mml_of_cic_sequent
+ ~width:400 ~height:275 ~packing:(scrolled_window1#add) () in
object(self)
method proofw = (assert false : TermViewer.sequent_viewer)
method content = vbox1
let dump_environment () =
try
- let oc = open_out environmentfile in
- output_html (outputhtml ()) (`Msg (`T "Dumping environment ..."));
- CicEnvironment.dump_to_channel
- ~callback:(fun uri -> output_html (outputhtml ()) (`Msg (`T uri)))
- oc;
- output_html (outputhtml ()) (`Msg (`T "... done!")) ;
+ let oc = open_out (Helm_registry.get "gtoplevel.environment_file") in
+ HelmLogger.log (`Msg (`T "Dumping environment ..."));
+ CicEnvironment.dump_to_channel oc;
+ HelmLogger.log (`Msg (`T "... done!")) ;
close_out oc
with exc ->
- output_html (outputhtml ())
+ HelmLogger.log
(`Error (`T (Printf.sprintf "Dump failure, uncaught exception:%s"
(Printexc.to_string exc))))
;;
let restore_environment () =
try
- let ic = open_in environmentfile in
- output_html (outputhtml ()) (`Msg (`T "Restoring environment ... "));
- CicEnvironment.restore_from_channel
- ~callback:(fun uri -> output_html (outputhtml ()) (`Msg (`T uri)))
- ic;
- output_html (outputhtml ()) (`Msg (`T "... done!"));
+ let ic = open_in (Helm_registry.get "gtoplevel.environment_file") in
+ HelmLogger.log (`Msg (`T "Restoring environment ... "));
+ CicEnvironment.restore_from_channel ic;
+ HelmLogger.log (`Msg (`T "... done!"));
close_in ic
with exc ->
- output_html (outputhtml ())
+ HelmLogger.log
(`Error (`T (Printf.sprintf "Restore failure, uncaught exception:%s"
(Printexc.to_string exc))))
;;
factory3#add_item "Reload Stylesheets"
~callback:
(function _ ->
- ChosenTransformer.reload_stylesheets () ;
if ProofEngine.get_proof () <> None then
try
refresh_goals notebook ;
refresh_proof output
with
InvokeTactics.RefreshSequentException e ->
- output_html (outputhtml ())
+ HelmLogger.log
(`Error (`T ("An error occurred while refreshing the " ^
"sequent: " ^ Printexc.to_string e))) ;
(*notebook#remove_all_pages ~skip_switch_page_event:false ;*)
notebook#set_empty_page
| InvokeTactics.RefreshProofException e ->
- output_html (outputhtml ())
+ HelmLogger.log
(`Error (`T ("An error occurred while refreshing the proof: " ^ Printexc.to_string e))) ;
output#unload
) in
~packing:frame#add () in
let inputt =
TermEditor'.term_editor
- mqi_handle
+ ~dbd
~width:400 ~height:100 ~packing:scrolled_window1#add ()
~isnotempty_callback:
(function b ->
let frame =
GBin.frame ~shadow_type:`IN ~packing:(vboxl#pack ~expand:true ~padding:5) ()
in
- let outputhtml =
- new Ui_logger.html_logger
+ let _ =
+ new HelmGtkLogger.html_logger
~width:400 ~height: 100 ~show:true ~packing:frame#add ()
in
object
- method outputhtml = outputhtml
method inputt = inputt
method output = (output : TermViewer.proof_viewer)
method scratch_window = scratch_window
let settings_window = new settings_window output scrolled_window0
(*export_to_postscript_menu_item*)() (choose_selection output) in
set_settings_window settings_window ;
- set_outputhtml outputhtml ;
- ignore(window#event#connect#delete (fun _ -> GMain.Main.quit () ; true )) ;
- CicLogger.log_callback := (outputhtml#log_cic_msg ~append_NL:true)
+ ignore(window#event#connect#delete (fun _ -> GMain.Main.quit () ; true ))
end
(* MAIN *)
let initialize_everything () =
- let module U = Unix in
- let output = TermViewer.proof_viewer ~width:350 ~height:280 () in
+ let output =
+ TermViewer.proof_viewer
+ ~mml_of_cic_object:ApplyTransformation.mml_of_cic_object
+ ~width:350 ~height:280 ()
+ in
let notebook = new notebook in
- let rendering_window' = new rendering_window output notebook in
- rendering_window'#set_auto_disambiguation !auto_disambiguation;
- set_rendering_window rendering_window' ;
- let print_error_as_html prefix msg =
- output_html (outputhtml ()) (`Error (`T (prefix ^ msg)))
- in
- Gdome_xslt.setErrorCallback (Some (print_error_as_html "XSLT Error: "));
- Gdome_xslt.setDebugCallback
- (Some (print_error_as_html "XSLT Debug Message: "));
- rendering_window'#show () ;
- if restore_environment_on_boot && Sys.file_exists environmentfile then
- restore_environment ();
- GtkThread.main ()
+ let rendering_window' = new rendering_window output notebook in
+ rendering_window'#set_auto_disambiguation !auto_disambiguation;
+ set_rendering_window rendering_window';
+ let print_error_as_html prefix msg =
+ HelmLogger.log (`Error (`T (prefix ^ msg)))
+ in
+ Gdome_xslt.setErrorCallback (Some (print_error_as_html "XSLT Error: "));
+ Gdome_xslt.setDebugCallback
+ (Some (print_error_as_html "XSLT Debug Message: "));
+ rendering_window'#show () ;
+ if restore_environment_on_boot &&
+ Sys.file_exists (Helm_registry.get "gtoplevel.environment_file")
+ then
+ restore_environment ();
+ GtkThread.main ()
;;
let main () =
;;
try
+(* CicEnvironment.set_trust (fun _ -> false); *)
Sys.catch_break true;
main ();
with Sys.Break -> () (* exit nicely, invoking at_exit functions *)
projects / helm.git / blobdiff