1.1 --- a/src/Tools/isac/Interpret/istate.sml Mon May 04 11:13:16 2020 +0200
1.2 +++ b/src/Tools/isac/Interpret/istate.sml Mon May 04 12:38:16 2020 +0200
1.3 @@ -18,6 +18,8 @@
1.4 val istates2str: T option * T option -> string
1.5 val the_pstate: T -> pstate
1.6
1.7 + val init_detail: Tactic.input -> term -> Istate_Def.T
1.8 +
1.9 val get_act_env: pstate -> (term * Env.T)
1.10 val get_subst: pstate -> (Env.T * (term option * term))
1.11
1.12 @@ -60,6 +62,8 @@
1.13 struct
1.14 (**)
1.15
1.16 +(** types **)
1.17 +
1.18 datatype asap = datatype Istate_Def.asap
1.19 val asap2str = Istate_Def.asap2str
1.20
1.21 @@ -72,6 +76,9 @@
1.22 fun the_pstate (Pstate pst) = pst
1.23 | the_pstate _ = raise ERROR ("the_pstate called for RrlsStated")
1.24
1.25 +
1.26 +(** access functions **)
1.27 +
1.28 val string_of = Istate_Def.string_of
1.29 val string_of' = Istate_Def.string_of'
1.30 val istates2str = Istate_Def.istates2str
1.31 @@ -92,7 +99,6 @@
1.32 {env = env, path = path, eval = eval, form_arg = form_arg, act_arg = act_arg,
1.33 or = or, found_accept = found_accept, assoc = assoc}
1.34
1.35 -
1.36 fun path_down p {env, path, eval, form_arg, act_arg, or, found_accept, assoc} =
1.37 {env = env, path = path @ p, eval = eval, form_arg = form_arg, act_arg = act_arg,
1.38 or = or, found_accept = found_accept, assoc = assoc}
1.39 @@ -159,10 +165,31 @@
1.40 {env = Env.update env (form, act), path = path, eval = eval, form_arg = SOME form, act_arg = act,
1.41 or = or, found_accept = found_accept, assoc = assoc}
1.42
1.43 -(*
1.44 - {env = env, path = path, eval = eval, form_arg = form_arg, act_arg = act_arg,
1.45 - or = or, found_accept = found_accept, assoc = assoc}
1.46 -*)
1.47 +(* initialize istate for Detail_Set *)
1.48 +fun init_detail (Tactic.Rewrite_Set rls) t =
1.49 + let
1.50 + val thy = ThyC.get_theory "Isac_Knowledge"
1.51 + val args = Auto_Prog.gen thy t (assoc_rls rls) |> Program.formal_args
1.52 + in
1.53 + Istate_Def.Pstate (Istate_Def.e_pstate |> Istate_Def.set_env_true [(hd args, t)])
1.54 + end
1.55 + | init_detail (Tactic.Rewrite_Set_Inst (subs, rls)) t =
1.56 + let
1.57 + val thy = ThyC.get_theory "Isac_Knowledge"
1.58 + val rls' = assoc_rls rls
1.59 + val v = case Subst.T_from_input thy subs of
1.60 + (_, v) :: _ => v (*...we suppose the substitution of only ONE bound variable*)
1.61 + | _ => raise ERROR "init_detail: uncovered case"
1.62 + val prog = Auto_Prog.gen thy t rls'
1.63 + val args = Program.formal_args prog
1.64 + in
1.65 + Istate_Def.Pstate (Istate_Def.e_pstate |> Istate_Def.set_env_true (args ~~ [t, v]))
1.66 + end
1.67 + | init_detail tac _ = raise ERROR ("init_detail: uncovered definition for " ^ Tactic.input_to_string tac)
1.68 +
1.69 +(** initialisation **)
1.70 +
1.71 +
1.72
1.73 (**)end(**)
1.74
2.1 --- a/src/Tools/isac/Interpret/solve-step.sml Mon May 04 11:13:16 2020 +0200
2.2 +++ b/src/Tools/isac/Interpret/solve-step.sml Mon May 04 12:38:16 2020 +0200
2.3 @@ -9,16 +9,22 @@
2.4 sig
2.5 val check: Tactic.input -> Calc.T -> Applicable.T
2.6 val add: Tactic.T -> Istate_Def.T * Proof.context -> Calc.T -> Generate.test_out
2.7 +
2.8 val add_general: Tactic.T -> Istate_Def.T * Proof.context -> Calc.T -> Generate.test_out
2.9 val s_add_general: State_Steps.T ->
2.10 Ctree.ctree * Pos.pos' list * Pos.pos' -> Ctree.ctree * Pos.pos' list * Pos.pos'
2.11 val add_hard:
2.12 theory -> Tactic.T -> Pos.pos' -> Ctree.ctree -> Generate.test_out
2.13
2.14 + val get_ruleset: 'a -> Pos.pos -> Ctree.ctree ->
2.15 + string * ThyC.id * Rule_Def.rew_ord' * Rule_Def.rule_set * bool
2.16 + val get_eval: string -> Pos.pos ->Ctree.ctree ->
2.17 + string * ThyC.id * (string * Rule_Def.eval_fn)
2.18 +
2.19 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
2.20 (*NONE*)
2.21 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
2.22 - (*NONE*)
2.23 + val rew_info: Rule_Def.rule_set -> string * Rule_Def.rule_set * Rule_Def.calc list
2.24 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
2.25 end
2.26
2.27 @@ -27,6 +33,62 @@
2.28 struct
2.29 (**)
2.30
2.31 +(** get data from Calc.T **)
2.32 +
2.33 +(* the source is the parent node, either a problem or a Rule_Set (with inter_steps) *)
2.34 +fun rew_info (Rule_Def.Repeat {erls, rew_ord = (rew_ord', _), calc = ca, ...}) =
2.35 + (rew_ord', erls, ca)
2.36 + | rew_info (Rule_Set.Sequence {erls, rew_ord = (rew_ord', _), calc = ca, ...}) =
2.37 + (rew_ord', erls, ca)
2.38 + | rew_info (Rule_Set.Rrls {erls, rew_ord = (rew_ord', _), calc = ca, ...}) =
2.39 + (rew_ord', erls, ca)
2.40 + | rew_info rls = error ("rew_info called with '" ^ Rule_Set.id rls ^ "'");
2.41 +
2.42 +fun get_ruleset _ p pt =
2.43 + let
2.44 + val (pbl, p', rls') = Ctree.parent_node pt p
2.45 + in
2.46 + if pbl
2.47 + then
2.48 + let
2.49 + val thy' = Ctree.get_obj Ctree.g_domID pt p'
2.50 + val {rew_ord', erls, ...} = Specify.get_met (Ctree.get_obj Ctree.g_metID pt p')
2.51 + in ("OK", thy', rew_ord', erls, false) end
2.52 + else
2.53 + let
2.54 + val thy' = Ctree.get_obj Ctree.g_domID pt (Ctree.par_pblobj pt p)
2.55 + val (rew_ord', erls, _) = rew_info rls'
2.56 + in ("OK", thy', rew_ord', erls, false) end
2.57 + end;
2.58 +
2.59 +fun get_eval scrop p pt =
2.60 + let
2.61 + val (pbl, p', rls') = Ctree.parent_node pt p
2.62 + in
2.63 + if pbl
2.64 + then
2.65 + let
2.66 + val thy' = Ctree.get_obj Ctree.g_domID pt p'
2.67 + val {calc = scr_isa_fns, ...} = Specify.get_met (Ctree.get_obj Ctree.g_metID pt p')
2.68 + val opt = assoc (scr_isa_fns, scrop)
2.69 + in
2.70 + case opt of
2.71 + SOME isa_fn => ("OK", thy', isa_fn)
2.72 + | NONE => ("applicable_in Calculate: unknown '" ^ scrop ^ "'", "", ("", Eval_Def.e_evalfn))
2.73 + end
2.74 + else
2.75 + let
2.76 + val thy' = Ctree.get_obj Ctree.g_domID pt (Ctree.par_pblobj pt p);
2.77 + val (_, _,(*_,*)scr_isa_fns) = rew_info rls'(*rls*)
2.78 + in
2.79 + case assoc (scr_isa_fns, scrop) of
2.80 + SOME isa_fn => ("OK",thy',isa_fn)
2.81 + | NONE => ("applicable_in Calculate: unknown '" ^ scrop ^ "'", "", ("", Eval_Def.e_evalfn))
2.82 + end
2.83 + end;
2.84 +
2.85 +(** Solve_Step.check **)
2.86 +
2.87 (*
2.88 check tactics (input by the user, mostly) for applicability
2.89 and determine as much of the result of the tactic as possible initially.
2.90 @@ -46,7 +108,7 @@
2.91 end
2.92 | check (Tactic.Calculate op_) (cs as (pt, (p, _))) =
2.93 let
2.94 - val (msg, thy', isa_fn) = ApplicableOLD.from_pblobj_or_detail_calc op_ p pt;
2.95 + val (msg, thy', isa_fn) = get_eval op_ p pt;
2.96 val f = Calc.current_formula cs;
2.97 in
2.98 if msg = "OK"
2.99 @@ -76,7 +138,7 @@
2.100 end
2.101 | check (Tactic.Rewrite thm) (cs as (pt, (p, _))) =
2.102 let
2.103 - val (msg, thy', ro, rls', _) = ApplicableOLD.from_pblobj_or_detail_thm thm p pt;
2.104 + val (msg, thy', ro, rls', _) = get_ruleset thm p pt;
2.105 val thy = ThyC.get_theory thy';
2.106 val f = Calc.current_formula cs;
2.107 in
2.108 @@ -182,6 +244,9 @@
2.109 | check Tactic.End_Proof' _ = Applicable.Yes Tactic.End_Proof''
2.110 | check m _ = raise ERROR ("Solve_Step.check called for " ^ Tactic.input_to_string m);
2.111
2.112 +
2.113 +(** Solve_Step.add **)
2.114 +
2.115 fun add (Tactic.Apply_Method' (_, topt, is, _)) (_, ctxt) (pt, pos as (p, _)) =
2.116 (case topt of
2.117 SOME t =>
3.1 --- a/src/Tools/isac/MathEngine/detail-step.sml Mon May 04 11:13:16 2020 +0200
3.2 +++ b/src/Tools/isac/MathEngine/detail-step.sml Mon May 04 12:38:16 2020 +0200
3.3 @@ -42,7 +42,7 @@
3.4 in ("detailrls", pt''', (p @ [length newnds], Res)) end
3.5 | _ =>
3.6 let
3.7 - val is = Generate.init_istate tac t
3.8 + val is = Istate.init_detail tac t
3.9 val tac_ = Tactic.Apply_Method' (Method.id_empty(*WN0402: see generate1 !?!*), SOME t, is, ctxt)
3.10 val pos' = ((lev_on o lev_dn) p, Frm)
3.11 val (_, _, _, pt') = Step.add tac_ (is, ctxt) (pt, pos') (* implicit Take *)
4.1 --- a/src/Tools/isac/Specify/appl.sml Mon May 04 11:13:16 2020 +0200
4.2 +++ b/src/Tools/isac/Specify/appl.sml Mon May 04 12:38:16 2020 +0200
4.3 @@ -6,15 +6,12 @@
4.4
4.5 signature APPLICABLE_OLD =
4.6 sig
4.7 - val from_pblobj_or_detail_thm: 'a -> Pos.pos -> Ctree.ctree -> string * ThyC.id * Rule_Def.rew_ord' * Rule_Def.rule_set * bool
4.8 - val from_pblobj_or_detail_calc: string -> Pos.pos -> Ctree.ctree -> string * ThyC.id * (string * Rule_Def.eval_fn)
4.9 val mk_set: 'a -> Ctree.ctree -> Pos.pos -> term -> term -> term * term list
4.10 val split_dummy: string -> string * string
4.11 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
4.12 (*NONE*)
4.13 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
4.14 val check_elementwise: theory -> Rule_Def.rule_set -> term -> term * term list -> term * term list
4.15 - val rew_info: Rule_Def.rule_set -> string * Rule_Def.rule_set * Rule_Def.calc list
4.16 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
4.17 end
4.18
4.19 @@ -23,58 +20,6 @@
4.20 struct
4.21 (**)
4.22
4.23 -fun rew_info (Rule_Def.Repeat {erls, rew_ord = (rew_ord', _), calc = ca, ...}) =
4.24 - (rew_ord', erls, ca)
4.25 - | rew_info (Rule_Set.Sequence {erls, rew_ord = (rew_ord', _), calc = ca, ...}) =
4.26 - (rew_ord', erls, ca)
4.27 - | rew_info (Rule_Set.Rrls {erls, rew_ord = (rew_ord', _), calc = ca, ...}) =
4.28 - (rew_ord', erls, ca)
4.29 - | rew_info rls = error ("rew_info called with '" ^ Rule_Set.id rls ^ "'");
4.30 -
4.31 -(*FIXME.3.4.03:re-organize from_pblobj_or_detail_thm after rls' --> rls*)
4.32 -fun from_pblobj_or_detail_thm _ p pt =
4.33 - let
4.34 - val (pbl, p', rls') = Ctree.parent_node pt p
4.35 - in
4.36 - if pbl
4.37 - then
4.38 - let
4.39 - val thy' = Ctree.get_obj Ctree.g_domID pt p'
4.40 - val {rew_ord', erls, ...} = Specify.get_met (Ctree.get_obj Ctree.g_metID pt p')
4.41 - in ("OK", thy', rew_ord', erls, false) end
4.42 - else
4.43 - let
4.44 - val thy' = Ctree.get_obj Ctree.g_domID pt (Ctree.par_pblobj pt p)
4.45 - val (rew_ord', erls, _) = rew_info rls'
4.46 - in ("OK", thy', rew_ord', erls, false) end
4.47 - end;
4.48 -(*FIXME.3.4.03:re-organize from_pblobj_or_detail_calc after rls' --> rls*)
4.49 -fun from_pblobj_or_detail_calc scrop p pt =
4.50 - let
4.51 - val (pbl, p', rls') = Ctree.parent_node pt p
4.52 - in
4.53 - if pbl
4.54 - then
4.55 - let
4.56 - val thy' = Ctree.get_obj Ctree.g_domID pt p'
4.57 - val {calc = scr_isa_fns, ...} = Specify.get_met (Ctree.get_obj Ctree.g_metID pt p')
4.58 - val opt = assoc (scr_isa_fns, scrop)
4.59 - in
4.60 - case opt of
4.61 - SOME isa_fn => ("OK", thy', isa_fn)
4.62 - | NONE => ("applicable_in Calculate: unknown '" ^ scrop ^ "'", "", ("", Eval_Def.e_evalfn))
4.63 - end
4.64 - else
4.65 - let
4.66 - val thy' = Ctree.get_obj Ctree.g_domID pt (Ctree.par_pblobj pt p);
4.67 - val (_, _,(*_,*)scr_isa_fns) = rew_info rls'(*rls*)
4.68 - in
4.69 - case assoc (scr_isa_fns, scrop) of
4.70 - SOME isa_fn => ("OK",thy',isa_fn)
4.71 - | NONE => ("applicable_in Calculate: unknown '" ^ scrop ^ "'", "", ("", Eval_Def.e_evalfn))
4.72 - end
4.73 - end;
4.74 -
4.75 (*for Check_elementwise in applicable_in: [x=1,..] Assumptions -> (x,0<=x&..)*)
4.76 fun mk_set _(*thy*) _ _ (Const ("List.list.Nil", _)) _ = (TermC.empty, [])
4.77 | mk_set _ pt p (Const ("ListC.UniversalList", _)) pred =
5.1 --- a/src/Tools/isac/Specify/generate.sml Mon May 04 11:13:16 2020 +0200
5.2 +++ b/src/Tools/isac/Specify/generate.sml Mon May 04 12:38:16 2020 +0200
5.3 @@ -15,7 +15,6 @@
5.4
5.5 type test_out = Pos.pos' * Pos.pos' list * mout * Ctree.ctree
5.6
5.7 - val init_istate: Tactic.input -> term -> Istate_Def.T
5.8 val init_pbl: (string * (term * 'a)) list -> Model.itm list
5.9 val init_pbl': (string * (term * term)) list -> Model.itm list
5.10 val generate_inconsistent_rew: Subst.input option * ThmC.T -> term -> Istate_Def.T * Proof.context ->
5.11 @@ -34,30 +33,6 @@
5.12 open Ctree
5.13 open Pos
5.14
5.15 -
5.16 -(* initialize istate for Detail_Set *)
5.17 -fun init_istate (Tactic.Rewrite_Set rls) t =
5.18 - let
5.19 - val thy = ThyC.get_theory "Isac_Knowledge"
5.20 - val args = Auto_Prog.gen thy t (assoc_rls rls) |> Program.formal_args
5.21 - in
5.22 - Istate_Def.Pstate (Istate_Def.e_pstate |> Istate_Def.set_env_true [(hd args, t)])
5.23 - end
5.24 - | init_istate (Tactic.Rewrite_Set_Inst (subs, rls)) t =
5.25 - let
5.26 - val thy = ThyC.get_theory "Isac_Knowledge"
5.27 - val rls' = assoc_rls rls
5.28 - val v = case Subst.T_from_input thy subs of
5.29 - (_, v) :: _ => v (*...we suppose the substitution of only ONE bound variable*)
5.30 - | _ => raise ERROR "init_istate: uncovered case"
5.31 - val prog = Auto_Prog.gen thy t rls'
5.32 - val args = Program.formal_args prog
5.33 - in
5.34 - Istate_Def.Pstate (Istate_Def.e_pstate |> Istate_Def.set_env_true (args ~~ [t, v]))
5.35 - end
5.36 - | init_istate tac _ = error ("init_istate: uncovered definition for " ^ Tactic.input_to_string tac)
5.37 -
5.38 -
5.39 datatype pblmet = (*%^%*)
5.40 Upblmet (*undefined*)
5.41 | Problem of Problem.id (*%^%*)
6.1 --- a/src/Tools/isac/TODO.thy Mon May 04 11:13:16 2020 +0200
6.2 +++ b/src/Tools/isac/TODO.thy Mon May 04 12:38:16 2020 +0200
6.3 @@ -27,7 +27,7 @@
6.4 (*\------- to from -------/*)
6.5 \begin{itemize}
6.6 \item xxx
6.7 - \item rm warnings from solve-step.sml
6.8 + \item rename Tactic.Calculate -> Tactic.Evaluate
6.9 \item xxx
6.10 \item rename/relocate: Selem.result -> Calc.result ?OR? (NEW..)Formula.result
6.11 \item xxx
7.1 --- a/test/Tools/isac/MathEngine/mathengine-stateless.sml Mon May 04 11:13:16 2020 +0200
7.2 +++ b/test/Tools/isac/MathEngine/mathengine-stateless.sml Mon May 04 12:38:16 2020 +0200
7.3 @@ -201,7 +201,7 @@
7.4 val rls = (assoc_rls o rls_of) tac
7.5 val ctxt = get_ctxt pt pos
7.6 (*rls = Rule_Set.Repeat {calc = [], erls = ...*)
7.7 - val is = init_istate tac t
7.8 + val is = Istate.init_detail tac t
7.9 (*TODO.WN060602 Pstate (["(t_, Problem (Isac,[equation,univar]))"]
7.10 is wrong for simpl, but working ?!? *)
7.11 val tac_ = Apply_Method' (Method.id_empty(*WN0402: see Step.add !?!*), SOME t, is, ctxt)
8.1 --- a/test/Tools/isac/Minisubpbl/700-interSteps.sml Mon May 04 11:13:16 2020 +0200
8.2 +++ b/test/Tools/isac/Minisubpbl/700-interSteps.sml Mon May 04 12:38:16 2020 +0200
8.3 @@ -87,7 +87,7 @@
8.4 val rls = (assoc_rls o Tactic.rls_of) tac
8.5 val ctxt = get_ctxt pt pos
8.6 val _ = (*case*) rls (*of*);
8.7 - val is = Generate.init_istate tac t
8.8 + val is = Istate.init_detail tac t
8.9
8.10 (*+*)val Rule_Set.Repeat {scr = EmptyProg, ...} = rls; (*this prog is replaced by Auto_Prog.gen on the fly*)
8.11
9.1 --- a/test/Tools/isac/ProgLang/auto_prog.sml Mon May 04 11:13:16 2020 +0200
9.2 +++ b/test/Tools/isac/ProgLang/auto_prog.sml Mon May 04 12:38:16 2020 +0200
9.3 @@ -50,9 +50,8 @@
9.4 if UnparseC.terms (formal_args auto_script) = "[\"t_t\",\"v\"]"
9.5 then () else error "formal_args of auto-gen.script changed";
9.6
9.7 - init_istate (Rewrite_Set_Inst (["(''bdv'', x)"], "integration_rules"))
9.8 - (str2term "someTermWithBdv");
9.9 -"~~~~~ fun init_istate , args:"; val ((Tactic.Rewrite_Set_Inst (subs, rls)), t)
9.10 + Istate.init_detail (Rewrite_Set_Inst (["(''bdv'', x)"], "integration_rules")) (str2term "someTermWithBdv");
9.11 +"~~~~~ fun init_detail , args:"; val ((Tactic.Rewrite_Set_Inst (subs, rls)), t)
9.12 = ((Rewrite_Set_Inst (["(''bdv'', x)"], "integration_rules")), str2term "someTermWithBdv");
9.13 val v = case Subst.T_from_input (ThyC.get_theory "Isac_Knowledge") subs of
9.14 (_, v) :: _ => v;
9.15 @@ -115,7 +114,7 @@
9.16 (*if*) (not o is_interpos) ip = false;
9.17 val ip' = lev_pred' pt ip;
9.18
9.19 -(*Detail_Step.go pt ip ..ERROR interSteps>..>init_istate: "norm_Poly" has Empty_Prog*)
9.20 +(*Detail_Step.go pt ip ..ERROR interSteps>..>init_detail: "norm_Poly" has Empty_Prog*)
9.21 val ("donesteps", ctree_BEFORE_step_into, pos'_BEFORE_step_into) = Detail_Step.go pt ip;
9.22 "~~~~~ fun go, args:"; val (pt, (pos as (p, _))) = (pt, ip);
9.23 val nd = Ctree.get_nd pt p
10.1 --- a/test/Tools/isac/Test_Isac_Short.thy Mon May 04 11:13:16 2020 +0200
10.2 +++ b/test/Tools/isac/Test_Isac_Short.thy Mon May 04 12:38:16 2020 +0200
10.3 @@ -7,6 +7,8 @@
10.4 plus
10.5 ~~/test/Tools/isac/ADDTESTS
10.6 ~~/test/Tools/isac/Minisubpbl: the Lucas-Interpreter's core functionality
10.7 +
10.8 +Note, that only the first error in a file is shown here.
10.9 *)
10.10
10.11 section \<open>Notes on running tests\<close>