# HG changeset patch
# User wenzelm
# Date 1139338609 -3600
# Node ID ea42ab6c08d153aff10c8a1a830aa7505e0a3848
# Parent  dc49d8b188863b07abc2c01af48aa842a8241bfb
export consts_of;
removed const_expansion;
pretty_term', infer_types(_simult): separate Consts.T argument;
added generic certify;
simplified certify_term/prop;

diff -r dc49d8b18886 -r ea42ab6c08d1 src/Pure/sign.ML
--- a/src/Pure/sign.ML	Tue Feb 07 19:56:48 2006 +0100
+++ b/src/Pure/sign.ML	Tue Feb 07 19:56:49 2006 +0100
@@ -25,8 +25,8 @@
   val del_modesyntax_i: (string * bool) -> (bstring * typ * mixfix) list -> theory -> theory
   val add_consts: (bstring * string * mixfix) list -> theory -> theory
   val add_consts_i: (bstring * typ * mixfix) list -> theory -> theory
-  val add_abbrevs: (bstring * string * mixfix) list -> theory -> theory
-  val add_abbrevs_i: (bstring * term * mixfix) list -> theory -> theory
+  val add_abbrevs: bool -> (bstring * string * mixfix) list -> theory -> theory
+  val add_abbrevs_i: bool -> (bstring * term * mixfix) list -> theory -> theory
   val add_const_constraint: xstring * string -> theory -> theory
   val add_const_constraint_i: string * typ -> theory -> theory
   val add_classes: (bstring * xstring list) list -> theory -> theory
@@ -109,6 +109,7 @@
   val typ_match: theory -> typ * typ -> Type.tyenv -> Type.tyenv
   val typ_unify: theory -> typ * typ -> Type.tyenv * int -> Type.tyenv * int
   val is_logtype: theory -> string -> bool
+  val consts_of: theory -> Consts.T
   val const_constraint: theory -> string -> typ option
   val the_const_constraint: theory -> string -> typ
   val const_type: theory -> string -> typ option
@@ -118,7 +119,6 @@
   val const_monomorphic: theory -> string -> bool
   val const_typargs: theory -> string * typ -> typ list
   val const_instance: theory -> string * typ list -> typ
-  val const_expansion: theory -> string * typ -> term option
   val class_space: theory -> NameSpace.T
   val type_space: theory -> NameSpace.T
   val const_space: theory -> NameSpace.T
@@ -133,9 +133,8 @@
   val intern_typ: theory -> typ -> typ
   val extern_typ: theory -> typ -> typ
   val intern_term: theory -> term -> term
-  val extern_term: theory -> term -> term
   val intern_tycons: theory -> typ -> typ
-  val pretty_term': Syntax.syntax -> Context.generic -> term -> Pretty.T
+  val pretty_term': Syntax.syntax -> Consts.T -> Context.generic -> term -> Pretty.T
   val pretty_term: theory -> term -> Pretty.T
   val pretty_typ: theory -> typ -> Pretty.T
   val pretty_sort: theory -> sort -> Pretty.T
@@ -154,8 +153,9 @@
   val certify_typ: theory -> typ -> typ
   val certify_typ_syntax: theory -> typ -> typ
   val certify_typ_abbrev: theory -> typ -> typ
-  val certify_term: Pretty.pp -> theory -> term -> term * typ * int
-  val certify_prop: Pretty.pp -> theory -> term -> term * typ * int
+  val certify: bool -> bool -> Pretty.pp -> theory -> term -> term * typ * int
+  val certify_term: theory -> term -> term * typ * int
+  val certify_prop: theory -> term -> term * typ * int
   val cert_term: theory -> term -> term
   val cert_prop: theory -> term -> term
   val no_vars: Pretty.pp -> term -> term
@@ -173,14 +173,14 @@
   val read_typ_abbrev: theory * (indexname -> sort option) -> string -> typ
   val read_tyname: theory -> string -> typ
   val read_const: theory -> string -> term
-  val infer_types_simult: Pretty.pp -> theory -> (indexname -> typ option) ->
+  val infer_types_simult: Pretty.pp -> theory -> Consts.T -> (indexname -> typ option) ->
     (indexname -> sort option) -> string list -> bool
     -> (term list * typ) list -> term list * (indexname * typ) list
-  val infer_types: Pretty.pp -> theory -> (indexname -> typ option) ->
+  val infer_types: Pretty.pp -> theory -> Consts.T -> (indexname -> typ option) ->
     (indexname -> sort option) -> string list -> bool
     -> term list * typ -> term * (indexname * typ) list
