diff -r 7dd0eb6e89f9 -r 90c51c932154 src/Pure/defs.ML --- a/src/Pure/defs.ML Mon Jun 13 15:10:52 2005 +0200 +++ b/src/Pure/defs.ML Mon Jun 13 21:28:57 2005 +0200 @@ -71,7 +71,7 @@ | Define of string * typ * string * (string * typ) list | Finalize of string * typ -type graph = int * (graphaction list) * (node Symtab.table) +type graph = int * (string Symtab.table) * (graphaction list) * (node Symtab.table) val CHAIN_HISTORY = let @@ -84,7 +84,7 @@ fun set_chain_history b = CHAIN_HISTORY := b fun chain_history () = !CHAIN_HISTORY -val empty = (0, [], Symtab.empty) +val empty = (0, Symtab.empty, [], Symtab.empty) exception DEFS of string; exception CIRCULAR of (typ * string * string) list; @@ -100,10 +100,30 @@ 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), []) +exception No_Change; + +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 + +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; @@ -237,8 +257,8 @@ 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, +fun declare' (g as (cost, axmap, actions, graph)) (cty as (name, ty)) = + (cost, axmap, (Declare cty)::actions, Symtab.update_new ((name, Node (ty, Symtab.empty, Symtab.empty, [], Open)), graph)) handle Symtab.DUP _ => let @@ -252,7 +272,28 @@ fun declare g (name, ty) = declare' g (name, checkT ty) -fun define' (cost, actions, graph) (mainref, ty) axname body = +val axcounter = ref (IntInf.fromInt 0) +fun newaxname axmap axname = + let + val c = !axcounter + val _ = axcounter := c+1 + val axname' = axname^"_"^(IntInf.toString c) + in + (Symtab.update ((axname', axname), axmap), axname') + end + +fun translate_ex axmap x = + let + fun translate (ty, nodename, axname) = + (ty, nodename, the (Symtab.lookup (axmap, axname))) + in + case x of + INFINITE_CHAIN chain => raise (INFINITE_CHAIN (map translate chain)) + | CIRCULAR cycle => raise (CIRCULAR (map translate cycle)) + | _ => raise x + end + +fun define' (cost, axmap, actions, graph) (mainref, ty) axname body = let val mainnode = (case Symtab.lookup (graph, mainref) of NONE => def_err ("constant "^mainref^" is not declared") @@ -474,10 +515,10 @@ val graph = Symtab.update ((mainref, Node (gty, defs, backs, finals, closed)), graph) val actions' = (Define (mainref, ty, axname, body))::actions in - (cost+3,actions', graph) - end + (cost+3, axmap, actions', graph) + end handle ex => translate_ex axmap ex -fun define (g as (_, _, graph)) (mainref, ty) axname body = +fun define (g as (cost, axmap, actions, graph)) (mainref, ty) axname body = let val ty = checkT ty fun checkbody (n, t) = @@ -489,11 +530,12 @@ | _ => SOME (n, checkT t) end val body = distinct (List.mapPartial checkbody body) + val (axmap, axname) = newaxname axmap axname in - define' g (mainref, ty) axname body + define' (cost, axmap, actions, graph) (mainref, ty) axname body end -fun finalize' (cost, history, graph) (noderef, ty) = +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)) => @@ -525,7 +567,7 @@ SOME (final_ty :: finals)) in case update_finals finals of - NONE => (cost, history, graph) + NONE => (cost, axmap, history, graph) | SOME finals => let val closed = if closed = Open andalso is_instance_r nodety ty then @@ -583,14 +625,14 @@ finals, closed)), graph') val history' = (Finalize (noderef, ty)) :: history in - (cost+1, history', graph') + (cost+1, axmap, history', graph') end end fun finalize g (noderef, ty) = finalize' g (noderef, checkT ty) fun merge' (Declare cty, g) = declare' g cty - | merge' (Define (name, ty, axname, body), g as (_,_, graph)) = + | 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, _, _, _)) => @@ -599,13 +641,13 @@ | SOME _ => g)) | merge' (Finalize finals, g) = finalize' g finals -fun merge (g1 as (cost1, actions1, _)) (g2 as (cost2, actions2, _)) = +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 (cost, history, graph) = +fun finals (_, _, history, graph) = Symtab.foldl (fn (finals, (name, Node(_, _, _, ftys, _))) => Symtab.update_new ((name, ftys), finals))