18 "--------- regr.test fun cpy_nam ------------------------"; |
18 "--------- regr.test fun cpy_nam ------------------------"; |
19 "--------- check specify phase --------------------------"; |
19 "--------- check specify phase --------------------------"; |
20 "--------- check: fmz matches pbt -----------------------"; |
20 "--------- check: fmz matches pbt -----------------------"; |
21 "--------- fun typeless ---------------------------------"; |
21 "--------- fun typeless ---------------------------------"; |
22 "--------- fun variants_in ------------------------------"; |
22 "--------- fun variants_in ------------------------------"; |
23 "--------- fun is_list_type -----------------------------"; |
|
24 "--------- fun has_list_type ----------------------------"; |
23 "--------- fun has_list_type ----------------------------"; |
25 "--------- fun tag_form ---------------------------------"; |
24 "--------- fun tag_form ---------------------------------"; |
26 "--------- fun foldr1, foldl1 ---------------------------"; |
25 "--------- fun foldr1, foldl1 ---------------------------"; |
27 "--------------------------------------------------------"; |
26 "--------------------------------------------------------"; |
28 "--------------------------------------------------------"; |
27 "--------------------------------------------------------"; |
885 > cnt (op=) [2,2,2,4,5,5,5,5,5] 2 0; |
884 > cnt (op=) [2,2,2,4,5,5,5,5,5] 2 0; |
886 val it = ([3],[4,5,5,5,5,5]) : int list * int list |
885 val it = ([3],[4,5,5,5,5,5]) : int list * int list |
887 > coll (op=) [] [1,2,2,2,4,5,5,5,5,5]; |
886 > coll (op=) [] [1,2,2,2,4,5,5,5,5,5]; |
888 val it = [1,3,1,5] : int list |
887 val it = [1,3,1,5] : int list |
889 *) |
888 *) |
890 "--------- fun is_list_type -----------------------------"; |
|
891 "--------- fun is_list_type -----------------------------"; |
|
892 "--------- fun is_list_type -----------------------------"; |
|
893 (* fun destr (Type(str,sort)) = (str,sort); |
|
894 > val (SOME ct) = parse thy "lll::real list"; |
|
895 > val ty = (#T o rep_cterm) ct; |
|
896 > is_list_type ty; |
|
897 val it = true : bool |
|
898 > destr ty; |
|
899 val it = ("List.list",["RealDef.real"]) : string * typ list |
|
900 > atomty ((#t o rep_cterm) ct); |
|
901 *** ------------- |
|
902 *** Free ( lll, real list) |
|
903 val it = () : unit |
|
904 |
|
905 > val (SOME ct) = parse thy "[lll::real]"; |
|
906 > val ty = (#T o rep_cterm) ct; |
|
907 > is_list_type ty; |
|
908 val it = true : bool |
|
909 > destr ty; |
|
910 val it = ("List.list",["'a"]) : string * typ list |
|
911 > atomty ((#t o rep_cterm) ct); |
|
912 *** ------------- |
|
913 *** Const ( List.list.Cons, [real, real list] => real list) |
|
914 *** Free ( lll, real) |
|
915 *** Const ( List.list.Nil, real list) |
|
916 |
|
917 > val (SOME ct) = parse thy "lll"; |
|
918 > val ty = (#T o rep_cterm) ct; |
|
919 > is_list_type ty; |
|
920 val it = false : bool *) |
|
921 "--------- fun has_list_type ----------------------------"; |
|
922 "--------- fun has_list_type ----------------------------"; |
|
923 "--------- fun has_list_type ----------------------------"; |
|
924 (* |
|
925 > val (SOME ct) = parse thy "lll::real list"; |
|
926 > has_list_type (Thm.term_of ct); |
|
927 val it = true : bool |
|
928 > val (SOME ct) = parse thy "[lll::real]"; |
|
929 > has_list_type (Thm.term_of ct); |
|
930 val it = false : bool *) |
|
931 "--------- fun tag_form ---------------------------------"; |
889 "--------- fun tag_form ---------------------------------"; |
932 "--------- fun tag_form ---------------------------------"; |
890 "--------- fun tag_form ---------------------------------"; |
933 "--------- fun tag_form ---------------------------------"; |
891 "--------- fun tag_form ---------------------------------"; |
934 (* val formal = (the o (parse thy)) "[R::real]"; |
892 (* val formal = (the o (parse thy)) "[R::real]"; |
935 > val given = (the o (parse thy)) "fixed_values (cs::real list)"; |
893 > val given = (the o (parse thy)) "fixed_values (cs::real list)"; |