(* Title:  ProgLang/Auto_Prog

   Author: Walther Neuper, Aug.2019

   (c) due to copyright terms

*)

theory Auto_Prog imports Prog_Tac Tactical begin

text \<open>Abstract:

  The tactics Rewrite_Set* create ONE step in a calculation by application of usually

  MORE than one theorem (here called "rule").

  However, students can request details of rewriting down to single applications of theorems.

  For accomplishing such requests, a program is auto-generated from the items of a rule-set.

\<close>

subsection \<open>consts for programs automatically built from rules\<close>

partial_function (tailrec) auto_generated :: "'z \<Rightarrow> 'z"

  where "auto_generated t_t = t_t"

partial_function (tailrec) auto_generated_inst :: "'z \<Rightarrow> real \<Rightarrow> 'z"

  where "auto_generated_inst t_t v =  t_t"

subsection \<open>TODO: code for above\<close>

ML \<open>

\<close> ML \<open>

signature AUTO_GERNERATE_PROGRAM =

  sig

    val contain_bdv: Rule.rule list -> bool

    val contains_bdv: thm -> bool

    val subst_typs: term -> typ -> typ -> term

    val pblterm: Rule.domID -> Celem.pblID -> term

    val subpbl: string -> string list -> term

    val stacpbls: term -> term list

    val op_of_calc: term -> string

    val get_calcs: theory -> term -> (Rule.prog_calcID * (Rule.calID * Rule.eval_fn)) list

    val prep_rls: theory -> Rule.rls -> Rule.rls (*ren insert*)

    val gen: theory -> term -> Rule.rls -> term

(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)

  (* NONE *)

(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )

    val subst_typ: string -> typ -> term list -> (typ * typ) list

    val is_calc: term -> bool

    val rule2stac: theory -> Rule.rule -> term

    val rule2stac_inst: theory -> Rule.rule -> term

    val #> : term list -> term

    val rules2scr_Rls : theory -> Rule.rule list -> term

    val rules2scr_Seq : theory -> Rule.rule list -> term

( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)

  end

(**)

structure Auto_Prog(**): AUTO_GERNERATE_PROGRAM(**) =

struct

(**)

(** build up a program from rules **)

(* make the term 'Subproblem (domID, pblID)' to a formula for frontend;

  needs to be here after def. Subproblem in Prog_Tac.thy *)

val subpbl_t $ (pair_t $ _ $ _) = (Thm.term_of o the o (TermC.parse @{theory Prog_Tac}))

  "Subproblem (''Isac_Knowledge'',[''equation'',''univar''])"

val pbl_t $ _ = 

  (Thm.term_of o the o (TermC.parse @{theory Prog_Tac})) "Problem (''Isac_Knowledge'',[''equation'',''univar''])"

fun subpbl domID pblID =

  subpbl_t $ (pair_t $ HOLogic.mk_string domID $ 

    list_comb (Syntax.const @{const_syntax Char}, map HOLogic.mk_string pblID));

fun pblterm domID pblID =

  pbl_t $ (pair_t $ HOLogic.mk_string domID $ 

    list_comb (Syntax.const @{const_syntax Char}, map HOLogic.mk_string pblID));

(* fetch tactics from a program omitting tacticals like While, Repeat,.. *)

fun stacpbls (_ $ body) =

    let

      fun scan (Const ("HOL.Let", _) $ e $ (Abs (_, _, b))) = (scan e) @ (scan b)

        | scan (Const ("Tactical.If", _) $ _ $ e1 $ e2) = (scan e1) @ (scan e2)

        | scan (Const ("Tactical.While", _) $ _ $ e $ _) = scan e

        | scan (Const ("Tactical.While", _) $ _ $ e) = scan e

        | scan (Const ("Tactical.Repeat", _) $ e $ _) = scan e

        | scan (Const ("Tactical.Repeat", _) $ e) = scan e

        | scan (Const ("Tactical.Try", _) $ e $ _) = scan e

        | scan (Const ("Tactical.Try", _) $ e) = scan e

        | scan (Const ("Tactical.Or", _) $ e1 $ e2 $ _) = (scan e1) @ (scan e2)

        | scan (Const ("Tactical.Or", _) $ e1 $ e2) = (scan e1) @ (scan e2)

        | scan (Const ("Tactical.Chain", _) $ e1 $ e2 $ _) = (scan e1) @ (scan e2)

        | scan (Const ("Tactical.Chain", _) $ e1 $ e2) = (scan e1) @ (scan e2)

        | scan t = case Prog_Tac.eval_leaf [] NONE Rule.e_term t of

  			  (Program.Tac _, _) => [t] | (Program.Expr _, _) => []

    in (distinct o scan) body end

  | stacpbls t = raise ERROR ("fun stacpbls not applicable to '" ^ Rule.term2str t ^ "'")

(* get operators out of a program *)

fun is_calc (Const ("Prog_Tac.Calculate",_) $ _) = true

  | is_calc (Const ("Prog_Tac.Calculate",_) $ _ $ _) = true

  | is_calc _ = false;

