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

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

Parent Directory Parent Directory | Revision Log Revision Log


Revision 2743 - (show annotations) (download)
Wed Jun 23 04:50:29 1999 UTC (22 years, 1 month ago) by jyh
File size: 4885 byte(s)
This is a major release; I bumped the release number to 0.6.
WARNING: There are major changes here, and there may be problems
   with this version that prevent you from using your old proof.
   Save your work before using this version.
NOTE: If you decide to try this out, and you find problems,
   please(!) send me email so I can fix it.

Changes:
   1. The proof structure is totally changed, so that the proof
      editor edits the raw proof extracts.  This means that you
      can view the actions of the refiner down to the primitive
      rule applications.  In the proof editor, you can use
      "down 0" (or "cd "0") to descend into the proof of a rule box.
      Primitive proofs are called "extracts", and are labeled with
      brackets (like [extract]).  To expand the extract, use the command
      "unfold ()".  You should be able to get all the way down to
      the primitive rule/rewrite applications.

      This also means that the format of the proof files (the .prlb
      files) has changed.  The old proof files are still valid,
      but this is a hack and will be deprecated in the next
      few months.  I haven't yet added Alexey's ASCII proof
      files, but that will come with the next release.

      As usual, the "undo ()" command undoes the last proof step,
      including "unfold ()".  The "nop ()" command, reset the undo
      stack.  I also added a "redo ()" command that undoes the
      last undo.

      There is a simple rule-box proof cache for collecting proofs
      as you edit them.  If cached proofs are available, you will
      see them in brackets (like [* # * *]) on the status line.
      I haven't yet:( added the commands to use cached proofs.

   2. Refiner changes.  I added two new features: the "cutT <term>"
      tactic cuts in a new assumption.  Also, you can apply
      rewrites directly on assumptions, with the "rwc" and
      "rwch" operations, that take a clause argument.  Basically,
      this means that instead of folding the goal, you can unfold
      the assumption.  I believe this is sound; let me know if
      you think otherwise!

   3. Resource changes.  I added resource automation, built on
      the basic resource parsing Alexey added.  Ratherthan writing
      resource code for every rule, you can annotate most rules
      to generate the resource code directly.  You can see lots of
      examples in the Itt theory.  Basically, there are three useful
      resources annotations:
         intro_resource []: adds the rule as an introduction in dT
         intro_resource [SelectOption i]: adds to selT i dT
         elim_resource []: adds as an elimination rule to dT.
            This normally tries to thin the hyp that was eliminated.
         elim_resource [ThinOption]: don't thin the hyp

      Rules should be annotated with labels on their clauses,
      like [wf], [main], [assertion], etc.  This means that in
      most tactic aplcations, you no longer need to have the
      thenLT [addHiddenLabel "main"; ...] part.

      N.B.  This is the most likey parts of this release to
      cause problems, because I deleted most old resource code.

      Also, you can still write standard resource code, but there
      is no longer a d_resource--it has been broken into two parts:
      the intro_resource for application to goals, and elim_resource
      for application to hyps.

   4. The proof editor is multi-threaded, so you can work on multiple
      proofs simultaneously.  In the normal Emacs editor, this is
      no help for you.  But there is a new Java editor with the
      standard point-and-click interface, and it views the proof
      in HTML, with multiple windows etc.  The beautiful thing is
      that you can use display forms to add commands to edit windows.
      The sad thing is that I built it on NT, Java 1.2 is required,
      and I haven't tried the blackdown.org Java release on Linux.
      This editor is pending some bug fixes from Sun to get the
      fonts right (they call this a standard release?).

      In any case, here are the direct implications.  The display
      forms have an "html" mode.  The display form formatting in
      the module Rformat has been completely redone, but display
      _should_ be the same as it was before.

      It is likely that I will add an HTML dump, so we can send
      uneditable proofs around by email or on the web.  Check out
      the file theories/base/summary.ml to see some example HTML
      display forms.

      The other issue: your MetaPRL process starts a web server on
      YOUR local machine using YOUR process id on the "next" available
      TCP port, and it serves files only from the search path that you pass
      MetaPRL.  I realize that this has security implications.  This
      is necessary to get browser access to the working MetaPRL proof.
      Is this crazy?  Let me know your beliefs, religious or
      otherwise.

   5. There are numerous minor changes.  I redid parts of the WeakMemo,
      Term_header_constr, and TermHash.  The theories/tactic directory
      has been split into tactic/boot (which is not compiled by MetaPRL),
      and theories/tactic (which is).

Jason

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 () = ls (get_current_shell ())
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
107 (*
108 * Nuprl5 interface.
109 *)
110 let edit_list_modules () = edit_list_modules (get_current_shell ())
111 let edit_list_module_all = edit_list_module_all (get_current_shell ())
112 let edit_list_module = edit_list_module (get_current_shell ())
113 let edit_list_module_rw = edit_list_module_rw (get_current_shell ())
114 let edit_list_parents = edit_list_parents (get_current_shell ())
115 let edit_list_dforms = edit_list_dforms (get_current_shell ())
116 let edit_list_precs = edit_list_precs (get_current_shell ())
117 let edit_list_prec_rels = edit_list_prec_rels (get_current_shell ())
118 let edit_create_thm = edit_create_thm (get_current_shell ())
119 let edit_create_rw = edit_create_rw (get_current_shell ())
120 let edit_cd_thm = edit_cd_thm (get_current_shell ())
121 let edit_set_goal = edit_set_goal (get_current_shell ())
122 let edit_set_redex = edit_set_redex (get_current_shell ())
123 let edit_set_contractum = edit_set_contractum (get_current_shell ())
124 let edit_set_assumptions = edit_set_assumptions (get_current_shell ())
125 let edit_set_params = edit_set_params (get_current_shell ())
126 let edit_refine = edit_refine (get_current_shell ())
127 let edit_node = edit_node (get_current_shell ())
128 let edit_save = edit_save (get_current_shell ())
129 let edit_undo () = edit_undo (get_current_shell ())
130
131 let _ = ShellHTTP.main ()
132
133 (*
134 * -*-
135 * Local Variables:
136 * Caml-master: "refiner"
137 * End:
138 * -*-
139 *)

Properties

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

  ViewVC Help
Powered by ViewVC 1.1.26