1structure quote :> quote = 2struct 3 4open HolKernel Parse boolLib quoteTheory; 5 6structure Parse = 7struct 8 open Parse 9 val (Type,Term) = parse_from_grammars quoteTheory.quote_grammars 10end 11 12fun QUOTE_ERR function message = 13 HOL_ERR{origin_structure = "quote", 14 origin_function = function, 15 message = message}; 16 17fun mk_comb2 (a,b,c) = mk_comb(mk_comb(a,b),c); 18fun mk_comb3 (a,b,c,d) = mk_comb(mk_comb2(a,b,c),d); 19 20(* reify varmap *) 21val mevm = ���Empty_vm : 'a varmap���; 22val mnvm = ���Node_vm : 'a->'a varmap->'a varmap->'a varmap���; 23fun vm_ty ty = inst [alpha |-> ty]; 24 25 26datatype varnode 27 = Lf 28 | Nd of term * varnode ref * varnode ref 29 30type varmap = varnode ref; 31 32fun meta_map ty = 33 let val mevm = vm_ty ty mevm 34 val mnvm = vm_ty ty mnvm 35 fun meta_rec r = case !r of 36 Lf => mevm 37 | (Nd(t,v1,v2)) => 38 mk_comb3(mnvm,t,meta_rec v1, meta_rec v2) 39 in meta_rec 40 end 41; 42 43 44 45(* abstract term and compute the varmap *) 46 47datatype index = Li of index | Lr of index | Ei; 48 49val mli = ���Left_idx��� 50val mri = ���Right_idx��� 51val mei = ���End_idx���; 52 53fun meta_index Ei = mei 54 | meta_index (Li i) = mk_comb(mli, meta_index i) 55 | meta_index (Lr i) = mk_comb(mri, meta_index i) 56; 57 58 59fun search_term t vm = 60 case !vm of 61 Lf => NONE 62 | Nd(x,v1,v2) => 63 (if aconv t x then SOME Ei 64 else case search_term t v1 of 65 SOME i => SOME (Li i) 66 | NONE => 67 (case search_term t v2 of 68 SOME i => SOME (Lr i) 69 | NONE => NONE)); 70 71 72fun add_term t vm i = 73 case (i, !vm) of 74 (1, Lf) => (vm := Nd(t,ref Lf, ref Lf); Ei) 75 | (n, Nd(_,v1,v2)) => 76 if n mod 2 = 0 then Li (add_term t v1 (i div 2)) 77 else Lr (add_term t v2 (i div 2)) 78 | _ => raise QUOTE_ERR "add_term" ""; 79 80 81type vmdb = (varnode ref * int ref) 82fun empty_map () = (ref Lf, ref 0) 83 84fun get_map ((vm, _) : vmdb) ty = 85 let 86 val meta = meta_map ty 87 in 88 fn () => meta vm 89 end 90 91fun term_index ((vm,size): vmdb) t = 92 case search_term t vm of 93 SOME i => i 94 | _ => 95 let val _ = size := (!size) + 1 in 96 add_term t vm (!size) 97 end 98 99 100 101datatype expr = 102 Pvar of index 103 | Pquote of term 104 | Pnode of term * expr list 105; 106 107fun is_quote (Pquote _) = true | is_quote _ = false; 108fun mk_op t h l = if all is_quote l then Pquote t else Pnode(h,l); 109 110 111 112fun op_assoc x [] = NONE 113 | op_assoc x ((y,v)::l) = if (aconv x y) then SOME v else op_assoc x l 114; 115 116 117fun meta_expr ty is_qu { Op1, Op2, Vars, Csts } = 118 let 119 fun meta_rec vmdb t = 120 let 121 val meta_rec = meta_rec vmdb 122 in 123 if is_qu t then Pquote t 124 else 125 let val oper = 126 if is_comb t then 127 let val (r1,a1) = dest_comb t in 128 case op_assoc r1 Op1 of 129 SOME ope => SOME(mk_op t ope [meta_rec a1]) 130 | NONE => 131 if is_comb r1 then 132 let val (r2,a2) = dest_comb r1 in 133 case op_assoc r2 Op2 of 134 SOME ope => 135 SOME(mk_op t ope [meta_rec a2, meta_rec a1]) 136 | NONE => NONE 137 end 138 else NONE 139 end 140 else NONE 141 in 142 case oper of 143 SOME mt => mt 144 | NONE => Pvar (term_index vmdb t) 145 end 146 end 147 148 fun meta_pol (Pvar i) = mk_comb(Vars,meta_index i) 149 | meta_pol (Pquote t) = mk_comb(Csts,t) 150 | meta_pol (Pnode(h,l)) = foldl(fn(a,ht) => mk_comb(ht,meta_pol a)) h l 151 152 fun non_trivial (Pvar _) = 153 raise QUOTE_ERR "meta_expr" "unrecognized polynomial expression" 154 | non_trivial p = p 155 156 fun mpol vmdb = meta_pol o non_trivial o meta_rec vmdb 157 fun mk_map vmdb = get_map vmdb ty 158 159 fun meta_list lt = 160 let val vmdb = empty_map() 161 val lmt = map (mpol vmdb) lt 162 val mm = mk_map vmdb () 163 in 164 {Metamap=mm,Poly=lmt} 165 end 166 in 167 meta_list 168 end; 169 170end; 171