- fixed bug concerning the renaming of axiom names
authorobua
Thu Jul 14 14:05:48 2005 +0200 (2005-07-14)
changeset 16826ed53f24149f6
parent 16825 0a28f033de03
child 16827 c90a1f450327
- fixed bug concerning the renaming of axiom names
- introduced new function Defs.fast_overloading_info
src/Pure/defs.ML
     1.1 --- a/src/Pure/defs.ML	Thu Jul 14 10:48:19 2005 +0200
     1.2 +++ b/src/Pure/defs.ML	Thu Jul 14 14:05:48 2005 +0200
     1.3 @@ -36,8 +36,10 @@
     1.4    val chain_history : unit -> bool
     1.5  
     1.6    datatype overloadingstate = Open | Closed | Final
     1.7 +  
     1.8 +
     1.9    val overloading_info : graph -> string -> (typ * (string*typ) list * overloadingstate) option
    1.10 -  val is_overloaded : graph -> string -> bool
    1.11 +  val fast_overloading_info : graph -> string -> (typ * int * overloadingstate) option
    1.12  
    1.13  end
    1.14  
    1.15 @@ -72,7 +74,7 @@
    1.16  fun table_size table = Symtab.foldl (fn (x, _) => x+1) (0, table)
    1.17          
    1.18  datatype graphaction = Declare of string * typ
    1.19 -		     | Define of string * typ * string * (string * typ) list
    1.20 +		     | Define of string * typ * string * string * (string * typ) list
    1.21  		     | Finalize of string * typ
    1.22  
    1.23  type graph = int * (string Symtab.table) * (graphaction list) * (node Symtab.table)
    1.24 @@ -297,7 +299,7 @@
    1.25        | _ => raise x
    1.26      end
    1.27  
    1.28 -fun define' (cost, axmap, actions, graph) (mainref, ty) axname body =
    1.29 +fun define' (cost, axmap, actions, graph) (mainref, ty) axname orig_axname body =
    1.30      let
    1.31        val mainnode  = (case Symtab.lookup (graph, mainref) of 
    1.32  			 NONE => def_err ("constant "^mainref^" is not declared")
    1.33 @@ -517,12 +519,12 @@
    1.34        val (Node (gty, defs, _, finals, closed)) = getnode graph mainref
    1.35        val closed = if closed = Closed andalso no_forwards defs then Final else closed
    1.36        val graph = Symtab.update ((mainref, Node (gty, defs, backs, finals, closed)), graph) 
    1.37 -      val actions' = (Define (mainref, ty, axname, body))::actions
    1.38 +      val actions' = (Define (mainref, ty, axname, orig_axname, body))::actions
    1.39      in	    
    1.40        (cost+3, axmap, actions', graph)
    1.41      end handle ex => translate_ex axmap ex
    1.42      
    1.43 -fun define (g as (cost, axmap, actions, graph)) (mainref, ty) axname body =
    1.44 +fun define (g as (cost, axmap, actions, graph)) (mainref, ty) orig_axname body =
    1.45      let
    1.46        val ty = checkT ty
    1.47        fun checkbody (n, t) = 
    1.48 @@ -534,9 +536,9 @@
    1.49              | _ => SOME (n, checkT t)
    1.50            end
    1.51        val body = distinct (List.mapPartial checkbody body)
    1.52 -      val (axmap, axname) = newaxname axmap axname
    1.53 +      val (axmap, axname) = newaxname axmap orig_axname
    1.54      in
    1.55 -      define' (cost, axmap, actions, graph) (mainref, ty) axname body
    1.56 +      define' (cost, axmap, actions, graph) (mainref, ty) axname orig_axname body
    1.57      end
    1.58  
    1.59  fun finalize' (cost, axmap, history, graph) (noderef, ty) = 
    1.60 @@ -635,13 +637,16 @@
    1.61   
    1.62  fun finalize g (noderef, ty) = finalize' g (noderef, checkT ty) 
    1.63  
    1.64 +fun update_axname ax orig_ax (cost, axmap, history, graph) =
    1.65 +  (cost, Symtab.update ((ax, orig_ax), axmap), history, graph)
    1.66 +
    1.67  fun merge' (Declare cty, g) = declare' g cty
    1.68 -  | merge' (Define (name, ty, axname, body), g as (_,_, _, graph)) = 
    1.69 +  | merge' (Define (name, ty, axname, orig_axname, body), g as (cost, axmap, history, graph)) = 
    1.70      (case Symtab.lookup (graph, name) of
    1.71 -       NONE => define' g (name, ty) axname body
    1.72 +       NONE => define' (update_axname axname orig_axname g) (name, ty) axname orig_axname body
    1.73       | SOME (Node (_, defs, _, _, _)) => 
    1.74         (case Symtab.lookup (defs, axname) of
    1.75 -	  NONE => define' g (name, ty) axname body
    1.76 +	  NONE => define' (update_axname axname orig_axname g) (name, ty) axname orig_axname body
    1.77  	| SOME _ => g))
    1.78    | merge' (Finalize finals, g) = finalize' g finals 
    1.79                         
    1.80 @@ -667,15 +672,14 @@
    1.81          SOME (ty, map translate (Symtab.dest defnodes), state)
    1.82      end
    1.83        
    1.84 -exception Overloaded;
    1.85 -fun is_overloaded (_, _, _, graph) c = 
    1.86 +fun fast_overloading_info (_, _, _, graph) c = 
    1.87      let 
    1.88 -      fun count (c, _) = if c = 1 then raise Overloaded else c+1
    1.89 +      fun count (c, _) = c+1
    1.90      in
    1.91        case Symtab.lookup (graph, c) of
    1.92 -        NONE => false
    1.93 -      | SOME (Node (_, defnodes, _, _, _)) =>
    1.94 -        ((Symtab.foldl count (0, defnodes); false) handle Overloaded => true)
    1.95 +        NONE => NONE
    1.96 +      | SOME (Node (ty, defnodes, _, _, state)) =>
    1.97 +        SOME (ty, Symtab.foldl count (0, defnodes), state)
    1.98      end
    1.99  
   1.100  end;