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

Annotation of /metaprl/editor/ml/mp.ml

Parent Directory Parent Directory | Revision Log Revision Log


Revision 2753 - (hide 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 jyh 2494 (*
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 jyh 2743 module Shell = Shell.Shell (Shell_p4.ShellP4 (Shell_state.ShellState))
34     module ShellHTTP = Shell_http.ShellHTTP (Shell)
35 jyh 2494
36     open Shell
37    
38     (*
39 jyh 2743 * 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 jyh 2494 * Navigation and display.
48     *)
49 jyh 2743 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 jyh 2494
53     (*
54     * Module commands.
55     *)
56 jyh 2743 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 jyh 2494
62     (*
63     * The possible objects in a package.
64     *)
65 jyh 2743 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 jyh 2494
79     (*
80     * View, close, check object.
81     * An object is not installed until it is checked.
82     *)
83 jyh 2743 let view = view (get_current_shell ())
84 jyh 2753 let ls s = ls (get_current_shell ()) s
85 jyh 2494
86     (*
87     * Editing commands.
88     *)
89 jyh 2743 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 jyh 2494
97     (*
98     * Proof editing.
99     *)
100 jyh 2743 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 jyh 2753 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 jyh 2494
113     (*
114     * Nuprl5 interface.
115     *)
116 jyh 2743 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 jyh 2494
137 jyh 2743 let _ = ShellHTTP.main ()
138 jyh 2494
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