tuned interfaces declare, define, finalize, merge:
authorwenzelm
Tue Jul 19 17:21:49 2005 +0200 (2005-07-19)
changeset 16877e92cba1d4842
parent 16876 f57b38cced32
child 16878 07213f0e291f
tuned interfaces declare, define, finalize, merge:
canonical argument order, produce errors;
tuned checkT';
src/Pure/defs.ML
     1.1 --- a/src/Pure/defs.ML	Tue Jul 19 17:21:47 2005 +0200
     1.2 +++ b/src/Pure/defs.ML	Tue Jul 19 17:21:49 2005 +0200
     1.3 @@ -2,45 +2,33 @@
     1.4      ID:         $Id$
     1.5      Author:     Steven Obua, TU Muenchen
     1.6  
     1.7 -    Checks if definitions preserve consistency of logic by enforcing 
     1.8 -    that there are no cyclic definitions. The algorithm is described in 
     1.9 -    "An Algorithm for Determining Definitional Cycles in Higher-Order Logic with Overloading", 
    1.10 +    Checks if definitions preserve consistency of logic by enforcing
    1.11 +    that there are no cyclic definitions. The algorithm is described in
    1.12 +    "An Algorithm for Determining Definitional Cycles in Higher-Order Logic with Overloading",
    1.13      Steven Obua, technical report, to be written :-)
    1.14  *)
    1.15  
    1.16 -signature DEFS = sig
    1.17 -    
    1.18 +signature DEFS =
    1.19 +sig
    1.20    type graph
    1.21 -       
    1.22 -  exception DEFS of string
    1.23 -  exception CIRCULAR of (typ * string * string) list
    1.24 -  exception INFINITE_CHAIN of (typ * string * string) list 
    1.25 -  exception FINAL of string * typ
    1.26 -  exception CLASH of string * string * string
    1.27 -                     
    1.28 -  val empty : graph
    1.29 -  val declare : graph -> string * typ -> graph  (* exception DEFS *)
    1.30 -  val define : graph -> string * typ -> string -> (string * typ) list -> graph 
    1.31 -    (* exception DEFS, CIRCULAR, INFINITE_CHAIN, CLASH, FINAL *)   
    1.32 -                                                                     
    1.33 -  val finalize : graph -> string * typ -> graph (* exception DEFS *)
    1.34 +  val empty: graph
    1.35 +  val declare: string * typ -> graph -> graph
    1.36 +  val define: Pretty.pp -> string * typ -> string -> (string * typ) list -> graph -> graph
    1.37 +  val finalize: string * typ -> graph -> graph
    1.38 +  val merge: Pretty.pp -> graph -> graph -> graph
    1.39  
    1.40    val finals : graph -> (typ list) Symtab.table
    1.41  
    1.42 -  val merge : graph -> graph -> graph (* exception CIRCULAR, INFINITE_CHAIN, CLASH *)
    1.43 -
    1.44    (* If set to true then the exceptions CIRCULAR and INFINITE_CHAIN return the full
    1.45 -     chain of definitions that lead to the exception. In the beginning, chain_history 
    1.46 +     chain of definitions that lead to the exception. In the beginning, chain_history
    1.47       is initialized with the Isabelle environment variable DEFS_CHAIN_HISTORY. *)
    1.48    val set_chain_history : bool -> unit
    1.49    val chain_history : unit -> bool
    1.50  
    1.51    datatype overloadingstate = Open | Closed | Final
    1.52 -  
    1.53  
    1.54    val overloading_info : graph -> string -> (typ * (string*typ) list * overloadingstate) option
    1.55    val fast_overloading_info : graph -> string -> (typ * int * overloadingstate) option
    1.56 -
    1.57  end
    1.58  
    1.59  structure Defs :> DEFS = struct
    1.60 @@ -53,14 +41,14 @@
    1.61  datatype node = Node of
    1.62           typ  (* most general type of constant *)
    1.63           * defnode Symtab.table
    1.64 -             (* a table of defnodes, each corresponding to 1 definition of the 
    1.65 +             (* a table of defnodes, each corresponding to 1 definition of the
    1.66                  constant for a particular type, indexed by axiom name *)
    1.67 -         * (unit Symtab.table) Symtab.table 
    1.68 -             (* a table of all back referencing defnodes to this node, 
    1.69 +         * (unit Symtab.table) Symtab.table
    1.70 +             (* a table of all back referencing defnodes to this node,
    1.71                  indexed by node name of the defnodes *)
    1.72           * typ list (* a list of all finalized types *)
    1.73           * overloadingstate
    1.74 -     
    1.75 +
    1.76       and defnode = Defnode of
    1.77           typ  (* type of the constant in this particular definition *)
    1.78           * (edgelabel list) Symtab.table (* The edges, grouped by nodes. *)
    1.79 @@ -68,20 +56,20 @@
    1.80  fun getnode graph noderef = the (Symtab.lookup (graph, noderef))
    1.81  fun get_nodedefs (Node (_, defs, _, _, _)) = defs
    1.82  fun get_defnode (Node (_, defs, _, _, _)) defname = Symtab.lookup (defs, defname)
    1.83 -fun get_defnode' graph noderef defname = 
    1.84 +fun get_defnode' graph noderef defname =
    1.85      Symtab.lookup (get_nodedefs (the (Symtab.lookup (graph, noderef))), defname)
    1.86  
    1.87  fun table_size table = Symtab.foldl (fn (x, _) => x+1) (0, table)
    1.88 -        
    1.89 +
    1.90  datatype graphaction = Declare of string * typ
    1.91 -		     | Define of string * typ * string * string * (string * typ) list
    1.92 -		     | Finalize of string * typ
    1.93 +                     | Define of string * typ * string * string * (string * typ) list
    1.94 +                     | Finalize of string * typ
    1.95  
    1.96  type graph = int * (string Symtab.table) * (graphaction list) * (node Symtab.table)
    1.97 -             
    1.98 -val CHAIN_HISTORY = 
    1.99 +
   1.100 +val CHAIN_HISTORY =
   1.101      let
   1.102 -      fun f c = if Char.isSpace c then "" else String.str (Char.toUpper c) 
   1.103 +      fun f c = if Char.isSpace c then "" else String.str (Char.toUpper c)
   1.104        val env = String.translate f (getenv "DEFS_CHAIN_HISTORY")
   1.105      in
   1.106        ref (env = "ON" orelse env = "TRUE")
   1.107 @@ -100,74 +88,56 @@
   1.108  
   1.109  fun def_err s = raise (DEFS s)
   1.110  
   1.111 -fun no_forwards defs = 
   1.112 -    Symtab.foldl 
   1.113 -    (fn (closed, (_, Defnode (_, edges))) => 
   1.114 +fun no_forwards defs =
   1.115 +    Symtab.foldl
   1.116 +    (fn (closed, (_, Defnode (_, edges))) =>
   1.117          if not closed then false else Symtab.is_empty edges)
   1.118      (true, defs)
   1.119  
   1.120 -exception No_Change;
   1.121 +fun checkT' (Type (a, Ts)) = Type (a, map checkT' Ts)
   1.122 +  | checkT' (TFree (a, _)) = TVar ((a, 0), [])        (* FIXME !? *)
   1.123 +  | checkT' (TVar ((a, 0), _)) = TVar ((a, 0), [])
   1.124 +  | checkT' (T as TVar _) = raise TYPE ("Illegal schematic type variable encountered", [T], []);
   1.125  
   1.126 -fun map_nc f list = 
   1.127 -    let 
   1.128 -      val changed = ref false
   1.129 -      fun f' x = 
   1.130 -          let 
   1.131 -            val x' = f x  
   1.132 -            val _ = changed := true
   1.133 -          in
   1.134 -            x'
   1.135 -          end handle No_Change => x
   1.136 -      val list' = map f' list
   1.137 -    in
   1.138 -      if !changed then list' else raise No_Change
   1.139 -    end
   1.140 +val checkT = Term.compress_type o checkT';
   1.141  
   1.142 -fun checkT' (t as (Type (a, Ts))) = (Type (a, map_nc checkT' Ts) handle No_Change => t)
   1.143 -  | checkT' (t as (TVar ((a, 0), []))) = raise No_Change
   1.144 -  | checkT' (t as (TVar ((a, 0), _))) = TVar ((a, 0), [])
   1.145 -  | checkT' (t as (TFree (a, _))) = TVar ((a, 0), [])
   1.146 -  | checkT' _ = def_err "type is not clean"
   1.147 -
   1.148 -fun checkT t = Term.compress_type (checkT' t handle No_Change => t)
   1.149 -
   1.150 -fun rename ty1 ty2 = incr_tvar ((maxidx_of_typ ty1)+1) ty2;  
   1.151 +fun rename ty1 ty2 = Logic.incr_tvar ((maxidx_of_typ ty1)+1) ty2;
   1.152  
   1.153  fun subst_incr_tvar inc t =
   1.154 -    if (inc > 0) then 
   1.155 +    if (inc > 0) then
   1.156        let
   1.157 -	val tv = typ_tvars t
   1.158 -	val t' = incr_tvar inc t
   1.159 -	fun update_subst (((n,i), _), s) =
   1.160 -	    Vartab.update (((n, i), ([], TVar ((n, i+inc), []))), s)
   1.161 +        val tv = typ_tvars t
   1.162 +        val t' = Logic.incr_tvar inc t
   1.163 +        fun update_subst (((n,i), _), s) =
   1.164 +            Vartab.update (((n, i), ([], TVar ((n, i+inc), []))), s)
   1.165        in
   1.166 -	(t',List.foldl update_subst Vartab.empty tv)
   1.167 -      end	
   1.168 +        (t',List.foldl update_subst Vartab.empty tv)
   1.169 +      end
   1.170      else
   1.171        (t, Vartab.empty)
   1.172 -    
   1.173 +
   1.174  fun subst s ty = Envir.norm_type s ty
   1.175 -                 
   1.176 +
   1.177  fun subst_history s history = map (fn (ty, cn, dn) => (subst s ty, cn, dn)) history
   1.178 -                              
   1.179 +
   1.180  fun is_instance instance_ty general_ty =
   1.181      Type.typ_instance Type.empty_tsig (instance_ty, general_ty)
   1.182 -    
   1.183 +
   1.184  fun is_instance_r instance_ty general_ty =
   1.185      is_instance instance_ty (rename instance_ty general_ty)
   1.186 -    
   1.187 -fun unify ty1 ty2 = 
   1.188 +
   1.189 +fun unify ty1 ty2 =
   1.190      SOME (fst (Type.unify Type.empty_tsig (Vartab.empty, 0) (ty1, ty2)))
   1.191      handle Type.TUNIFY => NONE
   1.192 -                            
   1.193 -(* 
   1.194 -   Unifies ty1 and ty2, renaming ty1 and ty2 so that they have greater indices than max and 
   1.195 -   so that they are different. All indices in ty1 and ty2 are supposed to be less than or 
   1.196 +
   1.197 +(*
   1.198 +   Unifies ty1 and ty2, renaming ty1 and ty2 so that they have greater indices than max and
   1.199 +   so that they are different. All indices in ty1 and ty2 are supposed to be less than or
   1.200     equal to max.
   1.201 -   Returns SOME (max', s1, s2), so that s1(ty1) = s2(ty2) and max' is greater or equal than 
   1.202 +   Returns SOME (max', s1, s2), so that s1(ty1) = s2(ty2) and max' is greater or equal than
   1.203     all indices in s1, s2, ty1, ty2.
   1.204  *)
   1.205 -fun unify_r max ty1 ty2 = 
   1.206 +fun unify_r max ty1 ty2 =
   1.207      let
   1.208        val max = Int.max(max, 0)
   1.209        val max1 = max (* >= maxidx_of_typ ty1 *)
   1.210 @@ -175,35 +145,35 @@
   1.211        val max = Int.max(max, Int.max (max1, max2))
   1.212        val (ty1, s1) = subst_incr_tvar (max + 1) ty1
   1.213        val (ty2, s2) = subst_incr_tvar (max + max1 + 2) ty2
   1.214 -      val max = max + max1 + max2 + 2	
   1.215 +      val max = max + max1 + max2 + 2
   1.216        fun merge a b = Vartab.merge (fn _ => false) (a, b)
   1.217      in
   1.218        case unify ty1 ty2 of
   1.219 -	NONE => NONE
   1.220 +        NONE => NONE
   1.221        | SOME s => SOME (max, merge s1 s, merge s2 s)
   1.222      end
   1.223 -    
   1.224 +
   1.225  fun can_be_unified_r ty1 ty2 =
   1.226      let
   1.227        val ty2 = rename ty1 ty2
   1.228      in
   1.229        case unify ty1 ty2 of
   1.230 -	NONE => false
   1.231 +        NONE => false
   1.232        | _ => true
   1.233      end
   1.234 -    
   1.235 +
   1.236  fun can_be_unified ty1 ty2 =
   1.237      case unify ty1 ty2 of
   1.238        NONE => false
   1.239      | _ => true
   1.240 -           
   1.241 +
   1.242  fun normalize_edge_idx (edge as (maxidx, u1, v1, history)) =
   1.243      if maxidx <= 1000000 then edge else
   1.244      let
   1.245 -      
   1.246 -      fun idxlist idx extract_ty inject_ty (tab, max) ts = 
   1.247 -          foldr 
   1.248 -            (fn (e, ((tab, max), ts)) => 
   1.249 +
   1.250 +      fun idxlist idx extract_ty inject_ty (tab, max) ts =
   1.251 +          foldr
   1.252 +            (fn (e, ((tab, max), ts)) =>
   1.253                  let
   1.254                    val ((tab, max), ty) = idx (tab, max) (extract_ty e)
   1.255                    val e = inject_ty (ty, e)
   1.256 @@ -211,60 +181,60 @@
   1.257                    ((tab, max), e::ts)
   1.258                  end)
   1.259              ((tab,max), []) ts
   1.260 -          
   1.261 -      fun idx (tab,max) (TVar ((a,i),_)) = 
   1.262 -          (case Inttab.lookup (tab, i) of 
   1.263 +
   1.264 +      fun idx (tab,max) (TVar ((a,i),_)) =
   1.265 +          (case Inttab.lookup (tab, i) of
   1.266               SOME j => ((tab, max), TVar ((a,j),[]))
   1.267             | NONE => ((Inttab.update ((i, max), tab), max+1), TVar ((a,max),[])))
   1.268 -        | idx (tab,max) (Type (t, ts)) = 
   1.269 -          let 
   1.270 +        | idx (tab,max) (Type (t, ts)) =
   1.271 +          let
   1.272              val ((tab, max), ts) = idxlist idx I fst (tab, max) ts
   1.273            in
   1.274              ((tab,max), Type (t, ts))
   1.275            end
   1.276          | idx (tab, max) ty = ((tab, max), ty)
   1.277 -      
   1.278 +
   1.279        val ((tab,max), u1) = idx (Inttab.empty, 0) u1
   1.280        val ((tab,max), v1) = idx (tab, max) v1
   1.281 -      val ((tab,max), history) = 
   1.282 +      val ((tab,max), history) =
   1.283            idxlist idx
   1.284 -            (fn (ty,_,_) => ty) 
   1.285 -            (fn (ty, (_, s1, s2)) => (ty, s1, s2)) 
   1.286 +            (fn (ty,_,_) => ty)
   1.287 +            (fn (ty, (_, s1, s2)) => (ty, s1, s2))
   1.288              (tab, max) history
   1.289      in
   1.290        (max, u1, v1, history)
   1.291      end
   1.292 -                        
   1.293 +
   1.294  fun compare_edges (e1 as (maxidx1, u1, v1, history1)) (e2 as (maxidx2, u2, v2, history2)) =
   1.295      let
   1.296        val t1 = u1 --> v1
   1.297 -      val t2 = incr_tvar (maxidx1+1) (u2 --> v2)
   1.298 +      val t2 = Logic.incr_tvar (maxidx1+1) (u2 --> v2)
   1.299      in
   1.300        if (is_instance t1 t2) then
   1.301 -	(if is_instance t2 t1 then
   1.302 -	   SOME (int_ord (length history2, length history1))
   1.303 -	 else
   1.304 -	   SOME LESS)
   1.305 +        (if is_instance t2 t1 then
   1.306 +           SOME (int_ord (length history2, length history1))
   1.307 +         else
   1.308 +           SOME LESS)
   1.309        else if (is_instance t2 t1) then
   1.310 -	SOME GREATER
   1.311 +        SOME GREATER
   1.312        else
   1.313 -	NONE
   1.314 +        NONE
   1.315      end
   1.316  
   1.317  fun merge_edges_1 (x, []) = [x]
   1.318 -  | merge_edges_1 (x, (y::ys)) = 
   1.319 +  | merge_edges_1 (x, (y::ys)) =
   1.320      (case compare_edges x y of
   1.321         SOME LESS => (y::ys)
   1.322       | SOME EQUAL => (y::ys)
   1.323       | SOME GREATER => merge_edges_1 (x, ys)
   1.324       | NONE => y::(merge_edges_1 (x, ys)))
   1.325 -    
   1.326 +
   1.327  fun merge_edges xs ys = foldl merge_edges_1 xs ys
   1.328  
   1.329  fun declare' (g as (cost, axmap, actions, graph)) (cty as (name, ty)) =
   1.330 -    (cost, axmap, (Declare cty)::actions, 
   1.331 +    (cost, axmap, (Declare cty)::actions,
   1.332       Symtab.update_new ((name, Node (ty, Symtab.empty, Symtab.empty, [], Open)), graph))
   1.333 -    handle Symtab.DUP _ => 
   1.334 +    handle Symtab.DUP _ =>
   1.335             let
   1.336               val (Node (gty, _, _, _, _)) = the (Symtab.lookup(graph, name))
   1.337             in
   1.338 @@ -274,7 +244,7 @@
   1.339                 def_err "constant is already declared with different type"
   1.340             end
   1.341  
   1.342 -fun declare g (name, ty) = declare' g (name, checkT ty)
   1.343 +fun declare'' g (name, ty) = declare' g (name, checkT ty)
   1.344  
   1.345  val axcounter = ref (IntInf.fromInt 0)
   1.346  fun newaxname axmap axname =
   1.347 @@ -286,9 +256,9 @@
   1.348        (Symtab.update ((axname', axname), axmap), axname')
   1.349      end
   1.350  
   1.351 -fun translate_ex axmap x = 
   1.352 +fun translate_ex axmap x =
   1.353      let
   1.354 -      fun translate (ty, nodename, axname) = 
   1.355 +      fun translate (ty, nodename, axname) =
   1.356            (ty, nodename, the (Symtab.lookup (axmap, axname)))
   1.357      in
   1.358        case x of
   1.359 @@ -299,107 +269,107 @@
   1.360  
   1.361  fun define' (cost, axmap, actions, graph) (mainref, ty) axname orig_axname body =
   1.362      let
   1.363 -      val mainnode  = (case Symtab.lookup (graph, mainref) of 
   1.364 -			 NONE => def_err ("constant "^mainref^" is not declared")
   1.365 -		       | SOME n => n)
   1.366 +      val mainnode  = (case Symtab.lookup (graph, mainref) of
   1.367 +                         NONE => def_err ("constant "^mainref^" is not declared")
   1.368 +                       | SOME n => n)
   1.369        val (Node (gty, defs, backs, finals, _)) = mainnode
   1.370 -      val _ = (if is_instance_r ty gty then () 
   1.371 +      val _ = (if is_instance_r ty gty then ()
   1.372                 else def_err "type of constant does not match declared type")
   1.373 -      fun check_def (s, Defnode (ty', _)) = 
   1.374 -          (if can_be_unified_r ty ty' then 
   1.375 -	     raise (CLASH (mainref, axname, s))
   1.376 -	   else if s = axname then
   1.377 -	     def_err "name of axiom is already used for another definition of this constant"
   1.378 -	   else false)	
   1.379 +      fun check_def (s, Defnode (ty', _)) =
   1.380 +          (if can_be_unified_r ty ty' then
   1.381 +             raise (CLASH (mainref, axname, s))
   1.382 +           else if s = axname then
   1.383 +             def_err "name of axiom is already used for another definition of this constant"
   1.384 +           else false)
   1.385        val _ = Symtab.exists check_def defs
   1.386 -      fun check_final finalty = 
   1.387 -	  (if can_be_unified_r finalty ty then
   1.388 -	     raise (FINAL (mainref, finalty))
   1.389 -	   else
   1.390 -	     true)
   1.391 +      fun check_final finalty =
   1.392 +          (if can_be_unified_r finalty ty then
   1.393 +             raise (FINAL (mainref, finalty))
   1.394 +           else
   1.395 +             true)
   1.396        val _ = forall check_final finals
   1.397 -	             
   1.398 -      (* now we know that the only thing that can prevent acceptance of the definition 
   1.399 +
   1.400 +      (* now we know that the only thing that can prevent acceptance of the definition
   1.401           is a cyclic dependency *)
   1.402 -              
   1.403 +
   1.404        fun insert_edges edges (nodename, links) =
   1.405 -          (if links = [] then 
   1.406 +          (if links = [] then
   1.407               edges
   1.408             else
   1.409               let
   1.410                 val links = map normalize_edge_idx links
   1.411               in
   1.412 -               Symtab.update ((nodename, 
   1.413 -	                       case Symtab.lookup (edges, nodename) of
   1.414 -	                         NONE => links
   1.415 -	                       | SOME links' => merge_edges links' links),
   1.416 +               Symtab.update ((nodename,
   1.417 +                               case Symtab.lookup (edges, nodename) of
   1.418 +                                 NONE => links
   1.419 +                               | SOME links' => merge_edges links' links),
   1.420                                edges)
   1.421               end)
   1.422 -	 
   1.423 +
   1.424        fun make_edges ((bodyn, bodyty), edges) =
   1.425 -	  let
   1.426 -	    val bnode = 
   1.427 -		(case Symtab.lookup (graph, bodyn) of 
   1.428 -		   NONE => def_err "body of constant definition references undeclared constant"
   1.429 -		 | SOME x => x)
   1.430 -	    val (Node (general_btyp, bdefs, bbacks, bfinals, closed)) = bnode
   1.431 -	  in
   1.432 +          let
   1.433 +            val bnode =
   1.434 +                (case Symtab.lookup (graph, bodyn) of
   1.435 +                   NONE => def_err "body of constant definition references undeclared constant"
   1.436 +                 | SOME x => x)
   1.437 +            val (Node (general_btyp, bdefs, bbacks, bfinals, closed)) = bnode
   1.438 +          in
   1.439              if closed = Final then edges else
   1.440 -	    case unify_r 0 bodyty general_btyp of
   1.441 -	      NONE => edges
   1.442 -	    | SOME (maxidx, sigma1, sigma2) => 
   1.443 -              if exists (is_instance_r bodyty) bfinals then 
   1.444 +            case unify_r 0 bodyty general_btyp of
   1.445 +              NONE => edges
   1.446 +            | SOME (maxidx, sigma1, sigma2) =>
   1.447 +              if exists (is_instance_r bodyty) bfinals then
   1.448                  edges
   1.449                else
   1.450 -	        let
   1.451 -		  fun insert_trans_edges ((step1, edges), (nodename, links)) =
   1.452 +                let
   1.453 +                  fun insert_trans_edges ((step1, edges), (nodename, links)) =
   1.454                        let
   1.455                          val (maxidx1, alpha1, beta1, defname) = step1
   1.456 -                        fun connect (maxidx2, alpha2, beta2, history) = 
   1.457 -		            case unify_r (Int.max (maxidx1, maxidx2)) beta1 alpha2 of
   1.458 -		              NONE => NONE
   1.459 -		            | SOME (max, sleft, sright) =>				  
   1.460 -			      SOME (max, subst sleft alpha1, subst sright beta2, 
   1.461 -                                    if !CHAIN_HISTORY then   
   1.462 -			              ((subst sleft beta1, bodyn, defname)::
   1.463 -				       (subst_history sright history))
   1.464 -                                    else [])            
   1.465 +                        fun connect (maxidx2, alpha2, beta2, history) =
   1.466 +                            case unify_r (Int.max (maxidx1, maxidx2)) beta1 alpha2 of
   1.467 +                              NONE => NONE
   1.468 +                            | SOME (max, sleft, sright) =>
   1.469 +                              SOME (max, subst sleft alpha1, subst sright beta2,
   1.470 +                                    if !CHAIN_HISTORY then
   1.471 +                                      ((subst sleft beta1, bodyn, defname)::
   1.472 +                                       (subst_history sright history))
   1.473 +                                    else [])
   1.474                          val links' = List.mapPartial connect links
   1.475                        in
   1.476                          (step1, insert_edges edges (nodename, links'))
   1.477                        end
   1.478 -                                                                
   1.479 +
   1.480                    fun make_edges' ((swallowed, edges),
   1.481                                     (def_name, Defnode (def_ty, def_edges))) =
   1.482 -		      if swallowed then
   1.483 -		        (swallowed, edges)
   1.484 -		      else 
   1.485 -		        (case unify_r 0 bodyty def_ty of
   1.486 -			   NONE => (swallowed, edges)
   1.487 -		         | SOME (maxidx, sigma1, sigma2) => 
   1.488 -			   (is_instance_r bodyty def_ty,
   1.489 -                            snd (Symtab.foldl insert_trans_edges 
   1.490 +                      if swallowed then
   1.491 +                        (swallowed, edges)
   1.492 +                      else
   1.493 +                        (case unify_r 0 bodyty def_ty of
   1.494 +                           NONE => (swallowed, edges)
   1.495 +                         | SOME (maxidx, sigma1, sigma2) =>
   1.496 +                           (is_instance_r bodyty def_ty,
   1.497 +                            snd (Symtab.foldl insert_trans_edges
   1.498                                (((maxidx, subst sigma1 ty, subst sigma2 def_ty, def_name),
   1.499                                  edges), def_edges))))
   1.500 -          	  val (swallowed, edges) = Symtab.foldl make_edges' ((false, edges), bdefs)
   1.501 -	        in
   1.502 -		  if swallowed then 
   1.503 -		    edges
   1.504 -		  else 
   1.505 -                    insert_edges edges 
   1.506 +                  val (swallowed, edges) = Symtab.foldl make_edges' ((false, edges), bdefs)
   1.507 +                in
   1.508 +                  if swallowed then
   1.509 +                    edges
   1.510 +                  else
   1.511 +                    insert_edges edges
   1.512                      (bodyn, [(maxidx, subst sigma1 ty, subst sigma2 general_btyp,[])])
   1.513 -	        end
   1.514 -	  end                    
   1.515 -          
   1.516 +                end
   1.517 +          end
   1.518 +
   1.519        val edges = foldl make_edges Symtab.empty body
   1.520 -                  				               
   1.521 -      (* We also have to add the backreferences that this new defnode induces. *)  
   1.522 +
   1.523 +      (* We also have to add the backreferences that this new defnode induces. *)
   1.524        fun install_backrefs (graph, (noderef, links)) =
   1.525            if links <> [] then
   1.526              let
   1.527                val (Node (ty, defs, backs, finals, closed)) = getnode graph noderef
   1.528 -              val _ = if closed = Final then 
   1.529 -                        sys_error ("install_backrefs: closed node cannot be updated") 
   1.530 +              val _ = if closed = Final then
   1.531 +                        sys_error ("install_backrefs: closed node cannot be updated")
   1.532                        else ()
   1.533                val defnames =
   1.534                    (case Symtab.lookup (backs, mainref) of
   1.535 @@ -412,72 +382,72 @@
   1.536              end
   1.537            else
   1.538              graph
   1.539 -            
   1.540 +
   1.541        val graph = Symtab.foldl install_backrefs (graph, edges)
   1.542 -                  
   1.543 +
   1.544        val (Node (_, _, backs, _, closed)) = getnode graph mainref
   1.545 -      val closed = 
   1.546 -          if closed = Final then sys_error "define: closed node" 
   1.547 +      val closed =
   1.548 +          if closed = Final then sys_error "define: closed node"
   1.549            else if closed = Open andalso is_instance_r gty ty then Closed else closed
   1.550  
   1.551        val thisDefnode = Defnode (ty, edges)
   1.552 -      val graph = Symtab.update ((mainref, Node (gty, Symtab.update_new 
   1.553 +      val graph = Symtab.update ((mainref, Node (gty, Symtab.update_new
   1.554          ((axname, thisDefnode), defs), backs, finals, closed)), graph)
   1.555 -		                
   1.556 -      (* Now we have to check all backreferences to this node and inform them about 
   1.557 +
   1.558 +      (* Now we have to check all backreferences to this node and inform them about
   1.559           the new defnode. In this section we also check for circularity. *)
   1.560        fun update_backrefs ((backs, graph), (noderef, defnames)) =
   1.561 -	  let
   1.562 -	    fun update_defs ((defnames, graph),(defname, _)) =
   1.563 -		let
   1.564 -                  val (Node (nodety, nodedefs, nodebacks, nodefinals, closed)) = 
   1.565 +          let
   1.566 +            fun update_defs ((defnames, graph),(defname, _)) =
   1.567 +                let
   1.568 +                  val (Node (nodety, nodedefs, nodebacks, nodefinals, closed)) =
   1.569                        getnode graph noderef
   1.570                    val _ = if closed = Final then sys_error "update_defs: closed node" else ()
   1.571 -		  val (Defnode (def_ty, defnode_edges)) = 
   1.572 +                  val (Defnode (def_ty, defnode_edges)) =
   1.573                        the (Symtab.lookup (nodedefs, defname))
   1.574 -		  val edges = the (Symtab.lookup (defnode_edges, mainref))
   1.575 +                  val edges = the (Symtab.lookup (defnode_edges, mainref))
   1.576                    val refclosed = ref false
   1.577 - 					
   1.578 -	          (* the type of thisDefnode is ty *)
   1.579 -		  fun update (e as (max, alpha, beta, history), (changed, edges)) = 
   1.580 -		      case unify_r max beta ty of
   1.581 -			NONE => (changed, e::edges)
   1.582 -		      | SOME (max', s_beta, s_ty) =>
   1.583 -			let
   1.584 -			  val alpha' = subst s_beta alpha
   1.585 -			  val ty' = subst s_ty ty				      
   1.586 -			  val _ = 
   1.587 -			      if noderef = mainref andalso defname = axname then
   1.588 -				(case unify alpha' ty' of
   1.589 -				   NONE => 
   1.590 -				   if (is_instance_r ty' alpha') then
   1.591 -				     raise (INFINITE_CHAIN (
   1.592 -					    (alpha', mainref, axname)::
   1.593 -					    (subst_history s_beta history)@
   1.594 -					    [(ty', mainref, axname)]))
   1.595 -				   else ()
   1.596 -				 | SOME s => 
   1.597 +
   1.598 +                  (* the type of thisDefnode is ty *)
   1.599 +                  fun update (e as (max, alpha, beta, history), (changed, edges)) =
   1.600 +                      case unify_r max beta ty of
   1.601 +                        NONE => (changed, e::edges)
   1.602 +                      | SOME (max', s_beta, s_ty) =>
   1.603 +                        let
   1.604 +                          val alpha' = subst s_beta alpha
   1.605 +                          val ty' = subst s_ty ty
   1.606 +                          val _ =
   1.607 +                              if noderef = mainref andalso defname = axname then
   1.608 +                                (case unify alpha' ty' of
   1.609 +                                   NONE =>
   1.610 +                                   if (is_instance_r ty' alpha') then
   1.611 +                                     raise (INFINITE_CHAIN (
   1.612 +                                            (alpha', mainref, axname)::
   1.613 +                                            (subst_history s_beta history)@
   1.614 +                                            [(ty', mainref, axname)]))
   1.615 +                                   else ()
   1.616 +                                 | SOME s =>
   1.617                                     raise (CIRCULAR (
   1.618 -					  (subst s alpha', mainref, axname)::
   1.619 -					  (subst_history s (subst_history s_beta history))@
   1.620 -					  [(subst s ty', mainref, axname)])))
   1.621 -			      else ()                             
   1.622 -			in
   1.623 -			  if is_instance_r beta ty then
   1.624 -			    (true, edges)
   1.625 -			  else
   1.626 -			    (changed, e::edges)
   1.627 -			end		    			   			       
   1.628 -                  
   1.629 +                                          (subst s alpha', mainref, axname)::
   1.630 +                                          (subst_history s (subst_history s_beta history))@
   1.631 +                                          [(subst s ty', mainref, axname)])))
   1.632 +                              else ()
   1.633 +                        in
   1.634 +                          if is_instance_r beta ty then
   1.635 +                            (true, edges)
   1.636 +                          else
   1.637 +                            (changed, e::edges)
   1.638 +                        end
   1.639 +
   1.640                    val (changed, edges') = foldl update (false, []) edges
   1.641 -                  val defnames' = if edges' = [] then 
   1.642 -                                    defnames 
   1.643 -                                  else 
   1.644 +                  val defnames' = if edges' = [] then
   1.645 +                                    defnames
   1.646 +                                  else
   1.647                                      Symtab.update ((defname, ()), defnames)
   1.648                  in
   1.649                    if changed then
   1.650                      let
   1.651 -                      val defnode_edges' = 
   1.652 +                      val defnode_edges' =
   1.653                            if edges' = [] then
   1.654                              Symtab.delete mainref defnode_edges
   1.655                            else
   1.656 @@ -485,48 +455,48 @@
   1.657                        val defnode' = Defnode (def_ty, defnode_edges')
   1.658                        val nodedefs' = Symtab.update ((defname, defnode'), nodedefs)
   1.659                        val closed = if closed = Closed andalso Symtab.is_empty defnode_edges'
   1.660 -                                      andalso no_forwards nodedefs' 
   1.661 +                                      andalso no_forwards nodedefs'
   1.662                                     then Final else closed
   1.663 -                      val graph' = 
   1.664 -                          Symtab.update 
   1.665 -                            ((noderef, 
   1.666 -                              Node (nodety, nodedefs', nodebacks, nodefinals, closed)),graph) 
   1.667 +                      val graph' =
   1.668 +                          Symtab.update
   1.669 +                            ((noderef,
   1.670 +                              Node (nodety, nodedefs', nodebacks, nodefinals, closed)),graph)
   1.671                      in
   1.672                        (defnames', graph')
   1.673                      end
   1.674                    else
   1.675                      (defnames', graph)
   1.676                  end
   1.677 -		    
   1.678 -	    val (defnames', graph') = Symtab.foldl update_defs 
   1.679 +
   1.680 +            val (defnames', graph') = Symtab.foldl update_defs
   1.681                                                     ((Symtab.empty, graph), defnames)
   1.682 -	  in
   1.683 -	    if Symtab.is_empty defnames' then 
   1.684 -	      (backs, graph')
   1.685 -	    else
   1.686 -	      let
   1.687 -		val backs' = Symtab.update_new ((noderef, defnames'), backs)
   1.688 -	      in
   1.689 -		(backs', graph')
   1.690 -	      end
   1.691 -	  end
   1.692 -        
   1.693 +          in
   1.694 +            if Symtab.is_empty defnames' then
   1.695 +              (backs, graph')
   1.696 +            else
   1.697 +              let
   1.698 +                val backs' = Symtab.update_new ((noderef, defnames'), backs)
   1.699 +              in
   1.700 +                (backs', graph')
   1.701 +              end
   1.702 +          end
   1.703 +
   1.704        val (backs, graph) = Symtab.foldl update_backrefs ((Symtab.empty, graph), backs)
   1.705 -                                        						 
   1.706 +
   1.707        (* If a Circular exception is thrown then we never reach this point. *)
   1.708        val (Node (gty, defs, _, finals, closed)) = getnode graph mainref
   1.709        val closed = if closed = Closed andalso no_forwards defs then Final else closed
   1.710 -      val graph = Symtab.update ((mainref, Node (gty, defs, backs, finals, closed)), graph) 
   1.711 +      val graph = Symtab.update ((mainref, Node (gty, defs, backs, finals, closed)), graph)
   1.712        val actions' = (Define (mainref, ty, axname, orig_axname, body))::actions
   1.713 -    in	    
   1.714 +    in
   1.715        (cost+3, axmap, actions', graph)
   1.716      end handle ex => translate_ex axmap ex
   1.717 -    
   1.718 -fun define (g as (cost, axmap, actions, graph)) (mainref, ty) orig_axname body =
   1.719 +
   1.720 +fun define'' (g as (cost, axmap, actions, graph)) (mainref, ty) orig_axname body =
   1.721      let
   1.722        val ty = checkT ty
   1.723 -      fun checkbody (n, t) = 
   1.724 -          let 
   1.725 +      fun checkbody (n, t) =
   1.726 +          let
   1.727              val (Node (_, _, _,_, closed)) = getnode graph n
   1.728            in
   1.729              case closed of
   1.730 @@ -539,27 +509,27 @@
   1.731        define' (cost, axmap, actions, graph) (mainref, ty) axname orig_axname body
   1.732      end
   1.733  
   1.734 -fun finalize' (cost, axmap, history, graph) (noderef, ty) = 
   1.735 -    case Symtab.lookup (graph, noderef) of 
   1.736 +fun finalize' (cost, axmap, history, graph) (noderef, ty) =
   1.737 +    case Symtab.lookup (graph, noderef) of
   1.738        NONE => def_err ("cannot finalize constant "^noderef^"; it is not declared")
   1.739      | SOME (Node (nodety, defs, backs, finals, closed)) =>
   1.740 -      let 
   1.741 -	val _ = 
   1.742 +      let
   1.743 +        val _ =
   1.744              if (not (is_instance_r ty nodety)) then
   1.745 -	      def_err ("only type instances of the declared constant "^
   1.746 +              def_err ("only type instances of the declared constant "^
   1.747                         noderef^" can be finalized")
   1.748 -	    else ()
   1.749 -	val _ = Symtab.exists 
   1.750 -                  (fn (def_name, Defnode (def_ty, _)) =>  
   1.751 -		      if can_be_unified_r ty def_ty then 
   1.752 -			def_err ("cannot finalize constant "^noderef^
   1.753 +            else ()
   1.754 +        val _ = Symtab.exists
   1.755 +                  (fn (def_name, Defnode (def_ty, _)) =>
   1.756 +                      if can_be_unified_r ty def_ty then
   1.757 +                        def_err ("cannot finalize constant "^noderef^
   1.758                                   "; clash with definition "^def_name)
   1.759 -		      else 
   1.760 -			false)
   1.761 -		  defs 
   1.762 -        
   1.763 +                      else
   1.764 +                        false)
   1.765 +                  defs
   1.766 +
   1.767          fun update_finals [] = SOME [ty]
   1.768 -          | update_finals (final_ty::finals) = 
   1.769 +          | update_finals (final_ty::finals) =
   1.770              (if is_instance_r ty final_ty then NONE
   1.771               else
   1.772                 case update_finals finals of
   1.773 @@ -568,99 +538,99 @@
   1.774                   if (is_instance_r final_ty ty) then
   1.775                     r
   1.776                   else
   1.777 -                   SOME (final_ty :: finals))                              
   1.778 -      in    
   1.779 +                   SOME (final_ty :: finals))
   1.780 +      in
   1.781          case update_finals finals of
   1.782            NONE => (cost, axmap, history, graph)
   1.783 -        | SOME finals => 
   1.784 -	  let
   1.785 -            val closed = if closed = Open andalso is_instance_r nodety ty then 
   1.786 -                           Closed else 
   1.787 +        | SOME finals =>
   1.788 +          let
   1.789 +            val closed = if closed = Open andalso is_instance_r nodety ty then
   1.790 +                           Closed else
   1.791                           closed
   1.792 -	    val graph = Symtab.update ((noderef, Node(nodety, defs, backs, finals, closed)), 
   1.793 +            val graph = Symtab.update ((noderef, Node(nodety, defs, backs, finals, closed)),
   1.794                                         graph)
   1.795 -	                
   1.796 -	    fun update_backref ((graph, backs), (backrefname, backdefnames)) =
   1.797 -		let
   1.798 -		  fun update_backdef ((graph, defnames), (backdefname, _)) = 
   1.799 -	              let 
   1.800 -			val (backnode as Node (backty, backdefs, backbacks, 
   1.801 -                                               backfinals, backclosed)) = 
   1.802 +
   1.803 +            fun update_backref ((graph, backs), (backrefname, backdefnames)) =
   1.804 +                let
   1.805 +                  fun update_backdef ((graph, defnames), (backdefname, _)) =
   1.806 +                      let
   1.807 +                        val (backnode as Node (backty, backdefs, backbacks,
   1.808 +                                               backfinals, backclosed)) =
   1.809                              getnode graph backrefname
   1.810 -			val (Defnode (def_ty, all_edges)) = 
   1.811 +                        val (Defnode (def_ty, all_edges)) =
   1.812                              the (get_defnode backnode backdefname)
   1.813  
   1.814 -			val (defnames', all_edges') = 
   1.815 -			    case Symtab.lookup (all_edges, noderef) of
   1.816 -			      NONE => sys_error "finalize: corrupt backref"
   1.817 -			    | SOME edges =>
   1.818 -			      let
   1.819 -				val edges' = List.filter (fn (_, _, beta, _) => 
   1.820 +                        val (defnames', all_edges') =
   1.821 +                            case Symtab.lookup (all_edges, noderef) of
   1.822 +                              NONE => sys_error "finalize: corrupt backref"
   1.823 +                            | SOME edges =>
   1.824 +                              let
   1.825 +                                val edges' = List.filter (fn (_, _, beta, _) =>
   1.826                                                               not (is_instance_r beta ty)) edges
   1.827 -			      in
   1.828 -				if edges' = [] then 
   1.829 -				  (defnames, Symtab.delete noderef all_edges)
   1.830 -				else
   1.831 -				  (Symtab.update ((backdefname, ()), defnames), 
   1.832 -				   Symtab.update ((noderef, edges'), all_edges))
   1.833 -			      end
   1.834 -			val defnode' = Defnode (def_ty, all_edges')
   1.835 +                              in
   1.836 +                                if edges' = [] then
   1.837 +                                  (defnames, Symtab.delete noderef all_edges)
   1.838 +                                else
   1.839 +                                  (Symtab.update ((backdefname, ()), defnames),
   1.840 +                                   Symtab.update ((noderef, edges'), all_edges))
   1.841 +                              end
   1.842 +                        val defnode' = Defnode (def_ty, all_edges')
   1.843                          val backdefs' = Symtab.update ((backdefname, defnode'), backdefs)
   1.844 -                        val backclosed' = if backclosed = Closed andalso 
   1.845 +                        val backclosed' = if backclosed = Closed andalso
   1.846                                               Symtab.is_empty all_edges'
   1.847                                               andalso no_forwards backdefs'
   1.848                                            then Final else backclosed
   1.849 -			val backnode' = 
   1.850 +                        val backnode' =
   1.851                              Node (backty, backdefs', backbacks, backfinals, backclosed')
   1.852 -		      in
   1.853 -			(Symtab.update ((backrefname, backnode'), graph), defnames') 
   1.854 -		      end
   1.855 -	              
   1.856 -		  val (graph', defnames') = 
   1.857 +                      in
   1.858 +                        (Symtab.update ((backrefname, backnode'), graph), defnames')
   1.859 +                      end
   1.860 +
   1.861 +                  val (graph', defnames') =
   1.862                        Symtab.foldl update_backdef ((graph, Symtab.empty), backdefnames)
   1.863 -		in
   1.864 -		  (graph', if Symtab.is_empty defnames' then backs 
   1.865 -			   else Symtab.update ((backrefname, defnames'), backs))
   1.866 -		end
   1.867 -	    val (graph', backs') = Symtab.foldl update_backref ((graph, Symtab.empty), backs)
   1.868 -	    val Node ( _, defs, _, _, closed) = getnode graph' noderef
   1.869 +                in
   1.870 +                  (graph', if Symtab.is_empty defnames' then backs
   1.871 +                           else Symtab.update ((backrefname, defnames'), backs))
   1.872 +                end
   1.873 +            val (graph', backs') = Symtab.foldl update_backref ((graph, Symtab.empty), backs)
   1.874 +            val Node ( _, defs, _, _, closed) = getnode graph' noderef
   1.875              val closed = if closed = Closed andalso no_forwards defs then Final else closed
   1.876 -	    val graph' = Symtab.update ((noderef, Node (nodety, defs, backs', 
   1.877 +            val graph' = Symtab.update ((noderef, Node (nodety, defs, backs',
   1.878                                                          finals, closed)), graph')
   1.879              val history' = (Finalize (noderef, ty)) :: history
   1.880 -	  in
   1.881 -	    (cost+1, axmap, history', graph')
   1.882 -	  end
   1.883 +          in
   1.884 +            (cost+1, axmap, history', graph')
   1.885 +          end
   1.886        end
   1.887 - 
   1.888 -fun finalize g (noderef, ty) = finalize' g (noderef, checkT ty) 
   1.889 +
   1.890 +fun finalize'' g (noderef, ty) = finalize' g (noderef, checkT ty)
   1.891  
   1.892  fun update_axname ax orig_ax (cost, axmap, history, graph) =
   1.893    (cost, Symtab.update ((ax, orig_ax), axmap), history, graph)
   1.894  
   1.895  fun merge' (Declare cty, g) = declare' g cty
   1.896 -  | merge' (Define (name, ty, axname, orig_axname, body), g as (cost, axmap, history, graph)) = 
   1.897 +  | merge' (Define (name, ty, axname, orig_axname, body), g as (cost, axmap, history, graph)) =
   1.898      (case Symtab.lookup (graph, name) of
   1.899         NONE => define' (update_axname axname orig_axname g) (name, ty) axname orig_axname body
   1.900 -     | SOME (Node (_, defs, _, _, _)) => 
   1.901 +     | SOME (Node (_, defs, _, _, _)) =>
   1.902         (case Symtab.lookup (defs, axname) of
   1.903 -	  NONE => define' (update_axname axname orig_axname g) (name, ty) axname orig_axname body
   1.904 -	| SOME _ => g))
   1.905 -  | merge' (Finalize finals, g) = finalize' g finals 
   1.906 -                       
   1.907 -fun merge (g1 as (cost1, _, actions1, _)) (g2 as (cost2, _, actions2, _)) =
   1.908 +          NONE => define' (update_axname axname orig_axname g) (name, ty) axname orig_axname body
   1.909 +        | SOME _ => g))
   1.910 +  | merge' (Finalize finals, g) = finalize' g finals
   1.911 +
   1.912 +fun merge'' (g1 as (cost1, _, actions1, _)) (g2 as (cost2, _, actions2, _)) =
   1.913      if cost1 < cost2 then
   1.914        foldr merge' g2 actions1
   1.915      else
   1.916        foldr merge' g1 actions2
   1.917 -                           
   1.918 -fun finals (_, _, history, graph) = 
   1.919 -    Symtab.foldl 
   1.920 -      (fn (finals, (name, Node(_, _, _, ftys, _))) => 
   1.921 -          Symtab.update_new ((name, ftys), finals)) 
   1.922 +
   1.923 +fun finals (_, _, history, graph) =
   1.924 +    Symtab.foldl
   1.925 +      (fn (finals, (name, Node(_, _, _, ftys, _))) =>
   1.926 +          Symtab.update_new ((name, ftys), finals))
   1.927        (Symtab.empty, graph)
   1.928  
   1.929 -fun overloading_info (_, axmap, _, graph) c = 
   1.930 +fun overloading_info (_, axmap, _, graph) c =
   1.931      let
   1.932        fun translate (ax, Defnode (ty, _)) = (the (Symtab.lookup (axmap, ax)), ty)
   1.933      in
   1.934 @@ -669,9 +639,9 @@
   1.935        | SOME (Node (ty, defnodes, _, _, state)) =>
   1.936          SOME (ty, map translate (Symtab.dest defnodes), state)
   1.937      end
   1.938 -      
   1.939 -fun fast_overloading_info (_, _, _, graph) c = 
   1.940 -    let 
   1.941 +
   1.942 +fun fast_overloading_info (_, _, _, graph) c =
   1.943 +    let
   1.944        fun count (c, _) = c+1
   1.945      in
   1.946        case Symtab.lookup (graph, c) of
   1.947 @@ -680,8 +650,61 @@
   1.948          SOME (ty, Symtab.foldl count (0, defnodes), state)
   1.949      end
   1.950  
   1.951 +
   1.952 +
   1.953 +(** diagnostics **)
   1.954 +
   1.955 +fun pretty_const pp (c, T) =
   1.956 + [Pretty.str c, Pretty.str " ::", Pretty.brk 1,
   1.957 +  Pretty.quote (Pretty.typ pp (Type.freeze_type T))];    (* FIXME zero indexes!? *)
   1.958 +
   1.959 +fun pretty_path pp path = fold_rev (fn (T, c, def) =>
   1.960 +  fn [] => [Pretty.block (pretty_const pp (c, T))]
   1.961 +   | prts => Pretty.block (pretty_const pp (c, T) @
   1.962 +      [Pretty.brk 1, Pretty.str ("depends via " ^ quote def ^ " on")]) :: prts) path [];
   1.963 +
   1.964 +fun chain_history_msg s =    (* FIXME huh!? *)
   1.965 +  if chain_history () then s ^ ": "
   1.966 +  else s ^ " (set DEFS_CHAIN_HISTORY=ON for full history): ";
   1.967 +
   1.968 +fun defs_circular pp path =
   1.969 +  Pretty.str (chain_history_msg "Cyclic dependency of definitions") :: pretty_path pp path
   1.970 +  |> Pretty.chunks |> Pretty.string_of;
   1.971 +
   1.972 +fun defs_infinite_chain pp path =
   1.973 +  Pretty.str (chain_history_msg "Infinite chain of definitions") :: pretty_path pp path
   1.974 +  |> Pretty.chunks |> Pretty.string_of;
   1.975 +
   1.976 +fun defs_clash def1 def2 = "Type clash in definitions " ^ quote def1 ^ " and " ^ quote def2;
   1.977 +
   1.978 +fun defs_final pp const =
   1.979 +  (Pretty.str "Attempt to define final constant" :: Pretty.brk 1 :: pretty_const pp const)
   1.980 +  |> Pretty.block |> Pretty.string_of;
   1.981 +
   1.982 +
   1.983 +(* external interfaces *)
   1.984 +
   1.985 +fun declare const defs =
   1.986 +  if_none (try (declare'' defs) const) defs;
   1.987 +
   1.988 +fun define pp const name rhs defs =
   1.989 +  define'' defs const name rhs
   1.990 +    handle DEFS msg => sys_error msg
   1.991 +      | CIRCULAR path => error (defs_circular pp path)
   1.992 +      | INFINITE_CHAIN path => error (defs_infinite_chain pp path)
   1.993 +      | CLASH (_, def1, def2) => error (defs_clash def1 def2)
   1.994 +      | FINAL const => error (defs_final pp const);
   1.995 +
   1.996 +fun finalize const defs =
   1.997 +  finalize'' defs const handle DEFS msg => sys_error msg;
   1.998 +
   1.999 +fun merge pp defs1 defs2 =
  1.1000 +  merge'' defs1 defs2
  1.1001 +    handle CIRCULAR namess => error (defs_circular pp namess)
  1.1002 +      | INFINITE_CHAIN namess => error (defs_infinite_chain pp namess);
  1.1003 +
  1.1004  end;
  1.1005 -		
  1.1006 +
  1.1007  (*
  1.1008  
  1.1009  fun tvar name = TVar ((name, 0), [])
  1.1010 @@ -697,7 +720,7 @@
  1.1011  val name = Type ("name", [])
  1.1012  
  1.1013  val _ = print "make empty"
  1.1014 -val g = Defs.empty 
  1.1015 +val g = Defs.empty
  1.1016  
  1.1017  val _ = print "declare perm"
  1.1018  val g = Defs.declare g ("perm", prm alpha --> beta --> beta)
  1.1019 @@ -706,7 +729,7 @@
  1.1020  val g = Defs.declare g ("permF", prm alpha --> lam --> lam)
  1.1021  
  1.1022  val _ = print "define perm (1)"
  1.1023 -val g = Defs.define g ("perm", prm alpha --> (beta --> gamma) --> (beta --> gamma)) "perm_fun" 
  1.1024 +val g = Defs.define g ("perm", prm alpha --> (beta --> gamma) --> (beta --> gamma)) "perm_fun"
  1.1025          [("perm", prm alpha --> gamma --> gamma), ("perm", prm alpha --> beta --> beta)]
  1.1026  
  1.1027  val _ = print "define permF (1)"
  1.1028 @@ -720,4 +743,4 @@
  1.1029  val g = Defs.define g ("perm", prm alpha --> lam --> lam) "perm_lam"
  1.1030          [("permF", (prm alpha --> lam --> lam))]
  1.1031  
  1.1032 -*)
  1.1033 \ No newline at end of file
  1.1034 +*)