(* 

   authors: Walther Neuper 2002, 2006

  (c) due to copyright terms

tools for rewriting, reverse rewriting, context to thy concerning rewriting

*)

signature THEORY_DATA_PRESENTATION =

sig

  eqtype filename

  datatype contthy

      = ContNOrew of {applto: term, thm_rls: Check_Unique.id, thyID: ThyC.id}

    | ContNOrewInst of {applto: term, bdvs: subst, thm_rls: Check_Unique.id, thminst: term, thyID: ThyC.id}

    | ContRls of {applto: term, asms: term list, result: term, rls: Check_Unique.id, thyID: ThyC.id}

    | ContRlsInst of {applto: term, asms: term list, bdvs: subst, result: term, rls: Check_Unique.id, thyID: ThyC.id}

    | ContThm of {applat: term, applto: term, asmrls: Rule_Set.id, asms: (term * term) list,

      lhs: term * term, resasms: term list, result: term, reword: Rewrite_Ord.rew_ord', rhs: term * term,

      thm: Check_Unique.id, thyID: ThyC.id}

    | ContThmInst of {applat: term, applto: term, asmrls: Rule_Set.id, asms: (term * term) list,

      bdvs: subst, lhs: term * term, resasms: term list, result: term, reword: Rewrite_Ord.rew_ord',

      rhs: term * term, thm: Check_Unique.id, thminst: term, thyID: ThyC.id}

    | EContThy

  val guh2filename : Check_Unique.id -> filename

  val thms_of_rls : Rule_Set.T -> Rule.rule list

  val theID2filename : Thy_Write.theID -> filename

  val no_thycontext : Check_Unique.id -> bool

  val subs_from : Istate.T -> 'a -> Check_Unique.id -> Subst.input

  val guh2rewtac : Check_Unique.id -> Subst.input -> Tactic.input

  val get_tac_checked : Ctree.ctree -> Pos.pos' -> Tactic.input

  val context_thy : Calc.T -> Tactic.input -> contthy

  val guh2theID : Check_Unique.id -> Thy_Write.theID

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

  (*  NONE *)

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

  (*  NONE *)

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

end 

(**)

structure Thy_Present(**): THEORY_DATA_PRESENTATION(**) =

struct

(**)

type filename = string;

(* packing return-values to matchTheory, contextToThy for xml-generation *)

