# HG changeset patch # User obua # Date 1118487325 -7200 # Node ID cb31cb768a6c270bfc9e643daf8f1759b99a7d29 # Parent 6897b5958be7effcfd24329cd51d41e03b99c2ec further optimizations of cycle test diff -r 6897b5958be7 -r cb31cb768a6c src/Pure/defs.ML --- a/src/Pure/defs.ML Fri Jun 10 19:21:16 2005 +0200 +++ b/src/Pure/defs.ML Sat Jun 11 12:55:25 2005 +0200 @@ -42,26 +42,31 @@ type tyenv = Type.tyenv type edgelabel = (int * typ * typ * (typ * string * string) list) +datatype forwardstate = Open | Closed | Final + datatype node = Node of typ (* most general type of constant *) - * defnode Symtab.table + * defnode Symtab.table (* a table of defnodes, each corresponding to 1 definition of the constant for a particular type, indexed by axiom name *) * (unit Symtab.table) Symtab.table (* a table of all back referencing defnodes to this node, indexed by node name of the defnodes *) * typ list (* a list of all finalized types *) + * forwardstate and defnode = Defnode of typ (* type of the constant in this particular definition *) * (edgelabel list) Symtab.table (* The edges, grouped by nodes. *) fun getnode graph noderef = the (Symtab.lookup (graph, noderef)) -fun get_nodedefs (Node (_, defs, _, _)) = defs -fun get_defnode (Node (_, defs, _, _)) defname = Symtab.lookup (defs, defname) +fun get_nodedefs (Node (_, defs, _, _, _)) = defs +fun get_defnode (Node (_, defs, _, _, _)) defname = Symtab.lookup (defs, defname) fun get_defnode' graph noderef defname = Symtab.lookup (get_nodedefs (the (Symtab.lookup (graph, noderef))), defname) +fun table_size table = Symtab.foldl (fn (x, _) => x+1) (0, table) + datatype graphaction = Declare of string * typ | Define of string * typ * string * (string * typ) list | Finalize of string * typ @@ -89,18 +94,17 @@ fun def_err s = raise (DEFS s) +fun no_forwards defs = + Symtab.foldl + (fn (closed, (_, Defnode (_, edges))) => + if not closed then false else Symtab.is_empty edges) + (true, defs) + fun checkT (Type (a, Ts)) = Type (a, map checkT Ts) | checkT (TVar ((a, 0), _)) = TVar ((a, 0), []) | checkT (TVar ((a, i), _)) = def_err "type is not clean" | checkT (TFree (a, _)) = TVar ((a, 0), []) -fun declare' (cost, actions, g) (cty as (name, ty)) = - (cost, (Declare cty)::actions, - Symtab.update_new ((name, Node (ty, Symtab.empty, Symtab.empty, [])), g)) - handle Symtab.DUP _ => def_err "constant is already declared" - -fun declare g (name, ty) = declare' g (name, checkT ty) - fun rename ty1 ty2 = incr_tvar ((maxidx_of_typ ty1)+1) ty2; fun subst_incr_tvar inc t = @@ -233,12 +237,27 @@ fun merge_edges xs ys = foldl merge_edges_1 xs ys +fun declare' (g as (cost, actions, graph)) (cty as (name, ty)) = + (cost, (Declare cty)::actions, + Symtab.update_new ((name, Node (ty, Symtab.empty, Symtab.empty, [], Open)), graph)) + handle Symtab.DUP _ => + let + val (Node (gty, _, _, _, _)) = the (Symtab.lookup(graph, name)) + in + if is_instance_r ty gty andalso is_instance_r gty ty then + g + else + def_err "constant is already declared with different type" + end + +fun declare g (name, ty) = declare' g (name, checkT ty) + fun define' (cost, actions, graph) (mainref, ty) axname body = let val mainnode = (case Symtab.lookup (graph, mainref) of NONE => def_err ("constant "^mainref^" is not declared") | SOME n => n) - val (Node (gty, defs, backs, finals)) = mainnode + val (Node (gty, defs, backs, finals, _)) = mainnode val _ = (if is_instance_r ty gty then () else def_err "type of constant does not match declared type") fun check_def (s, Defnode (ty', _)) = @@ -257,7 +276,7 @@ (* now we know that the only thing that can prevent acceptance of the definition is a cyclic dependency *) - + fun insert_edges edges (nodename, links) = (if links = [] then edges @@ -278,8 +297,9 @@ (case Symtab.lookup (graph, bodyn) of NONE => def_err "body of constant definition references undeclared constant" | SOME x => x) - val (Node (general_btyp, bdefs, bbacks, bfinals)) = bnode + val (Node (general_btyp, bdefs, bbacks, bfinals, closed)) = bnode in + if closed = Final then edges else case unify_r 0 bodyty general_btyp of NONE => edges | SOME (maxidx, sigma1, sigma2) => @@ -324,15 +344,18 @@ insert_edges edges (bodyn, [(maxidx, subst sigma1 ty, subst sigma2 general_btyp,[])]) end - end - + end + val edges = foldl make_edges Symtab.empty body (* We also have to add the backreferences that this new defnode induces. *) fun install_backrefs (graph, (noderef, links)) = if links <> [] then let - val (Node (ty, defs, backs, finals)) = getnode graph noderef + val (Node (ty, defs, backs, finals, closed)) = getnode graph noderef + val _ = if closed = Final then + sys_error ("install_backrefs: closed node cannot be updated") + else () val defnames = (case Symtab.lookup (backs, mainref) of NONE => Symtab.empty @@ -340,17 +363,21 @@ val defnames' = Symtab.update_new ((axname, ()), defnames) val backs' = Symtab.update ((mainref,defnames'), backs) in - Symtab.update ((noderef, Node (ty, defs, backs', finals)), graph) + Symtab.update ((noderef, Node (ty, defs, backs', finals, closed)), graph) end else graph val graph = Symtab.foldl install_backrefs (graph, edges) - val (Node (_, _, backs, _)) = getnode graph mainref + val (Node (_, _, backs, _, closed)) = getnode graph mainref + val closed = + if closed = Final then sys_error "define: closed node" + else if closed = Open andalso is_instance_r gty ty then Closed else closed + val thisDefnode = Defnode (ty, edges) val graph = Symtab.update ((mainref, Node (gty, Symtab.update_new - ((axname, thisDefnode), defs), backs, finals)), graph) + ((axname, thisDefnode), defs), backs, finals, closed)), graph) (* Now we have to check all backreferences to this node and inform them about the new defnode. In this section we also check for circularity. *) @@ -358,10 +385,13 @@ let fun update_defs ((defnames, graph),(defname, _)) = let - val (Node (nodety, nodedefs, nodebacks, nodefinals)) = getnode graph noderef + val (Node (nodety, nodedefs, nodebacks, nodefinals, closed)) = + getnode graph noderef + val _ = if closed = Final then sys_error "update_defs: closed node" else () val (Defnode (def_ty, defnode_edges)) = the (Symtab.lookup (nodedefs, defname)) val edges = the (Symtab.lookup (defnode_edges, mainref)) + val refclosed = ref false (* the type of thisDefnode is ty *) fun update (e as (max, alpha, beta, history), (changed, edges)) = @@ -409,9 +439,13 @@ Symtab.update ((mainref, edges'), defnode_edges) val defnode' = Defnode (def_ty, defnode_edges') val nodedefs' = Symtab.update ((defname, defnode'), nodedefs) + val closed = if closed = Closed andalso Symtab.is_empty defnode_edges' + andalso no_forwards nodedefs' + then Final else closed val graph' = Symtab.update - ((noderef, Node (nodety, nodedefs', nodebacks, nodefinals)),graph) + ((noderef, + Node (nodety, nodedefs', nodebacks, nodefinals, closed)),graph) in (defnames', graph') end @@ -435,16 +469,26 @@ val (backs, graph) = Symtab.foldl update_backrefs ((Symtab.empty, graph), backs) (* If a Circular exception is thrown then we never reach this point. *) - val (Node (gty, defs, _, finals)) = getnode graph mainref - val graph = Symtab.update ((mainref, Node (gty, defs, backs, finals)), graph) + val (Node (gty, defs, _, finals, closed)) = getnode graph mainref + val closed = if closed = Closed andalso no_forwards defs then Final else closed + val graph = Symtab.update ((mainref, Node (gty, defs, backs, finals, closed)), graph) + val actions' = (Define (mainref, ty, axname, body))::actions in - (cost+3,(Define (mainref, ty, axname, body))::actions, graph) + (cost+3,actions', graph) end -fun define g (mainref, ty) axname body = +fun define (g as (_, _, graph)) (mainref, ty) axname body = let val ty = checkT ty - val body = distinct (map (fn (n,t) => (n, checkT t)) body) + fun checkbody (n, t) = + let + val (Node (_, _, _,_, closed)) = getnode graph n + in + case closed of + Final => NONE + | _ => SOME (n, checkT t) + end + val body = distinct (List.mapPartial checkbody body) in define' g (mainref, ty) axname body end @@ -452,7 +496,7 @@ fun finalize' (cost, history, graph) (noderef, ty) = case Symtab.lookup (graph, noderef) of NONE => def_err ("cannot finalize constant "^noderef^"; it is not declared") - | SOME (Node (nodety, defs, backs, finals)) => + | SOME (Node (nodety, defs, backs, finals, closed)) => let val _ = if (not (is_instance_r ty nodety)) then @@ -484,14 +528,18 @@ NONE => (cost, history, graph) | SOME finals => let - val graph = Symtab.update ((noderef, Node(nodety, defs, backs, finals)), + val closed = if closed = Open andalso is_instance_r nodety ty then + Closed else + closed + val graph = Symtab.update ((noderef, Node(nodety, defs, backs, finals, closed)), graph) fun update_backref ((graph, backs), (backrefname, backdefnames)) = let fun update_backdef ((graph, defnames), (backdefname, _)) = let - val (backnode as Node (backty, backdefs, backbacks, backfinals)) = + val (backnode as Node (backty, backdefs, backbacks, + backfinals, backclosed)) = getnode graph backrefname val (Defnode (def_ty, all_edges)) = the (get_defnode backnode backdefname) @@ -511,10 +559,13 @@ Symtab.update ((noderef, edges'), all_edges)) end val defnode' = Defnode (def_ty, all_edges') + val backdefs' = Symtab.update ((backdefname, defnode'), backdefs) + val backclosed' = if backclosed = Closed andalso + Symtab.is_empty all_edges' + andalso no_forwards backdefs' + then Final else backclosed val backnode' = - Node (backty, - Symtab.update ((backdefname, defnode'), backdefs), - backbacks, backfinals) + Node (backty, backdefs', backbacks, backfinals, backclosed') in (Symtab.update ((backrefname, backnode'), graph), defnames') end @@ -526,20 +577,23 @@ else Symtab.update ((backrefname, defnames'), backs)) end val (graph', backs') = Symtab.foldl update_backref ((graph, Symtab.empty), backs) - val Node ( _, defs, _, _) = getnode graph' noderef - val graph' = Symtab.update ((noderef, Node (nodety, defs, backs', finals)), graph') + val Node ( _, defs, _, _, closed) = getnode graph' noderef + val closed = if closed = Closed andalso no_forwards defs then Final else closed + val graph' = Symtab.update ((noderef, Node (nodety, defs, backs', + finals, closed)), graph') + val history' = (Finalize (noderef, ty)) :: history in - (cost+1,(Finalize (noderef, ty)) :: history, graph') + (cost+1, history', graph') end end -fun finalize g (noderef, ty) = finalize' g (noderef, checkT ty) +fun finalize g (noderef, ty) = finalize' g (noderef, checkT ty) -fun merge' (Declare cty, g) = (declare' g cty handle _ => g) +fun merge' (Declare cty, g) = declare' g cty | merge' (Define (name, ty, axname, body), g as (_,_, graph)) = (case Symtab.lookup (graph, name) of NONE => define' g (name, ty) axname body - | SOME (Node (_, defs, _, _)) => + | SOME (Node (_, defs, _, _, _)) => (case Symtab.lookup (defs, axname) of NONE => define' g (name, ty) axname body | SOME _ => g)) @@ -553,7 +607,8 @@ fun finals (cost, history, graph) = Symtab.foldl - (fn (finals, (name, Node(_, _, _, ftys))) => Symtab.update_new ((name, ftys), finals)) + (fn (finals, (name, Node(_, _, _, ftys, _))) => + Symtab.update_new ((name, ftys), finals)) (Symtab.empty, graph) end;