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

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

Parent Directory Parent Directory | Revision Log Revision Log


Revision 3292 - (show 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 (*!
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_table =
151 (string, string * expr) Hashtbl.t
152
153 (************************************************************************
154 * IMPLEMENTATION *
155 ************************************************************************)
156
157 let create () =
158 Hashtbl.create 201
159
160 let add tbl (module_name,name,expr) =
161 Hashtbl.add tbl name (module_name,expr)
162
163 let add_commands tbl =
164 List.iter (fun (name, expr) -> Hashtbl.add tbl name ("",expr))
165
166 let retr tbl = tbl
167
168 (*!
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
182 (************************************************************************
183 * COMPILING *
184 ************************************************************************)
185
186 (*
187 * Right now most things are not supported.
188 *)
189 let not_supported loc str =
190 Stdpp.raise_with_loc loc (RefineError ("mptop", StringStringError ("operation is not implemented", str)))
191
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 search modname v (Hashtbl.find_all base v)
278 | _ ->
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 collect (name :: names) e2
286 | (<: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 | AddressFunExpr f ->
361 begin
362 match a with
363 AddressExpr a ->
364 f a
365 | IntExpr i ->
366 f (clause_address i)
367 | ListExpr _ ->
368 f (make_address (int_list_of_list loc a))
369 | _ ->
370 type_error loc "expr should be an address"
371 end
372 | 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 | AddressExpr _
390 | 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 mk_var_expr base loc s
476 | (<:expr< while $e$ do $list:el$ done >>) ->
477 not_supported loc "while"
478 | MLast.ExAnt (_, e) ->
479 not_supported loc "ExAnt"
480 | MLast.ExXnd (_, _, e) ->
481 mk_expr base e
482
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 | MLast.PaXnd _ ->
519 not_supported loc "patterm PaXnd"
520
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 (*
546 | (<:ctyp< < $list:stl$ $dd:b$ > >>) ->
547 *)
548 | MLast.TyObj (loc, _, _) ->
549 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 | MLast.TyXnd (_, _, t) ->
559 mk_type base t
560
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 | (<:sig_item< type $list:tdl$ >>) ->
585 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 | (<:str_item< type $list:tdl$ >>) ->
613 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 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 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
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