1(* ===================================================================== 2 * FILE : $Id$ 3 * DESCRIPTION : A programmable term traversal engine for hol90 4 * 5 * AUTHOR : Donald Syme 6 * Based loosely on original HOL rewriting by 7 * Larry Paulson et al. 8 * ===================================================================== *) 9 10 11(* ===================================================================== 12 * Traversal (opening) Rules 13 * =====================================================================*) 14 15structure Travrules :> Travrules = 16struct 17 18open HolKernel Drule Psyntax liteLib Trace Opening; 19 20fun WRAP x = STRUCT_WRAP "Travrules" x; 21fun ERR x = STRUCT_ERR "Travrules" x; 22 23 24 (* --------------------------------------------------------------------- 25 * preorders 26 * ---------------------------------------------------------------------*) 27 28 val equality = boolSyntax.equality; 29 30 datatype preorder = PREORDER of term 31 * (thm -> thm -> thm) 32 * ({Rinst:term,arg:term} -> thm); 33 34 fun find_relation rel = let 35 fun f ((h as PREORDER (cid,_,_))::t) = if Opening.samerel cid rel then h 36 else f t 37 | f [] = ERR("find_relation","relation not found") 38 in 39 f 40 end; 41 42 fun ARB_TRANS thm c1 c2 = MATCH_MP thm (CONJ c1 c2); 43 44 fun mk_preorder (TRANS_THM,REFL_THM) = let 45 fun refl {Rinst,arg} = PART_MATCH rator REFL_THM (mk_comb(Rinst,arg)) 46 in 47 PREORDER (rator(rator(snd(boolSyntax.strip_forall(concl REFL_THM)))), 48 ARB_TRANS TRANS_THM, 49 refl) 50 end 51 52 (* --------------------------------------------------------------------- 53 * travrules objects and basic operations on them 54 * merge_travrules: 55 * The order of congprocs is v. significant - the list in the object 56 * gets applied left to right. Congprocs from 57 * the second of two travsets have 58 * priority - hence the "foldl" below. 59 * ---------------------------------------------------------------------*) 60 61 datatype travrules = TRAVRULES of { 62 relations : preorder list, 63 congprocs : congproc list, 64 weakenprocs : congproc list 65 }; 66 67 fun dest(TRAVRULES x) = x; 68 val gen_mk_travrules = TRAVRULES 69 70 fun rel_of_preorder (PREORDER(r,_,_)) = r 71 72 fun merge_travrules tl = let 73 val ts = map dest tl 74 fun uniquify l = let 75 val sorted = Listsort.sort (inv_img_cmp rel_of_preorder Term.compare) l 76 fun recurse acc [] = acc 77 | recurse acc [h] = h::acc 78 | recurse acc (h1::(rest as h2::t)) = 79 if samerel (rel_of_preorder h1) (rel_of_preorder h2) then 80 recurse acc rest 81 else 82 recurse (h1::acc) rest 83 in 84 recurse [] sorted 85 end 86 in 87 TRAVRULES {relations=uniquify (flatten (map #relations ts)), 88 congprocs=foldl (op @) [] (map #congprocs ts), 89 weakenprocs=flatten (map #weakenprocs ts)} 90 end; 91 92 93(* --------------------------------------------------------------------- 94 * equality_travrules 95 * ---------------------------------------------------------------------*) 96 97val EQ_preorder = let 98 fun eqrefl {Rinst,arg} = REFL arg 99in 100 PREORDER(boolSyntax.equality,TRANS,eqrefl) 101end 102val EQ_tr = gen_mk_travrules 103 {relations=[EQ_preorder], 104 congprocs=[Opening.EQ_CONGPROC], 105 weakenprocs=[]} 106 107fun cong2proc rels th = let 108 open Opening 109 val r = rel_of_congrule th 110 val PREORDER(_,_,refl) = find_relation r rels 111in 112 CONGPROC refl th 113end 114 115fun mk_travrules relns congs = 116 TRAVRULES {relations=relns, 117 congprocs=map (cong2proc relns) congs, 118 weakenprocs=[]} 119 120 121end (* struct *) 122