module MQGU = MQGUtil
module MQG = MQueryGenerator
-(* GLOBAL CONSTANTS *)
+module DB = Dbi_mysql
+
+(* 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 configuration_file = "triciclo.conf.xml"
+(* 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 mqi_handle = MQIC.init_if_connected ~log:mqi_debug_fun ()
+let dbh = new DB.connection ~host:"mowgli.cs.unibo.it" ~user:"helm" "mowgli"
let xlinkns = Gdome.domString "http://www.w3.org/1999/xlink";;
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)
-;;
-
(* UTILITY FUNCTIONS TO DISAMBIGUATE AN URI *)
(* Check window *)
lazy
(let mmlwidget =
TermViewer.sequent_viewer
+ ~mml_of_cic_sequent:ChosenTransformer.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
+ let term = CicUtil.term_of_uri uri in
(Cic.Cast (term, CicTypeChecker.type_of_aux' [] [] term))
in
try
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
GtkThread.main ();
match !chosen with
None -> raise NoChoice
- | Some n -> n
+ | Some n -> [n]
;;
let innertypesuri = UriManager.innertypesuri_of_uri uri in
Xml.pp ~quiet:true xmlinnertypes (Some (path ^ ".types.xml")) ;
Http_getter.register' innertypesuri
- (Helm_registry.get "annotations.url" ^
+ (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")) ;
Http_getter.register' uri
- (Helm_registry.get "annotations.url" ^
+ (Helm_registry.get "local_library.url" ^
Str.replace_first (Str.regexp "^cic:") ""
(UriManager.string_of_uri uri) ^ ".xml"
) ;
in
Xml.pp ~quiet:true bodyxml' (Some (path ^ ".body.xml")) ;
Http_getter.register' bodyuri
- (Helm_registry.get "annotations.url" ^
+ (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 =
- Helm_registry.get "annotations.dir" ^
+ Helm_registry.get "local_library.dir" ^
Str.replace_first (Str.regexp "^cic:") "" uristring
;;
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 *)
+ (*let old_working = CicUniv.get_working () in
+ CicUniv.set_working (CicUniv.get_global ());*)
+ CicUniv.directly_to_env_begin () ;
+ prerr_endline "-------------> QED";
if
CicReduction.are_convertible []
(CicTypeChecker.type_of_aux' [] [] bo) ty
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
+ pathname;
+ (* add the object to the env *)
+ CicEnvironment.add_type_checked_term uri (
+ Cic.Constant ((UriManager.name_of_uri uri),(Some bo),ty,[]));
+ (* FIXME: the variable list!! *)
+ (*
+ CicUniv.qed (); (* now the env has the right constraints *)*)
+ CicUniv.directly_to_env_end();
+ CicUniv.reset_working ();
+ prerr_endline "-------------> FINE";
end
else
raise WrongProof
(** save an unfinished proof on the filesystem *)
let save_unfinished_proof () =
let (xml, bodyxml) = ProofEngine.get_current_status_as_xml () in
- let proof_file_type = Helm_registry.get "triciclo.proof_file_type" in
- let proof_file = Helm_registry.get "triciclo.proof_file" in
+ let proof_file_type = Helm_registry.get "gtoplevel.proof_file_type" in
+ let proof_file = Helm_registry.get "gtoplevel.proof_file" in
Xml.pp ~quiet:true xml (Some proof_file_type) ;
HelmLogger.log
(`Msg (`T ("Current proof type saved to " ^ proof_file_type))) ;
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"
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)
with
begin
notebook#set_current_page
~may_skip_switch_page_event:true metano ;
- notebook#proofw#load_sequent metasenv currentsequent
+prerr_endline "CIAO CIAO" ;
+prerr_endline ("SEQUENTE CORRENTE: " ^ SequentPp.TextualPp.print_sequent currentsequent) ;
+ notebook#proofw#load_sequent metasenv currentsequent ;
+prerr_endline "pASSO CIAO CIAO"
end
with
e ->
let decompose_uris_choice_callback = decompose_uris_choice_callback
let mk_fresh_name_callback = mk_fresh_name_callback
+ let mqi_handle = mqi_handle
+ let dbh = dbh
end
;;
module InvokeTactics' = InvokeTactics.Make (InvokeTacticsCallbacks);;
None -> raise NoChoice
| Some uri0 ->
let uri = UriManager.uri_of_string ("cic:" ^ uri0) in
- let proof_file_type = Helm_registry.get "triciclo.proof_file_type" in
- let proof_file = Helm_registry.get "triciclo.proof_file" in
+ 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
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 ->
HelmLogger.log
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 option) _ =
+ let show_in_show_window_callback mmlwidget ((n : Gdome.element option),_,_,_) =
match n with
None -> ()
| Some n' ->
;;
let locate_callback id =
- 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
- HelmLogger.log (`Msg (`T "Locate Query:")) ;
- MQueryUtil.text_of_query (fun m -> HelmLogger.log (`Msg (`T m))) "" query;
+ let uris = MetadataQuery.locate ~dbh id in
+ HelmLogger.log (`Msg (`T ("Locate Query: " ^ id))) ;
HelmLogger.log (`Msg (`T "Result:")) ;
- MQueryUtil.text_of_result (fun m -> HelmLogger.log (`Msg (`T m))) "" 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
;;
HelmLogger.log (`Msg (`T "OK")) ;
true
with
- Http_getter_types.Unresolvable_URI _ ->
+ Http_getter_types.Key_not_found _ ->
HelmLogger.log
(`Error (`T ("URI " ^ uri ^
" does not correspond to any object."))) ;
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
;;
try
ignore (Http_getter.resolve' uri) ;
raise UriAlreadyInUse
- with Http_getter_types.Unresolvable_URI _ ->
+ with Http_getter_types.Key_not_found _ ->
get_uri := (function () -> uri) ;
get_names := (function () -> names) ;
inductive := inductiveb#active ;
~packing:(vbox#pack ~expand:true ~padding:0) () in
let newinputt =
TermEditor'.term_editor
- mqi_handle
+ ~dbh
~width:400 ~height:20 ~packing:scrolled_window#add
~share_environment_with:inputt ()
~isnotempty_callback:
~packing:(vbox#pack ~expand:true ~padding:0) () in
let newinputt =
TermEditor'.term_editor
- mqi_handle
+ ~dbh
~width:400 ~height:20 ~packing:scrolled_window#add
~share_environment_with:inputt ()
~isnotempty_callback:
(* moved here to have visibility of the ok button *)
let newinputt =
TermEditor'.term_editor
- mqi_handle
+ ~dbh
~width:400 ~height:100 ~packing:scrolled_window#add
~share_environment_with:inputt ()
~isnotempty_callback:
try
ignore (Http_getter.resolve' uri) ;
raise UriAlreadyInUse
- with Http_getter_types.Unresolvable_URI _ ->
+ with Http_getter_types.Key_not_found _ ->
get_metasenv_and_term := (function () -> metasenv,parsed) ;
get_uri := (function () -> uri) ;
window#destroy ()
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 ;
let notebook = (rendering_window ())#notebook in
try
let uri = input_or_locate_uri ~title:"Open" in
- CicTypeChecker.typecheck uri ;
+ ignore(CicTypeChecker.typecheck uri);
+ (* 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.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 ;
(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 ()
match !ProofEngine.goal with
| None -> ()
| Some metano ->
- let uris' =
- TacticChaser.matchConclusion mqi_handle
- ~choose_must () ~status:(proof, metano)
- in
+ let uris' = List.map fst (MetadataQuery.hint ~dbh (proof, metano)) in
let uri' =
user_uri_choice ~title:"Ambiguous input."
~msg: "Many lemmas can be successfully applied. Please, choose one:"
~packing:(vbox#pack ~expand:true ~padding:5) () in
let sequent_viewer =
TermViewer.sequent_viewer
+ ~mml_of_cic_sequent:ChosenTransformer.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:ChosenTransformer.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:ChosenTransformer.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 (Helm_registry.get "triciclo.environment_file") in
+ 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!")) ;
;;
let restore_environment () =
try
- let ic = open_in (Helm_registry.get "triciclo.environment_file") in
+ 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!"));
~packing:frame#add () in
let inputt =
TermEditor'.term_editor
- mqi_handle
+ ~dbh
~width:400 ~height:100 ~packing:scrolled_window1#add ()
~isnotempty_callback:
(function b ->
(* MAIN *)
let initialize_everything () =
- 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 output = TermViewer.proof_viewer ~width:350 ~height:280 () in
+prerr_endline "STO PER CREARE LA PROOF WINDOW" ;
+ let output =
+ TermViewer.proof_viewer
+ ~mml_of_cic_object:ChosenTransformer.mml_of_cic_object
+ ~width:350 ~height:280 ()
+ in
+prerr_endline "CREATA" ;
let notebook = new notebook in
let rendering_window' = new rendering_window output notebook in
+prerr_endline "OK" ;
rendering_window'#set_auto_disambiguation !auto_disambiguation;
set_rendering_window rendering_window';
let print_error_as_html prefix msg =
(Some (print_error_as_html "XSLT Debug Message: "));
rendering_window'#show () ;
if restore_environment_on_boot &&
- Sys.file_exists (Helm_registry.get "triciclo.environment_file")
+ Sys.file_exists (Helm_registry.get "gtoplevel.environment_file")
then
restore_environment ();
GtkThread.main ()
;;
let main () =
+prerr_endline "CIAO" ;
ignore (GtkMain.Main.init ()) ;
initialize_everything () ;
MQIC.close mqi_handle;
projects / helm.git / blobdiff