(* Title:  CalcElements/rule-set.sml

   Author: Walther Neuper

   (c) due to copyright terms

In ISAC a Rule_Set serves rewriting. KEStore holds all rule-sets for ubiquitous access.

*)

signature RULE_SET =

sig

  datatype T = datatype Rule_Def.rule_set

  eqtype identifier

  val rep: T -> {calc: Rule_Def.calc list, erls: T, errpats: Rule_Def.errpatID list, id: string,

    preconds: term list, rew_ord: Rule_Def.rew_ord, rules: Rule_Def.rule list, scr: Rule_Def.program, srls: T}

  val append_rules: string -> T -> Rule_Def.rule list -> T

  val keep_unique_rules: string -> T ->  Rule_Def.rule list -> T

  val merge: string -> T -> T -> T

  val get_rules: T -> Rule_Def.rule list

  type for_kestore

  val equal: (''a * ('b * 'c)) * (''a * ('d * 'e)) -> bool

  val to_kestore: for_kestore list * for_kestore list -> for_kestore list

(*/------- this will disappear eventually -----------\*)

  val empty: T

  type rrlsstate = term * term * Rule_Def.rule list list * (Rule_Def.rule * (term * term list)) list

  val e_rrlsstate: rrlsstate

  val e_rrls: T

(*\------- this will disappear eventually -----------/*)

(*val id_rls: T -> string*)

(*/------- back to rule.sml -----------------------\*)

  val rls2str: T(*Rule_Def.rule_set*) -> string

  val id_rls: T(*Rule_Def.rule_set*) -> string

  val id_rule: Rule_Def.rule -> string

  val eq_rule: Rule_Def.rule * Rule_Def.rule -> bool

  val rule2str: Rule_Def.rule -> string

  val rule2str': Rule_Def.rule -> string

(*\------- back to rule.sml -----------------------/*)

(*/------- to exec-def.sml ------------------------\*)

  eqtype prog_calcID

  type cal

  type calc_elem

  val calc_eq: calc_elem * calc_elem -> bool

  val e_evalfn: Rule_Def.eval_fn

(*\------- to exec-def.sml ------------------------/*)

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

  (*NONE*)

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

  val insert_merge: for_kestore -> for_kestore list -> for_kestore list

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

end

(**)

structure Rule_Set(**): RULE_SET(**) =

struct

(**)

datatype T = datatype Rule_Def.rule_set

type identifier = string

(*/------- this will disappear eventually ----------------------------------------------------\*)

fun dummy_ord (_: (term * term) list) (_: term, _: term) = true;

val empty =

  Rule_Def.Repeat {id = "empty", preconds = [], rew_ord = ("dummy_ord", dummy_ord), erls = Rule_Def.Empty,

    srls = Rule_Def.Empty, calc = [], rules = [], errpatts = [], scr = Rule_Def.EmptyScr}

(*\------- this will disappear eventually ----------------------------------------------------/*)

fun rep Rule_Def.Empty = rep empty

  | rep (Rule_Def.Repeat {id, preconds, rew_ord, erls, srls, calc, errpatts, rules, scr}) =

    {id = id, preconds = preconds, rew_ord = rew_ord, erls = erls, srls = srls, errpats = errpatts,

      calc = calc, rules = rules, scr = scr}

  | rep (Rule_Def.Seqence {id, preconds, rew_ord, erls, srls, calc, errpatts, rules, scr}) =

    {id = id, preconds = preconds, rew_ord = rew_ord, erls = erls, srls = srls, errpats = errpatts,

      calc = calc, rules = rules, scr = scr}

  | rep (Rule_Def.Rrls _)  = rep empty

fun append_rules id Rule_Def.Empty _ = raise ERROR ("append_rules: with \"" ^ id ^ "\" not for Rule_Def.Empty")

  | append_rules id (Rule_Def.Repeat {id = _, preconds = pc, rew_ord = ro, erls = er, srls = sr, calc = ca,

			rules = rs, errpatts = errpatts, scr = sc}) r =

    Rule_Def.Repeat {id = id, preconds = pc, rew_ord = ro, erls = er, srls = sr, calc = ca,

      rules = rs @ r, errpatts = errpatts, scr = sc}

  | append_rules id (Rule_Def.Seqence {id = _, preconds = pc, rew_ord = ro, erls = er, srls = sr, calc = ca,

			rules = rs, errpatts = errpatts, scr = sc}) r =

    Rule_Def.Seqence {id = id, preconds = pc, rew_ord = ro, erls = er, srls = sr, calc = ca,

      rules = rs @ r, errpatts = errpatts, scr = sc}

  | append_rules id (Rule_Def.Rrls _) _ = raise ERROR ("append_rules: not for reverse-rewrite-rule-set " ^ id);

fun merge_ids rls1 rls2 =

  let 

    val id1 = (#id o rep) rls1

    val id2 = (#id o rep) rls2

  in

    if id1 = id2 then id1 else "merged_" ^ id1 ^ "_" ^ id2

  end

(*/------- to exec-def.sml ------------------------\*)

