/[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 3562 - (show annotations) (download)
Wed Apr 3 08:37:31 2002 UTC (19 years, 4 months ago) by emre
File size: 3332 byte(s)
So, I've defined the compile function in Mp_mc_compile to actually
take an Fir.prog, convert the function definitions to terms,
and then back again, in one big identity operation.  The current
term representation of the FIR functions is a bit of a hack that
will need to be cleaned up if anything non-trivial is to be done.
(Each individual function is fine I hope.  It's the program as a whole
that's represented rather poorly.  It's essentially a (term SymbolTable.t),
one term for each fundef in the original Fir.prog.prog_funs.)
Though, this should be sufficient for basic testing I think.

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

Properties

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

  ViewVC Help
Powered by ViewVC 1.1.26