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

Annotation of /metaprl/library/nuprl5.ml

Parent Directory Parent Directory | Revision Log Revision Log


Revision 2922 - (hide 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 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     * 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 lolorigo 2922 open Refine_error_sig
29    
30 jyh 2190 open Printf
31 jyh 2494 open Mp_debug
32 jyh 2190
33 jyh 2184 open Refiner.Refiner.Term
34 jyh 2283 open Refiner.Refiner.TermType
35 lolorigo 2041 open Opname
36 jyh 2494 open Mp_num
37 lolorigo 2041
38 jyh 2190 let _ =
39 nogin 2822 show_loading "Loading Nuprl5%t"
40 jyh 2190
41 lolorigo 2041 let nuprl5_opname = mk_opname "!nuprl5_implementation!" nil_opname
42 lolorigo 2922 let nuprl5_opname_p opname = opname = nuprl5_opname
43 lolorigo 2041
44     (* parameter mapping *)
45    
46     let make_bool_parameter b =
47 jyh 2184 make_param (ParamList
48 jyh 2494 [(make_param (Token "bool")); (make_param (Number (Mp_num.Int (if b then 1 else 0))))])
49 eaton 2149
50 lolorigo 2041 let make_time_parameter time =
51 jyh 2184 make_param (ParamList
52 eaton 2149 [(make_param (Token "time")); (make_param (Number time))])
53 lolorigo 2041
54     let time_parameter_p p =
55     match (dest_param p) with
56 jyh 2184 ParamList [h; a; b] -> (match (dest_param h) with
57 lolorigo 2041 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 jyh 2184 ParamList [h; v] -> (match (dest_param h) with
68 lolorigo 2041 Token s -> if s = "bool" then (match (dest_param v) with
69 jyh 2494 Number (Mp_num.Int i) -> (i = 1) or (i = 0)
70 lolorigo 2041 | _ -> false) else false
71     | _ -> false)
72     | _ -> false
73    
74     let destruct_time_parameter p =
75     match (dest_param p) with
76 jyh 2184 ParamList [h; n] -> (match (dest_param h) with
77 eaton 2149 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 lolorigo 2041
84 eaton 2149
85 lolorigo 2041 let destruct_bool_parameter p =
86     match (dest_param p) with
87 jyh 2184 ParamList [h; v] -> (match (dest_param h) with
88 lolorigo 2041 Token s -> if s = "bool" then (match (dest_param v) with
89 jyh 2494 Number (Mp_num.Int i) -> i = 1
90 lolorigo 2041 | _ -> 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 lolorigo 2922
96 lolorigo 2041 (* common terms *)
97    
98 lolorigo 2922 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 lolorigo 2041
101 lolorigo 2922 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 lolorigo 2041
107 lolorigo 2922 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 jyh 2209
114 lolorigo 2922 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