(****************** Equation manipulations *************)

open Prelude;;
open Terms;;

type rule = int * (int * (term * term));;

(* standardizes an equation so its variables are 1,2,... *)

let mk_rule m n =
  let all_vars = union (vars m) (vars n) in
  let (k,subst) =
    List.fold_left
      (fun (i, sigma) v -> (i + 1,(v, Var(i)) :: sigma)) (1, []) all_vars in
  (k - 1, (substitute subst m, substitute subst n))
;;

(* checks that rules are numbered in sequence and returns their number *)
let (check_rules: rule list -> int) =
  List.fold_left
   (fun n (k, _) ->
     if k = n + 1 then k else failwith "Rule numbers not in sequence") 0
;;

let pretty_rule (k,(_,(m,n)): rule) =
  print_int k; print_string " : ";
  pretty_term m; print_string " = "; pretty_term n;
  print_newline()
;;

let pretty_rules = List.iter pretty_rule
;; 

(****************** Rewriting **************************)

(* Top-level rewriting. Let eq:l=r be an equation, m be a term such that l<=m.
   With sigma = matching l m, we define the image of m by eq as sigma(r) *)
let reduce l m =
  substitute (matching l m)
;;

(* A more efficient version of can (rewrite1 (l, r)) for r arbitrary *)
let reducible l =
  let rec redrec m =
    try
      let _ = matching l m in true
    with Failure _ ->
      match m with
      | Term(_, sons) -> List.exists redrec sons
      | _ -> false in
  redrec
;;

(* mreduce : rules -> term -> term *)
let mreduce rules m =
  let redex (_, (_, (l, r))) = reduce l m r in try_find redex rules
;;

(* One step of rewriting in leftmost-outermost strategy, with multiple rules *)
(* fails if no redex is found *)
(* mrewrite1 : rules -> term -> term *)
let mrewrite1 rules =
  let rec rewrec m =
    try
      mreduce rules m
    with Failure _ ->
      let rec tryrec = function
        | [] -> failwith "mrewrite1"
        | son :: rest ->
            try
              rewrec son :: rest
            with Failure _ ->
              son :: tryrec rest in
      match m with
      | Term (f, sons) -> Term (f, tryrec sons)
      | _ -> failwith "mrewrite1" in
  rewrec
;;

(* Iterating rewrite1. Returns a normal form. May loop forever *)
(* mrewrite_all : rules -> term -> term *)
let mrewrite_all rules m =
  let rec rew_loop m =
    try
      rew_loop(mrewrite1 rules m)
    with Failure _ -> m in
  rew_loop m
;;

(*
pretty_term (mrewrite_all Group_rules m where m,_=<<A*(I(B)*B)>>);;
==> A*U
*)