1.1 --- a/TODO.md Wed Jul 20 12:16:36 2022 +0200
1.2 +++ b/TODO.md Sat Jul 23 20:05:25 2022 +0200
1.3 @@ -1,12 +1,15 @@
1.4 * MW: make Outer_Syntax.command \<^command_keyword>\<open>problem\<close> a model for ..\<open>Example\<close>
1.5 An ML syntax error should be indicated in place (in the string after \<^keyword>\<open>Given\<close> etc)
1.6 and not on the definition as a whole.
1.7 - This however is not the case despite there is no ISAC code involved.
1.8 - Reproducible e.g. at https://hg.risc.uni-linz.ac.at/wneuper/isa/file/9c2e1efe5cde/src/Tools/isac/Knowledge/Biegelinie.thy#l108
1.9 - The respective improvement would be the model for WN continuing ..\<open>Example\<close>.
1.10 + - in MathEngBasic/problem "Outer_Syntax.command \<^command_keyword>\<open>problem\<close>" there are writeln
1.11 + and comments with testdata from "problem pbl_bieg : "Biegelinien"" in Biegelinie.thy
1.12 + - in BridgeJEdit/Calculation.thy are remainings of time-consuming investigations
1.13 + - in MathEngBasic/problem there is guesswork ("TODO") how to reorganise "fun prep_input_PIDE"
1.14 + such that errors in "Given" etc are indicated WITHIN the term.
1.15
1.16 * ?MW?: In Outer_Syntax.command \<^command_keyword>\<open>Example\<close> is there a quick fix
1.17 for successfully replacing hacked Problem.parse_cas by parse_references_input?
1.18 + How get Token.src for testing purposes?
1.19 How can Scan.* be traced?
1.20 (Tracing should help understanding Problem.parse_cas, Problem.parse_model_input which involve Scan.*)
1.21
2.1 --- a/src/Tools/isac/BridgeJEdit/Calculation.thy Wed Jul 20 12:16:36 2022 +0200
2.2 +++ b/src/Tools/isac/BridgeJEdit/Calculation.thy Sat Jul 23 20:05:25 2022 +0200
2.3 @@ -156,6 +156,15 @@
2.4 (fn (example_id, (_(*probl_id'*), (model_input, _(*references_input*)))) =>
2.5 Toplevel.theory (fn thy =>
2.6 let
2.7 +
2.8 +val _ = writeln ("#Example model_input: " ^ @{make_string} model_input)
2.9 +(* #Example model_input:
2.10 + [("#Given", ["<markup>"]), ("#Where", ["<markup>"]), ("#Find", ["<markup>", "<markup>"]), ("#Relate", ["<markup>", "<markup>"])]*)
2.11 +val [("#Given", [m1]), ("#Where", [m2]), ("#Find", [m3, m4]), ("#Relate", [m5, m6])] =
2.12 + model_input : Problem.model_input
2.13 +val _ = writeln ("#Example m.: " ^ m1 ^ m2 ^ m3 ^ m4 ^ m4 ^ m5 ^ m6)
2.14 +(* #Example m.: Constants [r = 7]0 < rMaximum AAdditionalValues [u, v]AdditionalValues [u, v]Extremum A = 2 * u * v - u \<up> 2SideConditions [((u::real) / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]*)
2.15 +
2.16 val (thy_id, (probl_id, meth_id)) = (*references_input*)("Diff_App", ("univariate_calculus/Optimisation", "Optimisation/by_univariate_calculus"))
2.17 val input = update_state (example_id, (model_input,
2.18 (thy_id, References_Def.explode_id probl_id, References_Def.explode_id meth_id)))
2.19 @@ -180,7 +189,88 @@
2.20 ( *\----------------------------------------------------------------------------/*)
2.21 \<close> ML \<open>
2.22 \<close> ML \<open>
2.23 -\<close>
2.24 +\<close> text \<open>
2.25 + INVESTIGATE Problem.Outer_Syntax.command \ <^command_keyword>\<open>problem\<close>
2.26 + on Biegelinie.problem pbl_bieg : "Biegelinien"
2.27 +
2.28 + ML-source shows error-positions already perfectly: what types are involved?..
2.29 +\<close> ML \<open>
2.30 +Rule_Set.append_rules "empty" Rule_Set.empty [] (* ORIGINAL source = ARGUMENT IN fn *)
2.31 +(* (1a)
2.32 + Ouptut from Biegelinie.problem pbl_bieg : "Biegelinien":
2.33 + #problem source: Source {delimited = true, range = ({offset=38, end_offset=87, id=-1652}, {offset=87, id=-1652}),
2.34 + text = "\127Rule_Set.append_rules \"empty\" Rule_Set.empty []\127"}
2.35 +*)
2.36 +\<close> ML \<open>
2.37 +val source = Input.empty;
2.38 +val ml = ML_Lex.read;
2.39 +\<close> ML \<open>
2.40 + (ml "Theory.setup (Problem.set_data (" @ ML_Lex.read_source source @ ml "))")
2.41 +(*=
2.42 + [Text (Token (({}, {}), (Long_Ident, "Theory.setup"))), Text (Token (({}, {}), (Space, " "))), Text (Token (({}, {}), (Keyword, "("))), Text (Token (({}, {}), (Long_Ident, "Problem.set_data"))),
2.43 + Text (Token (({}, {}), (Space, " "))), Text (Token (({}, {}), (Keyword, "("))), Text (Token (({}, {}), (Space, " "))), Text (Token (({}, {}), (Keyword, ")"))), Text (Token (({}, {}), (Keyword, ")"))),
2.44 + Text (Token (({}, {}), (Space, " ")))]
2.45 + : ML_Lex.token Antiquote.antiquote list
2.46 + ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ type of (1a)
2.47 +*)
2.48 +\<close> ML \<open>
2.49 +ML_Context.expression (Input.pos_of source)
2.50 + (ml "Theory.setup (Problem.set_data (" @ ML_Lex.read_source source @ ml "))")
2.51 + : Context.generic -> Context.generic
2.52 +\<close> ML \<open>
2.53 +ML_Context.expression (Input.pos_of source)
2.54 + (ml "Theory.setup (Problem.set_data (" @ ML_Lex.read_source source @ ml "))")
2.55 + |> Context.theory_map
2.56 + : theory -> theory
2.57 +\<close> ML \<open>
2.58 +Outer_Syntax.command: Outer_Syntax.command_keyword -> string ->
2.59 + (Toplevel.transition -> Toplevel.transition) parser -> unit
2.60 +\<close> ML \<open>
2.61 +\<close> text \<open>
2.62 + ML-source shows error-positions already perfectly: types involved are above.
2.63 +
2.64 + Input at Given does NOT show error-position,
2.65 + but ISAC msg \<open>ME_Isa: thy "Isac_Knowledge" not in system\<close>
2.66 +
2.67 + Thus compare ML-source/input with model_input ...
2.68 +\<close> ML \<open>
2.69 +Problem.parse_model_input: Problem.model_input parser;
2.70 +Problem.parse_model_input: Token.src -> Problem.model_input * Token.src;
2.71 +Problem.parse_model_input: Token.T list -> Problem.model_input * (Token.T list)
2.72 +\<close> ML \<open>
2.73 +[]: Position.range list;
2.74 +[]: Position.T list;
2.75 +\<close> ML \<open>
2.76 +\<close> ML \<open>
2.77 +(* Given: "Traegerlaenge l_l" "Streckenlast q_q" *)
2.78 +(* (1b)
2.79 + Ouptut from Biegelinie.problem pbl_bieg : "Biegelinien":
2.80 + #problem model_input: [("#Given", ["<markup>", "<markup>"]), ("#Find", ["<markup>"]), ("#Relate", ["<markup>"])]
2.81 + : Problem.model_input
2.82 + type of (1b) --------^^^^^^^^^^^^^^^^^^^^^^> contains ? Markup.T ?..
2.83 +
2.84 + #problem m1: Traegerlaenge l_l
2.85 + #problem m2: Streckenlast q_q
2.86 + I this -----^^^______________^^^ Markup.T ?
2.87 +*)
2.88 +\<close> ML \<open> (** investigate parse_model_input **)
2.89 +\<close> ML \<open> (* how get a Token.T list without Outer_Syntax.command ? *)
2.90 +\<close> ML \<open>
2.91 +Parse.term: string parser;
2.92 +Parse.term: Token.T list -> string * Token.T list;
2.93 +\<close> ML \<open>
2.94 +\<close> ML \<open> (* relation Token.T -- Markup.T ??? *)
2.95 +\<close> ML \<open>
2.96 +val ctxt = Proof_Context.init_global @{theory};
2.97 +val given_1 = Syntax.read_term ctxt "Traegerlaenge l_l" (* as in parse_tagged_terms *)
2.98 +(* ^^^^^^^ : term -- why then evaluates parse_model_input to markup ? *)
2.99 +\<close> ML \<open>
2.100 +\<close> ML \<open>
2.101 +Markup.literal_fact "Traegerlaenge l_l" = ("literal_fact", [("name", "Traegerlaenge l_l")])
2.102 +\<close> ML \<open>
2.103 +\<close> ML \<open>
2.104 +\<close> ML \<open>
2.105 +\<close>
2.106
2.107
2.108 end
3.1 --- a/src/Tools/isac/BridgeJEdit/Calculation_OLD.thy Wed Jul 20 12:16:36 2022 +0200
3.2 +++ b/src/Tools/isac/BridgeJEdit/Calculation_OLD.thy Sat Jul 23 20:05:25 2022 +0200
3.3 @@ -75,9 +75,9 @@
3.4 \<close> text \<open>
3.5 datatype T = Token of (Symbol_Pos.text * Position.range) * (kind * string) * slot
3.6 \<close> ML \<open>
3.7 -Token.pos_of; (*^^^^^^^^^^^^^^^*)
3.8 -Token.range_of; (*^^^^^^^^^^^^^*)
3.9 -Token.unparse; (*^^^^^^^^^^^^^*)
3.10 +Token.pos_of; (*^^^^^^^^^^^^^^^*)
3.11 +Token.range_of; (*^^^^^^^^^^^^^*)
3.12 +Token.unparse; (*^^^^^^^^^^^^^*)
3.13 \<close> ML \<open>
3.14 fun string_of_tok (tok: Token.T) = "\n" ^ @{make_string} tok
3.15 \<close> ML \<open>
4.1 --- a/src/Tools/isac/MathEngBasic/problem.sml Wed Jul 20 12:16:36 2022 +0200
4.2 +++ b/src/Tools/isac/MathEngBasic/problem.sml Sat Jul 23 20:05:25 2022 +0200
4.3 @@ -16,8 +16,10 @@
4.4 type input
4.5 type model_input
4.6 val split_did: term -> term * term
4.7 + val split_did_PIDE: term -> term * term
4.8 (* TODO: ---------- remove always empty --- vvvvvvvvvvv -- vvv*)
4.9 val prep_input : theory -> Check_Unique.id -> string list -> id -> input -> T * id
4.10 + val prep_input_PIDE : theory -> Check_Unique.id -> string list -> id -> input -> T * id
4.11
4.12 val set_data: Rule_Def.rule_set -> theory -> theory
4.13 val the_data: theory -> Rule_Def.rule_set
4.14 @@ -75,6 +77,12 @@
4.15 (hd, [arg]) => (hd, arg)
4.16 | _ => raise ERROR ("split_did: doesn't match (hd,[arg]) for t = " ^ UnparseC.term t)
4.17 in (hd, arg) end
4.18 +fun split_did_PIDE t =
4.19 + let
4.20 + val (hd, arg) = case strip_comb t of
4.21 + (hd, [arg]) => (hd, arg)
4.22 + | _ => raise ERROR ("split_did_PIDE: doesn't match (hd,[arg]) for t = xxxxx" (*^ UnparseC.term t*))
4.23 + in (hd, arg) end
4.24
4.25 (* prepare problem-types before storing in pbltypes;
4.26 dont forget to "check_guh_unique" before ins *)
4.27 @@ -124,6 +132,58 @@
4.28 cas = Option.map (TermC.parseNEW'' thy) ca,
4.29 prls = ev, where_ = wh, ppc = gi @ fi @ re, met = metIDs}, pblID)
4.30 end;
4.31 +fun prep_input_PIDE thy guh maa init (pblID, dsc_dats, ev, ca, metIDs) =
4.32 + let
4.33 + fun eq f (f', _) = f = f';
4.34 +val _ = writeln "#prep_input_PIDE 1";
4.35 + val gi = filter (eq "#Given") dsc_dats;
4.36 +val _ = writeln "#prep_input_PIDE 1a";
4.37 + val gi = (case gi of
4.38 + [] => []
4.39 + | ((_, gi') :: []) =>
4.40 + (*(case \<^try>\<open> *)map (split_did_PIDE o (Syntax.read_term_global thy)) gi'(*\<close> of
4.41 + SOME x => x
4.42 + | NONE => raise ERROR ("prep_input_PIDE: syntax raise ERROR in '#Given' of " ^ strs2str pblID))*)
4.43 + | _ => raise ERROR ("prep_input_PIDE: more than one '#Given' in xxxxx" (*^ strs2str pblID*)));
4.44 +val _ = writeln "#prep_input_PIDE 1b";
4.45 + val gi = map (pair "#Given") gi;
4.46 +
4.47 +val _ = writeln "#prep_input_PIDE 2";
4.48 + val fi = filter (eq "#Find") dsc_dats;
4.49 + val fi = (case fi of
4.50 + [] => []
4.51 + | ((_, fi') :: []) =>
4.52 + (*(case \<^try>\<open> *)map (split_did_PIDE o (Syntax.read_term_global thy)) fi'(*\<close> of
4.53 + SOME x => x
4.54 + | NONE => raise ERROR ("prep_input_PIDE: syntax raise ERROR in '#Find' of " ^ strs2str pblID))*)
4.55 + | _ => raise ERROR ("prep_input_PIDE: more than one '#Find' in xxxxx" (*^ strs2str pblID*)));
4.56 + val fi = map (pair "#Find") fi;
4.57 +
4.58 +val _ = writeln "#prep_input_PIDE 3";
4.59 + val re = filter (eq "#Relate") dsc_dats;
4.60 + val re = (case re of
4.61 + [] => []
4.62 + | ((_, re') :: []) =>
4.63 + (*(case \<^try>\<open> *)map (split_did_PIDE o (Syntax.read_term_global thy)) re'(*\<close> of
4.64 + SOME x => x
4.65 + | NONE => raise ERROR ("prep_input_PIDE: syntax raise ERROR in '#Relate' of " ^ strs2str pblID))*)
4.66 + | _ => raise ERROR ("prep_input_PIDE: more than one '#Relate' in xxxxx" (*^ strs2str pblID*)));
4.67 + val re = map (pair "#Relate") re;
4.68 +
4.69 +val _ = writeln "#prep_input_PIDE 4";
4.70 + val wh = filter (eq "#Where") dsc_dats;
4.71 + val wh = (case wh of
4.72 + [] => []
4.73 + | ((_, wh') :: []) =>
4.74 + (*(case \<^try>\<open> *)map (TermC.parse_patt thy) wh'(*\<close> of
4.75 + SOME x => x
4.76 + | NONE => raise ERROR ("prep_input_PIDE: syntax raise ERROR in '#Where' of " ^ strs2str pblID))*)
4.77 + | _ => raise ERROR ("prep_input_PIDE: more than one '#Where' in xxxxx" (*^ strs2str pblID*)));
4.78 + in
4.79 + ({guh = guh, mathauthors = maa, init = init, thy = thy,
4.80 + cas = Option.map (Syntax.read_term_global thy) ca,
4.81 + prls = ev, where_ = wh, ppc = gi @ fi @ re, met = metIDs}, pblID)
4.82 + end;
4.83
4.84
4.85 (** Isar command **)
4.86 @@ -181,14 +241,34 @@
4.87 (fn (name, (id, ((((source, maa), mets), cas), model_input))) =>
4.88 Toplevel.theory (fn thy =>
4.89 let
4.90 +(*Ouptut from Biegelinie.problem pbl_bieg : "Biegelinien":*)
4.91 val pblID = References_Def.explode_id id;
4.92 val metIDs = map References_Def.explode_id mets;
4.93 +val _ = writeln ("#problem source: " ^ @{make_string} source)
4.94 val set_data =
4.95 ML_Context.expression (Input.pos_of source)
4.96 (ml "Theory.setup (Problem.set_data (" @ ML_Lex.read_source source @ ml "))")
4.97 |> Context.theory_map;
4.98 +val _ = writeln ("#problem set_data: " ^ @{make_string} set_data)
4.99 + (* Context.theory_map HAS STORED THE ml-source IN Theory_Data ALREADY,
4.100 + BUT prep_input_PIDE REQUIRES ml-source AGAIN ... *)
4.101 val input = the_data (set_data thy);
4.102 - val arg = prep_input thy name maa id_empty (pblID, model_input, input, cas, metIDs);
4.103 +val _ = writeln ("#problem input: " ^ @{make_string} input)
4.104 +
4.105 +val _ = writeln ("#problem model_input: " ^ @{make_string} model_input)
4.106 +val (m1, m2) = case model_input of
4.107 + ("#Given", [m1, m2]) :: _ => (m1, m2) (*=("<markup>", "<markup>")*)
4.108 +| _ => ("different case model_input", "different case model_input")
4.109 +val _ = writeln ("#problem m1: " ^ m1) (*= Traegerlaenge l_l*)
4.110 +val _ = writeln ("#problem m2: " ^ m2) (*= Streckenlast q_q *)
4.111 + (* TODO:
4.112 + * parse_model_input should preserve Position.T, Position.range, etc
4.113 + * ? preserve Position.T etc within ML_Lex.token Antiquote.antiquote list ?..
4.114 + ..in analogy to set_data ?!?
4.115 + * by Context.theory_map notify Isabelle/PIDE of errors from model_input at Position.T
4.116 + * in case there are no errors, do prep_input_PIDE (to be simplified)
4.117 + *)
4.118 + val arg = prep_input_PIDE thy name maa id_empty (pblID, model_input, input, cas, metIDs);
4.119 in KEStore_Elems.add_pbts [arg] thy end)))
4.120
4.121 in end;