cleaned up some diagnostic mathom
authorhaftmann
Mon Apr 24 16:36:07 2006 +0200 (2006-04-24)
changeset 19455d828bfab05af
parent 19454 46a7e133f802
child 19456 b5bfd2d17dd3
cleaned up some diagnostic mathom
src/Pure/tctical.ML
src/Pure/term.ML
     1.1 --- a/src/Pure/tctical.ML	Mon Apr 24 16:35:30 2006 +0200
     1.2 +++ b/src/Pure/tctical.ML	Mon Apr 24 16:36:07 2006 +0200
     1.3 @@ -482,36 +482,34 @@
     1.4    in SOME (map (forall_elim_vars 0 o assume o cterm) hyps) end
     1.5    handle TERM ("nth_prem", [A]) => NONE;
     1.6  
     1.7 -
     1.8 -fun find_vars thy (Const(c,tp)) vars =
     1.9 -    let val tvars = Term.typ_tvars tp
    1.10 -    in
    1.11 -	case tvars of [] => vars
    1.12 -		    | _ => insert (op =) (c ^ " has type: " ^ (Sign.string_of_typ thy tp)) vars
    1.13 -    end
    1.14 -  | find_vars thy (t as Var(_,_)) vars =
    1.15 -    insert (op =) ("Var " ^ (Term.str_of_term t)) vars
    1.16 -  | find_vars _ (Free(_,_)) vars = vars
    1.17 -  | find_vars _ (Bound _) vars = vars
    1.18 -  | find_vars thy (Abs(_,tp,b)) vars = find_vars thy b vars
    1.19 -  | find_vars thy (t1 $ t2) vars = 
    1.20 -    find_vars thy t2 (find_vars thy t1 vars);
    1.21 -
    1.22 -  
    1.23 -fun warning_multi [] = ()
    1.24 -  | warning_multi (str1::strs) =
    1.25 -    (warning str1; warning_multi strs);
    1.26 +local
    1.27  
    1.28  fun print_vars_terms thy (n,thm) =
    1.29 -    let val prem = Logic.nth_prem (n, Thm.prop_of thm)
    1.30 -	val tms = find_vars thy prem []
    1.31 -    in
    1.32 -	(warning "Found schematic vars in assumptions: "; warning_multi tms)
    1.33 -    end;
    1.34 +  let
    1.35 +    fun find_vars thy (Const (c, ty)) =
    1.36 +        (case Term.typ_tvars ty
    1.37 +         of [] => I
    1.38 +          | _ => insert (op =) (c ^ " has type: " ^ (Sign.string_of_typ thy ty)))
    1.39 +      | find_vars thy (t as Var _) =
    1.40 +          insert (op =) ("Var " ^ (Term.str_of_term t))
    1.41 +      | find_vars _ (Free _) = I
    1.42 +      | find_vars _ (Bound _) = I
    1.43 +      | find_vars thy (Abs (_, _, t)) = find_vars thy t
    1.44 +      | find_vars thy (t1 $ t2) = 
    1.45 +          find_vars thy t1 #> find_vars thy t1;
    1.46 +    val prem = Logic.nth_prem (n, Thm.prop_of thm)
    1.47 +    val tms = find_vars thy prem []
    1.48 +  in
    1.49 +    (warning "Found schematic vars in assumptions:"; warning (cat_lines tms))
    1.50 +  end;
    1.51 +
    1.52 +in
    1.53  
    1.54  fun METAHYPS tacf n thm = SUBGOAL (metahyps_aux_tac tacf) n thm
    1.55      handle THM("assume: variables",_,_) => (print_vars_terms (theory_of_thm thm) (n,thm); Seq.empty)
    1.56  
    1.57 +end; (*local*)
    1.58 +
    1.59  (*Makes a tactic whose effect on a state is given by thmfun: thm->thm seq.*)
    1.60  fun PRIMSEQ thmfun st =  thmfun st handle THM _ => Seq.empty;
    1.61  
    1.62 @@ -520,7 +518,7 @@
    1.63  
    1.64  (* Inverse (more or less) of PRIMITIVE *)
    1.65  fun SINGLE tacf = Option.map fst o Seq.pull o tacf
    1.66 -		  
    1.67 +
    1.68  end;
    1.69  
    1.70  open Tactical;
     2.1 --- a/src/Pure/term.ML	Mon Apr 24 16:35:30 2006 +0200
     2.2 +++ b/src/Pure/term.ML	Mon Apr 24 16:36:07 2006 +0200
     2.3 @@ -209,6 +209,8 @@
     2.4    val adhoc_freeze_vars: term -> term * string list
     2.5    val string_of_vname: indexname -> string
     2.6    val string_of_vname': indexname -> string
     2.7 +  val str_of_sort: sort -> string
     2.8 +  val str_of_typ: typ -> string
     2.9    val str_of_term: term -> string
    2.10  end;
    2.11  
    2.12 @@ -1312,8 +1314,6 @@
    2.13    in (subst_atomic insts tm, xs) end;
    2.14  
    2.15  
    2.16 -(* string_of_vname *)
    2.17 -
    2.18  val show_question_marks = ref true;
    2.19  
    2.20  fun string_of_vname (x, i) =
    2.21 @@ -1335,15 +1335,36 @@
    2.22  fun string_of_vname' (x, ~1) = x
    2.23    | string_of_vname' xi = string_of_vname xi;
    2.24  
    2.25 -
    2.26 -(* str_of_term *)
    2.27 +fun str_of_sort [] = "{}"
    2.28 +  | str_of_sort [c] = c
    2.29 +  | str_of_sort cs = (enclose "{" "}" o commas) cs
    2.30  
    2.31 -fun str_of_term (Const (c, _)) = c
    2.32 -  | str_of_term (Free (x, _)) = x
    2.33 -  | str_of_term (Var (xi, _)) = string_of_vname xi
    2.34 -  | str_of_term (Bound i) = string_of_int i
    2.35 -  | str_of_term (Abs (x, _, t)) = "%" ^ x ^ ". " ^ str_of_term t
    2.36 -  | str_of_term (t $ u) = "(" ^ str_of_term t ^ " " ^ str_of_term u ^ ")";
    2.37 +fun str_of_typ (Type ("fun", [ty1, ty2])) =
    2.38 +      "(" ^ str_of_typ ty1 ^ " => " ^ str_of_typ ty2 ^ ")"
    2.39 +  | str_of_typ (Type ("dummy", [])) =
    2.40 +      "_"
    2.41 +  | str_of_typ (Type (tyco, _)) =
    2.42 +      tyco
    2.43 +  | str_of_typ (Type (tyco, tys)) =
    2.44 +      (enclose "(" ")" o space_implode " ") (tyco :: map str_of_typ tys)
    2.45 +  | str_of_typ (TFree (v, sort)) =
    2.46 +      v ^ "::" ^ str_of_sort sort
    2.47 +  | str_of_typ (TVar (vi, sort)) =
    2.48 +      string_of_vname vi ^ "::" ^ str_of_sort sort;
    2.49 +
    2.50 +val str_of_term =
    2.51 +  let
    2.52 +    fun typed (s, ty) = s ^ "::" ^ str_of_typ ty;
    2.53 +    fun bound vs i = case AList.lookup (op =) vs i
    2.54 +     of SOME v => enclose "[" "]" (string_of_int i ^ " ~> " ^ v)
    2.55 +      | NONE => (enclose "[" "]" o string_of_int) i
    2.56 +    fun str vs (Const (c, _)) = c
    2.57 +      | str vs (Free (v, ty)) = typed (v, ty)
    2.58 +      | str vs (Var (vi, ty)) = typed (string_of_vname vi, ty)
    2.59 +      | str vs (Bound i) = bound vs i
    2.60 +      | str vs (Abs (x, ty, t)) = "(%" ^ typed (x, ty) ^ ". " ^ str ((length vs, x)::vs) t ^ ")"
    2.61 +      | str vs (t1 $ t2) = "(" ^ str vs t1 ^ " " ^ str vs t2 ^ ")";
    2.62 +  in str [] end;
    2.63  
    2.64  end;
    2.65