1 
(* 
2 
* This file is part of NuprlLight, 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 Printf 
29 
open Nl_debug 
30 

31 
open Refiner.Refiner.Term 
32 
open Refiner.Refiner.TermType 
33 
open Opname 
34 
open Nl_num 
35 

36 
let _ = 
37 
if !debug_load then 
38 
eprintf "Loading Nuprl5%t" eflush 
39 

40 
let nuprl5_opname = mk_opname "!nuprl5_implementation!" nil_opname 
41 

42 
(* parameter mapping *) 
43 

44 
let make_bool_parameter b = 
45 
make_param (ParamList 
46 
[(make_param (Token "bool")); (make_param (Number (Nl_num.Int (if b then 1 else 0))))]) 
47 

48 
let make_time_parameter time = 
49 
make_param (ParamList 
50 
[(make_param (Token "time")); (make_param (Number time))]) 
51 

52 
let time_parameter_p p = 
53 
match (dest_param p) with 
54 
ParamList [h; a; b] > (match (dest_param h) with 
55 
Token s > if s = "time" then (match (dest_param a) with 
56 
Number i > (match (dest_param b) with 
57 
Number i > true 
58 
 _ > false) 
59 
 _ > false) else false 
60 
 _ > false) 
61 
 _ > false 
62 

63 
let bool_parameter_p p = 
64 
match (dest_param p) with 
65 
ParamList [h; v] > (match (dest_param h) with 
66 
Token s > if s = "bool" then (match (dest_param v) with 
67 
Number (Nl_num.Int i) > (i = 1) or (i = 0) 
68 
 _ > false) else false 
69 
 _ > false) 
70 
 _ > false 
71 

72 
let destruct_time_parameter p = 
73 
match (dest_param p) with 
74 
ParamList [h; n] > (match (dest_param h) with 
75 
Token s > (if s = "time" then (match (dest_param n) with 
76 
Number i > i 
77 
 _ > raise (Invalid_argument "destruct_time_parameter_b")) 
78 
else raise (Invalid_argument "destruct_time_parameter_c")) 
79 
 _ > raise (Invalid_argument "destruct_time_parameter_d")) 
80 
 _ > raise (Invalid_argument "destruct_time_parameter_e") 
81 

82 

83 
let destruct_bool_parameter p = 
84 
match (dest_param p) with 
85 
ParamList [h; v] > (match (dest_param h) with 
86 
Token s > if s = "bool" then (match (dest_param v) with 
87 
Number (Nl_num.Int i) > i = 1 
88 
 _ > raise (Invalid_argument "destruct_bool_parameter")) 
89 
else raise (Invalid_argument "destruct_bool_parameter") 
90 
 _ > raise (Invalid_argument "destruct_bool_parameter")) 
91 
 _ > raise (Invalid_argument "destruct_bool_parameter") 
92 

93 
(* common terms *) 
94 

95 
(* 
96 
let itoken_term s = mk_token_term nuprl5_opname s 
97 
let inatural_term i = mk_number_term nuprl5_opname i 
98 
*) 
99 

100 

101 
