src/Pure/defs.ML
 author wenzelm Thu Sep 01 22:15:10 2005 +0200 (2005-09-01) changeset 17223 430edc6b7826 parent 16982 4600e74aeb0d child 17412 e26cb20ef0cc permissions -rw-r--r--
curried_lookup/update;
tuned;
```     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 *)
```