31 val make_fixed_const : string -> string |
31 val make_fixed_const : string -> string |
32 val make_fixed_type_const : string -> string |
32 val make_fixed_type_const : string -> string |
33 val make_type_class : string -> string |
33 val make_type_class : string -> string |
34 datatype kind = Axiom | Conjecture |
34 datatype kind = Axiom | Conjecture |
35 type axiom_name = string |
35 type axiom_name = string |
36 datatype typ_var = FOLTVar of indexname | FOLTFree of string |
|
37 datatype fol_type = |
36 datatype fol_type = |
38 AtomV of string |
37 AtomV of string |
39 | AtomF of string |
38 | AtomF of string |
40 | Comp of string * fol_type list |
39 | Comp of string * fol_type list |
41 val string_of_fol_type : fol_type -> string |
40 val string_of_fol_type : fol_type -> string |
42 datatype type_literal = LTVar of string * string | LTFree of string * string |
41 datatype type_literal = LTVar of string * string | LTFree of string * string |
43 val mk_typ_var_sort: typ -> typ_var * sort |
|
44 exception CLAUSE of string * term |
42 exception CLAUSE of string * term |
45 val isMeta : string -> bool |
43 val isMeta : string -> bool |
46 val add_typs : (typ_var * string list) list -> type_literal list |
44 val add_typs : typ list -> type_literal list |
47 val get_tvar_strs: (typ_var * sort) list -> string list |
45 val get_tvar_strs: typ list -> string list |
48 datatype arLit = |
46 datatype arLit = |
49 TConsLit of class * string * string list |
47 TConsLit of class * string * string list |
50 | TVarLit of class * string |
48 | TVarLit of class * string |
51 datatype arityClause = ArityClause of |
49 datatype arityClause = ArityClause of |
52 {axiom_name: axiom_name, conclLit: arLit, premLits: arLit list} |
50 {axiom_name: axiom_name, conclLit: arLit, premLits: arLit list} |
53 datatype classrelClause = ClassrelClause of |
51 datatype classrelClause = ClassrelClause of |
54 {axiom_name: axiom_name, subclass: class, superclass: class} |
52 {axiom_name: axiom_name, subclass: class, superclass: class} |
55 val make_classrel_clauses: theory -> class list -> class list -> classrelClause list |
53 val make_classrel_clauses: theory -> class list -> class list -> classrelClause list |
56 val make_arity_clauses: theory -> string list -> class list -> class list * arityClause list |
54 val make_arity_clauses: theory -> string list -> class list -> class list * arityClause list |
57 val add_type_sort_preds: (typ_var * string list) * int Symtab.table -> int Symtab.table |
55 val add_type_sort_preds: typ * int Symtab.table -> int Symtab.table |
58 val add_classrelClause_preds : classrelClause * int Symtab.table -> int Symtab.table |
56 val add_classrelClause_preds : classrelClause * int Symtab.table -> int Symtab.table |
59 val class_of_arityLit: arLit -> class |
57 val class_of_arityLit: arLit -> class |
60 val add_arityClause_preds: arityClause * int Symtab.table -> int Symtab.table |
58 val add_arityClause_preds: arityClause * int Symtab.table -> int Symtab.table |
61 val add_foltype_funcs: fol_type * int Symtab.table -> int Symtab.table |
59 val add_foltype_funcs: fol_type * int Symtab.table -> int Symtab.table |
62 val add_arityClause_funcs: arityClause * int Symtab.table -> int Symtab.table |
60 val add_arityClause_funcs: arityClause * int Symtab.table -> int Symtab.table |
247 tcon ^ (paren_pack (map string_of_fol_type tps)); |
243 tcon ^ (paren_pack (map string_of_fol_type tps)); |
248 |
244 |
249 (*First string is the type class; the second is a TVar or TFfree*) |
245 (*First string is the type class; the second is a TVar or TFfree*) |
250 datatype type_literal = LTVar of string * string | LTFree of string * string; |
246 datatype type_literal = LTVar of string * string | LTFree of string * string; |
251 |
247 |
252 fun mk_typ_var_sort (TFree(a,s)) = (FOLTFree a,s) |
|
253 | mk_typ_var_sort (TVar(v,s)) = (FOLTVar v,s); |
|
254 |
|
255 |
|
256 exception CLAUSE of string * term; |
248 exception CLAUSE of string * term; |
257 |
249 |
|
250 fun atomic_type (TFree (a,_)) = AtomF(make_fixed_type_var a) |
|
251 | atomic_type (TVar (v,_)) = AtomV(make_schematic_type_var v); |
258 |
252 |
259 (*Flatten a type to a fol_type while accumulating sort constraints on the TFrees and |
253 (*Flatten a type to a fol_type while accumulating sort constraints on the TFrees and |
260 TVars it contains.*) |
254 TVars it contains.*) |
261 fun type_of (Type (a, Ts)) = |
255 fun type_of (Type (a, Ts)) = |
262 let val (folTyps, ts) = types_of Ts |
256 let val (folTyps, ts) = types_of Ts |
263 val t = make_fixed_type_const a |
257 val t = make_fixed_type_const a |
264 in (Comp(t,folTyps), ts) end |
258 in (Comp(t,folTyps), ts) end |
265 | type_of (TFree (a,s)) = (AtomF(make_fixed_type_var a), [(FOLTFree a, s)]) |
259 | type_of T = (atomic_type T, [T]) |
266 | type_of (TVar (v, s)) = (AtomV(make_schematic_type_var v), [(FOLTVar v, s)]) |
|
267 and types_of Ts = |
260 and types_of Ts = |
268 let val (folTyps,ts) = ListPair.unzip (map type_of Ts) |
261 let val (folTyps,ts) = ListPair.unzip (map type_of Ts) |
269 in (folTyps, union_all ts) end; |
262 in (folTyps, union_all ts) end; |
270 |
263 |
271 |
264 |
272 (* Any variables created via the METAHYPS tactical should be treated as |
265 (* Any variables created via the METAHYPS tactical should be treated as |
273 universal vars, although it is represented as "Free(...)" by Isabelle *) |
266 universal vars, although it is represented as "Free(...)" by Isabelle *) |
274 val isMeta = String.isPrefix "METAHYP1_" |
267 val isMeta = String.isPrefix "METAHYP1_" |
275 |
268 |
276 (*Make literals for sorted type variables*) |
269 (*Make literals for sorted type variables*) |
277 fun sorts_on_typs (_, []) = [] |
270 fun sorts_on_typs_aux (_, []) = [] |
278 | sorts_on_typs (v, s::ss) = |
271 | sorts_on_typs_aux ((x,i), s::ss) = |
279 let val sorts = sorts_on_typs (v, ss) |
272 let val sorts = sorts_on_typs_aux ((x,i), ss) |
280 in |
273 in |
281 if s = "HOL.type" then sorts |
274 if s = "HOL.type" then sorts |
282 else case v of |
275 else if i = ~1 then LTFree(make_type_class s, make_fixed_type_var x) :: sorts |
283 FOLTVar indx => LTVar(make_type_class s, make_schematic_type_var indx) :: sorts |
276 else LTVar(make_type_class s, make_schematic_type_var (x,i)) :: sorts |
284 | FOLTFree x => LTFree(make_type_class s, make_fixed_type_var x) :: sorts |
|
285 end; |
277 end; |
|
278 |
|
279 fun sorts_on_typs (TFree (a,s)) = sorts_on_typs_aux ((a,~1),s) |
|
280 | sorts_on_typs (TVar (v,s)) = sorts_on_typs_aux (v,s); |
286 |
281 |
287 fun pred_of_sort (LTVar (s,ty)) = (s,1) |
282 fun pred_of_sort (LTVar (s,ty)) = (s,1) |
288 | pred_of_sort (LTFree (s,ty)) = (s,1) |
283 | pred_of_sort (LTFree (s,ty)) = (s,1) |
289 |
284 |
290 (*Given a list of sorted type variables, return a list of type literals.*) |
285 (*Given a list of sorted type variables, return a list of type literals.*) |
291 fun add_typs tss = foldl (op union) [] (map sorts_on_typs tss); |
286 fun add_typs Ts = foldl (op union) [] (map sorts_on_typs Ts); |
292 |
287 |
293 (** make axiom and conjecture clauses. **) |
288 (** make axiom and conjecture clauses. **) |
294 |
289 |
295 fun get_tvar_strs [] = [] |
290 fun get_tvar_strs [] = [] |
296 | get_tvar_strs ((FOLTVar indx,s)::tss) = |
291 | get_tvar_strs ((TVar (indx,s))::Ts) = |
297 insert (op =) (make_schematic_type_var indx) (get_tvar_strs tss) |
292 insert (op =) (make_schematic_type_var indx) (get_tvar_strs Ts) |
298 | get_tvar_strs((FOLTFree x,s)::tss) = get_tvar_strs tss |
293 | get_tvar_strs((TFree _)::Ts) = get_tvar_strs Ts |
299 |
294 |
300 |
295 |
301 |
296 |
302 (**** Isabelle arities ****) |
297 (**** Isabelle arities ****) |
303 |
298 |
403 (*FIXME: multiple-arity checking doesn't work, as update_new is the wrong |
398 (*FIXME: multiple-arity checking doesn't work, as update_new is the wrong |
404 function (it flags repeated declarations of a function, even with the same arity)*) |
399 function (it flags repeated declarations of a function, even with the same arity)*) |
405 |
400 |
406 fun update_many (tab, keypairs) = foldl (uncurry Symtab.update) tab keypairs; |
401 fun update_many (tab, keypairs) = foldl (uncurry Symtab.update) tab keypairs; |
407 |
402 |
408 fun add_type_sort_preds ((FOLTVar indx,s), preds) = |
403 fun add_type_sort_preds (T, preds) = |
409 update_many (preds, map pred_of_sort (sorts_on_typs (FOLTVar indx, s))) |
404 update_many (preds, map pred_of_sort (sorts_on_typs T)); |
410 | add_type_sort_preds ((FOLTFree x,s), preds) = |
|
411 update_many (preds, map pred_of_sort (sorts_on_typs (FOLTFree x, s))); |
|
412 |
405 |
413 fun add_classrelClause_preds (ClassrelClause {subclass,superclass,...}, preds) = |
406 fun add_classrelClause_preds (ClassrelClause {subclass,superclass,...}, preds) = |
414 Symtab.update (subclass,1) (Symtab.update (superclass,1) preds); |
407 Symtab.update (subclass,1) (Symtab.update (superclass,1) preds); |
415 |
408 |
416 fun class_of_arityLit (TConsLit (tclass, _, _)) = tclass |
409 fun class_of_arityLit (TConsLit (tclass, _, _)) = tclass |
427 | add_foltype_funcs (AtomF a, funcs) = Symtab.update (a,0) funcs |
420 | add_foltype_funcs (AtomF a, funcs) = Symtab.update (a,0) funcs |
428 | add_foltype_funcs (Comp(a,tys), funcs) = |
421 | add_foltype_funcs (Comp(a,tys), funcs) = |
429 foldl add_foltype_funcs (Symtab.update (a, length tys) funcs) tys; |
422 foldl add_foltype_funcs (Symtab.update (a, length tys) funcs) tys; |
430 |
423 |
431 (*TFrees are recorded as constants*) |
424 (*TFrees are recorded as constants*) |
432 fun add_type_sort_funcs ((FOLTVar _, _), funcs) = funcs |
425 fun add_type_sort_funcs (TVar _, funcs) = funcs |
433 | add_type_sort_funcs ((FOLTFree a, _), funcs) = |
426 | add_type_sort_funcs (TFree (a, _), funcs) = |
434 Symtab.update (make_fixed_type_var a, 0) funcs |
427 Symtab.update (make_fixed_type_var a, 0) funcs |
435 |
428 |
436 fun add_arityClause_funcs (ArityClause {conclLit,...}, funcs) = |
429 fun add_arityClause_funcs (ArityClause {conclLit,...}, funcs) = |
437 let val TConsLit (_, tcons, tvars) = conclLit |
430 let val TConsLit (_, tcons, tvars) = conclLit |
438 in Symtab.update (tcons, length tvars) funcs end; |
431 in Symtab.update (tcons, length tvars) funcs end; |