(* Title:  BaseDefinitions/rule.sml

   Author: Walther Neuper 2018

   (c) copyright due to lincense terms

TODO: use "Rule" for renaming identifiers.

Some stuff waits for later rounds of restructuring, e.g. TermC.empty

*)

signature RULE =

sig

  datatype rule = datatype Rule_Def.rule

  datatype program = datatype Rule_Def.program

  val set_id: Rule_Def.rule_set -> string

  val id: rule -> string

  val equal: rule * rule -> bool

  val to_string: Proof.context -> rule -> string

  val to_string_short: rule -> string

  val s_to_string: rule list -> string

  val thm: Proof.context -> rule -> thm

  val distinct' : rule list -> rule list

  val thm_id: rule -> string

  val eval: Proof.context -> rule -> string * Rule_Def.eval_fn

  val rls: Proof.context -> rule -> Rule_Def.rule_set

  val make_eval: string -> Rule_Def.eval_fn -> rule

end

(**)

structure Rule(**): RULE(**) =

struct

(**)

datatype rule = datatype Rule_Def.rule;

datatype program = datatype Rule_Def.program;

type is_as_string = string;

type calc = Rule_Def.eval_ml_from_prog

type calID = Rule_Def.eval_const_id;

type eval_fn = Rule_Def.eval_fn;

fun set_id Rule_Def.Empty = "empty"

  | set_id (Rule_Def.Repeat {id, ...}) = id

  | set_id (Rule_Def.Sequence {id, ...}) = id

  | set_id (Rule_Def.Rrls {id, ...}) = id;

fun id (Rule_Def.Thm (id, _)) = id

  | id (Rule_Def.Eval (id, _)) = id

  | id (Rule_Def.Cal1 (id, _)) = id

  | id (Rule_Def.Rls_ rls) = set_id rls

  | id Rule_Def.Erule = "Erule";

fun equal (Rule_Def.Thm (thm1, _), Rule_Def.Thm (thm2, _)) = thm1 = thm2

  | equal (Rule_Def.Eval (id1, _), Rule_Def.Eval (id2, _)) = id1 = id2

  | equal (Rule_Def.Rls_ rls1, Rule_Def.Rls_ rls2) = set_id rls1 = set_id rls2

  | equal _ = false;

fun distinct' rs = distinct equal rs

fun to_string _ Rule_Def.Erule = "Erule" 

  | to_string ctxt (Rule_Def.Thm (str, thm)) =

    "Thm (\"" ^ str ^ "\", " ^ ThmC_Def.string_of_thm_PIDE ctxt thm ^ ")"

  | to_string _ (Rule_Def.Eval (str, _)) = "Eval (\"" ^ str ^ "\",fn)"

  | to_string _ (Rule_Def.Cal1 (str, _)) = "Cal1 (\"" ^ str ^ "\",fn)"

  | to_string _ (Rule_Def.Rls_ rls) = "Rls_ (\"" ^ set_id rls ^ "\")";

fun to_string_short Rule_Def.Erule = "Erule"

  | to_string_short (Rule_Def.Thm (str, _)) = "Thm (\"" ^ str ^ "\",\"\")"

  | to_string_short (Rule_Def.Eval (str, _)) = "Eval (\"" ^ str ^ "\",fn)"

  | to_string_short (Rule_Def.Cal1 (str, _)) = "Cal1 (\"" ^ str ^ "\",fn)"

  | to_string_short (Rule_Def.Rls_ rls) = "Rls_ (\"" ^ set_id rls ^ "\")";

fun s_to_string rules = rules |> map to_string_short |> commas |> enclose "[" "]" 

fun thm_id (Rule_Def.Thm (id, _)) = id

  | thm_id _ = raise ERROR ("Rule.thm_id: uncovered case " (* ^ to_string r *))

fun thm _ (Rule_Def.Thm (_, thm)) = thm

  | thm ctxt r = raise ERROR ("Rule.thm: uncovered case " ^ to_string ctxt r)

fun eval _ (Eval e) = e

  | eval ctxt r = raise ERROR ("Rule.eval NOT FOR " ^ to_string ctxt r)

fun rls _ (Rls_ rls) = rls

  | rls ctxt r = raise ERROR ("Rule.rls NOT FOR " ^ to_string ctxt r) 

(* ML antiquotations *)

val make_eval = curry Eval;

val _ = Theory.setup

  (ML_Antiquotation.value_embedded \<^binding>\<open>rule_eval\<close>

    (Args.const {proper = true, strict = true} >>

      (fn name => "Rule.make_eval " ^ ML_Syntax.print_string name)));

(**)end(**)