/[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 3562 by emre, Wed Apr 3 08:37:31 2002 UTC revision 3563 by emre, Fri Apr 5 01:16:49 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. *)
102    
103    declare rawIntOfLabelOp{ 'int_precision; 'int_signed }
104    
105  (*  (*
106   * Binary operations.   * Binary operations.
107   *)   *)
# Line 220  Line 224 
224  declare subop{ 'sub_block; 'sub_value; 'sub_index; 'sub_script }  declare subop{ 'sub_block; 'sub_value; 'sub_index; 'sub_script }
225    
226  (*  (*
227     * Fields (frame labels).
228     *)
229    
230    declare frameLabel{ 'label1; 'label2; 'label3 }
231    
232    (*
233   * Normal values.   * Normal values.
234   *)   *)
235    
# Line 228  Line 238 
238  declare atomEnum{ 'int1; 'int2 }  declare atomEnum{ 'int1; 'int2 }
239  declare atomRawInt{ 'int_precision; 'int_signed; 'num }  declare atomRawInt{ 'int_precision; 'int_signed; 'num }
240  declare atomFloat{ 'float_precision; 'num }  declare atomFloat{ 'float_precision; 'num }
241    declare atomLabel{ 'frame_label }
242  declare atomConst{ 'ty; 'ty_var; 'int }  declare atomConst{ 'ty; 'ty_var; 'int }
243  declare atomVar{ 'var }  declare atomVar{ 'var }
244    
# Line 240  Line 251 
251  declare allocArray{ 'ty; 'atom_list }  declare allocArray{ 'ty; 'atom_list }
252  declare allocVArray{ 'ty; 'sub_index; 'atom1; 'atom2 }  declare allocVArray{ 'ty; 'sub_index; 'atom1; 'atom2 }
253  declare allocMalloc{ 'ty; 'atom }  declare allocMalloc{ 'ty; 'atom }
254    declare allocFrame{ 'var }
255    
256  (*  (*
257   * Tail calls / operations.   * Tail calls / operations.
# Line 299  Line 311 
311  (* Function application. *)  (* Function application. *)
312    
313  declare letExt{ 'ty1; 'string; 'ty2; 'atom_list; var. 'exp['var] }  declare letExt{ 'ty1; 'string; 'ty2; 'atom_list; var. 'exp['var] }
314  declare tailCall{ 'var; 'atom_list }  declare tailCall{ 'label; 'var; 'atom_list }
315  declare specialCall{ 'tailop }  declare specialCall{ 'label; 'tailop }
316    
317  (* Control. *)  (* Control. *)
318    
319  declare matchCase{ 'set; 'exp }  declare matchCase{ 'label; 'set; 'exp }
320  declare matchExp{ 'atom; 'matchCase_list }  declare matchExp{ 'atom; 'matchCase_list }
321  declare typeCase{ 'atom1; 'atom2; 'var1; 'var2; 'exp1; 'exp2 }  declare typeCase{ 'atom1; 'atom2; 'var1; 'var2; 'exp1; 'exp2 }
322    
# Line 321  Line 333 
333    
334  (* Assertions. *)  (* Assertions. *)
335    
336  declare call{ 'var; 'atom_option_list; 'exp }  declare call{ 'label; 'var; 'atom_option_list; 'exp }
337  declare assertExp{ 'label; 'pred; 'exp }  declare assertExp{ 'label; 'pred; 'exp }
338    
339  (* Debugging. *)  (* Debugging. *)
# Line 438  Line 450 
450     pointerOfRawIntOp{ 'int_precision; 'int_signed } =     pointerOfRawIntOp{ 'int_precision; 'int_signed } =
451     `"PointerOfRawIntOp(" slot{'int_precision} `"," slot{'int_signed} `")"     `"PointerOfRawIntOp(" slot{'int_precision} `"," slot{'int_signed} `")"
452    
453    (* Pointer operations. *)
454    
455    dform rawIntOfLabelOp_df : except_mode[src] ::
456       rawIntOfLabelOp{ 'int_precision; 'int_signed } =
457       `"RawIntOfLabelOp(" slot{'int_precision} `"," slot{'int_signed} `")"
458    
459  (*  (*
460   * Binary operations.   * Binary operations.
461   *)   *)
# Line 713  Line 731 
731     slot{'sub_index} `"," slot{'sub_script} `")"     slot{'sub_index} `"," slot{'sub_script} `")"
732    
733  (*  (*
734     * Fields (frame labels).
735     *)
736    
737    dform frameLabel_df : except_mode[src] ::
738       frameLabel{ 'label1; 'label2; 'label3 } =
739       `"FrameLabel(" slot{'label1} `"," slot{'label2} `","
740       slot{'label3} `")"
741    
742    (*
743   * Normal values.   * Normal values.
744   *)   *)
745    
# Line 732  Line 759 
759  dform atomFloat_df : except_mode[src] ::  dform atomFloat_df : except_mode[src] ::
760     atomFloat{ 'float_precision; 'num } =     atomFloat{ 'float_precision; 'num } =
761     `"AtomFloat(" slot{'float_precision} `", " slot{'num} `")"     `"AtomFloat(" slot{'float_precision} `", " slot{'num} `")"
762    dform atomLabel_df : except_mode[src] ::
763       atomLabel{ 'frame_label } =
764       `"AtomLabel(" slot{'frame_label} `")"
765  dform atomConst_df : except_mode[src] ::  dform atomConst_df : except_mode[src] ::
766     atomConst{ 'ty; 'ty_var; 'int } =     atomConst{ 'ty; 'ty_var; 'int } =
767     `"AtomConst(" slot{'ty} `", " slot{'ty_var} `", " slot{'int} `")"     `"AtomConst(" slot{'ty} `", " slot{'ty_var} `", " slot{'int} `")"
# Line 759  Line 789 
789  dform allocMalloc_df : except_mode[src] ::  dform allocMalloc_df : except_mode[src] ::
790     allocMalloc{ 'ty; 'atom } =     allocMalloc{ 'ty; 'atom } =
791     `"AllocMalloc(" slot{'ty} `"," slot{'atom} `")"     `"AllocMalloc(" slot{'ty} `"," slot{'atom} `")"
792    dform allocFrame_df : except_mode[src] ::
793       allocFrame{ 'var } =
794       `"AllocFrame(" slot{'var} `")"
795    
796  (*  (*
797   * Tail calls / operations.   * Tail calls / operations.
# Line 872  Line 905 
905     `"LetExt(" slot{'ty1} `"," slot{'string} `"," slot{'ty2} `","     `"LetExt(" slot{'ty1} `"," slot{'string} `"," slot{'ty2} `","
906     slot{'atom_list} `"," slot{'var} `". " slot{'exp} `")"     slot{'atom_list} `"," slot{'var} `". " slot{'exp} `")"
907  dform tailCall_df : except_mode[src] ::  dform tailCall_df : except_mode[src] ::
908     tailCall{ 'var; 'atom_list } =     tailCall{ 'label; 'var; 'atom_list } =
909     `"TailCall(" slot{'var} `"," slot{'atom_list} `")"     `"TailCall(" slot{'label} `"," slot{'var} `"," slot{'atom_list} `")"
910  dform specialCall_df : except_mode[src] ::  dform specialCall_df : except_mode[src] ::
911     specialCall{ 'tailop } =     specialCall{ 'label; 'tailop } =
912     `"SpeciaCall(" slot{'tailop} `")"     `"SpeciaCall(" slot{'label} `"," slot{'tailop} `")"
913    
914  (* Control. *)  (* Control. *)
915    
916  dform matchCase_df : except_mode[src] ::  dform matchCase_df : except_mode[src] ::
917     matchCase{ 'set; 'exp } =     matchCase{ 'label; 'set; 'exp } =
918     `"MatchCase(" slot{'set} `"," slot{'exp} `")"     `"MatchCase(" slot{'label} `"," slot{'set} `"," slot{'exp} `")"
919  dform matchExp_df : except_mode[src] ::  dform matchExp_df : except_mode[src] ::
920     matchExp{ 'atom; 'matchCase_list } =     matchExp{ 'atom; 'matchCase_list } =
921     `"MatchExp(" slot{'atom} `"," slot{'matchCase_list} `")"     `"MatchExp(" slot{'atom} `"," slot{'matchCase_list} `")"
# Line 920  Line 953 
953  (* Assertions. *)  (* Assertions. *)
954    
955  dform call_df : except_mode[src] ::  dform call_df : except_mode[src] ::
956     call{ 'var; 'atom_option_list; 'exp } =     call{ 'label; 'var; 'atom_option_list; 'exp } =
957     `"Call(" slot{'var} `"," slot{'atom_option_list} `"," slot{'exp} `")"     `"Call(" slot{'label} `","
958       slot{'var} `"," slot{'atom_option_list} `"," slot{'exp} `")"
959  dform assertExp_df : except_mode[src] ::  dform assertExp_df : except_mode[src] ::
960     assertExp{ 'label; 'pred; 'exp } =     assertExp{ 'label; 'pred; 'exp } =
961     `"AssertExp(" slot{'label} `"," slot{'pred} `"," slot{'exp} `")"     `"AssertExp(" slot{'label} `"," slot{'pred} `"," slot{'exp} `")"
# Line 1094  Line 1128 
1128  let mk_pointerOfRawIntOp_term = mk_dep0_dep0_term pointerOfRawIntOp_opname  let mk_pointerOfRawIntOp_term = mk_dep0_dep0_term pointerOfRawIntOp_opname
1129  let dest_pointerOfRawIntOp_term = dest_dep0_dep0_term pointerOfRawIntOp_opname  let dest_pointerOfRawIntOp_term = dest_dep0_dep0_term pointerOfRawIntOp_opname
1130    
1131    let rawIntOfLabelOp_term = << rawIntOfLabelOp{ 'int_precision; 'int_signed } >>
1132    let rawIntOfLabelOp_opname = opname_of_term rawIntOfLabelOp_term
1133    let is_rawIntOfLabelOp_term = is_dep0_dep0_term rawIntOfLabelOp_opname
1134    let mk_rawIntOfLabelOp_term = mk_dep0_dep0_term rawIntOfLabelOp_opname
1135    let dest_rawIntOfLabelOp_term = dest_dep0_dep0_term rawIntOfLabelOp_opname
1136    
1137  (*  (*
1138   * Binary operations.   * Binary operations.
1139   *)   *)
# Line 1512  Line 1552 
1552  let dest_subop_term = dest_4_dep0_term subop_opname  let dest_subop_term = dest_4_dep0_term subop_opname
1553    
1554  (*  (*
1555     * Fields (frame labels).
1556     *)
1557    
1558    let frameLabel_term = << frameLabel{ 'label1; 'label2; 'label3 } >>
1559    let frameLabel_opname = opname_of_term frameLabel_term
1560    let is_frameLabel_term = is_dep0_dep0_dep0_term frameLabel_opname
1561    let mk_frameLabel_term = mk_dep0_dep0_dep0_term frameLabel_opname
1562    let dest_frameLabel_term = dest_dep0_dep0_dep0_term frameLabel_opname
1563    
1564    (*
1565   * Normal values.   * Normal values.
1566   *)   *)
1567    
# Line 1545  Line 1595 
1595  let mk_atomFloat_term = mk_dep0_dep0_term atomFloat_opname  let mk_atomFloat_term = mk_dep0_dep0_term atomFloat_opname
1596  let dest_atomFloat_term = dest_dep0_dep0_term atomFloat_opname  let dest_atomFloat_term = dest_dep0_dep0_term atomFloat_opname
1597    
1598    let atomLabel_term = << atomLabel{ 'frame_label } >>
1599    let atomLabel_opname = opname_of_term atomLabel_term
1600    let is_atomLabel_term = is_dep0_term atomLabel_opname
1601    let mk_atomLabel_term = mk_dep0_term atomLabel_opname
1602    let dest_atomLabel_term = dest_dep0_term atomLabel_opname
1603    
1604  let atomConst_term = << atomConst{ 'ty; 'ty_var; 'int } >>  let atomConst_term = << atomConst{ 'ty; 'ty_var; 'int } >>
1605  let atomConst_opname = opname_of_term atomConst_term  let atomConst_opname = opname_of_term atomConst_term
1606  let is_atomConst_term = is_dep0_dep0_dep0_term atomConst_opname  let is_atomConst_term = is_dep0_dep0_dep0_term atomConst_opname
# Line 1591  Line 1647 
1647  let mk_allocMalloc_term = mk_dep0_dep0_term allocMalloc_opname  let mk_allocMalloc_term = mk_dep0_dep0_term allocMalloc_opname
1648  let dest_allocMalloc_term = dest_dep0_dep0_term allocMalloc_opname  let dest_allocMalloc_term = dest_dep0_dep0_term allocMalloc_opname
1649    
1650    let allocFrame_term = << allocFrame{ 'var } >>
1651    let allocFrame_opname = opname_of_term allocFrame_term
1652    let is_allocFrame_term = is_dep0_term allocFrame_opname
1653    let mk_allocFrame_term = mk_dep0_term allocFrame_opname
1654    let dest_allocFrame_term = dest_dep0_term allocFrame_opname
1655    
1656  (*  (*
1657   * Tail calls / operations.   * Tail calls / operations.
1658   *)   *)
# Line 1744  Line 1806 
1806  let mk_letExt_term = mk_4_dep0_1_dep1_term letExt_opname  let mk_letExt_term = mk_4_dep0_1_dep1_term letExt_opname
1807  let dest_letExt_term = dest_4_dep0_1_dep1_term letExt_opname  let dest_letExt_term = dest_4_dep0_1_dep1_term letExt_opname
1808    
1809  let tailCall_term = << tailCall{ 'var; 'atom_list } >>  let tailCall_term = << tailCall{ 'label; 'var; 'atom_list } >>
1810  let tailCall_opname = opname_of_term tailCall_term  let tailCall_opname = opname_of_term tailCall_term
1811  let is_tailCall_term = is_dep0_dep0_term tailCall_opname  let is_tailCall_term = is_dep0_dep0_dep0_term tailCall_opname
1812  let mk_tailCall_term = mk_dep0_dep0_term tailCall_opname  let mk_tailCall_term = mk_dep0_dep0_dep0_term tailCall_opname
1813  let dest_tailCall_term = dest_dep0_dep0_term tailCall_opname  let dest_tailCall_term = dest_dep0_dep0_dep0_term tailCall_opname
1814    
1815  let specialCall_term = << specialCall{ 'tailop } >>  let specialCall_term = << specialCall{ 'label; 'tailop } >>
1816  let specialCall_opname = opname_of_term specialCall_term  let specialCall_opname = opname_of_term specialCall_term
1817  let is_specialCall_term = is_dep0_term specialCall_opname  let is_specialCall_term = is_dep0_dep0_term specialCall_opname
1818  let mk_specialCall_term = mk_dep0_term specialCall_opname  let mk_specialCall_term = mk_dep0_dep0_term specialCall_opname
1819  let dest_specialCall_term = dest_dep0_term specialCall_opname  let dest_specialCall_term = dest_dep0_dep0_term specialCall_opname
1820    
1821  (* Control. *)  (* Control. *)
1822    
1823  let matchCase_term = << matchCase{ 'set; 'exp } >>  let matchCase_term = << matchCase{ 'label; 'set; 'exp } >>
1824  let matchCase_opname = opname_of_term matchCase_term  let matchCase_opname = opname_of_term matchCase_term
1825  let is_matchCase_term = is_dep0_dep0_term matchCase_opname  let is_matchCase_term = is_dep0_dep0_dep0_term matchCase_opname
1826  let mk_matchCase_term = mk_dep0_dep0_term matchCase_opname  let mk_matchCase_term = mk_dep0_dep0_dep0_term matchCase_opname
1827  let dest_matchCase_term = dest_dep0_dep0_term matchCase_opname  let dest_matchCase_term = dest_dep0_dep0_dep0_term matchCase_opname
1828    
1829  let matchExp_term = << matchExp{ 'atom; 'matchCase_list } >>  let matchExp_term = << matchExp{ 'atom; 'matchCase_list } >>
1830  let matchExp_opname = opname_of_term matchExp_term  let matchExp_opname = opname_of_term matchExp_term
# Line 1817  Line 1879 
1879    
1880  (* Assertions. *)  (* Assertions. *)
1881    
1882  let call_term = << call{ 'var; 'atom_option_list; 'exp } >>  let call_term = << call{ 'label; 'var; 'atom_option_list; 'exp } >>
1883  let call_opname = opname_of_term call_term  let call_opname = opname_of_term call_term
1884  let is_call_term = is_dep0_dep0_dep0_term call_opname  let is_call_term = is_4_dep0_term call_opname
1885  let mk_call_term = mk_dep0_dep0_dep0_term call_opname  let mk_call_term = mk_4_dep0_term call_opname
1886  let dest_call_term = dest_dep0_dep0_dep0_term call_opname  let dest_call_term = dest_4_dep0_term call_opname
1887    
1888  let assertExp_term = << assertExp{ 'label; 'pred; 'exp } >>  let assertExp_term = << assertExp{ 'label; 'pred; 'exp } >>
1889  let assertExp_opname = opname_of_term assertExp_term  let assertExp_opname = opname_of_term assertExp_term

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

  ViewVC Help
Powered by ViewVC 1.1.26