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

   Author: Walther Neuper 060605

   (c) due to copyright terms

*)

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

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

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

"-------- distinguish input to Model ----------------------------------------------------------";

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

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

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

"-------- distinguish input to Model ----------------------------------------------------------";

"-------- distinguish input to Model ----------------------------------------------------------";

"-------- distinguish input to Model ----------------------------------------------------------";

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

val t as Const ("Input_Descript.relations", 

  Type ("fun", [Type ("List.list", [Type ("HOL.bool",[])]), 

    Type ("Input_Descript.una", [])])) = @{term "relations"};

atomtyp (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";