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