1.1 --- a/src/Tools/isac/Interpret/derive.sml Mon May 04 10:19:16 2020 +0200
1.2 +++ b/src/Tools/isac/Interpret/derive.sml Mon May 04 11:13:16 2020 +0200
1.3 @@ -1,26 +1,25 @@
1.4 (* Title: Interpret/derive.sml
1.5 - Author: Walther Neuper 2019
1.6 + Author: Walther Neuper
1.7 (c) due to copyright terms
1.8
1.9 -Derive makes (term * rule * result) steps (= derivation) for term transformations,
1.10 -which cannot be done by rewriting, e.g cancellation of polynomials.
1.11 +Try to make (term * rule * result) steps (= derivation) by use of a Rule_Set.T.
1.12 +Two purposes:
1.13 +(1) derive steps from a given term towards another give term
1.14 +(2) term transformations, which cannot be done by rewriting, e.g cancellation of polynomials.
1.15 *)
1.16
1.17 signature DERIVE =
1.18 sig
1.19 - (*TODO cleanup signature*)
1.20 - type der
1.21 - type deri
1.22 + type rule_result
1.23 + type step
1.24 type derivation
1.25 -(*val make_deriv *)
1.26 +
1.27 val do_one : theory -> Rule_Set.T -> Rule.rule list -> Rule_Def.rew_ord_ ->
1.28 term option -> term -> derivation
1.29 -(*val reverse_deriv *)
1.30 val steps_reverse : theory -> Rule_Set.T -> Rule.rule list -> Rule_Def.rew_ord_ ->
1.31 - term option -> term -> deri list
1.32 -(*val concat_deriv *)
1.33 + term option -> term -> rule_result list
1.34 val steps : Rule_Def.rew_ord -> Rule_Set.T -> Rule.rule list -> term -> term ->
1.35 - bool * der list
1.36 + bool * derivation
1.37 val embed: State_Steps.T -> Calc.T -> Pos.pos' list * Calc.T
1.38 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
1.39 (* NONE *)
1.40 @@ -38,19 +37,16 @@
1.41
1.42 (** the triple for a step **)
1.43
1.44 -type der = (* derivation for inserting one level of nodes into the Ctree *)
1.45 - ( term * (* where the rule is applied to *)
1.46 - Rule.rule * (* rule to be applied *)
1.47 - ( term * (* resulting from rule application *)
1.48 - term list));(* assumptions resulting from rule application *)
1.49 -type deri = Rule.rule * (term * term list)
1.50 -type derivation = der list
1.51 +type rule_result = Rule.rule * Calc.result;
1.52 +type step = term * Rule.rule * Calc.result;
1.53 +type derivation = step list;
1.54
1.55 fun trta2str (t, r, (t', a)) =
1.56 "\n(" ^ UnparseC.term t ^ ", " ^ Rule.to_string_short r ^ ", (" ^ UnparseC.term t' ^ ", " ^ UnparseC.terms a ^ "))"
1.57 fun trtas2str trtas = (strs2str o (map trta2str)) trtas
1.58 val deriv2str = trtas2str
1.59
1.60 +
1.61 (** make one triple towards the goal term **)
1.62
1.63 fun msg_1 rts =
1.64 @@ -65,14 +61,14 @@
1.65 fun msg_5 t' =
1.66 if not (! Rewrite.trace_on) then () else tracing("=== calc. to: " ^ UnparseC.term t')
1.67
1.68 +
1.69 fun do_one thy erls rs ro goal tt =
1.70 let
1.71 datatype switch = Appl | Noap (* TODO: unify with version in Rewrite *)
1.72 fun rew_once _ rts t Noap [] =
1.73 (case goal of NONE => rts | SOME _ =>
1.74 - raise ERROR ("do_one: no derivation for " ^ UnparseC.term t))
1.75 + raise ERROR ("Derive.do_one: no derivation for " ^ UnparseC.term t))
1.76 | rew_once lim rts t Appl [] = rew_once lim rts t Noap rs
1.77 - (*| Seq _ => rts) FIXXXXXME 14.3.03*)
1.78 | rew_once lim rts t apno rs' =
1.79 (case goal of
1.80 NONE => rew_or_calc lim rts t apno rs'
1.81 @@ -142,8 +138,8 @@
1.82 else (false, [])
1.83 end
1.84
1.85 -(* embed the tacis created by a '_deriv'ation; sys.form <> input.form
1.86 - tacis are in order, thus are reverted for generate *)
1.87 +(** embed a derivation into the Ctree **)
1.88 +
1.89 fun embed tacis (pt, pos as (p, Pos.Frm)) =
1.90 (*inform at Frm: replace the whole PrfObj by a Transitive-ProfObj FIXME?0402
1.91 and transfer the istate (from _after_ compare_deriv) from Frm to Res*)
1.92 @@ -151,7 +147,7 @@
1.93 val (res, asm) = (State_Steps.result o last_elem) tacis
1.94 val (ist, ctxt) = case Ctree.get_obj Ctree.g_loc pt p of
1.95 (SOME (ist, ctxt), _) => (ist, ctxt)
1.96 - | (NONE, _) => error "Derive.embed Frm: uncovered case get_obj"
1.97 + | (NONE, _) => raise ERROR "Derive.embed Frm: uncovered case get_obj"
1.98 val form = Ctree.get_obj Ctree.g_form pt p
1.99 (*val p = lev_on p; ---------------only difference to (..,Res) below*)
1.100 val tacis = (Tactic.Begin_Trans, Tactic.Begin_Trans' form, (pos, (Istate_Def.Uistate, ctxt))) ::
1.101 @@ -169,7 +165,7 @@
1.102 val (res, asm) = (State_Steps.result o last_elem) tacis
1.103 val (ist, ctxt) = case Ctree.get_obj Ctree.g_loc pt p of
1.104 (_, SOME (ist, ctxt)) => (ist, ctxt)
1.105 - | (_, NONE) => error "Derive.embed Frm: uncovered case get_obj"
1.106 + | (_, NONE) => raise ERROR "Derive.embed Frm: uncovered case get_obj"
1.107 val (f, _) = Ctree.get_obj Ctree.g_result pt p
1.108 val p = Pos.lev_on p(*---------------only difference to (..,Frm) above*);
1.109 val tacis = (Tactic.Begin_Trans, Tactic.Begin_Trans' f, ((p, Pos.Frm), (Istate_Def.Uistate, ctxt))) ::
1.110 @@ -180,6 +176,6 @@
1.111 val pt = Ctree.update_tac pt p (Tactic.Derive (Rule_Set.id nrls))
1.112 val pt = Ctree.update_branch pt p Ctree.TransitiveB
1.113 in (c, (pt, pos)) end
1.114 - | embed _ _ = error "Derive.embed: uncovered definition"
1.115 + | embed _ _ = raise ERROR "Derive.embed: uncovered definition"
1.116
1.117 (**)end(**)
2.1 --- a/src/Tools/isac/Interpret/lucas-interpreter.sml Mon May 04 10:19:16 2020 +0200
2.2 +++ b/src/Tools/isac/Interpret/lucas-interpreter.sml Mon May 04 11:13:16 2020 +0200
2.3 @@ -611,11 +611,9 @@
2.4 (*
2.5 compare inform with ctree.form at current pos by nrls;
2.6 if found, embed the derivation generated during comparison
2.7 - if not, let the mat-engine compute the next ctree.form.
2.8 + if not, let the mat-engine compute the next Calc.result
2.9
2.10 - Code's structure is copied from complete_solve
2.11 - CAUTION: tacis in returned calcstate' do NOT construct resulting ptp --
2.12 - all_modspec etc. has to be inserted at Subproblem'
2.13 + TODO: find code in common with complete_solve
2.14 *)
2.15 fun compare_step (tacis, c, ptp as (pt, pos as (p, _))) ifo =
2.16 let
3.1 --- a/src/Tools/isac/MathEngBasic/calculation.sml Mon May 04 10:19:16 2020 +0200
3.2 +++ b/src/Tools/isac/MathEngBasic/calculation.sml Mon May 04 11:13:16 2020 +0200
3.3 @@ -6,6 +6,7 @@
3.4 signature CALCULATION =
3.5 sig
3.6 type T
3.7 + type result
3.8 val current_formula: T -> term
3.9
3.10 end
3.11 @@ -14,7 +15,8 @@
3.12 structure Calc(**): CALCULATION(**) =
3.13 struct
3.14 (**)
3.15 -type T = Ctree.state
3.16 +type T = Ctree.state;
3.17 +type result = (term * term list);
3.18
3.19 fun current_formula (pt, (p, p_)) =
3.20 case p_ of
4.1 --- a/src/Tools/isac/Specify/specify-step.sml Mon May 04 10:19:16 2020 +0200
4.2 +++ b/src/Tools/isac/Specify/specify-step.sml Mon May 04 11:13:16 2020 +0200
4.3 @@ -127,7 +127,7 @@
4.4 | add (Tactic.Specify_Method' (mID, oris, itms)) (_, ctxt) (pt, (p, _)) =
4.5 let
4.6 val pt = Ctree.update_oris pt p oris
4.7 - val pt = Ctree.update_met pt p itms
4.8 + val pt = Ctree.update_met pt p itms
4.9 val pt = Ctree.update_metID pt p mID
4.10 in
4.11 ((p, Pos.Met), [], Generate.PpcKF (Generate.Upblmet, Specify.itms2itemppc (Proof_Context.theory_of ctxt) [] []), pt)
5.1 --- a/src/Tools/isac/TODO.thy Mon May 04 10:19:16 2020 +0200
5.2 +++ b/src/Tools/isac/TODO.thy Mon May 04 11:13:16 2020 +0200
5.3 @@ -54,6 +54,9 @@
5.4 text \<open>
5.5 \begin{itemize}
5.6 \item xxx
5.7 + \item Derive.do_one: TODO find code in common with complete_solve
5.8 + Derive.embed: TODO rewrite according to CAO (+ no intermediate access to Ctree)
5.9 + \item xxx
5.10 \item Solve_Check: postponed parsing input to _ option
5.11 \item xxx
5.12 \item ? "fetch-tactics.sml" from Mathengine -> BridgeLibisabelle ?