(* Title:  collect all defitions for the Lucas-Interpreter

   Author: Walther Neuper 110226

   (c) due to copyright terms

 *)

theory Input_Descript imports "~~/src/Tools/isac/CalcElements/CalcElements"

begin

subsection \<open>typedecl for descriptions of input in specify-phase\<close>

text \<open>

  The typedecl below MUST ALL be registered in "fun is_dsc"

\<close>

  typedecl nam     (* named variables                                             *)

  typedecl una     (* unnamed variables                                           *)

  typedecl unl     (* unnamed variables of type list, elementwise input prohibited*)

  typedecl str     (* structured variables                                        *)

  typedecl toreal  (* var with undef real value: forces typing                    *)

  typedecl toreall (* var with undef real list value: forces typing               *)

  typedecl tobooll (* var with undef bool list value: forces typing               *)

  typedecl unknow  (* input without dsc in fmz=[]                                 *)

  typedecl cpy     (* copy-named variables identified by .._0, .._i .._' in pbt   *)

subsection \<open>consts for general descriptions of input in specify-phase\<close>

consts

(*TODO.180331: review for localisation of model-patterns and of method's guards*)

  someList       :: "'a list => unl" (*not for elementwise input, eg. inssort*)

  additionalRels :: "bool list => una"

  boundVariable  :: "real => una"

  derivative     :: "real => una"

  equalities     :: "bool list => tobooll" (*WN071228 see fixedValues*)

  equality       :: "bool => una"

  errorBound     :: "bool => nam"

  fixedValues    :: "bool list => nam"

  functionEq     :: "bool => una"     (*6.5.03: functionTerm -> functionEq*)

  antiDerivative :: "bool => una"

  functionOf     :: "real => una"

(*functionTerm   :: 'a => toreal 28.11.00*)

  functionTerm   :: "real => una"     (*6.5.03: functionTerm -> functionEq*)

  functionName   :: "real => una"

  interval       :: "real set => una"

  maxArgument    :: "bool => toreal"

  maximum        :: "real => toreal"

  relations      :: "bool list => una"

  solutions      :: "bool list => toreall"

(*solution       :: bool => toreal  WN0509 bool list=> toreall --->EqSystem*)

  solveFor       :: "real => una"

  differentiateFor:: "real => una"

  unknown        :: "'a => unknow"

  valuesFor      :: "real list => toreall"

  intTestGiven   :: "int => una"

  realTestGiven  :: "real => una"

  realTestFind   :: "real => una"

  boolTestGiven  :: "bool => una"

  boolTestFind   :: "bool => una"

subsection \<open>Functions decking for descriptions of input in specify-phase\<close>

ML \<open>

\<close> ML \<open>

signature INPUT_DESCRIPT =

sig

  val is_reall_dsc: term -> bool

  val is_booll_dsc: term -> bool

  val is_list_dsc: term -> bool

  val is_unl: term -> bool

  val is_dsc: term -> bool 

  val pbl_ids: Proof.context -> term -> term -> term list

(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)

  (* NONE *)

(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )

  (* NONE *)

( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)

end

\<close> ML \<open>

(**)

structure Input_Descript(**): INPUT_DESCRIPT =(**)

struct

(**)

(* distinguish input to Model (deep embedding of terms as Isac's object language) *)

fun is_reall_dsc (Const (_, Type("fun", [Type ("List.list", [Type ("Real.real", [])]), _]))) = true

  | is_reall_dsc (Const (_, Type("fun", [Type ("List.list", [Type ("Real.real", [])]),_])) $ _) = true

  | is_reall_dsc _ = false;

fun is_booll_dsc (Const (_, Type("fun", [Type ("List.list", [Type ("HOL.bool", [])]), _]))) = true

  | is_booll_dsc (Const (_, Type("fun", [Type ("List.list", [Type ("HOL.bool", [])]),_])) $ _) = true

  | is_booll_dsc _ = false;

fun is_list_dsc (Const (_, Type("fun", [Type("List.list", _), _]))) = true

  | is_list_dsc (Const (_, Type("fun", [Type("List.list", _), _])) $ _) = true

  (*WN:8.5.03: ???   TODO test/../scrtools.sml                ~~~~ ???*)

  | is_list_dsc _ = false;

fun is_unl (Const (_, Type("fun", [_, Type("Input_Descript.unl", _)]))) = true

  | is_unl _ = false;

fun is_dsc (Const(_, Type("fun", [_, Type ("Input_Descript.nam",_)]))) = true

  | is_dsc (Const(_, Type("fun", [_, Type ("Input_Descript.una",_)]))) = true

  | is_dsc (Const(_, Type("fun", [_, Type ("Input_Descript.unl",_)]))) = true

  | is_dsc (Const(_, Type("fun", [_, Type ("Input_Descript.str",_)]))) = true

  | is_dsc (Const(_, Type("fun", [_, Type ("Input_Descript.toreal",_)]))) = true

  | is_dsc (Const(_, Type("fun", [_, Type ("Input_Descript.toreall",_)])))= true

  | is_dsc (Const(_, Type("fun", [_, Type ("Input_Descript.tobooll",_)])))= true

  | is_dsc (Const(_, Type("fun", [_, Type ("Input_Descript.unknow",_)])))= true

  | is_dsc (Const(_, Type("fun", [_, Type ("Input_Descript.cpy",_)])))= true

  | is_dsc _ = false;

(* given the input value (from split_dts)

   make the value in a problem-env according to description-type

  28.8.01: .nam and .una impl. properly, others copied .. TODO.

  19/03/15 17:33, Makarius wrote:

  >>>     val i = case HOLogic.dest_number t of

  >>>               (Type ("Nat.nat", []), i) => i

  >> Formal names should never be hardwired as ML string constants.  Use

  >> @{type_name nat} above, or better @{typ nat} for the whole type  *)

fun pbl_ids ctxt (Const(_, Type ("fun", [_, Type ("Input_Descript.nam", _)]))) v =

    if TermC.is_list v 

    then [v]      (*eg. [r=Arbfix]*)

    else

      (case v of  (*eg. eps=#0*) (Const ("HOL.eq", _) $ l $ r) => [r, l]

	    | _ => error ("pbl_ids Input_Descript.nam: no equality " ^ Rule.term_to_string' ctxt v))

  | pbl_ids _ (Const (_, Type ("fun", [_,Type ("Input_Descript.una", _)]))) v = [v]

  | pbl_ids _ (Const (_, Type ("fun", [_,Type ("Input_Descript.unl", _)]))) v = [v]

  | pbl_ids _ (Const (_, Type ("fun", [_,Type ("Input_Descript.str", _)]))) v = [v]

  | pbl_ids _ (Const (_, Type ("fun", [_,Type ("Input_Descript.toreal", _)]))) v = [v] 

  | pbl_ids _ (Const (_, Type ("fun", [_,Type ("Input_Descript.toreall", _)])))v = [v] 

  | pbl_ids _ (Const (_, Type ("fun", [_,Type ("Input_Descript.unknown" ,_)])))v = [v] 

  | pbl_ids _ _ v = error ("pbl_ids: not implemented for " ^ Rule.term2str v);

(* given an already input itm, ((14.9.01: no difference to pbl_ids jet!!))

   make the value in a problem-env according to description-type.

   28.8.01: .nam and .una impl. properly, others copied .. TODO

fun pbl_ids' (Const(_, Type ("fun", [_, Type ("Input_Descript.nam", _)]))) vs =

    (case vs of 

      [] => error ("pbl_ids' Input_Descript.nam called with []")

    | [t] =>

        (case t of  (*eg. eps=#0*)

          (Const ("HOL.eq",_) $ l $ r) => [r,l]

        | _ => error ("pbl_ids' Input_Descript.nam: no equality " ^ term2str t))

    | _ => vs (*14.9.01: ???TODO *))

  | pbl_ids' (Const (_, Type ("fun", [_, Type("Input_Descript.una", _)]))) vs = vs

  | pbl_ids' (Const (_, Type ("fun", [_, Type("Input_Descript.unl", _)]))) vs = vs

  | pbl_ids' (Const (_, Type ("fun", [_, Type("Input_Descript.str", _)]))) vs = vs

  | pbl_ids' (Const (_, Type ("fun", [_, Type("Input_Descript.toreal", _)]))) vs = vs 

  | pbl_ids' (Const (_, Type ("fun", [_, Type("Input_Descript.toreall", _)])))vs = vs 

  | pbl_ids' (Const (_, Type ("fun", [_, Type("Input_Descript.unknown", _)])))vs = vs 

  | pbl_ids'  _ vs = error ("pbl_ids': not implemented for " ^ terms2str vs);*)

(**)end(**)

\<close> ML \<open>

\<close> ML \<open>

\<close> 

end