src/Pure/defs.ML
changeset 17994 6a1a49cba5b3
parent 17803 e235a57651a1
child 19025 596fb1eb7856
     1.1 --- a/src/Pure/defs.ML	Thu Oct 27 13:54:40 2005 +0200
     1.2 +++ b/src/Pure/defs.ML	Thu Oct 27 13:54:42 2005 +0200
     1.3 @@ -9,7 +9,6 @@
     1.4  signature DEFS =
     1.5  sig
     1.6    type T
     1.7 -  val monomorphic: T -> string -> bool
     1.8    val define: (string -> typ) -> string -> string * typ -> (string * typ) list -> T -> T
     1.9    val empty: T
    1.10    val merge: Pretty.pp -> T * T -> T
    1.11 @@ -22,16 +21,10 @@
    1.12  
    1.13  datatype T = Defs of
    1.14   {consts: typ Graph.T,                                 (*constant declarations and dependencies*)
    1.15 -  specified: (string * typ) Inttab.table Symtab.table, (*specification name and const type*)
    1.16 -  monomorphic: unit Symtab.table};                     (*constants having monomorphic specs*)
    1.17 -
    1.18 -fun rep_defs (Defs args) = args;
    1.19 +  specified: (string * typ) Inttab.table Symtab.table}; (*specification name and const type*)
    1.20  
    1.21 -fun make_defs (consts, specified, monomorphic) =
    1.22 -  Defs {consts = consts, specified = specified, monomorphic = monomorphic};
    1.23 -
    1.24 -fun map_defs f (Defs {consts, specified, monomorphic}) =
    1.25 -  make_defs (f (consts, specified, monomorphic));
    1.26 +fun make_defs (consts, specified) = Defs {consts = consts, specified = specified};
    1.27 +fun map_defs f (Defs {consts, specified}) = make_defs (f (consts, specified));
    1.28  
    1.29  
    1.30  (* specified consts *)
    1.31 @@ -46,29 +39,13 @@
    1.32        " for constant " ^ quote c));
    1.33  
    1.34  
    1.35 -(* monomorphic constants *)
    1.36 -
    1.37 -val monomorphic = Symtab.defined o #monomorphic o rep_defs;
    1.38 -
    1.39 -fun update_monomorphic specified c =
    1.40 -  let
    1.41 -    val specs = the_default Inttab.empty (Symtab.lookup specified c);
    1.42 -    fun is_monoT (Type (_, Ts)) = forall is_monoT Ts
    1.43 -      | is_monoT _ = false;
    1.44 -    val is_mono =
    1.45 -      Inttab.is_empty specs orelse
    1.46 -        Inttab.min_key specs = Inttab.max_key specs andalso
    1.47 -        is_monoT (snd (the (Inttab.lookup specs (the (Inttab.min_key specs)))));
    1.48 -  in if is_mono then Symtab.update (c, ()) else Symtab.remove (K true) (c, ()) end;
    1.49 -
    1.50 -
    1.51  (* define consts *)
    1.52  
    1.53  fun err_cyclic cycles =
    1.54    error ("Cyclic dependency of constants:\n" ^
    1.55      cat_lines (map (space_implode " -> " o map quote o rev) cycles));
    1.56  
    1.57 -fun define const_type name lhs rhs = map_defs (fn (consts, specified, monomorphic) =>
    1.58 +fun define const_type name lhs rhs = map_defs (fn (consts, specified) =>
    1.59    let
    1.60      fun declare (a, _) = Graph.default_node (a, const_type a);
    1.61      fun add_deps (a, bs) G = Graph.add_deps_acyclic (a, bs) G
    1.62 @@ -85,25 +62,22 @@
    1.63        |> Symtab.default (c, Inttab.empty)
    1.64        |> Symtab.map_entry c (fn specs =>
    1.65          (check_specified c spec specs; Inttab.update spec specs));
    1.66 -    val monomorphic' = monomorphic |> update_monomorphic specified' c;
    1.67 -  in (consts', specified', monomorphic') end);
    1.68 +  in (consts', specified') end);
    1.69  
    1.70  
    1.71  (* empty and merge *)
    1.72  
    1.73 -val empty = make_defs (Graph.empty, Symtab.empty, Symtab.empty);
    1.74 +val empty = make_defs (Graph.empty, Symtab.empty);
    1.75  
    1.76  fun merge pp
    1.77 -   (Defs {consts = consts1, specified = specified1, monomorphic},
    1.78 -    Defs {consts = consts2, specified = specified2, ...}) =
    1.79 +   (Defs {consts = consts1, specified = specified1},
    1.80 +    Defs {consts = consts2, specified = specified2}) =
    1.81    let
    1.82      val consts' = (consts1, consts2) |> Graph.merge_acyclic (K true)
    1.83        handle Graph.CYCLES cycles => err_cyclic cycles;
    1.84      val specified' = (specified1, specified2) |> Symtab.join (fn c => fn (orig_specs1, specs2) =>
    1.85        SOME (Inttab.fold (fn spec2 => fn specs1 =>
    1.86          (check_specified c spec2 orig_specs1; Inttab.update spec2 specs1)) specs2 orig_specs1));
    1.87 -    val monomorphic' = monomorphic
    1.88 -      |> Symtab.fold (update_monomorphic specified' o #1) specified';
    1.89 -  in make_defs (consts', specified', monomorphic') end;
    1.90 +  in make_defs (consts', specified') end;
    1.91  
    1.92  end;