1.1 --- a/src/Tools/isac/BaseDefinitions/BaseDefinitions.thy Fri Apr 24 09:01:48 2020 +0200
1.2 +++ b/src/Tools/isac/BaseDefinitions/BaseDefinitions.thy Mon Apr 27 12:36:21 2020 +0200
1.3 @@ -8,6 +8,7 @@
1.4 begin
1.5 ML_file calcelems.sml
1.6 ML_file termC.sml
1.7 + ML_file substitution.sml
1.8 ML_file contextC.sml
1.9 ML_file environment.sml
1.10
2.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
2.2 +++ b/src/Tools/isac/BaseDefinitions/substitution.sml Mon Apr 27 12:36:21 2020 +0200
2.3 @@ -0,0 +1,108 @@
2.4 +(* Title: BaseDefinitions/substitution.sml
2.5 + Author: Walther Neuper
2.6 + (c) due to copyright terms
2.7 +*)
2.8 +signature SUBSTITUTION =
2.9 +sig
2.10 + type T = (term * term) list
2.11 + val to_string: T -> string
2.12 +
2.13 + type as_equality = term list (* for Tactic.Substitute: [@{term "bdv = x"}, ...] *)
2.14 + type program = term (* in programs: @{term "[(''bdv_1'', x::real), ..]} *)
2.15 + type as_strings = (string * string) list
2.16 +
2.17 + type input = TermC.as_string list (* by student: ["(''bdv'', x)", ..] *)
2.18 + type tyty (* shall become input after generalisation of respective transformations *)
2.19 + val tyty_to_string: string list -> string
2.20 + val tyty_empty: string list
2.21 +
2.22 + val program_to_tyty: program -> tyty
2.23 + val eqs_to_tyty: term list -> tyty
2.24 + val T_to_tyty: T -> tyty
2.25 + val T_from_tyty: theory -> string list -> T
2.26 + val tyty_to_eqs: tyty -> as_equality
2.27 +
2.28 + val T_to_input: T -> input
2.29 + val T_from_input: theory -> input -> T
2.30 + val for_bdv: program -> T -> input option * T
2.31 +(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
2.32 + val input_empty: input
2.33 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
2.34 + val T_from_program: program -> T
2.35 +(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
2.36 +end
2.37 +
2.38 +(**)
2.39 +structure Subst(**): SUBSTITUTION(**) =
2.40 +struct
2.41 +(**)
2.42 +
2.43 +type T = (term * term) list;
2.44 +fun to_string s =
2.45 + (strs2str o
2.46 + (map (
2.47 + linefeed o pair2str o (apsnd UnparseC.term) o (apfst UnparseC.term)))) s;
2.48 +
2.49 +type input = TermC.as_string list;
2.50 +val input_empty = ["(''bdv'', x)"];
2.51 +
2.52 +type tyty = TermC.as_string list;
2.53 +val tyty_empty = []: TermC.as_string list; (* for tests only *)
2.54 +fun tyty_to_string s = strs2str s;
2.55 +
2.56 +type as_equality = term list;
2.57 +type program = term;
2.58 +type as_strings = (string * string) list;
2.59 +
2.60 +fun program_to_tyty sub = (sub
2.61 + |> HOLogic.dest_list
2.62 + |> map HOLogic.dest_prod
2.63 + |> map (fn (e1, e2) => (HOLogic.dest_string e1, UnparseC.term e2))
2.64 + |> map (fn (e1, e2) => "(''" ^ e1 ^ "'', " ^ e2 ^ ")"): TermC.as_string list)
2.65 + handle TERM _ => raise TERM ("program_to_tyty: wrong argument ", [sub])
2.66 +val eqs_to_tyty = map UnparseC.term;
2.67 +fun T_to_tyty subst = map UnparseC.term (map HOLogic.mk_eq subst)
2.68 +fun T_from_tyty thy s = map (TermC.dest_equals o (TermC.parse_patt thy)) s;
2.69 +val tyty_to_eqs = map TermC.str2term;
2.70 +
2.71 +fun T_to_input subst_rew = (subst_rew
2.72 + |> map (apsnd UnparseC.term)
2.73 + |> map (apfst UnparseC.term)
2.74 + |> map (apfst (enclose "''" "''")))
2.75 + |> map pair2str
2.76 + handle TERM _ => raise TERM ("T_to_input: wrong argument " ^ to_string subst_rew, [])
2.77 +fun T_from_input thy input = (input
2.78 + |> map (TermC.parse_patt thy(*FIXME use context, get type of snd (e.g. x,y,z), copy to fst*))
2.79 + |> map TermC.isapair2pair
2.80 + |> map (apfst HOLogic.dest_string)
2.81 + |> map (apfst (fn str => (TermC.mk_Free (str, HOLogic.realT)))))
2.82 + handle TERM _ => raise TERM ("T_from_input: wrong argument " ^ strs2str' input, [])
2.83 +fun T_from_program t = (t
2.84 + |> HOLogic.dest_list
2.85 + |> map HOLogic.dest_prod
2.86 + |> map (apfst HOLogic.dest_string))
2.87 + |> map (apfst (fn e1 => (TermC.mk_Free (e1, HOLogic.realT))))
2.88 + handle TERM _ => raise TERM ("T_from_program: wrong argument ", [t])
2.89 +
2.90 +(* get a substitution for "bdv*" from the current program and environment.
2.91 + returns a substitution: tyty for tac, subst for tac_, i.e. for rewriting *)
2.92 +fun for_bdv prog env =
2.93 + let
2.94 + fun scan (Const _) = NONE
2.95 + | scan (Free _) = NONE
2.96 + | scan (Var _) = NONE
2.97 + | scan (Bound _) = NONE
2.98 + | scan (t as Const ("List.list.Cons", _) $ (Const ("Product_Type.Pair", _) $ _ $ _) $ _) =
2.99 + if TermC.is_bdv_subst t then SOME t else NONE
2.100 + | scan (Abs (_, _, body)) = scan body
2.101 + | scan (t1 $ t2) = case scan t1 of NONE => scan t2 | SOME subst => SOME subst
2.102 + in
2.103 + case scan prog of
2.104 + NONE => (NONE: input option, []: subst)
2.105 + | SOME tm =>
2.106 + let val subst = subst_atomic env tm
2.107 + in (SOME (program_to_tyty subst), T_from_program subst) end
2.108 + end
2.109 +(*\------- for Subst from Rtools -------/*)
2.110 +
2.111 +(**)end(**)
3.1 --- a/src/Tools/isac/BridgeLibisabelle/datatypes.sml Fri Apr 24 09:01:48 2020 +0200
3.2 +++ b/src/Tools/isac/BridgeLibisabelle/datatypes.sml Mon Apr 27 12:36:21 2020 +0200
3.3 @@ -43,7 +43,7 @@
3.4 val scr2xml : int -> Program.T -> xml
3.5 val spec2xml : int -> Spec.T -> xml
3.6 val sub2xml : int -> Term.term * Term.term -> xml
3.7 - val subs2xml : int -> Selem.subs -> xml
3.8 + val subs2xml : int -> Subst.input -> xml
3.9 val subst2xml : int -> subst -> xml
3.10 val tac2xml : int -> Tactic.input -> xml
3.11 val tacs2xml : int -> Tactic.input list -> xml
3.12 @@ -451,17 +451,17 @@
3.13 XML.Elem (("VARIABLE", []), [id]),
3.14 XML.Elem (("VALUE", []), [value])])) = (xml_to_term id, xml_to_term value)
3.15 | xml_to_sub x = raise ERROR ("xml_to_sub wrong arg: " ^ xmlstr 0 x)
3.16 -fun xml_of_subs (subs : Selem.subs) =
3.17 - XML.Elem (("SUBSTITUTION", []), map xml_of_sub (Selem.subs2subst (ThyC.get_theory "Isac_Knowledge") subs))
3.18 +fun xml_of_subs (subs : Subst.input) =
3.19 + XML.Elem (("SUBSTITUTION", []), map xml_of_sub (Subst.T_from_input (ThyC.get_theory "Isac_Knowledge") subs))
3.20 fun xml_to_subs
3.21 (XML.Elem (("SUBSTITUTION", []),
3.22 - subs)) = Selem.subst2subs (map xml_to_sub subs)
3.23 + subs)) = Subst.T_to_input (map xml_to_sub subs)
3.24 | xml_to_subs x = raise ERROR ("xml_to_subs wrong arg: " ^ xmlstr 0 x)
3.25 fun xml_of_sube sube =
3.26 - XML.Elem (("SUBSTITUTION", []), map xml_of_sub (Selem.sube2subst (ThyC.get_theory "Isac_Knowledge") sube))
3.27 + XML.Elem (("SUBSTITUTION", []), map xml_of_sub (Subst.T_from_tyty (ThyC.get_theory "Isac_Knowledge") sube))
3.28 fun xml_to_sube
3.29 (XML.Elem (("SUBSTITUTION", []),
3.30 - xml_var_val_pairs)) = Selem.subst2sube (map xml_to_sub xml_var_val_pairs)
3.31 + xml_var_val_pairs)) = Subst.T_to_tyty (map xml_to_sub xml_var_val_pairs)
3.32 | xml_to_sube x = raise ERROR ("xml_to_sube wrong arg: " ^ xmlstr 0 x)
3.33
3.34 fun thm''2xml j (thm : thm) =
3.35 @@ -522,7 +522,7 @@
3.36 XML.Elem (("THEORY", []), [XML.Text dI]),
3.37 XML.Elem (("PROBLEM", []), [xml_of_strs pI])])
3.38 | xml_of_tac (Tactic.Substitute cterms) =
3.39 - (*Substitute: sube -> tac; e_sube: cterm' list; UNCLEAR HOW TO INPUT ON FRONTEND*)
3.40 + (*Substitute: sube -> tac; Subst.tyty_empty: cterm' list; UNCLEAR HOW TO INPUT ON FRONTEND*)
3.41 XML.Elem (("STRINGLISTTACTIC", [("name", "Substitute")]), [xml_of_sube cterms])
3.42 (*----- Rewrite* -----------------------------------------------------*)
3.43 | xml_of_tac (Tactic.Rewrite thm'') =
3.44 @@ -575,7 +575,7 @@
3.45 XML.Elem (("THEORY", []), [XML.Text dI]),
3.46 XML.Elem (("PROBLEM", []), [pI])])) = Tactic.Subproblem (dI, xml_to_strs pI)
3.47 | xml_to_tac
3.48 - (*Substitute: sube -> tac; e_sube: cterm' list; UNCLEAR HOW TO INPUT ON FRONTEND*)
3.49 + (*Substitute: sube -> tac; Subst.tyty_empty: cterm' list; UNCLEAR HOW TO INPUT ON FRONTEND*)
3.50 (XML.Elem (("STRINGLISTTACTIC", [
3.51 ("name", "Substitute")]), [cterms])) = Tactic.Substitute (xml_to_sube cterms)
3.52 (*----- Rewrite* -----------------------------------------------------*)
4.1 --- a/src/Tools/isac/BridgeLibisabelle/interface.sml Fri Apr 24 09:01:48 2020 +0200
4.2 +++ b/src/Tools/isac/BridgeLibisabelle/interface.sml Mon Apr 27 12:36:21 2020 +0200
4.3 @@ -678,7 +678,7 @@
4.4 val fillforms = Error_Pattern.find_fill_patterns (pt, pos) errpatID
4.5 in
4.6 case filter ((curry op = fillpatID) o
4.7 - (#1: (Error_Pattern_Def.fill_in_id * term * thm * (Selem.subs option) -> Error_Pattern_Def.fill_in_id))) fillforms of
4.8 + (#1: (Error_Pattern_Def.fill_in_id * term * thm * (Subst.input option) -> Error_Pattern_Def.fill_in_id))) fillforms of
4.9 (_, fillform, thm, sube_opt) :: _ =>
4.10 let
4.11 val (pt, pos') = Generate.generate_inconsistent_rew (sube_opt, ThmC.of_thm thm)
5.1 --- a/src/Tools/isac/Interpret/error-pattern.sml Fri Apr 24 09:01:48 2020 +0200
5.2 +++ b/src/Tools/isac/Interpret/error-pattern.sml Mon Apr 27 12:36:21 2020 +0200
5.3 @@ -25,9 +25,9 @@
5.4 val find_fill_patterns: Calc.T -> id -> record list
5.5 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
5.6 val check_for': term * term -> subst -> id * term -> Rule_Set.T -> id option
5.7 - val fill_from_store: Selem.subs option * (term * term) list -> term -> id -> thm ->
5.8 + val fill_from_store: Subst.input option * (term * term) list -> term -> id -> thm ->
5.9 record list
5.10 - val fill_form: Selem.subs option * (term * term) list -> thm * term -> id -> fill_in ->
5.11 + val fill_form: Subst.input option * (term * term) list -> thm * term -> id -> fill_in ->
5.12 record option
5.13 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
5.14 end
5.15 @@ -43,7 +43,7 @@
5.16
5.17 type fill_in_id = Error_Pattern_Def.fill_in_id;
5.18 type fill_in = Error_Pattern_Def.fill_in;
5.19 -type record = (fill_in_id * term * thm * Selem.subs option);
5.20 +type record = (fill_in_id * term * thm * Subst.input option);
5.21
5.22 (*
5.23 check if (agreed result, input formula) matches the error pattern "pat" modulo simplifier rls
5.24 @@ -73,7 +73,7 @@
5.25 *)
5.26 fun check_for (res, inf) (prog, env) (errpats, rls) =
5.27 let
5.28 - val (_, subst) = Rtools.get_bdv_subst prog env
5.29 + val (_, subst) = Subst.for_bdv prog env
5.30 fun scan (_, [], _) = NONE
5.31 | scan (id, T :: errpats, _) =
5.32 case check_for' (res, inf) subst (id, T) rls of
5.33 @@ -117,7 +117,7 @@
5.34 {errpats, scr = Rule.Prog prog, ...} => (errpats, prog)
5.35 | _ => raise ERROR "find_fill_patterns: uncovered case of get_met"
5.36 val {env, ...} = Ctree.get_istate_LI pt pos |> Istate.the_pstate
5.37 - val subst = Rtools.get_bdv_subst prog env
5.38 + val subst = Subst.for_bdv prog env
5.39 val errpatthms = errpats
5.40 |> filter ((curry op = id) o (#1: Error_Pattern_Def.T -> Error_Pattern_Def.id))
5.41 |> map (#3: Error_Pattern_Def.T -> thm list)
6.1 --- a/src/Tools/isac/Interpret/li-tool.sml Fri Apr 24 09:01:48 2020 +0200
6.2 +++ b/src/Tools/isac/Interpret/li-tool.sml Mon Apr 27 12:36:21 2020 +0200
6.3 @@ -78,16 +78,16 @@
6.4 | tac_from_prog _ thy (Const ("Prog_Tac.Rewrite'_Inst", _) $ sub $ thmID $ _) =
6.5 let
6.6 val tid = HOLogic.dest_string thmID
6.7 - in (Tactic.Rewrite_Inst (Selem.subst'_to_sube sub, (tid, ThmC.thm_from_thy thy tid))) end
6.8 + in (Tactic.Rewrite_Inst (Subst.program_to_tyty sub, (tid, ThmC.thm_from_thy thy tid))) end
6.9 | tac_from_prog _ _ (Const ("Prog_Tac.Rewrite'_Set",_) $ rls $ _) =
6.10 (Tactic.Rewrite_Set (HOLogic.dest_string rls))
6.11 | tac_from_prog _ _ (Const ("Prog_Tac.Rewrite'_Set'_Inst", _) $ sub $ rls $ _) =
6.12 - (Tactic.Rewrite_Set_Inst (Selem.subst'_to_sube sub, HOLogic.dest_string rls))
6.13 + (Tactic.Rewrite_Set_Inst (Subst.program_to_tyty sub, HOLogic.dest_string rls))
6.14 | tac_from_prog _ _ (Const ("Prog_Tac.Calculate", _) $ op_ $ _) =
6.15 (Tactic.Calculate (HOLogic.dest_string op_))
6.16 | tac_from_prog _ _ (Const ("Prog_Tac.Take", _) $ t) = (Tactic.Take (UnparseC.term t))
6.17 | tac_from_prog _ _ (Const ("Prog_Tac.Substitute", _) $ isasub $ _) =
6.18 - (Tactic.Substitute ((Selem.subte2sube o TermC.isalist2list) isasub))
6.19 + (Tactic.Substitute ((Subst.eqs_to_tyty o TermC.isalist2list) isasub))
6.20 | tac_from_prog _ thy (Const("Prog_Tac.Check'_elementwise", _) $ _ $
6.21 (Const ("Set.Collect", _) $ Abs (_, _, pred))) =
6.22 (Tactic.Check_elementwise (UnparseC.term_in_thy thy pred))
7.1 --- a/src/Tools/isac/Interpret/rewtools.sml Fri Apr 24 09:01:48 2020 +0200
7.2 +++ b/src/Tools/isac/Interpret/rewtools.sml Mon Apr 27 12:36:21 2020 +0200
7.3 @@ -9,7 +9,6 @@
7.4 sig
7.5
7.6 (*/------- for error-fill-pattern -------\*)
7.7 - val get_bdv_subst : term -> (term * term) list -> Selem.subs option * subst
7.8 val thy_containing_thm : string -> string * string
7.9 val thy_containing_rls : ThyC.id -> Rule_Set.id -> string * ThyC.id
7.10 val thy_containing_cal : ThyC.id -> Exec_Def.prog_calcID -> string * string
7.11 @@ -39,8 +38,8 @@
7.12 val thms_of_rls : Rule_Set.T -> Rule.rule list
7.13 val theID2filename : Thy_Html.theID -> Celem.filename
7.14 val no_thycontext : Check_Unique.id -> bool
7.15 - val subs_from : Istate.T -> 'a -> Check_Unique.id -> Selem.subs
7.16 - val guh2rewtac : Check_Unique.id -> Selem.subs -> Tactic.input
7.17 + val subs_from : Istate.T -> 'a -> Check_Unique.id -> Subst.input
7.18 + val guh2rewtac : Check_Unique.id -> Subst.input -> Tactic.input
7.19 val get_tac_checked : Ctree.ctree -> Pos.pos' -> Tactic.input
7.20 val context_thy : Calc.T -> Tactic.input -> contthy
7.21 val distinct_Thm : Rule.rule list -> Rule.rule list
7.22 @@ -238,7 +237,7 @@
7.23 val thm_deriv = Thm.get_name_hint thm
7.24 val pp = Ctree.par_pblobj pt p
7.25 val thy' = Ctree.get_obj Ctree.g_domID pt pp
7.26 - val subst = Selem.subs2subst (ThyC.get_theory thy') subs
7.27 + val subst = Subst.T_from_input (ThyC.get_theory thy') subs
7.28 val thminst = TermC.inst_bdv subst ((Eval.norm o #prop o Thm.rep_thm) thm)
7.29 val f = case p_ of
7.30 Pos.Frm => Ctree.get_obj Ctree.g_form pt p
7.31 @@ -328,12 +327,12 @@
7.32 | atomic_appl_tacs thy ro erls f (Tactic.Rewrite thm'') =
7.33 try_rew thy (ro, Rewrite_Ord.assoc_rew_ord ro) erls [] f (Rule.Thm thm'')
7.34 | atomic_appl_tacs thy ro erls f (Tactic.Rewrite_Inst (subs, thm'')) =
7.35 - try_rew thy (ro, Rewrite_Ord.assoc_rew_ord ro) erls (Selem.subs2subst thy subs) f (Rule.Thm thm'')
7.36 + try_rew thy (ro, Rewrite_Ord.assoc_rew_ord ro) erls (Subst.T_from_input thy subs) f (Rule.Thm thm'')
7.37
7.38 | atomic_appl_tacs thy _ _ f (Tactic.Rewrite_Set rls') =
7.39 filter_appl_rews thy [] f (assoc_rls rls')
7.40 | atomic_appl_tacs thy _ _ f (Tactic.Rewrite_Set_Inst (subs, rls')) =
7.41 - filter_appl_rews thy (Selem.subs2subst thy subs) f (assoc_rls rls')
7.42 + filter_appl_rews thy (Subst.T_from_input thy subs) f (assoc_rls rls')
7.43 | atomic_appl_tacs _ _ _ _ tac =
7.44 (tracing ("### atomic_appl_tacs: not impl. for tac = '" ^ Tactic.input_to_string tac ^ "'"); []);
7.45
7.46 @@ -431,7 +430,7 @@
7.47 let
7.48 val formal_arg = TermC.str2term "v_"
7.49 val value = subst_atomic env formal_arg
7.50 - in ["(''bdv''," ^ UnparseC.term value ^ ")"] : Selem.subs end
7.51 + in ["(''bdv''," ^ UnparseC.term value ^ ")"] : Subst.input end
7.52 else []
7.53 end
7.54 | "Rulesets" =>
7.55 @@ -443,31 +442,11 @@
7.56 let
7.57 val formal_arg = TermC.str2term "v_"
7.58 val value = subst_atomic env formal_arg
7.59 - in ["(''bdv''," ^ UnparseC.term value ^ ")"] : Selem.subs end
7.60 + in ["(''bdv''," ^ UnparseC.term value ^ ")"] : Subst.input end
7.61 else []
7.62 end
7.63 | str => error ("subs_from: uncovered case with " ^ str)
7.64 end
7.65 | subs_from _ _ guh = error ("subs_from: uncovered case with " ^ guh)
7.66
7.67 -(* get a substitution for "bdv*" from the current program and environment.
7.68 - returns a substitution: sube for tac, subst for tac_, i.e. for rewriting *)
7.69 -fun get_bdv_subst prog env =
7.70 - let
7.71 - fun scan (Const _) = NONE
7.72 - | scan (Free _) = NONE
7.73 - | scan (Var _) = NONE
7.74 - | scan (Bound _) = NONE
7.75 - | scan (t as Const ("List.list.Cons", _) $ (Const ("Product_Type.Pair", _) $ _ $ _) $ _) =
7.76 - if TermC.is_bdv_subst t then SOME t else NONE
7.77 - | scan (Abs (_, _, body)) = scan body
7.78 - | scan (t1 $ t2) = case scan t1 of NONE => scan t2 | SOME subst => SOME subst
7.79 - in
7.80 - case scan prog of
7.81 - NONE => (NONE: Selem.subs option, []: subst)
7.82 - | SOME tm =>
7.83 - let val subst = subst_atomic env tm
7.84 - in (SOME (Selem.subst'_to_sube subst), Selem.subst'_to_subst subst) end
7.85 - end
7.86 -
7.87 (**)end(**)
8.1 --- a/src/Tools/isac/MathEngBasic/specification-elems.sml Fri Apr 24 09:01:48 2020 +0200
8.2 +++ b/src/Tools/isac/MathEngBasic/specification-elems.sml Mon Apr 27 12:36:21 2020 +0200
8.3 @@ -10,29 +10,9 @@
8.4 type fmz_
8.5 type result
8.6 val res2str : term * term list -> string
8.7 - type subs (* substitution as seen by learner. rename stubst_user ["(''bdv'', x)"]*)
8.8 - type sube (* = subs. delete ! = stubst_user *)
8.9 - type subte (* _sub_stitution as _t_erms of _e_qualities: revise ! [bdv = x] *)
8.10 - type subst' (* substitution in isac-programs; rename subst_prog [(bdv, x)] *)
8.11 -(*type subst for rewriting, in Rule (+?Isabelle); rename subst_rew [(bools, x)] *)
8.12 - (* TODO use these types in functions below and elsewhere; rename below according to types *)
8.13 - val subst'_to_sube : subst' -> TermC.as_string list (* e.g. rename to subst_user_of_prog *)
8.14 - val subst_to_subst' : subst -> subst'
8.15 - val subst'_to_subst : subst' -> (term * term) list
8.16 - val sube2str : TermC.as_string list -> string
8.17 - val sube2subst : theory -> TermC.as_string list -> (term * term) list
8.18 - val sube2subte : TermC.as_string list -> term list
8.19 - val subs2subst : theory -> TermC.as_string list -> (term * term) list
8.20 - val subst2sube : (term * term) list -> TermC.as_string list (* for datatypes.sml *)
8.21 - val subst2subs : (term * term) list -> TermC.as_string list
8.22 - val subst2subs' : (term * term) list -> (string * string) list
8.23 - val subte2sube : term list -> TermC.as_string list
8.24
8.25 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
8.26 val e_fmz : fmz_ * Spec.T (* for datatypes.sml *)
8.27 - val e_sube : TermC.as_string list
8.28 - val e_subs : string list
8.29 - val subte2subst : term list -> (term * term) list
8.30 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
8.31 (* NONE *)
8.32 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
8.33 @@ -45,10 +25,6 @@
8.34 structure Selem(**): SPECIFY_ELEMENT(**) =
8.35 struct
8.36
8.37 -fun subst2str s =
8.38 - (strs2str o
8.39 - (map (
8.40 - linefeed o pair2str o (apsnd UnparseC.term) o (apfst UnparseC.term)))) s;
8.41 type fmz_ = TermC.as_string list;
8.42 (* a formalization of an example contains data
8.43 sufficient for mechanically finding the solution for the example.
8.44 @@ -59,54 +35,4 @@
8.45 type result = term * term list
8.46 fun res2str (t, ts) = pair2str (UnparseC.term t, UnparseC.terms ts); (* for tests only *)
8.47
8.48 -type subs = TermC.as_string list; (* substitution as seen by learner in tactics, in programs, etc.
8.49 - questionable design. rename to stubst_user *)
8.50 -val e_subs = ["(''bdv'', x)"]; (* for tests only *)
8.51 -
8.52 -(* argument type of tac Rewrite_Inst *)
8.53 -type sube = TermC.as_string list; (* = subs. delete *)
8.54 -val e_sube = []: TermC.as_string list; (* for tests only *)
8.55 -fun sube2str s = strs2str s;
8.56 -
8.57 -type subte = term list; (* _sub_stitution as _t_erms of _e_qualities: revise ! *)
8.58 -
8.59 -type subst' = term; (* substitution in isac-programs. rename to subst_prog
8.60 - is "(char list * term) list", where term is Free ("xxx", _)
8.61 - e.g. @{term "[(''bdv_1'', x::real), (''bdv_2'', y::real), (''bdv_3'', z::real)]"} *)
8.62 -fun subst'_to_sube sub = (sub
8.63 - |> HOLogic.dest_list
8.64 - |> map HOLogic.dest_prod
8.65 - |> map (fn (e1, e2) => (HOLogic.dest_string e1, UnparseC.term e2))
8.66 - |> map (fn (e1, e2) => "(''" ^ e1 ^ "'', " ^ e2 ^ ")"): TermC.as_string list)
8.67 - handle TERM _ => raise TERM ("subst'_to_sube: wrong argument ", [sub])
8.68 -fun subst_to_subst' subst = subst
8.69 - |> map (apfst TermC.free2str)
8.70 - |> map (apfst HOLogic.mk_string)
8.71 - |> map HOLogic.mk_prod
8.72 - |> HOLogic.mk_list (HOLogic.mk_prodT (HOLogic.stringT, HOLogic.realT (*FIXME: 'a*)))
8.73 -fun subst'_to_subst t = (t
8.74 - |> HOLogic.dest_list
8.75 - |> map HOLogic.dest_prod
8.76 - |> map (apfst HOLogic.dest_string))
8.77 - |> map (apfst (fn e1 => (TermC.mk_Free (e1, HOLogic.realT))))
8.78 - handle TERM _ => raise TERM ("subst'_to_subst: wrong argument ", [t])
8.79 -val subte2sube = map UnparseC.term;
8.80 -fun subst2subs subst_rew = (subst_rew
8.81 - |> map (apsnd UnparseC.term)
8.82 - |> map (apfst UnparseC.term)
8.83 - |> map (apfst (enclose "''" "''")))
8.84 - |> map pair2str
8.85 - handle TERM _ => raise TERM ("subst2subs: wrong argument " ^ subst2str subst_rew, [])
8.86 -fun subst2sube subst = map UnparseC.term (map HOLogic.mk_eq subst)
8.87 -val subst2subs' = map ((apfst UnparseC.term) o (apsnd UnparseC.term));
8.88 -fun subs2subst thy subs = (subs
8.89 - |> map (TermC.parse_patt thy(*FIXME use context, get type of snd (e.g. x,y,z), copy to fst*))
8.90 - |> map TermC.isapair2pair
8.91 - |> map (apfst HOLogic.dest_string)
8.92 - |> map (apfst (fn str => (TermC.mk_Free (str, HOLogic.realT)))))
8.93 - handle TERM _ => raise TERM ("subs2subst: wrong argument " ^ strs2str' subs, [])
8.94 -fun sube2subst thy s = map (TermC.dest_equals o (TermC.parse_patt thy)) s;
8.95 -val sube2subte = map TermC.str2term;
8.96 -val subte2subst = map HOLogic.dest_eq;
8.97 -
8.98 -end
8.99 +(**)end(**)
9.1 --- a/src/Tools/isac/MathEngBasic/tactic.sml Fri Apr 24 09:01:48 2020 +0200
9.2 +++ b/src/Tools/isac/MathEngBasic/tactic.sml Mon Apr 27 12:36:21 2020 +0200
9.3 @@ -55,7 +55,7 @@
9.4 (*Istate.T * ? *)
9.5 Proof.context * (* derived from prog. in ??? *)
9.6 term (* ?UNUSED, e.g."Subproblem\n (''Test'',\n ??.\<^const>String.char.Char ''LINEAR'' ''univariate'' ''equation''\n ''test'')" *)
9.7 - | Substitute' of Rule_Def.rew_ord_ * Rule_Set.T * Selem.subte * term * term
9.8 + | Substitute' of Rule_Def.rew_ord_ * Rule_Set.T * Subst.as_equality * term * term
9.9 | Tac_ of theory * string * string * string
9.10 | Take' of term
9.11 val string_of: T -> string
9.12 @@ -79,7 +79,7 @@
9.13
9.14 | Derive of Rule_Set.id
9.15 | Detail_Set of Rule_Set.id
9.16 - | Detail_Set_Inst of Selem.subs * Rule_Set.id
9.17 + | Detail_Set_Inst of Subst.input * Rule_Set.id
9.18 | End_Detail
9.19
9.20 | Empty_Tac
9.21 @@ -92,16 +92,16 @@
9.22 | Refine_Tacitly of Problem.id
9.23
9.24 | Rewrite of ThmC.T
9.25 - | Rewrite_Inst of Selem.subs * ThmC.T
9.26 + | Rewrite_Inst of Subst.input * ThmC.T
9.27 | Rewrite_Set of Rule_Set.id
9.28 - | Rewrite_Set_Inst of Selem.subs * Rule_Set.id
9.29 + | Rewrite_Set_Inst of Subst.input * Rule_Set.id
9.30
9.31 | Specify_Method of Method.id
9.32 | Specify_Problem of Problem.id
9.33 | Specify_Theory of ThyC.id
9.34 | Subproblem of ThyC.id * Problem.id
9.35
9.36 - | Substitute of Selem.sube
9.37 + | Substitute of Subst.tyty
9.38 | Tac of string
9.39 | Take of TermC.as_string | Take_Inst of TermC.as_string
9.40 val input_to_string : input -> string
9.41 @@ -167,7 +167,7 @@
9.42
9.43 | Derive of Rule_Set.id (* WN0509 drop *)
9.44 | Detail_Set of Rule_Set.id (* WN0509 drop *)
9.45 - | Detail_Set_Inst of Selem.subs * Rule_Set.id (* WN0509 drop *)
9.46 + | Detail_Set_Inst of Subst.input * Rule_Set.id (* WN0509 drop *)
9.47 | End_Detail (* WN0509 drop *)
9.48
9.49 | Empty_Tac
9.50 @@ -184,16 +184,16 @@
9.51 (where user-views can show both or only one of (thmID, thm)),
9.52 and thm is created from ThmID by assoc_thm'' when entering isabisac *)
9.53 | Rewrite of ThmC.T
9.54 - | Rewrite_Inst of Selem.subs * ThmC.T
9.55 + | Rewrite_Inst of Subst.input * ThmC.T
9.56 | Rewrite_Set of Rule_Set.id
9.57 - | Rewrite_Set_Inst of Selem.subs * Rule_Set.id
9.58 + | Rewrite_Set_Inst of Subst.input * Rule_Set.id
9.59
9.60 | Specify_Method of Method.id
9.61 | Specify_Problem of Problem.id
9.62 | Specify_Theory of ThyC.id
9.63 | Subproblem of ThyC.id * Problem.id (* WN0509 drop *)
9.64
9.65 - | Substitute of Selem.sube
9.66 + | Substitute of Subst.tyty
9.67 | Tac of string (* WN0509 drop *)
9.68 | Take of TermC.as_string | Take_Inst of TermC.as_string
9.69
9.70 @@ -227,8 +227,8 @@
9.71 | Detail_Set_Inst (subs, rls) => "Detail_Set_Inst " ^ pair2str (subs2str subs, quote rls)
9.72 | End_Detail => "End_Detail"
9.73 | Derive rls' => "Derive " ^ rls'
9.74 - | Calculate op_ => "Calculate " ^ op_
9.75 - | Substitute sube => "Substitute " ^ Selem.sube2str sube
9.76 + | Calculate op_ => "Calculate " ^ op_
9.77 + | Substitute sube => "Substitute " ^ Subst.tyty_to_string sube
9.78 | Apply_Assumption ct's => "Apply_Assumption " ^ strs2str ct's
9.79
9.80 | Take cterm' => "Take " ^ quote cterm'
9.81 @@ -314,10 +314,10 @@
9.82 fun rule2tac thy _ (Rule.Eval (opID, _)) = Calculate (assoc_calc thy opID)
9.83 | rule2tac _ [] (Rule.Thm thm'') = Rewrite thm''
9.84 | rule2tac _ subst (Rule.Thm thm'') =
9.85 - Rewrite_Inst (Selem.subst2subs subst, thm'')
9.86 + Rewrite_Inst (Subst.T_to_input subst, thm'')
9.87 | rule2tac _ [] (Rule.Rls_ rls) = Rewrite_Set (Rule_Set.id rls)
9.88 | rule2tac _ subst (Rule.Rls_ rls) =
9.89 - Rewrite_Set_Inst (Selem.subst2subs subst, (Rule_Set.id rls))
9.90 + Rewrite_Set_Inst (Subst.T_to_input subst, (Rule_Set.id rls))
9.91 | rule2tac _ _ rule =
9.92 error ("rule2tac: called with \"" ^ Rule.to_string rule ^ "\"");
9.93
9.94 @@ -402,7 +402,7 @@
9.95 | Substitute' of
9.96 Rule_Def.rew_ord_ * (* for re-calculation *)
9.97 Rule_Set.T * (* for re-calculation *)
9.98 - Selem.subte * (* the 'substitution': terms of type bool *)
9.99 + Subst.as_equality * (* the 'substitution': terms of type bool *)
9.100 term * (* to be substituted into *)
9.101 term (* resulting from the substitution *)
9.102 | Tac_ of theory * string * string * string
9.103 @@ -466,22 +466,22 @@
9.104 | input_from_T (Specify_Method' (dI, _, _)) = Specify_Method dI
9.105
9.106 | input_from_T (Rewrite' (_, _, _, _, thm, _, _)) = Rewrite thm
9.107 - | input_from_T (Rewrite_Inst' (_, _, _, _, sub, thm, _, _)) = Rewrite_Inst (Selem.subst2subs sub, thm)
9.108 + | input_from_T (Rewrite_Inst' (_, _, _, _, sub, thm, _, _)) = Rewrite_Inst (Subst.T_to_input sub, thm)
9.109
9.110 | input_from_T (Rewrite_Set' (_, _, rls, _, _)) = Rewrite_Set (Rule_Set.id rls)
9.111 | input_from_T (Detail_Set' (_, _, rls, _, _)) = Detail_Set (Rule_Set.id rls)
9.112
9.113 | input_from_T (Rewrite_Set_Inst' (_, _, sub, rls, _, _)) =
9.114 - Rewrite_Set_Inst (Selem.subst2subs sub, Rule_Set.id rls)
9.115 + Rewrite_Set_Inst (Subst.T_to_input sub, Rule_Set.id rls)
9.116 | input_from_T (Detail_Set_Inst' (_, _, sub, rls, _, _)) =
9.117 - Detail_Set_Inst (Selem.subst2subs sub, Rule_Set.id rls)
9.118 + Detail_Set_Inst (Subst.T_to_input sub, Rule_Set.id rls)
9.119
9.120 | input_from_T (Calculate' (_, op_, _, _)) = Calculate (op_)
9.121 | input_from_T (Check_elementwise' (_, pred, _)) = Check_elementwise pred
9.122
9.123 | input_from_T (Or_to_List' _) = Or_to_List
9.124 | input_from_T (Take' term) = Take (UnparseC.term term)
9.125 - | input_from_T (Substitute' (_, _, subte, _, _)) = Substitute (Selem.subte2sube subte)
9.126 + | input_from_T (Substitute' (_, _, subte, _, _)) = Substitute (Subst.eqs_to_tyty subte)
9.127 | input_from_T (Tac_ (_, _, id, _)) = Tac id
9.128
9.129 | input_from_T (Subproblem' ((domID, pblID, _), _, _, _,_ ,_)) = Subproblem (domID, pblID)
10.1 --- a/src/Tools/isac/Specify/appl.sml Fri Apr 24 09:01:48 2020 +0200
10.2 +++ b/src/Tools/isac/Specify/appl.sml Mon Apr 27 12:36:21 2020 +0200
10.3 @@ -261,7 +261,7 @@
10.4 | _ => error ("applicable_in: call by " ^ pos'2str (p, p_));
10.5 in
10.6 let
10.7 - val subst = Selem.subs2subst thy subs;
10.8 + val subst = Subst.T_from_input thy subs;
10.9 in
10.10 case Rewrite.rewrite_inst_ thy (Rewrite_Ord.assoc_rew_ord ro') erls false subst (snd thm'') f of
10.11 SOME (f',asm) =>
10.12 @@ -300,7 +300,7 @@
10.13 val f = case p_ of Frm => get_obj g_form pt p
10.14 | Res => (fst o (get_obj g_result pt)) p
10.15 | _ => error ("applicable_in: call by " ^ pos'2str (p, p_));
10.16 - val subst = Selem.subs2subst thy subs
10.17 + val subst = Subst.T_from_input thy subs
10.18 in
10.19 case Rewrite.rewrite_set_inst_ thy false subst (assoc_rls rls) f of
10.20 SOME (f', asm)
10.21 @@ -320,7 +320,7 @@
10.22 Frm => (get_obj g_form pt p, p)
10.23 | Res => ((fst o (get_obj g_result pt)) p, lev_on p)
10.24 | _ => error ("applicable_in: call by " ^ pos'2str (p, p_));
10.25 - val subst = Selem.subs2subst thy subs;
10.26 + val subst = Subst.T_from_input thy subs;
10.27 in
10.28 case Rewrite.rewrite_set_inst_ thy (*put_asm*)false subst (assoc_rls rls) f of
10.29 SOME (f',asm)
10.30 @@ -396,21 +396,21 @@
10.31 | Res => (fst o (get_obj g_result pt)) p
10.32 | _ => error ("applicable_in: call by " ^ pos'2str (p, p_));
10.33 val {rew_ord',erls,...} = Specify.get_met (get_obj g_metID pt pp)
10.34 - val subte = Selem.sube2subte sube
10.35 - val subst = Selem.sube2subst thy sube
10.36 + val subte = Subst.tyty_to_eqs sube
10.37 + val subst = Subst.T_from_tyty thy sube
10.38 val ro = Rewrite_Ord.assoc_rew_ord rew_ord'
10.39 in
10.40 if foldl and_ (true, map TermC.contains_Var subte)
10.41 then (*1*)
10.42 let val f' = subst_atomic subst f
10.43 in if f = f'
10.44 - then Notappl (Selem.sube2str sube^" not applicable")
10.45 + then Notappl (Subst.tyty_to_string sube^" not applicable")
10.46 else Appl (Tactic.Substitute' (ro, erls, subte, f, f'))
10.47 end
10.48 else (*2*)
10.49 case Rewrite.rewrite_terms_ thy ro erls subte f of
10.50 SOME (f', _) => Appl (Tactic.Substitute' (ro, erls, subte, f, f'))
10.51 - | NONE => Notappl (Selem.sube2str sube ^ " not applicable")
10.52 + | NONE => Notappl (Subst.tyty_to_string sube ^ " not applicable")
10.53 end
10.54 | applicable_in _ _ (Tactic.Apply_Assumption cts') =
10.55 error ("applicable_in: not impl. for " ^ Tactic.input_to_string (Tactic.Apply_Assumption cts'))
11.1 --- a/src/Tools/isac/Specify/generate.sml Fri Apr 24 09:01:48 2020 +0200
11.2 +++ b/src/Tools/isac/Specify/generate.sml Mon Apr 27 12:36:21 2020 +0200
11.3 @@ -22,7 +22,7 @@
11.4 theory -> Tactic.T -> Pos.pos' -> Ctree.ctree -> Pos.pos' * Pos.pos' list * mout * Ctree.ctree
11.5 val generate : (Tactic.input * Tactic.T * (Pos.pos' * (Istate_Def.T * Proof.context))) list ->
11.6 Ctree.ctree * Pos.pos' list * Pos.pos' -> Ctree.ctree * Pos.pos' list * Pos.pos'
11.7 - val generate_inconsistent_rew : Selem.subs option * ThmC.T -> term -> Istate_Def.T * Proof.context ->
11.8 + val generate_inconsistent_rew : Subst.input option * ThmC.T -> term -> Istate_Def.T * Proof.context ->
11.9 Pos.pos' -> Ctree.ctree -> Calc.T
11.10 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
11.11 val mout2str : mout -> string
11.12 @@ -50,7 +50,7 @@
11.13 let
11.14 val thy = ThyC.get_theory "Isac_Knowledge"
11.15 val rls' = assoc_rls rls
11.16 - val v = case Selem.subs2subst thy subs of
11.17 + val v = case Subst.T_from_input thy subs of
11.18 (_, v) :: _ => v (*...we suppose the substitution of only ONE bound variable*)
11.19 | _ => raise ERROR "init_istate: uncovered case"
11.20 val prog = Auto_Prog.gen thy t rls'
11.21 @@ -225,7 +225,7 @@
11.22 | generate1 (Tactic.Rewrite_Inst' (_, _, _, _, subs', thm', f, (f', asm))) (is, ctxt) (pt, (p, _)) =
11.23 let
11.24 val (pt, c) = cappend_atomic pt p (is, ctxt) f
11.25 - (Tactic.Rewrite_Inst (Selem.subst2subs subs', thm')) (f',asm) Complete;
11.26 + (Tactic.Rewrite_Inst (Subst.T_to_input subs', thm')) (f',asm) Complete;
11.27 val pt = update_branch pt p TransitiveB
11.28 in
11.29 ((p, Res), c, FormKF (UnparseC.term f'), pt)
11.30 @@ -240,7 +240,7 @@
11.31 | generate1 (Tactic.Rewrite_Set_Inst' (_, _, subs', rls', f, (f', asm))) (is, ctxt) (pt, (p, _)) =
11.32 let
11.33 val (pt, c) = cappend_atomic pt p (is, ctxt) f
11.34 - (Tactic.Rewrite_Set_Inst (Selem.subst2subs subs', Rule_Set.id rls')) (f', asm) Complete
11.35 + (Tactic.Rewrite_Set_Inst (Subst.T_to_input subs', Rule_Set.id rls')) (f', asm) Complete
11.36 val pt = update_branch pt p TransitiveB
11.37 in
11.38 ((p, Res), c, FormKF (UnparseC.term f'), pt)
11.39 @@ -249,7 +249,7 @@
11.40 let
11.41 val (pt, _) = cappend_form pt p (is, ctxt) f
11.42 val pt = update_branch pt p TransitiveB
11.43 - val is = init_istate (Tactic.Rewrite_Set_Inst (Selem.subst2subs subs, Rule_Set.id rls)) f
11.44 + val is = init_istate (Tactic.Rewrite_Set_Inst (Subst.T_to_input subs, Rule_Set.id rls)) f
11.45 val tac_ = Tactic.Apply_Method' (Method.id_empty, SOME TermC.empty (*t ..has not been declared*), is, ctxt)
11.46 val pos' = ((lev_on o lev_dn) p, Frm)
11.47 in
11.48 @@ -300,7 +300,7 @@
11.49 | generate1 (Tactic.Substitute' (_, _, subte, t, t')) l (pt, (p, _)) =
11.50 let
11.51 val (pt,c) =
11.52 - cappend_atomic pt p l t (Tactic.Substitute (Selem.subte2sube subte)) (t',[]) Complete
11.53 + cappend_atomic pt p l t (Tactic.Substitute (Subst.eqs_to_tyty subte)) (t',[]) Complete
11.54 in ((p, Res), c, FormKF (UnparseC.term t'), pt)
11.55 end
11.56 | generate1 (Tactic.Tac_ (_, f, id, f')) l (pt, (p, _)) =
12.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
12.2 +++ b/test/Tools/isac/BaseDefinitions/substitution.sml Mon Apr 27 12:36:21 2020 +0200
12.3 @@ -0,0 +1,77 @@
12.4 +(* Title: BaseDefinitions/substitution.sml
12.5 + Author: Walther Neuper
12.6 + (c) due to copyright terms
12.7 +*)
12.8 +
12.9 +"-----------------------------------------------------------------------------";
12.10 +"-----------------------------------------------------------------------------";
12.11 +"table of contents -----------------------------------------------------------";
12.12 +"-----------------------------------------------------------------------------";
12.13 +"-------- fun program_to_tyty ------------------------------------------------";
12.14 +"-------- fun T_from_input ---------------------------------------------------";
12.15 +"-------- fun T_from_program -------------------------------------------------";
12.16 +"-------- fun T_to_strings ---------------------------------------------------";
12.17 +"-------- build fun for_bdv --------------------------------------------------";
12.18 +"-----------------------------------------------------------------------------";
12.19 +"-----------------------------------------------------------------------------";
12.20 +
12.21 +"-------- fun program_to_tyty ------------------------------------------------";
12.22 +"-------- fun program_to_tyty ------------------------------------------------";
12.23 +"-------- fun program_to_tyty ------------------------------------------------";
12.24 +val subst_prog = @{term "[(''bdv_1'', x::real), (''bdv_2'', y::real), (''bdv_3'', z::real)]"};
12.25 +if Subst.program_to_tyty subst_prog = ["(''bdv_1'', x)", "(''bdv_2'', y)", "(''bdv_3'', z)"] then ()
12.26 +else error "subst'_to_sube changed";
12.27 +
12.28 +"-------- fun T_from_input -----------------------------------------------------";
12.29 +"-------- fun T_from_input -----------------------------------------------------";
12.30 +"-------- fun T_from_input -----------------------------------------------------";
12.31 +case Subst.T_from_input @{theory} ["(''bdv_1'', x)", "(''bdv_2'', y)", "(''bdv_3'', z)"] of
12.32 + [(Free ("bdv_1", _), Free ("x", _)),
12.33 + (Free ("bdv_2", _), Free ("y", _)),
12.34 + (Free ("bdv_3", _), Free ("z", _))] => ()
12.35 +| _ => error "T_from_input changed";
12.36 +
12.37 +"-------- fun T_from_program ------------------------------------------------";
12.38 +"-------- fun T_from_program ------------------------------------------------";
12.39 +"-------- fun T_from_program ------------------------------------------------";
12.40 +val t = @{term "[(''bdv_1'', x::real), (''bdv_2'', y::real), (''bdv_3'', z::real)]"};
12.41 +case Subst.T_from_program t of
12.42 + [(Free ("bdv_1", _), Free ("x", _)),
12.43 + (Free ("bdv_2", _), Free ("y", _)),
12.44 + (Free ("bdv_3", _), Free ("z", _))] => ()
12.45 +| _ => error "Subst.T_from_program changed";
12.46 +
12.47 +"-------- fun T_to_strings -----------------------------------------------------";
12.48 +"-------- fun T_to_strings -----------------------------------------------------";
12.49 +"-------- fun T_to_strings -----------------------------------------------------";
12.50 +val subst_rew =
12.51 + [(@{term "bdv_1 :: real"}, @{term "x :: real"}),
12.52 + (@{term "bdv_2 :: real"}, @{term "y :: real"}),
12.53 + (@{term "bdv_3 :: real"}, @{term "z :: real"})];
12.54 +if Subst.T_to_strings subst_rew = ["(''bdv_1'', x)", "(''bdv_2'', y)", "(''bdv_3'', z)"]then ()
12.55 +else error "T_to_strings changed";
12.56 +
12.57 +"-------- build fun for_bdv --------------------------------------------------";
12.58 +"-------- build fun for_bdv --------------------------------------------------";
12.59 +"-------- build fun for_bdv --------------------------------------------------";
12.60 +Subst.program_to_tyty: Subst.program -> string list;
12.61 +
12.62 +val {scr = Prog prog, ...} = get_met ["diff", "differentiate_on_R"];
12.63 +val env = [(str2term "v_v", str2term "x")] : Subst.T;
12.64 +
12.65 +"~~~~~ fun for_bdv, args:"; val (prog, env) = (prog, env);
12.66 + fun scan (Const _) = NONE
12.67 + | scan (Free _) = NONE
12.68 + | scan (Var _) = NONE
12.69 + | scan (Bound _) = NONE
12.70 + | scan (t as Const ("List.list.Cons", _) $ (Const ("Product_Type.Pair", _) $ _ $ _) $ _) =
12.71 + if TermC.is_bdv_subst t then SOME t else NONE
12.72 + | scan (Abs (_, _, body)) = scan body
12.73 + | scan (t1 $ t2) = case scan t1 of NONE => scan t2 | SOME subst => SOME subst
12.74 +
12.75 +val SOME tm = scan prog;
12.76 +val subst = tm |> subst_atomic env;
12.77 +if UnparseC.term tm = "[(''bdv'', v_v)]" then () else error "for_bdv changed 1";
12.78 +
12.79 +if Subst.program_to_tyty subst = (["(''bdv'', x)"] : Subst.input) then ()
12.80 +else error "for_bdv changed 2";
13.1 --- a/test/Tools/isac/BridgeLibisabelle/datatypes.sml Fri Apr 24 09:01:48 2020 +0200
13.2 +++ b/test/Tools/isac/BridgeLibisabelle/datatypes.sml Mon Apr 27 12:36:21 2020 +0200
13.3 @@ -142,7 +142,7 @@
13.4 ". (/THEOREM)\n" ^
13.5 "(/REWRITETACTIC)\n" then () else error "xml_of_tac Rewrite CHANGED";
13.6
13.7 -Rewrite_Inst: subs * ThmC.T -> Tactic.input;
13.8 +Rewrite_Inst: Subst.input * ThmC.T -> Tactic.input;
13.9 val tac = Rewrite_Inst(["(''bdv'', x)"], ("refl", @{thm refl}));
13.10 if xmlstr 0 (xml_of_tac tac) =
13.11 "(REWRITEINSTTACTIC name=Rewrite_Inst)\n" ^
13.12 @@ -195,7 +195,7 @@
13.13 ". simplify\n" ^
13.14 "(/REWRITESETTACTIC)\n" then () else error "xml_of_tac Rewrite_Set CHANGED";
13.15
13.16 -Rewrite_Set_Inst: subs * Rule_Set.id -> Tactic.input;
13.17 +Rewrite_Set_Inst: Subst.input * Rule_Set.id -> Tactic.input;
13.18 val tac = Rewrite_Set_Inst(["(''bdv'', x)"], "simplify");
13.19 if xmlstr 0 (xml_of_tac tac) =
13.20 "(REWRITESETINSTTACTIC name=Rewrite_Set_Inst)\n" ^
13.21 @@ -268,7 +268,7 @@
13.22 Refine_Tacitly: Problem.id -> Tactic.input;
13.23 Specify_Problem: Problem.id -> Tactic.input;
13.24 Specify_Method: Method.id -> Tactic.input;
13.25 -Substitute: sube -> Tactic.input;; (* Substitute: sube -> tac; e_sube: TermC.as_string list; UNCLEAR HOW TO INPUT *)
13.26 +Substitute: Subst.tyty -> Tactic.input;; (* Substitute: sube -> tac; Subst.tyty_empty: TermC.as_string list; UNCLEAR HOW TO INPUT *)
13.27 Check_Postcond: Problem.id -> Tactic.input;
13.28
13.29 Apply_Method: Method.id -> Tactic.input;
13.30 @@ -289,11 +289,11 @@
13.31 "----------- fun xml_of_tac: different substitutions converted to same XML ---------------------";
13.32 (* Note: tacs Substitute, Rewrite_Inst* have different substitutions,
13.33 while input in frontend is not yet clear: *)
13.34 -Rewrite_Inst: subs * ThmC.T -> Tactic.input;
13.35 -Substitute : sube -> Tactic.input;
13.36 +Rewrite_Inst: Subst.input * ThmC.T -> Tactic.input;
13.37 +Substitute : Subst.tyty -> Tactic.input;
13.38
13.39 -e_subs: TermC.as_string list;
13.40 -e_subs: subs;
13.41 +Subst.input_empty: Subst.input;
13.42 +Subst.input_empty: Subst.input;
13.43 val subs = ["(''bdv_1'', xxx)","(''bdv_2'', yyy)"]: TermC.as_string list;
13.44 xml_of_subs subs;(*
13.45 <SUBSTITUTION>
13.46 @@ -332,9 +332,9 @@
13.47 if (UnparseC.term o Thm.prop_of) term = "d_d ?bdv (sin ?u) = cos ?u * d_d ?bdv ?u"
13.48 then () else error "xml_to_tac Rewrite_Inst CHANGED";
13.49
13.50 -val sube = ["(bdv_1 = xxx)", "(bdv_2 = yyy)"]: sube;
13.51 -e_sube: TermC.as_string list;
13.52 -e_sube: sube;
13.53 +val sube = ["(bdv_1 = xxx)", "(bdv_2 = yyy)"]: Subst.tyty;
13.54 +Subst.tyty_empty: TermC.as_string list;
13.55 +Subst.tyty_empty: Subst.tyty;
13.56 xml_of_sube sube;(*
13.57 <SUBSTITUTION>
13.58 <PAIR>
14.1 --- a/test/Tools/isac/Interpret/error-pattern.sml Fri Apr 24 09:01:48 2020 +0200
14.2 +++ b/test/Tools/isac/Interpret/error-pattern.sml Mon Apr 27 12:36:21 2020 +0200
14.3 @@ -1082,7 +1082,7 @@
14.4 {errpats, scr = Rule.Prog prog, ...} => (errpats, prog)
14.5 | _ => error "find_fill_patterns: uncovered case of get_met"
14.6 val {env, ...} = Ctree.get_istate_LI pt pos |> Istate.the_pstate
14.7 - val subst = Rtools.get_bdv_subst prog env
14.8 + val subst = Subst.for_bdv prog env
14.9 val errpatthms = errpats
14.10 |> filter ((curry op = errpatID) o (#1: errpat -> errpatID))
14.11 |> map (#3: errpat -> thm list)
15.1 --- a/test/Tools/isac/Interpret/rewtools.sml Fri Apr 24 09:01:48 2020 +0200
15.2 +++ b/test/Tools/isac/Interpret/rewtools.sml Mon Apr 27 12:36:21 2020 +0200
15.3 @@ -29,7 +29,6 @@
15.4 "----------- fun filter_appl_rews -----------------------";
15.5 ============ inhibit exn WN120321 ==============================================*)
15.6 "----------- fun is_contained_in ------------------------";
15.7 -"----------- build fun get_bdv_subst --------------------------------";
15.8 "--------------------------------------------------------";
15.9 "--------------------------------------------------------";
15.10
15.11 @@ -360,32 +359,3 @@
15.12 val r1 = Eval ("Groups.minus_class.minus", eval_binop "#add_");
15.13 if not (Rtools.contains_rule r1 Test_simplify) then ()
15.14 else error "rewtools.sml Rtools.contains_rule Eval";
15.15 -
15.16 -"----------- build fun get_bdv_subst --------------------------------";
15.17 -"----------- build fun get_bdv_subst --------------------------------";
15.18 -"----------- build fun get_bdv_subst --------------------------------";
15.19 -val {scr = Prog prog, ...} = get_met ["diff", "differentiate_on_R"];
15.20 -val env = [(str2term "v_v", str2term "x")];
15.21 -subst2str env = "[\"\n(v_v, x)\"]";
15.22 -
15.23 -"~~~~~ fun get_bdv_subst, args:"; val (prog, env) = (prog, env);
15.24 - fun scan (Const _) = NONE
15.25 - | scan (Free _) = NONE
15.26 - | scan (Var _) = NONE
15.27 - | scan (Bound _) = NONE
15.28 - | scan (t as Const ("List.list.Cons", _) $ (Const ("Product_Type.Pair", _) $ _ $ _) $ _) =
15.29 - if TermC.is_bdv_subst t then SOME t else NONE
15.30 - | scan (Abs (_, _, body)) = scan body
15.31 - | scan (t1 $ t2) = case scan t1 of NONE => scan t2 | SOME subst => SOME subst
15.32 -
15.33 -val SOME tm = scan prog;
15.34 -val subst = tm |> subst_atomic env;
15.35 -if UnparseC.term tm = "[(''bdv'', v_v)]" then () else error "get_bdv_subst changed 1";
15.36 -
15.37 -if subst'_to_sube subst = ["(''bdv'', x)"] then () else error "get_bdv_subst changed 2";
15.38 -
15.39 -case get_bdv_subst prog env of
15.40 - (SOME ["(''bdv'', x)"], [(Free ("bdv", _), Free ("x", _))]: subst) => ()
15.41 -| _ => error "get_bdv_subst changed 3";
15.42 -
15.43 -val (SOME subs, _) = get_bdv_subst prog env;
16.1 --- a/test/Tools/isac/Knowledge/algein.sml Fri Apr 24 09:01:48 2020 +0200
16.2 +++ b/test/Tools/isac/Knowledge/algein.sml Mon Apr 27 12:36:21 2020 +0200
16.3 @@ -110,9 +110,9 @@
16.4
16.5 (*testing code in ME/appl.sml*)
16.6 val sube = ["?a1 = (3::real)"];
16.7 -val subte = sube2subte sube;
16.8 +val subte = Subst.tyty_to_eqs sube;
16.9 UnparseC.terms_short subte = "[?a1 = 3]"; (* = true*)
16.10 -val subst = sube2subst thy sube;
16.11 +val subst = Subst.T_from_tyty thy sube;
16.12 foldl and_ (true, map contains_Var subte);
16.13
16.14 val t'' = subst_atomic subst t';
17.1 --- a/test/Tools/isac/MathEngBasic/specification-elems.sml Fri Apr 24 09:01:48 2020 +0200
17.2 +++ b/test/Tools/isac/MathEngBasic/specification-elems.sml Mon Apr 27 12:36:21 2020 +0200
17.3 @@ -7,56 +7,12 @@
17.4 "-----------------------------------------------------------------------------";
17.5 "table of contents -----------------------------------------------------------";
17.6 "-----------------------------------------------------------------------------";
17.7 -"-------- fun subst_to_subst' ------------------------------------------------";
17.8 -"-------- fun subst'_to_sube -------------------------------------------------";
17.9 -"-------- fun subs2subst -----------------------------------------------------";
17.10 -"-------- fun subst'_to_subst ------------------------------------------------";
17.11 -"-------- fun subst2subs -----------------------------------------------------";
17.12 +"-------- TODO'---------------------------------------------------------------";
17.13 +"-----------------------------------------------------------------------------";
17.14 "-----------------------------------------------------------------------------";
17.15 "-----------------------------------------------------------------------------";
17.16
17.17 -"-------- fun subst_to_subst' ------------------------------------------------";
17.18 -"-------- fun subst_to_subst' ------------------------------------------------";
17.19 -"-------- fun subst_to_subst' ------------------------------------------------";
17.20 -val subst_rew =
17.21 - [(@{term "bdv_1 :: real"}, @{term "x :: real"}),
17.22 - (@{term "bdv_2 :: real"}, @{term "y :: real"}),
17.23 - (@{term "bdv_3 :: real"}, @{term "z :: real"})];
17.24 -if UnparseC.term (subst_to_subst' subst_rew) = "[(''bdv_1'', x), (''bdv_2'', y), (''bdv_3'', z)]"
17.25 -then () else error "subst_to_subst' changed"
17.26
17.27 -"-------- fun subst'_to_sube -------------------------------------------------";
17.28 -"-------- fun subst'_to_sube -------------------------------------------------";
17.29 -"-------- fun subst'_to_sube -------------------------------------------------";
17.30 -val subst_prog = @{term "[(''bdv_1'', x::real), (''bdv_2'', y::real), (''bdv_3'', z::real)]"};
17.31 -if Selem.subst'_to_sube subst_prog = ["(''bdv_1'', x)", "(''bdv_2'', y)", "(''bdv_3'', z)"] then ()
17.32 -else error "subst'_to_sube changed";
17.33 -
17.34 -"-------- fun subs2subst -----------------------------------------------------";
17.35 -"-------- fun subs2subst -----------------------------------------------------";
17.36 -"-------- fun subs2subst -----------------------------------------------------";
17.37 -case subs2subst @{theory} ["(''bdv_1'', x)", "(''bdv_2'', y)", "(''bdv_3'', z)"] of
17.38 - [(Free ("bdv_1", _), Free ("x", _)),
17.39 - (Free ("bdv_2", _), Free ("y", _)),
17.40 - (Free ("bdv_3", _), Free ("z", _))] => ()
17.41 -| _ => error "subs2subst changed";
17.42 -
17.43 -"-------- fun subst'_to_subst ------------------------------------------------";
17.44 -"-------- fun subst'_to_subst ------------------------------------------------";
17.45 -"-------- fun subst'_to_subst ------------------------------------------------";
17.46 -val t = @{term "[(''bdv_1'', x::real), (''bdv_2'', y::real), (''bdv_3'', z::real)]"};
17.47 -case subst'_to_subst t of
17.48 - [(Free ("bdv_1", _), Free ("x", _)),
17.49 - (Free ("bdv_2", _), Free ("y", _)),
17.50 - (Free ("bdv_3", _), Free ("z", _))] => ()
17.51 -| _ => error "subst'_to_subst changed";
17.52 -
17.53 -"-------- fun subst2subs -----------------------------------------------------";
17.54 -"-------- fun subst2subs -----------------------------------------------------";
17.55 -"-------- fun subst2subs -----------------------------------------------------";
17.56 -val subst_rew =
17.57 - [(@{term "bdv_1 :: real"}, @{term "x :: real"}),
17.58 - (@{term "bdv_2 :: real"}, @{term "y :: real"}),
17.59 - (@{term "bdv_3 :: real"}, @{term "z :: real"})];
17.60 -if subst2subs subst_rew = ["(''bdv_1'', x)", "(''bdv_2'', y)", "(''bdv_3'', z)"]then ()
17.61 -else error "subst2subs changed";
17.62 +"-------- TODO'---------------------------------------------------------------";
17.63 +"-------- TODO'---------------------------------------------------------------";
17.64 +"-------- TODO'---------------------------------------------------------------";
18.1 --- a/test/Tools/isac/ProgLang/auto_prog.sml Fri Apr 24 09:01:48 2020 +0200
18.2 +++ b/test/Tools/isac/ProgLang/auto_prog.sml Mon Apr 27 12:36:21 2020 +0200
18.3 @@ -54,7 +54,7 @@
18.4 (str2term "someTermWithBdv");
18.5 "~~~~~ fun init_istate , args:"; val ((Tactic.Rewrite_Set_Inst (subs, rls)), t)
18.6 = ((Rewrite_Set_Inst (["(''bdv'', x)"], "integration_rules")), str2term "someTermWithBdv");
18.7 - val v = case Selem.subs2subst (ThyC.get_theory "Isac_Knowledge") subs of
18.8 + val v = case Subst.T_from_input (ThyC.get_theory "Isac_Knowledge") subs of
18.9 (_, v) :: _ => v;
18.10 (*case*) assoc_rls rls (*of*);
18.11
19.1 --- a/test/Tools/isac/Test_Isac.thy Fri Apr 24 09:01:48 2020 +0200
19.2 +++ b/test/Tools/isac/Test_Isac.thy Mon Apr 27 12:36:21 2020 +0200
19.3 @@ -100,7 +100,7 @@
19.4 open Error_Pattern;
19.5 open Error_Pattern_Def;
19.6 open In_Chead;
19.7 - open Rtools; .trtas2str;
19.8 + open Rtools;
19.9 open Chead; pt_extract;
19.10 open Generate; (* NONE *)
19.11 open Ctree; append_problem;
19.12 @@ -126,7 +126,7 @@
19.13 open Rewrite;
19.14 open Eval; get_pair;
19.15 open TermC; atomt;
19.16 - open Celem; e_pbt;
19.17 + open Celem;
19.18 open Rule;
19.19 open Rule_Set; Sequence;
19.20 open Exec_Def
19.21 @@ -188,8 +188,10 @@
19.22 ML_file "BaseDefinitions/error-fill-def.sml"
19.23 ML_file "BaseDefinitions/rule-set.sml"
19.24 ML_file "BaseDefinitions/check-unique.sml"
19.25 +(*called by Know_Store*)
19.26 ML_file "BaseDefinitions/calcelems.sml"
19.27 ML_file "BaseDefinitions/termC.sml"
19.28 + ML_file substitution.sml
19.29 ML_file "BaseDefinitions/contextC.sml"
19.30 ML_file "BaseDefinitions/environment.sml"
19.31 ML_file "BaseDefinitions/kestore.sml" (* setup in ADDTEST/accumulate-val/lucas_interpreter.sml*)
20.1 --- a/test/Tools/isac/Test_Isac_Short.thy Fri Apr 24 09:01:48 2020 +0200
20.2 +++ b/test/Tools/isac/Test_Isac_Short.thy Mon Apr 27 12:36:21 2020 +0200
20.3 @@ -188,8 +188,10 @@
20.4 ML_file "BaseDefinitions/error-fill-def.sml"
20.5 ML_file "BaseDefinitions/rule-set.sml"
20.6 ML_file "BaseDefinitions/check-unique.sml"
20.7 +(*called by Know_Store*)
20.8 ML_file "BaseDefinitions/calcelems.sml"
20.9 ML_file "BaseDefinitions/termC.sml"
20.10 + ML_file substitution.sml
20.11 ML_file "BaseDefinitions/contextC.sml"
20.12 ML_file "BaseDefinitions/environment.sml"
20.13 ML_file "BaseDefinitions/kestore.sml" (* setup in ADDTEST/accumulate-val/lucas_interpreter.sml*)
21.1 --- a/test/Tools/isac/Test_Some.thy Fri Apr 24 09:01:48 2020 +0200
21.2 +++ b/test/Tools/isac/Test_Some.thy Mon Apr 27 12:36:21 2020 +0200
21.3 @@ -20,7 +20,7 @@
21.4 open Error_Pattern;
21.5 open Error_Pattern_Def;
21.6 open In_Chead;
21.7 - open Rtools; .trtas2str;
21.8 + open Rtools;
21.9 open Chead; pt_extract;
21.10 open Generate; (* NONE *)
21.11 open Ctree; append_problem;
21.12 @@ -46,7 +46,7 @@
21.13 open Rewrite;
21.14 open Eval; get_pair;
21.15 open TermC; atomt;
21.16 - open Celem; e_pbt;
21.17 + open Celem;
21.18 open Rule;
21.19 open Rule_Set
21.20 open Exec_Def
21.21 @@ -97,7 +97,6 @@
21.22 ML \<open>
21.23 \<close> ML \<open>
21.24 \<close> ML \<open>
21.25 -\<close> ML \<open>
21.26 \<close>
21.27
21.28 section \<open>===================================================================================\<close>