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

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

Parent Directory Parent Directory | Revision Log Revision Log


Revision 3085 - (hide 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 jyh 3058 (*!
2     * @spelling{mptop toplevel}
3 jyh 2494 *
4 jyh 3058 * @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 jyh 2494 * ----------------------------------------------------------------
16     *
17 jyh 3058 * @begin[license]
18     *
19 jyh 2494 * 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 jyh 2525 *
28 jyh 2494 * 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 jyh 2525 *
33 jyh 2494 * 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 jyh 2525 *
38 jyh 2494 * 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 jyh 2525 *
42 jyh 2494 * Author: Jason Hickey
43 jyh 3058 * @email{jyh@cs.caltech.edu}
44     *
45     * @end[license]
46 jyh 2494 *)
47    
48 jyh 3058 (*!
49     * @begin[doc]
50     * @parents
51     * @end[doc]
52     *)
53     include Summary
54     (*! @docoff *)
55    
56 jyh 2494 open MLast
57    
58     open Refiner.Refiner.TermType
59 jyh 2911 open Refiner.Refiner.TermAddr
60 jyh 2494 open Refiner.Refiner.RefineError
61     open Mp_resource
62    
63 jyh 2743 open Tactic_type.Tacticals
64     open Tactic_type.Conversionals
65 jyh 2494
66     (************************************************************************
67     * TYPES *
68     ************************************************************************)
69    
70 jyh 3058 (*!
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 jyh 2494 *)
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 jyh 2811 | AddressExpr of address
122 jyh 2494
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 jyh 2811 | AddressFunExpr of (address -> expr)
138 jyh 2494
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 jyh 3058 (*!
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 jyh 2630 resource (string * expr, top_table, top_data, unit) toploop_resource
167 jyh 2494
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 jyh 2577 let _ = collect "." [] data in
196 jyh 2494 hash
197    
198     (*
199     * Wrap up the joiner.
200     *)
201 jyh 2629 let join_resource base1 base2 =
202     Join (base1, base2)
203 jyh 2494
204 jyh 2629 let extract_resource data =
205 jyh 2494 collect_table data
206    
207 jyh 2629 let improve_resource data (name, expr) =
208     Expr (name, expr, data)
209 jyh 2494
210 jyh 2629 let close_resource data mod_name =
211     Label (String.capitalize mod_name, data)
212 jyh 2494
213     (************************************************************************
214     * COMPILING *
215     ************************************************************************)
216    
217     (*
218     * Right now most things are not supported.
219     *)
220     let not_supported loc str =
221 nogin 2502 Stdpp.raise_with_loc loc (RefineError ("mptop", StringStringError ("operation is not implemented", str)))
222 jyh 2494
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 nogin 2772 collect (name :: names) e2
323 jyh 2494 | (<: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 jyh 2811 | AddressFunExpr f ->
398     begin
399     match a with
400     AddressExpr a ->
401     f a
402 nogin 3085 | ListExpr _ ->
403     f (make_address (int_list_of_list loc a))
404 jyh 2811 | _ ->
405 nogin 3085 type_error loc "expr should be an address"
406 jyh 2811 end
407 jyh 2494 | 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 jyh 2811 | AddressExpr _
425 jyh 2494 | 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 jyh 2525 mk_var_expr base loc s
511 jyh 2494 | (<:expr< while $e$ do $list:el$ done >>) ->
512     not_supported loc "while"
513     | MLast.ExAnt (_, e) ->
514     not_supported loc "ExAnt"
515 jyh 2629 | MLast.ExXnd (_, _, e) ->
516     mk_expr base e
517 jyh 2494
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 jyh 2629 | MLast.PaXnd _ ->
554     not_supported loc "patterm PaXnd"
555 jyh 2494
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 jyh 2577 (*
581 jyh 2494 | (<:ctyp< < $list:stl$ $dd:b$ > >>) ->
582 jyh 2577 *)
583     | MLast.TyObj (loc, _, _) ->
584 jyh 2494 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 jyh 2629 | MLast.TyXnd (_, _, t) ->
594     mk_type base t
595 jyh 2494
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 nogin 2859 | (<:sig_item< type $list:tdl$ >>) ->
620 jyh 2494 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 nogin 2859 | (<:str_item< type $list:tdl$ >>) ->
648 jyh 2494 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 jyh 2525 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 jyh 2494 let values =
712     ["+", int_int_fun_int_expr ( + );
713     "-", int_int_fun_int_expr ( - );
714     "*", int_int_fun_int_expr ( * );
715 jyh 2525 "/", int_int_fun_int_expr ( / );
716     "::", cons_expr;
717     "()", UnitExpr ();
718     "[]", ListExpr [];
719 jyh 2549 "True", BoolExpr true;
720     "False", BoolExpr false]
721 jyh 2494
722 jyh 2525
723 jyh 2494 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 jyh 2629 Mp_resource.create (**)
731     { resource_join = join_resource;
732     resource_extract = extract_resource;
733     resource_improve = improve_resource;
734 jyh 2630 resource_improve_arg = Mp_resource.improve_arg_fail "toploop_resource";
735 jyh 2629 resource_close = close_resource
736     }
737     (add_resources Empty values)
738 jyh 2494
739 jyh 2629 let get_resource modname =
740     Mp_resource.find toploop_resource modname
741 jyh 2494
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