# HG changeset patch
# User blanchet
# Date 1271332637 -7200
# Node ID 0a6ed065683d4033d0d5d7199b1106764a37077c
# Parent  c1a35be8e4762f065fad18bdb5eb526c62b4b927
give more sensible names to "fol_type" constructors, as requested by a FIXME comment

diff -r c1a35be8e476 -r 0a6ed065683d src/HOL/Tools/Sledgehammer/metis_tactics.ML
--- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Thu Apr 15 13:49:46 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Thu Apr 15 13:57:17 2010 +0200
@@ -69,9 +69,9 @@
 
 fun metis_lit b c args = (b, (c, args));
 
-fun hol_type_to_fol (AtomV x) = Metis.Term.Var x
-  | hol_type_to_fol (AtomF x) = Metis.Term.Fn (x, [])
-  | hol_type_to_fol (Comp (tc, tps)) =
+fun hol_type_to_fol (TyVar x) = Metis.Term.Var x
+  | hol_type_to_fol (TyFree x) = Metis.Term.Fn (x, [])
+  | hol_type_to_fol (TyConstr (tc, tps)) =
     Metis.Term.Fn (tc, map hol_type_to_fol tps);
 
 (*These two functions insert type literals before the real literals. That is the
diff -r c1a35be8e476 -r 0a6ed065683d src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML	Thu Apr 15 13:49:46 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML	Thu Apr 15 13:57:17 2010 +0200
@@ -33,9 +33,9 @@
   datatype kind = Axiom | Conjecture
   type axiom_name = string
   datatype fol_type =
-      AtomV of string
-    | AtomF of string
-    | Comp of string * fol_type list
+    TyVar of string |
+    TyFree of string |
+    TyConstr of string * fol_type list
   val string_of_fol_type : fol_type -> string
   datatype type_literal = LTVar of string * string | LTFree of string * string
   exception CLAUSE of string * term
@@ -215,14 +215,14 @@
 
 (**** Isabelle FOL clauses ****)
 
-(*FIXME: give the constructors more sensible names*)
-datatype fol_type = AtomV of string
-                  | AtomF of string
-                  | Comp of string * fol_type list;
+datatype fol_type =
+  TyVar of string |
+  TyFree of string |
+  TyConstr 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)) =
+fun string_of_fol_type (TyVar s) = s
+  | string_of_fol_type (TyFree s) = s
+  | string_of_fol_type (TyConstr (tcon, tps)) =
       tcon ^ (paren_pack (map string_of_fol_type tps));
 
 (*First string is the type class; the second is a TVar or TFfree*)
@@ -230,15 +230,15 @@
 
 exception CLAUSE of string * term;
 
-fun atomic_type (TFree (a,_)) = AtomF(make_fixed_type_var a)
-  | atomic_type (TVar (v,_))  = AtomV(make_schematic_type_var v);
+fun atomic_type (TFree (a,_)) = TyFree(make_fixed_type_var a)
+  | atomic_type (TVar (v,_))  = TyVar(make_schematic_type_var v);
 
 (*Flatten a type to a fol_type while accumulating sort constraints on the TFrees and
   TVars it contains.*)
 fun type_of dfg (Type (a, Ts)) =
       let val (folTyps, ts) = types_of dfg Ts
           val t = make_fixed_type_const dfg a
-      in (Comp(t,folTyps), ts) end
+      in (TyConstr (t, folTyps), ts) end
   | type_of dfg T = (atomic_type T, [T])
 and types_of dfg Ts =
       let val (folTyps,ts) = ListPair.unzip (map (type_of dfg) Ts)
@@ -401,9 +401,9 @@
 
 (*** Find occurrences of functions in clauses ***)
 
-fun add_foltype_funcs (AtomV _, funcs) = funcs
-  | add_foltype_funcs (AtomF a, funcs) = Symtab.update (a,0) funcs
-  | add_foltype_funcs (Comp(a,tys), funcs) =
+fun add_foltype_funcs (TyVar _, funcs) = funcs
+  | add_foltype_funcs (TyFree a, funcs) = Symtab.update (a,0) funcs
+  | add_foltype_funcs (TyConstr (a, tys), funcs) =
       List.foldl add_foltype_funcs (Symtab.update (a, length tys) funcs) tys;
 
 (*TFrees are recorded as constants*)
diff -r c1a35be8e476 -r 0a6ed065683d src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML	Thu Apr 15 13:49:46 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML	Thu Apr 15 13:57:17 2010 +0200
@@ -103,18 +103,18 @@
 
 fun type_of dfg (Type (a, Ts)) =
       let val (folTypes,ts) = types_of dfg Ts
-      in  (Comp(make_fixed_type_const dfg a, folTypes), ts)  end
-  | type_of _ (tp as TFree (a, _)) = (AtomF (make_fixed_type_var a), [tp])
-  | type_of _ (tp as TVar (v, _)) = (AtomV (make_schematic_type_var v), [tp])
+      in  (TyConstr (make_fixed_type_const dfg a, folTypes), ts)  end
+  | type_of _ (tp as TFree (a, _)) = (TyFree (make_fixed_type_var a), [tp])
+  | type_of _ (tp as TVar (v, _)) = (TyVar (make_schematic_type_var v), [tp])
 and types_of dfg Ts =
       let val (folTyps,ts) = ListPair.unzip (map (type_of dfg) Ts)
       in  (folTyps, union_all ts)  end;
 
 (* same as above, but no gathering of sort information *)
 fun simp_type_of dfg (Type (a, Ts)) =
-      Comp(make_fixed_type_const dfg a, map (simp_type_of dfg) Ts)
-  | simp_type_of _ (TFree (a, _)) = AtomF (make_fixed_type_var a)
-  | simp_type_of _ (TVar (v, _)) = AtomV (make_schematic_type_var v);
+      TyConstr (make_fixed_type_const dfg a, map (simp_type_of dfg) Ts)
+  | simp_type_of _ (TFree (a, _)) = TyFree (make_fixed_type_var a)
+  | simp_type_of _ (TVar (v, _)) = TyVar (make_schematic_type_var v);
 
 
 fun const_type_of dfg thy (c,t) =
@@ -193,8 +193,8 @@
 (**********************************************************************)
 
 (*Result of a function type; no need to check that the argument type matches.*)
-fun result_type (Comp ("tc_fun", [_, tp2])) = tp2
-  | result_type _ = error "result_type"
+fun result_type (TyConstr ("tc_fun", [_, tp2])) = tp2
+  | result_type _ = raise Fail "Non-function type"
 
 fun type_of_combterm (CombConst (_, tp, _)) = tp
   | type_of_combterm (CombVar (_, tp)) = tp