1.1 --- a/src/Tools/isac/BaseDefinitions/BaseDefinitions.thy Wed Feb 08 07:51:39 2023 +0100
1.2 +++ b/src/Tools/isac/BaseDefinitions/BaseDefinitions.thy Wed Feb 08 08:59:37 2023 +0100
1.3 @@ -62,7 +62,19 @@
1.4 ML_file environment.sml
1.5
1.6 ML \<open>
1.7 +open ThyC
1.8 \<close> ML \<open>
1.9 +cut_longid "Simplify.assoc"
1.10 +\<close> ML \<open>
1.11 +fun strip_thy str =
1.12 + let fun strip bdVar [] = implode (rev bdVar)
1.13 + | strip bdVar ("." :: _) = implode (rev bdVar)
1.14 + | strip bdVar (c :: cs) = strip (bdVar @ [c]) cs
1.15 + in strip [] (rev (Symbol.explode str)) end;
1.16 +\<close> ML \<open>
1.17 +strip_thy "Simplify.assoc"
1.18 +\<close> ML \<open>
1.19 +strip_thy: string -> string
1.20 \<close> ML \<open>
1.21 \<close>
1.22 end
2.1 --- a/src/Tools/isac/BaseDefinitions/libraryC.sml Wed Feb 08 07:51:39 2023 +0100
2.2 +++ b/src/Tools/isac/BaseDefinitions/libraryC.sml Wed Feb 08 08:59:37 2023 +0100
2.3 @@ -88,7 +88,6 @@
2.4 \<close>
2.5
2.6 (*///------------------------------>>> thy ------------------------------------------------\\\*)
2.7 - val get_thy: string -> string
2.8 val strip_thy: string -> string
2.9 (*\\\------------------------------>>> thy ------------------------------------------------///*)
2.10 (*///------------------------------>>> term -----------------------------------------------\\\*)
2.11 @@ -253,14 +252,6 @@
2.12 in aaa [] xs ys end;
2.13
2.14 (*///------------------------------>>> thy ------------------------------------------------\\\*)
2.15 -fun get_thy str =
2.16 - let
2.17 - fun get strl [] = strl
2.18 - | get strl ("." :: _) = strl
2.19 - | get strl ( s :: ss) = get (strl @ [s]) ss
2.20 - in implode (get [] (Symbol.explode str)) end;
2.21 -
2.22 -
2.23 fun strip_thy str =
2.24 let fun strip bdVar [] = implode (rev bdVar)
2.25 | strip bdVar ("." :: _) = implode (rev bdVar)
3.1 --- a/src/Tools/isac/BaseDefinitions/theoryC.sml Wed Feb 08 07:51:39 2023 +0100
3.2 +++ b/src/Tools/isac/BaseDefinitions/theoryC.sml Wed Feb 08 08:59:37 2023 +0100
3.3 @@ -7,7 +7,7 @@
3.4 signature THEORY_ISAC =
3.5 sig
3.6 eqtype id
3.7 - val cut_id: string -> id
3.8 + val cut_longid: string -> id
3.9 val id_of: theory -> id
3.10 val get_theory: Proof.context -> id -> theory
3.11
3.12 @@ -30,7 +30,7 @@
3.13 (**)
3.14
3.15 type id = string;
3.16 -fun cut_id dn = hd (space_explode "." dn);
3.17 +fun cut_longid dn = hd (space_explode "." dn);
3.18 fun id_of thy = thy |> Context.theory_id |> Context.theory_id_name
3.19
3.20 fun get_theory ctxt thy_id =
4.1 --- a/src/Tools/isac/Interpret/error-pattern.sml Wed Feb 08 07:51:39 2023 +0100
4.2 +++ b/src/Tools/isac/Interpret/error-pattern.sml Wed Feb 08 08:59:37 2023 +0100
4.3 @@ -126,7 +126,7 @@
4.4 fun fill_from_store ctxt subst form errpat_id thm =
4.5 let
4.6 val thm_id_long = Thm.get_name_hint thm
4.7 - val thm_id = ThmC.cut_id thm_id_long
4.8 + val thm_id = ThmC.cut_longid thm_id_long
4.9 val fill_ins = get_fill_ins (Proof_Context.theory_of ctxt) thm_id;
4.10 val some = map (fill_form ctxt subst (thm, form) errpat_id) fill_ins;
4.11 in some |> filter is_some |> map the end
5.1 --- a/src/Tools/isac/Knowledge/Integrate.thy Wed Feb 08 07:51:39 2023 +0100
5.2 +++ b/src/Tools/isac/Knowledge/Integrate.thy Wed Feb 08 08:59:37 2023 +0100
5.3 @@ -46,28 +46,32 @@
5.4 val c = Free ("c", HOLogic.realT);
5.5 (*.create a new unique variable 'c..' in a term; for use by \<^rule_eval> in a rls;
5.6 an alternative to do this would be '(Try (Calculate new_c_) (new_c es__))'
5.7 - in the script; this will be possible if currying doesnt take the value
5.8 + in the program; this would be possible if currying would not take the value
5.9 from a variable, but the value '(new_c es__)' itself.*)
5.10 fun new_c term =
5.11 - let fun selc var =
5.12 - case (Symbol.explode o id_of) var of
5.13 - "c"::[] => true
5.14 - | "c"::"_"::is => (case (TermC.int_opt_of_string o implode) is of
5.15 - SOME _ => true
5.16 - | NONE => false)
5.17 - | _ => false;
5.18 - fun get_coeff c = case (Symbol.explode o id_of) c of
5.19 - "c"::"_"::is => (the o TermC.int_opt_of_string o implode) is
5.20 - | _ => 0;
5.21 - val cs = filter selc (TermC.vars term);
5.22 - in
5.23 - case cs of
5.24 + let
5.25 + fun selc var =
5.26 + case (Symbol.explode o LibraryC.id_of) var of
5.27 + "c"::[] => true
5.28 + | "c" :: "_":: is =>
5.29 + (case (TermC.int_opt_of_string o implode) is of
5.30 + SOME _ => true
5.31 + | NONE => false)
5.32 + | _ => false;
5.33 + fun get_coeff c =
5.34 + case (Symbol.explode o LibraryC.id_of) c of
5.35 + "c"::"_"::is => (the o TermC.int_opt_of_string o implode) is
5.36 + | _ => 0;
5.37 + val cs = filter selc (TermC.vars term);
5.38 + in
5.39 + case cs of
5.40 [] => c
5.41 | [_] => Free ("c_2", HOLogic.realT)
5.42 | cs =>
5.43 let val max_coeff = maxl (map get_coeff cs)
5.44 in Free ("c_"^string_of_int (max_coeff + 1), HOLogic.realT) end
5.45 - end;
5.46 + end;
5.47 +\<close> ML \<open>
5.48
5.49 (*WN080222:*)
5.50 (*("add_new_c", ("Integrate.add_new_c", eval_add_new_c "#add_new_c_"))
6.1 --- a/src/Tools/isac/MathEngBasic/thmC.sml Wed Feb 08 07:51:39 2023 +0100
6.2 +++ b/src/Tools/isac/MathEngBasic/thmC.sml Wed Feb 08 08:59:37 2023 +0100
6.3 @@ -11,7 +11,7 @@
6.4 type id = ThmC_Def.id (* shortest possible *)
6.5 type long_id (* e.g. "Test.radd_left_commute"*)
6.6
6.7 - val cut_id: string -> id
6.8 + val cut_longid: string -> id
6.9 val long_id: T -> long_id
6.10
6.11 val string_of_thm: Proof.context -> thm -> string
6.12 @@ -53,12 +53,12 @@
6.13 thmID
6.14 |> Global_Theory.get_thm (Know_Store.get_via_last_thy "Isac_Knowledge")
6.15 |> Thm.get_name_hint
6.16 -fun cut_id dn = last_elem (space_explode "." dn); (*the cut_id is the key into Know_Store*)
6.17 +fun cut_longid dn = last_elem (space_explode "." dn); (*the cut_longid is the key into Know_Store*)
6.18
6.19 val string_of_thm = ThmC_Def.string_of_thm;
6.20 val string_of_thms = ThmC_Def.string_of_thms;
6.21
6.22 -fun id_of_thm thm = thm |> Thm.get_name_hint |> cut_id;
6.23 +fun id_of_thm thm = thm |> Thm.get_name_hint |> cut_longid;
6.24 fun of_thm thm = (id_of_thm thm, thm);
6.25 fun from_rule _ (Rule.Thm (id, thm)) = (id, thm)
6.26 | from_rule ctxt r =
6.27 @@ -157,7 +157,7 @@
6.28 (* revert a thm RS @{thm sym} back to original thm, in case it ML\<open>is_sym\<close> *)
6.29 fun revert_sym_rule thy (Rule.Thm (id, thm)) =
6.30 (*this ^^ might come from the user, who doesn't care about thy*)
6.31 - if is_sym (cut_id id)
6.32 + if is_sym (cut_longid id)
6.33 then
6.34 let
6.35 val id' = id_drop_sym id
7.1 --- a/test/Tools/isac/BaseDefinitions/calcelems.sml Wed Feb 08 07:51:39 2023 +0100
7.2 +++ b/test/Tools/isac/BaseDefinitions/calcelems.sml Wed Feb 08 08:59:37 2023 +0100
7.3 @@ -8,9 +8,9 @@
7.4 "table of contents --------------------------------------";
7.5 "--------------------------------------------------------";
7.6 "-------- Unsynchronized.ref doesn't work any more ------";
7.7 -"-------- fun ThmC.cut_id ------------------";
7.8 +"-------- fun ThmC.cut_longid ------------------";
7.9 "-------- fun UnparseC.term ----------------------------------";
7.10 -"-------- fun ThmC.cut_id 000---------------";
7.11 +"-------- fun ThmC.cut_longid 000---------------";
7.12 "-------- fun Rule_Set.merge -----------------------------------------------------";
7.13 "-------- fun update_ptyps --------------------------------------------------";
7.14 "-------- fun subst2str' -----------------------------------------------------------------------";
7.15 @@ -35,24 +35,24 @@
7.16 --- fun insert_errpats ---, see changeset 90f3855dee3b *)
7.17
7.18
7.19 -"-------- fun ThmC.cut_id ----------------";
7.20 -"-------- fun ThmC.cut_id ----------------";
7.21 -"-------- fun ThmC.cut_id ----------------";
7.22 +"-------- fun ThmC.cut_longid ----------------";
7.23 +"-------- fun ThmC.cut_longid ----------------";
7.24 +"-------- fun ThmC.cut_longid ----------------";
7.25 val thm = @{thm radd_0};
7.26 val dn = Thm.derivation_name thm;
7.27 if dn = "Test.radd_0" then ()
7.28 else error "calcelems.sml Thm.derivation_name changed 1";
7.29
7.30 -val thmID = ThmC.cut_id dn;
7.31 -val thyID = ThyC.cut_id dn;
7.32 +val thmID = ThmC.cut_longid dn;
7.33 +val thyID = ThyC.cut_longid dn;
7.34 if thmID = "radd_0" andalso thyID = "Test" then ()
7.35 else error "calcelems.sml Thm.derivation_name changed 2";
7.36
7.37 "--- thm2 --";
7.38 val thm = @{thm add_divide_distrib}
7.39 val dn = Thm.derivation_name thm;
7.40 -val thmID = ThmC.cut_id dn;
7.41 -val thyID = ThyC.cut_id dn;
7.42 +val thmID = ThmC.cut_longid dn;
7.43 +val thyID = ThyC.cut_longid dn;
7.44 if thmID = "add_divide_distrib" andalso thyID = "Fields" then ()
7.45 else error "calcelems.sml Thm.derivation_name changed 3";
7.46
7.47 @@ -79,18 +79,18 @@
7.48 (*default_print_depth 3;*)
7.49 *)
7.50
7.51 -"-------- fun ThmC.cut_id 000---------------";
7.52 -"-------- fun ThmC.cut_id 000---------------";
7.53 -"-------- fun ThmC.cut_id 000---------------";
7.54 +"-------- fun ThmC.cut_longid 000---------------";
7.55 +"-------- fun ThmC.cut_longid 000---------------";
7.56 +"-------- fun ThmC.cut_longid 000---------------";
7.57 val long_id = Thm.get_name_hint @{thm mult_1_left};
7.58 if long_id = "Groups.monoid_mult_class.mult_1_left" then ()
7.59 else error "fun Thm.get_name_hint or @{thm mult_1_left} changed";
7.60
7.61 -if ThmC.cut_id long_id = "mult_1_left" then ()
7.62 -else error "fun ThmC.cut_id broken";
7.63 +if ThmC.cut_longid long_id = "mult_1_left" then ()
7.64 +else error "fun ThmC.cut_longid broken";
7.65
7.66 -if ThyC.cut_id long_id = "Groups" then ()
7.67 -else error "fun ThyC.cut_id broken";
7.68 +if ThyC.cut_longid long_id = "Groups" then ()
7.69 +else error "fun ThyC.cut_longid broken";
7.70
7.71 "-------- fun Rule_Set.merge -----------------------------------------------------";
7.72 "-------- fun Rule_Set.merge -----------------------------------------------------";
8.1 --- a/test/Tools/isac/Interpret/error-pattern.sml Wed Feb 08 07:51:39 2023 +0100
8.2 +++ b/test/Tools/isac/Interpret/error-pattern.sml Wed Feb 08 08:59:37 2023 +0100
8.3 @@ -1139,9 +1139,9 @@
8.4 val thm_id_long = Thm.get_name_hint thm
8.5
8.6 (*+*)val "Diff.diff_sin_chain" = thm_id_long;
8.7 -(*+*)val "diff_sin_chain" = ThmC.cut_id thm_id_long;
8.8 +(*+*)val "diff_sin_chain" = ThmC.cut_longid thm_id_long;
8.9
8.10 - val thm_id = ThmC.cut_id thm_id_long
8.11 + val thm_id = ThmC.cut_longid thm_id_long
8.12 val fill_ins =
8.13
8.14 Error_Pattern.get_fill_ins (Proof_Context.theory_of ctxt) thm_id;
9.1 --- a/test/Tools/isac/Knowledge/rational-2.sml Wed Feb 08 07:51:39 2023 +0100
9.2 +++ b/test/Tools/isac/Knowledge/rational-2.sml Wed Feb 08 08:59:37 2023 +0100
9.3 @@ -717,7 +717,7 @@
9.4
9.5 if length (hd revsets) = 11 then () else error "length of revset changed";
9.6 if (revsets |> nth 1 |> nth 1 |> Rule.id) =
9.7 - (@{thm realpow_twoI} |> Thm.get_name_hint |> ThmC.cut_id)
9.8 + (@{thm realpow_twoI} |> Thm.get_name_hint |> ThmC.cut_longid)
9.9 then () else error "first element of revset changed";
9.10 if
9.11 (revsets |> nth 1 |> nth 1 |> Rule.to_string ctxt) = "Thm (\"realpow_twoI\", ?r1 \<up> 2 = ?r1 * ?r1)" andalso
10.1 --- a/test/Tools/isac/MathEngBasic/thmC.sml Wed Feb 08 07:51:39 2023 +0100
10.2 +++ b/test/Tools/isac/MathEngBasic/thmC.sml Wed Feb 08 08:59:37 2023 +0100
10.3 @@ -50,8 +50,8 @@
10.4
10.5 if id = "sym_real_mult_minus1" andalso ThmC.string_of_thm ctxt thm = "- ?z1 = - 1 * ?z1" then ()
10.6 else error "input to revert_sym_rule CHANGED";
10.7 -
10.8 - (*if*) is_sym (cut_id id) (*then*);
10.9 +
10.10 + (*if*) is_sym (ThmC.cut_longid id) (*then*);
10.11 val id' = id_drop_sym id
10.12 val thm' = thm_from_thy thy id'
10.13 val id'' = Thm.get_name_hint thm'