type prog_calcID = string;

(* op in isa-term "Const(op,_)" *)

type cal = Rule_Def.calID * Rule_Def.eval_fn;

type calc_elem =  (* fun calculate_ fetches the evaluation-function via this list *)

  prog_calcID *   (* a simple identifier used in programs                    *)

  (Rule_Def.calID *        (* a long identifier used in Const                         *)

    Rule_Def.eval_fn)      (* an ML function                                          *)

fun calc_eq ((pi1, (ci1, _)), (pi2, (ci2, _))) =

  if pi1 = pi2

  then if ci1 = ci2 then true else error ("calc_eq: " ^ ci1 ^ " <> " ^ ci2)

  else false

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

(*\------- to exec-def.sml ------------------------/*)

(*val id_rls = Rule.identifier *)

(*/------- back to rule.sml -----------------------\*)

fun id_rls Rule_Def.Empty = "empty" (*WN060714 quick and dirty: recursive defs! TODO "Rule_Def.Empty"*)

  | id_rls (Rule_Def.Repeat {id, ...}) = id

  | id_rls (Rule_Def.Seqence {id, ...}) = id

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

val rls2str = id_rls; (*drop*)

fun id_rule (Rule_Def.Thm (id, _)) = id

  | id_rule (Rule_Def.Num_Calc (id, _)) = id

  | id_rule (Rule_Def.Cal1 (id, _)) = id

  | id_rule (Rule_Def.Rls_ rls) = id_rls rls

  | id_rule Rule_Def.Erule = "Erule";

fun eq_rule (Rule_Def.Thm (thm1, _), Rule_Def.Thm (thm2, _)) = thm1 = thm2

  | eq_rule (Rule_Def.Num_Calc (id1, _), Rule_Def.Num_Calc (id2, _)) = id1 = id2

  | eq_rule (Rule_Def.Rls_ rls1, Rule_Def.Rls_ rls2) = id_rls rls1 = id_rls rls2

  | eq_rule _ = false;

(*\------- back to rule.sml -----------------------/*)

fun merge _ Rule_Def.Empty rls = rls

  | merge _ rls Rule_Def.Empty = rls

  | merge _ (Rrls x) _ = Rrls x (* required for merging Theory_Data *)

  | merge _ _ (Rrls x) = Rrls x

  | merge id

	  (Rule_Def.Repeat {preconds = pc1, rew_ord = ro1, erls = er1, srls = sr1, calc = ca1,

	    rules = rs1, errpatts = eps1, scr = sc1, ...})

	  (Rule_Def.Repeat {preconds = pc2, erls = er2, srls = sr2, calc = ca2,

	    rules = rs2, errpatts = eps2, ...})

    =

	  Rule_Def.Repeat {id = id, rew_ord = ro1, scr = sc1,

	    preconds = union (op =) pc1 pc2,	    

	    erls = merge (merge_ids er1 er2) er1 er2,

	    srls = merge (merge_ids sr1 sr2) sr1 sr2,

	    calc = union calc_eq ca1 ca2,

		  rules = union eq_rule rs1 rs2,

      errpatts = union (op =) eps1 eps2}

  | merge id

	  (Rule_Def.Seqence {preconds = pc1, rew_ord = ro1, erls = er1, srls = sr1, calc = ca1,

	    rules = rs1, errpatts = eps1, scr = sc1, ...})

	  (Rule_Def.Seqence {preconds = pc2, erls = er2, srls = sr2, calc = ca2,

	    rules = rs2, errpatts = eps2, ...})

    =

	  Rule_Def.Seqence {id = id, rew_ord = ro1, scr = sc1,

	    preconds = union (op =) pc1 pc2,	    

	    erls = merge (merge_ids er1 er2) er1 er2,

	    srls = merge (merge_ids sr1 sr2) sr1 sr2,

	    calc = union calc_eq ca1 ca2,

		  rules = union eq_rule rs1 rs2,

      errpatts = union (op =) eps1 eps2}

  | merge id _ _ = error ("merge: \"" ^ id ^ 

    "\"; not for reverse-rewrite-rule-sets and not for mixed Rls -- Rule_Def.Seqence");

(*/------- this will disappear eventually -----------\*)

type rrlsstate =  (* state for reverse rewriting, comments see type rule and scr | Rfuns *)

  (term * term * Rule_Def.rule list list * (Rule_Def.rule * (term * term list)) list);

val e_rrlsstate = (Rule.e_term, Rule.e_term, [[Rule_Def.Erule]], [(Rule_Def.Erule, (Rule.e_term, []))]) : rrlsstate;

