src/Pure/sign.ML

   type sg
   type sg_ref
   type data
   val rep_sg: sg ->
    {self: sg_ref,
-    tsig: Type.type_sig,
-    const_tab: typ Symtab.table,
+    tsig: Type.tsig,
+    consts: (typ * stamp) Symtab.table,
     path: string list option,
     spaces: (string * NameSpace.T) list,
     data: data}
   val name_of: sg -> string
   val stamp_names_of: sg -> string list
   val exists_stamp: string -> sg -> bool
-  val tsig_of: sg -> Type.type_sig
+  val tsig_of: sg -> Type.tsig
   val deref: sg_ref -> sg
   val self_ref: sg -> sg_ref
   val subsig: sg * sg -> bool
   val joinable: sg * sg -> bool
   val eq_sg: sg * sg -> bool

   val const_type: sg -> string -> typ option
   val classes: sg -> class list
   val defaultS: sg -> sort
   val subsort: sg -> sort * sort -> bool
   val nodup_vars: term -> term
-  val norm_sort: sg -> sort -> sort
   val of_sort: sg -> typ * sort -> bool
   val witness_sorts: sg -> sort list -> sort list -> (typ * sort) list
-  val univ_witness: sg -> (typ * sort) option
+  val universal_witness: sg -> (typ * sort) option
   val typ_instance: sg -> typ * typ -> bool
   val classK: string
   val typeK: string
   val constK: string
   val full_name: sg -> bstring -> string

   val pprint_term: sg -> term -> pprint_args -> unit
   val pprint_typ: sg -> typ -> pprint_args -> unit
   val certify_class: sg -> class -> class
   val certify_sort: sg -> sort -> sort
   val certify_typ: sg -> typ -> typ
-  val certify_typ_no_norm: sg -> typ -> typ
-  val certify_tycon: sg -> string -> string
-  val certify_tyabbr: sg -> string -> string
+  val certify_typ_raw: sg -> typ -> typ
   val certify_tyname: sg -> string -> string
   val certify_const: sg -> string -> string
   val certify_term: sg -> term -> term * typ * int
   val read_sort: sg -> string -> sort
   val read_raw_typ: sg * (indexname -> sort option) -> string -> typ
   val read_typ: sg * (indexname -> sort option) -> string -> typ
   val read_typ': Syntax.syntax -> sg * (indexname -> sort option) -> string -> typ
-  val read_typ_no_norm': Syntax.syntax -> sg * (indexname -> sort option) -> string -> typ
+  val read_typ_raw': Syntax.syntax -> sg * (indexname -> sort option) -> string -> typ
   val infer_types: sg -> (indexname -> typ option) ->
     (indexname -> sort option) -> string list -> bool
     -> xterm list * typ -> term * (indexname * typ) list
   val infer_types_simult: sg -> (indexname -> typ option) ->
     (indexname -> sort option) -> string list -> bool

   Sg of
    {id: string ref,                             (*id*)
     stamps: string ref list,                    (*unique theory indentifier*)
     syn: syn} *                                 (*syntax for parsing and printing*)
    {self: sg_ref,                               (*mutable self reference*)
-    tsig: Type.type_sig,                        (*order-sorted signature of types*)
-    const_tab: typ Symtab.table,                (*type schemes of constants*)
+    tsig: Type.tsig,                            (*order-sorted signature of types*)
+    consts: (typ * stamp) Symtab.table,         (*type schemes of constants*)
     path: string list option,                   (*current name space entry prefix*)
     spaces: (string * NameSpace.T) list,        (*name spaces for consts, types etc.*)
     data: data}                                 (*anytype data*)
 and data =
   Data of

       ((sg -> ast list -> ast) * stamp) list Symtab.table)
 and sg_ref =
   SgRef of sg ref option;
 
 (*make signature*)
