Made swapping of triangular summations test case pass.

src/prover_phases/RecurrencePolynomial.ml

@@ -92,9 +92,9 @@ type poly = op list list
 and op =
 | C of Z.t (* never C 1; unique if present *)
 | A of atom (* unique and last in a monomial if present *)
+| S of var
 | D of var
 | XD of var
-| S of var
 | X of op list (* never X(X p · q) or X(C p · q) or X(A I); always X(_@[A _]) *)
 | O of (var*poly)list
 
@@ -215,8 +215,6 @@ end
 
 (* From ordered group of {r₀,r₁,r₂,...} form ordered group of pseudo-ordinals r₀+r₁ω+r₂ω²+...+rₙωⁿ represented by lists [r₀;...;rₙ]. Here ω is an infinitely large element. The results are never of the form [...;0] but inputs may be. *)
 let infinities r : 'r list ord_group =
-  (* let with_same_size f = pad_tail r#o %>> uncurry f in
-  let map2_trim f = with_same_size(map2 f) %>> trim_tail(equal' r r#o) in *)
   let map2_trim f = pad_tail r#o %>> uncurry(map2 f) %>> trim_tail(is0' r) in
   object
     method compare = rev%trim_head(is0' r) %%> length_lex_list r#compare
@@ -255,9 +253,10 @@ let indeterminate_shape = function C _->`C | S _->`S | D _->`D | XD _->`XD | O _
 (* Monomial and other orders
 TODO What nonstandard invariants the order must satisfy? At least the C(oefficient)s must contribute last because ++ changes them while linearly merging monomial lists instead of full resorting. *)
 
-(* This implements monomial orders and is parameterized by weights of (simple) indeterminates. (The functions compare_poly_by and tiebreak_by are merely mutually recursive helpers.) Usage interface is provided by rev_cmp_mono and the stateful indeterminate_weights. *)
+(* This implements monomial orders and is parameterized by weights of (simple) indeterminates. (The functions compare_poly_by and tiebreak_by are merely mutually recursive helpers. Parameter weights receives the measured monomial as a context for unplanned corner cases.) Usage interface is provided by rev_cmp_mono and the stateful indeterminate_weights. *)
 let rec compare_mono_by weights = dup %%>
-  (total_weight(infinities int_alg) weights %%> compare_later_dominant)
+  let sum_weight m = total_weight(infinities int_alg) (weights m) m in
+  (sum_weight %%> compare_later_dominant)
   *** tiebreak_by weights
 
 and compare_poly_by weights = lex_list(compare_mono_by weights)
@@ -276,7 +275,7 @@ and tiebreak_by weights = rev %%> lex_list(fun x y ->
 (* Assign this to set the global monomial order. Old polynomials become invalid when the order changes (because they are sorted by the monomial order) and must not be used afterwards. However polynomials stored in clauses can still be reretrieved (see poly_as_lit_term_id and poly_of_{lit,term,id}). The weights are effectively 0-extended and compared as “signed ordinals”. Trailing zeros do not matter.
  Desing: A global switch like this has natural drawbacks. Namely we cannot abstract polynomials computations over the order which prevents e.g. parallelization and pause-resume constructs. This could become an issue with infinitely branching inferences. However the global reference is much simpler to use because otherwise all abstractions on top of polynomial arithmetic would have to take the order as paramters either explicitly or as part of module construction. 
  To define a weight function see elim_oper_args and elim_indeterminate. *)
-let indeterminate_weights: (simple_indeterminate -> int list) ref = ref~=[]
+let indeterminate_weights: (op list -> simple_indeterminate -> int list) ref = ref ~= ~=[]
 
 (* The main interface to monomial orders, conveniently reversed for sorting maximal monomial first. *)
 let rev_cmp_mono n m = compare_mono_by !indeterminate_weights m n (* Keep parameters to reread indeterminate_weights! *)
@@ -285,12 +284,13 @@ let sort_poly: poly->poly = sort rev_cmp_mono
 (* Some indeterminate weights for common elimination operations *)
 
 (* An elimination priority to certain argument terms. For example: elim_oper_args[t,2; s,1; r,1] to eliminate terms t,s,r with priority among them in t. *)
-let elim_oper_args term_weight_list : simple_indeterminate -> int list = function
+let elim_oper_args term_weight_list _ : simple_indeterminate -> int list = function
 |`T t -> cons_maybe (assq_opt t term_weight_list) []
 | _ -> []
 
+let elim_indeterminate' weight _ : simple_indeterminate -> int list = weight
 (* An elimination priority to certain indeterminates. This legacy function now almost directly delegates to its weighting parameter. *)
-let elim_indeterminate weight : simple_indeterminate -> int list = fun x -> [weight x]
+let elim_indeterminate weight _ : simple_indeterminate -> int list = fun x -> [weight x]
 
 
 (* Use this instead of the X constructor. *)
@@ -341,7 +341,13 @@ let coef_view part_of_coef : poly -> (poly * op list) list =
 (* Separate pointwise-multiplicative coefficients, e.g. 2yY+3y+4Y+5 ↦ [(2y+4, Y); (3y+5, 1)] *)
 let mul_coef_view = coef_view(function C _ | X _ -> true | _ -> false)
 let lead_coef = fst % hd % mul_coef_view	(* e.g. 2y+4 from above *)
-let lead_main_ops = snd % hd % mul_coef_view	(* e.g. [Y] from above *)
+let lead_main_ops = snd % hd % mul_coef_view	(* e.g. [Y] from above *)
+
+let rec const_mono = function
+| [] -> Z.zero
+| [[]] | [[A I]] -> Z.one
+| [[C n]] | [[C n; A I]] -> n
+| _::p -> const_mono p
 
 (* Allows to compute e.g. ∑ₙᑉᵐ s.t. ∑ₙᑉᵐ(M·P) = -Pₘ + M·∑ₙᑉᵐP and ∑ₙᑉᵐ(N·P) = Pₘ - P₀ + ∑ₙᑉᵐP *)
 let rec fold_indeterminates a f = function
@@ -407,7 +413,7 @@ let terms_in = map term_of_arg % arg_terms_in
 let poly_id_cache = Hashtable.create 4
 
 let term0 = Term.const ~ty:term (ID.make "⬮")
-exception RepresentingPolynomial of poly * Precedence.Weight.t * (simple_indeterminate -> int list)
+exception RepresentingPolynomial of poly * Precedence.Weight.t * (op list -> simple_indeterminate -> int list)
 
 (* Given polynomial P!=0, embed P into an ID idP, that idP into a Term termP, and it into a literal term0≈termP. Return all three.
  ~name is the name given to the idP, if fresh is created. If omitted, the name is (somewhat wastefully) taken to be the string representation of P, which is further annotated to support nesting the terms back into polynomials and into terms again.
@@ -515,7 +521,8 @@ and indeterminate_product x y =
   | D i, XD j when i=j -> [[XD i; D i]; [D i]]
   | O f, X g -> x_[g] >< [[O f]]
   | X(S i ::f), S j when i=j -> let _Si_Xf = [[S i]]><mul_indet[f] in (_Si_Xf><[[S i]]) ++ [[S i; X(S i :: f)]] ++ _Si_Xf
-  | O[i,[[A(V j)];[A I]]], S l when i=j&i=l -> [[S i]; []]
+  | O[i,f], S j when i=j -> let c = const_mono f in map((@)(o[i,f--const_eq_poly c])) ([[S i]] ++ const_op_poly c)
+  (* | O f, S i -> [o(filter((=)i % fst) f)] >< S i >< [o(filter((!=)i % fst) f)] (* TODO swap's semantics *) *)
   | S l, O[i,[[A(V j)];[A I]]] when i=j&i=l -> [[S i]; C Z.minus_one :: eval_at Z.zero ~var:i; []]
   | S l, O[i,[[A(V j)];[A I]]] when i=j -> [[y;x]]
   | S l, (X[A(V i)] | D i | XD i) when l!=i -> [[y;x]]
@@ -595,17 +602,17 @@ let (|~>) general special = match lead_unifiers general special with
 
 let superpose p p' = if p==p' then [] else
   match lead_unifiers p p' with
-  | Some(u,u') -> [([u]><p) -- ([u']><p')]
+  | Some(u,u') -> ["p̲p̲."|<([u]><p) -- ([u']><p')]
   | None -> []
 
-let leadrewrite r p = CCOpt.map(fun u -> p -- ([u]><r)) (r |~> p)
+let leadrewrite r p = CCOpt.map(fun u -> "rw."^str r^"\n"|<p -- ([u]><r)) (r |~> p)
 
 
 module type View = sig type t type v val view: t -> v option end
 (* Create index from mapping clause->polynomial, that can be instantiated by empty_with' default_features. *)
 module LeadRewriteIndex(P: View with type v=poly) = FV_tree.FV_IDX(struct
   type t = P.t
-  let compare = P.view %%> CCOpt.compare(compare_poly_by~=[]) (* only used by sets *)
+  let compare = P.view %%> CCOpt.compare(compare_poly_by~= ~=[]) (* only used by sets *)
   type feature_func = poly -> int
   let compute_feature f p = match P.view p with Some p when p!=_0 -> Some(FV_tree.N(f p)) | _->None
 end)
@@ -684,10 +691,16 @@ let (@.) m (i,j) = if i >= Array.length m or m.(i)=[||] then if i=j then 1 else
   else try m.(i).(j) with Invalid_argument(*"index out of bounds"*)_ -> 0
 
 
-(* The input function produces polynomials, and its mapped version is a homomorphism. *)
+(* The input function produces polynomials, and its mapped version is linear. *)
 let map_monomials f = fold_left (++) _0 % map f
 let map_indeterminates f = map_monomials(product % map f)
 let map_terms ?(vars=id) f = map_indeterminates(function A(T(t,v)) -> of_term~vars:(vars v) (f t) | x -> [[x]])
+(* Like map_indeterminates but can stop mapping early. Input: f (rest of monomial) (its outermost indeterminate) -> (`Go/`End, polynomial into product) *)
+let map_outer_indeterminates f = map_monomials(let rec loop_f m = match m with
+  | [] -> assert false (* no 0 terms in polynomials, and below recursion structure prevents the empty case *)
+  | [x] -> snd(f m x)
+  | x::n -> match f m x with `End,p -> p | `Go,p -> p >< loop_f n
+in loop_f)
 
 (* Replace every term that embeds some polynomial p by p if act_on p. *)
 let unembed act_on = map_indeterminates(function A(T(t,_)) as x -> (

src/prover_phases/summation_equality.ml

@@ -347,17 +347,15 @@ and propagate_sum i f =
   let _,f_term,_ = R.poly_as_lit_term_id f in
   let embed_sumf_rewriter = definitional_poly_clause R.(([[S i]]>< of_term~vars:(free_variables' f) f_term) -- sumf) in
   Iter.of_list(propagate_recurrences_to f)
-  |> saturate_with_order sum_blocker
+  |> saturate_with_order(R.elim_indeterminate' sum_blocker)
   |> Iter.map(map_poly_in_clause R.((><)[[S i]]))
   (* Replace each ∑ᵢf by the embedding sumf by rewriting with temporary polynomial ∑ᵢf-sumf. *)
   |> Iter.cons embed_sumf_rewriter
-  (* TODO “i” has this weight problem: sum = 2 > 1 = term, but ∑g > ∑̲∑̲g̲ *)
-  |> saturate_with_order R.(elim_indeterminate(function`S _->2 |`T sum_f when sum_f == hd(terms_in sumf) -> 1 | _->0)) (* orient the rewriter but keep sumf leading for filtering *)
+  (* We orient the rewriteter while keeping sumf leading for filtering. Hence we need W ∑ᵢ + W f > W sumf, but at the same time sumf must dominate arbitrarily deep ∑'s in excess terms as well as substitutions of f. *)
+  |> saturate_with_order(R.elim_indeterminate'(function`S _->[2] |`T sum'f when sum'f==hd(R.terms_in sumf) -> [2;1] |`T f' when f'==f_term -> [1;1] | _->[]))
   |> Iter.filter((!=)embed_sumf_rewriter) (* perhaps filtered anyway in the end *)
   (* Add the definitional N∑ᑉⁿf = ∑ᑉⁿf + fₙ with sumf embedded while f is not. *)
   |> Iter.cons(definitional_poly_clause R.(([[shift i]]><sumf) -- sumf -- f))
-  |>Iter.persistent
-  |>(~<) (* see above to-do-note *)
   |> filter_recurrences_of R.[ [[S i]]><f ] (* recurrences of sumf, but the embedding level is weird *)
 
 and propagate_subst s f =
@@ -389,40 +387,51 @@ and propagate_subst s f =
       ((ss_j, shift j), j), eq_j
     ) in
     (* We must eliminate all domain shifts except ones skipped above: dom\( rangeO s \ {j | ∃ ss_j} ) *)
-    let elimIndices = Int_set.(diff dom (diff (R.rangeO s) (of_list(List.map(function((_,j),_)->j) multishifts_and_equations)))) in
-    (* Clause prosessing chain: to f's recurrences, add 𝕊=∏S, eliminate S, push ∘s i.e. map 𝕊ⱼ↦Sⱼ, and filter *)
+    let elimIndices = Int_set.(diff dom (diff (R.rangeO s) (of_list(List.map(snd%fst) multishifts_and_equations)))) in
+    (* * * * Clause prosessing chain: to f's recurrences, add 𝕊=∏S, eliminate S, push ∘s i.e. map 𝕊ⱼ↦Sⱼ, and filter *)
     Iter.of_list(propagate_recurrences_to f)
-    |> Iter.append(Iter.of_list(map (definitional_poly_clause % snd) multishifts_and_equations))
-    |> saturate_with_order(R.elim_indeterminate(function
-      |`O[i,R.[[A I]]] -> if Int_set.mem i elimIndices then 1 else 0
-      | _ -> 0))
+    |> Iter.append(Iter.of_list(map (definitional_poly_clause % snd) multishifts_and_equations))
+    |> saturate_with_order(fun m' -> function
+      |`O[i,R.[[A(V j)];[A I]]] when i=j & Int_set.mem i elimIndices ->
+        (* Eliminate 1-shifts ...except that multishift could be simplified to 1-shift in case an excess argument term does not depend on some of the multishifted variables—a valid result of such simplification won't be penaliced. *)
+        if multishifts_and_equations |> exists R.(function(((O ss,_),_),_)-> (* ∃𝕊 *)
+          Int_set.(match assq_opt i ss with Some[[A(V j)];[A I]] when i=j -> (* 𝕊i = i+1 *)
+            equal (of_list[i]) (inter (free_variables[m']) (of_list(List.map fst ss))) (* Sᵢ goes as well *)
+          |_->false) |_->false)
+        then [] else [1]
+      | _ -> [])
+    |>(|<)"kylläinen"
     |> Iter.filter_map(fun c -> try Some(c |> map_poly_in_clause R.(fun p ->
       let cache_t_to_st = HT.create 4 in
       let p = if equational p then p else p>< of_term~vars:(free_variables' f) f_term in
       p |> map_monomials(fun m' -> [m']|>
-        (* If the substitution does not change variables in the monomial m, then m can be kept as is even if m contains shifts that were to be eliminated. This is not robust because generally the essence is that m is constant (or even satisfies more recurrences compared to f) w.r.t. some variables, while the effect of the substitution plays no rôle. *)
+        (* If the substitution does not change variables in the monomial m, then m can be kept as is, even if m contains shifts that were to be eliminated. This is not robust because generally the essence is that m is constant (or even satisfies more recurrences compared to f) w.r.t. some variables, while the effect of the substitution plays no rôle. *)
         if Int_set.inter effect_dom (free_variables[m']) = Int_set.empty then id
-        else map_indeterminates(let rec transf = function
-          | C a -> const_op_poly a
+        else map_outer_indeterminates(let rec transf upcoming = function
+          | C a -> `Go, const_op_poly a
           (* Apply substitution to terminal indeterminates. *)
-          | A I -> const_eq_poly Z.one
-          | A(V i) as x -> transf(hd(hd(mul_indet[[x]]))) >< const_eq_poly Z.one
-          | A(T(f',vars)) when CCOpt.equal poly_eq (Some f) (poly_of_term f') -> of_term~vars:(free_variables'(get_exn(poly_of_term sf_term))) sf_term
-          | A(T(t,vars)) when HT.mem cache_t_to_st t -> HT.find cache_t_to_st t
+          | A I -> `Go, const_eq_poly Z.one
+          | A(V i) as x -> CCPair.map_snd((><)(const_eq_poly Z.one)) (transf upcoming (hd(hd(mul_indet[[x]]))))
+          | A(T(f',vars)) when CCOpt.equal poly_eq (Some f) (poly_of_term f') -> `Go, of_term~vars:(free_variables'(get_exn(poly_of_term sf_term))) sf_term
+          | A(T(t,vars)) when HT.mem cache_t_to_st t -> `Go, HT.find cache_t_to_st t
           | A(T(t,vars)) ->
             let st_poly = [o s] >< get_or~default:(of_term~vars t) (poly_of_term t) in
             let _,st,_ = poly_as_lit_term_id st_poly in
             let st = of_term~vars:(free_variables' st_poly) st in
-            HT.add cache_t_to_st t st; st
+            HT.add cache_t_to_st t st; `Go,st
           (* Replace Mᵢ=X[A(V i)] by ∑ⱼmᵢⱼMⱼ. *)
-          | X[A(V i)] -> fold_left (++) _0 (map(fun j -> const_op_poly(Z.of_int(m@.(i,j))) >< [[mul_var j]]) (Int_set.to_list(R.rangeO s)))
-          (* Discard clauses still containing shifts that were to be eliminated. Since elimIndices ⊆ dom, we keep shifts of new variables that the below case interpretates as multishifts. *)
-          | O[i,[[A(V j)];[A I]]]as x when i=j & Int_set.mem i elimIndices -> raise Exit
-          (* Replace 𝕊ⱼ by Sⱼ by looking it up from multishifts_and_equations. *)
-          | O _ as x -> [[get_or~default:x (CCList.assoc_opt ~eq:indet_eq x (map(fst%fst) multishifts_and_equations))]]
-          | _ -> raise Exit
+          | X[A(V i)] -> `Go, fold_left (++) _0 (map(fun j -> const_op_poly(Z.of_int(m@.(i,j))) >< [[mul_var j]]) (Int_set.to_list(rangeO s)))
+          (* Discard clauses still containing shifts that were to be eliminated. Since elimIndices ⊆ dom, we keep shifts of new variables that the below case interpretates as multishifts that need no further transforming. *)
+          | O[i,[[A(V j)];[A I]]]as x when i=j & Int_set.mem i elimIndices -> raise Exit
+          | O[i,[[A(V j)];[A I]]]as x when i=j -> `Go,[[x]]
+          (* Replace 𝕊ⱼ by Sⱼ by looking it up from multishifts_and_equations. *)
+          | O _ as x -> (match assoc_opt ~eq:indet_eq x (map(fst%fst) multishifts_and_equations) with
+            | Some sx	-> `Go, [[sx]]
+            | None	-> `End, [o s]><[upcoming])
+          | _ -> `End, [o s]><[upcoming]
           in transf))))
       with Exit -> None)
+    |>Iter.persistent|>(|<)"muunnettu"
     |> filter_recurrences_of~lead:false [get_exn(R.poly_of_term sf_term)(* safe by definition of sf_term *)]
 
 
@@ -476,10 +485,9 @@ let sum_equality_inference clause = try
     "{ˣx+y}{ⁿm}z	- {ⁿm+1}∑ⁿBZ{ˣy}{ⁿm-n}z	";(*6 binomial *)
     "{ᵐn+1}f	- {ᵐn+1}∑ᵐ{ⁿn-m}b	";(*7 Fibonacci *)
     "γ	- {ˣm}∑ˣ{ᵐm-1-x}g	";(*8 presented *)
-    "0	- ∑ⁿ∑ᵐg	";(*9 debug *)
+    "0	- {ᵐm-1-x}g	";(*9 debug *)
   |]in(*
-    (p,)r,e: ✓
-    i: miss
+    (p,)r,e,i: ✓
     F: leviää jo {ᵐn+1}fₘ kohdalla
     c,b,A,S: leviää etenkin bₘₙ kanssa, ja useille sijoituksille jää kaavoja löytymättä
   *)
@@ -494,7 +502,7 @@ let sum_equality_inference clause = try
     go()
   in go();
   exit 1;
-  let seeSatur pp = ((~<) % Iter.to_list % saturate_with_order~=[1] % Iter.of_list % map eq0) pp in
+  let seeSatur pp = ((~<) % Iter.to_list % saturate_with_order~= ~=[1] % Iter.of_list % map eq0) pp in
   seeSatur["vvvvv"; "vv-1"];
   seeSatur["yyx-x-y"; "yxx-x-1"];
   seeSatur[