(* isac's rewriter

   (c) Walther Neuper 2000

*)

signature REWRITE =

  sig

    val assoc_thm': theory -> thm' -> thm

    val assoc_thm'': theory -> thmID -> thm

    val calculate_: theory -> string * eval_fn -> term -> (term * (string * thm)) option

    val eval__true: theory -> int -> term list -> (term * term) list -> rls -> term list * bool

    val eval_listexpr_: theory -> rls -> term -> term

    val eval_true: theory -> term list -> rls -> bool

    val eval_true_: theory' -> rls -> term -> bool

    val rew_sub: theory -> int -> (term * term) list -> ((term * term) list -> term * term -> bool) -> rls -> bool -> lrd list -> term -> term -> term * term list * lrd list * bool

    val rewrite_: theory -> ((term * term) list -> term * term -> bool) -> rls -> bool -> thm -> term -> (term * term list) option

    val rewrite_inst_: theory -> ((term * term) list -> term * term -> bool) -> rls -> bool -> (term * term) list -> thm -> term -> (term * term list) option

    val rewrite_set_: theory -> bool -> rls -> term -> (term * term list) option

    val rewrite_set_inst_: theory -> bool -> (term * term) list -> rls -> term -> (term * term list) option

    val rewrite_terms_: theory -> ((term * term) list -> term * term -> bool) -> rls -> term list -> term -> (term * term list) option

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

  (* NONE *)

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

    val rewrite__: theory -> int -> (term * term) list -> ((term * term) list -> term * term -> bool) -> rls -> bool -> thm -> term -> (term * term list) option

    val rewrite__set_: theory -> int -> bool -> (term * term) list -> rls -> term -> (term * term list) option

    val app_rev: theory -> int -> rls -> term -> term * term list * bool

    val app_sub: theory -> int -> rls -> term -> term * term list * bool

    val mk_thm: theory -> string -> thm

    val trace1: int -> string -> unit

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

  end

(**)

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

struct

(**)

exception NO_REWRITE;

exception STOP_REW_SUB; (*WN050820 quick and dirty*)

fun trace i str = 

  if ! trace_rewrite andalso i < ! depth then tracing (idt "#" i ^ str) else ()

fun trace1 i str = 

  if ! trace_rewrite andalso i < ! depth then tracing (idt "#" (i + 1) ^ str) else ()