-  val read_def_terms': Pretty.pp -> (string -> bool) -> Syntax.syntax -> Context.generic ->
-    (indexname -> typ option) * (indexname -> sort option) ->
+  val read_def_terms': Pretty.pp -> (string -> bool) -> Syntax.syntax -> Consts.T ->
+    Context.generic -> (indexname -> typ option) * (indexname -> sort option) ->
     string list -> bool -> (string * typ) list -> term list * (indexname * typ) list
   val read_def_terms:
     theory * (indexname -> typ option) * (indexname -> sort option) ->
@@ -288,7 +288,6 @@
 val const_monomorphic = Consts.monomorphic o consts_of;
 val const_typargs = Consts.typargs o consts_of;
 val const_instance = Consts.instance o consts_of;
-fun const_expansion thy = Consts.expansion (tsig_of thy) (consts_of thy);
 
 val declared_tyname = Symtab.defined o #2 o #types o Type.rep_tsig o tsig_of;
 val declared_const = is_some oo const_type;
@@ -299,7 +298,7 @@
 
 val class_space = #1 o #classes o Type.rep_tsig o tsig_of;
 val type_space = #1 o #types o Type.rep_tsig o tsig_of;
-val const_space = Consts.space o consts_of;
+val const_space = Consts.space_of o consts_of;
 
 val intern_class = NameSpace.intern o class_space;
 val extern_class = NameSpace.extern o class_space;
@@ -347,7 +346,7 @@
 val intern_typ = typ_mapping intern_class intern_type;
 val extern_typ = typ_mapping extern_class extern_type;
 val intern_term = term_mapping intern_class intern_type intern_const;
-val extern_term = term_mapping extern_class extern_type extern_const;
+val extern_term = term_mapping extern_class extern_type;
 val intern_tycons = typ_mapping (K I) intern_type;
 
 end;
@@ -356,13 +355,14 @@
 
 (** pretty printing of terms, types etc. **)
 
-fun pretty_term' syn context t =
+fun pretty_term' syn consts context t =
   let
     val thy = Context.theory_of context;
     val curried = Context.exists_name Context.CPureN thy;
-  in Syntax.pretty_term context syn curried (extern_term thy t) end;
+    val extern = NameSpace.extern (Consts.space_of consts);
+  in Syntax.pretty_term context syn curried (extern_term (K extern) thy t) end;
 
-fun pretty_term thy t = pretty_term' (syn_of thy) (Context.Theory thy) t;
+fun pretty_term thy t = pretty_term' (syn_of thy) (consts_of thy) (Context.Theory thy) t;
 
 fun pretty_typ thy T = Syntax.pretty_typ (Context.Theory thy) (syn_of thy) (extern_typ thy T);
 fun pretty_sort thy S = Syntax.pretty_sort (Context.Theory thy) (syn_of thy) (extern_sort thy S);
@@ -405,11 +405,10 @@
 val certify_typ_abbrev = certify Type.cert_typ_abbrev;
 
 
-(* certify_term *)
+(* certify term/prop *)
 
 local
 
-(*determine and check the type of a term*)
 fun type_check pp tm =
   let
     fun err_appl why bs t T u U =
@@ -434,37 +433,37 @@
                 if T1 = U then T2 else err_appl "Incompatible operand type" bs t T u U
             | _ => err_appl "Operator not of function type" bs t T u U)
           end;
+  in typ_of ([], tm) end;
 
-  in typ_of ([], tm) end;
+fun err msg = raise TYPE (msg, [], []);
+
+fun check_vars (t $ u) = (check_vars t; check_vars u)
+  | check_vars (Abs (_, _, t)) = check_vars t
+  | check_vars (Var (xi as (_, i), _)) =
+      if i < 0 then err ("Malformed variable: " ^ quote (Term.string_of_vname xi)) else ()
+  | check_vars _ = ();
 
 in
 
-fun certify_term pp thy tm =
+fun certify normalize prop pp thy tm =
   let
     val _ = Context.check_thy thy;
-
-    fun check_vars (t $ u) = (check_vars t; check_vars u)
-      | check_vars (Abs (_, _, t)) = check_vars t
-      | check_vars (t as Var ((x, i), _)) =
-          if i < 0 then raise TYPE ("Malformed variable: " ^ quote x, [], [t]) else ()
-      | check_vars _ = ();
+    val _ = check_vars tm;
+    val tm' = Term.map_term_types (certify_typ thy) tm;
+    val T = type_check pp tm';
+    val _ = if prop andalso T <> propT then err "Term not of type prop" else ();
+    val tm'' = Consts.certify pp (tsig_of thy) (consts_of thy) tm';
+    val tm'' = if normalize then tm'' else tm';
+  in (if tm = tm'' then tm else tm'', T, Term.maxidx_of_term tm'') end;
 
