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