fun rewrite__ thy i bdv tless rls put_asm thm ct =

  let

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

		  (((TermC.inst_bdv bdv) o Calc.norm o #prop o Thm.rep_thm) thm) ct

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

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

and rew_sub thy 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

    (*?alternative Unify.matchers:

      http://isabelle.in.tum.de/repos/isabelle/file/Isabelle2017/src/Pure/more_unify.ML*)

    val r' = Envir.subst_term (Pattern.match thy (lhs, t) (Vartab.empty, Vartab.empty)) r

    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 _ = if ! trace_rewrite andalso i < ! depth andalso p' <> []

	    then tracing (idt "#" (i + 1) ^ " eval asms: " ^ t2str thy r') else ()

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

      let

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

	    in

	      if nofalse

        then

          (if ! trace_rewrite andalso i < ! depth andalso p' <> []

          then tracing (idt "#" (i + 1) ^ " asms accepted: " ^ ts2str thy p' ^

  	        "   stored: " ^ ts2str thy simpl_p')

  	      else();

          (t',simpl_p'))                                               (* uncond.rew. from above*)

        else 

          (if ! trace_rewrite andalso i < ! depth 

          then tracing (idt "#" (i + 1) ^ " asms false: " ^ ts2str thy p')

          else();

          raise STOP_REW_SUB (* don't go into subterms of cond *))

	    end

    in

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

      then (if ! trace_rewrite andalso i < ! depth 

  	    then tracing (idt"#"i ^ " not: \"" ^ t2str thy t ^ "\" > \"" ^ t2str thy t' ^ "\"")

  	    else (); 

  	    raise NO_REWRITE)

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

    end

    ) handle _ (*TODO Pattern.MATCH when tests are ready: ERROR 364ce4699452 *) => 

      (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 thy i bdv tless rls put_asm (lrd @ [D]) r body

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

      | t1 $ t2 => 

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

    	   in

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

    	    else

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

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

  end)

and eval__true thy i asms bdv rls =         (* simplify 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_ thy (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_ thy _ __ Erls t =                                  (* rewrite with a rule set *)

    error ("rewrite__set_ called with 'Erls' for '" ^ t2str thy t ^ "'")

  | rewrite__set_ thy i _ _ (rrls as Rrls _) t =           (* rewrite with a 'reverse rule set' *)

    let

      val _= trace i (" rls: " ^ id_rls rrls ^ " on: " ^ t2str thy t)

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

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

  | rewrite__set_ thy i put_asm bdv rls ct =          (* Rls, Seq containing Thms or Calc, Cal1 *)

    let

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

      datatype switch = Appl | Noap;

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

        | rew_once ruls asm ct Appl [] = 

          (case rls of Rls _ => rew_once ruls asm ct Noap ruls

          | Seq _ => (ct, asm)

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

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

          case rul of

            Thm (thmid, thm) =>

              (trace1 i (" try thm: " ^ thmid);

              case rewrite__ thy (i + 1) bdv ((snd o #rew_ord o rep_rls) rls)

                  ((#erls o rep_rls) rls) put_asm thm ct of

                NONE => rew_once ruls asm ct apno thms

              | SOME (ct', asm') => 

                (trace1 i (" rewrites to: " ^ t2str thy ct');

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

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

          | Calc (cc as (op_, _)) => 

            let val _= trace1 i (" try calc: " ^ op_ ^ "'")

              val ct = TermC.uminus_to_string ct

            in case Calc.adhoc_thm thy cc ct of

                NONE => rew_once ruls asm ct apno thms

              | SOME (_, thm') => 

                let 

                  val pairopt = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o rep_rls) rls)

                    ((#erls o rep_rls) rls) put_asm thm' ct;

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

                    string_of_thmI thm' ^ "\" " ^ t2str thy ct ^ " = NONE")

                  val _ = trace1 i (" calc. to: " ^ t2str thy ((fst o the) pairopt))

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

            end

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

            let val _= trace1 i (" try cal1: " ^ op_ ^ "'");

              val ct = TermC.uminus_to_string ct

            in case Calc.adhoc_thm1_ thy cc ct of

                NONE => (ct, asm)

              | SOME (_, thm') =>

                let 

                  val pairopt = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o rep_rls) rls)

                    ((#erls o rep_rls) rls) put_asm thm' ct;

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

                     string_of_thmI thm' ^ "\" " ^ t2str thy ct ^ " = NONE")

                  val _ = trace1 i (" cal1. to: " ^ t2str thy ((fst o the) pairopt))

                in the pairopt end

            end

          | Rls_ rls' => 

            (case rewrite__set_ thy (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 \"" ^ rule2str r ^ "\"");

      val ruls = (#rules o rep_rls) rls;

      val _ = trace i (" rls: " ^ id_rls rls ^ " on: " ^ t2str thy ct)

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

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

and app_rev thy 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 thy erls prepat t =

        let

          fun chk (pres, pat) =

            (let 

              val subst: Type.tyenv * Envir.tenv =

                Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty)

             in

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

             end) handle _ (*TODO 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' thy (Rrls {erls, prepat, scr = Rfuns {normal_form, ...}, ...}) t =

      if chk_prepat thy erls prepat t then normal_form t else NONE

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

    val opt = app_rev' thy rrls t

  in

    case opt of

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

    | NONE => app_sub thy i rrls t

  end

and app_sub thy 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 thy i rrls body

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

  | t1 $ t2 => 

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

    in

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

      else

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

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

           else (t1 $ t2, [], false)

        end

    end;

(* rewriting without argument [] for rew_ord;  WN110603: shouldnt asm<>[] lead to false? *)

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

(* rewriting without internal argument [] *)

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_ (e_term, []) equs t

    in if t'' = e_term then NONE else SOME (t'', asm'')

    end;

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

fun calculate_ thy isa_fn ct =

  let val ct = TermC.uminus_to_string ct

    in case Calc.adhoc_thm thy isa_fn ct of

	   NONE => NONE

	 | SOME (thmID, thm) =>

	   (let val rew = case rewrite_ thy dummy_ord e_rls false thm ct of

         SOME (rew, _) => rew

       | NONE => raise ERROR ""

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

	   handle _ (*TODO Pattern.MATCH ?del?*)=> error ("calculate_: " ^ thmID ^ " does not rewrite")

  end;

(* Thm.make_thm added to Pure/thm.ML *)

fun mk_thm thy str = 

  let

    val t = (Thm.term_of o the o (TermC.parse thy)) str

    val t' = case t of

        Const ("Pure.imp", _) $ _ $ _ => t

      | _ => HOLogic.Trueprop $ t

  in Thm.make_thm (Thm.global_cterm_of thy t') end;

(* "metaview" as seen from programs and from user input (both are parsed like terms presently) *)

fun convert_metaview_to_thmid thy thmid =

  let val thmid' = case thmid of

      "add_commute" => "add.commute"

    | "mult_commute" => "mult.commute"

    | "add_left_commute" => "add.left_commute"

    | "mult_left_commute" => "mult.left_commute"

    | "add_assoc" => "add.assoc"

    | "mult_assoc" => "mult.assoc"

    | _ => thmid

  in (Global_Theory.get_thm thy) thmid' end;

(* get the theorem associated with the xstring-identifier;

   if the identifier starts with "sym_" then swap lhs = rhs around =

   (ATTENTION: "RS sym" attaches a [.] -- remove it with string_of_thmI);

   identifiers starting with "#" come from Calc and

   get a hand-made theorem (containing numerals only) *)

fun assoc_thm'' thy thmid =

  case Symbol.explode thmid of

    "s"::"y"::"m"::"_"::"#"::_ => error ("assoc_thm'' not impl.for " ^ thmid)

  | "s"::"y"::"m"::"_"::id => ((TermC.num_str o (Global_Theory.get_thm thy)) (implode id)) RS sym

  | "#"::_ => error ("assoc_thm'' not impl.for " ^ thmid)

  | _ => thmid |> convert_metaview_to_thmid thy |> TermC.num_str

fun assoc_thm' thy (thmid, ct') =

  (case Symbol.explode thmid of

    "s"::"y"::"m"::"_"::id => 

      if hd id = "#" 

      then mk_thm thy ct'

      else ((TermC.num_str o (Global_Theory.get_thm thy)) (implode id)) RS sym

  | id =>

    if hd id = "#" 

    then mk_thm thy ct'

    else thmid |> convert_metaview_to_thmid thy |> TermC.num_str

  ) handle _ (*TODO: find exn behind ERROR: Undefined fact: "add_commute"*) => 

    error ("assoc_thm': \"" ^ thmid ^ "\" not in \"" ^ theory2domID thy ^ "\" (and parents)")

fun eval_listexpr_ 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 ("HOL.True",_)) = true

  | eval_true_ (thy':theory') rls t =

    case rewrite_set_ (assoc_thy thy') false rls t of

	   SOME (Const ("HOL.True",_),_) => true

	 | _ => false;

end