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

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

Parent Directory Parent Directory | Revision Log Revision Log


Revision 3085 - (show annotations) (download)
Wed Oct 18 21:32:01 2000 UTC (20 years, 9 months ago) by nogin
File size: 23407 byte(s)
Fixed Yegor's typos that prevented MetaPRL from staring (Yegor, please
take a look at my changes)

Other minor fixes.

1 (*!
2 * @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
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 *
28 * 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 *
33 * 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 *
38 * 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 *
42 * Author: Jason Hickey
43 * @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
57
58 open Refiner.Refiner.TermType
59 open Refiner.Refiner.TermAddr
60 open Refiner.Refiner.RefineError
61 open Mp_resource
62
63 open Tactic_type.Tacticals
64 open Tactic_type.Conversionals
65
66 (************************************************************************
67 * TYPES *
68 ************************************************************************)
69
70 (*!
71 * @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 =
113 (* Base types *)
114 UnitExpr of unit
115 | BoolExpr of bool
116 | IntExpr of int
117 | StringExpr of string
118 | TermExpr of term
119 | TacticExpr of tactic
120 | ConvExpr of conv
121 | AddressExpr of address
122
123 (* Uptyped tuples and functions *)
124 | ListExpr of expr list
125 | TupleExpr of expr list
126 | FunExpr of (expr -> expr)
127
128 (* Common cases are typed *)
129 | UnitFunExpr of (unit -> expr)
130 | BoolFunExpr of (bool -> expr)
131 | IntFunExpr of (int -> expr)
132 | StringFunExpr of (string -> expr)
133 | TermFunExpr of (term -> expr)
134 | TacticFunExpr of (tactic -> expr)
135 | IntTacticFunExpr of ((int -> tactic) -> expr)
136 | ConvFunExpr of (conv -> expr)
137 | AddressFunExpr of (address -> expr)
138
139 (* These functions take lists *)
140 | AddrFunExpr of (int list -> expr)
141 | StringListFunExpr of (string list -> expr)
142 | TermListFunExpr of (term list -> expr)
143 | TacticListFunExpr of (tactic list -> expr)
144 | ConvListFunExpr of (conv list -> expr)
145
146 (*
147 * The resource maps strings to values.
148 *)
149 type top_data =
150 Empty
151 | Label of string * top_data
152 | Expr of string * expr * top_data
153 | Join of top_data * top_data
154
155 type top_table =
156 (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
167
168 (************************************************************************
169 * IMPLEMENTATION *
170 ************************************************************************)
171
172 (*
173 * Construct a hash table of all the values.
174 * As in ML, the newer values override the previous.
175 *)
176 let collect_table data =
177 let hash = Hashtbl.create 201 in
178 let rec collect mod_name labels = function
179 Empty ->
180 labels
181 | (Label (mod_name, next)) as label ->
182 if List.memq label labels then
183 labels
184 else
185 collect mod_name (label :: labels) next
186 | Expr (name, expr, next) ->
187 let labels = collect mod_name labels next in
188 Hashtbl.add hash name (mod_name, expr);
189 labels
190
191 | Join (next1, next2) ->
192 let labels = collect mod_name labels next1 in
193 collect mod_name labels next2
194 in
195 let _ = collect "." [] data in
196 hash
197
198 (*
199 * Wrap up the joiner.
200 *)
201 let join_resource base1 base2 =
202 Join (base1, base2)
203
204 let extract_resource data =
205 collect_table data
206
207 let improve_resource data (name, expr) =
208 Expr (name, expr, data)
209
210 let close_resource data mod_name =
211 Label (String.capitalize mod_name, data)
212
213 (************************************************************************
214 * COMPILING *
215 ************************************************************************)
216
217 (*
218 * Right now most things are not supported.
219 *)
220 let not_supported loc str =
221 Stdpp.raise_with_loc loc (RefineError ("mptop", StringStringError ("operation is not implemented", str)))
222
223 let type_error loc str =
224 Stdpp.raise_with_loc loc (RefineError ("type error", StringError str))
225
226 (*
227 * Convert a list to a term list.
228 *)
229 let some_list_of_list f loc = function
230 ListExpr l ->
231 List.map f l
232 | _ ->
233 type_error loc "expr should be a list"
234
235 let term_expr loc = function
236 TermExpr t ->
237 t
238 | _ ->
239 type_error loc "expr should be a term"
240
241 let int_expr loc = function
242 IntExpr t ->
243 t
244 | _ ->
245 type_error loc "expr should be an int"
246
247 let string_expr loc = function
248 StringExpr t ->
249 t
250 | _ ->
251 type_error loc "expr should be a string"
252
253 let tactic_expr loc = function
254 TacticExpr t ->
255 t
256 | _ ->
257 type_error loc "expr should be a tactic"
258
259 let conv_expr loc = function
260 ConvExpr t ->
261 t
262 | _ ->
263 type_error loc "expr should be a conv"
264
265 let term_list_of_list loc = some_list_of_list (term_expr loc) loc
266 let int_list_of_list loc = some_list_of_list (int_expr loc) loc
267 let string_list_of_list loc = some_list_of_list (string_expr loc) loc
268 let tactic_list_of_list loc = some_list_of_list (tactic_expr loc) loc
269 let conv_list_of_list loc = some_list_of_list (conv_expr loc) loc
270
271 (*
272 * Want an int tactic.
273 *)
274 let int_tactic_expr loc = function
275 IntFunExpr f ->
276 (fun i ->
277 match f i with
278 TacticExpr tac ->
279 tac
280 | _ ->
281 type_error loc "int tactic expected")
282 | _ ->
283 type_error loc "int tactic expected"
284
285 (*
286 * Lookup a variable from the table.
287 *)
288 let rec mk_var_expr base loc v =
289 try snd (Hashtbl.find base v) with
290 Not_found ->
291 Stdpp.raise_with_loc loc (RefineError ("mk_var_expr", StringStringError ("undefined variable", v)))
292
293 and mk_proj_expr base loc expr =
294 let rec search modname v = function
295 (modname', expr) :: tl ->
296 if modname' = modname then
297 expr
298 else
299 search modname v tl
300 | [] ->
301 Stdpp.raise_with_loc loc (**)
302 (RefineError ("mk_proj_expr",
303 StringStringError ("undefined variable", modname ^ "." ^ v)))
304 in
305 let lookup names v =
306 match names with
307 [modname] ->
308 begin
309 try search modname v (Hashtbl.find_all base v) with
310 Not_found ->
311 Stdpp.raise_with_loc loc (**)
312 (RefineError ("mk_proj_expr",
313 StringStringError ("undefined variable", modname ^ "." ^ v)))
314 end
315 | _ ->
316 Stdpp.raise_with_loc loc (**)
317 (RefineError ("mk_proj_expr", StringError "nested modules are not implemented"))
318 in
319 let rec collect names expr =
320 match expr with
321 (<:expr< $uid: name$ . $e2$ >>) ->
322 collect (name :: names) e2
323 | (<:expr< $lid: v$ >>) ->
324 lookup names v
325 | _ ->
326 not_supported loc "expr projection"
327 in
328 collect [] expr
329
330 (*
331 * For an application, we lookup the function and try to
332 * specialize the argument.
333 *)
334 and mk_apply_expr base loc f a =
335 let a = mk_expr base a in
336 match mk_expr base f with
337 FunExpr f ->
338 f a
339 | UnitFunExpr f ->
340 begin
341 match a with
342 UnitExpr () ->
343 f ()
344 | _ ->
345 type_error loc "expr should be unit"
346 end
347 | BoolFunExpr f ->
348 begin
349 match a with
350 BoolExpr a ->
351 f a
352 | _ ->
353 type_error loc "expr should be a bool"
354 end
355 | IntFunExpr f ->
356 begin
357 match a with
358 IntExpr a ->
359 f a
360 | _ ->
361 type_error loc "expr should be int"
362 end
363 | StringFunExpr f ->
364 begin
365 match a with
366 StringExpr a ->
367 f a
368 | _ ->
369 type_error loc "expr should be a string"
370 end
371 | TermFunExpr f ->
372 begin
373 match a with
374 TermExpr a ->
375 f a
376 | _ ->
377 type_error loc "expr should be a term"
378 end
379 | TacticFunExpr f ->
380 begin
381 match a with
382 TacticExpr a ->
383 f a
384 | _ ->
385 type_error loc "expr should be a tactic"
386 end
387 | IntTacticFunExpr f ->
388 f (int_tactic_expr loc a)
389 | ConvFunExpr f ->
390 begin
391 match a with
392 ConvExpr a ->
393 f a
394 | _ ->
395 type_error loc "expr should be a conversion"
396 end
397 | AddressFunExpr f ->
398 begin
399 match a with
400 AddressExpr a ->
401 f a
402 | ListExpr _ ->
403 f (make_address (int_list_of_list loc a))
404 | _ ->
405 type_error loc "expr should be an address"
406 end
407 | AddrFunExpr f ->
408 f (int_list_of_list loc a)
409 | StringListFunExpr f ->
410 f (string_list_of_list loc a)
411 | TermListFunExpr f ->
412 f (term_list_of_list loc a)
413 | TacticListFunExpr f ->
414 f (tactic_list_of_list loc a)
415 | ConvListFunExpr f ->
416 f (conv_list_of_list loc a)
417 | UnitExpr _
418 | BoolExpr _
419 | IntExpr _
420 | StringExpr _
421 | TermExpr _
422 | TacticExpr _
423 | ConvExpr _
424 | AddressExpr _
425 | ListExpr _
426 | TupleExpr _ ->
427 type_error loc "expr should be a function"
428
429 (*
430 * A tuple of expressions.
431 * We only support unit for now.
432 *)
433 and mk_tuple_expr base loc = function
434 [] ->
435 UnitExpr ()
436 | _ ->
437 not_supported loc "tuple expression"
438
439 and mk_expr base expr =
440 let loc = loc_of_expr expr in
441 match expr with
442 (<:expr< $e1$ . $e2$ >> as expr) ->
443 mk_proj_expr base loc expr
444 | (<:expr< $e1$ $e2$ >>) ->
445 mk_apply_expr base loc e1 e2
446 | (<:expr< $e1$ .( $e2$ ) >>) ->
447 not_supported loc "array subscript"
448 | (<:expr< [| $list:el$ |] >>) ->
449 not_supported loc "array"
450 | (<:expr< $e1$ := $e2$ >>) ->
451 not_supported loc "assignment"
452 | (<:expr< $chr:c$ >>) ->
453 not_supported loc "char"
454 (*
455 | (<:expr< ( $e$ :> $t$ ) >>) ->
456 *)
457 | MLast.ExCoe (_, e, t) ->
458 not_supported loc "class coercion"
459 | (<:expr< $flo:s$ >>) ->
460 not_supported loc "float"
461 | (<:expr< for $s$ = $e1$ $to:b$ $e2$ do $list:el$ done >>) ->
462 not_supported loc "for loop"
463 | (<:expr< fun [ $list:pwel$ ] >>) ->
464 not_supported loc "fun"
465 | (<:expr< if $e1$ then $e2$ else $e3$ >>) ->
466 not_supported loc "ifthenelse"
467 | (<:expr< $int:s$ >>) ->
468 IntExpr (int_of_string s)
469 | (<:expr< let $rec:b$ $list:pel$ in $e$ >>) ->
470 not_supported loc "let"
471 | (<:expr< $lid:s$ >>) ->
472 mk_var_expr base loc s
473 | MLast.ExLmd _ ->
474 not_supported loc "local module"
475 | (<:expr< match $e$ with [ $list:pwel$ ] >>) ->
476 not_supported loc "match"
477 (*
478 | (<:expr< new $e$ >>) ->
479 *)
480 | MLast.ExNew _ ->
481 not_supported loc "new"
482 (*
483 | (<:expr< {< $list:sel$ >} >>) ->
484 *)
485 | MLast.ExOvr _ ->
486 not_supported loc "stream"
487 (*
488 | (<:expr< { $list:eel$ } >>) ->
489 *)
490 | MLast.ExRec _ ->
491 not_supported loc "record"
492 | (<:expr< do $list:el$ return $e$ >>) ->
493 not_supported loc "do"
494 (*
495 | (<:expr< $e$ # $i$ >>) ->
496 *)
497 | MLast.ExSnd _ ->
498 not_supported loc "class projection"
499 | (<:expr< $e1$ .[ $e2$ ] >>) ->
500 not_supported loc "string subscript"
501 | (<:expr< $str:s$ >>) ->
502 StringExpr s
503 | (<:expr< try $e$ with [ $list:pwel$ ] >>) ->
504 not_supported loc "try"
505 | (<:expr< ( $list:el$ ) >>) ->
506 mk_tuple_expr base loc el
507 | (<:expr< ( $e$ : $t$ ) >>) ->
508 mk_expr base e
509 | (<:expr< $uid:s$ >>) ->
510 mk_var_expr base loc s
511 | (<:expr< while $e$ do $list:el$ done >>) ->
512 not_supported loc "while"
513 | MLast.ExAnt (_, e) ->
514 not_supported loc "ExAnt"
515 | MLast.ExXnd (_, _, e) ->
516 mk_expr base e
517
518 and mk_patt base patt =
519 let loc = loc_of_patt patt in
520 match patt with
521 (<:patt< $p1$ . $p2$ >>) ->
522 not_supported loc "patt projection"
523 | (<:patt< ( $p1$ as $p2$ ) >>) ->
524 not_supported loc "patt"
525 | (<:patt< _ >>) ->
526 not_supported loc "wild pattern"
527 | (<:patt< $p1$ $p2$ >>) ->
528 not_supported loc "pattern application"
529 | (<:patt< [| $list: pl$ |] >>) ->
530 not_supported loc "array patterns"
531 | (<:patt< $chr:c$ >>) ->
532 not_supported loc "pattern char"
533 | (<:patt< $int:s$ >>) ->
534 not_supported loc "pattern int"
535 | (<:patt< $lid:v$ >>) ->
536 not_supported loc "pattern var"
537 | (<:patt< $p1$ | $p2$ >>) ->
538 not_supported loc "pattern choice"
539 | (<:patt< $p1$ .. $p2$ >>) ->
540 not_supported loc "pattern range"
541 | (<:patt< { $list:ppl$ } >>) ->
542 not_supported loc "pattern list"
543 | (<:patt< $str:s$ >>) ->
544 not_supported loc "pattern string"
545 | (<:patt< ( $list:pl$ ) >>) ->
546 not_supported loc "pattern list"
547 | (<:patt< ( $p$ : $t'$ ) >>) ->
548 not_supported loc "pattern cast"
549 | (<:patt< $uid:s$ >>) ->
550 not_supported loc "pattern uid"
551 | MLast.PaAnt (_, p) ->
552 not_supported loc "pattern PaAnt"
553 | MLast.PaXnd _ ->
554 not_supported loc "patterm PaXnd"
555
556 and mk_type base t =
557 let loc = loc_of_ctyp t in
558 match t with
559 (<:ctyp< $t1$ . $t2$ >>) ->
560 not_supported loc "type projection"
561 | (<:ctyp< $t1$ as $t2$ >>) ->
562 not_supported loc "type"
563 | (<:ctyp< _ >>) ->
564 not_supported loc "type wildcard"
565 | (<:ctyp< $t1$ $t2$ >>) ->
566 not_supported loc "type application"
567 | (<:ctyp< $t1$ -> $t2$ >>) ->
568 not_supported loc "type function"
569 (*
570 | (<:ctyp< # $i$ >>) ->
571 *)
572 | MLast.TyCls _ ->
573 not_supported loc "type method"
574 | (<:ctyp< $lid:s$ >>) ->
575 not_supported loc "type var"
576 | (<:ctyp< '$s$ >>) ->
577 not_supported loc "type param"
578 | (<:ctyp< $t1$ == $t2$ >>) ->
579 not_supported loc "type equality"
580 (*
581 | (<:ctyp< < $list:stl$ $dd:b$ > >>) ->
582 *)
583 | MLast.TyObj (loc, _, _) ->
584 not_supported loc "type class"
585 | (<:ctyp< { $list:sbtl$ } >>) ->
586 not_supported loc "type record"
587 | (<:ctyp< [ $list:stll$ ] >>) ->
588 not_supported loc "type list"
589 | (<:ctyp< ( $list:tl$ ) >>) ->
590 not_supported loc "type product"
591 | (<:ctyp< $uid:s$ >>) ->
592 not_supported loc "type constructor var"
593 | MLast.TyXnd (_, _, t) ->
594 mk_type base t
595
596 and mk_sig_item base si =
597 let loc = loc_of_sig_item si in
598 match si with
599 (*
600 (<:sig_item< class $list:ctl$ >>) ->
601 *)
602 MLast.SgCls _
603 | MLast.SgClt _ ->
604 not_supported loc "sig class"
605 | (<:sig_item< declare $list:sil$ end >>) ->
606 mk_sig_item base (List_util.last sil)
607 | (<:sig_item< exception $s$ of $list:tl$ >>) ->
608 not_supported loc "sig exception"
609 | (<:sig_item< external $s$ : $t$ = $list:sl$ >>) ->
610 not_supported loc "sig external"
611 | SgInc (_, mt) ->
612 not_supported loc "sig SgInc"
613 | (<:sig_item< module $s$ : $mt$ >>) ->
614 not_supported loc "sig module"
615 | (<:sig_item< module type $s$ = $mt$ >>) ->
616 not_supported loc "sig module type"
617 | (<:sig_item< open $sl$ >>) ->
618 not_supported loc "sig open"
619 | (<:sig_item< type $list:tdl$ >>) ->
620 not_supported loc "sig type"
621 | (<:sig_item< value $s$ : $t$ >>) ->
622 not_supported loc "sig value"
623
624 and mk_str_item base si =
625 let loc = loc_of_str_item si in
626 match si with
627 (*
628 (<:str_item< class $list:cdl$ >>) ->
629 *)
630 MLast.StCls _
631 | MLast.StClt _ ->
632 not_supported loc "str class"
633 | (<:str_item< declare $list:stl$ end >>) ->
634 mk_str_item base (List_util.last stl)
635 | (<:str_item< exception $s$ of $list:tl$ >>) ->
636 not_supported loc "str exception"
637 | (<:str_item< $exp:e$ >>) ->
638 mk_expr base e
639 | (<:str_item< external $s$ : $t$ = $list:sl$ >>) ->
640 not_supported loc "str external"
641 | (<:str_item< module $s$ = $me$ >>) ->
642 not_supported loc "str module"
643 | (<:str_item< module type $s$ = $mt$ >>) ->
644 not_supported loc "str module type"
645 | (<:str_item< open $sl$ >>) ->
646 not_supported loc "str module open"
647 | (<:str_item< type $list:tdl$ >>) ->
648 not_supported loc "str type"
649 | (<:str_item< value $rec:b$ $list:pel$ >>) ->
650 not_supported loc "str let"
651
652 and mk_module_type base mt =
653 let loc = loc_of_module_type mt in
654 match mt with
655 (<:module_type< $mt1$ . $mt2$ >>) ->
656 not_supported loc "module type projection"
657 | (<:module_type< $mt1$ $mt2$ >>) ->
658 not_supported loc "module type application"
659 | (<:module_type< functor ( $s$ : $mt1$ ) -> $mt2$ >>) ->
660 not_supported loc "module type functor"
661 | (<:module_type< $lid:i$ >>) ->
662 not_supported loc "module type var"
663 | (<:module_type< sig $list:sil$ end >>) ->
664 not_supported loc "module type sig"
665 | (<:module_type< $uid:i$ >>) ->
666 not_supported loc "module type var"
667 | (<:module_type< $mt$ with $list:wcl$ >>) ->
668 not_supported loc "module type constraint"
669
670 and mk_wc base = function
671 WcTyp (loc, sl1, sl2, t) ->
672 not_supported loc "with clause type"
673 | WcMod (loc, sl1, mt) ->
674 not_supported loc "with clause module"
675
676 and mk_module_expr base me =
677 let loc = loc_of_module_expr me in
678 match me with
679 (<:module_expr< $me1$ . $me2$ >>) ->
680 not_supported loc "module expr projection"
681 | (<:module_expr< $me1$ $me2$ >>) ->
682 not_supported loc "module expr application"
683 | (<:module_expr< functor ( $s$ : $mt$ ) -> $me$ >>) ->
684 not_supported loc "module expr functor"
685 | (<:module_expr< struct $list:sil$ end >>) ->
686 not_supported loc "module expr struct"
687 | (<:module_expr< ( $me$ : $mt$) >>) ->
688 not_supported loc "module expr type"
689 | (<:module_expr< $uid:i$ >>) ->
690 not_supported loc "module expr id"
691
692 (************************************************************************
693 * RESOURCES *
694 ************************************************************************)
695
696 (*
697 * Include the common library functions.
698 *)
699 let int_int_fun_int_expr f =
700 IntFunExpr (fun i -> IntFunExpr (fun j -> IntExpr (f i j)))
701
702 let cons_expr =
703 FunExpr (fun e1 ->
704 FunExpr (fun e2 ->
705 match e2 with
706 ListExpr e2 ->
707 ListExpr (e1 :: e2)
708 | _ ->
709 raise (RefineError ("cons_expr", StringError "type mismatch"))))
710
711 let values =
712 ["+", int_int_fun_int_expr ( + );
713 "-", int_int_fun_int_expr ( - );
714 "*", int_int_fun_int_expr ( * );
715 "/", int_int_fun_int_expr ( / );
716 "::", cons_expr;
717 "()", UnitExpr ();
718 "[]", ListExpr [];
719 "True", BoolExpr true;
720 "False", BoolExpr false]
721
722
723 let rec add_resources base = function
724 (name, expr) :: tl ->
725 add_resources (Expr (name, expr, base)) tl
726 | [] ->
727 base
728
729 let toploop_resource =
730 Mp_resource.create (**)
731 { resource_join = join_resource;
732 resource_extract = extract_resource;
733 resource_improve = improve_resource;
734 resource_improve_arg = Mp_resource.improve_arg_fail "toploop_resource";
735 resource_close = close_resource
736 }
737 (add_resources Empty values)
738
739 let get_resource modname =
740 Mp_resource.find toploop_resource modname
741
742 let expr_of_ocaml_expr = mk_expr
743 let expr_of_ocaml_str_item = mk_str_item
744
745 (*
746 * -*-
747 * Local Variables:
748 * Caml-master: "refiner"
749 * End:
750 * -*-
751 *)

Properties

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

  ViewVC Help
Powered by ViewVC 1.1.26