1(* =====================================================================
2 * FILE          : Ho_Net.sml
3 * DESCRIPTION   : Implementation of term nets, from GTT.
4 *
5 * AUTHOR        : Somebody in the ICL group.
6 * DATE          : August 26, 1991
7 * MODIFIED      : Sept 5, 1992, to use deBruijn representation
8 *
9 * MODIFIED     : Donald Syme, 1995, to add assumption-bound variables.
10 *
11 * Assumption bound variables are for storing rewrites like
12 *  [x=0] |- x = 0.
13 * Since "x" is free in the assumptions, this rewrite should only match
14 * terms which are exactly "x" on the left.  The old termnets chose this
15 * rewrite to try to rewrite every term!!
16 *
17 * This only becomes really important when you have contextual rewriting.
18 *
19 * MODIFIED    : Donald Syme, November 1995, to be keyed up to higher order
20 *               matching, based on JRH's code from GTT.
21 * ===================================================================== *)
22
23structure Ho_Net :> Ho_Net =
24struct
25
26
27open HolKernel boolSyntax;
28
29val ERR = mk_HOL_ERR "Ho_Net";
30
31(*--------------------------------------------------------------------
32 * Labels ascribed to head-operators of terms.
33 *-------------------------------------------------------------------*)
34
35datatype term_label
36   = Vnet
37   | FVnet of string * int
38   | Cnet of string * string * int
39   | Lnet of int;
40
41fun label_cmp p =
42    case p of
43      (Vnet, Vnet) => EQUAL
44    | (Vnet, _) => LESS
45    | (_, Vnet) => GREATER
46    | (FVnet f1, FVnet f2) => pair_compare (String.compare, Int.compare)
47                                           (f1, f2)
48    | (FVnet _, _) => LESS
49    | (_, FVnet _) => GREATER
50    | (Cnet (nm1,thy1,n1), Cnet(nm2,thy2,n2)) => let
51      in
52        case String.compare (nm1, nm2) of
53          EQUAL => (case String.compare(thy1, thy2) of
54                      EQUAL => Int.compare(n1, n2)
55                    | x => x)
56        | x => x
57      end
58    | (Cnet _, Lnet _) => LESS
59    | (Lnet _, Cnet _) => GREATER
60    | (Lnet n1, Lnet n2) => Int.compare(n1, n2)
61
62
63fun stored_label (fvars,tm) =
64  let val (oper,args) = strip_comb tm
65      val args' = map (fn x => (fvars,x)) args
66  in case dest_term oper
67      of CONST {Name,Thy,...} => (Cnet(Name,Thy,length args),args')
68       | LAMB (Bvar,Body) => (Lnet(length args),
69                              (subtract fvars [Bvar],Body)::args')
70       | VAR (Name,_) =>
71          if mem oper fvars then (FVnet(Name,length args),args') else (Vnet,[])
72       | _ => fail()
73    end;
74
75open Binarymap
76fun label_for_lookup tm =
77  let val (oper,args) = strip_comb tm
78  in case dest_term oper
79      of CONST {Name,Thy,...} => (Cnet(Name,Thy,length args),args)
80       | LAMB (Bvar,Body) => (Lnet(length args),Body::args)
81       | VAR (Name,_) => (FVnet(Name,length args),args)
82       | _ => fail()
83  end;
84
85(* double constructor design may seem redundant but it allows us to avoid
86   a value polymorphism problem, and have a simple value for empty.
87   If you try
88     val empty = NODE(mkDict label_cmp, [])
89   then empty can't be fully polymorphic, thanks to the call to
90   mkDict. *)
91datatype 'a net = NODE of (term_label,'a net) dict * 'a list
92                | EMPTY of 'a list
93
94val empty = EMPTY []
95
96
97
98fun edges (NODE(es, _)) = es
99  | edges (EMPTY _) = mkDict label_cmp
100fun tips (NODE(_, ts)) = ts
101  | tips (EMPTY ts) = ts
102fun add_tip e (NODE(es, tips)) = NODE(es, e::tips)
103  | add_tip e (EMPTY tips) = EMPTY (e::tips)
104
105fun check_edge(NODE(es, _), label) = peek(es, label)
106  | check_edge(EMPTY _, label) = NONE
107fun new_edge(NODE(es, ts), label, n) = NODE(insert(es, label, n), ts)
108  | new_edge(EMPTY ts, label, n) = NODE(insert(mkDict label_cmp, label, n), ts)
109
110
111fun net_update (elem, tms:(term list * term) list, net) =
112   case tms of
113     [] => add_tip elem net
114   | tm::rtms =>
115        let val (label,ntms) = stored_label tm
116            val child = case check_edge(net, label) of
117                          NONE => empty
118                        | SOME n => n
119            val new_child = net_update(elem,ntms @ rtms,child)
120        in
121          new_edge(net, label, new_child)
122        end;
123
124fun follow (tms, net) =
125   case tms
126    of [] => tips net
127     | tm::rtms =>
128        let val (label,ntms) = label_for_lookup tm
129            val collection =
130                case check_edge(net, label) of
131                  NONE => []
132                | SOME child => follow(ntms @ rtms, child)
133        in
134          collection @
135          (case check_edge(net, Vnet) of
136             NONE => []
137           | SOME n' => follow(rtms,n'))
138        end;
139
140fun enter (fvars,tm,elem) net = net_update(elem,[(fvars,tm)],net);
141
142fun lookup tm net = follow([tm],net);
143
144fun merge_nets (n1, n2) = let
145  fun add_node (lab, net, m) =
146      case peek(m, lab) of
147        SOME net' => insert(m, lab, merge_nets(net, net'))
148      | NONE => insert(m, lab, net)
149in
150  NODE (foldl add_node (edges n1) (edges n2), tips n1 @ tips n2)
151end
152
153end (* struct *)
154