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

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

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

revision 3579 by emre, Fri Apr 5 01:16:49 2002 UTC revision 3580 by emre, Fri Apr 19 08:09:21 2002 UTC
# Line 121  Line 121 
121           mk_pointerOfRawIntOp_term  (term_of_int_precision p)           mk_pointerOfRawIntOp_term  (term_of_int_precision p)
122                                      (term_of_int_signed s)                                      (term_of_int_signed s)
123    
124        (* Pointer operations. *)        (* Pointer from a block pointer. *)
125      | RawIntOfLabelOp (p, s) ->      | PointerOfBlockOp sub_block ->
126           mk_rawIntOfLabelOp_term    (term_of_int_precision p)           mk_pointerOfBlockOp_term   (term_of_sub_block sub_block)
                                     (term_of_int_signed s)  
127    
128  let unop_of_term t =  let unop_of_term t =
129    
# Line 216  Line 215 
215                             (int_signed_of_term s)                             (int_signed_of_term s)
216    
217     (* Pointer operations. *)     (* Pointer operations. *)
218     else if is_rawIntOfLabelOp_term t then     else if is_pointerOfBlockOp_term t then
219        let p, s = dest_rawIntOfLabelOp_term t in        PointerOfBlockOp  (sub_block_of_term (dest_pointerOfBlockOp_term t))
          RawIntOfLabelOp   (int_precision_of_term p)  
                            (int_signed_of_term s)  
