(* Title:  "Specify/m-match.sml"

   Author: Walther Neuper

   (c) due to copyright terms

*)

"-----------------------------------------------------------------------------------------------";

"table of contents -----------------------------------------------------------------------------";

"-----------------------------------------------------------------------------------------------";

"----------- fun by_o_model --------------------------------------------------------------------";

"----------- fun by_formalise ---------------------------------------------------------------------";

"----------- M_Match.arguments, is_cp, O_Model.copy_name +with EqSystem (!) --------------------";

"-----------------------------------------------------------------------------------------------";

"-----------------------------------------------------------------------------------------------";

"-----------------------------------------------------------------------------------------------";

open M_Match;

(*** ------- fun by_o_model ----------------------------------------------------------------- ***)

"----------- fun by_o_model --------------------------------------------------------------------";

"----------- fun by_o_model --------------------------------------------------------------------";

(*//------------------ setup test data for fun by_o_model 1 --------------------------------\\*)

val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))",

	      "solveFor x", "errorBound (eps=0)", "solutions L"];

val pbt as {model,...} = Problem.from_store @{context} ["univariate", "equation"];

val (o_model, ctxt) = O_Model.init @{theory} fmz model

val py1 = Problem.from_store @{context} ["equation"];

val py2 = Problem.from_store @{context} ["univariate", "equation"];

val py3 = Problem.from_store @{context} ["sq", "rootX", "univariate", "equation"];

