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                              (op_set_diff aconv fvars [Bvar],Body)::args')
70       | VAR (Name,_) =>
71          if op_mem aconv oper fvars then
72            (FVnet(Name,length args),args')
73          else (Vnet,[])
74       | _ => fail()
75    end;
76
77open Binarymap
78fun label_for_lookup tm =
79  let val (oper,args) = strip_comb tm
80  in case dest_term oper
81      of CONST {Name,Thy,...} => (Cnet(Name,Thy,length args),args)
82       | LAMB (Bvar,Body) => (Lnet(length args),Body::args)
83       | VAR (Name,_) => (FVnet(Name,length args),args)
84       | _ => fail()
85  end;
86
87(* double constructor design may seem redundant but it allows us to avoid
88   a value polymorphism problem, and have a simple value for empty.
89   If you try
90     val empty = NODE(mkDict label_cmp, [])
91   then empty can't be fully polymorphic, thanks to the call to
92   mkDict. *)
93datatype 'a net = NODE of (term_label,'a net) dict * 'a list
94                | EMPTY of 'a list
95
96val empty = EMPTY []
97
98
99
100fun edges (NODE(es, _)) = es
101  | edges (EMPTY _) = mkDict label_cmp
102fun tips (NODE(_, ts)) = ts
103  | tips (EMPTY ts) = ts
104fun add_tip e (NODE(es, tips)) = NODE(es, e::tips)
105  | add_tip e (EMPTY tips) = EMPTY (e::tips)
106
107fun check_edge(NODE(es, _), label) = peek(es, label)
108  | check_edge(EMPTY _, label) = NONE
109fun new_edge(NODE(es, ts), label, n) = NODE(insert(es, label, n), ts)
110  | new_edge(EMPTY ts, label, n) = NODE(insert(mkDict label_cmp, label, n), ts)
111
112
113fun net_update (elem, tms:(term list * term) list, net) =
114   case tms of
115     [] => add_tip elem net
116   | tm::rtms =>
117        let val (label,ntms) = stored_label tm
118            val child = case check_edge(net, label) of
119                          NONE => empty
120                        | SOME n => n
121            val new_child = net_update(elem,ntms @ rtms,child)
122        in
123          new_edge(net, label, new_child)
124        end;
125
126fun follow (tms, net) =
127   case tms
128    of [] => tips net
129     | tm::rtms =>
130        let val (label,ntms) = label_for_lookup tm
131            val collection =
132                case check_edge(net, label) of
133                  NONE => []
134                | SOME child => follow(ntms @ rtms, child)
135        in
136          collection @
137          (case check_edge(net, Vnet) of
138             NONE => []
139           | SOME n' => follow(rtms,n'))
140        end;
141
142fun enter (fvars,tm,elem) net = net_update(elem,[(fvars,tm)],net);
143
144fun lookup tm net = follow([tm],net);
145
146fun merge_nets (n1, n2) = let
147  fun add_node (lab, net, m) =
148      case peek(m, lab) of
149        SOME net' => insert(m, lab, merge_nets(net, net'))
150      | NONE => insert(m, lab, net)
151in
152  NODE (foldl add_node (edges n1) (edges n2), tips n1 @ tips n2)
153end
154
155fun fold' f n A =
156    case n of
157        NODE (children, vals) =>
158        let val A1 = Portable.foldl' f vals A
159        in
160          Binarymap.foldl (fn (_, n, A) => fold' f n A) A1 children
161        end
162      | EMPTY vs => Portable.foldl' f vs A
163
164fun vfilter P n =
165    case n of
166        NODE (children, vals) =>
167        let
168          val children' = Binarymap.map (fn (_, a) => vfilter P a) children
169          val vals' = List.filter P vals
170        in
171          if Binarymap.numItems children' = 0 then EMPTY vals'
172          else NODE (children', vals')
173        end
174      | EMPTY vs => EMPTY (List.filter P vs)
175
176end (* struct *)
177