[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

no subject (file transmission)



program Adl_int is
use Adl;
import add(_, _, _) from func;
import diff(_, _), write(_), writeln(_), 
       abort(), fail() from prolog;
import eval_op(BOP, VALUES, VALUES -> VALUES),
       eval_uop(UN_OP,VALUES -> VALUES),
       append_varenv(VARENV,VARENV -> VARENV) from Adl_aux1;
import make_closure(VARENV,FUNENV |- PATTERN, EXP -> CLOSURE),
       convert_pattern(|- PATTERN -> VARENV, EXP) from Adl_clos;
import handle_scan(VARENV, FUNENV |- ID, EXP_LIST, EXP_LIST, EXP_LIST, INT, 
       INT, INT, TRAREC_LIST, INT => EXP_LIST, TRAREC_LIST, INT), 
       strip(|- EXP -> EXP),
       no_of_elems(|- EXP_LIST, INT => INT),
       step_no(|- INT, INT => EXP_LIST),
       two_power_of(|- EXP_LIST, EXP_LIST => EXP_LIST),
       look_for_partner(|- EXP_LIST, INT => EXP),
       copy_first_few(|- EXP_LIST, EXP_LIST, INT => EXP_LIST),
       handle_pairwise( VARENV, FUNENV |- ID, EXP_LIST, EXP_LIST, INT, 
                        TRAREC_LIST, INT => VALUES, TRAREC_LIST, INT)
       from Adl_parll;      

judgement |- EXP = VALUES;

eval_expr(varenv[], funenv[] |- E, number 0, trarec_list[], number 0 => 
                                                      V, PROC, TRL, STOP_T) &
stop_tracing(TRL, STOP_T |- TRL') &
spew_trarec_list(TRL')
----------------
|- E = V ;

   set eval_expr is
   judgement VARENV, FUNENV |- EXP, INT, TRAREC_LIST, INT => 
                               VALUES, INT, TRAREC_LIST, INT ;
   judgement VARENV, FUNENV |- DECLS, INT, TRAREC_LIST, INT : VARENV, FUNENV,
                                             INT, TRAREC_LIST, INT;
   
   ve, fe |- number N, PROC, TRL, START_T => number N, PROC, TRL, START_T ;
   
   ve, fe |- realn N, PROC, TRL, START_T => realn N, PROC, TRL, START_T ;

   ve, fe |- boolean(true()), PROC, TRL, START_T => boolean(true()), PROC,
                                                    TRL, START_T ;

   ve, fe |- boolean(false()), PROC, TRL, START_T => boolean(false()), PROC,
                                                     TRL, START_T ;

   get_value(ve |- id X -> V) &
   start_proc(TRL, PROC, START_T |- TRL') &
   eval_op(plus(), START_T, number 5 -> STOP_T) &
   stop_proc(TRL', PROC, STOP_T |- TRL'') 
   ----------------
   ve, fe |- id X, PROC, TRL, START_T => V, PROC, TRL'', STOP_T ;


   ve, fe |- Y, PROC, TRL, START_T => V, PROC', TRL', STOP_T  & 
   start_proc(TRL', PROC, STOP_T |- TRL'') & 
   -- I don't use PROC' because the update of X with the value Y
   -- must strictly follow the evaluation of Y. So I use STOP_T as
   -- the starting time but the same original processor.  
   update_varenv(ve |- X, V -> ve') &
   eval_op(plus(), STOP_T, number 5 -> STOP_T') &
   stop_proc(TRL'', PROC, STOP_T' |- TRL''') 
   ----------------
   ve, fe |- decls[var_dec(X, Y)], PROC, TRL, START_T :
              ve', fe, PROC, TRL''', STOP_T' ;
   -- check that with these 4 decls rules PROC is indeed the correct thing 
   -- to return
   

   ve, fe |- Y, PROC, TRL, START_T => V, PROC', TRL', STOP_T &
   start_proc(TRL', PROC, STOP_T |- TRL'') &
   -- same reason as rule above
   update_varenv(ve |- X, V -> ve') &
   eval_op(plus(), STOP_T, number 5 -> STOP_T') &
   stop_proc(TRL'', PROC, STOP_T' |- TRL''') &
   ve', fe |- ds, PROC, TRL''',STOP_T' : ve'', fe'', PROC'',TRL'''', 
                                          STOP_T''
   ----------------
   ve, fe |- decls[var_dec(X, Y).ds], PROC, TRL, START_T : 
              ve'', fe'', PROC, TRL'''', STOP_T'' ;


   make_closure(ve, fe |- PAT, E -> CL) &
   start_proc(TRL, PROC, START_T |- TRL') &
   update_funenv(fe |- X, CL -> fe') &
   eval_op(plus(), START_T, number 5 -> STOP_T) &
   stop_proc(TRL', PROC, STOP_T |- TRL'') 
   ----------------
   ve, fe |- decls[fun_dec(X, PAT, E)], PROC, TRL, START_T :
              ve, fe', PROC, TRL'', STOP_T ;


   make_closure(ve, fe |- PAT, E -> CL) &
   start_proc(TRL, PROC, START_T |- TRL') &
   -- same reason as rule above
   update_funenv(fe |- X, CL -> fe') &
   eval_op(plus(), START_T, number 5 -> STOP_T) &
   stop_proc(TRL', PROC, STOP_T |- TRL'') &
   ve, fe' |- ds, PROC, TRL'', STOP_T : ve', fe'', PROC', TRL''', STOP_T'
   ----------------
   ve, fe |- decls[fun_dec(X, PAT, E).ds], PROC, TRL, START_T :
              ve', fe'', PROC, TRL''', STOP_T' ;

   set_up_env(ve, fe |- F, A, PROC, TRL, START_T -> ve', PROC', TRL', STOP_T) &

   report_app(F) &

   ve', FE |- E, PROC, TRL', STOP_T => V, PROC'', TRL'', STOP_T' &

   eval_op(gt(), PROC', PROC'' -> PROC''')
   ------------------------
   ve, fe |- fun_app(F, A), PROC, TRL, START_T => V, PROC''', TRL'', STOP_T' ;



   ve, fe |- A, PROC, TRL, START_T => AV, PROC', TRL', STOP_T_A &
   ve, fe |- B, PROC', TRL', START_T => BV, PROC'', TRL'', STOP_T_B &
                          -- you can evaluate A and B in parallel, can't you?
   eval_op(gt(), STOP_T_A, STOP_T_B -> STOP_T) &
   eval_op(OP, AV, BV -> V) & -- may let computation time be determined by
                              -- what OP is later on but for now...
   eval_op(plus(), STOP_T, number 10 -> STOP_T') &
   eval_op(gt(), PROC', PROC'' -> MAX_PROC)
   ----------------
   ve, fe |- primop(OP, A, B), PROC, TRL, START_T => V, MAX_PROC, TRL'',
                                                      STOP_T' ;


   ve, fe |- A, PROC, TRL, START_T => AV, PROC', TRL', STOP_T &
   eval_uop(U,AV -> V) & -- may let computation time be determined by
                         -- what OP is later on but for now...
   eval_op(plus(), STOP_T, number 10 -> STOP_T') 
   ----------------
   ve, fe |- uop(U, A), PROC, TRL, START_T => V, PROC', TRL', STOP_T' ;


   ve, fe |- P, PROC, TRL, START_T => B, PROC', TRL', STOP_T &
   choose_alternative(ve, fe |- B,C,A, PROC, TRL', STOP_T  -> V, PROC'', 
                                                           TRL'', STOP_T')
   ----------------
   ve, fe |- if(P, C, A), PROC, TRL, START_T => V, PROC'', TRL'', STOP_T' ;
   

   -- this form of "if" expression isn't as nice as the ordinary form
   -- as shown in G.Khans natural semantics article but it doesn't 
   -- introduce any backtracking which can be a problem when recovery 
   -- rules are in place.

    
   ve, fe |- D, PROC, TRL, START_T : ve', fe', PROC', TRL', STOP_T &
   ve', fe' |- E, PROC', TRL', STOP_T => V, PROC'', TRL'', STOP_T'
   ----------------
   ve, fe |- let(D, E), PROC, TRL, START_T => V, PROC'', TRL'', STOP_T' ;



   ve, fe |- E, PROC, TRL, START_T => X, MAX_PROC, TRL', STOP_T &
   ve, fe |- vector(EL), PROC, TRL', STOP_T => vector(XL), MAX_PROC', 
                                                TRL'', STOP_T' &
   eval_op(gt(), MAX_PROC, MAX_PROC' -> MAX_PROC'')
   ----------------
   ve, fe |- vector(exp_list[E.EL]), PROC, TRL, START_T => 
              vector(exp_list[X.XL]), MAX_PROC'', TRL'', STOP_T' ; 



   ve, fe |- vector(exp_list[]), PROC, TRL, START_T => 
              vector(exp_list[]), PROC, TRL, START_T ;


   -- should the evaluation of things in a tuple be done in parallel?

   ve, fe |- X, PROC, TRL, START_T => V, PROC', TRL', STOP_T &
   ve, fe |- XS, PROC, TRL', STOP_T => VS, PROC'', TRL'', STOP_T' &
   eval_op(gt(), PROC', PROC'' -> MAX_PROC) 
   -------------------------------
   ve, fe |- tuple[X.XS], PROC, TRL, START_T => tuple[V.VS], MAX_PROC, TRL'',
                                                STOP_T' ;


   ve, fe |- tuple[], PROC, TRL, START_T => tuple[], PROC, TRL, START_T ; 

         -- we really shouldn't have empty tuples
         -- I'm just being lazy, I'll fix it later.


   dc_test_div(ve, fe |- A, C, EX, PROC, TRL, START_T -> tuple[L,R], 
                                     PROC', TRL', STOP_T) &
   eval_op(plus(), PROC, number 1 -> PROC_L) &
   dist_sub_prob(ve, fe |- dc(A, B, C, D, L), PROC_L, TRL', STOP_T -> VL, 
                                              PROC_L', TRL_L', STOP_T_L' ) & 
   eval_op(plus(), PROC_L', number 1 -> PROC_R) &
   dist_sub_prob(ve, fe |- dc(A, B, C, D, R), PROC_R, TRL_L', STOP_T -> VR, 
                                              PROC_R', TRL_R', STOP_T_R' ) &
   eval_op(gt(), STOP_T_L', STOP_T_R' -> STOP_T') &
   ve, fe |- fun_app(B, tuple[VL,VR]), PROC, TRL_R', STOP_T' => V'', 
               PROC'', TRL_F, STOP_T_F &
   max_proc_4(PROC', PROC'', PROC_L', PROC_R' -> MAX_PROC) 
   ----------------
   ve, fe |- dc(A, B, C, D, EX), PROC, TRL, START_T => V'', MAX_PROC,
                                                      TRL_F, STOP_T_F ;

   
   ve, fe |- EX, PROC, TRL, START_T => V, PROC', TRL', STOP_T &
   ve, fe |- fun_app(C, V), PROC, TRL', STOP_T => boolean(true()), PROC'', 
                                                  TRL'', STOP_T' &
   ve, fe |- fun_app(D, V), PROC, TRL'', STOP_T'  => V', PROC''', TRL''',
                                                      STOP_T'' &
   eval_op(gt(), PROC', PROC'' -> PROC_MAX) &
   eval_op(gt(), PROC_MAX, PROC''' -> PROC_MAX') 
   ----------------
   ve, fe |- dc(A, B, C, D, EX), PROC, TRL, START_T => V', PROC_MAX', TRL''', 
                                                       STOP_T'' ;



   eval_op(plus(), PROC, number 1 -> PROC') &
   -- every new element that we come across requires a new processor

   start_proc(TRL, PROC', START_T |- TRL') &

   ve, fe |- fun_app(F, E), PROC', TRL', START_T => X, PROC'', TRL'', STOP_T &

   stop_proc(TRL'', PROC', STOP_T |- TRL''') &

   ve, fe |- map(F, vector(EL)), PROC', TRL''', START_T => 
              vector(XL), PROC''', TRL'''', STOP_T' &
    
   eval_op(gt(), STOP_T, STOP_T' -> STOP_T'')
   ----------------
   ve, fe |- map(F, vector(exp_list[E.EL])), PROC, TRL, START_T => 
              vector(exp_list[X.XL]), PROC''', TRL'''', STOP_T' ;


   ve, fe |- map(F, vector(exp_list[])), PROC, TRL, START_T =>
              vector(exp_list[]), PROC, TRL, START_T ;


   ve, fe |- VEC => vector(LS) & 
   eval_op(plus(), PROC, number 1 -> PROC') &
   handle_pairwise(ve, fe |- F, exp_list[A.LS], exp_list[], PROC`, PROC',
                   TRL, START_T, number 0 => V', MAX_PROC, TRL', STOP_T) 
   ----------------
   ve, fe |- reduce(F, A, VEC), PROC, TRL, START_T => V', MAX_PROC, TRL', 
                                                      STOP_T ;


   ve, fe |- VEC => vector(LS) &
   no_of_elems(|- exp_list[A.LS], number 0 => N) &
   step_no(N, number 1 => SL) &
   two_power_of(|- SL, exp_list[] => STRL) &
   eval_op(plus(), PROC, number 1 -> PROC') &
   handle_scan(ve, fe |- F, exp_list[A.LS], exp_list[A], STRL, number 1, 
   N, PROC', TRL, START_T => exp_list[E.LS'], MAX_PROC, TRL', STOP_T)
   ----------------
   ve, fe |- scan(F, A, VEC), PROC, TRL, START_T => vector(LS'), MAX_PROC, 
                                                    TRL', STOP_T ;


   ve, fe |- E, PROC, TRL, START_T => number N, PROC', TRL', STOP_T & 
   make_exp_list(|- number 0, number N -> V) &
   -- doing one big plus saves time, so I'll do it this way
   eval_op(times(), number N, number 10 -> number TIME_INC) &
   eval_op(plus(), STOP_T, number TIME_INC -> STOP_T')
   ----------------
   ve, fe |- iota(E), PROC, TRL, START_T => vector(V), PROC', TRL', STOP_T' ;


   ve, fe |- fun_app(C,A), PROC, TRL, START_T => boolean(true()), PROC',  
                                                 TRL', STOP_T &
   ve, fe |- fun_app(F,A), PROC, TRL', STOP_T => A', PROC'', TRL'', STOP_T' &
   ve, fe |- while(F,C,A'), PROC, TRL'', STOP_T' => V, PROC''', TRL''', 
                                                    STOP_T'' &
   eval_op(gt(), PROC', PROC'' -> MAX_PROC) &
   eval_op(gt(), MAX_PROC, PROC''' -> MAX_PROC')
   --------------------------
   ve, fe |- while(F,C,A), PROC, TRL, START_T => V, MAX_PROC', TRL''',
                                                 STOP_T'' ;


   ve, fe |- fun_app(C,A), PROC, TRL, START_T => boolean(false()), PROC', 
                                                 TRL', STOP_T 
   --------------------------
   ve, fe |- while(F,C,A), PROC, TRL, START_T => A, PROC', TRL', STOP_T ;

   end eval_expr;

   set get_value is
   judgement VARENV |- ID -> VALUES;

   varenv[varbind(X, V).BS] |- X -> V ;

   BS |- Y -> V'
   ----------------
   varenv[varbind(X, V).BS] |- Y -> V' ;
            provided diff(X, Y);

   end get_value;

   set make_lambda is
   judgement |- IDLIST, EXP -> EXP;

   |- IDL, EX -> lambda(IDL, EX) ;
   end make_lambda;

   set update_varenv is
   judgement VARENV |- ID, VALUES -> VARENV;

   VE |- X, V -> varenv[varbind(X, V).VE] ;
   end update_varenv;

   set update_funenv is
   judgement FUNENV |- ID, CLOSURE -> FUNENV;

   FE |- X, C -> funenv[funbind(X, C).FE] ;
      do write("The declaration of: ") &
         writeln(X);

   end update_funenv;

   set eval_list is
   judgement VARENV, FUNENV |- EXP_LIST -> EXP_LIST;

   eval_expr(VE, FE |- E => V')  &  
   VE, FE |- L -> L'
   ----------------
   VE, FE |- exp_list[E.L] -> exp_list[V'.L'];

   VE, FE |- exp_list[] -> exp_list[];
   
   end eval_list;

   set get_func is
   judgement FUNENV |- ID -> CLOSURE;

   funenv[funbind(X, CL).FS] |- X -> CL ;

   FS |- Y -> CL
   ----------------
   funenv[funbind(X, CL').FS] |- Y -> CL ;
            provided diff(X, Y);
   recovery
     _ |- Y -> _;
     do write("function: ") &
        write(Y) &
        writeln(" not found") & abort();   
   end get_func;

   set unify is
   judgement (EXP,EXP);

   (A,A);   
    
   end unify;


   set start_proc is
   judgement TRAREC_LIST, INT, INT |- TRAREC_LIST;
   TRL, PROC, START_T |- trarec_list[trarec(number 4, number 0, START_T, PROC, 
                             PROC, number 0 ,number 0).TRL]; 

   end start_proc;


   set stop_proc is
   judgement TRAREC_LIST, INT, INT |- TRAREC_LIST;

   TRL, PROC, STOP_T |- trarec_list[trarec(number 7, number 0, STOP_T, PROC, 
                                   number 0, number 0, number 0).TRL];

   end stop_proc;
   

   set stop_tracing is
   judgement TRAREC_LIST, INT |- TRAREC_LIST;

   
   TRL, STOP_T |- trarec_list[trarec(number 19, number 0, STOP_T, number 0, 
                                     number 0, number 0, number 0).TRL];
   end stop_tracing;

   set spew_trarec_list is
     judgement (TRAREC_LIST);
     (trarec_list[]);

     spew_trarec(TR) &
     spew_trarec_list(TRL)
     --------------------
     (trarec_list[TR.TRL]) ;
     
   end spew_trarec_list;

 
   set spew_trarec is
   judgement (TRAREC);
   
   (trarec(A,B,C,D,E,F,G));

   do write(A) & write(" ") &
      write(B) & write(" ") &
      write(C) & write(" ") &
      write(D) & write(" ") &
      write(E) & write(" ") &
      write(F) & write(" ") &
      writeln(G);  
    
   end spew_trarec;


   set report_app is
   judgement (ID);
    
   (X);
     do write("Application of: ") &
        writeln(X);
   end report_app;


   set choose_alternative is
   judgement VARENV, FUNENV |- VALUES, EXP, EXP, INT, TRAREC_LIST, INT -> 
                                    VALUES, INT, TRAREC_LIST, INT;

   eval_expr(VE, FE |- C, PROC, TRL, START_T => V, PROC', TRL', STOP_T)
   -------------------------------
   VE,FE |- boolean(true()), C, A, PROC, TRL, START_T -> V, PROC', TRL', 
                                                         STOP_T ;

   eval_expr(VE, FE |- A, PROC, TRL, START_T => V, PROC', TRL', STOP_T)
   --------------------------------
   VE,FE |- boolean(false()), C, A, PROC, TRL, START_T -> V, PROC', TRL', 
                                                          STOP_T ;
   
   end choose_alternative;


   set make_exp_list is
   judgement |- EXP, EXP -> EXP_LIST ;

   add(C, 1, C')  &  |- number C', number N -> CL'
   ----------------
   |- number C, number N -> exp_list[number C.CL'] ;
            provided diff(C, N);

   |- number N, number N -> exp_list[] ;
   end make_exp_list;


   set max_proc_4 is
   judgement INT, INT, INT, INT |- INT;

   eval_op(gt(), PROC1, PROC2 -> MAX_PROC) &
   eval_op(gt(), PROC3, PROC4 -> MAX_PROC') &
   eval_op(gt(), MAX_PROC, MAX_PROC' -> MAX_PROC'') 
   -------------------------------
   PROC1, PROC2, PROC3, PROC4 |- MAX_PROC'' ;

   end max_proc_4;


   set set_up_env is
   judgement VARENV, FUNENV |- EXP, EXP, INT, TRAREC_LIST, INT -> VARENV,
                                                    INT, TRAREC_LIST, INT;
  
   get_func(fe |- F -> closure(PAT, E, FE,VE)) &
                                   -- if F looks like f(a,b) := ...

   convert_pattern(|- PAT -> VF, UT) &
                           -- then PAT is a,b                            
                           -- VF is varenv[varbind(a,A),varbind(b,B)]
                           -- UT is A, B        
                           -- when A and B are unified with something
                           -- the varenv will automatically be updated 
  
   eval_op(plus(), START_T, number 10 -> ST_INC) &   
   -- to model the time taken to set up the base of the run-time stack 
   
   ve, fe |- A, PROC, TRL, ST_INC => VL, PROC', TRL', STOP_T &

   unify(UT, VL) &

   append_varenv(VF, VE -> ve')
   ------------------------------
   ve, fe |- F, A, PROC, TRL, START_T -> ve', PROC', TRL', STOP_T ; 
  


   end set_up_env;

   set dc_test_div is
   judgement VARENV, FUNENV |- ID, ID, EXP, INT, TRAREC_LIST, INT -> 
                                       VALUES, INT, TRAREC_LIST, INT;

   ve, fe |- EX, PROC, TRL, START_T => V, PROC', TRL', STOP_T &
   ve, fe |- fun_app(C, V), PROC, TRL', STOP_T => boolean(false()), PROC'',
                                                   TRL'', STOP_T' &
   ve, fe |- fun_app(A,V), PROC, TRL'', STOP_T' => tuple[L,R], PROC''', 
                                                    TRL''', STOP_T'' &
   eval_op(gt(), PROC', PROC'' -> MAX_PROC) &
   eval_op(gt(), MAX_PROC, PROC''' -> MAX_PROC')
   ---------------------------------
   ve, fe |- A, C, EX, PROC, TRL, START_T -> tuple[L,R], MAX_PROC', TRL''',
                                             STOP_T'' ;  

   end dc_test_div;

  
   set dist_sub_prob is
   judgement VARENV, FUNENV |- EXP, INT, TRAREC_LIST, INT -> VALUES, INT, 
                                                            TRAREC_LIST, INT;
   
   start_proc(TRL, PROC, START_T -> TRL') & 
   eval_expr(ve, fe |- dc(A, B, C, D, L), PROC, TRL', START_T => V, PROC',
                                                          TRL'', STOP_T) &
   stop_proc(TRL'', PROC, STOP_T |- TRL''')
   ------------------------------------
   ve, fe |- dc(A, B, C, D, L), PROC, TRL, START_T -> V, PROC', TRL''', 
                                                         STOP_T ;


   end dist_sub_prob;
end Adl_int;