1.1 --- a/TODO.md Sat Oct 08 15:57:10 2022 +0200
1.2 +++ b/TODO.md Sat Oct 08 19:17:24 2022 +0200
1.3 @@ -62,24 +62,17 @@
1.4
1.5 ***** priority of WN items is top down, most urgent/simple on top
1.6
1.7 -* WN: follow up 5b: clarify TermC.parse_patt/*_PIDE analogous to TermC.parse_strict/*_PIDE
1.8 +* WN: follow up 5d: clarify TermC.parse_patt/*_PIDE analogous to TermC.parse_strict/*_PIDE
1.9 follow up 6: ctxt_user at init Example mimiced by CalcTreeTest @{context}
1.10 Thus eliminate use of Thy_Info.get_theory
1.11 follow up 7: ANSWER: represent items, which have not yet been input IN VSCode_Example.thy WITH "__"
1.12
1.13 * WN: improve naming in refine.sml, m-match.sml
1.14 * WN: rename ‹ML_structure KEStore_Elems› to ‹ML_structure Know_Store›
1.15 -* WN: eliminate KEStore_Elems.get_thes, add_thes
1.16 -* What is the idea behind KEStore_Elems.add_thes? How to do it properly in current Isabelle?
1.17 - See notes in Build_Thydata.thy.
1.18 - https://static.miraheze.org/isacwiki/0/04/Isac-docu.pdf distinguishes
1.19 - several kinds of ISAC users, in particular "math author (Mathematik-Autor)" and
1.20 - "course designer (Kurs-Designer)". The latter just adds examples which re-use existing
1.21 - knowledge designed by the former. KEStore_Elems.add_thes is an interface for the latter.
1.22 - KEStore_Elems.get_thes and KEStore_Elems.add_thes are ONLY required for the Lucas-Interpreter
1.23 - retrieving Thm and Rls from string-identifiers (which do NOT indicate the theory of) --
1.24 - -- get_thes and add_thes are the main reason for (b)
1.25 - So: How can KEStore_Elems.get_thes and KEStore_Elems.add_thes be replaced in current Isabelle?
1.26 +* WN: KEStore_Elems.get_thes, add_thes still required for Error_Patterns, we want to eliminate thes:
1.27 + (1) Error_Pattern.T are already stored by MethodC -- place them in respective thys
1.28 + (2) Error_Pattern.fill_in stored with thm (in thes): instead introduce new Thy_Data for them.
1.29 + adapt KEStore_Elems.insert_fillpats for that purpose.
1.30
1.31 * WN: Specify/formalise.sml is in BaseDefinitions/ AND Specify/ DELETE ONE VERSION
1.32 * WN: Step_Specify.initialise: remove hdl in return-value, replace Step_Specify.nxt_specify_init_calc
2.1 --- a/src/Tools/isac/BaseDefinitions/Know_Store.thy Sat Oct 08 15:57:10 2022 +0200
2.2 +++ b/src/Tools/isac/BaseDefinitions/Know_Store.thy Sat Oct 08 19:17:24 2022 +0200
2.3 @@ -85,7 +85,7 @@
2.4 val get_expls: theory -> Example.store
2.5 val add_expls: (Example.T * Store.key) list -> theory -> theory
2.6 val get_thes: theory -> (Thy_Write.thydata Store.node) list
2.7 - val add_thes: (Thy_Write.thydata * Thy_Write.theID) list -> theory -> theory (* thydata dropped at existing elems *)
2.8 + val add_thes: (Thy_Write.thydata * Thy_Write.theID) list -> theory -> theory
2.9 val insert_fillpats: (Thy_Write.theID * Error_Pattern_Def.fill_in list) list -> theory -> theory
2.10 val get_ref_thy: unit -> theory
2.11 val set_ref_thy: theory -> unit
2.12 @@ -175,7 +175,7 @@
2.13 type T = (Thy_Write.thydata Store.node) list;
2.14 val empty = [];
2.15 val extend = I;
2.16 - val merge = Store.merge; (* relevant for store_thm, store_rls *)
2.17 + val merge = Store.merge;
2.18 );
2.19 fun get_thes thy = Data.get thy
2.20 fun add_thes thes thy = let
3.1 --- a/src/Tools/isac/BridgeLibisabelle/interface.sml Sat Oct 08 15:57:10 2022 +0200
3.2 +++ b/src/Tools/isac/BridgeLibisabelle/interface.sml Sat Oct 08 19:17:24 2022 +0200
3.3 @@ -147,7 +147,11 @@
3.4 let
3.5 val _ = States.upd_tacis cI tacis
3.6 val (tac, _, _) = last_elem tacis
3.7 - in fetchproposedtacticOK2xml cI tac (Error_Pattern.from_store tac) end
3.8 + in
3.9 + fetchproposedtacticOK2xml cI tac (Error_Pattern.from_store
3.10 + (Proof_Context.init_global (ThyC.get_theory "Isac_Knowledge")) tac)
3.11 + (*ctxt shallt become an argument ^^^^^^^^ of fetchProposedTactic*)
3.12 + end
3.13 | ("helpless", _) => fetchproposedtacticERROR2xml cI "helpless"
3.14 | ("no-fmz-spec", _) => fetchproposedtacticERROR2xml cI "no-fmz-spec"
3.15 | ("end-of-calculation", _) => fetchproposedtacticERROR2xml cI "end-of-calculation"
4.1 --- a/src/Tools/isac/BridgeLibisabelle/thy-hierarchy.sml Sat Oct 08 15:57:10 2022 +0200
4.2 +++ b/src/Tools/isac/BridgeLibisabelle/thy-hierarchy.sml Sat Oct 08 19:17:24 2022 +0200
4.3 @@ -157,7 +157,7 @@
4.4
4.5 fun insert_errpatIDs _(*thy*) theID errpatIDs = (* TODO: redo like insert_fillpatts *)
4.6 let
4.7 - val hrls = Thy_Read.from_store theID
4.8 + val hrls = Thy_Read.for_thy_hierarchy theID
4.9 val hrls' = update_hrls hrls errpatIDs
4.10 handle ERROR _ => raise ERROR ("insert_errpatIDs: " ^ strs2str theID ^ "must address a rule-set")
4.11 in (hrls', theID) end
5.1 --- a/src/Tools/isac/Interpret/error-pattern.sml Sat Oct 08 15:57:10 2022 +0200
5.2 +++ b/src/Tools/isac/Interpret/error-pattern.sml Sat Oct 08 19:17:24 2022 +0200
5.3 @@ -20,7 +20,7 @@
5.4
5.5 type record
5.6
5.7 - val from_store: Tactic.input -> Error_Pattern_Def.id list
5.8 + val from_store: Proof.context -> Tactic.input -> Error_Pattern_Def.id list
5.9 val filled_exactly: Calc.T -> string -> string * Tactic.input
5.10 val check_for: Proof.context -> term * term -> term * Env.T -> T list * Rule_Set.T -> id option
5.11
5.12 @@ -110,7 +110,7 @@
5.13 val thmDeriv = Thm.get_name_hint thm
5.14 val (part, thyID) = Thy_Read.thy_containing_thm thmDeriv
5.15 val theID = [part, thyID, "Theorems", ThmC.cut_id thmDeriv]
5.16 - val fillpats = case Thy_Read.from_store theID of
5.17 + val fillpats = case Thy_Read.from_store ctxt theID of
5.18 Thy_Write.Hthm {fillpats, ...} => fillpats
5.19 | _ => raise ERROR "fill_from_store: uncovered case of get_the"
5.20 val some = map (fill_form ctxt subst (thm, form) id) fillpats
5.21 @@ -161,7 +161,7 @@
5.22 end
5.23
5.24 (* fetch errpatIDs from an arbitrary tactic *)
5.25 -fun from_store tac =
5.26 +fun from_store ctxt tac =
5.27 let
5.28 val rlsID =
5.29 case tac of
5.30 @@ -169,7 +169,7 @@
5.31 |Tactic.Rewrite_Set_Inst (_, rlsID) => rlsID
5.32 | _ => "empty"
5.33 val (part, thyID) = Thy_Read.thy_containing_rls "Isac_Knowledge" rlsID;
5.34 - val rls = case Thy_Read.from_store [part, thyID, "Rulesets", rlsID] of
5.35 + val rls = case Thy_Read.from_store ctxt [part, thyID, "Rulesets", rlsID] of
5.36 Thy_Write.Hrls {thy_rls = (_, rls), ...} => rls
5.37 | _ => raise ERROR "from_store: uncovered case of get_the"
5.38 in case rls of
6.1 --- a/src/Tools/isac/Interpret/thy-read.sml Sat Oct 08 15:57:10 2022 +0200
6.2 +++ b/src/Tools/isac/Interpret/thy-read.sml Sat Oct 08 19:17:24 2022 +0200
6.3 @@ -11,7 +11,8 @@
6.4 val thy_containing_rls : ThyC.id -> Rule_Set.id -> string * ThyC.id
6.5 val thy_containing_cal : ThyC.id -> Eval_Def.prog_id -> string * string
6.6
6.7 - val from_store : Thy_Write.theID -> Thy_Write.thydata (* for inform.sml *)
6.8 + val for_thy_hierarchy : Thy_Write.theID -> Thy_Write.thydata (* for inform.sml *)
6.9 + val from_store : Proof.context -> Thy_Write.theID -> Thy_Write.thydata (* for inform.sml *)
6.10 \<^isac_test>\<open>
6.11 val isabthys: unit -> theory list
6.12 val knowthys: unit -> theory list
6.13 @@ -103,6 +104,22 @@
6.14 | _ => raise ERROR ("thy_containing_cal : rls '" ^ sop ^ "' not in ancestors of thy '" ^ thy' ^ "'")
6.15 end
6.16
6.17 -fun from_store theID = Store.get (get_thes ()) theID theID;
6.18 +fun for_thy_hierarchy theID = Store.get (get_thes ()) theID theID;
6.19 +
6.20 +(* adapt_fillpat: Proof.context -> Error_Pattern.fill_in -> Error_Pattern.fill_in*)
6.21 +fun adapt_fillpat ctxt (fill_in_id, term, id) =
6.22 + (fill_in_id, Model_Pattern.adapt_term_to_type ctxt term, id)
6.23 +
6.24 +fun adapt_to_type ctxt (Thy_Write.Hthm {coursedesign, fillpats, guh, mathauthors, thm}) =
6.25 + (Thy_Write.Hthm {coursedesign = coursedesign, fillpats = (map (adapt_fillpat ctxt)) fillpats,
6.26 + guh = guh, mathauthors = mathauthors, thm = thm})
6.27 + | adapt_to_type _ the = the;
6.28 +
6.29 +fun from_store ctxt id =
6.30 + let
6.31 + val the = Store.get (get_thes ()) id id
6.32 + in adapt_to_type ctxt the end
6.33 + handle ERROR _ =>
6.34 + raise error ("*** ERROR Thy_Read.from_store ctxt " ^ strs2str id ^ " not found");
6.35
6.36 (**)end(**)
7.1 --- a/test/Tools/isac/Interpret/error-pattern.sml Sat Oct 08 15:57:10 2022 +0200
7.2 +++ b/test/Tools/isac/Interpret/error-pattern.sml Sat Oct 08 19:17:24 2022 +0200
7.3 @@ -1101,12 +1101,12 @@
7.4 then () else error "find_fill_patterns changed 1a"
7.5 | _ => error "find_fill_patterns changed 1b"
7.6
7.7 -"~~~~~ fun fill_from_store, args:"; val (subst, form, errpatID, thm) =
7.8 - (subst, f_curr, errpatID, hd (*simulate beginning of "map"*) errpatthms);
7.9 +"~~~~~ fun fill_from_store, args:"; val (ctxt, subst, form, errpatID, thm) =
7.10 + (ctxt, subst, f_curr, errpatID, hd (*simulate beginning of "map"*) errpatthms);
7.11 val thmDeriv = Thm.get_name_hint thm
7.12 val (part, thyID) = Thy_Read.thy_containing_thm thmDeriv
7.13 val theID = [part, thyID, "Theorems", ThmC.cut_id thmDeriv]
7.14 - val Thy_Write.Hthm {fillpats, ...} = Thy_Read.from_store theID
7.15 + val Thy_Write.Hthm {fillpats, ...} = Thy_Read.from_store ctxt theID
7.16 val some = map (Error_Pattern.fill_form ctxt subst (thm, form) errpatID) fillpats;
7.17
7.18 case some |> filter is_some |> map the of