type path_string_elem = Cic.term;;
type path_string = path_string_elem list;;


(* needed by the retrieve_* functions, to know the arities of the "functions" *)
let arities = Hashtbl.create 11;;


let rec path_string_of_term = function
  | Cic.Meta _ -> [Cic.Implicit None]
  | Cic.Appl ((hd::tl) as l) ->
      if not (Hashtbl.mem arities hd) then
        Hashtbl.add arities hd (List.length tl);
      List.concat (List.map path_string_of_term l)
  | term -> [term]
;;


module OrderedPathStringElement = struct
  type t = path_string_elem

  let compare = Pervasives.compare
end

module PSMap = Map.Make(OrderedPathStringElement);;


module DiscriminationTree = struct
  type key = path_string
  type t = Node of (Utils.pos * Inference.equality) option * (t PSMap.t)

  let empty = Node (None, PSMap.empty)

  let rec find l t =
    match (l, t) with
    | [], Node (None, _) -> raise Not_found
    | [], Node (Some v, _) -> v
    | x::r, Node (_, m) -> find r (PSMap.find x m)
        
  let rec mem l t =
    match (l, t) with
    | [], Node (None, _) -> false
    | [], Node (Some _, _) -> true
    | x::r, Node (_, m) -> try mem r (PSMap.find x m) with Not_found -> false

  let add l v t =
    let rec ins = function
      | [], Node (_, m) -> Node (Some v, m)
      | x::r, Node (v, m) ->
	  let t' = try PSMap.find x m with Not_found -> empty in
	  let t'' = ins (r, t') in
	  Node (v, PSMap.add x t'' m)
    in
    ins (l, t)

  let rec remove l t =
    match (l, t) with
    | [], Node (_, m) -> Node (None, m)
    | x::r, Node (v, m) -> 
	try
	  let t' = remove r (PSMap.find x m) in
	  Node (v, if t' = empty then PSMap.remove x m else PSMap.add x t' m)
	with Not_found ->
	  t

  let rec fold f t acc =
    let rec traverse revp t acc = match t with
      | Node (None, m) -> 
	  PSMap.fold (fun x -> traverse (x::revp)) m acc
      | Node (Some v, m) -> 
	  f (List.rev revp) v (PSMap.fold (fun x -> traverse (x::revp)) m acc)
    in
    traverse [] t acc

end


let index tree equality =
  let _, (_, l, r, ordering), _, _ = equality in
  let psl = path_string_of_term l
  and psr = path_string_of_term r in
  match ordering with
  | Utils.Gt -> DiscriminationTree.add psl (Utils.Left, equality) tree
  | Utils.Lt -> DiscriminationTree.add psr (Utils.Right, equality) tree
  | _ ->
      let tree = DiscriminationTree.add psl (Utils.Left, equality) tree in
      DiscriminationTree.add psr (Utils.Right, equality) tree
;;


let remove_index tree equality =
  let _, (_, l, r, ordering), _, _ = equality in
  let psl = path_string_of_term l
  and psr = path_string_of_term r in
  match ordering with
  | Utils.Gt -> DiscriminationTree.remove psl tree
  | Utils.Lt -> DiscriminationTree.remove psr tree
  | _ ->
      let tree = DiscriminationTree.remove psl tree in
      DiscriminationTree.remove psr tree
;;


let in_index tree equality =
  let _, (_, l, r, ordering), _, _ = equality in
  let psl = path_string_of_term l
  and psr = path_string_of_term r in
  let meta_convertibility = Inference.meta_convertibility_eq equality in
  let ok ps =
    try let _, eq = DiscriminationTree.find ps tree in meta_convertibility eq
    with Not_found -> false
  in
  (ok psl) || (ok psr)
;;


let head_of_term = function
  | Cic.Appl (hd::tl) -> hd
  | term -> term
;;


let rec subterm_at_pos pos term =
  match pos with
  | [] -> term
  | index::pos ->
      match term with
      | Cic.Appl l ->
          (try subterm_at_pos pos (List.nth l index) with _ -> raise Not_found)
      | _ -> raise Not_found
;;


let next_t pos term =
  let t = subterm_at_pos pos term in
  try
    let t2 = subterm_at_pos [1] t in
    pos @ [1]
  with Not_found ->
    match pos with
    | [] -> [1]
    | pos -> List.fold_right (fun i r -> if r = [] then [i+1] else i::r) pos []
;;


let rec after_t pos term =
  let pos' =
    match pos with
    | [] -> raise Not_found
    | pos -> List.fold_right (fun i r -> if r = [] then [i+1] else i::r) pos []
  in
  try
    let t = subterm_at_pos pos' term in pos'
  with Not_found ->
    let pos, _ =
      List.fold_right
        (fun i (r, b) -> if b then (i::r, true) else (r, true)) pos ([], false)
    in
    after_t pos term
;;


let retrieve_generalizations tree term =
  let rec retrieve tree term pos = 
    match tree with
    | DiscriminationTree.Node (value, map) ->
        let res =
          try
            let hd_term = head_of_term (subterm_at_pos pos term) in
            let n = PSMap.find hd_term map in
            match n with
            | DiscriminationTree.Node (Some s, _) -> [s]
            | DiscriminationTree.Node (None, _) ->
                retrieve n term (next_t pos term)
          with Not_found ->
            []
        in
        try
          let n = PSMap.find (Cic.Implicit None) map in
          res @ (retrieve n term (after_t pos term))
        with Not_found ->
          res
  in
  retrieve tree term []
;;


let jump_list = function
  | DiscriminationTree.Node (value, map) ->
      let rec get n tree =
        match tree with
        | DiscriminationTree.Node (v, m) ->
            if n = 0 then
              [tree]
            else
              PSMap.fold
                (fun k v res ->
                   let a = try Hashtbl.find arities k with Not_found -> 0 in
                   (get (n-1 + a) v) @ res) m []
      in
      PSMap.fold
        (fun k v res ->
           let arity = try Hashtbl.find arities k with Not_found -> 0 in
           (get arity v) @ res)
        map []
;;


let retrieve_unifiables tree term =
  let rec retrieve tree term pos =
    match tree with
    | DiscriminationTree.Node (value, map) ->
        let res = 
          try
            match subterm_at_pos pos term with
            | Cic.Meta _ ->
                List.concat
                  (List.map
                     (fun t -> retrieve t term (next_t pos term))
                     (jump_list tree))
            | subterm ->
                let hd_term = head_of_term subterm in
                let n = PSMap.find hd_term map in
                match n with
                | DiscriminationTree.Node (Some s, _) -> [s]
                | DiscriminationTree.Node (None, _) ->
                    retrieve n term (next_t pos term)
          with Not_found ->
            []
        in
        try
          let n = PSMap.find (Cic.Implicit None) map in
          res @ (retrieve n term (after_t pos term))
        with Not_found ->
          res
  in
  retrieve tree term []
;;