-fun make_sign (id, self, tsig, const_tab, syn, path, spaces, data, stamps) =
+fun make_sign (id, self, tsig, consts, syn, path, spaces, data, stamps) =
   Sg ({id = id, stamps = stamps, syn = syn}, {self = self, tsig = tsig,
-    const_tab = const_tab, path = path, spaces = spaces, data = data});
+    consts = consts, path = path, spaces = spaces, data = data});
 
 
 (* basic operations *)
 
 fun rep_sg (Sg (_, args)) = args;

 fun pretty_sg sg = Pretty.str_list "{" "}" (stamp_names_of sg);
 val str_of_sg = Pretty.str_of o pretty_sg;
 val pprint_sg = Pretty.pprint o pretty_sg;
 
 val tsig_of = #tsig o rep_sg;
-fun const_type (Sg (_, {const_tab, ...})) c = Symtab.lookup (const_tab, c);
+fun const_type (Sg (_, {consts, ...})) c = apsome #1 (Symtab.lookup (consts, c));
 
 
 (* id and self *)
 
 fun check_stale (sg as Sg ({id, ...},

 (* classes and sorts *)
 
 val classes = Type.classes o tsig_of;
 val defaultS = Type.defaultS o tsig_of;
 val subsort = Type.subsort o tsig_of;
-val norm_sort = Type.norm_sort o tsig_of;
 val of_sort = Type.of_sort o tsig_of;
 val witness_sorts = Type.witness_sorts o tsig_of;
-val univ_witness = Type.univ_witness o tsig_of;
-fun typ_instance sg (T, U) = Type.typ_instance (tsig_of sg, T, U);
+val universal_witness = Type.universal_witness o tsig_of;
+val typ_instance = Type.typ_instance o tsig_of;
 
 
 (** signature data **)
 
 (* errors *)

 
 fun err_dup_init sg kind =
   error ("Duplicate initialization of " ^ quote kind ^ " data" ^ of_theory sg);
 
 fun err_uninit sg kind =
-  error ("Tried to access uninitialized " ^ quote kind ^ " data" ^
-         of_theory sg);
+  error ("Tried to access uninitialized " ^ quote kind ^ " data" ^ of_theory sg);
 
 (*Trying to access theory data using get / put operations from a different
   instance of the TheoryDataFun result.  Typical cure: re-load all files*)
 fun err_access sg kind =
   error ("Unauthorized access to " ^ quote kind ^ " data" ^ of_theory sg);

     | _ => sys_error "Sign.create_sign");
     sign
   end;
 
 fun extend_sign keep extfun name decls
-    (sg as Sg ({id = _, stamps, syn}, {self, tsig, const_tab, path, spaces, data})) =
+    (sg as Sg ({id = _, stamps, syn}, {self, tsig, consts, path, spaces, data})) =
   let
     val _ = check_stale sg;
     val (self', data') =
       if is_draft sg andalso keep then (self, data)
       else (SgRef (Some (ref sg)), prep_ext_data data);
   in
     create_sign self' stamps name
-      (extfun sg (syn, tsig, const_tab, (path, spaces), data') decls)
+      (extfun sg (syn, tsig, consts, (path, spaces), data') decls)
   end;
 
 
 
 (** name spaces **)

 fun add_names x = change_space NameSpace.extend x;
 fun hide_names b x = change_space (NameSpace.hide b) x;
 
 (*make full names*)
 fun full _ "" = error "Attempt to declare empty name \"\""
-  | full None name = name
-  | full (Some path) name =
-      if NameSpace.is_qualified name then
-        error ("Attempt to declare qualified name " ^ quote name)
+  | full None bname = bname
+  | full (Some path) bname =
+      if NameSpace.is_qualified bname then
+        error ("Attempt to declare qualified name " ^ quote bname)
       else
-       (if not (Syntax.is_identifier name)
-        then warning ("Declared non-identifier name " ^ quote name) else ();
-        NameSpace.pack (path @ [name]));
+        let val name = NameSpace.pack (path @ [bname]) in
+          if Syntax.is_identifier bname then ()
+          else warning ("Declared non-identifier " ^ quote name); name
+        end;
 
 (*base name*)
 val base_name = NameSpace.base;
 
 

 (** partial Pure signature **)
 
 val pure_syn =
   Syn (Syntax.pure_syn, (Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty));
 
-val dummy_sg = make_sign (ref "", SgRef None, Type.tsig0,
+val dummy_sg = make_sign (ref "", SgRef None, Type.empty_tsig,
   Symtab.empty, pure_syn, Some [], [], empty_data, []);
 
 val pre_pure =
   create_sign (SgRef (Some (ref dummy_sg))) [] "#"
-    (pure_syn, Type.tsig0, Symtab.empty, (Some [], []), empty_data);
+    (pure_syn, Type.empty_tsig, Symtab.empty, (Some [], []), empty_data);
 
 val PureN = "Pure";
 val CPureN = "CPure";
 
 

 
 fun err_in_type s =
   error ("The error(s) above occurred in type " ^ quote s);
 
 fun rd_raw_typ syn tsig spaces def_sort str =
-  intrn_tycons spaces
-    (Syntax.read_typ syn (Type.get_sort tsig def_sort (intrn_sort spaces)) (intrn_sort spaces) str
+  intrn_tycons spaces (Syntax.read_typ syn
+    (TypeInfer.get_sort tsig def_sort (intrn_sort spaces)) (intrn_sort spaces) str
       handle ERROR => err_in_type str);
 
 fun read_raw_typ' syn (sg as Sg (_, {tsig, spaces, ...}), def_sort) str =
   (check_stale sg; rd_raw_typ syn tsig spaces def_sort str);
 

 local
   fun read_typ_aux rd cert (sg, def_sort) str =
     (cert (tsig_of sg) (rd (sg, def_sort) str)
       handle TYPE (msg, _, _) => (error_msg msg; err_in_type str));
 in
-  val read_typ              = read_typ_aux read_raw_typ Type.cert_typ;
-  val read_typ_no_norm      = read_typ_aux read_raw_typ Type.cert_typ_no_norm;
-  fun read_typ' syn         = read_typ_aux (read_raw_typ' syn) Type.cert_typ;
-  fun read_typ_no_norm' syn = read_typ_aux (read_raw_typ' syn) Type.cert_typ_no_norm;
+  val read_typ          = read_typ_aux read_raw_typ Type.cert_typ;
+  val read_typ_raw      = read_typ_aux read_raw_typ Type.cert_typ_raw;
+  fun read_typ' syn     = read_typ_aux (read_raw_typ' syn) Type.cert_typ;
+  fun read_typ_raw' syn = read_typ_aux (read_raw_typ' syn) Type.cert_typ_raw;
 end;
 
 
 
 (** certify classes, sorts, types and terms **)   (*exception TYPE*)
 
 val certify_class = Type.cert_class o tsig_of;
 val certify_sort = Type.cert_sort o tsig_of;
 val certify_typ = Type.cert_typ o tsig_of;
-val certify_typ_no_norm = Type.cert_typ_no_norm o tsig_of;
-
-fun certify_tycon sg c =
-  if is_some (Symtab.lookup (#tycons (Type.rep_tsig (tsig_of sg)), c)) then c
-  else raise TYPE ("Undeclared type constructor " ^ quote c, [], []);
-
-fun certify_tyabbr sg c =
-  if is_some (Symtab.lookup (#abbrs (Type.rep_tsig (tsig_of sg)), c)) then c
-  else raise TYPE ("Unknown type abbreviation " ^ quote c, [], []);
+val certify_typ_raw = Type.cert_typ_raw o tsig_of;
 
 fun certify_tyname sg c =
-  certify_tycon sg c handle TYPE _ => certify_tyabbr sg c handle TYPE _ =>
-    raise TYPE ("Unknown type name " ^ quote c, [], []);
+  if is_some (Symtab.lookup (#types (Type.rep_tsig (tsig_of sg)), c)) then c
+  else raise TYPE ("Undeclared type constructor: " ^ quote c, [], []);
 
 fun certify_const sg c =
-  if is_some (const_type sg c) then c else raise TYPE ("Undeclared constant " ^ quote c, [], []);
+  if is_some (const_type sg c) then c
+  else raise TYPE ("Undeclared constant: " ^ quote c, [], []);
 
 
 (* certify_term *)
 
 (*check for duplicate occurrences of TFree/TVar with distinct sorts*)

             | _ => err_appl "Operator not of function type." bs t T u U)
           end;
 
   in typ_of ([], tm) end;
 
-
 fun certify_term sg tm =
   let
     val _ = check_stale sg;
-    val tsig = tsig_of sg;
+
+    val tm' = Term.map_term_types (Type.cert_typ (tsig_of sg)) tm;
+    val tm' = if tm = tm' then tm else tm';  (*avoid copying of already normal term*)
+
+    fun err msg = raise TYPE (msg, [], [tm']);
 
     fun show_const a T = quote a ^ " :: " ^ quote (string_of_typ sg T);
 
-    fun atom_err (errs, Const (a, T)) =
-        (case const_type sg a of
-          None => ("Undeclared constant " ^ show_const a T) :: errs
-        | Some U =>
-            if typ_instance sg (T, U) then errs
-            else ("Illegal type for constant " ^ show_const a T) :: errs)
-      | atom_err (errs, Var ((x, i), _)) =
-          if i < 0 then ("Negative index for Var " ^ quote x) :: errs else errs
-      | atom_err (errs, _) = errs;
-
-    val norm_tm =
-      (case it_term_types (Type.typ_errors tsig) (tm, []) of
-        [] => Type.norm_term tsig tm
-      | errs => raise TYPE (cat_lines errs, [], [tm]));
-    val _ = nodup_vars norm_tm;
+    fun check_atoms (t $ u) = (check_atoms t; check_atoms u)
+      | check_atoms (Abs (_, _, t)) = check_atoms t
+      | check_atoms (Const (a, T)) =
+          (case const_type sg a of
+            None => err ("Undeclared constant " ^ show_const a T)
+          | Some U =>
+              if typ_instance sg (T, U) then ()
+              else err ("Illegal type for constant " ^ show_const a T))
+      | check_atoms (Var ((x, i), _)) =
+          if i < 0 then err ("Malformed variable: " ^ quote x) else ()
+      | check_atoms _ = ();
   in
-    (case foldl_aterms atom_err ([], norm_tm) of
-      [] => (norm_tm, type_check sg norm_tm, maxidx_of_term norm_tm)
-    | errs => raise TYPE (cat_lines errs, [], [norm_tm]))
-  end;
+    check_atoms tm';
+    nodup_vars tm';
+    (tm', type_check sg tm', maxidx_of_term tm')
+  end;
+
 
 
 (** infer_types **)         (*exception ERROR*)
 
 (*

     val termss = foldr multiply (map fst args, [[]]);
     val typs =
       map (fn (_, T) => certify_typ sg T handle TYPE (msg, _, _) => error msg) args;
 
     fun infer ts = OK
-      (Type.infer_types prt prT tsig (const_type sg) def_type def_sort
+      (TypeInfer.infer_types prt prT tsig (const_type sg) def_type def_sort
         (intern_const sg) (intern_tycons sg) (intern_sort sg) used freeze typs ts)
       handle TYPE (msg, _, _) => Error msg;
 
     val err_results = map infer termss;
     val errs = mapfilter get_error err_results;

 
 
 (* add default sort *)
 
 fun ext_defS prep_sort sg (syn, tsig, ctab, (path, spaces), data) S =
-  (syn, Type.ext_tsig_defsort tsig (prep_sort sg syn tsig spaces S),
+  (syn, Type.set_defsort (prep_sort sg syn tsig spaces S) tsig,
     ctab, (path, spaces), data);
 
 fun ext_defsort arg = ext_defS rd_sort arg;
 fun ext_defsort_i arg = ext_defS cert_sort arg;
 

 (* add type constructors *)
 
 fun ext_types _ (syn, tsig, ctab, (path, spaces), data) types =
   let val decls = decls_of path Syntax.type_name types in
     (map_syntax (Syntax.extend_type_gram types) syn,
-      Type.ext_tsig_types tsig decls, ctab,
+      Type.add_types decls tsig, ctab,
       (path, add_names spaces typeK (map fst decls)), data)
   end;
-
-fun ext_nonterminals sign sg nonterms =
-  ext_types sign sg (map (fn n => (n, 0, Syntax.NoSyn)) nonterms);
 
 
 (* add type abbreviations *)
 
 fun read_abbr sg syn tsig spaces (t, vs, rhs_src) =

       map (fn (t, vs, rhs, mx) =>
         (full path (Syntax.type_name t mx), vs, rhs)) abbrs;
     val spaces' = add_names spaces typeK (map #1 abbrs');
     val decls = map (rd_abbr sg syn' tsig spaces') abbrs';
   in
-    (syn', Type.ext_tsig_abbrs tsig decls, ctab, (path, spaces'), data)
+    (syn', Type.add_abbrs decls tsig, ctab, (path, spaces'), data)
   end;
 
 fun ext_tyabbrs abbrs = ext_abbrs read_abbr abbrs;
 fun ext_tyabbrs_i abbrs = ext_abbrs no_read abbrs;
+
+
+(* add nonterminals *)
+
+fun ext_nonterminals _ (syn, tsig, ctab, (path, spaces), data) bnames =
+  let val names = map (full path) bnames in
+    (map_syntax (Syntax.extend_consts names) syn,
+      Type.add_nonterminals names tsig, ctab,
+      (path, add_names spaces typeK names), data)
+  end;
 
 
 (* add type arities *)
 
 fun ext_ars int prep_sort sg (syn, tsig, ctab, (path, spaces), data) arities =
   let
     val prepS = prep_sort sg syn tsig spaces;
     fun prep_arity (c, Ss, S) =
       (if int then intrn spaces typeK c else c, map prepS Ss, prepS S);
-    val tsig' = Type.ext_tsig_arities tsig (map prep_arity arities);
+    val tsig' = Type.add_arities (map prep_arity arities) tsig;
     val log_types = Type.logical_types tsig';
   in
     (map_syntax (Syntax.extend_log_types log_types) syn,
       tsig', ctab, (path, spaces), data)
   end;

     handle ERROR => err_in_const (const_name path c mx);
 
 fun ext_cnsts rd_const syn_only prmode sg (syn, tsig, ctab, (path, spaces), data)
     raw_consts =
   let
-    fun prep_const (c, ty, mx) =
-      (c, compress_type (Type.varifyT (Type.cert_typ tsig (Type.no_tvars ty))), mx)
-        handle TYPE (msg, _, _) =>
-          (error_msg msg; err_in_const (const_name path c mx));
+    val prep_typ = compress_type o Type.varifyT o Type.no_tvars o
+      (if syn_only then Type.cert_typ_syntax tsig else Term.no_dummyT o Type.cert_typ tsig);
+    fun prep_const (c, ty, mx) = (c, prep_typ ty, mx) handle TYPE (msg, _, _) =>
+      (error_msg msg; err_in_const (const_name path c mx));
 
     val consts = map (prep_const o rd_const sg syn tsig (path, spaces)) raw_consts;
     val decls =
       if syn_only then []
       else decls_of path Syntax.const_name consts;
   in
     (map_syntax (Syntax.extend_const_gram prmode consts) syn, tsig,
-      Symtab.extend (ctab, decls)
+      Symtab.extend (ctab, map (fn (c, T) => (c, (T, stamp ()))) decls)
         handle Symtab.DUPS cs => err_dup_consts cs,
       (path, add_names spaces constK (map fst decls)), data)
   end;
 
 fun ext_consts_i x = ext_cnsts no_read false ("", true) x;

     val classes' =
       ListPair.map (fn (c, (_, cs)) => (c, intrn cs)) (full_names, classes);
   in
     ext_consts_i sg
       (map_syntax (Syntax.extend_consts names) syn,
-        Type.ext_tsig_classes tsig classes', ctab, (path, spaces'), data)
+        Type.add_classes classes' tsig, ctab, (path, spaces'), data)
     consts
   end;
 
 
 (* add to classrel *)
 
 fun ext_classrel int _ (syn, tsig, ctab, (path, spaces), data) pairs =
   let val intrn = if int then map (pairself (intrn_class spaces)) else I in
-    (syn, Type.ext_tsig_classrel tsig (intrn pairs), ctab, (path, spaces), data)
+    (syn, Type.add_classrel (intrn pairs) tsig, ctab, (path, spaces), data)
   end;
 
 
 (* add translation functions *)
 

 
 
 fun copy_data (k, (e, mths as (cp, _, _, _))) =
   (k, (cp e handle exn => err_method "copy" (Object.name_of_kind k) exn, mths));
 
-fun copy (sg as Sg ({id = _, stamps, syn}, {self, tsig, const_tab, path, spaces, data})) =
+fun copy (sg as Sg ({id = _, stamps, syn}, {self, tsig, consts, path, spaces, data})) =
   let
     val _ = check_stale sg;
     val self' = SgRef (Some (ref sg));
     val Data tab = data;
     val data' = Data (Symtab.map copy_data tab);
-  in create_sign self' stamps "#" (syn, tsig, const_tab, (path, spaces), data') end;
+  in create_sign self' stamps "#" (syn, tsig, consts, (path, spaces), data') end;
 
 
 (* the external interfaces *)
 
 val add_classes          = extend_sign true (ext_classes true) "#";

       exists_stamp CPureN sg1 andalso exists_stamp PureN sg2 then
     raise TERM ("Cannot merge Pure and CPure signatures", [])
   else
     let
       val Sg ({id = _, stamps = stamps1, syn = Syn (syntax1, trfuns1)},
-          {self = _, tsig = tsig1, const_tab = const_tab1,
+          {self = _, tsig = tsig1, consts = consts1,
             path = _, spaces = spaces1, data = data1}) = sg1;
       val Sg ({id = _, stamps = stamps2, syn = Syn (syntax2, trfuns2)},
-          {self = _, tsig = tsig2, const_tab = const_tab2,
+          {self = _, tsig = tsig2, consts = consts2,
             path = _, spaces = spaces2, data = data2}) = sg2;
 
       val id = ref "";
       val self_ref = ref dummy_sg;
       val self = SgRef (Some self_ref);
 
       val stamps = merge_stamps stamps1 stamps2;
       val syntax = Syntax.merge_syntaxes syntax1 syntax2;
       val trfuns = merge_trfuns trfuns1 trfuns2;
       val tsig = Type.merge_tsigs (tsig1, tsig2);
-      val const_tab = Symtab.merge (op =) (const_tab1, const_tab2)
-        handle Symtab.DUPS cs =>
-          raise TERM ("Incompatible types for constant(s) " ^ commas_quote cs, []);
+      val consts = Symtab.merge eq_snd (consts1, consts2)
+        handle Symtab.DUPS cs => err_dup_consts cs;
 
       val path = Some [];
       val kinds = distinct (map fst (spaces1 @ spaces2));
       val spaces =
         kinds ~~
           ListPair.map NameSpace.merge
             (map (space_of spaces1) kinds, map (space_of spaces2) kinds);
 
       val data = merge_data (data1, data2);
 
-      val sign = make_sign (id, self, tsig, const_tab, Syn (syntax, trfuns),
+      val sign = make_sign (id, self, tsig, consts, Syn (syntax, trfuns),
         path, spaces, data, stamps);
     in self_ref := sign; syn_of sign; sign end;
 
 end;