(* data-definitions, which should not occur in code-files to be re-evaluated

   use"definitions.sml";

   *)

type cterm' = string;

val empty_cterm' = "empty_cterm'";

type thmID = string;

type thm' = thmID * cterm';

type rls' = string; 

(*.fun calculate_ fetches the evaluation-function via this list.*)

(*ie. there is NO rewriting involved in contrary to eval_rls*)

type calc =

     (string *     (*op in calculate_ from scripts*)

      (string *    (*op in isa-term 'Const(op,_)' *)

       (string -> term -> theory -> (string * term) option))); (*eval_fun*) 

fun e_evalfn (_:'a) (_:term) (_:theory) = None:(string * term) option;

type subs' = (cterm' * cterm') list; (*16.11.00 for FE-KE*)

type subst = (term * term) list; (*here for ets2str*)

fun subst2str (s:subst) = 

  (strs2str o 

   (map (pair2str o

	 (apsnd (Sign.string_of_term (sign_of thy))) o 

	 (apfst (Sign.string_of_term (sign_of thy)))))) s;

datatype rule = 

  Thm of (string * thm) 

| Calc of string *      (*check for equality*)

	  (string -> term -> theory -> (string * term) option)

| Rls_ of rls         (*.ie. rule sets may be nested.*)

and scr = 

    EmptyScr 

  | Script of term (*for meth'*)

  | Rfuns of {init_state : term -> 

     (term *          (*the current formula: 

                        goes locate_gen -> next_tac via istate*)

      term *          (*the final formula*)

      rule list       (*of reverse rewrite set (#1#)*)

	    list *    (*may be serveral, eg. in norm_rational*)

      (rule *         (*Thm (+ Thm generated from Calc) resulting in ...*)

       (term *        (*... rewrite with ...*)

	term list))   (*... assumptions*)

	  list),      (*derivation from given term to normalform

		       in reverse order with sym_thm; 

                       (#1#) could be extracted from here #1*)

	      normal_form: term -> (term * term list) option,

	      locate_rule: rule list list -> term -> rule 

			   -> (rule * (term * term list)) list,

	      next_rule  : rule list list -> term -> rule option,

	      attach_form: rule list list -> term -> term 

			   -> (rule * (term * term list)) list}

and rls =

    Erls                          (*for init e_rls*)

  | Rls of {id : string, (*for trace_rewrite:=true*)

	    preconds : term list, (*unused 20.8.02*)

	    rew_ord  : string * (subst -> (term * term) -> bool),(*for rules*)

	    erls     : rls,      (*for the conditions in rules*)

	    (*            '^ because of rewrite in applicable_in;

		compare type meth'; FIXXME take name as string into Rls !*)

	    srls     : rls,       (*for evaluation of list_fns in script*)

	    calc     : calc list, (*for Calculate in scr*)

	    asm_thm  : thm' list, (*FIXXME remove with put_asm*)

	    rules    : rule list,

	    scr      : scr}  (*Script term  (how to restrict type ???)*)

  | Seq of {id : string, (*for trace_rewrite:=true*)

	    preconds : term list, (*unused 20.8.02*)

	    rew_ord  : string * (subst -> (term * term) -> bool),(*for rules*)

	    erls     : rls,      (*for the conditions in rules*)

	    (*            '^ because of rewrite in applicable_in;

		compare type meth'; FIXXME take name as string into Rls !*)

	    srls     : rls,       (*for evaluation of list_fns in script*)

	    calc     : calc list, (*for Calculate in scr*)

	    asm_thm  : thm' list, (*FIXXME remove with put_asm*)

	    rules    : rule list,

	    scr      : scr}  (*Script term  (how to restrict type ???)*)

  | Rrls of {id : string, (*for trace_rewrite:=true*)

	     prepat  : (term list *

			          (*preconds, eval with subst from pattern*)

			 term )   (*pattern matched in subterms*)

			    list, (*meta-conjunction is or*)

	     rew_ord  : string * (subst -> (term * term) -> bool),(*for rules*)

	     erls     : rls,      (*for the conditions in rules and pat*)

	     (*            '^ because of rewrite in applicable_in

						       compare type meth'*)

	     calc     : calc list, (*for Calculate in scr*)

	     asm_thm  : thm' list, (*FIXXME remove with put_asm*)

	     scr      : scr}; (*Rfuns {...}  (how to restrict type ???)*)

(*1.8.02 ad (how to restrict type ???): scr should be usable indepentently

  from rls, and then contain both Script _AND_ Rfuns !!!*)

val e_rule = Thm ("refl",refl) : rule;

fun id_of_thm (Thm (id, _)) = id

  | id_of_thm _ = raise error "id_of_thm";

fun thm_of_thm (Thm (_, thm)) = thm

  | thm_of_thm _ = raise error "thm_of_thm";

fun rep_thm_G' (Thm (thmid, thm)) = (thmid, thm);

fun rule2str (Thm (str, thm)) = "Thm (\""^str^"\","^(string_of_thm thm)^")"

  | rule2str (Calc (str,f))  = "Calc (\""^str^"\",fn)"

  | rule2str (Rls_ _) = "Rls_ rls";(*FIXXME*)

fun eqrule (Thm (id1,_), Thm (id2,_)) = id1 = id2

  | eqrule (Calc (id1,_), Calc (id2,_)) = id1 = id2

  | eqrule (Rls_ _, Rls_ _) = false (*{id=id1}{id=id2} = id1 = id2 FIXXME*)

  | eqrule _ = false;

fun memrls r (Rls {rules,...}) = gen_mem eqrule (r, rules)

  | memrls r (Seq {rules,...}) = gen_mem eqrule (r, rules)

  | memrls r _ = raise error ("memrls: incomplete impl. r= "^(rule2str r));

type rrlsstate =      (*state for reverse rewriting*)

     (term *          (*the current formula: 

                        goes locate_gen -> next_tac via istate*)

      term *          (*the final formula*)

      rule list       (*of reverse rewrite set (#1#)*)

	    list *    (*may be serveral, eg. in norm_rational*)

      (rule *         (*Thm (+ Thm generated from Calc) resulting in ...*)

       (term *        (*... rewrite with ...*)

	term list))   (*... assumptions*)

	  list);      (*derivation from given term to normalform

		       in reverse order with sym_thm; 

                       (#1#) could be extracted from here #1*)

val e_type = Type("empty",[]);

val a_type = TFree("'a",[]);

val e_term = Const("empty",e_type);

val a_term = Free("empty",a_type);

val e_rrlsstate = (e_term,e_term,[[e_rule]],[(e_rule,(e_term,[]))]):rrlsstate;

(*22.2.02: ging auf Linux nicht (Stefan)

val e_scr = Script ((term_of o the o (parse thy)) "e_script");*)

val e_term = Const("empty", Type("'a", []));

val e_scr = Script e_term;

(*ad thm':

   there are two kinds of theorems ...

   (1) known by isabelle

   (2) not known, eg. calc_thm, instantiated rls

       the latter have a thmid "#..."

   and thus outside isa we ALWAYS transport both(thmid,string_of_thm)

   and have a special assoc_thm / assoc_rls in this interface      *)

type theory' = string; (* = domID ^".thy" *)

fun string_of_thy thy =  

((last_elem (Sign.stamp_names_of (sign_of thy)))^".thy"):theory';

val theory2domID = string_of_thy;

val theory2theory' = string_of_thy;

type rew_ord' = string;

val theory'  = ref ([]:(theory' * theory) list);

val rew_ord' = ref ([]:(rew_ord' * (subst -> (term * term) -> bool)) list);

val ruleset' = ref ([]:(string * rls) list);

val theorem' = ref ([]:(string * thm) list);

(*val xxx = fn: a b => (a,b);   ??? fun-definition ???*)

local

    fun ii (_:term) = e_rrlsstate;

    fun no (_:term) = Some (e_term,[e_term]);

    fun lo (_:rule list list) (_:term) (_:rule) = [(e_rule,(e_term,[e_term]))];

    fun ne (_:rule list list) (_:term) = Some e_rule;

    fun fo (_:rule list list) (_:term) (_:term) = [(e_rule,(e_term,[e_term]))];

in

val e_rfuns = Rfuns {init_state=ii,normal_form=no,locate_rule=lo,

		     next_rule=ne,attach_form=fo};

end;

fun dummy_ord (_:subst) (_:term,_:term) = true;

val e_rls = 

  Rls{id = "e_rls",

      preconds = [], 

      rew_ord = ("dummy_ord", dummy_ord),

      erls = Erls,srls = Erls,

      calc = [],

      asm_thm = [],

      rules = [], scr = EmptyScr}:rls;

val e_rrls = Rrls {id = "e_rrls",

		   prepat = [],

		   rew_ord = ("dummy_ord", dummy_ord),

		   erls = Erls,

		   calc = [],

		   asm_thm=[],

		   scr=e_rfuns}:rls;

ruleset' := overwritel (!ruleset', [("e_rls",e_rls),

				    ("e_rrls",e_rrls)

				    ]);

fun rep_rls (Rls {id,preconds,rew_ord,erls,srls,calc,asm_thm,rules,scr}) =

  {id=id,preconds=preconds,rew_ord=rew_ord,erls=erls,srls=srls,calc=calc,

   asm_thm=asm_thm,rules=rules,scr=scr}

  | rep_rls (Seq {id,preconds,rew_ord,erls,srls,calc,asm_thm,rules,scr}) =

  {id=id,preconds=preconds,rew_ord=rew_ord,erls=erls,srls=srls,calc=calc,

   asm_thm=asm_thm,rules=rules,scr=scr}

  | rep_rls (Rls {id,...})  = 

    raise error("rep_rls doesn't take apart reverse-rewrite-rule-sets: "^id)

  | rep_rls (Seq {id,...})  = 

    raise error("rep_rls doesn't take apart reverse-rewrite-rule-sets: "^id);

fun rep_rrls 

	(Rrls {id,asm_thm, calc, erls, prepat, rew_ord, 

	       scr=Rfuns

		       {attach_form,init_state,locate_rule,

			next_rule,normal_form}}) =

    {id=id,asm_thm=asm_thm, calc=calc, erls=erls, prepat=prepat, 

     rew_ord=rew_ord, attach_form=attach_form, init_state=init_state, 

     locate_rule=locate_rule, next_rule=next_rule, normal_form=normal_form}

  | rep_rrls (Rls {id,...}) = 

    raise error ("rep_rrls doesn't take apart (normal) rule-sets: "^id)

  | rep_rrls (Seq {id,...}) = 

    raise error ("rep_rrls doesn't take apart (normal) rule-sets: "^id);

(*.id requested for all, Rls,Seq,Rrls.*)

fun id_rls (Rls {id,...}) = id

  | id_rls (Seq {id,...}) = id

  | id_rls (Rrls {id,...}) = id;

fun append_rls id (Rls {id=_,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca,

			asm_thm=at,rules =rs,scr=sc}) r =

    (Rls{id=id,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca,

	 asm_thm=at,rules = rs @ r,scr=sc}:rls)

  | append_rls id (Seq {id=_,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca,

			asm_thm=at,rules =rs,scr=sc}) r =

    (Seq{id=id,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca,

	 asm_thm=at,rules = rs @ r,scr=sc}:rls)

  | append_rls id (Rrls _) _ = raise error 

                   ("append_rls: not for reverse-rewrite-rule-set "^id);

fun eq_rule (Thm thm1, Thm thm2) = thm1 = thm2

  | eq_rule (Calc (id1,_), Calc (id2,_)) = id1 = id2

  | eq_rule _ = false;

fun merge_rls _ Erls rls = rls

  | merge_rls _ rls Erls = rls

  | merge_rls id

	(Rls {id=id1,preconds=pc1,rew_ord=ro1,erls=er1,srls=sr1,calc=ca1,

	      asm_thm=at1,rules =rs1,scr=sc1}) 

	r2 =

	(Rls {id=id,preconds=pc1 @ ((#preconds o rep_rls) r2),

	      rew_ord=ro1,erls=(*merge_rls er1 er2*)er1,

	      srls=merge_rls ("merged_"^id1^"_"^((#id o rep_rls) r2)) sr1 

			     ((#srls o rep_rls) r2),

	      calc=ca1 @ ((#calc o rep_rls) r2),

	      asm_thm=at1 @ ((#asm_thm o rep_rls) r2),

	      rules = gen_union eq_rule rule2str (rs1, (#rules o rep_rls) r2),

	      scr=sc1}:rls)

  | merge_rls id 

	(Seq {id=id1,preconds=pc1,rew_ord=ro1,erls=er1,srls=sr1,calc=ca1,

	      asm_thm=at1,rules =rs1,scr=sc1}) 

	r2 =

	(Seq {id=id,preconds=pc1 @ ((#preconds o rep_rls) r2),

	      rew_ord=ro1,erls=(*merge_rls er1 er2*)er1,

	      srls=merge_rls ("merged_"^id1^"_"^((#id o rep_rls) r2)) sr1 

			     ((#srls o rep_rls) r2),

	      calc=ca1 @ ((#calc o rep_rls) r2),

	      asm_thm=at1 @ ((#asm_thm o rep_rls) r2),

	      rules = gen_union eq_rule rule2str (rs1, (#rules o rep_rls) r2),

	      scr=sc1}:rls)

  | merge_rls _ _ _ = raise error 

				"merge_rls: not for reverse-rewrite-rule-sets";

fun remove_rls id (Rls {id=_,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca,

		     asm_thm=at,rules =rs,scr=sc}) r =

    (Rls{id=id,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca,

	 asm_thm=at,rules = gen_rems eq_rule (rs, r),

	 scr=sc}:rls)

  | remove_rls id (Seq {id=_,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca,

		     asm_thm=at,rules =rs,scr=sc}) r =

    (Seq{id=id,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca,

	 asm_thm=at,rules = gen_rems eq_rule (rs, r),

	 scr=sc}:rls)

  | remove_rls id (Rrls _) _ = raise error 

                   ("remove_rls: not for reverse-rewrite-rule-set "^id);

 gen_rems (op=) ([1,2,3], [3,4,5]);

fun assoc' ([], key) = raise error ("ME_Isa: '"^key^"' not known")

  | assoc' ((keyi, xi) :: pairs, key) =

      if key = keyi then Some xi else assoc' (pairs, key);

fun assoc_thy (thy:theory') = ((the o assoc')(!theory',thy))

  handle _ => raise error ("ME_Isa: '"^thy^"' not in system");

fun assoc_rls (rls:rls') = ((the o assoc')(!ruleset',rls))

  handle _ => raise error ("ME_Isa: '"^rls^"' not in system");

fun termopt2str (Some t) = 

    "Some " ^ (Sign.string_of_term (sign_of(assoc_thy "Isac.thy")) t)

  | termopt2str None = "None";

fun term2str t = Sign.string_of_term (sign_of(assoc_thy "Isac.thy")) t;

(*for tests only*)

fun terms2str ts= (strs2str o (map (Sign.string_of_term 

					(sign_of (assoc_thy "Isac.thy"))))) ts;

(*recursive defs:*)

fun scr2str (Script s) = "Script "^(term2str s)

  | scr2str (Rfuns _)  = "Rfuns";

type domID = string;   (* domID ^"thy" = theory' ??check 3.00!!*)

val e_domID = "e_domID":domID;

type pblID = string list; (* domID::...*)

val e_pblID = ["e_pblID"]:pblID;

type metID = (domID * string);

val e_metID = (e_domID,"e_metID"):metID;

fun metID2str ((domID,mI):metID) = pair2str (domID,mI);