Walther@60778: (* Title: Interpret/cas-command.sml walther@59894: Author: Walther Neuper 2019 walther@59894: *) walther@59894: walther@59894: signature COMPUTER_ALGEBRA_SYSTEM_COMMAND = walther@59894: sig Walther@60603: type input_pos walther@59982: type T = CAS_Def.T walther@60097: val input : term -> (Ctree.ctree * SpecificationC.T) option walther@59982: val is_from: TermC.as_string -> Formalise.T -> bool Walther@60772: Walther@60772: (*/----- from isac_test for Minisubpbl*) walther@59982: val input_: References.T -> (term * term list) list -> Walther@60782: Problem.id * I_Model.T * MethodC.id * I_Model.T * Pre_Conds.T * Proof.context walther@59982: val dtss2itm_: Model_Pattern.T -> term * term list -> Walther@60782: int list * bool * Model_Def.m_field * (I_Model.feedback * Position.T) walther@59982: val flattup2: 'a * ('b * 'c * 'd * 'e) -> 'a * 'b * 'c * 'd * 'e Walther@60772: (*\----- from isac_test for Minisubpbl*) Walther@60772: Walther@60772: \<^isac_test>\ Walther@60772: (*put "from isac_test for Minisubpbl" here*) wenzelm@60223: \ walther@59894: end walther@59894: walther@59894: (**) walther@59894: structure CAS_Cmd(**): COMPUTER_ALGEBRA_SYSTEM_COMMAND(**) = walther@59894: struct walther@59894: (**) walther@59894: Walther@60603: type input_pos = CAS_Def.input_pos; Walther@60547: type T = CAS_Def.T; (*(term * (References_Def.T * generate_fn))*) walther@59896: Walther@60586: fun dtss2itm_ model (d, ts) = walther@59982: let walther@59982: val (f, (d, id)) = the (find_first ((curry op= d) o walther@59982: (#1: (term * term) -> term) o Walther@60586: (#2: Model_Pattern.single -> (term * term))) model) walther@59982: in Walther@60782: ([1], true, f, (I_Model.Cor (d, ts), Position.none)) walther@59982: end walther@59982: walther@59982: fun flattup2 (a, (b ,c, d, e)) = (a, b, c, d, e) walther@59982: walther@59982: fun is_from (hdf : TermC.as_string) ((fmz_, spec) : Formalise.T) = walther@59982: hdf <> "" andalso fmz_ = [] andalso spec = References.empty walther@59982: Walther@60729: fun input_ ((dI, pI, mI): References.T) dtss = (*WN110515 reconsider thy..ctxt*) Walther@60729: let Walther@60729: val thy = Know_Store.get_via_last_thy dI Walther@60729: val ctxt = Proof_Context.init_global thy Walther@60729: val {model, ...} = Problem.from_store ctxt pI Walther@60729: val its_ = map (dtss2itm_ model) dtss (*([1],true,"#Given",Cor (...))*) Walther@60729: val its = O_Model.add_enumerate its_ Walther@60729: val pits = map flattup2 its Walther@60729: val (pI, mI) = Walther@60729: if mI <> ["no_met"] Walther@60729: then (pI, mI) Walther@60729: else Walther@60778: case Refine.problem thy pI pits of Walther@60729: SOME (pI, _) => (pI, (hd o #solve_mets o Problem.from_store ctxt) pI) Walther@60729: | NONE => (pI, (hd o #solve_mets o Problem.from_store ctxt) pI) Walther@60729: val {model, where_, where_rls, ...} = MethodC.from_store ctxt mI Walther@60729: val its_ = map (dtss2itm_ model) dtss (*([1],true,"#Given",Cor (...))*) Walther@60729: val its = O_Model.add_enumerate its_ Walther@60729: val mits = map flattup2 its Walther@60778: val (_, where_) = Pre_Conds.check ctxt where_rls where_ (model, mits) Walther@60729: val ctxt = Proof_Context.init_global thy Walther@60778: in (pI, pits, mI, mits, where_, ctxt) end; walther@59982: walther@59982: (* check if the input term is a CAScmd and return a ctree with a _complete_ calchead *) walther@59982: fun input hdt = walther@59982: let walther@59982: val (h, argl) = strip_comb hdt walther@59982: in Walther@60550: case get_cas_global h of walther@59982: NONE => NONE walther@59982: | SOME (spec as (dI,_,_), argl2dtss) => walther@59982: let walther@59982: val dtss = argl2dtss argl Walther@60586: val (pI, pits, mI, mits, where_, ctxt) = input_ spec dtss walther@59982: val spec = (dI, pI, mI) walther@59982: val (pt,_) = Ctree.cappend_problem Ctree.e_ctree [] (Istate_Def.empty, ContextC.empty) walther@59982: ([], References.empty) ([], References.empty, hdt, ctxt) walther@59982: val pt = Ctree.update_spec pt [] spec Walther@60779: val pt = Ctree.update_pbl pt [] pits Walther@60779: val pt = Ctree.update_met pt [] mits walther@59982: in Walther@60773: SOME (pt, (true, Pos.Met, hdt, mits, where_, spec) : SpecificationC.T) walther@59982: end walther@59982: end walther@59894: wenzelm@60314: wenzelm@60314: (** Isar command **) wenzelm@60314: wenzelm@60314: local wenzelm@60314: Walther@60449: val parse_theory = Problem.parse_item_name \<^keyword>\Theory_Ref\ "Isac_Knowledge"; Walther@60449: val parse_problem = Problem.parse_item \<^keyword>\Problem_Ref\ Parse.name; Walther@60449: val parse_method = Problem.parse_item_name \<^keyword>\Method_Ref\ "no_met"; wenzelm@60314: wenzelm@60314: val ml = ML_Lex.read; wenzelm@60314: wenzelm@60314: val _ = wenzelm@60314: Outer_Syntax.command \<^command_keyword>\cas\ wenzelm@60314: "prepare ISAC Computer-Algebra System and register it to Knowledge Store" wenzelm@60314: (Parse.term -- (\<^keyword>\=\ |-- wenzelm@60314: Parse.!!! (Parse.ML_source -- parse_theory -- parse_problem -- parse_method)) wenzelm@60314: >> (fn (term, (((source, thry), pbl), met)) => Toplevel.theory (fn thy => wenzelm@60314: let Walther@60661: (*/------------ replace by ParseC.term_position ------------------\*) Walther@60661: val SOME t = ParseC.term_opt (Proof_Context.init_global thy) term; Walther@60661: (*\------------ replace by ParseC.term_position ------------------/*) wenzelm@60314: val pblID = References_Def.explode_id pbl; wenzelm@60314: val metID = References_Def.explode_id met; wenzelm@60314: val set_data = wenzelm@60314: ML_Context.expression (Input.pos_of source) wenzelm@60314: (ml "Theory.setup (CAS_Def.set_data (" @ ML_Lex.read_source source @ ml "))") wenzelm@60314: |> Context.theory_map; wenzelm@60314: val data = CAS_Def.the_data (set_data thy); Walther@60588: in Know_Store.add_cass [(t, ((thry, pblID, metID), data))] thy end))); wenzelm@60314: wenzelm@60314: in end; wenzelm@60314: walther@59894: (**)end(**)