local

    fun ii (_: term) = e_rrlsstate;

    fun no (_: term) = SOME (Rule.e_term, [Rule.e_term]);

    fun lo (_: Rule_Def.rule list list) (_: term) (_: Rule_Def.rule) = [(Rule_Def.Erule, (Rule.e_term, [Rule.e_term]))];

    fun ne (_: Rule_Def.rule list list) (_: term) = SOME Rule_Def.Erule;

    fun fo (_: Rule_Def.rule list list) (_: term) (_: term) = [(Rule_Def.Erule, (Rule.e_term, [Rule.e_term]))];

in

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

		  next_rule = ne, attach_form = fo};

end;

val e_rrls =

  Rule_Def.Rrls {id = "e_rrls", prepat = [], rew_ord = ("dummy_ord", dummy_ord), erls = Rule_Def.Empty,

    calc = [], errpatts = [], scr = e_rfuns}

(*\------- this will disappear eventually -----------/*)

(*/------- back to rule.sml -----------------------\*)

fun eq_rule (Rule_Def.Thm (thm1, _), Rule_Def.Thm (thm2, _)) = thm1 = thm2

  | eq_rule (Rule_Def.Num_Calc (id1, _), Rule_Def.Num_Calc (id2, _)) = id1 = id2

  | eq_rule (Rule_Def.Rls_ rls1, Rule_Def.Rls_ rls2) = id_rls rls1 = id_rls rls2

  | eq_rule _ = false;

fun rule2str Rule_Def.Erule = "Erule" 

  | rule2str (Rule_Def.Thm (str, thm)) = "Thm (\"" ^ str ^ "\"," ^ Rule.string_of_thmI thm ^ ")"

  | rule2str (Rule_Def.Num_Calc (str, _)) = "Num_Calc (\"" ^ str ^ "\",fn)"

  | rule2str (Rule_Def.Cal1 (str, _)) = "Cal1 (\"" ^ str ^ "\",fn)"

  | rule2str (Rule_Def.Rls_ rls) = "Rls_ (\"" ^ id_rls rls ^ "\")";

fun rule2str' Rule_Def.Erule = "Erule"

  | rule2str' (Rule_Def.Thm (str, _)) = "Thm (\"" ^ str ^ "\",\"\")"

  | rule2str' (Rule_Def.Num_Calc (str, _)) = "Num_Calc (\"" ^ str ^ "\",fn)"

  | rule2str' (Rule_Def.Cal1 (str, _)) = "Cal1 (\"" ^ str ^ "\",fn)"

  | rule2str' (Rule_Def.Rls_ rls) = "Rls_ (\"" ^ id_rls rls ^ "\")";

(*\------- back to rule.sml -----------------------/*)

(* datastructure for KEStore_Elems, intermediate for thehier *)

type for_kestore = 

  (identifier *     (* identifier unique within Isac *)

  (Rule.theory' *  (* just for assignment in thehier, not appropriate for parsing etc *)

    T))     (* ((#id o rep) T) = identifier   by coding discipline *)

fun equal ((id1, (_, _)), (id2, (_, _))) = id1 = id2

fun insert_merge (re as (id, (thyID, r1))) ys = 

    case get_index (fn y => if curry equal re y then SOME y else NONE) ys of

      NONE => re :: ys

    | SOME (i, (_, (_, r2))) => 

      let

        val r12 = merge id r1 r2

      in list_update ys i (id, (thyID, r12)) end

fun to_kestore (s1, s2) = fold insert_merge s1 s2;

(* used only for one hack *)

fun keep_unique_rules id 

     (Rule_Def.Repeat {id = _, preconds = pc, rew_ord = ro, erls = er, srls = sr, calc = ca,

  		  rules = rs, errpatts = eps, scr = sc}) r =

      Rule_Def.Repeat {id = id, preconds = pc, rew_ord = ro, erls = er, srls = sr, calc = ca,

  	    rules = gen_rems eq_rule (rs, r),

  	    errpatts = eps,

  	    scr = sc}

  | keep_unique_rules id

     (Rule_Def.Seqence {id = _, preconds = pc, rew_ord = ro, erls = er, srls = sr, calc = ca,

  		  rules = rs, errpatts = eps, scr = sc}) r =

      Rule_Def.Seqence {id = id, preconds = pc, rew_ord = ro, erls = er, srls = sr, calc = ca,

  	    rules = gen_rems eq_rule (rs, r),

  	    errpatts = eps,

  	    scr = sc}

  | keep_unique_rules id (Rule_Def.Rrls _) _ = raise ERROR ("keep_unique_rules: not for reverse-rewrite-rule-set "^id)

  | keep_unique_rules _ rls _ = raise ERROR ("remove_rls called with " ^ rls2str rls);

fun get_rules Rule_Def.Empty = []

  | get_rules (Rule_Def.Repeat {rules, ...}) = rules

  | get_rules (Rule_Def.Seqence {rules, ...}) = rules

  | get_rules (Rule_Def.Rrls _) = [];

(**)end(**)