1.1 --- a/src/Tools/isac/CalcElements/KEStore.thy Wed Apr 01 14:14:46 2020 +0200
1.2 +++ b/src/Tools/isac/CalcElements/KEStore.thy Wed Apr 01 18:54:03 2020 +0200
1.3 @@ -6,6 +6,7 @@
1.4
1.5 begin
1.6 ML_file libraryC.sml
1.7 +ML_file "rule-def.sml"
1.8 ML_file rule.sml
1.9 ML_file calcelems.sml
1.10
2.1 --- a/src/Tools/isac/Interpret/error-pattern.sml Wed Apr 01 14:14:46 2020 +0200
2.2 +++ b/src/Tools/isac/Interpret/error-pattern.sml Wed Apr 01 18:54:03 2020 +0200
2.3 @@ -43,18 +43,17 @@
2.4 (*the lists contain eq-al elem-pairs at the beginning;
2.5 return first list reverted (again) - ie. in order as required subsequently*)
2.6 fun dropwhile' equal (f1::f2::fs) (i1::i2::is) =
2.7 - if equal f1 i1
2.8 - then
2.9 + if equal f1 i1 then
2.10 if equal f2 i2 then dropwhile' equal (f2 :: fs) (i2 :: is)
2.11 else (rev (f1 :: f2 :: fs), i1 :: i2 :: is)
2.12 else error "dropwhile': did not start with equal elements"
2.13 | dropwhile' equal (f::fs) [i] =
2.14 - if equal f i
2.15 - then (rev (f::fs), [i])
2.16 + if equal f i then
2.17 + (rev (f::fs), [i])
2.18 else error "dropwhile': did not start with equal elements"
2.19 | dropwhile' equal [f] (i::is) =
2.20 - if equal f i
2.21 - then ([f], i::is)
2.22 + if equal f i then
2.23 + ([f], i::is)
2.24 else error "dropwhile': did not start with equal elements"
2.25 | dropwhile' _ _ _ = error "dropwhile': uncovered case"
2.26
2.27 @@ -85,8 +84,7 @@
2.28 | (fod, []) => if derivat fod = ifo then (true, fod) (*ifo is normal form*) else (false, [])
2.29 | ([], ifod) => if fo = derivat ifod then (true, ((map rev_deriv') o rev) ifod) else (false, [])
2.30 | (fod, ifod) =>
2.31 - if derivat fod = derivat ifod (*common normal form found*)
2.32 - then
2.33 + if derivat fod = derivat ifod (*common normal form found*) then
2.34 let
2.35 val (fod', rifod') = dropwhile' equal (rev fod) (rev ifod)
2.36 in (true, fod' @ (map rev_deriv' rifod')) end
2.37 @@ -101,8 +99,7 @@
2.38 val (res', _, _, rewritten) =
2.39 Rewrite.rew_sub (Rule.Isac()) 1 subst Rule.e_rew_ord Rule.e_rls false [] (HOLogic.Trueprop $ pat) res;
2.40 in
2.41 - if rewritten
2.42 - then
2.43 + if rewritten then
2.44 let
2.45 val norm_res = case Rewrite.rewrite_set_inst_ (Rule.Isac()) false subst rls res' of
2.46 NONE => res'
2.47 @@ -139,8 +136,8 @@
2.48 val (form', _, _, rewritten) =
2.49 Rewrite.rew_sub (Rule.Isac()) 1 subst Rule.e_rew_ord Rule.e_rls false [] (HOLogic.Trueprop $ pat) form;
2.50 in (*the fillpat of the thm must be dedicated to errpatID*)
2.51 - if errpatID = erpaID andalso rewritten
2.52 - then SOME (fillpatID, HOLogic.mk_eq (form, form'), thm, subs_opt)
2.53 + if errpatID = erpaID andalso rewritten then
2.54 + SOME (fillpatID, HOLogic.mk_eq (form, form'), thm, subs_opt)
2.55 else NONE
2.56 end
2.57
2.58 @@ -189,8 +186,8 @@
2.59 |Tactic.Rewrite' (_, _, _, _, _, _, (res, _)) => res
2.60 | t => error ("is_exactly_equal: uncovered case for " ^ Tactic.string_of t)
2.61 in
2.62 - if not (ifo = res)
2.63 - then ("input does not exactly fill the gaps", Tactic.Tac "")
2.64 + if not (ifo = res) then
2.65 + ("input does not exactly fill the gaps", Tactic.Tac "")
2.66 else ("ok", tac)
2.67 end
2.68 end
3.1 --- a/src/Tools/isac/Interpret/li-tool.sml Wed Apr 01 14:14:46 2020 +0200
3.2 +++ b/src/Tools/isac/Interpret/li-tool.sml Wed Apr 01 18:54:03 2020 +0200
3.3 @@ -13,7 +13,7 @@
3.4 | Not_Associated;
3.5 val associate: Ctree.ctree -> Proof.context -> (Tactic.T * term (*..Prog_Tac*)) -> ass
3.6
3.7 - val implicit_take : 'a -> Program.T -> (term * term) list -> term option
3.8 + val implicit_take : Program.T -> (term * term) list -> term option
3.9 val init_pstate : Rule.rls -> Proof.context -> Model.itm list -> Celem.metID ->
3.10 Istate.T * Proof.context * Program.T
3.11
3.12 @@ -27,12 +27,12 @@
3.13 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
3.14 (*NONE*)
3.15 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
3.16 - val itms2args : 'a -> Celem.metID -> Model.itm list -> term list
3.17 + val arguments_from_model : Celem.metID -> Model.itm list -> term list
3.18 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
3.19 end
3.20
3.21 -(* traces the leaves (ie. non-tactical nodes) of Prog found by find_next_step, see "and scr" *)
3.22 -val trace_LI = Unsynchronized.ref false; (* TODO: how are traces done in Isabelle? *)
3.23 +(* traces the leaves (ie. non-tactical nodes) of Prog found by find_next_step *)
3.24 +val trace_LI = Unsynchronized.ref false; (* TODO: adopt Isabelle's tracing *)
3.25
3.26 (**)
3.27 structure LItool(**): LUCAS_INTERPRETER_TOOL(**) =
3.28 @@ -41,41 +41,33 @@
3.29 open Ctree
3.30 open Pos
3.31
3.32 -(* determine the first tactic in case of a program with one argument (like simplification)
3.33 - and without an initial Tactic.Take *)
3.34 -fun implicit_take thy (Rule.Prog prog) env =
3.35 - (case Prog_Tac.get_first thy prog of
3.36 - NONE => NONE
3.37 - | SOME prog_tac => SOME (subst_atomic env prog_tac))
3.38 - | implicit_take _ _ _ = error "implicit_take: no match";
3.39 +(* find the formal argument of a tactic in case there is only one (e.g. in simplification) *)
3.40 +fun implicit_take (Rule.Prog prog) env =
3.41 + (case Prog_Tac.get_first_argument prog of
3.42 + NONE => NONE
3.43 + | SOME prog_tac => SOME (subst_atomic env prog_tac))
3.44 + | implicit_take _ _ = error "implicit_take: no match";
3.45
3.46 -type dsc = typ; (* <-> nam..unknow in Descript.thy *)
3.47 -
3.48 -(*.create the actual parameters (args) of script: their order
3.49 - is given by the order in met.pat .*)
3.50 -(*WN.5.5.03: ?: does this allow for different descriptions ???
3.51 - ?: why not taken from formal args of script ???
3.52 -!: FIXXXME penv: push it here in itms2args into script-evaluation*)
3.53 -val errmsg = "ERROR: the guard is missing (#ppc in 'type met' added in prep_met)."
3.54 -fun errmsg2 d itms = ("itms2args: '" ^ Rule.term2str d ^ "' not in itms:\n" ^
3.55 -"itms:\n" ^ Model.itms2str_ @{context} itms)
3.56 -fun itms2args _ mI itms =
3.57 +(* *)
3.58 +val error_msg_1 = "ERROR: the guard is missing (#ppc in 'type met' added in prep_met)."
3.59 +fun error_msg_2 d itms = ("arguments_from_model: '" ^ Rule.term2str d ^ "' not in itms:\n" ^
3.60 + "itms:\n" ^ Model.itms2str_ @{context} itms)
3.61 +(* turn model-items into arguments for a program *)
3.62 +fun arguments_from_model mI itms =
3.63 let
3.64 val mvat = Model.max_vt itms
3.65 fun okv mvat (_, vats, b, _, _) = member op = vats mvat andalso b
3.66 val itms = filter (okv mvat) itms
3.67 fun test_dsc d (_, _, _, _, itm_) = (d = Model.d_in itm_)
3.68 fun itm2arg itms (_,(d,_)) =
3.69 - case find_first (test_dsc d) itms of
3.70 - NONE => raise ERROR (errmsg2 d itms)
3.71 - | SOME (_, _, _, _, itm_) => Model.penvval_in itm_
3.72 - (*| SOME (_,_,_,_,itm_) => mk_arg thy (Model.d_in itm_) (ts_in itm_);
3.73 - penv postponed; presently penv holds already Env.update for script*)
3.74 + case find_first (test_dsc d) itms of
3.75 + NONE => raise ERROR (error_msg_2 d itms)
3.76 + | SOME (_, _, _, _, itm_) => Model.penvval_in itm_
3.77 val pats = (#ppc o Specify.get_met) mI
3.78 - val _ = if pats = [] then raise ERROR errmsg else ()
3.79 + val _ = if pats = [] then raise ERROR error_msg_1 else ()
3.80 in (flat o (map (itm2arg itms))) pats end;
3.81
3.82 -(* convert a Prog_Tac to Tactic.input *)
3.83 +(* convert a Prog_Tac to Tactic.input; specific for "Prog_Tac.SubProblem" *)
3.84 fun tac_from_prog _ thy (Const ("Prog_Tac.Rewrite", _) $ thmID $ _) =
3.85 let
3.86 val tid = HOLogic.dest_string thmID
3.87 @@ -103,165 +95,145 @@
3.88
3.89 datatype ass =
3.90 Associated of
3.91 - Tactic.T (* Subproblem' gets args instantiated in associate *)
3.92 - * term (* resulting from application of Tactic.T *)
3.93 - * Proof.context (* updated by assumptioons from Rewrite* *)
3.94 + Tactic.T (* Subproblem' gets args instantiated in associate *)
3.95 + * term (* resulting from application of Tactic.T *)
3.96 + * Proof.context (* updated by assumptioons from Rewrite* *)
3.97 | Ass_Weak of Tactic.T * term * Proof.context
3.98 | Not_Associated;
3.99
3.100 +fun trace_msg_3 tac =
3.101 + if (!trace_LI) then
3.102 + tracing("@@@ the \"tac_\" proposed to apply does NOT match the leaf found in the program:\n" ^
3.103 + "@@@ tac_ = \"" ^ Tactic.string_of tac ^ "\"")
3.104 + else ();
3.105 (*
3.106 associate is the ONLY code within by_tactic, which handles Tactic.T individually;
3.107 thus it does ContextC.insert_assumptions in case of Rewrite*.
3.108 + The argument Ctree.ctree is required only for Subproblem'.
3.109 *)
3.110 -fun trace_msg_3 tac =
3.111 - if (!trace_LI)
3.112 - then tracing("@@@ the \"tac_\" proposed to apply does NOT match the leaf found in the program:\n"
3.113 - ^ "@@@ tac_ = \"" ^ Tactic.string_of tac ^ "\"")
3.114 - else ();
3.115 fun associate _ ctxt (m as Tactic.Rewrite_Inst'
3.116 - (_, _, _, _, _, thm'' as (thmID, _), f, (f', asms')), stac) =
3.117 - (case stac of
3.118 - (Const ("Prog_Tac.Rewrite'_Inst", _) $ _ $ thmID_ $ f_) =>
3.119 - if thmID = HOLogic.dest_string thmID_
3.120 - then
3.121 - if f = f_
3.122 - then Associated (m, f', ContextC.insert_assumptions asms' ctxt)
3.123 - else Ass_Weak (m, f', ContextC.insert_assumptions asms' ctxt)
3.124 - else ((*tracing"3### associate ..Not_Associated";*) Not_Associated)
3.125 - | (Const ("Prog_Tac.Rewrite'_Set'_Inst",_) $ _ $ rls_ $ f_) =>
3.126 - if Rtools.contains_rule (Rule.Thm thm'') (assoc_rls (HOLogic.dest_string rls_))
3.127 - then if f = f_ then Associated (m, f', ContextC.insert_assumptions asms' ctxt)
3.128 - else Ass_Weak (m, f', ContextC.insert_assumptions asms' ctxt)
3.129 - else Not_Associated
3.130 - | _ => Not_Associated)
3.131 + (_, _, _, _, _, thm'' as (thmID, _), f, (f', asms')), stac) =
3.132 + (case stac of
3.133 + (Const ("Prog_Tac.Rewrite'_Inst", _) $ _ $ thmID_ $ f_) =>
3.134 + if thmID = HOLogic.dest_string thmID_ then
3.135 + if f = f_ then
3.136 + Associated (m, f', ContextC.insert_assumptions asms' ctxt)
3.137 + else Ass_Weak (m, f', ContextC.insert_assumptions asms' ctxt)
3.138 + else Not_Associated
3.139 + | (Const ("Prog_Tac.Rewrite'_Set'_Inst",_) $ _ $ rls_ $ f_) =>
3.140 + if Rtools.contains_rule (Rule.Thm thm'') (assoc_rls (HOLogic.dest_string rls_)) then
3.141 + if f = f_ then
3.142 + Associated (m, f', ContextC.insert_assumptions asms' ctxt)
3.143 + else Ass_Weak (m, f', ContextC.insert_assumptions asms' ctxt)
3.144 + else Not_Associated
3.145 + | _ => Not_Associated)
3.146 | associate _ ctxt (m as Tactic.Rewrite' (_, _, _, _, thm'' as (thmID, _), f, (f', asms')), stac) =
3.147 - (case stac of
3.148 - (Const ("Prog_Tac.Rewrite", _) $ thmID_ $ f_) =>
3.149 - if thmID = HOLogic.dest_string thmID_
3.150 - then
3.151 - if f = f_
3.152 - then Associated (m, f', ContextC.insert_assumptions asms' ctxt)
3.153 - else Ass_Weak (m, f', ContextC.insert_assumptions asms' ctxt)
3.154 - else Not_Associated
3.155 - | (Const ("Prog_Tac.Rewrite'_Set", _) $ rls_ $ f_) =>
3.156 - if Rtools.contains_rule (Rule.Thm thm'') (assoc_rls (HOLogic.dest_string rls_))
3.157 - then
3.158 - if f = f_
3.159 - then Associated (m, f', ContextC.insert_assumptions asms' ctxt)
3.160 - else Ass_Weak (m, f', ContextC.insert_assumptions asms' ctxt)
3.161 - else Not_Associated
3.162 - | _ => Not_Associated)
3.163 + (case stac of
3.164 + (Const ("Prog_Tac.Rewrite", _) $ thmID_ $ f_) =>
3.165 + if thmID = HOLogic.dest_string thmID_ then
3.166 + if f = f_ then
3.167 + Associated (m, f', ContextC.insert_assumptions asms' ctxt)
3.168 + else Ass_Weak (m, f', ContextC.insert_assumptions asms' ctxt)
3.169 + else Not_Associated
3.170 + | (Const ("Prog_Tac.Rewrite'_Set", _) $ rls_ $ f_) =>
3.171 + if Rtools.contains_rule (Rule.Thm thm'') (assoc_rls (HOLogic.dest_string rls_)) then
3.172 + if f = f_ then
3.173 + Associated (m, f', ContextC.insert_assumptions asms' ctxt)
3.174 + else Ass_Weak (m, f', ContextC.insert_assumptions asms' ctxt)
3.175 + else Not_Associated
3.176 + | _ => Not_Associated)
3.177 | associate _ ctxt (m as Tactic.Rewrite_Set_Inst' (_, _, _, rls, f, (f', asms')),
3.178 - (Const ("Prog_Tac.Rewrite'_Set'_Inst", _) $ _ $ rls_ $ f_)) =
3.179 - if Rule.id_rls rls = HOLogic.dest_string rls_
3.180 - then
3.181 - if f = f_
3.182 - then Associated (m, f', ContextC.insert_assumptions asms' ctxt)
3.183 - else Ass_Weak (m ,f', ContextC.insert_assumptions asms' ctxt)
3.184 - else Not_Associated
3.185 + (Const ("Prog_Tac.Rewrite'_Set'_Inst", _) $ _ $ rls_ $ f_)) =
3.186 + if Rule.id_rls rls = HOLogic.dest_string rls_ then
3.187 + if f = f_ then
3.188 + Associated (m, f', ContextC.insert_assumptions asms' ctxt)
3.189 + else Ass_Weak (m ,f', ContextC.insert_assumptions asms' ctxt)
3.190 + else Not_Associated
3.191 | associate _ ctxt (m as Tactic.Detail_Set_Inst' (_, _, _, rls, f, (f', asms')),
3.192 - (Const ("Prog_Tac.Rewrite'_Set'_Inst", _) $ _ $ rls_ $ f_)) =
3.193 - if Rule.id_rls rls = HOLogic.dest_string rls_
3.194 - then
3.195 - if f = f_
3.196 - then Associated (m, f', ContextC.insert_assumptions asms' ctxt)
3.197 - else Ass_Weak (m ,f', ContextC.insert_assumptions asms' ctxt)
3.198 - else Not_Associated
3.199 + (Const ("Prog_Tac.Rewrite'_Set'_Inst", _) $ _ $ rls_ $ f_)) =
3.200 + if Rule.id_rls rls = HOLogic.dest_string rls_ then
3.201 + if f = f_ then
3.202 + Associated (m, f', ContextC.insert_assumptions asms' ctxt)
3.203 + else Ass_Weak (m ,f', ContextC.insert_assumptions asms' ctxt)
3.204 + else Not_Associated
3.205 | associate _ ctxt (m as Tactic.Rewrite_Set' (_, _, rls, f, (f', asms')),
3.206 - (Const ("Prog_Tac.Rewrite'_Set", _) $ rls_ $ f_)) =
3.207 - if Rule.id_rls rls = HOLogic.dest_string rls_
3.208 - then
3.209 - if f = f_
3.210 - then Associated (m, f', ContextC.insert_assumptions asms' ctxt)
3.211 - else Ass_Weak (m ,f', ContextC.insert_assumptions asms' ctxt)
3.212 - else Not_Associated
3.213 + (Const ("Prog_Tac.Rewrite'_Set", _) $ rls_ $ f_)) =
3.214 + if Rule.id_rls rls = HOLogic.dest_string rls_ then
3.215 + if f = f_ then
3.216 + Associated (m, f', ContextC.insert_assumptions asms' ctxt)
3.217 + else Ass_Weak (m ,f', ContextC.insert_assumptions asms' ctxt)
3.218 + else Not_Associated
3.219 | associate _ ctxt (m as Tactic.Detail_Set' (_, _, rls, f, (f', asms')),
3.220 - (Const ("Prog_Tac.Rewrite'_Set", _) $ rls_ $ f_)) =
3.221 - if Rule.id_rls rls = HOLogic.dest_string rls_
3.222 - then
3.223 - if f = f_
3.224 - then Associated (m, f', ContextC.insert_assumptions asms' ctxt)
3.225 - else Ass_Weak (m ,f', ContextC.insert_assumptions asms' ctxt)
3.226 - else Not_Associated
3.227 + (Const ("Prog_Tac.Rewrite'_Set", _) $ rls_ $ f_)) =
3.228 + if Rule.id_rls rls = HOLogic.dest_string rls_ then
3.229 + if f = f_ then
3.230 + Associated (m, f', ContextC.insert_assumptions asms' ctxt)
3.231 + else Ass_Weak (m ,f', ContextC.insert_assumptions asms' ctxt)
3.232 + else Not_Associated
3.233 | associate _ ctxt (m as Tactic.Calculate' (_, op_, f, (f', _)), stac) =
3.234 - (case stac of
3.235 - (Const ("Prog_Tac.Calculate",_) $ op__ $ f_) =>
3.236 - if op_ = HOLogic.dest_string op__
3.237 - then
3.238 - if f = f_
3.239 - then Associated (m, f', ctxt)
3.240 - else Ass_Weak (m ,f', ctxt)
3.241 - else Not_Associated
3.242 - | (Const ("Prog_Tac.Rewrite'_Set'_Inst", _) $ _ $ rls_ $ f_) =>
3.243 - let val thy = Celem.assoc_thy "Isac_Knowledge";
3.244 - in
3.245 - if Rtools.contains_rule (Rule.Num_Calc (assoc_calc' thy op_ |> snd))
3.246 - (assoc_rls (HOLogic.dest_string rls_))
3.247 - then
3.248 - if f = f_
3.249 - then Associated (m, f', ctxt)
3.250 - else Ass_Weak (m ,f', ctxt)
3.251 + (case stac of
3.252 + (Const ("Prog_Tac.Calculate",_) $ op__ $ f_) =>
3.253 + if op_ = HOLogic.dest_string op__ then
3.254 + if f = f_ then Associated (m, f', ctxt) else Ass_Weak (m ,f', ctxt)
3.255 + else Not_Associated
3.256 + | (Const ("Prog_Tac.Rewrite'_Set'_Inst", _) $ _ $ rls_ $ f_) =>
3.257 + if Rtools.contains_rule (Rule.Num_Calc (assoc_calc' (Celem.assoc_thy "Isac_Knowledge")
3.258 + op_ |> snd)) (assoc_rls (HOLogic.dest_string rls_)) then
3.259 + if f = f_ then Associated (m, f', ctxt) else Ass_Weak (m ,f', ctxt)
3.260 else Not_Associated
3.261 - end
3.262 - | (Const ("Prog_Tac.Rewrite'_Set",_) $ rls_ $ f_) =>
3.263 - let val thy = Celem.assoc_thy "Isac_Knowledge";
3.264 - in
3.265 - if Rtools.contains_rule (Rule.Num_Calc (assoc_calc' thy op_ |> snd))
3.266 - (assoc_rls (HOLogic.dest_string rls_))
3.267 - then
3.268 - if f = f_
3.269 - then Associated (m, f', ctxt)
3.270 - else Ass_Weak (m ,f', ctxt)
3.271 + | (Const ("Prog_Tac.Rewrite'_Set",_) $ rls_ $ f_) =>
3.272 + if Rtools.contains_rule (Rule.Num_Calc (assoc_calc' ( Celem.assoc_thy "Isac_Knowledge")
3.273 + op_ |> snd)) (assoc_rls (HOLogic.dest_string rls_)) then
3.274 + if f = f_ then Associated (m, f', ctxt) else Ass_Weak (m ,f', ctxt)
3.275 else Not_Associated
3.276 - end
3.277 - | _ => Not_Associated)
3.278 + | _ => Not_Associated)
3.279 | associate _ ctxt (m as Tactic.Check_elementwise' (consts, _, (consts_chkd, _)),
3.280 - (Const ("Prog_Tac.Check'_elementwise",_) $ consts' $ _)) =
3.281 - if consts = consts'
3.282 - then Associated (m, consts_chkd, ctxt)
3.283 - else Not_Associated
3.284 + (Const ("Prog_Tac.Check'_elementwise",_) $ consts' $ _)) =
3.285 + if consts = consts' then Associated (m, consts_chkd, ctxt) else Not_Associated
3.286 | associate _ ctxt (m as Tactic.Or_to_List' (_, list), (Const ("Prog_Tac.Or'_to'_List", _) $ _)) =
3.287 - Associated (m, list, ctxt)
3.288 - | associate _ ctxt (m as Tactic.Take' term, (Const ("Prog_Tac.Take", _) $ _)) = Associated (m, term, ctxt)
3.289 + Associated (m, list, ctxt)
3.290 + | associate _ ctxt (m as Tactic.Take' term, (Const ("Prog_Tac.Take", _) $ _)) =
3.291 + Associated (m, term, ctxt)
3.292 | associate _ ctxt (m as Tactic.Substitute' (ro, erls, subte, f, f'),
3.293 - (Const ("Prog_Tac.Substitute", _) $ _ $ t)) =
3.294 - if f = t then Associated (m, f', ctxt)
3.295 - else (*compare | applicable_in (p,p_) pt (m as Substitute sube)*)
3.296 - if foldl and_ (true, map TermC.contains_Var subte)
3.297 - then
3.298 - let val t' = subst_atomic (map HOLogic.dest_eq subte (*TODO subte2subst*)) t
3.299 - in if t = t' then error "associate: Substitute' not applicable to val of Expr"
3.300 - else Associated (Tactic.Substitute' (ro, erls, subte, t, t'), t', ctxt)
3.301 - end
3.302 - else (case Rewrite.rewrite_terms_ (Rule.Isac ()) ro erls subte t of
3.303 - SOME (t', _) => Associated (Tactic.Substitute' (ro, erls, subte, t, t'), t', ctxt)
3.304 - | NONE => error "associate: Substitute' not applicable to val of Expr")
3.305 + (Const ("Prog_Tac.Substitute", _) $ _ $ t)) =
3.306 + if f = t then
3.307 + Associated (m, f', ctxt)
3.308 + else (*compare | applicable_in (p,p_) pt (m as Substitute sube)*)
3.309 + if foldl and_ (true, map TermC.contains_Var subte) then
3.310 + let
3.311 + val t' = subst_atomic (map HOLogic.dest_eq subte) t
3.312 + in
3.313 + if t = t' then error "associate: Substitute' not applicable to val of Expr"
3.314 + else Associated (Tactic.Substitute' (ro, erls, subte, t, t'), t', ctxt)
3.315 + end
3.316 + else
3.317 + (case Rewrite.rewrite_terms_ (Rule.Isac ()) ro erls subte t of
3.318 + SOME (t', _) => Associated (Tactic.Substitute' (ro, erls, subte, t, t'), t', ctxt)
3.319 + | NONE => error "associate: Substitute' not applicable to val of Expr")
3.320 | associate pt ctxt (Tactic.Subproblem' ((domID, pblID, _), _, _, _, _, _),
3.321 - (stac as Const ("Prog_Tac.SubProblem", _) $ _ $ _)) =
3.322 - (case Sub_Problem.tac_from_prog pt stac of
3.323 - (_, tac as Tactic.Subproblem' ((dI, pI, _), _, _, _, _, f)) =>
3.324 - if domID = dI andalso pblID = pI
3.325 - then Associated (tac, f, ctxt)
3.326 - else Not_Associated
3.327 - | _ => raise ERROR ("associate: uncovered case"))
3.328 + (stac as Const ("Prog_Tac.SubProblem", _) $ _ $ _)) =
3.329 + (case Sub_Problem.tac_from_prog pt stac of
3.330 + (_, tac as Tactic.Subproblem' ((dI, pI, _), _, _, _, _, f)) =>
3.331 + if domID = dI andalso pblID = pI then Associated (tac, f, ctxt) else Not_Associated
3.332 + | _ => raise ERROR ("associate: uncovered case"))
3.333 | associate _ _ (tac, _) =
3.334 (trace_msg_3 tac; Not_Associated);
3.335
3.336 (* create the initial interpreter state
3.337 - from the items of the guard and the formal arguments of the partial_function.
3.338 + from the items of the guard and the formal arguments of the program.
3.339 Note on progression from (a) type fmz_ \<longrightarrow> (e) arguments of the partial_function:
3.340 (a) fmz is given by a math author
3.341 (b) fmz_ is transformed to ori list as a prerequisite for efficient interactive modelling
3.342 (c) modelling creates an itm list from ori list + possible user input
3.343 - (d) specifying a theory might add some items and create a guard for the partial_function
3.344 - (e) fun relate_args creates an environment for evaluating the partial_function.
3.345 -Note on sequence-relation (a) -- (e), i.e. the (formal) arguments of the partial_function:
3.346 + (d) specifying a theory might add some items and create a guard for the program
3.347 + (e) fun relate_args creates an environment for evaluating the program.
3.348 +Note on sequence-relation (a) -- (e), i.e. the (formal) arguments of the program:
3.349 * Since the arguments of the partial_function have no description (see Descript.thy),
3.350 (e) depends on the sequence in fmz_ and on the types of the formal arguments.
3.351 * pairing formal arguments with itm's follows the sequence
3.352 * Thus the resulting sequence-relation can be ambiguous.
3.353 * Ambiguities are done by rearranging fmz_ or the formal arguments.
3.354 - * The latter is easier, albeit not optimal: a fmz_ can be used by different partial_functions.
3.355 + * The latter is easier, albeit not optimal: a fmz_ can be used by different programs.
3.356 *)
3.357 local
3.358 val errmsg = "ERROR: found no actual arguments for prog. of "
3.359 @@ -297,7 +269,7 @@
3.360 fun init_pstate srls ctxt itms metID =
3.361 let
3.362 val itms = Specify.hack_until_review_Specify_2 metID itms
3.363 - val actuals = itms2args (Proof_Context.theory_of ctxt) metID itms
3.364 + val actuals = arguments_from_model metID itms
3.365 val _ = if actuals <> [] then () else raise ERROR (errmsg ^ strs2str' metID)
3.366 val (scr, sc) = (case (#scr o Specify.get_met) metID of
3.367 scr as Rule.Prog sc => (trace_init metID; (scr, sc))
3.368 @@ -327,6 +299,7 @@
3.369 end;
3.370 end (*local*)
3.371
3.372 +(* get the simplifier of the current method *)
3.373 fun get_simplifier (pt, (p, _)) =
3.374 let
3.375 val p' = Ctree.par_pblobj pt p
3.376 @@ -334,12 +307,12 @@
3.377 val {srls, ...} = Specify.get_met metID
3.378 in srls end
3.379
3.380 +(* resume program interpretation at the beginning of a step *)
3.381 fun resume_prog thy (p, p_) pt =
3.382 let
3.383 val (is_problem, p', rls') = parent_node pt p
3.384 in
3.385 - if is_problem
3.386 - then
3.387 + if is_problem then
3.388 let
3.389 val metID = get_obj g_metID pt p'
3.390 val {srls, ...} = Specify.get_met metID
3.391 @@ -347,16 +320,15 @@
3.392 case get_loc pt (p, p_) of
3.393 (Istate.Pstate ist, ctxt) => (Istate.Pstate (Istate.set_eval srls ist), ctxt)
3.394 | _ => raise ERROR "resume_prog: unexpected result from get_loc"
3.395 - in ((is, ctxt), (#scr o Specify.get_met) metID) end
3.396 - else (* 3 *)
3.397 + in
3.398 + ((is, ctxt), (#scr o Specify.get_met) metID)
3.399 + end
3.400 + else
3.401 (get_loc pt (p, p_),
3.402 Rule.Prog (Auto_Prog.gen (Celem.assoc_thy thy) (get_last_formula (pt, (p, p_))) rls'))
3.403 end
3.404
3.405 -(*
3.406 - handle a leaf at the end of recursive descent; a leaf is either a Prog_Tac or a Prog_Expr.
3.407 - snd of return value is the formal arguments in case of currying.
3.408 -*)
3.409 +
3.410 fun trace_msg_1 call t stac =
3.411 if (! trace_LI) then
3.412 tracing ("@@@ " ^ call ^ " leaf \"" ^ Rule.term2str t ^ "\" \<longrightarrow> Tac \"" ^ Rule.term2str stac ^ "\"")
3.413 @@ -365,19 +337,22 @@
3.414 if (! trace_LI) then
3.415 tracing("@@@ " ^ call ^ " leaf '" ^ Rule.term2str t ^ "' \<longrightarrow> Expr \"" ^ Rule.term2str lexpr' ^ "\"")
3.416 else ();
3.417 -
3.418 +(*
3.419 + check a leaf at the end of recursive descent; a leaf is either a Prog_Tac or a Prog_Expr.
3.420 + snd of return value is the formal arguments in case of currying.
3.421 +*)
3.422 fun check_leaf call ctxt srls (E, (a, v)) t =
3.423 case Prog_Tac.eval_leaf E a v t of
3.424 (Program.Tac stac, a') =>
3.425 - let val stac' =
3.426 - Rewrite.eval_prog_expr (Proof_Context.theory_of ctxt) srls
3.427 + let
3.428 + val stac' = Rewrite.eval_prog_expr (Proof_Context.theory_of ctxt) srls
3.429 (subst_atomic (Env.update_opt E (a, v)) stac)
3.430 in
3.431 (trace_msg_1 call t stac; (Program.Tac stac', a'))
3.432 end
3.433 | (Program.Expr lexpr, a') =>
3.434 - let val lexpr' =
3.435 - Rewrite.eval_prog_expr (Proof_Context.theory_of ctxt) srls
3.436 + let
3.437 + val lexpr' = Rewrite.eval_prog_expr (Proof_Context.theory_of ctxt) srls
3.438 (subst_atomic (Env.update_opt E (a, v)) lexpr)
3.439 in
3.440 (trace_msg_2 call t lexpr'; (Program.Expr lexpr', a'))
4.1 --- a/src/Tools/isac/Interpret/lucas-interpreter.sml Wed Apr 01 14:14:46 2020 +0200
4.2 +++ b/src/Tools/isac/Interpret/lucas-interpreter.sml Wed Apr 01 18:54:03 2020 +0200
4.3 @@ -189,10 +189,9 @@
4.4 check_tac cc ist (prog_tac, form_arg)
4.5
4.6 fun go_scan_up (pcc as (sc, _)) (ist as {path, act_arg, found_accept, ...}) =
4.7 - if path = [R] (*root of the program body*)
4.8 - then
4.9 - if found_accept
4.10 - then Term_Val act_arg
4.11 + if path = [R] (*root of the program body*) then
4.12 + if found_accept then
4.13 + Term_Val act_arg
4.14 else raise ERROR "LItool.find_next_step without result"
4.15 else scan_up pcc (ist |> path_up) (go_up path sc)
4.16 (* scan is strictly to R, because at L there was an \<open>expr_val\<close> *)
4.17 @@ -265,8 +264,8 @@
4.18
4.19 (* scan program until an applicable tactic is found *)
4.20 fun scan_to_tactic (prog, cc) (Pstate (ist as {path, ...})) =
4.21 - if path = []
4.22 - then scan_dn cc (trans_scan_dn ist) (Program.body_of prog)
4.23 + if path = [] then
4.24 + scan_dn cc (trans_scan_dn ist) (Program.body_of prog)
4.25 else go_scan_up (prog, cc) (trans_scan_up ist)
4.26 | scan_to_tactic _ _ = raise ERROR "scan_to_tactic: uncovered pattern";
4.27
4.28 @@ -405,8 +404,8 @@
4.29 check_tac1 cct ist (prog_tac, form_arg)
4.30
4.31 fun go_scan_up1 (pcct as (prog, _)) (ist as {path, act_arg, ...}) =
4.32 - if 1 < length path
4.33 - then scan_up1 pcct (ist |> path_up) (at_location (path_up' path) prog)
4.34 + if 1 < length path then
4.35 + scan_up1 pcct (ist |> path_up) (at_location (path_up' path) prog)
4.36 else Term_Val1 act_arg
4.37 (* scan is strictly to R, because at L there was a expr_val *)
4.38 and scan_up1 pcct ist (Const ("Tactical.Try"(*1*), _) $ _ $ _) = go_scan_up1 pcct ist
4.39 @@ -487,8 +486,8 @@
4.40 fun locate_input_tactic (Rule.Prog prog) cstate istate ctxt tac =
4.41 (case scan_to_tactic1 (prog, (cstate, ctxt, tac)) istate of
4.42 Accept_Tac1 ((ist as {assoc, ...}), ctxt, tac') =>
4.43 - if assoc
4.44 - then Safe_Step (Pstate ist, ctxt, tac')
4.45 + if assoc then
4.46 + Safe_Step (Pstate ist, ctxt, tac')
4.47 else Unsafe_Step (Pstate ist, ctxt, tac')
4.48 | Reject_Tac1 _ => Not_Locatable (Tactic.string_of tac ^ " not locatable")
4.49 | err => raise ERROR ("not-found-in-program: NotLocatable from " ^ @{make_string} err))
4.50 @@ -500,106 +499,85 @@
4.51 datatype input_term_result = Found_Step of Calc.T | Not_Derivable
4.52
4.53 fun by_tactic (Tactic.Apply_Method' (mI, _, _, _)) (_, ctxt) (pt, pos as (p, _)) =
4.54 - let
4.55 - val (itms, (*l..*)oris, probl(*..l*)) = case get_obj I pt p of
4.56 - PblObj {meth = itms, origin = (oris, _, _), probl, ...} => (itms, oris, probl)
4.57 - | _ => error "LI.by_tactic Apply_Method': uncovered case get_obj"
4.58 - val {ppc, ...} = Specify.get_met mI;
4.59 - val itms = if itms <> [] then itms else Chead.complete_metitms oris probl [] ppc
4.60 - val itms = Specify.hack_until_review_Specify_1 mI itms
4.61 - val srls = LItool.get_simplifier (pt, pos)
4.62 - val (is, env, ctxt, prog) = case LItool.init_pstate srls ctxt itms mI of
4.63 - (is as Pstate {env, ...}, ctxt, scr) => (is, env, ctxt, scr)
4.64 - | _ => error "LI.by_tactic Apply_Method': uncovered case init_pstate"
4.65 - val ini = LItool.implicit_take (Celem.assoc_thy (get_obj g_domID pt p)) prog env;
4.66 - val pos = start_new_level pos
4.67 - in
4.68 - case ini of
4.69 - SOME t =>
4.70 - let (* implicit Take *)
4.71 - val show_add = Tactic.Apply_Method' (mI, SOME t, is, ctxt);
4.72 - val (pos, c, _, pt) = Generate.generate1 show_add (is, ctxt) (pt, pos)
4.73 - in
4.74 - ("ok", ([(Tactic.Apply_Method mI, show_add, (pos, (is, ctxt)))], c, (pt, pos)))
4.75 - end
4.76 - | NONE =>
4.77 - let
4.78 - val (tac', ist', ctxt') =
4.79 - case find_next_step prog (pt, (lev_dn p, Res)) is ctxt of
4.80 - Next_Step (ist, ctxt, tac) => (tac, ist, ctxt)
4.81 - | _ => raise ERROR ("LI.by_tactic..Apply_Method find_next_step \<rightarrow> " ^ strs2str' mI)
4.82 - in
4.83 - case tac' of
4.84 - Tactic.Take' t =>
4.85 - let (* explicit Take *)
4.86 - val show_add = Tactic.Apply_Method' (mI, SOME t, ist', ctxt');
4.87 - val (pos, c, _, pt) = Generate.generate1 show_add (ist', ctxt') (pt, pos)
4.88 - in
4.89 - ("ok", ([(Tactic.Apply_Method mI, show_add, (pos, (is, ctxt)))], c, (pt, pos)))
4.90 - end
4.91 - | add as Tactic.Subproblem' (_, _, headline, _, _, _) =>
4.92 - let (* Subproblem *)
4.93 - val show = Tactic.Apply_Method' (mI, SOME headline, ist', ctxt');
4.94 - val (pos, c, _, pt) = Generate.generate1 add (ist', ctxt') (pt, pos)
4.95 - in
4.96 - ("ok", ([(Tactic.Apply_Method mI, show, (pos, (ist', ctxt')))], c, (pt, pos)))
4.97 - end
4.98 - | tac =>
4.99 - raise ERROR ("LI.by_tactic..Apply_Method' does NOT expect " ^ Tactic.string_of tac)
4.100 - end
4.101 - end
4.102 -(*NEW* ) ------vvv: prog_res ( *NEW*)
4.103 + let
4.104 + val (itms, (*l..*)oris, probl(*..l*)) = case get_obj I pt p of
4.105 + PblObj {meth = itms, origin = (oris, _, _), probl, ...} => (itms, oris, probl)
4.106 + | _ => error "LI.by_tactic Apply_Method': uncovered case get_obj"
4.107 + val {ppc, ...} = Specify.get_met mI;
4.108 + val itms = if itms <> [] then itms else Chead.complete_metitms oris probl [] ppc
4.109 + val itms = Specify.hack_until_review_Specify_1 mI itms
4.110 + val srls = LItool.get_simplifier (pt, pos)
4.111 + val (is, env, ctxt, prog) = case LItool.init_pstate srls ctxt itms mI of
4.112 + (is as Pstate {env, ...}, ctxt, scr) => (is, env, ctxt, scr)
4.113 + | _ => error "LI.by_tactic Apply_Method': uncovered case init_pstate"
4.114 + val ini = LItool.implicit_take prog env;
4.115 + val pos = start_new_level pos
4.116 + in
4.117 + case ini of
4.118 + SOME t =>
4.119 + let (* implicit Take *)
4.120 + val show_add = Tactic.Apply_Method' (mI, SOME t, is, ctxt);
4.121 + val (pos, c, _, pt) = Generate.generate1 show_add (is, ctxt) (pt, pos)
4.122 + in
4.123 + ("ok", ([(Tactic.Apply_Method mI, show_add, (pos, (is, ctxt)))], c, (pt, pos)))
4.124 + end
4.125 + | NONE =>
4.126 + let
4.127 + val (tac', ist', ctxt') =
4.128 + case find_next_step prog (pt, (lev_dn p, Res)) is ctxt of
4.129 + Next_Step (ist, ctxt, tac) => (tac, ist, ctxt)
4.130 + | _ => raise ERROR ("LI.by_tactic..Apply_Method find_next_step \<rightarrow> " ^ strs2str' mI)
4.131 + in
4.132 + case tac' of
4.133 + Tactic.Take' t =>
4.134 + let (* explicit Take *)
4.135 + val show_add = Tactic.Apply_Method' (mI, SOME t, ist', ctxt');
4.136 + val (pos, c, _, pt) = Generate.generate1 show_add (ist', ctxt') (pt, pos)
4.137 + in
4.138 + ("ok", ([(Tactic.Apply_Method mI, show_add, (pos, (is, ctxt)))], c, (pt, pos)))
4.139 + end
4.140 + | add as Tactic.Subproblem' (_, _, headline, _, _, _) =>
4.141 + let (* Subproblem *)
4.142 + val show = Tactic.Apply_Method' (mI, SOME headline, ist', ctxt');
4.143 + val (pos, c, _, pt) = Generate.generate1 add (ist', ctxt') (pt, pos)
4.144 + in
4.145 + ("ok", ([(Tactic.Apply_Method mI, show, (pos, (ist', ctxt')))], c, (pt, pos)))
4.146 + end
4.147 + | tac =>
4.148 + raise ERROR ("LI.by_tactic..Apply_Method' does NOT expect " ^ Tactic.string_of tac)
4.149 + end
4.150 + end
4.151 | by_tactic (Tactic.Check_Postcond' (pI, _)) (sub_ist, sub_ctxt) (pt, pos as (p, _)) =
4.152 -(*NEW* ) BETTER (curr_ist, curr_ctxt) -----^^^^^^^^^^^^^^^^^^^ ( *NEW*)
4.153 - let
4.154 - val parent_pos = par_pblobj pt p
4.155 - val {scr, ...} = Specify.get_met (get_obj g_metID pt parent_pos);
4.156 - val prog_res =
4.157 - case find_next_step scr (pt, pos) sub_ist sub_ctxt of
4.158 -(*OLD*) Next_Step (_, _, Tactic.Check_elementwise' (_, _, (prog_res, _))) => prog_res
4.159 - |(*OLD*) End_Program (_, Tactic.Check_Postcond' (_, prog_res)) => prog_res
4.160 -(*OLD*) | _ => raise ERROR ("Step_Solve.by_tactic Check_Postcond " ^ strs2str' pI)
4.161 -(*OLD* ) vvv--- handled by ctxt \<rightarrow> drop ( *OLD*)
4.162 -(*OLD*)val asm = (*?!? Rfun,Rrls rm case*)(case get_obj g_tac pt p of
4.163 -(*OLD*) Tactic.Check_elementwise _ => (snd o (get_obj g_result pt)) p
4.164 -(*OLD*) | _ => Ctree.get_assumptions pt pos)
4.165 -(*OLD* )val tac = Tactic.Check_Postcond' (pI, (prog_res, asm))
4.166 -( *OLD*)
4.167 - in
4.168 - if parent_pos = []
4.169 - then
4.170 - let
4.171 -(*NEW*) val tac = Tactic.Check_Postcond' (pI, prog_res)
4.172 -(*NEW*)
4.173 - val is = Pstate (sub_ist |> the_pstate |> set_act prog_res |> set_found)
4.174 - val ((p, p_), ps, _, pt) = Generate.generate1 tac (is, sub_ctxt) (pt, (parent_pos, Res))
4.175 - in
4.176 - ("ok", ([(Tactic.Check_Postcond pI, tac, ((parent_pos, Res), (is, sub_ctxt)))], ps, (pt, (p, p_))))
4.177 - end
4.178 - else
4.179 - let (*resume program of parent PblObj, transfer result of Subproblem-program*)
4.180 -(*OLD* ) val tac = Tactic.Check_Postcond' (pI, (prog_res, asm))
4.181 -(*OLD*) val (ist_parent, ctxt_parent) = case get_loc pt (parent_pos, Frm) of
4.182 -(*OLD*) (Pstate i, c) => (i, c)
4.183 -(*OLD*) | _ => error "LI.by_tactic Check_Postcond': uncovered case get_loc"
4.184 -(*OLD*) val (ttttt, ctxt') = ContextC.subpbl_to_caller sub_ctxt prog_res ctxt_parent
4.185 -(*OLD*) val is' = Pstate (ist_parent |> set_act prog_res |> set_found)
4.186 -(*OLD*) val ((p, p_), ps, _, pt) = Generate.generate1 tac (is', ctxt') (pt, (parent_pos, Res))
4.187 -(*OLD*) in
4.188 -(*OLD*) ("ok", ([(Tactic.Check_Postcond pI, tac, ((parent_pos, Res), (is', ctxt')))], ps, (pt, (p, p_))))
4.189 -(*OLD*) end
4.190 -( *NEW*)
4.191 -(*NEW*) val (ist_parent, ctxt_parent) = case get_loc pt (parent_pos, Frm) of
4.192 -(*NEW*) (Pstate i, c) => (i, c)
4.193 -(*NEW*) | _ => error "LI.by_tactic Check_Postcond': uncovered case get_loc"
4.194 -(*NEW*) val (prog_res', ctxt') = ContextC.subpbl_to_caller sub_ctxt prog_res ctxt_parent
4.195 -(*NEW*) val tac = Tactic.Check_Postcond' (pI, prog_res')
4.196 -(*NEW*) val ist' = Pstate (ist_parent |> set_act prog_res |> set_found)
4.197 -(*NEW*) val ((p, p_), ps, _, pt) = Generate.generate1 tac (ist', ctxt') (pt, (parent_pos, Res))
4.198 -(*NEW*) in
4.199 -(*NEW*) ("ok", ([(Tactic.input_from_T tac, tac, ((parent_pos, Res), (ist', ctxt')))], ps, (pt, (p, p_))))
4.200 -(*NEW*) end
4.201 - end
4.202 + let
4.203 + val parent_pos = par_pblobj pt p
4.204 + val {scr, ...} = Specify.get_met (get_obj g_metID pt parent_pos);
4.205 + val prog_res =
4.206 + case find_next_step scr (pt, pos) sub_ist sub_ctxt of
4.207 + (*OLD*) Next_Step (_, _, Tactic.Check_elementwise' (_, _, (prog_res, _))) => prog_res
4.208 + |(*OLD*) End_Program (_, Tactic.Check_Postcond' (_, prog_res)) => prog_res
4.209 + | _ => raise ERROR ("Step_Solve.by_tactic Check_Postcond " ^ strs2str' pI)
4.210 + in
4.211 + if parent_pos = [] then
4.212 + let
4.213 + val tac = Tactic.Check_Postcond' (pI, prog_res)
4.214 + val is = Pstate (sub_ist |> the_pstate |> set_act prog_res |> set_found)
4.215 + val ((p, p_), ps, _, pt) = Generate.generate1 tac (is, sub_ctxt) (pt, (parent_pos, Res))
4.216 + in
4.217 + ("ok", ([(Tactic.Check_Postcond pI, tac, ((parent_pos, Res), (is, sub_ctxt)))], ps, (pt, (p, p_))))
4.218 + end
4.219 + else
4.220 + let (*resume program of parent PblObj, transfer result of Subproblem-program*)
4.221 + val (ist_parent, ctxt_parent) = case get_loc pt (parent_pos, Frm) of
4.222 + (Pstate i, c) => (i, c)
4.223 + | _ => error "LI.by_tactic Check_Postcond': uncovered case get_loc"
4.224 + val (prog_res', ctxt') = ContextC.subpbl_to_caller sub_ctxt prog_res ctxt_parent
4.225 + val tac = Tactic.Check_Postcond' (pI, prog_res')
4.226 + val ist' = Pstate (ist_parent |> set_act prog_res |> set_found)
4.227 + val ((p, p_), ps, _, pt) = Generate.generate1 tac (ist', ctxt') (pt, (parent_pos, Res))
4.228 + in
4.229 + ("ok", ([(Tactic.input_from_T tac, tac, ((parent_pos, Res), (ist', ctxt')))], ps, (pt, (p, p_))))
4.230 + end
4.231 + end
4.232 | by_tactic (Tactic.End_Proof'') _ ptp = ("end-of-calculation", ([], [], ptp))
4.233 | by_tactic tac_ ic (pt, pos) =
4.234 let
4.235 @@ -610,8 +588,8 @@
4.236 end
4.237 (*find_next_step from program, by_tactic will update Ctree*)
4.238 and do_next (ptp as (pt, pos as (p, p_))) =
4.239 - if Celem.e_metID = get_obj g_metID pt (par_pblobj pt p)
4.240 - then ("helpless", ([], [], (pt, (p, p_))))
4.241 + if Celem.e_metID = get_obj g_metID pt (par_pblobj pt p) then
4.242 + ("helpless", ([], [], (pt, (p, p_))))
4.243 else
4.244 let
4.245 val thy' = get_obj g_domID pt (par_pblobj pt p);
4.246 @@ -639,13 +617,9 @@
4.247 CAUTION: tacis in returned calcstate' do NOT construct resulting ptp --
4.248 all_modspec etc. has to be inserted at Subproblem'
4.249 *)
4.250 -fun compare_step (tacis, c, ptp as (pt, pos as (p, p_))) ifo =
4.251 +fun compare_step (tacis, c, ptp as (pt, pos as (p, _))) ifo =
4.252 let
4.253 - val fo =
4.254 - case p_ of
4.255 - Pos.Frm => Ctree.get_obj Ctree.g_form pt p
4.256 - | Pos.Res => (fst o (Ctree.get_obj Ctree.g_result pt)) p
4.257 - | _ => Rule.e_term (*on PblObj is fo <> ifo*);
4.258 + val fo = Calc.get_current_formula ptp
4.259 val {nrls, ...} = Specify.get_met (Ctree.get_obj Ctree.g_metID pt (Ctree.par_pblobj pt p))
4.260 val {rew_ord, erls, rules, ...} = Rule.rep_rls nrls
4.261 val (found, der) = Error_Pattern.concat_deriv rew_ord erls rules fo ifo; (*<---------------*)
4.262 @@ -675,22 +649,14 @@
4.263 in compare_step (tacis, c @ c' @ c'', ptp) ifo end
4.264 end
4.265
4.266 -(*
4.267 - handle a user-input formula, which may be a CAS-command, too.
4.268 - * CAS-command: create a calchead, and do 1 step
4.269 - * formula, which is no CAS-command:
4.270 - compare iform with calc-tree.form at pos by equ_nrls and all subsequent pos;
4.271 - collect all the Prog_Tac applied by the way; ...???TODO?
4.272 - If "no derivation found" then Error_Pattern.check_for.
4.273 - ALTERNATIVE: Error_Pattern.check_for _within_ compare_step: seems too expensive
4.274 -*)
4.275 +(* Locate a step in a program, which has been determined by input of a term *)
4.276 fun locate_input_term (pt, pos) tm =
4.277 let
4.278 val pos_pred = Pos.lev_back' pos (*f_pred ---"step pos cs"---> f_succ in appendFormula*)
4.279 val _(*f_pred*) = Ctree.get_curr_formula (pt, pos_pred)
4.280 in
4.281 case compare_step ([], [], (pt, pos_pred)) tm of
4.282 - ("no derivation found", _) => Not_Derivable
4.283 + ("no derivation found", _) => Not_Derivable
4.284 | ("ok", (_, _, cstate)) =>
4.285 Found_Step cstate
4.286 | _ => raise ERROR "compare_step: uncovered case"
5.1 --- a/src/Tools/isac/Interpret/rewtools.sml Wed Apr 01 14:14:46 2020 +0200
5.2 +++ b/src/Tools/isac/Interpret/rewtools.sml Wed Apr 01 18:54:03 2020 +0200
5.3 @@ -1,6 +1,8 @@
5.4 -(* tools for rewriting, reverse rewriting, context to thy concerning rewriting
5.5 +(*
5.6 authors: Walther Neuper 2002, 2006
5.7 (c) due to copyright terms
5.8 +
5.9 +tools for rewriting, reverse rewriting, context to thy concerning rewriting
5.10 *)
5.11
5.12 signature REWRITE_TOOLS =
5.13 @@ -56,9 +58,10 @@
5.14 val deri2str : (Rule.rule * (term * term list)) list -> string
5.15 val sym_trm : term -> term
5.16 end
5.17 -
5.18 +(**)
5.19 structure Rtools(**): REWRITE_TOOLS(**) =
5.20 struct
5.21 +(**)
5.22
5.23 (*** reverse rewriting ***)
5.24 (*. a '_deriv'ation is constructed during 'reverse rewring' by an Rrls *
5.25 @@ -79,12 +82,12 @@
5.26 * (4) FIXME find criteria on when _not_ to step until End_Proof' *
5.27 * (5) FIXME
5.28 .*)
5.29 -type deriv = (* derivation for insertin one level of nodes into the calctree *)
5.30 - ( term * (* where the rule is applied to *)
5.31 - Rule.rule * (* rule to be applied *)
5.32 - ( term * (* resulting from rule application *)
5.33 - term list)) (* assumptions resulting from rule application *)
5.34 - list (* *)
5.35 +type deriv = (* derivation for insertin one level of nodes into the Ctree *)
5.36 + ( term * (* where the rule is applied to *)
5.37 + Rule.rule * (* rule to be applied *)
5.38 + ( term * (* resulting from rule application *)
5.39 + term list)) (* assumptions resulting from rule application *)
5.40 + list
5.41
5.42 fun trta2str (t, r, (t', a)) =
5.43 "\n(" ^ Rule.term2str t ^ ", " ^ Rule.rule2str' r ^ ", (" ^ Rule.term2str t' ^ ", " ^ Rule.terms2str a ^ "))"
5.44 @@ -95,12 +98,7 @@
5.45 fun rtas2str rtas = (strs2str o (map rta2str)) rtas
5.46 val deri2str = rtas2str
5.47
5.48 -(* A1==>...==> An ==> (Lhs = Rhs) goes to A1 ==>...==> An ==> (Rhs = Lhs)
5.49 - WN120320: reconsider the desing including the java front-end with html representation;
5.50 - see tests
5.51 - --- old compute rlsthmsNOTisac by eq_thmID ---
5.52 - --- compute val rlsthmsNOTisac ---
5.53 -*)
5.54 +(* A1==>...==> An ==> (Lhs = Rhs) goes to A1 ==>...==> An ==> (Rhs = Lhs) *)
5.55 fun sym_thm thm =
5.56 let
5.57 val (deriv,
6.1 --- a/src/Tools/isac/Interpret/step-solve.sml Wed Apr 01 14:14:46 2020 +0200
6.2 +++ b/src/Tools/isac/Interpret/step-solve.sml Wed Apr 01 18:54:03 2020 +0200
6.3 @@ -82,6 +82,13 @@
6.4
6.5 val do_next = LI.do_next
6.6
6.7 +
6.8 +(*
6.9 + Locate a step in a program, which has been determined by input of a term.
6.10 + Special case: if the term is a CAS-command, then create a calchead, and do 1 step.
6.11 + If "no derivation found" then Error_Pattern.check_for.
6.12 + (Error_Pattern.check_for *within* compare_step seems too expensive)
6.13 +*)
6.14 (*fun by_term (next_cs as (_, _, (pt, pos as (p, _))): Chead.calcstate') istr =*)
6.15 fun by_term (pt, pos as (p, _)) istr =
6.16 case TermC.parse (Celem.assoc_thy "Isac_Knowledge") istr of
7.1 --- a/src/Tools/isac/Knowledge/DiffApp.thy Wed Apr 01 14:14:46 2020 +0200
7.2 +++ b/src/Tools/isac/Knowledge/DiffApp.thy Wed Apr 01 18:54:03 2020 +0200
7.3 @@ -23,11 +23,11 @@
7.4 found to be reconsidered:
7.5 - descriptions (Descript.thy)
7.6 - penv: really need term list; or just rerun the whole example with num/var
7.7 -- mk_arg, itms2args ... env in script different from penv ?
7.8 +- mk_arg, arguments_from_model ... env in script different from penv ?
7.9 - L = SubProblem eq ... show some vars on the worksheet ? (other means for
7.10 referencing are labels (no on worksheet))
7.11
7.12 -WN.6.5.03 quick-and-dirty: mk_arg, itms2args just make most convenient env
7.13 +WN.6.5.03 quick-and-dirty: mk_arg, arguments_from_model just make most convenient env
7.14 from penv as is.
7.15 \<close>
7.16
8.1 --- a/src/Tools/isac/MathEngBasic/calculation.sml Wed Apr 01 14:14:46 2020 +0200
8.2 +++ b/src/Tools/isac/MathEngBasic/calculation.sml Wed Apr 01 18:54:03 2020 +0200
8.3 @@ -6,6 +6,7 @@
8.4 signature CALCULATION =
8.5 sig
8.6 type T
8.7 + val get_current_formula: T -> term
8.8
8.9 end
8.10
8.11 @@ -15,5 +16,11 @@
8.12 (**)
8.13 type T = Ctree.state
8.14
8.15 +fun get_current_formula (pt, (p, p_)) =
8.16 + case p_ of
8.17 + Pos.Frm => Ctree.get_obj Ctree.g_form pt p
8.18 + | Pos.Res => (fst o (Ctree.get_obj Ctree.g_result pt)) p
8.19 + | _ => Rule.e_term (*on PblObj is fo <> ifo*);
8.20 +
8.21 (**)end(**)
8.22
9.1 --- a/src/Tools/isac/MathEngBasic/tactic.sml Wed Apr 01 14:14:46 2020 +0200
9.2 +++ b/src/Tools/isac/MathEngBasic/tactic.sml Wed Apr 01 18:54:03 2020 +0200
9.3 @@ -26,7 +26,7 @@
9.4 | Check_elementwise' of term * Rule.cterm' * Selem.result
9.5 | Del_Find' of Rule.cterm' | Del_Given' of Rule.cterm' | Del_Relation' of Rule.cterm'
9.6
9.7 - | Derive' of Rule.rls
9.8 + | Derive' of Rule.rls
9.9 | Detail_Set' of Rule.theory' * bool * Rule.rls * term * Selem.result
9.10 | Detail_Set_Inst' of Rule.theory' * bool * Rule.subst * Rule.rls * term * Selem.result
9.11 | End_Detail' of Selem.result
10.1 --- a/src/Tools/isac/ProgLang/Prog_Tac.thy Wed Apr 01 14:14:46 2020 +0200
10.2 +++ b/src/Tools/isac/ProgLang/Prog_Tac.thy Wed Apr 01 18:54:03 2020 +0200
10.3 @@ -58,7 +58,7 @@
10.4 signature PROGAM_TACTIC =
10.5 sig
10.6 val dest_spec : term -> Celem.spec
10.7 - val get_first : 'a -> term -> term option (*TODO rename get_first*)
10.8 + val get_first_argument : term -> term option (*TODO rename get_first_argument*)
10.9 val eval_leaf: Env.T -> term option -> term -> term -> Program.leaf * term option
10.10 val is: term -> bool
10.11 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
10.12 @@ -80,47 +80,47 @@
10.13 | dest_spec t = raise TERM ("dest_spec: called with ", [t])
10.14
10.15 (* get argument of first Prog_Tac in a progam for implicit_take *)
10.16 -fun get_first thy (_ $ body) =
10.17 +fun get_first_argument (_ $ body) =
10.18 let
10.19 (* entries occur twice, for form curried by #> or non-curried *)
10.20 - fun get_t y (Const ("Tactical.Chain",_) $ e1 $ e2) a =
10.21 - (case get_t y e1 a of NONE => get_t y e2 a | la => la)
10.22 - | get_t y (Const ("Tactical.Chain",_) $ e1 $ e2 $ a) _ =
10.23 - (case get_t y e1 a of NONE => get_t y e2 a | la => la)
10.24 - | get_t y (Const ("Tactical.Try",_) $ e) a = get_t y e a
10.25 - | get_t y (Const ("Tactical.Try",_) $ e $ a) _ = get_t y e a
10.26 - | get_t y (Const ("Tactical.Repeat",_) $ e) a = get_t y e a
10.27 - | get_t y (Const ("Tactical.Repeat",_) $ e $ a) _ = get_t y e a
10.28 - | get_t y (Const ("Tactical.Or",_) $e1 $ e2) a =
10.29 - (case get_t y e1 a of NONE => get_t y e2 a | la => la)
10.30 - | get_t y (Const ("Tactical.Or",_) $e1 $ e2 $ a) _ =
10.31 - (case get_t y e1 a of NONE => get_t y e2 a | la => la)
10.32 - | get_t y (Const ("Tactical.While",_) $ _ $ e) a = get_t y e a
10.33 - | get_t y (Const ("Tactical.While",_) $ _ $ e $ a) _ = get_t y e a
10.34 - | get_t y (Const ("Tactical.Letpar",_) $ e1 $ Abs (_, _, e2)) a =
10.35 - (case get_t y e1 a of NONE => get_t y e2 a | la => la)
10.36 - | get_t y (Const ("HOL.Let",_) $ e1 $ Abs (_, _, _)) a =
10.37 - get_t y e1 a (* don't go deeper without evaluation *)
10.38 - | get_t _ (Const ("If", _) $ _ $ _ $ _) _ = NONE
10.39 + fun get_t (Const ("Tactical.Chain",_) $ e1 $ e2) a =
10.40 + (case get_t e1 a of NONE => get_t e2 a | la => la)
10.41 + | get_t (Const ("Tactical.Chain",_) $ e1 $ e2 $ a) _ =
10.42 + (case get_t e1 a of NONE => get_t e2 a | la => la)
10.43 + | get_t (Const ("Tactical.Try",_) $ e) a = get_t e a
10.44 + | get_t (Const ("Tactical.Try",_) $ e $ a) _ = get_t e a
10.45 + | get_t (Const ("Tactical.Repeat",_) $ e) a = get_t e a
10.46 + | get_t (Const ("Tactical.Repeat",_) $ e $ a) _ = get_t e a
10.47 + | get_t (Const ("Tactical.Or",_) $e1 $ e2) a =
10.48 + (case get_t e1 a of NONE => get_t e2 a | la => la)
10.49 + | get_t (Const ("Tactical.Or",_) $e1 $ e2 $ a) _ =
10.50 + (case get_t e1 a of NONE => get_t e2 a | la => la)
10.51 + | get_t (Const ("Tactical.While",_) $ _ $ e) a = get_t e a
10.52 + | get_t (Const ("Tactical.While",_) $ _ $ e $ a) _ = get_t e a
10.53 + | get_t (Const ("Tactical.Letpar",_) $ e1 $ Abs (_, _, e2)) a =
10.54 + (case get_t e1 a of NONE => get_t e2 a | la => la)
10.55 + | get_t (Const ("HOL.Let",_) $ e1 $ Abs (_, _, _)) a =
10.56 + get_t e1 a (* don't go deeper without evaluation *)
10.57 + | get_t (Const ("If", _) $ _ $ _ $ _) _ = NONE
10.58
10.59 - | get_t _ (Const ("Prog_Tac.Rewrite",_) $ _ $ a) _ = SOME a
10.60 - | get_t _ (Const ("Prog_Tac.Rewrite",_) $ _ ) a = SOME a
10.61 - | get_t _ (Const ("Prog_Tac.Rewrite'_Inst",_) $ _ $ _ $ a) _ = SOME a
10.62 - | get_t _ (Const ("Prog_Tac.Rewrite'_Inst",_) $ _ $ _ ) a = SOME a
10.63 - | get_t _ (Const ("Prog_Tac.Rewrite'_Set",_) $ _ $ a) _ = SOME a
10.64 - | get_t _ (Const ("Prog_Tac.Rewrite'_Set",_) $ _ ) a = SOME a
10.65 - | get_t _ (Const ("Prog_Tac.Rewrite'_Set'_Inst",_) $ _ $ _ $a)_ =SOME a
10.66 - | get_t _ (Const ("Prog_Tac.Rewrite'_Set'_Inst",_) $ _ $ _ ) a =SOME a
10.67 - | get_t _ (Const ("Prog_Tac.Calculate",_) $ _ $ a) _ = SOME a
10.68 - | get_t _ (Const ("Prog_Tac.Calculate",_) $ _ ) a = SOME a
10.69 - | get_t _ (Const ("Prog_Tac.Substitute",_) $ _ $ a) _ = SOME a
10.70 - | get_t _ (Const ("Prog_Tac.Substitute",_) $ _ ) a = SOME a
10.71 + | get_t (Const ("Prog_Tac.Rewrite",_) $ _ $ a) _ = SOME a
10.72 + | get_t (Const ("Prog_Tac.Rewrite",_) $ _ ) a = SOME a
10.73 + | get_t (Const ("Prog_Tac.Rewrite'_Inst",_) $ _ $ _ $ a) _ = SOME a
10.74 + | get_t (Const ("Prog_Tac.Rewrite'_Inst",_) $ _ $ _ ) a = SOME a
10.75 + | get_t (Const ("Prog_Tac.Rewrite'_Set",_) $ _ $ a) _ = SOME a
10.76 + | get_t (Const ("Prog_Tac.Rewrite'_Set",_) $ _ ) a = SOME a
10.77 + | get_t (Const ("Prog_Tac.Rewrite'_Set'_Inst",_) $ _ $ _ $a)_ =SOME a
10.78 + | get_t (Const ("Prog_Tac.Rewrite'_Set'_Inst",_) $ _ $ _ ) a =SOME a
10.79 + | get_t (Const ("Prog_Tac.Calculate",_) $ _ $ a) _ = SOME a
10.80 + | get_t (Const ("Prog_Tac.Calculate",_) $ _ ) a = SOME a
10.81 + | get_t (Const ("Prog_Tac.Substitute",_) $ _ $ a) _ = SOME a
10.82 + | get_t (Const ("Prog_Tac.Substitute",_) $ _ ) a = SOME a
10.83
10.84 - | get_t _ (Const ("Prog_Tac.SubProblem",_) $ _ $ _) _ = NONE
10.85 + | get_t (Const ("Prog_Tac.SubProblem",_) $ _ $ _) _ = NONE
10.86
10.87 - | get_t _ _ _ = ((*tracing ("### get_t yac: list-expr "^(term2str x));*) NONE)
10.88 - in get_t thy body Rule.e_term end
10.89 - | get_first _ t = error ("get_first: no fun-def. for " ^ Rule.term2str t);
10.90 + | get_t _ _ = ((*tracing ("### get_t yac: list-expr "^(term2str x));*) NONE)
10.91 + in get_t body Rule.e_term end
10.92 + | get_first_argument t = error ("get_first_argument: no fun-def. for " ^ Rule.term2str t);
10.93
10.94 (* substitute the Istate.T's environment to a leaf of the program
10.95 and attach the curried argument of a tactic, if any.
11.1 --- a/src/Tools/isac/TODO.thy Wed Apr 01 14:14:46 2020 +0200
11.2 +++ b/src/Tools/isac/TODO.thy Wed Apr 01 18:54:03 2020 +0200
11.3 @@ -54,12 +54,12 @@
11.4 \item xxx
11.5 \item xxx
11.6 \item clarify Tactic.Subproblem (domID, pblID) as term in Pstate {act_arg, ...}
11.7 - there it is Free ("Subproblem", "char list \<times> ..
11.8 - instead of Const (|???.Subproblem", "char list \<times> ..
11.9 - AND THE STRING REPRESENTATION IS STRANGE:
11.10 - Subproblem (''Test'',
11.11 - ??.\ <^const> String.char.Char ''LINEAR'' ''univariate'' ''equation''
11.12 - ''test'')
11.13 + there it is Free ("Subproblem", "char list \<times> ..
11.14 + instead of Const (|???.Subproblem", "char list \<times> ..
11.15 + AND THE STRING REPRESENTATION IS STRANGE:
11.16 + Subproblem (''Test'',
11.17 + ??.\ <^const> String.char.Char ''LINEAR'' ''univariate'' ''equation''
11.18 + ''test'')
11.19 ML \<open>
11.20 \<close> ML \<open>
11.21 term2str; (*defined by..*)
11.22 @@ -266,7 +266,7 @@
11.23 \item xxx
11.24 \end{itemize}
11.25 \item xxx
11.26 - \item Prog_Tac: fun get_first takes both Prog_Tac + Program --- wait for separate Tactical
11.27 + \item Prog_Tac: fun get_first_argument takes both Prog_Tac + Program --- wait for separate Tactical
11.28 then shift into common descendant
11.29 \item xxx
11.30 \end{itemize}
11.31 @@ -385,7 +385,6 @@
11.32 \item xxx
11.33 \item xxx
11.34 \item in locate_input_tactic .. ?scan_dn1?; Program.is_eval_expr .use Term.exists_Const
11.35 - \item locate_input_tactic: get_simplifier cstate (*TODO: shift to init_istate*)
11.36 \item push srls into pstate
11.37 \item lucas-intrpreter.locate_input_tactic: scan_to_tactic1 srls tac cstate (progr, Rule.e_rls)
11.38 ^^^^^^^^^^
11.39 @@ -570,7 +569,8 @@
11.40 section \<open>Questions to Isabelle experts\<close>
11.41 text \<open>
11.42 \begin{itemize}
11.43 -\item ad ERROR @unknown fact all_left in Test_Isac
11.44 +\item ad ERROR Undefined fact "all_left" in Test_Isac: error-pattern.sml
11.45 + Undefined fact: "xfoldr_Nil" inssort.sml
11.46 \item xxx
11.47 \item xxx
11.48 \item ?OK Test_Isac_Short with
12.1 --- a/test/Tools/isac/Interpret/li-tool.sml Wed Apr 01 14:14:46 2020 +0200
12.2 +++ b/test/Tools/isac/Interpret/li-tool.sml Wed Apr 01 18:54:03 2020 +0200
12.3 @@ -6,14 +6,14 @@
12.4 "table of contents -----------------------------------------------";
12.5 "-----------------------------------------------------------------";
12.6 "----------- fun specific_from_prog ----------------------------";
12.7 -"----------- fun implicit_take, fun get_first -------------------------";
12.8 +"----------- fun implicit_take, fun get_first_argument -------------------------";
12.9 "----------- fun from_prog ---------------------------------------";
12.10 "----------- fun specific_from_prog ----------------------------";
12.11 "----------- fun de_esc_underscore -------------------------------";
12.12 "----------- fun go ----------------------------------------------";
12.13 "----------- fun formal_args -------------------------------------";
12.14 "----------- fun dsc_valT ----------------------------------------";
12.15 -"----------- fun itms2args ---------------------------------------";
12.16 +"----------- fun arguments_from_model ---------------------------------------";
12.17 "----------- fun init_pstate -----------------------------------------------------------------";
12.18 "-----------------------------------------------------------------";
12.19 "-----------------------------------------------------------------";
12.20 @@ -88,9 +88,9 @@
12.21 autoCalculate 1 CompleteCalc; (* ONE ERROR *)
12.22 ==============================^^^^^^^^^^^^^*)
12.23
12.24 -"----------- fun implicit_take, fun get_first -------------------------";
12.25 -"----------- fun implicit_take, fun get_first -------------------------";
12.26 -"----------- fun implicit_take, fun get_first -------------------------";
12.27 +"----------- fun implicit_take, fun get_first_argument -------------------------";
12.28 +"----------- fun implicit_take, fun get_first_argument -------------------------";
12.29 +"----------- fun implicit_take, fun get_first_argument -------------------------";
12.30 val fmz = ["equality (x+1=(2::real))", "solveFor x", "solutions L"];
12.31 val (dI',pI',mI') = ("Test",["sqroot-test","univariate","equation","test"],
12.32 ["Test","squ-equ-test-subpbl1"]);
12.33 @@ -115,10 +115,10 @@
12.34 val thy = assoc_thy thy';
12.35 val srls = LItool.get_simplifier (pt, pos)
12.36 val (is as Pstate {env, ...}, ctxt, sc) = init_pstate srls ctxt itms mI;
12.37 -val ini = implicit_take thy sc env;
12.38 +val ini = implicit_take sc env;
12.39 "----- fun implicit_take, args:"; val (Prog sc) = sc;
12.40 -"----- fun get_first, args:"; val (y, h $ body) = (thy, sc);
12.41 -case get_first thy sc of SOME (Free ("e_e", _)) => ()
12.42 +"----- fun get_first_argument, args:"; val (y, h $ body) = (thy, sc);
12.43 +case get_first_argument sc of SOME (Free ("e_e", _)) => ()
12.44 | _ => error "script: Const (?, ?) in script (as term) changed";;
12.45
12.46 "----------- fun from_prog ---------------------------------------";
12.47 @@ -273,14 +273,14 @@
12.48 val T = "bool List.list => Tools.nam" : typ
12.49 > val dsc = dsc_valT t;
12.50 val dsc = "nam" : string*)
12.51 -"----------- fun itms2args ---------------------------------------";
12.52 -"----------- fun itms2args ---------------------------------------";
12.53 -"----------- fun itms2args ---------------------------------------";
12.54 +"----------- fun arguments_from_model ---------------------------------------";
12.55 +"----------- fun arguments_from_model ---------------------------------------";
12.56 +"----------- fun arguments_from_model ---------------------------------------";
12.57 (*
12.58 > val sc = ... Solve_root_equation ...
12.59 > val mI = ("Program","sqrt-equ-test");
12.60 > val PblObj{meth={ppc=itms,...},...} = get_obj I pt [];
12.61 -> val ts = itms2args thy mI itms;
12.62 +> val ts = arguments_from_model thy mI itms;
12.63 > map (term_to_string''' thy) ts;
12.64 ["sqrt (#9 + #4 * x) = sqrt x + sqrt (#5 + x)","x","#0"] : string list
12.65 *)
13.1 --- a/test/Tools/isac/Interpret/lucas-interpreter.sml Wed Apr 01 14:14:46 2020 +0200
13.2 +++ b/test/Tools/isac/Interpret/lucas-interpreter.sml Wed Apr 01 18:54:03 2020 +0200
13.3 @@ -54,7 +54,7 @@
13.4 (is as Istate.Pstate {env, ...}, ctxt, sc) => (is, env, ctxt, sc)
13.5 | _ => error "solve Apply_Method: uncovered case init_pstate";
13.6 (*+*)pstate2str (the_pstate is) = "([\"\n(f_f, x ^^^ 2 + 1)\",\"\n(v_v, x)\"], [], e_rls, NONE, \n??.empty, ORundef, false, true)";
13.7 - val ini = LItool.implicit_take thy sc env;
13.8 + val ini = LItool.implicit_take sc env;
13.9 val p = lev_dn p;
13.10
13.11 val NONE = (*case*) ini (*of*);
14.1 --- a/test/Tools/isac/Interpret/rewtools.sml Wed Apr 01 14:14:46 2020 +0200
14.2 +++ b/test/Tools/isac/Interpret/rewtools.sml Wed Apr 01 18:54:03 2020 +0200
14.3 @@ -350,16 +350,16 @@
14.4 "----------- fun is_contained_in ------------------------";
14.5 "----------- fun is_contained_in ------------------------";
14.6 val r1 = Thm ("real_diff_minus",num_str @{thm real_diff_minus});
14.7 -if contains_rule r1 Test_simplify then ()
14.8 -else error "rewtools.sml contains_rule Thm";
14.9 +if Rule.contains_rule r1 Test_simplify then ()
14.10 +else error "rewtools.sml Rule.contains_rule Thm";
14.11
14.12 val r1 = Num_Calc ("Groups.plus_class.plus", eval_binop "#add_");
14.13 -if contains_rule r1 Test_simplify then ()
14.14 -else error "rewtools.sml contains_rule Num_Calc";
14.15 +if Rule.contains_rule r1 Test_simplify then ()
14.16 +else error "rewtools.sml Rule.contains_rule Num_Calc";
14.17
14.18 val r1 = Num_Calc ("Groups.minus_class.minus", eval_binop "#add_");
14.19 -if not (contains_rule r1 Test_simplify) then ()
14.20 -else error "rewtools.sml contains_rule Num_Calc";
14.21 +if not (Rule.contains_rule r1 Test_simplify) then ()
14.22 +else error "rewtools.sml Rule.contains_rule Num_Calc";
14.23
14.24 "----------- build fun get_bdv_subst --------------------------------";
14.25 "----------- build fun get_bdv_subst --------------------------------";
15.1 --- a/test/Tools/isac/Knowledge/biegelinie-4.sml Wed Apr 01 14:14:46 2020 +0200
15.2 +++ b/test/Tools/isac/Knowledge/biegelinie-4.sml Wed Apr 01 18:54:03 2020 +0200
15.3 @@ -162,7 +162,7 @@
15.4 val (is, env, ctxt, sc) = case LItool.init_pstate srls ctxt itms mI of
15.5 (is as Istate.Pstate ist, ctxt, sc) => (is, get_env ist, ctxt, sc)
15.6 | _ => error "Step_Solve.by_tactic Apply_Method: uncovered case init_pstate"
15.7 - val ini = LItool.implicit_take thy sc env;
15.8 + val ini = LItool.implicit_take sc env;
15.9 val p = lev_dn p;
15.10 val NONE = (*case*) ini (*of*);
15.11 val (m', (is', ctxt'), _) = LI.find_next_step sc (pt, (p, Res)) is ctxt;
15.12 @@ -194,11 +194,11 @@
15.13 (*----------- 20 -----------*)
15.14 (*//------------------------------------------------vvv Specify_Method ["Biegelinien", "ausBelastung"]-\\*)
15.15 (*[1], Pbl*)(*ERROR val (p,_,f,nxt,_,pt) = me nxt''''' p''''' c pt'''''; (*nxt = Apply_Method ["Biegelinien", "ausBelastung"]*)
15.16 -ERROR itms2args: 'Biegelinie' not in itms*)
15.17 +ERROR arguments_from_model: 'Biegelinie' not in itms*)
15.18
15.19 (*SubProblem (_, [''vonBelastungZu'', ''Biegelinien''], _)
15.20 [REAL q, REAL v, REAL_REAL b, REAL_REAL id_abl]
15.21 - ^^^^^^^^^^^ ..ERROR itms2args: 'Biegelinie' not in itms*)
15.22 + ^^^^^^^^^^^ ..ERROR arguments_from_model: 'Biegelinie' not in itms*)
15.23 (*+*)val PblObj {meth, probl, spec = (thy, _ , metID), origin = (oris, _, _), ...} = get_obj I pt''''' (fst p''''');
15.24 (*+*)if oris2str oris =
15.25 (*+*) "[\n(1, [\"1\"], #Given,Streckenlast, [\"q_0\"]),\n(2, [\"1\"], #Given,FunktionsVariable, [\"x\"]),\n(3, [\"1\"], #Find,Funktionen, [\"funs'''\"])]"
16.1 --- a/test/Tools/isac/Knowledge/diffapp.sml Wed Apr 01 14:14:46 2020 +0200
16.2 +++ b/test/Tools/isac/Knowledge/diffapp.sml Wed Apr 01 18:54:03 2020 +0200
16.3 @@ -399,7 +399,7 @@
16.4 val mits = get_obj g_met pt [];writeln(itms2str_ ctxt mits);
16.5
16.6 (*=== inhibit exn 110722=============================================================
16.7 -itms2args thy ["DiffApp","max_by_calculus"] mits;
16.8 +arguments_from_model ["DiffApp","max_by_calculus"] mits;
16.9
16.10 val (p,_,f,nxt,_,pt) = me nxt p c pt;
16.11 === inhibit exn 110722=============================================================*)
17.1 --- a/test/Tools/isac/Minisubpbl/200-start-method.sml Wed Apr 01 14:14:46 2020 +0200
17.2 +++ b/test/Tools/isac/Minisubpbl/200-start-method.sml Wed Apr 01 18:54:03 2020 +0200
17.3 @@ -58,7 +58,7 @@
17.4 val ctxt = ctxt |> ContextC.insert_assumptions pres;
17.5 val (is'''' as Pstate {env = env'''',...}, _, sc'''') = init_pstate srls ctxt meth mI;
17.6 "~~~~~ fun init_pstate , args:"; val (srls, thy, itms, metID) = (srls, thy, meth, mI)
17.7 - val actuals = itms2args thy metID itms
17.8 + val actuals = arguments_from_model metID itms
17.9 val scr as Prog sc = (#scr o get_met) metID
17.10 val formals = formal_args sc
17.11 (*expects same sequence of (actual) args in itms and (formal) args in met*)
17.12 @@ -98,7 +98,7 @@
17.13 val ctxt = ctxt |> ContextC.insert_assumptions pres;
17.14
17.15 "~~~~~ continue Step_Solve.by_tactic";
17.16 -val ini = implicit_take thy sc'''' env'''';
17.17 +val ini = implicit_take sc'''' env'''';
17.18 val p = lev_dn p;
17.19 val SOME t = ini;
17.20 val (pos,c,_,pt) =
18.1 --- a/test/Tools/isac/Test_Isac.thy Wed Apr 01 14:14:46 2020 +0200
18.2 +++ b/test/Tools/isac/Test_Isac.thy Wed Apr 01 18:54:03 2020 +0200
18.3 @@ -90,7 +90,7 @@
18.4 open Kernel;
18.5 open Math_Engine;
18.6 open Test_Code; CalcTreeTEST;
18.7 - open LItool; itms2args;
18.8 + open LItool; arguments_from_model;
18.9 open Sub_Problem;
18.10 open Fetch_Tacs;
18.11 open Step
18.12 @@ -179,7 +179,6 @@
18.13 ML_file "ProgLang/tactical.sml"
18.14 ML_file "ProgLang/auto_prog.sml"
18.15 ML_file "ProgLang/rewrite.sml"
18.16 - ML_file "ProgLang/tools.sml"
18.17 (*---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------
18.18 ---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------*)
18.19
18.20 @@ -247,7 +246,6 @@
18.21
18.22 ML_file "Knowledge/delete.sml"
18.23 ML_file "Knowledge/descript.sml"
18.24 - ML_file "Knowledge/atools.sml"
18.25 ML_file "Knowledge/simplify.sml"
18.26 ML_file "Knowledge/poly.sml"
18.27 ML_file "Knowledge/gcd_poly_ml.sml"
19.1 --- a/test/Tools/isac/Test_Isac_Short.thy Wed Apr 01 14:14:46 2020 +0200
19.2 +++ b/test/Tools/isac/Test_Isac_Short.thy Wed Apr 01 18:54:03 2020 +0200
19.3 @@ -90,7 +90,7 @@
19.4 open Kernel;
19.5 open Math_Engine;
19.6 open Test_Code; CalcTreeTEST;
19.7 - open LItool; itms2args;
19.8 + open LItool; arguments_from_model;
19.9 open Sub_Problem;
19.10 open Fetch_Tacs;
19.11 open Step
19.12 @@ -179,7 +179,6 @@
19.13 ML_file "ProgLang/tactical.sml"
19.14 ML_file "ProgLang/auto_prog.sml"
19.15 ML_file "ProgLang/rewrite.sml"
19.16 - ML_file "ProgLang/tools.sml"
19.17 (*---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------
19.18 ---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------*)
19.19
19.20 @@ -247,7 +246,6 @@
19.21
19.22 ML_file "Knowledge/delete.sml"
19.23 ML_file "Knowledge/descript.sml"
19.24 - ML_file "Knowledge/atools.sml"
19.25 ML_file "Knowledge/simplify.sml"
19.26 ML_file "Knowledge/poly.sml"
19.27 ML_file "Knowledge/gcd_poly_ml.sml"
20.1 --- a/test/Tools/isac/Test_Some.thy Wed Apr 01 14:14:46 2020 +0200
20.2 +++ b/test/Tools/isac/Test_Some.thy Wed Apr 01 18:54:03 2020 +0200
20.3 @@ -10,7 +10,7 @@
20.4 open Kernel;
20.5 open Math_Engine;
20.6 open Test_Code; CalcTreeTEST;
20.7 - open LItool; itms2args;
20.8 + open LItool; arguments_from_model;
20.9 open Sub_Problem;
20.10 open Step
20.11 open Env;
21.1 --- a/test/Tools/isac/Test_Some_meld.thy Wed Apr 01 14:14:46 2020 +0200
21.2 +++ b/test/Tools/isac/Test_Some_meld.thy Wed Apr 01 18:54:03 2020 +0200
21.3 @@ -6,7 +6,7 @@
21.4 in case of errors here consider ~~/xtest-to-coding.sh *)
21.5 open Kernel;
21.6 open Math_Engine; CalcTreeTEST;
21.7 - open LItool.; itms2args;
21.8 + open LItool.; arguments_from_model;
21.9 open Env;
21.10 open Exec;
21.11 open LI; scan_dn;