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

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

Parent Directory Parent Directory | Revision Log Revision Log


Revision 3292 - (hide annotations) (download)
Sun Jun 24 10:25:49 2001 UTC (20 years, 1 month ago) by nogin
File size: 21819 byte(s)
*** IMPORTANT: before doing "cvs update" see warning below ***

This commit implements a global resource that brings together resource management
that used to be done by each resource in its own way.

- A much simplier object (Mp_resource.resource_info) is now needed to create a new resource.
Additionally, many resource helper modules, such as term_match_table now provide functions
that create a resource_info for you.

- Funtions get_tactic_arg, get_int_tactic_arg, etc were replaced by a single function
get_resource_arg (note: functions for basci types, such as get_with_arg, get_sel_args, etc
were _not_ affected)

- Resource declaration statement now declares and resource creation statement now creates
a function get_<name>_resource. This function ca be passed as a second argument
to get_resource_arg to retrieve the current value of a particular resource.

- Resource annotation functions are now separate from the resource declaration/creation
mechanism. Resource annotation on a rule are now passed to a function named
process_<name>_resource_annotation. This function must have the appropriate
Mp_resource.annotation_processor type for the resource. This function can be declared
and implemented in _any_ module, not just the module that declares and creates the
<name> resource.

- Currenlty MetaPRL leaves it to Ocaml to keep track of these functions.
Consequently the module that defines the process_<name>_resource_annotation function
must be open'ed (not included!) by modules that use <name> annotations.

-----

Unfinished business in this commit:
- Remainder of TODO 1.12 and 1.13

- Some proofs were broken by this commit. It appears that they were broken for
a "good" reason, but still need to be fixed.

- I need to make sure things now always have the right precedences (all things being equal,
the later an item is added to resource, the earlier precedence it should have).

- Consider adding refiner sentinels and display forms to global resource as well.
Currently each of them still does its own way of resource management (although the way
display forms are managed was changed by this commit - need to make sure the precedences
are right).

- Distributed refinement: I am afraid that the current resource code
will either work correctly only if all processes in the distributed group have
the same global resource, or it will attempt to pass around all the resource data.
Obviously, neither of these choices is a good one.

*** WARNING ***

This commit changes the tactic_arg type and also makes minor changes in
the FilterCache.info type. Because of that old .prlb and .cmoz files
*will no longer work*. Old .prla files will work, but will produce lots
of (harmless) Filter_summary.dest_term warning.

