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

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

Parent Directory Parent Directory | Revision Log Revision Log


Revision 3410 - (hide annotations) (download)
Tue Sep 25 16:52:43 2001 UTC (19 years, 10 months ago) by nogin
File size: 22697 byte(s)
- Merged the Ocaml 3.02 changes

- Now http server is compiled in by default, but is only started if
the "-http true" argument is passed or MP_HTTP environment variable
is set to "true".

- A few other minor changes.

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 nogin 3294 Hashtbl.add tbl name ((String.capitalize 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 nogin 3410 | (<:expr< for $s$ = $e1$ $to:b$ $e2$ do { $list:el$ } >>) ->
427 jyh 2494 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 nogin 3410 | (<:expr< do { $list:el$ } >>) ->
458 jyh 2494 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 nogin 3410 | (<:expr< while $e$ do { $list:el$ } >>) ->
477 jyh 2494 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 nogin 3410 | MLast.ExVrn _ ->
483     not_supported loc "ExVrn"
484     | MLast.ExOlb _ ->
485     not_supported loc "ExOlb"
486     | MLast.ExLab _ ->
487     not_supported loc "ExLab"
488 jyh 2494
489     and mk_patt base patt =
490     let loc = loc_of_patt patt in
491     match patt with
492     (<:patt< $p1$ . $p2$ >>) ->
493     not_supported loc "patt projection"
494     | (<:patt< ( $p1$ as $p2$ ) >>) ->
495     not_supported loc "patt"
496     | (<:patt< _ >>) ->
497     not_supported loc "wild pattern"
498     | (<:patt< $p1$ $p2$ >>) ->
499     not_supported loc "pattern application"
500     | (<:patt< [| $list: pl$ |] >>) ->
501     not_supported loc "array patterns"
502     | (<:patt< $chr:c$ >>) ->
503     not_supported loc "pattern char"
504     | (<:patt< $int:s$ >>) ->
505     not_supported loc "pattern int"
506     | (<:patt< $lid:v$ >>) ->
507     not_supported loc "pattern var"
508     | (<:patt< $p1$ | $p2$ >>) ->
509     not_supported loc "pattern choice"
510     | (<:patt< $p1$ .. $p2$ >>) ->
511     not_supported loc "pattern range"
512     | (<:patt< { $list:ppl$ } >>) ->
513     not_supported loc "pattern list"
514     | (<:patt< $str:s$ >>) ->
515     not_supported loc "pattern string"
516     | (<:patt< ( $list:pl$ ) >>) ->
517     not_supported loc "pattern list"
518     | (<:patt< ( $p$ : $t'$ ) >>) ->
519     not_supported loc "pattern cast"
520     | (<:patt< $uid:s$ >>) ->
521     not_supported loc "pattern uid"
522     | MLast.PaAnt (_, p) ->
523     not_supported loc "pattern PaAnt"
524 jyh 2629 | MLast.PaXnd _ ->
525     not_supported loc "patterm PaXnd"
526 nogin 3410 | MLast.PaVrn _ ->
527     not_supported loc "patterm PaVrn"
528     | MLast.PaOlb _ ->
529     not_supported loc "patterm PaOlb"
530     | MLast.PaLab _ ->
531     not_supported loc "patterm PaLab"
532     | MLast.PaFlo _ ->
533     not_supported loc "patterm PaFlo"
534 jyh 2494
535     and mk_type base t =
536     let loc = loc_of_ctyp t in
537     match t with
538     (<:ctyp< $t1$ . $t2$ >>) ->
539     not_supported loc "type projection"
540     | (<:ctyp< $t1$ as $t2$ >>) ->
541     not_supported loc "type"
542     | (<:ctyp< _ >>) ->
543     not_supported loc "type wildcard"
544     | (<:ctyp< $t1$ $t2$ >>) ->
545     not_supported loc "type application"
546     | (<:ctyp< $t1$ -> $t2$ >>) ->
547     not_supported loc "type function"
548     (*
549     | (<:ctyp< # $i$ >>) ->
550     *)
551     | MLast.TyCls _ ->
552     not_supported loc "type method"
553     | (<:ctyp< $lid:s$ >>) ->
554     not_supported loc "type var"
555     | (<:ctyp< '$s$ >>) ->
556     not_supported loc "type param"
557     | (<:ctyp< $t1$ == $t2$ >>) ->
558     not_supported loc "type equality"
559 jyh 2577 (*
560 jyh 2494 | (<:ctyp< < $list:stl$ $dd:b$ > >>) ->
561 jyh 2577 *)
562     | MLast.TyObj (loc, _, _) ->
563 jyh 2494 not_supported loc "type class"
564     | (<:ctyp< { $list:sbtl$ } >>) ->
565     not_supported loc "type record"
566     | (<:ctyp< [ $list:stll$ ] >>) ->
567     not_supported loc "type list"
568     | (<:ctyp< ( $list:tl$ ) >>) ->
569     not_supported loc "type product"
570     | (<:ctyp< $uid:s$ >>) ->
571     not_supported loc "type constructor var"
572 jyh 2629 | MLast.TyXnd (_, _, t) ->
573     mk_type base t
574 nogin 3410 | MLast.TyVrn _ ->
575     not_supported loc "type constructor Vrn"
576     | MLast.TyOlb _ ->
577     not_supported loc "type constructor Olb"
578     | MLast.TyLab _ ->
579     not_supported loc "type constructor Lab"
580 jyh 2494
581     and mk_sig_item base si =
582     let loc = loc_of_sig_item si in
583     match si with
584     (*
585     (<:sig_item< class $list:ctl$ >>) ->
586     *)
587     MLast.SgCls _
588     | MLast.SgClt _ ->
589     not_supported loc "sig class"
590     | (<:sig_item< declare $list:sil$ end >>) ->
591     mk_sig_item base (List_util.last sil)
592     | (<:sig_item< exception $s$ of $list:tl$ >>) ->
593     not_supported loc "sig exception"
594     | (<:sig_item< external $s$ : $t$ = $list:sl$ >>) ->
595     not_supported loc "sig external"
596     | SgInc (_, mt) ->
597     not_supported loc "sig SgInc"
598     | (<:sig_item< module $s$ : $mt$ >>) ->
599     not_supported loc "sig module"
600     | (<:sig_item< module type $s$ = $mt$ >>) ->
601     not_supported loc "sig module type"
602     | (<:sig_item< open $sl$ >>) ->
603     not_supported loc "sig open"
604 nogin 2859 | (<:sig_item< type $list:tdl$ >>) ->
605 jyh 2494 not_supported loc "sig type"
606     | (<:sig_item< value $s$ : $t$ >>) ->
607     not_supported loc "sig value"
608 nogin 3410 | MLast.SgDir _ ->
609     not_supported loc "sig dir"
610 jyh 2494
611     and mk_str_item base si =
612     let loc = loc_of_str_item si in
613     match si with
614     MLast.StCls _
615     | MLast.StClt _ ->
616     not_supported loc "str class"
617     | (<:str_item< declare $list:stl$ end >>) ->
618     mk_str_item base (List_util.last stl)
619     | (<:str_item< exception $s$ of $list:tl$ >>) ->
620     not_supported loc "str exception"
621     | (<:str_item< $exp:e$ >>) ->
622     mk_expr base e
623     | (<:str_item< external $s$ : $t$ = $list:sl$ >>) ->
624     not_supported loc "str external"
625     | (<:str_item< module $s$ = $me$ >>) ->
626     not_supported loc "str module"
627     | (<:str_item< module type $s$ = $mt$ >>) ->
628     not_supported loc "str module type"
629     | (<:str_item< open $sl$ >>) ->
630     not_supported loc "str module open"
631 nogin 2859 | (<:str_item< type $list:tdl$ >>) ->
632 jyh 2494 not_supported loc "str type"
633     | (<:str_item< value $rec:b$ $list:pel$ >>) ->
634     not_supported loc "str let"
635 nogin 3410 | MLast.StDir _ ->
636     not_supported loc "str dir"
637     | MLast.StInc _ ->
638     not_supported loc "str include"
639 jyh 2494
640     and mk_module_type base mt =
641     let loc = loc_of_module_type mt in
642     match mt with
643     (<:module_type< $mt1$ . $mt2$ >>) ->
644     not_supported loc "module type projection"
645     | (<:module_type< $mt1$ $mt2$ >>) ->
646     not_supported loc "module type application"
647     | (<:module_type< functor ( $s$ : $mt1$ ) -> $mt2$ >>) ->
648     not_supported loc "module type functor"
649     | (<:module_type< $lid:i$ >>) ->
650     not_supported loc "module type var"
651     | (<:module_type< sig $list:sil$ end >>) ->
652     not_supported loc "module type sig"
653     | (<:module_type< $uid:i$ >>) ->
654     not_supported loc "module type var"
655     | (<:module_type< $mt$ with $list:wcl$ >>) ->
656     not_supported loc "module type constraint"
657    
658     and mk_wc base = function
659     WcTyp (loc, sl1, sl2, t) ->
660     not_supported loc "with clause type"
661     | WcMod (loc, sl1, mt) ->
662     not_supported loc "with clause module"
663    
664     and mk_module_expr base me =
665     let loc = loc_of_module_expr me in
666     match me with
667     (<:module_expr< $me1$ . $me2$ >>) ->
668     not_supported loc "module expr projection"
669     | (<:module_expr< $me1$ $me2$ >>) ->
670     not_supported loc "module expr application"
671     | (<:module_expr< functor ( $s$ : $mt$ ) -> $me$ >>) ->
672     not_supported loc "module expr functor"
673     | (<:module_expr< struct $list:sil$ end >>) ->
674     not_supported loc "module expr struct"
675     | (<:module_expr< ( $me$ : $mt$) >>) ->
676     not_supported loc "module expr type"
677     | (<:module_expr< $uid:i$ >>) ->
678     not_supported loc "module expr id"
679    
680     (************************************************************************
681     * RESOURCES *
682     ************************************************************************)
683    
684     (*
685     * Include the common library functions.
686     *)
687     let int_int_fun_int_expr f =
688     IntFunExpr (fun i -> IntFunExpr (fun j -> IntExpr (f i j)))
689    
690 jyh 2525 let cons_expr =
691     FunExpr (fun e1 ->
692     FunExpr (fun e2 ->
693     match e2 with
694     ListExpr e2 ->
695     ListExpr (e1 :: e2)
696     | _ ->
697     raise (RefineError ("cons_expr", StringError "type mismatch"))))
698    
699 nogin 3292 let resource toploop +=
700     ["Pervasives", "+", int_int_fun_int_expr ( + );
701     "Pervasives", "-", int_int_fun_int_expr ( - );
702     "Pervasives", "*", int_int_fun_int_expr ( * );
703     "Pervasives", "/", int_int_fun_int_expr ( / );
704     "Pervasives", "::", cons_expr;
705     "Pervasives", "()", UnitExpr ();
706     "Pervasives", "[]", ListExpr [];
707     "Pervasives", "True", BoolExpr true;
708     "Pervasives", "False", BoolExpr false]
709 jyh 2494
710     let expr_of_ocaml_expr = mk_expr
711     let expr_of_ocaml_str_item = mk_str_item
712    
713     (*
714     * -*-
715     * Local Variables:
716     * Caml-master: "refiner"
717     * End:
718     * -*-
719     *)

Properties

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

  ViewVC Help
Powered by ViewVC 1.1.26