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