chain_history: turned into runtime flag;
authorwenzelm
Mon Aug 01 19:20:36 2005 +0200 (2005-08-01)
changeset 169824600e74aeb0d
parent 16981 2ae3f621d076
child 16983 c895701d55ea
chain_history: turned into runtime flag;
added monomorphic;
removed (inefficient) fast_overloading_info;
Compress.typ;
tuned;
src/Pure/defs.ML
     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.14 +with Overloading", Steven Obua, technical report, to be written :-)
    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.40    datatype overloadingstate = Open | Closed | Final
    1.41 -
    1.42 -  val overloading_info : graph -> string -> (typ * (string*typ) list * overloadingstate) option
    1.43 -  val fast_overloading_info : graph -> string -> (typ * int * overloadingstate) option
    1.44 +  val overloading_info: graph -> string -> (typ * (string*typ) list * overloadingstate) option
    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.160 -fun fast_overloading_info (_, _, _, graph) c =
   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