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