From: Alberto Griggio Date: Fri, 10 Jun 2005 14:16:29 +0000 (+0000) Subject: integrated indexing.ml, breaks everything :-P (previous working version tagged PRE_IN... X-Git-Tag: PRE_STORAGE~78 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=50b01988edd12788a59aea3fb0f6704d5fd2bb69;p=helm.git integrated indexing.ml, breaks everything :-P (previous working version tagged PRE_INDEXING_1) --- diff --git a/helm/ocaml/paramodulation/Makefile b/helm/ocaml/paramodulation/Makefile index c50c1b41f..d1d4c0427 100644 --- a/helm/ocaml/paramodulation/Makefile +++ b/helm/ocaml/paramodulation/Makefile @@ -43,9 +43,12 @@ INTERFACE_FILES = \ DEPOBJS = \ $(INTERFACE_FILES) $(INTERFACE_FILES:%.mli=%.ml) \ + indexing.ml \ saturation.ml -TOPLEVELOBJS = $(INTERFACE_FILES:%.mli=%.cmo) saturation.cmo +TOPLEVELOBJS = $(INTERFACE_FILES:%.mli=%.cmo) \ + indexing.cmo \ + saturation.cmo # TESTOBJS = \ # disambiguatingParser.cmo \ # batchParser.cmo diff --git a/helm/ocaml/paramodulation/indexing.ml b/helm/ocaml/paramodulation/indexing.ml index 85821097d..5c08d906d 100644 --- a/helm/ocaml/paramodulation/indexing.ml +++ b/helm/ocaml/paramodulation/indexing.ml @@ -10,34 +10,35 @@ let head_of_term = function ;; -let index table (sign, eq) = +let index table eq = let _, (_, l, r, ordering), _, _ = eq in let hl = head_of_term l in let hr = head_of_term r in let index x pos = let x_entry = try Hashtbl.find table x with Not_found -> [] in - Hashtbl.replace table x ((pos, sign, eq)::x_entry) + Hashtbl.replace table x ((pos, eq)::x_entry) in -(* (match ordering with *) -(* | Utils.Gt -> *) -(* index hl Left *) -(* | Utils.Lt -> *) -(* index hr Right *) -(* | _ -> index hl Left; *) -(* index hr Right); *) - index hl Left; - index hr Right; + let _ = + match ordering with + | Utils.Gt -> + index hl Left + | Utils.Lt -> + index hr Right + | _ -> index hl Left; index hr Right + in +(* index hl Left; *) +(* index hr Right; *) table ;; -let remove_index table (sign, eq) = +let remove_index table eq = let _, (_, l, r, ordering), _, _ = eq in let hl = head_of_term l and hr = head_of_term r in let remove_index x pos = let x_entry = try Hashtbl.find table x with Not_found -> [] in - let newentry = List.filter (fun e -> e <> (pos, sign, eq)) x_entry in + let newentry = List.filter (fun e -> e <> (pos, eq)) x_entry in Hashtbl.replace table x newentry in remove_index hl Left; @@ -46,26 +47,38 @@ let remove_index table (sign, eq) = ;; -let rec find_matches metasenv context ugraph lift_amount term = +let rec find_matches unif_fun metasenv context ugraph lift_amount term = let module C = Cic in let module U = Utils in let module S = CicSubstitution in let module M = CicMetaSubst in let module HL = HelmLibraryObjects in let cmp = !Utils.compare_terms in + let names = Utils.names_of_context context in + Printf.printf "CHIAMO find_matches (%s) su: %s\n" + (if unif_fun == Inference.matching then "MATCHING" + else if unif_fun == CicUnification.fo_unif then "UNIFICATION" + else "??????????") + (CicPp.pp term names); function | [] -> None - | (_, U.Negative, _)::tl -> - find_matches metasenv context ugraph lift_amount term tl - | (pos, U.Positive, (_, (_, _, _, o), _, _))::tl - when (pos = Left && o = U.Lt) || (pos = Right && o = U.Gt) -> - find_matches metasenv context ugraph lift_amount term tl - | (pos, U.Positive, (proof, (ty, left, right, o), metas, args))::tl -> + | (pos, (proof, (ty, left, right, o), metas, args))::tl -> let do_match c other eq_URI = + Printf.printf "provo con %s: %s, %s\n\n" + (if unif_fun == Inference.matching then "MATCHING" + else if unif_fun == CicUnification.fo_unif then "UNIFICATION" + else "??????????") + (CicPp.pp term names) + (CicPp.pp (S.lift lift_amount c) names); let subst', metasenv', ugraph' = - Inference.matching (metasenv @ metas) context term - (S.lift lift_amount c) ugraph +(* Inference.matching (metasenv @ metas) context term *) +(* (S.lift lift_amount c) ugraph *) + unif_fun (metasenv @ metas) context + term (S.lift lift_amount c) ugraph in +(* let names = U.names_of_context context in *) + Printf.printf "MATCH FOUND: %s, %s\n" + (CicPp.pp term names) (CicPp.pp (S.lift lift_amount c) names); Some (C.Rel (1 + lift_amount), subst', metasenv', ugraph', (proof, ty, c, other, eq_URI)) in @@ -74,19 +87,38 @@ let rec find_matches metasenv context ugraph lift_amount term = else right, left, HL.Logic.eq_ind_r_URI in if o <> U.Incomparable then - try do_match c other eq_URI - with e -> find_matches metasenv context ugraph lift_amount term tl + try + print_endline "SONO QUI!"; + let res = do_match c other eq_URI in + print_endline "RITORNO RES"; + res + with e -> + Printf.printf "ERRORE!: %s\n" (Printexc.to_string e); + find_matches unif_fun metasenv context ugraph lift_amount term tl else - let res = try do_match c other eq_URI with e -> None in + let res = + try + let res = do_match c other eq_URI in + print_endline "RITORNO RES 2"; + res + with e -> None in match res with - | Some (_, s, _, _, _) -> - if cmp (M.apply_subst s left) (M.apply_subst s right) = - (if pos = Left then U.Gt else U.Lt) then - res + | Some (_, s, _, _, _) -> + let c' = M.apply_subst s c + and other' = M.apply_subst s other in + let order = cmp c' other' in + let names = U.names_of_context context in + Printf.printf "c': %s\nother': %s\norder: %s\n\n" + (CicPp.pp c' names) (CicPp.pp other' names) + (U.string_of_comparison order); +(* if cmp (M.apply_subst s c) (M.apply_subst s other) = U.Gt then *) + if order = U.Gt then + res else - find_matches metasenv context ugraph lift_amount term tl + find_matches unif_fun metasenv context ugraph + lift_amount term tl | None -> - find_matches metasenv context ugraph lift_amount term tl + find_matches unif_fun metasenv context ugraph lift_amount term tl ;; @@ -101,7 +133,8 @@ let rec demodulate_term metasenv context ugraph table lift_amount term = | C.Meta _ -> None | term -> let res = - find_matches metasenv context ugraph lift_amount term candidates + find_matches Inference.matching metasenv context ugraph + lift_amount term candidates in if res <> None then res @@ -148,8 +181,8 @@ let rec demodulate_term metasenv context ugraph table lift_amount term = Some (C.Prod (nn, s', (S.lift 1 t)), subst, menv, ug, info) ) | t -> - Printf.printf "Ne` Appl ne` Prod: %s\n" - (CicPp.pp t (Utils.names_of_context context)); +(* Printf.printf "Ne` Appl ne` Prod: %s\n" *) +(* (CicPp.pp t (Utils.names_of_context context)); *) None ;; @@ -159,9 +192,10 @@ let rec demodulate newmeta env table target = let module S = CicSubstitution in let module M = CicMetaSubst in let module HL = HelmLibraryObjects in + print_endline "\n\ndemodulate"; let metasenv, context, ugraph = env in let proof, (eq_ty, left, right, order), metas, args = target in - let metasenv = metasenv @ metas in + let metasenv' = metasenv @ metas in let build_newtarget is_left (t, subst, menv, ug, (proof', ty, what, other, eq_URI)) = let newterm, newproof = @@ -169,7 +203,7 @@ let rec demodulate newmeta env table target = let bo'' = C.Appl ([C.MutInd (HL.Logic.eq_URI, 0, []); S.lift 1 eq_ty] @ - if is_left then [bo; S.lift 1 right] else [S.lift 1 left; bo]) + if is_left then [bo; S.lift 1 right] else [S.lift 1 left; bo]) in let t' = C.Lambda (C.Anonymous, ty, bo'') in bo, @@ -192,20 +226,20 @@ let rec demodulate newmeta env table target = in newmeta, newtarget in - let res = demodulate_term metasenv context ugraph table 0 left in + let res = demodulate_term metasenv' context ugraph table 0 left in match res with | Some t -> let newmeta, newtarget = build_newtarget true t in - if Inference.is_identity (metasenv, context, ugraph) newtarget then + if Inference.is_identity (metasenv', context, ugraph) newtarget then newmeta, newtarget else demodulate newmeta env table newtarget | None -> - let res = demodulate_term metasenv context ugraph table 0 right in + let res = demodulate_term metasenv' context ugraph table 0 right in match res with | Some t -> let newmeta, newtarget = build_newtarget false t in - if Inference.is_identity (metasenv, context, ugraph) newtarget then + if Inference.is_identity (metasenv', context, ugraph) newtarget then newmeta, newtarget else demodulate newmeta env table newtarget @@ -277,11 +311,17 @@ let rec betaexpand_term metasenv context ugraph table lift_amount term = match term with | C.Meta _ -> res, lifted_term | _ -> +(* let names = Utils.names_of_context context in *) +(* Printf.printf "CHIAMO find_matches su: %s\n" (CicPp.pp term names); *) match - find_matches metasenv context ugraph lift_amount term candidates + find_matches CicUnification.fo_unif metasenv context ugraph + lift_amount term candidates with | None -> res, lifted_term - | Some r -> r::res, lifted_term + | Some r -> +(* let _, _, _, _, (_, _, what, _, _) = r in *) +(* Printf.printf "OK, aggiungo a res: %s\n" (CicPp.pp what names); *) + r::res, lifted_term ;; @@ -292,10 +332,20 @@ let superposition_left (metasenv, context, ugraph) table target = let module HL = HelmLibraryObjects in let module CR = CicReduction in let module U = Utils in + print_endline "\n\nsuperposition_left"; let proof, (eq_ty, left, right, ordering), _, _ = target in let expansions, _ = let term = if ordering = U.Gt then left else right in - betaexpand_term metasenv context ugraph table 0 term + let res = + betaexpand_term metasenv context ugraph table 0 term in +(* let names = U.names_of_context context in *) +(* Printf.printf "\n\nsuperposition_left: %s\n%s\n" *) +(* (CicPp.pp term names) *) +(* (String.concat "\n" *) +(* (List.map *) +(* (fun (_, _, _, _, (_, _, what, _, _)) -> CicPp.pp what names) *) +(* (fst res))); *) + res in let build_new (bo, s, m, ug, (proof', ty, what, other, eq_URI)) = let newgoal, newproof = @@ -332,12 +382,14 @@ let superposition_right newmeta (metasenv, context, ugraph) table target = let module HL = HelmLibraryObjects in let module CR = CicReduction in let module U = Utils in + print_endline "\n\nsuperposition_right"; let eqproof, (eq_ty, left, right, ordering), newmetas, args = target in + let metasenv' = metasenv @ newmetas in let maxmeta = ref newmeta in let res1, res2 = 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) + | U.Gt -> fst (betaexpand_term metasenv' context ugraph table 0 left), [] + | U.Lt -> [], fst (betaexpand_term metasenv' context ugraph table 0 right) | _ -> let res l r = List.filter @@ -345,7 +397,7 @@ let superposition_right newmeta (metasenv, context, ugraph) table target = let subst = M.apply_subst subst in let o = !Utils.compare_terms (subst l) (subst r) in o <> U.Lt && o <> U.Le) - (fst (betaexpand_term metasenv context ugraph table 0 l)) + (fst (betaexpand_term metasenv' context ugraph table 0 l)) in (res left right), (res right left) in diff --git a/helm/ocaml/paramodulation/saturation.ml b/helm/ocaml/paramodulation/saturation.ml index 5f9ffe335..e30b1545f 100644 --- a/helm/ocaml/paramodulation/saturation.ml +++ b/helm/ocaml/paramodulation/saturation.ml @@ -61,10 +61,10 @@ let symbols_ratio = ref 0;; let symbols_counter = ref 0;; -let select env passive active = - let (neg_list, neg_set), (pos_list, pos_set) = passive in +let select env passive (active, _) = + let (neg_list, neg_set), (pos_list, pos_set), passive_table = passive in let remove eq l = - List.filter (fun e -> not (e = eq)) l + List.filter (fun e -> e <> eq) l in if !weight_age_ratio > 0 then weight_age_counter := !weight_age_counter - 1; @@ -73,9 +73,13 @@ let select env passive active = weight_age_counter := !weight_age_ratio; match neg_list, pos_list with | hd::tl, pos -> - (Negative, hd), ((tl, EqualitySet.remove hd neg_set), (pos, pos_set)) + (* Negatives aren't indexed, no need to remove them... *) + (Negative, hd), + ((tl, EqualitySet.remove hd neg_set), (pos, pos_set), passive_table) | [], hd::tl -> - (Positive, hd), (([], neg_set), (tl, EqualitySet.remove hd pos_set)) + let passive_table = 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) -> ( @@ -125,14 +129,17 @@ let select env passive active = let _, current = EqualitySet.fold f pos_set initial in (* Printf.printf "\nsymbols-based selection: %s\n\n" *) (* (string_of_equality ~env current); *) + let passive_table = Indexing.remove_index passive_table current in (Positive, current), (([], neg_set), - (remove current pos_list, EqualitySet.remove current pos_set)) + (remove current pos_list, EqualitySet.remove current pos_set), + passive_table) | _ -> let current = EqualitySet.min_elt pos_set in let passive = (neg_list, neg_set), - (remove current pos_list, EqualitySet.remove current pos_set) + (remove current pos_list, EqualitySet.remove current pos_set), + Indexing.remove_index passive_table current in (Positive, current), passive ) @@ -143,14 +150,16 @@ let select env passive active = let current = set_selection pos_set in let passive = (neg_list, neg_set), - (remove current pos_list, EqualitySet.remove current pos_set) + (remove current pos_list, EqualitySet.remove current pos_set), + Indexing.remove_index passive_table current in (Positive, current), passive else let current = set_selection neg_set in let passive = (remove current neg_list, EqualitySet.remove current neg_set), - (pos_list, pos_set) + (pos_list, pos_set), + passive_table in (Negative, current), passive ;; @@ -160,24 +169,34 @@ let make_passive neg pos = let set_of equalities = List.fold_left (fun s e -> EqualitySet.add e s) EqualitySet.empty equalities in - (neg, set_of neg), (pos, set_of pos) + let table = Hashtbl.create (List.length pos) in + (neg, set_of neg), + (pos, set_of pos), + List.fold_left (fun tbl e -> Indexing.index tbl e) table pos +;; + + +let make_active () = + [], Hashtbl.create 1 ;; let add_to_passive passive (new_neg, new_pos) = - let (neg_list, neg_set), (pos_list, pos_set) = passive in + let (neg_list, neg_set), (pos_list, pos_set), table = passive in let ok set equality = not (EqualitySet.mem equality set) in let neg = List.filter (ok neg_set) new_neg and pos = List.filter (ok pos_set) new_pos in let add set equalities = List.fold_left (fun s e -> EqualitySet.add e s) set equalities in - (neg @ neg_list, add neg_set neg), (pos_list @ pos, add pos_set pos) + (neg @ neg_list, add neg_set neg), + (pos_list @ pos, add pos_set pos), + List.fold_left (fun tbl e -> Indexing.index tbl e) table pos ;; let passive_is_empty = function - | ([], _), ([], _) -> true + | ([], _), ([], _), _ -> true | _ -> false ;; @@ -185,39 +204,30 @@ let passive_is_empty = function (* TODO: find a better way! *) let maxmeta = ref 0;; -let infer env sign current active = - let rec infer_negative current = function - | [] -> [], [] - | (Negative, _)::tl -> infer_negative current tl - | (Positive, equality)::tl -> - let res = superposition_left env current equality in - let neg, pos = infer_negative current tl in - res @ neg, pos - - and infer_positive current = function - | [] -> [], [] - | (Negative, equality)::tl -> - let res = superposition_left env equality current in - let neg, pos = infer_positive current tl in - res @ neg, pos - | (Positive, equality)::tl -> - let maxm, res = superposition_right !maxmeta env current equality in - let maxm, res' = superposition_right maxm env equality current in - maxmeta := maxm; - let neg, pos = infer_positive current tl in - -(* Printf.printf "risultato di superposition_right: %s %s\n%s\n\n" *) -(* (string_of_equality ~env current) (string_of_equality ~env equality) *) -(* (String.concat "\n" (List.map (string_of_equality ~env) res)); *) -(* Printf.printf "risultato di superposition_right: %s %s\n%s\n\n" *) -(* (string_of_equality ~env equality) (string_of_equality ~env current) *) -(* (String.concat "\n" (List.map (string_of_equality ~env) res')); *) - - neg, res @ res' @ pos - in +let infer env sign current (active_list, active_table) = match sign with - | Negative -> infer_negative current active - | Positive -> infer_positive current active + | Negative -> + Indexing.superposition_left env active_table current, [] + | Positive -> + let maxm, res = + Indexing.superposition_right !maxmeta env active_table current in + maxmeta := maxm; + let rec infer_positive table = function + | [] -> [], [] + | (Negative, equality)::tl -> + let res = Indexing.superposition_left env table equality in + 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; + let neg, pos = infer_positive table tl in + neg, res @ pos + in + let curr_table = Indexing.index (Hashtbl.create 1) current in + let neg, pos = infer_positive curr_table active_list in + neg, res @ pos ;; @@ -236,15 +246,16 @@ let contains_empty env (negative, positive) = ;; -let forward_simplify env (sign, current) ?passive active = - let pn, pp = +let forward_simplify env (sign, current) ?passive (active_list, active_table) = + let pl, passive_table = match passive with - | None -> [], [] - | Some ((pn, _), (pp, _)) -> - (List.map (fun e -> Negative, e) pn), - (List.map (fun e -> Positive, e) pp) + | None -> [], None + | Some ((pn, _), (pp, _), pt) -> + let pn = List.map (fun e -> (Negative, e)) pn + and pp = List.map (fun e -> (Positive, e)) pp in + pn @ pp, Some pt in - let all = active @ pn @ pp in + let all = active_list @ pl in let rec find_duplicate sign current = function | [] -> false | (s, eq)::tl when s = sign -> @@ -252,28 +263,23 @@ let forward_simplify env (sign, current) ?passive active = else find_duplicate sign current tl | _::tl -> find_duplicate sign current tl in -(* let duplicate = find_duplicate sign current all in *) -(* if duplicate then *) -(* None *) -(* else *) - let rec aux env (sign, current) = function - | [] -> Some (sign, current) - | (Negative, _)::tl -> aux env (sign, current) tl - | (Positive, equality)::tl -> - let newmeta, newcurrent = - demodulation !maxmeta env current equality in - maxmeta := newmeta; - if is_identity env newcurrent then - if sign = Negative then - Some (sign, current) - else - None - else if newcurrent <> current then - aux env (sign, newcurrent) active - else - aux env (sign, newcurrent) tl + let demodulate table current = + let newmeta, newcurrent = Indexing.demodulate !maxmeta env table current in + maxmeta := newmeta; + if is_identity env newcurrent then + if sign = Negative then Some (sign, newcurrent) else None + else + Some (sign, newcurrent) + in + let res = + let res = demodulate active_table current in + match res with + | None -> None + | Some (sign, newcurrent) -> + match passive_table with + | None -> res + | Some passive_table -> demodulate passive_table newcurrent in - let res = aux env (sign, current) all in match res with | None -> None | Some (s, c) -> @@ -290,84 +296,73 @@ let forward_simplify env (sign, current) ?passive active = let forward_simplify_new env (new_neg, new_pos) ?passive active = - let pn, pp = + let active_list, active_table = active in + let pl, passive_table = match passive with - | None -> [], [] - | Some ((pn, _), (pp, _)) -> - (List.map (fun e -> Negative, e) pn), - (List.map (fun e -> Positive, e) pp) + | None -> [], None + | Some ((pn, _), (pp, _), pt) -> + let pn = List.map (fun e -> (Negative, e)) pn + and pp = List.map (fun e -> (Positive, e)) pp in + pn @ pp, Some pt in - let all = active @ pn @ pp in - let remove_identities equalities = - let ok eq = not (is_identity env eq) in - List.filter ok equalities + let all = active_list @ pl in + let demodulate table target = + let newmeta, newtarget = Indexing.demodulate !maxmeta env table target in + maxmeta := newmeta; + newtarget in - let rec simpl all' target = - match all' with - | [] -> target - | (Negative, _)::tl -> simpl tl target - | (Positive, source)::tl -> - let newmeta, newtarget = demodulation !maxmeta env target source in - maxmeta := newmeta; - if is_identity env newtarget then newtarget - else if newtarget <> target then ( -(* Printf.printf "OK:\n%s\n%s\n" *) -(* (string_of_equality ~env target) *) -(* (string_of_equality ~env newtarget); *) -(* print_newline (); *) - simpl all newtarget - ) - else simpl tl newtarget + let new_neg, new_pos = + let new_neg = List.map (demodulate active_table) new_neg + and new_pos = List.map (demodulate active_table) new_pos in + match passive_table with + | None -> new_neg, new_pos + | Some passive_table -> + List.map (demodulate passive_table) new_neg, + List.map (demodulate passive_table) new_pos in - let new_neg = List.map (simpl all) new_neg - and new_pos = remove_identities (List.map (simpl all) new_pos) in let new_pos_set = List.fold_left (fun s e -> EqualitySet.add e s) EqualitySet.empty new_pos in let new_pos = EqualitySet.elements new_pos_set in let f sign' target (sign, eq) = -(* Printf.printf "f %s <%s> (%s, <%s>)\n" *) -(* (string_of_sign sign') (string_of_equality ~env target) *) -(* (string_of_sign sign) (string_of_equality ~env eq); *) if sign <> sign' then false else subsumption env target eq in -(* new_neg, new_pos *) (List.filter (fun e -> not (List.exists (f Negative e) all)) new_neg, List.filter (fun e -> not (List.exists (f Positive e) all)) new_pos) ;; let backward_simplify_active env (new_neg, new_pos) active = - let new_pos = List.map (fun e -> Positive, e) new_pos in - let active, newa = + let active_list, active_table = active in + let new_pos, new_table = + List.fold_left + (fun (l, t) e -> (Positive, e)::l, Indexing.index t e) + ([], Hashtbl.create (List.length new_pos)) new_pos + in + let active_list, newa = List.fold_right (fun (s, equality) (res, newn) -> - match forward_simplify env (s, equality) new_pos with - | None when s = Negative -> - Printf.printf "\nECCO QUI: %s\n" - (string_of_equality ~env equality); - print_newline (); - res, newn + match forward_simplify env (s, equality) (new_pos, new_table) with | None -> res, newn | Some (s, e) -> if equality = e then (s, e)::res, newn - else + else res, (s, e)::newn) - active ([], []) + active_list ([], []) in let find eq1 where = List.exists (fun (s, e) -> meta_convertibility_eq eq1 e) where in let active, newa = - let f (s, eq) res = - if (is_identity env eq) || (find eq res) then res else (s, eq)::res - in List.fold_right - (fun (s, eq) res -> - if (is_identity env eq) || (find eq res) then res else (s, eq)::res) - active [], + (fun (s, eq) (res, tbl) -> + if (is_identity env eq) || (find eq res) then + res, tbl + else + (s, eq)::res, if s = Negative then tbl else Indexing.index tbl eq) + active_list ([], Hashtbl.create (List.length active_list)), List.fold_right (fun (s, eq) (n, p) -> if (s <> Negative) && (is_identity env eq) then @@ -384,10 +379,14 @@ let backward_simplify_active env (new_neg, new_pos) active = let backward_simplify_passive env (new_neg, new_pos) passive = - let new_pos = List.map (fun e -> Positive, e) new_pos in - let (nl, ns), (pl, ps) = passive in + let new_pos, new_table = + List.fold_left + (fun (l, t) e -> (Positive, e)::l, Indexing.index t e) + ([], Hashtbl.create (List.length new_pos)) new_pos + in + let (nl, ns), (pl, ps), passive_table = passive in let f sign equality (resl, ress, newn) = - match forward_simplify env (sign, equality) new_pos with + match forward_simplify env (sign, equality) (new_pos, new_table) with | None -> resl, EqualitySet.remove equality ress, newn | Some (s, e) -> if equality = e then @@ -398,9 +397,13 @@ let backward_simplify_passive env (new_neg, new_pos) passive = in let nl, ns, newn = List.fold_right (f Negative) nl ([], ns, []) and pl, ps, newp = List.fold_right (f Positive) pl ([], ps, []) in + let passive_table = + List.fold_left + (fun tbl e -> Indexing.index tbl e) (Hashtbl.create (List.length pl)) pl + in match newn, newp with - | [], [] -> ((nl, ns), (pl, ps)), None - | _, _ -> ((nl, ns), (pl, ps)), Some (newn, newp) + | [], [] -> ((nl, ns), (pl, ps), passive_table), None + | _, _ -> ((nl, ns), (pl, ps), passive_table), Some (newn, newp) ;; @@ -408,34 +411,21 @@ let backward_simplify env new' ?passive active = let active, newa = backward_simplify_active env new' active in match passive with | None -> - active, (([], EqualitySet.empty), ([], EqualitySet.empty)), newa, None + active, (make_passive [] []), newa, None | Some passive -> let passive, newp = backward_simplify_passive env new' passive in active, passive, newa, newp ;; - let rec given_clause env passive active = match passive_is_empty passive with | true -> Failure | false -> -(* Printf.printf "before select\n"; *) let (sign, current), passive = select env passive active in -(* Printf.printf "before simplification: sign: %s\ncurrent: %s\n\n" *) -(* (string_of_sign sign) (string_of_equality ~env current); *) match forward_simplify env (sign, current) ~passive active with -(* | None when sign = Negative -> *) -(* Printf.printf "OK!!! %s %s" (string_of_sign sign) *) -(* (string_of_equality ~env current); *) -(* print_newline (); *) -(* let proof, _, _, _ = current in *) -(* Success (Some proof, env) *) | None -> -(* Printf.printf "avanti... %s %s" (string_of_sign sign) *) -(* (string_of_equality ~env current); *) -(* print_newline (); *) given_clause env passive active | Some (sign, current) -> if (sign = Negative) && (is_identity env current) then ( @@ -466,16 +456,23 @@ let rec given_clause env passive active = match newa with | None -> active | Some (n, p) -> - let nn = List.map (fun e -> Negative, e) n - and pp = List.map (fun e -> Positive, e) p in - nn @ active @ pp + let al, tbl = active in + let nn = List.map (fun e -> Negative, e) n in + let pp, tbl = + List.fold_right + (fun e (l, t) -> + (Positive, e)::l, + Indexing.index tbl e) + p ([], tbl) + in + nn @ al @ pp, tbl in let _ = Printf.printf "active:\n%s\n" (String.concat "\n" ((List.map (fun (s, e) -> (string_of_sign s) ^ " " ^ - (string_of_equality ~env e)) active))); + (string_of_equality ~env e)) (fst active)))); print_newline (); in let _ = @@ -494,12 +491,14 @@ let rec given_clause env passive active = match contains_empty env new' with | false, _ -> let active = + let al, tbl = active in match sign with - | Negative -> (sign, current)::active - | Positive -> active @ [(sign, current)] + | Negative -> (sign, current)::al, tbl + | Positive -> + al @ [(sign, current)], Indexing.index tbl current in let passive = add_to_passive passive new' in - let (_, ns), (_, ps) = passive in + let (_, ns), (_, ps), _ = passive in Printf.printf "passive:\n%s\n" (String.concat "\n" ((List.map (fun e -> "Negative " ^ @@ -520,10 +519,7 @@ let rec given_clause_fullred env passive active = match passive_is_empty passive with | true -> Failure | false -> -(* Printf.printf "before select\n"; *) let (sign, current), passive = select env passive active in -(* Printf.printf "before simplification: sign: %s\ncurrent: %s\n\n" *) -(* (string_of_sign sign) (string_of_equality ~env current); *) match forward_simplify env (sign, current) ~passive active with | None -> given_clause_fullred env passive active @@ -545,23 +541,11 @@ let rec given_clause_fullred env passive active = let active = if is_identity env current then active else + let al, tbl = active in match sign with - | Negative -> (sign, current)::active - | Positive -> active @ [(sign, current)] + | Negative -> (sign, current)::al, tbl + | Positive -> al @ [(sign, current)], Indexing.index tbl current in -(* let _ = *) -(* match new' with *) -(* | neg, pos -> *) -(* Printf.printf "new' before simpl:\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))); *) -(* print_newline (); *) -(* in *) let rec simplify new' active passive = let new' = forward_simplify_new env new' ~passive active in let active, passive, newa, retained = @@ -583,7 +567,7 @@ let rec given_clause_fullred env passive active = (String.concat "\n" ((List.map (fun (s, e) -> (string_of_sign s) ^ " " ^ - (string_of_equality ~env e)) active))); + (string_of_equality ~env e)) (fst active)))); print_newline (); in let _ = @@ -602,16 +586,6 @@ let rec given_clause_fullred env passive active = match contains_empty env new' with | false, _ -> let passive = add_to_passive passive new' in -(* let (_, ns), (_, ps) = passive in *) -(* Printf.printf "passive:\n%s\n" *) -(* (String.concat "\n" *) -(* ((List.map (fun e -> "Negative " ^ *) -(* (string_of_equality ~env e)) *) -(* (EqualitySet.elements ns)) @ *) -(* (List.map (fun e -> "Positive " ^ *) -(* (string_of_equality ~env e)) *) -(* (EqualitySet.elements ps)))); *) -(* print_newline (); *) given_clause_fullred env passive active | true, proof -> Success (proof, env) @@ -656,7 +630,7 @@ let main () = try let term_equality = equality_of_term meta_proof goal in let meta_proof, (eq_ty, left, right, ordering), _, _ = term_equality in - let active = [] in + let active = make_active () in let passive = make_passive [term_equality] equalities in Printf.printf "\ncurrent goal: %s\n" (string_of_equality ~env term_equality);