src/Pure/theory.ML
changeset 16883 a89fafe1cbd8
parent 16803 014090d1e64b
child 16944 83ea7e3c6ec9
     1.1 --- a/src/Pure/theory.ML	Tue Jul 19 17:21:54 2005 +0200
     1.2 +++ b/src/Pure/theory.ML	Tue Jul 19 17:21:55 2005 +0200
     1.3 @@ -90,37 +90,6 @@
     1.4  
     1.5  
     1.6  
     1.7 -(** diagnostics **)  (* FIXME belongs to defs.ML *)
     1.8 -
     1.9 -fun pretty_const pp (c, T) =
    1.10 - [Pretty.str c, Pretty.str " ::", Pretty.brk 1,
    1.11 -  Pretty.quote (Pretty.typ pp (Type.freeze_type T))];    (* FIXME zero indexes!? *)
    1.12 -
    1.13 -fun pretty_path pp path = fold_rev (fn (T, c, def) =>
    1.14 -  fn [] => [Pretty.block (pretty_const pp (c, T))]
    1.15 -   | prts => Pretty.block (pretty_const pp (c, T) @
    1.16 -      [Pretty.brk 1, Pretty.str ("depends via " ^ quote def ^ " on")]) :: prts) path [];
    1.17 -
    1.18 -fun chain_history_msg s =    (* FIXME huh!? *)
    1.19 -  if Defs.chain_history () then s ^ ": "
    1.20 -  else s ^ " (set DEFS_CHAIN_HISTORY=ON for full history): ";
    1.21 -
    1.22 -fun defs_circular pp path =
    1.23 -  Pretty.str (chain_history_msg "Cyclic dependency of definitions") :: pretty_path pp path
    1.24 -  |> Pretty.chunks |> Pretty.string_of;
    1.25 -
    1.26 -fun defs_infinite_chain pp path =
    1.27 -  Pretty.str (chain_history_msg "Infinite chain of definitions") :: pretty_path pp path
    1.28 -  |> Pretty.chunks |> Pretty.string_of;
    1.29 -
    1.30 -fun defs_clash def1 def2 = "Type clash in definitions " ^ quote def1 ^ " and " ^ quote def2;
    1.31 -
    1.32 -fun defs_final pp const =
    1.33 -  (Pretty.str "Attempt to define final constant" :: Pretty.brk 1 :: pretty_const pp const)
    1.34 -  |> Pretty.block |> Pretty.string_of;
    1.35 -
    1.36 -
    1.37 -
    1.38  (** datatype thy **)
    1.39  
    1.40  datatype thy = Thy of
    1.41 @@ -149,9 +118,7 @@
    1.42        val Thy {axioms = _, defs = defs2, oracles = oracles2} = thy2;
    1.43  
    1.44        val axioms = NameSpace.empty_table;
    1.45 -      val defs = Defs.merge defs1 defs2  (* FIXME produce errors in defs.ML *)
    1.46 -        handle Defs.CIRCULAR namess => error (defs_circular pp namess)
    1.47 -          | Defs.INFINITE_CHAIN namess => error (defs_infinite_chain pp namess);
    1.48 +      val defs = Defs.merge pp defs1 defs2;
    1.49        val oracles = NameSpace.merge_tables eq_snd (oracles1, oracles2)
    1.50          handle Symtab.DUPS dups => err_dup_oras dups;
    1.51      in make_thy (axioms, defs, oracles) end;
    1.52 @@ -262,7 +229,7 @@
    1.53  
    1.54  fun overloading thy overloaded declT defT =
    1.55    let
    1.56 -    val defT' = Term.incr_tvar (maxidx_of_typ declT + 1) (Type.varifyT defT);
    1.57 +    val defT' = Logic.incr_tvar (maxidx_of_typ declT + 1) (Type.varifyT defT);
    1.58    in
    1.59      if Sign.typ_instance thy (declT, defT') then Clean
    1.60      else if Sign.typ_instance thy (Type.strip_sorts declT, Type.strip_sorts defT') then Useless
    1.61 @@ -312,19 +279,13 @@
    1.62  
    1.63  (* check_def *)
    1.64  
    1.65 -fun declare thy c defs =      (* FIXME move to defs.ML *)
    1.66 -  let val T = Sign.the_const_type thy c
    1.67 -  in if_none (try (Defs.declare defs) (c, T)) defs end;
    1.68 +fun pretty_const pp (c, T) =
    1.69 + [Pretty.str c, Pretty.str " ::", Pretty.brk 1,
    1.70 +  Pretty.quote (Pretty.typ pp (Type.freeze_type T))];
    1.71  
    1.72  fun check_def thy overloaded (bname, tm) defs =
    1.73    let
    1.74      val pp = Sign.pp thy;
    1.75 -
    1.76 -    fun err msg = error (Pretty.string_of (Pretty.chunks
    1.77 -     [Pretty.str msg, Pretty.block
    1.78 -      [Pretty.str ("The error(s) above occurred in definition " ^ quote bname ^ ":"),
    1.79 -        Pretty.fbrk, Pretty.quote (Pretty.term pp tm)]]));
    1.80 -
    1.81      fun prt_const (c, T) =
    1.82       [Pretty.str c, Pretty.str " ::", Pretty.brk 1,
    1.83        Pretty.quote (Pretty.typ pp (Type.freeze_type T))];
    1.84 @@ -332,28 +293,25 @@
    1.85        [Pretty.block (Pretty.str "Definition of " :: pretty_const pp const), Pretty.str txt]
    1.86        |> Pretty.chunks |> Pretty.string_of;
    1.87  
    1.88 -    val ((c, defT), rhs) = dest_def pp tm handle TERM (msg, _) => err msg;
    1.89 +    fun typed_const c = (c, Sign.the_const_type thy c);
    1.90 +
    1.91 +    val ((c, defT), rhs) = dest_def pp tm handle TERM (msg, _) => error msg;
    1.92      val rhs_consts = Term.term_constsT rhs;
    1.93      val declT = Sign.the_const_type thy c;
    1.94 -
    1.95      val _ =
    1.96        (case overloading thy overloaded declT defT of
    1.97          Clean => ()
    1.98        | Implicit => warning (string_of_def (c, defT)
    1.99            ("is strictly less general than the declared type (see " ^ quote bname ^ ")"))
   1.100 -      | Useless => err (Library.setmp show_sorts true (string_of_def (c, defT))
   1.101 +      | Useless => error (Library.setmp show_sorts true (string_of_def (c, defT))
   1.102            "imposes additional sort constraints on the declared type of the constant"));
   1.103 -
   1.104 -    val decl_defs = defs |> declare thy c |> fold (declare thy) (map #1 rhs_consts);
   1.105    in
   1.106 -    Defs.define decl_defs (c, defT) (Sign.full_name thy bname) rhs_consts
   1.107 -      (* FIXME produce errors in defs.ML *)
   1.108 -      handle Defs.DEFS msg => err ("DEFS: " ^ msg)   (* FIXME sys_error!? *)
   1.109 -        | Defs.CIRCULAR path => err (defs_circular pp path)
   1.110 -        | Defs.INFINITE_CHAIN path => err (defs_infinite_chain pp path)
   1.111 -        | Defs.CLASH (_, def1, def2) => err (defs_clash def1 def2)
   1.112 -        | Defs.FINAL const => err (defs_final pp const)
   1.113 -  end;
   1.114 +    defs |> Defs.declare (typed_const c) |> fold (Defs.declare o typed_const o #1) rhs_consts
   1.115 +    |> Defs.define pp (c, defT) (Sign.full_name thy bname) rhs_consts
   1.116 +  end
   1.117 +  handle ERROR => error (Pretty.string_of (Pretty.block
   1.118 +   [Pretty.str ("The error(s) above occurred in definition " ^ quote bname ^ ":"),
   1.119 +    Pretty.fbrk, Pretty.quote (Pretty.term (Sign.pp thy) tm)]));
   1.120  
   1.121  
   1.122  (* add_defs(_i) *)
   1.123 @@ -396,7 +354,7 @@
   1.124            | Implicit => warning ("Finalizing " ^ quote c ^
   1.125                " at a strictly less general type than declared")
   1.126            | Useless => err "Sort constraints stronger than declared");
   1.127 -      in Defs.finalize (if_none (try (Defs.declare finals) (c, declT)) finals) (c, defT) end;
   1.128 +      in finals |> Defs.declare (c, declT) |> Defs.finalize (c, defT) end;
   1.129    in thy |> map_defs (fold finalize (map (prep_term thy) raw_terms)) end;
   1.130  
   1.131  fun read_term thy = Sign.simple_read_term thy TypeInfer.logicT;