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

Annotation of /metaprl/library/nuprl5.ml

Parent Directory Parent Directory | Revision Log Revision Log


Revision 2494 - (hide annotations) (download)
Tue Oct 13 01:14:08 1998 UTC (22 years, 9 months ago) by jyh
File size: 3262 byte(s)
I changed all the obvious places of Nuprl-Light, NL, nl, or any
other instance to MetaPRL, MP, or mp, etc.  The docs may be broken
but I'll fix them soon.  As usual, let me know if anything breaks.

1 jyh 2456 (*
2 jyh 2494 * This file is part of MetaPRL, a modular, higher order
3 jyh 2456 * 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 2494 open Mp_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 2494 open Mp_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 2494 [(make_param (Token "bool")); (make_param (Number (Mp_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 2494 Number (Mp_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 2494 Number (Mp_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