# HG changeset patch # User wenzelm # Date 1121786509 -7200 # Node ID e92cba1d4842125a9267027f6c1c4508930eccd2 # Parent f57b38cced32886985e8ccec044965663e1becee tuned interfaces declare, define, finalize, merge: canonical argument order, produce errors; tuned checkT'; diff -r f57b38cced32 -r e92cba1d4842 src/Pure/defs.ML --- a/src/Pure/defs.ML Tue Jul 19 17:21:47 2005 +0200 +++ b/src/Pure/defs.ML Tue Jul 19 17:21:49 2005 +0200 @@ -2,45 +2,33 @@ ID: $Id$ Author: Steven Obua, TU Muenchen - Checks if definitions preserve consistency of logic by enforcing - that there are no cyclic definitions. The algorithm is described in - "An Algorithm for Determining Definitional Cycles in Higher-Order Logic with Overloading", + Checks if definitions preserve consistency of logic by enforcing + that there are no cyclic definitions. The algorithm is described in + "An Algorithm for Determining Definitional Cycles in Higher-Order Logic with Overloading", Steven Obua, technical report, to be written :-) *) -signature DEFS = sig - +signature DEFS = +sig type graph - - exception DEFS of string - exception CIRCULAR of (typ * string * string) list - exception INFINITE_CHAIN of (typ * string * string) list - exception FINAL of string * typ - exception CLASH of string * string * string - - val empty : graph - val declare : graph -> string * typ -> graph (* exception DEFS *) - val define : graph -> string * typ -> string -> (string * typ) list -> graph - (* exception DEFS, CIRCULAR, INFINITE_CHAIN, CLASH, FINAL *) - - val finalize : graph -> string * typ -> graph (* exception DEFS *) + val empty: graph + val declare: string * typ -> graph -> graph + val define: Pretty.pp -> string * typ -> string -> (string * typ) list -> graph -> graph + val finalize: string * typ -> graph -> graph + val merge: Pretty.pp -> graph -> graph -> graph val finals : graph -> (typ list) Symtab.table - val merge : graph -> graph -> graph (* exception CIRCULAR, INFINITE_CHAIN, CLASH *) - (* If set to true then the exceptions CIRCULAR and INFINITE_CHAIN return the full - chain of definitions that lead to the exception. In the beginning, chain_history + chain of definitions that lead to the exception. In the beginning, chain_history is initialized with the Isabelle environment variable DEFS_CHAIN_HISTORY. *) val set_chain_history : bool -> unit val chain_history : unit -> bool datatype overloadingstate = Open | Closed | Final - val overloading_info : graph -> string -> (typ * (string*typ) list * overloadingstate) option val fast_overloading_info : graph -> string -> (typ * int * overloadingstate) option - end structure Defs :> DEFS = struct @@ -53,14 +41,14 @@ datatype node = Node of typ (* most general type of constant *) * defnode Symtab.table - (* a table of defnodes, each corresponding to 1 definition of the + (* 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, + * (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 *) * overloadingstate - + and defnode = Defnode of typ (* type of the constant in this particular definition *) * (edgelabel list) Symtab.table (* The edges, grouped by nodes. *) @@ -68,20 +56,20 @@ 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_defnode' graph noderef 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 * (string * typ) list - | Finalize of string * typ + | Define of string * typ * string * string * (string * typ) list + | Finalize of string * typ type graph = int * (string Symtab.table) * (graphaction list) * (node Symtab.table) - -val CHAIN_HISTORY = + +val CHAIN_HISTORY = let - fun f c = if Char.isSpace c then "" else String.str (Char.toUpper c) + fun f c = if Char.isSpace c then "" else String.str (Char.toUpper c) val env = String.translate f (getenv "DEFS_CHAIN_HISTORY") in ref (env = "ON" orelse env = "TRUE") @@ -100,74 +88,56 @@ fun def_err s = raise (DEFS s) -fun no_forwards defs = - Symtab.foldl - (fn (closed, (_, Defnode (_, edges))) => +fun no_forwards defs = + Symtab.foldl + (fn (closed, (_, Defnode (_, edges))) => if not closed then false else Symtab.is_empty edges) (true, defs) -exception No_Change; +fun checkT' (Type (a, Ts)) = Type (a, map checkT' Ts) + | checkT' (TFree (a, _)) = TVar ((a, 0), []) (* FIXME !? *) + | checkT' (TVar ((a, 0), _)) = TVar ((a, 0), []) + | checkT' (T as TVar _) = raise TYPE ("Illegal schematic type variable encountered", [T], []); -fun map_nc f list = - let - val changed = ref false - fun f' x = - let - val x' = f x - val _ = changed := true - in - x' - end handle No_Change => x - val list' = map f' list - in - if !changed then list' else raise No_Change - end +val checkT = Term.compress_type o checkT'; -fun checkT' (t as (Type (a, Ts))) = (Type (a, map_nc checkT' Ts) handle No_Change => t) - | checkT' (t as (TVar ((a, 0), []))) = raise No_Change - | checkT' (t as (TVar ((a, 0), _))) = TVar ((a, 0), []) - | checkT' (t as (TFree (a, _))) = TVar ((a, 0), []) - | checkT' _ = def_err "type is not clean" - -fun checkT t = Term.compress_type (checkT' t handle No_Change => t) - -fun rename ty1 ty2 = incr_tvar ((maxidx_of_typ ty1)+1) ty2; +fun rename ty1 ty2 = Logic.incr_tvar ((maxidx_of_typ ty1)+1) ty2; fun subst_incr_tvar inc t = - if (inc > 0) then + if (inc > 0) then let - val tv = typ_tvars t - val t' = incr_tvar inc t - fun update_subst (((n,i), _), s) = - Vartab.update (((n, i), ([], TVar ((n, i+inc), []))), s) + val tv = typ_tvars t + val t' = Logic.incr_tvar inc t + fun update_subst (((n,i), _), s) = + Vartab.update (((n, i), ([], TVar ((n, i+inc), []))), s) in - (t',List.foldl update_subst Vartab.empty tv) - end + (t',List.foldl update_subst Vartab.empty tv) + end else (t, Vartab.empty) - + fun subst s ty = Envir.norm_type s ty - + fun subst_history s history = map (fn (ty, cn, dn) => (subst s ty, cn, dn)) history - + fun is_instance instance_ty general_ty = Type.typ_instance Type.empty_tsig (instance_ty, general_ty) - + fun is_instance_r instance_ty general_ty = is_instance instance_ty (rename instance_ty general_ty) - -fun unify ty1 ty2 = + +fun unify ty1 ty2 = SOME (fst (Type.unify Type.empty_tsig (Vartab.empty, 0) (ty1, ty2))) handle Type.TUNIFY => NONE - -(* - Unifies ty1 and ty2, renaming ty1 and ty2 so that they have greater indices than max and - so that they are different. All indices in ty1 and ty2 are supposed to be less than or + +(* + Unifies ty1 and ty2, renaming ty1 and ty2 so that they have greater indices than max and + so that they are different. All indices in ty1 and ty2 are supposed to be less than or equal to max. - Returns SOME (max', s1, s2), so that s1(ty1) = s2(ty2) and max' is greater or equal than + Returns SOME (max', s1, s2), so that s1(ty1) = s2(ty2) and max' is greater or equal than all indices in s1, s2, ty1, ty2. *) -fun unify_r max ty1 ty2 = +fun unify_r max ty1 ty2 = let val max = Int.max(max, 0) val max1 = max (* >= maxidx_of_typ ty1 *) @@ -175,35 +145,35 @@ val max = Int.max(max, Int.max (max1, max2)) val (ty1, s1) = subst_incr_tvar (max + 1) ty1 val (ty2, s2) = subst_incr_tvar (max + max1 + 2) ty2 - val max = max + max1 + max2 + 2 + val max = max + max1 + max2 + 2 fun merge a b = Vartab.merge (fn _ => false) (a, b) in case unify ty1 ty2 of - NONE => NONE + NONE => NONE | SOME s => SOME (max, merge s1 s, merge s2 s) end - + fun can_be_unified_r ty1 ty2 = let val ty2 = rename ty1 ty2 in case unify ty1 ty2 of - NONE => false + NONE => false | _ => true end - + fun can_be_unified ty1 ty2 = case unify ty1 ty2 of NONE => false | _ => true - + fun normalize_edge_idx (edge as (maxidx, u1, v1, history)) = if maxidx <= 1000000 then edge else let - - fun idxlist idx extract_ty inject_ty (tab, max) ts = - foldr - (fn (e, ((tab, max), ts)) => + + fun idxlist idx extract_ty inject_ty (tab, max) ts = + foldr + (fn (e, ((tab, max), ts)) => let val ((tab, max), ty) = idx (tab, max) (extract_ty e) val e = inject_ty (ty, e) @@ -211,60 +181,60 @@ ((tab, max), e::ts) end) ((tab,max), []) ts - - fun idx (tab,max) (TVar ((a,i),_)) = - (case Inttab.lookup (tab, i) of + + fun idx (tab,max) (TVar ((a,i),_)) = + (case Inttab.lookup (tab, i) of SOME j => ((tab, max), TVar ((a,j),[])) | NONE => ((Inttab.update ((i, max), tab), max+1), TVar ((a,max),[]))) - | idx (tab,max) (Type (t, ts)) = - let + | idx (tab,max) (Type (t, ts)) = + let val ((tab, max), ts) = idxlist idx I fst (tab, max) ts in ((tab,max), Type (t, ts)) end | idx (tab, max) ty = ((tab, max), ty) - + val ((tab,max), u1) = idx (Inttab.empty, 0) u1 val ((tab,max), v1) = idx (tab, max) v1 - val ((tab,max), history) = + val ((tab,max), history) = idxlist idx - (fn (ty,_,_) => ty) - (fn (ty, (_, s1, s2)) => (ty, s1, s2)) + (fn (ty,_,_) => ty) + (fn (ty, (_, s1, s2)) => (ty, s1, s2)) (tab, max) history in (max, u1, v1, history) end - + fun compare_edges (e1 as (maxidx1, u1, v1, history1)) (e2 as (maxidx2, u2, v2, history2)) = let val t1 = u1 --> v1 - val t2 = incr_tvar (maxidx1+1) (u2 --> v2) + val t2 = Logic.incr_tvar (maxidx1+1) (u2 --> v2) in if (is_instance t1 t2) then - (if is_instance t2 t1 then - SOME (int_ord (length history2, length history1)) - else - SOME LESS) + (if is_instance t2 t1 then + SOME (int_ord (length history2, length history1)) + else + SOME LESS) else if (is_instance t2 t1) then - SOME GREATER + SOME GREATER else - NONE + NONE end fun merge_edges_1 (x, []) = [x] - | merge_edges_1 (x, (y::ys)) = + | merge_edges_1 (x, (y::ys)) = (case compare_edges x y of SOME LESS => (y::ys) | SOME EQUAL => (y::ys) | SOME GREATER => merge_edges_1 (x, ys) | NONE => y::(merge_edges_1 (x, ys))) - + fun merge_edges xs ys = foldl merge_edges_1 xs ys fun declare' (g as (cost, axmap, actions, graph)) (cty as (name, ty)) = - (cost, axmap, (Declare cty)::actions, + (cost, axmap, (Declare cty)::actions, Symtab.update_new ((name, Node (ty, Symtab.empty, Symtab.empty, [], Open)), graph)) - handle Symtab.DUP _ => + handle Symtab.DUP _ => let val (Node (gty, _, _, _, _)) = the (Symtab.lookup(graph, name)) in @@ -274,7 +244,7 @@ def_err "constant is already declared with different type" end -fun declare g (name, ty) = declare' g (name, checkT ty) +fun declare'' g (name, ty) = declare' g (name, checkT ty) val axcounter = ref (IntInf.fromInt 0) fun newaxname axmap axname = @@ -286,9 +256,9 @@ (Symtab.update ((axname', axname), axmap), axname') end -fun translate_ex axmap x = +fun translate_ex axmap x = let - fun translate (ty, nodename, axname) = + fun translate (ty, nodename, axname) = (ty, nodename, the (Symtab.lookup (axmap, axname))) in case x of @@ -299,107 +269,107 @@ fun define' (cost, axmap, actions, graph) (mainref, ty) axname orig_axname body = let - val mainnode = (case Symtab.lookup (graph, mainref) of - NONE => def_err ("constant "^mainref^" is not declared") - | SOME n => n) + 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 _ = (if is_instance_r ty gty then () + 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', _)) = - (if can_be_unified_r ty ty' then - raise (CLASH (mainref, axname, s)) - else if s = axname then - def_err "name of axiom is already used for another definition of this constant" - else false) + fun check_def (s, Defnode (ty', _)) = + (if can_be_unified_r ty ty' then + raise (CLASH (mainref, axname, s)) + else if s = axname then + def_err "name of axiom is already used for another definition of this constant" + else false) val _ = Symtab.exists check_def defs - fun check_final finalty = - (if can_be_unified_r finalty ty then - raise (FINAL (mainref, finalty)) - else - true) + fun check_final finalty = + (if can_be_unified_r finalty ty then + raise (FINAL (mainref, finalty)) + else + true) val _ = forall check_final finals - - (* now we know that the only thing that can prevent acceptance of the definition + + (* 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 + (if links = [] then edges else let val links = map normalize_edge_idx links in - Symtab.update ((nodename, - case Symtab.lookup (edges, nodename) of - NONE => links - | SOME links' => merge_edges links' links), + Symtab.update ((nodename, + case Symtab.lookup (edges, nodename) of + NONE => links + | SOME links' => merge_edges links' links), edges) end) - + fun make_edges ((bodyn, bodyty), edges) = - let - val bnode = - (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, closed)) = bnode - in + let + val bnode = + (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, closed)) = bnode + in if closed = Final then edges else - case unify_r 0 bodyty general_btyp of - NONE => edges - | SOME (maxidx, sigma1, sigma2) => - if exists (is_instance_r bodyty) bfinals then + case unify_r 0 bodyty general_btyp of + NONE => edges + | SOME (maxidx, sigma1, sigma2) => + if exists (is_instance_r bodyty) bfinals then edges else - let - fun insert_trans_edges ((step1, edges), (nodename, links)) = + let + fun insert_trans_edges ((step1, edges), (nodename, links)) = let val (maxidx1, alpha1, beta1, defname) = step1 - fun connect (maxidx2, alpha2, beta2, history) = - case unify_r (Int.max (maxidx1, maxidx2)) beta1 alpha2 of - NONE => NONE - | SOME (max, sleft, sright) => - SOME (max, subst sleft alpha1, subst sright beta2, - if !CHAIN_HISTORY then - ((subst sleft beta1, bodyn, defname):: - (subst_history sright history)) - else []) + fun connect (maxidx2, alpha2, beta2, history) = + case unify_r (Int.max (maxidx1, maxidx2)) beta1 alpha2 of + NONE => NONE + | SOME (max, sleft, sright) => + SOME (max, subst sleft alpha1, subst sright beta2, + if !CHAIN_HISTORY then + ((subst sleft beta1, bodyn, defname):: + (subst_history sright history)) + else []) val links' = List.mapPartial connect links in (step1, insert_edges edges (nodename, links')) end - + fun make_edges' ((swallowed, edges), (def_name, Defnode (def_ty, def_edges))) = - if swallowed then - (swallowed, edges) - else - (case unify_r 0 bodyty def_ty of - NONE => (swallowed, edges) - | SOME (maxidx, sigma1, sigma2) => - (is_instance_r bodyty def_ty, - snd (Symtab.foldl insert_trans_edges + if swallowed then + (swallowed, edges) + else + (case unify_r 0 bodyty def_ty of + NONE => (swallowed, edges) + | SOME (maxidx, sigma1, sigma2) => + (is_instance_r bodyty def_ty, + snd (Symtab.foldl insert_trans_edges (((maxidx, subst sigma1 ty, subst sigma2 def_ty, def_name), edges), def_edges)))) - val (swallowed, edges) = Symtab.foldl make_edges' ((false, edges), bdefs) - in - if swallowed then - edges - else - insert_edges edges + val (swallowed, edges) = Symtab.foldl make_edges' ((false, edges), bdefs) + in + if swallowed then + edges + else + insert_edges edges (bodyn, [(maxidx, subst sigma1 ty, subst sigma2 general_btyp,[])]) - end - end - + end + end + val edges = foldl make_edges Symtab.empty body - - (* We also have to add the backreferences that this new defnode induces. *) + + (* 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, closed)) = getnode graph noderef - val _ = if closed = Final then - sys_error ("install_backrefs: closed node cannot be updated") + val _ = if closed = Final then + sys_error ("install_backrefs: closed node cannot be updated") else () val defnames = (case Symtab.lookup (backs, mainref) of @@ -412,72 +382,72 @@ end else graph - + val graph = Symtab.foldl install_backrefs (graph, edges) - + val (Node (_, _, backs, _, closed)) = getnode graph mainref - val closed = - if closed = Final then sys_error "define: closed node" + 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 + val graph = Symtab.update ((mainref, Node (gty, Symtab.update_new ((axname, thisDefnode), defs), backs, finals, closed)), graph) - - (* Now we have to check all backreferences to this node and inform them about + + (* 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. *) fun update_backrefs ((backs, graph), (noderef, defnames)) = - let - fun update_defs ((defnames, graph),(defname, _)) = - let - val (Node (nodety, nodedefs, nodebacks, nodefinals, closed)) = + let + fun update_defs ((defnames, graph),(defname, _)) = + let + 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)) = + val (Defnode (def_ty, defnode_edges)) = the (Symtab.lookup (nodedefs, defname)) - val edges = the (Symtab.lookup (defnode_edges, mainref)) + 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)) = - case unify_r max beta ty of - NONE => (changed, e::edges) - | SOME (max', s_beta, s_ty) => - let - val alpha' = subst s_beta alpha - val ty' = subst s_ty ty - val _ = - if noderef = mainref andalso defname = axname then - (case unify alpha' ty' of - NONE => - if (is_instance_r ty' alpha') then - raise (INFINITE_CHAIN ( - (alpha', mainref, axname):: - (subst_history s_beta history)@ - [(ty', mainref, axname)])) - else () - | SOME s => + + (* the type of thisDefnode is ty *) + fun update (e as (max, alpha, beta, history), (changed, edges)) = + case unify_r max beta ty of + NONE => (changed, e::edges) + | SOME (max', s_beta, s_ty) => + let + val alpha' = subst s_beta alpha + val ty' = subst s_ty ty + val _ = + if noderef = mainref andalso defname = axname then + (case unify alpha' ty' of + NONE => + if (is_instance_r ty' alpha') then + raise (INFINITE_CHAIN ( + (alpha', mainref, axname):: + (subst_history s_beta history)@ + [(ty', mainref, axname)])) + else () + | SOME s => raise (CIRCULAR ( - (subst s alpha', mainref, axname):: - (subst_history s (subst_history s_beta history))@ - [(subst s ty', mainref, axname)]))) - else () - in - if is_instance_r beta ty then - (true, edges) - else - (changed, e::edges) - end - + (subst s alpha', mainref, axname):: + (subst_history s (subst_history s_beta history))@ + [(subst s ty', mainref, axname)]))) + else () + in + if is_instance_r beta ty then + (true, edges) + else + (changed, e::edges) + end + val (changed, edges') = foldl update (false, []) edges - val defnames' = if edges' = [] then - defnames - else + val defnames' = if edges' = [] then + defnames + else Symtab.update ((defname, ()), defnames) in if changed then let - val defnode_edges' = + val defnode_edges' = if edges' = [] then Symtab.delete mainref defnode_edges else @@ -485,48 +455,48 @@ 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' + andalso no_forwards nodedefs' then Final else closed - val graph' = - Symtab.update - ((noderef, - Node (nodety, nodedefs', nodebacks, nodefinals, closed)),graph) + val graph' = + Symtab.update + ((noderef, + Node (nodety, nodedefs', nodebacks, nodefinals, closed)),graph) in (defnames', graph') end else (defnames', graph) end - - val (defnames', graph') = Symtab.foldl update_defs + + val (defnames', graph') = Symtab.foldl update_defs ((Symtab.empty, graph), defnames) - in - if Symtab.is_empty defnames' then - (backs, graph') - else - let - val backs' = Symtab.update_new ((noderef, defnames'), backs) - in - (backs', graph') - end - end - + in + if Symtab.is_empty defnames' then + (backs, graph') + else + let + val backs' = Symtab.update_new ((noderef, defnames'), backs) + in + (backs', graph') + end + end + 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, 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 graph = Symtab.update ((mainref, Node (gty, defs, backs, finals, closed)), graph) val actions' = (Define (mainref, ty, axname, orig_axname, body))::actions - in + in (cost+3, axmap, actions', graph) end handle ex => translate_ex axmap ex - -fun define (g as (cost, axmap, actions, graph)) (mainref, ty) orig_axname body = + +fun define'' (g as (cost, axmap, actions, graph)) (mainref, ty) orig_axname body = let val ty = checkT ty - fun checkbody (n, t) = - let + fun checkbody (n, t) = + let val (Node (_, _, _,_, closed)) = getnode graph n in case closed of @@ -539,27 +509,27 @@ define' (cost, axmap, actions, graph) (mainref, ty) axname orig_axname body end -fun finalize' (cost, axmap, history, graph) (noderef, ty) = - case Symtab.lookup (graph, noderef) of +fun finalize' (cost, axmap, 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, closed)) => - let - val _ = + let + val _ = if (not (is_instance_r ty nodety)) then - def_err ("only type instances of the declared constant "^ + def_err ("only type instances of the declared constant "^ noderef^" can be finalized") - else () - val _ = Symtab.exists - (fn (def_name, Defnode (def_ty, _)) => - if can_be_unified_r ty def_ty then - def_err ("cannot finalize constant "^noderef^ + else () + val _ = Symtab.exists + (fn (def_name, Defnode (def_ty, _)) => + if can_be_unified_r ty def_ty then + def_err ("cannot finalize constant "^noderef^ "; clash with definition "^def_name) - else - false) - defs - + else + false) + defs + fun update_finals [] = SOME [ty] - | update_finals (final_ty::finals) = + | update_finals (final_ty::finals) = (if is_instance_r ty final_ty then NONE else case update_finals finals of @@ -568,99 +538,99 @@ if (is_instance_r final_ty ty) then r else - SOME (final_ty :: finals)) - in + SOME (final_ty :: finals)) + in case update_finals finals of NONE => (cost, axmap, history, graph) - | SOME finals => - let - val closed = if closed = Open andalso is_instance_r nodety ty then - Closed else + | SOME finals => + let + 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)), + 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, backclosed)) = + + fun update_backref ((graph, backs), (backrefname, backdefnames)) = + let + fun update_backdef ((graph, defnames), (backdefname, _)) = + let + val (backnode as Node (backty, backdefs, backbacks, + backfinals, backclosed)) = getnode graph backrefname - val (Defnode (def_ty, all_edges)) = + val (Defnode (def_ty, all_edges)) = the (get_defnode backnode backdefname) - val (defnames', all_edges') = - case Symtab.lookup (all_edges, noderef) of - NONE => sys_error "finalize: corrupt backref" - | SOME edges => - let - val edges' = List.filter (fn (_, _, beta, _) => + val (defnames', all_edges') = + case Symtab.lookup (all_edges, noderef) of + NONE => sys_error "finalize: corrupt backref" + | SOME edges => + let + val edges' = List.filter (fn (_, _, beta, _) => not (is_instance_r beta ty)) edges - in - if edges' = [] then - (defnames, Symtab.delete noderef all_edges) - else - (Symtab.update ((backdefname, ()), defnames), - Symtab.update ((noderef, edges'), all_edges)) - end - val defnode' = Defnode (def_ty, all_edges') + in + if edges' = [] then + (defnames, Symtab.delete noderef all_edges) + else + (Symtab.update ((backdefname, ()), defnames), + 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 + val backclosed' = if backclosed = Closed andalso Symtab.is_empty all_edges' andalso no_forwards backdefs' then Final else backclosed - val backnode' = + val backnode' = Node (backty, backdefs', backbacks, backfinals, backclosed') - in - (Symtab.update ((backrefname, backnode'), graph), defnames') - end - - val (graph', defnames') = + in + (Symtab.update ((backrefname, backnode'), graph), defnames') + end + + val (graph', defnames') = Symtab.foldl update_backdef ((graph, Symtab.empty), backdefnames) - in - (graph', if Symtab.is_empty defnames' then backs - else Symtab.update ((backrefname, defnames'), backs)) - end - val (graph', backs') = Symtab.foldl update_backref ((graph, Symtab.empty), backs) - val Node ( _, defs, _, _, closed) = getnode graph' noderef + in + (graph', if Symtab.is_empty defnames' then backs + else Symtab.update ((backrefname, defnames'), backs)) + end + val (graph', backs') = Symtab.foldl update_backref ((graph, Symtab.empty), backs) + 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', + val graph' = Symtab.update ((noderef, Node (nodety, defs, backs', finals, closed)), graph') val history' = (Finalize (noderef, ty)) :: history - in - (cost+1, axmap, history', graph') - end + in + (cost+1, axmap, 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 update_axname ax orig_ax (cost, axmap, history, graph) = (cost, Symtab.update ((ax, orig_ax), axmap), history, graph) fun merge' (Declare cty, g) = declare' g cty - | merge' (Define (name, ty, axname, orig_axname, body), g as (cost, axmap, history, graph)) = + | merge' (Define (name, ty, axname, orig_axname, body), g as (cost, axmap, history, graph)) = (case Symtab.lookup (graph, name) of NONE => define' (update_axname axname orig_axname g) (name, ty) axname orig_axname body - | SOME (Node (_, defs, _, _, _)) => + | SOME (Node (_, defs, _, _, _)) => (case Symtab.lookup (defs, axname) of - NONE => define' (update_axname axname orig_axname g) (name, ty) axname orig_axname body - | SOME _ => g)) - | merge' (Finalize finals, g) = finalize' g finals - -fun merge (g1 as (cost1, _, actions1, _)) (g2 as (cost2, _, actions2, _)) = + NONE => define' (update_axname axname orig_axname g) (name, ty) axname orig_axname body + | SOME _ => g)) + | merge' (Finalize finals, g) = finalize' g finals + +fun merge'' (g1 as (cost1, _, actions1, _)) (g2 as (cost2, _, actions2, _)) = if cost1 < cost2 then foldr merge' g2 actions1 else foldr merge' g1 actions2 - -fun finals (_, _, history, graph) = - Symtab.foldl - (fn (finals, (name, Node(_, _, _, ftys, _))) => - Symtab.update_new ((name, ftys), finals)) + +fun finals (_, _, history, graph) = + Symtab.foldl + (fn (finals, (name, Node(_, _, _, ftys, _))) => + Symtab.update_new ((name, ftys), finals)) (Symtab.empty, graph) -fun overloading_info (_, axmap, _, graph) c = +fun overloading_info (_, axmap, _, graph) c = let fun translate (ax, Defnode (ty, _)) = (the (Symtab.lookup (axmap, ax)), ty) in @@ -669,9 +639,9 @@ | SOME (Node (ty, defnodes, _, _, state)) => SOME (ty, map translate (Symtab.dest defnodes), state) end - -fun fast_overloading_info (_, _, _, graph) c = - let + +fun fast_overloading_info (_, _, _, graph) c = + let fun count (c, _) = c+1 in case Symtab.lookup (graph, c) of @@ -680,8 +650,61 @@ SOME (ty, Symtab.foldl count (0, defnodes), state) end + + +(** diagnostics **) + +fun pretty_const pp (c, T) = + [Pretty.str c, Pretty.str " ::", Pretty.brk 1, + Pretty.quote (Pretty.typ pp (Type.freeze_type T))]; (* FIXME zero indexes!? *) + +fun pretty_path pp path = fold_rev (fn (T, c, def) => + fn [] => [Pretty.block (pretty_const pp (c, T))] + | prts => Pretty.block (pretty_const pp (c, T) @ + [Pretty.brk 1, Pretty.str ("depends via " ^ quote def ^ " on")]) :: prts) path []; + +fun chain_history_msg s = (* FIXME huh!? *) + if chain_history () then s ^ ": " + else s ^ " (set DEFS_CHAIN_HISTORY=ON for full history): "; + +fun defs_circular pp path = + Pretty.str (chain_history_msg "Cyclic dependency of definitions") :: pretty_path pp path + |> Pretty.chunks |> Pretty.string_of; + +fun defs_infinite_chain pp path = + Pretty.str (chain_history_msg "Infinite chain of definitions") :: pretty_path pp path + |> Pretty.chunks |> Pretty.string_of; + +fun defs_clash def1 def2 = "Type clash in definitions " ^ quote def1 ^ " and " ^ quote def2; + +fun defs_final pp const = + (Pretty.str "Attempt to define final constant" :: Pretty.brk 1 :: pretty_const pp const) + |> Pretty.block |> Pretty.string_of; + + +(* external interfaces *) + +fun declare const defs = + if_none (try (declare'' defs) const) defs; + +fun define pp const name rhs defs = + define'' defs const name rhs + handle DEFS msg => sys_error msg + | CIRCULAR path => error (defs_circular pp path) + | INFINITE_CHAIN path => error (defs_infinite_chain pp path) + | CLASH (_, def1, def2) => error (defs_clash def1 def2) + | FINAL const => error (defs_final pp const); + +fun finalize const defs = + finalize'' defs const handle DEFS msg => sys_error msg; + +fun merge pp defs1 defs2 = + merge'' defs1 defs2 + handle CIRCULAR namess => error (defs_circular pp namess) + | INFINITE_CHAIN namess => error (defs_infinite_chain pp namess); + end; - + (* fun tvar name = TVar ((name, 0), []) @@ -697,7 +720,7 @@ val name = Type ("name", []) val _ = print "make empty" -val g = Defs.empty +val g = Defs.empty val _ = print "declare perm" val g = Defs.declare g ("perm", prm alpha --> beta --> beta) @@ -706,7 +729,7 @@ val g = Defs.declare g ("permF", prm alpha --> lam --> lam) val _ = print "define perm (1)" -val g = Defs.define g ("perm", prm alpha --> (beta --> gamma) --> (beta --> gamma)) "perm_fun" +val g = Defs.define g ("perm", prm alpha --> (beta --> gamma) --> (beta --> gamma)) "perm_fun" [("perm", prm alpha --> gamma --> gamma), ("perm", prm alpha --> beta --> beta)] val _ = print "define permF (1)" @@ -720,4 +743,4 @@ val g = Defs.define g ("perm", prm alpha --> lam --> lam) "perm_lam" [("permF", (prm alpha --> lam --> lam))] -*) \ No newline at end of file +*)