(* Title:  "Specify/Specify.thy"

   Author: Walther Neuper 110226

   (c) due to copyright terms

 Specification phase

 *)

theory Specify

  imports "$ISABELLE_ISAC/MathEngBasic/MathEngBasic"

  keywords "cas" :: thy_decl

begin

  ML_file "o-model.sml"

  ML_file "pre-conditions.sml" (*uses Model_Def.i_model*)

  ML_file "i-model.sml"

  ML_file "p-model.sml"

  ML_file "m-match.sml"

  ML_file refine.sml

  ML_file "test-out.sml"

  ML_file "specify-step.sml"

  ML_file specification.sml

  ML_file "cas-command.sml"

  ML_file "p-spec.sml"

  ML_file specify.sml                                            

  ML_file "sub-problem.sml"

  ML_file "step-specify.sml"

ML \<open>

open P_Spec

\<close> ML \<open>

\<close> ML \<open>

\<close> ML \<open>

\<close> ML \<open>

\<close> ML \<open>

\<close> ML \<open>

\<close> text \<open>

fun ori_2itm (feedb:feedback_POS) _ all (id, vt, fd, d, ts) = 

  let 

    val ts' = union op = (values_POS' feedb) ts;

    val complete = if eq_set op = (ts', all) then true else false

  in

    case feedb of

      Cor_POS _ => if fd = "#undef"

      then (id, vt, complete, fd, (Sup_POS (d, ts'), Position.none))

	    else (id, vt, complete, fd, (Cor_POS (d, ts'), Position.none))

    | Inc_POS _ => if complete

  	  then (id, vt, true,  fd, (Cor_POS (d, ts'), Position.none))

  	  else (id, vt, false, fd, (Inc_POS (d, ts'), Position.none))

    | Sup_POS (d, ts') =>

  	  (id, vt, complete, fd, (Sup_POS (d, ts'), Position.none))

    | i => raise ERROR ("ori_2itm: uncovered case of " ^ feedback_POS_to_string (ContextC.for_ERROR ()) i)

  end

;

ori_2itm: feedback_POS -> descriptor -> Model_Def.values -> O_Model.single -> I_Model.single_POS

\<close> ML \<open>

\<close> text \<open>

(*old code kept for test/*)

fun is_notyet_input ctxt (itms:I_Model.T_POS) all (i, v, f, d, ts) pbt =

  case find_first (fn (_, (d', _)) => d = d') pbt of

    SOME (_, (_, pid)) =>

      (case find_first (fn (_, _, _, f', (feedb, _)) =>

          f = f' andalso d = (descriptor_POS feedb)) itms of

        SOME (_, _, _, _, (feedb:feedback_POS, _)) =>

          let val ts' = inter op = (values_POS' feedb) ts

          in

            if subset op = (ts, ts') 

            then (((strs2str' o map (UnparseC.term ctxt)) ts') ^ " already input", empty_single_POS)

	          else ("", ori_2itm feedb pid all (i, v, f, d, subtract op = ts' ts))

	        end

	    | NONE => ("", ori_2itm (Inc_POS (TermC.empty, [])) pid all (i, v, f, d, ts)))

  | NONE => ("", ori_2itm (Sup_POS (d, ts)) TermC.empty all (i, v, f, d, ts))

;

is_notyet_input: Proof.context -> I_Model.T_POS -> O_Model.values ->

  O_Model.single -> Model_Pattern.T -> I_Model.message * I_Model.single_POS

\<close> ML \<open>

\<close> ML \<open>

fun is_e_ts [] = true

  | is_e_ts [Const (\<^const_name>\<open>Nil\<close>, _)] = true

  | is_e_ts _ = false;

\<close> ML \<open>

\<close> ML \<open>

\<close> ML \<open>

\<close> ML \<open>

\<close> ML \<open>

\<close> ML \<open>

\<close> ML \<open>

\<close> ML \<open>

\<close> ML \<open>

\<close>

end