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

Contents of /metaprl/library/nuprl5.ml

Parent Directory Parent Directory | Revision Log Revision Log


Revision 2922 - (show annotations) (download)
Thu Mar 16 19:52:02 2000 UTC (21 years, 4 months ago) by lolorigo
File size: 6754 byte(s)
added/improved functionality for metaprl/jprover/nuprl5 io

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/index.html for information on Nuprl,
7 * OCaml, and more information about this system.
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 Refine_error_sig
29
30 open Printf
31 open Mp_debug
32
33 open Refiner.Refiner.Term
34 open Refiner.Refiner.TermType
35 open Opname
36 open Mp_num
37
38 let _ =
39 show_loading "Loading Nuprl5%t"
40
41 let nuprl5_opname = mk_opname "!nuprl5_implementation!" nil_opname
42 let nuprl5_opname_p opname = opname = nuprl5_opname
43
44 (* parameter mapping *)
45
46 let make_bool_parameter b =
47 make_param (ParamList
48 [(make_param (Token "bool")); (make_param (Number (Mp_num.Int (if b then 1 else 0))))])
49
50 let make_time_parameter time =
51 make_param (ParamList
52 [(make_param (Token "time")); (make_param (Number time))])
53
54 let time_parameter_p p =
55 match (dest_param p) with
56 ParamList [h; a; b] -> (match (dest_param h) with
57 Token s -> if s = "time" then (match (dest_param a) with
58 Number i -> (match (dest_param b) with
59 Number i -> true
60 | _ -> false)
61 | _ -> false) else false
62 | _ -> false)
63 | _ -> false
64
65 let bool_parameter_p p =
66 match (dest_param p) with
67 ParamList [h; v] -> (match (dest_param h) with
68 Token s -> if s = "bool" then (match (dest_param v) with
69 Number (Mp_num.Int i) -> (i = 1) or (i = 0)
70 | _ -> false) else false
71 | _ -> false)
72 | _ -> false
73
74 let destruct_time_parameter p =
75 match (dest_param p) with
76 ParamList [h; n] -> (match (dest_param h) with
77 Token s -> (if s = "time" then (match (dest_param n) with
78 Number i -> i
79 | _ -> raise (Invalid_argument "destruct_time_parameter_b"))
80 else raise (Invalid_argument "destruct_time_parameter_c"))
81 | _ -> raise (Invalid_argument "destruct_time_parameter_d"))
82 | _ -> raise (Invalid_argument "destruct_time_parameter_e")
83
84
85 let destruct_bool_parameter p =
86 match (dest_param p) with
87 ParamList [h; v] -> (match (dest_param h) with
88 Token s -> if s = "bool" then (match (dest_param v) with
89 Number (Mp_num.Int i) -> i = 1
90 | _ -> raise (Invalid_argument "destruct_bool_parameter"))
91 else raise (Invalid_argument "destruct_bool_parameter")
92 | _ -> raise (Invalid_argument "destruct_bool_parameter"))
93 | _ -> raise (Invalid_argument "destruct_bool_parameter")
94
95
96 (* common terms *)
97
98 let mk_nuprl5_op pl = mk_op nuprl5_opname pl
99 let mk_nuprl5_simple_op s = mk_op nuprl5_opname [(make_param (Token s))]
100
101 let nuprl_is_op_term opname term =
102 match Lib_term.dest_term term with
103 { term_op = term_op'; term_terms = _
104 } when term_op' = opname -> true
105 | _ -> false
106
107 let nuprl_is_not_term = nuprl_is_op_term (mk_nuprl5_simple_op "not")
108 let nuprl_is_exists_term = nuprl_is_op_term (mk_nuprl5_simple_op "exists")
109 let nuprl_is_or_term = nuprl_is_op_term (mk_nuprl5_simple_op "or")
110 let nuprl_is_and_term = nuprl_is_op_term (mk_nuprl5_simple_op "and")
111 let nuprl_is_implies_term = nuprl_is_op_term (mk_nuprl5_simple_op "implies")
112 let nuprl_is_all_term = nuprl_is_op_term (mk_nuprl5_simple_op "all")
113
114 let nuprl_dest_all term =
115 match Lib_term.dest_term term with
116 { term_op = term_op'; term_terms = [tp ; prop] }
117 when term_op' = (mk_nuprl5_simple_op "all") ->
118 (match dest_bterm tp with
119 { bvars = [x]; bterm = t1 } ->
120 (match dest_bterm prop with { bvars = []; bterm = t2 } ->
121 x, t1, t2
122 | _ -> failwith "nuprl_dest_all")
123 | _ -> failwith "nuprl_dest_all")
124 | _ -> failwith "nuprl_dest_all"
125
126
127 let nuprl_dest_exists term =
128 match Lib_term.dest_term term with
129 { term_op = term_op'; term_terms = [tp ; prop] }
130 when term_op' = (mk_nuprl5_simple_op "exists") ->
131 (match dest_bterm tp with
132 { bvars = [x]; bterm = t1 } ->
133 (match dest_bterm prop with { bvars = []; bterm = t2 } ->
134 x, t1, t2
135 | _ -> failwith "nuprl_dest_exists")
136 | _ -> failwith "nuprl_dest_exists")
137 | _ -> failwith "nuprl_dest_exists"
138
139
140 let nuprl_dest_not term =
141 match Lib_term.dest_term term with
142 { term_op = term_op'; term_terms = [tp ; prop] }
143 when term_op' = (mk_nuprl5_simple_op "not") ->
144 (match dest_bterm tp with
145 { bvars = []; bterm = t } ->
146 t
147 | _ -> failwith "nuprl_dest_not")
148 | _ -> failwith "nuprl_dest_not"
149
150
151 let nuprl_dest_or term =
152 match Lib_term.dest_term term with
153 { term_op = term_op'; term_terms = [tp ; prop] }
154 when term_op' = (mk_nuprl5_simple_op "or") ->
155 (match dest_bterm tp with
156 { bvars = []; bterm = t1 } ->
157 (match dest_bterm prop with { bvars = []; bterm = t2 } ->
158 t1, t2
159 | _ -> failwith "nuprl_dest_or")
160 | _ -> failwith "nuprl_dest_or")
161 | _ -> failwith "nuprl_dest_or"
162
163
164 let nuprl_dest_implies term =
165 match Lib_term.dest_term term with
166 { term_op = term_op'; term_terms = [tp ; prop] }
167 when term_op' = (mk_nuprl5_simple_op "implies") ->
168 (match dest_bterm tp with
169 { bvars = []; bterm = t1 } ->
170 (match dest_bterm prop with { bvars = []; bterm = t2 } ->
171 t1, t2
172 | _ -> failwith "nuprl_dest_implies")
173 | _ -> failwith "nuprl_dest_implies")
174 | _ -> failwith "nuprl_dest_implies"
175
176
177 let nuprl_dest_and term =
178 match Lib_term.dest_term term with
179 { term_op = term_op'; term_terms = [tp ; prop] }
180 when term_op' = (mk_nuprl5_simple_op "and") ->
181 (match dest_bterm tp with
182 { bvars = []; bterm = t1 } ->
183 (match dest_bterm prop with { bvars = []; bterm = t2 } ->
184 t1, t2
185 | _ -> failwith "nuprl_dest_and")
186 | _ -> failwith "nuprl_dest_and")
187 | _ -> failwith "nuprl_dest_and"
188
189
190 (*
191 let nuprl_is_all_term = function
192 { term_op = { op_name = nuprl5_opname; op_params = [make_param (Token "all")] };
193 term_terms = [{ bvars = [] }; { bvars = [_] }]
194 } -> true
195 | _ -> false
196 *)

Properties

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

  ViewVC Help
Powered by ViewVC 1.1.26