module Index = Equality_indexing.DT (* path tree based indexing *)
*)
+let beta_expand_time = ref 0.;;
+
let debug_print = Utils.debug_print;;
(*
for debugging
let check_equation env equation msg =
let w, proof, (eq_ty, left, right, order), metas, args = equation in
- let metasenv, context, ugraph = env in
+ let metasenv, context, ugraph = env
let metasenv' = metasenv @ metas in
try
CicTypeChecker.type_of_aux' metasenv' context left ugraph;
type retrieval_mode = Matching | Unification;;
-let print_candidates mode term res =
+let string_of_res ?env =
+ function
+ None -> "None"
+ | Some (t, s, m, u, ((p,e), eq_URI)) ->
+ Printf.sprintf "Some: (%s, %s, %s)"
+ (Utils.string_of_pos p)
+ (Inference.string_of_equality ?env e)
+ (CicPp.ppterm t)
+;;
+
+let print_res ?env res =
+ prerr_endline
+ (String.concat "\n"
+ (List.map (string_of_res ?env) res))
+;;
+
+let print_candidates ?env mode term res =
let _ =
match mode with
| Matching ->
- Printf.printf "| candidates Matching %s\n" (CicPp.ppterm term)
+ prerr_endline ("| candidates Matching " ^ (CicPp.ppterm term))
| Unification ->
- Printf.printf "| candidates Unification %s\n" (CicPp.ppterm term)
+ prerr_endline ("| candidates Unification " ^ (CicPp.ppterm term))
in
- print_endline
+ prerr_endline
(String.concat "\n"
(List.map
- (fun (p, e) ->
- Printf.sprintf "| (%s, %s)" (Utils.string_of_pos p)
- (Inference.string_of_equality e))
- res));
- print_endline "|";
+ (fun (p, e) ->
+ Printf.sprintf "| (%s, %s)" (Utils.string_of_pos p)
+ (Inference.string_of_equality ?env e))
+ res));
;;
let empty = Index.empty
let init_index = Index.init_index
+let check_disjoint_invariant subst metasenv msg =
+ if (List.exists
+ (fun (i,_,_) -> (List.exists (fun (j,_) -> i=j) subst)) metasenv)
+ then
+ begin
+ prerr_endline ("not disjoint: " ^ msg);
+ assert false
+ end
+;;
+
+let check_for_duplicates metas msg =
+let _ =
+ try
+ ignore(CicUtil.lookup_meta 190 metas);
+ prerr_endline ("eccoci in " ^ msg);
+ with
+ CicUtil.Meta_not_found _ -> () in
+if List.length metas <>
+ List.length (HExtlib.list_uniq (List.sort Pervasives.compare metas)) then
+ begin
+ prerr_endline ("DUPLICATI " ^ msg);
+ prerr_endline (CicMetaSubst.ppmetasenv [] metas);
+ assert false
+ end
+;;
+
+let check_res res msg =
+ match res with
+ Some (t, subst, menv, ug, (eq_found, eq_URI)) ->
+ let eqs = Inference.string_of_equality (snd eq_found) in
+ check_disjoint_invariant subst menv msg;
+ check_for_duplicates menv (msg ^ "\nchecking " ^ eqs);
+ | None -> ()
+;;
+
+let check_target context target msg =
+ let w, proof, (eq_ty, left, right, order), metas, args = target in
+ (* check that metas does not contains duplicates *)
+ let eqs = Inference.string_of_equality target in
+ let _ = check_for_duplicates metas (msg ^ "\nchecking " ^ eqs) in
+ let actual = (Inference.metas_of_term left)@(Inference.metas_of_term right)
+ @(Inference.metas_of_term eq_ty)@(Inference.metas_of_proof proof) in
+ let menv = List.filter (fun (i, _, _) -> List.mem i actual) metas in
+ let _ = if menv <> metas then
+ begin
+ prerr_endline ("extra metas " ^ msg);
+ prerr_endline (CicMetaSubst.ppmetasenv [] metas);
+ prerr_endline "**********************";
+ prerr_endline (CicMetaSubst.ppmetasenv [] menv);
+ prerr_endline ("left: " ^ (CicPp.ppterm left));
+ prerr_endline ("right: " ^ (CicPp.ppterm right));
+ prerr_endline ("ty: " ^ (CicPp.ppterm eq_ty));
+ assert false
+ end
+ else () in
+ try
+ CicTypeChecker.type_of_aux'
+ metas context (Inference.build_proof_term proof) CicUniv.empty_ugraph
+ with e ->
+ prerr_endline msg;
+ prerr_endline (Inference.string_of_proof proof);
+ prerr_endline (CicPp.ppterm (Inference.build_proof_term proof));
+ prerr_endline ("+++++++++++++left: " ^ (CicPp.ppterm left));
+ prerr_endline ("+++++++++++++right: " ^ (CicPp.ppterm right));
+ raise e
+;;
+
+
(* returns a list of all the equalities in the tree that are in relation
"mode" with the given term, where mode can be either Matching or
Unification.
the position will always be Left, and if the ordering is left < right,
position will be Right.
*)
-let get_candidates mode tree term =
+let local_max = ref 100;;
+
+let make_variant (p,eq) =
+ let maxmeta, eq = Inference.fix_metas !local_max eq in
+ local_max := maxmeta;
+ p, eq
+;;
+
+let get_candidates ?env mode tree term =
let t1 = Unix.gettimeofday () in
let res =
let s =
in
Index.PosEqSet.elements s
in
- (* print_candidates mode term res; *)
(* print_endline (Discrimination_tree.string_of_discrimination_tree tree); *)
(* print_newline (); *)
let t2 = Unix.gettimeofday () in
- indexing_retrieval_time := !indexing_retrieval_time +. (t2 -. t1);
- res
+ indexing_retrieval_time := !indexing_retrieval_time +. (t2 -. t1);
+ (* make fresh instances *)
+ res
;;
| [] -> None
| candidate::tl ->
let pos, (_, proof, (ty, left, right, o), metas, args) = candidate in
+ if Utils.debug_metas then
+ ignore(check_target context (snd candidate) "find_matches");
+ if Utils.debug_res then
+ begin
+ let c = "eq = " ^ (Inference.string_of_equality (snd candidate)) ^ "\n"in
+ let t = "t = " ^ (CicPp.ppterm term) ^ "\n" in
+ let m = "metas = " ^ (CicMetaSubst.ppmetasenv [] metas) ^ "\n" in
+ let p = "proof = " ^ (CicPp.ppterm (Inference.build_proof_term proof)) ^ "\n" in
+ check_for_duplicates metas "gia nella metas";
+ check_for_duplicates (metasenv @ metas) ("not disjoint" ^ c ^ t ^ m ^ p)
+ end;
if check && not (fst (CicReduction.are_convertible
~metasenv context termty ty ugraph)) then (
find_matches metasenv context ugraph lift_amount term termty tl
let t1 = Unix.gettimeofday () in
try
let r =
- Inference.matching (metasenv @ metas) context
- term (S.lift lift_amount c) ugraph
+ ( Inference.matching metasenv metas context
+ term (S.lift lift_amount c)) ugraph
in
let t2 = Unix.gettimeofday () in
match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1);
let t2 = Unix.gettimeofday () in
match_unif_time_no := !match_unif_time_no +. (t2 -. t1);
raise e
- | CicUtil.Meta_not_found _ as exn ->
- prerr_endline "zurg";
- raise exn
+ | CicUtil.Meta_not_found _ as exn -> raise exn
in
Some (C.Rel (1 + lift_amount), subst', metasenv', ugraph',
(candidate, eq_URI))
else right, left, Utils.eq_ind_r_URI ()
in
if o <> U.Incomparable then
- try
- do_match c eq_URI
- with Inference.MatchingFailure ->
- find_matches metasenv context ugraph lift_amount term termty tl
+ let res =
+ try
+ do_match c eq_URI
+ with Inference.MatchingFailure ->
+ find_matches metasenv context ugraph lift_amount term termty tl
+ in
+ if Utils.debug_res then ignore (check_res res "find1");
+ res
else
let res =
try do_match c eq_URI
with Inference.MatchingFailure -> None
in
+ if Utils.debug_res then ignore (check_res res "find2");
match res with
| Some (_, s, _, _, _) ->
let c' = apply_subst s c in
let t1 = Unix.gettimeofday () in
try
let r =
- unif_fun (metasenv @ metas) context
+ unif_fun metasenv metas context
term (S.lift lift_amount c) ugraph in
let t2 = Unix.gettimeofday () in
match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1);
let t1 = Unix.gettimeofday () in
try
let r =
- Inference.matching (metasenv @ menv @ m) context what other ugraph
+ Inference.matching menv m context what other ugraph
in
let t2 = Unix.gettimeofday () in
match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1);
r, s
;;
-
-let rec demodulation_aux ?(typecheck=false)
- metasenv context ugraph table lift_amount term =
+let rec demodulation_aux ?from ?(typecheck=false)
+ metasenv context ugraph table lift_amount term =
(* Printf.eprintf "term = %s\n" (CicPp.ppterm term); *)
-
let module C = Cic in
let module S = CicSubstitution in
let module M = CicMetaSubst in
let module HL = HelmLibraryObjects in
- let candidates = get_candidates Matching table term in
- match term with
- | C.Meta _ -> None
- | term ->
- let termty, ugraph =
- if typecheck then
- CicTypeChecker.type_of_aux' metasenv context term ugraph
- else
- C.Implicit None, ugraph
- in
- let res =
- find_matches metasenv context ugraph lift_amount term termty candidates
- in
- if res <> None then
- res
- else
- match term with
- | C.Appl l ->
- let res, ll =
- List.fold_left
- (fun (res, tl) t ->
- if res <> None then
- (res, tl @ [S.lift 1 t])
- else
- let r =
- demodulation_aux metasenv context ugraph table
- lift_amount t
- in
- match r with
- | None -> (None, tl @ [S.lift 1 t])
- | Some (rel, _, _, _, _) -> (r, tl @ [rel]))
- (None, []) l
- in (
- match res with
- | None -> None
- | Some (_, subst, menv, ug, eq_found) ->
- Some (C.Appl ll, subst, menv, ug, eq_found)
- )
- | C.Prod (nn, s, t) ->
- let r1 =
- demodulation_aux metasenv context ugraph table lift_amount s in (
- match r1 with
- | None ->
- let r2 =
- demodulation_aux metasenv
- ((Some (nn, C.Decl s))::context) ugraph
- table (lift_amount+1) t
- in (
- match r2 with
- | None -> None
- | Some (t', subst, menv, ug, eq_found) ->
- Some (C.Prod (nn, (S.lift 1 s), t'),
- subst, menv, ug, eq_found)
- )
- | Some (s', subst, menv, ug, eq_found) ->
- Some (C.Prod (nn, s', (S.lift 1 t)),
- subst, menv, ug, eq_found)
- )
- | C.Lambda (nn, s, t) ->
- let r1 =
- demodulation_aux metasenv context ugraph table lift_amount s in (
- match r1 with
- | None ->
- let r2 =
- demodulation_aux metasenv
- ((Some (nn, C.Decl s))::context) ugraph
- table (lift_amount+1) t
- in (
- match r2 with
- | None -> None
- | Some (t', subst, menv, ug, eq_found) ->
- Some (C.Lambda (nn, (S.lift 1 s), t'),
- subst, menv, ug, eq_found)
- )
- | Some (s', subst, menv, ug, eq_found) ->
- Some (C.Lambda (nn, s', (S.lift 1 t)),
- subst, menv, ug, eq_found)
- )
- | t ->
- None
+ let candidates =
+ get_candidates ~env:(metasenv,context,ugraph) Matching table term in
+(* let candidates = List.map make_variant candidates in *)
+ let res =
+ match term with
+ | C.Meta _ -> None
+ | term ->
+ let termty, ugraph =
+ if typecheck then
+ CicTypeChecker.type_of_aux' metasenv context term ugraph
+ else
+ C.Implicit None, ugraph
+ in
+ let res =
+ find_matches metasenv context ugraph lift_amount term termty candidates
+ in
+ if Utils.debug_res then ignore(check_res res "demod1");
+ if res <> None then
+ res
+ else
+ match term with
+ | C.Appl l ->
+ let res, ll =
+ List.fold_left
+ (fun (res, tl) t ->
+ if res <> None then
+ (res, tl @ [S.lift 1 t])
+ else
+ let r =
+ demodulation_aux ~from:"1" metasenv context ugraph table
+ lift_amount t
+ in
+ match r with
+ | None -> (None, tl @ [S.lift 1 t])
+ | Some (rel, _, _, _, _) -> (r, tl @ [rel]))
+ (None, []) l
+ in (
+ match res with
+ | None -> None
+ | Some (_, subst, menv, ug, eq_found) ->
+ Some (C.Appl ll, subst, menv, ug, eq_found)
+ )
+ | C.Prod (nn, s, t) ->
+ let r1 =
+ demodulation_aux ~from:"2"
+ metasenv context ugraph table lift_amount s in (
+ match r1 with
+ | None ->
+ let r2 =
+ demodulation_aux metasenv
+ ((Some (nn, C.Decl s))::context) ugraph
+ table (lift_amount+1) t
+ in (
+ match r2 with
+ | None -> None
+ | Some (t', subst, menv, ug, eq_found) ->
+ Some (C.Prod (nn, (S.lift 1 s), t'),
+ subst, menv, ug, eq_found)
+ )
+ | Some (s', subst, menv, ug, eq_found) ->
+ Some (C.Prod (nn, s', (S.lift 1 t)),
+ subst, menv, ug, eq_found)
+ )
+ | C.Lambda (nn, s, t) ->
+ let r1 =
+ demodulation_aux
+ metasenv context ugraph table lift_amount s in (
+ match r1 with
+ | None ->
+ let r2 =
+ demodulation_aux metasenv
+ ((Some (nn, C.Decl s))::context) ugraph
+ table (lift_amount+1) t
+ in (
+ match r2 with
+ | None -> None
+ | Some (t', subst, menv, ug, eq_found) ->
+ Some (C.Lambda (nn, (S.lift 1 s), t'),
+ subst, menv, ug, eq_found)
+ )
+ | Some (s', subst, menv, ug, eq_found) ->
+ Some (C.Lambda (nn, s', (S.lift 1 t)),
+ subst, menv, ug, eq_found)
+ )
+ | t ->
+ None
+ in
+ if Utils.debug_res then ignore(check_res res "demod_aux output");
+ res
;;
let demod_counter = ref 1;;
+exception Foo
+
(** demodulation, when target is an equality *)
-let rec demodulation_equality newmeta env table sign target =
+let rec demodulation_equality ?from newmeta env table sign target =
let module C = Cic in
let module S = CicSubstitution in
let module M = CicMetaSubst in
let w = Utils.compute_equality_weight eq_ty left right in
let order = !Utils.compare_terms left right in
let target = w, proof, (eq_ty, left, right, order), metas, args in
-
- let metasenv' = metasenv @ metas in
-
+ if Utils.debug_metas then
+ ignore(check_target context target "demod equalities input");
+ let metasenv' = (* metasenv @ *) metas in
let maxmeta = ref newmeta in
let build_newtarget is_left (t, subst, menv, ug, (eq_found, eq_URI)) =
let time1 = Unix.gettimeofday () in
+ if Utils.debug_metas then
+ begin
+ ignore(check_for_duplicates menv "input1");
+ ignore(check_disjoint_invariant subst menv "input2");
+ let substs = CicMetaSubst.ppsubst subst in
+ ignore(check_target context (snd eq_found) ("input3" ^ substs))
+ end;
let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found in
let ty =
- try fst (CicTypeChecker.type_of_aux' metasenv context what ugraph)
+ try fst (CicTypeChecker.type_of_aux' metasenv context what ugraph)
with CicUtil.Meta_not_found _ -> ty
in
let what, other = if pos = Utils.Left then what, other else other, what in
let newterm, newproof =
let bo = Utils.guarded_simpl context (apply_subst subst (S.subst other t)) in
- let name = C.Name ("x_Demod_" ^ (string_of_int !demod_counter)) in
+ let name = C.Name ("x_Demod" ^ (string_of_int !demod_counter)) in
incr demod_counter;
let bo' =
let l, r = if is_left then t, S.lift 1 right else S.lift 1 left, t in
- C.Appl [C.MutInd (LibraryObjects.eq_URI (), 0, []);
- S.lift 1 eq_ty; l; r]
+ C.Appl [C.MutInd (LibraryObjects.eq_URI (), 0, []);
+ S.lift 1 eq_ty; l; r]
in
if sign = Utils.Positive then
- (bo,
- Inference.ProofBlock (
- subst, eq_URI, (name, ty), bo'(* t' *), eq_found, proof))
+ (bo,
+ Inference.ProofBlock (
+ subst, eq_URI, (name, ty), bo'(* t' *), eq_found, proof))
else
let metaproof =
incr maxmeta;
in
match proof with
| Inference.BasicProof _ ->
- print_endline "replacing a BasicProof";
+ (* print_endline "replacing a BasicProof"; *)
pb
| Inference.ProofGoalBlock (_, parent_proof) ->
- print_endline "replacing another ProofGoalBlock";
+
+ (* print_endline "replacing another ProofGoalBlock"; *)
Inference.ProofGoalBlock (pb, parent_proof)
| _ -> assert false
in
(bo,
Inference.ProofGoalBlock (Inference.BasicProof refl, target_proof))
in
- let left, right = if is_left then newterm, right else left, newterm in
- let m =
- (Inference.metas_of_term left)
- @ (Inference.metas_of_term right)
- @ (Inference.metas_of_term eq_ty) in
- (* let newmetasenv = List.filter (fun (i, _, _) -> List.mem i m) (metas @ menv') *)
- let newmetasenv = List.filter (fun (i, _, _) -> List.mem i m) (metasenv' @ menv')
- and newargs = args
+ let newmenv = (* Inference.filter subst *) menv in
+ let _ =
+ if Utils.debug_metas then
+ try ignore(CicTypeChecker.type_of_aux'
+ newmenv context (Inference.build_proof_term newproof) ugraph);
+ ()
+ with exc ->
+ prerr_endline "sempre lui";
+ prerr_endline (CicMetaSubst.ppsubst subst);
+ prerr_endline (CicPp.ppterm (Inference.build_proof_term newproof));
+ prerr_endline ("+++++++++++++termine: " ^ (CicPp.ppterm t));
+ prerr_endline ("+++++++++++++what: " ^ (CicPp.ppterm what));
+ prerr_endline ("+++++++++++++other: " ^ (CicPp.ppterm other));
+ prerr_endline ("+++++++++++++subst: " ^ (CicMetaSubst.ppsubst subst));
+ raise exc;
+ else ()
in
+ let left, right = if is_left then newterm, right else left, newterm in
let ordering = !Utils.compare_terms left right in
-
let time2 = Unix.gettimeofday () in
build_newtarget_time := !build_newtarget_time +. (time2 -. time1);
-
let res =
let w = Utils.compute_equality_weight eq_ty left right in
- (w, newproof, (eq_ty, left, right, ordering), newmetasenv, newargs)
- in
- !maxmeta, res
- in
- let _ =
- try
- CicTypeChecker.type_of_aux' metasenv' context left ugraph;
- CicTypeChecker.type_of_aux' metasenv' context right ugraph;
- with
- CicUtil.Meta_not_found _ as exn ->
- begin
- prerr_endline "siamo in demodulation_equality 1";
- prerr_endline (CicPp.ppterm left);
- prerr_endline (CicPp.ppterm right);
- raise exn
- end
+ (w, newproof, (eq_ty, left, right, ordering),newmenv,args) in
+ if Utils.debug_metas then
+ ignore(check_target context res "buildnew_target output");
+ !maxmeta, res
in
- let res = demodulation_aux metasenv' context ugraph table 0 left in
+
+ let res = demodulation_aux ~from:"3" metasenv' context ugraph table 0 left in
+ if Utils.debug_res then check_res res "demod result";
let newmeta, newtarget =
match res with
| Some t ->
if (Inference.is_weak_identity (metasenv', context, ugraph) newtarget) ||
(Inference.meta_convertibility_eq target newtarget) then
newmeta, newtarget
- else
+ else
demodulation_equality newmeta env table sign newtarget
| None ->
let res = demodulation_aux metasenv' context ugraph table 0 right in
+ if Utils.debug_res then check_res res "demod result 1";
match res with
| Some t ->
let newmeta, newtarget = build_newtarget false t in
(Inference.meta_convertibility_eq target newtarget) then
newmeta, newtarget
else
- demodulation_equality newmeta env table sign newtarget
+ demodulation_equality newmeta env table sign newtarget
| None ->
newmeta, target
in
let module M = CicMetaSubst in
let module HL = HelmLibraryObjects in
let candidates = get_candidates Unification table term in
+
let res, lifted_term =
match term with
| C.Meta (i, l) ->
let module CR = CicReduction in
let module U = Utils in
let weight, proof, (eq_ty, left, right, ordering), menv, _ = target in
+ if Utils.debug_metas then
+ ignore(check_target context target "superpositionleft");
let expansions, _ =
let term = if ordering = U.Gt then left else right in
- betaexpand_term metasenv context ugraph table 0 term
+ begin
+ let t1 = Unix.gettimeofday () in
+ let res = betaexpand_term metasenv context ugraph table 0 term in
+ let t2 = Unix.gettimeofday () in
+ beta_expand_time := !beta_expand_time +. (t2 -. t1);
+ res
+ end
in
let maxmeta = ref newmeta in
let build_new (bo, s, m, ug, (eq_found, eq_URI)) =
-
(* debug_print (lazy "\nSUPERPOSITION LEFT\n"); *)
-
let time1 = Unix.gettimeofday () in
let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found in
let left, right =
if ordering = U.Gt then newgoal, right else left, newgoal in
let neworder = !Utils.compare_terms left right in
-
+ let newmenv = (* Inference.filter s *) menv in
let time2 = Unix.gettimeofday () in
build_newtarget_time := !build_newtarget_time +. (time2 -. time1);
- let res =
- let w = Utils.compute_equality_weight eq_ty left right in
- (w, newproof, (eq_ty, left, right, neworder), menv @ menv', [])
- in
- res
+ let w = Utils.compute_equality_weight eq_ty left right in
+ (w, newproof, (eq_ty, left, right, neworder), newmenv, [])
+
in
!maxmeta, List.map build_new expansions
;;
let module M = CicMetaSubst in
let module HL = HelmLibraryObjects in
let module CR = CicReduction in
- let module U = Utils in
- let _, eqproof, (eq_ty, left, right, ordering), newmetas, args = target in
- let metasenv' = metasenv @ newmetas in
+ let module U = Utils in
+ let w, eqproof, (eq_ty, left, right, ordering), newmetas, args = target in
+ if Utils.debug_metas then
+ ignore (check_target context target "superpositionright");
+ let metasenv' = newmetas in
let maxmeta = ref newmeta in
let res1, res2 =
+ let betaexpand_term metasenv context ugraph table d term =
+ let t1 = Unix.gettimeofday () in
+ let res = betaexpand_term metasenv context ugraph table d term in
+ let t2 = Unix.gettimeofday () in
+ beta_expand_time := !beta_expand_time +. (t2 -. t1);
+ res
+ in
match ordering with
| U.Gt -> fst (betaexpand_term metasenv' context ugraph table 0 left), []
| U.Lt -> [], fst (betaexpand_term metasenv' context ugraph table 0 right)
in
(res left right), (res right left)
in
- let build_new ordering (bo, s, m, ug, (eq_found, eq_URI)) =
-
+ let build_new ordering ((bo, s, m, ug, (eq_found, eq_URI)) as input) =
+ if Utils.debug_metas then
+ ignore (check_target context (snd eq_found) "buildnew1" );
let time1 = Unix.gettimeofday () in
let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found in
let left, right =
if ordering = U.Gt then newgoal, apply_subst s right
else apply_subst s left, newgoal in
- let neworder = !Utils.compare_terms left right
- and newmenv = newmetas @ menv'
- and newargs = args @ args' in
+ let neworder = !Utils.compare_terms left right in
+ let newmenv = (* Inference.filter s *) m in
+ let newargs = args @ args' in
let eq' =
let w = Utils.compute_equality_weight eq_ty left right in
(w, newproof, (eq_ty, left, right, neworder), newmenv, newargs) in
+ if Utils.debug_metas then
+ ignore (check_target context eq' "buildnew3");
let newm, eq' = Inference.fix_metas !maxmeta eq' in
+ if Utils.debug_metas then
+ ignore (check_target context eq' "buildnew4");
newm, eq'
in
maxmeta := newmeta;
-
let time2 = Unix.gettimeofday () in
build_newtarget_time := !build_newtarget_time +. (time2 -. time1);
-
+ if Utils.debug_metas then
+ ignore(check_target context newequality "buildnew2");
newequality
in
let new1 = List.map (build_new U.Gt) res1
and new2 = List.map (build_new U.Lt) res2 in
-(*
- let ok e = not (Inference.is_identity (metasenv, context, ugraph) e) in
-*)
let ok e = not (Inference.is_identity (metasenv', context, ugraph) e) in
(!maxmeta,
(List.filter ok (new1 @ new2)))
let proof, metas, term = goal in
let term = Utils.guarded_simpl (~debug:true) context term in
let goal = proof, metas, term in
- let metasenv' = metasenv @ metas in
+ let metasenv' = metas in
let build_newgoal (t, subst, menv, ug, (eq_found, eq_URI)) =
let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found in
with CicUtil.Meta_not_found _ -> ty
in
let newterm, newproof =
- (* qua *)
let bo = Utils.guarded_simpl context (apply_subst subst (S.subst other t)) in
let bo' = apply_subst subst t in
let name = C.Name ("x_DemodGoal_" ^ (string_of_int !demod_counter)) in
in
bo, Inference.ProofGoalBlock (Inference.NoProof, goal_proof)
in
- let m = Inference.metas_of_term newterm in
- (* QUA *)
- let newmetasenv = List.filter (fun (i, _, _) -> List.mem i m) (menv @ menv')in
+ let newmetasenv = (* Inference.filter subst *) menv in
!maxmeta, (newproof, newmetasenv, newterm)
in
let res =
- demodulation_aux ~typecheck:true metasenv' context ugraph table 0 term
+ demodulation_aux (* ~typecheck:true *) metasenv' context ugraph table 0 term
in
match res with
| Some t ->
let metasenv, context, ugraph = env in
let maxmeta = ref newmeta in
let term, termty, metas = theorem in
- let metasenv' = metasenv @ metas in
+ let metasenv' = metas in
let build_newtheorem (t, subst, menv, ug, (eq_found, eq_URI)) =
let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found in
let what, other = if pos = Utils.Left then what, other else other, what in
let newterm, newty =
- (* qua *)
let bo = Utils.guarded_simpl context (apply_subst subst (S.subst other t)) in
let bo' = apply_subst subst t in
let name = C.Name ("x_DemodThm_" ^ (string_of_int !demod_counter)) in
in
let m = Inference.metas_of_term newterm in
- let newmetasenv = List.filter (fun (i, _, _) -> List.mem i m) (metas @ menv') in
- !maxmeta, (newterm, newty, newmetasenv)
+ !maxmeta, (newterm, newty, menv)
in
let res =
- demodulation_aux ~typecheck:true metasenv' context ugraph table 0 termty
+ demodulation_aux (* ~typecheck:true *) metasenv' context ugraph table 0 termty
in
match res with
| Some t ->
(* $Id$ *)
+val beta_expand_time : float ref
+
module Index :
sig
module PosEqSet : Set.S
bool * Cic.substitution
val superposition_left :
int ->
- Cic.metasenv * Cic.context * CicUniv.universe_graph ->
+ Cic.conjecture list * Cic.context * CicUniv.universe_graph ->
Index.t ->
- 'a * Inference.proof *
- (Index.key * Index.key * Index.key * Utils.comparison) * Cic.metasenv * 'c ->
- int *
- (int * Inference.proof *
- (Index.key * Index.key * Index.key * Utils.comparison) * Cic.metasenv *
- 'e list)
- list
+ Inference.equality ->
+ int * Inference.equality list
+
val superposition_right :
int ->
- Cic.metasenv * Cic.context * CicUniv.universe_graph ->
+ 'a * Cic.context * CicUniv.universe_graph ->
Index.t ->
- 'a * Inference.proof *
- (Cic.term * Index.key * Index.key * Utils.comparison) *
- Cic.metasenv * Cic.term list -> int * Inference.equality list
+ Inference.equality ->
+ int * Inference.equality list
+
val demodulation_equality :
+ ?from:string ->
int ->
Cic.metasenv * Cic.context * CicUniv.universe_graph ->
Index.t ->
Index.t ->
Cic.term * Index.key * Cic.metasenv ->
'a * (Cic.term * Index.key * Cic.metasenv)
+val check_target:
+ Cic.context ->
+ Inference.equality -> string -> Cic.term * CicUniv.universe_graph
+(* maxmeta for relocate *)
+val local_max : int ref
open Utils;;
+let metas_of_proof_time = ref 0.;;
+let metas_of_term_time = ref 0.;;
type equality =
int * (* weight *)
| SubProof of Cic.term * int * proof
;;
-
let string_of_equality ?env =
match env with
| None -> (
Printf.sprintf "SubProof(%s, %s, %s)"
(CicPp.ppterm t) (string_of_int i) (string_of_proof p)
| ProofSymBlock _ -> "ProofSymBlock"
- | ProofBlock _ -> "ProofBlock"
+ | ProofBlock (subst, _, _, _ ,_,_) ->
+ "ProofBlock" ^ (CicMetaSubst.ppsubst subst)
| ProofGoalBlock (p1, p2) ->
Printf.sprintf "ProofGoalBlock(%s, %s)"
(string_of_proof p1) (string_of_proof p2)
;;
+let check_disjoint_invariant subst metasenv msg =
+ if (List.exists
+ (fun (i,_,_) -> (List.exists (fun (j,_) -> i=j) subst)) metasenv)
+ then
+ begin
+ prerr_endline ("not disjoint: " ^ msg);
+ assert false
+ end
+;;
+
+(* filter out from metasenv the variables in substs *)
+let filter subst metasenv =
+ List.filter
+ (fun (m, _, _) ->
+ try let _ = List.find (fun (i, _) -> m = i) subst in false
+ with Not_found -> true)
+ metasenv
+;;
+
(* returns an explicit named subst and a list of arguments for sym_eq_URI *)
let build_ens_for_sym_eq sym_eq_URI termlist =
let obj, _ = CicEnvironment.get_obj CicUniv.empty_ugraph sym_eq_URI in
| _ -> []
;;
+let rec metas_of_proof p =
+ if Utils.debug then
+ let t1 = Unix.gettimeofday () in
+ let res = metas_of_term (build_proof_term p) in
+ let t2 = Unix.gettimeofday () in
+ metas_of_proof_time := !metas_of_proof_time +. (t2 -. t1);
+ res
+ else
+ metas_of_term (build_proof_term p)
+;;
exception NotMetaConvertible;;
| C.Meta (i, l), t -> (
try
let _, _, ty = CicUtil.lookup_meta i menv in
- let subst =
- if not (List.mem_assoc i subst) then (i, (context, t, ty))::subst
- else subst
- in
+ assert (not (List.mem_assoc i subst));
+ let subst = (i, (context, t, ty))::subst in
let menv = menv in (* List.filter (fun (m, _, _) -> i <> m) menv in *)
subst, menv
with CicUtil.Meta_not_found m ->
raise (U.UnificationFailure (lazy "Inference.unification.unif"))
in
let subst, menv = unif [] metasenv t1 t2 in
- let menv =
- List.filter
- (fun (m, _, _) ->
- try let _ = List.find (fun (i, _) -> m = i) subst in false
- with Not_found -> true)
- menv
- in
+ let menv = filter subst menv in
List.rev subst, menv, ugraph
;;
-let unification metasenv context t1 t2 ugraph =
+let unification metasenv1 metasenv2 context t1 t2 ugraph =
+ let metasenv = metasenv1 metasenv2 in
let subst, menv, ug =
if not (is_simple_term t1) || not (is_simple_term t2) then (
debug_print
) else
unification_simple metasenv context t1 t2 ugraph
in
+ if Utils.debug_res then
+ ignore(check_disjoint_invariant subst menv "unif");
+ let subst =
+ List.map
+ (fun (i, (context, term, ty)) ->
+ let context = CicMetaSubst.apply_subst_context subst context in
+ let term = CicMetaSubst.apply_subst subst term in
+ let ty = CicMetaSubst.apply_subst subst ty in
+ (i, (context, term, ty))) subst in
+(*
let rec fix_term = function
| (Cic.Meta (i, l) as t) ->
let t' = lookup_subst t subst in
let rec fix_subst = function
| [] -> []
| (i, (c, t, ty))::tl -> (i, (c, fix_term t, fix_term ty))::(fix_subst tl)
- in
- fix_subst subst, menv, ug
+ in
+ fix_subst subst, menv, ug *)
+ subst, menv, ug
;;
-let unification = CicUnification.fo_unif;;
+let unification metasenv1 metasenv2 context t1 t2 ugraph =
+ let (subst, metasenv, ugraph) =
+ CicUnification.fo_unif (metasenv1@metasenv2) context t1 t2 ugraph in
+ if Utils.debug_res then
+ ignore(check_disjoint_invariant subst metasenv "fo_unif");
+ (subst, metasenv, ugraph)
+
+;;
exception MatchingFailure;;
;;
*)
-
+(*
let matching metasenv context t1 t2 ugraph =
try
let subst, metasenv, ugraph =
-try
+ try
unification metasenv context t1 t2 ugraph
-with CicUtil.Meta_not_found _ as exn ->
- Printf.eprintf "t1 == %s\nt2 = %s\nmetasenv == %s\n%!"
- (CicPp.ppterm t1) (CicPp.ppterm t2) (CicMetaSubst.ppmetasenv [] metasenv);
- raise exn
+ with CicUtil.Meta_not_found _ as exn ->
+ Printf.eprintf "t1 == %s\nt2 = %s\nmetasenv == %s\n%!"
+ (CicPp.ppterm t1) (CicPp.ppterm t2)
+ (CicMetaSubst.ppmetasenv [] metasenv);
+ raise exn
in
+ if Utils.debug_res then
+ ignore(check_disjoint_invariant subst metasenv "qua-2");
let t' = CicMetaSubst.apply_subst subst t1 in
if not (meta_convertibility t1 t') then
raise MatchingFailure
else
+ if Utils.debug_res then
+ ignore(check_disjoint_invariant subst metasenv "qua-1");
let metas = metas_of_term t1 in
+ let subst =
+ List.map
+ (fun (i, (context, term, ty)) ->
+ let context = CicMetaSubst.apply_subst_context subst context in
+ let term = CicMetaSubst.apply_subst subst term in
+ let ty = CicMetaSubst.apply_subst subst ty in
+ (i, (context, term, ty))) subst in
+ if Utils.debug_res then
+ ignore(check_disjoint_invariant subst metasenv "qua0");
+
+ let subst, metasenv =
+ List.fold_left
+ (fun
+ (subst,metasenv) s ->
+ match s with
+ | (i, (c, Cic.Meta (j, lc), ty)) when List.mem i metas ->
+ let metasenv' =
+ List.filter (fun (x, _, _) -> x<>j) metasenv
+ in
+ ((j, (c, Cic.Meta (i, lc), ty))::subst,
+ (i,c,ty)::metasenv')
+ |_ -> s::subst,metasenv) ([],metasenv) subst
+ in
+ if Utils.debug_res then
+ ignore(check_disjoint_invariant subst metasenv "qua1");
+(*
let fix_subst = function
| (i, (c, Cic.Meta (j, lc), ty)) when List.mem i metas ->
(j, (c, Cic.Meta (i, lc), ty))
| s -> s
in
- let subst = List.map fix_subst subst in
- subst, metasenv, ugraph
+ let subst = List.map fix_subst subst in *)
+ if CicMetaSubst.apply_subst subst t1 = t1 then
+ subst, metasenv, ugraph
+ else
+ (prerr_endline "mah"; raise MatchingFailure)
with
| CicUnification.UnificationFailure _
| CicUnification.Uncertain _ ->
raise MatchingFailure
;;
+*)
+
+(** matching takes in input the _disjoint_ metasenv of t1 and t2;
+it perform unification in the union metasenv, then check that
+the first metasenv has not changed *)
+
+let matching metasenv1 metasenv2 context t1 t2 ugraph =
+ let subst, metasenv, ugraph =
+ try
+ unification metasenv1 metasenv2 context t1 t2 ugraph
+ with
+ CicUtil.Meta_not_found _ as exn ->
+ Printf.eprintf "t1 == %s\nt2 = %s\nmetasenv == %s\n%!"
+ (CicPp.ppterm t1) (CicPp.ppterm t2)
+ (CicMetaSubst.ppmetasenv [] (metasenv1@metasenv2));
+ raise exn
+ | CicUnification.UnificationFailure _
+ | CicUnification.Uncertain _ ->
+ raise MatchingFailure
+ in
+ if Utils.debug_res then
+ ignore(check_disjoint_invariant subst metasenv "qua-2");
+ (* let us unfold subst *)
+ if metasenv = metasenv1 then
+ subst, metasenv, ugraph (* everything is fine *)
+ else
+ (* let us unfold subst *)
+ let subst =
+ List.map
+ (fun (i, (context, term, ty)) ->
+ let context = CicMetaSubst.apply_subst_context subst context in
+ let term = CicMetaSubst.apply_subst subst term in
+ let ty = CicMetaSubst.apply_subst subst ty in
+ (i, (context, term, ty))) subst in
+ (* let us revert Meta-Meta in subst privileging metasenv1 *)
+ let subst, metasenv =
+ List.fold_left
+ (fun
+ (subst,metasenv) s ->
+ match s with
+ | (i, (c, Cic.Meta (j, lc), ty))
+ when (List.exists (fun (x, _, _) -> x=i) metasenv1) &&
+ not (List.exists (fun (x, _) -> x=j) subst) ->
+ let metasenv' =
+ List.filter (fun (x, _, _) -> x<>j) metasenv
+ in
+ ((j, (c, Cic.Meta (i, lc), ty))::subst,
+ (i,c,ty)::metasenv')
+ |_ -> s::subst,metasenv) ([],metasenv) subst
+ in
+ (* finally, let us chek again that metasenv = metasenv1 *)
+ if metasenv = metasenv1 then
+ subst, metasenv, ugraph
+ else raise MatchingFailure
+;;
+let check_eq context msg eq =
+ let w, proof, (eq_ty, left, right, order), metas, args = eq in
+ if not (fst (CicReduction.are_convertible ~metasenv:metas context eq_ty
+ (fst (CicTypeChecker.type_of_aux' metas context left CicUniv.empty_ugraph))
+ CicUniv.empty_ugraph))
+ then
+ begin
+ prerr_endline msg;
+ assert false;
+ end
+ else ()
+;;
let find_equalities context proof =
let module C = Cic in
)
| C.Appl [C.MutInd (uri, _, _); ty; t1; t2]
when UriManager.eq uri eq_uri ->
- let t1 = S.lift index t1
- and t2 = S.lift index t2 in
+ let ty = S.lift index ty in
+ let t1 = S.lift index t1 in
+ let t2 = S.lift index t2 in
let o = !Utils.compare_terms t1 t2 in
let w = compute_equality_weight ty t1 t2 in
let e = (w, BasicProof (C.Rel index), (ty, t1, t2, o), [], []) in
in
let il, maxm = aux 1 newmeta context in
let indexes, equalities = List.split il in
+ ignore (List.iter (check_eq context "find") equalities);
indexes, equalities, maxm
;;
let ty = repl ty
and left = repl left
and right = repl right in
- let metas = (metas_of_term left) @ (metas_of_term right) @ (metas_of_term ty) in
+ let metas =
+ (metas_of_term left) @
+ (metas_of_term right) @
+ (metas_of_term ty) @ (metas_of_proof p) in
let menv' = List.filter (fun (i, _, _) -> List.mem i metas) menv' in
let newargs =
List.filter
let fix_metas newmeta (w, p, (ty, left, right, o), menv, args) =
+ (*
+ let metas = (metas_of_term left)@(metas_of_term right)
+ @(metas_of_term ty)@(metas_of_proof p) in
+ let menv = List.filter (fun (i, _, _) -> List.mem i metas) menv in
+ *)
(* debug
let _ , eq =
fix_metas_old newmeta (w, p, (ty, left, right, o), menv, args) in
| NoProof -> NoProof
| BasicProof term -> BasicProof (CicMetaSubst.apply_subst subst term)
| ProofBlock (subst', eq_URI, namety, bo, (pos, eq), p) ->
- ProofBlock (subst' @ subst, eq_URI, namety, bo, (pos, eq), p)
+ (*
+ let newsubst =
+ List.map
+ (fun (i, (context, term, ty)) ->
+ let context = CicMetaSubst.apply_subst_context subst context in
+ let term = CicMetaSubst.apply_subst subst term in
+ let ty = CicMetaSubst.apply_subst subst ty in
+ (i, (context, term, ty))) subst' in *)
+ ProofBlock (subst@subst', eq_URI, namety, bo, (pos, eq), p)
| p -> assert false
in
- let metas = (metas_of_term left)@(metas_of_term right)@(metas_of_term ty) in
+ let p = fix_proof p in
+ (*
+ let metas = (metas_of_term left)@(metas_of_term right)
+ @(metas_of_term ty)@(metas_of_proof p) in
let metasenv = List.filter (fun (i, _, _) -> List.mem i metas) metasenv in
- let eq = (w, fix_proof p, (ty, left, right, o), metasenv, args) in
+ *)
+ let eq = (w, p, (ty, left, right, o), metasenv, args) in
(* debug prerr_endline (string_of_equality eq); *)
- newmeta, eq
+ newmeta+1, eq
let term_is_equality term =
let iseq uri = UriManager.eq uri (LibraryObjects.eq_URI ()) in
let term_of_equality equality =
- let _, _, (ty, left, right, _), menv, args = equality in
+ let _, _, (ty, left, right, _), menv, _ = equality in
let eq i = function Cic.Meta (j, _) -> i = j | _ -> false in
- let argsno = List.length args in
+ let argsno = List.length menv in
let t =
CicSubstitution.lift argsno
(Cic.Appl [Cic.MutInd (LibraryObjects.eq_URI (), 0, []); ty; left; right])
in
snd (
List.fold_right
- (fun a (n, t) ->
- match a with
- | Cic.Meta (i, _) ->
- let name = Cic.Name ("X" ^ (string_of_int n)) in
- let _, _, ty = CicUtil.lookup_meta i menv in
- let t =
- ProofEngineReduction.replace
- ~equality:eq ~what:[i]
- ~with_what:[Cic.Rel (argsno - (n - 1))] ~where:t
- in
- (n-1, Cic.Prod (name, ty, t))
- | _ -> assert false)
- args (argsno, t))
+ (fun (i,_,ty) (n, t) ->
+ let name = Cic.Name ("X" ^ (string_of_int n)) in
+ let ty = CicSubstitution.lift (n-1) ty in
+ let t =
+ ProofEngineReduction.replace
+ ~equality:eq ~what:[i]
+ ~with_what:[Cic.Rel (argsno - (n - 1))] ~where:t
+ in
+ (n-1, Cic.Prod (name, ty, t)))
+ menv (argsno, t))
;;
* http://cs.unibo.it/helm/.
*)
+val metas_of_proof_time : float ref
+
type equality =
int * (* weight *)
proof * (* proof *)
val string_of_proof: proof -> string
+val filter : Cic.substitution -> Cic.metasenv -> Cic.metasenv
+
exception MatchingFailure
(** matching between two terms. Can raise MatchingFailure *)
val matching:
- Cic.metasenv -> Cic.context -> Cic.term -> Cic.term ->
+ Cic.metasenv -> Cic.metasenv -> Cic.context -> Cic.term -> Cic.term ->
CicUniv.universe_graph ->
Cic.substitution * Cic.metasenv * CicUniv.universe_graph
such case should be significantly faster than CicUnification.fo_unif
*)
val unification:
- Cic.metasenv -> Cic.context -> Cic.term -> Cic.term ->
+ Cic.metasenv -> Cic.metasenv -> Cic.context -> Cic.term -> Cic.term ->
CicUniv.universe_graph ->
Cic.substitution * Cic.metasenv * CicUniv.universe_graph
val string_of_equality: ?env:environment -> equality -> string
val metas_of_term: Cic.term -> int list
+val metas_of_proof: proof -> int list
(** ensures that metavariables in equality are unique *)
val fix_metas: int -> equality -> int * equality
open Inference;;
open Utils;;
+
(*
for debugging
let check_equation env equation msg =
(* equality-selection related globals *)
let use_fullred = ref true;;
-let weight_age_ratio = ref (* 5 *) 4;; (* settable by the user *)
-let weight_age_counter = ref !weight_age_ratio;;
-let symbols_ratio = ref (* 0 *) 3;;
+let weight_age_ratio = ref 4 (* 5 *);; (* settable by the user *)
+let weight_age_counter = ref !weight_age_ratio ;;
+let symbols_ratio = ref 0 (* 3 *);;
let symbols_counter = ref 0;;
(* non-recursive Knuth-Bendix term ordering by default *)
with Failure "hd" -> Pervasives.compare eq1 eq2
)
| res -> res
-end
+end
module EqualitySet = Set.Make(OrderedEquality);;
+exception Empty_list;;
+
+let passive_is_empty = function
+ | ([], _), ([], _), _ -> true
+ | _ -> false
+;;
+
+
+let size_of_passive ((_, ns), (_, ps), _) =
+ (EqualitySet.cardinal ns) + (EqualitySet.cardinal ps)
+;;
+
+
+let size_of_active (active_list, _) =
+ List.length active_list
+;;
+
+let age_factor = 0.01;;
+
+let min_elt weight l =
+ fst
+ (match l with
+ [] -> raise Empty_list
+ | a::tl ->
+ let wa = float_of_int (weight a) in
+ let x = ref 0. in
+ List.fold_left
+ (fun (current,w) arg ->
+ x:=!x +. 1.;
+ let w1 = weight arg in
+ let wa = (float_of_int w1) +. !x *. age_factor in
+ if wa < w then (arg,wa) else (current,w))
+ (a,wa) tl)
+;;
+
+(*
+let compare eq1 eq2 =
+ let w1, _, (ty, left, right, _), m1, _ = eq1 in
+ let w2, _, (ty', left', right', _), m2, _ = eq2 in
+ match Pervasives.compare w1 w2 with
+ | 0 -> (List.length m1) - (List.length m2)
+ | res -> res
+;;
+*)
(**
selects one equality from passive. The selection strategy is a combination
of weight, age and goal-similarity
*)
-let select env goals passive (active, _) =
+let rec select env goals passive (active, _) =
processed_clauses := !processed_clauses + 1;
let goal =
match (List.rev goals) with (_, goal::_)::_ -> goal | _ -> assert false
(Negative, hd),
((tl, EqualitySet.remove hd neg_set), (pos, pos_set), passive_table)
| [], (hd:EqualitySet.elt)::tl ->
+ let w,_,_,_,_ = hd in
let passive_table =
- Indexing.remove_index passive_table hd
- in
- (Positive, hd),
+ Indexing.remove_index passive_table hd
+ in (Positive, hd),
(([], neg_set), (tl, EqualitySet.remove hd pos_set), passive_table)
| _, _ -> assert false
)
- | _ when (!symbols_counter > 0) && (EqualitySet.is_empty neg_set) -> (
- symbols_counter := !symbols_counter - 1;
+ | _ when (!symbols_counter > 0) && (EqualitySet.is_empty neg_set) ->
+ (symbols_counter := !symbols_counter - 1;
let cardinality map =
TermMap.fold (fun k v res -> res + v) map 0
in
)
| _ ->
symbols_counter := !symbols_ratio;
- let set_selection set = EqualitySet.min_elt set in
+ (* let set_selection set = EqualitySet.min_elt set in *)
+ let set_selection l = min_elt (fun (w,_,_,_,_) -> w) l in
if EqualitySet.is_empty neg_set then
- let current = set_selection pos_set in
+ let current = set_selection pos_list in
let passive =
(neg_list, neg_set),
(remove current pos_list, EqualitySet.remove current pos_set),
in
(Positive, current), passive
else
- let current = set_selection neg_set in
+ let current = set_selection neg_list in
let passive =
(remove current neg_list, EqualitySet.remove current neg_set),
(pos_list, pos_set),
;;
-let passive_is_empty = function
- | ([], _), ([], _), _ -> true
- | _ -> false
-;;
-
-
-let size_of_passive ((_, ns), (_, ps), _) =
- (EqualitySet.cardinal ns) + (EqualitySet.cardinal ps)
-;;
-
-
-let size_of_active (active_list, _) =
- List.length active_list
-;;
-
-
(* removes from passive equalities that are estimated impossible to activate
within the current time limit *)
let prune_passive howmany (active, _) passive =
(** inference of new equalities between current and some in active *)
let infer env sign current (active_list, active_table) =
+ let (_,c,_) = env in
+ if Utils.debug_metas then
+ (ignore(Indexing.check_target c current "infer1");
+ ignore(List.map (function (_,current) -> Indexing.check_target c current "infer2") active_list));
let new_neg, new_pos =
match sign with
| Negative ->
let maxm, res =
Indexing.superposition_left !maxmeta env active_table current in
+ if Utils.debug_metas then
+ ignore(List.map
+ (function current ->
+ Indexing.check_target c current "sup-1") res);
maxmeta := maxm;
res, []
| Positive ->
let maxm, res =
Indexing.superposition_right !maxmeta env active_table current in
- maxmeta := maxm;
+ if Utils.debug_metas then
+ ignore(List.map
+ (function current ->
+ Indexing.check_target c current "sup0") res);
+ maxmeta := maxm;
let rec infer_positive table = function
| [] -> [], []
| (Negative, equality)::tl ->
let maxm, res =
Indexing.superposition_left !maxmeta env table equality in
maxmeta := maxm;
+ if Utils.debug_metas then
+ ignore(List.map
+ (function current ->
+ Indexing.check_target c current "supl") res);
let neg, pos = infer_positive table tl in
res @ neg, pos
| (Positive, equality)::tl ->
let maxm, res =
Indexing.superposition_right !maxmeta env table equality in
maxmeta := maxm;
+ if Utils.debug_metas then
+ ignore
+ (List.map
+ (function current ->
+ Indexing.check_target c current "sup2") res);
let neg, pos = infer_positive table tl in
neg, res @ pos
in
let curr_table = Indexing.index Indexing.empty current in
let neg, pos = infer_positive curr_table active_list in
+ if Utils.debug_metas then
+ ignore(List.map
+ (function current ->
+ Indexing.check_target c current "sup3") pos);
neg, res @ pos
in
derived_clauses := !derived_clauses + (List.length new_neg) +
(List.length new_pos);
match !maximal_retained_equality with
- | None -> new_neg, new_pos
+ | None ->
+ if Utils.debug_metas then
+ (ignore(List.map
+ (function current ->
+ Indexing.check_target c current "sup4") new_pos);
+ ignore(List.map
+ (function current ->
+ Indexing.check_target c current "sup5") new_neg));
+ new_neg, new_pos
| Some eq ->
+ ignore(assert false);
(* if we have a maximal_retained_equality, we can discard all equalities
"greater" than it, as they will never be reached... An equality is
greater than maximal_retained_equality if it is bigger
in
List.filter filterfun new_pos
in
- new_neg, new_pos
+ new_neg, new_pos
;;
(** simplifies current using active and passive *)
let forward_simplify env (sign, current) ?passive (active_list, active_table) =
+ let _, context, _ = env in
let pl, passive_table =
match passive with
| None -> [], None
and pp = List.map (fun e -> (Positive, e)) pp in
pn @ pp, Some pt
in
- let all = if pl = [] then active_list else active_list @ pl in
+ let all = if pl = [] then active_list else active_list @ pl in
let demodulate table current =
let newmeta, newcurrent =
Some (sign, newcurrent)
in
let res =
+ if Utils.debug_metas then
+ ignore (Indexing.check_target context current "demod0");
let res = demodulate active_table current in
+ if Utils.debug_metas then
+ ignore ((function None -> () | Some (_,x) ->
+ Indexing.check_target context x "demod1";()) res);
match res with
| None -> None
| Some (sign, newcurrent) ->
(** simplifies new using active and passive *)
let forward_simplify_new env (new_neg, new_pos) ?passive active =
+ if Utils.debug_metas then
+ begin
+ let m,c,u = env in
+ ignore(List.map
+ (fun current ->
+ Indexing.check_target c current "forward new neg") new_neg);
+ ignore(List.map
+ (fun current -> Indexing.check_target c current "forward new pos")
+ new_pos;)
+ end;
let t1 = Unix.gettimeofday () in
let active_list, active_table = active in
let new_neg, new_pos =
let new_neg = List.map (demodulate Negative active_table) new_neg
and new_pos = List.map (demodulate Positive active_table) new_pos in
- new_neg,new_pos
-
-(* PROVA
+ new_neg,new_pos
+(* PROVA
match passive_table with
| None -> new_neg, new_pos
| Some passive_table ->
| None ->
active, (make_passive [] []), newa, None
| Some passive ->
+ active, passive, newa, None
+(* prova
let passive, newp =
backward_simplify_passive env new_pos new_table min_weight passive in
- active, passive, newa, newp
+ active, passive, newa, newp *)
;;
+let close env new' given =
+ let new_pos, new_table, min_weight =
+ List.fold_left
+ (fun (l, t, w) e ->
+ let ew, _, _, _, _ = e in
+ (Positive, e)::l, Indexing.index t e, min ew w)
+ ([], Indexing.empty, 1000000) (snd new')
+ in
+ List.fold_left
+ (fun (n,p) (s,c) ->
+ let neg,pos = infer env s c (new_pos,new_table) in
+ neg@n,pos@p)
+ ([],[]) given
+;;
+
+let is_commutative_law eq =
+ let w, proof, (eq_ty, left, right, order), metas, args = snd eq in
+ match left,right with
+ Cic.Appl[f1;Cic.Meta _ as a1;Cic.Meta _ as b1],
+ Cic.Appl[f2;Cic.Meta _ as a2;Cic.Meta _ as b2] ->
+ f1 = f2 && a1 = b2 && a2 = b1
+ | _ -> false
+;;
+
+let prova env new' active =
+ let given = List.filter is_commutative_law (fst active) in
+ let _ =
+ debug_print
+ (lazy
+ (Printf.sprintf "symmetric:\n%s\n"
+ (String.concat "\n"
+ ((List.map
+ (fun (s, e) -> (string_of_sign s) ^ " " ^
+ (string_of_equality ~env e))
+ (given)))))) in
+ close env new' given
+;;
+
(* returns an estimation of how many equalities in passive can be activated
within the current time limit *)
let get_selection_estimate () =
try
let subst, metasenv', _ =
let menv = metasenv @ metas @ gmetas in
- Inference.unification menv context eqterm gterm ugraph
+ Inference.unification metas gmetas context eqterm gterm ugraph
in
let newproof =
match proof with
(* given-clause algorithm with lazy reduction strategy *)
let rec given_clause dbd env goals theorems passive active =
+ let _,context,_ = env in
let goals = simplify_goals env goals active in
let ok, goals = activate_goal goals in
(* let theorems = simplify_theorems env theorems active in *)
else given_clause_aux dbd env goals theorems passive active
and given_clause_aux dbd env goals theorems passive active =
+ let _,context,_ = env in
let time1 = Unix.gettimeofday () in
-
+
let selection_estimate = get_selection_estimate () in
let kept = size_of_passive passive in
let passive =
given_clause dbd env goals theorems passive active
| false ->
let (sign, current), passive = select env (fst goals) passive active in
+ let names = List.map (HExtlib.map_option (fun (name,_) -> name)) context in
+ prerr_endline ("Selected = " ^
+ (CicPp.pp (Inference.term_of_equality current) names));
let time1 = Unix.gettimeofday () in
let res = forward_simplify env (sign, current) ~passive active in
let time2 = Unix.gettimeofday () in
(string_of_equality ~env current)));
let _, proof, _, _, _ = current in
ParamodulationSuccess (Some proof, env)
- ) else (
+ ) else (
debug_print
(lazy "\n================================================");
debug_print (lazy (Printf.sprintf "selected: %s %s"
(** given-clause algorithm with full reduction strategy *)
let rec given_clause_fullred dbd env goals theorems passive active =
- let goals = simplify_goals env goals ~passive active in
+ let goals = simplify_goals env goals ~passive active in
+ let _,context,_ = env in
let ok, goals = activate_goal goals in
(* let theorems = simplify_theorems env theorems ~passive active in *)
if ok then
+ let names = List.map (HExtlib.map_option (fun (name,_) -> name)) context in
+ let _, _, t = List.hd (snd (List.hd (fst goals))) in
+ let _ = prerr_endline ("goal activated = " ^ (CicPp.pp t names)) in
(* let _ = *)
(* debug_print *)
(* (lazy *)
| (_, [proof, _, _])::_ -> Some proof
| _ -> assert false
in
- ParamodulationSuccess (proof, env)
+ ( prerr_endline "esco qui";
+ let s = Printf.sprintf "actives:\n%s\n"
+ (String.concat "\n"
+ ((List.map
+ (fun (s, e) -> (string_of_sign s) ^ " " ^
+ (string_of_equality ~env e))
+ (fst active)))) in
+ let sp = Printf.sprintf "passives:\n%s\n"
+ (String.concat "\n"
+ (List.map
+ (string_of_equality ~env)
+ (let x,y,_ = passive in (fst x)@(fst y)))) in
+ prerr_endline s;
+ prerr_endline sp;
+ ParamodulationSuccess (proof, env))
else
given_clause_fullred_aux dbd env goals theorems passive active
else
else given_clause_fullred_aux dbd env goals theorems passive active
and given_clause_fullred_aux dbd env goals theorems passive active =
+ prerr_endline ("MAXMETA: " ^ string_of_int !maxmeta ^
+ " LOCALMAX: " ^ string_of_int !Indexing.local_max ^
+ " #ACTIVES: " ^ string_of_int (size_of_active active) ^
+ " #PASSIVES: " ^ string_of_int (size_of_passive passive));
+ if (size_of_active active) mod 54 = 0 then
+ (let s = Printf.sprintf "actives:\n%s\n"
+ (String.concat "\n"
+ ((List.map
+ (fun (s, e) -> (string_of_sign s) ^ " " ^
+ (string_of_equality ~env e))
+ (fst active)))) in
+ let sp = Printf.sprintf "passives:\n%s\n"
+ (String.concat "\n"
+ (List.map
+ (string_of_equality ~env)
+ (let x,y,_ = passive in (fst x)@(fst y)))) in
+ prerr_endline s;
+ prerr_endline sp);
let time1 = Unix.gettimeofday () in
-
+ let (_,context,_) = env in
let selection_estimate = get_selection_estimate () in
let kept = size_of_passive passive in
let passive =
given_clause_fullred dbd env goals theorems passive active
| false ->
let (sign, current), passive = select env (fst goals) passive active in
+ let names = List.map (HExtlib.map_option (fun (name,_) -> name)) context in
+ prerr_endline ("Selected = " ^ (string_of_sign sign) ^ " " ^
+ string_of_equality ~env current);
+ (* (CicPp.pp (Inference.term_of_equality current) names));*)
let time1 = Unix.gettimeofday () in
let res = forward_simplify env (sign, current) ~passive active in
let time2 = Unix.gettimeofday () in
let t1 = Unix.gettimeofday () in
let new' = infer env sign current active in
+ let _ =
+ match new' with
+ | neg, pos ->
+ debug_print
+ (lazy
+ (Printf.sprintf "new' (senza semplificare):\n%s\n"
+ (String.concat "\n"
+ ((List.map
+ (fun e -> "Negative " ^
+ (string_of_equality ~env e)) neg) @
+ (List.map
+ (fun e -> "Positive " ^
+ (string_of_equality ~env e)) pos)))))
+ in
let t2 = Unix.gettimeofday () in
infer_time := !infer_time +. (t2 -. t1);
-
let active =
if is_identity env current then active
else
let active, passive, newa, retained =
backward_simplify env new' ~passive active in
let t2 = Unix.gettimeofday () in
- backward_simpl_time := !backward_simpl_time +. (t2 -. t1);
+ backward_simpl_time := !backward_simpl_time +. (t2 -. t1);
match newa, retained with
| None, None -> active, passive, new'
| Some (n, p), None
| None, Some (n, p) ->
let nn, np = new' in
+ if Utils.debug_metas then
+ ignore (
+ List.map (fun x -> Indexing.check_target context x "simplify1")n;
+ List.map (fun x -> Indexing.check_target context x "simplify2")p);
simplify (nn @ n, np @ p) active passive
| Some (n, p), Some (rn, rp) ->
let nn, np = new' in
simplify (nn @ n @ rn, np @ p @ rp) active passive
in
let active, passive, new' = simplify new' active passive in
-
+(* pessima prova
+ let new1 = prova env new' active in
+ let new' = (fst new') @ (fst new1), (snd new') @ (snd new1) in
+ let _ =
+ match new1 with
+ | neg, pos ->
+ debug_print
+ (lazy
+ (Printf.sprintf "new1:\n%s\n"
+ (String.concat "\n"
+ ((List.map
+ (fun e -> "Negative " ^
+ (string_of_equality ~env e)) neg) @
+ (List.map
+ (fun e -> "Positive " ^
+ (string_of_equality ~env e)) pos)))))
+ in
+end prova *)
let k = size_of_passive passive in
if k < (kept - 1) then
processed_clauses := !processed_clauses + (kept - 1 - k);
in
(*try*)
let goal = Inference.BasicProof new_meta_goal, [], goal in
- let equalities = simplify_equalities env (equalities@library_equalities) in
+ let equalities = simplify_equalities env
+ (equalities@library_equalities) in
let active = make_active () in
let passive = make_passive [] equalities in
Printf.printf "\ncurrent goal: %s\n"
| ParamodulationSuccess (None, env) ->
Printf.printf "Success, but no proof?!?\n\n"
in
- Printf.printf ("infer_time: %.9f\nforward_simpl_time: %.9f\n" ^^
+ if Utils.time then
+ begin
+ prerr_endline
+ ((Printf.sprintf ("infer_time: %.9f\nforward_simpl_time: %.9f\n" ^^
"forward_simpl_new_time: %.9f\n" ^^
"backward_simpl_time: %.9f\n")
- !infer_time !forward_simpl_time !forward_simpl_new_time
- !backward_simpl_time;
- Printf.printf "passive_maintainance_time: %.9f\n"
- !passive_maintainance_time;
- Printf.printf " successful unification/matching time: %.9f\n"
- !Indexing.match_unif_time_ok;
- Printf.printf " failed unification/matching time: %.9f\n"
- !Indexing.match_unif_time_no;
- Printf.printf " indexing retrieval time: %.9f\n"
- !Indexing.indexing_retrieval_time;
- Printf.printf " demodulate_term.build_newtarget_time: %.9f\n"
- !Indexing.build_newtarget_time;
- Printf.printf "derived %d clauses, kept %d clauses.\n"
- !derived_clauses !kept_clauses;
+ !infer_time !forward_simpl_time !forward_simpl_new_time
+ !backward_simpl_time) ^
+ (Printf.sprintf "beta_expand_time: %.9f\n"
+ !Indexing.beta_expand_time) ^
+ (Printf.sprintf "passive_maintainance_time: %.9f\n"
+ !passive_maintainance_time) ^
+ (Printf.sprintf " successful unification/matching time: %.9f\n"
+ !Indexing.match_unif_time_ok) ^
+ (Printf.sprintf " failed unification/matching time: %.9f\n"
+ !Indexing.match_unif_time_no) ^
+ (Printf.sprintf " indexing retrieval time: %.9f\n"
+ !Indexing.indexing_retrieval_time) ^
+ (Printf.sprintf " demodulate_term.build_newtarget_time: %.9f\n"
+ !Indexing.build_newtarget_time) ^
+ (Printf.sprintf "derived %d clauses, kept %d clauses.\n"
+ !derived_clauses !kept_clauses))
+ end
(*
with exc ->
print_endline ("EXCEPTION: " ^ (Printexc.to_string exc));
let reset_refs () =
maxmeta := 0;
+ Indexing.local_max := 100;
symbols_counter := 0;
weight_age_counter := !weight_age_ratio;
processed_clauses := 0;
passive_maintainance_time := 0.;
derived_clauses := 0;
kept_clauses := 0;
+ Indexing.beta_expand_time := 0.;
+ Inference.metas_of_proof_time := 0.;
;;
let saturate
let library_equalities = List.map snd library_equalities in
let t2 = Unix.gettimeofday () in
maxmeta := maxm+2;
- let equalities = simplify_equalities env (equalities@library_equalities) in
+ let equalities = simplify_equalities env (equalities@library_equalities) in
debug_print
(lazy
(Printf.sprintf "Time to retrieve equalities: %.9f\n" (t2 -. t1)));
let tall = fs_time_info.build_all in
let tdemodulate = fs_time_info.demodulate in
let tsubsumption = fs_time_info.subsumption in
- debug_print (lazy (Printf.sprintf "\nTIME NEEDED: %.9f" time));
- debug_print (lazy (Printf.sprintf "\ntall: %.9f" tall));
- debug_print (lazy (Printf.sprintf "\ntdemod: %.9f" tdemodulate));
- debug_print (lazy (Printf.sprintf "\ntsubsumption: %.9f" tsubsumption));
- debug_print (lazy (Printf.sprintf "\ninfer_time: %.9f" !infer_time));
- debug_print (lazy (Printf.sprintf "\nforward_simpl_times: %.9f" !forward_simpl_time));
- debug_print (lazy (Printf.sprintf "\nforward_simpl_new_times: %.9f" !forward_simpl_new_time));
- debug_print (lazy (Printf.sprintf "\nbackward_simpl_times: %.9f" !backward_simpl_time));
- debug_print (lazy (Printf.sprintf "\npassive_maintainance_time: %.9f" !passive_maintainance_time));
+ if Utils.time then
+ begin
+ prerr_endline (
+ (Printf.sprintf "\nTIME NEEDED: %.9f" time) ^
+ (Printf.sprintf "\ntall: %.9f" tall) ^
+ (Printf.sprintf "\ntdemod: %.9f" tdemodulate) ^
+ (Printf.sprintf "\ntsubsumption: %.9f" tsubsumption) ^
+ (Printf.sprintf "\ninfer_time: %.9f" !infer_time) ^
+ (Printf.sprintf "\nbeta_expand_time: %.9f\n"
+ !Indexing.beta_expand_time) ^
+ (Printf.sprintf "\nmetas_of_proof: %.9f\n"
+ !Inference.metas_of_proof_time) ^
+ (Printf.sprintf "\nforward_simpl_times: %.9f" !forward_simpl_time) ^
+ (Printf.sprintf "\nforward_simpl_new_times: %.9f"
+ !forward_simpl_new_time) ^
+ (Printf.sprintf "\nbackward_simpl_times: %.9f" !backward_simpl_time) ^
+ (Printf.sprintf "\npassive_maintainance_time: %.9f"
+ !passive_maintainance_time))
+ end;
newstatus
| _ ->
raise (ProofEngineTypes.Fail (lazy "NO proof found"))
(* (string_of_equality e) *)
)
equalities))));
- debug_print (lazy "SIMPLYFYING EQUALITIES...");
+ debug_print (lazy "RETR: SIMPLYFYING EQUALITIES...");
let rec simpl e others others_simpl =
let (u, e) = e in
let active = List.map (fun (u, e) -> (Positive, e))
let goalterm = Cic.Meta (metano,irl) in
let initgoal = Inference.BasicProof goalterm, [], ty in
let env = (metasenv, context, CicUniv.empty_ugraph) in
- let equalities = simplify_equalities env (equalities@library_equalities) in
+ let equalities = simplify_equalities env (equalities@library_equalities) in
let table =
List.fold_left
(fun tbl eq -> Indexing.index tbl eq)
(* $Id$ *)
+
val saturate :
HMysql.dbd ->
?full:bool ->
(* $Id$ *)
-let debug = true;;
+let time = true;;
+let debug = false;;
+let debug_metas = false;;
+let debug_res = false;;
let debug_print s = if debug then prerr_endline (Lazy.force s);;
Printf.sprintf "[%d; %s]" cw s
-let weight_of_term ?(consider_metas=true) term =
+let weight_of_term ?(consider_metas=true) ?(count_metas_occurrences=false) term =
let module C = Cic in
let vars_dict = Hashtbl.create 5 in
let rec aux = function
Hashtbl.replace vars_dict metano (oldw+1)
with Not_found ->
Hashtbl.add vars_dict metano 1);
- 0
- | C.Meta _ -> 0 (* "variables" are lighter than constants and functions...*)
-
+ if count_metas_occurrences then 1 else 0
+ | C.Meta _ -> (* "variables" are lighter than constants and functions...*)
+ if count_metas_occurrences then 1 else 0
| C.Var (_, ens)
| C.Const (_, ens)
| C.MutInd (_, _, ens)
| C.MutConstruct (_, _, _, ens) ->
List.fold_left (fun w (u, t) -> (aux t) + w) 1 ens
-
+
| C.Cast (t1, t2)
| C.Lambda (_, t1, t2)
| C.Prod (_, t1, t2)
let compute_equality_weight ty left right =
let metasw = ref 0 in
let weight_of t =
- let w, m = (weight_of_term ~consider_metas:true t) in
- metasw := !metasw + (2 * (List.length m));
+ let w, m = (weight_of_term
+ ~consider_metas:true ~count_metas_occurrences:false t) in
+ metasw := !metasw + (2 * (List.length m)) ;
w
in
(* Warning: the following let cannot be expanded since it forces the
*)
(* (weight of constants, [(meta, weight_of_meta)]) *)
+
+val time : bool
+val debug : bool
+val debug_metas: bool
+val debug_res: bool
+
type weight = int * (int * int) list;;
type comparison = Lt | Le | Eq | Ge | Gt | Incomparable;;
val string_of_weight: weight -> string
-val weight_of_term: ?consider_metas:bool -> Cic.term -> weight
+val weight_of_term:
+ ?consider_metas:bool ->
+ ?count_metas_occurrences:bool-> Cic.term -> weight
val normalize_weight: int -> weight -> weight
projects / helm.git / commitdiff