(* ========================================================================= *)
(* Term nets: reasonably fast lookup based on term matchability.             *)
(*                                                                           *)
(*       John Harrison, University of Cambridge Computer Laboratory          *)
(*                                                                           *)
(*            (c) Copyright, University of Cambridge 1998                    *)
(*              (c) Copyright, John Harrison 1998-2007                       *)
(* ========================================================================= *)

needs "basics.ml";;

(* ------------------------------------------------------------------------- *)
(* Term nets are a finitely branching tree structure; at each level we       *)
(* have a set of branches and a set of "values". Linearization is            *)
(* performed from the left of a combination; even in iterated                *)
(* combinations we look at the head first. This is probably fastest, and     *)
(* anyway it's useful to allow our restricted second order matches: if       *)
(* the head is a variable then then whole term is treated as a variable.     *)
(* ------------------------------------------------------------------------- *)

type term_label = Vnet                          (* variable (instantiable)   *)
                 | Lcnet of (string * int)      (* local constant            *)
                 | Cnet of (string * int)       (* constant                  *)
                 | Lnet of int                  (* lambda term (abstraction) *)
                 | Qnet of hol_type             (* quoted term               *) 
                 | Hnet of hol_type             (* holed term                *)
                 | Enet of hol_type;;           (*Eval term                  *)
type 'a net = Netnode of (term_label * 'a net) list * 'a list;;

(* ------------------------------------------------------------------------- *)
(* The empty net.                 
                                           *)
(* ------------------------------------------------------------------------- *)

let empty_net = Netnode([],[]);;

(* ------------------------------------------------------------------------- *)
(* Insert a new element into a net.                                          *)
(* ------------------------------------------------------------------------- *)

let enter =
  let label_to_store lconsts tm =
    let op,args = strip_comb tm in
    if is_const op then Cnet(fst(dest_const op),length args),args
    else if is_abs op then
      let bv,bod = dest_abs op in
      let bod' = if mem bv lconsts then vsubst [genvar(type_of bv),bv] bod
                 else bod in
      Lnet(length args),bod'::args
    else if mem op lconsts then Lcnet(fst(dest_var op),length args),args
    else if is_quote op then (Qnet (type_of (dest_quote op))) ,args
    else if is_hole op then (Hnet (snd (dest_hole op))) , args
    else if is_eval op then (Enet (snd (dest_eval op))) , args 
    else Vnet,[] in
  let canon_eq x y =
    try Pervasives.compare x y = 0 with Invalid_argument _ -> false
  and canon_lt x y =
    try Pervasives.compare x y < 0 with Invalid_argument _ -> false in
  let rec sinsert x l =
    if l = [] then [x] else
    let h = hd l in
    if canon_eq h x then failwith "sinsert" else
    if canon_lt x h then x::l else
    h::(sinsert x (tl l)) in
  let set_insert x l = try sinsert x l with Failure "sinsert" -> l in
  let rec net_update lconsts (elem,tms,Netnode(edges,tips)) =
    match tms with
      [] -> Netnode(edges,set_insert elem tips)
    | (tm::rtms) ->
          let label,ntms = label_to_store lconsts tm in
          let child,others =
            try (snd F_F I) (remove (fun (x,y) -> x = label) edges)
            with Failure _ -> (empty_net,edges) in
          let new_child = net_update lconsts (elem,ntms@rtms,child) in
          Netnode ((label,new_child)::others,tips) in
  fun lconsts (tm,elem) net -> net_update lconsts (elem,[tm],net);;

(* ------------------------------------------------------------------------- *)
(* Look up a term in a net and return possible matches.                      *)
(* ------------------------------------------------------------------------- *)

(*Potential cause for define bug is in here:
  define uses REWRITE_CONV
  REWRITE_CONV uses lookup
  Lookup is not working properly for anything inside a hole
  *)

let lookup =
  let rec label_for_lookup tm = 
    let op,args = strip_comb tm in
    if is_const op then Cnet(fst(dest_const op),length args),args
    else if is_abs op then Lnet(length args),(body op)::args
    else if is_quote op then (Qnet (type_of (dest_quote op))),args
    else if is_hole op then (Hnet (snd (dest_hole op))),args
    else if is_eval op then (Enet (snd (dest_eval op))),args
    else Lcnet(fst(dest_var op),length args),args in
  let rec follow (tms,Netnode(edges,tips)) =
    match tms with
      [] -> tips
    | (tm::rtms) ->
          let label,ntms = label_for_lookup tm in
          let collection =
            try let child = assoc label edges in
                follow(ntms @ rtms, child)
            with Failure _ -> [] in
          if label = Vnet then collection else
          try collection @ follow(rtms,assoc Vnet edges)
          with Failure _ -> collection in
  fun tm net -> follow([tm],net);;

(* ------------------------------------------------------------------------- *)
(* Function to merge two nets (code from Don Syme's hol-lite).               *)
(* ------------------------------------------------------------------------- *)

let merge_nets =
  let canon_eq x y =
    try Pervasives.compare x y = 0 with Invalid_argument _ -> false
  and canon_lt x y =
    try Pervasives.compare x y < 0 with Invalid_argument _ -> false in
  let rec set_merge l1 l2 =
    if l1 = [] then l2
    else if l2 = [] then l1 else
    let h1 = hd l1 and t1 = tl l1
    and h2 = hd l2 and t2 = tl l2 in
    if canon_eq h1 h2 then h1::(set_merge t1 t2)
    else if canon_lt h1 h2 then h1::(set_merge t1 l2)
    else h2::(set_merge l1 t2) in
  let rec merge_nets (Netnode(l1,data1),Netnode(l2,data2)) =
    let add_node ((lab,net) as p) l =
      try let (lab',net'),rest = remove (fun (x,y) -> x = lab) l in
          (lab',merge_nets (net,net'))::rest
      with Failure _ -> p::l in
    Netnode(itlist add_node l2 (itlist add_node l1 []),
            set_merge data1 data2) in
  merge_nets;;