1.1 --- a/ROOTS Tue Feb 04 16:45:36 2020 +0100
1.2 +++ b/ROOTS Tue Feb 04 17:11:54 2020 +0100
1.3 @@ -11,5 +11,4 @@
1.4 src/Doc
1.5 src/Tools
1.6 src/Tools/isac
1.7 -src/Tools/isac/Interpret
1.8 test/Tools/isac/ADDTESTS/session-get_theory/
1.9 \ No newline at end of file
2.1 --- a/src/Tools/isac/BridgeLibisabelle/interface.sml Tue Feb 04 16:45:36 2020 +0100
2.2 +++ b/src/Tools/isac/BridgeLibisabelle/interface.sml Tue Feb 04 17:11:54 2020 +0100
2.3 @@ -205,11 +205,11 @@
2.4 @see #TACTICS_ALL
2.5 @see #TACTICS_CURRENT_THEORY
2.6 @see #TACTICS_CURRENT_METHOD ..the only impl.WN040307
2.7 - Lucin.sel_appl_atomic_tacs waits to be used here
2.8 + LItool.sel_appl_atomic_tacs waits to be used here
2.9 *)
2.10 fun fetchApplicableTactics cI (_(*scope*): int) (p : pos') =
2.11 (let val ((pt, _), _) = get_calc cI
2.12 - in (applicabletacticsOK cI (Lucin.sel_rules pt p))
2.13 + in (applicabletacticsOK cI (LItool.sel_rules pt p))
2.14 handle PTREE str => sysERROR2xml cI str
2.15 end)
2.16 handle _ => sysERROR2xml cI "error in kernel 5";
3.1 --- a/src/Tools/isac/Interpret/Interpret.thy Tue Feb 04 16:45:36 2020 +0100
3.2 +++ b/src/Tools/isac/Interpret/Interpret.thy Tue Feb 04 17:11:54 2020 +0100
3.3 @@ -9,7 +9,7 @@
3.4 (* removed all warnings here, only "handle _" remains *)
3.5 ML_file istate.sml
3.6 ML_file rewtools.sml
3.7 - ML_file script.sml
3.8 + ML_file "li-tool.sml"
3.9 ML_file inform.sml
3.10 ML_file "lucas-interpreter.sml"
3.11 ML_file "step-solve.sml"
4.1 --- a/src/Tools/isac/Interpret/ROOT Tue Feb 04 16:45:36 2020 +0100
4.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
4.3 @@ -1,12 +0,0 @@
4.4 -(* run "./bin/isabelle build -v -b Lucin" *)
4.5 -session Lucin in "~~/src/Tools/isac/Interpret" = HOL +
4.6 - description \<open>
4.7 - Lucas Interpretation
4.8 -
4.9 - This is for code references by the IJCAR paper
4.10 - "Lucas-Interpretation on Isabelle’s Functions"
4.11 - and meant as a first step towards documentation.
4.12 - \<close>
4.13 - options [document = false (*, browser_info = true*)]
4.14 - theories
4.15 - Interpret
5.1 --- a/src/Tools/isac/Interpret/inform.sml Tue Feb 04 16:45:36 2020 +0100
5.2 +++ b/src/Tools/isac/Interpret/inform.sml Tue Feb 04 17:11:54 2020 +0100
5.3 @@ -13,7 +13,7 @@
5.4 val input_icalhd : Ctree.ctree -> icalhd -> Ctree.ctree * Ctree.ocalhd
5.5 val find_fillpatterns : Calc.T -> Rule.errpatID -> (Celem.fillpatID * term * thm * Selem.subs option) list
5.6 val is_exactly_equal : Calc.T -> string -> string * Tactic.input
5.7 -(*cp here from "! aktivate for Test_Isac" below due to LucinNEW*)
5.8 +(*cp here from "! aktivate for Test_Isac" below due to Lucin*)
5.9 val concat_deriv : 'a * ((term * term) list -> term * term -> bool) ->
5.10 Rule.rls -> Rule.rule list -> term -> term -> bool * (term * Rule.rule * (term * term list)) list
5.11 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))
5.12 @@ -339,10 +339,10 @@
5.13
5.14 fun mk_tacis ro erls (t, r as Rule.Thm (id, thm), (t', a)) =
5.15 (Tactic.Rewrite (id, thm),
5.16 - Tactic.Rewrite' ("Isac_Knowledge", fst ro, erls, false, Lucin.rule2thm'' r, t, (t', a)),
5.17 + Tactic.Rewrite' ("Isac_Knowledge", fst ro, erls, false, LItool.rule2thm'' r, t, (t', a)),
5.18 (Pos.e_pos'(*to be updated before generate tacis!!!*), (Istate.Uistate, ContextC.e_ctxt)))
5.19 | mk_tacis _ _ (t, r as Rule.Rls_ rls, (t', a)) =
5.20 - (Tactic.Rewrite_Set (Lucin.rule2rls' r),
5.21 + (Tactic.Rewrite_Set (LItool.rule2rls' r),
5.22 Tactic.Rewrite_Set' ("Isac_Knowledge", false, rls, t, (t', a)),
5.23 (Pos.e_pos'(*to be updated before generate tacis!!!*), (Istate.Uistate, ContextC.e_ctxt)))
5.24 | mk_tacis _ _ (t, r, _) = error ("mk_tacis: not impl. for " ^ Rule.rule2str r ^ " at " ^ Rule.term2str t)
6.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
6.2 +++ b/src/Tools/isac/Interpret/li-tool.sml Tue Feb 04 17:11:54 2020 +0100
6.3 @@ -0,0 +1,622 @@
6.4 +(* Title: interpreter for scripts
6.5 + Author: Walther Neuper 2000
6.6 + (c) due to copyright terms
6.7 +*)
6.8 +
6.9 +signature LUCAS_INTERPRETER_TOOL =
6.10 +sig
6.11 +
6.12 + type step = Tactic.T * Generate.mout * Ctree.ctree * Ctree.pos' * Ctree.pos' list
6.13 + datatype ass =
6.14 + Ass of Tactic.T * term * Proof.context
6.15 + | Ass_Weak of Tactic.T * term * Proof.context
6.16 + | NotAss;
6.17 + val associate: Ctree.ctree -> Proof.context -> (Tactic.T * term) -> ass
6.18 +
6.19 + val sel_rules : Ctree.ctree -> Ctree.pos' -> Tactic.input list
6.20 + val init_form : 'a -> Program.T -> (term * term) list -> term option
6.21 + val init_pstate : Rule.rls -> Proof.context -> Model.itm list -> Celem.metID -> Istate.T * Proof.context * Program.T
6.22 +
6.23 + val get_simplifier : Calc.T -> Rule.rls
6.24 +(*DEPR ^*)val from_pblobj' : Rule.theory' -> Ctree.pos' -> Ctree.ctree ->
6.25 + Rule.rls(*..\<in> ist*) * (Istate.T * Proof.context) * Program.T
6.26 +(*DEPR*)val from_pblobj_or_detail' : Rule.theory' -> Ctree.pos' -> Ctree.ctree ->
6.27 + Rule.rls(*..\<in> ist*) * (Istate.T * Proof.context) * Program.T
6.28 + val rule2thm'' : Rule.rule -> Celem.thm''
6.29 + val rule2rls' : Rule.rule -> string
6.30 + val sel_appl_atomic_tacs : Ctree.ctree -> Ctree.pos' -> Tactic.input list
6.31 +(*cp here from "! aktivate for Test_Isac" below due to Lucin*)
6.32 + val stac2tac_ : Ctree.ctree -> theory -> term -> Tactic.input * Tactic.T
6.33 + val stac2tac : Ctree.ctree -> theory -> term -> Tactic.input
6.34 + val rew_only: (Tactic.T * Generate.mout * Ctree.ctree * Ctree.pos' * Ctree.pos' list) list -> bool
6.35 + val check_leaf : (*TODO190625: shift to lucas-interpreter.sml ? <- sel_rules, sel_appl_atomic_tacs !*)
6.36 + string -> Proof.context -> Rule.rls -> (Env.T * (term option * term)) -> term ->
6.37 + Program.leaf * term option
6.38 +
6.39 +(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
6.40 + (*NONE*)
6.41 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
6.42 + val is_spec_pos : Ctree.pos_ -> bool
6.43 + val itms2args : 'a -> Celem.metID -> Model.itm list -> term list
6.44 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
6.45 +
6.46 +end
6.47 +
6.48 +(* traces the leaves (ie. non-tactical nodes) of Prog found by find_next_step, see "and scr" *)
6.49 +val trace_script = Unsynchronized.ref false; (* TODO: how are traces done in Isabelle? *)
6.50 +
6.51 +(**)
6.52 +structure LItool(**): LUCAS_INTERPRETER_TOOL(**) =
6.53 +struct
6.54 +(**)
6.55 +open Ctree
6.56 +open Pos
6.57 +(*TODO open Celem for L,R,D;
6.58 + the few other Celem.items are acceptable: metID, e_metID, assoc_thy, metID2str, thm''*)
6.59 +
6.60 +(**)
6.61 +(* data for creating a new node in ctree; designed for use as:
6.62 + fun ass* pstate steps = / ... case ass* pstate steps of /
6.63 + Accept_Tac1 (pstate, steps) => ... ass* pstate steps *)
6.64 +type step = (*WN190713 REMOVE: "creating a new node" was never implemented for more than one node?!?
6.65 + WN190713 COMPARE: taci list, see papernote #139 *)
6.66 + Tactic.T (*transformed from associated tac *)
6.67 + * Generate.mout (*result with indentation etc. *)
6.68 + * ctree (*containing node created by tac_ + resp. pstate *)
6.69 + * pos' (*position in ctree; ctree * pos' is the proofstate *)
6.70 + * pos' list; (*of ctree-nodes probably cut (by fst tac_)
6.71 + WN190713 COMPARE: pos' list also in calcstate'*)
6.72 +
6.73 +fun rule2thm'' (Rule.Thm (id, thm)) = (id, thm)
6.74 + | rule2thm'' r = error ("rule2thm': not defined for " ^ Rule.rule2str r);
6.75 +fun rule2rls' (Rule.Rls_ rls) = Rule.id_rls rls
6.76 + | rule2rls' r = error ("rule2rls': not defined for " ^ Rule.rule2str r);
6.77 +
6.78 +(*check if there are tacs for rewriting only*)
6.79 +fun rew_only ([]:step list) = true
6.80 + | rew_only (((Tactic.Rewrite' _ ,_,_,_,_))::ss) = rew_only ss
6.81 + | rew_only (((Tactic.Rewrite_Inst' _ ,_,_,_,_))::ss) = rew_only ss
6.82 + | rew_only (((Tactic.Rewrite_Set' _ ,_,_,_,_))::ss) = rew_only ss
6.83 + | rew_only (((Tactic.Rewrite_Set_Inst' _ ,_,_,_,_))::ss) = rew_only ss
6.84 + | rew_only (((Tactic.Calculate' _ ,_,_,_,_))::ss) = rew_only ss
6.85 + | rew_only (((Tactic.Begin_Trans' _ ,_,_,_,_))::ss) = rew_only ss
6.86 + | rew_only (((Tactic.End_Trans' _ ,_,_,_,_))::ss) = rew_only ss
6.87 + | rew_only _ = false;
6.88 +
6.89 +(* functions for the environment stack: NOT YET IMPLEMENTED
6.90 +fun accessenv id es = the (assoc ((top es) : Env.update, id))
6.91 + handle _ => error ("accessenv: " ^ free2str id ^ " not in Env.update");
6.92 +fun updateenv id vl (es : Env.update stack) =
6.93 + (push (overwrite(top es, (id, vl))) (pop es)) : Env.update stack;
6.94 +fun pushenv id vl (es : Env.update stack) =
6.95 + (push (overwrite(top es, (id, vl))) es) : Env.update stack;
6.96 +val popenv = pop : Env.update stack -> Env.update stack;
6.97 +*)
6.98 +
6.99 +fun de_esc_underscore str =
6.100 + let
6.101 + fun scan [] = []
6.102 + | scan (s :: ss) = if s = "'" then (scan ss) else (s :: (scan ss))
6.103 + in (implode o scan o Symbol.explode) str end;
6.104 +
6.105 +fun init_form thy (Rule.Prog sc) env =
6.106 + (case Prog_Tac.get_stac thy sc of NONE => NONE | SOME stac => SOME (subst_atomic env stac))
6.107 + | init_form _ _ _ = error "init_form: no match";
6.108 +
6.109 +type dsc = typ; (* <-> nam..unknow in Descript.thy *)
6.110 +
6.111 +(*.create the actual parameters (args) of script: their order
6.112 + is given by the order in met.pat .*)
6.113 +(*WN.5.5.03: ?: does this allow for different descriptions ???
6.114 + ?: why not taken from formal args of script ???
6.115 +!: FIXXXME penv: push it here in itms2args into script-evaluation*)
6.116 +val errmsg = "ERROR: the guard is missing (#ppc in 'type met' added in prep_met)."
6.117 +fun errmsg2 d itms = ("itms2args: '" ^ Rule.term2str d ^ "' not in itms:\n" ^
6.118 +"itms:\n" ^ Model.itms2str_ @{context} itms)
6.119 +fun itms2args _ mI itms =
6.120 + let
6.121 + val mvat = Model.max_vt itms
6.122 + fun okv mvat (_, vats, b, _, _) = member op = vats mvat andalso b
6.123 + val itms = filter (okv mvat) itms
6.124 + fun test_dsc d (_, _, _, _, itm_) = (d = Model.d_in itm_)
6.125 + fun itm2arg itms (_,(d,_)) =
6.126 + case find_first (test_dsc d) itms of
6.127 + NONE => raise ERROR (errmsg2 d itms)
6.128 + | SOME (_, _, _, _, itm_) => Model.penvval_in itm_
6.129 + (*| SOME (_,_,_,_,itm_) => mk_arg thy (Model.d_in itm_) (ts_in itm_);
6.130 + penv postponed; presently penv holds already Env.update for script*)
6.131 + val pats = (#ppc o Specify.get_met) mI
6.132 + val _ = if pats = [] then raise ERROR errmsg else ()
6.133 + in (flat o (map (itm2arg itms))) pats end;
6.134 +
6.135 +(* convert a script-tac 'stac' to 'tac' for users;
6.136 + for "Prog_Tac.SubProblem" also create a 'tac_' for internal use. FIXME separate?
6.137 + if stac is an initac, then convert to a 'tac_' (as required in scan_dn).
6.138 + arg ctree for pushing the thy specified in rootpbl into subpbls *)
6.139 +fun stac2tac_ _ thy (Const ("Prog_Tac.Rewrite", _) $ thmID $ _) =
6.140 + let
6.141 + val tid = HOLogic.dest_string thmID
6.142 + in (Tactic.Rewrite (tid, Rewrite.assoc_thm'' thy tid), Tactic.Empty_Tac_) end
6.143 + | stac2tac_ _ thy (Const ("Prog_Tac.Rewrite'_Inst", _) $ sub $ thmID $ _) =
6.144 + let
6.145 + val tid = HOLogic.dest_string thmID
6.146 + in (Tactic.Rewrite_Inst (Selem.subst'_to_sube sub, (tid, Rewrite.assoc_thm'' thy tid)), Tactic.Empty_Tac_) end
6.147 + | stac2tac_ _ _ (Const ("Prog_Tac.Rewrite'_Set",_) $ rls $ _) =
6.148 + (Tactic.Rewrite_Set (HOLogic.dest_string rls), Tactic.Empty_Tac_)
6.149 + | stac2tac_ _ _ (Const ("Prog_Tac.Rewrite'_Set'_Inst", _) $ sub $ rls $ _) =
6.150 + (Tactic.Rewrite_Set_Inst (Selem.subst'_to_sube sub, HOLogic.dest_string rls), Tactic.Empty_Tac_)
6.151 + | stac2tac_ _ _ (Const ("Prog_Tac.Calculate", _) $ op_ $ _) =
6.152 + (Tactic.Calculate (HOLogic.dest_string op_), Tactic.Empty_Tac_)
6.153 + | stac2tac_ _ _ (Const ("Prog_Tac.Take", _) $ t) = (Tactic.Take (Rule.term2str t), Tactic.Empty_Tac_)
6.154 + | stac2tac_ _ _ (Const ("Prog_Tac.Substitute", _) $ isasub $ _) =
6.155 + (Tactic.Substitute ((Selem.subte2sube o TermC.isalist2list) isasub), Tactic.Empty_Tac_)
6.156 + | stac2tac_ _ thy (Const("Prog_Tac.Check'_elementwise", _) $ _ $
6.157 + (Const ("Set.Collect", _) $ Abs (_, _, pred))) =
6.158 + (Tactic.Check_elementwise (Rule.term_to_string''' thy pred), Tactic.Empty_Tac_)
6.159 + | stac2tac_ _ _ (Const("Prog_Tac.Or'_to'_List", _) $ _ ) = (Tactic.Or_to_List, Tactic.Empty_Tac_)
6.160 +
6.161 + (*compare "| associate _ (Subproblem'" ..TODO: extract common code *)
6.162 + | stac2tac_ pt _ (stac as Const ("Prog_Tac.SubProblem", _) $ spec' $ ags') =
6.163 + let
6.164 + val (dI, pI, mI) = Prog_Tac.dest_spec spec'
6.165 + val thy = Stool.common_subthy (Celem.assoc_thy dI, rootthy pt);
6.166 + val ags = TermC.isalist2list ags';
6.167 + val (pI, pors, mI) =
6.168 + if mI = ["no_met"]
6.169 + then
6.170 + let
6.171 + val pors = (Chead.match_ags thy ((#ppc o Specify.get_pbt) pI) ags)
6.172 + (* Chead.match_ags : theory -> pat list -> term list -> ori list
6.173 + ^^^ variables ^^^ values *)
6.174 + handle ERROR "actual args do not match formal args"
6.175 + => (Chead.match_ags_msg pI stac ags(*raise exn*); [])
6.176 + val pI' = Specify.refine_ori' pors pI;
6.177 + in (pI', pors (* refinement over models with diff.prec only *),
6.178 + (hd o #met o Specify.get_pbt) pI') end
6.179 + else (pI, (Chead.match_ags thy ((#ppc o Specify.get_pbt) pI) ags)
6.180 + handle ERROR "actual args do not match formal args"
6.181 + => (Chead.match_ags_msg pI stac ags(*raise exn*); []), mI);
6.182 + val (fmz_, vals) = Chead.oris2fmz_vals pors;
6.183 + val {cas,ppc,thy,...} = Specify.get_pbt pI
6.184 + val dI = Rule.theory2theory' thy (*.take dI from _refined_ pbl.*)
6.185 + val dI = Rule.theory2theory' (Stool.common_subthy (Celem.assoc_thy dI, rootthy pt));
6.186 + val ctxt = ContextC.initialise dI vals
6.187 + val hdl =
6.188 + case cas of
6.189 + NONE => Auto_Prog.pblterm dI pI
6.190 + | SOME t => subst_atomic ((Chead.vars_of_pbl_' ppc) ~~~ vals) t
6.191 + val f = Auto_Prog.subpbl (strip_thy dI) pI
6.192 + in (Tactic.Subproblem (dI, pI), Tactic.Subproblem' ((dI, pI, mI), pors, hdl, fmz_, ctxt, f))
6.193 + end
6.194 + | stac2tac_ _ thy t = error ("stac2tac_ TODO: no match for " ^ Rule.term_to_string''' thy t);
6.195 +
6.196 +fun stac2tac pt thy t = (fst o stac2tac_ pt thy) t;
6.197 +
6.198 +datatype ass =
6.199 + Ass of
6.200 + Tactic.T (* SubProblem gets args instantiated in associate *)
6.201 + * term (* for itr_arg, result in ets *)
6.202 + * Proof.context (* separate from Tactic.T like in locate_input_tactic *)
6.203 + | Ass_Weak of Tactic.T * term * Proof.context
6.204 + | NotAss;
6.205 +
6.206 +(* check if tac_ is associated with stac.
6.207 + Note: this is the only fun in "fun locate_input_tactic", which handles tactics individually.
6.208 + Additional tasks:
6.209 + (1) to "Subproblem'" add "pors, hdl, fmz_, ctxt, f" TODO: ctxt <-?-> sig locate_input_tac
6.210 + (2) check if term t (the result has been calculated from) in tac_
6.211 + has been changed (see "datatype tac_"); if yes, recalculate result
6.212 + TODO.WN120106 recalculate impl.only for Substitute'
6.213 +args
6.214 + pt : ctree for pushing the thy specified in rootpbl into subpbls
6.215 + d : unused (planned for data for comparison)
6.216 + tac_ : from user (via applicable_in); to be compared with ...
6.217 + stac : found in program
6.218 +returns
6.219 + Ass : associated: e.g. thmID in stac = thmID in m
6.220 + +++ arg in stac = arg in m
6.221 + Ass_Weak: weakly ass.:e.g. thmID in stac = thmID in m, //arg//
6.222 + NotAss : e.g. thmID in stac/=/thmID in m (not =)
6.223 +*)
6.224 +fun associate _ ctxt (m as Tactic.Rewrite_Inst'
6.225 + (_, _, _, _, _, thm'' as (thmID, _), f, (f', asms')), stac) =
6.226 + (case stac of
6.227 + (Const ("Prog_Tac.Rewrite'_Inst", _) $ _ $ thmID_ $ f_) =>
6.228 + if thmID = HOLogic.dest_string thmID_
6.229 + then
6.230 + if f = f_
6.231 + then Ass (m, f', ContextC.insert_assumptions asms' ctxt)
6.232 + else Ass_Weak (m, f', ContextC.insert_assumptions asms' ctxt)
6.233 + else ((*tracing"3### associate ..NotAss";*) NotAss)
6.234 + | (Const ("Prog_Tac.Rewrite'_Set'_Inst",_) $ _ $ rls_ $ f_) =>
6.235 + if Rtools.contains_rule (Rule.Thm thm'') (assoc_rls (HOLogic.dest_string rls_))
6.236 + then if f = f_ then Ass (m, f', ContextC.insert_assumptions asms' ctxt)
6.237 + else Ass_Weak (m, f', ContextC.insert_assumptions asms' ctxt)
6.238 + else NotAss
6.239 + | _ => NotAss)
6.240 + | associate _ ctxt (m as Tactic.Rewrite' (_, _, _, _, thm'' as (thmID, _), f, (f', asms')), stac) =
6.241 + (case stac of
6.242 + (Const ("Prog_Tac.Rewrite", _) $ thmID_ $ f_) =>
6.243 + if thmID = HOLogic.dest_string thmID_
6.244 + then
6.245 + if f = f_
6.246 + then Ass (m, f', ContextC.insert_assumptions asms' ctxt)
6.247 + else Ass_Weak (m, f', ContextC.insert_assumptions asms' ctxt)
6.248 + else NotAss
6.249 + | (Const ("Prog_Tac.Rewrite'_Set", _) $ rls_ $ f_) =>
6.250 + if Rtools.contains_rule (Rule.Thm thm'') (assoc_rls (HOLogic.dest_string rls_))
6.251 + then
6.252 + if f = f_
6.253 + then Ass (m, f', ContextC.insert_assumptions asms' ctxt)
6.254 + else Ass_Weak (m, f', ContextC.insert_assumptions asms' ctxt)
6.255 + else NotAss
6.256 + | _ => NotAss)
6.257 + | associate _ ctxt (m as Tactic.Rewrite_Set_Inst' (_, _, _, rls, f, (f', asms')),
6.258 + (Const ("Prog_Tac.Rewrite'_Set'_Inst", _) $ _ $ rls_ $ f_)) =
6.259 + if Rule.id_rls rls = HOLogic.dest_string rls_
6.260 + then
6.261 + if f = f_
6.262 + then Ass (m, f', ContextC.insert_assumptions asms' ctxt)
6.263 + else Ass_Weak (m ,f', ContextC.insert_assumptions asms' ctxt)
6.264 + else NotAss
6.265 + | associate _ ctxt (m as Tactic.Detail_Set_Inst' (_, _, _, rls, f, (f', asms')),
6.266 + (Const ("Prog_Tac.Rewrite'_Set'_Inst", _) $ _ $ rls_ $ f_)) =
6.267 + if Rule.id_rls rls = HOLogic.dest_string rls_
6.268 + then
6.269 + if f = f_
6.270 + then Ass (m, f', ContextC.insert_assumptions asms' ctxt)
6.271 + else Ass_Weak (m ,f', ContextC.insert_assumptions asms' ctxt)
6.272 + else NotAss
6.273 + | associate _ ctxt (m as Tactic.Rewrite_Set' (_, _, rls, f, (f', asms')),
6.274 + (Const ("Prog_Tac.Rewrite'_Set", _) $ rls_ $ f_)) =
6.275 + if Rule.id_rls rls = HOLogic.dest_string rls_
6.276 + then
6.277 + if f = f_
6.278 + then Ass (m, f', ContextC.insert_assumptions asms' ctxt)
6.279 + else Ass_Weak (m ,f', ContextC.insert_assumptions asms' ctxt)
6.280 + else NotAss
6.281 + | associate _ ctxt (m as Tactic.Detail_Set' (_, _, rls, f, (f', asms')),
6.282 + (Const ("Prog_Tac.Rewrite'_Set", _) $ rls_ $ f_)) =
6.283 + if Rule.id_rls rls = HOLogic.dest_string rls_
6.284 + then
6.285 + if f = f_
6.286 + then Ass (m, f', ContextC.insert_assumptions asms' ctxt)
6.287 + else Ass_Weak (m ,f', ContextC.insert_assumptions asms' ctxt)
6.288 + else NotAss
6.289 + | associate _ ctxt (m as Tactic.Calculate' (_, op_, f, (f', _)), stac) =
6.290 + (case stac of
6.291 + (Const ("Prog_Tac.Calculate",_) $ op__ $ f_) =>
6.292 + if op_ = HOLogic.dest_string op__
6.293 + then
6.294 + if f = f_
6.295 + then Ass (m, f', ctxt)
6.296 + else Ass_Weak (m ,f', ctxt)
6.297 + else NotAss
6.298 + | (Const ("Prog_Tac.Rewrite'_Set'_Inst", _) $ _ $ rls_ $ f_) =>
6.299 + let val thy = Celem.assoc_thy "Isac_Knowledge";
6.300 + in
6.301 + if Rtools.contains_rule (Rule.Num_Calc (assoc_calc' thy op_ |> snd))
6.302 + (assoc_rls (HOLogic.dest_string rls_))
6.303 + then
6.304 + if f = f_
6.305 + then Ass (m, f', ctxt)
6.306 + else Ass_Weak (m ,f', ctxt)
6.307 + else NotAss
6.308 + end
6.309 + | (Const ("Prog_Tac.Rewrite'_Set",_) $ rls_ $ f_) =>
6.310 + let val thy = Celem.assoc_thy "Isac_Knowledge";
6.311 + in
6.312 + if Rtools.contains_rule (Rule.Num_Calc (assoc_calc' thy op_ |> snd))
6.313 + (assoc_rls (HOLogic.dest_string rls_))
6.314 + then
6.315 + if f = f_
6.316 + then Ass (m, f', ctxt)
6.317 + else Ass_Weak (m ,f', ctxt)
6.318 + else NotAss
6.319 + end
6.320 + | _ => NotAss)
6.321 + | associate _ ctxt (m as Tactic.Check_elementwise' (consts, _, (consts_chkd, _)),
6.322 + (Const ("Prog_Tac.Check'_elementwise",_) $ consts' $ _)) =
6.323 + if consts = consts'
6.324 + then Ass (m, consts_chkd, ctxt)
6.325 + else NotAss
6.326 + | associate _ ctxt (m as Tactic.Or_to_List' (_, list), (Const ("Prog_Tac.Or'_to'_List", _) $ _)) =
6.327 + Ass (m, list, ctxt)
6.328 + | associate _ ctxt (m as Tactic.Take' term, (Const ("Prog_Tac.Take", _) $ _)) = Ass (m, term, ctxt)
6.329 + | associate _ ctxt (m as Tactic.Substitute' (ro, erls, subte, f, f'),
6.330 + (Const ("Prog_Tac.Substitute", _) $ _ $ t)) =
6.331 + if f = t then Ass (m, f', ctxt)
6.332 + else (*compare | applicable_in (p,p_) pt (m as Substitute sube)*)
6.333 + if foldl and_ (true, map TermC.contains_Var subte)
6.334 + then
6.335 + let val t' = subst_atomic (map HOLogic.dest_eq subte (*TODO subte2subst*)) t
6.336 + in if t = t' then error "associate: Substitute' not applicable to val of Expr"
6.337 + else Ass (Tactic.Substitute' (ro, erls, subte, t, t'), t', ctxt)
6.338 + end
6.339 + else (case Rewrite.rewrite_terms_ (Rule.Isac ()) ro erls subte t of
6.340 + SOME (t', _) => Ass (Tactic.Substitute' (ro, erls, subte, t, t'), t', ctxt)
6.341 + | NONE => error "associate: Substitute' not applicable to val of Expr")
6.342 +
6.343 + (*compare "| stac2tac_ thy (Const ("Prog_Tac.SubProblem",_)" ..TODO: extract common code *)
6.344 + | associate pt _ (Tactic.Subproblem' ((domID, pblID, _), _, _, _, _, _),
6.345 + (stac as Const ("Prog_Tac.SubProblem", _) $ spec' $ ags')) =
6.346 + let
6.347 + val (dI, pI, mI) = Prog_Tac.dest_spec spec'
6.348 + val thy = Stool.common_subthy (Celem.assoc_thy dI, rootthy pt);
6.349 + val ags = TermC.isalist2list ags';
6.350 + val (pI, pors, mI) =
6.351 + if mI = ["no_met"]
6.352 + then
6.353 + let
6.354 + val pors = (Chead.match_ags thy ((#ppc o Specify.get_pbt) pI) ags)
6.355 + handle ERROR "actual args do not match formal args"
6.356 + => (Chead.match_ags_msg pI stac ags(*raise exn*);[]);
6.357 + val pI' = Specify.refine_ori' pors pI;
6.358 + in (pI', pors (*refinement over models with diff.prec only*), (hd o #met o Specify.get_pbt) pI')
6.359 + end
6.360 + else (pI, (Chead.match_ags thy ((#ppc o Specify.get_pbt) pI) ags)
6.361 + handle ERROR "actual args do not match formal args"
6.362 + => (Chead.match_ags_msg pI stac ags(*raise exn*); []), mI);
6.363 + val (fmz_, vals) = Chead.oris2fmz_vals pors;
6.364 + val {cas, ppc, thy, ...} = Specify.get_pbt pI
6.365 + val dI = Rule.theory2theory' thy (*take dI from _refined_ pbl*)
6.366 + val dI = Rule.theory2theory' (Stool.common_subthy (Celem.assoc_thy dI, rootthy pt))
6.367 + val ctxt = ContextC.initialise dI vals
6.368 + val hdl =
6.369 + case cas of
6.370 + NONE => Auto_Prog.pblterm dI pI
6.371 + | SOME t => subst_atomic ((Chead.vars_of_pbl_' ppc) ~~~ vals) t
6.372 + val f = Auto_Prog.subpbl (strip_thy dI) pI
6.373 + in
6.374 + if domID = dI andalso pblID = pI
6.375 + then Ass (Tactic.Subproblem' ((dI, pI, mI), pors, hdl, fmz_, ContextC.e_ctxt(*TODO rm*), f), f, ctxt)
6.376 + else NotAss
6.377 + end
6.378 + | associate _ _ (m, _) =
6.379 + (if (!trace_script)
6.380 + then tracing("@@@ the 'tac_' proposed to apply does NOT match the leaf found in the script:\n"
6.381 + ^ "@@@ tac_ = " ^ Tactic.string_of m)
6.382 + else ();
6.383 + NotAss);
6.384 +
6.385 +(* create the initial interpreter state
6.386 + from the items of the guard and the formal arguments of the partial_function.
6.387 +Note on progression from (a) type fmz_ \<longrightarrow> (e) arguments of the partial_function:
6.388 + (a) fmz is given by a math author
6.389 + (b) fmz_ is transformed to ori list as a prerequisite for efficient interactive modelling
6.390 + (c) modelling creates an itm list from ori list + possible user input
6.391 + (d) specifying a theory might add some items and create a guard for the partial_function
6.392 + (e) fun relate_args creates an environment for evaluating the partial_function.
6.393 +Note on sequence-relation (a) -- (e), i.e. the (formal) arguments of the partial_function:
6.394 + * Since the arguments of the partial_function have no description (see Descript.thy),
6.395 + (e) depends on the sequence in fmz_ and on the types of the formal arguments.
6.396 + * pairing formal arguments with itm's follows the sequence
6.397 + * Thus the resulting sequence-relation can be ambiguous.
6.398 + * Ambiguities are done by rearranging fmz_ or the formal arguments.
6.399 + * The latter is easier, albeit not optimal: a fmz_ can be used by different partial_functions.
6.400 + *)
6.401 +local
6.402 +val errmsg = "ERROR: found no actual arguments for prog. of "
6.403 +fun msg_miss sc metID caller f formals actuals =
6.404 + "ERROR in creating the environment from formal args. of partial_function \"" ^ fst (Program.get_fun_id sc) ^ "\"\n" ^
6.405 + "and the actual args., ie. items of the guard of \"" ^ Celem.metID2str metID ^ "\" by \"" ^ caller ^ "\":\n" ^
6.406 + "formal arg \"" ^ Rule.term2str f ^ "\" doesn't mach an actual arg.\n" ^
6.407 + "with:\n" ^
6.408 + (string_of_int o length) formals ^ " formal args: " ^ Rule.terms2str formals ^ "\n" ^
6.409 + (string_of_int o length) actuals ^ " actual args: " ^ Rule.terms2str actuals
6.410 +fun msg_miss_type sc metID f formals actuals =
6.411 + "ERROR in creating the environment from formal args. of partial_function \"" ^ fst (Program.get_fun_id sc) ^ "\"\n" ^
6.412 + "and the actual args., ie. items of the guard of \"" ^ Celem.metID2str metID ^ "\" by \"assoc_by_type\":\n" ^
6.413 + "formal arg \"" ^ Rule.term2str f ^ "\" of type \"" ^ Rule.type2str (type_of f) ^
6.414 + "\" doesn't mach an actual arg.\nwith:\n" ^
6.415 + (string_of_int o length) formals ^ " formal args: " ^ Rule.terms2str formals ^ "\n" ^
6.416 + (string_of_int o length) actuals ^ " actual args: " ^ Rule.terms2str actuals ^ "\n" ^
6.417 + " with types: " ^ (strs2str o (map (Rule.type2str o type_of))) actuals
6.418 +fun msg_ambiguous sc metID f aas formals actuals =
6.419 + "AMBIGUITY in creating the environment from formal args. of partial_function \"" ^ fst (Program.get_fun_id sc) ^ "\"\n" ^
6.420 + "and the actual args., ie. items of the guard of \"" ^ Celem.metID2str metID ^ "\" by \"assoc_by_type\":\n" ^
6.421 + "formal arg. \"" ^ Rule.term2str f ^ "\" type-matches with several..." ^
6.422 + "actual args. \"" ^ Rule.terms2str aas ^ "\"\n" ^
6.423 + "selected \"" ^ Rule.term2str (hd aas) ^ "\"\n" ^
6.424 + "with\n" ^
6.425 + "formals: " ^ Rule.terms2str formals ^ "\n" ^
6.426 + "actuals: " ^ Rule.terms2str actuals
6.427 +fun trace_init metID =
6.428 + if (!trace_script)
6.429 + then tracing("@@@ program " ^ strs2str metID)
6.430 + else ();
6.431 +fun trace_istate env =
6.432 + if (!trace_script)
6.433 + then tracing("@@@ istate " ^ Env.env2str env)
6.434 + else ();
6.435 +in
6.436 +fun init_pstate srls ctxt itms metID =
6.437 + let
6.438 + val itms = Specify.hack_until_review_Specify_2 metID itms
6.439 + val actuals = itms2args (Proof_Context.theory_of ctxt) metID itms
6.440 + val _ = if actuals <> [] then () else raise ERROR (errmsg ^ strs2str' metID)
6.441 + val (scr, sc) = (case (#scr o Specify.get_met) metID of
6.442 + scr as Rule.Prog sc => (trace_init metID; (scr, sc))
6.443 + | _ => raise ERROR ("init_pstate with " ^ Celem.metID2str metID))
6.444 + val formals = Program.formal_args sc
6.445 + fun assoc_by_type f aa =
6.446 + case filter (curry (fn (f, a) => type_of f = type_of a) f) aa of
6.447 + [] => error (msg_miss_type sc metID f formals actuals)
6.448 + | [a] => (f, a)
6.449 + | aas as (a :: _) => (writeln (msg_ambiguous sc metID f aas formals actuals); (f, a));
6.450 + fun relate_args _ (f::_) [] = error (msg_miss sc metID "relate_args" f formals actuals)
6.451 + | relate_args env [] _ = env (*may drop Find?*)
6.452 + | relate_args env (f::ff) (aas as (a::aa)) =
6.453 + if type_of f = type_of a
6.454 + then relate_args (env @ [(f, a)]) ff aa
6.455 + else
6.456 + let val (f, a) = assoc_by_type f aas
6.457 + in relate_args (env @ [(f, a)]) ff (remove op = a aas) end
6.458 + val {pre, prls, ...} = Specify.get_met metID;
6.459 + val pres = Stool.check_preconds (Proof_Context.theory_of ctxt) prls pre itms |> map snd;
6.460 + val ctxt = ctxt |> ContextC.insert_assumptions pres;
6.461 + val ist = Istate.e_pstate
6.462 + |> Istate.set_eval srls
6.463 + |> Istate.set_env_true (relate_args [] formals actuals)
6.464 + in
6.465 + (Istate.Pstate ist, ctxt, scr)
6.466 + end;
6.467 +end (*local*)
6.468 +
6.469 +fun get_simplifier (pt, (p, _)) =
6.470 + let
6.471 + val p' = Ctree.par_pblobj pt p
6.472 + val metID = Ctree.get_obj Ctree.g_metID pt p'
6.473 + val {srls, ...} = Specify.get_met metID
6.474 + in srls end
6.475 +
6.476 +(* decide, where to get program/istate from:
6.477 + (* 1 *) from PblObj.Env.update: at begin of program if no init_form
6.478 + (* 2 *) from PblObj/PrfObj: if Prog_Tac is in the middle of the program
6.479 + (* 3 *) from rls/PrfObj: in case of Math_Engine.detailstep *)
6.480 +fun from_pblobj_or_detail' _ (p, p_) pt =
6.481 + if member op = [Pbl, Met] p_
6.482 + then case get_obj g_env (*?DEPRECATED?*) pt p of
6.483 + NONE => error "from_pblobj_or_detail': no istate"
6.484 + | SOME (Istate.Pstate pst, ctxt) =>
6.485 + let
6.486 + val metID = get_obj g_metID pt p
6.487 + val {srls, ...} = Specify.get_met metID
6.488 + in
6.489 + (srls, (Istate.Pstate (Istate.set_eval srls pst), ctxt), (#scr o Specify.get_met) metID)
6.490 + end
6.491 + | _ => raise ERROR "from_pblobj_or_detail': unexpected result from g_env"
6.492 + else
6.493 + let val (pbl, p', rls') = par_pbl_det pt p
6.494 + in if pbl
6.495 + then (*if last_elem p = 0 nothing written to pt yet*) (* 2 *)
6.496 + let
6.497 + val metID = get_obj g_metID pt p'
6.498 + val {srls, ...} = Specify.get_met metID
6.499 + val (is, ctxt) =
6.500 + case get_loc pt (p, p_) of
6.501 + (Istate.Pstate ist, ctxt) => (Istate.Pstate (Istate.set_eval srls ist), ctxt)
6.502 + | _ => raise ERROR "from_pblobj_or_detail': unexpected result from get_loc"
6.503 + in (srls, (is, ctxt), (#scr o Specify.get_met) metID) end
6.504 + else
6.505 + let
6.506 + (*TODO.thy Auto_Prog.generate SHOULD REPLACE ALL HIS..*)
6.507 + val prog = case rls' of
6.508 + Rule.Rls {scr = Rule.Prog prog,...} => prog
6.509 + | Rule.Seq {scr = Rule.Prog prog,...} => prog
6.510 + | _ => raise ERROR ("from_pblobj_or_detail': not for rule-set \"" ^ Rule.id_rls rls' ^ "\"")
6.511 + val t = get_last_formula (pt, (p, p_))
6.512 + val prog' = Auto_Prog.subst_typs prog (type_of t) (TermC.guess_bdv_typ t)
6.513 + in (Rule.e_rls(*!!!*), get_loc pt (p, p_), Rule.Prog prog') end
6.514 + end
6.515 +
6.516 +fun from_pblobj' thy' (p,p_) pt = (*.get script and istate, UNUSED; see above ( * 1 *)
6.517 + let
6.518 + val p' = par_pblobj pt p
6.519 + val itms =
6.520 + (case get_obj I pt p' of
6.521 + PblObj {meth = itms, ...} => itms
6.522 + | PrfObj _ => error "from_pblobj' NOT with PrfObj")
6.523 + val metID = get_obj g_metID pt p'
6.524 + val {srls, scr, ...} = Specify.get_met metID
6.525 + in
6.526 + if last_elem p = 0 (*nothing written to pt yet*)
6.527 + then
6.528 + let
6.529 + val ctxt = ContextC.initialise thy' (Model.vars_of itms)
6.530 + val (is, ctxt, scr) = init_pstate srls ctxt itms metID
6.531 + in (srls(*..\<in> is*), (is, ctxt), scr) end
6.532 + else (srls(*..\<in> is*), get_loc pt (p,p_), scr)
6.533 + end;
6.534 +
6.535 +(*.get the stactics and problems of a script as tacs
6.536 + instantiated with the current environment;
6.537 + l is the location which generated the given formula.*)
6.538 +(*WN.12.5.03: quick-and-dirty repair for listexpressions*)
6.539 +fun is_spec_pos Pbl = true
6.540 + | is_spec_pos Met = true
6.541 + | is_spec_pos _ = false;
6.542 +
6.543 +(* handle a leaf at the end of recursive descent:
6.544 + a leaf is either a tactic or an 'expr' in "let v = expr"
6.545 + where "expr" does not contain a tactic.
6.546 + Handling a leaf comprises
6.547 + (1) 'subst_stacexpr' substitute Env.update and complete curried tactic
6.548 + (2) rewrite the leaf by 'srls'
6.549 +*)
6.550 +fun check_leaf call ctxt srls (E, (a, v)) t =
6.551 + case Prog_Tac.eval_leaf E a v t of
6.552 + (Program.Tac stac, a') =>
6.553 + let val stac' =
6.554 + Rewrite.eval_prog_expr (Proof_Context.theory_of ctxt) srls
6.555 + (subst_atomic (Env.update_opt E (a,v)) stac)
6.556 + in
6.557 + (if (! trace_script)
6.558 + then tracing ("@@@ " ^ call ^ " leaf '" ^ Rule.term2str t ^ "' ---> Tac '" ^ Rule.term2str stac ^ "'")
6.559 + else ();
6.560 + (Program.Tac stac', a'))
6.561 + end
6.562 + | (Program.Expr lexpr, a') =>
6.563 + let val lexpr' =
6.564 + Rewrite.eval_prog_expr (Proof_Context.theory_of ctxt) srls (subst_atomic (Env.update_opt E (a,v)) lexpr)
6.565 + in
6.566 + (if (! trace_script)
6.567 + then tracing("@@@ "^call^" leaf '" ^ Rule.term2str t ^ "' ---> Expr '" ^ Rule.term2str lexpr' ^ "'")
6.568 + else ();
6.569 + (Program.Expr lexpr', a')) (*lexpr' is the value of the Expr*)
6.570 + end;
6.571 +
6.572 +(*. fetch _all_ tactics from script .*)
6.573 +fun sel_rules _ (([],Res):pos') =
6.574 + raise PTREE "no tactics applicable at the end of a calculation"
6.575 + | sel_rules pt (p,p_) =
6.576 + if is_spec_pos p_
6.577 + then [get_obj g_tac pt p]
6.578 + else
6.579 + let
6.580 + val pp = par_pblobj pt p;
6.581 + val thy' = get_obj g_domID pt pp;
6.582 + val thy = Celem.assoc_thy thy';
6.583 + val metID = get_obj g_metID pt pp;
6.584 + val metID' = if metID = Celem.e_metID then (thd3 o snd3) (get_obj g_origin pt pp) else metID
6.585 + val (sc, srls) = (case Specify.get_met metID' of
6.586 + {scr = Rule.Prog sc, srls, ...} => (sc, srls) | _ => error "sel_rules 1")
6.587 + val subst = get_istate pt (p, p_) |> Istate.the_pstate |> Istate.get_subst
6.588 + val ctxt = get_ctxt pt (p, p_)
6.589 + in map ((stac2tac pt thy) o Program.rep_stacexpr o #1 o
6.590 + (check_leaf "selrul" ctxt srls subst)) (Auto_Prog.stacpbls sc)
6.591 + end;
6.592 +
6.593 +(* fetch tactics from script and filter _applicable_ tactics;
6.594 + in case of Rewrite_Set* go down to _atomic_ rewrite-tactics *)
6.595 +fun sel_appl_atomic_tacs _ (([], Res) : pos') =
6.596 + raise PTREE "no tactics applicable at the end of a calculation"
6.597 + | sel_appl_atomic_tacs pt (p, p_) =
6.598 + if is_spec_pos p_
6.599 + then [get_obj g_tac pt p]
6.600 + else
6.601 + let
6.602 + val pp = par_pblobj pt p
6.603 + val thy' = get_obj g_domID pt pp
6.604 + val thy = Celem.assoc_thy thy'
6.605 + val metID = get_obj g_metID pt pp
6.606 + val metID' =
6.607 + if metID = Celem.e_metID
6.608 + then (thd3 o snd3) (get_obj g_origin pt pp)
6.609 + else metID
6.610 + val (sc, srls, erls, ro) = (case Specify.get_met metID' of
6.611 + {scr = Rule.Prog sc, srls, erls, rew_ord' = ro, ...} => (sc, srls, erls, ro)
6.612 + | _ => error "sel_appl_atomic_tacs 1")
6.613 + val (env, (a, v)) = (case get_istate pt (p, p_) of
6.614 + Istate.Pstate pst => (Istate.get_subst pst) | _ => error "sel_appl_atomic_tacs 2")
6.615 + val ctxt = get_ctxt pt (p, p_)
6.616 + val alltacs = (*we expect at least 1 stac in a script*)
6.617 + map ((stac2tac pt thy) o Program.rep_stacexpr o #1 o
6.618 + (check_leaf "selrul" ctxt srls (env, (a, v)))) (Auto_Prog.stacpbls sc)
6.619 + val f =
6.620 + (case p_ of Frm => get_obj g_form pt p | Res => (fst o (get_obj g_result pt)) p
6.621 + | _ => error "")
6.622 + (*WN071231 ? replace atomic_appl_tacs with applicable_in (ineff!) ?*)
6.623 + in ((gen_distinct Tactic.eq_tac) o flat o (map (Rtools.atomic_appl_tacs thy ro erls f))) alltacs end;
6.624 +
6.625 +(**)end(**)
7.1 --- a/src/Tools/isac/Interpret/lucas-interpreter.sml Tue Feb 04 16:45:36 2020 +0100
7.2 +++ b/src/Tools/isac/Interpret/lucas-interpreter.sml Tue Feb 04 17:11:54 2020 +0100
7.3 @@ -66,7 +66,7 @@
7.4 end
7.5
7.6 (**)
7.7 -structure LucinNEW(**): LUCAS_INTERPRETER(**) = (*LucinNEW \<rightarrow> Lucin after code re-arrangement*)
7.8 +structure Lucin(**): LUCAS_INTERPRETER(**) =
7.9 struct
7.10 (**)
7.11 open Ctree
7.12 @@ -116,17 +116,17 @@
7.13 (** interpret a Prog_Tac: is it associated to Tactic ? **)
7.14
7.15 fun check_tac1 ((pt, p), ctxt, tac) (ist as {act_arg, or, ...}) (form_arg, prog_tac) =
7.16 - case Lucin.associate pt ctxt (tac, prog_tac) of
7.17 + case LItool.associate pt ctxt (tac, prog_tac) of
7.18 (* HERE ----------------vvvv ContextC.insert_assumptions asm ctxt DONE -- 2nd in gen//*)
7.19 - Lucin.Ass (m, v', ctxt)
7.20 + LItool.Ass (m, v', ctxt)
7.21 => Accept_Tac1 (ist |> set_subst_true (form_arg, v') |> set_found, ctxt, m)
7.22 - | Lucin.Ass_Weak (m, v', ctxt) (*the ONLY ones in locate_tac ^v^v^v^v^ *)
7.23 + | LItool.Ass_Weak (m, v', ctxt) (*the ONLY ones in locate_tac ^v^v^v^v^ *)
7.24 => Accept_Tac1 (ist |> set_subst_false (form_arg, v') |> set_found, ctxt, m)
7.25 - | Lucin.NotAss =>
7.26 + | LItool.NotAss =>
7.27 (case or of (* switch for Tactical.Or: 1st AssOnly, 2nd AssGen *)
7.28 AssOnly => Term_Val1 act_arg
7.29 | _(*ORundef*) =>
7.30 - case Applicable.applicable_in p pt (Lucin.stac2tac pt (Celem.assoc_thy "Isac_Knowledge") prog_tac) of
7.31 + case Applicable.applicable_in p pt (LItool.stac2tac pt (Celem.assoc_thy "Isac_Knowledge") prog_tac) of
7.32 Applicable.Appl m' => Reject_Tac1 (ist |> set_subst_false (form_arg, Tactic.result m'), ctxt, tac)
7.33 | Applicable.Notappl _ => Term_Val1 act_arg)
7.34
7.35 @@ -201,7 +201,7 @@
7.36 | scan_dn1 (cct as (_, ctxt, _)) (ist as {eval, ...}) t =
7.37 if Tactical.contained_in t then raise TERM ("scan_dn1 expects Prog_Tac or Prog_Expr", [t])
7.38 else
7.39 - case Lucin.check_leaf "locate" ctxt eval (get_subst ist) t of
7.40 + case LItool.check_leaf "locate" ctxt eval (get_subst ist) t of
7.41 (Program.Expr _, form_arg) =>
7.42 Term_Val1 (Rewrite.eval_prog_expr (Proof_Context.theory_of ctxt) eval
7.43 (subst_atomic (Env.update_opt'' (get_act_env ist, form_arg)) t))
7.44 @@ -317,7 +317,7 @@
7.45
7.46 fun check_tac ((pt, p), ctxt) ist (form_arg, prog_tac) =
7.47 let
7.48 - val (m, m') = Lucin.stac2tac_(*..see TODO.thy*)pt (Proof_Context.theory_of ctxt) prog_tac
7.49 + val (m, m') = LItool.stac2tac_(*..see TODO.thy*)pt (Proof_Context.theory_of ctxt) prog_tac
7.50 in
7.51 case m of (*TODO?: push both cases into make applicable_in (Subproblem..refine problem!)*)
7.52 Tactic.Subproblem _ =>
7.53 @@ -394,7 +394,7 @@
7.54 if Tactical.contained_in t
7.55 then raise TERM ("scan_dn expects Prog_Tac or Prog_Expr", [t])
7.56 else
7.57 - case Lucin.check_leaf "next " ctxt eval (get_subst ist) t of
7.58 + case LItool.check_leaf "next " ctxt eval (get_subst ist) t of
7.59 (Program.Expr s, _) => Term_Val s (*TODO?: include set_found here and drop those after call*)
7.60 | (Program.Tac prog_tac, form_arg) =>
7.61 check_tac cc ist (form_arg, prog_tac)
7.62 @@ -404,7 +404,7 @@
7.63 then
7.64 if found_accept
7.65 then Term_Val act_arg
7.66 - else raise ERROR "Lucin.find_next_step without result"
7.67 + else raise ERROR "LItool.find_next_step without result"
7.68 else scan_up pcc (ist |> path_up) (go_up path sc)
7.69 (* scan is strictly to R, because at L there was an \<open>expr_val\<close> *)
7.70 and scan_up pcc ist (Const ("Tactical.Try"(*1*), _) $ _ $ _) = go_scan_up pcc ist
7.71 @@ -512,16 +512,16 @@
7.72 let
7.73 val (itms, (*l..*)oris, probl(*..l*)) = case get_obj I pt p of
7.74 PblObj {meth = itms, origin = (oris, _, _), probl, ...} => (itms, oris, probl)
7.75 - | _ => error "LucinNEW.by_tactic Apply_Method': uncovered case get_obj"
7.76 + | _ => error "Lucin.by_tactic Apply_Method': uncovered case get_obj"
7.77 (*l*) val {ppc, ...} = Specify.get_met mI;
7.78 (*l*) val itms = if itms <> [] then itms else Chead.complete_metitms oris probl [] ppc
7.79 (*l*) val itms = Specify.hack_until_review_Specify_1 mI itms
7.80 val thy = Celem.assoc_thy (get_obj g_domID pt p);
7.81 - val srls = Lucin.get_simplifier (pt, pos)
7.82 - val (is, env, ctxt, scr) = case Lucin.init_pstate srls ctxt itms mI of
7.83 + val srls = LItool.get_simplifier (pt, pos)
7.84 + val (is, env, ctxt, scr) = case LItool.init_pstate srls ctxt itms mI of
7.85 (is as Pstate {env, ...}, ctxt, scr) => (is, env, ctxt, scr)
7.86 - | _ => error "LucinNEW.by_tactic Apply_Method': uncovered case init_pstate"
7.87 - val ini = Lucin.init_form thy scr env;
7.88 + | _ => error "Lucin.by_tactic Apply_Method': uncovered case init_pstate"
7.89 + val ini = LItool.init_form thy scr env;
7.90 in
7.91 case ini of
7.92 SOME t =>
7.93 @@ -583,7 +583,7 @@
7.94 else
7.95 let
7.96 val thy' = get_obj g_domID pt (par_pblobj pt p);
7.97 - val (_, (ist, ctxt), sc) = Lucin.from_pblobj_or_detail' thy' (p,p_) pt;
7.98 + val (_, (ist, ctxt), sc) = LItool.from_pblobj_or_detail' thy' (p,p_) pt;
7.99 in
7.100 case find_next_step sc (pt, pos) ist ctxt of
7.101 Next_Step (ist, ctxt, tac) =>
8.1 --- a/src/Tools/isac/Interpret/script.sml Tue Feb 04 16:45:36 2020 +0100
8.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
8.3 @@ -1,623 +0,0 @@
8.4 -(* Title: interpreter for scripts
8.5 - Author: Walther Neuper 2000
8.6 - (c) due to copyright terms
8.7 -*)
8.8 -
8.9 -signature LUCAS_INTERPRETER_DEL =
8.10 -sig
8.11 -
8.12 - type step = Tactic.T * Generate.mout * Ctree.ctree * Ctree.pos' * Ctree.pos' list
8.13 - datatype ass =
8.14 - Ass of Tactic.T * term * Proof.context
8.15 - | Ass_Weak of Tactic.T * term * Proof.context
8.16 - | NotAss;
8.17 - val associate: Ctree.ctree -> Proof.context -> (Tactic.T * term) -> ass
8.18 -
8.19 -(* can these functions be local to Lucin or part of LItools ? *)
8.20 - val sel_rules : Ctree.ctree -> Ctree.pos' -> Tactic.input list
8.21 - val init_form : 'a -> Program.T -> (term * term) list -> term option
8.22 - val init_pstate : Rule.rls -> Proof.context -> Model.itm list -> Celem.metID -> Istate.T * Proof.context * Program.T
8.23 -
8.24 - val get_simplifier : Calc.T -> Rule.rls
8.25 -(*DEPR ^*)val from_pblobj' : Rule.theory' -> Ctree.pos' -> Ctree.ctree ->
8.26 - Rule.rls(*..\<in> ist*) * (Istate.T * Proof.context) * Program.T
8.27 -(*DEPR*)val from_pblobj_or_detail' : Rule.theory' -> Ctree.pos' -> Ctree.ctree ->
8.28 - Rule.rls(*..\<in> ist*) * (Istate.T * Proof.context) * Program.T
8.29 - val rule2thm'' : Rule.rule -> Celem.thm''
8.30 - val rule2rls' : Rule.rule -> string
8.31 - val sel_appl_atomic_tacs : Ctree.ctree -> Ctree.pos' -> Tactic.input list
8.32 -(*cp here from "! aktivate for Test_Isac" below due to LucinNEW*)
8.33 - val stac2tac_ : Ctree.ctree -> theory -> term -> Tactic.input * Tactic.T
8.34 - val stac2tac : Ctree.ctree -> theory -> term -> Tactic.input
8.35 - val rew_only: (Tactic.T * Generate.mout * Ctree.ctree * Ctree.pos' * Ctree.pos' list) list -> bool
8.36 - val check_leaf : (*TODO190625: shift to lucas-interpreter.sml ? <- sel_rules, sel_appl_atomic_tacs !*)
8.37 - string -> Proof.context -> Rule.rls -> (Env.T * (term option * term)) -> term ->
8.38 - Program.leaf * term option
8.39 -
8.40 -(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
8.41 - (*NONE*)
8.42 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
8.43 - val is_spec_pos : Ctree.pos_ -> bool
8.44 - val itms2args : 'a -> Celem.metID -> Model.itm list -> term list
8.45 -( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
8.46 -
8.47 -end
8.48 -
8.49 -(* traces the leaves (ie. non-tactical nodes) of Prog found by find_next_step, see "and scr" *)
8.50 -val trace_script = Unsynchronized.ref false; (* TODO: how are traces done in Isabelle? *)
8.51 -
8.52 -(**)
8.53 -structure Lucin(**): LUCAS_INTERPRETER_DEL(**) =
8.54 -struct
8.55 -(**)
8.56 -open Ctree
8.57 -open Pos
8.58 -(*TODO open Celem for L,R,D;
8.59 - the few other Celem.items are acceptable: metID, e_metID, assoc_thy, metID2str, thm''*)
8.60 -
8.61 -(**)
8.62 -(* data for creating a new node in ctree; designed for use as:
8.63 - fun ass* pstate steps = / ... case ass* pstate steps of /
8.64 - Accept_Tac1 (pstate, steps) => ... ass* pstate steps *)
8.65 -type step = (*WN190713 REMOVE: "creating a new node" was never implemented for more than one node?!?
8.66 - WN190713 COMPARE: taci list, see papernote #139 *)
8.67 - Tactic.T (*transformed from associated tac *)
8.68 - * Generate.mout (*result with indentation etc. *)
8.69 - * ctree (*containing node created by tac_ + resp. pstate *)
8.70 - * pos' (*position in ctree; ctree * pos' is the proofstate *)
8.71 - * pos' list; (*of ctree-nodes probably cut (by fst tac_)
8.72 - WN190713 COMPARE: pos' list also in calcstate'*)
8.73 -
8.74 -fun rule2thm'' (Rule.Thm (id, thm)) = (id, thm)
8.75 - | rule2thm'' r = error ("rule2thm': not defined for " ^ Rule.rule2str r);
8.76 -fun rule2rls' (Rule.Rls_ rls) = Rule.id_rls rls
8.77 - | rule2rls' r = error ("rule2rls': not defined for " ^ Rule.rule2str r);
8.78 -
8.79 -(*check if there are tacs for rewriting only*)
8.80 -fun rew_only ([]:step list) = true
8.81 - | rew_only (((Tactic.Rewrite' _ ,_,_,_,_))::ss) = rew_only ss
8.82 - | rew_only (((Tactic.Rewrite_Inst' _ ,_,_,_,_))::ss) = rew_only ss
8.83 - | rew_only (((Tactic.Rewrite_Set' _ ,_,_,_,_))::ss) = rew_only ss
8.84 - | rew_only (((Tactic.Rewrite_Set_Inst' _ ,_,_,_,_))::ss) = rew_only ss
8.85 - | rew_only (((Tactic.Calculate' _ ,_,_,_,_))::ss) = rew_only ss
8.86 - | rew_only (((Tactic.Begin_Trans' _ ,_,_,_,_))::ss) = rew_only ss
8.87 - | rew_only (((Tactic.End_Trans' _ ,_,_,_,_))::ss) = rew_only ss
8.88 - | rew_only _ = false;
8.89 -
8.90 -(* functions for the environment stack: NOT YET IMPLEMENTED
8.91 -fun accessenv id es = the (assoc ((top es) : Env.update, id))
8.92 - handle _ => error ("accessenv: " ^ free2str id ^ " not in Env.update");
8.93 -fun updateenv id vl (es : Env.update stack) =
8.94 - (push (overwrite(top es, (id, vl))) (pop es)) : Env.update stack;
8.95 -fun pushenv id vl (es : Env.update stack) =
8.96 - (push (overwrite(top es, (id, vl))) es) : Env.update stack;
8.97 -val popenv = pop : Env.update stack -> Env.update stack;
8.98 -*)
8.99 -
8.100 -fun de_esc_underscore str =
8.101 - let
8.102 - fun scan [] = []
8.103 - | scan (s :: ss) = if s = "'" then (scan ss) else (s :: (scan ss))
8.104 - in (implode o scan o Symbol.explode) str end;
8.105 -
8.106 -fun init_form thy (Rule.Prog sc) env =
8.107 - (case Prog_Tac.get_stac thy sc of NONE => NONE | SOME stac => SOME (subst_atomic env stac))
8.108 - | init_form _ _ _ = error "init_form: no match";
8.109 -
8.110 -type dsc = typ; (* <-> nam..unknow in Descript.thy *)
8.111 -
8.112 -(*.create the actual parameters (args) of script: their order
8.113 - is given by the order in met.pat .*)
8.114 -(*WN.5.5.03: ?: does this allow for different descriptions ???
8.115 - ?: why not taken from formal args of script ???
8.116 -!: FIXXXME penv: push it here in itms2args into script-evaluation*)
8.117 -val errmsg = "ERROR: the guard is missing (#ppc in 'type met' added in prep_met)."
8.118 -fun errmsg2 d itms = ("itms2args: '" ^ Rule.term2str d ^ "' not in itms:\n" ^
8.119 -"itms:\n" ^ Model.itms2str_ @{context} itms)
8.120 -fun itms2args _ mI itms =
8.121 - let
8.122 - val mvat = Model.max_vt itms
8.123 - fun okv mvat (_, vats, b, _, _) = member op = vats mvat andalso b
8.124 - val itms = filter (okv mvat) itms
8.125 - fun test_dsc d (_, _, _, _, itm_) = (d = Model.d_in itm_)
8.126 - fun itm2arg itms (_,(d,_)) =
8.127 - case find_first (test_dsc d) itms of
8.128 - NONE => raise ERROR (errmsg2 d itms)
8.129 - | SOME (_, _, _, _, itm_) => Model.penvval_in itm_
8.130 - (*| SOME (_,_,_,_,itm_) => mk_arg thy (Model.d_in itm_) (ts_in itm_);
8.131 - penv postponed; presently penv holds already Env.update for script*)
8.132 - val pats = (#ppc o Specify.get_met) mI
8.133 - val _ = if pats = [] then raise ERROR errmsg else ()
8.134 - in (flat o (map (itm2arg itms))) pats end;
8.135 -
8.136 -(* convert a script-tac 'stac' to 'tac' for users;
8.137 - for "Prog_Tac.SubProblem" also create a 'tac_' for internal use. FIXME separate?
8.138 - if stac is an initac, then convert to a 'tac_' (as required in scan_dn).
8.139 - arg ctree for pushing the thy specified in rootpbl into subpbls *)
8.140 -fun stac2tac_ _ thy (Const ("Prog_Tac.Rewrite", _) $ thmID $ _) =
8.141 - let
8.142 - val tid = HOLogic.dest_string thmID
8.143 - in (Tactic.Rewrite (tid, Rewrite.assoc_thm'' thy tid), Tactic.Empty_Tac_) end
8.144 - | stac2tac_ _ thy (Const ("Prog_Tac.Rewrite'_Inst", _) $ sub $ thmID $ _) =
8.145 - let
8.146 - val tid = HOLogic.dest_string thmID
8.147 - in (Tactic.Rewrite_Inst (Selem.subst'_to_sube sub, (tid, Rewrite.assoc_thm'' thy tid)), Tactic.Empty_Tac_) end
8.148 - | stac2tac_ _ _ (Const ("Prog_Tac.Rewrite'_Set",_) $ rls $ _) =
8.149 - (Tactic.Rewrite_Set (HOLogic.dest_string rls), Tactic.Empty_Tac_)
8.150 - | stac2tac_ _ _ (Const ("Prog_Tac.Rewrite'_Set'_Inst", _) $ sub $ rls $ _) =
8.151 - (Tactic.Rewrite_Set_Inst (Selem.subst'_to_sube sub, HOLogic.dest_string rls), Tactic.Empty_Tac_)
8.152 - | stac2tac_ _ _ (Const ("Prog_Tac.Calculate", _) $ op_ $ _) =
8.153 - (Tactic.Calculate (HOLogic.dest_string op_), Tactic.Empty_Tac_)
8.154 - | stac2tac_ _ _ (Const ("Prog_Tac.Take", _) $ t) = (Tactic.Take (Rule.term2str t), Tactic.Empty_Tac_)
8.155 - | stac2tac_ _ _ (Const ("Prog_Tac.Substitute", _) $ isasub $ _) =
8.156 - (Tactic.Substitute ((Selem.subte2sube o TermC.isalist2list) isasub), Tactic.Empty_Tac_)
8.157 - | stac2tac_ _ thy (Const("Prog_Tac.Check'_elementwise", _) $ _ $
8.158 - (Const ("Set.Collect", _) $ Abs (_, _, pred))) =
8.159 - (Tactic.Check_elementwise (Rule.term_to_string''' thy pred), Tactic.Empty_Tac_)
8.160 - | stac2tac_ _ _ (Const("Prog_Tac.Or'_to'_List", _) $ _ ) = (Tactic.Or_to_List, Tactic.Empty_Tac_)
8.161 -
8.162 - (*compare "| associate _ (Subproblem'" ..TODO: extract common code *)
8.163 - | stac2tac_ pt _ (stac as Const ("Prog_Tac.SubProblem", _) $ spec' $ ags') =
8.164 - let
8.165 - val (dI, pI, mI) = Prog_Tac.dest_spec spec'
8.166 - val thy = Stool.common_subthy (Celem.assoc_thy dI, rootthy pt);
8.167 - val ags = TermC.isalist2list ags';
8.168 - val (pI, pors, mI) =
8.169 - if mI = ["no_met"]
8.170 - then
8.171 - let
8.172 - val pors = (Chead.match_ags thy ((#ppc o Specify.get_pbt) pI) ags)
8.173 - (* Chead.match_ags : theory -> pat list -> term list -> ori list
8.174 - ^^^ variables ^^^ values *)
8.175 - handle ERROR "actual args do not match formal args"
8.176 - => (Chead.match_ags_msg pI stac ags(*raise exn*); [])
8.177 - val pI' = Specify.refine_ori' pors pI;
8.178 - in (pI', pors (* refinement over models with diff.prec only *),
8.179 - (hd o #met o Specify.get_pbt) pI') end
8.180 - else (pI, (Chead.match_ags thy ((#ppc o Specify.get_pbt) pI) ags)
8.181 - handle ERROR "actual args do not match formal args"
8.182 - => (Chead.match_ags_msg pI stac ags(*raise exn*); []), mI);
8.183 - val (fmz_, vals) = Chead.oris2fmz_vals pors;
8.184 - val {cas,ppc,thy,...} = Specify.get_pbt pI
8.185 - val dI = Rule.theory2theory' thy (*.take dI from _refined_ pbl.*)
8.186 - val dI = Rule.theory2theory' (Stool.common_subthy (Celem.assoc_thy dI, rootthy pt));
8.187 - val ctxt = ContextC.initialise dI vals
8.188 - val hdl =
8.189 - case cas of
8.190 - NONE => Auto_Prog.pblterm dI pI
8.191 - | SOME t => subst_atomic ((Chead.vars_of_pbl_' ppc) ~~~ vals) t
8.192 - val f = Auto_Prog.subpbl (strip_thy dI) pI
8.193 - in (Tactic.Subproblem (dI, pI), Tactic.Subproblem' ((dI, pI, mI), pors, hdl, fmz_, ctxt, f))
8.194 - end
8.195 - | stac2tac_ _ thy t = error ("stac2tac_ TODO: no match for " ^ Rule.term_to_string''' thy t);
8.196 -
8.197 -fun stac2tac pt thy t = (fst o stac2tac_ pt thy) t;
8.198 -
8.199 -datatype ass =
8.200 - Ass of
8.201 - Tactic.T (* SubProblem gets args instantiated in associate *)
8.202 - * term (* for itr_arg, result in ets *)
8.203 - * Proof.context (* separate from Tactic.T like in locate_input_tactic *)
8.204 - | Ass_Weak of Tactic.T * term * Proof.context
8.205 - | NotAss;
8.206 -
8.207 -(* check if tac_ is associated with stac.
8.208 - Note: this is the only fun in "fun locate_input_tactic", which handles tactics individually.
8.209 - Additional tasks:
8.210 - (1) to "Subproblem'" add "pors, hdl, fmz_, ctxt, f" TODO: ctxt <-?-> sig locate_input_tac
8.211 - (2) check if term t (the result has been calculated from) in tac_
8.212 - has been changed (see "datatype tac_"); if yes, recalculate result
8.213 - TODO.WN120106 recalculate impl.only for Substitute'
8.214 -args
8.215 - pt : ctree for pushing the thy specified in rootpbl into subpbls
8.216 - d : unused (planned for data for comparison)
8.217 - tac_ : from user (via applicable_in); to be compared with ...
8.218 - stac : found in program
8.219 -returns
8.220 - Ass : associated: e.g. thmID in stac = thmID in m
8.221 - +++ arg in stac = arg in m
8.222 - Ass_Weak: weakly ass.:e.g. thmID in stac = thmID in m, //arg//
8.223 - NotAss : e.g. thmID in stac/=/thmID in m (not =)
8.224 -*)
8.225 -fun associate _ ctxt (m as Tactic.Rewrite_Inst'
8.226 - (_, _, _, _, _, thm'' as (thmID, _), f, (f', asms')), stac) =
8.227 - (case stac of
8.228 - (Const ("Prog_Tac.Rewrite'_Inst", _) $ _ $ thmID_ $ f_) =>
8.229 - if thmID = HOLogic.dest_string thmID_
8.230 - then
8.231 - if f = f_
8.232 - then Ass (m, f', ContextC.insert_assumptions asms' ctxt)
8.233 - else Ass_Weak (m, f', ContextC.insert_assumptions asms' ctxt)
8.234 - else ((*tracing"3### associate ..NotAss";*) NotAss)
8.235 - | (Const ("Prog_Tac.Rewrite'_Set'_Inst",_) $ _ $ rls_ $ f_) =>
8.236 - if Rtools.contains_rule (Rule.Thm thm'') (assoc_rls (HOLogic.dest_string rls_))
8.237 - then if f = f_ then Ass (m, f', ContextC.insert_assumptions asms' ctxt)
8.238 - else Ass_Weak (m, f', ContextC.insert_assumptions asms' ctxt)
8.239 - else NotAss
8.240 - | _ => NotAss)
8.241 - | associate _ ctxt (m as Tactic.Rewrite' (_, _, _, _, thm'' as (thmID, _), f, (f', asms')), stac) =
8.242 - (case stac of
8.243 - (Const ("Prog_Tac.Rewrite", _) $ thmID_ $ f_) =>
8.244 - if thmID = HOLogic.dest_string thmID_
8.245 - then
8.246 - if f = f_
8.247 - then Ass (m, f', ContextC.insert_assumptions asms' ctxt)
8.248 - else Ass_Weak (m, f', ContextC.insert_assumptions asms' ctxt)
8.249 - else NotAss
8.250 - | (Const ("Prog_Tac.Rewrite'_Set", _) $ rls_ $ f_) =>
8.251 - if Rtools.contains_rule (Rule.Thm thm'') (assoc_rls (HOLogic.dest_string rls_))
8.252 - then
8.253 - if f = f_
8.254 - then Ass (m, f', ContextC.insert_assumptions asms' ctxt)
8.255 - else Ass_Weak (m, f', ContextC.insert_assumptions asms' ctxt)
8.256 - else NotAss
8.257 - | _ => NotAss)
8.258 - | associate _ ctxt (m as Tactic.Rewrite_Set_Inst' (_, _, _, rls, f, (f', asms')),
8.259 - (Const ("Prog_Tac.Rewrite'_Set'_Inst", _) $ _ $ rls_ $ f_)) =
8.260 - if Rule.id_rls rls = HOLogic.dest_string rls_
8.261 - then
8.262 - if f = f_
8.263 - then Ass (m, f', ContextC.insert_assumptions asms' ctxt)
8.264 - else Ass_Weak (m ,f', ContextC.insert_assumptions asms' ctxt)
8.265 - else NotAss
8.266 - | associate _ ctxt (m as Tactic.Detail_Set_Inst' (_, _, _, rls, f, (f', asms')),
8.267 - (Const ("Prog_Tac.Rewrite'_Set'_Inst", _) $ _ $ rls_ $ f_)) =
8.268 - if Rule.id_rls rls = HOLogic.dest_string rls_
8.269 - then
8.270 - if f = f_
8.271 - then Ass (m, f', ContextC.insert_assumptions asms' ctxt)
8.272 - else Ass_Weak (m ,f', ContextC.insert_assumptions asms' ctxt)
8.273 - else NotAss
8.274 - | associate _ ctxt (m as Tactic.Rewrite_Set' (_, _, rls, f, (f', asms')),
8.275 - (Const ("Prog_Tac.Rewrite'_Set", _) $ rls_ $ f_)) =
8.276 - if Rule.id_rls rls = HOLogic.dest_string rls_
8.277 - then
8.278 - if f = f_
8.279 - then Ass (m, f', ContextC.insert_assumptions asms' ctxt)
8.280 - else Ass_Weak (m ,f', ContextC.insert_assumptions asms' ctxt)
8.281 - else NotAss
8.282 - | associate _ ctxt (m as Tactic.Detail_Set' (_, _, rls, f, (f', asms')),
8.283 - (Const ("Prog_Tac.Rewrite'_Set", _) $ rls_ $ f_)) =
8.284 - if Rule.id_rls rls = HOLogic.dest_string rls_
8.285 - then
8.286 - if f = f_
8.287 - then Ass (m, f', ContextC.insert_assumptions asms' ctxt)
8.288 - else Ass_Weak (m ,f', ContextC.insert_assumptions asms' ctxt)
8.289 - else NotAss
8.290 - | associate _ ctxt (m as Tactic.Calculate' (_, op_, f, (f', _)), stac) =
8.291 - (case stac of
8.292 - (Const ("Prog_Tac.Calculate",_) $ op__ $ f_) =>
8.293 - if op_ = HOLogic.dest_string op__
8.294 - then
8.295 - if f = f_
8.296 - then Ass (m, f', ctxt)
8.297 - else Ass_Weak (m ,f', ctxt)
8.298 - else NotAss
8.299 - | (Const ("Prog_Tac.Rewrite'_Set'_Inst", _) $ _ $ rls_ $ f_) =>
8.300 - let val thy = Celem.assoc_thy "Isac_Knowledge";
8.301 - in
8.302 - if Rtools.contains_rule (Rule.Num_Calc (assoc_calc' thy op_ |> snd))
8.303 - (assoc_rls (HOLogic.dest_string rls_))
8.304 - then
8.305 - if f = f_
8.306 - then Ass (m, f', ctxt)
8.307 - else Ass_Weak (m ,f', ctxt)
8.308 - else NotAss
8.309 - end
8.310 - | (Const ("Prog_Tac.Rewrite'_Set",_) $ rls_ $ f_) =>
8.311 - let val thy = Celem.assoc_thy "Isac_Knowledge";
8.312 - in
8.313 - if Rtools.contains_rule (Rule.Num_Calc (assoc_calc' thy op_ |> snd))
8.314 - (assoc_rls (HOLogic.dest_string rls_))
8.315 - then
8.316 - if f = f_
8.317 - then Ass (m, f', ctxt)
8.318 - else Ass_Weak (m ,f', ctxt)
8.319 - else NotAss
8.320 - end
8.321 - | _ => NotAss)
8.322 - | associate _ ctxt (m as Tactic.Check_elementwise' (consts, _, (consts_chkd, _)),
8.323 - (Const ("Prog_Tac.Check'_elementwise",_) $ consts' $ _)) =
8.324 - if consts = consts'
8.325 - then Ass (m, consts_chkd, ctxt)
8.326 - else NotAss
8.327 - | associate _ ctxt (m as Tactic.Or_to_List' (_, list), (Const ("Prog_Tac.Or'_to'_List", _) $ _)) =
8.328 - Ass (m, list, ctxt)
8.329 - | associate _ ctxt (m as Tactic.Take' term, (Const ("Prog_Tac.Take", _) $ _)) = Ass (m, term, ctxt)
8.330 - | associate _ ctxt (m as Tactic.Substitute' (ro, erls, subte, f, f'),
8.331 - (Const ("Prog_Tac.Substitute", _) $ _ $ t)) =
8.332 - if f = t then Ass (m, f', ctxt)
8.333 - else (*compare | applicable_in (p,p_) pt (m as Substitute sube)*)
8.334 - if foldl and_ (true, map TermC.contains_Var subte)
8.335 - then
8.336 - let val t' = subst_atomic (map HOLogic.dest_eq subte (*TODO subte2subst*)) t
8.337 - in if t = t' then error "associate: Substitute' not applicable to val of Expr"
8.338 - else Ass (Tactic.Substitute' (ro, erls, subte, t, t'), t', ctxt)
8.339 - end
8.340 - else (case Rewrite.rewrite_terms_ (Rule.Isac ()) ro erls subte t of
8.341 - SOME (t', _) => Ass (Tactic.Substitute' (ro, erls, subte, t, t'), t', ctxt)
8.342 - | NONE => error "associate: Substitute' not applicable to val of Expr")
8.343 -
8.344 - (*compare "| stac2tac_ thy (Const ("Prog_Tac.SubProblem",_)" ..TODO: extract common code *)
8.345 - | associate pt _ (Tactic.Subproblem' ((domID, pblID, _), _, _, _, _, _),
8.346 - (stac as Const ("Prog_Tac.SubProblem", _) $ spec' $ ags')) =
8.347 - let
8.348 - val (dI, pI, mI) = Prog_Tac.dest_spec spec'
8.349 - val thy = Stool.common_subthy (Celem.assoc_thy dI, rootthy pt);
8.350 - val ags = TermC.isalist2list ags';
8.351 - val (pI, pors, mI) =
8.352 - if mI = ["no_met"]
8.353 - then
8.354 - let
8.355 - val pors = (Chead.match_ags thy ((#ppc o Specify.get_pbt) pI) ags)
8.356 - handle ERROR "actual args do not match formal args"
8.357 - => (Chead.match_ags_msg pI stac ags(*raise exn*);[]);
8.358 - val pI' = Specify.refine_ori' pors pI;
8.359 - in (pI', pors (*refinement over models with diff.prec only*), (hd o #met o Specify.get_pbt) pI')
8.360 - end
8.361 - else (pI, (Chead.match_ags thy ((#ppc o Specify.get_pbt) pI) ags)
8.362 - handle ERROR "actual args do not match formal args"
8.363 - => (Chead.match_ags_msg pI stac ags(*raise exn*); []), mI);
8.364 - val (fmz_, vals) = Chead.oris2fmz_vals pors;
8.365 - val {cas, ppc, thy, ...} = Specify.get_pbt pI
8.366 - val dI = Rule.theory2theory' thy (*take dI from _refined_ pbl*)
8.367 - val dI = Rule.theory2theory' (Stool.common_subthy (Celem.assoc_thy dI, rootthy pt))
8.368 - val ctxt = ContextC.initialise dI vals
8.369 - val hdl =
8.370 - case cas of
8.371 - NONE => Auto_Prog.pblterm dI pI
8.372 - | SOME t => subst_atomic ((Chead.vars_of_pbl_' ppc) ~~~ vals) t
8.373 - val f = Auto_Prog.subpbl (strip_thy dI) pI
8.374 - in
8.375 - if domID = dI andalso pblID = pI
8.376 - then Ass (Tactic.Subproblem' ((dI, pI, mI), pors, hdl, fmz_, ContextC.e_ctxt(*TODO rm*), f), f, ctxt)
8.377 - else NotAss
8.378 - end
8.379 - | associate _ _ (m, _) =
8.380 - (if (!trace_script)
8.381 - then tracing("@@@ the 'tac_' proposed to apply does NOT match the leaf found in the script:\n"
8.382 - ^ "@@@ tac_ = " ^ Tactic.string_of m)
8.383 - else ();
8.384 - NotAss);
8.385 -
8.386 -(* create the initial interpreter state
8.387 - from the items of the guard and the formal arguments of the partial_function.
8.388 -Note on progression from (a) type fmz_ \<longrightarrow> (e) arguments of the partial_function:
8.389 - (a) fmz is given by a math author
8.390 - (b) fmz_ is transformed to ori list as a prerequisite for efficient interactive modelling
8.391 - (c) modelling creates an itm list from ori list + possible user input
8.392 - (d) specifying a theory might add some items and create a guard for the partial_function
8.393 - (e) fun relate_args creates an environment for evaluating the partial_function.
8.394 -Note on sequence-relation (a) -- (e), i.e. the (formal) arguments of the partial_function:
8.395 - * Since the arguments of the partial_function have no description (see Descript.thy),
8.396 - (e) depends on the sequence in fmz_ and on the types of the formal arguments.
8.397 - * pairing formal arguments with itm's follows the sequence
8.398 - * Thus the resulting sequence-relation can be ambiguous.
8.399 - * Ambiguities are done by rearranging fmz_ or the formal arguments.
8.400 - * The latter is easier, albeit not optimal: a fmz_ can be used by different partial_functions.
8.401 - *)
8.402 -local
8.403 -val errmsg = "ERROR: found no actual arguments for prog. of "
8.404 -fun msg_miss sc metID caller f formals actuals =
8.405 - "ERROR in creating the environment from formal args. of partial_function \"" ^ fst (Program.get_fun_id sc) ^ "\"\n" ^
8.406 - "and the actual args., ie. items of the guard of \"" ^ Celem.metID2str metID ^ "\" by \"" ^ caller ^ "\":\n" ^
8.407 - "formal arg \"" ^ Rule.term2str f ^ "\" doesn't mach an actual arg.\n" ^
8.408 - "with:\n" ^
8.409 - (string_of_int o length) formals ^ " formal args: " ^ Rule.terms2str formals ^ "\n" ^
8.410 - (string_of_int o length) actuals ^ " actual args: " ^ Rule.terms2str actuals
8.411 -fun msg_miss_type sc metID f formals actuals =
8.412 - "ERROR in creating the environment from formal args. of partial_function \"" ^ fst (Program.get_fun_id sc) ^ "\"\n" ^
8.413 - "and the actual args., ie. items of the guard of \"" ^ Celem.metID2str metID ^ "\" by \"assoc_by_type\":\n" ^
8.414 - "formal arg \"" ^ Rule.term2str f ^ "\" of type \"" ^ Rule.type2str (type_of f) ^
8.415 - "\" doesn't mach an actual arg.\nwith:\n" ^
8.416 - (string_of_int o length) formals ^ " formal args: " ^ Rule.terms2str formals ^ "\n" ^
8.417 - (string_of_int o length) actuals ^ " actual args: " ^ Rule.terms2str actuals ^ "\n" ^
8.418 - " with types: " ^ (strs2str o (map (Rule.type2str o type_of))) actuals
8.419 -fun msg_ambiguous sc metID f aas formals actuals =
8.420 - "AMBIGUITY in creating the environment from formal args. of partial_function \"" ^ fst (Program.get_fun_id sc) ^ "\"\n" ^
8.421 - "and the actual args., ie. items of the guard of \"" ^ Celem.metID2str metID ^ "\" by \"assoc_by_type\":\n" ^
8.422 - "formal arg. \"" ^ Rule.term2str f ^ "\" type-matches with several..." ^
8.423 - "actual args. \"" ^ Rule.terms2str aas ^ "\"\n" ^
8.424 - "selected \"" ^ Rule.term2str (hd aas) ^ "\"\n" ^
8.425 - "with\n" ^
8.426 - "formals: " ^ Rule.terms2str formals ^ "\n" ^
8.427 - "actuals: " ^ Rule.terms2str actuals
8.428 -fun trace_init metID =
8.429 - if (!trace_script)
8.430 - then tracing("@@@ program " ^ strs2str metID)
8.431 - else ();
8.432 -fun trace_istate env =
8.433 - if (!trace_script)
8.434 - then tracing("@@@ istate " ^ Env.env2str env)
8.435 - else ();
8.436 -in
8.437 -fun init_pstate srls ctxt itms metID =
8.438 - let
8.439 - val itms = Specify.hack_until_review_Specify_2 metID itms
8.440 - val actuals = itms2args (Proof_Context.theory_of ctxt) metID itms
8.441 - val _ = if actuals <> [] then () else raise ERROR (errmsg ^ strs2str' metID)
8.442 - val (scr, sc) = (case (#scr o Specify.get_met) metID of
8.443 - scr as Rule.Prog sc => (trace_init metID; (scr, sc))
8.444 - | _ => raise ERROR ("init_pstate with " ^ Celem.metID2str metID))
8.445 - val formals = Program.formal_args sc
8.446 - fun assoc_by_type f aa =
8.447 - case filter (curry (fn (f, a) => type_of f = type_of a) f) aa of
8.448 - [] => error (msg_miss_type sc metID f formals actuals)
8.449 - | [a] => (f, a)
8.450 - | aas as (a :: _) => (writeln (msg_ambiguous sc metID f aas formals actuals); (f, a));
8.451 - fun relate_args _ (f::_) [] = error (msg_miss sc metID "relate_args" f formals actuals)
8.452 - | relate_args env [] _ = env (*may drop Find?*)
8.453 - | relate_args env (f::ff) (aas as (a::aa)) =
8.454 - if type_of f = type_of a
8.455 - then relate_args (env @ [(f, a)]) ff aa
8.456 - else
8.457 - let val (f, a) = assoc_by_type f aas
8.458 - in relate_args (env @ [(f, a)]) ff (remove op = a aas) end
8.459 - val {pre, prls, ...} = Specify.get_met metID;
8.460 - val pres = Stool.check_preconds (Proof_Context.theory_of ctxt) prls pre itms |> map snd;
8.461 - val ctxt = ctxt |> ContextC.insert_assumptions pres;
8.462 - val ist = Istate.e_pstate
8.463 - |> Istate.set_eval srls
8.464 - |> Istate.set_env_true (relate_args [] formals actuals)
8.465 - in
8.466 - (Istate.Pstate ist, ctxt, scr)
8.467 - end;
8.468 -end (*local*)
8.469 -
8.470 -fun get_simplifier (pt, (p, _)) =
8.471 - let
8.472 - val p' = Ctree.par_pblobj pt p
8.473 - val metID = Ctree.get_obj Ctree.g_metID pt p'
8.474 - val {srls, ...} = Specify.get_met metID
8.475 - in srls end
8.476 -
8.477 -(* decide, where to get program/istate from:
8.478 - (* 1 *) from PblObj.Env.update: at begin of program if no init_form
8.479 - (* 2 *) from PblObj/PrfObj: if Prog_Tac is in the middle of the program
8.480 - (* 3 *) from rls/PrfObj: in case of Math_Engine.detailstep *)
8.481 -fun from_pblobj_or_detail' _ (p, p_) pt =
8.482 - if member op = [Pbl, Met] p_
8.483 - then case get_obj g_env (*?DEPRECATED?*) pt p of
8.484 - NONE => error "from_pblobj_or_detail': no istate"
8.485 - | SOME (Istate.Pstate pst, ctxt) =>
8.486 - let
8.487 - val metID = get_obj g_metID pt p
8.488 - val {srls, ...} = Specify.get_met metID
8.489 - in
8.490 - (srls, (Istate.Pstate (Istate.set_eval srls pst), ctxt), (#scr o Specify.get_met) metID)
8.491 - end
8.492 - | _ => raise ERROR "from_pblobj_or_detail': unexpected result from g_env"
8.493 - else
8.494 - let val (pbl, p', rls') = par_pbl_det pt p
8.495 - in if pbl
8.496 - then (*if last_elem p = 0 nothing written to pt yet*) (* 2 *)
8.497 - let
8.498 - val metID = get_obj g_metID pt p'
8.499 - val {srls, ...} = Specify.get_met metID
8.500 - val (is, ctxt) =
8.501 - case get_loc pt (p, p_) of
8.502 - (Istate.Pstate ist, ctxt) => (Istate.Pstate (Istate.set_eval srls ist), ctxt)
8.503 - | _ => raise ERROR "from_pblobj_or_detail': unexpected result from get_loc"
8.504 - in (srls, (is, ctxt), (#scr o Specify.get_met) metID) end
8.505 - else
8.506 - let
8.507 - (*TODO.thy Auto_Prog.generate SHOULD REPLACE ALL HIS..*)
8.508 - val prog = case rls' of
8.509 - Rule.Rls {scr = Rule.Prog prog,...} => prog
8.510 - | Rule.Seq {scr = Rule.Prog prog,...} => prog
8.511 - | _ => raise ERROR ("from_pblobj_or_detail': not for rule-set \"" ^ Rule.id_rls rls' ^ "\"")
8.512 - val t = get_last_formula (pt, (p, p_))
8.513 - val prog' = Auto_Prog.subst_typs prog (type_of t) (TermC.guess_bdv_typ t)
8.514 - in (Rule.e_rls(*!!!*), get_loc pt (p, p_), Rule.Prog prog') end
8.515 - end
8.516 -
8.517 -fun from_pblobj' thy' (p,p_) pt = (*.get script and istate, UNUSED; see above ( * 1 *)
8.518 - let
8.519 - val p' = par_pblobj pt p
8.520 - val itms =
8.521 - (case get_obj I pt p' of
8.522 - PblObj {meth = itms, ...} => itms
8.523 - | PrfObj _ => error "from_pblobj' NOT with PrfObj")
8.524 - val metID = get_obj g_metID pt p'
8.525 - val {srls, scr, ...} = Specify.get_met metID
8.526 - in
8.527 - if last_elem p = 0 (*nothing written to pt yet*)
8.528 - then
8.529 - let
8.530 - val ctxt = ContextC.initialise thy' (Model.vars_of itms)
8.531 - val (is, ctxt, scr) = init_pstate srls ctxt itms metID
8.532 - in (srls(*..\<in> is*), (is, ctxt), scr) end
8.533 - else (srls(*..\<in> is*), get_loc pt (p,p_), scr)
8.534 - end;
8.535 -
8.536 -(*.get the stactics and problems of a script as tacs
8.537 - instantiated with the current environment;
8.538 - l is the location which generated the given formula.*)
8.539 -(*WN.12.5.03: quick-and-dirty repair for listexpressions*)
8.540 -fun is_spec_pos Pbl = true
8.541 - | is_spec_pos Met = true
8.542 - | is_spec_pos _ = false;
8.543 -
8.544 -(* handle a leaf at the end of recursive descent:
8.545 - a leaf is either a tactic or an 'expr' in "let v = expr"
8.546 - where "expr" does not contain a tactic.
8.547 - Handling a leaf comprises
8.548 - (1) 'subst_stacexpr' substitute Env.update and complete curried tactic
8.549 - (2) rewrite the leaf by 'srls'
8.550 -*)
8.551 -fun check_leaf call ctxt srls (E, (a, v)) t =
8.552 - case Prog_Tac.eval_leaf E a v t of
8.553 - (Program.Tac stac, a') =>
8.554 - let val stac' =
8.555 - Rewrite.eval_prog_expr (Proof_Context.theory_of ctxt) srls
8.556 - (subst_atomic (Env.update_opt E (a,v)) stac)
8.557 - in
8.558 - (if (! trace_script)
8.559 - then tracing ("@@@ " ^ call ^ " leaf '" ^ Rule.term2str t ^ "' ---> Tac '" ^ Rule.term2str stac ^ "'")
8.560 - else ();
8.561 - (Program.Tac stac', a'))
8.562 - end
8.563 - | (Program.Expr lexpr, a') =>
8.564 - let val lexpr' =
8.565 - Rewrite.eval_prog_expr (Proof_Context.theory_of ctxt) srls (subst_atomic (Env.update_opt E (a,v)) lexpr)
8.566 - in
8.567 - (if (! trace_script)
8.568 - then tracing("@@@ "^call^" leaf '" ^ Rule.term2str t ^ "' ---> Expr '" ^ Rule.term2str lexpr' ^ "'")
8.569 - else ();
8.570 - (Program.Expr lexpr', a')) (*lexpr' is the value of the Expr*)
8.571 - end;
8.572 -
8.573 -(*. fetch _all_ tactics from script .*)
8.574 -fun sel_rules _ (([],Res):pos') =
8.575 - raise PTREE "no tactics applicable at the end of a calculation"
8.576 - | sel_rules pt (p,p_) =
8.577 - if is_spec_pos p_
8.578 - then [get_obj g_tac pt p]
8.579 - else
8.580 - let
8.581 - val pp = par_pblobj pt p;
8.582 - val thy' = get_obj g_domID pt pp;
8.583 - val thy = Celem.assoc_thy thy';
8.584 - val metID = get_obj g_metID pt pp;
8.585 - val metID' = if metID = Celem.e_metID then (thd3 o snd3) (get_obj g_origin pt pp) else metID
8.586 - val (sc, srls) = (case Specify.get_met metID' of
8.587 - {scr = Rule.Prog sc, srls, ...} => (sc, srls) | _ => error "sel_rules 1")
8.588 - val subst = get_istate pt (p, p_) |> Istate.the_pstate |> Istate.get_subst
8.589 - val ctxt = get_ctxt pt (p, p_)
8.590 - in map ((stac2tac pt thy) o Program.rep_stacexpr o #1 o
8.591 - (check_leaf "selrul" ctxt srls subst)) (Auto_Prog.stacpbls sc)
8.592 - end;
8.593 -
8.594 -(* fetch tactics from script and filter _applicable_ tactics;
8.595 - in case of Rewrite_Set* go down to _atomic_ rewrite-tactics *)
8.596 -fun sel_appl_atomic_tacs _ (([], Res) : pos') =
8.597 - raise PTREE "no tactics applicable at the end of a calculation"
8.598 - | sel_appl_atomic_tacs pt (p, p_) =
8.599 - if is_spec_pos p_
8.600 - then [get_obj g_tac pt p]
8.601 - else
8.602 - let
8.603 - val pp = par_pblobj pt p
8.604 - val thy' = get_obj g_domID pt pp
8.605 - val thy = Celem.assoc_thy thy'
8.606 - val metID = get_obj g_metID pt pp
8.607 - val metID' =
8.608 - if metID = Celem.e_metID
8.609 - then (thd3 o snd3) (get_obj g_origin pt pp)
8.610 - else metID
8.611 - val (sc, srls, erls, ro) = (case Specify.get_met metID' of
8.612 - {scr = Rule.Prog sc, srls, erls, rew_ord' = ro, ...} => (sc, srls, erls, ro)
8.613 - | _ => error "sel_appl_atomic_tacs 1")
8.614 - val (env, (a, v)) = (case get_istate pt (p, p_) of
8.615 - Istate.Pstate pst => (Istate.get_subst pst) | _ => error "sel_appl_atomic_tacs 2")
8.616 - val ctxt = get_ctxt pt (p, p_)
8.617 - val alltacs = (*we expect at least 1 stac in a script*)
8.618 - map ((stac2tac pt thy) o Program.rep_stacexpr o #1 o
8.619 - (check_leaf "selrul" ctxt srls (env, (a, v)))) (Auto_Prog.stacpbls sc)
8.620 - val f =
8.621 - (case p_ of Frm => get_obj g_form pt p | Res => (fst o (get_obj g_result pt)) p
8.622 - | _ => error "")
8.623 - (*WN071231 ? replace atomic_appl_tacs with applicable_in (ineff!) ?*)
8.624 - in ((gen_distinct Tactic.eq_tac) o flat o (map (Rtools.atomic_appl_tacs thy ro erls f))) alltacs end;
8.625 -
8.626 -(**)end(**)
9.1 --- a/src/Tools/isac/Interpret/step-solve.sml Tue Feb 04 16:45:36 2020 +0100
9.2 +++ b/src/Tools/isac/Interpret/step-solve.sml Tue Feb 04 17:11:54 2020 +0100
9.3 @@ -23,11 +23,11 @@
9.4 PblObj {meth=itms, ...} => itms
9.5 | _ => error "Step_Solve.by_tactic Apply_Method: uncovered case get_obj"
9.6 val thy = Celem.assoc_thy (get_obj g_domID pt p);
9.7 - val srls = Lucin.get_simplifier (pt, pos)
9.8 - val (is, env, ctxt, sc) = case Lucin.init_pstate srls ctxt itms mI of
9.9 + val srls = LItool.get_simplifier (pt, pos)
9.10 + val (is, env, ctxt, sc) = case LItool.init_pstate srls ctxt itms mI of
9.11 (is as Istate.Pstate {env, ...}, ctxt, sc) => (is, env, ctxt, sc)
9.12 | _ => error "Step_Solve.by_tactic Apply_Method: uncovered case init_pstate"
9.13 - val ini = Lucin.init_form thy sc env;
9.14 + val ini = LItool.init_form thy sc env;
9.15 in
9.16 case ini of
9.17 SOME t =>
9.18 @@ -41,12 +41,12 @@
9.19 | NONE =>
9.20 let
9.21 val (m', is', ctxt') =
9.22 - case LucinNEW.find_next_step sc (pt, (lev_dn p, Res)) is ctxt of
9.23 - LucinNEW.Next_Step (ist, ctxt, tac) => (tac, ist, ctxt)
9.24 + case Lucin.find_next_step sc (pt, (lev_dn p, Res)) is ctxt of
9.25 + Lucin.Next_Step (ist, ctxt, tac) => (tac, ist, ctxt)
9.26 | _ => raise ERROR ("Step_Solve.by_tactic Apply_Method " ^ strs2str' mI)
9.27 in
9.28 - case LucinNEW.locate_input_tactic sc (pt, (lev_dn p, Res)) is' ctxt' m' of
9.29 - LucinNEW.Safe_Step (istate, ctxt, tac) =>
9.30 + case Lucin.locate_input_tactic sc (pt, (lev_dn p, Res)) is' ctxt' m' of
9.31 + Lucin.Safe_Step (istate, ctxt, tac) =>
9.32 let
9.33 val (p'', _, _,pt') =
9.34 Generate.generate1 (Celem.assoc_thy "Isac_Knowledge") tac
9.35 @@ -77,12 +77,12 @@
9.36 val {scr, ...} = Specify.get_met (get_obj g_metID pt pp);
9.37 val (ist, ctxt) = get_loc pt pos
9.38 val prog_res =
9.39 - case LucinNEW.find_next_step scr (pt, pos) ist ctxt of
9.40 - LucinNEW.Next_Step (_, _, Tactic.Check_elementwise' (_, _, (prog_res, _))) => prog_res
9.41 - | LucinNEW.End_Program (_, Tactic.Check_Postcond' (_, (prog_res, _))) => prog_res
9.42 + case Lucin.find_next_step scr (pt, pos) ist ctxt of
9.43 + Lucin.Next_Step (_, _, Tactic.Check_elementwise' (_, _, (prog_res, _))) => prog_res
9.44 + | Lucin.End_Program (_, Tactic.Check_Postcond' (_, (prog_res, _))) => prog_res
9.45 | _ => raise ERROR ("Step_Solve.by_tactic Check_Postcond " ^ strs2str' pI)
9.46 in (*from Applicable.applicable_in not yet available -----vvvvvvvv*)
9.47 - (LucinNEW.by_tactic (Tactic.Check_Postcond' (pI, (prog_res, [(*fill.later*)])))
9.48 + (Lucin.by_tactic (Tactic.Check_Postcond' (pI, (prog_res, [(*fill.later*)])))
9.49 (Istate.e_istate, ContextC.e_ctxt) ptp)
9.50 end
9.51 | by_tactic (Tactic.End_Proof'') ptp = ("end-proof", ([], [], ptp))
9.52 @@ -106,10 +106,10 @@
9.53 else
9.54 let
9.55 val thy' = get_obj g_domID pt (par_pblobj pt p);
9.56 - val (_, is, sc) = Lucin.from_pblobj_or_detail' thy' (p,p_) pt;
9.57 + val (_, is, sc) = LItool.from_pblobj_or_detail' thy' (p,p_) pt;
9.58 in
9.59 - case LucinNEW.locate_input_tactic sc (pt, po) (fst is) (snd is) m of
9.60 - LucinNEW.Safe_Step (istate, ctxt, tac) =>
9.61 + case Lucin.locate_input_tactic sc (pt, po) (fst is) (snd is) m of
9.62 + Lucin.Safe_Step (istate, ctxt, tac) =>
9.63 let
9.64 val p' = next_in_prog po
9.65 val (p'', _, _,pt') =
9.66 @@ -118,7 +118,7 @@
9.67 ("ok", ([(Tactic.input_from_T tac, tac, (p'', (istate, ctxt)))],
9.68 [(*ctree NOT cut*)], (pt', p'')))
9.69 end
9.70 - | LucinNEW.Unsafe_Step (istate, ctxt, tac) =>
9.71 + | Lucin.Unsafe_Step (istate, ctxt, tac) =>
9.72 let
9.73 val p' =
9.74 case p_ of Frm => p
9.75 @@ -126,7 +126,7 @@
9.76 | _ => error ("Step_Solve.by_tactic: call by " ^ pos'2str (p, p_));
9.77 val (p'', _, _,pt') =
9.78 Generate.generate1 (Celem.assoc_thy "Isac_Knowledge") tac
9.79 - (* DEL.^^^^^ ContextC.insert_assumptions asms' ctxt 2nd, fst in Lucin.associate *)
9.80 + (* DEL.^^^^^ ContextC.insert_assumptions asms' ctxt 2nd, fst in LItool.associate *)
9.81 (istate, ctxt) (p', p_) pt;
9.82 in
9.83 ("ok", ([(Tactic.input_from_T tac, tac, (p'', (istate, ctxt)))],
9.84 @@ -140,6 +140,6 @@
9.85 end
9.86 end;
9.87
9.88 -val do_next = LucinNEW.do_next
9.89 +val do_next = Lucin.do_next
9.90
9.91 end
10.1 --- a/src/Tools/isac/MathEngine/solve.sml Tue Feb 04 16:45:36 2020 +0100
10.2 +++ b/src/Tools/isac/MathEngine/solve.sml Tue Feb 04 17:11:54 2020 +0100
10.3 @@ -89,7 +89,7 @@
10.4 let
10.5 val (_, _, mI) = get_obj g_spec pt p
10.6 val ctxt = get_ctxt pt pos
10.7 - val (_, (_, c', ptp)) = LucinNEW.by_tactic (Tactic.Apply_Method' (mI, NONE, Istate.e_istate, ctxt)) (Istate.e_istate, ctxt) ptp
10.8 + val (_, (_, c', ptp)) = Lucin.by_tactic (Tactic.Apply_Method' (mI, NONE, Istate.e_istate, ctxt)) (Istate.e_istate, ctxt) ptp
10.9 in
10.10 complete_solve auto (c @ c') ptp
10.11 end;
10.12 @@ -152,10 +152,10 @@
10.13 val istate = get_istate pt pos
10.14 val ctxt = get_ctxt pt pos
10.15 in
10.16 - case LucinNEW.locate_input_term prog (pt, pos) istate ctxt f_in of
10.17 - LucinNEW.Found_Step (cstate, _(*istate*), _(*ctxt*)) =>
10.18 + case Lucin.locate_input_term prog (pt, pos) istate ctxt f_in of
10.19 + Lucin.Found_Step (cstate, _(*istate*), _(*ctxt*)) =>
10.20 ("ok" , ([], [], cstate (* already contains istate, ctxt *)))
10.21 - | LucinNEW.Not_Derivable calcstate' =>
10.22 + | Lucin.Not_Derivable calcstate' =>
10.23 let
10.24 val pp = Ctree.par_pblobj pt p
10.25 val (errpats, nrls, prog) = case Specify.get_met (Ctree.get_obj Ctree.g_metID pt pp) of
11.1 --- a/src/Tools/isac/MathEngine/step.sml Tue Feb 04 16:45:36 2020 +0100
11.2 +++ b/src/Tools/isac/MathEngine/step.sml Tue Feb 04 17:11:54 2020 +0100
11.3 @@ -29,7 +29,7 @@
11.4 in
11.5 case tac of
11.6 Tactic.Apply_Method mI =>
11.7 - LucinNEW.by_tactic (Tactic.Apply_Method' (mI, NONE, Istate.e_istate, ContextC.e_ctxt))
11.8 + Lucin.by_tactic (Tactic.Apply_Method' (mI, NONE, Istate.e_istate, ContextC.e_ctxt))
11.9 ist_ctxt (pt, (p, p_'))
11.10 | _ => ("dummy", Step_Specify.by_tactic tac (pt, (p, p_')))
11.11 end
11.12 @@ -49,7 +49,7 @@
11.13 let val (pt', c', p') = Generate.generate tacis (pt, [], p)
11.14 in ("ok", (tacis, c', (pt', p'))) end
11.15 else (case (if member op = [Pos.Pbl, Pos.Met] p_
11.16 - then specify_do_next (pt, ip) else LucinNEW.do_next (pt, ip))
11.17 + then specify_do_next (pt, ip) else Lucin.do_next (pt, ip))
11.18 handle ERROR msg => (writeln ("*** " ^ msg);
11.19 ("e.g. Add_Given equality ///", ([], [], ptp))) of
11.20 (_, cs as ([], _, _)) => ("helpless", cs)
12.1 --- a/src/Tools/isac/ROOT Tue Feb 04 16:45:36 2020 +0100
12.2 +++ b/src/Tools/isac/ROOT Tue Feb 04 17:11:54 2020 +0100
12.3 @@ -29,6 +29,8 @@
12.4 session Lucas_Interpreter = HOL +
12.5 description \<open>
12.6 Session Isac restricted to code required for Lucas_Interpreter.
12.7 + "Lucas-Interpretation on Isabelle’s Functions"
12.8 + and meant as a first step towards documentation.
12.9 \<close>
12.10 options [document = false (*, browser_info = true*)]
12.11 theories
13.1 --- a/src/Tools/isac/Specify/step-specify.sml Tue Feb 04 16:45:36 2020 +0100
13.2 +++ b/src/Tools/isac/Specify/step-specify.sml Tue Feb 04 17:11:54 2020 +0100
13.3 @@ -6,7 +6,7 @@
13.4 signature STEP_SPECIFY =
13.5 sig
13.6 val by_tactic: Tactic.input -> Calc.T -> Chead.calcstate'
13.7 -(*val do_next: Step.specify_do_next requires LucinNEW.by_tactic, which is not yet known in Step_Specify*)
13.8 +(*val do_next: Step.specify_do_next requires Lucin.by_tactic, which is not yet known in Step_Specify*)
13.9
13.10 end
13.11
14.1 --- a/src/Tools/isac/TODO.thy Tue Feb 04 16:45:36 2020 +0100
14.2 +++ b/src/Tools/isac/TODO.thy Tue Feb 04 17:11:54 2020 +0100
14.3 @@ -38,8 +38,6 @@
14.4 check_tac cc ist (prog_tac, form_arg)
14.5 + in check_tac1
14.6 \item xxx
14.7 - \item shift check_leaf Lucin --> LucinNEW ? LItool ?
14.8 - \item xxx
14.9 \item rm test/..--- check Scripts ---
14.10 \item xxx
14.11 \item reformat + rename "fun eval_leaf"+"fun get_stac"
14.12 @@ -73,7 +71,7 @@
14.13 \item xxx
14.14 \item xxx
14.15 \item simplify calls of scan_dn1, scan_dn etc
14.16 - \item open Istate in LucinNEW
14.17 + \item open Istate in Lucin
14.18 \end{itemize}
14.19 \<close>
14.20 subsection \<open>Postponed from current changeset\<close>
14.21 @@ -171,7 +169,7 @@
14.22 \item xxx
14.23 \item inform: TermC.parse (Celem.assoc_thy "Isac_Knowledge") istr --> parseNEW context istr
14.24 \item extract common code from associate.. stac2tac_
14.25 - rename Lucin.stac2tac -> Tactic.from_prog_tac ? Solve_Tac.from_prog_tac,
14.26 + rename LItool.stac2tac -> Tactic.from_prog_tac ? Solve_Tac.from_prog_tac,
14.27 .. see \<open>Separate ..\<close>
14.28 \end{itemize}
14.29 \<close>
14.30 @@ -355,7 +353,7 @@
14.31 \item xxx
14.32 \end{itemize}
14.33 \item xxx
14.34 - \item ??????????? WHY CAN LucinNEW.by_tactic NOT BE REPLACED BY Step_Solve.by_tactic ???????????
14.35 + \item ??????????? WHY CAN Lucin.by_tactic NOT BE REPLACED BY Step_Solve.by_tactic ???????????
14.36 \item xxx
14.37 \item ..Separate:
14.38 MathEngine.solve, ...,
14.39 @@ -443,7 +441,7 @@
14.40 \item cleaup the many conversions string -- theory
14.41 \item make dest_spec --> (theory, pblID, metID) ?+ common_subthy ?
14.42 \item 1. Rewrite.eval_true_, then
14.43 - Lucin.check_leaf, Rewrite.eval_prog_expr, Generate.generate1, Lucin.stac2tac.
14.44 + LItool.check_leaf, Rewrite.eval_prog_expr, Generate.generate1, LItool.stac2tac.
14.45 \item fun associate
14.46 let val thy = Celem.assoc_thy "Isac_Knowledge";(*TODO*)
14.47 \item xxx
15.1 --- a/test/Tools/isac/BridgeLibisabelle/use-cases.sml Tue Feb 04 16:45:36 2020 +0100
15.2 +++ b/test/Tools/isac/BridgeLibisabelle/use-cases.sml Tue Feb 04 17:11:54 2020 +0100
15.3 @@ -199,9 +199,9 @@
15.4 "~~~~~ fun Step_Solve.by_tactic , args:"; val (m, (pt, po as (p, p_))) = (m, (pt, pos));
15.5 (*if*) Celem.e_metID = get_obj g_metID pt (par_pblobj pt p); (*else*)
15.6 val thy' = get_obj g_domID pt (par_pblobj pt p);
15.7 - val (srls, is, sc) = Lucin.from_pblobj_or_detail' thy' (p,p_) pt;
15.8 + val (srls, is, sc) = LItool.from_pblobj_or_detail' thy' (p,p_) pt;
15.9 val Safe_Step (istate, _, tac) =
15.10 - (*case*) LucinNEW.locate_input_tactic sc (pt, po) (fst is) (snd is) m (*of*);
15.11 + (*case*) Lucin.locate_input_tactic sc (pt, po) (fst is) (snd is) m (*of*);
15.12
15.13 (*+*)Safe_Step: Istate.T * Proof.context * T -> input_tactic_result;
15.14 (********************* locate_input_tactic returns cstate * istate * Proof.context *************)
16.1 --- a/test/Tools/isac/Interpret/inform.sml Tue Feb 04 16:45:36 2020 +0100
16.2 +++ b/test/Tools/isac/Interpret/inform.sml Tue Feb 04 17:11:54 2020 +0100
16.3 @@ -1025,8 +1025,8 @@
16.4 (*NEW*)val {scr = prog, ...} = Specify.get_met metID
16.5 (*NEW*)val istate = get_istate pt pos
16.6 (*NEW*)val ctxt = get_ctxt pt pos
16.7 - val LucinNEW.Not_Derivable calcstate' =
16.8 - (*case*) LucinNEW.locate_input_term prog (pt, pos) istate ctxt f_in (*of*);
16.9 + val Lucin.Not_Derivable calcstate' =
16.10 + (*case*) Lucin.locate_input_term prog (pt, pos) istate ctxt f_in (*of*);
16.11 val pp = Ctree.par_pblobj pt p
16.12 val (errpats, nrls, prog) = case Specify.get_met (Ctree.get_obj Ctree.g_metID pt pp) of
16.13 {errpats, nrls, scr = Rule.Prog prog, ...} => (errpats, nrls, prog)
17.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
17.2 +++ b/test/Tools/isac/Interpret/li-tool.sml Tue Feb 04 17:11:54 2020 +0100
17.3 @@ -0,0 +1,327 @@
17.4 +(* Title: test/../script.sml
17.5 + Author: Walther Neuper 050908
17.6 + (c) copyright due to lincense terms.
17.7 +*)
17.8 +"-----------------------------------------------------------------";
17.9 +"table of contents -----------------------------------------------";
17.10 +"-----------------------------------------------------------------";
17.11 +"----------- fun sel_appl_atomic_tacs ----------------------------";
17.12 +"----------- fun init_form, fun get_stac -------------------------";
17.13 +"----------- fun sel_rules ---------------------------------------";
17.14 +"----------- fun sel_appl_atomic_tacs ----------------------------";
17.15 +"----------- fun de_esc_underscore -------------------------------";
17.16 +"----------- fun go ----------------------------------------------";
17.17 +"----------- fun formal_args -------------------------------------";
17.18 +"----------- fun dsc_valT ----------------------------------------";
17.19 +"----------- fun itms2args ---------------------------------------";
17.20 +"----------- fun init_pstate -----------------------------------------------------------------";
17.21 +"-----------------------------------------------------------------";
17.22 +"-----------------------------------------------------------------";
17.23 +"-----------------------------------------------------------------";
17.24 +
17.25 +val thy = @{theory Isac_Knowledge};
17.26 +
17.27 +"----------- fun sel_appl_atomic_tacs ----------------------------";
17.28 +"----------- fun sel_appl_atomic_tacs ----------------------------";
17.29 +"----------- fun sel_appl_atomic_tacs ----------------------------";
17.30 +
17.31 +reset_states ();
17.32 +CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
17.33 + ("Test", ["sqroot-test","univariate","equation","test"],
17.34 + ["Test","squ-equ-test-subpbl1"]))];
17.35 +Iterator 1;
17.36 +moveActiveRoot 1;
17.37 +autoCalculate 1 CompleteCalcHead;
17.38 +autoCalculate 1 (Steps 1);
17.39 +autoCalculate 1 (Steps 1);
17.40 +val ((pt, p), _) = get_calc 1; show_pt pt;
17.41 +val appltacs = sel_appl_atomic_tacs pt p;
17.42 +case appltacs of
17.43 + [Rewrite ("radd_commute", radd_commute),
17.44 + Rewrite ("add_assoc", add_assoc), Calculate "TIMES"]
17.45 + => if (term2str o Thm.prop_of) radd_commute = "?m + ?n = ?n + ?m" andalso
17.46 + (term2str o Thm.prop_of) add_assoc = "?a + ?b + ?c = ?a + (?b + ?c)" then ()
17.47 + else error "script.sml fun sel_appl_atomic_tacs diff.behav. 2"
17.48 +| _ => error "script.sml fun sel_appl_atomic_tacs diff.behav. 1";
17.49 +
17.50 +trace_script := true;
17.51 +trace_script := false;
17.52 +applyTactic 1 p (hd appltacs);
17.53 +val ((pt, p), _) = get_calc 1; show_pt pt;
17.54 +val appltacs = sel_appl_atomic_tacs pt p;
17.55 +(*applyTactic 1 p (hd appltacs); WAS scan_dn1: call by ([3], Pbl)*)
17.56 +
17.57 +"~~~~~ fun applyTactic, args:"; val ((cI:calcID), ip, tac) = (1, p, (hd appltacs));
17.58 +val ((pt, _), _) = get_calc cI;
17.59 +val p = get_pos cI 1;
17.60 +locatetac;
17.61 +locatetac tac;
17.62 +
17.63 +(*locatetac tac (pt, ip); (*WAS scan_dn1: call by ([3], Pbl)*)*)
17.64 +"~~~~~ fun locatetac, args:"; val (tac, (ptp as (pt, p))) = (tac, (pt, ip));
17.65 + val Appl m = applicable_in p pt tac ; (*Appl*)
17.66 + (*if*) Tactic.for_specify' m; (*false*)
17.67 +(*loc_solve_ (mI,m) ptp; (*Argument: (mI, m) : string * tac Reason: Can't unify tac_ with tac*)*)
17.68 +loc_solve_; (*without _ ??? result is -> lOc writing error ???*)
17.69 +(*val it = fn: string * tac_ -> ctree * (pos * pos_) -> lOc_*)
17.70 +(mI,m); (*string * tac*)
17.71 +ptp (*ctree * pos'*);
17.72 +"~~~~~ fun loc_solve_, args:"; val (m ,(pt,pos)) = (m, ptp);
17.73 +(*val (msg, cs') = Step_Solve.by_tactic m (pt, pos);
17.74 +(*Argument: m : string * tac Reason: Can't unify tac_ with tac (Different type constructors)*)*)
17.75 +m;
17.76 +(pt, pos);
17.77 +"~~~~~ fun Step_Solve.by_tactic , args:"; val (m, (pt, po as (p,p_))) = (m, (pt, pos));
17.78 +(*solve has still p_!!!!!!!!!!!!!!!!!!!!!!!!!*)
17.79 +
17.80 +e_metID = get_obj g_metID pt (par_pblobj pt p); (*false*)
17.81 +val ctxt = get_ctxt pt po;
17.82 +
17.83 +(*generate1 (assoc_thy (get_obj g_domID pt (par_pblobj pt p))) m (e_istate, ctxt) (p,p_) pt;
17.84 +(*Argument: m : tac Reason: Can't unify tac_ with tac (Different type constructors)*)*)
17.85 +(assoc_thy (get_obj g_domID pt (par_pblobj pt p)));
17.86 +assoc_thy;
17.87 +
17.88 +(* ERROR which has NOT be created by this change set
17.89 +(1) actual : ERROR exception PTREE "get_obj f EmptyPtree" raised (line 289 of "~~/src/Tools/isac/MathEngBasic/ctree-basic.sml")
17.90 +(2) in 927379190abd: generate1: not impl.for Empty_Tac
17.91 +
17.92 +in case (2) exn.ERROR _ was caught, while in case (1) exn.Ptree is not caught before toplevel
17.93 +
17.94 +autoCalculate 1 CompleteCalc; (* ONE ERROR *)
17.95 +==============================^^^^^^^^^^^^^*)
17.96 +
17.97 +"----------- fun init_form, fun get_stac -------------------------";
17.98 +"----------- fun init_form, fun get_stac -------------------------";
17.99 +"----------- fun init_form, fun get_stac -------------------------";
17.100 +val fmz = ["equality (x+1=(2::real))", "solveFor x", "solutions L"];
17.101 +val (dI',pI',mI') = ("Test",["sqroot-test","univariate","equation","test"],
17.102 + ["Test","squ-equ-test-subpbl1"]);
17.103 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
17.104 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
17.105 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
17.106 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
17.107 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
17.108 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
17.109 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
17.110 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
17.111 +"~~~~~ fun me, args:"; val tac = nxt;
17.112 +"~~~~~ fun locatetac, args:"; val ptp as (pt, p) = (pt, p);
17.113 +val Appl m = applicable_in p pt tac;
17.114 + (*if*) Tactic.for_specify' m; (*false*)
17.115 +"~~~~~ fun loc_solve_, args:"; val (m, (pt, pos) ) = (m, ptp);
17.116 +"~~~~~ fun Step_Solve.by_tactic , args:"; val (Apply_Method' (mI,_,_,ctxt), pos as (p,_))
17.117 + = (m, pos);
17.118 +val {srls, ...} = get_met mI;
17.119 +val PblObj {meth=itms, ...} = get_obj I pt p;
17.120 +val thy' = get_obj g_domID pt p;
17.121 +val thy = assoc_thy thy';
17.122 +val srls = LItool.get_simplifier (pt, pos)
17.123 +val (is as Pstate {env, ...}, ctxt, sc) = init_pstate srls ctxt itms mI;
17.124 +val ini = init_form thy sc env;
17.125 +"----- fun init_form, args:"; val (Prog sc) = sc;
17.126 +"----- fun get_stac, args:"; val (y, h $ body) = (thy, sc);
17.127 +case get_stac thy sc of SOME (Free ("e_e", _)) => ()
17.128 +| _ => error "script: Const (?, ?) in script (as term) changed";;
17.129 +
17.130 +"----------- fun sel_rules ---------------------------------------";
17.131 +"----------- fun sel_rules ---------------------------------------";
17.132 +"----------- fun sel_rules ---------------------------------------";
17.133 +(* compare test/../interface.sml
17.134 +"--------- getTactic, fetchApplicableTactics ------------";
17.135 +*)
17.136 + reset_states ();
17.137 + CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
17.138 + ("Test", ["sqroot-test","univariate","equation","test"],
17.139 + ["Test","squ-equ-test-subpbl1"]))];
17.140 + Iterator 1;
17.141 + moveActiveRoot 1;
17.142 + autoCalculate 1 CompleteCalc;
17.143 + val ((pt,_),_) = get_calc 1;
17.144 + show_pt pt;
17.145 +
17.146 +(*UC\label{SOLVE:MANUAL:TACTIC:listall} UC 30.3.2.2 p.175*)
17.147 + val tacs = sel_rules pt ([],Pbl);
17.148 + case tacs of [Apply_Method ["Test", "squ-equ-test-subpbl1"]] => ()
17.149 + | _ => error "script.sml: diff.behav. in sel_rules ([],Pbl)";
17.150 +
17.151 + val tacs = sel_rules pt ([1],Res);
17.152 + case tacs of [Rewrite_Set "norm_equation", Rewrite_Set "Test_simplify",
17.153 + Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"]),
17.154 + Check_elementwise "Assumptions"] => ()
17.155 + | _ => error "script.sml: diff.behav. in sel_rules ([1],Res)";
17.156 +
17.157 + val tacs = sel_rules pt ([3],Pbl);
17.158 + case tacs of [Apply_Method ["Test", "solve_linear"]] => ()
17.159 + | _ => error "script.sml: diff.behav. in sel_rules ([3],Pbl)";
17.160 +
17.161 + val tacs = sel_rules pt ([3,1],Res);
17.162 + case tacs of [Rewrite_Set_Inst (["(''bdv'', x)"], "isolate_bdv"), Rewrite_Set "Test_simplify"] => ()
17.163 + | _ => error "script.sml: diff.behav. in sel_rules ([3,1],Res)";
17.164 +
17.165 + val tacs = sel_rules pt ([3],Res);
17.166 + case tacs of [Rewrite_Set "norm_equation", Rewrite_Set "Test_simplify",
17.167 + Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"]),
17.168 + Check_elementwise "Assumptions"] => ()
17.169 + | _ => error "script.sml: diff.behav. in sel_rules ([3],Res)";
17.170 +
17.171 + val tacs = (sel_rules pt ([],Res)) handle PTREE str => [Tac str];
17.172 + case tacs of [Tac "no tactics applicable at the end of a calculation"] => ()
17.173 + | _ => error "script.sml: diff.behav. in sel_rules ([],Res)";
17.174 +
17.175 +"----------- fun sel_appl_atomic_tacs ----------------------------";
17.176 +"----------- fun sel_appl_atomic_tacs ----------------------------";
17.177 +"----------- fun sel_appl_atomic_tacs ----------------------------";
17.178 + reset_states ();
17.179 + CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
17.180 + ("Test", ["sqroot-test","univariate","equation","test"],
17.181 + ["Test","squ-equ-test-subpbl1"]))];
17.182 + Iterator 1;
17.183 + moveActiveRoot 1;
17.184 + autoCalculate 1 CompleteCalc;
17.185 +
17.186 +(*UC\label{SOLVE:MANUAL:TACTIC:listall} UC 30.3.2.2 p.175*)
17.187 + fetchApplicableTactics 1 99999 ([],Pbl);
17.188 +
17.189 + fetchApplicableTactics 1 99999 ([1],Res);
17.190 +"~~~~~ fun fetchApplicableTactics, args:"; val (cI, (scope:int), (p:pos')) = (1, 99999, ([1],Res));
17.191 +val ((pt, _), _) = get_calc cI;
17.192 +(*version 1:*)
17.193 +case sel_rules pt p of [Rewrite_Set "norm_equation", Rewrite_Set "Test_simplify",
17.194 + Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"]),
17.195 + Check_elementwise "Assumptions"] => ()
17.196 +| _ => error "fetchApplicableTactics ([1],Res) changed";
17.197 +(*version 2:*)
17.198 +(*WAS:
17.199 +sel_appl_atomic_tacs pt p;
17.200 +...
17.201 +### atomic_appl_tacs: not impl. for tac='Subproblem(Test,["LINEAR","univariate","equation","test"])'
17.202 +### atomic_appl_tacs: not impl. for tac = 'Check_elementwise "Assumptions"'
17.203 +*)
17.204 +
17.205 +"~~~~~ fun sel_appl_atomic_tacs , args:"; val (pt, (p, p_)) = (pt, p);
17.206 +is_spec_pos p_ = false;
17.207 + val pp = par_pblobj pt p
17.208 + val thy' = (get_obj g_domID pt pp):theory'
17.209 + val thy = assoc_thy thy'
17.210 + val metID = get_obj g_metID pt pp
17.211 + val metID' =
17.212 + if metID = e_metID
17.213 + then (thd3 o snd3) (get_obj g_origin pt pp)
17.214 + else metID
17.215 + val {scr=Prog sc,srls,erls,rew_ord'=ro,...} = get_met metID'
17.216 + val Pstate ist = get_istate pt (p,p_)
17.217 + val ctxt = get_ctxt pt (p, p_)
17.218 + val alltacs = (*we expect at least 1 stac in a script*)
17.219 + map ((stac2tac pt thy) o rep_stacexpr o #1 o
17.220 + (check_leaf "selrul" ctxt srls (get_subst ist) )) (stacpbls sc)
17.221 + val f =
17.222 + (case p_ of Frm => get_obj g_form pt p | Res => (fst o (get_obj g_result pt)) p
17.223 + | _ => error "");
17.224 +(*WN120611 stopped and took version 1 again for fetchApplicableTactics !
17.225 +(distinct o flat o (map (atomic_appl_tacs thy ro erls f))) alltacs
17.226 +...
17.227 +### atomic_appl_tacs: not impl. for tac='Subproblem(Test,["LINEAR","univariate","equation","test"])'
17.228 +### atomic_appl_tacs: not impl. for tac = 'Check_elementwise "Assumptions"'
17.229 +*)
17.230 +
17.231 +"----------- fun de_esc_underscore -------------------------------";
17.232 +"----------- fun de_esc_underscore -------------------------------";
17.233 +"----------- fun de_esc_underscore -------------------------------";
17.234 +(*
17.235 +> val str = "Rewrite_Set_Inst";
17.236 +> val esc = esc_underscore str;
17.237 +val it = "Rewrite'_Set'_Inst" : string
17.238 +> val des = de_esc_underscore esc;
17.239 + val des = de_esc_underscore esc;*)
17.240 +
17.241 +"----------- fun go ----------------------------------------------";
17.242 +"----------- fun go ----------------------------------------------";
17.243 +"----------- fun go ----------------------------------------------";
17.244 +(*
17.245 +> val t = (Thm.term_of o the o (parse thy)) "a+b";
17.246 +val it = Const (#,#) $ Free (#,#) $ Free ("b","RealDef.real") : term
17.247 +> val plus_a = at_location [L] t;
17.248 +> val b = at_location [R] t;
17.249 +> val plus = at_location [L,L] t;
17.250 +> val a = at_location [L,R] t;
17.251 +
17.252 +> val t = (Thm.term_of o the o (parse thy)) "a+b+c";
17.253 +val t = Const (#,#) $ (# $ # $ Free #) $ Free ("c","RealDef.real") : term
17.254 +> val pl_pl_a_b = at_location [L] t;
17.255 +> val c = at_location [R] t;
17.256 +> val a = at_location [L,R,L,R] t;
17.257 +> val b = at_location [L,R,R] t;
17.258 +*)
17.259 +
17.260 +"----------- fun formal_args -------------------------------------";
17.261 +"----------- fun formal_args -------------------------------------";
17.262 +"----------- fun formal_args -------------------------------------";
17.263 +(*
17.264 +> formal_args scr;
17.265 + [Free ("f_","RealDef.real"),Free ("v_","RealDef.real"),
17.266 + Free ("eqs_","bool List.list")] : term list
17.267 +*)
17.268 +"----------- fun dsc_valT ----------------------------------------";
17.269 +"----------- fun dsc_valT ----------------------------------------";
17.270 +"----------- fun dsc_valT ----------------------------------------";
17.271 +(*> val t = (Thm.term_of o the o (parse thy)) "equality";
17.272 +> val T = type_of t;
17.273 +val T = "bool => Tools.una" : typ
17.274 +> val dsc = dsc_valT t;
17.275 +val dsc = "una" : string
17.276 +
17.277 +> val t = (Thm.term_of o the o (parse thy)) "fixedValues";
17.278 +> val T = type_of t;
17.279 +val T = "bool List.list => Tools.nam" : typ
17.280 +> val dsc = dsc_valT t;
17.281 +val dsc = "nam" : string*)
17.282 +"----------- fun itms2args ---------------------------------------";
17.283 +"----------- fun itms2args ---------------------------------------";
17.284 +"----------- fun itms2args ---------------------------------------";
17.285 +(*
17.286 +> val sc = ... Solve_root_equation ...
17.287 +> val mI = ("Program","sqrt-equ-test");
17.288 +> val PblObj{meth={ppc=itms,...},...} = get_obj I pt [];
17.289 +> val ts = itms2args thy mI itms;
17.290 +> map (term_to_string''' thy) ts;
17.291 +["sqrt (#9 + #4 * x) = sqrt x + sqrt (#5 + x)","x","#0"] : string list
17.292 +*)
17.293 +
17.294 +"----------- fun init_pstate -----------------------------------------------------------------";
17.295 +"----------- fun init_pstate -----------------------------------------------------------------";
17.296 +"----------- fun init_pstate -----------------------------------------------------------------";
17.297 +val fmz = ["Traegerlaenge L","Streckenlast q_0","Biegelinie y",
17.298 + "Randbedingungen [y 0 = (0::real), y L = 0, M_b 0 = 0, M_b L = 0]",
17.299 + "FunktionsVariable x", "GleichungsVariablen [c, c_2, c_3, c_4]",
17.300 + "AbleitungBiegelinie dy"];
17.301 +val (dI',pI',mI') = ("Biegelinie", ["Biegelinien"],
17.302 + ["IntegrierenUndKonstanteBestimmen2"]);
17.303 +val p = e_pos'; val c = [];
17.304 +(*[], Pbl*)val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; (*nxt = Model_Problem*)
17.305 +(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Add_Given "Traegerlaenge L"*)
17.306 +(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Add_Given "Streckenlast q_0"*)
17.307 +(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Add_Find "Biegelinie y"*)
17.308 +(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Add_Relation "Randbedingungen [y 0 = 0]", ERROR MISSING step: M_b 0 = 0*)
17.309 +(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Add_Relation "Randbedingungen [y L = 0, M_b 0 = 0, M_b L = 0]"*)
17.310 +(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Specify_Theory "Biegelinie"*)
17.311 +(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Specify_Problem ["Biegelinien"]*)
17.312 +(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Specify_Method ["IntegrierenUndKonstanteBestimmen2"]*)
17.313 +(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Add_Given "FunktionsVariable x"*)
17.314 +(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Add_Given "GleichungsVariablen [c, c_2, c_3, c_4]"*)
17.315 +(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Add_Given "AbleitungBiegelinie dy"*)
17.316 +(*[], Met*)val (p''''',_,f,nxt''''',_,pt''''') = me nxt p c pt; (*nxt''''' = Apply_Method ["IntegrierenUndKonstanteBestimmen2"*)
17.317 +
17.318 +(*+*)val PblObj {meth, spec = (thy, _ , metID), ...} = get_obj I pt''''' (fst p''''');
17.319 +(*+*)val ctxt = get_ctxt pt''''' p''''';
17.320 +(*+*)val srls = get_simplifier (pt''''', p''''');
17.321 +"~~~~~ fun init_pstate , args:"; val (srls, thy, itms, metID) = (srls, assoc_thy thy, meth, metID);
17.322 +val (Pstate st, ctxt, Prog _) = init_pstate srls ctxt itms metID;
17.323 +if pstate2str st =
17.324 + "([\"\n(l, L)\",\"\n(q, q_0)\",\"\n(v, x)\",\"\n(b, dy)\",\"\n(s, [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0])\",\"\n(vs, [c, c_2, c_3, c_4])\",\"\n(id_abl, y)\"], [], erls_IntegrierenUndK.., NONE, \n??.empty, ORundef, false, true)"
17.325 +then () else error "init_pstate changed for Biegelinie";
17.326 +
17.327 +(*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt''''' p''''' c pt'''''; (*nxt = Model_Problem*)
17.328 +if p = ([1], Pbl)
17.329 +then case nxt of Model_Problem => () | _ => error "Biegelinie 7.70 changed 1"
17.330 +else error "modeling root-problem of Biegelinie 7.70 changed";
18.1 --- a/test/Tools/isac/Interpret/lucas-interpreter.sml Tue Feb 04 16:45:36 2020 +0100
18.2 +++ b/test/Tools/isac/Interpret/lucas-interpreter.sml Tue Feb 04 17:11:54 2020 +0100
18.3 @@ -49,17 +49,17 @@
18.4 | _ => error "solve Apply_Method: uncovered case get_obj"
18.5 val thy' = get_obj g_domID pt p;
18.6 val thy = Celem.assoc_thy thy';
18.7 - val srls = Lucin.get_simplifier (pt, pos)
18.8 - val (is, env, ctxt, sc) = case Lucin.init_pstate srls ctxt itms mI of
18.9 + val srls = LItool.get_simplifier (pt, pos)
18.10 + val (is, env, ctxt, sc) = case LItool.init_pstate srls ctxt itms mI of
18.11 (is as Istate.Pstate {env, ...}, ctxt, sc) => (is, env, ctxt, sc)
18.12 | _ => error "solve Apply_Method: uncovered case init_pstate";
18.13 (*+*)pstate2str (the_pstate is) = "([\"\n(f_f, x ^^^ 2 + 1)\",\"\n(v_v, x)\"], [], e_rls, NONE, \n??.empty, ORundef, false, true)";
18.14 - val ini = Lucin.init_form thy sc env;
18.15 + val ini = LItool.init_form thy sc env;
18.16 val p = lev_dn p;
18.17
18.18 val NONE = (*case*) ini (*of*);
18.19 val Next_Step (is', ctxt', m') =
18.20 - LucinNEW.find_next_step sc (pt, (p, Res)) is ctxt;
18.21 + Lucin.find_next_step sc (pt, (p, Res)) is ctxt;
18.22 (*+*)pstate2str (the_pstate is') = "([\"\n(f_f, x ^^^ 2 + 1)\",\"\n(v_v, x)\"], [R,L,R], e_rls, NONE, \nIntegral x ^^^ 2 + 1 D x, ORundef, false, false)";
18.23 val Safe_Step (_, _, Take' _) = (*case*)
18.24 locate_input_tactic sc (pt, (p, Res)) is' ctxt' m' (*of*);
18.25 @@ -120,7 +120,7 @@
18.26 (*+*)val (pt'''''_', (p'''''_', p_'''''_')) = (pt, (p, p_));
18.27 (*if*) Celem.e_metID = get_obj g_metID pt (par_pblobj pt p); (*else*)
18.28 val thy' = get_obj g_domID pt (par_pblobj pt p);
18.29 - val (_, is, sc) = Lucin.from_pblobj' thy' (p,p_) pt;
18.30 + val (_, is, sc) = LItool.from_pblobj' thy' (p,p_) pt;
18.31
18.32 locate_input_tactic sc (pt, po) (fst is) (snd is) m;
18.33 "~~~~~ fun locate_input_tactic , args:"; val (Prog prog, cstate, istate, ctxt, tac)
18.34 @@ -152,7 +152,7 @@
18.35 = (xxx, (ist |> path_down [R]), e);
18.36 val (Program.Tac stac, a') =
18.37 (*case*) check_leaf "locate" ctxt eval (get_subst ist) t (*of*);
18.38 - val Lucin.Ass (m, v', ctxt) =
18.39 + val LItool.Ass (m, v', ctxt) =
18.40 (*case*) associate pt ctxt (m, stac) (*of*);
18.41
18.42 Accept_Tac1 (ist |> set_subst_true (a', v'), ctxt, m) (*return value*);
18.43 @@ -170,7 +170,7 @@
18.44 (*+*)val (pt, po as (p, p_)) = (pt'''''_', (p'''''_', p_'''''_')); (* from begin of by_tactic *)
18.45 val (p'', _, _,pt') =
18.46 Generate.generate1 (Celem.assoc_thy "Isac_Knowledge") tac
18.47 - (* DEL.^^^^^ ContextC.insert_assumptions asms' ctxt 2nd, fst in Lucin.associate *)
18.48 + (* DEL.^^^^^ ContextC.insert_assumptions asms' ctxt 2nd, fst in LItool.associate *)
18.49 (istate, ctxt) (lev_on p, Pbl) pt;
18.50 (*in*)
18.51
18.52 @@ -282,12 +282,12 @@
18.53 "~~~~~ fun Step_Solve.by_tactic , args:"; val (m, (pt, po as (p, p_))) = (m, (pt, pos));
18.54 (*if*) Celem.e_metID = get_obj g_metID pt (par_pblobj pt p) (*else*);
18.55 val thy' = get_obj g_domID pt (par_pblobj pt p);
18.56 - val (_, is, sc) = Lucin.from_pblobj_or_detail' thy' (p,p_) pt;
18.57 + val (_, is, sc) = LItool.from_pblobj_or_detail' thy' (p,p_) pt;
18.58
18.59 (*case*) locate_input_tactic sc (pt, po) (fst is) (snd is) m (*of*);
18.60 "~~~~~ fun locate_input_tactic , args:"; val ((Rule.Prog prog), (cstate as (pt, (*?*)pos(*?*))), istate, ctxt, tac)
18.61 = (sc, (pt, po), (fst is), (snd is), m);
18.62 - val srls = Lucin.get_simplifier cstate (*TODO: shift into Istate.T*);
18.63 + val srls = LItool.get_simplifier cstate (*TODO: shift into Istate.T*);
18.64
18.65 (*case*) scan_to_tactic1 (prog, (cstate, ctxt, tac)) istate (*of*);
18.66 "~~~~~ fun scan_to_tactic1 , args:"; val ((prog, (cctt as ((_, p), _, _))), (Istate.Pstate (ist as {path, ...})))
18.67 @@ -330,7 +330,7 @@
18.68 val NotAss = (*case*) associate pt ctxt (tac, stac) (*of*);
18.69 val ORundef = (*case*) or (*of*);
18.70 val Notappl "norm_equation not applicable" =
18.71 - (*case*) Applicable.applicable_in p pt (Lucin.stac2tac pt (Celem.assoc_thy "Isac_Knowledge") stac) (*of*);
18.72 + (*case*) Applicable.applicable_in p pt (LItool.stac2tac pt (Celem.assoc_thy "Isac_Knowledge") stac) (*of*);
18.73
18.74 (Term_Val1 act_arg) (* return value *);
18.75
18.76 @@ -384,10 +384,10 @@
18.77 "~~~~~ and do_next , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
18.78 (*if*) Celem.e_metID = get_obj g_metID pt (par_pblobj pt p) (*else*);
18.79 val thy' = get_obj g_domID pt (par_pblobj pt p);
18.80 - val (_, (ist, ctxt), sc) = Lucin.from_pblobj_or_detail' thy' (p,p_) pt;
18.81 + val (_, (ist, ctxt), sc) = LItool.from_pblobj_or_detail' thy' (p,p_) pt;
18.82
18.83 (*NEW*) val Next_Step (_, _, Rewrite_Set' (_, _, Rls {id = "Test_simplify", ...}, _, _)) = (*case*)
18.84 -(*NEW*) LucinNEW.find_next_step sc (pt, pos) ist ctxt (*of*);
18.85 +(*NEW*) Lucin.find_next_step sc (pt, pos) ist ctxt (*of*);
18.86 "~~~~~ fun find_next_step , args:"; val (Rule.Prog prog, ptp as (pt, (p, _)), Istate.Pstate ist, ctxt)
18.87 = (sc, (pt, pos), ist, ctxt);
18.88 (*OLD* ) val Accept_Tac (m', ist as {act_arg, ...}, ctxt) =
18.89 @@ -406,11 +406,11 @@
18.90 (*NEW*)
18.91 "~~~~~ from fun find_next_step\<longrightarrow>and do_next , return:"; val (Next_Step (ist, ctxt, tac))
18.92 = (Next_Step (Istate.Pstate ist, Tactic.insert_assumptions tac ctxt, tac));
18.93 -(*NEW* ) case LucinNEW.find_next_step sc (pt, pos) ist ctxt of
18.94 +(*NEW* ) case Lucin.find_next_step sc (pt, pos) ist ctxt of
18.95 (*NEW*) Next_Step (ist, ctxt, tac) =>
18.96 ( *NEW*)
18.97 - LucinNEW.by_tactic tac (ist, Tactic.insert_assumptions tac ctxt) ptp;
18.98 -(*NEW* ) | End_Program (ist, tac) => LucinNEW.by_tactic tac (ist, ctxt) ptp
18.99 + Lucin.by_tactic tac (ist, Tactic.insert_assumptions tac ctxt) ptp;
18.100 +(*NEW* ) | End_Program (ist, tac) => Lucin.by_tactic tac (ist, ctxt) ptp
18.101 (*NEW*) | Helpless => Chead.e_calcstate'
18.102 ( *NEW*)
18.103
18.104 @@ -454,14 +454,14 @@
18.105 val (res, asm) = (get_obj g_result pt (fst p));
18.106
18.107 if term2str res = "[x = 1]" andalso terms2str asm = "[\"precond_rootmet 1\"]"
18.108 -then () else error "re-build: fu LucinNEW.find_next_step CHANGED 1";
18.109 +then () else error "re-build: fu Lucin.find_next_step CHANGED 1";
18.110
18.111 if p = ([], Und) (*.. should be ([], Res) *)
18.112 then
18.113 case get_obj g_tac pt (fst p) of
18.114 Apply_Method ["Test", "squ-equ-test-subpbl1"] => ((*ok, further tactics are level down*))
18.115 - | _ => error "re-build: fun LucinNEW.find_next_step CHANGED 3"
18.116 -else error "re-build: fun LucinNEW.find_next_step CHANGED 2";
18.117 + | _ => error "re-build: fun Lucin.find_next_step CHANGED 3"
18.118 +else error "re-build: fun Lucin.find_next_step CHANGED 2";
18.119 \\--------- exception Size raised (line 171 of "./basis/LibrarySupport.sml") ---------------//*)
18.120
18.121
19.1 --- a/test/Tools/isac/Interpret/script.sml Tue Feb 04 16:45:36 2020 +0100
19.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
19.3 @@ -1,327 +0,0 @@
19.4 -(* Title: test/../script.sml
19.5 - Author: Walther Neuper 050908
19.6 - (c) copyright due to lincense terms.
19.7 -*)
19.8 -"-----------------------------------------------------------------";
19.9 -"table of contents -----------------------------------------------";
19.10 -"-----------------------------------------------------------------";
19.11 -"----------- fun sel_appl_atomic_tacs ----------------------------";
19.12 -"----------- fun init_form, fun get_stac -------------------------";
19.13 -"----------- fun sel_rules ---------------------------------------";
19.14 -"----------- fun sel_appl_atomic_tacs ----------------------------";
19.15 -"----------- fun de_esc_underscore -------------------------------";
19.16 -"----------- fun go ----------------------------------------------";
19.17 -"----------- fun formal_args -------------------------------------";
19.18 -"----------- fun dsc_valT ----------------------------------------";
19.19 -"----------- fun itms2args ---------------------------------------";
19.20 -"----------- fun init_pstate -----------------------------------------------------------------";
19.21 -"-----------------------------------------------------------------";
19.22 -"-----------------------------------------------------------------";
19.23 -"-----------------------------------------------------------------";
19.24 -
19.25 -val thy = @{theory Isac_Knowledge};
19.26 -
19.27 -"----------- fun sel_appl_atomic_tacs ----------------------------";
19.28 -"----------- fun sel_appl_atomic_tacs ----------------------------";
19.29 -"----------- fun sel_appl_atomic_tacs ----------------------------";
19.30 -
19.31 -reset_states ();
19.32 -CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
19.33 - ("Test", ["sqroot-test","univariate","equation","test"],
19.34 - ["Test","squ-equ-test-subpbl1"]))];
19.35 -Iterator 1;
19.36 -moveActiveRoot 1;
19.37 -autoCalculate 1 CompleteCalcHead;
19.38 -autoCalculate 1 (Steps 1);
19.39 -autoCalculate 1 (Steps 1);
19.40 -val ((pt, p), _) = get_calc 1; show_pt pt;
19.41 -val appltacs = sel_appl_atomic_tacs pt p;
19.42 -case appltacs of
19.43 - [Rewrite ("radd_commute", radd_commute),
19.44 - Rewrite ("add_assoc", add_assoc), Calculate "TIMES"]
19.45 - => if (term2str o Thm.prop_of) radd_commute = "?m + ?n = ?n + ?m" andalso
19.46 - (term2str o Thm.prop_of) add_assoc = "?a + ?b + ?c = ?a + (?b + ?c)" then ()
19.47 - else error "script.sml fun sel_appl_atomic_tacs diff.behav. 2"
19.48 -| _ => error "script.sml fun sel_appl_atomic_tacs diff.behav. 1";
19.49 -
19.50 -trace_script := true;
19.51 -trace_script := false;
19.52 -applyTactic 1 p (hd appltacs);
19.53 -val ((pt, p), _) = get_calc 1; show_pt pt;
19.54 -val appltacs = sel_appl_atomic_tacs pt p;
19.55 -(*applyTactic 1 p (hd appltacs); WAS scan_dn1: call by ([3], Pbl)*)
19.56 -
19.57 -"~~~~~ fun applyTactic, args:"; val ((cI:calcID), ip, tac) = (1, p, (hd appltacs));
19.58 -val ((pt, _), _) = get_calc cI;
19.59 -val p = get_pos cI 1;
19.60 -locatetac;
19.61 -locatetac tac;
19.62 -
19.63 -(*locatetac tac (pt, ip); (*WAS scan_dn1: call by ([3], Pbl)*)*)
19.64 -"~~~~~ fun locatetac, args:"; val (tac, (ptp as (pt, p))) = (tac, (pt, ip));
19.65 - val Appl m = applicable_in p pt tac ; (*Appl*)
19.66 - (*if*) Tactic.for_specify' m; (*false*)
19.67 -(*loc_solve_ (mI,m) ptp; (*Argument: (mI, m) : string * tac Reason: Can't unify tac_ with tac*)*)
19.68 -loc_solve_; (*without _ ??? result is -> lOc writing error ???*)
19.69 -(*val it = fn: string * tac_ -> ctree * (pos * pos_) -> lOc_*)
19.70 -(mI,m); (*string * tac*)
19.71 -ptp (*ctree * pos'*);
19.72 -"~~~~~ fun loc_solve_, args:"; val (m ,(pt,pos)) = (m, ptp);
19.73 -(*val (msg, cs') = Step_Solve.by_tactic m (pt, pos);
19.74 -(*Argument: m : string * tac Reason: Can't unify tac_ with tac (Different type constructors)*)*)
19.75 -m;
19.76 -(pt, pos);
19.77 -"~~~~~ fun Step_Solve.by_tactic , args:"; val (m, (pt, po as (p,p_))) = (m, (pt, pos));
19.78 -(*solve has still p_!!!!!!!!!!!!!!!!!!!!!!!!!*)
19.79 -
19.80 -e_metID = get_obj g_metID pt (par_pblobj pt p); (*false*)
19.81 -val ctxt = get_ctxt pt po;
19.82 -
19.83 -(*generate1 (assoc_thy (get_obj g_domID pt (par_pblobj pt p))) m (e_istate, ctxt) (p,p_) pt;
19.84 -(*Argument: m : tac Reason: Can't unify tac_ with tac (Different type constructors)*)*)
19.85 -(assoc_thy (get_obj g_domID pt (par_pblobj pt p)));
19.86 -assoc_thy;
19.87 -
19.88 -(* ERROR which has NOT be created by this change set
19.89 -(1) actual : ERROR exception PTREE "get_obj f EmptyPtree" raised (line 289 of "~~/src/Tools/isac/MathEngBasic/ctree-basic.sml")
19.90 -(2) in 927379190abd: generate1: not impl.for Empty_Tac
19.91 -
19.92 -in case (2) exn.ERROR _ was caught, while in case (1) exn.Ptree is not caught before toplevel
19.93 -
19.94 -autoCalculate 1 CompleteCalc; (* ONE ERROR *)
19.95 -==============================^^^^^^^^^^^^^*)
19.96 -
19.97 -"----------- fun init_form, fun get_stac -------------------------";
19.98 -"----------- fun init_form, fun get_stac -------------------------";
19.99 -"----------- fun init_form, fun get_stac -------------------------";
19.100 -val fmz = ["equality (x+1=(2::real))", "solveFor x", "solutions L"];
19.101 -val (dI',pI',mI') = ("Test",["sqroot-test","univariate","equation","test"],
19.102 - ["Test","squ-equ-test-subpbl1"]);
19.103 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
19.104 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
19.105 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
19.106 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
19.107 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
19.108 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
19.109 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
19.110 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
19.111 -"~~~~~ fun me, args:"; val tac = nxt;
19.112 -"~~~~~ fun locatetac, args:"; val ptp as (pt, p) = (pt, p);
19.113 -val Appl m = applicable_in p pt tac;
19.114 - (*if*) Tactic.for_specify' m; (*false*)
19.115 -"~~~~~ fun loc_solve_, args:"; val (m, (pt, pos) ) = (m, ptp);
19.116 -"~~~~~ fun Step_Solve.by_tactic , args:"; val (Apply_Method' (mI,_,_,ctxt), pos as (p,_))
19.117 - = (m, pos);
19.118 -val {srls, ...} = get_met mI;
19.119 -val PblObj {meth=itms, ...} = get_obj I pt p;
19.120 -val thy' = get_obj g_domID pt p;
19.121 -val thy = assoc_thy thy';
19.122 -val srls = Lucin.get_simplifier (pt, pos)
19.123 -val (is as Pstate {env, ...}, ctxt, sc) = init_pstate srls ctxt itms mI;
19.124 -val ini = init_form thy sc env;
19.125 -"----- fun init_form, args:"; val (Prog sc) = sc;
19.126 -"----- fun get_stac, args:"; val (y, h $ body) = (thy, sc);
19.127 -case get_stac thy sc of SOME (Free ("e_e", _)) => ()
19.128 -| _ => error "script: Const (?, ?) in script (as term) changed";;
19.129 -
19.130 -"----------- fun sel_rules ---------------------------------------";
19.131 -"----------- fun sel_rules ---------------------------------------";
19.132 -"----------- fun sel_rules ---------------------------------------";
19.133 -(* compare test/../interface.sml
19.134 -"--------- getTactic, fetchApplicableTactics ------------";
19.135 -*)
19.136 - reset_states ();
19.137 - CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
19.138 - ("Test", ["sqroot-test","univariate","equation","test"],
19.139 - ["Test","squ-equ-test-subpbl1"]))];
19.140 - Iterator 1;
19.141 - moveActiveRoot 1;
19.142 - autoCalculate 1 CompleteCalc;
19.143 - val ((pt,_),_) = get_calc 1;
19.144 - show_pt pt;
19.145 -
19.146 -(*UC\label{SOLVE:MANUAL:TACTIC:listall} UC 30.3.2.2 p.175*)
19.147 - val tacs = sel_rules pt ([],Pbl);
19.148 - case tacs of [Apply_Method ["Test", "squ-equ-test-subpbl1"]] => ()
19.149 - | _ => error "script.sml: diff.behav. in sel_rules ([],Pbl)";
19.150 -
19.151 - val tacs = sel_rules pt ([1],Res);
19.152 - case tacs of [Rewrite_Set "norm_equation", Rewrite_Set "Test_simplify",
19.153 - Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"]),
19.154 - Check_elementwise "Assumptions"] => ()
19.155 - | _ => error "script.sml: diff.behav. in sel_rules ([1],Res)";
19.156 -
19.157 - val tacs = sel_rules pt ([3],Pbl);
19.158 - case tacs of [Apply_Method ["Test", "solve_linear"]] => ()
19.159 - | _ => error "script.sml: diff.behav. in sel_rules ([3],Pbl)";
19.160 -
19.161 - val tacs = sel_rules pt ([3,1],Res);
19.162 - case tacs of [Rewrite_Set_Inst (["(''bdv'', x)"], "isolate_bdv"), Rewrite_Set "Test_simplify"] => ()
19.163 - | _ => error "script.sml: diff.behav. in sel_rules ([3,1],Res)";
19.164 -
19.165 - val tacs = sel_rules pt ([3],Res);
19.166 - case tacs of [Rewrite_Set "norm_equation", Rewrite_Set "Test_simplify",
19.167 - Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"]),
19.168 - Check_elementwise "Assumptions"] => ()
19.169 - | _ => error "script.sml: diff.behav. in sel_rules ([3],Res)";
19.170 -
19.171 - val tacs = (sel_rules pt ([],Res)) handle PTREE str => [Tac str];
19.172 - case tacs of [Tac "no tactics applicable at the end of a calculation"] => ()
19.173 - | _ => error "script.sml: diff.behav. in sel_rules ([],Res)";
19.174 -
19.175 -"----------- fun sel_appl_atomic_tacs ----------------------------";
19.176 -"----------- fun sel_appl_atomic_tacs ----------------------------";
19.177 -"----------- fun sel_appl_atomic_tacs ----------------------------";
19.178 - reset_states ();
19.179 - CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
19.180 - ("Test", ["sqroot-test","univariate","equation","test"],
19.181 - ["Test","squ-equ-test-subpbl1"]))];
19.182 - Iterator 1;
19.183 - moveActiveRoot 1;
19.184 - autoCalculate 1 CompleteCalc;
19.185 -
19.186 -(*UC\label{SOLVE:MANUAL:TACTIC:listall} UC 30.3.2.2 p.175*)
19.187 - fetchApplicableTactics 1 99999 ([],Pbl);
19.188 -
19.189 - fetchApplicableTactics 1 99999 ([1],Res);
19.190 -"~~~~~ fun fetchApplicableTactics, args:"; val (cI, (scope:int), (p:pos')) = (1, 99999, ([1],Res));
19.191 -val ((pt, _), _) = get_calc cI;
19.192 -(*version 1:*)
19.193 -case sel_rules pt p of [Rewrite_Set "norm_equation", Rewrite_Set "Test_simplify",
19.194 - Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"]),
19.195 - Check_elementwise "Assumptions"] => ()
19.196 -| _ => error "fetchApplicableTactics ([1],Res) changed";
19.197 -(*version 2:*)
19.198 -(*WAS:
19.199 -sel_appl_atomic_tacs pt p;
19.200 -...
19.201 -### atomic_appl_tacs: not impl. for tac='Subproblem(Test,["LINEAR","univariate","equation","test"])'
19.202 -### atomic_appl_tacs: not impl. for tac = 'Check_elementwise "Assumptions"'
19.203 -*)
19.204 -
19.205 -"~~~~~ fun sel_appl_atomic_tacs , args:"; val (pt, (p, p_)) = (pt, p);
19.206 -is_spec_pos p_ = false;
19.207 - val pp = par_pblobj pt p
19.208 - val thy' = (get_obj g_domID pt pp):theory'
19.209 - val thy = assoc_thy thy'
19.210 - val metID = get_obj g_metID pt pp
19.211 - val metID' =
19.212 - if metID = e_metID
19.213 - then (thd3 o snd3) (get_obj g_origin pt pp)
19.214 - else metID
19.215 - val {scr=Prog sc,srls,erls,rew_ord'=ro,...} = get_met metID'
19.216 - val Pstate ist = get_istate pt (p,p_)
19.217 - val ctxt = get_ctxt pt (p, p_)
19.218 - val alltacs = (*we expect at least 1 stac in a script*)
19.219 - map ((stac2tac pt thy) o rep_stacexpr o #1 o
19.220 - (check_leaf "selrul" ctxt srls (get_subst ist) )) (stacpbls sc)
19.221 - val f =
19.222 - (case p_ of Frm => get_obj g_form pt p | Res => (fst o (get_obj g_result pt)) p
19.223 - | _ => error "");
19.224 -(*WN120611 stopped and took version 1 again for fetchApplicableTactics !
19.225 -(distinct o flat o (map (atomic_appl_tacs thy ro erls f))) alltacs
19.226 -...
19.227 -### atomic_appl_tacs: not impl. for tac='Subproblem(Test,["LINEAR","univariate","equation","test"])'
19.228 -### atomic_appl_tacs: not impl. for tac = 'Check_elementwise "Assumptions"'
19.229 -*)
19.230 -
19.231 -"----------- fun de_esc_underscore -------------------------------";
19.232 -"----------- fun de_esc_underscore -------------------------------";
19.233 -"----------- fun de_esc_underscore -------------------------------";
19.234 -(*
19.235 -> val str = "Rewrite_Set_Inst";
19.236 -> val esc = esc_underscore str;
19.237 -val it = "Rewrite'_Set'_Inst" : string
19.238 -> val des = de_esc_underscore esc;
19.239 - val des = de_esc_underscore esc;*)
19.240 -
19.241 -"----------- fun go ----------------------------------------------";
19.242 -"----------- fun go ----------------------------------------------";
19.243 -"----------- fun go ----------------------------------------------";
19.244 -(*
19.245 -> val t = (Thm.term_of o the o (parse thy)) "a+b";
19.246 -val it = Const (#,#) $ Free (#,#) $ Free ("b","RealDef.real") : term
19.247 -> val plus_a = at_location [L] t;
19.248 -> val b = at_location [R] t;
19.249 -> val plus = at_location [L,L] t;
19.250 -> val a = at_location [L,R] t;
19.251 -
19.252 -> val t = (Thm.term_of o the o (parse thy)) "a+b+c";
19.253 -val t = Const (#,#) $ (# $ # $ Free #) $ Free ("c","RealDef.real") : term
19.254 -> val pl_pl_a_b = at_location [L] t;
19.255 -> val c = at_location [R] t;
19.256 -> val a = at_location [L,R,L,R] t;
19.257 -> val b = at_location [L,R,R] t;
19.258 -*)
19.259 -
19.260 -"----------- fun formal_args -------------------------------------";
19.261 -"----------- fun formal_args -------------------------------------";
19.262 -"----------- fun formal_args -------------------------------------";
19.263 -(*
19.264 -> formal_args scr;
19.265 - [Free ("f_","RealDef.real"),Free ("v_","RealDef.real"),
19.266 - Free ("eqs_","bool List.list")] : term list
19.267 -*)
19.268 -"----------- fun dsc_valT ----------------------------------------";
19.269 -"----------- fun dsc_valT ----------------------------------------";
19.270 -"----------- fun dsc_valT ----------------------------------------";
19.271 -(*> val t = (Thm.term_of o the o (parse thy)) "equality";
19.272 -> val T = type_of t;
19.273 -val T = "bool => Tools.una" : typ
19.274 -> val dsc = dsc_valT t;
19.275 -val dsc = "una" : string
19.276 -
19.277 -> val t = (Thm.term_of o the o (parse thy)) "fixedValues";
19.278 -> val T = type_of t;
19.279 -val T = "bool List.list => Tools.nam" : typ
19.280 -> val dsc = dsc_valT t;
19.281 -val dsc = "nam" : string*)
19.282 -"----------- fun itms2args ---------------------------------------";
19.283 -"----------- fun itms2args ---------------------------------------";
19.284 -"----------- fun itms2args ---------------------------------------";
19.285 -(*
19.286 -> val sc = ... Solve_root_equation ...
19.287 -> val mI = ("Program","sqrt-equ-test");
19.288 -> val PblObj{meth={ppc=itms,...},...} = get_obj I pt [];
19.289 -> val ts = itms2args thy mI itms;
19.290 -> map (term_to_string''' thy) ts;
19.291 -["sqrt (#9 + #4 * x) = sqrt x + sqrt (#5 + x)","x","#0"] : string list
19.292 -*)
19.293 -
19.294 -"----------- fun init_pstate -----------------------------------------------------------------";
19.295 -"----------- fun init_pstate -----------------------------------------------------------------";
19.296 -"----------- fun init_pstate -----------------------------------------------------------------";
19.297 -val fmz = ["Traegerlaenge L","Streckenlast q_0","Biegelinie y",
19.298 - "Randbedingungen [y 0 = (0::real), y L = 0, M_b 0 = 0, M_b L = 0]",
19.299 - "FunktionsVariable x", "GleichungsVariablen [c, c_2, c_3, c_4]",
19.300 - "AbleitungBiegelinie dy"];
19.301 -val (dI',pI',mI') = ("Biegelinie", ["Biegelinien"],
19.302 - ["IntegrierenUndKonstanteBestimmen2"]);
19.303 -val p = e_pos'; val c = [];
19.304 -(*[], Pbl*)val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; (*nxt = Model_Problem*)
19.305 -(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Add_Given "Traegerlaenge L"*)
19.306 -(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Add_Given "Streckenlast q_0"*)
19.307 -(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Add_Find "Biegelinie y"*)
19.308 -(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Add_Relation "Randbedingungen [y 0 = 0]", ERROR MISSING step: M_b 0 = 0*)
19.309 -(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Add_Relation "Randbedingungen [y L = 0, M_b 0 = 0, M_b L = 0]"*)
19.310 -(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Specify_Theory "Biegelinie"*)
19.311 -(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Specify_Problem ["Biegelinien"]*)
19.312 -(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Specify_Method ["IntegrierenUndKonstanteBestimmen2"]*)
19.313 -(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Add_Given "FunktionsVariable x"*)
19.314 -(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Add_Given "GleichungsVariablen [c, c_2, c_3, c_4]"*)
19.315 -(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Add_Given "AbleitungBiegelinie dy"*)
19.316 -(*[], Met*)val (p''''',_,f,nxt''''',_,pt''''') = me nxt p c pt; (*nxt''''' = Apply_Method ["IntegrierenUndKonstanteBestimmen2"*)
19.317 -
19.318 -(*+*)val PblObj {meth, spec = (thy, _ , metID), ...} = get_obj I pt''''' (fst p''''');
19.319 -(*+*)val ctxt = get_ctxt pt''''' p''''';
19.320 -(*+*)val srls = get_simplifier (pt''''', p''''');
19.321 -"~~~~~ fun init_pstate , args:"; val (srls, thy, itms, metID) = (srls, assoc_thy thy, meth, metID);
19.322 -val (Pstate st, ctxt, Prog _) = init_pstate srls ctxt itms metID;
19.323 -if pstate2str st =
19.324 - "([\"\n(l, L)\",\"\n(q, q_0)\",\"\n(v, x)\",\"\n(b, dy)\",\"\n(s, [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0])\",\"\n(vs, [c, c_2, c_3, c_4])\",\"\n(id_abl, y)\"], [], erls_IntegrierenUndK.., NONE, \n??.empty, ORundef, false, true)"
19.325 -then () else error "init_pstate changed for Biegelinie";
19.326 -
19.327 -(*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt''''' p''''' c pt'''''; (*nxt = Model_Problem*)
19.328 -if p = ([1], Pbl)
19.329 -then case nxt of Model_Problem => () | _ => error "Biegelinie 7.70 changed 1"
19.330 -else error "modeling root-problem of Biegelinie 7.70 changed";
20.1 --- a/test/Tools/isac/Knowledge/biegelinie-4.sml Tue Feb 04 16:45:36 2020 +0100
20.2 +++ b/test/Tools/isac/Knowledge/biegelinie-4.sml Tue Feb 04 17:11:54 2020 +0100
20.3 @@ -158,14 +158,14 @@
20.4 | _ => error "Step_Solve.by_tactic Apply_Method: uncovered case get_obj"
20.5 val thy' = get_obj g_domID pt p;
20.6 val thy = Celem.assoc_thy thy';
20.7 - val srls = Lucin.get_simplifier (pt, pos)
20.8 - val (is, env, ctxt, sc) = case Lucin.init_pstate srls ctxt itms mI of
20.9 + val srls = LItool.get_simplifier (pt, pos)
20.10 + val (is, env, ctxt, sc) = case LItool.init_pstate srls ctxt itms mI of
20.11 (is as Istate.Pstate ist, ctxt, sc) => (is, get_env ist, ctxt, sc)
20.12 | _ => error "Step_Solve.by_tactic Apply_Method: uncovered case init_pstate"
20.13 - val ini = Lucin.init_form thy sc env;
20.14 + val ini = LItool.init_form thy sc env;
20.15 val p = lev_dn p;
20.16 val NONE = (*case*) ini (*of*);
20.17 - val (m', (is', ctxt'), _) = LucinNEW.find_next_step sc (pt, (p, Res)) is ctxt;
20.18 + val (m', (is', ctxt'), _) = Lucin.find_next_step sc (pt, (p, Res)) is ctxt;
20.19 val d = Rule.e_rls (*FIXME: get simplifier from domID*);
20.20 val Safe_Step ((pt', p'), _, _, _) = (*case*) locate_input_tactic sc (pt,(p, Res)) is' ctxt' m' (*of*);
20.21 Safe_Step : state * Istate.T * Proof.context * Tactic.T -> input_tactic_result;
21.1 --- a/test/Tools/isac/Knowledge/poly.sml Tue Feb 04 16:45:36 2020 +0100
21.2 +++ b/test/Tools/isac/Knowledge/poly.sml Tue Feb 04 17:11:54 2020 +0100
21.3 @@ -633,7 +633,7 @@
21.4 (*+*)if f2str f = "17 + 15 * x ^^^ 2 + -48 * x ^^^ 4 + 3 * x ^^^ 5 + 6 * x ^^^ 7 + -8 * x ^^^ 9"
21.5 (*+*)then () else error "";
21.6
21.7 -(*[1], Res* )val (p,_,f,nxt,_,pt) = me nxt p c pt;( *SINCE Feb.2020 Lucin.find_next_step without result*)
21.8 +(*[1], Res* )val (p,_,f,nxt,_,pt) = me nxt p c pt;( *SINCE Feb.2020 LItool.find_next_step without result*)
21.9
21.10 (*+*)if f2str f = "17 + 15 * x ^^^ 2 + -48 * x ^^^ 4 + 3 * x ^^^ 5 + 6 * x ^^^ 7 + -8 * x ^^^ 9"
21.11 (*+*)then () else error "poly.sml diff.behav. in me Schalk I p.63 No.267b";
22.1 --- a/test/Tools/isac/MathEngine/mathengine-stateless.sml Tue Feb 04 16:45:36 2020 +0100
22.2 +++ b/test/Tools/isac/MathEngine/mathengine-stateless.sml Tue Feb 04 17:11:54 2020 +0100
22.3 @@ -269,7 +269,7 @@
22.4 (auto, c, ptp);
22.5 val (_,_,mI) = get_obj g_spec pt p
22.6 val ctxt = get_ctxt pt pos
22.7 - val (_, (ttt, c', ptp)) = LucinNEW.by_tactic (Apply_Method' (mI, NONE, e_istate, ctxt)) (e_istate, ctxt) ptp;
22.8 + val (_, (ttt, c', ptp)) = Lucin.by_tactic (Apply_Method' (mI, NONE, e_istate, ctxt)) (e_istate, ctxt) ptp;
22.9 (* complete_solve auto (c @ c') ptp; (*WAS Type unification failed...*) pos = ([], Met)*)
22.10 "~~~~~ fun complete_solve, args:"; val (auto, c, (ptp as (_, p as (_,p_)))) =
22.11 (auto, (c @ c'), ptp);
22.12 @@ -365,7 +365,7 @@
22.13 e_metID = get_obj g_metID pt (par_pblobj pt p); (*false*)
22.14 val thy' = get_obj g_domID pt (par_pblobj pt p);
22.15 val (srls, (ist, ctxt), sc) = from_pblobj_or_detail' thy' (p,p_) pt;
22.16 -val Next_Step (istate, ctxt, tac) = LucinNEW.find_next_step sc (pt,pos) ist ctxt; (*WAS Empty_Tac_: tac_*)
22.17 +val Next_Step (istate, ctxt, tac) = Lucin.find_next_step sc (pt,pos) ist ctxt; (*WAS Empty_Tac_: tac_*)
22.18 case tac of Or_to_List' _ => ()
22.19 | _ => error "Or_to_List broken ?"
22.20
22.21 @@ -469,7 +469,7 @@
22.22 e_metID = get_obj g_metID pt (par_pblobj pt p) = false;
22.23 val thy' = get_obj g_domID pt (par_pblobj pt p);
22.24 val (srls, (ist, ctxt), sc) = from_pblobj_or_detail' thy' (p,p_) pt;
22.25 - val Next_Step (is, ctxt, tac_) = LucinNEW.find_next_step sc (pt,pos) ist ctxt;
22.26 + val Next_Step (is, ctxt, tac_) = Lucin.find_next_step sc (pt,pos) ist ctxt;
22.27 (*tac_ = Rewrite' (..., ("rnorm_equation_add", "Test.rnorm_equation_add"), ...) !!!!!!!!!!!!!!!!*)
22.28
22.29 (*----- outcommented during cleanup of args in lucas-interpreter.sml ------------------------\\* )
23.1 --- a/test/Tools/isac/Minisubpbl/200-start-method.sml Tue Feb 04 16:45:36 2020 +0100
23.2 +++ b/test/Tools/isac/Minisubpbl/200-start-method.sml Tue Feb 04 17:11:54 2020 +0100
23.3 @@ -128,7 +128,7 @@
23.4 "~~~~~ and do_next , args:"; val (ptp as (pt, pos as (p, p_))) = (pt,ip);
23.5 Celem.e_metID = get_obj g_metID pt (par_pblobj pt p) (* = false*);
23.6 val thy' = get_obj g_domID pt (par_pblobj pt p);
23.7 - val (srls, is, sc) = Lucin.from_pblobj_or_detail' thy' (p,p_) pt;
23.8 + val (srls, is, sc) = LItool.from_pblobj_or_detail' thy' (p,p_) pt;
23.9 "~~~~~ fun find_next_step , args:"; val ((ptp as(pt, (p, _))), (Rule.Prog prog), (Istate.Pstate ist, ctxt))
23.10 = ((pt, pos), sc, is);
23.11 (*case*) scan_to_tactic (prog, (ptp, ctxt)) (Istate.Pstate ist) (*of*);
23.12 @@ -148,8 +148,8 @@
23.13 "~~~~~ fun scan_dn , args:"; val (((pt, p), ctxt), (ist as {eval, ...}), t) =
23.14 (cc, (ist |> path_down [R]), e);
23.15 val (Program.Tac stac, a') =
23.16 - (*case*) Lucin.check_leaf "next " ctxt eval (get_subst ist) t (*of*);
23.17 - val (m, m') = Lucin.stac2tac_ pt (Proof_Context.theory_of ctxt) stac;
23.18 + (*case*) LItool.check_leaf "next " ctxt eval (get_subst ist) t (*of*);
23.19 + val (m, m') = LItool.stac2tac_ pt (Proof_Context.theory_of ctxt) stac;
23.20 "~~~~~ fun stac2tac_ , args:"; val (_, _, (Const ("Prog_Tac.Rewrite'_Set",_) $ rls $ _)) =
23.21 (pt, (Proof_Context.theory_of ctxt), stac);
23.22 (*+*)case stac2tac_ pt (Proof_Context.theory_of ctxt) stac of (Rewrite_Set "norm_equation", _) => ()
24.1 --- a/test/Tools/isac/Minisubpbl/250-Rewrite_Set-from-method.sml Tue Feb 04 16:45:36 2020 +0100
24.2 +++ b/test/Tools/isac/Minisubpbl/250-Rewrite_Set-from-method.sml Tue Feb 04 17:11:54 2020 +0100
24.3 @@ -45,7 +45,7 @@
24.4 "~~~~~ fun Step_Solve.by_tactic , args:"; val (m, (pt, po as (p, p_))) = (m, (pt, pos));
24.5 (*if*) Celem.e_metID = get_obj g_metID pt (par_pblobj pt p) (* = else*);
24.6 val thy' = get_obj g_domID pt (par_pblobj pt p);
24.7 - val (_, is, sc) = Lucin.from_pblobj_or_detail' thy' (p,p_) pt;
24.8 + val (_, is, sc) = LItool.from_pblobj_or_detail' thy' (p,p_) pt;
24.9
24.10 val Safe_Step (_, _, Rewrite_Set' (_, _, Rls {id = "norm_equation", ...}, _, _)) = (*case*)
24.11 locate_input_tactic sc (pt, po) (fst is) (snd is) m (*of*);
24.12 @@ -101,10 +101,10 @@
24.13 e_metID = get_obj g_metID pt (par_pblobj pt p) = false;
24.14 (*if*) Celem.e_metID = get_obj g_metID pt (par_pblobj pt p)(*else*);
24.15 val thy' = get_obj g_domID pt (par_pblobj pt p);
24.16 - val (_, (ist, ctxt), sc) = Lucin.from_pblobj_or_detail' thy' (p,p_) pt;
24.17 + val (_, (ist, ctxt), sc) = LItool.from_pblobj_or_detail' thy' (p,p_) pt;
24.18
24.19 val Next_Step (_, _, _) =
24.20 - (*case*) LucinNEW.find_next_step sc (pt, pos) ist ctxt (*of*);
24.21 + (*case*) Lucin.find_next_step sc (pt, pos) ist ctxt (*of*);
24.22 "~~~~~ fun find_next_step , args:"; val ((Rule.Prog prog), (ptp as(pt, (p, _))), Istate.Pstate ist, ctxt)
24.23 = (sc, (pt, pos), ist, ctxt);
24.24
24.25 @@ -155,10 +155,10 @@
24.26 "~~~~~ and do_next , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
24.27 (*if*) Celem.e_metID = get_obj g_metID pt (par_pblobj pt p) (*else*);
24.28 val thy' = get_obj g_domID pt (par_pblobj pt p);
24.29 - val (srls, (ist, ctxt), sc) = Lucin.from_pblobj_or_detail' thy' (p,p_) pt;
24.30 + val (srls, (ist, ctxt), sc) = LItool.from_pblobj_or_detail' thy' (p,p_) pt;
24.31
24.32 val Next_Step (_, _, _) =
24.33 - (*case*) LucinNEW.find_next_step sc (pt, pos) ist ctxt (*of*);
24.34 + (*case*) Lucin.find_next_step sc (pt, pos) ist ctxt (*of*);
24.35 "~~~~~ fun find_next_step , args:"; val (Rule.Prog prog, (ptp as(pt, (p, _))), Istate.Pstate ist, ctxt)
24.36 = (sc, (pt, pos), ist, ctxt);
24.37
24.38 @@ -215,9 +215,9 @@
24.39 (*========== a leaf has been found ==========*)
24.40 "~~~~~ fun scan_dn , args:"; val (((pt, p), ctxt), (ist as {eval, ...}), t)
24.41 = (xxx, (ist |> path_down [L, R]), e);
24.42 - val (Program.Tac stac, a') = (*case*) Lucin.check_leaf "next " ctxt eval (get_subst ist) t (*of*);
24.43 + val (Program.Tac stac, a') = (*case*) LItool.check_leaf "next " ctxt eval (get_subst ist) t (*of*);
24.44
24.45 - (*val (m,m') = Lucin.*) stac2tac_ pt (Proof_Context.theory_of ctxt) stac;
24.46 + (*val (m,m') = LItool.*) stac2tac_ pt (Proof_Context.theory_of ctxt) stac;
24.47 "~~~~~ fun stac2tac_ , args:"; val (pt, _, (stac as Const ("Prog_Tac.SubProblem", _) $ spec' $ ags'))
24.48 = (pt, (Proof_Context.theory_of ctxt), stac);
24.49 val (dI, pI, mI) = Prog_Tac.dest_spec spec'
25.1 --- a/test/Tools/isac/Minisubpbl/300-init-subpbl-NEXT_STEP.sml Tue Feb 04 16:45:36 2020 +0100
25.2 +++ b/test/Tools/isac/Minisubpbl/300-init-subpbl-NEXT_STEP.sml Tue Feb 04 17:11:54 2020 +0100
25.3 @@ -47,7 +47,7 @@
25.4
25.5 val Apply_Method mI = (*case*) tac (*of*);
25.6 (*+*)val (_, (_, _, (pt'''', p''''))) =
25.7 - LucinNEW.by_tactic (Tactic.Apply_Method' (mI, NONE, Istate.e_istate, ContextC.e_ctxt)) ist_ctxt ptp;
25.8 + Lucin.by_tactic (Tactic.Apply_Method' (mI, NONE, Istate.e_istate, ContextC.e_ctxt)) ist_ctxt ptp;
25.9 "~~~~~ fun begin_end_prog , args:"; val ((Tactic.Apply_Method' (mI, _, _, _)), (ist, ctxt), (pt, pos as (p, _)))
25.10 = ((Tactic.Apply_Method' (mI, NONE, Istate.e_istate, ContextC.e_ctxt)), ist_ctxt, ptp);
25.11 val {ppc, ...} = Specify.get_met mI;
25.12 @@ -57,10 +57,10 @@
25.13 val itms = if itms <> [] then itms else Chead.complete_metitms oris probl [] ppc
25.14 val thy' = get_obj g_domID pt p;
25.15 val thy = Celem.assoc_thy thy';
25.16 - val srls = Lucin.get_simplifier (pt, pos);
25.17 + val srls = LItool.get_simplifier (pt, pos);
25.18
25.19 (*if*) mI = ["Biegelinien", "ausBelastung"] (*else*);
25.20 - val (is, env, ctxt, scr) = case Lucin.init_pstate srls ctxt itms mI of
25.21 + val (is, env, ctxt, scr) = case LItool.init_pstate srls ctxt itms mI of
25.22 (is as Istate.Pstate {env, ...}, ctxt, scr) => (is, env, ctxt, scr)
25.23 | _ => error "begin_end_prog Apply_Method': uncovered case init_pstate"
25.24
26.1 --- a/test/Tools/isac/Minisubpbl/300-init-subpbl.sml Tue Feb 04 16:45:36 2020 +0100
26.2 +++ b/test/Tools/isac/Minisubpbl/300-init-subpbl.sml Tue Feb 04 17:11:54 2020 +0100
26.3 @@ -113,7 +113,7 @@
26.4 (*return value*) (a', Program.Tac stac');
26.5 "~~~~~ from check_leaf to scan_dn1 return val:"; val (a', Program.Tac stac)
26.6 = ((a' : term option, Program.Tac stac'));
26.7 - val Lucin.Ass (m, v', ctxt) = (*case*) Lucin.associate pt ctxt (m, stac) (*of*);
26.8 + val LItool.Ass (m, v', ctxt) = (*case*) LItool.associate pt ctxt (m, stac) (*of*);
26.9
26.10 (*+*)if is_e_ctxt ctxt then error "ERROR: scan_dn1 returns e_ctxt" else ();
26.11 (*\\--1 end step into relevant call ----------------------------------------------------------//*)
27.1 --- a/test/Tools/isac/Minisubpbl/400-start-meth-subpbl.sml Tue Feb 04 16:45:36 2020 +0100
27.2 +++ b/test/Tools/isac/Minisubpbl/400-start-meth-subpbl.sml Tue Feb 04 17:11:54 2020 +0100
27.3 @@ -54,8 +54,8 @@
27.4 | _ => error "Step_Solve.by_tactic Apply_Method: uncovered case get_obj"
27.5 val thy' = get_obj g_domID pt p;
27.6 val thy = Celem.assoc_thy thy';
27.7 - val srls = Lucin.get_simplifier (pt, pos)
27.8 - val (is, env, ctxt, sc) = case Lucin.init_pstate srls ctxt itms mI of
27.9 + val srls = LItool.get_simplifier (pt, pos)
27.10 + val (is, env, ctxt, sc) = case LItool.init_pstate srls ctxt itms mI of
27.11 (is as Istate.Pstate {env, ...}, ctxt, sc) => (is, env, ctxt, sc)
27.12 | _ => error "Step_Solve.by_tactic Apply_Method: uncovered case init_pstate"
27.13
28.1 --- a/test/Tools/isac/Minisubpbl/470-Check_elementwise-NEXT_STEP.sml Tue Feb 04 16:45:36 2020 +0100
28.2 +++ b/test/Tools/isac/Minisubpbl/470-Check_elementwise-NEXT_STEP.sml Tue Feb 04 17:11:54 2020 +0100
28.3 @@ -50,13 +50,13 @@
28.4 (*if*) ip = p (*else*);
28.5 (*if*) member op = [Pos.Pbl, Pos.Met] p_ (*else*);
28.6
28.7 - LucinNEW.do_next (pt, ip);
28.8 + Lucin.do_next (pt, ip);
28.9 "~~~~~ and do_next , args:"; val ((ptp as (pt, pos as (p, p_)))) = ((pt, ip));
28.10 (*if*) Celem.e_metID = get_obj g_metID pt (par_pblobj pt p) (*else*);
28.11 val thy' = get_obj g_domID pt (par_pblobj pt p);
28.12 - val (srls, (ist, ctxt), sc) = Lucin.from_pblobj_or_detail' thy' (p,p_) pt;
28.13 + val (srls, (ist, ctxt), sc) = LItool.from_pblobj_or_detail' thy' (p,p_) pt;
28.14
28.15 - LucinNEW.find_next_step sc (pt, pos) ist ctxt;
28.16 + Lucin.find_next_step sc (pt, pos) ist ctxt;
28.17 "~~~~~ fun find_next_step , args:"; val (Rule.Prog prog, (ptp as(pt, (p, _))), Istate.Pstate ist, ctxt)
28.18 = (sc, (pt, pos), ist, ctxt);
28.19
29.1 --- a/test/Tools/isac/Minisubpbl/490-nxt-Check_Postcond.sml Tue Feb 04 16:45:36 2020 +0100
29.2 +++ b/test/Tools/isac/Minisubpbl/490-nxt-Check_Postcond.sml Tue Feb 04 17:11:54 2020 +0100
29.3 @@ -47,7 +47,7 @@
29.4 e_metID = get_obj g_metID pt (par_pblobj pt p); (*false*)
29.5 val thy' = get_obj g_domID pt (par_pblobj pt p);
29.6 val (srls, (ist, ctxt), sc) = from_pblobj_or_detail' thy' (p,p_) pt; (*is: which ctxt?*)
29.7 -val End_Program (ist, tac) = LucinNEW.find_next_step sc (pt,pos) ist ctxt;
29.8 +val End_Program (ist, tac) = Lucin.find_next_step sc (pt,pos) ist ctxt;
29.9
29.10 (*+*);tac; (* = Check_Postcond' *)
29.11
30.1 --- a/test/Tools/isac/Minisubpbl/530-error-Check_Elementwise.sml Tue Feb 04 16:45:36 2020 +0100
30.2 +++ b/test/Tools/isac/Minisubpbl/530-error-Check_Elementwise.sml Tue Feb 04 17:11:54 2020 +0100
30.3 @@ -55,10 +55,10 @@
30.4 "~~~~~ and do_next , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
30.5 (*if*) Celem.e_metID = get_obj g_metID pt (par_pblobj pt p) (*else*);
30.6 val thy' = get_obj g_domID pt (par_pblobj pt p);
30.7 - val (srls, (ist, ctxt), sc) = Lucin.from_pblobj_or_detail' thy' (p,p_) pt;
30.8 + val (srls, (ist, ctxt), sc) = LItool.from_pblobj_or_detail' thy' (p,p_) pt;
30.9
30.10 val Next_Step (_, _, Check_elementwise' _) =
30.11 - (*case*) LucinNEW.find_next_step sc (pt, pos) ist ctxt (*of*);
30.12 + (*case*) Lucin.find_next_step sc (pt, pos) ist ctxt (*of*);
30.13 "~~~~~ fun find_next_step , args:"; val ((Rule.Prog prog), (ptp as (pt, (p, _))), Istate.Pstate ist, ctxt)
30.14 = (sc, (pt, pos), ist, ctxt);
30.15
31.1 --- a/test/Tools/isac/Minisubpbl/600-postcond-NEXT_STEP.sml Tue Feb 04 16:45:36 2020 +0100
31.2 +++ b/test/Tools/isac/Minisubpbl/600-postcond-NEXT_STEP.sml Tue Feb 04 17:11:54 2020 +0100
31.3 @@ -109,13 +109,13 @@
31.4 "~~~~~ and do_next , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
31.5 (*if*) Celem.e_metID = get_obj g_metID pt (par_pblobj pt p) (*else*);
31.6 val thy' = get_obj g_domID pt (par_pblobj pt p);
31.7 - val (_, (ist, ctxt), sc) = Lucin.from_pblobj_or_detail' thy' (p,p_) pt;
31.8 + val (_, (ist, ctxt), sc) = LItool.from_pblobj_or_detail' thy' (p,p_) pt;
31.9
31.10 (*+*)istate2str ist
31.11 = "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.12 ^ " ORundef, true, false)"; (*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~true ok*)
31.13
31.14 - (*case*) LucinNEW.find_next_step sc (pt, pos) ist ctxt (*of*);
31.15 + (*case*) Lucin.find_next_step sc (pt, pos) ist ctxt (*of*);
31.16 "~~~~~ fun find_next_step , args:"; val ((Rule.Prog prog), (ptp as(pt, (p, _))), (Pstate ist), ctxt)
31.17 = (sc, (pt, pos), ist, ctxt);
31.18
32.1 --- a/test/Tools/isac/OLDTESTS/root-equ.sml Tue Feb 04 16:45:36 2020 +0100
32.2 +++ b/test/Tools/isac/OLDTESTS/root-equ.sml Tue Feb 04 17:11:54 2020 +0100
32.3 @@ -565,7 +565,7 @@
32.4 val Steps [(m',f',pt',p',c',s')] =
32.5 locate_input_tactic thy' m (pt,(p,p_)) (sc,d) is;
32.6 val is' = get_istate pt' p';
32.7 - LucinNEW.find_next_step thy' sc (pt'(*'*),p') is' (*as (ist, ctxt) ---> ist ctxt*);
32.8 + Lucin.find_next_step thy' sc (pt'(*'*),p') is' (*as (ist, ctxt) ---> ist ctxt*);
32.9
32.10
32.11
33.1 --- a/test/Tools/isac/Test_Isac.thy Tue Feb 04 16:45:36 2020 +0100
33.2 +++ b/test/Tools/isac/Test_Isac.thy Tue Feb 04 17:11:54 2020 +0100
33.3 @@ -89,9 +89,9 @@
33.4 in case of errors here consider ~~/xtest-to-coding.sh *)
33.5 open Kernel;
33.6 open Math_Engine; CalcTreeTEST;
33.7 - open Lucin; itms2args;
33.8 + open LItool.; itms2args;
33.9 open Env;
33.10 - open LucinNEW; scan_dn;
33.11 + open Lucin; scan_dn;
33.12 open Istate;
33.13 open Inform; cas_input;
33.14 open Rtools; trtas2str;
34.1 --- a/test/Tools/isac/Test_Isac_Short.thy Tue Feb 04 16:45:36 2020 +0100
34.2 +++ b/test/Tools/isac/Test_Isac_Short.thy Tue Feb 04 17:11:54 2020 +0100
34.3 @@ -89,9 +89,9 @@
34.4 in case of errors here consider ~~/xtest-to-coding.sh *)
34.5 open Kernel;
34.6 open Math_Engine; CalcTreeTEST;
34.7 - open Lucin; itms2args;
34.8 + open LItool; itms2args;
34.9 open Env;
34.10 - open LucinNEW; scan_dn;
34.11 + open Lucin; scan_dn;
34.12 open Istate;
34.13 open Inform; cas_input;
34.14 open Rtools; trtas2str;
34.15 @@ -216,7 +216,7 @@
34.16 ML_file "Specify/step-specify.sml"
34.17
34.18 ML_file "Interpret/rewtools.sml"
34.19 - ML_file "Interpret/script.sml"
34.20 + ML_file "Interpret/li-tool.sml"
34.21 ML_file "Interpret/inform.sml"
34.22 ML_file "Interpret/lucas-interpreter.sml"
34.23 ML_file "Interpret/step-solve.sml"
35.1 --- a/test/Tools/isac/Test_Some.thy Tue Feb 04 16:45:36 2020 +0100
35.2 +++ b/test/Tools/isac/Test_Some.thy Tue Feb 04 17:11:54 2020 +0100
35.3 @@ -8,9 +8,9 @@
35.4 in case of errors here consider ~~/xtest-to-coding.sh *)
35.5 open Kernel;
35.6 open Math_Engine; CalcTreeTEST;
35.7 - open Lucin; itms2args;
35.8 + open LItool.; itms2args;
35.9 open Env;
35.10 - open LucinNEW; scan_dn;
35.11 + open Lucin; scan_dn;
35.12 open Istate;
35.13 open Inform; cas_input;
35.14 open Rtools; trtas2str;
35.15 @@ -131,7 +131,7 @@
35.16 (*if*) Celem.e_metID = get_obj g_metID pt (par_pblobj pt p) (*else*);
35.17 \<close> ML \<open>
35.18 val thy' = get_obj g_domID pt (par_pblobj pt p);
35.19 - val (_, (ist, ctxt), sc) = Lucin.from_pblobj_or_detail' thy' (p,p_) pt;
35.20 + val (_, (ist, ctxt), sc) = LItool.from_pblobj_or_detail' thy' (p,p_) pt;
35.21 \<close> ML \<open>
35.22 val Next_Step (_, _, Rewrite_Set' ("Poly", _, Seq {id = "norm_Poly", ...}, _, _)) =
35.23 find_next_step sc (pt, pos) ist ctxt (*of*);
35.24 @@ -155,7 +155,7 @@
35.25 \<close> ML \<open>
35.26 (*if*) Tactical.contained_in t (*else*);
35.27 \<close> ML \<open>
35.28 - val (Program.Tac prog_tac, form_arg) = (*case*) Lucin.check_leaf "next " ctxt eval (get_subst ist) t (*of*);
35.29 + val (Program.Tac prog_tac, form_arg) = (*case*) LItool.check_leaf "next " ctxt eval (get_subst ist) t (*of*);
35.30 \<close> ML \<open>
35.31 val Accept_Tac (Rewrite_Set' ("Poly", _, Seq {id = "norm_Poly", ...}, _, _), _, _) =
35.32 check_tac cc ist (form_arg, prog_tac) (*return from xxx*);
35.33 @@ -208,7 +208,7 @@
35.34 (*if*) Celem.e_metID = get_obj g_metID pt (par_pblobj pt p) (*else*);
35.35 \<close> ML \<open>
35.36 val thy' = get_obj g_domID pt (par_pblobj pt p);
35.37 - val (_, (ist, ctxt), sc) = Lucin.from_pblobj_or_detail' thy' (p,p_) pt;
35.38 + val (_, (ist, ctxt), sc) = LItool.from_pblobj_or_detail' thy' (p,p_) pt;
35.39 \<close> ML \<open>
35.40 (** )val End_Program (ist, tac) = ( *case*) find_next_step sc (pt, pos) ist ctxt (*of*);
35.41 \<close> ML \<open>
36.1 --- a/test/Tools/isac/Test_Some_meld.thy Tue Feb 04 16:45:36 2020 +0100
36.2 +++ b/test/Tools/isac/Test_Some_meld.thy Tue Feb 04 17:11:54 2020 +0100
36.3 @@ -6,10 +6,10 @@
36.4 in case of errors here consider ~~/xtest-to-coding.sh *)
36.5 open Kernel;
36.6 open Math_Engine; CalcTreeTEST;
36.7 - open Lucin; itms2args;
36.8 + open LItool.; itms2args;
36.9 open Env;
36.10 open Exec;
36.11 - open LucinNEW; scan_dn;
36.12 + open Lucin; scan_dn;
36.13 open Istate;
36.14 open Inform; cas_input;
36.15 open Rtools; trtas2str;