1.1 --- a/src/Tools/isac/BridgeLibisabelle/interface.sml Tue Mar 31 14:05:10 2020 +0200
1.2 +++ b/src/Tools/isac/BridgeLibisabelle/interface.sml Tue Mar 31 15:43:33 2020 +0200
1.3 @@ -225,7 +225,7 @@
1.4 fun getAccumulatedAsms cI (p:pos') =
1.5 (let
1.6 val ((pt, _), _) = get_calc cI
1.7 - val ass = get_assumptions_ pt p
1.8 + val ass = Ctree.get_assumptions pt p
1.9 in getasmsOK2xml cI ass end)
1.10 handle _ => sysERROR2xml cI "syserror in getAccumulatedAsms"
1.11
2.1 --- a/src/Tools/isac/Interpret/error-pattern.sml Tue Mar 31 14:05:10 2020 +0200
2.2 +++ b/src/Tools/isac/Interpret/error-pattern.sml Tue Mar 31 15:43:33 2020 +0200
2.3 @@ -12,7 +12,7 @@
2.4 Rule.rls -> Rule.rule list -> term -> term -> bool * (term * Rule.rule * (term * term list)) list
2.5 val mk_tacis: Rule.rew_ord' * 'a -> Rule.rls -> term * Rule.rule * (term * term list) -> Tactic.input * Tactic.T * (Ctree.pos' * (Istate.T * Proof.context))
2.6 val fetchErrorpatterns : Tactic.input -> Rule.errpatID list
2.7 - val check_error_patterns :
2.8 + val check_for :
2.9 term * term ->
2.10 term * (term * term) list -> (Rule.errpatID * term list * 'a list) list * Rule.rls -> Rule.errpatID option
2.11 val rule2thm'' : Rule.rule -> Celem.thm''
2.12 @@ -117,7 +117,7 @@
2.13
2.14 (* check if (agreed result, input formula) matches SOME error pattern modulo simplifier rls;
2.15 (prog, env) for retrieval of casual substitution for bdv in the pattern. *)
2.16 -fun check_error_patterns (res, inf) (prog, env) (errpats, rls) =
2.17 +fun check_for (res, inf) (prog, env) (errpats, rls) =
2.18 let
2.19 val (_, subst) = Rtools.get_bdv_subst prog env
2.20 fun scan (_, [], _) = NONE
3.1 --- a/src/Tools/isac/Interpret/istate.sml Tue Mar 31 14:05:10 2020 +0200
3.2 +++ b/src/Tools/isac/Interpret/istate.sml Tue Mar 31 15:43:33 2020 +0200
3.3 @@ -13,8 +13,8 @@
3.4
3.5 datatype T = datatype Istate_Def.T
3.6 val e_istate: T
3.7 - val istate2str: T -> string
3.8 - val istate2str': T -> string
3.9 + val string_of: T -> string
3.10 + val string_of': T -> string
3.11 val istates2str: T option * T option -> string
3.12 val the_pstate: T -> pstate
3.13
3.14 @@ -74,8 +74,8 @@
3.15 fun the_pstate (Pstate pst) = pst
3.16 | the_pstate _ = raise ERROR ("the_pstate called for RrlsStated")
3.17
3.18 -val istate2str = Istate_Def.istate2str
3.19 -val istate2str' = Istate_Def.istate2str'
3.20 +val string_of = Istate_Def.string_of
3.21 +val string_of' = Istate_Def.string_of'
3.22 val istates2str = Istate_Def.istates2str
3.23
3.24 fun get_act_env {env, act_arg, ...} = (act_arg, env)
4.1 --- a/src/Tools/isac/Interpret/li-tool.sml Tue Mar 31 14:05:10 2020 +0200
4.2 +++ b/src/Tools/isac/Interpret/li-tool.sml Tue Mar 31 15:43:33 2020 +0200
4.3 @@ -6,9 +6,9 @@
4.4 signature LUCAS_INTERPRETER_TOOL =
4.5 sig
4.6 datatype ass =
4.7 - Ass of Tactic.T * term * Proof.context
4.8 + Associated of Tactic.T * term * Proof.context
4.9 | Ass_Weak of Tactic.T * term * Proof.context
4.10 - | NotAss;
4.11 + | Not_Associated;
4.12 val associate: Ctree.ctree -> Proof.context -> (Tactic.T * term) -> ass
4.13
4.14 val init_form : 'a -> Program.T -> (term * term) list -> term option
4.15 @@ -101,12 +101,12 @@
4.16 | tac_from_prog _ thy t = error ("stac2tac_ TODO: no match for " ^ Rule.term_to_string''' thy t);
4.17
4.18 datatype ass =
4.19 - Ass of
4.20 + Associated of
4.21 Tactic.T (* SubProblem gets args instantiated in associate *)
4.22 * term (* for itr_arg, result in ets *)
4.23 * Proof.context (* separate from Tactic.T like in locate_input_tactic *)
4.24 | Ass_Weak of Tactic.T * term * Proof.context
4.25 - | NotAss;
4.26 + | Not_Associated;
4.27
4.28 (* check if tac_ is associated with stac.
4.29 Note: this is the only fun in "fun locate_input_tactic", which handles tactics individually.
4.30 @@ -121,10 +121,10 @@
4.31 tac_ : from user (via applicable_in); to be compared with ...
4.32 stac : found in program
4.33 returns
4.34 - Ass : associated: e.g. thmID in stac = thmID in m
4.35 + Associated : associated: e.g. thmID in stac = thmID in m
4.36 +++ arg in stac = arg in m
4.37 Ass_Weak: weakly ass.:e.g. thmID in stac = thmID in m, //arg//
4.38 - NotAss : e.g. thmID in stac/=/thmID in m (not =)
4.39 + Not_Associated : e.g. thmID in stac/=/thmID in m (not =)
4.40 *)
4.41 fun associate _ ctxt (m as Tactic.Rewrite_Inst'
4.42 (_, _, _, _, _, thm'' as (thmID, _), f, (f', asms')), stac) =
4.43 @@ -133,73 +133,73 @@
4.44 if thmID = HOLogic.dest_string thmID_
4.45 then
4.46 if f = f_
4.47 - then Ass (m, f', ContextC.insert_assumptions asms' ctxt)
4.48 + then Associated (m, f', ContextC.insert_assumptions asms' ctxt)
4.49 else Ass_Weak (m, f', ContextC.insert_assumptions asms' ctxt)
4.50 - else ((*tracing"3### associate ..NotAss";*) NotAss)
4.51 + else ((*tracing"3### associate ..Not_Associated";*) Not_Associated)
4.52 | (Const ("Prog_Tac.Rewrite'_Set'_Inst",_) $ _ $ rls_ $ f_) =>
4.53 if Rtools.contains_rule (Rule.Thm thm'') (assoc_rls (HOLogic.dest_string rls_))
4.54 - then if f = f_ then Ass (m, f', ContextC.insert_assumptions asms' ctxt)
4.55 + then if f = f_ then Associated (m, f', ContextC.insert_assumptions asms' ctxt)
4.56 else Ass_Weak (m, f', ContextC.insert_assumptions asms' ctxt)
4.57 - else NotAss
4.58 - | _ => NotAss)
4.59 + else Not_Associated
4.60 + | _ => Not_Associated)
4.61 | associate _ ctxt (m as Tactic.Rewrite' (_, _, _, _, thm'' as (thmID, _), f, (f', asms')), stac) =
4.62 (case stac of
4.63 (Const ("Prog_Tac.Rewrite", _) $ thmID_ $ f_) =>
4.64 if thmID = HOLogic.dest_string thmID_
4.65 then
4.66 if f = f_
4.67 - then Ass (m, f', ContextC.insert_assumptions asms' ctxt)
4.68 + then Associated (m, f', ContextC.insert_assumptions asms' ctxt)
4.69 else Ass_Weak (m, f', ContextC.insert_assumptions asms' ctxt)
4.70 - else NotAss
4.71 + else Not_Associated
4.72 | (Const ("Prog_Tac.Rewrite'_Set", _) $ rls_ $ f_) =>
4.73 if Rtools.contains_rule (Rule.Thm thm'') (assoc_rls (HOLogic.dest_string rls_))
4.74 then
4.75 if f = f_
4.76 - then Ass (m, f', ContextC.insert_assumptions asms' ctxt)
4.77 + then Associated (m, f', ContextC.insert_assumptions asms' ctxt)
4.78 else Ass_Weak (m, f', ContextC.insert_assumptions asms' ctxt)
4.79 - else NotAss
4.80 - | _ => NotAss)
4.81 + else Not_Associated
4.82 + | _ => Not_Associated)
4.83 | associate _ ctxt (m as Tactic.Rewrite_Set_Inst' (_, _, _, rls, f, (f', asms')),
4.84 (Const ("Prog_Tac.Rewrite'_Set'_Inst", _) $ _ $ rls_ $ f_)) =
4.85 if Rule.id_rls rls = HOLogic.dest_string rls_
4.86 then
4.87 if f = f_
4.88 - then Ass (m, f', ContextC.insert_assumptions asms' ctxt)
4.89 + then Associated (m, f', ContextC.insert_assumptions asms' ctxt)
4.90 else Ass_Weak (m ,f', ContextC.insert_assumptions asms' ctxt)
4.91 - else NotAss
4.92 + else Not_Associated
4.93 | associate _ ctxt (m as Tactic.Detail_Set_Inst' (_, _, _, rls, f, (f', asms')),
4.94 (Const ("Prog_Tac.Rewrite'_Set'_Inst", _) $ _ $ rls_ $ f_)) =
4.95 if Rule.id_rls rls = HOLogic.dest_string rls_
4.96 then
4.97 if f = f_
4.98 - then Ass (m, f', ContextC.insert_assumptions asms' ctxt)
4.99 + then Associated (m, f', ContextC.insert_assumptions asms' ctxt)
4.100 else Ass_Weak (m ,f', ContextC.insert_assumptions asms' ctxt)
4.101 - else NotAss
4.102 + else Not_Associated
4.103 | associate _ ctxt (m as Tactic.Rewrite_Set' (_, _, rls, f, (f', asms')),
4.104 (Const ("Prog_Tac.Rewrite'_Set", _) $ rls_ $ f_)) =
4.105 if Rule.id_rls rls = HOLogic.dest_string rls_
4.106 then
4.107 if f = f_
4.108 - then Ass (m, f', ContextC.insert_assumptions asms' ctxt)
4.109 + then Associated (m, f', ContextC.insert_assumptions asms' ctxt)
4.110 else Ass_Weak (m ,f', ContextC.insert_assumptions asms' ctxt)
4.111 - else NotAss
4.112 + else Not_Associated
4.113 | associate _ ctxt (m as Tactic.Detail_Set' (_, _, rls, f, (f', asms')),
4.114 (Const ("Prog_Tac.Rewrite'_Set", _) $ rls_ $ f_)) =
4.115 if Rule.id_rls rls = HOLogic.dest_string rls_
4.116 then
4.117 if f = f_
4.118 - then Ass (m, f', ContextC.insert_assumptions asms' ctxt)
4.119 + then Associated (m, f', ContextC.insert_assumptions asms' ctxt)
4.120 else Ass_Weak (m ,f', ContextC.insert_assumptions asms' ctxt)
4.121 - else NotAss
4.122 + else Not_Associated
4.123 | associate _ ctxt (m as Tactic.Calculate' (_, op_, f, (f', _)), stac) =
4.124 (case stac of
4.125 (Const ("Prog_Tac.Calculate",_) $ op__ $ f_) =>
4.126 if op_ = HOLogic.dest_string op__
4.127 then
4.128 if f = f_
4.129 - then Ass (m, f', ctxt)
4.130 + then Associated (m, f', ctxt)
4.131 else Ass_Weak (m ,f', ctxt)
4.132 - else NotAss
4.133 + else Not_Associated
4.134 | (Const ("Prog_Tac.Rewrite'_Set'_Inst", _) $ _ $ rls_ $ f_) =>
4.135 let val thy = Celem.assoc_thy "Isac_Knowledge";
4.136 in
4.137 @@ -207,9 +207,9 @@
4.138 (assoc_rls (HOLogic.dest_string rls_))
4.139 then
4.140 if f = f_
4.141 - then Ass (m, f', ctxt)
4.142 + then Associated (m, f', ctxt)
4.143 else Ass_Weak (m ,f', ctxt)
4.144 - else NotAss
4.145 + else Not_Associated
4.146 end
4.147 | (Const ("Prog_Tac.Rewrite'_Set",_) $ rls_ $ f_) =>
4.148 let val thy = Celem.assoc_thy "Isac_Knowledge";
4.149 @@ -218,46 +218,46 @@
4.150 (assoc_rls (HOLogic.dest_string rls_))
4.151 then
4.152 if f = f_
4.153 - then Ass (m, f', ctxt)
4.154 + then Associated (m, f', ctxt)
4.155 else Ass_Weak (m ,f', ctxt)
4.156 - else NotAss
4.157 + else Not_Associated
4.158 end
4.159 - | _ => NotAss)
4.160 + | _ => Not_Associated)
4.161 | associate _ ctxt (m as Tactic.Check_elementwise' (consts, _, (consts_chkd, _)),
4.162 (Const ("Prog_Tac.Check'_elementwise",_) $ consts' $ _)) =
4.163 if consts = consts'
4.164 - then Ass (m, consts_chkd, ctxt)
4.165 - else NotAss
4.166 + then Associated (m, consts_chkd, ctxt)
4.167 + else Not_Associated
4.168 | associate _ ctxt (m as Tactic.Or_to_List' (_, list), (Const ("Prog_Tac.Or'_to'_List", _) $ _)) =
4.169 - Ass (m, list, ctxt)
4.170 - | associate _ ctxt (m as Tactic.Take' term, (Const ("Prog_Tac.Take", _) $ _)) = Ass (m, term, ctxt)
4.171 + Associated (m, list, ctxt)
4.172 + | associate _ ctxt (m as Tactic.Take' term, (Const ("Prog_Tac.Take", _) $ _)) = Associated (m, term, ctxt)
4.173 | associate _ ctxt (m as Tactic.Substitute' (ro, erls, subte, f, f'),
4.174 (Const ("Prog_Tac.Substitute", _) $ _ $ t)) =
4.175 - if f = t then Ass (m, f', ctxt)
4.176 + if f = t then Associated (m, f', ctxt)
4.177 else (*compare | applicable_in (p,p_) pt (m as Substitute sube)*)
4.178 if foldl and_ (true, map TermC.contains_Var subte)
4.179 then
4.180 let val t' = subst_atomic (map HOLogic.dest_eq subte (*TODO subte2subst*)) t
4.181 in if t = t' then error "associate: Substitute' not applicable to val of Expr"
4.182 - else Ass (Tactic.Substitute' (ro, erls, subte, t, t'), t', ctxt)
4.183 + else Associated (Tactic.Substitute' (ro, erls, subte, t, t'), t', ctxt)
4.184 end
4.185 else (case Rewrite.rewrite_terms_ (Rule.Isac ()) ro erls subte t of
4.186 - SOME (t', _) => Ass (Tactic.Substitute' (ro, erls, subte, t, t'), t', ctxt)
4.187 + SOME (t', _) => Associated (Tactic.Substitute' (ro, erls, subte, t, t'), t', ctxt)
4.188 | NONE => error "associate: Substitute' not applicable to val of Expr")
4.189 | associate pt ctxt (Tactic.Subproblem' ((domID, pblID, _), _, _, _, _, _),
4.190 (stac as Const ("Prog_Tac.SubProblem", _) $ _ $ _)) =
4.191 (case Sub_Problem.tac_from_prog pt stac of
4.192 (_, tac as Tactic.Subproblem' ((dI, pI, _), _, _, _, _, f)) =>
4.193 if domID = dI andalso pblID = pI
4.194 - then Ass (tac, f, ctxt)
4.195 - else NotAss
4.196 + then Associated (tac, f, ctxt)
4.197 + else Not_Associated
4.198 | _ => raise ERROR ("associate: uncovered case"))
4.199 | associate _ _ (m, _) =
4.200 (if (!trace_script)
4.201 then tracing("@@@ the 'tac_' proposed to apply does NOT match the leaf found in the script:\n"
4.202 ^ "@@@ tac_ = " ^ Tactic.string_of m)
4.203 else ();
4.204 - NotAss);
4.205 + Not_Associated);
4.206
4.207 (* create the initial interpreter state
4.208 from the items of the guard and the formal arguments of the partial_function.
5.1 --- a/src/Tools/isac/Interpret/lucas-interpreter.sml Tue Mar 31 14:05:10 2020 +0200
5.2 +++ b/src/Tools/isac/Interpret/lucas-interpreter.sml Tue Mar 31 15:43:33 2020 +0200
5.3 @@ -286,7 +286,7 @@
5.4 | _ => End_Program (Pstate ist, Tactic.End_Detail' (Rule.e_term,[])))
5.5 | Reject_Tac => Helpless)
5.6 | find_next_step _ _ ist _ =
5.7 - raise ERROR ("find_next_step: not impl for " ^ istate2str ist);
5.8 + raise ERROR ("find_next_step: not impl for " ^ Istate.string_of ist);
5.9
5.10
5.11 (*** locate an input tactic within a program ***)
5.12 @@ -315,12 +315,11 @@
5.13
5.14 fun check_tac1 ((pt, p), ctxt, tac) (ist as {act_arg, or, ...}) (prog_tac, form_arg) =
5.15 case LItool.associate pt ctxt (tac, prog_tac) of
5.16 - (* HERE ----------------vvvv ContextC.insert_assumptions asm ctxt DONE -- 2nd in gen//*)
5.17 - LItool.Ass (m, v', ctxt)
5.18 + LItool.Associated (m, v', ctxt)
5.19 => Accept_Tac1 (ist |> set_subst_true (form_arg, v') |> set_found, ctxt, m)
5.20 | LItool.Ass_Weak (m, v', ctxt) (*the ONLY ones in locate_tac ^v^v^v^v^ *)
5.21 => Accept_Tac1 (ist |> set_subst_false (form_arg, v') |> set_found, ctxt, m)
5.22 - | LItool.NotAss =>
5.23 + | LItool.Not_Associated =>
5.24 (case or of (* switch for Tactical.Or: 1st AssOnly, 2nd AssGen *)
5.25 AssOnly => Term_Val1 act_arg
5.26 | _(*ORundef*) =>
5.27 @@ -563,7 +562,7 @@
5.28 (*OLD* ) vvv--- handled by ctxt \<rightarrow> drop ( *OLD*)
5.29 (*OLD*)val asm = (*?!? Rfun,Rrls rm case*)(case get_obj g_tac pt p of
5.30 (*OLD*) Tactic.Check_elementwise _ => (snd o (get_obj g_result pt)) p
5.31 -(*OLD*) | _ => get_assumptions_ pt pos)
5.32 +(*OLD*) | _ => Ctree.get_assumptions pt pos)
5.33 (*OLD* )val tac = Tactic.Check_Postcond' (pI, (prog_res, asm))
5.34 ( *OLD*)
5.35 in
5.36 @@ -682,8 +681,8 @@
5.37 * formula, which is no CAS-command:
5.38 compare iform with calc-tree.form at pos by equ_nrls and all subsequent pos;
5.39 collect all the Prog_Tac applied by the way; ...???TODO?
5.40 - If "no derivation found" then check_error_patterns.
5.41 - ALTERNATIVE: check_error_patterns _within_ compare_step: seems too expensive
5.42 + If "no derivation found" then Error_Pattern.check_for.
5.43 + ALTERNATIVE: Error_Pattern.check_for _within_ compare_step: seems too expensive
5.44 *)
5.45 fun locate_input_term (pt, pos) tm =
5.46 let
6.1 --- a/src/Tools/isac/Interpret/rewtools.sml Tue Mar 31 14:05:10 2020 +0200
6.2 +++ b/src/Tools/isac/Interpret/rewtools.sml Tue Mar 31 15:43:33 2020 +0200
6.3 @@ -164,7 +164,7 @@
6.4 case Rewrite.rewrite_ thy ro erls true tm t of
6.5 NONE => rew_once lim rts t apno rs'
6.6 | SOME (t', a') =>
6.7 - (if ! Celem.trace_rewrite then tracing ("### rewrites to: " ^ Rule.term2str t') else ();
6.8 + (if ! Celem.trace_rewrite then tracing ("=== rewrites to: " ^ Rule.term2str t') else ();
6.9 rew_once (lim - 1) (rts @ [(t, r, (t', a'))]) t' Appl rrs'))
6.10 | Rule.Num_Calc (c as (op_, _)) =>
6.11 let
6.12 @@ -178,7 +178,7 @@
6.13 val (t', a') = case Rewrite.rewrite_ thy ro erls true tm t of
6.14 SOME ta => ta
6.15 | NONE => error "adhoc_thm: NONE"
6.16 - val _ = if not (! Celem.trace_rewrite) then () else tracing("### calc. to: " ^ Rule.term2str t')
6.17 + val _ = if not (! Celem.trace_rewrite) then () else tracing("=== calc. to: " ^ Rule.term2str t')
6.18 val r' = Rule.Thm (thmid, tm)
6.19 in rew_once (lim - 1) (rts @ [(t, r', (t', a'))]) t' Appl rrs' end)
6.20 handle _ => error "derive_norm, Num_Calc: no rewrite"
7.1 --- a/src/Tools/isac/Interpret/step-solve.sml Tue Mar 31 14:05:10 2020 +0200
7.2 +++ b/src/Tools/isac/Interpret/step-solve.sml Tue Mar 31 15:43:33 2020 +0200
7.3 @@ -110,7 +110,7 @@
7.4 | _ => error "inform: uncovered case of get_met"
7.5 val {env, ...} = Ctree.get_istate_LI pt pos |> Istate.the_pstate
7.6 in
7.7 - case Error_Pattern.check_error_patterns (f_pred, f_in) (prog, env) (errpats, nrls) of
7.8 + case Error_Pattern.check_for (f_pred, f_in) (prog, env) (errpats, nrls) of
7.9 SOME errpatID => ("error pattern #" ^ errpatID ^ "#", Chead.e_calcstate')
7.10 | NONE => ("no derivation found", Chead.e_calcstate')
7.11 end
8.1 --- a/src/Tools/isac/MathEngBasic/ctree-access.sml Tue Mar 31 14:05:10 2020 +0200
8.2 +++ b/src/Tools/isac/MathEngBasic/ctree-access.sml Tue Mar 31 15:43:33 2020 +0200
8.3 @@ -182,7 +182,7 @@
8.4 fun append_atomic p (ic_form, ic_res) f r f' s pt =
8.5 let
8.6 val (iss, f) =
8.7 - if existpt p pt andalso Tactic.is_empty_tac (get_obj g_tac pt p)
8.8 + if existpt p pt andalso Tactic.is_empty (get_obj g_tac pt p)
8.9 (* ^^^^^^^ ^^ probably is cut, so this ^^^^^^^^^^^^^^^^^^ might cause
8.10 exception PTREE "get_obj: pos = ... does not exist", (!) WHICH IS NOT RECOGNISED BY if *)
8.11 then ((fst (get_obj g_loc pt p), SOME ic_res), get_obj g_form pt p) (*after Take*)
8.12 @@ -195,7 +195,7 @@
8.13 detail - generate - cappend: inserted, not appended !!!
8.14 cut decided in applicable_in !?! and represented by flag ? *)
8.15 fun cappend_atomic pt p ic_res f r f' s =
8.16 - if existpt p pt andalso Tactic.is_empty_tac (get_obj g_tac pt p)
8.17 + if existpt p pt andalso Tactic.is_empty (get_obj g_tac pt p)
8.18 then (*after Take: transfer Frm and respective istate*)
8.19 let
8.20 val (ic_form, f) = (get_loc pt (p, Frm), get_obj g_form pt p)
9.1 --- a/src/Tools/isac/MathEngBasic/ctree-basic.sml Tue Mar 31 14:05:10 2020 +0200
9.2 +++ b/src/Tools/isac/MathEngBasic/ctree-basic.sml Tue Mar 31 15:43:33 2020 +0200
9.3 @@ -75,7 +75,7 @@
9.4 val get_ctxt : ctree -> pos' -> Proof.context (*DEPRECATED*)
9.5 val get_obj : (ppobj -> 'a) -> ctree -> pos -> 'a
9.6 val get_curr_formula : state -> term
9.7 - val get_assumptions_ : ctree -> pos' -> term list (* for appl.sml *)
9.8 + val get_assumptions : ctree -> pos' -> term list (* for appl.sml *)
9.9
9.10 val new_val : term -> Istate_Def.T -> Istate_Def.T
9.11 (* for calchead.sml *)
9.12 @@ -100,7 +100,6 @@
9.13 val g_res : ppobj -> term
9.14 val g_res' : ctree -> term
9.15 (*/---- duplicates in CTnavi, reconsider structs -----------------------------------------------
9.16 - val lev_on : CTbasic.pos -> CTbasic.pos (* duplicate in ctree-navi.sml *)
9.17 val lev_dn : CTbasic.pos -> CTbasic.pos (* duplicate in ctree-navi.sml *)
9.18 val par_pblobj : CTbasic.ctree -> CTbasic.pos -> CTbasic.pos (* duplicate in ctree-navi.sml *)
9.19 ---- duplicates in CTnavi, reconsider structs ----------------------------------------------/*)
9.20 @@ -375,10 +374,6 @@
9.21 | children _ = error "children: uncovered fun def.";
9.22
9.23 (*/--------------- duplicates in ctree-navi.sml: required also here below ---------------\*)
9.24 -fun lev_on [] = raise PTREE "lev_on []"
9.25 - | lev_on pos =
9.26 - let val len = length pos
9.27 - in (drop_last pos) @ [(nth len pos)+1] end;
9.28 fun lev_up [] = raise PTREE "lev_up []"
9.29 | lev_up p = (drop_last p):pos;
9.30 (* find the position of the next parent which is a PblObj in ctree *)
9.31 @@ -488,7 +483,7 @@
9.32 then get_loc pt pos |> #2 (*for script interpretation rely on fun get_loc*)
9.33 else get_obj g_ctxt pt p (*for specify phase take ctx from PblObj*)
9.34
9.35 -fun get_assumptions_ pt p = get_ctxt pt p |> ContextC.get_assumptions;
9.36 +fun get_assumptions pt p = get_ctxt pt p |> ContextC.get_assumptions;
9.37
9.38 fun get_somespec' (dI, pI, mI) (dI', pI', mI') =
9.39 let
10.1 --- a/src/Tools/isac/MathEngBasic/istate-def.sml Tue Mar 31 14:05:10 2020 +0200
10.2 +++ b/src/Tools/isac/MathEngBasic/istate-def.sml Tue Mar 31 15:43:33 2020 +0200
10.3 @@ -16,8 +16,8 @@
10.4
10.5 datatype T = RrlsState of Rule.rrlsstate | Pstate of pstate | Uistate
10.6 val e_istate: T
10.7 - val istate2str: T -> string
10.8 - val istate2str': T -> string
10.9 + val string_of: T -> string
10.10 + val string_of': T -> string
10.11 val istates2str: T option * T option -> string
10.12
10.13 val set_eval: Rule.rls -> pstate -> pstate
10.14 @@ -37,7 +37,7 @@
10.15 ORundef (* undefined: set only by (topmost) Or *)
10.16 | AssOnly (* do not execute applicable Prog_Tac - there could be an associated
10.17 in parallel Or-branch *)
10.18 -| AssGen; (* no Ass(Weak) found within Or, thus continue scan
10.19 +| AssGen; (* no Associated(Weak) found within Or, thus continue scan
10.20 search for _applicable_ stacs, execute and generate pt *)
10.21 (*this constructions doesnt allow arbitrary nesting of Or !!! *)
10.22 fun asap2str ORundef = "ORundef"
10.23 @@ -75,21 +75,21 @@
10.24 val e_istate = Pstate e_pstate;
10.25
10.26 fun rta2str (r, (t, a)) = "\n(" ^ Rule.rule2str r ^ ", (" ^ Rule.term2str t ^ ", " ^ Rule.terms2str a ^ "))";
10.27 -fun istate2str Uistate = "Uistate"
10.28 - | istate2str (Pstate pst) =
10.29 +fun string_of Uistate = "Uistate"
10.30 + | string_of (Pstate pst) =
10.31 "Pstate " ^ pstate2str pst
10.32 - | istate2str (RrlsState (t, t1, rss, rtas)) =
10.33 + | string_of (RrlsState (t, t1, rss, rtas)) =
10.34 "RrlsState (" ^ Rule.term2str t ^ ", " ^ Rule.term2str t1 ^ ", " ^
10.35 (strs2str o (map (strs2str o (map Rule.rule2str)))) rss ^ ", " ^
10.36 (strs2str o (map rta2str)) rtas ^ ")";
10.37 -fun istate2str' Uistate = "Uistate"
10.38 - | istate2str' (Pstate pst) =
10.39 +fun string_of' Uistate = "Uistate"
10.40 + | string_of' (Pstate pst) =
10.41 "Pstate " ^ pstate2str' pst
10.42 - | istate2str' (RrlsState _) = raise ERROR "istate2str: drop RrlsState"
10.43 + | string_of' (RrlsState _) = raise ERROR "istate2str: drop RrlsState"
10.44 fun istates2str (NONE, NONE) = "(#NONE, #NONE)" (* for tests only *)
10.45 - | istates2str (NONE, SOME ist) = "(#NONE,\n#SOME " ^ istate2str ist ^ ")"
10.46 - | istates2str (SOME ist, NONE) = "(#SOME " ^ istate2str ist ^ ",\n #NONE)"
10.47 - | istates2str (SOME i1, SOME i2) = "(#SOME " ^ istate2str i1 ^ ",\n #SOME " ^ istate2str i2 ^ ")";
10.48 + | istates2str (NONE, SOME ist) = "(#NONE,\n#SOME " ^ string_of ist ^ ")"
10.49 + | istates2str (SOME ist, NONE) = "(#SOME " ^ string_of ist ^ ",\n #NONE)"
10.50 + | istates2str (SOME i1, SOME i2) = "(#SOME " ^ string_of i1 ^ ",\n #SOME " ^ string_of i2 ^ ")";
10.51
10.52
10.53 fun set_eval e {env, path, form_arg, act_arg, or, found_accept, assoc, ...} =
11.1 --- a/src/Tools/isac/MathEngBasic/tactic-def.sml Tue Mar 31 14:05:10 2020 +0200
11.2 +++ b/src/Tools/isac/MathEngBasic/tactic-def.sml Tue Mar 31 15:43:33 2020 +0200
11.3 @@ -106,7 +106,7 @@
11.4 | Take of Rule.cterm' | Take_Inst of Rule.cterm'
11.5 val tac2str : input -> string
11.6 val tac2IDstr : input -> string
11.7 - val is_empty_tac : input -> bool
11.8 + val is_empty : input -> bool
11.9 end
11.10
11.11 (**)
11.12 @@ -225,7 +225,7 @@
11.13 | End_Proof' => "input End_Proof'"
11.14 | _ => "tac2str not impl. for ?!";
11.15
11.16 -fun is_empty_tac input = case input of Empty_Tac => true | _ => false
11.17 +fun is_empty input = case input of Empty_Tac => true | _ => false
11.18
11.19 (* tactics for for internal use, compare "input" for user at the front-end.
11.20 tac_ contains results from check in 'fun applicable_in'.
12.1 --- a/src/Tools/isac/MathEngBasic/tactic.sml Tue Mar 31 14:05:10 2020 +0200
12.2 +++ b/src/Tools/isac/MathEngBasic/tactic.sml Tue Mar 31 15:43:33 2020 +0200
12.3 @@ -15,7 +15,7 @@
12.4 datatype input = datatype Tactic_Def.input
12.5 val tac2str : input -> string
12.6 val tac2IDstr : input -> string
12.7 - val is_empty_tac : input -> bool
12.8 + val is_empty : input -> bool
12.9
12.10 (*//-------------------------------------------------------------- only AFTER ctree.sml required *)
12.11 val eq_tac : input * input -> bool
12.12 @@ -49,7 +49,7 @@
12.13
12.14 val tac2str = Tactic_Def.tac2str
12.15 val tac2IDstr = Tactic_Def.tac2IDstr
12.16 -val is_empty_tac = Tactic_Def.is_empty_tac
12.17 +val is_empty = Tactic_Def.is_empty
12.18
12.19 fun eq_tac (Rewrite (id1, _), Rewrite (id2, _)) = id1 = id2
12.20 | eq_tac (Rewrite_Inst (_, (id1, _)), Rewrite_Inst (_, (id2, _))) = id1 = id2
13.1 --- a/src/Tools/isac/Specify/appl.sml Tue Mar 31 14:05:10 2020 +0200
13.2 +++ b/src/Tools/isac/Specify/appl.sml Tue Mar 31 15:43:33 2020 +0200
13.3 @@ -80,13 +80,13 @@
13.4 | mk_set _ pt p (Const ("ListC.UniversalList", _)) pred =
13.5 (Rule.e_term, if pred <> Const ("Prog_Tac.Assumptions", HOLogic.boolT)
13.6 then [pred]
13.7 - else get_assumptions_ pt (p, Res))
13.8 + else Ctree.get_assumptions pt (p, Res))
13.9 | mk_set _ pt p (Const ("List.list.Cons",_) $ eq $ _) pred =
13.10 let
13.11 val (bdv,_) = HOLogic.dest_eq eq;
13.12 val pred = if pred <> Const ("Prog_Tac.Assumptions", HOLogic.boolT)
13.13 then [pred]
13.14 - else get_assumptions_ pt (p, Res)
13.15 + else Ctree.get_assumptions pt (p, Res)
13.16 in (bdv, pred) end
13.17 | mk_set _ _ _ l _ =
13.18 error ("check_elementwise: no set " ^ Rule.term2str l);
14.1 --- a/src/Tools/isac/Specify/generate.sml Tue Mar 31 14:05:10 2020 +0200
14.2 +++ b/src/Tools/isac/Specify/generate.sml Tue Mar 31 15:43:33 2020 +0200
14.3 @@ -82,7 +82,7 @@
14.4 val e_taci = (Tactic.Empty_Tac, Tactic.Empty_Tac_, (e_pos', (Istate_Def.e_istate, ContextC.e_ctxt))): taci
14.5 fun taci2str ((tac, tac_, (pos', (istate, _))):taci) =
14.6 "( " ^ Tactic.tac2str tac ^ ", " ^ Tactic.string_of tac_ ^ ", ( " ^ pos'2str pos' ^ ", " ^
14.7 - Istate_Def.istate2str istate ^ " ))"
14.8 + Istate_Def.string_of istate ^ " ))"
14.9 fun tacis2str tacis = (strs2str o (map (Celem.linefeed o taci2str))) tacis
14.10
14.11 datatype pblmet = (*%^%*)
15.1 --- a/src/Tools/isac/TODO.thy Tue Mar 31 14:05:10 2020 +0200
15.2 +++ b/src/Tools/isac/TODO.thy Tue Mar 31 15:43:33 2020 +0200
15.3 @@ -28,44 +28,24 @@
15.4 \item xxx
15.5 \item xxx
15.6 \item xxx
15.7 - \item RM asm FROM Check_Postcond' (pI, (prog_res, asm)) ... asms are handled by ctxt !
15.8 \item xxx
15.9 - \item generate.sml: RM datatype edit = EdUndef | Write | Protect
15.10 \item xxx
15.11 - \item ad ERROR @unknown fact all_left in Test_Isac: search "Undefined"
15.12 - Undef -> Real_Undef
15.13 \item xxx
15.14 - \item TermC.list2isalist: typ -> term list -> term .. should NOT requires typ
15.15 \item xxx
15.16 - \item restore clarity of "trace_rewrite": "=====" seems to be lost:
15.17 - ##### try calc: HOL.eq' <<<------------------------------- here the error comes from
15.18 - ===== calc. to: ~ False <<<------------------------------- \<not> x = 0 is NOT False
15.19 - ##### try calc: HOL.eq'
15.20 - ##### try thm: not_true
15.21 - ##### try thm: not_false
15.22 - ===== rewrites to: True <<<------------------------------- so x \<noteq> 0 is NOT True
15.23 \item xxx
15.24 - \item get_ctxt_LI should replace get_ctxt
15.25 \item xxx
15.26 - \item change separate test ----------------------vvv
15.27 - | by_tactic (tac as Tactic.Check_Postcond' _) ptp =
15.28 - LI.by_tactic tac (Istate.e_istate, ContextC.e_ctxt) ptp
15.29 - -----------------^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
15.30 \item xxx
15.31 - \item mv Ctree.get_assumptions_ -> Ctree.ctxt_assumptions
15.32 \item xxx
15.33 - \item Error_Pattern.check_error_pattern -> Error_Pattern.check
15.34 \item xxx
15.35 - \item DEL double code: lev_on +??? in ctree-basic.sml + position
15.36 \item xxx
15.37 \item DEL double code: nxt_specify_init_calc IN specify.sml + step-specify.sml
15.38 \item xxx
15.39 - \item ALL CODE: rename spec(ification) --> know(ledge), in Specification: Relation -> Knowledge
15.40 + \item associate: drop ctxt from arg.+ return
15.41 \item xxx
15.42 - \item replace ContextC.insert_assumptions by Tactic.insert_assumptions
15.43 - NOTE: DONE in associate, ??missing in LI.do_step ??
15.44 \item xxx
15.45 - \item associate: drop ctxt from arg.+ return
15.46 + \item xxx
15.47 + \item xxx
15.48 + \item xxx
15.49 \item xxx
15.50 \item in check_leaf SEPARATE tracing
15.51 collect all trace_script --> Trace_LI
15.52 @@ -73,13 +53,7 @@
15.53 \item xxx
15.54 \item renamings
15.55 \begin{itemize}
15.56 - \item NotAss -> Not_Associated | Ass -> Associated
15.57 - \item ContextC.subpbl_to_caller -> subpbl_to_caller
15.58 - \item Tactic.is_empty_tac -> Tactic.is_empty
15.59 - \item Istate.istate2str -> Istate.string_of
15.60 \item xxx
15.61 - \item rename Base_Tool.thy <--- Base_Tools
15.62 - \item adopt naming conventions in Knowledge: EqSystem --> Equation_System, etc
15.63 \item xxx
15.64 \item rename field scr in meth
15.65 \item xxx
15.66 @@ -159,6 +133,13 @@
15.67 subsection \<open>Postponed from current changeset\<close>
15.68 text \<open>
15.69 \begin{itemize}
15.70 + \item LI.do_next (*TODO RM..*) ???
15.71 + \item generate.sml: RM datatype edit TOGETHER WITH datatype inout
15.72 + \item TermC.list2isalist: typ -> term list -> term .. should NOT requires typ
15.73 + \item get_ctxt_LI should replace get_ctxt
15.74 + \item ALL CODE: rename spec(ification) --> know(ledge), in Specification: Relation -> Knowledge
15.75 + \item rename Base_Tool.thy <--- Base_Tools
15.76 + \item adopt naming conventions in Knowledge: EqSystem --> Equation_System, etc
15.77 \item xxx
15.78 \item xxx
15.79 \item cleanup fun me:
15.80 @@ -428,7 +409,7 @@
15.81 text \<open>
15.82 analysis
15.83 # mixture pos' .. pos in cappend_*, append_* is confusing
15.84 -# existpt p pt andalso Tactic.is_empty_tac DIFFERENT IN append_*, cappend_* is confusing
15.85 +# existpt p pt andalso Tactic.is_empty DIFFERENT IN append_*, cappend_* is confusing
15.86 "exception PTREE "get_obj: pos =" ^^^^^: ^^^^ due to cut !!!
15.87 NOTE: exn IN if..andalso.. IS NOT!!! DETECTED, THIS is confusing
15.88 see test/../--- Minisubpbl/800-append-on-Frm.sml ---
15.89 @@ -651,6 +632,7 @@
15.90 section \<open>Questions to Isabelle experts\<close>
15.91 text \<open>
15.92 \begin{itemize}
15.93 +\item ad ERROR @unknown fact all_left in Test_Isac
15.94 \item xxx
15.95 \item xxx
15.96 \item ?OK Test_Isac_Short with
16.1 --- a/src/Tools/isac/Test_Code/test-code.sml Tue Mar 31 14:05:10 2020 +0200
16.2 +++ b/src/Tools/isac/Test_Code/test-code.sml Tue Mar 31 15:43:33 2020 +0200
16.3 @@ -99,7 +99,7 @@
16.4 | quiet _ = false
16.5
16.6 fun mk_string (ist, ctxt) =
16.7 - ("(" ^ Istate.istate2str' ist ^ ",\n"
16.8 + ("(" ^ Istate.string_of' ist ^ ",\n"
16.9 ^ "... ctxt: " ^ (ctxt |> ContextC.get_assumptions |> Rule.terms2str) ^ ")")
16.10
16.11 fun trace_ist_ctxt (EmptyPtree , ([], Pos.Und)) _ = ()
17.1 --- a/test/Tools/isac/ADDTESTS/All_Ctxt.thy Tue Mar 31 14:05:10 2020 +0200
17.2 +++ b/test/Tools/isac/ADDTESTS/All_Ctxt.thy Tue Mar 31 15:43:33 2020 +0200
17.3 @@ -50,7 +50,7 @@
17.4 text \<open>preconditions are known at start of interpretation of (root-)method\<close>
17.5
17.6 ML \<open>
17.7 - if Rule.terms2strs (Ctree.get_assumptions_ pt p) = ["precond_rootmet x"]
17.8 + if Rule.terms2strs (Ctree.get_assumptions pt p) = ["precond_rootmet x"]
17.9 then () else error "All_Ctx: asms after start interpretation of root-method";
17.10 \<close>
17.11
17.12 @@ -94,7 +94,7 @@
17.13 \<close>
17.14
17.15 ML \<open>
17.16 - if eq_set op = (Rule.terms2strs (Ctree.get_assumptions_ pt p),
17.17 + if eq_set op = (Rule.terms2strs (Ctree.get_assumptions pt p),
17.18 ["matches (?a = ?b) (-1 + x = 0)", "precond_rootmet x"])
17.19 then () else error "All_Ctx: asms after start interpretation of SubProblem";
17.20 \<close>
17.21 @@ -128,7 +128,7 @@
17.22
17.23 ML \<open>
17.24 \<close> ML \<open>
17.25 - if eq_set op = (Rule.terms2strs (Ctree.get_assumptions_ pt p),
17.26 + if eq_set op = (Rule.terms2strs (Ctree.get_assumptions pt p),
17.27 ["matches (?a = ?b) (-1 + x = 0)", "x < sub_asm_out", "x = 1", "precond_rootmet x"])
17.28 then () else error "All_Ctx: asms after finishing SubProblem";
17.29 \<close>
17.30 @@ -148,7 +148,7 @@
17.31
17.32 ML \<open>
17.33 \<close> ML \<open>
17.34 - if eq_set op = (Rule.terms2strs (Ctree.get_assumptions_ pt p),
17.35 + if eq_set op = (Rule.terms2strs (Ctree.get_assumptions pt p),
17.36 ["matches (?a = ?b) (-1 + x = 0)", "x < sub_asm_out", "x = 1", "precond_rootmet x"])
17.37 then () else error "All_Ctx at final result";
17.38 \<close>
18.1 --- a/test/Tools/isac/BridgeLibisabelle/use-cases.sml Tue Mar 31 14:05:10 2020 +0200
18.2 +++ b/test/Tools/isac/BridgeLibisabelle/use-cases.sml Tue Mar 31 15:43:33 2020 +0200
18.3 @@ -160,7 +160,7 @@
18.4
18.5 val (ptp as (pt,p), tacis) = get_calc 1; get_pos 1 1; (*<---------------------- orig. test code*)
18.6 (*+isa=REP*) if p = ([1], Frm) andalso term2str (get_obj g_form pt [1]) = "1 + -1 * 2 + x = 0"
18.7 -andalso istate2str (get_istate_LI pt p)
18.8 +andalso Istate.string_of (get_istate_LI pt p)
18.9 = "Pstate ([\"\n(e_e, 1 + -1 * 2 + x = 0)\",\"\n(v_v, x)\"], [], e_rls, NONE, \n??.empty, ORundef, false, true)"
18.10 then () else error "refFormula = 1 + -1 * 2 + x = 0 changed";
18.11 (*-------------------------------------------------------------------------*)
18.12 @@ -180,11 +180,11 @@
18.13
18.14 (*//******************* Step.by_tactic returns tac_ + istate + cstate *****************************\\*)
18.15 Step.by_tactic : Tactic.input -> state -> string * (taci list * pos' list * state);
18.16 -if istate2str istate
18.17 +if Istate.string_of istate
18.18 = "Pstate ([\"\n(e_e, 1 + -1 * 2 + x = 0)\",\"\n(v_v, x)\"], [R,L,R,L,R,L,R], e_rls, SOME e_e, \nx = 0 + -1 * (1 + -1 * 2), ORundef, true, true)"
18.19 then () else error "from Step.by_tactic return --- changed 1";
18.20
18.21 -if istate2str (get_istate_LI (fst cstate) (snd cstate))
18.22 +if Istate.string_of (get_istate_LI (fst cstate) (snd cstate))
18.23 = "Pstate ([\"\n(e_e, 1 + -1 * 2 + x = 0)\",\"\n(v_v, x)\"], [R,L,R,L,R,L,R], e_rls, SOME e_e, \nx = 0 + -1 * (1 + -1 * 2), ORundef, true, true)"
18.24 then () else error "from Step.by_tactic return --- changed 2";
18.25 (*\\******************* Step.by_tactic returns tac_ + istate + cstate *****************************//*)
18.26 @@ -203,7 +203,7 @@
18.27
18.28 (*+*)Safe_Step: Istate.T * Proof.context * T -> input_tactic_result;
18.29 (********************* locate_input_tactic returns cstate * istate * Proof.context *************)
18.30 -(*+*)if istate2str istate
18.31 +(*+*)if Istate.string_of istate
18.32 (*+isa*) = "Pstate ([\"\n(e_e, 1 + -1 * 2 + x = 0)\",\"\n(v_v, x)\"], [R,L,R,L,R,L,R], e_rls, SOME e_e, \nx = 0 + -1 * (1 + -1 * 2), ORundef, true, true)"
18.33 then case m of Rewrite_Set_Inst' _ => ()
18.34 else error "from locate_input_tactic return --- changed";
18.35 @@ -229,7 +229,7 @@
18.36
18.37 (*+isa==REP*)val [(Rewrite_Set_Inst (["(''bdv'', x)"], "isolate_bdv"),
18.38 Rewrite_Set_Inst' _, (pos', (istate, ctxt)))] = tacis;
18.39 -(*+*)if pos' = ([1], Res) andalso istate2str istate
18.40 +(*+*)if pos' = ([1], Res) andalso Istate.string_of istate
18.41 = "Pstate ([\"\n(e_e, 1 + -1 * 2 + x = 0)\",\"\n(v_v, x)\"], [R,L,R,L,R,L,R], e_rls, SOME e_e, \nx = 0 + -1 * (1 + -1 * 2), ORundef, true, true)"
18.42 then () else error "init. step 1 + -1 * 2 + x = 0 changed";
18.43
18.44 @@ -241,7 +241,7 @@
18.45 (*//------------------------------------- final test -----------------------------------------\\*)
18.46 val ("ok", [], ptp as (pt, p)) = xxxx;
18.47
18.48 -if istate2str (get_istate_LI pt p) (* <> <> <> <> ^^^^^^^^^^^^^*)
18.49 +if Istate.string_of (get_istate_LI pt p) (* <> <> <> <> ^^^^^^^^^^^^^*)
18.50 (*REP*) = "Pstate ([\"\n(e_e, 1 + -1 * 2 + x = 0)\",\"\n(v_v, x)\"], [R,L,R,L,R,L,R], e_rls, SOME e_e, \nx = 0 + -1 * (1 + -1 * 2), ORundef, true, true)"
18.51 then () else error "REP autoCalculate on (e_e, 1 + -1 * 2 + x = 0) changed"
18.52
19.1 --- a/test/Tools/isac/CalcElements/contextC.sml Tue Mar 31 14:05:10 2020 +0200
19.2 +++ b/test/Tools/isac/CalcElements/contextC.sml Tue Mar 31 15:43:33 2020 +0200
19.3 @@ -155,7 +155,7 @@
19.4 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
19.5 val (p,_,f,nxt,_,pt) = me nxt p [] pt; f2str f = "(3 + -1 * x + x ^^^ 2) * x = 1 * (9 * x + -6 * x ^^^ 2 + x ^^^ 3)";
19.6
19.7 -(*+*)if (Ctree.get_assumptions_ pt p |> map term2str) =
19.8 +(*+*)if (Ctree.get_assumptions pt p |> map term2str) =
19.9 (*+*) ["x \<noteq> 0",
19.10 (*+*) "9 * x + -6 * x ^^^ 2 + x ^^^ 3 \<noteq> 0",
19.11 (*+*) "x / (x ^^^ 2 - 6 * x + 9) - 1 / (x ^^^ 2 - 3 * x) =\n1 / x is_ratequation_in x"]
19.12 @@ -201,7 +201,7 @@
19.13 (*[4, 4, 4], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; f2str f = "[x = 0, x = 6 / 5]";
19.14 (*[4, 4, 5], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*\<rightarrow>2. Check_Postcond ["bdv_only", "degree_2", "polynomial", "univariate", "equation"]*)
19.15
19.16 -(* *)if eq_set op = ((Ctree.get_assumptions_ pt p |> map term2str), [
19.17 +(* *)if eq_set op = ((Ctree.get_assumptions pt p |> map term2str), [
19.18 (*0.pre*) "x / (x ^^^ 2 - 6 * x + 9) - 1 / (x ^^^ 2 - 3 * x) =\n1 / x is_ratequation_in x",
19.19 (*1.pre*) "\<not> matches (?a = 0)\n ((3 + -1 * x + x ^^^ 2) * x =\n 1 * (9 * x + -6 * x ^^^ 2 + x ^^^ 3)) \<or>\n"
19.20 (*1.pre*) ^ "\<not> lhs ((3 + -1 * x + x ^^^ 2) * x =\n 1 * (9 * x + -6 * x ^^^ 2 + x ^^^ 3)) is_poly_in x",
19.21 @@ -239,7 +239,7 @@
19.22 (*OLD* ) vvv--- handled by ctxt \<rightarrow> drop ( *OLD*)
19.23 (*OLD*)val asm = (*?!? Rfun,Rrls rm case*)(case get_obj g_tac pt p of
19.24 (*OLD*) Tactic.Check_elementwise _ => (snd o (get_obj g_result pt)) p
19.25 -(*OLD*) | _ => get_assumptions_ pt pos);
19.26 +(*OLD*) | _ => Ctree.get_assumptions pt pos);
19.27 (*OLD* )val tac = Tactic.Check_Postcond' (pI, (prog_res, asm))
19.28 ( *OLD*)
19.29 (*if*) parent_pos = [] (*else*);
19.30 @@ -305,7 +305,7 @@
19.31 (*[], Res*)val (p,_,f,nxt,_,pt) = me nxt''''' p''''' [] pt''''';(*\<rightarrow>End_Proof'*)
19.32
19.33 (*/-------- final test -----------------------------------------------------------------------\*)
19.34 -if f2str f = "[x = 6 / 5]" andalso map term2str (get_assumptions_ pt p) =
19.35 +if f2str f = "[x = 6 / 5]" andalso map term2str (Ctree.get_assumptions pt p) =
19.36 ["x = 6 / 5", "lhs (-6 * x + 5 * x ^^^ 2 = 0) is_poly_in x",
19.37 "lhs (-6 * x + 5 * x ^^^ 2 = 0) has_degree_in x = 2",
19.38 "\<not> matches (?a = 0)\n ((3 + -1 * x + x ^^^ 2) * x =\n 1 * (9 * x + -6 * x ^^^ 2 + x ^^^ 3)) \<or>\n\<not> lhs ((3 + -1 * x + x ^^^ 2) * x =\n 1 * (9 * x + -6 * x ^^^ 2 + x ^^^ 3)) is_poly_in x",
20.1 --- a/test/Tools/isac/Interpret/error-pattern.sml Tue Mar 31 14:05:10 2020 +0200
20.2 +++ b/test/Tools/isac/Interpret/error-pattern.sml Tue Mar 31 15:43:33 2020 +0200
20.3 @@ -29,8 +29,8 @@
20.4 "--------- init_form, start with <NEW> (CAS input) ---------------";
20.5 "--------- build fun check_err_patt ------------------------------";
20.6 "--------- build fun check_err_patt ?bdv -------------------------";
20.7 -"--------- build fun check_error_patterns ------------------------";
20.8 -"--------- embed fun check_error_patterns ------------------------";
20.9 +"--------- build fun Error_Pattern.check_for ------------------------";
20.10 +"--------- embed fun Error_Pattern.check_for ------------------------";
20.11 "--------- build fun get_fillpats --------------------------------";
20.12 "--------- embed fun find_fillpatterns ---------------------------";
20.13 "--------- build fun is_exactly_equal, inputFillFormula ----------";
20.14 @@ -648,7 +648,7 @@
20.15 spec;
20.16 writeln (itms2str_ ctxt probl);
20.17 writeln (itms2str_ ctxt meth);
20.18 -writeln (istate2str (fst istate));
20.19 +writeln (Istate.string_of (fst istate));
20.20
20.21 refFormula 1 ([],Pbl) (*--> correct CalcHead*);
20.22 (*081016 NOT necessary (but leave it in Java):*)
20.23 @@ -661,7 +661,7 @@
20.24 val PblObj {probl, meth, spec, fmz, env, loc, ...} = get_obj I pt [];
20.25 val NONE = env;
20.26 val (SOME istate, NONE) = loc;
20.27 -(*default_print_depth 5;*) writeln (istate2str (fst istate)); (*default_print_depth 3;*)
20.28 +(*default_print_depth 5;*) writeln (Istate.string_of (fst istate)); (*default_print_depth 3;*)
20.29 (*Pstate ([],
20.30 [], NONE,
20.31 ??.empty, Sundef, false)*)
20.32 @@ -705,7 +705,7 @@
20.33 val PblObj {probl, meth, spec, fmz, env, loc, ...} = get_obj I pt [];
20.34 val NONE = env;
20.35 val (SOME istate, NONE) = loc;
20.36 -(*default_print_depth 5;*) writeln (istate2str (fst istate)); (*default_print_depth 3;*)
20.37 +(*default_print_depth 5;*) writeln (Istate.string_of (fst istate)); (*default_print_depth 3;*)
20.38 (*Pstate ([],
20.39 [], NONE,
20.40 ??.empty, Sundef, false)*)
20.41 @@ -971,9 +971,9 @@
20.42 if check_err_patt (res, inf) (subst: subst) ("errpatID": errpatID, pat) rls = SOME "errpatID"
20.43 then () else error "error patt example1 changed";
20.44
20.45 -"--------- build fun check_error_patterns ------------------------";
20.46 -"--------- build fun check_error_patterns ------------------------";
20.47 -"--------- build fun check_error_patterns ------------------------";
20.48 +"--------- build fun Error_Pattern.check_for ------------------------";
20.49 +"--------- build fun Error_Pattern.check_for ------------------------";
20.50 +"--------- build fun Error_Pattern.check_for ------------------------";
20.51 val (res, inf) =
20.52 (str2term "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))",
20.53 str2term "d_d x (x ^^^ 2) + cos (4 * x ^^^ 3)");
20.54 @@ -990,13 +990,13 @@
20.55 parse_patt @{theory} "d_d ?bdv (LogExp.ln ?u) = 1 / d_d ?bdv ?u"],
20.56 [@{thm diff_sin_chain}, @{thm diff_cos_chain}, @{thm diff_pow_chain},
20.57 @{thm diff_ln_chain}, @{thm diff_exp_chain}])]: errpat list;
20.58 -case check_error_patterns (res, inf) (prog, env) (errpats, rls) of SOME _ => ()
20.59 -| NONE => error "check_error_patterns broken";
20.60 +case Error_Pattern.check_for (res, inf) (prog, env) (errpats, rls) of SOME _ => ()
20.61 +| NONE => error "Error_Pattern.check_for broken";
20.62 DEconstrCalcTree 1;
20.63
20.64 -"--------- embed fun check_error_patterns ------------------------";
20.65 -"--------- embed fun check_error_patterns ------------------------";
20.66 -"--------- embed fun check_error_patterns ------------------------";
20.67 +"--------- embed fun Error_Pattern.check_for ------------------------";
20.68 +"--------- embed fun Error_Pattern.check_for ------------------------";
20.69 +"--------- embed fun Error_Pattern.check_for ------------------------";
20.70 reset_states ();
20.71 CalcTree
20.72 [(["functionTerm (x ^ 2 + sin (x ^ 4))", "differentiateFor x", "derivative f_f'"],
20.73 @@ -1012,7 +1012,7 @@
20.74 "~~~~~ fun appendFormula' , args:"; val (cI, (ifo: Rule.cterm')) = (cI, ifo);
20.75 val cs = get_calc cI
20.76 val pos = get_pos cI 1;
20.77 -(*+*)if pos = ([1], Res) then () else error "inform with (positive) check_error_patterns broken 1";
20.78 +(*+*)if pos = ([1], Res) then () else error "inform with (positive) Error_Pattern.check_for broken 1";
20.79 val ("ok", cs' as (_, _, ptp)) = (*case*) Step.do_next pos cs (*of*);
20.80 (*case*) Step_Solve.by_term ptp (encode ifo) (*of*); (*ERROR WAS: "no derivation found"*)
20.81 "~~~~~ fun Step_Solve.by_term , args:"; val (((*next_*)cs as (_, _, (pt, pos as (p, _))): Chead.calcstate'), istr)
20.82 @@ -1037,21 +1037,21 @@
20.83 | _ => error "inform: uncovered case of get_met"
20.84 ;
20.85 (*+*)if errpats2str errpats = "[(\"chain-rule-diff-both\",\n[\"d_d ?bdv (sin ?u) = cos (d_d ?bdv ?u)\",\"d_d ?bdv (cos ?u) = - sin (d_d ?bdv ?u)\",\"d_d ?bdv (?u ^^^ ?n) = ?n * ?u ^^^ (?n - 1)\",\"d_d ?bdv (LogExp.ln ?u) = 1 / ?u\",\"d_d ?bdv (LogExp.ln ?u) = 1 / d_d ?bdv ?u\"],\n[\"d_d ?bdv (sin ?u) = cos ?u * d_d ?bdv ?u\",\"d_d ?bdv (cos ?u) = - sin ?u * d_d ?bdv ?u\",\"d_d ?bdv (?u ^^^ ?n) = ?n * ?u ^^^ (?n - 1) * d_d ?bdv ?u\",\"d_d ?bdv (LogExp.ln ?u) = d_d ?bdv ?u / ?u\",\"d_d ?bdv (E_ ^^^ ?u) = E_ ^^^ ?u * d_d ?x ?u\"]]"
20.86 -(*+*)then () else error "inform with (positive) check_error_patterns broken 3";
20.87 +(*+*)then () else error "inform with (positive) Error_Pattern.check_for broken 3";
20.88
20.89 val {env, ...} = Ctree.get_istate_LI pt pos |> Istate.the_pstate
20.90 ;
20.91 (*+*)if term2str f_pred = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))" andalso
20.92 (*+*) term2str f_in = "d_d x (x ^^^ 2) + cos (4 * x ^^^ 3)"
20.93 -(*+*)then () else error "inform with (positive) check_error_patterns broken 2";
20.94 +(*+*)then () else error "inform with (positive) Error_Pattern.check_for broken 2";
20.95
20.96 - val SOME "chain-rule-diff-both" = (*case*) Error_Pattern.check_error_patterns (f_pred, f_in) (prog, env) (errpats, nrls) (*of*);
20.97 + val SOME "chain-rule-diff-both" = (*case*) Error_Pattern.Error_Pattern.check_for (f_pred, f_in) (prog, env) (errpats, nrls) (*of*);
20.98
20.99 "--- final check:";
20.100 (*+*)val (_, _, ptp') = cs';
20.101 case Step_Solve.by_term ptp' (encode ifo) of
20.102 ("error pattern #chain-rule-diff-both#", calcstate') => ()
20.103 -| _ => error "inform with (positive) check_error_patterns broken"
20.104 +| _ => error "inform with (positive) Error_Pattern.check_for broken"
20.105
20.106
20.107 "--------- embed fun find_fillpatterns ---------------------------";
21.1 --- a/test/Tools/isac/Interpret/lucas-interpreter.sml Tue Mar 31 14:05:10 2020 +0200
21.2 +++ b/test/Tools/isac/Interpret/lucas-interpreter.sml Tue Mar 31 15:43:33 2020 +0200
21.3 @@ -152,7 +152,7 @@
21.4 = (xxx, (ist |> path_down [R]), e);
21.5 val (Program.Tac stac, a') =
21.6 (*case*) check_leaf "locate" ctxt eval (get_subst ist) t (*of*);
21.7 - val LItool.Ass (m, v', ctxt) =
21.8 + val LItool.Associated (m, v', ctxt) =
21.9 (*case*) associate pt ctxt (m, stac) (*of*);
21.10
21.11 Accept_Tac1 (ist |> set_subst_true (a', v'), ctxt, m) (*return value*);
21.12 @@ -319,7 +319,7 @@
21.13 "~~~~~ fun scan_dn1 , args:"; val (((pt, p), ctxt, tac), (ist as {eval, act_arg, or, ...}), t)
21.14 = (xxx, (ist |> path_down [R]), e);
21.15 val (Program.Tac stac, a') = (*case*) check_leaf "locate" ctxt eval (get_subst ist) t (*of*);
21.16 - val NotAss = (*case*) associate pt ctxt (tac, stac) (*of*);
21.17 + val Not_Associated = (*case*) associate pt ctxt (tac, stac) (*of*);
21.18 val ORundef = (*case*) or (*of*);
21.19 val Notappl "norm_equation not applicable" =
21.20 (*case*) Applicable.applicable_in p pt (LItool.tac_from_prog pt (Celem.assoc_thy "Isac_Knowledge") stac) (*of*);
22.1 --- a/test/Tools/isac/Knowledge/biegelinie-3.sml Tue Mar 31 14:05:10 2020 +0200
22.2 +++ b/test/Tools/isac/Knowledge/biegelinie-3.sml Tue Mar 31 15:43:33 2020 +0200
22.3 @@ -65,7 +65,7 @@
22.4 "\n (c_2 / 2 * x ^^^ 2 + c / 6 * x ^^^ 3 + -1 * q_0 / 24 * x ^^^ 4))",
22.5 "substitution (y 0 = 0)", "equality equ'''"] then ()
22.6 else error "biegelinie.sml met setzeRandbed*Ein bb";
22.7 -(writeln o istate2str) (get_istate_LI pt p);
22.8 +(writeln o Istate.string_of) (get_istate_LI pt p);
22.9 "--- after 1.subpbl [Equation, fromFunction]";
22.10
22.11 val (p,_,f,nxt,_,pt) = me nxt p c pt;
23.1 --- a/test/Tools/isac/Knowledge/diffapp.sml Tue Mar 31 14:05:10 2020 +0200
23.2 +++ b/test/Tools/isac/Knowledge/diffapp.sml Tue Mar 31 15:43:33 2020 +0200
23.3 @@ -337,7 +337,7 @@
23.4 we get at ...
23.5 val (p,_,f,nxt,_,pt) = me nxt p c pt;
23.6 ...
23.7 -### associate: NotAss m= Subproblem' ,
23.8 +### associate: Not_Associated m= Subproblem' ,
23.9 stac= Substitute
23.10 [(b, (rhs o hd)
23.11 (Subproblem (thy, [normalise, polynomial, univariate, equation])))]
24.1 --- a/test/Tools/isac/Knowledge/polyeq-1.sml Tue Mar 31 14:05:10 2020 +0200
24.2 +++ b/test/Tools/isac/Knowledge/polyeq-1.sml Tue Mar 31 15:43:33 2020 +0200
24.3 @@ -238,8 +238,8 @@
24.4 val (Program.Tac stac, a') = check_leaf "locate" thy' sr (E, (a, v)) t
24.5 val ctxt = get_ctxt pt (p,p_)
24.6 val p' = lev_on p : pos;
24.7 -(* WAS val NotAss = associate pt d (m, stac)
24.8 - ... Ass ... is correct*)
24.9 +(* WAS val Not_Associated = associate pt d (m, stac)
24.10 + ... Associated ... is correct*)
24.11 "~~~~~ fun associate, args:"; val (pt, _, (m as Check_elementwise' (consts,_,(consts_chkd,_))),
24.12 (Const ("Prog_Tac.Check'_elementwise",_) $ consts' $ _)) = (pt, d, m, stac);
24.13 term2str consts;
24.14 @@ -267,7 +267,7 @@
24.15 ([2],Res) [] Check_elementwise "Assumptions"*)
24.16 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
24.17 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
24.18 -val asm = get_assumptions_ pt p;
24.19 +val asm = Ctree.get_assumptions pt p;
24.20 if f2str f = "[]" andalso
24.21 terms2str asm = "[\"lhs (2 + -1 * x + x ^^^ 2 = 0) is_poly_in x\"," ^
24.22 "\"lhs (2 + -1 * x + x ^^^ 2 = 0) has_degree_in x = 2\"]" then ()
25.1 --- a/test/Tools/isac/Knowledge/rateq.sml Tue Mar 31 14:05:10 2020 +0200
25.2 +++ b/test/Tools/isac/Knowledge/rateq.sml Tue Mar 31 15:43:33 2020 +0200
25.3 @@ -239,7 +239,7 @@
25.4 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
25.5 val (p,_,f,nxt,_,pt) = me nxt p [] pt; f2str f = "(3 + -1 * x + x ^^^ 2) * x = 1 * (9 * x + -6 * x ^^^ 2 + x ^^^ 3)";
25.6
25.7 -(*+*)if eq_set op = (Ctree.get_assumptions_ pt p |> map term2str,
25.8 +(*+*)if eq_set op = (Ctree.get_assumptions pt p |> map term2str,
25.9 (*+*) ["x \<noteq> 0",
25.10 (*+*) "9 * x + -6 * x ^^^ 2 + x ^^^ 3 \<noteq> 0",
25.11 (*+*) "x / (x ^^^ 2 - 6 * x + 9) - 1 / (x ^^^ 2 - 3 * x) =\n1 / x is_ratequation_in x"])
25.12 @@ -284,7 +284,7 @@
25.13 (*[4, 4, 4], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; f2str f = "[x = 0, x = 6 / 5]";
25.14 (*[4, 4, 5], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*\<rightarrow>2. Check_Postcond ["bdv_only", "degree_2", "polynomial", "univariate", "equation"]*)
25.15
25.16 -(* *)if eq_set op = ((Ctree.get_assumptions_ pt p |> map term2str), [
25.17 +(* *)if eq_set op = ((Ctree.get_assumptions pt p |> map term2str), [
25.18 (*0.pre*) "x / (x ^^^ 2 - 6 * x + 9) - 1 / (x ^^^ 2 - 3 * x) =\n1 / x is_ratequation_in x",
25.19 (*1.pre*) "\<not> matches (?a = 0)\n ((3 + -1 * x + x ^^^ 2) * x =\n 1 * (9 * x + -6 * x ^^^ 2 + x ^^^ 3)) \<or>\n"
25.20 (*1.pre*) ^ "\<not> lhs ((3 + -1 * x + x ^^^ 2) * x =\n 1 * (9 * x + -6 * x ^^^ 2 + x ^^^ 3)) is_poly_in x",
25.21 @@ -305,7 +305,7 @@
25.22 (*[], Res*)val (p,_,f,nxt,_,pt) = me nxt''''' p''''' [] pt''''';(*\<rightarrow>End_Proof'*)
25.23
25.24 (*/-------- final test -----------------------------------------------------------------------\*)
25.25 -if f2str f = "[x = 6 / 5]" andalso eq_set op = (map term2str (get_assumptions_ pt p),
25.26 +if f2str f = "[x = 6 / 5]" andalso eq_set op = (map term2str (Ctree.get_assumptions pt p),
25.27 ["x = 6 / 5", "lhs (-6 * x + 5 * x ^^^ 2 = 0) is_poly_in x",
25.28 "lhs (-6 * x + 5 * x ^^^ 2 = 0) has_degree_in x = 2",
25.29 "\<not> matches (?a = 0)\n ((3 + -1 * x + x ^^^ 2) * x =\n 1 * (9 * x + -6 * x ^^^ 2 + x ^^^ 3)) \<or>\n\<not> lhs ((3 + -1 * x + x ^^^ 2) * x =\n 1 * (9 * x + -6 * x ^^^ 2 + x ^^^ 3)) is_poly_in x",
25.30 @@ -327,13 +327,13 @@
25.31 (*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(*Apply_Method ["RatEq", "solve_rat_equation"]*)
25.32 (*[1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Rewrite_Set "RatEq_simplify":*)
25.33
25.34 -(*+*)if (get_istate_LI pt p |> istate2str) (* still specify-phase: found_accept = false ---------------------------------> vvvvv*)
25.35 +(*+*)if (get_istate_LI pt p |> Istate.string_of) (* still specify-phase: found_accept = false ---------------------------------> vvvvv*)
25.36 (*+*) = "Pstate ([\"\n(e_e, 5 * x / (x - 2) - x / (x + 2) = 4)\",\"\n(v_v, x)\"], [], e_rls, NONE, \n??.empty, ORundef, false, true)"
25.37 (*+*)then () else error "rat-eq + subpbl: istate in specify-phase";
25.38
25.39 (*[1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(*Rewrite_Set "norm_Rational"*)
25.40
25.41 -(*+*)if (get_istate_LI pt p |> istate2str) (* solve-phase: found_accept = true -----------------------------------------------------------------------------------------------> vvvvv*)
25.42 +(*+*)if (get_istate_LI pt p |> Istate.string_of) (* solve-phase: found_accept = true -----------------------------------------------------------------------------------------------> vvvvv*)
25.43 (*+*) = "Pstate ([\"\n(e_e, 5 * x / (x - 2) - x / (x + 2) = 4)\",\"\n(v_v, x)\"], [R,L,R,L,L,R,R,R], e_rls, SOME e_e, \n5 * x / (x + -1 * 2) + -1 * x / (x + 2) = 4, ORundef, true, true)"
25.44 (*+*)then () else error "rat-eq + subpbl: istate after found_accept";
25.45
26.1 --- a/test/Tools/isac/Knowledge/rlang.sml Tue Mar 31 14:05:10 2020 +0200
26.2 +++ b/test/Tools/isac/Knowledge/rlang.sml Tue Mar 31 15:43:33 2020 +0200
26.3 @@ -519,7 +519,7 @@
26.4 (*val f = "[v = -1 * (f * w + -1 * u * v0 + -1 * v0 * w) / f]")) : mout
26.5 val nxt = ("Check_elementwise",Check_elementwise "Assumptions")*)
26.6
26.7 -get_assumptions_ pt p;
26.8 +Ctree.get_assumptions pt p;
26.9 (*it = ["v + w ~= 0"] ... goes to the solution as an assumption*)
26.10
26.11 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
26.12 @@ -529,7 +529,7 @@
26.13 case f of Form' (FormKF (~1,EdUndef,0,Nundef,
26.14 "[v = (u * v0 + v0 * w + -1 * f * w) / f]")) => ()
26.15 | _ => error "rlang.sml: diff.behav. in Schalk I s.89 Bsp 90a (1) [v=...]";
26.16 -if get_assumptions_ pt p =
26.17 +if Ctree.get_assumptions pt p =
26.18 [str2term"(u * v0 + v0 * w + -1 * f * w) / f + w ~= 0"] then ()
26.19 else error "rlang.sml: diff.behav. in I s.89 Bsp 90a (1) [v=...] asm";
26.20
26.21 @@ -576,7 +576,7 @@
26.22 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
26.23 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[w = (u * v0 + -1 * f * v) / (f + -1 * v0)]")) => ()
26.24 | _ => error "rlang.sml: diff.behav. in Schalk I Bsp 90a(2)";
26.25 -if get_assumptions_ pt p =
26.26 +if Ctree.get_assumptions pt p =
26.27 [str2term"v + (u * v0 + -1 * f * v) / (f + -1 * v0) ~= 0",
26.28 str2term"f + -1 * v0 ~= 0"]
26.29 then writeln "asm should be simplified ???"
26.30 @@ -621,7 +621,7 @@
26.31 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
26.32 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[R1 = R * R2 / (R2 + -1 * R)]")) => ()
26.33 | _ => error "rlang.sml: diff.behav. in 98a(1) [R1 = ...]";
26.34 -if get_assumptions_ pt p = [str2term"R * R2 * R2 ~= (R2 + -1 * R) * 0",
26.35 +if Ctree.get_assumptions pt p = [str2term"R * R2 * R2 ~= (R2 + -1 * R) * 0",
26.36 str2term"R2 + -1 * R ~= 0",
26.37 str2term"R2 + -1 * R ~= 0"]
26.38 then writeln "asm should be simplified"
26.39 @@ -655,7 +655,7 @@
26.40 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
26.41 case f of Form' (FormKF (_,_,0,_,"[p = y ^^^ 2 / (2 * x)]")) => ()
26.42 | _ => error "rlang.sml: diff.behav. in Schalk I s.89 Bsp 104a (1) [p = y^2/(2*x)]";
26.43 -if get_assumptions_ pt p = [str2term"-2 * x ~= 0"]
26.44 +if Ctree.get_assumptions pt p = [str2term"-2 * x ~= 0"]
26.45 then writeln"should be x ~= 0\nshould be x ~= 0\nshould be x ~= 0\n"
26.46 else error "rlang.sml: diff.behav. in I s.89 Bsp 104a(1) asm";
26.47
26.48 @@ -689,7 +689,7 @@
26.49 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
26.50 case f of Form' (FormKF (_,_,0,_,"[y = sqrt (2 * p * x), y = -1 * sqrt (2 * p * x)]")) => ()
26.51 | _ => error "rlang.sml: diff.behav. Schalk I s.89 Bsp 104a(2) [x = ]";
26.52 -if get_assumptions_ pt p = [str2term"0 <= -1 * (-2 * p * x)",
26.53 +if Ctree.get_assumptions pt p = [str2term"0 <= -1 * (-2 * p * x)",
26.54 str2term"0 <= -1 * (-2 * p * x)"]
26.55 then writeln "asm should be simplified\nshould be simplified"
26.56 else error "rlang.sml: diff.behav. in I s.89 Bsp 104a(2) asm";
26.57 @@ -726,18 +726,18 @@
26.58 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
26.59 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
26.60 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;f2str f;
26.61 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;f2str f;get_assumptions_ pt p;
26.62 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;f2str f;get_assumptions_ pt p;
26.63 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;f2str f;get_assumptions_ pt p;
26.64 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;f2str f;get_assumptions_ pt p;
26.65 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;f2str f;terms2str (*WN1104changed*) (get_assumptions_ pt p);
26.66 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;f2str f;terms2str (*WN1104changed*) (get_assumptions_ pt p);
26.67 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;f2str f;Ctree.get_assumptions pt p;
26.68 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;f2str f;Ctree.get_assumptions pt p;
26.69 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;f2str f;Ctree.get_assumptions pt p;
26.70 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;f2str f;Ctree.get_assumptions pt p;
26.71 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;f2str f;terms2str (*WN1104changed*) (Ctree.get_assumptions pt p);
26.72 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;f2str f;terms2str (*WN1104changed*) (Ctree.get_assumptions pt p);
26.73
26.74 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;f2str f;get_assumptions_ pt p;
26.75 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;f2str f;get_assumptions_ pt p;
26.76 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;f2str f;Ctree.get_assumptions pt p;
26.77 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;f2str f;Ctree.get_assumptions pt p;
26.78 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = sqrt ((a ^^^ 2 * b ^^^ 2 + -1 * a ^^^ 2 * y ^^^ 2) / b ^^^ 2),\n x = -1 * sqrt ((a ^^^ 2 * b ^^^ 2 + -1 * a ^^^ 2 * y ^^^ 2) / b ^^^ 2)]")) => writeln"should be simplified MG"
26.79 | _ => error "rlang.sml: diff.behav. in Schalk I s.89 Bsp 118a(2) [x = ]";
26.80 -val asms = get_assumptions_ pt p;
26.81 +val asms = Ctree.get_assumptions pt p;
26.82 if asms =
26.83 [str2term"0 * b ^^^ 2 <= -1 * (a ^^^ 2 * y ^^^ 2 + -1 * a ^^^ 2 * b ^^^ 2)",
26.84 str2term"b ^^^ 2 ~= 0",
26.85 @@ -774,7 +774,7 @@
26.86 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
26.87 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x2 =\n (-2 * A + x1 * y2 + x3 * y1 + -1 * x1 * y3 + -1 * x3 * y2) /\n (y1 + -1 * y3)]")) => ()
26.88 | _ => error "rlang.sml: diff.behav. Schalk I s.102 Bsp 268(1) [x2=...]";
26.89 -if get_assumptions_ pt p = [str2term"y1 / 2 + -1 * y3 / 2 ~= 0"] then ()
26.90 +if Ctree.get_assumptions pt p = [str2term"y1 / 2 + -1 * y3 / 2 ~= 0"] then ()
26.91 else error "rlang.sml: diff.behav. in I s.102 Bsp 268(1) asm";
26.92
26.93 (*-------------------- Schalk II ----------------------------*)
26.94 @@ -857,7 +857,7 @@
26.95 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
26.96 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
26.97 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
26.98 -get_assumptions_ pt p;
26.99 +Ctree.get_assumptions pt p;
26.100 (* val nxt = ("Model_Problem", Model_Problem ["normalise","polynomial","univariate","equation"])*)
26.101 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
26.102 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
26.103 @@ -869,7 +869,7 @@
26.104 (~1, EdUndef, 0, Nundef, "256 + -2368 * x + 576 * x ^^^ 2 = 0"))then()
26.105 else error "rlang.sml: diff.behav. in Schalk II s.56 Bsp 68a";
26.106 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
26.107 -get_assumptions_ pt p;
26.108 +Ctree.get_assumptions pt p;
26.109 (* val nxt = ("Model_Problem", Model_Problem
26.110 ["abcFormula","degree_2","polynomial","univariate","equation"])*)
26.111 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
26.112 @@ -878,7 +878,7 @@
26.113 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
26.114 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
26.115 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
26.116 -get_assumptions_ pt p;
26.117 +Ctree.get_assumptions pt p;
26.118 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
26.119 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
26.120 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
26.121 @@ -886,7 +886,7 @@
26.122 if f = Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 4, x = 1 / 9]"))
26.123 then writeln "only [x = 4] !\nonly [x = 4] !\nonly [x = 4] !\n"
26.124 else error "rlang.sml: diff.behav. in II 68a";
26.125 -val asms = get_assumptions_ pt p;
26.126 +val asms = Ctree.get_assumptions pt p;
26.127 if terms2str (*WN1104changed*) asms =
26.128 "[0 <= (25 * (1 / 9) + -1 * (16 + 49 * (1 / 9))) * -56,\
26.129 \0 <= 1 / 9,\
26.130 @@ -951,7 +951,7 @@
26.131 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
26.132 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
26.133 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
26.134 -val asm = get_assumptions_ pt p;
26.135 +val asm = Ctree.get_assumptions pt p;
26.136 if asm=[] andalso f = Form' (FormKF (~1,EdUndef,0,Nundef,"UniversalList")) andalso nxt = ("End_Proof'",End_Proof') then ()
26.137 else error "rlang.sml: diff.behav. in UniversalList 2";
26.138
26.139 @@ -1584,7 +1584,7 @@
26.140 if f = Form' (FormKF (~1,EdUndef,0,Nundef,
26.141 "[x = (-2 * a + 4 * b + sqrt (16 * a * b + 16 * b ^^^ 2 + 4 * a ^^^ 2)) / 4,\n x =\n (-2 * a + 4 * b + -1 * sqrt (16 * a * b + 16 * b ^^^ 2 + 4 * a ^^^ 2)) / 4]")) then writeln "simplify MG"
26.142 else error "rlang.sml: diff.behav. in II 62b [x=...]";
26.143 -val asms = get_assumptions_ pt p;
26.144 +val asms = Ctree.get_assumptions pt p;
26.145 if asms = [str2term"0 <= ((-2 * a + 4 * b + sqrt (16 * a * b + 16 * b ^^^ 2 + 4 * a ^^^ 2)) / 4 + a) ^^^ 2 + ((-2 * a + 4 * b + sqrt (16 * a * b + 16 * b ^^^ 2 + 4 * a ^^^ 2)) / 4 - 2 * b) ^^^ 2",
26.146 str2term"0 <= a + 2 * b",
26.147 str2term"8 * (-4 * a * b) <= (-4 * b + 2 * a) ^^^ 2",
26.148 @@ -1683,7 +1683,7 @@
26.149 "[a = sqrt ((-1 * b ^^^ 2 + 4 * r ^^^ 2) / 1),\n a = -1 * sqrt ((-1 * b ^^^ 2 + 4 * r ^^^ 2) / 1)]")) andalso nxt = ("End_Proof'",End_Proof')
26.150 then writeln"simplify result\nsimplify result\nsimplify result"
26.151 else error "rlang.sml: diff.behav. in Pythagoras";
26.152 -val asms = get_assumptions_ pt p;
26.153 +val asms = Ctree.get_assumptions pt p;
26.154 (*if asms = [str2term"0 <= -4 * (b ^^^ 2 / 4 + -4 * r ^^^ 2 / 4)",
26.155 str2term"0 <= -4 * (b ^^^ 2 / 4 + -4 * r ^^^ 2 / 4)"]*)
26.156 if terms2str (*WN1104changed*) asms =
27.1 --- a/test/Tools/isac/Knowledge/rooteq.sml Tue Mar 31 14:05:10 2020 +0200
27.2 +++ b/test/Tools/isac/Knowledge/rooteq.sml Tue Mar 31 15:43:33 2020 +0200
27.3 @@ -134,7 +134,7 @@
27.4 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
27.5 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 1 / 25]")) => ()
27.6 | _ => error "rooteq.sml: diff.behav. [x = 1 / 25]";
27.7 -if terms2str (*WN1104changed*) (get_assumptions_ pt p) = "[0 <= 1 / 25]"
27.8 +if terms2str (*WN1104changed*) (Ctree.get_assumptions pt p) = "[0 <= 1 / 25]"
27.9 (*WN050916 before correction 'rewrite__set_ called with 'Erls' for ..:
27.10 [(str2term"25 ~= 0",[])] *)
27.11 then writeln "should be True\n\
27.12 @@ -207,7 +207,7 @@
27.13 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
27.14 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 4]")) => ()
27.15 | _ => error "rooteq.sml: diff.behav. [x = 4]";
27.16 -if get_assumptions_ pt p = [str2term"0 <= 12 * sqrt 2 * 4"]
27.17 +if Ctree.get_assumptions pt p = [str2term"0 <= 12 * sqrt 2 * 4"]
27.18 then writeln "should be True\nshould be True\nshould be True\n\
27.19 \should be True\nshould be True\nshould be True\n"
27.20 else error "rooteq.sml: diff.behav. with 0 <= 12 * sqrt 2 * 4";
27.21 @@ -257,7 +257,7 @@
27.22 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
27.23 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
27.24 val (p,_,f,nxt,_,pt) = me nxt p c pt;
27.25 -val asm = get_assumptions_ pt p;
27.26 +val asm = Ctree.get_assumptions pt p;
27.27 if f = Form' (FormKF (~1,EdUndef,0,Nundef,"UniversalList")) andalso asm = []
27.28 then () else error "rooteq.sml: diff.behav. in UniversalList 1";
27.29
28.1 --- a/test/Tools/isac/MathEngine/mathengine-stateless.sml Tue Mar 31 14:05:10 2020 +0200
28.2 +++ b/test/Tools/isac/MathEngine/mathengine-stateless.sml Tue Mar 31 15:43:33 2020 +0200
28.3 @@ -258,7 +258,7 @@
28.4 ^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
28.5 "~~~~~ fun cappend_atomic, args:"; val (pt, p, ist_res, f, r, f', s) =
28.6 (pt, p, (is, ContextC.insert_assumptions asm ctxt), f, (Rewrite thm'), (f',asm), Complete);
28.7 -existpt p pt andalso is_empty_tac (get_obj g_tac pt p) = false;
28.8 +existpt p pt andalso Tactic.is_empty (get_obj g_tac pt p) = false;
28.9 apfst (append_atomic p ist_res f r f' s) (cut_tree pt (p,Frm));
28.10 apfst : ('a -> 'b) -> 'a * 'c -> 'b * 'c;
28.11 (append_atomic p ist_res f r f' s) : ctree -> ctree;
29.1 --- a/test/Tools/isac/Minisubpbl/250-Rewrite_Set-from-method.sml Tue Mar 31 14:05:10 2020 +0200
29.2 +++ b/test/Tools/isac/Minisubpbl/250-Rewrite_Set-from-method.sml Tue Mar 31 15:43:33 2020 +0200
29.3 @@ -78,7 +78,7 @@
29.4 "~~~~~ fun scan_dn1 , args:"; val (((pt, p), ctxt, tac), (ist as {env, eval, or, ...}), t) =
29.5 (xxx, (ist |> path_down_form ([L, R], a)), e);
29.6 val (Program.Tac stac, a') = (*case*) check_leaf "locate" ctxt eval (get_subst ist) t (*of*);
29.7 -val Ass (Rewrite_Set' _, _, _) = (*case*)
29.8 +val Associated (Rewrite_Set' _, _, _) = (*case*)
29.9 associate pt ctxt (m, stac) (*of*);
29.10 "~~~~~ fun associate, args:"; val (_, ctxt, (m as Tactic.Rewrite_Set' (_, _, rls, f, (f', _))),
29.11 (Const ("Prog_Tac.Rewrite'_Set", _) $ rls_ $ f_)) = (pt, d, m, stac);
30.1 --- a/test/Tools/isac/Minisubpbl/490-nxt-Check_Postcond.sml Tue Mar 31 14:05:10 2020 +0200
30.2 +++ b/test/Tools/isac/Minisubpbl/490-nxt-Check_Postcond.sml Tue Mar 31 15:43:33 2020 +0200
30.3 @@ -65,7 +65,7 @@
30.4 (*OLD* ) vvv--- handled by ctxt \<rightarrow> drop ( *OLD*)
30.5 (*OLD*)val asm = (*?!? Rfun,Rrls rm case*)(case get_obj g_tac pt p of
30.6 (*OLD*) Tactic.Check_elementwise _ => (snd o (get_obj g_result pt)) p
30.7 -(*OLD*) | _ => get_assumptions_ pt pos);
30.8 +(*OLD*) | _ => Ctree.get_assumptions pt pos);
30.9 (*OLD* )val tac = Tactic.Check_Postcond' (pI, (prog_res, asm))
30.10 ( *OLD*)
30.11
31.1 --- a/test/Tools/isac/Minisubpbl/600-postcond-NEXT_STEP.sml Tue Mar 31 14:05:10 2020 +0200
31.2 +++ b/test/Tools/isac/Minisubpbl/600-postcond-NEXT_STEP.sml Tue Mar 31 15:43:33 2020 +0200
31.3 @@ -110,7 +110,7 @@
31.4 val thy' = get_obj g_domID pt (par_pblobj pt p);
31.5 val ((ist, ctxt), sc) = LItool.resume_prog thy' (p,p_) pt;
31.6
31.7 -(*+*)istate2str ist
31.8 +(*+*)Istate.string_of ist
31.9 = "Pstate ([\"\n(e_e, -1 + x = 0)\",\"\n(v_v, x)\",\"\n(L_L, [x = 1])\"], [R,R,D,R,D], e_rls, NONE, \n[x = 1],"
31.10 ^ " ORundef, true, false)"; (*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~true ok*)
31.11
32.1 --- a/test/Tools/isac/Minisubpbl/800-append-on-Frm.sml Tue Mar 31 14:05:10 2020 +0200
32.2 +++ b/test/Tools/isac/Minisubpbl/800-append-on-Frm.sml Tue Mar 31 15:43:33 2020 +0200
32.3 @@ -72,14 +72,14 @@
32.4 "~~~~~ fun cappend_atomic , args:"; val (pt, p: pos, ic_res, f, r, f', s)
32.5 = (pt, p, (is, ContextC.insert_assumptions asm ctxt), f,
32.6 (Tactic.Rewrite_Set (Rule.id_rls rls')), (f',asm), Complete);
32.7 - (*if*) existpt p pt andalso Tactic.is_empty_tac (get_obj g_tac pt p) (*then*);
32.8 + (*if*) existpt p pt andalso Tactic.is_empty (get_obj g_tac pt p) (*then*);
32.9 val (ic_form, f) = (get_loc pt (p, Frm), get_obj g_form pt p)
32.10 val (pt, cs) = cut_tree(*!*)pt (p, Frm);
32.11 (** )val pt = ( **)
32.12 append_atomic p (SOME ic_form, ic_res) f r f' s pt;
32.13 "~~~~~ fun append_atomic , args:"; val (p, (ic_form, ic_res), f, r, f', s, pt)
32.14 = (p, (SOME ic_form, ic_res), f, r, f', s, pt);
32.15 - (*if*) existpt p pt andalso Tactic.is_empty_tac (get_obj g_tac pt p) (*else*);
32.16 + (*if*) existpt p pt andalso Tactic.is_empty (get_obj g_tac pt p) (*else*);
32.17 val (iss, f) =
32.18 ((ic_form, SOME ic_res), f); (*return from if*)
32.19
32.20 @@ -100,7 +100,7 @@
32.21 andalso
32.22 (ctxt_res |> get_assumptions |> terms2str) = "[\"precond_rootmet x\"]"
32.23 andalso
32.24 - istate2str ist_res =
32.25 + Istate.string_of ist_res =
32.26 "Pstate ([\"\n(e_e, x + 1 = 2)\",\"\n(v_v, x)\"], [], e_rls, NONE, \n2 + -1 + x = 2, ORundef, false, true)"
32.27 then () else error "/800-append-on-Frm.sml CHANGED";
32.28
33.1 --- a/test/Tools/isac/OLDTESTS/root-equ.sml Tue Mar 31 14:05:10 2020 +0200
33.2 +++ b/test/Tools/isac/OLDTESTS/root-equ.sml Tue Mar 31 15:43:33 2020 +0200
33.3 @@ -362,7 +362,7 @@
33.4
33.5 val pos = lev_up pos;
33.6 val (pt,pos) = append_result pt pos e_istate (str2term ct,[]) Complete;
33.7 -get_assumptions_ pt ([],Res);
33.8 +Ctree.get_assumptions pt ([],Res);
33.9
33.10 writeln (pr_ctree pr_short pt);
33.11 (* aus src.24-11-99:
34.1 --- a/test/Tools/isac/OLDTESTS/scriptnew.sml Tue Mar 31 14:05:10 2020 +0200
34.2 +++ b/test/Tools/isac/OLDTESTS/scriptnew.sml Tue Mar 31 15:43:33 2020 +0200
34.3 @@ -400,12 +400,12 @@
34.4 val (p,_,f,nxt,_,pt) = me nxt p c pt;
34.5 (*val nxt = "square_equation_left",
34.6 "[| 0 <= ?a; 0 <= ?b |] ==> (sqrt ?a = ?b) = (?a = ?b ^^^ 2)"))*)
34.7 -get_assumptions_ pt p;
34.8 +Ctree.get_assumptions pt p;
34.9 (*it = [] : string list;*)
34.10 trace_rewrite := false;
34.11 val (p,_,f,nxt,_,pt) = me nxt p c pt;
34.12 trace_rewrite := false;
34.13 -val asms = get_assumptions_ pt p;
34.14 +val asms = Ctree.get_assumptions pt p;
34.15 if asms = [(str2term "0 <= 9 + 4 * x",[1]),
34.16 (str2term "0 <= x",[1]),
34.17 (str2term "0 <= -3 + x",[1])] then ()
34.18 @@ -414,10 +414,10 @@
34.19 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
34.20 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
34.21 (*val nxt = Rewrite ("square_equation_left", *)
34.22 -val asms = get_assumptions_ pt p;
34.23 +val asms = Ctree.get_assumptions pt p;
34.24 [("0 <= 9 + 4 * x",[1]),("0 <= x",[1]),("0 <= -3 + x",[1])];
34.25 val (p,_,f,nxt,_,pt) = me nxt p c pt;
34.26 -val asms = get_assumptions_ pt p;
34.27 +val asms = Ctree.get_assumptions pt p;
34.28 if asms = [(str2term "0 <= 9 + 4 * x",[1]),
34.29 (str2term "0 <= x",[1]),
34.30 (str2term "0 <= -3 + x",[1]),
34.31 @@ -438,13 +438,13 @@
34.32 val (p,_,f,nxt,_,pt) = me nxt p c pt;
34.33 (*val nxt =
34.34 ("Check_Postcond",Check_Postcond ["LINEAR","univariate","equation","test"])*)
34.35 -val asms = get_assumptions_ pt p;
34.36 +val asms = Ctree.get_assumptions pt p;
34.37 if asms = [] then ()
34.38 else error "scriptnew.sml diff.behav. in sqrt assumptions 3";
34.39 val (p,_,f,nxt,_,pt) = me nxt p c pt;
34.40 (*val nxt = ("Check_elementwise",Check_elementwise "Assumptions")*)
34.41
34.42 -val asms = get_assumptions_ pt p;
34.43 +val asms = Ctree.get_assumptions pt p;
34.44 if asms = [(str2term "0 <= 9 + 4 * x",[1]),
34.45 (str2term "0 <= x",[1]),
34.46 (str2term "0 <= -3 + x",[1]),
34.47 @@ -455,7 +455,7 @@
34.48
34.49 val (p,_,f,nxt,_,pt) = me nxt p c pt;
34.50 (*val nxt = Check_Postcond ["sqroot-test","univariate","equation","test"])*)
34.51 -val asms = get_assumptions_ pt p;
34.52 +val asms = Ctree.get_assumptions pt p;
34.53 [("0 <= 9 + 4 * x",[1]),("0 <= x",[1]),("0 <= -3 + x",[1]),
34.54 ("0 <= x ^^^ 2 + -3 * x",[6]),("0 <= 6 + x",[6]),
34.55 ("0 <= 6 + -12 / 5 &\n0 <= (-12 / 5) ^^^ 2 + -3 * (-12 / 5) &\n0 <= -3 + -12 / 5 & 0 <= -12 / 5 & 0 <= 9 + 4 * (-12 / 5)",
34.56 @@ -468,7 +468,7 @@
34.57 then writeln("there should be L = []\nthere should be L = []\nthere should be L = []\nthere should be L = []\nthere should be L = []\n")
34.58 else error "diff.behav. in scriptnew.sml; root-eq: L = []";
34.59
34.60 -val asms = get_assumptions_ pt p;
34.61 +val asms = Ctree.get_assumptions pt p;
34.62 if asms = [(str2term "0 <= 9 + 4 * (-12 / 5)",[]),
34.63 (str2term "0 <= -12 / 5", []),
34.64 (str2term "0 <= -3 + -12 / 5", []),