# HG changeset patch # User wneuper # Date 1673425398 -3600 # Node ID b2ff1902420fe97f8662e1d8403209f2930c1e28 # Parent 976b99bcfc96eff3788ba5396bce0d799ca4f4ff eliminate use of Thy_Info 12: prep.arg. ctxt in TermC, UnparseC diff -r 976b99bcfc96 -r b2ff1902420f src/Tools/isac/BaseDefinitions/Know_Store.thy --- a/src/Tools/isac/BaseDefinitions/Know_Store.thy Wed Jan 11 06:06:12 2023 +0100 +++ b/src/Tools/isac/BaseDefinitions/Know_Store.thy Wed Jan 11 09:23:18 2023 +0100 @@ -86,7 +86,8 @@ val get_ref_last_thy: unit -> theory val set_ref_last_thy: theory -> unit val get_via_last_thy: ThyC.id -> theory (*only used for * (Sub-)problem retrieving respective thy - * problem refinement *) + * problem refinement + * (test-)code to be deleted *) end; structure Know_Store(**): KNOW_STORE(**) = diff -r 976b99bcfc96 -r b2ff1902420f src/Tools/isac/BaseDefinitions/termC.sml --- a/src/Tools/isac/BaseDefinitions/termC.sml Wed Jan 11 06:06:12 2023 +0100 +++ b/src/Tools/isac/BaseDefinitions/termC.sml Wed Jan 11 09:23:18 2023 +0100 @@ -99,21 +99,24 @@ val dest_list': term -> term list val negates: term -> term -> bool -\<^isac_test>\ + val contains_one_of: thm * (string * typ) list -> bool + val contains_Const_typeless: term list -> term -> bool + val sym_trm : term -> term (* unused code, kept as hints to design ideas *) + +(*isac_test*) val mk_negative: typ -> term -> term + val free2var: term -> term val scala_of_term: term -> string - val atomtyp(*<-- atom_typ TODO*): typ -> unit + +(*val atom_typ: typ -> unit RENAME*) + val atomtyp: typ -> unit val atomty: term -> unit val atomw: term -> unit val atomt: term -> unit val atomwy: term -> unit - val atomty_thy: ThyC.id -> term -> unit - val free2var: term -> term + +\<^isac_test>\ \ - val contains_one_of: thm * (string * typ) list -> bool - val contains_Const_typeless: term list -> term -> bool -(*----- unused code, kept as hints to design ideas ---------------------------------------------*) - val sym_trm : term -> term end (**) @@ -148,8 +151,7 @@ handle Pattern.MATCH => false (** transform typ / term to a String to be parsed by Scala after transport via libisabelle **) - -\<^isac_test>\ +(*isac_test*) fun scala_of_typ (Type (s, typs)) = enclose "Type(" ")" (quote s ^ ", " ^ (typs |> map scala_of_typ |> commas |> enclose "List(" ")")) @@ -202,40 +204,28 @@ fun atomw t = writeln ("\n*** -------------" ^ ato t 0 ^ "\n***"); fun atomt t = tracing ("\n*** -------------" ^ ato t 0 ^ "\n***"); end; + +\<^isac_test>\ \ fun term_detail2str t = - let - fun ato (Const (a, T)) n = "\n*** " ^ indent n ^ "Const (" ^ a ^ ", " ^ UnparseC.typ T ^ ")" - | ato (Free (a, T)) n = "\n*** " ^ indent n ^ "Free (" ^ a ^ ", " ^ UnparseC.typ T ^ ")" + let + val ctxt = "Isac_Knowledge" |> Know_Store.get_via_last_thy |> Proof_Context.init_global + fun ato (Const (a, T)) n = "\n*** " ^ indent n ^ "Const (" ^ a ^ ", " ^ UnparseC.typ_in_ctxt ctxt T ^ ")" + | ato (Free (a, T)) n = "\n*** " ^ indent n ^ "Free (" ^ a ^ ", " ^ UnparseC.typ_in_ctxt ctxt T ^ ")" | ato (Var ((a, i), T)) n = - "\n*** " ^ indent n ^ "Var ((" ^ a ^ ", " ^ string_of_int i ^ "), " ^ UnparseC.typ T ^ ")" + "\n*** " ^ indent n ^ "Var ((" ^ a ^ ", " ^ string_of_int i ^ "), " ^ UnparseC.typ_in_ctxt ctxt T ^ ")" | ato (Bound i) n = "\n*** " ^ indent n ^ "Bound " ^ string_of_int i | ato (Abs(a, T, body)) n = - "\n*** " ^ indent n ^ "Abs (" ^ a ^ ", " ^ UnparseC.typ T ^ ",.." ^ ato body (n + 1) + "\n*** " ^ indent n ^ "Abs (" ^ a ^ ", " ^ UnparseC.typ_in_ctxt ctxt T ^ ",.." ^ ato body (n + 1) | ato (f $ t) n = ato f n ^ ato t (n + 1) in "\n*** " ^ ato t 0 ^ "\n***" end; -\<^isac_test>\ -fun term_detail2str_thy thy t = - let - fun ato (Const (a, T)) n = - "\n*** " ^ indent n ^ "Const (" ^ a ^ ", " ^ UnparseC.typ_by_thyID thy T ^ ")" - | ato (Free (a, T)) n = - "\n*** " ^ indent n ^ "Free (" ^ a ^ ", " ^ UnparseC.typ_by_thyID thy T ^ ")" - | ato (Var ((a, i), T)) n = - "\n*** " ^ indent n ^ "Var ((" ^ a ^ ", " ^ string_of_int i ^ "), " ^ - UnparseC.typ_by_thyID thy T ^ ")" - | ato (Bound i) n = - "\n*** " ^ indent n ^ "Bound " ^ string_of_int i - | ato (Abs(a, T, body)) n = - "\n*** " ^ indent n ^ "Abs (" ^ a ^ ", " ^ UnparseC.typ_by_thyID thy T ^ ",.." ^ - ato body (n + 1) - | ato (f $ t) n = ato f n ^ ato t (n + 1) - in "\n*** " ^ ato t 0 ^ "\n***" end; +(*isac_test*) fun atomwy t = (writeln o term_detail2str) t; fun atomty t = (tracing o term_detail2str) t; -fun atomty_thy thy t = (tracing o (term_detail2str_thy thy)) t; + +\<^isac_test>\ \ (* contains the term a VAR(("*",_),_) ? *) @@ -375,7 +365,7 @@ | var2free (Abs(s, T, t)) = Abs(s, T, var2free t) | var2free (t1 $ t2) = (var2free t1) $ (var2free t2); -\<^isac_test>\ +(*isac_test*) (* Logic.varify does NOT take care of 'Free ("1", _)'*) fun free2var (t as Const _) = t | free2var (t as Free (s, T)) = if is_num' s then t else Var ((s, 0), T) @@ -383,6 +373,8 @@ | free2var (t as Bound _) = t | free2var (Abs (s, T, t)) = Abs (s, T, free2var t) | free2var (t1 $ t2) = (free2var t1) $ (free2var t2); + +\<^isac_test>\ \ fun mk_listT T = Type (\<^type_name>\list\, [T]); diff -r 976b99bcfc96 -r b2ff1902420f src/Tools/isac/BaseDefinitions/unparseC.sml --- a/src/Tools/isac/BaseDefinitions/unparseC.sml Wed Jan 11 06:06:12 2023 +0100 +++ b/src/Tools/isac/BaseDefinitions/unparseC.sml Wed Jan 11 09:23:18 2023 +0100 @@ -27,12 +27,8 @@ (*val terms_short: Proof.context -> term list -> term_as_string*) val terms_short: term list -> term_as_string - (*val typ: Proof.context -> typ -> term_as_string*) val typ_in_ctxt: Proof.context -> typ -> term_as_string - val typ: typ -> term_as_string -(*replace by ^^^*) - val typ_by_thyID: ThyC.id -> typ -> term_as_string \<^isac_test>\ val term_by_thyID: ThyC.id -> term -> term_as_string @@ -76,16 +72,6 @@ fun term_opt (SOME t) = "(SOME " ^ term t ^ ")" | term_opt NONE = "NONE"; -fun type_to_string'' (thyID : ThyC.id) t = - let - val ctxt' = Config.put show_markup false (Proof_Context.init_global - (ThyC.get_theory thyID)) - in - Print_Mode.setmp [] (Syntax.string_of_typ ctxt') t - end; -fun typ typ = type_to_string'' "Isac_Knowledge" typ; (*TODO legacy*) -fun typ_by_thyID thy typ = type_to_string'' thy typ; (*legacy*) - fun type_to_string' ctxt typ = Print_Mode.setmp [] (Syntax.string_of_typ ctxt) typ fun typ_in_ctxt ctxt typ = type_to_string' ctxt typ diff -r 976b99bcfc96 -r b2ff1902420f src/Tools/isac/BridgeLibisabelle/datatypes.sml --- a/src/Tools/isac/BridgeLibisabelle/datatypes.sml Wed Jan 11 06:06:12 2023 +0100 +++ b/src/Tools/isac/BridgeLibisabelle/datatypes.sml Wed Jan 11 09:23:18 2023 +0100 @@ -159,7 +159,7 @@ map xml_of_sub (Tactic.subst_adapt_to_type (ThyC.id_to_ctxt "Isac_Knowledge") subs)) fun xml_of_sube sube = XML.Elem (("SUBSTITUTION", []), - map xml_of_sub (Subst.T_from_string_eqs (ThyC.get_theory "Isac_Knowledge") sube)) + map xml_of_sub (Subst.T_from_string_eqs (Know_Store.get_via_last_thy "Isac_Knowledge") sube)) fun thm''2xml j (thm : thm) = indt j ^ "\n" ^ diff -r 976b99bcfc96 -r b2ff1902420f src/Tools/isac/BridgeLibisabelle/present-tool.sml --- a/src/Tools/isac/BridgeLibisabelle/present-tool.sml Wed Jan 11 06:06:12 2023 +0100 +++ b/src/Tools/isac/BridgeLibisabelle/present-tool.sml Wed Jan 11 09:23:18 2023 +0100 @@ -76,7 +76,8 @@ EXCEPT theory hierarchy ... compare 'fun keref2xml' *) fun pblID2guh ctxt pblID = (((#guh o (Problem.from_store ctxt)) pblID) handle ERROR _ => raise ERROR ("Ptool.pblID2guh: not for \"" ^ strs2str' pblID ^ "\"")); -fun metID2guh metID = (((#guh o MethodC.from_store ("Isac_Knowledge" |> ThyC.get_theory |> Proof_Context.init_global)) metID) +fun metID2guh metID = + (((#guh o MethodC.from_store ("Isac_Knowledge" |> Know_Store.get_via_last_thy |> Proof_Context.init_global)) metID) handle ERROR _ => raise ERROR ("metID2guh: no 'Met_' for \"" ^ strs2str' metID ^ "\"")); fun kestoreID2guh ctxt Pbl_ kestoreID = pblID2guh ctxt kestoreID | kestoreID2guh _ Met_ kestoreID = metID2guh kestoreID diff -r 976b99bcfc96 -r b2ff1902420f src/Tools/isac/MathEngBasic/ctree-basic.sml --- a/src/Tools/isac/MathEngBasic/ctree-basic.sml Wed Jan 11 06:06:12 2023 +0100 +++ b/src/Tools/isac/MathEngBasic/ctree-basic.sml Wed Jan 11 09:23:18 2023 +0100 @@ -817,7 +817,7 @@ (* get the theory explicitly just for the rootpbl; thus use this function _after_ finishing specification *) -fun root_thy (Nd (PblObj {spec = (thyID, _, _), ...}, _)) = Know_Store.get_via_last_thy thyID +fun root_thy (Nd (PblObj {spec = (thyID, _, _), ctxt, ...}, _)) = ThyC.get_theory_PIDE ctxt thyID | root_thy _ = raise ERROR "root_thy: uncovered fun def."; (**) diff -r 976b99bcfc96 -r b2ff1902420f src/Tools/isac/Specify/Specify.thy --- a/src/Tools/isac/Specify/Specify.thy Wed Jan 11 06:06:12 2023 +0100 +++ b/src/Tools/isac/Specify/Specify.thy Wed Jan 11 09:23:18 2023 +0100 @@ -24,6 +24,7 @@ ML \ \ ML \ +ThyC.get_theory_PIDE \ ML \ \ ML \ \ diff -r 976b99bcfc96 -r b2ff1902420f src/Tools/isac/Specify/p-spec.sml --- a/src/Tools/isac/Specify/p-spec.sml Wed Jan 11 06:06:12 2023 +0100 +++ b/src/Tools/isac/Specify/p-spec.sml Wed Jan 11 09:23:18 2023 +0100 @@ -176,7 +176,7 @@ (*.input into empty PblObj, i.e. empty fmz+origin (unknown example).*) fun unknown_expl dI pbt selcts = let - val thy = ThyC.get_theory dI + val thy = Know_Store.get_via_last_thy dI val its_ = map (fstr2itm_ thy pbt) selcts (*([1],true,"#Given",Cor (...))*) val its = O_Model.add_enumerate its_ in map flattup2 its end diff -r 976b99bcfc96 -r b2ff1902420f test/Tools/isac/Test_Isac.thy --- a/test/Tools/isac/Test_Isac.thy Wed Jan 11 06:06:12 2023 +0100 +++ b/test/Tools/isac/Test_Isac.thy Wed Jan 11 09:23:18 2023 +0100 @@ -254,7 +254,7 @@ ML_file "Minisubpbl/600-postcond-NEXT_STEP.sml" ML_file "Minisubpbl/600-postcond.sml" ML_file "Minisubpbl/700-interSteps.sml" - ML_file "Minisubpbl/710-interSteps-short.sml" + ML_file "Minisubpbl/710-interSteps-short.sml" ML_file "Minisubpbl/790-complete-NEXT_STEP.sml" ML_file "Minisubpbl/790-complete.sml" ML_file "Minisubpbl/800-append-on-Frm.sml" diff -r 976b99bcfc96 -r b2ff1902420f test/Tools/isac/Test_Some.thy --- a/test/Tools/isac/Test_Some.thy Wed Jan 11 06:06:12 2023 +0100 +++ b/test/Tools/isac/Test_Some.thy Wed Jan 11 09:23:18 2023 +0100 @@ -120,7 +120,7 @@ \ ML \ \ -section \=============="Interpret/error-pattern.sml"========================================\ +section \===================================================================================\ ML \ \ ML \ \ ML \