(* isac's rewriter

   (c) Walther Neuper 2000

*)

signature REWRITE =

sig

  exception NO_REWRITE

  val calculate_: Proof.context -> string * Eval_Def.eval_fn -> term -> (term * (string * thm)) option

  val eval__true: Proof.context -> int -> term list -> Subst.T -> Rule_Set.T -> term list * bool

  val eval_prog_expr: Proof.context -> Rule_Set.T -> term -> term

  val eval_true_: Proof.context -> Rule_Set.T -> term -> bool

  val eval_true: Proof.context -> term list -> Rule_Set.T -> bool

  val rew_sub: Proof.context -> int -> Subst.T -> Rewrite_Ord.function

    -> Rule_Set.T -> bool -> TermC.path -> term -> term -> term * term list * TermC.path * bool

  val rewrite_: Proof.context -> Rewrite_Ord.function -> Rule_Set.T -> bool -> thm ->

    term -> (term * term list) option

  val rewrite_inst_: Proof.context -> Rewrite_Ord.function -> Rule_Set.T -> bool

    -> Subst.T -> thm -> term -> (term * term list) option

  val rewrite_set_: Proof.context -> bool -> Rule_Set.T -> term -> (term * term list) option

  val rewrite_set_inst_: Proof.context -> bool -> Subst.T -> Rule_Set.T -> term -> (term * term list) option

  val rewrite_terms_: Proof.context -> Rewrite_Ord.function -> Rule_Set.T -> term list

    -> term -> (term * term list) option

