src/Pure/defs.ML
changeset 16361 cb31cb768a6c
parent 16308 636a1a84977a
child 16384 90c51c932154
     1.1 --- a/src/Pure/defs.ML	Fri Jun 10 19:21:16 2005 +0200
     1.2 +++ b/src/Pure/defs.ML	Sat Jun 11 12:55:25 2005 +0200
     1.3 @@ -42,26 +42,31 @@
     1.4  type tyenv = Type.tyenv
     1.5  type edgelabel = (int * typ * typ * (typ * string * string) list)
     1.6  
     1.7 +datatype forwardstate = Open | Closed | Final
     1.8 +
     1.9  datatype node = Node of
    1.10           typ  (* most general type of constant *)
    1.11 -         * defnode Symtab.table  
    1.12 +         * defnode Symtab.table
    1.13               (* a table of defnodes, each corresponding to 1 definition of the 
    1.14                  constant for a particular type, indexed by axiom name *)
    1.15           * (unit Symtab.table) Symtab.table 
    1.16               (* a table of all back referencing defnodes to this node, 
    1.17                  indexed by node name of the defnodes *)
    1.18           * typ list (* a list of all finalized types *)
    1.19 +         * forwardstate
    1.20       
    1.21       and defnode = Defnode of
    1.22           typ  (* type of the constant in this particular definition *)
    1.23           * (edgelabel list) Symtab.table (* The edges, grouped by nodes. *)
    1.24  
    1.25  fun getnode graph noderef = the (Symtab.lookup (graph, noderef))
    1.26 -fun get_nodedefs (Node (_, defs, _, _)) = defs
    1.27 -fun get_defnode (Node (_, defs, _, _)) defname = Symtab.lookup (defs, defname)
    1.28 +fun get_nodedefs (Node (_, defs, _, _, _)) = defs
    1.29 +fun get_defnode (Node (_, defs, _, _, _)) defname = Symtab.lookup (defs, defname)
    1.30  fun get_defnode' graph noderef defname = 
    1.31      Symtab.lookup (get_nodedefs (the (Symtab.lookup (graph, noderef))), defname)
    1.32  
    1.33 +fun table_size table = Symtab.foldl (fn (x, _) => x+1) (0, table)
    1.34 +        
    1.35  datatype graphaction = Declare of string * typ
    1.36  		     | Define of string * typ * string * (string * typ) list
    1.37  		     | Finalize of string * typ
    1.38 @@ -89,18 +94,17 @@
    1.39  
    1.40  fun def_err s = raise (DEFS s)
    1.41  
    1.42 +fun no_forwards defs = 
    1.43 +    Symtab.foldl 
    1.44 +    (fn (closed, (_, Defnode (_, edges))) => 
    1.45 +        if not closed then false else Symtab.is_empty edges)
    1.46 +    (true, defs)
    1.47 +
    1.48  fun checkT (Type (a, Ts)) = Type (a, map checkT Ts)
    1.49    | checkT (TVar ((a, 0), _)) = TVar ((a, 0), [])
    1.50    | checkT (TVar ((a, i), _)) = def_err "type is not clean"
    1.51    | checkT (TFree (a, _)) = TVar ((a, 0), [])
    1.52  
    1.53 -fun declare' (cost, actions, g) (cty as (name, ty)) =
    1.54 -    (cost, (Declare cty)::actions, 
    1.55 -     Symtab.update_new ((name, Node (ty, Symtab.empty, Symtab.empty, [])), g))
    1.56 -    handle Symtab.DUP _ => def_err "constant is already declared"
    1.57 -
    1.58 -fun declare g (name, ty) = declare' g (name, checkT ty)
    1.59 -
    1.60  fun rename ty1 ty2 = incr_tvar ((maxidx_of_typ ty1)+1) ty2;  
    1.61  
    1.62  fun subst_incr_tvar inc t =
    1.63 @@ -233,12 +237,27 @@
    1.64      
    1.65  fun merge_edges xs ys = foldl merge_edges_1 xs ys
    1.66  
    1.67 +fun declare' (g as (cost, actions, graph)) (cty as (name, ty)) =
    1.68 +    (cost, (Declare cty)::actions, 
    1.69 +     Symtab.update_new ((name, Node (ty, Symtab.empty, Symtab.empty, [], Open)), graph))
    1.70 +    handle Symtab.DUP _ => 
    1.71 +           let
    1.72 +             val (Node (gty, _, _, _, _)) = the (Symtab.lookup(graph, name))
    1.73 +           in
    1.74 +             if is_instance_r ty gty andalso is_instance_r gty ty then
    1.75 +               g
    1.76 +             else
    1.77 +               def_err "constant is already declared with different type"
    1.78 +           end
    1.79 +
    1.80 +fun declare g (name, ty) = declare' g (name, checkT ty)
    1.81 +
    1.82  fun define' (cost, actions, graph) (mainref, ty) axname body =
    1.83      let
    1.84        val mainnode  = (case Symtab.lookup (graph, mainref) of 
    1.85  			 NONE => def_err ("constant "^mainref^" is not declared")
    1.86  		       | SOME n => n)
    1.87 -      val (Node (gty, defs, backs, finals)) = mainnode
    1.88 +      val (Node (gty, defs, backs, finals, _)) = mainnode
    1.89        val _ = (if is_instance_r ty gty then () 
    1.90                 else def_err "type of constant does not match declared type")
    1.91        fun check_def (s, Defnode (ty', _)) = 
    1.92 @@ -257,7 +276,7 @@
    1.93  	             
    1.94        (* now we know that the only thing that can prevent acceptance of the definition 
    1.95           is a cyclic dependency *)
    1.96 -
    1.97 +              
    1.98        fun insert_edges edges (nodename, links) =
    1.99            (if links = [] then 
   1.100               edges
   1.101 @@ -278,8 +297,9 @@
   1.102  		(case Symtab.lookup (graph, bodyn) of 
   1.103  		   NONE => def_err "body of constant definition references undeclared constant"
   1.104  		 | SOME x => x)
   1.105 -	    val (Node (general_btyp, bdefs, bbacks, bfinals)) = bnode
   1.106 +	    val (Node (general_btyp, bdefs, bbacks, bfinals, closed)) = bnode
   1.107  	  in
   1.108 +            if closed = Final then edges else
   1.109  	    case unify_r 0 bodyty general_btyp of
   1.110  	      NONE => edges
   1.111  	    | SOME (maxidx, sigma1, sigma2) => 
   1.112 @@ -324,15 +344,18 @@
   1.113                      insert_edges edges 
   1.114                      (bodyn, [(maxidx, subst sigma1 ty, subst sigma2 general_btyp,[])])
   1.115  	        end
   1.116 -	  end 
   1.117 -                    
   1.118 +	  end                    
   1.119 +          
   1.120        val edges = foldl make_edges Symtab.empty body
   1.121                    				               
   1.122        (* We also have to add the backreferences that this new defnode induces. *)  
   1.123        fun install_backrefs (graph, (noderef, links)) =
   1.124            if links <> [] then
   1.125              let
   1.126 -              val (Node (ty, defs, backs, finals)) = getnode graph noderef
   1.127 +              val (Node (ty, defs, backs, finals, closed)) = getnode graph noderef
   1.128 +              val _ = if closed = Final then 
   1.129 +                        sys_error ("install_backrefs: closed node cannot be updated") 
   1.130 +                      else ()
   1.131                val defnames =
   1.132                    (case Symtab.lookup (backs, mainref) of
   1.133                       NONE => Symtab.empty
   1.134 @@ -340,17 +363,21 @@
   1.135                val defnames' = Symtab.update_new ((axname, ()), defnames)
   1.136                val backs' = Symtab.update ((mainref,defnames'), backs)
   1.137              in
   1.138 -              Symtab.update ((noderef, Node (ty, defs, backs', finals)), graph)
   1.139 +              Symtab.update ((noderef, Node (ty, defs, backs', finals, closed)), graph)
   1.140              end
   1.141            else
   1.142              graph
   1.143              
   1.144        val graph = Symtab.foldl install_backrefs (graph, edges)
   1.145                    
   1.146 -      val (Node (_, _, backs, _)) = getnode graph mainref
   1.147 +      val (Node (_, _, backs, _, closed)) = getnode graph mainref
   1.148 +      val closed = 
   1.149 +          if closed = Final then sys_error "define: closed node" 
   1.150 +          else if closed = Open andalso is_instance_r gty ty then Closed else closed
   1.151 +
   1.152        val thisDefnode = Defnode (ty, edges)
   1.153        val graph = Symtab.update ((mainref, Node (gty, Symtab.update_new 
   1.154 -        ((axname, thisDefnode), defs), backs, finals)), graph)
   1.155 +        ((axname, thisDefnode), defs), backs, finals, closed)), graph)
   1.156  		                
   1.157        (* Now we have to check all backreferences to this node and inform them about 
   1.158           the new defnode. In this section we also check for circularity. *)
   1.159 @@ -358,10 +385,13 @@
   1.160  	  let
   1.161  	    fun update_defs ((defnames, graph),(defname, _)) =
   1.162  		let
   1.163 -                  val (Node (nodety, nodedefs, nodebacks, nodefinals)) = getnode graph noderef
   1.164 +                  val (Node (nodety, nodedefs, nodebacks, nodefinals, closed)) = 
   1.165 +                      getnode graph noderef
   1.166 +                  val _ = if closed = Final then sys_error "update_defs: closed node" else ()
   1.167  		  val (Defnode (def_ty, defnode_edges)) = 
   1.168                        the (Symtab.lookup (nodedefs, defname))
   1.169  		  val edges = the (Symtab.lookup (defnode_edges, mainref))
   1.170 +                  val refclosed = ref false
   1.171   					
   1.172  	          (* the type of thisDefnode is ty *)
   1.173  		  fun update (e as (max, alpha, beta, history), (changed, edges)) = 
   1.174 @@ -409,9 +439,13 @@
   1.175                              Symtab.update ((mainref, edges'), defnode_edges)
   1.176                        val defnode' = Defnode (def_ty, defnode_edges')
   1.177                        val nodedefs' = Symtab.update ((defname, defnode'), nodedefs)
   1.178 +                      val closed = if closed = Closed andalso Symtab.is_empty defnode_edges'
   1.179 +                                      andalso no_forwards nodedefs' 
   1.180 +                                   then Final else closed
   1.181                        val graph' = 
   1.182                            Symtab.update 
   1.183 -                            ((noderef, Node (nodety, nodedefs', nodebacks, nodefinals)),graph) 
   1.184 +                            ((noderef, 
   1.185 +                              Node (nodety, nodedefs', nodebacks, nodefinals, closed)),graph) 
   1.186                      in
   1.187                        (defnames', graph')
   1.188                      end
   1.189 @@ -435,16 +469,26 @@
   1.190        val (backs, graph) = Symtab.foldl update_backrefs ((Symtab.empty, graph), backs)
   1.191                                          						 
   1.192        (* If a Circular exception is thrown then we never reach this point. *)
   1.193 -      val (Node (gty, defs, _, finals)) = getnode graph mainref
   1.194 -      val graph = Symtab.update ((mainref, Node (gty, defs, backs, finals)), graph) 
   1.195 +      val (Node (gty, defs, _, finals, closed)) = getnode graph mainref
   1.196 +      val closed = if closed = Closed andalso no_forwards defs then Final else closed
   1.197 +      val graph = Symtab.update ((mainref, Node (gty, defs, backs, finals, closed)), graph) 
   1.198 +      val actions' = (Define (mainref, ty, axname, body))::actions
   1.199      in	    
   1.200 -      (cost+3,(Define (mainref, ty, axname, body))::actions, graph)
   1.201 +      (cost+3,actions', graph)
   1.202      end 
   1.203      
   1.204 -fun define g (mainref, ty) axname body =
   1.205 +fun define (g as (_, _, graph)) (mainref, ty) axname body =
   1.206      let
   1.207        val ty = checkT ty
   1.208 -      val body = distinct (map (fn (n,t) => (n, checkT t)) body)
   1.209 +      fun checkbody (n, t) = 
   1.210 +          let 
   1.211 +            val (Node (_, _, _,_, closed)) = getnode graph n
   1.212 +          in
   1.213 +            case closed of
   1.214 +              Final => NONE
   1.215 +            | _ => SOME (n, checkT t)
   1.216 +          end
   1.217 +      val body = distinct (List.mapPartial checkbody body)
   1.218      in
   1.219        define' g (mainref, ty) axname body
   1.220      end
   1.221 @@ -452,7 +496,7 @@
   1.222  fun finalize' (cost, history, graph) (noderef, ty) = 
   1.223      case Symtab.lookup (graph, noderef) of 
   1.224        NONE => def_err ("cannot finalize constant "^noderef^"; it is not declared")
   1.225 -    | SOME (Node (nodety, defs, backs, finals)) =>
   1.226 +    | SOME (Node (nodety, defs, backs, finals, closed)) =>
   1.227        let 
   1.228  	val _ = 
   1.229              if (not (is_instance_r ty nodety)) then
   1.230 @@ -484,14 +528,18 @@
   1.231            NONE => (cost, history, graph)
   1.232          | SOME finals => 
   1.233  	  let
   1.234 -	    val graph = Symtab.update ((noderef, Node(nodety, defs, backs, finals)), 
   1.235 +            val closed = if closed = Open andalso is_instance_r nodety ty then 
   1.236 +                           Closed else 
   1.237 +                         closed
   1.238 +	    val graph = Symtab.update ((noderef, Node(nodety, defs, backs, finals, closed)), 
   1.239                                         graph)
   1.240  	                
   1.241  	    fun update_backref ((graph, backs), (backrefname, backdefnames)) =
   1.242  		let
   1.243  		  fun update_backdef ((graph, defnames), (backdefname, _)) = 
   1.244  	              let 
   1.245 -			val (backnode as Node (backty, backdefs, backbacks, backfinals)) = 
   1.246 +			val (backnode as Node (backty, backdefs, backbacks, 
   1.247 +                                               backfinals, backclosed)) = 
   1.248                              getnode graph backrefname
   1.249  			val (Defnode (def_ty, all_edges)) = 
   1.250                              the (get_defnode backnode backdefname)
   1.251 @@ -511,10 +559,13 @@
   1.252  				   Symtab.update ((noderef, edges'), all_edges))
   1.253  			      end
   1.254  			val defnode' = Defnode (def_ty, all_edges')
   1.255 +                        val backdefs' = Symtab.update ((backdefname, defnode'), backdefs)
   1.256 +                        val backclosed' = if backclosed = Closed andalso 
   1.257 +                                             Symtab.is_empty all_edges'
   1.258 +                                             andalso no_forwards backdefs'
   1.259 +                                          then Final else backclosed
   1.260  			val backnode' = 
   1.261 -                            Node (backty, 
   1.262 -                                  Symtab.update ((backdefname, defnode'), backdefs), 
   1.263 -				  backbacks, backfinals)
   1.264 +                            Node (backty, backdefs', backbacks, backfinals, backclosed')
   1.265  		      in
   1.266  			(Symtab.update ((backrefname, backnode'), graph), defnames') 
   1.267  		      end
   1.268 @@ -526,20 +577,23 @@
   1.269  			   else Symtab.update ((backrefname, defnames'), backs))
   1.270  		end
   1.271  	    val (graph', backs') = Symtab.foldl update_backref ((graph, Symtab.empty), backs)
   1.272 -	    val Node ( _, defs, _, _) = getnode graph' noderef
   1.273 -	    val graph' = Symtab.update ((noderef, Node (nodety, defs, backs', finals)), graph')
   1.274 +	    val Node ( _, defs, _, _, closed) = getnode graph' noderef
   1.275 +            val closed = if closed = Closed andalso no_forwards defs then Final else closed
   1.276 +	    val graph' = Symtab.update ((noderef, Node (nodety, defs, backs', 
   1.277 +                                                        finals, closed)), graph')
   1.278 +            val history' = (Finalize (noderef, ty)) :: history
   1.279  	  in
   1.280 -	    (cost+1,(Finalize (noderef, ty)) :: history, graph')
   1.281 +	    (cost+1, history', graph')
   1.282  	  end
   1.283        end
   1.284   
   1.285 -fun finalize g (noderef, ty) = finalize' g (noderef, checkT ty)
   1.286 +fun finalize g (noderef, ty) = finalize' g (noderef, checkT ty) 
   1.287  
   1.288 -fun merge' (Declare cty, g) = (declare' g cty handle _ => g)
   1.289 +fun merge' (Declare cty, g) = declare' g cty
   1.290    | merge' (Define (name, ty, axname, body), g as (_,_, graph)) = 
   1.291      (case Symtab.lookup (graph, name) of
   1.292         NONE => define' g (name, ty) axname body
   1.293 -     | SOME (Node (_, defs, _, _)) => 
   1.294 +     | SOME (Node (_, defs, _, _, _)) => 
   1.295         (case Symtab.lookup (defs, axname) of
   1.296  	  NONE => define' g (name, ty) axname body
   1.297  	| SOME _ => g))
   1.298 @@ -553,7 +607,8 @@
   1.299                             
   1.300  fun finals (cost, history, graph) = 
   1.301      Symtab.foldl 
   1.302 -      (fn (finals, (name, Node(_, _, _, ftys))) => Symtab.update_new ((name, ftys), finals))  
   1.303 +      (fn (finals, (name, Node(_, _, _, ftys, _))) => 
   1.304 +          Symtab.update_new ((name, ftys), finals)) 
   1.305        (Symtab.empty, graph)
   1.306  
   1.307  end;