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
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 *)
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
27 structure Defs :> DEFS = struct
29 type tyenv = Type.tyenv
30 type edgelabel = (int * typ * typ * (typ * string * string) list)
32 datatype overloadingstate = Open | Closed | Final
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 *)
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. *)
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)))
55 fun table_size table = Symtab.fold (K (fn x => x + 1)) table 0;
57 datatype graphaction =
58     Declare of string * typ
59   | Define of string * typ * string * string * (string * typ) list
60   | Finalize of string * typ
62 type graph = int * string Symtab.table * graphaction list * node Symtab.table
64 val chain_history = ref true
66 val empty = (0, Symtab.empty, [], Symtab.empty)
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;
74 fun def_err s = raise (DEFS s)
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)
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], []);
87 fun checkT thy = Compress.typ thy o checkT';
89 fun rename ty1 ty2 = Logic.incr_tvar ((maxidx_of_typ ty1)+1) ty2;
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)
104 fun subst s ty = Envir.norm_type s ty
106 fun subst_history s history = map (fn (ty, cn, dn) => (subst s ty, cn, dn)) history
108 fun is_instance instance_ty general_ty =
109     Type.raw_instance (instance_ty, general_ty)
111 fun is_instance_r instance_ty general_ty =
112     is_instance instance_ty (rename instance_ty general_ty)
114 fun unify ty1 ty2 =
115     SOME (Type.raw_unify (ty1, ty2) Vartab.empty)
116     handle Type.TUNIFY => NONE
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
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)
144 fun normalize_edge_idx (edge as (maxidx, u1, v1, history)) =
145     if maxidx <= 1000000 then edge else
146     let
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
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)
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
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
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)))
206 fun merge_edges xs ys = foldl merge_edges_1 xs ys
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
221 fun declare'' thy g (name, ty) = declare' g (name, checkT thy ty)
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
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
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
266       (* now we know that the only thing that can prevent acceptance of the definition
267          is a cyclic dependency *)
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
280              end)
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
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
337       val edges = foldl make_edges Symtab.empty body
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
359       val graph = Symtab.foldl install_backrefs (graph, edges)
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
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
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
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
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
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
456       val (backs, graph) = Symtab.foldl update_backrefs ((Symtab.empty, graph), backs)
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
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
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
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
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)
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
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
577 fun finalize'' thy g (noderef, ty) = finalize' g (noderef, checkT thy ty)
579 fun update_axname ax orig_ax (cost, axmap, history, graph) =
580   (cost, Symtab.curried_update (ax, orig_ax) axmap, history, graph)
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
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
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)
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
615 (* monomorphic consts -- neither parametric nor ad-hoc polymorphism *)
617 fun monomorphicT (Type (_, Ts)) = forall monomorphicT Ts
618   | monomorphicT _ = false
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);
629 (** diagnostics **)
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)))];
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 [];
640 fun defs_circular pp path =
641   Pretty.str "Cyclic dependency of definitions: " :: pretty_path pp path
642   |> Pretty.chunks |> Pretty.string_of;
644 fun defs_infinite_chain pp path =
645   Pretty.str "Infinite chain of definitions: " :: pretty_path pp path
646   |> Pretty.chunks |> Pretty.string_of;
648 fun defs_clash def1 def2 = "Type clash in definitions " ^ quote def1 ^ " and " ^ quote def2;
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;
655 (* external interfaces *)
657 fun declare thy const defs =
658   if_none (try (declare'' thy defs) const) defs;
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);
668 fun finalize thy const defs =
669   finalize'' thy defs const handle DEFS msg => sys_error msg;
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);
676 end;
678 (*
680 fun tvar name = TVar ((name, 0), [])
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", [])
692 val _ = print "make empty"
693 val g = Defs.empty
695 val _ = print "declare perm"
696 val g = Defs.declare g ("perm", prm alpha --> beta --> beta)
698 val _ = print "declare permF"
699 val g = Defs.declare g ("permF", prm alpha --> lam --> lam)
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)]
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)])
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))]
716 *)