(* isac's rewriter

    (c) Walther Neuper 2000

 *)

 signature REWRITE =

   sig

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

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

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

     val eval__true: theory -> int -> term list -> (term * term) list -> Rule_Set.T -> term list * bool

     val eval_prog_expr: theory -> Rule_Set.T -> term -> term

     val eval_true_: theory -> Rule_Set.T -> term -> bool

     val eval_true: theory -> term list -> Rule_Set.T -> bool

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

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

     val rewrite_: theory -> ((term * term) list -> term * term -> bool) -> Rule_Set.T -> bool -> thm ->

       term -> (term * term list) option

     val rewrite_inst_: theory -> ((term * term) list -> term * term -> bool) -> Rule_Set.T -> bool

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

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

     val rewrite_set_inst_: theory -> bool -> (term * term) list -> Rule_Set.T -> term -> (term * term list) option

     val rewrite_terms_: theory -> ((term * term) list -> term * term -> bool) -> Rule_Set.T -> 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) ->

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

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

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

     val app_sub: theory -> int -> Rule_Set.T -> 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 ! Celem.trace_rewrite andalso i < ! Celem.depth then tracing (idt "#" i ^ str) else ()

 fun trace1 i str = 

   if ! Celem.trace_rewrite andalso i < ! Celem.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*)]: TermC.path)

 		  (((TermC.inst_bdv bdv) o Num_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 ! Celem.trace_rewrite andalso i < ! Celem.depth andalso p' <> []

 	    then tracing (idt "#" (i + 1) ^ " eval asms: " ^ UnparseC.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 ! Celem.trace_rewrite andalso i < ! Celem.depth andalso p' <> []

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

   	        "   stored: " ^ UnparseC.ts2str thy simpl_p')

   	      else();

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

         else 

           (if ! Celem.trace_rewrite andalso i < ! Celem.depth 

           then tracing (idt "#" (i + 1) ^ " asms false: " ^ UnparseC.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 ! Celem.trace_rewrite andalso i < ! Celem.depth 

   	    then tracing (idt"#"i ^ " not: \"" ^ UnparseC.t2str thy t ^ "\" > \"" ^ UnparseC.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 @ [TermC.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 @ [TermC.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 @ [TermC.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 _ __ Rule_Set.Empty t =                             (* rewrite with a rule set *)

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

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

     let

       val _= trace i (" rls: " ^ Rule_Set.rls2str rrls ^ " on: " ^ UnparseC.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 Num_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 Prog_Expr.rew_once? *)

         | rew_once ruls asm ct Appl [] = 

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

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

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

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

           case rul of

             Rule.Thm (thmid, thm) =>

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

               case rewrite__ thy (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') => 

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

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

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

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

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

               val ct = TermC.uminus_to_string ct (*WN190312: superfluous?*)

             in case Num_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 Rule_Set.rep) rls)

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

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

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

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

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

             end

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

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

               val ct = TermC.uminus_to_string ct

             in case Num_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 Rule_Set.rep) rls)

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

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

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

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

                 in the pairopt end

             end

           | Rule.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 \"" ^ Rule.rule2str r ^ "\"");

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

       val _ = trace i (" rls: " ^ Rule_Set.rls2str rls ^ " on: " ^ UnparseC.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 (Rule_Set.Rrls {erls, prepat, scr = Rule.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 \"" ^ Rule_Set.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_ (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_ thy isa_fn ct =

   let val ct = TermC.uminus_to_string ct

     in case Num_Calc.adhoc_thm thy isa_fn ct of

 	   NONE => NONE

 	 | SOME (thmID, thm) =>

 	   (let val rew = case rewrite_ thy Rewrite_Ord.dummy_ord Rule_Set.empty 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 ThmC.string_of_thmI);

    identifiers starting with "#" come from Num_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 \"" ^ ThyC.theory2domID thy ^ "\" (and parents)")

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

   | eval_true_ thy rls t =

     case rewrite_set_ thy false rls t of

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

 	 | _ => false;

 end