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

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

Parent Directory Parent Directory | Revision Log Revision Log


Revision 3278 - (show annotations) (download)
Wed Jun 20 00:27:36 2001 UTC (20 years, 1 month ago) by nogin
File size: 23396 byte(s)
- Changed the syntax of resource implementation. Now you no longer need to
re-declare resource types in the implementation. Instead of the declaration
and a Mp_resource.create call, use the following syntax in the implementation:

let resource <name> = <expr>

where <expr> is an expression that of the type Mp_resource.info

- Additionally, it is no longer necessary to use _resource in resource names
and resource annotations.

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