1.1 --- a/src/Tools/isac/Build_Isac.thy Wed Apr 08 12:32:51 2020 +0200
1.2 +++ b/src/Tools/isac/Build_Isac.thy Wed Apr 08 13:21:19 2020 +0200
1.3 @@ -16,6 +16,7 @@
1.4 (* theory KEStore imports Complex_Main
1.5 ML_file libraryC.sml
1.6 ML_file "rule-def.sml"
1.7 + ML_file "exec-def.sml"
1.8 ML_file rule.sml
1.9 ML_file "rule-set.sml"
1.10 ML_file calcelems.sml
2.1 --- a/src/Tools/isac/CalcElements/KEStore.thy Wed Apr 08 12:32:51 2020 +0200
2.2 +++ b/src/Tools/isac/CalcElements/KEStore.thy Wed Apr 08 13:21:19 2020 +0200
2.3 @@ -7,6 +7,7 @@
2.4 begin
2.5 ML_file libraryC.sml
2.6 ML_file "rule-def.sml"
2.7 +ML_file "exec-def.sml"
2.8 ML_file rule.sml
2.9 ML_file "rule-set.sml"
2.10 ML_file calcelems.sml
2.11 @@ -33,8 +34,8 @@
2.12 sig
2.13 val get_rlss: theory -> (Rule_Set.identifier * (Rule.theory' * Rule_Set.T)) list
2.14 val add_rlss: (Rule_Set.identifier * (Rule.theory' * Rule_Set.T)) list -> theory -> theory
2.15 - val get_calcs: theory -> (Rule_Set.prog_calcID * (Rule.calID * Rule.eval_fn)) list
2.16 - val add_calcs: (Rule_Set.prog_calcID * (Rule.calID * Rule.eval_fn)) list -> theory -> theory
2.17 + val get_calcs: theory -> (Exec_Def.prog_calcID * (Rule.calID * Rule.eval_fn)) list
2.18 + val add_calcs: (Exec_Def.prog_calcID * (Rule.calID * Rule.eval_fn)) list -> theory -> theory
2.19 val get_cas: theory -> Celem.cas_elem list
2.20 val add_cas: Celem.cas_elem list -> theory -> theory
2.21 val get_ptyps: theory -> Celem.ptyps
2.22 @@ -62,13 +63,13 @@
2.23 fun add_rlss rlss = Data.map (union_overwrite Rule_Set.equal rlss)
2.24
2.25 structure Data = Theory_Data (
2.26 - type T = (Rule_Set.prog_calcID * (Rule.calID * Rule.eval_fn)) list;
2.27 + type T = (Exec_Def.prog_calcID * (Rule.calID * Rule.eval_fn)) list;
2.28 val empty = [];
2.29 val extend = I;
2.30 - val merge = merge Rule_Set.calc_eq;
2.31 + val merge = merge Exec_Def.calc_eq;
2.32 );
2.33 fun get_calcs thy = Data.get thy
2.34 - fun add_calcs calcs = Data.map (union_overwrite Rule_Set.calc_eq calcs)
2.35 + fun add_calcs calcs = Data.map (union_overwrite Exec_Def.calc_eq calcs)
2.36
2.37 structure Data = Theory_Data (
2.38 type T = (term * (Celem.spec * (term list -> (term * term list) list))) list;
3.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
3.2 +++ b/src/Tools/isac/CalcElements/exec-def.sml Wed Apr 08 13:21:19 2020 +0200
3.3 @@ -0,0 +1,33 @@
3.4 +(* Title: CalcElements/exec-def.sml
3.5 + Author: Walther Neuper
3.6 + (c) due to copyright terms
3.7 +
3.8 +TODO: use "Exec_Def" for renaming identifiers
3.9 +*)
3.10 +signature EXECUTE_DEFINITION =
3.11 +sig
3.12 + eqtype prog_calcID
3.13 + type cal
3.14 + type calc_elem
3.15 + val calc_eq: calc_elem * calc_elem -> bool
3.16 + val e_evalfn: Rule_Def.eval_fn
3.17 +end
3.18 +
3.19 +(**)
3.20 +structure Exec_Def(**): EXECUTE_DEFINITION(**) =
3.21 +struct
3.22 +(**)
3.23 +
3.24 +type prog_calcID = string;
3.25 +(* op in isa-term "Const(op,_)" *)
3.26 +type cal = Rule_Def.calID * Rule_Def.eval_fn;
3.27 +type calc_elem = (* fun calculate_ fetches the evaluation-function via this list *)
3.28 + prog_calcID * (* a simple identifier used in programs *)
3.29 + (Rule_Def.calID * (* a long identifier used in Const *)
3.30 + Rule_Def.eval_fn) (* an ML function *)
3.31 +fun calc_eq ((pi1, (ci1, _)), (pi2, (ci2, _))) =
3.32 + if pi1 = pi2
3.33 + then if ci1 = ci2 then true else error ("calc_eq: " ^ ci1 ^ " <> " ^ ci2)
3.34 + else false
3.35 +fun e_evalfn (_ : 'a) (_ : term) (_ : theory) = NONE : (string * term) option;
3.36 +end
4.1 --- a/src/Tools/isac/CalcElements/rule-set.sml Wed Apr 08 12:32:51 2020 +0200
4.2 +++ b/src/Tools/isac/CalcElements/rule-set.sml Wed Apr 08 13:21:19 2020 +0200
4.3 @@ -39,14 +39,6 @@
4.4 val rule2str': Rule_Def.rule -> string
4.5 (*\------- back to rule.sml -----------------------/*)
4.6
4.7 -(*/------- to exec-def.sml ------------------------\*)
4.8 - eqtype prog_calcID
4.9 - type cal
4.10 - type calc_elem
4.11 - val calc_eq: calc_elem * calc_elem -> bool
4.12 - val e_evalfn: Rule_Def.eval_fn
4.13 -(*\------- to exec-def.sml ------------------------/*)
4.14 -
4.15 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
4.16 (*NONE*)
4.17 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
4.18 @@ -96,23 +88,6 @@
4.19 if id1 = id2 then id1 else "merged_" ^ id1 ^ "_" ^ id2
4.20 end
4.21
4.22 -(*/------- to exec-def.sml ------------------------\*)
4.23 -type prog_calcID = string;
4.24 -(* op in isa-term "Const(op,_)" *)
4.25 -type cal = Rule_Def.calID * Rule_Def.eval_fn;
4.26 -type calc_elem = (* fun calculate_ fetches the evaluation-function via this list *)
4.27 - prog_calcID * (* a simple identifier used in programs *)
4.28 - (Rule_Def.calID * (* a long identifier used in Const *)
4.29 - Rule_Def.eval_fn) (* an ML function *)
4.30 -fun calc_eq ((pi1, (ci1, _)), (pi2, (ci2, _))) =
4.31 - if pi1 = pi2
4.32 - then if ci1 = ci2 then true else error ("calc_eq: " ^ ci1 ^ " <> " ^ ci2)
4.33 - else false
4.34 -fun e_evalfn (_ : 'a) (_ : term) (_ : theory) = NONE : (string * term) option;
4.35 -(*\------- to exec-def.sml ------------------------/*)
4.36 -
4.37 -(*val id_rls = Rule.identifier *)
4.38 -
4.39 (*/------- back to rule.sml -----------------------\*)
4.40 fun id_rls Rule_Def.Empty = "empty" (*WN060714 quick and dirty: recursive defs! TODO "Rule_Def.Empty"*)
4.41 | id_rls (Rule_Def.Repeat {id, ...}) = id
4.42 @@ -145,7 +120,7 @@
4.43 preconds = union (op =) pc1 pc2,
4.44 erls = merge (merge_ids er1 er2) er1 er2,
4.45 srls = merge (merge_ids sr1 sr2) sr1 sr2,
4.46 - calc = union calc_eq ca1 ca2,
4.47 + calc = union Exec_Def.calc_eq ca1 ca2,
4.48 rules = union eq_rule rs1 rs2,
4.49 errpatts = union (op =) eps1 eps2}
4.50 | merge id
4.51 @@ -158,7 +133,7 @@
4.52 preconds = union (op =) pc1 pc2,
4.53 erls = merge (merge_ids er1 er2) er1 er2,
4.54 srls = merge (merge_ids sr1 sr2) sr1 sr2,
4.55 - calc = union calc_eq ca1 ca2,
4.56 + calc = union Exec_Def.calc_eq ca1 ca2,
4.57 rules = union eq_rule rs1 rs2,
4.58 errpatts = union (op =) eps1 eps2}
4.59 | merge id _ _ = error ("merge: \"" ^ id ^
5.1 --- a/src/Tools/isac/Interpret/rewtools.sml Wed Apr 08 12:32:51 2020 +0200
5.2 +++ b/src/Tools/isac/Interpret/rewtools.sml Wed Apr 08 13:21:19 2020 +0200
5.3 @@ -11,7 +11,7 @@
5.4 val contains_rule : Rule.rule -> Rule_Set.T -> bool
5.5 val atomic_appl_tacs : theory -> string -> Rule_Set.T -> term -> Tactic.input -> Tactic.input list
5.6 val thy_containing_rls : Rule.theory' -> Rule_Set.identifier -> string * Rule.theory'
5.7 - val thy_containing_cal : Rule.theory' -> Rule_Set.prog_calcID -> string * string
5.8 + val thy_containing_cal : Rule.theory' -> Exec_Def.prog_calcID -> string * string
5.9 datatype contthy
5.10 = ContNOrew of {applto: term, thm_rls: Celem.guh, thyID: Rule.thyID}
5.11 | ContNOrewInst of {applto: term, bdvs: Rule.subst, thm_rls: Celem.guh, thminst: term, thyID: Rule.thyID}
6.1 --- a/src/Tools/isac/ProgLang/Auto_Prog.thy Wed Apr 08 12:32:51 2020 +0200
6.2 +++ b/src/Tools/isac/ProgLang/Auto_Prog.thy Wed Apr 08 13:21:19 2020 +0200
6.3 @@ -32,7 +32,7 @@
6.4 val subpbl: string -> string list -> term
6.5 val stacpbls: term -> term list
6.6 val op_of_calc: term -> string
6.7 - val get_calcs: theory -> term -> (Rule_Set.prog_calcID * (Rule.calID * Rule.eval_fn)) list
6.8 + val get_calcs: theory -> term -> (Exec_Def.prog_calcID * (Rule.calID * Rule.eval_fn)) list
6.9 val prep_rls: theory -> Rule_Set.T -> Rule_Set.T (*ren insert*)
6.10 val gen: theory -> term -> Rule_Set.T -> term
6.11 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
7.1 --- a/src/Tools/isac/ProgLang/calculate.sml Wed Apr 08 12:32:51 2020 +0200
7.2 +++ b/src/Tools/isac/ProgLang/calculate.sml Wed Apr 08 13:21:19 2020 +0200
7.3 @@ -12,7 +12,7 @@
7.4 val gcd: int -> int -> int
7.5 val sqrt: int -> int
7.6 val adhoc_thm: theory -> string * Rule.eval_fn -> term -> (string * thm) option
7.7 - val adhoc_thm1_: theory -> Rule_Set.cal -> term -> (string * thm) option
7.8 + val adhoc_thm1_: theory -> Exec_Def.cal -> term -> (string * thm) option
7.9 val norm: term -> term
7.10 val popt2str: ('a * term) option -> string
7.11 val numeral: term -> ((int * int) * (int * int)) option
8.1 --- a/src/Tools/isac/Specify/appl.sml Wed Apr 08 12:32:51 2020 +0200
8.2 +++ b/src/Tools/isac/Specify/appl.sml Wed Apr 08 13:21:19 2020 +0200
8.3 @@ -62,7 +62,7 @@
8.4 in
8.5 case opt of
8.6 SOME isa_fn => ("OK", thy', isa_fn)
8.7 - | NONE => ("applicable_in Calculate: unknown '" ^ scrop ^ "'", "", ("", Rule_Set.e_evalfn))
8.8 + | NONE => ("applicable_in Calculate: unknown '" ^ scrop ^ "'", "", ("", Exec_Def.e_evalfn))
8.9 end
8.10 else
8.11 let
8.12 @@ -71,7 +71,7 @@
8.13 in
8.14 case assoc (scr_isa_fns, scrop) of
8.15 SOME isa_fn => ("OK",thy',isa_fn)
8.16 - | NONE => ("applicable_in Calculate: unknown '" ^ scrop ^ "'", "", ("", Rule_Set.e_evalfn))
8.17 + | NONE => ("applicable_in Calculate: unknown '" ^ scrop ^ "'", "", ("", Exec_Def.e_evalfn))
8.18 end
8.19 end;
8.20
9.1 --- a/src/Tools/isac/TODO.thy Wed Apr 08 12:32:51 2020 +0200
9.2 +++ b/src/Tools/isac/TODO.thy Wed Apr 08 13:21:19 2020 +0200
9.3 @@ -47,7 +47,7 @@
9.4 activate : thmID_of_derivation_name'
9.5 *)
9.6 \item xxx
9.7 - \item xxx
9.8 + \item use "Exec_Def" for renaming identifiers
9.9 \item xxx
9.10 \item xxx
9.11 \item xxx
10.1 --- a/test/Tools/isac/ADDTESTS/accumulate-val/Thy_1.thy Wed Apr 08 12:32:51 2020 +0200
10.2 +++ b/test/Tools/isac/ADDTESTS/accumulate-val/Thy_1.thy Wed Apr 08 13:21:19 2020 +0200
10.3 @@ -14,6 +14,6 @@
10.4 else error "removal of Unsynchonized.ref: ruleset' <> Test_KEStore_Elems.get_rlss in Thy_1"*)
10.5 \<close>
10.6
10.7 -setup \<open>Test_KEStore_Elems.add_calcs [("calc", ("Thy_1", Rule_Set.e_evalfn))]\<close>
10.8 +setup \<open>Test_KEStore_Elems.add_calcs [("calc", ("Thy_1", Exec_Def.e_evalfn))]\<close>
10.9
10.10 end
11.1 --- a/test/Tools/isac/ADDTESTS/accumulate-val/lucas_interpreter.sml Wed Apr 08 12:32:51 2020 +0200
11.2 +++ b/test/Tools/isac/ADDTESTS/accumulate-val/lucas_interpreter.sml Wed Apr 08 13:21:19 2020 +0200
11.3 @@ -9,8 +9,8 @@
11.4 sig
11.5 val get_rlss: theory -> (Rule_Set.identifier * (Rule.theory' * Rule_Set.T)) list
11.6 val add_rlss: (Rule_Set.identifier * (Rule.theory' * Rule_Set.T)) list -> theory -> theory
11.7 - val get_calcs: theory -> (Rule_Set.prog_calcID * (Rule.calID * Rule.eval_fn)) list
11.8 - val add_calcs: (Rule_Set.prog_calcID * (Rule.calID * Rule.eval_fn)) list -> theory -> theory
11.9 + val get_calcs: theory -> (Exec_Def.prog_calcID * (Rule.calID * Rule.eval_fn)) list
11.10 + val add_calcs: (Exec_Def.prog_calcID * (Rule.calID * Rule.eval_fn)) list -> theory -> theory
11.11 (*etc*)
11.12 end;
11.13
11.14 @@ -30,7 +30,7 @@
11.15
11.16 val calc_eq = rls_eq
11.17 structure Data = Theory_Data (
11.18 - type T = (Rule_Set.prog_calcID * (Rule.calID * Rule.eval_fn)) list;
11.19 + type T = (Exec_Def.prog_calcID * (Rule.calID * Rule.eval_fn)) list;
11.20 val empty = [];
11.21 val extend = I;
11.22 val merge = merge calc_eq;