val return_1 as true = by_o_model ctxt o_model (#model py1, #where_ py1, #where_rls py1)

val return_2 as true = by_o_model ctxt o_model (#model py2, #where_ py2, #where_rls py2)

val return_1 as true = by_o_model ctxt o_model (#model py3, #where_ py3, #where_rls py3);

(*\\------------------ setup test data for fun by_o_model 1 --------------------------------//*)

"~~~~~ fun by_o_model , args:"; val (ctxt, o_model, (model_patt, where_, where_rls))

  = (ctxt, o_model, (#model py3, #where_ py3, #where_rls py3));

          (data_by_o ctxt o_model (model_patt, where_, where_rls));

"~~~~~ fun data_by_o , args:"; val (ctxt, o_model, (model_patt, where_, where_rls)) =

  (ctxt, o_model, (model_patt, where_, where_rls));

    val o_model_vnt = o_model

      |> map (fn o_single as (_, variants, _, _, _)

        => if member_swap op = 1 (*variant 1 is mandatory*) variants then [o_single] else [])

      |> flat

    val is_complete as true = map (fn (_, (descr, _)) => contains_o descr o_model_vnt) model_patt

      |> curry (foldl and_) true

    val i_model = (*in order to match sig of Pre_Conds.check*)

      map (fn (a, b, c, d, e) => (a, b, true, c, (I_Model.Cor_TEST (d, e), Position.none))) o_model_vnt

(*+*)val "[\n(1, [1], true ,#Given, (Cor_TEST equality (sqrt (9 + 4 * x) = sqrt x + sqrt (5 + x)) , pen2str, Position.T)), \n(2, [1], true ,#Given, (Cor_TEST solveFor x , pen2str, Position.T)), \n(3, [1], true ,#undef, (Cor_TEST errorBound (eps = (0::'a)) , pen2str, Position.T)), \n(4, [1], true ,#Find, (Cor_TEST solutions L , pen2str, Position.T))]"

 = i_model |> I_Model.to_string_TEST ctxt

    val (pre_conds_check, pre_conds) = Pre_Conds.check ctxt where_rls where_ (model_patt, i_model)

val return_data_by_o_STEP = (is_complete andalso pre_conds_check, (i_model, pre_conds))

val return_by_o_model as true = (data_by_o ctxt o_model (model_patt, where_, where_rls)) |> #1;

(*** ------- fun by_formalise ------------------------------------------------------------------ ***)

"----------- fun by_formalise ---------------------------------------------------------------------";

"----------- fun by_formalise ---------------------------------------------------------------------";

val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))",

	      "solveFor x", "errorBound (eps=0)", "solutions L"];

val pbt as {thy = thy, where_ = where_, model = model,...} =

    Problem.from_store @{context} ["univariate", "equation"];

val xxx = M_Match.by_formalise fmz pbt;

val Matches'

   {Find = [Correct "solutions L"], 

    Given = [

      Correct "equality (sqrt (9 + 4 * x) = sqrt x + sqrt (5 + x))", 

      Correct "solveFor x", 

      Correct "errorBound (eps = (0::'a))"], 

    Relate = [], 

    Where = [Correct "matches (?a = ?b) (sqrt (9 + 4 * x) = sqrt x + sqrt (5 + x))"], 

    With = []} = xxx;

(*** ------- M_Match.arguments, is_cp, O_Model.copy_name +with EqSystem (!) ----------------- ***)

"----------- M_Match.arguments, is_cp, O_Model.copy_name +with EqSystem (!) --------------------";

"----------- M_Match.arguments, is_cp, O_Model.copy_name +with EqSystem (!) --------------------";

val Const (\<^const_name>\<open>SubProblem\<close>,_) $

	  (Const (\<^const_name>\<open>Pair\<close>,_) $

		 Free (dI',_) $ 

		 (Const (\<^const_name>\<open>Pair\<close>,_) $ pI' $ mI')) $ ags' =

    (*...copied from LItool.tac_from_prog*)

    ParseC.parse_test @{context} (

	"SubProblem (EqSystemX, [LINEAR, system], [no_met])         " ^

        "     [BOOL_LIST [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]," ^

        "      REAL_LIST [c, c_2]]");

val ags = isalist2list ags';

val pI = ["LINEAR", "system"];

val pats = (#model o Problem.from_store @{context}) pI;

"-a1-----------------------------------------------------";

(*M_Match.arguments = fn : theory -> pat list -> term list -> O_Model.T*)

val xxx = M_Match.arguments @{theory "EqSystem"} pats ags;

"-a2-----------------------------------------------------";

case M_Match.arguments @{theory  "Isac_Knowledge"} pats ags of 

    [(1, [1], "#Given", Const (\<^const_name>\<open>Input_Descript.equalities\<close>, _), _),

     (2, [1], "#Given", Const (\<^const_name>\<open>EqSystem.solveForVars\<close>, _),

      [ _ $ Free ("c", _) $ _, _ $ Free ("c_2", _) $ _]),

     (3, [1], "#Find", Const (\<^const_name>\<open>EqSystem.solution\<close>, _), [Free ("ss'''", _)])] 

    =>()

  | _ => error "calchead.sml M_Match.arguments 2 args Nok ----------------";

"-b------------------------------------------------------";

val Const (\<^const_name>\<open>SubProblem\<close>,_) $

	  (Const (\<^const_name>\<open>Pair\<close>,_) $

		 Free (dI',_) $ 

		 (Const (\<^const_name>\<open>Pair\<close>,_) $ pI' $ mI')) $ ags' =

    (*...copied from LItool.tac_from_prog*)

    ParseC.parse_test @{context} (

	"SubProblem (EqSystemX, [LINEAR, system], [no_met])         " ^

        "     [BOOL_LIST [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]," ^

        "      REAL_LIST [c, c_2], BOOL_LIST ss''']");

val ags = isalist2list ags';

val pI = ["LINEAR", "system"];

val pats = (#model o Problem.from_store @{context}) pI;

"-b1-----------------------------------------------------";

val xxx = M_Match.arguments @{theory  "Isac_Knowledge"} pats ags;

"-b2-----------------------------------------------------";

case M_Match.arguments @{theory "EqSystem"} pats ags of 

    [(1, [1], "#Given", Const (\<^const_name>\<open>Input_Descript.equalities\<close>, _), _),

     (2, [1], "#Given", Const (\<^const_name>\<open>EqSystem.solveForVars\<close>, _),

         [_ $ Free ("c", _) $ _,

          _ $ Free ("c_2", _) $ _]),

     (3, [1], "#Find", Const (\<^const_name>\<open>EqSystem.solution\<close>, _), [Free ("ss'''", _)])]

    (*         type of Find:            [Free ("ss'''", "bool List.list")]*)

    =>()

  | _ => error "calchead.sml M_Match.arguments copy-named dropped --------";

"-c---ERROR case: stac is missing #Given equalities e_s--";

val stac as Const (\<^const_name>\<open>SubProblem\<close>,_) $

	 (Const (\<^const_name>\<open>Pair\<close>,_) $

		Free (dI',_) $ 

		(Const (\<^const_name>\<open>Pair\<close>,_) $ pI' $ mI')) $ ags' =

    (*...copied from LItool.tac_from_prog*)

    ParseC.parse_test @{context} (

	"SubProblem (EqSystemX, [LINEAR, system], [no_met]) " ^

        "     [REAL_LIST [c, c_2]]");

val ags = isalist2list ags'; 

val pI = ["LINEAR", "system"];

val pats = (#model o Problem.from_store @{context}) pI;

(*============ inhibit exn AK110726 ==============================================

val xxx - M_Match.arguments (theory "EqSystem") pats ags;

============ inhibit exn AK110726 ==============================================*)

"-c1-----------------------------------------------------";

"--------------------------step through code M_Match.arguments---";

val (thy, pbt: Model_Pattern.T, ags) = (@{theory "EqSystem"}, pats, ags);

fun flattup (i,(var,bool,str,itm_)) = (i,var,bool,str,itm_);

	val pbt' = filter_out O_Model.is_copy_named pbt; (*=equalities, solveForVars*)

	val cy = filter O_Model.is_copy_named pbt;       (*=solution*)

(*============ inhibit exn AK110726 ==============================================

	val oris' - O_Model.matc thy pbt' ags [];

============ inhibit exn AK110726 ==============================================*)

"-------------------------------step through code O_Model.matc---";

val (thy, (p as (s,(d,t)))::pbt, a::ags, oris) = (thy, pbt', ags, []);

(O_Model.is_copy_named' o free2str) t;

"---if False:...";

(*============ inhibit exn AK110726 ==============================================

val opt - mtc thy p a;

============ inhibit exn AK110726 ==============================================*)

"--------------------------------step through code mtc---";

val (thy, (str, (dsc, _)): Model_Pattern.single, ty $ var) = (thy, p, a);

Thm.global_cterm_of;

val ttt = (dsc $ var);

(*============ inhibit exn AK110726 ==============================================

Thm.global_cterm_of thy (dsc $ var);

============ inhibit exn AK110726 ==============================================*)

"-------------------------------------step through end---";

"--------- M_Match.arguments, is_cp, O_Model.copy_name +with EqSystem (!)--";

val Const (\<^const_name>\<open>SubProblem\<close>,_) $

	  (Const (\<^const_name>\<open>Pair\<close>,_) $

		 Free (dI',_) $ 

		 (Const (\<^const_name>\<open>Pair\<close>,_) $ pI' $ mI')) $ ags' =

    (*...copied from LItool.tac_from_prog*)

    ParseC.parse_test @{context} (

	"SubProblem (EqSystemX, [LINEAR, system], [no_met])         " ^

        "     [BOOL_LIST [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]," ^

        "      REAL_LIST [c, c_2]]");

val ags = isalist2list ags';

val pI = ["LINEAR", "system"];

val pats = (#model o Problem.from_store @{context}) pI;

"-a1-----------------------------------------------------";

(*M_Match.arguments = fn : theory -> pat list -> term list -> O_Model.T*)

val xxx = M_Match.arguments @{theory "EqSystem"} pats ags;

"-a2-----------------------------------------------------";

case M_Match.arguments @{theory  "Isac_Knowledge"} pats ags of 

    [(1, [1], "#Given", Const (\<^const_name>\<open>Input_Descript.equalities\<close>, _), _),

     (2, [1], "#Given", Const (\<^const_name>\<open>EqSystem.solveForVars\<close>, _),

      [ _ $ Free ("c", _) $ _, _ $ Free ("c_2", _) $ _]),

     (3, [1], "#Find", Const (\<^const_name>\<open>EqSystem.solution\<close>, _), [Free ("ss'''", _)])] 

    =>()

  | _ => error "calchead.sml M_Match.arguments 2 args Nok ----------------";

"-b------------------------------------------------------";

val Const (\<^const_name>\<open>SubProblem\<close>,_) $

	  (Const (\<^const_name>\<open>Pair\<close>,_) $

		 Free (dI',_) $ 

		 (Const (\<^const_name>\<open>Pair\<close>,_) $ pI' $ mI')) $ ags' =

    (*...copied from LItool.tac_from_prog*)

    ParseC.parse_test @{context} (

	"SubProblem (EqSystemX, [LINEAR, system], [no_met])         " ^

        "     [BOOL_LIST [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]," ^

        "      REAL_LIST [c, c_2], BOOL_LIST ss''']");

val ags = isalist2list ags';

val pI = ["LINEAR", "system"];

val pats = (#model o Problem.from_store @{context}) pI;

"-b1-----------------------------------------------------";

val xxx = M_Match.arguments @{theory  "Isac_Knowledge"} pats ags;

"-b2-----------------------------------------------------";

case M_Match.arguments @{theory "EqSystem"} pats ags of 

    [(1, [1], "#Given", Const (\<^const_name>\<open>Input_Descript.equalities\<close>, _), _),

     (2, [1], "#Given", Const (\<^const_name>\<open>EqSystem.solveForVars\<close>, _),

         [_ $ Free ("c", _) $ _,

          _ $ Free ("c_2", _) $ _]),

     (3, [1], "#Find", Const (\<^const_name>\<open>EqSystem.solution\<close>, _), [Free ("ss'''", _)])]

    (*         type of Find:            [Free ("ss'''", "bool List.list")]*)

    =>()

  | _ => error "calchead.sml M_Match.arguments copy-named dropped --------";

"-c---ERROR case: stac is missing #Given equalities e_s--";

val stac as Const (\<^const_name>\<open>SubProblem\<close>,_) $

	 (Const (\<^const_name>\<open>Pair\<close>,_) $

		Free (dI',_) $ 

		(Const (\<^const_name>\<open>Pair\<close>,_) $ pI' $ mI')) $ ags' =

    (*...copied from LItool.tac_from_prog*)

    ParseC.parse_test @{context} (

	"SubProblem (EqSystemX, [LINEAR, system], [no_met]) " ^

        "     [REAL_LIST [c, c_2]]");

val ags = isalist2list ags'; 

val pI = ["LINEAR", "system"];

val pats = (#model o Problem.from_store @{context}) pI;

(*============ inhibit exn AK110726 ==============================================

val xxx - M_Match.arguments (theory "EqSystem") pats ags;

-------------------------------------------------------------------*)

"-c1-----------------------------------------------------";

"--------------------------step through code M_Match.arguments---";

val (thy, pbt: Model_Pattern.T, ags) = (@{theory "EqSystem"}, pats, ags);

fun flattup (i,(var,bool,str,itm_)) = (i,var,bool,str,itm_);

	val pbt' = filter_out O_Model.is_copy_named pbt; (*=equalities, solveForVars*)

	val cy = filter O_Model.is_copy_named pbt;       (*=solution*)

(*============ inhibit exn AK110726 ==============================================

	val oris' - O_Model.matc thy pbt' ags [];

-------------------------------------------------------------------*)

"-------------------------------step through code O_Model.matc---";

val (thy, (p as (s,(d,t)))::pbt, a::ags, oris) = (thy, pbt', ags, []);

(O_Model.is_copy_named' o free2str) t;

"---if False:...";

(*============ inhibit exn AK110726 ==============================================

val opt - mtc thy p a;

-------------------------------------------------------------------*)

"--------------------------------step through code mtc---";

val (thy, (str, (dsc, _)): Model_Pattern.single, ty $ var) = (thy, p, a);

Thm.global_cterm_of;

val ttt = (dsc $ var);

(*============ inhibit exn AK110726 ==============================================

Thm.global_cterm_of thy (dsc $ var);

-------------------------------------------------------------------*)

"-------------------------------------step through end---";

case ((M_Match.arguments @{theory "EqSystem"} pats ags)

      handle ERROR _ => []) of (*why not TYPE ?WN100920*)

    [] => M_Match.arguments_msg @{context} pI stac ags

  | _ => error "calchead.sml M_Match.arguments 1st arg missing --------";

"-d------------------------------------------------------";

val stac as Const (\<^const_name>\<open>SubProblem\<close>,_) $

	 (Const (\<^const_name>\<open>Pair\<close>,_) $

		Free (dI',_) $ 

		(Const (\<^const_name>\<open>Pair\<close>,_) $ pI' $ mI')) $ ags' =

    (*...copied from LItool.tac_from_prog*)

   ParseC.parse_test @{context} (

	"SubProblem (TestX,[univariate,equation,test]," ^

        "             [no_met]) [BOOL (x+1=2), REAL x]");

val AGS = isalist2list ags';

val pI = ["univariate", "equation", "test"];

case ((M_Match.arguments @{theory "EqSystem"} pats ags)

      handle ERROR _ => []) of (*why not TYPE ?WN100920*)

    [] => M_Match.arguments_msg @{context} pI stac ags

  | _ => error "calchead.sml M_Match.arguments 1st arg missing --------";

"-d------------------------------------------------------";

val stac as Const (\<^const_name>\<open>SubProblem\<close>, _) $

	 (Const (\<^const_name>\<open>Pair\<close>,_) $

		Free (dI',_) $ 

		(Const (\<^const_name>\<open>Pair\<close>,_) $ pI' $ mI')) $ ags' =

    (*...copied from LItool.tac_from_prog*)

    ParseC.parse_test @{context} (

	"SubProblem (TestX,[univariate,equation,test]," ^

        "             [no_met]) [BOOL (x+1=2), REAL x]");

val AGS = isalist2list ags';

val pI = ["univariate", "equation", "test"];

val PATS = (#model o Problem.from_store @{context}) pI;

"-d1-----------------------------------------------------";

"--------------------------step through code M_Match.arguments---";

val (thy, pbt: Model_Pattern.T, ags) = (@{theory "Test"}, PATS, AGS);

fun flattup (i,(var,bool,str,itm_)) = (i,var,bool,str,itm_);

	val pbt' = filter_out O_Model.is_copy_named pbt; 

	val cy = filter O_Model.is_copy_named pbt;       

	val oris' = M_Match.matc thy pbt' ags [];

"-------------------------------step through code O_Model.matc---";

val (thy, (p as (s,(d,t)))::pbt, a::ags, oris) = (thy, pbt', ags, []);

(O_Model.is_copy_named' o free2str) t;

"---if False:...";

val opt = mtc thy p a;

"--------------------------------step through code mtc---";

val (thy, (str, (dsc, _)): Model_Pattern.single, ty $ var) = (thy, p, a);

val ttt = (dsc $ var);

Thm.global_cterm_of thy (dsc $ var);

val ori = ((([1], str, dsc, (*[var]*) Input_Descript.split' (dsc, var))): O_Model.preori);

"-d2-----------------------------------------------------";

pbt = [];  (*false*)

"-------------------------------step through code O_Model.matc---";

val (thy, (p as (s,(d,t)))::pbt, a::ags, oris) = (thy, pbt, ags, oris @ [ori]);

(O_Model.is_copy_named' o free2str) t;

"---if False:...";

val opt = mtc thy p a;

"--------------------------------step through code mtc---";

val (thy, (str, (dsc, _)):Model_Pattern.single, ty $ var) = (thy, p, a);

val ttt = (dsc $ var);

Thm.global_cterm_of thy (dsc $ var);

val ori = ((([1], str, dsc, (*[var]*) Input_Descript.split' (dsc, var))): O_Model.preori);

"-d3-----------------------------------------------------";

pbt = [];  (*true, base case*)

"-----------------continue step through code M_Match.arguments---";

	val oris' = oris @ [ori]; (*result 2 oris, O_Model.copy_name added later*)

"--------------------------------step through O_Model.copy_name----";

val (pbt, oris, p as (field, (dsc, t)):Model_Pattern.single) = (pbt', oris', hd cy);

(*t = "v_v'i'" : term             OLD: t = "v_i_"*)

"--------------------------------------------------------";

fun is_copy_named_generating_idstr str =

    if O_Model.is_copy_named' str

    then case (rev o Symbol.explode) str of

      (*"_"::"_"::"_"::_ => false*)

	"'"::"'"::"'"::_ => false

      | _ => true

    else false;

fun is_copy_named_generating (_, (_, t)) = 

    (is_copy_named_generating_idstr o free2str) t;

"--------------------------------------------------------";

is_copy_named_generating p (*true*);

           fun sel (_,_,d,ts) = Input_Descript.join'''' (d, ts);

	   val cy' = (String.concat o (drop_last_n 3) o Symbol.explode o free2str) t;

               (*"v_v"             OLD: "v_"*)

	   val ext = (last_elem o drop_last o Symbol.explode o free2str) t;

               (*"i"               OLD: "i"*)

	   val vars' = map (free2str o snd o snd) pbt(*cpy-nam filtered_out*);

               (*["e_e", "v_v"]    OLD: ["e_", "v_"]*)

	   val vals = map sel oris;

               (*[x+1=2, x]        OLD: [x+1=2, x] : term list*)

vars' ~~ vals;

(*[("e_e", [x+1=2), ("v_v", x)]    OLD: [("e_", [x+1=2), ("v_", x)]*)

(LibraryC.assoc (vars'~~vals, cy'));

(*SOME (Free ("x", "Real.real")) : term option*)

	   val cy_ext = (free2str o the) (LibraryC.assoc (vars'~~vals, cy'))^"_"^ext;

               (*x_i*)

"-----------------continue step through code M_Match.arguments---";

	val cy' = map (O_Model.copy_name pbt' oris') cy;

               (*[([1], "#Find", "solutions, [x_i"] (*as terms*) )]*)

"-------------------------------------step through end---";

case M_Match.arguments thy PATS AGS of

[(1, [1], "#Given", Const (\<^const_name>\<open>Input_Descript.equality\<close>, _),

  [Const (\<^const_name>\<open>HOL.eq\<close>, _) $ (Const (\<^const_name>\<open>plus_class.plus\<close>, _) $

		Free ("x", _) $ _(*1*)) $ _(*1*)]),

 (2, [1], "#Given", Const (\<^const_name>\<open>Input_Descript.solveFor\<close>, _), [Free ("x", _)]),

 (3, [1], "#Find", Const (\<^const_name>\<open>Input_Descript.solutions\<close>, _), [Free ("x_i", _)])]

    => ()

  | _ => error "calchead.sml M_Match.arguments [univariate,equation,test]--";