/[mojave]/metaprl/theories/tactic/mptop.ml
ViewVC logotype

Diff of /metaprl/theories/tactic/mptop.ml

Parent Directory Parent Directory | Revision Log Revision Log | View Patch Patch

revision 2911 by jyh, Thu Feb 24 01:42:53 2000 UTC revision 3058 by jyh, Sun Sep 10 20:41:19 2000 UTC
# Line 1  Line 1 
1  (*  (*!
2   * Define a resource to evaluate toplevel expressions.   * @spelling{mptop toplevel}
3     *
4     * @begin[doc]
5     * @theory[Mptop]
6     *
7     * The @tt{Mptop} module defines a simplified OCaml top-loop
8     * that is used by the @MetaPRL editor to evaluate user input.
9     * The evaluator handle only a few basic types (for example, for
10     * strings, numbers, terms, and tactics), and it handle function
11     * application.  It does not implement more sophisticated OCaml
12     * expressions such as function definition and pattern matching.
13     * @end[doc]
14   *   *
15   * ----------------------------------------------------------------   * ----------------------------------------------------------------
16   *   *
17     * @begin[license]
18     *
19   * This file is part of MetaPRL, a modular, higher order   * This file is part of MetaPRL, a modular, higher order
20   * logical framework that provides a logical programming   * logical framework that provides a logical programming
21   * environment for OCaml and other languages.   * environment for OCaml and other languages.
# Line 27  Line 40 
40   * Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA.   * Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA.
41   *   *
42   * Author: Jason Hickey   * Author: Jason Hickey
43   * jyh@cs.cornell.edu   * @email{jyh@cs.caltech.edu}
44     *
45     * @end[license]
46   *)   *)
47    
48    (*!
49     * @begin[doc]
50     * @parents
51     * @end[doc]
52     *)
53    include Summary
54    (*! @docoff *)
55    
56  open MLast  open MLast
57    
58  open Refiner.Refiner.TermType  open Refiner.Refiner.TermType
# Line 44  Line 67 
67   * TYPES                                                                *   * TYPES                                                                *
68   ************************************************************************)   ************************************************************************)
69    
70  (*  (*!
71   * These are the values that we recognize.   * @begin[doc]
72     * The valid expression types are given with the following type
73     * definition.
74     *
75     * @begin[verbatim]
76     * type expr =
77     *    (* Base types *)
78     *    UnitExpr of unit
79     *  | BoolExpr of bool
80     *  | IntExpr of int
81     *  | StringExpr of string
82     *  | TermExpr of term
83     *  | TacticExpr of tactic
84     *  | ConvExpr of conv
85     *  | AddressExpr of address
86     *
87     *    (* Untyped tuples and functions *)
88     *  | ListExpr of expr list
89     *  | TupleExpr of expr list
90     *  | FunExpr of (expr -> expr)
91     *
92     *    (* Common cases are typed *)
93     *  | UnitFunExpr of (unit -> expr)
94     *  | BoolFunExpr of (bool -> expr)
95     *  | IntFunExpr of (int -> expr)
96     *  | StringFunExpr of (string -> expr)
97     *  | TermFunExpr of (term -> expr)
98     *  | TacticFunExpr of (tactic -> expr)
99     *  | IntTacticFunExpr of ((int -> tactic) -> expr)
100     *  | ConvFunExpr of (conv -> expr)
101     *  | AddressFunExpr of (address -> expr)
102     *
103     *    (* These functions take lists *)
104     *  | AddrFunExpr of (int list -> expr)
105     *  | StringListFunExpr of (string list -> expr)
106     *  | TermListFunExpr of (term list -> expr)
107     *  | TacticListFunExpr of (tactic list -> expr)
108     *  | ConvListFunExpr of (conv list -> expr)
109     * @end[verbatim]
110     * @end[doc]
111   *)   *)
112  type expr =  type expr =
113     (* Base types *)     (* Base types *)
# Line 93  Line 155 
155  type top_table =  type top_table =
156     (string, string * expr) Hashtbl.t     (string, string * expr) Hashtbl.t
157    
158    (*!
159     * @begin[doc]
160     * Toplevel values are added to the @Comment!resource[toploop_resource] resource.
161     * The argument has type @code{string * expr}, which includes
162     * the string name of the value, and it's value.
163     * @docoff
164     * @end[doc]
165     *)
166  resource (string * expr, top_table, top_data, unit) toploop_resource  resource (string * expr, top_table, top_data, unit) toploop_resource
167    
168  (************************************************************************  (************************************************************************

Legend:
Removed from v.2911  
changed lines
  Added in v.3058

  ViewVC Help
Powered by ViewVC 1.1.26