module MQGU = MQGUtil
module MQG = MQueryGenerator
+module DB = Dbi_mysql
(* first of all let's initialize the Helm_registry *)
let _ =
let mqi_debug_fun s = debug_print ~level:2 s
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 *)
~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
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 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);;
;;
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."))) ;
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 ()
(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 () (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:frame#add () in
let inputt =
TermEditor'.term_editor
- mqi_handle
+ ~dbh
~width:400 ~height:100 ~packing:scrolled_window1#add ()
~isnotempty_callback:
(function b ->
projects / helm.git / commitdiff