1. changed fol_type, it's not a string type anymore.
authormengj
Wed Dec 14 01:40:43 2005 +0100 (2005-12-14)
changeset 18402aaba095cf62b
parent 18401 8faa44b32a8c
child 18403 df0c0f35c897
1. changed fol_type, it's not a string type anymore.
2. sort literals in clauses.
src/HOL/Tools/res_clause.ML
     1.1 --- a/src/HOL/Tools/res_clause.ML	Wed Dec 14 01:39:41 2005 +0100
     1.2 +++ b/src/HOL/Tools/res_clause.ML	Wed Dec 14 01:40:43 2005 +0100
     1.3 @@ -208,7 +208,23 @@
     1.4  
     1.5  type pred_name = string;
     1.6  type sort = Term.sort;
     1.7 -type fol_type = string;
     1.8 +
     1.9 +
    1.10 +
    1.11 +datatype typ_var = FOLTVar of indexname | FOLTFree of string;
    1.12 +
    1.13 +datatype fol_type = AtomV of string
    1.14 +		  | AtomF of string
    1.15 +		  | Comp of string * fol_type list;
    1.16 +
    1.17 +fun string_of_fol_type (AtomV x) = x
    1.18 +  | string_of_fol_type (AtomF x) = x
    1.19 +  | string_of_fol_type (Comp(tcon,tps)) = 
    1.20 +    let val tstrs = map string_of_fol_type tps
    1.21 +    in
    1.22 +	tcon ^ (paren_pack tstrs)
    1.23 +    end;
    1.24 +
    1.25  
    1.26  datatype type_literal = LTVar of string | LTFree of string;
    1.27  
    1.28 @@ -218,8 +234,6 @@
    1.29  
    1.30  datatype literal = Literal of polarity * predicate * tag;
    1.31  
    1.32 -datatype typ_var = FOLTVar of indexname | FOLTFree of string;
    1.33 -
    1.34  fun mk_typ_var_sort (TFree(a,s)) = (FOLTFree a,s)
    1.35    | mk_typ_var_sort (TVar(v,s)) = (FOLTVar v,s);
    1.36  
    1.37 @@ -241,6 +255,12 @@
    1.38  
    1.39  exception CLAUSE of string * term;
    1.40  
    1.41 +fun get_literals (c as Clause(cls)) = #literals cls;
    1.42 +
    1.43 +fun components_of_literal (Literal (pol,pred,tag)) = ((pol,pred),tag);
    1.44 +
    1.45 +fun predicate_name (Predicate(predname,_,_)) = predname;
    1.46 +
    1.47  
    1.48  (*** make clauses ***)
    1.49  
    1.50 @@ -293,18 +313,18 @@
    1.51  fun init thy = (const_typargs := Sign.const_typargs thy);
    1.52      
    1.53  
    1.54 -(*Flatten a type to a string while accumulating sort constraints on the TFrees and
    1.55 +(*Flatten a type to a fol_type while accumulating sort constraints on the TFrees and
    1.56    TVars it contains.*)    
    1.57  fun type_of (Type (a, Ts)) = 
    1.58        let val (folTyps, (ts, funcs)) = types_of Ts 
    1.59  	  val t = make_fixed_type_const a
    1.60        in    
    1.61 -	  ((t ^ paren_pack folTyps), (ts, (t, length Ts)::funcs))
    1.62 +	  (Comp(t,folTyps), (ts, (t, length Ts)::funcs))
    1.63        end
    1.64    | type_of (TFree (a,s)) = 
    1.65        let val t = make_fixed_type_var a
    1.66 -      in (t, ([((FOLTFree a),s)], [(t,0)])) end
    1.67 -  | type_of (TVar (v, s)) = (make_schematic_type_var v, ([((FOLTVar v),s)], []))
    1.68 +      in (AtomF(t), ([((FOLTFree a),s)], [(t,0)])) end
    1.69 +  | type_of (TVar (v, s)) = (AtomV(make_schematic_type_var v), ([((FOLTVar v),s)], []))
    1.70  and types_of Ts =
    1.71        let val foltyps_ts = map type_of Ts 
    1.72  	  val (folTyps,ts_funcs) = ListPair.unzip foltyps_ts
    1.73 @@ -447,6 +467,17 @@
    1.74  val literals_of_term = literals_of_term1 ([],[],[],[]);
    1.75  
    1.76  
    1.77 +fun predicate_ord (Predicate(predname1,_,_),Predicate(predname2,_,_)) = string_ord (predname1,predname2);
    1.78 +
    1.79 +
    1.80 +fun literal_ord (Literal(false,_,_),Literal(true,_,_)) = LESS
    1.81 +  | literal_ord (Literal(true,_,_),Literal(false,_,_)) = GREATER
    1.82 +  | literal_ord (Literal(_,pred1,_),Literal(_,pred2,_)) = predicate_ord(pred1,pred2);
    1.83 +
    1.84 +fun sort_lits lits = sort literal_ord lits;
    1.85 +
    1.86 +
    1.87 +
    1.88  (* FIX: not sure what to do with these funcs *)
    1.89  
    1.90  (*Make literals for sorted type variables*) 
    1.91 @@ -522,11 +553,12 @@
    1.92  
    1.93  fun make_axiom_clause_thm thm (ax_name,cls_id) =
    1.94      let val (lits,types_sorts, preds, funcs) = literals_of_term (prop_of thm)
    1.95 +	val lits' = sort_lits lits
    1.96  	val (tvar_lits,tfree_lits, preds) = add_typs_aux types_sorts preds 
    1.97          val tvars = get_tvar_strs types_sorts
    1.98      in 
    1.99  	make_clause(cls_id,ax_name,Axiom,
   1.100 -	            lits,types_sorts,tvar_lits,tfree_lits,
   1.101 +	            lits',types_sorts,tvar_lits,tfree_lits,
   1.102  	            tvars, preds, funcs)
   1.103      end;
   1.104  
   1.105 @@ -556,11 +588,12 @@
   1.106      let val _ = check_is_fol_term term 
   1.107  	    handle TERM("check_is_fol_term",_) => raise CLAUSE("Axiom is not FOL", term) 
   1.108  	val (lits,types_sorts, preds,funcs) = literals_of_term term
   1.109 +	val lits' = sort_lits lits
   1.110  	val (tvar_lits,tfree_lits, preds) = add_typs_aux types_sorts preds
   1.111          val tvars = get_tvar_strs types_sorts	
   1.112      in 
   1.113  	make_clause(cls_id,ax_name,Axiom,
   1.114 -	            lits,types_sorts,tvar_lits,tfree_lits,
   1.115 +	            lits',types_sorts,tvar_lits,tfree_lits,
   1.116  	            tvars, preds,funcs)
   1.117      end;
   1.118  
   1.119 @@ -679,10 +712,11 @@
   1.120   and if we specifically ask for types to be included.   *)
   1.121  fun string_of_equality (typ,terms) =
   1.122        let val [tstr1,tstr2] = map string_of_term terms
   1.123 +	  val typ' = string_of_fol_type typ
   1.124        in
   1.125  	  if !keep_types andalso !special_equal 
   1.126 -	  then "equal(" ^ (wrap_eq_type typ tstr1) ^ "," ^ 
   1.127 -		 	  (wrap_eq_type typ tstr2) ^ ")"
   1.128 +	  then "equal(" ^ (wrap_eq_type typ' tstr1) ^ "," ^ 
   1.129 +		 	  (wrap_eq_type typ' tstr2) ^ ")"
   1.130  	  else "equal(" ^ tstr1 ^ "," ^ tstr2 ^ ")"
   1.131        end
   1.132  and string_of_term (UVar(x,_)) = x
   1.133 @@ -690,7 +724,7 @@
   1.134    | string_of_term (Fun (name,typs,[])) = name (*Overloaded consts like 0 don't get types!*)
   1.135    | string_of_term (Fun (name,typs,terms)) = 
   1.136        let val terms_as_strings = map string_of_term terms
   1.137 -	  val typs' = if !keep_types then typs else []
   1.138 +	  val typs' = if !keep_types then map string_of_fol_type typs else []
   1.139        in  name ^ (paren_pack (terms_as_strings @ typs'))  end
   1.140    | string_of_term _ = error "string_of_term";      
   1.141  
   1.142 @@ -698,7 +732,7 @@
   1.143  fun string_of_predicate (Predicate("equal",[typ],terms)) = string_of_equality(typ,terms)
   1.144    | string_of_predicate (Predicate(name,typs,terms)) = 
   1.145        let val terms_as_strings = map string_of_term terms
   1.146 -	  val typs' = if !keep_types then typs else []
   1.147 +	  val typs' = if !keep_types then map string_of_fol_type typs else []
   1.148        in  name ^ (paren_pack (terms_as_strings @ typs'))  end
   1.149    | string_of_predicate _ = error "string_of_predicate";      
   1.150