(* Title:  ProgLang/program.sml

   Author: Walther Neuper 190922

   (c) due to copyright terms

*)

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

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

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

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

"-------- fun eval_equal for x \<noteq> 0: \<rightarrow> indetermined, NOT \<rightarrow> 'True' -----------------------------";

"-------- occurs_in ----------------------------------------------------------------------------";

"-------- fun eval_occurs_in -------------------------------------------------------------------";

"-------- fun eval_argument_of -----------------------------------------------------------------";

"-------- fun eval_sameFunId -------------------------------------------------------------------";

"-------- fun eval_filter_sameFunId ------------------------------------------------------------";

"-------- fun eval_boollist2sum ----------------------------------------------------------------";

"-------- fun eval_binop -----------------------------------------------------------------------";

"-------- fun matchsub -------------------------------------------------------------------------";

"-------- fun or2list: HOL.disj HOL.eq HOL.True HOL.False etc ----------------------------------";

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

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

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

"-------- fun eval_equal for x \<noteq> 0: \<rightarrow> indetermined, NOT \<rightarrow> 'True' -----------------------------";

"-------- fun eval_equal for x \<noteq> 0: \<rightarrow> indetermined, NOT \<rightarrow> 'True' -----------------------------";

"-------- fun eval_equal for x \<noteq> 0: \<rightarrow> indetermined, NOT \<rightarrow> 'True' -----------------------------";

val thy = @{theory}

val t = str2term "x = 0";

val NONE(*= indetermined*) = eval_equal "equal_" "HOL.eq" t thy;

val t = str2term "(x + 1) = (x + 1)";

val (Const _(*op0,t0*) $ t1 $ t2 ) = t

