1.1 --- a/src/Tools/isac/MathEngBasic/problem.sml Wed Jul 20 12:16:36 2022 +0200
1.2 +++ b/src/Tools/isac/MathEngBasic/problem.sml Sat Jul 23 20:05:25 2022 +0200
1.3 @@ -16,8 +16,10 @@
1.4 type input
1.5 type model_input
1.6 val split_did: term -> term * term
1.7 + val split_did_PIDE: term -> term * term
1.8 (* TODO: ---------- remove always empty --- vvvvvvvvvvv -- vvv*)
1.9 val prep_input : theory -> Check_Unique.id -> string list -> id -> input -> T * id
1.10 + val prep_input_PIDE : theory -> Check_Unique.id -> string list -> id -> input -> T * id
1.11
1.12 val set_data: Rule_Def.rule_set -> theory -> theory
1.13 val the_data: theory -> Rule_Def.rule_set
1.14 @@ -75,6 +77,12 @@
1.15 (hd, [arg]) => (hd, arg)
1.16 | _ => raise ERROR ("split_did: doesn't match (hd,[arg]) for t = " ^ UnparseC.term t)
1.17 in (hd, arg) end
1.18 +fun split_did_PIDE t =
1.19 + let
1.20 + val (hd, arg) = case strip_comb t of
1.21 + (hd, [arg]) => (hd, arg)
1.22 + | _ => raise ERROR ("split_did_PIDE: doesn't match (hd,[arg]) for t = xxxxx" (*^ UnparseC.term t*))
1.23 + in (hd, arg) end
1.24
1.25 (* prepare problem-types before storing in pbltypes;
1.26 dont forget to "check_guh_unique" before ins *)
1.27 @@ -124,6 +132,58 @@
1.28 cas = Option.map (TermC.parseNEW'' thy) ca,
1.29 prls = ev, where_ = wh, ppc = gi @ fi @ re, met = metIDs}, pblID)
1.30 end;
1.31 +fun prep_input_PIDE thy guh maa init (pblID, dsc_dats, ev, ca, metIDs) =
1.32 + let
1.33 + fun eq f (f', _) = f = f';
1.34 +val _ = writeln "#prep_input_PIDE 1";
1.35 + val gi = filter (eq "#Given") dsc_dats;
1.36 +val _ = writeln "#prep_input_PIDE 1a";
1.37 + val gi = (case gi of
1.38 + [] => []
1.39 + | ((_, gi') :: []) =>
1.40 + (*(case \<^try>\<open> *)map (split_did_PIDE o (Syntax.read_term_global thy)) gi'(*\<close> of
1.41 + SOME x => x
1.42 + | NONE => raise ERROR ("prep_input_PIDE: syntax raise ERROR in '#Given' of " ^ strs2str pblID))*)
1.43 + | _ => raise ERROR ("prep_input_PIDE: more than one '#Given' in xxxxx" (*^ strs2str pblID*)));
1.44 +val _ = writeln "#prep_input_PIDE 1b";
1.45 + val gi = map (pair "#Given") gi;
1.46 +
1.47 +val _ = writeln "#prep_input_PIDE 2";
1.48 + val fi = filter (eq "#Find") dsc_dats;
1.49 + val fi = (case fi of
1.50 + [] => []
1.51 + | ((_, fi') :: []) =>
1.52 + (*(case \<^try>\<open> *)map (split_did_PIDE o (Syntax.read_term_global thy)) fi'(*\<close> of
1.53 + SOME x => x
1.54 + | NONE => raise ERROR ("prep_input_PIDE: syntax raise ERROR in '#Find' of " ^ strs2str pblID))*)
1.55 + | _ => raise ERROR ("prep_input_PIDE: more than one '#Find' in xxxxx" (*^ strs2str pblID*)));
1.56 + val fi = map (pair "#Find") fi;
1.57 +
1.58 +val _ = writeln "#prep_input_PIDE 3";
1.59 + val re = filter (eq "#Relate") dsc_dats;
1.60 + val re = (case re of
1.61 + [] => []
1.62 + | ((_, re') :: []) =>
1.63 + (*(case \<^try>\<open> *)map (split_did_PIDE o (Syntax.read_term_global thy)) re'(*\<close> of
1.64 + SOME x => x
1.65 + | NONE => raise ERROR ("prep_input_PIDE: syntax raise ERROR in '#Relate' of " ^ strs2str pblID))*)
1.66 + | _ => raise ERROR ("prep_input_PIDE: more than one '#Relate' in xxxxx" (*^ strs2str pblID*)));
1.67 + val re = map (pair "#Relate") re;
1.68 +
1.69 +val _ = writeln "#prep_input_PIDE 4";
1.70 + val wh = filter (eq "#Where") dsc_dats;
1.71 + val wh = (case wh of
1.72 + [] => []
1.73 + | ((_, wh') :: []) =>
1.74 + (*(case \<^try>\<open> *)map (TermC.parse_patt thy) wh'(*\<close> of
1.75 + SOME x => x
1.76 + | NONE => raise ERROR ("prep_input_PIDE: syntax raise ERROR in '#Where' of " ^ strs2str pblID))*)
1.77 + | _ => raise ERROR ("prep_input_PIDE: more than one '#Where' in xxxxx" (*^ strs2str pblID*)));
1.78 + in
1.79 + ({guh = guh, mathauthors = maa, init = init, thy = thy,
1.80 + cas = Option.map (Syntax.read_term_global thy) ca,
1.81 + prls = ev, where_ = wh, ppc = gi @ fi @ re, met = metIDs}, pblID)
1.82 + end;
1.83
1.84
1.85 (** Isar command **)
1.86 @@ -181,14 +241,34 @@
1.87 (fn (name, (id, ((((source, maa), mets), cas), model_input))) =>
1.88 Toplevel.theory (fn thy =>
1.89 let
1.90 +(*Ouptut from Biegelinie.problem pbl_bieg : "Biegelinien":*)
1.91 val pblID = References_Def.explode_id id;
1.92 val metIDs = map References_Def.explode_id mets;
1.93 +val _ = writeln ("#problem source: " ^ @{make_string} source)
1.94 val set_data =
1.95 ML_Context.expression (Input.pos_of source)
1.96 (ml "Theory.setup (Problem.set_data (" @ ML_Lex.read_source source @ ml "))")
1.97 |> Context.theory_map;
1.98 +val _ = writeln ("#problem set_data: " ^ @{make_string} set_data)
1.99 + (* Context.theory_map HAS STORED THE ml-source IN Theory_Data ALREADY,
1.100 + BUT prep_input_PIDE REQUIRES ml-source AGAIN ... *)
1.101 val input = the_data (set_data thy);
1.102 - val arg = prep_input thy name maa id_empty (pblID, model_input, input, cas, metIDs);
1.103 +val _ = writeln ("#problem input: " ^ @{make_string} input)
1.104 +
1.105 +val _ = writeln ("#problem model_input: " ^ @{make_string} model_input)
1.106 +val (m1, m2) = case model_input of
1.107 + ("#Given", [m1, m2]) :: _ => (m1, m2) (*=("<markup>", "<markup>")*)
1.108 +| _ => ("different case model_input", "different case model_input")
1.109 +val _ = writeln ("#problem m1: " ^ m1) (*= Traegerlaenge l_l*)
1.110 +val _ = writeln ("#problem m2: " ^ m2) (*= Streckenlast q_q *)
1.111 + (* TODO:
1.112 + * parse_model_input should preserve Position.T, Position.range, etc
1.113 + * ? preserve Position.T etc within ML_Lex.token Antiquote.antiquote list ?..
1.114 + ..in analogy to set_data ?!?
1.115 + * by Context.theory_map notify Isabelle/PIDE of errors from model_input at Position.T
1.116 + * in case there are no errors, do prep_input_PIDE (to be simplified)
1.117 + *)
1.118 + val arg = prep_input_PIDE thy name maa id_empty (pblID, model_input, input, cas, metIDs);
1.119 in KEStore_Elems.add_pbts [arg] thy end)))
1.120
1.121 in end;