(* 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 -> Spec.pblID -> term

     val subpbl: string -> string list -> term

     val stacpbls: term -> term list

     val op_of_calc: term -> string

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

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

     val gen: theory -> term -> Rule_Set.T -> 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 TermC.empty t of

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

     in (distinct 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 ("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 " ^ UnparseC.term 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.Eval (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_Set.id rls))

   | rule2stac _ r = raise ERROR ("rule2stac: not applicable to \"" ^ Rule.to_string 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 (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_Set.id rls))

   | rule2stac_inst _ r = raise ERROR ("rule2stac_inst: not applicable to \"" ^ Rule.to_string 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  ^ "\"");

 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 \"" ^ UnparseC.terms 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.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 :: _) = 

     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 KEStore_Elems.add_rlss

 *)

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

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

       let

         val sc = (rules2scr_Rls thy rules)

       in

         Rule_Def.Repeat {id = id, preconds = preconds, rew_ord = rew_ord, erls = erls, srls = srls,

   	      calc = get_calcs thy sc,

   	      rules = rules, errpatts = errpatts,

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

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

       let

         val sc = (rules2scr_Seq thy rules)

       in

         Rule_Set.Sequence {id = id, preconds = preconds, rew_ord = rew_ord, erls = erls, srls = srls,

 	        calc = get_calcs thy sc,

 	        rules = rules, errpatts = errpatts,

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

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

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

 \<close> ML \<open>

 \<close> ML \<open>

 \<close> 

 end