# HG changeset patch # User Walther Neuper # Date 1585760043 -7200 # Node ID 06a5cfe042230811b97e8534c931f516689dd20d # Parent 566d1b41dd550ced53c44704d39854bdfb5a4bbd renaming, cleanup diff -r 566d1b41dd55 -r 06a5cfe04223 src/Tools/isac/CalcElements/KEStore.thy --- a/src/Tools/isac/CalcElements/KEStore.thy Wed Apr 01 14:14:46 2020 +0200 +++ b/src/Tools/isac/CalcElements/KEStore.thy Wed Apr 01 18:54:03 2020 +0200 @@ -6,6 +6,7 @@ begin ML_file libraryC.sml +ML_file "rule-def.sml" ML_file rule.sml ML_file calcelems.sml diff -r 566d1b41dd55 -r 06a5cfe04223 src/Tools/isac/Interpret/error-pattern.sml --- a/src/Tools/isac/Interpret/error-pattern.sml Wed Apr 01 14:14:46 2020 +0200 +++ b/src/Tools/isac/Interpret/error-pattern.sml Wed Apr 01 18:54:03 2020 +0200 @@ -43,18 +43,17 @@ (*the lists contain eq-al elem-pairs at the beginning; return first list reverted (again) - ie. in order as required subsequently*) fun dropwhile' equal (f1::f2::fs) (i1::i2::is) = - if equal f1 i1 - then + if equal f1 i1 then if equal f2 i2 then dropwhile' equal (f2 :: fs) (i2 :: is) else (rev (f1 :: f2 :: fs), i1 :: i2 :: is) else error "dropwhile': did not start with equal elements" | dropwhile' equal (f::fs) [i] = - if equal f i - then (rev (f::fs), [i]) + if equal f i then + (rev (f::fs), [i]) else error "dropwhile': did not start with equal elements" | dropwhile' equal [f] (i::is) = - if equal f i - then ([f], i::is) + if equal f i then + ([f], i::is) else error "dropwhile': did not start with equal elements" | dropwhile' _ _ _ = error "dropwhile': uncovered case" @@ -85,8 +84,7 @@ | (fod, []) => if derivat fod = ifo then (true, fod) (*ifo is normal form*) else (false, []) | ([], ifod) => if fo = derivat ifod then (true, ((map rev_deriv') o rev) ifod) else (false, []) | (fod, ifod) => - if derivat fod = derivat ifod (*common normal form found*) - then + if derivat fod = derivat ifod (*common normal form found*) then let val (fod', rifod') = dropwhile' equal (rev fod) (rev ifod) in (true, fod' @ (map rev_deriv' rifod')) end @@ -101,8 +99,7 @@ val (res', _, _, rewritten) = Rewrite.rew_sub (Rule.Isac()) 1 subst Rule.e_rew_ord Rule.e_rls false [] (HOLogic.Trueprop $ pat) res; in - if rewritten - then + if rewritten then let val norm_res = case Rewrite.rewrite_set_inst_ (Rule.Isac()) false subst rls res' of NONE => res' @@ -139,8 +136,8 @@ val (form', _, _, rewritten) = Rewrite.rew_sub (Rule.Isac()) 1 subst Rule.e_rew_ord Rule.e_rls false [] (HOLogic.Trueprop $ pat) form; in (*the fillpat of the thm must be dedicated to errpatID*) - if errpatID = erpaID andalso rewritten - then SOME (fillpatID, HOLogic.mk_eq (form, form'), thm, subs_opt) + if errpatID = erpaID andalso rewritten then + SOME (fillpatID, HOLogic.mk_eq (form, form'), thm, subs_opt) else NONE end @@ -189,8 +186,8 @@ |Tactic.Rewrite' (_, _, _, _, _, _, (res, _)) => res | t => error ("is_exactly_equal: uncovered case for " ^ Tactic.string_of t) in - if not (ifo = res) - then ("input does not exactly fill the gaps", Tactic.Tac "") + if not (ifo = res) then + ("input does not exactly fill the gaps", Tactic.Tac "") else ("ok", tac) end end diff -r 566d1b41dd55 -r 06a5cfe04223 src/Tools/isac/Interpret/li-tool.sml --- a/src/Tools/isac/Interpret/li-tool.sml Wed Apr 01 14:14:46 2020 +0200 +++ b/src/Tools/isac/Interpret/li-tool.sml Wed Apr 01 18:54:03 2020 +0200 @@ -13,7 +13,7 @@ | Not_Associated; val associate: Ctree.ctree -> Proof.context -> (Tactic.T * term (*..Prog_Tac*)) -> ass - val implicit_take : 'a -> Program.T -> (term * term) list -> term option + val implicit_take : Program.T -> (term * term) list -> term option val init_pstate : Rule.rls -> Proof.context -> Model.itm list -> Celem.metID -> Istate.T * Proof.context * Program.T @@ -27,12 +27,12 @@ (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *) (*NONE*) (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* ) - val itms2args : 'a -> Celem.metID -> Model.itm list -> term list + val arguments_from_model : Celem.metID -> Model.itm list -> term list ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*) end -(* traces the leaves (ie. non-tactical nodes) of Prog found by find_next_step, see "and scr" *) -val trace_LI = Unsynchronized.ref false; (* TODO: how are traces done in Isabelle? *) +(* traces the leaves (ie. non-tactical nodes) of Prog found by find_next_step *) +val trace_LI = Unsynchronized.ref false; (* TODO: adopt Isabelle's tracing *) (**) structure LItool(**): LUCAS_INTERPRETER_TOOL(**) = @@ -41,41 +41,33 @@ open Ctree open Pos -(* determine the first tactic in case of a program with one argument (like simplification) - and without an initial Tactic.Take *) -fun implicit_take thy (Rule.Prog prog) env = - (case Prog_Tac.get_first thy prog of - NONE => NONE - | SOME prog_tac => SOME (subst_atomic env prog_tac)) - | implicit_take _ _ _ = error "implicit_take: no match"; +(* find the formal argument of a tactic in case there is only one (e.g. in simplification) *) +fun implicit_take (Rule.Prog prog) env = + (case Prog_Tac.get_first_argument prog of + NONE => NONE + | SOME prog_tac => SOME (subst_atomic env prog_tac)) + | implicit_take _ _ = error "implicit_take: no match"; -type dsc = typ; (* <-> nam..unknow in Descript.thy *) - -(*.create the actual parameters (args) of script: their order - is given by the order in met.pat .*) -(*WN.5.5.03: ?: does this allow for different descriptions ??? - ?: why not taken from formal args of script ??? -!: FIXXXME penv: push it here in itms2args into script-evaluation*) -val errmsg = "ERROR: the guard is missing (#ppc in 'type met' added in prep_met)." -fun errmsg2 d itms = ("itms2args: '" ^ Rule.term2str d ^ "' not in itms:\n" ^ -"itms:\n" ^ Model.itms2str_ @{context} itms) -fun itms2args _ mI itms = +(* *) +val error_msg_1 = "ERROR: the guard is missing (#ppc in 'type met' added in prep_met)." +fun error_msg_2 d itms = ("arguments_from_model: '" ^ Rule.term2str d ^ "' not in itms:\n" ^ + "itms:\n" ^ Model.itms2str_ @{context} itms) +(* turn model-items into arguments for a program *) +fun arguments_from_model mI itms = let val mvat = Model.max_vt itms fun okv mvat (_, vats, b, _, _) = member op = vats mvat andalso b val itms = filter (okv mvat) itms fun test_dsc d (_, _, _, _, itm_) = (d = Model.d_in itm_) fun itm2arg itms (_,(d,_)) = - case find_first (test_dsc d) itms of - NONE => raise ERROR (errmsg2 d itms) - | SOME (_, _, _, _, itm_) => Model.penvval_in itm_ - (*| SOME (_,_,_,_,itm_) => mk_arg thy (Model.d_in itm_) (ts_in itm_); - penv postponed; presently penv holds already Env.update for script*) + case find_first (test_dsc d) itms of + NONE => raise ERROR (error_msg_2 d itms) + | SOME (_, _, _, _, itm_) => Model.penvval_in itm_ val pats = (#ppc o Specify.get_met) mI - val _ = if pats = [] then raise ERROR errmsg else () + val _ = if pats = [] then raise ERROR error_msg_1 else () in (flat o (map (itm2arg itms))) pats end; -(* convert a Prog_Tac to Tactic.input *) +(* convert a Prog_Tac to Tactic.input; specific for "Prog_Tac.SubProblem" *) fun tac_from_prog _ thy (Const ("Prog_Tac.Rewrite", _) $ thmID $ _) = let val tid = HOLogic.dest_string thmID @@ -103,165 +95,145 @@ datatype ass = Associated of - Tactic.T (* Subproblem' gets args instantiated in associate *) - * term (* resulting from application of Tactic.T *) - * Proof.context (* updated by assumptioons from Rewrite* *) + Tactic.T (* Subproblem' gets args instantiated in associate *) + * term (* resulting from application of Tactic.T *) + * Proof.context (* updated by assumptioons from Rewrite* *) | Ass_Weak of Tactic.T * term * Proof.context | Not_Associated; +fun trace_msg_3 tac = + if (!trace_LI) then + tracing("@@@ the \"tac_\" proposed to apply does NOT match the leaf found in the program:\n" ^ + "@@@ tac_ = \"" ^ Tactic.string_of tac ^ "\"") + else (); (* associate is the ONLY code within by_tactic, which handles Tactic.T individually; thus it does ContextC.insert_assumptions in case of Rewrite*. + The argument Ctree.ctree is required only for Subproblem'. *) -fun trace_msg_3 tac = - if (!trace_LI) - then tracing("@@@ the \"tac_\" proposed to apply does NOT match the leaf found in the program:\n" - ^ "@@@ tac_ = \"" ^ Tactic.string_of tac ^ "\"") - else (); fun associate _ ctxt (m as Tactic.Rewrite_Inst' - (_, _, _, _, _, thm'' as (thmID, _), f, (f', asms')), stac) = - (case stac of - (Const ("Prog_Tac.Rewrite'_Inst", _) $ _ $ thmID_ $ f_) => - if thmID = HOLogic.dest_string thmID_ - then - if f = f_ - then Associated (m, f', ContextC.insert_assumptions asms' ctxt) - else Ass_Weak (m, f', ContextC.insert_assumptions asms' ctxt) - else ((*tracing"3### associate ..Not_Associated";*) Not_Associated) - | (Const ("Prog_Tac.Rewrite'_Set'_Inst",_) $ _ $ rls_ $ f_) => - if Rtools.contains_rule (Rule.Thm thm'') (assoc_rls (HOLogic.dest_string rls_)) - then if f = f_ then Associated (m, f', ContextC.insert_assumptions asms' ctxt) - else Ass_Weak (m, f', ContextC.insert_assumptions asms' ctxt) - else Not_Associated - | _ => Not_Associated) + (_, _, _, _, _, thm'' as (thmID, _), f, (f', asms')), stac) = + (case stac of + (Const ("Prog_Tac.Rewrite'_Inst", _) $ _ $ thmID_ $ f_) => + if thmID = HOLogic.dest_string thmID_ then + if f = f_ then + Associated (m, f', ContextC.insert_assumptions asms' ctxt) + else Ass_Weak (m, f', ContextC.insert_assumptions asms' ctxt) + else Not_Associated + | (Const ("Prog_Tac.Rewrite'_Set'_Inst",_) $ _ $ rls_ $ f_) => + if Rtools.contains_rule (Rule.Thm thm'') (assoc_rls (HOLogic.dest_string rls_)) then + if f = f_ then + Associated (m, f', ContextC.insert_assumptions asms' ctxt) + else Ass_Weak (m, f', ContextC.insert_assumptions asms' ctxt) + else Not_Associated + | _ => Not_Associated) | associate _ ctxt (m as Tactic.Rewrite' (_, _, _, _, thm'' as (thmID, _), f, (f', asms')), stac) = - (case stac of - (Const ("Prog_Tac.Rewrite", _) $ thmID_ $ f_) => - if thmID = HOLogic.dest_string thmID_ - then - if f = f_ - then Associated (m, f', ContextC.insert_assumptions asms' ctxt) - else Ass_Weak (m, f', ContextC.insert_assumptions asms' ctxt) - else Not_Associated - | (Const ("Prog_Tac.Rewrite'_Set", _) $ rls_ $ f_) => - if Rtools.contains_rule (Rule.Thm thm'') (assoc_rls (HOLogic.dest_string rls_)) - then - if f = f_ - then Associated (m, f', ContextC.insert_assumptions asms' ctxt) - else Ass_Weak (m, f', ContextC.insert_assumptions asms' ctxt) - else Not_Associated - | _ => Not_Associated) + (case stac of + (Const ("Prog_Tac.Rewrite", _) $ thmID_ $ f_) => + if thmID = HOLogic.dest_string thmID_ then + if f = f_ then + Associated (m, f', ContextC.insert_assumptions asms' ctxt) + else Ass_Weak (m, f', ContextC.insert_assumptions asms' ctxt) + else Not_Associated + | (Const ("Prog_Tac.Rewrite'_Set", _) $ rls_ $ f_) => + if Rtools.contains_rule (Rule.Thm thm'') (assoc_rls (HOLogic.dest_string rls_)) then + if f = f_ then + Associated (m, f', ContextC.insert_assumptions asms' ctxt) + else Ass_Weak (m, f', ContextC.insert_assumptions asms' ctxt) + else Not_Associated + | _ => Not_Associated) | associate _ ctxt (m as Tactic.Rewrite_Set_Inst' (_, _, _, rls, f, (f', asms')), - (Const ("Prog_Tac.Rewrite'_Set'_Inst", _) $ _ $ rls_ $ f_)) = - if Rule.id_rls rls = HOLogic.dest_string rls_ - then - if f = f_ - then Associated (m, f', ContextC.insert_assumptions asms' ctxt) - else Ass_Weak (m ,f', ContextC.insert_assumptions asms' ctxt) - else Not_Associated + (Const ("Prog_Tac.Rewrite'_Set'_Inst", _) $ _ $ rls_ $ f_)) = + if Rule.id_rls rls = HOLogic.dest_string rls_ then + if f = f_ then + Associated (m, f', ContextC.insert_assumptions asms' ctxt) + else Ass_Weak (m ,f', ContextC.insert_assumptions asms' ctxt) + else Not_Associated | associate _ ctxt (m as Tactic.Detail_Set_Inst' (_, _, _, rls, f, (f', asms')), - (Const ("Prog_Tac.Rewrite'_Set'_Inst", _) $ _ $ rls_ $ f_)) = - if Rule.id_rls rls = HOLogic.dest_string rls_ - then - if f = f_ - then Associated (m, f', ContextC.insert_assumptions asms' ctxt) - else Ass_Weak (m ,f', ContextC.insert_assumptions asms' ctxt) - else Not_Associated + (Const ("Prog_Tac.Rewrite'_Set'_Inst", _) $ _ $ rls_ $ f_)) = + if Rule.id_rls rls = HOLogic.dest_string rls_ then + if f = f_ then + Associated (m, f', ContextC.insert_assumptions asms' ctxt) + else Ass_Weak (m ,f', ContextC.insert_assumptions asms' ctxt) + else Not_Associated | associate _ ctxt (m as Tactic.Rewrite_Set' (_, _, rls, f, (f', asms')), - (Const ("Prog_Tac.Rewrite'_Set", _) $ rls_ $ f_)) = - if Rule.id_rls rls = HOLogic.dest_string rls_ - then - if f = f_ - then Associated (m, f', ContextC.insert_assumptions asms' ctxt) - else Ass_Weak (m ,f', ContextC.insert_assumptions asms' ctxt) - else Not_Associated + (Const ("Prog_Tac.Rewrite'_Set", _) $ rls_ $ f_)) = + if Rule.id_rls rls = HOLogic.dest_string rls_ then + if f = f_ then + Associated (m, f', ContextC.insert_assumptions asms' ctxt) + else Ass_Weak (m ,f', ContextC.insert_assumptions asms' ctxt) + else Not_Associated | associate _ ctxt (m as Tactic.Detail_Set' (_, _, rls, f, (f', asms')), - (Const ("Prog_Tac.Rewrite'_Set", _) $ rls_ $ f_)) = - if Rule.id_rls rls = HOLogic.dest_string rls_ - then - if f = f_ - then Associated (m, f', ContextC.insert_assumptions asms' ctxt) - else Ass_Weak (m ,f', ContextC.insert_assumptions asms' ctxt) - else Not_Associated + (Const ("Prog_Tac.Rewrite'_Set", _) $ rls_ $ f_)) = + if Rule.id_rls rls = HOLogic.dest_string rls_ then + if f = f_ then + Associated (m, f', ContextC.insert_assumptions asms' ctxt) + else Ass_Weak (m ,f', ContextC.insert_assumptions asms' ctxt) + else Not_Associated | associate _ ctxt (m as Tactic.Calculate' (_, op_, f, (f', _)), stac) = - (case stac of - (Const ("Prog_Tac.Calculate",_) $ op__ $ f_) => - if op_ = HOLogic.dest_string op__ - then - if f = f_ - then Associated (m, f', ctxt) - else Ass_Weak (m ,f', ctxt) - else Not_Associated - | (Const ("Prog_Tac.Rewrite'_Set'_Inst", _) $ _ $ rls_ $ f_) => - let val thy = Celem.assoc_thy "Isac_Knowledge"; - in - if Rtools.contains_rule (Rule.Num_Calc (assoc_calc' thy op_ |> snd)) - (assoc_rls (HOLogic.dest_string rls_)) - then - if f = f_ - then Associated (m, f', ctxt) - else Ass_Weak (m ,f', ctxt) + (case stac of + (Const ("Prog_Tac.Calculate",_) $ op__ $ f_) => + if op_ = HOLogic.dest_string op__ then + if f = f_ then Associated (m, f', ctxt) else Ass_Weak (m ,f', ctxt) + else Not_Associated + | (Const ("Prog_Tac.Rewrite'_Set'_Inst", _) $ _ $ rls_ $ f_) => + if Rtools.contains_rule (Rule.Num_Calc (assoc_calc' (Celem.assoc_thy "Isac_Knowledge") + op_ |> snd)) (assoc_rls (HOLogic.dest_string rls_)) then + if f = f_ then Associated (m, f', ctxt) else Ass_Weak (m ,f', ctxt) else Not_Associated - end - | (Const ("Prog_Tac.Rewrite'_Set",_) $ rls_ $ f_) => - let val thy = Celem.assoc_thy "Isac_Knowledge"; - in - if Rtools.contains_rule (Rule.Num_Calc (assoc_calc' thy op_ |> snd)) - (assoc_rls (HOLogic.dest_string rls_)) - then - if f = f_ - then Associated (m, f', ctxt) - else Ass_Weak (m ,f', ctxt) + | (Const ("Prog_Tac.Rewrite'_Set",_) $ rls_ $ f_) => + if Rtools.contains_rule (Rule.Num_Calc (assoc_calc' ( Celem.assoc_thy "Isac_Knowledge") + op_ |> snd)) (assoc_rls (HOLogic.dest_string rls_)) then + if f = f_ then Associated (m, f', ctxt) else Ass_Weak (m ,f', ctxt) else Not_Associated - end - | _ => Not_Associated) + | _ => Not_Associated) | associate _ ctxt (m as Tactic.Check_elementwise' (consts, _, (consts_chkd, _)), - (Const ("Prog_Tac.Check'_elementwise",_) $ consts' $ _)) = - if consts = consts' - then Associated (m, consts_chkd, ctxt) - else Not_Associated + (Const ("Prog_Tac.Check'_elementwise",_) $ consts' $ _)) = + if consts = consts' then Associated (m, consts_chkd, ctxt) else Not_Associated | associate _ ctxt (m as Tactic.Or_to_List' (_, list), (Const ("Prog_Tac.Or'_to'_List", _) $ _)) = - Associated (m, list, ctxt) - | associate _ ctxt (m as Tactic.Take' term, (Const ("Prog_Tac.Take", _) $ _)) = Associated (m, term, ctxt) + Associated (m, list, ctxt) + | associate _ ctxt (m as Tactic.Take' term, (Const ("Prog_Tac.Take", _) $ _)) = + Associated (m, term, ctxt) | associate _ ctxt (m as Tactic.Substitute' (ro, erls, subte, f, f'), - (Const ("Prog_Tac.Substitute", _) $ _ $ t)) = - if f = t then Associated (m, f', ctxt) - else (*compare | applicable_in (p,p_) pt (m as Substitute sube)*) - if foldl and_ (true, map TermC.contains_Var subte) - then - let val t' = subst_atomic (map HOLogic.dest_eq subte (*TODO subte2subst*)) t - in if t = t' then error "associate: Substitute' not applicable to val of Expr" - else Associated (Tactic.Substitute' (ro, erls, subte, t, t'), t', ctxt) - end - else (case Rewrite.rewrite_terms_ (Rule.Isac ()) ro erls subte t of - SOME (t', _) => Associated (Tactic.Substitute' (ro, erls, subte, t, t'), t', ctxt) - | NONE => error "associate: Substitute' not applicable to val of Expr") + (Const ("Prog_Tac.Substitute", _) $ _ $ t)) = + if f = t then + Associated (m, f', ctxt) + else (*compare | applicable_in (p,p_) pt (m as Substitute sube)*) + if foldl and_ (true, map TermC.contains_Var subte) then + let + val t' = subst_atomic (map HOLogic.dest_eq subte) t + in + if t = t' then error "associate: Substitute' not applicable to val of Expr" + else Associated (Tactic.Substitute' (ro, erls, subte, t, t'), t', ctxt) + end + else + (case Rewrite.rewrite_terms_ (Rule.Isac ()) ro erls subte t of + SOME (t', _) => Associated (Tactic.Substitute' (ro, erls, subte, t, t'), t', ctxt) + | NONE => error "associate: Substitute' not applicable to val of Expr") | associate pt ctxt (Tactic.Subproblem' ((domID, pblID, _), _, _, _, _, _), - (stac as Const ("Prog_Tac.SubProblem", _) $ _ $ _)) = - (case Sub_Problem.tac_from_prog pt stac of - (_, tac as Tactic.Subproblem' ((dI, pI, _), _, _, _, _, f)) => - if domID = dI andalso pblID = pI - then Associated (tac, f, ctxt) - else Not_Associated - | _ => raise ERROR ("associate: uncovered case")) + (stac as Const ("Prog_Tac.SubProblem", _) $ _ $ _)) = + (case Sub_Problem.tac_from_prog pt stac of + (_, tac as Tactic.Subproblem' ((dI, pI, _), _, _, _, _, f)) => + if domID = dI andalso pblID = pI then Associated (tac, f, ctxt) else Not_Associated + | _ => raise ERROR ("associate: uncovered case")) | associate _ _ (tac, _) = (trace_msg_3 tac; Not_Associated); (* create the initial interpreter state - from the items of the guard and the formal arguments of the partial_function. + from the items of the guard and the formal arguments of the program. Note on progression from (a) type fmz_ \ (e) arguments of the partial_function: (a) fmz is given by a math author (b) fmz_ is transformed to ori list as a prerequisite for efficient interactive modelling (c) modelling creates an itm list from ori list + possible user input - (d) specifying a theory might add some items and create a guard for the partial_function - (e) fun relate_args creates an environment for evaluating the partial_function. -Note on sequence-relation (a) -- (e), i.e. the (formal) arguments of the partial_function: + (d) specifying a theory might add some items and create a guard for the program + (e) fun relate_args creates an environment for evaluating the program. +Note on sequence-relation (a) -- (e), i.e. the (formal) arguments of the program: * Since the arguments of the partial_function have no description (see Descript.thy), (e) depends on the sequence in fmz_ and on the types of the formal arguments. * pairing formal arguments with itm's follows the sequence * Thus the resulting sequence-relation can be ambiguous. * Ambiguities are done by rearranging fmz_ or the formal arguments. - * The latter is easier, albeit not optimal: a fmz_ can be used by different partial_functions. + * The latter is easier, albeit not optimal: a fmz_ can be used by different programs. *) local val errmsg = "ERROR: found no actual arguments for prog. of " @@ -297,7 +269,7 @@ fun init_pstate srls ctxt itms metID = let val itms = Specify.hack_until_review_Specify_2 metID itms - val actuals = itms2args (Proof_Context.theory_of ctxt) metID itms + val actuals = arguments_from_model metID itms val _ = if actuals <> [] then () else raise ERROR (errmsg ^ strs2str' metID) val (scr, sc) = (case (#scr o Specify.get_met) metID of scr as Rule.Prog sc => (trace_init metID; (scr, sc)) @@ -327,6 +299,7 @@ end; end (*local*) +(* get the simplifier of the current method *) fun get_simplifier (pt, (p, _)) = let val p' = Ctree.par_pblobj pt p @@ -334,12 +307,12 @@ val {srls, ...} = Specify.get_met metID in srls end +(* resume program interpretation at the beginning of a step *) fun resume_prog thy (p, p_) pt = let val (is_problem, p', rls') = parent_node pt p in - if is_problem - then + if is_problem then let val metID = get_obj g_metID pt p' val {srls, ...} = Specify.get_met metID @@ -347,16 +320,15 @@ case get_loc pt (p, p_) of (Istate.Pstate ist, ctxt) => (Istate.Pstate (Istate.set_eval srls ist), ctxt) | _ => raise ERROR "resume_prog: unexpected result from get_loc" - in ((is, ctxt), (#scr o Specify.get_met) metID) end - else (* 3 *) + in + ((is, ctxt), (#scr o Specify.get_met) metID) + end + else (get_loc pt (p, p_), Rule.Prog (Auto_Prog.gen (Celem.assoc_thy thy) (get_last_formula (pt, (p, p_))) rls')) end -(* - handle a leaf at the end of recursive descent; a leaf is either a Prog_Tac or a Prog_Expr. - snd of return value is the formal arguments in case of currying. -*) + fun trace_msg_1 call t stac = if (! trace_LI) then tracing ("@@@ " ^ call ^ " leaf \"" ^ Rule.term2str t ^ "\" \ Tac \"" ^ Rule.term2str stac ^ "\"") @@ -365,19 +337,22 @@ if (! trace_LI) then tracing("@@@ " ^ call ^ " leaf '" ^ Rule.term2str t ^ "' \ Expr \"" ^ Rule.term2str lexpr' ^ "\"") else (); - +(* + check a leaf at the end of recursive descent; a leaf is either a Prog_Tac or a Prog_Expr. + snd of return value is the formal arguments in case of currying. +*) fun check_leaf call ctxt srls (E, (a, v)) t = case Prog_Tac.eval_leaf E a v t of (Program.Tac stac, a') => - let val stac' = - Rewrite.eval_prog_expr (Proof_Context.theory_of ctxt) srls + let + val stac' = Rewrite.eval_prog_expr (Proof_Context.theory_of ctxt) srls (subst_atomic (Env.update_opt E (a, v)) stac) in (trace_msg_1 call t stac; (Program.Tac stac', a')) end | (Program.Expr lexpr, a') => - let val lexpr' = - Rewrite.eval_prog_expr (Proof_Context.theory_of ctxt) srls + let + val lexpr' = Rewrite.eval_prog_expr (Proof_Context.theory_of ctxt) srls (subst_atomic (Env.update_opt E (a, v)) lexpr) in (trace_msg_2 call t lexpr'; (Program.Expr lexpr', a')) diff -r 566d1b41dd55 -r 06a5cfe04223 src/Tools/isac/Interpret/lucas-interpreter.sml --- a/src/Tools/isac/Interpret/lucas-interpreter.sml Wed Apr 01 14:14:46 2020 +0200 +++ b/src/Tools/isac/Interpret/lucas-interpreter.sml Wed Apr 01 18:54:03 2020 +0200 @@ -189,10 +189,9 @@ check_tac cc ist (prog_tac, form_arg) fun go_scan_up (pcc as (sc, _)) (ist as {path, act_arg, found_accept, ...}) = - if path = [R] (*root of the program body*) - then - if found_accept - then Term_Val act_arg + if path = [R] (*root of the program body*) then + if found_accept then + Term_Val act_arg else raise ERROR "LItool.find_next_step without result" else scan_up pcc (ist |> path_up) (go_up path sc) (* scan is strictly to R, because at L there was an \expr_val\ *) @@ -265,8 +264,8 @@ (* scan program until an applicable tactic is found *) fun scan_to_tactic (prog, cc) (Pstate (ist as {path, ...})) = - if path = [] - then scan_dn cc (trans_scan_dn ist) (Program.body_of prog) + if path = [] then + scan_dn cc (trans_scan_dn ist) (Program.body_of prog) else go_scan_up (prog, cc) (trans_scan_up ist) | scan_to_tactic _ _ = raise ERROR "scan_to_tactic: uncovered pattern"; @@ -405,8 +404,8 @@ check_tac1 cct ist (prog_tac, form_arg) fun go_scan_up1 (pcct as (prog, _)) (ist as {path, act_arg, ...}) = - if 1 < length path - then scan_up1 pcct (ist |> path_up) (at_location (path_up' path) prog) + if 1 < length path then + scan_up1 pcct (ist |> path_up) (at_location (path_up' path) prog) else Term_Val1 act_arg (* scan is strictly to R, because at L there was a expr_val *) and scan_up1 pcct ist (Const ("Tactical.Try"(*1*), _) $ _ $ _) = go_scan_up1 pcct ist @@ -487,8 +486,8 @@ fun locate_input_tactic (Rule.Prog prog) cstate istate ctxt tac = (case scan_to_tactic1 (prog, (cstate, ctxt, tac)) istate of Accept_Tac1 ((ist as {assoc, ...}), ctxt, tac') => - if assoc - then Safe_Step (Pstate ist, ctxt, tac') + if assoc then + Safe_Step (Pstate ist, ctxt, tac') else Unsafe_Step (Pstate ist, ctxt, tac') | Reject_Tac1 _ => Not_Locatable (Tactic.string_of tac ^ " not locatable") | err => raise ERROR ("not-found-in-program: NotLocatable from " ^ @{make_string} err)) @@ -500,106 +499,85 @@ datatype input_term_result = Found_Step of Calc.T | Not_Derivable fun by_tactic (Tactic.Apply_Method' (mI, _, _, _)) (_, ctxt) (pt, pos as (p, _)) = - let - val (itms, (*l..*)oris, probl(*..l*)) = case get_obj I pt p of - PblObj {meth = itms, origin = (oris, _, _), probl, ...} => (itms, oris, probl) - | _ => error "LI.by_tactic Apply_Method': uncovered case get_obj" - val {ppc, ...} = Specify.get_met mI; - val itms = if itms <> [] then itms else Chead.complete_metitms oris probl [] ppc - val itms = Specify.hack_until_review_Specify_1 mI itms - val srls = LItool.get_simplifier (pt, pos) - val (is, env, ctxt, prog) = case LItool.init_pstate srls ctxt itms mI of - (is as Pstate {env, ...}, ctxt, scr) => (is, env, ctxt, scr) - | _ => error "LI.by_tactic Apply_Method': uncovered case init_pstate" - val ini = LItool.implicit_take (Celem.assoc_thy (get_obj g_domID pt p)) prog env; - val pos = start_new_level pos - in - case ini of - SOME t => - let (* implicit Take *) - val show_add = Tactic.Apply_Method' (mI, SOME t, is, ctxt); - val (pos, c, _, pt) = Generate.generate1 show_add (is, ctxt) (pt, pos) - in - ("ok", ([(Tactic.Apply_Method mI, show_add, (pos, (is, ctxt)))], c, (pt, pos))) - end - | NONE => - let - val (tac', ist', ctxt') = - case find_next_step prog (pt, (lev_dn p, Res)) is ctxt of - Next_Step (ist, ctxt, tac) => (tac, ist, ctxt) - | _ => raise ERROR ("LI.by_tactic..Apply_Method find_next_step \ " ^ strs2str' mI) - in - case tac' of - Tactic.Take' t => - let (* explicit Take *) - val show_add = Tactic.Apply_Method' (mI, SOME t, ist', ctxt'); - val (pos, c, _, pt) = Generate.generate1 show_add (ist', ctxt') (pt, pos) - in - ("ok", ([(Tactic.Apply_Method mI, show_add, (pos, (is, ctxt)))], c, (pt, pos))) - end - | add as Tactic.Subproblem' (_, _, headline, _, _, _) => - let (* Subproblem *) - val show = Tactic.Apply_Method' (mI, SOME headline, ist', ctxt'); - val (pos, c, _, pt) = Generate.generate1 add (ist', ctxt') (pt, pos) - in - ("ok", ([(Tactic.Apply_Method mI, show, (pos, (ist', ctxt')))], c, (pt, pos))) - end - | tac => - raise ERROR ("LI.by_tactic..Apply_Method' does NOT expect " ^ Tactic.string_of tac) - end - end -(*NEW* ) ------vvv: prog_res ( *NEW*) + let + val (itms, (*l..*)oris, probl(*..l*)) = case get_obj I pt p of + PblObj {meth = itms, origin = (oris, _, _), probl, ...} => (itms, oris, probl) + | _ => error "LI.by_tactic Apply_Method': uncovered case get_obj" + val {ppc, ...} = Specify.get_met mI; + val itms = if itms <> [] then itms else Chead.complete_metitms oris probl [] ppc + val itms = Specify.hack_until_review_Specify_1 mI itms + val srls = LItool.get_simplifier (pt, pos) + val (is, env, ctxt, prog) = case LItool.init_pstate srls ctxt itms mI of + (is as Pstate {env, ...}, ctxt, scr) => (is, env, ctxt, scr) + | _ => error "LI.by_tactic Apply_Method': uncovered case init_pstate" + val ini = LItool.implicit_take prog env; + val pos = start_new_level pos + in + case ini of + SOME t => + let (* implicit Take *) + val show_add = Tactic.Apply_Method' (mI, SOME t, is, ctxt); + val (pos, c, _, pt) = Generate.generate1 show_add (is, ctxt) (pt, pos) + in + ("ok", ([(Tactic.Apply_Method mI, show_add, (pos, (is, ctxt)))], c, (pt, pos))) + end + | NONE => + let + val (tac', ist', ctxt') = + case find_next_step prog (pt, (lev_dn p, Res)) is ctxt of + Next_Step (ist, ctxt, tac) => (tac, ist, ctxt) + | _ => raise ERROR ("LI.by_tactic..Apply_Method find_next_step \ " ^ strs2str' mI) + in + case tac' of + Tactic.Take' t => + let (* explicit Take *) + val show_add = Tactic.Apply_Method' (mI, SOME t, ist', ctxt'); + val (pos, c, _, pt) = Generate.generate1 show_add (ist', ctxt') (pt, pos) + in + ("ok", ([(Tactic.Apply_Method mI, show_add, (pos, (is, ctxt)))], c, (pt, pos))) + end + | add as Tactic.Subproblem' (_, _, headline, _, _, _) => + let (* Subproblem *) + val show = Tactic.Apply_Method' (mI, SOME headline, ist', ctxt'); + val (pos, c, _, pt) = Generate.generate1 add (ist', ctxt') (pt, pos) + in + ("ok", ([(Tactic.Apply_Method mI, show, (pos, (ist', ctxt')))], c, (pt, pos))) + end + | tac => + raise ERROR ("LI.by_tactic..Apply_Method' does NOT expect " ^ Tactic.string_of tac) + end + end | by_tactic (Tactic.Check_Postcond' (pI, _)) (sub_ist, sub_ctxt) (pt, pos as (p, _)) = -(*NEW* ) BETTER (curr_ist, curr_ctxt) -----^^^^^^^^^^^^^^^^^^^ ( *NEW*) - let - val parent_pos = par_pblobj pt p - val {scr, ...} = Specify.get_met (get_obj g_metID pt parent_pos); - val prog_res = - case find_next_step scr (pt, pos) sub_ist sub_ctxt of -(*OLD*) Next_Step (_, _, Tactic.Check_elementwise' (_, _, (prog_res, _))) => prog_res - |(*OLD*) End_Program (_, Tactic.Check_Postcond' (_, prog_res)) => prog_res -(*OLD*) | _ => raise ERROR ("Step_Solve.by_tactic Check_Postcond " ^ strs2str' pI) -(*OLD* ) vvv--- handled by ctxt \ drop ( *OLD*) -(*OLD*)val asm = (*?!? Rfun,Rrls rm case*)(case get_obj g_tac pt p of -(*OLD*) Tactic.Check_elementwise _ => (snd o (get_obj g_result pt)) p -(*OLD*) | _ => Ctree.get_assumptions pt pos) -(*OLD* )val tac = Tactic.Check_Postcond' (pI, (prog_res, asm)) -( *OLD*) - in - if parent_pos = [] - then - let -(*NEW*) val tac = Tactic.Check_Postcond' (pI, prog_res) -(*NEW*) - val is = Pstate (sub_ist |> the_pstate |> set_act prog_res |> set_found) - val ((p, p_), ps, _, pt) = Generate.generate1 tac (is, sub_ctxt) (pt, (parent_pos, Res)) - in - ("ok", ([(Tactic.Check_Postcond pI, tac, ((parent_pos, Res), (is, sub_ctxt)))], ps, (pt, (p, p_)))) - end - else - let (*resume program of parent PblObj, transfer result of Subproblem-program*) -(*OLD* ) val tac = Tactic.Check_Postcond' (pI, (prog_res, asm)) -(*OLD*) val (ist_parent, ctxt_parent) = case get_loc pt (parent_pos, Frm) of -(*OLD*) (Pstate i, c) => (i, c) -(*OLD*) | _ => error "LI.by_tactic Check_Postcond': uncovered case get_loc" -(*OLD*) val (ttttt, ctxt') = ContextC.subpbl_to_caller sub_ctxt prog_res ctxt_parent -(*OLD*) val is' = Pstate (ist_parent |> set_act prog_res |> set_found) -(*OLD*) val ((p, p_), ps, _, pt) = Generate.generate1 tac (is', ctxt') (pt, (parent_pos, Res)) -(*OLD*) in -(*OLD*) ("ok", ([(Tactic.Check_Postcond pI, tac, ((parent_pos, Res), (is', ctxt')))], ps, (pt, (p, p_)))) -(*OLD*) end -( *NEW*) -(*NEW*) val (ist_parent, ctxt_parent) = case get_loc pt (parent_pos, Frm) of -(*NEW*) (Pstate i, c) => (i, c) -(*NEW*) | _ => error "LI.by_tactic Check_Postcond': uncovered case get_loc" -(*NEW*) val (prog_res', ctxt') = ContextC.subpbl_to_caller sub_ctxt prog_res ctxt_parent -(*NEW*) val tac = Tactic.Check_Postcond' (pI, prog_res') -(*NEW*) val ist' = Pstate (ist_parent |> set_act prog_res |> set_found) -(*NEW*) val ((p, p_), ps, _, pt) = Generate.generate1 tac (ist', ctxt') (pt, (parent_pos, Res)) -(*NEW*) in -(*NEW*) ("ok", ([(Tactic.input_from_T tac, tac, ((parent_pos, Res), (ist', ctxt')))], ps, (pt, (p, p_)))) -(*NEW*) end - end + let + val parent_pos = par_pblobj pt p + val {scr, ...} = Specify.get_met (get_obj g_metID pt parent_pos); + val prog_res = + case find_next_step scr (pt, pos) sub_ist sub_ctxt of + (*OLD*) Next_Step (_, _, Tactic.Check_elementwise' (_, _, (prog_res, _))) => prog_res + |(*OLD*) End_Program (_, Tactic.Check_Postcond' (_, prog_res)) => prog_res + | _ => raise ERROR ("Step_Solve.by_tactic Check_Postcond " ^ strs2str' pI) + in + if parent_pos = [] then + let + val tac = Tactic.Check_Postcond' (pI, prog_res) + val is = Pstate (sub_ist |> the_pstate |> set_act prog_res |> set_found) + val ((p, p_), ps, _, pt) = Generate.generate1 tac (is, sub_ctxt) (pt, (parent_pos, Res)) + in + ("ok", ([(Tactic.Check_Postcond pI, tac, ((parent_pos, Res), (is, sub_ctxt)))], ps, (pt, (p, p_)))) + end + else + let (*resume program of parent PblObj, transfer result of Subproblem-program*) + val (ist_parent, ctxt_parent) = case get_loc pt (parent_pos, Frm) of + (Pstate i, c) => (i, c) + | _ => error "LI.by_tactic Check_Postcond': uncovered case get_loc" + val (prog_res', ctxt') = ContextC.subpbl_to_caller sub_ctxt prog_res ctxt_parent + val tac = Tactic.Check_Postcond' (pI, prog_res') + val ist' = Pstate (ist_parent |> set_act prog_res |> set_found) + val ((p, p_), ps, _, pt) = Generate.generate1 tac (ist', ctxt') (pt, (parent_pos, Res)) + in + ("ok", ([(Tactic.input_from_T tac, tac, ((parent_pos, Res), (ist', ctxt')))], ps, (pt, (p, p_)))) + end + end | by_tactic (Tactic.End_Proof'') _ ptp = ("end-of-calculation", ([], [], ptp)) | by_tactic tac_ ic (pt, pos) = let @@ -610,8 +588,8 @@ end (*find_next_step from program, by_tactic will update Ctree*) and do_next (ptp as (pt, pos as (p, p_))) = - if Celem.e_metID = get_obj g_metID pt (par_pblobj pt p) - then ("helpless", ([], [], (pt, (p, p_)))) + if Celem.e_metID = get_obj g_metID pt (par_pblobj pt p) then + ("helpless", ([], [], (pt, (p, p_)))) else let val thy' = get_obj g_domID pt (par_pblobj pt p); @@ -639,13 +617,9 @@ CAUTION: tacis in returned calcstate' do NOT construct resulting ptp -- all_modspec etc. has to be inserted at Subproblem' *) -fun compare_step (tacis, c, ptp as (pt, pos as (p, p_))) ifo = +fun compare_step (tacis, c, ptp as (pt, pos as (p, _))) ifo = let - val fo = - case p_ of - Pos.Frm => Ctree.get_obj Ctree.g_form pt p - | Pos.Res => (fst o (Ctree.get_obj Ctree.g_result pt)) p - | _ => Rule.e_term (*on PblObj is fo <> ifo*); + val fo = Calc.get_current_formula ptp val {nrls, ...} = Specify.get_met (Ctree.get_obj Ctree.g_metID pt (Ctree.par_pblobj pt p)) val {rew_ord, erls, rules, ...} = Rule.rep_rls nrls val (found, der) = Error_Pattern.concat_deriv rew_ord erls rules fo ifo; (*<---------------*) @@ -675,22 +649,14 @@ in compare_step (tacis, c @ c' @ c'', ptp) ifo end end -(* - handle a user-input formula, which may be a CAS-command, too. - * CAS-command: create a calchead, and do 1 step - * formula, which is no CAS-command: - compare iform with calc-tree.form at pos by equ_nrls and all subsequent pos; - collect all the Prog_Tac applied by the way; ...???TODO? - If "no derivation found" then Error_Pattern.check_for. - ALTERNATIVE: Error_Pattern.check_for _within_ compare_step: seems too expensive -*) +(* Locate a step in a program, which has been determined by input of a term *) fun locate_input_term (pt, pos) tm = let val pos_pred = Pos.lev_back' pos (*f_pred ---"step pos cs"---> f_succ in appendFormula*) val _(*f_pred*) = Ctree.get_curr_formula (pt, pos_pred) in case compare_step ([], [], (pt, pos_pred)) tm of - ("no derivation found", _) => Not_Derivable + ("no derivation found", _) => Not_Derivable | ("ok", (_, _, cstate)) => Found_Step cstate | _ => raise ERROR "compare_step: uncovered case" diff -r 566d1b41dd55 -r 06a5cfe04223 src/Tools/isac/Interpret/rewtools.sml --- a/src/Tools/isac/Interpret/rewtools.sml Wed Apr 01 14:14:46 2020 +0200 +++ b/src/Tools/isac/Interpret/rewtools.sml Wed Apr 01 18:54:03 2020 +0200 @@ -1,6 +1,8 @@ -(* tools for rewriting, reverse rewriting, context to thy concerning rewriting +(* authors: Walther Neuper 2002, 2006 (c) due to copyright terms + +tools for rewriting, reverse rewriting, context to thy concerning rewriting *) signature REWRITE_TOOLS = @@ -56,9 +58,10 @@ val deri2str : (Rule.rule * (term * term list)) list -> string val sym_trm : term -> term end - +(**) structure Rtools(**): REWRITE_TOOLS(**) = struct +(**) (*** reverse rewriting ***) (*. a '_deriv'ation is constructed during 'reverse rewring' by an Rrls * @@ -79,12 +82,12 @@ * (4) FIXME find criteria on when _not_ to step until End_Proof' * * (5) FIXME .*) -type deriv = (* derivation for insertin one level of nodes into the calctree *) - ( term * (* where the rule is applied to *) - Rule.rule * (* rule to be applied *) - ( term * (* resulting from rule application *) - term list)) (* assumptions resulting from rule application *) - list (* *) +type deriv = (* derivation for insertin one level of nodes into the Ctree *) + ( term * (* where the rule is applied to *) + Rule.rule * (* rule to be applied *) + ( term * (* resulting from rule application *) + term list)) (* assumptions resulting from rule application *) + list fun trta2str (t, r, (t', a)) = "\n(" ^ Rule.term2str t ^ ", " ^ Rule.rule2str' r ^ ", (" ^ Rule.term2str t' ^ ", " ^ Rule.terms2str a ^ "))" @@ -95,12 +98,7 @@ fun rtas2str rtas = (strs2str o (map rta2str)) rtas val deri2str = rtas2str -(* A1==>...==> An ==> (Lhs = Rhs) goes to A1 ==>...==> An ==> (Rhs = Lhs) - WN120320: reconsider the desing including the java front-end with html representation; - see tests - --- old compute rlsthmsNOTisac by eq_thmID --- - --- compute val rlsthmsNOTisac --- -*) +(* A1==>...==> An ==> (Lhs = Rhs) goes to A1 ==>...==> An ==> (Rhs = Lhs) *) fun sym_thm thm = let val (deriv, diff -r 566d1b41dd55 -r 06a5cfe04223 src/Tools/isac/Interpret/step-solve.sml --- a/src/Tools/isac/Interpret/step-solve.sml Wed Apr 01 14:14:46 2020 +0200 +++ b/src/Tools/isac/Interpret/step-solve.sml Wed Apr 01 18:54:03 2020 +0200 @@ -82,6 +82,13 @@ val do_next = LI.do_next + +(* + Locate a step in a program, which has been determined by input of a term. + Special case: if the term is a CAS-command, then create a calchead, and do 1 step. + If "no derivation found" then Error_Pattern.check_for. + (Error_Pattern.check_for *within* compare_step seems too expensive) +*) (*fun by_term (next_cs as (_, _, (pt, pos as (p, _))): Chead.calcstate') istr =*) fun by_term (pt, pos as (p, _)) istr = case TermC.parse (Celem.assoc_thy "Isac_Knowledge") istr of diff -r 566d1b41dd55 -r 06a5cfe04223 src/Tools/isac/Knowledge/DiffApp.thy --- a/src/Tools/isac/Knowledge/DiffApp.thy Wed Apr 01 14:14:46 2020 +0200 +++ b/src/Tools/isac/Knowledge/DiffApp.thy Wed Apr 01 18:54:03 2020 +0200 @@ -23,11 +23,11 @@ found to be reconsidered: - descriptions (Descript.thy) - penv: really need term list; or just rerun the whole example with num/var -- mk_arg, itms2args ... env in script different from penv ? +- mk_arg, arguments_from_model ... env in script different from penv ? - L = SubProblem eq ... show some vars on the worksheet ? (other means for referencing are labels (no on worksheet)) -WN.6.5.03 quick-and-dirty: mk_arg, itms2args just make most convenient env +WN.6.5.03 quick-and-dirty: mk_arg, arguments_from_model just make most convenient env from penv as is. \ diff -r 566d1b41dd55 -r 06a5cfe04223 src/Tools/isac/MathEngBasic/calculation.sml --- a/src/Tools/isac/MathEngBasic/calculation.sml Wed Apr 01 14:14:46 2020 +0200 +++ b/src/Tools/isac/MathEngBasic/calculation.sml Wed Apr 01 18:54:03 2020 +0200 @@ -6,6 +6,7 @@ signature CALCULATION = sig type T + val get_current_formula: T -> term end @@ -15,5 +16,11 @@ (**) type T = Ctree.state +fun get_current_formula (pt, (p, p_)) = + case p_ of + Pos.Frm => Ctree.get_obj Ctree.g_form pt p + | Pos.Res => (fst o (Ctree.get_obj Ctree.g_result pt)) p + | _ => Rule.e_term (*on PblObj is fo <> ifo*); + (**)end(**) diff -r 566d1b41dd55 -r 06a5cfe04223 src/Tools/isac/MathEngBasic/tactic.sml --- a/src/Tools/isac/MathEngBasic/tactic.sml Wed Apr 01 14:14:46 2020 +0200 +++ b/src/Tools/isac/MathEngBasic/tactic.sml Wed Apr 01 18:54:03 2020 +0200 @@ -26,7 +26,7 @@ | Check_elementwise' of term * Rule.cterm' * Selem.result | Del_Find' of Rule.cterm' | Del_Given' of Rule.cterm' | Del_Relation' of Rule.cterm' - | Derive' of Rule.rls + | Derive' of Rule.rls | Detail_Set' of Rule.theory' * bool * Rule.rls * term * Selem.result | Detail_Set_Inst' of Rule.theory' * bool * Rule.subst * Rule.rls * term * Selem.result | End_Detail' of Selem.result diff -r 566d1b41dd55 -r 06a5cfe04223 src/Tools/isac/ProgLang/Prog_Tac.thy --- a/src/Tools/isac/ProgLang/Prog_Tac.thy Wed Apr 01 14:14:46 2020 +0200 +++ b/src/Tools/isac/ProgLang/Prog_Tac.thy Wed Apr 01 18:54:03 2020 +0200 @@ -58,7 +58,7 @@ signature PROGAM_TACTIC = sig val dest_spec : term -> Celem.spec - val get_first : 'a -> term -> term option (*TODO rename get_first*) + val get_first_argument : term -> term option (*TODO rename get_first_argument*) val eval_leaf: Env.T -> term option -> term -> term -> Program.leaf * term option val is: term -> bool (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *) @@ -80,47 +80,47 @@ | dest_spec t = raise TERM ("dest_spec: called with ", [t]) (* get argument of first Prog_Tac in a progam for implicit_take *) -fun get_first thy (_ $ body) = +fun get_first_argument (_ $ body) = let (* entries occur twice, for form curried by #> or non-curried *) - fun get_t y (Const ("Tactical.Chain",_) $ e1 $ e2) a = - (case get_t y e1 a of NONE => get_t y e2 a | la => la) - | get_t y (Const ("Tactical.Chain",_) $ e1 $ e2 $ a) _ = - (case get_t y e1 a of NONE => get_t y e2 a | la => la) - | get_t y (Const ("Tactical.Try",_) $ e) a = get_t y e a - | get_t y (Const ("Tactical.Try",_) $ e $ a) _ = get_t y e a - | get_t y (Const ("Tactical.Repeat",_) $ e) a = get_t y e a - | get_t y (Const ("Tactical.Repeat",_) $ e $ a) _ = get_t y e a - | get_t y (Const ("Tactical.Or",_) $e1 $ e2) a = - (case get_t y e1 a of NONE => get_t y e2 a | la => la) - | get_t y (Const ("Tactical.Or",_) $e1 $ e2 $ a) _ = - (case get_t y e1 a of NONE => get_t y e2 a | la => la) - | get_t y (Const ("Tactical.While",_) $ _ $ e) a = get_t y e a - | get_t y (Const ("Tactical.While",_) $ _ $ e $ a) _ = get_t y e a - | get_t y (Const ("Tactical.Letpar",_) $ e1 $ Abs (_, _, e2)) a = - (case get_t y e1 a of NONE => get_t y e2 a | la => la) - | get_t y (Const ("HOL.Let",_) $ e1 $ Abs (_, _, _)) a = - get_t y e1 a (* don't go deeper without evaluation *) - | get_t _ (Const ("If", _) $ _ $ _ $ _) _ = NONE + fun get_t (Const ("Tactical.Chain",_) $ e1 $ e2) a = + (case get_t e1 a of NONE => get_t e2 a | la => la) + | get_t (Const ("Tactical.Chain",_) $ e1 $ e2 $ a) _ = + (case get_t e1 a of NONE => get_t e2 a | la => la) + | get_t (Const ("Tactical.Try",_) $ e) a = get_t e a + | get_t (Const ("Tactical.Try",_) $ e $ a) _ = get_t e a + | get_t (Const ("Tactical.Repeat",_) $ e) a = get_t e a + | get_t (Const ("Tactical.Repeat",_) $ e $ a) _ = get_t e a + | get_t (Const ("Tactical.Or",_) $e1 $ e2) a = + (case get_t e1 a of NONE => get_t e2 a | la => la) + | get_t (Const ("Tactical.Or",_) $e1 $ e2 $ a) _ = + (case get_t e1 a of NONE => get_t e2 a | la => la) + | get_t (Const ("Tactical.While",_) $ _ $ e) a = get_t e a + | get_t (Const ("Tactical.While",_) $ _ $ e $ a) _ = get_t e a + | get_t (Const ("Tactical.Letpar",_) $ e1 $ Abs (_, _, e2)) a = + (case get_t e1 a of NONE => get_t e2 a | la => la) + | get_t (Const ("HOL.Let",_) $ e1 $ Abs (_, _, _)) a = + get_t e1 a (* don't go deeper without evaluation *) + | get_t (Const ("If", _) $ _ $ _ $ _) _ = NONE - | get_t _ (Const ("Prog_Tac.Rewrite",_) $ _ $ a) _ = SOME a - | get_t _ (Const ("Prog_Tac.Rewrite",_) $ _ ) a = SOME a - | get_t _ (Const ("Prog_Tac.Rewrite'_Inst",_) $ _ $ _ $ a) _ = SOME a - | get_t _ (Const ("Prog_Tac.Rewrite'_Inst",_) $ _ $ _ ) a = SOME a - | get_t _ (Const ("Prog_Tac.Rewrite'_Set",_) $ _ $ a) _ = SOME a - | get_t _ (Const ("Prog_Tac.Rewrite'_Set",_) $ _ ) a = SOME a - | get_t _ (Const ("Prog_Tac.Rewrite'_Set'_Inst",_) $ _ $ _ $a)_ =SOME a - | get_t _ (Const ("Prog_Tac.Rewrite'_Set'_Inst",_) $ _ $ _ ) a =SOME a - | get_t _ (Const ("Prog_Tac.Calculate",_) $ _ $ a) _ = SOME a - | get_t _ (Const ("Prog_Tac.Calculate",_) $ _ ) a = SOME a - | get_t _ (Const ("Prog_Tac.Substitute",_) $ _ $ a) _ = SOME a - | get_t _ (Const ("Prog_Tac.Substitute",_) $ _ ) a = SOME a + | get_t (Const ("Prog_Tac.Rewrite",_) $ _ $ a) _ = SOME a + | get_t (Const ("Prog_Tac.Rewrite",_) $ _ ) a = SOME a + | get_t (Const ("Prog_Tac.Rewrite'_Inst",_) $ _ $ _ $ a) _ = SOME a + | get_t (Const ("Prog_Tac.Rewrite'_Inst",_) $ _ $ _ ) a = SOME a + | get_t (Const ("Prog_Tac.Rewrite'_Set",_) $ _ $ a) _ = SOME a + | get_t (Const ("Prog_Tac.Rewrite'_Set",_) $ _ ) a = SOME a + | get_t (Const ("Prog_Tac.Rewrite'_Set'_Inst",_) $ _ $ _ $a)_ =SOME a + | get_t (Const ("Prog_Tac.Rewrite'_Set'_Inst",_) $ _ $ _ ) a =SOME a + | get_t (Const ("Prog_Tac.Calculate",_) $ _ $ a) _ = SOME a + | get_t (Const ("Prog_Tac.Calculate",_) $ _ ) a = SOME a + | get_t (Const ("Prog_Tac.Substitute",_) $ _ $ a) _ = SOME a + | get_t (Const ("Prog_Tac.Substitute",_) $ _ ) a = SOME a - | get_t _ (Const ("Prog_Tac.SubProblem",_) $ _ $ _) _ = NONE + | get_t (Const ("Prog_Tac.SubProblem",_) $ _ $ _) _ = NONE - | get_t _ _ _ = ((*tracing ("### get_t yac: list-expr "^(term2str x));*) NONE) - in get_t thy body Rule.e_term end - | get_first _ t = error ("get_first: no fun-def. for " ^ Rule.term2str t); + | get_t _ _ = ((*tracing ("### get_t yac: list-expr "^(term2str x));*) NONE) + in get_t body Rule.e_term end + | get_first_argument t = error ("get_first_argument: no fun-def. for " ^ Rule.term2str t); (* substitute the Istate.T's environment to a leaf of the program and attach the curried argument of a tactic, if any. diff -r 566d1b41dd55 -r 06a5cfe04223 src/Tools/isac/TODO.thy --- a/src/Tools/isac/TODO.thy Wed Apr 01 14:14:46 2020 +0200 +++ b/src/Tools/isac/TODO.thy Wed Apr 01 18:54:03 2020 +0200 @@ -54,12 +54,12 @@ \item xxx \item xxx \item clarify Tactic.Subproblem (domID, pblID) as term in Pstate {act_arg, ...} - there it is Free ("Subproblem", "char list \ .. - instead of Const (|???.Subproblem", "char list \ .. - AND THE STRING REPRESENTATION IS STRANGE: - Subproblem (''Test'', - ??.\ <^const> String.char.Char ''LINEAR'' ''univariate'' ''equation'' - ''test'') + there it is Free ("Subproblem", "char list \ .. + instead of Const (|???.Subproblem", "char list \ .. + AND THE STRING REPRESENTATION IS STRANGE: + Subproblem (''Test'', + ??.\ <^const> String.char.Char ''LINEAR'' ''univariate'' ''equation'' + ''test'') ML \ \ ML \ term2str; (*defined by..*) @@ -266,7 +266,7 @@ \item xxx \end{itemize} \item xxx - \item Prog_Tac: fun get_first takes both Prog_Tac + Program --- wait for separate Tactical + \item Prog_Tac: fun get_first_argument takes both Prog_Tac + Program --- wait for separate Tactical then shift into common descendant \item xxx \end{itemize} @@ -385,7 +385,6 @@ \item xxx \item xxx \item in locate_input_tactic .. ?scan_dn1?; Program.is_eval_expr .use Term.exists_Const - \item locate_input_tactic: get_simplifier cstate (*TODO: shift to init_istate*) \item push srls into pstate \item lucas-intrpreter.locate_input_tactic: scan_to_tactic1 srls tac cstate (progr, Rule.e_rls) ^^^^^^^^^^ @@ -570,7 +569,8 @@ section \Questions to Isabelle experts\ text \ \begin{itemize} -\item ad ERROR @unknown fact all_left in Test_Isac +\item ad ERROR Undefined fact "all_left" in Test_Isac: error-pattern.sml + Undefined fact: "xfoldr_Nil" inssort.sml \item xxx \item xxx \item ?OK Test_Isac_Short with diff -r 566d1b41dd55 -r 06a5cfe04223 test/Tools/isac/Interpret/li-tool.sml --- a/test/Tools/isac/Interpret/li-tool.sml Wed Apr 01 14:14:46 2020 +0200 +++ b/test/Tools/isac/Interpret/li-tool.sml Wed Apr 01 18:54:03 2020 +0200 @@ -6,14 +6,14 @@ "table of contents -----------------------------------------------"; "-----------------------------------------------------------------"; "----------- fun specific_from_prog ----------------------------"; -"----------- fun implicit_take, fun get_first -------------------------"; +"----------- fun implicit_take, fun get_first_argument -------------------------"; "----------- fun from_prog ---------------------------------------"; "----------- fun specific_from_prog ----------------------------"; "----------- fun de_esc_underscore -------------------------------"; "----------- fun go ----------------------------------------------"; "----------- fun formal_args -------------------------------------"; "----------- fun dsc_valT ----------------------------------------"; -"----------- fun itms2args ---------------------------------------"; +"----------- fun arguments_from_model ---------------------------------------"; "----------- fun init_pstate -----------------------------------------------------------------"; "-----------------------------------------------------------------"; "-----------------------------------------------------------------"; @@ -88,9 +88,9 @@ autoCalculate 1 CompleteCalc; (* ONE ERROR *) ==============================^^^^^^^^^^^^^*) -"----------- fun implicit_take, fun get_first -------------------------"; -"----------- fun implicit_take, fun get_first -------------------------"; -"----------- fun implicit_take, fun get_first -------------------------"; +"----------- fun implicit_take, fun get_first_argument -------------------------"; +"----------- fun implicit_take, fun get_first_argument -------------------------"; +"----------- fun implicit_take, fun get_first_argument -------------------------"; val fmz = ["equality (x+1=(2::real))", "solveFor x", "solutions L"]; val (dI',pI',mI') = ("Test",["sqroot-test","univariate","equation","test"], ["Test","squ-equ-test-subpbl1"]); @@ -115,10 +115,10 @@ val thy = assoc_thy thy'; val srls = LItool.get_simplifier (pt, pos) val (is as Pstate {env, ...}, ctxt, sc) = init_pstate srls ctxt itms mI; -val ini = implicit_take thy sc env; +val ini = implicit_take sc env; "----- fun implicit_take, args:"; val (Prog sc) = sc; -"----- fun get_first, args:"; val (y, h $ body) = (thy, sc); -case get_first thy sc of SOME (Free ("e_e", _)) => () +"----- fun get_first_argument, args:"; val (y, h $ body) = (thy, sc); +case get_first_argument sc of SOME (Free ("e_e", _)) => () | _ => error "script: Const (?, ?) in script (as term) changed";; "----------- fun from_prog ---------------------------------------"; @@ -273,14 +273,14 @@ val T = "bool List.list => Tools.nam" : typ > val dsc = dsc_valT t; val dsc = "nam" : string*) -"----------- fun itms2args ---------------------------------------"; -"----------- fun itms2args ---------------------------------------"; -"----------- fun itms2args ---------------------------------------"; +"----------- fun arguments_from_model ---------------------------------------"; +"----------- fun arguments_from_model ---------------------------------------"; +"----------- fun arguments_from_model ---------------------------------------"; (* > val sc = ... Solve_root_equation ... > val mI = ("Program","sqrt-equ-test"); > val PblObj{meth={ppc=itms,...},...} = get_obj I pt []; -> val ts = itms2args thy mI itms; +> val ts = arguments_from_model thy mI itms; > map (term_to_string''' thy) ts; ["sqrt (#9 + #4 * x) = sqrt x + sqrt (#5 + x)","x","#0"] : string list *) diff -r 566d1b41dd55 -r 06a5cfe04223 test/Tools/isac/Interpret/lucas-interpreter.sml --- a/test/Tools/isac/Interpret/lucas-interpreter.sml Wed Apr 01 14:14:46 2020 +0200 +++ b/test/Tools/isac/Interpret/lucas-interpreter.sml Wed Apr 01 18:54:03 2020 +0200 @@ -54,7 +54,7 @@ (is as Istate.Pstate {env, ...}, ctxt, sc) => (is, env, ctxt, sc) | _ => error "solve Apply_Method: uncovered case init_pstate"; (*+*)pstate2str (the_pstate is) = "([\"\n(f_f, x ^^^ 2 + 1)\",\"\n(v_v, x)\"], [], e_rls, NONE, \n??.empty, ORundef, false, true)"; - val ini = LItool.implicit_take thy sc env; + val ini = LItool.implicit_take sc env; val p = lev_dn p; val NONE = (*case*) ini (*of*); diff -r 566d1b41dd55 -r 06a5cfe04223 test/Tools/isac/Interpret/rewtools.sml --- a/test/Tools/isac/Interpret/rewtools.sml Wed Apr 01 14:14:46 2020 +0200 +++ b/test/Tools/isac/Interpret/rewtools.sml Wed Apr 01 18:54:03 2020 +0200 @@ -350,16 +350,16 @@ "----------- fun is_contained_in ------------------------"; "----------- fun is_contained_in ------------------------"; val r1 = Thm ("real_diff_minus",num_str @{thm real_diff_minus}); -if contains_rule r1 Test_simplify then () -else error "rewtools.sml contains_rule Thm"; +if Rule.contains_rule r1 Test_simplify then () +else error "rewtools.sml Rule.contains_rule Thm"; val r1 = Num_Calc ("Groups.plus_class.plus", eval_binop "#add_"); -if contains_rule r1 Test_simplify then () -else error "rewtools.sml contains_rule Num_Calc"; +if Rule.contains_rule r1 Test_simplify then () +else error "rewtools.sml Rule.contains_rule Num_Calc"; val r1 = Num_Calc ("Groups.minus_class.minus", eval_binop "#add_"); -if not (contains_rule r1 Test_simplify) then () -else error "rewtools.sml contains_rule Num_Calc"; +if not (Rule.contains_rule r1 Test_simplify) then () +else error "rewtools.sml Rule.contains_rule Num_Calc"; "----------- build fun get_bdv_subst --------------------------------"; "----------- build fun get_bdv_subst --------------------------------"; diff -r 566d1b41dd55 -r 06a5cfe04223 test/Tools/isac/Knowledge/biegelinie-4.sml --- a/test/Tools/isac/Knowledge/biegelinie-4.sml Wed Apr 01 14:14:46 2020 +0200 +++ b/test/Tools/isac/Knowledge/biegelinie-4.sml Wed Apr 01 18:54:03 2020 +0200 @@ -162,7 +162,7 @@ val (is, env, ctxt, sc) = case LItool.init_pstate srls ctxt itms mI of (is as Istate.Pstate ist, ctxt, sc) => (is, get_env ist, ctxt, sc) | _ => error "Step_Solve.by_tactic Apply_Method: uncovered case init_pstate" - val ini = LItool.implicit_take thy sc env; + val ini = LItool.implicit_take sc env; val p = lev_dn p; val NONE = (*case*) ini (*of*); val (m', (is', ctxt'), _) = LI.find_next_step sc (pt, (p, Res)) is ctxt; @@ -194,11 +194,11 @@ (*----------- 20 -----------*) (*//------------------------------------------------vvv Specify_Method ["Biegelinien", "ausBelastung"]-\\*) (*[1], Pbl*)(*ERROR val (p,_,f,nxt,_,pt) = me nxt''''' p''''' c pt'''''; (*nxt = Apply_Method ["Biegelinien", "ausBelastung"]*) -ERROR itms2args: 'Biegelinie' not in itms*) +ERROR arguments_from_model: 'Biegelinie' not in itms*) (*SubProblem (_, [''vonBelastungZu'', ''Biegelinien''], _) [REAL q, REAL v, REAL_REAL b, REAL_REAL id_abl] - ^^^^^^^^^^^ ..ERROR itms2args: 'Biegelinie' not in itms*) + ^^^^^^^^^^^ ..ERROR arguments_from_model: 'Biegelinie' not in itms*) (*+*)val PblObj {meth, probl, spec = (thy, _ , metID), origin = (oris, _, _), ...} = get_obj I pt''''' (fst p'''''); (*+*)if oris2str oris = (*+*) "[\n(1, [\"1\"], #Given,Streckenlast, [\"q_0\"]),\n(2, [\"1\"], #Given,FunktionsVariable, [\"x\"]),\n(3, [\"1\"], #Find,Funktionen, [\"funs'''\"])]" diff -r 566d1b41dd55 -r 06a5cfe04223 test/Tools/isac/Knowledge/diffapp.sml --- a/test/Tools/isac/Knowledge/diffapp.sml Wed Apr 01 14:14:46 2020 +0200 +++ b/test/Tools/isac/Knowledge/diffapp.sml Wed Apr 01 18:54:03 2020 +0200 @@ -399,7 +399,7 @@ val mits = get_obj g_met pt [];writeln(itms2str_ ctxt mits); (*=== inhibit exn 110722============================================================= -itms2args thy ["DiffApp","max_by_calculus"] mits; +arguments_from_model ["DiffApp","max_by_calculus"] mits; val (p,_,f,nxt,_,pt) = me nxt p c pt; === inhibit exn 110722=============================================================*) diff -r 566d1b41dd55 -r 06a5cfe04223 test/Tools/isac/Minisubpbl/200-start-method.sml --- a/test/Tools/isac/Minisubpbl/200-start-method.sml Wed Apr 01 14:14:46 2020 +0200 +++ b/test/Tools/isac/Minisubpbl/200-start-method.sml Wed Apr 01 18:54:03 2020 +0200 @@ -58,7 +58,7 @@ val ctxt = ctxt |> ContextC.insert_assumptions pres; val (is'''' as Pstate {env = env'''',...}, _, sc'''') = init_pstate srls ctxt meth mI; "~~~~~ fun init_pstate , args:"; val (srls, thy, itms, metID) = (srls, thy, meth, mI) - val actuals = itms2args thy metID itms + val actuals = arguments_from_model metID itms val scr as Prog sc = (#scr o get_met) metID val formals = formal_args sc (*expects same sequence of (actual) args in itms and (formal) args in met*) @@ -98,7 +98,7 @@ val ctxt = ctxt |> ContextC.insert_assumptions pres; "~~~~~ continue Step_Solve.by_tactic"; -val ini = implicit_take thy sc'''' env''''; +val ini = implicit_take sc'''' env''''; val p = lev_dn p; val SOME t = ini; val (pos,c,_,pt) = diff -r 566d1b41dd55 -r 06a5cfe04223 test/Tools/isac/Test_Isac.thy --- a/test/Tools/isac/Test_Isac.thy Wed Apr 01 14:14:46 2020 +0200 +++ b/test/Tools/isac/Test_Isac.thy Wed Apr 01 18:54:03 2020 +0200 @@ -90,7 +90,7 @@ open Kernel; open Math_Engine; open Test_Code; CalcTreeTEST; - open LItool; itms2args; + open LItool; arguments_from_model; open Sub_Problem; open Fetch_Tacs; open Step @@ -179,7 +179,6 @@ ML_file "ProgLang/tactical.sml" ML_file "ProgLang/auto_prog.sml" ML_file "ProgLang/rewrite.sml" - ML_file "ProgLang/tools.sml" (*---------------------- do Minisubpbl before ADDTESTS/All_Ctxt -------------------------------- ---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------*) @@ -247,7 +246,6 @@ ML_file "Knowledge/delete.sml" ML_file "Knowledge/descript.sml" - ML_file "Knowledge/atools.sml" ML_file "Knowledge/simplify.sml" ML_file "Knowledge/poly.sml" ML_file "Knowledge/gcd_poly_ml.sml" diff -r 566d1b41dd55 -r 06a5cfe04223 test/Tools/isac/Test_Isac_Short.thy --- a/test/Tools/isac/Test_Isac_Short.thy Wed Apr 01 14:14:46 2020 +0200 +++ b/test/Tools/isac/Test_Isac_Short.thy Wed Apr 01 18:54:03 2020 +0200 @@ -90,7 +90,7 @@ open Kernel; open Math_Engine; open Test_Code; CalcTreeTEST; - open LItool; itms2args; + open LItool; arguments_from_model; open Sub_Problem; open Fetch_Tacs; open Step @@ -179,7 +179,6 @@ ML_file "ProgLang/tactical.sml" ML_file "ProgLang/auto_prog.sml" ML_file "ProgLang/rewrite.sml" - ML_file "ProgLang/tools.sml" (*---------------------- do Minisubpbl before ADDTESTS/All_Ctxt -------------------------------- ---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------*) @@ -247,7 +246,6 @@ ML_file "Knowledge/delete.sml" ML_file "Knowledge/descript.sml" - ML_file "Knowledge/atools.sml" ML_file "Knowledge/simplify.sml" ML_file "Knowledge/poly.sml" ML_file "Knowledge/gcd_poly_ml.sml" diff -r 566d1b41dd55 -r 06a5cfe04223 test/Tools/isac/Test_Some.thy --- a/test/Tools/isac/Test_Some.thy Wed Apr 01 14:14:46 2020 +0200 +++ b/test/Tools/isac/Test_Some.thy Wed Apr 01 18:54:03 2020 +0200 @@ -10,7 +10,7 @@ open Kernel; open Math_Engine; open Test_Code; CalcTreeTEST; - open LItool; itms2args; + open LItool; arguments_from_model; open Sub_Problem; open Step open Env; diff -r 566d1b41dd55 -r 06a5cfe04223 test/Tools/isac/Test_Some_meld.thy --- a/test/Tools/isac/Test_Some_meld.thy Wed Apr 01 14:14:46 2020 +0200 +++ b/test/Tools/isac/Test_Some_meld.thy Wed Apr 01 18:54:03 2020 +0200 @@ -6,7 +6,7 @@ in case of errors here consider ~~/xtest-to-coding.sh *) open Kernel; open Math_Engine; CalcTreeTEST; - open LItool.; itms2args; + open LItool.; arguments_from_model; open Env; open Exec; open LI; scan_dn;