(* Title: "Specify/input-descript.sml"

   Author: Walther Neuper 060605

   (c) due to copyright terms

*)

"----------------------------------------------------------------------------------------------";

"table of contents ----------------------------------------------------------------------------";

"----------------------------------------------------------------------------------------------";

"-------- distinguish input to I_Model --------------------------------------------------------";

"----------------------------------------------------------------------------------------------";

"----------------------------------------------------------------------------------------------";

"----------------------------------------------------------------------------------------------";

"-------- distinguish input to I_Model --------------------------------------------------------";

"-------- distinguish input to I_Model --------------------------------------------------------";

"-------- distinguish input to I_Model --------------------------------------------------------";

"----- fun Input_Descript.for_bool_list -----";

val t as Const (\<^const_name>\<open>Input_Descript.relations\<close>, 

  Type (\<^type_name>\<open>fun\<close>, [Type (\<^type_name>\<open>list\<close>, [Type (\<^type_name>\<open>bool\<close>,[])]), 

    Type e(\<^type_name>\<open>una\<close>, [])])) = @{term "relations"};

TermC.atom_typ @{context} (type_of t);

if Input_Descript.for_bool_list t then () else error "Input_Descript.for_bool_list changed";

"----- fun Input_Descript.for_real -----";

if not (Input_Descript.for_real t) then () else error "Input_Descript.for_real changed";

"----- fun is_list_dsc -----";

val t = @{term "someList"};

if is_list_dsc t then () else error "is_list_dsc changed 1";

val t = @{term "additionalRels [a=b,c=(d::real)]"};

if is_list_dsc t then () else error "is_list_dsc changed 2";

if is_list_dsc (head_of t) then () else error "is_list_dsc changed 3";

"----- fun is_list_dsc -----";

val t = @{term "maximum"};

if Input_Descript.is_a t then () else error "Input_Descript.is_a changed 1";

val t = head_of @{term "maximum A"};

if Input_Descript.is_a t then () else error "Input_Descript.is_a changed 2";

val t = head_of @{term "fixedValues [R=(R::real)]"};

if Input_Descript.is_a t then () else error "Input_Descript.is_a changed 3";