1.1 --- a/src/Tools/isac/CalcElements/KEStore.thy Thu Apr 09 18:21:09 2020 +0200
1.2 +++ b/src/Tools/isac/CalcElements/KEStore.thy Fri Apr 10 12:28:47 2020 +0200
1.3 @@ -6,13 +6,13 @@
1.4
1.5 begin
1.6 ML_file libraryC.sml
1.7 +ML_file theoryC.sml
1.8 +ML_file "unparseC.sml"
1.9 ML_file "rule-def.sml"
1.10 +ML_file thmC.sml
1.11 ML_file "exec-def.sml"
1.12 ML_file "rewrite-order.sml"
1.13 -ML_file theoryC.sml
1.14 ML_file rule.sml
1.15 -ML_file "unparseC.sml"
1.16 -ML_file thmC.sml
1.17 ML_file "error-fill-def.sml"
1.18 ML_file "rule-set.sml"
1.19 ML_file calcelems.sml
2.1 --- a/src/Tools/isac/CalcElements/rule-set.sml Thu Apr 09 18:21:09 2020 +0200
2.2 +++ b/src/Tools/isac/CalcElements/rule-set.sml Fri Apr 10 12:28:47 2020 +0200
2.3 @@ -29,9 +29,6 @@
2.4 val e_rrls: T
2.5 (*\------- this will disappear eventually -----------/*)
2.6
2.7 - val rule2str: Rule_Def.rule -> string
2.8 - val rule2str': Rule_Def.rule -> string
2.9 -
2.10 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
2.11 (*NONE*)
2.12 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
2.13 @@ -115,17 +112,6 @@
2.14 | merge id _ _ = error ("merge: \"" ^ id ^
2.15 "\"; not for reverse-rewrite-rule-sets and not for mixed Rls -- Rule_Def.Seqence");
2.16
2.17 -fun rule2str Rule_Def.Erule = "Erule"
2.18 - | rule2str (Rule_Def.Thm (str, thm)) = "Thm (\"" ^ str ^ "\"," ^ ThmC.string_of_thmI thm ^ ")"
2.19 - | rule2str (Rule_Def.Num_Calc (str, _)) = "Num_Calc (\"" ^ str ^ "\",fn)"
2.20 - | rule2str (Rule_Def.Cal1 (str, _)) = "Cal1 (\"" ^ str ^ "\",fn)"
2.21 - | rule2str (Rule_Def.Rls_ rls) = "Rls_ (\"" ^ rls2str rls ^ "\")";
2.22 -fun rule2str' Rule_Def.Erule = "Erule"
2.23 - | rule2str' (Rule_Def.Thm (str, _)) = "Thm (\"" ^ str ^ "\",\"\")"
2.24 - | rule2str' (Rule_Def.Num_Calc (str, _)) = "Num_Calc (\"" ^ str ^ "\",fn)"
2.25 - | rule2str' (Rule_Def.Cal1 (str, _)) = "Cal1 (\"" ^ str ^ "\",fn)"
2.26 - | rule2str' (Rule_Def.Rls_ rls) = "Rls_ (\"" ^ rls2str rls ^ "\")";
2.27 -
2.28 (* datastructure for KEStore_Elems, intermediate for thehier *)
2.29 type for_kestore =
2.30 (identifier * (* identifier unique within Isac *)
3.1 --- a/src/Tools/isac/CalcElements/rule.sml Thu Apr 09 18:21:09 2020 +0200
3.2 +++ b/src/Tools/isac/CalcElements/rule.sml Fri Apr 10 12:28:47 2020 +0200
3.3 @@ -14,10 +14,12 @@
3.4 val id_rls: Rule_Def.rule_set -> string
3.5 val id_rule: Rule_Def.rule -> string
3.6 val eq_rule: Rule_Def.rule * Rule_Def.rule -> bool
3.7 + val rule2str: Rule_Def.rule -> string
3.8 + val rule2str': Rule_Def.rule -> string
3.9 +
3.10 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
3.11 (*NONE*)
3.12 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
3.13 - (*NONE*)
3.14 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
3.15 end
3.16
3.17 @@ -54,4 +56,15 @@
3.18 | eq_rule (Rule_Def.Rls_ rls1, Rule_Def.Rls_ rls2) = id_rls rls1 = id_rls rls2
3.19 | eq_rule _ = false;
3.20
3.21 +fun rule2str Rule_Def.Erule = "Erule"
3.22 + | rule2str (Rule_Def.Thm (str, thm)) = "Thm (\"" ^ str ^ "\"," ^ ThmC.string_of_thmI thm ^ ")"
3.23 + | rule2str (Rule_Def.Num_Calc (str, _)) = "Num_Calc (\"" ^ str ^ "\",fn)"
3.24 + | rule2str (Rule_Def.Cal1 (str, _)) = "Cal1 (\"" ^ str ^ "\",fn)"
3.25 + | rule2str (Rule_Def.Rls_ rls) = "Rls_ (\"" ^ id_rls rls ^ "\")";
3.26 +fun rule2str' Rule_Def.Erule = "Erule"
3.27 + | rule2str' (Rule_Def.Thm (str, _)) = "Thm (\"" ^ str ^ "\",\"\")"
3.28 + | rule2str' (Rule_Def.Num_Calc (str, _)) = "Num_Calc (\"" ^ str ^ "\",fn)"
3.29 + | rule2str' (Rule_Def.Cal1 (str, _)) = "Cal1 (\"" ^ str ^ "\",fn)"
3.30 + | rule2str' (Rule_Def.Rls_ rls) = "Rls_ (\"" ^ id_rls rls ^ "\")";
3.31 +
3.32 (**)end(**)
4.1 --- a/src/Tools/isac/CalcElements/thmC.sml Thu Apr 09 18:21:09 2020 +0200
4.2 +++ b/src/Tools/isac/CalcElements/thmC.sml Fri Apr 10 12:28:47 2020 +0200
4.3 @@ -17,7 +17,7 @@
4.4 val thmID_of_derivation_name: string -> string
4.5 val thmID_of_derivation_name': thm -> string
4.6 val thm''_of_thm: thm -> thm''
4.7 - val thm_of_thm: Rule.rule -> thm
4.8 + val thm_of_thm: Rule_Def.rule -> thm
4.9
4.10 val string_of_thmI: thm -> string
4.11 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
4.12 @@ -28,7 +28,7 @@
4.13 val string_of_thm': theory -> thm -> string
4.14 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
4.15 (*/------- to ThmC.sml ------\*)
4.16 - val id_of_thm: Rule.rule -> string
4.17 + val id_of_thm: Rule_Def.rule -> string
4.18 (*\------- to ThmC.sml ------/*)
4.19 end
4.20
4.21 @@ -84,13 +84,13 @@
4.22 | _ => str
4.23 end
4.24
4.25 -fun id_of_thm (Rule.Thm (id, _)) = id (* TODO re-arrange code for rule2str *)
4.26 +fun id_of_thm (Rule_Def.Thm (id, _)) = id (* TODO re-arrange code for rule2str *)
4.27 | id_of_thm _ = raise ERROR ("id_of_thm: uncovered case " (* ^ rule2str r *))
4.28
4.29 fun thmID_of_derivation_name dn = last_elem (space_explode "." dn);
4.30 fun thmID_of_derivation_name' thm = (thmID_of_derivation_name o Thm.get_name_hint) thm
4.31 fun thyID_of_derivation_name dn = hd (space_explode "." dn);
4.32 -fun thm_of_thm (Rule.Thm (_, thm)) = thm (* TODO re-arrange code for rule2str *)
4.33 +fun thm_of_thm (Rule_Def.Thm (_, thm)) = thm (* TODO re-arrange code for rule2str *)
4.34 | thm_of_thm _ = raise ERROR ("thm_of_thm: uncovered case " (* ^ rule2str r *))
4.35 fun thm''_of_thm thm = (thmID_of_derivation_name' thm, thm) : thm''
4.36
5.1 --- a/src/Tools/isac/Interpret/error-fill-pattern.sml Thu Apr 09 18:21:09 2020 +0200
5.2 +++ b/src/Tools/isac/Interpret/error-fill-pattern.sml Fri Apr 10 12:28:47 2020 +0200
5.3 @@ -44,9 +44,9 @@
5.4 type errpatID = Rule_Def.errpatID
5.5
5.6 fun rule2thm'' (Rule.Thm (id, thm)) = (id, thm)
5.7 - | rule2thm'' r = error ("rule2thm': not defined for " ^ Rule_Set.rule2str r);
5.8 + | rule2thm'' r = error ("rule2thm': not defined for " ^ Rule.rule2str r);
5.9 fun rule2rls' (Rule.Rls_ rls) = Rule_Set.rls2str rls
5.10 - | rule2rls' r = error ("rule2rls': not defined for " ^ Rule_Set.rule2str r);
5.11 + | rule2rls' r = error ("rule2rls': not defined for " ^ Rule.rule2str r);
5.12
5.13 (*the lists contain eq-al elem-pairs at the beginning;
5.14 return first list reverted (again) - ie. in order as required subsequently*)
5.15 @@ -76,7 +76,7 @@
5.16 (Tactic.Rewrite_Set (rule2rls' r),
5.17 Tactic.Rewrite_Set' ("Isac_Knowledge", false, rls, t, (t', a)),
5.18 (Pos.e_pos'(*to be updated before generate tacis!!!*), (Istate.Uistate, ContextC.empty)))
5.19 - | mk_tacis _ _ (t, r, _) = error ("mk_tacis: not impl. for " ^ Rule_Set.rule2str r ^ " at " ^ UnparseC.term2str t)
5.20 + | mk_tacis _ _ (t, r, _) = error ("mk_tacis: not impl. for " ^ Rule.rule2str r ^ " at " ^ UnparseC.term2str t)
5.21
5.22 (* fo = ifo excluded already in inform *)
5.23 fun concat_deriv rew_ord erls rules fo ifo =
6.1 --- a/src/Tools/isac/Interpret/rewtools.sml Thu Apr 09 18:21:09 2020 +0200
6.2 +++ b/src/Tools/isac/Interpret/rewtools.sml Fri Apr 10 12:28:47 2020 +0200
6.3 @@ -90,11 +90,11 @@
6.4 list
6.5
6.6 fun trta2str (t, r, (t', a)) =
6.7 - "\n(" ^ UnparseC.term2str t ^ ", " ^ Rule_Set.rule2str' r ^ ", (" ^ UnparseC.term2str t' ^ ", " ^ UnparseC.terms2str a ^ "))"
6.8 + "\n(" ^ UnparseC.term2str t ^ ", " ^ Rule.rule2str' r ^ ", (" ^ UnparseC.term2str t' ^ ", " ^ UnparseC.terms2str a ^ "))"
6.9 fun trtas2str trtas = (strs2str o (map trta2str)) trtas
6.10 val deriv2str = trtas2str
6.11 fun rta2str (r, (t, a)) =
6.12 - "\n(" ^ Rule_Set.rule2str' r ^ ", (" ^ UnparseC.term2str t ^ ", " ^ UnparseC.terms2str a ^ "))"
6.13 + "\n(" ^ Rule.rule2str' r ^ ", (" ^ UnparseC.term2str t ^ ", " ^ UnparseC.terms2str a ^ "))"
6.14 fun rtas2str rtas = (strs2str o (map rta2str)) rtas
6.15 val deri2str = rtas2str
6.16
6.17 @@ -186,7 +186,7 @@
6.18 (case Rewrite.rewrite_set_ thy true rls t of
6.19 NONE => rew_once lim rts t apno rs'
6.20 | SOME (t', a') => rew_once (lim - 1) (rts @ [(t, r, (t', a'))]) t' Appl rrs')
6.21 - | rule => error ("rew_once: uncovered case " ^ Rule_Set.rule2str rule))
6.22 + | rule => error ("rew_once: uncovered case " ^ Rule.rule2str rule))
6.23 | rew_or_calc _ _ _ _ [] = error "rew_or_calc: called with []"
6.24 in rew_once (! Celem.lim_deriv) [] tt Noap rs end
6.25
6.26 @@ -222,7 +222,7 @@
6.27 | _ => "sym_" ^ thmID
6.28 in Rule.Thm (thmID', thm') end
6.29 | sym_rule (Rule.Rls_ rls) = Rule.Rls_ (sym_rls rls) (* TODO? handle with interSteps ? *)
6.30 -| sym_rule r = error ("sym_rule: not for " ^ Rule_Set.rule2str r)
6.31 +| sym_rule r = error ("sym_rule: not for " ^ Rule.rule2str r)
6.32
6.33 (*version for reverse rewrite used before 040214*)
6.34 fun rev_deriv (t, r, (_, a)) = (sym_rule r, (t, a));
6.35 @@ -233,7 +233,7 @@
6.36 | eq_Thm (Rule.Thm (_, _), _) = false
6.37 | eq_Thm (Rule.Rls_ r1, Rule.Rls_ r2) = Rule_Set.rls2str r1 = Rule_Set.rls2str r2
6.38 | eq_Thm (Rule.Rls_ _, _) = false
6.39 - | eq_Thm (r1, r2) = error ("eq_Thm: called with '" ^ Rule_Set.rule2str r1 ^ "' '" ^ Rule_Set.rule2str r2 ^ "'")
6.40 + | eq_Thm (r1, r2) = error ("eq_Thm: called with '" ^ Rule.rule2str r1 ^ "' '" ^ Rule.rule2str r2 ^ "'")
6.41 fun distinct_Thm r = gen_distinct eq_Thm r
6.42
6.43 fun eq_Thms thmIDs thm = (member op = thmIDs (ThmC.id_of_thm thm))
7.1 --- a/src/Tools/isac/MathEngBasic/istate-def.sml Thu Apr 09 18:21:09 2020 +0200
7.2 +++ b/src/Tools/isac/MathEngBasic/istate-def.sml Fri Apr 10 12:28:47 2020 +0200
7.3 @@ -74,13 +74,13 @@
7.4 | RrlsState of Rule_Set.rrlsstate; (*for reverse rewriting*)
7.5 val empty = Pstate e_pstate;
7.6
7.7 -fun rta2str (r, (t, a)) = "\n(" ^ Rule_Set.rule2str r ^ ", (" ^ UnparseC.term2str t ^ ", " ^ UnparseC.terms2str a ^ "))";
7.8 +fun rta2str (r, (t, a)) = "\n(" ^ Rule.rule2str r ^ ", (" ^ UnparseC.term2str t ^ ", " ^ UnparseC.terms2str a ^ "))";
7.9 fun string_of Uistate = "Uistate"
7.10 | string_of (Pstate pst) =
7.11 "Pstate " ^ pstate2str pst
7.12 | string_of (RrlsState (t, t1, rss, rtas)) =
7.13 "RrlsState (" ^ UnparseC.term2str t ^ ", " ^ UnparseC.term2str t1 ^ ", " ^
7.14 - (strs2str o (map (strs2str o (map Rule_Set.rule2str)))) rss ^ ", " ^
7.15 + (strs2str o (map (strs2str o (map Rule.rule2str)))) rss ^ ", " ^
7.16 (strs2str o (map rta2str)) rtas ^ ")";
7.17 fun string_of' Uistate = "Uistate"
7.18 | string_of' (Pstate pst) =
8.1 --- a/src/Tools/isac/MathEngBasic/tactic.sml Thu Apr 09 18:21:09 2020 +0200
8.2 +++ b/src/Tools/isac/MathEngBasic/tactic.sml Fri Apr 10 12:28:47 2020 +0200
8.3 @@ -319,7 +319,7 @@
8.4 | rule2tac _ subst (Rule.Rls_ rls) =
8.5 Rewrite_Set_Inst (Selem.subst2subs subst, (Rule_Set.rls2str rls))
8.6 | rule2tac _ _ rule =
8.7 - error ("rule2tac: called with \"" ^ Rule_Set.rule2str rule ^ "\"");
8.8 + error ("rule2tac: called with \"" ^ Rule.rule2str rule ^ "\"");
8.9
8.10 (* tactics for for internal use, compare "input" for user at the front-end.
8.11 tac_ contains results from check in 'fun applicable_in'.
9.1 --- a/src/Tools/isac/ProgLang/Auto_Prog.thy Thu Apr 09 18:21:09 2020 +0200
9.2 +++ b/src/Tools/isac/ProgLang/Auto_Prog.thy Fri Apr 10 12:28:47 2020 +0200
9.3 @@ -134,7 +134,7 @@
9.4 | rule2stac thy (Rule.Num_Calc (c, _)) = Try $ (Repeat $ (Cal $ HOLogic.mk_string (assoc_calc thy c)))
9.5 | rule2stac thy (Rule.Cal1 (c, _)) = Try $ (Repeat $ (Ca1 $ HOLogic.mk_string (assoc_calc thy c)))
9.6 | rule2stac _ (Rule.Rls_ rls) = Try $ (Rew_Set $ HOLogic.mk_string (Rule_Set.rls2str rls))
9.7 - | rule2stac _ r = raise ERROR ("rule2stac: not applicable to \"" ^ Rule_Set.rule2str r ^ "\"");
9.8 + | rule2stac _ r = raise ERROR ("rule2stac: not applicable to \"" ^ Rule.rule2str r ^ "\"");
9.9 fun rule2stac_inst _ (Rule.Thm (thmID, _)) =
9.10 Try $ (Repeat $ (Rew_Inst $ Subs $ HOLogic.mk_string thmID))
9.11 | rule2stac_inst thy (Rule.Num_Calc (c, _)) =
9.12 @@ -143,7 +143,7 @@
9.13 Try $ (Repeat $ (Cal $ HOLogic.mk_string (assoc_calc thy c)))
9.14 | rule2stac_inst _ (Rule.Rls_ rls) =
9.15 Try $ (Rew_Set_Inst $ Subs $ HOLogic.mk_string (Rule_Set.rls2str rls))
9.16 - | rule2stac_inst _ r = raise ERROR ("rule2stac_inst: not applicable to \"" ^ Rule_Set.rule2str r ^ "\"");
9.17 + | rule2stac_inst _ r = raise ERROR ("rule2stac_inst: not applicable to \"" ^ Rule.rule2str r ^ "\"");
9.18
9.19 (*for appropriate nesting take stacs in _reverse_ order*)
9.20 fun op #>@ sts [s] = SEq $ s $ sts
10.1 --- a/src/Tools/isac/ProgLang/rewrite.sml Thu Apr 09 18:21:09 2020 +0200
10.2 +++ b/src/Tools/isac/ProgLang/rewrite.sml Fri Apr 10 12:28:47 2020 +0200
10.3 @@ -180,7 +180,7 @@
10.4 (case rewrite__set_ thy (i + 1) put_asm bdv rls' ct of
10.5 SOME (t', asm') => rew_once ruls (union (op =) asm asm') t' Appl thms
10.6 | NONE => rew_once ruls asm ct apno thms)
10.7 - | r => raise ERROR ("rew_once not appl. to \"" ^ Rule_Set.rule2str r ^ "\"");
10.8 + | r => raise ERROR ("rew_once not appl. to \"" ^ Rule.rule2str r ^ "\"");
10.9 val ruls = (#rules o Rule_Set.rep) rls;
10.10 val _ = trace i (" rls: " ^ Rule_Set.rls2str rls ^ " on: " ^ UnparseC.t2str thy ct)
10.11 val (ct', asm') = rew_once ruls [] ct Noap ruls;