src/Pure/defs.ML
author obua
Fri, 03 Jun 2005 01:08:07 +0200
changeset 16198 cfd070a2cc4d
parent 16177 1af9f5c69745
child 16308 636a1a84977a
permissions -rw-r--r--
Integrates cycle detection in definitions with finalconsts
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
16108
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
     1
(*  Title:      Pure/General/defs.ML
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
     2
    ID:         $Id$
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
     3
    Author:     Steven Obua, TU Muenchen
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
     4
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
     5
    Checks if definitions preserve consistency of logic by enforcing that there are no cyclic definitions.
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
     6
    The algorithm is described in 
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
     7
    "Cycle-free Overloading in Isabelle", Steven Obua, technical report, to be written :-)
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
     8
*)
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
     9
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
    10
signature DEFS = sig
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
    11
    
16198
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
    12
  type graph
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
    13
       
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
    14
  exception DEFS of string
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
    15
  exception CIRCULAR of (typ * string * string) list
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
    16
  exception INFINITE_CHAIN of (typ * string * string) list 
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
    17
  exception FINAL of string * typ
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
    18
  exception CLASH of string * string * string
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
    19
                     
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
    20
  val empty : graph
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
    21
  val declare : graph -> string * typ -> graph  (* exception DEFS *)
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
    22
  val define : graph -> string * typ -> string -> (string * typ) list -> graph 
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
    23
    (* exception DEFS, CIRCULAR, INFINITE_CHAIN, CLASH, FINAL *)
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
    24
                                                                         
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
    25
  val finalize : graph -> string * typ -> graph (* exception DEFS *)
16108
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
    26
16198
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
    27
  val finals : graph -> (typ list) Symtab.table
16158
2c3565b74b7a Removed final_consts from theory data. Now const_deps deals with final
obua
parents: 16113
diff changeset
    28
16198
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
    29
  (* the first argument should be the smaller graph *)
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
    30
  val merge : graph -> graph -> graph (* exception CIRCULAR, INFINITE_CHAIN, CLASH *)
16108
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
    31
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
    32
end
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
    33
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
    34
structure Defs :> DEFS = struct
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
    35
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
    36
type tyenv = Type.tyenv
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
    37
type edgelabel = (int * typ * typ * (typ * string * string) list)
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
    38
type noderef = string
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
    39
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
    40
datatype node = Node of
16198
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
    41
         string  (* name of constant *)
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
    42
         * typ  (* most general type of constant *)
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
    43
         * defnode Symtab.table  (* a table of defnodes, each corresponding to 1 definition of the 
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
    44
             constant for a particular type, indexed by axiom name *)
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
    45
         * backref Symtab.table (* a table of all back references to this node, indexed by node name *)
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
    46
         * typ list (* a list of all finalized types *)
16108
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
    47
     
16198
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
    48
     and defnode = Defnode of
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
    49
         typ  (* type of the constant in this particular definition *)
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
    50
         * ((noderef * (string option * edgelabel list) list) Symtab.table) (* The edges, grouped by nodes. *)
16108
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
    51
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
    52
and backref = Backref of
16198
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
    53
    noderef  (* the name of the node that has defnodes which reference a certain node A *)
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
    54
    * (unit Symtab.table) (* the names of the defnodes that DIRECTLY reference A. *)
16108
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
    55
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
    56
fun getnode graph noderef = the (Symtab.lookup (graph, noderef))
16158
2c3565b74b7a Removed final_consts from theory data. Now const_deps deals with final
obua
parents: 16113
diff changeset
    57
fun get_nodename (Node (n, _, _ ,_, _)) = n
2c3565b74b7a Removed final_consts from theory data. Now const_deps deals with final
obua
parents: 16113
diff changeset
    58
fun get_nodedefs (Node (_, _, defs, _, _)) = defs
2c3565b74b7a Removed final_consts from theory data. Now const_deps deals with final
obua
parents: 16113
diff changeset
    59
fun get_defnode (Node (_, _, defs, _, _)) defname = Symtab.lookup (defs, defname)
16108
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
    60
fun get_defnode' graph noderef defname = Symtab.lookup (get_nodedefs (the (Symtab.lookup (graph, noderef))), defname)
16158
2c3565b74b7a Removed final_consts from theory data. Now const_deps deals with final
obua
parents: 16113
diff changeset
    61
fun get_nodename (Node (n, _, _ , _, _)) = n
16108
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
    62
