No axiom, arity or classrel clauses contain HOL.type. Negative occurrences are
authorpaulson
Thu Dec 15 15:26:37 2005 +0100 (2005-12-15)
changeset 184112d3165a0fb40
parent 18410 73bb08d2823c
child 18412 9f6b3e1da352
No axiom, arity or classrel clauses contain HOL.type. Negative occurrences are
deleted; any positive occurrence of HOL.type kills the entire clause.
src/HOL/Tools/res_clause.ML
     1.1 --- a/src/HOL/Tools/res_clause.ML	Thu Dec 15 11:53:38 2005 +0100
     1.2 +++ b/src/HOL/Tools/res_clause.ML	Thu Dec 15 15:26:37 2005 +0100
     1.3 @@ -1,5 +1,4 @@
     1.4  (*  Author: Jia Meng, Cambridge University Computer Laboratory
     1.5 -
     1.6      ID: $Id$
     1.7      Copyright 2004 University of Cambridge
     1.8  
     1.9 @@ -117,9 +116,9 @@
    1.10  		   ("List.op @", "append")];
    1.11  
    1.12  val type_const_trans_table =
    1.13 -      Symtab.make [("*", "t_prod"),
    1.14 -	  	   ("+", "t_sum"),
    1.15 -		   ("~=>", "t_map")];
    1.16 +      Symtab.make [("*", "prod"),
    1.17 +	  	   ("+", "sum"),
    1.18 +		   ("~=>", "map")];
    1.19  
    1.20  (*Escaping of special characters.
    1.21    Alphanumeric characters are left unchanged.
    1.22 @@ -166,15 +165,20 @@
    1.23        tvar_prefix ^ (ascii_of_indexname (trim_type_var x,i));
    1.24  fun make_fixed_type_var x = tfree_prefix ^ (ascii_of (trim_type_var x));
    1.25  
    1.26 -fun make_fixed_const c =
    1.27 +fun lookup_const c =
    1.28      case Symtab.lookup const_trans_table c of
    1.29          SOME c' => c'
    1.30 -      | NONE =>  const_prefix ^ ascii_of c;
    1.31 +      | NONE => ascii_of c;
    1.32  
    1.33 -fun make_fixed_type_const c = 
    1.34 +fun lookup_type_const c = 
    1.35      case Symtab.lookup type_const_trans_table c of
    1.36          SOME c' => c'
    1.37 -      | NONE =>  tconst_prefix ^ ascii_of c;
    1.38 +      | NONE => ascii_of c;
    1.39 +
    1.40 +fun make_fixed_const "op =" = "equal"   (*MUST BE "equal" because it's built-in to ATPs*)
    1.41 +  | make_fixed_const c      = const_prefix ^ lookup_const c;
    1.42 +
    1.43 +fun make_fixed_type_const c = tconst_prefix ^ lookup_type_const c;
    1.44  
    1.45  fun make_type_class clas = class_prefix ^ ascii_of clas;
    1.46  
    1.47 @@ -645,7 +649,7 @@
    1.48  (*Make literals for sorted type variables*) 
    1.49  fun sorts_on_typs (_, [])   = ([]) 
    1.50    | sorts_on_typs (v, "HOL.type" :: s) =
    1.51 -      sorts_on_typs (v,s)   (*Ignore sort "type"*)
    1.52 +      sorts_on_typs (v,s)                (*IGNORE sort "type"*)
    1.53    | sorts_on_typs ((FOLTVar indx), (s::ss)) =
    1.54        LTVar((make_type_class s) ^ 
    1.55          "(" ^ (make_schematic_type_var indx) ^ ")") :: 
    1.56 @@ -664,7 +668,6 @@
    1.57  
    1.58  
    1.59  
    1.60 -
    1.61  (*Given a list of sorted type variables, return two separate lists.
    1.62    The first is for TVars, the second for TFrees.*)
    1.63  fun add_typs_aux [] preds  = ([],[], preds)
    1.64 @@ -784,17 +787,15 @@
    1.65  fun get_TVars 0 = []
    1.66    | get_TVars n = ("T_" ^ (Int.toString n)) :: get_TVars (n-1);
    1.67  
    1.68 -
    1.69 -
    1.70 -fun pack_sort(_,[])  = raise ARCLAUSE("Empty Sort Found") 
    1.71 -  | pack_sort(tvar, [cls]) = [(make_type_class cls, tvar)] 
    1.72 -  | pack_sort(tvar, cls::srt) =  (make_type_class cls,tvar) :: (pack_sort(tvar, srt));
    1.73 -    
    1.74 +fun pack_sort(_,[])  = []
    1.75 +  | pack_sort(tvar, "HOL.type"::srt) = pack_sort(tvar, srt)   (*IGNORE sort "type"*)
    1.76 +  | pack_sort(tvar, cls::srt) =  (make_type_class cls, tvar) :: pack_sort(tvar, srt);
    1.77      
    1.78  fun make_TVarLit (b,(cls,str)) = TVarLit(b,(cls,str));
    1.79  fun make_TConsLit (b,(cls,tcons,tvars)) = TConsLit(b,(make_type_class cls,make_fixed_type_const tcons,tvars));
    1.80  
    1.81 -fun make_axiom_arity_clause (tcons,n,(res,args)) =
    1.82 +(*Arity of type constructor tcon :: (arg1,...,argN)res*)
    1.83 +fun make_axiom_arity_clause (tcons, n, (res,args)) =
    1.84     let val nargs = length args
    1.85         val tvars = get_TVars nargs
    1.86         val tvars_srts = ListPair.zip (tvars,args)
    1.87 @@ -802,8 +803,8 @@
    1.88         val false_tvars_srts' = map (pair false) tvars_srts'
    1.89     in
    1.90        ArityClause {clause_id = n, kind = Axiom, 
    1.91 -                   axiom_name = tcons,
    1.92 -                   conclLit = make_TConsLit(true,(res,tcons,tvars)), 
    1.93 +                   axiom_name = lookup_type_const tcons,
    1.94 +                   conclLit = make_TConsLit(true, (res,tcons,tvars)), 
    1.95                     premLits = map make_TVarLit false_tvars_srts'}
    1.96     end;
    1.97      
    1.98 @@ -817,32 +818,30 @@
    1.99  
   1.100  (**** Isabelle class relations ****)
   1.101  
   1.102 -
   1.103  datatype classrelClause = 
   1.104  	 ClassrelClause of {clause_id: clause_id,
   1.105  			    subclass: class,
   1.106 -			    superclass: class option};
   1.107 -
   1.108 +			    superclass: class};
   1.109  
   1.110  fun make_axiom_classrelClause n subclass superclass =
   1.111    ClassrelClause {clause_id = n,
   1.112                    subclass = subclass, superclass = superclass};
   1.113  
   1.114 -
   1.115  fun classrelClauses_of_aux n sub [] = []
   1.116 +  | classrelClauses_of_aux n sub ("HOL.type"::sups) = (*Should be ignored*)
   1.117 +      classrelClauses_of_aux n sub sups
   1.118    | classrelClauses_of_aux n sub (sup::sups) =
   1.119 -      make_axiom_classrelClause n sub (SOME sup) :: classrelClauses_of_aux (n+1) sub sups;
   1.120 +      ClassrelClause {clause_id = n, subclass = sub, superclass = sup} 
   1.121 +      :: classrelClauses_of_aux (n+1) sub sups;
   1.122  
   1.123 -
   1.124 -fun classrelClauses_of (sub,sups) = 
   1.125 -    case sups of [] => [make_axiom_classrelClause 0 sub NONE]
   1.126 -	       | _ => classrelClauses_of_aux 0 sub sups;
   1.127 +fun classrelClauses_of (sub,sups) = classrelClauses_of_aux 0 sub sups;
   1.128  
   1.129  
   1.130  (***** Isabelle arities *****)
   1.131  
   1.132 -
   1.133  fun arity_clause _ (tcons, []) = []
   1.134 +  | arity_clause n (tcons, ("HOL.type",_)::ars) =  (*Should be ignored*)
   1.135 +      arity_clause n (tcons,ars)
   1.136    | arity_clause n (tcons, ar::ars) =
   1.137        make_axiom_arity_clause (tcons,n,ar) :: 
   1.138        arity_clause (n+1) (tcons,ars);
   1.139 @@ -1249,16 +1248,13 @@
   1.140  fun tptp_classrelLits sub sup = 
   1.141      let val tvar = "(T)"
   1.142      in 
   1.143 -	case sup of NONE => "[++" ^ sub ^ tvar ^ "]"
   1.144 -		  | (SOME supcls) =>  "[--" ^ sub ^ tvar ^ ",++" ^ supcls ^ tvar ^ "]"
   1.145 +	"[--" ^ sub ^ tvar ^ ",++" ^ sup ^ tvar ^ "]"
   1.146      end;
   1.147  
   1.148 -
   1.149  fun tptp_classrelClause (ClassrelClause {clause_id,subclass,superclass,...}) =
   1.150      let val relcls_id = clrelclause_prefix ^ ascii_of subclass ^ "_" ^ 
   1.151                          Int.toString clause_id
   1.152 -	val lits = tptp_classrelLits (make_type_class subclass) 
   1.153 -	                (Option.map make_type_class superclass)
   1.154 +	val lits = tptp_classrelLits (make_type_class subclass) (make_type_class superclass)
   1.155      in
   1.156  	"input_clause(" ^ relcls_id ^ ",axiom," ^ lits ^ ")."
   1.157      end;