+ 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 html' ;
+ uris'
+;;
+
+
+(*matchConclusion modificata per evitare una doppia apply*)
+let matchConclusion2 mqi_handle ?(output_html = (fun _ -> ())) ~choose_must() status =
+ let ((_, metasenv, _, _), metano) = status in
+ let (_, ey ,ty) = CicUtil.lookup_meta metano metasenv in
+ let conn =
+ match mqi_handle.MQIConn.pgc with
+ MQIConn.MySQL_C conn -> conn
+ | _ -> assert false in
+ let result = Match_concl.cmatch conn ty in
+ 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 isvar (_,s) =
+ let len = String.length s in
+ let suffix = String.sub s (len-4) 4 in
+ not (suffix = ".var") in
+ let uris = List.filter isvar uris in
+ let uris =
+ (* TODO ristretto per ragioni di efficienza *)
+ prerr_endline "STO FILTRANDO2";
+ List.filter (fun _,uri -> Pcre.pmatch ~pat:"^cic:/Coq/" uri) uris in
+(*
+ let uris =
+ (* TODO ristretto per ragioni di efficienza *)
+ prerr_endline "STO FILTRANDO2";
+ List.filter (fun uri -> Pcre.pmatch ~pat:"^cic:/Coq/" uri) uris
+ in
+ let uris =
+ (* ristretto all cache *)
+ prerr_endline "SOLO CACHE";
+ List.filter
+ (fun uri -> CicEnvironment.in_cache (UriManager.uri_of_string uri)) uris
+ in
+ prerr_endline "HO FILTRATO2";
+*)
+ let uris' =
+ let rec filter_out =
+ function
+ [] -> []
+ | (m,uri)::tl ->
+ let tl' = filter_out tl in
+ try
+ (m,
+ (prerr_endline ("STO APPLICANDO " ^ uri);
+ (PrimitiveTactics.apply_tac
+ ~term:(MQueryMisc.term_of_cic_textual_parser_uri
+ (MQueryMisc.cic_textual_parser_uri_of_string uri))
+ status)))::tl'
+ (* with ProofEngineTypes.Fail _ -> tl' *)
+ (* patch to cover CSC's exportation bug *)
+ with _ -> tl'
+ in
+ prerr_endline ("Ne sono rimasti " ^ string_of_int (List.length uris));
+ filter_out uris
+ in
+ uris'
+;;
+
+(*funzione che sceglie il penultimo livello di profondita' dei must*)
+
+(*
+let choose_must list_of_must only=
+let n = (List.length list_of_must) - 1 in
+ List.nth list_of_must n
+;;*)
+
+(* questa prende solo il main *)
+let choose_must list_of_must only =
+ List.nth list_of_must 0
+
+(* livello 1
+let choose_must list_of_must only =
+ try
+ List.nth list_of_must 1
+ with _ ->
+ List.nth list_of_must 0 *)
+
+(* OLD CODE: TO BE REMOVED
+(*Funzione position prende una lista e un elemento e mi ritorna la posizione dell'elem nella lista*)
+(*Mi serve per ritornare la posizione del teo che produce meno subgoal*)
+
+exception NotInTheList;;
+
+
+let position n =
+ let rec aux k =
+ function
+ [] -> raise NotInTheList
+ | m::_ when m=n -> k
+ | _::tl -> aux (k+1) tl in
+ aux 1
+;;
+
+
+
+(*function taking a status and returning a new status after having searching a theorem to apply ,theorem which *)
+(*generate the less number of subgoals*)
+
+let searchTheorem (proof,goal) =
+ let mqi_flags = [MQIC.Postgres ; MQIC.Stat ; MQIC.Warn ; MQIC.Log] (* default MathQL interpreter options *)
+ in
+ let mqi_handle = MQIC.init mqi_flags prerr_string
+in
+ let uris' =
+ matchConclusion
+ mqi_handle ~choose_must() (proof, goal)
+ in
+ let list_of_termin =
+ List.map
+ (function string ->
+ (MQueryMisc.term_of_cic_textual_parser_uri
+ (MQueryMisc.cic_textual_parser_uri_of_string string))
+ )
+ uris'
+ in
+ let list_proofgoal =
+ List.map
+ (function term ->
+ PrimitiveTactics.apply_tac ~term (proof,goal))
+ list_of_termin
+ in
+ let (list_of_subgoal: int list list) =
+ List.map snd list_proofgoal
+ in
+ let list_of_num =
+ List.map List.length list_of_subgoal
+ in
+ let list_sort =
+ List.sort Pervasives.compare list_of_num
+ in (*ordino la lista in modo cresc*)
+ let min= List.nth list_sort 0 (*prendo il minimo*)
+ in
+ let uri' = (*cerco il teo di pos k*)
+ List.nth list_of_termin (position min list_of_num)
+ in
+ (* let teo=
+ String.sub uri' 4 (String.length uri' - 4)
+
+ (* modifico la str in modo che sia accettata da apply*)
+ in*)
+ PrimitiveTactics.apply_tac ~term:uri' (proof,goal)
+;;
+*)
+
+
+let searchTheorems mqi_handle (proof,goal) =
+(*prerr_endline "1";*)
+ let subproofs =
+ matchConclusion2 mqi_handle ~choose_must() (proof, goal) in
+ let res =
+ List.sort
+ (fun (n1,(_,gl1)) (n2,(_,gl2)) ->
+ let l1 = List.length gl1 in
+ let l2 = List.length gl2 in
+ (* if the list of subgoals have the same lenght we use the
+ prefix tag, where higher tags have precedence *)
+ if l1 = l2 then n2 - n1
+ else l1 - l2)
+ subproofs
+ in
+ (* now we may drop the prefix tag *)
+ List.map snd res
+
+