1 
(* 
2 
* Functional Intermediate Representation formalized in MetaPRL. 
3 
* 
4 
* Operations for converting between MC Fir expressions and MetaPRL terms. 
5 
* 
6 
*  
7 
* 
8 
* Copyright (C) 2002 Brian Emre Aydemir, Caltech 
9 
* 
10 
* This file is part of MetaPRL, a modular, higher order 
11 
* logical framework that provides a logical programming 
12 
* environment for OCaml and other languages. 
13 
* 
14 
* See the file doc/index.html for information on Nuprl, 
15 
* OCaml, and more information about this system. 
16 
* 
17 
* This program is free software; you can redistribute it and/or 
18 
* modify it under the terms of the GNU General Public License 
19 
* as published by the Free Software Foundation; either version 2 
20 
* of the License, or (at your option) any later version. 
21 
* 
22 
* This program is distributed in the hope that it will be useful, 
23 
* but WITHOUT ANY WARRANTY; without even the implied warranty of 
24 
* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the 
25 
* GNU General Public License for more details. 
26 
* 
27 
* You should have received a copy of the GNU General Public License 
28 
* along with this program; if not, write to the Free Software 
29 
* Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA. 
30 
* 
31 
* Author: Brian Emre Aydemir 
32 
* Email: emre@its.caltech.edu 
33 
*) 
34 

35 
(* Open MC ML namespaces. *) 
36 

37 
open Fir 
38 

39 
(* Open MetaPRL ML namespaces. *) 
40 

41 
open Refiner.Refiner.Term 
42 

43 
(* 
44 
* Convert to and from unop. 
45 
*) 
46 

47 
val term_of_unop : unop > term 
48 
val unop_of_term : term > unop 
49 

50 
(* 
51 
* Convert to and from binop. 
52 
*) 
53 

54 
val term_of_binop : binop > term 
55 
val binop_of_term : term > binop 
56 

57 
(* 
58 
* Convert to and from subscripting terms. 
59 
*) 
60 

61 
val term_of_sub_block : sub_block > term 
62 
val sub_block_of_term : term > sub_block 
63 

64 
val term_of_sub_value : sub_value > term 
65 
val sub_value_of_term : term > sub_value 
66 

67 
val term_of_sub_index : sub_index > term 
68 
val sub_index_of_term : term > sub_index 
69 

70 
val term_of_sub_script : sub_script > term 
71 
val sub_script_of_term : term > sub_script 
72 

73 
val term_of_subop : subop > term 
74 
val subop_of_term : term > subop 
75 

76 
(* 
77 
* Convert to and from atom. 
78 
*) 
79 

80 
val term_of_atom : atom > term 
81 
val atom_of_term : term > atom 
82 

83 
(* 
84 
* Convert to and from alloc_op. 
85 
*) 
86 

87 
val term_of_alloc_op : alloc_op > term 
88 
val alloc_op_of_term : term > alloc_op 
89 

90 
(* 
91 
* Convert to and from tailop. 
92 
*) 
93 

94 
val term_of_tailop : tailop > term 
95 
val tailop_of_term : term > tailop 
96 

97 
(* 
98 
* Convert to and from predicate / assertion terms. 
99 
*) 
100 

101 
val term_of_pred_nop : pred_nop > term 
102 
val pred_nop_of_term : term > pred_nop 
103 

104 
val term_of_pred_unop : pred_unop > term 
105 
val pred_unop_of_term : term > pred_unop 
106 

107 
val term_of_pred_binop : pred_binop > term 
108 
val pred_binop_of_term : term > pred_binop 
109 

110 
val term_of_pred : pred > term 
111 
val pred_of_term : term > pred 
112 

113 
(* 
114 
* Convert debugging info to and from terms. 
115 
*) 
116 

117 
val term_of_debug_line : debug_line > term 
118 
val debug_line_of_term : term > debug_line 
119 

120 
val term_of_debug_vars : debug_vars > term 
121 
val debug_vars_of_term : term > debug_vars 
122 

123 
val term_of_debug_info : debug_info > term 
124 
val debug_info_of_term : term > debug_info 
125 

126 
(* 
127 
* Convert to and from exp. 
128 
*) 
129 

130 
val term_of_exp : exp > term 
131 
val exp_of_term : term > exp 
132 

133 
(* 
134 
* Convert to and from fundef. 
135 
*) 
136 

137 
val term_of_fundef : fundef > term 
138 
val fundef_of_term : term > fundef 