1.1 --- a/TODO.md Fri Dec 01 06:08:22 2023 +0100
1.2 +++ b/TODO.md Tue Dec 05 18:15:45 2023 +0100
1.3 @@ -45,6 +45,13 @@
1.4 ***** priority of WN items is top down, most urgent/simple on top
1.5
1.6 * WN:
1.7 +* WN: clarify handling "#undef" -> type m_field +++ bool in i_single
1.8 + ?RN?or?just for OLD? ori_2itm -> single_from_o, ori_2itm_POS -> single_from_o_POS
1.9 +* WN: replace I_Model.values_POS' -> val get_values = Pre_Conds.get_values
1.10 +* WN: RN o_model_values -> get_values, values_POS' -> get_values_POS,
1.11 + TEST_to_OLD -> POS_to_OLD, TEST_to_OLD_single -> POS_to_OLD_single,
1.12 +
1.13 +* WN: eliminate max_variant in favour of max_variants
1.14 * WN: replace I_Model.descriptor with fun descr_exists: descriptor -> feedback -> bool
1.15 * WN: review Model_Def.is_list_descr, replace by Term.is_list. Exception: make_values
1.16 (values determine handling_lists by [[..], [..], ..])
2.1 --- a/src/Tools/isac/Build_Isac.thy Fri Dec 01 06:08:22 2023 +0100
2.2 +++ b/src/Tools/isac/Build_Isac.thy Tue Dec 05 18:15:45 2023 +0100
2.3 @@ -271,11 +271,16 @@
2.4 subsection \<open>(5) Adopt Isabelle/jEdit for Isac\<close>
2.5
2.6 ML \<open>
2.7 -\<close> ML \<open>
2.8 -
2.9 +\<close> text \<open>
2.10 +I_Model.T_POS
2.11 \<close> ML \<open>
2.12 I_Model.TEST_to_OLD ;
2.13 -I_Model.OLD_to_POS
2.14 +I_Model.TEST_to_OLD_single ;
2.15 +I_Model.feedback_POS_to_OLD ;
2.16 +
2.17 +I_Model.OLD_to_POS ;
2.18 +I_Model.OLD_to_POS_single ;
2.19 +I_Model.feedback_OLD_to_POS ;
2.20 (*OLD*)
2.21 (*---*)
2.22 (*NEW*)
3.1 --- a/src/Tools/isac/MathEngBasic/model-def.sml Fri Dec 01 06:08:22 2023 +0100
3.2 +++ b/src/Tools/isac/MathEngBasic/model-def.sml Tue Dec 05 18:15:45 2023 +0100
3.3 @@ -155,7 +155,7 @@
3.4 Cor_POS of (descriptor * (* correct input: descriptor, see Input_Descript.thy *)
3.5 (values)) (* set of values for list-types: for decding
3.6 Inc the values packed out from the list;
3.7 - They are packed back to an isalist for envs *)
3.8 + They are packed back to an isalist for envs *)
3.9 | Syn_POS of TermC.as_string (* syntax error kept for P_Model.switch_pbl_met *)
3.10 | Inc_POS of (descriptor * values) (* see Cor *)
3.11 | Sup_POS of (descriptor * values) (* superfluous; input not found in O_Model.T *)
4.1 --- a/src/Tools/isac/Specify/Specify.thy Fri Dec 01 06:08:22 2023 +0100
4.2 +++ b/src/Tools/isac/Specify/Specify.thy Tue Dec 05 18:15:45 2023 +0100
4.3 @@ -20,13 +20,70 @@
4.4 ML_file specification.sml
4.5 ML_file "cas-command.sml"
4.6 ML_file "p-spec.sml"
4.7 - ML_file specify.sml
4.8 + ML_file specify.sml
4.9 ML_file "sub-problem.sml"
4.10 ML_file "step-specify.sml"
4.11
4.12 ML \<open>
4.13 +open P_Spec
4.14 \<close> ML \<open>
4.15 -
4.16 +\<close> ML \<open>
4.17 +\<close> ML \<open>
4.18 +\<close> ML \<open>
4.19 +\<close> ML \<open>
4.20 +\<close> ML \<open>
4.21 +\<close> text \<open>
4.22 +fun ori_2itm (feedb:feedback_POS) _ all (id, vt, fd, d, ts) =
4.23 + let
4.24 + val ts' = union op = (values_POS' feedb) ts;
4.25 + val complete = if eq_set op = (ts', all) then true else false
4.26 + in
4.27 + case feedb of
4.28 + Cor_POS _ => if fd = "#undef"
4.29 + then (id, vt, complete, fd, (Sup_POS (d, ts'), Position.none))
4.30 + else (id, vt, complete, fd, (Cor_POS (d, ts'), Position.none))
4.31 + | Inc_POS _ => if complete
4.32 + then (id, vt, true, fd, (Cor_POS (d, ts'), Position.none))
4.33 + else (id, vt, false, fd, (Inc_POS (d, ts'), Position.none))
4.34 + | Sup_POS (d, ts') =>
4.35 + (id, vt, complete, fd, (Sup_POS (d, ts'), Position.none))
4.36 + | i => raise ERROR ("ori_2itm: uncovered case of " ^ feedback_POS_to_string (ContextC.for_ERROR ()) i)
4.37 + end
4.38 +;
4.39 +ori_2itm: feedback_POS -> descriptor -> Model_Def.values -> O_Model.single -> I_Model.single_POS
4.40 +\<close> ML \<open>
4.41 +\<close> text \<open>
4.42 +(*old code kept for test/*)
4.43 +fun is_notyet_input ctxt (itms:I_Model.T_POS) all (i, v, f, d, ts) pbt =
4.44 + case find_first (fn (_, (d', _)) => d = d') pbt of
4.45 + SOME (_, (_, pid)) =>
4.46 + (case find_first (fn (_, _, _, f', (feedb, _)) =>
4.47 + f = f' andalso d = (descriptor_POS feedb)) itms of
4.48 + SOME (_, _, _, _, (feedb:feedback_POS, _)) =>
4.49 + let val ts' = inter op = (values_POS' feedb) ts
4.50 + in
4.51 + if subset op = (ts, ts')
4.52 + then (((strs2str' o map (UnparseC.term ctxt)) ts') ^ " already input", empty_single_POS)
4.53 + else ("", ori_2itm feedb pid all (i, v, f, d, subtract op = ts' ts))
4.54 + end
4.55 + | NONE => ("", ori_2itm (Inc_POS (TermC.empty, [])) pid all (i, v, f, d, ts)))
4.56 + | NONE => ("", ori_2itm (Sup_POS (d, ts)) TermC.empty all (i, v, f, d, ts))
4.57 +;
4.58 +is_notyet_input: Proof.context -> I_Model.T_POS -> O_Model.values ->
4.59 + O_Model.single -> Model_Pattern.T -> I_Model.message * I_Model.single_POS
4.60 +\<close> ML \<open>
4.61 +\<close> ML \<open>
4.62 +fun is_e_ts [] = true
4.63 + | is_e_ts [Const (\<^const_name>\<open>Nil\<close>, _)] = true
4.64 + | is_e_ts _ = false;
4.65 +\<close> ML \<open>
4.66 +\<close> ML \<open>
4.67 +\<close> ML \<open>
4.68 +\<close> ML \<open>
4.69 +\<close> ML \<open>
4.70 +\<close> ML \<open>
4.71 +\<close> ML \<open>
4.72 +\<close> ML \<open>
4.73 \<close> ML \<open>
4.74 \<close>
4.75 end
5.1 --- a/src/Tools/isac/Specify/cas-command.sml Fri Dec 01 06:08:22 2023 +0100
5.2 +++ b/src/Tools/isac/Specify/cas-command.sml Tue Dec 05 18:15:45 2023 +0100
5.3 @@ -9,13 +9,17 @@
5.4 type T = CAS_Def.T
5.5 val input : term -> (Ctree.ctree * SpecificationC.T) option
5.6 val is_from: TermC.as_string -> Formalise.T -> bool
5.7 -\<^isac_test>\<open>
5.8 +
5.9 +(*/----- from isac_test for Minisubpbl*)
5.10 val input_: References.T -> (term * term list) list ->
5.11 - Problem.id * I_Model.T * MethodC.id * I_Model.T * Pre_Conds.T * Proof.context
5.12 -
5.13 + Problem.id * I_Model.T_POS * MethodC.id * I_Model.T_POS * Pre_Conds.T * Proof.context
5.14 val dtss2itm_: Model_Pattern.T -> term * term list ->
5.15 int list * bool * string * I_Model.feedback (*I_Model.single'*)
5.16 val flattup2: 'a * ('b * 'c * 'd * 'e) -> 'a * 'b * 'c * 'd * 'e
5.17 +(*\----- from isac_test for Minisubpbl*)
5.18 +
5.19 +\<^isac_test>\<open>
5.20 +(*put "from isac_test for Minisubpbl" here*)
5.21 \<close>
5.22 end
5.23
5.24 @@ -62,7 +66,7 @@
5.25 val mits = map flattup2 its
5.26 val (_, where_) = Pre_Conds.check ctxt where_rls where_ (model, I_Model.OLD_to_POS mits)
5.27 val ctxt = Proof_Context.init_global thy
5.28 - in (pI, pits, mI, mits, where_, ctxt) end;
5.29 + in (pI, I_Model.OLD_to_POS pits, mI, I_Model.OLD_to_POS mits, where_, ctxt) end;
5.30
5.31 (* check if the input term is a CAScmd and return a ctree with a _complete_ calchead *)
5.32 fun input hdt =
5.33 @@ -79,10 +83,11 @@
5.34 val (pt,_) = Ctree.cappend_problem Ctree.e_ctree [] (Istate_Def.empty, ContextC.empty)
5.35 ([], References.empty) ([], References.empty, hdt, ctxt)
5.36 val pt = Ctree.update_spec pt [] spec
5.37 - val pt = Ctree.update_pbl pt [] pits
5.38 - val pt = Ctree.update_met pt [] mits
5.39 + val pt = Ctree.update_pbl pt [] (I_Model.TEST_to_OLD pits)
5.40 + val pt = Ctree.update_met pt [] (I_Model.TEST_to_OLD mits)
5.41 in
5.42 - SOME (pt, (true, Pos.Met, hdt, mits, where_, spec) : SpecificationC.T)
5.43 +(*quick and dirty------------------------vvvvvvvvvvvvvvvvvvv-----*)
5.44 + SOME (pt, (true, Pos.Met, hdt, I_Model.TEST_to_OLD mits, where_, spec) : SpecificationC.T)
5.45 end
5.46 end
5.47
6.1 --- a/src/Tools/isac/Specify/i-model.sml Fri Dec 01 06:08:22 2023 +0100
6.2 +++ b/src/Tools/isac/Specify/i-model.sml Tue Dec 05 18:15:45 2023 +0100
6.3 @@ -41,26 +41,29 @@
6.4 val to_string_POS: Proof.context -> T_POS -> string
6.5
6.6 val feedback_OLD_to_POS: feedback -> feedback_POS
6.7 + val feedback_POS_to_OLD: feedback_POS -> feedback
6.8 + val OLD_to_POS_single: single -> single_POS
6.9 + val TEST_to_OLD_single: single_POS -> single
6.10
6.11 - datatype add_single = Add of single | Err of string
6.12 + datatype add_single = Add of single_POS | Err of string
6.13 val init: Model_Pattern.T -> T
6.14 val init_POS: Proof.context -> O_Model.T -> Model_Pattern.T -> T_POS
6.15 val check_single: Proof.context -> m_field -> O_Model.T -> T -> Model_Pattern.T ->
6.16 TermC.as_string -> add_single
6.17 + (*probably unused in PIDE, thus-----v----v*)
6.18 val add_single: theory -> single -> T -> T
6.19
6.20 val make_tactic: m_field -> TermC.as_string * T -> Tactic.T
6.21 -(*--*)
6.22 +
6.23 val descriptor: feedback -> descriptor
6.24 -(*--*)
6.25 val descriptor_POS: feedback_POS -> descriptor
6.26 val values: feedback -> values option
6.27 val o_model_values: feedback -> values
6.28 val values_POS': feedback_POS -> values
6.29 val descr_pairs_to_string: Proof.context -> (Model_Pattern.single * single_POS) list -> string
6.30 val variables: Model_Pattern.T -> Model_Def.i_model_POS -> term list
6.31 - val is_notyet_input : Proof.context -> T -> O_Model.values -> O_Model.single -> Model_Pattern.T
6.32 - -> message * single
6.33 + val is_notyet_input: Proof.context -> T_POS -> O_Model.values -> O_Model.single ->
6.34 + Model_Pattern.T -> message * single_POS
6.35 val get_field_term: theory -> O_Model.single -> single -> m_field * TermC.as_string
6.36
6.37 val fill_from_o: O_Model.T -> single_POS -> single_POS option
6.38 @@ -78,19 +81,18 @@
6.39 val msg: variants -> feedback_POS -> string
6.40 val transfer_terms: O_Model.single -> single_POS
6.41
6.42 - val eq1: ''a -> 'b * (''a * 'c) -> bool
6.43 val feedback_to_string: Proof.context -> feedback -> string
6.44 val feedback_POS_to_string: Proof.context -> feedback_POS -> string
6.45 val descr_vals_to_string: Proof.context -> descriptor * values -> string
6.46 val feedb_args_to_string: Proof.context -> feedback_POS -> string
6.47
6.48 - val ori_2itm: feedback -> descriptor -> Model_Def.values -> O_Model.single -> single
6.49 + val ori_2itm: feedback_POS -> descriptor -> Model_Def.values -> O_Model.single -> single_POS
6.50 val seek_ppc: int -> T -> single option
6.51 val overwrite_ppc: theory -> single -> T -> T
6.52 (*\----- from isac_test for Minisubpbl*)
6.53
6.54 \<^isac_test>\<open>
6.55 - (**)
6.56 + (*copy "from isac_test for Minisubpbl" here*)
6.57
6.58 \<close>
6.59
6.60 @@ -141,15 +143,15 @@
6.61 | feedback_OLD_to_POS (Mis (d, pid)) = Model_Def.Syn_POS ((UnparseC.term (ContextC.for_ERROR ()) d) ^ " " ^
6.62 (UnparseC.term (ContextC.for_ERROR ()) pid))
6.63 | feedback_OLD_to_POS (Par s) = (Model_Def.Syn_POS s)
6.64 -fun OLD_to_POS i_old =
6.65 - map (fn (a, b, c, d, e) => (a, b, c, d, (feedback_OLD_to_POS e, Position.none))) i_old
6.66 +fun OLD_to_POS_single (a, b, c, d, e) = (a, b, c, d, (feedback_OLD_to_POS e, Position.none))
6.67 +fun OLD_to_POS i_old = map OLD_to_POS_single i_old
6.68
6.69 fun feedback_POS_to_OLD (Model_Def.Cor_POS (d, ts)) = (Cor ((d, ts), (TermC.empty, [])))
6.70 | feedback_POS_to_OLD (Model_Def.Syn_POS c) = (Syn c)
6.71 | feedback_POS_to_OLD (Model_Def.Inc_POS (d, ts)) = (Inc ((d, ts), (TermC.empty, [])))
6.72 | feedback_POS_to_OLD (Model_Def.Sup_POS (d, ts)) = (Sup (d, ts))
6.73 -fun TEST_to_OLD i_model =
6.74 - map (fn (a, b, c, d, (e, _)) => (a, b, c, d, feedback_POS_to_OLD e)) i_model
6.75 +fun TEST_to_OLD_single (a, b, c, d, (e, _)) = (a, b, c, d, feedback_POS_to_OLD e)
6.76 +fun TEST_to_OLD i_model = map TEST_to_OLD_single i_model
6.77
6.78 type message = string;
6.79
6.80 @@ -287,8 +289,9 @@
6.81 Pre_Conds.environment_POS model_patt i_model
6.82 |> map snd
6.83
6.84 +(*
6.85 val unknown_descriptor = Syntax.read_term\<^context> "unknown::'a => unknow";
6.86 -
6.87 +*)
6.88 (* get a term from O_Model, notyet input in I_Model.
6.89 the term from O_Model is thrown back to a string in order to reuse
6.90 machinery for immediate input by the user. *)
6.91 @@ -296,56 +299,44 @@
6.92 (fd, ((UnparseC.term_in_thy thy) o Input_Descript.join) (d, subtract op = (o_model_values itm_) ts))
6.93
6.94 (*update the itm_ already input, all..from ori*)
6.95 -fun ori_2itm itm_ pid all (id, vt, fd, d, ts) =
6.96 +fun ori_2itm (feedb:feedback_POS) _ all (id, vt, fd, d, ts) =
6.97 let
6.98 - val ts' = union op = (o_model_values itm_) ts;
6.99 - val pval = [Input_Descript.join'''' (d, ts')]
6.100 - (*WN.9.5.03: FIXXXME [#0, epsilon] here would upd_penv be called for [#0, epsilon] etc*)
6.101 + val ts' = union op = (values_POS' feedb) ts;
6.102 val complete = if eq_set op = (ts', all) then true else false
6.103 in
6.104 - case itm_ of
6.105 - (Cor _) =>
6.106 - (if fd = "#undef" then (id, vt, complete, fd, Sup (d, ts'))
6.107 - else (id, vt, complete, fd, Cor ((d, ts'), (pid, pval))))
6.108 - | (Syn c) => raise ERROR ("ori_2itm wants to overwrite " ^ c)
6.109 - | (Typ c) => raise ERROR ("ori_2itm wants to overwrite " ^ c)
6.110 - | (Inc _) =>
6.111 - if complete
6.112 - then (id, vt, true, fd, Cor ((d, ts'), (pid, pval)))
6.113 - else (id, vt, false, fd, Inc ((d, ts'), (pid, pval)))
6.114 - | (Sup (d,ts')) => (*4.9.01 lost env*)
6.115 - (*if fd = "#undef" then*) (id,vt,complete,fd,Sup(d,ts'))
6.116 - (*else (id,vt,complete,fd,Cor((d,ts'),e))*)
6.117 - (* 28.1.00: not completely clear ---^^^ etc.*)
6.118 - | (Mis _) => (* 4.9.01: Mis just copied *)
6.119 - if complete
6.120 - then (id, vt, true, fd, Cor ((d,ts'), (pid, pval)))
6.121 - else (id, vt, false, fd, Inc ((d,ts'), (pid, pval)))
6.122 - | i => raise ERROR ("ori_2itm: uncovered case of " ^ feedback_to_string (ContextC.for_ERROR ()) i)
6.123 + case feedb of
6.124 + Cor_POS _ => if fd = "#undef"
6.125 + then (id, vt, complete, fd, (Sup_POS (d, ts'), Position.none))
6.126 + else (id, vt, complete, fd, (Cor_POS (d, ts'), Position.none))
6.127 + | Inc_POS _ => if complete
6.128 + then (id, vt, true, fd, (Cor_POS (d, ts'), Position.none))
6.129 + else (id, vt, false, fd, (Inc_POS (d, ts'), Position.none))
6.130 + | Sup_POS (d, ts') =>
6.131 + (id, vt, complete, fd, (Sup_POS (d, ts'), Position.none))
6.132 + | i => raise ERROR ("ori_2itm: uncovered case of " ^ feedback_POS_to_string (ContextC.for_ERROR ()) i)
6.133 end
6.134
6.135
6.136 (** find next step **)
6.137
6.138 -fun eq1 d (_, (d', _)) = (d = d')
6.139 -fun eq3 f d (_, _, _, f', itm_) = f = f' andalso d = (descriptor itm_)
6.140 -
6.141 +(*old code kept for test/*)
6.142 fun is_notyet_input ctxt itms all (i, v, f, d, ts) pbt =
6.143 - case find_first (eq1 d) pbt of
6.144 + case find_first (fn (_, (d', _)) => d = d') pbt of
6.145 SOME (_, (_, pid)) =>
6.146 - (case find_first (eq3 f d) itms of
6.147 - SOME (_, _, _, _, itm_) =>
6.148 - let val ts' = inter op = (o_model_values itm_) ts
6.149 - in
6.150 + (case find_first (fn (_, _, _, f', (feedb, _)) =>
6.151 + f = f' andalso d = (descriptor_POS feedb)) itms of
6.152 + SOME (_, _, _, _, (feedb, _)) =>
6.153 + let val ts' = inter op = (values_POS' feedb) ts
6.154 + in
6.155 if subset op = (ts, ts')
6.156 - then (((strs2str' o map (UnparseC.term ctxt)) ts') ^ " already input", empty_single)
6.157 - else ("", ori_2itm itm_ pid all (i, v, f, d, subtract op = ts' ts))
6.158 - end
6.159 - | NONE => ("", ori_2itm (Inc ((TermC.empty, []), (pid, []))) pid all (i, v, f, d, ts)))
6.160 - | NONE => ("", ori_2itm (Sup (d, ts)) TermC.empty all (i, v, f, d, ts))
6.161 + then (((strs2str' o map (UnparseC.term ctxt)) ts') ^ " already input", empty_single_POS)
6.162 + else ("", ori_2itm feedb pid all (i, v, f, d, subtract op = ts' ts))
6.163 + end
6.164 + | NONE => ("", ori_2itm (Inc_POS (TermC.empty, [])) pid all (i, v, f, d, ts)))
6.165 + | NONE => ("", ori_2itm (Sup_POS (d, ts)) TermC.empty all (i, v, f, d, ts))
6.166
6.167 datatype add_single =
6.168 - Add of single (* return-value of check_single *)
6.169 + Add of single_POS (* return-value of check_single *)
6.170 | Err of string (* error-message *)
6.171
6.172 (*
6.173 @@ -365,27 +356,22 @@
6.174 (*\------------ replace by ParseC.term_position -----------/*)
6.175 (*NONE => Add (i, [], false, m_field, Syn ct)*)
6.176 val (d, ts) = Input_Descript.split t
6.177 - in
6.178 - if d = TermC.empty then
6.179 - Add (i, [], false, m_field, Mis (unknown_descriptor, hd ts))
6.180 - else
6.181 - (case find_first (eq1 d) m_patt of
6.182 - NONE => Add (i, [], true, m_field, Sup (d,ts))
6.183 + in
6.184 + (*if d = TermC.empty then .. *)
6.185 + (case find_first (fn (_, (d', _)) => d = d') m_patt of
6.186 + NONE => Add (i, [], true, m_field, (Sup_POS (d,ts), Position.none))
6.187 | SOME (f, (_, id)) =>
6.188 - let
6.189 - fun eq2 d (i, _, _, _, itm_) = d = (descriptor itm_) andalso i <> 0
6.190 - in
6.191 - case find_first (eq2 d) i_model of
6.192 - NONE => Add (i, [], true, f,Cor ((d, ts), (id, [Input_Descript.join'''' (d, ts)])))
6.193 - | SOME (i', _, _, _, itm_) =>
6.194 - if Input_Descript.for_list d then
6.195 - let
6.196 - val in_itm = o_model_values itm_
6.197 - val ts' = union op = ts in_itm
6.198 - val i'' = if in_itm = [] then i else i'
6.199 - in Add (i'', [], true, f, Cor ((d, ts'), (id, [Input_Descript.join'''' (d, ts')])))end
6.200 - else Add (i', [], true, f, Cor ((d, ts), (id, [Input_Descript.join'''' (d, ts)])))
6.201 - end)
6.202 + case find_first (fn (i, _, _, _, feedb) => d = (descriptor feedb) andalso i <> 0) i_model of
6.203 + NONE =>
6.204 + Add (i, [], true, f, (Cor_POS (d, ts), Position.none))
6.205 + | SOME (i', _, _, _, itm_) =>
6.206 + if Input_Descript.for_list d then
6.207 + let
6.208 + val in_itm = o_model_values itm_
6.209 + val ts' = union op = ts in_itm
6.210 + val i'' = if in_itm = [] then i else i'
6.211 + in Add (i'', [], true, f, (Cor_POS (d, ts'), Position.none)) end
6.212 + else Add (i', [], true, f, (Cor_POS (d, ts), Position.none)))
6.213 end
6.214 (*will come directly from PIDE ----------------------vvvvvvvvvvv*)
6.215 | check_single ctxt m_field o_model i_model m_patt (str(*, pos*)) =
6.216 @@ -404,7 +390,7 @@
6.217 else
6.218 case O_Model.contains ctxt m_field o_model t of
6.219 ("", ori', all) =>
6.220 - (case is_notyet_input ctxt i_model all ori' m_patt of
6.221 + (case is_notyet_input ctxt (OLD_to_POS i_model) all ori' m_patt of
6.222 ("", itm) => Add itm
6.223 | (msg, _) => Err ("ERROR I_Model.check_single: is_notyet_input: " ^ msg))
6.224 | (msg, _, _) => Err ("ERROR I_Model.check_single: contains: " ^ msg)
6.225 @@ -486,7 +472,7 @@
6.226 | NONE => raise ERROR "I_Model.fill_from_o does NOT find a descriptor in O_Model"
6.227 val descr = Model_Def.get_descr feedb (*i_single has been filtered appropriately*)
6.228 in
6.229 -(*---------------vvvvvvvvvvvvv MV if TermC-is_list all_value-----*)
6.230 +(*---------------vvvvvvvvvvvvv MV if TermC.is_list all_value-----*)
6.231 if Model_Def.is_list_descr descr
6.232 then
6.233 let
6.234 @@ -512,8 +498,8 @@
6.235 | SOME descr1 => descr1 = descr2 andalso Model_Def.member_vnt vnts1 max_vnt) i1_model of
6.236 NONE =>
6.237 (i2, [max_vnt], bool2, m_field2, (Sup_POS (descr2, ts2), pos2)) (*the present in i2_model*)
6.238 - | SOME i1_single => i1_single) (*shift the item from i1_model to i2_model*)
6.239 - | add_other _ _ i2_single = i2_single (*keep all the other items in i2_model*)
6.240 + | SOME i1_single => i1_single) (*shift the item from i1_model to i2_model*)
6.241 + | add_other _ _ i2_single = i2_single (*keep all the other items in i2_model*)
6.242
6.243 (*fill method from items already input*)
6.244 fun fill_method o_model (pbl_imod, met_imod) met_patt =
7.1 --- a/src/Tools/isac/Specify/m-match.sml Fri Dec 01 06:08:22 2023 +0100
7.2 +++ b/src/Tools/isac/Specify/m-match.sml Tue Dec 05 18:15:45 2023 +0100
7.3 @@ -31,7 +31,6 @@
7.4 val by_formalise : Formalise.model -> Problem.T -> match'
7.5
7.6 (*from isac_test for Minisubpbl*)
7.7 - val chk1_: Model_Pattern.T -> O_Model.single -> I_Model.T
7.8 val contains_o: Model_Def.descriptor -> O_Model.T -> bool
7.9
7.10 \<^isac_test>\<open>
7.11 @@ -116,8 +115,8 @@
7.12 val (bool, (itms, where_')) = data_by_o ctxt oris (model, where_, where_rls);
7.13 in
7.14 if bool
7.15 - then Matches' (P_Model.from thy (I_Model.TEST_to_OLD itms) where_')
7.16 - else NoMatch' (P_Model.from thy (I_Model.TEST_to_OLD itms) where_')
7.17 + then Matches' (P_Model.from thy itms where_')
7.18 + else NoMatch' (P_Model.from thy itms where_')
7.19 end;
7.20
7.21 (* split type-wrapper from program-arg and build part of an ori;
8.1 --- a/src/Tools/isac/Specify/p-model.sml Fri Dec 01 06:08:22 2023 +0100
8.2 +++ b/src/Tools/isac/Specify/p-model.sml Tue Dec 05 18:15:45 2023 +0100
8.3 @@ -17,7 +17,8 @@
8.4 | Missing of TermC.as_string | Superfl of string | SyntaxE of string | TypeE of string
8.5 type 'a model (*shall be dropped with PIDE*)
8.6
8.7 - val from : theory -> I_Model.T -> Pre_Conds.T -> T
8.8 + val from: theory -> I_Model.T_POS -> Pre_Conds.T ->
8.9 + {Find: item list, Given: item list, Relate: item list, Where: item list, With: item list}
8.10
8.11 val to_list: 'a model -> 'a list
8.12 val mk_delete: theory -> string -> I_Model.feedback -> Tactic.input
8.13 @@ -76,7 +77,6 @@
8.14
8.15 (** build T **)
8.16
8.17 -(*T_POSold*)
8.18 fun item_from_feedback thy (I_Model.Cor ((d, ts), _)) = Correct (UnparseC.term_in_thy thy (Input_Descript.join (d, ts)))
8.19 | item_from_feedback _ (I_Model.Syn c) = SyntaxE c
8.20 | item_from_feedback _ (I_Model.Typ c) = TypeE c
8.21 @@ -84,12 +84,13 @@
8.22 | item_from_feedback thy (I_Model.Sup (d, ts)) = Superfl (UnparseC.term_in_thy thy (Input_Descript.join (d, ts)))
8.23 | item_from_feedback thy (I_Model.Mis (d, pid)) = Missing (UnparseC.term_in_thy thy d ^ " " ^ UnparseC.term_in_thy thy pid)
8.24 | item_from_feedback _ _ = raise ERROR "item_from_feedback: uncovered definition"
8.25 -(*T_POS* )
8.26 -fun item_from_feedback_POS thy (I_Model.Cor_POS ((d, ts), _)) = Correct (UnparseC.term_in_thy thy (Input_Descript.join (d, ts)))
8.27 +fun item_from_feedback_POS thy (I_Model.Cor_POS ((d, ts))) =
8.28 + Correct (UnparseC.term_in_thy thy (Input_Descript.join (d, ts)))
8.29 | item_from_feedback_POS _ (I_Model.Syn_POS c) = SyntaxE c
8.30 - | item_from_feedback_POS thy (I_Model.Inc_POS ((d, ts), _)) = Incompl (UnparseC.term_in_thy thy (Input_Descript.join (d, ts)))
8.31 - | item_from_feedback_POS thy (I_Model.Sup_POS (d, ts)) = Superfl (UnparseC.term_in_thy thy (Input_Descript.join (d, ts)))
8.32 -( *T_POSnew*)
8.33 + | item_from_feedback_POS thy (I_Model.Inc_POS ((d, ts))) =
8.34 + Incompl (UnparseC.term_in_thy thy (Input_Descript.join (d, ts)))
8.35 + | item_from_feedback_POS thy (I_Model.Sup_POS (d, ts)) =
8.36 + Superfl (UnparseC.term_in_thy thy (Input_Descript.join (d, ts)))
8.37
8.38 fun add_sel_ppc (_: theory) sel {Given = gi, Where = wh, Find = fi, With = wi, Relate = re} x =
8.39 case sel of
8.40 @@ -106,12 +107,12 @@
8.41 fun boolterm2item ctxt (true, term) = Correct (UnparseC.term ctxt term)
8.42 | boolterm2item ctxt(false, term) = False (UnparseC.term ctxt term);
8.43
8.44 -fun from thy itms where_ =
8.45 +fun from thy i_model where_ =
8.46 let
8.47 fun coll model [] = model
8.48 - | coll model ((_, _, _, field, itm_) :: itms) =
8.49 - coll (add_sel_ppc thy field model (item_from_feedback thy itm_)) itms;
8.50 - val gfr = coll empty itms;
8.51 + | coll model ((_, _, _, field, (feedb, _)) :: itms) =
8.52 + coll (add_sel_ppc thy field model (item_from_feedback_POS thy feedb)) itms;
8.53 + val gfr = coll empty i_model;
8.54 in add_where gfr (map (boolterm2item (Proof_Context.init_global thy)) where_) end;
8.55
8.56 fun mk_delete thy "#Given" itm_ = Tactic.Del_Given (I_Model.to_p_model thy itm_)
9.1 --- a/src/Tools/isac/Specify/p-spec.sml Fri Dec 01 06:08:22 2023 +0100
9.2 +++ b/src/Tools/isac/Specify/p-spec.sml Tue Dec 05 18:15:45 2023 +0100
9.3 @@ -2,7 +2,8 @@
9.4 Author: Walther Neuper
9.5 (c) due to copyright terms
9.6
9.7 -This will be dropped at switch to Isabelle/PIDE .
9.8 +Major parts will be dropped at switch to Isabelle/PIDE.
9.9 +Thus the switch to I_Model.T_POS is prepared quick and dirty.
9.10 *)
9.11
9.12 signature PRESENTATION_SPECIFICATION =
9.13 @@ -17,11 +18,11 @@
9.14 type icalhd = Pos.pos' * TermC.as_string * imodel * Pos.pos_ * References.T
9.15 val empty: icalhd
9.16 val input_icalhd : Ctree.ctree -> icalhd -> Ctree.ctree * SpecificationC.T
9.17 -\<^isac_test>\<open>
9.18 +(*/----- from isac_test for Minisubpbl*)
9.19 val appl_add': ThyC.id -> O_Model.T -> I_Model.T -> Model_Pattern.T ->
9.20 string * TermC.as_string -> I_Model.single
9.21 val appl_adds: ThyC.id -> O_Model.T -> I_Model.T -> Model_Pattern.T ->
9.22 - (string * TermC.as_string) list -> I_Model.T
9.23 + (Model_Def.m_field * TermC.as_string) list -> I_Model.T
9.24 val eq7: ''a * ''b -> ''a * (''b * 'c) -> bool
9.25 val fstr2itm_: theory -> (''a * (term * term)) list -> ''a * string ->
9.26 int list * bool * ''a * I_Model.feedback (*I_Model.single'*)
9.27 @@ -32,6 +33,10 @@
9.28 val unknown_expl: ThyC.id -> (''a * (term * term)) list -> (*Model_Pattern.T*)
9.29 (''a * string) list ->
9.30 (int * int list * bool * ''a * Model_Def.i_model_feedback) list (*I_Model.T*)
9.31 +(*\----- from isac_test for Minisubpbl*)
9.32 +
9.33 +\<^isac_test>\<open>
9.34 +(**)
9.35 \<close>
9.36 (*\------- rename -------/*)
9.37 end
9.38 @@ -82,8 +87,8 @@
9.39 | SOME t =>
9.40 (case O_Model.contains ctxt sel oris t of
9.41 ("", ori', all) =>
9.42 - (case I_Model.is_notyet_input ctxt model all ori' pbt of
9.43 - ("",itm) => itm
9.44 + (case I_Model.is_notyet_input ctxt (I_Model.OLD_to_POS model) all ori' pbt of
9.45 + ("", itm) => I_Model.TEST_to_OLD_single itm
9.46 | (msg,_) => raise ERROR ("appl_add': " ^ msg))
9.47 | (_, (i, v, _, d, ts), _) =>
9.48 if is_e_ts ts
10.1 --- a/src/Tools/isac/Specify/pre-conditions.sml Fri Dec 01 06:08:22 2023 +0100
10.2 +++ b/src/Tools/isac/Specify/pre-conditions.sml Tue Dec 05 18:15:45 2023 +0100
10.3 @@ -148,9 +148,9 @@
10.4 end
10.5
10.6 fun get_values (Cor_POS (_, values)) = values
10.7 + | get_values (Syn_POS _) = raise ERROR "Pre_Conds.get_values not for Syn_POS"
10.8 | get_values (Inc_POS (_, values)) = values
10.9 | get_values (Sup_POS (_, values)) = values
10.10 - | get_values _ = raise ERROR "get_descr from item without this description"
10.11
10.12 (*
10.13 get an appropriate (description, variant)-item from i_model, otherwise return empty item,
11.1 --- a/src/Tools/isac/Specify/refine.sml Fri Dec 01 06:08:22 2023 +0100
11.2 +++ b/src/Tools/isac/Specify/refine.sml Tue Dec 05 18:15:45 2023 +0100
11.3 @@ -150,8 +150,8 @@
11.4 M_Match.data_by_o ctxt oris (model, where_, where_rls)
11.5 in
11.6 if b
11.7 - then pbls @ [M_Match.Matches (rev (pblRD @ [pI]), P_Model.from thy (I_Model.TEST_to_OLD itms) where_')]
11.8 - else pbls @ [M_Match.NoMatch (rev (pblRD @ [pI]), P_Model.from thy (I_Model.TEST_to_OLD itms) where_')]
11.9 + then pbls @ [M_Match.Matches (rev (pblRD @ [pI]), P_Model.from thy itms where_')]
11.10 + else pbls @ [M_Match.NoMatch (rev (pblRD @ [pI]), P_Model.from thy itms where_')]
11.11 end
11.12 | refin' ctxt pblRD fmz pbls (Store.Node (pI, [py], pys)) =
11.13 let
11.14 @@ -165,9 +165,9 @@
11.15 in
11.16 if b
11.17 then
11.18 - let val pbl = M_Match.Matches (rev (pblRD @ [pI]), P_Model.from thy (I_Model.TEST_to_OLD itms) where_')
11.19 + let val pbl = M_Match.Matches (rev (pblRD @ [pI]), P_Model.from thy itms where_')
11.20 in refins' ctxt (pblRD @ [pI]) fmz (pbls @ [pbl]) pys end
11.21 - else (pbls @ [M_Match.NoMatch (rev (pblRD @ [pI]), P_Model.from thy (I_Model.TEST_to_OLD itms) where_')])
11.22 + else (pbls @ [M_Match.NoMatch (rev (pblRD @ [pI]), P_Model.from thy itms where_')])
11.23 end
11.24 | refin' _ _ _ _ _ = raise ERROR "refin': uncovered fun def."
11.25 and refins' _ _ _ pbls [] = pbls
12.1 --- a/src/Tools/isac/Specify/specify.sml Fri Dec 01 06:08:22 2023 +0100
12.2 +++ b/src/Tools/isac/Specify/specify.sml Tue Dec 05 18:15:45 2023 +0100
12.3 @@ -156,7 +156,8 @@
12.4 case I_Model.check_single ctxt m_field oris i_model m_patt ct of
12.5 I_Model.Add i_single => (*..union old input *)
12.6 let
12.7 - val i_model' = I_Model.add_single (Proof_Context.theory_of ctxt) i_single i_model
12.8 + val i_model' = I_Model.add_single (Proof_Context.theory_of ctxt)
12.9 + (I_Model.TEST_to_OLD_single i_single) i_model
12.10 val tac' = I_Model.make_tactic m_field (ct, i_model')
12.11 val (_, _, _, pt') = Specify_Step.add tac' (Istate_Def.Uistate, ctxt) (pt, pos)
12.12 in
13.1 --- a/src/Tools/isac/Test_Code/test-code.sml Fri Dec 01 06:08:22 2023 +0100
13.2 +++ b/src/Tools/isac/Test_Code/test-code.sml Tue Dec 05 18:15:45 2023 +0100
13.3 @@ -49,7 +49,7 @@
13.4 Pos.Pbl => Test_Out.Problem []
13.5 | Pos.Met => Test_Out.MethodC []
13.6 | _ => raise ERROR "TESTg_form: uncovered case"),
13.7 - P_Model.from (Proof_Context.theory_of ctxt) gfr where_)
13.8 + P_Model.from (Proof_Context.theory_of ctxt) (I_Model.OLD_to_POS gfr) where_)
13.9 end
13.10 (* for quick test-print-out, until 'type inout' is removed *)
13.11 fun f2str (Test_Out.FormKF cterm') = cterm'
14.1 --- a/test/Tools/isac/Minisubpbl/100-init-rootpbl.sml Fri Dec 01 06:08:22 2023 +0100
14.2 +++ b/test/Tools/isac/Minisubpbl/100-init-rootpbl.sml Tue Dec 05 18:15:45 2023 +0100
14.3 @@ -66,7 +66,7 @@
14.4
14.5 (*val return =*)
14.6 Test_Out.PpcKF (Test_Out.Problem [],
14.7 - P_Model.from (Proof_Context.theory_of ctxt) gfr where_);
14.8 + P_Model.from (Proof_Context.theory_of ctxt) (I_Model.OLD_to_POS gfr) where_);
14.9 "~~~~~ fun from , args:"; val (thy, itms, where_) = ((Proof_Context.theory_of ctxt), gfr, where_);
14.10
14.11 (*//------------------ inserted hidden code ------------------------------------------------\\*)
15.1 --- a/test/Tools/isac/Minisubpbl/150a-add-given-Maximum.sml Fri Dec 01 06:08:22 2023 +0100
15.2 +++ b/test/Tools/isac/Minisubpbl/150a-add-given-Maximum.sml Tue Dec 05 18:15:45 2023 +0100
15.3 @@ -108,10 +108,11 @@
15.4
15.5 (** )val i_model' =( **)
15.6 (**)val return_add_single =(**)
15.7 - I_Model.add_single (Proof_Context.theory_of ctxt) i_single i_model;
15.8 + I_Model.add_single (Proof_Context.theory_of ctxt)
15.9 + (I_Model.TEST_to_OLD_single i_single) i_model;
15.10 (*/////--------------- step add_single -----------------------------------------------------\\*)
15.11 "~~~~~ fun add_single , args:"; val (thy, itm, model) =
15.12 - ((Proof_Context.theory_of ctxt), i_single, i_model);
15.13 + ((Proof_Context.theory_of ctxt), I_Model.TEST_to_OLD_single i_single, i_model);
15.14 fun eq_untouched d (0, _, _, _, itm_) = (d = I_Model.descriptor itm_)
15.15 | eq_untouched _ _ = false
15.16 val model' = case I_Model.seek_ppc (#1 itm) model of
16.1 --- a/test/Tools/isac/Specify/i-model.sml Fri Dec 01 06:08:22 2023 +0100
16.2 +++ b/test/Tools/isac/Specify/i-model.sml Tue Dec 05 18:15:45 2023 +0100
16.3 @@ -170,14 +170,15 @@
16.4 (*+*)val [Free ("q_0", _)] = all;
16.5
16.6 (**)val ("", itm) =(**)
16.7 - (*case*) is_notyet_input ctxt i_model all ori' m_patt (*of*);
16.8 + (*case*) is_notyet_input ctxt (OLD_to_POS i_model) all ori' m_patt (*of*);
16.9
16.10 -(*+*)val (2, [1], true, "#Given", Cor ((Const (\<^const_name>\<open>Streckenlast\<close>, _), [Free ("q_0", _)]), (Free ("q_q", _), [Free ("q_0", _)]))) = itm
16.11 +(*+*)val (2, [1], true, "#Given", (Cor_POS (Const (\<^const_name>\<open>Streckenlast\<close>, _), [Free ("q_0", _)]), _)) = itm
16.12 (*\\------------------ step into check_single ----------------------------------------------//*)
16.13 val return_check_single = Add itm;
16.14
16.15 "~~~~~ from fun check_single \<longrightarrow>fun by_Add_ , return:"; val (I_Model.Add i_single) = (return_check_single);
16.16 - val i_model' = I_Model.add_single (Proof_Context.theory_of ctxt) i_single i_model
16.17 + val i_model' = I_Model.add_single (Proof_Context.theory_of ctxt)
16.18 + (I_Model.TEST_to_OLD_single i_single) i_model
16.19 val tac' = I_Model.make_tactic m_field (ct, i_model')
16.20 ;
16.21 (*+*)if I_Model.to_string ctxt i_model' = "[\n" ^