(* Title:  BaseDefinitions/rule-def.sml

   Author: Walther Neuper

   (c) due to copyright terms

Here is a minimum of code required for Know_Store.thy.

For main code see structure Rule.

*)

signature RULE_DEFINITION =

sig

  type calc

  eqtype calID

  eqtype errpatID

  type rew_ord_id = string

  type rew_ord_function = LibraryC.subst -> term * term -> bool

  type rew_ord_T = rew_ord_id * rew_ord_function

  type eval_fn = string -> term -> Proof.context -> (string * term) option

  datatype rule_set =

       Empty

     | Repeat of {calc: calc list, erls: rule_set, errpatts: errpatID list, id: string,

       preconds: term list, rew_ord: rew_ord_T, rules: rule list, scr: program, srls: rule_set}

     | Sequence of {calc: calc list, erls: rule_set, errpatts: errpatID list, id: string,

       preconds: term list, rew_ord: rew_ord_T, rules: rule list, scr: program, srls: rule_set}

     | Rrls of {calc: calc list, erls: rule_set, errpatts: errpatID list, id: string,

       prepat: (term list * term) list, rew_ord: rew_ord_T, scr: program}

  and rule = Cal1 of string * eval_fn | Eval of string * eval_fn | Erule

     | Rls_ of rule_set | Thm of string * thm

  and program =

       Empty_Prog

     | Prog of term

     | Rfuns of

         {attach_form: rule list list -> term -> term -> (rule * (term * term list)) list,

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

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

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

          (term * term list) option}

  val program_to_string: program -> string

end

(**)

structure Rule_Def(**): RULE_DEFINITION(**) =

struct

(**)

type eval_fn = string -> term -> Proof.context -> (string * term) option;

type rew_ord_id = string;

type rew_ord_function = LibraryC.subst -> term * term -> bool;

type rew_ord_T = rew_ord_id * rew_ord_function;

type calID = string;

type cal = calID * eval_fn;

type prog_calcID = string;

type calc = (prog_calcID * cal);

(* error patterns and fill patterns *)

type errpatID = string

(* all these different data justify a step in a calculation *)

datatype rule =

    Erule             (* the empty rule                                               *)

  | Thm of            (* theorem associated with the identifier for reflection        *)

      string *        (* required for ThmC.sym_thm                                    *)

        Thm.thm       (* see TODO CLEANUP Thm                                         *)

  | Eval of           (* evaluation by rewriting                                      *)

      string *        (* unique identifier for the evaluation function                *)

  	    eval_fn       (* evaluation function in ML code                               *)

  | Cal1 of string *  (* applied once to whole term or lhs/rhs of an eqality          *)

  	  eval_fn         (* evaluation function in ML code                               *)

  | Rls_ of rule_set  (* rule sets may be nested                                      *)

and program =         (* program for Lucas-Interpretation                             *)

    Empty_Prog        (* DEPRECATED: needless after removal of Rfuns                  *)

  | Prog of term      (* Lucas-Interpretation works on Isabelle's terms               *)

  | Rfuns of          (* DEPRECATED, replaced by Auto_Prog                            *)

    {init_state :     (* initialise for reverse rewriting by the Interpreter          *)

      term ->         (* for this the rrlsstate is initialised:                       *)

      term *          (* the current formula 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 Eval) resulting in ...         *)

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

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

      list,           (* derivation from given term to normalform in reverse order    *)  

	  normal_form:      (* the function which drives the Rrls                           *)

	    term -> (term * term list) option,

	  locate_rule:      (* checks a rule R for being a cancel-rule                      *)

	    rule list list -> (* the reverse rule list                                      *)

	    term ->         (* ... to which the rule shall be applied                       *)

	    rule ->         (* ... to be applied to term                                    *)

	    ( rule *        (* value: a rule rewriting to ...                               *)

	      (term *       (*   ... the resulting term ...                                 *)

	      term list))   (*   ... with the assumptions ( //#0)                           *)

	    list,           (*   there may be several such rules                            *)

	  next_rule:        (* for a given term return the next rules to be done for cancel *)

	    rule list list->(* the reverse rule list                                        *)

	    term ->         (* the term for which ...                                       *)

	    rule option,    (* ... this rule is appropriate for cancellation                *)

	  attach_form:      (* checks an input term TI, if it may belong to a current cancel*)

	    rule list list->

	    term ->         (* TG, the last one agreed upon by user + math-eng              *)

	    term ->         (* TI, the next one input by the user                           *)

	    ( rule *        (* the rule to be applied in order to reach TI                  *) 

	      (term *       (* ... obtained by applying the rule ...                        *)

	      term list))   (* ... and the respective assumptions                           *) 

	    list}           (* there may be several such rules; the list is empty, if ...   *)

and rule_set =        (* a collection for ordered & conditional rewriting             *)

    Empty             (* empty Rule_Set.T                                             *)

  | Repeat of         (*a confluent and terminating ruleset, in principle             *)

    {id: string,      (* for trace_rewrite                                            *)

     preconds: term list, (* STILL UNUSED                                             *)

     rew_ord: rew_ord_T,(* for rules                                                  *)                                             

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

     srls: rule_set,  (* for evaluation of Prog_Expr                                  *)

     calc: calc list, (* for Calculate in program, set by prep_rls'                   *)

     rules: rule list,

     errpatts: errpatID list,(* by dialog-authoring in Build_Thydata.thy              *)

     scr: program}    (* DEPRECATED: intersteps are created on the fly now            *)

  | Sequence of       (* a sequence of rules to be tried only once                    *)

    {id: string, preconds: term list, rew_ord: rew_ord_T, erls: rule_set, srls: rule_set,

     calc: calc list, rules: rule list, errpatts: errpatID list, scr: program}

  | Rrls of           (* ML-functions within rewriting, _ONE_ redex rewritten per call*)

    {id: string,      (* for trace_rewrite                                            *)

     prepat:          (* a guard which guarantees a redex                             *)

       (term list *   (* preconds, eval with subst from pattern below                 *)

		     term)        (* pattern matched with current (sub)term                       *)

		   list,          (* meta-conjunction in guarding is or                           *)

     rew_ord: rew_ord_T, erls: rule_set, calc: calc list, errpatts: errpatID list, scr: program}

fun program_to_string Empty_Prog = "Empty_Prog"

  | program_to_string (Prog s) = "Prog " ^ UnparseC.term s

  | program_to_string (Rfuns _)  = "Rfuns";

(**)end(**)