1.1 --- a/src/Tools/isac/Specify/Specify.thy	Fri Dec 01 06:08:22 2023 +0100
     1.2 +++ b/src/Tools/isac/Specify/Specify.thy	Tue Dec 05 18:15:45 2023 +0100
     1.3 @@ -20,13 +20,70 @@
     1.4    ML_file specification.sml
     1.5    ML_file "cas-command.sml"
     1.6    ML_file "p-spec.sml"
     1.7 -  ML_file specify.sml
     1.8 +  ML_file specify.sml                                            
     1.9    ML_file "sub-problem.sml"
    1.10    ML_file "step-specify.sml"
    1.11  
    1.12  ML \<open>
    1.13 +open P_Spec
    1.14  \<close> ML \<open>
    1.15 -
    1.16 +\<close> ML \<open>
    1.17 +\<close> ML \<open>
    1.18 +\<close> ML \<open>
    1.19 +\<close> ML \<open>
    1.20 +\<close> ML \<open>
    1.21 +\<close> text \<open>
    1.22 +fun ori_2itm (feedb:feedback_POS) _ all (id, vt, fd, d, ts) = 
    1.23 +  let 
    1.24 +    val ts' = union op = (values_POS' feedb) ts;
    1.25 +    val complete = if eq_set op = (ts', all) then true else false
    1.26 +  in
    1.27 +    case feedb of
    1.28 +      Cor_POS _ => if fd = "#undef"
    1.29 +      then (id, vt, complete, fd, (Sup_POS (d, ts'), Position.none))
    1.30 +	    else (id, vt, complete, fd, (Cor_POS (d, ts'), Position.none))
    1.31 +    | Inc_POS _ => if complete
    1.32 +  	  then (id, vt, true,  fd, (Cor_POS (d, ts'), Position.none))
    1.33 +  	  else (id, vt, false, fd, (Inc_POS (d, ts'), Position.none))
    1.34 +    | Sup_POS (d, ts') =>
    1.35 +  	  (id, vt, complete, fd, (Sup_POS (d, ts'), Position.none))
    1.36 +    | i => raise ERROR ("ori_2itm: uncovered case of " ^ feedback_POS_to_string (ContextC.for_ERROR ()) i)
    1.37 +  end
    1.38 +;
    1.39 +ori_2itm: feedback_POS -> descriptor -> Model_Def.values -> O_Model.single -> I_Model.single_POS
    1.40 +\<close> ML \<open>
    1.41 +\<close> text \<open>
    1.42 +(*old code kept for test/*)
    1.43 +fun is_notyet_input ctxt (itms:I_Model.T_POS) all (i, v, f, d, ts) pbt =
    1.44 +  case find_first (fn (_, (d', _)) => d = d') pbt of
    1.45 +    SOME (_, (_, pid)) =>
    1.46 +      (case find_first (fn (_, _, _, f', (feedb, _)) =>
    1.47 +          f = f' andalso d = (descriptor_POS feedb)) itms of
    1.48 +        SOME (_, _, _, _, (feedb:feedback_POS, _)) =>
    1.49 +          let val ts' = inter op = (values_POS' feedb) ts
    1.50 +          in
    1.51 +            if subset op = (ts, ts') 
    1.52 +            then (((strs2str' o map (UnparseC.term ctxt)) ts') ^ " already input", empty_single_POS)
    1.53 +	          else ("", ori_2itm feedb pid all (i, v, f, d, subtract op = ts' ts))
    1.54 +	        end
    1.55 +	    | NONE => ("", ori_2itm (Inc_POS (TermC.empty, [])) pid all (i, v, f, d, ts)))
    1.56 +  | NONE => ("", ori_2itm (Sup_POS (d, ts)) TermC.empty all (i, v, f, d, ts))
    1.57 +;
    1.58 +is_notyet_input: Proof.context -> I_Model.T_POS -> O_Model.values ->
    1.59 +  O_Model.single -> Model_Pattern.T -> I_Model.message * I_Model.single_POS
    1.60 +\<close> ML \<open>
    1.61 +\<close> ML \<open>
    1.62 +fun is_e_ts [] = true
    1.63 +  | is_e_ts [Const (\<^const_name>\<open>Nil\<close>, _)] = true
    1.64 +  | is_e_ts _ = false;
    1.65 +\<close> ML \<open>
    1.66 +\<close> ML \<open>
    1.67 +\<close> ML \<open>
    1.68 +\<close> ML \<open>
    1.69 +\<close> ML \<open>
    1.70 +\<close> ML \<open>
    1.71 +\<close> ML \<open>
    1.72 +\<close> ML \<open>
    1.73  \<close> ML \<open>
    1.74  \<close>
    1.75  end