(* Title:  BaseDefinitions/rule-set.sml

   Author: Walther Neuper

   (c) due to copyright terms

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

*)                                       

signature RULE_SET =

sig

  datatype T = datatype Rule_Def.rule_set

  eqtype id

  val id: T -> string

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

    preconds: term list, rew_ord: Rewrite_Ord.T, rules: Rule_Def.rule list, program: Rule_Def.program, prog_rls: T}

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

  val append_erls_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

  val id_from_rule: Proof.context -> Rule.rule -> string

  val contains: Rule.rule -> T -> bool

(*type for_know_store*)

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

(*from isac_test for Minisubpbl*)

  val to_string_test: Proof.context -> T -> string

\<^isac_test>\<open>

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

\<close>

end

(**)

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

struct

(**)

datatype T = datatype Rule_Def.rule_set;

type id = string;

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

val dummy_ord = Rewrite_Ord.function_empty;

val empty =

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

    prog_rls = Rule_Def.Empty, calc = [], rules = [], errpatts = [], program = Rule_Def.Empty_Prog}

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

val id = Rule.set_id;

fun rep Rule_Def.Empty = rep empty

  | rep (Rule_Def.Repeat {id, preconds, rew_ord, asm_rls, prog_rls, calc, errpatts, rules, program}) =

    {id = id, preconds = preconds, rew_ord = rew_ord, asm_rls = asm_rls, prog_rls = prog_rls, errpats = errpatts,

      calc = calc, rules = rules, program = program}

  | rep (Rule_Def.Sequence {id, preconds, rew_ord, asm_rls, prog_rls, calc, errpatts, rules, program}) =

    {id = id, preconds = preconds, rew_ord = rew_ord, asm_rls = asm_rls, prog_rls = prog_rls, errpats = errpatts,

      calc = calc, rules = rules, program = program}

  | rep (Rule_Def.Rrls _)  = rep empty

fun to_string_test _ Rule_Def.Empty = "Rule_Set.Empty"

  | to_string_test ctxt (Rule_Def.Repeat {id, preconds, rew_ord, asm_rls = _, prog_rls = _, calc = _, errpatts = _, rules, program}) =

    "(Rule_Def.Repeat {id = " ^ id ^ ", preconds = " ^ UnparseC.terms_in_ctxt ctxt preconds ^ ", rew_ord = " ^ Rewrite_Ord.to_string rew_ord

    ^ ",\n  asm_rls = _, prog_rls = _, calc = _, errpatts = _, "

    ^ ",\n  rules = " ^ Rule.s_to_string rules

    ^ ",\n  rules = " ^ Rule_Def.program_to_string program ^ "})"

  | to_string_test ctxt (Rule_Def.Sequence {id, preconds, rew_ord, asm_rls = _, prog_rls = _, calc = _, errpatts = _, rules, program}) =

    "(Rule_Def.Repeat {id = " ^ id ^ ", preconds = " ^ UnparseC.terms_in_ctxt ctxt preconds ^ ", rew_ord = " ^ Rewrite_Ord.to_string rew_ord

    ^ ",\n  asm_rls = _, prog_rls = _, calc = _, errpatts = _, "

    ^ ",\n  rules = " ^ Rule.s_to_string rules

    ^ ",\n  rules = " ^ Rule_Def.program_to_string program ^ "})"

  | to_string_test _ (Rule_Def.Rrls _)  = "Rule_Def.Rrls _"