Before doing "cvs update" do the following:
1) export all your unsaved proofs into .prla files.
2) rm -f theories/*/*.prlb
3) run "make clean"

1 jyh 3058 (*!
2     * @spelling{mptop toplevel}
3 jyh 2494 *
4 jyh 3058 * @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 jyh 2494 * ----------------------------------------------------------------
16     *
17 jyh 3058 * @begin[license]
18     *
19 jyh 2494 * This file is part of MetaPRL, a modular, higher order
20     * logical framework that provides a logical programming
21     * environment for OCaml and other languages.
22     *
23     * See the file doc/index.html for information on Nuprl,
24     * OCaml, and more information about this system.
25     *
26     * Copyright (C) 1998 Jason Hickey, Cornell University
27 jyh 2525 *
28 jyh 2494 * This program is free software; you can redistribute it and/or
29     * modify it under the terms of the GNU General Public License
30     * as published by the Free Software Foundation; either version 2
31     * of the License, or (at your option) any later version.
32 jyh 2525 *
33 jyh 2494 * This program is distributed in the hope that it will be useful,
34     * but WITHOUT ANY WARRANTY; without even the implied warranty of
35     * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
36     * GNU General Public License for more details.
37 jyh 2525 *
38 jyh 2494 * You should have received a copy of the GNU General Public License
39     * along with this program; if not, write to the Free Software
40     * Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA.
41 jyh 2525 *
42 jyh 2494 * Author: Jason Hickey
43 jyh 3058 * @email{jyh@cs.caltech.edu}
44     *
45     * @end[license]
46 jyh 2494 *)
47    
48 jyh 3058 (*!
49     * @begin[doc]
50     * @parents
51     * @end[doc]
52     *)
53     include Summary
54     (*! @docoff *)
55    
56 jyh 2494 open MLast
57    
58     open Refiner.Refiner.TermType
59 jyh 2911 open Refiner.Refiner.TermAddr
60 nogin 3086 open Refiner.Refiner.TermMan
61 jyh 2494 open Refiner.Refiner.RefineError
62     open Mp_resource
63    
64 jyh 2743 open Tactic_type.Tacticals
65     open Tactic_type.Conversionals
66 jyh 2494
67     (************************************************************************
68     * TYPES *
69     ************************************************************************)
70    
71 jyh 3058 (*!
72     * @begin[doc]
73     * The valid expression types are given with the following type
74     * definition.
75     *
76     * @begin[verbatim]
77     * type expr =
78     * (* Base types *)
79     * UnitExpr of unit
80     * | BoolExpr of bool
81     * | IntExpr of int
82     * | StringExpr of string
83     * | TermExpr of term
84     * | TacticExpr of tactic
85     * | ConvExpr of conv
86     * | AddressExpr of address
87     *
88     * (* Untyped tuples and functions *)
89     * | ListExpr of expr list
90     * | TupleExpr of expr list
91     * | FunExpr of (expr -> expr)
92     *
93     * (* Common cases are typed *)
94     * | UnitFunExpr of (unit -> expr)
95     * | BoolFunExpr of (bool -> expr)
96     * | IntFunExpr of (int -> expr)
97     * | StringFunExpr of (string -> expr)
98     * | TermFunExpr of (term -> expr)
99     * | TacticFunExpr of (tactic -> expr)
100     * | IntTacticFunExpr of ((int -> tactic) -> expr)
101     * | ConvFunExpr of (conv -> expr)
102     * | AddressFunExpr of (address -> expr)
103     *
104     * (* These functions take lists *)
105     * | AddrFunExpr of (int list -> expr)
106     * | StringListFunExpr of (string list -> expr)
107     * | TermListFunExpr of (term list -> expr)
108     * | TacticListFunExpr of (tactic list -> expr)
109     * | ConvListFunExpr of (conv list -> expr)
110     * @end[verbatim]
111     * @end[doc]
112 jyh 2494 *)
113     type expr =
114     (* Base types *)
115     UnitExpr of unit
116     | BoolExpr of bool
117     | IntExpr of int
118     | StringExpr of string
119     | TermExpr of term
120     | TacticExpr of tactic
121     | ConvExpr of conv
122 jyh 2811 | AddressExpr of address
123 jyh 2494
124     (* Uptyped tuples and functions *)
125     | ListExpr of expr list
126     | TupleExpr of expr list
127     | FunExpr of (expr -> expr)
128    
129     (* Common cases are typed *)
130     | UnitFunExpr of (unit -> expr)
131     | BoolFunExpr of (bool -> expr)
132     | IntFunExpr of (int -> expr)
133     | StringFunExpr of (string -> expr)
134     | TermFunExpr of (term -> expr)
135     | TacticFunExpr of (tactic -> expr)
136     | IntTacticFunExpr of ((int -> tactic) -> expr)
137     | ConvFunExpr of (conv -> expr)
138 jyh 2811 | AddressFunExpr of (address -> expr)
139 jyh 2494
140     (* These functions take lists *)
141     | AddrFunExpr of (int list -> expr)
142     | StringListFunExpr of (string list -> expr)
143     | TermListFunExpr of (term list -> expr)
144     | TacticListFunExpr of (tactic list -> expr)
145     | ConvListFunExpr of (conv list -> expr)
146    
147     (*
148     * The resource maps strings to values.
149     *)
150     type top_table =
151     (string, string * expr) Hashtbl.t
152    
153     (************************************************************************
154     * IMPLEMENTATION *
155     ************************************************************************)
156    
157 nogin 3292 let create () =
158     Hashtbl.create 201
159 jyh 2494
160 nogin 3292 let add tbl (module_name,name,expr) =
161     Hashtbl.add tbl name (module_name,expr)
162 jyh 2494
163 nogin 3292 let add_commands tbl =
164     List.iter (fun (name, expr) -> Hashtbl.add tbl name ("",expr))
165 jyh 2494
166 nogin 3292 let retr tbl = tbl
167 jyh 2494
168 nogin 3292 (*!
169     * @begin[doc]
170     * Toplevel values are added to the @Comment!resource[toploop_resource] resource.
171     * The argument has type @code{string * expr}, which includes
172     * the string name of the value, and it's value.
173     * @docoff
174     * @end[doc]
175     *)
176     let resource toploop = Imperative {
177     imp_create = create;
178     imp_add = add;
179     imp_retr = retr
180     }
181 jyh 2494
182     (************************************************************************
183     * COMPILING *
184     ************************************************************************)
185    
186     (*
187     * Right now most things are not supported.
188     *)
189     let not_supported loc str =
190 nogin 2502 Stdpp.raise_with_loc loc (RefineError ("mptop", StringStringError ("operation is not implemented", str)))
191 jyh 2494
192     let type_error loc str =
193     Stdpp.raise_with_loc loc (RefineError ("type error", StringError str))
194    
195     (*
196     * Convert a list to a term list.
197     *)
198     let some_list_of_list f loc = function
199     ListExpr l ->
200     List.map f l
201     | _ ->
202     type_error loc "expr should be a list"
203    
204     let term_expr loc = function
205     TermExpr t ->
206     t
207     | _ ->
208     type_error loc "expr should be a term"
209    
210     let int_expr loc = function
211     IntExpr t ->
212     t
213     | _ ->
214     type_error loc "expr should be an int"
215    
216     let string_expr loc = function
217     StringExpr t ->
218     t
219     | _ ->
220     type_error loc "expr should be a string"
221    
222     let tactic_expr loc = function
223     TacticExpr t ->
224     t
225     | _ ->
226     type_error loc "expr should be a tactic"
227    
228     let conv_expr loc = function
229     ConvExpr t ->
230     t
231     | _ ->
232     type_error loc "expr should be a conv"
233    
234     let term_list_of_list loc = some_list_of_list (term_expr loc) loc
235     let int_list_of_list loc = some_list_of_list (int_expr loc) loc
236     let string_list_of_list loc = some_list_of_list (string_expr loc) loc
237     let tactic_list_of_list loc = some_list_of_list (tactic_expr loc) loc
238     let conv_list_of_list loc = some_list_of_list (conv_expr loc) loc
239    
240     (*
241     * Want an int tactic.
242     *)
243     let int_tactic_expr loc = function
244     IntFunExpr f ->
245     (fun i ->
246     match f i with
247     TacticExpr tac ->
248     tac
249     | _ ->
250     type_error loc "int tactic expected")
251     | _ ->
252     type_error loc "int tactic expected"
253    
254     (*
255     * Lookup a variable from the table.
256     *)
257     let rec mk_var_expr base loc v =
258     try snd (Hashtbl.find base v) with
259     Not_found ->
260     Stdpp.raise_with_loc loc (RefineError ("mk_var_expr", StringStringError ("undefined variable", v)))
261    
262     and mk_proj_expr base loc expr =
263     let rec search modname v = function
264     (modname', expr) :: tl ->
265     if modname' = modname then
266     expr
267     else
268     search modname v tl
269     | [] ->
270     Stdpp.raise_with_loc loc (**)
271     (RefineError ("mk_proj_expr",
272     StringStringError ("undefined variable", modname ^ "." ^ v)))
273     in
274     let lookup names v =
275     match names with
276     [modname] ->
277 nogin 3292 search modname v (Hashtbl.find_all base v)
278 jyh 2494 | _ ->
279     Stdpp.raise_with_loc loc (**)
280     (RefineError ("mk_proj_expr", StringError "nested modules are not implemented"))
281     in
282     let rec collect names expr =
283     match expr with
284     (<:expr< $uid: name$ . $e2$ >>) ->
285 nogin 2772 collect (name :: names) e2
286 jyh 2494 | (<:expr< $lid: v$ >>) ->
287     lookup names v
288     | _ ->
289     not_supported loc "expr projection"
290     in
291     collect [] expr
292    
293     (*
294     * For an application, we lookup the function and try to
295     * specialize the argument.
296     *)
297     and mk_apply_expr base loc f a =
298     let a = mk_expr base a in
299     match mk_expr base f with
300     FunExpr f ->
301     f a
302     | UnitFunExpr f ->
303     begin
304     match a with
305     UnitExpr () ->
306     f ()
307     | _ ->
308     type_error loc "expr should be unit"
309     end
310     | BoolFunExpr f ->
311     begin
312     match a with
313     BoolExpr a ->
314     f a
315     | _ ->
316     type_error loc "expr should be a bool"
317     end
318     | IntFunExpr f ->
319     begin
320     match a with
321     IntExpr a ->
322     f a
323     | _ ->
324     type_error loc "expr should be int"
325     end
326     | StringFunExpr f ->
327     begin
328     match a with
329     StringExpr a ->
330     f a
331     | _ ->
332     type_error loc "expr should be a string"
333     end
334     | TermFunExpr f ->
335     begin
336     match a with
337     TermExpr a ->
338     f a
339     | _ ->
340     type_error loc "expr should be a term"
341     end
342     | TacticFunExpr f ->
343     begin
344     match a with
345     TacticExpr a ->
346     f a
347     | _ ->
348     type_error loc "expr should be a tactic"
349     end
350     | IntTacticFunExpr f ->
351     f (int_tactic_expr loc a)
352     | ConvFunExpr f ->
353     begin
354     match a with
355     ConvExpr a ->
356     f a
357     | _ ->
358     type_error loc "expr should be a conversion"
359     end
360 jyh 2811 | AddressFunExpr f ->
361     begin
362     match a with
363     AddressExpr a ->
364     f a
365 nogin 3086 | IntExpr i ->
366     f (clause_address i)
367 nogin 3085 | ListExpr _ ->
368     f (make_address (int_list_of_list loc a))
369 jyh 2811 | _ ->
370 nogin 3085 type_error loc "expr should be an address"
371 jyh 2811 end
372 jyh 2494 | AddrFunExpr f ->
373     f (int_list_of_list loc a)
374     | StringListFunExpr f ->
375     f (string_list_of_list loc a)
376     | TermListFunExpr f ->
377     f (term_list_of_list loc a)
378     | TacticListFunExpr f ->
379     f (tactic_list_of_list loc a)
380     | ConvListFunExpr f ->
381     f (conv_list_of_list loc a)
382     | UnitExpr _
383     | BoolExpr _
384     | IntExpr _
385     | StringExpr _
386     | TermExpr _
387     | TacticExpr _
388     | ConvExpr _
389 jyh 2811 | AddressExpr _
390 jyh 2494 | ListExpr _
391     | TupleExpr _ ->
392     type_error loc "expr should be a function"
393    
394     (*
395     * A tuple of expressions.
396     * We only support unit for now.
397     *)
398     and mk_tuple_expr base loc = function
399     [] ->
400     UnitExpr ()
401     | _ ->
402     not_supported loc "tuple expression"
403    
404     and mk_expr base expr =
405     let loc = loc_of_expr expr in
406     match expr with
407     (<:expr< $e1$ . $e2$ >> as expr) ->
408     mk_proj_expr base loc expr
409     | (<:expr< $e1$ $e2$ >>) ->
410     mk_apply_expr base loc e1 e2
411     | (<:expr< $e1$ .( $e2$ ) >>) ->
412     not_supported loc "array subscript"
413     | (<:expr< [| $list:el$ |] >>) ->
414     not_supported loc "array"
415     | (<:expr< $e1$ := $e2$ >>) ->
416     not_supported loc "assignment"
417     | (<:expr< $chr:c$ >>) ->
418     not_supported loc "char"
419     (*
420     | (<:expr< ( $e$ :> $t$ ) >>) ->
421     *)
422     | MLast.ExCoe (_, e, t) ->
423     not_supported loc "class coercion"
424     | (<:expr< $flo:s$ >>) ->
425     not_supported loc "float"
426     | (<:expr< for $s$ = $e1$ $to:b$ $e2$ do $list:el$ done >>) ->
427     not_supported loc "for loop"
428     | (<:expr< fun [ $list:pwel$ ] >>) ->
429     not_supported loc "fun"
430     | (<:expr< if $e1$ then $e2$ else $e3$ >>) ->
431     not_supported loc "ifthenelse"
432     | (<:expr< $int:s$ >>) ->
433     IntExpr (int_of_string s)
434     | (<:expr< let $rec:b$ $list:pel$ in $e$ >>) ->
435     not_supported loc "let"
436     | (<:expr< $lid:s$ >>) ->
437     mk_var_expr base loc s
438     | MLast.ExLmd _ ->
439     not_supported loc "local module"
440     | (<:expr< match $e$ with [ $list:pwel$ ] >>) ->
441     not_supported loc "match"
442     (*
443     | (<:expr< new $e$ >>) ->
444     *)
445     | MLast.ExNew _ ->
446     not_supported loc "new"
447     (*
448     | (<:expr< {< $list:sel$ >} >>) ->
449     *)
450     | MLast.ExOvr _ ->
451     not_supported loc "stream"
452     (*
453     | (<:expr< { $list:eel$ } >>) ->
454     *)
455     | MLast.ExRec _ ->
456     not_supported loc "record"
457     | (<:expr< do $list:el$ return $e$ >>) ->
458     not_supported loc "do"
459     (*
460     | (<:expr< $e$ # $i$ >>) ->
461     *)
462     | MLast.ExSnd _ ->
463     not_supported loc "class projection"
464     | (<:expr< $e1$ .[ $e2$ ] >>) ->
465     not_supported loc "string subscript"
466     | (<:expr< $str:s$ >>) ->
467     StringExpr s
468     | (<:expr< try $e$ with [ $list:pwel$ ] >>) ->
469     not_supported loc "try"
470     | (<:expr< ( $list:el$ ) >>) ->
471     mk_tuple_expr base loc el
472     | (<:expr< ( $e$ : $t$ ) >>) ->
473     mk_expr base e
474     | (<:expr< $uid:s$ >>) ->
475 jyh 2525 mk_var_expr base loc s
476 jyh 2494 | (<:expr< while $e$ do $list:el$ done >>) ->
477     not_supported loc "while"
478     | MLast.ExAnt (_, e) ->
479     not_supported loc "ExAnt"
480 jyh 2629 | MLast.ExXnd (_, _, e) ->
481     mk_expr base e
482 jyh 2494
483     and mk_patt base patt =
484     let loc = loc_of_patt patt in
485     match patt with
486     (<:patt< $p1$ . $p2$ >>) ->
487     not_supported loc "patt projection"
488     | (<:patt< ( $p1$ as $p2$ ) >>) ->
489     not_supported loc "patt"
490     | (<:patt< _ >>) ->
491     not_supported loc "wild pattern"
492     | (<:patt< $p1$ $p2$ >>) ->
493     not_supported loc "pattern application"
494     | (<:patt< [| $list: pl$ |] >>) ->
495     not_supported loc "array patterns"
496     | (<:patt< $chr:c$ >>) ->
497     not_supported loc "pattern char"
498     | (<:patt< $int:s$ >>) ->
499     not_supported loc "pattern int"
500     | (<:patt< $lid:v$ >>) ->
501     not_supported loc "pattern var"
502     | (<:patt< $p1$ | $p2$ >>) ->
503     not_supported loc "pattern choice"
504     | (<:patt< $p1$ .. $p2$ >>) ->
505     not_supported loc "pattern range"
506     | (<:patt< { $list:ppl$ } >>) ->
507     not_supported loc "pattern list"
508     | (<:patt< $str:s$ >>) ->
509     not_supported loc "pattern string"
510     | (<:patt< ( $list:pl$ ) >>) ->
511     not_supported loc "pattern list"
512     | (<:patt< ( $p$ : $t'$ ) >>) ->
513     not_supported loc "pattern cast"
514     | (<:patt< $uid:s$ >>) ->
515     not_supported loc "pattern uid"
516     | MLast.PaAnt (_, p) ->
517     not_supported loc "pattern PaAnt"
518 jyh 2629 | MLast.PaXnd _ ->
519     not_supported loc "patterm PaXnd"
520 jyh 2494
521     and mk_type base t =
522     let loc = loc_of_ctyp t in
523     match t with
524     (<:ctyp< $t1$ . $t2$ >>) ->
525     not_supported loc "type projection"
526     | (<:ctyp< $t1$ as $t2$ >>) ->
527     not_supported loc "type"
528     | (<:ctyp< _ >>) ->
529     not_supported loc "type wildcard"
530     | (<:ctyp< $t1$ $t2$ >>) ->
531     not_supported loc "type application"
532     | (<:ctyp< $t1$ -> $t2$ >>) ->
533     not_supported loc "type function"
534     (*
535     | (<:ctyp< # $i$ >>) ->
536     *)
537     | MLast.TyCls _ ->
538     not_supported loc "type method"
539     | (<:ctyp< $lid:s$ >>) ->
540     not_supported loc "type var"
541     | (<:ctyp< '$s$ >>) ->
542     not_supported loc "type param"
543     | (<:ctyp< $t1$ == $t2$ >>) ->
544     not_supported loc "type equality"
545 jyh 2577 (*
546 jyh 2494 | (<:ctyp< < $list:stl$ $dd:b$ > >>) ->
547 jyh 2577 *)
548     | MLast.TyObj (loc, _, _) ->
549 jyh 2494 not_supported loc "type class"
550     | (<:ctyp< { $list:sbtl$ } >>) ->
551     not_supported loc "type record"
552     | (<:ctyp< [ $list:stll$ ] >>) ->
553     not_supported loc "type list"
554     | (<:ctyp< ( $list:tl$ ) >>) ->
555     not_supported loc "type product"
556     | (<:ctyp< $uid:s$ >>) ->
557     not_supported loc "type constructor var"
558 jyh 2629 | MLast.TyXnd (_, _, t) ->
559     mk_type base t
560 jyh 2494
561     and mk_sig_item base si =
562     let loc = loc_of_sig_item si in
563     match si with
564     (*
565     (<:sig_item< class $list:ctl$ >>) ->
566     *)
567     MLast.SgCls _
568     | MLast.SgClt _ ->
569     not_supported loc "sig class"
570     | (<:sig_item< declare $list:sil$ end >>) ->
571     mk_sig_item base (List_util.last sil)
572     | (<:sig_item< exception $s$ of $list:tl$ >>) ->
573     not_supported loc "sig exception"
574     | (<:sig_item< external $s$ : $t$ = $list:sl$ >>) ->
575     not_supported loc "sig external"
576     | SgInc (_, mt) ->
577     not_supported loc "sig SgInc"
578     | (<:sig_item< module $s$ : $mt$ >>) ->
579     not_supported loc "sig module"
580     | (<:sig_item< module type $s$ = $mt$ >>) ->
581     not_supported loc "sig module type"
582     | (<:sig_item< open $sl$ >>) ->
583     not_supported loc "sig open"
584 nogin 2859 | (<:sig_item< type $list:tdl$ >>) ->
585 jyh 2494 not_supported loc "sig type"
586     | (<:sig_item< value $s$ : $t$ >>) ->
587     not_supported loc "sig value"
588    
589     and mk_str_item base si =
590     let loc = loc_of_str_item si in
591     match si with
592     (*
593     (<:str_item< class $list:cdl$ >>) ->
594     *)
595     MLast.StCls _
596     | MLast.StClt _ ->
597     not_supported loc "str class"
598     | (<:str_item< declare $list:stl$ end >>) ->
599     mk_str_item base (List_util.last stl)
600     | (<:str_item< exception $s$ of $list:tl$ >>) ->
601     not_supported loc "str exception"
602     | (<:str_item< $exp:e$ >>) ->
603     mk_expr base e
604     | (<:str_item< external $s$ : $t$ = $list:sl$ >>) ->
605     not_supported loc "str external"
606     | (<:str_item< module $s$ = $me$ >>) ->
607     not_supported loc "str module"
608     | (<:str_item< module type $s$ = $mt$ >>) ->
609     not_supported loc "str module type"
610     | (<:str_item< open $sl$ >>) ->
611     not_supported loc "str module open"
612 nogin 2859 | (<:str_item< type $list:tdl$ >>) ->
613 jyh 2494 not_supported loc "str type"
614     | (<:str_item< value $rec:b$ $list:pel$ >>) ->
615     not_supported loc "str let"
616    
617     and mk_module_type base mt =
618     let loc = loc_of_module_type mt in
619     match mt with
620     (<:module_type< $mt1$ . $mt2$ >>) ->
621     not_supported loc "module type projection"
622     | (<:module_type< $mt1$ $mt2$ >>) ->
623     not_supported loc "module type application"
624     | (<:module_type< functor ( $s$ : $mt1$ ) -> $mt2$ >>) ->
625     not_supported loc "module type functor"
626     | (<:module_type< $lid:i$ >>) ->
627     not_supported loc "module type var"
628     | (<:module_type< sig $list:sil$ end >>) ->
629     not_supported loc "module type sig"
630     | (<:module_type< $uid:i$ >>) ->
631     not_supported loc "module type var"
632     | (<:module_type< $mt$ with $list:wcl$ >>) ->
633     not_supported loc "module type constraint"
634    
635     and mk_wc base = function
636     WcTyp (loc, sl1, sl2, t) ->
637     not_supported loc "with clause type"
638     | WcMod (loc, sl1, mt) ->
639     not_supported loc "with clause module"
640    
641     and mk_module_expr base me =
642     let loc = loc_of_module_expr me in
643     match me with
644     (<:module_expr< $me1$ . $me2$ >>) ->
645     not_supported loc "module expr projection"
646     | (<:module_expr< $me1$ $me2$ >>) ->
647     not_supported loc "module expr application"
648     | (<:module_expr< functor ( $s$ : $mt$ ) -> $me$ >>) ->
649     not_supported loc "module expr functor"
650     | (<:module_expr< struct $list:sil$ end >>) ->
651     not_supported loc "module expr struct"
652     | (<:module_expr< ( $me$ : $mt$) >>) ->
653     not_supported loc "module expr type"
654     | (<:module_expr< $uid:i$ >>) ->
655     not_supported loc "module expr id"
656    
657     (************************************************************************
658     * RESOURCES *
659     ************************************************************************)
660    
661     (*
662     * Include the common library functions.
663     *)
664     let int_int_fun_int_expr f =
665     IntFunExpr (fun i -> IntFunExpr (fun j -> IntExpr (f i j)))
666    
667 jyh 2525 let cons_expr =
668     FunExpr (fun e1 ->
669     FunExpr (fun e2 ->
670     match e2 with
671     ListExpr e2 ->
672     ListExpr (e1 :: e2)
673     | _ ->
674     raise (RefineError ("cons_expr", StringError "type mismatch"))))
675    
676 nogin 3292 let resource toploop +=
677     ["Pervasives", "+", int_int_fun_int_expr ( + );
678     "Pervasives", "-", int_int_fun_int_expr ( - );
679     "Pervasives", "*", int_int_fun_int_expr ( * );
680     "Pervasives", "/", int_int_fun_int_expr ( / );
681     "Pervasives", "::", cons_expr;
682     "Pervasives", "()", UnitExpr ();
683     "Pervasives", "[]", ListExpr [];
684     "Pervasives", "True", BoolExpr true;
685     "Pervasives", "False", BoolExpr false]
686 jyh 2494
687     let expr_of_ocaml_expr = mk_expr
688     let expr_of_ocaml_str_item = mk_str_item
689    
690     (*
691     * -*-
692     * Local Variables:
693     * Caml-master: "refiner"
694     * End:
695     * -*-
696     *)

Properties

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

  ViewVC Help
Powered by ViewVC 1.1.26