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