(* Title:  BaseDefinitions/substitution.sml

   Author: Walther Neuper

   (c) due to copyright terms

*)

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

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

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

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

"-------- fun program_to_input -----------------------------------------------";

"-------- fun T_from_input ---------------------------------------------------";

"-------- fun T_from_program -------------------------------------------------";

"-------- fun T_to_input -----------------------------------------------------";

"-------- fun T_to_string_eqs ------------------------------------------------";

"-------- fun T_from_string_eqs ----------------------------------------------";

"-------- fun input_to_terms -------------------------------------------------";

"-------- build fun for_bdv --------------------------------------------------";

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

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

"-------- fun program_to_input -----------------------------------------------";

"-------- fun program_to_input -----------------------------------------------";

"-------- fun program_to_input -----------------------------------------------";

val ctxt = Proof_Context.init_global @{theory}

val subst_prog = @{term "[(''bdv_1'', x::real), (''bdv_2'', y::real), (''bdv_3'', z::real)]"};

if Subst.program_to_input subst_prog = ["(''bdv_1'', x)", "(''bdv_2'', y)", "(''bdv_3'', z)"] then ()

else error "program_to_input changed";

"-------- fun T_from_input -----------------------------------------------------";

"-------- fun T_from_input -----------------------------------------------------";

"-------- fun T_from_input -----------------------------------------------------";

case Subst.T_from_input ctxt ["(''bdv_1'', x)", "(''bdv_2'', y)", "(''bdv_3'', z)"] of 

  [(Free ("bdv_1", _), Free ("x", _)),

   (Free ("bdv_2", _), Free ("y", _)),

   (Free ("bdv_3", _), Free ("z", _))] => ()

| _ => error "T_from_input changed";

"-------- fun T_from_program ------------------------------------------------";

"-------- fun T_from_program ------------------------------------------------";

"-------- fun T_from_program ------------------------------------------------";

val t = @{term "[(''bdv_1'', x::real), (''bdv_2'', y::real), (''bdv_3'', z::real)]"};

case Subst.T_from_program t of 

  [(Free ("bdv_1", _), Free ("x", _)),

   (Free ("bdv_2", _), Free ("y", _)),

   (Free ("bdv_3", _), Free ("z", _))] => ()

| _ => error "Subst.T_from_program changed";

"-------- fun T_to_input -----------------------------------------------------";

"-------- fun T_to_input -----------------------------------------------------";

"-------- fun T_to_input -----------------------------------------------------";

val subst_rew = 

  [(@{term "bdv_1 :: real"}, @{term "x :: real"}),

   (@{term "bdv_2 :: real"}, @{term "y :: real"}),

   (@{term "bdv_3 :: real"}, @{term "z :: real"})];

if Subst.T_to_input subst_rew  = ["(''bdv_1'', x)", "(''bdv_2'', y)", "(''bdv_3'', z)"] then ()

else error "T_to_strings changed";

"-------- fun T_to_string_eqs ------------------------------------------------";

"-------- fun T_to_string_eqs ------------------------------------------------";

"-------- fun T_to_string_eqs ------------------------------------------------";

val subst = 

  [(@{term "bdv_1 :: real"}, @{term "x :: real"}),

   (@{term "bdv_2 :: real"}, @{term "y :: real"}),

   (@{term "xxx :: real"}, @{term "aaa + (111 :: real)"})];

if Subst.T_to_string_eqs subst = ["bdv_1 = x", "bdv_2 = y", "xxx = aaa + 111"] then ()

else error "T_to_tyty changed";

"-------- fun T_from_string_eqs ----------------------------------------------";

"-------- fun T_from_string_eqs ----------------------------------------------";

"-------- fun T_from_string_eqs ----------------------------------------------";

val string_eqs = ["bdv_1 = x", "bdv_2 = y", "xxx = aaa + 111"];

case Subst.T_from_string_eqs @{theory} string_eqs of

  [(Free ("bdv_1", _), Free ("x", _)),

   (Free ("bdv_2", _), Free ("y", _)),

    (Free ("xxx", _),

     Const (\<^const_name>\<open>plus_class.plus\<close>, _) $ Free ("aaa", _) $

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

         (Const (\<^const_name>\<open>num.Bit1\<close>, _) $ _ )))] => ()

| _ => error "fun T_from_string_eqs";

"-------- fun input_to_terms -------------------------------------------------";

"-------- fun input_to_terms -------------------------------------------------";

"-------- fun input_to_terms -------------------------------------------------";

val input = ["(''bdv_1'', x)", "(''bdv_2'', y)", "(aaa, bbb + 2)"];

case Subst.input_to_terms @{context} input of

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

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

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

    Free ("x", _),

  _,

  Const (\<^const_name>\<open>Pair\<close>, _) $ Free ("aaa", _) $ _] => ()

| _ => error "input_to_eqs CHANGED";

"-------- build fun for_bdv --------------------------------------------------";

"-------- build fun for_bdv --------------------------------------------------";

"-------- build fun for_bdv --------------------------------------------------";

Subst.program_to_input: Subst.program -> string list;

val {scr = Prog prog, ...} = MethodC.from_store ctxt ["diff", "differentiate_on_R"];

val env = [(TermC.parse_test @{context} "v_v", TermC.parse_test @{context} "x")] : Subst.T;

"~~~~~ fun for_bdv, args:"; val (prog, env) = (prog, env);

    fun scan (Const _) = NONE

      | scan (Free _) = NONE

      | scan (Var _) = NONE

      | scan (Bound _) = NONE

      | scan (t as Const (\<^const_name>\<open>Cons\<close>, _) $ (Const (\<^const_name>\<open>Pair\<close>, _) $ _ $ _) $ _) =

        if TermC.is_bdv_subst t then SOME t else NONE

      | scan (Abs (_, _, body)) = scan body

      | scan (t1 $ t2) = case scan t1 of NONE => scan t2 | SOME subst => SOME subst

val SOME tm = scan prog;

val subst = tm |> subst_atomic env;

if UnparseC.term tm = "[(''bdv'', v_v)]" then () else error "for_bdv changed 1";

if Subst.program_to_input subst = (["(''bdv'', x)"] : Subst.input) then ()

else error "for_bdv changed 2";