(* 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: ThyC.id -> Probl_Def.id -> term

    val subpbl: string -> string list -> term

    val stacpbls: term -> term list

    val op_of_calc: term -> string

    val get_calcs: theory -> term -> Eval_Def.ml_from_prog list

    val prep_rls: theory -> Rule_Set.T -> Rule_Set.T (*ren insert*)

    val gen: theory -> term -> Rule_Set.T -> term

\<^isac_test>\<open>

    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

\<close>

  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 $ _ $ _) = (TermC.parseNEW'' @{theory Prog_Tac})

  "Subproblem (''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 =

  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 (\<^const_name>\<open>Let\<close>, _) $ e $ (Abs (_, _, b))) = (scan e) @ (scan b)

        | scan (Const (\<^const_name>\<open>Tactical.If\<close>, _) $ _ $ e1 $ e2) = (scan e1) @ (scan e2)

        | scan (Const (\<^const_name>\<open>Tactical.While\<close>, _) $ _ $ e $ _) = scan e

        | scan (Const (\<^const_name>\<open>Tactical.While\<close>, _) $ _ $ e) = scan e

        | scan (Const (\<^const_name>\<open>Tactical.Repeat\<close>, _) $ e $ _) = scan e

        | scan (Const (\<^const_name>\<open>Tactical.Repeat\<close>, _) $ e) = scan e

        | scan (Const (\<^const_name>\<open>Tactical.Try\<close>, _) $ e $ _) = scan e

        | scan (Const (\<^const_name>\<open>Tactical.Try\<close>, _) $ e) = scan e

        | scan (Const (\<^const_name>\<open>Tactical.Or\<close>, _) $ e1 $ e2 $ _) = (scan e1) @ (scan e2)

        | scan (Const (\<^const_name>\<open>Tactical.Or\<close>, _) $ e1 $ e2) = (scan e1) @ (scan e2)

        | scan (Const (\<^const_name>\<open>Tactical.Chain\<close>, _) $ e1 $ e2 $ _) = (scan e1) @ (scan e2)

        | scan (Const (\<^const_name>\<open>Tactical.Chain\<close>, _) $ e1 $ e2) = (scan e1) @ (scan e2)

        | scan t = case Prog_Tac.eval_leaf [] NONE TermC.empty t of

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

    in ((distinct op =) o scan) body end

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

(* get operators out of a program *)

fun is_calc (Const (\<^const_name>\<open>Prog_Tac.Calculate\<close>,_) $ _) = true

  | is_calc (Const (\<^const_name>\<open>Prog_Tac.Calculate\<close>,_) $ _ $ _) = true

  | is_calc _ = false;

fun op_of_calc (Const (\<^const_name>\<open>Prog_Tac.Calculate\<close>,_) $ op_) = HOLogic.dest_string op_

  | op_of_calc (Const (\<^const_name>\<open>Prog_Tac.Calculate\<close>,_) $ op_ $ _) = HOLogic.dest_string op_

  | op_of_calc t = raise ERROR ("op_of_calc called with " ^ UnparseC.term t);

