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

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

Parent Directory Parent Directory | Revision Log Revision Log


Revision 3584 - (show annotations) (download)
Thu Apr 25 15:28:40 2002 UTC (19 years, 3 months ago) by nogin
File size: 22584 byte(s)
- Added the comment module to the theories.pdf ("make latex").

- Added a hack allowing to override a theory display with another theory's
display. This is necessary for bootstrapping reasons - it allows one
to get a reasonable output of a theory (e.g. Comment) that is defined before
all essential display forms (e.g. the Summary ones) are there.

- Added debugging code to make it easier to find dforms that cause
zone begin/end mismatch (and used it to get rid of all
the "Unballanced buffer" warnings in "make latex").

- Minor dforms&comments updates.

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 (* XXX Bootstrapping HACK *)
68 let _ = Theory.substitute_dforms "comment" "summary"
69
70 (************************************************************************
71 * TYPES *
72 ************************************************************************)
73
74 (*!
75 * @begin[doc]
76 * The valid expression types are given with the following type
77 * definition.
78 *
79 * @begin[verbatim]
80 * type expr =
81 * (* Base types *)
82 * UnitExpr of unit
83 * | BoolExpr of bool
84 * | IntExpr of int
85 * | StringExpr of string
86 * | TermExpr of term
87 * | TacticExpr of tactic
88 * | ConvExpr of conv
89 * | AddressExpr of address
90 *
91 * (* Untyped tuples and functions *)
92 * | ListExpr of expr list
93 * | TupleExpr of expr list
94 * | FunExpr of (expr -> expr)
95 *
96 * (* Common cases are typed *)
97 * | UnitFunExpr of (unit -> expr)
98 * | BoolFunExpr of (bool -> expr)
99 * | IntFunExpr of (int -> expr)
100 * | StringFunExpr of (string -> expr)
101 * | TermFunExpr of (term -> expr)
102 * | TacticFunExpr of (tactic -> expr)
103 * | IntTacticFunExpr of ((int -> tactic) -> expr)
104 * | ConvFunExpr of (conv -> expr)
105 * | AddressFunExpr of (address -> expr)
106 *
107 * (* These functions take lists *)
108 * | AddrFunExpr of (int list -> expr)
109 * | StringListFunExpr of (string list -> expr)
110 * | TermListFunExpr of (term list -> expr)
111 * | TacticListFunExpr of (tactic list -> expr)
112 * | ConvListFunExpr of (conv list -> expr)
113 * @end[verbatim]
114 * @end[doc]
115 *)
116 type expr =
117 (* Base types *)
118 UnitExpr of unit
119 | BoolExpr of bool
120 | IntExpr of int
121 | StringExpr of string
122 | TermExpr of term
123 | TacticExpr of tactic
124 | ConvExpr of conv
125 | AddressExpr of address
126
127 (* Uptyped tuples and functions *)
128 | ListExpr of expr list
129 | TupleExpr of expr list
130 | FunExpr of (expr -> expr)
131
132 (* Common cases are typed *)
133 | UnitFunExpr of (unit -> expr)
134 | BoolFunExpr of (bool -> expr)
135 | IntFunExpr of (int -> expr)
136 | StringFunExpr of (string -> expr)
137 | TermFunExpr of (term -> expr)
138 | TacticFunExpr of (tactic -> expr)
139 | IntTacticFunExpr of ((int -> tactic) -> expr)
140 | ConvFunExpr of (conv -> expr)
141 | AddressFunExpr of (address -> expr)
142
143 (* These functions take lists *)
144 | AddrFunExpr of (int list -> expr)
145 | StringListFunExpr of (string list -> expr)
146 | TermListFunExpr of (term list -> expr)
147 | TacticListFunExpr of (tactic list -> expr)
148 | ConvListFunExpr of (conv list -> expr)
149
150 (*
151 * The resource maps strings to values.
152 *)
153 type top_table =
154 (string, string * expr) Hashtbl.t
155
156 (************************************************************************
157 * IMPLEMENTATION *
158 ************************************************************************)
159
160 let create () =
161 Hashtbl.create 201
162
163 let add tbl (module_name,name,expr) =
164 Hashtbl.add tbl name ((String.capitalize module_name),expr)
165
166 let add_commands tbl =
167 List.iter (fun (name, expr) -> Hashtbl.add tbl name ("",expr))
168
169 let retr tbl = tbl
170
171 (*!
172 * @begin[doc]
173 * Toplevel values are added to the @Comment!resource[toploop_resource] resource.
174 * The argument has type @code{string * expr}, which includes
175 * the string name of the value, and it's value.
176 * @docoff
177 * @end[doc]
178 *)
179 let resource toploop = Imperative {
180 imp_create = create;
181 imp_add = add;
182 imp_retr = retr
183 }
184
185 (************************************************************************
186 * COMPILING *
187 ************************************************************************)
188
189 (*
190 * Right now most things are not supported.
191 *)
192 let not_supported loc str =
193 Stdpp.raise_with_loc loc (RefineError ("mptop", StringStringError ("operation is not implemented", str)))
194
195 let type_error loc str =
196 Stdpp.raise_with_loc loc (RefineError ("type error", StringError str))
197
198 (*
199 * Convert a list to a term list.
200 *)
201 let some_list_of_list f loc = function
202 ListExpr l ->
203 List.map f l
204 | _ ->
205 type_error loc "expr should be a list"
206
207 let term_expr loc = function
208 TermExpr t ->
209 t
210 | _ ->
211 type_error loc "expr should be a term"
212
213 let int_expr loc = function
214 IntExpr t ->
215 t
216 | _ ->
217 type_error loc "expr should be an int"
218
219 let string_expr loc = function
220 StringExpr t ->
221 t
222 | _ ->
223 type_error loc "expr should be a string"
224
225 let tactic_expr loc = function
226 TacticExpr t ->
227 t
228 | _ ->
229 type_error loc "expr should be a tactic"
230
231 let conv_expr loc = function
232 ConvExpr t ->
233 t
234 | _ ->
235 type_error loc "expr should be a conv"
236
237 let term_list_of_list loc = some_list_of_list (term_expr loc) loc
238 let int_list_of_list loc = some_list_of_list (int_expr loc) loc
239 let string_list_of_list loc = some_list_of_list (string_expr loc) loc
240 let tactic_list_of_list loc = some_list_of_list (tactic_expr loc) loc
241 let conv_list_of_list loc = some_list_of_list (conv_expr loc) loc
242
243 (*
244 * Want an int tactic.
245 *)
246 let int_tactic_expr loc = function
247 IntFunExpr f ->
248 (fun i ->
249 match f i with
250 TacticExpr tac ->
251 tac
252 | _ ->
253 type_error loc "int tactic expected")
254 | _ ->
255 type_error loc "int tactic expected"
256
257 (*
258 * Lookup a variable from the table.
259 *)
260 let rec mk_var_expr base loc v =
261 try snd (Hashtbl.find base v) with
262 Not_found ->
263 Stdpp.raise_with_loc loc (RefineError ("mk_var_expr", StringStringError ("undefined variable", v)))
264
265 and mk_proj_expr base loc expr =
266 let rec search modname v = function
267 (modname', expr) :: tl ->
268 if modname' = modname then
269 expr
270 else
271 search modname v tl
272 | [] ->
273 Stdpp.raise_with_loc loc (**)
274 (RefineError ("mk_proj_expr",
275 StringStringError ("undefined variable", modname ^ "." ^ v)))
276 in
277 let lookup names v =
278 match names with
279 [modname] ->
280 search modname v (Hashtbl.find_all base v)
281 | _ ->
282 Stdpp.raise_with_loc loc (**)
283 (RefineError ("mk_proj_expr", StringError "nested modules are not implemented"))
284 in
285 let rec collect names expr =
286 match expr with
287 (<:expr< $uid: name$ . $e2$ >>) ->
288 collect (name :: names) e2
289 | (<:expr< $lid: v$ >>) ->
290 lookup names v
291 | _ ->
292 not_supported loc "expr projection"
293 in
294 collect [] expr
295
296 (*
297 * For an application, we lookup the function and try to
298 * specialize the argument.
299 *)
300 and mk_apply_expr base loc f a =
301 let a = mk_expr base a in
302 match mk_expr base f with
303 FunExpr f ->
304 f a
305 | UnitFunExpr f ->
306 begin
307 match a with
308 UnitExpr () ->
309 f ()
310 | _ ->
311 type_error loc "expr should be unit"
312 end
313 | BoolFunExpr f ->
314 begin
315 match a with
316 BoolExpr a ->
317 f a
318 | _ ->
319 type_error loc "expr should be a bool"
320 end
321 | IntFunExpr f ->
322 begin
323 match a with
324 IntExpr a ->
325 f a
326 | _ ->
327 type_error loc "expr should be int"
328 end
329 | StringFunExpr f ->
330 begin
331 match a with
332 StringExpr a ->
333 f a
334 | _ ->
335 type_error loc "expr should be a string"
336 end
337 | TermFunExpr f ->
338 begin
339 match a with
340 TermExpr a ->
341 f a
342 | _ ->
343 type_error loc "expr should be a term"
344 end
345 | TacticFunExpr f ->
346 begin
347 match a with
348 TacticExpr a ->
349 f a
350 | _ ->
351 type_error loc "expr should be a tactic"
352 end
353 | IntTacticFunExpr f ->
354 f (int_tactic_expr loc a)
355 | ConvFunExpr f ->
356 begin
357 match a with
358 ConvExpr a ->
359 f a
360 | _ ->
361 type_error loc "expr should be a conversion"
362 end
363 | AddressFunExpr f ->
364 begin
365 match a with
366 AddressExpr a ->
367 f a
368 | IntExpr i ->
369 f (clause_address i)
370 | ListExpr _ ->
371 f (make_address (int_list_of_list loc a))
372 | _ ->
373 type_error loc "expr should be an address"
374 end
375 | AddrFunExpr f ->
376 f (int_list_of_list loc a)
377 | StringListFunExpr f ->
378 f (string_list_of_list loc a)
379 | TermListFunExpr f ->
380 f (term_list_of_list loc a)
381 | TacticListFunExpr f ->
382 f (tactic_list_of_list loc a)
383 | ConvListFunExpr f ->
384 f (conv_list_of_list loc a)
385 | UnitExpr _
386 | BoolExpr _
387 | IntExpr _
388 | StringExpr _
389 | TermExpr _
390 | TacticExpr _
391 | ConvExpr _
392 | AddressExpr _
393 | ListExpr _
394 | TupleExpr _ ->
395 type_error loc "expr should be a function"
396
397 (*
398 * A tuple of expressions.
399 * We only support unit for now.
400 *)
401 and mk_tuple_expr base loc = function
402 [] ->
403 UnitExpr ()
404 | _ ->
405 not_supported loc "tuple expression"
406
407 and mk_expr base expr =
408 let loc = loc_of_expr expr in
409 match expr with
410 (<:expr< $e1$ . $e2$ >> as expr) ->
411 mk_proj_expr base loc expr
412 | (<:expr< $e1$ $e2$ >>) ->
413 mk_apply_expr base loc e1 e2
414 | (<:expr< $e1$ .( $e2$ ) >>) ->
415 not_supported loc "array subscript"
416 | (<:expr< [| $list:el$ |] >>) ->
417 not_supported loc "array"
418 | (<:expr< $e1$ := $e2$ >>) ->
419 not_supported loc "assignment"
420 | (<:expr< $chr:c$ >>) ->
421 not_supported loc "char"
422 | (<:expr< ( $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$ } >>) ->
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 | (<:expr< $uid:s$ >>) ->
438 mk_var_expr base loc s
439 | MLast.ExLmd _ ->
440 not_supported loc "local module"
441 | (<:expr< match $e$ with [ $list:pwel$ ] >>) ->
442 not_supported loc "match"
443 | MLast.ExNew _ ->
444 not_supported loc "new"
445 (*
446 | (<:expr< {< $list:sel$ >} >>) ->
447 *)
448 | MLast.ExOvr _ ->
449 not_supported loc "stream"
450 (*
451 | (<:expr< { $list:eel$ } >>) ->
452 *)
453 | MLast.ExRec _ ->
454 not_supported loc "record"
455 | (<:expr< do { $list:el$ } >>) ->
456 not_supported loc "do"
457 (*
458 | (<:expr< $e$ # $i$ >>) ->
459 *)
460 | MLast.ExSnd _ ->
461 not_supported loc "class projection"
462 | (<:expr< $e1$ .[ $e2$ ] >>) ->
463 not_supported loc "string subscript"
464 | (<:expr< $str:s$ >>) ->
465 StringExpr s
466 | (<:expr< try $e$ with [ $list:pwel$ ] >>) ->
467 not_supported loc "try"
468 | (<:expr< ( $list:el$ ) >>) ->
469 mk_tuple_expr base loc el
470 | (<:expr< ( $e$ : $_$ ) >>)
471 | MLast.ExXnd (_, _, e) ->
472 mk_expr base e
473 | (<:expr< while $e$ do { $list:el$ } >>) ->
474 not_supported loc "while"
475 | MLast.ExAnt (_, e) ->
476 not_supported loc "ExAnt"
477 | MLast.ExVrn _ ->
478 not_supported loc "ExVrn"
479 | MLast.ExOlb _ ->
480 not_supported loc "ExOlb"
481 | MLast.ExLab _ ->
482 not_supported loc "ExLab"
483
484 and mk_patt base patt =
485 let loc = loc_of_patt patt in
486 match patt with
487 (<:patt< $p1$ . $p2$ >>) ->
488 not_supported loc "patt projection"
489 | (<:patt< ( $p1$ as $p2$ ) >>) ->
490 not_supported loc "patt"
491 | (<:patt< _ >>) ->
492 not_supported loc "wild pattern"
493 | (<:patt< $p1$ $p2$ >>) ->
494 not_supported loc "pattern application"
495 | (<:patt< [| $list: pl$ |] >>) ->
496 not_supported loc "array patterns"
497 | (<:patt< $chr:c$ >>) ->
498 not_supported loc "pattern char"
499 | (<:patt< $int:s$ >>) ->
500 not_supported loc "pattern int"
501 | (<:patt< $lid:v$ >>) ->
502 not_supported loc "pattern var"
503 | (<:patt< $p1$ | $p2$ >>) ->
504 not_supported loc "pattern choice"
505 | (<:patt< $p1$ .. $p2$ >>) ->
506 not_supported loc "pattern range"
507 | (<:patt< { $list:ppl$ } >>) ->
508 not_supported loc "pattern record"
509 | (<:patt< $str:s$ >>) ->
510 not_supported loc "pattern string"
511 | (<:patt< ( $list:pl$ ) >>) ->
512 not_supported loc "pattern list"
513 | (<:patt< ( $p$ : $t'$ ) >>) ->
514 not_supported loc "pattern cast"
515 | (<:patt< $uid:s$ >>) ->
516 not_supported loc "pattern uid"
517 | MLast.PaAnt (_, p) ->
518 not_supported loc "pattern PaAnt"
519 | MLast.PaXnd _ ->
520 not_supported loc "patterm PaXnd"
521 | MLast.PaVrn _ ->
522 not_supported loc "patterm PaVrn"
523 | MLast.PaOlb _ ->
524 not_supported loc "patterm PaOlb"
525 | MLast.PaLab _ ->
526 not_supported loc "patterm PaLab"
527 | MLast.PaFlo _ ->
528 not_supported loc "patterm PaFlo"
529
530 and mk_type base t =
531 let loc = loc_of_ctyp t in
532 match t with
533 (<:ctyp< $t1$ . $t2$ >>) ->
534 not_supported loc "type projection"
535 | (<:ctyp< $t1$ as $t2$ >>) ->
536 not_supported loc "type"
537 | (<:ctyp< _ >>) ->
538 not_supported loc "type wildcard"
539 | (<:ctyp< $t1$ $t2$ >>) ->
540 not_supported loc "type application"
541 | (<:ctyp< $t1$ -> $t2$ >>) ->
542 not_supported loc "type function"
543 (*
544 | (<:ctyp< # $i$ >>) ->
545 *)
546 | MLast.TyCls _ ->
547 not_supported loc "type method"
548 | (<:ctyp< $lid:s$ >>) ->
549 not_supported loc "type var"
550 | (<:ctyp< '$s$ >>) ->
551 not_supported loc "type param"
552 | (<:ctyp< $t1$ == $t2$ >>) ->
553 not_supported loc "type equality"
554 (*
555 | (<:ctyp< < $list:stl$ $dd:b$ > >>) ->
556 *)
557 | MLast.TyObj (loc, _, _) ->
558 not_supported loc "type class"
559 | (<:ctyp< { $list:sbtl$ } >>) ->
560 not_supported loc "type record"
561 | (<:ctyp< [ $list:stll$ ] >>) ->
562 not_supported loc "type list"
563 | (<:ctyp< ( $list:tl$ ) >>) ->
564 not_supported loc "type product"
565 | (<:ctyp< $uid:s$ >>) ->
566 not_supported loc "type constructor var"
567 | MLast.TyXnd (_, _, t) ->
568 mk_type base t
569 | MLast.TyVrn _ ->
570 not_supported loc "type constructor Vrn"
571 | MLast.TyOlb _ ->
572 not_supported loc "type constructor Olb"
573 | MLast.TyLab _ ->
574 not_supported loc "type constructor Lab"
575
576 and mk_sig_item base si =
577 let loc = loc_of_sig_item si in
578 match si with
579 (*
580 (<:sig_item< class $list:ctl$ >>) ->
581 *)
582 MLast.SgCls _
583 | MLast.SgClt _ ->
584 not_supported loc "sig class"
585 | (<:sig_item< declare $list:sil$ end >>) ->
586 mk_sig_item base (List_util.last sil)
587 | (<:sig_item< exception $s$ of $list:tl$ >>) ->
588 not_supported loc "sig exception"
589 | (<:sig_item< external $s$ : $t$ = $list:sl$ >>) ->
590 not_supported loc "sig external"
591 | SgInc (_, mt) ->
592 not_supported loc "sig SgInc"
593 | (<:sig_item< module $s$ : $mt$ >>) ->
594 not_supported loc "sig module"
595 | (<:sig_item< module type $s$ = $mt$ >>) ->
596 not_supported loc "sig module type"
597 | (<:sig_item< open $sl$ >>) ->
598 not_supported loc "sig open"
599 | (<:sig_item< type $list:tdl$ >>) ->
600 not_supported loc "sig type"
601 | (<:sig_item< value $s$ : $t$ >>) ->
602 not_supported loc "sig value"
603 | MLast.SgDir _ ->
604 not_supported loc "sig dir"
605
606 and mk_str_item base si =
607 let loc = loc_of_str_item si in
608 match si with
609 MLast.StCls _
610 | MLast.StClt _ ->
611 not_supported loc "str class"
612 | (<:str_item< declare $list:stl$ end >>) ->
613 mk_str_item base (List_util.last stl)
614 | (<:str_item< exception $s$ of $list:tl$ >>) ->
615 not_supported loc "str exception"
616 | (<:str_item< $exp:e$ >>) ->
617 mk_expr base e
618 | (<:str_item< external $s$ : $t$ = $list:sl$ >>) ->
619 not_supported loc "str external"
620 | (<:str_item< module $s$ = $me$ >>) ->
621 not_supported loc "str module"
622 | (<:str_item< module type $s$ = $mt$ >>) ->
623 not_supported loc "str module type"
624 | (<:str_item< open $sl$ >>) ->
625 not_supported loc "str module open"
626 | (<:str_item< type $list:tdl$ >>) ->
627 not_supported loc "str type"
628 | (<:str_item< value $rec:b$ $list:pel$ >>) ->
629 not_supported loc "str let"
630 | MLast.StDir _ ->
631 not_supported loc "str dir"
632 | MLast.StInc _ ->
633 not_supported loc "str include"
634
635 and mk_module_type base mt =
636 let loc = loc_of_module_type mt in
637 match mt with
638 (<:module_type< $mt1$ . $mt2$ >>) ->
639 not_supported loc "module type projection"
640 | (<:module_type< $mt1$ $mt2$ >>) ->
641 not_supported loc "module type application"
642 | (<:module_type< functor ( $s$ : $mt1$ ) -> $mt2$ >>) ->
643 not_supported loc "module type functor"
644 | (<:module_type< $lid:i$ >>)
645 | (<:module_type< $uid:i$ >>) ->
646 not_supported loc "module type var"
647 | (<:module_type< sig $list:sil$ end >>) ->
648 not_supported loc "module type sig"
649 | (<:module_type< $mt$ with $list:wcl$ >>) ->
650 not_supported loc "module type constraint"
651
652 and mk_wc base = function
653 WcTyp (loc, sl1, sl2, t) ->
654 not_supported loc "with clause type"
655 | WcMod (loc, sl1, mt) ->
656 not_supported loc "with clause module"
657
658 and mk_module_expr base me =
659 let loc = loc_of_module_expr me in
660 match me with
661 (<:module_expr< $me1$ . $me2$ >>) ->
662 not_supported loc "module expr projection"
663 | (<:module_expr< $me1$ $me2$ >>) ->
664 not_supported loc "module expr application"
665 | (<:module_expr< functor ( $s$ : $mt$ ) -> $me$ >>) ->
666 not_supported loc "module expr functor"
667 | (<:module_expr< struct $list:sil$ end >>) ->
668 not_supported loc "module expr struct"
669 | (<:module_expr< ( $me$ : $mt$) >>) ->
670 not_supported loc "module expr type"
671 | (<:module_expr< $uid:i$ >>) ->
672 not_supported loc "module expr id"
673
674 (************************************************************************
675 * RESOURCES *
676 ************************************************************************)
677
678 (*
679 * Include the common library functions.
680 *)
681 let int_int_fun_int_expr f =
682 IntFunExpr (fun i -> IntFunExpr (fun j -> IntExpr (f i j)))
683
684 let cons_expr =
685 FunExpr (fun e1 ->
686 FunExpr (fun e2 ->
687 match e2 with
688 ListExpr e2 ->
689 ListExpr (e1 :: e2)
690 | _ ->
691 raise (RefineError ("cons_expr", StringError "type mismatch"))))
692
693 let resource toploop +=
694 ["Pervasives", "+", int_int_fun_int_expr ( + );
695 "Pervasives", "-", int_int_fun_int_expr ( - );
696 "Pervasives", "*", int_int_fun_int_expr ( * );
697 "Pervasives", "/", int_int_fun_int_expr ( / );
698 "Pervasives", "::", cons_expr;
699 "Pervasives", "()", UnitExpr ();
700 "Pervasives", "[]", ListExpr [];
701 "Pervasives", "True", BoolExpr true;
702 "Pervasives", "False", BoolExpr false]
703
704 let expr_of_ocaml_expr = mk_expr
705 let expr_of_ocaml_str_item = mk_str_item
706
707 (*
708 * -*-
709 * Local Variables:
710 * Caml-master: "refiner"
711 * End:
712 * -*-
713 *)

Properties

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

  ViewVC Help
Powered by ViewVC 1.1.26