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

Annotation of /metaprl/library/nuprl5.ml

Parent Directory Parent Directory | Revision Log Revision Log


Revision 2456 - (hide annotations) (download)
Sat Sep 5 22:31:37 1998 UTC (22 years, 10 months ago) by jyh
File size: 3266 byte(s)
Added license headers to each of the files in preparation for
the first major release.  The license is GNU public license; if
any of you have problems with that, let me know right away.  When
you add new code, you should credit yourself as the author.  When
you modify code, you should add a "Modified by:" to the header,
and possibly a short summary of your changes.

I tried to get the Author lists as correct as I remember, but there
are more than 550 files(!) and I may have made some mistakes. Please
add yourself if I didn't do it right.

1 jyh 2456 (*
2     * This file is part of Nuprl-Light, 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 jyh 2190 open Printf
29 jyh 2336 open Nl_debug
30 jyh 2190
31 jyh 2184 open Refiner.Refiner.Term
32 jyh 2283 open Refiner.Refiner.TermType
33 lolorigo 2041 open Opname
34 jyh 2443 open Nl_num
35 lolorigo 2041
36 jyh 2190 let _ =
37     if !debug_load then
38     eprintf "Loading Nuprl5%t" eflush
39    
40 lolorigo 2041 let nuprl5_opname = mk_opname "!nuprl5_implementation!" nil_opname
41    
42     (* parameter mapping *)
43    
44     let make_bool_parameter b =
45 jyh 2184 make_param (ParamList
46 jyh 2443 [(make_param (Token "bool")); (make_param (Number (Nl_num.Int (if b then 1 else 0))))])
47 eaton 2149
48 lolorigo 2041 let make_time_parameter time =
49 jyh 2184 make_param (ParamList
50 eaton 2149 [(make_param (Token "time")); (make_param (Number time))])
51 lolorigo 2041
52     let time_parameter_p p =
53     match (dest_param p) with
54 jyh 2184 ParamList [h; a; b] -> (match (dest_param h) with
55 lolorigo 2041 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 jyh 2184 ParamList [h; v] -> (match (dest_param h) with
66 lolorigo 2041 Token s -> if s = "bool" then (match (dest_param v) with
67 jyh 2443 Number (Nl_num.Int i) -> (i = 1) or (i = 0)
68 lolorigo 2041 | _ -> false) else false
69     | _ -> false)
70     | _ -> false
71    
72     let destruct_time_parameter p =
73     match (dest_param p) with
74 jyh 2184 ParamList [h; n] -> (match (dest_param h) with
75 eaton 2149 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 lolorigo 2041
82 eaton 2149
83 lolorigo 2041 let destruct_bool_parameter p =
84     match (dest_param p) with
85 jyh 2184 ParamList [h; v] -> (match (dest_param h) with
86 lolorigo 2041 Token s -> if s = "bool" then (match (dest_param v) with
87 jyh 2443 Number (Nl_num.Int i) -> i = 1
88 lolorigo 2041 | _ -> 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 jyh 2209

Properties

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

  ViewVC Help
Powered by ViewVC 1.1.26