1 (* Title: "Specify/input-descript.sml"
2 Author: Walther Neuper 060605
3 (c) due to copyright terms
5 "----------------------------------------------------------------------------------------------";
6 "table of contents ----------------------------------------------------------------------------";
7 "----------------------------------------------------------------------------------------------";
8 "-------- distinguish input to I_Model --------------------------------------------------------";
9 "----------------------------------------------------------------------------------------------";
10 "----------------------------------------------------------------------------------------------";
11 "----------------------------------------------------------------------------------------------";
14 "-------- distinguish input to I_Model --------------------------------------------------------";
15 "-------- distinguish input to I_Model --------------------------------------------------------";
16 "-------- distinguish input to I_Model --------------------------------------------------------";
17 "----- fun Input_Descript.for_bool_list -----";
18 val t as Const (\<^const_name>\<open>Input_Descript.relations\<close>,
19 Type (\<^type_name>\<open>fun\<close>, [Type (\<^type_name>\<open>list\<close>, [Type (\<^type_name>\<open>bool\<close>,[])]),
20 Type e(\<^type_name>\<open>una\<close>, [])])) = @{term "relations"};
22 if Input_Descript.for_bool_list t then () else error "Input_Descript.for_bool_list changed";
23 "----- fun Input_Descript.for_real -----";
24 if not (Input_Descript.for_real t) then () else error "Input_Descript.for_real changed";
26 "----- fun is_list_dsc -----";
27 val t = @{term "someList"};
28 if is_list_dsc t then () else error "is_list_dsc changed 1";
30 val t = @{term "additionalRels [a=b,c=(d::real)]"};
31 if is_list_dsc t then () else error "is_list_dsc changed 2";
32 if is_list_dsc (head_of t) then () else error "is_list_dsc changed 3";
34 "----- fun is_list_dsc -----";
35 val t = @{term "maximum"};
36 if Input_Descript.is_a t then () else error "Input_Descript.is_a changed 1";
38 val t = head_of @{term "maximum A"};
39 if Input_Descript.is_a t then () else error "Input_Descript.is_a changed 2";
41 val t = head_of @{term "fixedValues [R=(R::real)]"};
42 if Input_Descript.is_a t then () else error "Input_Descript.is_a changed 3";