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

Annotation of /metaprl/library/nuprl5.ml

Parent Directory Parent Directory | Revision Log Revision Log


Revision 2190 - (hide annotations) (download)
Thu May 28 13:48:44 1998 UTC (23 years, 2 months ago) by jyh
File size: 2122 byte(s)
Updated the editor to use new Refiner structure.
ITT needs dform names.

1 jyh 2190 open Printf
2     open Debug
3    
4 jyh 2184 open Refiner.Refiner.Term
5 lolorigo 2041 open Opname
6 eaton 2149 open Num
7 lolorigo 2041
8 jyh 2190 let _ =
9     if !debug_load then
10     eprintf "Loading Nuprl5%t" eflush
11    
12 lolorigo 2041 let nuprl5_opname = mk_opname "!nuprl5_implementation!" nil_opname
13    
14     (* parameter mapping *)
15    
16     let make_bool_parameter b =
17 jyh 2184 make_param (ParamList
18 eli 2099 [(make_param (Token "bool")); (make_param (Number (Num.Int (if b then 1 else 0))))])
19 eaton 2149
20 lolorigo 2041 let make_time_parameter time =
21 jyh 2184 make_param (ParamList
22 eaton 2149 [(make_param (Token "time")); (make_param (Number time))])
23 lolorigo 2041
24     let time_parameter_p p =
25     match (dest_param p) with
26 jyh 2184 ParamList [h; a; b] -> (match (dest_param h) with
27 lolorigo 2041 Token s -> if s = "time" then (match (dest_param a) with
28     Number i -> (match (dest_param b) with
29     Number i -> true
30     | _ -> false)
31     | _ -> false) else false
32     | _ -> false)
33     | _ -> false
34    
35     let bool_parameter_p p =
36     match (dest_param p) with
37 jyh 2184 ParamList [h; v] -> (match (dest_param h) with
38 lolorigo 2041 Token s -> if s = "bool" then (match (dest_param v) with
39 eli 2099 Number (Num.Int i) -> (i = 1) or (i = 0)
40 lolorigo 2041 | _ -> false) else false
41     | _ -> false)
42     | _ -> false
43    
44     let destruct_time_parameter p =
45     match (dest_param p) with
46 jyh 2184 ParamList [h; n] -> (match (dest_param h) with
47 eaton 2149 Token s -> (if s = "time" then (match (dest_param n) with
48     Number i -> i
49     | _ -> raise (Invalid_argument "destruct_time_parameter_b"))
50     else raise (Invalid_argument "destruct_time_parameter_c"))
51     | _ -> raise (Invalid_argument "destruct_time_parameter_d"))
52     | _ -> raise (Invalid_argument "destruct_time_parameter_e")
53 lolorigo 2041
54 eaton 2149
55 lolorigo 2041 let destruct_bool_parameter p =
56     match (dest_param p) with
57 jyh 2184 ParamList [h; v] -> (match (dest_param h) with
58 lolorigo 2041 Token s -> if s = "bool" then (match (dest_param v) with
59 eli 2099 Number (Num.Int i) -> i = 1
60 lolorigo 2041 | _ -> raise (Invalid_argument "destruct_bool_parameter"))
61     else raise (Invalid_argument "destruct_bool_parameter")
62     | _ -> raise (Invalid_argument "destruct_bool_parameter"))
63     | _ -> raise (Invalid_argument "destruct_bool_parameter")
64    
65     (* common terms *)
66    
67     (*
68     let itoken_term s = mk_token_term nuprl5_opname s
69     let inatural_term i = mk_number_term nuprl5_opname i
70     *)
71    
72    
73    

Properties

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

  ViewVC Help
Powered by ViewVC 1.1.26