fun op_of_calc (Const ("Prog_Tac.Calculate",_) $ op_) = HOLogic.dest_string op_

  | op_of_calc (Const ("Prog_Tac.Calculate",_) $ op_ $ _) = HOLogic.dest_string op_

  | op_of_calc t = error ("op_of_calc called with " ^ Rule.term2str t);

fun get_calcs thy sc =

    sc

    |> stacpbls

    |> filter is_calc

    |> map op_of_calc

    |> (assoc_calc' thy |> map);

(** build up a program from rules **)

(* transform type rule to a term *)

(*WN060605 script-arg (t_::'z) and "Free (t_, 'a)" at end of body are inconsistent !!!*)

val (FunID_Term $ _) = Program.prep_program @{thm auto_generated.simps}

val (FunID_Term_Bdv $ _) = Program.prep_program @{thm auto_generated_inst.simps}

val Repeat $ _ = (TermC.inst_abs o Thm.term_of o the o (TermC.parseN @{theory})) 

	"Repeat (Rewrite ''real_diff_minus'' t)";

val Try $ _ = (TermC.inst_abs o Thm.term_of o the o (TermC.parseN @{theory})) 

	"Try (Rewrite ''real_diff_minus'' t)";

val Cal $ _ = (TermC.inst_abs o Thm.term_of o the o (TermC.parseN @{theory})) 

	"Calculate ''PLUS''";

val Ca1 $ _ = (TermC.inst_abs o Thm.term_of o the o (TermC.parseN @{theory})) 

	"Calculate1 ''PLUS''";

val Rew $ _ $ _ = (TermC.inst_abs o Thm.term_of o the o (TermC.parseN @{theory})) 

	"Rewrite ''real_diff_minus'' t";

(*this is specific to FunHead_inst ...*)

val Rew_Inst $ Subs $ _ = (TermC.inst_abs o Thm.term_of o the o (TermC.parseN @{theory})) 

	"Rewrite_Inst [(''bdv'',v)] ''real_diff_minus''";

val Rew_Set $ _ = (TermC.inst_abs o Thm.term_of o the o (TermC.parseN @{theory})) 

	"Rewrite_Set ''real_diff_minus''";

val Rew_Set_Inst $ _ $ _ = (TermC.inst_abs o Thm.term_of o the o (TermC.parseN @{theory})) 

	"Rewrite_Set_Inst [(''bdv'',v)] ''real_diff_minus''";

val SEq $ _ $ _ $ _ = (TermC.inst_abs o Thm.term_of o the o (TermC.parseN @{theory})) 

	"  ((Try (Repeat (Rewrite ''real_diff_minus''))) #>  \

        \   (Try (Repeat (Rewrite ''add_commute''))) #> \

        \   (Try (Repeat (Rewrite ''mult_commute'')))) t";

fun rule2stac _ (Rule.Thm (thmID, _)) = Try $ (Repeat $ (Rew $ HOLogic.mk_string thmID))

  | rule2stac thy (Rule.Num_Calc (c, _)) = Try $ (Repeat $ (Cal $ HOLogic.mk_string (assoc_calc thy c)))

  | rule2stac thy (Rule.Cal1 (c, _)) = Try $ (Repeat $ (Ca1 $ HOLogic.mk_string (assoc_calc thy c)))

  | rule2stac _ (Rule.Rls_ rls) = Try $ (Rew_Set $ HOLogic.mk_string (Rule.id_rls rls))

  | rule2stac _ r = raise ERROR ("rule2stac: not applicable to \"" ^ Rule.rule2str r ^ "\"");

fun rule2stac_inst _ (Rule.Thm (thmID, _)) = 

    Try $ (Repeat $ (Rew_Inst $ Subs $ HOLogic.mk_string thmID))

  | rule2stac_inst thy (Rule.Num_Calc (c, _)) = 

    Try $ (Repeat $ (Cal $ HOLogic.mk_string (assoc_calc thy c)))

  | rule2stac_inst thy (Rule.Cal1 (c, _)) = 

    Try $ (Repeat $ (Cal $ HOLogic.mk_string (assoc_calc thy c)))

  | rule2stac_inst _ (Rule.Rls_ rls) = 

    Try $ (Rew_Set_Inst $ Subs $ HOLogic.mk_string (Rule.id_rls rls))

  | rule2stac_inst _ r = raise ERROR ("rule2stac_inst: not applicable to \"" ^ Rule.rule2str r ^ "\"");

(*for appropriate nesting take stacs in _reverse_ order*)

fun op #>@ sts [s] = SEq $ s $ sts

  | op #>@ sts (s::ss) = op #>@ (SEq $ s $ sts) ss

  | op #>@ t ts =

    raise ERROR ("fun #>@ not applicable to \"" ^ Rule.term2str t ^ "\" \"" ^ Rule.terms2str ts  ^ "\"");

fun #> [stac] = stac

  | #> [s1, s2] = SEq $ s1 $ s2

  | #> stacs = case rev stacs of

      s3 :: s2 :: ss => op #>@ (SEq $ s2 $ s3) ss

    | ts => raise ERROR ("fun #> not applicable to \"" ^ Rule.terms2str ts ^ "\"")

val contains_bdv = (not o null o (filter TermC.is_bdv) o TermC.ids2str o #prop o Thm.rep_thm);

(* does a rule contain a 'bdv'; descend recursively into Rls_ *)

fun contain_bdv [] = false

  | contain_bdv (Rule.Thm (_, thm) :: rs) = 

    if (not o contains_bdv) thm

    then contain_bdv rs

    else true

  | contain_bdv (Rule.Num_Calc _ :: rs) = contain_bdv rs

  | contain_bdv (Rule.Cal1 _ :: rs) = contain_bdv rs

  | contain_bdv (Rule.Rls_ rls :: rs) = 

    contain_bdv (Rule.get_rules rls) orelse contain_bdv rs

  | contain_bdv (r :: _) = 

    error ("contain_bdv called with [" ^ Rule.id_rule r ^ ",...]");

(* filter Frees for free_str and pair their respective types with typ *)

fun subst_typ free_str typ frees =

  let

    val vars_v = filter (fn t => curry op = (t |> dest_Free |> fst) free_str) frees

    val typs_v = map (fn t => (t |> dest_Free |> snd)) vars_v

  in

    map (fn T => (T, typ)) typs_v

  end

(* instantiate typs in Prog auto_generated or auto_generated_ins for args "t_t", "v" *)

fun subst_typs prog typ_t typ_bdv =

  let

    val args = Program.formal_args prog

    val frees = TermC.vars prog

    val prog' = subst_atomic_types (subst_typ "t_t" typ_t frees) prog

  in

    if length args <= 1

    then

      prog'

    else (* auto_generated_inst has second argument "v" *)

      subst_atomic_types (subst_typ "v" typ_bdv frees) prog'

  end

fun rules2scr_Rls thy rules =

    if contain_bdv rules

    then FunID_Term_Bdv $ (Repeat $ (((op #> o (map (rule2stac_inst thy))) rules) $ Rule.e_term))

    else FunID_Term $ (Repeat $ (((op #> o (map (rule2stac thy))) rules) $ Rule.e_term));

fun rules2scr_Seq thy rules =

    if contain_bdv rules

    then FunID_Term_Bdv $ (((op #> o (map (rule2stac_inst thy))) rules) $ Rule.e_term)

    else FunID_Term $ (((op #> o (map (rule2stac thy))) rules) $ Rule.e_term);

(* REPLACED BY Auto_Prog.gen:

   prepare the input for an rls for use:

   # generate a program for stepwise execution of the rls

   # filter the operators for Num_Calc out of the script ?WN111014?

   use this function while storing (TODO integrate..) into KEStore_Elems.add_rlss

*)

fun prep_rls _ Rule.Erls = error "prep_rls: not required for Erls"

  | prep_rls thy (Rule.Rls {id, preconds, rew_ord, erls, srls, rules, errpatts, ...}) = 

      let

        val sc = (rules2scr_Rls thy rules)

      in

        Rule.Rls {id = id, preconds = preconds, rew_ord = rew_ord, erls = erls, srls = srls,

  	      calc = get_calcs thy sc,

  	      rules = rules, errpatts = errpatts,

  	      scr = Rule.EmptyScr (*Rule.Prog sc  AD-HOC REPLACED BY Auto_Prog.gen*)} end

  | prep_rls thy (Rule.Seq {id, preconds, rew_ord, erls, srls, rules, errpatts, ...}) = 

      let

        val sc = (rules2scr_Seq thy rules)

      in

        Rule.Seq {id = id, preconds = preconds, rew_ord = rew_ord, erls = erls, srls = srls,

	        calc = get_calcs thy sc,

	        rules = rules, errpatts = errpatts,

  	      scr = Rule.EmptyScr (*Rule.Prog sc  AD-HOC REPLACED BY Auto_Prog.gen*)} end

  | prep_rls _ (Rule.Rrls {id, ...}) = 

      error ("prep_rls: not required for Rrls \"" ^ id ^ "\"");

(* on the fly generate a Prog from an rls for Math_Engine.detailstep.

  Types are not precise, but these are not required by LI.

  Argument "thy" is only required for lookup in KEStore.

*)

fun gen thy t rls =

  let

    val prog = case rls of

	      Rule.Rls {rules, ...} => rules2scr_Rls thy rules

	    | Rule.Seq {rules, ...} => rules2scr_Seq thy rules

	    | _ => raise ERROR ("Auto_Prog.gen: not for rule-set \"" ^ Rule.id_rls rls ^ "\"")

  in

    subst_typs prog (type_of t) (TermC.guess_bdv_typ t)

  end

(**)end(**)

\<close> ML \<open>

\<close> ML \<open>

\<close> 

end