-    val tm' = tm
-      |> map_term_types (certify_typ thy)
-      |> Consts.certify pp (tsig_of thy) (consts_of thy)
-      |> tap check_vars;
-    val tm' = if tm = tm' then tm else tm';  (*avoid copying of already normal term*)
-  in (tm', type_check pp tm', maxidx_of_term tm') end;
+fun certify_term thy = certify true false (pp thy) thy;
+fun certify_prop thy = certify true true (pp thy) thy;
+
+val cert_term = #1 oo certify_term;
+val cert_prop = #1 oo certify_prop;
 
 end;
 
-fun certify_prop pp thy tm =
-  let val res as (tm', T, _) = certify_term pp thy tm
-  in if T <> propT then raise TYPE ("Term not of type prop", [T], [tm']) else res end;
-
-fun cert_term thy tm = #1 (certify_term (pp thy) thy tm);
-fun cert_prop thy tm = #1 (certify_prop (pp thy) thy tm);
-
 
 (* specifications *)
 
@@ -538,11 +537,7 @@
     | _ => error ("Undeclared type constructor: " ^ quote c))
   end;
 
-fun read_const thy raw_c =
-  let
-    val c = intern_const thy raw_c;
-    val _ = the_const_type thy c handle TYPE (msg, _, _) => error msg;
-  in Const (c, dummyT) end;
+val read_const = Consts.read_const o consts_of;
 
 
 
@@ -558,15 +553,16 @@
   typs: expected types
 *)
 
-fun infer_types_simult pp thy def_type def_sort used freeze args =
+fun infer_types_simult pp thy consts def_type def_sort used freeze args =
   let
     val termss = fold_rev (multiply o fst) args [[]];
     val typs =
       map (fn (_, T) => certify_typ thy T handle TYPE (msg, _, _) => error msg) args;
 
     fun infer ts = Result (TypeInfer.infer_types (Syntax.pp_show_brackets pp) (tsig_of thy)
-        (const_constraint thy) def_type def_sort (intern_const thy) (intern_tycons thy)
-        (intern_sort thy) used freeze typs ts)
+        (try (Consts.constraint consts)) def_type def_sort
+        (NameSpace.intern (Consts.space_of consts))
+        (intern_tycons thy) (intern_sort thy) used freeze typs ts)
       handle TYPE (msg, _, _) => Exn (ERROR msg);
 
     val err_results = map infer termss;
@@ -590,22 +586,23 @@
       cat_lines (map (Pretty.string_of_term pp) (List.concat (map fst results)))))
   end;
 
-fun infer_types pp thy def_type def_sort used freeze tsT =
-  apfst hd (infer_types_simult pp thy def_type def_sort used freeze [tsT]);
+fun infer_types pp thy consts def_type def_sort used freeze tsT =
+  apfst hd (infer_types_simult pp thy consts def_type def_sort used freeze [tsT]);
 
 
 (* read_def_terms -- read terms and infer types *)    (*exception ERROR*)
 
-fun read_def_terms' pp is_logtype syn context (types, sorts) used freeze sTs =
+fun read_def_terms' pp is_logtype syn consts context (types, sorts) used freeze sTs =
   let
     val thy = Context.theory_of context;
     fun read (s, T) =
       let val T' = certify_typ thy T handle TYPE (msg, _, _) => error msg
       in (Syntax.read context is_logtype syn T' s, T') end;
-  in infer_types_simult pp thy types sorts used freeze (map read sTs) end;
+  in infer_types_simult pp thy consts types sorts used freeze (map read sTs) end;
 
 fun read_def_terms (thy, types, sorts) =
-  read_def_terms' (pp thy) (is_logtype thy) (syn_of thy) (Context.Theory thy) (types, sorts);
+  read_def_terms' (pp thy) (is_logtype thy) (syn_of thy) (consts_of thy)
+    (Context.Theory thy) (types, sorts);
 
 fun simple_read_term thy T s =
   let val ([t], _) = read_def_terms (thy, K NONE, K NONE) [] true [(s, T)]
@@ -731,7 +728,7 @@
 
 local
 
-fun gen_add_abbrevs prep_term raw_args thy =
+fun gen_add_abbrevs prep_term revert raw_args thy =
   let
     val prep_tm =
       Compress.term thy o Logic.varify o no_vars (pp thy) o Term.no_dummy_patterns o prep_term thy;
@@ -744,7 +741,7 @@
     val (abbrs, syn) = split_list (map prep raw_args);
   in
     thy
-    |> map_consts (fold (Consts.abbreviate (pp thy) (tsig_of thy) (naming_of thy)) abbrs)
+    |> map_consts (fold (Consts.abbreviate (pp thy) (tsig_of thy) (naming_of thy) revert) abbrs)
     |> add_syntax_i syn
   end;