Walther@60778
|
1 |
(* Title: Interpret/cas-command.sml
|
walther@59894
|
2 |
Author: Walther Neuper 2019
|
walther@59894
|
3 |
*)
|
walther@59894
|
4 |
|
walther@59894
|
5 |
signature COMPUTER_ALGEBRA_SYSTEM_COMMAND =
|
walther@59894
|
6 |
sig
|
Walther@60603
|
7 |
type input_pos
|
walther@59982
|
8 |
type T = CAS_Def.T
|
walther@60097
|
9 |
val input : term -> (Ctree.ctree * SpecificationC.T) option
|
walther@59982
|
10 |
val is_from: TermC.as_string -> Formalise.T -> bool
|
Walther@60772
|
11 |
|
Walther@60772
|
12 |
(*/----- from isac_test for Minisubpbl*)
|
walther@59982
|
13 |
val input_: References.T -> (term * term list) list ->
|
Walther@60782
|
14 |
Problem.id * I_Model.T * MethodC.id * I_Model.T * Pre_Conds.T * Proof.context
|
walther@59982
|
15 |
val dtss2itm_: Model_Pattern.T -> term * term list ->
|
Walther@60782
|
16 |
int list * bool * Model_Def.m_field * (I_Model.feedback * Position.T)
|
walther@59982
|
17 |
val flattup2: 'a * ('b * 'c * 'd * 'e) -> 'a * 'b * 'c * 'd * 'e
|
Walther@60772
|
18 |
(*\----- from isac_test for Minisubpbl*)
|
Walther@60772
|
19 |
|
Walther@60772
|
20 |
\<^isac_test>\<open>
|
Walther@60772
|
21 |
(*put "from isac_test for Minisubpbl" here*)
|
wenzelm@60223
|
22 |
\<close>
|
walther@59894
|
23 |
end
|
walther@59894
|
24 |
|
walther@59894
|
25 |
(**)
|
walther@59894
|
26 |
structure CAS_Cmd(**): COMPUTER_ALGEBRA_SYSTEM_COMMAND(**) =
|
walther@59894
|
27 |
struct
|
walther@59894
|
28 |
(**)
|
walther@59894
|
29 |
|
Walther@60603
|
30 |
type input_pos = CAS_Def.input_pos;
|
Walther@60547
|
31 |
type T = CAS_Def.T; (*(term * (References_Def.T * generate_fn))*)
|
walther@59896
|
32 |
|
Walther@60586
|
33 |
fun dtss2itm_ model (d, ts) =
|
walther@59982
|
34 |
let
|
walther@59982
|
35 |
val (f, (d, id)) = the (find_first ((curry op= d) o
|
walther@59982
|
36 |
(#1: (term * term) -> term) o
|
Walther@60586
|
37 |
(#2: Model_Pattern.single -> (term * term))) model)
|
walther@59982
|
38 |
in
|
Walther@60782
|
39 |
([1], true, f, (I_Model.Cor (d, ts), Position.none))
|
walther@59982
|
40 |
end
|
walther@59982
|
41 |
|
walther@59982
|
42 |
fun flattup2 (a, (b ,c, d, e)) = (a, b, c, d, e)
|
walther@59982
|
43 |
|
walther@59982
|
44 |
fun is_from (hdf : TermC.as_string) ((fmz_, spec) : Formalise.T) =
|
walther@59982
|
45 |
hdf <> "" andalso fmz_ = [] andalso spec = References.empty
|
walther@59982
|
46 |
|
Walther@60729
|
47 |
fun input_ ((dI, pI, mI): References.T) dtss = (*WN110515 reconsider thy..ctxt*)
|
Walther@60729
|
48 |
let
|
Walther@60729
|
49 |
val thy = Know_Store.get_via_last_thy dI
|
Walther@60729
|
50 |
val ctxt = Proof_Context.init_global thy
|
Walther@60729
|
51 |
val {model, ...} = Problem.from_store ctxt pI
|
Walther@60729
|
52 |
val its_ = map (dtss2itm_ model) dtss (*([1],true,"#Given",Cor (...))*)
|
Walther@60729
|
53 |
val its = O_Model.add_enumerate its_
|
Walther@60729
|
54 |
val pits = map flattup2 its
|
Walther@60729
|
55 |
val (pI, mI) =
|
Walther@60729
|
56 |
if mI <> ["no_met"]
|
Walther@60729
|
57 |
then (pI, mI)
|
Walther@60729
|
58 |
else
|
Walther@60778
|
59 |
case Refine.problem thy pI pits of
|
Walther@60729
|
60 |
SOME (pI, _) => (pI, (hd o #solve_mets o Problem.from_store ctxt) pI)
|
Walther@60729
|
61 |
| NONE => (pI, (hd o #solve_mets o Problem.from_store ctxt) pI)
|
Walther@60729
|
62 |
val {model, where_, where_rls, ...} = MethodC.from_store ctxt mI
|
Walther@60729
|
63 |
val its_ = map (dtss2itm_ model) dtss (*([1],true,"#Given",Cor (...))*)
|
Walther@60729
|
64 |
val its = O_Model.add_enumerate its_
|
Walther@60729
|
65 |
val mits = map flattup2 its
|
Walther@60778
|
66 |
val (_, where_) = Pre_Conds.check ctxt where_rls where_ (model, mits)
|
Walther@60729
|
67 |
val ctxt = Proof_Context.init_global thy
|
Walther@60778
|
68 |
in (pI, pits, mI, mits, where_, ctxt) end;
|
walther@59982
|
69 |
|
walther@59982
|
70 |
(* check if the input term is a CAScmd and return a ctree with a _complete_ calchead *)
|
walther@59982
|
71 |
fun input hdt =
|
walther@59982
|
72 |
let
|
walther@59982
|
73 |
val (h, argl) = strip_comb hdt
|
walther@59982
|
74 |
in
|
Walther@60550
|
75 |
case get_cas_global h of
|
walther@59982
|
76 |
NONE => NONE
|
walther@59982
|
77 |
| SOME (spec as (dI,_,_), argl2dtss) =>
|
walther@59982
|
78 |
let
|
walther@59982
|
79 |
val dtss = argl2dtss argl
|
Walther@60586
|
80 |
val (pI, pits, mI, mits, where_, ctxt) = input_ spec dtss
|
walther@59982
|
81 |
val spec = (dI, pI, mI)
|
walther@59982
|
82 |
val (pt,_) = Ctree.cappend_problem Ctree.e_ctree [] (Istate_Def.empty, ContextC.empty)
|
walther@59982
|
83 |
([], References.empty) ([], References.empty, hdt, ctxt)
|
walther@59982
|
84 |
val pt = Ctree.update_spec pt [] spec
|
Walther@60779
|
85 |
val pt = Ctree.update_pbl pt [] pits
|
Walther@60779
|
86 |
val pt = Ctree.update_met pt [] mits
|
walther@59982
|
87 |
in
|
Walther@60773
|
88 |
SOME (pt, (true, Pos.Met, hdt, mits, where_, spec) : SpecificationC.T)
|
walther@59982
|
89 |
end
|
walther@59982
|
90 |
end
|
walther@59894
|
91 |
|
wenzelm@60314
|
92 |
|
wenzelm@60314
|
93 |
(** Isar command **)
|
wenzelm@60314
|
94 |
|
wenzelm@60314
|
95 |
local
|
wenzelm@60314
|
96 |
|
Walther@60449
|
97 |
val parse_theory = Problem.parse_item_name \<^keyword>\<open>Theory_Ref\<close> "Isac_Knowledge";
|
Walther@60449
|
98 |
val parse_problem = Problem.parse_item \<^keyword>\<open>Problem_Ref\<close> Parse.name;
|
Walther@60449
|
99 |
val parse_method = Problem.parse_item_name \<^keyword>\<open>Method_Ref\<close> "no_met";
|
wenzelm@60314
|
100 |
|
wenzelm@60314
|
101 |
val ml = ML_Lex.read;
|
wenzelm@60314
|
102 |
|
wenzelm@60314
|
103 |
val _ =
|
wenzelm@60314
|
104 |
Outer_Syntax.command \<^command_keyword>\<open>cas\<close>
|
wenzelm@60314
|
105 |
"prepare ISAC Computer-Algebra System and register it to Knowledge Store"
|
wenzelm@60314
|
106 |
(Parse.term -- (\<^keyword>\<open>=\<close> |--
|
wenzelm@60314
|
107 |
Parse.!!! (Parse.ML_source -- parse_theory -- parse_problem -- parse_method))
|
wenzelm@60314
|
108 |
>> (fn (term, (((source, thry), pbl), met)) => Toplevel.theory (fn thy =>
|
wenzelm@60314
|
109 |
let
|
Walther@60661
|
110 |
(*/------------ replace by ParseC.term_position ------------------\*)
|
Walther@60661
|
111 |
val SOME t = ParseC.term_opt (Proof_Context.init_global thy) term;
|
Walther@60661
|
112 |
(*\------------ replace by ParseC.term_position ------------------/*)
|
wenzelm@60314
|
113 |
val pblID = References_Def.explode_id pbl;
|
wenzelm@60314
|
114 |
val metID = References_Def.explode_id met;
|
wenzelm@60314
|
115 |
val set_data =
|
wenzelm@60314
|
116 |
ML_Context.expression (Input.pos_of source)
|
wenzelm@60314
|
117 |
(ml "Theory.setup (CAS_Def.set_data (" @ ML_Lex.read_source source @ ml "))")
|
wenzelm@60314
|
118 |
|> Context.theory_map;
|
wenzelm@60314
|
119 |
val data = CAS_Def.the_data (set_data thy);
|
Walther@60588
|
120 |
in Know_Store.add_cass [(t, ((thry, pblID, metID), data))] thy end)));
|
wenzelm@60314
|
121 |
|
wenzelm@60314
|
122 |
in end;
|
wenzelm@60314
|
123 |
|
walther@59894
|
124 |
(**)end(**)
|