/[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 3562 by emre, Wed Apr 3 08:37:31 2002 UTC revision 3563 by emre, Fri Apr 5 01:16:49 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. *)
100    
101    declare rawIntOfLabelOp{ 'int_precision; 'int_signed }
102    
103  (*  (*
104   * Binary operations.   * Binary operations.
105   *)   *)
# Line 218  Line 222 
222  declare subop{ 'sub_block; 'sub_value; 'sub_index; 'sub_script }  declare subop{ 'sub_block; 'sub_value; 'sub_index; 'sub_script }
223    
224  (*  (*
225     * Fields (frame labels).
226     *)
227    
228    declare frameLabel{ 'label1; 'label2; 'label3 }
229    
230    (*
231   * Normal values.   * Normal values.
232   *)   *)
233    
# Line 226  Line 236 
236  declare atomEnum{ 'int1; 'int2 }  declare atomEnum{ 'int1; 'int2 }
237  declare atomRawInt{ 'int_precision; 'int_signed; 'num }  declare atomRawInt{ 'int_precision; 'int_signed; 'num }
238  declare atomFloat{ 'float_precision; 'num }  declare atomFloat{ 'float_precision; 'num }
239    declare atomLabel{ 'frame_label }
240  declare atomConst{ 'ty; 'ty_var; 'int }  declare atomConst{ 'ty; 'ty_var; 'int }
241  declare atomVar{ 'var }  declare atomVar{ 'var }
242    
# Line 238  Line 249 
249  declare allocArray{ 'ty; 'atom_list }  declare allocArray{ 'ty; 'atom_list }
250  declare allocVArray{ 'ty; 'sub_index; 'atom1; 'atom2 }  declare allocVArray{ 'ty; 'sub_index; 'atom1; 'atom2 }
251  declare allocMalloc{ 'ty; 'atom }  declare allocMalloc{ 'ty; 'atom }
252    declare allocFrame{ 'var }
253    
254  (*  (*
255   * Tail calls / operations.   * Tail calls / operations.
# Line 297  Line 309 
309  (* Function application. *)  (* Function application. *)
310    
311  declare letExt{ 'ty1; 'string; 'ty2; 'atom_list; var. 'exp['var] }  declare letExt{ 'ty1; 'string; 'ty2; 'atom_list; var. 'exp['var] }
312  declare tailCall{ 'var; 'atom_list }  declare tailCall{ 'label; 'var; 'atom_list }
313  declare specialCall{ 'tailop }  declare specialCall{ 'label; 'tailop }
314    
315  (* Control. *)  (* Control. *)
316    
317  declare matchCase{ 'set; 'exp }  declare matchCase{ 'label; 'set; 'exp }
318  declare matchExp{ 'atom; 'matchCase_list }  declare matchExp{ 'atom; 'matchCase_list }
319  declare typeCase{ 'atom1; 'atom2; 'var1; 'var2; 'exp1; 'exp2 }  declare typeCase{ 'atom1; 'atom2; 'var1; 'var2; 'exp1; 'exp2 }
320    
# Line 319  Line 331 
331    
332  (* Assertions. *)  (* Assertions. *)
333    
334  declare call{ 'var; 'atom_option_list; 'exp }  declare call{ 'label; 'var; 'atom_option_list; 'exp }
335  declare assertExp{ 'label; 'pred; 'exp }  declare assertExp{ 'label; 'pred; 'exp }
336    
337  (* Debugging. *)  (* Debugging. *)
# Line 457  Line 469 
469  val mk_pointerOfRawIntOp_term : term -> term -> term  val mk_pointerOfRawIntOp_term : term -> term -> term
470  val dest_pointerOfRawIntOp_term : term -> term * term  val dest_pointerOfRawIntOp_term : term -> term * term
471    
472    val rawIntOfLabelOp_term : term
473    val is_rawIntOfLabelOp_term : term -> bool
474    val mk_rawIntOfLabelOp_term : term -> term -> term
475    val dest_rawIntOfLabelOp_term : term -> term * term
476    
477  (*  (*
478   * Binary operations.   * Binary operations.
479   *)   *)
# Line 804  Line 821 
821  val dest_subop_term : term -> term * term * term * term  val dest_subop_term : term -> term * term * term * term
822    
823  (*  (*
824     * Fields (frame labels).
825     *)
826    
827    val frameLabel_term : term
828    val is_frameLabel_term : term -> bool
829    val mk_frameLabel_term : term -> term -> term -> term
830    val dest_frameLabel_term : term -> term * term * term
831    
832    (*
833   * Normal values.   * Normal values.
834   *)   *)
835    
# Line 832  Line 858 
858  val mk_atomFloat_term : term -> term -> term  val mk_atomFloat_term : term -> term -> term
859  val dest_atomFloat_term : term -> term * term  val dest_atomFloat_term : term -> term * term
860    
861    val atomLabel_term : term
862    val is_atomLabel_term : term -> bool
863    val mk_atomLabel_term : term -> term
864    val dest_atomLabel_term : term -> term
865    
866  val atomConst_term : term  val atomConst_term : term
867  val is_atomConst_term : term -> bool  val is_atomConst_term : term -> bool
868  val mk_atomConst_term : term -> term -> term -> term  val mk_atomConst_term : term -> term -> term -> term
# Line 871  Line 902 
902  val mk_allocMalloc_term : term -> term -> term  val mk_allocMalloc_term : term -> term -> term
903  val dest_allocMalloc_term : term -> term * term  val dest_allocMalloc_term : term -> term * term
904    
905    val allocFrame_term : term
906    val is_allocFrame_term : term -> bool
907    val mk_allocFrame_term : term -> term
908    val dest_allocFrame_term : term -> term
909    
910  (*  (*
911   * Tail calls / operations.   * Tail calls / operations.
912   *)   *)
# Line 1000  Line 1036 
1036    
1037  val tailCall_term : term  val tailCall_term : term
1038  val is_tailCall_term : term -> bool  val is_tailCall_term : term -> bool
1039  val mk_tailCall_term : term -> term -> term  val mk_tailCall_term : term -> term -> term -> term
1040  val dest_tailCall_term : term -> term * term  val dest_tailCall_term : term -> term * term * term
1041    
1042  val specialCall_term : term  val specialCall_term : term
1043  val is_specialCall_term : term -> bool  val is_specialCall_term : term -> bool
1044  val mk_specialCall_term : term -> term  val mk_specialCall_term : term -> term -> term
1045  val dest_specialCall_term : term -> term  val dest_specialCall_term : term -> term * term
1046    
1047  (* Control. *)  (* Control. *)
1048    
1049  val matchCase_term : term  val matchCase_term : term
1050  val is_matchCase_term : term -> bool  val is_matchCase_term : term -> bool
1051  val mk_matchCase_term : term -> term -> term  val mk_matchCase_term : term -> term -> term -> term
1052  val dest_matchCase_term : term -> term * term  val dest_matchCase_term : term -> term * term * term
1053    
1054  val matchExp_term : term  val matchExp_term : term
1055  val is_matchExp_term : term -> bool  val is_matchExp_term : term -> bool
# Line 1068  Line 1104 
1104    
1105  val call_term : term  val call_term : term
1106  val is_call_term : term -> bool  val is_call_term : term -> bool
1107  val mk_call_term : term -> term -> term -> term  val mk_call_term : term -> term -> term -> term -> term
1108  val dest_call_term : term -> term * term * term  val dest_call_term : term -> term * term * term * term
1109    
1110  val assertExp_term : term  val assertExp_term : term
1111  val is_assertExp_term : term -> bool  val is_assertExp_term : term -> bool

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

  ViewVC Help
Powered by ViewVC 1.1.26