1.1 --- a/src/Tools/isac/Specify/i-model.sml Mon Nov 20 10:49:54 2023 +0100
1.2 +++ b/src/Tools/isac/Specify/i-model.sml Fri Nov 24 15:34:07 2023 +0100
1.3 @@ -61,8 +61,8 @@
1.4 -> message * single
1.5 val get_field_term: theory -> O_Model.single -> single -> m_field * TermC.as_string
1.6
1.7 +(*OLD* )
1.8 val add: single -> T -> T
1.9 -(*OLD* )
1.10 val handle_atom: values -> values
1.11 ( *---*)
1.12 val unpack_values: descriptor * values -> values
1.13 @@ -92,7 +92,7 @@
1.14 val feedb_args_to_string: Proof.context -> feedback_TEST -> string
1.15 (*NEW*)
1.16
1.17 - val ori_2itm: feedback -> descriptor -> Model_Pattern.values -> O_Model.single -> single
1.18 + val ori_2itm: feedback -> descriptor -> Model_Def.values -> O_Model.single -> single
1.19 val seek_ppc: int -> T -> single option
1.20 val overwrite_ppc: theory -> single -> T -> T
1.21 (*\----- from isac_test for Minisubpbl*)
1.22 @@ -115,7 +115,7 @@
1.23 type variants = Model_Def.variants;
1.24 type m_field = Model_Def.m_field;
1.25 type descriptor = Model_Def.descriptor;
1.26 -type values = Model_Pattern.values
1.27 +type values = Model_Def.values
1.28
1.29 type T = Model_Def.i_model_single list;
1.30 (* for developing input from PIDE, we use T_TEST with these ideas:
1.31 @@ -185,22 +185,39 @@
1.32 | feedback_TEST_to_string ctxt (Sup_TEST (d, ts)) =
1.33 "Sup_TEST " ^ UnparseC.term ctxt (Input_Descript.join (d, ts))
1.34
1.35 +(*OLD* )
1.36 fun descr_vals_to_string ctxt (descr, values) =
1.37 - if Pre_Conds.is_list_descr descr
1.38 + if Model_Def.is_list_descr descr
1.39 then if Pre_Conds.is_NObrack_list descr
1.40 then UnparseC.term ctxt descr ^ " " ^ UnparseC.terms_NObrack ctxt values
1.41 - else UnparseC.term ctxt descr ^ " " ^ UnparseC.terms(*_NObrack*) ctxt values(* ^ "]"*)
1.42 + else UnparseC.term ctxt descr ^ " " ^ UnparseC.terms ctxt values
1.43 else if TermC.is_atom (hd values)
1.44 then UnparseC.term ctxt descr ^ " " ^ UnparseC.term ctxt (hd values)
1.45 else UnparseC.term ctxt descr ^ " (" ^ UnparseC.term ctxt (hd values) ^ ")"
1.46 +( *---*)
1.47 +fun descr_vals_to_string ctxt (descr, values) =
1.48 + UnparseC.term ctxt (descr $ Model_Def.dest_values values)
1.49 +(*NEW*)
1.50
1.51 (*prepare for presentation to user; thus Syn_TEST does NOT raise an exn*)
1.52 +(*OLD*)
1.53 fun feedb_args_to_string ctxt (Cor_TEST (descr, values)) = descr_vals_to_string ctxt (descr, values)
1.54 | feedb_args_to_string _ (Syn_TEST str) = str
1.55 | feedb_args_to_string ctxt (Inc_TEST (descr, [])) =
1.56 UnparseC.term ctxt descr ^ Model_Pattern.empty_for descr
1.57 | feedb_args_to_string ctxt (Inc_TEST (descr, values)) = descr_vals_to_string ctxt (descr, values)
1.58 | feedb_args_to_string ctxt (Sup_TEST (descr, values)) = descr_vals_to_string ctxt (descr, values)
1.59 +(*---*)
1.60 +fun feedb_args_to_string ctxt (Cor_TEST (descr, values)) =
1.61 + UnparseC.term ctxt (descr $ Model_Def.dest_values values)
1.62 + | feedb_args_to_string _ (Syn_TEST str) = str
1.63 + | feedb_args_to_string ctxt (Inc_TEST (descr, [])) =
1.64 + UnparseC.term ctxt descr ^ Model_Pattern.empty_for descr
1.65 + | feedb_args_to_string ctxt (Inc_TEST (descr, values)) =
1.66 + UnparseC.term ctxt (descr $ Model_Def.dest_values values)
1.67 + | feedb_args_to_string ctxt (Sup_TEST (descr, values)) =
1.68 + UnparseC.term ctxt (descr $ Model_Def.dest_values values)
1.69 +(*NEW*)
1.70
1.71 fun single_to_string ctxt (i, is, b, s, itm_) =
1.72 "(" ^ string_of_int i ^ " ," ^ ints2str' is ^ " ," ^ bool2str b ^ " ," ^
1.73 @@ -504,22 +521,21 @@
1.74 (*NEW*)
1.75
1.76 (*OLD*)
1.77 -(*---*)
1.78 +fun is_NObrack_list (Const ("Input_Descript.solutions", _)) = true
1.79 + | is_NObrack_list (Const ("EqSystem.solution", _)) = true
1.80 + | is_NObrack_list (Const ("Biegelinie.Gleichungen", _)) = true
1.81 + | is_NObrack_list _ = false
1.82 fun unpack_values (descr, [t]) =
1.83 - if Pre_Conds.is_list_descr descr
1.84 - then if Pre_Conds.is_NObrack_list descr
1.85 + if Model_Def.is_list_descr descr
1.86 + then if is_NObrack_list descr
1.87 then [t]
1.88 else t |> TermC.isalist2list
1.89 else [t]
1.90 | unpack_values (_, ts) = ts |> map TermC.isalist2list |> flat
1.91 +(*---*)
1.92 (*NEW*)
1.93
1.94 (*OLD*)
1.95 -fun eq_dsc ((_, _, _, _, itm_), (_, _, _, _, iitm_)) = (descriptor itm_ = descriptor iitm_)
1.96 -(* insert_ppc = add for appl_add', input_icalhd 11.03,
1.97 - handles superfluous items carelessly *)
1.98 -(*---*)
1.99 -fun add itm itms = if member eq_dsc itms itm then itms else itms @ [itm] (* @ new itm *)
1.100 fun fill_from_o o_model (i, vnts, bool, _, (feedb, pos)) =
1.101 let
1.102 val (m_field, all_value) =
1.103 @@ -528,7 +544,7 @@
1.104 | NONE => raise ERROR "I_Model.fill_from_o does NOT find a descriptor in O_Model"
1.105 val descr = Pre_Conds.get_dscr'' feedb (*i_single has been filtered appropriately*)
1.106 in
1.107 - if Pre_Conds.is_list_descr descr
1.108 + if Model_Def.is_list_descr descr
1.109 then
1.110 let
1.111 val all_value' = unpack_values (descr, all_value)
1.112 @@ -542,6 +558,29 @@
1.113 end
1.114 else SOME (i, vnts, bool, m_field, (Cor_TEST (descr, all_value), pos))
1.115 end
1.116 +(*---*)
1.117 +fun fill_from_o o_model (i, vnts, bool, _, (feedb, pos)) =
1.118 + let
1.119 + val (m_field, all_values) =
1.120 + case find_first (fn (_, _, _, descr', _) => Pre_Conds.descriptor_exists descr' feedb) o_model of
1.121 + SOME (_, _, m_field, _, ts) => (m_field, ts)
1.122 + | NONE => raise ERROR "I_Model.fill_from_o does NOT find a descriptor in O_Model"
1.123 + val descr = Pre_Conds.get_dscr'' feedb (*i_single has been filtered appropriately*)
1.124 + in
1.125 +(*---------------vvvvvvvvvvvvv MV if TermC-is_list all_value-----*)
1.126 + if Model_Def.is_list_descr descr
1.127 + then
1.128 + let
1.129 + val already_input = feedb |> values_TEST'
1.130 + val miss = subtract op= already_input all_values (*"[[c], [c_2], [c_3], [c_4]]"*)
1.131 + val ts = already_input @ [hd miss]
1.132 + in
1.133 + if length all_values = length ts
1.134 + then SOME (i, vnts, bool, m_field, (Cor_TEST (descr, [Model_Def.dest_values ts]), pos))
1.135 + else SOME (i, vnts, bool, m_field, (Inc_TEST (descr, [Model_Def.dest_values ts]), pos))
1.136 + end
1.137 + else SOME (i, vnts, bool, m_field, (Cor_TEST (descr, all_values(*only 1 term*)), pos))
1.138 + end
1.139 (*NEW*)
1.140
1.141 (*