# HG changeset patch # User paulson # Date 1134656797 -3600 # Node ID 2d3165a0fb40e35cc935e58d07691b0d1277a74a # Parent 73bb08d2823c39edbafaf9bcac422ff610bcdf77 No axiom, arity or classrel clauses contain HOL.type. Negative occurrences are deleted; any positive occurrence of HOL.type kills the entire clause. diff -r 73bb08d2823c -r 2d3165a0fb40 src/HOL/Tools/res_clause.ML --- a/src/HOL/Tools/res_clause.ML Thu Dec 15 11:53:38 2005 +0100 +++ b/src/HOL/Tools/res_clause.ML Thu Dec 15 15:26:37 2005 +0100 @@ -1,5 +1,4 @@ (* Author: Jia Meng, Cambridge University Computer Laboratory - ID: $Id$ Copyright 2004 University of Cambridge @@ -117,9 +116,9 @@ ("List.op @", "append")]; val type_const_trans_table = - Symtab.make [("*", "t_prod"), - ("+", "t_sum"), - ("~=>", "t_map")]; + Symtab.make [("*", "prod"), + ("+", "sum"), + ("~=>", "map")]; (*Escaping of special characters. Alphanumeric characters are left unchanged. @@ -166,15 +165,20 @@ tvar_prefix ^ (ascii_of_indexname (trim_type_var x,i)); fun make_fixed_type_var x = tfree_prefix ^ (ascii_of (trim_type_var x)); -fun make_fixed_const c = +fun lookup_const c = case Symtab.lookup const_trans_table c of SOME c' => c' - | NONE => const_prefix ^ ascii_of c; + | NONE => ascii_of c; -fun make_fixed_type_const c = +fun lookup_type_const c = case Symtab.lookup type_const_trans_table c of SOME c' => c' - | NONE => tconst_prefix ^ ascii_of c; + | NONE => ascii_of c; + +fun make_fixed_const "op =" = "equal" (*MUST BE "equal" because it's built-in to ATPs*) + | make_fixed_const c = const_prefix ^ lookup_const c; + +fun make_fixed_type_const c = tconst_prefix ^ lookup_type_const c; fun make_type_class clas = class_prefix ^ ascii_of clas; @@ -645,7 +649,7 @@ (*Make literals for sorted type variables*) fun sorts_on_typs (_, []) = ([]) | sorts_on_typs (v, "HOL.type" :: s) = - sorts_on_typs (v,s) (*Ignore sort "type"*) + sorts_on_typs (v,s) (*IGNORE sort "type"*) | sorts_on_typs ((FOLTVar indx), (s::ss)) = LTVar((make_type_class s) ^ "(" ^ (make_schematic_type_var indx) ^ ")") :: @@ -664,7 +668,6 @@ - (*Given a list of sorted type variables, return two separate lists. The first is for TVars, the second for TFrees.*) fun add_typs_aux [] preds = ([],[], preds) @@ -784,17 +787,15 @@ fun get_TVars 0 = [] | get_TVars n = ("T_" ^ (Int.toString n)) :: get_TVars (n-1); - - -fun pack_sort(_,[]) = raise ARCLAUSE("Empty Sort Found") - | pack_sort(tvar, [cls]) = [(make_type_class cls, tvar)] - | pack_sort(tvar, cls::srt) = (make_type_class cls,tvar) :: (pack_sort(tvar, srt)); - +fun pack_sort(_,[]) = [] + | pack_sort(tvar, "HOL.type"::srt) = pack_sort(tvar, srt) (*IGNORE sort "type"*) + | pack_sort(tvar, cls::srt) = (make_type_class cls, tvar) :: pack_sort(tvar, srt); fun make_TVarLit (b,(cls,str)) = TVarLit(b,(cls,str)); fun make_TConsLit (b,(cls,tcons,tvars)) = TConsLit(b,(make_type_class cls,make_fixed_type_const tcons,tvars)); -fun make_axiom_arity_clause (tcons,n,(res,args)) = +(*Arity of type constructor tcon :: (arg1,...,argN)res*) +fun make_axiom_arity_clause (tcons, n, (res,args)) = let val nargs = length args val tvars = get_TVars nargs val tvars_srts = ListPair.zip (tvars,args) @@ -802,8 +803,8 @@ val false_tvars_srts' = map (pair false) tvars_srts' in ArityClause {clause_id = n, kind = Axiom, - axiom_name = tcons, - conclLit = make_TConsLit(true,(res,tcons,tvars)), + axiom_name = lookup_type_const tcons, + conclLit = make_TConsLit(true, (res,tcons,tvars)), premLits = map make_TVarLit false_tvars_srts'} end; @@ -817,32 +818,30 @@ (**** Isabelle class relations ****) - datatype classrelClause = ClassrelClause of {clause_id: clause_id, subclass: class, - superclass: class option}; - + superclass: class}; fun make_axiom_classrelClause n subclass superclass = ClassrelClause {clause_id = n, subclass = subclass, superclass = superclass}; - fun classrelClauses_of_aux n sub [] = [] + | classrelClauses_of_aux n sub ("HOL.type"::sups) = (*Should be ignored*) + classrelClauses_of_aux n sub sups | classrelClauses_of_aux n sub (sup::sups) = - make_axiom_classrelClause n sub (SOME sup) :: classrelClauses_of_aux (n+1) sub sups; + ClassrelClause {clause_id = n, subclass = sub, superclass = sup} + :: classrelClauses_of_aux (n+1) sub sups; - -fun classrelClauses_of (sub,sups) = - case sups of [] => [make_axiom_classrelClause 0 sub NONE] - | _ => classrelClauses_of_aux 0 sub sups; +fun classrelClauses_of (sub,sups) = classrelClauses_of_aux 0 sub sups; (***** Isabelle arities *****) - fun arity_clause _ (tcons, []) = [] + | arity_clause n (tcons, ("HOL.type",_)::ars) = (*Should be ignored*) + arity_clause n (tcons,ars) | arity_clause n (tcons, ar::ars) = make_axiom_arity_clause (tcons,n,ar) :: arity_clause (n+1) (tcons,ars); @@ -1249,16 +1248,13 @@ fun tptp_classrelLits sub sup = let val tvar = "(T)" in - case sup of NONE => "[++" ^ sub ^ tvar ^ "]" - | (SOME supcls) => "[--" ^ sub ^ tvar ^ ",++" ^ supcls ^ tvar ^ "]" + "[--" ^ sub ^ tvar ^ ",++" ^ sup ^ tvar ^ "]" end; - fun tptp_classrelClause (ClassrelClause {clause_id,subclass,superclass,...}) = let val relcls_id = clrelclause_prefix ^ ascii_of subclass ^ "_" ^ Int.toString clause_id - val lits = tptp_classrelLits (make_type_class subclass) - (Option.map make_type_class superclass) + val lits = tptp_classrelLits (make_type_class subclass) (make_type_class superclass) in "input_clause(" ^ relcls_id ^ ",axiom," ^ lits ^ ")." end;