analogous naming P_Specific .. P_Model
1.1 --- a/src/Tools/isac/BridgeLibisabelle/datatypes.sml Thu May 14 13:48:45 2020 +0200
1.2 +++ b/src/Tools/isac/BridgeLibisabelle/datatypes.sml Thu May 14 14:49:13 2020 +0200
1.3 @@ -424,9 +424,9 @@
1.4 (*XML.Elem (("WHERE", []), wheres), ... Where is never input*)
1.5 XML.Elem (("FIND", []), finds),
1.6 XML.Elem (("RELATE", []), relates)])) =
1.7 - ([Input_Spec.Given (map xml_to_cterm givens),
1.8 - Input_Spec.Find (map xml_to_cterm finds),
1.9 - Input_Spec.Relate (map xml_to_cterm relates)]) : Input_Spec.imodel
1.10 + ([P_Specific.Given (map xml_to_cterm givens),
1.11 + P_Specific.Find (map xml_to_cterm finds),
1.12 + P_Specific.Relate (map xml_to_cterm relates)]) : P_Specific.imodel
1.13 | xml_to_imodel x = raise ERROR ("xml_to_imodel: WRONG arg = " ^ xmlstr 0 x)
1.14 fun xml_to_icalhd
1.15 (XML.Elem (( "ICALCHEAD", []), [
1.16 @@ -436,7 +436,7 @@
1.17 XML.Elem (( "POS", []), [XML.Text belongsto]),
1.18 spec as XML.Elem (( "SPECIFICATION", []), _)])) =
1.19 (xml_to_pos pos, xml_to_term_NEW form |> UnparseC.term, xml_to_imodel imodel,
1.20 - Pos.str2pos_ belongsto, xml_to_spec spec) : Input_Spec.icalhd
1.21 + Pos.str2pos_ belongsto, xml_to_spec spec) : P_Specific.icalhd
1.22 | xml_to_icalhd x = raise ERROR ("xml_to_icalhd: WRONG arg = " ^ xmlstr 0 x)
1.23
1.24 fun xml_of_sub (id, value) =
2.1 --- a/src/Tools/isac/BridgeLibisabelle/interface.sml Thu May 14 13:48:45 2020 +0200
2.2 +++ b/src/Tools/isac/BridgeLibisabelle/interface.sml Thu May 14 14:49:13 2020 +0200
2.3 @@ -31,7 +31,7 @@
2.4 val Iterator : calcID -> XML.tree
2.5 val IteratorTEST : calcID -> iterID
2.6 val modelProblem : calcID -> XML.tree
2.7 - val modifyCalcHead : calcID -> Input_Spec.icalhd -> XML.tree
2.8 + val modifyCalcHead : calcID -> P_Specific.icalhd -> XML.tree
2.9 val moveActiveCalcHead : calcID -> XML.tree
2.10 val moveActiveDown : calcID -> XML.tree
2.11 val moveActiveFormula : calcID -> Pos.pos' -> XML.tree
2.12 @@ -73,12 +73,12 @@
2.13 called for each cterm', icalhd, fmz in this interface;
2.14 + see "fun en/decode" in /mathml.sml *)
2.15 fun encode_imodel imodel =
2.16 - let fun enc (Input_Spec.Given ifos) = Input_Spec.Given (map encode ifos)
2.17 - | enc (Input_Spec.Find ifos) = Input_Spec.Find (map encode ifos)
2.18 - | enc (Input_Spec.Relate ifos) = Input_Spec.Relate (map encode ifos)
2.19 - in map enc imodel:Input_Spec.imodel end;
2.20 -fun encode_icalhd ((pos', headl, imodel, pos_, spec) : Input_Spec.icalhd) =
2.21 - (pos', encode headl, encode_imodel imodel, pos_, spec) : Input_Spec.icalhd;
2.22 + let fun enc (P_Specific.Given ifos) = P_Specific.Given (map encode ifos)
2.23 + | enc (P_Specific.Find ifos) = P_Specific.Find (map encode ifos)
2.24 + | enc (P_Specific.Relate ifos) = P_Specific.Relate (map encode ifos)
2.25 + in map enc imodel:P_Specific.imodel end;
2.26 +fun encode_icalhd ((pos', headl, imodel, pos_, spec) : P_Specific.icalhd) =
2.27 + (pos', encode headl, encode_imodel imodel, pos_, spec) : P_Specific.icalhd;
2.28 fun encode_fmz (ifos, spec) = (map encode ifos, spec);
2.29
2.30
2.31 @@ -288,10 +288,10 @@
2.32 end)
2.33 handle _ => sysERROR2xml cI "error in kernel 8";
2.34
2.35 -fun modifyCalcHead cI (ichd as ((p,_),_,_,_,_) : Input_Spec.icalhd) =
2.36 +fun modifyCalcHead cI (ichd as ((p,_),_,_,_,_) : P_Specific.icalhd) =
2.37 (let
2.38 val ((pt,_),_) = get_calc cI
2.39 - val (pt, chd as (_,p_,_,_,_,_)) = Input_Spec.input_icalhd pt ichd
2.40 + val (pt, chd as (_,p_,_,_,_,_)) = P_Specific.input_icalhd pt ichd
2.41 in (upd_calc cI ((pt, (p,p_)), []); modifycalcheadOK2xml cI chd) end)
2.42 handle _ => sysERROR2xml cI "error in kernel 9";
2.43
3.1 --- a/src/Tools/isac/Interpret/step-solve.sml Thu May 14 13:48:45 2020 +0200
3.2 +++ b/src/Tools/isac/Interpret/step-solve.sml Thu May 14 14:49:13 2020 +0200
3.3 @@ -100,7 +100,7 @@
3.4 if f_succ = f_in
3.5 then ("same-formula", ([], [], (pt, pos))) (* ctree not cut with replaceFormula *)
3.6 else
3.7 - case Input_Spec.cas_input f_in of
3.8 + case P_Specific.cas_input f_in of
3.9 SOME (pt, _) => ("ok", ([], [], (pt, (p, Pos.Met))))
3.10 | NONE =>
3.11 case LI.locate_input_term (pt, pos) f_in of
4.1 --- a/src/Tools/isac/Specify/input-spec.sml Thu May 14 13:48:45 2020 +0200
4.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
4.3 @@ -1,314 +0,0 @@
4.4 -(* Title: Specify/input-calchead.sml
4.5 - Author: Walther Neuper
4.6 - (c) due to copyright terms
4.7 -
4.8 -This will be dropped at switch to Isabelle/PIDE.
4.9 -*)
4.10 -
4.11 -signature INPUT_SPECIFICATION =
4.12 -sig
4.13 - datatype iitem =
4.14 - Find of TermC.as_string list
4.15 - | Given of TermC.as_string list
4.16 - | Relate of TermC.as_string list
4.17 - type imodel = iitem list
4.18 - type icalhd = Pos.pos' * TermC.as_string * imodel * Pos.pos_ * References.T
4.19 - val input_icalhd : Ctree.ctree -> icalhd -> Ctree.ctree * Specification.T
4.20 - val cas_input : term -> (Ctree.ctree * Specification.T) option
4.21 -(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
4.22 - (* NONE *)
4.23 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
4.24 - val appl_add': ThyC.id -> O_Model.T -> I_Model.T -> Model_Pattern.T ->
4.25 - string * TermC.as_string -> I_Model.single
4.26 - val appl_adds: ThyC.id -> O_Model.T -> I_Model.T -> Model_Pattern.T ->
4.27 - (string * TermC.as_string) list -> I_Model.T
4.28 - val cas_input_: References.T -> (term * term list) list ->
4.29 - Problem.id * I_Model.T * Method.id * I_Model.T * Pre_Conds.T * Proof.context
4.30 - val dtss2itm_: Model_Pattern.single list -> term * term list ->
4.31 - int list * bool * string * I_Model.feedback (*I_Model.single'*)
4.32 - val e_icalhd: icalhd
4.33 - val eq7: ''a * ''b -> ''a * (''b * 'c) -> bool
4.34 - val filter_sep: ('a -> bool) -> 'a list -> 'a list * 'a list
4.35 - val flattup2: 'a * ('b * 'c * 'd * 'e) -> 'a * 'b * 'c * 'd * 'e
4.36 - val fstr2itm_: theory -> (''a * (term * term)) list -> ''a * string ->
4.37 - int list * bool * ''a * I_Model.feedback (*I_Model.single'*)
4.38 - val imodel2fstr: iitem list -> (string * TermC.as_string) list
4.39 - val is_Par: 'a * 'b * 'c * 'd * I_Model.feedback -> bool (*I_Model.T?*)
4.40 - val is_casinput: TermC.as_string -> Formalise.T -> bool
4.41 - val is_e_ts: term list -> bool
4.42 - val itms2fstr: I_Model.single -> string * string
4.43 - val par2fstr: I_Model.single -> string * TermC.as_string
4.44 - val parsitm: theory -> I_Model.single -> I_Model.single
4.45 - val unknown_expl: ThyC.id -> (''a * (term * term)) list -> (*Model_Pattern.T?*)
4.46 - (''a * string) list ->
4.47 - (int * int list * bool * ''a * Model_Def.i_model_feedback) list (*I_Model.T?*)
4.48 -( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
4.49 -end
4.50 -
4.51 -(**)
4.52 -structure Input_Spec(**): INPUT_SPECIFICATION(**) =
4.53 -struct
4.54 -(**)
4.55 -
4.56 -(** handle input **)
4.57 -
4.58 -fun dtss2itm_ ppc (d, ts) =
4.59 - let
4.60 - val (f, (d, id)) = the (find_first ((curry op= d) o
4.61 - (#1: (term * term) -> term) o
4.62 - (#2: Model_Pattern.single -> (term * term))) ppc)
4.63 - in
4.64 - ([1], true, f, I_Model.Cor ((d, ts), (id, ts)))
4.65 - end
4.66 -
4.67 -fun flattup2 (a, (b ,c, d, e)) = (a, b, c, d, e)
4.68 -
4.69 -fun cas_input_ ((dI, pI, mI): References.T) dtss = (*WN110515 reconsider thy..ctxt*)
4.70 - let
4.71 - val thy = ThyC.get_theory dI
4.72 - val {ppc, ...} = Problem.from_store pI
4.73 - val its_ = map (dtss2itm_ ppc) dtss (*([1],true,"#Given",Cor (...))*)
4.74 - val its = O_Model.add_id its_
4.75 - val pits = map flattup2 its
4.76 - val (pI, mI) =
4.77 - if mI <> ["no_met"]
4.78 - then (pI, mI)
4.79 - else
4.80 - case Refine.problem thy pI pits of
4.81 - SOME (pI,_) => (pI, (hd o #met o Problem.from_store) pI)
4.82 - | NONE => (pI, (hd o #met o Problem.from_store) pI)
4.83 - val {ppc, pre, prls, ...} = Method.from_store mI
4.84 - val its_ = map (dtss2itm_ ppc) dtss (*([1],true,"#Given",Cor (...))*)
4.85 - val its = O_Model.add_id its_
4.86 - val mits = map flattup2 its
4.87 - val pre = Pre_Conds.check' thy prls pre mits
4.88 - val ctxt = Proof_Context.init_global thy
4.89 - in (pI, pits, mI, mits, pre, ctxt) end;
4.90 -
4.91 -
4.92 -(* check if the input term is a CAScmd and return a ctree with a _complete_ calchead *)
4.93 -fun cas_input hdt =
4.94 - let
4.95 - val (h, argl) = strip_comb hdt
4.96 - in
4.97 - case assoc_cas (ThyC.get_theory "Isac_Knowledge") h of
4.98 - NONE => NONE
4.99 - | SOME (spec as (dI,_,_), argl2dtss) =>
4.100 - let
4.101 - val dtss = argl2dtss argl
4.102 - val (pI, pits, mI, mits, pre, ctxt) = cas_input_ spec dtss
4.103 - val spec = (dI, pI, mI)
4.104 - val (pt,_) = Ctree.cappend_problem Ctree.e_ctree [] (Istate_Def.empty, ContextC.empty)
4.105 - ([], References.empty) ([], References.empty, hdt, ctxt)
4.106 - val pt = Ctree.update_spec pt [] spec
4.107 - val pt = Ctree.update_pbl pt [] pits
4.108 - val pt = Ctree.update_met pt [] mits
4.109 - in
4.110 - SOME (pt, (true, Pos.Met, hdt, mits, pre, spec) : Specification.T)
4.111 - end
4.112 - end
4.113 -
4.114 -
4.115 -(** handle an input calc-head **)
4.116 -
4.117 -datatype iitem =
4.118 - Given of TermC.as_string list
4.119 -(*Where is still not input*)
4.120 -| Find of TermC.as_string list
4.121 -| Relate of TermC.as_string list
4.122 -
4.123 -type imodel = iitem list
4.124 -
4.125 -type icalhd =
4.126 - Pos.pos' * (* the position in Ctree *)
4.127 - TermC.as_string * (* the headline shown on Calc.T *)
4.128 - imodel * (* the model *)
4.129 - Pos.pos_ * (* model belongs to Problem or Method *)
4.130 - References.T; (* into Know_Store *)
4.131 -val e_icalhd = (Pos.e_pos', "", [Given [""]], Pos.Pbl, References.empty)
4.132 -
4.133 -fun is_casinput (hdf : TermC.as_string) ((fmz_, spec) : Formalise.T) =
4.134 - hdf <> "" andalso fmz_ = [] andalso spec = References.empty
4.135 -
4.136 -(* re-parse itms with a new thy and prepare for checking with ori list *)
4.137 -fun parsitm dI (itm as (i, v, _, f, I_Model.Cor ((d, ts), _))) =
4.138 - (let val t = Input_Descript.join (d, ts)
4.139 - val _ = (UnparseC.term_in_thy dI t)
4.140 - (*t his ^^^^^^^^^^^^ should raise the exn on unability of re-parsing dts *)
4.141 - in itm end
4.142 - handle _ => (i, v, false, f, I_Model.Syn (UnparseC.term TermC.empty (*t ..(t) has not been declared*))))
4.143 - | parsitm dI (i, v, b, f, I_Model.Syn str) =
4.144 - (let val _ = (Thm.term_of o the o (TermC.parse dI)) str
4.145 - in (i, v, b ,f, I_Model.Par str) end
4.146 - handle _ => (i, v, b, f, I_Model.Syn str))
4.147 - | parsitm dI (i, v, b, f, I_Model.Typ str) =
4.148 - (let val _ = (Thm.term_of o the o (TermC.parse dI)) str
4.149 - in (i, v, b, f, I_Model.Par str) end
4.150 - handle _ => (i, v, b, f, I_Model.Syn str))
4.151 - | parsitm dI (itm as (i, v, _, f, I_Model.Inc ((d, ts), _))) =
4.152 - (let val t = Input_Descript.join (d,ts);
4.153 - val _ = UnparseC.term_in_thy dI t;
4.154 - (*this ^ should raise the exn on unability of re-parsing dts*)
4.155 - in itm end
4.156 - handle _ => (i, v, false, f, I_Model.Syn (UnparseC.term TermC.empty (*t ..(t) has not been declared*))))
4.157 - | parsitm dI (itm as (i, v, _, f, I_Model.Sup (d, ts))) =
4.158 - (let val t = Input_Descript.join (d,ts);
4.159 - val _ = UnparseC.term_in_thy dI t;
4.160 - (*this ^ should raise the exn on unability of re-parsing dts*)
4.161 - in itm end
4.162 - handle _ => (i, v, false, f, I_Model.Syn (UnparseC.term TermC.empty (*t ..(t) has not been declared*))))
4.163 - | parsitm dI (itm as (i, v, _, f, I_Model.Mis (d, t'))) =
4.164 - (let val t = d $ t';
4.165 - val _ = UnparseC.term_in_thy dI t;
4.166 - (*this ^ should raise the exn on unability of re-parsing dts*)
4.167 - in itm end
4.168 - handle _ => (i, v, false, f, I_Model.Syn (UnparseC.term TermC.empty (*t ..(t) has not been declared*))))
4.169 - | parsitm dI (itm as (_, _, _, _, I_Model.Par _)) =
4.170 - raise ERROR ("parsitm (" ^ I_Model.single_to_string (ThyC.to_ctxt dI) itm ^ "): Par should be internal");
4.171 -
4.172 -(*separate a list to a pair of elements that do NOT satisfy the predicate,
4.173 - and of elements that satisfy the predicate, i.e. (false, true)*)
4.174 -fun filter_sep pred xs =
4.175 - let
4.176 - fun filt ab [] = ab
4.177 - | filt (a, b) (x :: xs) =
4.178 - if pred x
4.179 - then filt (a, b @ [x]) xs
4.180 - else filt (a @ [x], b) xs
4.181 - in filt ([], []) xs end;
4.182 -fun is_Par (_, _, _, _, I_Model.Par _) = true
4.183 - | is_Par _ = false;
4.184 -
4.185 -fun is_e_ts [] = true
4.186 - | is_e_ts [Const ("List.list.Nil", _)] = true
4.187 - | is_e_ts _ = false;
4.188 -
4.189 -(* WN.9.11.03 copied from fun appl_add *)
4.190 -fun appl_add' dI oris ppc pbt (sel, ct) =
4.191 - let
4.192 - val ctxt = ThyC.get_theory dI |> ThyC.to_ctxt;
4.193 - in
4.194 - case TermC.parseNEW ctxt ct of
4.195 - NONE => (0, [], false, sel, I_Model.Syn ct)
4.196 - | SOME t =>
4.197 - (case I_Model.is_known ctxt sel oris t of
4.198 - ("", ori', all) =>
4.199 - (case I_Model.is_notyet_input ctxt ppc all ori' pbt of
4.200 - ("",itm) => itm
4.201 - | (msg,_) => raise ERROR ("appl_add': " ^ msg))
4.202 - | (_, (i, v, _, d, ts), _) =>
4.203 - if is_e_ts ts
4.204 - then (i, v, false, sel, I_Model.Inc ((d, ts), (TermC.empty, [])))
4.205 - else (i, v, false, sel, I_Model.Sup (d, ts)))
4.206 - end
4.207 -
4.208 -(* generate preliminary itm_ from a strin (with field "#Given" etc.) *)
4.209 -fun eq7 (f, d) (f', (d', _)) = f = f' andalso d = d';
4.210 -fun fstr2itm_ thy pbt (f, str) =
4.211 - let
4.212 - val topt = TermC.parse thy str
4.213 - in
4.214 - case topt of
4.215 - NONE => ([], false, f, I_Model.Syn str)
4.216 - | SOME ct =>
4.217 - let
4.218 - val (d, ts) = (Input_Descript.split o Thm.term_of) ct
4.219 - val popt = find_first (eq7 (f, d)) pbt
4.220 - in
4.221 - case popt of
4.222 - NONE => ([1](*??*), true(*??*), f, I_Model.Sup (d, ts))
4.223 - | SOME (f, (d, id)) => ([1], true, f, I_Model.Cor ((d, ts), (id, ts)))
4.224 - end
4.225 - end
4.226 -
4.227 -(*.input into empty PblObj, i.e. empty fmz+origin (unknown example).*)
4.228 -fun unknown_expl dI pbt selcts =
4.229 - let
4.230 - val thy = ThyC.get_theory dI
4.231 - val its_ = map (fstr2itm_ thy pbt) selcts (*([1],true,"#Given",Cor (...))*)
4.232 - val its = O_Model.add_id its_
4.233 - in map flattup2 its end
4.234 -
4.235 -(* WN.11.03 for input_icalhd, ~ specify_additem for Add_Given/_Find/_Relation
4.236 - appl_add': generate 1 item
4.237 - appl_add' . is_known: parse, get data from oris (vats, all (elems if list)..)
4.238 - appl_add' . is_notyet_input: compare with items in model already input
4.239 - insert_ppc': insert this 1 item*)
4.240 -fun appl_adds dI [] _ pbt selcts = unknown_expl dI pbt selcts
4.241 - (*already present itms in model are being overwritten*)
4.242 - | appl_adds _ _ ppc _ [] = ppc
4.243 - | appl_adds dI oris ppc pbt (selct :: ss) =
4.244 - let val itm = appl_add' dI oris ppc pbt selct;
4.245 - in appl_adds dI oris (Specification.insert_ppc' itm ppc) pbt ss end
4.246 -
4.247 -fun par2fstr (_, _, _, f, I_Model.Par s) = (f, s)
4.248 - | par2fstr itm = raise ERROR ("par2fstr: called with " ^ I_Model.single_to_string (ThyC.id_to_ctxt "Isac_Knowledge") itm)
4.249 -fun itms2fstr (_, _, _, f, I_Model.Cor ((d, ts), _)) = (f, Input_Descript.join''' (d, ts))
4.250 - | itms2fstr (_, _, _, f, I_Model.Syn str) = (f, str)
4.251 - | itms2fstr (_, _, _, f, I_Model.Typ str) = (f, str)
4.252 - | itms2fstr (_, _, _, f, I_Model.Inc ((d, ts), _)) = (f, Input_Descript.join''' (d,ts))
4.253 - | itms2fstr (_, _, _, f, I_Model.Sup (d, ts)) = (f, Input_Descript.join''' (d, ts))
4.254 - | itms2fstr (_, _, _, f, I_Model.Mis (d, t)) = (f, UnparseC.term (d $ t))
4.255 - | itms2fstr (itm as (_, _, _, _, I_Model.Par _)) =
4.256 - raise ERROR ("parsitm (" ^ I_Model.single_to_string (ThyC.id_to_ctxt "Isac_Knowledge") itm ^ "): Par should be internal");
4.257 -
4.258 -fun imodel2fstr iitems =
4.259 - let
4.260 - fun xxx is [] = is
4.261 - | xxx is ((Given strs)::iis) = xxx (is @ (map (pair "#Given") strs)) iis
4.262 - | xxx is ((Find strs)::iis) = xxx (is @ (map (pair "#Find") strs)) iis
4.263 - | xxx is ((Relate strs)::iis) = xxx (is @ (map (pair "#Relate") strs)) iis
4.264 - in xxx [] iitems end;
4.265 -
4.266 -(* input a calchead, WN110505 "prep_oris -> (_, ctxt)" not handled properly *)
4.267 -fun input_icalhd pt (((p, _), hdf, imodel, Pos.Pbl, spec as (dI, pI, mI)) : icalhd) =
4.268 - let
4.269 - val (fmz, fmz_, oris, ospec, hdf', sspec, sdI, spI, smI, probl, meth) = case Ctree.get_obj I pt p of
4.270 - Ctree.PblObj {fmz = fmz as (fmz_,_), origin = (oris, ospec, hdf'),
4.271 - spec = sspec as (sdI, spI, smI), probl, meth, ...}
4.272 - => (fmz, fmz_, oris, ospec, hdf', sspec, sdI, spI, smI, probl, meth)
4.273 - | _ => raise ERROR "input_icalhd: uncovered case of get_obj I pt p"
4.274 - in if is_casinput hdf fmz then the (cas_input (TermC.str2term hdf))
4.275 - else (*hacked WN0602 ~~~ ~~~~~~~~~, ..dropped !*)
4.276 - let val (pos_, pits, mits) =
4.277 - if dI <> sdI
4.278 - then let val its = map (parsitm (ThyC.get_theory dI)) probl;
4.279 - val (its, trms) = filter_sep is_Par its;
4.280 - val pbt = (#ppc o Problem.from_store) (#2 (Specification.some_spec ospec sspec))
4.281 - in (Pos.Pbl, appl_adds dI oris its pbt (map par2fstr trms), meth) end
4.282 - else
4.283 - if pI <> spI
4.284 - then if pI = snd3 ospec then (Pos.Pbl, probl, meth)
4.285 - else
4.286 - let val pbt = (#ppc o Problem.from_store) pI
4.287 - val dI' = #1 (Specification.some_spec ospec spec)
4.288 - val oris = if pI = #2 ospec then oris
4.289 - else O_Model.init fmz_(ThyC.get_theory"Isac_Knowledge") pbt(* |> #1*);
4.290 - in (Pos.Pbl, appl_adds dI' oris probl pbt
4.291 - (map itms2fstr probl), meth) end
4.292 - else if mI <> smI (*FIXME.WN0311: what if probl is incomplete?!*)
4.293 - then let val met = (#ppc o Method.from_store) mI
4.294 - val mits = Specification.complete_metitms oris probl meth met
4.295 - in if foldl and_ (true, map #3 mits)
4.296 - then (Pos.Pbl, probl, mits) else (Pos.Met, probl, mits)
4.297 - end
4.298 - else (Pos.Pbl, appl_adds (#1 (Specification.some_spec ospec spec)) oris [(*!!!*)]
4.299 - ((#ppc o Problem.from_store) (#2 (Specification.some_spec ospec spec)))
4.300 - (imodel2fstr imodel), meth)
4.301 - val pt = Ctree.update_spec pt p spec;
4.302 - in if pos_ = Pos.Pbl
4.303 - then let val {prls,where_,...} = Problem.from_store (#2 (Specification.some_spec ospec spec))
4.304 - val pre = Pre_Conds.check' (ThyC.get_theory"Isac_Knowledge") prls where_ pits
4.305 - in (Ctree.update_pbl pt p pits,
4.306 - (Specification.ocalhd_complete pits pre spec, Pos.Pbl, hdf', pits, pre, spec): Specification.T)
4.307 - end
4.308 - else let val {prls,pre,...} = Method.from_store (#3 (Specification.some_spec ospec spec))
4.309 - val pre = Pre_Conds.check' (ThyC.get_theory"Isac_Knowledge") prls pre mits
4.310 - in (Ctree.update_met pt p mits,
4.311 - (Specification.ocalhd_complete mits pre spec, Pos.Met, hdf', mits, pre, spec) : Specification.T)
4.312 - end
4.313 - end
4.314 - end
4.315 - | input_icalhd _ (_, _, _, _(*Met*), _) = raise ERROR "input_icalhd Met not impl."
4.316 -
4.317 -(**)end (**)
4.318 \ No newline at end of file
5.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
5.2 +++ b/src/Tools/isac/Specify/p-specific.sml Thu May 14 14:49:13 2020 +0200
5.3 @@ -0,0 +1,314 @@
5.4 +(* Title: Specify/input-calchead.sml
5.5 + Author: Walther Neuper
5.6 + (c) due to copyright terms
5.7 +
5.8 +This will be dropped at switch to Isabelle/PIDE.
5.9 +*)
5.10 +
5.11 +signature INPUT_SPECIFICATION =
5.12 +sig
5.13 + datatype iitem =
5.14 + Find of TermC.as_string list
5.15 + | Given of TermC.as_string list
5.16 + | Relate of TermC.as_string list
5.17 + type imodel = iitem list
5.18 + type icalhd = Pos.pos' * TermC.as_string * imodel * Pos.pos_ * References.T
5.19 + val input_icalhd : Ctree.ctree -> icalhd -> Ctree.ctree * Specification.T
5.20 + val cas_input : term -> (Ctree.ctree * Specification.T) option
5.21 +(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
5.22 + (* NONE *)
5.23 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
5.24 + val appl_add': ThyC.id -> O_Model.T -> I_Model.T -> Model_Pattern.T ->
5.25 + string * TermC.as_string -> I_Model.single
5.26 + val appl_adds: ThyC.id -> O_Model.T -> I_Model.T -> Model_Pattern.T ->
5.27 + (string * TermC.as_string) list -> I_Model.T
5.28 + val cas_input_: References.T -> (term * term list) list ->
5.29 + Problem.id * I_Model.T * Method.id * I_Model.T * Pre_Conds.T * Proof.context
5.30 + val dtss2itm_: Model_Pattern.single list -> term * term list ->
5.31 + int list * bool * string * I_Model.feedback (*I_Model.single'*)
5.32 + val e_icalhd: icalhd
5.33 + val eq7: ''a * ''b -> ''a * (''b * 'c) -> bool
5.34 + val filter_sep: ('a -> bool) -> 'a list -> 'a list * 'a list
5.35 + val flattup2: 'a * ('b * 'c * 'd * 'e) -> 'a * 'b * 'c * 'd * 'e
5.36 + val fstr2itm_: theory -> (''a * (term * term)) list -> ''a * string ->
5.37 + int list * bool * ''a * I_Model.feedback (*I_Model.single'*)
5.38 + val imodel2fstr: iitem list -> (string * TermC.as_string) list
5.39 + val is_Par: 'a * 'b * 'c * 'd * I_Model.feedback -> bool (*I_Model.T?*)
5.40 + val is_casinput: TermC.as_string -> Formalise.T -> bool
5.41 + val is_e_ts: term list -> bool
5.42 + val itms2fstr: I_Model.single -> string * string
5.43 + val par2fstr: I_Model.single -> string * TermC.as_string
5.44 + val parsitm: theory -> I_Model.single -> I_Model.single
5.45 + val unknown_expl: ThyC.id -> (''a * (term * term)) list -> (*Model_Pattern.T?*)
5.46 + (''a * string) list ->
5.47 + (int * int list * bool * ''a * Model_Def.i_model_feedback) list (*I_Model.T?*)
5.48 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
5.49 +end
5.50 +
5.51 +(**)
5.52 +structure P_Specific(**): INPUT_SPECIFICATION(**) =
5.53 +struct
5.54 +(**)
5.55 +
5.56 +(** handle input **)
5.57 +
5.58 +fun dtss2itm_ ppc (d, ts) =
5.59 + let
5.60 + val (f, (d, id)) = the (find_first ((curry op= d) o
5.61 + (#1: (term * term) -> term) o
5.62 + (#2: Model_Pattern.single -> (term * term))) ppc)
5.63 + in
5.64 + ([1], true, f, I_Model.Cor ((d, ts), (id, ts)))
5.65 + end
5.66 +
5.67 +fun flattup2 (a, (b ,c, d, e)) = (a, b, c, d, e)
5.68 +
5.69 +fun cas_input_ ((dI, pI, mI): References.T) dtss = (*WN110515 reconsider thy..ctxt*)
5.70 + let
5.71 + val thy = ThyC.get_theory dI
5.72 + val {ppc, ...} = Problem.from_store pI
5.73 + val its_ = map (dtss2itm_ ppc) dtss (*([1],true,"#Given",Cor (...))*)
5.74 + val its = O_Model.add_id its_
5.75 + val pits = map flattup2 its
5.76 + val (pI, mI) =
5.77 + if mI <> ["no_met"]
5.78 + then (pI, mI)
5.79 + else
5.80 + case Refine.problem thy pI pits of
5.81 + SOME (pI,_) => (pI, (hd o #met o Problem.from_store) pI)
5.82 + | NONE => (pI, (hd o #met o Problem.from_store) pI)
5.83 + val {ppc, pre, prls, ...} = Method.from_store mI
5.84 + val its_ = map (dtss2itm_ ppc) dtss (*([1],true,"#Given",Cor (...))*)
5.85 + val its = O_Model.add_id its_
5.86 + val mits = map flattup2 its
5.87 + val pre = Pre_Conds.check' thy prls pre mits
5.88 + val ctxt = Proof_Context.init_global thy
5.89 + in (pI, pits, mI, mits, pre, ctxt) end;
5.90 +
5.91 +
5.92 +(* check if the input term is a CAScmd and return a ctree with a _complete_ calchead *)
5.93 +fun cas_input hdt =
5.94 + let
5.95 + val (h, argl) = strip_comb hdt
5.96 + in
5.97 + case assoc_cas (ThyC.get_theory "Isac_Knowledge") h of
5.98 + NONE => NONE
5.99 + | SOME (spec as (dI,_,_), argl2dtss) =>
5.100 + let
5.101 + val dtss = argl2dtss argl
5.102 + val (pI, pits, mI, mits, pre, ctxt) = cas_input_ spec dtss
5.103 + val spec = (dI, pI, mI)
5.104 + val (pt,_) = Ctree.cappend_problem Ctree.e_ctree [] (Istate_Def.empty, ContextC.empty)
5.105 + ([], References.empty) ([], References.empty, hdt, ctxt)
5.106 + val pt = Ctree.update_spec pt [] spec
5.107 + val pt = Ctree.update_pbl pt [] pits
5.108 + val pt = Ctree.update_met pt [] mits
5.109 + in
5.110 + SOME (pt, (true, Pos.Met, hdt, mits, pre, spec) : Specification.T)
5.111 + end
5.112 + end
5.113 +
5.114 +
5.115 +(** handle an input calc-head **)
5.116 +
5.117 +datatype iitem =
5.118 + Given of TermC.as_string list
5.119 +(*Where is still not input*)
5.120 +| Find of TermC.as_string list
5.121 +| Relate of TermC.as_string list
5.122 +
5.123 +type imodel = iitem list
5.124 +
5.125 +type icalhd =
5.126 + Pos.pos' * (* the position in Ctree *)
5.127 + TermC.as_string * (* the headline shown on Calc.T *)
5.128 + imodel * (* the model *)
5.129 + Pos.pos_ * (* model belongs to Problem or Method *)
5.130 + References.T; (* into Know_Store *)
5.131 +val e_icalhd = (Pos.e_pos', "", [Given [""]], Pos.Pbl, References.empty)
5.132 +
5.133 +fun is_casinput (hdf : TermC.as_string) ((fmz_, spec) : Formalise.T) =
5.134 + hdf <> "" andalso fmz_ = [] andalso spec = References.empty
5.135 +
5.136 +(* re-parse itms with a new thy and prepare for checking with ori list *)
5.137 +fun parsitm dI (itm as (i, v, _, f, I_Model.Cor ((d, ts), _))) =
5.138 + (let val t = Input_Descript.join (d, ts)
5.139 + val _ = (UnparseC.term_in_thy dI t)
5.140 + (*t his ^^^^^^^^^^^^ should raise the exn on unability of re-parsing dts *)
5.141 + in itm end
5.142 + handle _ => (i, v, false, f, I_Model.Syn (UnparseC.term TermC.empty (*t ..(t) has not been declared*))))
5.143 + | parsitm dI (i, v, b, f, I_Model.Syn str) =
5.144 + (let val _ = (Thm.term_of o the o (TermC.parse dI)) str
5.145 + in (i, v, b ,f, I_Model.Par str) end
5.146 + handle _ => (i, v, b, f, I_Model.Syn str))
5.147 + | parsitm dI (i, v, b, f, I_Model.Typ str) =
5.148 + (let val _ = (Thm.term_of o the o (TermC.parse dI)) str
5.149 + in (i, v, b, f, I_Model.Par str) end
5.150 + handle _ => (i, v, b, f, I_Model.Syn str))
5.151 + | parsitm dI (itm as (i, v, _, f, I_Model.Inc ((d, ts), _))) =
5.152 + (let val t = Input_Descript.join (d,ts);
5.153 + val _ = UnparseC.term_in_thy dI t;
5.154 + (*this ^ should raise the exn on unability of re-parsing dts*)
5.155 + in itm end
5.156 + handle _ => (i, v, false, f, I_Model.Syn (UnparseC.term TermC.empty (*t ..(t) has not been declared*))))
5.157 + | parsitm dI (itm as (i, v, _, f, I_Model.Sup (d, ts))) =
5.158 + (let val t = Input_Descript.join (d,ts);
5.159 + val _ = UnparseC.term_in_thy dI t;
5.160 + (*this ^ should raise the exn on unability of re-parsing dts*)
5.161 + in itm end
5.162 + handle _ => (i, v, false, f, I_Model.Syn (UnparseC.term TermC.empty (*t ..(t) has not been declared*))))
5.163 + | parsitm dI (itm as (i, v, _, f, I_Model.Mis (d, t'))) =
5.164 + (let val t = d $ t';
5.165 + val _ = UnparseC.term_in_thy dI t;
5.166 + (*this ^ should raise the exn on unability of re-parsing dts*)
5.167 + in itm end
5.168 + handle _ => (i, v, false, f, I_Model.Syn (UnparseC.term TermC.empty (*t ..(t) has not been declared*))))
5.169 + | parsitm dI (itm as (_, _, _, _, I_Model.Par _)) =
5.170 + raise ERROR ("parsitm (" ^ I_Model.single_to_string (ThyC.to_ctxt dI) itm ^ "): Par should be internal");
5.171 +
5.172 +(*separate a list to a pair of elements that do NOT satisfy the predicate,
5.173 + and of elements that satisfy the predicate, i.e. (false, true)*)
5.174 +fun filter_sep pred xs =
5.175 + let
5.176 + fun filt ab [] = ab
5.177 + | filt (a, b) (x :: xs) =
5.178 + if pred x
5.179 + then filt (a, b @ [x]) xs
5.180 + else filt (a @ [x], b) xs
5.181 + in filt ([], []) xs end;
5.182 +fun is_Par (_, _, _, _, I_Model.Par _) = true
5.183 + | is_Par _ = false;
5.184 +
5.185 +fun is_e_ts [] = true
5.186 + | is_e_ts [Const ("List.list.Nil", _)] = true
5.187 + | is_e_ts _ = false;
5.188 +
5.189 +(* WN.9.11.03 copied from fun appl_add *)
5.190 +fun appl_add' dI oris ppc pbt (sel, ct) =
5.191 + let
5.192 + val ctxt = ThyC.get_theory dI |> ThyC.to_ctxt;
5.193 + in
5.194 + case TermC.parseNEW ctxt ct of
5.195 + NONE => (0, [], false, sel, I_Model.Syn ct)
5.196 + | SOME t =>
5.197 + (case I_Model.is_known ctxt sel oris t of
5.198 + ("", ori', all) =>
5.199 + (case I_Model.is_notyet_input ctxt ppc all ori' pbt of
5.200 + ("",itm) => itm
5.201 + | (msg,_) => raise ERROR ("appl_add': " ^ msg))
5.202 + | (_, (i, v, _, d, ts), _) =>
5.203 + if is_e_ts ts
5.204 + then (i, v, false, sel, I_Model.Inc ((d, ts), (TermC.empty, [])))
5.205 + else (i, v, false, sel, I_Model.Sup (d, ts)))
5.206 + end
5.207 +
5.208 +(* generate preliminary itm_ from a strin (with field "#Given" etc.) *)
5.209 +fun eq7 (f, d) (f', (d', _)) = f = f' andalso d = d';
5.210 +fun fstr2itm_ thy pbt (f, str) =
5.211 + let
5.212 + val topt = TermC.parse thy str
5.213 + in
5.214 + case topt of
5.215 + NONE => ([], false, f, I_Model.Syn str)
5.216 + | SOME ct =>
5.217 + let
5.218 + val (d, ts) = (Input_Descript.split o Thm.term_of) ct
5.219 + val popt = find_first (eq7 (f, d)) pbt
5.220 + in
5.221 + case popt of
5.222 + NONE => ([1](*??*), true(*??*), f, I_Model.Sup (d, ts))
5.223 + | SOME (f, (d, id)) => ([1], true, f, I_Model.Cor ((d, ts), (id, ts)))
5.224 + end
5.225 + end
5.226 +
5.227 +(*.input into empty PblObj, i.e. empty fmz+origin (unknown example).*)
5.228 +fun unknown_expl dI pbt selcts =
5.229 + let
5.230 + val thy = ThyC.get_theory dI
5.231 + val its_ = map (fstr2itm_ thy pbt) selcts (*([1],true,"#Given",Cor (...))*)
5.232 + val its = O_Model.add_id its_
5.233 + in map flattup2 its end
5.234 +
5.235 +(* WN.11.03 for input_icalhd, ~ specify_additem for Add_Given/_Find/_Relation
5.236 + appl_add': generate 1 item
5.237 + appl_add' . is_known: parse, get data from oris (vats, all (elems if list)..)
5.238 + appl_add' . is_notyet_input: compare with items in model already input
5.239 + insert_ppc': insert this 1 item*)
5.240 +fun appl_adds dI [] _ pbt selcts = unknown_expl dI pbt selcts
5.241 + (*already present itms in model are being overwritten*)
5.242 + | appl_adds _ _ ppc _ [] = ppc
5.243 + | appl_adds dI oris ppc pbt (selct :: ss) =
5.244 + let val itm = appl_add' dI oris ppc pbt selct;
5.245 + in appl_adds dI oris (Specification.insert_ppc' itm ppc) pbt ss end
5.246 +
5.247 +fun par2fstr (_, _, _, f, I_Model.Par s) = (f, s)
5.248 + | par2fstr itm = raise ERROR ("par2fstr: called with " ^ I_Model.single_to_string (ThyC.id_to_ctxt "Isac_Knowledge") itm)
5.249 +fun itms2fstr (_, _, _, f, I_Model.Cor ((d, ts), _)) = (f, Input_Descript.join''' (d, ts))
5.250 + | itms2fstr (_, _, _, f, I_Model.Syn str) = (f, str)
5.251 + | itms2fstr (_, _, _, f, I_Model.Typ str) = (f, str)
5.252 + | itms2fstr (_, _, _, f, I_Model.Inc ((d, ts), _)) = (f, Input_Descript.join''' (d,ts))
5.253 + | itms2fstr (_, _, _, f, I_Model.Sup (d, ts)) = (f, Input_Descript.join''' (d, ts))
5.254 + | itms2fstr (_, _, _, f, I_Model.Mis (d, t)) = (f, UnparseC.term (d $ t))
5.255 + | itms2fstr (itm as (_, _, _, _, I_Model.Par _)) =
5.256 + raise ERROR ("parsitm (" ^ I_Model.single_to_string (ThyC.id_to_ctxt "Isac_Knowledge") itm ^ "): Par should be internal");
5.257 +
5.258 +fun imodel2fstr iitems =
5.259 + let
5.260 + fun xxx is [] = is
5.261 + | xxx is ((Given strs)::iis) = xxx (is @ (map (pair "#Given") strs)) iis
5.262 + | xxx is ((Find strs)::iis) = xxx (is @ (map (pair "#Find") strs)) iis
5.263 + | xxx is ((Relate strs)::iis) = xxx (is @ (map (pair "#Relate") strs)) iis
5.264 + in xxx [] iitems end;
5.265 +
5.266 +(* input a calchead, WN110505 "prep_oris -> (_, ctxt)" not handled properly *)
5.267 +fun input_icalhd pt (((p, _), hdf, imodel, Pos.Pbl, spec as (dI, pI, mI)) : icalhd) =
5.268 + let
5.269 + val (fmz, fmz_, oris, ospec, hdf', sspec, sdI, spI, smI, probl, meth) = case Ctree.get_obj I pt p of
5.270 + Ctree.PblObj {fmz = fmz as (fmz_,_), origin = (oris, ospec, hdf'),
5.271 + spec = sspec as (sdI, spI, smI), probl, meth, ...}
5.272 + => (fmz, fmz_, oris, ospec, hdf', sspec, sdI, spI, smI, probl, meth)
5.273 + | _ => raise ERROR "input_icalhd: uncovered case of get_obj I pt p"
5.274 + in if is_casinput hdf fmz then the (cas_input (TermC.str2term hdf))
5.275 + else (*hacked WN0602 ~~~ ~~~~~~~~~, ..dropped !*)
5.276 + let val (pos_, pits, mits) =
5.277 + if dI <> sdI
5.278 + then let val its = map (parsitm (ThyC.get_theory dI)) probl;
5.279 + val (its, trms) = filter_sep is_Par its;
5.280 + val pbt = (#ppc o Problem.from_store) (#2 (Specification.some_spec ospec sspec))
5.281 + in (Pos.Pbl, appl_adds dI oris its pbt (map par2fstr trms), meth) end
5.282 + else
5.283 + if pI <> spI
5.284 + then if pI = snd3 ospec then (Pos.Pbl, probl, meth)
5.285 + else
5.286 + let val pbt = (#ppc o Problem.from_store) pI
5.287 + val dI' = #1 (Specification.some_spec ospec spec)
5.288 + val oris = if pI = #2 ospec then oris
5.289 + else O_Model.init fmz_(ThyC.get_theory"Isac_Knowledge") pbt(* |> #1*);
5.290 + in (Pos.Pbl, appl_adds dI' oris probl pbt
5.291 + (map itms2fstr probl), meth) end
5.292 + else if mI <> smI (*FIXME.WN0311: what if probl is incomplete?!*)
5.293 + then let val met = (#ppc o Method.from_store) mI
5.294 + val mits = Specification.complete_metitms oris probl meth met
5.295 + in if foldl and_ (true, map #3 mits)
5.296 + then (Pos.Pbl, probl, mits) else (Pos.Met, probl, mits)
5.297 + end
5.298 + else (Pos.Pbl, appl_adds (#1 (Specification.some_spec ospec spec)) oris [(*!!!*)]
5.299 + ((#ppc o Problem.from_store) (#2 (Specification.some_spec ospec spec)))
5.300 + (imodel2fstr imodel), meth)
5.301 + val pt = Ctree.update_spec pt p spec;
5.302 + in if pos_ = Pos.Pbl
5.303 + then let val {prls,where_,...} = Problem.from_store (#2 (Specification.some_spec ospec spec))
5.304 + val pre = Pre_Conds.check' (ThyC.get_theory"Isac_Knowledge") prls where_ pits
5.305 + in (Ctree.update_pbl pt p pits,
5.306 + (Specification.ocalhd_complete pits pre spec, Pos.Pbl, hdf', pits, pre, spec): Specification.T)
5.307 + end
5.308 + else let val {prls,pre,...} = Method.from_store (#3 (Specification.some_spec ospec spec))
5.309 + val pre = Pre_Conds.check' (ThyC.get_theory"Isac_Knowledge") prls pre mits
5.310 + in (Ctree.update_met pt p mits,
5.311 + (Specification.ocalhd_complete mits pre spec, Pos.Met, hdf', mits, pre, spec) : Specification.T)
5.312 + end
5.313 + end
5.314 + end
5.315 + | input_icalhd _ (_, _, _, _(*Met*), _) = raise ERROR "input_icalhd Met not impl."
5.316 +
5.317 +(**)end (**)
5.318 \ No newline at end of file
6.1 --- a/src/Tools/isac/Specify/specify.sml Thu May 14 13:48:45 2020 +0200
6.2 +++ b/src/Tools/isac/Specify/specify.sml Thu May 14 14:49:13 2020 +0200
6.3 @@ -44,30 +44,31 @@
6.4 (if dI' = ThyC.id_empty andalso dI = ThyC.id_empty then ("dummy", (Pbl, Tactic.Specify_Theory dI'))
6.5 else if pI' = Problem.id_empty andalso pI = Problem.id_empty then ("dummy", (Pbl, Tactic.Specify_Problem pI'))
6.6 else
6.7 - case find_first (is_error o #5) pbl of
6.8 + case find_first (Specification.is_error o #5) pbl of
6.9 SOME (_, _, _, fd, itm_) =>
6.10 - ("dummy", (Pbl, mk_delete (ThyC.get_theory (if dI = ThyC.id_empty then dI' else dI)) fd itm_))
6.11 + ("dummy", (Pbl, Specification.mk_delete (ThyC.get_theory
6.12 + (if dI = ThyC.id_empty then dI' else dI)) fd itm_))
6.13 | NONE =>
6.14 - (case nxt_add (ThyC.get_theory (if dI = ThyC.id_empty then dI' else dI)) oris pbt pbl of
6.15 - SOME (fd, ct') => ("dummy", (Pbl, mk_additem fd ct'))
6.16 + (case Specification.nxt_add (ThyC.get_theory (if dI = ThyC.id_empty then dI' else dI)) oris pbt pbl of
6.17 + SOME (fd, ct') => ("dummy", (Pbl, Specification.mk_additem fd ct'))
6.18 | NONE => (*pbl-items complete*)
6.19 if not preok then ("dummy", (Pbl, Tactic.Refine_Problem pI'))
6.20 else if dI = ThyC.id_empty then ("dummy", (Pbl, Tactic.Specify_Theory dI'))
6.21 else if pI = Problem.id_empty then ("dummy", (Pbl, Tactic.Specify_Problem pI'))
6.22 else if mI = Method.id_empty then ("dummy", (Pbl, Tactic.Specify_Method mI'))
6.23 else
6.24 - case find_first (is_error o #5) met of
6.25 - SOME (_, _, _, fd, itm_) => ("dummy", (Met, mk_delete (ThyC.get_theory dI) fd itm_))
6.26 + case find_first (Specification.is_error o #5) met of
6.27 + SOME (_, _, _, fd, itm_) => ("dummy", (Met, Specification.mk_delete (ThyC.get_theory dI) fd itm_))
6.28 | NONE =>
6.29 - (case nxt_add (ThyC.get_theory dI) oris mpc met of
6.30 - SOME (fd, ct') => ("dummy", (Met, mk_additem fd ct')) (*30.8.01: pre?!?*)
6.31 + (case Specification.nxt_add (ThyC.get_theory dI) oris mpc met of
6.32 + SOME (fd, ct') => ("dummy", (Met, Specification.mk_additem fd ct')) (*30.8.01: pre?!?*)
6.33 | NONE => ("dummy", (Met, Tactic.Apply_Method mI)))))
6.34 | Met =>
6.35 - (case find_first (is_error o #5) met of
6.36 - SOME (_,_,_,fd,itm_) => ("dummy", (Met, mk_delete (ThyC.get_theory (if dI = ThyC.id_empty then dI' else dI)) fd itm_))
6.37 + (case find_first (Specification.is_error o #5) met of
6.38 + SOME (_,_,_,fd,itm_) => ("dummy", (Met, Specification.mk_delete (ThyC.get_theory (if dI = ThyC.id_empty then dI' else dI)) fd itm_))
6.39 | NONE =>
6.40 - case nxt_add (ThyC.get_theory (if dI = ThyC.id_empty then dI' else dI)) oris mpc met of
6.41 - SOME (fd,ct') => ("dummy", (Met, mk_additem fd ct'))
6.42 + case Specification.nxt_add (ThyC.get_theory (if dI = ThyC.id_empty then dI' else dI)) oris mpc met of
6.43 + SOME (fd,ct') => ("dummy", (Met, Specification.mk_additem fd ct'))
6.44 | NONE =>
6.45 (if dI = ThyC.id_empty then ("dummy", (Met, Tactic.Specify_Theory dI'))
6.46 else if pI = Problem.id_empty then ("dummy", (Met, Tactic.Specify_Problem pI'))
7.1 --- a/test/Tools/isac/Interpret/error-pattern.sml Thu May 14 13:48:45 2020 +0200
7.2 +++ b/test/Tools/isac/Interpret/error-pattern.sml Thu May 14 14:49:13 2020 +0200
7.3 @@ -1030,7 +1030,7 @@
7.4 val pos_pred = lev_back' pos
7.5 val f_pred = Ctree.get_curr_formula (pt, pos_pred);
7.6 (*if*) f_pred = f_in; (*else*)
7.7 - val NONE = (*case*) Input_Spec.cas_input f_in (*of*);
7.8 + val NONE = (*case*) P_Specificcas_input f_in (*of*);
7.9 (*old* )val (_, _, metID) = get_obj g_spec pt (par_pblobj pt p)
7.10 (*old*)val {scr = prog, ...} = Method.from_store metID
7.11 (*old*)val istate = get_istate_LI pt pos
8.1 --- a/test/Tools/isac/Interpret/lucas-interpreter.sml Thu May 14 13:48:45 2020 +0200
8.2 +++ b/test/Tools/isac/Interpret/lucas-interpreter.sml Thu May 14 14:49:13 2020 +0200
8.3 @@ -542,7 +542,7 @@
8.4 val f_succ = Ctree.get_curr_formula (pt, pos);
8.5 (*if*) f_succ = f_in (*else*);
8.6 val NONE =
8.7 - (*case*) Input_Spec.cas_input f_in (*of*);
8.8 + (*case*) P_Specificcas_input f_in (*of*);
8.9
8.10 (*old* ) val (_, _, metID) = get_obj g_spec pt (par_pblobj pt p)
8.11 (*old*) val {scr = prog, ...} = Method.from_store metID
9.1 --- a/test/Tools/isac/Minisubpbl/800-append-on-Frm.sml Thu May 14 13:48:45 2020 +0200
9.2 +++ b/test/Tools/isac/Minisubpbl/800-append-on-Frm.sml Thu May 14 14:49:13 2020 +0200
9.3 @@ -101,7 +101,7 @@
9.4 val f_pred = Ctree.get_curr_formula (pt, pos_pred);
9.5 val f_succ = Ctree.get_curr_formula (pt, pos);
9.6 (*if*) f_succ = f_in (*else*);
9.7 - val NONE =(*case*) Input_Spec.cas_input f_in (*of*);
9.8 + val NONE =(*case*) P_Specificcas_input f_in (*of*);
9.9
9.10 (*case*)
9.11 LI.locate_input_term (pt, pos) f_in (*of*);