src/HOLCF/IOA/ABP/Check.ML
changeset 39733 6d373e9dcb9d
parent 36692 54b64d4ad524
equal deleted inserted replaced
39732:4dbc72759706 39733:6d373e9dcb9d
   110 (* ------------------------------------
   110 (* ------------------------------------
   111            Input / Output utilities 
   111            Input / Output utilities 
   112    ------------------------------------*)
   112    ------------------------------------*)
   113 
   113 
   114 fun print_list (lpar, rpar, pre: 'a -> unit) (lll : 'a list) =
   114 fun print_list (lpar, rpar, pre: 'a -> unit) (lll : 'a list) =
   115   let fun prec x = (Output.std_output ","; pre x)
   115   let fun prec x = (Output.raw_stdout ","; pre x)
   116   in
   116   in
   117     (case lll of
   117     (case lll of
   118       [] => (Output.std_output lpar; Output.std_output rpar)
   118       [] => (Output.raw_stdout lpar; Output.raw_stdout rpar)
   119     | x::lll => (Output.std_output lpar; pre x; List.app prec lll; Output.std_output rpar))
   119     | x::lll => (Output.raw_stdout lpar; pre x; List.app prec lll; Output.raw_stdout rpar))
   120    end;
   120    end;
   121 
   121 
   122 fun pr_bool true = Output.std_output "true"
   122 fun pr_bool true = Output.raw_stdout "true"
   123 |   pr_bool false = Output.std_output "false";
   123 |   pr_bool false = Output.raw_stdout "false";
   124 
   124 
   125 fun pr_msg m = Output.std_output "m"
   125 fun pr_msg m = Output.raw_stdout "m"
   126 |   pr_msg n = Output.std_output "n"
   126 |   pr_msg n = Output.raw_stdout "n"
   127 |   pr_msg l = Output.std_output "l";
   127 |   pr_msg l = Output.raw_stdout "l";
   128 
   128 
   129 fun pr_act a = Output.std_output (case a of
   129 fun pr_act a = Output.raw_stdout (case a of
   130       Next => "Next"|                         
   130       Next => "Next"|                         
   131       S_msg(ma) => "S_msg(ma)"  |
   131       S_msg(ma) => "S_msg(ma)"  |
   132       R_msg(ma) => "R_msg(ma)"  |
   132       R_msg(ma) => "R_msg(ma)"  |
   133       S_pkt(b,ma) => "S_pkt(b,ma)" |                    
   133       S_pkt(b,ma) => "S_pkt(b,ma)" |                    
   134       R_pkt(b,ma) => "R_pkt(b,ma)" |                    
   134       R_pkt(b,ma) => "R_pkt(b,ma)" |                    
   135       S_ack(b)   => "S_ack(b)" |                      
   135       S_ack(b)   => "S_ack(b)" |                      
   136       R_ack(b)   => "R_ack(b)");
   136       R_ack(b)   => "R_ack(b)");
   137 
   137 
   138 fun pr_pkt (b,ma) = (Output.std_output "<"; pr_bool b;Output.std_output ", "; pr_msg ma; Output.std_output ">");
   138 fun pr_pkt (b,ma) = (Output.raw_stdout "<"; pr_bool b;Output.raw_stdout ", "; pr_msg ma; Output.raw_stdout ">");
   139 
   139 
   140 val pr_bool_list  = print_list("[","]",pr_bool);
   140 val pr_bool_list  = print_list("[","]",pr_bool);
   141 val pr_msg_list   = print_list("[","]",pr_msg);
   141 val pr_msg_list   = print_list("[","]",pr_msg);
   142 val pr_pkt_list   = print_list("[","]",pr_pkt);
   142 val pr_pkt_list   = print_list("[","]",pr_pkt);
   143 
   143 
   144 fun pr_tuple (env,p,a,q,b,ch1,ch2) = 
   144 fun pr_tuple (env,p,a,q,b,ch1,ch2) = 
   145         (Output.std_output "{"; pr_bool env; Output.std_output ", "; pr_msg_list p;  Output.std_output ", ";
   145         (Output.raw_stdout "{"; pr_bool env; Output.raw_stdout ", "; pr_msg_list p;  Output.raw_stdout ", ";
   146          pr_bool a;  Output.std_output ", "; pr_msg_list q; Output.std_output ", ";
   146          pr_bool a;  Output.raw_stdout ", "; pr_msg_list q; Output.raw_stdout ", ";
   147          pr_bool b;  Output.std_output ", "; pr_pkt_list ch1;  Output.std_output ", ";
   147          pr_bool b;  Output.raw_stdout ", "; pr_pkt_list ch1;  Output.raw_stdout ", ";
   148          pr_bool_list ch2; Output.std_output "}");
   148          pr_bool_list ch2; Output.raw_stdout "}");
   149 
   149 
   150 
   150 
   151 
   151 
   152 (* ---------------------------------
   152 (* ---------------------------------
   153          Main function call
   153          Main function call