src/Pure/unify.ML
changeset 24178 4ff1dc2aa18d
parent 23178 07ba6b58b3d2
child 26328 b2d6f520172c
     1.1 --- a/src/Pure/unify.ML	Tue Aug 07 20:19:54 2007 +0200
     1.2 +++ b/src/Pure/unify.ML	Tue Aug 07 20:19:55 2007 +0200
     1.3 @@ -12,10 +12,14 @@
     1.4  
     1.5  signature UNIFY =
     1.6  sig
     1.7 -  val trace_bound: int ref
     1.8 -  val trace_simp: bool ref
     1.9 -  val trace_types: bool ref
    1.10 -  val search_bound: int ref
    1.11 +  val trace_bound_value: Config.value Config.T
    1.12 +  val trace_bound: int Config.T
    1.13 +  val search_bound_value: Config.value Config.T
    1.14 +  val search_bound: int Config.T
    1.15 +  val trace_simp_value: Config.value Config.T
    1.16 +  val trace_simp: bool Config.T
    1.17 +  val trace_types_value: Config.value Config.T
    1.18 +  val trace_types: bool Config.T
    1.19    val unifiers: theory * Envir.env * ((term * term) list) ->
    1.20      (Envir.env * (term * term) list) Seq.seq
    1.21    val smash_unifiers: theory -> (term * term) list -> Envir.env -> Envir.env Seq.seq
    1.22 @@ -28,10 +32,22 @@
    1.23  
    1.24  (*Unification options*)
    1.25  
    1.26 -val trace_bound = ref 25  (*tracing starts above this depth, 0 for full*)
    1.27 -and search_bound = ref 30 (*unification quits above this depth*)
    1.28 -and trace_simp = ref false  (*print dpairs before calling SIMPL*)
    1.29 -and trace_types = ref false (*announce potential incompleteness of type unification*)
    1.30 +(*tracing starts above this depth, 0 for full*)
    1.31 +val trace_bound_value = Config.declare true "unify_trace_bound" (Config.Int 25);
    1.32 +val trace_bound = Config.int trace_bound_value;
    1.33 +
    1.34 +(*unification quits above this depth*)
    1.35 +val search_bound_value = Config.declare true "unify_search_bound" (Config.Int 30);
    1.36 +val search_bound = Config.int search_bound_value;
    1.37 +
    1.38 +(*print dpairs before calling SIMPL*)
    1.39 +val trace_simp_value = Config.declare true "unify_trace_simp" (Config.Bool false);
    1.40 +val trace_simp = Config.bool trace_simp_value;
    1.41 +
    1.42 +(*announce potential incompleteness of type unification*)
    1.43 +val trace_types_value = Config.declare true "unify_trace_types" (Config.Bool false);
    1.44 +val trace_types = Config.bool trace_types_value;
    1.45 +
    1.46  
    1.47  type binderlist = (string*typ) list;
    1.48  
    1.49 @@ -318,8 +334,10 @@
    1.50    NB "vname" is only used in the call to make_args!!   *)
    1.51  fun matchcopy thy vname = let fun mc(rbinder, targs, u, ed as (env,dpairs))
    1.52    : (term * (Envir.env * dpair list))Seq.seq =
    1.53 -let (*Produce copies of uarg and cons them in front of uargs*)
    1.54 -    fun copycons uarg (uargs, (env, dpairs)) =
    1.55 +let
    1.56 +  val trace_tps = Config.get_thy thy trace_types;
    1.57 +  (*Produce copies of uarg and cons them in front of uargs*)
    1.58 +  fun copycons uarg (uargs, (env, dpairs)) =
    1.59    Seq.map(fn (uarg', ed') => (uarg'::uargs, ed'))
    1.60        (mc (rbinder, targs,eta_norm env (rbinder, Envir.head_norm env uarg),
    1.61       (env, dpairs)));
    1.62 @@ -332,7 +350,7 @@
    1.63      (*attempt projection on argument with given typ*)
    1.64      val Ts = map (curry (fastype env) rbinder) targs;
    1.65      fun projenv (head, (Us,bary), targ, tail) =
    1.66 -  let val env = if !trace_types then test_unify_types thy (base,bary,env)
    1.67 +  let val env = if trace_tps then test_unify_types thy (base,bary,env)
    1.68            else unify_types thy (base,bary,env)
    1.69    in Seq.make (fn () =>
    1.70        let val (env',args) = make_args vname (Ts,env,Us);
    1.71 @@ -551,26 +569,30 @@
    1.72    SIMPL may raise exception CANTUNIFY. *)
    1.73  fun hounifiers (thy,env, tus : (term*term)list)
    1.74    : (Envir.env * (term*term)list)Seq.seq =
    1.75 -  let fun add_unify tdepth ((env,dpairs), reseq) =
    1.76 +  let
    1.77 +    val trace_bnd = Config.get_thy thy trace_bound;
    1.78 +    val search_bnd = Config.get_thy thy search_bound;
    1.79 +    val trace_smp = Config.get_thy thy trace_simp;
    1.80 +    fun add_unify tdepth ((env,dpairs), reseq) =
    1.81      Seq.make (fn()=>
    1.82      let val (env',flexflex,flexrigid) =
    1.83 -         (if tdepth> !trace_bound andalso !trace_simp
    1.84 +         (if tdepth> trace_bnd andalso trace_smp
    1.85      then print_dpairs thy "Enter SIMPL" (env,dpairs)  else ();
    1.86      SIMPL thy (env,dpairs))
    1.87      in case flexrigid of
    1.88          [] => SOME (List.foldr (add_ffpair thy) (env',[]) flexflex, reseq)
    1.89        | dp::frigid' =>
    1.90 -    if tdepth > !search_bound then
    1.91 +    if tdepth > search_bnd then
    1.92          (warning "Unification bound exceeded"; Seq.pull reseq)
    1.93      else
    1.94 -    (if tdepth > !trace_bound then
    1.95 +    (if tdepth > trace_bnd then
    1.96          print_dpairs thy "Enter MATCH" (env',flexrigid@flexflex)
    1.97       else ();
    1.98       Seq.pull (Seq.it_right (add_unify (tdepth+1))
    1.99           (MATCH thy (env',dp, frigid'@flexflex), reseq)))
   1.100      end
   1.101      handle CANTUNIFY =>
   1.102 -      (if tdepth > !trace_bound then tracing"Failure node" else ();
   1.103 +      (if tdepth > trace_bnd then tracing"Failure node" else ();
   1.104         Seq.pull reseq));
   1.105       val dps = map (fn(t,u)=> ([],t,u)) tus
   1.106    in add_unify 1 ((env, dps), Seq.empty) end;