- let (_, ey ,ty) = List.find (function (m,_,_) -> m=metano) metasenv in
- let list_of_must,only = MQueryLevels.out_restr metasenv ey ty in
- let must = choose_must list_of_must only in
- let torigth_restriction (u,b) =
- let p =
- if b then
- "http://www.cs.unibo.it/helm/schemas/schema-helm#MainConclusion"
- else
- "http://www.cs.unibo.it/helm/schemas/schema-helm#InConclusion"
- in
- (u,p,None)
- in
- let rigth_must = List.map torigth_restriction must in
- let rigth_only = Some (List.map torigth_restriction only) in
- let result =
- MQueryGenerator.searchPattern
- (rigth_must,[],[]) (rigth_only,None,None) in
- let uris =
- List.map
- (function uri,_ ->
- Misc.wrong_xpointer_format_from_wrong_xpointer_format' uri
- ) result in
- let html =
- " <h1>Backward Query: </h1>" ^
- " <pre>" ^ get_last_query result ^ "</pre>"
- in
- output_html outputhtml html ;
- let uris',exc =
- let rec filter_out =
- function
- [] -> [],""
- | uri::tl ->
- let tl',exc = filter_out tl in
- try
- if
- ProofEngine.can_apply
- (term_of_cic_textual_parser_uri
- (Misc.cic_textual_parser_uri_of_string uri))
- then
- uri::tl',exc
- else
- tl',exc
- with
- e ->
- let exc' =
- "<h1 color=\"red\"> ^ Exception raised trying to apply " ^
- uri ^ ": " ^ Printexc.to_string e ^ " </h1>" ^ exc
- in
- tl',exc'
- in
- filter_out uris
- in
- let html' =
- " <h1>Objects that can actually be applied: </h1> " ^
- String.concat "<br>" uris' ^ exc ^
- " <h1>Number of false matches: " ^
- string_of_int (List.length uris - List.length uris') ^ "</h1>" ^
- " <h1>Number of good matches: " ^
- string_of_int (List.length uris') ^ "</h1>"
- in
- output_html outputhtml html' ;
- let uri' =
- user_uri_choice ~title:"Ambiguous input."
- ~msg:
- "Many lemmas can be successfully applied. Please, choose one:"
- uris'
- in
- inputt#set_term uri' ;
- InvokeTactics'.apply ()
+ let uris' =
+ TacticChaser.searchPattern
+ ~output_html:(output_html outputhtml) ~choose_must ()
+ ~status:(proof, metano)
+ in
+ let uri' =
+ user_uri_choice ~title:"Ambiguous input."
+ ~msg: "Many lemmas can be successfully applied. Please, choose one:"
+ uris'
+ in
+ inputt#set_term uri' ;
+ InvokeTactics'.apply ()