45 end |
45 end |
46 |
46 |
47 structure SMT_Builtin: SMT_BUILTIN = |
47 structure SMT_Builtin: SMT_BUILTIN = |
48 struct |
48 struct |
49 |
49 |
50 structure U = SMT_Utils |
|
51 structure C = SMT_Config |
|
52 |
|
53 |
50 |
54 (* built-in tables *) |
51 (* built-in tables *) |
55 |
52 |
56 datatype ('a, 'b) kind = Ext of 'a | Int of 'b |
53 datatype ('a, 'b) kind = Ext of 'a | Int of 'b |
57 |
54 |
58 type ('a, 'b) ttab = ((typ * ('a, 'b) kind) Ord_List.T) U.dict |
55 type ('a, 'b) ttab = ((typ * ('a, 'b) kind) Ord_List.T) SMT_Utils.dict |
59 |
56 |
60 fun typ_ord ((T, _), (U, _)) = |
57 fun typ_ord ((T, _), (U, _)) = |
61 let |
58 let |
62 fun tord (TVar _, Type _) = GREATER |
59 fun tord (TVar _, Type _) = GREATER |
63 | tord (Type _, TVar _) = LESS |
60 | tord (Type _, TVar _) = LESS |
66 else Term_Ord.typ_ord (T, U) |
63 else Term_Ord.typ_ord (T, U) |
67 | tord TU = Term_Ord.typ_ord TU |
64 | tord TU = Term_Ord.typ_ord TU |
68 in tord (T, U) end |
65 in tord (T, U) end |
69 |
66 |
70 fun insert_ttab cs T f = |
67 fun insert_ttab cs T f = |
71 U.dict_map_default (cs, []) |
68 SMT_Utils.dict_map_default (cs, []) |
72 (Ord_List.insert typ_ord (perhaps (try Logic.varifyT_global) T, f)) |
69 (Ord_List.insert typ_ord (perhaps (try Logic.varifyT_global) T, f)) |
73 |
70 |
74 fun merge_ttab ttabp = |
71 fun merge_ttab ttabp = |
75 U.dict_merge (uncurry (Ord_List.union typ_ord) o swap) ttabp |
72 SMT_Utils.dict_merge (uncurry (Ord_List.union typ_ord) o swap) ttabp |
76 |
73 |
77 fun lookup_ttab ctxt ttab T = |
74 fun lookup_ttab ctxt ttab T = |
78 let fun match (U, _) = Sign.typ_instance (ProofContext.theory_of ctxt) (T, U) |
75 let fun match (U, _) = Sign.typ_instance (ProofContext.theory_of ctxt) (T, U) |
79 in |
76 in |
80 get_first (find_first match) (U.dict_lookup ttab (C.solver_class_of ctxt)) |
77 get_first (find_first match) |
|
78 (SMT_Utils.dict_lookup ttab (SMT_Config.solver_class_of ctxt)) |
81 end |
79 end |
82 |
80 |
83 type ('a, 'b) btab = ('a, 'b) ttab Symtab.table |
81 type ('a, 'b) btab = ('a, 'b) ttab Symtab.table |
84 |
82 |
85 fun insert_btab cs n T f = |
83 fun insert_btab cs n T f = |
106 |
104 |
107 fun add_builtin_typ cs (T, f, g) = |
105 fun add_builtin_typ cs (T, f, g) = |
108 Builtin_Types.map (insert_ttab cs T (Int (f, g))) |
106 Builtin_Types.map (insert_ttab cs T (Int (f, g))) |
109 |
107 |
110 fun add_builtin_typ_ext (T, f) = |
108 fun add_builtin_typ_ext (T, f) = |
111 Builtin_Types.map (insert_ttab U.basicC T (Ext f)) |
109 Builtin_Types.map (insert_ttab SMT_Utils.basicC T (Ext f)) |
112 |
110 |
113 fun lookup_builtin_typ ctxt = |
111 fun lookup_builtin_typ ctxt = |
114 lookup_ttab ctxt (Builtin_Types.get (Context.Proof ctxt)) |
112 lookup_ttab ctxt (Builtin_Types.get (Context.Proof ctxt)) |
115 |
113 |
116 fun dest_builtin_typ ctxt T = |
114 fun dest_builtin_typ ctxt T = |
166 fun app U ts = Term.list_comb (Const (m, U), ts) |
164 fun app U ts = Term.list_comb (Const (m, U), ts) |
167 fun bfun _ U ts = SOME (n, length (Term.binder_types T), ts, app U) |
165 fun bfun _ U ts = SOME (n, length (Term.binder_types T), ts, app U) |
168 in add_builtin_fun cs (c, bfun) end |
166 in add_builtin_fun cs (c, bfun) end |
169 |
167 |
170 fun add_builtin_fun_ext ((n, T), f) = |
168 fun add_builtin_fun_ext ((n, T), f) = |
171 Builtin_Funcs.map (insert_btab U.basicC n T (Ext f)) |
169 Builtin_Funcs.map (insert_btab SMT_Utils.basicC n T (Ext f)) |
172 |
170 |
173 fun add_builtin_fun_ext' c = |
171 fun add_builtin_fun_ext' c = |
174 add_builtin_fun_ext (c, fn _ => fn _ => fn _ => true) |
172 add_builtin_fun_ext (c, fn _ => fn _ => fn _ => true) |
175 |
173 |
176 fun add_builtin_fun_ext'' n context = |
174 fun add_builtin_fun_ext'' n context = |