1 (* Title: Tools/Compute_Oracle/linker.ML |
1 (* Title: Tools/Compute_Oracle/linker.ML |
2 ID: $Id$ |
|
3 Author: Steven Obua |
2 Author: Steven Obua |
4 |
3 |
5 Linker.ML solves the problem that the computing oracle does not |
4 Linker.ML solves the problem that the computing oracle does not |
6 instantiate polymorphic rules. By going through the PCompute interface, |
5 instantiate polymorphic rules. By going through the PCompute interface, |
7 all possible instantiations are resolved by compiling new programs, if |
6 all possible instantiations are resolved by compiling new programs, if |
49 fun constant_of (Const (name, ty)) = Constant (false, name, ty) |
48 fun constant_of (Const (name, ty)) = Constant (false, name, ty) |
50 | constant_of (Free (name, ty)) = Constant (true, name, ty) |
49 | constant_of (Free (name, ty)) = Constant (true, name, ty) |
51 | constant_of _ = raise Link "constant_of" |
50 | constant_of _ = raise Link "constant_of" |
52 |
51 |
53 fun bool_ord (x,y) = if x then (if y then EQUAL else GREATER) else (if y then LESS else EQUAL) |
52 fun bool_ord (x,y) = if x then (if y then EQUAL else GREATER) else (if y then LESS else EQUAL) |
54 fun constant_ord (Constant (x1,x2,x3), Constant (y1,y2,y3)) = (prod_ord (prod_ord bool_ord fast_string_ord) Term.typ_ord) (((x1,x2),x3), ((y1,y2),y3)) |
53 fun constant_ord (Constant (x1,x2,x3), Constant (y1,y2,y3)) = (prod_ord (prod_ord bool_ord fast_string_ord) TermOrd.typ_ord) (((x1,x2),x3), ((y1,y2),y3)) |
55 fun constant_modty_ord (Constant (x1,x2,_), Constant (y1,y2,_)) = (prod_ord bool_ord fast_string_ord) ((x1,x2), (y1,y2)) |
54 fun constant_modty_ord (Constant (x1,x2,_), Constant (y1,y2,_)) = (prod_ord bool_ord fast_string_ord) ((x1,x2), (y1,y2)) |
56 |
55 |
57 |
56 |
58 structure Consttab = TableFun(type key = constant val ord = constant_ord); |
57 structure Consttab = TableFun(type key = constant val ord = constant_ord); |
59 structure ConsttabModTy = TableFun(type key = constant val ord = constant_modty_ord); |
58 structure ConsttabModTy = TableFun(type key = constant val ord = constant_modty_ord); |
69 NONE => Vartab.update (v, t) tab |
68 NONE => Vartab.update (v, t) tab |
70 | SOME t' => if t = t' then tab else raise Type.TYPE_MATCH)) A B) |
69 | SOME t' => if t = t' then tab else raise Type.TYPE_MATCH)) A B) |
71 handle Type.TYPE_MATCH => NONE |
70 handle Type.TYPE_MATCH => NONE |
72 |
71 |
73 fun subst_ord (A:Type.tyenv, B:Type.tyenv) = |
72 fun subst_ord (A:Type.tyenv, B:Type.tyenv) = |
74 (list_ord (prod_ord Term.fast_indexname_ord (prod_ord Term.sort_ord Term.typ_ord))) (Vartab.dest A, Vartab.dest B) |
73 (list_ord (prod_ord TermOrd.fast_indexname_ord (prod_ord TermOrd.sort_ord TermOrd.typ_ord))) (Vartab.dest A, Vartab.dest B) |
75 |
74 |
76 structure Substtab = TableFun(type key = Type.tyenv val ord = subst_ord); |
75 structure Substtab = TableFun(type key = Type.tyenv val ord = subst_ord); |
77 |
76 |
78 fun substtab_union c = Substtab.fold Substtab.update c |
77 fun substtab_union c = Substtab.fold Substtab.update c |
79 fun substtab_unions [] = Substtab.empty |
78 fun substtab_unions [] = Substtab.empty |
377 val {hyps, prop, shyps, ...} = Thm.rep_thm th |
376 val {hyps, prop, shyps, ...} = Thm.rep_thm th |
378 in |
377 in |
379 ComputeThm (hyps, shyps, prop) |
378 ComputeThm (hyps, shyps, prop) |
380 end |
379 end |
381 |
380 |
382 val cthm_ord' = prod_ord (prod_ord (list_ord Term.term_ord) (list_ord Term.sort_ord)) Term.term_ord |
381 val cthm_ord' = prod_ord (prod_ord (list_ord TermOrd.term_ord) (list_ord TermOrd.sort_ord)) TermOrd.term_ord |
383 |
382 |
384 fun cthm_ord (ComputeThm (h1, sh1, p1), ComputeThm (h2, sh2, p2)) = cthm_ord' (((h1,sh1), p1), ((h2, sh2), p2)) |
383 fun cthm_ord (ComputeThm (h1, sh1, p1), ComputeThm (h2, sh2, p2)) = cthm_ord' (((h1,sh1), p1), ((h2, sh2), p2)) |
385 |
384 |
386 structure CThmtab = TableFun (type key = cthm val ord = cthm_ord) |
385 structure CThmtab = TableFun (type key = cthm val ord = cthm_ord) |
387 |
386 |