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

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

Parent Directory Parent Directory | Revision Log Revision Log


Revision 2775 - (show annotations) (download)
Sun Jul 4 13:13:44 1999 UTC (22 years ago) by jyh
File size: 5392 byte(s)
Things seem to be working pretty smoothly now.  This is mostly minor
fixes.  Still need to fix the problems with the mp toploop.

    1. Proofs now use Alexey's ASCII format.  By default, proofs
       should be saved to CVS in .prla format.  You can generate ASCII
       files by using "make export", or you can use the "export ()"
       instead of the "save ()" command in the editor.  For speed,
       .prlb files are now saved in a raw, marshaled format.  When you
       edit a theory, the newest of .cmoz, .prlb, or .prla files is
       loaded.  There is a new command "convert" to convert between
       all the different proof file formats.
          convert -I ... [-raw|-term|-lib|-ascii] -impl file.cmoz
          raw: save the file in fast, raw format
	  term: save the file as <magic#>/<marshaled term_io>
	  lib: send the file to the Nuprl5 library
	  ascii: create a .prla file

       Developers: _please_ mention any changes to the basic data
          structures in your CVS logs.  The things that matter are:
          Refiner.Refiner.TermType.term
	  Filter_summary.summary_info
	  Tactic_boot_sig.TacticType.{tactic_arg,extract}
	  Proof_boot.io_proof

       Users: to be safe, save all your proofs using "make export"
          before doing a cvs update.

    2. "expand ()" and "expand_all ()" now work.  I also added
       "clean ()" and "clean_all ()" commands to remove those peasky
       dangling proof nodes when you are satisfied with a proof.  By
       default, proofs are saved only down to the innermost rule-box
       level, and primitive refinements are omitted.  I haven't added
       a "deep_save ()" command; it seems unecessary.

    3. Sorry, but I had to move theories/boot into the filter.  There
       are no major changes here, but the directory structure in
       filter has changed significantly.

    4. I added a THEORIES variable to the mk/config file that
       specifies what theories you want to compile.  This means that
       you don't have to edit all the Makefiles when you add a theory,
       and it also means that you can keep your own theories without
       having to commit them to cvs.

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 export () = export (get_current_shell ())
61 let save_all () = save_all (get_current_shell ())
62
63 (*
64 * The possible objects in a package.
65 *)
66 let create_rw = create_rw (get_current_shell ())
67 let create_axiom = create_axiom (get_current_shell ())
68 let create_thm = create_thm (get_current_shell ())
69 let create_tptp = create_tptp (get_current_shell ())
70 let create_opname = create_opname (get_current_shell ())
71 let create_condition = create_condition (get_current_shell ())
72 let create_parent = create_parent (get_current_shell ())
73 let create_dform = create_dform (get_current_shell ())
74 let create_prec = create_prec (get_current_shell ())
75 let create_prec_rel = create_prec_rel (get_current_shell ())
76 let create_resource = create_resource (get_current_shell ())
77 let create_infix = create_infix (get_current_shell ())
78 let create_ml = create_ml (get_current_shell ())
79
80 (*
81 * View, close, check object.
82 * An object is not installed until it is checked.
83 *)
84 let view = view (get_current_shell ())
85 let ls s = ls (get_current_shell ()) s
86
87 (*
88 * Editing commands.
89 *)
90 let set_goal = set_goal (get_current_shell ())
91 let set_redex = set_redex (get_current_shell ())
92 let set_contractum = set_contractum (get_current_shell ())
93 let set_assumptions = set_assumptions (get_current_shell ())
94 let set_params = set_params (get_current_shell ())
95 let check () = check (get_current_shell ())
96 let expand () = expand (get_current_shell ())
97
98 (*
99 * Proof editing.
100 *)
101 let root () = root (get_current_shell ())
102 let up = up (get_current_shell ())
103 let down = down (get_current_shell ())
104 let goal () = goal (get_current_shell ())
105 let refine = refine (get_current_shell ())
106 let undo () = undo (get_current_shell ())
107 let redo () = redo (get_current_shell ())
108 let nop () = nop (get_current_shell ())
109 let unfold () = unfold (get_current_shell ())
110 let copy s = copy (get_current_shell ()) s
111 let paste s = paste (get_current_shell ()) s
112 let kreitz () = kreitz (get_current_shell ())
113 let clean () = clean (get_current_shell ())
114 let squash () = squash (get_current_shell ())
115 let make_assum () = make_assum (get_current_shell ())
116
117 (*
118 * Nuprl5 interface.
119 *)
120 let edit_list_modules () = edit_list_modules (get_current_shell ())
121 let edit_list_module_all = edit_list_module_all (get_current_shell ())
122 let edit_list_module = edit_list_module (get_current_shell ())
123 let edit_list_module_rw = edit_list_module_rw (get_current_shell ())
124 let edit_list_parents = edit_list_parents (get_current_shell ())
125 let edit_list_dforms = edit_list_dforms (get_current_shell ())
126 let edit_list_precs = edit_list_precs (get_current_shell ())
127 let edit_list_prec_rels = edit_list_prec_rels (get_current_shell ())
128 let edit_create_thm = edit_create_thm (get_current_shell ())
129 let edit_create_rw = edit_create_rw (get_current_shell ())
130 let edit_cd_thm = edit_cd_thm (get_current_shell ())
131 let edit_set_goal = edit_set_goal (get_current_shell ())
132 let edit_set_redex = edit_set_redex (get_current_shell ())
133 let edit_set_contractum = edit_set_contractum (get_current_shell ())
134 let edit_set_assumptions = edit_set_assumptions (get_current_shell ())
135 let edit_set_params = edit_set_params (get_current_shell ())
136 let edit_refine = edit_refine (get_current_shell ())
137 let edit_node = edit_node (get_current_shell ())
138 let edit_save = edit_save (get_current_shell ())
139 let edit_undo () = edit_undo (get_current_shell ())
140
141 let shell_get_term = Shell_state.ShellState.get_term
142
143 let _ = ShellHTTP.main ()
144
145 (*
146 * -*-
147 * Local Variables:
148 * Caml-master: "refiner"
149 * End:
150 * -*-
151 *)

Properties

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

  ViewVC Help
Powered by ViewVC 1.1.26