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

Contents of /metaprl/theories/mc/mp_mc_connect_exp.mli

Parent Directory Parent Directory | Revision Log Revision Log


Revision 3563 - (show annotations) (download)
Fri Apr 5 01:16:49 2002 UTC (19 years, 4 months ago) by emre
File size: 3469 byte(s)
Updates to reflect the (ever changing) MC FIR.

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 frame_label.
78 *)
79
80 val term_of_frame_label : frame_label -> term
81 val frame_label_of_term : term -> frame_label
82
83 (*
84 * Convert to and from atom.
85 *)
86
87 val term_of_atom : atom -> term
88 val atom_of_term : term -> atom
89
90 (*
91 * Convert to and from alloc_op.
92 *)
93
94 val term_of_alloc_op : alloc_op -> term
95 val alloc_op_of_term : term -> alloc_op
96
97 (*
98 * Convert to and from tailop.
99 *)
100
101 val term_of_tailop : tailop -> term
102 val tailop_of_term : term -> tailop
103
104 (*
105 * Convert to and from predicate / assertion terms.
106 *)
107
108 val term_of_pred_nop : pred_nop -> term
109 val pred_nop_of_term : term -> pred_nop
110
111 val term_of_pred_unop : pred_unop -> term
112 val pred_unop_of_term : term -> pred_unop
113
114 val term_of_pred_binop : pred_binop -> term
115 val pred_binop_of_term : term -> pred_binop
116
117 val term_of_pred : pred -> term
118 val pred_of_term : term -> pred
119
120 (*
121 * Convert debugging info to and from terms.
122 *)
123
124 val term_of_debug_line : debug_line -> term
125 val debug_line_of_term : term -> debug_line
126
127 val term_of_debug_vars : debug_vars -> term
128 val debug_vars_of_term : term -> debug_vars
129
130 val term_of_debug_info : debug_info -> term
131 val debug_info_of_term : term -> debug_info
132
133 (*
134 * Convert to and from exp.
135 *)
136
137 val term_of_exp : exp -> term
138 val exp_of_term : term -> exp
139
140 (*
141 * Convert to and from fundef.
142 *)
143
144 val term_of_fundef : fundef -> term
145 val fundef_of_term : term -> fundef

Properties

Name Value
svn:eol-style native
svn:keywords Author Date Id Revision

  ViewVC Help
Powered by ViewVC 1.1.26