1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/test/Tools/isac/Specify/input-descript.sml	Tue Aug 27 15:32:38 2019 +0200
     1.3 @@ -0,0 +1,43 @@
     1.4 +(* Title: "Specify/input-descript.sml"
     1.5 +   Author: Walther Neuper 060605
     1.6 +   (c) due to copyright terms
     1.7 +*)
     1.8 +"----------------------------------------------------------------------------------------------";
     1.9 +"table of contents ----------------------------------------------------------------------------";
    1.10 +"----------------------------------------------------------------------------------------------";
    1.11 +"-------- distinguish input to Model ----------------------------------------------------------";
    1.12 +"----------------------------------------------------------------------------------------------";
    1.13 +"----------------------------------------------------------------------------------------------";
    1.14 +"----------------------------------------------------------------------------------------------";
    1.15 +
    1.16 +
    1.17 +"-------- distinguish input to Model ----------------------------------------------------------";
    1.18 +"-------- distinguish input to Model ----------------------------------------------------------";
    1.19 +"-------- distinguish input to Model ----------------------------------------------------------";
    1.20 +"----- fun is_booll_dsc -----";
    1.21 +val t as Const ("Input_Descript.relations", 
    1.22 +  Type ("fun", [Type ("List.list", [Type ("HOL.bool",[])]), 
    1.23 +    Type ("Input_Descript.una", [])])) = @{term "relations"};
    1.24 +atomtyp (type_of t);
    1.25 +if is_booll_dsc t then () else error "is_booll_dsc changed";
    1.26 +"----- fun is_reall_dsc -----";
    1.27 +if not (is_reall_dsc t) then () else error "is_reall_dsc changed";
    1.28 +
    1.29 +"----- fun is_list_dsc -----";
    1.30 +val t = @{term "someList"};
    1.31 +if is_list_dsc t then () else error "is_list_dsc changed 1";
    1.32 +
    1.33 +val t = @{term "additionalRels [a=b,c=(d::real)]"};
    1.34 +if is_list_dsc t then () else error "is_list_dsc changed 2";
    1.35 +if is_list_dsc (head_of t) then () else error "is_list_dsc changed 3";
    1.36 +
    1.37 +"----- fun is_list_dsc -----";
    1.38 +val t = @{term "maximum"};
    1.39 +if is_dsc t then () else error "is_dsc changed 1";
    1.40 +
    1.41 +val t = head_of @{term "maximum A"};
    1.42 +if is_dsc t then () else error "is_dsc changed 2";
    1.43 +
    1.44 +val t = head_of @{term "fixedValues [R=(R::real)]"};
    1.45 +if is_dsc t then () else error "is_dsc changed 3";
    1.46 +