1.1 --- a/src/Tools/isac/BaseDefinitions/substitution.sml Mon Apr 27 12:36:21 2020 +0200
1.2 +++ b/src/Tools/isac/BaseDefinitions/substitution.sml Mon Apr 27 16:37:56 2020 +0200
1.3 @@ -1,35 +1,40 @@
1.4 (* Title: BaseDefinitions/substitution.sml
1.5 Author: Walther Neuper
1.6 (c) due to copyright terms
1.7 +
1.8 +The variety of substitutions is required by various presentations to the front end;
1.9 +this shall be simplified during the shift to Isabelle/PIDE.
1.10 +
1.11 +Two different formats shall remain, probably:
1.12 +# type input: is what the user sees (pairs of terms)
1.13 +# type as_eqs: a format useful for handling results of equation solving
1.14 *)
1.15 signature SUBSTITUTION =
1.16 sig
1.17 type T = (term * term) list
1.18 val to_string: T -> string
1.19
1.20 - type as_equality = term list (* for Tactic.Substitute: [@{term "bdv = x"}, ...] *)
1.21 + type as_eqs = term list (* for Tactic.Substitute: [@{term "bdv = x"}, ...] *)
1.22 type program = term (* in programs: @{term "[(''bdv_1'', x::real), ..]} *)
1.23 - type as_strings = (string * string) list
1.24 + type input = TermC.as_string list (* by student: ["(''bdv'', x)", ..] *)
1.25 + val input_empty: input
1.26
1.27 - type input = TermC.as_string list (* by student: ["(''bdv'', x)", ..] *)
1.28 - type tyty (* shall become input after generalisation of respective transformations *)
1.29 - val tyty_to_string: string list -> string
1.30 - val tyty_empty: string list
1.31 + type as_string_eqs (* for Tactic.Substitute ["bdv_1 = x", ...] *)
1.32 + val string_eqs_to_string: as_string_eqs -> string
1.33 + val string_eqs_empty: as_string_eqs
1.34
1.35 - val program_to_tyty: program -> tyty
1.36 - val eqs_to_tyty: term list -> tyty
1.37 - val T_to_tyty: T -> tyty
1.38 - val T_from_tyty: theory -> string list -> T
1.39 - val tyty_to_eqs: tyty -> as_equality
1.40 + val T_to_string_eqs: T -> as_string_eqs
1.41 + val T_to_input: T -> input
1.42 + val T_from_string_eqs: theory -> as_string_eqs -> T
1.43 + val T_from_input: theory -> input -> T
1.44
1.45 - val T_to_input: T -> input
1.46 - val T_from_input: theory -> input -> T
1.47 + val input_to_terms: input -> term list
1.48 + val eqs_to_input: as_eqs -> as_string_eqs
1.49 + val program_to_input: program -> input
1.50 val for_bdv: program -> T -> input option * T
1.51 -(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
1.52 - val input_empty: input
1.53 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
1.54 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
1.55 val T_from_program: program -> T
1.56 -(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
1.57 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
1.58 end
1.59
1.60 (**)
1.61 @@ -44,39 +49,41 @@
1.62 linefeed o pair2str o (apsnd UnparseC.term) o (apfst UnparseC.term)))) s;
1.63
1.64 type input = TermC.as_string list;
1.65 -val input_empty = ["(''bdv'', x)"];
1.66 +val input_empty = [];
1.67
1.68 -type tyty = TermC.as_string list;
1.69 -val tyty_empty = []: TermC.as_string list; (* for tests only *)
1.70 -fun tyty_to_string s = strs2str s;
1.71 +type as_string_eqs = TermC.as_string list;
1.72 +val string_eqs_empty = []: TermC.as_string list; (* for tests only *)
1.73 +fun string_eqs_to_string s = strs2str s;
1.74
1.75 -type as_equality = term list;
1.76 +type as_eqs = term list;
1.77 type program = term;
1.78 -type as_strings = (string * string) list;
1.79
1.80 -fun program_to_tyty sub = (sub
1.81 - |> HOLogic.dest_list
1.82 - |> map HOLogic.dest_prod
1.83 - |> map (fn (e1, e2) => (HOLogic.dest_string e1, UnparseC.term e2))
1.84 - |> map (fn (e1, e2) => "(''" ^ e1 ^ "'', " ^ e2 ^ ")"): TermC.as_string list)
1.85 - handle TERM _ => raise TERM ("program_to_tyty: wrong argument ", [sub])
1.86 -val eqs_to_tyty = map UnparseC.term;
1.87 -fun T_to_tyty subst = map UnparseC.term (map HOLogic.mk_eq subst)
1.88 -fun T_from_tyty thy s = map (TermC.dest_equals o (TermC.parse_patt thy)) s;
1.89 -val tyty_to_eqs = map TermC.str2term;
1.90 -
1.91 +fun T_to_string_eqs subst = map UnparseC.term (map HOLogic.mk_eq subst)
1.92 fun T_to_input subst_rew = (subst_rew
1.93 |> map (apsnd UnparseC.term)
1.94 |> map (apfst UnparseC.term)
1.95 |> map (apfst (enclose "''" "''")))
1.96 |> map pair2str
1.97 handle TERM _ => raise TERM ("T_to_input: wrong argument " ^ to_string subst_rew, [])
1.98 +
1.99 +fun T_from_string_eqs thy s = map (TermC.dest_equals o (TermC.parse_patt thy)) s;
1.100 fun T_from_input thy input = (input
1.101 |> map (TermC.parse_patt thy(*FIXME use context, get type of snd (e.g. x,y,z), copy to fst*))
1.102 |> map TermC.isapair2pair
1.103 |> map (apfst HOLogic.dest_string)
1.104 |> map (apfst (fn str => (TermC.mk_Free (str, HOLogic.realT)))))
1.105 handle TERM _ => raise TERM ("T_from_input: wrong argument " ^ strs2str' input, [])
1.106 +
1.107 +val input_to_terms = map TermC.str2term;
1.108 +val eqs_to_input = map UnparseC.term;
1.109 +
1.110 +fun program_to_input sub = (sub
1.111 + |> HOLogic.dest_list
1.112 + |> map HOLogic.dest_prod
1.113 + |> map (fn (e1, e2) => (HOLogic.dest_string e1, UnparseC.term e2))
1.114 + |> map (fn (e1, e2) => "(''" ^ e1 ^ "'', " ^ e2 ^ ")"): TermC.as_string list)
1.115 + handle TERM _ => raise TERM ("program_to_input: wrong argument ", [sub])
1.116 +
1.117 fun T_from_program t = (t
1.118 |> HOLogic.dest_list
1.119 |> map HOLogic.dest_prod
1.120 @@ -85,7 +92,7 @@
1.121 handle TERM _ => raise TERM ("T_from_program: wrong argument ", [t])
1.122
1.123 (* get a substitution for "bdv*" from the current program and environment.
1.124 - returns a substitution: tyty for tac, subst for tac_, i.e. for rewriting *)
1.125 + returns a substitution: as_string_eqs for tac, subst for tac_, i.e. for rewriting *)
1.126 fun for_bdv prog env =
1.127 let
1.128 fun scan (Const _) = NONE
1.129 @@ -101,8 +108,7 @@
1.130 NONE => (NONE: input option, []: subst)
1.131 | SOME tm =>
1.132 let val subst = subst_atomic env tm
1.133 - in (SOME (program_to_tyty subst), T_from_program subst) end
1.134 + in (SOME (program_to_input subst), T_from_program subst) end
1.135 end
1.136 -(*\------- for Subst from Rtools -------/*)
1.137
1.138 (**)end(**)
2.1 --- a/src/Tools/isac/BridgeLibisabelle/datatypes.sml Mon Apr 27 12:36:21 2020 +0200
2.2 +++ b/src/Tools/isac/BridgeLibisabelle/datatypes.sml Mon Apr 27 16:37:56 2020 +0200
2.3 @@ -458,10 +458,10 @@
2.4 subs)) = Subst.T_to_input (map xml_to_sub subs)
2.5 | xml_to_subs x = raise ERROR ("xml_to_subs wrong arg: " ^ xmlstr 0 x)
2.6 fun xml_of_sube sube =
2.7 - XML.Elem (("SUBSTITUTION", []), map xml_of_sub (Subst.T_from_tyty (ThyC.get_theory "Isac_Knowledge") sube))
2.8 + XML.Elem (("SUBSTITUTION", []), map xml_of_sub (Subst.T_from_string_eqs (ThyC.get_theory "Isac_Knowledge") sube))
2.9 fun xml_to_sube
2.10 (XML.Elem (("SUBSTITUTION", []),
2.11 - xml_var_val_pairs)) = Subst.T_to_tyty (map xml_to_sub xml_var_val_pairs)
2.12 + xml_var_val_pairs)) = Subst.T_to_string_eqs (map xml_to_sub xml_var_val_pairs)
2.13 | xml_to_sube x = raise ERROR ("xml_to_sube wrong arg: " ^ xmlstr 0 x)
2.14
2.15 fun thm''2xml j (thm : thm) =
2.16 @@ -522,7 +522,7 @@
2.17 XML.Elem (("THEORY", []), [XML.Text dI]),
2.18 XML.Elem (("PROBLEM", []), [xml_of_strs pI])])
2.19 | xml_of_tac (Tactic.Substitute cterms) =
2.20 - (*Substitute: sube -> tac; Subst.tyty_empty: cterm' list; UNCLEAR HOW TO INPUT ON FRONTEND*)
2.21 + (*Substitute: sube -> tac; Subst.string_eqs_empty: cterm' list; UNCLEAR HOW TO INPUT ON FRONTEND*)
2.22 XML.Elem (("STRINGLISTTACTIC", [("name", "Substitute")]), [xml_of_sube cterms])
2.23 (*----- Rewrite* -----------------------------------------------------*)
2.24 | xml_of_tac (Tactic.Rewrite thm'') =
2.25 @@ -575,7 +575,7 @@
2.26 XML.Elem (("THEORY", []), [XML.Text dI]),
2.27 XML.Elem (("PROBLEM", []), [pI])])) = Tactic.Subproblem (dI, xml_to_strs pI)
2.28 | xml_to_tac
2.29 - (*Substitute: sube -> tac; Subst.tyty_empty: cterm' list; UNCLEAR HOW TO INPUT ON FRONTEND*)
2.30 + (*Substitute: sube -> tac; Subst.string_eqs_empty: cterm' list; UNCLEAR HOW TO INPUT ON FRONTEND*)
2.31 (XML.Elem (("STRINGLISTTACTIC", [
2.32 ("name", "Substitute")]), [cterms])) = Tactic.Substitute (xml_to_sube cterms)
2.33 (*----- Rewrite* -----------------------------------------------------*)
3.1 --- a/src/Tools/isac/Interpret/li-tool.sml Mon Apr 27 12:36:21 2020 +0200
3.2 +++ b/src/Tools/isac/Interpret/li-tool.sml Mon Apr 27 16:37:56 2020 +0200
3.3 @@ -78,16 +78,16 @@
3.4 | tac_from_prog _ thy (Const ("Prog_Tac.Rewrite'_Inst", _) $ sub $ thmID $ _) =
3.5 let
3.6 val tid = HOLogic.dest_string thmID
3.7 - in (Tactic.Rewrite_Inst (Subst.program_to_tyty sub, (tid, ThmC.thm_from_thy thy tid))) end
3.8 + in (Tactic.Rewrite_Inst (Subst.program_to_input sub, (tid, ThmC.thm_from_thy thy tid))) end
3.9 | tac_from_prog _ _ (Const ("Prog_Tac.Rewrite'_Set",_) $ rls $ _) =
3.10 (Tactic.Rewrite_Set (HOLogic.dest_string rls))
3.11 | tac_from_prog _ _ (Const ("Prog_Tac.Rewrite'_Set'_Inst", _) $ sub $ rls $ _) =
3.12 - (Tactic.Rewrite_Set_Inst (Subst.program_to_tyty sub, HOLogic.dest_string rls))
3.13 + (Tactic.Rewrite_Set_Inst (Subst.program_to_input sub, HOLogic.dest_string rls))
3.14 | tac_from_prog _ _ (Const ("Prog_Tac.Calculate", _) $ op_ $ _) =
3.15 (Tactic.Calculate (HOLogic.dest_string op_))
3.16 | tac_from_prog _ _ (Const ("Prog_Tac.Take", _) $ t) = (Tactic.Take (UnparseC.term t))
3.17 | tac_from_prog _ _ (Const ("Prog_Tac.Substitute", _) $ isasub $ _) =
3.18 - (Tactic.Substitute ((Subst.eqs_to_tyty o TermC.isalist2list) isasub))
3.19 + (Tactic.Substitute ((Subst.eqs_to_input o TermC.isalist2list) isasub))
3.20 | tac_from_prog _ thy (Const("Prog_Tac.Check'_elementwise", _) $ _ $
3.21 (Const ("Set.Collect", _) $ Abs (_, _, pred))) =
3.22 (Tactic.Check_elementwise (UnparseC.term_in_thy thy pred))
4.1 --- a/src/Tools/isac/MathEngBasic/tactic.sml Mon Apr 27 12:36:21 2020 +0200
4.2 +++ b/src/Tools/isac/MathEngBasic/tactic.sml Mon Apr 27 16:37:56 2020 +0200
4.3 @@ -55,7 +55,7 @@
4.4 (*Istate.T * ? *)
4.5 Proof.context * (* derived from prog. in ??? *)
4.6 term (* ?UNUSED, e.g."Subproblem\n (''Test'',\n ??.\<^const>String.char.Char ''LINEAR'' ''univariate'' ''equation''\n ''test'')" *)
4.7 - | Substitute' of Rule_Def.rew_ord_ * Rule_Set.T * Subst.as_equality * term * term
4.8 + | Substitute' of Rule_Def.rew_ord_ * Rule_Set.T * Subst.as_eqs * term * term
4.9 | Tac_ of theory * string * string * string
4.10 | Take' of term
4.11 val string_of: T -> string
4.12 @@ -101,7 +101,7 @@
4.13 | Specify_Theory of ThyC.id
4.14 | Subproblem of ThyC.id * Problem.id
4.15
4.16 - | Substitute of Subst.tyty
4.17 + | Substitute of Subst.input
4.18 | Tac of string
4.19 | Take of TermC.as_string | Take_Inst of TermC.as_string
4.20 val input_to_string : input -> string
4.21 @@ -193,7 +193,7 @@
4.22 | Specify_Theory of ThyC.id
4.23 | Subproblem of ThyC.id * Problem.id (* WN0509 drop *)
4.24
4.25 - | Substitute of Subst.tyty
4.26 + | Substitute of Subst.input
4.27 | Tac of string (* WN0509 drop *)
4.28 | Take of TermC.as_string | Take_Inst of TermC.as_string
4.29
4.30 @@ -228,7 +228,7 @@
4.31 | End_Detail => "End_Detail"
4.32 | Derive rls' => "Derive " ^ rls'
4.33 | Calculate op_ => "Calculate " ^ op_
4.34 - | Substitute sube => "Substitute " ^ Subst.tyty_to_string sube
4.35 + | Substitute sube => "Substitute " ^ Subst.string_eqs_to_string sube
4.36 | Apply_Assumption ct's => "Apply_Assumption " ^ strs2str ct's
4.37
4.38 | Take cterm' => "Take " ^ quote cterm'
4.39 @@ -402,7 +402,7 @@
4.40 | Substitute' of
4.41 Rule_Def.rew_ord_ * (* for re-calculation *)
4.42 Rule_Set.T * (* for re-calculation *)
4.43 - Subst.as_equality * (* the 'substitution': terms of type bool *)
4.44 + Subst.as_eqs * (* the 'substitution': terms of type bool *)
4.45 term * (* to be substituted into *)
4.46 term (* resulting from the substitution *)
4.47 | Tac_ of theory * string * string * string
4.48 @@ -481,7 +481,7 @@
4.49
4.50 | input_from_T (Or_to_List' _) = Or_to_List
4.51 | input_from_T (Take' term) = Take (UnparseC.term term)
4.52 - | input_from_T (Substitute' (_, _, subte, _, _)) = Substitute (Subst.eqs_to_tyty subte)
4.53 + | input_from_T (Substitute' (_, _, subte, _, _)) = Substitute (Subst.eqs_to_input subte)
4.54 | input_from_T (Tac_ (_, _, id, _)) = Tac id
4.55
4.56 | input_from_T (Subproblem' ((domID, pblID, _), _, _, _,_ ,_)) = Subproblem (domID, pblID)
5.1 --- a/src/Tools/isac/Specify/appl.sml Mon Apr 27 12:36:21 2020 +0200
5.2 +++ b/src/Tools/isac/Specify/appl.sml Mon Apr 27 16:37:56 2020 +0200
5.3 @@ -395,22 +395,22 @@
5.4 Frm => get_obj g_form pt p
5.5 | Res => (fst o (get_obj g_result pt)) p
5.6 | _ => error ("applicable_in: call by " ^ pos'2str (p, p_));
5.7 - val {rew_ord',erls,...} = Specify.get_met (get_obj g_metID pt pp)
5.8 - val subte = Subst.tyty_to_eqs sube
5.9 - val subst = Subst.T_from_tyty thy sube
5.10 + val {rew_ord', erls, ...} = Specify.get_met (get_obj g_metID pt pp)
5.11 + val subte = Subst.input_to_terms sube
5.12 + val subst = Subst.T_from_string_eqs thy sube
5.13 val ro = Rewrite_Ord.assoc_rew_ord rew_ord'
5.14 in
5.15 if foldl and_ (true, map TermC.contains_Var subte)
5.16 then (*1*)
5.17 let val f' = subst_atomic subst f
5.18 in if f = f'
5.19 - then Notappl (Subst.tyty_to_string sube^" not applicable")
5.20 + then Notappl (Subst.string_eqs_to_string sube ^ " not applicable")
5.21 else Appl (Tactic.Substitute' (ro, erls, subte, f, f'))
5.22 end
5.23 else (*2*)
5.24 case Rewrite.rewrite_terms_ thy ro erls subte f of
5.25 SOME (f', _) => Appl (Tactic.Substitute' (ro, erls, subte, f, f'))
5.26 - | NONE => Notappl (Subst.tyty_to_string sube ^ " not applicable")
5.27 + | NONE => Notappl (Subst.string_eqs_to_string sube ^ " not applicable")
5.28 end
5.29 | applicable_in _ _ (Tactic.Apply_Assumption cts') =
5.30 error ("applicable_in: not impl. for " ^ Tactic.input_to_string (Tactic.Apply_Assumption cts'))
6.1 --- a/src/Tools/isac/Specify/generate.sml Mon Apr 27 12:36:21 2020 +0200
6.2 +++ b/src/Tools/isac/Specify/generate.sml Mon Apr 27 16:37:56 2020 +0200
6.3 @@ -300,7 +300,7 @@
6.4 | generate1 (Tactic.Substitute' (_, _, subte, t, t')) l (pt, (p, _)) =
6.5 let
6.6 val (pt,c) =
6.7 - cappend_atomic pt p l t (Tactic.Substitute (Subst.eqs_to_tyty subte)) (t',[]) Complete
6.8 + cappend_atomic pt p l t (Tactic.Substitute (Subst.eqs_to_input subte)) (t',[]) Complete
6.9 in ((p, Res), c, FormKF (UnparseC.term t'), pt)
6.10 end
6.11 | generate1 (Tactic.Tac_ (_, f, id, f')) l (pt, (p, _)) =
7.1 --- a/test/Tools/isac/BaseDefinitions/substitution.sml Mon Apr 27 12:36:21 2020 +0200
7.2 +++ b/test/Tools/isac/BaseDefinitions/substitution.sml Mon Apr 27 16:37:56 2020 +0200
7.3 @@ -7,20 +7,23 @@
7.4 "-----------------------------------------------------------------------------";
7.5 "table of contents -----------------------------------------------------------";
7.6 "-----------------------------------------------------------------------------";
7.7 -"-------- fun program_to_tyty ------------------------------------------------";
7.8 +"-------- fun program_to_input -----------------------------------------------";
7.9 "-------- fun T_from_input ---------------------------------------------------";
7.10 "-------- fun T_from_program -------------------------------------------------";
7.11 -"-------- fun T_to_strings ---------------------------------------------------";
7.12 +"-------- fun T_to_input -----------------------------------------------------";
7.13 +"-------- fun T_to_string_eqs ------------------------------------------------";
7.14 +"-------- fun T_from_string_eqs ----------------------------------------------";
7.15 +"-------- fun input_to_terms -------------------------------------------------";
7.16 "-------- build fun for_bdv --------------------------------------------------";
7.17 "-----------------------------------------------------------------------------";
7.18 "-----------------------------------------------------------------------------";
7.19
7.20 -"-------- fun program_to_tyty ------------------------------------------------";
7.21 -"-------- fun program_to_tyty ------------------------------------------------";
7.22 -"-------- fun program_to_tyty ------------------------------------------------";
7.23 +"-------- fun program_to_input -----------------------------------------------";
7.24 +"-------- fun program_to_input -----------------------------------------------";
7.25 +"-------- fun program_to_input -----------------------------------------------";
7.26 val subst_prog = @{term "[(''bdv_1'', x::real), (''bdv_2'', y::real), (''bdv_3'', z::real)]"};
7.27 -if Subst.program_to_tyty subst_prog = ["(''bdv_1'', x)", "(''bdv_2'', y)", "(''bdv_3'', z)"] then ()
7.28 -else error "subst'_to_sube changed";
7.29 +if Subst.program_to_input subst_prog = ["(''bdv_1'', x)", "(''bdv_2'', y)", "(''bdv_3'', z)"] then ()
7.30 +else error "program_to_input changed";
7.31
7.32 "-------- fun T_from_input -----------------------------------------------------";
7.33 "-------- fun T_from_input -----------------------------------------------------";
7.34 @@ -41,20 +44,57 @@
7.35 (Free ("bdv_3", _), Free ("z", _))] => ()
7.36 | _ => error "Subst.T_from_program changed";
7.37
7.38 -"-------- fun T_to_strings -----------------------------------------------------";
7.39 -"-------- fun T_to_strings -----------------------------------------------------";
7.40 -"-------- fun T_to_strings -----------------------------------------------------";
7.41 +"-------- fun T_to_input -----------------------------------------------------";
7.42 +"-------- fun T_to_input -----------------------------------------------------";
7.43 +"-------- fun T_to_input -----------------------------------------------------";
7.44 val subst_rew =
7.45 [(@{term "bdv_1 :: real"}, @{term "x :: real"}),
7.46 (@{term "bdv_2 :: real"}, @{term "y :: real"}),
7.47 (@{term "bdv_3 :: real"}, @{term "z :: real"})];
7.48 -if Subst.T_to_strings subst_rew = ["(''bdv_1'', x)", "(''bdv_2'', y)", "(''bdv_3'', z)"]then ()
7.49 +if Subst.T_to_input subst_rew = ["(''bdv_1'', x)", "(''bdv_2'', y)", "(''bdv_3'', z)"] then ()
7.50 else error "T_to_strings changed";
7.51
7.52 +"-------- fun T_to_string_eqs ------------------------------------------------";
7.53 +"-------- fun T_to_string_eqs ------------------------------------------------";
7.54 +"-------- fun T_to_string_eqs ------------------------------------------------";
7.55 +val subst =
7.56 + [(@{term "bdv_1 :: real"}, @{term "x :: real"}),
7.57 + (@{term "bdv_2 :: real"}, @{term "y :: real"}),
7.58 + (@{term "xxx :: real"}, @{term "aaa + (111 :: real)"})];
7.59 +
7.60 +if Subst.T_to_string_eqs subst = ["bdv_1 = x", "bdv_2 = y", "xxx = aaa + 111"] then ()
7.61 +else error "T_to_tyty changed";
7.62 +
7.63 +"-------- fun T_from_string_eqs ----------------------------------------------";
7.64 +"-------- fun T_from_string_eqs ----------------------------------------------";
7.65 +"-------- fun T_from_string_eqs ----------------------------------------------";
7.66 +val string_eqs = ["bdv_1 = x", "bdv_2 = y", "xxx = aaa + 111"];
7.67 +
7.68 +case Subst.T_from_string_eqs @{theory} string_eqs of
7.69 + [(Free ("bdv_1", _), Free ("x", _)),
7.70 + (Free ("bdv_2", _), Free ("y", _)),
7.71 + (Free ("xxx", _), Const ("Groups.plus_class.plus", _) $ Free ("aaa", _) $ Free ("111", _))] => ()
7.72 +| _ => error "";
7.73 +
7.74 +"-------- fun input_to_terms -------------------------------------------------";
7.75 +"-------- fun input_to_terms -------------------------------------------------";
7.76 +"-------- fun input_to_terms -------------------------------------------------";
7.77 +Subst.input_to_terms: Subst.input -> term list;
7.78 +val input = ["(''bdv_1'', x)", "(''bdv_2'', y)", "(aaa, bbb + 2)"];
7.79 +
7.80 +case Subst.input_to_terms input of
7.81 + [Const ("Product_Type.Pair", _) $
7.82 + (Const ("List.list.Cons", _) $ (Const ("String.char.Char", _) $
7.83 + Const ("HOL.False", _) $ _ $ _ $ _ $ _ $ _ $ _ $ _) $ _) $
7.84 + Free ("x", _),
7.85 + _,
7.86 + Const ("Product_Type.Pair", _) $ Free ("aaa", _) $ _] => ()
7.87 +| _ => error "input_to_eqs CHANGED";
7.88 +
7.89 "-------- build fun for_bdv --------------------------------------------------";
7.90 "-------- build fun for_bdv --------------------------------------------------";
7.91 "-------- build fun for_bdv --------------------------------------------------";
7.92 -Subst.program_to_tyty: Subst.program -> string list;
7.93 +Subst.program_to_input: Subst.program -> string list;
7.94
7.95 val {scr = Prog prog, ...} = get_met ["diff", "differentiate_on_R"];
7.96 val env = [(str2term "v_v", str2term "x")] : Subst.T;
7.97 @@ -73,5 +113,5 @@
7.98 val subst = tm |> subst_atomic env;
7.99 if UnparseC.term tm = "[(''bdv'', v_v)]" then () else error "for_bdv changed 1";
7.100
7.101 -if Subst.program_to_tyty subst = (["(''bdv'', x)"] : Subst.input) then ()
7.102 +if Subst.program_to_input subst = (["(''bdv'', x)"] : Subst.input) then ()
7.103 else error "for_bdv changed 2";
8.1 --- a/test/Tools/isac/BridgeLibisabelle/datatypes.sml Mon Apr 27 12:36:21 2020 +0200
8.2 +++ b/test/Tools/isac/BridgeLibisabelle/datatypes.sml Mon Apr 27 16:37:56 2020 +0200
8.3 @@ -268,7 +268,7 @@
8.4 Refine_Tacitly: Problem.id -> Tactic.input;
8.5 Specify_Problem: Problem.id -> Tactic.input;
8.6 Specify_Method: Method.id -> Tactic.input;
8.7 -Substitute: Subst.tyty -> Tactic.input;; (* Substitute: sube -> tac; Subst.tyty_empty: TermC.as_string list; UNCLEAR HOW TO INPUT *)
8.8 +Substitute: Subst.input -> Tactic.input;; (* Substitute: sube -> tac; Subst.string_eqs_empty: TermC.as_string list; UNCLEAR HOW TO INPUT *)
8.9 Check_Postcond: Problem.id -> Tactic.input;
8.10
8.11 Apply_Method: Method.id -> Tactic.input;
8.12 @@ -290,7 +290,7 @@
8.13 (* Note: tacs Substitute, Rewrite_Inst* have different substitutions,
8.14 while input in frontend is not yet clear: *)
8.15 Rewrite_Inst: Subst.input * ThmC.T -> Tactic.input;
8.16 -Substitute : Subst.tyty -> Tactic.input;
8.17 +Substitute : Subst.input -> Tactic.input;
8.18
8.19 Subst.input_empty: Subst.input;
8.20 Subst.input_empty: Subst.input;
8.21 @@ -332,9 +332,9 @@
8.22 if (UnparseC.term o Thm.prop_of) term = "d_d ?bdv (sin ?u) = cos ?u * d_d ?bdv ?u"
8.23 then () else error "xml_to_tac Rewrite_Inst CHANGED";
8.24
8.25 -val sube = ["(bdv_1 = xxx)", "(bdv_2 = yyy)"]: Subst.tyty;
8.26 -Subst.tyty_empty: TermC.as_string list;
8.27 -Subst.tyty_empty: Subst.tyty;
8.28 +val sube = ["(bdv_1 = xxx)", "(bdv_2 = yyy)"]: Subst.input;
8.29 +Subst.string_eqs_empty: TermC.as_string list;
8.30 +Subst.string_eqs_empty: Subst.input;
8.31 xml_of_sube sube;(*
8.32 <SUBSTITUTION>
8.33 <PAIR>
9.1 --- a/test/Tools/isac/Knowledge/algein.sml Mon Apr 27 12:36:21 2020 +0200
9.2 +++ b/test/Tools/isac/Knowledge/algein.sml Mon Apr 27 16:37:56 2020 +0200
9.3 @@ -110,9 +110,9 @@
9.4
9.5 (*testing code in ME/appl.sml*)
9.6 val sube = ["?a1 = (3::real)"];
9.7 -val subte = Subst.tyty_to_eqs sube;
9.8 +val subte = Subst.input_to_terms sube;
9.9 UnparseC.terms_short subte = "[?a1 = 3]"; (* = true*)
9.10 -val subst = Subst.T_from_tyty thy sube;
9.11 +val subst = Subst.T_from_string_eqs thy sube;
9.12 foldl and_ (true, map contains_Var subte);
9.13
9.14 val t'' = subst_atomic subst t';
10.1 --- a/test/Tools/isac/Test_Isac_Short.thy Mon Apr 27 12:36:21 2020 +0200
10.2 +++ b/test/Tools/isac/Test_Isac_Short.thy Mon Apr 27 16:37:56 2020 +0200
10.3 @@ -191,7 +191,7 @@
10.4 (*called by Know_Store*)
10.5 ML_file "BaseDefinitions/calcelems.sml"
10.6 ML_file "BaseDefinitions/termC.sml"
10.7 - ML_file substitution.sml
10.8 + ML_file "BaseDefinitions/substitution.sml"
10.9 ML_file "BaseDefinitions/contextC.sml"
10.10 ML_file "BaseDefinitions/environment.sml"
10.11 ML_file "BaseDefinitions/kestore.sml" (* setup in ADDTEST/accumulate-val/lucas_interpreter.sml*)