1.1 --- a/src/Tools/isac/Specify/pre-conditions.sml Wed Jul 26 11:12:55 2023 +0200
1.2 +++ b/src/Tools/isac/Specify/pre-conditions.sml Fri Aug 04 10:46:05 2023 +0200
1.3 @@ -22,11 +22,14 @@
1.4 val max_variant: Model_Def.i_model -> int
1.5 val environment: Model_Def.i_model -> Env.T
1.6
1.7 + (* WRONG ENVS *)
1.8 val check: Proof.context -> Rule_Set.T -> unchecked -> Model_Def.i_model -> 'a -> checked
1.9 - (*check_TEST is intermediately introduced for step-wise adapting test/* to I_Model.T_TEST
1.10 - in parallel to check, and will finally be replaced by check_from_store:*)
1.11 + (* WRONG ENVS *)
1.12 val check_from_store: Proof.context -> Rule_Set.T -> unchecked -> env_subst -> env_eval -> checked
1.13 -(*REN check_input: Proof.context -> Rule_Set.T -> unchecked_input -> env_eval -> checked_input*)
1.14 + (* vvv-replaces-^^^*)
1.15 + val check_envs_TEST: Proof.context -> Rule_Def.rule_set -> term list ->
1.16 + Env.T * (env_subst * env_eval) -> checked
1.17 + (* WRONG ENVS *)
1.18 val check_TEST : Proof.context -> Rule_Set.T -> unchecked_TEST -> env_eval -> checked_TEST
1.19
1.20 (*this makes the OLD tests run AFTER introduction of I_Model.T_TEST..*)
1.21 @@ -46,13 +49,13 @@
1.22 val sep_variants_envs_OLD: Model_Pattern.T -> Model_Def.i_model_TEST ->
1.23 env_subst * env_eval;
1.24
1.25 -(*T_TESTold* )
1.26 +(*T_TESTold*)
1.27 val of_max_variant: Model_Pattern.T -> Model_Def.i_model_TEST ->
1.28 Model_Def.i_model_TEST * env_subst * env_eval
1.29 -( *T_TEST*)
1.30 +(*T_TEST* )
1.31 val of_max_variant:Model_Pattern.T -> Model_Def.i_model_TEST ->
1.32 Model_Def.i_model_TEST * Env.T * (env_subst * env_eval)
1.33 -(*T_TESTnew*)
1.34 +( *T_TESTnew*)
1.35
1.36 (*from isac_test for Minisubpbl*)
1.37 val discern_feedback_subst: Model_Def.descriptor -> Model_Def.i_model_feedback_TEST -> Env.T;
1.38 @@ -511,23 +514,23 @@
1.39
1.40 fun mk_env_model _ (Model_Def.Cor_TEST ((_, []), _)) = []
1.41 | mk_env_model id (Model_Def.Cor_TEST ((descr, ts), _)) =
1.42 -(*T_TEST.150* )
1.43 +(*T_TEST.150*)
1.44 if Model_Pattern.is_list_descr descr
1.45 then [(id, TermC.list2isalist (Model_Pattern.typ_of_element descr) ts)]
1.46 else [(id, hd ts)]
1.47 -( *T_TEST*)
1.48 +(*T_TEST* )
1.49 handle_lists id (descr, ts)
1.50 -(*T_TEST.100*)
1.51 +( *T_TEST.100*)
1.52 | mk_env_model _ (Model_Def.Syn_TEST _) = [] (*TODO handle correct list elements*)
1.53 | mk_env_model _ (Model_Def.Inc_TEST ((_, []), _)) = []
1.54 | mk_env_model id (Model_Def.Inc_TEST ((descr, ts), _)) =
1.55 -(*T_TEST.150* )
1.56 +(*T_TEST.150*)
1.57 if Model_Pattern.is_list_descr descr
1.58 then [(id, TermC.list2isalist (Model_Pattern.typ_of_element descr) ts)]
1.59 else [(id, hd ts)]
1.60 -( *T_TEST*)
1.61 +(*T_TEST* )
1.62 handle_lists id (descr, ts)
1.63 -(*T_TEST.100*)
1.64 +( *T_TEST.100*)
1.65 | mk_env_model _ (Model_Def.Sup_TEST _) = []
1.66 fun make_env_model equal_descr_pairs =
1.67 map (fn ((_, (_, id)), (_, _, _, _, (feedb, _)))
1.68 @@ -578,12 +581,12 @@
1.69 fun cnt_corrects i_model =
1.70 fold (curry op +) (map (fn (_, _, _, _, (Cor_TEST _, _)) => 1 | _ => 0) i_model) 0;
1.71
1.72 -(*T_TESTold* )
1.73 +(*T_TESTold*)
1.74 fun of_max_variant model_patt i_model =
1.75 -( *T_TEST*)
1.76 +(*T_TEST* )
1.77 fun of_max_variant _ [] = ([], [], ([], []))
1.78 | of_max_variant model_patt i_model =
1.79 -(*T_TESTnew*)
1.80 +( *T_TESTnew*)
1.81 let
1.82 val all_variants =
1.83 map (fn (_, variants, _, _, _) => variants) i_model
1.84 @@ -597,13 +600,13 @@
1.85 val i_model_max =
1.86 filter (fn (_, variants, _ , _ ,_) => member (op =) variants max_variant) i_model
1.87 val equal_descr_pairs = map (get_equal_descr i_model) model_patt |> flat
1.88 -(*T_TESTold* )
1.89 +(*T_TESTold*)
1.90 val env_subst = mk_env_subst_DEL equal_descr_pairs
1.91 val env_eval = mk_env_eval_DEL i_model_max
1.92 in
1.93 (i_model_max, env_subst, env_eval)
1.94 end
1.95 -( *T_TEST*)
1.96 +(*T_TEST* )
1.97 val env_model = make_env_model equal_descr_pairs
1.98 val equal_givens = filter (fn ((m_field, _), _) => m_field = "#Given") equal_descr_pairs
1.99 val subst_eval_list = make_envs_preconds equal_givens
1.100 @@ -611,12 +614,12 @@
1.101 in
1.102 (i_model_max, env_model, (env_subst, env_eval))
1.103 end
1.104 -(*T_TESTnew*)
1.105 +( *T_TESTnew*)
1.106
1.107
1.108 (** check pre-conditions **)
1.109
1.110 -(* expects the precondition from Problem, ie. needs substitution *)
1.111 +(* WRONG ENVS expects the precondition from Problem, ie. needs substitution *)
1.112 fun check _ _ [] _ _ = (true, [])
1.113 | check ctxt where_rls pres pbl (_ (*I_Model.variants UNNECESSARY: I_Model.T filtered for*)) =
1.114 let
1.115 @@ -624,7 +627,7 @@
1.116 val pres' = map (TermC.subst_atomic_all env) pres;
1.117 val evals = map (eval ctxt where_rls) pres';
1.118 in (foldl and_ (true, map fst evals), evals) end;
1.119 -(* expects the precondition from PIDE, ie. already substituted *)
1.120 +(* WRONG ENVS expects the precondition from PIDE, ie. already substituted *)
1.121 fun check_TEST _ _ [] _ = (true, [])
1.122 | check_TEST ctxt where_rls preconds env_eval =
1.123 let
1.124 @@ -635,6 +638,7 @@
1.125 in
1.126 (foldl and_ (true, map fst evals), (map fst evals) ~~ preconds)
1.127 end;
1.128 +(* WRONG ENVS *)
1.129 fun check_from_store ctxt where_rls pres env_subst env_eval =
1.130 let
1.131 val pres_subst = map (TermC.subst_atomic_all env_subst) pres;
1.132 @@ -643,27 +647,41 @@
1.133 in
1.134 (foldl and_ (true, map fst evals), pres_subst)
1.135 end
1.136 -
1.137 +(* vvv-replaces-^^^*)
1.138 +fun check_envs_TEST ctxt where_rls pres (env_model, (env_subst, env_eval)) =
1.139 + let
1.140 + val pres_subst = map (TermC.subst_atomic_all env_subst) pres;
1.141 + val pres_subst_other = map (TermC.subst_atomic_all env_model) (map #2 pres_subst);
1.142 + val full_subst = if env_eval = [] then pres_subst_other
1.143 + else map (TermC.subst_atomic_all env_eval) (map #2 pres_subst_other)
1.144 + val evals = map (eval ctxt where_rls) full_subst
1.145 + in
1.146 + (foldl and_ (true, map fst evals), pres_subst_other)
1.147 + end
1.148
1.149 (* expects the precondition from Problem, ie. needs substitution by env_model*)
1.150 fun check_OLD _ _ [] _ = (true, [])
1.151 | check_OLD ctxt where_rls pres (model_patt, i_model) =
1.152 let
1.153 -(*T_TESTold* )
1.154 +(*T_TESTold*)
1.155 val (env_subst, env_eval) = sep_variants_envs_OLD model_patt i_model
1.156 val pres_subst = map (TermC.subst_atomic_all env_subst) pres;
1.157 val full_subst = map (fn (bool, t) => (bool, subst_atomic env_eval t)) pres_subst
1.158 -( *T_TEST*)
1.159 + val evals = map (eval ctxt where_rls) full_subst
1.160 + in
1.161 + (foldl and_ (true, map fst evals), pres_subst)
1.162 + end;
1.163 +(*T_TEST* )
1.164 val (_, env_model, (env_subst, env_eval)) = of_max_variant model_patt i_model
1.165 val pres_subst = map (TermC.subst_atomic_all env_subst) pres;
1.166 val pres_subst_other = map (TermC.subst_atomic_all env_model) (map #2 pres_subst);
1.167 val full_subst = if env_eval = [] then pres_subst_other
1.168 else map (TermC.subst_atomic_all env_eval) (map #2 pres_subst_other)
1.169 -(*T_TESTnew*)
1.170 val evals = map (eval ctxt where_rls) full_subst
1.171 in
1.172 (foldl and_ (true, map fst evals), pres_subst_other)
1.173 end;
1.174 +( *T_TESTnew*)
1.175
1.176 fun unchecked_OLD_to_TEST pres = map (fn t => (t, Position.none)) pres
1.177