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

Contents of /metaprl/library/nuprl5.ml

Parent Directory Parent Directory | Revision Log Revision Log


Revision 2456 - (show 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 (*
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 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

Properties

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

  ViewVC Help
Powered by ViewVC 1.1.26