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

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

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

revision 3579 by emre, Fri Apr 5 07:07:58 2002 UTC revision 3580 by emre, Fri Apr 19 08:09:21 2002 UTC
# Line 98  Line 98 
98  declare rawIntOfPointerOp{ 'int_precision; 'int_signed }  declare rawIntOfPointerOp{ 'int_precision; 'int_signed }
99  declare pointerOfRawIntOp{ 'int_precision; 'int_signed }  declare pointerOfRawIntOp{ 'int_precision; 'int_signed }
100    
101  (* Pointer operations. *)  (* Pointer from a block pointer. *)
102    
103  declare rawIntOfLabelOp{ 'int_precision; 'int_signed }  declare pointerOfBlockOp{ 'sub_block }
104    
105  (*  (*
106   * Binary operations.   * Binary operations.
# Line 188  Line 188 
188    
189  (* Pointer arithmetic. *)  (* Pointer arithmetic. *)
190    
191  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 }  
192    
193  (*  (*
194   * Fields (frame labels).   * Fields (frame labels).
# Line 238  Line 205 
205  declare atomEnum{ 'int1; 'int2 } (* 'int1 = bound, 'int2 = value *)  declare atomEnum{ 'int1; 'int2 } (* 'int1 = bound, 'int2 = value *)
206  declare atomRawInt{ 'int_precision; 'int_signed; 'num }  declare atomRawInt{ 'int_precision; 'int_signed; 'num }
207  declare atomFloat{ 'float_precision; 'num }  declare atomFloat{ 'float_precision; 'num }
208  declare atomLabel{ 'frame_label }  declare atomLabel{ 'frame_label; 'atom_rawint }
209    declare atomSizeof{ 'var_list; 'atom_rawint }
210  declare atomConst{ 'ty; 'ty_var; 'int }  declare atomConst{ 'ty; 'ty_var; 'int }
211  declare atomVar{ 'var }  declare atomVar{ 'var }
212    
# Line 266  Line 234 
234   * Predicates and assertions.   * Predicates and assertions.
235   *)   *)
236    
237  (* No-ops. *)  declare isMutable{ 'var }
238    declare reserve{ 'atom1; 'atom2 }
239  declare isMutable  declare boundsCheck{ 'subop; 'var; 'atom1; 'atom2 }
240    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 }  
241    
242  (*  (*
243   * Debugging info.   * Debugging info.
# Line 450  Line 400 
400     pointerOfRawIntOp{ 'int_precision; 'int_signed } =     pointerOfRawIntOp{ 'int_precision; 'int_signed } =
401     `"PointerOfRawIntOp(" slot{'int_precision} `"," slot{'int_signed} `")"     `"PointerOfRawIntOp(" slot{'int_precision} `"," slot{'int_signed} `")"
402    
403  (* Pointer operations. *)  (* Pointer from a block pointer. *)
404    
405  dform rawIntOfLabelOp_df : except_mode[src] ::  dform pointerOfBlockOp_df : except_mode[src] ::
406     rawIntOfLabelOp{ 'int_precision; 'int_signed } =     pointerOfBlockOp{ 'sub_block } =
407     `"RawIntOfLabelOp(" slot{'int_precision} `"," slot{'int_signed} `")"     `"PointerOfBlockOp(" slot{'sub_block} `")"
408    
409  (*  (*
410   * Binary operations.   * Binary operations.
# Line 665  Line 615 
615  (* Pointer arithmetic. *)  (* Pointer arithmetic. *)
616    
617  dform plusPointerOp_df : except_mode[src] ::  dform plusPointerOp_df : except_mode[src] ::
618     plusPointerOp{ 'int_precision; 'int_signed } =     plusPointerOp{ 'sub_block; 'int_precision; 'int_signed } =
619     `"PlusPointerOp(" slot{'int_precision} `"," slot{'int_signed} `")"     `"PlusPointerOp(" slot{'sub_block} `","
620       slot{'int_precision} `"," slot{'int_signed} `")"
 (*  
  * Subscript operators.  
  *)  
   
 (* Blocks. *)  
   
 dform blockSub_df : except_mode[src] ::  
    blockSub =  
    `"BlockSub"  
 dform rawDataSub_df : except_mode[src] ::  
    rawDataSub =  
    `"RawDataSub"  
 dform tupleSub_df : except_mode[src] ::  
    tupleSub =  
    `"TupleSub"  
 dform rawTupleSub_df : except_mode[src] ::  
    rawTupleSub =  
    `"RawTupleSub"  
   
 (* Values. *)  
   
 dform polySub_df : except_mode[src] ::  
    polySub =  
    `"PolySub"  
 dform rawIntSub_df : except_mode[src] ::  
    rawIntSub{ 'int_precision; 'int_signed } =  
    `"RawIntSub(" slot{'int_precision} `"," slot{'int_signed}  
 dform rawFloatSub_df : except_mode[src] ::  
    rawFloatSub{ 'float_precision } =  
    `"RawFloatSub(" slot{'float_precision} `")"  
 dform pointerSub_df : except_mode[src] ::  
    pointerSub =  
    `"PointerSub"  
 dform functionSub_df : except_mode[src] ::  
    functionSub =  
    `"FunctionSub"  
   
 (* Indexing. *)  
   
 dform byteIndex_df : except_mode[src] ::  
    byteIndex =  
    `"ByteIndex"  
 dform wordIndex_df : except_mode[src] ::  
    wordIndex =  
    `"WordIndex"  
   
 (* Subscripting. *)  
   
 dform intIndex_df : except_mode[src] ::  
    intIndex =  
    `"IntIndex"  
 dform rawIntIndex_df : except_mode[src] ::  
    rawIntIndex{ 'int_precision; 'int_signed } =  
    `"RawIntIndex(" slot{'int_precision} `"," slot{'int_signed} `")"  
   
 (* Subscripting op. *)  
   
 dform subop_df : except_mode[src] ::  
    subop{ 'sub_block; 'sub_value; 'sub_index; 'sub_script } =  
    `"Subop(" slot{'sub_block} `"," slot{'sub_value} `","  
    slot{'sub_index} `"," slot{'sub_script} `")"  
621    
622  (*  (*
623   * Fields (frame labels).   * Fields (frame labels).
# Line 760  Line 649 
649     atomFloat{ 'float_precision; 'num } =     atomFloat{ 'float_precision; 'num } =
650     `"AtomFloat(" slot{'float_precision} `", " slot{'num} `")"     `"AtomFloat(" slot{'float_precision} `", " slot{'num} `")"
651  dform atomLabel_df : except_mode[src] ::  dform atomLabel_df : except_mode[src] ::
652     atomLabel{ 'frame_label } =     atomLabel{ 'frame_label; 'atom_rawint } =
653     `"AtomLabel(" slot{'frame_label} `")"     `"AtomLabel(" slot{'frame_label} `"," slot{'atom_rawint} `")"
654    dform atomSizeof_df : except_mode[src] ::
655       atomSizeof{ 'var_list; 'atom_rawint } =
656       `"AtomSizeof(" slot{'var_list} `"," slot{'atom_rawint} `")"
657  dform atomConst_df : except_mode[src] ::  dform atomConst_df : except_mode[src] ::
658     atomConst{ 'ty; 'ty_var; 'int } =     atomConst{ 'ty; 'ty_var; 'int } =
659     `"AtomConst(" slot{'ty} `", " slot{'ty_var} `", " slot{'int} `")"     `"AtomConst(" slot{'ty} `", " slot{'ty_var} `", " slot{'int} `")"
# Line 815  Line 707 
707   * Predicates and assertions.   * Predicates and assertions.
708   *)   *)
709    
 (* No-ops. *)  
   
710  dform isMutable_df : except_mode[src] ::  dform isMutable_df : except_mode[src] ::
711     isMutable =     isMutable{ 'var } =
712     `"IsMutable"     `"IsMutable(" slot{'var} `")"
   
 (* Unary operations. *)  
   
713  dform reserve_df : except_mode[src] ::  dform reserve_df : except_mode[src] ::
714     reserve =     reserve{ 'atom1; 'atom2 } =
715     `"Reserve"     `"Reserve(" slot{'atom1} `"," slot{'atom2} `")"
 dform boundsCheckLower_df : except_mode[src] ::  
    boundsCheckLower =  
    `"BoundsCheckLower"  
 dform boundsCheckUpper_df : except_mode[src] ::  
    boundsCheckUpper =  
    `"BoundsCheckUpper"  
 dform polyCheck_df : except_mode[src] ::  
    polyCheck =  
    `"PolyCheck"  
 dform pointerCheck_df : except_mode[src] ::  
    pointerCheck =  
    `"PointerCheck"  
 dform functionCheck_df : except_mode[src] ::  
    functionCheck =  
    `"FunctionCheck"  
   
 (* Binary operations. *)  
   
716  dform boundsCheck_df : except_mode[src] ::  dform boundsCheck_df : except_mode[src] ::
717     boundsCheck =     boundsCheck{ 'subop; 'var; 'atom1; 'atom2 } =
718     `"BoundsCheck"     `"BoundsCheck(" slot{'subop} `"," slot{'var} `","
   
 (* Predicates. *)  
   
 dform predNop_df : except_mode[src] ::  
    predNop{ 'var; 'pred_nop } =  
    `"PredNop(" slot{'var} `"," slot{'pred_nop} `")"  
 dform predUnop_df : except_mode[src] ::  
    predUnop{ 'var; 'pred_unop; 'atom } =  
    `"PredUnop(" slot{'var} `"," slot{'pred_unop} `"," slot{'atom} `")"  
 dform predBinop_df : except_mode[src] ::  
    predBinop{ 'var; 'pred_binop; 'atom1; 'atom2 } =  
    `"PredBinop(" slot{'var} `"," slot{'pred_binop} `","  
719     slot{'atom1} `"," slot{'atom2} `")"     slot{'atom1} `"," slot{'atom2} `")"
720    dform elementCheck_df : except_mode[src] ::
721       elementCheck{ 'ty; 'subop; 'var; 'atom } =
722       `"ElementCheck(" slot{'ty} `"," slot{'subop} `","
723       slot{'var} `"," slot{'atom} `")"
724    
725  (*  (*
726   * Debugging info.   * Debugging info.
727   *)   *)
728    
729  dform debugLine_df : except_mode[src] :: debugLine{ 'string; 'int } =  dform debugLine_df : except_mode[src] ::
730     lzone `"DebugLine(" slot{'string} `"," slot{'int} `")" ezone     debugLine{ 'string; 'int } =
731  dform debugVarItem_df : except_mode[src] :: debugVarItem{ 'var1; 'ty; 'var2 } =     `"DebugLine(" slot{'string} `"," slot{'int} `")"
732     lzone `"(" slot{'var1} `"," slot{'ty} `"," slot{'var2} `")" ezone  dform debugVarItem_df : except_mode[src] ::
733  dform debugVars_df : except_mode[src] :: debugVars{ 'debugVarItem_list } =     debugVarItem{ 'var1; 'ty; 'var2 } =
734     pushm[0] szone push_indent `"DebugVars(" hspace     `"(" slot{'var1} `"," slot{'ty} `"," slot{'var2} `")"
735     szone slot{'debugVarItem_list} `")" ezone popm  dform debugVars_df : except_mode[src] ::
736     ezone popm     debugVars{ 'debugVarItem_list } =
737  dform debugString_df : except_mode[src] :: debugString{ 'string } =     `"DebugVars(" slot{'debugVarItem_list} `")"
738     lzone `"DebugString(" slot{'string} `")" ezone  dform debugString_df : except_mode[src] ::
739       debugString{ 'string } =
740       `"DebugString(" slot{'string} `")"
741  dform debugContext : except_mode[src] ::  dform debugContext : except_mode[src] ::
742     debugContext{ 'debug_line; 'debug_vars } =     debugContext{ 'debug_line; 'debug_vars } =
743     pushm[0] szone push_indent `"DebugContext(" hspace     `"DebugContext(" slot{'debug_line} `"," slot{'debug_vars} `")"
    szone slot{'debug_line} `"," ezone popm  
    push_indent hspace  
    szone slot{'debug_vars} `")" ezone popm  
    ezone popm  
744    
745  (*  (*
746   * Expressions.   * Expressions.
# Line 1128  Line 987 
987  let mk_pointerOfRawIntOp_term = mk_dep0_dep0_term pointerOfRawIntOp_opname  let mk_pointerOfRawIntOp_term = mk_dep0_dep0_term pointerOfRawIntOp_opname
988  let dest_pointerOfRawIntOp_term = dest_dep0_dep0_term pointerOfRawIntOp_opname  let dest_pointerOfRawIntOp_term = dest_dep0_dep0_term pointerOfRawIntOp_opname
989    
990  let rawIntOfLabelOp_term = << rawIntOfLabelOp{ 'int_precision; 'int_signed } >>  (* Pointer from a block pointer. *)
991  let rawIntOfLabelOp_opname = opname_of_term rawIntOfLabelOp_term  
992  let is_rawIntOfLabelOp_term = is_dep0_dep0_term rawIntOfLabelOp_opname  let pointerOfBlockOp_term = << pointerOfBlockOp{ 'sub_block } >>
993  let mk_rawIntOfLabelOp_term = mk_dep0_dep0_term rawIntOfLabelOp_opname  let pointerOfBlockOp_opname = opname_of_term pointerOfBlockOp_term
994  let dest_rawIntOfLabelOp_term = dest_dep0_dep0_term rawIntOfLabelOp_opname  let is_pointerOfBlockOp_term = is_dep0_term pointerOfBlockOp_opname
995    let mk_pointerOfBlockOp_term = mk_dep0_term pointerOfBlockOp_opname
996    let dest_pointerOfBlockOp_term = dest_dep0_term pointerOfBlockOp_opname
997    
998  (*  (*
999   * Binary operations.   * Binary operations.
# Line 1467  Line 1328 
1328    
1329  (* Pointer arithmetic. *)  (* Pointer arithmetic. *)
1330    
1331  let plusPointerOp_term = << plusPointerOp{ 'int_precision; 'int_signed } >>  let plusPointerOp_term =
1332       << plusPointerOp{ 'sub_block; 'int_precision; 'int_signed } >>
1333  let plusPointerOp_opname = opname_of_term plusPointerOp_term  let plusPointerOp_opname = opname_of_term plusPointerOp_term
1334  let is_plusPointerOp_term = is_dep0_dep0_term plusPointerOp_opname  let is_plusPointerOp_term = is_dep0_dep0_dep0_term plusPointerOp_opname
1335  let mk_plusPointerOp_term = mk_dep0_dep0_term plusPointerOp_opname  let mk_plusPointerOp_term = mk_dep0_dep0_dep0_term plusPointerOp_opname
1336  let dest_plusPointerOp_term = dest_dep0_dep0_term plusPointerOp_opname  let dest_plusPointerOp_term = dest_dep0_dep0_dep0_term plusPointerOp_opname
   
 (*  
  * Subscript operators.  
  *)  
   
 (* Blocks. *)  
   
 let blockSub_term = << blockSub >>  
 let blockSub_opname = opname_of_term blockSub_term  
 let is_blockSub_term = is_no_subterms_term blockSub_opname  
   
 let rawDataSub_term = << rawDataSub >>  
 let rawDataSub_opname = opname_of_term rawDataSub_term  
 let is_rawDataSub_term = is_no_subterms_term rawDataSub_opname  
   
 let tupleSub_term = << tupleSub >>  
 let tupleSub_opname = opname_of_term tupleSub_term  
 let is_tupleSub_term = is_no_subterms_term tupleSub_opname  
   
 let rawTupleSub_term = << rawTupleSub >>  
 let rawTupleSub_opname = opname_of_term rawTupleSub_term  
 let is_rawTupleSub_term = is_no_subterms_term rawTupleSub_opname  
   
 (* Values. *)  
   
 let polySub_term = << polySub >>  
 let polySub_opname = opname_of_term polySub_term  
 let is_polySub_term = is_no_subterms_term polySub_opname  
   
 let rawIntSub_term = << rawIntSub{ 'int_precision; 'int_signed } >>  
 let rawIntSub_opname = opname_of_term rawIntSub_term  
 let is_rawIntSub_term = is_dep0_dep0_term rawIntSub_opname  
 let mk_rawIntSub_term = mk_dep0_dep0_term rawIntSub_opname  
 let dest_rawIntSub_term = dest_dep0_dep0_term rawIntSub_opname  
   
 let rawFloatSub_term = << rawFloatSub{ 'float_precision } >>  
 let rawFloatSub_opname = opname_of_term rawFloatSub_term  
 let is_rawFloatSub_term = is_dep0_term rawFloatSub_opname  
 let mk_rawFloatSub_term = mk_dep0_term rawFloatSub_opname  
 let dest_rawFloatSub_term = dest_dep0_term rawFloatSub_opname  
   
 let pointerSub_term = << pointerSub >>  
 let pointerSub_opname = opname_of_term pointerSub_term  
 let is_pointerSub_term = is_no_subterms_term pointerSub_opname  
   
 let functionSub_term = << functionSub >>  
 let functionSub_opname = opname_of_term functionSub_term  
 let is_functionSub_term = is_no_subterms_term functionSub_opname  
   
 (* Indexing. *)  
   
 let byteIndex_term = << byteIndex >>  
 let byteIndex_opname = opname_of_term byteIndex_term  
 let is_byteIndex_term = is_no_subterms_term byteIndex_opname  
   
 let wordIndex_term = << wordIndex >>  
 let wordIndex_opname = opname_of_term wordIndex_term  
 let is_wordIndex_term = is_no_subterms_term wordIndex_opname  
   
 (* Subscripting. *)  
   
 let intIndex_term = << intIndex >>  
 let intIndex_opname = opname_of_term intIndex_term  
 let is_intIndex_term = is_no_subterms_term intIndex_opname  
   
 let rawIntIndex_term = << rawIntIndex{ 'int_precision; 'int_signed } >>  
 let rawIntIndex_opname = opname_of_term rawIntIndex_term  
 let is_rawIntIndex_term = is_dep0_dep0_term rawIntIndex_opname  
 let mk_rawIntIndex_term = mk_dep0_dep0_term rawIntIndex_opname  
 let dest_rawIntIndex_term = dest_dep0_dep0_term rawIntIndex_opname  
   
 (* Subscripting op. *)  
   
 let subop_term = << subop{ 'sub_block; 'sub_value; 'sub_index; 'sub_script } >>  
 let subop_opname = opname_of_term subop_term  
 let is_subop_term = is_4_dep0_term subop_opname  
 let mk_subop_term = mk_4_dep0_term subop_opname  
 let dest_subop_term = dest_4_dep0_term subop_opname  
1337    
1338  (*  (*
1339   * Fields (frame labels).   * Fields (frame labels).
# Line 1595  Line 1379 
1379  let mk_atomFloat_term = mk_dep0_dep0_term atomFloat_opname  let mk_atomFloat_term = mk_dep0_dep0_term atomFloat_opname
1380  let dest_atomFloat_term = dest_dep0_dep0_term atomFloat_opname  let dest_atomFloat_term = dest_dep0_dep0_term atomFloat_opname
1381    
1382  let atomLabel_term = << atomLabel{ 'frame_label } >>  let atomLabel_term = << atomLabel{ 'frame_label; 'atom_rawint } >>
1383  let atomLabel_opname = opname_of_term atomLabel_term  let atomLabel_opname = opname_of_term atomLabel_term
1384  let is_atomLabel_term = is_dep0_term atomLabel_opname  let is_atomLabel_term = is_dep0_dep0_term atomLabel_opname
1385  let mk_atomLabel_term = mk_dep0_term atomLabel_opname  let mk_atomLabel_term = mk_dep0_dep0_term atomLabel_opname
1386  let dest_atomLabel_term = dest_dep0_term atomLabel_opname  let dest_atomLabel_term = dest_dep0_dep0_term atomLabel_opname
1387    
1388    let atomSizeof_term = << atomSizeof{ 'var_list; 'atom_rawint } >>
1389    let atomSizeof_opname = opname_of_term atomSizeof_term
1390    let is_atomSizeof_term = is_dep0_dep0_term atomSizeof_opname
1391    let mk_atomSizeof_term = mk_dep0_dep0_term atomSizeof_opname
1392    let dest_atomSizeof_term = dest_dep0_dep0_term atomSizeof_opname
1393    
1394  let atomConst_term = << atomConst{ 'ty; 'ty_var; 'int } >>  let atomConst_term = << atomConst{ 'ty; 'ty_var; 'int } >>
1395  let atomConst_opname = opname_of_term atomConst_term  let atomConst_opname = opname_of_term atomConst_term
# Line 1686  Line 1476 
1476   * Predicates and assertions.   * Predicates and assertions.
1477   *)   *)
1478    
1479  (* No-ops. *)  let isMutable_term = << isMutable{ 'var } >>
   
 let isMutable_term = << isMutable >>  
1480  let isMutable_opname = opname_of_term isMutable_term  let isMutable_opname = opname_of_term isMutable_term
1481  let is_isMutable_term = is_no_subterms_term isMutable_opname  let is_isMutable_term = is_dep0_term isMutable_opname
1482    let mk_isMutable_term = mk_dep0_term isMutable_opname
1483  (* Unary operations. *)  let dest_isMutable_term = dest_dep0_term isMutable_opname
1484    
1485  let reserve_term = << reserve >>  let reserve_term = << reserve{ 'atom1; 'atom2 } >>
1486  let reserve_opname = opname_of_term reserve_term  let reserve_opname = opname_of_term reserve_term
1487  let is_reserve_term = is_no_subterms_term reserve_opname  let is_reserve_term = is_dep0_dep0_term reserve_opname
1488    let mk_reserve_term = mk_dep0_dep0_term reserve_opname
1489    let dest_reserve_term = dest_dep0_dep0_term reserve_opname
1490    
1491  let boundsCheckLower_term = << boundsCheckLower >>  let boundsCheck_term = << boundsCheck{ 'subop; 'var; 'atom1; 'atom2 } >>
 let boundsCheckLower_opname = opname_of_term boundsCheckLower_term  
 let is_boundsCheckLower_term = is_no_subterms_term boundsCheckLower_opname  
   
 let boundsCheckUpper_term = << boundsCheckUpper >>  
 let boundsCheckUpper_opname = opname_of_term boundsCheckUpper_term  
 let is_boundsCheckUpper_term = is_no_subterms_term boundsCheckUpper_opname  
   
 let polyCheck_term = << polyCheck >>  
 let polyCheck_opname = opname_of_term polyCheck_term  
 let is_polyCheck_term = is_no_subterms_term polyCheck_opname  
   
 let pointerCheck_term = << pointerCheck >>  
 let pointerCheck_opname = opname_of_term pointerCheck_term  
 let is_pointerCheck_term = is_no_subterms_term pointerCheck_opname  
   
 let functionCheck_term = << functionCheck >>  
 let functionCheck_opname = opname_of_term functionCheck_term  
 let is_functionCheck_term = is_no_subterms_term functionCheck_opname  
   
 (* Binary operations. *)  
   
 let boundsCheck_term = << boundsCheck >>  
1492  let boundsCheck_opname = opname_of_term boundsCheck_term  let boundsCheck_opname = opname_of_term boundsCheck_term
1493  let is_boundsCheck_term = is_no_subterms_term boundsCheck_opname  let is_boundsCheck_term = is_4_dep0_term boundsCheck_opname
1494    let mk_boundsCheck_term = mk_4_dep0_term boundsCheck_opname
1495  (* Predicates. *)  let dest_boundsCheck_term = dest_4_dep0_term boundsCheck_opname
1496    
1497  let predNop_term = << predNop{ 'var; 'pred_nop } >>  let elementCheck_term = << elementCheck{ 'ty; 'subop; 'var; 'atom } >>
1498  let predNop_opname = opname_of_term predNop_term  let elementCheck_opname = opname_of_term elementCheck_term
1499  let is_predNop_term = is_dep0_dep0_term predNop_opname  let is_elementCheck_term = is_4_dep0_term elementCheck_opname
1500  let mk_predNop_term = mk_dep0_dep0_term predNop_opname  let mk_elementCheck_term = mk_4_dep0_term elementCheck_opname
1501  let dest_predNop_term = dest_dep0_dep0_term predNop_opname  let dest_elementCheck_term = dest_4_dep0_term elementCheck_opname
   
 let predUnop_term = << predUnop{ 'var; 'pred_unop; 'atom } >>  
 let predUnop_opname = opname_of_term predUnop_term  
 let is_predUnop_term = is_dep0_dep0_dep0_term predUnop_opname  
 let mk_predUnop_term = mk_dep0_dep0_dep0_term predUnop_opname  
 let dest_predUnop_term = dest_dep0_dep0_dep0_term predUnop_opname  
   
 let predBinop_term = << predBinop{ 'var; 'pred_binop; 'atom1; 'atom2 } >>  
 let predBinop_opname = opname_of_term predBinop_term  
 let is_predBinop_term = is_4_dep0_term predBinop_opname  
 let mk_predBinop_term = mk_4_dep0_term predBinop_opname  
 let dest_predBinop_term = dest_4_dep0_term predBinop_opname  
1502    
1503  (*  (*
1504   * Debugging info.   * Debugging info.

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

  ViewVC Help
Powered by ViewVC 1.1.26