1.1 --- a/src/Tools/isac/BaseDefinitions/Know_Store.thy Tue Apr 21 10:53:04 2020 +0200
1.2 +++ b/src/Tools/isac/BaseDefinitions/Know_Store.thy Tue Apr 21 11:28:20 2020 +0200
1.3 @@ -63,8 +63,8 @@
1.4 val add_rlss: (Rule_Set.id * (ThyC.id * Rule_Set.T)) list -> theory -> theory
1.5 val get_calcs: theory -> (Exec_Def.prog_calcID * (Exec_Def.calID * Exec_Def.eval_fn)) list
1.6 val add_calcs: (Exec_Def.prog_calcID * (Exec_Def.calID * Exec_Def.eval_fn)) list -> theory -> theory
1.7 - val get_cas: theory -> CAS_Def.cas_elem list
1.8 - val add_cas: CAS_Def.cas_elem list -> theory -> theory
1.9 + val get_cas: theory -> CAS_Def.T list
1.10 + val add_cas: CAS_Def.T list -> theory -> theory
1.11 val get_ptyps: theory -> Probl_Def.store
1.12 val add_pbts: (Probl_Def.T * Spec.pblID) list -> theory -> theory
1.13 val get_mets: theory -> Meth_Def.store
1.14 @@ -102,10 +102,10 @@
1.15 type T = (term * (Spec.spec * (term list -> (term * term list) list))) list;
1.16 val empty = [];
1.17 val extend = I;
1.18 - val merge = merge CAS_Def.cas_eq;
1.19 + val merge = merge CAS_Def.equal;
1.20 );
1.21 fun get_cas thy = Data.get thy
1.22 - fun add_cas cas = Data.map (union_overwrite CAS_Def.cas_eq cas)
1.23 + fun add_cas cas = Data.map (union_overwrite CAS_Def.equal cas)
1.24
1.25 structure Data = Theory_Data (
1.26 type T = Probl_Def.store;
1.27 @@ -232,7 +232,7 @@
1.28 fun check_kestore_calc ((id, (c, _)) : Rule_Def.calc) = "(" ^ id ^ ", (" ^ c ^ ", fn))";
1.29
1.30 (* we avoid term_to_string''' defined later *)
1.31 -fun check_kestore_cas ((t, (s, _)) : CAS_Def.cas_elem) =
1.32 +fun check_kestore_cas ((t, (s, _)) : CAS_Def.T) =
1.33 "(" ^ (Print_Mode.setmp [] (Syntax.string_of_term (Config.put show_markup false
1.34 (Proof_Context.init_global @{theory})))) t ^ ", " ^ Spec.spec2str s ^ ")";
1.35
2.1 --- a/src/Tools/isac/BaseDefinitions/calcelems.sml Tue Apr 21 10:53:04 2020 +0200
2.2 +++ b/src/Tools/isac/BaseDefinitions/calcelems.sml Tue Apr 21 11:28:20 2020 +0200
2.3 @@ -182,8 +182,8 @@
2.4 (*\------- to Spec -------/*)
2.5
2.6 (*/------- to Celem7 -------\*)
2.7 -type cas_elem = CAS_Def.cas_elem;
2.8 -val cas_eq = CAS_Def.cas_eq;
2.9 +type cas_elem = CAS_Def.T;
2.10 +val cas_eq = CAS_Def.equal;
2.11 (*\------- to Celem7 -------/*)
2.12
2.13 (*either theID or pblID or metID*)
3.1 --- a/src/Tools/isac/BaseDefinitions/cas-def.sml Tue Apr 21 10:53:04 2020 +0200
3.2 +++ b/src/Tools/isac/BaseDefinitions/cas-def.sml Tue Apr 21 11:28:20 2020 +0200
3.3 @@ -4,13 +4,12 @@
3.4
3.5 *)
3.6 signature COMPUTER_ALGEBRA_SYSTEM__COMMAND_DEF =
3.7 -(*/------- to Celem7 -------\*)
3.8 -(*\------- to Celem7 -------/*)
3.9 sig
3.10 -(*/------- to Celem7 -------\*)
3.11 - type cas_elem
3.12 - val cas_eq: cas_elem * cas_elem -> bool
3.13 -(*\------- to Celem7 -------/*)
3.14 + type T
3.15 +(*type cas_elem*)
3.16 + val equal: T * T -> bool
3.17 +(*val cas_eq: T * T -> bool*)
3.18 +
3.19 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
3.20 (*NONE*)
3.21 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
3.22 @@ -30,11 +29,11 @@
3.23 (term * (* description of an element *)
3.24 term list) (* value of the element (always put into a list) *)
3.25 list) (* of elements in the formalization *)
3.26 -type cas_elem =
3.27 +type T =
3.28 (term * (* cas-command, eg. 'solve' *)
3.29 (Spec.spec * (* theory, problem, method *)
3.30 generate_fn))
3.31 -fun cas_eq ((t1, (_, _)) : cas_elem, (t2, (_, _)) : cas_elem) = t1 = t2
3.32 +fun equal ((t1, (_, _)) : T, (t2, (_, _)) : T) = t1 = t2
3.33 (*\------- to Celem7 -------/*)
3.34
3.35 (**)end(**)
4.1 --- a/src/Tools/isac/MathEngBasic/cas-command.sml Tue Apr 21 10:53:04 2020 +0200
4.2 +++ b/src/Tools/isac/MathEngBasic/cas-command.sml Tue Apr 21 11:28:20 2020 +0200
4.3 @@ -5,6 +5,7 @@
4.4
4.5 signature COMPUTER_ALGEBRA_SYSTEM_COMMAND =
4.6 sig
4.7 +(*type T = CAS_Def.T .. not required after Know_Store?*)
4.8
4.9 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
4.10 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
4.11 @@ -16,5 +17,8 @@
4.12 struct
4.13 (**)
4.14
4.15 +type T = CAS_Def.T;
4.16 +
4.17 +(*type T = CAS_Def.T .. not required after Know_Store?*)
4.18
4.19 (**)end(**)
5.1 --- a/test/Tools/isac/BaseDefinitions/check-unique.sml Tue Apr 21 10:53:04 2020 +0200
5.2 +++ b/test/Tools/isac/BaseDefinitions/check-unique.sml Tue Apr 21 11:28:20 2020 +0200
5.3 @@ -54,11 +54,11 @@
5.4 (message (collect met_select_guh)): met Store.ptyp list -> guh -> unit;
5.5
5.6 (Check_Unique.collect (#guh : Probl_Def.T -> Check_Unique.guh)): pbt Store.ptyp list -> guh list;
5.7 -(Check_Unique.collect (#guh : Meth_Def.met -> Check_Unique.guh)): met Store.ptyp list -> guh list;
5.8 +(Check_Unique.collect (#guh : Meth_Def.T -> Check_Unique.guh)): met Store.ptyp list -> guh list;
5.9
5.10 val check_pblguh_unique = message (Check_Unique.collect (#guh : Probl_Def.T -> Check_Unique.guh));
5.11 check_pblguh_unique: pbt Store.ptyp list -> guh -> unit
5.12 ;
5.13 -val check_metguh_unique = message (Check_Unique.collect (#guh : Meth_Def.met -> Check_Unique.guh));
5.14 +val check_metguh_unique = message (Check_Unique.collect (#guh : Meth_Def.T -> Check_Unique.guh));
5.15 check_metguh_unique: met Store.ptyp list -> guh -> unit
5.16 ;
5.17 \ No newline at end of file