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

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

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

revision 3575 by emre, Fri Apr 5 09:33:57 2002 UTC revision 3576 by emre, Fri Apr 12 05:37:53 2002 UTC
# Line 58  Line 58 
58   * Binary operations.   * Binary operations.
59   *)   *)
60    
61    (* Naml ints. *)
62    
63  interactive_rw const_elim_plusIntOp :  interactive_rw const_elim_plusIntOp :
64     letBinop{ tyInt; plusIntOp; atomInt{'i1}; atomInt{'i2}; v. 'exp['v] } <-->     letBinop{ tyInt; plusIntOp; atomInt{'i1}; atomInt{'i2}; v. 'exp['v] } <-->
65     'exp[ binop_exp{ plusIntOp; tyInt; 'i1; 'i2 } ]     'exp[ binop_exp{ plusIntOp; tyInt; 'i1; 'i2 } ]
# Line 70  Line 72 
72     letBinop{ tyInt; mulIntOp; atomInt{'i1}; atomInt{'i2}; v. 'exp['v] } <-->     letBinop{ tyInt; mulIntOp; atomInt{'i1}; atomInt{'i2}; v. 'exp['v] } <-->
73     'exp[ binop_exp{ mulIntOp; tyInt; 'i1; 'i2 } ]     'exp[ binop_exp{ mulIntOp; tyInt; 'i1; 'i2 } ]
74    
75    (* Native ints. *)
76    
77  interactive_rw const_elim_plusRawIntOp :  interactive_rw const_elim_plusRawIntOp :
78     letBinop{ tyRawInt{'p; 's}; plusRawIntOp{'p; 's};     letBinop{ tyRawInt{'p; 's}; plusRawIntOp{'p; 's};
79        atomRawInt{'p; 's; 'i1}; atomRawInt{'p; 's; 'i2}; v. 'exp['v] } <-->        atomRawInt{'p; 's; 'i1}; atomRawInt{'p; 's; 'i2}; v. 'exp['v] } <-->

Legend:
Removed from v.3575  
changed lines
  Added in v.3576

  ViewVC Help
Powered by ViewVC 1.1.26