/[mojave]/metaprl/library/nuprl5.ml
ViewVC logotype

Contents of /metaprl/library/nuprl5.ml

Parent Directory Parent Directory | Revision Log Revision Log


Revision 7563 - (show annotations) (download)
Thu Jul 7 02:30:10 2005 UTC (16 years ago) by nogin
File size: 8248 byte(s)
This is a huge commit that is mostly no-op:

- Updated the standard preamble text to point to the correct location for the
  documentation and to avoid mentioning Nuprl.

- Changed "Nuprl-Light" -> "MetaPRL" in a few places (amazingly, we still had
  those).

- Split the Nuprl_font file into Mpfont and Mpsymbols.

- Protected a few display forms in ITT with a "doc docoff".

1 (*
2 * This file is part of MetaPRL, a modular, higher order
3 * logical framework that provides a logical programming
4 * environment for OCaml and other languages.
5 *
6 * See the file doc/htmlman/default.html or visit http://metaprl.org/
7 * for more information.
8 *
9 * Copyright (C) 1998 Lori Lorigo, Richard Eaton, Cornell University
10 *
11 * This program is free software; you can redistribute it and/or
12 * modify it under the terms of the GNU General Public License
13 * as published by the Free Software Foundation; either version 2
14 * of the License, or (at your option) any later version.
15 *
16 * This program is distributed in the hope that it will be useful,
17 * but WITHOUT ANY WARRANTY; without even the implied warranty of
18 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
19 * GNU General Public License for more details.
20 *
21 * You should have received a copy of the GNU General Public License
22 * along with this program; if not, write to the Free Software
23 * Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA.
24 *
25 * Authors: Lori Lorigo, Richard Eaton
26 *)
27
28 open Lm_debug
29
30 open Term_sig
31 open Refiner.Refiner.Term
32 open Refiner.Refiner.TermType
33 open Opname
34
35 let _ =
36 show_loading "Loading Nuprl5%t"
37
38 let nuprl5_opname = mk_opname "!nuprl5_implementation!" nil_opname
39 let nuprl5_opname_p opname = opname = nuprl5_opname
40
41 (* parameter mapping *)
42 let time_opname = mk_opname "time" nil_opname
43 let bool_opname = mk_opname "bool" nil_opname
44
45 let make_bool_parameter b =
46 make_param (ParamList
47 [(make_param (Token bool_opname)); (make_param (Number (Lm_num.num_of_int (if b then 1 else 0))))])
48
49 let make_time_parameter time =
50 make_param (ParamList
51 [(make_param (Token time_opname)); (make_param (Number time))])
52
53 let time_parameter_p p =
54 match (dest_param p) with
55 ParamList [h; a; b] ->
56 (match (dest_param h) with
57 Token s ->
58 if Opname.eq s time_opname then
59 (match (dest_param a) with
60 Number i ->
61 (match (dest_param b) with
62 Number i -> true
63 | _ -> false)
64 | _ -> false)
65 else
66 false
67 | _ ->
68 false)
69 | _ -> false
70
71 let bool_parameter_p p =
72 match (dest_param p) with
73 ParamList [h; v] ->
74 (match (dest_param h) with
75 Token s ->
76 if Opname.eq s bool_opname then
77 (match (dest_param v) with
78 Number i when Lm_num.is_integer_num i -> let i = Lm_num.int_of_num i in (i = 1 || i = 0)
79 | _ -> false)
80 else
81 false
82 | _ -> false)
83 | _ -> false
84
85 let destruct_time_parameter p =
86 match (dest_param p) with
87 ParamList [h; n] ->
88 (match (dest_param h) with
89 Token s ->
90 (if Opname.eq s time_opname then
91 (match (dest_param n) with
92 Number i -> i
93 | _ -> raise (Invalid_argument "destruct_time_parameter_b"))
94 else
95 raise (Invalid_argument "destruct_time_parameter_c"))
96 | _ -> raise (Invalid_argument "destruct_time_parameter_d"))
97 | _ -> raise (Invalid_argument "destruct_time_parameter_e")
98
99
100 let destruct_bool_parameter p =
101 match (dest_param p) with
102 ParamList [h; v] ->
103 (match (dest_param h) with
104 Token s ->
105 if Opname.eq s bool_opname then
106 (match (dest_param v) with
107 Number i when Lm_num.is_integer_num i -> let i = Lm_num.int_of_num i in i = 1
108 | _ -> raise (Invalid_argument "destruct_bool_parameter"))
109 else raise (Invalid_argument "destruct_bool_parameter")
110 | _ -> raise (Invalid_argument "destruct_bool_parameter"))
111 | _ -> raise (Invalid_argument "destruct_bool_parameter")
112
113
114 (* common terms *)
115
116 let mk_nuprl5_op pl = mk_op nuprl5_opname pl
117 let mk_nuprl5_simple_op s = mk_op nuprl5_opname [(make_param (Token (mk_opname s nil_opname)))]
118
119 let nuprl_is_op_term opname term =
120 match Lib_term.dest_term term with
121 { term_op = term_op'; term_terms = _
122 } when term_op' = opname -> true
123 | _ -> false
124
125 let nuprl_is_not_term = nuprl_is_op_term (mk_nuprl5_simple_op "not")
126 let nuprl_is_exists_term = nuprl_is_op_term (mk_nuprl5_simple_op "exists")
127 let nuprl_is_or_term = nuprl_is_op_term (mk_nuprl5_simple_op "or")
128 let nuprl_is_and_term = nuprl_is_op_term (mk_nuprl5_simple_op "and")
129 let nuprl_is_implies_term = nuprl_is_op_term (mk_nuprl5_simple_op "implies")
130 let nuprl_is_all_term = nuprl_is_op_term (mk_nuprl5_simple_op "all")
131
132 let variable_opname = mk_opname "variable" nil_opname
133
134 let nuprl_is_var_term term =
135 match Lib_term.dest_term term with
136 { term_op = term_op'; term_terms = _ } ->
137 match dest_op term_op' with
138 {op_name = opname; op_params = [p1; p2] } ->
139 (match (dest_param p1) with
140 Token v when Opname.eq v variable_opname -> true
141 | _ -> false)
142 | _ -> false
143
144 let nuprl_dest_var term =
145 match Lib_term.dest_term term with
146 { term_op = term_op'; term_terms = [] } ->
147 (match dest_op term_op' with
148 {op_name = opname; op_params = [p1; p2]} ->
149 (match (dest_param p2) with
150 Var p -> p
151 | x -> failwith "nuprl_dest_var")
152 | x -> failwith "nuprl_dest_var")
153 | x -> failwith "nuprl_dest_var"
154
155 let nuprl_dest_all term =
156 match Lib_term.dest_term term with
157 { term_op = term_op'; term_terms = [tp ; prop] }
158 when term_op' = (mk_nuprl5_simple_op "all") ->
159 (match dest_bterm tp with
160 { bvars = []; bterm = t1 } ->
161 (match dest_bterm prop with { bvars = [x]; bterm = t2 } ->
162 x, t1, t2
163 | _ -> failwith "nuprl_dest_all")
164 | _ -> failwith "nuprl_dest_all")
165 | _ -> failwith "nuprl_dest_all"
166
167 let nuprl_dest_exists term =
168 match Lib_term.dest_term term with
169 { term_op = term_op'; term_terms = [tp ; prop] }
170 when term_op' = (mk_nuprl5_simple_op "exists") ->
171 (match dest_bterm tp with
172 { bvars = []; bterm = t1 } ->
173 (match dest_bterm prop with { bvars = [x]; bterm = t2 } ->
174 x, t1, t2
175 | _ -> failwith "nuprl_dest_exists")
176 | _ -> failwith "nuprl_dest_exists")
177 | _ -> failwith "nuprl_dest_exists"
178
179
180 let nuprl_dest_not term =
181 match Lib_term.dest_term term with
182 { term_op = term_op'; term_terms = [prop] }
183 when term_op' = (mk_nuprl5_simple_op "not") ->
184 (match dest_bterm prop with
185 { bvars = []; bterm = t } ->
186 t
187 | _ -> failwith "nuprl_dest_not")
188 | _ -> failwith "nuprl_dest_not"
189
190
191 let nuprl_dest_or term =
192 match Lib_term.dest_term term with
193 { term_op = term_op'; term_terms = [left; right] }
194 when term_op' = (mk_nuprl5_simple_op "or") ->
195 (match dest_bterm left with
196 { bvars = []; bterm = t1 } ->
197 (match dest_bterm right with { bvars = []; bterm = t2 } ->
198 t1, t2
199 | _ -> failwith "nuprl_dest_or")
200 | _ -> failwith "nuprl_dest_or")
201 | _ -> failwith "nuprl_dest_or"
202
203
204 let nuprl_dest_implies term =
205 match Lib_term.dest_term term with
206 { term_op = term_op'; term_terms = [tp; prop] }
207 when term_op' = (mk_nuprl5_simple_op "implies") ->
208 (match dest_bterm tp with
209 { bvars = []; bterm = t1 } ->
210 (match dest_bterm prop with { bvars = []; bterm = t2 } ->
211 t1, t2
212 | _ -> failwith "nuprl_dest_implies")
213 | _ -> failwith "nuprl_dest_implies")
214 | _ -> failwith "nuprl_dest_implies"
215
216
217 let nuprl_dest_and term =
218 match Lib_term.dest_term term with
219 { term_op = term_op'; term_terms = [left; right] }
220 when term_op' = (mk_nuprl5_simple_op "and") ->
221 (match dest_bterm left with
222 { bvars = []; bterm = t1 } ->
223 (match dest_bterm right with { bvars = []; bterm = t2 } ->
224 t1, t2
225 | _ -> failwith "nuprl_dest_and")
226 | _ -> failwith "nuprl_dest_and")
227 | _ -> failwith "nuprl_dest_and"
228
229
230 (*
231 let nuprl_is_all_term = function
232 { term_op = { op_name = nuprl5_opname; op_params = [make_param (Token "all")] };
233 term_terms = [{ bvars = [] }; { bvars = [_] }]
234 } -> true
235 | _ -> false
236 *)

Properties

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

  ViewVC Help
Powered by ViewVC 1.1.26