1.1 --- a/src/Tools/isac/BridgeLibisabelle/interface.sml Mon May 18 11:58:55 2020 +0200
1.2 +++ b/src/Tools/isac/BridgeLibisabelle/interface.sml Mon May 18 14:02:54 2020 +0200
1.3 @@ -300,17 +300,17 @@
1.4 fun resetCalcHead cI =
1.5 (let
1.6 val (ptp,_) = get_calc cI
1.7 - val ptp = Specification.reset_calchead ptp
1.8 - in (upd_calc cI (ptp, []); modifycalcheadOK2xml cI (Specification.get_ocalhd ptp)) end)
1.9 + val ptp = Specification.reset ptp
1.10 + in (upd_calc cI (ptp, []); modifycalcheadOK2xml cI (Specification.get ptp)) end)
1.11 handle _ => sysERROR2xml cI "error in kernel 10";
1.12
1.13 (* at the activeFormula insert all the Descriptions in the Model and return a CalcHead;
1.14 the Descriptions are for user-guidance; the rest of the items are left empty for user-input *)
1.15 fun modelProblem cI =
1.16 (let val (ptp, _) = get_calc cI
1.17 - val ptp = Specification.reset_calchead ptp
1.18 + val ptp = Specification.reset ptp
1.19 val (_, _, ptp) = Step_Specify.by_tactic_input Tactic.Model_Problem ptp
1.20 - in (upd_calc cI (ptp, []); modifycalcheadOK2xml cI (Specification.get_ocalhd ptp)) end)
1.21 + in (upd_calc cI (ptp, []); modifycalcheadOK2xml cI (Specification.get ptp)) end)
1.22 handle _ => sysERROR2xml cI "error in kernel 11";
1.23
1.24 (* set the UContext determined on a knowledgebrowser to the current calc
2.1 --- a/src/Tools/isac/MathEngine/mathengine-stateless.sml Mon May 18 11:58:55 2020 +0200
2.2 +++ b/src/Tools/isac/MathEngine/mathengine-stateless.sml Mon May 18 14:02:54 2020 +0200
2.3 @@ -109,7 +109,7 @@
2.4 else
2.5 if member op = [Pos.Pbl, Pos.Met] p_
2.6 then
2.7 - if not (Specification.is_complete_mod (pt, pos))
2.8 + if not (Specification.is_complete (pt, pos))
2.9 then
2.10 let val ptp = Specify.finish_phase (pt, pos) (*... auto = 2 | 3 *)
2.11 in
3.1 --- a/src/Tools/isac/Specify/i-model.sml Mon May 18 11:58:55 2020 +0200
3.2 +++ b/src/Tools/isac/Specify/i-model.sml Mon May 18 14:02:54 2020 +0200
3.3 @@ -26,6 +26,10 @@
3.4 T -> Model_Pattern.T -> TermC.as_string -> additm
3.5 val add_single: theory -> single -> T -> T
3.6
3.7 +(*/------- to I_Model from Specify -------\*)
3.8 +(*val make: I_Model.m_field -> TermC.as_string * I_Model.T -> Tactic.T*)
3.9 + val get_tac: m_field -> TermC.as_string * T -> Tactic.T
3.10 +(*\------- to I_Model from Specify -------/*)
3.11 (*/------- rename -------\*)
3.12 val d_in: feedback -> term
3.13 val ts_in: feedback -> term list
3.14 @@ -35,6 +39,7 @@
3.15 val is_notyet_input : Proof.context -> T -> term list -> O_Model.single -> ('a * (term * term)) list
3.16 -> string * single
3.17 val dsc_unknown: term
3.18 + val geti_ct: theory -> O_Model.single -> single -> m_field * UnparseC.term_as_string
3.19 val pbl_ids': term -> term list -> term list
3.20
3.21 val mk_env: T -> (term * term) list
3.22 @@ -100,6 +105,16 @@
3.23 fun to_string ctxt itms = strs2str' (map (linefeed o (single_to_string ctxt)) itms);
3.24
3.25
3.26 +(*/------- to I_Model from Specify -------\*)
3.27 +fun get_tac m_field (term_as_string, i_model) =
3.28 + case m_field of
3.29 + "#Given" => Tactic.Add_Given' (term_as_string, i_model)
3.30 + | "#Find" => Tactic.Add_Find' (term_as_string, i_model)
3.31 + | "#Relate" => Tactic.Add_Relation'(term_as_string, i_model)
3.32 + | str => raise ERROR ("specify_additem Frm, Pbl: uncovered case with " ^ str);
3.33 +(*\------- to I_Model from Specify -------/*)
3.34 +
3.35 +
3.36 (** initialise a model **)
3.37
3.38 fun init pbt =
3.39 @@ -253,6 +268,12 @@
3.40
3.41 val dsc_unknown = (Thm.term_of o the o (TermC.parseold @{theory})) "unknown::'a => unknow";
3.42
3.43 +(* get a term from ori, notyet input in itm.
3.44 + the term from ori is thrown back to a string in order to reuse
3.45 + machinery for immediate input by the user. *)
3.46 +fun geti_ct thy (_, _, _, d, ts) (_, _, _, fd, itm_) =
3.47 + (fd, ((UnparseC.term_in_thy thy) o Input_Descript.join) (d, subtract op = (ts_in itm_) ts))
3.48 +
3.49 (* 9.5.03 penv postponed: pbl_ids' *)
3.50 fun pbl_ids' d vs = [Input_Descript.join'''' (d, vs)];
3.51
4.1 --- a/src/Tools/isac/Specify/o-model.sml Mon May 18 11:58:55 2020 +0200
4.2 +++ b/src/Tools/isac/Specify/o-model.sml Mon May 18 14:02:54 2020 +0200
4.3 @@ -36,6 +36,8 @@
4.4 val is_copy_named_generating: Model_Pattern.single -> bool
4.5
4.6 val preoris2str : preori list -> string
4.7 + val getr_ct: theory -> single -> m_field * UnparseC.term_as_string
4.8 +
4.9 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
4.10 val add_field: theory -> Model_Pattern.T -> term * 'b -> m_field * descriptor * 'b
4.11 val add_variants: ('a * ''b * 'c) list -> (int * ('a * ''b * 'c)) list
4.12 @@ -71,6 +73,10 @@
4.13 UnparseC.term t ^ ", " ^ (strs2str o (map UnparseC.term)) ts ^ ")";
4.14 val preoris2str = (strs2str' o (map (linefeed o preori2str)));
4.15
4.16 +(* get the first term in ts from ori *)
4.17 +fun getr_ct thy (_, _, fd, d, ts) =
4.18 + (fd, ((UnparseC.term_in_thy thy) o Input_Descript.join) (d,[hd ts]))
4.19 +
4.20
4.21 (** initialise O_Model **)
4.22
5.1 --- a/src/Tools/isac/Specify/p-spec.sml Mon May 18 11:58:55 2020 +0200
5.2 +++ b/src/Tools/isac/Specify/p-spec.sml Mon May 18 14:02:54 2020 +0200
5.3 @@ -233,12 +233,12 @@
5.4 then let val {prls,where_,...} = Problem.from_store (#2 (References.select ospec spec))
5.5 val pre = Pre_Conds.check' (ThyC.get_theory"Isac_Knowledge") prls where_ pits
5.6 in (Ctree.update_pbl pt p pits,
5.7 - (Specification.ocalhd_complete pits pre spec, Pos.Pbl, hdf', pits, pre, spec): Specification.T)
5.8 + (Specification.complete pits pre spec, Pos.Pbl, hdf', pits, pre, spec): Specification.T)
5.9 end
5.10 else let val {prls,pre,...} = Method.from_store (#3 (References.select ospec spec))
5.11 val pre = Pre_Conds.check' (ThyC.get_theory"Isac_Knowledge") prls pre mits
5.12 in (Ctree.update_met pt p mits,
5.13 - (Specification.ocalhd_complete mits pre spec, Pos.Met, hdf', mits, pre, spec) : Specification.T)
5.14 + (Specification.complete mits pre spec, Pos.Met, hdf', mits, pre, spec) : Specification.T)
5.15 end
5.16 end
5.17 end
6.1 --- a/src/Tools/isac/Specify/specification.sml Mon May 18 11:58:55 2020 +0200
6.2 +++ b/src/Tools/isac/Specify/specification.sml Mon May 18 14:02:54 2020 +0200
6.3 @@ -60,68 +60,80 @@
6.4
6.5 type T = Specification_Def.T
6.6
6.7 -(*val reset: Calc.T -> Calc.T*)
6.8 - val reset_calchead: Calc.T -> Calc.T
6.9 -(*val get: Calc.T -> T*)
6.10 - val get_ocalhd: Calc.T -> T
6.11 -(*val complete: I_Model.T -> Pre_Conds.T -> ThyC.id * Problem.id * Method.id -> bool*)
6.12 - val ocalhd_complete: I_Model.T -> Pre_Conds.T -> ThyC.id * Problem.id * Method.id -> bool
6.13 -(*val is_complete: Calc.T -> bool*)
6.14 - val is_complete_mod: Calc.T -> bool
6.15 +(*val reset_calchead: Calc.T -> Calc.T*)
6.16 + val reset: Calc.T -> Calc.T
6.17 +(*val get_ocalhd: Calc.T -> T*)
6.18 + val get: Calc.T -> T
6.19 +(*val get: Calc.T ->
6.20 + I_Model.T * O_Model.T * References.T * I_Model.T * References.T * Proof.context*)
6.21 + val get_data: Calc.T ->
6.22 + I_Model.T * O_Model.T * References.T * I_Model.T * References.T * Proof.context
6.23 +
6.24 +(*/----- delete -----\* )
6.25 + val make: I_Model.m_field -> TermC.as_string * I_Model.T -> Tactic.T
6.26 +( *\----- delete -----/*)
6.27 +
6.28 +(*val ocalhd_complete: I_Model.T -> Pre_Conds.T -> ThyC.id * Problem.id * Method.id -> bool*)
6.29 + val complete: I_Model.T -> Pre_Conds.T -> ThyC.id * Problem.id * Method.id -> bool
6.30 +(*val is_complete_mod: Calc.T -> bool*)
6.31 + val is_complete: Calc.T -> bool
6.32
6.33 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
6.34 (*NONE*)
6.35 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
6.36 - val get: Calc.T -> I_Model.T * O_Model.T * References.T * I_Model.T * References.T * Proof.context
6.37 - val make: I_Model.m_field -> TermC.as_string * I_Model.T -> Tactic.T
6.38 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
6.39 end
6.40
6.41 (**)
6.42 -structure Specification(** ): SPECIFICATION( **) =
6.43 +structure Specification(**): SPECIFICATION(**) =
6.44 struct
6.45 (**)
6.46
6.47 type T = Specification_Def.T;
6.48
6.49 (* is the calchead complete ? *)
6.50 -fun ocalhd_complete its pre (dI, pI, mI) =
6.51 +fun complete its pre (dI, pI, mI) =
6.52 foldl and_ (true, map #3 (its: I_Model.T)) andalso
6.53 foldl and_ (true, map #1 (pre: Pre_Conds.T)) andalso
6.54 dI <> ThyC.id_empty andalso pI <> Problem.id_empty andalso mI <> Method.id_empty
6.55
6.56 +(*/----- delete -----\* )
6.57 fun is_parsed (I_Model.Syn _) = false
6.58 | is_parsed _ = true
6.59
6.60 -(* get the first term in ts from ori *)
6.61 -fun getr_ct thy (_, _, fd, d, ts) =
6.62 - (fd, ((UnparseC.term_in_thy thy) o Input_Descript.join) (d,[hd ts]))
6.63 -
6.64 (* get a term from ori, notyet input in itm.
6.65 the term from ori is thrown back to a string in order to reuse
6.66 machinery for immediate input by the user. *)
6.67 fun geti_ct thy (_, _, _, d, ts) (_, _, _, fd, itm_) =
6.68 (fd, ((UnparseC.term_in_thy thy) o Input_Descript.join) (d, subtract op = (I_Model.ts_in itm_) ts))
6.69 +( *\----- delete -----/*)
6.70
6.71 +(*/----- delete -----\* )
6.72 (* output the headline to a ppc *)
6.73 fun header p_ pI mI =
6.74 case p_ of
6.75 Pos.Pbl => Test_Out.Problem (if pI = Problem.id_empty then [] else pI)
6.76 | Pos.Met => Test_Out.Method mI
6.77 | pos => raise ERROR ("header called with "^ Pos.pos_2str pos)
6.78 +( *\----- delete -----/*)
6.79
6.80 +(** )
6.81 fun make m_field (term_as_string, i_model) =
6.82 case m_field of
6.83 "#Given" => Tactic.Add_Given' (term_as_string, i_model)
6.84 | "#Find" => Tactic.Add_Find' (term_as_string, i_model)
6.85 | "#Relate" => Tactic.Add_Relation'(term_as_string, i_model)
6.86 | str => raise ERROR ("specify_additem Frm, Pbl: uncovered case with " ^ str);
6.87 -fun get (pt, (p, _)) =
6.88 +( **)
6.89 +
6.90 +fun get_data (pt, (p, _)) =
6.91 case Ctree.get_obj I pt p of
6.92 (Ctree.PblObj {meth, origin = (oris, (dI', pI', mI'), _), probl, spec = (dI, pI, mI), ctxt, ...})
6.93 => (meth, oris, (dI', pI', mI'), probl, (dI, pI, mI), ctxt)
6.94 | _ => raise ERROR "specify_additem: uncovered case of get_obj I pt p";
6.95
6.96 +
6.97 +(*/----- delete -----\* )
6.98 (* fun tag_form thy (formal, given) = Thm.global_cterm_of thy
6.99 (((head_of o Thm.term_of) given) $ (Thm.term_of formal)); WN100819 *)
6.100 fun tag_form thy (formal, given) =
6.101 @@ -131,18 +143,20 @@
6.102 in gf end)
6.103 handle _ => raise ERROR ("calchead.tag_form: " ^ UnparseC.term_in_thy thy given ^
6.104 " .. " ^ UnparseC.term_in_thy thy formal ^ " ..types do not match")
6.105 +( *\----- delete -----/*)
6.106
6.107 -fun is_complete_mod (pt, pos as (p, Pos.Pbl)) =
6.108 +fun is_complete (pt, pos as (p, Pos.Pbl)) =
6.109 if (Ctree.is_pblobj o (Ctree.get_obj I pt)) p
6.110 then (I_Model.is_complete o (Ctree.get_obj Ctree.g_pbl pt)) p
6.111 - else raise ERROR ("is_complete_mod: called by PrfObj at " ^ Pos.pos'2str pos)
6.112 - | is_complete_mod (pt, pos as (p, Pos.Met)) =
6.113 + else raise ERROR ("is_complete: called by PrfObj at " ^ Pos.pos'2str pos)
6.114 + | is_complete (pt, pos as (p, Pos.Met)) =
6.115 if (Ctree.is_pblobj o (Ctree.get_obj I pt)) p
6.116 then (I_Model.is_complete o (Ctree.get_obj Ctree.g_met pt)) p
6.117 - else raise ERROR ("is_complete_mod: called by PrfObj at " ^ Pos.pos'2str pos)
6.118 - | is_complete_mod (_, pos) =
6.119 - raise ERROR ("is_complete_mod called by " ^ Pos.pos'2str pos ^ " (should be Pbl or Met)")
6.120 + else raise ERROR ("is_complete: called by PrfObj at " ^ Pos.pos'2str pos)
6.121 + | is_complete (_, pos) =
6.122 + raise ERROR ("is_complete called by " ^ Pos.pos'2str pos ^ " (should be Pbl or Met)")
6.123
6.124 +(*/----- delete -----\* )
6.125 (** get the formula from a ctree-node **)
6.126 (*
6.127 take form+res from PblObj and 1.PrfObj and (PrfObj after PblObj)
6.128 @@ -157,38 +171,39 @@
6.129 fun form p (Ctree.Nd (Ctree.PrfObj {result = (r, _), ...}, _)) =
6.130 [("stepform", (p, Pos.Res), r)]
6.131 | form _ _ = raise ERROR "form: uncovered definition"
6.132 +( *\----- delete -----/*)
6.133
6.134 (* get a calchead from a PblObj-node in the ctree; preconditions must be calculated *)
6.135 -fun get_ocalhd (pt, (p, Pos.Pbl)) =
6.136 +fun get (pt, (p, Pos.Pbl)) =
6.137 let
6.138 val (ospec, hdf', spec, probl) = case Ctree.get_obj I pt p of
6.139 Ctree.PblObj {origin = (_, ospec, hdf'), spec, probl,...} => (ospec, hdf', spec, probl)
6.140 - | _ => raise ERROR "get_ocalhd Pbl: uncovered case get_obj"
6.141 + | _ => raise ERROR "get Pbl: uncovered case get_obj"
6.142 val {prls, where_, ...} = Problem.from_store (#2 (References.select ospec spec))
6.143 val pre = Pre_Conds.check' (ThyC.get_theory "Isac_Knowledge") prls where_ probl
6.144 in
6.145 - (ocalhd_complete probl pre spec, Pos.Pbl, hdf', probl, pre, spec)
6.146 + (complete probl pre spec, Pos.Pbl, hdf', probl, pre, spec)
6.147 end
6.148 - | get_ocalhd (pt, (p, Pos.Met)) =
6.149 + | get (pt, (p, Pos.Met)) =
6.150 let
6.151 val (ospec, hdf', spec, meth) = case Ctree.get_obj I pt p of
6.152 Ctree.PblObj {origin = (_, ospec, hdf'), spec, meth, ...} => (ospec, hdf', spec, meth)
6.153 - | _ => raise ERROR "get_ocalhd Met: uncovered case get_obj"
6.154 + | _ => raise ERROR "get Met: uncovered case get_obj"
6.155 val {prls, pre, ...} = Method.from_store (#3 (References.select ospec spec))
6.156 val pre = Pre_Conds.check' (ThyC.get_theory "Isac_Knowledge") prls pre meth
6.157 in
6.158 - (ocalhd_complete meth pre spec, Pos.Met, hdf', meth, pre, spec)
6.159 + (complete meth pre spec, Pos.Met, hdf', meth, pre, spec)
6.160 end
6.161 - | get_ocalhd _ = raise ERROR "get_ocalhd: uncovered definition"
6.162 + | get _ = raise ERROR "get: uncovered definition"
6.163
6.164 (* at the activeFormula set the Specification
6.165 to empty and return a CalcHead;
6.166 the 'origin' remains (for reconstructing all that) *)
6.167 -fun reset_calchead (pt, (p,_)) =
6.168 +fun reset (pt, (p,_)) =
6.169 let
6.170 val () = case Ctree.get_obj I pt p of
6.171 Ctree.PblObj _ => ()
6.172 - | _ => raise ERROR "reset_calchead: uncovered case get_obj"
6.173 + | _ => raise ERROR "reset: uncovered case get_obj"
6.174 val pt = Ctree.update_pbl pt p []
6.175 val pt = Ctree.update_met pt p []
6.176 val pt = Ctree.update_spec pt p References.empty
7.1 --- a/src/Tools/isac/Specify/specify.sml Mon May 18 11:58:55 2020 +0200
7.2 +++ b/src/Tools/isac/Specify/specify.sml Mon May 18 14:02:54 2020 +0200
7.3 @@ -6,6 +6,10 @@
7.4 val do_all: Calc.T -> Calc.T
7.5 val finish_phase: Calc.T -> Calc.T
7.6
7.7 +(*/------- to I_Model from Specify -------\* )
7.8 +(*val get_tac: I_Model.m_field -> TermC.as_string * I_Model.T -> Tactic.T*)
7.9 + val make: I_Model.m_field -> TermC.as_string * I_Model.T -> Tactic.T
7.10 +( *\------- to I_Model from Specify -------/*)
7.11 val item_to_add': theory -> O_Model.T -> Model_Pattern.T -> I_Model.T ->
7.12 (Model_Def.m_field * TermC.as_string) option
7.13 (*TODO: vvvvvvvvvvvvvv unify code*)
7.14 @@ -23,9 +27,6 @@
7.15 structure Specify(**): SPECIFY(**) =
7.16 struct
7.17 (**)
7.18 -open Pos
7.19 -open Ctree
7.20 -open Specification
7.21
7.22 (*
7.23 select an item in oris, notyet input in itms
7.24 @@ -67,11 +68,11 @@
7.25 if icl = []
7.26 then case filter_out (test_id (map #1 vits)) vors of
7.27 [] => NONE
7.28 - | miss => SOME (getr_ct thy (hd miss))
7.29 + | miss => SOME (O_Model.getr_ct thy (hd miss))
7.30 else
7.31 case find_first (test_subset (hd icl)) vors of
7.32 NONE => raise ERROR "item_to_add': types or dsc DO NOT MATCH BETWEEN fmz --- pbt"
7.33 - | SOME ori => SOME (geti_ct thy ori (hd icl))
7.34 + | SOME ori => SOME (I_Model.geti_ct thy ori (hd icl))
7.35 end
7.36
7.37 fun find_next_step (pt, (p, p_)) =
7.38 @@ -85,8 +86,8 @@
7.39 if Ctree.just_created_ pblobj (*by Subproblem*) andalso origin <> Ctree.e_origin
7.40 then
7.41 case mI' of
7.42 - ["no_met"] => ("ok", (Pbl, Tactic.Refine_Tacitly pI'))
7.43 - | _ => ("ok", (Pbl, Tactic.Model_Problem))
7.44 + ["no_met"] => ("ok", (Pos.Pbl, Tactic.Refine_Tacitly pI'))
7.45 + | _ => ("ok", (Pos.Pbl, Tactic.Model_Problem))
7.46 else
7.47 let
7.48 val cpI = if pI = Problem.id_empty then pI' else pI;
7.49 @@ -98,40 +99,40 @@
7.50 val mpc = (#ppc o Method.from_store) cmI
7.51 in
7.52 case p_ of
7.53 - Pbl =>
7.54 - (if dI' = ThyC.id_empty andalso dI = ThyC.id_empty then ("dummy", (Pbl, Tactic.Specify_Theory dI'))
7.55 - else if pI' = Problem.id_empty andalso pI = Problem.id_empty then ("dummy", (Pbl, Tactic.Specify_Problem pI'))
7.56 + Pos.Pbl =>
7.57 + (if dI' = ThyC.id_empty andalso dI = ThyC.id_empty then ("dummy", (Pos.Pbl, Tactic.Specify_Theory dI'))
7.58 + else if pI' = Problem.id_empty andalso pI = Problem.id_empty then ("dummy", (Pos.Pbl, Tactic.Specify_Problem pI'))
7.59 else
7.60 case find_first (I_Model.is_error o #5) pbl of
7.61 SOME (_, _, _, fd, itm_) =>
7.62 - ("dummy", (Pbl, P_Model.mk_delete (ThyC.get_theory
7.63 + ("dummy", (Pos.Pbl, P_Model.mk_delete (ThyC.get_theory
7.64 (if dI = ThyC.id_empty then dI' else dI)) fd itm_))
7.65 | NONE =>
7.66 (case item_to_add' (ThyC.get_theory (if dI = ThyC.id_empty then dI' else dI)) oris pbt pbl of
7.67 - SOME (fd, ct') => ("dummy", (Pbl, P_Model.mk_additem fd ct'))
7.68 + SOME (fd, ct') => ("dummy", (Pos.Pbl, P_Model.mk_additem fd ct'))
7.69 | NONE => (*pbl-items complete*)
7.70 - if not preok then ("dummy", (Pbl, Tactic.Refine_Problem pI'))
7.71 - else if dI = ThyC.id_empty then ("dummy", (Pbl, Tactic.Specify_Theory dI'))
7.72 - else if pI = Problem.id_empty then ("dummy", (Pbl, Tactic.Specify_Problem pI'))
7.73 - else if mI = Method.id_empty then ("dummy", (Pbl, Tactic.Specify_Method mI'))
7.74 + if not preok then ("dummy", (Pos.Pbl, Tactic.Refine_Problem pI'))
7.75 + else if dI = ThyC.id_empty then ("dummy", (Pos.Pbl, Tactic.Specify_Theory dI'))
7.76 + else if pI = Problem.id_empty then ("dummy", (Pos.Pbl, Tactic.Specify_Problem pI'))
7.77 + else if mI = Method.id_empty then ("dummy", (Pos.Pbl, Tactic.Specify_Method mI'))
7.78 else
7.79 case find_first (I_Model.is_error o #5) met of
7.80 - SOME (_, _, _, fd, itm_) => ("dummy", (Met, P_Model.mk_delete (ThyC.get_theory dI) fd itm_))
7.81 + SOME (_, _, _, fd, itm_) => ("dummy", (Pos.Met, P_Model.mk_delete (ThyC.get_theory dI) fd itm_))
7.82 | NONE =>
7.83 (case item_to_add' (ThyC.get_theory dI) oris mpc met of
7.84 - SOME (fd, ct') => ("dummy", (Met, P_Model.mk_additem fd ct')) (*30.8.01: pre?!?*)
7.85 - | NONE => ("dummy", (Met, Tactic.Apply_Method mI)))))
7.86 - | Met =>
7.87 + SOME (fd, ct') => ("dummy", (Pos.Met, P_Model.mk_additem fd ct')) (*30.8.01: pre?!?*)
7.88 + | NONE => ("dummy", (Pos.Met, Tactic.Apply_Method mI)))))
7.89 + | Pos.Met =>
7.90 (case find_first (I_Model.is_error o #5) met of
7.91 - SOME (_,_,_,fd,itm_) => ("dummy", (Met, P_Model.mk_delete (ThyC.get_theory (if dI = ThyC.id_empty then dI' else dI)) fd itm_))
7.92 + SOME (_,_,_,fd,itm_) => ("dummy", (Pos.Met, P_Model.mk_delete (ThyC.get_theory (if dI = ThyC.id_empty then dI' else dI)) fd itm_))
7.93 | NONE =>
7.94 case item_to_add' (ThyC.get_theory (if dI = ThyC.id_empty then dI' else dI)) oris mpc met of
7.95 - SOME (fd,ct') => ("dummy", (Met, P_Model.mk_additem fd ct'))
7.96 + SOME (fd,ct') => ("dummy", (Pos.Met, P_Model.mk_additem fd ct'))
7.97 | NONE =>
7.98 - (if dI = ThyC.id_empty then ("dummy", (Met, Tactic.Specify_Theory dI'))
7.99 - else if pI = Problem.id_empty then ("dummy", (Met, Tactic.Specify_Problem pI'))
7.100 - else if not preok then ("dummy", (Met, Tactic.Specify_Method mI))
7.101 - else ("dummy", (Met, Tactic.Apply_Method mI))))
7.102 + (if dI = ThyC.id_empty then ("dummy", (Pos.Met, Tactic.Specify_Theory dI'))
7.103 + else if pI = Problem.id_empty then ("dummy", (Pos.Met, Tactic.Specify_Problem pI'))
7.104 + else if not preok then ("dummy", (Pos.Met, Tactic.Specify_Method mI))
7.105 + else ("dummy", (Pos.Met, Tactic.Apply_Method mI))))
7.106 | p_ => raise ERROR ("Specify.find_next_step called with " ^ Pos.pos_2str p_)
7.107 end
7.108 end
7.109 @@ -186,9 +187,18 @@
7.110 else (Pos.Met, Tactic.Apply_Method mI)))
7.111 | find_next_step' p _ _ _ _ _ _ = raise ERROR ("find_next_step': uncovered case with " ^ Pos.pos_2str p)
7.112
7.113 +(*/------- to I_Model from Specify -------\* )
7.114 +fun make m_field (term_as_string, i_model) =
7.115 + case m_field of
7.116 + "#Given" => Tactic.Add_Given' (term_as_string, i_model)
7.117 + | "#Find" => Tactic.Add_Find' (term_as_string, i_model)
7.118 + | "#Relate" => Tactic.Add_Relation'(term_as_string, i_model)
7.119 + | str => raise ERROR ("specify_additem Frm, Pbl: uncovered case with " ^ str);
7.120 +( *\------- to I_Model from Specify -------/*)
7.121 +
7.122 fun by_tactic' sel ct (pt, pos as (p, Pos.Met)) =
7.123 let
7.124 - val (met, oris, (dI', pI', mI'), pbl, (dI, pI, mI), ctxt) = get (pt, pos)
7.125 + val (met, oris, (dI', pI', mI'), pbl, (dI, pI, mI), ctxt) = Specification.get_data (pt, pos)
7.126 val thy = if dI = ThyC.id_empty then ThyC.get_theory dI' else ThyC.get_theory dI
7.127 val cpI = if pI = Problem.id_empty then pI' else pI
7.128 val cmI = if mI = Method.id_empty then mI' else mI
7.129 @@ -198,8 +208,9 @@
7.130 I_Model.Add itm => (*..union old input *)
7.131 let
7.132 val met' = I_Model.add_single thy itm met
7.133 + val tac' = I_Model.get_tac sel (ct, met')
7.134 val (p, pt') =
7.135 - case Specify_Step.add (make sel (ct, met')) (Istate_Def.Uistate, ctxt) (pt, (p, Pos.Met)) of
7.136 + case Specify_Step.add tac' (Istate_Def.Uistate, ctxt) (pt, (p, Pos.Met)) of
7.137 ((p, Pos.Met), _, _, pt') => (p, pt')
7.138 | _ => raise ERROR "by_tactic': uncovered case of generate1"
7.139 val pre' = Pre_Conds.check' thy prls pre met'
7.140 @@ -223,7 +234,7 @@
7.141 end
7.142 | by_tactic' sel ct (pt, pos as (p, _(*Frm, Pbl*))) =
7.143 let
7.144 - val (met, oris, (dI', pI', mI'), pbl, (dI, pI, mI), ctxt) = get (pt, pos)
7.145 + val (met, oris, (dI', pI', mI'), pbl, (dI, pI, mI), ctxt) = Specification.get_data (pt, pos)
7.146 val thy = if dI = ThyC.id_empty then ThyC.get_theory dI' else ThyC.get_theory dI
7.147 val cpI = if pI = Problem.id_empty then pI' else pI
7.148 val cmI = if mI = Method.id_empty then mI' else mI
7.149 @@ -233,8 +244,9 @@
7.150 I_Model.Add itm => (*..union old input *)
7.151 let
7.152 val pbl' = I_Model.add_single thy itm pbl
7.153 + val tac' = I_Model.get_tac sel (ct, pbl')
7.154 val (p, pt') =
7.155 - case Specify_Step.add (make sel (ct, pbl')) (Istate_Def.Uistate, ctxt) (pt, (p, Pos.Pbl)) of
7.156 + case Specify_Step.add tac' (Istate_Def.Uistate, ctxt) (pt, (p, Pos.Pbl)) of
7.157 ((p, Pos.Pbl), _, _, pt') => (p, pt')
7.158 | _ => raise ERROR "by_tactic': uncovered case of Specify_Step.add"
7.159 (* only for getting final p_ ..*)
8.1 --- a/test/Tools/isac/BridgeLibisabelle/use-cases.sml Mon May 18 11:58:55 2020 +0200
8.2 +++ b/test/Tools/isac/BridgeLibisabelle/use-cases.sml Mon May 18 14:02:54 2020 +0200
8.3 @@ -153,7 +153,7 @@
8.4 (*8*) setNextTactic 1 (Apply_Method ["Test","solve_linear"]);
8.5 (*ERROR.110620 <SETNEXTTACTIC>..<MESSAGE> end-of-calculation*)
8.6 val (ptp as (pt,p), tacis) = get_calc 1; get_pos 1 1;
8.7 - is_complete_mod ptp;
8.8 + Specification.is_complete ptp;
8.9 References.are_complete ptp;
8.10
8.11 (*8*) autoCalculate 1 (Steps 1); refFormula 1 (get_pos 1 1); (*<---------------------- orig. test code*)
9.1 --- a/test/Tools/isac/Specify/i-model.sml Mon May 18 11:58:55 2020 +0200
9.2 +++ b/test/Tools/isac/Specify/i-model.sml Mon May 18 14:02:54 2020 +0200
9.3 @@ -45,7 +45,7 @@
9.4 Specify.by_tactic' "#Given" ct (pt, p);
9.5 "~~~~~ fun specify_additem , args:"; val (sel, ct, (pt, pos as (p,_(*Frm, Pbl*)))) =
9.6 ("#Given", ct, (pt, p));
9.7 - val (met, oris, (dI', pI', mI'), pbl, (dI, pI, mI), ctxt) = get (pt, pos)
9.8 + val (met, oris, (dI', pI', mI'), pbl, (dI, pI, mI), ctxt) = Specification.get_data (pt, pos)
9.9 val thy = if dI = ThyC.id_empty then ThyC.get_theory dI' else ThyC.get_theory dI
9.10 val cpI = if pI = Problem.id_empty then pI' else pI
9.11 val cmI = if mI = Method.id_empty then mI' else mI
9.12 @@ -101,7 +101,7 @@
9.13 (*+*)then () else error "FINAL I_Model CHANGED";
9.14
9.15 val (p, pt') =
9.16 - case Specify_Step.add (make sel (ct, pbl')) (Istate.Uistate, ctxt) (pt, (p, Pos.Pbl)) of
9.17 + case Specify_Step.add (I_Model.get_tac sel (ct, pbl')) (Istate.Uistate, ctxt) (pt, (p, Pos.Pbl)) of
9.18 ((p, Pbl), _, _, pt') => (p, pt')
9.19 val pre = Pre_Conds.check' thy prls where_ pbl'
9.20 val pb = foldl and_ (true, map fst pre)