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

(* 

Synopsis rewriting (prep for reference manual):

----------------------------------------------

Rewriting uses theorems for transforming terms. However, not all kinds

of such transformations can be done by rewriting. Examples are

calculation with numerals or cancellation of fractions. 

Isac tries to present transformations like calculations or cancellation 

as simple rewrite steps for the naive user. However, some of such

transformations should be transparent to the user by single-stepping.

For instance, cancellation involves interesting CA algorithms like 

GCD of multivariate polynomials.

Thus Isac has two mechanisms for including SML code, "thm Calc" and "Rrls",

the former for steps which are not meant to be inspected by single-stepping

the latter meant for single-stepping and providing respective mechanisms.

(1) Inclusion by "thm Calc" for 1-step execution

TODO

(2) Inclusion by "Rrls" for multi-step execution

TODO

In multi-step execution "reverse rewriting" worked only as passive presentation

without any interaction. So the functions init_state, locate_rule etc are just dummies.

TODO

? multi-step execution did never work.

what worked is "reverse rewriting", 

i.e. presentation of intermediate steps *without* interaction

TODO

# type rule and scr | Rfuns

# type rrlsstate = (*state for reverse rewriting*) 

# type and rls | Rrls

all in calcelems.sml

TODO

*)

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)

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

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

  ((*tracing ("@@@ rew_sub begin: t = "^(term2str t));

   tracing ("@@@ rew_sub begin: bdv = "^(@{make_string} bdv));

   tracing ("@@@ rew_sub begin: r = "^(term2str r));*)

    let                  (* copy from Pure/thm.ML: fun rewritec *)

     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 _= tracing("@@@ rew_sub match: t'= "^(term2str t'));*)

     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 (*dont 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 ((*tracing("##@ rew_sub: (t''= "^(term2str t'')^

		      ", p'' ="^(terms2str p'')^", true)");*)

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

   end

   ) handle _ (*NO_REWRITE WN050820 causes diff.behav. in tests + MATCH!*) => 

     ((*tracing ("@@@ rew_sub gosub: t = "^(term2str t));*)

      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)

(* simplify asumptions until one evaluates to false, store intermined's (x~=0)*)

and eval__true thy i asms bdv rls =

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

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

  else 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

(* rewrite with a rule set, which must not be the empty Erls *)

and rewrite__set_ _ _ __ Erls t = 

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

  (* rewrite with a 'reverse rule set' implemented by ML code *)

  | rewrite__set_ thy i _ _ (rrls as Rrls _) t =

    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 with a rule set containing Thms or Calculations *)

  | rewrite__set_ thy i put_asm bdv rls ct =

    let

      datatype switch = Appl | Noap;

      fun rew_once ruls asm ct Noap [] = (ct, asm) (* unify with version in rewtools.sml *)

        | rew_once ruls asm ct Appl [] = 

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

          | Seq _ => (ct, asm))

        | 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 (thmid, 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 (thmid, 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);

      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

(* apply an Rrls; if not applicable proceed with subterms *)

and app_rev thy i rrls t = 

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

    fun chk_prepat thy erls [] t = 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 _ => false

           fun scan_ f [] = false (*scan_ NEVER called by []*)

             | 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;

    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

(* apply an Rrls to subterms *)

and app_sub thy i rrls t =

  ((*tracing("### app_sub: subterm = "^(term2str t));*)

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

(*WN.11.6.03: 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;

fun subs'2subst thy (s:subs') = 

    (((map (apfst (Thm.term_of o the o (parse thy)))) 

     o (map (apsnd (Thm.term_of o the o (parse thy))))) s):subst;

(*.variants of rewrite.*)

(*FIXME 12.8.02: put_asm = true <==> rewrite_inst,

  thus the argument put_asm  IS NOT NECESSARY -- FIXME*)

(* val (rew_ord,rls,put_asm,thm,ct)=

       (e_rew_ord,poly_erls,false,num_str d1_isolate_add2,t);

   *)

fun rewrite_inst_ (thy:theory) rew_ord (rls:rls) (put_asm:bool) 

		  (subst:(term * term) list) (thm:thm) (ct:term) =

    rewrite__ thy 1 subst rew_ord rls put_asm thm ct;

fun rewrite_set_inst_ (thy:theory) 

  (put_asm:bool) (subst:(term * term) list) (rls:rls) (ct:term) =

  (*let 

    val subst = subs'2subst thy subs';

    val subrls = instantiate_rls subs' rls

  in*) rewrite__set_ thy 1 put_asm subst (*sub*)rls ct

  (*end*);

(* 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 SOME (rew,_) = rewrite_ thy dummy_ord e_rls false thm ct

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

	   handle _ => error ("calculate_: "^thmID^" does not rewrite")

  end;

(*

> val thy = InsSort.thy;

> val op_ = "le";      (* < *)

> val ct = (the o (parse thy)) 

   "foldr ins [#2] (if #1 < #3 then #1 # ins [] #3 else [#3, #1])";

> calculate_ thy op_ ct;

  SOME

    ("foldr ins [#2] (if True then #1 # ins [] #3 else [#3, #1])",

     "(#1 < #3) = True") : (cterm * thm) option  *)

fun get_rls_scr rls' = ((#scr o rep_rls o assoc_rls) rls')

  handle _ => error ("get_rls_scr: no script for " ^ rls');

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

fun mk_thm'' thy t = 

    let val t' = case t of

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

		   | _ => Trueprop $ t

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

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;

(*

  val str = "?r ^^^ 2 = ?r * ?r";

  val thm = realpow_twoI;

  val t1 = (#prop o rep_thm) (num_str thm);

  val t2 = Trueprop $ ((Thm.term_of o the o (parse thy)) str);

  t1 = t2;

val it = true : bool      ... !!!

  val th1 = (num_str thm);

  val th2 = ((*num_str*) (mk_thm thy str)) handle e => print_exn e;

  th1 = th2;

ML> val it = false : bool ... HIDDEN DIFFERENCES IRRELEVANT FOR ISAC ?!

~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

  val str = "k ~= 0 ==> m * k / (n * k) = m / n";

  val thm = real_mult_div_cancel2;

  val t1 = (#prop o rep_thm) (num_str thm);

  val t2 = ((Thm.term_of o the o (parse thy)) str);

  t1 = t2;

val it = false : bool     ... Var .. Free

  val th1 = (num_str thm);

  val th2 = ((*num_str*) (mk_thm thy str)) handle e => print_exn e;

  th1 = th2;

ML> val it = false : bool ... PLUS HIDDEN DIFFERENCES IRRELEVANT FOR ISAC ?!

*)

(*prints subgoal etc. 

((goal thy);(topthm()) o ) str;                      *)

(*assume rejects scheme variables 

  assume ((Thm.global_cterm_of thy) (Trueprop $ 

		(Thm.term_of o the o (parse thy)) str)); *)

(* outcommented 18.11.xx, xx < 02 -------

fun rul2rul' (Thm (thmid, thm)) = Thm'(thmid, string_of_thmI thm)

  | rul2rul' (Calc op_)         = Calc' op_;

fun rul'2rul thy (Thm'(thmid, ct')) = 

       Thm (thmid, mk_thm thy ct')

  | rul'2rul thy' (Calc' op_)        = Calc op_;

fun rls2rls' (Rls{preconds=preconds,rew_ord=rew_ord,rules=rules}:rls) =

  Rls'{preconds'= map string_of_cterm preconds,

       rew_ord' = fst rew_ord,

       rules'   = map rul2rul' rules}:rlsdat';

fun rls'2rls thy' (Rls'{preconds'=preconds,rew_ord'=rew_ord,

		   rules'=rules}:rlsdat') =

  let val thy = assoc_thy thy';

  in Rls{preconds = map (the o (parse thy)) preconds,

	 rew_ord  = (rew_ord, the (assoc'(rew_ord',rew_ord))),

	 rules    = map (rul'2rul thy) rules}:rls 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;

(* FIXME: the other direction below is probably concerned with this fun:

thmID_of_derivation_name' @{thm add.assoc} = "assoc"    TODO: repair this fun *);

fun convert thmid_to_metaview 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;

(*.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 : theory) (thmid : 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:theory) ((thmid, ct'):thm') =

  (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: fin exn behind ERROR: Undefined fact: "add_commute"*) => 

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

fun parse' (thy:theory') (ct:cterm') =

    case parse (assoc_thy thy) ct of

	NONE => NONE

      | SOME ct => SOME ((term2str (Thm.term_of ct)):cterm');

(*FIXME 12.8.02: put_asm = true <==> rewrite_inst, rewrite_set_inst

  thus the argument put_asm  IS NOT NECESSARY -- FIXME        ~~~~~*)

fun rewrite (thy':theory') (rew_ord:rew_ord') (rls:rls') (put_asm:bool) (thm:thm') (ct:cterm') =

  let val thy = assoc_thy thy';

  in

    case rewrite_ thy ((the o assoc')(!rew_ord',rew_ord))(assoc_rls rls)

      put_asm ((assoc_thm' thy) thm) ((Thm.term_of o the o (parse thy)) ct) of

      NONE => NONE

    | SOME (t, ts) => SOME (term2str t, terms2str ts)

  end;

(*FIXME 12.8.02: put_asm = true <==> rewrite_inst, rewrite_set_inst

  thus the argument put_asm  IS NOT NECESSARY -- FIXME        ~~~~~*)

fun rewrite_set (thy':theory') (put_asm:bool) (rls:rls') (ct:cterm') =

  let val thy = (assoc_thy thy');

  in

    case rewrite_set_ thy put_asm (assoc_rls rls) ((Thm.term_of o the o (parse thy)) ct) of

      NONE => NONE

    | SOME (t, ts) => SOME (term2str t, terms2str ts)

  end;

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 adhoc_thm' (thy:theory') op_ (ct:cterm') =

   case adhoc_thm (assoc_thy thy) op_

    ((uminus_to_string o Thm.term_of o the o 

      (parse (assoc_thy thy))) ct) of

	NONE => NONE

      | SOME (thmid, thm) => 

	    SOME ((thmid, string_of_thmI thm):thm');

fun calculate (thy':theory') op_ (ct:cterm') =

    let val thy = (assoc_thy thy');

    in

	case calculate_ thy op_

			((Thm.term_of o the o (parse thy)) ct) of

	    NONE => NONE

	  | SOME (ct,(thmID,thm)) => 

	    SOME (term2str ct, 

		  (thmID, string_of_thmI thm):thm')

    end;

(*FIXME 12.8.02: put_asm = true <==> rewrite_inst, rewrite_set_inst

  thus the argument put_asm  IS NOT NECESSARY -- FIXME        ~~~~~*)

fun rewrite_inst (thy':theory') (rew_ord:rew_ord') (rls:rls') 

  (put_asm:bool) subs (thm:thm') (ct:cterm') =

  let

    val thy = assoc_thy thy';

    val thm = assoc_thm' thy thm; (*28.10.02*)

    (*val subthm = read_instantiate subs ((assoc_thm' thy) thm)*)

  in

    case rewrite_ thy

      ((the o assoc')(!rew_ord',rew_ord)) (assoc_rls rls)

      put_asm (*sub*)thm ((Thm.term_of o the o (parse thy)) ct) of

      NONE => NONE

    | SOME (ctm, ctms) => 

      SOME ((term2str ctm):cterm', (map term2str ctms):cterm' list)

  end;

(*FIXME 12.8.02: put_asm = true <==> rewrite_inst, rewrite_set_inst

  thus the argument put_asm  IS NOT NECESSARY -- FIXME        ~~~~~*)

fun rewrite_set_inst (thy':theory') (put_asm:bool)

  subs' (rls:rls') (ct:cterm') =

  let

    val thy = assoc_thy thy';

    val rls = assoc_rls rls

    val subst = subs'2subst thy subs'

  in case rewrite_set_inst_ thy put_asm subst (*sub*)rls

			    ((Thm.term_of o the o (parse thy)) ct) of

	 NONE => NONE

       | SOME (t, ts) => SOME (term2str t, terms2str ts)

  end;

(*vor check_elementwise: SqRoot_eval_rls .. wie *_simplify ?! TODO *)

fun eval_true' (thy':theory') (rls':rls') (Const ("HOL.True",_)) = true

  | eval_true' (thy':theory') (rls':rls') (t:term) =

(* val thy'="Isac"; val rls'="eval_rls"; val t=hd pres';

   *)

    let val ct' = term2str t;

    in case rewrite_set thy' false rls' ct' of

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

	 | _ => false 

    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;

(*

val test_rls = 

  Rls{preconds = [], rew_ord = ("sqrt_right",sqrt_right), 

      rules = [Calc ("matches",eval_matches "")

	       ],

      scr = Prog ((Thm.term_of o the o (parse thy)) 

      "empty_script")

      }:rls;      

  rewrite_set_ (Thy_Info_get_theory "Isac") eval_rls false test_rls 

        ((the o (parse thy)) "matches (?a = ?b) (x = #0)");

  val xxx = (Thm.term_of o the o (parse thy)) 

	       "matches (?a = ?b) (x = #0)";

  eval_matches """" xxx thy;

SOME ("matches (?a = ?b) (x + #1 + #-1 * #2 = #0) = True",

     Const ("HOL.Trueprop","bool => prop") $ (Const # $ (# $ #) $ Const (#,#)))

  rewrite_set_ (Thy_Info_get_theory "Isac") eval_rls false eval_rls 

        ((the o (parse thy)) "contains_root (sqrt #0)");

val it = SOME ("HOL.True",[]) : (cterm * cterm list) option

*)

(*----------WN:16.5.03 stuff below considered illdesigned, thus coded from scratch in appl.sml fun check_elementwise

datatype det = TRUE  | FALSE | INDET;(*FIXXME.WN:16.5.03

				     introduced with quick-and-dirty code*)

fun determine dts =

    let val false_indet = 

	    filter_out ((curry op= TRUE) o (#1:det * term -> det)) dts

        val ts = map (#2: det * term -> term) dts

    in if nil = false_indet then (TRUE, ts)

       else if nil = filter ((curry op= FALSE) o (#1:det * term -> det))

			    false_indet

       then (INDET, ts)

       else (FALSE, ts) end;

(* val dts = [(INDET,e_term), (FALSE,@{term False}), 

	      (INDET,e_term), (TRUE,@{term True})];

  determine dts;

val it =

  (FALSE,

   [Const ("empty","'a"),Const ("HOL.False","bool"),Const ("empty","'a"),

    Const ("HOL.True","bool")]) : det * term list*)

fun eval__indet_ thy cs rls = (*FIXXME.WN:16.5.03 pull into eval__true_, update check (check_elementwise), and regard eval_true_ + eval_true*)

if cs = [@{term True}] orelse cs = [] then (TRUE, [])

    else if cs = [@{term False}] then (FALSE, cs)

    else

	let fun eval t = 

		let val taopt = rewrite__set_ thy 1 false [] rls t

		in case taopt of

		       SOME (t,_) =>

		       if t = @{term True} then (TRUE, t)

		       else if t = @{term False} then (FALSE, t)

		       else (INDET, t)

		     | NONE => (INDET, t) end

	in (determine o (map eval)) cs end;

WN.16.5.0-------------------------------------------------------------*)

end