fun get_calcs thy sc =

    sc

    |> stacpbls

    |> filter is_calc

    |> map op_of_calc

    |> (get_calc (Proof_Context.init_global 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 (TermC.parseNEW'' @{theory}))

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

val Try $ _ = (TermC.inst_abs o (TermC.parseNEW'' @{theory}))

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

val Cal $ _ = (TermC.inst_abs o (TermC.parseNEW'' @{theory}))

	"Calculate ''PLUS''";

val Ca1 $ _ = (TermC.inst_abs o (TermC.parseNEW'' @{theory}))

	"Calculate1 ''PLUS''";

val Rew $ _ $ _ = (TermC.inst_abs o (TermC.parseNEW'' @{theory}))

	"Rewrite ''real_diff_minus'' t";

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

val Rew_Inst $ Subs $ _ = (TermC.inst_abs o (TermC.parseNEW'' @{theory}))

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

val Rew_Set $ _ = (TermC.inst_abs o (TermC.parseNEW'' @{theory}))

	"Rewrite_Set ''real_diff_minus''";

val Rew_Set_Inst $ _ $ _ = (TermC.inst_abs o (TermC.parseNEW'' @{theory}))

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

val SEq $ _ $ _ $ _ = (TermC.inst_abs o (TermC.parseNEW'' @{theory}))

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

        \   (Try (Repeat (Rewrite ''add.commute''))) #> \

        \   (Try (Repeat (Rewrite ''mult_commute'')))) t"; (*has not yet been needed*)

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

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

    (get_calc_prog_id (Proof_Context.init_global thy) c)))

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

    (get_calc_prog_id (Proof_Context.init_global thy) c)))

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

  | rule2stac thy r = raise ERROR ("rule2stac: not applicable to \"" ^

      Rule.to_string (Proof_Context.init_global thy) r ^ "\"");

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

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

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

    Try $ (Repeat $ (Cal $ HOLogic.mk_string (get_calc_prog_id (Proof_Context.init_global thy) c)))

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

    Try $ (Repeat $ (Cal $ HOLogic.mk_string (get_calc_prog_id (Proof_Context.init_global thy) c)))

  | rule2stac_inst _ (Rule.Rls_ rls) = 

    Try $ (Rew_Set_Inst $ Subs $ HOLogic.mk_string (Rule_Set.id rls))

  | rule2stac_inst thy r = raise ERROR ("rule2stac_inst: not applicable to \"" ^

      Rule.to_string (Proof_Context.init_global thy) 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 \"" ^ UnparseC.term t ^ "\" \"" ^ UnparseC.terms ts  ^ "\"");

(*IS NOT*)

fun op #> [stac] = stac

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

  | op #> stacs = case rev stacs of

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

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

val contains_bdv = not o null o filter TermC.is_bdv o TermC.ids2str o Thm.prop_of;

(* 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.Eval _ :: rs) = contain_bdv rs

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

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

    contain_bdv (Rule_Set.get_rules rls) orelse contain_bdv rs

  | contain_bdv (r :: _) = 

    raise ERROR ("contain_bdv called with [" ^ Rule.id 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) $ TermC.empty))

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

fun rules2scr_Seq thy rules =

    if contain_bdv rules

    then FunID_Term_Bdv $ (((op #> o (map (rule2stac_inst thy))) rules) $ TermC.empty)

    else FunID_Term $ (((op #> o (map (rule2stac thy))) rules) $ TermC.empty);

(* 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 Eval out of the script ?WN111014?

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

*)

fun prep_rls _ Rule_Set.Empty = raise ERROR "prep_rls: not required for Erls"

  | prep_rls thy (Rule_Def.Repeat {id, preconds, rew_ord, asm_rls, prog_rls, rules, errpatts, ...}) = 

      let

        val sc = rules2scr_Rls thy rules

      in

        Rule_Def.Repeat {id = id, preconds = preconds, rew_ord = rew_ord, asm_rls = asm_rls, prog_rls = prog_rls,

  	      calc = get_calcs thy sc,

  	      rules = rules, errpatts = errpatts,

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

  | prep_rls thy (Rule_Set.Sequence {id, preconds, rew_ord, asm_rls, prog_rls, rules, errpatts, ...}) = 

      let

        val sc = (rules2scr_Seq thy rules)

      in

        Rule_Set.Sequence {id = id, preconds = preconds, rew_ord = rew_ord, asm_rls = asm_rls, prog_rls = prog_rls,

	        calc = get_calcs thy sc,

	        rules = rules, errpatts = errpatts,

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

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

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

(* on the fly generate a Prog from an rls for Detail_Step.go.

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

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

*)

fun gen thy t rls =

  let

    val prog = case rls of

	      Rule_Def.Repeat {rules, ...} => rules2scr_Rls thy rules

	    | Rule_Set.Sequence {rules, ...} => rules2scr_Seq thy rules

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

  in

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

  end

(**)end(*Auto_Prog*)

\<close> ML \<open>

\<close> ML \<open>

\<close> 

end