give more sensible names to "fol_type" constructors, as requested by a FIXME comment
authorblanchet
Thu Apr 15 13:57:17 2010 +0200 (2010-04-15 ago)
changeset 361680a6ed065683d
parent 36167 c1a35be8e476
child 36169 27b1cc58715e
give more sensible names to "fol_type" constructors, as requested by a FIXME comment
src/HOL/Tools/Sledgehammer/metis_tactics.ML
src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML
src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML
     1.1 --- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Thu Apr 15 13:49:46 2010 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Thu Apr 15 13:57:17 2010 +0200
     1.3 @@ -69,9 +69,9 @@
     1.4  
     1.5  fun metis_lit b c args = (b, (c, args));
     1.6  
     1.7 -fun hol_type_to_fol (AtomV x) = Metis.Term.Var x
     1.8 -  | hol_type_to_fol (AtomF x) = Metis.Term.Fn (x, [])
     1.9 -  | hol_type_to_fol (Comp (tc, tps)) =
    1.10 +fun hol_type_to_fol (TyVar x) = Metis.Term.Var x
    1.11 +  | hol_type_to_fol (TyFree x) = Metis.Term.Fn (x, [])
    1.12 +  | hol_type_to_fol (TyConstr (tc, tps)) =
    1.13      Metis.Term.Fn (tc, map hol_type_to_fol tps);
    1.14  
    1.15  (*These two functions insert type literals before the real literals. That is the
     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML	Thu Apr 15 13:49:46 2010 +0200
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML	Thu Apr 15 13:57:17 2010 +0200
     2.3 @@ -33,9 +33,9 @@
     2.4    datatype kind = Axiom | Conjecture
     2.5    type axiom_name = string
     2.6    datatype fol_type =
     2.7 -      AtomV of string
     2.8 -    | AtomF of string
     2.9 -    | Comp of string * fol_type list
    2.10 +    TyVar of string |
    2.11 +    TyFree of string |
    2.12 +    TyConstr of string * fol_type list
    2.13    val string_of_fol_type : fol_type -> string
    2.14    datatype type_literal = LTVar of string * string | LTFree of string * string
    2.15    exception CLAUSE of string * term
    2.16 @@ -215,14 +215,14 @@
    2.17  
    2.18  (**** Isabelle FOL clauses ****)
    2.19  
    2.20 -(*FIXME: give the constructors more sensible names*)
    2.21 -datatype fol_type = AtomV of string
    2.22 -                  | AtomF of string
    2.23 -                  | Comp of string * fol_type list;
    2.24 +datatype fol_type =
    2.25 +  TyVar of string |
    2.26 +  TyFree of string |
    2.27 +  TyConstr of string * fol_type list
    2.28  
    2.29 -fun string_of_fol_type (AtomV x) = x
    2.30 -  | string_of_fol_type (AtomF x) = x
    2.31 -  | string_of_fol_type (Comp(tcon,tps)) =
    2.32 +fun string_of_fol_type (TyVar s) = s
    2.33 +  | string_of_fol_type (TyFree s) = s
    2.34 +  | string_of_fol_type (TyConstr (tcon, tps)) =
    2.35        tcon ^ (paren_pack (map string_of_fol_type tps));
    2.36  
    2.37  (*First string is the type class; the second is a TVar or TFfree*)
    2.38 @@ -230,15 +230,15 @@
    2.39  
    2.40  exception CLAUSE of string * term;
    2.41  
    2.42 -fun atomic_type (TFree (a,_)) = AtomF(make_fixed_type_var a)
    2.43 -  | atomic_type (TVar (v,_))  = AtomV(make_schematic_type_var v);
    2.44 +fun atomic_type (TFree (a,_)) = TyFree(make_fixed_type_var a)
    2.45 +  | atomic_type (TVar (v,_))  = TyVar(make_schematic_type_var v);
    2.46  
    2.47  (*Flatten a type to a fol_type while accumulating sort constraints on the TFrees and
    2.48    TVars it contains.*)
    2.49  fun type_of dfg (Type (a, Ts)) =
    2.50        let val (folTyps, ts) = types_of dfg Ts
    2.51            val t = make_fixed_type_const dfg a
    2.52 -      in (Comp(t,folTyps), ts) end
    2.53 +      in (TyConstr (t, folTyps), ts) end
    2.54    | type_of dfg T = (atomic_type T, [T])
    2.55  and types_of dfg Ts =
    2.56        let val (folTyps,ts) = ListPair.unzip (map (type_of dfg) Ts)
    2.57 @@ -401,9 +401,9 @@
    2.58  
    2.59  (*** Find occurrences of functions in clauses ***)
    2.60  
    2.61 -fun add_foltype_funcs (AtomV _, funcs) = funcs
    2.62 -  | add_foltype_funcs (AtomF a, funcs) = Symtab.update (a,0) funcs
    2.63 -  | add_foltype_funcs (Comp(a,tys), funcs) =
    2.64 +fun add_foltype_funcs (TyVar _, funcs) = funcs
    2.65 +  | add_foltype_funcs (TyFree a, funcs) = Symtab.update (a,0) funcs
    2.66 +  | add_foltype_funcs (TyConstr (a, tys), funcs) =
    2.67        List.foldl add_foltype_funcs (Symtab.update (a, length tys) funcs) tys;
    2.68  
    2.69  (*TFrees are recorded as constants*)
     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML	Thu Apr 15 13:49:46 2010 +0200
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML	Thu Apr 15 13:57:17 2010 +0200
     3.3 @@ -103,18 +103,18 @@
     3.4  
     3.5  fun type_of dfg (Type (a, Ts)) =
     3.6        let val (folTypes,ts) = types_of dfg Ts
     3.7 -      in  (Comp(make_fixed_type_const dfg a, folTypes), ts)  end
     3.8 -  | type_of _ (tp as TFree (a, _)) = (AtomF (make_fixed_type_var a), [tp])
     3.9 -  | type_of _ (tp as TVar (v, _)) = (AtomV (make_schematic_type_var v), [tp])
    3.10 +      in  (TyConstr (make_fixed_type_const dfg a, folTypes), ts)  end
    3.11 +  | type_of _ (tp as TFree (a, _)) = (TyFree (make_fixed_type_var a), [tp])
    3.12 +  | type_of _ (tp as TVar (v, _)) = (TyVar (make_schematic_type_var v), [tp])
    3.13  and types_of dfg Ts =
    3.14        let val (folTyps,ts) = ListPair.unzip (map (type_of dfg) Ts)
    3.15        in  (folTyps, union_all ts)  end;
    3.16  
    3.17  (* same as above, but no gathering of sort information *)
    3.18  fun simp_type_of dfg (Type (a, Ts)) =
    3.19 -      Comp(make_fixed_type_const dfg a, map (simp_type_of dfg) Ts)
    3.20 -  | simp_type_of _ (TFree (a, _)) = AtomF (make_fixed_type_var a)
    3.21 -  | simp_type_of _ (TVar (v, _)) = AtomV (make_schematic_type_var v);
    3.22 +      TyConstr (make_fixed_type_const dfg a, map (simp_type_of dfg) Ts)
    3.23 +  | simp_type_of _ (TFree (a, _)) = TyFree (make_fixed_type_var a)
    3.24 +  | simp_type_of _ (TVar (v, _)) = TyVar (make_schematic_type_var v);
    3.25  
    3.26  
    3.27  fun const_type_of dfg thy (c,t) =
    3.28 @@ -193,8 +193,8 @@
    3.29  (**********************************************************************)
    3.30  
    3.31  (*Result of a function type; no need to check that the argument type matches.*)
    3.32 -fun result_type (Comp ("tc_fun", [_, tp2])) = tp2
    3.33 -  | result_type _ = error "result_type"
    3.34 +fun result_type (TyConstr ("tc_fun", [_, tp2])) = tp2
    3.35 +  | result_type _ = raise Fail "Non-function type"
    3.36  
    3.37  fun type_of_combterm (CombConst (_, tp, _)) = tp
    3.38    | type_of_combterm (CombVar (_, tp)) = tp