nets.ml

   1 (* ========================================================================= *)
   2 (* Term nets: reasonably fast lookup based on term matchability.             *)
   3 (*                                                                           *)
   4 (*       John Harrison, University of Cambridge Computer Laboratory          *)
   5 (*                                                                           *)
   6 (*            (c) Copyright, University of Cambridge 1998                    *)
   7 (*              (c) Copyright, John Harrison 1998-2007                       *)
   8 (* ========================================================================= *)
   9
  10 needs "basics.ml";;
  11
  12 (* ------------------------------------------------------------------------- *)
  13 (* Term nets are a finitely branching tree structure; at each level we       *)
  14 (* have a set of branches and a set of "values". Linearization is            *)
  15 (* performed from the left of a combination; even in iterated                *)
  16 (* combinations we look at the head first. This is probably fastest, and     *)
  17 (* anyway it's useful to allow our restricted second order matches: if       *)
  18 (* the head is a variable then then whole term is treated as a variable.     *)
  19 (* ------------------------------------------------------------------------- *)
  20
  21 type term_label = Vnet                          (* variable (instantiable)   *)
  22                  | Lcnet of (string * int)      (* local constant            *)
  23                  | Cnet of (string * int)       (* constant                  *)
  24                  | Lnet of int;;                (* lambda term (abstraction) *)
  25
  26 type 'a net = Netnode of (term_label * 'a net) list * 'a list;;
  27
  28 (* ------------------------------------------------------------------------- *)
  29 (* The empty net.                                                            *)
  30 (* ------------------------------------------------------------------------- *)
  31
  32 let empty_net = Netnode([],[]);;
  33
  34 (* ------------------------------------------------------------------------- *)
  35 (* Insert a new element into a net.                                          *)
  36 (* ------------------------------------------------------------------------- *)
  37
  38 let enter =
  39   let label_to_store lconsts tm =
  40     let op,args = strip_comb tm in
  41     if is_const op then Cnet(fst(dest_const op),length args),args
  42     else if is_abs op then
  43       let bv,bod = dest_abs op in
  44       let bod' = if mem bv lconsts then vsubst [genvar(type_of bv),bv] bod
  45                  else bod in
  46       Lnet(length args),bod'::args
  47     else if mem op lconsts then Lcnet(fst(dest_var op),length args),args
  48     else Vnet,[] in
  49   let canon_eq x y =
  50     try Pervasives.compare x y = 0 with Invalid_argument _ -> false
  51   and canon_lt x y =
  52     try Pervasives.compare x y < 0 with Invalid_argument _ -> false in
  53   let rec sinsert x l =
  54     if l = [] then [x] else
  55     let h = hd l in
  56     if canon_eq h x then failwith "sinsert" else
  57     if canon_lt x h then x::l else
  58     h::(sinsert x (tl l)) in
  59   let set_insert x l = try sinsert x l with Failure "sinsert" -> l in
  60   let rec net_update lconsts (elem,tms,Netnode(edges,tips)) =
  61     match tms with
  62       [] -> Netnode(edges,set_insert elem tips)
  63     | (tm::rtms) ->
  64           let label,ntms = label_to_store lconsts tm in
  65           let child,others =
  66             try (snd F_F I) (remove (fun (x,y) -> x = label) edges)
  67             with Failure _ -> (empty_net,edges) in
  68           let new_child = net_update lconsts (elem,ntms@rtms,child) in
  69           Netnode ((label,new_child)::others,tips) in
  70   fun lconsts (tm,elem) net -> net_update lconsts (elem,[tm],net);;
  71
  72 (* ------------------------------------------------------------------------- *)
  73 (* Look up a term in a net and return possible matches.                      *)
  74 (* ------------------------------------------------------------------------- *)
  75
  76 let lookup =
  77   let label_for_lookup tm =
  78     let op,args = strip_comb tm in
  79     if is_const op then Cnet(fst(dest_const op),length args),args
  80     else if is_abs op then Lnet(length args),(body op)::args
  81     else Lcnet(fst(dest_var op),length args),args in
  82   let rec follow (tms,Netnode(edges,tips)) =
  83     match tms with
  84       [] -> tips
  85     | (tm::rtms) ->
  86           let label,ntms = label_for_lookup tm in
  87           let collection =
  88             try let child = assoc label edges in
  89                 follow(ntms @ rtms, child)
  90             with Failure _ -> [] in
  91           if label = Vnet then collection else
  92           try collection @ follow(rtms,assoc Vnet edges)
  93           with Failure _ -> collection in
  94   fun tm net -> follow([tm],net);;
  95
  96 (* ------------------------------------------------------------------------- *)
  97 (* Function to merge two nets (code from Don Syme's hol-lite).               *)
  98 (* ------------------------------------------------------------------------- *)
  99
 100 let merge_nets =
 101   let canon_eq x y =
 102     try Pervasives.compare x y = 0 with Invalid_argument _ -> false
 103   and canon_lt x y =
 104     try Pervasives.compare x y < 0 with Invalid_argument _ -> false in
 105   let rec set_merge l1 l2 =
 106     if l1 = [] then l2
 107     else if l2 = [] then l1 else
 108     let h1 = hd l1 and t1 = tl l1
 109     and h2 = hd l2 and t2 = tl l2 in
 110     if canon_eq h1 h2 then h1::(set_merge t1 t2)
 111     else if canon_lt h1 h2 then h1::(set_merge t1 l2)
 112     else h2::(set_merge l1 t2) in
 113   let rec merge_nets (Netnode(l1,data1),Netnode(l2,data2)) =
 114     let add_node ((lab,net) as p) l =
 115       try let (lab',net'),rest = remove (fun (x,y) -> x = lab) l in
 116           (lab',merge_nets (net,net'))::rest
 117       with Failure _ -> p::l in
 118     Netnode(itlist add_node l2 (itlist add_node l1 []),
 119             set_merge data1 data2) in
 120   merge_nets;;