author wenzelm Mon Aug 01 19:20:36 2005 +0200 (2005-08-01) changeset 16982 4600e74aeb0d parent 16981 2ae3f621d076 child 16983 c895701d55ea
chain_history: turned into runtime flag;
Compress.typ;
tuned;
 src/Pure/defs.ML file | annotate | diff | revisions
```     1.1 --- a/src/Pure/defs.ML	Mon Aug 01 19:20:35 2005 +0200
1.2 +++ b/src/Pure/defs.ML	Mon Aug 01 19:20:36 2005 +0200
1.3 @@ -2,33 +2,26 @@
1.4      ID:         \$Id\$
1.5      Author:     Steven Obua, TU Muenchen
1.6
1.7 -    Checks if definitions preserve consistency of logic by enforcing
1.8 -    that there are no cyclic definitions. The algorithm is described in
1.9 -    "An Algorithm for Determining Definitional Cycles in Higher-Order Logic with Overloading",
1.10 -    Steven Obua, technical report, to be written :-)
1.11 +Checks if definitions preserve consistency of logic by enforcing that
1.12 +there are no cyclic definitions. The algorithm is described in "An
1.13 +Algorithm for Determining Definitional Cycles in Higher-Order Logic
1.15  *)
1.16
1.17  signature DEFS =
1.18  sig
1.19 +  (*true: record the full chain of definitions that lead to a circularity*)
1.20 +  val chain_history: bool ref
1.21    type graph
1.22    val empty: graph
1.23 -  val declare: string * typ -> graph -> graph
1.24 -  val define: Pretty.pp -> string * typ -> string -> (string * typ) list -> graph -> graph
1.25 -  val finalize: string * typ -> graph -> graph
1.26 +  val declare: theory -> string * typ -> graph -> graph
1.27 +  val define: theory -> string * typ -> string -> (string * typ) list -> graph -> graph
1.28 +  val finalize: theory -> string * typ -> graph -> graph
1.29    val merge: Pretty.pp -> graph -> graph -> graph
1.30 -
1.31 -  val finals : graph -> (typ list) Symtab.table
1.32 -
1.33 -  (* If set to true then the exceptions CIRCULAR and INFINITE_CHAIN return the full
1.34 -     chain of definitions that lead to the exception. In the beginning, chain_history
1.35 -     is initialized with the Isabelle environment variable DEFS_CHAIN_HISTORY. *)
1.36 -  val set_chain_history : bool -> unit
1.37 -  val chain_history : unit -> bool
1.38 -
1.39 +  val finals: graph -> typ list Symtab.table
1.41 -
1.45 +  val monomorphic: graph -> string -> bool
1.46  end
1.47
1.48  structure Defs :> DEFS = struct
1.49 @@ -61,22 +54,14 @@
1.50
1.51  fun table_size table = Symtab.foldl (fn (x, _) => x+1) (0, table)
1.52
1.53 -datatype graphaction = Declare of string * typ
1.54 -                     | Define of string * typ * string * string * (string * typ) list
1.55 -                     | Finalize of string * typ
1.56 -
1.57 -type graph = int * (string Symtab.table) * (graphaction list) * (node Symtab.table)
1.58 +datatype graphaction =
1.59 +    Declare of string * typ
1.60 +  | Define of string * typ * string * string * (string * typ) list
1.61 +  | Finalize of string * typ
1.62
1.63 -val CHAIN_HISTORY =
1.64 -    let
1.65 -      fun f c = if Char.isSpace c then "" else String.str (Char.toUpper c)
1.66 -      val env = String.translate f (getenv "DEFS_CHAIN_HISTORY")
1.67 -    in
1.68 -      ref (env = "ON" orelse env = "TRUE")
1.69 -    end
1.70 +type graph = int * string Symtab.table * graphaction list * node Symtab.table
1.71
1.72 -fun set_chain_history b = CHAIN_HISTORY := b
1.73 -fun chain_history () = !CHAIN_HISTORY
1.74 +val chain_history = ref true
1.75
1.76  val empty = (0, Symtab.empty, [], Symtab.empty)
1.77
1.78 @@ -99,7 +84,7 @@
1.79    | checkT' (TVar ((a, 0), _)) = TVar ((a, 0), [])
1.80    | checkT' (T as TVar _) = raise TYPE ("Illegal schematic type variable encountered", [T], []);
1.81
1.82 -val checkT = Term.compress_type o checkT';
1.83 +fun checkT thy = Compress.typ thy o checkT';
1.84
1.85  fun rename ty1 ty2 = Logic.incr_tvar ((maxidx_of_typ ty1)+1) ty2;
1.86
1.87 @@ -153,19 +138,8 @@
1.88        | SOME s => SOME (max, merge s1 s, merge s2 s)
1.89      end
1.90
1.91 -fun can_be_unified_r ty1 ty2 =
1.92 -    let
1.93 -      val ty2 = rename ty1 ty2
1.94 -    in
1.95 -      case unify ty1 ty2 of
1.96 -        NONE => false
1.97 -      | _ => true
1.98 -    end
1.99 -
1.100 -fun can_be_unified ty1 ty2 =
1.101 -    case unify ty1 ty2 of
1.102 -      NONE => false
1.103 -    | _ => true
1.104 +fun can_be_unified_r ty1 ty2 = is_some (unify ty1 (rename ty1 ty2))
1.105 +fun can_be_unified ty1 ty2 = is_some (unify ty1 ty2)
1.106
1.107  fun normalize_edge_idx (edge as (maxidx, u1, v1, history)) =
1.108      if maxidx <= 1000000 then edge else
1.109 @@ -244,7 +218,7 @@
1.110                 def_err "constant is already declared with different type"
1.111             end
1.112
1.113 -fun declare'' g (name, ty) = declare' g (name, checkT ty)
1.114 +fun declare'' thy g (name, ty) = declare' g (name, checkT thy ty)
1.115
1.116  val axcounter = ref (IntInf.fromInt 0)
1.117  fun newaxname axmap axname =
1.118 @@ -330,7 +304,7 @@
1.119                                NONE => NONE
1.120                              | SOME (max, sleft, sright) =>
1.121                                SOME (max, subst sleft alpha1, subst sright beta2,
1.122 -                                    if !CHAIN_HISTORY then
1.123 +                                    if !chain_history then
1.124                                        ((subst sleft beta1, bodyn, defname)::
1.125                                         (subst_history sright history))
1.126                                      else [])
1.127 @@ -492,16 +466,16 @@
1.128        (cost+3, axmap, actions', graph)
1.129      end handle ex => translate_ex axmap ex
1.130
1.131 -fun define'' (g as (cost, axmap, actions, graph)) (mainref, ty) orig_axname body =
1.132 +fun define'' thy (g as (cost, axmap, actions, graph)) (mainref, ty) orig_axname body =
1.133      let
1.134 -      val ty = checkT ty
1.135 +      val ty = checkT thy ty
1.136        fun checkbody (n, t) =
1.137            let
1.138              val (Node (_, _, _,_, closed)) = getnode graph n
1.139            in
1.140              case closed of
1.141                Final => NONE
1.142 -            | _ => SOME (n, checkT t)
1.143 +            | _ => SOME (n, checkT thy t)
1.144            end
1.145        val body = distinct (List.mapPartial checkbody body)
1.146        val (axmap, axname) = newaxname axmap orig_axname
1.147 @@ -603,7 +577,7 @@
1.148            end
1.149        end
1.150
1.151 -fun finalize'' g (noderef, ty) = finalize' g (noderef, checkT ty)
1.152 +fun finalize'' thy g (noderef, ty) = finalize' g (noderef, checkT thy ty)
1.153
1.154  fun update_axname ax orig_ax (cost, axmap, history, graph) =
1.155    (cost, Symtab.update ((ax, orig_ax), axmap), history, graph)
1.156 @@ -640,15 +614,18 @@
1.157          SOME (ty, map translate (Symtab.dest defnodes), state)
1.158      end
1.159
1.161 -    let
1.162 -      fun count (c, _) = c+1
1.163 -    in
1.164 -      case Symtab.lookup (graph, c) of
1.165 -        NONE => NONE
1.166 -      | SOME (Node (ty, defnodes, _, _, state)) =>
1.167 -        SOME (ty, Symtab.foldl count (0, defnodes), state)
1.168 -    end
1.169 +
1.170 +(* monomorphic consts -- neither parametric nor ad-hoc polymorphism *)
1.171 +
1.172 +fun monomorphicT (Type (_, Ts)) = forall monomorphicT Ts
1.173 +  | monomorphicT _ = false
1.174 +
1.175 +fun monomorphic (_, _, _, graph) c =
1.176 +  (case Symtab.lookup (graph, c) of
1.177 +    NONE => true
1.178 +  | SOME (Node (ty, defnodes, _, _, _)) =>
1.179 +      Symtab.min_key defnodes = Symtab.max_key defnodes andalso
1.180 +      monomorphicT ty);
1.181
1.182
1.183
1.184 @@ -663,16 +640,12 @@
1.185     | prts => Pretty.block (pretty_const pp (c, T) @
1.186        [Pretty.brk 1, Pretty.str ("depends via " ^ quote def ^ " on")]) :: prts) path [];
1.187
1.188 -fun chain_history_msg s =    (* FIXME huh!? *)
1.189 -  if chain_history () then s ^ ": "
1.190 -  else s ^ " (set DEFS_CHAIN_HISTORY=ON for full history): ";
1.191 -
1.192  fun defs_circular pp path =
1.193 -  Pretty.str (chain_history_msg "Cyclic dependency of definitions") :: pretty_path pp path
1.194 +  Pretty.str "Cyclic dependency of definitions: " :: pretty_path pp path
1.195    |> Pretty.chunks |> Pretty.string_of;
1.196
1.197  fun defs_infinite_chain pp path =
1.198 -  Pretty.str (chain_history_msg "Infinite chain of definitions") :: pretty_path pp path
1.199 +  Pretty.str "Infinite chain of definitions: " :: pretty_path pp path
1.200    |> Pretty.chunks |> Pretty.string_of;
1.201
1.202  fun defs_clash def1 def2 = "Type clash in definitions " ^ quote def1 ^ " and " ^ quote def2;
1.203 @@ -684,19 +657,19 @@
1.204
1.205  (* external interfaces *)
1.206
1.207 -fun declare const defs =
1.208 -  if_none (try (declare'' defs) const) defs;
1.209 +fun declare thy const defs =
1.210 +  if_none (try (declare'' thy defs) const) defs;
1.211
1.212 -fun define pp const name rhs defs =
1.213 -  define'' defs const name rhs
1.214 +fun define thy const name rhs defs =
1.215 +  define'' thy defs const name rhs
1.216      handle DEFS msg => sys_error msg
1.217 -      | CIRCULAR path => error (defs_circular pp path)
1.218 -      | INFINITE_CHAIN path => error (defs_infinite_chain pp path)
1.219 +      | CIRCULAR path => error (defs_circular (Sign.pp thy) path)
1.220 +      | INFINITE_CHAIN path => error (defs_infinite_chain (Sign.pp thy) path)
1.221        | CLASH (_, def1, def2) => error (defs_clash def1 def2)
1.222 -      | FINAL const => error (defs_final pp const);
1.223 +      | FINAL const => error (defs_final (Sign.pp thy) const);
1.224
1.225 -fun finalize const defs =
1.226 -  finalize'' defs const handle DEFS msg => sys_error msg;
1.227 +fun finalize thy const defs =
1.228 +  finalize'' thy defs const handle DEFS msg => sys_error msg;
1.229
1.230  fun merge pp defs1 defs2 =
1.231    merge'' defs1 defs2
```