src/Pure/defs.ML
changeset 17412 e26cb20ef0cc
parent 17223 430edc6b7826
child 17669 94dbbffbf94b
     1.1 --- a/src/Pure/defs.ML	Thu Sep 15 17:16:55 2005 +0200
     1.2 +++ b/src/Pure/defs.ML	Thu Sep 15 17:16:56 2005 +0200
     1.3 @@ -46,11 +46,11 @@
     1.4           typ  (* type of the constant in this particular definition *)
     1.5           * (edgelabel list) Symtab.table (* The edges, grouped by nodes. *)
     1.6  
     1.7 -fun getnode graph = the o Symtab.curried_lookup graph
     1.8 +fun getnode graph = the o Symtab.lookup graph
     1.9  fun get_nodedefs (Node (_, defs, _, _, _)) = defs
    1.10 -fun get_defnode (Node (_, defs, _, _, _)) defname = Symtab.curried_lookup defs defname
    1.11 +fun get_defnode (Node (_, defs, _, _, _)) defname = Symtab.lookup defs defname
    1.12  fun get_defnode' graph noderef =
    1.13 -  Symtab.curried_lookup (get_nodedefs (the (Symtab.curried_lookup graph noderef)))
    1.14 +  Symtab.lookup (get_nodedefs (the (Symtab.lookup graph noderef)))
    1.15  
    1.16  fun table_size table = Symtab.fold (K (fn x => x + 1)) table 0;
    1.17  
    1.18 @@ -94,7 +94,7 @@
    1.19          val tv = typ_tvars t
    1.20          val t' = Logic.incr_tvar inc t
    1.21          fun update_subst ((n, i), _) =
    1.22 -          Vartab.curried_update ((n, i), ([], TVar ((n, i + inc), [])));
    1.23 +          Vartab.update ((n, i), ([], TVar ((n, i + inc), [])));
    1.24        in
    1.25          (t', fold update_subst tv Vartab.empty)
    1.26        end
    1.27 @@ -157,9 +157,9 @@
    1.28              ((tab,max), []) ts
    1.29  
    1.30        fun idx (tab,max) (TVar ((a,i),_)) =
    1.31 -          (case Inttab.curried_lookup tab i of
    1.32 +          (case Inttab.lookup tab i of
    1.33               SOME j => ((tab, max), TVar ((a,j),[]))
    1.34 -           | NONE => ((Inttab.curried_update (i, max) tab, max + 1), TVar ((a,max),[])))
    1.35 +           | NONE => ((Inttab.update (i, max) tab, max + 1), TVar ((a,max),[])))
    1.36          | idx (tab,max) (Type (t, ts)) =
    1.37            let
    1.38              val ((tab, max), ts) = idxlist idx I fst (tab, max) ts
    1.39 @@ -207,10 +207,10 @@
    1.40  
    1.41  fun declare' (g as (cost, axmap, actions, graph)) (cty as (name, ty)) =
    1.42      (cost, axmap, (Declare cty)::actions,
    1.43 -     Symtab.curried_update_new (name, Node (ty, Symtab.empty, Symtab.empty, [], Open)) graph)
    1.44 +     Symtab.update_new (name, Node (ty, Symtab.empty, Symtab.empty, [], Open)) graph)
    1.45      handle Symtab.DUP _ =>
    1.46             let
    1.47 -             val (Node (gty, _, _, _, _)) = the (Symtab.curried_lookup graph name)
    1.48 +             val (Node (gty, _, _, _, _)) = the (Symtab.lookup graph name)
    1.49             in
    1.50               if is_instance_r ty gty andalso is_instance_r gty ty then
    1.51                 g
    1.52 @@ -227,13 +227,13 @@
    1.53        val _ = axcounter := c+1
    1.54        val axname' = axname^"_"^(IntInf.toString c)
    1.55      in
    1.56 -      (Symtab.curried_update (axname', axname) axmap, axname')
    1.57 +      (Symtab.update (axname', axname) axmap, axname')
    1.58      end
    1.59  
    1.60  fun translate_ex axmap x =
    1.61      let
    1.62        fun translate (ty, nodename, axname) =
    1.63 -          (ty, nodename, the (Symtab.curried_lookup axmap axname))
    1.64 +          (ty, nodename, the (Symtab.lookup axmap axname))
    1.65      in
    1.66        case x of
    1.67          INFINITE_CHAIN chain => raise (INFINITE_CHAIN (map translate chain))
    1.68 @@ -243,7 +243,7 @@
    1.69  
    1.70  fun define' (cost, axmap, actions, graph) (mainref, ty) axname orig_axname body =
    1.71      let
    1.72 -      val mainnode  = (case Symtab.curried_lookup graph mainref of
    1.73 +      val mainnode  = (case Symtab.lookup graph mainref of
    1.74                           NONE => def_err ("constant "^mainref^" is not declared")
    1.75                         | SOME n => n)
    1.76        val (Node (gty, defs, backs, finals, _)) = mainnode
    1.77 @@ -273,8 +273,8 @@
    1.78               let
    1.79                 val links = map normalize_edge_idx links
    1.80               in
    1.81 -               Symtab.curried_update (nodename,
    1.82 -                               case Symtab.curried_lookup edges nodename of
    1.83 +               Symtab.update (nodename,
    1.84 +                               case Symtab.lookup edges nodename of
    1.85                                   NONE => links
    1.86                                 | SOME links' => merge_edges links' links) edges
    1.87               end)
    1.88 @@ -282,7 +282,7 @@
    1.89        fun make_edges ((bodyn, bodyty), edges) =
    1.90            let
    1.91              val bnode =
    1.92 -                (case Symtab.curried_lookup graph bodyn of
    1.93 +                (case Symtab.lookup graph bodyn of
    1.94                     NONE => def_err "body of constant definition references undeclared constant"
    1.95                   | SOME x => x)
    1.96              val (Node (general_btyp, bdefs, bbacks, bfinals, closed)) = bnode
    1.97 @@ -345,13 +345,13 @@
    1.98                          sys_error ("install_backrefs: closed node cannot be updated")
    1.99                        else ()
   1.100                val defnames =
   1.101 -                  (case Symtab.curried_lookup backs mainref of
   1.102 +                  (case Symtab.lookup backs mainref of
   1.103                       NONE => Symtab.empty
   1.104                     | SOME s => s)
   1.105 -              val defnames' = Symtab.curried_update_new (axname, ()) defnames
   1.106 -              val backs' = Symtab.curried_update (mainref, defnames') backs
   1.107 +              val defnames' = Symtab.update_new (axname, ()) defnames
   1.108 +              val backs' = Symtab.update (mainref, defnames') backs
   1.109              in
   1.110 -              Symtab.curried_update (noderef, Node (ty, defs, backs', finals, closed)) graph
   1.111 +              Symtab.update (noderef, Node (ty, defs, backs', finals, closed)) graph
   1.112              end
   1.113            else
   1.114              graph
   1.115 @@ -364,7 +364,7 @@
   1.116            else if closed = Open andalso is_instance_r gty ty then Closed else closed
   1.117  
   1.118        val thisDefnode = Defnode (ty, edges)
   1.119 -      val graph = Symtab.curried_update (mainref, Node (gty, Symtab.curried_update_new
   1.120 +      val graph = Symtab.update (mainref, Node (gty, Symtab.update_new
   1.121          (axname, thisDefnode) defs, backs, finals, closed)) graph
   1.122  
   1.123        (* Now we have to check all backreferences to this node and inform them about
   1.124 @@ -377,8 +377,8 @@
   1.125                        getnode graph noderef
   1.126                    val _ = if closed = Final then sys_error "update_defs: closed node" else ()
   1.127                    val (Defnode (def_ty, defnode_edges)) =
   1.128 -                      the (Symtab.curried_lookup nodedefs defname)
   1.129 -                  val edges = the (Symtab.curried_lookup defnode_edges mainref)
   1.130 +                      the (Symtab.lookup nodedefs defname)
   1.131 +                  val edges = the (Symtab.lookup defnode_edges mainref)
   1.132                    val refclosed = ref false
   1.133  
   1.134                    (* the type of thisDefnode is ty *)
   1.135 @@ -416,7 +416,7 @@
   1.136                    val defnames' = if edges' = [] then
   1.137                                      defnames
   1.138                                    else
   1.139 -                                    Symtab.curried_update (defname, ()) defnames
   1.140 +                                    Symtab.update (defname, ()) defnames
   1.141                  in
   1.142                    if changed then
   1.143                      let
   1.144 @@ -424,14 +424,14 @@
   1.145                            if edges' = [] then
   1.146                              Symtab.delete mainref defnode_edges
   1.147                            else
   1.148 -                            Symtab.curried_update (mainref, edges') defnode_edges
   1.149 +                            Symtab.update (mainref, edges') defnode_edges
   1.150                        val defnode' = Defnode (def_ty, defnode_edges')
   1.151 -                      val nodedefs' = Symtab.curried_update (defname, defnode') nodedefs
   1.152 +                      val nodedefs' = Symtab.update (defname, defnode') nodedefs
   1.153                        val closed = if closed = Closed andalso Symtab.is_empty defnode_edges'
   1.154                                        andalso no_forwards nodedefs'
   1.155                                     then Final else closed
   1.156                        val graph' =
   1.157 -                        Symtab.curried_update
   1.158 +                        Symtab.update
   1.159                            (noderef, Node (nodety, nodedefs', nodebacks, nodefinals, closed)) graph
   1.160                      in
   1.161                        (defnames', graph')
   1.162 @@ -447,7 +447,7 @@
   1.163                (backs, graph')
   1.164              else
   1.165                let
   1.166 -                val backs' = Symtab.curried_update_new (noderef, defnames') backs
   1.167 +                val backs' = Symtab.update_new (noderef, defnames') backs
   1.168                in
   1.169                  (backs', graph')
   1.170                end
   1.171 @@ -458,7 +458,7 @@
   1.172        (* If a Circular exception is thrown then we never reach this point. *)
   1.173        val (Node (gty, defs, _, finals, closed)) = getnode graph mainref
   1.174        val closed = if closed = Closed andalso no_forwards defs then Final else closed
   1.175 -      val graph = Symtab.curried_update (mainref, Node (gty, defs, backs, finals, closed)) graph
   1.176 +      val graph = Symtab.update (mainref, Node (gty, defs, backs, finals, closed)) graph
   1.177        val actions' = (Define (mainref, ty, axname, orig_axname, body))::actions
   1.178      in
   1.179        (cost+3, axmap, actions', graph)
   1.180 @@ -482,7 +482,7 @@
   1.181      end
   1.182  
   1.183  fun finalize' (cost, axmap, history, graph) (noderef, ty) =
   1.184 -    case Symtab.curried_lookup graph noderef of
   1.185 +    case Symtab.lookup graph noderef of
   1.186        NONE => def_err ("cannot finalize constant "^noderef^"; it is not declared")
   1.187      | SOME (Node (nodety, defs, backs, finals, closed)) =>
   1.188        let
   1.189 @@ -519,7 +519,7 @@
   1.190              val closed = if closed = Open andalso is_instance_r nodety ty then
   1.191                             Closed else
   1.192                           closed
   1.193 -            val graph = Symtab.curried_update (noderef, Node (nodety, defs, backs, finals, closed)) graph
   1.194 +            val graph = Symtab.update (noderef, Node (nodety, defs, backs, finals, closed)) graph
   1.195  
   1.196              fun update_backref ((graph, backs), (backrefname, backdefnames)) =
   1.197                  let
   1.198 @@ -532,7 +532,7 @@
   1.199                              the (get_defnode backnode backdefname)
   1.200  
   1.201                          val (defnames', all_edges') =
   1.202 -                            case Symtab.curried_lookup all_edges noderef of
   1.203 +                            case Symtab.lookup all_edges noderef of
   1.204                                NONE => sys_error "finalize: corrupt backref"
   1.205                              | SOME edges =>
   1.206                                let
   1.207 @@ -542,11 +542,11 @@
   1.208                                  if edges' = [] then
   1.209                                    (defnames, Symtab.delete noderef all_edges)
   1.210                                  else
   1.211 -                                  (Symtab.curried_update (backdefname, ()) defnames,
   1.212 -                                   Symtab.curried_update (noderef, edges') all_edges)
   1.213 +                                  (Symtab.update (backdefname, ()) defnames,
   1.214 +                                   Symtab.update (noderef, edges') all_edges)
   1.215                                end
   1.216                          val defnode' = Defnode (def_ty, all_edges')
   1.217 -                        val backdefs' = Symtab.curried_update (backdefname, defnode') backdefs
   1.218 +                        val backdefs' = Symtab.update (backdefname, defnode') backdefs
   1.219                          val backclosed' = if backclosed = Closed andalso
   1.220                                               Symtab.is_empty all_edges'
   1.221                                               andalso no_forwards backdefs'
   1.222 @@ -554,19 +554,19 @@
   1.223                          val backnode' =
   1.224                              Node (backty, backdefs', backbacks, backfinals, backclosed')
   1.225                        in
   1.226 -                        (Symtab.curried_update (backrefname, backnode') graph, defnames')
   1.227 +                        (Symtab.update (backrefname, backnode') graph, defnames')
   1.228                        end
   1.229  
   1.230                    val (graph', defnames') =
   1.231                        Symtab.foldl update_backdef ((graph, Symtab.empty), backdefnames)
   1.232                  in
   1.233                    (graph', if Symtab.is_empty defnames' then backs
   1.234 -                           else Symtab.curried_update (backrefname, defnames') backs)
   1.235 +                           else Symtab.update (backrefname, defnames') backs)
   1.236                  end
   1.237              val (graph', backs') = Symtab.foldl update_backref ((graph, Symtab.empty), backs)
   1.238              val Node ( _, defs, _, _, closed) = getnode graph' noderef
   1.239              val closed = if closed = Closed andalso no_forwards defs then Final else closed
   1.240 -            val graph' = Symtab.curried_update (noderef, Node (nodety, defs, backs',
   1.241 +            val graph' = Symtab.update (noderef, Node (nodety, defs, backs',
   1.242                                                          finals, closed)) graph'
   1.243              val history' = (Finalize (noderef, ty)) :: history
   1.244            in
   1.245 @@ -577,14 +577,14 @@
   1.246  fun finalize'' thy g (noderef, ty) = finalize' g (noderef, checkT thy ty)
   1.247  
   1.248  fun update_axname ax orig_ax (cost, axmap, history, graph) =
   1.249 -  (cost, Symtab.curried_update (ax, orig_ax) axmap, history, graph)
   1.250 +  (cost, Symtab.update (ax, orig_ax) axmap, history, graph)
   1.251  
   1.252  fun merge' (Declare cty, g) = declare' g cty
   1.253    | merge' (Define (name, ty, axname, orig_axname, body), g as (cost, axmap, history, graph)) =
   1.254 -    (case Symtab.curried_lookup graph name of
   1.255 +    (case Symtab.lookup graph name of
   1.256         NONE => define' (update_axname axname orig_axname g) (name, ty) axname orig_axname body
   1.257       | SOME (Node (_, defs, _, _, _)) =>
   1.258 -       (case Symtab.curried_lookup defs axname of
   1.259 +       (case Symtab.lookup defs axname of
   1.260            NONE => define' (update_axname axname orig_axname g) (name, ty) axname orig_axname body
   1.261          | SOME _ => g))
   1.262    | merge' (Finalize finals, g) = finalize' g finals
   1.263 @@ -598,14 +598,14 @@
   1.264  fun finals (_, _, history, graph) =
   1.265      Symtab.foldl
   1.266        (fn (finals, (name, Node(_, _, _, ftys, _))) =>
   1.267 -          Symtab.curried_update_new (name, ftys) finals)
   1.268 +          Symtab.update_new (name, ftys) finals)
   1.269        (Symtab.empty, graph)
   1.270  
   1.271  fun overloading_info (_, axmap, _, graph) c =
   1.272      let
   1.273 -      fun translate (ax, Defnode (ty, _)) = (the (Symtab.curried_lookup axmap ax), ty)
   1.274 +      fun translate (ax, Defnode (ty, _)) = (the (Symtab.lookup axmap ax), ty)
   1.275      in
   1.276 -      case Symtab.curried_lookup graph c of
   1.277 +      case Symtab.lookup graph c of
   1.278          NONE => NONE
   1.279        | SOME (Node (ty, defnodes, _, _, state)) =>
   1.280          SOME (ty, map translate (Symtab.dest defnodes), state)
   1.281 @@ -618,7 +618,7 @@
   1.282    | monomorphicT _ = false
   1.283  
   1.284  fun monomorphic (_, _, _, graph) c =
   1.285 -  (case Symtab.curried_lookup graph c of
   1.286 +  (case Symtab.lookup graph c of
   1.287      NONE => true
   1.288    | SOME (Node (ty, defnodes, _, _, _)) =>
   1.289        Symtab.min_key defnodes = Symtab.max_key defnodes andalso