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

  (* NONE *)

(* probably shift up ---------------

    exception NO_REWRITE

    exception STOP_REW_SUB

    val adhoc_thm': theory' -> string * eval_fn -> cterm' -> thm' option

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

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

    val calculate: theory' -> string * eval_fn -> cterm' -> (string * thm') option

    val convert: 'a -> string -> string

    val convert_metaview_to_thmid: theory -> string -> thm

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

    val get_rls_scr: rls' -> scr

    val mk_thm: theory -> string -> thm

    val mk_thm'': theory -> term -> thm

    val parse': theory' -> cterm' -> cterm' option

    val rewrite: theory' -> rew_ord' -> rls' -> bool -> thm' -> cterm' -> (string * string) option

    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 rewrite_inst: theory' -> rew_ord' -> rls' -> bool -> 'a -> thm' -> cterm' -> (cterm' * cterm' list) option

    val rewrite_set: theory' -> bool -> rls' -> cterm' -> (string * string) option

    val rewrite_set_inst: theory' -> bool -> subs' -> rls' -> cterm' -> (string * string) option

    val subs'2subst: theory -> subs' -> subst

    val trace: int -> string -> unit

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

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

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

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: " ^ term2str 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: " ^ terms2str p' ^

  	        "   stored: " ^ terms2str simpl_p')

  	      else();

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

        else 

          (if ! trace_rewrite andalso i < ! depth 

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

          else();

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

	    end

    in

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

      then (if ! trace_rewrite andalso i < ! depth 

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

  	    else (); 

  	    raise NO_REWRITE)

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

    end

    ) handle Pattern.MATCH (*TODO Pattern.MATCH when tests are ready *) => 

      (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_ _ _ __ Erls t =                                    (* rewrite with a rule set *)

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

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

    let

      val _= trace i (" rls: " ^ id_rls rrls ^ " on: " ^ term2str 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 =        (* rule set containing Thms or Calculations *)

    let

      datatype switch = Appl | Noap;

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

        | 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: " ^ term2str ct');

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

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

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

              val ct = uminus_to_string ct

            in case 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' ^ "\" " ^ term2str ct ^ " = NONE")

                  val _ = trace1 i (" calc. to: " ^ term2str ((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 = uminus_to_string ct

            in case 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' ^ "\" " ^ term2str ct ^ " = NONE")

                  val _ = trace1 i (" cal1. to: " ^ term2str ((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: " ^ term2str 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 [] (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 = uminus_to_string ct

    in case 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 (parse thy)) str

	val t' = case t of

		     Const ("==>",_) $ _ $ _ => t

		   | _ => 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 => ((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 |> 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 ((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 |> 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