1.1 --- a/TODO.md Wed Apr 21 11:24:46 2021 +0200
1.2 +++ b/TODO.md Wed Apr 21 11:47:33 2021 +0200
1.3 @@ -3,8 +3,6 @@
1.4 - or more basic try/can combinators;
1.5 - or more direct ML of intention;
1.6
1.7 -* WN: check remaining "for tests only" wrt. \<^isac_test>CARTOUCHE;
1.8 -
1.9 * WN: purge BridgeLibisabelle: eliminate unused code;
1.10
1.11
2.1 --- a/src/Tools/isac/BaseDefinitions/libraryC.sml Wed Apr 21 11:24:46 2021 +0200
2.2 +++ b/src/Tools/isac/BaseDefinitions/libraryC.sml Wed Apr 21 11:47:33 2021 +0200
2.3 @@ -25,7 +25,6 @@
2.4 val assoc_string: (string * 'a) list * string -> 'a option
2.5 val bool2str: bool -> string
2.6 val commas: string list -> string
2.7 - val compare_strs: string -> string -> unit list
2.8 val dashs: int -> string
2.9 val de_quote: string -> string
2.10 val dots: int -> string
2.11 @@ -226,12 +225,6 @@
2.12 fun if_none NONE y = y (*cp from 2002 Pure/library.ML FIXXXME replace*)
2.13 | if_none (SOME x) _ = x;
2.14
2.15 -(* for tests only *)
2.16 -fun compare_strs str1 str2 =
2.17 - let
2.18 - fun comp_char (c1, c2) = tracing ("comp_strs: " ^ c1 ^ " = " ^ c2 ^ " ..." ^ bool2str (c1 = c2))
2.19 - in map comp_char ((Symbol.explode str1) ~~ (Symbol.explode str2)) end;
2.20 -
2.21 fun triple2pair (a, b, _) = (a, b);
2.22 \<^isac_test>\<open>
2.23 fun quad2pair (a, b, _, _) = (a, b);
2.24 @@ -267,6 +260,7 @@
2.25 | get strl ( s :: ss) = get (strl @ [s]) ss
2.26 in implode (get [] (Symbol.explode str)) end;
2.27
2.28 +
2.29 fun strip_thy str =
2.30 let fun strip bdVar [] = implode (rev bdVar)
2.31 | strip bdVar ("." :: _) = implode (rev bdVar)
3.1 --- a/src/Tools/isac/BaseDefinitions/substitution.sml Wed Apr 21 11:24:46 2021 +0200
3.2 +++ b/src/Tools/isac/BaseDefinitions/substitution.sml Wed Apr 21 11:47:33 2021 +0200
3.3 @@ -21,7 +21,6 @@
3.4
3.5 type as_string_eqs (* for Tactic.Substitute ["bdv_1 = x", ...] *)
3.6 val string_eqs_to_string: as_string_eqs -> string
3.7 - val string_eqs_empty: as_string_eqs
3.8
3.9 val T_to_string_eqs: T -> as_string_eqs
3.10 val T_to_input: T -> input
3.11 @@ -33,6 +32,7 @@
3.12 val program_to_input: program -> input
3.13 val for_bdv: program -> T -> input option * T
3.14 \<^isac_test>\<open>
3.15 + val string_eqs_empty: as_string_eqs
3.16 val T_from_program: program -> T
3.17 \<close>
3.18 end
3.19 @@ -52,7 +52,9 @@
3.20 val input_empty = [];
3.21
3.22 type as_string_eqs = TermC.as_string list;
3.23 -val string_eqs_empty = []: TermC.as_string list; (* for tests only *)
3.24 +\<^isac_test>\<open>
3.25 +val string_eqs_empty = []: TermC.as_string list;
3.26 +\<close>
3.27 fun string_eqs_to_string s = strs2str s;
3.28
3.29 type as_eqs = term list;
4.1 --- a/src/Tools/isac/Interpret/lucas-interpreter.sml Wed Apr 21 11:24:46 2021 +0200
4.2 +++ b/src/Tools/isac/Interpret/lucas-interpreter.sml Wed Apr 21 11:47:33 2021 +0200
4.3 @@ -28,12 +28,14 @@
4.4 val by_tactic: Tactic.T -> Istate.T * Proof.context -> Calc.T -> string * Calc.state_post
4.5 val do_next: Calc.T -> string * Calc.state_post
4.6
4.7 -(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
4.8 - datatype expr_val1 =
4.9 +
4.10 + datatype expr_val1 = (* constructors for tests only *)
4.11 Accept_Tac1 of Istate.pstate * Proof.context * Tactic.T
4.12 | Reject_Tac1 of Istate.pstate * Proof.context * Tactic.T
4.13 | Term_Val1 of term;
4.14 +\<^isac_test>\<open>
4.15 val assoc2str: expr_val1 -> string
4.16 +\<close>
4.17 (* ---- for Doc/Lucas-Interpreter ------------------------------------------------------------- *)
4.18 val check_Seq_up: Istate.pstate -> term -> term
4.19 datatype expr_val = Accept_Tac of Tactic.T * Istate.pstate * Proof.context
4.20 @@ -299,9 +301,11 @@
4.21 Tactic.T (* Prog_Tac is associated to Tactic.input *)
4.22 | Term_Val1 of (* Prog_Expr is found and evaluated, scan is continued *)
4.23 term (* value of Prog_Expr, for updating environment *)
4.24 +\<^isac_test>\<open>
4.25 fun assoc2str (Accept_Tac1 _) = "Accept_Tac1"
4.26 | assoc2str (Term_Val1 _) = "Term_Val1"
4.27 | assoc2str (Reject_Tac1 _) = "Reject_Tac1";
4.28 +\<close>
4.29
4.30
4.31 (** check a Prog_Tac: is it associated to Tactic ? **)
5.1 --- a/src/Tools/isac/MathEngBasic/calc-tree-elem.sml Wed Apr 21 11:24:46 2021 +0200
5.2 +++ b/src/Tools/isac/MathEngBasic/calc-tree-elem.sml Wed Apr 21 11:47:33 2021 +0200
5.3 @@ -8,7 +8,9 @@
5.4 type fmz_
5.5 val e_fmz : fmz_ * References_Def.T
5.6 type result
5.7 +\<^isac_test>\<open>
5.8 val res2str : term * term list -> string
5.9 +\<close>
5.10
5.11 datatype safe = Sundef | Safe | Unsafe | Helpless_;
5.12 val safe2str: safe -> string
5.13 @@ -27,7 +29,9 @@
5.14 val e_fmz = ([], References_Def.empty);
5.15
5.16 type result = term * term list
5.17 -fun res2str (t, ts) = pair2str (UnparseC.term t, UnparseC.terms ts); (* for tests only *)
5.18 +\<^isac_test>\<open>
5.19 +fun res2str (t, ts) = pair2str (UnparseC.term t, UnparseC.terms ts);
5.20 +\<close>
5.21
5.22 datatype safe = Sundef | Safe | Unsafe | Helpless_;
5.23 fun safe2str Sundef = "Sundef"
6.1 --- a/src/Tools/isac/MathEngBasic/calculation.sml Wed Apr 21 11:24:46 2021 +0200
6.2 +++ b/src/Tools/isac/MathEngBasic/calculation.sml Wed Apr 21 11:47:33 2021 +0200
6.3 @@ -15,9 +15,10 @@
6.4
6.5 type state_pre
6.6 type state_post
6.7 -(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
6.8 +\<^isac_test>\<open>
6.9 (*val state_pre_empty: state_pre*)
6.10 val state_empty_pre: state_pre
6.11 +\<close>
6.12 (*val state_post_empty: state_post*)
6.13 val state_empty_post: state_post
6.14 end
6.15 @@ -65,7 +66,9 @@
6.16 this has to be addresses in another layer.
6.17 *)
6.18 type state_pre = T * State_Steps.T;
6.19 +\<^isac_test>\<open>
6.20 val state_empty_pre = ((Ctree.EmptyPtree, Pos.e_pos'), [State_Steps.single_empty]);
6.21 +\<close>
6.22
6.23 type state_post =
6.24 State_Steps.T *
6.25 @@ -73,5 +76,6 @@
6.26 T;
6.27 val state_empty_post = ([State_Steps.single_empty], [Pos.e_pos'], (Ctree.EmptyPtree, Pos.e_pos'));
6.28
6.29 +
6.30 (**)end(**)
6.31
7.1 --- a/src/Tools/isac/MathEngBasic/ctree-basic.sml Wed Apr 21 11:24:46 2021 +0200
7.2 +++ b/src/Tools/isac/MathEngBasic/ctree-basic.sml Wed Apr 21 11:47:33 2021 +0200
7.3 @@ -246,9 +246,9 @@
7.4 (* convert a pos from list to string *)
7.5 fun pr_pos ps = (space_implode "." (map string_of_int ps)) ^ ". ";
7.6 (* show hd origin or form only *)
7.7 -fun pr_short p (PblObj _) = pr_pos p ^ " ----- pblobj -----\n" (* for tests only *)
7.8 +fun pr_short p (PblObj _) = pr_pos p ^ " ----- pblobj -----\n"
7.9 | pr_short p (PrfObj {form = form, ...}) = pr_pos p ^ UnparseC.term form ^ "\n";
7.10 -fun pr_ctree f pt = (* for tests only *)
7.11 +fun pr_ctree f pt =
7.12 let
7.13 fun pr_pt _ _ EmptyPtree = ""
7.14 | pr_pt pfn ps (Nd (b, [])) = pfn ps b
8.1 --- a/src/Tools/isac/MathEngBasic/istate-def.sml Wed Apr 21 11:24:46 2021 +0200
8.2 +++ b/src/Tools/isac/MathEngBasic/istate-def.sml Wed Apr 21 11:47:33 2021 +0200
8.3 @@ -56,11 +56,11 @@
8.4 or = ORundef, found_accept = false, assoc = false}
8.5 fun topt2str NONE = "NONE"
8.6 | topt2str (SOME t) = "SOME " ^ UnparseC.term t;
8.7 -fun pstate2str {env, path, eval, form_arg, act_arg, or, found_accept, assoc} = (* for tests only *)
8.8 +fun pstate2str {env, path, eval, form_arg, act_arg, or, found_accept, assoc} =
8.9 "(" ^ Env.env2str env ^ ", " ^ TermC.string_of_path path ^ ", " ^ Rule_Set.id eval ^ ", " ^
8.10 topt2str form_arg ^ ", \n" ^ UnparseC.term act_arg ^ ", " ^ asap2str or ^ ", " ^
8.11 bool2str found_accept ^ ", " ^ bool2str assoc ^ ")";
8.12 -fun pstate2str' {env, path, eval, form_arg, act_arg, or, found_accept, assoc} = (* for tests only *)
8.13 +fun pstate2str' {env, path, eval, form_arg, act_arg, or, found_accept, assoc} =
8.14 "(" ^ Env.env2str' env ^ ", " ^ TermC.string_of_path path ^ ", " ^ Rule_Set.id eval ^ ", " ^
8.15 topt2str form_arg ^ ", " ^ UnparseC.term act_arg ^ ", " ^ asap2str or ^ ", " ^
8.16 bool2str found_accept ^ ", " ^ bool2str assoc ^ ")";
8.17 @@ -84,7 +84,7 @@
8.18 | string_of' (Pstate pst) =
8.19 "Pstate " ^ pstate2str' pst
8.20 | string_of' (RrlsState _) = raise ERROR "istate2str: drop RrlsState"
8.21 -fun istates2str (NONE, NONE) = "(#NONE, #NONE)" (* for tests only *)
8.22 +fun istates2str (NONE, NONE) = "(#NONE, #NONE)"
8.23 | istates2str (NONE, SOME ist) = "(#NONE,\n#SOME " ^ string_of ist ^ ")"
8.24 | istates2str (SOME ist, NONE) = "(#SOME " ^ string_of ist ^ ",\n #NONE)"
8.25 | istates2str (SOME i1, SOME i2) = "(#SOME " ^ string_of i1 ^ ",\n #SOME " ^ string_of i2 ^ ")";
9.1 --- a/src/Tools/isac/Specify/i-model.sml Wed Apr 21 11:24:46 2021 +0200
9.2 +++ b/src/Tools/isac/Specify/i-model.sml Wed Apr 21 11:47:33 2021 +0200
9.3 @@ -66,7 +66,6 @@
9.4 val is_error: feedback -> bool
9.5 val complete': Model_Pattern.T -> O_Model.single -> single
9.6
9.7 -(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
9.8 val is_complete: T -> bool
9.9 val to_p_model: theory -> feedback -> string
9.10 (*/------- rename -------\*)
10.1 --- a/src/Tools/isac/Specify/m-match.sml Wed Apr 21 11:24:46 2021 +0200
10.2 +++ b/src/Tools/isac/Specify/m-match.sml Wed Apr 21 11:47:33 2021 +0200
10.3 @@ -30,10 +30,8 @@
10.4 (*val arguments_msg: Problem.id -> term -> term list -> unit*)
10.5 val arguments_msg: Problem.id -> term -> term list -> unit
10.6
10.7 -(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
10.8 -(*datatype match' = Matches' of P_Model.T | NoMatch' of P_Model.T*)
10.9 - datatype match' = Matches' of P_Model.T | NoMatch' of P_Model.T
10.10 -(*val match_pbl : Formalise.model -> Problem.T -> match'*)
10.11 + datatype match' = (* constructors for tests only *)
10.12 + Matches' of P_Model.T | NoMatch' of P_Model.T
10.13 val match_pbl : Formalise.model -> Problem.T -> match'
10.14 \<^isac_test>\<open>
10.15 (*val matc: theory -> Model_Pattern.T -> term list -> O_Model.T -> O_Model.T*)
11.1 --- a/src/Tools/isac/Specify/o-model.sml Wed Apr 21 11:24:46 2021 +0200
11.2 +++ b/src/Tools/isac/Specify/o-model.sml Wed Apr 21 11:47:33 2021 +0200
11.3 @@ -50,16 +50,18 @@
11.4 (*put add_id into a new auxiliary fun, see ONLY call..*)
11.5 val add_id: 'a list -> (int * 'a) list
11.6 type preori
11.7 -(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
11.8 (*val cpy_nam: Model_Pattern.T -> preori list -> Model_Pattern.single -> preori*)
11.9 val cpy_nam: Model_Pattern.T -> preori list -> Model_Pattern.single -> preori
11.10 val is_copy_named: Model_Pattern.single -> bool
11.11 val is_copy_named_idstr: string -> bool
11.12 +\<^isac_test>\<open>
11.13 val is_copy_named_generating_idstr: string -> bool
11.14 +\<close>
11.15 val is_copy_named_generating: Model_Pattern.single -> bool
11.16
11.17 +\<^isac_test>\<open>
11.18 val preoris2str : preori list -> string
11.19 -(*val getr_ct: theory -> single -> m_field * UnparseC.term_as_string*)
11.20 +\<close>
11.21 val getr_ct: theory -> single -> m_field * UnparseC.term_as_string
11.22
11.23 \<^isac_test>\<open>
12.1 --- a/src/Tools/isac/Specify/p-model.sml Wed Apr 21 11:24:46 2021 +0200
12.2 +++ b/src/Tools/isac/Specify/p-model.sml Wed Apr 21 11:47:33 2021 +0200
12.3 @@ -18,7 +18,6 @@
12.4
12.5 val from : theory -> I_Model.T -> Pre_Conds.T -> T
12.6
12.7 -(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
12.8 val to_list: 'a ppc -> 'a list
12.9 (*/------- rename -------\*)
12.10 (*val mk_delete: theory -> string -> I_Model.feedback -> Tactic.input*)