1.1 --- a/test/Tools/isac/Interpret/calchead.sml	Wed Nov 30 13:05:08 2016 +0100
     1.2 +++ b/test/Tools/isac/Interpret/calchead.sml	Mon Dec 12 18:08:13 2016 +0100
     1.3 @@ -18,6 +18,12 @@
     1.4  "--------- regr.test fun cpy_nam ------------------------";
     1.5  "--------- check specify phase --------------------------";
     1.6  "--------- check: fmz matches pbt -----------------------";
     1.7 +"--------- fun typeless ---------------------------------";
     1.8 +"--------- fun variants_in ------------------------------";
     1.9 +"--------- fun is_list_type -----------------------------";
    1.10 +"--------- fun has_list_type ----------------------------";
    1.11 +"--------- fun tag_form ---------------------------------";
    1.12 +"--------- fun foldr1, foldl1 ---------------------------";
    1.13  "--------------------------------------------------------";
    1.14  "--------------------------------------------------------";
    1.15  "--------------------------------------------------------";
    1.16 @@ -861,3 +867,89 @@
    1.17  val [("#Given", (Const ("Simplify.Term", _), Free ("t_t", _))),
    1.18       ("#Find", (Const ("Simplify.normalform", _), Free ("n_n", _)))] = (#ppc o get_pbt) pI;
    1.19  
    1.20 +"--------- fun typeless ---------------------------------";
    1.21 +"--------- fun typeless ---------------------------------";
    1.22 +"--------- fun typeless ---------------------------------";
    1.23 +(*
    1.24 +> val (SOME ct) = parse thy "max_relation (A=#2*a*b - a^^^#2)";
    1.25 +> val (_,t1) = split_dsc_t hs (Thm.term_of ct);
    1.26 +> val (SOME ct) = parse thy "A=#2*a*b - a^^^#2";
    1.27 +> val (_,t2) = split_dsc_t hs (Thm.term_of ct);
    1.28 +> typeless t1 = typeless t2;
    1.29 +val it = true : bool
    1.30 +*)
    1.31 +"--------- fun variants_in ------------------------------";
    1.32 +"--------- fun variants_in ------------------------------";
    1.33 +"--------- fun variants_in ------------------------------";
    1.34 +(*
    1.35 +> cnt (op=) [2,2,2,4,5,5,5,5,5] 2 0;
    1.36 +val it = ([3],[4,5,5,5,5,5]) : int list * int list
    1.37 +> coll (op=) [] [1,2,2,2,4,5,5,5,5,5];
    1.38 +val it = [1,3,1,5] : int list
    1.39 +*)
    1.40 +"--------- fun is_list_type -----------------------------";
    1.41 +"--------- fun is_list_type -----------------------------";
    1.42 +"--------- fun is_list_type -----------------------------";
    1.43 +(* fun destr (Type(str,sort)) = (str,sort);
    1.44 +> val (SOME ct) = parse thy "lll::real list";
    1.45 +> val ty = (#T o rep_cterm) ct;
    1.46 +> is_list_type ty;
    1.47 +val it = true : bool 
    1.48 +> destr ty;
    1.49 +val it = ("List.list",["RealDef.real"]) : string * typ list
    1.50 +> atomty ((#t o rep_cterm) ct);
    1.51 +*** -------------
    1.52 +*** Free ( lll, real list)
    1.53 +val it = () : unit
    1.54 + 
    1.55 +> val (SOME ct) = parse thy "[lll::real]";
    1.56 +> val ty = (#T o rep_cterm) ct;
    1.57 +> is_list_type ty;
    1.58 +val it = true : bool 
    1.59 +> destr ty;
    1.60 +val it = ("List.list",["'a"]) : string * typ list
    1.61 +> atomty ((#t o rep_cterm) ct);
    1.62 +*** -------------
    1.63 +*** Const ( List.list.Cons, [real, real list] => real list)
    1.64 +***   Free ( lll, real)
    1.65 +***   Const ( List.list.Nil, real list) 
    1.66 +
    1.67 +> val (SOME ct) = parse thy "lll";
    1.68 +> val ty = (#T o rep_cterm) ct;
    1.69 +> is_list_type ty;
    1.70 +val it = false : bool  *)
    1.71 +"--------- fun has_list_type ----------------------------";
    1.72 +"--------- fun has_list_type ----------------------------";
    1.73 +"--------- fun has_list_type ----------------------------";
    1.74 +(*
    1.75 +> val (SOME ct) = parse thy "lll::real list";
    1.76 +> has_list_type (Thm.term_of ct);
    1.77 +val it = true : bool
    1.78 +> val (SOME ct) = parse thy "[lll::real]";
    1.79 +> has_list_type (Thm.term_of ct);
    1.80 +val it = false : bool *)
    1.81 +"--------- fun tag_form ---------------------------------";
    1.82 +"--------- fun tag_form ---------------------------------";
    1.83 +"--------- fun tag_form ---------------------------------";
    1.84 +(* val formal = (the o (parse thy)) "[R::real]";
    1.85 +> val given = (the o (parse thy)) "fixed_values (cs::real list)";
    1.86 +> tag_form thy (formal, given);
    1.87 +val it = "fixed_values [R]" : cterm
    1.88 +*)
    1.89 +"--------- fun foldr1, foldl1 ---------------------------";
    1.90 +"--------- fun foldr1, foldl1 ---------------------------";
    1.91 +"--------- fun foldr1, foldl1 ---------------------------";
    1.92 +(*
    1.93 +> val (SOME ct) = parse thy "[a=b,c=d,e=f]";
    1.94 +> val ces = map (Thm.global_cterm_of thy) (isalist2list (Thm.term_of ct));
    1.95 +> val conj = foldr1 HOLogic.mk_conj (isalist2list (Thm.term_of ct));
    1.96 +> Thm.global_cterm_of thy conj;
    1.97 +val it = "(a = b & c = d) & e = f" : cterm
    1.98 +*)
    1.99 +(*
   1.100 +> val (SOME ct) = parse thy "[a=b,c=d,e=f,g=h]";
   1.101 +> val ces = map (Thm.global_cterm_of thy) (isalist2list (Thm.term_of ct));
   1.102 +> val conj = foldl1 HOLogic.mk_conj (isalist2list (Thm.term_of ct));
   1.103 +> Thm.global_cterm_of thy conj;
   1.104 +val it = "a = b & c = d & e = f & g = h" : cterm
   1.105 +*)