220    
221     else     else
222        raise (RefineError ("unop_of_term", StringTermError        raise (RefineError ("unop_of_term", StringTermError
# Line 331  Line 328 
328      | NeqEqOp ->  neqEqOp_term      | NeqEqOp ->  neqEqOp_term
329    
330        (* Pointer arithmetic. *)        (* Pointer arithmetic. *)
331      | PlusPointerOp (p, s) ->      | PlusPointerOp (sub_block, p, s) ->
332           mk_plusPointerOp_term   (term_of_int_precision p)           mk_plusPointerOp_term   (term_of_sub_block sub_block)
333                                     (term_of_int_precision p)
334                                   (term_of_int_signed s)                                   (term_of_int_signed s)
335    
336  let binop_of_term t =  let binop_of_term t =
# Line 477  Line 475 
475    
476     (* Pointer arithmetic. *)     (* Pointer arithmetic. *)
477     else if is_plusPointerOp_term t then     else if is_plusPointerOp_term t then
478        let p, s = dest_plusPointerOp_term t in        let sub_block, p, s = dest_plusPointerOp_term t in
479           PlusPointerOp  (int_precision_of_term p)           PlusPointerOp  (sub_block_of_term sub_block)
480                            (int_precision_of_term p)
481                          (int_signed_of_term s)                          (int_signed_of_term s)
482    
483     else     else
# Line 486  Line 485 
485              ("not a binop", t)))              ("not a binop", t)))
486    
487  (*  (*
  * Convert to and from subscripting terms.  
  *)  
   
 let term_of_sub_block b =  
    match b with  
       BlockSub ->    blockSub_term  
     | RawDataSub ->  rawDataSub_term  
     | TupleSub ->    tupleSub_term  
     | RawTupleSub -> rawTupleSub_term  
   
 let sub_block_of_term t =  
    if is_blockSub_term t then  
       BlockSub  
    else if is_rawDataSub_term t then  
       RawDataSub  
    else if is_tupleSub_term t then  
       TupleSub  
    else if is_rawTupleSub_term t then  
       RawTupleSub  
   
    else  
       raise (RefineError ("sub_block_of_term", StringTermError  
             ("not a sub_block", t)))  
   
 let term_of_sub_value v =  
    match v with  
       PolySub ->           polySub_term  
     | RawIntSub (p, s) ->  mk_rawIntSub_term (term_of_int_precision p)  
                                              (term_of_int_signed s)  
     | RawFloatSub p ->     mk_rawFloatSub_term (term_of_float_precision p)  
     | PointerSub ->        pointerSub_term  
     | FunctionSub ->       functionSub_term  
   
 let sub_value_of_term t =  
    if is_polySub_term t then  
       PolySub  
    else if is_rawIntSub_term t then  
       let p, s = dest_rawIntSub_term t in  
          RawIntSub   (int_precision_of_term p)  
                      (int_signed_of_term s)  
    else if is_rawFloatSub_term t then  
       RawFloatSub (float_precision_of_term (dest_rawFloatSub_term t))  
    else if is_pointerSub_term t then  
       PointerSub  
    else if is_functionSub_term t then  
       FunctionSub  
   
    else  
       raise (RefineError ("sub_value_of_term", StringTermError  
             ("not a sub_value", t)))  
   
 let term_of_sub_index i =  
    match i with  
       ByteIndex -> byteIndex_term  
     | WordIndex -> wordIndex_term  
   
 let sub_index_of_term t =  
    if is_byteIndex_term t then  
       ByteIndex  
    else if is_wordIndex_term t then  
       WordIndex  
   
    else  
       raise (RefineError ("sub_index_of_term", StringTermError  
             ("not a sub_index", t)))  
   
 let term_of_sub_script t =  
    match t with  
       IntIndex ->             intIndex_term  
     | RawIntIndex (p, s) ->   mk_rawIntIndex_term (term_of_int_precision p)  
                                                   (term_of_int_signed s)  
   
 let sub_script_of_term t =  
    if is_intIndex_term t then  
       IntIndex  
    else if is_rawIntIndex_term t then  
       let p, s = dest_rawIntIndex_term t in  
          RawIntIndex (int_precision_of_term p)  
                      (int_signed_of_term s)  
   
    else  
       raise (RefineError ("sub_script_of_term", StringTermError  
             ("not a sub_script", t)))  
   
 let term_of_subop op =  
    mk_subop_term        (term_of_sub_block op.sub_block)  
                         (term_of_sub_value op.sub_value)  
                         (term_of_sub_index op.sub_index)  
                         (term_of_sub_script op.sub_script)  
   
 let subop_of_term t =  
    if is_subop_term t then  
       let block, value, index, script = dest_subop_term t in  
          {  sub_block = sub_block_of_term block;  
             sub_value = sub_value_of_term value;  
             sub_index = sub_index_of_term index;  
             sub_script = sub_script_of_term script  
          }  
   
    else  
       raise (RefineError ("subop_of_term", StringTermError  
             ("not a subop", t)))  
   
 (*  
488   * Convert to and from frame_label.   * Convert to and from frame_label.
489   *)   *)
490    
# Line 613  Line 508 
508   * Convert to and from atom.   * Convert to and from atom.
509   *)   *)
510    
511  let term_of_atom a =  let rec term_of_atom a =
512     match a with     match a with
513        AtomNil t ->        AtomNil t ->
514           mk_atomNil_term      (term_of_ty t)           mk_atomNil_term      (term_of_ty t)
# Line 628  Line 523 
523      | AtomFloat f ->      | AtomFloat f ->
524           mk_atomFloat_term    (term_of_float_precision (Rawfloat.precision f))           mk_atomFloat_term    (term_of_float_precision (Rawfloat.precision f))
525                                (number_term_of_rawfloat f)                                (number_term_of_rawfloat f)
526      | AtomLabel flbl ->      | AtomLabel (flbl, rawint) ->
527           mk_atomLabel_term    (term_of_frame_label flbl)           mk_atomLabel_term    (term_of_frame_label flbl)
528                                  (term_of_atom (AtomRawInt rawint))
529        | AtomSizeof (vl, rawint) ->
530             mk_atomSizeof_term   (term_of_list term_of_var vl)
531                                  (term_of_atom (AtomRawInt rawint))
532      | AtomConst (t, tv, i) ->      | AtomConst (t, tv, i) ->
533           mk_atomConst_term    (term_of_ty t)           mk_atomConst_term    (term_of_ty t)
534                                (term_of_ty_var tv)                                (term_of_ty_var tv)
# Line 637  Line 536 
536      | AtomVar v ->      | AtomVar v ->
537           mk_atomVar_term      (term_of_var v)           mk_atomVar_term      (term_of_var v)
538    
539  let atom_of_term t =  let rec atom_of_term t =
540     if is_atomNil_term t then     if is_atomNil_term t then
541        AtomNil (ty_of_term (dest_atomNil_term t))        AtomNil (ty_of_term (dest_atomNil_term t))
542     else if is_atomInt_term t then     else if is_atomInt_term t then
# Line 654  Line 553 
553        let p, f = dest_atomFloat_term t in        let p, f = dest_atomFloat_term t in
554           AtomFloat (rawfloat_of_number_term (float_precision_of_term p) f)           AtomFloat (rawfloat_of_number_term (float_precision_of_term p) f)
555     else if is_atomLabel_term t then     else if is_atomLabel_term t then
556        AtomLabel (frame_label_of_term (dest_atomLabel_term t))        let flbl, num = dest_atomLabel_term t in
557          let atom_rawint = atom_of_term num in
558             match atom_rawint with
559                AtomRawInt r ->
560                   AtomLabel   (frame_label_of_term flbl)
561                               r
562                 | _ ->
563                      raise (RefineError ("atom_of_term", StringTermError
564                            ("internal error", t)))
565       else if is_atomSizeof_term t then
566          let var_list, num = dest_atomSizeof_term t in
567          let atom_rawint = atom_of_term num in
568             match atom_rawint with
569                AtomRawInt r ->
570                   AtomSizeof  (list_of_term var_of_term var_list)
571                               r
572              | _ ->
573                      raise (RefineError ("atom_of_term", StringTermError
574                            ("internal error", t)))
575     else if is_atomConst_term t then     else if is_atomConst_term t then
576        let t, tv, i = dest_atomConst_term t in        let t, tv, i = dest_atomConst_term t in
577           AtomConst (ty_of_term t) (ty_var_of_term tv) (int_of_number_term i)           AtomConst (ty_of_term t) (ty_var_of_term tv) (int_of_number_term i)
# Line 777  Line 694 
694   * Convert to and from predicate / assertion terms.   * Convert to and from predicate / assertion terms.
695   *)   *)
696    
 let term_of_pred_nop op =  
    match op with  
       IsMutable -> isMutable_term  
   
 let pred_nop_of_term t =  
    if is_isMutable_term t then  
       IsMutable  
   
    else  
       raise (RefineError ("pred_nop_of_term", StringTermError  
             ("not a pred_nop", t)))  
   
 let term_of_pred_unop op =  
    match op with  
       Reserve ->           reserve_term  
     | BoundsCheckLower ->  boundsCheckLower_term  
     | BoundsCheckUpper ->  boundsCheckUpper_term  
     | PolyCheck ->         polyCheck_term  
     | PointerCheck ->      pointerCheck_term  
     | FunctionCheck ->     functionCheck_term  
   
 let pred_unop_of_term t =  
    if is_reserve_term t then  
       Reserve  
    else if is_boundsCheckLower_term t then  
       BoundsCheckLower  
    else if is_boundsCheckUpper_term t then  
       BoundsCheckUpper  
    else if is_polyCheck_term t then  
       PolyCheck  
    else if is_pointerCheck_term t then  
       PointerCheck  
    else if is_functionCheck_term t then  
       FunctionCheck  
   
    else  
       raise (RefineError ("pred_unop_of_term", StringTermError  
             ("not a pred_unop", t)))  
   
 let term_of_pred_binop op =  
    match op with  
       BoundsCheck -> boundsCheck_term  
   
 let pred_binop_of_term t =  
    if is_boundsCheck_term t then  
       BoundsCheck  
   
    else  
       raise (RefineError ("pred_binop_of_term", StringTermError  
             ("not a pred_binop", t)))  
   
