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

Annotation of /metaprl/library/nuprl5.ml

Parent Directory Parent Directory | Revision Log Revision Log


Revision 7563 - (hide 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 jyh 2456 (*
2 jyh 2494 * This file is part of MetaPRL, a modular, higher order
3 jyh 2456 * logical framework that provides a logical programming
4     * environment for OCaml and other languages.
5     *
6 nogin 7563 * See the file doc/htmlman/default.html or visit http://metaprl.org/
7     * for more information.
8 jyh 2456 *
9     * Copyright (C) 1998 Lori Lorigo, Richard Eaton, Cornell University
10 nogin 3429 *
11 jyh 2456 * 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 nogin 3429 *
16 jyh 2456 * 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 nogin 3429 *
21 jyh 2456 * 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 nogin 3429 *
25 jyh 2456 * Authors: Lori Lorigo, Richard Eaton
26     *)
27    
28 nogin 4723 open Lm_debug
29 jyh 2190
30 nogin 5786 open Term_sig
31 jyh 2184 open Refiner.Refiner.Term
32 jyh 2283 open Refiner.Refiner.TermType
33 lolorigo 2041 open Opname
34    
35 jyh 2190 let _ =
36 nogin 2822 show_loading "Loading Nuprl5%t"
37 jyh 2190
38 lolorigo 2041 let nuprl5_opname = mk_opname "!nuprl5_implementation!" nil_opname
39 lolorigo 2922 let nuprl5_opname_p opname = opname = nuprl5_opname
40 lolorigo 2041
41     (* parameter mapping *)
42 nogin 6624 let time_opname = mk_opname "time" nil_opname
43     let bool_opname = mk_opname "bool" nil_opname
44 lolorigo 2041
45     let make_bool_parameter b =
46 jyh 2184 make_param (ParamList
47 nogin 6624 [(make_param (Token bool_opname)); (make_param (Number (Lm_num.num_of_int (if b then 1 else 0))))])
48 eaton 2149
49 lolorigo 2041 let make_time_parameter time =
50 jyh 2184 make_param (ParamList
51 nogin 6624 [(make_param (Token time_opname)); (make_param (Number time))])
52 lolorigo 2041
53     let time_parameter_p p =
54 nogin 6624 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 lolorigo 2041
71     let bool_parameter_p p =
72 nogin 6624 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 lolorigo 2041
85     let destruct_time_parameter p =
86 nogin 6624 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 lolorigo 2041
99 eaton 2149
100 lolorigo 2041 let destruct_bool_parameter p =
101 nogin 6624 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 lolorigo 2041
113 lolorigo 2922
114 lolorigo 2041 (* common terms *)
115    
116 lolorigo 2922 let mk_nuprl5_op pl = mk_op nuprl5_opname pl
117 nogin 6624 let mk_nuprl5_simple_op s = mk_op nuprl5_opname [(make_param (Token (mk_opname s nil_opname)))]
118 lolorigo 2041
119 nogin 3429 let nuprl_is_op_term opname term =
120 lolorigo 2922 match Lib_term.dest_term term with
121 nogin 3429 { term_op = term_op'; term_terms = _
122 lolorigo 2922 } when term_op' = opname -> true
123     | _ -> false
124 lolorigo 2041
125 lolorigo 2922 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 jyh 2209
132 nogin 6624 let variable_opname = mk_opname "variable" nil_opname
133    
134 nogin 3429 let nuprl_is_var_term term =
135 lolorigo 2948 match Lib_term.dest_term term with
136     { term_op = term_op'; term_terms = _ } ->
137 nogin 3429 match dest_op term_op' with
138     {op_name = opname; op_params = [p1; p2] } ->
139 lolorigo 2948 (match (dest_param p1) with
140 nogin 6624 Token v when Opname.eq v variable_opname -> true
141 lolorigo 2948 | _ -> false)
142     | _ -> false
143    
144 nogin 3429 let nuprl_dest_var term =
145 lolorigo 2948 match Lib_term.dest_term term with
146     { term_op = term_op'; term_terms = [] } ->
147 nogin 3429 (match dest_op term_op' with
148 lolorigo 2948 {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 nogin 3429 let nuprl_dest_all term =
156 lolorigo 2922 match Lib_term.dest_term term with
157 nogin 3429 { term_op = term_op'; term_terms = [tp ; prop] }
158     when term_op' = (mk_nuprl5_simple_op "all") ->
159 lolorigo 2922 (match dest_bterm tp with
160 lolorigo 2948 { bvars = []; bterm = t1 } ->
161 nogin 3429 (match dest_bterm prop with { bvars = [x]; bterm = t2 } ->
162 lolorigo 2922 x, t1, t2
163     | _ -> failwith "nuprl_dest_all")
164 nogin 3429 | _ -> failwith "nuprl_dest_all")
165 lolorigo 2922 | _ -> failwith "nuprl_dest_all"
166 nogin 3429
167     let nuprl_dest_exists term =
168 lolorigo 2922 match Lib_term.dest_term term with
169 nogin 3429 { term_op = term_op'; term_terms = [tp ; prop] }
170     when term_op' = (mk_nuprl5_simple_op "exists") ->
171 lolorigo 2922 (match dest_bterm tp with
172 lolorigo 2948 { bvars = []; bterm = t1 } ->
173 nogin 3429 (match dest_bterm prop with { bvars = [x]; bterm = t2 } ->
174 lolorigo 2922 x, t1, t2
175     | _ -> failwith "nuprl_dest_exists")
176 nogin 3429 | _ -> failwith "nuprl_dest_exists")
177 lolorigo 2922 | _ -> failwith "nuprl_dest_exists"
178    
179 nogin 3429
180     let nuprl_dest_not term =
181 lolorigo 2922 match Lib_term.dest_term term with
182 nogin 3429 { term_op = term_op'; term_terms = [prop] }
183     when term_op' = (mk_nuprl5_simple_op "not") ->
184 lolorigo 2932 (match dest_bterm prop with
185 lolorigo 2922 { bvars = []; bterm = t } ->
186     t
187 nogin 3429 | _ -> failwith "nuprl_dest_not")
188 lolorigo 2922 | _ -> failwith "nuprl_dest_not"
189    
190 nogin 3429
191     let nuprl_dest_or term =
192 lolorigo 2922 match Lib_term.dest_term term with
193 nogin 3429 { term_op = term_op'; term_terms = [left; right] }
194     when term_op' = (mk_nuprl5_simple_op "or") ->
195 lolorigo 2932 (match dest_bterm left with
196 lolorigo 2922 { bvars = []; bterm = t1 } ->
197 nogin 3429 (match dest_bterm right with { bvars = []; bterm = t2 } ->
198 lolorigo 2922 t1, t2
199     | _ -> failwith "nuprl_dest_or")
200 nogin 3429 | _ -> failwith "nuprl_dest_or")
201 lolorigo 2922 | _ -> failwith "nuprl_dest_or"
202    
203 nogin 3429
204     let nuprl_dest_implies term =
205 lolorigo 2922 match Lib_term.dest_term term with
206 nogin 3429 { term_op = term_op'; term_terms = [tp; prop] }
207     when term_op' = (mk_nuprl5_simple_op "implies") ->
208 lolorigo 2922 (match dest_bterm tp with
209     { bvars = []; bterm = t1 } ->
210 nogin 3429 (match dest_bterm prop with { bvars = []; bterm = t2 } ->
211 lolorigo 2922 t1, t2
212     | _ -> failwith "nuprl_dest_implies")
213 nogin 3429 | _ -> failwith "nuprl_dest_implies")
214 lolorigo 2922 | _ -> failwith "nuprl_dest_implies"
215    
216 nogin 3429
217     let nuprl_dest_and term =
218 lolorigo 2922 match Lib_term.dest_term term with
219 nogin 3429 { term_op = term_op'; term_terms = [left; right] }
220     when term_op' = (mk_nuprl5_simple_op "and") ->
221 lolorigo 2932 (match dest_bterm left with
222 lolorigo 2922 { bvars = []; bterm = t1 } ->
223 nogin 3429 (match dest_bterm right with { bvars = []; bterm = t2 } ->
224 lolorigo 2922 t1, t2
225     | _ -> failwith "nuprl_dest_and")
226 nogin 3429 | _ -> failwith "nuprl_dest_and")
227 lolorigo 2922 | _ -> failwith "nuprl_dest_and"
228    
229 nogin 3429
230 lolorigo 2922 (*
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 nogin 3429 *)

Properties

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

  ViewVC Help
Powered by ViewVC 1.1.26