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