697  let term_of_pred p =  let term_of_pred p =
698     match p with     match p with
699        PredNop (v, op) ->        IsMutable var ->
700           mk_predNop_term         (term_of_var v)           mk_isMutable_term    (term_of_var var)
701                                   (term_of_pred_nop op)      | Reserve (a1, a2) ->
702      | PredUnop (v, op, a) ->           mk_reserve_term      (term_of_atom a1)
703           mk_predUnop_term        (term_of_var v)                                (term_of_atom a2)
704                                   (term_of_pred_unop op)      | BoundsCheck (subop, var, a1, a2) ->
705                                   (term_of_atom a)           mk_boundsCheck_term  (term_of_subop subop)
706      | PredBinop (v, op, a1, a2) ->                                (term_of_var var)
707           mk_predBinop_term       (term_of_var v)                                (term_of_atom a1)
708                                   (term_of_pred_binop op)                                (term_of_atom a2)
709                                   (term_of_atom a1)      | ElementCheck (ty, subop, var, atom) ->
710                                   (term_of_atom a2)           mk_elementCheck_term (term_of_ty ty)
711                                  (term_of_subop subop)
712                                  (term_of_var var)
713                                  (term_of_atom atom)
714    
715  let pred_of_term t =  let pred_of_term t =
716     if is_predNop_term t then     if is_isMutable_term t then
717        let v, op = dest_predNop_term t in        IsMutable (var_of_term (dest_isMutable_term t))
718           PredNop           (var_of_term v)     else if is_reserve_term t then
719                             (pred_nop_of_term op)        let a1, a2 = dest_reserve_term t in
720     else if is_predUnop_term t then           Reserve           (atom_of_term a1)
721        let v, op, a = dest_predUnop_term t in                             (atom_of_term a2)
722           PredUnop          (var_of_term v)     else if is_boundsCheck_term t then
723                             (pred_unop_of_term op)        let subop, var, a1, a2 = dest_boundsCheck_term t in
724                             (atom_of_term a)           BoundsCheck       (subop_of_term subop)
725     else if is_predBinop_term t then                             (var_of_term var)
       let v, op, a1, a2 = dest_predBinop_term t in  
          PredBinop         (var_of_term v)  
                            (pred_binop_of_term op)  
726                             (atom_of_term a1)                             (atom_of_term a1)
727                             (atom_of_term a2)                             (atom_of_term a2)
728       else if is_elementCheck_term t then
729          let ty, subop, var, atom = dest_elementCheck_term t in
730             ElementCheck      (ty_of_term ty)
731                               (subop_of_term subop)
732                               (var_of_term var)
733                               (atom_of_term atom)
734    
735     else     else
736        raise (RefineError ("pred_of_term", StringTermError        raise (RefineError ("pred_of_term", StringTermError

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

  ViewVC Help
Powered by ViewVC 1.1.26