(* Title:  BaseDefinitions/eval-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 Eval.

*)

signature EVALUATE__DEFINITION =

sig

  eqtype calID

  eqtype prog_calcID

  type cal

  type calc_elem

  val calc_eq: calc_elem * calc_elem -> bool

  type eval_fn = Rule_Def.eval_fn

  val e_evalfn: Rule_Def.eval_fn

  val set_data: eval_fn -> theory -> theory

  val the_data: theory -> eval_fn

end

(**)

structure Eval_Def(**): EVALUATE__DEFINITION(**) =

struct

(**)

type calID = Rule_Def.calID

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 raise ERROR ("calc_eq: " ^ ci1 ^ " <> " ^ ci2)

  else false

(* eval function calling sml code during rewriting.

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

  see "fun rule2stac": instead of 

    Eval: calID * eval_fn -> rule

  would be better

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

type eval_fn = Rule_Def.eval_fn

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

(* theory data for Isar command 'calculation' *)

structure Data = Theory_Data

(

  type T = eval_fn option;

  val empty = NONE;

  val extend = I;

  fun merge _ = NONE;

);

val set_data = Data.put o SOME;

val the_data = the o Data.get;

end