/[mojave]/metaprl/editor/ml/mp.ml
ViewVC logotype

Contents of /metaprl/editor/ml/mp.ml

Parent Directory Parent Directory | Revision Log Revision Log


Revision 2753 - (show annotations) (download)
Fri Jun 25 00:19:15 1999 UTC (22 years, 1 month ago) by jyh
File size: 5156 byte(s)
These are some minor changes to make things work better.  Changed
meaning of ThinOption in elim_resource: it now means to thin the hyp
by default, unless overridden by thinningT false.

Fixed some proof operations.  Added "move_to_assum" command to take
the current subgoal and make it an extra assumption of the entire
proof (it may not work at the moment).

ls now takes a _string_ argument.  Use ls "u";; to display only the
unproved rules in the current module.

Proved many membership variants of the standard type constructors,
but there are a few more to go.  When you are defining theories, I
believe you should use membership, not equality.  After all, equality
is derivable from membership, and membership is a lot easier.

Still to go: ASCII format proof files; save proofs _without_ extracts
by default.  The expand () function does not reexpand proofs correctly.
A few problems with proof navigation.

1 (*
2 * This is the main file for MetaPRL.
3 *
4 * ----------------------------------------------------------------
5 *
6 * This file is part of MetaPRL, a modular, higher order
7 * logical framework that provides a logical programming
8 * environment for OCaml and other languages.
9 *
10 * See the file doc/index.html for information on Nuprl,
11 * OCaml, and more information about this system.
12 *
13 * Copyright (C) 1998 Jason Hickey, Cornell University
14 *
15 * This program is free software; you can redistribute it and/or
16 * modify it under the terms of the GNU General Public License
17 * as published by the Free Software Foundation; either version 2
18 * of the License, or (at your option) any later version.
19 *
20 * This program is distributed in the hope that it will be useful,
21 * but WITHOUT ANY WARRANTY; without even the implied warranty of
22 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
23 * GNU General Public License for more details.
24 *
25 * You should have received a copy of the GNU General Public License
26 * along with this program; if not, write to the Free Software
27 * Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA.
28 *
29 * Author: Jason Hickey
30 * jyh@cs.cornell.edu
31 *)
32
33 module Shell = Shell.Shell (Shell_p4.ShellP4 (Shell_state.ShellState))
34 module ShellHTTP = Shell_http.ShellHTTP (Shell)
35
36 open Shell
37
38 (*
39 * Job control.
40 *)
41 let fork = fork (get_current_shell ())
42 let pid = pid (get_current_shell ())
43 let jobs = jobs (get_current_shell ())
44 let fg = fg (get_current_shell ())
45
46 (*
47 * Navigation and display.
48 *)
49 let cd = cd (get_current_shell ())
50 let pwd () = pwd (get_current_shell ())
51 let set_window_width = set_window_width (get_current_shell ())
52
53 (*
54 * Module commands.
55 *)
56 let load = load (get_current_shell ())
57 let create_pkg = create_pkg (get_current_shell ())
58 let set_writeable () = set_writeable (get_current_shell ())
59 let save () = save (get_current_shell ())
60 let save_all () = save_all (get_current_shell ())
61
62 (*
63 * The possible objects in a package.
64 *)
65 let create_rw = create_rw (get_current_shell ())
66 let create_axiom = create_axiom (get_current_shell ())
67 let create_thm = create_thm (get_current_shell ())
68 let create_tptp = create_tptp (get_current_shell ())
69 let create_opname = create_opname (get_current_shell ())
70 let create_condition = create_condition (get_current_shell ())
71 let create_parent = create_parent (get_current_shell ())
72 let create_dform = create_dform (get_current_shell ())
73 let create_prec = create_prec (get_current_shell ())
74 let create_prec_rel = create_prec_rel (get_current_shell ())
75 let create_resource = create_resource (get_current_shell ())
76 let create_infix = create_infix (get_current_shell ())
77 let create_ml = create_ml (get_current_shell ())
78
79 (*
80 * View, close, check object.
81 * An object is not installed until it is checked.
82 *)
83 let view = view (get_current_shell ())
84 let ls s = ls (get_current_shell ()) s
85
86 (*
87 * Editing commands.
88 *)
89 let set_goal = set_goal (get_current_shell ())
90 let set_redex = set_redex (get_current_shell ())
91 let set_contractum = set_contractum (get_current_shell ())
92 let set_assumptions = set_assumptions (get_current_shell ())
93 let set_params = set_params (get_current_shell ())
94 let check () = check (get_current_shell ())
95 let expand () = expand (get_current_shell ())
96
97 (*
98 * Proof editing.
99 *)
100 let root () = root (get_current_shell ())
101 let up = up (get_current_shell ())
102 let down = down (get_current_shell ())
103 let goal () = goal (get_current_shell ())
104 let refine = refine (get_current_shell ())
105 let undo () = undo (get_current_shell ())
106 let redo () = redo (get_current_shell ())
107 let nop () = nop (get_current_shell ())
108 let unfold () = unfold (get_current_shell ())
109 let copy s = copy (get_current_shell ()) s
110 let paste s = paste (get_current_shell ()) s
111 let make_assum () = make_assum (get_current_shell ())
112
113 (*
114 * Nuprl5 interface.
115 *)
116 let edit_list_modules () = edit_list_modules (get_current_shell ())
117 let edit_list_module_all = edit_list_module_all (get_current_shell ())
118 let edit_list_module = edit_list_module (get_current_shell ())
119 let edit_list_module_rw = edit_list_module_rw (get_current_shell ())
120 let edit_list_parents = edit_list_parents (get_current_shell ())
121 let edit_list_dforms = edit_list_dforms (get_current_shell ())
122 let edit_list_precs = edit_list_precs (get_current_shell ())
123 let edit_list_prec_rels = edit_list_prec_rels (get_current_shell ())
124 let edit_create_thm = edit_create_thm (get_current_shell ())
125 let edit_create_rw = edit_create_rw (get_current_shell ())
126 let edit_cd_thm = edit_cd_thm (get_current_shell ())
127 let edit_set_goal = edit_set_goal (get_current_shell ())
128 let edit_set_redex = edit_set_redex (get_current_shell ())
129 let edit_set_contractum = edit_set_contractum (get_current_shell ())
130 let edit_set_assumptions = edit_set_assumptions (get_current_shell ())
131 let edit_set_params = edit_set_params (get_current_shell ())
132 let edit_refine = edit_refine (get_current_shell ())
133 let edit_node = edit_node (get_current_shell ())
134 let edit_save = edit_save (get_current_shell ())
135 let edit_undo () = edit_undo (get_current_shell ())
136
137 let _ = ShellHTTP.main ()
138
139 (*
140 * -*-
141 * Local Variables:
142 * Caml-master: "refiner"
143 * End:
144 * -*-
145 *)

Properties

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

  ViewVC Help
Powered by ViewVC 1.1.26