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

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

Parent Directory Parent Directory | Revision Log Revision Log


Revision 3086 - (hide 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 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 jyh 3058 (*!
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 jyh 2630 resource (string * expr, top_table, top_data, unit) toploop_resource
168 jyh 2494
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 jyh 2577 let _ = collect "." [] data in
197 jyh 2494 hash
198    
199     (*
200     * Wrap up the joiner.
201     *)
202 jyh 2629 let join_resource base1 base2 =
203     Join (base1, base2)
204 jyh 2494
205 jyh 2629 let extract_resource data =
206 jyh 2494 collect_table data
207    
208 jyh 2629 let improve_resource data (name, expr) =
209     Expr (name, expr, data)
210 jyh 2494
211 jyh 2629 let close_resource data mod_name =
212     Label (String.capitalize mod_name, data)
213 jyh 2494
214     (************************************************************************
215     * COMPILING *
216     ************************************************************************)
217    
218     (*
219     * Right now most things are not supported.
220     *)
221     let not_supported loc str =
222 nogin 2502 Stdpp.raise_with_loc loc (RefineError ("mptop", StringStringError ("operation is not implemented", str)))
223 jyh 2494
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 nogin 2772 collect (name :: names) e2
324 jyh 2494 | (<: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 jyh 2811 | AddressFunExpr f ->
399     begin
400     match a with
401     AddressExpr a ->
402     f a
403 nogin 3086 | IntExpr i ->
404     f (clause_address i)
405 nogin 3085 | ListExpr _ ->
406     f (make_address (int_list_of_list loc a))
407 jyh 2811 | _ ->
408 nogin 3085 type_error loc "expr should be an address"
409 jyh 2811 end
410 jyh 2494 | 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 jyh 2811 | AddressExpr _
428 jyh 2494 | 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 jyh 2525 mk_var_expr base loc s
514 jyh 2494 | (<:expr< while $e$ do $list:el$ done >>) ->
515     not_supported loc "while"
516     | MLast.ExAnt (_, e) ->
517     not_supported loc "ExAnt"
518 jyh 2629 | MLast.ExXnd (_, _, e) ->
519     mk_expr base e
520 jyh 2494
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 jyh 2629 | MLast.PaXnd _ ->
557     not_supported loc "patterm PaXnd"
558 jyh 2494
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 jyh 2577 (*
584 jyh 2494 | (<:ctyp< < $list:stl$ $dd:b$ > >>) ->
585 jyh 2577 *)
586     | MLast.TyObj (loc, _, _) ->
587 jyh 2494 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 jyh 2629 | MLast.TyXnd (_, _, t) ->
597     mk_type base t
598 jyh 2494
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 nogin 2859 | (<:sig_item< type $list:tdl$ >>) ->
623 jyh 2494 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 nogin 2859 | (<:str_item< type $list:tdl$ >>) ->
651 jyh 2494 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 jyh 2525 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 jyh 2494 let values =
715     ["+", int_int_fun_int_expr ( + );
716     "-", int_int_fun_int_expr ( - );
717     "*", int_int_fun_int_expr ( * );
718 jyh 2525 "/", int_int_fun_int_expr ( / );
719     "::", cons_expr;
720     "()", UnitExpr ();
721     "[]", ListExpr [];
722 jyh 2549 "True", BoolExpr true;
723     "False", BoolExpr false]
724 jyh 2494
725 jyh 2525
726 jyh 2494 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 jyh 2629 Mp_resource.create (**)
734     { resource_join = join_resource;
735     resource_extract = extract_resource;
736     resource_improve = improve_resource;
737 jyh 2630 resource_improve_arg = Mp_resource.improve_arg_fail "toploop_resource";
738 jyh 2629 resource_close = close_resource
739     }
740     (add_resources Empty values)
741 jyh 2494
742 jyh 2629 let get_resource modname =
743     Mp_resource.find toploop_resource modname
744 jyh 2494
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