1 (* Title: Interpret/lucas-interpreter.sml
2 Author: Walther Neuper 2019
3 (c) due to copyright terms
6 signature COMPUTER_ALGEBRA_SYSTEM_COMMAND =
10 val input : term -> (Ctree.ctree * SpecificationC.T) option
11 val is_from: TermC.as_string -> Formalise.T -> bool
13 (*/----- from isac_test for Minisubpbl*)
14 val input_: References.T -> (term * term list) list ->
15 Problem.id * I_Model.T_POS * MethodC.id * I_Model.T_POS * Pre_Conds.T * Proof.context
16 val dtss2itm_: Model_Pattern.T -> term * term list ->
17 int list * bool * string * I_Model.feedback (*I_Model.single'*)
18 val flattup2: 'a * ('b * 'c * 'd * 'e) -> 'a * 'b * 'c * 'd * 'e
19 (*\----- from isac_test for Minisubpbl*)
22 (*put "from isac_test for Minisubpbl" here*)
27 structure CAS_Cmd(**): COMPUTER_ALGEBRA_SYSTEM_COMMAND(**) =
31 type input_pos = CAS_Def.input_pos;
32 type T = CAS_Def.T; (*(term * (References_Def.T * generate_fn))*)
34 fun dtss2itm_ model (d, ts) =
36 val (f, (d, id)) = the (find_first ((curry op= d) o
37 (#1: (term * term) -> term) o
38 (#2: Model_Pattern.single -> (term * term))) model)
40 ([1], true, f, I_Model.Cor ((d, ts), (id, ts)))
43 fun flattup2 (a, (b ,c, d, e)) = (a, b, c, d, e)
45 fun is_from (hdf : TermC.as_string) ((fmz_, spec) : Formalise.T) =
46 hdf <> "" andalso fmz_ = [] andalso spec = References.empty
48 fun input_ ((dI, pI, mI): References.T) dtss = (*WN110515 reconsider thy..ctxt*)
50 val thy = Know_Store.get_via_last_thy dI
51 val ctxt = Proof_Context.init_global thy
52 val {model, ...} = Problem.from_store ctxt pI
53 val its_ = map (dtss2itm_ model) dtss (*([1],true,"#Given",Cor (...))*)
54 val its = O_Model.add_enumerate its_
55 val pits = map flattup2 its
60 case Refine.problem thy pI pits of
61 SOME (pI, _) => (pI, (hd o #solve_mets o Problem.from_store ctxt) pI)
62 | NONE => (pI, (hd o #solve_mets o Problem.from_store ctxt) pI)
63 val {model, where_, where_rls, ...} = MethodC.from_store ctxt mI
64 val its_ = map (dtss2itm_ model) dtss (*([1],true,"#Given",Cor (...))*)
65 val its = O_Model.add_enumerate its_
66 val mits = map flattup2 its
67 val (_, where_) = Pre_Conds.check ctxt where_rls where_ (model, I_Model.OLD_to_POS mits)
68 val ctxt = Proof_Context.init_global thy
69 in (pI, I_Model.OLD_to_POS pits, mI, I_Model.OLD_to_POS mits, where_, ctxt) end;
71 (* check if the input term is a CAScmd and return a ctree with a _complete_ calchead *)
74 val (h, argl) = strip_comb hdt
76 case get_cas_global h of
78 | SOME (spec as (dI,_,_), argl2dtss) =>
80 val dtss = argl2dtss argl
81 val (pI, pits, mI, mits, where_, ctxt) = input_ spec dtss
82 val spec = (dI, pI, mI)
83 val (pt,_) = Ctree.cappend_problem Ctree.e_ctree [] (Istate_Def.empty, ContextC.empty)
84 ([], References.empty) ([], References.empty, hdt, ctxt)
85 val pt = Ctree.update_spec pt [] spec
86 val pt = Ctree.update_pbl pt [] (I_Model.TEST_to_OLD pits)
87 val pt = Ctree.update_met pt [] (I_Model.TEST_to_OLD mits)
89 (*quick and dirty------------------------vvvvvvvvvvvvvvvvvvv-----*)
90 SOME (pt, (true, Pos.Met, hdt, I_Model.TEST_to_OLD mits, where_, spec) : SpecificationC.T)
99 val parse_theory = Problem.parse_item_name \<^keyword>\<open>Theory_Ref\<close> "Isac_Knowledge";
100 val parse_problem = Problem.parse_item \<^keyword>\<open>Problem_Ref\<close> Parse.name;
101 val parse_method = Problem.parse_item_name \<^keyword>\<open>Method_Ref\<close> "no_met";
103 val ml = ML_Lex.read;
106 Outer_Syntax.command \<^command_keyword>\<open>cas\<close>
107 "prepare ISAC Computer-Algebra System and register it to Knowledge Store"
108 (Parse.term -- (\<^keyword>\<open>=\<close> |--
109 Parse.!!! (Parse.ML_source -- parse_theory -- parse_problem -- parse_method))
110 >> (fn (term, (((source, thry), pbl), met)) => Toplevel.theory (fn thy =>
112 (*/------------ replace by ParseC.term_position ------------------\*)
113 val SOME t = ParseC.term_opt (Proof_Context.init_global thy) term;
114 (*\------------ replace by ParseC.term_position ------------------/*)
115 val pblID = References_Def.explode_id pbl;
116 val metID = References_Def.explode_id met;
118 ML_Context.expression (Input.pos_of source)
119 (ml "Theory.setup (CAS_Def.set_data (" @ ML_Lex.read_source source @ ml "))")
120 |> Context.theory_map;
121 val data = CAS_Def.the_data (set_data thy);
122 in Know_Store.add_cass [(t, ((thry, pblID, metID), data))] thy end)));