16158
2c3565b74b7a Removed final_consts from theory data. Now const_deps deals with final
obua
parents: 16113
diff changeset
    63
datatype graphaction = Declare of string * typ 
2c3565b74b7a Removed final_consts from theory data. Now const_deps deals with final
obua
parents: 16113
diff changeset
    64
		     | Define of string * typ * string * (string * typ) list
2c3565b74b7a Removed final_consts from theory data. Now const_deps deals with final
obua
parents: 16113
diff changeset
    65
		     | Finalize of string * typ
16108
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
    66
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
    67
type graph = (graphaction list) * (node Symtab.table)
16198
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
    68
             
16108
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
    69
val empty = ([], Symtab.empty)
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
    70
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
    71
exception DEFS of string;
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
    72
exception CIRCULAR of (typ * string * string) list;
16113
692fe6595755 Infinite chains in definitions are now detected, too.
obua
parents: 16108
diff changeset
    73
exception INFINITE_CHAIN of (typ * string * string) list;
16108
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
    74
exception CLASH of string * string * string;
16158
2c3565b74b7a Removed final_consts from theory data. Now const_deps deals with final
obua
parents: 16113
diff changeset
    75
exception FINAL of string * typ;
16108
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
    76
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
    77
fun def_err s = raise (DEFS s)
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
    78
16158
2c3565b74b7a Removed final_consts from theory data. Now const_deps deals with final
obua
parents: 16113
diff changeset
    79
fun declare (actions, g) (cty as (name, ty)) =
2c3565b74b7a Removed final_consts from theory data. Now const_deps deals with final
obua
parents: 16113
diff changeset
    80
    ((Declare cty)::actions, 
2c3565b74b7a Removed final_consts from theory data. Now const_deps deals with final
obua
parents: 16113
diff changeset
    81
     Symtab.update_new ((name, Node (name, Type.varifyT(Type.strip_sorts ty), Symtab.empty, Symtab.empty, [])), g))
2c3565b74b7a Removed final_consts from theory data. Now const_deps deals with final
obua
parents: 16113
diff changeset
    82
    handle Symtab.DUP _ => def_err "constant is already declared"
16108
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
    83
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
    84
fun rename ty1 ty2 = incr_tvar ((maxidx_of_typ ty1)+1) ty2;  
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
    85
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
    86
fun subst_incr_tvar inc t =
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
    87
    if (inc > 0) then 
