| author | wenzelm |
| Mon, 21 Jun 2021 15:36:09 +0200 | |
| changeset 60309 | 70a1d102660d |
| parent 59959 | 0f0718c61f68 |
| child 60336 | dcb37736d573 |
| permissions | -rw-r--r-- |
| wneuper@59596 | 1 |
(* Title: "Specify/input-descript.sml" |
| wneuper@59596 | 2 |
Author: Walther Neuper 060605 |
| wneuper@59596 | 3 |
(c) due to copyright terms |
| wneuper@59596 | 4 |
*) |
| wneuper@59596 | 5 |
"----------------------------------------------------------------------------------------------"; |
| wneuper@59596 | 6 |
"table of contents ----------------------------------------------------------------------------"; |
| wneuper@59596 | 7 |
"----------------------------------------------------------------------------------------------"; |
| walther@59959 | 8 |
"-------- distinguish input to I_Model --------------------------------------------------------"; |
| wneuper@59596 | 9 |
"----------------------------------------------------------------------------------------------"; |
| wneuper@59596 | 10 |
"----------------------------------------------------------------------------------------------"; |
| wneuper@59596 | 11 |
"----------------------------------------------------------------------------------------------"; |
| wneuper@59596 | 12 |
|
| wneuper@59596 | 13 |
|
| walther@59959 | 14 |
"-------- distinguish input to I_Model --------------------------------------------------------"; |
| walther@59959 | 15 |
"-------- distinguish input to I_Model --------------------------------------------------------"; |
| walther@59959 | 16 |
"-------- distinguish input to I_Model --------------------------------------------------------"; |
| walther@59953 | 17 |
"----- fun Input_Descript.for_bool_list -----"; |
| wneuper@59596 | 18 |
val t as Const ("Input_Descript.relations",
|
| wenzelm@60309 | 19 |
Type (\<^type_name>\<open>fun\<close>, [Type (\<^type_name>\<open>list\<close>, [Type (\<^type_name>\<open>bool\<close>,[])]), |
| wneuper@59596 | 20 |
Type ("Input_Descript.una", [])])) = @{term "relations"};
|
| wneuper@59596 | 21 |
atomtyp (type_of t); |
| walther@59953 | 22 |
if Input_Descript.for_bool_list t then () else error "Input_Descript.for_bool_list changed"; |
| walther@59953 | 23 |
"----- fun Input_Descript.for_real -----"; |
| walther@59953 | 24 |
if not (Input_Descript.for_real t) then () else error "Input_Descript.for_real changed"; |
| wneuper@59596 | 25 |
|
| wneuper@59596 | 26 |
"----- fun is_list_dsc -----"; |
| wneuper@59596 | 27 |
val t = @{term "someList"};
|
| wneuper@59596 | 28 |
if is_list_dsc t then () else error "is_list_dsc changed 1"; |
| wneuper@59596 | 29 |
|
| wneuper@59596 | 30 |
val t = @{term "additionalRels [a=b,c=(d::real)]"};
|
| wneuper@59596 | 31 |
if is_list_dsc t then () else error "is_list_dsc changed 2"; |
| wneuper@59596 | 32 |
if is_list_dsc (head_of t) then () else error "is_list_dsc changed 3"; |
| wneuper@59596 | 33 |
|
| wneuper@59596 | 34 |
"----- fun is_list_dsc -----"; |
| wneuper@59596 | 35 |
val t = @{term "maximum"};
|
| walther@59953 | 36 |
if Input_Descript.is_a t then () else error "Input_Descript.is_a changed 1"; |
| wneuper@59596 | 37 |
|
| wneuper@59596 | 38 |
val t = head_of @{term "maximum A"};
|
| walther@59953 | 39 |
if Input_Descript.is_a t then () else error "Input_Descript.is_a changed 2"; |
| wneuper@59596 | 40 |
|
| wneuper@59596 | 41 |
val t = head_of @{term "fixedValues [R=(R::real)]"};
|
| walther@59953 | 42 |
if Input_Descript.is_a t then () else error "Input_Descript.is_a changed 3"; |
| wneuper@59596 | 43 |