(* 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