# HG changeset patch # User wenzelm # Date 1122916836 -7200 # Node ID 4600e74aeb0d43cff79826ed9f58df5417ea7dab # Parent 2ae3f621d0764f120ba91d206571ed4c17eb3d98 chain_history: turned into runtime flag; added monomorphic; removed (inefficient) fast_overloading_info; Compress.typ; tuned; diff -r 2ae3f621d076 -r 4600e74aeb0d src/Pure/defs.ML --- a/src/Pure/defs.ML Mon Aug 01 19:20:35 2005 +0200 +++ b/src/Pure/defs.ML Mon Aug 01 19:20:36 2005 +0200 @@ -2,33 +2,26 @@ 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", - Steven Obua, technical report, to be written :-) +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 + (*true: record the full chain of definitions that lead to a circularity*) + val chain_history: bool ref type graph 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 declare: theory -> string * typ -> graph -> graph + val define: theory -> string * typ -> string -> (string * typ) list -> graph -> graph + val finalize: theory -> string * typ -> graph -> graph val merge: Pretty.pp -> graph -> graph -> graph - - val finals : graph -> (typ list) Symtab.table - - (* 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 - is initialized with the Isabelle environment variable DEFS_CHAIN_HISTORY. *) - val set_chain_history : bool -> unit - val chain_history : unit -> bool - + val finals: graph -> typ list Symtab.table 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 + val overloading_info: graph -> string -> (typ * (string*typ) list * overloadingstate) option + val monomorphic: graph -> string -> bool end structure Defs :> DEFS = struct @@ -61,22 +54,14 @@ 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 - -type graph = int * (string Symtab.table) * (graphaction list) * (node Symtab.table) +datatype graphaction = + Declare of string * typ + | Define of string * typ * string * string * (string * typ) list + | Finalize of string * typ -val CHAIN_HISTORY = - let - 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") - end +type graph = int * string Symtab.table * graphaction list * node Symtab.table -fun set_chain_history b = CHAIN_HISTORY := b -fun chain_history () = !CHAIN_HISTORY +val chain_history = ref true val empty = (0, Symtab.empty, [], Symtab.empty) @@ -99,7 +84,7 @@ | checkT' (TVar ((a, 0), _)) = TVar ((a, 0), []) | checkT' (T as TVar _) = raise TYPE ("Illegal schematic type variable encountered", [T], []); -val checkT = Term.compress_type o checkT'; +fun checkT thy = Compress.typ thy o checkT'; fun rename ty1 ty2 = Logic.incr_tvar ((maxidx_of_typ ty1)+1) ty2; @@ -153,19 +138,8 @@ | 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 - | _ => true - end - -fun can_be_unified ty1 ty2 = - case unify ty1 ty2 of - NONE => false - | _ => true +fun can_be_unified_r ty1 ty2 = is_some (unify ty1 (rename ty1 ty2)) +fun can_be_unified ty1 ty2 = is_some (unify ty1 ty2) fun normalize_edge_idx (edge as (maxidx, u1, v1, history)) = if maxidx <= 1000000 then edge else @@ -244,7 +218,7 @@ def_err "constant is already declared with different type" end -fun declare'' g (name, ty) = declare' g (name, checkT ty) +fun declare'' thy g (name, ty) = declare' g (name, checkT thy ty) val axcounter = ref (IntInf.fromInt 0) fun newaxname axmap axname = @@ -330,7 +304,7 @@ NONE => NONE | SOME (max, sleft, sright) => SOME (max, subst sleft alpha1, subst sright beta2, - if !CHAIN_HISTORY then + if !chain_history then ((subst sleft beta1, bodyn, defname):: (subst_history sright history)) else []) @@ -492,16 +466,16 @@ (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'' thy (g as (cost, axmap, actions, graph)) (mainref, ty) orig_axname body = let - val ty = checkT ty + val ty = checkT thy ty fun checkbody (n, t) = let val (Node (_, _, _,_, closed)) = getnode graph n in case closed of Final => NONE - | _ => SOME (n, checkT t) + | _ => SOME (n, checkT thy t) end val body = distinct (List.mapPartial checkbody body) val (axmap, axname) = newaxname axmap orig_axname @@ -603,7 +577,7 @@ end end -fun finalize'' g (noderef, ty) = finalize' g (noderef, checkT ty) +fun finalize'' thy g (noderef, ty) = finalize' g (noderef, checkT thy ty) fun update_axname ax orig_ax (cost, axmap, history, graph) = (cost, Symtab.update ((ax, orig_ax), axmap), history, graph) @@ -640,15 +614,18 @@ SOME (ty, map translate (Symtab.dest defnodes), state) end -fun fast_overloading_info (_, _, _, graph) c = - let - fun count (c, _) = c+1 - in - case Symtab.lookup (graph, c) of - NONE => NONE - | SOME (Node (ty, defnodes, _, _, state)) => - SOME (ty, Symtab.foldl count (0, defnodes), state) - end + +(* monomorphic consts -- neither parametric nor ad-hoc polymorphism *) + +fun monomorphicT (Type (_, Ts)) = forall monomorphicT Ts + | monomorphicT _ = false + +fun monomorphic (_, _, _, graph) c = + (case Symtab.lookup (graph, c) of + NONE => true + | SOME (Node (ty, defnodes, _, _, _)) => + Symtab.min_key defnodes = Symtab.max_key defnodes andalso + monomorphicT ty); @@ -663,16 +640,12 @@ | 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.str "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.str "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; @@ -684,19 +657,19 @@ (* external interfaces *) -fun declare const defs = - if_none (try (declare'' defs) const) defs; +fun declare thy const defs = + if_none (try (declare'' thy defs) const) defs; -fun define pp const name rhs defs = - define'' defs const name rhs +fun define thy const name rhs defs = + define'' thy 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) + | CIRCULAR path => error (defs_circular (Sign.pp thy) path) + | INFINITE_CHAIN path => error (defs_infinite_chain (Sign.pp thy) path) | CLASH (_, def1, def2) => error (defs_clash def1 def2) - | FINAL const => error (defs_final pp const); + | FINAL const => error (defs_final (Sign.pp thy) const); -fun finalize const defs = - finalize'' defs const handle DEFS msg => sys_error msg; +fun finalize thy const defs = + finalize'' thy defs const handle DEFS msg => sys_error msg; fun merge pp defs1 defs2 = merge'' defs1 defs2