# HG changeset patch
# User mengj
# Date 1134520843 -3600
# Node ID aaba095cf62bb11ea0c48f4abddc9463307b3726
# Parent  8faa44b32a8c91cb704b522bdd3bac5fb7ba41a5
1. changed fol_type, it's not a string type anymore.
2. sort literals in clauses.

diff -r 8faa44b32a8c -r aaba095cf62b src/HOL/Tools/res_clause.ML
--- a/src/HOL/Tools/res_clause.ML	Wed Dec 14 01:39:41 2005 +0100
+++ b/src/HOL/Tools/res_clause.ML	Wed Dec 14 01:40:43 2005 +0100
@@ -208,7 +208,23 @@
 
 type pred_name = string;
 type sort = Term.sort;
-type fol_type = string;
+
+
+
+datatype typ_var = FOLTVar of indexname | FOLTFree of string;
+
+datatype fol_type = AtomV of string
+		  | AtomF of string
+		  | Comp of string * fol_type list;
+
+fun string_of_fol_type (AtomV x) = x
+  | string_of_fol_type (AtomF x) = x
+  | string_of_fol_type (Comp(tcon,tps)) = 
+    let val tstrs = map string_of_fol_type tps
+    in
+	tcon ^ (paren_pack tstrs)
+    end;
+
 
 datatype type_literal = LTVar of string | LTFree of string;
 
@@ -218,8 +234,6 @@
 
 datatype literal = Literal of polarity * predicate * tag;
 
-datatype typ_var = FOLTVar of indexname | FOLTFree of string;
-
 fun mk_typ_var_sort (TFree(a,s)) = (FOLTFree a,s)
   | mk_typ_var_sort (TVar(v,s)) = (FOLTVar v,s);
 
@@ -241,6 +255,12 @@
 
 exception CLAUSE of string * term;
 
+fun get_literals (c as Clause(cls)) = #literals cls;
+
+fun components_of_literal (Literal (pol,pred,tag)) = ((pol,pred),tag);
+
+fun predicate_name (Predicate(predname,_,_)) = predname;
+
 
 (*** make clauses ***)
 
@@ -293,18 +313,18 @@
 fun init thy = (const_typargs := Sign.const_typargs thy);
     
 
-(*Flatten a type to a string while accumulating sort constraints on the TFrees and
+(*Flatten a type to a fol_type while accumulating sort constraints on the TFrees and
   TVars it contains.*)    
 fun type_of (Type (a, Ts)) = 
       let val (folTyps, (ts, funcs)) = types_of Ts 
 	  val t = make_fixed_type_const a
       in    
-	  ((t ^ paren_pack folTyps), (ts, (t, length Ts)::funcs))
+	  (Comp(t,folTyps), (ts, (t, length Ts)::funcs))
       end
   | type_of (TFree (a,s)) = 
       let val t = make_fixed_type_var a
-      in (t, ([((FOLTFree a),s)], [(t,0)])) end
-  | type_of (TVar (v, s)) = (make_schematic_type_var v, ([((FOLTVar v),s)], []))
+      in (AtomF(t), ([((FOLTFree a),s)], [(t,0)])) end
+  | type_of (TVar (v, s)) = (AtomV(make_schematic_type_var v), ([((FOLTVar v),s)], []))
 and types_of Ts =
       let val foltyps_ts = map type_of Ts 
 	  val (folTyps,ts_funcs) = ListPair.unzip foltyps_ts
@@ -447,6 +467,17 @@
 val literals_of_term = literals_of_term1 ([],[],[],[]);
 
 
+fun predicate_ord (Predicate(predname1,_,_),Predicate(predname2,_,_)) = string_ord (predname1,predname2);
+
+
+fun literal_ord (Literal(false,_,_),Literal(true,_,_)) = LESS
+  | literal_ord (Literal(true,_,_),Literal(false,_,_)) = GREATER
+  | literal_ord (Literal(_,pred1,_),Literal(_,pred2,_)) = predicate_ord(pred1,pred2);
+
+fun sort_lits lits = sort literal_ord lits;
+
+
+
 (* FIX: not sure what to do with these funcs *)
 
 (*Make literals for sorted type variables*) 
@@ -522,11 +553,12 @@
 
 fun make_axiom_clause_thm thm (ax_name,cls_id) =
     let val (lits,types_sorts, preds, funcs) = literals_of_term (prop_of thm)
+	val lits' = sort_lits lits
 	val (tvar_lits,tfree_lits, preds) = add_typs_aux types_sorts preds 
         val tvars = get_tvar_strs types_sorts
     in 
 	make_clause(cls_id,ax_name,Axiom,
-	            lits,types_sorts,tvar_lits,tfree_lits,
+	            lits',types_sorts,tvar_lits,tfree_lits,
 	            tvars, preds, funcs)
     end;
 
@@ -556,11 +588,12 @@
     let val _ = check_is_fol_term term 
 	    handle TERM("check_is_fol_term",_) => raise CLAUSE("Axiom is not FOL", term) 
 	val (lits,types_sorts, preds,funcs) = literals_of_term term
+	val lits' = sort_lits lits
 	val (tvar_lits,tfree_lits, preds) = add_typs_aux types_sorts preds
         val tvars = get_tvar_strs types_sorts	
     in 
 	make_clause(cls_id,ax_name,Axiom,
-	            lits,types_sorts,tvar_lits,tfree_lits,
+	            lits',types_sorts,tvar_lits,tfree_lits,
 	            tvars, preds,funcs)
     end;
 
@@ -679,10 +712,11 @@
  and if we specifically ask for types to be included.   *)
 fun string_of_equality (typ,terms) =
       let val [tstr1,tstr2] = map string_of_term terms
+	  val typ' = string_of_fol_type typ
       in
 	  if !keep_types andalso !special_equal 
-	  then "equal(" ^ (wrap_eq_type typ tstr1) ^ "," ^ 
-		 	  (wrap_eq_type typ tstr2) ^ ")"
+	  then "equal(" ^ (wrap_eq_type typ' tstr1) ^ "," ^ 
+		 	  (wrap_eq_type typ' tstr2) ^ ")"
 	  else "equal(" ^ tstr1 ^ "," ^ tstr2 ^ ")"
       end
 and string_of_term (UVar(x,_)) = x
@@ -690,7 +724,7 @@
   | string_of_term (Fun (name,typs,[])) = name (*Overloaded consts like 0 don't get types!*)
   | string_of_term (Fun (name,typs,terms)) = 
       let val terms_as_strings = map string_of_term terms
-	  val typs' = if !keep_types then typs else []
+	  val typs' = if !keep_types then map string_of_fol_type typs else []
       in  name ^ (paren_pack (terms_as_strings @ typs'))  end
   | string_of_term _ = error "string_of_term";      
 
@@ -698,7 +732,7 @@
 fun string_of_predicate (Predicate("equal",[typ],terms)) = string_of_equality(typ,terms)
   | string_of_predicate (Predicate(name,typs,terms)) = 
       let val terms_as_strings = map string_of_term terms
-	  val typs' = if !keep_types then typs else []
+	  val typs' = if !keep_types then map string_of_fol_type typs else []
       in  name ^ (paren_pack (terms_as_strings @ typs'))  end
   | string_of_predicate _ = error "string_of_predicate";