1.1 --- a/src/Tools/isac/Specify/i-model.sml	Sat Apr 29 16:47:59 2023 +0200
     1.2 +++ b/src/Tools/isac/Specify/i-model.sml	Tue May 23 07:56:29 2023 +0200
     1.3 @@ -46,6 +46,7 @@
     1.4    val make_tactic: m_field -> TermC.as_string * T -> Tactic.T
     1.5    val descriptor: feedback -> descriptor
     1.6    val descriptor_TEST: feedback_TEST -> descriptor
     1.7 +  val descr_pairs_to_string: Proof.context -> (Model_Pattern.single * single_TEST) list -> string
     1.8    val o_model_values: feedback -> O_Model.values
     1.9    val variables: T -> term list
    1.10    val is_notyet_input : Proof.context -> T -> O_Model.values -> O_Model.single -> Model_Pattern.T
    1.11 @@ -67,8 +68,11 @@
    1.12    val is_complete_OLD: Proof.context -> Model_Pattern.T -> Rule_Def.rule_set ->
    1.13      Pre_Conds.unchecked -> T_TEST -> variants option
    1.14    val is_complete_variant: int -> T_TEST-> bool
    1.15 +
    1.16 +  val of_max_variant: Model_Pattern.T -> T_TEST -> T_TEST * Pre_Conds.env_subst * Pre_Conds.env_eval
    1.17 +
    1.18  (*from isac_test for Minisubpbl*)
    1.19 -  (**)
    1.20 +  val penv_to_string: Proof.context -> T -> string
    1.21   
    1.22  \<^isac_test>\<open>
    1.23    (**)
    1.24 @@ -233,12 +237,17 @@
    1.25    | descriptor_TEST (Sup_TEST (d, _)) = d
    1.26    | descriptor_TEST _ = raise ERROR "descriptor_TEST: uncovered case in fun.def.";
    1.27  
    1.28 +fun descr_pairs_to_string ctxt equal_descr_pairs =
    1.29 +(map (fn (a, b) => pair (Model_Pattern.pat2str ctxt a) (single_to_string_TEST ctxt b)
    1.30 +    |> pair2str) equal_descr_pairs)
    1.31 +  |> strs2str'
    1.32 +
    1.33  (*val string_of_descr_values: term * (term list) -> string
    1.34    fun string_of_descr_values (d, ts) = pair2str (UnparseC.term (ContextC.for_ERROR ()) d, UnparseC.terms ts);*)
    1.35 -fun penvval_in (Cor ((d, _), (_, ts))) = [Input_Descript.join'''' (d, ts)]
    1.36 +fun penvval_in (Cor ((d, _), (_, ts))) = (**)[Input_Descript.join'''' (d, ts)](** )------(**)[]( **)
    1.37    | penvval_in (Syn  (_)) = ((*tracing("*** penvval_in: Syn ("^c^")");*) [])
    1.38    | penvval_in (Typ  (_)) = ((*tracing("*** penvval_in: Typ ("^c^")");*) [])
    1.39 -  | penvval_in (Inc (_, (_, ts))) = ts
    1.40 +  | penvval_in (Inc (_, (_, ts))) = (**)ts(** )------------------------------------------(**)[]( **)
    1.41    | penvval_in (Sup _) = ((*tracing ("*** penvval_in: Sup " ^ string_of_descr_values dts);*) [])
    1.42    | penvval_in (Mis (_, _)) = ((*tracing ("*** penvval_in: Mis " ^
    1.43  			pair2str(UnparseC.term (ContextC.for_ERROR ()) d, UnparseC.term (ContextC.for_ERROR ()) t));*) [])
    1.44 @@ -496,4 +505,15 @@
    1.45      else SOME (map (fn x => if is_some x then [the x] else []) result_all_variants |> flat |> flat)
    1.46    end
    1.47  
    1.48 +val of_max_variant = Pre_Conds.of_max_variant
    1.49 +
    1.50 +(*get_penv: single -> (term * term list) list*)
    1.51 +fun get_penv (_, _, _, _, Cor (_, elem)) = [elem]
    1.52 +  | get_penv (_, _, _, _, Inc (_, elem)) = [elem]
    1.53 +  | get_penv _ = []
    1.54 +fun penv_to_string ctxt i_model = map get_penv i_model
    1.55 +  |> flat
    1.56 +  |> map (fn (t, ts) => pair2str (UnparseC.term ctxt t, UnparseC.terms ctxt ts))
    1.57 +  |> strs2str'
    1.58 +
    1.59  (**)end(**);