From: Andrea Asperti Date: Mon, 20 Mar 2006 16:30:08 +0000 (+0000) Subject: Snapshot. X-Git-Tag: 0.4.95@7852~1590 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=1d7de941e98a1d80ef3103636148537ada3e2b9e;p=helm.git Snapshot. --- diff --git a/components/tactics/paramodulation/indexing.ml b/components/tactics/paramodulation/indexing.ml index 5830b0842..83dc1b180 100644 --- a/components/tactics/paramodulation/indexing.ml +++ b/components/tactics/paramodulation/indexing.ml @@ -30,13 +30,15 @@ module Index = Equality_indexing.DT (* discrimination tree based indexing *) 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; @@ -54,22 +56,37 @@ let check_equation env equation msg = 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)); ;; @@ -84,6 +101,74 @@ let in_index = Index.in_index 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. @@ -97,7 +182,15 @@ let init_index = Index.init_index 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 = @@ -107,12 +200,12 @@ let get_candidates mode tree term = 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 ;; @@ -154,6 +247,17 @@ let rec find_matches metasenv context ugraph lift_amount term termty = | [] -> 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 @@ -163,8 +267,8 @@ let rec find_matches metasenv context ugraph lift_amount term termty = 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); @@ -174,9 +278,7 @@ let rec find_matches metasenv context ugraph lift_amount term termty = 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)) @@ -186,15 +288,20 @@ let rec find_matches metasenv context ugraph lift_amount term termty = 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 @@ -233,7 +340,7 @@ let rec find_all_matches ?(unif_fun=Inference.unification) 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); @@ -324,7 +431,7 @@ let subsumption env table target = 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); @@ -364,95 +471,102 @@ let subsumption env table target = 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 ;; @@ -461,8 +575,10 @@ let build_newtarget_time = ref 0.;; 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 @@ -476,33 +592,40 @@ let rec demodulation_equality newmeta env table sign target = 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; @@ -533,10 +656,11 @@ let rec demodulation_equality newmeta env table sign target = 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 @@ -548,40 +672,37 @@ let rec demodulation_equality newmeta env table sign target = (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 -> @@ -589,10 +710,11 @@ let rec demodulation_equality newmeta env table sign target = 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 @@ -600,7 +722,7 @@ let rec demodulation_equality newmeta env table sign target = (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 @@ -620,6 +742,7 @@ let rec betaexpand_term metasenv context ugraph table lift_amount term = 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) -> @@ -749,15 +872,21 @@ let superposition_left newmeta (metasenv, context, ugraph) table target = 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 @@ -816,15 +945,13 @@ let superposition_left newmeta (metasenv, context, ugraph) table target = 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 ;; @@ -845,11 +972,20 @@ let superposition_right newmeta (metasenv, context, ugraph) table target = 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) @@ -864,8 +1000,9 @@ let superposition_right newmeta (metasenv, context, ugraph) table target = 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 @@ -888,27 +1025,28 @@ let superposition_right newmeta (metasenv, context, ugraph) table target = 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))) @@ -926,7 +1064,7 @@ let rec demodulation_goal newmeta env table goal = 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 @@ -936,7 +1074,6 @@ let rec demodulation_goal newmeta env table goal = 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 @@ -983,13 +1120,11 @@ let rec demodulation_goal newmeta env table goal = 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 -> @@ -1013,13 +1148,12 @@ let rec demodulation_theorem newmeta env table theorem = 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 @@ -1032,11 +1166,10 @@ let rec demodulation_theorem newmeta env table theorem = 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 -> diff --git a/components/tactics/paramodulation/indexing.mli b/components/tactics/paramodulation/indexing.mli index 8a6f9c2b6..bb005f8d3 100644 --- a/components/tactics/paramodulation/indexing.mli +++ b/components/tactics/paramodulation/indexing.mli @@ -25,6 +25,8 @@ (* $Id$ *) +val beta_expand_time : float ref + module Index : sig module PosEqSet : Set.S @@ -50,23 +52,20 @@ val subsumption : 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 -> @@ -83,4 +82,9 @@ val demodulation_theorem : 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 diff --git a/components/tactics/paramodulation/inference.ml b/components/tactics/paramodulation/inference.ml index dfb67583e..fdaf68018 100644 --- a/components/tactics/paramodulation/inference.ml +++ b/components/tactics/paramodulation/inference.ml @@ -27,6 +27,8 @@ open Utils;; +let metas_of_proof_time = ref 0.;; +let metas_of_term_time = ref 0.;; type equality = int * (* weight *) @@ -49,7 +51,6 @@ and proof = | SubProof of Cic.term * int * proof ;; - let string_of_equality ?env = match env with | None -> ( @@ -76,13 +77,33 @@ let rec string_of_proof = function 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 @@ -186,6 +207,16 @@ let rec metas_of_term = function | _ -> [] ;; +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;; @@ -374,10 +405,8 @@ let unification_simple metasenv context t1 t2 ugraph = | 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 -> @@ -404,18 +433,13 @@ let unification_simple metasenv context t1 t2 ugraph = 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 @@ -426,6 +450,16 @@ let unification metasenv context t1 t2 ugraph = ) 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 @@ -436,12 +470,20 @@ let unification metasenv context t1 t2 ugraph = 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;; @@ -493,35 +535,136 @@ let matching_simple metasenv context t1 t2 ugraph = ;; *) - +(* 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 @@ -563,8 +706,9 @@ let find_equalities context proof = ) | 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 @@ -585,6 +729,7 @@ let find_equalities context proof = 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 ;; @@ -834,7 +979,10 @@ let fix_metas_old newmeta (w, p, (ty, left, right, o), menv, args) = 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 @@ -912,6 +1060,11 @@ let relocate newmeta menv = 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 @@ -925,14 +1078,26 @@ let fix_metas newmeta (w, p, (ty, left, right, o), menv, args) = | 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 @@ -980,26 +1145,23 @@ let is_identity (metasenv, context, ugraph) = function 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)) ;; diff --git a/components/tactics/paramodulation/inference.mli b/components/tactics/paramodulation/inference.mli index b31d8bacf..5fdf694fc 100644 --- a/components/tactics/paramodulation/inference.mli +++ b/components/tactics/paramodulation/inference.mli @@ -23,6 +23,8 @@ * http://cs.unibo.it/helm/. *) +val metas_of_proof_time : float ref + type equality = int * (* weight *) proof * (* proof *) @@ -52,11 +54,13 @@ val build_proof_term: ?noproof:Cic.term -> proof -> Cic.term 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 @@ -65,7 +69,7 @@ val matching: 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 @@ -129,6 +133,7 @@ val is_identity: environment -> equality -> bool 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 diff --git a/components/tactics/paramodulation/saturation.ml b/components/tactics/paramodulation/saturation.ml index 6a700d868..9bc9d2464 100644 --- a/components/tactics/paramodulation/saturation.ml +++ b/components/tactics/paramodulation/saturation.ml @@ -28,6 +28,7 @@ open Inference;; open Utils;; + (* for debugging let check_equation env equation msg = @@ -69,9 +70,9 @@ let maximal_retained_equality = ref None;; (* 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 *) @@ -134,16 +135,60 @@ module OrderedEquality = struct 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 @@ -163,15 +208,15 @@ let select env goals passive (active, _) = (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 @@ -215,9 +260,10 @@ let select env goals passive (active, _) = ) | _ -> 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), @@ -225,7 +271,7 @@ let select env goals passive (active, _) = 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), @@ -273,22 +319,6 @@ let add_to_passive passive (new_neg, new_pos) = ;; -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 = @@ -391,41 +421,75 @@ 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 @@ -469,7 +533,7 @@ let infer env sign current (active_list, active_table) = in List.filter filterfun new_pos in - new_neg, new_pos + new_neg, new_pos ;; @@ -490,6 +554,7 @@ let contains_empty env (negative, positive) = (** 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 @@ -498,7 +563,7 @@ let forward_simplify env (sign, current) ?passive (active_list, active_table) = 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 = @@ -523,7 +588,12 @@ let forward_simplify env (sign, current) ?passive (active_list, active_table) = 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) -> @@ -570,6 +640,16 @@ let fs_time_info = { build_all = 0.; demodulate = 0.; subsumption = 0. };; (** 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 @@ -596,9 +676,8 @@ let forward_simplify_new env (new_neg, new_pos) ?passive active = 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 -> @@ -735,12 +814,52 @@ let backward_simplify env new' ?passive active = | 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 () = @@ -929,7 +1048,7 @@ let apply_equality_to_goal env equality goal = 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 @@ -1427,6 +1546,7 @@ let apply_theorem_to_goals env theorems active goals = (* 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 *) @@ -1460,8 +1580,9 @@ let rec given_clause dbd env goals theorems passive active = 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 = @@ -1490,6 +1611,9 @@ and given_clause_aux dbd env goals theorems passive active = 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 @@ -1504,7 +1628,7 @@ and given_clause_aux dbd env goals theorems passive active = (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" @@ -1582,10 +1706,14 @@ and given_clause_aux dbd env goals theorems passive active = (** 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 *) @@ -1607,7 +1735,21 @@ let rec given_clause_fullred dbd env goals theorems passive active = | (_, [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 @@ -1628,8 +1770,26 @@ let rec given_clause_fullred dbd env goals theorems passive active = 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 = @@ -1658,6 +1818,10 @@ and given_clause_fullred_aux dbd env goals theorems passive active = 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 @@ -1681,9 +1845,22 @@ and given_clause_fullred_aux dbd env goals theorems passive active = 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 @@ -1703,19 +1880,40 @@ and given_clause_fullred_aux dbd env goals theorems passive active = 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); @@ -1892,7 +2090,8 @@ let main dbd full term metasenv ugraph = 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" @@ -1952,23 +2151,29 @@ let main dbd full term metasenv ugraph = | 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)); @@ -1982,6 +2187,7 @@ and default_width = !maxwidth;; let reset_refs () = maxmeta := 0; + Indexing.local_max := 100; symbols_counter := 0; weight_age_counter := !weight_age_ratio; processed_clauses := 0; @@ -1995,6 +2201,8 @@ let reset_refs () = passive_maintainance_time := 0.; derived_clauses := 0; kept_clauses := 0; + Indexing.beta_expand_time := 0.; + Inference.metas_of_proof_time := 0.; ;; let saturate @@ -2030,7 +2238,7 @@ 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))); @@ -2131,15 +2339,25 @@ let saturate 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")) @@ -2190,7 +2408,7 @@ let retrieve_and_print dbd term metasenv ugraph = (* (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)) @@ -2331,7 +2549,7 @@ let demodulate_tac ~dbd ~pattern ((proof,goal) as initialstatus) = 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) diff --git a/components/tactics/paramodulation/saturation.mli b/components/tactics/paramodulation/saturation.mli index 34159810d..17fbb8cfd 100644 --- a/components/tactics/paramodulation/saturation.mli +++ b/components/tactics/paramodulation/saturation.mli @@ -25,6 +25,7 @@ (* $Id$ *) + val saturate : HMysql.dbd -> ?full:bool -> diff --git a/components/tactics/paramodulation/utils.ml b/components/tactics/paramodulation/utils.ml index b212d0fab..84de8800e 100644 --- a/components/tactics/paramodulation/utils.ml +++ b/components/tactics/paramodulation/utils.ml @@ -25,7 +25,10 @@ (* $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);; @@ -227,7 +230,7 @@ let string_of_weight (cw, mw) = 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 @@ -237,15 +240,15 @@ let weight_of_term ?(consider_metas=true) term = 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) @@ -292,8 +295,9 @@ module IntSet = Set.Make(OrderedInt) 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 diff --git a/components/tactics/paramodulation/utils.mli b/components/tactics/paramodulation/utils.mli index ce14d480f..9dc6501d7 100644 --- a/components/tactics/paramodulation/utils.mli +++ b/components/tactics/paramodulation/utils.mli @@ -24,6 +24,12 @@ *) (* (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;; @@ -34,7 +40,9 @@ val print_subst: ?prefix:string -> Cic.substitution -> string 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