datatype contthy =  (*also an item from Know_Store on Browser ...........#*)

	EContThy   (* not from Know_Store ..............................*)

  | ContThm of (* a theorem in contex ===========================*)

    {thyID   : ThyC.id,      (* for *2guh in sub-elems here        .*)

     thm     : Check_Unique.id,       (* theorem in the context             .*)

     applto  : term,	          (* applied to formula ...             .*)

     applat  : term,	          (* ...  with lhs inserted             .*)

     reword  : Rewrite_Ord.rew_ord',   (* order used for rewrite             .*)

     asms    : (term            (* asumption instantiated             .*)

   	   * term) list,            (* asumption evaluated                .*)

     lhs     : term             (* lhs of the theorem ...             #*)

   	   * term,                  (* ... instantiated                   .*)

     rhs     : term             (* rhs of the theorem ...             #*)

   	   * term,                  (* ... instantiated                   .*)

     result  : term,	          (* resulting from the rewrite         .*)

     resasms : term list,       (* ... with asms stored               .*)

     asmrls  : Rule_Set.id        (* ruleset for evaluating asms        .*)

   	}						 

  | ContThmInst of (* a theorem with bdvs in contex ============ *)

    {thyID   : ThyC.id,      (*for *2guh in sub-elems here         .*)

     thm     : Check_Unique.id,       (*theorem in the context              .*)

     bdvs    : subst,      (*bound variables to modify...        .*)

     thminst : term,            (*... theorem instantiated            .*)

     applto  : term,	          (*applied to formula ...              .*)

     applat  : term,	          (*...  with lhs inserted              .*)

     reword  : Rewrite_Ord.rew_ord',   (*order used for rewrite              .*)

     asms    : (term            (*asumption instantiated              .*)

   	   * term) list,            (*asumption evaluated                 .*)

     lhs     : term             (*lhs of the theorem ...              #*)

   	   * term,                  (*... instantiated                    .*)

     rhs     : term             (*rhs of the theorem ...              #*)

   	   * term,                  (*... instantiated                    .*)

     result  : term,	          (*resulting from the rewrite          .*)

     resasms : term list,       (*... with asms stored                .*)

     asmrls  : Rule_Set.id        (*ruleset for evaluating asms         .*)

    }						 

  | ContRls of (* a rule set in contex ========================= *)

    {thyID   : ThyC.id,      (*for *2guh in sub-elems here         .*)

     rls     : Check_Unique.id,       (*rule set in the context             .*)

     applto  : term,	          (*rewrite this formula                .*)

     result  : term,	          (*resulting from the rewrite          .*)

     asms    : term list        (*... with asms stored                .*)

   	}						 

  | ContRlsInst of (* a rule set with bdvs in contex =========== *)

	{thyID   : ThyC.id,        (*for *2guh in sub-elems here         .*)

	 rls     : Check_Unique.id,         (*rule set in the context             .*)

	 bdvs    : subst,        (*for bound variables in thms         .*)

	 applto  : term,	            (*rewrite this formula                .*)

	 result  : term,	            (*resulting from the rewrite          .*)

	 asms    : term list          (*... with asms stored                .*)

   	}						 

  | ContNOrew of (* no rewrite for thm or rls ================== *)

    {thyID   : ThyC.id,      (*for *2guh in sub-elems here         .*)

     thm_rls : Check_Unique.id,       (*thm or rls in the context           .*)

     applto  : term	            (*rewrite this formula                .*)

   	}						 

  | ContNOrewInst of (* no rewrite for some instantiation ====== *)

    {thyID   : ThyC.id,      (*for *2guh in sub-elems here         .*)

     thm_rls : Check_Unique.id,       (*thm or rls in the context           .*)

     bdvs    : subst,      (*for bound variables in thms         .*)

     thminst : term,            (*... theorem instantiated            .*)

     applto  : term	            (*rewrite this formula                .*)

   	}						 

(*.check a rewrite-tac for bdv (RL always used *_Inst !) TODO.WN060718

   pass other tacs unchanged.*)

fun get_tac_checked pt ((p, _) : Pos.pos') = Ctree.get_obj Ctree.g_tac pt p;

(* get the formula f at ptp rewritten by the Rewrite_* already applied to f *)

fun context_thy (pt, pos as (p, p_)) (tac as Tactic.Rewrite thm'') =

    let

      val thm_deriv = ThmC.long_id thm''

    in

    (case Step.check tac (pt, pos) of

      Applicable.Yes (Tactic.Rewrite' (thy', ord', erls, _, _, f, (res, asm))) =>

        ContThm

         {thyID = thy',

          thm = Thy_Write.thm2guh (Thy_Read.thy_containing_thm thm_deriv) (ThmC.cut_id thm_deriv),

          applto = f, applat  = TermC.empty, reword  = ord',

          asms = [](*asms ~~ asms'*), lhs = (TermC.empty, TermC.empty)(*(lhs, lhs')*), rhs = (TermC.empty, TermC.empty)(*(rhs, rhs')*),

          result = res, resasms = asm, asmrls  = Rule_Set.id erls}

     | Applicable.No _ =>

         let

           val pp = Ctree.par_pblobj pt p

           val thy' = Ctree.get_obj Ctree.g_domID pt pp

           val f = case p_ of

             Pos.Frm => Ctree.get_obj Ctree.g_form pt p

           | Pos.Res => (fst o (Ctree.get_obj Ctree.g_result pt)) p 

           | _ => error "context_thy: uncovered position"

         in

           ContNOrew

            {thyID   = thy',

             thm_rls = 

               Thy_Write.thm2guh (Thy_Read.thy_containing_thm thm_deriv) (ThmC.cut_id thm_deriv),

             applto  = f}

		     end

     | _ => error "context_thy..Rewrite: uncovered case 2")

    end

  | context_thy (pt, pos as (p, p_)) (tac as Tactic.Rewrite_Inst (subs, (thmID, _))) =

    let val thm = Global_Theory.get_thm (ThyC.Isac ()) thmID

    in

	  (case Step.check tac (pt, pos) of

	     Applicable.Yes (Tactic.Rewrite_Inst' (thy', ord', erls, _, subst, _, f, (res, asm))) =>

	       let

           val thm_deriv = Thm.get_name_hint thm

           val thminst = TermC.inst_bdv subst ((Eval.norm o #prop o Thm.rep_thm) thm)

	       in

	         ContThmInst

	          {thyID = thy',

	           thm = 

	             Thy_Write.thm2guh (Thy_Read.thy_containing_thm thm_deriv) (ThmC.cut_id thm_deriv),

	           bdvs = subst, thminst = thminst, applto  = f, applat  = TermC.empty, reword  = ord',

	           asms = [](*asms ~~ asms'*), lhs = (TermC.empty, TermC.empty)(*(lhs, lhs')*), rhs = (TermC.empty, TermC.empty)(*(rhs, rhs')*),

	           result = res, resasms = asm, asmrls  = Rule_Set.id erls}

	       end

     | Applicable.No _ =>

         let

           val thm = Global_Theory.get_thm (ThyC.Isac ()(*WN141021 assoc_thy thy' ERROR*)) thmID

           val thm_deriv = Thm.get_name_hint thm

           val pp = Ctree.par_pblobj pt p

           val thy' = Ctree.get_obj Ctree.g_domID pt pp

           val subst = Subst.T_from_input (ThyC.get_theory thy') subs

           val thminst = TermC.inst_bdv subst ((Eval.norm o #prop o Thm.rep_thm) thm)

           val f = case p_ of

               Pos.Frm => Ctree.get_obj Ctree.g_form pt p

             | Pos.Res => (fst o (Ctree.get_obj Ctree.g_result pt)) p 

             | _ => error "context_thy: uncovered case 3"

         in

           ContNOrewInst

            {thyID = thy',

             thm_rls = Thy_Write.thm2guh (Thy_Read.thy_containing_thm thm_deriv) (ThmC.cut_id thm_deriv),

             bdvs = subst, thminst = thminst, applto = f}

         end

      | _ => error "context_thy..Rewrite_Inst: uncovered case 4")

    end

  | context_thy (pt, p) (tac as Tactic.Rewrite_Set rls') =

    (case Step.check tac (pt, p) of

       Applicable.Yes (Tactic.Rewrite_Set' (thy', _, _(*rls*), f, (res,asm))) =>

         ContRls

          {thyID = thy',

           rls = Thy_Write.rls2guh (Thy_Read.thy_containing_rls thy' rls') rls',

           applto = f, result = res, asms = asm}

     | _ => error ("context_thy Rewrite_Set: not for Applicable.No"))

  | context_thy (pt,p) (tac as Tactic.Rewrite_Set_Inst (_(*subs*), rls')) = 

    (case Step.check tac (pt, p) of

       Applicable.Yes (Tactic.Rewrite_Set_Inst' (thy', _, subst, _, f, (res,asm))) =>

         ContRlsInst

          {thyID = thy',

           rls = Thy_Write.rls2guh (Thy_Read.thy_containing_rls thy' rls') rls',

           bdvs = subst, applto = f, result = res, asms = asm}

     | _ => error ("context_thy Rewrite_Set_Inst: not for Applicable.No"))

  | context_thy (_, p) tac =

      error ("context_thy: not for tac " ^ Tactic.input_to_string tac ^ " at " ^ Pos.pos'2str p)

(* get all theorems in a rule set (recursivley containing rule sets) *)

fun thm_of_rule Rule.Erule = []

  | thm_of_rule (thm as Rule.Thm _) = [thm]

  | thm_of_rule (Rule.Eval _) = []

  | thm_of_rule (Rule.Cal1 _) = []

  | thm_of_rule (Rule.Rls_ rls) = thms_of_rls rls

and thms_of_rls Rule_Set.Empty = []

  | thms_of_rls (Rule_Def.Repeat {rules,...}) = (flat o (map  thm_of_rule)) rules

  | thms_of_rls (Rule_Set.Sequence {rules,...}) = (flat o (map  thm_of_rule)) rules

  | thms_of_rls (Rule_Set.Rrls _) = []

(* filenames not only for thydata, but also for thy's etc *)

fun theID2filename theID = Thy_Write.theID2guh theID ^ ".xml"

fun guh2theID guh =

  let

    val guh' = Symbol.explode guh

    val part = implode (take_fromto 1 4 guh')

    val isa = implode (take_fromto 5 9 guh')

  in

    if not (member op = ["exp_", "thy_", "pbl_", "met_"] part)

    then raise ERROR ("guh '" ^ guh ^ "' does not begin with exp_ | thy_ | pbl_ | met_")

    else

      let

  	    val chap = case isa of

  		  "isab_" => "Isabelle"

  		| "scri_" => "IsacScripts"

  		| "isac_" => "IsacKnowledge"

  		| _ =>

  		  raise ERROR ("guh2theID: '" ^ guh ^ "' does not have isab_ | scri_ | isac_ at position 5..9")

        val rest = takerest (9, guh') 

        val thyID = takewhile [] (not o (curry op= "-")) rest

        val rest' = dropuntil (curry op = "-") rest

	    in case implode rest' of

		    "-part" => [chap] : Thy_Write.theID

      | "" => [chap, implode thyID]

      | "-Theorems" => [chap, implode thyID, "Theorems"]

      | "-Rulesets" => [chap, implode thyID, "Rulesets"]

      | "-Operations" => [chap, implode thyID, "Operations"]

      | "-Orders" => [chap, implode thyID, "Orders"]

      | _ => 

		    let val sect = implode (take_fromto 1 5 rest')

		       val sect' = case sect of

			       "-thm-" => "Theorems"

			     | "-rls-" => "Rulesets"

			     | "-cal-" => "Operations"

			     | "-ord-" => "Orders"

			     | _ =>

			     raise ERROR ("guh2theID: '" ^ guh ^ "' has '" ^ sect ^ "' instead -thm- | -rls- | -cal- | -ord-")

		    in

		      [chap, implode thyID, sect', implode (takerest (5, rest'))]

		    end

	    end	

    end

fun guh2filename guh = guh ^ ".xml";

fun guh2rewtac guh [] =

    let

      val (_, thy, sect, xstr) = case guh2theID guh of

        [isa, thy, sect, xstr] => (isa, thy, sect, xstr)

      | _ => error "guh2rewtac: uncovered case"

    in case sect of

      "Theorems" => Tactic.Rewrite (xstr, ThmC.thm_from_thy (ThyC.get_theory thy) xstr)

    | "Rulesets" => Tactic.Rewrite_Set xstr

    | _ => error ("guh2rewtac: not impl. for '"^xstr^"'") 

    end

  | guh2rewtac guh subs =

    let

      val (_, thy, sect, xstr) = case guh2theID guh of

        [isa, thy, sect, xstr] => (isa, thy, sect, xstr)

      | _ => error "guh2rewtac: uncovered case"

    in case sect of

      "Theorems" => 

        Tactic.Rewrite_Inst (subs, (xstr, ThmC.thm_from_thy (ThyC.get_theory thy) xstr))

    | "Rulesets" => Tactic.Rewrite_Set_Inst (subs,  xstr)

    | str => error ("guh2rewtac: not impl. for '" ^ str ^ "'") 

    end

(* the front-end may request a context for any element of the hierarchy *)

fun no_thycontext guh = (guh2theID guh; false)

  handle ERROR _ => true;

(* get the substitution of bound variables for matchTheory:

   # lookup the thm|rls' in the script

   # take the [(bdv, v_),..] from the respective Rewrite_(Set_)Inst

   # instantiate this subs with the istates env to [(bdv, x),..]

   # otherwise []

   WN060617 hack assuming that all scripts use only one bound variable

   and use 'v_' as the formal argument for this bound variable*)

fun subs_from (Istate.Pstate ({env, ...})) _ guh =

    let

      val (_, _, thyID, sect, xstr) = case guh2theID guh of

        theID as [isa, thyID, sect, xstr] => (theID, isa, thyID, sect, xstr)

      | _ => error "subs_from: uncovered case"

    in

      case sect of

        "Theorems" => 

          let val thm = Global_Theory.get_thm (ThyC.get_theory thyID) xstr

          in

            if Auto_Prog.contains_bdv thm

            then

              let

                val formal_arg = TermC.str2term "v_"      

                val value = subst_atomic env formal_arg

              in ["(''bdv''," ^ UnparseC.term value ^ ")"] : Subst.input end

            else []

	        end

  	  | "Rulesets" => 

        let

          val rules = (Rule_Set.get_rules o assoc_rls) xstr

        in

          if Auto_Prog.contain_bdv rules

          then

            let

              val formal_arg = TermC.str2term "v_"

              val value = subst_atomic env formal_arg

            in ["(''bdv''," ^ UnparseC.term value ^ ")"] : Subst.input end

          else []

        end

      | str => error ("subs_from: uncovered case with " ^ str)

    end

  | subs_from _ _  guh = error ("subs_from: uncovered case with " ^ guh)

(**)end(**)