consts: monomorphic;
authorwenzelm
Thu Oct 27 13:54:43 2005 +0200 (2005-10-27)
changeset 179958b9c6af78a67
parent 17994 6a1a49cba5b3
child 17996 71f250e05e05
consts: monomorphic;
src/Pure/display.ML
src/Pure/sign.ML
     1.1 --- a/src/Pure/display.ML	Thu Oct 27 13:54:42 2005 +0200
     1.2 +++ b/src/Pure/display.ML	Thu Oct 27 13:54:43 2005 +0200
     1.3 @@ -201,7 +201,7 @@
     1.4      val clsses = NameSpace.dest_table (apsnd (Symtab.make o Graph.dest) classes);
     1.5      val tdecls = NameSpace.dest_table types;
     1.6      val arties = NameSpace.dest_table (Sign.type_space thy, arities);
     1.7 -    val cnsts = NameSpace.extern_table consts |> map (apsnd fst);
     1.8 +    val cnsts = NameSpace.extern_table consts |> map (apsnd (fst o fst));
     1.9      val cnsts' = NameSpace.extern_table (#1 consts, constraints);
    1.10      val axms = NameSpace.extern_table axioms;
    1.11      val oras = NameSpace.extern_table oracles;
     2.1 --- a/src/Pure/sign.ML	Thu Oct 27 13:54:42 2005 +0200
     2.2 +++ b/src/Pure/sign.ML	Thu Oct 27 13:54:43 2005 +0200
     2.3 @@ -86,7 +86,7 @@
     2.4     {naming: NameSpace.naming,
     2.5      syn: Syntax.syntax,
     2.6      tsig: Type.tsig,
     2.7 -    consts: (typ * stamp) NameSpace.table * typ Symtab.table}
     2.8 +    consts: ((typ * bool) * serial) NameSpace.table * typ Symtab.table}
     2.9    val naming_of: theory -> NameSpace.naming
    2.10    val base_name: string -> bstring
    2.11    val full_name: theory -> bstring -> string
    2.12 @@ -113,6 +113,7 @@
    2.13    val the_const_type: theory -> string -> typ
    2.14    val declared_tyname: theory -> string -> bool
    2.15    val declared_const: theory -> string -> bool
    2.16 +  val monomorphic: theory -> string -> bool
    2.17    val class_space: theory -> NameSpace.T
    2.18    val type_space: theory -> NameSpace.T
    2.19    val const_space: theory -> NameSpace.T
    2.20 @@ -191,12 +192,12 @@
    2.21  (** datatype sign **)
    2.22  
    2.23  datatype sign = Sign of
    2.24 - {naming: NameSpace.naming,                 (*common naming conventions*)
    2.25 -  syn: Syntax.syntax,                       (*concrete syntax for terms, types, sorts*)
    2.26 -  tsig: Type.tsig,                          (*order-sorted signature of types*)
    2.27 + {naming: NameSpace.naming,                   (*common naming conventions*)
    2.28 +  syn: Syntax.syntax,                         (*concrete syntax for terms, types, sorts*)
    2.29 +  tsig: Type.tsig,                            (*order-sorted signature of types*)
    2.30    consts:
    2.31 -    (typ * stamp) NameSpace.table *         (*type schemes of declared term constants*)
    2.32 -    typ Symtab.table};                      (*type constraints for constants*)
    2.33 +    ((typ * bool) * serial) NameSpace.table * (*type schemes of declared term constants*)
    2.34 +    typ Symtab.table};                        (*type constraints for constants*)
    2.35  
    2.36  
    2.37  fun make_sign (naming, syn, tsig, consts) =
    2.38 @@ -286,7 +287,7 @@
    2.39  fun const_constraint thy c =
    2.40    let val ((_, consts), constraints) = #consts (rep_sg thy) in
    2.41      (case Symtab.lookup constraints c of
    2.42 -      NONE => Option.map #1 (Symtab.lookup consts c)
    2.43 +      NONE => Option.map (#1 o #1) (Symtab.lookup consts c)
    2.44      | some => some)
    2.45    end;
    2.46  
    2.47 @@ -294,7 +295,7 @@
    2.48    (case const_constraint thy c of SOME T => T
    2.49    | NONE => raise TYPE ("Undeclared constant " ^ quote c, [], []));
    2.50  
    2.51 -val const_type = Option.map #1 oo (Symtab.lookup o #2 o #1 o #consts o rep_sg);
    2.52 +val const_type = Option.map (#1 o #1) oo (Symtab.lookup o #2 o #1 o #consts o rep_sg);
    2.53  
    2.54  fun the_const_type thy c =
    2.55    (case const_type thy c of SOME T => T
    2.56 @@ -303,6 +304,10 @@
    2.57  val declared_tyname = Symtab.defined o #2 o #types o Type.rep_tsig o tsig_of;
    2.58  val declared_const = is_some oo const_type;
    2.59  
    2.60 +fun monomorphic thy =
    2.61 +  let val mono = Symtab.lookup (#2 (#1 (#consts (rep_sg thy))))
    2.62 +  in fn c => (case mono c of SOME ((_, m), _) => m | _ => false) end;
    2.63 +
    2.64  
    2.65  
    2.66  (** intern / extern names **)
    2.67 @@ -688,13 +693,20 @@
    2.68  
    2.69  (* add constants *)
    2.70  
    2.71 +local
    2.72 +
    2.73 +fun is_mono (Type (_, Ts)) = forall is_mono Ts
    2.74 +  | is_mono _ = false;
    2.75 +
    2.76  fun gen_add_consts prep_typ raw_args thy =
    2.77    let
    2.78      val prepT = Compress.typ thy o Type.varifyT o Type.no_tvars o Term.no_dummyT o prep_typ thy;
    2.79      fun prep (c, T, mx) = ((c, prepT T, mx) handle TYPE (msg, _, _) => error msg)
    2.80        handle ERROR => error ("in declaration of constant " ^ quote (Syntax.const_name c mx));
    2.81      val args = map prep raw_args;
    2.82 -    val decls = args |> map (fn (c, T, mx) => (Syntax.const_name c mx, (T, stamp ())));
    2.83 +
    2.84 +    val decls = args |> map (fn (c, T, mx) =>
    2.85 +      (Syntax.const_name c mx, ((T, is_mono T), serial ())));
    2.86  
    2.87      fun extend_consts consts = NameSpace.extend_table (naming_of thy) (consts, decls)
    2.88        handle Symtab.DUPS cs => err_dup_consts cs;
    2.89 @@ -704,9 +716,13 @@
    2.90      |> add_syntax_i args
    2.91    end;
    2.92  
    2.93 +in
    2.94 +
    2.95  val add_consts = gen_add_consts (read_typ o no_def_sort);
    2.96  val add_consts_i = gen_add_consts certify_typ;
    2.97  
    2.98 +end;
    2.99 +
   2.100  
   2.101  (* add constraints *)
   2.102