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.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
```