(*
    ||M||  This file is part of HELM, an Hypertextual, Electronic        
    ||A||  Library of Mathematics, developed at the Computer Science     
    ||T||  Department, University of Bologna, Italy.                     
    ||I||                                                                
    ||T||  HELM is free software; you can redistribute it and/or         
    ||A||  modify it under the terms of the GNU General Public License   
    \   /  version 2 or (at your option) any later version.      
     \ /   This software is distributed as is, NO WARRANTY.     
      V_______________________________________________________________ *)

(* $Id$ *)

type aux_comparison = XEQ | XLE | XGE | XLT | XGT | XINCOMPARABLE

module Orderings (B : Terms.Blob) = struct

  type weight = int * (int * int) list;;
  
  let string_of_weight (cw, mw) =
    let s =
      String.concat ", "
        (List.map (function (m, w) -> Printf.sprintf "(%d,%d)" m w) mw)
    in
    Printf.sprintf "[%d; %s]" cw s
  ;;
  
  let weight_of_term term =
    let vars_dict = Hashtbl.create 5 in
    let rec aux = function
      | Terms.Var i -> 
          (try
             let oldw = Hashtbl.find vars_dict i in
             Hashtbl.replace vars_dict i (oldw+1)
           with Not_found ->
             Hashtbl.add vars_dict i 1);
          0
      | Terms.Leaf _ -> 1
      | Terms.Node l -> List.fold_left (+) 0 (List.map aux l)
    in
    let w = aux term in
    let l =
      Hashtbl.fold (fun meta metaw resw -> (meta, metaw)::resw) vars_dict [] 
    in
    let compare w1 w2 = 
      match w1, w2 with
      | (m1, _), (m2, _) -> m2 - m1 
    in 
    (w, List.sort compare l) (* from the biggest meta to the smallest (0) *)
  ;;
  
  let compute_unit_clause_weight = 
    let weight_of_polynomial w m =
      let factor = 2 in      
      w + factor * List.fold_left (fun acc (_,occ) -> acc+occ) 0 m
    in
    function
    | Terms.Predicate t -> 
        let w, m = weight_of_term t in 
        weight_of_polynomial w m
    | Terms.Equation (_,x,_,Terms.Lt)
    | Terms.Equation (x,_,_,Terms.Gt) ->
        let w, m = weight_of_term x in 
        weight_of_polynomial w m
    | Terms.Equation (l,r,_,Terms.Eq) 
    | Terms.Equation (l,r,_,Terms.Incomparable) ->
        let wl, ml = weight_of_term l in 
        let wr, mr = weight_of_term r in 
        weight_of_polynomial (wl+wr) (ml@mr)
  ;;
  
  (* returns a "normalized" version of the polynomial weight wl (with type
   * weight list), i.e. a list sorted ascending by meta number,
   * from 0 to maxmeta. wl must be sorted descending by meta number. Example:
   * normalize_weight 5 (3, [(3, 2); (1, 1)]) ->
   *      (3, [(1, 1); (2, 0); (3, 2); (4, 0); (5, 0)]) *)
  let normalize_weight maxmeta (cw, wl) =
    let rec aux = function
      | 0 -> []
      | m -> (m, 0)::(aux (m-1))
    in
    let tmpl = aux maxmeta in
    let wl =
      List.sort
        (fun (m, _) (n, _) -> Pervasives.compare m n)
        (List.fold_left
           (fun res (m, w) -> (m, w)::(List.remove_assoc m res)) tmpl wl)
    in
    (cw, wl)
  ;;
  
  
  let normalize_weights (cw1, wl1) (cw2, wl2) =
    let rec aux wl1 wl2 =
      match wl1, wl2 with
      | [], [] -> [], []
      | (m, w)::tl1, (n, w')::tl2 when m = n ->
          let res1, res2 = aux tl1 tl2 in
          (m, w)::res1, (n, w')::res2
      | (m, w)::tl1, ((n, w')::_ as wl2) when m < n ->
          let res1, res2 = aux tl1 wl2 in
          (m, w)::res1, (m, 0)::res2
      | ((m, w)::_ as wl1), (n, w')::tl2 when m > n ->
          let res1, res2 = aux wl1 tl2 in
          (n, 0)::res1, (n, w')::res2
      | [], (n, w)::tl2 ->
          let res1, res2 = aux [] tl2 in
          (n, 0)::res1, (n, w)::res2
      | (m, w)::tl1, [] ->
          let res1, res2 = aux tl1 [] in
          (m, w)::res1, (m, 0)::res2
      | _, _ -> assert false
    in
    let cmp (m, _) (n, _) = compare m n in
    let wl1, wl2 = aux (List.sort cmp wl1) (List.sort cmp wl2) in
    (cw1, wl1), (cw2, wl2)
  ;;
  
  (* Riazanov: 3.1.5 pag 38 *)
  (* TODO: optimize early detection of XINCOMPARABLE case *)
  let compare_weights (h1, w1) (h2, w2) =
    let res, diffs =
      try
        List.fold_left2
          (fun ((lt, eq, gt), diffs) w1 w2 ->
             match w1, w2 with
             | (meta1, w1), (meta2, w2) when meta1 = meta2 ->
                 let diffs = (w1 - w2) + diffs in 
                 let r = compare w1 w2 in
                 if r < 0 then (lt+1, eq, gt), diffs
                 else if r = 0 then (lt, eq+1, gt), diffs
                 else (lt, eq, gt+1), diffs
             | _ -> assert false)
          ((0, 0, 0), 0) w1 w2
      with Invalid_argument _ -> assert false
    in
    let hdiff = h1 - h2 in 
    match res with
    | (0, _, 0) ->
        if hdiff < 0 then XLT
        else if hdiff > 0 then XGT
        else XEQ 
    | (m, _, 0) ->
        if hdiff <= 0 then XLT
        else if (- diffs) >= hdiff then XLE else XINCOMPARABLE
    | (0, _, m) ->
        if hdiff >= 0 then XGT
        else if diffs >= (- hdiff) then XGE else XINCOMPARABLE
    | (m, _, n) when m > 0 && n > 0 -> XINCOMPARABLE
    | _ -> assert false 
  ;;
  
  (* Riazanov: p. 40, relation >>> 
   * if head_only=true then it is not >>> but helps case 2 of 3.14 p 39 *)
  let rec aux_ordering ?(head_only=false) t1 t2 =
    match t1, t2 with
    (* 1. *)
    | Terms.Var _, _
    | _, Terms.Var _ -> XINCOMPARABLE
    (* 2.a *)
    | Terms.Leaf a1, Terms.Leaf a2 -> 
        let cmp = B.compare a1 a2 in
        if cmp = 0 then XEQ else if cmp < 0 then XLT else XGT
    | Terms.Leaf _, Terms.Node _ -> XLT
    | Terms.Node _, Terms.Leaf _ -> XGT
    (* 2.b *)
    | Terms.Node l1, Terms.Node l2 ->
        let rec cmp t1 t2 =
          match t1, t2 with
          | [], [] -> XEQ
          | _, [] -> XGT
          | [], _ -> XLT
          | hd1::tl1, hd2::tl2 ->
              let o = aux_ordering ~head_only hd1 hd2 in
              if o = XEQ && not head_only then cmp tl1 tl2 else o
        in
        cmp l1 l2
  ;;
  
  (* Riazanov: p. 40, relation >_n *)
  let nonrec_kbo t1 t2 =
    let w1 = weight_of_term t1 in
    let w2 = weight_of_term t2 in
    let w1, w2 = normalize_weights w1 w2 in
    match compare_weights w1 w2 with
    | XLE ->  (* this is .> *)
        if aux_ordering t1 t2 = XLT then XLT else XINCOMPARABLE
    | XGE -> 
        if aux_ordering t1 t2 = XGT then XGT else XINCOMPARABLE
    | XEQ -> aux_ordering t1 t2
    | res -> res
  ;;
  
  (* Riazanov: p. 38, relation > *)
  let rec kbo t1 t2 =
    let aux = aux_ordering ~head_only:true in
    let rec cmp t1 t2 =
      match t1, t2 with
      | [], [] -> XEQ
      | _, [] -> XGT
      | [], _ -> XLT
      | hd1::tl1, hd2::tl2 ->
          let o = kbo hd1 hd2 in
          if o = XEQ then cmp tl1 tl2
          else o
    in
    let w1 = weight_of_term t1 in
    let w2 = weight_of_term t2 in
    let w1, w2 = normalize_weights w1 w2 in
    let comparison = compare_weights w1 w2 in
    match comparison with
    | XLE ->
        let r = aux t1 t2 in
        if r = XLT then XLT
        else if r = XEQ then (
          match t1, t2 with
          | Terms.Node (_::tl1), Terms.Node (_::tl2) ->
              if cmp tl1 tl2 = XLT then XLT else XINCOMPARABLE
          | _, _ -> assert false
        ) else XINCOMPARABLE
    | XGE ->
        let r = aux t1 t2 in
        if r = XGT then XGT
        else if r = XEQ then (
          match t1, t2 with
          | Terms.Node (_::tl1), Terms.Node (_::tl2) ->
              if cmp tl1 tl2 = XGT then XGT else XINCOMPARABLE
          | _, _ ->  assert false
        ) else XINCOMPARABLE
    | XEQ ->
        let r = aux t1 t2 in
        if r = XEQ then (
          match t1, t2 with
          | Terms.Node (_::tl1), Terms.Node (_::tl2) -> cmp tl1 tl2
          | _, _ ->  XINCOMPARABLE
        ) else r 
    | res -> res
  ;;
            
  let compare_terms x y = 
    match nonrec_kbo x y with
    | XINCOMPARABLE -> Terms.Incomparable
    | XGT -> Terms.Gt
    | XLT -> Terms.Lt
    | XEQ -> Terms.Eq
    | _ -> assert false
  ;; 

end