(* Title:  CalcElements/rule-def.sml

   Author: Walther Neuper

   (c) due to copyright terms

Separate the mutual recursive definition from individual items specified later.

*)

signature RULE_DEFINITION =

  sig

    type calc                                       (*struct:   sig: OK in rule*)

    eqtype calID                                    (*struct:   sig: NOT ok in rule*)

    eqtype errpatID                                 (*struct:   sig: *)

    type rew_ord                                    (*struct:   sig: *)

    type eval_fn                                    (*struct:   sig: OK in rule*)

    val e_evalfn: eval_fn                           (*struct:   sig: (*NOT ok in rule*)*)

    datatype rls                                                                 (*OK*)

      =  Erls

       | Rls of {calc: calc list, erls: rls, errpatts: errpatID list, id: string,

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

       | Seq of {calc: calc list, erls: rls, errpatts: errpatID list, id: string,

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

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

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

    and rule = Cal1 of string * eval_fn | Num_Calc of string * eval_fn | Erule  (*OK*)

       | Rls_ of rls | Thm of string * thm

    and program                                                                 (*OK*)

      =  EmptyScr

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

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

  (*NONE*)

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

  (*NONE*)

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

(*----- unused code, kept as hints to design ideas ---------------------------------------------*)

  end

(**)

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

struct

(**)

type calID = string;

(* eval function calling sml code during rewriting.

Unifying "type cal" and "type calc" would make Lucas-Interpretation more efficient,

  see "fun rule2stac": instead of 

    Num_Calc: calID * eval_fn -> rule

  would be better

    Num_Calc: prog_calcID * (calID * eval_fn)) -> rule*)

type eval_fn = (string -> term -> theory -> (string * term) option);

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

type subst = (term * term) list;

type rew_ord' = string;

type rew_ord_ = subst -> Term.term * Term.term -> bool;

type rew_ord = rew_ord' * rew_ord_;

val e_rew_ord' = "e_rew_ord" : rew_ord';

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

val e_rew_ord_ = dummy_ord;

val e_rew_ord = dummy_ord; (* TODO.WN071231 clarify identifiers..e_rew_ordX*)

val e_rew_ordX = (e_rew_ord', e_rew_ord_);

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

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 (string * Basic_Thm.thm) (* see TODO CLEANUP Thm     *)

  | Num_Calc of string *     (*.sml-code manipulating a (sub)term  .*)

  	  eval_fn

  | Cal1 of string *     (*.sml-code applied only to whole term

                            or left/right-hand-side of eqality .*)

  	  eval_fn

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

and program =

    EmptyScr

  | Prog of term (* a leaf is either a tactic or an 'exp' in 'let v = expr' 

                    where 'exp' does not contain a tactic. *)

  | Rfuns of     (* for Rrls, usage see rational.sml ----- reverse rewrite -----      *)

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

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

      term *          (* the current formula:                                         *)

                      (* goes locate_input_tactic -> find_next_step 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 Num_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:  (* the function which drives the Rrls ##############################*)

	    term -> (term * term list) option,

	  locate_rule:  (* checks a rule R for being a cancel-rule, and if it is,

                     then return the list of rules (+ the terms they are rewriting to)

                     which need to be applied before R should be applied.

                     precondition: the rule is applicable to the argument-term.       *)

	    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; the list is empty,          

                           if the rule has nothing to do with e.g. cancelation        *)

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

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

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

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

		                     there may be no such rule (if the term is eg.canceled already*)

	  attach_form:  (* checks an input term TI, if it may belong to e.g. a current 

                     cancellation, by trying to derive it from the given term TG.     

                     NOT IMPLEMENTED                                                  *)

	    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 the 

                         users term does not belong to e.g. a cancellation of the term 

                         last agreed upon.                                            *)

and rls =

    Erls                          (*for init e_rls*)

  | Rls of (*a confluent and terminating ruleset, in general                         *)

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

     preconds : term list, (*unused WN020820                                         *)

     (*WN060616 for efficiency...                                                    

      bdvs    : false,       (*set in prep_rls' for get_bdvs *)*)                    

     rew_ord  : rew_ord,   (*for rules*)                                             

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

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

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

     rules    : rule list,                                                           

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

     scr      : program}   (*Prog term: generating intermed.steps  *)                

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

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

     preconds : term list, (*unused 20.8.02                                          *)

     (*WN060616 for efficiency...                                                    

      bdvs    : false,       (*set in prep_rls' for get_bdvs *)*)                    

     rew_ord  : rew_ord,   (*for rules                                               *)

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

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

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

     rules    : rule list,

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

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

  (*Rrls call SML-code and simulate an rls

    difference: there is always _ONE_ redex rewritten in 1 call,

    thus wrap Rrls by: Rls (Rls_ ...)*)

  | Rrls of (* SML-functions within rewriting; step-wise execution provided;   

               Rrls simulate an rls

               difference: there is always _ONE_ redex rewritten in 1 call,

               thus wrap Rrls by: Rls (Rls_ ...)                                     *)

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

     prepat  : (term list *(* preconds, eval with subst from pattern;                

                              if [@{term True}], match decides alone                 *)

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

		   list,               (* meta-conjunction is or                                 *)

     rew_ord  : rew_ord,   (* for rules                                              *)

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

     calc     : calc list, (* for Calculate in scr, set automatic.in prep_rls'       *)

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

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

(**)end(**)