\<^isac_test>\<open>

  val rewrite__: Proof.context -> int -> Subst.T -> Rewrite_Ord.function ->

    Rule_Set.T -> bool -> thm -> term -> (term * term list) option

  val rewrite__set_: Proof.context -> int -> bool -> Subst.T -> Rule_Set.T -> term -> (term * term list) option

  val app_rev: Proof.context -> int -> Rule_Set.T -> term -> term * term list * bool

  val app_sub: Proof.context -> int -> Rule_Set.T -> term -> term * term list * bool

  val trace1: Proof.context -> int -> string -> unit

  val trace_eq1 : Proof.context -> int -> string -> Rule_Def.rule_set -> term -> unit;

  val trace_eq2 : Proof.context -> int -> string -> term -> term -> unit;

  val trace_in1 : Proof.context -> int -> string -> string -> unit;

  val trace_in2 : Proof.context -> int -> string -> term -> unit;

  val trace_in3 : Proof.context -> int -> string -> (term * 'a) option -> unit;

  val trace_in4 : Proof.context -> int -> string -> term list -> term list -> unit;

  val trace_in5 : Proof.context -> int -> string -> term list -> unit;

\<close>

end

(* must be global for re-use in other structs *)

val rewrite_trace = Attrib.setup_config_bool \<^binding>\<open>rewrite_trace\<close> (K false);

(* no of rewrites exceeding this int -> NO_REWRITE *)

val rewrite_limit = Attrib.setup_config_int \<^binding>\<open>rewrite_limit\<close> (K 100);

(**)

structure Rewrite(**): REWRITE(**) =

struct

(**)

exception NO_REWRITE;

(* depth of recursion in traces of the rewriter, if trace_on = true *)

val rewrite_trace_depth = Attrib.setup_config_int \<^binding>\<open>rewrite_trace_depth\<close> (K 99999);

fun trace ctxt i str = 

  if Config.get ctxt rewrite_trace andalso i < Config.get ctxt rewrite_trace_depth

  then tracing (idt "#" i ^ str) else ()

fun trace_eq1 ctxt i str rrls t =

  trace ctxt i (" " ^ str ^ ": " ^ Rule_Set.id rrls ^ " on: " ^ UnparseC.term_in_ctxt ctxt t)

fun trace_eq2 ctxt i str t t' =

  trace ctxt i (" " ^ str ^ ": \"" ^

    UnparseC.term_in_ctxt ctxt t ^ "\" > \"" ^ UnparseC.term_in_ctxt ctxt t' ^ "\"");

fun trace1 ctxt i str =

  if Config.get ctxt rewrite_trace andalso i < Config.get ctxt rewrite_trace_depth

  then tracing (idt "#" (i + 1) ^ str) else ()

fun trace_in1 ctxt i str thmid =

  trace1 ctxt i (" " ^ str ^ ": \"" ^ thmid ^ "\"")

fun trace_in2 ctxt i str t =

  trace1 ctxt i (" " ^ str ^ ": \"" ^ UnparseC.term_in_ctxt ctxt t ^ "\"");

fun trace_in3 ctxt i str pairopt =

  trace1 ctxt i (" " ^ str ^ ": " ^ UnparseC.term_in_ctxt ctxt ((fst o the) pairopt));

fun trace_in4 ctxt i str ts ts' =

  if Config.get ctxt rewrite_trace andalso i < Config.get ctxt rewrite_trace_depth andalso ts <> []

  then tracing (idt "#" (i + 1) ^ " " ^ str ^ ": " ^ UnparseC.terms_in_ctxt ctxt ts ^

  	"   stored: " ^ UnparseC.terms_in_ctxt ctxt ts')

  else ();

fun trace_in5 ctxt i str p' =

  if Config.get ctxt rewrite_trace andalso i < Config.get ctxt rewrite_trace_depth

  then tracing (idt "#" (i + 1) ^ " " ^ str ^ ": " ^ UnparseC.terms_in_ctxt ctxt p')

  else();

fun msg call ctxt op_ thmC t = 

  call ^ ": \n" ^

  "Eval.get_pair for " ^ quote op_ ^ " \<longrightarrow> SOME (_, " ^ quote (ThmC.string_of_thm thmC) ^ ")\n" ^

  "but rewrite__ on " ^ quote (UnparseC.term_in_ctxt ctxt t) ^ " \<longrightarrow> NONE";

fun rewrite__ ctxt i bdv tless rls put_asm thm ct =

  let

    val (t', asms, _(*lrd*), rew) = rew_sub ctxt i bdv tless rls put_asm ([(*root of the term*)]: TermC.path)

		  (TermC.inst_bdv bdv (Eval.norm (Thm.prop_of thm))) ct

  in if rew then SOME (t', distinct op = asms) else NONE end

  (* one rewrite (possibly conditional, ordered) EXOR exn EXOR go into subterms *)

and rew_sub ctxt i bdv tless rls put_asm lrd r t = 

  (let

    val (lhs, rhs) = (HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r

    val r' = (Envir.subst_term (Pattern.match (Proof_Context.theory_of ctxt) 

      (lhs, t) (Vartab.empty, Vartab.empty)) r)

      handle Pattern.MATCH => raise NO_REWRITE

    val p' = map HOLogic.dest_Trueprop ((fst o Logic.strip_prems) (Logic.count_prems r', [], r'))

    val t' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r'

    val _ = trace_in2 ctxt i "eval asms" r';

    val (t'', p'') =                                                      (*conditional rewriting*)

      let val (simpl_p', nofalse) = eval__true ctxt (i + 1) p' bdv rls 	     

	    in

	      if nofalse

        then (trace_in4 ctxt i "asms accepted" p' simpl_p'; (t', simpl_p'))(*uncond.rew.from above*)

        else (trace_in5 ctxt i "asms false" p'; raise NO_REWRITE)   (* don't go into subtm.of cond*)

	    end                                    

  in

    if TermC.perm lhs rhs andalso not (tless bdv (t', t))                     (*ordered rewriting*)

    then (trace_eq2 ctxt i "not >" t t'; raise NO_REWRITE)

    else (t'', p'', [], true)

  end

  ) handle NO_REWRITE =>

    (case t of

      Const(s, T) => (Const(s, T), [], lrd, false)

    | Free(s, T) => (Free(s, T), [], lrd, false)

    | Var(n, T) => (Var(n, T), [], lrd, false)

    | Bound i => (Bound i, [], lrd, false)

    | Abs(s, T, body) => 

      let val (t', asms, _ (*lrd*), rew) =  rew_sub ctxt i bdv tless rls put_asm (lrd @ [TermC.D]) r body

       in (Abs(s, T, t'), asms, [], rew) end

    | t1 $ t2 => 

       let val (t2', asm2, lrd, rew2) = rew_sub ctxt i bdv tless rls put_asm (lrd @ [TermC.R]) r t2

       in

        if rew2 then (t1 $ t2', asm2, lrd, true)

        else

          let val (t1', asm1, lrd, rew1) = rew_sub ctxt i bdv tless rls put_asm (lrd @ [TermC.L]) r t1

          in if rew1 then (t1' $ t2, asm1, lrd, true) else (t1 $ t2,[], lrd, false) end

    end)

and eval__true ctxt i asms bdv rls =            (* rewrite asumptions until one evaluates to false*)

  if asms = [@{term True}] orelse asms = [] then ([], true)

  else (* this allows to check Rrls with prepat = ([@{term True}], pat) *)

    if asms = [@{term False}] then ([], false)

    else

      let                            

        fun chk indets [] = (indets, true) (*return asms<>True until false*)

          | chk indets (a :: asms) =

            (case rewrite__set_ ctxt (i + 1) false bdv rls a of

              NONE => (chk (indets @ [a]) asms)

            | SOME (t, a') =>

              if t = @{term True} then (chk (indets @ a') asms) 

              else if t = @{term False} then ([], false)

            (*asm false .. thm not applied ^^^; continue until False vvv*)

            else chk (indets @ [t] @ a') asms);

      in chk [] asms end

and rewrite__set_ ctxt (*1*)_ _ _ Rule_Set.Empty t =                         (* rewrite with a rule set*)

    raise ERROR ("rewrite__set_ called with 'Erls' for '" ^ UnparseC.term_in_ctxt ctxt t ^ "'")

  | rewrite__set_ (*2*)ctxt i _ _ (rrls as Rule_Set.Rrls _) t =    (* rewrite with a 'reverse rule set'*)

    let

      val _= trace_eq1 ctxt i "rls" rrls t;

	    val (t', asm, rew) = app_rev ctxt (i + 1) rrls t                   

    in if rew then SOME (t', distinct op = asm) else NONE end

  | rewrite__set_ (*3*)ctxt i put_asm bdv rls ct =           (* Rls, Seq containing Thms or Eval, Cal1 *)

    let

      (* attention with cp to test/..: unbound ctxt, i, bdv, rls; TODO1803? pull out to rewrite__*)

      datatype switch = Appl | Noap;

      fun rew_once (*1*)_ asm ct Noap [] = (ct, asm) (* ?TODO unify with Prog_Expr.rew_once? *)

        | rew_once (*2*)ruls asm ct Appl [] = 

          (case rls of Rule_Def.Repeat _ => rew_once ruls asm ct Noap ruls

          | Rule_Set.Sequence _ => (ct, asm)

          | rls => raise ERROR ("rew_once not appl. to \"" ^ Rule_Set.id rls ^ "\""))

        | rew_once (*3*)ruls asm ct apno (rul :: thms) =

          case rul of

            Rule.Thm (thmid, thm) =>

              (trace_in1 ctxt i "try thm" thmid;

              case rewrite__ ctxt (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls)

                  ((#erls o Rule_Set.rep) rls) put_asm thm ct of

                NONE => rew_once ruls asm ct apno thms

              | SOME (ct', asm') => 

                (trace_in2 ctxt i "rewrites to" ct';

                rew_once ruls (union (op =) asm asm') ct' Appl (rul :: thms)))

                (* once again try the same rule, e.g. associativity against "()"*)

          | Rule.Eval (cc as (op_, _)) =>

            let val _ = trace_in1 ctxt i "try calc" op_;

            in case Eval.adhoc_thm (Proof_Context.theory_of ctxt) cc ct of

                NONE => rew_once ruls asm ct apno thms

              | SOME (_, thm') => 

                let 

                  val pairopt = rewrite__ ctxt (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls)

                    ((#erls o Rule_Set.rep) rls) put_asm thm' ct;

                  val _ = if pairopt <> NONE then () else raise ERROR (msg "rew_once" ctxt op_ thm' ct)

                  val _ = trace_in3 ctxt i "calc. to" pairopt;

                in rew_once ruls asm ((fst o the) pairopt) Appl (rul :: thms) end

            end

          | Rule.Cal1 (cc as (op_, _)) => 

            let val _ = trace_in1 ctxt i "try cal1" op_;

            in case Eval.adhoc_thm1_ (Proof_Context.theory_of ctxt) cc ct of

                NONE => (ct, asm)

              | SOME (_, thm') =>

                let 

                  val pairopt = rewrite__ ctxt (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls)

                    ((#erls o Rule_Set.rep) rls) put_asm thm' ct;

                  val _ = if pairopt <> NONE then () else raise ERROR ("rewrite_set_, rewrite_ \"" ^

                     ThmC.string_of_thm thm' ^ "\" " ^ UnparseC.term_in_ctxt ctxt ct ^ " = NONE")

                  val _ = trace_in3 ctxt i "cal1. to" pairopt;

                in the pairopt end

            end

          | Rule.Rls_ rls' => 

            (case rewrite__set_ ctxt (i + 1) put_asm bdv rls' ct of

              SOME (t', asm') => rew_once ruls (union (op =) asm asm') t' Appl thms

            | NONE => rew_once ruls asm ct apno thms)

          | r => raise ERROR ("rew_once not appl. to \"" ^ Rule.to_string r ^ "\"");

      val ruls = (#rules o Rule_Set.rep) rls;

      val _ = trace_eq1 ctxt i "rls" rls ct

      val (ct', asm') = rew_once ruls [] ct Noap ruls;

	  in if ct = ct' then NONE else SOME (ct', distinct op =  asm') end

(*--vvv and app_sub are type correct-----------------------------------------------------------*)

and app_rev ctxt i rrls t =             (* apply an Rrls; if not applicable proceed with subterms*)

  let (* check a (precond, pattern) of a rev-set; stops with 1st true *)

    fun chk_prepat _ _ [] _ = true

      | chk_prepat ctxt erls prepat t =

        let

          fun chk (pres, pat) =

            (let 

              val subst: Type.tyenv * Envir.tenv =

                Pattern.match (Proof_Context.theory_of ctxt) (pat, t) (Vartab.empty, Vartab.empty)

             in

              snd (eval__true ctxt (i + 1) (map (Envir.subst_term subst) pres) [] erls)

             end) handle Pattern.MATCH => false

           fun scan_ _ [] = false

             | scan_ f (pp :: pps) =

               if f pp then true else scan_ f pps;

        in scan_ chk prepat end;

    (* apply the normal_form of a rev-set *)

    fun app_rev' ctxt (Rule_Set.Rrls {erls, prepat, scr = Rule.Rfuns {normal_form, ...}, ...}) t =

      if chk_prepat ctxt erls prepat t then normal_form t else NONE

      | app_rev' _ r _ = raise ERROR ("app_rev' not appl. to \"" ^ Rule_Set.id r ^ "\"");

    val opt = app_rev' ctxt rrls t

  in

    case opt of

      SOME (t', asm) => (t', asm, true)

    | NONE => app_sub ctxt i rrls t

  end

and app_sub ctxt i rrls t =                                          (* apply an Rrls to subterms*)

  case t of

    Const (s, T) => (Const(s, T), [], false)

  | Free (s, T) => (Free(s, T), [], false)

  | Var (n, T) => (Var(n, T), [], false)

  | Bound i => (Bound i, [], false)

  | Abs (s, T, body) => 

	  let val (t', asm, rew) = app_rev ctxt i rrls body

	  in (Abs(s, T, t'), asm, rew) end

  | t1 $ t2 => 

    let val (t2', asm2, rew2) = app_rev ctxt i rrls t2

    in

      if rew2 then (t1 $ t2', asm2, true)

      else

        let val (t1', asm1, rew1) = app_rev ctxt i rrls t1

        in if rew1 then (t1' $ t2, asm1, true)

           else (t1 $ t2, [], false)

        end

    end;

(* rewriting without argument [] for rew_ord *)

fun eval_true thy terms rls = (snd o (eval__true thy 1 terms [])) rls;

(* rewriting without internal arguments 1, [] *)

fun rewrite_ thy rew_ord erls bool thm term = rewrite__ thy 1 [] rew_ord erls bool thm term;

fun rewrite_set_ thy bool rls term = rewrite__set_ thy 1 bool [] rls term;

(* variants of rewrite; TODO del. put_asm *)

fun rewrite_inst_  thy rew_ord rls put_asm subst thm ct =

  rewrite__ thy 1 subst rew_ord rls put_asm thm ct;

fun rewrite_set_inst_ thy put_asm subst rls ct = rewrite__set_ thy 1 put_asm subst rls ct;

(* given a list of equalities (lhs = rhs) and a term, 

   replace all occurrences of lhs in the term with rhs;

   thus the order or equalities matters: put variables in lhs first. *)

fun rewrite_terms_ thy ord erls equs t =

  let

	  fun rew_ (t', asm') [] _ = (t', asm')

	    | rew_ (t', asm') (rules as r::rs) t =

	        let

	          val (t'', asm'', _(*lrd*), rew) = rew_sub thy 1 [] ord erls false [] (HOLogic.Trueprop $ r) t

	        in 

	          if rew 

	          then rew_ (t'', asm' @ asm'') rules t''

	          else rew_ (t', asm') rs t'

	        end

	  val (t'', asm'') = rew_ (TermC.empty, []) equs t

    in if t'' = TermC.empty then NONE else SOME (t'', asm'')

    end;

(* search ct for adjacent numerals and calculate them by operator isa_fn *)

fun calculate_ ctxt (isa_fn as (id, eval_fn)) t =

  case Eval.adhoc_thm (Proof_Context.theory_of ctxt) isa_fn t of

	  NONE => NONE

	| SOME (thmID, thm) =>

	  (let val rew = case rewrite_ ctxt Rewrite_Ord.function_empty Rule_Set.empty false thm t of

        SOME (rew, _) => rew

      | NONE => raise ERROR (msg "calculate_" ctxt id thm t)

    in SOME (rew, (thmID, thm)) end)

	    handle NO_REWRITE => raise ERROR ("calculate_: " ^ thmID ^ " does not rewrite");

fun eval_prog_expr thy srls t =

  let val rew = rewrite_set_ thy false srls t;

  in case rew of SOME (res,_) => res | NONE => t end;

fun eval_true_ _ _ (Const (\<^const_name>\<open>True\<close>,_)) = true

  | eval_true_ thy rls t =

    case rewrite_set_ thy false rls t of

	   SOME (Const (\<^const_name>\<open>True\<close>,_),_) => true

	 | _ => false;

end