+ 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'
+;;
+
+
+(*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
+;;*)
+
+let choose_must list_of_must only =
+ 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 ~status:(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() ~status:(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 ~status:(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' ~status:(proof,goal)
+;;
+*)
+
+
+let searchTheorems mqi_handle ~status:(proof,goal) =
+prerr_endline "1";
+ let uris' =
+ matchConclusion mqi_handle ~choose_must() ~status:(proof, goal) in
+prerr_endline "2";
+ 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
+prerr_endline "3";
+ let list_proofgoal =
+ List.map
+ (function term ->
+ PrimitiveTactics.apply_tac ~term ~status:(proof,goal)) list_of_termin in
+prerr_endline "4";
+let res =
+ List.sort
+ (fun (_,gl1) (_,gl2) ->
+ Pervasives.compare (List.length gl1) (List.length gl2))
+ list_proofgoal
+ in
+prerr_endline "5";
+res