1structure abstraction :> abstraction =
2struct
3
4open HolKernel Parse boolLib;
5infix o |->;
6
7fun ABS_ERR function message =
8    HOL_ERR{origin_structure = "abs_tools",
9                      origin_function = function,
10                      message = message};
11
12val curr_assums = ref ([]:term list);
13val fv_ass = ref ([]:term list);
14
15
16fun add_parameter v =
17  let val _ = dest_var v in
18  fv_ass := v :: !fv_ass
19  end;
20
21fun get_assums () = !curr_assums;
22
23fun set_assums asl =
24  (curr_assums := asl;
25   fv_ass := free_varsl asl)
26;
27
28fun add_assums asl =
29  (curr_assums := rev asl @ !curr_assums;
30   fv_ass := subtract (free_varsl asl) (!fv_ass) @ !fv_ass)
31;
32
33
34fun select_disch (h,th) =
35  if HOLset.member(hypset th, h) then DISCH h th
36  else th;
37
38(* Only the variables appearing in the discharged hypothese should
39 * be generalized.
40 *)
41fun gen_assums thm =
42  GENL (!fv_ass) (foldr select_disch thm (!curr_assums));
43
44
45
46val impl_param_cstr = ref ([]:(string * term list) list);
47fun add_impl_param x p =
48  impl_param_cstr := (x,p)::(!impl_param_cstr);
49fun impl_of x =
50  map Absyn.mk_AQ (assoc x (!impl_param_cstr)) handle HOL_ERR _ => []
51
52
53
54fun head tm =
55  let val a = fst(strip_comb(lhs
56                 (snd(strip_forall(Lib.trye hd (strip_conj tm))))))
57  in
58    fst(dest_var a handle HOL_ERR _ => dest_const a)
59  end;
60
61fun param_eq eqs0 =
62 let val nm = head eqs0
63     val eqs = map (snd o strip_forall) (strip_conj eqs0)
64     val fvrhs = subtract (free_varsl (map rhs eqs)) (free_varsl (map lhs eqs))
65     val pv = filter (C mem fvrhs) (!fv_ass)
66     val ty = type_of(fst(strip_comb(lhs(hd eqs))))
67     val old_var = mk_var(nm, ty)
68     val newvar = mk_var(nm, foldr (op -->) ty (map type_of pv))
69     val _ = if null pv then () else add_impl_param nm pv
70 in subst [old_var |-> list_mk_comb(newvar,pv)] eqs0
71 end;
72
73fun new_param_definition (x,tm) = new_definition(x, param_eq tm);
74
75
76
77(* Instantiating variables such that general constants can be replaced by
78 * the local constants.
79 * Could be improved (both in efficiency and soundness!).
80 *)
81
82fun is_defd sub v = exists (fn {redex,residue} => v=redex) sub;
83
84fun except_assoc x [] = raise ABS_ERR "except_assoc" ""
85  | except_assoc x ((s as {redex,residue})::l) =
86      if x=redex then (residue,l)
87      else
88        let val (v,nsub) = except_assoc x l in
89        (v,s::nsub)
90        end
91;
92
93fun majo NONE o2 = o2
94  | majo o1 NONE = o1
95  | majo (SOME x1) (SOME x2) =
96      if x1=x2 then (SOME x1)
97      else raise ABS_ERR "under_conj"
98          "vars were instantiated differently in conjuncts"
99;
100
101fun under_conj f th =
102  case (f (CONJUNCT1 th), f (CONJUNCT2 th)) of
103    ((NONE, _),(NONE, _)) => (NONE, th)
104  | ((o1,th1),(o2,th2)) => (majo o1 o2, CONJ th1 th2)
105;
106
107
108fun under_forall f th =
109  let val qvars = fst(strip_forall(concl th))
110      val thm = SPECL qvars th
111      val (ovars,rthm) = f thm in
112  case ovars of
113    SOME (ivars,ti) =>
114      let val (rsub,thm) =
115        foldr (fn (x,(sub,th)) =>
116          let val (v,nsub) = except_assoc (inst ti x) sub in
117          (nsub,SPEC v (GEN (inst ti x) th))
118          end
119          handle HOL_ERR _ => (sub,GEN (inst ti x) th)) (ivars,rthm) qvars
120      in (SOME (rsub,ti), thm)
121      end
122  | NONE => (NONE,th)
123  end
124;
125
126fun under_all f th =
127  if is_forall (concl th) then under_forall (under_all f) th
128  else if is_conj (concl th) then under_conj (under_all f) th
129  else f th
130;
131
132
133fun first_match env mfun [] = raise ABS_ERR "first_match" "no match"
134  | first_match env mfun (x::l) =
135      (let val (vi,ti) = mfun x in
136      if exists (fn {redex,residue} => mem redex env) vi then
137        raise ABS_ERR "" ""
138      else (vi,ti)
139      end
140      handle HOL_ERR _ => first_match env mfun l)
141;
142
143
144fun inst_csts inst env tm =
145  case dest_term tm of
146    LAMB(Bvar,Body) => inst_csts inst (Bvar::env) Body
147  | COMB(Rator,Rand) =>
148      (SOME (first_match env (match_term tm) inst)
149       handle HOL_ERR _ =>
150         (case inst_csts inst env Rand of
151           SOME i => SOME i
152         | NONE => inst_csts inst env Rator))
153  | _ => NONE
154;
155
156
157fun inst_thm inst thm =
158  case inst_csts inst [] (concl thm) of
159    NONE => (NONE,thm)
160  | SOME(vi,ti) => (SOME (vi,ti), INST_TYPE ti thm)
161;
162
163fun inst_all ctab thm =
164  let val (osub,thm) = under_all (inst_thm ctab) thm in
165  case osub of
166    SOME (sub,ti) =>
167      foldl (fn ({redex,residue},th) => SPEC residue (GEN redex th))
168        thm sub
169  | NONE => thm
170  end
171  handle HOL_ERR _ => thm;
172
173(* example:
174   inst_all [--`0+0`--,--`0-0`--]
175      (GEN_ALL(CONJ(GEN (--`y:num`--) (REFL(--` x+y = x-y `--)))
176                 (REFL(--`z`--))))
177    ;
178*)
179
180
181fun inst_hyp (h,thm) =
182  MATCH_MP thm h
183  handle HOL_ERR _ => thm
184;
185
186fun import_fun inst thm =
187  foldl inst_hyp thm inst
188;
189
190
191(*----------------*)
192
193type inst_infos =
194    { Vals : term list,
195      Inst : thm list,
196      Rule : thm -> thm,
197      Rename : string -> string option };
198
199type cinst_infos =
200    { Inst : thm list, Rule : thm -> thm, Csts : term list, Defs : thm list };
201
202
203fun compute_inst_infos ctab ({Rename,Inst,Rule,...}:inst_infos) =
204  let fun mk_def tm =
205        case Rename(#Name(dest_thy_const(fst(strip_comb tm)))) of
206          SOME name => SOME(name^"_def", mk_eq(mk_var(name,type_of tm),tm))
207        | NONE => NONE
208      val defs = List.mapPartial mk_def ctab
209      val thms = map (GSYM o new_param_definition) defs
210  in { Csts=ctab, Defs=thms, Inst=Inst, Rule=Rule }
211  end;
212
213fun inst_thm_fun { Inst=inst, Rule=f, Csts=ctab, Defs=thms } =
214    f o REWRITE_RULE thms o inst_all ctab o import_fun inst
215;
216
217
218(* --> abs_tools ? *)
219
220val pr_list_sep = PP.pr_list
221
222val S = PP.add_string;
223val NL = PP.add_newline;
224val N = PP.add_string o int_to_string;
225val SPC = PP.add_break(1,0)
226val B = PP.block PP.CONSISTENT 0
227
228
229val functor_header = [S "fun IMPORT P =", NL]
230;
231
232fun compute_cst_arg_map (fv,impargs) =
233  let val thcsts = map (#Name o dest_thy_const) (constants(current_theory()))
234      fun is_param_cst (x,iargs) =
235        mem x thcsts andalso all (C mem fv) iargs
236      val ptab = filter is_param_cst impargs
237      val pr_var = S o fst o dest_var
238      val sep = [S ",", NL, S "          "]
239  in
240     B [
241      S "  let open Parse abstraction",              NL,
242      S "      fun sing [x] = x | sing _ = raise Match", NL,
243      S "      val ",
244      B (pr_list_sep pr_var [S","] (!fv_ass)),
245      S " = sing (#Vals P)", NL,
246      S "      val ctab =", NL,
247      S "        [ ",
248      B (pr_list_sep (fn (x,iargs) =>
249                      B [
250                          S ("Term`"^x^" "),
251                          B (pr_list_sep (fn v => S ("^"^fst(dest_var v)))
252                                         [S " "] iargs),
253                          S "`"
254                        ])
255                  sep ptab),
256      S " ]",  NL,
257      S "      val inst_fun = inst_thm_fun (compute_inst_infos ctab P) in",
258      NL]
259  end
260;
261
262fun export_param_theory () = let
263  val _ = Theory.scrub()
264  val defs = rev (map fst (definitions"-"))
265  val thms = rev (map fst (theorems"-"))
266  fun struct_line thn = B [S thn, SPC, S "= inst_fun ", S thn]
267  fun sig_line thn = B [S thn, S " : thm"]
268  val sep = [S ",", NL, S "    "]
269  val adj = {
270    sig_ps =
271      SOME (fn _ => B[
272                     S "val IMPORT : abstraction.inst_infos ->", NL,
273                     S "  { ",
274                     B (pr_list_sep sig_line [S ",", SPC] (defs@thms)),
275                     S " }", NL
276                   ]),
277    struct_ps =
278      SOME (fn _ => B (
279                     functor_header @
280                     [compute_cst_arg_map (!fv_ass, !impl_param_cstr),
281                      S "  { ",
282                      B (pr_list_sep struct_line sep (defs@thms)),
283                      S " }", NL,
284                      S "  end", NL]))
285  }
286in
287  adjoin_to_theory adj;
288  export_theory()
289end;
290
291
292end;
293