1.1 --- a/src/Tools/isac/Interpret/derive.sml	Thu Jul 28 11:43:27 2022 +0200
     1.2 +++ b/src/Tools/isac/Interpret/derive.sml	Sat Jul 30 16:47:45 2022 +0200
     1.3 @@ -14,9 +14,9 @@
     1.4    type step
     1.5    type derivation
     1.6  
     1.7 -  val do_one : theory -> Rule_Set.T -> Rule.rule list -> Rule_Def.rew_ord_ ->
     1.8 +  val do_one : Proof.context -> Rule_Set.T -> Rule.rule list -> Rule_Def.rew_ord_ ->
     1.9      term option -> term -> derivation
    1.10 -  val steps_reverse : theory -> Rule_Set.T -> Rule.rule list -> Rule_Def.rew_ord_ ->
    1.11 +  val steps_reverse : Proof.context -> Rule_Set.T -> Rule.rule list -> Rule_Def.rew_ord_ ->
    1.12      term option -> term -> rule_result list
    1.13    val steps : Rule_Def.rew_ord -> Rule_Set.T -> Rule.rule list -> term -> term ->
    1.14      bool * derivation
    1.15 @@ -50,17 +50,17 @@
    1.16  fun msg_1 rts =
    1.17    (tracing ("do_one exceeds " ^ int2str (! Rewrite.lim_deriv) ^ "with derivation =\n");
    1.18     tracing (deriv2str rts));
    1.19 -fun msg_2 thmid =
    1.20 -  if not (! Rewrite.trace_on) then () else tracing ("### trying thm \"" ^ thmid ^ "\"");
    1.21 -fun msg_3 t' =
    1.22 -  if ! Rewrite.trace_on then tracing ("=== rewrites to: " ^ UnparseC.term t') else ();
    1.23 -fun msg_4 op_ =
    1.24 -  if not (! Rewrite.trace_on) then () else tracing ("### trying calc. \"" ^ op_^"\"");
    1.25 -fun msg_5 t' =
    1.26 -  if not (! Rewrite.trace_on) then () else tracing("=== calc. to: " ^ UnparseC.term t')
    1.27 +fun msg_2 ctxt thmid =
    1.28 +  if not (Config.get ctxt rewrite_trace) then () else tracing ("### trying thm \"" ^ thmid ^ "\"");
    1.29 +fun msg_3 ctxt t' =
    1.30 +  if Config.get ctxt rewrite_trace then tracing ("=== rewrites to: " ^ UnparseC.term t') else ();
    1.31 +fun msg_4 ctxt op_ =
    1.32 +  if not (Config.get ctxt rewrite_trace) then () else tracing ("### trying calc. \"" ^ op_^"\"");
    1.33 +fun msg_5 ctxt t' =
    1.34 +  if not (Config.get ctxt rewrite_trace) then () else tracing("=== calc. to: " ^ UnparseC.term t')
    1.35  
    1.36  
    1.37 -fun do_one thy erls rs ro goal tt = 
    1.38 +fun do_one ctxt erls rs ro goal tt = 
    1.39    let 
    1.40      datatype switch = Appl | Noap (* TODO: unify with version in Rewrite *)
    1.41      fun rew_once _ rts t Noap [] = 
    1.42 @@ -77,26 +77,26 @@
    1.43        else
    1.44          (case r of
    1.45            Rule.Thm (thmid, tm) => 
    1.46 -            (msg_2 thmid;
    1.47 -            case Rewrite.rewrite_ thy ro erls true tm t of
    1.48 +            (msg_2 ctxt thmid;
    1.49 +            case Rewrite.rewrite_ ctxt ro erls true tm t of
    1.50                NONE => rew_once lim rts t apno rs'
    1.51              | SOME (t', a') =>
    1.52 -              (msg_3 t'; rew_once (lim - 1) (rts @ [(t, r, (t', a'))]) t' Appl rrs'))
    1.53 +              (msg_3 ctxt t'; rew_once (lim - 1) (rts @ [(t, r, (t', a'))]) t' Appl rrs'))
    1.54          | Rule.Eval (c as (op_, _)) => 
    1.55 -            (msg_4 op_;
    1.56 -            case Eval.adhoc_thm thy c t of
    1.57 +            (msg_4 ctxt op_;
    1.58 +            case Eval.adhoc_thm (Proof_Context.theory_of ctxt) c t of
    1.59                NONE => rew_once lim rts t apno rs'
    1.60              | SOME (thmid, tm) => 
    1.61                (let
    1.62 -                val (t', a') = case Rewrite.rewrite_ thy ro erls true tm t of
    1.63 +                val (t', a') = case Rewrite.rewrite_ ctxt ro erls true tm t of
    1.64                    SOME ta => ta
    1.65                  | NONE => raise ERROR "adhoc_thm: NONE"
    1.66 -                val _ = msg_5 t'
    1.67 +                val _ = msg_5 ctxt t'
    1.68                  val r' = Rule.Thm (thmid, tm)
    1.69                in rew_once (lim - 1) (rts @ [(t, r', (t', a'))]) t' Appl rrs' end) 
    1.70                  handle Rewrite.NO_REWRITE => raise ERROR "derive_norm, Eval: no rewrite")
    1.71          | Rule.Rls_ rls =>
    1.72 -          (case Rewrite.rewrite_set_ thy true rls t of
    1.73 +          (case Rewrite.rewrite_set_ ctxt true rls t of
    1.74              NONE => rew_once lim rts t apno rs'
    1.75            | SOME (t', a') => rew_once (lim - 1) (rts @ [(t, r, (t', a'))]) t' Appl rrs')
    1.76          | rule => raise ERROR ("rew_once: uncovered case " ^ Rule.to_string rule))
    1.77 @@ -121,8 +121,8 @@
    1.78      fun derivat ([]:(term * Rule.rule * (term * term list)) list) = TermC.empty
    1.79        | derivat dt = (#1 o #3 o last_elem) dt
    1.80      fun equal (_, _, (t1, _)) (_, _, (t2, _)) = t1 = t2
    1.81 -    val  fod = do_one (ThyC.Isac()) erls rules (snd rew_ord) NONE  fo
    1.82 -    val ifod = do_one (ThyC.Isac()) erls rules (snd rew_ord) NONE ifo
    1.83 +    val  fod = do_one (Proof_Context.init_global (ThyC.Isac())) erls rules (snd rew_ord) NONE  fo
    1.84 +    val ifod = do_one (Proof_Context.init_global (ThyC.Isac())) erls rules (snd rew_ord) NONE ifo
    1.85    in 
    1.86      case (fod, ifod) of
    1.87        ([], []) => if fo = ifo then (true, []) else (false, [])