wneuper@59596: (* Title: "Specify/input-descript.sml"
wneuper@59596:    Author: Walther Neuper 060605
wneuper@59596:    (c) due to copyright terms
wneuper@59596: *)
wneuper@59596: "----------------------------------------------------------------------------------------------";
wneuper@59596: "table of contents ----------------------------------------------------------------------------";
wneuper@59596: "----------------------------------------------------------------------------------------------";
walther@59959: "-------- distinguish input to I_Model --------------------------------------------------------";
wneuper@59596: "----------------------------------------------------------------------------------------------";
wneuper@59596: "----------------------------------------------------------------------------------------------";
wneuper@59596: "----------------------------------------------------------------------------------------------";
wneuper@59596: 
wneuper@59596: 
walther@59959: "-------- distinguish input to I_Model --------------------------------------------------------";
walther@59959: "-------- distinguish input to I_Model --------------------------------------------------------";
walther@59959: "-------- distinguish input to I_Model --------------------------------------------------------";
walther@59953: "----- fun Input_Descript.for_bool_list -----";
walther@60336: val t as Const (\<^const_name>\<open>Input_Descript.relations\<close>, 
wenzelm@60309:   Type (\<^type_name>\<open>fun\<close>, [Type (\<^type_name>\<open>list\<close>, [Type (\<^type_name>\<open>bool\<close>,[])]), 
walther@60373:     Type e(\<^type_name>\<open>una\<close>, [])])) = @{term "relations"};
Walther@60650: TermC.atom_typ @{context} (type_of t);
walther@59953: if Input_Descript.for_bool_list t then () else error "Input_Descript.for_bool_list changed";
walther@59953: "----- fun Input_Descript.for_real -----";
walther@59953: if not (Input_Descript.for_real t) then () else error "Input_Descript.for_real changed";
wneuper@59596: 
wneuper@59596: "----- fun is_list_dsc -----";
wneuper@59596: val t = @{term "someList"};
wneuper@59596: if is_list_dsc t then () else error "is_list_dsc changed 1";
wneuper@59596: 
wneuper@59596: val t = @{term "additionalRels [a=b,c=(d::real)]"};
wneuper@59596: if is_list_dsc t then () else error "is_list_dsc changed 2";
wneuper@59596: if is_list_dsc (head_of t) then () else error "is_list_dsc changed 3";
wneuper@59596: 
wneuper@59596: "----- fun is_list_dsc -----";
wneuper@59596: val t = @{term "maximum"};
walther@59953: if Input_Descript.is_a t then () else error "Input_Descript.is_a changed 1";
wneuper@59596: 
wneuper@59596: val t = head_of @{term "maximum A"};
walther@59953: if Input_Descript.is_a t then () else error "Input_Descript.is_a changed 2";
wneuper@59596: 
wneuper@59596: val t = head_of @{term "fixedValues [R=(R::real)]"};
walther@59953: if Input_Descript.is_a t then () else error "Input_Descript.is_a changed 3";
wneuper@59596: