/[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 3562 by emre, Wed Apr 3 08:37:31 2002 UTC revision 3563 by emre, Fri Apr 5 01:16:49 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. *)
125        | RawIntOfLabelOp (p, s) ->
126             mk_rawIntOfLabelOp_term    (term_of_int_precision p)
127                                        (term_of_int_signed s)
128    
129  let unop_of_term t =  let unop_of_term t =
130    
131     (* Identity (polymorhpic). *)     (* Identity (polymorhpic). *)
# Line 210  Line 215 
215           PointerOfRawIntOp (int_precision_of_term p)           PointerOfRawIntOp (int_precision_of_term p)
216                             (int_signed_of_term s)                             (int_signed_of_term s)
217    
218       (* Pointer operations. *)
219       else if is_rawIntOfLabelOp_term t then
220          let p, s = dest_rawIntOfLabelOp_term t in
221             RawIntOfLabelOp   (int_precision_of_term p)
222                               (int_signed_of_term s)
223    
224     else     else
225        raise (RefineError ("unop_of_term", StringTermError        raise (RefineError ("unop_of_term", StringTermError
226              ("not a unop", t)))              ("not a unop", t)))
# Line 579  Line 590 
590              ("not a subop", t)))              ("not a subop", t)))
591    
592  (*  (*
593     * Convert to and from frame_label.
594     *)
595    
596    let term_of_frame_label (lbl1, lbl2, lbl3) =
597       mk_frameLabel_term   (term_of_label lbl1)
598                            (term_of_label lbl2)
599                            (term_of_label lbl3)
600    
601    let frame_label_of_term t =
602       if is_frameLabel_term t then
603          let lbl1, lbl2, lbl3 = dest_frameLabel_term t in
604             (label_of_term lbl1),
605             (label_of_term lbl2),
606             (label_of_term lbl3)
607    
608       else
609          raise (RefineError ("frame_label_of_term", StringTermError
610                ("not a frame_label", t)))
611    
612    (*
613   * Convert to and from atom.   * Convert to and from atom.
614   *)   *)
615    
# Line 597  Line 628 
628      | AtomFloat f ->      | AtomFloat f ->
629           mk_atomFloat_term    (term_of_float_precision (Rawfloat.precision f))           mk_atomFloat_term    (term_of_float_precision (Rawfloat.precision f))
630                                (number_term_of_rawfloat f)                                (number_term_of_rawfloat f)
631        | AtomLabel flbl ->
632             mk_atomLabel_term    (term_of_frame_label flbl)
633      | AtomConst (t, tv, i) ->      | AtomConst (t, tv, i) ->
634           mk_atomConst_term    (term_of_ty t)           mk_atomConst_term    (term_of_ty t)
635                                (term_of_ty_var tv)                                (term_of_ty_var tv)
# Line 620  Line 653 
653     else if is_atomFloat_term t then     else if is_atomFloat_term t then
654        let p, f = dest_atomFloat_term t in        let p, f = dest_atomFloat_term t in
655           AtomFloat (rawfloat_of_number_term (float_precision_of_term p) f)           AtomFloat (rawfloat_of_number_term (float_precision_of_term p) f)
656       else if is_atomLabel_term t then
657          AtomLabel (frame_label_of_term (dest_atomLabel_term t))
658     else if is_atomConst_term t then     else if is_atomConst_term t then
659        let t, tv, i = dest_atomConst_term t in        let t, tv, i = dest_atomConst_term t in
660           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 656  Line 691 
691      | AllocMalloc (t, a) ->      | AllocMalloc (t, a) ->
692           mk_allocMalloc_term  (term_of_ty t)           mk_allocMalloc_term  (term_of_ty t)
693                                (term_of_atom a)                                (term_of_atom a)
694        | AllocFrame v ->
695             mk_allocFrame_term   (term_of_var v)
696    
697  let alloc_op_of_term t =  let alloc_op_of_term t =
698     if is_allocTuple_term t then     if is_allocTuple_term t then
# Line 683  Line 720 
720        let t, a = dest_allocMalloc_term t in        let t, a = dest_allocMalloc_term t in
721           AllocMalloc (ty_of_term t)           AllocMalloc (ty_of_term t)
722                       (atom_of_term a)                       (atom_of_term a)
723       else if is_allocFrame_term t then
724          AllocFrame (var_of_term (dest_allocFrame_term t))
725    
726     else     else
727        raise (RefineError ("term_of_alloc_op", StringTermError        raise (RefineError ("term_of_alloc_op", StringTermError
# Line 886  Line 925 
925    
926  (* Helper functions. *)  (* Helper functions. *)
927    
928  let rec term_of_case (set, expr) =  let rec term_of_case (lbl, set, expr) =
929     mk_matchCase_term (term_of_set set) (term_of_exp expr)     mk_matchCase_term (term_of_label lbl) (term_of_set set) (term_of_exp expr)
930    
931  and case_of_term t =  and case_of_term t =
932     if is_matchCase_term t then     if is_matchCase_term t then
933        let set, expr = dest_matchCase_term t in        let lbl, set, expr = dest_matchCase_term t in
934           (set_of_term set), (exp_of_term expr)           (label_of_term lbl), (set_of_term set), (exp_of_term expr)
935     else     else
936        raise (RefineError ("case of term", StringTermError        raise (RefineError ("case of term", StringTermError
937              ("not a match case (set * exp)", t)))              ("not a match case (set * exp)", t)))
# Line 925  Line 964 
964                                   (term_of_list term_of_atom al)                                   (term_of_list term_of_atom al)
965                                   (string_of_var v)                                   (string_of_var v)
966                                   (term_of_exp expr)                                   (term_of_exp expr)
967      | TailCall (v, al) ->      | TailCall (lbl, v, al) ->
968           mk_tailCall_term        (term_of_var v)           mk_tailCall_term        (term_of_label lbl)
969                                     (term_of_var v)
970                                   (term_of_list term_of_atom al)                                   (term_of_list term_of_atom al)
971      | SpecialCall op ->      | SpecialCall (lbl, op) ->
972           mk_specialCall_term     (term_of_tailop op)           mk_specialCall_term     (term_of_label lbl)
973                                     (term_of_tailop op)
974    
975        (* Control. *)        (* Control. *)
976      | Match (a, cases) ->      | Match (a, cases) ->
# Line 983  Line 1024 
1024                                   (term_of_exp expr)                                   (term_of_exp expr)
1025    
1026        (* Assertions. *)        (* Assertions. *)
1027      | Call (v, aol, expr) ->      | Call (lbl, v, aol, expr) ->
1028           mk_call_term         (term_of_var v)           mk_call_term         (term_of_label lbl)
1029                                  (term_of_var v)
1030                                (term_of_list (term_of_option term_of_atom) aol)                                (term_of_list (term_of_option term_of_atom) aol)
1031                                (term_of_exp expr)                                (term_of_exp expr)
1032      | Assert (lbl, p, expr) ->      | Assert (lbl, p, expr) ->
# Line 1026  Line 1068 
1068                             (list_of_term atom_of_term al)                             (list_of_term atom_of_term al)
1069                             (exp_of_term expr)                             (exp_of_term expr)
1070     else if is_tailCall_term t then     else if is_tailCall_term t then
1071        let v, al = dest_tailCall_term t in        let lbl, v, al = dest_tailCall_term t in
1072           TailCall          (var_of_term v)           TailCall          (label_of_term lbl)
1073                               (var_of_term v)
1074                             (list_of_term atom_of_term al)                             (list_of_term atom_of_term al)
1075     else if is_specialCall_term t then     else if is_specialCall_term t then
1076           SpecialCall       (tailop_of_term (dest_specialCall_term t))        let lbl, tailop = dest_specialCall_term t in
1077             SpecialCall       (label_of_term lbl)
1078                               (tailop_of_term tailop)
1079    
1080     (* Control. *)     (* Control. *)
1081     else if is_matchExp_term t then     else if is_matchExp_term t then
# Line 1092  Line 1137 
1137    
1138     (* Assertions. *)     (* Assertions. *)
1139     else if is_call_term t then     else if is_call_term t then
1140        let v, aol, expr = dest_call_term t in        let lbl, v, aol, expr = dest_call_term t in
1141           Call              (var_of_term v)           Call              (label_of_term lbl)
1142                               (var_of_term v)
1143                             (list_of_term (option_of_term atom_of_term) aol)                             (list_of_term (option_of_term atom_of_term) aol)
1144                             (exp_of_term expr)                             (exp_of_term expr)
1145     else if is_assertExp_term t then     else if is_assertExp_term t then

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

  ViewVC Help
Powered by ViewVC 1.1.26