/[mojave]/metaprl/theories/mc/mp_mc_fir_eval.ml
ViewVC logotype

Diff of /metaprl/theories/mc/mp_mc_fir_eval.ml

Parent Directory Parent Directory | Revision Log Revision Log | View Patch Patch

revision 3563 by emre, Sun Mar 24 22:35:29 2002 UTC revision 3564 by emre, Fri Apr 5 07:07:58 2002 UTC
# Line 50  Line 50 
50   * Modular arithmetic for integers.   * Modular arithmetic for integers.
51   *)   *)
52    
53  (* Precision of naml integers. *)  (* Precision of naml integers. Corresponds to tyInt. *)
54    
55  declare naml_prec  declare naml_prec
56    
# Line 112  Line 112 
112   *************************************************************************)   *************************************************************************)
113    
114  (*  (*
115     * Since these rewrites express computation equivalence, I assume
116     * well-formedness of all terms.  In particular, if the rewrite
117     * is applied to an ill-formed term, the result will be meaningless.
118     * The goal is to define the rewrites as generally as possible
119     * while still preserving the semantics of the FIR.
120     *)
121    
122    (*
123   * Modular arithmetic for integers.   * Modular arithmetic for integers.
124     * Essentially, arithmetic in the FIR is not infinite precision.
125   *)   *)
126    
127    (* Precisions correspond to some number of bits. *)
128    
129  prim_rw reduce_naml_prec :  prim_rw reduce_naml_prec :
130     naml_prec <--> 31     naml_prec <--> 31
131  prim_rw reduce_int8 :  prim_rw reduce_int8 :
# Line 126  Line 137 
137  prim_rw reduce_int64 :  prim_rw reduce_int64 :
138     int64 <--> 64     int64 <--> 64
139    
140    (* Precompute some common powers of 2. *)
141    
142  prim_rw reduce_pow :  prim_rw reduce_pow :
143     pow{ 'base; 'exp } <-->     pow{ 'base; 'exp } <-->
144     ind{ 'exp; i, j. 1; 1; i, j. ('base *@ 'j) }     ifthenelse{ beq_int{'exp; 0}; 1; ('base *@ pow{'base; ('exp -@ 1)}) }
145  interactive_rw reduce_pow_2_7 :  interactive_rw reduce_pow_2_7 :
146     pow{ 2; 7 } <--> 128     pow{ 2; 7 } <--> 128
147  interactive_rw reduce_pow_2_8 :  interactive_rw reduce_pow_2_8 :
# Line 148  Line 161 
161  interactive_rw reduce_pow_2_64 :  interactive_rw reduce_pow_2_64 :
162     pow{ 2; 64 } <--> 18446744073709551616     pow{ 2; 64 } <--> 18446744073709551616
163    
164    (* Perform 2's complement arithmetic in the precision specified. *)
165    
166  prim_rw reduce_mod_arith1 :  prim_rw reduce_mod_arith1 :
167     mod_arith{ 'int_precision; signedInt; 'num } <-->     mod_arith{ 'int_precision; signedInt; 'num } <-->
168     mod_arith_signed{ 'int_precision; 'num }     mod_arith_signed{ 'int_precision; 'num }
# Line 177  Line 192 
192  prim_rw reduce_idOp :  prim_rw reduce_idOp :
193     unop_exp{ idOp; 'ty; 'atom1 } <--> 'atom1     unop_exp{ idOp; 'ty; 'atom1 } <--> 'atom1
194    
195  (* Naml ints. *)  (* Naml ints. Arithmetic results are always atomInt's (we get a value). *)
196    
197  prim_rw reduce_uminusIntOp :  prim_rw reduce_uminusIntOp :
198     unop_exp{ uminusIntOp; tyInt; atomInt{'atom1} } <-->     unop_exp{ uminusIntOp; tyInt; 'atom1 } <-->
199     atomInt{ ."minus"{'atom1} }     atomInt{ ."minus"{'atom1} }
200    
201  (*  (*
202   * Binary operations.   * Binary operations.
203   *)   *)
204    
205  (* Naml ints. *)  (* Naml ints. Arithmetic results are always atomInt's (we get a value). *)
206    
207  prim_rw reduce_plusIntOp :  prim_rw reduce_plusIntOp :
208     binop_exp{ plusIntOp; tyInt; atomInt{'atom1}; atomInt{'atom2} } <-->     binop_exp{ plusIntOp; tyInt; 'atom1; 'atom2 } <-->
209     atomInt{ mod_arith{ naml_prec; signedInt; ('atom1 +@ 'atom2) } }     atomInt{ mod_arith{ naml_prec; signedInt; ('atom1 +@ 'atom2) } }
210  prim_rw reduce_minusIntOp :  prim_rw reduce_minusIntOp :
211     binop_exp{ minusIntOp; tyInt; atomInt{'atom1}; atomInt{'atom2} } <-->     binop_exp{ minusIntOp; tyInt; 'atom1; 'atom2 } <-->
212     atomInt{ mod_arith{ naml_prec; signedInt; ('atom1 -@ 'atom2) } }     atomInt{ mod_arith{ naml_prec; signedInt; ('atom1 -@ 'atom2) } }
213  prim_rw reduce_mulIntOp :  prim_rw reduce_mulIntOp :
214     binop_exp{ mulIntOp; tyInt; atomInt{'atom1}; atomInt{'atom2} } <-->     binop_exp{ mulIntOp; tyInt; 'atom1; 'atom2 } <-->
215     atomInt{ mod_arith{ naml_prec; signedInt; ('atom1 *@ 'atom2) } }     atomInt{ mod_arith{ naml_prec; signedInt; ('atom1 *@ 'atom2) } }
216  prim_rw reduce_divIntOp :  prim_rw reduce_divIntOp :
217     binop_exp{ divIntOp; tyInt; atomInt{'atom1}; atomInt{'atom2} } <-->     binop_exp{ divIntOp; tyInt; 'atom1; 'atom2 } <-->
218     atomInt{ mod_arith{ naml_prec; signedInt; ('atom1 /@ 'atom2) } }     atomInt{ mod_arith{ naml_prec; signedInt; ('atom1 /@ 'atom2) } }
219  prim_rw reduce_remIntOp :  prim_rw reduce_remIntOp :
220     binop_exp{ remIntOp; tyInt; atomInt{'atom1}; atomInt{'atom2} } <-->     binop_exp{ remIntOp; tyInt; 'atom1; 'atom2 } <-->
221     atomInt{ mod_arith{ naml_prec; signedInt; ('atom1 %@ 'atom2) } }     atomInt{ mod_arith{ naml_prec; signedInt; ('atom1 %@ 'atom2) } }
222  prim_rw reduce_maxIntOp :  prim_rw reduce_maxIntOp :
223     binop_exp{ maxIntOp; tyInt; atomInt{'atom1}; atomInt{'atom2} } <-->     binop_exp{ maxIntOp; tyInt; 'atom1; 'atom2 } <-->
224     atomInt{ ifthenelse{ lt_bool{'atom1; 'atom2}; 'atom2; 'atom1 } }     atomInt{ ifthenelse{ lt_bool{'atom1; 'atom2}; 'atom2; 'atom1 } }
225  prim_rw reduce_minIntOp :  prim_rw reduce_minIntOp :
226     binop_exp{ minIntOp; tyInt; atomInt{'atom1}; atomInt{'atom2} } <-->     binop_exp{ minIntOp; tyInt; 'atom1; 'atom2 } <-->
227     atomInt{ ifthenelse{ lt_bool{'atom1; 'atom2}; 'atom1; 'atom2 } }     atomInt{ ifthenelse{ lt_bool{'atom1; 'atom2}; 'atom1; 'atom2 } }
228    
229  (* Native ints. *)  (* Native ints. Arithmetic results are always atomRawInt's with
230     * the appropriate precision and signing (we get a value). *)
231    
232  prim_rw reduce_plusRawIntOp :  prim_rw reduce_plusRawIntOp :
233     binop_exp{ plusRawIntOp{'p; 's}; tyRawInt{'p; 's};     binop_exp{ plusRawIntOp{'p; 's}; tyRawInt{'p; 's}; 'atom1; 'atom2 } <-->
234                atomRawInt{'p; 's; 'a1}; atomRawInt{'p; 's; 'a2} } <-->     atomRawInt{ 'p; 's; mod_arith{ 'p; 's; ('atom1 +@ 'atom2) } }
    atomRawInt{ 'p; 's; mod_arith{ 'p; 's; ('a1 +@ 'a2) } }  
235  prim_rw reduce_minusRawIntOp :  prim_rw reduce_minusRawIntOp :
236     binop_exp{ minusRawIntOp{'p; 's}; tyRawInt{'p; 's};     binop_exp{ minusRawIntOp{'p; 's}; tyRawInt{'p; 's}; 'atom1; 'atom2 } <-->
237                atomRawInt{'p; 's; 'a1}; atomRawInt{'p; 's; 'a2} } <-->     atomRawInt{ 'p; 's; mod_arith{ 'p; 's; ('atom1 -@ 'atom2) } }
    atomRawInt{ 'p; 's; mod_arith{ 'p; 's; ('a1 -@ 'a2) } }  
238  prim_rw reduce_mulRawIntOp :  prim_rw reduce_mulRawIntOp :
239     binop_exp{ mulRawIntOp{'p; 's}; tyRawInt{'p; 's};     binop_exp{ mulRawIntOp{'p; 's}; tyRawInt{'p; 's}; 'atom1; 'atom2 } <-->
240                atomRawInt{'p; 's; 'a1}; atomRawInt{'p; 's; 'a2} } <-->     atomRawInt{ 'p; 's; mod_arith{ 'p; 's; ('atom1 *@ 'atom2) } }
    atomRawInt{ 'p; 's; mod_arith{ 'p; 's; ('a1 *@ 'a2) } }  
241  prim_rw reduce_divRawIntOp :  prim_rw reduce_divRawIntOp :
242     binop_exp{ divRawIntOp{'p; 's}; tyRawInt{'p; 's};     binop_exp{ divRawIntOp{'p; 's}; tyRawInt{'p; 's}; 'atom1; 'atom2 } <-->
243                atomRawInt{'p; 's; 'a1}; atomRawInt{'p; 's; 'a2} } <-->     atomRawInt{ 'p; 's; mod_arith{ 'p; 's; ('atom1 /@ 'atom2) } }
    atomRawInt{ 'p; 's; mod_arith{ 'p; 's; ('a1 /@ 'a2) } }  
244  prim_rw reduce_remRawIntOp :  prim_rw reduce_remRawIntOp :
245     binop_exp{ remRawIntOp{'p; 's}; tyRawInt{'p; 's};     binop_exp{ remRawIntOp{'p; 's}; tyRawInt{'p; 's}; 'atom1; 'atom2 } <-->
246                atomRawInt{'p; 's; 'a1}; atomRawInt{'p; 's; 'a2} } <-->     atomRawInt{ 'p; 's; mod_arith{ 'p; 's; ('atom1 %@ 'atom2) } }
    atomRawInt{ 'p; 's; mod_arith{ 'p; 's; ('a1 %@ 'a2) } }  
247  prim_rw reduce_maxRawIntOp :  prim_rw reduce_maxRawIntOp :
248     binop_exp{ maxRawIntOp{'p; 's}; tyRawInt{'p; 's};     binop_exp{ maxRawIntOp{'p; 's}; tyRawInt{'p; 's}; 'atom1; 'atom2 } <-->
249                atomRawInt{'p; 's; 'a1}; atomRawInt{'p; 's; 'a2} } <-->     atomRawInt{ 'p; 's; ifthenelse{ lt_bool{'atom1; 'atom2}; 'atom2; 'atom1 } }
    atomRawInt{ 'p; 's; ifthenelse{ lt_bool{'a1; 'a2}; 'a2; 'a1 } }  
250  prim_rw reduce_minRawIntOp :  prim_rw reduce_minRawIntOp :
251     binop_exp{ minRawIntOp{'p; 's}; tyRawInt{'p; 's};     binop_exp{ minRawIntOp{'p; 's}; tyRawInt{'p; 's}; 'atom1; 'atom2 } <-->
252                atomRawInt{'p; 's; 'a1}; atomRawInt{'p; 's; 'a2} } <-->     atomRawInt{ 'p; 's; ifthenelse{ lt_bool{'atom1; 'atom2}; 'atom1; 'atom2 } }
    atomRawInt{ 'p; 's; ifthenelse{ lt_bool{'a1; 'a2}; 'a1; 'a2 } }  
253    
254  (*  (*
255   * Normal values. *)   * Normal values.
256     * The atomInt, atomRawInt, and atomVar "wrappers" have no meaning
257  prim_rw reduce_atomVar_atomNil :   * when we try to evaluate the FIR in MetaPRL, though they are
258     atomVar{ atomNil{ 'ty } } <--> atomNil{ 'ty }   * required in order for expressions / terms to be well-formed.
259  prim_rw reduce_atomVar_atomInt :   *)
260     atomVar{ atomInt{'int} } <--> atomInt{'int}  
261  prim_rw reduce_atomVar_atomEnum :  prim_rw reduce_atomInt :
262     atomVar{ atomEnum{ 'int1; 'int2 } } <-->     atomInt{ 'int } <--> 'int
263     atomEnum{ 'int1; 'int2 }  prim_rw reduce_atomRawInt :
264  prim_rw reduce_atomVar_atomRawInt :     atomRawInt{ 'int_precision; 'int_signed; 'num } <--> 'num
265     atomVar{ atomRawInt{ 'int_precision; 'int_signed; 'num } } <-->  prim_rw reduce_atomVar :
266     atomRawInt{ 'int_precision; 'int_signed; 'num }     atomVar{ 'var } <--> 'var
 prim_rw reduce_atomVar_atomFloat :  
    atomVar{ atomFloat{ 'float_precision; 'num } } <-->  
    atomFloat{ 'float_precision; 'num }  
 prim_rw reduce_atomVar_atomConst :  
    atomVar{ atomConst{ 'ty; 'ty_var; 'int } } <-->  
    atomConst{ 'ty; 'ty_var; 'int }  
267    
268  (*  (*
269   * Expressions.   * Expressions.
# Line 274  Line 277 
277  prim_rw reduce_letBinop :  prim_rw reduce_letBinop :
278     letBinop{ 'ty; 'binop; 'atom1; 'atom2; var. 'exp['var] } <-->     letBinop{ 'ty; 'binop; 'atom1; 'atom2; var. 'exp['var] } <-->
279     'exp[ binop_exp{ 'binop; 'ty; 'atom1; 'atom2 } ]     'exp[ binop_exp{ 'binop; 'ty; 'atom1; 'atom2 } ]
   
 (*************************************************************************  
  * Automation.  
  *************************************************************************)  
   
 let firEvalT i =  
    rwh (repeatC (applyAllC [  
   
       reduce_naml_prec;  
       reduce_int8;  
       reduce_int16;  
       reduce_int32;  
       reduce_int64;  
       reduce_pow_2_7;  
       reduce_pow_2_8;  
       reduce_pow_2_15;  
       reduce_pow_2_16;  
       reduce_pow_2_30;  
       reduce_pow_2_31;  
       reduce_pow_2_32;  
       reduce_pow_2_63;  
       reduce_pow_2_64;  
       reduce_pow;  
       reduce_mod_arith1;  
       reduce_mod_arith2;  
       reduce_mod_arith_signed;  
       reduce_mod_arith_unsigned;  
   
       reduce_plusIntOp;  
       reduce_minusIntOp;  
       reduce_mulIntOp;  
       reduce_divIntOp;  
       reduce_remIntOp;  
       reduce_maxIntOp;  
       reduce_minIntOp;  
   
       reduce_plusRawIntOp;  
       reduce_minusRawIntOp;  
       reduce_mulRawIntOp;  
       reduce_divRawIntOp;  
       reduce_remRawIntOp;  
       reduce_maxRawIntOp;  
       reduce_minRawIntOp;  
   
       reduce_atomVar_atomNil;  
       reduce_atomVar_atomInt;  
       reduce_atomVar_atomEnum;  
       reduce_atomVar_atomRawInt;  
       reduce_atomVar_atomFloat;  
       reduce_atomVar_atomConst;  
   
       reduce_letUnop;  
       reduce_letBinop;  
   
       reduceTopC (* reduce everything else; mainly for Itt term reductions. *)  
    ] )) i  

Legend:
Removed from v.3563  
changed lines
  Added in v.3564

  ViewVC Help
Powered by ViewVC 1.1.26