(fun (n,u) ->
(n,MQueryMisc.wrong_xpointer_format_from_wrong_xpointer_format' u))
result in
+ (* delete all .var uris *)
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
+ (* delete all not "cic:/Coq" uris *)
let uris =
(* TODO ristretto per ragioni di efficienza *)
- prerr_endline "STO FILTRANDO2";
List.filter (fun _,uri -> Pcre.pmatch ~pat:"^cic:/Coq/" uri) uris in
+ (* concl_cost are the costants in the conclusion of the proof
+ while hyp_const are the constants in the hypothesis *)
+ let (_,concl_const) = NewConstraints.constants_of ty in
+ 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))
+ | Some (_,Cic.Def (t,_)) -> (NewConstraints.StringSet.union set (NewConstraints.constants_concl t))
+ | _ -> set in
+ let hyp_const =
+ List.fold_right hyp ey NewConstraints.StringSet.empty in
+ prerr_endline (NewConstraints.pp_StringSet (NewConstraints.StringSet.union hyp_const concl_const));
+ (* uris with new constants in the proof are filtered *)
+ let uris = List.filter (Filter_auto.filter_new_constants conn (NewConstraints.StringSet.union hyp_const concl_const)) 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";
prerr_endline ("Ne sono rimasti " ^ string_of_int (List.length uris));
filter_out uris
in
- uris'
+ prerr_endline ("Ne sono rimasti " ^ string_of_int (List.length uris'));
+ uris'
;;
(*funzione che sceglie il penultimo livello di profondita' dei must*)
else l1 - l2)
subproofs
in
- (* now we may drop the prefix tag *)
+ (* now we may drop the prefix tag *)
List.map snd res