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

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

Parent Directory Parent Directory | Revision Log Revision Log


Revision 3563 - (hide 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 emre 3479 (*
2     * Functional Intermediate Representation formalized in MetaPRL.
3     *
4     * Operations for converting between MC Fir expressions and MetaPRL terms.
5     *
6     * ----------------------------------------------------------------
7     *
8 emre 3550 * Copyright (C) 2002 Brian Emre Aydemir, Caltech
9     *
10 emre 3479 * 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 emre 3550 * Convert to and from subscripting terms.
59 emre 3479 *)
60    
61 emre 3550 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 emre 3479 val term_of_subop : subop -> term
74     val subop_of_term : term -> subop
75    
76     (*
77 emre 3563 * 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 emre 3479 * 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 emre 3550 * 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 emre 3479 * 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 emre 3562
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