1.1 --- a/src/Tools/isac/BaseDefinitions/Know_Store.thy Sun Apr 19 16:17:27 2020 +0200
1.2 +++ b/src/Tools/isac/BaseDefinitions/Know_Store.thy Sun Apr 19 16:43:53 2020 +0200
1.3 @@ -30,9 +30,8 @@
1.4 ML_file "rule-set.sml"
1.5
1.6 ML_file "celem-0.sml" (*survey Celem.*)
1.7 -ML_file "celem-1.sml" (*datatype 'a ptyp*)
1.8 -ML_file "celem-2.sml" (*guh*)
1.9 -ML_file "celem-3.sml" (*spec*)
1.10 +ML_file "store.sml"
1.11 +ML_file "specification.sml"
1.12 ML_file "celem-4.sml" (*pat*)
1.13 ML_file "celem-5.sml" (*ptyps*)
1.14 ML_file "celem-6.sml" (*mets*)
1.15 @@ -69,9 +68,9 @@
1.16 val get_cas: theory -> Celem7.cas_elem list
1.17 val add_cas: Celem7.cas_elem list -> theory -> theory
1.18 val get_ptyps: theory -> Celem5.ptyps
1.19 - val add_pbts: (Celem5.pbt * Celem3.pblID) list -> theory -> theory
1.20 + val add_pbts: (Celem5.pbt * Spec.pblID) list -> theory -> theory
1.21 val get_mets: theory -> Celem6.mets
1.22 - val add_mets: (Celem6.met * Celem3.metID) list -> theory -> theory
1.23 + val add_mets: (Celem6.met * Spec.metID) list -> theory -> theory
1.24 val get_thes: theory -> (Celem8.thydata Store.ptyp) list
1.25 val add_thes: (Celem8.thydata * Celem8.theID) list -> theory -> theory (* thydata dropped at existing elems *)
1.26 val insert_fillpats: (Celem8.theID * Error_Fill_Def.fillpat list) list -> theory -> theory
1.27 @@ -102,7 +101,7 @@
1.28 fun add_calcs calcs = Data.map (union_overwrite Exec_Def.calc_eq calcs)
1.29
1.30 structure Data = Theory_Data (
1.31 - type T = (term * (Celem3.spec * (term list -> (term * term list) list))) list;
1.32 + type T = (term * (Spec.spec * (term list -> (term * term list) list))) list;
1.33 val empty = [];
1.34 val extend = I;
1.35 val merge = merge Celem7.cas_eq;
1.36 @@ -237,7 +236,7 @@
1.37 (* we avoid term_to_string''' defined later *)
1.38 fun check_kestore_cas ((t, (s, _)) : Celem7.cas_elem) =
1.39 "(" ^ (Print_Mode.setmp [] (Syntax.string_of_term (Config.put show_markup false
1.40 - (Proof_Context.init_global @{theory})))) t ^ ", " ^ Celem3.spec2str s ^ ")";
1.41 + (Proof_Context.init_global @{theory})))) t ^ ", " ^ Spec.spec2str s ^ ")";
1.42
1.43 fun count_kestore_ptyps [] = 0
1.44 | count_kestore_ptyps ((Store.Ptyp (_, _, ps)) :: ps') =
2.1 --- a/src/Tools/isac/BaseDefinitions/calcelems.sml Sun Apr 19 16:17:27 2020 +0200
2.2 +++ b/src/Tools/isac/BaseDefinitions/calcelems.sml Sun Apr 19 16:43:53 2020 +0200
2.3 @@ -23,7 +23,7 @@
2.4 val pbts2str: pbt list -> string
2.5 (*\------- to Celem5 -------/*)
2.6
2.7 -(*/------- to Celem3 -------\*)
2.8 +(*/------- to Spec -------\*)
2.9 type metID
2.10 type pblID
2.11 type spec
2.12 @@ -33,7 +33,7 @@
2.13 val e_metID: metID
2.14 val empty_spec: spec
2.15 val e_spec: spec
2.16 -(*\------- to Celem3 -------/*)
2.17 +(*\------- to Spec -------/*)
2.18
2.19 (*/------- to Store -------\*)
2.20 (*datatype 'a ptyp = Ptyp of string * 'a list * 'a ptyp list\*)
2.21 @@ -136,7 +136,7 @@
2.22 type calcID = int;
2.23
2.24 (*/------- to Celem2 -------\*)
2.25 -type guh = Celem2.guh;
2.26 +type guh = Spec.guh;
2.27 (*\------- to Celem2 -------/*)
2.28 type xml = string; (* rm together with old code replaced by XML.tree *)
2.29
2.30 @@ -168,18 +168,18 @@
2.31 # ???
2.32 *)
2.33
2.34 -(*/------- to Celem3 -------\*)
2.35 +(*/------- to Spec -------\*)
2.36 (*the key into the hierarchy ob problems*)
2.37 -type pblID = Celem3.pblID;
2.38 -val e_pblID = Celem3.e_pblID;
2.39 -type metID = Celem3.metID;
2.40 -type spec = Celem3.spec;
2.41 -val spec2str = Celem3.spec2str;
2.42 -val e_metID = Celem3.e_metID;
2.43 -val metID2str = Celem3.metID2str;
2.44 -val empty_spec = Celem3.empty_spec;
2.45 -val e_spec = Celem3.e_spec;
2.46 -(*\------- to Celem3 -------/*)
2.47 +type pblID = Spec.pblID;
2.48 +val e_pblID = Spec.e_pblID;
2.49 +type metID = Spec.metID;
2.50 +type spec = Spec.spec;
2.51 +val spec2str = Spec.spec2str;
2.52 +val e_metID = Spec.e_metID;
2.53 +val metID2str = Spec.metID2str;
2.54 +val empty_spec = Spec.empty_spec;
2.55 +val e_spec = Spec.e_spec;
2.56 +(*\------- to Spec -------/*)
2.57
2.58 (*/------- to Celem7 -------\*)
2.59 type cas_elem = Celem7.cas_elem;
3.1 --- a/src/Tools/isac/BaseDefinitions/celem-0.sml Sun Apr 19 16:17:27 2020 +0200
3.2 +++ b/src/Tools/isac/BaseDefinitions/celem-0.sml Sun Apr 19 16:43:53 2020 +0200
3.3 @@ -22,13 +22,13 @@
3.4 val get_cas: theory -> Celem7.cas_elem list
3.5 val add_cas: Celem7.cas_elem list -> theory -> theory
3.6 val get_ptyps: theory -> Celem5.ptyps
3.7 - val add_pbts: (Celem5.pbt * Celem3.pblID) list -> theory -> theory
3.8 + val add_pbts: (Celem5.pbt * Spec.pblID) list -> theory -> theory
3.9 val get_mets: theory -> Celem6.mets
3.10 - val add_mets: (Celem6.met * Celem3.metID) list -> theory -> theory
3.11 + val add_mets: (Celem6.met * Spec.metID) list -> theory -> theory
3.12 val get_thes: theory -> (Celem8.thydata Store.ptyp) list
3.13 val add_thes: (Celem8.thydata * Celem8.theID) list -> theory -> theory (* thydata dropped at existing elems *)
3.14 val insert_fillpats: (Celem8.theID * Error_Fill_Def.fillpat list) list -> theory -> theory
3.15 - type T = (term * (Celem3.spec * (term list -> (term * term list) list))) list;
3.16 + type T = (term * (Spec.spec * (term list -> (term * term list) list))) list;
3.17 val merge = merge Celem7.cas_eq;
3.18 fun add_cas cas = Data.map (union_overwrite Celem7.cas_eq cas)
3.19 type T = Celem5.ptyps;
3.20 @@ -51,7 +51,7 @@
3.21 (Celem8.Html {guh = Celem8.part2guh ["Isabelle"], html = "",
3.22 (Celem8.Html {guh = Celem8.part2guh ["IsacScripts"], html = "",
3.23 fun check_kestore_cas ((t, (s, _)) : Celem7.cas_elem) =
3.24 - (Proof_Context.init_global @{theory})))) t ^ ", " ^ Celem3.spec2str s ^ ")";
3.25 + (Proof_Context.init_global @{theory})))) t ^ ", " ^ Spec.spec2str s ^ ")";
3.26 | count_kestore_ptyps ((Store.Ptyp (_, _, ps)) :: ps') =
3.27 fun check_kestore_ptyp' strfun (Store.Ptyp (key, pbts, pts)) = "Ptyp (" ^ (quote key) ^ ", " ^
3.28 (strfun pbts) ^ ", " ^ (map (check_kestore_ptyp' strfun) pts |> list2str) ^ ")" |> linefeed;
4.1 --- a/src/Tools/isac/BaseDefinitions/celem-1.sml Sun Apr 19 16:17:27 2020 +0200
4.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
4.3 @@ -1,100 +0,0 @@
4.4 -(* Title: BaseDefinitions/celem-1.sml
4.5 - Author: Walther Neuper
4.6 - (c) due to copyright terms
4.7 -
4.8 - *)
4.9 -signature STORE_TREE =
4.10 -(*/------- to Store -------\*)
4.11 -(*\------- to Store -------/*)
4.12 -sig
4.13 -(*/------- to Store -------\*)
4.14 - datatype 'a ptyp = Ptyp of string * 'a list * 'a ptyp list
4.15 - val merge_ptyps: 'a ptyp list * 'a ptyp list -> 'a ptyp list
4.16 - val insrt: (*pblID*)string list -> 'a -> string list -> 'a ptyp list -> 'a ptyp list
4.17 - val get_py: 'a ptyp list -> (*pblID*)string list -> string list -> 'a
4.18 - val update_ptyps: string list -> string list -> 'a -> 'a ptyp list -> 'a ptyp list
4.19 - val app_py: 'a ptyp list -> ('a ptyp -> 'b) -> (*pblID*)string list -> string list -> 'b
4.20 -(*\------- to Store -------/*)
4.21 -(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
4.22 - (*NONE*)
4.23 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
4.24 - (*NONE*)
4.25 -( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
4.26 -end
4.27 -
4.28 -(**)
4.29 -structure Store(**): STORE_TREE(**) =
4.30 -struct
4.31 -(**)
4.32 -
4.33 -(*/------- to Store -------\*)
4.34 -(* A tree for storing data defined in different theories
4.35 - for access from the Interpreter and from dialogue authoring
4.36 - using a string list as key.
4.37 - 'a is for pbt | met | thydata; after WN030424 naming "pbt" became inappropriate *)
4.38 -datatype 'a ptyp =
4.39 - Ptyp of string * (* element of the key *)
4.40 - 'a list * (* several pbts with different domIDs/thy TODO: select by subthy (isaref.p.69)
4.41 - presently only _ONE_ elem FOR ALL KINDS OF CONTENT pbt | met | thydata *)
4.42 - ('a ptyp) list; (* the children nodes *)
4.43 -
4.44 -(* this function only works wrt. the way Isabelle evaluates Theories and is not a general merge
4.45 - function for trees / ptyps *)
4.46 -fun merge_ptyps ([], pt) = pt
4.47 - | merge_ptyps (pt, []) = pt
4.48 - | merge_ptyps ((x' as Ptyp (k, _, ps)) :: xs, (xs' as Ptyp (k', y, ps') :: ys)) =
4.49 - if k = k'
4.50 - then Ptyp (k, y, merge_ptyps (ps, ps')) :: merge_ptyps (xs, ys)
4.51 - else x' :: merge_ptyps (xs, xs');
4.52 -
4.53 -fun insrt _ pbt [k] [] = [Ptyp (k, [pbt], [])]
4.54 - | insrt d pbt [k] ((Ptyp (k', [p], ps)) :: pys) =
4.55 - ((*writeln ("### insert 1: ks = " ^ strs2str [k] ^ " k'= " ^ k');*)
4.56 - if k = k'
4.57 - then ((Ptyp (k', [pbt], ps)) :: pys)
4.58 - else ((Ptyp (k', [p], ps)) :: (insrt d pbt [k] pys))
4.59 - )
4.60 - | insrt d pbt (k::ks) ((Ptyp (k', [p], ps)) :: pys) =
4.61 - ((*writeln ("### insert 2: ks = "^(strs2str (k::ks))^" k'= "^k');*)
4.62 - if k = k'
4.63 - then ((Ptyp (k', [p], insrt d pbt ks ps)) :: pys)
4.64 - else
4.65 - if length pys = 0
4.66 - then error ("insert: not found " ^ (strs2str (d(* : pblID*))))
4.67 - else ((Ptyp (k', [p], ps)) :: (insrt d pbt (k :: ks) pys))
4.68 - )
4.69 - | insrt _ _ _ _ = raise ERROR "";
4.70 -
4.71 -fun app_py p f (d(*:pblID*)) (k(*:pblRD*)) =
4.72 - let
4.73 - fun py_err _ = raise ERROR ("app_py: not found: " ^ strs2str d);
4.74 - fun app_py' _ [] = py_err ()
4.75 - | app_py' [] _ = py_err ()
4.76 - | app_py' [k0] ((p' as Ptyp (k', _, _ )) :: ps) =
4.77 - if k0 = k' then f p' else app_py' [k0] ps
4.78 - | app_py' (k' as (k0 :: ks)) (Ptyp (k'', _, ps) :: ps') =
4.79 - if k0 = k'' then app_py' ks ps else app_py' k' ps';
4.80 - in app_py' k p end;
4.81 -fun get_py p =
4.82 - let
4.83 - fun extract_py (Ptyp (_, [py], _)) = py
4.84 - | extract_py _ = raise ERROR ("extract_py: Ptyp has wrong format.");
4.85 - in app_py p extract_py end;
4.86 -
4.87 -fun update_ptyps ID _ _ [] =
4.88 - error ("update_ptyps: " ^ strs2str' ID ^ " does not exist")
4.89 - | update_ptyps ID [i] data ((py as Ptyp (key, _, pys)) :: pyss) =
4.90 - if i = key
4.91 - then
4.92 - if length pys = 0
4.93 - then ((Ptyp (key, [data], [])) :: pyss)
4.94 - else error ("update_ptyps: " ^ strs2str' ID ^ " has descendants")
4.95 - else py :: update_ptyps ID [i] data pyss
4.96 - | update_ptyps ID (i :: is) data ((py as Ptyp (key, d, pys)) :: pyss) =
4.97 - if i = key
4.98 - then ((Ptyp (key, d, update_ptyps ID is data pys)) :: pyss)
4.99 - else (py :: (update_ptyps ID (i :: is) data pyss))
4.100 - | update_ptyps _ _ _ _ = raise ERROR "update_ptyps called with undef pattern.";
4.101 -(*\------- to Store -------/*)
4.102 -
4.103 -(**)end(**)
5.1 --- a/src/Tools/isac/BaseDefinitions/celem-2.sml Sun Apr 19 16:17:27 2020 +0200
5.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
5.3 @@ -1,29 +0,0 @@
5.4 -(* Title: BaseDefinitions/celem-2.sml
5.5 - Author: Walther Neuper
5.6 - (c) due to copyright terms
5.7 -
5.8 - *)
5.9 -signature CALCELEMENT_2 =
5.10 -(*/------- to Celem2 -------\*)
5.11 -(*\------- to Celem2 -------/*)
5.12 -sig
5.13 -(*/------- to Celem2 -------\*)
5.14 - type guh
5.15 -(*\------- to Celem2 -------/*)
5.16 -(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
5.17 - (*NONE*)
5.18 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
5.19 - (*NONE*)
5.20 -( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
5.21 -end
5.22 -
5.23 -(**)
5.24 -structure Celem2(**): CALCELEMENT_2(**) =
5.25 -struct
5.26 -(**)
5.27 -
5.28 -(*/------- to Celem2 -------\*)
5.29 -type guh = string;
5.30 -(*\------- to Celem2 -------/*)
5.31 -
5.32 -(**)end(**)
6.1 --- a/src/Tools/isac/BaseDefinitions/celem-3.sml Sun Apr 19 16:17:27 2020 +0200
6.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
6.3 @@ -1,49 +0,0 @@
6.4 -(* Title: BaseDefinitions/celem-3.sml
6.5 - Author: Walther Neuper
6.6 - (c) due to copyright terms
6.7 -
6.8 - *)
6.9 -signature CALCELEMENT_3 =
6.10 -(*/------- to Celem3 -------\*)
6.11 -(*\------- to Celem3 -------/*)
6.12 -sig
6.13 -(*/------- to Celem3 -------\*)
6.14 - type metID
6.15 - type pblID
6.16 - type spec
6.17 - val spec2str: string * string list * string list -> string
6.18 - val metID2str: string list -> string
6.19 - val e_pblID: pblID
6.20 - val e_metID: metID
6.21 - val empty_spec: spec
6.22 - val e_spec: spec
6.23 -(*\------- to Celem3 -------/*)
6.24 -(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
6.25 - (*NONE*)
6.26 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
6.27 - (*NONE*)
6.28 -( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
6.29 -end
6.30 -
6.31 -(**)
6.32 -structure Celem3(**): CALCELEMENT_3(**) =
6.33 -struct
6.34 -(**)
6.35 -
6.36 -(*/------- to Celem3 -------\*)
6.37 -(*the key into the hierarchy ob problems*)
6.38 -type pblID = string list; (* domID :: ...*)
6.39 -val e_pblID = ["e_pblID"];
6.40 -
6.41 -(*the key into the hierarchy ob methods*)
6.42 -type metID = string list;
6.43 -type spec = ThyC.id * pblID * metID;
6.44 -fun spec2str (dom, pbl, met) =
6.45 - "(" ^ quote dom ^ ", " ^ strs2str pbl ^ ", " ^ strs2str met ^ ")";
6.46 -val e_metID = ["e_metID"];
6.47 -val metID2str = strs2str;
6.48 -val empty_spec = (ThyC.id_empty, e_pblID, e_metID);
6.49 -val e_spec = empty_spec;
6.50 -(*\------- to Celem3 -------/*)
6.51 -
6.52 -(**)end(**)
7.1 --- a/src/Tools/isac/BaseDefinitions/celem-5.sml Sun Apr 19 16:17:27 2020 +0200
7.2 +++ b/src/Tools/isac/BaseDefinitions/celem-5.sml Sun Apr 19 16:43:53 2020 +0200
7.3 @@ -27,16 +27,16 @@
7.4
7.5 (*/------- to Celem5 -------\*)
7.6 type pbt =
7.7 - {guh : Celem2.guh, (* unique within this isac-knowledge *)
7.8 + {guh : Spec.guh, (* unique within this isac-knowledge *)
7.9 mathauthors : string list, (* copyright *)
7.10 - init : Celem3.pblID, (* to start refinement with *)
7.11 + init : Spec.pblID, (* to start refinement with *)
7.12 thy : theory, (* which allows to compile that pbt
7.13 TODO: search generalized for subthy (ref.p.69*)
7.14 (*^^^ WN050912 NOT used during application of the problem,
7.15 because applied terms may be from 'subthy' as well as from super;
7.16 thus we take 'maxthy'; see match_ags ! *)
7.17 cas : term option, (* 'CAS-command' *)
7.18 - met : Celem3.metID list, (* methods solving the pbt *)
7.19 + met : Spec.metID list, (* methods solving the pbt *)
7.20 (*TODO: abstract to ?pre_model?...*)
7.21 prls : Rule_Set.T, (* for preds in where_ *)
7.22 where_ : term list, (* where - predicates *)
7.23 @@ -44,7 +44,7 @@
7.24 it contains "#Given","#Where","#Find","#Relate"-patterns
7.25 for constraints on identifiers see "fun cpy_nam" *)
7.26 }
7.27 -val e_pbt = {guh = "pbl_empty", mathauthors = [], init = Celem3.e_pblID, thy = Thy_Info.get_theory "Pure",
7.28 +val e_pbt = {guh = "pbl_empty", mathauthors = [], init = Spec.e_pblID, thy = Thy_Info.get_theory "Pure",
7.29 cas = NONE, prls = Rule_Set.Empty, where_ = [], ppc = [], met = []} : pbt
7.30 fun pbt2str ({cas = cas', guh = guh', init = init', mathauthors = ma', met = met', ppc = ppc',
7.31 prls = prls', thy = thy', where_ = w'} : pbt)
8.1 --- a/src/Tools/isac/BaseDefinitions/celem-6.sml Sun Apr 19 16:17:27 2020 +0200
8.2 +++ b/src/Tools/isac/BaseDefinitions/celem-6.sml Sun Apr 19 16:43:53 2020 +0200
8.3 @@ -28,9 +28,9 @@
8.4 (*/------- to Celem6 -------\*)
8.5 (* data for methods stored in 'methods'-database*)
8.6 type met =
8.7 - {guh : Celem2.guh, (* unique within this isac-knowledge *)
8.8 + {guh : Spec.guh, (* unique within this isac-knowledge *)
8.9 mathauthors: string list, (* copyright *)
8.10 - init : Celem3.pblID, (* WN060721 introduced mistakenly--TODO.REMOVE! *)
8.11 + init : Spec.pblID, (* WN060721 introduced mistakenly--TODO.REMOVE! *)
8.12 rew_ord' : Rule_Def.rew_ord', (* for rules in Detail
8.13 TODO.WN0509 store fun itself, see 'type pbt' *)
8.14 erls : Rule_Set.T, (* the eval_rls for cond. in rules FIXME "rls'
8.15 @@ -51,7 +51,7 @@
8.16 see ME/calchead.sml 'fun is_copy_named'. *)
8.17 pre : term list (* preconditions in where *)
8.18 };
8.19 -val e_met = {guh = "met_empty", mathauthors = [], init = Celem3.e_metID, rew_ord' = Rewrite_Ord.e_rew_ord',
8.20 +val e_met = {guh = "met_empty", mathauthors = [], init = Spec.e_metID, rew_ord' = Rewrite_Ord.e_rew_ord',
8.21 erls = Rule_Set.empty, srls = Rule_Set.empty, prls = Rule_Set.empty, calc = [], crls = Rule_Set.empty,
8.22 errpats = [], nrls = Rule_Set.empty, ppc = [], pre = [], scr = Rule.Empty_Prog};
8.23 val e_Mets = Store.Ptyp ("e_metID", [e_met],[]);
9.1 --- a/src/Tools/isac/BaseDefinitions/celem-7.sml Sun Apr 19 16:17:27 2020 +0200
9.2 +++ b/src/Tools/isac/BaseDefinitions/celem-7.sml Sun Apr 19 16:43:53 2020 +0200
9.3 @@ -32,7 +32,7 @@
9.4 list) (* of elements in the formalization *)
9.5 type cas_elem =
9.6 (term * (* cas-command, eg. 'solve' *)
9.7 - (Celem3.spec * (* theory, problem, method *)
9.8 + (Spec.spec * (* theory, problem, method *)
9.9 generate_fn))
9.10 fun cas_eq ((t1, (_, _)) : cas_elem, (t2, (_, _)) : cas_elem) = t1 = t2
9.11 (*\------- to Celem7 -------/*)
10.1 --- a/src/Tools/isac/BaseDefinitions/celem-8.sml Sun Apr 19 16:17:27 2020 +0200
10.2 +++ b/src/Tools/isac/BaseDefinitions/celem-8.sml Sun Apr 19 16:43:53 2020 +0200
10.3 @@ -10,25 +10,25 @@
10.4 (*/------- to Celem8 -------\*)
10.5 type authors
10.6 datatype thydata
10.7 - = Hcal of {calc: Rule_Def.calc, coursedesign: authors, guh: Celem2.guh, mathauthors: authors}
10.8 - | Hord of {coursedesign: authors, guh: Celem2.guh, mathauthors: authors, ord: (term * term) list -> term * term -> bool}
10.9 - | Hrls of {coursedesign: authors, guh: Celem2.guh, mathauthors: authors, thy_rls: ThyC.id * Rule_Set.T}
10.10 - | Hthm of {coursedesign: authors, fillpats: Error_Fill_Def.fillpat list, guh: Celem2.guh, mathauthors: authors, thm: thm}
10.11 - | Html of {coursedesign: authors, guh: Celem2.guh, html: string, mathauthors: authors}
10.12 + = Hcal of {calc: Rule_Def.calc, coursedesign: authors, guh: Spec.guh, mathauthors: authors}
10.13 + | Hord of {coursedesign: authors, guh: Spec.guh, mathauthors: authors, ord: (term * term) list -> term * term -> bool}
10.14 + | Hrls of {coursedesign: authors, guh: Spec.guh, mathauthors: authors, thy_rls: ThyC.id * Rule_Set.T}
10.15 + | Hthm of {coursedesign: authors, fillpats: Error_Fill_Def.fillpat list, guh: Spec.guh, mathauthors: authors, thm: thm}
10.16 + | Html of {coursedesign: authors, guh: Spec.guh, html: string, mathauthors: authors}
10.17 type theID
10.18 val theID2str: string list -> string
10.19 val the2str: thydata -> string
10.20 val thes2str: thydata list -> string
10.21 val theID2thyID: theID -> ThyC.id
10.22
10.23 - val part2guh: theID -> Celem2.guh
10.24 - val thy2guh: theID -> Celem2.guh
10.25 - val thypart2guh: theID -> Celem2.guh
10.26 - val thm2guh: string * ThyC.id -> ThmC_Def.id -> Celem2.guh
10.27 - val rls2guh: string * ThyC.id -> Rule_Set.id -> Celem2.guh
10.28 - val cal2guh: string * ThyC.id -> string -> Celem2.guh
10.29 - val ord2guh: string * ThyC.id -> string -> Celem2.guh
10.30 - val theID2guh: theID -> Celem2.guh
10.31 + val part2guh: theID -> Spec.guh
10.32 + val thy2guh: theID -> Spec.guh
10.33 + val thypart2guh: theID -> Spec.guh
10.34 + val thm2guh: string * ThyC.id -> ThmC_Def.id -> Spec.guh
10.35 + val rls2guh: string * ThyC.id -> Rule_Set.id -> Spec.guh
10.36 + val cal2guh: string * ThyC.id -> string -> Spec.guh
10.37 + val ord2guh: string * ThyC.id -> string -> Spec.guh
10.38 + val theID2guh: theID -> Spec.guh
10.39
10.40 val add_thydata: string list * string list -> thydata -> thydata Store.ptyp list -> thydata Store.ptyp list
10.41 val update_hthm: thydata -> Error_Fill_Def.fillpat list -> thydata
10.42 @@ -56,12 +56,12 @@
10.43 (* datatype for collecting thydata for hierarchy *)
10.44 (*WN060720 more consistent naming would be 'type thyelem' or 'thelem'*)
10.45 datatype thydata =
10.46 - Html of {guh: Celem2.guh, coursedesign: authors, mathauthors: authors, html: string}
10.47 -| Hthm of {guh: Celem2.guh, coursedesign: authors, mathauthors: authors, fillpats: Error_Fill_Def.fillpat list,
10.48 + Html of {guh: Spec.guh, coursedesign: authors, mathauthors: authors, html: string}
10.49 +| Hthm of {guh: Spec.guh, coursedesign: authors, mathauthors: authors, fillpats: Error_Fill_Def.fillpat list,
10.50 thm: thm} (* here no sym_thm, thus no thmID required *)
10.51 -| Hrls of {guh: Celem2.guh, coursedesign: authors, mathauthors: authors, thy_rls: (ThyC.id * Rule_Set.T)}
10.52 -| Hcal of {guh: Celem2.guh, coursedesign: authors, mathauthors: authors, calc: Rule_Def.calc}
10.53 -| Hord of {guh: Celem2.guh, coursedesign: authors, mathauthors: authors,
10.54 +| Hrls of {guh: Spec.guh, coursedesign: authors, mathauthors: authors, thy_rls: (ThyC.id * Rule_Set.T)}
10.55 +| Hcal of {guh: Spec.guh, coursedesign: authors, mathauthors: authors, calc: Rule_Def.calc}
10.56 +| Hord of {guh: Spec.guh, coursedesign: authors, mathauthors: authors,
10.57 ord: (UnparseC.subst -> (term * term) -> bool)};
10.58 fun the2str (Html {guh, ...}) = guh
10.59 | the2str (Hthm {guh, ...}) = guh
10.60 @@ -86,7 +86,7 @@
10.61 type thehier = (thydata Store.ptyp) list;
10.62 (* required to determine sequence of main nodes of thehier in Know_Store.thy *)
10.63 fun part2guh [str] = (case str of
10.64 - "Isabelle" => "thy_isab_" ^ str ^ "-part" : Celem2.guh
10.65 + "Isabelle" => "thy_isab_" ^ str ^ "-part" : Spec.guh
10.66 | "IsacScripts" => "thy_scri_" ^ str ^ "-part"
10.67 | "IsacKnowledge" => "thy_isac_" ^ str ^ "-part"
10.68 | str => raise ERROR ("thy2guh: called with \""^ str ^"\""))
10.69 @@ -100,7 +100,7 @@
10.70 | thy2guh theID = raise ERROR ("thy2guh called with \"" ^ strs2str' theID ^ "\"");
10.71
10.72 fun thypart2guh ([part, thyID, thypart] : theID) = (case part of
10.73 - "Isabelle" => "thy_isab_" ^ thyID ^ "-" ^ thypart : Celem2.guh
10.74 + "Isabelle" => "thy_isab_" ^ thyID ^ "-" ^ thypart : Spec.guh
10.75 | "IsacScripts" => "thy_scri_" ^ thyID ^ "-" ^ thypart
10.76 | "IsacKnowledge" => "thy_isac_" ^ thyID ^ "-" ^ thypart
10.77 | str => raise ERROR ("thypart2guh: called with '" ^ str ^ "'"))
10.78 @@ -110,28 +110,28 @@
10.79 (* convert the data got via contextToThy to a globally unique handle.
10.80 there is another way to get the guh: get out of the 'theID' in the hierarchy *)
10.81 fun thm2guh (isa, thyID) thmID = case isa of
10.82 - "Isabelle" => "thy_isab_" ^ thyID ^ "-thm-" ^ strip_thy thmID : Celem2.guh
10.83 + "Isabelle" => "thy_isab_" ^ thyID ^ "-thm-" ^ strip_thy thmID : Spec.guh
10.84 | "IsacKnowledge" => "thy_isac_" ^ thyID ^ "-thm-" ^ strip_thy thmID
10.85 | "IsacScripts" => "thy_scri_" ^ thyID ^ "-thm-" ^ strip_thy thmID
10.86 | _ => raise ERROR
10.87 ("thm2guh called with (isa, thyID) = (" ^ isa ^ ", " ^ thyID ^ ") for thm = \"" ^ thmID ^ "\"");
10.88
10.89 fun rls2guh (isa, thyID) rls' = case isa of
10.90 - "Isabelle" => "thy_isab_" ^ thyID ^ "-rls-" ^ rls' : Celem2.guh
10.91 + "Isabelle" => "thy_isab_" ^ thyID ^ "-rls-" ^ rls' : Spec.guh
10.92 | "IsacKnowledge" => "thy_isac_" ^ thyID ^ "-rls-" ^ rls'
10.93 | "IsacScripts" => "thy_scri_" ^ thyID ^ "-rls-" ^ rls'
10.94 | _ => raise ERROR
10.95 ("rls2guh called with (isa, thyID) = (" ^ isa ^ ", " ^ thyID ^ ") for rls = \"" ^ rls' ^ "\"");
10.96
10.97 fun cal2guh (isa, thyID) calID = case isa of
10.98 - "Isabelle" => "thy_isab_" ^ thyID ^ "-cal-" ^ calID : Celem2.guh
10.99 + "Isabelle" => "thy_isab_" ^ thyID ^ "-cal-" ^ calID : Spec.guh
10.100 | "IsacKnowledge" => "thy_isac_" ^ thyID ^ "-cal-" ^ calID
10.101 | "IsacScripts" => "thy_scri_" ^ thyID ^ "-cal-" ^ calID
10.102 | _ => raise ERROR
10.103 ("cal2guh called with (isa, thyID) = (" ^ isa ^ ", " ^ thyID ^ ") for cal = \"" ^ calID ^ "\"");
10.104
10.105 fun ord2guh (isa, thyID) rew_ord' = case isa of
10.106 - "Isabelle" => "thy_isab_" ^ thyID ^ "-ord-" ^ rew_ord' : Celem2.guh
10.107 + "Isabelle" => "thy_isab_" ^ thyID ^ "-ord-" ^ rew_ord' : Spec.guh
10.108 | "IsacKnowledge" => "thy_isac_" ^ thyID ^ "-ord-" ^ rew_ord'
10.109 | "IsacScripts" => "thy_scri_" ^ thyID ^ "-ord-" ^ rew_ord'
10.110 | _ => raise ERROR
11.1 --- a/src/Tools/isac/BaseDefinitions/celem-91.sml Sun Apr 19 16:17:27 2020 +0200
11.2 +++ b/src/Tools/isac/BaseDefinitions/celem-91.sml Sun Apr 19 16:43:53 2020 +0200
11.3 @@ -9,10 +9,10 @@
11.4 sig
11.5 (*/------- to Celem91 -------\*)
11.6 val check_guhs_unique: bool Unsynchronized.ref
11.7 - val check_pblguh_unique: Celem2.guh -> Celem5.pbt Store.ptyp list -> unit
11.8 - val check_metguh_unique: Celem2.guh -> Celem6.met Store.ptyp list -> unit
11.9 - val coll_pblguhs: Celem5.pbt Store.ptyp list -> Celem2.guh list
11.10 - val coll_metguhs: Celem6.met Store.ptyp list -> Celem2.guh list
11.11 + val check_pblguh_unique: Spec.guh -> Celem5.pbt Store.ptyp list -> unit
11.12 + val check_metguh_unique: Spec.guh -> Celem6.met Store.ptyp list -> unit
11.13 + val coll_pblguhs: Celem5.pbt Store.ptyp list -> Spec.guh list
11.14 + val coll_metguhs: Celem6.met Store.ptyp list -> Spec.guh list
11.15 (*\------- to Celem91 -------/*)
11.16 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
11.17 (*NONE*)
11.18 @@ -34,7 +34,7 @@
11.19
11.20 fun coll_pblguhs pbls =
11.21 let
11.22 - fun node coll (Store.Ptyp (_, [n], ns)) = [(#guh : Celem5.pbt -> Celem2.guh) n] @ (nodes coll ns)
11.23 + fun node coll (Store.Ptyp (_, [n], ns)) = [(#guh : Celem5.pbt -> Spec.guh) n] @ (nodes coll ns)
11.24 | node _ _ = raise ERROR "coll_pblguhs - node"
11.25 and nodes coll [] = coll
11.26 | nodes coll (n :: ns) = (node coll n) @ (nodes coll ns);
11.27 @@ -47,12 +47,12 @@
11.28 else ();
11.29 fun coll_metguhs mets =
11.30 let
11.31 - fun node coll (Store.Ptyp (_, [n], ns)) = [(#guh : Celem6.met -> Celem2.guh) n] @ (nodes coll ns)
11.32 + fun node coll (Store.Ptyp (_, [n], ns)) = [(#guh : Celem6.met -> Spec.guh) n] @ (nodes coll ns)
11.33 | node _ _ = raise ERROR "coll_pblguhs - node"
11.34 and nodes coll [] = coll
11.35 | nodes coll (n :: ns) = (node coll n) @ (nodes coll ns);
11.36 in nodes [] mets end;
11.37 -fun check_metguh_unique (guh: Celem2.guh) (mets: (Celem6.met Store.ptyp) list) =
11.38 +fun check_metguh_unique (guh: Spec.guh) (mets: (Celem6.met Store.ptyp) list) =
11.39 if member op = (coll_metguhs mets) guh
11.40 then raise ERROR ("check_guh_unique failed with \"" ^ guh ^"\";\n"^
11.41 (*"use \"sort_metguhs()\" for a list of guhs;\n" ^ ...evaluates to [] ?!?*)
12.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
12.2 +++ b/src/Tools/isac/BaseDefinitions/specification.sml Sun Apr 19 16:43:53 2020 +0200
12.3 @@ -0,0 +1,53 @@
12.4 +(* Title: BaseDefinitions/celem-3.sml
12.5 + Author: Walther Neuper
12.6 + (c) due to copyright terms
12.7 +
12.8 +
12.9 +*)
12.10 +signature SPECIFICATION =
12.11 +sig
12.12 + type guh
12.13 + type metID
12.14 + type pblID
12.15 + type spec
12.16 + val spec2str: string * string list * string list -> string
12.17 + val metID2str: string list -> string
12.18 + val e_pblID: pblID
12.19 + val e_metID: metID
12.20 + val empty_spec: spec
12.21 + val e_spec: spec
12.22 +(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
12.23 + (*NONE*)
12.24 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
12.25 + (*NONE*)
12.26 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
12.27 +end
12.28 +
12.29 +(**)
12.30 +structure Spec(**): SPECIFICATION(**) =
12.31 +struct
12.32 +(**)
12.33 +
12.34 +(*
12.35 +The last remainder from Klaus Schmaranz' Dinopolis Project, which used "globally unique handles"
12.36 +abbreviated "guh". These are used for files names; can be dropped with switch to Isabelle/PIDE.
12.37 +*)
12.38 +type guh = string;
12.39 +
12.40 +(*/------- to Spec -------\*)
12.41 +(*the key into the hierarchy ob problems*)
12.42 +type pblID = string list; (* domID :: ...*)
12.43 +val e_pblID = ["e_pblID"];
12.44 +
12.45 +(*the key into the hierarchy ob methods*)
12.46 +type metID = string list;
12.47 +type spec = ThyC.id * pblID * metID;
12.48 +fun spec2str (dom, pbl, met) =
12.49 + "(" ^ quote dom ^ ", " ^ strs2str pbl ^ ", " ^ strs2str met ^ ")";
12.50 +val e_metID = ["e_metID"];
12.51 +val metID2str = strs2str;
12.52 +val empty_spec = (ThyC.id_empty, e_pblID, e_metID);
12.53 +val e_spec = empty_spec;
12.54 +(*\------- to Spec -------/*)
12.55 +
12.56 +(**)end(**)
13.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
13.2 +++ b/src/Tools/isac/BaseDefinitions/store.sml Sun Apr 19 16:43:53 2020 +0200
13.3 @@ -0,0 +1,97 @@
13.4 +(* Title: BaseDefinitions/store.sml
13.5 + Author: Walther Neuper
13.6 + (c) due to copyright terms
13.7 +
13.8 +A tree for storing collections of Problem, Method and Thy_Html.
13.9 +*)
13.10 +signature STORE_TREE =
13.11 +sig
13.12 + datatype 'a ptyp = Ptyp of string * 'a list * 'a ptyp list
13.13 + val merge_ptyps: 'a ptyp list * 'a ptyp list -> 'a ptyp list
13.14 + val insrt: (*pblID*)string list -> 'a -> string list -> 'a ptyp list -> 'a ptyp list
13.15 + val get_py: 'a ptyp list -> (*pblID*)string list -> string list -> 'a
13.16 + val update_ptyps: string list -> string list -> 'a -> 'a ptyp list -> 'a ptyp list
13.17 + val app_py: 'a ptyp list -> ('a ptyp -> 'b) -> (*pblID*)string list -> string list -> 'b
13.18 +(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
13.19 + (*NONE*)
13.20 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
13.21 + (*NONE*)
13.22 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
13.23 +end
13.24 +
13.25 +(**)
13.26 +structure Store(**): STORE_TREE(**) =
13.27 +struct
13.28 +(**)
13.29 +
13.30 +(*/------- to Store -------\*)
13.31 +(* A tree for storing data defined in different theories
13.32 + for access from the Interpreter and from dialogue authoring
13.33 + using a string list as key.
13.34 + 'a is for pbt | met | thydata; after WN030424 naming "pbt" became inappropriate *)
13.35 +datatype 'a ptyp =
13.36 + Ptyp of string * (* element of the key *)
13.37 + 'a list * (* several pbts with different domIDs/thy TODO: select by subthy (isaref.p.69)
13.38 + presently only _ONE_ elem FOR ALL KINDS OF CONTENT pbt | met | thydata *)
13.39 + ('a ptyp) list; (* the children nodes *)
13.40 +
13.41 +(* this function only works wrt. the way Isabelle evaluates Theories and is not a general merge
13.42 + function for trees / ptyps *)
13.43 +fun merge_ptyps ([], pt) = pt
13.44 + | merge_ptyps (pt, []) = pt
13.45 + | merge_ptyps ((x' as Ptyp (k, _, ps)) :: xs, (xs' as Ptyp (k', y, ps') :: ys)) =
13.46 + if k = k'
13.47 + then Ptyp (k, y, merge_ptyps (ps, ps')) :: merge_ptyps (xs, ys)
13.48 + else x' :: merge_ptyps (xs, xs');
13.49 +
13.50 +fun insrt _ pbt [k] [] = [Ptyp (k, [pbt], [])]
13.51 + | insrt d pbt [k] ((Ptyp (k', [p], ps)) :: pys) =
13.52 + ((*writeln ("### insert 1: ks = " ^ strs2str [k] ^ " k'= " ^ k');*)
13.53 + if k = k'
13.54 + then ((Ptyp (k', [pbt], ps)) :: pys)
13.55 + else ((Ptyp (k', [p], ps)) :: (insrt d pbt [k] pys))
13.56 + )
13.57 + | insrt d pbt (k::ks) ((Ptyp (k', [p], ps)) :: pys) =
13.58 + ((*writeln ("### insert 2: ks = "^(strs2str (k::ks))^" k'= "^k');*)
13.59 + if k = k'
13.60 + then ((Ptyp (k', [p], insrt d pbt ks ps)) :: pys)
13.61 + else
13.62 + if length pys = 0
13.63 + then error ("insert: not found " ^ (strs2str (d(* : pblID*))))
13.64 + else ((Ptyp (k', [p], ps)) :: (insrt d pbt (k :: ks) pys))
13.65 + )
13.66 + | insrt _ _ _ _ = raise ERROR "";
13.67 +
13.68 +fun app_py p f (d(*:pblID*)) (k(*:pblRD*)) =
13.69 + let
13.70 + fun py_err _ = raise ERROR ("app_py: not found: " ^ strs2str d);
13.71 + fun app_py' _ [] = py_err ()
13.72 + | app_py' [] _ = py_err ()
13.73 + | app_py' [k0] ((p' as Ptyp (k', _, _ )) :: ps) =
13.74 + if k0 = k' then f p' else app_py' [k0] ps
13.75 + | app_py' (k' as (k0 :: ks)) (Ptyp (k'', _, ps) :: ps') =
13.76 + if k0 = k'' then app_py' ks ps else app_py' k' ps';
13.77 + in app_py' k p end;
13.78 +fun get_py p =
13.79 + let
13.80 + fun extract_py (Ptyp (_, [py], _)) = py
13.81 + | extract_py _ = raise ERROR ("extract_py: Ptyp has wrong format.");
13.82 + in app_py p extract_py end;
13.83 +
13.84 +fun update_ptyps ID _ _ [] =
13.85 + error ("update_ptyps: " ^ strs2str' ID ^ " does not exist")
13.86 + | update_ptyps ID [i] data ((py as Ptyp (key, _, pys)) :: pyss) =
13.87 + if i = key
13.88 + then
13.89 + if length pys = 0
13.90 + then ((Ptyp (key, [data], [])) :: pyss)
13.91 + else error ("update_ptyps: " ^ strs2str' ID ^ " has descendants")
13.92 + else py :: update_ptyps ID [i] data pyss
13.93 + | update_ptyps ID (i :: is) data ((py as Ptyp (key, d, pys)) :: pyss) =
13.94 + if i = key
13.95 + then ((Ptyp (key, d, update_ptyps ID is data pys)) :: pyss)
13.96 + else (py :: (update_ptyps ID (i :: is) data pyss))
13.97 + | update_ptyps _ _ _ _ = raise ERROR "update_ptyps called with undef pattern.";
13.98 +(*\------- to Store -------/*)
13.99 +
13.100 +(**)end(**)
14.1 --- a/src/Tools/isac/BridgeLibisabelle/BridgeLibisabelle.thy Sun Apr 19 16:17:27 2020 +0200
14.2 +++ b/src/Tools/isac/BridgeLibisabelle/BridgeLibisabelle.thy Sun Apr 19 16:43:53 2020 +0200
14.3 @@ -6,7 +6,7 @@
14.4 theory BridgeLibisabelle
14.5 imports "~~/src/Tools/isac/MathEngine/MathEngine"
14.6 begin
14.7 - ML_file mathml.sml
14.8 + ML_file mathml.sml
14.9 ML_file datatypes.sml
14.10 ML_file "pbl-met-hierarchy.sml"
14.11 ML_file "thy-hierarchy.sml"