1.1 --- a/src/Tools/isac/Interpret/lucas-interpreter.sml Sat May 16 14:04:35 2020 +0200
1.2 +++ b/src/Tools/isac/Interpret/lucas-interpreter.sml Sat May 16 16:23:24 2020 +0200
1.3 @@ -504,7 +504,7 @@
1.4 PblObj {meth = itms, origin = (oris, _, _), probl, ...} => (itms, oris, probl)
1.5 | _ => raise ERROR "LI.by_tactic Apply_Method': uncovered case get_obj"
1.6 val {ppc, ...} = Method.from_store mI;
1.7 - val itms = if itms <> [] then itms else Specification.complete_metitms oris probl [] ppc
1.8 + val itms = if itms <> [] then itms else I_Model.complete oris probl [] ppc
1.9 val itms = Step_Specify.hack_until_review_Specify_1 mI itms
1.10 val srls = LItool.get_simplifier (pt, pos)
1.11 val (is, env, ctxt, prog) = case LItool.init_pstate srls ctxt itms mI of
2.1 --- a/src/Tools/isac/MathEngine/me-misc.sml Sat May 16 14:04:35 2020 +0200
2.2 +++ b/src/Tools/isac/MathEngine/me-misc.sml Sat May 16 16:23:24 2020 +0200
2.3 @@ -30,7 +30,7 @@
2.4 val {prls, pre= where_, ...} = Method.from_store metID
2.5 val pre = Pre_Conds.check prls where_ meth 0
2.6 in pre end
2.7 - val allcorrect = Specification.is_complete_mod_ meth andalso foldl and_ (true, (map #1 pre))
2.8 + val allcorrect = I_Model.is_complete meth andalso foldl and_ (true, (map #1 pre))
2.9 in
2.10 Ctree.ModSpec (allcorrect, Pos.Met, hdl, meth, pre, spec)
2.11 end
2.12 @@ -43,7 +43,7 @@
2.13 val {prls, where_, ...} = Problem.from_store pI
2.14 val pre = Pre_Conds.check prls where_ probl 0
2.15 in pre end
2.16 - val allcorrect = Specification.is_complete_mod_ probl andalso foldl and_ (true, (map #1 pre))
2.17 + val allcorrect = I_Model.is_complete probl andalso foldl and_ (true, (map #1 pre))
2.18 in
2.19 Ctree.ModSpec (allcorrect, Pos.Pbl, hdl, probl, pre, spec)
2.20 end
3.1 --- a/src/Tools/isac/Specify/i-model.sml Sat May 16 14:04:35 2020 +0200
3.2 +++ b/src/Tools/isac/Specify/i-model.sml Sat May 16 16:23:24 2020 +0200
3.3 @@ -26,6 +26,7 @@
3.4 T -> Model_Pattern.T -> TermC.as_string -> additm
3.5 val add_single: theory -> single -> T -> T
3.6
3.7 +(*/------- rename -------\*)
3.8 val d_in: feedback -> term
3.9 val ts_in: feedback -> term list
3.10 val vars_of: T -> term list
3.11 @@ -34,22 +35,30 @@
3.12 val is_notyet_input : Proof.context -> T -> term list -> O_Model.single -> ('a * (term * term)) list
3.13 -> string * single
3.14 val dsc_unknown: term
3.15 + val pbl_ids': term -> term list -> term list
3.16
3.17 val mk_env: T -> (term * term) list
3.18 val penvval_in: feedback -> term list
3.19 +(*\------- rename -------/*)
3.20
3.21 - val pbl_ids': term -> term list -> term list
3.22 -(*/------- to I_Model from Specification -------\* )
3.23 - val ori2Coritm: Model_Pattern.T -> single -> single
3.24 -( *\------- to I_Model from Specification -------/*)
3.25 -
3.26 + val complete: O_Model.T -> T -> T -> Model_Pattern.T -> T
3.27 + val add: single -> T -> T
3.28 + val complete_method: O_Model.T * Model_Pattern.T * Model_Pattern.T * T -> T * T
3.29 + val is_error: feedback -> bool
3.30 + val complete': Model_Pattern.T -> O_Model.single -> single
3.31
3.32 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
3.33 + val is_complete: T -> bool
3.34 + val to_p_model: theory -> feedback -> string
3.35 +(*/------- rename -------\*)
3.36 val dts2str: term * (term list) -> string
3.37 val eq1: ''a -> 'b * (''a * 'c) -> bool
3.38 +(*\------- rename -------/*)
3.39 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
3.40 +(*/------- rename -------\*)
3.41 val vts_in: T -> int list
3.42 val seek_oridts: Proof.context -> ''a -> term * term list -> (int * 'b list * ''a * term * term list) list -> string * (int * 'b list * ''a * term * term list) * term list
3.43 +(*\------- rename -------/*)
3.44 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
3.45 end
3.46
3.47 @@ -374,11 +383,75 @@
3.48 | NONE => (ppc @ [itm])
3.49 in filter_out (eq_untouched ((d_in o #5) itm)) ppc' end
3.50
3.51 -(*/------- to I_Model from Specification -------\*)
3.52 -fun ori2Coritm pbt (i, v, f, d, ts) =
3.53 +fun complete' pbt (i, v, f, d, ts) =
3.54 (i, v, true, f, Cor ((d, ts), ((snd o snd o the o (find_first (eq1 d))) pbt, ts)))
3.55 handle _ => (i, v, true, f, Cor ((d, ts), (d, ts)))
3.56 (*dsc in oris, but not in pbl pat list: keep this dsc*)
3.57 -(*\------- to I_Model from Specification -------/*)
3.58 +
3.59 +(* filter out oris which have same description in itms *)
3.60 +fun filter_outs oris [] = oris
3.61 + | filter_outs oris (i::itms) =
3.62 + let
3.63 + val ors = filter_out ((curry op = ((d_in o #5) i)) o (#4)) oris
3.64 + in
3.65 + filter_outs ors itms
3.66 + end
3.67 +
3.68 +(* filter oris which are in pbt, too *)
3.69 +fun filter_pbt oris pbt =
3.70 + let
3.71 + val dscs = map (fst o snd) pbt
3.72 + in
3.73 + filter ((member op= dscs) o (#4)) oris
3.74 + end
3.75 +
3.76 +fun is_error (Cor _) = false
3.77 + | is_error (Sup _) = false
3.78 + | is_error (Inc _) = false
3.79 + | is_error (Mis _) = false
3.80 + | is_error _ = true
3.81 +
3.82 +(*create output-string for itm_*)
3.83 +fun to_p_model _ (Cor ((d, ts), _)) = UnparseC.term (Input_Descript.join (d, ts))
3.84 + | to_p_model _ (Syn c) = c
3.85 + | to_p_model _ (Typ c) = c
3.86 + | to_p_model _ (Inc ((d, ts), _)) = UnparseC.term (Input_Descript.join (d, ts))
3.87 + | to_p_model _ (Sup (d, ts)) = UnparseC.term (Input_Descript.join (d, ts))
3.88 + | to_p_model _ (Mis (d, pid)) = UnparseC.term d ^ " " ^ UnparseC.term pid
3.89 + | to_p_model _ _ = raise ERROR "to_p_model: uncovered definition"
3.90 +
3.91 +fun eq_dsc ((_, _, _, _, itm_), (_, _, _, _, iitm_)) = (d_in itm_ = d_in iitm_)
3.92 +
3.93 +(* insert_ppc = add for appl_add', input_icalhd 11.03,
3.94 + handles superfluous items carelessly *)
3.95 +fun add itm itms = if member eq_dsc itms itm then itms else itms @ [itm] (* @ new itm *)
3.96 +
3.97 +(* combine itms from pbl + met and complete them wrt. pbt *)
3.98 +(* FIXXXME.WN031205 complete doesnt handle incorrect itms !*)
3.99 +fun complete oris pits mits met =
3.100 + let
3.101 + val vat = max_vt pits;
3.102 + val itms = pits @ (filter ((member_swap op = vat) o (#2 )) mits)
3.103 + val ors = filter ((member_swap op= vat) o (#2)) oris
3.104 + val os = filter_outs ors itms (*WN.12.03?: does _NOT_ add itms from met ?!*)
3.105 + in
3.106 + itms @ (map (complete' met) os)
3.107 + end
3.108 +
3.109 +(* complete model and guard of a calc-head *)
3.110 +fun complete_method (oris, mpc, ppc, probl) =
3.111 + let
3.112 + val pits = filter_out ((curry op= false) o (#3)) probl
3.113 + val vat = if probl = [] then 1 else max_vt probl
3.114 + val pors = filter ((member_swap op = vat) o (#2)) oris
3.115 + val pors = filter_outs pors pits (*which are in pbl already*)
3.116 + val pors = (filter_pbt pors ppc) (*which are in pbt, too*)
3.117 + val pits = pits @ (map (complete' ppc) pors)
3.118 + val mits = complete oris pits [] mpc
3.119 + in (pits, mits) end
3.120 +
3.121 +(* WN0312: use in nxt_spec, too ? what about variants ??? *)
3.122 +fun is_complete [] = false
3.123 + | is_complete itms = foldl and_ (true, (map #3 itms))
3.124
3.125 (**)end(**);
3.126 \ No newline at end of file
4.1 --- a/src/Tools/isac/Specify/p-spec.sml Sat May 16 14:04:35 2020 +0200
4.2 +++ b/src/Tools/isac/Specify/p-spec.sml Sat May 16 16:23:24 2020 +0200
4.3 @@ -172,7 +172,7 @@
4.4 | appl_adds _ _ ppc _ [] = ppc
4.5 | appl_adds dI oris ppc pbt (selct :: ss) =
4.6 let val itm = appl_add' dI oris ppc pbt selct;
4.7 - in appl_adds dI oris (Specification.insert_ppc' itm ppc) pbt ss end
4.8 + in appl_adds dI oris (I_Model.add itm ppc) pbt ss end
4.9
4.10 fun par2fstr (_, _, _, f, I_Model.Par s) = (f, s)
4.11 | par2fstr itm = raise ERROR ("par2fstr: called with " ^ I_Model.single_to_string (ThyC.id_to_ctxt "Isac_Knowledge") itm)
4.12 @@ -221,7 +221,7 @@
4.13 (map itms2fstr probl), meth) end
4.14 else if mI <> smI (*FIXME.WN0311: what if probl is incomplete?!*)
4.15 then let val met = (#ppc o Method.from_store) mI
4.16 - val mits = Specification.complete_metitms oris probl meth met
4.17 + val mits = I_Model.complete oris probl meth met
4.18 in if foldl and_ (true, map #3 mits)
4.19 then (Pos.Pbl, probl, mits) else (Pos.Met, probl, mits)
4.20 end
5.1 --- a/src/Tools/isac/Specify/specification.sml Sat May 16 14:04:35 2020 +0200
5.2 +++ b/src/Tools/isac/Specify/specification.sml Sat May 16 16:23:24 2020 +0200
5.3 @@ -86,17 +86,6 @@
5.4 val specify_additem: string -> TermC.as_string -> Calc.T -> string * Calc.state_post
5.5 ( *\------- to Specify from Specification -------/*)
5.6
5.7 -(*/------- to I_Model from Specification -------\*)
5.8 - val complete_metitms: O_Model.T -> I_Model.T -> I_Model.T -> Model_Pattern.T -> I_Model.T
5.9 - val insert_ppc': I_Model.single -> I_Model.T -> I_Model.T
5.10 - val complete_mod_: O_Model.T * Model_Pattern.T * Model_Pattern.T * I_Model.T ->
5.11 - I_Model.T * I_Model.T
5.12 - val is_error: I_Model.feedback -> bool
5.13 - val itm_out: theory -> I_Model.feedback -> string
5.14 - val is_complete_mod_: ('a * 'b * bool * 'c * 'd) list -> bool
5.15 - val ori2Coritm: Model_Pattern.T -> O_Model.single -> I_Model.single
5.16 -(*\------- to I_Model from Specification -------/*)
5.17 -
5.18 (*/------- to P_Model from Specification -------\*)
5.19 val ppc2list: 'a P_Model.ppc -> 'a list
5.20 val mk_delete: theory -> string -> I_Model.feedback -> Tactic.input
5.21 @@ -176,12 +165,6 @@
5.22 | d_in i = raise ERROR ("all_dsc_in: uncovered case with " ^ I_Model.feedback_to_string' i)
5.23 in (flat o (map d_in)) itm_s end;
5.24
5.25 -fun is_error (I_Model.Cor _) = false
5.26 - | is_error (I_Model.Sup _) = false
5.27 - | is_error (I_Model.Inc _) = false
5.28 - | is_error (I_Model.Mis _) = false
5.29 - | is_error _ = true
5.30 -
5.31 (* get the first term in ts from ori *)
5.32 fun getr_ct thy (_, _, fd, d, ts) =
5.33 (fd, ((UnparseC.term_in_thy thy) o Input_Descript.join) (d,[hd ts]))
5.34 @@ -242,18 +225,9 @@
5.35 | SOME ori => SOME (geti_ct thy ori (hd icl))
5.36 end
5.37
5.38 -(*create output-string for itm_*)
5.39 -fun itm_out _ (I_Model.Cor ((d, ts), _)) = UnparseC.term (Input_Descript.join (d, ts))
5.40 - | itm_out _ (I_Model.Syn c) = c
5.41 - | itm_out _ (I_Model.Typ c) = c
5.42 - | itm_out _ (I_Model.Inc ((d, ts), _)) = UnparseC.term (Input_Descript.join (d, ts))
5.43 - | itm_out _ (I_Model.Sup (d, ts)) = UnparseC.term (Input_Descript.join (d, ts))
5.44 - | itm_out _ (I_Model.Mis (d, pid)) = UnparseC.term d ^ " " ^ UnparseC.term pid
5.45 - | itm_out _ _ = raise ERROR "itm_out: uncovered definition"
5.46 -
5.47 -fun mk_delete thy "#Given" itm_ = Tactic.Del_Given (itm_out thy itm_)
5.48 - | mk_delete thy "#Find" itm_ = Tactic.Del_Find (itm_out thy itm_)
5.49 - | mk_delete thy "#Relate" itm_ = Tactic.Del_Relation (itm_out thy itm_)
5.50 +fun mk_delete thy "#Given" itm_ = Tactic.Del_Given (I_Model.to_p_model thy itm_)
5.51 + | mk_delete thy "#Find" itm_ = Tactic.Del_Find (I_Model.to_p_model thy itm_)
5.52 + | mk_delete thy "#Relate" itm_ = Tactic.Del_Relation (I_Model.to_p_model thy itm_)
5.53 | mk_delete _ str _ = raise ERROR ("mk_delete: called with field \"" ^ str ^ "\"")
5.54 fun mk_additem "#Given" ct = Tactic.Add_Given ct
5.55 | mk_additem "#Find" ct = Tactic.Add_Find ct
5.56 @@ -280,7 +254,7 @@
5.57 (if dI' = ThyC.id_empty andalso dI = ThyC.id_empty then (Pos.Pbl, Tactic.Specify_Theory dI')
5.58 else if pI' = Problem.id_empty andalso pI = Problem.id_empty then (Pos.Pbl, Tactic.Specify_Problem pI')
5.59 else
5.60 - case find_first (is_error o #5) pbl of
5.61 + case find_first (I_Model.is_error o #5) pbl of
5.62 SOME (_, _, _, fd, itm_) =>
5.63 (Pos.Pbl, mk_delete (ThyC.get_theory (if dI = ThyC.id_empty then dI' else dI)) fd itm_)
5.64 | NONE =>
5.65 @@ -292,14 +266,14 @@
5.66 else if pI = Problem.id_empty then (Pos.Pbl, Tactic.Specify_Problem pI')
5.67 else if mI = Method.id_empty then (Pos.Pbl, Tactic.Specify_Method mI')
5.68 else
5.69 - case find_first (is_error o #5) met of
5.70 + case find_first (I_Model.is_error o #5) met of
5.71 SOME (_, _, _, fd, itm_) => (Pos.Met, mk_delete (ThyC.get_theory dI) fd itm_)
5.72 | NONE =>
5.73 (case nxt_add (ThyC.get_theory dI) oris mpc met of
5.74 SOME (fd, ct') => (Pos.Met, mk_additem fd ct') (*30.8.01: pre?!?*)
5.75 | NONE => (Pos.Met, Tactic.Apply_Method mI))))
5.76 | nxt_spec Pos.Met preok oris (dI', pI', _) (_, met) (_ ,mpc) (dI, pI, mI) =
5.77 - (case find_first (is_error o #5) met of
5.78 + (case find_first (I_Model.is_error o #5) met of
5.79 SOME (_,_,_,fd,itm_) => (Pos.Met, mk_delete (ThyC.get_theory (if dI = ThyC.id_empty then dI' else dI)) fd itm_)
5.80 | NONE =>
5.81 case nxt_add (ThyC.get_theory (if dI = ThyC.id_empty then dI' else dI)) oris mpc met of
5.82 @@ -312,13 +286,6 @@
5.83 | nxt_spec p _ _ _ _ _ _ = raise ERROR ("nxt_spec: uncovered case with " ^ Pos.pos_2str p)
5.84 (*\------- to Specify from Specification -------/*)
5.85
5.86 -
5.87 -fun eq_dsc ((_, _, _, _, itm_), (_, _, _, _, iitm_)) = (I_Model.d_in itm_ = I_Model.d_in iitm_)
5.88 -
5.89 -(* insert_ppc = insert_ppc' for appl_add', input_icalhd 11.03,
5.90 - handles superfluous items carelessly *)
5.91 -fun insert_ppc' itm itms = if member eq_dsc itms itm then itms else itms @ [itm] (* @ new itm *)
5.92 -
5.93 (* output the headline to a ppc *)
5.94 fun header p_ pI mI =
5.95 case p_ of
5.96 @@ -469,54 +436,6 @@
5.97 end
5.98 | nxt_specif_additem _ _ (_, p) = raise ERROR ("nxt_specif_additem not impl. for" ^ Pos.pos'2str p)
5.99
5.100 -(*/------- to I_Model from Specification -------\*)
5.101 -fun ori2Coritm pbt (i, v, f, d, ts) =
5.102 - (i, v, true, f, I_Model.Cor ((d, ts), ((snd o snd o the o (find_first (I_Model.eq1 d))) pbt, ts)))
5.103 - handle _ => (i, v, true, f, I_Model.Cor ((d, ts), (d, ts)))
5.104 - (*dsc in oris, but not in pbl pat list: keep this dsc*)
5.105 -(*\------- to I_Model from Specification -------/*)
5.106 -
5.107 -(* filter out oris which have same description in itms *)
5.108 -fun filter_outs oris [] = oris
5.109 - | filter_outs oris (i::itms) =
5.110 - let
5.111 - val ors = filter_out ((curry op = ((I_Model.d_in o #5) i)) o (#4)) oris
5.112 - in
5.113 - filter_outs ors itms
5.114 - end
5.115 -
5.116 -(* filter oris which are in pbt, too *)
5.117 -fun filter_pbt oris pbt =
5.118 - let
5.119 - val dscs = map (fst o snd) pbt
5.120 - in
5.121 - filter ((member op= dscs) o (#4)) oris
5.122 - end
5.123 -
5.124 -(* combine itms from pbl + met and complete them wrt. pbt *)
5.125 -(* FIXXXME.WN031205 complete_metitms doesnt handle incorrect itms !*)
5.126 -fun complete_metitms oris pits mits met =
5.127 - let
5.128 - val vat = I_Model.max_vt pits;
5.129 - val itms = pits @ (filter ((member_swap op = vat) o (#2 )) mits)
5.130 - val ors = filter ((member_swap op= vat) o (#2)) oris
5.131 - val os = filter_outs ors itms (*WN.12.03?: does _NOT_ add itms from met ?!*)
5.132 - in
5.133 - itms @ (map (ori2Coritm met) os)
5.134 - end
5.135 -
5.136 -(* complete model and guard of a calc-head *)
5.137 -fun complete_mod_ (oris, mpc, ppc, probl) =
5.138 - let
5.139 - val pits = filter_out ((curry op= false) o (#3)) probl
5.140 - val vat = if probl = [] then 1 else I_Model.max_vt probl
5.141 - val pors = filter ((member_swap op = vat) o (#2)) oris
5.142 - val pors = filter_outs pors pits (*which are in pbl already*)
5.143 - val pors = (filter_pbt pors ppc) (*which are in pbt, too*)
5.144 - val pits = pits @ (map (ori2Coritm ppc) pors)
5.145 - val mits = complete_metitms oris pits [] mpc
5.146 - in (pits, mits) end
5.147 -
5.148 (* fun tag_form thy (formal, given) = Thm.global_cterm_of thy
5.149 (((head_of o Thm.term_of) given) $ (Thm.term_of formal)); WN100819 *)
5.150 fun tag_form thy (formal, given) =
5.151 @@ -542,7 +461,7 @@
5.152 val (_, pI, mI) = References.select ospec spec
5.153 val mpc = (#ppc o Method.from_store) mI
5.154 val ppc = (#ppc o Problem.from_store) pI
5.155 - val (pits, mits) = complete_mod_ (oris, mpc, ppc, probl)
5.156 + val (pits, mits) = I_Model.complete_method (oris, mpc, ppc, probl)
5.157 val pt = Ctree.update_pblppc pt p pits
5.158 val pt = Ctree.update_metppc pt p mits
5.159 in (pt, (p, Pos.Met)) end
5.160 @@ -561,22 +480,24 @@
5.161 val (_, vals) = O_Model.values' pors
5.162 val ctxt = ContextC.initialise dI vals
5.163 val (pt, _) = Ctree.cupdate_problem pt p ((dI, pI, mI),
5.164 - map (ori2Coritm ppc) pors, map (ori2Coritm ppc) pors, ctxt)
5.165 + map (I_Model.complete' ppc) pors, map (I_Model.complete' ppc) pors, ctxt)
5.166 in
5.167 (pt, (p, Pos.Met))
5.168 end
5.169
5.170 +(*/------- to I_Model from Specification -------\* )
5.171 (* WN0312: use in nxt_spec, too ? what about variants ??? *)
5.172 fun is_complete_mod_ [] = false
5.173 | is_complete_mod_ itms = foldl and_ (true, (map #3 itms))
5.174 +( *\------- to I_Model from Specification -------/*)
5.175
5.176 fun is_complete_mod (pt, pos as (p, Pos.Pbl)) =
5.177 if (Ctree.is_pblobj o (Ctree.get_obj I pt)) p
5.178 - then (is_complete_mod_ o (Ctree.get_obj Ctree.g_pbl pt)) p
5.179 + then (I_Model.is_complete o (Ctree.get_obj Ctree.g_pbl pt)) p
5.180 else raise ERROR ("is_complete_mod: called by PrfObj at " ^ Pos.pos'2str pos)
5.181 | is_complete_mod (pt, pos as (p, Pos.Met)) =
5.182 if (Ctree.is_pblobj o (Ctree.get_obj I pt)) p
5.183 - then (is_complete_mod_ o (Ctree.get_obj Ctree.g_met pt)) p
5.184 + then (I_Model.is_complete o (Ctree.get_obj Ctree.g_met pt)) p
5.185 else raise ERROR ("is_complete_mod: called by PrfObj at " ^ Pos.pos'2str pos)
5.186 | is_complete_mod (_, pos) =
5.187 raise ERROR ("is_complete_mod called by " ^ Pos.pos'2str pos ^ " (should be Pbl or Met)")
6.1 --- a/src/Tools/isac/Specify/specify.sml Sat May 16 14:04:35 2020 +0200
6.2 +++ b/src/Tools/isac/Specify/specify.sml Sat May 16 16:23:24 2020 +0200
6.3 @@ -45,7 +45,7 @@
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 (Specification.is_error o #5) pbl of
6.8 + case find_first (I_Model.is_error o #5) pbl of
6.9 SOME (_, _, _, fd, itm_) =>
6.10 ("dummy", (Pbl, Specification.mk_delete (ThyC.get_theory
6.11 (if dI = ThyC.id_empty then dI' else dI)) fd itm_))
6.12 @@ -58,14 +58,14 @@
6.13 else if pI = Problem.id_empty then ("dummy", (Pbl, Tactic.Specify_Problem pI'))
6.14 else if mI = Method.id_empty then ("dummy", (Pbl, Tactic.Specify_Method mI'))
6.15 else
6.16 - case find_first (Specification.is_error o #5) met of
6.17 + case find_first (I_Model.is_error o #5) met of
6.18 SOME (_, _, _, fd, itm_) => ("dummy", (Met, Specification.mk_delete (ThyC.get_theory dI) fd itm_))
6.19 | NONE =>
6.20 (case Specification.nxt_add (ThyC.get_theory dI) oris mpc met of
6.21 SOME (fd, ct') => ("dummy", (Met, Specification.mk_additem fd ct')) (*30.8.01: pre?!?*)
6.22 | NONE => ("dummy", (Met, Tactic.Apply_Method mI)))))
6.23 | Met =>
6.24 - (case find_first (Specification.is_error o #5) met of
6.25 + (case find_first (I_Model.is_error o #5) met of
6.26 SOME (_,_,_,fd,itm_) => ("dummy", (Met, Specification.mk_delete (ThyC.get_theory (if dI = ThyC.id_empty then dI' else dI)) fd itm_))
6.27 | NONE =>
6.28 case Specification.nxt_add (ThyC.get_theory (if dI = ThyC.id_empty then dI' else dI)) oris mpc met of
7.1 --- a/src/Tools/isac/Specify/step-specify.sml Sat May 16 14:04:35 2020 +0200
7.2 +++ b/src/Tools/isac/Specify/step-specify.sml Sat May 16 16:23:24 2020 +0200
7.3 @@ -66,14 +66,14 @@
7.4 | _ => raise ERROR "by_tactic_input Model_Problem; uncovered case get_obj"
7.5 val (dI, pI, mI) = References.select ospec spec
7.6 val thy = ThyC.get_theory dI
7.7 - val mpc = (#ppc o Method.from_store) mI (* just for reuse complete_mod_ *)
7.8 + val mpc = (#ppc o Method.from_store) mI (* just for reuse I_Model.complete_method *)
7.9 val {cas, ppc, ...} = Problem.from_store pI
7.10 val pbl = I_Model.init ppc (* fill in descriptions *)
7.11 (*----------------if you think, this should be done by the Dialog
7.12 in the java front-end, search there for WN060225-modelProblem----*)
7.13 val (pbl, met) = case cas of
7.14 NONE => (pbl, [])
7.15 - | _ => complete_mod_ (oris, mpc, ppc, probl)
7.16 + | _ => I_Model.complete_method (oris, mpc, ppc, probl)
7.17 (*----------------------------------------------------------------*)
7.18 val tac_ = Tactic.Model_Problem' (pI, pbl, met)
7.19 val (pos,c,_,pt) = Specify_Step.add tac_ (Istate_Def.Uistate, ctxt) (pt, pos)
8.1 --- a/test/Tools/isac/Interpret/error-pattern.sml Sat May 16 14:04:35 2020 +0200
8.2 +++ b/test/Tools/isac/Interpret/error-pattern.sml Sat May 16 16:23:24 2020 +0200
8.3 @@ -1256,20 +1256,20 @@
8.4 tracing(I_Model.to_string thy iii);
8.5
8.6 val itm = add_single' dI oris ppc pbt selct;
8.7 - val ppc = insert_ppc' itm ppc;
8.8 + val ppc = I_Model.add itm ppc;
8.9
8.10 val _::selct::ss = (selct::ss);
8.11 val itm = add_single' dI oris ppc pbt selct;
8.12 - val ppc = insert_ppc' itm ppc;
8.13 + val ppc = I_Model.add itm ppc;
8.14
8.15 val _::selct::ss = (selct::ss);
8.16 val itm = add_single' dI oris ppc pbt selct;
8.17 - val ppc = insert_ppc' itm ppc;
8.18 + val ppc = I_Model.add itm ppc;
8.19 tracing(I_Model.to_string thy ppc);
8.20
8.21 val _::selct::ss = (selct::ss);
8.22 val itm = add_single' dI oris ppc pbt selct;
8.23 - val ppc = insert_ppc' itm ppc;
8.24 + val ppc = I_Model.add itm ppc;
8.25 *)
8.26 "--------- fun concat_deriv --------------------------------------";
8.27 "--------- fun concat_deriv --------------------------------------";
9.1 --- a/test/Tools/isac/Knowledge/diffapp.sml Sat May 16 14:04:35 2020 +0200
9.2 +++ b/test/Tools/isac/Knowledge/diffapp.sml Sat May 16 16:23:24 2020 +0200
9.3 @@ -400,7 +400,7 @@
9.4 "--------- autoCalc .. scripts for maximum-example ---------------";
9.5 "--------- autoCalc .. scripts for maximum-example ---------------";
9.6 "--------- autoCalc .. scripts for maximum-example ---------------";
9.7 -(*++++++++ see systest/inform.sml 'complete_metitms' ++++++++*)
9.8 +(*++++++++ see systest/inform.sml 'I_Model.complete' ++++++++*)
9.9 reset_states ();
9.10 val fmz =
9.11 ["fixedValues [r=Arbfix]","maximum A",
10.1 --- a/test/Tools/isac/Minisubpbl/150-add-given.sml Sat May 16 14:04:35 2020 +0200
10.2 +++ b/test/Tools/isac/Minisubpbl/150-add-given.sml Sat May 16 16:23:24 2020 +0200
10.3 @@ -48,7 +48,7 @@
10.4
10.5 dI' = ThyC.id_empty andalso dI = ThyC.id_empty; (* = false*)
10.6 pI' = Problem.id_empty andalso pI = Problem.id_empty; (* = false*)
10.7 -find_first (is_error o #5) (pbl:I_Model.T); (* = NONE*)
10.8 +find_first (I_Model.is_error o #5) (pbl:I_Model.T); (* = NONE*)
10.9
10.10 (* nxt_add (ThyC.get_theory (if dI = ThyC.id_empty then dI' else dI)) oris pbt pbl;
10.11 = SOME ("#Given", "equality (<markup> + <markup> = <markup>)") *)
11.1 --- a/test/Tools/isac/Minisubpbl/200-start-method.sml Sat May 16 14:04:35 2020 +0200
11.2 +++ b/test/Tools/isac/Minisubpbl/200-start-method.sml Sat May 16 16:23:24 2020 +0200
11.3 @@ -67,7 +67,7 @@
11.4 PblObj {meth = itms, origin = (oris, _, _), probl, ...} => (itms, oris, probl)
11.5 | _ => error "LI.by_tactic Apply_Method': uncovered case get_obj"
11.6 val {ppc, ...} = Method.from_store mI;
11.7 - val itms = if itms <> [] then itms else Specification.complete_metitms oris probl [] ppc
11.8 + val itms = if itms <> [] then itms else I_Model.complete oris probl [] ppc
11.9 val itms = Step_Specify.hack_until_review_Specify_1 mI itms
11.10 val srls = LItool.get_simplifier (pt, pos)
11.11 val (is, env, ctxt, prog) = case LItool.init_pstate srls ctxt itms mI of
12.1 --- a/test/Tools/isac/Minisubpbl/300-init-subpbl-NEXT_STEP.sml Sat May 16 14:04:35 2020 +0200
12.2 +++ b/test/Tools/isac/Minisubpbl/300-init-subpbl-NEXT_STEP.sml Sat May 16 16:23:24 2020 +0200
12.3 @@ -53,7 +53,7 @@
12.4 val (itms, oris, probl) = case get_obj I pt p of
12.5 PblObj {meth = itms, origin = (oris, _, _), probl, ...} => (itms, oris, probl)
12.6 | _ => error "begin_end_prog Apply_Method': uncovered case get_obj"
12.7 - val itms = if itms <> [] then itms else Specification.complete_metitms oris probl [] ppc
12.8 + val itms = if itms <> [] then itms else I_Model.complete oris probl [] ppc
12.9 val thy' = get_obj g_domID pt p;
12.10 val thy = ThyC.get_theory thy';
12.11 val srls = LItool.get_simplifier (pt, pos);
13.1 --- a/test/Tools/isac/Specify/specify.sml Sat May 16 14:04:35 2020 +0200
13.2 +++ b/test/Tools/isac/Specify/specify.sml Sat May 16 16:23:24 2020 +0200
13.3 @@ -8,7 +8,7 @@
13.4 "-----------------------------------------------------------------------------------------------";
13.5 "-----------------------------------------------------------------------------------------------";
13.6 "----------- maximum-example: complete_mod ERROR formalisation inconsistent w.r.t. type inferenc";
13.7 -"----------- maximum-example: complete_metitms -------------------------------------------------";
13.8 +"----------- maximum-example: I_Model.complete -------------------------------------------------";
13.9 "-----------------------------------------------------------------------------------------------";
13.10 "-----------------------------------------------------------------------------------------------";
13.11 "-----------------------------------------------------------------------------------------------";
13.12 @@ -70,9 +70,9 @@
13.13 (11 ,[1,2,3] ,true ,#undef ,Cor errorBound (eps = 0) ,(errorBound, [eps = 0]))]*)
13.14 ( *\\-------- WAS OUT OF Test UNTIL 200209, ERROR PROBABLY FROM INTRO. OF Isabelle's funpack --//*)
13.15
13.16 -"----------- maximum-example: complete_metitms -------------------------------------------------";
13.17 -"----------- maximum-example: complete_metitms -------------------------------------------------";
13.18 -"----------- maximum-example: complete_metitms -------------------------------------------------";
13.19 +"----------- maximum-example: I_Model.complete -------------------------------------------------";
13.20 +"----------- maximum-example: I_Model.complete -------------------------------------------------";
13.21 +"----------- maximum-example: I_Model.complete -------------------------------------------------";
13.22 val c = [];
13.23 val (p,_,f,nxt,_,pt) =
13.24 CalcTreeTEST
13.25 @@ -120,7 +120,7 @@
13.26 (4 ,[1,2] ,true,#Relate ,Cor relations [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^
13.27 2 = r ^^^ 2] ,(rs_, [[A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]]))]*)
13.28 val mits = get_obj g_met pt (fst p);
13.29 - val mits = complete_metitms oris pits []
13.30 + val mits = I_Model.complete oris pits []
13.31 ((#ppc o Method.from_store) ["DiffApp","max_by_calculus"]);
13.32 writeln (I_Model.to_string ctxt mits);
13.33 (*[
13.34 @@ -135,6 +135,6 @@
13.35 (11 ,[1,2,3] ,true ,#undef ,Cor errorBound (eps = 0) ,(errorBound, [eps = 0]))]*)
13.36 if I_Model.to_string ctxt mits
13.37 = "[\n(1 ,[1,2,3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(f_ix, [[r = Arbfix]])),\n(2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_m, [A])),\n(3 ,[1,2,3] ,true ,#Find ,Cor valuesFor [a, b] ,(v_s, [[a, b]])),\n(4 ,[1,2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2] ,(r_s, [[A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]])),\n(6 ,[1] ,true ,#undef ,Cor boundVariable a ,(v_v, [a])),\n(9 ,[1,2] ,true ,#undef ,Cor interval {x. 0 \<le> x \<and> x \<le> 2 * r} ,(i_tv, [{x. 0 \<le> x \<and> x \<le> 2 * r}])),\n(11 ,[1,2,3] ,true ,#undef ,Cor errorBound (eps = 0) ,(e_rr, [eps = 0]))]"
13.38 -then () else error "completetest.sml: new behav. in complete_metitms 1";
13.39 +then () else error "completetest.sml: new behav. in I_Model.complete 1";
13.40
13.41
14.1 --- a/test/Tools/isac/Specify/step-specify.sml Sat May 16 14:04:35 2020 +0200
14.2 +++ b/test/Tools/isac/Specify/step-specify.sml Sat May 16 16:23:24 2020 +0200
14.3 @@ -70,7 +70,7 @@
14.4 = (p_, pb, oris, (dI', pI', mI'), (probl, meth), (ppc, (#ppc o Method.from_store) cmI), (dI, pI, mI));
14.5 (*if*) dI' = ThyC.id_empty andalso dI = ThyC.id_empty (*else*);
14.6 (*if*) pI' = Problem.id_empty andalso pI = Problem.id_empty (*else*);
14.7 - val NONE = (*case*) find_first (is_error o #5) pbl (*of*);
14.8 + val NONE = (*case*) find_first (I_Model.is_error o #5) pbl (*of*);
14.9 val NONE = (*case*) nxt_add (ThyC.get_theory (if dI = ThyC.id_empty then dI' else dI)) oris pbt pbl (*of*);
14.10 (*if*) not preok (*else*);
14.11 (*if*) dI = ThyC.id_empty (*then*);
15.1 --- a/test/Tools/isac/Test_Some.thy Sat May 16 14:04:35 2020 +0200
15.2 +++ b/test/Tools/isac/Test_Some.thy Sat May 16 16:23:24 2020 +0200
15.3 @@ -19,7 +19,6 @@
15.4 open Istate;
15.5 open Error_Pattern;
15.6 open Error_Pattern_Def;
15.7 - open In_Chead;
15.8 open Specification;
15.9 open Ctree; append_problem;
15.10 open Pos;