1.1 --- a/src/Tools/isac/BaseDefinitions/environment.sml Fri Apr 24 08:51:05 2020 +0200
1.2 +++ b/src/Tools/isac/BaseDefinitions/environment.sml Fri Apr 24 09:01:48 2020 +0200
1.3 @@ -6,10 +6,10 @@
1.4 sig
1.5 (*Celem*)
1.6 type T
1.7 - val env2str: UnparseC.subst -> string
1.8 - val env2str': UnparseC.subst -> string
1.9 - val subst2str: UnparseC.subst -> string
1.10 - val subst2str': UnparseC.subst -> string
1.11 + val env2str: subst -> string
1.12 + val env2str': subst -> string
1.13 + val subst2str: subst -> string
1.14 + val subst2str': subst -> string
1.15 val update: T -> term * term -> T
1.16 val update': term -> term * T -> T
1.17 val update_opt: T -> term option * term -> T
2.1 --- a/src/Tools/isac/BaseDefinitions/libraryC.sml Fri Apr 24 08:51:05 2020 +0200
2.2 +++ b/src/Tools/isac/BaseDefinitions/libraryC.sml Fri Apr 24 09:01:48 2020 +0200
2.3 @@ -58,17 +58,21 @@
2.4 val nth: int -> 'a list -> 'a
2.5 val overwrite: (''a * 'b) list * (''a * 'b) -> (''a * 'b) list
2.6 val overwritel: (''a * 'b) list * (''a * 'b) list -> (''a * 'b) list
2.7 +
2.8 val pair2str: string * string -> string
2.9 val pair2str_: string * string -> string
2.10 val pair2tri: ('a * 'b) * 'c -> 'a * 'b * 'c
2.11 val snd3: 'a * 'b * 'c -> 'b
2.12 val spair2str: string * string -> string
2.13 +
2.14 val split_nlast: int * 'a list -> 'a list * 'a list
2.15 val string_to_bool: string -> bool
2.16 val strs2str: string list -> string
2.17 val strs2str': string list -> string
2.18 val strs2str_: string list -> string (* duplicates in Rule *)
2.19 val strslist2strs: string list list -> string
2.20 + type subst = (term * term) list
2.21 +
2.22 val take: int * 'a list -> 'a list
2.23 val take_fromto: int -> int -> 'a list -> 'a list
2.24 val takelast: int * 'a list -> 'a list
2.25 @@ -78,8 +82,8 @@
2.26 val thd3: 'a * 'b * 'c -> 'c
2.27 val triple2pair: 'a * 'b * 'c -> 'a * 'b
2.28 val ~~~ : 'a list * 'b list -> ('a * 'b) list
2.29 +
2.30 val linefeed: string -> string
2.31 -
2.32 val dropwhile' : ('a -> 'b -> bool) -> 'a list -> 'b list -> 'a list * 'b list
2.33 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
2.34 (* NONE *)
2.35 @@ -184,6 +188,8 @@
2.36 val nos = space_implode "#";
2.37 fun strs2str_ strl = "#" ^ (nos strl) ^ "#";
2.38 fun strslist2strs strslist = map strs2str strslist |> strs2str';
2.39 +type subst = (term * term) list;
2.40 +
2.41 fun spair2str (s1, s2) = "(" ^ quote s1 ^ ", " ^ quote s2 ^ ")";
2.42 fun pair2str_ (s1, s2) = s1 ^ "#" ^ s2;
2.43 fun pair2str (s1, s2) = "(" ^ s1 ^ ", " ^ s2 ^ ")";
3.1 --- a/src/Tools/isac/BaseDefinitions/thy-html.sml Fri Apr 24 08:51:05 2020 +0200
3.2 +++ b/src/Tools/isac/BaseDefinitions/thy-html.sml Fri Apr 24 09:01:48 2020 +0200
3.3 @@ -59,7 +59,7 @@
3.4 | Hrls of {guh: Check_Unique.id, coursedesign: authors, mathauthors: authors, thy_rls: (ThyC.id * Rule_Set.T)}
3.5 | Hcal of {guh: Check_Unique.id, coursedesign: authors, mathauthors: authors, calc: Rule_Def.calc}
3.6 | Hord of {guh: Check_Unique.id, coursedesign: authors, mathauthors: authors,
3.7 - ord: (UnparseC.subst -> (term * term) -> bool)};
3.8 + ord: (subst -> (term * term) -> bool)};
3.9 fun the2str (Html {guh, ...}) = guh
3.10 | the2str (Hthm {guh, ...}) = guh
3.11 | the2str (Hrls {guh, ...}) = guh
4.1 --- a/src/Tools/isac/BaseDefinitions/unparseC.sml Fri Apr 24 08:51:05 2020 +0200
4.2 +++ b/src/Tools/isac/BaseDefinitions/unparseC.sml Fri Apr 24 09:01:48 2020 +0200
4.3 @@ -6,7 +6,6 @@
4.4 signature UNPARSE_ISAC =
4.5 sig
4.6 eqtype term_as_string
4.7 - type subst = (term * term) list
4.8
4.9 val term_empty: term
4.10 val typ_empty: typ
4.11 @@ -38,7 +37,6 @@
4.12 (**)
4.13
4.14 type term_as_string = string;
4.15 -type subst = (term * term) list;
4.16
4.17 fun term_in_ctxt ctxt t =
4.18 let
5.1 --- a/src/Tools/isac/BridgeLibisabelle/datatypes.sml Fri Apr 24 08:51:05 2020 +0200
5.2 +++ b/src/Tools/isac/BridgeLibisabelle/datatypes.sml Fri Apr 24 09:01:48 2020 +0200
5.3 @@ -44,7 +44,7 @@
5.4 val spec2xml : int -> Spec.T -> xml
5.5 val sub2xml : int -> Term.term * Term.term -> xml
5.6 val subs2xml : int -> Selem.subs -> xml
5.7 - val subst2xml : int -> UnparseC.subst -> xml
5.8 + val subst2xml : int -> subst -> xml
5.9 val tac2xml : int -> Tactic.input -> xml
5.10 val tacs2xml : int -> Tactic.input list -> xml
5.11 val theref2xml : int -> ThyC.id -> string -> xstring -> string
6.1 --- a/src/Tools/isac/Interpret/error-pattern.sml Fri Apr 24 08:51:05 2020 +0200
6.2 +++ b/src/Tools/isac/Interpret/error-pattern.sml Fri Apr 24 09:01:48 2020 +0200
6.3 @@ -24,7 +24,7 @@
6.4 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
6.5 val find_fill_patterns: Calc.T -> id -> record list
6.6 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
6.7 - val check_for': term * term -> UnparseC.subst -> id * term -> Rule_Set.T -> id option
6.8 + val check_for': term * term -> subst -> id * term -> Rule_Set.T -> id option
6.9 val fill_from_store: Selem.subs option * (term * term) list -> term -> id -> thm ->
6.10 record list
6.11 val fill_form: Selem.subs option * (term * term) list -> thm * term -> id -> fill_in ->
7.1 --- a/src/Tools/isac/Interpret/rewtools.sml Fri Apr 24 08:51:05 2020 +0200
7.2 +++ b/src/Tools/isac/Interpret/rewtools.sml Fri Apr 24 09:01:48 2020 +0200
7.3 @@ -9,7 +9,7 @@
7.4 sig
7.5
7.6 (*/------- for error-fill-pattern -------\*)
7.7 - val get_bdv_subst : term -> (term * term) list -> Selem.subs option * UnparseC.subst
7.8 + val get_bdv_subst : term -> (term * term) list -> Selem.subs option * subst
7.9 val thy_containing_thm : string -> string * string
7.10 val thy_containing_rls : ThyC.id -> Rule_Set.id -> string * ThyC.id
7.11 val thy_containing_cal : ThyC.id -> Exec_Def.prog_calcID -> string * string
7.12 @@ -25,14 +25,14 @@
7.13
7.14 datatype contthy
7.15 = ContNOrew of {applto: term, thm_rls: Check_Unique.id, thyID: ThyC.id}
7.16 - | ContNOrewInst of {applto: term, bdvs: UnparseC.subst, thm_rls: Check_Unique.id, thminst: term, thyID: ThyC.id}
7.17 + | ContNOrewInst of {applto: term, bdvs: subst, thm_rls: Check_Unique.id, thminst: term, thyID: ThyC.id}
7.18 | ContRls of {applto: term, asms: term list, result: term, rls: Check_Unique.id, thyID: ThyC.id}
7.19 - | ContRlsInst of {applto: term, asms: term list, bdvs: UnparseC.subst, result: term, rls: Check_Unique.id, thyID: ThyC.id}
7.20 + | ContRlsInst of {applto: term, asms: term list, bdvs: subst, result: term, rls: Check_Unique.id, thyID: ThyC.id}
7.21 | ContThm of {applat: term, applto: term, asmrls: Rule_Set.id, asms: (term * term) list,
7.22 lhs: term * term, resasms: term list, result: term, reword: Rewrite_Ord.rew_ord', rhs: term * term,
7.23 thm: Check_Unique.id, thyID: ThyC.id}
7.24 | ContThmInst of {applat: term, applto: term, asmrls: Rule_Set.id, asms: (term * term) list,
7.25 - bdvs: UnparseC.subst, lhs: term * term, resasms: term list, result: term, reword: Rewrite_Ord.rew_ord',
7.26 + bdvs: subst, lhs: term * term, resasms: term list, result: term, reword: Rewrite_Ord.rew_ord',
7.27 rhs: term * term, thm: Check_Unique.id, thminst: term, thyID: ThyC.id}
7.28 | EContThy
7.29 val guh2filename : Check_Unique.id -> Celem.filename
7.30 @@ -135,7 +135,7 @@
7.31 | ContThmInst of (* a theorem with bdvs in contex ============ *)
7.32 {thyID : ThyC.id, (*for *2guh in sub-elems here .*)
7.33 thm : Check_Unique.id, (*theorem in the context .*)
7.34 - bdvs : UnparseC.subst, (*bound variables to modify... .*)
7.35 + bdvs : subst, (*bound variables to modify... .*)
7.36 thminst : term, (*... theorem instantiated .*)
7.37 applto : term, (*applied to formula ... .*)
7.38 applat : term, (*... with lhs inserted .*)
7.39 @@ -160,7 +160,7 @@
7.40 | ContRlsInst of (* a rule set with bdvs in contex =========== *)
7.41 {thyID : ThyC.id, (*for *2guh in sub-elems here .*)
7.42 rls : Check_Unique.id, (*rule set in the context .*)
7.43 - bdvs : UnparseC.subst, (*for bound variables in thms .*)
7.44 + bdvs : subst, (*for bound variables in thms .*)
7.45 applto : term, (*rewrite this formula .*)
7.46 result : term, (*resulting from the rewrite .*)
7.47 asms : term list (*... with asms stored .*)
7.48 @@ -173,7 +173,7 @@
7.49 | ContNOrewInst of (* no rewrite for some instantiation ====== *)
7.50 {thyID : ThyC.id, (*for *2guh in sub-elems here .*)
7.51 thm_rls : Check_Unique.id, (*thm or rls in the context .*)
7.52 - bdvs : UnparseC.subst, (*for bound variables in thms .*)
7.53 + bdvs : subst, (*for bound variables in thms .*)
7.54 thminst : term, (*... theorem instantiated .*)
7.55 applto : term (*rewrite this formula .*)
7.56 }
7.57 @@ -296,7 +296,7 @@
7.58
7.59 (* try if a rewrite-rule is applicable to a given formula;
7.60 in case of rule-sets (recursivley) collect all _atomic_ rewrites *)
7.61 -fun try_rew thy ((_, ro) : Rewrite_Ord.rew_ord) erls (subst : UnparseC.subst) f (thm' as Rule.Thm (_, thm)) =
7.62 +fun try_rew thy ((_, ro) : Rewrite_Ord.rew_ord) erls (subst : subst) f (thm' as Rule.Thm (_, thm)) =
7.63 if Auto_Prog.contains_bdv thm
7.64 then case Rewrite.rewrite_inst_ thy ro erls false subst thm f of
7.65 SOME _ => [Tactic.rule2tac thy subst thm']
7.66 @@ -464,7 +464,7 @@
7.67 | scan (t1 $ t2) = case scan t1 of NONE => scan t2 | SOME subst => SOME subst
7.68 in
7.69 case scan prog of
7.70 - NONE => (NONE: Selem.subs option, []: UnparseC.subst)
7.71 + NONE => (NONE: Selem.subs option, []: subst)
7.72 | SOME tm =>
7.73 let val subst = subst_atomic env tm
7.74 in (SOME (Selem.subst'_to_sube subst), Selem.subst'_to_subst subst) end
8.1 --- a/src/Tools/isac/Knowledge/Base_Tools.thy Fri Apr 24 08:51:05 2020 +0200
8.2 +++ b/src/Tools/isac/Knowledge/Base_Tools.thy Fri Apr 24 09:01:48 2020 +0200
8.3 @@ -42,8 +42,8 @@
8.4 local
8.5 open Term;
8.6 in
8.7 - fun termlessI (_: UnparseC.subst) uv = LibraryC.termless uv;
8.8 - fun term_ordI (_: UnparseC.subst) uv = Term_Ord.term_ord uv;
8.9 + fun termlessI (_: subst) uv = LibraryC.termless uv;
8.10 + fun term_ordI (_: subst) uv = Term_Ord.term_ord uv;
8.11 end;
8.12 \<close> ML \<open>
8.13 (*TODO.WN0509 reduce ids: tless_true = e_rew_ord' = Rewrite_Ord.e_rew_ord = Rewrite_Ord.dummy_ord*)
9.1 --- a/src/Tools/isac/Knowledge/Poly.thy Fri Apr 24 08:51:05 2020 +0200
9.2 +++ b/src/Tools/isac/Knowledge/Poly.thy Fri Apr 24 09:01:48 2020 +0200
9.3 @@ -505,7 +505,7 @@
9.4
9.5 in
9.6
9.7 -fun ord_make_polynomial (pr:bool) thy (_: UnparseC.subst) tu =
9.8 +fun ord_make_polynomial (pr:bool) thy (_: subst) tu =
9.9 (term_ord' pr thy(***) tu = LESS );
9.10
9.11 end;(*local*)
10.1 --- a/src/Tools/isac/Knowledge/Root.thy Fri Apr 24 08:51:05 2020 +0200
10.2 +++ b/src/Tools/isac/Knowledge/Root.thy Fri Apr 24 09:01:48 2020 +0200
10.3 @@ -151,7 +151,7 @@
10.4 thy:
10.5 subst: no bound variables, only Root.sqrt
10.6 tu: the terms to compare (t1, t2) ... *)
10.7 -fun sqrt_right (pr:bool) thy (_: UnparseC.subst) tu =
10.8 +fun sqrt_right (pr:bool) thy (_: subst) tu =
10.9 (term_ord' pr thy(***) tu = LESS );
10.10 end;
10.11
11.1 --- a/src/Tools/isac/Knowledge/Test.thy Fri Apr 24 08:51:05 2020 +0200
11.2 +++ b/src/Tools/isac/Knowledge/Test.thy Fri Apr 24 09:01:48 2020 +0200
11.3 @@ -345,7 +345,7 @@
11.4 list_ord (term_ord' pr (ThyC.get_theory "Isac_Knowledge"))(ts, us);
11.5 in
11.6
11.7 -fun ord_make_polytest (pr:bool) thy (_: UnparseC.subst) tu =
11.8 +fun ord_make_polytest (pr:bool) thy (_: subst) tu =
11.9 (term_ord' pr thy(***) tu = LESS );
11.10
11.11 end;(*local*)
11.12 @@ -353,7 +353,7 @@
11.13
11.14 section \<open>term order\<close>
11.15 ML \<open>
11.16 -fun term_order (_: UnparseC.subst) tu = (term_ordI [] tu = LESS);
11.17 +fun term_order (_: subst) tu = (term_ordI [] tu = LESS);
11.18 \<close>
11.19
11.20 section \<open>rulesets\<close>
12.1 --- a/src/Tools/isac/Knowledge/Test_Build_Thydata.thy Fri Apr 24 08:51:05 2020 +0200
12.2 +++ b/src/Tools/isac/Knowledge/Test_Build_Thydata.thy Fri Apr 24 09:01:48 2020 +0200
12.3 @@ -6,7 +6,7 @@
12.4
12.5 ML \<open>
12.6 open Rule
12.7 -fun termlessI (_: UnparseC.subst) uv = LibraryC.termless uv;
12.8 +fun termlessI (_: subst) uv = LibraryC.termless uv;
12.9 \<close>
12.10 axiomatization where
12.11 thm111: "thm111 = thm111 + (111::int)" and
13.1 --- a/src/Tools/isac/MathEngBasic/specification-elems.sml Fri Apr 24 08:51:05 2020 +0200
13.2 +++ b/src/Tools/isac/MathEngBasic/specification-elems.sml Fri Apr 24 09:01:48 2020 +0200
13.3 @@ -17,7 +17,7 @@
13.4 (*type subst for rewriting, in Rule (+?Isabelle); rename subst_rew [(bools, x)] *)
13.5 (* TODO use these types in functions below and elsewhere; rename below according to types *)
13.6 val subst'_to_sube : subst' -> TermC.as_string list (* e.g. rename to subst_user_of_prog *)
13.7 - val subst_to_subst' : UnparseC.subst -> subst'
13.8 + val subst_to_subst' : subst -> subst'
13.9 val subst'_to_subst : subst' -> (term * term) list
13.10 val sube2str : TermC.as_string list -> string
13.11 val sube2subst : theory -> TermC.as_string list -> (term * term) list
14.1 --- a/src/Tools/isac/MathEngBasic/tactic.sml Fri Apr 24 08:51:05 2020 +0200
14.2 +++ b/src/Tools/isac/MathEngBasic/tactic.sml Fri Apr 24 09:01:48 2020 +0200
14.3 @@ -28,7 +28,7 @@
14.4
14.5 | Derive' of Rule_Set.T
14.6 | Detail_Set' of ThyC.id * bool * Rule_Set.T * term * Selem.result
14.7 - | Detail_Set_Inst' of ThyC.id * bool * UnparseC.subst * Rule_Set.T * term * Selem.result
14.8 + | Detail_Set_Inst' of ThyC.id * bool * subst * Rule_Set.T * term * Selem.result
14.9 | End_Detail' of Selem.result
14.10
14.11 | Empty_Tac_
14.12 @@ -41,9 +41,9 @@
14.13 | Refine_Tacitly' of Problem.id * Problem.id * ThyC.id * Method.id * Model.itm list
14.14
14.15 | Rewrite' of ThyC.id * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * ThmC.T * term * Selem.result
14.16 - | Rewrite_Inst' of ThyC.id * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * UnparseC.subst * ThmC.T * term * Selem.result
14.17 + | Rewrite_Inst' of ThyC.id * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * subst * ThmC.T * term * Selem.result
14.18 | Rewrite_Set' of ThyC.id * bool * Rule_Set.T * term * Selem.result
14.19 - | Rewrite_Set_Inst' of ThyC.id * bool * UnparseC.subst * Rule_Set.T * term * Selem.result
14.20 + | Rewrite_Set_Inst' of ThyC.id * bool * subst * Rule_Set.T * term * Selem.result
14.21
14.22 | Specify_Method' of Method.id * Model.ori list * Model.itm list
14.23 | Specify_Problem' of Problem.id * (bool * (Model.itm list * (bool * term) list))
14.24 @@ -362,7 +362,7 @@
14.25
14.26 | Derive' of Rule_Set.T
14.27 | Detail_Set' of ThyC.id * bool * Rule_Set.T * term * Selem.result
14.28 - | Detail_Set_Inst' of ThyC.id * bool * UnparseC.subst * Rule_Set.T * term * Selem.result
14.29 + | Detail_Set_Inst' of ThyC.id * bool * subst * Rule_Set.T * term * Selem.result
14.30 | End_Detail' of Selem.result
14.31
14.32 | Empty_Tac_
14.33 @@ -382,9 +382,9 @@
14.34 Method.id * (* from new pbt?! filled in specify *)
14.35 Model.itm list (* drop ! 9.03: remains [] for Model_Problem recognizing its activation *)
14.36 | Rewrite' of ThyC.id * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * ThmC.T * term * Selem.result
14.37 - | Rewrite_Inst' of ThyC.id * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * UnparseC.subst * ThmC.T * term * Selem.result
14.38 + | Rewrite_Inst' of ThyC.id * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * subst * ThmC.T * term * Selem.result
14.39 | Rewrite_Set' of ThyC.id * bool * Rule_Set.T * term * Selem.result
14.40 - | Rewrite_Set_Inst' of ThyC.id * bool * UnparseC.subst * Rule_Set.T * term * Selem.result
14.41 + | Rewrite_Set_Inst' of ThyC.id * bool * subst * Rule_Set.T * term * Selem.result
14.42
14.43 | Specify_Method' of Method.id * Model.ori list * Model.itm list
14.44 | Specify_Problem' of Problem.id *