src/Pure/defs.ML
changeset 17707 bc0270e9d27f
parent 17670 bf4f2c1b26cc
child 17711 c16cbe73798c
     1.1 --- a/src/Pure/defs.ML	Thu Sep 29 00:58:59 2005 +0200
     1.2 +++ b/src/Pure/defs.ML	Thu Sep 29 00:59:00 2005 +0200
     1.3 @@ -1,720 +1,108 @@
     1.4 -(*  Title:      Pure/General/defs.ML
     1.5 +(*  Title:      Pure/defs.ML
     1.6      ID:         $Id$
     1.7 -    Author:     Steven Obua, TU Muenchen
     1.8 +    Author:     Makarius
     1.9  
    1.10 -Checks if definitions preserve consistency of logic by enforcing that
    1.11 -there are no cyclic definitions. The algorithm is described in "An
    1.12 -Algorithm for Determining Definitional Cycles in Higher-Order Logic
    1.13 -with Overloading", Steven Obua, technical report, to be written :-)
    1.14 -
    1.15 -ATTENTION:
    1.16 -Currently this implementation of the cycle test contains a bug of which the author is fully aware.
    1.17 -This bug makes it possible to introduce inconsistent definitional cycles in Isabelle. 
    1.18 +Global well-formedness checks for constant definitions.  Dependencies
    1.19 +are only tracked for non-overloaded definitions!
    1.20  *)
    1.21  
    1.22  signature DEFS =
    1.23  sig
    1.24 -  (*true: record the full chain of definitions that lead to a circularity*)
    1.25 -  val chain_history: bool ref
    1.26 -  type graph
    1.27 -  val empty: graph
    1.28 -  val declare: theory -> string * typ -> graph -> graph
    1.29 -  val define: theory -> string * typ -> string -> (string * typ) list -> graph -> graph
    1.30 -  val finalize: theory -> string * typ -> graph -> graph
    1.31 -  val merge: Pretty.pp -> graph -> graph -> graph
    1.32 -  val finals: graph -> typ list Symtab.table
    1.33 -  datatype overloadingstate = Open | Closed | Final
    1.34 -  val overloading_info: graph -> string -> (typ * (string*typ) list * overloadingstate) option
    1.35 -  val monomorphic: graph -> string -> bool
    1.36 +  type T
    1.37 +  val monomorphic: T -> string -> bool
    1.38 +  val define: string -> string * typ -> (string * typ) list -> T -> T
    1.39 +  val empty: T
    1.40 +  val merge: Pretty.pp -> T * T -> T
    1.41  end
    1.42  
    1.43 -structure Defs :> DEFS = struct
    1.44 -
    1.45 -type tyenv = Type.tyenv
    1.46 -type edgelabel = (int * typ * typ * (typ * string * string) list)
    1.47 -
    1.48 -datatype overloadingstate = Open | Closed | Final
    1.49 -
    1.50 -datatype node = Node of
    1.51 -         typ  (* most general type of constant *)
    1.52 -         * defnode Symtab.table
    1.53 -             (* a table of defnodes, each corresponding to 1 definition of the
    1.54 -                constant for a particular type, indexed by axiom name *)
    1.55 -         * (unit Symtab.table) Symtab.table
    1.56 -             (* a table of all back referencing defnodes to this node,
    1.57 -                indexed by node name of the defnodes *)
    1.58 -         * typ list (* a list of all finalized types *)
    1.59 -         * overloadingstate
    1.60 -
    1.61 -     and defnode = Defnode of
    1.62 -         typ  (* type of the constant in this particular definition *)
    1.63 -         * (edgelabel list) Symtab.table (* The edges, grouped by nodes. *)
    1.64 -
    1.65 -fun getnode graph = the o Symtab.lookup graph
    1.66 -fun get_nodedefs (Node (_, defs, _, _, _)) = defs
    1.67 -fun get_defnode (Node (_, defs, _, _, _)) defname = Symtab.lookup defs defname
    1.68 -fun get_defnode' graph noderef =
    1.69 -  Symtab.lookup (get_nodedefs (the (Symtab.lookup graph noderef)))
    1.70 -
    1.71 -fun table_size table = Symtab.fold (K (fn x => x + 1)) table 0;
    1.72 -
    1.73 -datatype graphaction =
    1.74 -    Declare of string * typ
    1.75 -  | Define of string * typ * string * string * (string * typ) list
    1.76 -  | Finalize of string * typ
    1.77 -
    1.78 -type graph = int * string Symtab.table * graphaction list * node Symtab.table
    1.79 -
    1.80 -val chain_history = ref true
    1.81 -
    1.82 -val empty = (0, Symtab.empty, [], Symtab.empty)
    1.83 -
    1.84 -exception DEFS of string;
    1.85 -exception CIRCULAR of (typ * string * string) list;
    1.86 -exception INFINITE_CHAIN of (typ * string * string) list;
    1.87 -exception CLASH of string * string * string;
    1.88 -exception FINAL of string * typ;
    1.89 -
    1.90 -fun def_err s = raise (DEFS s)
    1.91 -
    1.92 -fun no_forwards defs =
    1.93 -    Symtab.foldl
    1.94 -    (fn (closed, (_, Defnode (_, edges))) =>
    1.95 -        if not closed then false else Symtab.is_empty edges)
    1.96 -    (true, defs)
    1.97 -
    1.98 -fun checkT' (Type (a, Ts)) = Type (a, map checkT' Ts)
    1.99 -  | checkT' (TFree (a, _)) = TVar ((a, 0), [])        
   1.100 -  | checkT' (TVar ((a, 0), _)) = TVar ((a, 0), [])
   1.101 -  | checkT' (T as TVar _) = raise TYPE ("Illegal schematic type variable encountered", [T], []);
   1.102 -
   1.103 -fun checkT thy = Compress.typ thy o checkT';
   1.104 -
   1.105 -fun rename ty1 ty2 = Logic.incr_tvar ((maxidx_of_typ ty1)+1) ty2;
   1.106 +structure Defs (* FIXME : DEFS *) =
   1.107 +struct
   1.108  
   1.109 -fun subst_incr_tvar inc t =
   1.110 -    if inc > 0 then
   1.111 -      let
   1.112 -        val tv = typ_tvars t
   1.113 -        val t' = Logic.incr_tvar inc t
   1.114 -        fun update_subst ((n, i), _) =
   1.115 -          Vartab.update ((n, i), ([], TVar ((n, i + inc), [])));
   1.116 -      in
   1.117 -        (t', fold update_subst tv Vartab.empty)
   1.118 -      end
   1.119 -    else
   1.120 -      (t, Vartab.empty)
   1.121 -
   1.122 -fun subst s ty = Envir.norm_type s ty
   1.123 -
   1.124 -fun subst_history s history = map (fn (ty, cn, dn) => (subst s ty, cn, dn)) history
   1.125 -
   1.126 -fun is_instance instance_ty general_ty =
   1.127 -    Type.raw_instance (instance_ty, general_ty)
   1.128 -
   1.129 -fun is_instance_r instance_ty general_ty =
   1.130 -    is_instance instance_ty (rename instance_ty general_ty)
   1.131 -
   1.132 -fun unify ty1 ty2 =
   1.133 -    SOME (Type.raw_unify (ty1, ty2) Vartab.empty)
   1.134 -    handle Type.TUNIFY => NONE
   1.135 -
   1.136 -(*
   1.137 -   Unifies ty1 and ty2, renaming ty1 and ty2 so that they have greater indices than max and
   1.138 -   so that they are different. All indices in ty1 and ty2 are supposed to be less than or
   1.139 -   equal to max.
   1.140 -   Returns SOME (max', s1, s2), so that s1(ty1) = s2(ty2) and max' is greater or equal than
   1.141 -   all indices in s1, s2, ty1, ty2.
   1.142 -*)
   1.143 -fun unify_r max ty1 ty2 =
   1.144 -    let
   1.145 -      val max = Int.max(max, 0)
   1.146 -      val max1 = max (* >= maxidx_of_typ ty1 *)
   1.147 -      val max2 = max (* >= maxidx_of_typ ty2 *)
   1.148 -      val max = Int.max(max, Int.max (max1, max2))
   1.149 -      val (ty1, s1) = subst_incr_tvar (max + 1) ty1
   1.150 -      val (ty2, s2) = subst_incr_tvar (max + max1 + 2) ty2
   1.151 -      val max = max + max1 + max2 + 2
   1.152 -      fun merge a b = Vartab.merge (fn _ => false) (a, b)
   1.153 -    in
   1.154 -      case unify ty1 ty2 of
   1.155 -        NONE => NONE
   1.156 -      | SOME s => SOME (max, merge s1 s, merge s2 s)
   1.157 -    end
   1.158 -
   1.159 -fun can_be_unified_r ty1 ty2 = is_some (unify ty1 (rename ty1 ty2))
   1.160 -fun can_be_unified ty1 ty2 = is_some (unify ty1 ty2)
   1.161 -
   1.162 -fun normalize_edge_idx (edge as (maxidx, u1, v1, history)) =
   1.163 -    if maxidx <= 1000000 then edge else
   1.164 -    let
   1.165 -
   1.166 -      fun idxlist idx extract_ty inject_ty (tab, max) ts =
   1.167 -          foldr
   1.168 -            (fn (e, ((tab, max), ts)) =>
   1.169 -                let
   1.170 -                  val ((tab, max), ty) = idx (tab, max) (extract_ty e)
   1.171 -                  val e = inject_ty (ty, e)
   1.172 -                in
   1.173 -                  ((tab, max), e::ts)
   1.174 -                end)
   1.175 -            ((tab,max), []) ts
   1.176 -
   1.177 -      fun idx (tab,max) (TVar ((a,i),_)) =
   1.178 -          (case Inttab.lookup tab i of
   1.179 -             SOME j => ((tab, max), TVar ((a,j),[]))
   1.180 -           | NONE => ((Inttab.update (i, max) tab, max + 1), TVar ((a,max),[])))
   1.181 -        | idx (tab,max) (Type (t, ts)) =
   1.182 -          let
   1.183 -            val ((tab, max), ts) = idxlist idx I fst (tab, max) ts
   1.184 -          in
   1.185 -            ((tab,max), Type (t, ts))
   1.186 -          end
   1.187 -        | idx (tab, max) ty = ((tab, max), ty)
   1.188 +(** datatype T **)
   1.189  
   1.190 -      val ((tab,max), u1) = idx (Inttab.empty, 0) u1
   1.191 -      val ((tab,max), v1) = idx (tab, max) v1
   1.192 -      val ((tab,max), history) =
   1.193 -          idxlist idx
   1.194 -            (fn (ty,_,_) => ty)
   1.195 -            (fn (ty, (_, s1, s2)) => (ty, s1, s2))
   1.196 -            (tab, max) history
   1.197 -    in
   1.198 -      (max, u1, v1, history)
   1.199 -    end
   1.200 -
   1.201 -fun compare_edges (e1 as (maxidx1, u1, v1, history1)) (e2 as (maxidx2, u2, v2, history2)) =
   1.202 -    let
   1.203 -      val t1 = u1 --> v1
   1.204 -      val t2 = Logic.incr_tvar (maxidx1+1) (u2 --> v2)
   1.205 -    in
   1.206 -      if (is_instance t1 t2) then
   1.207 -        (if is_instance t2 t1 then
   1.208 -           SOME (int_ord (length history2, length history1))
   1.209 -         else
   1.210 -           SOME LESS)
   1.211 -      else if (is_instance t2 t1) then
   1.212 -        SOME GREATER
   1.213 -      else
   1.214 -        NONE
   1.215 -    end
   1.216 -
   1.217 -fun merge_edges_1 (x, []) = [x]
   1.218 -  | merge_edges_1 (x, (y::ys)) =
   1.219 -    (case compare_edges x y of
   1.220 -       SOME LESS => (y::ys)
   1.221 -     | SOME EQUAL => (y::ys)
   1.222 -     | SOME GREATER => merge_edges_1 (x, ys)
   1.223 -     | NONE => y::(merge_edges_1 (x, ys)))
   1.224 -
   1.225 -fun merge_edges xs ys = foldl merge_edges_1 xs ys
   1.226 -
   1.227 -fun declare' (g as (cost, axmap, actions, graph)) (cty as (name, ty)) =
   1.228 -    (cost, axmap, (Declare cty)::actions,
   1.229 -     Symtab.update_new (name, Node (ty, Symtab.empty, Symtab.empty, [], Open)) graph)
   1.230 -    handle Symtab.DUP _ =>
   1.231 -           let
   1.232 -             val (Node (gty, _, _, _, _)) = the (Symtab.lookup graph name)
   1.233 -           in
   1.234 -             if is_instance_r ty gty andalso is_instance_r gty ty then
   1.235 -               g
   1.236 -             else
   1.237 -               def_err "constant is already declared with different type"
   1.238 -           end
   1.239 -
   1.240 -fun declare'' thy g (name, ty) = declare' g (name, checkT thy ty)
   1.241 -
   1.242 -val axcounter = ref (IntInf.fromInt 0)
   1.243 -fun newaxname axmap axname =
   1.244 -    let
   1.245 -      val c = !axcounter
   1.246 -      val _ = axcounter := c+1
   1.247 -      val axname' = axname^"_"^(IntInf.toString c)
   1.248 -    in
   1.249 -      (Symtab.update (axname', axname) axmap, axname')
   1.250 -    end
   1.251 +datatype T = Defs of
   1.252 + {consts: typ Graph.T,                                 (*constant declarations and dependencies*)
   1.253 +  specified: (string * typ) Inttab.table Symtab.table, (*specification name and const type*)
   1.254 +  monomorphic: unit Symtab.table};                     (*constants having monomorphic specs*)
   1.255  
   1.256 -fun translate_ex axmap x =
   1.257 -    let
   1.258 -      fun translate (ty, nodename, axname) =
   1.259 -          (ty, nodename, the (Symtab.lookup axmap axname))
   1.260 -    in
   1.261 -      case x of
   1.262 -        INFINITE_CHAIN chain => raise (INFINITE_CHAIN (map translate chain))
   1.263 -      | CIRCULAR cycle => raise (CIRCULAR (map translate cycle))
   1.264 -      | _ => raise x
   1.265 -    end
   1.266 -
   1.267 -fun define' (cost, axmap, actions, graph) (mainref, ty) axname orig_axname body =
   1.268 -    let
   1.269 -      val mainnode  = (case Symtab.lookup graph mainref of
   1.270 -                         NONE => def_err ("constant "^mainref^" is not declared")
   1.271 -                       | SOME n => n)
   1.272 -      val (Node (gty, defs, backs, finals, _)) = mainnode
   1.273 -      val _ = (if is_instance_r ty gty then ()
   1.274 -               else def_err "type of constant does not match declared type")
   1.275 -      fun check_def (s, Defnode (ty', _)) =
   1.276 -          (if can_be_unified_r ty ty' then
   1.277 -             raise (CLASH (mainref, axname, s))
   1.278 -           else if s = axname then
   1.279 -             def_err "name of axiom is already used for another definition of this constant"
   1.280 -           else false)
   1.281 -      val _ = Symtab.exists check_def defs
   1.282 -      fun check_final finalty =
   1.283 -          (if can_be_unified_r finalty ty then
   1.284 -             raise (FINAL (mainref, finalty))
   1.285 -           else
   1.286 -             true)
   1.287 -      val _ = forall check_final finals
   1.288 -
   1.289 -      (* now we know that the only thing that can prevent acceptance of the definition
   1.290 -         is a cyclic dependency *)
   1.291 +fun rep_defs (Defs args) = args;
   1.292  
   1.293 -      fun insert_edges edges (nodename, links) =
   1.294 -          (if links = [] then
   1.295 -             edges
   1.296 -           else
   1.297 -             let
   1.298 -               val links = map normalize_edge_idx links
   1.299 -             in
   1.300 -               Symtab.update (nodename,
   1.301 -                               case Symtab.lookup edges nodename of
   1.302 -                                 NONE => links
   1.303 -                               | SOME links' => merge_edges links' links) edges
   1.304 -             end)
   1.305 -
   1.306 -      fun make_edges ((bodyn, bodyty), edges) =
   1.307 -          let
   1.308 -            val bnode =
   1.309 -                (case Symtab.lookup graph bodyn of
   1.310 -                   NONE => def_err "body of constant definition references undeclared constant"
   1.311 -                 | SOME x => x)
   1.312 -            val (Node (general_btyp, bdefs, bbacks, bfinals, closed)) = bnode
   1.313 -          in
   1.314 -            if closed = Final then edges else
   1.315 -            case unify_r 0 bodyty general_btyp of
   1.316 -              NONE => edges
   1.317 -            | SOME (maxidx, sigma1, sigma2) =>
   1.318 -              if exists (is_instance_r bodyty) bfinals then
   1.319 -                edges
   1.320 -              else
   1.321 -                let
   1.322 -                  fun insert_trans_edges ((step1, edges), (nodename, links)) =
   1.323 -                      let
   1.324 -                        val (maxidx1, alpha1, beta1, defname) = step1
   1.325 -                        fun connect (maxidx2, alpha2, beta2, history) =
   1.326 -                            case unify_r (Int.max (maxidx1, maxidx2)) beta1 alpha2 of
   1.327 -                              NONE => NONE
   1.328 -                            | SOME (max, sleft, sright) =>
   1.329 -                              SOME (max, subst sleft alpha1, subst sright beta2,
   1.330 -                                    if !chain_history then
   1.331 -                                      ((subst sleft beta1, bodyn, defname)::
   1.332 -                                       (subst_history sright history))
   1.333 -                                    else [])
   1.334 -                        val links' = List.mapPartial connect links
   1.335 -                      in
   1.336 -                        (step1, insert_edges edges (nodename, links'))
   1.337 -                      end
   1.338 +fun make_defs (consts, specified, monomorphic) =
   1.339 +  Defs {consts = consts, specified = specified, monomorphic = monomorphic};
   1.340  
   1.341 -                  fun make_edges' ((swallowed, edges),
   1.342 -                                   (def_name, Defnode (def_ty, def_edges))) =
   1.343 -                      if swallowed then
   1.344 -                        (swallowed, edges)
   1.345 -                      else
   1.346 -                        (case unify_r 0 bodyty def_ty of
   1.347 -                           NONE => (swallowed, edges)
   1.348 -                         | SOME (maxidx, sigma1, sigma2) =>
   1.349 -                           (is_instance_r bodyty def_ty,
   1.350 -                            snd (Symtab.foldl insert_trans_edges
   1.351 -                              (((maxidx, subst sigma1 ty, subst sigma2 def_ty, def_name),
   1.352 -                                edges), def_edges))))
   1.353 -                  val (swallowed, edges) = Symtab.foldl make_edges' ((false, edges), bdefs)
   1.354 -                in
   1.355 -                  if swallowed then
   1.356 -                    edges
   1.357 -                  else
   1.358 -                    insert_edges edges
   1.359 -                    (bodyn, [(maxidx, subst sigma1 ty, subst sigma2 general_btyp,[])])
   1.360 -                end
   1.361 -          end
   1.362 -
   1.363 -      val edges = foldl make_edges Symtab.empty body
   1.364 -
   1.365 -      (* We also have to add the backreferences that this new defnode induces. *)
   1.366 -      fun install_backrefs (graph, (noderef, links)) =
   1.367 -          if links <> [] then
   1.368 -            let
   1.369 -              val (Node (ty, defs, backs, finals, closed)) = getnode graph noderef
   1.370 -              val _ = if closed = Final then
   1.371 -                        sys_error ("install_backrefs: closed node cannot be updated")
   1.372 -                      else ()
   1.373 -              val defnames =
   1.374 -                  (case Symtab.lookup backs mainref of
   1.375 -                     NONE => Symtab.empty
   1.376 -                   | SOME s => s)
   1.377 -              val defnames' = Symtab.update_new (axname, ()) defnames
   1.378 -              val backs' = Symtab.update (mainref, defnames') backs
   1.379 -            in
   1.380 -              Symtab.update (noderef, Node (ty, defs, backs', finals, closed)) graph
   1.381 -            end
   1.382 -          else
   1.383 -            graph
   1.384 -
   1.385 -      val graph = Symtab.foldl install_backrefs (graph, edges)
   1.386 -
   1.387 -      val (Node (_, _, backs, _, closed)) = getnode graph mainref
   1.388 -      val closed =
   1.389 -          if closed = Final then sys_error "define: closed node"
   1.390 -          else if closed = Open andalso is_instance_r gty ty then Closed else closed
   1.391 -
   1.392 -      val thisDefnode = Defnode (ty, edges)
   1.393 -      val graph = Symtab.update (mainref, Node (gty, Symtab.update_new
   1.394 -        (axname, thisDefnode) defs, backs, finals, closed)) graph
   1.395 -
   1.396 -      (* Now we have to check all backreferences to this node and inform them about
   1.397 -         the new defnode. In this section we also check for circularity. *)
   1.398 -      fun update_backrefs ((backs, graph), (noderef, defnames)) =
   1.399 -          let
   1.400 -            fun update_defs ((defnames, graph),(defname, _)) =
   1.401 -                let
   1.402 -                  val (Node (nodety, nodedefs, nodebacks, nodefinals, closed)) =
   1.403 -                      getnode graph noderef
   1.404 -                  val _ = if closed = Final then sys_error "update_defs: closed node" else ()
   1.405 -                  val (Defnode (def_ty, defnode_edges)) =
   1.406 -                      the (Symtab.lookup nodedefs defname)
   1.407 -                  val edges = the (Symtab.lookup defnode_edges mainref)
   1.408 -                  val refclosed = ref false
   1.409 +fun map_defs f (Defs {consts, specified, monomorphic}) =
   1.410 +  make_defs (f (consts, specified, monomorphic));
   1.411  
   1.412 -                  (* the type of thisDefnode is ty *)
   1.413 -                  fun update (e as (max, alpha, beta, history), (changed, edges)) =
   1.414 -                      case unify_r max beta ty of
   1.415 -                        NONE => (changed, e::edges)
   1.416 -                      | SOME (max', s_beta, s_ty) =>
   1.417 -                        let
   1.418 -                          val alpha' = subst s_beta alpha
   1.419 -                          val ty' = subst s_ty ty
   1.420 -                          val _ =
   1.421 -                              if noderef = mainref andalso defname = axname then
   1.422 -                                (case unify alpha' ty' of
   1.423 -                                   NONE =>
   1.424 -                                   if (is_instance_r ty' alpha') then
   1.425 -                                     raise (INFINITE_CHAIN (
   1.426 -                                            (alpha', mainref, axname)::
   1.427 -                                            (subst_history s_beta history)@
   1.428 -                                            [(ty', mainref, axname)]))
   1.429 -                                   else ()
   1.430 -                                 | SOME s =>
   1.431 -                                   raise (CIRCULAR (
   1.432 -                                          (subst s alpha', mainref, axname)::
   1.433 -                                          (subst_history s (subst_history s_beta history))@
   1.434 -                                          [(subst s ty', mainref, axname)])))
   1.435 -                              else ()
   1.436 -                        in
   1.437 -                          if is_instance_r beta ty then
   1.438 -                            (true, edges)
   1.439 -                          else
   1.440 -                            (changed, e::edges)
   1.441 -                        end
   1.442  
   1.443 -                  val (changed, edges') = foldl update (false, []) edges
   1.444 -                  val defnames' = if edges' = [] then
   1.445 -                                    defnames
   1.446 -                                  else
   1.447 -                                    Symtab.update (defname, ()) defnames
   1.448 -                in
   1.449 -                  if changed then
   1.450 -                    let
   1.451 -                      val defnode_edges' =
   1.452 -                          if edges' = [] then
   1.453 -                            Symtab.delete mainref defnode_edges
   1.454 -                          else
   1.455 -                            Symtab.update (mainref, edges') defnode_edges
   1.456 -                      val defnode' = Defnode (def_ty, defnode_edges')
   1.457 -                      val nodedefs' = Symtab.update (defname, defnode') nodedefs
   1.458 -                      val closed = if closed = Closed andalso Symtab.is_empty defnode_edges'
   1.459 -                                      andalso no_forwards nodedefs'
   1.460 -                                   then Final else closed
   1.461 -                      val graph' =
   1.462 -                        Symtab.update
   1.463 -                          (noderef, Node (nodety, nodedefs', nodebacks, nodefinals, closed)) graph
   1.464 -                    in
   1.465 -                      (defnames', graph')
   1.466 -                    end
   1.467 -                  else
   1.468 -                    (defnames', graph)
   1.469 -                end
   1.470 -
   1.471 -            val (defnames', graph') = Symtab.foldl update_defs
   1.472 -                                                   ((Symtab.empty, graph), defnames)
   1.473 -          in
   1.474 -            if Symtab.is_empty defnames' then
   1.475 -              (backs, graph')
   1.476 -            else
   1.477 -              let
   1.478 -                val backs' = Symtab.update_new (noderef, defnames') backs
   1.479 -              in
   1.480 -                (backs', graph')
   1.481 -              end
   1.482 -          end
   1.483 -
   1.484 -      val (backs, graph) = Symtab.foldl update_backrefs ((Symtab.empty, graph), backs)
   1.485 +(* specified consts *)
   1.486  
   1.487 -      (* If a Circular exception is thrown then we never reach this point. *)
   1.488 -      val (Node (gty, defs, _, finals, closed)) = getnode graph mainref
   1.489 -      val closed = if closed = Closed andalso no_forwards defs then Final else closed
   1.490 -      val graph = Symtab.update (mainref, Node (gty, defs, backs, finals, closed)) graph
   1.491 -      val actions' = (Define (mainref, ty, axname, orig_axname, body))::actions
   1.492 -    in
   1.493 -      (cost+3, axmap, actions', graph)
   1.494 -    end handle ex => translate_ex axmap ex
   1.495 -
   1.496 -fun define'' thy (g as (cost, axmap, actions, graph)) (mainref, ty) orig_axname body =
   1.497 -    let
   1.498 -      val ty = checkT thy ty
   1.499 -      fun checkbody (n, t) =
   1.500 -          let
   1.501 -            val (Node (_, _, _,_, closed)) = getnode graph n
   1.502 -          in
   1.503 -            case closed of
   1.504 -              Final => NONE
   1.505 -            | _ => SOME (n, checkT thy t)
   1.506 -          end
   1.507 -      val body = distinct (List.mapPartial checkbody body)
   1.508 -      val (axmap, axname) = newaxname axmap orig_axname
   1.509 -    in
   1.510 -      define' (cost, axmap, actions, graph) (mainref, ty) axname orig_axname body
   1.511 -    end
   1.512 -
   1.513 -fun finalize' (cost, axmap, history, graph) (noderef, ty) =
   1.514 -    case Symtab.lookup graph noderef of
   1.515 -      NONE => def_err ("cannot finalize constant "^noderef^"; it is not declared")
   1.516 -    | SOME (Node (nodety, defs, backs, finals, closed)) =>
   1.517 -      let
   1.518 -        val _ =
   1.519 -            if (not (is_instance_r ty nodety)) then
   1.520 -              def_err ("only type instances of the declared constant "^
   1.521 -                       noderef^" can be finalized")
   1.522 -            else ()
   1.523 -        val _ = Symtab.exists
   1.524 -                  (fn (def_name, Defnode (def_ty, _)) =>
   1.525 -                      if can_be_unified_r ty def_ty then
   1.526 -                        def_err ("cannot finalize constant "^noderef^
   1.527 -                                 "; clash with definition "^def_name)
   1.528 -                      else
   1.529 -                        false)
   1.530 -                  defs
   1.531 -
   1.532 -        fun update_finals [] = SOME [ty]
   1.533 -          | update_finals (final_ty::finals) =
   1.534 -            (if is_instance_r ty final_ty then NONE
   1.535 -             else
   1.536 -               case update_finals finals of
   1.537 -                 NONE => NONE
   1.538 -               | (r as SOME finals) =>
   1.539 -                 if (is_instance_r final_ty ty) then
   1.540 -                   r
   1.541 -                 else
   1.542 -                   SOME (final_ty :: finals))
   1.543 -      in
   1.544 -        case update_finals finals of
   1.545 -          NONE => (cost, axmap, history, graph)
   1.546 -        | SOME finals =>
   1.547 -          let
   1.548 -            val closed = if closed = Open andalso is_instance_r nodety ty then
   1.549 -                           Closed else
   1.550 -                         closed
   1.551 -            val graph = Symtab.update (noderef, Node (nodety, defs, backs, finals, closed)) graph
   1.552 -
   1.553 -            fun update_backref ((graph, backs), (backrefname, backdefnames)) =
   1.554 -                let
   1.555 -                  fun update_backdef ((graph, defnames), (backdefname, _)) =
   1.556 -                      let
   1.557 -                        val (backnode as Node (backty, backdefs, backbacks,
   1.558 -                                               backfinals, backclosed)) =
   1.559 -                            getnode graph backrefname
   1.560 -                        val (Defnode (def_ty, all_edges)) =
   1.561 -                            the (get_defnode backnode backdefname)
   1.562 +fun disjoint_types T U =
   1.563 +  (Type.raw_unify (T, Logic.incr_tvar (maxidx_of_typ T + 1) U) Vartab.empty; false)
   1.564 +    handle Type.TUNIFY => true;
   1.565  
   1.566 -                        val (defnames', all_edges') =
   1.567 -                            case Symtab.lookup all_edges noderef of
   1.568 -                              NONE => sys_error "finalize: corrupt backref"
   1.569 -                            | SOME edges =>
   1.570 -                              let
   1.571 -                                val edges' = List.filter (fn (_, _, beta, _) =>
   1.572 -                                                             not (is_instance_r beta ty)) edges
   1.573 -                              in
   1.574 -                                if edges' = [] then
   1.575 -                                  (defnames, Symtab.delete noderef all_edges)
   1.576 -                                else
   1.577 -                                  (Symtab.update (backdefname, ()) defnames,
   1.578 -                                   Symtab.update (noderef, edges') all_edges)
   1.579 -                              end
   1.580 -                        val defnode' = Defnode (def_ty, all_edges')
   1.581 -                        val backdefs' = Symtab.update (backdefname, defnode') backdefs
   1.582 -                        val backclosed' = if backclosed = Closed andalso
   1.583 -                                             Symtab.is_empty all_edges'
   1.584 -                                             andalso no_forwards backdefs'
   1.585 -                                          then Final else backclosed
   1.586 -                        val backnode' =
   1.587 -                            Node (backty, backdefs', backbacks, backfinals, backclosed')
   1.588 -                      in
   1.589 -                        (Symtab.update (backrefname, backnode') graph, defnames')
   1.590 -                      end
   1.591 -
   1.592 -                  val (graph', defnames') =
   1.593 -                      Symtab.foldl update_backdef ((graph, Symtab.empty), backdefnames)
   1.594 -                in
   1.595 -                  (graph', if Symtab.is_empty defnames' then backs
   1.596 -                           else Symtab.update (backrefname, defnames') backs)
   1.597 -                end
   1.598 -            val (graph', backs') = Symtab.foldl update_backref ((graph, Symtab.empty), backs)
   1.599 -            val Node ( _, defs, _, _, closed) = getnode graph' noderef
   1.600 -            val closed = if closed = Closed andalso no_forwards defs then Final else closed
   1.601 -            val graph' = Symtab.update (noderef, Node (nodety, defs, backs',
   1.602 -                                                        finals, closed)) graph'
   1.603 -            val history' = (Finalize (noderef, ty)) :: history
   1.604 -          in
   1.605 -            (cost+1, axmap, history', graph')
   1.606 -          end
   1.607 -      end
   1.608 -
   1.609 -fun finalize'' thy g (noderef, ty) = finalize' g (noderef, checkT thy ty)
   1.610 -
   1.611 -fun update_axname ax orig_ax (cost, axmap, history, graph) =
   1.612 -  (cost, Symtab.update (ax, orig_ax) axmap, history, graph)
   1.613 -
   1.614 -fun merge' (Declare cty, g) = declare' g cty
   1.615 -  | merge' (Define (name, ty, axname, orig_axname, body), g as (cost, axmap, history, graph)) =
   1.616 -    (case Symtab.lookup graph name of
   1.617 -       NONE => define' (update_axname axname orig_axname g) (name, ty) axname orig_axname body
   1.618 -     | SOME (Node (_, defs, _, _, _)) =>
   1.619 -       (case Symtab.lookup defs axname of
   1.620 -          NONE => define' (update_axname axname orig_axname g) (name, ty) axname orig_axname body
   1.621 -        | SOME _ => g))
   1.622 -  | merge' (Finalize finals, g) = finalize' g finals
   1.623 -
   1.624 -fun merge'' (g1 as (cost1, _, actions1, _)) (g2 as (cost2, _, actions2, _)) =
   1.625 -    if cost1 < cost2 then
   1.626 -      foldr merge' g2 actions1
   1.627 -    else
   1.628 -      foldr merge' g1 actions2
   1.629 -
   1.630 -fun finals (_, _, history, graph) =
   1.631 -    Symtab.foldl
   1.632 -      (fn (finals, (name, Node(_, _, _, ftys, _))) =>
   1.633 -          Symtab.update_new (name, ftys) finals)
   1.634 -      (Symtab.empty, graph)
   1.635 -
   1.636 -fun overloading_info (_, axmap, _, graph) c =
   1.637 -    let
   1.638 -      fun translate (ax, Defnode (ty, _)) = (the (Symtab.lookup axmap ax), ty)
   1.639 -    in
   1.640 -      case Symtab.lookup graph c of
   1.641 -        NONE => NONE
   1.642 -      | SOME (Node (ty, defnodes, _, _, state)) =>
   1.643 -        SOME (ty, map translate (Symtab.dest defnodes), state)
   1.644 -    end
   1.645 +fun check_specified c specified =
   1.646 +  specified |> Inttab.forall (fn (i, (a, T)) =>
   1.647 +    specified |> Inttab.forall (fn (j, (b, U)) =>
   1.648 +      i = j orelse disjoint_types T U orelse
   1.649 +        error ("Type clash in specifications " ^ quote a ^ " and " ^ quote b ^
   1.650 +          " for constant " ^ quote c)));
   1.651  
   1.652  
   1.653 -(* monomorphic consts -- neither parametric nor ad-hoc polymorphism *)
   1.654 -
   1.655 -fun monomorphicT (Type (_, Ts)) = forall monomorphicT Ts
   1.656 -  | monomorphicT _ = false
   1.657 +(* monomorphic constants *)
   1.658  
   1.659 -fun monomorphic (_, _, _, graph) c =
   1.660 -  (case Symtab.lookup graph c of
   1.661 -    NONE => true
   1.662 -  | SOME (Node (ty, defnodes, _, _, _)) =>
   1.663 -      Symtab.min_key defnodes = Symtab.max_key defnodes andalso
   1.664 -      monomorphicT ty);
   1.665 -
   1.666 -
   1.667 -
   1.668 -(** diagnostics **)
   1.669 +val monomorphic = Symtab.defined o #monomorphic o rep_defs;
   1.670  
   1.671 -fun pretty_const pp (c, T) =
   1.672 - [Pretty.str c, Pretty.str " ::", Pretty.brk 1,
   1.673 -  Pretty.quote (Pretty.typ pp (Type.freeze_type (Term.zero_var_indexesT T)))];
   1.674 -
   1.675 -fun pretty_path pp path = fold_rev (fn (T, c, def) =>
   1.676 -  fn [] => [Pretty.block (pretty_const pp (c, T))]
   1.677 -   | prts => Pretty.block (pretty_const pp (c, T) @
   1.678 -      [Pretty.brk 1, Pretty.str ("depends via " ^ quote def ^ " on")]) :: prts) path [];
   1.679 -
   1.680 -fun defs_circular pp path =
   1.681 -  Pretty.str "Cyclic dependency of definitions: " :: pretty_path pp path
   1.682 -  |> Pretty.chunks |> Pretty.string_of;
   1.683 -
   1.684 -fun defs_infinite_chain pp path =
   1.685 -  Pretty.str "Infinite chain of definitions: " :: pretty_path pp path
   1.686 -  |> Pretty.chunks |> Pretty.string_of;
   1.687 -
   1.688 -fun defs_clash def1 def2 = "Type clash in definitions " ^ quote def1 ^ " and " ^ quote def2;
   1.689 -
   1.690 -fun defs_final pp const =
   1.691 -  (Pretty.str "Attempt to define final constant" :: Pretty.brk 1 :: pretty_const pp const)
   1.692 -  |> Pretty.block |> Pretty.string_of;
   1.693 +fun update_monomorphic specified c =
   1.694 +  let
   1.695 +    val specs = the_default Inttab.empty (Symtab.lookup specified c);
   1.696 +    fun is_monoT (Type (_, Ts)) = forall is_monoT Ts
   1.697 +      | is_monoT _ = false;
   1.698 +    val is_mono =
   1.699 +      Inttab.is_empty specs orelse
   1.700 +        Inttab.min_key specs = Inttab.max_key specs andalso
   1.701 +        is_monoT (snd (the (Inttab.lookup specs (the (Inttab.min_key specs)))));
   1.702 +  in if is_mono then Symtab.update (c, ()) else Symtab.remove (K true) (c, ()) end;
   1.703  
   1.704  
   1.705 -(* external interfaces *)
   1.706 +(* define consts *)
   1.707 +
   1.708 +fun err_cyclic cycles =
   1.709 +  error ("Cyclic dependency of constants:\n" ^
   1.710 +    cat_lines (map (space_implode " -> " o map quote o rev) cycles));
   1.711  
   1.712 -fun declare thy const defs =
   1.713 -  if_none (try (declare'' thy defs) const) defs;
   1.714 +fun define const_type name lhs rhs = map_defs (fn (consts, specified, monomorphic) =>
   1.715 +  let
   1.716 +    fun declare (a, _) = Graph.default_node (a, const_type a);
   1.717 +    fun add_deps (a, bs) G = Graph.add_deps_acyclic (a, bs) G
   1.718 +      handle Graph.CYCLES cycles => err_cyclic cycles;
   1.719 +
   1.720 +    val (c, T) = lhs;
   1.721 +    val no_overloading = Type.raw_instance (const_type c, T);
   1.722  
   1.723 -fun define thy const name rhs defs =
   1.724 -  define'' thy defs const name rhs
   1.725 -    handle DEFS msg => sys_error msg
   1.726 -      | CIRCULAR path => error (defs_circular (Sign.pp thy) path)
   1.727 -      | INFINITE_CHAIN path => error (defs_infinite_chain (Sign.pp thy) path)
   1.728 -      | CLASH (_, def1, def2) => error (defs_clash def1 def2)
   1.729 -      | FINAL const => error (defs_final (Sign.pp thy) const);
   1.730 +    val consts' =
   1.731 +      consts |> declare lhs |> fold declare rhs
   1.732 +      |> K no_overloading ? add_deps (c, map #1 rhs);
   1.733 +    val specified' =
   1.734 +      specified |> Symtab.default (c, Inttab.empty)
   1.735 +      |> Symtab.map_entry c (Inttab.update (serial (), (name, T)) #> tap (check_specified c));
   1.736 +    val monomorphic' = monomorphic |> update_monomorphic specified' c;
   1.737 +  in (consts', specified', monomorphic') end);
   1.738 +
   1.739 +
   1.740 +(* empty and merge *)
   1.741  
   1.742 -fun finalize thy const defs =
   1.743 -  finalize'' thy defs const handle DEFS msg => sys_error msg;
   1.744 +val empty = make_defs (Graph.empty, Symtab.empty, Symtab.empty);
   1.745  
   1.746 -fun merge pp defs1 defs2 =
   1.747 -  merge'' defs1 defs2
   1.748 -    handle CIRCULAR namess => error (defs_circular pp namess)
   1.749 -      | INFINITE_CHAIN namess => error (defs_infinite_chain pp namess);
   1.750 +fun merge pp
   1.751 +   (Defs {consts = consts1, specified = specified1, monomorphic},
   1.752 +    Defs {consts = consts2, specified = specified2, ...}) =
   1.753 +  let
   1.754 +    val consts' = (consts1, consts2) |> Graph.merge_acyclic (K true)
   1.755 +      handle Graph.CYCLES cycles => err_cyclic cycles;
   1.756 +    val specified' = (specified1, specified2)
   1.757 +      |> Symtab.join (fn c => Inttab.merge (K true) #> tap (check_specified c) #> SOME);
   1.758 +    val monomorphic' = monomorphic
   1.759 +      |> Symtab.fold (update_monomorphic specified' o #1) specified';
   1.760 +  in make_defs (consts', specified', monomorphic') end;
   1.761  
   1.762  end;
   1.763 -
   1.764 -(*
   1.765 -
   1.766 -fun tvar name = TVar ((name, 0), [])
   1.767 -
   1.768 -val bool = Type ("bool", [])
   1.769 -val int = Type ("int", [])
   1.770 -val lam = Type("lam", [])
   1.771 -val alpha = tvar "'a"
   1.772 -val beta = tvar "'b"
   1.773 -val gamma = tvar "'c"
   1.774 -fun pair a b = Type ("pair", [a,b])
   1.775 -fun prm a = Type ("prm", [a])
   1.776 -val name = Type ("name", [])
   1.777 -
   1.778 -val _ = print "make empty"
   1.779 -val g = Defs.empty
   1.780 -
   1.781 -val _ = print "declare perm"
   1.782 -val g = Defs.declare g ("perm", prm alpha --> beta --> beta)
   1.783 -
   1.784 -val _ = print "declare permF"
   1.785 -val g = Defs.declare g ("permF", prm alpha --> lam --> lam)
   1.786 -
   1.787 -val _ = print "define perm (1)"
   1.788 -val g = Defs.define g ("perm", prm alpha --> (beta --> gamma) --> (beta --> gamma)) "perm_fun"
   1.789 -        [("perm", prm alpha --> gamma --> gamma), ("perm", prm alpha --> beta --> beta)]
   1.790 -
   1.791 -val _ = print "define permF (1)"
   1.792 -val g = Defs.define g ("permF", prm alpha --> lam --> lam) "permF_app"
   1.793 -        ([("perm", prm alpha --> lam --> lam),
   1.794 -         ("perm", prm alpha --> lam --> lam),
   1.795 -         ("perm", prm alpha --> lam --> lam),
   1.796 -         ("perm", prm alpha --> name --> name)])
   1.797 -
   1.798 -val _ = print "define perm (2)"
   1.799 -val g = Defs.define g ("perm", prm alpha --> lam --> lam) "perm_lam"
   1.800 -        [("permF", (prm alpha --> lam --> lam))]
   1.801 -
   1.802 -*)