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

Diff of /metaprl/library/nuprl5.ml

Parent Directory Parent Directory | Revision Log Revision Log | View Patch Patch

revision 2921 by nogin, Fri Oct 22 01:07:59 1999 UTC revision 2922 by lolorigo, Thu Mar 16 19:52:02 2000 UTC
# Line 25  Line 25 
25   * Authors: Lori Lorigo, Richard Eaton   * Authors: Lori Lorigo, Richard Eaton
26   *)   *)
27    
28    open Refine_error_sig
29    
30  open Printf  open Printf
31  open Mp_debug  open Mp_debug
32    
# Line 37  Line 39 
39     show_loading "Loading Nuprl5%t"     show_loading "Loading Nuprl5%t"
40    
41  let nuprl5_opname = mk_opname "!nuprl5_implementation!" nil_opname  let nuprl5_opname = mk_opname "!nuprl5_implementation!" nil_opname
42    let nuprl5_opname_p opname = opname = nuprl5_opname
43    
44  (* parameter mapping *)  (* parameter mapping *)
45    
# Line 89  Line 92 
92      | _ -> raise (Invalid_argument "destruct_bool_parameter"))      | _ -> raise (Invalid_argument "destruct_bool_parameter"))
93    | _ -> raise (Invalid_argument "destruct_bool_parameter")    | _ -> raise (Invalid_argument "destruct_bool_parameter")
94    
 (* common terms *)  
95    
96  (*  (* common terms *)
 let itoken_term s = mk_token_term nuprl5_opname s  
 let inatural_term i = mk_number_term nuprl5_opname i  
 *)  
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    *)

Legend:
Removed from v.2921  
changed lines
  Added in v.2922

  ViewVC Help
Powered by ViewVC 1.1.26