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

Contents of /metaprl/library/nuprl5.ml

Parent Directory Parent Directory | Revision Log Revision Log


Revision 2822 - (show annotations) (download)
Fri Oct 22 01:07:59 1999 UTC (21 years, 9 months ago) by nogin
File size: 3234 byte(s)
Added new function to mp_debug
let show_loading s = if !debug_load then Printf.eprintf s eflush

and replaced all usages of debug_load with show_loading

1 (*
2 * This file is part of MetaPRL, 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 Mp_debug
30
31 open Refiner.Refiner.Term
32 open Refiner.Refiner.TermType
33 open Opname
34 open Mp_num
35
36 let _ =
37 show_loading "Loading Nuprl5%t"
38
39 let nuprl5_opname = mk_opname "!nuprl5_implementation!" nil_opname
40
41 (* parameter mapping *)
42
43 let make_bool_parameter b =
44 make_param (ParamList
45 [(make_param (Token "bool")); (make_param (Number (Mp_num.Int (if b then 1 else 0))))])
46
47 let make_time_parameter time =
48 make_param (ParamList
49 [(make_param (Token "time")); (make_param (Number time))])
50
51 let time_parameter_p p =
52 match (dest_param p) with
53 ParamList [h; a; b] -> (match (dest_param h) with
54 Token s -> if s = "time" then (match (dest_param a) with
55 Number i -> (match (dest_param b) with
56 Number i -> true
57 | _ -> false)
58 | _ -> false) else false
59 | _ -> false)
60 | _ -> false
61
62 let bool_parameter_p p =
63 match (dest_param p) with
64 ParamList [h; v] -> (match (dest_param h) with
65 Token s -> if s = "bool" then (match (dest_param v) with
66 Number (Mp_num.Int i) -> (i = 1) or (i = 0)
67 | _ -> false) else false
68 | _ -> false)
69 | _ -> false
70
71 let destruct_time_parameter p =
72 match (dest_param p) with
73 ParamList [h; n] -> (match (dest_param h) with
74 Token s -> (if s = "time" then (match (dest_param n) with
75 Number i -> i
76 | _ -> raise (Invalid_argument "destruct_time_parameter_b"))
77 else raise (Invalid_argument "destruct_time_parameter_c"))
78 | _ -> raise (Invalid_argument "destruct_time_parameter_d"))
79 | _ -> raise (Invalid_argument "destruct_time_parameter_e")
80
81
82 let destruct_bool_parameter p =
83 match (dest_param p) with
84 ParamList [h; v] -> (match (dest_param h) with
85 Token s -> if s = "bool" then (match (dest_param v) with
86 Number (Mp_num.Int i) -> i = 1
87 | _ -> raise (Invalid_argument "destruct_bool_parameter"))
88 else raise (Invalid_argument "destruct_bool_parameter")
89 | _ -> raise (Invalid_argument "destruct_bool_parameter"))
90 | _ -> raise (Invalid_argument "destruct_bool_parameter")
91
92 (* common terms *)
93
94 (*
95 let itoken_term s = mk_token_term nuprl5_opname s
96 let inatural_term i = mk_number_term nuprl5_opname i
97 *)
98
99
100

Properties

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

  ViewVC Help
Powered by ViewVC 1.1.26