src/Pure/defs.ML
 author obua Thu Jul 07 19:01:04 2005 +0200 (2005-07-07) changeset 16743 21dbff595bf6 parent 16384 90c51c932154 child 16766 ea667a5426fe permissions -rw-r--r--
1) all theorems in Orderings can now be given as a parameter
2) new function Theory.defs_of
```     1 (*  Title:      Pure/General/defs.ML
```
```     2     ID:         \$Id\$
```
```     3     Author:     Steven Obua, TU Muenchen
```
```     4
```
```     5     Checks if definitions preserve consistency of logic by enforcing
```
```     6     that there are no cyclic definitions. The algorithm is described in
```
```     7     "An Algorithm for Determining Definitional Cycles in Higher-Order Logic with Overloading",
```
```     8     Steven Obua, technical report, to be written :-)
```
```     9 *)
```
```    10
```
```    11 signature DEFS = sig
```
```    12
```
```    13   type graph
```
```    14
```
```    15   exception DEFS of string
```
```    16   exception CIRCULAR of (typ * string * string) list
```
```    17   exception INFINITE_CHAIN of (typ * string * string) list
```
```    18   exception FINAL of string * typ
```
```    19   exception CLASH of string * string * string
```
```    20
```
```    21   val empty : graph
```
```    22   val declare : graph -> string * typ -> graph  (* exception DEFS *)
```
```    23   val define : graph -> string * typ -> string -> (string * typ) list -> graph
```
```    24     (* exception DEFS, CIRCULAR, INFINITE_CHAIN, CLASH, FINAL *)
```
```    25
```
```    26   val finalize : graph -> string * typ -> graph (* exception DEFS *)
```
```    27
```
```    28   val finals : graph -> (typ list) Symtab.table
```
```    29
```
```    30   val merge : graph -> graph -> graph (* exception CIRCULAR, INFINITE_CHAIN, CLASH *)
```
```    31
```
```    32   (* If set to true then the exceptions CIRCULAR and INFINITE_CHAIN return the full
```
```    33      chain of definitions that lead to the exception. In the beginning, chain_history
```
```    34      is initialized with the Isabelle environment variable DEFS_CHAIN_HISTORY. *)
```
```    35   val set_chain_history : bool -> unit
```
```    36   val chain_history : unit -> bool
```
```    37
```
```    38   datatype overloadingstate = Open | Closed | Final
```
```    39   val overloading_info : graph -> string -> (typ * (string*typ) list * overloadingstate) option
```
```    40   val is_overloaded : graph -> string -> bool
```
```    41
```
```    42 end
```
```    43
```
```    44 structure Defs :> DEFS = struct
```
```    45
```
```    46 type tyenv = Type.tyenv
```
```    47 type edgelabel = (int * typ * typ * (typ * string * string) list)
```
```    48
```
```    49 datatype overloadingstate = Open | Closed | Final
```
```    50
```
```    51 datatype node = Node of
```
```    52          typ  (* most general type of constant *)
```
```    53          * defnode Symtab.table
```
```    54              (* a table of defnodes, each corresponding to 1 definition of the
```
```    55                 constant for a particular type, indexed by axiom name *)
```
```    56          * (unit Symtab.table) Symtab.table
```
```    57              (* a table of all back referencing defnodes to this node,
```
```    58                 indexed by node name of the defnodes *)
```
```    59          * typ list (* a list of all finalized types *)
```
```    60          * overloadingstate
```
```    61
```
```    62      and defnode = Defnode of
```
```    63          typ  (* type of the constant in this particular definition *)
```
```    64          * (edgelabel list) Symtab.table (* The edges, grouped by nodes. *)
```
```    65
```
```    66 fun getnode graph noderef = the (Symtab.lookup (graph, noderef))
```
```    67 fun get_nodedefs (Node (_, defs, _, _, _)) = defs
```
```    68 fun get_defnode (Node (_, defs, _, _, _)) defname = Symtab.lookup (defs, defname)
```
```    69 fun get_defnode' graph noderef defname =
```
```    70     Symtab.lookup (get_nodedefs (the (Symtab.lookup (graph, noderef))), defname)
```
```    71
```
```    72 fun table_size table = Symtab.foldl (fn (x, _) => x+1) (0, table)
```
```    73
```
```    74 datatype graphaction = Declare of string * typ
```
```    75 		     | Define of string * typ * string * (string * typ) list
```
```    76 		     | Finalize of string * typ
```
```    77
```
```    78 type graph = int * (string Symtab.table) * (graphaction list) * (node Symtab.table)
```
```    79
```
```    80 val CHAIN_HISTORY =
```
```    81     let
```
```    82       fun f c = if Char.isSpace c then "" else String.str (Char.toUpper c)
```
```    83       val env = String.translate f (getenv "DEFS_CHAIN_HISTORY")
```
```    84     in
```
```    85       ref (env = "ON" orelse env = "TRUE")
```
```    86     end
```
```    87
```
```    88 fun set_chain_history b = CHAIN_HISTORY := b
```
```    89 fun chain_history () = !CHAIN_HISTORY
```
```    90
```
```    91 val empty = (0, Symtab.empty, [], Symtab.empty)
```
```    92
```
```    93 exception DEFS of string;
```
```    94 exception CIRCULAR of (typ * string * string) list;
```
```    95 exception INFINITE_CHAIN of (typ * string * string) list;
```
```    96 exception CLASH of string * string * string;
```
```    97 exception FINAL of string * typ;
```
```    98
```
```    99 fun def_err s = raise (DEFS s)
```
```   100
```
```   101 fun no_forwards defs =
```
```   102     Symtab.foldl
```
```   103     (fn (closed, (_, Defnode (_, edges))) =>
```
```   104         if not closed then false else Symtab.is_empty edges)
```
```   105     (true, defs)
```
```   106
```
```   107 exception No_Change;
```
```   108
```
```   109 fun map_nc f list =
```
```   110     let
```
```   111       val changed = ref false
```
```   112       fun f' x =
```
```   113           let
```
```   114             val x' = f x
```
```   115             val _ = changed := true
```
```   116           in
```
```   117             x'
```
```   118           end handle No_Change => x
```
```   119       val list' = map f' list
```
```   120     in
```
```   121       if !changed then list' else raise No_Change
```
```   122     end
```
```   123
```
```   124 fun checkT' (t as (Type (a, Ts))) = (Type (a, map_nc checkT' Ts) handle No_Change => t)
```
```   125   | checkT' (t as (TVar ((a, 0), []))) = raise No_Change
```
```   126   | checkT' (t as (TVar ((a, 0), _))) = TVar ((a, 0), [])
```
```   127   | checkT' (t as (TFree (a, _))) = TVar ((a, 0), [])
```
```   128   | checkT' _ = def_err "type is not clean"
```
```   129
```
```   130 fun checkT t = Term.compress_type (checkT' t handle No_Change => t)
```
```   131
```
```   132 fun rename ty1 ty2 = incr_tvar ((maxidx_of_typ ty1)+1) ty2;
```
```   133
```
```   134 fun subst_incr_tvar inc t =
```
```   135     if (inc > 0) then
```
```   136       let
```
```   137 	val tv = typ_tvars t
```
```   138 	val t' = incr_tvar inc t
```
```   139 	fun update_subst (((n,i), _), s) =
```
```   140 	    Vartab.update (((n, i), ([], TVar ((n, i+inc), []))), s)
```
```   141       in
```
```   142 	(t',List.foldl update_subst Vartab.empty tv)
```
```   143       end
```
```   144     else
```
```   145       (t, Vartab.empty)
```
```   146
```
```   147 fun subst s ty = Envir.norm_type s ty
```
```   148
```
```   149 fun subst_history s history = map (fn (ty, cn, dn) => (subst s ty, cn, dn)) history
```
```   150
```
```   151 fun is_instance instance_ty general_ty =
```
```   152     Type.typ_instance Type.empty_tsig (instance_ty, general_ty)
```
```   153
```
```   154 fun is_instance_r instance_ty general_ty =
```
```   155     is_instance instance_ty (rename instance_ty general_ty)
```
```   156
```
```   157 fun unify ty1 ty2 =
```
```   158     SOME (fst (Type.unify Type.empty_tsig (Vartab.empty, 0) (ty1, ty2)))
```
```   159     handle Type.TUNIFY => NONE
```
```   160
```
```   161 (*
```
```   162    Unifies ty1 and ty2, renaming ty1 and ty2 so that they have greater indices than max and
```
```   163    so that they are different. All indices in ty1 and ty2 are supposed to be less than or
```
```   164    equal to max.
```
```   165    Returns SOME (max', s1, s2), so that s1(ty1) = s2(ty2) and max' is greater or equal than
```
```   166    all indices in s1, s2, ty1, ty2.
```
```   167 *)
```
```   168 fun unify_r max ty1 ty2 =
```
```   169     let
```
```   170       val max = Int.max(max, 0)
```
```   171       val max1 = max (* >= maxidx_of_typ ty1 *)
```
```   172       val max2 = max (* >= maxidx_of_typ ty2 *)
```
```   173       val max = Int.max(max, Int.max (max1, max2))
```
```   174       val (ty1, s1) = subst_incr_tvar (max + 1) ty1
```
```   175       val (ty2, s2) = subst_incr_tvar (max + max1 + 2) ty2
```
```   176       val max = max + max1 + max2 + 2
```
```   177       fun merge a b = Vartab.merge (fn _ => false) (a, b)
```
```   178     in
```
```   179       case unify ty1 ty2 of
```
```   180 	NONE => NONE
```
```   181       | SOME s => SOME (max, merge s1 s, merge s2 s)
```
```   182     end
```
```   183
```
```   184 fun can_be_unified_r ty1 ty2 =
```
```   185     let
```
```   186       val ty2 = rename ty1 ty2
```
```   187     in
```
```   188       case unify ty1 ty2 of
```
```   189 	NONE => false
```
```   190       | _ => true
```
```   191     end
```
```   192
```
```   193 fun can_be_unified ty1 ty2 =
```
```   194     case unify ty1 ty2 of
```
```   195       NONE => false
```
```   196     | _ => true
```
```   197
```
```   198 structure Inttab = TableFun(type key = int val ord = int_ord);
```
```   199
```
```   200 fun normalize_edge_idx (edge as (maxidx, u1, v1, history)) =
```
```   201     if maxidx <= 1000000 then edge else
```
```   202     let
```
```   203
```
```   204       fun idxlist idx extract_ty inject_ty (tab, max) ts =
```
```   205           foldr
```
```   206             (fn (e, ((tab, max), ts)) =>
```
```   207                 let
```
```   208                   val ((tab, max), ty) = idx (tab, max) (extract_ty e)
```
```   209                   val e = inject_ty (ty, e)
```
```   210                 in
```
```   211                   ((tab, max), e::ts)
```
```   212                 end)
```
```   213             ((tab,max), []) ts
```
```   214
```
```   215       fun idx (tab,max) (TVar ((a,i),_)) =
```
```   216           (case Inttab.lookup (tab, i) of
```
```   217              SOME j => ((tab, max), TVar ((a,j),[]))
```
```   218            | NONE => ((Inttab.update ((i, max), tab), max+1), TVar ((a,max),[])))
```
```   219         | idx (tab,max) (Type (t, ts)) =
```
```   220           let
```
```   221             val ((tab, max), ts) = idxlist idx I fst (tab, max) ts
```
```   222           in
```
```   223             ((tab,max), Type (t, ts))
```
```   224           end
```
```   225         | idx (tab, max) ty = ((tab, max), ty)
```
```   226
```
```   227       val ((tab,max), u1) = idx (Inttab.empty, 0) u1
```
```   228       val ((tab,max), v1) = idx (tab, max) v1
```
```   229       val ((tab,max), history) =
```
```   230           idxlist idx
```
```   231             (fn (ty,_,_) => ty)
```
```   232             (fn (ty, (_, s1, s2)) => (ty, s1, s2))
```
```   233             (tab, max) history
```
```   234     in
```
```   235       (max, u1, v1, history)
```
```   236     end
```
```   237
```
```   238 fun compare_edges (e1 as (maxidx1, u1, v1, history1)) (e2 as (maxidx2, u2, v2, history2)) =
```
```   239     let
```
```   240       val t1 = u1 --> v1
```
```   241       val t2 = incr_tvar (maxidx1+1) (u2 --> v2)
```
```   242     in
```
```   243       if (is_instance t1 t2) then
```
```   244 	(if is_instance t2 t1 then
```
```   245 	   SOME (int_ord (length history2, length history1))
```
```   246 	 else
```
```   247 	   SOME LESS)
```
```   248       else if (is_instance t2 t1) then
```
```   249 	SOME GREATER
```
```   250       else
```
```   251 	NONE
```
```   252     end
```
```   253
```
```   254 fun merge_edges_1 (x, []) = [x]
```
```   255   | merge_edges_1 (x, (y::ys)) =
```
```   256     (case compare_edges x y of
```
```   257        SOME LESS => (y::ys)
```
```   258      | SOME EQUAL => (y::ys)
```
```   259      | SOME GREATER => merge_edges_1 (x, ys)
```
```   260      | NONE => y::(merge_edges_1 (x, ys)))
```
```   261
```
```   262 fun merge_edges xs ys = foldl merge_edges_1 xs ys
```
```   263
```
```   264 fun declare' (g as (cost, axmap, actions, graph)) (cty as (name, ty)) =
```
```   265     (cost, axmap, (Declare cty)::actions,
```
```   266      Symtab.update_new ((name, Node (ty, Symtab.empty, Symtab.empty, [], Open)), graph))
```
```   267     handle Symtab.DUP _ =>
```
```   268            let
```
```   269              val (Node (gty, _, _, _, _)) = the (Symtab.lookup(graph, name))
```
```   270            in
```
```   271              if is_instance_r ty gty andalso is_instance_r gty ty then
```
```   272                g
```
```   273              else
```
```   274                def_err "constant is already declared with different type"
```
```   275            end
```
```   276
```
```   277 fun declare g (name, ty) = declare' g (name, checkT ty)
```
```   278
```
```   279 val axcounter = ref (IntInf.fromInt 0)
```
```   280 fun newaxname axmap axname =
```
```   281     let
```
```   282       val c = !axcounter
```
```   283       val _ = axcounter := c+1
```
```   284       val axname' = axname^"_"^(IntInf.toString c)
```
```   285     in
```
```   286       (Symtab.update ((axname', axname), axmap), axname')
```
```   287     end
```
```   288
```
```   289 fun translate_ex axmap x =
```
```   290     let
```
```   291       fun translate (ty, nodename, axname) =
```
```   292           (ty, nodename, the (Symtab.lookup (axmap, axname)))
```
```   293     in
```
```   294       case x of
```
```   295         INFINITE_CHAIN chain => raise (INFINITE_CHAIN (map translate chain))
```
```   296       | CIRCULAR cycle => raise (CIRCULAR (map translate cycle))
```
```   297       | _ => raise x
```
```   298     end
```
```   299
```
```   300 fun define' (cost, axmap, actions, graph) (mainref, ty) axname body =
```
```   301     let
```
```   302       val mainnode  = (case Symtab.lookup (graph, mainref) of
```
```   303 			 NONE => def_err ("constant "^mainref^" is not declared")
```
```   304 		       | SOME n => n)
```
```   305       val (Node (gty, defs, backs, finals, _)) = mainnode
```
```   306       val _ = (if is_instance_r ty gty then ()
```
```   307                else def_err "type of constant does not match declared type")
```
```   308       fun check_def (s, Defnode (ty', _)) =
```
```   309           (if can_be_unified_r ty ty' then
```
```   310 	     raise (CLASH (mainref, axname, s))
```
```   311 	   else if s = axname then
```
```   312 	     def_err "name of axiom is already used for another definition of this constant"
```
```   313 	   else false)
```
```   314       val _ = Symtab.exists check_def defs
```
```   315       fun check_final finalty =
```
```   316 	  (if can_be_unified_r finalty ty then
```
```   317 	     raise (FINAL (mainref, finalty))
```
```   318 	   else
```
```   319 	     true)
```
```   320       val _ = forall check_final finals
```
```   321
```
```   322       (* now we know that the only thing that can prevent acceptance of the definition
```
```   323          is a cyclic dependency *)
```
```   324
```
```   325       fun insert_edges edges (nodename, links) =
```
```   326           (if links = [] then
```
```   327              edges
```
```   328            else
```
```   329              let
```
```   330                val links = map normalize_edge_idx links
```
```   331              in
```
```   332                Symtab.update ((nodename,
```
```   333 	                       case Symtab.lookup (edges, nodename) of
```
```   334 	                         NONE => links
```
```   335 	                       | SOME links' => merge_edges links' links),
```
```   336                               edges)
```
```   337              end)
```
```   338
```
```   339       fun make_edges ((bodyn, bodyty), edges) =
```
```   340 	  let
```
```   341 	    val bnode =
```
```   342 		(case Symtab.lookup (graph, bodyn) of
```
```   343 		   NONE => def_err "body of constant definition references undeclared constant"
```
```   344 		 | SOME x => x)
```
```   345 	    val (Node (general_btyp, bdefs, bbacks, bfinals, closed)) = bnode
```
```   346 	  in
```
```   347             if closed = Final then edges else
```
```   348 	    case unify_r 0 bodyty general_btyp of
```
```   349 	      NONE => edges
```
```   350 	    | SOME (maxidx, sigma1, sigma2) =>
```
```   351               if exists (is_instance_r bodyty) bfinals then
```
```   352                 edges
```
```   353               else
```
```   354 	        let
```
```   355 		  fun insert_trans_edges ((step1, edges), (nodename, links)) =
```
```   356                       let
```
```   357                         val (maxidx1, alpha1, beta1, defname) = step1
```
```   358                         fun connect (maxidx2, alpha2, beta2, history) =
```
```   359 		            case unify_r (Int.max (maxidx1, maxidx2)) beta1 alpha2 of
```
```   360 		              NONE => NONE
```
```   361 		            | SOME (max, sleft, sright) =>
```
```   362 			      SOME (max, subst sleft alpha1, subst sright beta2,
```
```   363                                     if !CHAIN_HISTORY then
```
```   364 			              ((subst sleft beta1, bodyn, defname)::
```
```   365 				       (subst_history sright history))
```
```   366                                     else [])
```
```   367                         val links' = List.mapPartial connect links
```
```   368                       in
```
```   369                         (step1, insert_edges edges (nodename, links'))
```
```   370                       end
```
```   371
```
```   372                   fun make_edges' ((swallowed, edges),
```
```   373                                    (def_name, Defnode (def_ty, def_edges))) =
```
```   374 		      if swallowed then
```
```   375 		        (swallowed, edges)
```
```   376 		      else
```
```   377 		        (case unify_r 0 bodyty def_ty of
```
```   378 			   NONE => (swallowed, edges)
```
```   379 		         | SOME (maxidx, sigma1, sigma2) =>
```
```   380 			   (is_instance_r bodyty def_ty,
```
```   381                             snd (Symtab.foldl insert_trans_edges
```
```   382                               (((maxidx, subst sigma1 ty, subst sigma2 def_ty, def_name),
```
```   383                                 edges), def_edges))))
```
```   384           	  val (swallowed, edges) = Symtab.foldl make_edges' ((false, edges), bdefs)
```
```   385 	        in
```
```   386 		  if swallowed then
```
```   387 		    edges
```
```   388 		  else
```
```   389                     insert_edges edges
```
```   390                     (bodyn, [(maxidx, subst sigma1 ty, subst sigma2 general_btyp,[])])
```
```   391 	        end
```
```   392 	  end
```
```   393
```
```   394       val edges = foldl make_edges Symtab.empty body
```
```   395
```
```   396       (* We also have to add the backreferences that this new defnode induces. *)
```
```   397       fun install_backrefs (graph, (noderef, links)) =
```
```   398           if links <> [] then
```
```   399             let
```
```   400               val (Node (ty, defs, backs, finals, closed)) = getnode graph noderef
```
```   401               val _ = if closed = Final then
```
```   402                         sys_error ("install_backrefs: closed node cannot be updated")
```
```   403                       else ()
```
```   404               val defnames =
```
```   405                   (case Symtab.lookup (backs, mainref) of
```
```   406                      NONE => Symtab.empty
```
```   407                    | SOME s => s)
```
```   408               val defnames' = Symtab.update_new ((axname, ()), defnames)
```
```   409               val backs' = Symtab.update ((mainref,defnames'), backs)
```
```   410             in
```
```   411               Symtab.update ((noderef, Node (ty, defs, backs', finals, closed)), graph)
```
```   412             end
```
```   413           else
```
```   414             graph
```
```   415
```
```   416       val graph = Symtab.foldl install_backrefs (graph, edges)
```
```   417
```
```   418       val (Node (_, _, backs, _, closed)) = getnode graph mainref
```
```   419       val closed =
```
```   420           if closed = Final then sys_error "define: closed node"
```
```   421           else if closed = Open andalso is_instance_r gty ty then Closed else closed
```
```   422
```
```   423       val thisDefnode = Defnode (ty, edges)
```
```   424       val graph = Symtab.update ((mainref, Node (gty, Symtab.update_new
```
```   425         ((axname, thisDefnode), defs), backs, finals, closed)), graph)
```
```   426
```
```   427       (* Now we have to check all backreferences to this node and inform them about
```
```   428          the new defnode. In this section we also check for circularity. *)
```
```   429       fun update_backrefs ((backs, graph), (noderef, defnames)) =
```
```   430 	  let
```
```   431 	    fun update_defs ((defnames, graph),(defname, _)) =
```
```   432 		let
```
```   433                   val (Node (nodety, nodedefs, nodebacks, nodefinals, closed)) =
```
```   434                       getnode graph noderef
```
```   435                   val _ = if closed = Final then sys_error "update_defs: closed node" else ()
```
```   436 		  val (Defnode (def_ty, defnode_edges)) =
```
```   437                       the (Symtab.lookup (nodedefs, defname))
```
```   438 		  val edges = the (Symtab.lookup (defnode_edges, mainref))
```
```   439                   val refclosed = ref false
```
```   440
```
```   441 	          (* the type of thisDefnode is ty *)
```
```   442 		  fun update (e as (max, alpha, beta, history), (changed, edges)) =
```
```   443 		      case unify_r max beta ty of
```
```   444 			NONE => (changed, e::edges)
```
```   445 		      | SOME (max', s_beta, s_ty) =>
```
```   446 			let
```
```   447 			  val alpha' = subst s_beta alpha
```
```   448 			  val ty' = subst s_ty ty
```
```   449 			  val _ =
```
```   450 			      if noderef = mainref andalso defname = axname then
```
```   451 				(case unify alpha' ty' of
```
```   452 				   NONE =>
```
```   453 				   if (is_instance_r ty' alpha') then
```
```   454 				     raise (INFINITE_CHAIN (
```
```   455 					    (alpha', mainref, axname)::
```
```   456 					    (subst_history s_beta history)@
```
```   457 					    [(ty', mainref, axname)]))
```
```   458 				   else ()
```
```   459 				 | SOME s =>
```
```   460                                    raise (CIRCULAR (
```
```   461 					  (subst s alpha', mainref, axname)::
```
```   462 					  (subst_history s (subst_history s_beta history))@
```
```   463 					  [(subst s ty', mainref, axname)])))
```
```   464 			      else ()
```
```   465 			in
```
```   466 			  if is_instance_r beta ty then
```
```   467 			    (true, edges)
```
```   468 			  else
```
```   469 			    (changed, e::edges)
```
```   470 			end
```
```   471
```
```   472                   val (changed, edges') = foldl update (false, []) edges
```
```   473                   val defnames' = if edges' = [] then
```
```   474                                     defnames
```
```   475                                   else
```
```   476                                     Symtab.update ((defname, ()), defnames)
```
```   477                 in
```
```   478                   if changed then
```
```   479                     let
```
```   480                       val defnode_edges' =
```
```   481                           if edges' = [] then
```
```   482                             Symtab.delete mainref defnode_edges
```
```   483                           else
```
```   484                             Symtab.update ((mainref, edges'), defnode_edges)
```
```   485                       val defnode' = Defnode (def_ty, defnode_edges')
```
```   486                       val nodedefs' = Symtab.update ((defname, defnode'), nodedefs)
```
```   487                       val closed = if closed = Closed andalso Symtab.is_empty defnode_edges'
```
```   488                                       andalso no_forwards nodedefs'
```
```   489                                    then Final else closed
```
```   490                       val graph' =
```
```   491                           Symtab.update
```
```   492                             ((noderef,
```
```   493                               Node (nodety, nodedefs', nodebacks, nodefinals, closed)),graph)
```
```   494                     in
```
```   495                       (defnames', graph')
```
```   496                     end
```
```   497                   else
```
```   498                     (defnames', graph)
```
```   499                 end
```
```   500
```
```   501 	    val (defnames', graph') = Symtab.foldl update_defs
```
```   502                                                    ((Symtab.empty, graph), defnames)
```
```   503 	  in
```
```   504 	    if Symtab.is_empty defnames' then
```
```   505 	      (backs, graph')
```
```   506 	    else
```
```   507 	      let
```
```   508 		val backs' = Symtab.update_new ((noderef, defnames'), backs)
```
```   509 	      in
```
```   510 		(backs', graph')
```
```   511 	      end
```
```   512 	  end
```
```   513
```
```   514       val (backs, graph) = Symtab.foldl update_backrefs ((Symtab.empty, graph), backs)
```
```   515
```
```   516       (* If a Circular exception is thrown then we never reach this point. *)
```
```   517       val (Node (gty, defs, _, finals, closed)) = getnode graph mainref
```
```   518       val closed = if closed = Closed andalso no_forwards defs then Final else closed
```
```   519       val graph = Symtab.update ((mainref, Node (gty, defs, backs, finals, closed)), graph)
```
```   520       val actions' = (Define (mainref, ty, axname, body))::actions
```
```   521     in
```
```   522       (cost+3, axmap, actions', graph)
```
```   523     end handle ex => translate_ex axmap ex
```
```   524
```
```   525 fun define (g as (cost, axmap, actions, graph)) (mainref, ty) axname body =
```
```   526     let
```
```   527       val ty = checkT ty
```
```   528       fun checkbody (n, t) =
```
```   529           let
```
```   530             val (Node (_, _, _,_, closed)) = getnode graph n
```
```   531           in
```
```   532             case closed of
```
```   533               Final => NONE
```
```   534             | _ => SOME (n, checkT t)
```
```   535           end
```
```   536       val body = distinct (List.mapPartial checkbody body)
```
```   537       val (axmap, axname) = newaxname axmap axname
```
```   538     in
```
```   539       define' (cost, axmap, actions, graph) (mainref, ty) axname body
```
```   540     end
```
```   541
```
```   542 fun finalize' (cost, axmap, history, graph) (noderef, ty) =
```
```   543     case Symtab.lookup (graph, noderef) of
```
```   544       NONE => def_err ("cannot finalize constant "^noderef^"; it is not declared")
```
```   545     | SOME (Node (nodety, defs, backs, finals, closed)) =>
```
```   546       let
```
```   547 	val _ =
```
```   548             if (not (is_instance_r ty nodety)) then
```
```   549 	      def_err ("only type instances of the declared constant "^
```
```   550                        noderef^" can be finalized")
```
```   551 	    else ()
```
```   552 	val _ = Symtab.exists
```
```   553                   (fn (def_name, Defnode (def_ty, _)) =>
```
```   554 		      if can_be_unified_r ty def_ty then
```
```   555 			def_err ("cannot finalize constant "^noderef^
```
```   556                                  "; clash with definition "^def_name)
```
```   557 		      else
```
```   558 			false)
```
```   559 		  defs
```
```   560
```
```   561         fun update_finals [] = SOME [ty]
```
```   562           | update_finals (final_ty::finals) =
```
```   563             (if is_instance_r ty final_ty then NONE
```
```   564              else
```
```   565                case update_finals finals of
```
```   566                  NONE => NONE
```
```   567                | (r as SOME finals) =>
```
```   568                  if (is_instance_r final_ty ty) then
```
```   569                    r
```
```   570                  else
```
```   571                    SOME (final_ty :: finals))
```
```   572       in
```
```   573         case update_finals finals of
```
```   574           NONE => (cost, axmap, history, graph)
```
```   575         | SOME finals =>
```
```   576 	  let
```
```   577             val closed = if closed = Open andalso is_instance_r nodety ty then
```
```   578                            Closed else
```
```   579                          closed
```
```   580 	    val graph = Symtab.update ((noderef, Node(nodety, defs, backs, finals, closed)),
```
```   581                                        graph)
```
```   582
```
```   583 	    fun update_backref ((graph, backs), (backrefname, backdefnames)) =
```
```   584 		let
```
```   585 		  fun update_backdef ((graph, defnames), (backdefname, _)) =
```
```   586 	              let
```
```   587 			val (backnode as Node (backty, backdefs, backbacks,
```
```   588                                                backfinals, backclosed)) =
```
```   589                             getnode graph backrefname
```
```   590 			val (Defnode (def_ty, all_edges)) =
```
```   591                             the (get_defnode backnode backdefname)
```
```   592
```
```   593 			val (defnames', all_edges') =
```
```   594 			    case Symtab.lookup (all_edges, noderef) of
```
```   595 			      NONE => sys_error "finalize: corrupt backref"
```
```   596 			    | SOME edges =>
```
```   597 			      let
```
```   598 				val edges' = List.filter (fn (_, _, beta, _) =>
```
```   599                                                              not (is_instance_r beta ty)) edges
```
```   600 			      in
```
```   601 				if edges' = [] then
```
```   602 				  (defnames, Symtab.delete noderef all_edges)
```
```   603 				else
```
```   604 				  (Symtab.update ((backdefname, ()), defnames),
```
```   605 				   Symtab.update ((noderef, edges'), all_edges))
```
```   606 			      end
```
```   607 			val defnode' = Defnode (def_ty, all_edges')
```
```   608                         val backdefs' = Symtab.update ((backdefname, defnode'), backdefs)
```
```   609                         val backclosed' = if backclosed = Closed andalso
```
```   610                                              Symtab.is_empty all_edges'
```
```   611                                              andalso no_forwards backdefs'
```
```   612                                           then Final else backclosed
```
```   613 			val backnode' =
```
```   614                             Node (backty, backdefs', backbacks, backfinals, backclosed')
```
```   615 		      in
```
```   616 			(Symtab.update ((backrefname, backnode'), graph), defnames')
```
```   617 		      end
```
```   618
```
```   619 		  val (graph', defnames') =
```
```   620                       Symtab.foldl update_backdef ((graph, Symtab.empty), backdefnames)
```
```   621 		in
```
```   622 		  (graph', if Symtab.is_empty defnames' then backs
```
```   623 			   else Symtab.update ((backrefname, defnames'), backs))
```
```   624 		end
```
```   625 	    val (graph', backs') = Symtab.foldl update_backref ((graph, Symtab.empty), backs)
```
```   626 	    val Node ( _, defs, _, _, closed) = getnode graph' noderef
```
```   627             val closed = if closed = Closed andalso no_forwards defs then Final else closed
```
```   628 	    val graph' = Symtab.update ((noderef, Node (nodety, defs, backs',
```
```   629                                                         finals, closed)), graph')
```
```   630             val history' = (Finalize (noderef, ty)) :: history
```
```   631 	  in
```
```   632 	    (cost+1, axmap, history', graph')
```
```   633 	  end
```
```   634       end
```
```   635
```
```   636 fun finalize g (noderef, ty) = finalize' g (noderef, checkT ty)
```
```   637
```
```   638 fun merge' (Declare cty, g) = declare' g cty
```
```   639   | merge' (Define (name, ty, axname, body), g as (_,_, _, graph)) =
```
```   640     (case Symtab.lookup (graph, name) of
```
```   641        NONE => define' g (name, ty) axname body
```
```   642      | SOME (Node (_, defs, _, _, _)) =>
```
```   643        (case Symtab.lookup (defs, axname) of
```
```   644 	  NONE => define' g (name, ty) axname body
```
```   645 	| SOME _ => g))
```
```   646   | merge' (Finalize finals, g) = finalize' g finals
```
```   647
```
```   648 fun merge (g1 as (cost1, _, actions1, _)) (g2 as (cost2, _, actions2, _)) =
```
```   649     if cost1 < cost2 then
```
```   650       foldr merge' g2 actions1
```
```   651     else
```
```   652       foldr merge' g1 actions2
```
```   653
```
```   654 fun finals (_, _, history, graph) =
```
```   655     Symtab.foldl
```
```   656       (fn (finals, (name, Node(_, _, _, ftys, _))) =>
```
```   657           Symtab.update_new ((name, ftys), finals))
```
```   658       (Symtab.empty, graph)
```
```   659
```
```   660 fun overloading_info (_, axmap, _, graph) c =
```
```   661     let
```
```   662       fun translate (ax, Defnode (ty, _)) = (the (Symtab.lookup (axmap, ax)), ty)
```
```   663     in
```
```   664       case Symtab.lookup (graph, c) of
```
```   665         NONE => NONE
```
```   666       | SOME (Node (ty, defnodes, _, _, state)) =>
```
```   667         SOME (ty, map translate (Symtab.dest defnodes), state)
```
```   668     end
```
```   669
```
```   670 fun is_overloaded g c =
```
```   671     case overloading_info g c of
```
```   672       NONE => false
```
```   673     | SOME (_, l, _) => length l >= 2
```
```   674
```
```   675 end;
```
```   676
```
```   677 (*
```
```   678
```
```   679 fun tvar name = TVar ((name, 0), [])
```
```   680
```
```   681 val bool = Type ("bool", [])
```
```   682 val int = Type ("int", [])
```
```   683 val lam = Type("lam", [])
```
```   684 val alpha = tvar "'a"
```
```   685 val beta = tvar "'b"
```
```   686 val gamma = tvar "'c"
```
```   687 fun pair a b = Type ("pair", [a,b])
```
```   688 fun prm a = Type ("prm", [a])
```
```   689 val name = Type ("name", [])
```
```   690
```
```   691 val _ = print "make empty"
```
```   692 val g = Defs.empty
```
```   693
```
```   694 val _ = print "declare perm"
```
```   695 val g = Defs.declare g ("perm", prm alpha --> beta --> beta)
```
```   696
```
```   697 val _ = print "declare permF"
```
```   698 val g = Defs.declare g ("permF", prm alpha --> lam --> lam)
```
```   699
```
```   700 val _ = print "define perm (1)"
```
```   701 val g = Defs.define g ("perm", prm alpha --> (beta --> gamma) --> (beta --> gamma)) "perm_fun"
```
```   702         [("perm", prm alpha --> gamma --> gamma), ("perm", prm alpha --> beta --> beta)]
```
```   703
```
```   704 val _ = print "define permF (1)"
```
```   705 val g = Defs.define g ("permF", prm alpha --> lam --> lam) "permF_app"
```
```   706         ([("perm", prm alpha --> lam --> lam),
```
```   707          ("perm", prm alpha --> lam --> lam),
```
```   708          ("perm", prm alpha --> lam --> lam),
```
```   709          ("perm", prm alpha --> name --> name)])
```
```   710
```
```   711 val _ = print "define perm (2)"
```
```   712 val g = Defs.define g ("perm", prm alpha --> lam --> lam) "perm_lam"
```
```   713         [("permF", (prm alpha --> lam --> lam))]
```
```   714
```
`   715 *)`