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

   Author: Walther Neuper

   (c) due to copyright terms

*)

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

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

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

"----------- fun match_pbl ---------------------------------------------------------------------";

"----------- fun match_oris --------------------------------------------------------------------";

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

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

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

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

open M_Match;

"----------- fun match_pbl ---------------------------------------------------------------------";

"----------- fun match_pbl ---------------------------------------------------------------------";

"----------- fun match_pbl ---------------------------------------------------------------------";

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_ = pre, ppc = ppc,...} =

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

val xxx = M_Match.match_pbl fmz pbt;

case xxx of

  Matches'

    {Find = [Correct "solutions L"],

    Given = [

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

      Correct "solveFor x",

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

    Relate = [],

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

    With = []} => ()

  | _ => error "M_Match.match_pbl CHANGED";

"----------- fun match_oris --------------------------------------------------------------------";

"----------- fun match_oris --------------------------------------------------------------------";

"----------- fun match_oris --------------------------------------------------------------------";

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

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

val pbt as {ppc = ppc,...} =

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

val o_model = O_Model.init @{theory} fmz ppc

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

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

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

if match_oris @{theory} (#prls py) o_model (#ppc py, #where_ py)

then () else error "fun match_oris CHANGED";

"----------- 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*)

    TermC.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 = (#ppc 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*)

    TermC.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 = (#ppc 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*)

    TermC.parse_test @{context} (

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

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

val ags = isalist2list ags'; 

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

val pats = (#ppc 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*)

    TermC.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 = (#ppc 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*)

    TermC.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 = (#ppc 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*)

    TermC.parse_test @{context} (

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

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

val ags = isalist2list ags'; 

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

val pats = (#ppc 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*)

   TermC.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*)

    TermC.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 = (#ppc 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' = (implode 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]--";