16198
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
    88
      let
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
    89
	val tv = typ_tvars t
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
    90
	val t' = incr_tvar inc t
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
    91
	fun update_subst (((n,i), _), s) =
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
    92
	    Vartab.update (((n, i), ([], TVar ((n, i+inc), []))), s)
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
    93
      in
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
    94
	(t',List.foldl update_subst Vartab.empty tv)
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
    95
      end	
16108
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
    96
    else
16198
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
    97
      (t, Vartab.empty)
16108
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
    98
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
    99
(* Rename tys2 so that tys2 and tys1 do not have any variables in common any more.
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
   100
   As a result, return the renamed tys2' and the substitution that takes tys2 to tys2'. *)
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
   101
fun subst_rename max1 ty2 =
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
   102
    let
16198
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   103
      val max2 = (maxidx_of_typ ty2)
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   104
      val (ty2', s) = subst_incr_tvar (max1 + 1) ty2                
16108
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
   105
    in
16198
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   106
      (ty2', s, max1 + max2 + 1)
16108
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
   107
    end	       
16198
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   108
    
16108
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
   109
fun subst s ty = Envir.norm_type s ty
16198
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   110
                 
16108
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
   111
fun subst_history s history = map (fn (ty, cn, dn) => (subst s ty, cn, dn)) history
16198
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   112
                              
16108
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
   113
fun is_instance instance_ty general_ty =
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
   114
    Type.typ_instance Type.empty_tsig (instance_ty, general_ty)
16198
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   115
    
16108
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
   116
fun is_instance_r instance_ty general_ty =
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
   117
    is_instance instance_ty (rename instance_ty general_ty)
16198
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   118
    
16108
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
   119
fun unify ty1 ty2 = 
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
   120
    SOME (fst (Type.unify Type.empty_tsig (Vartab.empty, 0) (ty1, ty2)))
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
   121
    handle Type.TUNIFY => NONE
16198
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   122
                            
16108
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
   123
(* 
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
   124
   Unifies ty1 and ty2, renaming ty1 and ty2 so that they have greater indices than max and so that they
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
   125
   are different. All indices in ty1 and ty2 are supposed to be less than or equal to max.
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
   126
   Returns SOME (max', s1, s2), so that s1(ty1) = s2(ty2) and max' is greater or equal than all 
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
   127
   indices in s1, s2, ty1, ty2.
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
   128
*)
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
   129
fun unify_r max ty1 ty2 = 
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
   130
    let
16198
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   131
      val max =  Int.max(max, 0)
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   132
      val max1 = max (* >= maxidx_of_typ ty1 *)
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   133
      val max2 = max (* >= maxidx_of_typ ty2 *)
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   134
      val max = Int.max(max, Int.max (max1, max2))
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   135
      val (ty1, s1) = subst_incr_tvar (max+1) ty1
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   136
      val (ty2, s2) = subst_incr_tvar (max+max1+2) ty2
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   137
      val max = max+max1+max2+2	
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   138
      fun merge a b = Vartab.merge (fn _ => false) (a, b)
16108
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
   139
    in
16198
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   140
      case unify ty1 ty2 of
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   141
	NONE => NONE
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   142
      | SOME s => SOME (max, merge s1 s, merge s2 s)
16108
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
   143
    end
16198
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   144
    
16108
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
   145
fun can_be_unified_r ty1 ty2 =
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
   146
    let
16198
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   147
      val ty2 = rename ty1 ty2
16108
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
   148
    in
16198
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   149
      case unify ty1 ty2 of
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   150
	NONE => false
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   151
      | _ => true
16108
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
   152
    end
16198
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   153
    
16108
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
   154
fun can_be_unified ty1 ty2 =
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
   155
    case unify ty1 ty2 of
16198
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   156
      NONE => false
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   157
    | _ => true
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   158
           
16108
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
   159
fun checkT (Type (a, Ts)) = Type (a, map checkT Ts)
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
   160
  | checkT (TVar ((a, 0), _)) = TVar ((a, 0), [])
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
   161
  | checkT (TVar ((a, i), _)) = def_err "type is not clean"
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
   162
  | checkT (TFree (a, _)) = TVar ((a, 0), [])
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
   163
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
   164
fun label_ord NONE NONE = EQUAL
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
   165
  | label_ord NONE (SOME _) = LESS
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
   166
  | label_ord (SOME _) NONE = GREATER
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
   167
  | label_ord (SOME l1) (SOME l2) = string_ord (l1,l2)
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
   168
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
   169
fun compare_edges (e1 as (maxidx1, u1, v1, history1)) (e2 as (maxidx2, u2, v2, history2)) =
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
   170
    let
16198
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   171
      val t1 = u1 --> v1
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   172
      val t2 = u2 --> v2
16108
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
   173
    in
16198
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   174
      if (is_instance_r t1 t2) then
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   175
	(if is_instance_r t2 t1 then
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   176
	   SOME (int_ord (length history2, length history1))
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   177
	 else
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   178
	   SOME LESS)
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   179
      else if (is_instance_r t2 t1) then
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   180
	SOME GREATER
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   181
      else
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   182
	NONE
16108
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
   183
    end
16198
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   184
    
16108
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
   185
fun merge_edges_1 (x, []) = []
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
   186
  | merge_edges_1 (x, (y::ys)) = 
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
   187
    (case compare_edges x y of
16198
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   188
       SOME LESS => (y::ys)
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   189
     | SOME EQUAL => (y::ys)
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   190
     | SOME GREATER => merge_edges_1 (x, ys)
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   191
     | NONE => y::(merge_edges_1 (x, ys)))
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   192
    
16108
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
   193
fun merge_edges xs ys = foldl merge_edges_1 xs ys
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
   194
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
   195
fun pack_edges xs = merge_edges [] xs
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
   196
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
   197
fun merge_labelled_edges [] es = es
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
   198
  | merge_labelled_edges es [] = es
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
   199
  | merge_labelled_edges ((l1,e1)::es1) ((l2,e2)::es2) = 
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
   200
    (case label_ord l1 l2 of
16198
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   201
       LESS => (l1, e1)::(merge_labelled_edges es1 ((l2, e2)::es2))
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   202
     | GREATER => (l2, e2)::(merge_labelled_edges ((l1, e1)::es1) es2)
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   203
     | EQUAL => (l1, merge_edges e1 e2)::(merge_labelled_edges es1 es2))
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   204
    
16108
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
   205
fun defnode_edges_foldl f a defnode =
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
   206
    let
16198
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   207
      val (Defnode (ty, def_edges)) = defnode
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   208
      fun g (b, (_, (n, labelled_edges))) =
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   209
	  foldl (fn ((s, edges), b') => 
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   210
		    (foldl (fn (e, b'') => f ty n s e b'') b' edges))
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   211
		b
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   212
		labelled_edges		  		     
16108
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
   213
    in
16198
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   214
      Symtab.foldl g (a, def_edges)
16108
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
   215
    end	
16198
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   216
    
16158
2c3565b74b7a Removed final_consts from theory data. Now const_deps deals with final
obua
parents: 16113
diff changeset
   217
fun define (actions, graph) (name, ty) axname body =
16108
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
   218
    let
16198
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   219
      val ty = checkT ty
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   220
      val body = map (fn (n,t) => (n, checkT t)) body		 
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   221
      val mainref = name
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   222
      val mainnode  = (case Symtab.lookup (graph, mainref) of 
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   223
			 NONE => def_err ("constant "^mainref^" is not declared")
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   224
		       | SOME n => n)
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   225
      val (Node (n, gty, defs, backs, finals)) = mainnode
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   226
      val _ = (if is_instance_r ty gty then () else def_err "type of constant does not match declared type")
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   227
      fun check_def (s, Defnode (ty', _)) = 
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   228
	  (if can_be_unified_r ty ty' then 
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   229
	     raise (CLASH (mainref, axname, s))
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   230
	   else if s = axname then
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   231
	     def_err "name of axiom is already used for another definition of this constant"
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   232
	   else false)	
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   233
      val _ = Symtab.exists check_def defs
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   234
      fun check_final finalty = 
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   235
	  (if can_be_unified_r finalty ty then
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   236
	     raise (FINAL (mainref, finalty))
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   237
	   else
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   238
	     true)
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   239
      val _ = forall check_final finals
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   240
	             
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   241
      (* now we know that the only thing that can prevent acceptance of the definition is a cyclic dependency *)
16108
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
   242
16198
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   243
      (* body contains the constants that this constant definition depends on. For each element of body,
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   244
         the function make_edges_to calculates a group of edges that connect this constant with 
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   245
         the constant that is denoted by the element of the body *)
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   246
      fun make_edges_to (bodyn, bodyty) =
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   247
	  let
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   248
	    val bnode = 
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   249
		(case Symtab.lookup (graph, bodyn) of 
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   250
		   NONE => def_err "body of constant definition references undeclared constant"
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   251
		 | SOME x => x)
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   252
	    val (Node (_, general_btyp, bdefs, bbacks, bfinals)) = bnode
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   253
	  in
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   254
	    case unify_r 0 bodyty general_btyp of
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   255
	      NONE => NONE
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   256
	    | SOME (maxidx, sigma1, sigma2) => 
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   257
	      SOME (
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   258
	      let
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   259
		(* For each definition of the constant in the body, 
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   260
		   check if the definition unifies with the type of the constant in the body. *)	                
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   261
                fun make_edges ((swallowed, l),(def_name, Defnode (def_ty, _))) =
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   262
		    if swallowed then
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   263
		      (swallowed, l)
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   264
		    else 
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   265
		      (case unify_r 0 bodyty def_ty of
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   266
			 NONE => (swallowed, l)
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   267
		       | SOME (maxidx, sigma1, sigma2) => 
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   268
			 (is_instance_r bodyty def_ty,
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   269
			  merge_labelled_edges l [(SOME def_name,[(maxidx, subst sigma1 ty, subst sigma2 def_ty, [])])]))
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   270
                val swallowed = exists (is_instance_r bodyty) bfinals
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   271
          	val (swallowed, edges) = Symtab.foldl make_edges ((swallowed, []), bdefs)
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   272
	      in
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   273
		if swallowed then 
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   274
		  (bodyn, edges)
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   275
		else 
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   276
		  (bodyn, [(NONE, [(maxidx, subst sigma1 ty, subst sigma2 general_btyp,[])])]@edges)
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   277
	      end)
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   278
	  end 
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   279
          
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   280
      fun update_edges (b as (bodyn, bodyty), edges) =
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   281
	  (case make_edges_to b of
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   282
	     NONE => edges
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   283
	   | SOME m =>
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   284
	     (case Symtab.lookup (edges, bodyn) of
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   285
		NONE => Symtab.update ((bodyn, m), edges)
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   286
	      | SOME (_, es') => 
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   287
		let 
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   288
		  val (_, es) = m
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   289
		  val es = merge_labelled_edges es es'
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   290
		in
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   291
		  Symtab.update ((bodyn, (bodyn, es)), edges)
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   292
		end
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   293
	     )
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   294
	  )
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   295
          
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   296
      val edges = foldl update_edges Symtab.empty body
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   297
                  
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   298
      fun insert_edge edges (nodename, (defname_opt, edge)) = 
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   299
	  let
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   300
	    val newlink = [(defname_opt, [edge])]
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   301
	  in
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   302
	    case Symtab.lookup (edges, nodename) of
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   303
	      NONE => Symtab.update ((nodename, (nodename, newlink)), edges)		    
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   304
	    | SOME (_, links) => 
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   305
	      let
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   306
		val links' = merge_labelled_edges links newlink
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   307
	      in
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   308
		Symtab.update ((nodename, (nodename, links')), edges)
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   309
	      end
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   310
	  end				    
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   311
            
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   312
      (* We constructed all direct edges that this defnode has. 
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   313
         Now we have to construct the transitive hull by going a single step further. *)
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   314
          
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   315
      val thisDefnode = Defnode (ty, edges)
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   316
                        
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   317
      fun make_trans_edges _ noderef defname_opt (max1, alpha1, beta1, history1) edges = 
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   318
	  case defname_opt of 
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   319
	    NONE => edges
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   320
	  | SOME defname => 		
16108
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
   321
	    let
16198
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   322
	      val defnode = the (get_defnode' graph noderef defname)
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   323
	      fun make_trans_edge _ noderef2 defname_opt2 (max2, alpha2, beta2, history2) edges =
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   324
		  case unify_r (Int.max (max1, max2)) beta1 alpha2 of
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   325
		    NONE => edges
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   326
		  | SOME (max, sleft, sright) =>
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   327
		    insert_edge edges (noderef2, 
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   328
				       (defname_opt2, 							  
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   329
					(max, subst sleft alpha1, subst sright beta2, 
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   330
					 (subst_history sleft history1)@
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   331
					 ((subst sleft beta1, noderef, defname)::
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   332
					  (subst_history sright history2)))))
16108
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
   333
	    in
16198
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   334
	      defnode_edges_foldl make_trans_edge edges defnode
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   335
	    end
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   336
            
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   337
      val edges = defnode_edges_foldl make_trans_edges edges thisDefnode
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   338
                  
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   339
      val thisDefnode = Defnode (ty, edges)
16108
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
   340
16198
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   341
      (* We also have to add the backreferences that this new defnode induces. *)
16108
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
   342
	    
16198
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   343
      fun hasNONElink ((NONE, _)::_) = true
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   344
	| hasNONElink _ = false
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   345
	                  
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   346
      fun install_backref graph noderef pointingnoderef pointingdefname = 
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   347
	  let
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   348
	    val (Node (pname, _, _, _, _)) = getnode graph pointingnoderef
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   349
	    val (Node (name, ty, defs, backs, finals)) = getnode graph noderef
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   350
	  in
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   351
	    case Symtab.lookup (backs, pname) of
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   352
	      NONE => 
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   353
	      let 
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   354
		val defnames = Symtab.update ((pointingdefname, ()), Symtab.empty)
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   355
		val backs = Symtab.update ((pname, Backref (pointingnoderef, defnames)), backs)
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   356
	      in
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   357
		Symtab.update ((name, Node (name, ty, defs, backs, finals)), graph) 			
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   358
	      end
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   359
	    | SOME (Backref (pointingnoderef, defnames)) =>
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   360
	      let
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   361
		val defnames = Symtab.update_new ((pointingdefname, ()), defnames)
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   362
		val backs = Symtab.update ((pname, Backref (pointingnoderef, defnames)), backs)
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   363
	      in
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   364
		Symtab.update ((name, Node (name, ty, defs, backs, finals)), graph)
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   365
	      end
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   366
	      handle Symtab.DUP _ => graph
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   367
	  end
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   368
          
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   369
      fun install_backrefs (graph, (_, (noderef, labelled_edges))) =
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   370
	  if hasNONElink labelled_edges then
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   371
	    install_backref graph noderef mainref axname
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   372
	  else 
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   373
	    graph
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   374
            
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   375
      val graph = Symtab.foldl install_backrefs (graph, edges)
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   376
                  
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   377
      val (Node (_, _, _, backs, _)) = getnode graph mainref
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   378
      val graph = Symtab.update ((mainref, Node (n, gty, Symtab.update_new 
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   379
        ((axname, thisDefnode), defs), backs, finals)), graph)
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   380
		                
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   381
      (* Now we have to check all backreferences to this node and inform them about the new defnode. 
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   382
	 In this section we also check for circularity. *)
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   383
      fun update_backrefs ((backs, newedges), (nodename, Backref (noderef, defnames))) =	    
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   384
	  let
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   385
	    val node = getnode graph noderef
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   386
	    fun update_defs ((defnames, newedges),(defname, _)) =
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   387
		let
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   388
		  val (Defnode (_, defnode_edges)) = the (get_defnode node defname)
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   389
		  val (_, labelled_edges) = the (Symtab.lookup (defnode_edges, n))
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   390
						
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   391
	          (* the type of thisDefnode is ty *)
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   392
		  fun update (e as (max, alpha, beta, history), (none_edges, this_edges)) = 
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   393
		      case unify_r max beta ty of
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   394
			NONE => (e::none_edges, this_edges)
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   395
		      | SOME (max', s_beta, s_ty) =>
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   396
			let
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   397
			  val alpha' = subst s_beta alpha
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   398
			  val ty' = subst s_ty ty				      
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   399
			  val _ = 
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   400
			      if noderef = mainref andalso defname = axname then
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   401
				(case unify alpha' ty' of
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   402
				   NONE => 
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   403
				   if (is_instance_r ty' alpha') then
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   404
				     raise (INFINITE_CHAIN (
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   405
					    (alpha', mainref, axname)::
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   406
					    (subst_history s_beta history)@
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   407
					    [(ty', mainref, axname)]))
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   408
				   else ()
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   409
				 | SOME s => raise (CIRCULAR (
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   410
						    (subst s alpha', mainref, axname)::
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   411
						    (subst_history s (subst_history s_beta history))@
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   412
						    [(subst s ty', mainref, axname)])))
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   413
			      else ()
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   414
			  val edge = (max', alpha', ty', subst_history s_beta history)
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   415
			in
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   416
			  if is_instance_r beta ty then 
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   417
			    (none_edges, edge::this_edges)
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   418
			  else
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   419
			    (e::none_edges, edge::this_edges)
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   420
			end					    			   			    
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   421
		in
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   422
		  case labelled_edges of 
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   423
		    ((NONE, edges)::_) => 
16108
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
   424
		    let
16198
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   425
		      val (none_edges, this_edges) = foldl update ([], []) edges
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   426
		      val defnames = if none_edges = [] then defnames else Symtab.update_new ((defname, ()), defnames) 
16108
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
   427
		    in
16198
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   428
		      (defnames, (defname, none_edges, this_edges)::newedges)
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   429
		    end			    
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   430
		  | _ => sys_error "define: update_defs, internal error, corrupt backrefs"
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   431
		end
16108
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
   432
		    
16198
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   433
	    val (defnames, newedges') = Symtab.foldl update_defs ((Symtab.empty, []), defnames)
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   434
	  in
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   435
	    if Symtab.is_empty defnames then 
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   436
	      (backs, (noderef, newedges')::newedges)
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   437
	    else
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   438
	      let
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   439
		val backs = Symtab.update_new ((nodename, Backref (noderef, defnames)), backs)
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   440
	      in
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   441
		(backs, newedges)
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   442
	      end
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   443
	  end
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   444
	  
16108
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
   445
16198
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   446
      val (backs, newedges) = Symtab.foldl update_backrefs ((Symtab.empty, []), backs)
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   447
						 
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   448
      (* If a Circular exception is thrown then we never reach this point. *)
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   449
      (* Ok, the definition is consistent, let's update this node. *)
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   450
      val graph = Symtab.update ((mainref, Node (n, gty, Symtab.update 
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   451
        ((axname, thisDefnode), defs), backs, finals)), graph)
16108
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
   452
16198
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   453
      (* Furthermore, update all the other nodes that backreference this node. *)
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   454
      fun final_update_backrefs graph noderef defname none_edges this_edges =
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   455
	  let
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   456
	    val node = getnode graph noderef
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   457
	    val (Node (nodename, nodety, defs, backs, finals)) = node
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   458
	    val (Defnode (defnode_ty, defnode_edges)) = the (get_defnode node defname)
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   459
	    val (_, defnode_links) = the (Symtab.lookup (defnode_edges, n))
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   460
                                     
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   461
	    fun update edges none_edges this_edges =
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   462
		let 
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   463
		  val u = merge_labelled_edges edges [(SOME axname, pack_edges this_edges)]
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   464
		in
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   465
		  if none_edges = [] then
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   466
		    u
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   467
		  else
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   468
		    (NONE, pack_edges none_edges)::u
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   469
		end
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   470
		
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   471
	    val defnode_links' = 
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   472
		case defnode_links of 
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   473
		  ((NONE, _) :: edges) => update edges none_edges this_edges
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   474
		| edges => update edges none_edges this_edges
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   475
	    val defnode_edges' = Symtab.update ((n, (mainref, defnode_links')), defnode_edges)
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   476
	    val defs' = Symtab.update ((defname, Defnode (defnode_ty, defnode_edges')), defs)
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   477
	  in
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   478
	    Symtab.update ((nodename, Node (nodename, nodety, defs', backs, finals)), graph)
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   479
	  end
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   480
          
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   481
      val graph = foldl (fn ((noderef, newedges),graph) => foldl (fn ((defname, none_edges, this_edges), graph) =>
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   482
        final_update_backrefs graph noderef defname none_edges this_edges) graph newedges) graph newedges		    
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   483
                  
16108
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
   484
    in	    
16198
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   485
      ((Define (name, ty, axname, body))::actions, graph)	   
16108
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
   486
    end 
16198
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   487
    
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   488
fun finalize (history, graph) (c, ty) = 
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   489
    case Symtab.lookup (graph, c) of 
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   490
      NONE => def_err ("cannot finalize constant "^c^"; it is not declared")
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   491
    | SOME (Node (noderef, nodety, defs, backs, finals)) =>
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   492
      let 
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   493
	val ty = checkT ty
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   494
	val _ = if (not (is_instance_r ty nodety)) then
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   495
		  def_err ("only type instances of the declared constant "^c^" can be finalized")
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   496
		else ()
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   497
	val _ = Symtab.exists (fn (def_name, Defnode (def_ty, _)) =>  
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   498
				  if can_be_unified_r ty def_ty then 
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   499
				    def_err ("cannot finalize constant "^c^"; clash with definition "^def_name)
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   500
				  else 
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   501
				    false)
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   502
			      defs 
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   503
        
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   504
        fun update_finals [] = SOME [ty]
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   505
          | update_finals (final_ty::finals) = 
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   506
            (if is_instance_r ty final_ty then NONE
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   507
             else
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   508
               case update_finals finals of
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   509
                 NONE => NONE
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   510
               | (r as SOME finals) =>
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   511
                 if (is_instance_r final_ty ty) then
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   512
                   r
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   513
                 else
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   514
                   SOME (final_ty :: finals))                              
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   515
      in    
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   516
        case update_finals finals of
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   517
          NONE => (history, graph)
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   518
        | SOME finals => 
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   519
	  let
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   520
	    val graph = Symtab.update ((noderef, Node(noderef, nodety, defs, backs, finals)), graph)
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   521
	                
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   522
	    fun update_backref ((graph, backs), (backrefname, Backref (_, backdefnames))) =
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   523
		let
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   524
		  fun update_backdef ((graph, defnames), (backdefname, _)) = 
16158
2c3565b74b7a Removed final_consts from theory data. Now const_deps deals with final
obua
parents: 16113
diff changeset
   525
	              let 
16198
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   526
			val (backnode as Node (_, backty, backdefs, backbacks, backfinals)) = getnode graph backrefname
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   527
			val (Defnode (def_ty, all_edges)) = the (get_defnode backnode backdefname)						      
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   528
			val (defnames', all_edges') = 
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   529
			    case Symtab.lookup (all_edges, noderef) of
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   530
			      NONE => sys_error "finalize: corrupt backref"
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   531
			    | SOME (_, (NONE, edges)::rest) =>
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   532
			      let
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   533
				val edges' = List.filter (fn (_, _, beta, _) => not (is_instance_r beta ty)) edges
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   534
			      in
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   535
				if edges' = [] then 
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   536
				  (defnames, Symtab.update ((noderef, (noderef, rest)), all_edges))
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   537
				else
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   538
				  (Symtab.update ((backdefname, ()), defnames), 
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   539
				   Symtab.update ((noderef, (noderef, (NONE, edges')::rest)), all_edges))
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   540
			      end
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   541
			val defnode' = Defnode (def_ty, all_edges')
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   542
			val backnode' = Node (backrefname, backty, Symtab.update ((backdefname, defnode'), backdefs), 
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   543
					      backbacks, backfinals)
16158
2c3565b74b7a Removed final_consts from theory data. Now const_deps deals with final
obua
parents: 16113
diff changeset
   544
		      in
16198
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   545
			(Symtab.update ((backrefname, backnode'), graph), defnames')			  			  
16158
2c3565b74b7a Removed final_consts from theory data. Now const_deps deals with final
obua
parents: 16113
diff changeset
   546
		      end
16198
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   547
	              
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   548
		  val (graph', defnames') = Symtab.foldl update_backdef ((graph, Symtab.empty), backdefnames)
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   549
		in
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   550
		  (graph', if Symtab.is_empty defnames' then backs 
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   551
			   else Symtab.update ((backrefname, Backref (backrefname, defnames')), backs))
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   552
		end
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   553
	    val (graph', backs') = Symtab.foldl update_backref ((graph, Symtab.empty), backs)
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   554
	    val Node (_, _, defs, _, _) = getnode graph' noderef
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   555
	  in
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   556
	    ((Finalize (c, ty)) :: history, Symtab.update ((noderef, Node (noderef, nodety, defs, backs', finals)), graph'))
16158
2c3565b74b7a Removed final_consts from theory data. Now const_deps deals with final
obua
parents: 16113
diff changeset
   557
	  end
16198
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   558
      end
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   559
      
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   560
fun merge' (Declare cty, g) = (declare g cty handle _ => g)
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   561
  | merge' (Define (name, ty, axname, body), g as (_, graph)) = 
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   562
    (case Symtab.lookup (graph, name) of
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   563
       NONE => define g (name, ty) axname body
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   564
     | SOME (Node (_, _, defs, _, _)) => 
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   565
       (case Symtab.lookup (defs, axname) of
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   566
	  NONE => define g (name, ty) axname body
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   567
	| SOME _ => g))
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   568
  | merge' (Finalize finals, g) = finalize g finals 
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   569
                       
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   570
fun merge (actions, _) g = foldr merge' g actions
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   571
                           
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   572
fun finals (history, graph) = 
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   573
    Symtab.foldl 
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   574
      (fn (finals, (_, Node(name, _, _, _, ftys))) => Symtab.update_new ((name, ftys), finals))  
cfd070a2cc4d Integrates cycle detection in definitions with finalconsts
obua
parents: 16177
diff changeset
   575
      (Symtab.empty, graph)
16158
2c3565b74b7a Removed final_consts from theory data. Now const_deps deals with final
obua
parents: 16113
diff changeset
   576
16108
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
   577
end;
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
   578
		
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
   579
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
   580
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
   581
(*fun tvar name = TVar ((name, 0), [])
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
   582
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
   583
val bool = Type ("bool", [])
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
   584
val int = Type ("int", [])
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
   585
val alpha = tvar "'a"
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
   586
val beta = tvar "'b"
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
   587
val gamma = tvar "'c"
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
   588
fun pair a b = Type ("pair", [a,b])
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
   589
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
   590
val _ = print "make empty"
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
   591
val g = Defs.empty 
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
   592
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
   593
val _ = print "declare"
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
   594
val g = Defs.declare g "M" (alpha --> bool)
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
   595
val g = Defs.declare g "N" (beta --> bool)
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
   596
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
   597
val _ = print "define"
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
   598
val g = Defs.define g "N" (alpha --> bool) "defN" [("M", alpha --> bool)]
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
   599
val g = Defs.define g "M" (alpha --> bool) "defM" [("N", int --> alpha)]
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
   600
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
   601
val g = Defs.declare g "0" alpha
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
   602
val g = Defs.define g "0" (pair alpha beta) "zp" [("0", alpha), ("0", beta)]*)
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
   603
cf468b93a02e Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff changeset
   604