1 (* Title: BaseDefinitions/rule.sml
2 Author: Walther Neuper 2018
3 (c) copyright due to lincense terms
5 TODO: use "Rule" for renaming identifiers.
6 Some stuff waits for later rounds of restructuring, e.g. TermC.empty
11 datatype rule = datatype Rule_Def.rule
12 datatype program = datatype Rule_Def.program
14 val set_id: Rule_Def.rule_set -> string
15 val id: rule -> string
16 val equal: rule * rule -> bool
17 val to_string: Proof.context -> rule -> string
18 val to_string_short: rule -> string
19 val s_to_string: rule list -> string
21 val thm: Proof.context -> rule -> thm
22 val distinct' : rule list -> rule list
24 val thm_id: rule -> string
25 val eval: Proof.context -> rule -> string * Rule_Def.eval_fn
26 val rls: Proof.context -> rule -> Rule_Def.rule_set
28 val make_eval: string -> Rule_Def.eval_fn -> rule
32 structure Rule(**): RULE(**) =
36 datatype rule = datatype Rule_Def.rule;
37 datatype program = datatype Rule_Def.program;
38 type is_as_string = string;
40 type calc = Rule_Def.eval_ml_from_prog
41 type calID = Rule_Def.eval_const_id;
42 type eval_fn = Rule_Def.eval_fn;
44 fun set_id Rule_Def.Empty = "empty"
45 | set_id (Rule_Def.Repeat {id, ...}) = id
46 | set_id (Rule_Def.Sequence {id, ...}) = id
47 | set_id (Rule_Def.Rrls {id, ...}) = id;
49 fun id (Rule_Def.Thm (id, _)) = id
50 | id (Rule_Def.Eval (id, _)) = id
51 | id (Rule_Def.Cal1 (id, _)) = id
52 | id (Rule_Def.Rls_ rls) = set_id rls
53 | id Rule_Def.Erule = "Erule";
54 fun equal (Rule_Def.Thm (thm1, _), Rule_Def.Thm (thm2, _)) = thm1 = thm2
55 | equal (Rule_Def.Eval (id1, _), Rule_Def.Eval (id2, _)) = id1 = id2
56 | equal (Rule_Def.Rls_ rls1, Rule_Def.Rls_ rls2) = set_id rls1 = set_id rls2
58 fun distinct' rs = distinct equal rs
60 fun to_string _ Rule_Def.Erule = "Erule"
61 | to_string ctxt (Rule_Def.Thm (str, thm)) =
62 "Thm (\"" ^ str ^ "\", " ^ ThmC_Def.string_of_thm ctxt thm ^ ")"
63 | to_string _ (Rule_Def.Eval (str, _)) = "Eval (\"" ^ str ^ "\",fn)"
64 | to_string _ (Rule_Def.Cal1 (str, _)) = "Cal1 (\"" ^ str ^ "\",fn)"
65 | to_string _ (Rule_Def.Rls_ rls) = "Rls_ (\"" ^ set_id rls ^ "\")";
66 fun to_string_short Rule_Def.Erule = "Erule"
67 | to_string_short (Rule_Def.Thm (str, _)) = "Thm (\"" ^ str ^ "\",\"\")"
68 | to_string_short (Rule_Def.Eval (str, _)) = "Eval (\"" ^ str ^ "\",fn)"
69 | to_string_short (Rule_Def.Cal1 (str, _)) = "Cal1 (\"" ^ str ^ "\",fn)"
70 | to_string_short (Rule_Def.Rls_ rls) = "Rls_ (\"" ^ set_id rls ^ "\")";
71 fun s_to_string rules = rules |> map to_string_short |> commas |> enclose "[" "]"
73 fun thm_id (Rule_Def.Thm (id, _)) = id
74 | thm_id _ = raise ERROR ("Rule.thm_id: uncovered case " (* ^ to_string r *))
75 fun thm _ (Rule_Def.Thm (_, thm)) = thm
76 | thm ctxt r = raise ERROR ("Rule.thm: uncovered case " ^ to_string ctxt r)
78 fun eval _ (Eval e) = e
79 | eval ctxt r = raise ERROR ("Rule.eval NOT FOR " ^ to_string ctxt r)
80 fun rls _ (Rls_ rls) = rls
81 | rls ctxt r = raise ERROR ("Rule.rls NOT FOR " ^ to_string ctxt r)
84 (* ML antiquotations *)
86 val make_eval = curry Eval;
89 (ML_Antiquotation.value_embedded \<^binding>\<open>rule_eval\<close>
90 (Args.const {proper = true, strict = true} >>
91 (fn name => "Rule.make_eval " ^ ML_Syntax.print_string name)));