(* Title:  Interpret/lucas-interpreter.sml

   Author: Walther Neuper 2019

   (c) due to copyright terms

*)

signature METHOD =

sig

  type T = Meth_Def.T

  val empty: T

  type id = Meth_Def.id

  val id_empty: id

  val id_to_string: id -> string

  val from_store: id -> T

  val from_store': theory -> id -> T

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

end

(**)

structure Method(**): METHOD(**) =

struct

(**)

type T = Meth_Def.T;

val empty = Meth_Def.empty;

type id = Meth_Def.id;

val id_empty = Meth_Def.id_empty;

val id_to_string = Meth_Def.id_to_string;

(* TODO: throws exn 'get_pbt not found: ' ... confusing !! take 'ketype' as an argument *)

fun from_store metID = Store.get (get_mets ()) metID metID;

fun from_store' thy metID = Store.get (KEStore_Elems.get_mets thy) metID metID;

(**)end(**)