/[mojave]/metaprl/theories/mc/mp_mc_fir_exp.mli
ViewVC logotype

Diff of /metaprl/theories/mc/mp_mc_fir_exp.mli

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

revision 3564 by emre, Fri Apr 5 07:07:58 2002 UTC revision 3580 by emre, Fri Apr 19 08:09:21 2002 UTC
# Line 96  Line 96 
96  declare rawIntOfPointerOp{ 'int_precision; 'int_signed }  declare rawIntOfPointerOp{ 'int_precision; 'int_signed }
97  declare pointerOfRawIntOp{ 'int_precision; 'int_signed }  declare pointerOfRawIntOp{ 'int_precision; 'int_signed }
98    
99  (* Pointer operations. *)  (* Pointer from a block pointer. *)
100    
101  declare rawIntOfLabelOp{ 'int_precision; 'int_signed }  declare pointerOfBlockOp{ 'sub_block }
102    
103  (*  (*
104   * Binary operations.   * Binary operations.
# Line 186  Line 186 
186    
187  (* Pointer arithmetic. *)  (* Pointer arithmetic. *)
188    
189  declare plusPointerOp{ 'int_precision; 'int_signed }  declare plusPointerOp{ 'sub_block; 'int_precision; 'int_signed }
   
 (*  
  * Subscript operators.  
  *)  
   
 (* Blocks. *)  
   
 declare blockSub  
 declare rawDataSub  
 declare tupleSub  
 declare rawTupleSub  
   
 (* Values. *)  
   
 declare polySub  
 declare rawIntSub{ 'int_precision; 'int_signed }  
 declare rawFloatSub{ 'float_precision }  
 declare pointerSub  
 declare functionSub  
   
 (* Indexing. *)  
   
 declare byteIndex  
 declare wordIndex  
   
 (* Subscripting. *)  
   
 declare intIndex  
 declare rawIntIndex{ 'int_precision; 'int_signed }  
   
 (* Subscripting op. *)  
   
 declare subop{ 'sub_block; 'sub_value; 'sub_index; 'sub_script }  
190    
191  (*  (*
192   * Fields (frame labels).   * Fields (frame labels).
# Line 236  Line 203 
203  declare atomEnum{ 'int1; 'int2 } (* 'int1 = bound, 'int2 = value *)  declare atomEnum{ 'int1; 'int2 } (* 'int1 = bound, 'int2 = value *)
204  declare atomRawInt{ 'int_precision; 'int_signed; 'num }  declare atomRawInt{ 'int_precision; 'int_signed; 'num }
205  declare atomFloat{ 'float_precision; 'num }  declare atomFloat{ 'float_precision; 'num }
206  declare atomLabel{ 'frame_label }  declare atomLabel{ 'frame_label; 'atom_rawint }
207    declare atomSizeof{ 'var_list; 'atom_rawint }
208  declare atomConst{ 'ty; 'ty_var; 'int }  declare atomConst{ 'ty; 'ty_var; 'int }
209  declare atomVar{ 'var }  declare atomVar{ 'var }
210    
# Line 264  Line 232 
232   * Predicates and assertions.   * Predicates and assertions.
233   *)   *)
234    
235  (* No-ops. *)  declare isMutable{ 'var }
236    declare reserve{ 'atom1; 'atom2 }
237  declare isMutable  declare boundsCheck{ 'subop; 'var; 'atom1; 'atom2 }
238    declare elementCheck{ 'ty; 'subop; 'var; 'atom }
 (* Unary operations. *)  
   
 declare reserve  
 declare boundsCheckLower  
 declare boundsCheckUpper  
 declare polyCheck  
 declare pointerCheck  
 declare functionCheck  
   
 (* Binary operations. *)  
   
 declare boundsCheck  
   
 (* Predicates. *)  
   
 declare predNop{ 'var; 'pred_nop }  
 declare predUnop{ 'var; 'pred_unop; 'atom }  
 declare predBinop{ 'var; 'pred_binop; 'atom1; 'atom2 }  
239    
240  (*  (*
241   * Debugging info.   * Debugging info.
# Line 469  Line 419 
419  val mk_pointerOfRawIntOp_term : term -> term -> term  val mk_pointerOfRawIntOp_term : term -> term -> term
420  val dest_pointerOfRawIntOp_term : term -> term * term  val dest_pointerOfRawIntOp_term : term -> term * term
421    
422  val rawIntOfLabelOp_term : term  val pointerOfBlockOp_term : term
423  val is_rawIntOfLabelOp_term : term -> bool  val is_pointerOfBlockOp_term : term -> bool
424  val mk_rawIntOfLabelOp_term : term -> term -> term  val mk_pointerOfBlockOp_term : term -> term
425  val dest_rawIntOfLabelOp_term : term -> term * term  val dest_pointerOfBlockOp_term : term -> term
426    
427  (*  (*
428   * Binary operations.   * Binary operations.
# Line 753  Line 703 
703    
704  val plusPointerOp_term : term  val plusPointerOp_term : term
705  val is_plusPointerOp_term : term -> bool  val is_plusPointerOp_term : term -> bool
706  val mk_plusPointerOp_term : term -> term -> term  val mk_plusPointerOp_term : term -> term -> term -> term
707  val dest_plusPointerOp_term : term -> term * term  val dest_plusPointerOp_term : term -> term * term * term
   
 (*  
  * Subscript operators.  
  *)  
   
 (* Blocks. *)  
   
 val blockSub_term : term  
 val is_blockSub_term : term -> bool  
   
 val rawDataSub_term : term  
 val is_rawDataSub_term : term -> bool  
   
 val tupleSub_term : term  
 val is_tupleSub_term : term -> bool  
   
 val rawTupleSub_term : term  
 val is_rawTupleSub_term : term -> bool  
   
 (* Values. *)  
   
 val polySub_term : term  
 val is_polySub_term : term -> bool  
   
 val rawIntSub_term : term  
 val is_rawIntSub_term : term -> bool  
 val mk_rawIntSub_term : term -> term -> term  
 val dest_rawIntSub_term : term -> term * term  
   
 val rawFloatSub_term : term  
 val is_rawFloatSub_term : term -> bool  
 val mk_rawFloatSub_term : term -> term  
 val dest_rawFloatSub_term : term -> term  
   
 val pointerSub_term : term  
 val is_pointerSub_term : term -> bool  
   
 val functionSub_term : term  
 val is_functionSub_term : term -> bool  
   
 (* Indexing. *)  
   
 val byteIndex_term : term  
 val is_byteIndex_term : term -> bool  
   
 val wordIndex_term : term  
 val is_wordIndex_term : term -> bool  
   
 (* Subscripting. *)  
   
 val intIndex_term : term  
 val is_intIndex_term : term -> bool  
   
 val rawIntIndex_term : term  
 val is_rawIntIndex_term : term -> bool  
 val mk_rawIntIndex_term : term -> term -> term  
 val dest_rawIntIndex_term : term -> term * term  
   
 (* Susbscripting op. *)  
   
 val subop_term : term  
 val is_subop_term : term -> bool  
 val mk_subop_term : term -> term -> term -> term -> term  
 val dest_subop_term : term -> term * term * term * term  
708    
709  (*  (*
710   * Fields (frame labels).   * Fields (frame labels).
# Line 860  Line 746 
746    
747  val atomLabel_term : term  val atomLabel_term : term
748  val is_atomLabel_term : term -> bool  val is_atomLabel_term : term -> bool
749  val mk_atomLabel_term : term -> term  val mk_atomLabel_term : term -> term -> term
750  val dest_atomLabel_term : term -> term  val dest_atomLabel_term : term -> term * term
751    
752    val atomSizeof_term : term
753    val is_atomSizeof_term : term -> bool
754    val mk_atomSizeof_term : term -> term -> term
755    val dest_atomSizeof_term : term -> term * term
756    
757  val atomConst_term : term  val atomConst_term : term
758  val is_atomConst_term : term -> bool  val is_atomConst_term : term -> bool
# Line 935  Line 826 
826   * Predicates and assertions.   * Predicates and assertions.
827   *)   *)
828    
 (* No-ops. *)  
   
829  val isMutable_term : term  val isMutable_term : term
830  val is_isMutable_term : term -> bool  val is_isMutable_term : term -> bool
831    val mk_isMutable_term : term -> term
832  (* Unary operations. *)  val dest_isMutable_term : term -> term
833    
834  val reserve_term : term  val reserve_term : term
835  val is_reserve_term : term -> bool  val is_reserve_term : term -> bool
836    val mk_reserve_term : term -> term -> term
837  val boundsCheckLower_term : term  val dest_reserve_term : term -> term * term
 val is_boundsCheckLower_term : term -> bool  
   
 val boundsCheckUpper_term : term  
 val is_boundsCheckUpper_term : term -> bool  
   
 val polyCheck_term : term  
 val is_polyCheck_term : term -> bool  
   
 val pointerCheck_term : term  
 val is_pointerCheck_term : term -> bool  
   
 val functionCheck_term : term  
 val is_functionCheck_term : term -> bool  
   
 (* Binary operations. *)  
838    
839  val boundsCheck_term : term  val boundsCheck_term : term
840  val is_boundsCheck_term : term -> bool  val is_boundsCheck_term : term -> bool
841    val mk_boundsCheck_term : term -> term -> term -> term -> term
842    val dest_boundsCheck_term : term -> term * term * term * term
843    
844  (* Predicates. *)  val elementCheck_term : term
845    val is_elementCheck_term : term -> bool
846  val predNop_term : term  val mk_elementCheck_term : term -> term -> term -> term -> term
847  val is_predNop_term : term -> bool  val dest_elementCheck_term : term -> term * term * term * term
 val mk_predNop_term : term -> term -> term  
 val dest_predNop_term : term -> term * term  
   
 val predUnop_term : term  
 val is_predUnop_term : term -> bool  
 val mk_predUnop_term : term -> term -> term -> term  
 val dest_predUnop_term : term -> term * term * term  
   
 val predBinop_term : term  
 val is_predBinop_term : term -> bool  
 val mk_predBinop_term : term -> term -> term -> term -> term  
 val dest_predBinop_term : term -> term * term * term * term  
848    
849  (*  (*
850   * Debugging info.   * Debugging info.

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

  ViewVC Help
Powered by ViewVC 1.1.26