src/Pure/defs.ML
changeset 16743 21dbff595bf6
parent 16384 90c51c932154
child 16766 ea667a5426fe
     1.1 --- a/src/Pure/defs.ML	Thu Jul 07 18:38:00 2005 +0200
     1.2 +++ b/src/Pure/defs.ML	Thu Jul 07 19:01:04 2005 +0200
     1.3 @@ -35,6 +35,10 @@
     1.4    val set_chain_history : bool -> unit
     1.5    val chain_history : unit -> bool
     1.6  
     1.7 +  datatype overloadingstate = Open | Closed | Final
     1.8 +  val overloading_info : graph -> string -> (typ * (string*typ) list * overloadingstate) option
     1.9 +  val is_overloaded : graph -> string -> bool
    1.10 +
    1.11  end
    1.12  
    1.13  structure Defs :> DEFS = struct
    1.14 @@ -42,7 +46,7 @@
    1.15  type tyenv = Type.tyenv
    1.16  type edgelabel = (int * typ * typ * (typ * string * string) list)
    1.17  
    1.18 -datatype forwardstate = Open | Closed | Final
    1.19 +datatype overloadingstate = Open | Closed | Final
    1.20  
    1.21  datatype node = Node of
    1.22           typ  (* most general type of constant *)
    1.23 @@ -53,7 +57,7 @@
    1.24               (* a table of all back referencing defnodes to this node, 
    1.25                  indexed by node name of the defnodes *)
    1.26           * typ list (* a list of all finalized types *)
    1.27 -         * forwardstate
    1.28 +         * overloadingstate
    1.29       
    1.30       and defnode = Defnode of
    1.31           typ  (* type of the constant in this particular definition *)
    1.32 @@ -653,6 +657,21 @@
    1.33            Symtab.update_new ((name, ftys), finals)) 
    1.34        (Symtab.empty, graph)
    1.35  
    1.36 +fun overloading_info (_, axmap, _, graph) c = 
    1.37 +    let
    1.38 +      fun translate (ax, Defnode (ty, _)) = (the (Symtab.lookup (axmap, ax)), ty)
    1.39 +    in
    1.40 +      case Symtab.lookup (graph, c) of
    1.41 +        NONE => NONE
    1.42 +      | SOME (Node (ty, defnodes, _, _, state)) =>
    1.43 +        SOME (ty, map translate (Symtab.dest defnodes), state)
    1.44 +    end
    1.45 +      
    1.46 +fun is_overloaded g c = 
    1.47 +    case overloading_info g c of
    1.48 +      NONE => false
    1.49 +    | SOME (_, l, _) => length l >= 2
    1.50 +
    1.51  end;
    1.52  		
    1.53  (*