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

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

Parent Directory Parent Directory | Revision Log Revision Log


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

let resource <name> = <expr>

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

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

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