1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Tools/isac/Specify/cas-command.sml	Thu May 14 16:58:33 2020 +0200
     1.3 @@ -0,0 +1,90 @@
     1.4 +(* Title:  Interpret/lucas-interpreter.sml
     1.5 +   Author: Walther Neuper 2019
     1.6 +   (c) due to copyright terms
     1.7 +*)
     1.8 +
     1.9 +signature COMPUTER_ALGEBRA_SYSTEM_COMMAND =
    1.10 +sig
    1.11 +  type T = CAS_Def.T
    1.12 +  val input : term -> (Ctree.ctree * Specification.T) option
    1.13 +  val is_from: TermC.as_string -> Formalise.T -> bool
    1.14 +
    1.15 +(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
    1.16 +  (*NONE*)
    1.17 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
    1.18 +(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
    1.19 +  val input_: References.T -> (term * term list) list ->
    1.20 +    Problem.id * I_Model.T * Method.id * I_Model.T * Pre_Conds.T * Proof.context
    1.21 +
    1.22 +  val dtss2itm_: Model_Pattern.T -> term * term list ->
    1.23 +    int list * bool * string * I_Model.feedback (*I_Model.single'*)
    1.24 +  val flattup2: 'a * ('b * 'c * 'd * 'e) -> 'a * 'b * 'c * 'd * 'e
    1.25 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
    1.26 +end
    1.27 +
    1.28 +(**)
    1.29 +structure CAS_Cmd(**): COMPUTER_ALGEBRA_SYSTEM_COMMAND(**) =
    1.30 +struct
    1.31 +(**)
    1.32 +
    1.33 +type T = CAS_Def.T;
    1.34 +
    1.35 +fun dtss2itm_ ppc (d, ts) =
    1.36 +  let
    1.37 +    val (f, (d, id)) = the (find_first ((curry op= d) o 
    1.38 +  		(#1: (term * term) -> term) o
    1.39 +  		(#2: Model_Pattern.single -> (term * term))) ppc)
    1.40 +  in
    1.41 +    ([1], true, f, I_Model.Cor ((d, ts), (id, ts)))
    1.42 +  end
    1.43 +
    1.44 +fun flattup2 (a, (b ,c, d, e)) = (a, b, c, d, e)
    1.45 +
    1.46 +fun is_from (hdf : TermC.as_string) ((fmz_, spec) : Formalise.T) =
    1.47 +  hdf <> "" andalso fmz_ = [] andalso spec = References.empty
    1.48 +
    1.49 +fun input_ ((dI, pI, mI): References.T) dtss = (*WN110515 reconsider thy..ctxt*)
    1.50 +  let
    1.51 +    val thy = ThyC.get_theory dI
    1.52 +	  val {ppc, ...} = Problem.from_store pI
    1.53 +	  val its_ = map (dtss2itm_ ppc) dtss (*([1],true,"#Given",Cor (...))*)
    1.54 +	  val its = O_Model.add_id its_
    1.55 +	  val pits = map flattup2 its
    1.56 +	  val (pI, mI) =
    1.57 +      if mI <> ["no_met"]
    1.58 +      then (pI, mI)
    1.59 +		  else
    1.60 +        case Refine.problem thy pI pits of
    1.61 +			    SOME (pI,_) => (pI, (hd o #met o Problem.from_store) pI)
    1.62 +			  | NONE => (pI, (hd o #met o Problem.from_store) pI)
    1.63 +	  val {ppc, pre, prls, ...} = Method.from_store mI
    1.64 +	  val its_ = map (dtss2itm_ ppc) dtss (*([1],true,"#Given",Cor (...))*)
    1.65 +	  val its = O_Model.add_id its_
    1.66 +	  val mits = map flattup2 its
    1.67 +	  val pre = Pre_Conds.check' thy prls pre mits
    1.68 +    val ctxt = Proof_Context.init_global thy
    1.69 +  in (pI, pits, mI, mits, pre, ctxt) end;
    1.70 +
    1.71 +(* check if the input term is a CAScmd and return a ctree with a _complete_ calchead *)
    1.72 +fun input hdt =
    1.73 +  let
    1.74 +    val (h, argl) = strip_comb hdt
    1.75 +  in
    1.76 +    case assoc_cas (ThyC.get_theory "Isac_Knowledge") h of
    1.77 +      NONE => NONE
    1.78 +    | SOME (spec as (dI,_,_), argl2dtss) =>
    1.79 +	      let
    1.80 +          val dtss = argl2dtss argl
    1.81 +	        val (pI, pits, mI, mits, pre, ctxt) = input_ spec dtss
    1.82 +	        val spec = (dI, pI, mI)
    1.83 +	        val (pt,_) = Ctree.cappend_problem Ctree.e_ctree [] (Istate_Def.empty, ContextC.empty)
    1.84 +		        ([], References.empty) ([], References.empty, hdt, ctxt)
    1.85 +	        val pt = Ctree.update_spec pt [] spec
    1.86 +	        val pt = Ctree.update_pbl pt [] pits
    1.87 +	        val pt = Ctree.update_met pt [] mits
    1.88 +	      in
    1.89 +	        SOME (pt, (true, Pos.Met, hdt, mits, pre, spec) : Specification.T)
    1.90 +	      end
    1.91 +  end
    1.92 +
    1.93 +(**)end(**)