# HG changeset patch # User Walther Neuper # Date 1589803374 -7200 # Node ID 7431c60c4fcc081b2437a83102c1a949363313a4 # Parent 2adc8406b7462a145f91ac72626a7d7d1fb5ba77 sprep.cleanup Specification, Specify diff -r 2adc8406b746 -r 7431c60c4fcc src/Tools/isac/BridgeLibisabelle/interface.sml --- a/src/Tools/isac/BridgeLibisabelle/interface.sml Mon May 18 11:58:55 2020 +0200 +++ b/src/Tools/isac/BridgeLibisabelle/interface.sml Mon May 18 14:02:54 2020 +0200 @@ -300,17 +300,17 @@ fun resetCalcHead cI = (let val (ptp,_) = get_calc cI - val ptp = Specification.reset_calchead ptp - in (upd_calc cI (ptp, []); modifycalcheadOK2xml cI (Specification.get_ocalhd ptp)) end) + val ptp = Specification.reset ptp + in (upd_calc cI (ptp, []); modifycalcheadOK2xml cI (Specification.get ptp)) end) handle _ => sysERROR2xml cI "error in kernel 10"; (* at the activeFormula insert all the Descriptions in the Model and return a CalcHead; the Descriptions are for user-guidance; the rest of the items are left empty for user-input *) fun modelProblem cI = (let val (ptp, _) = get_calc cI - val ptp = Specification.reset_calchead ptp + val ptp = Specification.reset ptp val (_, _, ptp) = Step_Specify.by_tactic_input Tactic.Model_Problem ptp - in (upd_calc cI (ptp, []); modifycalcheadOK2xml cI (Specification.get_ocalhd ptp)) end) + in (upd_calc cI (ptp, []); modifycalcheadOK2xml cI (Specification.get ptp)) end) handle _ => sysERROR2xml cI "error in kernel 11"; (* set the UContext determined on a knowledgebrowser to the current calc diff -r 2adc8406b746 -r 7431c60c4fcc src/Tools/isac/MathEngine/mathengine-stateless.sml --- a/src/Tools/isac/MathEngine/mathengine-stateless.sml Mon May 18 11:58:55 2020 +0200 +++ b/src/Tools/isac/MathEngine/mathengine-stateless.sml Mon May 18 14:02:54 2020 +0200 @@ -109,7 +109,7 @@ else if member op = [Pos.Pbl, Pos.Met] p_ then - if not (Specification.is_complete_mod (pt, pos)) + if not (Specification.is_complete (pt, pos)) then let val ptp = Specify.finish_phase (pt, pos) (*... auto = 2 | 3 *) in diff -r 2adc8406b746 -r 7431c60c4fcc src/Tools/isac/Specify/i-model.sml --- a/src/Tools/isac/Specify/i-model.sml Mon May 18 11:58:55 2020 +0200 +++ b/src/Tools/isac/Specify/i-model.sml Mon May 18 14:02:54 2020 +0200 @@ -26,6 +26,10 @@ T -> Model_Pattern.T -> TermC.as_string -> additm val add_single: theory -> single -> T -> T +(*/------- to I_Model from Specify -------\*) +(*val make: I_Model.m_field -> TermC.as_string * I_Model.T -> Tactic.T*) + val get_tac: m_field -> TermC.as_string * T -> Tactic.T +(*\------- to I_Model from Specify -------/*) (*/------- rename -------\*) val d_in: feedback -> term val ts_in: feedback -> term list @@ -35,6 +39,7 @@ val is_notyet_input : Proof.context -> T -> term list -> O_Model.single -> ('a * (term * term)) list -> string * single val dsc_unknown: term + val geti_ct: theory -> O_Model.single -> single -> m_field * UnparseC.term_as_string val pbl_ids': term -> term list -> term list val mk_env: T -> (term * term) list @@ -100,6 +105,16 @@ fun to_string ctxt itms = strs2str' (map (linefeed o (single_to_string ctxt)) itms); +(*/------- to I_Model from Specify -------\*) +fun get_tac m_field (term_as_string, i_model) = + case m_field of + "#Given" => Tactic.Add_Given' (term_as_string, i_model) + | "#Find" => Tactic.Add_Find' (term_as_string, i_model) + | "#Relate" => Tactic.Add_Relation'(term_as_string, i_model) + | str => raise ERROR ("specify_additem Frm, Pbl: uncovered case with " ^ str); +(*\------- to I_Model from Specify -------/*) + + (** initialise a model **) fun init pbt = @@ -253,6 +268,12 @@ val dsc_unknown = (Thm.term_of o the o (TermC.parseold @{theory})) "unknown::'a => unknow"; +(* get a term from ori, notyet input in itm. + the term from ori is thrown back to a string in order to reuse + machinery for immediate input by the user. *) +fun geti_ct thy (_, _, _, d, ts) (_, _, _, fd, itm_) = + (fd, ((UnparseC.term_in_thy thy) o Input_Descript.join) (d, subtract op = (ts_in itm_) ts)) + (* 9.5.03 penv postponed: pbl_ids' *) fun pbl_ids' d vs = [Input_Descript.join'''' (d, vs)]; diff -r 2adc8406b746 -r 7431c60c4fcc src/Tools/isac/Specify/o-model.sml --- a/src/Tools/isac/Specify/o-model.sml Mon May 18 11:58:55 2020 +0200 +++ b/src/Tools/isac/Specify/o-model.sml Mon May 18 14:02:54 2020 +0200 @@ -36,6 +36,8 @@ val is_copy_named_generating: Model_Pattern.single -> bool val preoris2str : preori list -> string + val getr_ct: theory -> single -> m_field * UnparseC.term_as_string + (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* ) val add_field: theory -> Model_Pattern.T -> term * 'b -> m_field * descriptor * 'b val add_variants: ('a * ''b * 'c) list -> (int * ('a * ''b * 'c)) list @@ -71,6 +73,10 @@ UnparseC.term t ^ ", " ^ (strs2str o (map UnparseC.term)) ts ^ ")"; val preoris2str = (strs2str' o (map (linefeed o preori2str))); +(* get the first term in ts from ori *) +fun getr_ct thy (_, _, fd, d, ts) = + (fd, ((UnparseC.term_in_thy thy) o Input_Descript.join) (d,[hd ts])) + (** initialise O_Model **) diff -r 2adc8406b746 -r 7431c60c4fcc src/Tools/isac/Specify/p-spec.sml --- a/src/Tools/isac/Specify/p-spec.sml Mon May 18 11:58:55 2020 +0200 +++ b/src/Tools/isac/Specify/p-spec.sml Mon May 18 14:02:54 2020 +0200 @@ -233,12 +233,12 @@ then let val {prls,where_,...} = Problem.from_store (#2 (References.select ospec spec)) val pre = Pre_Conds.check' (ThyC.get_theory"Isac_Knowledge") prls where_ pits in (Ctree.update_pbl pt p pits, - (Specification.ocalhd_complete pits pre spec, Pos.Pbl, hdf', pits, pre, spec): Specification.T) + (Specification.complete pits pre spec, Pos.Pbl, hdf', pits, pre, spec): Specification.T) end else let val {prls,pre,...} = Method.from_store (#3 (References.select ospec spec)) val pre = Pre_Conds.check' (ThyC.get_theory"Isac_Knowledge") prls pre mits in (Ctree.update_met pt p mits, - (Specification.ocalhd_complete mits pre spec, Pos.Met, hdf', mits, pre, spec) : Specification.T) + (Specification.complete mits pre spec, Pos.Met, hdf', mits, pre, spec) : Specification.T) end end end diff -r 2adc8406b746 -r 7431c60c4fcc src/Tools/isac/Specify/specification.sml --- a/src/Tools/isac/Specify/specification.sml Mon May 18 11:58:55 2020 +0200 +++ b/src/Tools/isac/Specify/specification.sml Mon May 18 14:02:54 2020 +0200 @@ -60,68 +60,80 @@ type T = Specification_Def.T -(*val reset: Calc.T -> Calc.T*) - val reset_calchead: Calc.T -> Calc.T -(*val get: Calc.T -> T*) - val get_ocalhd: Calc.T -> T -(*val complete: I_Model.T -> Pre_Conds.T -> ThyC.id * Problem.id * Method.id -> bool*) - val ocalhd_complete: I_Model.T -> Pre_Conds.T -> ThyC.id * Problem.id * Method.id -> bool -(*val is_complete: Calc.T -> bool*) - val is_complete_mod: Calc.T -> bool +(*val reset_calchead: Calc.T -> Calc.T*) + val reset: Calc.T -> Calc.T +(*val get_ocalhd: Calc.T -> T*) + val get: Calc.T -> T +(*val get: Calc.T -> + I_Model.T * O_Model.T * References.T * I_Model.T * References.T * Proof.context*) + val get_data: Calc.T -> + I_Model.T * O_Model.T * References.T * I_Model.T * References.T * Proof.context + +(*/----- delete -----\* ) + val make: I_Model.m_field -> TermC.as_string * I_Model.T -> Tactic.T +( *\----- delete -----/*) + +(*val ocalhd_complete: I_Model.T -> Pre_Conds.T -> ThyC.id * Problem.id * Method.id -> bool*) + val complete: I_Model.T -> Pre_Conds.T -> ThyC.id * Problem.id * Method.id -> bool +(*val is_complete_mod: Calc.T -> bool*) + val is_complete: Calc.T -> bool (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *) (*NONE*) (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* ) - val get: Calc.T -> I_Model.T * O_Model.T * References.T * I_Model.T * References.T * Proof.context - val make: I_Model.m_field -> TermC.as_string * I_Model.T -> Tactic.T ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*) end (**) -structure Specification(** ): SPECIFICATION( **) = +structure Specification(**): SPECIFICATION(**) = struct (**) type T = Specification_Def.T; (* is the calchead complete ? *) -fun ocalhd_complete its pre (dI, pI, mI) = +fun complete its pre (dI, pI, mI) = foldl and_ (true, map #3 (its: I_Model.T)) andalso foldl and_ (true, map #1 (pre: Pre_Conds.T)) andalso dI <> ThyC.id_empty andalso pI <> Problem.id_empty andalso mI <> Method.id_empty +(*/----- delete -----\* ) fun is_parsed (I_Model.Syn _) = false | is_parsed _ = true -(* get the first term in ts from ori *) -fun getr_ct thy (_, _, fd, d, ts) = - (fd, ((UnparseC.term_in_thy thy) o Input_Descript.join) (d,[hd ts])) - (* get a term from ori, notyet input in itm. the term from ori is thrown back to a string in order to reuse machinery for immediate input by the user. *) fun geti_ct thy (_, _, _, d, ts) (_, _, _, fd, itm_) = (fd, ((UnparseC.term_in_thy thy) o Input_Descript.join) (d, subtract op = (I_Model.ts_in itm_) ts)) +( *\----- delete -----/*) +(*/----- delete -----\* ) (* output the headline to a ppc *) fun header p_ pI mI = case p_ of Pos.Pbl => Test_Out.Problem (if pI = Problem.id_empty then [] else pI) | Pos.Met => Test_Out.Method mI | pos => raise ERROR ("header called with "^ Pos.pos_2str pos) +( *\----- delete -----/*) +(** ) fun make m_field (term_as_string, i_model) = case m_field of "#Given" => Tactic.Add_Given' (term_as_string, i_model) | "#Find" => Tactic.Add_Find' (term_as_string, i_model) | "#Relate" => Tactic.Add_Relation'(term_as_string, i_model) | str => raise ERROR ("specify_additem Frm, Pbl: uncovered case with " ^ str); -fun get (pt, (p, _)) = +( **) + +fun get_data (pt, (p, _)) = case Ctree.get_obj I pt p of (Ctree.PblObj {meth, origin = (oris, (dI', pI', mI'), _), probl, spec = (dI, pI, mI), ctxt, ...}) => (meth, oris, (dI', pI', mI'), probl, (dI, pI, mI), ctxt) | _ => raise ERROR "specify_additem: uncovered case of get_obj I pt p"; + +(*/----- delete -----\* ) (* fun tag_form thy (formal, given) = Thm.global_cterm_of thy (((head_of o Thm.term_of) given) $ (Thm.term_of formal)); WN100819 *) fun tag_form thy (formal, given) = @@ -131,18 +143,20 @@ in gf end) handle _ => raise ERROR ("calchead.tag_form: " ^ UnparseC.term_in_thy thy given ^ " .. " ^ UnparseC.term_in_thy thy formal ^ " ..types do not match") +( *\----- delete -----/*) -fun is_complete_mod (pt, pos as (p, Pos.Pbl)) = +fun is_complete (pt, pos as (p, Pos.Pbl)) = if (Ctree.is_pblobj o (Ctree.get_obj I pt)) p then (I_Model.is_complete o (Ctree.get_obj Ctree.g_pbl pt)) p - else raise ERROR ("is_complete_mod: called by PrfObj at " ^ Pos.pos'2str pos) - | is_complete_mod (pt, pos as (p, Pos.Met)) = + else raise ERROR ("is_complete: called by PrfObj at " ^ Pos.pos'2str pos) + | is_complete (pt, pos as (p, Pos.Met)) = if (Ctree.is_pblobj o (Ctree.get_obj I pt)) p then (I_Model.is_complete o (Ctree.get_obj Ctree.g_met pt)) p - else raise ERROR ("is_complete_mod: called by PrfObj at " ^ Pos.pos'2str pos) - | is_complete_mod (_, pos) = - raise ERROR ("is_complete_mod called by " ^ Pos.pos'2str pos ^ " (should be Pbl or Met)") + else raise ERROR ("is_complete: called by PrfObj at " ^ Pos.pos'2str pos) + | is_complete (_, pos) = + raise ERROR ("is_complete called by " ^ Pos.pos'2str pos ^ " (should be Pbl or Met)") +(*/----- delete -----\* ) (** get the formula from a ctree-node **) (* take form+res from PblObj and 1.PrfObj and (PrfObj after PblObj) @@ -157,38 +171,39 @@ fun form p (Ctree.Nd (Ctree.PrfObj {result = (r, _), ...}, _)) = [("stepform", (p, Pos.Res), r)] | form _ _ = raise ERROR "form: uncovered definition" +( *\----- delete -----/*) (* get a calchead from a PblObj-node in the ctree; preconditions must be calculated *) -fun get_ocalhd (pt, (p, Pos.Pbl)) = +fun get (pt, (p, Pos.Pbl)) = let val (ospec, hdf', spec, probl) = case Ctree.get_obj I pt p of Ctree.PblObj {origin = (_, ospec, hdf'), spec, probl,...} => (ospec, hdf', spec, probl) - | _ => raise ERROR "get_ocalhd Pbl: uncovered case get_obj" + | _ => raise ERROR "get Pbl: uncovered case get_obj" val {prls, where_, ...} = Problem.from_store (#2 (References.select ospec spec)) val pre = Pre_Conds.check' (ThyC.get_theory "Isac_Knowledge") prls where_ probl in - (ocalhd_complete probl pre spec, Pos.Pbl, hdf', probl, pre, spec) + (complete probl pre spec, Pos.Pbl, hdf', probl, pre, spec) end - | get_ocalhd (pt, (p, Pos.Met)) = + | get (pt, (p, Pos.Met)) = let val (ospec, hdf', spec, meth) = case Ctree.get_obj I pt p of Ctree.PblObj {origin = (_, ospec, hdf'), spec, meth, ...} => (ospec, hdf', spec, meth) - | _ => raise ERROR "get_ocalhd Met: uncovered case get_obj" + | _ => raise ERROR "get Met: uncovered case get_obj" val {prls, pre, ...} = Method.from_store (#3 (References.select ospec spec)) val pre = Pre_Conds.check' (ThyC.get_theory "Isac_Knowledge") prls pre meth in - (ocalhd_complete meth pre spec, Pos.Met, hdf', meth, pre, spec) + (complete meth pre spec, Pos.Met, hdf', meth, pre, spec) end - | get_ocalhd _ = raise ERROR "get_ocalhd: uncovered definition" + | get _ = raise ERROR "get: uncovered definition" (* at the activeFormula set the Specification to empty and return a CalcHead; the 'origin' remains (for reconstructing all that) *) -fun reset_calchead (pt, (p,_)) = +fun reset (pt, (p,_)) = let val () = case Ctree.get_obj I pt p of Ctree.PblObj _ => () - | _ => raise ERROR "reset_calchead: uncovered case get_obj" + | _ => raise ERROR "reset: uncovered case get_obj" val pt = Ctree.update_pbl pt p [] val pt = Ctree.update_met pt p [] val pt = Ctree.update_spec pt p References.empty diff -r 2adc8406b746 -r 7431c60c4fcc src/Tools/isac/Specify/specify.sml --- a/src/Tools/isac/Specify/specify.sml Mon May 18 11:58:55 2020 +0200 +++ b/src/Tools/isac/Specify/specify.sml Mon May 18 14:02:54 2020 +0200 @@ -6,6 +6,10 @@ val do_all: Calc.T -> Calc.T val finish_phase: Calc.T -> Calc.T +(*/------- to I_Model from Specify -------\* ) +(*val get_tac: I_Model.m_field -> TermC.as_string * I_Model.T -> Tactic.T*) + val make: I_Model.m_field -> TermC.as_string * I_Model.T -> Tactic.T +( *\------- to I_Model from Specify -------/*) val item_to_add': theory -> O_Model.T -> Model_Pattern.T -> I_Model.T -> (Model_Def.m_field * TermC.as_string) option (*TODO: vvvvvvvvvvvvvv unify code*) @@ -23,9 +27,6 @@ structure Specify(**): SPECIFY(**) = struct (**) -open Pos -open Ctree -open Specification (* select an item in oris, notyet input in itms @@ -67,11 +68,11 @@ if icl = [] then case filter_out (test_id (map #1 vits)) vors of [] => NONE - | miss => SOME (getr_ct thy (hd miss)) + | miss => SOME (O_Model.getr_ct thy (hd miss)) else case find_first (test_subset (hd icl)) vors of NONE => raise ERROR "item_to_add': types or dsc DO NOT MATCH BETWEEN fmz --- pbt" - | SOME ori => SOME (geti_ct thy ori (hd icl)) + | SOME ori => SOME (I_Model.geti_ct thy ori (hd icl)) end fun find_next_step (pt, (p, p_)) = @@ -85,8 +86,8 @@ if Ctree.just_created_ pblobj (*by Subproblem*) andalso origin <> Ctree.e_origin then case mI' of - ["no_met"] => ("ok", (Pbl, Tactic.Refine_Tacitly pI')) - | _ => ("ok", (Pbl, Tactic.Model_Problem)) + ["no_met"] => ("ok", (Pos.Pbl, Tactic.Refine_Tacitly pI')) + | _ => ("ok", (Pos.Pbl, Tactic.Model_Problem)) else let val cpI = if pI = Problem.id_empty then pI' else pI; @@ -98,40 +99,40 @@ val mpc = (#ppc o Method.from_store) cmI in case p_ of - Pbl => - (if dI' = ThyC.id_empty andalso dI = ThyC.id_empty then ("dummy", (Pbl, Tactic.Specify_Theory dI')) - else if pI' = Problem.id_empty andalso pI = Problem.id_empty then ("dummy", (Pbl, Tactic.Specify_Problem pI')) + Pos.Pbl => + (if dI' = ThyC.id_empty andalso dI = ThyC.id_empty then ("dummy", (Pos.Pbl, Tactic.Specify_Theory dI')) + else if pI' = Problem.id_empty andalso pI = Problem.id_empty then ("dummy", (Pos.Pbl, Tactic.Specify_Problem pI')) else case find_first (I_Model.is_error o #5) pbl of SOME (_, _, _, fd, itm_) => - ("dummy", (Pbl, P_Model.mk_delete (ThyC.get_theory + ("dummy", (Pos.Pbl, P_Model.mk_delete (ThyC.get_theory (if dI = ThyC.id_empty then dI' else dI)) fd itm_)) | NONE => (case item_to_add' (ThyC.get_theory (if dI = ThyC.id_empty then dI' else dI)) oris pbt pbl of - SOME (fd, ct') => ("dummy", (Pbl, P_Model.mk_additem fd ct')) + SOME (fd, ct') => ("dummy", (Pos.Pbl, P_Model.mk_additem fd ct')) | NONE => (*pbl-items complete*) - if not preok then ("dummy", (Pbl, Tactic.Refine_Problem pI')) - else if dI = ThyC.id_empty then ("dummy", (Pbl, Tactic.Specify_Theory dI')) - else if pI = Problem.id_empty then ("dummy", (Pbl, Tactic.Specify_Problem pI')) - else if mI = Method.id_empty then ("dummy", (Pbl, Tactic.Specify_Method mI')) + if not preok then ("dummy", (Pos.Pbl, Tactic.Refine_Problem pI')) + else if dI = ThyC.id_empty then ("dummy", (Pos.Pbl, Tactic.Specify_Theory dI')) + else if pI = Problem.id_empty then ("dummy", (Pos.Pbl, Tactic.Specify_Problem pI')) + else if mI = Method.id_empty then ("dummy", (Pos.Pbl, Tactic.Specify_Method mI')) else case find_first (I_Model.is_error o #5) met of - SOME (_, _, _, fd, itm_) => ("dummy", (Met, P_Model.mk_delete (ThyC.get_theory dI) fd itm_)) + SOME (_, _, _, fd, itm_) => ("dummy", (Pos.Met, P_Model.mk_delete (ThyC.get_theory dI) fd itm_)) | NONE => (case item_to_add' (ThyC.get_theory dI) oris mpc met of - SOME (fd, ct') => ("dummy", (Met, P_Model.mk_additem fd ct')) (*30.8.01: pre?!?*) - | NONE => ("dummy", (Met, Tactic.Apply_Method mI))))) - | Met => + SOME (fd, ct') => ("dummy", (Pos.Met, P_Model.mk_additem fd ct')) (*30.8.01: pre?!?*) + | NONE => ("dummy", (Pos.Met, Tactic.Apply_Method mI))))) + | Pos.Met => (case find_first (I_Model.is_error o #5) met of - SOME (_,_,_,fd,itm_) => ("dummy", (Met, P_Model.mk_delete (ThyC.get_theory (if dI = ThyC.id_empty then dI' else dI)) fd itm_)) + SOME (_,_,_,fd,itm_) => ("dummy", (Pos.Met, P_Model.mk_delete (ThyC.get_theory (if dI = ThyC.id_empty then dI' else dI)) fd itm_)) | NONE => case item_to_add' (ThyC.get_theory (if dI = ThyC.id_empty then dI' else dI)) oris mpc met of - SOME (fd,ct') => ("dummy", (Met, P_Model.mk_additem fd ct')) + SOME (fd,ct') => ("dummy", (Pos.Met, P_Model.mk_additem fd ct')) | NONE => - (if dI = ThyC.id_empty then ("dummy", (Met, Tactic.Specify_Theory dI')) - else if pI = Problem.id_empty then ("dummy", (Met, Tactic.Specify_Problem pI')) - else if not preok then ("dummy", (Met, Tactic.Specify_Method mI)) - else ("dummy", (Met, Tactic.Apply_Method mI)))) + (if dI = ThyC.id_empty then ("dummy", (Pos.Met, Tactic.Specify_Theory dI')) + else if pI = Problem.id_empty then ("dummy", (Pos.Met, Tactic.Specify_Problem pI')) + else if not preok then ("dummy", (Pos.Met, Tactic.Specify_Method mI)) + else ("dummy", (Pos.Met, Tactic.Apply_Method mI)))) | p_ => raise ERROR ("Specify.find_next_step called with " ^ Pos.pos_2str p_) end end @@ -186,9 +187,18 @@ else (Pos.Met, Tactic.Apply_Method mI))) | find_next_step' p _ _ _ _ _ _ = raise ERROR ("find_next_step': uncovered case with " ^ Pos.pos_2str p) +(*/------- to I_Model from Specify -------\* ) +fun make m_field (term_as_string, i_model) = + case m_field of + "#Given" => Tactic.Add_Given' (term_as_string, i_model) + | "#Find" => Tactic.Add_Find' (term_as_string, i_model) + | "#Relate" => Tactic.Add_Relation'(term_as_string, i_model) + | str => raise ERROR ("specify_additem Frm, Pbl: uncovered case with " ^ str); +( *\------- to I_Model from Specify -------/*) + fun by_tactic' sel ct (pt, pos as (p, Pos.Met)) = let - val (met, oris, (dI', pI', mI'), pbl, (dI, pI, mI), ctxt) = get (pt, pos) + val (met, oris, (dI', pI', mI'), pbl, (dI, pI, mI), ctxt) = Specification.get_data (pt, pos) val thy = if dI = ThyC.id_empty then ThyC.get_theory dI' else ThyC.get_theory dI val cpI = if pI = Problem.id_empty then pI' else pI val cmI = if mI = Method.id_empty then mI' else mI @@ -198,8 +208,9 @@ I_Model.Add itm => (*..union old input *) let val met' = I_Model.add_single thy itm met + val tac' = I_Model.get_tac sel (ct, met') val (p, pt') = - case Specify_Step.add (make sel (ct, met')) (Istate_Def.Uistate, ctxt) (pt, (p, Pos.Met)) of + case Specify_Step.add tac' (Istate_Def.Uistate, ctxt) (pt, (p, Pos.Met)) of ((p, Pos.Met), _, _, pt') => (p, pt') | _ => raise ERROR "by_tactic': uncovered case of generate1" val pre' = Pre_Conds.check' thy prls pre met' @@ -223,7 +234,7 @@ end | by_tactic' sel ct (pt, pos as (p, _(*Frm, Pbl*))) = let - val (met, oris, (dI', pI', mI'), pbl, (dI, pI, mI), ctxt) = get (pt, pos) + val (met, oris, (dI', pI', mI'), pbl, (dI, pI, mI), ctxt) = Specification.get_data (pt, pos) val thy = if dI = ThyC.id_empty then ThyC.get_theory dI' else ThyC.get_theory dI val cpI = if pI = Problem.id_empty then pI' else pI val cmI = if mI = Method.id_empty then mI' else mI @@ -233,8 +244,9 @@ I_Model.Add itm => (*..union old input *) let val pbl' = I_Model.add_single thy itm pbl + val tac' = I_Model.get_tac sel (ct, pbl') val (p, pt') = - case Specify_Step.add (make sel (ct, pbl')) (Istate_Def.Uistate, ctxt) (pt, (p, Pos.Pbl)) of + case Specify_Step.add tac' (Istate_Def.Uistate, ctxt) (pt, (p, Pos.Pbl)) of ((p, Pos.Pbl), _, _, pt') => (p, pt') | _ => raise ERROR "by_tactic': uncovered case of Specify_Step.add" (* only for getting final p_ ..*) diff -r 2adc8406b746 -r 7431c60c4fcc test/Tools/isac/BridgeLibisabelle/use-cases.sml --- a/test/Tools/isac/BridgeLibisabelle/use-cases.sml Mon May 18 11:58:55 2020 +0200 +++ b/test/Tools/isac/BridgeLibisabelle/use-cases.sml Mon May 18 14:02:54 2020 +0200 @@ -153,7 +153,7 @@ (*8*) setNextTactic 1 (Apply_Method ["Test","solve_linear"]); (*ERROR.110620 .. end-of-calculation*) val (ptp as (pt,p), tacis) = get_calc 1; get_pos 1 1; - is_complete_mod ptp; + Specification.is_complete ptp; References.are_complete ptp; (*8*) autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1); (*<---------------------- orig. test code*) diff -r 2adc8406b746 -r 7431c60c4fcc test/Tools/isac/Specify/i-model.sml --- a/test/Tools/isac/Specify/i-model.sml Mon May 18 11:58:55 2020 +0200 +++ b/test/Tools/isac/Specify/i-model.sml Mon May 18 14:02:54 2020 +0200 @@ -45,7 +45,7 @@ Specify.by_tactic' "#Given" ct (pt, p); "~~~~~ fun specify_additem , args:"; val (sel, ct, (pt, pos as (p,_(*Frm, Pbl*)))) = ("#Given", ct, (pt, p)); - val (met, oris, (dI', pI', mI'), pbl, (dI, pI, mI), ctxt) = get (pt, pos) + val (met, oris, (dI', pI', mI'), pbl, (dI, pI, mI), ctxt) = Specification.get_data (pt, pos) val thy = if dI = ThyC.id_empty then ThyC.get_theory dI' else ThyC.get_theory dI val cpI = if pI = Problem.id_empty then pI' else pI val cmI = if mI = Method.id_empty then mI' else mI @@ -101,7 +101,7 @@ (*+*)then () else error "FINAL I_Model CHANGED"; val (p, pt') = - case Specify_Step.add (make sel (ct, pbl')) (Istate.Uistate, ctxt) (pt, (p, Pos.Pbl)) of + case Specify_Step.add (I_Model.get_tac sel (ct, pbl')) (Istate.Uistate, ctxt) (pt, (p, Pos.Pbl)) of ((p, Pbl), _, _, pt') => (p, pt') val pre = Pre_Conds.check' thy prls where_ pbl' val pb = foldl and_ (true, map fst pre)