returns true if target is subsumed by some equality in table
*)
let subsumption env table target =
- let _, (ty, left, right, _), tmetas, _ = target in
+ let _, _, (ty, left, right, _), tmetas, _ = target in
let metasenv, context, ugraph = env in
let metasenv = metasenv @ tmetas in
let samesubst subst subst' =
in
let rec ok what = function
| [] -> false, []
- | (_, subst, menv, ug, ((pos, (_, _, (_, l, r, o), _, _)), _))::tl ->
+ | (_, subst, menv, ug, ((pos, (_, _, (_, l, r, o), m, _)), _))::tl ->
try
let other = if pos = Utils.Left then r else l in
let subst', menv', ug' =
let t1 = Unix.gettimeofday () in
try
let r =
- Inference.matching metasenv context what other ugraph in
+ Inference.matching (metasenv @ menv @ m) context what other ugraph
+ in
let t2 = Unix.gettimeofday () in
match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1);
r
ok what tl
in
let r, subst = ok right leftr in
- if r then
- true, subst
- else
- let rightr =
- match right with
- | Cic.Meta _ -> []
- | _ ->
- let rightc = get_candidates Matching table right in
- find_all_matches ~unif_fun:Inference.matching
- metasenv context ugraph 0 right ty rightc
- in
- ok left rightr
+ let r, s =
+ if r then
+ true, subst
+ else
+ let rightr =
+ match right with
+ | Cic.Meta _ -> []
+ | _ ->
+ let rightc = get_candidates Matching table right in
+ find_all_matches ~unif_fun:Inference.matching
+ metasenv context ugraph 0 right ty rightc
+ in
+ ok left rightr
+ in
+ (if r then
+ debug_print
+ (lazy
+ (Printf.sprintf "SUBSUMPTION! %s\n%s\n"
+ (Inference.string_of_equality target) (Utils.print_subst s))));
+ r, s
;;
!maxmeta, res
in
let res = demodulation_aux metasenv' context ugraph table 0 left in
- match res with
- | Some t ->
- let newmeta, newtarget = build_newtarget true t in
- if (Inference.is_identity (metasenv', context, ugraph) newtarget) ||
- (Inference.meta_convertibility_eq target newtarget) then
- newmeta, newtarget
- else
- demodulation_equality newmeta env table sign newtarget
- | None ->
- let res = demodulation_aux metasenv' context ugraph table 0 right in
- match res with
- | Some t ->
- let newmeta, newtarget = build_newtarget false t in
- if (Inference.is_identity (metasenv', context, ugraph) newtarget) ||
+ let newmeta, newtarget =
+ match res with
+ | Some t ->
+ let newmeta, newtarget = build_newtarget true t in
+ if (Inference.is_identity (metasenv', context, ugraph) newtarget) ||
(Inference.meta_convertibility_eq target newtarget) then
- newmeta, newtarget
- else
- demodulation_equality newmeta env table sign newtarget
- | None ->
- newmeta, target
+ newmeta, newtarget
+ else
+ demodulation_equality newmeta env table sign newtarget
+ | None ->
+ let res = demodulation_aux metasenv' context ugraph table 0 right in
+ match res with
+ | Some t ->
+ let newmeta, newtarget = build_newtarget false t in
+ if (Inference.is_identity (metasenv', context, ugraph) newtarget) ||
+ (Inference.meta_convertibility_eq target newtarget) then
+ newmeta, newtarget
+ else
+ demodulation_equality newmeta env table sign newtarget
+ | None ->
+ newmeta, target
+ in
+ (* newmeta, newtarget *)
+ (* tentiamo di ridurre usando CicReduction.normalize *)
+ let w, p, (ty, left, right, o), m, a = newtarget in
+ let left' = ProofEngineReduction.simpl context left in
+ let right' = ProofEngineReduction.simpl context right in
+ let newleft =
+ if !Utils.compare_terms left' left = Utils.Lt then left' else left in
+ let newright =
+ if !Utils.compare_terms right' right = Utils.Lt then right' else right in
+ if newleft != left || newright != right then (
+ debug_print
+ (lazy
+ (Printf.sprintf "left: %s, left': %s\nright: %s, right': %s\n"
+ (CicPp.ppterm left) (CicPp.ppterm left') (CicPp.ppterm right)
+ (CicPp.ppterm right')))
+ );
+ let w' = Utils.compute_equality_weight ty newleft newright in
+ let o' = !Utils.compare_terms newleft newright in
+ newmeta, (w', p, (ty, newleft, newright, o'), m, a)
;;
;;
-(* let unification = CicUnification.fo_unif;; *)
+let unification = CicUnification.fo_unif;;
exception MatchingFailure;;
;;
+(*
let equations_blacklist =
List.fold_left
(fun s u -> UriManager.UriSet.add (UriManager.uri_of_string u) s)
"cic:/matita/logic/equality/eq_rect.con";
]
;;
+*)
+let equations_blacklist = UriManager.UriSet.empty;;
+
let find_library_equalities dbd context status maxmeta =
let module C = Cic in
let uriset, eqlist =
(List.fold_left
(fun (s, l) (u, e) ->
- if List.exists (meta_convertibility_eq e) l then (
+ if List.exists (meta_convertibility_eq e) (List.map snd l) then (
debug_print
(lazy
(Printf.sprintf "NO!! %s already there!"
(string_of_equality e)));
(UriManager.UriSet.add u s, l)
- ) else (UriManager.UriSet.add u s, e::l))
+ ) else (UriManager.UriSet.add u s, (u, e)::l))
(UriManager.UriSet.empty, []) found)
in
uriset, eqlist, maxm
type environment = Cic.metasenv * Cic.context * CicUniv.universe_graph;;
-let is_identity ((_, context, ugraph) as env) = function
- | ((_, _, (ty, left, right, _), _, _) as equality) ->
+let is_identity ((metasenv, context, ugraph) as env) = function
+ | ((_, _, (ty, left, right, _), menv, _) as equality) ->
(left = right ||
- (meta_convertibility left right) ||
- (fst (CicReduction.are_convertible context left right ugraph)))
+ (* (meta_convertibility left right) || *)
+ (fst (CicReduction.are_convertible
+ ~metasenv:(metasenv @ menv) context left right ugraph)))
;;
*)
val find_library_equalities:
HMysql.dbd -> Cic.context -> ProofEngineTypes.status -> int ->
- UriManager.UriSet.t * equality list * int
+ UriManager.UriSet.t * (UriManager.uri * equality) list * int
(**
searches the library for theorems that are not equalities (returned by the
let full = ref false;;
+let retrieve_only = ref false;;
+
let _ =
let module S = Saturation in
let set_ratio v = S.weight_age_ratio := v; S.weight_age_counter := v
and set_width w = S.maxwidth := w
and set_depth d = S.maxdepth := d
and set_full () = full := true
+ and set_retrieve () = retrieve_only := true
in
Arg.parse [
"-full", Arg.Unit set_full, "Enable full mode";
"-d", Arg.Int set_depth,
Printf.sprintf "Maximal depth (default: %d)" !Saturation.maxdepth;
+
+ "-retrieve", Arg.Unit set_retrieve, "retrieve only";
] (fun a -> ()) "Usage:"
in
Helm_registry.load_from !configuration_file;
()
in
let term, metasenv, ugraph = get_from_user ~dbd in
-Saturation.main dbd !full term metasenv ugraph;;
+if !retrieve_only then
+ Saturation.retrieve_and_print dbd term metasenv ugraph
+else
+ Saturation.main dbd !full term metasenv ugraph
+;;
maxmeta := newmeta;
if is_identity env newcurrent then
if sign = Negative then Some (sign, newcurrent)
- else None
+ else (
+(* debug_print *)
+(* (lazy *)
+(* (Printf.sprintf "\ncurrent was: %s\nnewcurrent is: %s\n" *)
+(* (string_of_equality current) *)
+(* (string_of_equality newcurrent))); *)
+(* debug_print *)
+(* (lazy *)
+(* (Printf.sprintf "active is: %s" *)
+(* (String.concat "\n" *)
+(* (List.map (fun (_, e) -> (string_of_equality e)) active_list)))); *)
+ None
+ )
else
Some (sign, newcurrent)
in
None
else
match passive_table with
- | None -> res
+ | None ->
+ if fst (Indexing.subsumption env active_table c) then
+ None
+ else
+ res
| Some passive_table ->
if Indexing.in_index passive_table c then None
- else res
+ else
+ let r1, _ = Indexing.subsumption env active_table c in
+ if r1 then None else
+ let r2, _ = Indexing.subsumption env passive_table c in
+ if r2 then None else res
;;
type fs_time_info_t = {
not ((Indexing.in_index active_table e) ||
(Indexing.in_index passive_table e)))
in
- new_neg, List.filter is_duplicate new_pos
+ new_neg, List.filter subs (List.filter is_duplicate new_pos)
;;
let lib_eq_uris, library_equalities, maxm =
find_library_equalities dbd context (proof, goal') (maxm+2)
in
+ let library_equalities = List.map snd library_equalities in
maxmeta := maxm+2; (* TODO ugly!! *)
let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
let new_meta_goal, metasenv, type_of_goal =
Printf.printf "\nequalities:\n%s\n"
(String.concat "\n"
(List.map
- (string_of_equality ~env)
- (equalities @ library_equalities)));
+ (string_of_equality ~env) equalities));
+(* (equalities @ library_equalities))); *)
print_endline "--------------------------------------------------";
let start = Unix.gettimeofday () in
print_endline "GO!";
let lib_eq_uris, library_equalities, maxm =
find_library_equalities dbd context (proof, goal') (maxm+2)
in
+ let library_equalities = List.map snd library_equalities in
let t2 = Unix.gettimeofday () in
maxmeta := maxm+2;
let equalities =
AutoTactic.term_is_equality := Inference.term_is_equality;
);;
+
+let retrieve_and_print dbd term metasenv ugraph =
+ let module C = Cic in
+ let module T = CicTypeChecker in
+ let module PET = ProofEngineTypes in
+ let module PP = CicPp in
+ let proof = None, (1, [], term)::metasenv, C.Meta (1, []), term in
+ let status = PET.apply_tactic (PrimitiveTactics.intros_tac ()) (proof, 1) in
+ let proof, goals = status in
+ let goal' = List.nth goals 0 in
+ let uri, metasenv, meta_proof, term_to_prove = proof in
+ let _, context, goal = CicUtil.lookup_meta goal' metasenv in
+ let eq_indexes, equalities, maxm = find_equalities context proof in
+ let new_meta_goal, metasenv, type_of_goal =
+ let irl =
+ CicMkImplicit.identity_relocation_list_for_metavariable context in
+ let _, context, ty = CicUtil.lookup_meta goal' metasenv in
+ debug_print
+ (lazy (Printf.sprintf "\n\nTIPO DEL GOAL: %s\n" (CicPp.ppterm ty)));
+ Cic.Meta (maxm+1, irl),
+ (maxm+1, context, ty)::metasenv,
+ ty
+ in
+ let ugraph = CicUniv.empty_ugraph in
+ let env = (metasenv, context, ugraph) in
+ let goal = Inference.BasicProof new_meta_goal, [], goal in
+ let t1 = Unix.gettimeofday () in
+ let lib_eq_uris, library_equalities, maxm =
+ find_library_equalities dbd context (proof, goal') (maxm+2)
+ in
+ let t2 = Unix.gettimeofday () in
+ maxmeta := maxm+2;
+ let equalities =
+ let equalities = (* equalities @ *) library_equalities in
+ debug_print
+ (lazy
+ (Printf.sprintf "\n\nequalities:\n%s\n"
+ (String.concat "\n"
+ (List.map
+ (fun (u, e) ->
+(* Printf.sprintf "%s: %s" *)
+ (UriManager.string_of_uri u)
+(* (string_of_equality e) *)
+ )
+ equalities))));
+ debug_print (lazy "SIMPLYFYING EQUALITIES...");
+ let rec simpl e others others_simpl =
+ let (u, e) = e in
+ let active = List.map (fun (u, e) -> (Positive, e))
+ (others @ others_simpl) in
+ let tbl =
+ List.fold_left
+ (fun t (_, e) -> Indexing.index t e)
+ (Indexing.empty_table ()) active
+ in
+ let res = forward_simplify env (Positive, e) (active, tbl) in
+ match others with
+ | hd::tl -> (
+ match res with
+ | None -> simpl hd tl others_simpl
+ | Some e -> simpl hd tl ((u, (snd e))::others_simpl)
+ )
+ | [] -> (
+ match res with
+ | None -> others_simpl
+ | Some e -> (u, (snd e))::others_simpl
+ )
+ in
+ match equalities with
+ | [] -> []
+ | hd::tl ->
+ let others = tl in (* List.map (fun e -> (Positive, e)) tl in *)
+ let res =
+ List.rev (simpl (*(Positive,*) hd others [])
+ in
+ debug_print
+ (lazy
+ (Printf.sprintf "\nequalities AFTER:\n%s\n"
+ (String.concat "\n"
+ (List.map
+ (fun (u, e) ->
+ Printf.sprintf "%s: %s"
+ (UriManager.string_of_uri u)
+ (string_of_equality e)
+ )
+ res))));
+ res
+ in
+ debug_print
+ (lazy
+ (Printf.sprintf "Time to retrieve equalities: %.9f\n" (t2 -. t1)))
+;;
projects / helm.git / commitdiff