1.1 --- a/src/Tools/isac/Specify/pre-conditions.sml Sun Aug 27 16:09:04 2023 +0200
1.2 +++ b/src/Tools/isac/Specify/pre-conditions.sml Sun Aug 27 16:48:03 2023 +0200
1.3 @@ -7,11 +7,9 @@
1.4 sig
1.5 type T
1.6 type unchecked
1.7 -(*RENA unchecked_pos*)
1.8 - type unchecked_TEST
1.9 + type unchecked_pos
1.10 type checked
1.11 -(*RENA checked_pos*)
1.12 - type checked_TEST
1.13 + type checked_pos
1.14
1.15 type env_subst
1.16 type env_eval
1.17 @@ -26,11 +24,11 @@
1.18 val of_max_variant: Model_Pattern.T -> Model_Def.i_model_TEST ->
1.19 Model_Def.i_model_TEST * Env.T * (env_subst * env_eval)
1.20
1.21 - val check_pos: Proof.context -> Rule_Set.T -> unchecked_TEST ->
1.22 - Model_Pattern.T * Model_Def.i_model_TEST -> checked_TEST
1.23 - val check_envs_TEST: Proof.context -> Rule_Set.T -> unchecked -> Env.T * (env_subst * env_eval)
1.24 + val check_pos: Proof.context -> Rule_Set.T -> unchecked_pos ->
1.25 + Model_Pattern.T * Model_Def.i_model_TEST -> checked_pos
1.26 + val check_envs: Proof.context -> Rule_Set.T -> unchecked -> Env.T * (env_subst * env_eval)
1.27 -> checked
1.28 - val check_OLD: Proof.context -> Rule_Set.T -> unchecked ->
1.29 + val check: Proof.context -> Rule_Set.T -> unchecked ->
1.30 Model_Pattern.T * Model_Def.i_model_TEST -> checked
1.31
1.32 (*from isac_test for Minisubpbl*)
1.33 @@ -38,13 +36,13 @@
1.34 (Model_Pattern.single * Model_Def.i_model_single_TEST) list
1.35 val unchecked_OLD_to_TEST: term list -> (term * Position.T) list
1.36
1.37 - val arrange_args1: int list -> int * Model_Def.variant list -> (int * Model_Def.variant) list
1.38 + val arrange_args: int list -> int * Model_Def.variant list -> (int * Model_Def.variant) list
1.39 val cnt_corrects: Model_Def.i_model_TEST -> int
1.40
1.41 val all_lhs_atoms: term list -> bool
1.42 val handle_lists: term -> Model_Def.descriptor * term list -> Env.T;
1.43 val filter_variants': Model_Def.i_model_TEST -> Model_Def.variant -> Model_Def.i_model_TEST
1.44 - val switch_type_TEST: Model_Def.descriptor -> term list -> Model_Def.descriptor;
1.45 + val switch_type: Model_Def.descriptor -> term list -> Model_Def.descriptor;
1.46 val discern_feedback: term -> Model_Def.i_model_feedback_TEST ->
1.47 ((term * term) * (term * term)) list
1.48 val discern_typ: term -> Model_Pattern.descriptor * term list ->
1.49 @@ -68,9 +66,9 @@
1.50
1.51 type T = Pre_Conds_Def.T; (*= (bool * term) list;*)
1.52 type unchecked = term list
1.53 -type unchecked_TEST = (term * Position.T) list
1.54 +type unchecked_pos = (term * Position.T) list
1.55 type checked = bool * (bool * term) list
1.56 -type checked_TEST = bool * ((bool * (term * Position.T)) list)
1.57 +type checked_pos = bool * ((bool * (term * Position.T)) list)
1.58
1.59 (*
1.60 we have three kinds of Env.T in the specification-phase:
1.61 @@ -187,10 +185,10 @@
1.62 => (mk_env_model id feedb)) equal_descr_pairs
1.63 |> flat
1.64
1.65 -fun switch_type_TEST descr [] = descr
1.66 - | switch_type_TEST (Free (id_string, _)) ts =
1.67 +fun switch_type descr [] = descr
1.68 + | switch_type (Free (id_string, _)) ts =
1.69 Free (id_string, ts |> hd |> TermC.lhs |> type_of)
1.70 - | switch_type_TEST descr _ = raise ERROR ("switch_type_TEST undefined argument " ^
1.71 + | switch_type descr _ = raise ERROR ("switch_type undefined argument " ^
1.72 quote (UnparseC.term (ContextC.for_ERROR ()) descr))
1.73
1.74 fun discern_typ _ (_, []) = []
1.75 @@ -209,7 +207,7 @@
1.76 if length ts > 1
1.77 then (writeln "model items of type 'bool' in lists with 'lengt ts > 1' NOT YET IMPLEMENTED";
1.78 [])
1.79 - else [((switch_type_TEST id ts, TermC.lhs (hd ts)),
1.80 + else [((switch_type id ts, TermC.lhs (hd ts)),
1.81 (TermC.lhs (hd ts), TermC.rhs (hd ts)))]
1.82 else []
1.83 (*TODO.md "review (descriptor, ts)" REMOVE--------------------------------------\*)
1.84 @@ -228,9 +226,9 @@
1.85 (* filter_variants': Model_Def.i_model_TEST -> Model_Def.variant -> Model_Def.i_model_TEST*)
1.86 fun filter_variants' i_singles n =
1.87 filter (fn (_, variants, _, _, _) => member op= variants n) i_singles
1.88 -(*arrange_args1: int list -> int * Model_Def.variant list -> (int * Model_Def.variant) list*)
1.89 -fun arrange_args1 [] _ = []
1.90 - | arrange_args1 (sum :: ss) (cnt, all) = (sum, nth cnt all) :: (arrange_args1 ss (cnt + 1, all))
1.91 +(*arrange_args: int list -> int * Model_Def.variant list -> (int * Model_Def.variant) list*)
1.92 +fun arrange_args [] _ = []
1.93 + | arrange_args (sum :: ss) (cnt, all) = (sum, nth cnt all) :: (arrange_args ss (cnt + 1, all))
1.94 (*cnt_corrects: I_Model.T_TEST -> int*)
1.95 fun cnt_corrects i_model =
1.96 fold (curry op +) (map (fn (_, _, _, _, (Cor_TEST _, _)) => 1 | _ => 0) i_model) 0;
1.97 @@ -244,7 +242,7 @@
1.98 |> distinct op =
1.99 val variants_separated = map (filter_variants' i_model) all_variants
1.100 val sums_corr = map (cnt_corrects) variants_separated
1.101 - val sum_variant_s = arrange_args1 sums_corr (1, all_variants)
1.102 + val sum_variant_s = arrange_args sums_corr (1, all_variants)
1.103 val (_, max_variant) = hd (*..crude decision, up to improvement *)
1.104 (sort (fn ((i, _), (j, _)) => int_ord (i, j)) sum_variant_s)
1.105 val i_model_max =
1.106 @@ -278,7 +276,7 @@
1.107 end;
1.108
1.109 (*takes the envs resulting from of_max_variant*)
1.110 -fun check_envs_TEST ctxt where_rls where_ (env_model, (env_subst, env_eval)) =
1.111 +fun check_envs ctxt where_rls where_ (env_model, (env_subst, env_eval)) =
1.112 let
1.113 val pres_subst = map (TermC.subst_atomic_all env_subst) where_;
1.114 val pres_subst_other = map (TermC.subst_atomic_all env_model) (map #2 pres_subst);
1.115 @@ -290,9 +288,9 @@
1.116 end
1.117
1.118 (*expects the precondition from Problem, ie. needs substitution by env_model*)
1.119 -(*TODO: check_OLD shall call check_envs_TEST*)
1.120 -fun check_OLD _ _ [] _ = (true, [])
1.121 - | check_OLD ctxt where_rls where_ (model_patt, i_model) =
1.122 +(*TODO: check shall call check_envs*)
1.123 +fun check _ _ [] _ = (true, [])
1.124 + | check ctxt where_rls where_ (model_patt, i_model) =
1.125 let
1.126 val (_, env_model, (env_subst, env_eval)) = of_max_variant model_patt i_model
1.127 val pres_subst = map (TermC.subst_atomic_all env_subst) where_;