fun append_rules id Rule_Def.Empty r = (*.. required for append_erls_rules *)

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

      prog_rls = Rule_Def.Empty, calc = [], rules = r, errpatts = [], program = Rule_Def.Empty_Prog}

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

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

    Rule_Def.Repeat {id = id, preconds = pc, rew_ord = ro, asm_rls = er, prog_rls = sr, calc = ca,

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

  | append_rules id (Rule_Def.Sequence {id = _, preconds = pc, rew_ord = ro, asm_rls = er, prog_rls = sr, calc = ca,

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

    Rule_Def.Sequence {id = id, preconds = pc, rew_ord = ro, asm_rls = er, prog_rls = sr, calc = ca,

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

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

fun append_erls_rules id_erls Rule_Def.Empty _ =

    raise ERROR ("append_erls_rules: with \"" ^ id_erls ^ "\" not for Rule_Def.Empty")

  | append_erls_rules id_erls (Rule_Def.Repeat 

    {id = id, preconds = pc, rew_ord = ro, asm_rls = asm_rls, prog_rls = sr, calc = ca,

			rules = rules, errpatts = errpatts, program = sc}) rs =

    Rule_Def.Repeat {id = id, preconds = pc, rew_ord = ro, asm_rls = append_rules id_erls asm_rls rs, 

      prog_rls = sr, calc = ca, rules = rules, errpatts = errpatts, program = sc}

  | append_erls_rules id_erls (Rule_Def.Sequence

    {id = id, preconds = pc, rew_ord = ro, asm_rls = asm_rls, prog_rls = sr, calc = ca,

			rules = rules, errpatts = errpatts, program = sc}) rs =

    Rule_Def.Sequence {id = id, preconds = pc, rew_ord = ro, asm_rls = append_rules id_erls asm_rls rs,

      prog_rls = sr, calc = ca, rules = rules, errpatts = errpatts, program = sc}

  | append_erls_rules id_erls (Rule_Def.Rrls _) _ =

    raise ERROR ("append_erls_rules: not for reverse-rewrite-rule-set " ^ id_erls);

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

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, asm_rls = er1, prog_rls = sr1, calc = ca1,

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

	  (Rule_Def.Repeat {preconds = pc2, asm_rls = er2, prog_rls = sr2, calc = ca2,

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

    =

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

	    preconds = union (op =) pc1 pc2,	    

	    asm_rls = merge (merge_ids er1 er2) er1 er2,

	    prog_rls = merge (merge_ids sr1 sr2) sr1 sr2,

	    calc = union Eval_Def.equal ca1 ca2,

		  rules = union Rule.equal rs1 rs2,

      errpatts = union (op =) eps1 eps2}

  | merge id

	  (Rule_Def.Sequence {preconds = pc1, rew_ord = ro1, asm_rls = er1, prog_rls = sr1, calc = ca1,

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

	  (Rule_Def.Sequence {preconds = pc2, asm_rls = er2, prog_rls = sr2, calc = ca2,

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

    =

	  Rule_Def.Sequence {id = id, rew_ord = ro1, program = sc1,

	    preconds = union (op =) pc1 pc2,	    

	    asm_rls = merge (merge_ids er1 er2) er1 er2,

	    prog_rls = merge (merge_ids sr1 sr2) sr1 sr2,

	    calc = union Eval_Def.equal ca1 ca2,

		  rules = union Rule.equal rs1 rs2,

      errpatts = union (op =) eps1 eps2}

  | merge id _ _ = raise ERROR ("merge: \"" ^ id ^ 

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

(* datastructure for Know_Store, intermediate for thehier *)

type for_kestore = 

  (id *     (* id unique within Isac *)

  (ThyC.id *  (* just for assignment in thehier, not appropriate for parsing etc *)

    T))     (* ((#id o rep) T) = id   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, asm_rls = er, prog_rls = sr, calc = ca,

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

      Rule_Def.Repeat {id = id, preconds = pc, rew_ord = ro, asm_rls = er, prog_rls = sr, calc = ca,

  	    rules = gen_rems Rule.equal (rs, r),

  	    errpatts = eps,

  	    program = sc}

  | keep_unique_rules id

     (Rule_Def.Sequence {id = _, preconds = pc, rew_ord = ro, asm_rls = er, prog_rls = sr, calc = ca,

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

      Rule_Def.Sequence {id = id, preconds = pc, rew_ord = ro, asm_rls = er, prog_rls = sr, calc = ca,

  	    rules = gen_rems Rule.equal (rs, r),

  	    errpatts = eps,

  	    program = 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 " ^ id rls);

fun get_rules Rule_Def.Empty = []

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

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

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

fun id_from_rule _ (Rule.Rls_ rls) = id rls

  | id_from_rule ctxt r =

    raise ERROR ("id_from_rule: not defined for " ^ Rule.to_string ctxt r);

(* check if a rule is contained in a rule-set (recursivley down in Rls_);

   this rule can even be a rule-set itself                             *)

fun contains r rls = 

  let 

    fun (*find (_, Rls_ rls) = finds (get_rules rls)

      | find r12 = equal r12

    and*) finds [] = false

    | finds (r1 :: rs) = if Rule.equal (r, r1) then true else finds rs

  in 

    finds (get_rules rls) 

  end

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

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

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

val e_rrlsstate = (UnparseC.term_empty, UnparseC.term_empty, [[Rule_Def.Erule]], [(Rule_Def.Erule, (UnparseC.term_empty, []))]) : rrlsstate;

local           

    fun ii (_: term) = e_rrlsstate;

    fun no (_: term) = SOME (UnparseC.term_empty, [UnparseC.term_empty]);

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

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

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

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), asm_rls = Rule_Def.Empty,

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

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

(**)end(**)