1 (* Title: Interpret/lucas-interpreter.sml
2 Author: Walther Neuper 2019
3 (c) due to copyright terms
6 signature COMPUTER_ALGEBRA_SYSTEM_COMMAND =
9 val input : term -> (Ctree.ctree * SpecificationC.T) option
10 val is_from: TermC.as_string -> Formalise.T -> bool
12 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
14 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
15 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
16 val input_: References.T -> (term * term list) list ->
17 Problem.id * I_Model.T * MethodC.id * I_Model.T * Pre_Conds.T * Proof.context
19 val dtss2itm_: Model_Pattern.T -> term * term list ->
20 int list * bool * string * I_Model.feedback (*I_Model.single'*)
21 val flattup2: 'a * ('b * 'c * 'd * 'e) -> 'a * 'b * 'c * 'd * 'e
22 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
26 structure CAS_Cmd(**): COMPUTER_ALGEBRA_SYSTEM_COMMAND(**) =
32 fun dtss2itm_ ppc (d, ts) =
34 val (f, (d, id)) = the (find_first ((curry op= d) o
35 (#1: (term * term) -> term) o
36 (#2: Model_Pattern.single -> (term * term))) ppc)
38 ([1], true, f, I_Model.Cor ((d, ts), (id, ts)))
41 fun flattup2 (a, (b ,c, d, e)) = (a, b, c, d, e)
43 fun is_from (hdf : TermC.as_string) ((fmz_, spec) : Formalise.T) =
44 hdf <> "" andalso fmz_ = [] andalso spec = References.empty
46 fun input_ ((dI, pI, mI): References.T) dtss = (*WN110515 reconsider thy..ctxt*)
48 val thy = ThyC.get_theory dI
49 val {ppc, ...} = Problem.from_store pI
50 val its_ = map (dtss2itm_ ppc) dtss (*([1],true,"#Given",Cor (...))*)
51 val its = O_Model.add_id its_
52 val pits = map flattup2 its
57 case Refine.problem thy pI pits of
58 SOME (pI,_) => (pI, (hd o #met o Problem.from_store) pI)
59 | NONE => (pI, (hd o #met o Problem.from_store) pI)
60 val {ppc, pre, prls, ...} = MethodC.from_store mI
61 val its_ = map (dtss2itm_ ppc) dtss (*([1],true,"#Given",Cor (...))*)
62 val its = O_Model.add_id its_
63 val mits = map flattup2 its
64 val (_, pre) = Pre_Conds.check prls pre mits 0
65 val ctxt = Proof_Context.init_global thy
66 in (pI, pits, mI, mits, pre, ctxt) end;
68 (* check if the input term is a CAScmd and return a ctree with a _complete_ calchead *)
71 val (h, argl) = strip_comb hdt
73 case assoc_cas (ThyC.get_theory "Isac_Knowledge") h of
75 | SOME (spec as (dI,_,_), argl2dtss) =>
77 val dtss = argl2dtss argl
78 val (pI, pits, mI, mits, pre, ctxt) = input_ spec dtss
79 val spec = (dI, pI, mI)
80 val (pt,_) = Ctree.cappend_problem Ctree.e_ctree [] (Istate_Def.empty, ContextC.empty)
81 ([], References.empty) ([], References.empty, hdt, ctxt)
82 val pt = Ctree.update_spec pt [] spec
83 val pt = Ctree.update_pbl pt [] pits
84 val pt = Ctree.update_met pt [] mits
86 SOME (pt, (true, Pos.Met, hdt, mits, pre, spec) : SpecificationC.T)