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

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

Parent Directory Parent Directory | Revision Log Revision Log


Revision 3086 - (show annotations) (download)
Sun Oct 22 20:58:58 2000 UTC (20 years, 9 months ago) by nogin
File size: 23509 byte(s)
1) Proved some *Formation rules that used to be primitive (using in part
Alexei's cut rule idea). We should probably continue this job and
eliminate "primitiveness" from as much Formation rules as we can.

2) unitSqequal rule should be primitive

3) mk: don't pass -j1 to make when MAKE_JOBS = 1

4) In MP toploop, when a non-negatice integer is found where
an address was expected, that integer is considered to be
the hypothesis number. This enables applying primitive rules
from the MP toploop.

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

Properties

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

  ViewVC Help
Powered by ViewVC 1.1.26