val SOME ("equal_(x + 1)_(x + 1)", t') = eval_equal "equal_" "HOL.eq" t thy;

if UnparseC.term t' = "(x + 1 = x + 1) = True" then () else error "(x + 1) = (x + 1) CHANGED";

val t as Const _ $ v $ c = str2term "1 = 0";

val false = variable_constant_pair (v, c);

val SOME ("equal_(1)_(0)", t') = eval_equal "equal_" "HOL.eq" t thy;

if UnparseC.term t' = "(1 = 0) = False" then () else error "1 = 0 CHANGED";

val t = str2term "0 = 0";

val SOME ("equal_(0)_(0)", t') = eval_equal "equal_" "HOL.eq" t thy;

if UnparseC.term t' = "(0 = 0) = True" then () else error "0 = 0 CHANGED";

"-------- occurs_in ----------------------------------------------------------------------------";

"-------- occurs_in ----------------------------------------------------------------------------";

"-------- occurs_in ----------------------------------------------------------------------------";

(*=========================================================================*)

fun str2t str = (Thm.term_of o the o (parse thy)) str;

fun term2s t = UnparseC.term_in_thy thy t;

(*=========================================================================*)

val t = str2t "x";

if occurs_in t t then "OK" else error "occurs_in x x -> f ..changed";

val t = str2term "x occurs_in x";

val SOME (str, t') = eval_occurs_in 0 "Prog_Expr.occurs'_in" t 0;

if UnparseC.term t' = "x occurs_in x = True" then ()

else error "x occurs_in x = True ..changed";

"------- some_occur_in";

some_occur_in [str2t"c",str2t"c_2"] (str2t"a + b + c");

val t = str2t "some_of [c, c_2, c_3, c_4] occur_in \

		 \-1 * q_0 * L ^^^ 2 / 2 + L * c + c_2";

val SOME (str,t') = eval_some_occur_in 0 "Prog_Expr.some'_occur'_in" t 0;

if UnparseC.term t' =

   "some_of [c, c_2, c_3, c_4] occur_in -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2 =\nTrue" then ()

else error "atools.sml: some_occur_in true";

val t = str2t "some_of [c_3, c_4] occur_in \

		 \-1 * q_0 * L ^^^ 2 / 2 + L * c + c_2";

val SOME (str,t') = eval_some_occur_in 0 "Prog_Expr.some'_occur'_in" t 0;

if UnparseC.term t' =

   "some_of [c_3, c_4] occur_in -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2 = False" then ()

else error "atools.sml: some_occur_in false";

"-------- fun eval_occurs_in -------------------------------------------------------------------";

"-------- fun eval_occurs_in -------------------------------------------------------------------";

"-------- fun eval_occurs_in -------------------------------------------------------------------";

val v = (Thm.term_of o the o (parse thy)) "x";

val t = (Thm.term_of o the o (parse thy)) "1";

if occurs_in v t then error "factor_right_deg (1) x ..changed" else ();

val v = (Thm.term_of o the o (parse thy)) "AA";

val t = (Thm.term_of o the o (parse thy)) "1";

if occurs_in v t then error "factor_right_deg (1) AA ..changed" else ();

(*----------*)

val v = (Thm.term_of o the o (parse thy)) "x";

val t = (Thm.term_of o the o (parse thy)) "a*b+c";

if occurs_in v t then error "factor_right_deg (a*b+c) x ..changed" else ();

val v = (Thm.term_of o the o (parse thy)) "AA";

val t = (Thm.term_of o the o (parse thy)) "a*b+c";

if occurs_in v t then error "factor_right_deg (a*b+c) AA ..changed" else ();

(*----------*)

val v = (Thm.term_of o the o (parse thy)) "x";

val t = (Thm.term_of o the o (parse thy)) "a*x+c";

if occurs_in v t then () else error "factor_right_deg (a*x+c) x ..changed";

val v = (Thm.term_of o the o (parse thy)) "AA";

val t = (Thm.term_of o the o (parse thy)) "a*AA+c";

if occurs_in v t then () else error "factor_right_deg (a*AA+c) AA ..changed";

(*----------*)

val v = (Thm.term_of o the o (parse thy)) "x";

val t = (Thm.term_of o the o (parse thy)) "(a*b+c)*x^^^7";

if occurs_in v t then () else error "factor_right_deg (a*b+c)*x^^^7) x ..changed";

val v = (Thm.term_of o the o (parse thy)) "AA";

val t = (Thm.term_of o the o (parse thy)) "(a*b+c)*AA^^^7";

if occurs_in v t then () else error "factor_right_deg (a*b+c)*AA^^^7) AA ..changed";

(*----------*)

val v = (Thm.term_of o the o (parse thy)) "x";

val t = (Thm.term_of o the o (parse thy)) "x^^^7";

if occurs_in v t then () else error "factor_right_deg (x^^^7) x ..changed";

val v = (Thm.term_of o the o (parse thy)) "AA";

val t = (Thm.term_of o the o (parse thy)) "AA^^^7";

if occurs_in v t then () else error "factor_right_deg (AA^^^7) AA ..changed";

(*----------*)

val v = (Thm.term_of o the o (parse thy)) "x";

val t = (Thm.term_of o the o (parse thy)) "(a*b+c)*x";

if occurs_in v t then () else error "factor_right_deg ((a*b+c)*x) x ..changed";

val v = (Thm.term_of o the o (parse thy)) "AA";

val t = (Thm.term_of o the o (parse thy)) "(a*b+c)*AA";

if occurs_in v t then () else error "factor_right_deg ((a*b+c)*AA) AA ..changed";

(*----------*)

val v = (Thm.term_of o the o (parse thy)) "x";

val t = (Thm.term_of o the o (parse thy)) "(a*b+x)*x";

if occurs_in v t then () else error "factor_right_deg ((a*b+x)*x) x ..changed";

val v = (Thm.term_of o the o (parse thy)) "AA";

val t = (Thm.term_of o the o (parse thy)) "(a*b+AA)*AA";

if occurs_in v t then () else error "factor_right_deg ((a*b+AA)*AA) AA ..changed";

(*----------*)

val v = (Thm.term_of o the o (parse thy)) "x";

val t = (Thm.term_of o the o (parse thy)) "x";

if occurs_in v t then () else error "factor_right_deg (x) x ..changed";

val v = (Thm.term_of o the o (parse thy)) "AA";

val t = (Thm.term_of o the o (parse thy)) "AA";

if occurs_in v t then () else error "factor_right_deg (AA) AA ..changed";

(*----------*)

val v = (Thm.term_of o the o (parse thy)) "x";

val t = (Thm.term_of o the o (parse thy)) "ab - (a*b)*x";

if occurs_in v t then () else error "factor_right_deg (ab - (a*b)*x) x ..changed";

val v = (Thm.term_of o the o (parse thy)) "AA";

val t = (Thm.term_of o the o (parse thy)) "ab - (a*b)*AA";

if occurs_in v t then () else error "factor_right_deg (ab - (a*b)*AA) AA ..changed";

"---------fun eval_argument_of -----------------------------------------------------------------";

"---------fun eval_argument_of -----------------------------------------------------------------";

"---------fun eval_argument_of -----------------------------------------------------------------";

val t = str2term "argument_in (M_b x)";

val SOME (str, t') = eval_argument_in "0" "Prog_Expr.argument'_in" t 0;

if UnparseC.term t' = "(argument_in M_b x) = x" then ()

else error "atools.sml:(argument_in M_b x) = x  ???";

"---------fun eval_sameFunId -------------------------------------------------------------------";

"---------fun eval_sameFunId -------------------------------------------------------------------";

"---------fun eval_sameFunId -------------------------------------------------------------------";

val t = str2t "M_b L"; atomty t;

val t as f1 $ _ = str2t "M_b L";

val t as Const ("HOL.eq", _) $ (f2 $ _) $ _ = str2t "M_b x = c + L*x";

f1 = f2 (*true*);

val (p as Const ("Prog_Expr.sameFunId",_) $ 

			(f1 $ _) $ 

			(Const ("HOL.eq", _) $ (f2 $ _) $ _)) = 

    str2t "sameFunId (M_b L) (M_b x = c + L*x)";

f1 = f2 (*true*);

eval_sameFunId "" "Prog_Expr.sameFunId" 

		 (str2t "sameFunId (M_b L) (M_b x = c + L*x)")""(*true*);

eval_sameFunId "" "Prog_Expr.sameFunId" 

		 (str2t "sameFunId (M_b L) ( y' x = c + L*x)")""(*false*);

eval_sameFunId "" "Prog_Expr.sameFunId" 

		 (str2t "sameFunId (M_b L) (  y x = c + L*x)")""(*false*);

eval_sameFunId "" "Prog_Expr.sameFunId" 

		 (str2t "sameFunId (  y L) (M_b x = c + L*x)")""(*false*);

eval_sameFunId "" "Prog_Expr.sameFunId" 

		 (str2t "sameFunId (  y L) (  y x = c + L*x)")""(*true*);

"---------fun eval_filter_sameFunId ------------------------------------------------------------";

"---------fun eval_filter_sameFunId ------------------------------------------------------------";

"---------fun eval_filter_sameFunId ------------------------------------------------------------";

val flhs as (fid $ _) = str2t "y' L";

val fs = str2t "[M_b x = c + L*x, y' x = c + L*x, y x = c + L*x]";

val (p as Const ("Prog_Expr.filter'_sameFunId",_) $ (fid $ _) $ fs) = 

    str2t "filter_sameFunId (y' L) \

	     \[M_b x = c + L*x, y' x = c + L*x, y x = c + L*x]";

val SOME (str, es) = eval_filter_sameFunId "" "Prog_Expr.filter'_sameFunId" p "";

if UnparseC.term es = "(filter_sameFunId y' L [M_b x = c + L * x, y' x = c + L * x,\n                        y x = c + L * x]) =\n[y' x = c + L * x]" then ()

else error "atools.slm diff.behav. in filter_sameFunId";

"---------fun eval_boollist2sum ----------------------------------------------------------------";

"---------fun eval_boollist2sum ----------------------------------------------------------------";

"---------fun eval_boollist2sum ----------------------------------------------------------------";

fun lhs (Const ("HOL.eq",_) $ l $ _) = l

  | lhs t = error("lhs called with (" ^ UnparseC.term t ^ ")");

"-----------^^^redefined due to overwritten identifier -----------";

val u_ = str2t "[]";

val u_ = str2t "[b1 = k - 2*q]";

val u_ = str2t "[b1 = k - 2*q, b2 = k - 2*q, b3 = k - 2*q, b4 = k - 2*q]";

val ut_ = isalist2list u_;

val sum_ = map lhs ut_;

val t = list2sum sum_;

UnparseC.term t;

val t = str2t "boollist2sum [b1 = k - 2*q, b2 = k - 2*q, b3 = k - 2*q, b4 = k - 2*q]";

val p as Const ("Prog_Expr.boollist2sum", _) $ (Const ("List.list.Cons", _) $ _ $ _) = t;

val SOME (str, pred) = eval_boollist2sum "" "Prog_Expr.boollist2sum" t "";

if UnparseC.term pred = "boollist2sum\n [b1 = k - 2 * q, b2 = k - 2 * q, b3 = k - 2 * q, b4 = k - 2 * q] =\nb1 + b2 + b3 + b4" then () 

else error "atools.sml diff.behav. in eval_boollist2sum";

Rewrite.trace_on := false;

val srls_ = Rule_Set.append_rules "srls_..Berechnung-erstSymbolisch" Rule_Set.empty 

		      [Eval ("Prog_Expr.boollist2sum", eval_boollist2sum "")];

val t = str2t 

       "boollist2sum [b1 = k - 2*q, b2 = k - 2*q, b3 = k - 2*q, b4 = k - 2*q]";

case rewrite_set_ thy false srls_ t of SOME _ => ()

| _ => error "atools.sml diff.rewrite boollist2sum";

Rewrite.trace_on := false;

"---------fun eval_binop -----------------------------------------------------------------------";

"---------fun eval_binop -----------------------------------------------------------------------";

"---------fun eval_binop -----------------------------------------------------------------------";

val (op_, ef) = the (LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "TIMES"));

val t = (Thm.term_of o the o (parse thy)) "2 * 3";

(*val SOME (thmid,t') = *)get_pair thy op_ ef t;

;

"~~~~~ fun get_pair, args:"; val (thy, op_, ef, (t as (Const (op0,_) $ t1 $ t2))) =

  (thy, op_, ef, t);

op_ = op0 = true;

ef op_ t thy

;

"~~~~~ fun eval_binop, args:"; val ((thmid : string), (op_: string), 

      (t as (Const (op0, t0) $ t1 $ t2)), _) = ("#mult_", op_, t, thy); (* binary . n1.(n2.v) *)

val (SOME n1, SOME n2) = (numeral t1, numeral t2)

          val (_, _, Trange) = dest_binop_typ t0;

          val res = calcul op0 n1 n2;

          val rhs = term_of_float Trange res;

          val prop = HOLogic.Trueprop $ (mk_equality (t, rhs));

val SOME (thmid, tm) = SOME ("#: " ^ UnparseC.term prop, prop)

;

if thmid = "#: 2 * 3 = 6" andalso UnparseC.term prop = "2 * 3 = 6" then ()

else error "eval_binop changed"

;

val SOME (thmid, tm) = eval_binop "#mult_"  op_ t thy;

if thmid = "#: 2 * 3 = 6" andalso UnparseC.term prop = "2 * 3 = 6" then ()

else error "eval_binop changed 2"

"-------- fun matchsub -------------------------------------------------------------------------";

"-------- fun matchsub -------------------------------------------------------------------------";

"-------- fun matchsub -------------------------------------------------------------------------";

if matchsub thy (str2term "(a + (b + c))") (str2term "?x + (?y + ?z)")

then () else error "tools.sml matchsub a + (b + c)";

if matchsub thy (str2term "(a + (b + c)) + d") (str2term "?x + (?y + ?z)")

then () else error "tools.sml matchsub (a + (b + c)) + d";

"-------- fun or2list: HOL.disj HOL.eq HOL.True HOL.False etc ----------------------------------";

"-------- fun or2list: HOL.disj HOL.eq HOL.True HOL.False etc ----------------------------------";

"-------- fun or2list: HOL.disj HOL.eq HOL.True HOL.False etc ----------------------------------";

"see: --------- search for Or_to_List ---";

case or2list @{term True} of Const ("ListC.UniversalList", _) => ()

  | _ => error "TermC.UniversalList changed 1";

case or2list @{term False} of Const ("List.list.Nil", _) => ()

  | _ => error "TermC.UniversalList changed 2";

val t =  (str2term "x=3");

if UnparseC.term (or2list t) = "[x = 3]" then ()

else error "or2list changed";

val t =  (str2term "x=3 | x=-3 | x=0");

if UnparseC.term (or2list t) = "[x = 3, x = -3, x = 0]" then ()

else error "HOL.eq ? HOL.disj ? changed";