1.1 --- a/TODO.md Sun Jul 31 13:45:20 2022 +0200
1.2 +++ b/TODO.md Sun Jul 31 16:35:33 2022 +0200
1.3 @@ -85,12 +85,15 @@
1.4 val rewrite_trace = Attrib.setup_config_bool \<^binding>\<open>rewrite_trace\<close> (K false);
1.5 \<close>
1.6
1.7 +* WN: Calculate.the: add structure Calculate
1.8 +
1.9 * WN: rewriting with ctxt not complete (cause errors hard to indentify later)
1.10 - Prconditions.eval
1.11 - Solve_Step.check ..Rewrite_Inst, Substitute, ..
1.12 - Error_Pattern.check_for', fill_form
1.13 - Derive.steps
1.14 - Fetch_Tacs.specific_from_prog ?
1.15 + - Eval.adhoc_thm, adhoc_thm1_
1.16 - ? LIST IS NOT COMPLETE
1.17
1.18 * WN: ? Rational.Cancel_p; extend use of \<^theory> to \<^theory_context>
2.1 --- a/src/Tools/isac/BaseDefinitions/eval-def.sml Sun Jul 31 13:45:20 2022 +0200
2.2 +++ b/src/Tools/isac/BaseDefinitions/eval-def.sml Sun Jul 31 16:35:33 2022 +0200
2.3 @@ -43,7 +43,7 @@
2.4 would be better
2.5 Eval: prog_calcID * (calID * eval_fn)) -> rule*)
2.6 type eval_fn = Rule_Def.eval_fn
2.7 -fun e_evalfn (_ : 'a) (_ : term) (_ : theory) = NONE : (string * term) option;
2.8 +fun e_evalfn (_ : 'a) (_ : term) (_ : Proof.context) = NONE : (string * term) option;
2.9
2.10
2.11 (* theory data for Isar command 'calculation' *)
3.1 --- a/src/Tools/isac/BaseDefinitions/rule-def.sml Sun Jul 31 13:45:20 2022 +0200
3.2 +++ b/src/Tools/isac/BaseDefinitions/rule-def.sml Sun Jul 31 16:35:33 2022 +0200
3.3 @@ -13,7 +13,7 @@
3.4 type rew_ord' = string
3.5 type rew_ord_ = LibraryC.subst -> term * term -> bool
3.6 type rew_ord = rew_ord' * rew_ord_
3.7 - type eval_fn = string -> term -> theory -> (string * term) option
3.8 + type eval_fn = string -> term -> Proof.context -> (string * term) option
3.9
3.10 datatype rule_set =
3.11 Empty
3.12 @@ -42,7 +42,7 @@
3.13 struct
3.14 (**)
3.15
3.16 -type eval_fn = string -> term -> theory -> (string * term) option;
3.17 +type eval_fn = string -> term -> Proof.context -> (string * term) option;
3.18
3.19 type rew_ord' = string;
3.20 type rew_ord_ = LibraryC.subst -> term * term -> bool;
4.1 --- a/src/Tools/isac/Knowledge/Integrate.thy Sun Jul 31 13:45:20 2022 +0200
4.2 +++ b/src/Tools/isac/Knowledge/Integrate.thy Sun Jul 31 16:35:33 2022 +0200
4.3 @@ -81,7 +81,7 @@
4.4 (*("add_new_c", ("Integrate.add_new_c", eval_add_new_c "#add_new_c_"))
4.5 add a new c to a term or a fun-equation;
4.6 this is _not in_ the term, because only applied to _whole_ term*)
4.7 -fun eval_add_new_c (_:string) "Integrate.add_new_c" p (_:theory) =
4.8 +fun eval_add_new_c (_:string) "Integrate.add_new_c" p (_:Proof.context) =
4.9 let val p' = case p of
4.10 Const (\<^const_name>\<open>HOL.eq\<close>, T) $ lh $ rh =>
4.11 Const (\<^const_name>\<open>HOL.eq\<close>, T) $ lh $ TermC.mk_add rh (new_c rh)
5.1 --- a/src/Tools/isac/Knowledge/Partial_Fractions.thy Sun Jul 31 13:45:20 2022 +0200
5.2 +++ b/src/Tools/isac/Knowledge/Partial_Fractions.thy Sun Jul 31 16:35:33 2022 +0200
5.3 @@ -59,9 +59,9 @@
5.4 eval_factors_from_solution ""))
5.5 this code is limited (max 3 solutions) AND has too little checks *)
5.6 fun eval_factors_from_solution (thmid:string) _
5.7 - (t as Const (\<^const_name>\<open>Partial_Fractions.factors_from_solution\<close>, _) $ sol) thy =
5.8 + (t as Const (\<^const_name>\<open>Partial_Fractions.factors_from_solution\<close>, _) $ sol) ctxt =
5.9 let val prod = factors_from_solution sol
5.10 - in SOME (TermC.mk_thmid thmid (UnparseC.term_in_thy thy prod) "",
5.11 + in SOME (TermC.mk_thmid thmid (UnparseC.term_in_ctxt ctxt prod) "",
5.12 HOLogic.Trueprop $ (TermC.mk_equality (t, prod)))
5.13 end
5.14 | eval_factors_from_solution _ _ _ _ = NONE;
6.1 --- a/src/Tools/isac/Knowledge/Poly.thy Sun Jul 31 13:45:20 2022 +0200
6.2 +++ b/src/Tools/isac/Knowledge/Poly.thy Sun Jul 31 16:35:33 2022 +0200
6.3 @@ -659,11 +659,11 @@
6.4
6.5 (*("is_polyexp", ("Poly.is_polyexp", eval_is_polyexp ""))*)
6.6 fun eval_is_polyexp (thmid:string) _
6.7 - (t as (Const (\<^const_name>\<open>is_polyexp\<close>, _) $ arg)) thy =
6.8 + (t as (Const (\<^const_name>\<open>is_polyexp\<close>, _) $ arg)) ctxt =
6.9 if is_polyexp arg
6.10 - then SOME (TermC.mk_thmid thmid (UnparseC.term_in_thy thy arg) "",
6.11 + then SOME (TermC.mk_thmid thmid (UnparseC.term_in_ctxt ctxt arg) "",
6.12 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
6.13 - else SOME (TermC.mk_thmid thmid (UnparseC.term_in_thy thy arg) "",
6.14 + else SOME (TermC.mk_thmid thmid (UnparseC.term_in_ctxt ctxt arg) "",
6.15 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
6.16 | eval_is_polyexp _ _ _ _ = NONE;
6.17 \<close>
6.18 @@ -673,20 +673,20 @@
6.19 (*WN.18.6.03 *)
6.20 (*("is_addUnordered", ("Poly.is_addUnordered", eval_is_addUnordered ""))*)
6.21 fun eval_is_addUnordered (thmid:string) _
6.22 - (t as (Const (\<^const_name>\<open>is_addUnordered\<close>, _) $ arg)) thy =
6.23 + (t as (Const (\<^const_name>\<open>is_addUnordered\<close>, _) $ arg)) ctxt =
6.24 if is_addUnordered arg
6.25 - then SOME (TermC.mk_thmid thmid (UnparseC.term_in_thy thy arg) "",
6.26 + then SOME (TermC.mk_thmid thmid (UnparseC.term_in_ctxt ctxt arg) "",
6.27 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
6.28 - else SOME (TermC.mk_thmid thmid (UnparseC.term_in_thy thy arg) "",
6.29 + else SOME (TermC.mk_thmid thmid (UnparseC.term_in_ctxt ctxt arg) "",
6.30 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
6.31 | eval_is_addUnordered _ _ _ _ = NONE;
6.32
6.33 fun eval_is_multUnordered (thmid:string) _
6.34 - (t as (Const (\<^const_name>\<open>is_multUnordered\<close>, _) $ arg)) thy =
6.35 + (t as (Const (\<^const_name>\<open>is_multUnordered\<close>, _) $ arg)) ctxt =
6.36 if is_multUnordered arg
6.37 - then SOME (TermC.mk_thmid thmid (UnparseC.term_in_thy thy arg) "",
6.38 + then SOME (TermC.mk_thmid thmid (UnparseC.term_in_ctxt ctxt arg) "",
6.39 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
6.40 - else SOME (TermC.mk_thmid thmid (UnparseC.term_in_thy thy arg) "",
6.41 + else SOME (TermC.mk_thmid thmid (UnparseC.term_in_ctxt ctxt arg) "",
6.42 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
6.43 | eval_is_multUnordered _ _ _ _ = NONE;
6.44 \<close>
7.1 --- a/src/Tools/isac/Knowledge/Rational.thy Sun Jul 31 13:45:20 2022 +0200
7.2 +++ b/src/Tools/isac/Knowledge/Rational.thy Sun Jul 31 16:35:33 2022 +0200
7.3 @@ -41,11 +41,11 @@
7.4
7.5 (*("is_ratpolyexp", ("Rational.is_ratpolyexp", eval_is_ratpolyexp ""))*)
7.6 fun eval_is_ratpolyexp (thmid:string) _
7.7 - (t as (Const (\<^const_name>\<open>Rational.is_ratpolyexp\<close>, _) $ arg)) thy =
7.8 + (t as (Const (\<^const_name>\<open>Rational.is_ratpolyexp\<close>, _) $ arg)) ctxt =
7.9 if is_ratpolyexp arg
7.10 - then SOME (TermC.mk_thmid thmid (UnparseC.term_in_thy thy arg) "",
7.11 + then SOME (TermC.mk_thmid thmid (UnparseC.term_in_ctxt ctxt arg) "",
7.12 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
7.13 - else SOME (TermC.mk_thmid thmid (UnparseC.term_in_thy thy arg) "",
7.14 + else SOME (TermC.mk_thmid thmid (UnparseC.term_in_ctxt ctxt arg) "",
7.15 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
7.16 | eval_is_ratpolyexp _ _ _ _ = NONE;
7.17
7.18 @@ -53,8 +53,8 @@
7.19 fun eval_get_denominator (thmid:string) _
7.20 (t as Const (\<^const_name>\<open>Rational.get_denominator\<close>, _) $
7.21 (Const (\<^const_name>\<open>divide\<close>, _) $ _(*num*) $
7.22 - denom)) thy =
7.23 - SOME (TermC.mk_thmid thmid (UnparseC.term_in_thy thy denom) "",
7.24 + denom)) ctxt =
7.25 + SOME (TermC.mk_thmid thmid (UnparseC.term_in_ctxt ctxt denom) "",
7.26 HOLogic.Trueprop $ (TermC.mk_equality (t, denom)))
7.27 | eval_get_denominator _ _ _ _ = NONE;
7.28
7.29 @@ -62,8 +62,8 @@
7.30 fun eval_get_numerator (thmid:string) _
7.31 (t as Const (\<^const_name>\<open>Rational.get_numerator\<close>, _) $
7.32 (Const (\<^const_name>\<open>divide\<close>, _) $num
7.33 - $denom )) thy =
7.34 - SOME (TermC.mk_thmid thmid (UnparseC.term_in_thy thy num) "",
7.35 + $denom )) ctxt =
7.36 + SOME (TermC.mk_thmid thmid (UnparseC.term_in_ctxt ctxt num) "",
7.37 HOLogic.Trueprop $ (TermC.mk_equality (t, num)))
7.38 | eval_get_numerator _ _ _ _ = NONE;
7.39 \<close>
7.40 @@ -454,11 +454,11 @@
7.41
7.42 (*("is_expanded", ("Rational.is_expanded", eval_is_expanded ""))*)
7.43 fun eval_is_expanded (thmid:string) _
7.44 - (t as (Const (\<^const_name>\<open>Rational.is_expanded\<close>, _) $ arg)) thy =
7.45 + (t as (Const (\<^const_name>\<open>Rational.is_expanded\<close>, _) $ arg)) ctxt =
7.46 if is_expanded arg
7.47 - then SOME (TermC.mk_thmid thmid (UnparseC.term_in_thy thy arg) "",
7.48 + then SOME (TermC.mk_thmid thmid (UnparseC.term_in_ctxt ctxt arg) "",
7.49 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
7.50 - else SOME (TermC.mk_thmid thmid (UnparseC.term_in_thy thy arg) "",
7.51 + else SOME (TermC.mk_thmid thmid (UnparseC.term_in_ctxt ctxt arg) "",
7.52 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
7.53 | eval_is_expanded _ _ _ _ = NONE;
7.54 \<close>
8.1 --- a/src/Tools/isac/Knowledge/Root.thy Sun Jul 31 13:45:20 2022 +0200
8.2 +++ b/src/Tools/isac/Knowledge/Root.thy Sun Jul 31 16:35:33 2022 +0200
8.3 @@ -44,7 +44,7 @@
8.4 ML \<open>
8.5 (*-------------------------functions---------------------*)
8.6 (*evaluation square-root over the integers*)
8.7 -fun eval_sqrt (_ : string) (_ : string) t (_: theory) =
8.8 +fun eval_sqrt (_ : string) (_ : string) t (_: Proof.context) =
8.9 (case t of
8.10 Const (op0, _) $ num =>
8.11 (case try HOLogic.dest_number num of
9.1 --- a/src/Tools/isac/Knowledge/Test.thy Sun Jul 31 13:45:20 2022 +0200
9.2 +++ b/src/Tools/isac/Knowledge/Test.thy Sun Jul 31 16:35:33 2022 +0200
9.3 @@ -253,23 +253,23 @@
9.4
9.5 (*does a term contain a root ?*)
9.6 fun eval_contains_root (thmid:string) _
9.7 - (t as (Const (\<^const_name>\<open>Test.contains_root\<close>, _) $ arg)) thy =
9.8 + (t as (Const (\<^const_name>\<open>Test.contains_root\<close>, _) $ arg)) ctxt =
9.9 if member op = (ids_of arg) "sqrt"
9.10 - then SOME (TermC.mk_thmid thmid (UnparseC.term_in_thy thy arg)"",
9.11 + then SOME (TermC.mk_thmid thmid (UnparseC.term_in_ctxt ctxt arg)"",
9.12 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
9.13 - else SOME (TermC.mk_thmid thmid (UnparseC.term_in_thy thy arg)"",
9.14 + else SOME (TermC.mk_thmid thmid (UnparseC.term_in_ctxt ctxt arg)"",
9.15 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
9.16 | eval_contains_root _ _ _ _ = NONE;
9.17
9.18 (*dummy precondition for root-met of x+1=2*)
9.19 -fun eval_precond_rootmet (thmid:string) _ (t as (Const (\<^const_name>\<open>Test.precond_rootmet\<close>, _) $ arg)) thy =
9.20 - SOME (TermC.mk_thmid thmid (UnparseC.term_in_thy thy arg)"",
9.21 +fun eval_precond_rootmet (thmid:string) _ (t as (Const (\<^const_name>\<open>Test.precond_rootmet\<close>, _) $ arg)) ctxt =
9.22 + SOME (TermC.mk_thmid thmid (UnparseC.term_in_ctxt ctxt arg)"",
9.23 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
9.24 | eval_precond_rootmet _ _ _ _ = NONE;
9.25
9.26 (*dummy precondition for root-pbl of x+1=2*)
9.27 -fun eval_precond_rootpbl (thmid:string) _ (t as (Const (\<^const_name>\<open>Test.precond_rootpbl\<close>, _) $ arg)) thy =
9.28 - SOME (TermC.mk_thmid thmid (UnparseC.term_in_thy thy arg) "",
9.29 +fun eval_precond_rootpbl (thmid:string) _ (t as (Const (\<^const_name>\<open>Test.precond_rootpbl\<close>, _) $ arg)) ctxt =
9.30 + SOME (TermC.mk_thmid thmid (UnparseC.term_in_ctxt ctxt arg) "",
9.31 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
9.32 | eval_precond_rootpbl _ _ _ _ = NONE;
9.33 \<close>
10.1 --- a/src/Tools/isac/ProgLang/Calculate.thy Sun Jul 31 13:45:20 2022 +0200
10.2 +++ b/src/Tools/isac/ProgLang/Calculate.thy Sun Jul 31 16:35:33 2022 +0200
10.3 @@ -29,22 +29,24 @@
10.4 val is_calcul_op =
10.5 member (op =) [\<^const_name>\<open>plus\<close>, \<^const_name>\<open>minus\<close>, \<^const_name>\<open>times\<close>, \<^const_name>\<open>realpow\<close>];
10.6
10.7 -fun calcul thy lhs =
10.8 +fun calcul ctxt lhs =
10.9 let
10.10 val simp_ctxt =
10.11 +(*
10.12 Proof_Context.init_global thy
10.13 - |> put_simpset (Simplifier.simpset_of @{theory_context BaseDefinitions});
10.14 - val eq = Simplifier.rewrite simp_ctxt (Thm.global_cterm_of thy lhs);
10.15 +*)
10.16 + ctxt |> put_simpset (Simplifier.simpset_of @{theory_context BaseDefinitions});
10.17 + val eq = Simplifier.rewrite simp_ctxt (Thm.cterm_of ctxt lhs);
10.18 val rhs = Thm.term_of (Thm.rhs_of eq);
10.19 in rhs end;
10.20
10.21 -fun eval_binop (_: string) (_: string) t thy =
10.22 +fun eval_binop (_: string) (_: string) t ctxt =
10.23 (case t of
10.24 (opp as Const (c1, T)) $ (Const (c2, _) $ v $ t1) $ t2 => (* binary \<circ> (v \<circ> n1) \<circ> n2 *)
10.25 if c1 = c2 andalso is_calcul_op c1 andalso is_num t1 andalso is_num t2 then
10.26 let
10.27 val opp' = Const (if c1 = \<^const_name>\<open>minus\<close> then \<^const_name>\<open>plus\<close> else c1, T);
10.28 - val res = calcul thy (opp' $ t1 $ t2);
10.29 + val res = calcul ctxt (opp' $ t1 $ t2);
10.30 val prop = HOLogic.Trueprop $ (HOLogic.mk_eq (t, opp $ v $ res));
10.31 in SOME ("#: " ^ UnparseC.term prop, prop) end
10.32 else NONE
10.33 @@ -53,7 +55,7 @@
10.34 andalso is_num t1 andalso is_num t2
10.35 then
10.36 let
10.37 - val res = calcul thy (opp $ t1 $ t2);
10.38 + val res = calcul ctxt (opp $ t1 $ t2);
10.39 val prop = HOLogic.Trueprop $ HOLogic.mk_eq (t, opp $ res $ v);
10.40 in
10.41 SOME ("#: " ^ UnparseC.term prop, prop)
10.42 @@ -62,7 +64,7 @@
10.43 | Const (c, _) $ t1 $ t2 => (* binary \<circ> n1 \<circ> n2 *)
10.44 if is_calcul_op c andalso is_num t1 andalso is_num t2 then
10.45 let
10.46 - val res = calcul thy t;
10.47 + val res = calcul ctxt t;
10.48 val prop = HOLogic.Trueprop $ (HOLogic.mk_eq (t, res));
10.49 in
10.50 SOME ("#: " ^ UnparseC.term prop, prop)
11.1 --- a/src/Tools/isac/ProgLang/Prog_Expr.thy Sun Jul 31 13:45:20 2022 +0200
11.2 +++ b/src/Tools/isac/ProgLang/Prog_Expr.thy Sun Jul 31 16:35:33 2022 +0200
11.3 @@ -45,11 +45,11 @@
11.4 signature PROG_EXPR =
11.5 sig
11.6 val eval_lhs: 'a -> string -> term -> 'b -> (string * term) option
11.7 - val eval_matches: string -> string -> term -> theory -> (string * term) option
11.8 + val eval_matches: string -> string -> term -> Proof.context -> (string * term) option
11.9 val matchsub: theory -> term -> term -> bool
11.10 - val eval_matchsub: string -> string -> term -> theory -> (string * term) option
11.11 + val eval_matchsub: string -> string -> term -> Proof.context -> (string * term) option
11.12 val eval_rhs: 'a -> string -> term -> 'b -> (string * term) option
11.13 - val eval_var: string -> string -> term -> theory -> (string * term) option
11.14 + val eval_var: string -> string -> term -> Proof.context -> (string * term) option
11.15
11.16 val or2list: term -> term
11.17
11.18 @@ -62,8 +62,8 @@
11.19 val even: int -> bool
11.20 val eval_is_even: string -> string -> term -> 'a -> (string * term) option
11.21 val eval_equ: string -> string -> term -> 'a -> (string * term) option
11.22 - val eval_ident: string -> string -> term -> theory -> (string * term) option
11.23 - val eval_equal: string -> string -> term -> theory -> (string * term) option
11.24 + val eval_ident: string -> string -> term -> Proof.context -> (string * term) option
11.25 + val eval_equal: string -> string -> term -> Proof.context -> (string * term) option
11.26 val eval_cancel: string -> string -> term -> 'a -> (string * term) option
11.27 val eval_argument_in: string -> string -> term -> 'a -> (string * term) option
11.28 val same_funid: term -> term -> bool
11.29 @@ -76,7 +76,7 @@
11.30 end
11.31
11.32 (**)
11.33 -structure Prog_Expr(**): PROG_EXPR =(**)
11.34 +structure Prog_Expr(**): PROG_EXPR(**) =
11.35 struct
11.36 (**)
11.37
11.38 @@ -98,16 +98,17 @@
11.39
11.40 (*. evaluate the predicate matches (match on whole term only) .*)
11.41 (*("matches",("Prog_Expr.matches", eval_matches "#matches_")):calc*)
11.42 -fun eval_matches (_:string) "Prog_Expr.matches" (t as Const (\<^const_name>\<open>Prog_Expr.matches\<close>, _) $ pat $ tst) thy =
11.43 - if TermC.matches thy tst pat
11.44 +fun eval_matches (_:string) "Prog_Expr.matches"
11.45 + (t as Const (\<^const_name>\<open>Prog_Expr.matches\<close>, _) $ pat $ tst) ctxt =
11.46 + if TermC.matches (Proof_Context.theory_of ctxt) tst pat
11.47 then
11.48 let
11.49 val prop = HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True}))
11.50 - in SOME (UnparseC.term_in_thy thy prop, prop) end
11.51 + in SOME (UnparseC.term_in_ctxt ctxt prop, prop) end
11.52 else
11.53 let
11.54 val prop = HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False}))
11.55 - in SOME (UnparseC.term_in_thy thy prop, prop) end
11.56 + in SOME (UnparseC.term_in_ctxt ctxt prop, prop) end
11.57 | eval_matches _ _ _ _ = NONE;
11.58
11.59 (*.does a pattern match some subterm ?.*)
11.60 @@ -126,22 +127,22 @@
11.61
11.62 (*("matchsub",("Prog_Expr.matchsub", eval_matchsub "#matchsub_")):calc*)
11.63 fun eval_matchsub (_:string) "Prog_Expr.matchsub"
11.64 - (t as Const (\<^const_name>\<open>Prog_Expr.matchsub\<close>, _) $ pat $ tst) thy =
11.65 - if matchsub thy tst pat
11.66 + (t as Const (\<^const_name>\<open>Prog_Expr.matchsub\<close>, _) $ pat $ tst) ctxt =
11.67 + if matchsub (Proof_Context.theory_of ctxt) tst pat
11.68 then
11.69 let val prop = HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True}))
11.70 - in SOME (UnparseC.term_in_thy thy prop, prop) end
11.71 + in SOME (UnparseC.term_in_ctxt ctxt prop, prop) end
11.72 else
11.73 let val prop = HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False}))
11.74 - in SOME (UnparseC.term_in_thy thy prop, prop) end
11.75 + in SOME (UnparseC.term_in_ctxt ctxt prop, prop) end
11.76 | eval_matchsub _ _ _ _ = NONE;
11.77
11.78 (*get the variables in an isabelle-term*)
11.79 (*("Vars" ,("Prog_Expr.Vars" , eval_var "#Vars_")):calc*)
11.80 -fun eval_var (thmid:string) "Prog_Expr.Vars" (t as (Const _ $ arg)) thy =
11.81 +fun eval_var (thmid:string) "Prog_Expr.Vars" (t as (Const _ $ arg)) ctxt =
11.82 let
11.83 val t' = ((TermC.list2isalist HOLogic.realT) o TermC.vars) t;
11.84 - val thmId = thmid ^ UnparseC.term_in_thy thy arg;
11.85 + val thmId = thmid ^ UnparseC.term_in_ctxt ctxt arg;
11.86 in SOME (thmId, HOLogic.Trueprop $ (TermC.mk_equality (t, t'))) end
11.87 | eval_var _ _ _ _ = NONE;
11.88
11.89 @@ -158,11 +159,9 @@
11.90 SOME (UnparseC.term t ^ " = " ^ UnparseC.term r,
11.91 HOLogic.Trueprop $ (TermC.mk_equality (t, r)))
11.92 | eval_rhs _ _ _ _ = NONE;
11.93 -(*\\------------------------- from Prog_Expr.thy-------------------------------------------------//*)
11.94
11.95 -(*//------------------------- from Atools.thy------------------------------------------------\\*)
11.96 +
11.97 fun occurs_in v t = member op = (((map strip_thy) o TermC.ids2str) t) (Term.term_name v);
11.98 -
11.99 (*("occurs_in", ("Prog_Expr.occurs_in", Prog_Expr.eval_occurs_in ""))*)
11.100 fun eval_occurs_in _ "Prog_Expr.occurs_in" (p as (Const (\<^const_name>\<open>occurs_in\<close>, _) $ v $ t)) _ =
11.101 ((*tracing("#>@ eval_occurs_in: v= "^(UnparseC.term v));
11.102 @@ -287,15 +286,15 @@
11.103 the arguments: thus special handling by 'fun eval_binop'*)
11.104 (*("ident" ,("Prog_Expr.ident", Prog_Expr.eval_ident "#ident_")):calc*)
11.105 fun eval_ident (thmid:string) "Prog_Expr.ident" (t as
11.106 - (Const _(*op0, t0*) $ t1 $ t2 )) thy =
11.107 + (Const _(*op0, t0*) $ t1 $ t2 )) ctxt =
11.108 if t1 = t2
11.109 then SOME (TermC.mk_thmid thmid
11.110 - ("(" ^ (UnparseC.term_in_thy thy t1) ^ ")")
11.111 - ("(" ^ (UnparseC.term_in_thy thy t2) ^ ")"),
11.112 + ("(" ^ (UnparseC.term_in_ctxt ctxt t1) ^ ")")
11.113 + ("(" ^ (UnparseC.term_in_ctxt ctxt t2) ^ ")"),
11.114 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
11.115 else SOME (TermC.mk_thmid thmid
11.116 - ("(" ^ (UnparseC.term_in_thy thy t1) ^ ")")
11.117 - ("(" ^ (UnparseC.term_in_thy thy t2) ^ ")"),
11.118 + ("(" ^ (UnparseC.term_in_ctxt ctxt t1) ^ ")")
11.119 + ("(" ^ (UnparseC.term_in_ctxt ctxt t2) ^ ")"),
11.120 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
11.121 | eval_ident _ _ _ _ = NONE;
11.122 (* TODO
11.123 @@ -320,11 +319,11 @@
11.124 (* evaluate identity of terms, which stay ready for further evaluation;
11.125 thus returns False only for atoms *)
11.126 (*("equal" ,(\<^const_name>\<open>HOL.eq\<close>, Prog_Expr.eval_equal "#equal_")):calc*)
11.127 -fun eval_equal (thmid : string) \<^const_name>\<open>HOL.eq\<close> (t as (Const _(*op0,t0*) $ t1 $ t2 )) thy =
11.128 +fun eval_equal (thmid : string) \<^const_name>\<open>HOL.eq\<close> (t as (Const _(*op0,t0*) $ t1 $ t2 )) ctxt =
11.129 if t1 = t2
11.130 then
11.131 SOME (TermC.mk_thmid thmid
11.132 - ("(" ^ UnparseC.term_in_thy thy t1 ^ ")") ("(" ^ UnparseC.term_in_thy thy t2 ^ ")"),
11.133 + ("(" ^ UnparseC.term_in_ctxt ctxt t1 ^ ")") ("(" ^ UnparseC.term_in_ctxt ctxt t2 ^ ")"),
11.134 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
11.135 else
11.136 (case (TermC.is_atom t1, TermC.is_atom t2) of
11.137 @@ -332,7 +331,7 @@
11.138 if TermC.variable_constant_pair (t1, t2)
11.139 then NONE
11.140 else SOME (TermC.mk_thmid thmid
11.141 - ("(" ^ UnparseC.term_in_thy thy t1 ^ ")") ("(" ^ UnparseC.term_in_thy thy t2 ^ ")"),
11.142 + ("(" ^ UnparseC.term_in_ctxt ctxt t1 ^ ")") ("(" ^ UnparseC.term_in_ctxt ctxt t2 ^ ")"),
11.143 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
11.144 | _ => NONE) (* NOT is_atom t1,t2 --> rew_sub *)
11.145 | eval_equal _ _ _ _ = NONE; (* error-exit *)
12.1 --- a/src/Tools/isac/ProgLang/evaluate.sml Sun Jul 31 13:45:20 2022 +0200
12.2 +++ b/src/Tools/isac/ProgLang/evaluate.sml Sun Jul 31 16:35:33 2022 +0200
12.3 @@ -18,10 +18,9 @@
12.4 val adhoc_thm1_: theory -> Eval_Def.cal -> term -> (string * thm) option
12.5 val norm: term -> term
12.6 val popt2str: ('a * term) option -> string
12.7 - val trace_on: bool Unsynchronized.ref
12.8 val int_of_numeral: term -> int
12.9 \<^isac_test>\<open>
12.10 - val get_pair: theory -> string -> Eval_Def.eval_fn -> term -> (string * term) option
12.11 + val get_pair: Proof.context -> string -> Eval_Def.eval_fn -> term -> (string * term) option
12.12 val mk_rule: term list * term * term -> term
12.13 val divisors: int -> int list
12.14 val doubles: int list -> int list
12.15 @@ -34,7 +33,7 @@
12.16 (**)
12.17
12.18 (* trace internal steps of isac's numeral calculations *)
12.19 -val trace_on = Unsynchronized.ref false;
12.20 +val eval_trace = Attrib.setup_config_bool \<^binding>\<open>eval_trace\<close> (K false);
12.21
12.22 (** calculate integers **)
12.23
12.24 @@ -98,71 +97,71 @@
12.25 fn : string -> string -> term -> theory -> (string * term) option
12.26 ^^^^^^... the selecting operator op_ (variable for eval_binop)
12.27 *)
12.28 -fun trace_calc0 str =
12.29 - if ! trace_on then writeln ("### " ^ str) else ()
12.30 -fun trace_calc1 str1 str2 =
12.31 - if ! trace_on then writeln (str1 ^ str2) else ()
12.32 -fun trace_calc2 str term popt =
12.33 - if ! trace_on then writeln (str ^ UnparseC.term term ^ " , " ^ popt2str popt) else ()
12.34 -fun trace_calc3 str term =
12.35 - if ! trace_on then writeln ("### " ^ str ^ UnparseC.term term) else ()
12.36 -fun trace_calc4 str t1 t2 =
12.37 - if ! trace_on then writeln ("### " ^ str ^ UnparseC.term t1 ^ " $ " ^ UnparseC.term t2) else ()
12.38 +fun trace_calc0 ctxt str =
12.39 + if Config.get ctxt eval_trace then writeln ("### " ^ str) else ()
12.40 +fun trace_calc1 ctxt str1 str2 =
12.41 + if Config.get ctxt eval_trace then writeln (str1 ^ str2) else ()
12.42 +fun trace_calc2 ctxt str term popt =
12.43 + if Config.get ctxt eval_trace then writeln (str ^ UnparseC.term term ^ " , " ^ popt2str popt) else ()
12.44 +fun trace_calc3 ctxt str term =
12.45 + if Config.get ctxt eval_trace then writeln ("### " ^ str ^ UnparseC.term term) else ()
12.46 +fun trace_calc4 ctxt str t1 t2 =
12.47 + if Config.get ctxt eval_trace then writeln ("### " ^ str ^ UnparseC.term t1 ^ " $ " ^ UnparseC.term t2) else ()
12.48
12.49 -fun get_pair (*1*)thy op_ (ef: Eval_Def.eval_fn) (t as (Const (op0, _) $ arg)) = (* unary fns *)
12.50 +fun get_pair (*1*)ctxt op_ (ef: Eval_Def.eval_fn) (t as (Const (op0, _) $ arg)) = (* unary fns *)
12.51 if op_ = op0 then
12.52 - let val popt = ef op_ t thy
12.53 - in case popt of SOME _ => popt | NONE => get_pair thy op_ ef arg end
12.54 - else get_pair thy op_ ef arg
12.55 - | get_pair (*2*)thy "Prog_Expr.ident" ef (t as (Const ("Prog_Expr.ident", _) $ _ $ _ )) =
12.56 - ef "Prog_Expr.ident" t thy (* not nested *)
12.57 - | get_pair (*3*)thy op_ ef (t as (Const (op0, _) $ t1 $ t2)) = (* binary funs *)
12.58 - (trace_calc1 "1.. get_pair: binop = " op_;
12.59 + let val popt = ef op_ t ctxt
12.60 + in case popt of SOME _ => popt | NONE => get_pair ctxt op_ ef arg end
12.61 + else get_pair ctxt op_ ef arg
12.62 + | get_pair (*2*)ctxt "Prog_Expr.ident" ef (t as (Const ("Prog_Expr.ident", _) $ _ $ _ )) =
12.63 + ef "Prog_Expr.ident" t ctxt (* not nested *)
12.64 + | get_pair (*3*)ctxt op_ ef (t as (Const (op0, _) $ t1 $ t2)) = (* binary funs *)
12.65 + (trace_calc1 ctxt "1.. get_pair: binop = " op_;
12.66 if op_ = op0 then
12.67 let
12.68 - val popt = ef op_ t thy
12.69 - val _ = trace_calc2 "2.. get_pair: " t popt
12.70 + val popt = ef op_ t ctxt
12.71 + val _ = trace_calc2 ctxt "2.. get_pair: " t popt
12.72 in case popt of SOME _ => popt | NONE =>
12.73 let
12.74 - val popt = get_pair thy op_ ef t1
12.75 - val _ = trace_calc2 "3.. get_pair: " t1 popt
12.76 - in case popt of SOME _ => popt | NONE => get_pair thy op_ ef t2 end (* search subterms *)
12.77 + val popt = get_pair ctxt op_ ef t1
12.78 + val _ = trace_calc2 ctxt "3.. get_pair: " t1 popt
12.79 + in case popt of SOME _ => popt | NONE => get_pair ctxt op_ ef t2 end (* search subterms *)
12.80 end
12.81 else (* search subterms *)
12.82 let
12.83 - val popt = get_pair thy op_ ef t1
12.84 - val _ = trace_calc2 "4.. get_pair: " t popt
12.85 - in case popt of SOME _ => popt | NONE => get_pair thy op_ ef t2 end)
12.86 - | get_pair (*4*)thy op_ ef (t as (Const (op0, _) $ t1 $ t2 $ t3)) = (* ternary funs *)
12.87 - (trace_calc3 "get_pair 4a: t= "t;
12.88 - trace_calc1 "get_pair 4a: op_= " op_;
12.89 - trace_calc1 "get_pair 4a: op0= " op0;
12.90 + val popt = get_pair ctxt op_ ef t1
12.91 + val _ = trace_calc2 ctxt "4.. get_pair: " t popt
12.92 + in case popt of SOME _ => popt | NONE => get_pair ctxt op_ ef t2 end)
12.93 + | get_pair (*4*)ctxt op_ ef (t as (Const (op0, _) $ t1 $ t2 $ t3)) = (* ternary funs *)
12.94 + (trace_calc3 ctxt "get_pair 4a: t= "t;
12.95 + trace_calc1 ctxt "get_pair 4a: op_= " op_;
12.96 + trace_calc1 ctxt "get_pair 4a: op0= " op0;
12.97 if op_ = op0 then
12.98 - case ef op_ t thy of st as SOME _ => st | NONE =>
12.99 - (case get_pair thy op_ ef t2 of st as SOME _ => st | NONE => get_pair thy op_ ef t3)
12.100 + case ef op_ t ctxt of st as SOME _ => st | NONE =>
12.101 + (case get_pair ctxt op_ ef t2 of st as SOME _ => st | NONE => get_pair ctxt op_ ef t3)
12.102 else
12.103 - (case get_pair thy op_ ef t1 of st as SOME _ => st | NONE =>
12.104 - (case get_pair thy op_ ef t2 of st as SOME _ => st | NONE => get_pair thy op_ ef t3)))
12.105 - | get_pair (*5*)thy op_ ef (Abs (_, _, body)) = get_pair thy op_ ef body
12.106 - | get_pair (*6*)thy op_ ef (t1 $ t2) =
12.107 + (case get_pair ctxt op_ ef t1 of st as SOME _ => st | NONE =>
12.108 + (case get_pair ctxt op_ ef t2 of st as SOME _ => st | NONE => get_pair ctxt op_ ef t3)))
12.109 + | get_pair (*5*)ctxt op_ ef (Abs (_, _, body)) = get_pair ctxt op_ ef body
12.110 + | get_pair (*6*)ctxt op_ ef (t1 $ t2) =
12.111 let
12.112 - val _ = trace_calc4 "5.. get_pair t1 $ t2: " t1 t2;
12.113 - val popt = get_pair thy op_ ef t1
12.114 + val _ = trace_calc4 ctxt "5.. get_pair t1 $ t2: " t1 t2;
12.115 + val popt = get_pair ctxt op_ ef t1
12.116 in case popt of SOME _ => popt
12.117 - | NONE => (trace_calc0 "### get_pair: t1 $ t2 -> NONE"; get_pair thy op_ ef t2)
12.118 + | NONE => (trace_calc0 ctxt "### get_pair: t1 $ t2 -> NONE"; get_pair ctxt op_ ef t2)
12.119 end
12.120 | get_pair (*7*)_ _ _ _ = NONE
12.121
12.122 (* get a thm from an op_ somewhere in a term by use of get_pair *)
12.123 fun adhoc_thm thy (op_, eval_fn) t =
12.124 ((*@{print\<open>tracing\<close>}{a = "adhoc_thm", op_ = op_, t = t, get_p = get_pair thy op_ eval_fn t};*)
12.125 - case get_pair thy op_ eval_fn t of
12.126 + case get_pair (Proof_Context.init_global thy) op_ eval_fn t of
12.127 NONE => NONE
12.128 | SOME (thmid, t') => SOME (thmid, Skip_Proof.make_thm thy t'));
12.129
12.130 (* get a thm applying an op_ to a term by direct use of eval_fn *)
12.131 fun adhoc_thm1_ thy (op_, eval_fn) ct =
12.132 - case eval_fn op_ ct thy of
12.133 + case eval_fn op_ ct (Proof_Context.init_global thy) of
12.134 NONE => NONE
12.135 | SOME (thmid, t') => SOME (thmid, Skip_Proof.make_thm thy t');
12.136
13.1 --- a/test/Tools/isac/BaseDefinitions/base-definitions.sml Sun Jul 31 13:45:20 2022 +0200
13.2 +++ b/test/Tools/isac/BaseDefinitions/base-definitions.sml Sun Jul 31 16:35:33 2022 +0200
13.3 @@ -17,7 +17,7 @@
13.4
13.5 (* these and other numeral calculations have been accomplished by Simplifier.rewrite so far *)
13.6
13.7 -val t = calcul @{theory} @{term "4 * - 1 * 4 ::real"};
13.8 +val t = calcul @{context} @{term "4 * - 1 * 4 ::real"};
13.9 if UnparseC.term_in_ctxt @{context} t = "- 16"
13.10 then () else error "calcul 4 * - 1 * 4 \<longrightarrow> - 16";
13.11
13.12 @@ -25,19 +25,19 @@
13.13 guess: simp_ctxt is not sufficient for simplifying the conditions in the definition -- RIGHT.
13.14 note: missing cases, defined in lemma realpow_uminus_simps, go via [simp] into simp_ctxt.
13.15 *)
13.16 -val t = calcul @{theory} @{term "4 \<up> 2 ::real"};
13.17 +val t = calcul @{context} @{term "4 \<up> 2 ::real"};
13.18 if UnparseC.term_in_ctxt @{context} t = "16"
13.19 then () else error "calcul 4 \<up> 2 \<longrightarrow> 16";
13.20
13.21 -val t = calcul @{theory} @{term "(- 1) \<up> 2"};
13.22 +val t = calcul @{context} @{term "(- 1) \<up> 2"};
13.23 if UnparseC.term_in_ctxt @{context} t = "1"
13.24 then () else error "calcul (- 1) \<up> 2 \<longrightarrow> 1";
13.25
13.26 -val t = calcul @{theory} @{term "3 \<up> (- 2)"};
13.27 +val t = calcul @{context} @{term "3 \<up> (- 2)"};
13.28 if UnparseC.term_in_ctxt @{context} t = "1 / 9"
13.29 then () else error "calcul 3 \<up> (- 2) \<longrightarrow> 1 / 9";
13.30
13.31 -val t = calcul @{theory} @{term "3 \<up> - 1"};
13.32 +val t = calcul @{context} @{term "3 \<up> - 1"};
13.33 if UnparseC.term_in_ctxt @{context} t = "1 / 3"
13.34 then () else error "calcul 3 \<up> - 1 \<longrightarrow> 1 / 3";
13.35
14.1 --- a/test/Tools/isac/Knowledge/integrate.sml Sun Jul 31 13:45:20 2022 +0200
14.2 +++ b/test/Tools/isac/Knowledge/integrate.sml Sun Jul 31 16:35:33 2022 +0200
14.3 @@ -97,7 +97,7 @@
14.4 val cc = new_c term;
14.5 if UnparseC.term cc = "c_3" then () else error "integrate.sml: new_c ???";
14.6
14.7 -val SOME (id,t') = eval_add_new_c "" "Integrate.add_new_c" term thy;
14.8 +val SOME (id,t') = eval_add_new_c "" "Integrate.add_new_c" term ctxt;
14.9 if UnparseC.term t' = "x \<up> 2 * c + c_2 = x \<up> 2 * c + c_2 + c_3" then ()
14.10 else error "intergrate.sml: diff. eval_add_new_c";
14.11
15.1 --- a/test/Tools/isac/Knowledge/polyminus.sml Sun Jul 31 13:45:20 2022 +0200
15.2 +++ b/test/Tools/isac/Knowledge/polyminus.sml Sun Jul 31 16:35:33 2022 +0200
15.3 @@ -666,7 +666,7 @@
15.4 "--- does the predicate evaluate correctly ?";
15.5 val t = TermC.str2term
15.6 "matchsub (?a * (?b - ?c)) (8 * (a - q) + a - 2 * q + 3 * (a - 2 * (q::real)))";
15.7 -val ma = eval_matchsub "" "Prog_Expr.matchsub" t thy;
15.8 +val ma = eval_matchsub "" "Prog_Expr.matchsub" t ctxt;
15.9 case ma of
15.10 SOME ("matchsub (?a * (?b - ?c)) (8 * (a - q) + \
15.11 \a - 2 * q + 3 * (a - 2 * q)) = True", _) => ()
16.1 --- a/test/Tools/isac/Knowledge/rational-2.sml Sun Jul 31 13:45:20 2022 +0200
16.2 +++ b/test/Tools/isac/Knowledge/rational-2.sml Sun Jul 31 16:35:33 2022 +0200
16.3 @@ -1602,7 +1602,7 @@
16.4 val thy = @{theory Isac_Knowledge};
16.5 val ctxt = Proof_Context.init_global thy;
16.6 val t = TermC.parseNEW' ctxt "get_denominator ((a +x)/b)";
16.7 -val SOME (_, t') = eval_get_denominator "" 0 t thy;
16.8 +val SOME (_, t') = eval_get_denominator "" 0 t ctxt;
16.9 if UnparseC.term t' = "get_denominator ((a + x) / b) = b"
16.10 then () else error "get_denominator ((a + x) / b) = b"
16.11
17.1 --- a/test/Tools/isac/MathEngBasic/rewrite.sml Sun Jul 31 13:45:20 2022 +0200
17.2 +++ b/test/Tools/isac/MathEngBasic/rewrite.sml Sun Jul 31 16:35:33 2022 +0200
17.3 @@ -374,7 +374,7 @@
17.4 if is_multUnordered t then () else error "rewrite.sml diff. is_multUnordered 2";
17.5 val tm = TermC.str2term "(x \<up> 2 * x) is_multUnordered";
17.6
17.7 -(*+*)case eval_is_multUnordered "testid" "" tm thy of
17.8 +(*+*)case eval_is_multUnordered "testid" "" tm ctxt of
17.9 (*+*) SOME
17.10 (*+*) ("testidx \<up> 2 * x_",
17.11 (*+*) Const (\<^const_name>\<open>Trueprop\<close>, _) $
17.12 @@ -387,9 +387,9 @@
17.13 (*+*)| _ => error "rewrite.sml diff. eval_is_multUnordered 2b CHANGED";
17.14
17.15
17.16 - eval_is_multUnordered "testid" "" tm thy;
17.17 + eval_is_multUnordered "testid" "" tm ctxt;
17.18
17.19 -case eval_is_multUnordered "testid" "" tm thy of
17.20 +case eval_is_multUnordered "testid" "" tm ctxt of
17.21 SOME (_, Const (\<^const_name>\<open>Trueprop\<close>, _) $
17.22 (Const (\<^const_name>\<open>HOL.eq\<close>, _) $
17.23 (Const (\<^const_name>\<open>is_multUnordered\<close>, _) $ _) $
18.1 --- a/test/Tools/isac/ProgLang/evaluate.sml Sun Jul 31 13:45:20 2022 +0200
18.2 +++ b/test/Tools/isac/ProgLang/evaluate.sml Sun Jul 31 16:35:33 2022 +0200
18.3 @@ -268,10 +268,10 @@
18.4 val op_ = \<^const_name>\<open>realpow\<close> : string
18.5 val eval_fn = fn : string -> term -> theory -> (string * term) option*)
18.6
18.7 - val SOME (thmid,t') = get_pair thy op_ eval_fn t;
18.8 + val SOME (thmid,t') = get_pair ctxt op_ eval_fn t;
18.9 (*** calc: operator = pow not defined*)
18.10
18.11 - val SOME (id,t') = eval_fn op_ t thy;
18.12 + val SOME (id,t') = eval_fn op_ t ctxt;
18.13 (*** calc: operator = pow not defined*)
18.14
18.15 case (op_, t) of
18.16 @@ -279,7 +279,7 @@
18.17 Const (\<^const_name>\<open>realpow\<close>, _) $ (Const (\<^const_name>\<open>numeral\<close>, _) $ (Const (\<^const_name>\<open>num.Bit1\<close>, _) $ Const (\<^const_name>\<open>num.One\<close>, _))) $
18.18 (Const (\<^const_name>\<open>numeral\<close>, _) $ (Const (\<^const_name>\<open>num.Bit0\<close>, _) $ Const (\<^const_name>\<open>num.One\<close>, _)))) => ()
18.19 | _ => error "3 \<up> 2 CHANGED";
18.20 - val SOME (id, t') = eval_binop thmid op_ t thy;
18.21 + val SOME (id, t') = eval_binop thmid op_ t ctxt;
18.22 (*** calc: operator = pow not defined*)
18.23
18.24 if UnparseC.term t' = "3 \<up> 2 = 9" then () else error "eval_binop 3 \<up> 2 = 9 CHANGED";
18.25 @@ -322,7 +322,7 @@
18.26 TermC.str2term
18.27 "[] from [c, c_2, c_3, c_4] occur_exactly_in - 1 * (q_0 * L \<up> 2) / 2"
18.28 );
18.29 -val SOME (str, simpl) = get_pair thy op_ ef arg;
18.30 +val SOME (str, simpl) = get_pair ctxt op_ ef arg;
18.31 if str =
18.32 "[] from [c, c_2, c_3, c_4] occur_exactly_in - 1 * (q_0 * L \<up> 2) / 2 = True"
18.33 then () else error "evaluate.sml get_pair with 3 args:occur_exactly_in";
18.34 @@ -349,36 +349,36 @@
18.35 if isa_str = "Groups.plus_class.plus" then () else error "eval_fn PLUS changed";
18.36
18.37 val t = @{term "3 + 4 :: real"};
18.38 -val SOME (str, term) = get_pair thy isa_str eval_fn t;
18.39 +val SOME (str, term) = get_pair ctxt isa_str eval_fn t;
18.40 (*+*)if str = "#: 3 + 4 = 7" andalso UnparseC.term term = "3 + 4 = 7"
18.41 (*+*)then () else error "get_pair 3 + 4 changed";
18.42
18.43 val t = @{term "(a + 3) + 4 :: real"};
18.44 -val SOME (str, term) = get_pair thy isa_str eval_fn t;
18.45 +val SOME (str, term) = get_pair ctxt isa_str eval_fn t;
18.46 if str = "#: a + 3 + 4 = a + 7" andalso UnparseC.term term = "a + 3 + 4 = a + 7"
18.47 then () else error "get_pair (a + 3) + 4 changed";
18.48
18.49 val t = @{term "(a + 3) + 4 :: real"};
18.50 -val SOME (str, term) = get_pair thy isa_str eval_fn t;
18.51 +val SOME (str, term) = get_pair ctxt isa_str eval_fn t;
18.52 if str = "#: a + 3 + 4 = a + 7" andalso UnparseC.term term = "a + 3 + 4 = a + 7"
18.53 then () else error "get_pair (a + 3) + 4 changed";
18.54
18.55 val t = @{term "x = 5 * (3 + (4 + a) :: real)"};
18.56 -val SOME (str, term) = get_pair thy isa_str eval_fn t;
18.57 +val SOME (str, term) = get_pair ctxt isa_str eval_fn t;
18.58 if str = "#: 3 + (4 + a) = 7 + a" andalso UnparseC.term term = "3 + (4 + a) = 7 + a"
18.59 then ((* !!! gets subterm !!!*)) else error "get_pair x = 5 * (3 + (4 + a)) (subterm) changed";
18.60
18.61 val SOME (isa_str, eval_fn) = LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "DIVIDE");
18.62
18.63 val t = @{term "-4 / - 2 :: real"};
18.64 -val SOME (str, term) = get_pair thy isa_str eval_fn t;
18.65 +val SOME (str, term) = get_pair ctxt isa_str eval_fn t;
18.66 if str = "#divide_e~4_~2" andalso UnparseC.term term = "- 4 / - 2 = 2"
18.67 then () else error "get_pair -4 / - 2 changed";
18.68
18.69 val SOME (isa_str, eval_fn) = LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "POWER");
18.70
18.71 val t = @{term "2 \<up> 3 :: real"};
18.72 -val SOME (str, term) = get_pair thy isa_str eval_fn t;
18.73 +val SOME (str, term) = get_pair ctxt isa_str eval_fn t;
18.74 if str = "#: 2 \<up> 3 = 8" andalso UnparseC.term term = "2 \<up> 3 = 8"
18.75 then () else error "get_pair 2 \<up> 3 changed";
18.76
18.77 @@ -452,7 +452,7 @@
18.78 "~~~~~ fun adhoc_thm , args:"; val (thy, (op_, eval_fn), t) = (@{theory}, eval_, t);
18.79 val SOME
18.80 ("#divide_e~1_2", t'') =
18.81 - (*case*) get_pair thy op_ eval_fn t (*of*);
18.82 + (*case*) get_pair ctxt op_ eval_fn t (*of*);
18.83 (*
18.84 get_pair finds two adjacent numerals and does NOT distinguish between different kinds of
18.85 \<^ML_type>\<open>eval_fn\<close>. In case of \<^ML>\<open>eval_cancel\<close> the return value WAS the same as the input..
18.86 @@ -463,7 +463,7 @@
18.87 val NONE = adhoc_thm @{theory} eval_ t;
18.88 "~~~~~ fun adhoc_thm , args:"; val (thy, (op_, eval_fn), t) = (@{theory}, eval_, t);
18.89 val NONE =
18.90 - (*case*) get_pair thy op_ eval_fn t (*of*);
18.91 + (*case*) get_pair ctxt op_ eval_fn t (*of*);
18.92
18.93
18.94 "----------- fun adhoc_thm \<longrightarrow> exception TYPE --------------------------------------------------";
18.95 @@ -474,10 +474,10 @@
18.96
18.97 "~~~~~ fun adhoc_thm , args:"; val (thy, (op_, eval_fn), ct) =
18.98 ((ThyC.get_theory "Isac_Knowledge"),
18.99 - ("NthRoot.sqrt", eval_sqrt "#sqrt_": string -> term -> theory -> (string * term) option), t);
18.100 + ("NthRoot.sqrt", eval_sqrt "#sqrt_": string -> term -> Proof.context -> (string * term) option), t);
18.101
18.102 val SOME (thmid, t) =
18.103 - (*case*) get_pair thy op_ eval_fn ct (*of*);
18.104 + (*case*) get_pair ctxt op_ eval_fn ct (*of*);
18.105 (*+*)val "sqrt 4 = 2" = UnparseC.term t;
18.106
18.107 (** )
19.1 --- a/test/Tools/isac/ProgLang/prog_expr.sml Sun Jul 31 13:45:20 2022 +0200
19.2 +++ b/test/Tools/isac/ProgLang/prog_expr.sml Sun Jul 31 16:35:33 2022 +0200
19.3 @@ -205,20 +205,20 @@
19.4 val ctxt = (ThyC.id_to_ctxt "Isac_Knowledge")
19.5
19.6 val t = TermC.str2term "x = 0";
19.7 -val NONE(*= indetermined*) = eval_equal "equal_" \<^const_name>\<open>HOL.eq\<close> t thy;
19.8 +val NONE(*= indetermined*) = eval_equal "equal_" \<^const_name>\<open>HOL.eq\<close> t ctxt;
19.9
19.10 val t = TermC.str2term "(x + 1) = (x + 1)";
19.11 val (Const _(*op0,t0*) $ t1 $ t2 ) = t
19.12 -val SOME ("equal_(x + 1)_(x + 1)", t') = eval_equal "equal_" \<^const_name>\<open>HOL.eq\<close> t thy;
19.13 +val SOME ("equal_(x + 1)_(x + 1)", t') = eval_equal "equal_" \<^const_name>\<open>HOL.eq\<close> t ctxt;
19.14 if UnparseC.term t' = "(x + 1 = x + 1) = True" then () else error "(x + 1) = (x + 1) CHANGED";
19.15
19.16 val t as Const _ $ v $ c = TermC.str2term "1 = 0";
19.17 val false = variable_constant_pair (v, c);
19.18 -val SOME ("equal_(1)_(0)", t') = eval_equal "equal_" \<^const_name>\<open>HOL.eq\<close> t thy;
19.19 +val SOME ("equal_(1)_(0)", t') = eval_equal "equal_" \<^const_name>\<open>HOL.eq\<close> t ctxt;
19.20 if UnparseC.term t' = "(1 = 0) = False" then () else error "1 = 0 CHANGED";
19.21
19.22 val t = TermC.str2term "0 = 0";
19.23 -val SOME ("equal_(0)_(0)", t') = eval_equal "equal_" \<^const_name>\<open>HOL.eq\<close> t thy;
19.24 +val SOME ("equal_(0)_(0)", t') = eval_equal "equal_" \<^const_name>\<open>HOL.eq\<close> t ctxt;
19.25 if UnparseC.term t' = "(0 = 0) = True" then () else error "0 = 0 CHANGED";
19.26
19.27
19.28 @@ -422,27 +422,27 @@
19.29 "-------- REBUILD fun eval_binop FOR Isabelle's NUMERALS ---------------------------------------";
19.30 val (op_, ef) = the (LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "TIMES"));
19.31 val t = TermC.parseNEW' ctxt "2 * (3::real)";
19.32 -(*val SOME (thmid,t') = *)get_pair thy op_ ef t;
19.33 +(*val SOME (thmid,t') = *)get_pair ctxt op_ ef t;
19.34 ;
19.35 "~~~~~ fun get_pair, args:"; val(*3*)(thy, op_, ef, (t as (Const (op0,_) $ t1 $ t2))) =
19.36 (thy, op_, ef, t);
19.37 (*if*) op_ = op0; (*then*)
19.38 val popt =
19.39 - ef op_ t thy;
19.40 + ef op_ t ctxt;
19.41 "~~~~~ fun eval_binop , args:"; val ((_ : string), (_: string),
19.42 (t as (Const (op0, _) $ t1 $ t2)), thy) =
19.43 ("#mult_", op_, t, thy);
19.44 val Const (c, _) $ t1 $ t2 = (* binary \<circ> n1 \<circ> n2 *)
19.45 (*case*) t (*of*);
19.46 (*if*) is_calcul_op c andalso is_num t1 andalso is_num t2 (*then*);
19.47 - val res = calcul thy t;
19.48 + val res = calcul ctxt t;
19.49 val prop = HOLogic.Trueprop $ (HOLogic.mk_eq (t, res));
19.50 SOME ("#: " ^ UnparseC.term prop, prop) (*return value*);
19.51 ;
19.52 if "#: " ^ UnparseC.term prop = "#: 2 * 3 = 6" andalso UnparseC.term prop = "2 * 3 = 6" then ()
19.53 else error "eval_binop changed"
19.54 ;
19.55 -val SOME (thmid, tm) = eval_binop "#mult_" op_ t thy;
19.56 +val SOME (thmid, tm) = eval_binop "#mult_" op_ t ctxt;
19.57 if thmid = "#: 2 * 3 = 6" andalso UnparseC.term prop = "2 * 3 = 6" then ()
19.58 else error "eval_binop changed 2"
19.59