1.1 --- a/src/Tools/isac/Specify/pre-conditions.sml Fri Jul 14 12:33:25 2023 +0200
1.2 +++ b/src/Tools/isac/Specify/pre-conditions.sml Sat Jul 15 17:44:37 2023 +0200
1.3 @@ -50,8 +50,8 @@
1.4 val of_max_variant: Model_Pattern.T -> Model_Def.i_model_TEST ->
1.5 Model_Def.i_model_TEST * env_subst * env_eval
1.6 (*T_TEST* )
1.7 - val of_max_variant: Model_Pattern.T -> Model_def.i_model_TEST -> Model_def.i_model_TEST * Env.T
1.8 -(*val mk_envs: Model_def.i_model_TEST -> unchecked -> env_subst * env_eval*)
1.9 + val of_max_variant:Model_Pattern.T -> Model_Def.i_model_TEST ->
1.10 + Model_Def.i_model_TEST * Env.T * (env_subst * env_eval)
1.11 ( *T_TESTnew*)
1.12
1.13 (*from isac_test for Minisubpbl*)
1.14 @@ -82,12 +82,19 @@
1.15 val all_atoms: term list -> bool
1.16 val all_lhs_atoms: term list -> bool
1.17
1.18 -\<^isac_test>\<open>
1.19 -(**)
1.20 +\<^isac_test>\<open>
1.21 + val mk_env_model: term -> Model_Def.i_model_feedback_TEST -> Env.T
1.22 + val switch_type: Model_Pattern.descriptor -> typ -> Model_Pattern.descriptor
1.23 + val discern_typ: term -> Model_Pattern.descriptor * term list ->
1.24 + ((term * term) * (term * term)) list
1.25 + val discern_feedback: term -> Model_Def.i_model_feedback_TEST ->
1.26 + ((term * term) * (term * term)) list
1.27 + val make_envs_preconds: (Model_Pattern.single * Model_Def.i_model_single_TEST) list ->
1.28 + ((term * term) * (term * term)) list
1.29
1.30 \<close>
1.31 end
1.32 -
1.33 +
1.34 (**)
1.35 structure Pre_Conds(**) : PRE_CONDITIONS(**) =
1.36 struct
1.37 @@ -106,7 +113,7 @@
1.38 Model_Pattern.T.
1.39 Env.T / (Constants, fixes) in Model_Pattern.T
1.40 e.g.[(fixes, [r = 7])] |
1.41 - > (Constants, [r = 7]) in O/I_Model.T *)
1.42 + > (Constants, [<r = 7>]) in O/I_Model.T *)
1.43
1.44 (*2*) type env_subst = Env.T (* / 0 < fixes in Problem.{where_, ...}
1.45 eg. [(fixes, r)] |
1.46 @@ -493,24 +500,48 @@
1.47
1.48 (** of_max_variant **)
1.49
1.50 -(*T_TEST* )
1.51 -fun mk_env_mod _ (Model_Def.Cor_TEST ((_, []), _)) = []
1.52 - | mk_env_mod id (Model_Def.Cor_TEST ((descr, ts), _)) =
1.53 - if is_list_descr descr
1.54 +(*T_TESTold*)
1.55 +(*T_TEST*)
1.56 +fun mk_env_model _ (Model_Def.Cor_TEST ((_, []), _)) = []
1.57 + | mk_env_model id (Model_Def.Cor_TEST ((descr, ts), _)) =
1.58 + if Model_Pattern.is_list_descr descr
1.59 then [(id, TermC.list2isalist (Model_Pattern.typ_of_element descr) ts)]
1.60 else [(id, hd ts)]
1.61 - | mk_env_mod _ (Model_Def.Syn_TEST _) = [] (*TODO handle correct list elements*)
1.62 - | mk_env_mod _ (Model_Def.Inc_TEST ((_, []), _)) = []
1.63 - | mk_env_mod id (Model_Def.Inc_TEST ((descr, ts), _)) =
1.64 - if is_list_descr descr
1.65 + | mk_env_model _ (Model_Def.Syn_TEST _) = [] (*TODO handle correct list elements*)
1.66 + | mk_env_model _ (Model_Def.Inc_TEST ((_, []), _)) = []
1.67 + | mk_env_model id (Model_Def.Inc_TEST ((descr, ts), _)) =
1.68 + if Model_Pattern.is_list_descr descr
1.69 then [(id, TermC.list2isalist (Model_Pattern.typ_of_element descr) ts)]
1.70 else [(id, hd ts)]
1.71 - | mk_env_mod _ (Model_Def.Sup_TEST _) = []
1.72 -fun mk_env_model equal_descr_pairs =
1.73 + | mk_env_model _ (Model_Def.Sup_TEST _) = []
1.74 +fun make_env_model equal_descr_pairs =
1.75 map (fn ((_, (_, id)), (_, _, _, _, (feedb, _)))
1.76 - => (mk_env_mod id feedb)) equal_descr_pairs
1.77 + => (mk_env_model id feedb)) equal_descr_pairs
1.78 |> flat
1.79 -( *T_TESTnew*)
1.80 +
1.81 +fun switch_type_TEST descr [] = descr
1.82 + | switch_type_TEST (Free (id_string, _)) ts =
1.83 + Const (id_string, ts |> hd |> TermC.lhs |> type_of)
1.84 + | switch_type_TEST descr _ = raise ERROR ("switch_type undefined argument " ^
1.85 + quote (UnparseC.term (ContextC.for_ERROR ()) descr))
1.86 +fun discern_typ _ (_, []) = []
1.87 + | discern_typ id (descr, ts) =
1.88 + if Model_Pattern.typ_of_element descr = HOLogic.boolT
1.89 + andalso ts |> map TermC.lhs |> all_atoms
1.90 + then
1.91 + if length ts > 1
1.92 + then raise ERROR "model items of type 'bool' in lists with 'lengt ts > 1' NOT YET IMPLEMENTED"
1.93 + else [((switch_type_TEST id ts, TermC.lhs (hd ts)),
1.94 + (TermC.lhs (hd ts), TermC.rhs (hd ts)))]
1.95 + else []
1.96 +fun discern_feedback id (Model_Def.Cor_TEST ((descr, ts), _)) = discern_typ id (descr, ts)
1.97 + | discern_feedback _ (Model_Def.Syn_TEST _) = [] (*TODO: handle correct elements*)
1.98 + | discern_feedback id (Model_Def.Inc_TEST ((descr, ts), _)) = discern_typ id (descr, ts)
1.99 + | discern_feedback _ (Model_Def.Sup_TEST _) = []
1.100 +fun make_envs_preconds equal_givens =
1.101 + map (fn ((_, (_, id)), (_, _, _, _, (feedb, _))) => discern_feedback id feedb) equal_givens
1.102 + |> flat
1.103 +(*T_TESTnew*)
1.104
1.105 (* filter_variants': Model_Def.i_model_TEST -> Model_Def.variant -> Model_Def.i_model_TEST*)
1.106 fun filter_variants' i_singles n =
1.107 @@ -542,9 +573,12 @@
1.108 (i_model_max, env_subst, env_eval)
1.109 end
1.110 (*T_TEST* )
1.111 - val env_model = mk_env_model equal_descr_pairs
1.112 + val env_model = make_env_model equal_descr_pairs
1.113 + val equal_givens = filter (fn ((m_field, _), _) => m_field = "#Given") equal_descr_pairs
1.114 + val subst_eval_list = make_envs_preconds equal_givens
1.115 + val (env_subst, env_eval) = split_list subst_eval_list
1.116 in
1.117 - (i_model_max, env_model)
1.118 + (i_model_max, env_model, (env_subst, env_eval))
1.119 end
1.120 ( *T_TESTnew*)
1.121
1.122 @@ -584,7 +618,11 @@
1.123 fun check_OLD _ _ [] _ = (true, [])
1.124 | check_OLD ctxt where_rls pres (model_patt, i_model) =
1.125 let
1.126 +(*T_TESTold*)
1.127 val (env_subst, env_eval) = sep_variants_envs_OLD model_patt i_model
1.128 +(*T_TEST* )
1.129 + val (_, _, (env_subst, env_eval)) = of_max_variant model_patt i_model
1.130 +( *T_TESTnew*)
1.131 val pres_subst = map (TermC.subst_atomic_all env_subst) pres;
1.132 val full_subst = map (fn (bool, t) => (bool, subst_atomic env_eval t)) pres_subst
1.133 val evals = map (eval ctxt where_rls) full_subst