From 584455a9f581cd2f0fa76a6720c5749b083db8bf Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Wed, 1 Sep 2004 07:24:22 +0000 Subject: [PATCH] Bug fixing: the call to MQueryMisc.wrong_xpointer_format_from_wrong_xpointer_format' must be done after filter_new_constants (that compares uris). --- helm/ocaml/tactics/tacticChaser.ml | 45 +++++++++++++++--------------- 1 file changed, 22 insertions(+), 23 deletions(-) diff --git a/helm/ocaml/tactics/tacticChaser.ml b/helm/ocaml/tactics/tacticChaser.ml index 831ccc6f4..2235670a0 100644 --- a/helm/ocaml/tactics/tacticChaser.ml +++ b/helm/ocaml/tactics/tacticChaser.ml @@ -23,15 +23,15 @@ * http://cs.unibo.it/helm/. *) -(******************************************************************************) -(* *) -(* PROJECT HELM *) -(* *) -(* Claudio Sacerdoti Coen *) -(* 18/02/2003 *) -(* *) -(* *) -(******************************************************************************) +(*****************************************************************************) +(* *) +(* PROJECT HELM *) +(* *) +(* Claudio Sacerdoti Coen *) +(* 18/02/2003 *) +(* *) +(* *) +(*****************************************************************************) module MQI = MQueryInterpreter module MQIC = MQIConn @@ -121,16 +121,9 @@ let matchConclusion2 mqi_handle ?(output_html = (fun _ -> ())) ~choose_must() st match mqi_handle.MQIConn.pgc with MQIConn.MySQL_C conn -> conn | _ -> assert false in - let result = Match_concl.cmatch conn ty in - (* Stampa il risultato della query - List.iter - (fun (n,u) -> prerr_endline ((string_of_int n) ^ " " ^u)) result; - *) - let uris = - List.map - (fun (n,u) -> - (n,MQueryMisc.wrong_xpointer_format_from_wrong_xpointer_format' u)) - result in + let uris = Match_concl.cmatch conn ty in + (* List.iter + (fun (n,u) -> prerr_endline ((string_of_int n) ^ " " ^u)) uris; *) (* delete all .var uris *) let isvar (_,s) = let len = String.length s in @@ -146,7 +139,7 @@ let matchConclusion2 mqi_handle ?(output_html = (fun _ -> ())) ~choose_must() st (* concl_cost are the costants in the conclusion of the proof while hyp_const are the constants in the hypothesis *) let (main_concl,concl_const) = NewConstraints.mainandcons ty in - prerr_endline ("Ne sono rimasti 1 " ^ string_of_int (List.length uris)); + prerr_endline ("Ne sono rimasti" ^ string_of_int (List.length uris)); let hyp t set = match t with Some (_,Cic.Decl t) -> (NewConstraints.StringSet.union set (NewConstraints.constants_concl t)) @@ -171,6 +164,11 @@ let matchConclusion2 mqi_handle ?(output_html = (fun _ -> ())) ~choose_must() st in prerr_endline "HO FILTRATO2"; *) + let uris = + List.map + (fun (n,u) -> + (n,MQueryMisc.wrong_xpointer_format_from_wrong_xpointer_format' u)) + uris in let uris' = let rec filter_out = function @@ -179,14 +177,15 @@ let matchConclusion2 mqi_handle ?(output_html = (fun _ -> ())) ~choose_must() st let tl' = filter_out tl in try prerr_endline ("STO APPLICANDO " ^ uri); - (m, + let res = (m, (ProofEngineTypes.apply_tactic( PrimitiveTactics.apply_tac ~term:(MQueryMisc.term_of_cic_textual_parser_uri (MQueryMisc.cic_textual_parser_uri_of_string uri))) - status))::tl' + status))::tl' in + prerr_endline ("OK");res (* with ProofEngineTypes.Fail _ -> tl' *) (* patch to cover CSC's exportation bug *) - with _ -> tl' + with _ -> prerr_endline ("FAIL");tl' in prerr_endline ("Ne sono rimasti 2 " ^ string_of_int (List.length uris)); filter_out uris -- 2.39.2