1.1 --- a/src/Tools/isac/BaseDefinitions/Know_Store.thy Sun Nov 20 11:36:46 2022 +0100
1.2 +++ b/src/Tools/isac/BaseDefinitions/Know_Store.thy Wed Nov 23 11:14:38 2022 +0100
1.3 @@ -31,6 +31,7 @@
1.4 ML_file "rewrite-order.sml"
1.5 ML_file rule.sml
1.6 ML_file "references-def.sml"
1.7 +ML_file "cas-def.sml"
1.8 ML_file "model-pattern.sml"
1.9 ML_file "error-pattern-def.sml"
1.10 ML_file "rule-set.sml"
1.11 @@ -39,7 +40,6 @@
1.12 ML_file "check-unique.sml"
1.13 ML_file "problem-def.sml"
1.14 ML_file "method-def.sml"
1.15 -ML_file "cas-def.sml"
1.16 ML_file "formalise.sml"
1.17 ML_file "example.sml"
1.18 ML_file "thy-write.sml"
2.1 --- a/src/Tools/isac/BaseDefinitions/cas-def.sml Sun Nov 20 11:36:46 2022 +0100
2.2 +++ b/src/Tools/isac/BaseDefinitions/cas-def.sml Wed Nov 23 11:14:38 2022 +0100
2.3 @@ -7,6 +7,9 @@
2.4 *)
2.5 signature COMPUTER_ALGEBRA_SYSTEM__COMMAND_DEF =
2.6 sig
2.7 + type input
2.8 + val parse: Proof.context -> input -> term option
2.9 +
2.10 type generate_fn
2.11 type T
2.12 (*type cas_elem*)
2.13 @@ -21,6 +24,16 @@
2.14 struct
2.15 (**)
2.16
2.17 +type input = ((*TermC.as_*)string * Position.T) option;
2.18 +
2.19 +fun parse ctxt cas =
2.20 + (case cas of
2.21 + SOME (s, pos) =>
2.22 + SOME (Syntax.read_term ctxt s
2.23 + handle ERROR msg => error (msg ^ Position.here pos))
2.24 + | NONE => NONE)
2.25 +
2.26 +
2.27 (* association list with cas-commands, for generating a complete calc-head *)
2.28 type generate_fn =
2.29 (term list -> (* the arguments of the cas-command, eg. (x+1=2, x) *)
3.1 --- a/src/Tools/isac/BaseDefinitions/model-pattern.sml Sun Nov 20 11:36:46 2022 +0100
3.2 +++ b/src/Tools/isac/BaseDefinitions/model-pattern.sml Wed Nov 23 11:14:38 2022 +0100
3.3 @@ -12,13 +12,22 @@
3.4 type T
3.5 type single
3.6 val to_string: single list -> string
3.7 + type pre_model
3.8 + type model_input_pos
3.9 type m_field = string
3.10 type descriptor = term
3.11 - val split_descriptor: Proof.context -> term -> descriptor * term
3.12 + val split_descriptor: Proof.context -> term -> (descriptor * term)
3.13 +(**)
3.14 + val split_descriptor_PIDE: Proof.context -> m_field * term -> m_field * (descriptor * term)
3.15 + val split_model: Proof.context -> pre_model -> T
3.16 + val parse_separate: Proof.context -> m_field * (string * Position.T) -> m_field * term
3.17 + val parse: Proof.context -> model_input_pos -> pre_model * term list
3.18 +(**)
3.19 val parse_split_items: Proof.context -> References_Def.id -> m_field ->
3.20 (m_field * (*TermC.as_*)string list) list -> T
3.21 val parse_items: Proof.context -> References_Def.id ->
3.22 (m_field * (*TermC.as_*)string list) list -> single list * single list * single list * term list
3.23 +(**)
3.24
3.25 val variables: T -> term list
3.26 val get_field: descriptor -> T -> m_field option
3.27 @@ -45,8 +54,13 @@
3.28 (m_field * (* field Given, Find, Relate *)
3.29 (descriptor * (* for snd term *)
3.30 term)) (* id | arbitrary term *);
3.31 +(* does NOT contain pre-conditions, because these have no \<open>descriptor\<close> *)
3.32 type T = single list;
3.33
3.34 +type pre_model = (m_field * term) list
3.35 +type model_input_pos = (string * (string * Position.T) list) list
3.36 +
3.37 +(**)
3.38 fun split_descriptor ctxt dsc_tm =
3.39 let
3.40 val (hd, arg) = case strip_comb dsc_tm of
3.41 @@ -54,6 +68,15 @@
3.42 | _ => raise ERROR ("Model_Pattern.split_descriptor: doesn't match (hd,[arg]) for t = " ^
3.43 quote (UnparseC.term_in_ctxt ctxt dsc_tm))
3.44 in (hd, arg) end
3.45 +(**)
3.46 +fun split_descriptor_PIDE ctxt (m_field, dsc_tm) =
3.47 + let
3.48 + val (hd, arg) = case strip_comb dsc_tm of
3.49 + (hd, [arg]) => (m_field, (hd, arg))
3.50 + | _ => raise ERROR ("Model_Pattern.split_descriptor: doesn't match (hd,[arg]) for t = " ^
3.51 + quote (UnparseC.term_in_ctxt ctxt dsc_tm))
3.52 + in (hd, arg) end
3.53 +(**)
3.54 fun parse_split_items ctxt pbl_id m_field model_input =
3.55 let
3.56 val items = filter ((fn f => (fn (f', _) => f = f')) m_field) model_input
3.57 @@ -68,6 +91,9 @@
3.58 in
3.59 map (pair m_field) items'
3.60 end
3.61 +(**)
3.62 +fun split_model ctxt (gi_fi_re) = map (split_descriptor_PIDE ctxt) gi_fi_re
3.63 +(**)
3.64 fun parse_items ctxt pbl_id model_input =
3.65 let
3.66 val gi = parse_split_items ctxt pbl_id "#Given" model_input;
3.67 @@ -84,6 +110,20 @@
3.68 in
3.69 (gi, fi, re, wh)
3.70 end;
3.71 +(**)
3.72 +fun parse_separate ctxt (m_field, (str, _(*Position.T*))) =
3.73 + (m_field, (Syntax.read_term ctxt str))
3.74 +fun parse ctxt model_input =
3.75 + let
3.76 + val items = model_input |> map (fn (m_field, items) => map (pair m_field) items) |> flat;
3.77 + val model = items
3.78 + |> filter_out ((fn f => (fn (f', _) => f = f')) "#Where")
3.79 + |> map (parse_separate ctxt)
3.80 + val where_ = items
3.81 + |> filter_out ((fn f => (fn (f', _) => f = f')) "#Where")
3.82 + |> map (parse_separate ctxt)
3.83 + |> map snd
3.84 + in (model, where_) end
3.85
3.86 fun pat2str (field, (dsc, id)) = pair2str (field, pair2str (UnparseC.term dsc, UnparseC.term id));
3.87 fun to_string pats = (strs2str o (map pat2str)) pats;
4.1 --- a/src/Tools/isac/BridgeJEdit/Calculation.thy Sun Nov 20 11:36:46 2022 +0100
4.2 +++ b/src/Tools/isac/BridgeJEdit/Calculation.thy Wed Nov 23 11:14:38 2022 +0100
4.3 @@ -146,7 +146,7 @@
4.4 \<close> ML \<open>
4.5 (*
4.6 parse_references_input: references_input parser (*TODO: does not yet work,
4.7 - thus in Outer_Syntax.command \<^command_keyword>\<open>Example\<close> replacced by Problem.parse_cas*)
4.8 + thus in Outer_Syntax.command \<^command_keyword>\<open>Example\<close> replacced by Problem.parse_pos_cas*)
4.9 *)
4.10 \<close> ML \<open>
4.11 op -- : ('a -> 'b * 'c) * ('c -> 'd * 'e) -> 'a -> ('b * 'd) * 'e;
5.1 --- a/src/Tools/isac/Build_Isac.thy Sun Nov 20 11:36:46 2022 +0100
5.2 +++ b/src/Tools/isac/Build_Isac.thy Wed Nov 23 11:14:38 2022 +0100
5.3 @@ -59,13 +59,13 @@
5.4 "$ISABELLE_ISAC/ProgLang/ProgLang" "$ISABELLE_ISAC/Specify/Input_Descript"
5.5 at $ISABELLE_ISAC/MathEngBasic
5.6 ML_file thmC.sml
5.7 + ML_file "model-def.sml"
5.8 ML_file problem.sml
5.9 ML_file method.sml
5.10 ML_file "cas-command.sml"
5.11
5.12 ML_file rewrite.sml
5.13
5.14 - ML_file "model-def.sml"
5.15 ML_file "istate-def.sml"
5.16 ML_file "calc-tree-elem.sml"
5.17 ML_file "pre-conds-def.sml"
6.1 --- a/src/Tools/isac/Knowledge/Equation.thy Sun Nov 20 11:36:46 2022 +0100
6.2 +++ b/src/Tools/isac/Knowledge/Equation.thy Wed Nov 23 11:14:38 2022 +0100
6.3 @@ -55,8 +55,8 @@
6.4 Find: "solutions v_v'i'"
6.5
6.6 ML\<open>
6.7 -(*.function for handling the cas-input "solve (x+1=2, x)":
6.8 - make a model which is already in ctree-internal format.*)
6.9 +(* function for handling the cas-input "solve (x+1=2, x)":
6.10 + make a model which is already in ctree-internal formatarbitrary *)
6.11 fun argl2dtss [Const (\<^const_name>\<open>Pair\<close>, _) $ eq $ bdv] =
6.12 [((the o (TermC.parseNEW \<^context>)) "equality", [eq]),
6.13 ((the o (TermC.parseNEW \<^context>)) "solveFor", [bdv]),
7.1 --- a/src/Tools/isac/MathEngBasic/MathEngBasic.thy Sun Nov 20 11:36:46 2022 +0100
7.2 +++ b/src/Tools/isac/MathEngBasic/MathEngBasic.thy Wed Nov 23 11:14:38 2022 +0100
7.3 @@ -47,7 +47,201 @@
7.4
7.5 ML \<open>
7.6 \<close> ML \<open>
7.7 -Rewrite_Ord.function_empty
7.8 +\<close> ML \<open> (*=============== from model-pattern.sml ==============================================*)
7.9 +\<close> ML \<open>
7.10 +\<close> ML \<open> (*--------------- new model-pattern.sml -----------------------------------------------*)
7.11 +open Model_Pattern
7.12 +\<close> ML \<open>
7.13 +(fn (m_field, items) => map (pair m_field) items)
7.14 +: m_field * (((*TermC*)string * Position.T) list) -> (m_field * ((*TermC*)string * Position.T)) list
7.15 +\<close> ML \<open>
7.16 +\<close> ML \<open>
7.17 +fun parse_separate ctxt (m_field, (str, _(*Position.T*))) =
7.18 + (m_field, (Syntax.read_term ctxt str))
7.19 +\<close> ML \<open>
7.20 +parse_separate: Proof.context -> m_field * (string * Position.T) -> m_field * term
7.21 +\<close> text \<open>
7.22 +(*+*)val items = model_input |> map (fn (m_field, items) => map (pair m_field) items) |> flat
7.23 +\<close> text \<open>
7.24 +(*+*)val model = items
7.25 + |> filter_out ((fn f => (fn (f', _) => f = f')) "#Where")
7.26 + |> map (parse_separate ctxt)
7.27 +\<close> text \<open>
7.28 +(*+*)val where_ = items
7.29 + |> filter_out ((fn f => (fn (f', _) => f = f')) "#Where")
7.30 + |> map (parse_separate ctxt)
7.31 + |> map snd
7.32 +\<close> ML \<open>
7.33 +type pre_model = (m_field * term) list
7.34 +type model_input_pos = (string * (string * Position.T) list) list
7.35 +\<close> ML \<open>
7.36 +\<close> ML \<open>
7.37 +fun parse ctxt cas =
7.38 + (case cas of
7.39 + SOME (s, pos) =>
7.40 + SOME (Syntax.read_term ctxt s
7.41 + handle ERROR msg => error (msg ^ Position.here pos))
7.42 + | NONE => NONE)
7.43 +\<close> ML \<open>
7.44 +parse: Proof.context -> (string * Position.T) option -> term option
7.45 +\<close> ML \<open>
7.46 +fun parse ctxt model_input =
7.47 + let
7.48 + val items = model_input |> map (fn (m_field, items) => map (pair m_field) items) |> flat;
7.49 + val model = items
7.50 + |> filter_out ((fn f => (fn (f', _) => f = f')) "#Where")
7.51 + |> map (parse_separate ctxt)
7.52 + val where_ = items
7.53 + |> filter_out ((fn f => (fn (f', _) => f = f')) "#Where")
7.54 + |> map (parse_separate ctxt)
7.55 + |> map snd
7.56 + in (model, where_) end
7.57 +\<close> ML \<open>
7.58 +parse: Proof.context -> model_input_pos -> pre_model * term list;
7.59 +Model_Pattern.parse: Proof.context -> model_input_pos -> pre_model * term list;
7.60 +\<close> ML \<open>
7.61 +\<close> ML \<open> (* Model_Pattern.parse*, Probelm.parse* GET Input.source -- CANNOT BE HANDMADE*)
7.62 +(*+* )val (model, where_, cas) = Model_Pattern.parse @{context} model_input cas( *+*)
7.63 +\<close> ML \<open>
7.64 +\<close> ML \<open> (*------------------------- parse done -------------------------------------------------*)
7.65 +\<close> ML \<open>
7.66 +fun split_descriptor_PIDE ctxt (m_field, dsc_tm) =
7.67 + let
7.68 + val (hd, arg) = case strip_comb dsc_tm of
7.69 + (hd, [arg]) => (m_field, (hd, arg))
7.70 + | _ => raise ERROR ("Model_Pattern.split_descriptor: doesn't match (hd,[arg]) for t = " ^
7.71 + quote (UnparseC.term_in_ctxt ctxt dsc_tm))
7.72 + in (hd, arg) end
7.73 +\<close> ML \<open>
7.74 +split_descriptor_PIDE: Proof.context -> m_field * term -> m_field * (descriptor * term)
7.75 +\<close> ML \<open>
7.76 +\<close> ML \<open>
7.77 +fun split_model ctxt (gi_fi_re) = map (split_descriptor_PIDE ctxt) gi_fi_re
7.78 +\<close> ML \<open>
7.79 +split_model: Proof.context -> pre_model -> Model_Pattern.T
7.80 +\<close> ML \<open>
7.81 +\<close> ML \<open> (*=============== from problem.sml ====================================================*)
7.82 +open Problem
7.83 +\<close> ML \<open>
7.84 +type model_input =
7.85 + (Model_Pattern.m_field * (* "#Given", "#Find", "#Where", "#Relate" *)
7.86 + TermC.as_string list) (* list of items belonging to m_field *)
7.87 + list; (* list of "#Given" .. "#Relate" *)
7.88 +\<close> ML \<open>
7.89 +(* is the cut Parse.!!! still appropriate? better for each element? *)
7.90 +fun parse_item (keyword: string parser) (parse: 'a parser) =
7.91 + (keyword -- Args.colon) |-- Parse.!!! parse;
7.92 +\<close> ML \<open>
7.93 +\<close> ML \<open> (*--------------- new problem.sml -----------------------------------------------------*)
7.94 +\<close> ML \<open>
7.95 +type model_input_PIDE = (* for internal use *)
7.96 + (Model_Pattern.m_field * (* "#Given", "#Find", "#Where", "#Relate" *)
7.97 + (TermC.as_string * Position.T) list) (* list of items belonging to m_field *)
7.98 + list; (* list of "#Given" .. "#Relate" *)
7.99 +\<close> ML \<open>
7.100 +fun parse_tagged_terms keyword (tag: string) =
7.101 + Scan.optional (* vvvvvvvvvvv*)
7.102 + (parse_item keyword (Scan.repeat Parse.term) >>
7.103 + (fn ts => [(tag, ts)])) [];
7.104 +(**)
7.105 +fun parse_tagged_terms_PIDE keyword (tag: string) =
7.106 + Scan.optional (* vvvvvvvvvvvvvvvvvvvvvvvvvvv*)
7.107 + (parse_item keyword (Scan.repeat (Parse.position Parse.term)) >>
7.108 + (fn ts => [(tag, ts)])) [];
7.109 +\<close> ML \<open>
7.110 +parse_tagged_terms_PIDE: string parser -> string -> model_input_PIDE parser
7.111 +\<close> ML \<open>
7.112 +val parse_model_input : model_input parser =
7.113 + parse_tagged_terms \<^keyword>\<open>Given\<close> "#Given" @@@
7.114 + parse_tagged_terms \<^keyword>\<open>Where\<close> "#Where" @@@
7.115 + parse_tagged_terms \<^keyword>\<open>Find\<close> "#Find" @@@
7.116 + parse_tagged_terms \<^keyword>\<open>Relate\<close> "#Relate";
7.117 +(**)
7.118 +val parse_pos_model_input : model_input_PIDE parser =
7.119 + parse_tagged_terms_PIDE \<^keyword>\<open>Given\<close> "#Given" @@@
7.120 + parse_tagged_terms_PIDE \<^keyword>\<open>Where\<close> "#Where" @@@
7.121 + parse_tagged_terms_PIDE \<^keyword>\<open>Find\<close> "#Find" @@@
7.122 + parse_tagged_terms_PIDE \<^keyword>\<open>Relate\<close> "#Relate";
7.123 +\<close> ML \<open>
7.124 +parse_model_input: model_input parser;
7.125 +parse_pos_model_input: model_input_PIDE parser;
7.126 +\<close> ML \<open>
7.127 +\<close> ML \<open> (* after parse_* we have (string * Position.T)
7.128 +@{print} model_input on problem pbl_equ_univ_lin:
7.129 +
7.130 +[("#Given", ["<markup>", "<markup>"]),
7.131 +("#Where", ["<markup>", "<markup>", "<markup>", "<markup>", "<markup>"]),
7.132 +("#Find", ["<markup>"])]
7.133 +(line 189 of "/home/walthern/repos/isa/src/Tools/isac/MathEngBasic/problem.sml")
7.134 +"-----------------------------------------------------------------------------"
7.135 +SOME ("<markup>", {offset=124, end_offset=148, id=-1127})
7.136 + -----------------^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Position.T ONLY IN CAS
7.137 +(line 191 of "/home/walthern/repos/isa/src/Tools/isac/MathEngBasic/problem.sml")
7.138 +*)
7.139 +val ctxt = @{context};
7.140 +val pbl_id = ["univariate", "equation"];
7.141 +val m_field = "#Given";
7.142 +val model_input = [
7.143 + ("#Given", [("equality e_e", Position.none), ("solveFor v_v", Position.none)]),
7.144 + ("#Where", [("matches (?a = ?b) e_e", Position.none)]),
7.145 + ("#Find", [("solutions v_v'i'", Position.none)]),
7.146 + ("#Relate", [])];
7.147 +val cas = SOME ("solve (e_e::bool, v_v)", Position.none)
7.148 +\<close> ML \<open>
7.149 +\<close> ML \<open> (*method...*)
7.150 +open MethodC
7.151 +\<close> ML \<open>
7.152 +fun prep_store thy guh mathauthors start_refine (met_id, model, where_,
7.153 + {rew_ord = ro, rls' = rls, prog_rls = prog_rls, where_rls = where_rls, calc = _(*scr_isa_fns*),
7.154 + errpats = ep, rew_rls = nr}, prog) =
7.155 + let
7.156 + val ctxt = Proof_Context.init_global thy
7.157 +
7.158 + val model' = Model_Pattern.split_model ctxt model
7.159 +(** )val (gi, fi, re, wh) = Model_Pattern.parse_items ctxt met_id model_input( **)
7.160 +
7.161 + val sc = Program.prep_program prog
7.162 + val calc = if Thm.eq_thm (prog, @{thm refl}) then [] else Auto_Prog.get_calcs thy sc
7.163 + in
7.164 + ({guh = guh, mathauthors = mathauthors, start_refine = start_refine, model = model',
7.165 + where_ = where_, rew_ord = ro, asm_rls = rls, prog_rls = prog_rls, where_rls = where_rls,
7.166 + calc = calc, errpats = ep, rew_rls = nr, program = Rule.Prog sc}: T, met_id)
7.167 + end;
7.168 +\<close> ML \<open>
7.169 +prep_store: theory -> Check_Unique.id -> string list -> References_Def.id ->
7.170 + id * pre_model * term list *
7.171 +{calc: 'b, errpats: Error_Pattern_Def.T list, prog_rls: Rule_Def.rule_set, rew_ord: string,
7.172 +rew_rls: Rule_Def.rule_set, rls': Rule_Def.rule_set, where_rls: Rule_Def.rule_set} * thm
7.173 + -> T * id
7.174 +\<close> ML \<open>
7.175 +\<close> ML \<open>
7.176 +\<close> ML \<open>
7.177 +\<close> ML \<open> (*problem...*)
7.178 +\<close> text \<open>
7.179 +fun prep_store thy name maa start_refine (model, where_, cas) (pbl_id, met_ids, where_rls) =
7.180 + let
7.181 + val model' = Model_Pattern.split_model (Proof_Context.init_global thy) model
7.182 + in
7.183 + ({guh = name, mathauthors = maa, start_refine = start_refine, thy = thy, cas = cas,
7.184 + where_rls = where_rls, where_ = where_, model = model', solve_mets = met_ids}, pbl_id)
7.185 + end;
7.186 +
7.187 + prep_store : theory -> Check_Unique.id -> string list -> References_Def.id ->
7.188 + pre_model * term list * term option -> id * References_Def.id list * Rule_Set.T -> T * id;
7.189 +Problem.prep_store: theory -> Check_Unique.id -> string list -> References_Def.id ->
7.190 + pre_model * term list * term option -> id * References_Def.id list * Rule_Set.T -> T * id;
7.191 +\<close> ML \<open>
7.192 +val thy = @{theory}
7.193 +val name = "pbl_equ_univ"
7.194 +val maa = ["math author"]
7.195 +val met_ids = [["LinEq", "solve_lineq_equation"]]
7.196 +val where_rls = Rule_Set.empty
7.197 +\<close> ML \<open>
7.198 +(*+* )
7.199 +Problem.prep_store @{theory} name maa id_empty
7.200 + (model, where_, cas) (pbl_id, met_ids, where_rls)
7.201 +( *+*)
7.202 +\<close> ML \<open>
7.203 \<close> ML \<open>
7.204 \<close>
7.205 -end
7.206 +end
7.207 \ No newline at end of file
8.1 --- a/src/Tools/isac/MathEngBasic/method.sml Sun Nov 20 11:36:46 2022 +0100
8.2 +++ b/src/Tools/isac/MathEngBasic/method.sml Wed Nov 23 11:14:38 2022 +0100
8.3 @@ -18,6 +18,7 @@
8.4 val id_empty: id
8.5 val id_to_string: id -> string
8.6
8.7 +(**)
8.8 type input
8.9 val prep_input: theory -> Check_Unique.id -> string list -> id ->
8.10 id * Problem.model_input * input * thm -> T * id
8.11 @@ -46,7 +47,7 @@
8.12
8.13 (* a subset of MethodC.T record's fields *)
8.14 type input =
8.15 - {calc: Rule_Def.eval_ml_from_prog list, (*crls: Rule_Set.T,*) errpats: Error_Pattern_Def.T list, rew_rls: Rule_Set.T,
8.16 + {calc: Rule_Def.eval_ml_from_prog list, errpats: Error_Pattern_Def.T list, rew_rls: Rule_Set.T,
8.17 where_rls: Rule_Set.T, rew_ord: Rewrite_Ord.id, rls': Rule_Set.T, prog_rls: Rule_Set.T}
8.18
8.19 fun prep_input thy guh mathauthors start_refine (met_id, model_input,
8.20 @@ -88,21 +89,24 @@
8.21 "prepare ISAC method and register it to Knowledge Store"
8.22 (Parse.name -- Parse.!!! (\<^keyword>\<open>:\<close> |-- Parse.name --
8.23 Parse.!!! (\<^keyword>\<open>=\<close> |-- Parse.ML_source -- Problem.parse_authors --
8.24 - parse_program -- Problem.parse_model_input)) >>
8.25 + parse_program -- (**)Problem.parse_model_input(** )Problem.parse_pos_model_input( **) )) >>
8.26 (fn (name, (id, (((source, maa), program), model_input))) => Toplevel.theory (fn thy =>
8.27 let
8.28 + val ctxt = Proof_Context.init_global thy
8.29 val metID = References_Def.explode_id id;
8.30 + (** )val (model, where_) = Model_Pattern.parse @{context} model_input( **)
8.31 val set_data =
8.32 ML_Context.expression (Input.pos_of source)
8.33 (ml "Theory.setup (MethodC.set_data (" @ ML_Lex.read_source source @ ml "))")
8.34 |> Context.theory_map;
8.35 - val input = the_data (set_data thy);
8.36 + val ml_input = the_data (set_data thy);
8.37 val thm =
8.38 (case program of
8.39 NONE => @{thm refl}
8.40 | SOME a => Global_Theory.get_thm thy (Global_Theory.check_fact thy a));
8.41 - val arg = prep_input thy name maa id_empty (metID, model_input, input, thm);
8.42 - in Know_Store.add_mets @{context} [arg] thy end)))
8.43 + (** )val arg = prep_store thy name maa id_empty (metID, model, where_, ml_input, thm);( **)
8.44 + (**)val arg = prep_input thy name maa id_empty (metID, model_input, ml_input, thm);(**)
8.45 + in Know_Store.add_mets ctxt [arg] thy end)))
8.46
8.47 in end;
8.48
9.1 --- a/src/Tools/isac/MathEngBasic/problem.sml Sun Nov 20 11:36:46 2022 +0100
9.2 +++ b/src/Tools/isac/MathEngBasic/problem.sml Wed Nov 23 11:14:38 2022 +0100
9.3 @@ -21,8 +21,10 @@
9.4
9.5 type input
9.6 type model_input
9.7 - val prep_input: theory -> Check_Unique.id -> string list -> id -> input -> T * id
9.8 -
9.9 + type model_input_PIDE
9.10 + val prep_store: theory -> Check_Unique.id -> string list -> References_Def.id ->
9.11 + Model_Pattern.pre_model * term list * term option -> id * References_Def.id list * Rule_Set.T ->
9.12 + T * id
9.13 val set_data: Rule_Def.rule_set -> theory -> theory
9.14 val the_data: theory -> Rule_Def.rule_set
9.15
9.16 @@ -30,13 +32,12 @@
9.17 val parse_item_name: string parser -> string -> string parser
9.18 val parse_item_names: string parser -> string list parser
9.19 val parse_model_input: model_input parser
9.20 + val parse_pos_model_input: model_input_PIDE parser
9.21 val parse_authors: string list parser
9.22 - val parse_cas: Token.T list -> (string * Position.T) option * Token.T list
9.23 + val parse_pos_cas: (string * Position.T) option parser
9.24 val parse_methods: string list parser
9.25 val ml: string -> ML_Lex.token Antiquote.antiquote list
9.26
9.27 -(*val adapt_to_type: Proof.context -> T -> T*)
9.28 -(** )val from_store: id -> T( **)
9.29 val from_store: Proof.context -> id -> T
9.30 end
9.31
9.32 @@ -63,34 +64,30 @@
9.33
9.34 (** prepare Problem for Store **)
9.35
9.36 +(**)
9.37 type model_input =
9.38 (Model_Pattern.m_field * (* "#Given", "#Find", "#Where", "#Relate" *)
9.39 TermC.as_string list) (* list of items belonging to m_field *)
9.40 list; (* list of "#Given" .. "#Relate" *)
9.41 +(**)
9.42 +type model_input_PIDE = (* for internal use *)
9.43 + (Model_Pattern.m_field * (* "#Given", "#Find", "#Where", "#Relate" *)
9.44 + (TermC.as_string * Position.T) list) (* list of items belonging to m_field *)
9.45 + list; (* list of "#Given" .. "#Relate" *)
9.46 +(**)
9.47 type input =
9.48 - id * (* the key into the problem hierarchy *)
9.49 - model_input * (* e.g. ("#Given", ["unsorted u_u"]) list *)
9.50 - Rule_Set.T * (* for evaluating "#Where" *)
9.51 - (TermC.as_string * Position.T) option * (* CAS_Cmd *)
9.52 - Meth_Def.id list; (* methods that can solve the problem *)
9.53 -
9.54 -(* prepare problem-types before storing in pbltypes;
9.55 - dont forget to "check_guh_unique" before inserting *)
9.56 -(*??? Syntax.read_term_global below ------+-------vvvvvvvvvvv Parse.term in parse_tagged_terms ???*)
9.57 -fun prep_input thy name maa start_refine (pbl_id, model_input, where_rls, cas, met_ids) =
9.58 + id * (* the key into the problem hierarchy *)
9.59 + model_input * (* e.g. ("#Given", [("unsorted u_u", Position.T)]) list *)
9.60 + Rule_Set.T * (* for evaluating "#Where" *)
9.61 + CAS_Def.input * (* CAS_Cmd *)
9.62 + Meth_Def.id list; (* methods that can solve the problem *)
9.63 +fun prep_store thy name maa start_refine (model, where_, cas) (pbl_id, met_ids, where_rls) =
9.64 let
9.65 - val ctxt = Proof_Context.init_global thy
9.66 - val (gi, fi, re, wh) = Model_Pattern.parse_items ctxt pbl_id model_input
9.67 + val model' = Model_Pattern.split_model (Proof_Context.init_global thy) model
9.68 in
9.69 - ({guh = name, mathauthors = maa, start_refine = start_refine, thy = thy,
9.70 - cas =
9.71 - (case cas of
9.72 - SOME (s, pos) =>
9.73 - SOME (Syntax.read_term_global thy s
9.74 - handle ERROR msg => error (msg ^ Position.here pos))
9.75 - | NONE => NONE),
9.76 - where_rls = where_rls, where_ = wh, model = gi @ fi @ re, solve_mets = met_ids}, pbl_id)
9.77 - end;
9.78 + ({guh = name, mathauthors = maa, start_refine = start_refine, thy = thy, cas = cas,
9.79 + where_rls = where_rls, where_ = where_, model = model', solve_mets = met_ids}, pbl_id)
9.80 + end
9.81
9.82
9.83 (** Isar command **)
9.84 @@ -120,17 +117,30 @@
9.85 fun parse_item_names (keyword: string parser) =
9.86 Scan.optional (parse_item keyword (Scan.repeat1 Parse.name)) [];
9.87
9.88 +(**)
9.89 fun parse_tagged_terms keyword (tag: string) =
9.90 Scan.optional (parse_item keyword (Scan.repeat Parse.term) >> (fn ts => [(tag, ts)])) [];
9.91 +(**)
9.92 +fun parse_tagged_terms_PIDE keyword (tag: string) =
9.93 + Scan.optional
9.94 + (parse_item keyword (Scan.repeat (Parse.position Parse.term)) >>
9.95 + (fn ts => [(tag, ts)])) [];
9.96 +(**)
9.97
9.98 val parse_model_input : model_input parser =
9.99 parse_tagged_terms \<^keyword>\<open>Given\<close> "#Given" @@@
9.100 parse_tagged_terms \<^keyword>\<open>Where\<close> "#Where" @@@
9.101 parse_tagged_terms \<^keyword>\<open>Find\<close> "#Find" @@@
9.102 parse_tagged_terms \<^keyword>\<open>Relate\<close> "#Relate";
9.103 +(**)
9.104 +val parse_pos_model_input : model_input_PIDE parser =
9.105 + parse_tagged_terms_PIDE \<^keyword>\<open>Given\<close> "#Given" @@@
9.106 + parse_tagged_terms_PIDE \<^keyword>\<open>Where\<close> "#Where" @@@
9.107 + parse_tagged_terms_PIDE \<^keyword>\<open>Find\<close> "#Find" @@@
9.108 + parse_tagged_terms_PIDE \<^keyword>\<open>Relate\<close> "#Relate";
9.109
9.110 val parse_authors = parse_item_names \<^keyword>\<open>Author\<close>;
9.111 -val parse_cas = Scan.option (parse_item \<^keyword>\<open>CAS\<close> (Parse.position Parse.term));
9.112 +val parse_pos_cas = Scan.option (parse_item \<^keyword>\<open>CAS\<close> (Parse.position Parse.term));
9.113 val parse_methods = parse_item_names \<^keyword>\<open>Method_Ref\<close>;
9.114 val ml = ML_Lex.read;
9.115
9.116 @@ -144,18 +154,23 @@
9.117 "prepare ISAC problem type and register it to Knowledge Store"
9.118 (Parse.name -- Parse.!!! (\<^keyword>\<open>:\<close> |-- Parse.name --
9.119 Parse.!!! (\<^keyword>\<open>=\<close> |-- Parse.ML_source -- parse_authors --
9.120 - parse_methods -- parse_cas -- parse_model_input)) >>
9.121 + parse_methods -- parse_pos_cas -- (** )parse_model_input( **)parse_pos_model_input(**) )) >>
9.122 (fn (name, (id, ((((source, maa), mets), cas), model_input))) =>
9.123 Toplevel.theory (fn thy =>
9.124 let
9.125 - val pblID = References_Def.explode_id id;
9.126 - val metIDs = map References_Def.explode_id mets;
9.127 + val pbl_id = References_Def.explode_id id;
9.128 + val met_ids = map References_Def.explode_id mets;
9.129 + (**)val (model, where_) = Model_Pattern.parse @{context} model_input(**)
9.130 + val cas = CAS_Def.parse @{context} cas
9.131 val set_data =
9.132 ML_Context.expression (Input.pos_of source)
9.133 (ml "Theory.setup (Problem.set_data (" @ ML_Lex.read_source source @ ml "))")
9.134 |> Context.theory_map;
9.135 val where_rls = the_data (set_data thy);
9.136 - val arg = prep_input thy name maa id_empty (pblID, model_input, where_rls, cas, metIDs);
9.137 + (**)val arg = prep_store @{theory} name maa id_empty
9.138 + (model, where_, cas) (pbl_id, met_ids, where_rls)(**)
9.139 + (** )val arg = prep_input thy name maa id_empty
9.140 + (pbl_id, model_input, where_rls, cas, met_ids);( **)
9.141 in Know_Store.add_pbls @{context} [arg] thy end)))
9.142
9.143 in end;
10.1 --- a/src/Tools/isac/Specify/cas-command.sml Sun Nov 20 11:36:46 2022 +0100
10.2 +++ b/src/Tools/isac/Specify/cas-command.sml Wed Nov 23 11:14:38 2022 +0100
10.3 @@ -5,6 +5,7 @@
10.4
10.5 signature COMPUTER_ALGEBRA_SYSTEM_COMMAND =
10.6 sig
10.7 + type pos_input
10.8 type T = CAS_Def.T
10.9 val input : term -> (Ctree.ctree * SpecificationC.T) option
10.10 val is_from: TermC.as_string -> Formalise.T -> bool
10.11 @@ -23,6 +24,7 @@
10.12 struct
10.13 (**)
10.14
10.15 +type pos_input = (TermC.as_string * Position.T) option;
10.16 type T = CAS_Def.T; (*(term * (References_Def.T * generate_fn))*)
10.17
10.18 fun dtss2itm_ model (d, ts) =